Within-cell displacement of the fully-real fractional correction

Proved

Erdos390.WholePaper.roughSaiasFullyRealBaseFreeFractionalIntegral_hyperbola_cell_abs_sub_le

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

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

Let $X>0$ , $2\le a\le b\le X$ , $a\le m<b$ be natural numbers with $\log X/\log a\le5$ , and let $s\in[m,m+1]$ be real. Write $I_{\mathbb R}(q,z)$ for the fully-real base-free fractional integral, and $\mathcal O_{X,a}(m)$ for the integrated cell oscillation ledger. Then

\left|I_{\mathbb R}(X/s,s)-I_{\mathbb R}(X/(m+1),m+1)\right|\le\mathcal O_{X,a}(m).

The bound transfers pointwise kernel oscillation to the continuous correction integral.

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_009

Formal statement

theorem Erdos390.WholePaper.roughSaiasFullyRealBaseFreeFractionalIntegral_hyperbola_cell_abs_sub_le : Erdos390.RemainingAnalyticGoal008_027 := by sorry

Source

https://github.com/ShouqiaoW/erdos/blob/61325b10bbdc29f4fb5e0618b414b9f2189333ad/390/lean/Erdos390/WholePaper/RoughSaiasSharpVariation.lean#L2146-L2261

View graph