Interior Domain at the Origin from a Lower Bound

This gives the normalization precursor for a convex potential.

Let $\mu$ be a finite Borel measure on a finite-dimensional real inner-product space. Assume:

1. $0$ lies in the interior of the convex hull of $\operatorname{supp}\mu$;
2. the identity map is integrable with respect to $\mu$;
3. $c$ is a convex potential that is potential-integrable with respect to $\mu$;
4. for some $M\in\mathbb R$, $-M\leq c(x)$ for every $x$.

Then

The result converts a signed lower-bounded convex potential into the nonnegative setting needed for effective-domain interior arguments.

Original Lean declaration header

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

theorem origin_mem_interior_domain_of_lower_bound (μ : Measure E) [IsFiniteMeasure μ]
    (h0 : (0 : E) ∈ interior (convexHull ℝ μ.support))
    (hfirst : Integrable (fun x : E => x) μ)
    (c : E → EReal) (hc : ConvexPotential c) (hp : PotentialIntegrable c μ)
    (M : ℝ) (hlower : ∀ x, ((-M : ℝ) : EReal) ≤ c x) :
    (0 : E) ∈ interior {x | c x ≠ ⊤}

Module navigation

Module: Probability/MomentMeasure/Normalization.

Definition modules: Analysis/Convex/Legendre, Probability/MomentMeasure/Basic.

Supporting theorems: convex_epigraph_affineSubtract, affineSubtract_potentialIntegrable, mem_interior_setOf_ne_top_of_lintegral_ne_top.

Source excerpt, lines 30–35 · Frozen source 408915f.