feat(analysis/inner_product_space/basic): criterion for summability (#11224)

In a complete inner product space `E`, a family `f` of mutually-orthogonal elements of `E` is summable, if and only if
`(λ i, ∥f i∥ ^ 2)` is summable.

Author: hrmacbeth

src/algebra/big_operators/basic.lean

@@ -1277,6 +1277,13 @@ lemma prod_zpow (f : α → β) (s : finset α) (n : ℤ) :
   (∏ a in s, f a) ^ n = ∏ a in s, (f a) ^ n :=
 multiset.prod_map_zpow.symm
 
+@[to_additive]
+lemma prod_sdiff_div_prod_sdiff [decidable_eq α] :
+  (∏ (x : α) in s₂ \ s₁, f x) / (∏ (x : α) in s₁ \ s₂, f x)
+  = (∏ (x : α) in s₂, f x) / (∏ (x : α) in s₁, f x) :=
+by simp [← finset.prod_sdiff (@inf_le_left _ _ s₁ s₂),
+  ← finset.prod_sdiff (@inf_le_right _ _ s₁ s₂)]
+
 end comm_group
 
 @[simp] theorem card_sigma {σ : α → Type*} (s : finset α) (t : Π a, finset (σ a)) :

src/algebra/big_operators/order.lean

@@ -118,9 +118,13 @@ or equal to the corresponding summand `g i` of another finite sum, then
 `∑ i in s, f i ≤ ∑ i in s, g i`. -/
 add_decl_doc sum_le_sum
 
-@[to_additive sum_nonneg]  lemma one_le_prod' (h : ∀i ∈ s, 1 ≤ f i) : 1 ≤ (∏ i in s, f i) :=
+@[to_additive sum_nonneg] lemma one_le_prod' (h : ∀i ∈ s, 1 ≤ f i) : 1 ≤ (∏ i in s, f i) :=
 le_trans (by rw prod_const_one) (prod_le_prod'' h)
 
+@[to_additive finset.sum_nonneg']
+lemma one_le_prod'' (h : ∀ (i : ι), 1 ≤ f i) : 1 ≤ ∏ (i : ι) in s, f i :=
+finset.one_le_prod' (λ i hi, h i)
+
 @[to_additive sum_nonpos] lemma prod_le_one' (h : ∀i ∈ s, f i ≤ 1) : (∏ i in s, f i) ≤ 1 :=
 (prod_le_prod'' h).trans_eq (by rw prod_const_one)
 
@@ -207,6 +211,16 @@ lemma abs_sum_le_sum_abs {G : Type*} [linear_ordered_add_comm_group G] (f : ι 
   |∑ i in s, f i| ≤ ∑ i in s, |f i| :=
 le_sum_of_subadditive _ abs_zero abs_add s f
 
+lemma abs_sum_of_nonneg {G : Type*} [linear_ordered_add_comm_group G] {f : ι → G} {s : finset ι}
+  (hf : ∀ i ∈ s, 0 ≤ f i) :
+  |∑ (i : ι) in s, f i| = ∑ (i : ι) in s, f i :=
+by rw abs_of_nonneg (finset.sum_nonneg hf)
+
+lemma abs_sum_of_nonneg' {G : Type*} [linear_ordered_add_comm_group G] {f : ι → G} {s : finset ι}
+  (hf : ∀ i, 0 ≤ f i) :
+  |∑ (i : ι) in s, f i| = ∑ (i : ι) in s, f i :=
+by rw abs_of_nonneg (finset.sum_nonneg' hf)
+
 lemma abs_prod {R : Type*} [linear_ordered_comm_ring R] {f : ι → R} {s : finset ι} :
   |∏ x in s, f x| = ∏ x in s, |f x| :=
 (abs_hom.to_monoid_hom : R →* R).map_prod _ _

src/analysis/inner_product_space/basic.lean

@@ -1663,6 +1663,27 @@ calc ⟪(v : E), ∑ j : ι, l j⟫
   congr_arg (finset.sum finset.univ) $ funext $ λ j, (hV.eq_ite v (l j))
 ... = ⟪v, l i⟫ : by simp
 
+lemma orthogonal_family.inner_sum (l₁ l₂ : Π i, V i) (s : finset ι) :
+  ⟪∑ i in s, (l₁ i : E), ∑ j in s, (l₂ j : E)⟫ = ∑ i in s, ⟪l₁ i, l₂ i⟫ :=
+by classical;
+calc ⟪∑ i in s, (l₁ i : E), ∑ j in s, (l₂ j : E)⟫
+    = ∑ j in s, ∑ i in s, ⟪(l₁ i : E), l₂ j⟫ : by simp [sum_inner, inner_sum]
+... = ∑ j in s, ∑ i in s, ite (i = j) ⟪(l₁ i : E), l₂ j⟫ 0 :
+begin
+  congr' with i,
+  congr' with j,
+  apply hV.eq_ite,
+end
+... = ∑ i in s, ⟪l₁ i, l₂ i⟫ : by simp [finset.sum_ite_of_true]
+
+lemma orthogonal_family.norm_sum (l : Π i, V i) (s : finset ι) :
+  ∥∑ i in s, (l i : E)∥ ^ 2 = ∑ i in s, ∥l i∥ ^ 2 :=
+begin
+  have : (∥∑ i in s, (l i : E)∥ ^ 2 : 𝕜) = ∑ i in s, ∥l i∥ ^ 2,
+  { simp [← inner_self_eq_norm_sq_to_K, hV.inner_sum] },
+  exact_mod_cast this,
+end
+
 /-- An orthogonal family forms an independent family of subspaces; that is, any collection of
 elements each from a different subspace in the family is linearly independent. In particular, the
 pairwise intersections of elements of the family are 0. -/
@@ -1708,8 +1729,81 @@ lemma direct_sum.submodule_is_internal.collected_basis_orthonormal
   {v_family : Π i, basis (α i) 𝕜 (V i)} (hv_family : ∀ i, orthonormal 𝕜 (v_family i)) :
   orthonormal 𝕜 (hV_sum.collected_basis v_family) :=
 by simpa using hV.orthonormal_sigma_orthonormal hv_family
+
+lemma orthogonal_family.norm_sq_diff_sum (f : Π i, V i) (s₁ s₂ : finset ι) :
+  ∥∑ i in s₁, (f i : E) - ∑ i in s₂, f i∥ ^ 2
+  = ∑ i in s₁ \ s₂, ∥f i∥ ^ 2 + ∑ i in s₂ \ s₁, ∥f i∥ ^ 2 :=
+begin
+  rw [← finset.sum_sdiff_sub_sum_sdiff, sub_eq_add_neg, ← finset.sum_neg_distrib],
+  let F : Π i, V i := λ i, if i ∈ s₁ then f i else - (f i),
+  have hF₁ : ∀ i ∈ s₁ \ s₂, F i = f i := λ i hi, if_pos (finset.sdiff_subset _ _ hi),
+  have hF₂ : ∀ i ∈ s₂ \ s₁, F i = - f i := λ i hi, if_neg (finset.mem_sdiff.mp hi).2,
+  have hF : ∀ i, ∥F i∥ = ∥f i∥,
+  { intros i,
+    dsimp [F],
+    split_ifs;
+    simp, },
+  have : ∥∑ i in s₁ \ s₂, (F i : E) + ∑ i in s₂ \ s₁, F i∥ ^ 2 =
+    ∑ i in s₁ \ s₂, ∥F i∥ ^ 2 + ∑ i in s₂ \ s₁, ∥F i∥ ^ 2,
+  { have hs : disjoint (s₁ \ s₂) (s₂ \ s₁) := disjoint_sdiff_sdiff,
+    simpa only [finset.sum_union hs] using hV.norm_sum F (s₁ \ s₂ ∪ s₂ \ s₁) },
+  convert this using 4,
+  { refine finset.sum_congr rfl (λ i hi, _),
+    simp [hF₁ i hi] },
+  { refine finset.sum_congr rfl (λ i hi, _),
+    simp [hF₂ i hi] },
+  { simp [hF] },
+  { simp [hF] },
+end
+
 omit dec_ι
 
+/-- A family `f` of mutually-orthogonal elements of `E` is summable, if and only if
+`(λ i, ∥f i∥ ^ 2)` is summable. -/
+lemma orthogonal_family.summable_iff_norm_sq_summable [complete_space E] (f : Π i, V i) :
+  summable (λ i, (f i : E)) ↔ summable (λ i, ∥f i∥ ^ 2) :=
+begin
+  classical,
+  simp only [summable_iff_cauchy_seq_finset, normed_group.cauchy_seq_iff, real.norm_eq_abs],
+  split,
+  { intros hf ε hε,
+    obtain ⟨a, H⟩ := hf _ (sqrt_pos.mpr hε),
+    use a,
+    intros s₁ hs₁ s₂ hs₂,
+    rw ← finset.sum_sdiff_sub_sum_sdiff,
+    refine (_root_.abs_sub _ _).trans_lt _,
+    have : ∀ i, 0 ≤ ∥f i∥ ^ 2 := λ i : ι, sq_nonneg _,
+    simp only [finset.abs_sum_of_nonneg' this],
+    have : ∑ i in s₁ \ s₂, ∥f i∥ ^ 2 + ∑ i in s₂ \ s₁, ∥f i∥ ^ 2 < (sqrt ε) ^ 2,
+    { rw ← hV.norm_sq_diff_sum,
+      apply sq_lt_sq,
+      rw _root_.abs_of_nonneg (norm_nonneg _),
+      exact H s₁ hs₁ s₂ hs₂ },
+    have hη := sq_sqrt (le_of_lt hε),
+    linarith },
+  { intros hf ε hε,
+    have hε' : 0 < ε ^ 2 / 2 := half_pos (sq_pos_of_pos hε),
+    obtain ⟨a, H⟩ := hf _ hε',
+    use a,
+    intros s₁ hs₁ s₂ hs₂,
+    refine (abs_lt_of_sq_lt_sq' _ (le_of_lt hε)).2,
+    have has : a ≤ s₁ ⊓ s₂ := le_inf hs₁ hs₂,
+    rw hV.norm_sq_diff_sum,
+    have Hs₁ : ∑ (x : ι) in s₁ \ s₂, ∥f x∥ ^ 2 < ε ^ 2 / 2,
+    { convert H _ hs₁ _ has,
+      have : s₁ ⊓ s₂ ⊆ s₁ := finset.inter_subset_left _ _,
+      rw [← finset.sum_sdiff this, add_tsub_cancel_right, finset.abs_sum_of_nonneg'],
+      { simp },
+      { exact λ i, sq_nonneg _ } },
+    have Hs₂ : ∑ (x : ι) in s₂ \ s₁, ∥f x∥ ^ 2 < ε ^ 2 /2,
+    { convert H _ hs₂ _ has,
+      have : s₁ ⊓ s₂ ⊆ s₂ := finset.inter_subset_right _ _,
+      rw [← finset.sum_sdiff this, add_tsub_cancel_right, finset.abs_sum_of_nonneg'],
+      { simp },
+      { exact λ i, sq_nonneg _ } },
+    linarith },
+end
+
 end orthogonal_family
 
 section is_R_or_C_to_real