OAI/Analysis/RelativeGeneration/ConditionalMembership.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Generator.Tracial.mem_subalgebra_of_baseVector_mem line 13

   Source documentation

   This is the actual bounded conditional-expectation step, including faithfulness.

   theorem mem_subalgebra_of_baseVector_mem {Q : VonNeumannAlgebra H}
       (hQM : Q ≤ M) (x : M.toStarSubalgebra)
       (hx : baseVector τ x ∈ vectorOrbitClosure Q.toStarSubalgebra τ.vector) :
       x.val ∈ Q := by
   …

   Mentions: OAI.Generator.Tracial.Q, OAI.Generator.Tracial.baseVector, OAI.Generator.vectorOrbitClosure