Squared divisor-weighted error bound conditional on a genuine BDH hypothesis

Proved

gpy_divWeightedErrSum_sq_le_of_genuineBDH

by pitimespi · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

number-theory

CONDITIONAL on the explicit, unproved hypothesis hBDH (a genuine Barban-Davenport-Halberstam-shaped summed second-moment bound with explicit constants D and polylog exponent E, at full range L up to R squared over all coprime residues): the squared divisor-weighted error sum is at most the tau-fourth bound times the BDH bound. This does NOT prove genuine BDH and does NOT discharge hDiv.

Preamble

import Mathlib
open Classical

Formal statement

theorem gpy_divWeightedErrSum_sq_le_of_genuineBDH (M : ℕ → ℕ → ℝ) (Y' R : ℕ) (k : ℕ)
    (D : ℝ) (E : ℕ) (hD : 0 ≤ D) (hR : 1 ≤ R) (hY : 1 ≤ Y')
    (hBDH : ∑ L ∈ Finset.range (R ^ 2 + 1),
        ∑ r ∈ (Finset.range L).filter (fun r => Nat.Coprime r L),
          (abs (((((Finset.range (Y' + 1)).filter (fun p => Nat.Prime p ∧ p ≡ r [MOD L])).card : ℝ)) - M Y' L)) ^ 2
        ≤ D * ((R : ℝ) ^ 2 * (Y' : ℝ) * (1 + Real.log (Y' : ℝ)) ^ E)) :
    (∑ L ∈ Finset.range (R ^ 2 + 1), (((Fintype.piFinset (fun _ : Fin (k + 1) => Finset.Icc 1 (L))).filter (fun t => ∏ i, t i = (L))).card : ℝ) ^ 2 * (if h : (((Finset.range L).filter (fun r => Nat.Coprime r L)).image
      (fun r => abs (((((Finset.range (Y' + 1)).filter (fun p => Nat.Prime p ∧ p ≡ r [MOD L])).card : ℝ)) - M Y' L))).Nonempty then
    (((Finset.range L).filter (fun r => Nat.Coprime r L)).image
      (fun r => abs (((((Finset.range (Y' + 1)).filter (fun p => Nat.Prime p ∧ p ≡ r [MOD L])).card : ℝ)) - M Y' L))).max' h
    else 0)) ^ 2 ≤
      ((R : ℝ) ^ 2 * (1 + Real.log ((R : ℝ) ^ 2)) ^ (2 ^ (4 * k) - 1)) *
        (D * ((R : ℝ) ^ 2 * (Y' : ℝ) * (1 + Real.log (Y' : ℝ)) ^ E)) := by sorry

Source

GPY genuine-BDH conditional reduction (GPYBDHFull.lean), restated into Mathlib-only terms

View graph