OAI/Probability/InvariantIsing/Gaussian/GaussianFourthMoment.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Scalar Gaussian polynomial moments needed for the quadratic leave-one-column estimate.

  1. lemma OAI.InvariantIsing.gaussianReal_pow_integrable line 12
  2. lemma OAI.InvariantIsing.gaussianReal_second_moment line 18
  3. lemma OAI.InvariantIsing.gaussianReal_fourth_moment line 23
  4. lemma OAI.InvariantIsing.gaussianReal_square_memLp line 33
  5. lemma OAI.InvariantIsing.gaussianReal_square_variance line 37