Monotonicity of Subgradient Images

This formalizes the comparison principle stated as Lemma 1.4.1 of Gutiérrez, The Monge–Ampère equation.

Let $E$ be a finite-dimensional real inner-product normed space, and let $u,v:E\to\mathbb R$ be convex on all of $E$. Let $\Omega\subseteq E$ be open and bounded. Assume:

1. $u(x)\le v(x)$ for every $x\in\Omega$;
2. $u(x)=v(x)$ for every $x\in\partial\Omega$.

Writing subgradientImage for the set of vectors that are subgradients at points of a set, the conclusion is

This is a finite-dimensional comparison result for convex subgradient images and is reusable in Alexandrov- and Monge–Ampère-type arguments.

Original Lean declaration header

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

theorem subgradientImage_subset_of_le
    [FiniteDimensional ℝ E] {u v : E → ℝ} (hu : ConvexOn ℝ univ u) (hv : ConvexOn ℝ univ v)
    {Ω : Set E} (hΩ : IsOpen Ω) (hb : Bornology.IsBounded Ω) (hle : ∀ x ∈ Ω, u x ≤ v x)
    (heq : ∀ x ∈ frontier Ω, u x = v x) : subgradientImage v Ω ⊆ subgradientImage u Ω

Module navigation

Module: Analysis/Convex/Subgradient.

Supporting theorems: support_of_max.

Previous: support_of_max · Next: volume_subgradient_two_points_eq_zero.

Source excerpt, lines 992–995 · Frozen source 408915f.