Prove2Me

`BookProof.ChapterG2.commuting_normal_operators_simultaneously_diagonalizable` {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {ι : Type*} [Finit

Proved
BookProof.ChapterG2.commuting_normal_operators_simultaneously_diagonalizable

by leonardopedro · Oct 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

theoremstimepiece

Prove the following Lean 4 theorem from ChapterG2.

BookProof.ChapterG2.commuting_normal_operators_simultaneously_diagonalizable {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {ι : Type*} [Finite ι] (T : ι → H →ₗ[ℂ] H) (h_symm : ∀ i, (T i).IsSymmetric) (h_comm : ∀ i j, i ≠ j → Commute (T i) (T j)) : ⨆ (χ : ι → ℂ), ⨅ i, Module.End.eigenspace (T i) (χ i) = ⊤

Formalization note: Lean 4 identifier BookProof.ChapterG2.commuting_normal_operators_simultaneously_diagonalizable.

Preamble
-- Generated from ChapterG2.lean — theorem BookProof.ChapterG2.commuting_normal_operators_simultaneously_diagonalizable
import Mathlib
import Definitions.Def_ChapterG2
open BookProof.ChapterG2


open MeasureTheory ProbabilityTheory
open scoped ProbabilityTheory

variable {Ω : Type*} [MeasurableSpace Ω]
variable {A : Type*} [CommRing A] (Q : A)
variable {G : Type*} [Group G] [MeasurableSpace G]
variable {μG : Measure G} [IsProbabilityMeasure μG] [μG.IsMulLeftInvariant]
variable {X : Type*} [MulAction G X]
Formal statement
theorem BookProof.ChapterG2.commuting_normal_operators_simultaneously_diagonalizable
    {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H]
    {ι : Type*} [Finite ι]
    (T : ι → H →ₗ[ℂ] H) (h_symm : ∀ i, (T i).IsSymmetric)
    (h_comm : ∀ i j, i ≠ j → Commute (T i) (T j)) :
    ⨆ (χ : ι → ℂ), ⨅ i, Module.End.eigenspace (T i) (χ i) = ⊤ := by sorry

View graph