OAI/Analysis/WeakInfiniteness/SpectralWindows.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WeakPureInfiniteness.spectralTent line 26
  2. lemma OAI.WeakPureInfiniteness.spectralTent_continuous line 28
  3. lemma OAI.WeakPureInfiniteness.spectralTent_nonneg line 31
  4. lemma OAI.WeakPureInfiniteness.spectralTent_center line 33
  5. lemma OAI.WeakPureInfiniteness.spectralTent_zero line 36
  6. def OAI.WeakPureInfiniteness.spectralPlateau line 42
  7. lemma OAI.WeakPureInfiniteness.spectralPlateau_continuous line 44
  8. lemma OAI.WeakPureInfiniteness.spectralPlateau_one line 47
  9. lemma OAI.WeakPureInfiniteness.spectralPlateau_zero line 53
  10. lemma OAI.WeakPureInfiniteness.continuouslySupported_cfc line 62
  11. lemma OAI.WeakPureInfiniteness.continuouslySupported_hereditary line 87
  12. lemma OAI.WeakPureInfiniteness.cfc_nonzero_of_spectral_value line 98
  13. lemma OAI.WeakPureInfiniteness.cfc_mem_of_zero line 107
  14. lemma OAI.WeakPureInfiniteness.exists_nonzero_spectral_value line 112