Subgradient Realizing the One-Sided Convex Slope

This is an auxiliary max-formula statement for directional slopes of finite convex functions.

Let $E$ be a finite-dimensional real inner-product space and let $u:E\to\mathbb R$ be convex on all of $E$. For every $x,v\in E$, there exists $g\in E$ such that:

1. $g$ is a subgradient of $u$ at $x$:

2. For every $\varepsilon>0$, there exists $t>0$ with

Thus the pairing with $v$ is approximated from above by positive directional difference quotients, while the subgradient inequality supplies the corresponding lower bound. The declaration exists_subgradient_slope_le_inner_add_readable is useful for selecting subgradients compatible with one-sided directional derivatives.

Original Lean declaration header

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

theorem exists_subgradient_slope_le_inner_add {E : Type*} [NormedAddCommGroup E]
    [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {u : E → ℝ}
    (hconv : ConvexOn ℝ Set.univ u) (x v : E) :
    ∃ g : E, (∀ y, u x + ⟪g, y - x⟫ ≤ u y) ∧
      ∀ ε > 0, ∃ t > 0, (u (x + t • v) - u x) / t ≤ ⟪g, v⟫ + ε

Module navigation

Module: Analysis/Convex/Subgradient.

Previous: subgradient_mem_of_ae_gradient_mem · Next: ConvexOn.ae_differentiableAt_of_isOpen.

Source excerpt, lines 208–212 · Frozen source 408915f.