OAI/Probability/SKBarriers/Gaussian/GaussianSecondStep.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SK.Analytic.fderiv_fderiv_const_mul line 28
2. theorem OAI.SK.Analytic.BoundedDerivs.exp_growths line 36
3. theorem OAI.SK.Analytic.fderiv_fderiv_gaussianStep_nonzero line 47
4. theorem OAI.SK.Analytic.fderiv_fderiv_gaussianStep_zero line 68
5. theorem OAI.SK.Analytic.integrable_exp_smul_of_bounded line 80