OAI/Analysis/ProductSpaces/GaussianMoments.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.IndependentProducts.weighted_sum_memLp_two line 17
  2. lemma OAI.IndependentProducts.weighted_sum_mean line 24
  3. lemma OAI.IndependentProducts.weighted_sum_second_moment_le line 30
  4. lemma OAI.IndependentProducts.weighted_sum_tail line 54
  5. def OAI.IndependentProducts.gaussianVector line 80
  6. instance OAI.IndependentProducts.(instance at line 81) line 81
  7. lemma OAI.IndependentProducts.gaussian_eval_hasLaw line 83
  8. lemma OAI.IndependentProducts.gaussian_square_memLp line 86
  9. lemma OAI.IndependentProducts.gaussian_quadratic_tail line 96
  10. def OAI.IndependentProducts.excess line 121
  11. lemma OAI.IndependentProducts.excess_nonneg line 123
  12. lemma OAI.IndependentProducts.excess_midpoint line 125
  13. lemma OAI.IndependentProducts.integrable_excess line 138
  14. lemma OAI.IndependentProducts.integral_excess_independent_copy line 143
  15. lemma OAI.IndependentProducts.integral_excess_ge_tail line 162
  16. lemma OAI.IndependentProducts.gaussian_sqrt_scale line 185
  17. lemma OAI.IndependentProducts.gaussian_tail_variance_lower line 195
  18. lemma OAI.IndependentProducts.gaussian_weighted_hasLaw line 219
  19. lemma OAI.IndependentProducts.gaussian_weighted_excess line 230
  20. def OAI.IndependentProducts.gaussianVectorRotate line 245
  21. lemma OAI.IndependentProducts.measurePreserving_gaussianVectorRotate line 248
  22. lemma OAI.IndependentProducts.integrable_gaussian_bilinear line 257
  23. lemma OAI.IndependentProducts.gaussian_bilinear_excess line 265