The proof-side convex smooth optimization instance and its condition number.

Objectives are differentiable and convex on the whole finite-dimensional real space, with an attained minimum and a positive global Lipschitz-gradient bound from the primal norm to its dual. MainStatement restricts the exponent to finite real p > 1 and separately requires supplied nondegenerate secant initialization. Its query count starts after initialization. The strict-local and known-parameter lower bounds use the separate method models in StrictModel and LowerBoundStatements.

def V7.IsCoordinateGradient {d : ℕ} (oracle : PairOracle d) : Prop

The oracle's gradient is the coordinate gradient of its value function.

Equations

• V7.IsCoordinateGradient oracle = O3.IsCoordinateGradient oracle.value oracle.gradient

def V7.MinimizerSet {d : ℕ} (oracle : PairOracle d) : Set (Point d)

The set of global minimizers of the oracle's value function.

Equations

• V7.MinimizerSet oracle = O3.MinimizerSet oracle.value

noncomputable def V7.minimizerDistance {d : ℕ} (p : ℝ) (oracle : PairOracle d) (x0 : Point d) : ℝ

The ℓp distance from the initial point to the objective's minimizer set.

Equations

• V7.minimizerDistance p oracle x0 = O3.minimizerDistance p oracle.value x0

def V7.IsLpSmooth {d : ℕ} (p L : ℝ) (oracle : PairOracle d) : Prop

The oracle gradient is L-Lipschitz from the primal norm to its dual norm.

Equations

• V7.IsLpSmooth p L oracle = O3.IsLpSmooth p (V7.conjugateExponent p) L oracle.gradient

structure V7.PositiveInstance (p : ℝ) (d : ℕ) (x0 : Point d) : Type

Proof-side objective certificate. It is never an algorithm input.

• oracle : PairOracle d

  The value-gradient oracle of the certified optimization instance.

• L : ℝ

  A positive global Lipschitz constant for the gradient.

• L_pos : 0 < self.L
• coordinateGradient : IsCoordinateGradient self.oracle
• convex : O3.IsConvexObjective self.oracle.value
• minimizerNonempty : (MinimizerSet self.oracle).Nonempty
• smooth : IsLpSmooth p self.L self.oracle

noncomputable def V7.PositiveInstance.R {p : ℝ} {d : ℕ} {x0 : Point d} (inst : PositiveInstance p d x0) : ℝ

The initial distance to the minimizer set.

Equations

• inst.R = V7.minimizerDistance p inst.oracle x0

noncomputable def V7.PositiveInstance.fstar {p : ℝ} {d : ℕ} {x0 : Point d} (inst : PositiveInstance p d x0) : ℝ

The common minimum value, expressed as an infimum over minimizers.

Equations

• inst.fstar = sInf (inst.oracle.value '' V7.MinimizerSet inst.oracle)

noncomputable def V7.conditionNumber {p : ℝ} {d : ℕ} {x0 : Point d} (inst : PositiveInstance p d x0) (eps : ℝ) : ℝ

The gradient-accuracy condition number L * R / eps.

Equations

• V7.conditionNumber inst eps = inst.L * inst.R / eps

noncomputable def V7.conditionBar {p : ℝ} {d : ℕ} {x0 : Point d} (inst : PositiveInstance p d x0) (eps : ℝ) : ℝ

The condition number truncated below at one.

Equations

• V7.conditionBar inst eps = max 1 (V7.conditionNumber inst eps)

def V7.PositiveStandingAssumptions {d : ℕ} (input : MethodInput d) (inst : PositiveInstance input.p d input.x0) : Prop

Exact model split: the secant relation is proof-side evidence about the primitive input, not an extra field of the method family.

Equations

• V7.PositiveStandingAssumptions input inst = (1 < input.p ∧ 0 < input.eps ∧ V7.SecantInitialization input inst.oracle)