OAI/NumberTheory/Ostmann/Characters/CharacterFourierBudgets.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Explicit finite-frequency and Fourier-window costs

  1. theorem OAI.Ostmann.naturalTransferCutoff_linear_bound line 12
  2. theorem OAI.Ostmann.character_initial_window_bounds line 19
  3. theorem OAI.Ostmann.character_uniform_profile_bounds line 31
  4. theorem OAI.Ostmann.character_prime_band_log_ratio line 39
  5. theorem OAI.Ostmann.character_prime_band_dyadic_budget line 49