Example (24.5)

　得られた結果をもとの式に適用します．

g `!f n k. 1 <= n /\ 1 <= k /\ k <= n /\ (!x. &(k - 1) / &n <= x /\ x <= &k / &n ==> f contl x)
==> ?z. &(k - 1) / &n <= z /\ z <= &k / &n /\
        integral (&(k - 1) / &n,&k / &n) (\x. f x * abs (sin (&n * pi * x)))
      = f z * integral (&(k - 1) / &n,&k / &n) (\x. abs (sin (&n * pi * x)))`;;
e(REPEAT STRIP_TAC THEN MATCH_MP_TAC thm15 THEN MP_TAC(SPEC_ALL thm18));;
e(ASM_SIMP_TAC[thm05; ABS_POS; CONV_RULE(ONCE_DEPTH_CONV BETA_CONV)(MATCH_MP CONT_ABS thm09)]);;

e(SUBGOAL_TAC""`&1 <= &n`[ASM_SIMP_TAC[REAL_LE]] THEN ASSUME_TAC PI_POS THEN MP_TAC (REAL_SOSFIELD`&1 <= &n /\ &0 < pi ==> &0 < &2 / pi * &1 / &n`) THEN ASM_SIMP_TAC[]);;
let thm19 = top_thm();;

g`!f n k.
    1 <= n /\ 1 <= k /\ k <= n /\
             (!x. &(k - 1) / &n <= x /\ x <= &k / &n ==> f contl x)
             ==> ?z. &(k - 1) / &n <= z /\
                      z <= &k / &n /\
                      integral (&(k - 1) / &n,&k / &n)
                      (\x. f x * abs (sin (&n * pi * x))) =
                      &2 / pi * &1 / &n * f z`;;

e(REPEAT STRIP_TAC THEN MP_TAC(SPEC_ALL thm18) THEN ASM_SIMP_TAC[]);;
e(REPEAT STRIP_TAC THEN MP_TAC(SPEC_ALL thm19) THEN ASM_MESON_TAC[REAL_MUL_AC]);;
let thm20 = top_thm();;


(* thm20 ここまで *)

let lemma08 = prove(
 `!n f. 1 <= n ==> sum (1,n) f = sum (1..n) f`,
 REPEAT STRIP_TAC THEN MP_TAC(SPECL[`f:num->real`;`1`;`n:num`]PSUM_SUM_NUMSEG) THEN ASM_SIMP_TAC[UNDISCH(ARITH_RULE`1 <= n ==> ~(m = 0 /\ n = 0) /\ (1 + n) - 1 = n`)]);;

let thm21 = MESON[thm05; REAL_LE_TRANS; thm20]
    `!f n k. 1 <= n /\ 1 <= k /\ k <= n /\ (!x. &0 <= x /\ x <= &1 ==> f contl x)
             ==> (?z. &(k - 1) / &n <= z /\
                      z <= &k / &n /\
                      integral (&(k - 1) / &n,&k / &n)
                      (\x. f x * abs (sin (&n * pi * x))) =
                      &2 / pi * &1 / &n * f z)`;;

let thm22 = prove(
 `!f n. 1 <= n /\ (!x. &0 <= x /\ x <= &1 ==> f contl x)
 ==> ?z. !k.  1 <= k /\ k <= n 
             ==> &(k - 1) / &n <= z k /\
                      z k <= &k / &n /\
                      integral (&(k - 1) / &n,&k / &n)
                      (\x. f x * abs (sin (&n * pi * x))) =
                      &2 / pi * &1 / &n * f (z k)`,
 REPEAT STRIP_TAC THEN MP_TAC(SPECL[`f:real->real`;`n:num`]thm21) THEN ASM_SIMP_TAC[] THEN MESON_TAC[]);;


g `!f. (!x. &0 <= x /\ x <= &1 ==> f contl x)
    ==> (!n. ?z. 1 <= n
             ==> ( (!k. 1 <= k /\ k <= n
                           ==> &(k - 1) / &n <= z k /\ z k <= &k / &n) /\
                      integral (&0,&1)
                      (\x. f x * abs (sin (&n * pi * x))) =
                      &2 / pi * &1 / &n * sum (1..n) (\k. f (z k))))`;;
