Uniform Halfspace Mass For A Finite Measure

This formalizes the finite-measure version of the halfspace estimate associated with Lemma 16 of Cordero–Erausquin–Klartag, Moment measures (arXiv:1304.0630v1), cited there as an alternative formulation.

Let $E$ be finite-dimensional with a real inner product and Borel measurable structure. Let $\mu$ be a finite measure, and assume $x_0$ lies in the interior of the convex hull of $\operatorname{supp}(\mu)$. Then there exists $m\in\mathbb R$ such that

and, for every $u\in E$ with $\|u\|=1$,

The conclusion is uniform over all unit directions and uses the real-valued measure conversion.

Original Lean declaration header

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

theorem exists_pos_le_measure_halfspace_of_mem_interior_convexHull_support_of_isFiniteMeasure {E : Type*}
    [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    (μ : Measure E) [IsFiniteMeasure μ] {x₀ : E} (hx₀ : x₀ ∈ interior (convexHull ℝ μ.support)) :
    ∃ m : ℝ, 0 < m ∧ m ≤ μ.real Set.univ ∧ ∀ u : E, ‖u‖ = 1 → m ≤ μ.real {x | 0 < ⟪u, x - x₀⟫}

Module navigation

Module: Probability/ConvexSupport.

Supporting theorems: exists_pos_le_measure_halfspace_of_mem_interior_convexHull_support.

Previous: mem_interior_setOf_ne_top_of_lintegral_ne_top · Next: real_convexOn_effective_domain.

Source excerpt, lines 477–480 · Frozen source 408915f.