𝕜 : Type u_4
E : Type u_1
F : Type ?u.3720833
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_2
G : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst✝ : CompleteSpace E
f : (i : ι) → G i
⊢ (Summable fun i => ↑(V i) (f i)) ↔ Summable fun i => ‖f i‖ ^ 2
𝕜 : Type u_4
E : Type u_1
F : Type ?u.3720833
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_2
dec_ι : DecidableEq ι
G : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst✝ : CompleteSpace E
f : (i : ι) → G i
⊢ (Summable fun i => ↑(V i) (f i)) ↔ Summable fun i => ‖f i‖ ^ 2
clear dec_ι
𝕜 : Type u_4
E : Type u_1
F : Type ?u.3720833
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_2
G : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst✝ : CompleteSpace E
f : (i : ι) → G i
⊢ (∀ (ε : ℝ),
      ε > 0 →
        ∃ N,
          ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → ‖∑ b in m, ↑(V b) (f b) - ∑ b in n, ↑(V b) (f b)‖ < ε) ↔
    ∀ (ε : ℝ),
      ε > 0 →
        ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε
𝕜 : Type u_4
E : Type u_1
F : Type ?u.3720833
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_2
G : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst✝ : CompleteSpace E
f : (i : ι) → G i
⊢ (Summable fun i => ↑(V i) (f i)) ↔ Summable fun i => ‖f i‖ ^ 2
simp only [summable_iff_cauchySeq_finset, NormedAddCommGroup.cauchySeq_iff, Real.norm_eq_abs]
case mp
𝕜 : Type u_4
E : Type u_1
F : Type ?u.3720833
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_2
G : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst✝ : CompleteSpace E
f : (i : ι) → G i
⊢ (∀ (ε : ℝ),
      ε > 0 →
        ∃ N,
          ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → ‖∑ b in m, ↑(V b) (f b) - ∑ b in n, ↑(V b) (f b)‖ < ε) →
    ∀ (ε : ℝ),
      ε > 0 →
        ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε

case mpr
𝕜 : Type u_4
E : Type u_1
F : Type ?u.3720833
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_2
G : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst✝ : CompleteSpace E
f : (i : ι) → G i
⊢ (∀ (ε : ℝ),
      ε > 0 →
        ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε) →
    ∀ (ε : ℝ),
      ε > 0 →
        ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → ‖∑ b in m, ↑(V b) (f b) - ∑ b in n, ↑(V b) (f b)‖ < ε
𝕜 : Type u_4
E : Type u_1
F : Type ?u.3720833
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_2
G : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst✝ : CompleteSpace E
f : (i : ι) → G i
⊢ (∀ (ε : ℝ),
      ε > 0 →
        ∃ N,
          ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → ‖∑ b in m, ↑(V b) (f b) - ∑ b in n, ↑(V b) (f b)‖ < ε) ↔
    ∀ (ε : ℝ),
      ε > 0 →
        ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε
constructor
case mp
𝕜 : Type u_4
E : Type u_1
F : Type ?u.3720833
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_2
G : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst✝ : CompleteSpace E
f : (i : ι) → G i
hf :
  ∀ (ε : ℝ),
    ε > 0 →
      ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → ‖∑ b in m, ↑(V b) (f b) - ∑ b in n, ↑(V b) (f b)‖ < ε
ε : ℝ
hε : ε > 0
⊢ ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε
case mp
𝕜 : Type u_4
E : Type u_1
F : Type ?u.3720833
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_2
G : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst✝ : CompleteSpace E
f : (i : ι) → G i
⊢ (∀ (ε : ℝ),
      ε > 0 →
        ∃ N,
          ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → ‖∑ b in m, ↑(V b) (f b) - ∑ b in n, ↑(V b) (f b)‖ < ε) →
    ∀ (ε : ℝ),
      ε > 0 →
        ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε
intro hf ε hε
case mp.intro
𝕜 : Type u_4
E : Type u_1
F : Type ?u.3720833
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_2
G : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst✝ : CompleteSpace E
f : (i : ι) → G i
hf :
  ∀ (ε : ℝ),
    ε > 0 →
      ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → ‖∑ b in m, ↑(V b) (f b) - ∑ b in n, ↑(V b) (f b)‖ < ε
ε : ℝ
hε : ε > 0
a : Finset ι
H : ∀ (m : Finset ι), a ≤ m → ∀ (n : Finset ι), a ≤ n → ‖∑ b in m, ↑(V b) (f b) - ∑ b in n, ↑(V b) (f b)‖ < sqrt ε
⊢ ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε
case mp
𝕜 : Type u_4
E : Type u_1
F : Type ?u.3720833
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_2
G : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst✝ : CompleteSpace E
f : (i : ι) → G i
hf :
  ∀ (ε : ℝ),
    ε > 0 →
      ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → ‖∑ b in m, ↑(V b) (f b) - ∑ b in n, ↑(V b) (f b)‖ < ε
ε : ℝ
hε : ε > 0
⊢ ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε
obtain ⟨a, H⟩ := hf _ (sqrt_pos.mpr hε)
case mp.intro
𝕜 : Type u_4
E : Type u_1
F : Type ?u.3720833
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_2
G : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst✝ : CompleteSpace E
f : (i : ι) → G i
hf :
  ∀ (ε : ℝ),
    ε > 0 →
      ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → ‖∑ b in m, ↑(V b) (f b) - ∑ b in n, ↑(V b) (f b)‖ < ε
ε : ℝ
hε : ε > 0
a : Finset ι
H : ∀ (m : Finset ι), a ≤ m → ∀ (n : Finset ι), a ≤ n → ‖∑ b in m, ↑(V b) (f b) - ∑ b in n, ↑(V b) (f b)‖ < sqrt ε
⊢ ∀ (m : Finset ι), a ≤ m → ∀ (n : Finset ι), a ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε
case mp.intro
𝕜 : Type u_4
E : Type u_1
F : Type ?u.3720833
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_2
G : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst✝ : CompleteSpace E
f : (i : ι) → G i
hf :
  ∀ (ε : ℝ),
    ε > 0 →
      ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → ‖∑ b in m, ↑(V b) (f b) - ∑ b in n, ↑(V b) (f b)‖ < ε
ε : ℝ
hε : ε > 0
a : Finset ι
H : ∀ (m : Finset ι), a ≤ m → ∀ (n : Finset ι), a ≤ n → ‖∑ b in m, ↑(V b) (f b) - ∑ b in n, ↑(V b) (f b)‖ < sqrt ε
⊢ ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε
use a
case mp.intro
𝕜 : Type u_4
E : Type u_1
F : Type ?u.3720833
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_2
G : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst✝ : CompleteSpace E
f : (i : ι) → G i
hf :
  ∀ (ε : ℝ),
    ε > 0 →
      ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → ‖∑ b in m, ↑(V b) (f b) - ∑ b in n, ↑(V b) (f b)‖ < ε
