Convergence of the logarithm series in a Banach algebra

Mathlib defines the logarithm NormedSpace.log x = ∑ n ≥ 1, (-1)^(n+1) / n • (x - 1)^n as the sum of NormedSpace.logSeries at x - 1. This file establishes the convergence and analyticity of NormedSpace.logSeries and NormedSpace.log: in a Banach algebra over a characteristic-zero normed field, the radius of convergence of NormedSpace.logSeries is at least one, so NormedSpace.log is analytic at one. It supplies the local logarithm needed to define the Baker–Campbell–Hausdorff map near the origin.

Main results

• NormedSpace.logSeries_apply: the homogeneous terms of NormedSpace.logSeries.
• NormedSpace.logSeries_partialSum_three: its third partial sum, u - 2⁻¹ • u ^ 2.
• NormedSpace.one_le_logSeries_radius: the radius of convergence is at least one.
• NormedSpace.log_hasFPowerSeriesOnBall: the series represents NormedSpace.log on the unit ball about one.
• NormedSpace.isBigO_log_one_add_sub_quadratic: log (1 + u) - (u - 2⁻¹ • u ^ 2) is O(‖u‖ ^ 3) at the origin.

@[simp]

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

The homogeneous terms of logSeries.

@[simp]

theorem NormedSpace.logSeries_partialSum_three (𝕂 : Type u_1) (A : Type u_2) [Field 𝕂] [Ring A] [Algebra 𝕂 A] [TopologicalSpace A] [IsTopologicalRing A] (u : A) : (logSeries 𝕂 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.

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

The radius of logSeries is at least one.

theorem NormedSpace.logSeries_summable_of_norm_lt_one (𝕂 : 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 series for log (1 + u) is summable in the open unit ball.

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

logSeries represents log throughout the open unit ball about one.

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

log is analytic at one.

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

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