Absolute twisted weight is nonnegative

Proved

gpy_twistedAbsWeight_nonneg

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

number-theory

The absolute twisted weight at any natural number n, defined as the absolute value of the Möbius function times the twisted weight, is nonnegative. This is immediate from nonnegativity of absolute value, stated here in fully unfolded Mathlib terms. It claims no asymptotic main term. Formalization Note: the statement is written out in Mathlib terms, with no local definitions.

Preamble

import Mathlib
open Classical

Formal statement

theorem gpy_twistedAbsWeight_nonneg {k : ℕ} (h : Fin k → ℕ) (i : Fin k) (hd he : Prop) [Decidable hd] [Decidable he] (n : ℕ) :
    (0 : ℝ) ≤ 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 : ℕ) : ℝ))) := 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