ε : ℝ
hε : ε > 0
a : Finset ι
H : ∀ (m : Finset ι), a ≤ m → ∀ (n : Finset ι), a ≤ n → ‖∑ b in m, ↑(V b) (f b) - ∑ b in n, ↑(V b) (f b)‖ < sqrt ε
s₁ : Finset ι
hs₁ : a ≤ s₁
s₂ : Finset ι
hs₂ : a ≤ s₂
⊢ abs (∑ i in s₁, ‖f i‖ ^ 2 - ∑ i in s₂, ‖f i‖ ^ 2) < ε
case mp.intro
𝕜 : Type u_4
E : Type u_1
F : Type ?u.3720833
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_2
G : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst✝ : CompleteSpace E
f : (i : ι) → G i
hf :
  ∀ (ε : ℝ),
    ε > 0 →
      ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → ‖∑ b in m, ↑(V b) (f b) - ∑ b in n, ↑(V b) (f b)‖ < ε
ε : ℝ
hε : ε > 0
a : Finset ι
H : ∀ (m : Finset ι), a ≤ m → ∀ (n : Finset ι), a ≤ n → ‖∑ b in m, ↑(V b) (f b) - ∑ b in n, ↑(V b) (f b)‖ < sqrt ε
⊢ ∀ (m : Finset ι), a ≤ m → ∀ (n : Finset ι), a ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε
intro s₁ hs₁ s₂ hs₂
case mp.intro
𝕜 : Type u_4
E : Type u_1
F : Type ?u.3720833
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_2
G : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst✝ : CompleteSpace E
f : (i : ι) → G i
hf :
  ∀ (ε : ℝ),
    ε > 0 →
      ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → ‖∑ b in m, ↑(V b) (f b) - ∑ b in n, ↑(V b) (f b)‖ < ε
ε : ℝ
hε : ε > 0
a : Finset ι
H : ∀ (m : Finset ι), a ≤ m → ∀ (n : Finset ι), a ≤ n → ‖∑ b in m, ↑(V b) (f b) - ∑ b in n, ↑(V b) (f b)‖ < sqrt ε
s₁ : Finset ι
hs₁ : a ≤ s₁
s₂ : Finset ι
hs₂ : a ≤ s₂
⊢ abs (∑ x in s₁ \ s₂, ‖f x‖ ^ 2 - ∑ x in s₂ \ s₁, ‖f x‖ ^ 2) < ε
case mp.intro
𝕜 : Type u_4
E : Type u_1
F : Type ?u.3720833
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_2
G : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst✝ : CompleteSpace E
f : (i : ι) → G i
hf :
  ∀ (ε : ℝ),
    ε > 0 →
      ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → ‖∑ b in m, ↑(V b) (f b) - ∑ b in n, ↑(V b) (f b)‖ < ε
ε : ℝ
hε : ε > 0
a : Finset ι
H : ∀ (m : Finset ι), a ≤ m → ∀ (n : Finset ι), a ≤ n → ‖∑ b in m, ↑(V b) (f b) - ∑ b in n, ↑(V b) (f b)‖ < sqrt ε
s₁ : Finset ι
hs₁ : a ≤ s₁
s₂ : Finset ι
hs₂ : a ≤ s₂
⊢ abs (∑ i in s₁, ‖f i‖ ^ 2 - ∑ i in s₂, ‖f i‖ ^ 2) < ε
rw [← Finset.sum_sdiff_sub_sum_sdiff]
case mp.intro
𝕜 : Type u_4
E : Type u_1
F : Type ?u.3720833
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_2
G : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst✝ : CompleteSpace E
f : (i : ι) → G i
hf :
  ∀ (ε : ℝ),
    ε > 0 →
      ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → ‖∑ b in m, ↑(V b) (f b) - ∑ b in n, ↑(V b) (f b)‖ < ε
ε : ℝ
hε : ε > 0
a : Finset ι
H : ∀ (m : Finset ι), a ≤ m → ∀ (n : Finset ι), a ≤ n → ‖∑ b in m, ↑(V b) (f b) - ∑ b in n, ↑(V b) (f b)‖ < sqrt ε
s₁ : Finset ι
hs₁ : a ≤ s₁
s₂ : Finset ι
hs₂ : a ≤ s₂
⊢ abs (∑ x in s₁ \ s₂, ‖f x‖ ^ 2) + abs (∑ x in s₂ \ s₁, ‖f x‖ ^ 2) < ε
case mp.intro
𝕜 : Type u_4
E : Type u_1
F : Type ?u.3720833
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_2
G : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst✝ : CompleteSpace E
f : (i : ι) → G i
hf :
  ∀ (ε : ℝ),
    ε > 0 →
      ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → ‖∑ b in m, ↑(V b) (f b) - ∑ b in n, ↑(V b) (f b)‖ < ε
ε : ℝ
hε : ε > 0
a : Finset ι
H : ∀ (m : Finset ι), a ≤ m → ∀ (n : Finset ι), a ≤ n → ‖∑ b in m, ↑(V b) (f b) - ∑ b in n, ↑(V b) (f b)‖ < sqrt ε
s₁ : Finset ι
hs₁ : a ≤ s₁
s₂ : Finset ι
hs₂ : a ≤ s₂
⊢ abs (∑ x in s₁ \ s₂, ‖f x‖ ^ 2 - ∑ x in s₂ \ s₁, ‖f x‖ ^ 2) < ε
refine' (abs_sub _ _).trans_lt _
case mp.intro
𝕜 : Type u_4
E : Type u_1
F : Type ?u.3720833
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_2
G : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst✝ : CompleteSpace E
f : (i : ι) → G i
hf :
  ∀ (ε : ℝ),
    ε > 0 →
      ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → ‖∑ b in m, ↑(V b) (f b) - ∑ b in n, ↑(V b) (f b)‖ < ε
ε : ℝ
hε : ε > 0
a : Finset ι
H : ∀ (m : Finset ι), a ≤ m → ∀ (n : Finset ι), a ≤ n → ‖∑ b in m, ↑(V b) (f b) - ∑ b in n, ↑(V b) (f b)‖ < sqrt ε
s₁ : Finset ι
hs₁ : a ≤ s₁
s₂ : Finset ι
hs₂ : a ≤ s₂
this : ∀ (i : ι), 0 ≤ ‖f i‖ ^ 2
⊢ abs (∑ x in s₁ \ s₂, ‖f x‖ ^ 2) + abs (∑ x in s₂ \ s₁, ‖f x‖ ^ 2) < ε
case mp.intro
𝕜 : Type u_4
E : Type u_1
F : Type ?u.3720833
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_2
G : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst✝ : CompleteSpace E
f : (i : ι) → G i
hf :
  ∀ (ε : ℝ),
    ε > 0 →
      ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → ‖∑ b in m, ↑(V b) (f b) - ∑ b in n, ↑(V b) (f b)‖ < ε
