OAI/Probability/InvariantIsing/Gaussian/GaussianQuadraticLaw.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Identification of the normalized quadratic-potential law with stdGaussian.

  1. lemma OAI.InvariantIsing.gaussianQuadratic_integral_cexp line 11
  2. lemma OAI.InvariantIsing.gaussianQuadratic_charFun line 39
  3. lemma OAI.InvariantIsing.gaussianQuadratic_potentialMeasure_eq_stdGaussian line 64