English
An a priori infinite sum expression for the convolution term: term (f ⍟ g) s n = ∑' b : (ℕ×ℕ → ℕ)⁻¹{n}, term f s b.1 · term g s b.2.
Русский
Неопределённая бесконечная сумма: term(f ⍟ g) s n = ∑' b, term f s b1 · term g s b2, где b описывает пары, чьё произведение равно n.
LaTeX
$$$\\operatorname{term}(f \\star g)\\, s\\, n = \\sum'\\,b\\, \\operatorname{term} f\\, s\\, b.1 \\cdot \\operatorname{term} g\\, s\\, b.2.$$$
Lean4
/-- We give an expression of the `LSeries.term` of the convolution of two functions
in terms of an a priori infinite sum over all pairs `(k, m)` with `k * m = n`
(the set we sum over is infinite when `n = 0`). This is the version needed for the
proof that `L (f ⍟ g) = L f * L g`. -/
theorem term_convolution' (f g : ℕ → ℂ) (s : ℂ) :
term (f ⍟ g) s = fun n ↦ ∑' (b : (fun p : ℕ × ℕ ↦ p.1 * p.2) ⁻¹' { n }), term f s b.val.1 * term g s b.val.2 :=
by
ext n
rcases eq_or_ne n 0 with rfl | hn
· -- show that both sides vanish when `n = 0`; this is the hardest part of the proof!
refine
(term_zero ..).trans
?_
-- the right-hand sum is over the union below, but in each term, one factor is always zero
have hS : (fun p ↦ p.1 * p.2) ⁻¹' {0} = {0} ×ˢ univ ∪ univ ×ˢ {0} :=
by
ext
simp
have : ∀ p : (fun p : ℕ × ℕ ↦ p.1 * p.2) ⁻¹' {0}, term f s p.val.1 * term g s p.val.2 = 0 :=
by
rintro ⟨⟨_, _⟩, hp⟩
rcases hS ▸ hp with ⟨rfl, -⟩ | ⟨-, rfl⟩ <;> simp
simp [this]
-- now `n ≠ 0`
rw [show (fun p : ℕ × ℕ ↦ p.1 * p.2) ⁻¹' { n } = n.divisorsAntidiagonal by ext; simp [hn],
Finset.tsum_subtype' n.divisorsAntidiagonal fun p ↦ term f s p.1 * term g s p.2, term_convolution f g s n]
