theorem BrunnMinkowskiInequality.brunn_minkowski_inequality {n : ℕ} (hn : 0 < n) (A B : Set (EuclideanSpace ℝ (Fin n))) (hA : MeasurableSet A) (hB : MeasurableSet B) (hA0 : 0 < MeasureTheory.volume A) (hB0 : 0 < MeasureTheory.volume B) (hAfin : MeasureTheory.volume A ≠ ⊤) (hBfin : MeasureTheory.volume B ≠ ⊤) (hABfin : MeasureTheory.volume (A + B) ≠ ⊤) : (MeasureTheory.volume (A + B)).toReal ^ (1 / ↑n) ≥ (MeasureTheory.volume A).toReal ^ (1 / ↑n) + (MeasureTheory.volume B).toReal ^ (1 / ↑n)

theorem BrunnMinkowskiInequality.brunn_minkowski_equality_condition {n : ℕ} (hn : 0 < n) (A B : Set (EuclideanSpace ℝ (Fin n))) (hA : MeasurableSet A) (hB : MeasurableSet B) (hA0 : 0 < MeasureTheory.volume A) (hB0 : 0 < MeasureTheory.volume B) (hAfin : MeasureTheory.volume A ≠ ⊤) (hBfin : MeasureTheory.volume B ≠ ⊤) (hABfin : MeasureTheory.volume (A + B) ≠ ⊤) : (MeasureTheory.volume (A + B)).toReal ^ (1 / ↑n) = (MeasureTheory.volume A).toReal ^ (1 / ↑n) + (MeasureTheory.volume B).toReal ^ (1 / ↑n) ↔ ∃ (c : ℝ) (_ : c > 0) (v : EuclideanSpace ℝ (Fin n)), MeasureTheory.volume (symmDiff B (c • A + {v})) = 0

theorem BrunnMinkowskiInequality.brunn_minkowski_theorem {n : ℕ} (hn : 0 < n) (A B : Set (EuclideanSpace ℝ (Fin n))) (hA : MeasurableSet A) (hB : MeasurableSet B) (hA0 : 0 < MeasureTheory.volume A) (hB0 : 0 < MeasureTheory.volume B) (hAfin : MeasureTheory.volume A ≠ ⊤) (hBfin : MeasureTheory.volume B ≠ ⊤) (hABfin : MeasureTheory.volume (A + B) ≠ ⊤) : (MeasureTheory.volume (A + B)).toReal ^ (1 / ↑n) ≥ (MeasureTheory.volume A).toReal ^ (1 / ↑n) + (MeasureTheory.volume B).toReal ^ (1 / ↑n) ∧ ((MeasureTheory.volume (A + B)).toReal ^ (1 / ↑n) = (MeasureTheory.volume A).toReal ^ (1 / ↑n) + (MeasureTheory.volume B).toReal ^ (1 / ↑n) ↔ ∃ (c : ℝ) (_ : c > 0) (v : EuclideanSpace ℝ (Fin n)), MeasureTheory.volume (symmDiff B (c • A + {v})) = 0)

def BrunnsTheorem.parallelSlice {n : ℕ} (K : Set (Fin (n + 1) → ℝ)) (t : ℝ) : Set (Fin n → ℝ)

noncomputable def BrunnsTheorem.sliceVolume {n : ℕ} (K : Set (Fin (n + 1) → ℝ)) (t : ℝ) : ENNReal

noncomputable def BrunnsTheorem.brunnFunction (n : ℕ) (K : Set (Fin (n + 1) → ℝ)) (t : ℝ) : ℝ

theorem BrunnsTheorem.brunn_minkowski_superset_scaled {n : ℕ} (hn : 0 < n) (A B S : Set (Fin n → ℝ)) (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) (hsub : a • A + b • B ⊆ S) : (MeasureTheory.volume S).toReal ^ (1 / ↑n) ≥ a * (MeasureTheory.volume A).toReal ^ (1 / ↑n) + b * (MeasureTheory.volume B).toReal ^ (1 / ↑n)

theorem BrunnsTheorem.slice_minkowski_subset {n : ℕ} (K : Set (Fin (n + 1) → ℝ)) (hK : Convex ℝ K) (r t a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) : a • parallelSlice K r + b • parallelSlice K t ⊆ parallelSlice K (a * r + b * t)

theorem BrunnsTheorem.brunn_theorem {n : ℕ} (hn : 0 < n) (K : Set (Fin (n + 1) → ℝ)) (hK : ConvexGeometry.IsConvexBody K) : ConcaveOn ℝ Set.univ (brunnFunction n K)