Brunn's concavity principle

Let s ⊆ P × F be convex, where F is a finite-dimensional real inner product space of dimension m. A weighted sum of two fibers of s lies in the fiber over the weighted base point, so the Brunn–Minkowski inequality in F shows that the dimension root of the fiber volume, p ↦ volume (Prod.mk p ⁻¹' s) ^ (1 / m), is concave on the projection Prod.fst '' s. This is Brunn's concavity principle. When the fibers have finite volume, a concave function on a finite-dimensional base is continuous on the interior of its domain, hence so is the fiber volume itself. No finiteness is needed for the continuity: if one fiber has infinite volume, then so does every fiber over the interior of the projection.

The main specialization concerns the hyperplane sections {y ∈ (ℝ ∙ e)ᗮ | y + t • e ∈ s} of a convex set s in a Euclidean space of dimension n, along a unit vector e. Their volume, raised to the power 1 / (n - 1), is concave in t on the interval ⟪e, s⟫. For a bounded Borel convex set, the volume of the part {x ∈ s | ⟪e, x⟫ ≤ c} below a hyperplane is the integral of the section volumes up to height c, and the continuity of the sections shows that it is differentiable, with derivative the section volume, at every interior height. These are the inputs for the classical analysis of equality cases in the Brunn–Minkowski inequality for convex bodies, which compares the volume distributions of two bodies along each direction.

No dimension assumption is made. In a zero-dimensional fiber space every nonempty fiber is the whole space and the dimension root is the constant 1 on the projection, so concavity and continuity hold trivially.

Main results

• Convex.concaveOn_volume_real_preimage_prodMk_rpow: Brunn's concavity principle for fibers.
• Convex.volume_preimage_prodMk_eq_top: one fiber of infinite volume makes every fiber over the interior of the projection infinite.
• Convex.continuousOn_volume_real_preimage_prodMk: continuity of fiber volumes on the interior of the projection.
• Convex.concaveOn_volume_real_hyperplaneSection_rpow: concavity of hyperplane sections.
• Convex.continuousOn_volume_real_hyperplaneSection: continuity of hyperplane sections.
• Convex.hasDerivAt_volume_real_sep_inner_le: the volume below a hyperplane has the section volume as derivative.
• TauCeti.volume_hyperplaneSection_rpow_mul_volume_hyperplaneSection_rpow_le: multiplicative Brunn–Minkowski for the hyperplane sections of two sets, at the weighted height.

References

• R. J. Gardner, The Brunn–Minkowski inequality, Bull. Amer. Math. Soc. 39 (2002), 355–405, Section 4, for Brunn's concavity principle as a consequence of the Brunn–Minkowski inequality.
• R. Schneider, Convex Bodies: The Brunn–Minkowski Theory, 2nd ed., Cambridge University Press, 2014, Section 7.1.

theorem Convex.mul_volume_preimage_prodMk_rpow_add_mul_volume_preimage_prodMk_rpow_le {P : Type u_1} {F : Type u_2} [AddCommGroup P] [Module ℝ P] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] [MeasurableSpace F] [BorelSpace F] {s : Set (P × F)} (hs : Convex ℝ s) {p q : P} (hp : (Prod.mk p ⁻¹' s).Nonempty) (hq : (Prod.mk q ⁻¹' s).Nonempty) {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) : ENNReal.ofReal a * MeasureTheory.volume (Prod.mk p ⁻¹' s) ^ (↑(Module.finrank ℝ F))⁻¹ + ENNReal.ofReal b * MeasureTheory.volume (Prod.mk q ⁻¹' s) ^ (↑(Module.finrank ℝ F))⁻¹ ≤ MeasureTheory.volume (Prod.mk (a • p + b • q) ⁻¹' s) ^ (↑(Module.finrank ℝ F))⁻¹

Brunn's concavity principle, extended form: the dimension root of the fiber volume of a convex set is concave along segments joining points with nonempty fibers. Fibers may have infinite volume, and no dimension assumption is needed.

theorem Convex.concaveOn_volume_real_preimage_prodMk_rpow {P : Type u_1} {F : Type u_2} [AddCommGroup P] [Module ℝ P] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] [MeasurableSpace F] [BorelSpace F] {s : Set (P × F)} (hs : Convex ℝ s) (hfin : ∀ (p : P), MeasureTheory.volume (Prod.mk p ⁻¹' s) ≠ ⊤) : ConcaveOn ℝ (Prod.fst '' s) fun (p : P) => MeasureTheory.volume.real (Prod.mk p ⁻¹' s) ^ (↑(Module.finrank ℝ F))⁻¹

Brunn's concavity principle: if every fiber of a convex set has finite volume, the dimension root of the fiber volume is concave on the projection of the set.

theorem Convex.volume_preimage_prodMk_eq_top {P : Type u_1} {F : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] [MeasurableSpace F] [BorelSpace F] {s : Set (P × F)} (hs : Convex ℝ s) {p z : P} (hp : MeasureTheory.volume (Prod.mk p ⁻¹' s) = ⊤) (hz : z ∈ interior (Prod.fst '' s)) : MeasureTheory.volume (Prod.mk z ⁻¹' s) = ⊤

If one fiber of a convex set has infinite volume, then so does every fiber over the interior of the projection of the set.

theorem Convex.continuousOn_volume_real_preimage_prodMk {P : Type u_1} {F : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] [FiniteDimensional ℝ P] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] [MeasurableSpace F] [BorelSpace F] {s : Set (P × F)} (hs : Convex ℝ s) : ContinuousOn (fun (p : P) => MeasureTheory.volume.real (Prod.mk p ⁻¹' s)) (interior (Prod.fst '' s))

The fiber volume of a convex set is continuous on the interior of the projection of the set. The fibers need not have finite volume: volume.real reads an infinite fiber volume as 0.

theorem TauCeti.smul_hyperplaneSection_add_smul_hyperplaneSection_subset {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (e : E) (K L : Set E) (a b s t : ℝ) : a • {y : ↥(ℝ ∙ e)ᗮ | ↑y + s • e ∈ K} + b • {y : ↥(ℝ ∙ e)ᗮ | ↑y + t • e ∈ L} ⊆ {y : ↥(ℝ ∙ e)ᗮ | ↑y + (a * s + b * t) • e ∈ a • K + b • L}

A weighted sum of hyperplane sections of two sets lies in the hyperplane section of their weighted sum, at the weighted height.

theorem Convex.mul_volume_hyperplaneSection_rpow_add_mul_volume_hyperplaneSection_rpow_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {s : Set E} (hs : Convex ℝ s) {e : E} (he : ‖e‖ = 1) {t u : ℝ} (ht : t ∈ (fun (x : E) => inner ℝ e x) '' s) (hu : u ∈ (fun (x : E) => inner ℝ e x) '' s) {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) : ENNReal.ofReal a * MeasureTheory.volume {y : ↥(ℝ ∙ e)ᗮ | ↑y + t • e ∈ s} ^ (↑(Module.finrank ℝ E - 1))⁻¹ + ENNReal.ofReal b * MeasureTheory.volume {y : ↥(ℝ ∙ e)ᗮ | ↑y + u • e ∈ s} ^ (↑(Module.finrank ℝ E - 1))⁻¹ ≤ MeasureTheory.volume {y : ↥(ℝ ∙ e)ᗮ | ↑y + (a * t + b * u) • e ∈ s} ^ (↑(Module.finrank ℝ E - 1))⁻¹

Brunn's concavity principle for hyperplane sections, extended form. Along a unit vector e in a space of dimension n, the (n - 1)-th root of the section volume of a convex set is concave on the heights at which the section is nonempty.

theorem Convex.concaveOn_volume_real_hyperplaneSection_rpow {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {s : Set E} (hs : Convex ℝ s) {e : E} (he : ‖e‖ = 1) (hfin : ∀ (t : ℝ), MeasureTheory.volume {y : ↥(ℝ ∙ e)ᗮ | ↑y + t • e ∈ s} ≠ ⊤) : ConcaveOn ℝ ((fun (x : E) => inner ℝ e x) '' s) fun (t : ℝ) => MeasureTheory.volume.real {y : ↥(ℝ ∙ e)ᗮ | ↑y + t • e ∈ s} ^ (↑(Module.finrank ℝ E - 1))⁻¹

Brunn's concavity principle for hyperplane sections. If the hyperplane sections of a convex set along a unit vector e have finite volume, then in a space of dimension n the (n - 1)-th root of their volume is concave on the interval ⟪e, s⟫.

theorem Convex.continuousOn_volume_real_hyperplaneSection {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {s : Set E} (hs : Convex ℝ s) {e : E} (he : ‖e‖ = 1) : ContinuousOn (fun (t : ℝ) => MeasureTheory.volume.real {y : ↥(ℝ ∙ e)ᗮ | ↑y + t • e ∈ s}) (interior ((fun (x : E) => inner ℝ e x) '' s))

The volume of the hyperplane sections of a convex set along a unit vector is continuous on the interior of the interval ⟪e, s⟫.

theorem Convex.hasDerivAt_volume_real_sep_inner_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {s : Set E} (hs : Convex ℝ s) (hsb : Bornology.IsBounded s) (hsm : MeasurableSet s) {e : E} (he : ‖e‖ = 1) {c : ℝ} (hc : c ∈ interior ((fun (x : E) => inner ℝ e x) '' s)) : HasDerivAt (fun (c : ℝ) => MeasureTheory.volume.real {x : E | x ∈ s ∧ inner ℝ e x ≤ c}) (MeasureTheory.volume.real {y : ↥(ℝ ∙ e)ᗮ | ↑y + c • e ∈ s}) c

For a bounded Borel convex set, the volume of the part below the hyperplane ⟪e, x⟫ = c is differentiable in c at every height interior to ⟪e, s⟫, and its derivative is the volume of the hyperplane section at height c.

theorem TauCeti.volume_hyperplaneSection_rpow_mul_volume_hyperplaneSection_rpow_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (e : E) {K L : Set E} (hK : MeasurableSet K) (hL : MeasurableSet L) {θ : ℝ} (hθ₀ : 0 < θ) (hθ₁ : θ < 1) (s t : ℝ) : MeasureTheory.volume {y : ↥(ℝ ∙ e)ᗮ | ↑y + s • e ∈ K} ^ (1 - θ) * MeasureTheory.volume {y : ↥(ℝ ∙ e)ᗮ | ↑y + t • e ∈ L} ^ θ ≤ MeasureTheory.volume {y : ↥(ℝ ∙ e)ᗮ | ↑y + ((1 - θ) * s + θ * t) • e ∈ (1 - θ) • K + θ • L}

Multiplicative Brunn–Minkowski for hyperplane sections. The weighted geometric mean of the volumes of a section of K and a section of L is at most the volume of the section of (1 - θ) • K + θ • L at the weighted height.