OAI/Probability/GaussianPropeller/CapCertificates.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.GaussianPropeller.FourCertificates.affine line 36
2. lemma OAI.GaussianPropeller.FourCertificates.cap_envelope line 38
3. lemma OAI.GaussianPropeller.FourCertificates.affine_cap_poly_0 line 45
4. lemma OAI.GaussianPropeller.FourCertificates.affine_cap_poly_1 line 54
5. lemma OAI.GaussianPropeller.FourCertificates.affine_cap_poly_2 line 63
6. lemma OAI.GaussianPropeller.FourCertificates.affine_cap_poly_3 line 72
7. lemma OAI.GaussianPropeller.FourCertificates.affine_cap_poly_4 line 81
8. lemma OAI.GaussianPropeller.FourCertificates.affine_from_cap line 90
9. lemma OAI.GaussianPropeller.FourCertificates.quartic_cap_poly_0 line 107
10. lemma OAI.GaussianPropeller.FourCertificates.quartic_cap_poly_1 line 116
11. lemma OAI.GaussianPropeller.FourCertificates.quartic_cap_poly_2 line 125
12. lemma OAI.GaussianPropeller.FourCertificates.quartic_from_cap line 134
13. lemma OAI.GaussianPropeller.FourCertificates.large_cap_poly_0 line 147
14. lemma OAI.GaussianPropeller.FourCertificates.large_from_cap line 156