OAI/Probability/InvariantIsing/Magnetic/MagneticSlabExponentOrder.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual finite-slab inverse curvature increases with its exponent. All comparison hypotheses, including the degenerate endpoints and uniform zeroth-order coefficient bound, are discharged here.

  1. theorem OAI.InvariantIsing.magneticScalarInverseCurvature_exponent_mono line 16