OAI/Combinatorics/Progressions/Estimates/UnitExpansionCorrelation.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.exists_large_weighted_term line 11
  2. theorem OAI.Erdos3.sum_pair_coefficient_norms_le line 34
  3. theorem OAI.Erdos3.exists_large_weighted_pair line 46
  4. theorem OAI.Erdos3.exists_large_weighted_pair_nonzero line 58
  5. theorem OAI.Erdos3.exists_correlating_components_on_finset line 92
  6. theorem OAI.Erdos3.two_site_model_identity line 158
  7. theorem OAI.Erdos3.two_site_model_error_bound line 193
  8. theorem OAI.Erdos3.complex_unit_vector_resolution line 225
  9. theorem OAI.Erdos3.exists_unit_expansion_correlation line 238