coeff_hsum_mul — Mathlib

English

The coefficient of the hsum of a product is given by a convolution over the addAntidiagonal.

Русский

Коэффициент суммы произведения задаётся свёрткой по addAntidiagonal.

LaTeX

$$$ (coeff\_hsum\_mul) (s,t,g) = \sum_{gh \in addAntidiagonal s.isPWO_iUnion_support t.isPWO_iUnion_support g} (s.hsum.coeff gh.fst) * (t.hsum.coeff gh.snd) $$$

Lean4

theorem coeff_hsum_mul (s : SummableFamily Γ R α) (t : SummableFamily Γ R β) (g : Γ) :
    (mul s t).hsum.coeff g =
      ∑ gh ∈ addAntidiagonal s.isPWO_iUnion_support t.isPWO_iUnion_support g,
        (s.hsum.coeff gh.1) * (t.hsum.coeff gh.2) :=
  by
  simp_rw [← smul_eq_mul, mul_eq_smul]
  exact coeff_smul s t g

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