Brunn–Minkowski in finite-dimensional Euclidean spaces

The Brunn–Minkowski inequality bounds the outer volume of a Minkowski sum from below by the sum of the dimension roots of the input volumes. We work with Lebesgue-measurable sets and do not require their sum to be measurable. Nonemptiness is retained even when an input has zero volume.

The multiplicative formulation bounds the volume of a convex combination by a weighted geometric mean of volumes. The additive formulation bounds its dimension root by a weighted sum of dimension roots, for arbitrary nonnegative coefficients. Real-valued versions assume finite outer volume of the weighted sum. These inequalities support convex isoperimetric estimates and concavity of outer parallel volumes.

If the r-neighbourhood of a set G lies in a set F of finite volume, Brunn–Minkowski bounds the volume of F \ G from below by n |G|^(1 - 1/n) ω_n^(1/n) r, where ω_n = volume (ball 0 1) (TauCeti.finrank_mul_rpow_pow_mul_le_volume_real_sub). This is the shell estimate behind the isoperimetric inequality. The isoperimetric constant n^n ω_n |s|^(n-1) is the n-th power of n ω_n^(1/n) |s|^(1 - 1/n) (TauCeti.finrank_pow_mul_volume_ball_mul_volume_pow_eq_ofReal).

References

• R. J. Gardner, The Brunn–Minkowski inequality, Bull. Amer. Math. Soc. 39 (2002), 355–405, for the deduction from Prékopa–Leindler by indicators and rescaling.

theorem TauCeti.volume_rpow_mul_volume_rpow_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {A B : Set E} (hA : MeasureTheory.NullMeasurableSet A MeasureTheory.volume) (hB : MeasureTheory.NullMeasurableSet B MeasureTheory.volume) {θ : ℝ} (hθ₀ : 0 < θ) (hθ₁ : θ < 1) : MeasureTheory.volume A ^ (1 - θ) * MeasureTheory.volume B ^ θ ≤ MeasureTheory.volume ((1 - θ) • A + θ • B)

The multiplicative Brunn–Minkowski inequality, with outer volume on the right. The weight is strictly between zero and one; input volumes may be zero or infinite.

theorem TauCeti.mul_volume_rpow_add_mul_volume_rpow_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {A B : Set E} (hn : Module.finrank ℝ E ≠ 0) (hAn : A.Nonempty) (hA : MeasureTheory.NullMeasurableSet A MeasureTheory.volume) (hBn : B.Nonempty) (hB : MeasureTheory.NullMeasurableSet B MeasureTheory.volume) {c d : ℝ} (hc : 0 ≤ c) (hd : 0 ≤ d) : ENNReal.ofReal c * MeasureTheory.volume A ^ (↑(Module.finrank ℝ E))⁻¹ + ENNReal.ofReal d * MeasureTheory.volume B ^ (↑(Module.finrank ℝ E))⁻¹ ≤ MeasureTheory.volume (c • A + d • B) ^ (↑(Module.finrank ℝ E))⁻¹

Weighted Brunn–Minkowski inequality with arbitrary nonnegative coefficients. It includes the convex-combination weights 1 - θ, θ for every θ ∈ [0,1]. Zero coefficients and infinite input volumes use extended multiplication 0 * ∞ = 0.

theorem TauCeti.volume_rpow_add_volume_rpow_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {A B : Set E} (hn : Module.finrank ℝ E ≠ 0) (hAn : A.Nonempty) (hA : MeasureTheory.NullMeasurableSet A MeasureTheory.volume) (hBn : B.Nonempty) (hB : MeasureTheory.NullMeasurableSet B MeasureTheory.volume) : MeasureTheory.volume A ^ (↑(Module.finrank ℝ E))⁻¹ + MeasureTheory.volume B ^ (↑(Module.finrank ℝ E))⁻¹ ≤ MeasureTheory.volume (A + B) ^ (↑(Module.finrank ℝ E))⁻¹

Brunn–Minkowski inequality for nonempty Lebesgue-measurable sets in a positive-dimensional real inner product space. The sum has its outer volume and need not be measurable or have finite volume.

