Prove2Me

Fourth-power weighted variation of the natural theta weight

Proved
Erdos390.WholePaper.sum_roughSaiasNaturalThetaWeightVariation_mul_fourth_le_hyperbola_compact

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

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

Let C≥0C\ge0 and 2≤a≤b≤X2\le a\le b\le X be natural numbers with log⁡X/log⁡a≤5\log X/\log a\le5. Let ΘX(m)\Theta_X(m) be the natural Saias main term at (⌊X/m⌋,m)(\lfloor X/m\rfloor,m) divided by log⁡m\log m. Then

∑m=ab−1∣ΘX(m+1)−ΘX(m)∣Cmlog⁡4m≤16(CX(2+log⁡b)log⁡5a+CX(1+log⁡b)log⁡6a)+CXlog⁡5a(1+2log⁡a).\sum_{m=a}^{b-1}|\Theta_X(m+1)-\Theta_X(m)|\frac{Cm}{\log^4m}\le16\left(\frac{CX(2+\log b)}{\log^5a}+\frac{CX(1+\log b)}{\log^6a}\right)+\frac{CX}{\log^5a}\left(1+\frac2{\log a}\right).

This controls the lower-face Abel weight using the same logarithmic precision as the selector estimate.

Preamble
import Definitions.Def_erdos390_remaining_analytic_propositions_008
Formal statement
theorem Erdos390.WholePaper.sum_roughSaiasNaturalThetaWeightVariation_mul_fourth_le_hyperbola_compact : Erdos390.RemainingAnalyticGoal008_035 := by sorry
Source
https://github.com/ShouqiaoW/erdos/blob/61325b10bbdc29f4fb5e0618b414b9f2189333ad/390/lean/Erdos390/WholePaper/RoughSaiasSharpCorrectionTarget.lean#L1449-L1573

View graph