Arbitrary-interval theta-weight variation at inverse-log-square scale
ProvedErdos390.WholePaper.sum_roughSaiasNaturalThetaWeightVariation_mul_fourth_le_invLogSq_compactanalytic-number-theoryerdos-390erdos390-source-construction
Let C≥0 and let X,a,b be natural numbers with 3≤a≤b≤X and log X/log a≤5. Define the natural-quotient theta weight Q_X(m)=roughSaiasNaturalMain(⌊X/m⌋,m)/log m. Then its discrete variation on the half-open integer interval [a,b), weighted by Cm/(log m)⁴, satisfies the explicit bound below. Unlike the upper-selector estimate, this covers arbitrary faces of the hyperbola decomposition without assuming X≤a².
Preamble
import Definitions.Def_erdos390_remaining_analytic_propositions_008
Formal statement
theorem Erdos390.WholePaper.sum_roughSaiasNaturalThetaWeightVariation_mul_fourth_le_invLogSq_compact : Erdos390.RemainingAnalyticGoal008_036 := by sorry
Source