ε : ℝ
hε : ε > 0
a : Finset ι
H : ∀ (m : Finset ι), a ≤ m → ∀ (n : Finset ι), a ≤ n → ‖∑ b in m, ↑(V b) (f b) - ∑ b in n, ↑(V b) (f b)‖ < sqrt ε
s₁ : Finset ι
hs₁ : a ≤ s₁
s₂ : Finset ι
hs₂ : a ≤ s₂
⊢ abs (∑ x in s₁ \ s₂, ‖f x‖ ^ 2) + abs (∑ x in s₂ \ s₁, ‖f x‖ ^ 2) < ε
have : ∀ i, 0 ≤ ‖f i‖ ^ 2 := fun i : ι => sq_nonneg _
case mp.intro
𝕜 : Type u_4
E : Type u_1
F : Type ?u.3720833
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_2
G : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst✝ : CompleteSpace E
f : (i : ι) → G i
hf :
  ∀ (ε : ℝ),
    ε > 0 →
      ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → ‖∑ b in m, ↑(V b) (f b) - ∑ b in n, ↑(V b) (f b)‖ < ε
ε : ℝ
hε : ε > 0
a : Finset ι
H : ∀ (m : Finset ι), a ≤ m → ∀ (n : Finset ι), a ≤ n → ‖∑ b in m, ↑(V b) (f b) - ∑ b in n, ↑(V b) (f b)‖ < sqrt ε
s₁ : Finset ι
hs₁ : a ≤ s₁
s₂ : Finset ι
hs₂ : a ≤ s₂
this : ∀ (i : ι), 0 ≤ ‖f i‖ ^ 2
⊢ ∑ x in s₁ \ s₂, ‖f x‖ ^ 2 + ∑ x in s₂ \ s₁, ‖f x‖ ^ 2 < ε
case mp.intro
𝕜 : Type u_4
E : Type u_1
F : Type ?u.3720833
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_2
G : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst✝ : CompleteSpace E
f : (i : ι) → G i
hf :
  ∀ (ε : ℝ),
    ε > 0 →
      ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → ‖∑ b in m, ↑(V b) (f b) - ∑ b in n, ↑(V b) (f b)‖ < ε
