CyclicFactorization.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

Cyclic column factorization from equality of vector functionals

Equality of quadratic forms yields an intertwining column contraction. Existence of a realizing vector is a consequence of standard form.

def OAI.KadisonSimilarity.VectorQuadraticFormsAgree line 21
Source documentation
Equality of the quadratic forms represented by one vector and by a finite family of vectors, tested on an operator star subalgebra.
```
def VectorQuadraticFormsAgree (N : StarSubalgebra ℂ (K →L[ℂ] K))
    {n : ℕ} (ξ : HilbertCopies K n) (ζ : K) : Prop :=
…
```
Mentions: OAI.KadisonSimilarity.HilbertCopies
def OAI.KadisonSimilarity.orbitLinearMap line 27
Source documentation
The linear orbit map at the vector realizing the positive functional.
```
def orbitLinearMap (N : StarSubalgebra ℂ (K →L[ℂ] K)) (ζ : K) : N →ₗ[ℂ] K where
…
```
theorem OAI.KadisonSimilarity.orbitLinearMap_apply line 32
def OAI.KadisonSimilarity.columnOrbitLinearMap line 36
Source documentation
The corresponding orbit map of the finite family.
```
def columnOrbitLinearMap (N : StarSubalgebra ℂ (K →L[ℂ] K))
    {n : ℕ} (ξ : HilbertCopies K n) : N →ₗ[ℂ] HilbertCopies K n where
…
```
Mentions: OAI.KadisonSimilarity.HilbertCopies
theorem OAI.KadisonSimilarity.columnOrbitLinearMap_apply line 48
def OAI.KadisonSimilarity.orbitClosure line 54
Source documentation
The closed cyclic subspace generated by the realizing vector.
```
def orbitClosure (N : StarSubalgebra ℂ (K →L[ℂ] K)) (ζ : K) : ClosedSubmodule ℂ K :=
…
```
def OAI.KadisonSimilarity.orbitIntoClosure line 58
Source documentation
The orbit map with codomain restricted to the closed cyclic subspace.
```
def orbitIntoClosure (N : StarSubalgebra ℂ (K →L[ℂ] K)) (ζ : K) :
    N →ₗ[ℂ] orbitClosure N ζ :=
…
```
Mentions: OAI.KadisonSimilarity.orbitClosure
theorem OAI.KadisonSimilarity.orbitIntoClosure_coe line 63
theorem OAI.KadisonSimilarity.orbitIntoClosure_dense line 67
Source documentation
The algebraic orbit is dense in its closed cyclic subspace.
```
theorem orbitIntoClosure_dense (N : StarSubalgebra ℂ (K →L[ℂ] K)) (ζ : K) :
    DenseRange (orbitIntoClosure N ζ) := by
…
```
Mentions: OAI.KadisonSimilarity.orbitIntoClosure

theorem OAI.KadisonSimilarity.orbitClosure_invariant line 76

Source documentation

The closed orbit is invariant under the star subalgebra.

theorem orbitClosure_invariant (N : StarSubalgebra ℂ (K →L[ℂ] K)) (ζ : K)
    (a : N) (x : K) (hx : x ∈ orbitClosure N ζ) :
    (a : K →L[ℂ] K) x ∈ orbitClosure N ζ := by
…

Mentions: OAI.KadisonSimilarity.orbitClosure

