The closed form of the Banach-algebra exponential derivative

This file identifies the Fréchet derivative of the noncommutative exponential with the regularized commutator quotient, followed by left multiplication by exp x.

Main results

• TauCeti.Lie.expFDeriv_apply_eq_exp_mul_banachDexpFactor: the pointwise formula.
• TauCeti.Lie.expFDeriv_eq_exp_mul_banachDexpFactor: the bundled operator formula.
• TauCeti.Lie.fderiv_exp_eq_exp_mul_banachDexpFactor: the corresponding fderiv formula.
• TauCeti.Lie.fderiv_exp_apply_eq_exp_mul_integral: the pointwise integral formula.

References

• Lie groups and the Lie algebra correspondence roadmap, Deliverable A, Layer 1, "The conjugation formulas".

theorem TauCeti.Lie.expFDeriv_apply_eq_exp_mul_banachDexpFactor {R : Type u_1} [NormedRing R] [NormedAlgebra ℝ R] [CompleteSpace R] {𝕂 : Type u_2} [NontriviallyNormedField 𝕂] [NormedAlgebra ℝ 𝕂] [NormedAlgebra 𝕂 R] [IsScalarTower ℝ 𝕂 R] (x y : R) : (expFDeriv 𝕂 x) y = NormedSpace.exp x * (banachDexpFactor x) y

The exponential derivative in direction y is left multiplication by exp x applied to the regularized commutator factor.

theorem TauCeti.Lie.expFDeriv_eq_exp_mul_banachDexpFactor {R : Type u_1} [NormedRing R] [NormedAlgebra ℝ R] [CompleteSpace R] (x : R) : expFDeriv ℝ x = (ContinuousLinearMap.mul ℝ R) (NormedSpace.exp x) ∘SL banachDexpFactor x

The Fréchet derivative is left multiplication by exp x composed with the regularized commutator factor.

theorem TauCeti.Lie.fderiv_exp_eq_exp_mul_banachDexpFactor {R : Type u_1} [NormedRing R] [NormedAlgebra ℝ R] [CompleteSpace R] (x : R) : fderiv ℝ NormedSpace.exp x = (ContinuousLinearMap.mul ℝ R) (NormedSpace.exp x) ∘SL banachDexpFactor x

The Fréchet derivative of the Banach-algebra exponential is left multiplication by exp x composed with (1 - exp (-ad x)) / ad x.

theorem TauCeti.Lie.fderiv_exp_apply_eq_exp_mul_integral {R : Type u_1} [NormedRing R] [NormedAlgebra ℝ R] [CompleteSpace R] {𝕂 : Type u_2} [NontriviallyNormedField 𝕂] [NormedAlgebra ℝ 𝕂] [NormedAlgebra 𝕂 R] [IsScalarTower ℝ 𝕂 R] (x y : R) : (fderiv 𝕂 NormedSpace.exp x) y = NormedSpace.exp x * ∫ (t : ℝ) in 0..1, NormedSpace.exp (-(t • x)) * y * NormedSpace.exp (t • x)

The Fréchet derivative of the Banach-algebra exponential, applied to y, is left multiplication by exp x applied to the integral of conjugations along the exponential line.