Library/agm.ml

   1 (* ========================================================================= *)
   2 (* Arithmetic-geometric mean inequality.                                     *)
   3 (* ========================================================================= *)
   4
   5 needs "Library/products.ml";;
   6
   7 prioritize_real();;
   8
   9 (* ------------------------------------------------------------------------- *)
  10 (* Various trivial lemmas.                                                   *)
  11 (* ------------------------------------------------------------------------- *)
  12
  13 let FORALL_2 = prove
  14  (`!P. (!i. 1 <= i /\ i <= 2 ==> P i) <=> P 1 /\ P 2`,
  15   MESON_TAC[ARITH_RULE `1 <= i /\ i <= 2 <=> i = 1 \/ i = 2`]);;
  16
  17 let NUMSEG_2 = prove
  18  (`1..2 = {1,2}`,
  19   REWRITE_TAC[EXTENSION; IN_INSERT; NOT_IN_EMPTY; IN_NUMSEG] THEN ARITH_TAC);;
  20
  21 let AGM_2 = prove
  22  (`!x y. x * y <= ((x + y) / &2) pow 2`,
  23   REWRITE_TAC[REAL_LE_SQUARE; REAL_ARITH
  24    `x * y <= ((x + y) / &2) pow 2 <=> &0 <= (x - y) * (x - y)`]);;
  25
  26 let SUM_SPLIT_2 = prove
  27  (`sum(1..2*n) f = sum(1..n) f + sum(n+1..2*n) f`,
  28   SIMP_TAC[MULT_2; ARITH_RULE `1 <= n + 1`; SUM_ADD_SPLIT]);;
  29
  30 let PRODUCT_SPLIT_2 = prove
  31  (`product(1..2*n) f = product(1..n) f * product(n+1..2*n) f`,
  32   SIMP_TAC[MULT_2; ARITH_RULE `1 <= n + 1`; PRODUCT_ADD_SPLIT]);;
  33
  34 (* ------------------------------------------------------------------------- *)
  35 (* Specialized induction principle.                                          *)
  36 (* ------------------------------------------------------------------------- *)
  37
  38 let CAUCHY_INDUCT = prove
  39  (`!P. P 2 /\ (!n. P n ==> P(2 * n)) /\ (!n. P(n + 1) ==> P n) ==> !n. P n`,
  40   GEN_TAC THEN STRIP_TAC THEN MATCH_MP_TAC num_WF THEN
  41   X_GEN_TAC `n:num` THEN DISCH_TAC THEN
  42   SUBGOAL_THEN `P(0) /\ P(1)` STRIP_ASSUME_TAC THENL
  43    [ASM_MESON_TAC[ARITH_RULE `1 = 0 + 1 /\ 2 = 1 + 1`]; ALL_TAC] THEN
  44   ASM_CASES_TAC `EVEN n` THENL
  45    [FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [EVEN_EXISTS]) THEN
  46     ASM_MESON_TAC[ARITH_RULE `2 * n = 0 \/ n < 2 * n`];
  47     ALL_TAC] THEN
  48   FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [NOT_EVEN]) THEN
  49   SIMP_TAC[ODD_EXISTS; LEFT_IMP_EXISTS_THM] THEN
  50   ASM_MESON_TAC[ARITH_RULE `SUC(2 * m) = 1 \/ m + 1 < SUC(2 * m)`;
  51                 ARITH_RULE `SUC(2 * m) + 1 = 2 * (m + 1)`]);;
  52
  53 (* ------------------------------------------------------------------------- *)
  54 (* The main result.                                                          *)
  55 (* ------------------------------------------------------------------------- *)
  56
  57 let AGM = prove
  58  (`!n a. 1 <= n /\ (!i. 1 <= i /\ i <= n ==> &0 <= a(i))
  59          ==> product(1..n) a <= (sum(1..n) a / &n) pow n`,
  60   MATCH_MP_TAC CAUCHY_INDUCT THEN REPEAT CONJ_TAC THENL
  61    [REWRITE_TAC[FORALL_2; NUMSEG_2] THEN
  62     SIMP_TAC[SUM_CLAUSES; PRODUCT_CLAUSES; FINITE_RULES; IN_INSERT;
  63              NOT_IN_EMPTY; ARITH; REAL_MUL_RID; REAL_ADD_RID] THEN
  64     REWRITE_TAC[AGM_2];
  65     X_GEN_TAC `n:num` THEN DISCH_TAC THEN X_GEN_TAC `a:num->real` THEN
  66     STRIP_TAC THEN REWRITE_TAC[SUM_SPLIT_2; PRODUCT_SPLIT_2] THEN
  67     MATCH_MP_TAC REAL_LE_TRANS THEN
  68     EXISTS_TAC `(sum(1..n) a / &n) pow n * (sum(n+1..2*n) a / &n) pow n` THEN
  69     CONJ_TAC THENL
  70      [MATCH_MP_TAC REAL_LE_MUL2 THEN REPEAT CONJ_TAC THENL
  71        [MATCH_MP_TAC PRODUCT_POS_LE THEN
  72         REWRITE_TAC[FINITE_NUMSEG; IN_NUMSEG] THEN
  73         ASM_MESON_TAC[ARITH_RULE `i <= n ==> i <= 2 * n`];
  74         FIRST_X_ASSUM MATCH_MP_TAC THEN
  75         ASM_MESON_TAC[ARITH_RULE `i <= n ==> i <= 2 * n`;
  76                       ARITH_RULE `1 <= 2 * n ==> 1 <= n`];
  77         MATCH_MP_TAC PRODUCT_POS_LE THEN
  78         REWRITE_TAC[FINITE_NUMSEG; IN_NUMSEG] THEN
  79         ASM_MESON_TAC[ARITH_RULE `n + 1 <= i ==> 1 <= i`];
  80         ONCE_REWRITE_TAC[ADD_SYM] THEN REWRITE_TAC[MULT_2] THEN
  81         REWRITE_TAC[PRODUCT_OFFSET; SUM_OFFSET] THEN
  82         FIRST_X_ASSUM MATCH_MP_TAC THEN
  83         ASM_MESON_TAC[ARITH_RULE
  84           `1 <= i /\ i <= n ==> 1 <= i + n /\ i + n <= 2 * n`;
  85                       ARITH_RULE `1 <= 2 * n ==> 1 <= n`]];
  86       ALL_TAC] THEN
  87     REWRITE_TAC[GSYM REAL_POW_MUL; GSYM REAL_POW_POW] THEN
  88     MATCH_MP_TAC REAL_POW_LE2 THEN REWRITE_TAC[GSYM REAL_OF_NUM_MUL] THEN
  89     SUBST1_TAC(REAL_ARITH `&2 * &n = &n * &2`) THEN
  90     REWRITE_TAC[real_div; REAL_INV_MUL] THEN
  91     REWRITE_TAC[REAL_ARITH `(x + y) * (a * b) = (x * a + y * a) * b`] THEN
  92     REWRITE_TAC[GSYM real_div; AGM_2] THEN
  93     MATCH_MP_TAC REAL_LE_MUL THEN CONJ_TAC THEN MATCH_MP_TAC REAL_LE_DIV THEN
  94     REWRITE_TAC[REAL_POS] THEN MATCH_MP_TAC SUM_POS_LE THEN
  95     REWRITE_TAC[FINITE_NUMSEG; IN_NUMSEG] THEN REPEAT STRIP_TAC THEN
  96     FIRST_X_ASSUM MATCH_MP_TAC THEN
  97     POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN ARITH_TAC;
  98     X_GEN_TAC `n:num` THEN DISCH_TAC THEN X_GEN_TAC `a:num->real` THEN
  99     STRIP_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC
 100      `\i. if i <= n then a(i) else sum(1..n) a / &n`) THEN
 101     REWRITE_TAC[ARITH_RULE `1 <= n + 1`] THEN ANTS_TAC THENL
 102      [REPEAT STRIP_TAC THEN COND_CASES_TAC THEN ASM_SIMP_TAC[] THEN
 103       MATCH_MP_TAC REAL_LE_DIV THEN REWRITE_TAC[REAL_POS] THEN
 104       ASM_SIMP_TAC[SUM_POS_LE; FINITE_NUMSEG; IN_NUMSEG];
 105       ALL_TAC] THEN
 106     ABBREV_TAC `A = sum(1..n) a / &n` THEN
 107     SIMP_TAC[GSYM ADD1; PRODUCT_CLAUSES_NUMSEG; SUM_CLAUSES_NUMSEG] THEN
 108     SIMP_TAC[ARITH_RULE `1 <= SUC n /\ ~(SUC n <= n)`] THEN
 109     REWRITE_TAC[GSYM REAL_OF_NUM_SUC] THEN EXPAND_TAC "A" THEN
 110     SIMP_TAC[REAL_OF_NUM_LE; ASSUME `1 <= n`; REAL_FIELD
 111      `&1 <= &n ==> (s + s / &n) / (&n + &1) = s / &n`] THEN
 112     ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN ASM_REWRITE_TAC[real_pow] THEN
 113     ASM_CASES_TAC `&0 < A` THEN ASM_SIMP_TAC[REAL_LE_LMUL_EQ] THEN
 114     SUBGOAL_THEN `A = &0` MP_TAC THENL
 115      [ASM_REWRITE_TAC[GSYM REAL_LE_ANTISYM; GSYM REAL_NOT_LT] THEN
 116       REWRITE_TAC[REAL_NOT_LT] THEN EXPAND_TAC "A" THEN
 117       MATCH_MP_TAC REAL_LE_DIV THEN REWRITE_TAC[REAL_POS] THEN
 118       ASM_SIMP_TAC[SUM_POS_LE; FINITE_NUMSEG; IN_NUMSEG];
 119       ALL_TAC] THEN
 120     EXPAND_TAC "A" THEN
 121     REWRITE_TAC[real_div; REAL_ENTIRE; REAL_INV_EQ_0; REAL_OF_NUM_EQ] THEN
 122     ASM_SIMP_TAC[ARITH_RULE `1 <= n ==> ~(n = 0)`] THEN DISCH_TAC THEN
 123     DISCH_THEN(K ALL_TAC) THEN
 124     MP_TAC(SPECL [`a:num->real`; `1`; `n:num`] SUM_POS_EQ_0_NUMSEG) THEN
 125     ASM_SIMP_TAC[] THEN DISCH_THEN(MP_TAC o SPEC `n:num`) THEN
 126     ASM_REWRITE_TAC[LE_REFL] THEN DISCH_TAC THEN
 127     FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [LE_EXISTS]) THEN
 128     REWRITE_TAC[ARITH_RULE `1 + n = SUC n`] THEN
 129     DISCH_THEN(CHOOSE_THEN SUBST_ALL_TAC) THEN
 130     ASM_REWRITE_TAC[real_pow; REAL_MUL_LZERO; PRODUCT_CLAUSES_NUMSEG] THEN
 131     REWRITE_TAC[ARITH_RULE `1 <= SUC n`; REAL_MUL_RZERO; REAL_LE_REFL]]);;