Interior of the Effective Domain from Finite Integral

This is the effective-domain interior lemma corresponding to Lemma 16 of Cordero–Erausquin–Klartag (arXiv:1304.0630v1).

Let $E$ be finite-dimensional, let $\mu$ be a finite Borel measure, and let $x_0$ lie in the interior of the convex hull of $\operatorname{supp}\mu$. Let $\phi:E\to\overline{\mathbb R}$ satisfy:

1. $\phi\geq0$;
2. its real epigraph is convex;
3. $x\mapsto\phi(x).\operatorname{toENNReal}$ is almost everywhere measurable;
4. $\int^\infty \phi.\operatorname{toENNReal}\,d\mu\neq+\infty$.

Then

Thus finite extended-real integral control forces finiteness on a neighborhood of every interior support point.

Original Lean declaration header

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

theorem mem_interior_setOf_ne_top_of_lintegral_ne_top [FiniteDimensional ℝ E] [BorelSpace E] (μ : Measure E) [IsFiniteMeasure μ] (x₀ : E) :
    x₀ ∈ interior (convexHull ℝ μ.support) →
      ∀ φ : E → EReal, (∀ x, 0 ≤ φ x) → Convex ℝ {p : E × ℝ | φ p.1 ≤ (p.2 : EReal)} →
        AEMeasurable (fun x => (φ x).toENNReal) μ →
        (∫⁻ x, (φ x).toENNReal ∂μ) ≠ ⊤ →
          x₀ ∈ interior {x | φ x ≠ ⊤}

Module navigation

Module: Probability/ConvexSupport.

Previous: exists_pos_le_measure_halfspace_of_mem_interior_convexHull_support · Next: exists_pos_le_measure_halfspace_of_mem_interior_convexHull_support_of_isFiniteMeasure.

Source excerpt, lines 434–439 · Frozen source 408915f.