Range absolute bound for the twisted weight

Proved

gpy_twistedAbsWeight_sum_Icc_le_exp

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

number-theory

For T at least 2, the sum of the absolute twisted weight over n in [1, T] is at most exp(2 (k+1)^2 (log T + 2)). The bound passes through the truncated Euler product, uses the uniform local-count bound c_p at most (k+1)^2 together with c_p/(p-1) at most 2(k+1)^2/p, and the elementary harmonic bound on the sum of reciprocals of primes up to T. This is an unconditional absolute/tail bound; it identifies no asymptotic main term and claims none. Formalization Note: the statement is written out in Mathlib terms, with no local definitions.

Preamble

import Mathlib
open Classical

Formal statement

theorem gpy_twistedAbsWeight_sum_Icc_le_exp {k : ℕ} (h : Fin k → ℕ) (i : Fin k) (hd he : Prop) [Decidable hd] [Decidable he] {T : ℕ} (hT : 2 ≤ T) :
    ∑ n ∈ Finset.Icc 1 T, abs ((ArithmeticFunction.moebius n : ℝ) * ((∏ p ∈ n.primeFactors, ((((Finset.univ : Finset (Option (Fin k) × Option (Fin k))).filter (fun ab =>
    (ab.1.isSome ↔ hd) ∧ (ab.2.isSome ↔ he) ∧
    (∀ j j', (ab.1 = some j ∨ ab.2 = some j) →
      (ab.1 = some j' ∨ ab.2 = some j') → h j ≡ h j' [MOD p]) ∧
    (∀ j, (ab.1 = some j ∨ ab.2 = some j) → ¬ h i ≡ h j [MOD p])))).card : ℝ)) / ((Nat.totient n : ℕ) : ℝ))) ≤ Real.exp (2 * ((k : ℝ) + 1) ^ 2 * (Real.log (T : ℝ) + 2)) := by sorry

Source

GPY twisted absolute bounds: unconditional absolute/tail control for the twisted Mertens sums (local file GPYTwistedMertens.lean); the asymptotic twisted Mertens main term is NOT proved and NOT claimed.

View graph