OAI/Probability/InvariantIsing/Magnetic/MagneticScaledSlab.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

The literal scaled inverse curvature used in the radial comparison. Time is physical variance; its scaling yields the coefficient αζ.

  1. lemma OAI.InvariantIsing.fieldScaleIncrements_positive line 15
  2. lemma OAI.InvariantIsing.fieldScaleIncrements_exponent_le_one line 22
  3. lemma OAI.InvariantIsing.magneticThirdRatioCap_scale line 29
  4. lemma OAI.InvariantIsing.magneticFourthRatioCap_scale line 35
  5. lemma OAI.InvariantIsing.magneticSlabPotentialCap_scale line 45
  6. def OAI.InvariantIsing.magneticScaledClosedCurvature line 50
  7. def OAI.InvariantIsing.magneticScaledClosedSlope line 55
  8. def OAI.InvariantIsing.magneticScaledClosedSecond line 60
  9. def OAI.InvariantIsing.magneticScaledClosedTime line 65
  10. lemma OAI.InvariantIsing.magneticScaledClosedCurvature_hasDerivAt_time line 70
  11. lemma OAI.InvariantIsing.magneticScaledClosedCurvature_hasDerivAt_spin line 85
  12. lemma OAI.InvariantIsing.magneticScaledClosedSlope_hasDerivAt_spin line 93
  13. lemma OAI.InvariantIsing.magneticScaledClosedCurvature_nil_initial line 101
  14. lemma OAI.InvariantIsing.magneticScaledClosedCurvature_continuousOn line 114
  15. lemma OAI.InvariantIsing.magneticScaledClosedCurvature_mem_interval line 124