OAI/Analysis/ModularRecovery/Centralizer.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Equivalence of the modular and vector-state centralizers.

  1. lemma OAI.BoundedRecovery.RealSpectralCalculus.bandMultiplier_of_fixed line 19
  2. lemma OAI.BoundedRecovery.RealSpectralCalculus.spectralSupport_of_fixed line 30
  3. lemma OAI.BoundedRecovery.RealSpectralCalculus.halfGraph_of_fixed line 68
  4. lemma OAI.BoundedRecovery.RealSpectralCalculus.fixed_of_halfGraph line 81
  5. def OAI.BoundedRecovery.StandardModularData.InStateCentralizer line 104
  6. def OAI.BoundedRecovery.StandardModularData.StateScalarCentralizer line 107
  7. lemma OAI.BoundedRecovery.StandardModularData.state_mul_inner line 110
  8. lemma OAI.BoundedRecovery.StandardModularData.fixed_mem_stateCentralizer line 114
  9. lemma OAI.BoundedRecovery.StandardModularData.stateCentralizer_fixed line 132
  10. lemma OAI.BoundedRecovery.StandardModularData.inStateCentralizer_iff_fixed line 174
  11. lemma OAI.BoundedRecovery.StandardModularData.scalarCentralizer_of_state line 179
  12. lemma OAI.BoundedRecovery.StandardModularData.scalarCentralizer_iff_state line 184