MatrixClosureExpectation.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

State-preserving expectations onto increasing matrix closures

The finite compressions retain the state on the larger algebra. Taking their weak limit gives the required expectation on the original space.

theorem OAI.KadisonKastler.exists_matrixClosure_state_retraction line 25

Source documentation

Centralizing matrix stages give a state-preserving retraction on their closure.

theorem exists_matrixClosure_state_retraction [Nontrivial H]
    (A : ℕ → FiniteMatrixStage M)
    (hA : Monotone (fun n => (A n).units.concreteAlgebra))
    (τ : TracialRepresentation (FiniteMatrixStage.generatedVonNeumann A))
    (hcentral : ∀ n a, a ∈ (A n).units.concreteAlgebra → ∀ x : Algebra M,
      inner ℂ τ.vector ((a * x.val) τ.vector) =
        inner ℂ τ.vector ((x.val * a) τ.vector)) :
    ∃ P : Algebra M →L[ℂ] Algebra (FiniteMatrixStage.generatedVonNeumann A),
      ‖P‖ ≤ 1 ∧
      (∀ a, P (coordinateInclusion (FiniteMatrixStage.generatedVonNeumann_le A) a) = a) ∧
      (∀ a : Algebra M,
        inner ℂ τ.vector ((P a).val τ.vector) = inner ℂ τ.vector (a.val τ.vector)) := by
…

Mentions: OAI.KadisonKastler.Algebra

theorem OAI.KadisonKastler.expectedMatrixSubfactorModel_of_centralizing_stages line 91

Source documentation

Centralizing matrix stages yield an expectation and a faithful trace.

theorem expectedMatrixSubfactorModel_of_centralizing_stages [Nontrivial H]
    (A : ℕ → FiniteMatrixStage M)
    (hA : Monotone (fun n => (A n).units.concreteAlgebra))
    (Ω : H) (hΩ : ‖Ω‖ = 1)
    (hcyc : DenseRange (algebraVectorMap M Ω))
    (hsep : Function.Injective (algebraVectorMap M Ω))
    (hcentral : ∀ n a, a ∈ (A n).units.concreteAlgebra → ∀ x : Algebra M,
      inner ℂ Ω ((a * x.val) Ω) = inner ℂ Ω ((x.val * a) Ω))
    (hirr : ∀ T ∈ M,
      (∀ r ∈ FiniteMatrixStage.generatedVonNeumann A, r * T = T * r) →
      ∃ z : ℂ, T = z • (1 : H →L[ℂ] H)) :
    Nonempty (ExpectedMatrixSubfactorModel M) := by
…

Mentions: OAI.KadisonKastler.algebraVectorMap, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.ExpectedMatrixSubfactorModel