𝕜 : Type u_2
E : Type u_3
F : Type ?u.3426813
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_1
x : E
v : ι → E
s : Finset ι
hv : Orthonormal 𝕜 v
h₂ : ∑ i in s, ∑ j in s, inner (v i) x * inner x (v j) * inner (v j) (v i) = ∑ k in s, inner (v k) x * inner x (v k)
⊢ ∑ i in s, ‖inner (v i) x‖ ^ 2 ≤ ‖x‖ ^ 2
𝕜 : Type u_2
E : Type u_3
F : Type ?u.3426813
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_1
x : E
v : ι → E
s : Finset ι
hv : Orthonormal 𝕜 v
⊢ ∑ i in s, ‖inner (v i) x‖ ^ 2 ≤ ‖x‖ ^ 2
have h₂ :
  (∑ i in s, ∑ j in s, ⟪v i, x⟫ * ⟪x, v j⟫ * ⟪v j, v i⟫) = (∑ k in s, ⟪v k, x⟫ * ⟪x, v k⟫ : 𝕜) :=
  by classical exact hv.inner_left_right_finset
𝕜 : Type u_2
E : Type u_3
F : Type ?u.3426813
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_1
x : E
v : ι → E
s : Finset ι
hv : Orthonormal 𝕜 v
h₂ : ∑ i in s, ∑ j in s, inner (v i) x * inner x (v j) * inner (v j) (v i) = ∑ k in s, inner (v k) x * inner x (v k)
h₃ : ∀ (z : 𝕜), ↑re (z * ↑(starRingEnd 𝕜) z) = ‖z‖ ^ 2
⊢ ∑ i in s, ‖inner (v i) x‖ ^ 2 ≤ ‖x‖ ^ 2
𝕜 : Type u_2
E : Type u_3
F : Type ?u.3426813
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_1
x : E
v : ι → E
s : Finset ι
hv : Orthonormal 𝕜 v
h₂ : ∑ i in s, ∑ j in s, inner (v i) x * inner x (v j) * inner (v j) (v i) = ∑ k in s, inner (v k) x * inner x (v k)
⊢ ∑ i in s, ‖inner (v i) x‖ ^ 2 ≤ ‖x‖ ^ 2
have h₃ : ∀ z : 𝕜, re (z * conj z) = ‖z‖ ^ 2 := by
  intro z
  simp only [mul_conj, normSq_eq_def']
  norm_cast
𝕜 : Type u_2
E : Type u_3
F : Type ?u.3426813
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_1
x : E
v : ι → E
s : Finset ι
hv : Orthonormal 𝕜 v
h₂ : ∑ i in s, ∑ j in s, inner (v i) x * inner x (v j) * inner (v j) (v i) = ∑ k in s, inner (v k) x * inner x (v k)
h₃ : ∀ (z : 𝕜), ↑re (z * ↑(starRingEnd 𝕜) z) = ‖z‖ ^ 2
hbf : ‖x - ∑ i in s, inner (v i) x • v i‖ ^ 2 = ‖x‖ ^ 2 - ∑ i in s, ‖inner (v i) x‖ ^ 2
⊢ ∑ i in s, ‖inner (v i) x‖ ^ 2 ≤ ‖x‖ ^ 2

case hbf
𝕜 : Type u_2
E : Type u_3
F : Type ?u.3426813
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_1
x : E
v : ι → E
s : Finset ι
hv : Orthonormal 𝕜 v
h₂ : ∑ i in s, ∑ j in s, inner (v i) x * inner x (v j) * inner (v j) (v i) = ∑ k in s, inner (v k) x * inner x (v k)
h₃ : ∀ (z : 𝕜), ↑re (z * ↑(starRingEnd 𝕜) z) = ‖z‖ ^ 2
⊢ ‖x - ∑ i in s, inner (v i) x • v i‖ ^ 2 = ‖x‖ ^ 2 - ∑ i in s, ‖inner (v i) x‖ ^ 2
𝕜 : Type u_2
E : Type u_3
F : Type ?u.3426813
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_1
x : E
v : ι → E
s : Finset ι
hv : Orthonormal 𝕜 v
h₂ : ∑ i in s, ∑ j in s, inner (v i) x * inner x (v j) * inner (v j) (v i) = ∑ k in s, inner (v k) x * inner x (v k)
h₃ : ∀ (z : 𝕜), ↑re (z * ↑(starRingEnd 𝕜) z) = ‖z‖ ^ 2
⊢ ∑ i in s, ‖inner (v i) x‖ ^ 2 ≤ ‖x‖ ^ 2
suffices hbf : ‖x - ∑ i in s, ⟪v i, x⟫ • v i‖ ^ 2 = ‖x‖ ^ 2 - ∑ i in s, ‖⟪v i, x⟫‖ ^ 2
case hbf
𝕜 : Type u_2
E : Type u_3
F : Type ?u.3426813
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_1
x : E
v : ι → E
s : Finset ι
hv : Orthonormal 𝕜 v
h₂ : ∑ i in s, ∑ j in s, inner (v i) x * inner x (v j) * inner (v j) (v i) = ∑ k in s, inner (v k) x * inner x (v k)
h₃ : ∀ (z : 𝕜), ↑re (z * ↑(starRingEnd 𝕜) z) = ‖z‖ ^ 2
⊢ ‖x‖ ^ 2 - (2 * ↑re (inner x (∑ i in s, inner (v i) x • v i)) - ‖∑ i in s, inner (v i) x • v i‖ ^ 2) =
    ‖x‖ ^ 2 - ∑ i in s, ‖inner (v i) x‖ ^ 2
case hbf
𝕜 : Type u_2
E : Type u_3
F : Type ?u.3426813
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_1
x : E
v : ι → E
s : Finset ι
hv : Orthonormal 𝕜 v
h₂ : ∑ i in s, ∑ j in s, inner (v i) x * inner x (v j) * inner (v j) (v i) = ∑ k in s, inner (v k) x * inner x (v k)
h₃ : ∀ (z : 𝕜), ↑re (z * ↑(starRingEnd 𝕜) z) = ‖z‖ ^ 2
⊢ ‖x - ∑ i in s, inner (v i) x • v i‖ ^ 2 = ‖x‖ ^ 2 - ∑ i in s, ‖inner (v i) x‖ ^ 2
rw [@norm_sub_sq 𝕜, sub_add]
no goals
case hbf
𝕜 : Type u_2
E : Type u_3
F : Type ?u.3426813
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_1
x : E
v : ι → E
s : Finset ι
hv : Orthonormal 𝕜 v
h₂ : ∑ i in s, ∑ j in s, inner (v i) x * inner x (v j) * inner (v j) (v i) = ∑ k in s, inner (v k) x * inner x (v k)
h₃ : ∀ (z : 𝕜), ↑re (z * ↑(starRingEnd 𝕜) z) = ‖z‖ ^ 2
⊢ ‖x‖ ^ 2 - (2 * ↑re (inner x (∑ i in s, inner (v i) x • v i)) - ‖∑ i in s, inner (v i) x • v i‖ ^ 2) =
    ‖x‖ ^ 2 - ∑ i in s, ‖inner (v i) x‖ ^ 2
classical
  simp only [@InnerProductSpace.norm_sq_eq_inner 𝕜, _root_.inner_sum, _root_.sum_inner]
  simp only [inner_smul_right, two_mul, inner_smul_left, inner_conj_symm, ←mul_assoc, h₂,
    add_sub_cancel, sub_right_inj]
  simp only [map_sum, ← inner_conj_symm x, ← h₃]
no goals
𝕜 : Type u_2
E : Type u_3
F : Type ?u.3426813
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_1
x : E
v : ι → E
s : Finset ι
hv : Orthonormal 𝕜 v
⊢ ∑ i in s, ∑ j in s, inner (v i) x * inner x (v j) * inner (v j) (v i) = ∑ k in s, inner (v k) x * inner x (v k)
classical exact hv.inner_left_right_finset
no goals
𝕜 : Type u_2
E : Type u_3
F : Type ?u.3426813
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_1
x : E
v : ι → E
s : Finset ι
hv : Orthonormal 𝕜 v
⊢ ∑ i in s, ∑ j in s, inner (v i) x * inner x (v j) * inner (v j) (v i) = ∑ k in s, inner (v k) x * inner x (v k)
exact hv.inner_left_right_finset
𝕜 : Type u_2
E : Type u_3
F : Type ?u.3426813
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_1
x : E
v : ι → E
s : Finset ι
hv : Orthonormal 𝕜 v
h₂ : ∑ i in s, ∑ j in s, inner (v i) x * inner x (v j) * inner (v j) (v i) = ∑ k in s, inner (v k) x * inner x (v k)
z : 𝕜
⊢ ↑re (z * ↑(starRingEnd 𝕜) z) = ‖z‖ ^ 2
𝕜 : Type u_2
E : Type u_3
F : Type ?u.3426813
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_1
x : E
v : ι → E
s : Finset ι
hv : Orthonormal 𝕜 v
h₂ : ∑ i in s, ∑ j in s, inner (v i) x * inner x (v j) * inner (v j) (v i) = ∑ k in s, inner (v k) x * inner x (v k)
⊢ ∀ (z : 𝕜), ↑re (z * ↑(starRingEnd 𝕜) z) = ‖z‖ ^ 2
intro z
𝕜 : Type u_2
E : Type u_3
F : Type ?u.3426813
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_1
x : E
v : ι → E
s : Finset ι
hv : Orthonormal 𝕜 v
h₂ : ∑ i in s, ∑ j in s, inner (v i) x * inner x (v j) * inner (v j) (v i) = ∑ k in s, inner (v k) x * inner x (v k)
z : 𝕜
⊢ ↑re ↑(‖z‖ ^ 2) = ‖z‖ ^ 2
𝕜 : Type u_2
E : Type u_3
F : Type ?u.3426813
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_1
x : E
v : ι → E
s : Finset ι
hv : Orthonormal 𝕜 v
h₂ : ∑ i in s, ∑ j in s, inner (v i) x * inner x (v j) * inner (v j) (v i) = ∑ k in s, inner (v k) x * inner x (v k)
z : 𝕜
⊢ ↑re (z * ↑(starRingEnd 𝕜) z) = ‖z‖ ^ 2
simp only [mul_conj, normSq_eq_def']
no goals
𝕜 : Type u_2
E : Type u_3
F : Type ?u.3426813
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_1
x : E
v : ι → E
s : Finset ι
hv : Orthonormal 𝕜 v
h₂ : ∑ i in s, ∑ j in s, inner (v i) x * inner x (v j) * inner (v j) (v i) = ∑ k in s, inner (v k) x * inner x (v k)
z : 𝕜
⊢ ↑re ↑(‖z‖ ^ 2) = ‖z‖ ^ 2
norm_cast
𝕜 : Type u_2
E : Type u_3
F : Type ?u.3426813
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_1
x : E
v : ι → E
s : Finset ι
hv : Orthonormal 𝕜 v
h₂ : ∑ i in s, ∑ j in s, inner (v i) x * inner x (v j) * inner (v j) (v i) = ∑ k in s, inner (v k) x * inner x (v k)
h₃ : ∀ (z : 𝕜), ↑re (z * ↑(starRingEnd 𝕜) z) = ‖z‖ ^ 2
hbf : ‖x - ∑ i in s, inner (v i) x • v i‖ ^ 2 = ‖x‖ ^ 2 - ∑ i in s, ‖inner (v i) x‖ ^ 2
⊢ 0 ≤ ‖x - ∑ i in s, inner (v i) x • v i‖ ^ 2
𝕜 : Type u_2
E : Type u_3
F : Type ?u.3426813
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_1
x : E
v : ι → E
s : Finset ι
hv : Orthonormal 𝕜 v
h₂ : ∑ i in s, ∑ j in s, inner (v i) x * inner x (v j) * inner (v j) (v i) = ∑ k in s, inner (v k) x * inner x (v k)
h₃ : ∀ (z : 𝕜), ↑re (z * ↑(starRingEnd 𝕜) z) = ‖z‖ ^ 2
hbf : ‖x - ∑ i in s, inner (v i) x • v i‖ ^ 2 = ‖x‖ ^ 2 - ∑ i in s, ‖inner (v i) x‖ ^ 2
⊢ ∑ i in s, ‖inner (v i) x‖ ^ 2 ≤ ‖x‖ ^ 2
rw [← sub_nonneg, ← hbf]
no goals
𝕜 : Type u_2
E : Type u_3
F : Type ?u.3426813
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_1
x : E
v : ι → E
s : Finset ι
hv : Orthonormal 𝕜 v
h₂ : ∑ i in s, ∑ j in s, inner (v i) x * inner x (v j) * inner (v j) (v i) = ∑ k in s, inner (v k) x * inner x (v k)
h₃ : ∀ (z : 𝕜), ↑re (z * ↑(starRingEnd 𝕜) z) = ‖z‖ ^ 2
hbf : ‖x - ∑ i in s, inner (v i) x • v i‖ ^ 2 = ‖x‖ ^ 2 - ∑ i in s, ‖inner (v i) x‖ ^ 2
⊢ 0 ≤ ‖x - ∑ i in s, inner (v i) x • v i‖ ^ 2
simp only [norm_nonneg, pow_nonneg]
case hbf
𝕜 : Type u_2
E : Type u_3
F : Type ?u.3426813
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_1
x : E
v : ι → E
s : Finset ι
hv : Orthonormal 𝕜 v
h₂ : ∑ i in s, ∑ j in s, inner (v i) x * inner x (v j) * inner (v j) (v i) = ∑ k in s, inner (v k) x * inner x (v k)
h₃ : ∀ (z : 𝕜), ↑re (z * ↑(starRingEnd 𝕜) z) = ‖z‖ ^ 2
⊢ ↑re (inner x x) -
      (2 * ↑re (∑ i in s, inner x (inner (v i) x • v i)) -
        ↑re (∑ x_1 in s, ∑ i in s, inner (inner (v i) x • v i) (inner (v x_1) x • v x_1))) =
    ↑re (inner x x) - ∑ i in s, ‖inner (v i) x‖ ^ 2
case hbf
𝕜 : Type u_2
E : Type u_3
F : Type ?u.3426813
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_1
x : E
v : ι → E
s : Finset ι
hv : Orthonormal 𝕜 v
h₂ : ∑ i in s, ∑ j in s, inner (v i) x * inner x (v j) * inner (v j) (v i) = ∑ k in s, inner (v k) x * inner x (v k)
h₃ : ∀ (z : 𝕜), ↑re (z * ↑(starRingEnd 𝕜) z) = ‖z‖ ^ 2
⊢ ‖x‖ ^ 2 - (2 * ↑re (inner x (∑ i in s, inner (v i) x • v i)) - ‖∑ i in s, inner (v i) x • v i‖ ^ 2) =
    ‖x‖ ^ 2 - ∑ i in s, ‖inner (v i) x‖ ^ 2
simp only [@InnerProductSpace.norm_sq_eq_inner 𝕜, _root_.inner_sum, _root_.sum_inner]
case hbf
𝕜 : Type u_2
E : Type u_3
F : Type ?u.3426813
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_1
x : E
v : ι → E
s : Finset ι
hv : Orthonormal 𝕜 v
h₂ : ∑ i in s, ∑ j in s, inner (v i) x * inner x (v j) * inner (v j) (v i) = ∑ k in s, inner (v k) x * inner x (v k)
h₃ : ∀ (z : 𝕜), ↑re (z * ↑(starRingEnd 𝕜) z) = ‖z‖ ^ 2
⊢ ↑re (∑ x_1 in s, inner (v x_1) x * inner x (v x_1)) = ∑ i in s, ‖inner (v i) x‖ ^ 2
case hbf
𝕜 : Type u_2
E : Type u_3
F : Type ?u.3426813
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_1
x : E
v : ι → E
s : Finset ι
hv : Orthonormal 𝕜 v
h₂ : ∑ i in s, ∑ j in s, inner (v i) x * inner x (v j) * inner (v j) (v i) = ∑ k in s, inner (v k) x * inner x (v k)
h₃ : ∀ (z : 𝕜), ↑re (z * ↑(starRingEnd 𝕜) z) = ‖z‖ ^ 2
⊢ ↑re (inner x x) -
      (2 * ↑re (∑ i in s, inner x (inner (v i) x • v i)) -
        ↑re (∑ x_1 in s, ∑ i in s, inner (inner (v i) x • v i) (inner (v x_1) x • v x_1))) =
    ↑re (inner x x) - ∑ i in s, ‖inner (v i) x‖ ^ 2
simp only [inner_smul_right, two_mul, inner_smul_left, inner_conj_symm, ←mul_assoc, h₂,
  add_sub_cancel, sub_right_inj]
no goals
case hbf
𝕜 : Type u_2
E : Type u_3
F : Type ?u.3426813
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_1
x : E
v : ι → E
s : Finset ι
hv : Orthonormal 𝕜 v
h₂ : ∑ i in s, ∑ j in s, inner (v i) x * inner x (v j) * inner (v j) (v i) = ∑ k in s, inner (v k) x * inner x (v k)
h₃ : ∀ (z : 𝕜), ↑re (z * ↑(starRingEnd 𝕜) z) = ‖z‖ ^ 2
⊢ ↑re (∑ x_1 in s, inner (v x_1) x * inner x (v x_1)) = ∑ i in s, ‖inner (v i) x‖ ^ 2
simp only [map_sum, ← inner_conj_symm x, ← h₃]