OAI/Probability/InvariantIsing/Fields/PriorContactGG.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Geometric GG limits at the same joint constrained-prior contact minima. The perturbation parameters are not reselected after minimizing temperature and field, so subsequent contact inequalities refer to this same sequence.

  1. theorem OAI.InvariantIsing.priorContact_minimizers_have_GG_limit line 15