Example (24.8)

　以上をまとめると次のようになります．

g `!f (z:num->num->real).
     (!x. &0 <= x /\ x <= &1 ==> f contl x)
     ==> (?z. !N. 1 <= N
                  ==> (!n. if n < N
                           then &n / &N <= z N n /\ z N n <= &(n + 1) / &N
                           else z N n = &1) /\
                      integral (&0,&1) (\x. f x * abs (sin (&N * pi * x))) =
                      &2 / pi * sum (0..N - 1) (\n. f (z N n) * &1 / &N))`;;
e(REPEAT STRIP_TAC THEN MP_TAC(UNDISCH(SPEC`f:real->real`thm25)) THEN REPEAT STRIP_TAC);;
e(EXISTS_TAC`\N n:num. if n < N then (z:num->num->real) N n else &1` THEN BETA_TAC);;
e(REPEAT STRIP_TAC);;
e(ASM_MESON_TAC[]);;
e(ASM_SIMP_TAC[GSYM SUM_LMUL; REAL_MUL_AC]);;
e(MATCH_MP_TAC SUM_EQ_NUMSEG THEN BETA_TAC THEN ASM_MESON_TAC[LE_0; ARITH_RULE`1 <= N ==> i <= N - 1 ==> i < N`]);;
let thm28 = top_thm();;

let lemma10 = prove
 (`!x0:real y y0. y tends_num_real y0
    ==> (\n. x0 * y n) tends_num_real x0 * y0`,
  REPEAT STRIP_TAC THEN MP_TAC(SPEC`(\n:num. x0:real)`SEQ_MUL) THEN ASM_SIMP_TAC[SEQ_CONST] THEN BETA_TAC);;


g `!f. (!x. &0 <= x /\ x <= &1 ==> f contl x) /\ rintegrable (&0,&1) f
       ==> (\N. integral (&0,&1) (\x. f x * abs (sin (&N * pi * x))))
           tends_num_real &2 / pi * integral (&0,&1) f`;;
e(REPEAT STRIP_TAC);;
e(MP_TAC(SPEC_ALL thm28) THEN ASM_SIMP_TAC[] THEN REPEAT STRIP_TAC);;
e(MP_TAC(SPEC_ALL thm27) THEN ASM_SIMP_TAC[] THEN ONCE_SIMP_TAC[SEQ_SUC] THEN BETA_TAC THEN REPEAT STRIP_TAC);;
e(ASM_SIMP_TAC[my; lemma10]);;
let thm29 = MESON[top_thm()]
`!f. (!x. &0 <= x /\ x <= &1 ==> f contl x) /\ rintegrable (&0,&1) f
     ==> (\n. integral (&0,&1) (\x. f x * abs (sin (&n * pi * x))))
         tends_num_real &2 / pi * integral (&0,&1) f`;;

　仮定のrintegrable (&0,&1) fを連続性から導くのは別の機会にしたいと思います．