CyclicDecomposition.lean`

26 declarations, 0 contain sorry, 0 declared as axioms

Every unital star representation is the orthogonal sum of cyclic reducing representations. The family is constructed by Zorn's lemma.

theorem OAI.KadisonSimilarity.self_mem_orbitClosure line 17

theorem OAI.KadisonSimilarity.orbitClosure_le_orthogonal line 24

Source documentation

Orthogonality to one reducing cyclic subspace persists on the whole orbit of a vector, including its closure.

theorem orbitClosure_le_orthogonal (N : StarSubalgebra ℂ (H →L[ℂ] H)) (ξ η : H)
    (hξ : ξ ∈ (orbitClosure N η).toSubmodule.orthogonal) :
    (orbitClosure N ξ).toSubmodule ≤ (orbitClosure N η).toSubmodule.orthogonal := by
…

Mentions: OAI.KadisonSimilarity.orbitClosure

def OAI.KadisonSimilarity.CyclicOrbitOrthogonal line 37
Source documentation
Pairwise orthogonality of the full closed cyclic spaces.
```
def CyclicOrbitOrthogonal (N : StarSubalgebra ℂ (H →L[ℂ] H)) (ξ η : H) : Prop :=
…
```
theorem OAI.KadisonSimilarity.cyclicOrbitOrthogonal_symm line 40
def OAI.KadisonSimilarity.OrthogonalCyclicFamily line 45
def OAI.KadisonSimilarity.cyclicFamilySpan line 48
theorem OAI.KadisonSimilarity.orbitClosure_le_cyclicFamilySpan line 51
theorem OAI.KadisonSimilarity.exists_maximal_orthogonalCyclicFamily line 57
theorem OAI.KadisonSimilarity.maximal_orthogonalCyclicFamily_dense line 72
Source documentation
Maximality forces density: any nonzero vector in the orthogonal complement would supply an additional orthogonal cyclic summand.
```
theorem maximal_orthogonalCyclicFamily_dense
    (N : StarSubalgebra ℂ (H →L[ℂ] H)) {S : Set H}
    (hS : Maximal (OrthogonalCyclicFamily N) S) :
    (cyclicFamilySpan N S).topologicalClosure = ⊤ := by
…
```
Mentions: OAI.KadisonSimilarity.OrthogonalCyclicFamily, OAI.KadisonSimilarity.cyclicFamilySpan
structure OAI.KadisonSimilarity.CyclicDecompositionData line 114
Source documentation
A chosen maximal family, together with its proved density.
```
structure CyclicDecompositionData (N : StarSubalgebra ℂ (H →L[ℂ] H)) where
…
```
def OAI.KadisonSimilarity.cyclicDecompositionData line 120
abbrev OAI.KadisonSimilarity.CyclicDecompositionData.Space line 129
def OAI.KadisonSimilarity.CyclicDecompositionData.summands line 132
Source documentation
The closed cyclic spaces, as an actual complete orthogonal family.
```
def summands : OrthogonalSummandDecomposition D.Space H where
…
```
Mentions: OAI.KadisonSimilarity.OrthogonalSummandDecomposition
def OAI.KadisonSimilarity.orbitAction line 157
Source documentation
The bounded action on the actual closed orbit subspace.
```
def orbitAction (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (ξ : H) (a : A) :
    orbitClosure σ.range ξ →L[ℂ] orbitClosure σ.range ξ :=
…
```
Mentions: OAI.KadisonSimilarity.orbitClosure
theorem OAI.KadisonSimilarity.orbitAction_coe line 161
def OAI.KadisonSimilarity.orbitRepresentation line 165
Source documentation
Restriction to a cyclic reducing subspace is a unital star representation.
```
def orbitRepresentation (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (ξ : H) :
    A →⋆ₐ[ℂ] (orbitClosure σ.range ξ →L[ℂ] orbitClosure σ.range ξ) where
…
```
Mentions: OAI.KadisonSimilarity.orbitClosure
theorem OAI.KadisonSimilarity.orbitRepresentation_coe line 196
def OAI.KadisonSimilarity.orbitGenerator line 199
theorem OAI.KadisonSimilarity.orbitGenerator_dense line 203
Source documentation
The original vector has dense orbit for the restricted action.
```
theorem orbitGenerator_dense (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (ξ : H) :
    DenseRange (fun a : A => orbitRepresentation σ ξ a (orbitGenerator σ ξ)) := by
…
```
Mentions: OAI.KadisonSimilarity.orbitRepresentation, OAI.KadisonSimilarity.orbitGenerator
theorem OAI.KadisonSimilarity.orbitRepresentation_cyclic line 223
Source documentation
The original vector is a cyclic generator for the restricted action.
```
theorem orbitRepresentation_cyclic (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (ξ : H) :
    CyclicStarRepresentation (orbitRepresentation σ ξ) :=
…
```
Mentions: OAI.KadisonSimilarity.CyclicStarRepresentation, OAI.KadisonSimilarity.orbitRepresentation
def OAI.KadisonSimilarity.CyclicDecompositionData.representation line 232
Source documentation
The star representation on each member of the Zorn family.
```
def representation (i : D.generators) : A →⋆ₐ[ℂ] (D.Space i →L[ℂ] D.Space i) :=
…
```
def OAI.KadisonSimilarity.CyclicDecompositionData.generator line 235
theorem OAI.KadisonSimilarity.CyclicDecompositionData.generator_dense line 237
theorem OAI.KadisonSimilarity.CyclicDecompositionData.representation_cyclic line 241
theorem OAI.KadisonSimilarity.CyclicDecompositionData.representation_intertwines line 244
theorem OAI.KadisonSimilarity.CyclicDecompositionData.representation_generator_nonzero line 250