Chapter SpectralCommutant

import Definitions.Def_ChapterSpectralMultiplication
import Definitions.Def_ChapterLinftyMaximalAbelian
import Definitions.Def_ChapterAbelianGelfandModel
import Definitions.Def_ChapterLinftyMultiplication
import Mathlib
import Theorems.Thm_BookProof_ChapterLinftyMultiplication_multOp_comm
import Theorems.Thm_BookProof_ChapterLinftyMaximalAbelian_memLp_top_symbol
import Theorems.Thm_BookProof_ChapterLinftyMaximalAbelian_commutant_eq_multOp
import Theorems.Thm_BookProof_ChapterLinftyMaximalAbelian_oneLp_coeFn
import Theorems.Thm_BookProof_ChapterLinftyMaximalAbelian_symbol_ae_eq
import Theorems.Thm_BookProof_ChapterLinftyMaximalAbelian_stronglyMeasurable_symbol


/-!
# The commutant of a singly generated abelian algebra (plan GAP-2, the von Neumann level)

`ChapterSpectralMultiplication` identifies a normal operator with a cyclic unit
vector with multiplication by the coordinate function on `L²(μ)`.  That is the
**C\*-level** model: it identifies the algebra of *continuous* functions of `T`.

This module upgrades the identification to the **von Neumann level** in the same
(cyclic) situation, by computing the *commutant*.  Two ingredients:

* a strengthening of `ChapterLinftyMaximalAbelian.commutant_eq_multOp`: on a compact
  space with a finite regular Borel measure it is enough to commute with the
  multiplication operators whose symbol is **continuous**
  (`contCommutant_eq_multOp`) — the essential bound on the symbol is obtained by
  truncating and testing against continuous functions, which are dense in `L²`;
* the transport of that statement through the spectral unitary
  (`commutant_eq_conj_multOp`).

The consequences are the von Neumann statements in the cyclic case:

* `centralizer_cfcSet` — the commutant of `{f(T) : f ∈ C(σ(T))}` is *exactly* the
  unitary copy of the multiplication algebra `L∞(μ)`;
* `centralizer_multModel` and `bicommutant_cfcSet` — that copy is its own
  commutant, so the **bicommutant** of `{f(T)}`, i.e. the von Neumann algebra
  generated by `T`, is again the unitary copy of `L∞(μ)`;
* `commutant_cfcSet_isCommutative` — in particular the commutant is abelian, i.e.
  the algebra generated by a normal operator with a cyclic vector is *maximal*
  abelian.

Everything is `sorry`-free and `axiom`-free.  What is still not claimed is the
non-cyclic case: a general separable Hilbert space decomposes into a direct sum of
cyclic subspaces, and assembling the models over that decomposition is not done
here.
-/

noncomputable section

open MeasureTheory ENNReal Complex

namespace BookProof.ChapterSpectralCommutant

open BookProof.ChapterLinftyMultiplication BookProof.ChapterLinftyMaximalAbelian
open BookProof.ChapterAbelianGelfandModel BookProof.ChapterSpectralMultiplication

/-! ## 1. The multiplication algebra and its commutant -/

section Algebra

variable {α : Type*} [MeasurableSpace α] {μ : Measure α}

/-- The **multiplication algebra** of `μ`: the bounded operators on `L²(μ)` that are
multiplication by an essentially bounded symbol. -/
def multAlgebra (μ : Measure α) : Set (Lp ℂ 2 μ →L[ℂ] Lp ℂ 2 μ) :=
  {S | ∃ (ψ : α → ℂ) (hψ : MemLp ψ ⊤ μ), S = multOp ψ hψ}

theorem multOp_mem_multAlgebra (ψ : α → ℂ) (hψ : MemLp ψ ⊤ μ) :
    multOp ψ hψ ∈ multAlgebra μ := ⟨ψ, hψ, rfl⟩

/-- The multiplication algebra is **commutative**. -/
theorem multAlgebra_comm {S R : Lp ℂ 2 μ →L[ℂ] Lp ℂ 2 μ} (hS : S ∈ multAlgebra μ)
    (hR : R ∈ multAlgebra μ) : S * R = R * S := by
  obtain ⟨ψ, hψ, rfl⟩ := hS
  obtain ⟨φ, hφ, rfl⟩ := hR
  have h := multOp_comm ψ φ hψ hφ
  simpa [ContinuousLinearMap.mul_def] using h

