Moving prefixes have sharp normalized Dickman divisibility profiles
ProvedErdos390.WholePaper.BankPaperRealization.exists_uniform_movingPrefix_uniformAverage_divInd_paper_bound_of_fraction_compactanalytic-number-theoryerdos-390erdos390-source-construction
Write , , , and . Fix a head pattern , , and . There exist such that whenever , , and the physical prefix fraction is at least , the prefix cell is nonempty and
This holds simultaneously for every integer with , all prime factors at most , and . The constant and threshold do not depend on the moving prefix or divisor. The physical prefix fraction means exactly .
Preamble
import Definitions.Def_erdos390_remaining_analytic_propositions_007
Formal statement
theorem Erdos390.WholePaper.BankPaperRealization.exists_uniform_movingPrefix_uniformAverage_divInd_paper_bound_of_fraction_compact : Erdos390.RemainingAnalyticGoal007_008 := by sorry
Source