OAI/Probability/InvariantIsing/Magnetic/MagneticContinuationComparison.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Increasing the inverse-curvature coefficient increases a convex continued observable. This is the comparison used for conditional square means.

  1. theorem OAI.InvariantIsing.magnetic_continuation_coefficient_comparison line 14