OAI/Combinatorics/Progressions/Fourier/UniformSpectrumLogBounds.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.majorArcBiasLog line 10
  2. def OAI.Erdos3.majorArcLocalizationLog line 14
  3. def OAI.Erdos3.majorArcLengthLog line 17
  4. def OAI.Erdos3.majorArcErrorLog line 20
  5. def OAI.Erdos3.majorArcCoverLog line 23
  6. theorem OAI.Erdos3.majorArcBaseLogs_nonneg line 26
  7. theorem OAI.Erdos3.majorArcCoverLog_nonneg line 32
  8. theorem OAI.Erdos3.majorArcConstants_exp_bounds line 38
  9. theorem OAI.Erdos3.majorArcCoverConstant_exp_bound line 86
  10. def OAI.Erdos3.majorArcSpectrumLog line 117
  11. def OAI.Erdos3.uniformBlockAccuracyLog line 120
  12. def OAI.Erdos3.uniformSpectrumSizeLog line 125
  13. theorem OAI.Erdos3.uniformSpectrumLogs_nonneg line 131
  14. theorem OAI.Erdos3.majorArcSpectrumConstant_exp_bound line 147
  15. theorem OAI.Erdos3.uniformBlockSpectrumAccuracy_exp_bound line 160
  16. theorem OAI.Erdos3.uniformSpectrumSizeConstant_exp_bound line 201
  17. theorem OAI.Erdos3.uniformSpectrumAbsoluteCap_exp_bound line 225