OAI/Probability/InvariantIsing/Spectral/SelectedSpectralPressure.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

No-outlier spectral pressure along selected dimensions, used in the subsequence proof of convergence in probability.

  1. lemma OAI.InvariantIsing.selected_clip_empirical_tendsto line 13
  2. theorem OAI.InvariantIsing.selected_spectral_pressure_tendsto line 35