CountableConjugacyTests.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Countable tests for the implementer relation

Strongly dense contraction families determine both inclusions of a unitary conjugacy. This is the algebraic equivalence used when forming the measurable implementer relation in the central decomposition.

theorem OAI.KadisonKastler.unitBall_subset_algebra_iff line 24
theorem OAI.KadisonKastler.unitaryConj_mem_of_strong_tests line 40
theorem OAI.KadisonKastler.unitaryConj_inclusion_of_dense_tests line 55

theorem OAI.KadisonKastler.exists_countable_conjugacy_tests line 71

Source documentation

There are two countable contraction families that determine exactly which ambient unitaries conjugate the two algebras.

theorem exists_countable_conjugacy_tests [SeparableSpace H]
    (M N : VonNeumannAlgebra H) :
    ∃ E F : Set (H →L[ℂ] H), E.Countable ∧ F.Countable ∧
      E ⊆ unitBall M ∧ F ⊆ unitBall N ∧
      ∀ v : unitary (H →L[ℂ] H), Conjugates v M N ↔
        (∀ x ∈ E, unitaryConj v x ∈ N) ∧
        (∀ y ∈ F, unitaryConj (star v) y ∈ M) := by
…

Mentions: OAI.KadisonKastler.unitBall, OAI.KadisonKastler.Conjugates, OAI.KadisonKastler.unitaryConj