𝕜 : Type u_1
E : Type u_2
F : Type ?u.3502141
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
x : E
v : ι → E
hv : Orthonormal 𝕜 v
⊢ HasSum (fun i => ‖inner (v i) x‖ ^ 2) (⨆ (s : Finset ι), ∑ i in s, ‖inner (v i) x‖ ^ 2)
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3502141
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
x : E
v : ι → E
hv : Orthonormal 𝕜 v
⊢ Summable fun i => ‖inner (v i) x‖ ^ 2
use ⨆ s : Finset ι, ∑ i in s, ‖⟪v i, x⟫‖ ^ 2
case h
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3502141
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
x : E
v : ι → E
hv : Orthonormal 𝕜 v
⊢ ∀ (i : ι), 0 ≤ ‖inner (v i) x‖ ^ 2

case hf
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3502141
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
x : E
v : ι → E
hv : Orthonormal 𝕜 v
⊢ IsLUB (Set.range fun s => ∑ i in s, ‖inner (v i) x‖ ^ 2) (⨆ (s : Finset ι), ∑ i in s, ‖inner (v i) x‖ ^ 2)
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3502141
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
x : E
v : ι → E
hv : Orthonormal 𝕜 v
⊢ HasSum (fun i => ‖inner (v i) x‖ ^ 2) (⨆ (s : Finset ι), ∑ i in s, ‖inner (v i) x‖ ^ 2)
apply hasSum_of_isLUB_of_nonneg
case h
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3502141
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
x : E
v : ι → E
hv : Orthonormal 𝕜 v
b : ι
⊢ 0 ≤ ‖inner (v b) x‖ ^ 2
case h
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3502141
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
x : E
v : ι → E
hv : Orthonormal 𝕜 v
⊢ ∀ (i : ι), 0 ≤ ‖inner (v i) x‖ ^ 2
intro b
no goals
case h
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3502141
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
x : E
v : ι → E
hv : Orthonormal 𝕜 v
b : ι
⊢ 0 ≤ ‖inner (v b) x‖ ^ 2
simp only [norm_nonneg, pow_nonneg]
case hf
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3502141
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
x : E
v : ι → E
hv : Orthonormal 𝕜 v
⊢ BddAbove (Set.range fun s => ∑ i in s, ‖inner (v i) x‖ ^ 2)
case hf
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3502141
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
x : E
v : ι → E
hv : Orthonormal 𝕜 v
⊢ IsLUB (Set.range fun s => ∑ i in s, ‖inner (v i) x‖ ^ 2) (⨆ (s : Finset ι), ∑ i in s, ‖inner (v i) x‖ ^ 2)
refine' isLUB_ciSup _
case hf
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3502141
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
x : E
v : ι → E
hv : Orthonormal 𝕜 v
⊢ ‖x‖ ^ 2 ∈ upperBounds (Set.range fun s => ∑ i in s, ‖inner (v i) x‖ ^ 2)
case hf
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3502141
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
x : E
v : ι → E
hv : Orthonormal 𝕜 v
⊢ BddAbove (Set.range fun s => ∑ i in s, ‖inner (v i) x‖ ^ 2)
use ‖x‖ ^ 2
case hf.intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3502141
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
x : E
v : ι → E
hv : Orthonormal 𝕜 v
s : Finset ι
⊢ (fun s => ∑ i in s, ‖inner (v i) x‖ ^ 2) s ≤ ‖x‖ ^ 2
case hf
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3502141
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
x : E
v : ι → E
hv : Orthonormal 𝕜 v
⊢ ‖x‖ ^ 2 ∈ upperBounds (Set.range fun s => ∑ i in s, ‖inner (v i) x‖ ^ 2)
rintro y ⟨s, rfl⟩
no goals
case hf.intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3502141
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
x : E
v : ι → E
hv : Orthonormal 𝕜 v
s : Finset ι
⊢ (fun s => ∑ i in s, ‖inner (v i) x‖ ^ 2) s ≤ ‖x‖ ^ 2
exact hv.sum_inner_products_le x