logMap_expMap — Mathlib

English

If the norm of expMap x equals 1, then logMap of expMap x equals logMap x, in particular the coordinate-wise log map recovers x.

Русский

Если норма expMap x равна 1, то logMap(expMap x) = logMap x; координатное восстановление x по логарифму выполняется.

LaTeX

$$$\\logMap(\\mathrm{mixedSpaceOfRealSpace}(\\expMap x)) = x$ when a normalization holds$$

Lean4

theorem logMap_expMap {x : realSpace K} (hx : mixedEmbedding.norm (mixedSpaceOfRealSpace (expMap x)) = 1) :
    logMap (mixedSpaceOfRealSpace (expMap x)) = fun w ↦ x w.1 :=
  by
  ext
  rw [logMap, normAtPlace_mixedSpaceOfRealSpace (Real.exp_nonneg _), expMap_apply, Real.log_exp, mul_sub,
    mul_inv_cancel_left₀ mult_coe_ne_zero, hx, Real.log_one, zero_mul, mul_zero, sub_zero]

Похожие утверждения