SmoothWindowBound.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Summing the shorter-window estimates costs a reciprocal smooth sum, not the number of smooth divisors. The elementary endpoint error is explicit.

lemma OAI.TwoPointCorrelations.smooth_harmonic_sum_le line 13
lemma OAI.TwoPointCorrelations.dilation_window_count_bound line 31

theorem OAI.TwoPointCorrelations.smooth_dilation_window_bound line 59

Source documentation

The finite analytic assembly used for a dilated nonpretentious factor. hbase is subsequently supplied by the published MRT theorem, uniformly in the original function's finite-prime changes.

theorem smooth_dilation_window_bound {f : ℕ → ℂ}
    (hf : Multiplicative f) (hfb : OneBounded f)
    (q K D Y : ℕ) (hq : 0 < q) (hK : 0 < K)
    (hKD : K ≤ D) (hDY : D ≤ Y) (C E : ℝ) (hC : 0 ≤ C) (hE : 0 ≤ E)
    (hbase : ∀ a ∈ Icc 1 K, ∀ β : ℝ,
      (∑ m ∈ range (Y / a + 1),
        ‖shortWindowSum (coprimeRestriction q f) (D / a + 1) β m‖) ≤
        C * (D / a + 1 : ℕ) * (Y / a + 1 : ℕ) * E)
    (α : ℝ) :
    (∑ v ∈ range Y, ‖shortWindowSum (fun n => f (q * n)) D α v‖) ≤
      4 * C * D * Y * E * smoothReciprocalProduct q.primeFactors (1 / 2 : ℝ) +
        (K : ℝ) * Y + 2 * D * Y * (K : ℝ) ^ (-(1 / 2) : ℝ) *
…

Mentions: OAI.TwoPointCorrelations.Multiplicative, OAI.TwoPointCorrelations.OneBounded, OAI.TwoPointCorrelations.shortWindowSum, OAI.TwoPointCorrelations.coprimeRestriction, OAI.TwoPointCorrelations.smoothReciprocalProduct