OAI/Probability/GaussianPropeller/LossCertificates.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.GaussianPropeller.FourCertificates.large_25 line 37
2. lemma OAI.GaussianPropeller.FourCertificates.large_26 line 57
3. lemma OAI.GaussianPropeller.FourCertificates.large_27 line 77
4. lemma OAI.GaussianPropeller.FourCertificates.large_28 line 97
5. lemma OAI.GaussianPropeller.FourCertificates.large_29 line 117
6. lemma OAI.GaussianPropeller.FourCertificates.large_30 line 137
7. lemma OAI.GaussianPropeller.FourCertificates.large_31 line 157
8. lemma OAI.GaussianPropeller.FourCertificates.large_32 line 177
9. lemma OAI.GaussianPropeller.FourCertificates.large_33 line 197
10. lemma OAI.GaussianPropeller.FourCertificates.large_34 line 217
11. lemma OAI.GaussianPropeller.FourCertificates.large_35 line 237
12. lemma OAI.GaussianPropeller.FourCertificates.large_36 line 257
13. lemma OAI.GaussianPropeller.FourCertificates.large_37 line 277
14. lemma OAI.GaussianPropeller.FourCertificates.large_38 line 297
15. lemma OAI.GaussianPropeller.FourCertificates.large_39 line 317
16. lemma OAI.GaussianPropeller.FourCertificates.large_40 line 337
17. lemma OAI.GaussianPropeller.FourCertificates.large_41 line 357
18. lemma OAI.GaussianPropeller.FourCertificates.large_42 line 377
19. lemma OAI.GaussianPropeller.FourCertificates.large_43 line 397
20. lemma OAI.GaussianPropeller.FourCertificates.large_44 line 417
21. lemma OAI.GaussianPropeller.FourCertificates.large_45 line 437
22. lemma OAI.GaussianPropeller.FourCertificates.large_46 line 457
23. lemma OAI.GaussianPropeller.FourCertificates.large_47 line 477
24. lemma OAI.GaussianPropeller.FourCertificates.large_48 line 497
25. lemma OAI.GaussianPropeller.FourCertificates.large_49 line 517
26. lemma OAI.GaussianPropeller.FourCertificates.large_of_loss line 537