OAI/Combinatorics/Progressions/FixedDensity/StrongOrderedComplexRegularity.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Erdos3.FixedDensity.FixedUpperLayerRegularityCertificate line 12
  2. theorem OAI.Erdos3.FixedDensity.FixedUpperLayerRegularityCertificate.nonempty line 29
  3. def OAI.Erdos3.FixedDensity.chosenFixedUpperLayerRegularityCertificate line 54
  4. def OAI.Erdos3.FixedDensity.fixedUpperLayerRegularityTower line 70
  5. theorem OAI.Erdos3.FixedDensity.fixedUpperLayerRegularityTower_zero line 92
  6. theorem OAI.Erdos3.FixedDensity.fixedUpperLayerRegularityTower_succ line 109
  7. theorem OAI.Erdos3.FixedDensity.fixedUpperLayerRegularityTower_refines line 131
  8. theorem OAI.Erdos3.FixedDensity.fixedUpperLayerRegularityTower_refines_initial line 157
  9. theorem OAI.Erdos3.FixedDensity.fixedUpperLayerRegularityTower_regular line 184
  10. def OAI.Erdos3.FixedDensity.fixedUpperLayerComplexityFactor line 209
  11. theorem OAI.Erdos3.FixedDensity.complexity_fixedUpperLayerRegularityTower_le line 216
  12. structure OAI.Erdos3.FixedDensity.FixedUpperLayerCoarseFine line 280
  13. theorem OAI.Erdos3.FixedDensity.exists_adjacent_real_sub_le_div line 317
  14. theorem OAI.Erdos3.FixedDensity.FixedUpperLayerCoarseFine.nonempty line 349
  15. def OAI.Erdos3.FixedDensity.chosenFixedUpperLayerCoarseFine line 405
  16. def OAI.Erdos3.FixedDensity.selectedOrderedComplexTolerance line 424
  17. structure OAI.Erdos3.FixedDensity.StrongOrderedComplexRegularityCertificate line 431
  18. def OAI.Erdos3.FixedDensity.StrongOrderedComplexRegularityCertificate.toCoarseFine line 490
  19. theorem OAI.Erdos3.FixedDensity.StrongOrderedComplexRegularityCertificate.fine_refines_initial line 504
  20. theorem OAI.Erdos3.FixedDensity.StrongOrderedComplexRegularityCertificate.boundedRegular line 517
  21. theorem OAI.Erdos3.FixedDensity.StrongOrderedComplexRegularityCertificate.nonempty line 532
  22. theorem OAI.Erdos3.FixedDensity.StrongOrderedComplexRegularityCertificate.totalAtomEnergyGap_le_sum_div line 936
  23. theorem OAI.Erdos3.FixedDensity.StrongOrderedComplexRegularityCertificate.totalAtomEnergyGap_nonneg line 955
  24. theorem OAI.Erdos3.FixedDensity.StrongOrderedComplexRegularityCertificate.sum_faceAtomEnergyGap_trans_le_layer line 967
  25. theorem OAI.Erdos3.FixedDensity.StrongOrderedComplexRegularityCertificate.sum_faceAtomEnergyGap_trans_le_total line 1010
  26. theorem OAI.Erdos3.FixedDensity.StrongOrderedComplexRegularityCertificate.sum_fineUpperComplexity_trans_le_allRankUpperComplexity line 1059
  27. theorem OAI.Erdos3.FixedDensity.StrongOrderedComplexRegularityCertificate.faceDeletionDensity_badBase_constant_le line 1146
  28. theorem OAI.Erdos3.FixedDensity.StrongOrderedComplexRegularityCertificate.faceDeletionDensity_badBase_constant_le_sum_div line 1209
  29. theorem OAI.Erdos3.FixedDensity.StrongOrderedComplexRegularityCertificate.faceDeletionDensity_badBase_constant_le_globalComplexity_sum_div line 1237
  30. theorem OAI.Erdos3.FixedDensity.StrongOrderedComplexRegularityCertificate.faceDeletionDensity_badBase_constant_of_complexity_le_sum_div line 1266
  31. theorem OAI.Erdos3.FixedDensity.exists_strongOrderedComplexRegularity line 1320
  32. theorem OAI.Erdos3.FixedDensity.exists_strongOrderedComplexRegularity_of_sum_div_le line 1346
  33. theorem OAI.Erdos3.FixedDensity.exists_strongOrderedComplexRegularity_of_sum_div_lt line 1374