OAI/Probability/InvariantIsing/Magnetic/MagneticTailComparison.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Finite-tail comparison with initial inverse-curvature order. The analytic comparison hypotheses are derived from the actual Gaussian recursions, leaving only the initial orders for use in a finite induction.

  1. theorem OAI.InvariantIsing.magneticClosedCurvature_compare_initial line 18
  2. theorem OAI.InvariantIsing.magneticClosedSquare_compare_initial line 56