Coercive Lower Bound for a Finite Affine Maximum

This is a geometric coercivity statement for a finite affine maximum.

Let $E$ be a finite-dimensional real inner-product space, let $s\subseteq E$ be a nonempty finite set, and assume

Then there exists $c>0$ such that, for every function $a:E\to\mathbb R$, every $M\in\mathbb R$, and every $y\in E$, if $a(x)\le M$ for all $x\in s$, then

where affineMaximum is the maximum of $\langle x,y\rangle-a(x)$ over $x\in s$. The constant $c$ depends on the finite set and its neighborhood condition, but not on $a$, $M$, or $y$. The vertex intercept bound is required only on the elements of $s$.

Original Lean declaration header

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

theorem affineMaximum_coercive [FiniteDimensional ℝ E]
    (s : Finset E) (hs : s.Nonempty)
    (h0 : (0 : E) ∈ interior (convexHull ℝ (↑s : Set E))) :
    ∃ c : ℝ, 0 < c ∧ ∀ (a : E → ℝ) (M : ℝ), (∀ x ∈ s, a x ≤ M) →
      ∀ y, c * ‖y‖ - M ≤ affineMaximum s hs a y

Module navigation

Module: Analysis/Convex/AffineMaximum.

Next: eventually_affineMaximum_sub_le_legendre.

Source excerpt, lines 53–57 · Frozen source 408915f.