Inverse-log-square bound for lower natural Buchstab cells

Proved

Erdos390.WholePaper.abs_sum_roughSaiasFullyRealNaturalCells_lower_le_forty_invLogSq_compact

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

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

Let $X>0$ and $3\le a\le b\le X$ be natural numbers. Assume $b\le\lfloor\sqrt X\rfloor+1$ and $\log X/\log a\le5$ . Let $E_X(m)$ be the canonical fully-real natural Buchstab cell remainder. Then

\left|\sum_{m=a}^{b-1}E_X(m)\right|\le\frac{40X}{\log^2a}.

This supplies the sharp lower-block correction estimate.

Preamble

import Definitions.Def_erdos390_remaining_analytic_propositions_008

Formal statement

theorem Erdos390.WholePaper.abs_sum_roughSaiasFullyRealNaturalCells_lower_le_forty_invLogSq_compact : Erdos390.RemainingAnalyticGoal008_002 := by sorry

Source

https://github.com/ShouqiaoW/erdos/blob/61325b10bbdc29f4fb5e0618b414b9f2189333ad/390/lean/Erdos390/WholePaper/RoughSaiasSharpCorrectionTarget.lean#L949-L1135

View graph