OAI/Probability/InvariantIsing/Cavity/CavityFiniteTestComparison.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

On a fixed geometric cutoff, the full perturbed model and the base model tilted by the unperturbed cavity energy have the same bounded replica tests up to explicit vanishing perturbation errors.

  1. theorem OAI.InvariantIsing.cavity_finite_cutoff_test_comparison line 16