/-- **The multiplication algebra is its own commutant** (a finite measure space).
This is `ChapterLinftyMaximalAbelian.commutant_eq_multOp` read as an equality of
sets of operators. -/
theorem centralizer_multAlgebra [IsFiniteMeasure μ] :
    (multAlgebra μ).centralizer = multAlgebra μ := by
  apply Set.eq_of_subset_of_subset
  · intro S hS
    have hcomm : CommutesWithMultOps S := by
      intro φ hφ
      have h := hS (multOp φ hφ) (multOp_mem_multAlgebra φ hφ)
      simpa [ContinuousLinearMap.mul_def] using h.symm
    exact ⟨symbol S, memLp_top_symbol hcomm, commutant_eq_multOp hcomm⟩
  · intro S hS R hR
    exact multAlgebra_comm hR hS

/-- **The multiplication algebra is a von Neumann algebra**: it equals its own
bicommutant. -/
theorem bicommutant_multAlgebra [IsFiniteMeasure μ] :
    (multAlgebra μ).centralizer.centralizer = multAlgebra μ := by
  rw [centralizer_multAlgebra, centralizer_multAlgebra]

end Algebra

/-! ## 2. Continuous symbols suffice -/

section ContinuousSymbols

variable {X : Type*} [TopologicalSpace X] [CompactSpace X] [T2Space X]
  [MeasurableSpace X] [BorelSpace X] {mu : Measure X} [IsFiniteMeasure mu] [mu.WeaklyRegular]

/-- Commuting with every multiplication operator whose symbol is **continuous**. -/
def CommutesWithContMult (S : Lp ℂ 2 mu →L[ℂ] Lp ℂ 2 mu) : Prop :=
  ∀ g : C(X, ℂ), S.comp (mulRep mu g) = (mulRep mu g).comp S

/-- Continuous functions are dense in `L²` of a finite regular measure on a compact
space. -/
theorem denseRange_toLp :
    DenseRange (fun g : C(X, ℂ) => ContinuousMap.toLp 2 mu ℂ g) :=
  ContinuousMap.toLp_denseRange (μ := mu) ℂ (p := 2) ℂ (by simp)

omit [T2Space X] [mu.WeaklyRegular] in
theorem toLp_eq_mulRep_oneLp (g : C(X, ℂ)) :
    ContinuousMap.toLp 2 mu ℂ g = mulRep mu g (oneLp mu) := by
  refine Lp.ext ?_
  filter_upwards [ContinuousMap.coeFn_toLp (p := 2) mu (𝕜 := ℂ) g,
    mulRep_coeFn mu g (oneLp mu), oneLp_coeFn (μ := mu)] with x h1 h2 h3
  rw [h1, h2, h3, mul_one]

