OAI/Analysis/FreeWords/SpectralCuts.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.KKSpectralSupport.supportProjection_of_isUnit line 76
  2. theorem OAI.KKSpectralSupport.spectralCut_eq_one line 82
  3. theorem OAI.KKSpectralSupport.spectralCut_eq_zero line 94
  4. theorem OAI.KKSpectralSupport.spectralCut_commute_of_commute line 108
  5. theorem OAI.KKSpectralSupport.projection_restrict_nonneg line 113
  6. def OAI.KKSpectralSupport.spectralBand line 124
  7. theorem OAI.KKSpectralSupport.spectralBand_isProjection line 127
  8. theorem OAI.KKSpectralSupport.spectralBand_commute line 131
  9. theorem OAI.KKSpectralSupport.spectralBand_lower line 134
  10. theorem OAI.KKSpectralSupport.spectralBand_upper line 142