feat(analysis/convex): Carathéodory's convexity theorem (#2960)
```
theorem caratheodory (s : set E) :
convex_hull s = ⋃ (t : finset E) (w : ↑t ⊆ s) (b : t.card ≤ findim ℝ E + 1), convex_hull ↑t
```
and more explicitly
```
theorem eq_center_mass_card_dim_succ_of_mem_convex_hull (s : set E) (x : E) (h : x ∈ convex_hull s) :
∃ (t : finset E) (w : ↑t ⊆ s) (b : t.card ≤ findim ℝ E + 1)
(f : E → ℝ), (∀ y ∈ t, 0 ≤ f y) ∧ t.sum f = 1 ∧ t.center_mass f id = x
```
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Co-authored-by: Johan Commelin <johan@commelin.net>
