The prescribed primal and dual horizons imply objective-gap and terminal-gradient bounds.

noncomputable def V7.Stage4AboveTwoDualPhase.plateauU (p eta : ℝ) (n : ℕ) : ScalarSeq

The scaled quadratic weight sequence held constant from the terminal index onward.

Equations

• V7.Stage4AboveTwoDualPhase.plateauU p eta n k = if k < n then V7.aboveGamma p eta n * (↑k + 1) ^ 2 else V7.aboveGamma p eta n * ↑n ^ 2

noncomputable def V7.Stage4AboveTwoDualPhase.plateauDw (p eta : ℝ) (n : ℕ) : ScalarSeq

The increments of the scaled quadratic weight sequence with terminal plateau.

Equations

• V7.Stage4AboveTwoDualPhase.plateauDw p eta n k = V7.Stage4AboveTwoDualPhase.plateauU p eta n k - if k = 0 then 0 else V7.Stage4AboveTwoDualPhase.plateauU p eta n (k - 1)

theorem V7.Stage4AboveTwoDualPhase.conjugate_budget_identity {p : ℝ} (hp : 2 < p) : conjugateExponent p * (1 + aboveBudgetExponent p) = 2

theorem V7.Stage4AboveTwoDualPhase.phaseOnePowerBound {d : ℕ} (p : ℝ) (hp : 2 < p) (n : ℕ) (hn : 1 ≤ n) (data : AbovePrimalPhaseData p d n) (hass : AbovePrimalPhaseAssumptions data) (z : Point d) (hzstar : data.oracle.value z = data.fstar) (hznorm : lpNorm p z ≤ 1) (hu : data.u = plateauU p (1 / p) n) (hdw : data.dw = plateauDw p (1 / p) n) : data.oracle.value (data.x n) - data.fstar ≤ aboveHp p / ↑n ^ ((p + 2) / p)

theorem V7.Stage4AboveTwoDualPhase.phaseOneHorizonBound {d : ℕ} (p : ℝ) (hp : 2 < p) (delta : ℝ) (hdelta : 0 < delta) (n : ℕ) (hn : n = ⌈(aboveHp p / delta) ^ (p / (p + 2))⌉₊) (data : AbovePrimalPhaseData p d n) (hass : AbovePrimalPhaseAssumptions data) (z : Point d) (hzstar : data.oracle.value z = data.fstar) (hznorm : lpNorm p z ≤ 1) (hu : data.u = plateauU p (1 / p) n) (hdw : data.dw = plateauDw p (1 / p) n) : data.oracle.value (data.x n) - data.fstar ≤ delta

theorem V7.Stage4AboveTwoDualPhase.phaseTwoEnergyBound {d : ℕ} (p : ℝ) (hp : 2 < p) (n : ℕ) (hn : 1 ≤ n) (delta : ℝ) (hdelta : 0 < delta) (data : AboveDualPhaseData p d n) (hass : AboveDualPhaseAssumptions data) (hgap0 : data.oracle.value (data.q 0) - sInf (Set.range data.oracle.value) ≤ delta) (hu : data.u = plateauU p (delta ^ conjugateExponent p / conjugateExponent p) n) (hdw : data.dw = plateauDw p (delta ^ conjugateExponent p / conjugateExponent p) n) : aboveHstar p (data.oracle.gradient (data.q n)) ≤ delta / (aboveGrowthConstant p * (delta ^ conjugateExponent p / conjugateExponent p) ^ aboveBudgetExponent p * ↑n ^ ((p + 2) / p)) + delta ^ conjugateExponent p / conjugateExponent p / 2