theorem TauCeti.mul_volume_real_rpow_add_mul_volume_real_rpow_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {A B : Set E} (hn : Module.finrank ℝ E ≠ 0) (hAn : A.Nonempty) (hA : MeasureTheory.NullMeasurableSet A MeasureTheory.volume) (hBn : B.Nonempty) (hB : MeasureTheory.NullMeasurableSet B MeasureTheory.volume) {c d : ℝ} (hc : 0 ≤ c) (hd : 0 ≤ d) (hfin : MeasureTheory.volume (c • A + d • B) ≠ ⊤) : c * MeasureTheory.volume.real A ^ (↑(Module.finrank ℝ E))⁻¹ + d * MeasureTheory.volume.real B ^ (↑(Module.finrank ℝ E))⁻¹ ≤ MeasureTheory.volume.real (c • A + d • B) ^ (↑(Module.finrank ℝ E))⁻¹

Real-valued weighted Brunn–Minkowski inequality. Only the weighted sum is required to have finite outer volume: an input with zero coefficient may have infinite volume.

theorem TauCeti.volume_real_rpow_add_volume_real_rpow_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {A B : Set E} (hn : Module.finrank ℝ E ≠ 0) (hAn : A.Nonempty) (hA : MeasureTheory.NullMeasurableSet A MeasureTheory.volume) (hBn : B.Nonempty) (hB : MeasureTheory.NullMeasurableSet B MeasureTheory.volume) (hfin : MeasureTheory.volume (A + B) ≠ ⊤) : MeasureTheory.volume.real A ^ (↑(Module.finrank ℝ E))⁻¹ + MeasureTheory.volume.real B ^ (↑(Module.finrank ℝ E))⁻¹ ≤ MeasureTheory.volume.real (A + B) ^ (↑(Module.finrank ℝ E))⁻¹

Real-valued Brunn–Minkowski inequality. The sum's outer volume must be finite; this implies finiteness of both input volumes.

theorem TauCeti.finrank_mul_rpow_pow_mul_le_volume_real_sub {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (hn : Module.finrank ℝ E ≠ 0) {G F : Set E} (hG : MeasureTheory.NullMeasurableSet G MeasureTheory.volume) (hG0 : G.Nonempty) (hF : MeasureTheory.volume F ≠ ⊤) {r : ℝ} (hr : 0 < r) (hsub : G + Metric.ball 0 r ⊆ F) : ↑(Module.finrank ℝ E) * (MeasureTheory.volume.real G ^ (↑(Module.finrank ℝ E))⁻¹) ^ (Module.finrank ℝ E - 1) * (r * MeasureTheory.volume.real (Metric.ball 0 1) ^ (↑(Module.finrank ℝ E))⁻¹) ≤ MeasureTheory.volume.real F - MeasureTheory.volume.real G

Brunn–Minkowski for a shell. If the r-neighbourhood G + ball 0 r of a nonempty null-measurable set G lies in a set F of finite volume, then in dimension n ≥ 1 volume F - volume G ≥ n (volume G ^ (1 / n)) ^ (n - 1) r ω_n ^ (1 / n).

theorem TauCeti.finrank_pow_mul_volume_ball_mul_volume_pow_eq_ofReal {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {s : Set E} (hs : MeasureTheory.volume s ≠ ⊤) (hn : Module.finrank ℝ E ≠ 0) : ↑(Module.finrank ℝ E) ^ Module.finrank ℝ E * MeasureTheory.volume (Metric.ball 0 1) * MeasureTheory.volume s ^ (Module.finrank ℝ E - 1) = ENNReal.ofReal ((↑(Module.finrank ℝ E) * MeasureTheory.volume.real (Metric.ball 0 1) ^ (↑(Module.finrank ℝ E))⁻¹ * MeasureTheory.volume.real s ^ (1 - (↑(Module.finrank ℝ E))⁻¹)) ^ Module.finrank ℝ E)

The isoperimetric bound n^n ω_n |s|^(n-1) for a set s of finite volume is the n-th power of the real quantity n ω_n^(1/n) |s|^(1 - 1/n), read in ℝ≥0∞.