The Lean 4 theorem `orthogonalFamily_cyclicSubspace` in the `?` chapter of the timepiece formalization

import Theorems.Thm_BookProof_ChapterCyclicDecomposition_isClosed_cyclicSubspace

import Definitions.Def_ChapterCyclicDecomposition
import Mathlib


/-!
# The cyclic decomposition as a Hilbert sum (plan GAP-2, the direct-sum form)

`ChapterCyclicDecomposition` produced, for a normal operator `T` on a complex
Hilbert space, a family `S` of unit vectors whose cyclic subspaces are pairwise
orthogonal and jointly dense.  This module packages that family as an honest
**orthogonal direct sum decomposition** of the space and records the operator-level
consequence: the orthogonal projections onto the summands commute with the whole
functional-calculus algebra, so `T` really is the direct sum of its restrictions.

* `orthogonalFamily_cyclicSubspace` — the cyclic subspaces of an orthogonal cyclic
  family form an `OrthogonalFamily`;
* `isHilbertSum_cyclicSubspace`, `cyclicHilbertEquiv` — when they are moreover
  total, `H` *is* their Hilbert sum: a unitary `H ≃ₗᵢ[ℂ] lp (cyclic summands) 2`;
* HEADLINE `exists_isHilbertSum_cyclicSubspace` — combining with
  `exists_cyclic_decomposition`, for **every** normal `T` such a family exists, so
  every complex Hilbert space is the Hilbert sum of subspaces cyclic for `T`;
* `starProjection_commutes_cfcHom`, `commute_starProjection_cfcHom` — the
  orthogonal projection onto an invariant subspace commutes with `f(T)` for every
  continuous `f` (the `*`-closedness of the algebra makes the complement invariant
  too), hence lies in the commutant of the algebra generated by `T`;
* `starProjection_cyclicSubspace_commutes`, `hasSum_starProjection_cyclicSubspace` —
  the same for the cyclic summands, together with the strong convergence
  `∑ₓ Pₓ v = v` of the projections of the decomposition.

Everything is `sorry`-free and `axiom`-free (only `propext`, `Classical.choice`,
`Quot.sound`).
-/

noncomputable section

open MeasureTheory Complex

namespace BookProof.ChapterCyclicDirectSum

open BookProof.ChapterCyclicDecomposition

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

/-! ## 1. The summands are complete -/

instance instCompleteSpaceCyclicSubspace (xi : H) :
    CompleteSpace (cyclicSubspace T hT xi) :=
  (isClosed_cyclicSubspace T hT xi).completeSpace_coe

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

/-- The cyclic subspaces of an orthogonal cyclic family are an orthogonal family of
subspaces in the sense of `OrthogonalFamily`. -/
theorem orthogonalFamily_cyclicSubspace {S : Set H} (hS : OrthogonalCyclicFamily T hT S) :
    OrthogonalFamily ℂ (fun x : S => (cyclicSubspace T hT (x : H)))
      (fun x : S => (cyclicSubspace T hT (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)

/-- **`H` is the Hilbert sum of the cyclic subspaces** of a total orthogonal cyclic
family. -/
theorem isHilbertSum_cyclicSubspace {S : Set H} (hS : OrthogonalCyclicFamily T hT S)
    (htop : (⨆ x ∈ S, cyclicSubspace T hT x).topologicalClosure = ⊤) :
    IsHilbertSum ℂ (fun x : S => (cyclicSubspace T hT (x : H)))
      (fun x : S => (cyclicSubspace T hT (x : H)).subtypeₗᵢ) := by
  refine IsHilbertSum.mkInternal _ (orthogonalFamily_cyclicSubspace T hT hS) ?_
  have hsup : (⨆ x : S, cyclicSubspace T hT (x : H)) = ⨆ x ∈ S, cyclicSubspace T hT x := by
    rw [iSup_subtype]
  rw [hsup, htop]

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



/-! ## 3. The projections lie in the commutant -/











end BookProof.ChapterCyclicDirectSum

end