OAI/Combinatorics/Progressions/Estimates/WeightedSmoothSampledError.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.finite_mean_square_as_pair line 11
  2. theorem OAI.Erdos3.sampled_second_moment_identity line 17
  3. theorem OAI.Erdos3.finite_mean_bad_event_bound line 24
  4. theorem OAI.Erdos3.sampled_second_moment_bad_pairs line 38
  5. theorem OAI.Erdos3.sampled_weighted_error_of_bad_pairs line 53
  6. theorem OAI.Erdos3.sampled_pair_correlation_cap line 74
  7. theorem OAI.Erdos3.sampled_weighted_error_of_energy line 85
  8. theorem OAI.Erdos3.sampled_error_of_dominated_source line 106
  9. theorem OAI.Erdos3.smooth_window_sampled_error line 120
  10. theorem OAI.Erdos3.sampled_weighted_error_of_dominated_source line 163
  11. theorem OAI.Erdos3.smooth_window_weighted_sampled_error line 181