OAI/Analysis/KadisonKastler/IsometryGraphShift.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The adjoint isometry step in the modular graph shift

The adjoints of the constructed coisometries supply the positive-eigenvalue case of Marrakchi's Lemma 4.2.

  1. theorem OAI.KadisonKastler.coisometry_adjoint_isometry line 21
  2. theorem OAI.KadisonKastler.ModularConjugationData.isometry_graph_shift_identity line 32
  3. theorem OAI.KadisonKastler.ModularConjugationData.isometry_graph_shift_bound line 43
  4. theorem OAI.KadisonKastler.ModularConjugationData.isometry_coefficient_identity line 54
  5. theorem OAI.KadisonKastler.ModularConjugationData.isometry_coefficient_tendsto line 73
  6. theorem OAI.KadisonKastler.ModularConjugationData.exists_isometry_graph_shift line 89