OAI/Probability/SpanningForest/GaussianBoundedCorrection.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem336.GaussianBoundedCorrection.abs_sq_add_sub_sq_le line 13
  2. theorem OAI.Problem336.GaussianBoundedCorrection.abs_add_cube_le line 22
  3. theorem OAI.Problem336.GaussianBoundedCorrection.sq_add_le line 30
  4. theorem OAI.Problem336.GaussianBoundedCorrection.integrable_sq_add_of_bounded line 42
  5. theorem OAI.Problem336.GaussianBoundedCorrection.abs_integral_sq_add_sub_sq_le line 54
  6. theorem OAI.Problem336.GaussianBoundedCorrection.integrable_abs_cube_add_of_bounded line 76
  7. theorem OAI.Problem336.GaussianBoundedCorrection.integral_abs_cube_add_le line 89
  8. def OAI.Problem336.GaussianBoundedCorrection.standardGaussianAbsMoment line 107
  9. theorem OAI.Problem336.GaussianBoundedCorrection.standardGaussianAbsMoment_nonneg line 110
  10. theorem OAI.Problem336.GaussianBoundedCorrection.gaussian_abs_moment line 114
  11. theorem OAI.Problem336.GaussianBoundedCorrection.hasLaw_gaussian_abs_moment line 127
  12. theorem OAI.Problem336.GaussianBoundedCorrection.hasLaw_gaussian_integral_sq line 136
  13. theorem OAI.Problem336.GaussianBoundedCorrection.gaussian_bounded_correction_second_moment line 146
  14. theorem OAI.Problem336.GaussianBoundedCorrection.gaussian_bounded_correction_third_moment line 164