Prove2Me

Upper-selector theta variation at inverse-log-square scale

Proved
Erdos390.WholePaper.roughSaiasNaturalThetaPNTVariationLedger_fourth_le_upper_invLogSq_compact

by doctosil · Sep 17, 2026 · Mathlib c5ea003 (Lean v4.30.0)

analytic-number-theoryerdos-390erdos390-source-construction

Let C≥0 and let X,M,Z be natural numbers satisfying 3≤M≤Z≤X, log X/log M≤5 and X≤M². Write Q_X(m)=roughSaiasNaturalMain(⌊X/m⌋,m)/log m for the natural-quotient theta weight. Its fourth-power PNT variation ledger is the sum over M<m≤Z−1 displayed below. In this upper-selector regime it satisfies the inverse-log-square estimate with constant 13, providing the required scale for the sharp correction bound.

∑M<m≤Z−1∣QX(m+1)−QX(m)∣ Cm(log⁡m)4≤13CX(log⁡M)2.\sum_{M<m\le Z-1}|Q_X(m+1)-Q_X(m)|\,\frac{Cm}{(\log m)^4}\le\frac{13CX}{(\log M)^2}.
Preamble
import Definitions.Def_erdos390_remaining_analytic_propositions_008
Formal statement
theorem Erdos390.WholePaper.roughSaiasNaturalThetaPNTVariationLedger_fourth_le_upper_invLogSq_compact : Erdos390.RemainingAnalyticGoal008_031 := by sorry
Source
https://github.com/ShouqiaoW/erdos/blob/61325b10bbdc29f4fb5e0618b414b9f2189333ad/390/lean/Erdos390/WholePaper/RoughSaiasSharpCorrectionTarget.lean#L1818-L1917

View graph