FiniteVectorMatrixDensity.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Matrix-stage density for a finite vector trace

Finite strong approximation on both vectors of each coefficient controls τ(y* y). A trace vector in the original representation is not required.

theorem OAI.KadisonKastler.FiniteVectorTrace.matrix_stage_approximation line 23

Source documentation

The finite vector formula turns strong matrix-stage approximation into trace approximation.

theorem FiniteVectorTrace.matrix_stage_approximation
    {τ : FaithfulTracialState (Algebra M)} (hτ : FiniteVectorTrace τ)
    (A : ℕ → FiniteMatrixStage M)
    (hA : Monotone (fun n => (A n).units.concreteAlgebra))
    (x : Algebra M) (hx : x.val ∈ FiniteMatrixStage.generated A)
    {ε : ℝ} (hε : 0 < ε) :
    ∃ n, ∃ a : Algebra M, a.val ∈ (A n).units.concreteAlgebra ∧
      traceTwoNorm τ (x - a) < ε := by
…

Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.FiniteVectorTrace, OAI.KadisonKastler.traceTwoNorm