LogPhaseUniform.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform cancellation for logarithmic exponential sums

Only finitely many derivative orders are required when the frequency is bounded by a fixed power of the length scale.

theorem OAI.JointDickman.logarithmic_phase_uniform line 18

Source documentation

A fixed power range of frequencies admits a positive power saving, uniformly in an additional linear phase and in the interval endpoints.

theorem logarithmic_phase_uniform (B : ℝ) (hB : 1/2 ≤ B) :
    ∃ A δ : ℝ, 0 < A ∧ 0 < δ ∧
      ∀ᶠ U : ℝ in atTop, ∀ (a Z : ℝ) (L R : ℤ),
        U^(1/2:ℝ) ≤ |Z| → |Z| ≤ U^B →
        U ≤ (L:ℝ) → (R:ℝ) ≤ 2*U →
        ‖∑ n ∈ Finset.Icc L R, differencingPhase (a*n+Z*Real.log n)‖ ≤
          A*U^(1-δ) := by
…