OAI/Analysis/ModularTheory/CommutantExpectation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Tomita conjugation transfers a cpc commutant projection to the von Neumann algebra in a cyclic separating representation, including quotient representations without assuming nuclearity or semidiscreteness of the quotient.

  1. theorem OAI.WeakPureInfiniteness.modular_expectation_of_commutant_expectation line 20
  2. lemma OAI.WeakPureInfiniteness.representation_bicommutant_commutant line 43
  3. theorem OAI.WeakPureInfiniteness.nuclear_quotient_standard_expectation line 58

    Source documentation

    The cyclic separating representation of a quotient of a nuclear algebra has a cpc projection onto its represented von Neumann algebra.

    theorem nuclear_quotient_standard_expectation [Nontrivial H] (hA : Nuclear A)
    (q : A →⋆ₐ[ℂ] Q) (hq : Function.Surjective q) (π : Q →⋆ₐ[ℂ] (H →L[ℂ] H))
    (S : BoundedRecovery.CyclicSeparatingData H) (hS : S.M = bicommutant π.range) :
    ∃ E : (H →L[ℂ] H) →L[ℂ] (H →L[ℂ] H), CompletelyPositive E ∧ ‖E‖ ≤ 1 ∧
      (∀ T, E T ∈ S.M) ∧ (∀ T, T ∈ S.M → E T = T) := by
…

    Mentions: OAI.WeakPureInfiniteness.Nuclear, OAI.BoundedRecovery.CyclicSeparatingData, OAI.WeakPureInfiniteness.CompletelyPositive