OAI/Probability/SKRatio/Matrices/GaussianQuadratic.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SKRatioGaussian.gaussian_integrable_pow line 55
  2. lemma OAI.SKRatioGaussian.gaussian_memLp_sq line 61
  3. lemma OAI.SKRatioGaussian.gaussian_integral_sq line 65
  4. lemma OAI.SKRatioGaussian.gaussian_integral_fourth line 70
  5. lemma OAI.SKRatioGaussian.gaussian_variance_sq line 80
  6. def OAI.SKRatioGaussian.gaussianQuadratic line 88
  7. lemma OAI.SKRatioGaussian.gaussianQuadratic_memLp line 90
  8. lemma OAI.SKRatioGaussian.gaussianQuadratic_mean line 97
  9. lemma OAI.SKRatioGaussian.gaussianQuadratic_variance line 114
  10. lemma OAI.SKRatioGaussian.sqrt_sub_sq_le_abs_sub line 129
  11. lemma OAI.SKRatioGaussian.memLp_sqrt_of_nonneg line 145
  12. lemma OAI.SKRatioGaussian.integral_abs_le_sqrt_sq line 151
  13. theorem OAI.SKRatioGaussian.integral_sqrt_fluctuation line 162