English
Under summable norms of f and g, the convolution-like product over finite sums converges to the product of sums, with a variant where indices vary with respect to sums.
Русский
При суммируемости норм функций плюс вариации индексов, сумма конволюции сходится к произведению сумм.
LaTeX
$$$((\\sum_i f(i)) (\\sum_j g(j))) = \\sum_{(i,j)\\in \\mathbb{N}\\times\\mathbb{N}} f(i)g(j).$$$
Lean4
theorem summable_mul_of_summable_norm' {f : ι → R} {g : ι' → R} (hf : Summable fun x => ‖f x‖) (h'f : Summable f)
(hg : Summable fun x => ‖g x‖) (h'g : Summable g) : Summable fun x : ι × ι' => f x.1 * g x.2 := by
classical
suffices HasSum (fun x : ι × ι' => f x.1 * g x.2) ((∑' i, f i) * (∑' j, g j)) from this.summable
let s : Finset ι × Finset ι' → Finset (ι × ι') := fun p ↦ p.1 ×ˢ p.2
apply hasSum_of_subseq_of_summable (hf.mul_norm hg) tendsto_finset_prod_atTop
rw [← prod_atTop_atTop_eq]
have := Tendsto.prodMap h'f.hasSum h'g.hasSum
rw [← nhds_prod_eq] at this
convert ((continuous_mul (M := R)).continuousAt (x := (∑' (i : ι), f i, ∑' (j : ι'), g j))).tendsto.comp this with p
simp [sum_product, ← mul_sum, ← sum_mul]
