OAI/Probability/InvariantIsing/Cavity/CavityFullProjectionMoment.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The full perturbed Gibbs law has at most unit mean squared spectral projection at every physical site. No cutoff is imposed.

  1. def OAI.InvariantIsing.cavityProjectionSiteTest line 15
  2. lemma OAI.InvariantIsing.measurable_cavityProjectionSiteTest line 19
  3. lemma OAI.InvariantIsing.cavityProjectionSiteTest_bound line 26
  4. theorem OAI.InvariantIsing.cavity_full_projection_site_mean_le_one line 33