CyclicApproximation.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Approximate cyclic columns

Standard-form vector realization and matrix Kaplansky density with quotient norm lifting give uniformly bounded approximating columns.

def OAI.KadisonSimilarity.starSubalgebraCommutant line 26
Source documentation
The commutant of an operator star subalgebra, bundled as a von Neumann algebra by the elementary triple-commutant identity.
```
def starSubalgebraCommutant (N : StarSubalgebra ℂ (K →L[ℂ] K)) : VonNeumannAlgebra K where
…
```
theorem OAI.KadisonSimilarity.coe_starSubalgebraCommutant line 30
def OAI.KadisonSimilarity.representationVonNeumannAlgebra line 36
Source documentation
The bicommutant σ(A)″ of the represented C-star algebra.
```
def representationVonNeumannAlgebra (σ : A →⋆ₐ[ℂ] (K →L[ℂ] K)) : VonNeumannAlgebra K :=
…
```
theorem OAI.KadisonSimilarity.coe_representationVonNeumannAlgebra line 40
theorem OAI.KadisonSimilarity.mem_representationVonNeumannAlgebra line 46
def OAI.KadisonSimilarity.HaagerupCyclicVectorRealization line 54
Source documentation
The standard-form vector-realization property of a cyclic representation. It is the consequence of Haagerup (1975), Lemma 2.10(1), pp. 278–279, applied to the commutant on the cyclic subspace of a separating vector.
```
def HaagerupCyclicVectorRealization (σ : A →⋆ₐ[ℂ] (K →L[ℂ] K)) : Prop :=
…
```
def OAI.KadisonSimilarity.KaplanskyColumnApproximation line 62
Source documentation
The matrix-column consequence of Kaplansky density (Blackadar, I.9.1.3), together with the C-star first isomorphism theorem and quotient norm lifting. The lifting bound has fixed slack 2.
```
def KaplanskyColumnApproximation (σ : A →⋆ₐ[ℂ] (K →L[ℂ] K)) : Prop :=
…
```

theorem OAI.KadisonSimilarity.exists_approximating_column_sequence line 71

Source documentation

Pointwise approximation with arbitrary positive errors supplies a sequence of columns with the same norm bound.

theorem exists_approximating_column_sequence
    (σ : A →⋆ₐ[ℂ] (K →L[ℂ] K)) (kaplansky : KaplanskyColumnApproximation σ)
    {n : ℕ} (V : K →L[ℂ] HilbertCopies K n) (hV : ‖V‖ ≤ 1)
    (hentry : ∀ i : Fin n, columnEntry V i ∈ representationVonNeumannAlgebra σ)
    (ζ : K) :
    ∃ W : ℕ → Matrix (Fin n) (Fin 1) A,
      (∀ j, ‖CStarMatrix.ofMatrix (W j)‖ ≤ 2) ∧
      Tendsto (fun j => columnAction σ (W j) ζ) atTop (𝓝 (V ζ)) := by
…

Mentions: OAI.KadisonSimilarity.KaplanskyColumnApproximation, OAI.KadisonSimilarity.HilbertCopies, OAI.KadisonSimilarity.columnEntry, OAI.KadisonSimilarity.representationVonNeumannAlgebra, OAI.KadisonSimilarity.columnAction

theorem OAI.KadisonSimilarity.approximateCyclicColumns_of_published_inputs line 91
Source documentation
Vector realization and Kaplansky approximation imply approximate cyclic column factorization.
```
theorem approximateCyclicColumns_of_published_inputs
    (σ : A →⋆ₐ[ℂ] (K →L[ℂ] K))
    (haagerup : HaagerupCyclicVectorRealization σ)
    (kaplansky : KaplanskyColumnApproximation σ) : ApproximateCyclicColumns σ := by
…
```
Mentions: OAI.KadisonSimilarity.HaagerupCyclicVectorRealization, OAI.KadisonSimilarity.KaplanskyColumnApproximation, OAI.KadisonSimilarity.ApproximateCyclicColumns

theorem OAI.KadisonSimilarity.cyclic_derivation_implementation_of_published_inputs line 105

Source documentation

A cyclic derivation is implemented with a uniform norm bound under Dickson's estimate, vector realization, Kaplansky approximation and Paulsen similarity.

theorem cyclic_derivation_implementation_of_published_inputs
    {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F]
    (ρ : A →⋆ₐ[ℂ] (F →L[ℂ] F)) (σ : A →⋆ₐ[ℂ] (K →L[ℂ] K))
    (δ : A →L[ℂ] (K →L[ℂ] F))
    (hδ : ∀ a b, δ (a * b) = (ρ a).comp (δ b) + (δ a).comp (σ b))
    (dickson : DicksonTwoBound (A := A) (RectangularSum F K))
…

Mentions: OAI.KadisonSimilarity.DicksonTwoBound, OAI.KadisonSimilarity.RectangularSum