Support Point On The Positive Side Of An Interior Point

This formalizes the support-side geometric ingredient associated with Lemma 16 of Cordero–Erausquin–Klartag, Moment measures (arXiv:1304.0630v1), cited there as an alternative formulation.

Let $E$ be a real inner-product normed additive group, let $\mu$ be a probability measure on $E$, and let $x_0\in E$ lie in the interior of the convex hull of the support of $\mu$. For every nonzero direction $u\in E$, there exists a support point $y$ such that

This is a basic separation fact used to obtain positive-mass halfspace information around an interior point.

Original Lean declaration header

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

theorem exists_mem_support_inner_sub_pos_of_mem_interior_convexHull (μ : ProbabilityMeasure E) {x₀ : E}
    (hx₀ : x₀ ∈ interior (convexHull ℝ (μ : Measure E).support)) {u : E} (hu : u ≠ 0) :
    ∃ y ∈ (μ : Measure E).support, 0 < ⟪u, y - x₀⟫

Module navigation

Module: Probability/ConvexSupport.

Next: exists_pos_ball_inner_sub_pos_of_mem_support.

Source excerpt, lines 55–57 · Frozen source 408915f.