The Trotter product formula

This file proves a tangent-to-identity power limit for finite-dimensional real Lie groups and applies it to the product of two exponential curves. The resulting Trotter formula supplies the addition-closure input for the subgroup Lie algebra in Deliverable A, Layer 2 of the Lie-groups roadmap.

Main results

• tendsto_pow_div_of_hasDerivAt_mulInvariantLog: a curve whose local logarithm has initial derivative X has rescaled powers converging to exp (t X).
• tendsto_mulInvariantExp_smul_mul_mulInvariantExp_smul_pow: the Trotter product formula in the tangent model.
• tendsto_lieExp_smul_mul_lieExp_smul_pow: the Trotter product formula for left-invariant derivations.
• lieExp_add_of_commute: the exponential of a sum of derivations with commuting one-parameter subgroups is the product of the exponentials.

References

• H. Liu, Notes for Lie Groups & Representations, notes from Andrei Okounkov's Fall 2016 course, Proposition 2.4.3.
• Lie groups and the Lie algebra correspondence roadmap, Deliverable A, Layer 2, "The Lie subalgebra of a subgroup".

theorem tendsto_pow_div_of_hasDerivAt_mulInvariantLog {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {G : Type u_3} [TopologicalSpace G] [ChartedSpace H G] [Group G] [FiniteDimensional ℝ E] [LieGroup I (↑⊤) G] {f : ℝ → G} (X : GroupLieAlgebra I G) (hf0 : f 0 = 1) : have x := ⋯; have x_1 := ⋯; ContinuousAt f 0 → HasDerivAt (fun (s : ℝ) => have this := mulInvariantLog (f s); this) (have this := X; this) 0 → ∀ (t : ℝ), Filter.Tendsto (fun (n : ℕ) => f (t / ↑n) ^ n) Filter.atTop (nhds (mulInvariantExp (t • X)))

A tangent-to-identity curve has the expected exponential power limit. The derivative is stated in local logarithmic coordinates so the result can be reused independently of a chosen manifold expression for the curve.

theorem tendsto_mulInvariantExp_smul_mul_mulInvariantExp_smul_pow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {G : Type u_3} [TopologicalSpace G] [ChartedSpace H G] [Group G] [FiniteDimensional ℝ E] [LieGroup I (↑⊤) G] : have x := ⋯; have x_1 := ⋯; ∀ (X Y : GroupLieAlgebra I G) (t : ℝ), Filter.Tendsto (fun (n : ℕ) => (mulInvariantExp ((t / ↑n) • X) * mulInvariantExp ((t / ↑n) • Y)) ^ n) Filter.atTop (nhds (mulInvariantExp (t • (X + Y))))

The Trotter product formula for the tangent-space exponential.

theorem tendsto_lieExp_smul_mul_lieExp_smul_pow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {G : Type u_3} [TopologicalSpace G] [ChartedSpace H G] [Group G] [FiniteDimensional ℝ E] [LieGroup I (↑⊤) G] : have x := ⋯; have x_1 := ⋯; ∀ (X Y : LeftInvariantDerivation I G) (t : ℝ), Filter.Tendsto (fun (n : ℕ) => (lieExp ((t / ↑n) • X) * lieExp ((t / ↑n) • Y)) ^ n) Filter.atTop (nhds (lieExp (t • (X + Y))))

The Trotter product formula for the exponential of left-invariant derivations.

theorem lieExp_add_of_commute {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {G : Type u_3} [TopologicalSpace G] [ChartedSpace H G] [Group G] [FiniteDimensional ℝ E] [LieGroup I (↑⊤) G] : have x := ⋯; have x_1 := ⋯; ∀ {X Y : LeftInvariantDerivation I G}, (∀ (t : ℝ), Commute (lieExp (t • X)) (lieExp (t • Y))) → lieExp (X + Y) = lieExp X * lieExp Y

The exponential of a sum of derivations with commuting one-parameter subgroups is the product of the exponentials.