OAI/Probability/InvariantIsing/Magnetic/MagneticInwardApproximation.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Rational approximation toward zero improves the constrained entropy. This avoids a height-dependent continuity estimate for the magnetic profile.

  1. lemma OAI.InvariantIsing.constrainedFieldValue_antitone_nonneg line 13
  2. lemma OAI.InvariantIsing.constrainedFieldValue_abs line 26
  3. lemma OAI.InvariantIsing.constrainedFieldValue_le_of_abs_le line 32
  4. lemma OAI.InvariantIsing.exists_inward_rat_close line 38
  5. lemma OAI.InvariantIsing.magneticVariational_inward_mono line 62