radon_partition — Mathlib

English

If a finite family of points in a Euclidean space is affinely dependent, there exists a nontrivial partition of the index set into I and its complement such that the convex hulls of the corresponding subfamilies intersect nontrivially.

Русский

Если множество точек в евклидовом пространстве является аффинно зависимым, существует непустое разбиение индексов на I и его дополнение так, что выпуклые оболочки соответствующих подпопуляций пересекаются не тривиально.

LaTeX

$$$\neg\text{AffineIndependent} 𝕜\ f \rightarrow \exists I, (convexHull 𝕜 (f '' I) \cap convexHull 𝕜 (f '' Iᶜ)).Nonempty$$$

Lean4

/-- **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 radon_partition {f : ι → E} (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 ι := {i ∈ s | 0 ≤ w i}
  let J : Finset ι := {i ∈ s | w i < 0}
  let p : E := centerMass I w f
  have hJI : ∑ j ∈ J, w j + ∑ i ∈ 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 ∈ 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' (fun _i hi ↦ (mem_filter.1 hi).2) ⟨pos_w_index, by simp only [I, mem_filter, h1', h2'.le, and_self, h2']⟩
  have hp : centerMass J w f = p :=
    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 ↦ mem_image_of_mem _ hi)
  rw [← hp]
  refine
    centerMass_mem_convexHull_of_nonpos _ (fun _ hi ↦ (mem_filter.mp hi).2.le) ?_
      (fun _i hi ↦ mem_image_of_mem _ fun hi' ↦ ?_)
  · linarith only [hI, hJI]
  · exact (mem_filter.mp hi').2.not_gt (mem_filter.mp hi).2

Похожие утверждения