The Brunn–Minkowski inequality #
This file deduces the Brunn–Minkowski inequality from the Prékopa–Leindler
inequality, both for the standard product measure on ℝⁿ and for the
Euclidean structure EuclideanSpace ℝ (Fin n).
theorem
brunn_minkowski_zero
{d : ℕ}
{A B C : Set (Fin (d + 1) → ℝ)}
(hA_zero : MeasureTheory.volume A = 0)
(hA_nonempty : A.Nonempty)
(hABC : A + B ⊆ C)
:
MeasureTheory.volume A ^ (↑d + 1)⁻¹ + MeasureTheory.volume B ^ (↑d + 1)⁻¹ ≤ MeasureTheory.volume C ^ (↑d + 1)⁻¹
Brunn–Minkowski when A has zero volume.
theorem
prekopa_leindler_indicator
{d : ℕ}
{θ : ℝ}
{A B : Set (Fin (d + 1) → ℝ)}
(hθ0 : 0 < θ)
(hθ1 : θ < 1)
(hA_measurable : MeasurableSet A)
(hB_measurable : MeasurableSet B)
(hAB_measurable : MeasurableSet (A + B))
:
Prékopa–Leindler applied to indicator functions of two measurable sets.
theorem
brunn_minkowski
{d : ℕ}
{A B : Set (Fin (d + 1) → ℝ)}
(hA_nonempty : A.Nonempty)
(hA_measurable : MeasurableSet A)
(hB_nonempty : B.Nonempty)
(hB_measurable : MeasurableSet B)
(hAB_measurable : MeasurableSet (A + B))
:
MeasureTheory.volume A ^ (↑d + 1)⁻¹ + MeasureTheory.volume B ^ (↑d + 1)⁻¹ ≤ MeasureTheory.volume (A + B) ^ (↑d + 1)⁻¹
The Brunn–Minkowski inequality in arbitrary dimension.
theorem
brunn_minkowski_euclideanSpace
{d : ℕ}
{A B : Set (EuclideanSpace ℝ (Fin (d + 1)))}
(hA_nonempty : A.Nonempty)
(hA_measurable : MeasurableSet A)
(hB_nonempty : B.Nonempty)
(hB_measurable : MeasurableSet B)
(hAB_measurable : MeasurableSet (A + B))
:
MeasureTheory.volume A ^ (↑d + 1)⁻¹ + MeasureTheory.volume B ^ (↑d + 1)⁻¹ ≤ MeasureTheory.volume (A + B) ^ (↑d + 1)⁻¹
Brunn–Minkowski for EuclideanSpace ℝ (Fin (d + 1)) (a wrapper around brunn_minkowski).