Nonnegative Affine Normalization of a Convex Potential

This is a pointwise affine-normalization lemma supporting Proposition 12 of Cordero–Erausquin–Klartag (CorderoKlartag2015).

Let $E$ be finite-dimensional, let $f:E\to\overline{\mathbb R}$ be a ConvexPotential, and assume $0$ lies in the interior of its finite effective domain. Then there exists $a\in E$ such that, for $g=\operatorname{affineSubtract}(f,a,(f(0))_{\mathrm{toReal}})$, $g$ is a ConvexPotential and

The conclusion concerns only pointwise normalization and does not involve measures or integrals.

Original Lean declaration header

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

theorem exists_nonnegative_origin_zero_affine [FiniteDimensional ℝ E]
    (f : E → EReal) (hf : ConvexPotential f)
    (h0 : (0 : E) ∈ interior {x | f x ≠ ⊤}) :
    ∃ a : E, let g := affineSubtract f a (f 0).toReal
      ConvexPotential g ∧ (∀ x, 0 ≤ g x) ∧ g 0 = 0

Module navigation

Module: Analysis/Convex/Affine.

Definition modules: Analysis/Convex/Legendre.

Supporting theorems: convex_epigraph_affineSubtract, exists_supporting_affine_at_zero.

Previous: convex_epigraph_affineSubtract.

Source excerpt, lines 124–128 · Frozen source 408915f.