Subgradient Expansion Implies Quadratic Function Expansion

This is an auxiliary second-order expansion lemma for convex functions.

Let $E$ be a finite-dimensional real inner-product space, let $f:E\to\mathbb R$ be convex on $E$, let $x,p\in E$, and let $B:E\to E$ be continuous linear. Assume that for every $\varepsilon>0$, for all $y$ sufficiently near $x$, every subgradient $q$ of $f$ at $y$ satisfies

Then, for every $\varepsilon>0$, for all $y$ sufficiently near $x$,

The declaration eventually_abs_sub_quadratic_le_of_subgradient_expansion_readable converts a first-order local estimate on all subgradients into a second-order local estimate for the function. The same symbol $\varepsilon$ is used in both quantified conclusions, exactly as in the Lean statement.

Original Lean declaration header

Within namespace FunctionalInequalities.Analysis. Shown in its original module context. Proof omitted.

theorem eventually_abs_sub_quadratic_le_of_subgradient_expansion [FiniteDimensional ℝ E] {f : E → ℝ}
    (hconv : ConvexOn ℝ univ f) {x p : E} {B : E →L[ℝ] E}
    (hexp : ∀ ε > 0, ∀ᶠ y in 𝓝 x, ∀ q : E, (∀ w, f y + ⟪q, w - y⟫ ≤ f w) →
      ‖q - p - B (y - x)‖ ≤ ε * ‖y - x‖) :
    ∀ ε > 0, ∀ᶠ y in 𝓝 x,
      |f y - f x - ⟪p, y - x⟫ - (1 / 2) * ⟪B (y - x), y - x⟫| ≤ ε * ‖y - x‖ ^ 2

Module navigation

Module: Analysis/Convex/Subgradient.

Supporting theorems: exists_subgradient_slope_le_inner_add.

Previous: volume_subgradient_two_points_eq_zero.

Source excerpt, lines 1439–1444 · Frozen source 408915f.