OAI/Combinatorics/Progressions/FixedDensity/CoarseOrderedRemoval.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.energy_sub_eq_mean_sq_of_le line 19
  2. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.energy_mono_of_le line 31
  3. def OAI.Erdos3.FixedDensity.OrderedRefines line 43
  4. theorem OAI.Erdos3.FixedDensity.OrderedRefines.refl line 49
  5. theorem OAI.Erdos3.FixedDensity.OrderedRefines.trans line 56
  6. def OAI.Erdos3.FixedDensity.orderedTotalEnergy line 65
  7. theorem OAI.Erdos3.FixedDensity.orderedTotalEnergy_nonneg line 73
  8. theorem OAI.Erdos3.FixedDensity.orderedTotalEnergy_le_card line 85
  9. theorem OAI.Erdos3.FixedDensity.orderedTotalEnergy_mono line 107
  10. theorem OAI.Erdos3.FixedDensity.orderedTotalEnergy_sub_eq_sum_mean_sq line 120
  11. theorem OAI.Erdos3.FixedDensity.orderedTotalEnergy_sub_nonneg line 139
  12. theorem OAI.Erdos3.FixedDensity.mean_comp_orderedFaceTuple line 149
  13. theorem OAI.Erdos3.FixedDensity.mixedOrderedPatternTerm_sq_le_edgeDiff_sq line 160
  14. theorem OAI.Erdos3.FixedDensity.mixedOrderedPatternCorrelation_sq_le_mean_edgeDiff_sq line 234
  15. theorem OAI.Erdos3.FixedDensity.regularizedOrderedPattern_count_sub_sq_le_totalEnergyGap line 267
  16. theorem OAI.Erdos3.FixedDensity.regularizedOrderedPattern_count_abs_sub_lt_of_energyGap line 334
  17. theorem OAI.Erdos3.FixedDensity.exists_adjacent_sub_le_div line 359
  18. theorem OAI.Erdos3.FixedDensity.finsetIndicator_biUnion_le_sum line 398
  19. theorem OAI.Erdos3.FixedDensity.mean_finsetIndicator_biUnion_le_sum line 420
  20. def OAI.Erdos3.FixedDensity.ownAtomBadBaseSupport line 434
  21. theorem OAI.Erdos3.FixedDensity.mem_ownAtomBadBaseSupport line 444
  22. theorem OAI.Erdos3.FixedDensity.mean_indicator_atom_inter_badBaseSupport_le_local line 476
  23. theorem OAI.Erdos3.FixedDensity.mean_indicator_ownAtomBadBaseSupport_le line 514
  24. def OAI.Erdos3.FixedDensity.orderedOwnAtomBadBaseSupport line 560
  25. theorem OAI.Erdos3.FixedDensity.mem_orderedOwnAtomBadBaseSupport line 574
  26. theorem OAI.Erdos3.FixedDensity.mean_indicator_orderedOwnAtomBadBaseSupport_le line 592
  27. abbrev OAI.Erdos3.FixedDensity.OrderedPositiveSubface line 611
  28. theorem OAI.Erdos3.FixedDensity.exists_orderedFace_factor_through line 614
  29. def OAI.Erdos3.FixedDensity.orderedFacePullbackFinset line 657
  30. theorem OAI.Erdos3.FixedDensity.mem_orderedFacePullbackFinset line 668
  31. theorem OAI.Erdos3.FixedDensity.mean_indicator_orderedFacePullbackFinset line 678
  32. def OAI.Erdos3.FixedDensity.orderedTopBadBaseDeletion line 703
  33. theorem OAI.Erdos3.FixedDensity.mean_indicator_orderedTopBadBaseDeletion_le line 726
  34. def OAI.Erdos3.FixedDensity.orderedBadBaseDeletionFamily line 828
  35. theorem OAI.Erdos3.FixedDensity.faceDeletionDensity_orderedBadBaseDeletionFamily_le line 836
  36. theorem OAI.Erdos3.FixedDensity.faceDeletionDensity_orderedBadBaseDeletionFamily_constant_le line 880
  37. theorem OAI.Erdos3.FixedDensity.faceDeletionDensity_orderedBadBaseDeletionFamily_constant_le_of_bound line 954
  38. theorem OAI.Erdos3.FixedDensity.ClosedOrderedAtomConfiguration.isGood_of_avoids_topBadBaseDeletion line 975
  39. def OAI.Erdos3.FixedDensity.OrderedCoarseFineComplex.orderedCoarseOwnAtomBadBaseSupport line 1030
  40. theorem OAI.Erdos3.FixedDensity.OrderedCoarseFineComplex.mem_orderedCoarseOwnAtomBadBaseSupport line 1046
  41. theorem OAI.Erdos3.FixedDensity.OrderedCoarseFineComplex.mean_indicator_orderedCoarseOwnAtomBadBaseSupport_le line 1068
  42. def OAI.Erdos3.FixedDensity.ClosedOrderedAtomConfiguration.IsMixedGoodAt line 1092
  43. def OAI.Erdos3.FixedDensity.ClosedOrderedAtomConfiguration.IsMixedGood line 1112
  44. theorem OAI.Erdos3.FixedDensity.ClosedOrderedAtomConfiguration.isMixedGoodAt_of_not_mem_coarseBadBase line 1122
  45. theorem OAI.Erdos3.FixedDensity.ClosedOrderedAtomConfiguration.isMixedGood_of_avoids_coarseBadBases line 1160
  46. def OAI.Erdos3.FixedDensity.OrderedCoarseFineComplex.orderedCoarseTopBadBaseDeletion line 1184
  47. def OAI.Erdos3.FixedDensity.OrderedCoarseFineComplex.orderedCoarseBadBaseDeletionFamily line 1201
  48. theorem OAI.Erdos3.FixedDensity.OrderedCoarseFineComplex.mean_indicator_orderedCoarseTopBadBaseDeletion_le line 1209
  49. theorem OAI.Erdos3.FixedDensity.OrderedCoarseFineComplex.faceDeletionDensity_orderedCoarseBadBaseDeletionFamily_le line 1264
  50. theorem OAI.Erdos3.FixedDensity.OrderedCoarseFineComplex.faceDeletionDensity_orderedCoarseBadBaseDeletionFamily_le_fineGap line 1294
  51. theorem OAI.Erdos3.FixedDensity.OrderedCoarseFineComplex.faceDeletionDensity_orderedCoarseBadBaseDeletionFamily_constant_le line 1349
  52. theorem OAI.Erdos3.FixedDensity.ClosedOrderedAtomConfiguration.isMixedGood_of_avoids_coarseTopBadBaseDeletion line 1430