(* ========================================================================= *)
(* Arithmetic-geometric mean inequality.                                     *)
(* ========================================================================= *)

needs "Library/products.ml";;

prioritize_real();;

(* ------------------------------------------------------------------------- *)
(* Various trivial lemmas.                                                   *)
(* ------------------------------------------------------------------------- *)

let FORALL_2 = 
prove (`!P. (!i. 1 <= i /\ i <= 2 ==> P i) <=> P 1 /\ P 2`,
MESON_TAC[ARITH_RULE `1 <= i /\ i <= 2 <=> i = 1 \/ i = 2`]);;
let NUMSEG_2 = 
prove (`1..2 = {1,2}`,
REWRITE_TAC[EXTENSION; IN_INSERT; NOT_IN_EMPTY; IN_NUMSEG] THEN ARITH_TAC);;
let AGM_2 = 
prove (`!x y. x * y <= ((x + y) / &2) pow 2`,
REWRITE_TAC[REAL_LE_SQUARE; REAL_ARITH `x * y <= ((x + y) / &2) pow 2 <=> &0 <= (x - y) * (x - y)`]);;
let SUM_SPLIT_2 = 
prove (`sum(1..2*n) f = sum(1..n) f + sum(n+1..2*n) f`,
SIMP_TAC[MULT_2; ARITH_RULE `1 <= n + 1`; SUM_ADD_SPLIT]);;
let PRODUCT_SPLIT_2 = 
prove (`product(1..2*n) f = product(1..n) f * product(n+1..2*n) f`,
SIMP_TAC[MULT_2; ARITH_RULE `1 <= n + 1`; PRODUCT_ADD_SPLIT]);;
(* ------------------------------------------------------------------------- *) (* Specialized induction principle. *) (* ------------------------------------------------------------------------- *)
let CAUCHY_INDUCT = 
prove (`!P. P 2 /\ (!n. P n ==> P(2 * n)) /\ (!n. P(n + 1) ==> P n) ==> !n. P n`,
GEN_TAC THEN STRIP_TAC THEN MATCH_MP_TAC num_WF THEN X_GEN_TAC `n:num` THEN DISCH_TAC THEN SUBGOAL_THEN `P(0) /\ P(1)` STRIP_ASSUME_TAC THENL [ASM_MESON_TAC[ARITH_RULE `1 = 0 + 1 /\ 2 = 1 + 1`]; ALL_TAC] THEN ASM_CASES_TAC `EVEN n` THENL [FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [EVEN_EXISTS]) THEN ASM_MESON_TAC[ARITH_RULE `2 * n = 0 \/ n < 2 * n`]; ALL_TAC] THEN FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [NOT_EVEN]) THEN SIMP_TAC[ODD_EXISTS; LEFT_IMP_EXISTS_THM] THEN ASM_MESON_TAC[ARITH_RULE `SUC(2 * m) = 1 \/ m + 1 < SUC(2 * m)`; ARITH_RULE `SUC(2 * m) + 1 = 2 * (m + 1)`]);;
(* ------------------------------------------------------------------------- *) (* The main result. *) (* ------------------------------------------------------------------------- *)
let AGM = 
prove (`!n a. 1 <= n /\ (!i. 1 <= i /\ i <= n ==> &0 <= a(i)) ==> product(1..n) a <= (sum(1..n) a / &n) pow n`,
MATCH_MP_TAC CAUCHY_INDUCT THEN REPEAT CONJ_TAC THENL [REWRITE_TAC[FORALL_2; NUMSEG_2] THEN SIMP_TAC[SUM_CLAUSES; PRODUCT_CLAUSES; FINITE_RULES; IN_INSERT; NOT_IN_EMPTY; ARITH; REAL_MUL_RID; REAL_ADD_RID] THEN REWRITE_TAC[AGM_2]; X_GEN_TAC `n:num` THEN DISCH_TAC THEN X_GEN_TAC `a:num->real` THEN STRIP_TAC THEN REWRITE_TAC[SUM_SPLIT_2; PRODUCT_SPLIT_2] THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `(sum(1..n) a / &n) pow n * (sum(n+1..2*n) a / &n) pow n` THEN CONJ_TAC THENL [MATCH_MP_TAC REAL_LE_MUL2 THEN REPEAT CONJ_TAC THENL [MATCH_MP_TAC PRODUCT_POS_LE THEN REWRITE_TAC[FINITE_NUMSEG; IN_NUMSEG] THEN ASM_MESON_TAC[ARITH_RULE `i <= n ==> i <= 2 * n`]; FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_MESON_TAC[ARITH_RULE `i <= n ==> i <= 2 * n`; ARITH_RULE `1 <= 2 * n ==> 1 <= n`]; MATCH_MP_TAC PRODUCT_POS_LE THEN REWRITE_TAC[FINITE_NUMSEG; IN_NUMSEG] THEN ASM_MESON_TAC[ARITH_RULE `n + 1 <= i ==> 1 <= i`]; ONCE_REWRITE_TAC[ADD_SYM] THEN REWRITE_TAC[MULT_2] THEN REWRITE_TAC[PRODUCT_OFFSET; SUM_OFFSET] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_MESON_TAC[ARITH_RULE `1 <= i /\ i <= n ==> 1 <= i + n /\ i + n <= 2 * n`; ARITH_RULE `1 <= 2 * n ==> 1 <= n`]]; ALL_TAC] THEN REWRITE_TAC[GSYM REAL_POW_MUL; GSYM REAL_POW_POW] THEN MATCH_MP_TAC REAL_POW_LE2 THEN REWRITE_TAC[GSYM REAL_OF_NUM_MUL] THEN SUBST1_TAC(REAL_ARITH `&2 * &n = &n * &2`) THEN REWRITE_TAC[real_div; REAL_INV_MUL] THEN REWRITE_TAC[REAL_ARITH `(x + y) * (a * b) = (x * a + y * a) * b`] THEN REWRITE_TAC[GSYM real_div; AGM_2] THEN MATCH_MP_TAC REAL_LE_MUL THEN CONJ_TAC THEN MATCH_MP_TAC REAL_LE_DIV THEN REWRITE_TAC[REAL_POS] THEN MATCH_MP_TAC SUM_POS_LE THEN REWRITE_TAC[FINITE_NUMSEG; IN_NUMSEG] THEN REPEAT STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN ARITH_TAC; X_GEN_TAC `n:num` THEN DISCH_TAC THEN X_GEN_TAC `a:num->real` THEN STRIP_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC `\i. if i <= n then a(i) else sum(1..n) a / &n`) THEN REWRITE_TAC[ARITH_RULE `1 <= n + 1`] THEN ANTS_TAC THENL [REPEAT STRIP_TAC THEN COND_CASES_TAC THEN ASM_SIMP_TAC[] THEN MATCH_MP_TAC REAL_LE_DIV THEN REWRITE_TAC[REAL_POS] THEN ASM_SIMP_TAC[SUM_POS_LE; FINITE_NUMSEG; IN_NUMSEG]; ALL_TAC] THEN ABBREV_TAC `A = sum(1..n) a / &n` THEN SIMP_TAC[GSYM ADD1; PRODUCT_CLAUSES_NUMSEG; SUM_CLAUSES_NUMSEG] THEN SIMP_TAC[ARITH_RULE `1 <= SUC n /\ ~(SUC n <= n)`] THEN REWRITE_TAC[GSYM REAL_OF_NUM_SUC] THEN EXPAND_TAC "A" THEN SIMP_TAC[REAL_OF_NUM_LE; ASSUME `1 <= n`; REAL_FIELD `&1 <= &n ==> (s + s / &n) / (&n + &1) = s / &n`] THEN ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN ASM_REWRITE_TAC[real_pow] THEN ASM_CASES_TAC `&0 < A` THEN ASM_SIMP_TAC[REAL_LE_LMUL_EQ] THEN SUBGOAL_THEN `A = &0` MP_TAC THENL [ASM_REWRITE_TAC[GSYM REAL_LE_ANTISYM; GSYM REAL_NOT_LT] THEN REWRITE_TAC[REAL_NOT_LT] THEN EXPAND_TAC "A" THEN MATCH_MP_TAC REAL_LE_DIV THEN REWRITE_TAC[REAL_POS] THEN ASM_SIMP_TAC[SUM_POS_LE; FINITE_NUMSEG; IN_NUMSEG]; ALL_TAC] THEN EXPAND_TAC "A" THEN REWRITE_TAC[real_div; REAL_ENTIRE; REAL_INV_EQ_0; REAL_OF_NUM_EQ] THEN ASM_SIMP_TAC[ARITH_RULE `1 <= n ==> ~(n = 0)`] THEN DISCH_TAC THEN DISCH_THEN(K ALL_TAC) THEN MP_TAC(SPECL [`a:num->real`; `1`; `n:num`] SUM_POS_EQ_0_NUMSEG) THEN ASM_SIMP_TAC[] THEN DISCH_THEN(MP_TAC o SPEC `n:num`) THEN ASM_REWRITE_TAC[LE_REFL] THEN DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [LE_EXISTS]) THEN REWRITE_TAC[ARITH_RULE `1 + n = SUC n`] THEN DISCH_THEN(CHOOSE_THEN SUBST_ALL_TAC) THEN ASM_REWRITE_TAC[real_pow; REAL_MUL_LZERO; PRODUCT_CLAUSES_NUMSEG] THEN REWRITE_TAC[ARITH_RULE `1 <= SUC n`; REAL_MUL_RZERO; REAL_LE_REFL]]);;