OAI/Probability/SKBarriers/Gaussian/LocalGaussian.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SK.Analytic.GaussianLocallyDominated line 15
2. theorem OAI.SK.Analytic.GaussianLocallyDominated.of_norm_le line 20
3. theorem OAI.SK.Analytic.HasExpGrowth.locallyDominated line 33
4. theorem OAI.SK.Analytic.GaussianLocallyDominated.integrable_section line 36
5. theorem OAI.SK.Analytic.GaussianLocallyDominated.clm line 45
6. theorem OAI.SK.Analytic.GaussianLocallyDominated.continuous_integral line 50
7. theorem OAI.SK.Analytic.hasFDerivAt_local_gaussian_integral line 70
8. theorem OAI.SK.Analytic.contDiff_two_local_gaussian_integral line 91
9. theorem OAI.SK.Analytic.contDiff_two_local_gaussian_integral_fderiv line 107