OAI/Probability/InvariantIsing/Magnetic/MagneticCompactPartition.lean
2 declarations, 0 contain sorry, 0 declared as axioms
Positive spectral partition bounds for the finite-field pressure.
- lemma
OAI.InvariantIsing.CompactSpectralPartition.field_pressure_tendstoline 13 - lemma
OAI.InvariantIsing.CompactSpectralPartition.mean_field_pressure_boundsline 37