OAI/Probability/InvariantIsing/Arrays/TensorLimitingDiagonal.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Actual diagonal-minimum fluctuations give constant limiting diagonals.

  1. def OAI.InvariantIsing.tensorMinimumArrayDiagonal line 16
  2. theorem OAI.InvariantIsing.tensorPerturbation_minimizers_constantDiagonal line 21