OAI/Probability/InvariantIsing/Arrays/TensorLimitExistence.lean
1 declarations, 0 contain sorry, 0 declared as axioms
Actual finite perturbation minima admit limiting GG arrays with constant diagonals.
- theorem
OAI.InvariantIsing.tensorPerturbation_minimizers_have_GG_limitline 14