OAI/Analysis/KadisonKastler/SequentialConjugacyTests.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Sequential tests for the measurable conjugacy relation

Each represented algebra on a separable Hilbert space has an actual sequence of contractions whose range is strongly dense in its unit ball. Conjugacy is exactly two countable families of finite-vector tests.

  1. structure OAI.KadisonKastler.StrongUnitBallTestSequence line 21
  2. theorem OAI.KadisonKastler.exists_strongUnitBallTestSequence line 27
  3. theorem OAI.KadisonKastler.StrongUnitBallTestSequence.range_subset line 38
  4. theorem OAI.KadisonKastler.conjugates_iff_strong_sequence_mem line 43
  5. theorem OAI.KadisonKastler.conjugates_iff_countable_strong_tests line 64

    Source documentation

    This is the exact countable relation used for choosing implementers.

    theorem conjugates_iff_countable_strong_tests {M N : VonNeumannAlgebra H}
    (A : StrongUnitBallTestSequence M) (B : StrongUnitBallTestSequence N)
    (ξ : ℕ → H) (hξ : DenseRange ξ) (v : unitary (H →L[ℂ] H)) :
    Conjugates v M N ↔
      (∀ j, CountableStrongTests ξ (Set.range B.op) (unitaryConj v (A.op j))) ∧
      (∀ j, CountableStrongTests ξ (Set.range A.op) (unitaryConj (star v) (B.op j))) := by
…

    Mentions: OAI.KadisonKastler.StrongUnitBallTestSequence, OAI.KadisonKastler.Conjugates, OAI.KadisonKastler.CountableStrongTests, OAI.KadisonKastler.unitaryConj