OAI/Probability/InvariantIsing/Gaussian/GaussianNormMoments.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Exact variance gives the second-moment upper bound needed for Gaussian Gram tails.

  1. theorem OAI.InvariantIsing.gaussianPatternSingularMax_mean_le line 10
  2. lemma OAI.InvariantIsing.gaussianPatternSingularMax_mean_nonneg line 29
  3. lemma OAI.InvariantIsing.gaussianPatternSingularMax_sq_integral_le line 33
  4. lemma OAI.InvariantIsing.gaussianPatternSingularMax_upper_tail line 45