OAI/Probability/InvariantIsing/Magnetic/MagneticFiniteTemplateLower.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The full rational magnetization supremum is a lower bound for physical pressure whenever the spectral and field populations have a finite template.

  1. theorem OAI.InvariantIsing.finite_template_magnetic_pressure_lower line 14