Radon's theorem on convex sets

Radon's theorem states that any affine dependent set can be partitioned into two sets whose convex hulls intersect nontrivially.

As a corollary, we prove Helly's theorem, which is a basic result in discrete geometry on the intersection of convex sets. Let X₁, ⋯, Xₙ be a finite family of convex sets in ℝᵈ with n ≥ d + 1. The theorem states that if any d + 1 sets from this family intersect nontrivially, then the whole family intersect nontrivially. For the infinite family of sets it is not true, as example of Set.Ioo 0 (1 / n) for n : ℕ shows. But the statement is true, if we assume compactness of sets (see helly_theorem_compact)

Tags

convex hull, affine independence, Radon, Helly

theorem Convex.radon_partition {ι : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {f : ι → E} (h : ¬AffineIndependent 𝕜 f) : ∃ (I : Set ι), ((convexHull 𝕜) (f '' I) ∩ (convexHull 𝕜) (f '' Iᶜ)).Nonempty

Radon's theorem on convex sets.

Any family f of affine dependent vectors contains a set I with the property that convex hulls of I and Iᶜ intersect nontrivially. In particular, any d + 2 points in a d-dimensional space can be partitioned this way, since they are affinely dependent (see finrank_vectorSpan_le_iff_not_affineIndependent).

theorem Convex.helly_theorem' {ι : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] [FiniteDimensional 𝕜 E] {F : ι → Set E} {s : Finset ι} (h_convex : ∀ i ∈ s, Convex 𝕜 (F i)) (h_inter : ∀ I ⊆ s, I.card ≤ Module.finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty) : (⋂ i ∈ s, F i).Nonempty

Helly's theorem for finite families of convex sets.

If F is a finite family of convex sets in a vector space of finite dimension d, and any k ≤ d + 1 sets of F intersect nontrivially, then all sets of F intersect nontrivially.

theorem Convex.helly_theorem {ι : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] [FiniteDimensional 𝕜 E] {F : ι → Set E} {s : Finset ι} (h_card : Module.finrank 𝕜 E + 1 ≤ s.card) (h_convex : ∀ i ∈ s, Convex 𝕜 (F i)) (h_inter : ∀ I ⊆ s, I.card = Module.finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty) : (⋂ i ∈ s, F i).Nonempty

Helly's theorem for finite families of convex sets in its classical form.

If F is a family of n convex sets in a vector space of finite dimension d, with n ≥ d + 1, and any d + 1 sets of F intersect nontrivially, then all sets of F intersect nontrivially.

theorem Convex.helly_theorem_set' {𝕜 : Type u_2} {E : Type u_3} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] [FiniteDimensional 𝕜 E] {F : Finset (Set E)} (h_convex : ∀ X ∈ F, Convex 𝕜 X) (h_inter : ∀ G ⊆ F, G.card ≤ Module.finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty) : (⋂₀ ↑F).Nonempty

Helly's theorem for finite sets of convex sets.

If F is a finite set of convex sets in a vector space of finite dimension d, and any k ≤ d + 1 sets from F intersect nontrivially, then all sets from F intersect nontrivially.

theorem Convex.helly_theorem_set {𝕜 : Type u_2} {E : Type u_3} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] [FiniteDimensional 𝕜 E] {F : Finset (Set E)} (h_card : Module.finrank 𝕜 E + 1 ≤ F.card) (h_convex : ∀ X ∈ F, Convex 𝕜 X) (h_inter : ∀ G ⊆ F, G.card = Module.finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty) : (⋂₀ ↑F).Nonempty

Helly's theorem for finite sets of convex sets in its classical form.

If F is a finite set of convex sets in a vector space of finite dimension d, with n ≥ d + 1, and any d + 1 sets from F intersect nontrivially, then all sets from F intersect nontrivially.

theorem Convex.helly_theorem_compact' {ι : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] [FiniteDimensional 𝕜 E] [TopologicalSpace E] [T2Space E] {F : ι → Set E} (h_convex : ∀ (i : ι), Convex 𝕜 (F i)) (h_compact : ∀ (i : ι), IsCompact (F i)) (h_inter : ∀ (I : Finset ι), I.card ≤ Module.finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty) : (⋂ (i : ι), F i).Nonempty

Helly's theorem for families of compact convex sets.

If F is a family of compact convex sets in a vector space of finite dimension d, and any k ≤ d + 1 sets of F intersect nontrivially, then all sets of F intersect nontrivially.

theorem Convex.helly_theorem_compact {ι : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] [FiniteDimensional 𝕜 E] [TopologicalSpace E] [T2Space E] {F : ι → Set E} (h_card : ↑(Module.finrank 𝕜 E) + 1 ≤ ENat.card ι) (h_convex : ∀ (i : ι), Convex 𝕜 (F i)) (h_compact : ∀ (i : ι), IsCompact (F i)) (h_inter : ∀ (I : Finset ι), I.card = Module.finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty) : (⋂ (i : ι), F i).Nonempty

Helly's theorem for families of compact convex sets in its classical form.

If F is a (possibly infinite) family of more than d + 1 compact convex sets in a vector space of finite dimension d, and any d + 1 sets of F intersect nontrivially, then all sets of F intersect nontrivially.

theorem Convex.helly_theorem_set_compact' {𝕜 : Type u_2} {E : Type u_3} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] [FiniteDimensional 𝕜 E] [TopologicalSpace E] [T2Space E] {F : Set (Set E)} (h_convex : ∀ X ∈ F, Convex 𝕜 X) (h_compact : ∀ X ∈ F, IsCompact X) (h_inter : ∀ (G : Finset (Set E)), ↑G ⊆ F → G.card ≤ Module.finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty) : (⋂₀ F).Nonempty

Helly's theorem for sets of compact convex sets.

If F is a set of compact convex sets in a vector space of finite dimension d, and any k ≤ d + 1 sets from F intersect nontrivially, then all sets from F intersect nontrivially.

theorem Convex.helly_theorem_set_compact {𝕜 : Type u_2} {E : Type u_3} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] [FiniteDimensional 𝕜 E] [TopologicalSpace E] [T2Space E] {F : Set (Set E)} (h_card : ↑(Module.finrank 𝕜 E) + 1 ≤ F.encard) (h_convex : ∀ X ∈ F, Convex 𝕜 X) (h_compact : ∀ X ∈ F, IsCompact X) (h_inter : ∀ (G : Finset (Set E)), ↑G ⊆ F → G.card = Module.finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty) : (⋂₀ F).Nonempty

Helly's theorem for sets of compact convex sets in its classical version.

If F is a (possibly infinite) set of more than d + 1 compact convex sets in a vector space of finite dimension d, and any d + 1 sets from F intersect nontrivially, then all sets from F intersect nontrivially.