Minkowski-Caratheodory theorem | Lean AI formalization leaderboard

Problem statement

Notes: Finite-dimensional compact convex sets are generated by their extreme points, with a finrank + 1 bound.

Source: Classical theorem in convex geometry.

Informal solution: Combine Krein-Milman with Caratheodory to represent each point as a convex combination of at most finrank + 1 extreme points.

theorem declaration uses `sorry`mem_convexHull_finset_extremePoints_of_mem_compact_convex {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
    {s : Set E} {x : E}
    (hscomp : IsCompact s)
    (hsconv : Convex ℝ s)
    (hx : x ∈ s) :
    ∃ t : Finset E,
      (↑t : Set E) ⊆ s.extremePoints ℝ ∧
      t.card ≤ Module.finrank ℝ E + 1 ∧
      x ∈ convexHull ℝ (↑t : Set E) := byE:Type u_1inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace ℝ Einst✝:FiniteDimensional ℝ Es:Set Ex:Ehscomp:IsCompact shsconv:Convex ℝ shx:x ∈ s⊢ ∃ t, ↑t ⊆ extremePoints ℝ s ∧ t.card ≤ Module.finrank ℝ E + 1 ∧ x ∈ (convexHull ℝ) ↑t
  sorryAll goals completed! 🐙