Convexification of a Lower Truncation

This formalizes the convexification statement corresponding to Proposition 12 of Cordero–Erausquin–Klartag (arXiv:1304.0630v1).

Let $\phi:E\to\overline{\mathbb R}$ and $M\in\mathbb R$. Assume that $\phi$ has at least one point where it is not $+\infty$. Define

Then $c$ is a convex proper lower-semicontinuous potential, and for every $x$,

Moreover, the conjugate is preserved:

for every $y$. The construction requires no convexity assumption on the original $\phi$.

Original Lean declaration header

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

theorem lowerTruncate_convexification (φ : E → EReal) (M : ℝ)
    (hfinite : ∃ x, φ x ≠ ⊤) :
    let g := lowerTruncate φ M
    let c := legendre (legendre g)
    ConvexPotential c ∧ LowerSemicontinuous c ∧ ProperPotential c ∧
      (∀ x, ((-M : ℝ) : EReal) ≤ c x ∧ c x ≤ g x) ∧
      (∀ y, legendre c y = legendre g y)

Module navigation

Module: Analysis/Convex/Legendre.

Supporting theorems: convex_epigraph_legendre, legendre_ne_bot_iff.

Previous: legendre_ne_bot_iff · Next: legendre_eq_interior_sup.

Source excerpt, lines 228–234 · Frozen source 408915f.