OAI/Combinatorics/Progressions/FixedDensity/TowerDominatingGrowth.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Erdos3.FixedDensity.DescendingGrowthHierarchy line 9
  2. theorem OAI.Erdos3.FixedDensity.DescendingGrowthHierarchy.lower_le_growth line 18
  3. theorem OAI.Erdos3.FixedDensity.DescendingGrowthHierarchy.growth_eq_upper line 26
  4. theorem OAI.Erdos3.FixedDensity.DescendingGrowthHierarchy.lower_le_growth_le_upper line 33
  5. theorem OAI.Erdos3.FixedDensity.DescendingGrowthHierarchy.antitone line 42
  6. def OAI.Erdos3.FixedDensity.canonicalDescendingGrowthHierarchy line 53
  7. theorem OAI.Erdos3.FixedDensity.canonicalDescendingGrowthHierarchy_last line 70
  8. theorem OAI.Erdos3.FixedDensity.canonicalDescendingGrowthHierarchy_zero line 78
  9. def OAI.Erdos3.FixedDensity.growthComplexRegularityTolerance line 85
  10. def OAI.Erdos3.FixedDensity.growthComplexRegularityBudget line 94
  11. def OAI.Erdos3.FixedDensity.growthComplexRegularityLength line 103
  12. def OAI.Erdos3.FixedDensity.selectedGrowthCoarseComplexityBound line 109
  13. def OAI.Erdos3.FixedDensity.selectedGrowthFineComplexityBound line 118
  14. def OAI.Erdos3.FixedDensity.selectedGrowthCoarseLayerComplexityBound line 127
  15. def OAI.Erdos3.FixedDensity.selectedGrowthFineLayerComplexityBound line 139
  16. theorem OAI.Erdos3.FixedDensity.growthComplexRegularityTolerance_pos line 151
  17. theorem OAI.Erdos3.FixedDensity.growthComplexRegularityBudget_spec line 163
  18. theorem OAI.Erdos3.FixedDensity.growthComplexRegularityLength_pos line 178
  19. structure OAI.Erdos3.FixedDensity.GrowthFunctionOrderedComplexRegularityCertificate line 186
  20. def OAI.Erdos3.FixedDensity.GrowthFunctionOrderedComplexRegularityCertificate.localCertificate line 245
  21. theorem OAI.Erdos3.FixedDensity.GrowthFunctionOrderedComplexRegularityCertificate.coarse_upper_complexity line 287
  22. theorem OAI.Erdos3.FixedDensity.GrowthFunctionOrderedComplexRegularityCertificate.fine_upper_complexity line 303
  23. theorem OAI.Erdos3.FixedDensity.GrowthFunctionOrderedComplexRegularityCertificate.nonempty line 321
  24. def OAI.Erdos3.FixedDensity.growthRegularityOneStep line 464
  25. theorem OAI.Erdos3.FixedDensity.growthRegularityComplexity_succ_eq_oneStep line 470
  26. def OAI.Erdos3.FixedDensity.boundedGrowthRegularityOneStepMaximum line 479
  27. theorem OAI.Erdos3.FixedDensity.growthRegularityOneStep_le_boundedMaximum line 487
  28. theorem OAI.Erdos3.FixedDensity.boundedGrowthRegularityOneStepMaximum_monotone line 505
  29. def OAI.Erdos3.FixedDensity.finiteRankGrowthRegularityOneStepMaximum line 514
  30. theorem OAI.Erdos3.FixedDensity.growthRegularityOneStep_le_finiteRankMaximum line 522
  31. theorem OAI.Erdos3.FixedDensity.finiteRankGrowthRegularityOneStepMaximum_monotone line 540
  32. def OAI.Erdos3.FixedDensity.towerDominatingGrowth line 556
  33. theorem OAI.Erdos3.FixedDensity.towerDominatingGrowth_apply line 577
  34. theorem OAI.Erdos3.FixedDensity.le_towerDominatingGrowth line 586
  35. theorem OAI.Erdos3.FixedDensity.growthFunction_le_towerDominatingGrowth_of_le line 592
  36. theorem OAI.Erdos3.FixedDensity.growthRegularityOneStep_le_towerDominatingGrowth line 599
  37. def OAI.Erdos3.FixedDensity.towerDominatingGrowthIteration line 610
  38. theorem OAI.Erdos3.FixedDensity.towerDominatingGrowthIteration_zero line 619
  39. theorem OAI.Erdos3.FixedDensity.towerDominatingGrowthIteration_succ line 625
  40. theorem OAI.Erdos3.FixedDensity.le_towerDominatingGrowthIteration line 632
  41. theorem OAI.Erdos3.FixedDensity.towerDominatingGrowthIteration_le_succ line 647
  42. theorem OAI.Erdos3.FixedDensity.growthRegularityOneStep_le_nextGrowthIteration line 655
  43. theorem OAI.Erdos3.FixedDensity.growthRegularityComplexity_succ_le_nextGrowthIteration line 666
  44. theorem OAI.Erdos3.FixedDensity.towerDominatingGrowthIteration_reciprocal_le line 682
  45. def OAI.Erdos3.FixedDensity.finiteMaximum line 695
  46. theorem OAI.Erdos3.FixedDensity.le_finiteMaximum line 702
  47. theorem OAI.Erdos3.FixedDensity.GrowthFunctionOrderedComplexRegularityCertificate.selectedFineComplexity_le_nextGrowthIteration line 720
  48. theorem OAI.Erdos3.FixedDensity.GrowthFunctionOrderedComplexRegularityCertificate.regular_with_requestedGrowth line 744
  49. def OAI.Erdos3.FixedDensity.GrowthFunctionOrderedComplexRegularityCertificate.selectedRankTowerHierarchy line 771
  50. theorem OAI.Erdos3.FixedDensity.GrowthFunctionOrderedComplexRegularityCertificate.selectedRankTowerHierarchy_last line 793
  51. theorem OAI.Erdos3.FixedDensity.GrowthFunctionOrderedComplexRegularityCertificate.selectedRankTowerHierarchy_zero line 818
  52. theorem OAI.Erdos3.FixedDensity.GrowthFunctionOrderedComplexRegularityCertificate.selectedFineComplexity_le_selectedRankTowerHierarchy line 838
  53. theorem OAI.Erdos3.FixedDensity.GrowthFunctionOrderedComplexRegularityCertificate.finePartitionComplexity_le_selectedRankTowerHierarchy line 858
  54. def OAI.Erdos3.FixedDensity.GrowthFunctionOrderedComplexRegularityCertificate.selectedFineLayerMaximum line 877
  55. def OAI.Erdos3.FixedDensity.GrowthFunctionOrderedComplexRegularityCertificate.selectedAllRankTowerHierarchy line 894
  56. theorem OAI.Erdos3.FixedDensity.GrowthFunctionOrderedComplexRegularityCertificate.selectedAllRankTowerHierarchy_last line 912
  57. theorem OAI.Erdos3.FixedDensity.GrowthFunctionOrderedComplexRegularityCertificate.selectedFineLayerComplexity_le_allRankTowerHierarchy line 929
  58. theorem OAI.Erdos3.FixedDensity.GrowthFunctionOrderedComplexRegularityCertificate.fineComplexity_le_allRankTowerHierarchy line 963