OAI/Probability/GaussianPropeller/QuantileCalculus.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.GaussianPropeller.QuantilePDE.quantile_fderiv line 24
2. lemma OAI.GaussianPropeller.QuantilePDE.quantile_gradient_line_derivative line 30
3. lemma OAI.GaussianPropeller.QuantilePDE.trace_quantile_hessian line 55
4. lemma OAI.GaussianPropeller.SmoothCDF.abs_mul_φ_le line 69
5. def OAI.GaussianPropeller.SmoothCDF.grad line 80
6. def OAI.GaussianPropeller.SmoothCDF.hess line 81
7. lemma OAI.GaussianPropeller.SmoothCDF.fderiv line 84
8. lemma OAI.GaussianPropeller.SmoothCDF.grad_fderiv line 90
9. lemma OAI.GaussianPropeller.SmoothCDF.continuous_hess line 101
10. lemma OAI.GaussianPropeller.SmoothCDF.cdf_bound line 108
11. lemma OAI.GaussianPropeller.SmoothCDF.grad_bound line 112
12. lemma OAI.GaussianPropeller.SmoothCDF.hess_bound line 117