OAI/Probability/InvariantIsing/Cavity/CavityBoundedSecant.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Bounded Gibbs tests can be compared through logarithmic generating functions. Hoeffding's bound makes the finite-difference error uniform over the reference probability, including cavity cutoffs.

  1. lemma OAI.InvariantIsing.cavity_bounded_cgf_secant line 16
  2. lemma OAI.InvariantIsing.cavity_secant_comparison_algebra line 45
  3. theorem OAI.InvariantIsing.cavity_bounded_random_test_compare line 60