Strict deterministic and randomized oracle models, exact transcripts, and normalized hard instances.

@[reducible, inline]

abbrev V7.StrictPoint : Type

The one-dimensional real point space used for strict-oracle lower bounds.

Equations

• V7.StrictPoint = V7.Point 1

@[reducible, inline]

abbrev V7.StrictObservation : Type

An exact value-gradient observation in one dimension.

Equations

• V7.StrictObservation = V7.Observation 1

@[reducible, inline]

abbrev V7.StrictTranscript : Type

A finite chronological list of one-dimensional exact observations.

Equations

• V7.StrictTranscript = List V7.StrictObservation

@[instance_reducible]

instance V7.instMeasurableSpaceStrictObservation : MeasurableSpace StrictObservation

Natural Borel structure on one exact value-gradient observation.

Equations

• V7.instMeasurableSpaceStrictObservation = MeasurableSpace.comap (fun (obs : V7.StrictObservation) => (obs.point, obs.value, obs.gradient)) inferInstance

@[instance_reducible]

def V7.strictTranscriptMeasurableSpace : MeasurableSpace StrictTranscript

Cylinder sigma algebra on finite exact-pair transcripts, generated by length events and Borel events at each finite coordinate.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance V7.instMeasurableSpaceStrictTranscript : MeasurableSpace StrictTranscript

Equations

• V7.instMeasurableSpaceStrictTranscript = V7.strictTranscriptMeasurableSpace

structure V7.StrictLocalMethod : Type

A deterministic strict-local method sees only the supplied accuracy, initial point, and its finite exact-pair transcript.

• eps : ℝ

  The gradient accuracy requested from the strict local method.

• x0 : StrictPoint

  The initial point of the strict local method.

• nextQuery : StrictTranscript → StrictPoint

  The next query determined solely by the exact observation transcript.

• output : ℕ → StrictTranscript → StrictPoint

  The proposed output after a given finite query budget and transcript.

• nextQuery_measurable : Measurable self.nextQuery
• output_measurable (N : ℕ) : Measurable (self.output N)

structure V7.RandomizedStrictLocalMethod (Ω : Type u_1) [MeasurableSpace Ω] : Type u_1

A randomized strict method is a measurable seed-indexed family of strict methods. The adversarial instance is quantified after this whole family, not separately for each seed.

• run : Ω → StrictLocalMethod

  The strict deterministic method associated with each random seed.

• joint_nextQuery_measurable : Measurable fun (z : Ω × StrictTranscript) => (self.run z.1).nextQuery z.2
• joint_output_measurable (N : ℕ) : Measurable fun (z : Ω × StrictTranscript) => (self.run z.1).output N z.2

@[instance_reducible]

instance V7.instCoeFunRandomizedStrictLocalMethodForallStrictLocalMethod {Ω : Type u_1} [MeasurableSpace Ω] : CoeFun (RandomizedStrictLocalMethod Ω) fun (x : RandomizedStrictLocalMethod Ω) => Ω → StrictLocalMethod

Equations

• V7.instCoeFunRandomizedStrictLocalMethodForallStrictLocalMethod = { coe := V7.RandomizedStrictLocalMethod.run }

def V7.StrictTranscriptExact (oracle : PairOracle 1) (trace : StrictTranscript) : Prop

Every transcript entry is the exact observation of the one-dimensional oracle.

Equations

• V7.StrictTranscriptExact oracle trace = V7.TraceExact oracle trace

def V7.StrictAllFirstNQueriesFail (eps : ℝ) (oracle : PairOracle 1) (trace : StrictTranscript) (N : ℕ) : Prop

The transcript contains N queries, all with gradient magnitude above the target accuracy.

Equations

• V7.StrictAllFirstNQueriesFail eps oracle trace N = (List.length trace = N ∧ ∀ obs ∈ trace, eps < |oracle.gradient obs.point 0|)

def V7.StrictFiniteOutputFails (method : StrictLocalMethod) (oracle : PairOracle 1) (trace : StrictTranscript) (N : ℕ) : Prop

