OAI/Probability/SKBarriers/Gaussian/ExponentialAverage.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.SK.Analytic.HasExpGrowth.gaussian_integralline 19 - theorem
OAI.SK.Analytic.gaussianAverage_exp_representationline 42 - theorem
OAI.SK.Analytic.gaussianAverage_expGrowthline 53 - theorem
OAI.SK.Analytic.gaussianAverage_continuous_of_expGrowthline 61 - theorem
OAI.SK.Analytic.hierarchyPathWeight_expGrowthline 76 - theorem
OAI.SK.Analytic.hierarchyPath_exp_integrableline 84