Ordered compact bounded-variation translation estimate
ProvedErdos390.WholePaper.roughCompactBV_translation_le_of_le_compactanalytic-number-theoryerdos-390erdos390-source-construction
Let have total variation at most on . For ,
Only variation on the compact interval is needed. The estimate provides the translation input for the Saias correction analysis.
Preamble
import Definitions.Def_erdos390_remaining_analytic_propositions_008
Formal statement
theorem Erdos390.WholePaper.roughCompactBV_translation_le_of_le_compact : Erdos390.RemainingAnalyticGoal008_019 := by sorry
Source