OAI/Probability/InvariantIsing/Cavity/CavitySpectralMoment.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform radial moments for the actual spectral quadratic cavity law, after its remaining spin-linear tilt. No Gaussian marginal or norm bound is assumed: both are derived from the spectral data.

  1. theorem OAI.InvariantIsing.cavity_rooted_spectral_linear_moment line 16