OAI/Probability/SKBarriers/Gaussian/GaussianGrowth.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SK.Analytic.HasExpGrowth.mul line 24
2. theorem OAI.SK.Analytic.HasExpGrowth.norm_id line 36
3. theorem OAI.SK.Analytic.HasExpGrowth.section_right line 42
4. theorem OAI.SK.Analytic.HasExpGrowth.integrable_gaussianMeasure line 56
5. instance OAI.SK.Analytic.fiberGaussian_isGaussian line 74
6. theorem OAI.SK.Analytic.HasExpGrowth.integrable_fiberGaussian line 80
7. def OAI.SK.Analytic.coordinateAxis line 84
8. theorem OAI.SK.Analytic.coordinateAxis_last line 88
9. theorem OAI.SK.Analytic.coordinateAxis_castSucc line 91
10. theorem OAI.SK.Analytic.HasExpGrowth.linear line 97
11. theorem OAI.SK.Analytic.HasExpGrowth.derivative_eval line 102