CentralLineApproximation.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Dense finite tests force a central line

The finite-dimensional refinement estimates pass through the projection onto the common central-vector space. Vanishing errors on a dense family then force its entire range into a single line.

theorem OAI.KadisonKastler.projection_range_line_of_dense_tests line 23

theorem OAI.KadisonKastler.matrixCentralVectorSpace_le_line_of_dense_tests line 64

Source documentation

The finite central-vector tests used in the refinement construction force the common central-vector space to be a line.

theorem matrixCentralVectorSpace_le_line_of_dense_tests
    (A : ℕ → FiniteMatrixStage M) (J : H ≃ₗᵢ⋆[ℂ] H)
    (ξ : H) (η : ℕ → H) (hdense : DenseRange η)
    (ε : ℕ → ℝ) (hε : Tendsto ε atTop (𝓝 0))
    (htest : ∀ n i, i ≤ n → ∃ c : ℂ,
      ‖(centralVectorSpace (matrixUnitConcreteAlgebra (A n).units) J).starProjection (η i) -
        c • (centralVectorSpace (matrixUnitConcreteAlgebra (A n).units) J).starProjection ξ‖ ≤ ε n) :
    matrixCentralVectorSpace A J ≤
      Submodule.span ℂ {(matrixCentralVectorSpace A J).starProjection ξ} :=
…

Mentions: OAI.KadisonKastler.centralVectorSpace, OAI.KadisonKastler.matrixUnitConcreteAlgebra, OAI.KadisonKastler.matrixCentralVectorSpace

theorem OAI.KadisonKastler.matrixCentralVectorSpace_displacement_le line 76

Source documentation

The displacement bound survives the strong projection limit.

theorem matrixCentralVectorSpace_displacement_le
    (A : ℕ → FiniteMatrixStage M)
    (hA : Monotone (fun n => (A n).units.concreteAlgebra))
    (J : H ≃ₗᵢ⋆[ℂ] H) (ξ : H) (δ : ℝ)
    (hδ : ∀ n,
      ‖ξ - (centralVectorSpace (matrixUnitConcreteAlgebra (A n).units) J).starProjection ξ‖ ≤ δ) :
    ‖ξ - (matrixCentralVectorSpace A J).starProjection ξ‖ ≤ δ :=
…

Mentions: OAI.KadisonKastler.centralVectorSpace, OAI.KadisonKastler.matrixUnitConcreteAlgebra, OAI.KadisonKastler.matrixCentralVectorSpace