Real Convexity On The Effective Domain

This statement extracts ordinary real convexity from an extended-real convex epigraph.

Let $E$ be a real inner-product normed additive group and let $\phi:E\to\overline{\mathbb R}$. Assume:

1. $\phi(x)\ge 0$ for every $x\in E$.
2. The real epigraph

is convex.

Then the function $x\mapsto(\phi(x)).\operatorname{toReal}$ is ConvexOn on the effective domain

This is a technical bridge between extended-real convex potentials and ordinary real convex-analysis results.

Original Lean declaration header

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

lemma real_convexOn_effective_domain {φ : E → EReal} (h0 : ∀ x, 0 ≤ φ x)
    (hφ : Convex ℝ {p : E × ℝ | φ p.1 ≤ (p.2 : EReal)}) :
    ConvexOn ℝ {x | φ x ≠ ⊤} (fun x => (φ x).toReal)

Module navigation

Module: Probability/ConvexSupport.

Previous: exists_pos_le_measure_halfspace_of_mem_interior_convexHull_support_of_isFiniteMeasure · Next: strict_sublevel_convex_and_interior.

Source excerpt, lines 541–543 · Frozen source 408915f.