English
The s-term of the convolution equals a sum over divisors: term (f ⍟ g) s n = ∑_{p ∈ n.divisorsAntidiagonal} term f s p1 · term g s p2.
Русский
Значение члена конволюции равно сумме по делителям: term(f ⍟ g) s n = ∑_{p ∈ n.divisorsAntidiagonal} term f s p1 · term g s p2.
LaTeX
$$$\\operatorname{term}(f \\star g)\\, s\\, n = \\sum_{p \\in n.divisorsAntidiagonal} \\operatorname{term} f\\, s\\, p.1 \\cdot \\operatorname{term} g\\, s\\, p.2.$$$
Lean4
/-- We give an expression of the `LSeries.term` of the convolution of two functions
in terms of a sum over `Nat.divisorsAntidiagonal`. -/
theorem term_convolution (f g : ℕ → ℂ) (s : ℂ) (n : ℕ) :
term (f ⍟ g) s n = ∑ p ∈ n.divisorsAntidiagonal, term f s p.1 * term g s p.2 :=
by
rcases eq_or_ne n 0 with rfl | hn
·
simp
-- now `n ≠ 0`
rw [term_of_ne_zero hn, convolution_def, Finset.sum_div]
refine Finset.sum_congr rfl fun p hp ↦ ?_
have ⟨hp₁, hp₂⟩ := ne_zero_of_mem_divisorsAntidiagonal hp
rw [term_of_ne_zero hp₁, term_of_ne_zero hp₂, mul_comm_div, div_div, ← mul_div_assoc, ← natCast_mul_natCast_cpow, ←
cast_mul, mul_comm p.2, (mem_divisorsAntidiagonal.mp hp).1]
