Example (24.2)

　次は積分の平均値定理ですが，第２はありますが，簡単な第１が見当たらないので，CONT_ATTAINS_ALLとIVTなどから証明しました．

let thm12 = MESON[thm05; REAL_LE_TRANS]
`(!x. &0 <= x /\ x <= &1 ==> f contl x)
    ==> !n. 1 <= n
             ==> !k. 1 <= k /\ k <= n
                     ==>  !x. &(k - 1) / &n <= x /\ x <= &k / &n ==> f contl x`;;

g`!f a b.
    a <= b /\ (!x. a <= x /\ x <= b ==> f contl x)
    ==> (?L M.
             (!x. a <= x /\ x <= b ==> L <= f x /\ f x <= M) /\
             (?x. a <= x /\ x <= b /\ L = f x) /\
             (?x. a <= x /\ x <= b /\ f x = M))`;;
e(REPEAT STRIP_TAC THEN MP_TAC (SPEC_ALL CONT_ATTAINS_ALL) THEN ASM_SIMP_TAC[] THEN REPEAT STRIP_TAC);;
e(EXISTS_TAC`L:real` THEN EXISTS_TAC`M:real` THEN ASM_SIMP_TAC[] THEN REPEAT STRIP_TAC);;
e(FIRST_X_ASSUM(MP_TAC o (SPEC`L:real`)) THEN FIRST_X_ASSUM(MP_TAC o (SPEC`a:real`)) THEN ASM_MESON_TAC[REAL_LE_REFL; REAL_LE_TRANS]);;
e(FIRST_X_ASSUM(MP_TAC o (SPEC`M:real`)) THEN FIRST_X_ASSUM(MP_TAC o (SPEC`a:real`)) THEN ASM_MESON_TAC[REAL_LE_REFL; REAL_LE_TRANS]);;
let thm13 = top_thm();;

g `!f a b.
    a <= b /\ (!x. a <= x /\ x <= b ==> f contl x)
    ==> (?x1 x2. a <= x1 /\ x1 <= b /\ a <= x2 /\ x2 <= b /\
               (!x. a <= x /\ x <= b ==> f x1 <= f x /\ f x <= f x2))`;;
e(REPEAT STRIP_TAC THEN MP_TAC (SPEC_ALL thm13) THEN ASM_SIMP_TAC[] THEN REPEAT STRIP_TAC THEN FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM) THEN FIRST_X_ASSUM SUBST_ALL_TAC THEN ASM_MESON_TAC[]);;
let thm14 = top_thm();;

g `!f g a b.
    a <= b /\ (!x. a <= x /\ x <= b ==> f contl x)
           /\ (!x. a <= x /\ x <= b ==> g contl x)
           /\ (!x. a <= x /\ x <= b ==> &0 <= g x)
           /\ &0 < integral (a,b) g
    ==> (?z. a <= z /\ z <= b /\
            integral (a,b) (\x. f x * g x) = f z * integral (a,b) g)`;;
e(REPEAT STRIP_TAC THEN MP_TAC (SPEC_ALL thm14) THEN ASM_SIMP_TAC[] THEN REPEAT STRIP_TAC THEN MAP_EVERY ABBREV_TAC [`L = (f:real->real) x1`; `M = (f:real->real) x2`]);;
e(SUBGOAL_TAC""`!x. a <= x /\ x <= b ==> L * g x <= f x * g x /\ f x * g x <= M * g x`[ASM_MESON_TAC[REAL_LE_RMUL]]);;
e(SUBGOAL_THEN`L * integral (a,b) g <= integral (a,b) (\x. f x * g x) /\ integral (a,b) (\x. f x * g x) <= M * integral (a,b) g`ASSUME_TAC);;
e(SUBGOAL_TAC""`integrable (a,b) g`[ASM_MESON_TAC[INTEGRABLE_CONTINUOUS]] THEN ASM_SIMP_TAC[GSYM INTEGRAL_CMUL]);;
e(SUBGOAL_TAC""`!x. a <= x /\ x <= b ==> (\x. L:real * (g:real->real) x) contl x`[ASM_MESON_TAC[CONT_CONST; INST[`(\x:real. L:real)`,`f:real->real`]CONT_MUL;]]);;
e(SUBGOAL_TAC""`!x. a <= x /\ x <= b ==> (\x. M:real * (g:real->real) x) contl x`[ASM_MESON_TAC[CONT_CONST; INST[`(\x:real. M:real)`,`f:real->real`]CONT_MUL;]]);;
e(SUBGOAL_TAC""`integrable (a,b) (\x. L * g x) /\ integrable (a,b) (\x. f x * g x) /\ integrable (a,b) (\x. M * g x)`[ASM_MESON_TAC[CONT_CONST; CONT_MUL; INTEGRABLE_CONTINUOUS]] THEN ASM_SIMP_TAC[INTEGRAL_LE]);;
e(MAP_EVERY MP_TAC[
SPECL[`integral (a,b) g`;`L:real`;`integral (a,b) (\x. f x * g x)`]REAL_LE_RDIV;
SPECL[`integral (a,b) g`;`integral (a,b) (\x. f x * g x)`;`M:real`]REAL_LE_LDIV] THEN ASM_SIMP_TAC[] THEN REPEAT STRIP_TAC );;
e(DISJ_CASES_TAC(REAL_ARITH`x1 <= x2 \/ x2 <=x1`));;
e(MP_TAC(SPECL[`f:real->real`;`x1:real`;`x2:real`;`integral (a,b) (\x. f x * g x) / integral (a,b) g`]IVT) THEN SUBGOAL_TAC""`(!x. x1 <= x /\ x <= x2 ==> f contl x)`[ASM_MESON_TAC[REAL_LE_TRANS]] THEN ASM_SIMP_TAC[REAL_EQ_RDIV_EQ] THEN ASM_MESON_TAC[REAL_LE_TRANS]);;
e(MP_TAC(SPECL[`f:real->real`;`x2:real`;`x1:real`;`integral (a,b) (\x. f x * g x) / integral (a,b) g`]IVT2) THEN SUBGOAL_TAC""`(!x. x2 <= x /\ x <= x1 ==> f contl x)`[ASM_MESON_TAC[REAL_LE_TRANS]] THEN ASM_SIMP_TAC[REAL_EQ_RDIV_EQ] THEN ASM_MESON_TAC[REAL_LE_TRANS]);;
let thm15 = top_thm();;

val thm15 : thm =
  |- !f g a b.
         a <= b /\
         (!x. a <= x /\ x <= b ==> f contl x) /\
         (!x. a <= x /\ x <= b ==> g contl x) /\
         (!x. a <= x /\ x <= b ==> &0 <= g x) /\
         &0 < integral (a,b) g
         ==> (?z. a <= z /\
                  z <= b /\
                  integral (a,b) (\x. f x * g x) = f z * integral (a,b) g)