OAI/Probability/InvariantIsing/Magnetic/MagneticGaussianLaplace.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Positive weighted Gaussian Laplace transforms. This supplies spatial smoothing of the finite field without assuming additional derivatives of the terminal observable.

  1. def OAI.InvariantIsing.magneticWeightedGaussian line 16
  2. lemma OAI.InvariantIsing.magneticWeightedGaussian_exp_integrable line 19
  3. lemma OAI.InvariantIsing.magneticWeightedGaussian_mgf_analytic line 51
  4. lemma OAI.InvariantIsing.magneticGaussian_pdf_shift line 63
  5. lemma OAI.InvariantIsing.magneticGaussian_weighted_eq_laplace line 76
  6. lemma OAI.InvariantIsing.magneticGaussian_weighted_analytic line 98