OAI/Probability/InvariantIsing/Magnetic/MagneticSpatialThird.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Third spatial differentiation of one actual Gaussian backward step. The formula is kept as tilted averages, so it also applies to zero variance.

  1. def OAI.InvariantIsing.fieldCurvatureTransform line 14
  2. def OAI.InvariantIsing.fieldThirdTransform line 19
  3. lemma OAI.InvariantIsing.hasDerivAt_fieldCurvatureTransform line 29
  4. lemma OAI.InvariantIsing.measurable_fieldThirdTransform line 69
  5. def OAI.InvariantIsing.fieldThirdTransformCap line 86
  6. lemma OAI.InvariantIsing.fieldThirdTransform_bound line 90