Duhamel formulas for the Banach-algebra exponential

This file expresses a finite increment of the exponential in a possibly noncommutative real Banach algebra as an integral. Unlike a first-order derivative formula, the identity is exact for every increment. It also derives the corresponding integral formula for the Fréchet derivative.

Main results

• intervalIntegrable_exp_smul_mul_mul_exp_smul: a three-factor exponential integrand is interval integrable.
• exp_add_sub_exp_eq_integral: exp (x + h) - exp x is the integral of exp ((1 - t) (x + h)) * h * exp (t x) over the unit interval.
• TauCeti.expFDeriv_apply_eq_integral: the Fréchet derivative is the corresponding Duhamel integral linear in the increment.

References

• Lie groups and the Lie algebra correspondence roadmap, Deliverable A, Layer 1, "The conjugation formulas".
• R. M. Wilcox, Exponential Operators and Parameter Differentiation in Quantum Physics, Journal of Mathematical Physics 8 (1967), 962–982.

theorem TauCeti.intervalIntegrable_exp_smul_mul_mul_exp_smul {A : Type u_1} [NormedRing A] [NormedAlgebra ℝ A] [CompleteSpace A] (x y z : A) : IntervalIntegrable (fun (t : ℝ) => NormedSpace.exp ((1 - t) • x) * y * NormedSpace.exp (t • z)) MeasureTheory.volume 0 1

The three-factor exponential integrand underlying Duhamel's formulas is interval integrable.

theorem TauCeti.exp_add_sub_exp_eq_integral {A : Type u_1} [NormedRing A] [NormedAlgebra ℝ A] [CompleteSpace A] (x h : A) : NormedSpace.exp (x + h) - NormedSpace.exp x = ∫ (t : ℝ) in 0..1, NormedSpace.exp ((1 - t) • (x + h)) * h * NormedSpace.exp (t • x)

Duhamel's exact finite-increment formula for the exponential in a possibly noncommutative real Banach algebra.

The Fréchet derivative series

The Fréchet derivative of the exponential in a possibly noncommutative Banach algebra over a normed characteristic-zero field with continuous rational scalar action is the convergent series whose nth homogeneous contribution inserts the tangent vector in every position among n copies of the base point.

Main definitions

• TauCeti.expFDerivTerm: the degree-n insertion term in the derivative series.
• TauCeti.expFDeriv: the sum of the derivative series as a continuous linear map.

Main results

• TauCeti.expFDerivTerm_apply: the pointwise insertion formula for one term.
• TauCeti.expFDerivTerm_eq_derivSeries: the identification with Mathlib's formal derivative series.
• TauCeti.expFDeriv_eq_tsum: the operator-valued defining series.
• TauCeti.summable_expFDerivTerm: summability of the operator-valued series.
• TauCeti.summable_expFDerivTerm_apply: pointwise summability of the insertion series.
• TauCeti.expFDeriv_apply: the pointwise formula for the summed operator.
• TauCeti.hasStrictFDerivAt_exp: the exponential has strict derivative expFDeriv 𝕂 x at x.
• TauCeti.hasFDerivAt_exp: the corresponding ordinary Fréchet derivative statement.
• TauCeti.fderiv_exp: the derivative expressed using fderiv.
• TauCeti.expFDeriv_eq_smul_one: the commutative-algebra specialization.
• TauCeti.expFDeriv_zero: at zero, the formal derivative-series operator is the identity.

noncomputable def TauCeti.expFDerivTerm (𝕂 : Type u_3) [NontriviallyNormedField 𝕂] {R : Type u_4} [NormedRing R] [NormedAlgebra 𝕂 R] (x : R) (n : ℕ) : R →L[𝕂] R

The degree-n contribution to the Fréchet derivative of the Banach-algebra exponential. Applied to y, this is (n + 1)!⁻¹ • ∑ i < n + 1, x ^ (n - i) * y * x ^ i.

Equations

• TauCeti.expFDerivTerm 𝕂 x n = (↑(n + 1).factorial)⁻¹ • ∑ i ∈ Finset.range (n + 1), MulOpposite.op (x ^ i) • x ^ (n - i) • ContinuousLinearMap.id 𝕂 R

noncomputable def TauCeti.expFDeriv (𝕂 : Type u_3) [NontriviallyNormedField 𝕂] {R : Type u_4} [NormedRing R] [NormedAlgebra 𝕂 R] (x : R) : R →L[𝕂] R

The sum of the Fréchet-derivative series of the Banach-algebra exponential. It converges under the hypotheses of summable_expFDerivTerm; as usual for tsum, it has the junk value zero when the series is not summable.

Equations

• TauCeti.expFDeriv 𝕂 x = ∑' (n : ℕ), TauCeti.expFDerivTerm 𝕂 x n

@[simp]

theorem TauCeti.expFDerivTerm_apply {𝕂 : Type u_1} {R : Type u_2} [NontriviallyNormedField 𝕂] [NormedRing R] [NormedAlgebra 𝕂 R] (x y : R) (n : ℕ) : (expFDerivTerm 𝕂 x n) y = (↑(n + 1).factorial)⁻¹ • ∑ i ∈ Finset.range (n + 1), x ^ (n - i) * y * x ^ i

Evaluating a homogeneous derivative term inserts the tangent vector in every possible position.

