Linear lower bound for the raw smooth correction pool
ProvedErdos390.WholePaper.eventually_bankPaperCanonicalRawSmoothBasePool_linear_lower_compactanalytic-number-theoryerdos-390erdos390-source-construction
Fix natural parameters and a real . Let be the canonical upper-tail length and the raw head-free smooth base pool. With the rough-head density and the canonical Dickman pool floor, eventually
The quantifier is over all sufficiently large natural .
This supplies positive linear capacity for label one, which is excluded from the nonsmooth active-row estimate.
Preamble
import Definitions.Def_erdos390_remaining_analytic_propositions_008
Formal statement
theorem Erdos390.WholePaper.eventually_bankPaperCanonicalRawSmoothBasePool_linear_lower_compact : Erdos390.RemainingAnalyticGoal008_004 := by sorry
Source