Fixed-divisor shift of the Dickman main term
ProvedErdos390.WholePaper.roughFriableMain_fixedDivisorShift_compactanalytic-number-theoryerdos-390erdos390-source-construction
Let be natural numbers with , , and . Write and let be the Dickman function. Then
This quantifies both the floor loss and the change of the Dickman parameter caused by a fixed divisor.
Preamble
import Definitions.Def_erdos390_remaining_analytic_propositions_008
Formal statement
theorem Erdos390.WholePaper.roughFriableMain_fixedDivisorShift_compact : Erdos390.RemainingAnalyticGoal008_023 := by sorry
Source