Concavity of parallel volume and its extremal bodies

For convex bodies K and L in a positive-dimensional Euclidean space of dimension n, the function t ↦ volume.real (K + t • L) ^ (n : ℝ)⁻¹ is concave on t ≥ 0. Here a convex body is compact and nonempty, but may have empty interior or zero volume. All volumes in these real-valued statements are finite by compactness.

Brunn–Minkowski also bounds this function below by the affine function with intercept volume.real K ^ (n : ℝ)⁻¹ and slope volume.real L ^ (n : ℝ)⁻¹. Consequently, whenever the right derivative at zero exists, it is at least this slope. Equality holds exactly when the whole volume profile equals that affine function. For the closed unit ball L, this is the concave tangent argument that turns a sharp first-variation identity into equality in Brunn–Minkowski at every positive radius. The derivative is an explicit hypothesis; no perimeter or first-variation formula is asserted.

When K and L both have positive volume, the equality case of Brunn–Minkowski for convex bodies identifies the extremal profiles: the right derivative at zero equals the volume root of L exactly when L is homothetic to K. For the closed unit ball L, the right derivative equals volume (closedBall 0 1) ^ (1 / n) exactly when K is a closed ball of positive radius. This is the step of the ball-rigidity argument for the sharp isoperimetric inequality that passes from a sharp first variation of parallel volume to the shape of K.

The concavity proof combines Convex.add_smul_interpolation with TauCeti.mul_volume_real_rpow_add_mul_volume_real_rpow_le. The derivative comparison uses Mathlib's ConcaveOn.slope_le_of_hasDerivWithinAt_Ioi. The homothety characterization applies Convex.volume_real_smul_add_smul_rpow_eq_iff at a single positive parameter.

References

• R. J. Gardner, The Brunn–Minkowski inequality, Bull. Amer. Math. Soc. 39 (2002), 355–405, for concavity of volume roots and the first Minkowski inequality.
• R. Schneider, Convex Bodies: The Brunn–Minkowski Theory, 2nd ed., Cambridge University Press, 2014, Section 7.2, for the equality case of the first Minkowski inequality.

