feat(topology/algebra/infinite_sum, analysis/normed_space/basic): pro…

…duct of two tsums, cauchy product (#8445)

src/analysis/normed_space/basic.lean

@@ -6,7 +6,7 @@ Authors: Patrick Massot, Johannes Hölzl
 import algebra.algebra.subalgebra
 import order.liminf_limsup
 import topology.algebra.group_completion
-import topology.instances.nnreal
+import topology.instances.ennreal
 import topology.metric_space.completion
 import topology.sequences
 import topology.locally_constant.algebra
@@ -1985,6 +1985,127 @@ summable_of_nnnorm_bounded _ hf (assume i, le_refl _)
 
 end summable
 
+section cauchy_product
+
+/-! ## Multipliying two infinite sums in a normed ring
+
+In this section, we prove various results about `(∑' x : ι, f x) * (∑' y : ι', g y)` in a normed
+ring. There are similar results proven in `topology/algebra/infinite_sum` (e.g `tsum_mul_tsum`),
+but in a normed ring we get summability results which aren't true in general.
+
+We first establish results about arbitrary index types, `β` and `γ`, and then we specialize to
+`β = γ = ℕ` to prove the Cauchy product formula
+(see `tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm`).
+
+### Arbitrary index types
+-/
+
+variables {ι' : Type*} [normed_ring α]
+
+open finset
+open_locale classical
+
+lemma summable.mul_of_nonneg {f : ι → ℝ} {g : ι' → ℝ}
+  (hf : summable f) (hg : summable g) (hf' : 0 ≤ f) (hg' : 0 ≤ g) :
+  summable (λ (x : ι × ι'), f x.1 * g x.2) :=
+let ⟨s, hf⟩ := hf in
+let ⟨t, hg⟩ := hg in
+suffices this : ∀ u : finset (ι × ι'), ∑ x in u, f x.1 * g x.2 ≤ s*t,
+  from summable_of_sum_le (λ x, mul_nonneg (hf' _) (hg' _)) this,
+assume u,
+calc  ∑ x in u, f x.1 * g x.2
+    ≤ ∑ x in (u.image prod.fst).product (u.image prod.snd), f x.1 * g x.2 :
+      sum_mono_set_of_nonneg (λ x, mul_nonneg (hf' _) (hg' _)) subset_product
+... = ∑ x in u.image prod.fst, ∑ y in u.image prod.snd, f x * g y : sum_product
+... = ∑ x in u.image prod.fst, f x * ∑ y in u.image prod.snd, g y :
+      sum_congr rfl (λ x _, mul_sum.symm)
+... ≤ ∑ x in u.image prod.fst, f x * t :
+      sum_le_sum
+        (λ x _, mul_le_mul_of_nonneg_left (sum_le_has_sum _ (λ _ _, hg' _) hg) (hf' _))
+... = (∑ x in u.image prod.fst, f x) * t : sum_mul.symm
+... ≤ s * t :
+      mul_le_mul_of_nonneg_right (sum_le_has_sum _ (λ _ _, hf' _) hf) (hg.nonneg $ λ _, hg' _)
+
+lemma summable.mul_norm {f : ι → α} {g : ι' → α}
+  (hf : summable (λ x, ∥f x∥)) (hg : summable (λ x, ∥g x∥)) :
+  summable (λ (x : ι × ι'), ∥f x.1 * g x.2∥) :=
+summable_of_nonneg_of_le (λ x, norm_nonneg (f x.1 * g x.2)) (λ x, norm_mul_le (f x.1) (g x.2))
+  (hf.mul_of_nonneg hg (λ x, norm_nonneg $ f x) (λ x, norm_nonneg $ g x) : _)
+
+lemma summable_mul_of_summable_norm [complete_space α] {f : ι → α} {g : ι' → α}
+  (hf : summable (λ x, ∥f x∥)) (hg : summable (λ x, ∥g x∥)) :
+  summable (λ (x : ι × ι'), f x.1 * g x.2) :=
+summable_of_summable_norm (hf.mul_norm hg)
+
+/-- Product of two infinites sums indexed by arbitrary types.
+    See also `tsum_mul_tsum` if `f` and `g` are *not* absolutely summable. -/
+lemma tsum_mul_tsum_of_summable_norm [complete_space α] {f : ι → α} {g : ι' → α}
+  (hf : summable (λ x, ∥f x∥)) (hg : summable (λ x, ∥g x∥)) :
+  (∑' x, f x) * (∑' y, g y) = (∑' z : ι × ι', f z.1 * g z.2) :=
+tsum_mul_tsum (summable_of_summable_norm hf) (summable_of_summable_norm hg)
+  (summable_mul_of_summable_norm hf hg)
+
+/-! ### `ℕ`-indexed families (Cauchy product)
+
+We prove two versions of the Cauchy product formula. The first one is
+`tsum_mul_tsum_eq_tsum_sum_range_of_summable_norm`, where the `n`-th term is a sum over
+`finset.range (n+1)` involving `nat` substraction.
+In order to avoid `nat` substraction, we also provide
+`tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm`,
+where the `n`-th term is a sum over all pairs `(k, l)` such that `k+l=n`, which corresponds to the
+`finset` `finset.nat.antidiagonal n`. -/
+
+section nat
+
+open finset.nat
+
+lemma summable_norm_sum_mul_antidiagonal_of_summable_norm {f g : ℕ → α}
+  (hf : summable (λ x, ∥f x∥)) (hg : summable (λ x, ∥g x∥)) :
+  summable (λ n, ∥∑ kl in antidiagonal n, f kl.1 * g kl.2∥) :=
+begin
+  have := summable_sum_mul_antidiagonal_of_summable_mul
+    (summable.mul_of_nonneg hf hg (λ _, norm_nonneg _) (λ _, norm_nonneg _)),
+  refine summable_of_nonneg_of_le (λ _, norm_nonneg _) _ this,
+  intros n,
+  calc  ∥∑ kl in antidiagonal n, f kl.1 * g kl.2∥
+      ≤ ∑ kl in antidiagonal n, ∥f kl.1 * g kl.2∥ : norm_sum_le _ _
+  ... ≤ ∑ kl in antidiagonal n, ∥f kl.1∥ * ∥g kl.2∥ : sum_le_sum (λ i _, norm_mul_le _ _)
+end
+
+/-- The Cauchy product formula for the product of two infinites sums indexed by `ℕ`,
+    expressed by summing on `finset.nat.antidiagonal`.
+    See also `tsum_mul_tsum_eq_tsum_sum_antidiagonal` if `f` and `g` are
+    *not* absolutely summable. -/
+lemma tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm [complete_space α] {f g : ℕ → α}
+  (hf : summable (λ x, ∥f x∥)) (hg : summable (λ x, ∥g x∥)) :
+  (∑' n, f n) * (∑' n, g n) = ∑' n, ∑ kl in antidiagonal n, f kl.1 * g kl.2 :=
+tsum_mul_tsum_eq_tsum_sum_antidiagonal (summable_of_summable_norm hf) (summable_of_summable_norm hg)
+  (summable_mul_of_summable_norm hf hg)
+
+lemma summable_norm_sum_mul_range_of_summable_norm {f g : ℕ → α}
+  (hf : summable (λ x, ∥f x∥)) (hg : summable (λ x, ∥g x∥)) :
+  summable (λ n, ∥∑ k in range (n+1), f k * g (n - k)∥) :=
+begin
+  simp_rw ← sum_antidiagonal_eq_sum_range_succ (λ k l, f k * g l),
+  exact summable_norm_sum_mul_antidiagonal_of_summable_norm hf hg
+end
+
+/-- The Cauchy product formula for the product of two infinites sums indexed by `ℕ`,
+    expressed by summing on `finset.range`.
+    See also `tsum_mul_tsum_eq_tsum_sum_range` if `f` and `g` are
+    *not* absolutely summable. -/
+lemma tsum_mul_tsum_eq_tsum_sum_range_of_summable_norm [complete_space α] {f g : ℕ → α}
+  (hf : summable (λ x, ∥f x∥)) (hg : summable (λ x, ∥g x∥)) :
+  (∑' n, f n) * (∑' n, g n) = ∑' n, ∑ k in range (n+1), f k * g (n - k) :=
+begin
+  simp_rw ← sum_antidiagonal_eq_sum_range_succ (λ k l, f k * g l),
+  exact tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm hf hg
+end
+
+end nat
+
+end cauchy_product
+
 namespace uniform_space
 namespace completion
 

src/data/finset/nat_antidiagonal.lean

@@ -74,6 +74,23 @@ begin
   rw [hq, ← h, hp],
 end
 
+section equiv_prod
+
+/-- The disjoint union of antidiagonals `Σ (n : ℕ), antidiagonal n` is equivalent to the product
+    `ℕ × ℕ`. This is such an equivalence, obtained by mapping `(n, (k, l))` to `(k, l)`. -/
+@[simps] def sigma_antidiagonal_equiv_prod : (Σ (n : ℕ), antidiagonal n) ≃ ℕ × ℕ :=
+{ to_fun := λ x, x.2,
+  inv_fun := λ x, ⟨x.1 + x.2, x, mem_antidiagonal.mpr rfl⟩,
+  left_inv :=
+    begin
+      rintros ⟨n, ⟨k, l⟩, h⟩,
+      rw mem_antidiagonal at h,
+      exact sigma.subtype_ext h rfl,
+    end,
+  right_inv := λ x, rfl }
+
+end equiv_prod
+
 end nat
 
 end finset

src/topology/algebra/infinite_sum.lean

@@ -10,6 +10,7 @@ import algebra.indicator_function
 import data.equiv.encodable.lattice
 import data.fintype.card
 import data.nat.parity
+import algebra.big_operators.nat_antidiagonal
 import order.filter.at_top_bot
 
 /-!
@@ -1222,3 +1223,119 @@ lemma dist_le_tsum_dist_of_tendsto₀ [pseudo_metric_space α] {f : ℕ → α}
 by simpa only [zero_add] using dist_le_tsum_dist_of_tendsto h ha 0
 
 end cauchy_seq
+
+/-! ## Multipliying two infinite sums
+
+In this section, we prove various results about `(∑' x : β, f x) * (∑' y : γ, g y)`. Not that we
+always assume that the family `λ x : β × γ, f x.1 * g x.2` is summable, since there is no way to
+deduce this from the summmabilities of `f` and `g` in general, but if you are working in a normed
+space, you may want to use the analogous lemmas in `analysis/normed_space/basic`
+(e.g `tsum_mul_tsum_of_summable_norm`).
+
+We first establish results about arbitrary index types, `β` and `γ`, and then we specialize to
+`β = γ = ℕ` to prove the Cauchy product formula (see `tsum_mul_tsum_eq_tsum_sum_antidiagonal`).
+
+### Arbitrary index types
+-/
+
+section tsum_mul_tsum
+
+variables [topological_space α] [regular_space α] [semiring α] [topological_semiring α]
+  {f : β → α} {g : γ → α} {s t u : α}
+
+lemma has_sum.mul_eq (hf : has_sum f s) (hg : has_sum g t)
+  (hfg : has_sum (λ (x : β × γ), f x.1 * g x.2) u) :
+  s * t = u :=
+have key₁ : has_sum (λ b, f b * t) (s * t),
+  from hf.mul_right t,
+have this : ∀ b : β, has_sum (λ c : γ, f b * g c) (f b * t),
+  from λ b, hg.mul_left (f b),
+have key₂ : has_sum (λ b, f b * t) u,
+  from has_sum.prod_fiberwise hfg this,
+key₁.unique key₂
+
+lemma has_sum.mul (hf : has_sum f s) (hg : has_sum g t)
+  (hfg : summable (λ (x : β × γ), f x.1 * g x.2)) :
+  has_sum (λ (x : β × γ), f x.1 * g x.2) (s * t) :=
+let ⟨u, hu⟩ := hfg in
+(hf.mul_eq hg hu).symm ▸ hu
+
+/-- Product of two infinites sums indexed by arbitrary types.
+    See also `tsum_mul_tsum_of_summable_norm` if `f` and `g` are abolutely summable. -/
+lemma tsum_mul_tsum (hf : summable f) (hg : summable g)
+  (hfg : summable (λ (x : β × γ), f x.1 * g x.2)) :
+  (∑' x, f x) * (∑' y, g y) = (∑' z : β × γ, f z.1 * g z.2) :=
+hf.has_sum.mul_eq hg.has_sum hfg.has_sum
+
+end tsum_mul_tsum
+
+section cauchy_product
+
+/-! ### `ℕ`-indexed families (Cauchy product)
+
+We prove two versions of the Cauchy product formula. The first one is
+`tsum_mul_tsum_eq_tsum_sum_range`, where the `n`-th term is a sum over `finset.range (n+1)`
+involving `nat` substraction.
+In order to avoid `nat` substraction, we also provide `tsum_mul_tsum_eq_tsum_sum_antidiagonal`,
+where the `n`-th term is a sum over all pairs `(k, l)` such that `k+l=n`, which corresponds to the
+`finset` `finset.nat.antidiagonal n` -/
+
+variables {f : ℕ → α} {g : ℕ → α}
+
+open finset
+
+variables [topological_space α] [semiring α]
+
+/- The family `(k, l) : ℕ × ℕ ↦ f k * g l` is summable if and only if the family
+`(n, k, l) : Σ (n : ℕ), nat.antidiagonal n ↦ f k * g l` is summable. -/
+lemma summable_mul_prod_iff_summable_mul_sigma_antidiagonal {f g : ℕ → α} :
+  summable (λ x : ℕ × ℕ, f x.1 * g x.2) ↔
+  summable (λ x : (Σ (n : ℕ), nat.antidiagonal n), f (x.2 : ℕ × ℕ).1 * g (x.2 : ℕ × ℕ).2) :=
+nat.sigma_antidiagonal_equiv_prod.summable_iff.symm
+
+variables [regular_space α] [topological_semiring α]
+
+lemma summable_sum_mul_antidiagonal_of_summable_mul {f g : ℕ → α}
+  (h : summable (λ x : ℕ × ℕ, f x.1 * g x.2)) :
+  summable (λ n, ∑ kl in nat.antidiagonal n, f kl.1 * g kl.2) :=
+begin
+  rw summable_mul_prod_iff_summable_mul_sigma_antidiagonal at h,
+  conv {congr, funext, rw [← finset.sum_finset_coe, ← tsum_fintype]},
+  exact h.sigma' (λ n, (has_sum_fintype _).summable),
+end
+
+/-- The Cauchy product formula for the product of two infinites sums indexed by `ℕ`,
+    expressed by summing on `finset.nat.antidiagonal`.
+    See also `tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm`
+    if `f` and `g` are absolutely summable. -/
+lemma tsum_mul_tsum_eq_tsum_sum_antidiagonal (hf : summable f) (hg : summable g)
+  (hfg : summable (λ (x : ℕ × ℕ), f x.1 * g x.2)) :
+  (∑' n, f n) * (∑' n, g n) = (∑' n, ∑ kl in nat.antidiagonal n, f kl.1 * g kl.2) :=
+begin
+  conv_rhs {congr, funext, rw [← finset.sum_finset_coe, ← tsum_fintype]},
+  rw [tsum_mul_tsum hf hg hfg, ← nat.sigma_antidiagonal_equiv_prod.tsum_eq (_ : ℕ × ℕ → α)],
+  exact tsum_sigma' (λ n, (has_sum_fintype _).summable)
+    (summable_mul_prod_iff_summable_mul_sigma_antidiagonal.mp hfg)
+end
+
+lemma summable_sum_mul_range_of_summable_mul {f g : ℕ → α}
+  (h : summable (λ x : ℕ × ℕ, f x.1 * g x.2)) :
+  summable (λ n, ∑ k in range (n+1), f k * g (n - k)) :=
+begin
+  simp_rw ← nat.sum_antidiagonal_eq_sum_range_succ (λ k l, f k * g l),
+  exact summable_sum_mul_antidiagonal_of_summable_mul h
+end
+
+/-- The Cauchy product formula for the product of two infinites sums indexed by `ℕ`,
+    expressed by summing on `finset.range`.
+    See also `tsum_mul_tsum_eq_tsum_sum_range_of_summable_norm`
+    if `f` and `g` are absolutely summable. -/
+lemma tsum_mul_tsum_eq_tsum_sum_range (hf : summable f) (hg : summable g)
+  (hfg : summable (λ (x : ℕ × ℕ), f x.1 * g x.2)) :
+  (∑' n, f n) * (∑' n, g n) = (∑' n, ∑ k in range (n+1), f k * g (n - k)) :=
+begin
+  simp_rw ← nat.sum_antidiagonal_eq_sum_range_succ (λ k l, f k * g l),
+  exact tsum_mul_tsum_eq_tsum_sum_antidiagonal hf hg hfg
+end
+
+end cauchy_product

src/topology/instances/ennreal.lean

@@ -916,6 +916,12 @@ lemma summable_sigma_of_nonneg {β : Π x : α, Type*} {f : (Σ x, β x) → ℝ
   summable f ↔ (∀ x, summable (λ y, f ⟨x, y⟩)) ∧ summable (λ x, ∑' y, f ⟨x, y⟩) :=
 by { lift f to (Σ x, β x) → ℝ≥0 using hf, exact_mod_cast nnreal.summable_sigma }
 
+lemma summable_of_sum_le {ι : Type*} {f : ι → ℝ} {c : ℝ} (hf : 0 ≤ f)
+  (h : ∀ u : finset ι, ∑ x in u, f x ≤ c) :
+  summable f :=
+⟨ ⨆ u : finset ι, ∑ x in u, f x,
+  tendsto_at_top_csupr (finset.sum_mono_set_of_nonneg hf) ⟨c, λ y ⟨u, hu⟩, hu ▸ h u⟩ ⟩
+
 lemma summable_of_sum_range_le {f : ℕ → ℝ} {c : ℝ} (hf : ∀ n, 0 ≤ f n)
   (h : ∀ n, ∑ i in finset.range n, f i ≤ c) : summable f :=
 begin