OAI/Probability/FreeIsing/Brownian/DriftMoments.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.standardGaussianThirdMoment line 13
  2. theorem OAI.Problem367.standardGaussianThirdMoment_nonneg line 16
  3. theorem OAI.Problem367.integrable_standardGaussian_abs_pow line 19
  4. theorem OAI.Problem367.standardGaussianThirdMoment_le line 27
  5. theorem OAI.Problem367.gaussianReal_map_sqrt_mul line 40
  6. theorem OAI.Problem367.integrable_gaussianReal_abs_pow line 48
  7. theorem OAI.Problem367.integral_gaussianReal_abs_pow line 56
  8. theorem OAI.Problem367.integral_abs_cube_of_gaussianLaw line 63
  9. theorem OAI.Problem367.abs_sq_sub_sq_le_of_abs_sub_le line 75
  10. theorem OAI.Problem367.integral_abs_sq_sub_sq_le line 91
  11. theorem OAI.Problem367.integral_abs_cube_le_of_bounded_perturbation line 122
  12. theorem OAI.Problem367.integrable_abs_pow_of_gaussianLaw line 147
  13. theorem OAI.Problem367.preBrownian_hasLaw_increment line 155
  14. theorem OAI.Problem367.preBrownian_integral_abs_increment_cube line 161
  15. theorem OAI.Problem367.preBrownian_bounded_drift_increment_moments line 170