Endpoint variation bound for the Saias–Dickman correction
ProvedErdos390.WholePaper.roughSaiasDickmanCorrection_difference_abs_le_compactanalytic-number-theoryerdos-390erdos390-source-construction
Assume the source's compact bounded-variation translation principle. For natural , , and , let denote the source's Saias–Dickman correction. Then
This turns the compact translation estimate into an interval error bound for the correction term.
Preamble
import Definitions.Def_erdos390_remaining_analytic_propositions_008
Formal statement
theorem Erdos390.WholePaper.roughSaiasDickmanCorrection_difference_abs_le_compact : Erdos390.RemainingAnalyticGoal008_026 := by sorry
Source