OAI/Probability/InvariantIsing/Magnetic/MagneticSlabContinuation.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Actual bounded observables continued in the inverse mean coordinate. Both spatial derivatives and the drift cancellation follow from the finite Gaussian field, with no inverse-regularity assumptions left over.

  1. def OAI.InvariantIsing.magneticScalarSlabContinuation line 16
  2. def OAI.InvariantIsing.magneticScalarSlabContinuationJet line 21
  3. lemma OAI.InvariantIsing.magneticScalarSlabContinuation_eq_jet line 29
  4. def OAI.InvariantIsing.magneticScalarSlabContinuationSlope line 36
  5. def OAI.InvariantIsing.magneticScalarSlabContinuationSecond line 43
  6. lemma OAI.InvariantIsing.magneticScalarSlabContinuation_hasDerivAt_spin line 50
  7. lemma OAI.InvariantIsing.magneticScalarSlabContinuationSlope_hasDerivAt line 63
  8. lemma OAI.InvariantIsing.magneticScalarSlabContinuation_second_deriv line 77
  9. theorem OAI.InvariantIsing.magneticScalarSlabContinuation_PDE line 87