Prove2Me

Explicit inverse-log-square majorant for the interval shift budget

Proved
Erdos390.WholePaper.roughSaiasIntervalFixedDivisorShiftBudget_sharp_le

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

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

For natural A,B,y,d with y≥2, d>0 and A≤B, let C⋆ denote roughSaiasSharpDefectConstant and use the sharp endpoint rate η(y)=10C⋆/(log y)². Denote by Bη(A,B;y,d) the source interval fixed-divisor budget: 6+(B−A)(log d+2)/(d log y)+Pη(⌊A/d⌋,⌊B/d⌋;y)+Pη(A,B;y)/d, where Pη(a,b;y)=η(y)(a+b)+5(b−a)/log y. Then this abstract budget is bounded by the explicit sharp budget below. No condition d≤A or upper restriction on log B is required for this deterministic comparison.

Bη(A,B;y,d)≤6+5log⁡y+(B−A)(log⁡d+12)dlog⁡y+20C⋆(A+B)d(log⁡y)2.B_\eta(A,B;y,d)\le6+\frac5{\log y}+\frac{(B-A)(\log d+12)}{d\log y}+\frac{20C_\star(A+B)}{d(\log y)^2}.
Preamble
import Definitions.Def_erdos390_remaining_analytic_propositions_008
import Mathlib
import Definitions.Def_erdos390_source_bank_interface
import Definitions.Def_erdos390_dickman_step_function
import Theorems.Thm_MediumPNT
import Definitions.Def_erdos390_analytic_foundations_001
import Theorems.Thm_Erdos390_Full_DickmanBasic_kernel_product_bound
import Theorems.Thm_Erdos390_Full_DickmanBasic_rho_pos_on_zero_five
import Theorems.Thm_Erdos390_Full_DickmanBasic_kernel_secondDerivative_first_bound
import Definitions.Def_erdos390_analytic_foundations_006
import Definitions.Def_erdos390_analytic_foundations_008
import Definitions.Def_erdos390_analytic_foundations_009
Formal statement
theorem Erdos390.WholePaper.roughSaiasIntervalFixedDivisorShiftBudget_sharp_le : Erdos390.RemainingAnalyticGoal008_028 := by sorry
Source
https://github.com/ShouqiaoW/erdos/blob/61325b10bbdc29f4fb5e0618b414b9f2189333ad/390/lean/Erdos390/WholePaper/RoughSaiasSharpFixedHeadIntervalShift.lean#L475-L585

View graph