OAI/Combinatorics/Progressions/Fourier/QuadraticFrequencyCoordinates.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.finiteFourierCoeff_convolution line 13
  2. theorem OAI.Erdos3.finiteFourierCoeff_reflected_conjugate line 34
  3. theorem OAI.Erdos3.gowersNorm_two_fourier line 42
  4. theorem OAI.Erdos3.cross_correlation_fourier_energy line 74
  5. theorem OAI.Erdos3.exists_large_fourier_of_mean_cross_correlation line 88
  6. theorem OAI.Erdos3.exists_large_fourier_of_gowers_two line 123
  7. theorem OAI.Erdos3.mean_derivative_fourier_fourth_le_gowers_three line 160
  8. theorem OAI.Erdos3.exp_le_gowers_three_of_mean_derivative_fourier line 185
  9. theorem OAI.Erdos3.character_relation_of_quadruple_pos line 211
  10. theorem OAI.Erdos3.exists_many_derivative_character_relations line 238
  11. theorem OAI.Erdos3.derivative_character_graph_energy line 270
  12. theorem OAI.Erdos3.exists_quadratic_frequency_graph line 303
  13. theorem OAI.Erdos3.exists_quadratic_frequency_small_difference line 343
  14. theorem OAI.Erdos3.exists_cyclic_interval_fourier_smoothing line 416
  15. theorem OAI.Erdos3.additiveGraph_difference_card_hom line 459
  16. theorem OAI.Erdos3.exists_quadratic_affine_frequency_coordinates line 482
  17. theorem OAI.Erdos3.exists_quadratic_affine_frequency_coordinates_budget line 544