OAI/Probability/InvariantIsing/Fields/FieldFiniteLocal.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A local Gaussian domination envelope for the finite vector of field heights. Its constants are uniform over a neighborhood of the height vector and the spatial field.

  1. lemma OAI.InvariantIsing.FieldFiniteFamily.local_envelope line 18