expMapBasis_apply'' — Mathlib

English

A refinement of ExpMapBasis_apply'' with simp rules; expMapBasis x equals Real.exp (x w₀) times a product over i ≠ w₀.

Русский

Уточнение через правила упрощения; expMapBasis x равен Real.exp (x w₀) умножить на произведение по i ≠ w₀.

LaTeX

$$$\text{ExpMapBasisApply''}(x):\ \text{ExpMapBasis}(x) = \operatorname{Real}.\exp(x(w_0)) \cdot \prod_{i\neq w_0} w(\text{fundSystem}(K,\text{equivFinRank}.symm(i)))^{x(i)} $$$

Lean4

theorem expMapBasis_apply'' (x : realSpace K) :
    expMapBasis x = Real.exp (x w₀) • expMapBasis (fun i ↦ if i = w₀ then 0 else x i) :=
  by
  rw [expMapBasis_apply', expMapBasis_apply', if_pos rfl, smul_smul, ← Real.exp_add, add_zero]
  conv_rhs =>
    enter [2, w, 2, i]
    rw [if_neg i.prop]

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