Supporting Hyperplane From an Interior Maximum

This is a technical supporting-hyperplane lemma for a convex function.

Let $E$ be a real inner-product normed additive group, let $u:E\to\mathbb R$ be convex on all of $E$, and let $\Omega\subseteq E$ be open. For $x_0,x_1,p\in E$ and $c\in\mathbb R$, assume $x_1\in\Omega$ and that $x_1$ maximizes

on over $\overline\Omega$. Then, for every $y\in E$,

The result identifies $p$ as a subgradient of $u$ at $x_1$, using the inline subgradient formulation rather than a separate subdifferential object. It is used to convert a maximizer of an affine perturbation into a global supporting inequality.

Original Lean declaration header

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

private lemma support_of_max
    {u : E → ℝ} {Ω : Set E} (hu : ConvexOn ℝ univ u) (hΩ : IsOpen Ω)
    (x₀ x₁ p : E) (c : ℝ) (hx₁ : x₁ ∈ Ω)
    (hmax :
      IsMaxOn (fun z => c + ⟪p, z - x₀⟫ - u z) (closure Ω) x₁) :
    ∀ y, u x₁ + ⟪p, y - x₁⟫ ≤ u y

Module navigation

Module: Analysis/Convex/Subgradient.

Previous: hasFDerivAt_of_convexOn_of_unique_subgradient · Next: subgradientImage_subset_of_le.

Source excerpt, lines 870–875 · Frozen source 408915f.