English
If s is a finite set of pairs p = (p1,p2) with the products p1·p2 = m, then (x*y)(m) = sum_{p∈s} x(p1) y(p2). This is a refinement of the convolution along an antidiagonal in M × M.
Русский
Если s — конечное множество пар p = (p1,p2) с p1·p2 = m, то (x*y)(m) = сумма по p∈s от x(p1) y(p2). Это уточнение свёртки вдоль антиподиагонали в M × M.
LaTeX
$$$ (x*y)(m) = \sum_{p\in s} x(p_1) \cdot y(p_2) \quad \text{при } p_1 p_2 = m $$$
Lean4
@[to_additive (dont_translate := R) mul_apply_antidiagonal]
theorem mul_apply_antidiagonal (x y : MonoidAlgebra R M) (m : M) (s : Finset (M × M))
(hs : ∀ {p}, p ∈ s ↔ p.1 * p.2 = m) : (x * y) m = ∑ p ∈ s, x p.1 * y p.2 := by
classical
let F (p : M × M) : R := if p.1 * p.2 = m then x p.1 * y p.2 else 0
calc
(x * y) m = ∑ m₁ ∈ x.support, ∑ m₂ ∈ y.support, F (m₁, m₂) := mul_apply ..
_ = ∑ p ∈ x.support ×ˢ y.support with p.1 * p.2 = m, x p.1 * y p.2 := by rw [Finset.sum_filter, Finset.sum_product]
_ = ∑ p ∈ s with p.1 ∈ x.support ∧ p.2 ∈ y.support, x p.1 * y p.2 := by congr! 1; ext;
simp only [mem_filter, mem_product, hs, and_comm]
_ = ∑ p ∈ s, x p.1 * y p.2 :=
sum_subset (filter_subset _ _) fun p hps hp =>
by
simp only [mem_filter, mem_support_iff, not_and, Classical.not_not] at hp ⊢
by_cases h1 : x p.1 = 0
· rw [h1, zero_mul]
· rw [hp hps h1, mul_zero]
