OAI/Probability/InvariantIsing/Magnetic/MagneticGaussianMoments.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Integrable moments and the scaled Gaussian integration-by-parts identity used to turn the variance differential of a bounded continuation into its parabolic generator.

  1. lemma OAI.InvariantIsing.magnetic_tilted_shift_integrable line 15
  2. lemma OAI.InvariantIsing.magnetic_tilted_linear_integrable line 29
  3. lemma OAI.InvariantIsing.magnetic_tilted_scaled_test_ibp line 47