OAI/InformationTheory/BooleanNoise/CurvatureCertificates.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LeanBlast.CourtadeKumar.bernsteinSum line 13
  2. theorem OAI.LeanBlast.CourtadeKumar.bernsteinSum_pos line 16
  3. def OAI.LeanBlast.CourtadeKumar.curvatureT line 35
  4. def OAI.LeanBlast.CourtadeKumar.curvatureP line 38
  5. def OAI.LeanBlast.CourtadeKumar.curvatureN line 41
  6. def OAI.LeanBlast.CourtadeKumar.curvaturePolynomial line 45
  7. def OAI.LeanBlast.CourtadeKumar.curvatureBernstein line 48
  8. theorem OAI.LeanBlast.CourtadeKumar.curvatureBernstein_pos line 69
  9. theorem OAI.LeanBlast.CourtadeKumar.curvaturePolynomial_bernstein line 72
  10. theorem OAI.LeanBlast.CourtadeKumar.curvatureCertificate_pos line 80
  11. def OAI.LeanBlast.CourtadeKumar.lambdaPolynomial line 89
  12. def OAI.LeanBlast.CourtadeKumar.lambdaBernsteinLow line 93
  13. def OAI.LeanBlast.CourtadeKumar.lambdaBernsteinHigh line 104
  14. theorem OAI.LeanBlast.CourtadeKumar.lambdaBernsteinLow_pos line 115
  15. theorem OAI.LeanBlast.CourtadeKumar.lambdaBernsteinHigh_pos line 118
  16. theorem OAI.LeanBlast.CourtadeKumar.lambdaPolynomial_bernstein_low line 121
  17. theorem OAI.LeanBlast.CourtadeKumar.lambdaPolynomial_bernstein_high line 129
  18. theorem OAI.LeanBlast.CourtadeKumar.lambdaCertificate_pos line 137
  19. theorem OAI.LeanBlast.CourtadeKumar.two_lt_exp_347_div_500 line 153
  20. theorem OAI.LeanBlast.CourtadeKumar.ell_lt_347_div_500 line 157
  21. theorem OAI.LeanBlast.CourtadeKumar.nine_lt_exp_eleven_fifths line 160
  22. theorem OAI.LeanBlast.CourtadeKumar.nineteen_lt_exp_three line 164
  23. theorem OAI.LeanBlast.CourtadeKumar.log_nineteen_lt_three line 168
  24. theorem OAI.LeanBlast.CourtadeKumar.nine_halves_lt_exp_151_div_100 line 171
  25. theorem OAI.LeanBlast.CourtadeKumar.log_nine_halves_lt_151_div_100 line 175
  26. def OAI.LeanBlast.CourtadeKumar.smallCurvatureBound line 178
  27. theorem OAI.LeanBlast.CourtadeKumar.smallCurvatureBound_lt_ten_sevenths line 181
  28. theorem OAI.LeanBlast.CourtadeKumar.ten_sevenths_lt_inv_ell line 202
  29. theorem OAI.LeanBlast.CourtadeKumar.smallCurvatureBound_lt_inv_ell line 208
  30. theorem OAI.LeanBlast.CourtadeKumar.largeCurvature_first_term_le line 212
  31. theorem OAI.LeanBlast.CourtadeKumar.largeCurvature_second_term_le line 218
  32. theorem OAI.LeanBlast.CourtadeKumar.largeCurvature_rational_sum line 226
  33. theorem OAI.LeanBlast.CourtadeKumar.largeCurvatureEnvelope_lt line 229