Sliding Lemma for the Subgradient Image

This formalizes the sliding lemma for the Alexandrov maximum principle.

Let $E$ be finite-dimensional, let $u:E\to\mathbb R$ be convex, and let $\Omega\subseteq E$ be open and bounded. Assume:

1. $u\ge0$ on $\partial\Omega$.
2. $x_0\in\Omega$ and $u(x_0)<0$.
3. For some $p\in E$, the affine function satisfies

for every $x\in\overline\Omega$.

Then $p$ belongs to the subgradient image of $u$ over $\Omega$:

The declaration is mem_subgradientImage_of_affine_le_of_nonneg_frontier_readable. It asserts membership in the image, not a specified point realizing the subgradient.

Original Lean declaration header

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

theorem mem_subgradientImage_of_affine_le_of_nonneg_frontier {E : Type*} [NormedAddCommGroup E]
    [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {u : E → ℝ} (hconv : ConvexOn ℝ univ u)
    {Ω : Set E} (hΩ : IsOpen Ω) (hb : Bornology.IsBounded Ω)
    (hfr : ∀ x ∈ frontier Ω, 0 ≤ u x) {x₀ : E} (hx₀ : x₀ ∈ Ω) (hneg : u x₀ < 0)
    {p : E} (hp : ∀ x ∈ closure Ω, u x₀ + ⟪p, x - x₀⟫ ≤ 0) : p ∈ subgradientImage u Ω

Module navigation

Module: Analysis/Convex/Alexandrov.

Definition modules: Analysis/Convex/Subgradient.

Previous: lintegral_subgradientImage_eq_of_map_gradient · Next: exists_unit_inner_le_infDist_frontier.

Source excerpt, lines 455–459 · Frozen source 408915f.