The completed below-two phases imply the requested physical terminal-gradient bound.

@[reducible, inline]

abbrev V7.Stage3BelowTwoS3F.LpSpace (p : ℝ) (d : ℕ) : Type

Finite-dimensional real coordinate space with the PiLp p norm.

Equations

• V7.Stage3BelowTwoS3F.LpSpace p d = PiLp (ENNReal.ofReal p) fun (x : Fin d) => ℝ

theorem V7.Stage3BelowTwoS3F.minimizerSet_isClosed {p : ℝ} {d : ℕ} {x0 : Point d} (inst : PositiveInstance p d x0) : IsClosed (MinimizerSet inst.oracle)

theorem V7.Stage3BelowTwoS3F.lpNorm_eq_transport_dist {d : ℕ} (p : ℝ) (hp : 1 ≤ p) (x y : Point d) : lpNorm p (x - y) = dist (WithLp.toLp (ENNReal.ofReal p) x) (WithLp.toLp (ENNReal.ofReal p) y)

theorem V7.Stage3BelowTwoS3F.exists_minimizer_at_radius {p : ℝ} {d : ℕ} {x0 : Point d} (inst : PositiveInstance p d x0) (hp : 1 < p) : ∃ xstar ∈ MinimizerSet inst.oracle, lpNorm p (xstar - x0) = inst.R

theorem V7.Stage3BelowTwoS3F.horizon_ge (p eps M D : ℝ) : 2 * √(M * D / ((p - 1) * eps)) ≤ ↑(horizon p eps M D)

theorem V7.Stage3BelowTwoS3F.one_le_horizon {p eps M D : ℝ} (hp : 1 < p) (heps : 0 < eps) (hM : 0 < M) (hD : 0 < D) : 1 ≤ horizon p eps M D

theorem V7.Stage3BelowTwoS3F.sInf_range_eq_of_min {d : ℕ} (f : Point d → ℝ) (z : Point d) (hz : ∀ (y : Point d), f z ≤ f y) : sInf (Set.range f) = f z

theorem V7.Stage3BelowTwoS3F.cocoPairHolds_exact_iff {d : ℕ} (p M : ℝ) (oracle : PairOracle d) (x y : Point d) : cocoPairHolds p M (O3.PairOracle.observe oracle x) (O3.PairOracle.observe oracle y) ↔ CocoercivityGuard p M oracle x y

theorem V7.Stage3BelowTwoS3F.terminal_gradient_le {d : ℕ} {x0 : Point d} (p eps M D : ℝ) (hp : 1 < p) (hp2 : p < 2) (heps : 0 < eps) (hM : 0 < M) (hD : 0 < D) (inst : PositiveInstance p d x0) (hDR : inst.R ≤ D) (hP : ∀ k < horizon p eps M D, cocoPairHolds p M (phaseOneObs p eps M D x0 inst.oracle k) (phaseOneObs p eps M D x0 inst.oracle (k + 1))) (hQ : ∀ k < horizon p eps M D, cocoPairHolds p M (phaseTwoObs p eps M D x0 inst.oracle k) (phaseTwoObs p eps M D x0 inst.oracle (k + 1))) : lpNorm (conjugateExponent p) (phaseTwoObs p eps M D x0 inst.oracle (horizon p eps M D)).gradient ≤ eps