OAI/NumberTheory/Ostmann/Characters/ConcreteQuartetFourier.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The quartet Fourier estimate with the actual autocorrelation spectra

  1. def OAI.Ostmann.twoBadQuartetError line 14
  2. theorem OAI.Ostmann.twoBadQuartetError_nonneg line 21
  3. theorem OAI.Ostmann.concrete_two_bad_fourier_le line 24
  4. def OAI.Ostmann.friendlyQuartetError line 66
  5. theorem OAI.Ostmann.friendlyQuartetError_nonneg line 70
  6. theorem OAI.Ostmann.concrete_left_friendly_fourier_le line 73
  7. theorem OAI.Ostmann.concrete_quartet_fourier_le line 93