linearCombination_dualBasis — Mathlib

English

For any finite index set, the sum over i of f(b_i) · b.coord i equals f, i.e., the dual evaluation recovers f from its coordinates.

Русский

Для конечного множества индексов сумма по i от f(b_i) · b.coord i равна f; дуальная аппроксимация восстанавливает f по координатам.

LaTeX

$$$ \sum_{x} f(b_x) \cdot b.coord x = f. $$$

Lean4

theorem linearCombination_dualBasis (f : ι →₀ R) (i : ι) : Finsupp.linearCombination R b.dualBasis f (b i) = f i :=
  by
  cases nonempty_fintype ι
  rw [Finsupp.linearCombination_apply, Finsupp.sum_fintype, LinearMap.sum_apply]
  ·
    simp_rw [LinearMap.smul_apply, smul_eq_mul, dualBasis_apply_self, mul_boole, Finset.sum_ite_eq,
      if_pos (Finset.mem_univ i)]
  · intro
    rw [zero_smul]

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