OAI/Probability/InvariantIsing/Magnetic/MagneticParabolicNegative.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Comparison only needs a bound for the zeroth-order coefficient on the negative set of the proposed difference. This avoids division estimates between two different inverse curvatures at the degenerate endpoints.

  1. lemma OAI.InvariantIsing.parabolic_minimum_nonneg_bounded_on_negative line 15
  2. lemma OAI.InvariantIsing.inverse_curvature_difference_coefficient_bound line 42