ε : ℝ
hε : ε > 0
a : Finset ι
H : ∀ (m : Finset ι), a ≤ m → ∀ (n : Finset ι), a ≤ n → ‖∑ b in m, ↑(V b) (f b) - ∑ b in n, ↑(V b) (f b)‖ < sqrt ε
s₁ : Finset ι
hs₁ : a ≤ s₁
s₂ : Finset ι
hs₂ : a ≤ s₂
this : ∀ (i : ι), 0 ≤ ‖f i‖ ^ 2
⊢ abs (∑ x in s₁ \ s₂, ‖f x‖ ^ 2) + abs (∑ x in s₂ \ s₁, ‖f x‖ ^ 2) < ε
simp only [Finset.abs_sum_of_nonneg' this]
case mp.intro
𝕜 : Type u_4
E : Type u_1
F : Type ?u.3720833
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_2
G : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst✝ : CompleteSpace E
f : (i : ι) → G i
hf :
  ∀ (ε : ℝ),
    ε > 0 →
      ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → ‖∑ b in m, ↑(V b) (f b) - ∑ b in n, ↑(V b) (f b)‖ < ε
ε : ℝ
hε : ε > 0
a : Finset ι
H : ∀ (m : Finset ι), a ≤ m → ∀ (n : Finset ι), a ≤ n → ‖∑ b in m, ↑(V b) (f b) - ∑ b in n, ↑(V b) (f b)‖ < sqrt ε
s₁ : Finset ι
hs₁ : a ≤ s₁
s₂ : Finset ι
hs₂ : a ≤ s₂
this✝ : ∀ (i : ι), 0 ≤ ‖f i‖ ^ 2
this : ∑ i in s₁ \ s₂, ‖f i‖ ^ 2 + ∑ i in s₂ \ s₁, ‖f i‖ ^ 2 < sqrt ε ^ 2
⊢ ∑ x in s₁ \ s₂, ‖f x‖ ^ 2 + ∑ x in s₂ \ s₁, ‖f x‖ ^ 2 < ε
case mp.intro
𝕜 : Type u_4
E : Type u_1
F : Type ?u.3720833
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_2
G : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst✝ : CompleteSpace E
f : (i : ι) → G i
hf :
  ∀ (ε : ℝ),
    ε > 0 →
      ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → ‖∑ b in m, ↑(V b) (f b) - ∑ b in n, ↑(V b) (f b)‖ < ε
ε : ℝ
hε : ε > 0
a : Finset ι
H : ∀ (m : Finset ι), a ≤ m → ∀ (n : Finset ι), a ≤ n → ‖∑ b in m, ↑(V b) (f b) - ∑ b in n, ↑(V b) (f b)‖ < sqrt ε
s₁ : Finset ι
hs₁ : a ≤ s₁
s₂ : Finset ι
hs₂ : a ≤ s₂
this : ∀ (i : ι), 0 ≤ ‖f i‖ ^ 2
⊢ ∑ x in s₁ \ s₂, ‖f x‖ ^ 2 + ∑ x in s₂ \ s₁, ‖f x‖ ^ 2 < ε
have : ((∑ i in s₁ \ s₂, ‖f i‖ ^ 2) + ∑ i in s₂ \ s₁, ‖f i‖ ^ 2) < sqrt ε ^ 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₂
case mp.intro
𝕜 : Type u_4
E : Type u_1
F : Type ?u.3720833
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_2
G : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst✝ : CompleteSpace E
f : (i : ι) → G i
hf :
  ∀ (ε : ℝ),
    ε > 0 →
      ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → ‖∑ b in m, ↑(V b) (f b) - ∑ b in n, ↑(V b) (f b)‖ < ε
ε : ℝ
hε : ε > 0
a : Finset ι
H : ∀ (m : Finset ι), a ≤ m → ∀ (n : Finset ι), a ≤ n → ‖∑ b in m, ↑(V b) (f b) - ∑ b in n, ↑(V b) (f b)‖ < sqrt ε
s₁ : Finset ι
hs₁ : a ≤ s₁
s₂ : Finset ι
hs₂ : a ≤ s₂
this✝ : ∀ (i : ι), 0 ≤ ‖f i‖ ^ 2
this : ∑ i in s₁ \ s₂, ‖f i‖ ^ 2 + ∑ i in s₂ \ s₁, ‖f i‖ ^ 2 < sqrt ε ^ 2
hη : sqrt ε ^ 2 = ε
⊢ ∑ x in s₁ \ s₂, ‖f x‖ ^ 2 + ∑ x in s₂ \ s₁, ‖f x‖ ^ 2 < ε
case mp.intro
𝕜 : Type u_4
E : Type u_1
F : Type ?u.3720833
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_2
G : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst✝ : CompleteSpace E
f : (i : ι) → G i
hf :
  ∀ (ε : ℝ),
    ε > 0 →
      ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → ‖∑ b in m, ↑(V b) (f b) - ∑ b in n, ↑(V b) (f b)‖ < ε
ε : ℝ
hε : ε > 0
a : Finset ι
H : ∀ (m : Finset ι), a ≤ m → ∀ (n : Finset ι), a ≤ n → ‖∑ b in m, ↑(V b) (f b) - ∑ b in n, ↑(V b) (f b)‖ < sqrt ε
s₁ : Finset ι
hs₁ : a ≤ s₁
s₂ : Finset ι
hs₂ : a ≤ s₂
this✝ : ∀ (i : ι), 0 ≤ ‖f i‖ ^ 2
this : ∑ i in s₁ \ s₂, ‖f i‖ ^ 2 + ∑ i in s₂ \ s₁, ‖f i‖ ^ 2 < sqrt ε ^ 2
⊢ ∑ x in s₁ \ s₂, ‖f x‖ ^ 2 + ∑ x in s₂ \ s₁, ‖f x‖ ^ 2 < ε
have hη := sq_sqrt (le_of_lt hε)
no goals
case mp.intro
𝕜 : Type u_4
E : Type u_1
F : Type ?u.3720833
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_2
G : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst✝ : CompleteSpace E
f : (i : ι) → G i
hf :
  ∀ (ε : ℝ),
    ε > 0 →
      ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → ‖∑ b in m, ↑(V b) (f b) - ∑ b in n, ↑(V b) (f b)‖ < ε
ε : ℝ
hε : ε > 0
a : Finset ι
H : ∀ (m : Finset ι), a ≤ m → ∀ (n : Finset ι), a ≤ n → ‖∑ b in m, ↑(V b) (f b) - ∑ b in n, ↑(V b) (f b)‖ < sqrt ε
s₁ : Finset ι
hs₁ : a ≤ s₁
s₂ : Finset ι
hs₂ : a ≤ s₂
this✝ : ∀ (i : ι), 0 ≤ ‖f i‖ ^ 2
this : ∑ i in s₁ \ s₂, ‖f i‖ ^ 2 + ∑ i in s₂ \ s₁, ‖f i‖ ^ 2 < sqrt ε ^ 2
hη : sqrt ε ^ 2 = ε
⊢ ∑ x in s₁ \ s₂, ‖f x‖ ^ 2 + ∑ x in s₂ \ s₁, ‖f x‖ ^ 2 < ε
linarith
𝕜 : Type u_4
E : Type u_1
F : Type ?u.3720833
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_2
G : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst✝ : CompleteSpace E
f : (i : ι) → G i
hf :
  ∀ (ε : ℝ),
    ε > 0 →
      ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → ‖∑ b in m, ↑(V b) (f b) - ∑ b in n, ↑(V b) (f b)‖ < ε
ε : ℝ
hε : ε > 0
a : Finset ι
H : ∀ (m : Finset ι), a ≤ m → ∀ (n : Finset ι), a ≤ n → ‖∑ b in m, ↑(V b) (f b) - ∑ b in n, ↑(V b) (f b)‖ < sqrt ε
s₁ : Finset ι
hs₁ : a ≤ s₁
s₂ : Finset ι
hs₂ : a ≤ s₂
this : ∀ (i : ι), 0 ≤ ‖f i‖ ^ 2
⊢ ‖∑ i in s₁, ↑(V i) (f i) - ∑ i in s₂, ↑(V i) (f i)‖ < sqrt ε
𝕜 : Type u_4
E : Type u_1
F : Type ?u.3720833
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_2
G : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst✝ : CompleteSpace E
f : (i : ι) → G i
hf :
  ∀ (ε : ℝ),
    ε > 0 →
      ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → ‖∑ b in m, ↑(V b) (f b) - ∑ b in n, ↑(V b) (f b)‖ < ε
ε : ℝ
hε : ε > 0
a : Finset ι
H : ∀ (m : Finset ι), a ≤ m → ∀ (n : Finset ι), a ≤ n → ‖∑ b in m, ↑(V b) (f b) - ∑ b in n, ↑(V b) (f b)‖ < sqrt ε
s₁ : Finset ι
hs₁ : a ≤ s₁
s₂ : Finset ι
hs₂ : a ≤ s₂
this : ∀ (i : ι), 0 ≤ ‖f i‖ ^ 2
⊢ ∑ i in s₁ \ s₂, ‖f i‖ ^ 2 + ∑ i in s₂ \ s₁, ‖f i‖ ^ 2 < sqrt ε ^ 2
rw [← hV.norm_sq_diff_sum, sq_lt_sq, abs_of_nonneg (sqrt_nonneg _),
  abs_of_nonneg (norm_nonneg _)]
no goals
𝕜 : Type u_4
E : Type u_1
F : Type ?u.3720833
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_2
G : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst✝ : CompleteSpace E
f : (i : ι) → G i
hf :
  ∀ (ε : ℝ),
    ε > 0 →
      ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → ‖∑ b in m, ↑(V b) (f b) - ∑ b in n, ↑(V b) (f b)‖ < ε
ε : ℝ
hε : ε > 0
a : Finset ι
H : ∀ (m : Finset ι), a ≤ m → ∀ (n : Finset ι), a ≤ n → ‖∑ b in m, ↑(V b) (f b) - ∑ b in n, ↑(V b) (f b)‖ < sqrt ε
s₁ : Finset ι
hs₁ : a ≤ s₁
s₂ : Finset ι
hs₂ : a ≤ s₂
this : ∀ (i : ι), 0 ≤ ‖f i‖ ^ 2
⊢ ‖∑ i in s₁, ↑(V i) (f i) - ∑ i in s₂, ↑(V i) (f i)‖ < sqrt ε
exact H s₁ hs₁ s₂ hs₂
case mpr
𝕜 : Type u_4
E : Type u_1
F : Type ?u.3720833
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_2
G : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst✝ : CompleteSpace E
f : (i : ι) → G i
hf :
  ∀ (ε : ℝ),
    ε > 0 → ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε
ε : ℝ
hε : ε > 0
⊢ ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → ‖∑ b in m, ↑(V b) (f b) - ∑ b in n, ↑(V b) (f b)‖ < ε
case mpr
𝕜 : Type u_4
E : Type u_1
F : Type ?u.3720833
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_2
G : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst✝ : CompleteSpace E
f : (i : ι) → G i
⊢ (∀ (ε : ℝ),
      ε > 0 →
        ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε) →
    ∀ (ε : ℝ),
      ε > 0 →
        ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → ‖∑ b in m, ↑(V b) (f b) - ∑ b in n, ↑(V b) (f b)‖ < ε
intro hf ε hε
case mpr
𝕜 : Type u_4
E : Type u_1
F : Type ?u.3720833
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_2
G : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst✝ : CompleteSpace E
f : (i : ι) → G i
hf :
  ∀ (ε : ℝ),
    ε > 0 → ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε
ε : ℝ
hε : ε > 0
hε' : 0 < ε ^ 2 / 2
⊢ ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → ‖∑ b in m, ↑(V b) (f b) - ∑ b in n, ↑(V b) (f b)‖ < ε
case mpr
𝕜 : Type u_4
E : Type u_1
F : Type ?u.3720833
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_2
G : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst✝ : CompleteSpace E
f : (i : ι) → G i
hf :
  ∀ (ε : ℝ),
    ε > 0 → ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε
ε : ℝ
hε : ε > 0
⊢ ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → ‖∑ b in m, ↑(V b) (f b) - ∑ b in n, ↑(V b) (f b)‖ < ε
have hε' : 0 < ε ^ 2 / 2 := half_pos (sq_pos_of_pos hε)
case mpr.intro
𝕜 : Type u_4
E : Type u_1
F : Type ?u.3720833
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_2
G : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst✝ : CompleteSpace E
f : (i : ι) → G i
hf :
  ∀ (ε : ℝ),
    ε > 0 → ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε
ε : ℝ
hε : ε > 0
hε' : 0 < ε ^ 2 / 2
a : Finset ι
H : ∀ (m : Finset ι), a ≤ m → ∀ (n : Finset ι), a ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε ^ 2 / 2
⊢ ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → ‖∑ b in m, ↑(V b) (f b) - ∑ b in n, ↑(V b) (f b)‖ < ε
case mpr
𝕜 : Type u_4
E : Type u_1
F : Type ?u.3720833
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_2
G : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst✝ : CompleteSpace E
f : (i : ι) → G i
hf :
  ∀ (ε : ℝ),
    ε > 0 → ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε
ε : ℝ
hε : ε > 0
hε' : 0 < ε ^ 2 / 2
⊢ ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → ‖∑ b in m, ↑(V b) (f b) - ∑ b in n, ↑(V b) (f b)‖ < ε
obtain ⟨a, H⟩ := hf _ hε'
case mpr.intro
𝕜 : Type u_4
E : Type u_1
F : Type ?u.3720833
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_2
G : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst✝ : CompleteSpace E
f : (i : ι) → G i
hf :
  ∀ (ε : ℝ),
    ε > 0 → ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε
ε : ℝ
hε : ε > 0
hε' : 0 < ε ^ 2 / 2
a : Finset ι
H : ∀ (m : Finset ι), a ≤ m → ∀ (n : Finset ι), a ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε ^ 2 / 2
⊢ ∀ (m : Finset ι), a ≤ m → ∀ (n : Finset ι), a ≤ n → ‖∑ b in m, ↑(V b) (f b) - ∑ b in n, ↑(V b) (f b)‖ < ε
case mpr.intro
𝕜 : Type u_4
E : Type u_1
F : Type ?u.3720833
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_2
G : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst✝ : CompleteSpace E
f : (i : ι) → G i
hf :
  ∀ (ε : ℝ),
    ε > 0 → ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε
ε : ℝ
hε : ε > 0
hε' : 0 < ε ^ 2 / 2
a : Finset ι
H : ∀ (m : Finset ι), a ≤ m → ∀ (n : Finset ι), a ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε ^ 2 / 2
⊢ ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → ‖∑ b in m, ↑(V b) (f b) - ∑ b in n, ↑(V b) (f b)‖ < ε
use a
case mpr.intro
𝕜 : Type u_4
E : Type u_1
F : Type ?u.3720833
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_2
G : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst✝ : CompleteSpace E
f : (i : ι) → G i
hf :
  ∀ (ε : ℝ),
    ε > 0 → ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε
ε : ℝ
hε : ε > 0
hε' : 0 < ε ^ 2 / 2
a : Finset ι
H : ∀ (m : Finset ι), a ≤ m → ∀ (n : Finset ι), a ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε ^ 2 / 2
s₁ : Finset ι
hs₁ : a ≤ s₁
s₂ : Finset ι
hs₂ : a ≤ s₂
⊢ ‖∑ b in s₁, ↑(V b) (f b) - ∑ b in s₂, ↑(V b) (f b)‖ < ε
case mpr.intro
𝕜 : Type u_4
E : Type u_1
F : Type ?u.3720833
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_2
G : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst✝ : CompleteSpace E
f : (i : ι) → G i
hf :
  ∀ (ε : ℝ),
    ε > 0 → ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε
ε : ℝ
hε : ε > 0
hε' : 0 < ε ^ 2 / 2
a : Finset ι
H : ∀ (m : Finset ι), a ≤ m → ∀ (n : Finset ι), a ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε ^ 2 / 2
⊢ ∀ (m : Finset ι), a ≤ m → ∀ (n : Finset ι), a ≤ n → ‖∑ b in m, ↑(V b) (f b) - ∑ b in n, ↑(V b) (f b)‖ < ε
intro s₁ hs₁ s₂ hs₂
case mpr.intro
𝕜 : Type u_4
E : Type u_1
F : Type ?u.3720833
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_2
G : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst✝ : CompleteSpace E
f : (i : ι) → G i
hf :
  ∀ (ε : ℝ),
    ε > 0 → ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε
ε : ℝ
hε : ε > 0
hε' : 0 < ε ^ 2 / 2
a : Finset ι
H : ∀ (m : Finset ι), a ≤ m → ∀ (n : Finset ι), a ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε ^ 2 / 2
s₁ : Finset ι
hs₁ : a ≤ s₁
s₂ : Finset ι
hs₂ : a ≤ s₂
⊢ ‖∑ b in s₁, ↑(V b) (f b) - ∑ b in s₂, ↑(V b) (f b)‖ ^ 2 < ε ^ 2
case mpr.intro
𝕜 : Type u_4
E : Type u_1
F : Type ?u.3720833
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_2
G : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst✝ : CompleteSpace E
f : (i : ι) → G i
hf :
  ∀ (ε : ℝ),
    ε > 0 → ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε
ε : ℝ
hε : ε > 0
hε' : 0 < ε ^ 2 / 2
a : Finset ι
H : ∀ (m : Finset ι), a ≤ m → ∀ (n : Finset ι), a ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε ^ 2 / 2
s₁ : Finset ι
hs₁ : a ≤ s₁
s₂ : Finset ι
hs₂ : a ≤ s₂
⊢ ‖∑ b in s₁, ↑(V b) (f b) - ∑ b in s₂, ↑(V b) (f b)‖ < ε
refine' (abs_lt_of_sq_lt_sq' _ (le_of_lt hε)).2
case mpr.intro
𝕜 : Type u_4
E : Type u_1
F : Type ?u.3720833
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_2
G : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst✝ : CompleteSpace E
f : (i : ι) → G i
hf :
  ∀ (ε : ℝ),
    ε > 0 → ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε
