OAI/Probability/SKRatio/Certificates/CertifiedGaussian.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKRatio.Certificate.gaussianWeight line 11
2. def OAI.SKRatio.Certificate.gaussianNormalizer line 12
3. lemma OAI.SKRatio.Certificate.gaussian_weight_factor line 14
4. lemma OAI.SKRatio.Certificate.polynomial_weight_bound line 21
5. lemma OAI.SKRatio.Certificate.polynomial_tail_bound line 30
6. lemma OAI.SKRatio.Certificate.gaussian_tail_constant line 39
7. lemma OAI.SKRatio.Certificate.integrable_weighted line 52
8. lemma OAI.SKRatio.Certificate.gaussian_truncation line 71
9. lemma OAI.SKRatio.Certificate.normalizer_bounds line 119
10. lemma OAI.SKRatio.Certificate.affine_gaussian_integral line 133