𝕜 : Type u_1
E : Type u_2
F : Type ?u.3500272
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
⊢ 0 ≤ ‖x‖ ^ 2
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3500272
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 : ι), ‖inner (v i) x‖ ^ 2) ≤ ‖x‖ ^ 2
refine' tsum_le_of_sum_le' _ fun s => hv.sum_inner_products_le x
no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3500272
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
⊢ 0 ≤ ‖x‖ ^ 2
simp only [norm_nonneg, pow_nonneg]