Calculus, convexity, minimizers, and growth of the scalar affine-quadratic-affine hard objective.

noncomputable def V7.Stage6StrictDeterministic.hardValue (eps H z : ℝ) : ℝ

The piecewise linear-quadratic hard objective in displacement coordinates.

Equations

• V7.Stage6StrictDeterministic.hardValue eps H z = if z ≤ H then -(2 * eps) * z else if z ≤ 3 * H then -(2 * eps) * z + 2 * eps / (2 * H) * (z - H) ^ 2 else 2 * eps * z - 4 * (2 * eps) * H

noncomputable def V7.Stage6StrictDeterministic.hardSlope (eps H z : ℝ) : ℝ

The continuous piecewise affine slope of the hard objective.

Equations

• V7.Stage6StrictDeterministic.hardSlope eps H z = if z ≤ H then -(2 * eps) else if z ≤ 3 * H then 2 * eps * (z / H - 2) else 2 * eps

theorem V7.Stage6StrictDeterministic.hardValue_of_le {eps H z : ℝ} (hz : z ≤ H) : hardValue eps H z = -(2 * eps) * z

theorem V7.Stage6StrictDeterministic.hardValue_of_middle {eps H z : ℝ} (hzH : H < z) (hz3 : z ≤ 3 * H) : hardValue eps H z = -(2 * eps) * z + 2 * eps / (2 * H) * (z - H) ^ 2

theorem V7.Stage6StrictDeterministic.hardValue_of_right {eps H z : ℝ} (hH : 0 ≤ H) (hz3 : 3 * H < z) : hardValue eps H z = 2 * eps * z - 4 * (2 * eps) * H

theorem V7.Stage6StrictDeterministic.hardSlope_of_le {eps H z : ℝ} (hz : z ≤ H) : hardSlope eps H z = -(2 * eps)

theorem V7.Stage6StrictDeterministic.hardSlope_of_middle {eps H z : ℝ} (hzH : H < z) (hz3 : z ≤ 3 * H) : hardSlope eps H z = 2 * eps * (z / H - 2)

theorem V7.Stage6StrictDeterministic.hardSlope_of_right {eps H z : ℝ} (hH : 0 ≤ H) (hz3 : 3 * H < z) : hardSlope eps H z = 2 * eps

theorem V7.Stage6StrictDeterministic.hardValue_hasDerivAt {eps H : ℝ} (hH : 0 < H) (z : ℝ) : HasDerivAt (hardValue eps H) (hardSlope eps H z) z

The literal frozen affine--quadratic--affine value has the literal frozen piecewise derivative, including both seams.

theorem V7.Stage6StrictDeterministic.hardValue_differentiable {eps H : ℝ} (hH : 0 < H) : Differentiable ℝ (hardValue eps H)

theorem V7.Stage6StrictDeterministic.deriv_hardValue {eps H : ℝ} (hH : 0 < H) (z : ℝ) : deriv (hardValue eps H) z = hardSlope eps H z

noncomputable def V7.Stage6StrictDeterministic.clippedCoordinate (H z : ℝ) : ℝ

The scaled displacement clipped to the interval from minus one to one.

Equations

• V7.Stage6StrictDeterministic.clippedCoordinate H z = min 1 (max (-1) (z / H - 2))

theorem V7.Stage6StrictDeterministic.hardSlope_eq_clipped {eps H z : ℝ} (hH : 0 < H) : hardSlope eps H z = 2 * eps * clippedCoordinate H z

theorem V7.Stage6StrictDeterministic.clippedCoordinate_monotone {H : ℝ} (hH : 0 < H) : Monotone (clippedCoordinate H)

theorem V7.Stage6StrictDeterministic.hardSlope_monotone {eps H : ℝ} (heps : 0 < eps) (hH : 0 < H) : Monotone (hardSlope eps H)

theorem V7.Stage6StrictDeterministic.hardValue_convex {eps H : ℝ} (heps : 0 < eps) (hH : 0 < H) : ConvexOn ℝ Set.univ (hardValue eps H)

Scalar convexity follows from the globally monotone literal derivative.

theorem V7.Stage6StrictDeterministic.clippedCoordinate_lipschitz (H x y : ℝ) : |clippedCoordinate H x - clippedCoordinate H y| ≤ |x / H - 2 - (y / H - 2)|

theorem V7.Stage6StrictDeterministic.hardSlope_lipschitz {eps H : ℝ} (heps : 0 < eps) (hH : 0 < H) (x y : ℝ) : |hardSlope eps H x - hardSlope eps H y| ≤ 2 * eps / H * |x - y|

theorem V7.Stage6StrictDeterministic.hardValue_at_minimizer {eps H : ℝ} (hH : 0 < H) : hardValue eps H (2 * H) = -3 * eps * H

theorem V7.Stage6StrictDeterministic.hardValue_minimum {eps H : ℝ} (heps : 0 < eps) (hH : 0 < H) (z : ℝ) : hardValue eps H (2 * H) ≤ hardValue eps H z

theorem V7.Stage6StrictDeterministic.hardValue_eq_minimizer_iff {eps H : ℝ} (heps : 0 < eps) (hH : 0 < H) (z : ℝ) : hardValue eps H z = hardValue eps H (2 * H) ↔ z = 2 * H

theorem V7.Stage6StrictDeterministic.hardValue_linear_lower {eps H : ℝ} (heps : 0 < eps) (hH : 0 < H) (z : ℝ) : 2 * eps * |z| - 4 * (2 * eps) * H ≤ hardValue eps H z

A global linear lower bound exposing both affine tails.