Exponentials in normed algebras

This file records basic facts about the exponential in normed algebras, including the specialization to continuous linear endomorphisms of a real normed space: the norm bound ‖exp x‖ ≤ Real.exp ‖x‖, exponential bounds for power-bounded operators, the exponential of a scalar multiple of the identity, and the Duhamel identity exp (t • B) x - x = ∫₀ᵗ exp (u • B) (B x) du for the orbits of a bounded operator.

theorem TauCeti.norm_exp_le_exp_norm {𝔸 : Type u_1} [NormedRing 𝔸] [NormedAlgebra ℚ 𝔸] (h_one : ‖1‖ ≤ 1) (x : 𝔸) : ‖NormedSpace.exp x‖ ≤ Real.exp ‖x‖

In a normed algebra whose unit has norm at most one, the exponential is norm-bounded by the scalar exponential of the norm: ‖exp x‖ ≤ Real.exp ‖x‖.

theorem TauCeti.norm_exp_smul_le {X : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] (A : X →L[ℝ] X) (t : ℝ) : ‖NormedSpace.exp (t • A)‖ ≤ Real.exp (‖A‖ * |t|)

The exponential of a real scalar multiple of a bounded operator satisfies ‖exp (t A)‖ ≤ exp (‖A‖ |t|).

theorem TauCeti.exp_add_smul {X : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (A : X →L[ℝ] X) (s t : ℝ) : NormedSpace.exp ((s + t) • A) = NormedSpace.exp (s • A) ∘SL NormedSpace.exp (t • A)

Exponentials of real scalar multiples of the same bounded operator split over addition.

theorem ContinuousLinearMap.norm_exp_smul_le_mul_exp_of_norm_pow_le {X : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {B : X →L[ℝ] X} {M s : ℝ} (hs : 0 ≤ s) (hpow : ∀ (n : ℕ), ‖B ^ n‖ ≤ M) : ‖NormedSpace.exp (s • B)‖ ≤ M * Real.exp s

If every power of a bounded operator B has norm at most M, then ‖exp (s B)‖ ≤ M exp s for every s ≥ 0.

@[simp]

theorem ContinuousLinearMap.exp_smul_one {X : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] (c : ℝ) : NormedSpace.exp (c • 1) = Real.exp c • 1

The exponential of a real scalar multiple of the identity operator is the corresponding scalar exponential times the identity.

theorem ContinuousLinearMap.norm_exp_smul_one_le {X : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] (c : ℝ) : ‖NormedSpace.exp (c • 1)‖ ≤ Real.exp c

The norm of the exponential of a real scalar multiple of the identity operator is at most the corresponding scalar exponential.

theorem ContinuousLinearMap.exp_smul_apply_sub_eq_intervalIntegral {X : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (B : X →L[ℝ] X) (t : ℝ) (x : X) : (NormedSpace.exp (t • B)) x - x = ∫ (u : ℝ) in 0..t, (NormedSpace.exp (u • B)) (B x)

The Duhamel identity for the exponential of a bounded operator. For B : X →L[ℝ] X, exp (t B) x - x = ∫₀ᵗ exp (u B) (B x) du.

This is the fundamental theorem of calculus applied to the differentiable orbit u ↦ exp (u B) x, whose derivative is the continuous function u ↦ exp (u B) (B x).

theorem ContinuousLinearMap.exp_smul_apply_of_apply_eq_smul {𝕜 : Type u_3} [RCLike 𝕜] {Y : Type u_4} [NormedAddCommGroup Y] [NormedSpace 𝕜 Y] [CompleteSpace Y] (B : Y →L[𝕜] Y) {x : Y} {μ : 𝕜} (hx : B x = μ • x) (t : 𝕜) : (NormedSpace.exp (t • B)) x = NormedSpace.exp (t * μ) • x

The exponential of an operator acts exponentially on an eigenvector. If B x = μ • x, then exp (t B) x = exp (t μ) • x. The statement also covers x = 0, without requiring a bundled Module.End.HasEigenvector witness.