OAI/Analysis/KadisonKastler/CoisometryGraphShift.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The coisometry step in the modular graph shift

These are the bounded identities underlying the negative-eigenvalue case of Marrakchi, arXiv:1811.10253v2, Lemma 4.2. The identities require neither spectral approximation nor state decomposition.

  1. theorem OAI.KadisonKastler.ModularConjugationData.coisometry_graph_shift_identity line 22
  2. theorem OAI.KadisonKastler.ModularConjugationData.coisometry_graph_shift_bound line 33
  3. theorem OAI.KadisonKastler.ModularConjugationData.coisometry_coefficient_identity line 42