Example (21)

今回は，２重根号をexpを用いずに，４変数の相加相乗平均の大小関係を証明してみます．

(* amgm4 *)

(* まず，２変数の場合を証明します．*)

g`!a b. &0 <= a /\ &0 <= b ==> (a + b) / &2 >= sqrt(a * b)`;;
e(REPEAT GEN_TAC);;
e(DISCH_THEN(fun t -> MP_TAC (CONJ (MATCH_MP REAL_LE_MUL t) t)));;
e(SQRT_SOSFIELD_TAC[]);;
let amgm2 = top_thm();;

(* 次に非負実数の２重の平方根が４乗根となることを証明します．*)

g`!x. &0 <= x ==> sqrt( sqrt x ) = root 4 x`;;
e(REPEAT STRIP_TAC);;
e(FIRST_ASSUM(ASSUME_TAC o (MATCH_MP SQRT_POS_LE)));;
e(FIRST_X_ASSUM(ASSUME_TAC o (MATCH_MP SQRT_POW_2)));;
e(FIRST_ASSUM(ASSUME_TAC o (MATCH_MP SQRT_POW_2)));;
e(FIRST_ASSUM(ASSUME_TAC o (MATCH_MP SQRT_POS_LE)));;
e(FIRST_ASSUM(ASSUME_TAC o (MATCH_MP SQRT_POS_LE)));;
let lemma = CONV_RULE (REWRITE_CONV [ARITH_RULE`SUC 3 = 4`]) (SPECL[`3`;`x:real`;`sqrt (sqrt x)`]ROOT_POS_UNIQ);;
e(MP_TAC lemma);;
e(EVERY_ASSUM MP_TAC);;
e(CONV_TAC REAL_FIELD);;
let root4 = top_thm();;

(* 以下，本体です．*)

g`!a b c d. &0 <= a /\ &0 <= b /\ &0 <= c /\ &0 <= d ==> (a + b + c + d) / &4 >= root 4 (a * b * c * d)`;;

e(REPEAT STRIP_TAC);;
e(SUBGOAL_THEN `&0 <= a * b /\ &0 <= c * d` ASSUME_TAC THENL [ASM_SIMP_TAC[REAL_LE_MUL]; ALL_TAC]);;

(*
e(REPEAT GEN_TAC);;
e(DISCH_THEN (fun t -> ASSUME_TAC (CONJ t (MESON[t;REAL_LE_MUL]`&0 <= a * b /\ &0 <= c * d`))));;

e(REPEAT STRIP_TAC);;
e(MAP_EVERY MP_TAC[
SPECL[`a:real`;`b:real`]REAL_LE_MUL;
SPECL[`c:real`;`d:real`]REAL_LE_MUL;
] THEN ASM_SIMP_TAC[] THEN REPEAT STRIP_TAC);;
*)

e(MAP_EVERY MP_TAC[
SPECL[`a * b:real`;`c * d:real`]REAL_LE_MUL;
SPECL[`a * b:real`;`c * d:real`]SQRT_MUL;
SPECL[`a * b:real`]SQRT_POS_LE;
SPECL[`c * d:real`]SQRT_POS_LE;
] THEN ASM_SIMP_TAC[REAL_MUL_AC] THEN REPEAT STRIP_TAC);;

e(MAP_EVERY MP_TAC[
SPECL[`a:real`;`b:real`]amgm2;
SPECL[`c:real`;`d:real`]amgm2;
SPECL[`sqrt(a * b)`;`sqrt(c * d)`]amgm2;
] THEN ASM_SIMP_TAC[root4]);;
e(REAL_ARITH_TAC);;

let amgm4 = top_thm();;