OAI/Analysis/KadisonKastler/PopaPosition.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The second finite-base independence application

The test space is constructed inside the algebra generated by the constant algebra and the first model unitary. Its separability follows from the proved trace-separability extension theorem.

  1. def OAI.KadisonKastler.positionAlgebra line 19
  2. def OAI.KadisonKastler.positionTestSpace line 22
  3. theorem OAI.KadisonKastler.mem_positionTestSpace line 26
  4. theorem OAI.KadisonKastler.positionTestSpace_traceSeparable line 35

    Source documentation

    This is exactly the separable test space needed in the second Popa application; no separability premise remains for the generated algebra.

    theorem positionTestSpace_traceSeparable (τ : FaithfulTracialState B)
    (D : StarSubalgebra ℂ B) [FiniteDimensional ℂ D]
    (A : StarSubalgebra ℂ B) (hA : TraceSeparable τ (A : Set B)) (u : B) :
    TraceSeparable τ (positionTestSpace τ D A u : Set B) :=
…

    Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.TraceSeparable, OAI.KadisonKastler.positionTestSpace

  5. theorem OAI.KadisonKastler.FiniteBaseIndependence.exists_position line 41