OAI/NumberTheory/EgyptianFractions/DeterministicMeanBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.deterministic_mean_bound line 13

   Source documentation

   The deterministic high-level Fourier second moment, at the exact exponential rate used by the residue exceptional-set construction. The threshold is uniform in the scale, cutoff, frequency, and indexed list.

   theorem deterministic_mean_bound (D : ℝ) (hD : 255 ≤ D) :
       ∀ᶠ S : ℝ in atTop, ∀ (m X C ell : ℝ),
         S / (2 * Real.log S) ≤ m → m ≤ S / Real.log S →
         Real.exp S ≤ X → X ≤ Real.exp (D * S / 4) →
         Real.exp (D * S) ≤ C → C ≤ Real.exp (2 * D * S) →
         1 ≤ ell → ell ≤ Real.exp (m / 2500) →
         ∀ {β : Type*} (T : Finset β) (t : β → ℕ),
           Set.InjOn t (T : Set β) →
           Real.exp (Real.log 2 * m) ≤ (T.card : ℝ) →
           (∀ i ∈ T, (t i : ℝ) ≤ Real.exp (101 * S)) →
           (∑ u ∈ Finset.Icc (⌊Real.exp (-m / 10000) * X⌋₊ + 1) ⌊X⌋₊,
             ‖(∑ i ∈ T, differencingPhase (ell * C * (t i : ℝ) / (u : ℝ))) /
   …

   Mentions: OAI.Problem337.D, OAI.Problem337.differencingPhase