OAI/Probability/InvariantIsing/Magnetic/MagneticGaussianSmoothing.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Positive-variance scalar Gaussian transitions are smooth in the spatial coordinate even when the bounded terminal test has no derivatives. This justifies the interior fourth derivatives in the inverse-mean parabolic comparison.

  1. lemma OAI.InvariantIsing.analyticAt_fieldSpinTransition_nonneg line 17
  2. lemma OAI.InvariantIsing.analyticAt_fieldSpinTransition line 38
  3. lemma OAI.InvariantIsing.contDiff_fieldSpinTransition line 60