ε : ℝ
hε : ε > 0
hε' : 0 < ε ^ 2 / 2
a : Finset ι
H : ∀ (m : Finset ι), a ≤ m → ∀ (n : Finset ι), a ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε ^ 2 / 2
s₁ : Finset ι
hs₁ : a ≤ s₁
s₂ : Finset ι
hs₂ : a ≤ s₂
has : a ≤ s₁ ⊓ s₂
⊢ ‖∑ b in s₁, ↑(V b) (f b) - ∑ b in s₂, ↑(V b) (f b)‖ ^ 2 < ε ^ 2
case mpr.intro
𝕜 : Type u_4
E : Type u_1
F : Type ?u.3720833
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_2
G : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst✝ : CompleteSpace E
f : (i : ι) → G i
hf :
  ∀ (ε : ℝ),
    ε > 0 → ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε
ε : ℝ
hε : ε > 0
hε' : 0 < ε ^ 2 / 2
a : Finset ι
H : ∀ (m : Finset ι), a ≤ m → ∀ (n : Finset ι), a ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε ^ 2 / 2
s₁ : Finset ι
hs₁ : a ≤ s₁
s₂ : Finset ι
hs₂ : a ≤ s₂
⊢ ‖∑ b in s₁, ↑(V b) (f b) - ∑ b in s₂, ↑(V b) (f b)‖ ^ 2 < ε ^ 2
have has : a ≤ s₁ ⊓ s₂ := le_inf hs₁ hs₂
case mpr.intro
𝕜 : Type u_4
E : Type u_1
F : Type ?u.3720833
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_2
G : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst✝ : CompleteSpace E
f : (i : ι) → G i
hf :
  ∀ (ε : ℝ),
    ε > 0 → ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε
