Local inverse equations for the Banach algebra logarithm

This file proves that NormedSpace.logOneAdd and the exponential are inverse near the origin, in a complete normed algebra over a characteristic-zero nontrivially normed field on which ℚ acts continuously (the setting of NormedSpace.exp_hasFPowerSeriesAt_zero).

Main results

• NormedSpace.eventually_logOneAdd_exp_sub_one: near zero, logOneAdd (exp x - 1) = x.
• NormedSpace.eventually_exp_logOneAdd: near zero, exp (logOneAdd x) = 1 + x.

Implementation notes

The power series of logOneAdd and of the exponential have rational coefficients, and so do their formal compositions. These rational coefficients are identified over ℝ, where Real.log and Real.exp are inverse, and the identities then hold over every characteristic-zero field and in every algebra over it.

theorem NormedSpace.eventually_logOneAdd_exp_sub_one (𝕂 : Type u_1) (A : Type u_2) [NontriviallyNormedField 𝕂] [CharZero 𝕂] [ContinuousSMul ℚ 𝕂] [NormedRing A] [NormedAlgebra 𝕂 A] [CompleteSpace A] : ∀ᶠ (x : A) in nhds 0, logOneAdd 𝕂 A (exp x - 1) = x

Near zero, taking logOneAdd after subtracting one from the exponential is the identity.

theorem NormedSpace.eventually_exp_logOneAdd (𝕂 : Type u_1) (A : Type u_2) [NontriviallyNormedField 𝕂] [CharZero 𝕂] [ContinuousSMul ℚ 𝕂] [NormedRing A] [NormedAlgebra 𝕂 A] [CompleteSpace A] : ∀ᶠ (x : A) in nhds 0, exp (logOneAdd 𝕂 A x) = 1 + x

Near zero, exponentiating logOneAdd recovers one plus the argument.