OAI/Probability/SKBarriers/Gaussian/GaussianMassDerivative.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SK.Analytic.hasDerivAt_dslope_zero_of_analytic line 13
2. theorem OAI.SK.Analytic.BoundedDerivs.integrableExpSet_section line 25
3. theorem OAI.SK.Analytic.BoundedDerivs.mem_interior_integrableExpSet_section line 31
4. theorem OAI.SK.Analytic.gaussianStep_mass_eq_dslope line 37
5. theorem OAI.SK.Analytic.gaussianStep_hasDerivAt_mass_zero line 51
6. theorem OAI.SK.Analytic.gaussianStep_hasDerivAt_mass_ne_zero line 64