The completed above-two phases imply the requested physical terminal-gradient accuracy.
theorem
V7.Stage4AboveTwoFinalTrial.terminal_gradient_le
{d : ℕ}
{x0 : Point d}
(p eps M D : ℝ)
(hp : 2 < p)
(heps : 0 < eps)
(hM : 0 < M)
(hD : 0 < D)
(inst : PositiveInstance p d x0)
(hDR : inst.R ≤ D)
(hP :
∀ k < nF p eps M D,
Stage3BelowTwoS3F.cocoPairHolds p M (phaseOneObs p eps M D x0 inst.oracle k)
(phaseOneObs p eps M D x0 inst.oracle (k + 1)))
(hQ :
∀ k < nD p eps M D,
Stage3BelowTwoS3F.cocoPairHolds p M (phaseTwoObs p eps M D x0 inst.oracle k)
(phaseTwoObs p eps M D x0 inst.oracle (k + 1)))
: