OAI/Probability/InvariantIsing/Cavity/CavitySpectralDensityIntegral.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Integrals of the spectral-group density on the root interval, finite overlap gaps, and ordinary terminal residual.

  1. lemma OAI.InvariantIsing.integral_spectralPathDensity_root line 18
  2. lemma OAI.InvariantIsing.integral_spectralPathDensity_gap line 33
  3. lemma OAI.InvariantIsing.integral_spectralPathDensity_tail line 68