expMapBasis_apply' — Mathlib

English

expMapBasis x = Real.exp (x w₀) • expMapBasis (fun i ↦ if i = w₀ then 0 else x i).

Русский

expMapBasis x = exp( x(w₀) ) · expMapBasis( функции i→ если i = w₀ тогда 0, иначе x i ).

LaTeX

$$$\text{expMapBasis}(x) = \operatorname{Real}.\exp(x(w_0)) \cdot \text{expMapBasis}\bigl(\lambda i, \text{if } i=w_0 \text{ then }0\text{ else } x(i)\bigr)$$$

Lean4

theorem expMapBasis_apply' (x : realSpace K) :
    expMapBasis x =
      Real.exp (x w₀) • fun w : InfinitePlace K ↦ ∏ i : { w // w ≠ w₀ }, w (fundSystem K (equivFinRank.symm i)) ^ x i :=
  by
  simp_rw [expMapBasis_apply, Basis.equivFun_symm_apply, Fintype.sum_eq_add_sum_subtype_ne _ w₀, expMap_add,
    expMap_smul, expMap_basis_of_eq, Pi.pow_def, Real.exp_one_rpow, Pi.mul_def, expMap_sum, expMap_smul,
    expMap_basis_of_ne, Pi.smul_def, smul_eq_mul, prod_apply, Pi.pow_apply, normAtAllPlaces_mixedEmbedding]

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