AM-GM equality case

Stream: Is there code for X?

[Eric Rodriguez]

We have all the AM-GM inequalities, but I wonder if we are in any way close to the _equality_ cases of AM-GM? That is, AM-GM is strict unless the vector is constant (I'm not sure how this interacts with the weighted version, I'm sure it's a similar statement)

[Ruben Van de Velde]

I started looking into that in ml3, but didn't figure out the weighted part either. Not sure how far I got, but there should be a branch somewhere I can find later

[Yaël Dillies]

We just got the equality case of Jensen, so you could do the equality case of the general mean inequality

[Terence Tao]

Nice to see a PFR Mathlib contribution get a use case! docs#StrictConvexOn.map_sum_eq_iff