OAI/Combinatorics/Progressions/FixedDensity/OrderedCounting.lean

GitHub source file

72 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.FixedDensity.EdgeWeightsInUnitInterval line 13
  2. def OAI.Erdos3.FixedDensity.EdgeSupDistanceLe line 17
  3. theorem OAI.Erdos3.FixedDensity.abs_prod_sub_prod_le_card_mul line 21
  4. theorem OAI.Erdos3.FixedDensity.simplexWeight_abs_sub_le line 113
  5. theorem OAI.Erdos3.FixedDensity.simplexCount_abs_sub_le line 137
  6. def OAI.Erdos3.FixedDensity.orderedAPEdgeFactor line 166
  7. theorem OAI.Erdos3.FixedDensity.orderedAPEdgeFactor_self line 177
  8. theorem OAI.Erdos3.FixedDensity.deleteCoordinate_update_same line 184
  9. theorem OAI.Erdos3.FixedDensity.insertNth_eraseCoordinate_eq_update line 192
  10. theorem OAI.Erdos3.FixedDensity.insertNth_insertNth_eraseCoordinate line 199
  11. def OAI.Erdos3.FixedDensity.apMixedCutTest line 209
  12. theorem OAI.Erdos3.FixedDensity.apMixedCutTest_eraseCoordinate line 217
  13. theorem OAI.Erdos3.FixedDensity.apMixedCutTest_bounded line 228
  14. theorem OAI.Erdos3.FixedDensity.prod_orderedAPEdgeFactor line 264
  15. theorem OAI.Erdos3.FixedDensity.prod_apMixedCutTest_eraseCoordinate line 276
  16. theorem OAI.Erdos3.FixedDensity.apSimplexForm_deleteCoordinate_insertNth line 315
  17. theorem OAI.Erdos3.FixedDensity.mean_insertNth line 326
  18. theorem OAI.Erdos3.FixedDensity.mixedSimplexTerm_ap_insertNth line 351
  19. theorem OAI.Erdos3.FixedDensity.mixedSimplexCorrelation_ap_eq_mean_linearCutCorrelation line 384
  20. theorem OAI.Erdos3.FixedDensity.abs_mixedSimplexCorrelation_ap_le line 415
  21. theorem OAI.Erdos3.FixedDensity.apSimplexSystem_mixedCorrelationLe line 448
  22. theorem OAI.Erdos3.FixedDensity.cyclicAPCount_abs_sub_le_of_cutDiscrepancy line 462
  23. def OAI.Erdos3.FixedDensity.deletedFaceTuple line 490
  24. theorem OAI.Erdos3.FixedDensity.deletedFaceTuple_finTupleToDeletedVector line 497
  25. theorem OAI.Erdos3.FixedDensity.finTupleToDeletedVector_deletedFaceTuple line 505
  26. theorem OAI.Erdos3.FixedDensity.deletedFaceTuple_deleteCoordinate line 516
  27. def OAI.Erdos3.FixedDensity.canonicalEdgeFunction line 523
  28. abbrev OAI.Erdos3.FixedDensity.SimplexRegularitySystem line 531
  29. def OAI.Erdos3.FixedDensity.regularizedSimplexSystem line 537
  30. theorem OAI.Erdos3.FixedDensity.regularizedSimplexSystem_edge_finTuple line 548
  31. theorem OAI.Erdos3.FixedDensity.canonicalEdgeFunction_nonneg line 559
  32. theorem OAI.Erdos3.FixedDensity.canonicalEdgeFunction_le_one line 568
  33. theorem OAI.Erdos3.FixedDensity.regularizedSimplexSystem_unitInterval line 577
  34. def OAI.Erdos3.FixedDensity.orderedSimplexEdgeFactor line 595
  35. theorem OAI.Erdos3.FixedDensity.orderedSimplexEdgeFactor_self line 604
  36. def OAI.Erdos3.FixedDensity.insertErasedCoordinate line 612
  37. theorem OAI.Erdos3.FixedDensity.insertErasedCoordinate_eraseCoordinate line 621
  38. def OAI.Erdos3.FixedDensity.simplexMixedCutTest line 631
  39. theorem OAI.Erdos3.FixedDensity.simplexMixedCutTest_eraseCoordinate line 641
  40. theorem OAI.Erdos3.FixedDensity.simplexMixedCutTest_bounded line 656
  41. theorem OAI.Erdos3.FixedDensity.prod_orderedSimplexEdgeFactor line 698
  42. theorem OAI.Erdos3.FixedDensity.prod_simplexMixedCutTest_eraseCoordinate line 712
  43. theorem OAI.Erdos3.FixedDensity.mixedSimplexTerm_regularized_insertNth line 755
  44. theorem OAI.Erdos3.FixedDensity.mixedSimplexCorrelation_regularized_eq_mean line 795
  45. theorem OAI.Erdos3.FixedDensity.abs_mixedSimplexCorrelation_regularized_le line 817
  46. theorem OAI.Erdos3.FixedDensity.regularizedSimplexSystem_mixedCorrelationLe line 853
  47. theorem OAI.Erdos3.FixedDensity.simplexCount_abs_sub_regularized_le line 870
  48. theorem OAI.Erdos3.FixedDensity.exists_regularizedSimplexSystem_count_close line 889
  49. abbrev OAI.Erdos3.FixedDensity.OrderedRegularitySystem line 951
  50. def OAI.Erdos3.FixedDensity.regularizedOrderedPattern line 957
  51. theorem OAI.Erdos3.FixedDensity.regularizedOrderedPattern_edgeWeight line 967
  52. theorem OAI.Erdos3.FixedDensity.regularizedOrderedPattern_unitInterval line 977
  53. theorem OAI.Erdos3.FixedDensity.orderedFaceTuple_split_update_eq line 991
  54. theorem OAI.Erdos3.FixedDensity.orderedFaceTuple_split_insertErased_eq line 1042
  55. def OAI.Erdos3.FixedDensity.orderedPatternEdgeFactor line 1058
  56. theorem OAI.Erdos3.FixedDensity.orderedPatternEdgeFactor_self line 1070
  57. theorem OAI.Erdos3.FixedDensity.prod_orderedPatternEdgeFactor line 1077
  58. theorem OAI.Erdos3.FixedDensity.orderedPatternEdgeFactor_split_insertErased_eq line 1093
  59. theorem OAI.Erdos3.FixedDensity.orderedPatternEdgeFactor_nonneg line 1110
  60. theorem OAI.Erdos3.FixedDensity.orderedPatternEdgeFactor_le_one line 1127
  61. def OAI.Erdos3.FixedDensity.orderedPatternMixedCutTest line 1144
  62. theorem OAI.Erdos3.FixedDensity.orderedPatternMixedCutTest_bounded line 1162
  63. theorem OAI.Erdos3.FixedDensity.cutTestProduct_orderedPatternMixedCutTest line 1197
  64. def OAI.Erdos3.FixedDensity.mixedOrderedPatternTerm line 1264
  65. theorem OAI.Erdos3.FixedDensity.patternWeight_sub_eq_sum_mixedOrderedPatternTerm line 1277
  66. def OAI.Erdos3.FixedDensity.mixedOrderedPatternCorrelation line 1291
  67. theorem OAI.Erdos3.FixedDensity.patternCount_sub_eq_sum_mixedOrderedPatternCorrelation line 1297
  68. theorem OAI.Erdos3.FixedDensity.abs_patternCount_sub_le_sum_mixedOrderedPatternCorrelation line 1323
  69. theorem OAI.Erdos3.FixedDensity.mixedOrderedPatternTerm_regularized_split line 1332
  70. theorem OAI.Erdos3.FixedDensity.mixedOrderedPatternCorrelation_regularized_eq_mean line 1361
  71. theorem OAI.Erdos3.FixedDensity.abs_mixedOrderedPatternCorrelation_regularized_le line 1387
  72. theorem OAI.Erdos3.FixedDensity.patternCount_abs_sub_regularizedOrderedPattern_le line 1427