OAI/Probability/InvariantIsing/Magnetic/MagneticContinuationTime.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Joint variance/spatial differentiation of the actual scalar continuation. The covariance differential is left as integrals here; Gaussian integration by parts then identifies its time generator.

  1. def OAI.InvariantIsing.magneticGaussianAverageDifferential line 17
  2. theorem OAI.InvariantIsing.magneticGaussianAverageTwo_hasFDerivAt line 28
  3. theorem OAI.InvariantIsing.magneticGaussianAverage_hasFDerivAt line 91