theorem OAI.KadisonSimilarity.orbitClosure_projection_commutes line 89
Source documentation
The orthogonal projection onto the cyclic subspace commutes with the star subalgebra.
```
theorem orbitClosure_projection_commutes (N : StarSubalgebra ℂ (K →L[ℂ] K)) (ζ : K)
    (a : N) : Commute (orbitClosure N ζ).toSubmodule.starProjection (a : K →L[ℂ] K) := by
…
```
Mentions: OAI.KadisonSimilarity.orbitClosure
theorem OAI.KadisonSimilarity.columnOrbit_norm_eq line 107
Source documentation
Equality of quadratic forms makes the two orbit maps isometric.
```
theorem columnOrbit_norm_eq (N : StarSubalgebra ℂ (K →L[ℂ] K))
    {n : ℕ} (ξ : HilbertCopies K n) (ζ : K)
    (hforms : VectorQuadraticFormsAgree N ξ ζ) (a : N) :
    ‖columnOrbitLinearMap N ξ a‖ = ‖orbitIntoClosure N ζ a‖ := by
…
```
Mentions: OAI.KadisonSimilarity.HilbertCopies, OAI.KadisonSimilarity.VectorQuadraticFormsAgree, OAI.KadisonSimilarity.columnOrbitLinearMap, OAI.KadisonSimilarity.orbitIntoClosure
theorem OAI.KadisonSimilarity.norm_eq_of_vectorQuadraticFormsAgree line 119
Source documentation
Testing the identity gives equality of the norms of the realizing vector and the finite vector family.
```
theorem norm_eq_of_vectorQuadraticFormsAgree
    (N : StarSubalgebra ℂ (K →L[ℂ] K)) {n : ℕ}
    (ξ : HilbertCopies K n) (ζ : K) (hforms : VectorQuadraticFormsAgree N ξ ζ) :
    ‖ξ‖ = ‖ζ‖ := by
…
```
Mentions: OAI.KadisonSimilarity.HilbertCopies, OAI.KadisonSimilarity.VectorQuadraticFormsAgree

theorem OAI.KadisonSimilarity.exists_intertwining_column_contraction line 130

Source documentation

Construction of the column contraction from a vector realizing the finite sum of vector functionals. It vanishes on the orthogonal complement of the closed orbit of that vector.

theorem exists_intertwining_column_contraction
    (N : StarSubalgebra ℂ (K →L[ℂ] K)) {n : ℕ}
    (ξ : HilbertCopies K n) (ζ : K) (hforms : VectorQuadraticFormsAgree N ξ ζ) :
    ∃ V : K →L[ℂ] HilbertCopies K n,
      ‖V‖ ≤ 1 ∧ V ζ = ξ ∧
      (∀ a : N, V.comp (a : K →L[ℂ] K) = (amplify (a : K →L[ℂ] K) n).comp V) ∧
      (∀ x ∈ (orbitClosure N ζ).toSubmodule.orthogonal, V x = 0) := by
…

Mentions: OAI.KadisonSimilarity.HilbertCopies, OAI.KadisonSimilarity.VectorQuadraticFormsAgree, OAI.KadisonSimilarity.amplify, OAI.KadisonSimilarity.orbitClosure

def OAI.KadisonSimilarity.columnEntry line 198
Source documentation
The coordinates of a bounded column operator.
```
def columnEntry {n : ℕ} (V : K →L[ℂ] HilbertCopies K n) (i : Fin n) : K →L[ℂ] K :=
…
```
Mentions: OAI.KadisonSimilarity.HilbertCopies
theorem OAI.KadisonSimilarity.columnEntry_apply line 202

theorem OAI.KadisonSimilarity.columnEntry_commutes line 207

Source documentation

Intertwining the diagonal action puts each column entry in the commutant.

theorem columnEntry_commutes {n : ℕ} (N : StarSubalgebra ℂ (K →L[ℂ] K))
    (V : K →L[ℂ] HilbertCopies K n)
    (hV : ∀ a : N, V.comp (a : K →L[ℂ] K) = (amplify (a : K →L[ℂ] K) n).comp V)
    (i : Fin n) (a : N) : Commute (columnEntry V i) (a : K →L[ℂ] K) := by
…

Mentions: OAI.KadisonSimilarity.HilbertCopies, OAI.KadisonSimilarity.amplify, OAI.KadisonSimilarity.columnEntry

theorem OAI.KadisonSimilarity.exists_column_factorization_of_vector_realization line 219
Source documentation
The column factorization needed in the manuscript once the realizing vector for the commutant has been supplied.
```
theorem exists_column_factorization_of_vector_realization
    (P : VonNeumannAlgebra K) {n : ℕ} (ξ : HilbertCopies K n) (ζ : K)
    (hforms : VectorQuadraticFormsAgree P.commutant.toStarSubalgebra ξ ζ) :
    ∃ V : K →L[ℂ] HilbertCopies K n,
      ‖V‖ ≤ 1 ∧ V ζ = ξ ∧ ∀ i : Fin n, columnEntry V i ∈ P := by
…
```
Mentions: OAI.KadisonSimilarity.HilbertCopies, OAI.KadisonSimilarity.VectorQuadraticFormsAgree, OAI.KadisonSimilarity.columnEntry