Second moment of max coprime errors is at most the summed squared-error second moment

Proved

gpy_sum_maxCoprimeErr_sq_le_sum_sum_sq

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

number-theory

Unconditional bridge summed over moduli: the second moment of the max coprime-residue errors is at most the summed squared-error second moment. All local definitions are unfolded into Mathlib terms.

Preamble

import Mathlib
open Classical

Formal statement

theorem gpy_sum_maxCoprimeErr_sq_le_sum_sum_sq (M : ℕ → ℕ → ℝ) (Y Q : ℕ) :
    ∑ L ∈ Finset.range (Q + 1), ((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 ≤
      ∑ L ∈ Finset.range (Q + 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 := by sorry

Source

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

View graph