realSpaceToLogSpace_expMap_symm — Mathlib

English

realSpaceToLogSpace_expMap_symm expresses a relation between log-space images and norms across all places via the exp/log maps.

Русский

Соотношение между изображениями в лог-пространстве и нормами по всем местам выражается через экспонтент и лог-анализ.

LaTeX

$$$\text{realSpaceToLogSpace}(\expMap^{-1}(\|\cdot\|_{\text{All}})) = \logMap(\text{mixedEmbedding}).$$$

Lean4

theorem realSpaceToLogSpace_expMap_symm {x : K} (hx : x ≠ 0) :
    realSpaceToLogSpace (expMap.symm (normAtAllPlaces (mixedEmbedding K x))) = logMap (mixedEmbedding K x) :=
  by
  ext w
  simp_rw [realSpaceToLogSpace_apply, sum_expMap_symm_apply hx, expMap_symm_apply, logMap, normAtPlace_apply, mul_sub,
    mul_assoc, norm_eq_norm]

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