Squared max coprime-residue error is at most the summed squared errors

Proved

gpy_maxCoprimeErr_sq_le_sum_sq

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

number-theory

Unconditional bridge lemma: at one modulus, the squared maximum coprime-residue error is at most the sum of the squared errors over all coprime residues, since the attained residue is one nonnegative term of the sum. All local definitions are unfolded into Mathlib terms.

Preamble

import Mathlib
open Classical

Formal statement

theorem gpy_maxCoprimeErr_sq_le_sum_sq (M : ℕ → ℕ → ℝ) (Y L : ℕ) :
    ((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 ∈ (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