ε : ℝ
hε : ε > 0
hε' : 0 < ε ^ 2 / 2
a : Finset ι
H : ∀ (m : Finset ι), a ≤ m → ∀ (n : Finset ι), a ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε ^ 2 / 2
s₁ : Finset ι
hs₁ : a ≤ s₁
s₂ : Finset ι
hs₂ : a ≤ s₂
has : a ≤ s₁ ⊓ s₂
⊢ ∑ i in s₁ \ s₂, ‖f i‖ ^ 2 + ∑ i in s₂ \ s₁, ‖f i‖ ^ 2 < ε ^ 2
case mpr.intro
𝕜 : Type u_4
E : Type u_1
F : Type ?u.3720833
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_2
G : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst✝ : CompleteSpace E
f : (i : ι) → G i
hf :
  ∀ (ε : ℝ),
    ε > 0 → ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε
ε : ℝ
hε : ε > 0
hε' : 0 < ε ^ 2 / 2
a : Finset ι
H : ∀ (m : Finset ι), a ≤ m → ∀ (n : Finset ι), a ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε ^ 2 / 2
s₁ : Finset ι
hs₁ : a ≤ s₁
s₂ : Finset ι
hs₂ : a ≤ s₂
has : a ≤ s₁ ⊓ s₂
⊢ ‖∑ b in s₁, ↑(V b) (f b) - ∑ b in s₂, ↑(V b) (f b)‖ ^ 2 < ε ^ 2
rw [hV.norm_sq_diff_sum]
no goals
case mpr.intro
𝕜 : Type u_4
E : Type u_1
F : Type ?u.3720833
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_2
G : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst✝ : CompleteSpace E
f : (i : ι) → G i
hf :
  ∀ (ε : ℝ),
    ε > 0 → ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε
ε : ℝ
hε : ε > 0
hε' : 0 < ε ^ 2 / 2
a : Finset ι
H : ∀ (m : Finset ι), a ≤ m → ∀ (n : Finset ι), a ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε ^ 2 / 2
s₁ : Finset ι
hs₁ : a ≤ s₁
s₂ : Finset ι
hs₂ : a ≤ s₂
has : a ≤ s₁ ⊓ s₂
Hs₁ : ∑ x in s₁ \ s₂, ‖f x‖ ^ 2 < ε ^ 2 / 2
Hs₂ : ∑ x in s₂ \ s₁, ‖f x‖ ^ 2 < ε ^ 2 / 2
⊢ ∑ i in s₁ \ s₂, ‖f i‖ ^ 2 + ∑ i in s₂ \ s₁, ‖f i‖ ^ 2 < ε ^ 2
linarith
case h.e'_3
𝕜 : Type u_4
E : Type u_1
F : Type ?u.3720833
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_2
G : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst✝ : CompleteSpace E
f : (i : ι) → G i
hf :
  ∀ (ε : ℝ),
    ε > 0 → ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε
ε : ℝ
hε : ε > 0
hε' : 0 < ε ^ 2 / 2
a : Finset ι
H : ∀ (m : Finset ι), a ≤ m → ∀ (n : Finset ι), a ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε ^ 2 / 2
s₁ : Finset ι
hs₁ : a ≤ s₁
s₂ : Finset ι
hs₂ : a ≤ s₂
has : a ≤ s₁ ⊓ s₂
⊢ ∑ x in s₁ \ s₂, ‖f x‖ ^ 2 = abs (∑ i in s₁, ‖f i‖ ^ 2 - ∑ i in s₁ ⊓ s₂, ‖f i‖ ^ 2)
𝕜 : Type u_4
E : Type u_1
F : Type ?u.3720833
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_2
G : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst✝ : CompleteSpace E
f : (i : ι) → G i
hf :
  ∀ (ε : ℝ),
    ε > 0 → ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε
ε : ℝ
hε : ε > 0
hε' : 0 < ε ^ 2 / 2
a : Finset ι
H : ∀ (m : Finset ι), a ≤ m → ∀ (n : Finset ι), a ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε ^ 2 / 2
s₁ : Finset ι
hs₁ : a ≤ s₁
s₂ : Finset ι
hs₂ : a ≤ s₂
has : a ≤ s₁ ⊓ s₂
⊢ ∑ x in s₁ \ s₂, ‖f x‖ ^ 2 < ε ^ 2 / 2
convert H _ hs₁ _ has
case h.e'_3
𝕜 : Type u_4
E : Type u_1
F : Type ?u.3720833
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_2
G : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst✝ : CompleteSpace E
f : (i : ι) → G i
hf :
  ∀ (ε : ℝ),
    ε > 0 → ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε
ε : ℝ
hε : ε > 0
hε' : 0 < ε ^ 2 / 2
a : Finset ι
H : ∀ (m : Finset ι), a ≤ m → ∀ (n : Finset ι), a ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε ^ 2 / 2
s₁ : Finset ι
hs₁ : a ≤ s₁
s₂ : Finset ι
hs₂ : a ≤ s₂
has : a ≤ s₁ ⊓ s₂
this : s₁ ⊓ s₂ ⊆ s₁
⊢ ∑ x in s₁ \ s₂, ‖f x‖ ^ 2 = abs (∑ i in s₁, ‖f i‖ ^ 2 - ∑ i in s₁ ⊓ s₂, ‖f i‖ ^ 2)
case h.e'_3
𝕜 : Type u_4
E : Type u_1
F : Type ?u.3720833
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_2
G : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst✝ : CompleteSpace E
f : (i : ι) → G i
hf :
  ∀ (ε : ℝ),
    ε > 0 → ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε
ε : ℝ
hε : ε > 0
hε' : 0 < ε ^ 2 / 2
a : Finset ι
H : ∀ (m : Finset ι), a ≤ m → ∀ (n : Finset ι), a ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε ^ 2 / 2
s₁ : Finset ι
hs₁ : a ≤ s₁
s₂ : Finset ι
hs₂ : a ≤ s₂
has : a ≤ s₁ ⊓ s₂
⊢ ∑ x in s₁ \ s₂, ‖f x‖ ^ 2 = abs (∑ i in s₁, ‖f i‖ ^ 2 - ∑ i in s₁ ⊓ s₂, ‖f i‖ ^ 2)
have : s₁ ⊓ s₂ ⊆ s₁ := Finset.inter_subset_left _ _
case h.e'_3
𝕜 : Type u_4
E : Type u_1
F : Type ?u.3720833
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_2
G : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst✝ : CompleteSpace E
f : (i : ι) → G i
hf :
  ∀ (ε : ℝ),
    ε > 0 → ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε
