OAI/Probability/InvariantIsing/Arrays/TensorMinimizerDiagonal.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Actual minimizers have compact-centered spectral diagonal fluctuations.

  1. theorem OAI.InvariantIsing.tensorPerturbation_minimizers_diagonal_bound line 15