Commit 2021-09-07 03:50 ceb9da60

feat(analysis/convex/caratheodory): strengthen Caratheodory's lemma to provide affine independence (#8892) The changes here are:

• Use hypothesis ¬ affine_independent ℝ (coe : t → E) instead of finrank ℝ E + 1 < t.card
• Drop no-longer-necessary [finite_dimensional ℝ E] assumption
• Do not use a shrinking argument but start by choosing an appropriate subset of minimum cardinality via min_card_finset_of_mem_convex_hull
• Provide a single alternative form of Carathéodory's lemma eq_pos_convex_span_of_mem_convex_hull
• In the alternate form, define the explicit linear combination using elements parameterised by a new fintype rather than on the entire ambient space E (we thus avoid the issue of junk values outside of the relevant subset)