The one-dimensional hard family has a unique minimizer and exact smoothness and radius constants.

noncomputable def V7.Stage6StrictDeterministic.hardOracle (eps : ℝ) (x0 : StrictPoint) (H : ℝ) : PairOracle 1

The one-dimensional hard objective paired with its exact derivative oracle.

Equations

• V7.Stage6StrictDeterministic.hardOracle eps x0 H = { value := V7.strictHardFamily eps x0 H, gradient := V7.strictHardDerivative eps x0 H }

def V7.Stage6StrictDeterministic.hardMinimizer (x0 : StrictPoint) (H : ℝ) : StrictPoint

The minimizer located a distance 2 * H to the right of the initial point.

Equations

• V7.Stage6StrictDeterministic.hardMinimizer x0 H x✝ = x0 0 + 2 * H

theorem V7.Stage6StrictDeterministic.strictPoint_ext {x y : StrictPoint} (h : x 0 = y 0) : x = y

@[simp]

theorem V7.Stage6StrictDeterministic.hardMinimizer_apply (x0 : StrictPoint) (H : ℝ) (i : Fin 1) : hardMinimizer x0 H i = x0 0 + 2 * H

theorem V7.Stage6StrictDeterministic.strictHardFamily_eq_hardValue (eps : ℝ) (x0 : StrictPoint) (H : ℝ) (x : StrictPoint) : strictHardFamily eps x0 H x = hardValue eps H (x 0 - x0 0)

theorem V7.Stage6StrictDeterministic.strictHardDerivative_apply (eps : ℝ) (x0 : StrictPoint) (H : ℝ) (x : StrictPoint) (i : Fin 1) : strictHardDerivative eps x0 H x i = hardSlope eps H (x 0 - x0 0)

noncomputable def V7.Stage6StrictDeterministic.scalarPairingCLM (a : ℝ) : StrictPoint →L[ℝ] ℝ

The continuous linear functional multiplying the unique coordinate by a.

Equations

• V7.Stage6StrictDeterministic.scalarPairingCLM a = ContinuousLinearMap.toSpanSingleton ℝ a ∘SL ContinuousLinearMap.proj 0

@[simp]

theorem V7.Stage6StrictDeterministic.scalarPairingCLM_apply (a : ℝ) (h : StrictPoint) : (scalarPairingCLM a) h = a * h 0

theorem V7.Stage6StrictDeterministic.strictHardFamily_hasFDerivAt {eps H : ℝ} (x0 : StrictPoint) (hH : 0 < H) (x : StrictPoint) : HasFDerivAt (strictHardFamily eps x0 H) (scalarPairingCLM (hardSlope eps H (x 0 - x0 0))) x

theorem V7.Stage6StrictDeterministic.strictHard_coordinateGradient {eps H : ℝ} (x0 : StrictPoint) (hH : 0 < H) : O3.IsCoordinateGradient (strictHardFamily eps x0 H) (strictHardDerivative eps x0 H)

theorem V7.Stage6StrictDeterministic.strictHard_convex {eps H : ℝ} (x0 : StrictPoint) (heps : 0 < eps) (hH : 0 < H) : O3.IsConvexObjective (strictHardFamily eps x0 H)

theorem V7.Stage6StrictDeterministic.strictHard_coercive {eps H : ℝ} (x0 : StrictPoint) (heps : 0 < eps) (hH : 0 < H) : IsCoerciveReal (strictHardFamily eps x0 H)

theorem V7.Stage6StrictDeterministic.strictHard_uniqueMinimizer {eps H : ℝ} (x0 : StrictPoint) (heps : 0 < eps) (hH : 0 < H) : UniqueMinimizer (strictHardFamily eps x0 H) (hardMinimizer x0 H)

theorem V7.Stage6StrictDeterministic.strictHard_exactLipschitz {eps H : ℝ} (x0 : StrictPoint) (heps : 0 < eps) (hH : 0 < H) : ExactGradientLipschitzConstant (hardOracle eps x0 H) (2 * eps / H)

theorem V7.Stage6StrictDeterministic.strictHard_radius (x0 : StrictPoint) {H : ℝ} (hH : 0 < H) : |hardMinimizer x0 H 0 - x0 0| = 2 * H

theorem V7.Stage6StrictDeterministic.strictHardInstance (eps : ℝ) (x0 : StrictPoint) (H : ℝ) (heps : 0 < eps) (hH : 0 < H) : StrictHardInstance eps x0 H (2 * eps / H) (2 * H) (hardOracle eps x0 H) (hardMinimizer x0 H)

Full frozen hard-instance package with the exact choices L=2 eps/H, R=2H, and normalization four.