Common-range formula for a quotient drop and base increment

Proved

Erdos390.WholePaper.roughSaiasBaseFreeFractionalIntegral_quotient_succ_sub_eq_common

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

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

Let $1\le q_1\le q_0$ and $m\ge2$ be natural numbers with $\log q_0/\log m\le5$ . Write $K(q,m,t)=D_\rho((\log q-\log t)/\log m)/\log m$ for the scaled Dickman kernel, where $D_\rho$ is the source-defined Dickman derivative, and $I(q,m)=\int_1^{m^5}\{t\}t^{-2}K(q,m,t)\,dt$ for its base-free fractional correction.

Then

I(q_1,m+1)-I(q_0,m)=\int_1^{m^5}\frac{\{t\}}{t^2}\bigl(K(q_1,m+1,t)-K(q_0,m,t)\bigr)\,dt.

The common cap permits variation estimates across changing natural quotients.

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

Formal statement

theorem Erdos390.WholePaper.roughSaiasBaseFreeFractionalIntegral_quotient_succ_sub_eq_common : Erdos390.RemainingAnalyticGoal008_025 := by sorry

Source

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

View graph