OAI/Probability/SKRatio/Certificates/ScalarDataJ1K4.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKRatio.Certificate.Data.J1K4.expression line 11
  2. def OAI.SKRatio.Certificate.Data.J1K4.blocks line 12
  3. lemma OAI.SKRatio.Certificate.Data.J1K4.check_0 line 55
  4. lemma OAI.SKRatio.Certificate.Data.J1K4.check_1 line 56
  5. lemma OAI.SKRatio.Certificate.Data.J1K4.check_2 line 57
  6. lemma OAI.SKRatio.Certificate.Data.J1K4.check_3 line 58
  7. lemma OAI.SKRatio.Certificate.Data.J1K4.check_4 line 59
  8. lemma OAI.SKRatio.Certificate.Data.J1K4.check_5 line 60
  9. lemma OAI.SKRatio.Certificate.Data.J1K4.check_6 line 61
  10. lemma OAI.SKRatio.Certificate.Data.J1K4.check_7 line 62
  11. lemma OAI.SKRatio.Certificate.Data.J1K4.check_8 line 63
  12. lemma OAI.SKRatio.Certificate.Data.J1K4.check_9 line 64
  13. lemma OAI.SKRatio.Certificate.Data.J1K4.check_10 line 65
  14. lemma OAI.SKRatio.Certificate.Data.J1K4.check_11 line 66
  15. lemma OAI.SKRatio.Certificate.Data.J1K4.check_12 line 67
  16. lemma OAI.SKRatio.Certificate.Data.J1K4.check_13 line 68
  17. lemma OAI.SKRatio.Certificate.Data.J1K4.check_14 line 69
  18. lemma OAI.SKRatio.Certificate.Data.J1K4.check_15 line 70
  19. lemma OAI.SKRatio.Certificate.Data.J1K4.check_16 line 71
  20. lemma OAI.SKRatio.Certificate.Data.J1K4.check_17 line 72
  21. lemma OAI.SKRatio.Certificate.Data.J1K4.check_18 line 73
  22. lemma OAI.SKRatio.Certificate.Data.J1K4.check_19 line 74
  23. lemma OAI.SKRatio.Certificate.Data.J1K4.check_20 line 75
  24. lemma OAI.SKRatio.Certificate.Data.J1K4.check_21 line 76
  25. lemma OAI.SKRatio.Certificate.Data.J1K4.check_22 line 77
  26. lemma OAI.SKRatio.Certificate.Data.J1K4.check_23 line 78
  27. lemma OAI.SKRatio.Certificate.Data.J1K4.check_24 line 79
  28. lemma OAI.SKRatio.Certificate.Data.J1K4.check_25 line 80
  29. lemma OAI.SKRatio.Certificate.Data.J1K4.check_26 line 81
  30. lemma OAI.SKRatio.Certificate.Data.J1K4.check_27 line 82
  31. lemma OAI.SKRatio.Certificate.Data.J1K4.check_28 line 83
  32. lemma OAI.SKRatio.Certificate.Data.J1K4.check_29 line 84
  33. lemma OAI.SKRatio.Certificate.Data.J1K4.check_30 line 85
  34. lemma OAI.SKRatio.Certificate.Data.J1K4.check_31 line 86
  35. lemma OAI.SKRatio.Certificate.Data.J1K4.check_32 line 87
  36. lemma OAI.SKRatio.Certificate.Data.J1K4.check_33 line 88
  37. lemma OAI.SKRatio.Certificate.Data.J1K4.check_34 line 89
  38. lemma OAI.SKRatio.Certificate.Data.J1K4.check_35 line 90
  39. lemma OAI.SKRatio.Certificate.Data.J1K4.check_36 line 91
  40. lemma OAI.SKRatio.Certificate.Data.J1K4.check_37 line 92
  41. lemma OAI.SKRatio.Certificate.Data.J1K4.check_38 line 93
  42. lemma OAI.SKRatio.Certificate.Data.J1K4.check_39 line 94
  43. lemma OAI.SKRatio.Certificate.Data.J1K4.checks line 96
  44. theorem OAI.SKRatio.Certificate.Data.J1K4.integral_bound line 140