OAI/Probability/GaussianPropeller/ConeConcavity.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.GaussianPropeller.EhrhardCone.cone line 30
  2. def OAI.GaussianPropeller.EhrhardCone.shifted line 31
  3. def OAI.GaussianPropeller.EhrhardCone.prob line 32
  4. lemma OAI.GaussianPropeller.EhrhardCone.measurableSet_shifted line 35
  5. lemma OAI.GaussianPropeller.EhrhardCone.gaussian_open_pos line 41
  6. lemma OAI.GaussianPropeller.EhrhardCone.prob_mem line 50
  7. lemma OAI.GaussianPropeller.EhrhardCone.gaussian_hyperplane_null line 78
  8. lemma OAI.GaussianPropeller.EhrhardCone.ae_no_boundary line 97
  9. lemma OAI.GaussianPropeller.EhrhardCone.cdf_softmin_limit line 111
  10. lemma OAI.GaussianPropeller.EhrhardCone.prob_limit line 124
  11. lemma OAI.GaussianPropeller.EhrhardCone.quantile_prob_concave line 147
  12. lemma OAI.GaussianPropeller.Quantile.Φ_eq_gaussianReal line 170
  13. lemma OAI.GaussianPropeller.Quantile.integrable_mul_φ line 178
  14. lemma OAI.GaussianPropeller.Quantile.tendsto_φ_atBot line 187
  15. lemma OAI.GaussianPropeller.Quantile.left_first_moment line 196
  16. lemma OAI.GaussianPropeller.Quantile.integral_positive_cdf line 204
  17. lemma OAI.GaussianPropeller.Quantile.tail_integrable line 222
  18. lemma OAI.GaussianPropeller.Quantile.integral_cdf_tail line 231
  19. lemma OAI.GaussianPropeller.EhrhardCone.measurableSet_cone line 262
  20. lemma OAI.GaussianPropeller.EhrhardCone.prob_zero line 266
  21. lemma OAI.GaussianPropeller.EhrhardCone.prob_line_deriv line 269
  22. lemma OAI.GaussianPropeller.EhrhardCone.prob_tangent line 284
  23. lemma OAI.GaussianPropeller.EhrhardCone.integral_prob_upper line 306