Moving forward to weighted AM-GM inequality

[Kunhao Zheng]

Hello all,

    I've formalized amgmw2d months ago, a special case for 2 variable weighted AM-GM inequality. I would like to move forward in case of 3 variables or more.

    I thought about going with a more generic way: I will try to formalize a proof weighted version of the amgmlem. The statement I formalize is:

    |- M = ( mulGrp ` CCfld )

    |- ( ph -> A e. Fin )

    |- ( ph -> A =/= (/) )

    |- ( ph -> F : A --> RR+ )

    |- ( ph -> W : A --> RR+ )

    |- ( ph -> ( CCfld gsum W ) = 1 )

    |- ( ph -> ( M gsum ( F oF ^c W ) ) <_ ( CCfld gsum ( F oF x. W ) ) )

The skeleton of this proof will be quite similar to that of amgmlem. Then amgmlem will become a special case of it, where W is just ( A X. { ( 1 / ( # ` A ) ) } ). From this, I believe we can derive the amgmw3d and amgmw4d the same way as what we've done to amgm3d.

 

What do you think of this plan? I'm very willing to hear your comments or suggestions.

[Thierry Arnoux]

Hi Kunhao,

This sounds like a good plan! I believe you could directly plug your W function as the T function of Jensen’s inequality, and follow the same proof scheme.
Good luck!
BR,
_
Thierry