MinorArcWindowFourth.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The discrete weighted-window fourth moment in MRT's minor-arc argument.

theorem OAI.TwoPointCorrelations.minor_arc_window_fourth line 13

Source documentation

A prime block contributes only X (3H+1)^3 possible origin quadruples. The remaining cancellation is exactly the four-prime geometric kernel.

theorem minor_arc_window_fourth (P : Finset ℕ) (X M H d : ℕ) (hd : 0 < d)
    (hP : ∀ p ∈ P, 0 < p ∧ ∀ q ∈ P, q ≤ 2 * p)
    (c θ : ℕ → ℂ) (hc : ∀ p ∈ P, ‖c p‖ ≤ 1) (hθ : ∀ k, ‖θ k‖ ≤ 1)
    (α V : ℝ) (hV : ∀ p ∈ P, (H : ℝ) / (d * p : ℕ) + 1 ≤ V) :
    (∑ m ∈ range M, ‖∑ p ∈ P, ∑ k ∈ range X,
      minorArcWindowTerm M (d * p) k H (c p * θ k) (α * p) m‖ ^ 4) ≤
      (X * (3 * H + 1) ^ 3 : ℕ) *
        ∑ p₁ ∈ P, ∑ p₂ ∈ P, ∑ p₃ ∈ P, ∑ p₄ ∈ P,
          minorArcGeometricBound V (α * ((p₁ : ℝ) + p₂ - p₃ - p₄)) := by
…

Mentions: OAI.TwoPointCorrelations.minorArcWindowTerm, OAI.TwoPointCorrelations.minorArcGeometricBound