English
An orthogonal family of subspaces yields an independent family of subspaces: the iSupIndep of V holds.
Русский
Ортогональное семейство подпространств образует независимое семейство подпространств: iSupIndep(V) выполняется.
LaTeX
$$iSupIndep V$$
Lean4
/-- A family `f` of mutually-orthogonal elements of `E` is summable, if and only if
`(fun i ↦ ‖f i‖ ^ 2)` is summable. -/
theorem summable_iff_norm_sq_summable [CompleteSpace E] (f : ∀ i, G i) :
(Summable fun i => V i (f i)) ↔ Summable fun i => ‖f i‖ ^ 2 := by
classical
simp only [summable_iff_cauchySeq_finset, NormedAddCommGroup.cauchySeq_iff, Real.norm_eq_abs]
constructor
· intro hf ε hε
obtain ⟨a, H⟩ := hf _ (sqrt_pos.mpr hε)
use a
intro s₁ hs₁ s₂ hs₂
rw [← Finset.sum_sdiff_sub_sum_sdiff]
refine (abs_sub _ _).trans_lt ?_
have : ∀ i, 0 ≤ ‖f i‖ ^ 2 := fun i : ι => sq_nonneg _
simp only [Finset.abs_sum_of_nonneg' this]
have : ((∑ i ∈ s₁ \ s₂, ‖f i‖ ^ 2) + ∑ i ∈ s₂ \ s₁, ‖f i‖ ^ 2) < √ε ^ 2 :=
by
rw [← hV.norm_sq_diff_sum, sq_lt_sq, abs_of_nonneg (sqrt_nonneg _), abs_of_nonneg (norm_nonneg _)]
exact H s₁ hs₁ s₂ hs₂
have hη := sq_sqrt (le_of_lt hε)
linarith
· intro hf ε hε
have hε' : 0 < ε ^ 2 / 2 := half_pos (sq_pos_of_pos hε)
obtain ⟨a, H⟩ := hf _ hε'
use a
intro 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 ∈ s₁ \ s₂, ‖f x‖ ^ 2 < ε ^ 2 / 2 :=
by
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 fun i => sq_nonneg _
have Hs₂ : ∑ x ∈ s₂ \ s₁, ‖f x‖ ^ 2 < ε ^ 2 / 2 :=
by
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 fun i => sq_nonneg _
linarith
