P. 500 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 49901-49905   *Has distinct variable group(s)

Type	Label	Description
Statement
21.51.14  Theorems about algebraic numbers
Theorem	aacllem 49901*	Lemma for other theorems about AA. (Contributed by Brendan Leahy, 3-Jan-2020.) (Revised by Alexander van der Vekens and David A. Wheeler, 25-Apr-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> N e. NN0 )   &    |- ( ( ph /\ n e. ( 1 ... N ) ) -> X e. CC )   &    |- ( ( ph /\ k e. ( 0 ... N ) /\ n e. ( 1 ... N ) ) -> C e. QQ )   &    |- ( ( ph /\ k e. ( 0 ... N ) ) -> ( A ^ k ) = sum_ n e. ( 1 ... N ) ( C x. X ) )   =>    |- ( ph -> A e. AA )
21.52  Mathbox for Kunhao Zheng
21.52.1  Weighted AM-GM inequality
Theorem	amgmwlem 49902	Weighted version of amgmlem 26927. (Contributed by Kunhao Zheng, 19-Jun-2021.)
|- M = (mulGrp ` ℂfld )   &    |- ( ph -> A e. Fin )   &    |- ( ph -> A =/= (/) )   &    |- ( ph -> F : A --> RR+ )   &    |- ( ph -> W : A --> RR+ )   &    |- ( ph -> (ℂfld gsumg W ) = 1 )   =>    |- ( ph -> ( M gsumg ( F oF ^c W ) ) <_ (ℂfld gsumg ( F oF x. W ) ) )
Theorem	amgmlemALT 49903	Alternate proof of amgmlem 26927 using amgmwlem 49902. (Contributed by Kunhao Zheng, 20-Jun-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
|- M = (mulGrp ` ℂfld )   &    |- ( ph -> A e. Fin )   &    |- ( ph -> A =/= (/) )   &    |- ( ph -> F : A --> RR+ )   =>    |- ( ph -> ( ( M gsumg F ) ^c ( 1 / (♯ ` A ) ) ) <_ ( (ℂfld gsumg F ) / (♯ ` A ) ) )
Theorem	amgmw2d 49904	Weighted arithmetic-geometric mean inequality for n = 2 (compare amgm2d 44290). (Contributed by Kunhao Zheng, 20-Jun-2021.)
|- ( ph -> A e. RR+ )   &    |- ( ph -> P e. RR+ )   &    |- ( ph -> B e. RR+ )   &    |- ( ph -> Q e. RR+ )   &    |- ( ph -> ( P + Q ) = 1 )   =>    |- ( ph -> ( ( A ^c P ) x. ( B ^c Q ) ) <_ ( ( A x. P ) + ( B x. Q ) ) )
Theorem	young2d 49905	Young's inequality for n = 2, a direct application of amgmw2d 49904. (Contributed by Kunhao Zheng, 6-Jul-2021.)
|- ( ph -> A e. RR+ )   &    |- ( ph -> P e. RR+ )   &    |- ( ph -> B e. RR+ )   &    |- ( ph -> Q e. RR+ )   &    |- ( ph -> ( ( 1 / P ) + ( 1 / Q ) ) = 1 )   =>    |- ( ph -> ( A x. B ) <_ ( ( ( A ^c P ) / P ) + ( ( B ^c Q ) / Q ) ) )

< Previous  Wrap >