Attainment of the Truncated Conjugate

This states attainment and domination for a truncated conjugate.

Let $E$ be a finite-dimensional real inner-product space, let $u:E\to\mathbb R$ be continuous, let $M\ge0$, and let $p\in E$. The supremum over the closed ball $\overline B(0,M)$ is attained: there exists $x\in\overline B(0,M)$ such that

Moreover, every point of the ball gives a value no larger than the truncated conjugate:

The declaration is exists_truncatedConjugate_eq_readable. It is a compactness result and does not assert attainment of the unrestricted Legendre transform.

Original Lean declaration header

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

theorem exists_truncatedConjugate_eq {u : E → ℝ} (hu : Continuous u) {M : ℝ} (hM : 0 ≤ M) (p : E) :
    (∃ x ∈ closedBall (0 : E) M, truncatedConjugate u M p = ⟪p, x⟫ - u x) ∧
      ∀ x ∈ closedBall (0 : E) M, ⟪p, x⟫ - u x ≤ truncatedConjugate u M p

Module navigation

Module: Analysis/Convex/Caffarelli.

Previous: exists_exposed_contact_of_lt · Next: convexOn_truncatedConjugate.

Source excerpt, lines 1292–1294 · Frozen source 408915f.