OAI/Probability/InvariantIsing/Spectral/SpectralCountEndpoint.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Endpoint derivative bounds for changing spectral multiplicities. The fraction estimate uses the actual Haar Gibbs projection masses.

  1. lemma OAI.InvariantIsing.integrable_gibbsSpectralDirection line 15
  2. lemma OAI.InvariantIsing.integral_gibbsSpectralDirection line 36
  3. lemma OAI.InvariantIsing.abs_integral_gibbsSpectralDirection_le line 59