OAI/NumberTheory/Catalan/Estimates/OddLowerPairPool.lean

GitHub source file

75 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InternalCatalan.oddLowerPairProfile line 11
  2. def OAI.InternalCatalan.oddLowerLossProfile line 14
  3. def OAI.InternalCatalan.oddUpperRankProfile line 17
  4. def OAI.InternalCatalan.oddUpperSimpleProfile line 21
  5. def OAI.InternalCatalan.oddUpperLossProfile line 25
  6. def OAI.InternalCatalan.oddLowerPairCountReal line 29
  7. def OAI.InternalCatalan.oddLowerCountLossReal line 33
  8. def OAI.InternalCatalan.oddUpperRankCountReal line 36
  9. def OAI.InternalCatalan.oddUpperSimpleCountReal line 40
  10. def OAI.InternalCatalan.oddUpperCountLossReal line 44
  11. def OAI.InternalCatalan.oddLowerPairCount line 48
  12. def OAI.InternalCatalan.oddLowerCountLoss line 52
  13. def OAI.InternalCatalan.oddUpperRankCount line 55
  14. def OAI.InternalCatalan.oddUpperSimpleCount line 59
  15. def OAI.InternalCatalan.oddUpperCountLoss line 63
  16. theorem OAI.InternalCatalan.oddLoss_intToNat_cast line 73
  17. theorem OAI.InternalCatalan.oddLoss_natSub_cast line 83
  18. theorem OAI.InternalCatalan.oddLoss_intCast_min line 93
  19. theorem OAI.InternalCatalan.oddLoss_intCast_max line 101
  20. theorem OAI.InternalCatalan.oddLoss_natCast_min line 109
  21. theorem OAI.InternalCatalan.oddLowerPairCount_cast line 117
  22. theorem OAI.InternalCatalan.oddUpperRankCount_cast line 123
  23. theorem OAI.InternalCatalan.oddUpperSimpleCount_cast line 128
  24. theorem OAI.InternalCatalan.oddUpperCountLoss_cast line 134
  25. theorem OAI.InternalCatalan.oddLowerPairCount_le_A line 140
  26. theorem OAI.InternalCatalan.oddLowerLossSubtrahend_le line 149
  27. theorem OAI.InternalCatalan.oddLowerCountLoss_cast line 159
  28. theorem OAI.InternalCatalan.oddLowerPairProfile_of_le_23 line 174
  29. theorem OAI.InternalCatalan.oddLowerPairProfile_23_29 line 184
  30. theorem OAI.InternalCatalan.oddLowerPairProfile_29_65div2 line 193
  31. theorem OAI.InternalCatalan.oddLowerLossProfile_eq line 202
  32. theorem OAI.InternalCatalan.oddUpperProfiles_65div2_40 line 230
  33. theorem OAI.InternalCatalan.oddUpperProfiles_40_52 line 248
  34. theorem OAI.InternalCatalan.oddUpperProfiles_52_58 line 265
  35. theorem OAI.InternalCatalan.oddUpperProfiles_58_59 line 282
  36. theorem OAI.InternalCatalan.oddUpperProfiles_59_65 line 299
  37. theorem OAI.InternalCatalan.oddUpperProfiles_of_ge_65 line 316
  38. theorem OAI.InternalCatalan.oddUpperLossProfile_of_second line 333
  39. theorem OAI.InternalCatalan.oddUpperLossProfile_eq line 339
  40. theorem OAI.InternalCatalan.oddUpperRankCount_eq_nat line 391
  41. theorem OAI.InternalCatalan.oddUpperSimpleCount_eq_nat line 398
  42. theorem OAI.InternalCatalan.oddUpperRetainedCount_eq line 405
  43. theorem OAI.InternalCatalan.oddUpperSimplePhysicalCount_eq line 414
  44. theorem OAI.InternalCatalan.oddCount_mul_max line 424
  45. theorem OAI.InternalCatalan.oddCount_mul_min line 430
  46. theorem OAI.InternalCatalan.oddLowerPairCountReal_mul line 436
  47. theorem OAI.InternalCatalan.oddLowerCountLossReal_mul line 444
  48. theorem OAI.InternalCatalan.oddUpperRankCountReal_mul line 452
  49. theorem OAI.InternalCatalan.oddUpperSimpleCountReal_mul line 460
  50. theorem OAI.InternalCatalan.oddUpperCountLossReal_mul line 468
  51. theorem OAI.InternalCatalan.oddCount_scale_cancel line 476
  52. theorem OAI.InternalCatalan.oddLowerPairCountReal_scaled line 481
  53. theorem OAI.InternalCatalan.oddUpperRankCountReal_scaled line 487
  54. theorem OAI.InternalCatalan.oddUpperSimpleCountReal_scaled line 493
  55. theorem OAI.InternalCatalan.oddLowerCountLossReal_eq line 499
  56. theorem OAI.InternalCatalan.oddUpperCountLossReal_eq line 511
  57. theorem OAI.InternalCatalan.oddLowerPairCount_scaled line 527
  58. theorem OAI.InternalCatalan.oddUpperRankCount_scaled line 533
  59. theorem OAI.InternalCatalan.oddUpperSimpleCount_scaled line 539
  60. theorem OAI.InternalCatalan.oddLowerCountLoss_eq line 545
  61. theorem OAI.InternalCatalan.oddUpperCountLoss_eq line 552
  62. def OAI.InternalCatalan.oddCountLoss line 559
  63. theorem OAI.InternalCatalan.oddCountLoss_eq line 562
  64. def OAI.InternalCatalan.oddLowerPairSet line 581
  65. def OAI.InternalCatalan.oddLowerHighSet line 584
  66. def OAI.InternalCatalan.oddLowerRetainedSet line 587
  67. theorem OAI.InternalCatalan.oddLower_prime_lt_L line 590
  68. theorem OAI.InternalCatalan.oddLowerPairSet_bounds line 593
  69. theorem OAI.InternalCatalan.oddLowerPairSet_mem_pool line 602
  70. theorem OAI.InternalCatalan.oddLowerHighSet_subset_pool line 608
  71. theorem OAI.InternalCatalan.oddLowerPairSet_mem_retained line 615
  72. theorem OAI.InternalCatalan.oddLowerHighSet_card line 624
  73. theorem OAI.InternalCatalan.oddLowerPairSet_card line 631
  74. theorem OAI.InternalCatalan.oddLowerRetainedSet_card line 638
  75. theorem OAI.InternalCatalan.oddLowerPairCount_le_pool line 646