OAI/Probability/InvariantIsing/Magnetic/RationalConstrainedMinima.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Actual compact minimizers of each physical rational product-constraint objective.

  1. theorem OAI.InvariantIsing.rational_constrained_minimizers_exist line 11