OAI/Probability/InvariantIsing/Magnetic/MagneticContinuationInverse.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Ordinary continuation derivatives pulled back through the actual optimizing bias. The weighted second derivative has zero boundary limits.

  1. def OAI.InvariantIsing.magneticContinuationPullback line 14
  2. def OAI.InvariantIsing.magneticContinuationPullbackFirst line 17
  3. def OAI.InvariantIsing.magneticContinuationPullbackSecond line 20
  4. lemma OAI.InvariantIsing.magneticContinuationPullback_hasDerivAt line 25
  5. lemma OAI.InvariantIsing.magneticContinuationPullbackFirst_hasDerivAt line 33
  6. lemma OAI.InvariantIsing.magneticContinuationPullback_second_deriv line 42
  7. lemma OAI.InvariantIsing.magneticContinuation_weighted_second line 52
  8. lemma OAI.InvariantIsing.magneticFieldLevel_weighted_second_endpoint line 59
  9. lemma OAI.InvariantIsing.magneticFieldLevel_weighted_second_neg_endpoint line 76