OAI/Probability/GaussianPropeller/QuarticCertificates.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.GaussianPropeller.FourCertificates.loss_bound line 38
  2. lemma OAI.GaussianPropeller.FourCertificates.loss_row line 44
  3. def OAI.GaussianPropeller.FourCertificates.quartic line 72
  4. def OAI.GaussianPropeller.FourCertificates.small line 73
  5. def OAI.GaussianPropeller.FourCertificates.large line 74
  6. lemma OAI.GaussianPropeller.FourCertificates.quartic_mono line 76
  7. lemma OAI.GaussianPropeller.FourCertificates.small_mono line 81
  8. lemma OAI.GaussianPropeller.FourCertificates.large_mono line 85
  9. lemma OAI.GaussianPropeller.FourCertificates.quartic_0 line 90
  10. lemma OAI.GaussianPropeller.FourCertificates.quartic_1 line 110
  11. lemma OAI.GaussianPropeller.FourCertificates.quartic_2 line 130
  12. lemma OAI.GaussianPropeller.FourCertificates.quartic_3 line 150
  13. lemma OAI.GaussianPropeller.FourCertificates.quartic_4 line 170
  14. lemma OAI.GaussianPropeller.FourCertificates.quartic_5 line 190
  15. lemma OAI.GaussianPropeller.FourCertificates.quartic_6 line 210
  16. lemma OAI.GaussianPropeller.FourCertificates.quartic_7 line 230
  17. lemma OAI.GaussianPropeller.FourCertificates.quartic_8 line 250
  18. lemma OAI.GaussianPropeller.FourCertificates.quartic_9 line 270
  19. lemma OAI.GaussianPropeller.FourCertificates.quartic_10 line 290
  20. lemma OAI.GaussianPropeller.FourCertificates.quartic_11 line 310
  21. lemma OAI.GaussianPropeller.FourCertificates.quartic_12 line 330
  22. lemma OAI.GaussianPropeller.FourCertificates.quartic_13 line 350
  23. lemma OAI.GaussianPropeller.FourCertificates.quartic_14 line 370
  24. lemma OAI.GaussianPropeller.FourCertificates.quartic_15 line 390
  25. lemma OAI.GaussianPropeller.FourCertificates.quartic_16 line 410
  26. lemma OAI.GaussianPropeller.FourCertificates.quartic_17 line 430
  27. lemma OAI.GaussianPropeller.FourCertificates.quartic_18 line 450
  28. lemma OAI.GaussianPropeller.FourCertificates.quartic_19 line 470
  29. lemma OAI.GaussianPropeller.FourCertificates.quartic_20 line 490
  30. lemma OAI.GaussianPropeller.FourCertificates.quartic_of_loss line 510