The method's finite-budget output has gradient magnitude above its target accuracy.

Equations

• V7.StrictFiniteOutputFails method oracle trace N = (method.eps < |oracle.gradient (method.output N trace) 0|)

def V7.StrictSuccessThrough (method : StrictLocalMethod) (oracle : PairOracle 1) (trace : StrictTranscript) (N : ℕ) : Prop

Some query before budget N, or the corresponding output, meets the gradient accuracy.

Equations

• V7.StrictSuccessThrough method oracle trace N = ((∃ obs ∈ List.take N trace, |oracle.gradient obs.point 0| ≤ method.eps) ∨ |oracle.gradient (method.output N trace) 0| ≤ method.eps)

def V7.ExactGradientLipschitzConstant (oracle : PairOracle 1) (L : ℝ) : Prop

The constant bounds every gradient difference and is the least such bound.

Equations

• One or more equations did not get rendered due to their size.

def V7.IsCoerciveReal (f : StrictPoint → ℝ) : Prop

The one-dimensional objective tends above every bound outside a sufficiently large interval.

Equations

• V7.IsCoerciveReal f = ∀ (B : ℝ), ∃ (R : ℝ), 0 ≤ R ∧ ∀ (x : V7.StrictPoint), R ≤ |x 0| → B ≤ f x

def V7.UniqueMinimizer (f : StrictPoint → ℝ) (xstar : StrictPoint) : Prop

The specified point is a global minimizer and is the only point attaining its value.

Equations

• V7.UniqueMinimizer f xstar = ((∀ (x : V7.StrictPoint), f xstar ≤ f x) ∧ ∀ (x : V7.StrictPoint), f x = f xstar → x = xstar)

noncomputable def V7.strictHardFamily (eps : ℝ) (x0 : StrictPoint) (H : ℝ) (x : StrictPoint) : ℝ

The affine--quadratic--affine family from thm:impossibility.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def V7.strictHardDerivative (eps : ℝ) (x0 : StrictPoint) (H : ℝ) (x : StrictPoint) : StrictPoint

The exact piecewise derivative of the affine-quadratic-affine hard family.

Equations

• V7.strictHardDerivative eps x0 H x x✝ = if x 0 - x0 0 ≤ H then -(2 * eps) else if x 0 - x0 0 ≤ 3 * H then 2 * eps * ((x 0 - x0 0) / H - 2) else 2 * eps

def V7.StrictHardInstance (eps : ℝ) (x0 : StrictPoint) (H L R : ℝ) (oracle : PairOracle 1) (xstar : StrictPoint) : Prop

The hard-family oracle has the required convexity, minimizer, and exact normalization properties.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def V7.strictAffineOracle (eps : ℝ) (x0 : StrictPoint) : PairOracle 1

The affine oracle matching the left tail of every hard-family instance.

Equations

• V7.strictAffineOracle eps x0 = { value := fun (x : O3.Vec 1) => -(2 * eps) * (x 0 - x0 0), gradient := fun (x : O3.Vec 1) (x_1 : Fin 1) => -(2 * eps) }

def V7.StrictNormalizedInstance (eps : ℝ) (x0 : StrictPoint) (L R : ℝ) (oracle : PairOracle 1) (xstar : StrictPoint) : Prop

A convex coercive exact-gradient instance with unique minimizer and condition number four.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def V7.strictHittingTime (method : StrictLocalMethod) (oracle : PairOracle 1) (traces : ℕ → StrictTranscript) : ENNReal

A source-level hitting-time carrier. top means no queried or returned small-gradient point is reached.

Equations

• V7.strictHittingTime method oracle traces = sInf {t : ENNReal | ∃ (N : ℕ), t = ↑N ∧ V7.StrictSuccessThrough method oracle (traces N) N}

def V7.StrictRunConsistent (method : StrictLocalMethod) (oracle : PairOracle 1) (trace : StrictTranscript) : Prop

The exact transcript follows the strict method's causal query rule.

Equations

• One or more equations did not get rendered due to their size.