Centered divisibility-prefix bound on a raw structured cell
ProvedErdos390.Full.PaperMovingPrefixMarkedCell.exists_uniform_movingPrefix_divInd_centered_boundanalytic-number-theoryerdos-390erdos390-source-construction
Write , , , and . For a head pattern , let be the positive -smooth integers in having exactly the valuations prescribed by . Fix a pattern and . Uniformly for integers with , , all prime factors of at most , and , there exist such that for , writing for the source uniform average on ,
The centered estimate preserves the marked modulus factor needed when summing prime-power contributions.
Preamble
import Definitions.Def_erdos390_remaining_analytic_propositions_004 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.Full.PaperMovingPrefixMarkedCell.exists_uniform_movingPrefix_divInd_centered_bound : Erdos390.RemainingAnalyticGoal004_005 := by sorry
Source