Truncated Conjugate Image Identification

This gives the Danskin-type identification of a truncated-conjugate subgradient image.

Let $E$ be a finite-dimensional real inner-product space, let $u:E\to\mathbb R$ be continuous and strictly convex, and let $M\ge0$. Let $S\subseteq E$ satisfy the interior-maximizer condition: for every $p\in S$ and every $x\in\overline B(0,M)$,

Then

This result converts a subgradient image of the truncated conjugate into an inverse subgradient image of $u$.

Original Lean declaration header

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

theorem subgradientImage_truncatedConjugate_eq {u : E → ℝ} (hu : Continuous u)
    (hstrict : StrictConvexOn ℝ univ u) {M : ℝ} (hM : 0 ≤ M) {S : Set E}
    (hS : ∀ p ∈ S, ∀ x ∈ closedBall (0 : E) M, truncatedConjugate u M p = ⟪p, x⟫ - u x → ‖x‖ < M) :
    subgradientImage (truncatedConjugate u M) S = {x | ∃ p ∈ S, ∀ y, u x + ⟪p, y - x⟫ ≤ u y}

Module navigation

Module: Analysis/Convex/Caffarelli.

Definition modules: Analysis/Convex/Subgradient.

Supporting theorems: exists_truncatedConjugate_eq, n7_subgradient_eq_maximizer.

Previous: n7_subgradient_eq_maximizer · Next: eq_of_two_contacts_below.

Source excerpt, lines 1661–1664 · Frozen source 408915f.