Centered Truncated Conjugate Properties

This describes the centered truncated conjugate around an interior point.

Let $E$ be a finite-dimensional real inner-product space, let $u:E\to\mathbb R$ be convex, let $M\in\mathbb R$, and let $x_c\in E$ satisfy $\|x_c\|<M$. Define

Then:

1. $f(p)\ge0$ for every $p$.
2. $f(p)=0$ exactly when $p$ is a subgradient of $u$ at $x_c$:

3. Every sublevel set $\{p:f(p)\le R\}$ is compact for every $R\in\mathbb R$.

This provides the compact sublevel structure needed for the contact-set uniqueness argument.

Original Lean declaration header

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

theorem truncatedConjugate_centered_spec {u : E → ℝ} (hconv : ConvexOn ℝ univ u) {M : ℝ} {xc : E}
    (hxc : ‖xc‖ < M) :
    (∀ p, 0 ≤ truncatedConjugate u M p - ⟪p, xc⟫ + u xc) ∧
    (∀ p, truncatedConjugate u M p - ⟪p, xc⟫ + u xc = 0 ↔ ∀ y, u xc + ⟪p, y - xc⟫ ≤ u y) ∧
    ∀ R : ℝ, IsCompact {p | truncatedConjugate u M p - ⟪p, xc⟫ + u xc ≤ R}

Module navigation

Module: Analysis/Convex/Caffarelli.

Supporting theorems: convexOn_truncatedConjugate, exists_truncatedConjugate_eq.

Previous: convexOn_truncatedConjugate · Next: isOpen_setOf_truncatedConjugate_maximizer_lt.

Source excerpt, lines 1332–1336 · Frozen source 408915f.