OAI/Probability/InvariantIsing/Cavity/CavityTestExhaustion.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Bounded Gibbs tests pass from finite leaf restrictions to the full countable reference. Only almost-everywhere partition integrability is needed for the full Gaussian field.

  1. lemma OAI.InvariantIsing.cavity_subtype_tilted_integral line 16
  2. lemma OAI.InvariantIsing.cavity_tilted_test_norm_le line 28
  3. lemma OAI.InvariantIsing.cavity_tilted_test_restriction_tendsto line 35
  4. theorem OAI.InvariantIsing.cavity_cylinder_test_restriction_mean_tendsto line 53