OAI/Probability/InvariantIsing/Magnetic/MagneticSpatialFourth.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Fourth spatial differentiation of the actual Gaussian field step. The derivative is expressed in bounded tilted averages; no positive-variance assumption is needed.

  1. def OAI.InvariantIsing.fieldTiltSpatial line 15
  2. lemma OAI.InvariantIsing.measurable_fieldTiltSpatial line 20
  3. def OAI.InvariantIsing.fieldFourthTransform line 28
  4. lemma OAI.InvariantIsing.hasDerivAt_fieldThirdTransform line 41
  5. lemma OAI.InvariantIsing.measurable_fieldFourthTransform line 137
  6. def OAI.InvariantIsing.MagneticUniformBound line 162
  7. lemma OAI.InvariantIsing.magnetic_uniform_const line 165
  8. lemma OAI.InvariantIsing.magnetic_uniform_add line 168
  9. lemma OAI.InvariantIsing.magnetic_uniform_sub line 176
  10. lemma OAI.InvariantIsing.magnetic_uniform_mul line 184
  11. lemma OAI.InvariantIsing.fieldFourthTransform_bounded line 193