ε : ℝ
hε : ε > 0
hε' : 0 < ε ^ 2 / 2
a : Finset ι
H : ∀ (m : Finset ι), a ≤ m → ∀ (n : Finset ι), a ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε ^ 2 / 2
s₁ : Finset ι
hs₁ : a ≤ s₁
s₂ : Finset ι
hs₂ : a ≤ s₂
has : a ≤ s₁ ⊓ s₂
this : s₁ ⊓ s₂ ⊆ s₁
⊢ ∑ x in s₁ \ s₂, ‖f x‖ ^ 2 = ∑ i in s₁ \ (s₁ ⊓ s₂), ‖f i‖ ^ 2

case h.e'_3
𝕜 : Type u_4
E : Type u_1
F : Type ?u.3720833
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_2
G : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst✝ : CompleteSpace E
f : (i : ι) → G i
hf :
  ∀ (ε : ℝ),
    ε > 0 → ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε
ε : ℝ
hε : ε > 0
hε' : 0 < ε ^ 2 / 2
a : Finset ι
H : ∀ (m : Finset ι), a ≤ m → ∀ (n : Finset ι), a ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε ^ 2 / 2
s₁ : Finset ι
hs₁ : a ≤ s₁
s₂ : Finset ι
hs₂ : a ≤ s₂
has : a ≤ s₁ ⊓ s₂
this : s₁ ⊓ s₂ ⊆ s₁
⊢ ∀ (i : ι), 0 ≤ ‖f i‖ ^ 2
case h.e'_3
𝕜 : Type u_4
E : Type u_1
F : Type ?u.3720833
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_2
G : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst✝ : CompleteSpace E
f : (i : ι) → G i
hf :
  ∀ (ε : ℝ),
    ε > 0 → ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε
