jensen inequality for countable sums

Stream: Is there code for X?

[Pietro Lavino]

I need to use Jensen's inequality for convex functions over countable sets not finite, does that exist in lean? Is someone working on it?

[Daniel Weber]

There's docs#ConvexOn.map_integral_le, perhaps you can apply this with some measure?