Hello all,
I've formalized amgmw2d <http://us.metamath.org/mpeuni/amgmw2d.html> 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
<http://us.metamath.org/mpeuni/amgmlem.html>. 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
<http://us.metamath.org/mpeuni/amgm3d.html>.
What do you think of this plan? I'm very willing to hear your comments or
suggestions.
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/6f3cf923-19df-4498-87f4-de18f197af54n%40googlegroups.com.
