OAI/Analysis/KadisonKastler/TomitaResolventFaithful.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Faithfulness of the bounded Tomita graph resolvent

Both endpoints of the positive contraction have zero eigenspace. This is the bounded starting point for recovering the modular operator by spectral calculus.

  1. theorem OAI.KadisonKastler.inner_tupleSingle_left line 20
  2. theorem OAI.KadisonKastler.tupleSingle_adjoint line 25
  3. theorem OAI.KadisonKastler.graphResolvent_eq_compression line 33
  4. theorem OAI.KadisonKastler.graphResolvent_positive line 40
  5. theorem OAI.KadisonKastler.graphResolvent_norm_le_one line 48
  6. theorem OAI.KadisonKastler.graphResolvent_eq_zero_iff line 53