Primitive objects for the O3 probe

This file fixes the finite-dimensional real model, genuine-real ℓ_p functional, exact pair oracle, and an explicit deterministic interaction machine. In particular, a method can obtain objective information only by a query transition; the smoothness constant, solution radius, optimum value, and an optimizer are not fields of MethodInput.

@[reducible, inline]

abbrev O3.Vec (d : ℕ) : Type

The finite-dimensional real vector space used by the oracle and algorithms.

Equations

• O3.Vec d = O3.Point d

structure O3.PairOracle (d : ℕ) : Type

A supplied exact local first-order oracle.

• value : Vec d → ℝ

  The scalar objective value returned at a query point.

• gradient : Vec d → Vec d

  The gradient vector returned at a query point.

structure O3.Observation (d : ℕ) : Type

One counted exact pair-oracle response.

• point : Vec d

  The point at which this oracle response was obtained.

• value : ℝ

  The objective value returned by this query.

• gradient : Vec d

  The gradient vector returned by this query.

def O3.PairOracle.observe {d : ℕ} (oracle : PairOracle d) (x : Vec d) : Observation d

Package a query point with its exact objective value and gradient.

Equations

• oracle.observe x = { point := x, value := oracle.value x, gradient := oracle.gradient x }

structure O3.MethodInput (d : ℕ) : Type

The only numerical/problem data supplied to the O3 state machine.

• p : ℝ

  The exponent specifying the primal norm geometry.

• eps : ℝ

  The target bound on the dual norm of the returned gradient.

• x0 : Vec d

  The initial optimization point.

• z0 : Vec d

  The second point supplied for secant initialization.

• M0 : ℝ

  The observable initial scale obtained from the supplied secant data.

inductive O3.Action (d : ℕ) (State : Type) : Type

One deterministic machine action. A continuation receives exactly the pair returned at the point named by query.

• done {d : ℕ} {State : Type} (point : Vec d) : Action d State
• query {d : ℕ} {State : Type} (point : Vec d) (next : Observation d → State) : Action d State

structure O3.FirstOrderMethod (d : ℕ) : Type 1

An explicit deterministic first-order method. Its transition function is fixed before the oracle is supplied and can inspect the objective only through the observations delivered to Action.query.

• State : Type

  The internal states of the deterministic first-order method.

• initial : MethodInput d → self.State

  Construct the initial internal state from the permitted method inputs.

• action : self.State → Action d self.State

  Select the next oracle query or terminal action from an internal state.

structure O3.RunResult (d : ℕ) : Type

Result of a fuel-bounded execution. queries contains every counted post-initialization pair-oracle call, including rejected and terminal calls.

• returned : Vec d

  The point returned when the bounded execution succeeds.

• queries : List (Observation d)

  Every counted oracle response in the completed execution.

def O3.FirstOrderMethod.runFuel {d : ℕ} (method : FirstOrderMethod d) (oracle : PairOracle d) : ℕ → method.State → List (Observation d) → Option (RunResult d)

Execute at most the given number of machine steps while accumulating query responses.

Equations

• One or more equations did not get rendered due to their size.
• method.runFuel oracle 0 x✝¹ x✝ = none

def O3.FirstOrderMethod.run {d : ℕ} (method : FirstOrderMethod d) (oracle : PairOracle d) (input : MethodInput d) (fuel : ℕ) : Option (RunResult d)

Run a first-order method from its initial state with an empty query history.

Equations

• method.run oracle input fuel = method.runFuel oracle fuel (method.initial input) []

def O3.RunResult.callCount {d : ℕ} (result : RunResult d) : ℕ

The number of oracle responses in a completed run.

Equations

• result.callCount = result.queries.length

def O3.RunResult.returnedWasQueried {d : ℕ} (result : RunResult d) : Prop

The returned point really was queried; a bare unobserved terminal point is not enough for the frozen theorem.

Equations

• result.returnedWasQueried = (result.returned ∈ List.map O3.Observation.point result.queries)

def O3.IsCoordinateGradient {d : ℕ} (f : Vec d → ℝ) (grad : Vec d → Vec d) : Prop

The coordinate gradient represents the Frechet derivative. The ambient norm used by Mathlib for differentiability is immaterial in finite dimension.

Equations

• O3.IsCoordinateGradient f grad = ∀ (x : O3.Vec d), DifferentiableAt ℝ f x ∧ ∀ (h : O3.Vec d), (fderiv ℝ f x) h = O3.pairing (grad x) h

def O3.MinimizerSet {d : ℕ} (f : Vec d → ℝ) : Set (Vec d)

