Chapter AbelianDirectSum

import Definitions.Def_ChapterAbelianCyclicModel
import Definitions.Def_ChapterAbelianGelfandModel
import Mathlib
import Theorems.Thm_BookProof_ChapterAbelianCyclicModel_isProbabilityMeasure_repMeasure
import Theorems.Thm_BookProof_ChapterAbelianCyclicModel_mulRep_toLp


/-!
# Abelian algebras without a cyclic vector: the direct-sum model (plan GAP-2)

`ChapterAbelianCyclicModel` models an **arbitrary** abelian algebra — a unital
`*`-representation `π : C(X, ℂ) →⋆ₐ[ℂ] (H →L[ℂ] H)` of the continuous functions on a
compact Hausdorff space — **with a cyclic unit vector**, as multiplication operators
on `L²(μ)`.  This module removes the cyclic-vector hypothesis, exactly as
`ChapterCyclicDecomposition` / `ChapterCyclicDirectSum` / `ChapterSpectralDirectSum`
do for the algebra generated by a single normal operator, but now for a whole
abelian algebra at once.

* `repCyclicSubspace` — the closed subspace generated by `{π(f)ξ}`;
  `RepInvariant`, `repInvariant_repCyclicSubspace`, `repInvariant_orthogonal`
  (the `*`-closedness of the algebra makes the orthogonal complement of an invariant
  subspace invariant), `repCyclicSubspace_le_orthogonal`;
* `exists_rep_cyclic_decomposition` — by Zorn's lemma a family of unit vectors whose
  cyclic subspaces are pairwise orthogonal and jointly dense;
* `orthogonalFamily_repCyclicSubspace`, `isHilbertSum_repCyclicSubspace`,
  `exists_isHilbertSum_repCyclicSubspace` — the space *is* the Hilbert sum of those
  subspaces; `starProjection_commutes_rep` — the projections onto the summands lie in
  the commutant of the algebra;
* `repCyclicUnitary`, `repEmbedding`, `range_repEmbedding`,
  `repEmbedding_intertwines` — the model of a summand, built inside the ambient
  space: an isometric embedding of `L²(μ_ξ)` with range the cyclic subspace of `ξ`,
  carrying multiplication by every continuous symbol `g` into `π(g)`;
* HEADLINE `abelian_multiplication_model_general` — **every** unital
  `*`-representation of `C(X, ℂ)` on a complex Hilbert space is a direct sum of
  multiplication representations: there are Borel probability measures `μₓ` on `X`
  and isometric embeddings `Vₓ : L²(μₓ) → H` exhibiting `H` as their Hilbert sum,
  with `π(g)` acting on each summand as multiplication by `g`.  No cyclic vector, no
  generator and no separability are assumed;
* `abelian_multiplication_model_separable` — on a separable space the family is
  countable;
* `abelian_algebra_multiplication_model_general` — the Gelfand form, for a
  representation of an abstract commutative unital C\*-algebra.

Everything is `sorry`-free and `axiom`-free.
-/

noncomputable section

open MeasureTheory Complex WeakDual

namespace BookProof.ChapterAbelianDirectSum

open BookProof.ChapterAbelianGelfandModel BookProof.ChapterAbelianCyclicModel

variable {X : Type*} [TopologicalSpace X] [CompactSpace X] [T2Space X]
  [MeasurableSpace X] [BorelSpace X]
