[Merged by Bors] - feat(Analysis/Convex): Helly's convexity theorem

[vasnesterov]

• Prove Helly's convexity theorem (including compact and set versions) and fix typos in Analysis.Convex.Radon
• Add alias Set.sInter_mono in the style of Set.sUnion_mono
• Mark encard_coe_eq_coe_finsetCard with simp and norm_cast

---

• depends on: [Merged by Bors] - refactor: Improve lemmas about sets of intermediate size #14062

This PR is a natural continuation of my recent PR #6598, introducing Radon's theorem.

[j-loreaux]

I would just move this to the Analysis.Convex.Radon file, as that file only has the convex_partition declaration anyway, and the imports for the current file are not egregious.

This looks pretty good, but I haven't had an in-depth think about possible ways to improve the proof yet. I'll come back to that later. For now, here are a few comments.

[j-loreaux]

I've left some comments below, but mainly I added them for your own benefit so you can see how I transformed the proof into what I am copying below. If you want, you can just copy this proof and resolve the conversations below after you have read and understand them. If you want me to explain any part of this proof I'm happy to. Note: it was not the case that your proof was bad. I'm only trying to show you alternative techniques that can make things a bit easier for you.

/-- **Helly's theorem on convex sets**: If `F` is a finite family of convex sets in a vector space
of finite dimension `d`, and any `d + 1` sets of `F` intersect, then all sets of `F` intersect. -/
theorem helly_theorem (F : Set (Set E)) {hF_fin : Set.Finite F}
    (h_card : (finrank 𝕜 E) + 1 ≤ ncard F) (h_convex : ∀ X ∈ F, Convex 𝕜 X)
    (h_inter : ∀ G : Set (Set E), (G ⊆ F) → (ncard G = (finrank 𝕜 E) + 1) →
    (⋂₀ G).Nonempty) : (⋂₀ F).Nonempty := by
  obtain ⟨n, hn⟩ : ∃ n : ℕ, ncard F = n := ⟨ncard F, rfl⟩ -- for induction on ncard F
  rw [hn] at h_card
  induction' n, h_card using Nat.le_induction with k h_card hk generalizing F
  exact h_inter F (Eq.subset rfl) hn
  /- construct a family of vectors indexed by `F` such that the vector corresponding to `X : F` is
  an arbitrary element of the intersection `⋂₀ F` which *does not lie in `X`*. -/
  let a : F → E := fun X : F ↦ Set.Nonempty.some (s := ⋂₀ (F \ {(X : Set E)})) <| by
    apply @hk _ (Finite.diff hF_fin {(X : Set E)})
    · exact fun Y hY ↦ h_convex Y (mem_of_mem_diff hY)
    · exact fun G hG_1 hG_2 ↦ h_inter G (Subset.trans hG_1 (diff_subset F {(X : Set E)})) hG_2
    · rw [ncard_diff_singleton_of_mem X.property hF_fin, Nat.sub_eq_of_eq_add hn]
  /- This family of vectors is not affine independent because the number of them exceeds the
  dimension of the space. -/
  have h2 : ¬AffineIndependent 𝕜 a := by
    have : Fintype ↑F := Finite.fintype hF_fin -- for instance inferring
    rw [←finrank_vectorSpan_le_iff_not_affineIndependent 𝕜 a (n := (k - 1))]
    · exact (Submodule.finrank_le (vectorSpan 𝕜 (Set.range a))).trans (Nat.le_pred_of_lt h_card)
    · rw [←Finite.card_toFinset hF_fin, ←ncard_eq_toFinset_card F hF_fin, hn,
        ←Nat.sub_add_comm (Nat.one_le_of_lt h_card)]
      rfl
  /- Use `Convex.radon_partition` to conclude there is a subset `I` of `F` and a point `p : E`
  which lies in the convex hull of either `a '' I` or `a '' Iᶜ`. We claim that `p ∈ ⋂₀ F`.
  (here `Iᶜ` is the complement within `F`, i.e., it is effectively `F \ I`.) -/
  obtain ⟨I, p, h4_I, h4_Ic⟩ := Convex.radon_partition h2
  refine ⟨p, fun X hX ↦ ?_⟩
  lift X to F using hX
  /- It suffices to show that for any set `X` in a subcollection `I` of `F`, that the convex hull
  of `a '' Iᶜ` is contained in `X`. -/
  suffices ∀ I : Set F, X ∈ I → (convexHull 𝕜) (a '' Iᶜ) ⊆ X by
    by_cases (X ∈ I)
    · exact this I h h4_Ic
    · apply this Iᶜ h; rwa [compl_compl]
  /- Given any subcollection `I` of `F` containing `X`, because `X` is convex, we need only show
  that `a Y ∈ X` for each `Y ∈ Iᶜ` -/
  intro I h
  rw [Convex.convexHull_subset_iff (h_convex _ X.prop)]
  rintro - ⟨Y, hY, rfl⟩
  /- Since `Y ∈ Iᶜ` and `X ∈ I`, we conclude that `X ≠ Y`, and hence by the definition of `a`:
  `a Y ∈ ⋂₀ F \ {Y} ⊆ X`  -/
  have : X ≠ Y := fun h' ↦ hY (h' ▸ h)
  exact (sInter_subset_of_mem <| mem_diff_singleton.mpr ⟨X.prop, Subtype.coe_injective.ne this⟩)
    (Set.Nonempty.some_mem _)

[vasnesterov]

Thank you very much! And sorry for such a delay. I learned a lot from your comments. In the end, I decided to keep your proof. I don't think I can improve it :)

I added you to the authors list in the heading. Hope you don't mind.

[j-loreaux]

@vasnesterov can you address the earlier unresolved comments?

[vasnesterov]

I added a comment about the theorem at the beginning, switched to indexed families instead sets and proved the infinite version.

[j-loreaux]

I would like to get this merged sooner rather than later. So if you have any questions let me know. Otherwise ping me (i.e., request my review) when you add the set version back in and I'll do a last review.

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• [Merged by Bors] - refactor: Improve lemmas about sets of intermediate size #14062
  By Dependent Issues (🤖). Happy coding!

[YaelDillies]

A good thing to remember is that s : Finset ι is more general than Fintype ι

[YaelDillies]

... namely

Suggested change

	generalize hn : Fintype.card ι = n
	rw [hn] at h_card
	induction' n, h_card using Nat.le_induction with k h_card hk generalizing ι
	induction' s using Finset.induction

and more simplifications below

[vasnesterov]

Here it is more convenient to use induction on the size of the set rather than its elements.

[YaelDillies]

I merged master because you are now on an old toolchain

[jcommelin]

Thanks 🎉

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style