OAI/Combinatorics/Progressions/Fourier/PolynomialSpectrumAccuracy.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.product_spectrumTail_levels line 12
  2. theorem OAI.Erdos3.product_spectrum_truncation_levels line 24
  3. theorem OAI.Erdos3.product_spectrumTail_geometric line 35
  4. theorem OAI.Erdos3.dyadic_power_ratio line 58
  5. theorem OAI.Erdos3.dyadic_level_mass_bound line 66
  6. theorem OAI.Erdos3.product_spectrumTail_dyadic line 79
  7. theorem OAI.Erdos3.cutoff_power_mass_bound line 101
  8. theorem OAI.Erdos3.dyadic_polynomial_count_factor line 110
  9. theorem OAI.Erdos3.polynomial_bias_mass_factor line 116
  10. theorem OAI.Erdos3.product_spectrumTail_polynomial_cutoff line 122
  11. theorem OAI.Erdos3.exists_spectrum_retained_level line 154
  12. theorem OAI.Erdos3.product_spectrumTail_le_accuracy line 169