Equuivalence of convexity definitions.

Stream: Is there code for X?

[Pietro Lavino]

In Lean ConvexOn is defined from pairs of points and coefficients that add up to one, but I would need the definition for any n t terms and corresponding coefficients, i know this could be proved by induction but was wondering if I could save some work.

[Yaël Dillies]

This is called Jensen's theorem

[Yaël Dillies]

docs#ConvexOn.map_sum_le

[Pietro Lavino]

thanks!