Positive-Mass Ball Stable Under Nearby Halfspace Directions

This is a local support and halfspace lemma used in the geometric argument for 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, and let $x_0,u,y\in E$. Assume that $y\in\operatorname{supp}(\mu)$ and

Then there exist $\delta>0$ and $r>0$ such that the ball $B(y,r)$ has strictly positive $\mu$-measure and, for every $v\in E$ with $\|v-u\|<\delta$ and every $x\in B(y,r)$,

The result supplies a positive-mass neighborhood on which nearby directions define strict open halfspaces.

Original Lean declaration header

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

theorem exists_pos_ball_inner_sub_pos_of_mem_support (μ : ProbabilityMeasure E) {x₀ u y : E}
    (hy : y ∈ (μ : Measure E).support) (hpos : 0 < ⟪u, y - x₀⟫) :
    ∃ δ > 0, ∃ r > 0, 0 < (μ : Measure E) (Metric.ball y r) ∧
      ∀ v : E, ‖v - u‖ < δ → ∀ x ∈ Metric.ball y r, 0 < ⟪v, x - x₀⟫

Module navigation

Module: Probability/ConvexSupport.

Previous: exists_mem_support_inner_sub_pos_of_mem_interior_convexHull · Next: exists_pos_le_measure_halfspace_of_mem_interior_convexHull_support.

Source excerpt, lines 112–115 · Frozen source 408915f.