`BookProof.ChapterGaugeCasimirAverage.inner_casimir` (T : ι → V →ₗ[ℂ] V) (hT : ∀ a, (T a).IsSymmetric) (v : V) : ⟪v, casimir T v⟫_ℂ = ((∑ a, ‖T a v‖ ^ 2 : ℝ) : ℂ)
ProvedBookProof.ChapterGaugeCasimirAverage.inner_casimirtheoremstimepiece
Prove the following Lean 4 theorem from ChapterGaugeCasimirAverage.
BookProof.ChapterGaugeCasimirAverage.inner_casimir (T : ι → V →ₗ[ℂ] V) (hT : ∀ a, (T a).IsSymmetric) (v : V) : ⟪v, casimir T v⟫_ℂ = ((∑ a, ‖T a v‖ ^ 2 : ℝ) : ℂ)
Formalization note: Lean 4 identifier BookProof.ChapterGaugeCasimirAverage.inner_casimir.
Preamble
-- Generated from ChapterGaugeCasimirAverage.lean — theorem BookProof.ChapterGaugeCasimirAverage.inner_casimir
import Definitions.Def_ChapterGaugeIncompleteFixing
import Mathlib
import Definitions.Def_ChapterGaugeCasimirAverage
open BookProof.ChapterGaugeCasimirAverage
open BookProof.ChapterGaugeIncompleteFixing
open MeasureTheory
open scoped InnerProductSpace
variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℂ V]
variable {ι : Type*} [Fintype ι]Formal statement
theorem BookProof.ChapterGaugeCasimirAverage.inner_casimir (T : ι → V →ₗ[ℂ] V) (hT : ∀ a, (T a).IsSymmetric) (v : V) :
⟪v, casimir T v⟫_ℂ = ((∑ a, ‖T a v‖ ^ 2 : ℝ) : ℂ) := by sorry