coe_mul_of_apply — Mathlib

English

An auxiliary coefficient formula expressing the convolution in terms of inner sums over a chosen index pair.

Русский

Вспомогательная формула коэффициентов, выражающая свёртку через вложенные суммы по выбранной паре индексов.

LaTeX

$$$$ (r * r')_n = \sum_i \sum_j r_i r'_j \mathbf{1}_{\{i+j=n\}}.$$$$

Lean4

theorem coe_mul_of_apply (r : ⨁ i, A i) {i : ι} (r' : A i) (n : ι) [Decidable (i ≤ n)] :
    ((r * of (fun i => A i) i r') n : R) = if i ≤ n then (r (n - i) : R) * r' else 0 :=
  by
  split_ifs with h
  exacts [coe_mul_of_apply_of_le _ _ _ n h, coe_mul_of_apply_of_not_le _ _ _ n h]

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