OAI/Probability/InvariantIsing/Cavity/CavityFirstEnergyMoment.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A quadratic spatial bound needs only the second tilted radial moment when removing the cap from bounded spin tests.

  1. lemma OAI.InvariantIsing.cavity_growth_first_moment line 13
  2. theorem OAI.InvariantIsing.cavity_random_first_energy_moment line 28