Proof of Theorem 2.1, p. 246 — the shrunk copy X_ε = {(1 − ε)x* + εx : x ∈ X} has vol(X_ε) = εⁿ vol(X)

Proved

ConvexOptAlg.CenterGravity.thm_2_1_vol_scaled_copy

by mikedeng1 · Oct 5, 2026 · Mathlib 0df444a (Lean v4.33.1)

center-of-gravityconvex-geometryp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-bookp2o-v1volume

Let $\mathcal X\subset\mathbb R^n$ be a convex body, $x^*\in\mathcal X$ and $\varepsilon\in[0,1]$ . Set

\mathcal X_\varepsilon=\{(1-\varepsilon)x^*+\varepsilon x,\ x\in\mathcal X\}.

Then

\mathrm{vol}(\mathcal X_\varepsilon)=\varepsilon^n\,\mathrm{vol}(\mathcal X).

$\mathcal X_\varepsilon$ is the image of $\mathcal X$ under the homothety of centre $x^*$ and ratio $\varepsilon$ . Comparing its volume with that of the localizer sets is how the proof of Theorem 2.1 finds a point of $\mathcal X_\varepsilon$ that has been cut away.

Formalization Note $\mathcal X_\varepsilon$ is written as the image of $\mathcal X$ under $x\mapsto(1-\varepsilon)x^*+\varepsilon x$ . Volumes are extended non-negative reals, so $\varepsilon^n$ appears as the extended real $\varepsilon$ raised to the $n$ -th power.

Preamble

import Mathlib
import Definitions.Def_ConvexOptAlg_CenterGravity_Defs

open MeasureTheory
open scoped InnerProductSpace

Formal statement

namespace ConvexOptAlg.CenterGravity

/-- Bubeck, arXiv:1405.4980v2, proof of Theorem 2.1, p. 246: for `ε ∈ [0, 1]` and
`X_ε = {(1 - ε)x* + εx, x ∈ X}` one has `vol(X_ε) = εⁿ vol(X)`. Here `X` is the chapter's convex body and
`x* ∈ X`. -/
theorem thm_2_1_vol_scaled_copy {n : ℕ} {X : Set (EuclideanSpace ℝ (Fin n))} (hX : IsConvexBody X)
    {xstar : EuclideanSpace ℝ (Fin n)} (hxstar : xstar ∈ X) (ε : ℝ) (hε0 : 0 ≤ ε) (hε1 : ε ≤ 1) :
    volume ((fun x => (1 - ε) • xstar + ε • x) '' X) = ENNReal.ofReal ε ^ n * volume X := by sorry

end ConvexOptAlg.CenterGravity

Source

Bubeck, arXiv:1405.4980v2, proof of Theorem 2.1, p. 246

Human review

Endorsed by Shuze Chen · Oct 5, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 5, 2026
Confirmed by the mission captain (proposal self-audit).

View graph