ExponentialLocalSeparation.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Separation of arbitrary exponential preimages near a regular logarithm

If the exponential has trivial kernel, a local injectivity neighborhood cannot have an additional logarithm outside that neighborhood. Conjugating the small logarithm by the one-parameter subgroup of the other logarithm first forces the two logarithms to commute.

theorem OAI.PolycyclicRecognition.exp_eq_of_local_injectivity line 24

theorem OAI.PolycyclicRecognition.exists_unique_local_logarithm line 77

Source documentation

Near the identity the inverse-function logarithm is the only logarithm, even among points outside its initial domain.

theorem exists_unique_local_logarithm
    (hker : ∀ a : A, NormedSpace.exp a = 1 → a = 0) :
    ∃ log : A → A, ContinuousAt log 1 ∧ log 1 = 0 ∧
      ∀ᶠ z in 𝓝 (1 : A), NormedSpace.exp (log z) = z ∧
        ∀ a, NormedSpace.exp a = z → a = log z := by
…