OAI/Probability/InvariantIsing/Cavity/CavityBaseCutoffProduct.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual perturbed base cutoff is the base Gibbs kernel reweighted by the unperturbed cavity factor, with the spatial cutoff inside the weight.

  1. theorem OAI.InvariantIsing.cavity_base_cutoff_product line 15