Uniform fixed-head divisor shift for friable counts
ProvedErdos390.WholePaper.exists_uniform_roughFixedHead_friableCount_shift_bound_compactanalytic-number-theoryerdos-390erdos390-source-construction
Fix a natural head cutoff , and let be its rough-head modulus. There exist and such that for all natural with , , and ,
Here ranges over the positive divisors of and counts friable integers. The constants are uniform across the fixed finite divisor family.
Preamble
import Definitions.Def_erdos390_remaining_analytic_propositions_008
Formal statement
theorem Erdos390.WholePaper.exists_uniform_roughFixedHead_friableCount_shift_bound_compact : Erdos390.RemainingAnalyticGoal008_013 := by sorry
Source