Muirhead's inequality

Stream: maths

[Tian Chen]

Hi all, I proved Muirhead's inequality as a side project: https://github.com/peakpoint/muirhead

I hope some of y'all find it interesting!

[Yaël Dillies]

Interesting! I have a definition of majorize over at branch#karamata

[Yaël Dillies]

Also I see Birkhoff's theorem in there. Have you tried using docs#is_extreme_point and the Krein-Milman theorem (file#analysis/convex/krein_milman)?

[Scott Morrison]

Will you PR it to mathlib?

[Yaël Dillies]

I would like to see the Minkowski-Carathéodory bit extracted from the proof, which I suspect could take a while.