OAI/Probability/GaussianPropeller/LargeCertificates.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.GaussianPropeller.FourCertificates.large_0 line 37
  2. lemma OAI.GaussianPropeller.FourCertificates.large_1 line 57
  3. lemma OAI.GaussianPropeller.FourCertificates.large_2 line 77
  4. lemma OAI.GaussianPropeller.FourCertificates.large_3 line 97
  5. lemma OAI.GaussianPropeller.FourCertificates.large_4 line 117
  6. lemma OAI.GaussianPropeller.FourCertificates.large_5 line 137
  7. lemma OAI.GaussianPropeller.FourCertificates.large_6 line 157
  8. lemma OAI.GaussianPropeller.FourCertificates.large_7 line 177
  9. lemma OAI.GaussianPropeller.FourCertificates.large_8 line 197
  10. lemma OAI.GaussianPropeller.FourCertificates.large_9 line 217
  11. lemma OAI.GaussianPropeller.FourCertificates.large_10 line 237
  12. lemma OAI.GaussianPropeller.FourCertificates.large_11 line 257
  13. lemma OAI.GaussianPropeller.FourCertificates.large_12 line 277
  14. lemma OAI.GaussianPropeller.FourCertificates.large_13 line 297
  15. lemma OAI.GaussianPropeller.FourCertificates.large_14 line 317
  16. lemma OAI.GaussianPropeller.FourCertificates.large_15 line 337
  17. lemma OAI.GaussianPropeller.FourCertificates.large_16 line 357
  18. lemma OAI.GaussianPropeller.FourCertificates.large_17 line 377
  19. lemma OAI.GaussianPropeller.FourCertificates.large_18 line 397
  20. lemma OAI.GaussianPropeller.FourCertificates.large_19 line 417
  21. lemma OAI.GaussianPropeller.FourCertificates.large_20 line 437
  22. lemma OAI.GaussianPropeller.FourCertificates.large_21 line 457
  23. lemma OAI.GaussianPropeller.FourCertificates.large_22 line 477
  24. lemma OAI.GaussianPropeller.FourCertificates.large_23 line 497
  25. lemma OAI.GaussianPropeller.FourCertificates.large_24 line 517