OAI/Probability/InvariantIsing/Magnetic/MagneticSlabClosedDerivatives.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Closed-spin-interval derivatives of the finite slab. The two endpoints are constant zero in time, while all spatial derivatives are used only in the open spin interval.

  1. def OAI.InvariantIsing.closedMagneticScalarSlope line 16
  2. def OAI.InvariantIsing.closedMagneticScalarSecond line 20
  3. def OAI.InvariantIsing.closedMagneticScalarTime line 24
  4. lemma OAI.InvariantIsing.closedMagneticScalarCurvature_hasDerivAt_spin line 29
  5. lemma OAI.InvariantIsing.closedMagneticScalarSlope_hasDerivAt_spin line 40
  6. lemma OAI.InvariantIsing.closedMagneticScalarCurvature_hasDerivAt_time line 51
  7. lemma OAI.InvariantIsing.closedMagneticScalarCurvature_endpoints line 64
  8. lemma OAI.InvariantIsing.closedMagneticScalarCurvature_le_one line 71
  9. lemma OAI.InvariantIsing.closedMagneticScalarCurvature_weighted_second_bound line 78
  10. lemma OAI.InvariantIsing.closedMagneticScalarCurvature_initial line 90