variable {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
variable (pi : C(X, ℂ) →⋆ₐ[ℂ] (H →L[ℂ] H))

/-! ## 1. Cyclic subspaces of a representation -/

/-- **The cyclic subspace generated by a vector**: the closed linear span of the
vectors `π(f)ξ`, `f` continuous on `X`. -/
def repCyclicSubspace (xi : H) : Submodule ℂ H :=
  (Submodule.span ℂ (Set.range fun g : C(X, ℂ) => pi g xi)).topologicalClosure

omit [CompactSpace X] [T2Space X] [MeasurableSpace X] [BorelSpace X] in
theorem isClosed_repCyclicSubspace (xi : H) :
    IsClosed (repCyclicSubspace pi xi : Set H) :=
  Submodule.isClosed_topologicalClosure _

omit [CompactSpace X] [T2Space X] [MeasurableSpace X] [BorelSpace X] in
theorem rep_apply_mem_repCyclicSubspace (xi : H) (g : C(X, ℂ)) :
    pi g xi ∈ repCyclicSubspace pi xi :=
  Submodule.le_topologicalClosure _ (Submodule.subset_span ⟨g, rfl⟩)

omit [CompactSpace X] [T2Space X] [MeasurableSpace X] [BorelSpace X] in
theorem self_mem_repCyclicSubspace (xi : H) : xi ∈ repCyclicSubspace pi xi := by
  have h := rep_apply_mem_repCyclicSubspace pi xi 1
  rwa [map_one] at h

/-! ## 2. Invariance -/

/-- A subspace invariant under the whole represented algebra. -/
def RepInvariant (M : Submodule ℂ H) : Prop :=
  ∀ (g : C(X, ℂ)) (v : H), v ∈ M → pi g v ∈ M

omit [CompactSpace X] [T2Space X] [MeasurableSpace X] [BorelSpace X] in
theorem repInvariant_repCyclicSubspace (xi : H) :
    RepInvariant pi (repCyclicSubspace pi xi) := by
  intro g v hv
  have hle : Submodule.span ℂ (Set.range fun f : C(X, ℂ) => pi f xi)
      ≤ (repCyclicSubspace pi xi).comap (pi g).toLinearMap := by
    refine Submodule.span_le.mpr ?_
    rintro _ ⟨f, rfl⟩
    have hgf : pi g (pi f xi) = pi (g * f) xi := by
      rw [map_mul]
      rfl
    simp only [SetLike.mem_coe, Submodule.mem_comap, ContinuousLinearMap.coe_coe, hgf]
    exact rep_apply_mem_repCyclicSubspace pi xi (g * f)
  have hclosed : IsClosed
      ((repCyclicSubspace pi xi).comap (pi g).toLinearMap : Set H) :=
    (isClosed_repCyclicSubspace pi xi).preimage (pi g).continuous
  exact Submodule.topologicalClosure_minimal _ hle hclosed hv

omit [CompactSpace X] [T2Space X] [MeasurableSpace X] [BorelSpace X] in
/-- **The orthogonal complement of an invariant subspace is invariant** — this is
where `*`-closedness of the represented algebra enters. -/
theorem repInvariant_orthogonal {M : Submodule ℂ H} (hM : RepInvariant pi M) :
    RepInvariant pi Mᗮ := by
  intro g v hv
  rw [Submodule.mem_orthogonal]
  intro u hu
  have hadj : (ContinuousLinearMap.adjoint (pi g)) u = pi (star g) u := by
    have h : star (pi g) = pi (star g) := (map_star pi g).symm
    rw [← ContinuousLinearMap.star_eq_adjoint, h]
  have h0 : (inner ℂ (pi (star g) u) v : ℂ) = 0 :=
    (Submodule.mem_orthogonal M v).1 hv _ (hM (star g) u hu)
  rw [← ContinuousLinearMap.adjoint_inner_left, hadj, h0]

omit [CompactSpace X] [T2Space X] [MeasurableSpace X] [BorelSpace X] in
/-- The cyclic subspace of a vector orthogonal to an invariant subspace is again
orthogonal to it. -/
theorem repCyclicSubspace_le_orthogonal {M : Submodule ℂ H} (hM : RepInvariant pi M) {v : H}
    (hv : v ∈ Mᗮ) : repCyclicSubspace pi v ≤ Mᗮ := by
  refine Submodule.topologicalClosure_minimal _ (Submodule.span_le.mpr ?_)
    (Submodule.isClosed_orthogonal M)
  rintro _ ⟨g, rfl⟩
  exact repInvariant_orthogonal pi hM g v hv

/-! ## 3. The decomposition -/

/-- A set of unit vectors with pairwise orthogonal cyclic subspaces. -/
def OrthogonalRepCyclicFamily (S : Set H) : Prop :=
  (∀ x ∈ S, ‖x‖ = 1) ∧
    ∀ x ∈ S, ∀ y ∈ S, x ≠ y → repCyclicSubspace pi x ≤ (repCyclicSubspace pi y)ᗮ

omit [CompactSpace X] [T2Space X] [MeasurableSpace X] [BorelSpace X] in
theorem repInvariant_iSup_repCyclicSubspace (S : Set H) :
    RepInvariant pi (⨆ x ∈ S, repCyclicSubspace pi x).topologicalClosure := by
  intro g v hv
  have hle : (⨆ x ∈ S, repCyclicSubspace pi x)
      ≤ ((⨆ x ∈ S, repCyclicSubspace pi x).topologicalClosure).comap (pi g).toLinearMap := by
    refine iSup_le fun x => iSup_le fun hx => ?_
    intro w hw
    simp only [Submodule.mem_comap, ContinuousLinearMap.coe_coe]
    refine Submodule.le_topologicalClosure _ ?_
    have : pi g w ∈ repCyclicSubspace pi x := repInvariant_repCyclicSubspace pi x g w hw
    exact le_iSup₂ (f := fun x (_ : x ∈ S) => repCyclicSubspace pi x) x hx this
  have hclosed : IsClosed
      (((⨆ x ∈ S, repCyclicSubspace pi x).topologicalClosure).comap
        (pi g).toLinearMap : Set H) :=
    (Submodule.isClosed_topologicalClosure _).preimage (pi g).continuous
  exact Submodule.topologicalClosure_minimal _ hle hclosed hv

omit [CompactSpace X] [T2Space X] [MeasurableSpace X] [BorelSpace X] in
/-- **Cyclic decomposition for a representation.**  There is a family of unit vectors
whose cyclic subspaces are pairwise orthogonal and whose span is dense: the space is
the orthogonal direct sum of subspaces cyclic for the whole algebra. -/
theorem exists_rep_cyclic_decomposition :
    ∃ S : Set H, OrthogonalRepCyclicFamily pi S ∧
      (⨆ x ∈ S, repCyclicSubspace pi x).topologicalClosure = ⊤ := by
  obtain ⟨S, hS⟩ :=
    zorn_subset {S : Set H | OrthogonalRepCyclicFamily pi S} (fun c hc hchain => by
      refine ⟨⋃₀ c, ⟨?_, ?_⟩, fun s hs => Set.subset_sUnion_of_mem hs⟩
      · rintro x ⟨s, hs, hx⟩
        exact ((hc hs).1) x hx
      · rintro x ⟨s, hs, hx⟩ y ⟨t, ht, hy⟩ hxy
        rcases hchain.total hs ht with h | h
        · exact ((hc ht).2) x (h hx) y hy hxy
        · exact ((hc hs).2) x hx y (h hy) hxy)
  refine ⟨S, hS.1, ?_⟩
  set N : Submodule ℂ H := ⨆ x ∈ S, repCyclicSubspace pi x with hN
  haveI : CompleteSpace N.topologicalClosure :=
    (Submodule.isClosed_topologicalClosure N).completeSpace_coe
  by_contra hne
  have hbot : N.topologicalClosureᗮ ≠ ⊥ := by
    intro h
    exact hne (Submodule.orthogonal_eq_bot_iff.1 h)
  obtain ⟨v, hv, hv0⟩ := Submodule.exists_mem_ne_zero_of_ne_bot hbot
  set u : H := ‖v‖⁻¹ • v with hu
  have hnv : ‖v‖ ≠ 0 := norm_ne_zero_iff.2 hv0
  have hunorm : ‖u‖ = 1 := by
    rw [hu, norm_smul]
    simp [hnv]
  have humem : u ∈ N.topologicalClosureᗮ := Submodule.smul_mem _ _ hv
  have hcyc : repCyclicSubspace pi u ≤ N.topologicalClosureᗮ :=
    repCyclicSubspace_le_orthogonal pi (repInvariant_iSup_repCyclicSubspace pi S) humem
  have hle : ∀ x ∈ S, repCyclicSubspace pi x ≤ N.topologicalClosure := fun x hx =>
    le_trans (le_iSup₂ (f := fun x (_ : x ∈ S) => repCyclicSubspace pi x) x hx)
      (Submodule.le_topologicalClosure N)
  have hnew : (insert u S) ∈ {S : Set H | OrthogonalRepCyclicFamily pi S} := by
    constructor
    · rintro x (rfl | hx)
      · exact hunorm
      · exact hS.1.1 x hx
    · have key : ∀ x ∈ S, repCyclicSubspace pi u ≤ (repCyclicSubspace pi x)ᗮ := fun x hx =>
        le_trans hcyc (Submodule.orthogonal_le (hle x hx))
      have key' : ∀ x ∈ S, repCyclicSubspace pi x ≤ (repCyclicSubspace pi u)ᗮ := fun x hx =>
        le_trans (le_trans (hle x hx) (Submodule.le_orthogonal_orthogonal _))
          (Submodule.orthogonal_le hcyc)
      rintro x (rfl | hx) y (rfl | hy) hxy
      · exact absurd rfl hxy
      · exact key y hy
      · exact key' x hx
      · exact hS.1.2 x hx y hy hxy
  have hnotmem : u ∉ S := by
    intro hmem
    have h1 : u ∈ N.topologicalClosure := hle u hmem (self_mem_repCyclicSubspace pi u)
    have : u = 0 := inner_self_eq_zero.1 ((Submodule.mem_orthogonal _ _).1 humem u h1)
    rw [this] at hunorm
    simp at hunorm
  exact hnotmem (hS.2 hnew (Set.subset_insert u S) (Set.mem_insert u S))

/-! ## 4. The Hilbert sum -/

instance instCompleteSpaceRepCyclicSubspace (xi : H) :
    CompleteSpace (repCyclicSubspace pi xi) :=
  (isClosed_repCyclicSubspace pi xi).completeSpace_coe

omit [CompactSpace X] [T2Space X] [MeasurableSpace X] [BorelSpace X] in
theorem orthogonalFamily_repCyclicSubspace {S : Set H} (hS : OrthogonalRepCyclicFamily pi S) :
    OrthogonalFamily ℂ (fun x : S => (repCyclicSubspace pi (x : H)))
      (fun x : S => (repCyclicSubspace pi (x : H)).subtypeₗᵢ) := by
  refine OrthogonalFamily.of_pairwise ?_
  intro x y hxy
  refine Submodule.isOrtho_iff_le.2 ?_
  exact hS.2 (x : H) x.2 (y : H) y.2 (Subtype.coe_injective.ne hxy)

omit [CompactSpace X] [T2Space X] [MeasurableSpace X] [BorelSpace X] in
/-- **`H` is the Hilbert sum of the cyclic subspaces** of a total orthogonal cyclic
family. -/
theorem isHilbertSum_repCyclicSubspace {S : Set H} (hS : OrthogonalRepCyclicFamily pi S)
    (htop : (⨆ x ∈ S, repCyclicSubspace pi x).topologicalClosure = ⊤) :
    IsHilbertSum ℂ (fun x : S => (repCyclicSubspace pi (x : H)))
      (fun x : S => (repCyclicSubspace pi (x : H)).subtypeₗᵢ) := by
  refine IsHilbertSum.mkInternal _ (orthogonalFamily_repCyclicSubspace pi hS) ?_
  have hsup : (⨆ x : S, repCyclicSubspace pi (x : H)) = ⨆ x ∈ S, repCyclicSubspace pi x := by
    rw [iSup_subtype]
  rw [hsup, htop]

/-- The unitary identification of `H` with the `ℓ²`-sum of the cyclic subspaces. -/
def repCyclicHilbertEquiv {S : Set H} (hS : OrthogonalRepCyclicFamily pi S)
    (htop : (⨆ x ∈ S, repCyclicSubspace pi x).topologicalClosure = ⊤) :
    H ≃ₗᵢ[ℂ] lp (fun x : S => (repCyclicSubspace pi (x : H))) 2 :=
  (isHilbertSum_repCyclicSubspace pi hS htop).linearIsometryEquiv

omit [CompactSpace X] [T2Space X] [MeasurableSpace X] [BorelSpace X] in
/-- For every representation the space is the Hilbert sum of cyclic subspaces. -/
theorem exists_isHilbertSum_repCyclicSubspace :
    ∃ S : Set H, OrthogonalRepCyclicFamily pi S ∧
      IsHilbertSum ℂ (fun x : S => (repCyclicSubspace pi (x : H)))
        (fun x : S => (repCyclicSubspace pi (x : H)).subtypeₗᵢ) := by
  obtain ⟨S, hS, htop⟩ := exists_rep_cyclic_decomposition pi
  exact ⟨S, hS, isHilbertSum_repCyclicSubspace pi hS htop⟩

omit [CompactSpace X] [T2Space X] [MeasurableSpace X] [BorelSpace X] in
/-- **The orthogonal projection onto an invariant subspace lies in the commutant** of
the represented algebra. -/
theorem starProjection_commutes_rep {M : Submodule ℂ H} [M.HasOrthogonalProjection]
    (hM : RepInvariant pi M) (g : C(X, ℂ)) (v : H) :
    M.starProjection (pi g v) = pi g (M.starProjection v) := by
  refine Submodule.eq_starProjection_of_mem_orthogonal'
    (hM g _ (M.starProjection_apply_mem v))
    (repInvariant_orthogonal pi hM g _ (M.sub_starProjection_mem_orthogonal v)) ?_
  rw [← map_add]
  congr 1
  abel

omit [CompactSpace X] [T2Space X] [MeasurableSpace X] [BorelSpace X] in
theorem commute_starProjection_rep {M : Submodule ℂ H} [M.HasOrthogonalProjection]
    (hM : RepInvariant pi M) (g : C(X, ℂ)) :
    Commute M.starProjection (pi g) := by
  ext v
  simpa [ContinuousLinearMap.mul_apply] using starProjection_commutes_rep pi hM g v

/-! ## 5. The model of a summand, built inside the ambient space -/

variable (xi : H)

omit [T2Space X] [MeasurableSpace X] [BorelSpace X] in
theorem repCyclicSubspace_eq_closure_range :
    (repCyclicSubspace pi xi : Set H) = closure (Set.range (repVec pi xi)) := by
  have hrange : (Set.range fun g : C(X, ℂ) => pi g xi) = Set.range (repVec pi xi) := rfl
  have hspan : Submodule.span ℂ (Set.range fun g : C(X, ℂ) => pi g xi)
      = LinearMap.range (repVec pi xi) := by
    rw [hrange, ← LinearMap.coe_range, Submodule.span_eq]
  rw [repCyclicSubspace, hspan]
  exact Submodule.topologicalClosure_coe _

/-- The generating map `f ↦ π(f)ξ`, seen as a map into the cyclic subspace of `ξ`. -/
def repVecTo : C(X, ℂ) →ₗ[ℂ] repCyclicSubspace pi xi :=
  LinearMap.codRestrict _ (repVec pi xi) (rep_apply_mem_repCyclicSubspace pi xi)

omit [T2Space X] [MeasurableSpace X] [BorelSpace X] in
@[simp] theorem repVecTo_apply (f : C(X, ℂ)) : (repVecTo pi xi f : H) = pi f xi := rfl

omit [T2Space X] [MeasurableSpace X] [BorelSpace X] in
theorem denseRange_repVecTo : DenseRange (repVecTo pi xi) := by
  change Dense (Set.range (repVecTo pi xi))
  rw [Topology.IsInducing.subtypeVal.dense_iff]
  intro m
  have hm : (m : H) ∈ closure (Set.range (repVec pi xi)) := by
    rw [← repCyclicSubspace_eq_closure_range]
    exact m.2
  refine closure_mono ?_ hm
  rintro _ ⟨f, rfl⟩
  exact ⟨repVecTo pi xi f, ⟨f, rfl⟩, rfl⟩

/-- **The model of a cyclic summand**: since `‖π(f)ξ‖ = ‖f‖_{L²(μ_ξ)}` with no
cyclicity hypothesis, `f ↦ π(f)ξ` extends to a unitary from `L²(μ_ξ)` onto the cyclic
subspace of `ξ`. -/
def repCyclicUnitary : Lp ℂ 2 (repMeasure pi xi) ≃ₗᵢ[ℂ] repCyclicSubspace pi xi :=
  (LinearEquiv.refl ℂ C(X, ℂ)).extendOfIsometry
    (ContinuousMap.toLp 2 (repMeasure pi xi) ℂ).toLinearMap
    (repVecTo pi xi)
    (ContinuousMap.toLp_denseRange ℂ _ (μ := repMeasure pi xi) (by simp))
    (denseRange_repVecTo pi xi)
    (fun f => by simpa using (norm_rep_apply pi xi f))

@[simp] theorem repCyclicUnitary_toLp (f : C(X, ℂ)) :
    repCyclicUnitary pi xi (ContinuousMap.toLp 2 (repMeasure pi xi) ℂ f) = repVecTo pi xi f :=
  LinearEquiv.extendOfIsometry_eq _ _ _ _ _ _ f

/-- The model read inside the ambient space: an isometric embedding of `L²(μ_ξ)` into
`H` with range the cyclic subspace of `ξ`. -/
def repEmbedding : Lp ℂ 2 (repMeasure pi xi) →ₗᵢ[ℂ] H :=
  (repCyclicSubspace pi xi).subtypeₗᵢ.comp (repCyclicUnitary pi xi).toLinearIsometry

@[simp] theorem repEmbedding_apply (u : Lp ℂ 2 (repMeasure pi xi)) :
    repEmbedding pi xi u = (repCyclicUnitary pi xi u : H) := rfl

@[simp] theorem repEmbedding_toLp (f : C(X, ℂ)) :
    repEmbedding pi xi (ContinuousMap.toLp 2 (repMeasure pi xi) ℂ f) = pi f xi := by
  simp [repEmbedding]

theorem mem_repCyclicSubspace_repEmbedding (u : Lp ℂ 2 (repMeasure pi xi)) :
    repEmbedding pi xi u ∈ repCyclicSubspace pi xi := (repCyclicUnitary pi xi u).2

theorem range_repEmbedding :
    LinearMap.range (repEmbedding pi xi).toLinearMap = repCyclicSubspace pi xi := by
  apply le_antisymm
  · rintro _ ⟨u, rfl⟩
    exact mem_repCyclicSubspace_repEmbedding pi xi u
  · intro v hv
    refine ⟨(repCyclicUnitary pi xi).symm ⟨v, hv⟩, ?_⟩
    change (repCyclicUnitary pi xi ((repCyclicUnitary pi xi).symm ⟨v, hv⟩) : H) = v
    rw [LinearIsometryEquiv.apply_symm_apply]

/-- **The embedding intertwines multiplication by a continuous symbol with the
representation**: `V M_g = π(g) V`. -/
theorem repEmbedding_intertwines (g : C(X, ℂ)) (u : Lp ℂ 2 (repMeasure pi xi)) :
    repEmbedding pi xi (mulRep (repMeasure pi xi) g u) = pi g (repEmbedding pi xi u) := by
  have hdense : DenseRange
      ((ContinuousMap.toLp 2 (repMeasure pi xi) ℂ).toLinearMap :
        C(X, ℂ) → Lp ℂ 2 (repMeasure pi xi)) :=
    ContinuousMap.toLp_denseRange ℂ _ (μ := repMeasure pi xi) (by simp)
  have hcont₁ : Continuous fun v : Lp ℂ 2 (repMeasure pi xi) =>
      repEmbedding pi xi (mulRep (repMeasure pi xi) g v) :=
    (repEmbedding pi xi).continuous.comp (mulRep (repMeasure pi xi) g).continuous
  have hcont₂ : Continuous fun v : Lp ℂ 2 (repMeasure pi xi) =>
      pi g (repEmbedding pi xi v) :=
    (pi g).continuous.comp (repEmbedding pi xi).continuous
  have hfun : (fun v : Lp ℂ 2 (repMeasure pi xi) =>
        repEmbedding pi xi (mulRep (repMeasure pi xi) g v))
      = fun v : Lp ℂ 2 (repMeasure pi xi) => pi g (repEmbedding pi xi v) := by
    refine hdense.equalizer hcont₁ hcont₂ (funext fun f => ?_)
    simp only [Function.comp_apply, ContinuousLinearMap.coe_coe]
    rw [mulRep_toLp pi xi g f, repEmbedding_toLp, repEmbedding_toLp, map_mul]
    rfl
  exact congrFun hfun u

/-! ## 6. Gluing the summand models -/

variable {pi}

omit [CompleteSpace H] in
theorem inner_eq_zero_of_le_orthogonal {M N : Submodule ℂ H} (h : M ≤ Nᗮ) {a b : H}
    (ha : a ∈ M) (hb : b ∈ N) : inner ℂ a b = 0 := by
  have h0 := (Submodule.mem_orthogonal N a).1 (h ha) b hb
  simpa [inner_eq_zero_symm] using h0

theorem orthogonalFamily_repEmbedding {S : Set H} (hS : OrthogonalRepCyclicFamily pi S) :
    OrthogonalFamily ℂ (fun x : S => Lp ℂ 2 (repMeasure pi (x : H)))
      (fun x : S => repEmbedding pi (x : H)) := by
  intro x y hxy u v
  have hle := hS.2 (x : H) x.2 (y : H) y.2 (Subtype.coe_injective.ne hxy)
  exact inner_eq_zero_of_le_orthogonal hle
    (mem_repCyclicSubspace_repEmbedding pi (x : H) u)
    (mem_repCyclicSubspace_repEmbedding pi (y : H) v)

variable (pi)

/-- **HEADLINE (the general multiplication model of an abelian algebra).**  For every
unital `*`-representation `π` of `C(X, ℂ)` on a complex Hilbert space there are Borel
probability measures `μₓ` on `X` and isometric embeddings `Vₓ : L²(μₓ) → H` which
exhibit `H` as the Hilbert sum of the spaces `L²(μₓ)` and carry multiplication by
every continuous symbol `g` into `π(g)`.

Every abelian algebra of operators is a direct sum of multiplication algebras: no
cyclic vector, no generator and no separability are assumed. -/
theorem abelian_multiplication_model_general :
    ∃ (S : Set H) (mu : S → Measure X) (V : ∀ x : S, Lp ℂ 2 (mu x) →ₗᵢ[ℂ] H),
      (∀ x : S, IsProbabilityMeasure (mu x)) ∧
      IsHilbertSum ℂ (fun x : S => Lp ℂ 2 (mu x)) V ∧
      (∀ (x : S) (g : C(X, ℂ)) (u : Lp ℂ 2 (mu x)),
        V x (mulRep (mu x) g u) = pi g (V x u)) := by
  obtain ⟨S, hS, htop⟩ := exists_rep_cyclic_decomposition pi
  refine ⟨S, fun x => repMeasure pi (x : H), fun x => repEmbedding pi (x : H),
    fun x => isProbabilityMeasure_repMeasure pi (x : H) (hS.1 (x : H) x.2), ?_,
    fun x g u => repEmbedding_intertwines pi (x : H) g u⟩
  refine IsHilbertSum.mk (orthogonalFamily_repEmbedding hS) ?_
  have hrange : (⨆ x : S, LinearMap.range (repEmbedding pi (x : H)).toLinearMap)
      = ⨆ x ∈ S, repCyclicSubspace pi x := by
    rw [iSup_subtype]
    exact iSup_congr fun x => iSup_congr fun _ => range_repEmbedding pi x
  rw [hrange, htop]

/-! ## 7. The separable case -/

variable {pi}

omit [CompactSpace X] [T2Space X] [MeasurableSpace X] [BorelSpace X] in
theorem inner_eq_zero_of_orthogonalRepCyclicFamily {S : Set H}
    (hS : OrthogonalRepCyclicFamily pi S) {x y : H} (hx : x ∈ S) (hy : y ∈ S) (hxy : x ≠ y) :
    inner ℂ x y = (0 : ℂ) :=
  inner_eq_zero_of_le_orthogonal (hS.2 x hx y hy hxy) (self_mem_repCyclicSubspace pi x)
    (self_mem_repCyclicSubspace pi y)

omit [CompactSpace X] [T2Space X] [MeasurableSpace X] [BorelSpace X] in
theorem one_lt_dist_of_orthogonalRepCyclicFamily {S : Set H}
    (hS : OrthogonalRepCyclicFamily pi S) {x y : H} (hx : x ∈ S) (hy : y ∈ S) (hxy : x ≠ y) :
    1 < dist x y := by
  have h := inner_eq_zero_of_orthogonalRepCyclicFamily hS hx hy hxy
  have hxn : ‖x‖ = 1 := hS.1 x hx
  have hyn : ‖y‖ = 1 := hS.1 y hy
  have hneg : inner ℂ x (-y) = (0 : ℂ) := by simp [h]
  have h2 : ‖x + -y‖ * ‖x + -y‖ = 2 := by
    rw [norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero x (-y) hneg, hxn, norm_neg, hyn]
    norm_num
  have hd : dist x y = ‖x + -y‖ := by rw [dist_eq_norm, sub_eq_add_neg]
  nlinarith [norm_nonneg (x + -y), hd, h2]

omit [CompactSpace X] [T2Space X] [MeasurableSpace X] [BorelSpace X] in
/-- On a separable space such a family is countable. -/
theorem countable_orthogonalRepCyclicFamily [TopologicalSpace.SeparableSpace H] {S : Set H}
    (hS : OrthogonalRepCyclicFamily pi S) : S.Countable := by
  refine Set.PairwiseDisjoint.countable_of_isOpen (s := fun x : H => Metric.ball x (1 / 2)) ?_
    (fun x _ => Metric.isOpen_ball) (fun x _ => ⟨x, Metric.mem_ball_self (by norm_num)⟩)
  intro x hx y hy hxy
  refine Metric.ball_disjoint_ball ?_
  have := one_lt_dist_of_orthogonalRepCyclicFamily hS hx hy hxy
  linarith

variable (pi)

/-- **HEADLINE (the separable case).**  On a separable complex Hilbert space every
abelian algebra, presented as a unital `*`-representation of `C(X, ℂ)`, is a
*countable* direct sum of multiplication algebras. -/
theorem abelian_multiplication_model_separable [TopologicalSpace.SeparableSpace H] :
    ∃ (S : Set H) (mu : S → Measure X) (V : ∀ x : S, Lp ℂ 2 (mu x) →ₗᵢ[ℂ] H),
      S.Countable ∧
      (∀ x : S, IsProbabilityMeasure (mu x)) ∧
      IsHilbertSum ℂ (fun x : S => Lp ℂ 2 (mu x)) V ∧
      (∀ (x : S) (g : C(X, ℂ)) (u : Lp ℂ 2 (mu x)),
        V x (mulRep (mu x) g u) = pi g (V x u)) := by
  obtain ⟨S, hS, htop⟩ := exists_rep_cyclic_decomposition pi
  refine ⟨S, fun x => repMeasure pi (x : H), fun x => repEmbedding pi (x : H),
    countable_orthogonalRepCyclicFamily hS,
    fun x => isProbabilityMeasure_repMeasure pi (x : H) (hS.1 (x : H) x.2), ?_,
    fun x g u => repEmbedding_intertwines pi (x : H) g u⟩
  refine IsHilbertSum.mk (orthogonalFamily_repEmbedding hS) ?_
  have hrange : (⨆ x : S, LinearMap.range (repEmbedding pi (x : H)).toLinearMap)
      = ⨆ x ∈ S, repCyclicSubspace pi x := by
    rw [iSup_subtype]
    exact iSup_congr fun x => iSup_congr fun _ => range_repEmbedding pi x
  rw [hrange, htop]

end BookProof.ChapterAbelianDirectSum

/-! ## 8. The Gelfand form -/

namespace BookProof.ChapterAbelianDirectSum

open BookProof.ChapterAbelianGelfandModel BookProof.ChapterAbelianCyclicModel

variable {A : Type*} [CommCStarAlgebra A]
variable {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]



end BookProof.ChapterAbelianDirectSum

end