expMapBasis — Mathlib

English

The map expMapBasis is equal to expMap composed with the inverse of the equiv Fun basis, i.e., expMapBasis(x) = expMap((completeBasis(K).equivFun.symm) x).

Русский

Отображение expMapBasis равно композиции expMap с обратным отображением базиса equivFun: expMapBasis(x) = expMap((completeBasis(K).equivFun.symm) x).

LaTeX

$$$\expMapBasis(x) = \exp\big( (\text{completeBasis}(K).\text{equivFun}).\text{symm}(x) \big)$$$

Lean4

/-- The map that sends `x : realSpace K` to
`Real.exp (x w₀) * ∏_{i ≠ w₀} |ηᵢ| ^ x i` where `|ηᵢ|` denote the vector of `realSpace K` given
by `w (ηᵢ)` and `ηᵢ` denote the units in `fundSystem K`, see `expMapBasis_apply'`.
-/
def expMapBasis : OpenPartialHomeomorph (realSpace K) (realSpace K) :=
  (completeBasis K).equivFunL.symm.toHomeomorph.transOpenPartialHomeomorph expMap

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