OAI/Probability/InvariantIsing/Magnetic/MagneticContinuationGenerator.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The exact heat generator of the scalar continuation. Integration by parts removes the apparent inverse square-root singularity from the positive-variance differential.

  1. def OAI.InvariantIsing.magneticGaussianGenerator line 16
  2. lemma OAI.InvariantIsing.magneticGaussianTimeTwo_eq_generator line 22
  3. lemma OAI.InvariantIsing.magneticContinuation_secondTwo_generator line 82
  4. lemma OAI.InvariantIsing.magneticGaussianTime_eq_generator line 119
  5. lemma OAI.InvariantIsing.magneticContinuation_second_generator line 126