OAI/Probability/SKBarriers/Gaussian/GaussianZeroMass.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SK.Analytic.growth_of_fderiv_bound line 26
2. theorem OAI.SK.Analytic.BoundedDerivs.gaussian_integral line 40
3. theorem OAI.SK.Analytic.gaussian_integral_convex line 64
4. def OAI.SK.Analytic.gaussianStep line 81
5. def OAI.SK.Analytic.RegularConvex line 84
6. theorem OAI.SK.Analytic.RegularConvex.gaussianStep line 86