def ConvexGeometry.IsConvexBody {E : Type u_1} [TopologicalSpace E] [AddCommGroup E] [Module ℝ E] (C : Set E) : Prop

theorem ConvexGeometry.IsConvexBody.convex {E : Type u_1} [TopologicalSpace E] [AddCommGroup E] [Module ℝ E] {C : Set E} (h : IsConvexBody C) : Convex ℝ C

theorem ConvexGeometry.IsConvexBody.isCompact {E : Type u_1} [TopologicalSpace E] [AddCommGroup E] [Module ℝ E] {C : Set E} (h : IsConvexBody C) : IsCompact C

theorem ConvexGeometry.IsConvexBody.interior_nonempty {E : Type u_1} [TopologicalSpace E] [AddCommGroup E] [Module ℝ E] {C : Set E} (h : IsConvexBody C) : (interior C).Nonempty

@[reducible, inline]

noncomputable abbrev ConvexGeometry.minkowskiFunctional {E : Type u_1} [AddCommGroup E] [Module ℝ E] (C : Set E) (x : E) : ℝ

def ConvexGeometry.banachMazurAdmissible {E : Type u_1} [AddCommGroup E] [Module ℝ E] (K L : Set E) : Set ℝ

noncomputable def ConvexGeometry.banachMazurDist {E : Type u_1} [AddCommGroup E] [Module ℝ E] (K L : Set E) : ℝ

def ConvexGeometry.IsEllipsoid {n : ℕ} (E : Set (EuclideanSpace ℝ (Fin n))) : Prop

def ConvexGeometry.IsOriginSymmetric {n : ℕ} (K : Set (EuclideanSpace ℝ (Fin n))) : Prop

def ConvexGeometry.unitBall (n : ℕ) : Set (EuclideanSpace ℝ (Fin n))

def ConvexGeometry.IsMaxVolInscribedEllipsoid {n : ℕ} (E K : Set (EuclideanSpace ℝ (Fin n))) : Prop

def ConvexGeometry.JohnConditions (n : ℕ) (K : Set (EuclideanSpace ℝ (Fin n))) : Prop

theorem ConvexGeometry.john_conditions_imply_max_vol (n : ℕ) (K : Set (EuclideanSpace ℝ (Fin n))) (hK_convex : Convex ℝ K) (hK_compact : IsCompact K) (hK_interior : (interior K).Nonempty) (hK_symm : IsOriginSymmetric K) (hJ : JohnConditions n K) : IsMaxVolInscribedEllipsoid (unitBall n) K ∧ ∀ (E : Set (EuclideanSpace ℝ (Fin n))), IsMaxVolInscribedEllipsoid E K → E = unitBall n

theorem ConvexGeometry.max_vol_implies_john_conditions (n : ℕ) (K : Set (EuclideanSpace ℝ (Fin n))) (hK_convex : Convex ℝ K) (hK_compact : IsCompact K) (hK_interior : (interior K).Nonempty) (hK_symm : IsOriginSymmetric K) (hMax : IsMaxVolInscribedEllipsoid (unitBall n) K ∧ ∀ (E : Set (EuclideanSpace ℝ (Fin n))), IsMaxVolInscribedEllipsoid E K → E = unitBall n) : JohnConditions n K

theorem ConvexGeometry.john_ellipsoid_characterization (n : ℕ) (K : Set (EuclideanSpace ℝ (Fin n))) (hK_convex : Convex ℝ K) (hK_compact : IsCompact K) (hK_interior : (interior K).Nonempty) (hK_symm : IsOriginSymmetric K) : (IsMaxVolInscribedEllipsoid (unitBall n) K ∧ ∀ (E : Set (EuclideanSpace ℝ (Fin n))), IsMaxVolInscribedEllipsoid E K → E = unitBall n) ↔ JohnConditions n K

theorem ConvexGeometry.separating_hyperplane {E : Type u_1} [TopologicalSpace E] [AddCommGroup E] [Module ℝ E] [T2Space E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] {K : Set E} {p : E} (hK : IsConvexBody K) (hp : p ∉ K) : ∃ (f : E →L[ℝ] ℝ) (u : ℝ), (∀ a ∈ K, f a < u) ∧ u < f p

theorem ConvexGeometry.john_theorem_containment (n : ℕ) (hn : 0 < n) (K : Set (EuclideanSpace ℝ (Fin n))) (hK_convex : Convex ℝ K) (hK_compact : IsCompact K) (hK_interior : (interior K).Nonempty) (hK_symm : IsOriginSymmetric K) : ∃ (T : EuclideanSpace ℝ (Fin n) ≃ₗ[ℝ] EuclideanSpace ℝ (Fin n)), ⇑T '' Metric.closedBall 0 1 ⊆ K ∧ K ⊆ √↑n • ⇑T '' Metric.closedBall 0 1

theorem ConvexGeometry.banachMazur_distance_ball (n : ℕ) (hn : 0 < n) (K : Set (EuclideanSpace ℝ (Fin n))) (hK_convex : Convex ℝ K) (hK_compact : IsCompact K) (hK_interior : (interior K).Nonempty) (hK_symm : IsOriginSymmetric K) : banachMazurDist K (Metric.closedBall 0 1) ≤ √↑n

def ConvexGeometry.halfspacePolytope {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} (a : ι → E) : Set E

theorem ConvexGeometry.polarBody_halfspacePolytope_eq_convexHull {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} [Fintype ι] (a : ι → E) (hC : Bornology.IsBounded (halfspacePolytope a)) : polarBody (halfspacePolytope a) = (convexHull ℝ) (Set.range a)

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

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

def ConvexGeometry.IsConeAligned {n : ℕ} (C : Set (Fin (n + 1) → ℝ)) : Prop

theorem ConvexGeometry.cone_with_prescribed_volumes (n : ℕ) (hn : 1 ≤ n) (v_total v_pos : ENNReal) (hv_total_pos : v_total ≠ 0) (hv_total_fin : v_total ≠ ⊤) (hv_pos_pos : v_pos ≠ 0) (hv_pos_le : v_pos ≤ v_total) : ∃ (C' : Set (Fin (n + 1) → ℝ)), IsConeAligned C' ∧ MeasureTheory.volume C' = v_total ∧ MeasureTheory.volume (C' ∩ posHalfSpace n) = v_pos ∧ ∃ L' ⊆ posHalfSpace n, ENNReal.ofReal (Real.exp (-1)) ≤ volumeRatio MeasureTheory.volume C' L'

theorem ConvexGeometry.lemma8_cone_construction (n : ℕ) (hn : 1 ≤ n) (K' : Set (Fin (n + 1) → ℝ)) (hK' : 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) → ℝ)), 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'