`BookProof.ChapterMackeyImprimitivity.sum_norm_sq_of_orthogonal` {f : X → E} {ψ : E} (hsum : ∑ x, f x = ψ) (horth : ∀ x y, x ≠ y → ⟪f x, f y⟫_ℂ = 0) : ∑ x : X, ‖f x‖ ^ 2...
ProvedBookProof.ChapterMackeyImprimitivity.sum_norm_sq_of_orthogonaltheoremstimepiece
Prove the following Lean 4 theorem from ChapterMackeyImprimitivity.
BookProof.ChapterMackeyImprimitivity.sum_norm_sq_of_orthogonal {f : X → E} {ψ : E} (hsum : ∑ x, f x = ψ) (horth : ∀ x y, x ≠ y → ⟪f x, f y⟫_ℂ = 0) : ∑ x : X, ‖f x‖ ^ 2 = ‖ψ‖ ^ 2
Formalization note: Lean 4 identifier BookProof.ChapterMackeyImprimitivity.sum_norm_sq_of_orthogonal.
Preamble
-- Generated from ChapterMackeyImprimitivity.lean — theorem BookProof.ChapterMackeyImprimitivity.sum_norm_sq_of_orthogonal
import Mathlib
import Definitions.Def_ChapterMackeyImprimitivity
open BookProof.ChapterMackeyImprimitivity
open scoped InnerProductSpace
open Finset
variable {G : Type*} [Group G] {X : Type*} [Fintype X] [MulAction G X]
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℂ E]Formal statement
theorem BookProof.ChapterMackeyImprimitivity.sum_norm_sq_of_orthogonal {f : X → E} {ψ : E} (hsum : ∑ x, f x = ψ)
(horth : ∀ x y, x ≠ y → ⟪f x, f y⟫_ℂ = 0) :
∑ x : X, ‖f x‖ ^ 2 = ‖ψ‖ ^ 2 := by sorry