OAI/Combinatorics/Progressions/FixedDensity/StrongFullOrderedRegularity.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.FixedDensity.IsFullyPreliminaryOrderedBoundedRegular line 11
  2. theorem OAI.Erdos3.FixedDensity.IsFullyPreliminaryOrderedRegular.toBounded line 22
  3. def OAI.Erdos3.FixedDensity.chosenFullOrderedRegularityCertificate line 32
  4. def OAI.Erdos3.FixedDensity.strongFullOrderedRegularityTower line 46
  5. theorem OAI.Erdos3.FixedDensity.strongFullOrderedRegularityTower_zero line 65
  6. theorem OAI.Erdos3.FixedDensity.strongFullOrderedRegularityTower_succ line 80
  7. def OAI.Erdos3.FixedDensity.strongFullOrderedRegularityStepSchedule line 99
  8. theorem OAI.Erdos3.FixedDensity.strongFullOrderedRegularityTower_refines line 116
  9. theorem OAI.Erdos3.FixedDensity.strongFullOrderedRegularityTower_topLayer_succ line 138
  10. theorem OAI.Erdos3.FixedDensity.strongFullOrderedRegularityTower_topLayer line 160
  11. theorem OAI.Erdos3.FixedDensity.strongFullOrderedRegularityTower_regular line 181
  12. theorem OAI.Erdos3.FixedDensity.strongFullOrderedRegularityTower_boundedRegular line 203
  13. theorem OAI.Erdos3.FixedDensity.strongFullOrderedRegularityStepSchedule_lt line 221
  14. def OAI.Erdos3.FixedDensity.strongFullOrderedComplexityFactor line 240
  15. theorem OAI.Erdos3.FixedDensity.strongFullOrderedComplexityFactor_zero line 250
  16. theorem OAI.Erdos3.FixedDensity.strongFullOrderedComplexityFactor_succ line 258
  17. theorem OAI.Erdos3.FixedDensity.complexity_strongFullOrderedRegularityTower_succ_le line 267
  18. theorem OAI.Erdos3.FixedDensity.complexity_strongFullOrderedRegularityTower_le line 303
  19. def OAI.Erdos3.FixedDensity.orderedAllRankAtomEnergyBudget line 356
  20. def OAI.Erdos3.FixedDensity.orderedFixedTargetAtomEnergy line 362
  21. theorem OAI.Erdos3.FixedDensity.orderedFixedTargetAtomEnergy_nonneg line 371
  22. theorem OAI.Erdos3.FixedDensity.orderedFixedTargetAtomEnergy_le_budget line 382
  23. theorem OAI.Erdos3.FixedDensity.orderedFixedTargetAtomEnergy_mono line 395
  24. def OAI.Erdos3.FixedDensity.orderedFixedTargetAtomEnergyGap line 410
  25. theorem OAI.Erdos3.FixedDensity.orderedFixedTargetAtomEnergyGap_nonneg line 418
  26. theorem OAI.Erdos3.FixedDensity.exists_adjacent_fixedTargetAtomEnergyGap_le_div line 429
  27. theorem OAI.Erdos3.FixedDensity.exists_strongFullOrdered_fixedTarget_pair line 484
  28. def OAI.Erdos3.FixedDensity.orderedMovingAtomEnergy line 535
  29. def OAI.Erdos3.FixedDensity.orderedUpperRefinementAtomEnergyLoss line 541
  30. theorem OAI.Erdos3.FixedDensity.totalAtomEnergyGap_eq_fixedTarget line 548
  31. theorem OAI.Erdos3.FixedDensity.totalAtomEnergyGap_eq_moving_sub_add_upperLoss line 561
  32. theorem OAI.Erdos3.FixedDensity.orderedUpperRefinementAtomEnergyLoss_le_budget line 576
  33. theorem OAI.Erdos3.FixedDensity.one_le_facePartition_complexity line 591
  34. def OAI.Erdos3.FixedDensity.orderedAllRankUpperComplexity line 600
  35. theorem OAI.Erdos3.FixedDensity.orderedAllRankAtomEnergyBudget_le_upperComplexity line 609
  36. theorem OAI.Erdos3.FixedDensity.orderedUpperRefinementAtomEnergyLoss_le_upperComplexity line 634
  37. theorem OAI.Erdos3.FixedDensity.totalAtomEnergyGap_le_moving_sub_add_budget line 645