feat(Analysis/Convex): Radon's convexity theorem (#6598)

Add Radon's theorem on convex sets



Co-authored-by: Vasily Nesterov <118051017+vasnesterov@users.noreply.github.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Author: vasnesterov

Mathlib.lean

@@ -659,6 +659,7 @@ import Mathlib.Analysis.Convex.Measure
 import Mathlib.Analysis.Convex.Normed
 import Mathlib.Analysis.Convex.PartitionOfUnity
 import Mathlib.Analysis.Convex.Quasiconvex
+import Mathlib.Analysis.Convex.Radon
 import Mathlib.Analysis.Convex.Segment
 import Mathlib.Analysis.Convex.Side
 import Mathlib.Analysis.Convex.SimplicialComplex.Basic

Mathlib/Analysis/Convex/Combination.lean

@@ -32,8 +32,9 @@ open BigOperators Classical Pointwise
 
 universe u u'
 
-variable {R E F ι ι' α : Type*} [LinearOrderedField R] [AddCommGroup E] [AddCommGroup F]
-  [LinearOrderedAddCommGroup α] [Module R E] [Module R F] [Module R α] [OrderedSMul R α] {s : Set E}
+variable {R R' E F ι ι' α : Type*} [LinearOrderedField R] [LinearOrderedField R'] [AddCommGroup E]
+  [AddCommGroup F] [LinearOrderedAddCommGroup α] [Module R E] [Module R F] [Module R α]
+  [OrderedSMul R α] {s : Set E}
 
 /-- Center of mass of a finite collection of points with prescribed weights.
 Note that we require neither `0 ≤ w i` nor `∑ w = 1`. -/
@@ -69,6 +70,14 @@ theorem Finset.centerMass_singleton (hw : w i ≠ 0) : ({i} : Finset ι).centerM
   rw [centerMass, sum_singleton, sum_singleton, ← mul_smul, inv_mul_cancel hw, one_smul]
 #align finset.center_mass_singleton Finset.centerMass_singleton
 
+@[simp] lemma Finset.centerMass_neg_left : t.centerMass (-w) z = t.centerMass w z := by
+  simp [centerMass, inv_neg]
+
+lemma Finset.centerMass_smul_left {c : R'} [Module R' R] [Module R' E] [SMulCommClass R' R R]
+  [IsScalarTower R' R R] [SMulCommClass R R' E] [IsScalarTower R' R E] (hc : c ≠ 0) :
+    t.centerMass (c • w) z = t.centerMass w z := by
+  simp [centerMass, -smul_assoc, smul_assoc c, ←smul_sum, smul_inv₀, smul_smul_smul_comm, hc]
+
 theorem Finset.centerMass_eq_of_sum_1 (hw : ∑ i in t, w i = 1) :
     t.centerMass w z = ∑ i in t, w i • z i := by
   simp only [Finset.centerMass, hw, inv_one, one_smul]
@@ -148,6 +157,11 @@ end Finset
 
 variable {z}
 
+lemma Finset.centerMass_of_sum_add_sum_eq_zero {s t : Finset ι}
+    (hw : ∑ i in s, w i + ∑ i in t, w i = 0) (hz : ∑ i in s, w i • z i + ∑ i in t, w i • z i = 0) :
+    s.centerMass w z = t.centerMass w z := by
+  simp [centerMass, eq_neg_of_add_eq_zero_right hw, eq_neg_of_add_eq_zero_left hz, ←neg_inv]
+
 /-- The center of mass of a finite subset of a convex set belongs to the set
 provided that all weights are non-negative, and the total weight is positive. -/
 theorem Convex.centerMass_mem (hs : Convex R s) :
@@ -223,13 +237,25 @@ theorem Finset.centerMass_mem_convexHull (t : Finset ι) {w : ι → R} (hw₀ :
   (convex_convexHull R s).centerMass_mem hw₀ hws fun i hi => subset_convexHull R s <| hz i hi
 #align finset.center_mass_mem_convex_hull Finset.centerMass_mem_convexHull
 
+/-- A version of `Finset.centerMass_mem_convexHull` for when the weights are nonpositive. -/
+lemma Finset.centerMass_mem_convexHull_of_nonpos (t : Finset ι) (hw₀ : ∀ i ∈ t, w i ≤ 0)
+    (hws : ∑ i in t, w i < 0) (hz : ∀ i ∈ t, z i ∈ s) : t.centerMass w z ∈ convexHull R s := by
+  rw [←centerMass_neg_left]
+  exact Finset.centerMass_mem_convexHull _ (λ _i hi ↦ neg_nonneg.2 $ hw₀ _ hi) (by simpa) hz
+
 /-- A refinement of `Finset.centerMass_mem_convexHull` when the indexed family is a `Finset` of
 the space. -/
 theorem Finset.centerMass_id_mem_convexHull (t : Finset E) {w : E → R} (hw₀ : ∀ i ∈ t, 0 ≤ w i)
     (hws : 0 < ∑ i in t, w i) : t.centerMass w id ∈ convexHull R (t : Set E) :=
   t.centerMass_mem_convexHull hw₀ hws fun _ => mem_coe.2
 #align finset.center_mass_id_mem_convex_hull Finset.centerMass_id_mem_convexHull
 
+/-- A version of `Finset.centerMass_mem_convexHull` for when the weights are nonpositive. -/
+lemma Finset.centerMass_id_mem_convexHull_of_nonpos (t : Finset E) {w : E → R}
+  (hw₀ : ∀ i ∈ t, w i ≤ 0) (hws : ∑ i in t, w i < 0) :
+    t.centerMass w id ∈ convexHull R (t : Set E) :=
+  t.centerMass_mem_convexHull_of_nonpos hw₀ hws fun _ ↦ mem_coe.2
+
 theorem affineCombination_eq_centerMass {ι : Type*} {t : Finset ι} {p : ι → E} {w : ι → R}
     (hw₂ : ∑ i in t, w i = 1) : t.affineCombination R p w = centerMass t w p := by
   rw [affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one _ w _ hw₂ (0 : E),

Mathlib/Analysis/Convex/Radon.lean

@@ -0,0 +1,51 @@
+/-
+Copyright (c) 2023 Vasily Nesterov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Vasily Nesterov
+-/
+import Mathlib.Analysis.Convex.Combination
+import Mathlib.Tactic.Linarith
+
+/-!
+# 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.
+
+## Tags
+
+convex hull, radon, affine independence
+-/
+
+open Finset Set
+open BigOperators
+
+variable {ι 𝕜 E : Type*} [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {f : ι → E}
+
+/-- **Radon 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. -/
+theorem radon_partition (h : ¬ AffineIndependent 𝕜 f) :
+    ∃ I, (convexHull 𝕜 (f '' I) ∩ convexHull 𝕜 (f '' Iᶜ)).Nonempty := by
+  rw [affineIndependent_iff] at h
+  push_neg at h
+  obtain ⟨s, w, h_wsum, h_vsum, nonzero_w_index, h1, h2⟩ := h
+  let I : Finset ι := s.filter fun i ↦ 0 ≤ w i
+  let J : Finset ι := s.filter fun i ↦ w i < 0
+  let p : E := centerMass I w f -- point of intersection
+  have hJI : ∑ j in J, w j + ∑ i in I, w i = 0 := by
+    simpa only [h_wsum, not_lt] using sum_filter_add_sum_filter_not s (fun i ↦ w i < 0) w
+  have hI : 0 < ∑ i in I, w i := by
+    rcases exists_pos_of_sum_zero_of_exists_nonzero _ h_wsum ⟨nonzero_w_index, h1, h2⟩
+      with ⟨pos_w_index, h1', h2'⟩
+    exact sum_pos' (λ _i hi ↦ (mem_filter.1 hi).2)
+      ⟨pos_w_index, by simp only [mem_filter, h1', h2'.le, and_self, h2']⟩
+  have hp : centerMass J w f = p := Finset.centerMass_of_sum_add_sum_eq_zero hJI $ by
+    simpa only [←h_vsum, not_lt] using sum_filter_add_sum_filter_not s (fun i ↦ w i < 0) _
+  refine ⟨I, p, ?_, ?_⟩
+  · exact centerMass_mem_convexHull _ (fun _i hi ↦ (mem_filter.mp hi).2) hI
+      (fun _i hi ↦ Set.mem_image_of_mem _ hi)
+  rw [←hp]
+  refine centerMass_mem_convexHull_of_nonpos _ (fun _ hi ↦ (mem_filter.mp hi).2.le) ?_
+    (fun _i hi ↦ Set.mem_image_of_mem _ fun hi' ↦ ?_)
+  · linarith only [hI, hJI]
+  · exact (mem_filter.mp hi').2.not_lt (mem_filter.mp hi).2