ε : ℝ
hε : ε > 0
hε' : 0 < ε ^ 2 / 2
a : Finset ι
H : ∀ (m : Finset ι), a ≤ m → ∀ (n : Finset ι), a ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε ^ 2 / 2
s₁ : Finset ι
hs₁ : a ≤ s₁
s₂ : Finset ι
hs₂ : a ≤ s₂
has : a ≤ s₁ ⊓ s₂
this : s₁ ⊓ s₂ ⊆ s₁
⊢ ∑ x in s₁ \ s₂, ‖f x‖ ^ 2 = abs (∑ i in s₁, ‖f i‖ ^ 2 - ∑ i in s₁ ⊓ s₂, ‖f i‖ ^ 2)
rw [← Finset.sum_sdiff this, add_tsub_cancel_right, Finset.abs_sum_of_nonneg']
no goals
case h.e'_3
𝕜 : Type u_4
E : Type u_1
F : Type ?u.3720833
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_2
G : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst✝ : CompleteSpace E
f : (i : ι) → G i
hf :
  ∀ (ε : ℝ),
    ε > 0 → ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε
ε : ℝ
hε : ε > 0
hε' : 0 < ε ^ 2 / 2
a : Finset ι
H : ∀ (m : Finset ι), a ≤ m → ∀ (n : Finset ι), a ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε ^ 2 / 2
s₁ : Finset ι
hs₁ : a ≤ s₁
s₂ : Finset ι
hs₂ : a ≤ s₂
has : a ≤ s₁ ⊓ s₂
this : s₁ ⊓ s₂ ⊆ s₁
⊢ ∑ x in s₁ \ s₂, ‖f x‖ ^ 2 = ∑ i in s₁ \ (s₁ ⊓ s₂), ‖f i‖ ^ 2
simp
no goals
case h.e'_3
𝕜 : Type u_4
E : Type u_1
F : Type ?u.3720833
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_2
G : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst✝ : CompleteSpace E
f : (i : ι) → G i
hf :
  ∀ (ε : ℝ),
    ε > 0 → ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε
ε : ℝ
hε : ε > 0
hε' : 0 < ε ^ 2 / 2
a : Finset ι
H : ∀ (m : Finset ι), a ≤ m → ∀ (n : Finset ι), a ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε ^ 2 / 2
s₁ : Finset ι
hs₁ : a ≤ s₁
s₂ : Finset ι
hs₂ : a ≤ s₂
has : a ≤ s₁ ⊓ s₂
this : s₁ ⊓ s₂ ⊆ s₁
⊢ ∀ (i : ι), 0 ≤ ‖f i‖ ^ 2
exact fun i => sq_nonneg _
case h.e'_3
𝕜 : Type u_4
E : Type u_1
F : Type ?u.3720833
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_2
G : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst✝ : CompleteSpace E
f : (i : ι) → G i
hf :
  ∀ (ε : ℝ),
    ε > 0 → ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε
ε : ℝ
hε : ε > 0
hε' : 0 < ε ^ 2 / 2
a : Finset ι
H : ∀ (m : Finset ι), a ≤ m → ∀ (n : Finset ι), a ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε ^ 2 / 2
s₁ : Finset ι
hs₁ : a ≤ s₁
s₂ : Finset ι
hs₂ : a ≤ s₂
has : a ≤ s₁ ⊓ s₂
Hs₁ : ∑ x in s₁ \ s₂, ‖f x‖ ^ 2 < ε ^ 2 / 2
⊢ ∑ x in s₂ \ s₁, ‖f x‖ ^ 2 = abs (∑ i in s₂, ‖f i‖ ^ 2 - ∑ i in s₁ ⊓ s₂, ‖f i‖ ^ 2)
𝕜 : Type u_4
E : Type u_1
F : Type ?u.3720833
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_2
G : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst✝ : CompleteSpace E
f : (i : ι) → G i
hf :
  ∀ (ε : ℝ),
    ε > 0 → ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε
ε : ℝ
hε : ε > 0
hε' : 0 < ε ^ 2 / 2
a : Finset ι
H : ∀ (m : Finset ι), a ≤ m → ∀ (n : Finset ι), a ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε ^ 2 / 2
s₁ : Finset ι
hs₁ : a ≤ s₁
s₂ : Finset ι
hs₂ : a ≤ s₂
has : a ≤ s₁ ⊓ s₂
Hs₁ : ∑ x in s₁ \ s₂, ‖f x‖ ^ 2 < ε ^ 2 / 2
⊢ ∑ x in s₂ \ s₁, ‖f x‖ ^ 2 < ε ^ 2 / 2
convert H _ hs₂ _ has
case h.e'_3
𝕜 : Type u_4
E : Type u_1
F : Type ?u.3720833
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_2
G : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst✝ : CompleteSpace E
f : (i : ι) → G i
hf :
  ∀ (ε : ℝ),
    ε > 0 → ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε
ε : ℝ
hε : ε > 0
hε' : 0 < ε ^ 2 / 2
a : Finset ι
H : ∀ (m : Finset ι), a ≤ m → ∀ (n : Finset ι), a ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε ^ 2 / 2
s₁ : Finset ι
hs₁ : a ≤ s₁
s₂ : Finset ι
hs₂ : a ≤ s₂
has : a ≤ s₁ ⊓ s₂
Hs₁ : ∑ x in s₁ \ s₂, ‖f x‖ ^ 2 < ε ^ 2 / 2
this : s₁ ⊓ s₂ ⊆ s₂
⊢ ∑ x in s₂ \ s₁, ‖f x‖ ^ 2 = abs (∑ i in s₂, ‖f i‖ ^ 2 - ∑ i in s₁ ⊓ s₂, ‖f i‖ ^ 2)
case h.e'_3
𝕜 : Type u_4
E : Type u_1
F : Type ?u.3720833
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_2
G : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst✝ : CompleteSpace E
f : (i : ι) → G i
hf :
  ∀ (ε : ℝ),
    ε > 0 → ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε
ε : ℝ
hε : ε > 0
hε' : 0 < ε ^ 2 / 2
a : Finset ι
H : ∀ (m : Finset ι), a ≤ m → ∀ (n : Finset ι), a ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε ^ 2 / 2
s₁ : Finset ι
hs₁ : a ≤ s₁
s₂ : Finset ι
hs₂ : a ≤ s₂
has : a ≤ s₁ ⊓ s₂
Hs₁ : ∑ x in s₁ \ s₂, ‖f x‖ ^ 2 < ε ^ 2 / 2
⊢ ∑ x in s₂ \ s₁, ‖f x‖ ^ 2 = abs (∑ i in s₂, ‖f i‖ ^ 2 - ∑ i in s₁ ⊓ s₂, ‖f i‖ ^ 2)
have : s₁ ⊓ s₂ ⊆ s₂ := Finset.inter_subset_right _ _
case h.e'_3
𝕜 : Type u_4
E : Type u_1
F : Type ?u.3720833
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_2
G : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst✝ : CompleteSpace E
f : (i : ι) → G i
hf :
  ∀ (ε : ℝ),
    ε > 0 → ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε
ε : ℝ
hε : ε > 0
hε' : 0 < ε ^ 2 / 2
a : Finset ι
H : ∀ (m : Finset ι), a ≤ m → ∀ (n : Finset ι), a ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε ^ 2 / 2
s₁ : Finset ι
hs₁ : a ≤ s₁
s₂ : Finset ι
hs₂ : a ≤ s₂
has : a ≤ s₁ ⊓ s₂
Hs₁ : ∑ x in s₁ \ s₂, ‖f x‖ ^ 2 < ε ^ 2 / 2
this : s₁ ⊓ s₂ ⊆ s₂
⊢ ∑ x in s₂ \ s₁, ‖f x‖ ^ 2 = ∑ i in s₂ \ (s₁ ⊓ s₂), ‖f i‖ ^ 2

case h.e'_3
𝕜 : Type u_4
E : Type u_1
F : Type ?u.3720833
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_2
G : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst✝ : CompleteSpace E
f : (i : ι) → G i
hf :
  ∀ (ε : ℝ),
    ε > 0 → ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε
ε : ℝ
hε : ε > 0
hε' : 0 < ε ^ 2 / 2
a : Finset ι
H : ∀ (m : Finset ι), a ≤ m → ∀ (n : Finset ι), a ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε ^ 2 / 2
s₁ : Finset ι
hs₁ : a ≤ s₁
s₂ : Finset ι
hs₂ : a ≤ s₂
has : a ≤ s₁ ⊓ s₂
Hs₁ : ∑ x in s₁ \ s₂, ‖f x‖ ^ 2 < ε ^ 2 / 2
this : s₁ ⊓ s₂ ⊆ s₂
⊢ ∀ (i : ι), 0 ≤ ‖f i‖ ^ 2
case h.e'_3
𝕜 : Type u_4
E : Type u_1
F : Type ?u.3720833
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_2
G : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst✝ : CompleteSpace E
f : (i : ι) → G i
hf :
  ∀ (ε : ℝ),
    ε > 0 → ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε
ε : ℝ
hε : ε > 0
hε' : 0 < ε ^ 2 / 2
a : Finset ι
H : ∀ (m : Finset ι), a ≤ m → ∀ (n : Finset ι), a ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε ^ 2 / 2
s₁ : Finset ι
hs₁ : a ≤ s₁
s₂ : Finset ι
hs₂ : a ≤ s₂
has : a ≤ s₁ ⊓ s₂
Hs₁ : ∑ x in s₁ \ s₂, ‖f x‖ ^ 2 < ε ^ 2 / 2
this : s₁ ⊓ s₂ ⊆ s₂
⊢ ∑ x in s₂ \ s₁, ‖f x‖ ^ 2 = abs (∑ i in s₂, ‖f i‖ ^ 2 - ∑ i in s₁ ⊓ s₂, ‖f i‖ ^ 2)
rw [← Finset.sum_sdiff this, add_tsub_cancel_right, Finset.abs_sum_of_nonneg']
no goals
case h.e'_3
𝕜 : Type u_4
E : Type u_1
F : Type ?u.3720833
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_2
G : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst✝ : CompleteSpace E
f : (i : ι) → G i
hf :
  ∀ (ε : ℝ),
    ε > 0 → ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε
ε : ℝ
hε : ε > 0
hε' : 0 < ε ^ 2 / 2
a : Finset ι
H : ∀ (m : Finset ι), a ≤ m → ∀ (n : Finset ι), a ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε ^ 2 / 2
s₁ : Finset ι
hs₁ : a ≤ s₁
s₂ : Finset ι
hs₂ : a ≤ s₂
has : a ≤ s₁ ⊓ s₂
Hs₁ : ∑ x in s₁ \ s₂, ‖f x‖ ^ 2 < ε ^ 2 / 2
this : s₁ ⊓ s₂ ⊆ s₂
⊢ ∑ x in s₂ \ s₁, ‖f x‖ ^ 2 = ∑ i in s₂ \ (s₁ ⊓ s₂), ‖f i‖ ^ 2
simp
no goals
case h.e'_3
𝕜 : Type u_4
E : Type u_1
F : Type ?u.3720833
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_2
G : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst✝ : CompleteSpace E
f : (i : ι) → G i
hf :
  ∀ (ε : ℝ),
    ε > 0 → ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε
ε : ℝ
hε : ε > 0
hε' : 0 < ε ^ 2 / 2
a : Finset ι
H : ∀ (m : Finset ι), a ≤ m → ∀ (n : Finset ι), a ≤ n → abs (∑ i in m, ‖f i‖ ^ 2 - ∑ i in n, ‖f i‖ ^ 2) < ε ^ 2 / 2
s₁ : Finset ι
hs₁ : a ≤ s₁
s₂ : Finset ι
hs₂ : a ≤ s₂
has : a ≤ s₁ ⊓ s₂
Hs₁ : ∑ x in s₁ \ s₂, ‖f x‖ ^ 2 < ε ^ 2 / 2
this : s₁ ⊓ s₂ ⊆ s₂
⊢ ∀ (i : ι), 0 ≤ ‖f i‖ ^ 2
exact fun i => sq_nonneg _