The raw smooth base pool inherits the moving-prefix valuation profile
ProvedErdos390.WholePaper.BankPaperRealization.exists_uniform_rawSmoothBasePool_valuation_mean_profile_paperRate_compactanalytic-number-theoryerdos-390erdos390-source-construction
Write , , , and . For a prime put and , where is the paper Dickman divisibility main term. Fix , natural , and . There are such that for every and , the canonical raw smooth-base pool for width , multiplicity , and upper-tail length associated to is nonempty and
This is the label-one, head-free broad pool used by the smooth source construction.
Preamble
import Definitions.Def_erdos390_remaining_analytic_propositions_007
Formal statement
theorem Erdos390.WholePaper.BankPaperRealization.exists_uniform_rawSmoothBasePool_valuation_mean_profile_paperRate_compact : Erdos390.RemainingAnalyticGoal007_010 := by sorry
Source