OAI/Analysis/FreeWords/PositiveSupport.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.KKSpectralSupport.positive_sqrt_square line 52
  2. theorem OAI.KKSpectralSupport.positive_annihilate line 62
  3. theorem OAI.KKSpectralSupport.supportProjection_mono line 75
  4. def OAI.KKSpectralSupport.positiveCut line 98
  5. def OAI.KKSpectralSupport.negativeCut line 100
  6. def OAI.KKSpectralSupport.spectralCut line 102
  7. theorem OAI.KKSpectralSupport.positiveCut_nonneg line 104
  8. theorem OAI.KKSpectralSupport.negativeCut_nonneg line 107
  9. theorem OAI.KKSpectralSupport.spectralCut_isProjection line 110
  10. theorem OAI.KKSpectralSupport.cuts_difference line 113
  11. theorem OAI.KKSpectralSupport.cuts_product line 129
  12. theorem OAI.KKSpectralSupport.spectralCut_commute line 142
  13. theorem OAI.KKSpectralSupport.spectralCut_compression line 148
  14. theorem OAI.KKSpectralSupport.spectralCut_complement line 153
  15. theorem OAI.KKSpectralSupport.spectralCut_antitone line 158