OAI/Combinatorics/Progressions/Estimates/LocalWeightedSifting.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.exists_subset_sum_ge_weighted line 13
  2. theorem OAI.Erdos3.exists_rectangle_sum_ge_weighted line 26
  3. def OAI.Erdos3.WeightedSifting.sampleWeight line 59
  4. theorem OAI.Erdos3.WeightedSifting.sampleWeight_bounds line 62
  5. theorem OAI.Erdos3.WeightedSifting.expect_sampleWeight_mul line 71
  6. theorem OAI.Erdos3.WeightedSifting.expect_sample_score line 78
  7. theorem OAI.Erdos3.WeightedSifting.exists_rectangle_score_ge line 91
  8. theorem OAI.Erdos3.WeightedSifting.exists_dense_rectangle_of_score line 120
  9. theorem OAI.Erdos3.WeightedSifting.exists_dense_rectangle_of_moments line 155
  10. theorem OAI.Erdos3.LocalConvolution.exists_dense_sets_of_correlation_moment line 197