OAI/Combinatorics/Progressions/FixedDensity/OrderedRemovalAssembly.lean

GitHub source file

80 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.FixedDensity.orderedRemovalConfigurationFaceCount line 12
  2. def OAI.Erdos3.FixedDensity.orderedRemovalTopSubfaceCount line 15
  3. def OAI.Erdos3.FixedDensity.orderedRemovalComplexityCoefficient line 18
  4. def OAI.Erdos3.FixedDensity.orderedRemovalDensityFloor line 21
  5. def OAI.Erdos3.FixedDensity.orderedRemovalCountingError line 28
  6. def OAI.Erdos3.FixedDensity.orderedRemovalDefectThreshold line 35
  7. def OAI.Erdos3.FixedDensity.orderedRemovalEnergyGapTarget line 39
  8. def OAI.Erdos3.FixedDensity.orderedRemovalAlpha line 43
  9. def OAI.Erdos3.FixedDensity.orderedRemovalBeta line 47
  10. def OAI.Erdos3.FixedDensity.orderedRemovalTolerance line 51
  11. def OAI.Erdos3.FixedDensity.orderedRemovalDeletionError line 56
  12. def OAI.Erdos3.FixedDensity.orderedRemovalConfigurationLowerBound line 61
  13. theorem OAI.Erdos3.FixedDensity.orderedRemovalDensityFloor_pos line 67
  14. theorem OAI.Erdos3.FixedDensity.orderedRemovalDensityFloor_nonneg line 77
  15. theorem OAI.Erdos3.FixedDensity.orderedRemovalDensityFloor_le_half line 82
  16. theorem OAI.Erdos3.FixedDensity.orderedRemovalDensityFloor_le_fraction line 88
  17. theorem OAI.Erdos3.FixedDensity.orderedRemovalCountingError_pos line 97
  18. theorem OAI.Erdos3.FixedDensity.orderedRemovalCountingError_nonneg line 105
  19. theorem OAI.Erdos3.FixedDensity.orderedRemovalDefectThreshold_pos line 110
  20. theorem OAI.Erdos3.FixedDensity.orderedRemovalDefectThreshold_nonneg line 117
  21. theorem OAI.Erdos3.FixedDensity.orderedRemovalEnergyGapTarget_pos line 122
  22. theorem OAI.Erdos3.FixedDensity.orderedRemoval_complexity_mul_densityFloor_le_quarter line 130
  23. theorem OAI.Erdos3.FixedDensity.orderedRemovalEnergyGapTarget_div_defectThreshold line 156
  24. theorem OAI.Erdos3.FixedDensity.orderedRemovalDeletionError_le line 167
  25. theorem OAI.Erdos3.FixedDensity.orderedRemoval_counting_margin line 196
  26. theorem OAI.Erdos3.FixedDensity.orderedRemovalConfigurationLowerBound_pos line 229
  27. def OAI.Erdos3.FixedDensity.orderedRemovalRegularityBudget line 242
  28. def OAI.Erdos3.FixedDensity.orderedRemovalRegularityBudgetSchedule line 249
  29. theorem OAI.Erdos3.FixedDensity.orderedRemovalRegularityBudget_pos line 255
  30. theorem OAI.Erdos3.FixedDensity.orderedRemovalRegularityBudget_spec line 261
  31. theorem OAI.Erdos3.FixedDensity.orderedRemovalRegularityBudgetSchedule_spec line 293
  32. def OAI.Erdos3.FixedDensity.orderedRemovalEnergyTimescale line 305
  33. def OAI.Erdos3.FixedDensity.orderedRemovalEnergyLength line 309
  34. theorem OAI.Erdos3.FixedDensity.orderedRemovalEnergyTimescale_pos line 313
  35. theorem OAI.Erdos3.FixedDensity.orderedRemovalEnergyLength_pos line 319
  36. theorem OAI.Erdos3.FixedDensity.orderedRemovalEnergyLength_sum_div_lt line 325
  37. theorem OAI.Erdos3.FixedDensity.fixedUpperLayerComplexityFactor_monotone line 366
  38. def OAI.Erdos3.FixedDensity.orderedRemovalFinePartitionComplexityBound line 375
  39. theorem OAI.Erdos3.FixedDensity.fixedUpperLayerComplexityFactor_le_removalBoundFactor line 385
  40. theorem OAI.Erdos3.FixedDensity.StrongOrderedComplexRegularityCertificate.fine_complexity_le_removalBound line 411
  41. def OAI.Erdos3.FixedDensity.orderedRemovalRankCleaningError line 490
  42. def OAI.Erdos3.FixedDensity.orderedRemovalRankDensityProduct line 502
  43. def OAI.Erdos3.FixedDensity.orderedRemovalRankCountingError line 506
  44. def OAI.Erdos3.FixedDensity.IsRankSensitiveOrderedRemovalChoice line 513
  45. structure OAI.Erdos3.FixedDensity.IsStrongOrderedRemovalCompatible line 525
  46. theorem OAI.Erdos3.FixedDensity.StrongOrderedComplexRegularityCertificate.faceDeletionDensity_badBase_le_removalAllowance line 552
  47. theorem OAI.Erdos3.FixedDensity.StrongOrderedComplexRegularityCertificate.removalConfigurationLowerBound_le_fullConfigurationCount line 636
  48. theorem OAI.Erdos3.FixedDensity.StrongOrderedComplexRegularityCertificate.fullConfigurationCount_pos_of_removalParameters line 691
  49. structure OAI.Erdos3.FixedDensity.NatGrowthFunction line 732
  50. instance OAI.Erdos3.FixedDensity.NatGrowthFunction.(instance at line 739) line 739
  51. theorem OAI.Erdos3.FixedDensity.NatGrowthFunction.monotone line 742
  52. theorem OAI.Erdos3.FixedDensity.NatGrowthFunction.positive line 746
  53. theorem OAI.Erdos3.FixedDensity.NatGrowthFunction.one_le line 751
  54. def OAI.Erdos3.FixedDensity.growthRegularityStepTolerance line 757
  55. def OAI.Erdos3.FixedDensity.growthRegularityStepBudget line 761
  56. def OAI.Erdos3.FixedDensity.growthRegularityComplexity line 766
  57. def OAI.Erdos3.FixedDensity.growthRegularityTolerance line 779
  58. def OAI.Erdos3.FixedDensity.growthRegularityBudget line 787
  59. theorem OAI.Erdos3.FixedDensity.growthRegularityComplexity_zero line 796
  60. theorem OAI.Erdos3.FixedDensity.growthRegularityComplexity_succ line 803
  61. theorem OAI.Erdos3.FixedDensity.growthRegularityTolerance_eq line 815
  62. theorem OAI.Erdos3.FixedDensity.growthRegularityBudget_eq line 825
  63. theorem OAI.Erdos3.FixedDensity.growthRegularityStepTolerance_pos line 837
  64. theorem OAI.Erdos3.FixedDensity.growthRegularityTolerance_pos line 844
  65. theorem OAI.Erdos3.FixedDensity.growthRegularityBudget_pos line 855
  66. theorem OAI.Erdos3.FixedDensity.growthRegularityBudget_spec line 864
  67. theorem OAI.Erdos3.FixedDensity.growthRegularityComplexity_eq_factor_mul line 878
  68. theorem OAI.Erdos3.FixedDensity.growthRegularityComplexity_pos line 896
  69. theorem OAI.Erdos3.FixedDensity.growthRegularityComplexity_monotone line 913
  70. def OAI.Erdos3.FixedDensity.growthRegularityLength line 924
  71. theorem OAI.Erdos3.FixedDensity.growthRegularityLength_pos line 931
  72. theorem OAI.Erdos3.FixedDensity.orderedFace_card_div_growthRegularityLength_lt line 937
  73. structure OAI.Erdos3.FixedDensity.GrowthFunctionFixedUpperCertificate line 977
  74. theorem OAI.Erdos3.FixedDensity.GrowthFunctionFixedUpperCertificate.nonempty line 1014
  75. theorem OAI.Erdos3.FixedDensity.complexity_orderedPatternInitialComplex_le_two line 1103
  76. structure OAI.Erdos3.FixedDensity.OrderedRemovalSchedule line 1124
  77. def OAI.Erdos3.FixedDensity.HasOrderedRemovalSchedules line 1151
  78. theorem OAI.Erdos3.FixedDensity.OrderedRemovalSchedule.certificateCompatible line 1158
  79. theorem OAI.Erdos3.FixedDensity.OrderedRemovalSchedule.certificate_nonempty line 1172
  80. theorem OAI.Erdos3.FixedDensity.hasUniformOrderedPatternRemoval_succ_of_schedules line 1187