The above-two primal potential identity and terminal objective-gap estimate.

noncomputable def V7.Stage4AboveTwoPrimalRepair.primalPotential {d : ℕ} (p : ℝ) (n : ℕ) (data : AbovePrimalPhaseData p d n) (z : Point d) : ℝ

The primal mirror potential after subtracting the accumulated Bregman and smoothness gaps.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def V7.Stage4AboveTwoPrimalRepair.primalResidual {d : ℕ} (p : ℝ) (n : ℕ) (data : AbovePrimalPhaseData p d n) : ℝ

The accumulated gradient, mirror, and mixed-pairing residual of the actual primal trajectory.

Equations

• One or more equations did not get rendered due to their size.

theorem V7.Stage4AboveTwoPrimalRepair.primalPotential_le {d : ℕ} (p : ℝ) (hp : 2 < p) (n : ℕ) (data : AbovePrimalPhaseData p d n) (hass : AbovePrimalPhaseAssumptions data) (z : Point d) : primalPotential p n data z ≤ aboveH p z

theorem V7.Stage4AboveTwoPrimalRepair.primalResidual_lower {d : ℕ} (p : ℝ) (hp : 2 < p) (n : ℕ) (data : AbovePrimalPhaseData p d n) (hcoeff : AboveCoefficientAssumptions n data.u data.dw data.alpha data.c data.b) : primalResidual p n data ≥ -aboveErrorSum p n data.u data.dw

theorem V7.Stage4AboveTwoPrimalRepair.primalPotential_identity {d : ℕ} (p : ℝ) (hp : 2 < p) (n : ℕ) (data : AbovePrimalPhaseData p d n) (hass : AbovePrimalPhaseAssumptions data) (z : Point d) : primalPotential p n data z = data.u n * (data.oracle.value (data.x n) - data.oracle.value z) + aboveH p z + aboveHstar p (data.s n) - O3.pairing (data.s n) z + primalResidual p n data

theorem V7.Stage4AboveTwoPrimalRepair.terminalGap (p : ℝ) : 2 < p → ∀ (d n : ℕ) (data : AbovePrimalPhaseData p d n), AbovePrimalPhaseAssumptions data → ∀ (z : O3.Vec d), data.oracle.value z = data.fstar → data.oracle.value (data.x n) - data.fstar ≤ (aboveH p z + aboveErrorSum p n data.u data.dw) / data.u n

theorem V7.abovePrimalTerminalGap (p : ℝ) : 2 < p → ∀ (d n : ℕ) (data : AbovePrimalPhaseData p d n), AbovePrimalPhaseAssumptions data → ∀ (z : O3.Vec d), data.oracle.value z = data.fstar → data.oracle.value (data.x n) - data.fstar ≤ (aboveH p z + aboveErrorSum p n data.u data.dw) / data.u n