Commit 2023-04-24 14:36 cc8afbdc

View on Github →

feat: port Analysis.Convex.Combination (#3598)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Convex/Combination.lean

added theorem AffineBasis.convexHull_eq_nonneg_coord

added theorem Convex.centerMass_mem

added theorem Convex.finsum_mem

added theorem Convex.sum_mem

added def Finset.centerMass

added theorem Finset.centerMass_empty

added theorem Finset.centerMass_eq_of_sum_1

added theorem Finset.centerMass_filter_ne_zero

added theorem Finset.centerMass_id_mem_convexHull

added theorem Finset.centerMass_insert

added theorem Finset.centerMass_ite_eq

added theorem Finset.centerMass_le_sup

added theorem Finset.centerMass_mem_convexHull

added theorem Finset.centerMass_pair

added theorem Finset.centerMass_segment'

added theorem Finset.centerMass_segment

added theorem Finset.centerMass_singleton

added theorem Finset.centerMass_smul

added theorem Finset.centerMass_subset

added theorem Finset.centroid_eq_centerMass

added theorem Finset.centroid_mem_convexHull

added theorem Finset.convexHull_eq

added theorem Finset.inf_le_centerMass

added theorem Finset.mem_convexHull

added theorem Set.Finite.convexHull_eq

added theorem Set.Finite.convexHull_eq_image

added theorem affineCombination_eq_centerMass

added theorem affineCombination_mem_convexHull

added theorem convexHull_add

added theorem convexHull_basis_eq_stdSimplex

added theorem convexHull_eq

added theorem convexHull_eq_union_convexHull_finite_subsets

added theorem convexHull_prod

added theorem convexHull_range_eq_exists_affineCombination

added theorem convexHull_sub

added theorem convex_iff_sum_mem

added theorem mem_Icc_of_mem_stdSimplex

added theorem mk_mem_convexHull_prod