Documentation

TauCeti.MeasureTheory.Measure.Lebesgue.BrunnMinkowski.Equality

Equality in Brunn–Minkowski for convex sets: matching height quantiles #

Let K and L be bounded Borel convex sets of positive volume in a finite-dimensional Euclidean space, let 0 < θ < 1, and let e be a unit vector. Write z_K and z_L for the quantile functions of the height ⟪e, x⟫ of a point drawn uniformly from K and from L. This file shows that if the multiplicative Brunn–Minkowski inequality volume K ^ (1 - θ) * volume L ^ θ ≤ volume ((1 - θ) • K + θ • L) is an equality, then z_L - z_K is constant on the levels Ioo 0 1. In other words, along each direction the heights at which K and L cut off equal volume fractions differ by a constant, which may depend on the direction.

This is the analytic core of the Kneser–Süss proof that equality in Brunn–Minkowski forces a homothety. Put z = (1 - θ) z_K + θ z_L. The weighted sum of the hyperplane sections of K at height z_K τ and of L at height z_L τ lies in the section of (1 - θ) • K + θ • L at height z τ, so Brunn–Minkowski in the hyperplane bounds the section of the sum from below. The change of variables ζ = z τ then gives volume ((1 - θ) • K + θ • L) ≥ ∫ τ in Ioo 0 1, z' τ * volume (section at z τ), and by the derivative of the height quantile and weighted AM-GM the integrand is at least volume K ^ (1 - θ) * volume L ^ θ. It is strictly larger wherever volume K / volume (K_{z_K τ}) ≠ volume L / volume (L_{z_L τ}). These two ratios are z_K' and z_L', so under equality they agree on all of Ioo 0 1 by continuity, and z_L - z_K is constant.

The estimate on sections is TauCeti.volume_hyperplaneSection_rpow_mul_volume_hyperplaneSection_rpow_le.

Main results #

References #

theorem Convex.exists_quantile_map_inner_cond_eq_add_of_volume_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {e : E} {K L : Set E} (hK : Convex ℝ K) (hKb : Bornology.IsBounded K) (hKm : MeasurableSet K) (hK0 : MeasureTheory.volume K ≠ 0) (hL : Convex ℝ L) (hLb : Bornology.IsBounded L) (hLm : MeasurableSet L) (hL0 : MeasureTheory.volume L ≠ 0) (he : ‖e‖ = 1) {θ : ℝ} (hθ₀ : 0 < θ) (hθ₁ : θ < 1) (hvol : MeasureTheory.volume ((1 - θ) • K + θ • L) ≤ MeasureTheory.volume K ^ (1 - θ) * MeasureTheory.volume L ^ θ) :

Matching height quantiles under Brunn–Minkowski equality. Let K and L be bounded Borel convex sets of positive volume, 0 < θ < 1, and e a unit vector. If the volume of (1 - θ) • K + θ • L is at most volume K ^ (1 - θ) * volume L ^ θ, that is, if the multiplicative Brunn–Minkowski inequality is an equality, then the quantile functions of the height ⟪e, x⟫ of a point drawn uniformly from L and from K differ by a constant on the levels Ioo 0 1.