Naturality of the local logarithm

This file proves that continuous ring homomorphisms commute with NormedSpace.log on the open unit ball about one. It also packages this local identity as an equality of germs at one.

Main results

• NormedSpace.map_logSeries_apply: naturality of each homogeneous term.
• NormedSpace.map_log_of_mem_ball: naturality on the open unit ball about one.
• NormedSpace.eventually_map_log: naturality near one.
• NormedSpace.map_log_germ: naturality as an equality of germs.
• NormedSpace.map_log_germ_continuousMapClass: the simp form of map_log_germ.
• RingEquiv.map_log_of_continuous: a ring isomorphism that is a homeomorphism commutes with log everywhere.

See also

• NormedSpace.map_exp_of_mem_ball in Mathlib's exponential naturality development.

theorem NormedSpace.map_logSeries_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 ((logSeries 𝕂 A n) v) = (logSeries 𝕃 B n) (⇑f ∘ v)

Ring homomorphisms commute with each homogeneous term of logSeries.

theorem NormedSpace.map_log_of_mem_ball {A : Type u_1} {B : Type u_2} [NormedRing A] [NormedAlgebra ℚ A] [CompleteSpace A] [Ring B] [TopologicalSpace B] [IsTopologicalRing B] [T2Space B] {F : Type u_3} [FunLike F A B] [RingHomClass F A B] (f : F) (hf : Continuous ⇑f) {x : A} (hx : x ∈ Metric.ball 1 1) : f (log x) = log (f x)

Continuous ring homomorphisms commute with log on the open unit ball about one.

theorem NormedSpace.eventually_map_log {A : Type u_1} {B : Type u_2} [NormedRing A] [NormedAlgebra ℚ A] [CompleteSpace A] [Ring B] [TopologicalSpace B] [IsTopologicalRing B] [T2Space B] {F : Type u_3} [FunLike F A B] [RingHomClass F A B] (f : F) (hf : Continuous ⇑f) : ∀ᶠ (x : A) in nhds 1, f (log x) = log (f x)

A continuous ring homomorphism commutes with log near one.

theorem NormedSpace.map_log_germ {A : Type u_1} {B : Type u_2} [NormedRing A] [NormedAlgebra ℚ A] [CompleteSpace A] [Ring B] [TopologicalSpace B] [IsTopologicalRing B] [T2Space B] {F : Type u_3} [FunLike F A B] [RingHomClass F A B] (f : F) (hf : Continuous ⇑f) : ↑(⇑f ∘ log) = (↑log).compTendsto ⇑f ⋯

Continuous ring homomorphisms commute with the germ of log at one.

@[simp]

theorem NormedSpace.map_log_germ_continuousMapClass {A : Type u_1} {B : Type u_2} [NormedRing A] [NormedAlgebra ℚ A] [CompleteSpace A] [Ring B] [TopologicalSpace B] [IsTopologicalRing B] [T2Space B] {F : Type u_3} [FunLike F A B] [ContinuousMapClass F A B] [RingHomClass F A B] (f : F) : ↑(⇑f ∘ log) = (↑log).compTendsto ⇑f ⋯

Continuous ring homomorphisms in a ContinuousMapClass commute with the germ of log at one. This is the simp form of map_log_germ, which takes an explicit continuity proof.

theorem RingEquiv.map_log_of_continuous {A : Type u_1} {B : Type u_2} [Ring A] [TopologicalSpace A] [IsTopologicalRing A] [Ring B] [TopologicalSpace B] [IsTopologicalRing B] [T2Space B] (σ : A ≃+* B) (hσ : Continuous ⇑σ) (hσ' : Continuous ⇑σ.symm) (x : A) : σ (NormedSpace.log x) = NormedSpace.log (σ x)

A ring isomorphism that is a homeomorphism commutes with log everywhere. The logarithm series of x is mapped termwise to that of σ x, and σ preserves summability and tsum because it has a continuous inverse. When A has no ℚ-algebra structure, neither has B, and both sides are 0.