SmoothWindowSum.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The exact smooth-divisor decomposition inside a short Fourier window, with the discarded tail bounded before any cancellation is used.

lemma OAI.TwoPointCorrelations.shortWindowSum_sub line 14
lemma OAI.TwoPointCorrelations.norm_shortWindowSum_le line 19
lemma OAI.TwoPointCorrelations.window_error_from_density line 24
lemma OAI.TwoPointCorrelations.truncated_window_error line 54
lemma OAI.TwoPointCorrelations.smoothDilationTerm_as_dilation line 71
lemma OAI.TwoPointCorrelations.truncated_shortWindowSum line 81

theorem OAI.TwoPointCorrelations.smooth_dilation_window_sum line 112

Source documentation

Finite short-window majorant: one genuine shorter window for each smooth divisor, and one density term for all discarded smooth divisors.

theorem smooth_dilation_window_sum {f : ℕ → ℂ} (hf : Multiplicative f)
    (hfb : OneBounded f) (q K D Y : ℕ) (hq : 0 < q) (hK : 0 < K) (α : ℝ) :
    (∑ v ∈ range Y, ‖shortWindowSum (fun n => f (q * n)) D α v‖) ≤
      (∑ a ∈ (Icc 1 K).filter (fun a => a.primeFactors ⊆ q.primeFactors),
        ((a : ℝ) * (∑ m ∈ range (Y / a + 1),
          ‖shortWindowSum (coprimeRestriction q f) (D / a + 1) (a * α) m‖) + Y)) +
      (D : ℝ) * (Y + D) * (K : ℝ) ^ (-(1 / 2) : ℝ) *
        smoothReciprocalProduct q.primeFactors (1 / 2 : ℝ) := by
…

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