Uniform Positive Halfspace Mass For A Probability Measure

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

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

and, for every unit vector $u\in E$,

This gives a dimension-dependent uniform lower bound for all strict open halfspaces through $x_0$.

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 [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    (μ : ProbabilityMeasure E) {x₀ : E} (hx₀ : x₀ ∈ interior (convexHull ℝ (μ : Measure E).support)) :
    ∃ m : ℝ, 0 < m ∧ m ≤ 1 ∧
      ∀ u : E, ‖u‖ = 1 → m ≤ ((μ : Measure E) {x | 0 < ⟪u, x - x₀⟫}).toReal

Module navigation

Module: Probability/ConvexSupport.

Supporting theorems: exists_mem_support_inner_sub_pos_of_mem_interior_convexHull, exists_pos_ball_inner_sub_pos_of_mem_support.

Previous: exists_pos_ball_inner_sub_pos_of_mem_support · Next: mem_interior_setOf_ne_top_of_lintegral_ne_top.

Source excerpt, lines 305–308 · Frozen source 408915f.