theorem TauCeti.expFDeriv_eq_tsum {𝕂 : Type u_1} {R : Type u_2} [NontriviallyNormedField 𝕂] [NormedRing R] [NormedAlgebra 𝕂 R] (x : R) : expFDeriv 𝕂 x = ∑' (n : ℕ), expFDerivTerm 𝕂 x n

The operator-valued defining series for expFDeriv.

theorem TauCeti.expFDerivTerm_eq_derivSeries {𝕂 : Type u_1} {R : Type u_2} [NontriviallyNormedField 𝕂] [NormedRing R] [NormedAlgebra 𝕂 R] (x : R) (n : ℕ) : expFDerivTerm 𝕂 x n = ((NormedSpace.expSeries 𝕂 R).derivSeries n) fun (x_1 : Fin n) => x

The explicit insertion term is the corresponding term of Mathlib's derivative series for the exponential formal multilinear series.

theorem TauCeti.summable_expFDerivTerm {𝕂 : Type u_1} {R : Type u_2} [NontriviallyNormedField 𝕂] [CharZero 𝕂] [ContinuousSMul ℚ 𝕂] [NormedRing R] [NormedAlgebra 𝕂 R] [CompleteSpace R] (x : R) : Summable (expFDerivTerm 𝕂 x)

The operator-valued derivative series is summable.

theorem TauCeti.summable_expFDerivTerm_apply {𝕂 : Type u_1} {R : Type u_2} [NontriviallyNormedField 𝕂] [CharZero 𝕂] [ContinuousSMul ℚ 𝕂] [NormedRing R] [NormedAlgebra 𝕂 R] [CompleteSpace R] (x y : R) : Summable fun (n : ℕ) => (expFDerivTerm 𝕂 x n) y

Applying the derivative terms to a fixed tangent vector gives a summable series.

@[simp]

theorem TauCeti.expFDeriv_apply {𝕂 : Type u_1} {R : Type u_2} [NontriviallyNormedField 𝕂] [CharZero 𝕂] [ContinuousSMul ℚ 𝕂] [NormedRing R] [NormedAlgebra 𝕂 R] [CompleteSpace R] (x y : R) : (expFDeriv 𝕂 x) y = ∑' (n : ℕ), (expFDerivTerm 𝕂 x n) y

The summed derivative operator takes a tangent vector to the corresponding insertion series.

theorem TauCeti.hasFDerivAt_exp {𝕂 : Type u_1} {R : Type u_2} [NontriviallyNormedField 𝕂] [CharZero 𝕂] [ContinuousSMul ℚ 𝕂] [NormedRing R] [NormedAlgebra 𝕂 R] [CompleteSpace R] (x : R) : HasFDerivAt NormedSpace.exp (expFDeriv 𝕂 x) x

The exponential in a possibly noncommutative Banach algebra has the convergent insertion sum expFDeriv 𝕂 x as its Fréchet derivative at x.

theorem TauCeti.hasStrictFDerivAt_exp {𝕂 : Type u_1} {R : Type u_2} [NontriviallyNormedField 𝕂] [CharZero 𝕂] [ContinuousSMul ℚ 𝕂] [NormedRing R] [NormedAlgebra 𝕂 R] [CompleteSpace R] (x : R) : HasStrictFDerivAt NormedSpace.exp (expFDeriv 𝕂 x) x

The strict Fréchet-derivative form of hasFDerivAt_exp.

@[simp]

theorem TauCeti.fderiv_exp {𝕂 : Type u_1} {R : Type u_2} [NontriviallyNormedField 𝕂] [CharZero 𝕂] [ContinuousSMul ℚ 𝕂] [NormedRing R] [NormedAlgebra 𝕂 R] [CompleteSpace R] (x : R) : fderiv 𝕂 NormedSpace.exp x = expFDeriv 𝕂 x

The Fréchet derivative of the exponential in a possibly noncommutative Banach algebra is the convergent insertion sum.

@[simp]

theorem TauCeti.expFDeriv_eq_smul_one {𝕂 : Type u_3} {R : Type u_4} [NontriviallyNormedField 𝕂] [CharZero 𝕂] [ContinuousSMul ℚ 𝕂] [NormedCommRing R] [NormedAlgebra 𝕂 R] [CompleteSpace R] (x : R) : expFDeriv 𝕂 x = NormedSpace.exp x • 1

In a commutative Banach algebra, the insertion sum agrees with scalar multiplication by the exponential.

@[simp]

theorem TauCeti.expFDeriv_zero {𝕂 : Type u_3} {R : Type u_4} [NontriviallyNormedField 𝕂] [NormedRing R] [NormedAlgebra 𝕂 R] : expFDeriv 𝕂 0 = 1

At zero, the formal derivative-series operator is the identity continuous linear map.

theorem TauCeti.expFDeriv_apply_eq_integral {A : Type u_3} [NormedRing A] [NormedAlgebra ℝ A] [CompleteSpace A] {𝕂 : Type u_4} [NontriviallyNormedField 𝕂] [NormedAlgebra ℝ 𝕂] [NormedAlgebra 𝕂 A] [IsScalarTower ℝ 𝕂 A] (x y : A) : (expFDeriv 𝕂 x) y = ∫ (t : ℝ) in 0..1, NormedSpace.exp ((1 - t) • x) * y * NormedSpace.exp (t • x)

The Fréchet derivative of the noncommutative exponential, applied to y, is its Duhamel integral.