OAI/Analysis/ModularRecovery/TomitaFundamental.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Closed Tomita relations and bounded transforms.

  1. def OAI.BoundedRecovery.modularEnergy line 18
  2. lemma OAI.BoundedRecovery.RealSpectralCalculus.halfGraph_energy_identity line 23
  3. lemma OAI.BoundedRecovery.StandardModularData.core_halfGraph line 54
  4. def OAI.BoundedRecovery.vectorStateLM line 66
  5. lemma OAI.BoundedRecovery.vectorState_star_mul line 71
  6. lemma OAI.BoundedRecovery.re_vectorState_mono line 79
  7. lemma OAI.BoundedRecovery.vonNeumannAlgebra_isClosed line 86
  8. lemma OAI.BoundedRecovery.polarCutoff_mem line 98
  9. lemma OAI.BoundedRecovery.cutoffLeft_mem line 105
  10. lemma OAI.BoundedRecovery.vectorState_mul_star line 112
  11. lemma OAI.BoundedRecovery.cutoffRight_vector_loss line 116
  12. lemma OAI.BoundedRecovery.cutoffLeft_vector_loss line 122
  13. lemma OAI.BoundedRecovery.cutoff_cross_term line 129
  14. lemma OAI.BoundedRecovery.cutoff_energy_le line 154
  15. def OAI.BoundedRecovery.operatorOrbit line 168
  16. lemma OAI.BoundedRecovery.operatorOrbit_invariant line 178
  17. lemma OAI.BoundedRecovery.commutant_cyclic line 185
  18. def OAI.BoundedRecovery.operatorEvaluation line 211
  19. lemma OAI.BoundedRecovery.bounded_orbit_lift line 216
  20. lemma OAI.BoundedRecovery.isClosed_bounded_orbit line 261
  21. lemma OAI.BoundedRecovery.StandardModularData.fundamental_resolvent_lift line 271