`BookProof.ChapterOrthogonalSums.norm_sum_sq_of_orthogonal` {ι : Type*} (t : Finset ι) {v : ι → E} (horth : ∀ x y, x ≠ y → ⟪v x, v y⟫_ℂ = 0) : ‖∑ x ∈ t, v x‖ ^ 2 = ∑...
ProvedBookProof.ChapterOrthogonalSums.norm_sum_sq_of_orthogonaltheoremstimepiece
Prove the following Lean 4 theorem from ChapterOrthogonalSums.
BookProof.ChapterOrthogonalSums.norm_sum_sq_of_orthogonal {ι : Type*} (t : Finset ι) {v : ι → E} (horth : ∀ x y, x ≠ y → ⟪v x, v y⟫_ℂ = 0) : ‖∑ x ∈ t, v x‖ ^ 2 = ∑ x ∈ t, ‖v x‖ ^ 2
Formalization note: Lean 4 identifier BookProof.ChapterOrthogonalSums.norm_sum_sq_of_orthogonal.
Preamble
-- Generated from ChapterOrthogonalSums.lean — theorem BookProof.ChapterOrthogonalSums.norm_sum_sq_of_orthogonal
import Mathlib
import Definitions.Def_ChapterOrthogonalSums
open BookProof.ChapterOrthogonalSums
open scoped InnerProductSpace
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℂ E]Formal statement
theorem BookProof.ChapterOrthogonalSums.norm_sum_sq_of_orthogonal {ι : Type*} (t : Finset ι) {v : ι → E}
(horth : ∀ x y, x ≠ y → ⟪v x, v y⟫_ℂ = 0) :
‖∑ x ∈ t, v x‖ ^ 2 = ∑ x ∈ t, ‖v x‖ ^ 2 := by sorry