Convexity And Interior Of A Strict Sublevel Set

This auxiliary lemma concerns strict sublevel geometry for an extended-real convex function.

Let $E$ be finite-dimensional with a real inner product, and let $\phi:E\to\overline{\mathbb R}$. Assume:

1. $\phi(x)\ge0$ for every $x$.
2. The real epigraph of $\phi$ is convex.
3. $x_0$ lies in the interior of $\{x:\phi(x)\ne+\infty\}$.
4. $\phi(y)<\phi(x_0)$.

Then the strict sublevel set

is convex and has nonempty interior.

The result is an internal geometric component for pointwise control of convex extended-real functions.

Original Lean declaration header

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

private lemma strict_sublevel_convex_and_interior {φ : E → EReal}
    (h0 : ∀ x, 0 ≤ φ x) (hφ : Convex ℝ {p : E × ℝ | φ p.1 ≤ (p.2 : EReal)})
    {x₀ y : E} (hx₀ : x₀ ∈ interior {x | φ x ≠ ⊤}) (hy : φ y < φ x₀) :
    Convex ℝ {x | φ x < φ x₀} ∧ (interior {x | φ x < φ x₀}).Nonempty

Module navigation

Module: Probability/ConvexSupport.

Supporting theorems: real_convexOn_effective_domain.

Previous: real_convexOn_effective_domain · Next: exists_pos_le_mul_lintegral_toReal_of_convex_epigraph.

Source excerpt, lines 565–568 · Frozen source 408915f.