theorem ConvexBody.concaveOn_volume_real_add_smul_rpow {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (K L : ConvexBody E) (hn : Module.finrank ℝ E ≠ 0) : ConcaveOn ℝ (Set.Ici 0) fun (t : ℝ) => MeasureTheory.volume.real (↑K + t • ↑L) ^ (↑(Module.finrank ℝ E))⁻¹

The dimension root of the volume of parallel convex bodies is concave for nonnegative parameters. No positive-volume or interior hypothesis is needed.

theorem ConvexBody.volume_real_rpow_add_mul_le_volume_real_add_smul_rpow {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (K L : ConvexBody E) (hn : Module.finrank ℝ E ≠ 0) {t : ℝ} (ht : 0 ≤ t) : MeasureTheory.volume.real ↑K ^ (↑(Module.finrank ℝ E))⁻¹ + t * MeasureTheory.volume.real ↑L ^ (↑(Module.finrank ℝ E))⁻¹ ≤ MeasureTheory.volume.real (↑K + t • ↑L) ^ (↑(Module.finrank ℝ E))⁻¹

The dimension root of parallel volume is bounded below by the affine function whose intercept and slope are the volume roots of the two convex bodies.

theorem ConvexBody.volume_real_add_smul_rpow_le_of_hasDerivWithinAt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (K L : ConvexBody E) (hn : Module.finrank ℝ E ≠ 0) {d : ℝ} (hd : HasDerivWithinAt (fun (t : ℝ) => MeasureTheory.volume.real (↑K + t • ↑L) ^ (↑(Module.finrank ℝ E))⁻¹) d (Set.Ioi 0) 0) {t : ℝ} (ht : 0 ≤ t) : MeasureTheory.volume.real (↑K + t • ↑L) ^ (↑(Module.finrank ℝ E))⁻¹ ≤ MeasureTheory.volume.real ↑K ^ (↑(Module.finrank ℝ E))⁻¹ + t * d

The dimension root of parallel volume is bounded above on nonnegative parameters by its tangent at zero whenever the right derivative exists.

theorem ConvexBody.volume_real_rpow_le_of_hasDerivWithinAt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (K L : ConvexBody E) (hn : Module.finrank ℝ E ≠ 0) {d : ℝ} (hd : HasDerivWithinAt (fun (t : ℝ) => MeasureTheory.volume.real (↑K + t • ↑L) ^ (↑(Module.finrank ℝ E))⁻¹) d (Set.Ioi 0) 0) : MeasureTheory.volume.real ↑L ^ (↑(Module.finrank ℝ E))⁻¹ ≤ d

If the right derivative of the parallel volume root exists at zero, it is bounded below by the volume root of the added convex body.

theorem ConvexBody.hasDerivWithinAt_volume_real_add_smul_rpow_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (K L : ConvexBody E) (hn : Module.finrank ℝ E ≠ 0) : HasDerivWithinAt (fun (t : ℝ) => MeasureTheory.volume.real (↑K + t • ↑L) ^ (↑(Module.finrank ℝ E))⁻¹) (MeasureTheory.volume.real ↑L ^ (↑(Module.finrank ℝ E))⁻¹) (Set.Ioi 0) 0 ↔ ∀ (t : ℝ), 0 ≤ t → MeasureTheory.volume.real (↑K + t • ↑L) ^ (↑(Module.finrank ℝ E))⁻¹ = MeasureTheory.volume.real ↑K ^ (↑(Module.finrank ℝ E))⁻¹ + t * MeasureTheory.volume.real ↑L ^ (↑(Module.finrank ℝ E))⁻¹

The right derivative at zero attains its Brunn–Minkowski lower bound exactly when the dimension root of parallel volume is affine on the entire nonnegative half-line. This includes zero-volume convex bodies.

theorem ConvexBody.hasDerivWithinAt_volume_real_add_smul_rpow_iff_exists_eq_vadd_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (K L : ConvexBody E) (hn : Module.finrank ℝ E ≠ 0) (hK : MeasureTheory.volume ↑K ≠ 0) (hL : MeasureTheory.volume ↑L ≠ 0) : HasDerivWithinAt (fun (t : ℝ) => MeasureTheory.volume.real (↑K + t • ↑L) ^ (↑(Module.finrank ℝ E))⁻¹) (MeasureTheory.volume.real ↑L ^ (↑(Module.finrank ℝ E))⁻¹) (Set.Ioi 0) 0 ↔ ∃ (v : E) (r : ℝ), 0 < r ∧ ↑L = v +ᵥ r • ↑K

For convex bodies K and L of positive volume, the right derivative at zero of the dimension root of parallel volume attains its Brunn–Minkowski lower bound volume L ^ (1 / n) exactly when L is homothetic to K.

theorem ConvexBody.hasDerivWithinAt_volume_real_add_smul_closedBall_rpow_iff_exists_eq_closedBall {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (K : ConvexBody E) (hn : Module.finrank ℝ E ≠ 0) (hK : MeasureTheory.volume ↑K ≠ 0) : HasDerivWithinAt (fun (t : ℝ) => MeasureTheory.volume.real (↑K + t • Metric.closedBall 0 1) ^ (↑(Module.finrank ℝ E))⁻¹) (MeasureTheory.volume.real (Metric.closedBall 0 1) ^ (↑(Module.finrank ℝ E))⁻¹) (Set.Ioi 0) 0 ↔ ∃ (c : E) (r : ℝ), 0 < r ∧ ↑K = Metric.closedBall c r

Ball rigidity from the sharp first variation of parallel volume. A convex body K of positive volume has parallel-volume root t ↦ volume (K + t • closedBall 0 1) ^ (1 / n) with right derivative volume (closedBall 0 1) ^ (1 / n) at zero exactly when K is a closed ball of positive radius.