A moving prefix of positive relative length has uniform positive density

Proved

Erdos390.WholePaper.BankPaperRealization.exists_uniform_movingPrefix_density_lower_bound_of_fraction

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

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

Fix a head pattern $P$ , real $0<A<C$ , and $r_{\min}>0$ . There are $c_{\rm prefix}>0$ and $N_0$ such that for every $n\ge N_0$ and integer endpoint $k$ with $\lfloor An\rfloor<k\le\lfloor Cn\rfloor$ and normalized physical prefix fraction at least $r_{\min}$ ,

\lfloor Cn\rfloor>0,\qquad |\operatorname{structuredCell}(P,\lfloor An\rfloor,k,y_n)|\ge c_{\rm prefix}\lfloor Cn\rfloor.

Here the prefix fraction is exactly $(k/n-A)/(C-A)$ , using the real physical endpoints before rounding. The lower bound is uniform over the moving endpoint.

Preamble

import Definitions.Def_erdos390_remaining_analytic_propositions_007
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_005

Formal statement

theorem Erdos390.WholePaper.BankPaperRealization.exists_uniform_movingPrefix_density_lower_bound_of_fraction : Erdos390.RemainingAnalyticGoal007_007 := by sorry

Source

https://github.com/ShouqiaoW/erdos/blob/61325b10bbdc29f4fb5e0618b414b9f2189333ad/390/lean/Erdos390/WholePaper/BankPaperCanonicalSmoothSourceGuardedSharpValuationRateClosureMoving.lean#L258-L384

View graph