OAI/Probability/SKGap/Gaussian/LocalGaussianMoments.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SKGap.matrix_fourth_sum_integrable line 13
  2. lemma OAI.SKGap.matrix_fourth_sum_mean line 20
  3. lemma OAI.SKGap.matrix_fourth_sum_bound line 29
  4. lemma OAI.SKGap.matrix_norm_fourth_integrable line 40
  5. lemma OAI.SKGap.matrix_norm_fourth_bound line 53
  6. theorem OAI.SKGap.localGaussian_fourth_moments line 64
  7. lemma OAI.SKGap.gaussian_vectorSqNorm_integrable line 91
  8. lemma OAI.SKGap.gaussian_vectorSqNorm_mean line 98
  9. def OAI.SKGap.localGaussianBall line 104
  10. lemma OAI.SKGap.localGaussianBall_measurable line 106
  11. lemma OAI.SKGap.localGaussianBall_norm line 110
  12. theorem OAI.SKGap.localGaussianBall_probability line 116
  13. lemma OAI.SKGap.localGaussianBall_ne_zero line 133
  14. lemma OAI.SKGap.integrable_cond_of_integrable line 140
  15. lemma OAI.SKGap.integral_cond_nonneg_le_two line 145