The logarithm of one added to an element of a Banach algebra

This file packages the power series log (1 + u) = ∑ n ≥ 1, (-1)^(n+1) / n • u^n in a Banach algebra over a characteristic-zero normed field. Its radius of convergence is at least one, so it supplies the local logarithm needed to define the Baker–Campbell–Hausdorff map near the origin.

Main definitions and results

• NormedSpace.logOneAddSeries: the formal multilinear series for log (1 + u).
• NormedSpace.logOneAddSeries_apply: its homogeneous terms.
• NormedSpace.logOneAddSeries_partialSum_three: its third partial sum, u - 2⁻¹ • u ^ 2.
• NormedSpace.logOneAdd: its sum.
• NormedSpace.logOneAdd_eq_tsum: the defining series equation.
• NormedSpace.one_le_logOneAddSeries_radius: the radius of convergence is at least one.
• NormedSpace.hasFPowerSeriesOnBall_logOneAdd: the series represents logOneAdd on the unit ball.
• NormedSpace.isBigO_logOneAdd_sub_quadratic: logOneAdd u - (u - 2⁻¹ • u ^ 2) is O(‖u‖ ^ 3) at the origin.

def NormedSpace.logOneAddSeries (𝕂 : Type u_1) (A : Type u_2) [Field 𝕂] [Ring A] [Algebra 𝕂 A] [TopologicalSpace A] [IsTopologicalRing A] [CharZero 𝕂] : FormalMultilinearSeries 𝕂 A A

The formal multilinear series for log (1 + u) in a topological algebra.

Equations

• NormedSpace.logOneAddSeries 𝕂 A = FormalMultilinearSeries.ofScalars A fun (n : ℕ) => (-1) ^ (n + 1) / Nat.castEmbedding n

@[simp]

theorem NormedSpace.logOneAddSeries_apply (𝕂 : Type u_1) (A : Type u_2) [Field 𝕂] [Ring A] [Algebra 𝕂 A] [TopologicalSpace A] [IsTopologicalRing A] [CharZero 𝕂] {n : ℕ} (v : Fin n → A) : (logOneAddSeries 𝕂 A n) v = ((-1) ^ (n + 1) / ↑n) • (List.ofFn v).prod

The homogeneous terms of logOneAddSeries.

@[simp]

theorem NormedSpace.logOneAddSeries_partialSum_three (𝕂 : Type u_1) (A : Type u_2) [Field 𝕂] [Ring A] [Algebra 𝕂 A] [TopologicalSpace A] [IsTopologicalRing A] [CharZero 𝕂] (u : A) : (logOneAddSeries 𝕂 A).partialSum 3 u = u - 2⁻¹ • u ^ 2

The third partial sum of the series for log (1 + u) is the quadratic truncation u - 2⁻¹ • u ^ 2.

noncomputable def NormedSpace.logOneAdd (𝕂 : Type u_1) (A : Type u_2) [Field 𝕂] [Ring A] [Algebra 𝕂 A] [TopologicalSpace A] [IsTopologicalRing A] [CharZero 𝕂] (u : A) : A

The tsum of the power series for log (1 + u).

Equations

• NormedSpace.logOneAdd 𝕂 A u = (NormedSpace.logOneAddSeries 𝕂 A).sum u

theorem NormedSpace.logOneAdd_eq_tsum (𝕂 : Type u_1) (A : Type u_2) [Field 𝕂] [Ring A] [Algebra 𝕂 A] [TopologicalSpace A] [IsTopologicalRing A] [CharZero 𝕂] (u : A) : logOneAdd 𝕂 A u = ∑' (n : ℕ), ((-1) ^ (n + 1) / ↑n) • u ^ n

The defining power-series equation for logOneAdd.

theorem NormedSpace.one_le_logOneAddSeries_radius (𝕂 : Type u_1) (A : Type u_2) [NontriviallyNormedField 𝕂] [NormedRing A] [NormedAlgebra 𝕂 A] [CharZero 𝕂] [ContinuousSMul ℚ≥0 𝕂] : 1 ≤ (logOneAddSeries 𝕂 A).radius

The radius of logOneAddSeries is at least one.

theorem NormedSpace.summable_logOneAdd (𝕂 : Type u_1) (A : Type u_2) [NontriviallyNormedField 𝕂] [NormedRing A] [NormedAlgebra 𝕂 A] [CharZero 𝕂] [ContinuousSMul ℚ≥0 𝕂] [CompleteSpace A] {u : A} (hu : ‖u‖ < 1) : Summable fun (n : ℕ) => ((-1) ^ (n + 1) / ↑n) • u ^ n

The defining series for logOneAdd is summable in the open unit ball.

theorem NormedSpace.hasFPowerSeriesOnBall_logOneAdd (𝕂 : Type u_1) (A : Type u_2) [NontriviallyNormedField 𝕂] [NormedRing A] [NormedAlgebra 𝕂 A] [CharZero 𝕂] [ContinuousSMul ℚ≥0 𝕂] [CompleteSpace A] : HasFPowerSeriesOnBall (logOneAdd 𝕂 A) (logOneAddSeries 𝕂 A) 0 1

logOneAddSeries represents logOneAdd throughout the open unit ball.

theorem NormedSpace.analyticAt_logOneAdd (𝕂 : Type u_1) (A : Type u_2) [NontriviallyNormedField 𝕂] [NormedRing A] [NormedAlgebra 𝕂 A] [CharZero 𝕂] [ContinuousSMul ℚ≥0 𝕂] [CompleteSpace A] : AnalyticAt 𝕂 (logOneAdd 𝕂 A) 0

logOneAdd is analytic at the origin.

theorem NormedSpace.isBigO_logOneAdd_sub_quadratic (𝕂 : Type u_1) (A : Type u_2) [NontriviallyNormedField 𝕂] [NormedRing A] [NormedAlgebra 𝕂 A] [CharZero 𝕂] [ContinuousSMul ℚ≥0 𝕂] [CompleteSpace A] : (fun (u : A) => logOneAdd 𝕂 A u - (u - 2⁻¹ • u ^ 2)) =O[nhds 0] fun (u : A) => ‖u‖ ^ 3

The quadratic Taylor estimate for the Banach algebra logarithm. The difference logOneAdd u - (u - 2⁻¹ • u ^ 2) is O(‖u‖ ^ 3) as u → 0.

@[simp]

theorem NormedSpace.logOneAdd_zero (𝕂 : Type u_1) (A : Type u_2) [Field 𝕂] [CharZero 𝕂] [Ring A] [Algebra 𝕂 A] [TopologicalSpace A] [IsTopologicalRing A] : logOneAdd 𝕂 A 0 = 0

logOneAdd vanishes at zero.