Documentation

Mathlib.Analysis.Convex.Radon

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} [LinearOrderedField 𝕜] [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.

theorem Convex.helly_theorem' {ι : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [DecidableEq ι] [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [FiniteDimensional 𝕜 E] {F : ιSet E} {s : Finset ι} (h_convex : is, Convex 𝕜 (F i)) (h_inter : Is, I.card FiniteDimensional.finrank 𝕜 E + 1(iI, F i).Nonempty) :
(is, 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} [DecidableEq ι] [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [FiniteDimensional 𝕜 E] {F : ιSet E} {s : Finset ι} (h_card : FiniteDimensional.finrank 𝕜 E + 1 s.card) (h_convex : is, Convex 𝕜 (F i)) (h_inter : Is, I.card = FiniteDimensional.finrank 𝕜 E + 1(iI, F i).Nonempty) :
(is, 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} [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [FiniteDimensional 𝕜 E] {F : Finset (Set E)} (h_convex : XF, Convex 𝕜 X) (h_inter : GF, G.card FiniteDimensional.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} [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [FiniteDimensional 𝕜 E] {F : Finset (Set E)} (h_card : FiniteDimensional.finrank 𝕜 E + 1 F.card) (h_convex : XF, Convex 𝕜 X) (h_inter : GF, G.card = FiniteDimensional.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} [DecidableEq ι] [LinearOrderedField 𝕜] [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 FiniteDimensional.finrank 𝕜 E + 1(iI, 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} [DecidableEq ι] [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [FiniteDimensional 𝕜 E] [TopologicalSpace E] [T2Space E] {F : ιSet E} (h_card : (FiniteDimensional.finrank 𝕜 E) + 1 PartENat.card ι) (h_convex : ∀ (i : ι), Convex 𝕜 (F i)) (h_compact : ∀ (i : ι), IsCompact (F i)) (h_inter : ∀ (I : Finset ι), I.card = FiniteDimensional.finrank 𝕜 E + 1(iI, 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} [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [FiniteDimensional 𝕜 E] [TopologicalSpace E] [T2Space E] {F : Set (Set E)} (h_convex : XF, Convex 𝕜 X) (h_compact : XF, IsCompact X) (h_inter : ∀ (G : Finset (Set E)), G FG.card FiniteDimensional.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} [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [FiniteDimensional 𝕜 E] [TopologicalSpace E] [T2Space E] {F : Set (Set E)} (h_card : (FiniteDimensional.finrank 𝕜 E) + 1 F.encard) (h_convex : XF, Convex 𝕜 X) (h_compact : XF, IsCompact X) (h_inter : ∀ (G : Finset (Set E)), G FG.card = FiniteDimensional.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.