Colorful Carathéodory theorem

TheoremColorful Carathéodory theorem in finite-dimensional inner product spaces#✓fully proved

Let \(V\) be a finite-dimensional real inner product space of dimension \(n\), and let \(S_0, \dots, S_n\) be finite subsets of \(V\) such that \(0\) lies in the convex hull of each \(S_l\). Then there are points \(t_0 \in S_0, \dots, t_n \in S_n\) such that \(0\) lies in the convex hull of \(\{t_0, \dots, t_n\}\).

theorem colorful_caratheodory_finrank
    {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V]
    {m : ℕ} (hm : Module.finrank ℝ V + 1 = m)
    (S : Fin m → Finset V)
    (h0 : ∀ l, (0 : V) ∈ convexHull ℝ ((S l : Finset V) : Set V)) :
    ∃ t : (l : Fin m) → ↥(S l),
      (0 : V) ∈ convexHull ℝ (Set.range fun l => ((t l : V)))
Sources
  • I. Barany, Discrete Math. 40 (1982), 141-152, DOI 10.1016/0012-365X(82)90115-7.
Used by 2

TheoremColorful Carathéodory theorem for finite sets#✓fully proved

Let \(d \ge 0\) and let \(S_0, \dots, S_d\) be finite subsets of the Euclidean space \(\mathbb{R}^d\) such that the origin lies in the convex hull of each \(S_i\). Then there are points \(c_0 \in S_0, \dots, c_d \in S_d\) such that the origin lies in the convex hull of \(\{c_0, \dots, c_d\}\).

theorem colorful_caratheodory
    {d : ℕ}
    (S : Fin (d + 1) → Set (EuclideanSpace ℝ (Fin d)))
    (hfin : ∀ i, (S i).Finite)
    (hmem : ∀ i, (0 : EuclideanSpace ℝ (Fin d)) ∈ convexHull ℝ (S i)) :
    ∃ (choice : Fin (d + 1) → EuclideanSpace ℝ (Fin d)),
      (∀ i, choice i ∈ S i) ∧
      (0 : EuclideanSpace ℝ (Fin d)) ∈ convexHull ℝ (Set.range choice)
Sources
  • I. Barany, Discrete Math. 40 (1982), 141-152, DOI 10.1016/0012-365X(82)90115-7.
Uses 1 · Used by 1

TheoremColorful Carathéodory theorem#✓fully proved

Let \(d \ge 0\) and let \(S_0, \dots, S_d\) be subsets of the Euclidean space \(\mathbb{R}^d\) such that the origin lies in the convex hull of each \(S_i\). Then there are points \(c_0 \in S_0, \dots, c_d \in S_d\) such that the origin lies in the convex hull of \(\{c_0, \dots, c_d\}\).

theorem exists_colorful_mem_convexHull
    {d : ℕ}
    (S : Fin (d + 1) → Set (EuclideanSpace ℝ (Fin d)))
    (hmem : ∀ i, (0 : EuclideanSpace ℝ (Fin d)) ∈ convexHull ℝ (S i)) :
    ∃ (choice : Fin (d + 1) → EuclideanSpace ℝ (Fin d)),
      (∀ i, choice i ∈ S i) ∧
      (0 : EuclideanSpace ℝ (Fin d)) ∈ convexHull ℝ (Set.range choice)
Sources
  • I. Barany, Discrete Math. 40 (1982), 141-152, DOI 10.1016/0012-365X(82)90115-7.
Uses 1
3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.