Volume Lower Bound for a Ball Cone

This gives the volume lower bound for the convex hull of a ball and an exterior point.

Let $E$ be a finite-dimensional real inner-product space with its measurable and Borel structures, and write $n=\dim E$. There exists $c>0$, depending only on $E$, such that for every $r>0$ and every $q\in E$ with $r\le\|q\|$,

The volume values are in $[0,\infty]$ (ENNReal), and the real expression is embedded using ofReal. The declaration is exists_pos_volume_convexHull_closedBall_union_singleton_ge_readable.

Original Lean declaration header

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

theorem exists_pos_volume_convexHull_closedBall_union_singleton_ge {E : Type*}
    [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E]
    [BorelSpace E] :
    ∃ c : ℝ, 0 < c ∧ ∀ r : ℝ, 0 < r → ∀ q : E, r ≤ ‖q‖ →
      ENNReal.ofReal (c * r ^ (Module.finrank ℝ E - 1) * ‖q‖) ≤
        (volume : Measure E) (convexHull ℝ (closedBall (0 : E) r ∪ {q}))

Module navigation

Module: Analysis/Convex/Alexandrov.

Previous: exists_unit_inner_le_infDist_frontier · Next: exists_pos_alexandrov_maximum_principle.

Source excerpt, lines 749–754 · Frozen source 408915f.