OAI/Combinatorics/Progressions/FixedDensity/BooleanCutReduction.lean

GitHub source file

119 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.FixedDensity.eraseCoordinate line 17
  2. theorem OAI.Erdos3.FixedDensity.eraseCoordinate_apply line 24
  3. theorem OAI.Erdos3.FixedDensity.eraseCoordinate_eq_removeNth line 29
  4. theorem OAI.Erdos3.FixedDensity.eraseCoordinate_insertNth line 36
  5. abbrev OAI.Erdos3.FixedDensity.CutTestFamily line 42
  6. def OAI.Erdos3.FixedDensity.IsBoundedCutTest line 45
  7. theorem OAI.Erdos3.FixedDensity.IsBoundedCutTest.nonneg line 49
  8. theorem OAI.Erdos3.FixedDensity.IsBoundedCutTest.le_one line 55
  9. theorem OAI.Erdos3.FixedDensity.isBoundedCutTest_const line 61
  10. theorem OAI.Erdos3.FixedDensity.isBoundedCutTest_zero line 68
  11. theorem OAI.Erdos3.FixedDensity.isBoundedCutTest_one line 75
  12. theorem OAI.Erdos3.FixedDensity.IsBoundedCutTest.mono line 81
  13. theorem OAI.Erdos3.FixedDensity.IsBoundedCutTest.mul line 89
  14. def OAI.Erdos3.FixedDensity.cutCorrelation line 99
  15. def OAI.Erdos3.FixedDensity.CutDiscrepancyLe line 106
  16. theorem OAI.Erdos3.FixedDensity.CutDiscrepancyLe.apply_bounded line 114
  17. theorem OAI.Erdos3.FixedDensity.cutCorrelation_self line 123
  18. theorem OAI.Erdos3.FixedDensity.cutCorrelation_swap line 129
  19. theorem OAI.Erdos3.FixedDensity.cutCorrelation_add_middle line 150
  20. theorem OAI.Erdos3.FixedDensity.CutDiscrepancyLe.mono line 160
  21. theorem OAI.Erdos3.FixedDensity.CutDiscrepancyLe.refl line 168
  22. theorem OAI.Erdos3.FixedDensity.CutDiscrepancyLe.refl_of_nonneg line 175
  23. theorem OAI.Erdos3.FixedDensity.CutDiscrepancyLe.of_eq line 181
  24. theorem OAI.Erdos3.FixedDensity.CutDiscrepancyLe.symm line 188
  25. theorem OAI.Erdos3.FixedDensity.CutDiscrepancyLe.triangle line 197
  26. theorem OAI.Erdos3.FixedDensity.CutDiscrepancyLe.epsilon_nonneg line 213
  27. theorem OAI.Erdos3.FixedDensity.mean_add_right line 223
  28. theorem OAI.Erdos3.FixedDensity.mean_sum_fin_succ line 231
  29. theorem OAI.Erdos3.FixedDensity.mean_sum_fin_of_pos line 260
  30. theorem OAI.Erdos3.FixedDensity.cutCorrelation_one line 269
  31. theorem OAI.Erdos3.FixedDensity.cutCorrelation_one_eq_mean_sub line 278
  32. theorem OAI.Erdos3.FixedDensity.CutDiscrepancyLe.abs_mean_sub_le line 294
  33. def OAI.Erdos3.FixedDensity.mulAddEquivOfIsUnit line 314
  34. theorem OAI.Erdos3.FixedDensity.mulAddEquivOfIsUnit_apply line 320
  35. def OAI.Erdos3.FixedDensity.coordinatewiseAddEquiv line 327
  36. theorem OAI.Erdos3.FixedDensity.coordinatewiseAddEquiv_apply line 340
  37. theorem OAI.Erdos3.FixedDensity.coordinatewiseAddEquiv_symm_apply line 347
  38. def OAI.Erdos3.FixedDensity.pullCutTest line 354
  39. theorem OAI.Erdos3.FixedDensity.IsBoundedCutTest.pull line 365
  40. def OAI.Erdos3.FixedDensity.linearCutCorrelation line 384
  41. theorem OAI.Erdos3.FixedDensity.linearCutCorrelation_eq_cutCorrelation line 393
  42. theorem OAI.Erdos3.FixedDensity.CutDiscrepancyLe.abs_linearCutCorrelation_le line 419
  43. def OAI.Erdos3.FixedDensity.sumFiberTuple line 439
  44. theorem OAI.Erdos3.FixedDensity.sumFiberTuple_zero line 444
  45. theorem OAI.Erdos3.FixedDensity.sumFiberTuple_succ line 450
  46. theorem OAI.Erdos3.FixedDensity.sum_sumFiberTuple line 456
  47. def OAI.Erdos3.FixedDensity.sumFiberEquiv line 461
  48. def OAI.Erdos3.FixedDensity.zeroFiberDelta line 480
  49. theorem OAI.Erdos3.FixedDensity.zeroFiberDelta_zero line 486
  50. theorem OAI.Erdos3.FixedDensity.zeroFiberDelta_of_ne line 493
  51. theorem OAI.Erdos3.FixedDensity.zeroFiberDelta_nonneg line 500
  52. def OAI.Erdos3.FixedDensity.fiberConvolution line 509
  53. theorem OAI.Erdos3.FixedDensity.fiberConvolution_arity_zero line 519
  54. theorem OAI.Erdos3.FixedDensity.fiberConvolution_succ line 527
  55. def OAI.Erdos3.FixedDensity.cutTestProduct line 534
  56. theorem OAI.Erdos3.FixedDensity.cutTestProduct_one line 539
  57. theorem OAI.Erdos3.FixedDensity.cutTestProduct_nonneg line 544
  58. theorem OAI.Erdos3.FixedDensity.cutTestProduct_le_one line 550
  59. theorem OAI.Erdos3.FixedDensity.cutTestProduct_mem_Icc line 558
  60. theorem OAI.Erdos3.FixedDensity.cutTestProduct_mul line 565
  61. def OAI.Erdos3.FixedDensity.generalizedConvolution line 572
  62. theorem OAI.Erdos3.FixedDensity.generalizedConvolution_arity_zero line 578
  63. theorem OAI.Erdos3.FixedDensity.generalizedConvolution_succ line 585
  64. theorem OAI.Erdos3.FixedDensity.fiberConvolution_add line 593
  65. theorem OAI.Erdos3.FixedDensity.fiberConvolution_smul line 610
  66. theorem OAI.Erdos3.FixedDensity.fiberConvolution_zero_weight line 625
  67. theorem OAI.Erdos3.FixedDensity.fiberConvolution_const_succ line 632
  68. theorem OAI.Erdos3.FixedDensity.fiberConvolution_linearCombination line 639
  69. theorem OAI.Erdos3.FixedDensity.fiberConvolution_nonneg_succ line 649
  70. theorem OAI.Erdos3.FixedDensity.fiberConvolution_le_one_succ line 657
  71. theorem OAI.Erdos3.FixedDensity.fiberConvolution_mono_succ line 665
  72. theorem OAI.Erdos3.FixedDensity.generalizedConvolution_nonneg_succ line 673
  73. theorem OAI.Erdos3.FixedDensity.generalizedConvolution_le_one_succ line 680
  74. theorem OAI.Erdos3.FixedDensity.generalizedConvolution_mem_Icc line 687
  75. theorem OAI.Erdos3.FixedDensity.generalizedConvolution_nonneg line 698
  76. theorem OAI.Erdos3.FixedDensity.generalizedConvolution_le_one line 705
  77. theorem OAI.Erdos3.FixedDensity.generalizedConvolution_one_succ line 713
  78. theorem OAI.Erdos3.FixedDensity.generalizedConvolution_zero_succ line 731
  79. theorem OAI.Erdos3.FixedDensity.fiberConvolution_pairing_zero line 739
  80. theorem OAI.Erdos3.FixedDensity.fiberConvolution_pairing_succ line 763
  81. theorem OAI.Erdos3.FixedDensity.fiberConvolution_pairing line 798
  82. theorem OAI.Erdos3.FixedDensity.mean_fiberConvolution line 807
  83. theorem OAI.Erdos3.FixedDensity.mean_generalizedConvolution line 814
  84. theorem OAI.Erdos3.FixedDensity.cutCorrelation_eq_mean_mul_generalizedConvolution line 820
  85. theorem OAI.Erdos3.FixedDensity.apCoefficient_isUnit_of_coprime_factorial line 839
  86. def OAI.Erdos3.FixedDensity.apCoefficientAddEquiv line 866
  87. theorem OAI.Erdos3.FixedDensity.apCoefficientAddEquiv_apply line 876
  88. def OAI.Erdos3.FixedDensity.finSuccAboveEquiv line 884
  89. theorem OAI.Erdos3.FixedDensity.finSuccAboveEquiv_apply_val line 898
  90. def OAI.Erdos3.FixedDensity.finTupleToDeletedVector line 903
  91. theorem OAI.Erdos3.FixedDensity.finTupleToDeletedVector_succAbove line 911
  92. theorem OAI.Erdos3.FixedDensity.apSimplexForm_finTupleToDeletedVector line 921
  93. theorem OAI.Erdos3.FixedDensity.deleteCoordinate_eq_finTupleToDeletedVector line 940
  94. theorem OAI.Erdos3.FixedDensity.apSimplexForm_deleteCoordinate_eq_weightedSum line 955
  95. def OAI.Erdos3.FixedDensity.apFaceScalingEquiv line 965
  96. theorem OAI.Erdos3.FixedDensity.apFaceScalingEquiv_apply line 975
  97. def OAI.Erdos3.FixedDensity.bernoulliAssignmentWeight line 994
  98. def OAI.Erdos3.FixedDensity.booleanValue line 999
  99. theorem OAI.Erdos3.FixedDensity.bernoulliAssignmentWeight_nonneg line 1002
  100. theorem OAI.Erdos3.FixedDensity.sum_bernoulliAssignmentWeight line 1016
  101. theorem OAI.Erdos3.FixedDensity.sum_bernoulliAssignmentWeight_mul_selected line 1037
  102. theorem OAI.Erdos3.FixedDensity.sum_bernoulliAssignmentWeight_mul_embedding line 1077
  103. abbrev OAI.Erdos3.FixedDensity.CutTestCoordinate line 1090
  104. abbrev OAI.Erdos3.FixedDensity.BooleanCutAssignment line 1093
  105. def OAI.Erdos3.FixedDensity.cutTestFamilyOfBooleanAssignment line 1096
  106. theorem OAI.Erdos3.FixedDensity.cutTestFamilyOfBooleanAssignment_bounded line 1102
  107. def OAI.Erdos3.FixedDensity.cutTestCoordinateValue line 1110
  108. def OAI.Erdos3.FixedDensity.usedCutTestCoordinateEmbedding line 1116
  109. theorem OAI.Erdos3.FixedDensity.usedCutTestCoordinateEmbedding_apply line 1125
  110. theorem OAI.Erdos3.FixedDensity.cutTestProduct_eq_sum_boolean line 1131
  111. theorem OAI.Erdos3.FixedDensity.cutCorrelation_eq_sum_boolean line 1149
  112. theorem OAI.Erdos3.FixedDensity.abs_cutCorrelation_le_of_boolean line 1205
  113. def OAI.Erdos3.FixedDensity.booleanCutConvolution line 1246
  114. theorem OAI.Erdos3.FixedDensity.booleanCutConvolution_unitBounded line 1252
  115. theorem OAI.Erdos3.FixedDensity.booleanCutConvolution_unitBoundedFamily line 1265
  116. theorem OAI.Erdos3.FixedDensity.cutCorrelation_boolean_eq_pairing line 1272
  117. theorem OAI.Erdos3.FixedDensity.exists_cutDiscrepancy_model_of_finiteBooleanModel line 1282
  118. theorem OAI.Erdos3.FixedDensity.exists_cutDiscrepancy_model_of_positivePartCorrelationBound line 1298
  119. theorem OAI.Erdos3.FixedDensity.exists_cutDiscrepancy_model_of_monomialCorrelationBound line 1313