OAI/Probability/InvariantIsing/Magnetic/RestrictedBaseCutoffProduct.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.restricted_base_cutoff_product line 16