e(SIMP_TAC[RIGHT_EXISTS_IMP_THM] THEN REPEAT STRIP_TAC THEN MP_TAC thm11 THEN ASM_SIMP_TAC[lemma08; GSYM SUM_LMUL] THEN DISCH_THEN(MP_TAC o (SPEC`n:num`)) THEN ASM_SIMP_TAC[] THEN REPEAT STRIP_TAC THEN ASM_SIMP_TAC[] THEN MP_TAC(SPECL[`f:real->real`;`n:num`]thm22) THEN ASM_SIMP_TAC[] THEN REPEAT STRIP_TAC);;

e(SUBGOAL_TAC""
`sum (1..n) (\k. integral (&(k - 1) / &n,&k / &n)
(\x. f x * abs (sin (&n * pi * x)))) =
sum (1..n) (\k. &2 / pi * &1 / &n * f (z k))`
[ASM_MESON_TAC[SUM_EQ_NUMSEG;]]);;

e(ASM_MESON_TAC[]);;
let thm23 = top_thm();;

g `!f. (!x. &0 <= x /\ x <= &1 ==> f contl x)
     ==> (?z. !n. 1 <= n
                  ==> (!k. 1 <= k /\ k <= n
                           ==> &(k - 1) / &n <= z n k /\ z n k <= &k / &n) /\
                      integral (&0,&1) (\x. f x * abs (sin (&n * pi * x))) =
                      &2 / pi * &1 / &n * sum (1..n) (\k. f (z n k)))`;;
e(REPEAT STRIP_TAC THEN MP_TAC(SPEC`f:real->real`thm23) THEN ASM_SIMP_TAC[SKOLEM_THM] THEN REPEAT STRIP_TAC THEN ASM_MESON_TAC[]);;
let thm24 = top_thm();;

g`!f. (!x. &0 <= x /\ x <= &1 ==> f contl x)
         ==> (?z. !n. 1 <= n
                      ==> (!k. k < n
                               ==> &k / &n <= z n k /\ z n k <= &(k + 1) / &n) /\
                          integral (&0,&1)
                          (\x. f x * abs (sin (&n * pi * x))) =
                          &2 / pi * &1 / &n * sum (0..n - 1) (\k. f (z n k)))`;;
e(REPEAT STRIP_TAC THEN MP_TAC(SPEC`f:real->real`thm24) THEN ASM_SIMP_TAC[] THEN REPEAT STRIP_TAC);;
e(EXISTS_TAC`(\n. \k:num. (z:num->num->real) n (k+1))`);;
e(GEN_TAC THEN STRIP_TAC THEN FIRST_X_ASSUM(MP_TAC o (SPEC`n:num`)) THEN ASM_SIMP_TAC[] THEN REPEAT STRIP_TAC);;
e(DISJ_CASES_TAC(ARITH_RULE`k = 0 \/ 1 <= k`) );;
e(ASM_SIMP_TAC[ADD] THEN FIRST_X_ASSUM(MP_TAC o (SPEC`1`)) THEN ASM_SIMP_TAC[LE_REFL; SUB_REFL]);;
e(FIRST_X_ASSUM(MP_TAC o (SPEC`k+1`)) THEN ASM_SIMP_TAC[ARITH_RULE`k < n ==> 1 <= k+1 /\ k+1 <= n`; ARITH_RULE`(k + 1) - 1 = k`]);;
e(SIMP_TAC[ARITH_RULE`1 <= k + 1`]);;
e(FIRST_X_ASSUM(MP_TAC o (SPEC`k+1`)) THEN ASM_SIMP_TAC[ARITH_RULE`k < n ==> k+1 <= n`] THEN SIMP_TAC[ARITH_RULE`1 <= k + 1`]);;
e(ASM_SIMP_TAC[SUM_OFFSET_0]);;
let thm25 = top_thm();;