English
Coefficients of the smul of two summable families are given by a bilinear sum over the cross-diagonal.
Русский
Коэффициенты произведения-smul двух суммируемых семейств задаются билинейной суммой по перекрестной диагонали.
LaTeX
$$$ (smul\ s\ t).hsum.coeff g = \sum_{gh \in VAddAntidiagonal s.isPWO_iUnion_support t.isPWO_iUnion_support g} (s.hsum.coeff gh.1) \cdot (t.hsum.coeff gh.2) $$$
Lean4
theorem sum_vAddAntidiagonal_eq (s : SummableFamily Γ R α) (t : SummableFamily Γ' V β) (g : Γ') (a : α × β) :
∑ x ∈ VAddAntidiagonal (s a.1).isPWO_support' (t a.2).isPWO_support' g, (s a.1).coeff x.1 • (t a.2).coeff x.2 =
∑ x ∈ VAddAntidiagonal s.isPWO_iUnion_support' t.isPWO_iUnion_support' g, (s a.1).coeff x.1 • (t a.2).coeff x.2 :=
by
refine sum_subset (fun gh hgh => ?_) fun gh hgh h => ?_
· simp_all only [mem_vaddAntidiagonal, Function.mem_support, Set.mem_iUnion, mem_support]
exact ⟨Exists.intro a.1 hgh.1, Exists.intro a.2 hgh.2.1, trivial⟩
· by_cases hs : (s a.1).coeff gh.1 = 0
· exact smul_eq_zero_of_left hs ((t a.2).coeff gh.2)
· simp_all
