Example(26.3)

　先のJENSEN_LT_INFを用いて，変数の相加平均と相乗平均の不等式を証明します．

let lemma0 = prove
 (`!n s x. (!i. i <= n ==> &0 <= s i) /\ sum (0..n) s = &1 /\
           (!i. i <= n ==> &0 < x i)
    ==> sum (0..n) (\i. s i * ln (x i)) <= ln (sum (0..n) (\i. s i * x i))`,
  REPEAT STRIP_TAC THEN
  MATCH_MP_TAC JENSEN_LT_INF THEN
  EXISTS_TAC `&0` THEN EXISTS_TAC `\x. inv x * &1` THEN 
  EXISTS_TAC `\x. --(&1 / x pow 2) * &1 + &0 * inv x` THEN
  ASM_SIMP_TAC[] THEN REPEAT STRIP_TAC THENL
   [ASM_SIMP_TAC[DIFF_CONV`ln`];
    ASM_SIMP_TAC[REAL_POS_NZ; DIFF_CONV`\x. inv x * &1`];
    ASM_SIMP_TAC[GSYM REAL_INV_1OVER; REAL_MUL_RID; REAL_MUL_LZERO; REAL_ADD_RID; 
                 REAL_LE_POW_2; REAL_LE_INV; REAL_NEG_LE0]]);;

let lemma1 = prove
 (`!n x. (!i. i <= n ==> &0 < x i)
     ==> &0 < (sum (0..n) x) / &(SUC n)`,
  REPEAT STRIP_TAC THEN
  SIMP_TAC[NOT_SUC; REAL_LT_FRACTION_0] THEN
  SUBST1_TAC(MESON[SUM_EQ_0_NUMSEG]`&0 = sum (0..n) (\k. &0)`) THEN
  MATCH_MP_TAC SUM_LT_ALL THEN
  ASM_SIMP_TAC[FINITE_NUMSEG; NUMSEG_EMPTY; LT; IN_NUMSEG_0]);;

let lemma2 = prove
 (`!n x. (!i. i <= n ==> &0 < x i)
     ==> &0 < product (0..n) x`,
  REPEAT STRIP_TAC THEN
  ASM_MESON_TAC[LE_0; PRODUCT_POS_LT_NUMSEG]);;

let lemma3 = prove
 (`!n x. (!i. i <= n ==> &0 < x i)
     ==> ln (product (0..n) x) = sum (0..n) (\i. ln (x i))`,
  SIMP_TAC[SWAP_FORALL_THM] THEN GEN_TAC THEN
  INDUCT_TAC THENL
   [SIMP_TAC[PRODUCT_SING_NUMSEG; SUM_SING_NUMSEG];
    DISCH_THEN(ASSUME_TAC o (MATCH_MP (MESON[LESS_EQ_SUC_REFL; LE_TRANS; LE_REFL]
     `(!i. i <= SUC n ==> &0 < x i) ==> (!i. i <= n ==> &0 < x i) /\ &0 < x (SUC n)`))) THEN
    ASM_SIMP_TAC[LE_0; PRODUCT_CLAUSES_NUMSEG; SUM_CLAUSES_NUMSEG; LN_MUL; lemma2]]);;

let amgm = prove
 (`!n x.
       (!i. i <= n ==> &0 < x i)
       ==> root (SUC n) (product (0..n) x) <= sum (0..n) x / &(SUC n)`,
  REPEAT STRIP_TAC THEN
  MAP_EVERY (ASSUME_TAC o UNDISCH o SPEC_ALL) [lemma1; lemma2] THEN
  ONCE_ASM_REWRITE_TAC[UNDISCH(SPEC `(sum (0..n) x) / &(SUC n)` (GSYM EXP_LN))] THEN
  ASM_SIMP_TAC[ROOT_LN; REAL_EXP_MONO_LE; lemma3; real_div; GSYM SUM_RMUL] THEN
  ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
  MATCH_MP_TAC lemma0 THEN 
  ASM_SIMP_TAC[REAL_POS; REAL_LE_INV; SUM_CONST_NUMSEG; SUB; GSYM ADD1;
               REAL_INJ; NOT_SUC; REAL_MUL_RINV]);;