Naturality of the local logarithm

This file proves that continuous ring homomorphisms commute with the power series for log (1 + u) on the open unit ball. It also packages this local identity as an equality of germs at the origin.

Main results

• NormedSpace.map_logOneAddSeries_apply: naturality of each homogeneous term.
• NormedSpace.map_logOneAdd_of_norm_lt_one: naturality on the open unit ball.
• NormedSpace.eventually_map_logOneAdd: naturality near the origin.
• NormedSpace.map_logOneAdd_germ: naturality as an equality of germs.

References

• Lie groups and the Lie algebra correspondence roadmap, Deliverable A, Layer 3, "Baker--Campbell--Hausdorff".
• NormedSpace.map_exp_of_mem_ball in Mathlib's exponential naturality development.

theorem NormedSpace.map_logOneAddSeries_apply {𝕂 : Type u_1} {𝕃 : Type u_2} {A : Type u_3} {B : Type u_4} [Field 𝕂] [CharZero 𝕂] [Field 𝕃] [CharZero 𝕃] [Ring A] [Algebra 𝕂 A] [TopologicalSpace A] [IsTopologicalRing A] [Ring B] [Algebra 𝕃 B] [TopologicalSpace B] [IsTopologicalRing B] {F : Type u_5} [FunLike F A B] [RingHomClass F A B] (f : F) {n : ℕ} (v : Fin n → A) : f ((logOneAddSeries 𝕂 A n) v) = (logOneAddSeries 𝕃 B n) (⇑f ∘ v)

Ring homomorphisms commute with each homogeneous term of logOneAddSeries.

theorem NormedSpace.map_logOneAdd_of_norm_lt_one {𝕂 : Type u_1} {𝕃 : Type u_2} {A : Type u_3} {B : Type u_4} [NontriviallyNormedField 𝕂] [CharZero 𝕂] [Field 𝕃] [CharZero 𝕃] [ContinuousSMul ℚ≥0 𝕂] [NormedRing A] [NormedAlgebra 𝕂 A] [Ring B] [Algebra 𝕃 B] [TopologicalSpace B] [IsTopologicalRing B] [CompleteSpace A] {F : Type u_5} [FunLike F A B] [RingHomClass F A B] [T2Space B] (f : F) (hf : Continuous ⇑f) {u : A} (hu : ‖u‖ < 1) : f (logOneAdd 𝕂 A u) = logOneAdd 𝕃 B (f u)

Continuous ring homomorphisms commute with logOneAdd on the open unit ball.

theorem NormedSpace.eventually_map_logOneAdd {𝕂 : Type u_1} {𝕃 : Type u_2} {A : Type u_3} {B : Type u_4} [NontriviallyNormedField 𝕂] [CharZero 𝕂] [Field 𝕃] [CharZero 𝕃] [ContinuousSMul ℚ≥0 𝕂] [NormedRing A] [NormedAlgebra 𝕂 A] [Ring B] [Algebra 𝕃 B] [TopologicalSpace B] [IsTopologicalRing B] [CompleteSpace A] {F : Type u_5} [FunLike F A B] [RingHomClass F A B] [T2Space B] (f : F) (hf : Continuous ⇑f) : ∀ᶠ (u : A) in nhds 0, f (logOneAdd 𝕂 A u) = logOneAdd 𝕃 B (f u)

A continuous ring homomorphism commutes with logOneAdd near the origin.

theorem NormedSpace.map_logOneAdd_germ {𝕂 : Type u_1} {𝕃 : Type u_2} {A : Type u_3} {B : Type u_4} [NontriviallyNormedField 𝕂] [CharZero 𝕂] [Field 𝕃] [CharZero 𝕃] [ContinuousSMul ℚ≥0 𝕂] [NormedRing A] [NormedAlgebra 𝕂 A] [Ring B] [Algebra 𝕃 B] [TopologicalSpace B] [IsTopologicalRing B] [CompleteSpace A] {F : Type u_5} [FunLike F A B] [RingHomClass F A B] [T2Space B] (f : F) (hf : Continuous ⇑f) : ↑(⇑f ∘ logOneAdd 𝕂 A) = (↑(logOneAdd 𝕃 B)).compTendsto ⇑f ⋯

Continuous ring homomorphisms commute with the germ of logOneAdd at the origin.