OAI/Combinatorics/Progressions/Estimates/WeightedOverlapCorrelation.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.sum_overlaps line 13
  2. theorem OAI.Erdos3.sum_overlap_card line 49
  3. theorem OAI.Erdos3.sum_overlap_weights line 54
  4. theorem OAI.Erdos3.correlation_sq_mul_card line 71
  5. theorem OAI.Erdos3.correlation_sq_eq_sum_overlap line 99
  6. theorem OAI.Erdos3.correlation_sq_le_sum_overlap_norm line 112
  7. theorem OAI.Erdos3.norm_overlapCorrelation_le line 122
  8. theorem OAI.Erdos3.weight_large_values_of_sum line 148
  9. theorem OAI.Erdos3.weight_correlating_overlaps line 173
  10. theorem OAI.Erdos3.weight_small_overlaps line 186