OAI/Analysis/KadisonKastler/MeasurableConjugacyTests.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Measurable conjugacy relations from vector evaluations

The two countable strong-test families recognize actual algebra conjugacy. Their measurability and the countable operator norm tests give the bounded implementer relation used for measurable selection.

  1. theorem OAI.KadisonKastler.measurableSet_conjugates_of_vector_tests line 23
  2. theorem OAI.KadisonKastler.measurableSet_bounded_conjugates_of_vector_tests line 49