The initial gradient is bounded by smoothness times the distance to the minimizer set.

theorem V7.Stage5AboveTwoLowerS5F.minimizer_gradient_zero {p : ℝ} {d : ℕ} {x0 : Point d} (inst : PositiveInstance p d x0) {xstar : Point d} (hxstar : xstar ∈ MinimizerSet inst.oracle) : inst.oracle.gradient xstar = 0

theorem V7.Stage5AboveTwoLowerS5F.initial_gradient_le_LR {p : ℝ} {d : ℕ} {x0 : Point d} (inst : PositiveInstance p d x0) (hp : 2 < p) {L R : ℝ} (hL : 0 < L) (hinstL : inst.L = L) (hinstR : inst.R ≤ R) : lpNorm (conjugateExponent p) (inst.oracle.gradient x0) ≤ L * R