OAI/Analysis/IrrationalRotation/Model/SpectralCutoff.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Invariant233.WeightedShift.SpectralCutoff.boundedWeight line 13
  2. def OAI.Invariant233.WeightedShift.SpectralCutoff.boundedOperator line 17
  3. def OAI.Invariant233.WeightedShift.SpectralCutoff.window line 24
  4. def OAI.Invariant233.WeightedShift.SpectralCutoff.symbol line 26
  5. theorem OAI.Invariant233.WeightedShift.SpectralCutoff.norm_symbol_le line 28
  6. def OAI.Invariant233.WeightedShift.SpectralCutoff.projection line 34
  7. def OAI.Invariant233.WeightedShift.SpectralCutoff.productSymbol line 40
  8. def OAI.Invariant233.WeightedShift.SpectralCutoff.inverseSymbol line 42
  9. theorem OAI.Invariant233.WeightedShift.SpectralCutoff.norm_productSymbol_le line 44
  10. theorem OAI.Invariant233.WeightedShift.SpectralCutoff.norm_inverseSymbol_le line 52
  11. def OAI.Invariant233.WeightedShift.SpectralCutoff.productOperator line 61
  12. def OAI.Invariant233.WeightedShift.SpectralCutoff.inverseOperator line 68
  13. def OAI.Invariant233.WeightedShift.SpectralCutoff.cutoffSpace line 75
  14. instance OAI.Invariant233.WeightedShift.SpectralCutoff.cutoffSpace_hasOrthogonalProjection line 78