def BrunnMinkowski.minkowskiSum {α : Type u_1} [Add α] (A B : Set α) : Set α

theorem BrunnMinkowski.singleton_add_subset_add {G : Type u_1} [AddCommGroup G] {A B : Set G} {a : G} (ha : a ∈ A) : {a} + B ⊆ A + B

theorem BrunnMinkowski.measure_singleton_add {G : Type u_1} [AddCommGroup G] [MeasurableSpace G] [MeasurableAdd G] (μ : MeasureTheory.Measure G) [μ.IsAddLeftInvariant] (a : G) (B : Set G) : μ ({a} + B) = μ B

theorem BrunnMinkowski.measure_add_ge_right {G : Type u_1} [AddCommGroup G] [MeasurableSpace G] [MeasurableAdd G] (μ : MeasureTheory.Measure G) [μ.IsAddLeftInvariant] {A B : Set G} (hA : A.Nonempty) : μ B ≤ μ (A + B)

theorem BrunnMinkowski.measure_add_ge_left {G : Type u_1} [AddCommGroup G] [MeasurableSpace G] [MeasurableAdd G] (μ : MeasureTheory.Measure G) [μ.IsAddLeftInvariant] {A B : Set G} (hB : B.Nonempty) : μ A ≤ μ (A + B)

theorem BrunnMinkowski.measure_add_ge_max {G : Type u_1} [AddCommGroup G] [MeasurableSpace G] [MeasurableAdd G] (μ : MeasureTheory.Measure G) [μ.IsAddLeftInvariant] {A B : Set G} (hA : A.Nonempty) (hB : B.Nonempty) : max (μ A) (μ B) ≤ μ (A + B)

def BrunnMinkowski.bodyOfRevolution {E : Type u_2} [SeminormedAddCommGroup E] (s : Set ℝ) (f : ℝ → ℝ) : Set (ℝ × E)

