OAI/Probability/GaussianPropeller/ProbabilityBounds.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.GaussianPropeller.ProbabilityBounds.p line 28
  2. lemma OAI.GaussianPropeller.ProbabilityBounds.gaussianConst_tight line 30
  3. lemma OAI.GaussianPropeller.ProbabilityBounds.p_pos line 38
  4. lemma OAI.GaussianPropeller.ProbabilityBounds.hasDerivAt_p line 41
  5. lemma OAI.GaussianPropeller.ProbabilityBounds.p_antitone line 44
  6. lemma OAI.GaussianPropeller.ProbabilityBounds.p_le_half line 49
  7. lemma OAI.GaussianPropeller.ProbabilityBounds.p_taylor_lower line 53
  8. lemma OAI.GaussianPropeller.ProbabilityBounds.p_taylor_upper line 64
  9. lemma OAI.GaussianPropeller.ProbabilityBounds.lambda_taylor_upper line 75
  10. lemma OAI.GaussianPropeller.ProbabilityBounds.G_upper_of_lambda line 92
  11. lemma OAI.GaussianPropeller.ProbabilityBounds.certificate_005 line 100
  12. lemma OAI.GaussianPropeller.ProbabilityBounds.certificate_014 line 113
  13. lemma OAI.GaussianPropeller.ProbabilityBounds.certificate_024 line 126
  14. lemma OAI.GaussianPropeller.ProbabilityBounds.certificate_033 line 139
  15. lemma OAI.GaussianPropeller.ProbabilityBounds.certificate_041 line 152
  16. lemma OAI.GaussianPropeller.ProbabilityBounds.certificate_048 line 165
  17. lemma OAI.GaussianPropeller.ProbabilityBounds.certificate_054 line 178
  18. lemma OAI.GaussianPropeller.ProbabilityBounds.certificate_059 line 191
  19. lemma OAI.GaussianPropeller.ProbabilityBounds.certificate_064 line 204
  20. lemma OAI.GaussianPropeller.ProbabilityBounds.exists_p line 217
  21. def OAI.GaussianPropeller.ProbabilityBounds.loss line 227
  22. lemma OAI.GaussianPropeller.ProbabilityBounds.loss_eq line 229
  23. lemma OAI.GaussianPropeller.ProbabilityBounds.hasDerivAt_loss line 233
  24. lemma OAI.GaussianPropeller.ProbabilityBounds.loss_antitone line 241
  25. lemma OAI.GaussianPropeller.ProbabilityBounds.G_test_bound line 257
  26. lemma OAI.GaussianPropeller.ProbabilityBounds.row_margin line 269
  27. lemma OAI.GaussianPropeller.ProbabilityBounds.test_probability line 293
  28. lemma OAI.GaussianPropeller.ProbabilityBounds.linear_quadratic_of_loss line 406