The first-order term of the local Baker--Campbell--Hausdorff germ

The local Baker--Campbell--Hausdorff germ of TauCeti/Analysis/Normed/Algebra/BCH/Local.lean is represented by fun p ↦ logOneAdd (exp p.1 * exp p.2 - 1). This file proves the law that fixes its expansion at the origin:

logOneAdd (exp x * exp y - 1) = x + y + 2⁻¹ • (x * y - y * x) + O(‖(x, y)‖ ^ 3).

The second-order term x * y - y * x is the commutator ⁅x, y⁆ of the Lie ring underlying the associative ring, so this is the familiar x + y + ½⁅x, y⁆ of the Baker--Campbell--Hausdorff series. It is written as a difference of products rather than as a bracket because LieRing.ofAssociativeRing is not an instance.

The proof is the classical formal computation, carried out with the two quadratic Taylor estimates that the ingredients satisfy, NormedSpace.isBigO_exp_sub_quadratic and NormedSpace.isBigO_logOneAdd_sub_quadratic. Writing u = exp x * exp y - 1 and q = x + y:

• multiplying the two quadratic truncations gives u = q + 2⁻¹ • q ^ 2 + 2⁻¹ • (x * y - y * x) to third order, the three leftover monomials x * y ^ 2, x ^ 2 * y and x ^ 2 * y ^ 2 being of order at least three;
• hence u - q is of order two, so u ^ 2 and q ^ 2 agree to third order;
• and logOneAdd u = u - 2⁻¹ • u ^ 2 to third order, with ‖u‖ of order one, so the two quadratic terms cancel and only q + 2⁻¹ • (x * y - y * x) survives.

Only the germ at the origin is involved, so the statement transfers to any representative of NormedSpace.localBCH.

Main results

• NormedSpace.isBigO_exp_mul_exp_sub_one_sub_quadratic: the quadratic Taylor estimate for exp x * exp y - 1.
• NormedSpace.isBigO_logOneAdd_exp_mul_exp_sub_one_sub_firstOrder: the first-order law, that the representative of the local Baker--Campbell--Hausdorff germ is x + y + 2⁻¹ • (x * y - y * x) up to O(‖(x, y)‖ ^ 3).
• NormedSpace.isBigO_sub_firstOrder_of_coe_eq_localBCH: the same for an arbitrary representative of NormedSpace.localBCH.

The quadratic Taylor estimate for a product of two exponentials

theorem NormedSpace.isBigO_exp_mul_exp_sub_one_sub_quadratic (A : Type u_1) [NormedRing A] [NormedAlgebra ℝ A] [CompleteSpace A] : (fun (p : A × A) => exp p.1 * exp p.2 - 1 - (p.1 + p.2) - (2⁻¹ • p.1 ^ 2 + p.1 * p.2 + 2⁻¹ • p.2 ^ 2)) =O[nhds (0, 0)] fun (p : A × A) => ‖p‖ ^ 3

The quadratic Taylor estimate for exp x * exp y - 1. Multiplying the two quadratic truncations of the exponential leaves monomials of degree at least three.

The first-order law

theorem NormedSpace.isBigO_logOneAdd_exp_mul_exp_sub_one_sub_firstOrder (A : Type u_1) [NormedRing A] [NormedAlgebra ℝ A] [CompleteSpace A] : (fun (p : A × A) => logOneAdd ℝ A (exp p.1 * exp p.2 - 1) - (p.1 + p.2 + 2⁻¹ • (p.1 * p.2 - p.2 * p.1))) =O[nhds (0, 0)] fun (p : A × A) => ‖p‖ ^ 3

The first-order law of the local Baker--Campbell--Hausdorff germ. Its defining representative is x + y + 2⁻¹ • (x * y - y * x) up to third order at the origin; the second-order term is half the commutator.

theorem NormedSpace.isBigO_sub_firstOrder_of_coe_eq_localBCH (A : Type u_1) [NormedRing A] [NormedAlgebra ℝ A] [CompleteSpace A] (f : A × A → A) (hf : ↑f = localBCH A) : (fun (p : A × A) => f p - (p.1 + p.2 + 2⁻¹ • (p.1 * p.2 - p.2 * p.1))) =O[nhds (0, 0)] fun (p : A × A) => ‖p‖ ^ 3

The first-order law holds for every representative of the local Baker--Campbell--Hausdorff germ, the estimate at the origin depending only on the germ.