The local Baker--Campbell--Hausdorff map

This file defines the germ at (0, 0) represented by logOneAdd (exp x * exp y - 1) in a complete real normed algebra. Using a germ records that this expression is a local logarithm; its values away from the origin have no mathematical role.

The exponential of this germ is the product of the two exponentials. Its restrictions to either coordinate axis are the identity germ, and its chosen representative is analytic at the origin.

Main declarations

• NormedSpace.localBCH: the local Baker--Campbell--Hausdorff germ.
• NormedSpace.localBCH_def: its defining representative equation.
• NormedSpace.localBCH_sliceLeft and NormedSpace.localBCH_sliceRight: the endpoint equations.
• NormedSpace.localBCH_map_exp: the local exponential equation.
• NormedSpace.analyticAt_localBCH_representative: the defining representative is analytic at the origin.
• NormedSpace.localBCH_tendsto: the germ tends to zero at the origin.
• NormedSpace.eq_localBCH_of_tendsto_of_map_exp_eq: uniqueness among germs tending to zero with the same exponential image.
• NormedSpace.map_localBCH: continuous ring homomorphisms commute with the local BCH germ.

References

• Lie groups and the Lie algebra correspondence roadmap, Deliverable A, Layer 3, "Baker--Campbell--Hausdorff".

noncomputable def NormedSpace.localBCH (A : Type u_1) [NormedRing A] [NormedAlgebra ℝ A] [hA : CompleteSpace A] : (nhds (0, 0)).Germ A

The germ at (0, 0) represented by the local logarithm fun p ↦ logOneAdd ℝ A (exp p.1 * exp p.2 - 1) of exp p.1 * exp p.2.

Equations

• NormedSpace.localBCH A = ↑fun (p : A × A) => NormedSpace.logOneAdd ℝ A (NormedSpace.exp p.1 * NormedSpace.exp p.2 - 1)

theorem NormedSpace.localBCH_def (A : Type u_1) [NormedRing A] [NormedAlgebra ℝ A] [CompleteSpace A] : localBCH A = ↑fun (p : A × A) => logOneAdd ℝ A (exp p.1 * exp p.2 - 1)

localBCH is the germ of fun p ↦ logOneAdd ℝ A (exp p.1 * exp p.2 - 1).

@[simp]

theorem NormedSpace.localBCH_value (A : Type u_1) [NormedRing A] [NormedAlgebra ℝ A] [CompleteSpace A] : (localBCH A).value = 0

The local Baker--Campbell--Hausdorff germ takes the value zero at the origin.

@[simp]

theorem NormedSpace.localBCH_sliceLeft (A : Type u_1) [NormedRing A] [NormedAlgebra ℝ A] [CompleteSpace A] : (localBCH A).sliceLeft = ↑fun (x : A) => x

Restricting the local Baker--Campbell--Hausdorff germ to the first coordinate axis gives the identity germ.

@[simp]

theorem NormedSpace.localBCH_sliceRight (A : Type u_1) [NormedRing A] [NormedAlgebra ℝ A] [CompleteSpace A] : (localBCH A).sliceRight = ↑fun (y : A) => y

Restricting the local Baker--Campbell--Hausdorff germ to the second coordinate axis gives the identity germ.

@[simp]

theorem NormedSpace.localBCH_map_exp (A : Type u_1) [NormedRing A] [NormedAlgebra ℝ A] [CompleteSpace A] : Filter.Germ.map exp (localBCH A) = ↑fun (p : A × A) => exp p.1 * exp p.2

Applying exponential to the local Baker--Campbell--Hausdorff germ gives the germ of the product of the two exponentials.

theorem NormedSpace.analyticAt_localBCH_representative (A : Type u_1) [NormedRing A] [NormedAlgebra ℝ A] [CompleteSpace A] : AnalyticAt ℝ (fun (p : A × A) => logOneAdd ℝ A (exp p.1 * exp p.2 - 1)) (0, 0)

The representative defining localBCH is analytic at the origin.

theorem NormedSpace.localBCH_tendsto (A : Type u_1) [NormedRing A] [NormedAlgebra ℝ A] [CompleteSpace A] : (localBCH A).Tendsto (nhds 0)

The local Baker--Campbell--Hausdorff germ tends to zero at the origin.

theorem NormedSpace.eq_localBCH_of_tendsto_of_map_exp_eq (A : Type u_1) [NormedRing A] [NormedAlgebra ℝ A] [CompleteSpace A] (f : (nhds (0, 0)).Germ A) (hf : f.Tendsto (nhds 0)) (hmap : Filter.Germ.map exp f = Filter.Germ.map exp (localBCH A)) : f = localBCH A

A germ tending to zero with the same exponential image as localBCH equals localBCH.

@[simp]

theorem NormedSpace.map_localBCH (A : Type u_1) [NormedRing A] [NormedAlgebra ℝ A] [CompleteSpace A] {B : Type u_2} [NormedRing B] [NormedAlgebra ℝ B] [CompleteSpace B] {F : Type u_3} [FunLike F A B] [RingHomClass F A B] (f : F) (hf : Continuous ⇑f) : Filter.Germ.map (⇑f) (localBCH A) = (localBCH B).compTendsto (Prod.map ⇑f ⇑f) ⋯

Continuous ring homomorphisms commute with the local Baker--Campbell--Hausdorff germ.