OAI/Probability/InvariantIsing/Magnetic/MagneticWeightedClosed.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Closed-strip derivative data for the weighted continuation. At either spin endpoint the continued function is identically zero in time.

  1. def OAI.InvariantIsing.closedMagneticWeightedSlope line 16
  2. def OAI.InvariantIsing.closedMagneticWeightedSecond line 21
  3. def OAI.InvariantIsing.closedMagneticWeightedPotential line 26
  4. def OAI.InvariantIsing.closedMagneticWeightedTime line 30
  5. lemma OAI.InvariantIsing.closedMagneticSlabWeighted_hasDerivAt_spin line 38
  6. lemma OAI.InvariantIsing.closedMagneticWeightedSlope_hasDerivAt_spin line 50
  7. lemma OAI.InvariantIsing.closedMagneticSlabWeighted_hasDerivAt_time line 62
  8. lemma OAI.InvariantIsing.closedMagneticWeightedPotential_bound line 77