OAI/Probability/InvariantIsing/Magnetic/MagneticSlabPDE.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The literal inverse-coordinate PDE of a finite Gaussian slab, with spatial derivatives and inverse regularity discharged. Time here denotes applied variance; reversing it gives the manuscript's backward equation.

  1. def OAI.InvariantIsing.magneticScalarSlabJet line 15
  2. lemma OAI.InvariantIsing.magneticScalarInverseCurvature_eq_jet line 23
  3. lemma OAI.InvariantIsing.magneticScalarSlabJet_curvature_pos line 31
  4. def OAI.InvariantIsing.magneticScalarInverseSlope line 38
  5. def OAI.InvariantIsing.magneticScalarInverseSecond line 44
  6. lemma OAI.InvariantIsing.magneticScalarSlabBias_hasDerivAt_jet line 50
  7. lemma OAI.InvariantIsing.magneticScalarInverseCurvature_hasDerivAt_spin line 58
  8. lemma OAI.InvariantIsing.magneticScalarInverseSlope_hasDerivAt line 69
  9. lemma OAI.InvariantIsing.magneticScalarInverse_second_deriv line 84
  10. theorem OAI.InvariantIsing.magneticScalarInverseCurvature_PDE line 95

    Source documentation

    The actual inverse curvature solves the forward-variance version of mag:inverse-PDE on every positive-variance slab.

    theorem magneticScalarInverseCurvature_PDE (L : List (ℝ × ℝ≥0))
    (hL : ∀ av ∈ L, 0 < av.1) {ζ s v : ℝ}
    (hζ : 0 ≤ ζ) (hs : |s| < 1) (hv : 0 < v) :
    HasDerivAt (fun t => magneticScalarInverseCurvature L hL ζ t s)
      ((magneticScalarInverseCurvature L hL ζ v s) ^ 2 / 2 *
        deriv (deriv (magneticScalarInverseCurvature L hL ζ v)) s +
        ζ * (magneticScalarInverseCurvature L hL ζ v s) ^ 2) v := by
…

    Mentions: OAI.InvariantIsing.magneticScalarInverseCurvature