Example(26.2)

　普通の数学ならTaylorの定理が簡単ですが，HOL Lightで書いてみると予想外に長くなりましたので，MVTを二重に使う方針にしました．

(* f(x)<=f(p)+(x-p)*f'(p) *)
let ass = ASM_SIMP_TAC[] THEN STRIP_TAC;;
g`!a b:real f f' f'':real->real. a<b /\ (!x. a<=x /\ x<=b ==> (f diffl f' x) x /\ (f' diffl f'' x) x /\ f'' x<= &0) ==> a<b /\ (!x p:real. a<=x /\ x<=b /\ a<=p /\ p<=b ==> f(x)<=f(p)+(x-p)*f'(p)) `;;
e(REPEAT STRIP_TAC THEN ASM_SIMP_TAC[]);;
e(DISJ_CASES_TAC(REAL_ARITH`x=p \/ ~(x=p:real)`));;
(* x = p *)
e(ASM_SIMP_TAC[REAL_LE_REFL; REAL_SUB_REFL; REAL_MUL_LZERO; REAL_ADD_RID]);;
e(DISJ_CASES_TAC(UNDISCH(REAL_ARITH`~(x=p:real)==> p<x \/ x<p`)));;
(* p < x *)
e(MP_TAC(REAL_ARITH`a<=p /\ x<=b ==> (!x':real. p <= x' /\ x' <= x ==> a <= x' /\ x' <= b)`) THEN ass THEN MP_TAC(SPECL[`f:real->real`;`f':real->real`;`p:real`;`x:real`]MVT_ALT) THEN ass);;
e(MP_TAC(REAL_ARITH`a<=p /\ z<x /\ x<=b ==> (!x':real. p <= x' /\ x' <= z ==> a <= x' /\ x' <= b)`) THEN ass THEN MP_TAC(SPECL[`f':real->real`;`f'':real->real`;`p:real`;`z:real`]MVT_ALT) THEN ass);;
e(MP_TAC(REAL_RING`(f:real->real) x - f p = (x - p) * (f':real->real) z /\ f' z - f' p = (z - p) * (f'':real->real) z' ==> f x - (f p + (x - p) * f' p) = (x - p) * (z - p) * f'' z'`) THEN ASM_SIMP_TAC[] THEN STRIP_TAC THEN ONCE_ASM_SIMP_TAC[REAL_ARITH`x<=y <=> x-y<= &0`] THEN ASM_SIMP_TAC[]);;
(*e(SUBGOAL_TAC""`a<= z':real /\ z'<=b`[ASM_REAL_ARITH_TAC]);;*)
e(SUBGOAL_TAC""`(f'':real->real) z' <= &0`[ASM_MESON_TAC[REAL_LT_IMP_LE; REAL_LE_TRANS]]);;
e(SUBGOAL_THEN`p:real < x /\ p < z /\ (f'':real->real) z' <= &0`MP_TAC THENL [ASM_SIMP_TAC[]; CONV_TAC REAL_SOS] );;
(* x < p *)
e(MP_TAC(REAL_ARITH`a<=x /\ p<=b ==> (!x':real. x <= x' /\ x' <= p ==> a <= x' /\ x' <= b)`) THEN ass THEN MP_TAC(SPECL[`f:real->real`;`f':real->real`;`x:real`;`p:real`]MVT_ALT) THEN ass);;
e(MP_TAC(REAL_ARITH`a<=x /\ x<z /\ p<=b ==> (!x':real. z <= x' /\ x' <= p ==> a <= x' /\ x' <= b)`) THEN ass THEN MP_TAC(SPECL[`f':real->real`;`f'':real->real`;`z:real`;`p:real`]MVT_ALT) THEN ass);;
e(MP_TAC(REAL_RING`(f:real->real) p - f x = (p - x) * (f':real->real) z /\ f' p - f' z = (p - z) * (f'':real->real) z' ==> f x - (f p + (x - p) * f' p) = (x - p) * (z - p) * f'' z'`) THEN ASM_SIMP_TAC[] THEN STRIP_TAC THEN ONCE_ASM_SIMP_TAC[REAL_ARITH`x<=y <=> x-y<= &0`] THEN ASM_SIMP_TAC[]);;
(*e(SUBGOAL_TAC""`a<= z':real /\ z'<=b`[ASM_REAL_ARITH_TAC]);;*)
e(SUBGOAL_TAC""`(f'':real->real) z' <= &0`[ASM_MESON_TAC[REAL_LT_IMP_LE; REAL_LE_TRANS]]);;
e(SUBGOAL_THEN`x:real < p /\ z < p /\ (f'':real->real) z' <= &0`MP_TAC THENL [ASM_SIMP_TAC[]; CONV_TAC REAL_SOS] );;
let JENSEN_1=top_thm();;

g`sum (0..n) s = &1  /\ (!i:num. i <= n ==> a <= (x:num->real) i /\ x i <= b /\ &0 <= s i) ==> a <= sum(0..n)(\i. s i * x i) /\ sum(0..n)(\i. s i * x i) <= b`;;
e(DISCH_THEN(ASSUME_TAC o GSYM) THEN REPEAT STRIP_TAC);;
e(GEN_REWRITE_TAC(RATOR_CONV o ONCE_DEPTH_CONV)[GSYM REAL_MUL_RID]);;
e(SUBGOAL_THEN`!i:num. i <= n ==> a * (s:num->real) i <= s i * (x:num->real) i`ASSUME_TAC THENL [ASM_MESON_TAC[REAL_LE_LMUL; REAL_MUL_SYM]; ASM_SIMP_TAC[LE_0; SUM_LE_NUMSEG; GSYM SUM_LMUL]]);;
e(GEN_REWRITE_TAC(RAND_CONV o ONCE_DEPTH_CONV)[GSYM REAL_MUL_RID]);;
e(SUBGOAL_THEN`!i:num. i <= n ==> s i * (x:num->real) i <= b * (s:num->real) i`ASSUME_TAC THENL [ASM_MESON_TAC[REAL_LE_LMUL; REAL_MUL_SYM]; ASM_SIMP_TAC[LE_0; SUM_LE_NUMSEG; GSYM SUM_LMUL]]);;
let JENSEN_2 = top_thm();;

g`!a b f f':real->real. a<b /\ (!x p:real. a <= x /\ x <= b /\ a <= p /\ p <= b ==> f(x)<=f(p)+(x-p)*f'(p))==>(!n s:num->real x:num->real. (!i:num. i <= n ==> a <= x i /\ x i <= b /\ &0<=s i) /\ sum(0..n) s = &1 ==> sum(0..n)(\i. s i*f(x i))<=f(sum(0..n)(\i. s i*x i)))`;;
e(REPEAT STRIP_TAC);;
e(ABBREV_TAC `p = sum(0..n)(\i. s i*x i)`);;
e(MP_TAC JENSEN_2 THEN ASM_SIMP_TAC[] THEN REPEAT STRIP_TAC);;
e(MP_TAC((REAL_SOS`!p:real i:num. &0 <= s i /\ f (x i) <= f p + (x i - p) * f' p ==> s i * f (x i) <= s i * f p + (s i * x i - p *s i) * f' p`)) THEN ASM_SIMP_TAC[] THEN STRIP_TAC);;
e(SUBGOAL_TAC""`!i:num. i <= n ==> s i * f (x i) <= s i * f p + (s i * x i - p * s i) * f' p`[ASM_MESON_TAC[]]);;
e(FIRST_X_ASSUM(fun t -> MP_TAC((MATCH_MP (MESON[LE_0; SUM_LE_NUMSEG]`!f g. (!i. i <= n ==> f i<=g i)==> sum(0..n) f<=sum(0..n) g`) t))));;
e(ASM_SIMP_TAC[SUM_ADD_NUMSEG; SUM_RMUL; SUM_SUB_NUMSEG; SUM_LMUL; ] THEN REAL_ARITH_TAC);;
let JENSEN_3 = top_thm();;

let JENSEN_LT = GEN_ALL (IMP_TRANS (SPEC_ALL JENSEN_1) (SPEC_ALL JENSEN_3));;

g `!a b:real f f' f'':real->real.
     a <= b /\
     (!x. a <= x /\ x <= b
          ==> (f diffl f' x) x /\ (f' diffl f'' x) x /\ f'' x <= &0)
     ==> (!n s x.
              (!i. i <= n ==> &0 <= s i) /\
              (!i. i <= n ==> a <= x i /\ x i <= b) /\
              sum (0..n) s = &1
              ==> sum (0..n) (\i. s i * f (x i)) <=
                  f (sum (0..n) (\i. s i * x i)))`;;
e(REPEAT STRIP_TAC);;
e(DISJ_CASES_TAC(UNDISCH(REAL_ARITH`a<=b:real ==> a<b \/ a=b`)));;
e(MP_TAC(SPEC_ALL JENSEN_LT) THEN ASM_SIMP_TAC[]);;
e(FIRST_X_ASSUM SUBST_ALL_TAC);;
e(RULE_ASSUM_TAC(REWRITE_RULE[REAL_LE_ANTISYM]));;
e(SUBGOAL_THEN`sum (0..n) (\i. s i * (f:real->real) b) = sum (0..n) (\i. s i * f (x i))`MP_TAC);;
e(MATCH_MP_TAC SUM_EQ_NUMSEG);;
e(REPEAT STRIP_TAC THEN BETA_TAC THEN ASM_SIMP_TAC[]);;
e(SIMP_TAC[SUM_RMUL] THEN DISCH_THEN(SUBST_ALL_TAC o GSYM) THEN ASM_SIMP_TAC[REAL_MUL_LID]);;
e(SUBGOAL_THEN`sum (0..n) (\i. s i * b) = sum (0..n) (\i. s i * x i)`MP_TAC);;
e(MATCH_MP_TAC SUM_EQ_NUMSEG);;
e(REPEAT STRIP_TAC THEN BETA_TAC THEN ASM_SIMP_TAC[]);;
e(SIMP_TAC[SUM_RMUL] THEN DISCH_THEN(SUBST_ALL_TAC o GSYM) THEN ASM_SIMP_TAC[REAL_MUL_LID; REAL_LE_REFL]);;
let JENSEN_LE = top_thm();;

g `!x:num->real n:num. ?i j. i <= n /\ j <= n /\ (!k. k <= n ==> x i <= x k /\ x k <= x j)`;;
e(GEN_TAC THEN INDUCT_TAC);;
e(EXISTS_TAC `0` THEN EXISTS_TAC `0` THEN SIMP_TAC[LE] THEN REAL_ARITH_TAC);;
e(POP_ASSUM MP_TAC THEN REPEAT STRIP_TAC);;
(* (x:num->real) i <= x (SUC n) /\ x (SUC n) <= x j *)
e(ASM_CASES_TAC `(x:num->real) i <= x (SUC n) /\ x (SUC n) <= x j`);;
e(EXISTS_TAC `i:num` THEN EXISTS_TAC `j:num`);;
e(ASM_SIMP_TAC[ARITH_RULE`i <= n ==> i <= SUC n`]);;
e(REPEAT STRIP_TAC);;
e(DISJ_CASES_TAC(UNDISCH(ARITH_RULE`k <= SUC n ==> k = SUC n \/ k <= n`)) THENL [ASM_SIMP_TAC[]; ASM_SIMP_TAC[]]) ;;
e(DISJ_CASES_TAC(UNDISCH(ARITH_RULE`k <= SUC n ==> k = SUC n \/ k <= n`)) THENL [ASM_SIMP_TAC[]; ASM_SIMP_TAC[]]);;
(* else *)
e(FIRST_X_ASSUM MP_TAC THEN SIMP_TAC[DE_MORGAN_THM; REAL_NOT_LE] THEN REPEAT STRIP_TAC);;

(* x (SUC n) < x i *)
e(EXISTS_TAC `SUC n` THEN EXISTS_TAC `j:num`);;
e(ASM_SIMP_TAC[ARITH_RULE`j <= n ==> j <= SUC n`; LE_REFL]);;
e(REPEAT STRIP_TAC);;

e(DISJ_CASES_TAC(UNDISCH(ARITH_RULE`k <= SUC n ==> k = SUC n \/ k <= n`)));;
e(ASM_SIMP_TAC[REAL_LE_REFL]);;
e(MATCH_MP_TAC REAL_LT_IMP_LE THEN MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC`(x:num->real) i` THEN ASM_SIMP_TAC[]);;

e(DISJ_CASES_TAC(UNDISCH(ARITH_RULE`k <= SUC n ==> k = SUC n \/ k <= n`)));;
e(ASM_SIMP_TAC[]);;
e(MATCH_MP_TAC REAL_LT_IMP_LE THEN MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC`(x:num->real) i` THEN ASM_SIMP_TAC[]);;
e(ASM_SIMP_TAC[]);;

(* x j < x (SUC n) *)
e(EXISTS_TAC `i:num` THEN EXISTS_TAC `SUC n`);;
e(ASM_SIMP_TAC[ARITH_RULE`i <= n ==> i <= SUC n`; LE_REFL]);;
e(REPEAT STRIP_TAC);;

e(DISJ_CASES_TAC(UNDISCH(ARITH_RULE`k <= SUC n ==> k = SUC n \/ k <= n`)));;
e(ASM_SIMP_TAC[]);;
e(MATCH_MP_TAC REAL_LT_IMP_LE THEN MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC`(x:num->real) j` THEN ASM_SIMP_TAC[]);;
e(ASM_SIMP_TAC[]);;

e(DISJ_CASES_TAC(UNDISCH(ARITH_RULE`k <= SUC n ==> k = SUC n \/ k <= n`)));;
e(ASM_SIMP_TAC[REAL_LE_REFL]);;
e(MATCH_MP_TAC REAL_LT_IMP_LE THEN MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC`(x:num->real) j` THEN ASM_SIMP_TAC[]);;
let FINITE_SEQ_MIN_MAX = top_thm();;

g `!m:real f f' f'':real->real.
     (!x. m < x
          ==> (f diffl f' x) x /\ (f' diffl f'' x) x /\ f'' x <= &0)
     ==> (!n s x.
              (!i. i <= n ==> &0 <= s i) /\
              sum (0..n) s = &1 /\
              (!i. i <= n ==> m < x i)
              ==> sum (0..n) (\i. s i * f (x i)) <=
                  f (sum (0..n) (\i. s i * x i)))`;;
e(REPEAT STRIP_TAC);;
e(MP_TAC(SPEC_ALL FINITE_SEQ_MIN_MAX) THEN ASM_SIMP_TAC[] THEN REPEAT STRIP_TAC);;
e(MAP_EVERY ABBREV_TAC [`a = (x:num->real) i`; `b = (x:num->real) j`]);;
e(SUBGOAL_THEN` a <= b /\
 (!x. a <= x /\ x <= b
      ==> (f diffl f' x) x /\ (f' diffl f'' x) x /\ f'' x <= &0)`ASSUME_TAC);;
e(FIRST_X_ASSUM(MP_TAC o SPEC `i:num`) THEN ASM_SIMP_TAC[REAL_LE_REFL] THEN STRIP_TAC THEN ASM_SIMP_TAC[]);;
e(FIRST_X_ASSUM(ASSUME_TAC o SPEC `i:num`) THEN GEN_TAC THEN ASM_MESON_TAC[REAL_ARITH`m < a:real /\ a <= x /\ x <= b ==> m < x`]);;
e(MP_TAC(SPEC_ALL JENSEN_LE) THEN ASM_SIMP_TAC[]);;
let JENSEN_LT_INF_1 = top_thm();;

g `!m f f' f'' n s x.
     (!x. m < x ==> (f diffl f' x) x /\ (f' diffl f'' x) x /\ f'' x <= &0) /\
     (!i. i <= n ==> &0 <= s i) /\
     sum (0..n) s = &1 /\
     (!i. i <= n ==> m < x i)
     ==> sum (0..n) (\i. s i * f (x i)) <= f (sum (0..n) (\i. s i * x i))`;;
e(REPEAT STRIP_TAC);;
e(MP_TAC(SPEC_ALL JENSEN_LT_INF_1) THEN ASM_SIMP_TAC[]);;
let JENSEN_LT_INF = top_thm();;