Head-free smooth interval lower bound from divisor shifts

Proved

Erdos390.WholePaper.roughCanonical_headFreeSmoothInterval_lower_of_shift

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

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

Fix $W$ , $K>0$ , and a natural threshold $Y_0$ . Let $P_W$ and $d_W$ denote the rough-head modulus and density. Assume that for every $z\ge Y_0$ , positive divisor $d\mid P_W$ , $d\le X$ and $\log X\le5\log z$ ,

|\Psi(\lfloor X/d\rfloor,z)-\Psi(X,z)/d|\le KX/(d\log z)+3.

For natural endpoints with $Y_0\le y$ , $W\le y$ , $y\ge2$ , $P_W\le A\le B$ and $\log B\le5\log y$ , let $S(A,B;y)$ be the smooth interval and $S_W^*(A,B;y)$ its head-free subset. Then

|S_W^*(A,B;y)|\ge d_W|S(A,B;y)|-P_W\left(\frac{K(A+B)}{\log y}+6\right).

This makes the loss in the finite Möbius removal of head primes explicit.

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

Formal statement

theorem Erdos390.WholePaper.roughCanonical_headFreeSmoothInterval_lower_of_shift : Erdos390.RemainingAnalyticGoal008_018 := by sorry

Source

https://github.com/ShouqiaoW/erdos/blob/61325b10bbdc29f4fb5e0618b414b9f2189333ad/390/lean/Erdos390/WholePaper/BankPaperCanonicalRawBroadSurplusAsymptotic.lean#L365-L472

View graph