Chapter CyclicDecomposition

import Definitions.Def_ChapterSpectralMultiplication
import Mathlib


/-!
# Decomposition into cyclic subspaces (plan GAP-2, the reduction to the cyclic case)

`ChapterSpectralMultiplication` and `ChapterSpectralCommutant` model a normal
operator **with a cyclic vector** — as multiplication by `z` on `L²(μ)`, with
commutant and bicommutant `L∞(μ)`.  The step that reduces the general case to that
one is the classical *cyclic decomposition*: for any normal `T` the space splits as
an orthogonal family of subspaces, each of which is generated by a single vector
under the continuous functional calculus of `T`.

This module proves that decomposition:

* `cyclicSubspace` — the closed subspace generated by `{f(T)ξ : f ∈ C(σ(T))}`;
* `Invariant`, `invariant_cyclicSubspace` — the cyclic subspaces are invariant under
  the whole functional calculus algebra;
* `invariant_orthogonal` — because the algebra is `*`-closed, the orthogonal
  complement of an invariant subspace is invariant, and
  `cyclicSubspace_le_orthogonal` — the cyclic subspace of a vector orthogonal to an
  invariant subspace stays orthogonal to it;
* HEADLINE `exists_cyclic_decomposition` — by Zorn's lemma there is a family of unit
  vectors whose cyclic subspaces are pairwise orthogonal and together span a dense
  subspace of `H`.

Everything is `sorry`-free and `axiom`-free.  What is still not claimed is the
assembly step: transporting the multiplication model of each summand (which requires
identifying the functional calculus of the restriction of `T` to an invariant
subspace with the restriction of the functional calculus) into a single model on a
direct sum of `L²` spaces.
-/

noncomputable section

open MeasureTheory Complex

namespace BookProof.ChapterCyclicDecomposition

open BookProof.ChapterSpectralMultiplication

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

/-! ## 1. Cyclic subspaces -/

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






  
/-! ## 2. Invariance -/

/-- A subspace invariant under the whole continuous functional calculus algebra. -/
def Invariant (M : Submodule ℂ H) : Prop :=
  ∀ (g : C(spectrum ℂ T, ℂ)) (v : H), v ∈ M → cfcHom hT g v ∈ M







/-! ## 3. The decomposition -/

/-- The property defining the family we maximize over: a set of unit vectors with
pairwise orthogonal cyclic subspaces. -/
def OrthogonalCyclicFamily (S : Set H) : Prop :=
  (∀ x ∈ S, ‖x‖ = 1) ∧
    ∀ x ∈ S, ∀ y ∈ S, x ≠ y → cyclicSubspace T hT x ≤ (cyclicSubspace T hT y)ᗮ





end BookProof.ChapterCyclicDecomposition

end