OAI/Probability/InvariantIsing/Magnetic/MagneticScaledContinuation.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The actual square continuation in the rescaled physical variance. Its diffusion coefficient is the rescaled inverse curvature.

  1. def OAI.InvariantIsing.magneticScaledSquareJet line 15
  2. def OAI.InvariantIsing.magneticScaledSquareContinuation line 22
  3. def OAI.InvariantIsing.magneticScaledSquareSlope line 28
  4. def OAI.InvariantIsing.magneticScaledSquareSecond line 35
  5. def OAI.InvariantIsing.magneticScaledSquareTime line 42
  6. lemma OAI.InvariantIsing.magneticScaledSquareContinuation_continuousOn line 48
  7. lemma OAI.InvariantIsing.magneticScaledSquareContinuation_hasDerivAt_time line 59
  8. lemma OAI.InvariantIsing.magneticScaledSquareContinuation_hasDerivAt_spin line 75
  9. lemma OAI.InvariantIsing.magneticScaledSquareSlope_hasDerivAt_spin line 84
  10. lemma OAI.InvariantIsing.magneticScaledSquareSecond_nonneg line 93