One-dimensional Brunn–Minkowski inequality

For two nonempty Lebesgue-measurable subsets of the real line, the outer volume of their Minkowski sum is at least the sum of their volumes. No measurability of the Minkowski sum is required, and the inequality includes zero and infinite volumes. Nonemptiness is essential: adding the empty set to a positive-volume set gives the empty set.

The compact-set and Borel-set arguments are adapted from Weiyi Wang and Jonathan Ho's Mathlib PR #44802, originating in Jonathan Ho's isoperimetric formalization. The proof translates the compact sets so that their extreme points meet at zero; the two translates have null intersection and their union lies in their Minkowski sum. Inner regularity then gives the Borel-set inequality. Measurable subsets with the same volume extend it to Lebesgue-measurable sets. The weighted form uses Mathlib's Measure.addHaar_smul.

This is the one-dimensional set inequality used in the Prékopa–Leindler argument. Adding an open interval shows that the open ρ-neighbourhood of any nonempty set of reals is longer than the set by at least 2 ρ (TauCeti.Real.volume_add_le_volume_thickening).

References

• Terence Tao, [The Brunn–Minkowski inequality for nilpotent groups] (https://terrytao.wordpress.com/2011/09/16/the-brunn-minkowski-inequality-for-nilpotent-groups/), for the one-dimensional set argument and its role in the functional inequality.

theorem TauCeti.Real.volume_add_volume_le_of_isCompact {A B : Set ℝ} (hAn : A.Nonempty) (hAc : IsCompact A) (hBn : B.Nonempty) (hBc : IsCompact B) : MeasureTheory.volume A + MeasureTheory.volume B ≤ MeasureTheory.volume (A + B)

One-dimensional Brunn–Minkowski theorem for compact sets.

theorem TauCeti.Real.volume_add_volume_le {A B : Set ℝ} (hAn : A.Nonempty) (hAm : MeasurableSet A) (hBn : B.Nonempty) (hBm : MeasurableSet B) : MeasureTheory.volume A + MeasureTheory.volume B ≤ MeasureTheory.volume (A + B)

One-dimensional Brunn–Minkowski theorem for Borel sets, with outer volume on the right. The sum need not be Borel, and the input sets may have infinite volume.

theorem TauCeti.Real.volume_add_volume_le_of_nullMeasurableSet {A B : Set ℝ} (hAn : A.Nonempty) (hAm : MeasureTheory.NullMeasurableSet A MeasureTheory.volume) (hBn : B.Nonempty) (hBm : MeasureTheory.NullMeasurableSet B MeasureTheory.volume) : MeasureTheory.volume A + MeasureTheory.volume B ≤ MeasureTheory.volume (A + B)

One-dimensional Brunn–Minkowski theorem for Lebesgue-measurable sets, with outer volume on the right. No finiteness or measurability of the sum is assumed.

theorem TauCeti.Real.mul_volume_add_mul_volume_le {A B : Set ℝ} (hAn : A.Nonempty) (hAm : MeasureTheory.NullMeasurableSet A MeasureTheory.volume) (hBn : B.Nonempty) (hBm : MeasureTheory.NullMeasurableSet B MeasureTheory.volume) {c d : ℝ} (hc : 0 ≤ c) (hd : 0 ≤ d) : ENNReal.ofReal c * MeasureTheory.volume A + ENNReal.ofReal d * MeasureTheory.volume B ≤ MeasureTheory.volume (c • A + d • B)

Weighted one-dimensional Brunn–Minkowski theorem for Lebesgue-measurable sets. The coefficients may vanish; extended multiplication uses 0 * ∞ = 0. Taking c = 1 - θ and d = θ gives the convex-combination form for every θ ∈ [0,1].

theorem TauCeti.Real.volume_real_add_volume_real_le {A B : Set ℝ} (hAn : A.Nonempty) (hAm : MeasureTheory.NullMeasurableSet A MeasureTheory.volume) (hBn : B.Nonempty) (hBm : MeasureTheory.NullMeasurableSet B MeasureTheory.volume) (hfin : MeasureTheory.volume (A + B) ≠ ⊤) : MeasureTheory.volume.real A + MeasureTheory.volume.real B ≤ MeasureTheory.volume.real (A + B)

Real-valued one-dimensional Brunn–Minkowski inequality. Finiteness of the outer volume of the sum implies finiteness of both input volumes.

theorem TauCeti.Real.mul_volume_real_add_mul_volume_real_le {A B : Set ℝ} (hAn : A.Nonempty) (hAm : MeasureTheory.NullMeasurableSet A MeasureTheory.volume) (hBn : B.Nonempty) (hBm : 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 + d * MeasureTheory.volume.real B ≤ MeasureTheory.volume.real (c • A + d • B)

Real-valued weighted one-dimensional Brunn–Minkowski inequality. The outer volume of the weighted sum must be finite; a zero coefficient still permits an infinite input volume.

theorem TauCeti.Real.volume_add_le_volume_thickening {A : Set ℝ} (hA : A.Nonempty) {ρ : ℝ} (hρ : 0 < ρ) : MeasureTheory.volume A + ENNReal.ofReal (2 * ρ) ≤ MeasureTheory.volume (Metric.thickening ρ A)

The open ρ-neighbourhood of a nonempty subset of the real line has volume at least that of the set plus 2 ρ. No measurability of the set is required: the volume on the left is its outer volume.