OAI/Analysis/KadisonKastler/NormPreservingGraphShift.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Remote graph shifts with exact preservation of the relevant vector norm

  1. theorem OAI.KadisonKastler.ModularConjugationData.exists_coisometry_test_shift line 21
  2. theorem OAI.KadisonKastler.ModularConjugationData.exists_isometry_test_shift line 48