The set of global minimizers of the objective function.

Equations

• O3.MinimizerSet f = {x : O3.Vec d | ∀ (y : O3.Vec d), f x ≤ f y}

noncomputable def O3.minimizerDistance {d : ℕ} (p : ℝ) (f : Vec d → ℝ) (x0 : Vec d) : ℝ

The exact source-level ℓ_p distance to the nonempty minimizer set.

Equations

• O3.minimizerDistance p f x0 = sInf ((fun (x : O3.Vec d) => O3.lpNorm p (x - x0)) '' O3.MinimizerSet f)

def O3.IsLpSmooth {d : ℕ} (p q L : ℝ) (grad : Vec d → Vec d) : Prop

The gradient is Lipschitz from the primal ℓ_p norm to the specified dual norm.

Equations

• O3.IsLpSmooth p q L grad = ∀ (x y : O3.Vec d), O3.lpNorm q (grad x - grad y) ≤ L * O3.lpNorm p (x - y)

def O3.SecantWitness {d : ℕ} (p q M0 : ℝ) (grad : Vec d → Vec d) (x0 z0 : Vec d) : Prop

Exact nondegenerate secant initialization and its observable scale.

Equations

• O3.SecantWitness p q M0 grad x0 z0 = (z0 ≠ x0 ∧ grad z0 ≠ grad x0 ∧ M0 = O3.lpNorm q (grad z0 - grad x0) / O3.lpNorm p (z0 - x0) ∧ 0 < M0)

def O3.IsConvexObjective {d : ℕ} (f : Vec d → ℝ) : Prop

Exact convexity hypothesis from the frozen source.

Equations

• O3.IsConvexObjective f = ConvexOn ℝ Set.univ f

structure O3.AdmissibleInstance (d : ℕ) (p : ℝ) : Type

One complete admissible instance. The algorithm never receives this structure; it is used only by the correctness theorem.

• f : Vec d → ℝ

  The objective function of the admissible optimization instance.

• grad : Vec d → Vec d

  The coordinate gradient of the objective.

• L : ℝ

  The positive smoothness bound used in the instance's analytic certificate.

• eps : ℝ

  The requested terminal gradient tolerance.

• x0 : Vec d

  The point from which the method starts.

• z0 : Vec d

  The second point in the nondegenerate secant initialization.

• M0 : ℝ

  The initial scale witnessed by the secant data.

• p_gt_one : 1 < p
• L_pos : 0 < self.L
• eps_pos : 0 < self.eps
• gradient_spec : IsCoordinateGradient self.f self.grad
• convex : IsConvexObjective self.f
• minimizer_nonempty : (MinimizerSet self.f).Nonempty
• smooth : IsLpSmooth p (conjugateExponent p) self.L self.grad
• secant : SecantWitness p (conjugateExponent p) self.M0 self.grad self.x0 self.z0

def O3.AdmissibleInstance.oracle {d : ℕ} {p : ℝ} (P : AdmissibleInstance d p) : PairOracle d

The exact value-gradient oracle associated with an admissible instance.

Equations

• P.oracle = { value := P.f, gradient := P.grad }

def O3.AdmissibleInstance.methodInput {d : ℕ} {p : ℝ} (P : AdmissibleInstance d p) : MethodInput d

Extract the observable numerical inputs supplied to the method.

Equations

• P.methodInput = { p := p, eps := P.eps, x0 := P.x0, z0 := P.z0, M0 := P.M0 }

noncomputable def O3.AdmissibleInstance.radius {d : ℕ} {p : ℝ} (P : AdmissibleInstance d p) : ℝ

The primal-norm distance from the initial point to the minimizer set.

Equations

• P.radius = O3.minimizerDistance p P.f P.x0

noncomputable def O3.AdmissibleInstance.condition {d : ℕ} {p : ℝ} (P : AdmissibleInstance d p) : ℝ

The dimensionless quantity L R / ε governing the complexity bounds.

Equations

• P.condition = P.L * P.radius / P.eps

noncomputable def O3.AdmissibleInstance.conditionBar {d : ℕ} {p : ℝ} (P : AdmissibleInstance d p) : ℝ

The condition quantity truncated below at one.

Equations

• P.conditionBar = max 1 P.condition

def O3.RunResult.hasTargetGradient {d : ℕ} {p : ℝ} (P : AdmissibleInstance d p) (result : RunResult d) : Prop

The returned point's gradient satisfies the prescribed dual-norm tolerance.

Equations

• O3.RunResult.hasTargetGradient P result = (O3.lpNorm (O3.conjugateExponent p) (P.grad result.returned) ≤ P.eps)