OAI/Probability/SKBarriers/Gaussian/GaussianLogStep.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SK.Analytic.norm_le_of_fderiv_bound line 24
2. theorem OAI.SK.Analytic.exp_mul_growth_of_fderiv_bound line 37
3. def OAI.SK.Analytic.positiveGaussianLogStep line 50
4. theorem OAI.SK.Analytic.positiveGaussianLogStep_partition_pos line 53