OAI/Probability/InvariantIsing/Magnetic/MagneticContinuationPDE.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The actual bounded continuation solves the scalar heat equation with the nonlinear backward-field drift. The first coordinate is the amount of Gaussian variance already applied; reversing it gives the backward time convention in the manuscript.

  1. lemma OAI.InvariantIsing.magneticGaussianSpaceTwo_eq line 17
  2. lemma OAI.InvariantIsing.magneticGaussianGeneratorTwo_eq line 28
  3. theorem OAI.InvariantIsing.magneticGaussianAverageTwo_hasFDerivAt_generator line 49
  4. lemma OAI.InvariantIsing.magneticGaussianSpace_eq line 66
  5. lemma OAI.InvariantIsing.magneticGaussianGenerator_eq line 72
  6. theorem OAI.InvariantIsing.magneticGaussianAverage_hasFDerivAt_generator line 81