theorem V7.Stage4AboveTwoDualPhase.phaseTwoHorizonBound {d : ℕ} (p : ℝ) (hp : 2 < p) (delta : ℝ) (hdelta : 0 < delta) (n : ℕ) (hn : n = ⌈(aboveJp p / delta) ^ (p / (p + 2))⌉₊) (data : AboveDualPhaseData p d n) (hass : AboveDualPhaseAssumptions data) (hgap0 : data.oracle.value (data.q 0) - sInf (Set.range data.oracle.value) ≤ delta) (hu : data.u = plateauU p (delta ^ conjugateExponent p / conjugateExponent p) n) (hdw : data.dw = plateauDw p (delta ^ conjugateExponent p / conjugateExponent p) n) : aboveHstar p (data.oracle.gradient (data.q n)) ≤ delta ^ conjugateExponent p / conjugateExponent p ∧ lpNorm (conjugateExponent p) (data.oracle.gradient (data.q n)) ≤ delta

theorem V7.abovePhaseOneGapBound {d : ℕ} (p : ℝ) (hp : 2 < p) (n : ℕ) (hn : 1 ≤ n) (data : AbovePrimalPhaseData p d n) (hass : AbovePrimalPhaseAssumptions data) (z : Point d) (hzstar : data.oracle.value z = data.fstar) (hznorm : lpNorm p z ≤ 1) (hu : data.u = Stage4AboveTwoDualPhase.plateauU p (1 / p) n) (hdw : data.dw = Stage4AboveTwoDualPhase.plateauDw p (1 / p) n) : data.oracle.value (data.x n) - data.fstar ≤ aboveHp p / ↑n ^ ((p + 2) / p)

theorem V7.abovePhaseOneHorizonBound {d : ℕ} (p : ℝ) (hp : 2 < p) (delta : ℝ) (hdelta : 0 < delta) (n : ℕ) (hn : n = ⌈(aboveHp p / delta) ^ (p / (p + 2))⌉₊) (data : AbovePrimalPhaseData p d n) (hass : AbovePrimalPhaseAssumptions data) (z : Point d) (hzstar : data.oracle.value z = data.fstar) (hznorm : lpNorm p z ≤ 1) (hu : data.u = Stage4AboveTwoDualPhase.plateauU p (1 / p) n) (hdw : data.dw = Stage4AboveTwoDualPhase.plateauDw p (1 / p) n) : data.oracle.value (data.x n) - data.fstar ≤ delta

theorem V7.abovePhaseTwoEnergyBound {d : ℕ} (p : ℝ) (hp : 2 < p) (n : ℕ) (hn : 1 ≤ n) (delta : ℝ) (hdelta : 0 < delta) (data : AboveDualPhaseData p d n) (hass : AboveDualPhaseAssumptions data) (hgap0 : data.oracle.value (data.q 0) - sInf (Set.range data.oracle.value) ≤ delta) (hu : data.u = Stage4AboveTwoDualPhase.plateauU p (delta ^ conjugateExponent p / conjugateExponent p) n) (hdw : data.dw = Stage4AboveTwoDualPhase.plateauDw p (delta ^ conjugateExponent p / conjugateExponent p) n) : aboveHstar p (data.oracle.gradient (data.q n)) ≤ delta / (aboveGrowthConstant p * (delta ^ conjugateExponent p / conjugateExponent p) ^ aboveBudgetExponent p * ↑n ^ ((p + 2) / p)) + delta ^ conjugateExponent p / conjugateExponent p / 2

theorem V7.abovePhaseTwoTerminalGradientBound {d : ℕ} (p : ℝ) (hp : 2 < p) (delta : ℝ) (hdelta : 0 < delta) (n : ℕ) (hn : n = ⌈(aboveJp p / delta) ^ (p / (p + 2))⌉₊) (data : AboveDualPhaseData p d n) (hass : AboveDualPhaseAssumptions data) (hgap0 : data.oracle.value (data.q 0) - sInf (Set.range data.oracle.value) ≤ delta) (hu : data.u = Stage4AboveTwoDualPhase.plateauU p (delta ^ conjugateExponent p / conjugateExponent p) n) (hdw : data.dw = Stage4AboveTwoDualPhase.plateauDw p (delta ^ conjugateExponent p / conjugateExponent p) n) : aboveHstar p (data.oracle.gradient (data.q n)) ≤ delta ^ conjugateExponent p / conjugateExponent p ∧ lpNorm (conjugateExponent p) (data.oracle.gradient (data.q n)) ≤ delta