OAI/NumberTheory/EgyptianFractions/CyclicDiscrepancyAutomatic.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.CyclicSmoothing.cyclic_small_interval_of_fourier_automatic line 12

   Source documentation

   Low-frequency cancellation itself supplies both numerical modulus conditions needed for the cyclic localization argument.

   theorem cyclic_small_interval_of_fourier_automatic {q : ℕ} [NeZero q]
       {Ω : Type*} [Fintype Ω] (x : Ω → ZMod q) (δ : ℝ)
       (hδ : 0 < δ) (hsmall : δ ≤ 1 / 65536)
       (hfourier : ∀ l : ℕ, 1 ≤ l → l ≤ ⌊1 / δ ^ 4⌋₊ →
         ‖∑ ω : Ω, ZMod.stdAddChar ((l : ZMod q) * x ω)‖ ≤
           (Fintype.card Ω : ℝ) * δ ^ 3) :
       (δ / 2) * (Fintype.card Ω : ℝ) ≤
         ((Finset.univ.filter (fun ω => ((x ω).val : ℝ) < δ * q)).card : ℝ) := by
   …