OAI/Probability/InvariantIsing/Spectral/SpectralClipping.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Clipping the finite spectra to the limiting support interval.

  1. def OAI.InvariantIsing.spectralClip line 14
  2. lemma OAI.InvariantIsing.continuous_spectralClip line 16
  3. lemma OAI.InvariantIsing.spectralClip_mem line 19
  4. lemma OAI.InvariantIsing.spectralClip_eq line 22
  5. lemma OAI.InvariantIsing.spectralClip_close line 25
  6. lemma OAI.InvariantIsing.spectral_clip_empirical_tendsto line 38
  7. lemma OAI.InvariantIsing.spectral_clip_mean_pressure_close line 60