Inverse-log-square endpoint approximation from the normal-form defect
ProvedErdos390.WholePaper.roughSaiasInvLogSqEndpointApproximationUpToFive_of_defect_compactanalytic-number-theoryerdos-390erdos390-source-construction
Let and . Suppose the reverse normal-form defect satisfies whenever , , and . Let , where the latter is the canonical reciprocal-log prime contraction threshold. Then for all natural and with , the Saias endpoint error satisfies
This produces the sharp endpoint envelope on all five constructed faces from the explicit defect bound.
Preamble
import Definitions.Def_erdos390_remaining_analytic_propositions_008
Formal statement
theorem Erdos390.WholePaper.roughSaiasInvLogSqEndpointApproximationUpToFive_of_defect_compact : Erdos390.RemainingAnalyticGoal008_029 := by sorry
Source