OAI/Probability/InvariantIsing/Arrays/TensorContactGG.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The GG subsequence is obtained from the same joint contact minima used for the temperature and field inequalities.

  1. theorem OAI.InvariantIsing.tensorContact_minimizers_have_GG_limit line 15