OAI/Combinatorics/Progressions/FixedDensity/BundleCountingRecurrence.lean

GitHub source file

67 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.FixedDensity.mean_mul_sq_le_product line 9
  2. theorem OAI.Erdos3.FixedDensity.mean_sq_eq_mean_pair_mul line 19
  3. theorem OAI.Erdos3.FixedDensity.mean_inner_sq_eq_mean₂_pair line 33
  4. theorem OAI.Erdos3.FixedDensity.mean_square_le_mean_square line 44
  5. theorem OAI.Erdos3.FixedDensity.mean_pow_two_le_mean_pow_two line 53
  6. theorem OAI.Erdos3.FixedDensity.mean_pow_two_le_mean_pow_two_of_pos line 88
  7. theorem OAI.Erdos3.FixedDensity.mean_pow_two_le_mean_pow_two' line 111
  8. theorem OAI.Erdos3.FixedDensity.cauchySchwarz_eliminate_outer_factor line 121
  9. structure OAI.Erdos3.FixedDensity.HypergraphBundle line 165
  10. def OAI.Erdos3.FixedDensity.HypergraphBundle.IsClosedUnderInclusion line 181
  11. def OAI.Erdos3.FixedDensity.HypergraphBundle.order line 186
  12. def OAI.Erdos3.FixedDensity.HypergraphBundle.edgeCountAtRank line 189
  13. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.edge_card_le_order line 193
  14. def OAI.Erdos3.FixedDensity.HypergraphBundle.eraseEdge line 199
  15. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.eraseEdge_edges line 214
  16. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.eraseEdge_order_le line 219
  17. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.edgeCountAtRank_eraseEdge line 227
  18. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.eraseEdge_closed_of_maximal line 246
  19. def OAI.Erdos3.FixedDensity.HypergraphBundle.edgeTuple line 267
  20. def OAI.Erdos3.FixedDensity.HypergraphBundle.projectionEquiv line 272
  21. def OAI.Erdos3.FixedDensity.HypergraphBundle.projectedEdgeTuple line 295
  22. abbrev OAI.Erdos3.FixedDensity.HypergraphBundle.BaseEdgeWeight line 302
  23. def OAI.Erdos3.FixedDensity.HypergraphBundle.BaseWeightsInUnitInterval line 306
  24. def OAI.Erdos3.FixedDensity.HypergraphBundle.pullbackBaseEdgeWeight line 311
  25. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.pullbackBaseEdgeWeight_of_mem line 323
  26. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.pullbackBaseEdgeWeight_unitInterval line 334
  27. def OAI.Erdos3.FixedDensity.HypergraphBundle.WeightsInUnitInterval line 345
  28. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.pullbackBaseEdgeWeight_weightsInUnitInterval line 351
  29. def OAI.Erdos3.FixedDensity.HypergraphBundle.bundleProduct line 360
  30. def OAI.Erdos3.FixedDensity.HypergraphBundle.bundleCount line 367
  31. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.bundleProduct_nonneg line 374
  32. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.bundleProduct_le_one line 385
  33. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.bundleCount_nonneg line 399
  34. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.bundleCount_le_one line 408
  35. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.WeightsInUnitInterval.eraseEdge line 417
  36. def OAI.Erdos3.FixedDensity.HypergraphBundle.edgeRemainder line 427
  37. def OAI.Erdos3.FixedDensity.HypergraphBundle.edgeContribution line 435
  38. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.bundleCount_eq_edgeContribution line 445
  39. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.bundleCount_decompose_edge line 460
  40. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.edgeContribution_const line 506
  41. abbrev OAI.Erdos3.FixedDensity.HypergraphBundle.EdgeComplement line 519
  42. def OAI.Erdos3.FixedDensity.HypergraphBundle.edgeSumEquiv line 522
  43. def OAI.Erdos3.FixedDensity.HypergraphBundle.splitEdgeEquiv line 526
  44. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.splitEdgeEquiv_fst line 538
  45. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.edgeTuple_splitEdgeEquiv_symm line 545
  46. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.mean_splitEdge line 553
  47. def OAI.Erdos3.FixedDensity.HypergraphBundle.edgeRemainderFiber line 577
  48. def OAI.Erdos3.FixedDensity.HypergraphBundle.edgeRemainderAverage line 587
  49. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.edgeContribution_eq_mean_mul_remainderAverage line 596
  50. def OAI.Erdos3.FixedDensity.HypergraphBundle.frozenEdgeCorrelation line 614
  51. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.edgeContribution_eq_mean_frozenEdgeCorrelation line 625
  52. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.abs_edgeContribution_le_of_frozen line 651
  53. def OAI.Erdos3.FixedDensity.HypergraphBundle.doubledRemainderMoment line 672
  54. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.doubledRemainderMoment_nonneg line 681
  55. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.edgeRemainderAverage_unitInterval line 690
  56. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.doubledRemainderMoment_le_one line 712
  57. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.doubledRemainderMoment_eq_mean₂_pair line 727
  58. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.edgeContribution_sq_le_localSquare_mul_doubled line 745
  59. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.edgeContribution_sq_le_of_localized_defect line 759
  60. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.edgeContribution_sq_le_of_localized_defect_unitInterval line 785
  61. theorem OAI.Erdos3.FixedDensity.abs_finiteCount_sub_prod_le_card_mul line 823
  62. theorem OAI.Erdos3.FixedDensity.finiteCount_prod_sub_card_mul_le line 899
  63. theorem OAI.Erdos3.FixedDensity.pow_sub_card_mul_le_finiteCount line 921
  64. theorem OAI.Erdos3.FixedDensity.finiteCount_pos_of_card_mul_lt_pow line 951
  65. theorem OAI.Erdos3.FixedDensity.abs_finiteCount_sub_prod_le_sum_error line 971
  66. theorem OAI.Erdos3.FixedDensity.finiteCount_prod_sub_sum_error_le line 1044
  67. theorem OAI.Erdos3.FixedDensity.finiteCount_pos_of_sum_error_lt_prod line 1066