OAI/Analysis/ModularRecovery/Commutant.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The commutant core and reverse operators.

  1. lemma OAI.BoundedRecovery.RealSpectralCalculus.halfGraph_smul line 19
  2. lemma OAI.BoundedRecovery.StandardModularData.fixed_adjoint_core_approx line 27
  3. lemma OAI.BoundedRecovery.StandardModularData.commutant_tomita_graph line 40
  4. def OAI.BoundedRecovery.spectralReflection line 111
  5. lemma OAI.BoundedRecovery.spectralReflection_apply line 121
  6. lemma OAI.BoundedRecovery.spectralReflection_involutive line 124
  7. lemma OAI.BoundedRecovery.spectralReflection_halfResolvent line 127
  8. def OAI.BoundedRecovery.RealSpectralCalculus.reverse line 140
  9. lemma OAI.BoundedRecovery.RealSpectralCalculus.reverse_halfGraph line 147
  10. lemma OAI.BoundedRecovery.RealSpectralCalculus.reverse_unitary line 163
  11. lemma OAI.BoundedRecovery.StandardModularData.commutant_separating line 174
  12. def OAI.BoundedRecovery.StandardModularData.commutantData line 185