Example (26.1)

　かなり刹那的ですが，とりあえず２変数の場合です．MVT_ALTではなくMVTを参照すれば端点での可微分性は不要なのですが，その分contlを付さねばならず煩雑？なので，この形にしました（transc.mlのMCLAURINの証明にもWe could weaken the hypotheses slightly, but it's not worth itなるコメントが付いています）．

needs "Library/transc.ml";;
needs "Examples/sos.ml";;
let ass = ASM_SIMP_TAC[] THEN STRIP_TAC;;
g `!a b.
       a < b /\
       (!x. a <= x /\ x <= b
            ==> (f diffl f' x) x /\ (f' diffl f'' x) x /\ f'' x <= &0)
       ==> (!s t.
                &0 < s /\ &0 < t /\ s + t = &1
                ==> s * f a + t * f b <= f (s * a + t * b))`;;
e(REPEAT STRIP_TAC);;
e(ABBREV_TAC`p=s*a+t*b`);;
e(MP_TAC(REAL_SOS
  `a<b /\ &0<s /\ &0<t /\ s+t = &1 /\ p=s*a+t*b ==> a < p /\ p < b`) THEN ass);;
e(MP_TAC(REAL_SOS
  `a < p /\ p < b ==> (!x. x<=p ==> x<=b ) /\ (!x. p<=x ==> a<=x )`) THEN ass);;
e(MP_TAC(SPECL[`f:real->real`;`f':real->real`;`a:real`;`p:real`]MVT_ALT) THEN ass);;
e(MP_TAC(SPECL[`f:real->real`;`f':real->real`;`p:real`;`b:real`]MVT_ALT) THEN ass);;
e(ASM_REWRITE_TAC[UNDISCH(REAL_SOS
  `s+t= &1 ==> ( s * f a + t * f b <= f p <=> t * (f b - f p) <= s * (f p - f a) )`)]);;
e(MP_TAC(REAL_SOS
  `a<b /\ &0<s /\ &0<t /\ s+t = &1 /\ p=s*a+t*b 
   ==> t * (b - p) = s * (p - a) /\ &0<=t * (b - p)`) THEN ass);;
e(MATCH_MP_TAC(REAL_SOS
  `a*b=c*d /\ &0<=a*b /\ f x<=f y ==> a *b* f x <= c*d *f y`) THEN  ASM_SIMP_TAC[]);;
e(MP_TAC(REAL_SOS`z < p /\ p < z'==> z<z'`) THEN ass);;
e(MP_TAC(REAL_SOS`a<z /\ z'< b ==> !x. (z<=x /\ x<=z' ==> a<=x /\ x<=b)`) THEN ass);;
e(MP_TAC(SPECL[`f':real->real`;`f'':real->real`;`z:real`;`z':real`]MVT_ALT) THEN ass);;
e(ASM_REWRITE_TAC[REAL_ARITH`f x<=f y<=>f x-f y<= &0`]);;
e(MP_TAC(REAL_FIELD
  `a<z /\ z<z'' /\ z''<z' /\ z'< b ==> (a<=z''/\ z''<=b /\ &0<z'-z)`) THEN ass);;
e(ASM_SIMP_TAC[REAL_SOS`&0<x /\ f y<= &0 ==> x*f y<= &0`]);;
let JENSEN_0 = top_thm();;

　多変数版は，上記と帰納法によるか，リプシッツ形の不等式によるかでしょうが，後者の方が見通しは良さそうです．