theorem BrunnMinkowski.convex_bodyOfRevolution {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {s : Set ℝ} {f : ℝ → ℝ} (hs : Convex ℝ s) (hf : ConcaveOn ℝ s f) : Convex ℝ (bodyOfRevolution s f)

def BrunnMinkowski.slice {E : Type u_2} (K : Set (ℝ × E)) (t : ℝ) : Set E

theorem BrunnMinkowski.slice_volume_concavity_ineq {n : ℕ} (hn : 0 < n) (K : Set (ℝ × (Fin n → ℝ))) (hK : Convex ℝ K) (s : Set ℝ) (hs : s = {t : ℝ | (slice K t).Nonempty}) ⦃t₁ : ℝ⦄ : t₁ ∈ s → ∀ ⦃t₂ : ℝ⦄, t₂ ∈ s → ∀ ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a * (MeasureTheory.volume (slice K t₁)).toReal ^ (1 / ↑n) + b * (MeasureTheory.volume (slice K t₂)).toReal ^ (1 / ↑n) ≤ (MeasureTheory.volume (slice K (a * t₁ + b * t₂))).toReal ^ (1 / ↑n)

theorem BrunnMinkowski.brunns_theorem {n : ℕ} (hn : 0 < n) (K : Set (ℝ × (Fin n → ℝ))) (hK : Convex ℝ K) (s : Set ℝ) (hs : s = {t : ℝ | (slice K t).Nonempty}) : ConcaveOn ℝ s fun (t : ℝ) => (MeasureTheory.volume (slice K t)).toReal ^ (1 / ↑n)

theorem BrunnMinkowski.convex_bodyOfRevolution_of_convex {n : ℕ} (hn : 0 < n) (K : Set (ℝ × (Fin n → ℝ))) (hK : Convex ℝ K) (s : Set ℝ) (hs : s = {t : ℝ | (slice K t).Nonempty}) (f : ℝ → ℝ) (hf : f = fun (t : ℝ) => (MeasureTheory.volume (slice K t)).toReal ^ (1 / ↑n)) : Convex ℝ (bodyOfRevolution s f)

theorem BrunnMinkowski.cone_volume_ratio_le_half (n : ℕ) (hn : 0 < n) : (↑n / (↑n + 1)) ^ n ≤ 1 / 2

theorem BrunnMinkowski.exp_neg_one_le_cone_volume_ratio (n : ℕ) (hn : 0 < n) : Real.exp (-1) ≤ (↑n / (↑n + 1)) ^ n

theorem BrunnMinkowski.cone_centroid_cut_bounds (n : ℕ) (hn : 0 < n) : Real.exp (-1) ≤ (↑n / (↑n + 1)) ^ n ∧ (↑n / (↑n + 1)) ^ n ≤ 1 / 2

theorem BrunnMinkowski.brunn_minkowski_boxes {n : ℕ} (hn : 0 < n) (a b : Fin n → ℝ) (ha : ∀ (i : Fin n), 0 < a i) (hb : ∀ (i : Fin n), 0 < b i) : (∏ i : Fin n, (a i + b i)) ^ (1 / ↑n) ≥ (∏ i : Fin n, a i) ^ (1 / ↑n) + (∏ i : Fin n, b i) ^ (1 / ↑n)

theorem BrunnMinkowski.volume_singleton_add' {m : ℕ} (a : Fin (m + 1) → ℝ) (s : Set (Fin (m + 1) → ℝ)) : MeasureTheory.volume ({a} + s) = MeasureTheory.volume s

theorem BrunnMinkowski.volume_add_singleton' {m : ℕ} (s : Set (Fin (m + 1) → ℝ)) (b : Fin (m + 1) → ℝ) : MeasureTheory.volume (s + {b}) = MeasureTheory.volume s

theorem BrunnMinkowski.volume_hyperplane {m : ℕ} (c : ℝ) : MeasureTheory.volume {x : Fin (m + 1) → ℝ | x 0 = c} = 0

theorem BrunnMinkowski.intersection_subset_hyperplane {m : ℕ} (A B : Set (Fin (m + 1) → ℝ)) (a₀ : Fin (m + 1) → ℝ) (ha₀_max : ∀ a ∈ A, a 0 ≤ a₀ 0) (b₀ : Fin (m + 1) → ℝ) (hb₀_min : ∀ b ∈ B, b₀ 0 ≤ b 0) : (A + {b₀}) ∩ ({a₀} + B) ⊆ {x : Fin (m + 1) → ℝ | x 0 = a₀ 0 + b₀ 0}

theorem BrunnMinkowski.volume_add_le_volume_minkowski_sum {m : ℕ} (A B : Set (Fin (m + 1) → ℝ)) (hA_compact : IsCompact A) (hA_ne : A.Nonempty) (hB_compact : IsCompact B) (hB_ne : B.Nonempty) (hB_meas : MeasurableSet B) : MeasureTheory.volume A + MeasureTheory.volume B ≤ MeasureTheory.volume (A + B)

noncomputable def GrunbaumsTheorem.centroid {n : ℕ} (K : Set (Fin (n + 1) → ℝ)) : Fin (n + 1) → ℝ

def GrunbaumsTheorem.closedHalfspace {n : ℕ} (f : (Fin (n + 1) → ℝ) →ₗ[ℝ] ℝ) (c : ℝ) : Set (Fin (n + 1) → ℝ)

theorem GrunbaumsTheorem.grunbaum_wlog_reduction {n : ℕ} (K : Set (Fin (n + 1) → ℝ)) (hK_convex : Convex ℝ K) (hK_compact : IsCompact K) (hK_interior : (interior K).Nonempty) (hK_meas : MeasurableSet K) (f : (Fin (n + 1) → ℝ) →ₗ[ℝ] ℝ) (c : ℝ) (hcentroid : centroid K ∈ closedHalfspace f c) (hKnotsubH : ¬K ⊆ closedHalfspace f c) : 1 ≤ n ∧ ∃ (K' : Set (Fin (n + 1) → ℝ)), ConvexGeometry.IsConvexBody K' ∧ MeasureTheory.volume K' ≠ 0 ∧ MeasureTheory.volume K' ≠ ⊤ ∧ (∃ x ∈ K', x 0 > 0) ∧ (∃ x ∈ K', x 0 < 0) ∧ 0 ≤ ∫ (x : Fin (n + 1) → ℝ) in K', x 0 ∧ MeasureTheory.volume (K ∩ closedHalfspace f c) / MeasureTheory.volume K = MeasureTheory.volume (K' ∩ {x : Fin (n + 1) → ℝ | 0 ≤ x 0}) / MeasureTheory.volume K'

noncomputable def IsoperimetricInequality.modulusOfConvexity (ε : ℝ) : ℝ

noncomputable def GrunbaumConeReplacement.volumeRatio {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) (K L : Set α) : ENNReal

def GrunbaumConeReplacement.posHalfSpace (n : ℕ) : Set (Fin (n + 1) → ℝ)

theorem GrunbaumConeReplacement.volumeRatio_eq_of_measures_eq {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) {K C L : Set α} (hvol_total : μ K = μ C) (hvol_part : μ (K ∩ L) = μ (C ∩ L)) : volumeRatio μ K L = volumeRatio μ C L

theorem GrunbaumConeReplacement.volumeRatio_mono_right {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) (K : Set α) {L₁ L₂ : Set α} (h : L₁ ⊆ L₂) : volumeRatio μ K L₁ ≤ volumeRatio μ K L₂

theorem GrunbaumConeReplacement.volume_ratio_chain {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) {K C L L' : Set α} {b : ENNReal} (hvol_total : μ K = μ C) (hvol_part : μ (K ∩ L) = μ (C ∩ L)) (hL' : L' ⊆ L) (hbound : b ≤ volumeRatio μ C L') : b ≤ volumeRatio μ K L

theorem GrunbaumConeReplacement.lemma8_cone_construction (n : ℕ) (hn : 1 ≤ n) (K' : Set (Fin (n + 1) → ℝ)) (hK' : ConvexGeometry.IsConvexBody K') (hpos : MeasureTheory.volume K' ≠ 0) (hfin : MeasureTheory.volume K' ≠ ⊤) (hH_pos : ∃ x ∈ K', x 0 > 0) (hH_neg : ∃ x ∈ K', x 0 < 0) (hcentroid : 0 ≤ ∫ (x : Fin (n + 1) → ℝ) in K', x 0) : ∃ (C' : Set (Fin (n + 1) → ℝ)), ConvexGeometry.IsConeAligned C' ∧ MeasureTheory.volume C' = MeasureTheory.volume K' ∧ MeasureTheory.volume (C' ∩ posHalfSpace n) = MeasureTheory.volume (K' ∩ posHalfSpace n) ∧ ∃ L' ⊆ posHalfSpace n, ENNReal.ofReal (Real.exp (-1)) ≤ volumeRatio MeasureTheory.volume C' L'

theorem GrunbaumConeReplacement.lemma8_volume_ratio_bound (n : ℕ) (hn : 1 ≤ n) (K' : Set (Fin (n + 1) → ℝ)) (hK' : ConvexGeometry.IsConvexBody K') (hpos : MeasureTheory.volume K' ≠ 0) (hfin : MeasureTheory.volume K' ≠ ⊤) (hH_pos : ∃ x ∈ K', x 0 > 0) (hH_neg : ∃ x ∈ K', x 0 < 0) (hcentroid : 0 ≤ ∫ (x : Fin (n + 1) → ℝ) in K', x 0) : ENNReal.ofReal (Real.exp (-1)) ≤ volumeRatio MeasureTheory.volume K' (posHalfSpace n)

theorem GrunbaumsTheorem.grunbaum_theorem {n : ℕ} (K : Set (Fin (n + 1) → ℝ)) (hK_convex : Convex ℝ K) (hK_compact : IsCompact K) (hK_interior : (interior K).Nonempty) (hK_meas : MeasurableSet K) (f : (Fin (n + 1) → ℝ) →ₗ[ℝ] ℝ) (c : ℝ) (hcentroid : centroid K ∈ closedHalfspace f c) : Real.exp (-1) * (MeasureTheory.volume K).toReal ≤ (MeasureTheory.volume (K ∩ closedHalfspace f c)).toReal