Interval cancellation for the continuous fixed-divisor Dickman defect
ProvedErdos390.WholePaper.roughFriableContinuousFixedDivisorDefect_sub_abs_le_compactanalytic-number-theoryerdos-390erdos390-source-construction
Let A,B,y,d be natural numbers with y≥2, 0<d≤A≤B and log B≤5 log y. Set u_X=log X/log y, t=log d/log y, and D(X)=X[ρ(u_X−t)−ρ(u_X)]/d, where ρ is the Dickman function used in the source. Then the continuous fixed-divisor defects at the two endpoints satisfy the interval-length bound below. It preserves cancellation before taking absolute values and is the continuous contribution to the fixed-head interval shift.
Preamble
import Definitions.Def_erdos390_remaining_analytic_propositions_008
Formal statement
theorem Erdos390.WholePaper.roughFriableContinuousFixedDivisorDefect_sub_abs_le_compact : Erdos390.RemainingAnalyticGoal008_020 := by sorry
Source