The quotient (1 - exp (-a)) / a

This basic file packages the power series representing (1 - exp (-a)) / a without requiring a to be invertible. In a complete normed algebra over a normed characteristic-zero field the series is summable at every point. It is the analytic factor in the differential of a Lie-group exponential map.

Main results

• oneSubExpNegDivSelf: the series ∑ n, (n + 1)!⁻¹ • (-a)ⁿ.
• summable_oneSubExpNegDivSelf: the series is summable in a complete normed algebra.
• commute_oneSubExpNegDivSelf: the series commutes with its argument.
• mul_oneSubExpNegDivSelf: multiplying the series by a gives 1 - exp (-a).
• oneSubExpNegDivSelf_mul: the corresponding right-multiplication identity.
• map_oneSubExpNegDivSelf: continuous ring homomorphisms preserve the series.

References

• Lie groups and the Lie algebra correspondence roadmap, Deliverable A, Layer 1, "The conjugation formulas".
• Mathlib's spectrum.exp_mem_exp, whose proof supplies the shifted-exponential series argument adapted here.

noncomputable def oneSubExpNegDivSelf (𝕂 : Type u_3) [Field 𝕂] {A : Type u_4} [Ring A] [Algebra 𝕂 A] [TopologicalSpace A] [IsTopologicalRing A] (a : A) : A

The value of (1 - exp (-a)) / a with its removable singularity filled in, defined by a power series. The series is summable everywhere in the complete normed-algebra setting below.

Equations

• oneSubExpNegDivSelf 𝕂 a = FormalMultilinearSeries.ofScalarsSum (fun (n : ℕ) => (↑(n + 1).factorial)⁻¹) (-a)

theorem oneSubExpNegDivSelf_eq_tsum {𝕂 : Type u_1} {A : Type u_2} [Field 𝕂] [Ring A] [Algebra 𝕂 A] [TopologicalSpace A] [IsTopologicalRing A] (a : A) : oneSubExpNegDivSelf 𝕂 a = ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (-a) ^ n

The defining series for oneSubExpNegDivSelf.

@[simp]

theorem oneSubExpNegDivSelf_zero {𝕂 : Type u_1} {A : Type u_2} [Field 𝕂] [Ring A] [Algebra 𝕂 A] [TopologicalSpace A] [IsTopologicalRing A] : oneSubExpNegDivSelf 𝕂 0 = 1

The quotient with its removable singularity filled in takes the value 1 at zero.

theorem commute_oneSubExpNegDivSelf {𝕂 : Type u_1} {A : Type u_2} [Field 𝕂] [Ring A] [Algebra 𝕂 A] [TopologicalSpace A] [IsTopologicalRing A] [T2Space A] (a : A) : Commute a (oneSubExpNegDivSelf 𝕂 a)

The filled-in quotient commutes with its argument.

theorem summable_oneSubExpNegDivSelf {𝕂 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕂] [CharZero 𝕂] [ContinuousSMul ℚ 𝕂] [NormedRing A] [NormedAlgebra 𝕂 A] [CompleteSpace A] (a : A) : Summable fun (n : ℕ) => (↑(n + 1).factorial)⁻¹ • (-a) ^ n

The series defining oneSubExpNegDivSelf is summable in a complete normed algebra.

@[simp]

theorem mul_oneSubExpNegDivSelf {𝕂 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕂] [CharZero 𝕂] [ContinuousSMul ℚ 𝕂] [NormedRing A] [NormedAlgebra 𝕂 A] [CompleteSpace A] (a : A) : a * oneSubExpNegDivSelf 𝕂 a = 1 - NormedSpace.exp (-a)

Multiplying the filled-in quotient on the left by its argument recovers its numerator.

@[simp]

theorem oneSubExpNegDivSelf_mul {𝕂 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕂] [CharZero 𝕂] [ContinuousSMul ℚ 𝕂] [NormedRing A] [NormedAlgebra 𝕂 A] [CompleteSpace A] (a : A) : oneSubExpNegDivSelf 𝕂 a * a = 1 - NormedSpace.exp (-a)

Multiplying the filled-in quotient on the right by its argument recovers its numerator.

theorem oneSubExpNegDivSelf_eq_invOf_mul {𝕂 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕂] [CharZero 𝕂] [ContinuousSMul ℚ 𝕂] [NormedRing A] [NormedAlgebra 𝕂 A] [CompleteSpace A] (a : A) [Invertible a] : oneSubExpNegDivSelf 𝕂 a = ⅟a * (1 - NormedSpace.exp (-a))

At an invertible argument, the filled-in quotient is left division by that argument.

theorem oneSubExpNegDivSelf_eq_mul_invOf {𝕂 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕂] [CharZero 𝕂] [ContinuousSMul ℚ 𝕂] [NormedRing A] [NormedAlgebra 𝕂 A] [CompleteSpace A] (a : A) [Invertible a] : oneSubExpNegDivSelf 𝕂 a = (1 - NormedSpace.exp (-a)) * ⅟a

At an invertible argument, the filled-in quotient is right division by that argument.

theorem map_oneSubExpNegDivSelf {𝕂 : Type u_1} {A : Type u_2} {B : Type u_3} [NontriviallyNormedField 𝕂] [CharZero 𝕂] [ContinuousSMul ℚ 𝕂] [NormedRing A] [NormedAlgebra 𝕂 A] [CompleteSpace A] [Ring B] [Algebra 𝕂 B] [TopologicalSpace B] [IsTopologicalRing B] [T2Space B] {F : Type u_4} [FunLike F A B] [RingHomClass F A B] (f : F) (hf : Continuous ⇑f) (a : A) : f (oneSubExpNegDivSelf 𝕂 a) = oneSubExpNegDivSelf 𝕂 (f a)

Any continuous ring homomorphism commutes with oneSubExpNegDivSelf.