OAI/Probability/GaussianPropeller/SmallCertificates.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.GaussianPropeller.FourCertificates.small_0 line 37
2. lemma OAI.GaussianPropeller.FourCertificates.small_1 line 57
3. lemma OAI.GaussianPropeller.FourCertificates.small_2 line 77
4. lemma OAI.GaussianPropeller.FourCertificates.small_3 line 97
5. lemma OAI.GaussianPropeller.FourCertificates.small_4 line 117
6. lemma OAI.GaussianPropeller.FourCertificates.small_5 line 137
7. lemma OAI.GaussianPropeller.FourCertificates.small_6 line 157
8. lemma OAI.GaussianPropeller.FourCertificates.small_7 line 177
9. lemma OAI.GaussianPropeller.FourCertificates.small_8 line 197
10. lemma OAI.GaussianPropeller.FourCertificates.small_9 line 217
11. lemma OAI.GaussianPropeller.FourCertificates.small_10 line 237
12. lemma OAI.GaussianPropeller.FourCertificates.small_11 line 257
13. lemma OAI.GaussianPropeller.FourCertificates.small_12 line 277
14. lemma OAI.GaussianPropeller.FourCertificates.small_13 line 297
15. lemma OAI.GaussianPropeller.FourCertificates.small_14 line 317
16. lemma OAI.GaussianPropeller.FourCertificates.small_15 line 337
17. lemma OAI.GaussianPropeller.FourCertificates.small_16 line 357
18. lemma OAI.GaussianPropeller.FourCertificates.small_17 line 377
19. lemma OAI.GaussianPropeller.FourCertificates.small_18 line 397
20. lemma OAI.GaussianPropeller.FourCertificates.small_19 line 417
21. lemma OAI.GaussianPropeller.FourCertificates.small_20 line 437
22. lemma OAI.GaussianPropeller.FourCertificates.small_21 line 457
23. lemma OAI.GaussianPropeller.FourCertificates.small_22 line 477
24. lemma OAI.GaussianPropeller.FourCertificates.small_23 line 497
25. lemma OAI.GaussianPropeller.FourCertificates.small_of_loss line 517