OAI/Probability/InvariantIsing/Cavity/CavityFiniteTest.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Bounded test comparison for finite spin/leaf restrictions. A common test tilt reduces comparison of Gibbs means to the covariance-only log-partition estimate and a uniform bounded-variable secant bound.

  1. lemma OAI.InvariantIsing.finite_cylinder_test_cgf_eq line 15
  2. theorem OAI.InvariantIsing.cavity_finite_test_comparison line 43