omit [T2Space X] [mu.WeaklyRegular] in
/-- Commutation with continuous multiplications already determines `S` on the
continuous functions: `S g = g · ψ` with `ψ = S(1)`. -/
theorem contSymbol_mul {S : Lp ℂ 2 mu →L[ℂ] Lp ℂ 2 mu} (hS : CommutesWithContMult S)
    (g : C(X, ℂ)) :
    ((S (ContinuousMap.toLp 2 mu ℂ g)) : X → ℂ) =ᵐ[mu] fun x => g x * symbol S x := by
  have h := congrArg (fun P : Lp ℂ 2 mu →L[ℂ] Lp ℂ 2 mu => P (oneLp mu)) (hS g)
  simp only [ContinuousLinearMap.coe_comp', Function.comp_apply] at h
  rw [toLp_eq_mulRep_oneLp, h]
  filter_upwards [mulRep_coeFn mu g (S (oneLp mu)), symbol_ae_eq S] with x h1 h2
  rw [h1, h2]

/-- An operator-norm bound that holds on the continuous functions holds on all of
`L²`, by density. -/
theorem multOp_norm_le_of_toLp {φ : X → ℂ} (hφ : MemLp φ ⊤ mu) {c : ℝ}
    (h : ∀ g : C(X, ℂ), ‖multOp φ hφ (ContinuousMap.toLp 2 mu ℂ g)‖
      ≤ c * ‖ContinuousMap.toLp 2 mu ℂ g‖) (u : Lp ℂ 2 mu) :
    ‖multOp φ hφ u‖ ≤ c * ‖u‖ := by
  have hclosed : IsClosed {v : Lp ℂ 2 mu | ‖multOp φ hφ v‖ ≤ c * ‖v‖} :=
    isClosed_le ((multOp φ hφ).continuous.norm) (continuous_const.mul continuous_norm)
  have hsub : Set.range (fun g : C(X, ℂ) => ContinuousMap.toLp 2 mu ℂ g)
      ⊆ {v : Lp ℂ 2 mu | ‖multOp φ hφ v‖ ≤ c * ‖v‖} := by
    rintro _ ⟨g, rfl⟩
    exact h g
  have : (Set.univ : Set (Lp ℂ 2 mu)) ⊆ {v : Lp ℂ 2 mu | ‖multOp φ hφ v‖ ≤ c * ‖v‖} := by
    rw [← denseRange_toLp.closure_range]
    exact hclosed.closure_subset_iff.mpr hsub
  exact this (Set.mem_univ u)

/-- **The symbol is essentially bounded by the operator norm** — the version in which
only *continuous* symbols are tested.  The truncation `1_s · ψ` is a genuine `L∞`
symbol, the inequality `‖(1_s ψ) g‖₂ ≤ ‖S‖ ‖g‖₂` holds for continuous `g`, hence for
all `g` by density, and testing it on `g = 1_s` forces `μ s = 0`. -/
theorem contSymbol_ae_norm_le {S : Lp ℂ 2 mu →L[ℂ] Lp ℂ 2 mu} (hS : CommutesWithContMult S) :
    ∀ᵐ x ∂mu, ‖symbol S x‖ ≤ ‖S‖ := by
  set c : ℝ := ‖S‖ with hc
  have key : ∀ n m : ℕ,
      mu {x | c + 1 / (n + 1 : ℝ) ≤ ‖symbol S x‖ ∧ ‖symbol S x‖ ≤ (m : ℝ)} = 0 := by
    intro n m
    set ε : ℝ := 1 / (n + 1 : ℝ) with hε
    have hεpos : 0 < ε := by positivity
    set s : Set X := {x | c + ε ≤ ‖symbol S x‖ ∧ ‖symbol S x‖ ≤ (m : ℝ)} with hsdef
    have hmeas : Measurable fun x => ‖symbol S x‖ :=
      (stronglyMeasurable_symbol S).measurable.norm
    have hs : MeasurableSet s :=
      (measurableSet_le measurable_const hmeas).inter (measurableSet_le hmeas measurable_const)
    -- the truncated symbol
    set φ : X → ℂ := s.indicator (symbol S) with hφdef
    have hφ : MemLp φ ⊤ mu := by
      refine memLp_top_of_bound
        (((stronglyMeasurable_symbol S).indicator hs).aestronglyMeasurable) (m : ℝ)
        (.of_forall fun x => ?_)
      by_cases hx : x ∈ s
      · rw [hφdef, Set.indicator_of_mem hx]
        exact hx.2
      · rw [hφdef, Set.indicator_of_notMem hx]
        simp
    -- the bound on continuous test functions
    have hcont : ∀ g : C(X, ℂ), ‖multOp φ hφ (ContinuousMap.toLp 2 mu ℂ g)‖
        ≤ c * ‖ContinuousMap.toLp 2 mu ℂ g‖ := by
      intro g
      have h1 : ‖multOp φ hφ (ContinuousMap.toLp 2 mu ℂ g)‖
          ≤ ‖S (ContinuousMap.toLp 2 mu ℂ g)‖ := by
        refine Lp.norm_le_norm_of_ae_le ?_
        filter_upwards [multOp_coeFn φ hφ (ContinuousMap.toLp 2 mu ℂ g),
          ContinuousMap.coeFn_toLp (p := 2) mu (𝕜 := ℂ) g, contSymbol_mul hS g] with x h2 h3 h4
        rw [h2, h3, h4]
        by_cases hx : x ∈ s
        · rw [hφdef, Set.indicator_of_mem hx, mul_comm]
        · rw [hφdef, Set.indicator_of_notMem hx]
          simp only [zero_mul, norm_zero, norm_mul]
          positivity
      exact h1.trans (S.le_opNorm _)
    have hall := multOp_norm_le_of_toLp hφ hcont
    -- test on the indicator of `s`
    obtain ⟨u, hu⟩ : ∃ u : Lp ℂ 2 mu, u = indicatorConstLp 2 hs (measure_ne_top mu s) (1 : ℂ) :=
      ⟨_, rfl⟩
    have hnorm_u : ‖u‖ = mu.real s ^ (1 / (2 : ℝ)) := by
      rw [hu, norm_indicatorConstLp (by norm_num) (by norm_num)]
      simp
    have hlow : ‖indicatorConstLp 2 hs (measure_ne_top mu s) ((c + ε : ℝ) : ℂ)‖
        ≤ ‖multOp φ hφ u‖ := by
      refine Lp.norm_le_norm_of_ae_le ?_
      filter_upwards [indicatorConstLp_coeFn (p := (2 : ℝ≥0∞)) (hs := hs)
          (hμs := measure_ne_top mu s) (c := ((c + ε : ℝ) : ℂ)),
        multOp_coeFn φ hφ u,
        indicatorConstLp_coeFn (p := (2 : ℝ≥0∞)) (hs := hs)
          (hμs := measure_ne_top mu s) (c := (1 : ℂ))] with x h1 h2 h3
      rw [h1, h2, hu, h3]
      by_cases hx : x ∈ s
      · have hnn : (0 : ℝ) ≤ c + ε := by rw [hc]; positivity
        rw [Set.indicator_of_mem hx, Set.indicator_of_mem hx, hφdef,
          Set.indicator_of_mem hx, mul_one, Complex.norm_real, Real.norm_eq_abs,
          abs_of_nonneg hnn]
        exact hx.1
      · rw [Set.indicator_of_notMem hx]
        simp only [norm_zero]
        positivity
    have hupper : ‖multOp φ hφ u‖ ≤ c * mu.real s ^ (1 / (2 : ℝ)) := by
      have := hall u
      rwa [hnorm_u] at this
    have hlow' : (c + ε) * mu.real s ^ (1 / (2 : ℝ)) ≤ c * mu.real s ^ (1 / (2 : ℝ)) := by
      have h := hlow.trans hupper
      rwa [norm_indicatorConstLp (by norm_num) (by norm_num), Complex.norm_real,
        Real.norm_eq_abs, abs_of_nonneg (by positivity)] at h
    have hzero : mu.real s ^ (1 / (2 : ℝ)) ≤ 0 := by nlinarith [hεpos]
    have hpow : mu.real s ^ (1 / (2 : ℝ)) = 0 :=
      le_antisymm hzero (Real.rpow_nonneg measureReal_nonneg _)
    have hms : mu.real s = 0 := by
      by_contra h
      have hpos : 0 < mu.real s := lt_of_le_of_ne measureReal_nonneg (Ne.symm h)
      exact absurd hpow (ne_of_gt (Real.rpow_pos_of_pos hpos _))
    exact (measureReal_eq_zero_iff (measure_ne_top mu s)).mp hms
  have hnull : mu {x | ¬ ‖symbol S x‖ ≤ c} = 0 := by
    have hsub : {x | ¬ ‖symbol S x‖ ≤ c}
        ⊆ ⋃ n : ℕ, ⋃ m : ℕ,
          {x | c + 1 / (n + 1 : ℝ) ≤ ‖symbol S x‖ ∧ ‖symbol S x‖ ≤ (m : ℝ)} := by
      intro x hx
      simp only [Set.mem_setOf_eq, not_le] at hx
      obtain ⟨n, hn⟩ := exists_nat_one_div_lt (sub_pos.mpr hx)
      obtain ⟨m, hm⟩ := exists_nat_ge ‖symbol S x‖
      exact Set.mem_iUnion.mpr ⟨n, Set.mem_iUnion.mpr ⟨m,
        ⟨by linarith, hm⟩⟩⟩
    refine measure_mono_null hsub (measure_iUnion_null fun n => measure_iUnion_null fun m => ?_)
    exact key n m
  simpa [ae_iff] using hnull

theorem memLp_top_contSymbol {S : Lp ℂ 2 mu →L[ℂ] Lp ℂ 2 mu} (hS : CommutesWithContMult S) :
    MemLp (symbol S) ⊤ mu :=
  memLp_top_of_bound (stronglyMeasurable_symbol S).aestronglyMeasurable ‖S‖
    (contSymbol_ae_norm_le hS)

/-- **Continuous symbols suffice.**  On a compact space with a finite regular Borel
measure, an operator on `L²(μ)` that commutes with multiplication by every
*continuous* function is itself a multiplication operator. -/
theorem contCommutant_eq_multOp {S : Lp ℂ 2 mu →L[ℂ] Lp ℂ 2 mu} (hS : CommutesWithContMult S) :
    S = multOp (symbol S) (memLp_top_contSymbol hS) := by
  set ψ := memLp_top_contSymbol hS with hψ
  have hfun : (fun v : Lp ℂ 2 mu => S v) = fun v => multOp (symbol S) ψ v := by
    refine denseRange_toLp.equalizer S.continuous (multOp (symbol S) ψ).continuous
      (funext fun g => ?_)
    simp only [Function.comp_apply]
    refine Lp.ext ?_
    filter_upwards [contSymbol_mul hS g, multOp_coeFn (symbol S) ψ (ContinuousMap.toLp 2 mu ℂ g),
      ContinuousMap.coeFn_toLp (p := 2) mu (𝕜 := ℂ) g] with x h1 h2 h3
    rw [h1, h2, h3, mul_comm]
  exact ContinuousLinearMap.ext (congrFun hfun)

theorem contCommutant_mem_multAlgebra {S : Lp ℂ 2 mu →L[ℂ] Lp ℂ 2 mu}
    (hS : CommutesWithContMult S) : S ∈ multAlgebra mu :=
  ⟨symbol S, memLp_top_contSymbol hS, contCommutant_eq_multOp hS⟩

end ContinuousSymbols

/-! ## 3. Transport through the spectral unitary -/

section Operator

variable {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
variable (T : H →L[ℂ] H) (hT : IsStarNormal T) (xi : H)
  (hcyc : DenseRange (cfcVec T hT xi))

/-- Conjugation of an operator on `L²(μ)` by the spectral unitary. -/
def conjSpectral (S : Lp ℂ 2 (spectralMeasure T hT xi) →L[ℂ] Lp ℂ 2 (spectralMeasure T hT xi)) :
    H →L[ℂ] H :=
  ((spectralUnitary T hT xi hcyc).toLinearIsometry.toContinuousLinearMap).comp
    (S.comp ((spectralUnitary T hT xi hcyc).symm.toLinearIsometry.toContinuousLinearMap))

@[simp] theorem conjSpectral_apply
    (S : Lp ℂ 2 (spectralMeasure T hT xi) →L[ℂ] Lp ℂ 2 (spectralMeasure T hT xi)) (v : H) :
    conjSpectral T hT xi hcyc S v
      = spectralUnitary T hT xi hcyc (S ((spectralUnitary T hT xi hcyc).symm v)) := rfl

/-- Conjugation of an operator on `H` back to `L²(μ)`. -/
def conjSpectralSymm (S : H →L[ℂ] H) :
    Lp ℂ 2 (spectralMeasure T hT xi) →L[ℂ] Lp ℂ 2 (spectralMeasure T hT xi) :=
  ((spectralUnitary T hT xi hcyc).symm.toLinearIsometry.toContinuousLinearMap).comp
    (S.comp ((spectralUnitary T hT xi hcyc).toLinearIsometry.toContinuousLinearMap))

@[simp] theorem conjSpectralSymm_apply (S : H →L[ℂ] H)
    (u : Lp ℂ 2 (spectralMeasure T hT xi)) :
    conjSpectralSymm T hT xi hcyc S u
      = (spectralUnitary T hT xi hcyc).symm (S (spectralUnitary T hT xi hcyc u)) := rfl

theorem conjSpectral_conjSpectralSymm (S : H →L[ℂ] H) :
    conjSpectral T hT xi hcyc (conjSpectralSymm T hT xi hcyc S) = S := by
  refine ContinuousLinearMap.ext fun v => ?_
  simp

theorem conjSpectralSymm_conjSpectral
    (S : Lp ℂ 2 (spectralMeasure T hT xi) →L[ℂ] Lp ℂ 2 (spectralMeasure T hT xi)) :
    conjSpectralSymm T hT xi hcyc (conjSpectral T hT xi hcyc S) = S := by
  refine ContinuousLinearMap.ext fun u => ?_
  simp

theorem conjSpectral_mul
    (A B : Lp ℂ 2 (spectralMeasure T hT xi) →L[ℂ] Lp ℂ 2 (spectralMeasure T hT xi)) :
    conjSpectral T hT xi hcyc (A * B)
      = conjSpectral T hT xi hcyc A * conjSpectral T hT xi hcyc B := by
  refine ContinuousLinearMap.ext fun v => ?_
  simp [ContinuousLinearMap.mul_apply]

/-- The continuous functional calculus algebra of `T`. -/
def cfcSet : Set (H →L[ℂ] H) := Set.range fun g : C(spectrum ℂ T, ℂ) => cfcHom hT g

/-- The unitary copy of the multiplication algebra `L∞(μ)` inside `B(H)`. -/
def multModel : Set (H →L[ℂ] H) :=
  conjSpectral T hT xi hcyc '' multAlgebra (spectralMeasure T hT xi)

theorem mem_multModel_iff (S : H →L[ℂ] H) :
    S ∈ multModel T hT xi hcyc ↔
      conjSpectralSymm T hT xi hcyc S ∈ multAlgebra (spectralMeasure T hT xi) := by
  constructor
  · rintro ⟨A, hA, rfl⟩
    rwa [conjSpectralSymm_conjSpectral]
  · intro h
    exact ⟨conjSpectralSymm T hT xi hcyc S, h, conjSpectral_conjSpectralSymm T hT xi hcyc S⟩

/-- Multiplication by a continuous symbol belongs to the multiplication algebra. -/
theorem mulRep_mem_multAlgebra (g : C(spectrum ℂ T, ℂ)) :
    mulRep (spectralMeasure T hT xi) g ∈ multAlgebra (spectralMeasure T hT xi) :=
  ⟨_, contMemLpTop _ g, rfl⟩

/-- **The commutation condition transported.**  `S` commutes with every `f(T)` iff its
conjugate on `L²(μ)` commutes with every multiplication by a continuous symbol. -/
theorem commutesWithContMult_conjSpectralSymm {S : H →L[ℂ] H}
    (hS : ∀ g : C(spectrum ℂ T, ℂ), cfcHom hT g * S = S * cfcHom hT g) :
    CommutesWithContMult (conjSpectralSymm T hT xi hcyc S) := by
  intro g
  refine ContinuousLinearMap.ext fun u => ?_
  simp only [ContinuousLinearMap.coe_comp', Function.comp_apply, conjSpectralSymm_apply]
  have h1 : spectralUnitary T hT xi hcyc (mulRep (spectralMeasure T hT xi) g u)
      = cfcHom hT g (spectralUnitary T hT xi hcyc u) :=
    spectralUnitary_intertwines_cfc T hT xi hcyc g u
  have h2 := congrArg (fun P : H →L[ℂ] H => P (spectralUnitary T hT xi hcyc u)) (hS g)
  simp only [ContinuousLinearMap.mul_apply] at h2
  have h3 : spectralUnitary T hT xi hcyc
        (mulRep (spectralMeasure T hT xi) g
          ((spectralUnitary T hT xi hcyc).symm (S (spectralUnitary T hT xi hcyc u))))
      = cfcHom hT g (S (spectralUnitary T hT xi hcyc u)) := by
    rw [spectralUnitary_intertwines_cfc T hT xi hcyc g, LinearIsometryEquiv.apply_symm_apply]
  rw [h1, ← h2, ← h3, LinearIsometryEquiv.symm_apply_apply]

include hcyc in
/-- **The commutant of the continuous functional calculus algebra.**  For a normal `T`
with a cyclic unit vector, an operator commutes with every `f(T)` exactly when it is
the unitary copy of a multiplication operator with essentially bounded symbol: the
commutant of `{f(T)}` *is* `L∞(μ)`. -/
theorem centralizer_cfcSet : (cfcSet T hT).centralizer = multModel T hT xi hcyc := by
  apply Set.eq_of_subset_of_subset
  · intro S hS
    have hcomm : ∀ g : C(spectrum ℂ T, ℂ), cfcHom hT g * S = S * cfcHom hT g := fun g =>
      hS _ ⟨g, rfl⟩
    rw [mem_multModel_iff]
    exact contCommutant_mem_multAlgebra (commutesWithContMult_conjSpectralSymm T hT xi hcyc hcomm)
  · rintro S hS R ⟨g, rfl⟩
    obtain ⟨ψ, hψ, hSeq⟩ := (mem_multModel_iff T hT xi hcyc S).1 hS
    have hS' : S = conjSpectral T hT xi hcyc (multOp ψ hψ) := by
      rw [← hSeq, conjSpectral_conjSpectralSymm]
    subst hS'
    refine ContinuousLinearMap.ext fun v => ?_
    simp only [ContinuousLinearMap.mul_apply, conjSpectral_apply]
    have hcomm := multOp_comm (μ := spectralMeasure T hT xi) ψ (fun z => g z) hψ
      (contMemLpTop _ g)
    have hkey := congrArg
      (fun P : Lp ℂ 2 (spectralMeasure T hT xi) →L[ℂ] Lp ℂ 2 (spectralMeasure T hT xi) =>
        P ((spectralUnitary T hT xi hcyc).symm v)) hcomm
    simp only [ContinuousLinearMap.coe_comp', Function.comp_apply] at hkey
    have h1 : spectralUnitary T hT xi hcyc
          (mulRep (spectralMeasure T hT xi) g
            (multOp ψ hψ ((spectralUnitary T hT xi hcyc).symm v)))
        = cfcHom hT g (spectralUnitary T hT xi hcyc
            (multOp ψ hψ ((spectralUnitary T hT xi hcyc).symm v))) :=
      spectralUnitary_intertwines_cfc T hT xi hcyc g _
    have h2 : (spectralUnitary T hT xi hcyc).symm (cfcHom hT g v)
        = mulRep (spectralMeasure T hT xi) g ((spectralUnitary T hT xi hcyc).symm v) := by
      have := spectralUnitary_intertwines_cfc T hT xi hcyc g
        ((spectralUnitary T hT xi hcyc).symm v)
      rw [LinearIsometryEquiv.apply_symm_apply] at this
      rw [← this, LinearIsometryEquiv.symm_apply_apply]
    rw [h2, ← h1]
    exact congrArg (spectralUnitary T hT xi hcyc) hkey.symm

include hcyc in
/-- **The model is its own commutant**: the transported multiplication algebra is a von
Neumann algebra. -/
theorem centralizer_multModel :
    (multModel T hT xi hcyc).centralizer = multModel T hT xi hcyc := by
  apply Set.eq_of_subset_of_subset
  · intro S hS
    rw [mem_multModel_iff]
    rw [← centralizer_multAlgebra (μ := spectralMeasure T hT xi)]
    intro A hA
    have hmem : conjSpectral T hT xi hcyc A ∈ multModel T hT xi hcyc := ⟨A, hA, rfl⟩
    have h := hS _ hmem
    refine ContinuousLinearMap.ext fun u => ?_
    have h2 := congrArg (fun P : H →L[ℂ] H => P (spectralUnitary T hT xi hcyc u)) h
    simp only [ContinuousLinearMap.mul_apply, conjSpectral_apply,
      LinearIsometryEquiv.symm_apply_apply] at h2
    simp only [ContinuousLinearMap.mul_apply, conjSpectralSymm_apply]
    have h3 := congrArg (spectralUnitary T hT xi hcyc).symm h2
    rwa [LinearIsometryEquiv.symm_apply_apply] at h3
  · rintro S hS R ⟨A, hA, rfl⟩
    obtain ⟨B, hB, rfl⟩ := hS
    rw [← conjSpectral_mul, ← conjSpectral_mul, multAlgebra_comm hA hB]

/-- **The bicommutant of the continuous functional calculus algebra** — the von
Neumann algebra generated by a normal operator with a cyclic vector — is the unitary
copy of `L∞(μ)`. -/
theorem bicommutant_cfcSet :
    (cfcSet T hT).centralizer.centralizer = multModel T hT xi hcyc := by
  rw [centralizer_cfcSet, centralizer_multModel]

include hcyc in
/-- **Maximal abelianness.**  The commutant of `{f(T)}` is commutative: no operator
outside the model can be adjoined to the algebra generated by `T` without breaking
commutativity. -/
theorem commutant_cfcSet_isCommutative {S R : H →L[ℂ] H}
    (hS : S ∈ (cfcSet T hT).centralizer) (hR : R ∈ (cfcSet T hT).centralizer) :
    S * R = R * S := by
  rw [centralizer_cfcSet T hT xi hcyc] at hS hR
  obtain ⟨A, hA, rfl⟩ := hS
  obtain ⟨B, hB, rfl⟩ := hR
  rw [← conjSpectral_mul, ← conjSpectral_mul, multAlgebra_comm hA hB]

end Operator

end BookProof.ChapterSpectralCommutant

end