(* ========================================================================= *)
(* L_p spaces, square integrable functions and basics of Fourier series.     *)
(* ========================================================================= *)
needs "Multivariate/realanalysis.ml";;
(* ------------------------------------------------------------------------- *)
(* Somewhat general lemmas, but perhaps not enough to be installed.          *)
(* ------------------------------------------------------------------------- *)
let REAL_MAX_RPOW = prove
 (`!x y z. &0 <= x /\ &0 <= y /\ &0 <= z
           ==> max (x rpow z) (y rpow z) = (max x y) rpow z`,
  MATCH_MP_TAC 
REAL_WLOG_LE THEN CONJ_TAC THENL
   [MESON_TAC[REAL_ARITH `max x y:real = max y x`]; ALL_TAC] THEN
  SIMP_TAC[
RPOW_LE2; REAL_ARITH `max x y:real = if x <= y then y else x`]);;
 
let REAL_MIN_RPOW = prove
 (`!x y z. &0 <= x /\ &0 <= y /\ &0 <= z
           ==> min (x rpow z) (y rpow z) = (min x y) rpow z`,
  MATCH_MP_TAC 
REAL_WLOG_LE THEN CONJ_TAC THENL
   [MESON_TAC[REAL_ARITH `min x y:real = min y x`]; ALL_TAC] THEN
  SIMP_TAC[
RPOW_LE2; REAL_ARITH `min x y:real = if x <= y then x else y`]);;
 
let LIM_RPOW_NULL = prove
 (`!net p x:A->real.
        ((lift o x) --> vec 0) net /\ &0 < p
        ==> ((\i. lift(x(i) rpow p)) --> vec 0) net`,
 
let LSPACE_NEG = prove
 (`!s p f:real^M->real^N. f 
IN lspace s p ==> (\x. --(f x)) 
IN lspace s p`,
  REWRITE_TAC[VECTOR_ARITH `--x:real^N = --(&1) % x`; 
LSPACE_CMUL]);;
 
let LSPACE_ADD = prove
 (`!s p f g:real^M->real^N.
      &0 <= p /\ f 
IN lspace s p /\ g 
IN lspace s p
      ==> (\x. f(x) + g(x)) 
IN lspace s p`,
 
let LSPACE_SUB = prove
 (`!s p f g:real^M->real^N.
      &0 <= p /\ f 
IN lspace s p /\ g 
IN lspace s p
      ==> (\x. f(x) - g(x)) 
IN lspace s p`,
 
let LSPACE_VSUM = prove
 (`!s p f:A->real^M->real^N t.
        &0 < p /\ 
FINITE t /\ (!i. i 
IN t ==> (f i) 
IN lspace s p)
        ==> (\x. vsum t (\i. f i x)) 
IN lspace s p`,
 
let LSPACE_MAX = prove
 (`!s p k f:real^M->real^N g:real^M->real^N.
      f 
IN lspace s p /\ g 
IN lspace s p /\ &0 < p
      ==> ((\x. lambda i. max (f x$i) (g x$i)):real^M->real^N) 
IN lspace s p`,
 
let LSPACE_MIN = prove
 (`!s p k f:real^M->real^N g:real^M->real^N.
      f 
IN lspace s p /\ g 
IN lspace s p /\ &0 < p
      ==> ((\x. lambda i. min (f x$i) (g x$i)):real^M->real^N) 
IN lspace s p`,
 
let LSPACE_MONO = prove
 (`!f:real^M->real^N s p q.
        f 
IN lspace s q /\ measurable s /\ &0 < p /\ p <= q
        ==> f 
IN lspace s p`,
 
let LSPACE_INCLUSION = prove
 (`!s p q. measurable s /\ &0 < p /\ p <= q
           ==> (lspace s q :(real^M->real^N)->bool) 
SUBSET (lspace s p)`,
  REWRITE_TAC[
SUBSET] THEN REPEAT STRIP_TAC THEN
  MATCH_MP_TAC 
LSPACE_MONO THEN EXISTS_TAC `q:real` THEN
  ASM_REWRITE_TAC[]);;
 
let LNORM_NEG = prove
 (`!s p f:real^M->real^N. lnorm s p (\x. --(f x)) = lnorm s p f`,
 
let LNORM_MUL = prove
 (`!s p f c. f 
IN lspace s p /\ ~(p = &0)
             ==> lnorm s p (\x. c % f x) = abs(c) * lnorm s p f`,
 
let LNORM_EQ_0 = prove
 (`!s p f. ~(p = &0) /\ f 
IN lspace s p
           ==> (lnorm s p f = &0 <=>
                negligible {x | x 
IN s /\ ~(f x = vec 0)})`,
 
let LNORM_RPOW = prove
 (`!s p f:real^M->real^N.
        f 
IN lspace s p /\ ~(p = &0)
        ==> (lnorm s p f) rpow p =
            drop(integral s (\x. lift(norm(f x) rpow p)))`,
 
let INTEGRAL_LNORM_RPOW = prove
 (`!s p f:real^M->real^N.
        f 
IN lspace s p /\ ~(p = &0)
        ==> integral s (\x. lift(norm(f x) rpow p)) =
            lift((lnorm s p f) rpow p)`,
 
let HOELDER_INEQUALITY = prove
 (`!s p q f:real^M->real^N g:real^M->real^N.
        &0 < p /\ &0 < q /\ inv(p) + inv(q) = &1 /\
        f 
IN lspace s p /\ g 
IN lspace s q
        ==> drop(integral s (\x. lift(norm(f x) * norm(g x))))
              <= lnorm s p f * lnorm s q g`,
 
let HOELDER_INEQUALITY_FULL = prove
 (`!s p q f:real^M->real^N g:real^M->real^N.
        &0 < p /\ &0 < q /\ inv(p) + inv(q) = &1 /\
        f 
IN lspace s p /\ g 
IN lspace s q
        ==> (\x. lift(norm(f x) * norm(g x))) 
integrable_on s /\
            drop(integral s (\x. lift(norm(f x) * norm(g x))))
              <= lnorm s p f * lnorm s q g`,
 
let LNORM_TRIANGLE = prove
 (`!s p f:real^M->real^N g:real^M->real^N.
        f 
IN lspace s p /\ g 
IN lspace s p /\ &1 <= p
        ==> lnorm s p (\x. f x + g x) <= lnorm s p f + lnorm s p g`,
 
let VSUM_LNORM = prove
 (`!s p f:A->real^M->real^N t.
        &1 <= p /\ 
FINITE t /\ (!i. i 
IN t ==> (f i) 
IN lspace s p)
        ==> lnorm s p (\x. vsum t (\i. f i x)) <= sum t (\i. lnorm s p (f i))`,
  REWRITE_TAC[
IMP_CONJ; 
RIGHT_FORALL_IMP_THM] THEN
  REPEAT GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN
  MATCH_MP_TAC 
FINITE_INDUCT_STRONG THEN
  ASM_SIMP_TAC[
SUM_CLAUSES; 
VSUM_CLAUSES; 
LNORM_0; 
REAL_LE_REFL;
               REAL_ARITH `&1 <= p ==> ~(p = &0)`] THEN
  MAP_EVERY X_GEN_TAC [`i:A`; `u:A->bool`] THEN
  REWRITE_TAC[
IN_INSERT] THEN
  DISCH_THEN(fun th -> DISCH_TAC THEN MP_TAC th) THEN
  ASM_SIMP_TAC[] THEN DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
  MATCH_MP_TAC(REAL_ARITH `a <= x + y ==> y <= z ==> a <= x + z`) THEN
  W(MP_TAC o PART_MATCH (lhand o rand) 
LNORM_TRIANGLE o lhand o snd) THEN
  ASM_SIMP_TAC[ETA_AX; 
LSPACE_VSUM; REAL_ARITH `&1 <= p ==> &0 < p`]);;
 
let LSPACE_SUMMABLE_UNIV = prove
 (`!f:num->real^M->real^N p s.
        &1 <= p /\
        (!i. f i 
IN lspace s p) /\
        
real_summable (:num) (\i. lnorm s p (f i))
        ==> ?g. g 
IN lspace s p /\
                !e. &0 < e  ==> eventually
                                  (\n. lnorm s p (\x. vsum (0..n) (\i. f i x) -
                                                      g(x)) < e)
                                  sequentially`,
 
let LSPACE_SUMMABLE = prove
 (`!f:num->real^M->real^N p s t.
        &1 <= p /\
        (!i. i 
IN t ==> f i 
IN lspace s p) /\
        
real_summable t (\i. lnorm s p (f i))
        ==> ?g. g 
IN lspace s p /\
                ((\n. lnorm s p (\x. vsum (t 
INTER (0..n)) (\i. f i x) - g x))
                 ---> &0) sequentially`,
  REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[GSYM 
REAL_SUMMABLE_RESTRICT] THEN
  REWRITE_TAC[] THEN STRIP_TAC THEN
  MP_TAC(ISPECL
    [`(\n:num x. if n 
IN t then f n x else vec 0):num->real^M->real^N`;
     `p:real`; `s:real^M->bool`] 
LSPACE_SUMMABLE_UNIV) THEN
  ASM_REWRITE_TAC[] THEN ANTS_TAC THENL
   [CONJ_TAC THENL
     [X_GEN_TAC `i:num` THEN ASM_CASES_TAC `(i:num) 
IN t` THEN
      ASM_SIMP_TAC[
LSPACE_0; ETA_AX; REAL_ARITH `&1 <= p ==> ~(p = &0)`];
      FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [
real_summable]) THEN
      REWRITE_TAC[
real_summable] THEN MATCH_MP_TAC 
MONO_EXISTS THEN
      GEN_TAC THEN MATCH_MP_TAC EQ_IMP THEN
      AP_THM_TAC THEN AP_THM_TAC THEN AP_TERM_TAC THEN
      REWRITE_TAC[
FUN_EQ_THM] THEN GEN_TAC THEN COND_CASES_TAC THEN
      ASM_SIMP_TAC[ETA_AX; 
LNORM_0; REAL_ARITH `&1 <= p ==> ~(p = &0)`]];
    MATCH_MP_TAC 
MONO_EXISTS THEN X_GEN_TAC `g:real^M->real^N` THEN
    ASM_CASES_TAC `(g:real^M->real^N) 
IN lspace s p` THEN
    ASM_REWRITE_TAC[
tendsto_real] THEN
    MATCH_MP_TAC 
MONO_FORALL THEN GEN_TAC THEN
    MATCH_MP_TAC MONO_IMP THEN REWRITE_TAC[] THEN
    MATCH_MP_TAC(REWRITE_RULE[
IMP_CONJ] 
EVENTUALLY_MONO) THEN
    X_GEN_TAC `n:num` THEN REWRITE_TAC[
REAL_SUB_RZERO] THEN
    MATCH_MP_TAC(REAL_ARITH `&0 <= x /\ x = y ==> x < e ==> abs y < e`) THEN
    CONJ_TAC THENL
     [MATCH_MP_TAC 
LNORM_POS_LE THEN MATCH_MP_TAC 
LSPACE_SUB THEN
      ASM_SIMP_TAC[REAL_ARITH `&1 <= p ==> &0 <= p`] THEN
      MATCH_MP_TAC 
LSPACE_VSUM THEN
      ASM_SIMP_TAC[
FINITE_NUMSEG; REAL_ARITH `&1 <= p ==> &0 < p`] THEN
      X_GEN_TAC `i:num` THEN ASM_CASES_TAC `(i:num) 
IN t` THEN
      ASM_SIMP_TAC[ETA_AX; 
LSPACE_0; REAL_ARITH `&1 <= p ==> ~(p = &0)`];
      AP_TERM_TAC THEN REWRITE_TAC[
FUN_EQ_THM] THEN
      X_GEN_TAC `x:real^M` THEN REWRITE_TAC[GSYM 
VSUM_RESTRICT_SET] THEN
      REWRITE_TAC[SET_RULE `s 
INTER t = {x | x 
IN t /\ x 
IN s}`]]]);;
 
let RIESZ_FISCHER = prove
 (`!f:num->real^M->real^N p s.
        &1 <= p /\ (!n. (f n) 
IN lspace s p) /\
        (!e. &0 < e
             ==> ?N. !m n. m >= N /\ n >= N
                           ==> lnorm s p (\x. f m x - f n x) < e)
        ==> ?g. g 
IN lspace s p /\
                !e. &0 < e
                    ==> ?N. !n. n >= N
                                ==> lnorm s p (\x. f n x - g x) < e`,
  REPEAT STRIP_TAC THEN
  SUBGOAL_THEN
   `?k:num->num.
        (!n. k n < k (SUC n)) /\
        (!n. lnorm s p ((\x. f (k(SUC n)) x - f (k n) x):real^M->real^N)
             < inv(&2 pow n))`
  STRIP_ASSUME_TAC THENL
   [FIRST_X_ASSUM(MP_TAC o GEN `n:num` o SPEC `inv(&2 pow n)`) THEN
    REWRITE_TAC[
REAL_LT_INV_EQ; 
REAL_LT_POW2; 
SKOLEM_THM] THEN
    DISCH_THEN(X_CHOOSE_TAC `N:num->num`) THEN
    MP_TAC(prove_recursive_functions_exist num_RECURSION
     `k 0 = N 0 /\
      !n. k(SUC n) = 
MAX (k n + 1) (
MAX (N n) (N(SUC n)))`) THEN
    MATCH_MP_TAC 
MONO_EXISTS THEN REPEAT STRIP_TAC THEN
    ASM_REWRITE_TAC[ARITH_RULE `n < 
MAX (n + 1) m`] THEN
    FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN
    CONJ_TAC THENL [ARITH_TAC; SPEC_TAC(`n:num`,`n:num`)] THEN
    INDUCT_TAC THEN ASM_REWRITE_TAC[] THEN ARITH_TAC;
    ALL_TAC] THEN
  MP_TAC(ISPECL
   [`\n x. f (k(SUC n)) x - (f:num->real^M->real^N) (k n) x`;
    `p:real`; `s:real^M->bool`] 
LSPACE_SUMMABLE_UNIV) THEN
  ASM_REWRITE_TAC[] THEN ANTS_TAC THENL
   [ASM_SIMP_TAC[
LSPACE_SUB; ETA_AX; REAL_ARITH `&1 <= p ==> &0 <= p`] THEN
    MATCH_MP_TAC 
REAL_SUMMABLE_COMPARISON THEN
    EXISTS_TAC `\n. inv(&2) pow n` THEN CONJ_TAC THENL
     [MATCH_MP_TAC 
REAL_SUMMABLE_GP THEN CONV_TAC REAL_RAT_REDUCE_CONV;
      EXISTS_TAC `0` THEN X_GEN_TAC `n:num` THEN DISCH_THEN(K ALL_TAC) THEN
      REWRITE_TAC[GSYM 
REAL_INV_POW] THEN
      MATCH_MP_TAC(REAL_ARITH `&0 <= x /\ x < y ==> abs x <= y`) THEN
      ASM_SIMP_TAC[
LNORM_POS_LE; 
LSPACE_SUB; ETA_AX;
                   REAL_ARITH `&1 <= p ==> &0 <= p`]];
    DISCH_THEN(X_CHOOSE_THEN `g:real^M->real^N` MP_TAC) THEN
    DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC (LABEL_TAC "*")) THEN
    EXISTS_TAC `\x. (g:real^M->real^N) x + f (k 0:num) x` THEN
    ASM_SIMP_TAC[
LSPACE_ADD; ETA_AX; REAL_ARITH `&1 <= p ==> &0 <= p`] THEN
    X_GEN_TAC `e:real` THEN DISCH_TAC THEN
    REMOVE_THEN "*" (MP_TAC o SPEC `e / &2`) THEN
    ASM_REWRITE_TAC[
REAL_HALF; 
EVENTUALLY_SEQUENTIALLY] THEN
    REWRITE_TAC[
ADD1; 
VSUM_DIFFS_ALT; 
LE_0] THEN
    DISCH_THEN(X_CHOOSE_THEN `N1:num` (LABEL_TAC "+")) THEN
    FIRST_X_ASSUM(MP_TAC o SPEC `e / &2`) THEN
    ASM_REWRITE_TAC[
REAL_HALF; 
GE] THEN
    DISCH_THEN(X_CHOOSE_TAC `N2:num`) THEN
    EXISTS_TAC `
MAX N1 N2` THEN X_GEN_TAC `n:num` THEN
    REWRITE_TAC[ARITH_RULE `
MAX N1 N2 <= n <=> N1 <= n /\ N2 <= n`] THEN
    STRIP_TAC THEN REMOVE_THEN "+" (MP_TAC o SPEC `n:num`) THEN
    FIRST_X_ASSUM(MP_TAC o SPECL [`k(n + 1):num`; `n:num`]) THEN
    ASM_REWRITE_TAC[] THEN ANTS_TAC THENL
     [MATCH_MP_TAC 
LE_TRANS THEN EXISTS_TAC `n + 1` THEN
      CONJ_TAC THENL [ASM_ARITH_TAC; SPEC_TAC(`n + 1`,`m:num`)] THEN
      INDUCT_TAC THEN REWRITE_TAC[
LE_0] THEN
      MATCH_MP_TAC(ARITH_RULE
       `m <= k m /\ k m < k(SUC m) ==> SUC m <= k(SUC m)`) THEN
      ASM_REWRITE_TAC[];
      REPEAT DISCH_TAC THEN
      ONCE_REWRITE_TAC[VECTOR_ARITH
       `f n x - (g x + f (k 0) x):real^N =
        (f (k (n + 1)) x - f (k 0) x - g x) +
        --(f (k (n + 1)) x - f n x)`] THEN
      W(MP_TAC o PART_MATCH (lhand o rand) 
LNORM_TRIANGLE o lhand o snd) THEN
      ASM_SIMP_TAC[
LSPACE_SUB; 
LSPACE_NEG; ETA_AX;
                    REAL_ARITH `&1 <= p ==> &0 <= p`] THEN
      MATCH_MP_TAC(REAL_ARITH
       `x < e / &2 /\ y < e / &2 ==> z <= x + y ==> z < e`) THEN
      ASM_SIMP_TAC[
LNORM_NEG; 
LSPACE_SUB; ETA_AX;
                   REAL_ARITH `&1 <= p ==> &0 <= p`]]]);;
 
let LSPACE_DOMINATED_CONVERGENCE = prove
 (`!f:num->real^M->real^N g h:real^M->real^N s p k.
        &0 < p /\
        (!n. (f n) 
IN lspace s p) /\ h 
IN lspace s p /\
        (!n x. x 
IN s ==> norm(f n x) <= norm(h x)) /\
        negligible k /\
        (!x. x 
IN s 
DIFF k ==> ((\n. f n x) --> g(x)) sequentially)
        ==> g 
IN lspace s p /\
            ((\n. lnorm s p (\x. f n x - g x)) ---> &0) sequentially`,
 
let LSPACE_APPROXIMATE_CONTINUOUS = prove
 (`!f:real^M->real^N s p e.
        &1 <= p /\ measurable s /\ f 
IN lspace s p /\ &0 < e
        ==> ?g. g 
continuous_on (:real^M) /\
                g 
IN lspace s p /\
                lnorm s p (\x. f x - g x) < e`,
  REPEAT STRIP_TAC THEN
  FIRST_ASSUM(ASSUME_TAC o MATCH_MP (REAL_ARITH `&1 <= p ==> &0 < p`)) THEN
  MP_TAC(ISPECL [`f:real^M->real^N`; `s:real^M->bool`; `p:real`; `e / &2`]
        
LSPACE_APPROXIMATE_BOUNDED) THEN
  ASM_REWRITE_TAC[
REAL_HALF] THEN
  DISCH_THEN(X_CHOOSE_THEN `h:real^M->real^N` STRIP_ASSUME_TAC) THEN
  FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [
BOUNDED_POS]) THEN
  REWRITE_TAC[
FORALL_IN_IMAGE] THEN
  DISCH_THEN(X_CHOOSE_THEN `B:real` STRIP_ASSUME_TAC) THEN
  SUBGOAL_THEN
   `?k g. negligible k /\
          (!n. g n 
continuous_on (:real^M)) /\
          (!n x. x 
IN s ==> norm(g n x:real^N) <= norm(B % vec 1:real^N)) /\
          (!x. x 
IN (s 
DIFF k)  ==> ((\n. g n x) --> h x) sequentially)`
  STRIP_ASSUME_TAC THENL
   [SUBGOAL_THEN `(h:real^M->real^N) 
measurable_on s` MP_TAC THENL
     [RULE_ASSUM_TAC(REWRITE_RULE[lspace; 
IN_ELIM_THM]) THEN ASM_REWRITE_TAC[];
      ALL_TAC] THEN
    REWRITE_TAC[
measurable_on] THEN MATCH_MP_TAC 
MONO_EXISTS THEN
    X_GEN_TAC `k:real^M->bool` THEN
    DISCH_THEN(X_CHOOSE_THEN `g:num->real^M->real^N` STRIP_ASSUME_TAC) THEN
    EXISTS_TAC `(\n x. lambda i. max (--B) (min B (((g n x):real^N)$i))):
                num->real^M->real^N` THEN
    ASM_REWRITE_TAC[] THEN REPEAT CONJ_TAC THENL
     [X_GEN_TAC `n:num` THEN
      FIRST_X_ASSUM(MP_TAC o SPEC `n:num`) THEN
      MP_TAC(ISPECL [`(:real^M)`; `(lambda i. B):real^N`]
                
CONTINUOUS_ON_CONST) THEN
      REWRITE_TAC[IMP_IMP] THEN
      DISCH_THEN(MP_TAC o MATCH_MP 
CONTINUOUS_ON_MIN) THEN
      MP_TAC(ISPECL [`(:real^M)`; `(lambda i. --B):real^N`]
                
CONTINUOUS_ON_CONST) THEN
      REWRITE_TAC[IMP_IMP] THEN
      DISCH_THEN(MP_TAC o MATCH_MP 
CONTINUOUS_ON_MAX) THEN
      MATCH_MP_TAC EQ_IMP THEN AP_THM_TAC THEN AP_TERM_TAC THEN
      SIMP_TAC[
FUN_EQ_THM; 
CART_EQ; 
LAMBDA_BETA];
      REPEAT STRIP_TAC THEN MATCH_MP_TAC 
NORM_LE_COMPONENTWISE THEN
      SIMP_TAC[
LAMBDA_BETA; 
VEC_COMPONENT; 
VECTOR_MUL_COMPONENT] THEN
      REAL_ARITH_TAC;
      X_GEN_TAC `x:real^M` THEN REWRITE_TAC[
IN_DIFF] THEN STRIP_TAC THEN
      FIRST_X_ASSUM(MP_TAC o SPEC `x:real^M`) THEN ASM_REWRITE_TAC[] THEN
      REWRITE_TAC[
LIM_SEQUENTIALLY] THEN
      MATCH_MP_TAC 
MONO_FORALL THEN X_GEN_TAC `ee:real` THEN
      MATCH_MP_TAC MONO_IMP THEN REWRITE_TAC[] THEN
      MATCH_MP_TAC 
MONO_EXISTS THEN X_GEN_TAC `N:num` THEN
      MATCH_MP_TAC 
MONO_FORALL THEN X_GEN_TAC `n:num` THEN
      MATCH_MP_TAC MONO_IMP THEN REWRITE_TAC[] THEN
      MATCH_MP_TAC(NORM_ARITH
       `norm(c - a:real^N) <= norm(b - a)
        ==> dist(b,a) < ee ==> dist(c,a) < ee`) THEN
      MATCH_MP_TAC 
NORM_LE_COMPONENTWISE THEN
      SIMP_TAC[
LAMBDA_BETA; 
VECTOR_SUB_COMPONENT] THEN
      X_GEN_TAC `k:num` THEN STRIP_TAC THEN
      FIRST_X_ASSUM(MP_TAC o SPEC `x:real^M`) THEN ASM_REWRITE_TAC[] THEN
      DISCH_THEN(MP_TAC o MATCH_MP 
NORM_BOUND_COMPONENT_LE) THEN
      DISCH_THEN(MP_TAC o SPEC `k:num`) THEN ASM_REWRITE_TAC[] THEN
      REAL_ARITH_TAC];
    ALL_TAC] THEN
  SUBGOAL_THEN `!n. ((g:num->real^M->real^N) n) 
IN lspace s p` ASSUME_TAC THENL
   [X_GEN_TAC `n:num` THEN
    MATCH_MP_TAC 
LSPACE_BOUNDED_MEASURABLE THEN
    EXISTS_TAC `(\x. B % vec 1):real^M->real^N` THEN
    ASM_SIMP_TAC[
LSPACE_CONST] THEN
    ONCE_REWRITE_TAC[GSYM 
MEASURABLE_ON_UNIV] THEN
    MATCH_MP_TAC(REWRITE_RULE[
lebesgue_measurable; indicator]
        
MEASURABLE_ON_RESTRICT) THEN
    ASM_SIMP_TAC[
CONTINUOUS_IMP_MEASURABLE_ON; ETA_AX] THEN
    MATCH_MP_TAC 
INTEGRABLE_IMP_MEASURABLE THEN
    ASM_REWRITE_TAC[GSYM 
MEASURABLE_INTEGRABLE];
    ALL_TAC] THEN
  MP_TAC(ISPECL
   [`g:num->real^M->real^N`; `h:real^M->real^N`;
    `(\x. B % vec 1):real^M->real^N`;
    `s:real^M->bool`; `p:real`; `k:real^M->bool`]
        
LSPACE_DOMINATED_CONVERGENCE) THEN
  ASM_SIMP_TAC[
LSPACE_CONST] THEN
  REWRITE_TAC[
REALLIM_SEQUENTIALLY; 
REAL_SUB_RZERO] THEN
  DISCH_THEN(MP_TAC o SPEC `e / &2`) THEN ASM_REWRITE_TAC[
REAL_HALF] THEN
  DISCH_THEN(X_CHOOSE_THEN `n:num` (MP_TAC o SPEC `n:num`)) THEN
  REWRITE_TAC[
LE_REFL] THEN DISCH_TAC THEN
  EXISTS_TAC `(g:num->real^M->real^N) n` THEN
  ASM_REWRITE_TAC[] THEN
  SUBGOAL_THEN
   `(\x. f x - (g:num->real^M->real^N) n x) =
    (\x. (f x - h x) + --(g n x - h x))`
  SUBST1_TAC THENL [SIMP_TAC[
FUN_EQ_THM] THEN VECTOR_ARITH_TAC; ALL_TAC] THEN
  W(MP_TAC o PART_MATCH (lhand o rand) 
LNORM_TRIANGLE o lhand o snd) THEN
  ASM_SIMP_TAC[
LSPACE_SUB; ETA_AX; 
REAL_LT_IMP_LE; 
LSPACE_NEG] THEN
  MATCH_MP_TAC(REAL_ARITH
   `y < e / &2 /\ z < e / &2 ==> x <= y + z ==> x < e`) THEN
  ASM_SIMP_TAC[
LNORM_NEG; REAL_ARITH `abs x < e ==> x < e`]);;
 
let L2PRODUCT_SYM = prove
 (`!s f g. l2product s f g = l2product s g f`,
  REWRITE_TAC[l2product; REAL_MUL_SYM]);;
 
let ODD_EVEN_INDUCT_LEMMA = prove
 (`(!n:num. P 0) /\ (!n. P(2 * n + 1)) /\ (!n. P(2 * n + 2)) ==> !n. P n`,
  REWRITE_TAC[
FORALL_SIMP] THEN STRIP_TAC THEN
  MATCH_MP_TAC 
num_INDUCTION THEN ASM_REWRITE_TAC[] THEN
  X_GEN_TAC `n:num` THEN DISCH_THEN(K ALL_TAC) THEN
  MP_TAC(ISPEC `n:num` 
EVEN_OR_ODD) THEN
  REWRITE_TAC[
EVEN_EXISTS; 
ODD_EXISTS] THEN STRIP_TAC THEN
  ASM_REWRITE_TAC[ARITH_RULE
    `SUC(2 * n) = 2 * n + 1 /\ SUC(2 * n + 1) = 2 * n + 2`]);;
 
let FOURIER_SUM_LIMIT_PAIR = prove
 (`!f n t l.
        f 
absolutely_real_integrable_on real_interval [--pi,pi]
        ==> (((\n. sum(0..2*n) (\k. 
fourier_coefficient f k *
                                    
trigonometric_set k t)) ---> l)
             sequentially <=>
             ((\n. sum(0..n) (\k. 
fourier_coefficient f k *
                                  
trigonometric_set k t)) ---> l)
             sequentially)`,
  REPEAT STRIP_TAC THEN REWRITE_TAC[
REALLIM_SEQUENTIALLY] THEN
  EQ_TAC THEN DISCH_TAC THEN X_GEN_TAC `e:real` THEN DISCH_TAC THENL
   [FIRST_ASSUM(MP_TAC o MATCH_MP 
RIEMANN_LEBESGUE) THEN
    REWRITE_TAC[
REALLIM_SEQUENTIALLY; 
REAL_SUB_RZERO] THEN
    DISCH_THEN(MP_TAC o SPEC `e / &2`) THEN ASM_REWRITE_TAC[
REAL_HALF] THEN
    DISCH_THEN(X_CHOOSE_THEN `N1:num` (LABEL_TAC "1")) THEN
    SUBGOAL_THEN `&0 < e / &2` (fun th -> FIRST_ASSUM(MP_TAC o C MATCH_MP th))
    THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
    DISCH_THEN(X_CHOOSE_THEN `N2:num` (LABEL_TAC "2")) THEN
    EXISTS_TAC `N1 + 2 * N2 + 1` THEN X_GEN_TAC `n:num` THEN DISCH_TAC THEN
    DISJ_CASES_THEN SUBST1_TAC
     (ARITH_RULE `n = 2 * n DIV 2 \/ n = SUC(2 * n DIV 2)`) THEN
    REWRITE_TAC[
SUM_CLAUSES_NUMSEG; 
LE_0] THENL
     [MATCH_MP_TAC(REAL_ARITH `abs x < e / &2 ==> abs x < e`) THEN
      FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC;
      MATCH_MP_TAC(REAL_ARITH
       `abs(x - l) < e / &2 /\ abs y < e / &2 ==> abs((x + y) - l) < e`) THEN
      CONJ_TAC THENL
       [FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC; ALL_TAC] THEN
      MATCH_MP_TAC(REAL_ARITH
       `abs(x * y) <= abs(x) * &1 /\ abs(x) < e ==> abs(x * y) < e`) THEN
      CONJ_TAC THENL
       [REWRITE_TAC[
REAL_ABS_MUL] THEN MATCH_MP_TAC 
REAL_LE_LMUL THEN
        REWRITE_TAC[
REAL_ABS_POS] THEN
        SPEC_TAC(`SUC(2 * n DIV 2)`,`r:num`) THEN
        MATCH_MP_TAC 
ODD_EVEN_INDUCT_LEMMA THEN
        REWRITE_TAC[
ADD1; 
trigonometric_set; 
REAL_ABS_DIV] THEN
        SIMP_TAC[
REAL_LE_LDIV_EQ; REAL_ARITH `&0 < x ==> &0 < abs x`;
                 
SQRT_POS_LT; REAL_ARITH `&0 < &2 * x <=> &0 < x`; 
PI_POS] THEN
        REPEAT STRIP_TAC THEN MATCH_MP_TAC 
REAL_LE_TRANS THEN
        EXISTS_TAC `&1` THEN REWRITE_TAC[
COS_BOUND; 
SIN_BOUND] THEN
        MATCH_MP_TAC(REAL_ARITH `&1 <= x ==> &1 <= &1 * abs x`) THEN
        SUBST1_TAC(GSYM 
SQRT_1) THEN MATCH_MP_TAC 
SQRT_MONO_LE THEN
        MP_TAC 
PI_APPROX_32 THEN REAL_ARITH_TAC;
        FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC]];
    FIRST_X_ASSUM(MP_TAC o SPEC `e:real`) THEN ASM_REWRITE_TAC[] THEN
    MATCH_MP_TAC 
MONO_EXISTS THEN GEN_TAC THEN DISCH_TAC THEN
    REPEAT STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC]);;
 
let DIRICHLET_KERNEL_0 = prove
 (`!x. abs(x) < &2 * pi ==> 
dirichlet_kernel 0 x = &1 / &2`,
  REPEAT STRIP_TAC THEN REWRITE_TAC[
dirichlet_kernel] THEN
  COND_CASES_TAC THEN ASM_REWRITE_TAC[REAL_ADD_LID] THEN
  REWRITE_TAC[
real_div; REAL_MUL_LID; REAL_MUL_SYM; 
REAL_MUL_RID] THEN
  MATCH_MP_TAC(REAL_FIELD `~(x = &0) ==> inv(&2 * x) * x = inv(&2)`) THEN
  DISCH_TAC THEN SUBGOAL_THEN `~(x * inv(&2) = &0)` MP_TAC THENL
   [ASM_REAL_ARITH_TAC; REWRITE_TAC[] THEN MATCH_MP_TAC 
SIN_EQ_0_PI] THEN
  ASM_REAL_ARITH_TAC);;
 
let COSINE_SUM_LEMMA = prove
 (`!n x. (&1 / &2 + sum(1..n) (\k. cos(&k * x))) * sin(x / &2) =
         sin((&n + &1 / &2) * x) / &2`,
  REPEAT STRIP_TAC THEN DISJ_CASES_TAC(ARITH_RULE `n = 0 \/ 1 <= n`) THENL
   [ASM_REWRITE_TAC[REAL_ADD_LID; 
SUM_CLAUSES_NUMSEG; ARITH] THEN
    REWRITE_TAC[
real_div; REAL_MUL_LID; 
REAL_ADD_RID; REAL_MUL_SYM];
    REPEAT STRIP_TAC THEN REWRITE_TAC[
REAL_ADD_RDISTRIB; GSYM 
SUM_RMUL] THEN
    REWRITE_TAC[
REAL_MUL_COS_SIN; 
real_div; 
REAL_SUB_RDISTRIB] THEN
    SUBGOAL_THEN
     `!k x. &k * x + x * inv(&2) = (&(k + 1) * x - x * inv(&2))`
     (fun th -> REWRITE_TAC[th; 
SUM_DIFFS_ALT])
    THENL [REWRITE_TAC[GSYM REAL_OF_NUM_ADD] THEN REAL_ARITH_TAC; ALL_TAC] THEN
    ASM_REWRITE_TAC[GSYM REAL_OF_NUM_ADD; GSYM 
real_div] THEN
    REWRITE_TAC[REAL_ARITH `&1 * x - x / &2 = x / &2`] THEN
    REWRITE_TAC[REAL_ARITH `(&n + &1) * x - x / &2 = (&n + &1 / &2) * x`] THEN
    REWRITE_TAC[
REAL_ADD_RDISTRIB] THEN REAL_ARITH_TAC]);;
 
let FOURIER_SUM_LIMIT_SINE_PART = prove
 (`!f t l d.
        f 
absolutely_real_integrable_on real_interval[--pi,pi] /\
        (!x. f (x + &2 * pi) = f x) /\ &0 < d /\ d <= pi
        ==> (((\n. sum (0..n)
                       (\k. 
fourier_coefficient f k * 
trigonometric_set k t))
              ---> l) sequentially <=>
            ((\n. 
real_integral (
real_interval[&0,d])
                                (\x. sin((&n + &1 / &2) * x) *
                                     ((f(t + x) + f(t - x)) - &2 * l) / x))
             ---> &0) sequentially)`,
  let lemma0 = prove
   (`!x. abs(sin(x) - x) <= abs(x) pow 3`,
    GEN_TAC THEN MP_TAC(ISPECL [`0`; `Cx x`] TAYLOR_CSIN) THEN
    REWRITE_TAC[VSUM_CLAUSES_NUMSEG; GSYM CX_SIN] THEN
    CONV_TAC NUM_REDUCE_CONV THEN
    REWRITE_TAC[complex_pow; COMPLEX_POW_1; COMPLEX_DIV_1; IM_CX] THEN
    REWRITE_TAC[GSYM CX_MUL; GSYM CX_SUB; COMPLEX_NORM_CX; REAL_ABS_0] THEN
    REWRITE_TAC[REAL_EXP_0; REAL_MUL_LID] THEN REAL_ARITH_TAC) in
  let lemma1 = prove
   (`!x. ~(x = &0) ==> abs(sin(x) / x - &1) <= x pow 2`,
    REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[GSYM REAL_POW2_ABS] THEN
    MATCH_MP_TAC REAL_LE_LCANCEL_IMP THEN EXISTS_TAC `abs x` THEN
    REWRITE_TAC[GSYM REAL_ABS_MUL; GSYM(CONJUNCT2 real_pow)] THEN
    ASM_REWRITE_TAC[GSYM REAL_ABS_NZ; ARITH] THEN
    ASM_SIMP_TAC[REAL_SUB_LDISTRIB; REAL_DIV_LMUL; REAL_MUL_RID] THEN
    REWRITE_TAC[lemma0]) in
  let lemma2 = prove
   (`!x. abs(x) <= &1 / &2  ==> abs(x) / &2 <= abs(sin x)`,
    REPEAT STRIP_TAC THEN MP_TAC(SPEC `x:real` lemma0) THEN
    MATCH_MP_TAC(REAL_ARITH
      `&4 * x3 <= abs x ==> abs(s - x) <= x3 ==> abs(x) / &2 <= abs s`) THEN
    REWRITE_TAC[REAL_ARITH
     `&4 * x pow 3 <= x <=> x * x pow 2 <= x * (&1 / &2) pow 2`] THEN
    MATCH_MP_TAC REAL_LE_LMUL THEN REWRITE_TAC[GSYM REAL_LE_SQUARE_ABS] THEN
    ASM_REAL_ARITH_TAC) in
  let lemma3 = prove
   (`!x. ~(x = &0) /\ abs x <= &1 / &2
         ==> abs(inv(sin x) - inv x) <= &2 * abs x`,
    REPEAT STRIP_TAC THEN
    MATCH_MP_TAC REAL_LE_LCANCEL_IMP THEN EXISTS_TAC `abs(sin x)` THEN
    REWRITE_TAC[GSYM REAL_ABS_MUL] THEN ASM_CASES_TAC `sin x = &0` THENL
     [MP_TAC(SPEC `x:real` SIN_EQ_0_PI) THEN
      MP_TAC PI_APPROX_32 THEN ASM_REAL_ARITH_TAC;
      ASM_SIMP_TAC[GSYM REAL_ABS_NZ; REAL_SUB_LDISTRIB; REAL_MUL_RINV] THEN
      REWRITE_TAC[REAL_ARITH `abs(&1 - s * inv x) = abs(s / x - &1)`] THEN
      MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `(x:real) pow 2` THEN
      ASM_SIMP_TAC[lemma1] THEN ONCE_REWRITE_TAC[GSYM REAL_POW2_ABS] THEN
      REWRITE_TAC[REAL_POW_2; REAL_MUL_ASSOC] THEN
      MATCH_MP_TAC REAL_LE_RMUL THEN
      MP_TAC(ISPEC `x:real` lemma2) THEN ASM_REAL_ARITH_TAC]) in
  REPEAT STRIP_TAC THEN
  MP_TAC(ISPECL [`f:real->real`; `t:real`; `l:real`; `d:real`]
        FOURIER_SUM_LIMIT_DIRICHLET_KERNEL_PART) THEN
  ASM_REWRITE_TAC[] THEN MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC THEN
  MATCH_MP_TAC REALLIM_TRANSFORM_EQ THEN REWRITE_TAC[] THEN
  MATCH_MP_TAC REALLIM_TRANSFORM_EVENTUALLY THEN
  MP_TAC(ISPECL [`f:real->real`; `--pi`; `pi`; `t:real`]
        ABSOLUTELY_REAL_INTEGRABLE_PERIODIC_OFFSET) THEN
  ASM_REWRITE_TAC[REAL_ARITH `pi - --pi = &2 * pi`] THEN
  GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [REAL_ADD_SYM] THEN
  DISCH_THEN(fun th -> ASSUME_TAC th THEN MP_TAC th) THEN
  GEN_REWRITE_TAC LAND_CONV [absolutely_real_integrable_on] THEN
  GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV)
   [GSYM REAL_INTEGRABLE_REFLECT] THEN
  REWRITE_TAC[GSYM absolutely_real_integrable_on; GSYM real_sub] THEN
  REWRITE_TAC[REAL_NEG_NEG] THEN DISCH_TAC THEN EXISTS_TAC
   `\n. real_integral (real_interval[&0,d])
                      (\x. sin((&n + &1 / &2) * x) *
                           (inv(&2 * sin(x / &2)) - inv x) *
                           ((f(t + x) + f(t - x)) - &2 * l))` THEN
  REWRITE_TAC[EVENTUALLY_SEQUENTIALLY] THEN CONJ_TAC THENL
   [EXISTS_TAC `1` THEN X_GEN_TAC `n:num` THEN DISCH_TAC THEN
    REWRITE_TAC[REAL_INTEGRAL_DIRICHLET_KERNEL_MUL_EXPAND] THEN
    REWRITE_TAC[REAL_ARITH
     `a * (inv y - inv x) * b:real = a / y * b - a / x * b`] THEN
    REWRITE_TAC[REAL_ARITH `sin(y) * (a - b) / x = sin(y) / x * (a - b)`] THEN
    MATCH_MP_TAC REAL_INTEGRAL_SUB THEN CONJ_TAC THENL
     [REWRITE_TAC[GSYM REAL_INTEGRABLE_DIRICHLET_KERNEL_MUL_EXPAND] THEN
      MATCH_MP_TAC ABSOLUTELY_REAL_INTEGRABLE_IMP_INTEGRABLE THEN
      MATCH_MP_TAC ABSOLUTELY_REAL_INTEGRABLE_ON_SUBINTERVAL THEN
      EXISTS_TAC `real_interval[--pi,pi]` THEN CONJ_TAC THENL
      [ALL_TAC; REWRITE_TAC[SUBSET_REAL_INTERVAL] THEN ASM_REAL_ARITH_TAC] THEN
      MATCH_MP_TAC ABSOLUTELY_REAL_INTEGRABLE_MUL_DIRICHLET_KERNEL THEN
      ASM_SIMP_TAC[ABSOLUTELY_REAL_INTEGRABLE_ADD;
                   ABSOLUTELY_REAL_INTEGRABLE_SUB;
                   ABSOLUTELY_REAL_INTEGRABLE_CONST];
      MATCH_MP_TAC(REWRITE_RULE[IMP_IMP] REAL_INTEGRABLE_SPIKE) THEN
      EXISTS_TAC `\x. dirichlet_kernel n x * (&2 * sin(x / &2)) / x *
                      ((f(t + x) + f(t - x)) - &2 * l)` THEN
      EXISTS_TAC `{&0}` THEN REWRITE_TAC[REAL_NEGLIGIBLE_SING] THEN
      CONJ_TAC THENL
       [X_GEN_TAC `x:real` THEN
        REWRITE_TAC[IN_DIFF; IN_SING; IN_REAL_INTERVAL; REAL_MUL_ASSOC] THEN
        STRIP_TAC THEN AP_THM_TAC THEN AP_TERM_TAC THEN
        ASM_REWRITE_TAC[dirichlet_kernel] THEN
        MATCH_MP_TAC(REAL_FIELD
         `~(x = &0) /\ ~(y = &0) ==> a / x = a / (&2 * y) * (&2 * y) / x`) THEN
        MP_TAC(ISPEC `x / &2` SIN_EQ_0_PI) THEN ASM_REAL_ARITH_TAC;
        MATCH_MP_TAC ABSOLUTELY_REAL_INTEGRABLE_IMP_INTEGRABLE THEN
        MATCH_MP_TAC ABSOLUTELY_REAL_INTEGRABLE_ON_SUBINTERVAL THEN
        EXISTS_TAC `real_interval[--pi,pi]` THEN CONJ_TAC THENL
         [ALL_TAC;
          REWRITE_TAC[SUBSET_REAL_INTERVAL] THEN ASM_REAL_ARITH_TAC] THEN
        MATCH_MP_TAC ABSOLUTELY_REAL_INTEGRABLE_MUL_DIRICHLET_KERNEL THEN
        MATCH_MP_TAC ABSOLUTELY_REAL_INTEGRABLE_BOUNDED_MEASURABLE_PRODUCT THEN
        ASM_SIMP_TAC[ABSOLUTELY_REAL_INTEGRABLE_ADD;
                     ABSOLUTELY_REAL_INTEGRABLE_SUB;
                     ABSOLUTELY_REAL_INTEGRABLE_CONST] THEN
        CONJ_TAC THENL
         [MATCH_MP_TAC REAL_MEASURABLE_ON_DIV THEN
          REWRITE_TAC[REAL_NEGLIGIBLE_SING; SING_GSPEC] THEN
          CONJ_TAC THEN MATCH_MP_TAC
            REAL_CONTINUOUS_IMP_REAL_MEASURABLE_ON_CLOSED_SUBSET THEN
          REWRITE_TAC[REAL_CLOSED_UNIV; REAL_CLOSED_REAL_INTERVAL] THEN
          REWRITE_TAC[REAL_CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN] THEN
          REPEAT STRIP_TAC THEN
          MATCH_MP_TAC REAL_CONTINUOUS_ATREAL_WITHINREAL THEN
          MATCH_MP_TAC REAL_DIFFERENTIABLE_IMP_CONTINUOUS_ATREAL THEN
          REAL_DIFFERENTIABLE_TAC;
          ALL_TAC]]] THEN
    SUBGOAL_THEN `real_bounded (IMAGE (\x. &1 + (x / &2) pow 2)
                                      (real_interval[--pi,pi]))`
    MP_TAC THENL
     [MATCH_MP_TAC REAL_COMPACT_IMP_BOUNDED THEN
      MATCH_MP_TAC REAL_COMPACT_CONTINUOUS_IMAGE THEN
      REWRITE_TAC[REAL_COMPACT_INTERVAL] THEN
      REWRITE_TAC[REAL_CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN] THEN
      REPEAT STRIP_TAC THEN
      MATCH_MP_TAC REAL_CONTINUOUS_ATREAL_WITHINREAL THEN
      MATCH_MP_TAC REAL_DIFFERENTIABLE_IMP_CONTINUOUS_ATREAL THEN
      REAL_DIFFERENTIABLE_TAC;
      REWRITE_TAC[REAL_BOUNDED_POS; FORALL_IN_IMAGE] THEN
      MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `B:real` THEN
      DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC (LABEL_TAC "*")) THEN
      ASM_REWRITE_TAC[] THEN X_GEN_TAC `x:real` THEN DISCH_TAC THEN
      ASM_CASES_TAC `x = &0` THENL
       [ASM_REWRITE_TAC[real_div; REAL_INV_0; REAL_MUL_RID] THEN
        ASM_REAL_ARITH_TAC;
        REMOVE_THEN "*" (MP_TAC o SPEC `x:real`) THEN ASM_REWRITE_TAC[] THEN
        MATCH_MP_TAC(REAL_ARITH
         `abs(z - &1) <= y ==> abs(&1 + y) <= B ==> abs(z) <= B`) THEN
        ASM_SIMP_TAC[REAL_FIELD
          `~(x = &0) ==> (&2 * y) / x = y / (x / &2)`] THEN
        MATCH_MP_TAC lemma1 THEN ASM_REAL_ARITH_TAC]];
    SUBGOAL_THEN `real_interval[&0,d] SUBSET real_interval[--pi,pi]`
    MP_TAC THENL
     [REWRITE_TAC[SUBSET_REAL_INTERVAL] THEN ASM_REAL_ARITH_TAC;
      DISCH_THEN(fun th -> REWRITE_TAC
       [GSYM(MATCH_MP REAL_INTEGRAL_RESTRICT th)])] THEN
    REWRITE_TAC[MESON[REAL_MUL_LZERO; REAL_MUL_RZERO]
     `(if p x then a x * b x * c x else &0) =
      a x * (if p x then b x else &0) * c x`] THEN
    MATCH_MP_TAC RIEMANN_LEBESGUE_SIN_HALF THEN
    MATCH_MP_TAC ABSOLUTELY_REAL_INTEGRABLE_BOUNDED_MEASURABLE_PRODUCT THEN
    ASM_SIMP_TAC[ABSOLUTELY_REAL_INTEGRABLE_ADD;
                 ABSOLUTELY_REAL_INTEGRABLE_SUB;
                 ABSOLUTELY_REAL_INTEGRABLE_CONST] THEN
    CONJ_TAC THENL
     [MATCH_MP_TAC REAL_MEASURABLE_ON_CASES THEN
      REWRITE_TAC[REAL_MEASURABLE_ON_0; SET_RULE `{x | x IN s} = s`;
                  REAL_LEBESGUE_MEASURABLE_INTERVAL] THEN
      MATCH_MP_TAC REAL_MEASURABLE_ON_SUB THEN CONJ_TAC THEN
      GEN_REWRITE_TAC (LAND_CONV) [GSYM ETA_AX] THEN REWRITE_TAC[] THEN
      ONCE_REWRITE_TAC[REAL_ARITH `inv x = &1 / x`] THEN
      MATCH_MP_TAC REAL_MEASURABLE_ON_DIV THEN
      SIMP_TAC[REAL_CONTINUOUS_IMP_REAL_MEASURABLE_ON_CLOSED_SUBSET;
               REAL_CLOSED_REAL_INTERVAL; REAL_CONTINUOUS_ON_CONST;
               REAL_CONTINUOUS_ON_ID; SING_GSPEC; REAL_NEGLIGIBLE_SING;
               REAL_CLOSED_UNIV] THEN
      CONJ_TAC THENL
       [MATCH_MP_TAC CONTINUOUS_IMP_REAL_MEASURABLE_ON THEN
        REWRITE_TAC[REAL_CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN] THEN
        REPEAT STRIP_TAC THEN
        MATCH_MP_TAC REAL_CONTINUOUS_ATREAL_WITHINREAL THEN
        MATCH_MP_TAC REAL_DIFFERENTIABLE_IMP_CONTINUOUS_ATREAL THEN
        REAL_DIFFERENTIABLE_TAC;
        REWRITE_TAC[REAL_ARITH `&2 * x = &0 <=> x = &0`] THEN
        REWRITE_TAC[REAL_SIN_X2_ZEROS] THEN
        MATCH_MP_TAC REAL_NEGLIGIBLE_COUNTABLE THEN
        MATCH_MP_TAC COUNTABLE_IMAGE THEN REWRITE_TAC[COUNTABLE_INTEGER]];
      ALL_TAC] THEN
    SUBGOAL_THEN
     `real_bounded(IMAGE (\x. inv (&2 * sin (x / &2)) - inv x)
                         (real_interval[--pi,-- &1] UNION
                          real_interval[&1,pi]))`
    MP_TAC THENL
     [MATCH_MP_TAC REAL_COMPACT_IMP_BOUNDED THEN
      MATCH_MP_TAC REAL_COMPACT_CONTINUOUS_IMAGE THEN
      SIMP_TAC[REAL_COMPACT_INTERVAL; REAL_COMPACT_UNION] THEN
      REWRITE_TAC[REAL_CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN] THEN
      REPEAT STRIP_TAC THEN
      MATCH_MP_TAC REAL_CONTINUOUS_ATREAL_WITHINREAL THEN
      MATCH_MP_TAC REAL_DIFFERENTIABLE_IMP_CONTINUOUS_ATREAL THEN
      REAL_DIFFERENTIABLE_TAC THEN MP_TAC(ISPEC `x / &2` SIN_EQ_0_PI) THEN
      FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [IN_UNION]) THEN
      REWRITE_TAC[IN_REAL_INTERVAL] THEN REAL_ARITH_TAC;
      ALL_TAC] THEN
    REWRITE_TAC[REAL_BOUNDED_POS; FORALL_IN_IMAGE] THEN
    REWRITE_TAC[IN_REAL_INTERVAL; IN_UNION] THEN
    DISCH_THEN(X_CHOOSE_THEN `B:real` STRIP_ASSUME_TAC) THEN
    EXISTS_TAC `max B (&2)` THEN CONJ_TAC THENL [REAL_ARITH_TAC; ALL_TAC] THEN
    X_GEN_TAC `x:real` THEN STRIP_TAC THEN
    COND_CASES_TAC THENL [ALL_TAC; ASM_REAL_ARITH_TAC] THEN
    ASM_CASES_TAC `abs(x) <= &1` THENL
     [ALL_TAC;
      MATCH_MP_TAC(REAL_ARITH `x <= B ==> x <= max B C`) THEN
      FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REAL_ARITH_TAC] THEN
    ASM_CASES_TAC `x = &0` THENL
     [ASM_REWRITE_TAC[real_div; REAL_MUL_LZERO; REAL_INV_0; SIN_0] THEN
      ASM_REAL_ARITH_TAC;
      ALL_TAC] THEN
    REWRITE_TAC[REAL_INV_MUL] THEN
    MATCH_MP_TAC(REAL_ARITH
     `abs(is - &2 * ix) <= &1 ==> abs(inv(&2) * is - ix) <= max B (&2)`) THEN
    REWRITE_TAC[GSYM real_div] THEN
    GEN_REWRITE_TAC (LAND_CONV o RAND_CONV o RAND_CONV)
     [GSYM REAL_INV_DIV] THEN
    MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&2 * abs(x / &2)` THEN
    CONJ_TAC THENL [MATCH_MP_TAC lemma3; ASM_REAL_ARITH_TAC] THEN
    ASM_REAL_ARITH_TAC]);;  
let FOURIER_DINI_TEST = prove
 (`!f t l d.
        f 
absolutely_real_integrable_on real_interval[--pi,pi] /\
        (!x. f (x + &2 * pi) = f x) /\
        &0 < d /\
        (\x. abs((f(t + x) + f(t - x)) - &2 * l) / x)
        
real_integrable_on real_interval[&0,d]
        ==> ((\n. sum (0..n)
                      (\k. 
fourier_coefficient f k * 
trigonometric_set k t))
             ---> l) sequentially`,
  REPEAT STRIP_TAC THEN
  MP_TAC(ISPECL [`f:real->real`; `t:real`; `l:real`; `pi`]
                
FOURIER_SUM_LIMIT_SINE_PART) THEN
  ASM_REWRITE_TAC[
PI_POS; 
REAL_LE_REFL] THEN DISCH_THEN SUBST1_TAC THEN
  REWRITE_TAC[
REALLIM_SEQUENTIALLY] THEN X_GEN_TAC `e:real` THEN DISCH_TAC THEN
  FIRST_ASSUM(MP_TAC o MATCH_MP 
REAL_INDEFINITE_INTEGRAL_CONTINUOUS_RIGHT) THEN
  REWRITE_TAC[
real_continuous_on] THEN DISCH_THEN(MP_TAC o SPEC `&0`) THEN
  ASM_SIMP_TAC[
IN_REAL_INTERVAL; 
REAL_LE_REFL; 
REAL_LT_IMP_LE] THEN
  SIMP_TAC[
REAL_INTEGRAL_NULL; 
REAL_LE_REFL] THEN
  DISCH_THEN(MP_TAC o SPEC `e / &2`) THEN ASM_REWRITE_TAC[
REAL_HALF] THEN
  DISCH_THEN(X_CHOOSE_THEN `k:real` (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
  ABBREV_TAC `dd = min d (min (k / &2) pi)` THEN
  DISCH_THEN(MP_TAC o SPEC `dd:real`) THEN
  REWRITE_TAC[
REAL_SUB_RZERO] THEN ANTS_TAC THENL
   [MP_TAC 
PI_POS THEN ASM_REAL_ARITH_TAC; ALL_TAC] THEN
  SUBGOAL_THEN `&0 < dd /\ dd <= d /\ dd <= pi /\ dd < k`
  STRIP_ASSUME_TAC THENL
   [MP_TAC 
PI_POS THEN ASM_REAL_ARITH_TAC; ALL_TAC] THEN
  MP_TAC(ISPECL [`f:real->real`; `--pi`; `pi`; `t:real`]
      
ABSOLUTELY_REAL_INTEGRABLE_PERIODIC_OFFSET) THEN
  ASM_REWRITE_TAC[REAL_ARITH `pi - --pi = &2 * pi`] THEN
  GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [REAL_ADD_SYM] THEN
  DISCH_THEN(fun th -> ASSUME_TAC th THEN MP_TAC th) THEN
  GEN_REWRITE_TAC LAND_CONV [
absolutely_real_integrable_on] THEN
  GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV)
   [GSYM 
REAL_INTEGRABLE_REFLECT] THEN
  REWRITE_TAC[GSYM 
absolutely_real_integrable_on; GSYM 
real_sub] THEN
  REWRITE_TAC[
REAL_NEG_NEG] THEN DISCH_TAC THEN
  SUBGOAL_THEN
   `(\x. ((f(t + x) + f(t - x)) - &2 * l) / x) 
absolutely_real_integrable_on
    real_interval[&0,dd]`
  ASSUME_TAC THENL
   [REWRITE_TAC[
ABSOLUTELY_REAL_INTEGRABLE_REAL_MEASURABLE] THEN CONJ_TAC THENL
     [MATCH_MP_TAC 
REAL_MEASURABLE_ON_DIV THEN
      SIMP_TAC[
REAL_CONTINUOUS_IMP_REAL_MEASURABLE_ON_CLOSED_SUBSET;
               
REAL_CLOSED_REAL_INTERVAL; 
REAL_CONTINUOUS_ON_CONST;
               
REAL_CONTINUOUS_ON_ID; 
SING_GSPEC; 
REAL_NEGLIGIBLE_SING;
               
REAL_CLOSED_UNIV] THEN
      MATCH_MP_TAC 
INTEGRABLE_IMP_REAL_MEASURABLE THEN
      MATCH_MP_TAC 
REAL_INTEGRABLE_SUBINTERVAL THEN
      MAP_EVERY EXISTS_TAC [`--pi`; `pi`] THEN
      ASM_SIMP_TAC[
ABSOLUTELY_REAL_INTEGRABLE_IMP_INTEGRABLE;
                   
REAL_INTEGRABLE_ADD; 
REAL_INTEGRABLE_SUB;
                   
REAL_INTEGRABLE_CONST] THEN
      REWRITE_TAC[
SUBSET_REAL_INTERVAL] THEN ASM_REAL_ARITH_TAC;
      MATCH_MP_TAC 
REAL_INTEGRABLE_SUBINTERVAL THEN
      MAP_EVERY EXISTS_TAC [`&0:real`; `d:real`] THEN CONJ_TAC THENL
       [FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (ONCE_REWRITE_RULE
         [TAUT `p ==> q ==> r <=> q ==> p ==> r`]
                
REAL_INTEGRABLE_SPIKE)) THEN
        EXISTS_TAC `{}:real->bool` THEN REWRITE_TAC[
REAL_NEGLIGIBLE_EMPTY] THEN
        SIMP_TAC[
REAL_ABS_DIV; 
IN_REAL_INTERVAL; 
IN_DIFF] THEN
        SIMP_TAC[
real_abs];
        REWRITE_TAC[
SUBSET_REAL_INTERVAL] THEN ASM_REAL_ARITH_TAC]];
    ALL_TAC] THEN
  SUBGOAL_THEN
   `(\x. ((f(t + x) + f(t - x)) - &2 * l) / x) 
absolutely_real_integrable_on
    real_interval[dd,pi]`
  ASSUME_TAC THENL
   [REWRITE_TAC[ONCE_REWRITE_RULE[REAL_MUL_SYM] 
real_div] THEN
    MATCH_MP_TAC 
ABSOLUTELY_REAL_INTEGRABLE_BOUNDED_MEASURABLE_PRODUCT THEN
    REPEAT CONJ_TAC THENL
     [GEN_REWRITE_TAC LAND_CONV [GSYM ETA_AX] THEN REWRITE_TAC[] THEN
      ONCE_REWRITE_TAC[REAL_ARITH `inv x = &1 / x`] THEN
      MATCH_MP_TAC 
REAL_MEASURABLE_ON_DIV THEN
      SIMP_TAC[
REAL_CONTINUOUS_IMP_REAL_MEASURABLE_ON_CLOSED_SUBSET;
               
REAL_CLOSED_REAL_INTERVAL; 
REAL_CONTINUOUS_ON_CONST;
               
REAL_CONTINUOUS_ON_ID; 
SING_GSPEC; 
REAL_NEGLIGIBLE_SING;
               
REAL_CLOSED_UNIV];
      REWRITE_TAC[
real_bounded; 
FORALL_IN_IMAGE] THEN
      EXISTS_TAC `inv dd:real` THEN X_GEN_TAC `x:real` THEN
      REWRITE_TAC[
IN_REAL_INTERVAL; 
REAL_ABS_INV] THEN STRIP_TAC THEN
      MATCH_MP_TAC 
REAL_LE_INV2 THEN ASM_REAL_ARITH_TAC;
      MATCH_MP_TAC 
ABSOLUTELY_REAL_INTEGRABLE_ON_SUBINTERVAL THEN
      EXISTS_TAC `
real_interval[--pi,pi]` THEN
      ASM_SIMP_TAC[
ABSOLUTELY_REAL_INTEGRABLE_ADD;
                   
ABSOLUTELY_REAL_INTEGRABLE_SUB;
                   
ABSOLUTELY_REAL_INTEGRABLE_CONST] THEN
      REWRITE_TAC[
SUBSET_REAL_INTERVAL] THEN ASM_REAL_ARITH_TAC];
    ALL_TAC] THEN
  SUBGOAL_THEN
   `(!n. (\x. sin((&n + &1 / &2) * x) *
           ((f(t + x) + f(t - x)) - &2 * l) / x) 
absolutely_real_integrable_on
         real_interval[&0,dd]) /\
    (!n. (\x. sin((&n + &1 / &2) * x) *
          ((f(t + x) + f(t - x)) - &2 * l) / x) 
absolutely_real_integrable_on
         real_interval[dd,pi])`
  STRIP_ASSUME_TAC THENL
   [REPEAT STRIP_TAC THEN
    MATCH_MP_TAC 
ABSOLUTELY_REAL_INTEGRABLE_BOUNDED_MEASURABLE_PRODUCT THEN
    ASM_REWRITE_TAC[] THEN
    (CONJ_TAC THENL
      [MATCH_MP_TAC 
REAL_CONTINUOUS_IMP_REAL_MEASURABLE_ON_CLOSED_SUBSET THEN
       REWRITE_TAC[
REAL_CLOSED_UNIV; 
REAL_CLOSED_REAL_INTERVAL] THEN
       REWRITE_TAC[
REAL_CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN] THEN
       REPEAT STRIP_TAC THEN
       MATCH_MP_TAC 
REAL_CONTINUOUS_ATREAL_WITHINREAL THEN
       MATCH_MP_TAC 
REAL_DIFFERENTIABLE_IMP_CONTINUOUS_ATREAL THEN
       REAL_DIFFERENTIABLE_TAC;
       REWRITE_TAC[
real_bounded; 
FORALL_IN_IMAGE] THEN
       EXISTS_TAC `&1` THEN REWRITE_TAC[
SIN_BOUND]]);
    ALL_TAC] THEN
  REPEAT STRIP_TAC THEN
  MP_TAC(ISPEC `\x. if abs x < dd then &0
                    else ((f:real->real)(t + x) - l) / x`
     
RIEMANN_LEBESGUE_SIN_HALF) THEN
  SIMP_TAC[
REAL_INTEGRAL_REFLECT_AND_ADD;
           
ABSOLUTELY_REAL_INTEGRABLE_IMP_INTEGRABLE;
           
FOURIER_PRODUCTS_INTEGRABLE_STRONG] THEN
  ANTS_TAC THENL
   [ONCE_REWRITE_TAC[GSYM 
ABSOLUTELY_REAL_INTEGRABLE_RESTRICT_UNIV] THEN
    REWRITE_TAC[MESON[] `(if P x then if Q x then &0 else a x else &0) =
                         (if P x /\ ~Q x then a x else &0)`] THEN
    REWRITE_TAC[ONCE_REWRITE_RULE[REAL_MUL_SYM] 
real_div] THEN
    REWRITE_TAC[MESON[
REAL_MUL_RZERO; 
REAL_MUL_LZERO]
    `(if P x /\ Q x then a x * b x else &0) =
     (if Q x then a x else &0) * (if P x then b x else &0)`] THEN
    MATCH_MP_TAC 
ABSOLUTELY_REAL_INTEGRABLE_BOUNDED_MEASURABLE_PRODUCT THEN
    ASM_SIMP_TAC[
ABSOLUTELY_REAL_INTEGRABLE_RESTRICT_UNIV;
                 
ABSOLUTELY_REAL_INTEGRABLE_SUB;
                 
ABSOLUTELY_REAL_INTEGRABLE_CONST] THEN
    CONJ_TAC THENL
     [MATCH_MP_TAC 
REAL_MEASURABLE_ON_CASES THEN
      REWRITE_TAC[
REAL_MEASURABLE_ON_0] THEN CONJ_TAC THENL
       [REWRITE_TAC[SET_RULE `{x | ~P x} = 
UNIV DIFF {x | P x}`] THEN
        REWRITE_TAC[
REAL_LEBESGUE_MEASURABLE_COMPL] THEN
        REWRITE_TAC[REAL_ARITH `abs x < d <=> --d < x /\ x < d`] THEN
        REWRITE_TAC[GSYM 
real_interval; 
REAL_LEBESGUE_MEASURABLE_INTERVAL];
        GEN_REWRITE_TAC LAND_CONV [GSYM ETA_AX] THEN REWRITE_TAC[] THEN
        ONCE_REWRITE_TAC[REAL_ARITH `inv x = &1 / x`] THEN
        MATCH_MP_TAC 
REAL_MEASURABLE_ON_DIV THEN
        SIMP_TAC[
REAL_CONTINUOUS_IMP_REAL_MEASURABLE_ON_CLOSED_SUBSET;
                 
REAL_CLOSED_REAL_INTERVAL; 
REAL_CONTINUOUS_ON_CONST;
                 
REAL_CONTINUOUS_ON_ID; 
SING_GSPEC; 
REAL_NEGLIGIBLE_SING;
                 
REAL_CLOSED_UNIV]];
      REWRITE_TAC[
real_bounded; 
FORALL_IN_IMAGE; 
IN_UNIV] THEN
      EXISTS_TAC `inv dd:real` THEN X_GEN_TAC `x:real` THEN
      REWRITE_TAC[
REAL_NOT_LT] THEN COND_CASES_TAC THEN
      ASM_SIMP_TAC[
REAL_LE_INV_EQ; 
REAL_LT_IMP_LE; 
REAL_ABS_NUM;
                   
REAL_ABS_INV] THEN
      MATCH_MP_TAC 
REAL_LE_INV2 THEN ASM_REAL_ARITH_TAC];
    ALL_TAC] THEN
  REWRITE_TAC[
REAL_ABS_NEG; 
REAL_MUL_RNEG; 
SIN_NEG; 
REAL_MUL_LNEG] THEN
  REWRITE_TAC[GSYM 
real_sub; GSYM 
REAL_SUB_LDISTRIB] THEN
  REWRITE_TAC[
real_div; 
REAL_INV_NEG; 
REAL_MUL_RNEG; 
REAL_NEG_NEG] THEN
  REWRITE_TAC[REAL_ARITH
   `(if p then &0 else a) - (if p then &0 else --b) =
    (if p then &0 else a + b)`] THEN
  REWRITE_TAC[GSYM 
REAL_ADD_RDISTRIB] THEN REWRITE_TAC[GSYM 
real_div] THEN
  REWRITE_TAC[MESON[
REAL_MUL_RZERO]
   `s * (if p then &0 else y) = (if ~p then s * y else &0)`] THEN
  ONCE_REWRITE_TAC[GSYM 
REAL_INTEGRAL_RESTRICT_UNIV] THEN
  REWRITE_TAC[MESON[]
   `(if p then if q then x else &0 else &0) =
    (if p /\ q then x else &0)`] THEN
  REWRITE_TAC[
IN_REAL_INTERVAL] THEN
  ASM_SIMP_TAC[REAL_ARITH
   `&0 < dd /\ dd <= pi
    ==> ((&0 <= x /\ x <= pi) /\ ~(abs x < dd) <=>
         dd <= x /\ x <= pi)`] THEN
  REWRITE_TAC[GSYM 
IN_REAL_INTERVAL; 
REAL_INTEGRAL_RESTRICT_UNIV] THEN
  REWRITE_TAC[REAL_ARITH `(x - l) + (y - l) = (x + y) - &2 * l`] THEN
  REWRITE_TAC[
REALLIM_SEQUENTIALLY] THEN
  DISCH_THEN(MP_TAC o SPEC `e / &2`) THEN ASM_REWRITE_TAC[
REAL_HALF] THEN
  MATCH_MP_TAC 
MONO_EXISTS THEN X_GEN_TAC `N:num` THEN DISCH_TAC THEN
  X_GEN_TAC `n:num` THEN DISCH_TAC THEN
  FIRST_X_ASSUM(MP_TAC o SPEC `n:num`) THEN
  ASM_REWRITE_TAC[] THEN MATCH_MP_TAC(REAL_ARITH
   `
real_integral(
real_interval[&0,dd]) f +
    
real_integral(
real_interval[dd,pi]) f =
    
real_integral(
real_interval[&0,pi]) f /\
    abs(
real_integral(
real_interval[&0,dd]) f) < e / &2
    ==> abs(
real_integral(
real_interval[dd,pi]) f - &0) < e / &2
        ==> abs(
real_integral(
real_interval[&0,pi]) f) < e`) THEN
  CONJ_TAC THENL
   [MATCH_MP_TAC 
REAL_INTEGRAL_COMBINE THEN
    REPEAT(CONJ_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC]) THEN
    MATCH_MP_TAC 
REAL_INTEGRABLE_COMBINE THEN EXISTS_TAC `dd:real` THEN
    ASM_SIMP_TAC[
ABSOLUTELY_REAL_INTEGRABLE_IMP_INTEGRABLE; 
REAL_LT_IMP_LE];
    FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH
     `abs x < e / &2 ==> abs y <= x ==> abs y < e / &2`)) THEN
    MATCH_MP_TAC 
REAL_INTEGRAL_ABS_BOUND_INTEGRAL THEN
    ASM_SIMP_TAC[
ABSOLUTELY_REAL_INTEGRABLE_IMP_INTEGRABLE] THEN
    CONJ_TAC THENL
     [MATCH_MP_TAC 
REAL_INTEGRABLE_SUBINTERVAL THEN
      MAP_EVERY EXISTS_TAC [`&0`; `d:real`] THEN
      ASM_REWRITE_TAC[
SUBSET_REAL_INTERVAL] THEN ASM_REAL_ARITH_TAC;
      X_GEN_TAC `x:real` THEN REWRITE_TAC[
IN_REAL_INTERVAL] THEN
      SIMP_TAC[
REAL_ABS_MUL; 
REAL_ABS_DIV; REAL_ARITH
        `&0 <= x ==> abs x = x`] THEN
      REPEAT STRIP_TAC THEN REWRITE_TAC[
real_div; REAL_MUL_ASSOC] THEN
      MATCH_MP_TAC 
REAL_LE_RMUL THEN ASM_REWRITE_TAC[
REAL_LE_INV_EQ] THEN
      ONCE_REWRITE_TAC[REAL_ARITH `x * y <= y <=> x * y <= &1 * y`] THEN
      MATCH_MP_TAC 
REAL_LE_RMUL THEN
      REWRITE_TAC[
REAL_ABS_POS; 
SIN_BOUND]]]);;
 
let REAL_INTEGRAL_SIN_OVER_X_BOUND = prove
 (`!a b c.
       &0 <= a /\ &0 < c
       ==> (\x. sin(c * x) / x) 
real_integrable_on real_interval[a,b] /\
           abs(
real_integral (
real_interval[a,b]) (\x. sin(c * x) / x)) <= &4`,
  let lemma0 = prove
   (`!a b. (\x. sin x) real_integrable_on (real_interval[a,b]) /\
           abs(real_integral (real_interval[a,b]) (\x. sin x)) <= &2`,
    REPEAT GEN_TAC THEN ASM_CASES_TAC `a <= b` THENL
     [MP_TAC(ISPECL [`\x. --(cos x)`; `\x. sin x`; `a:real`; `b:real`]
        REAL_FUNDAMENTAL_THEOREM_OF_CALCULUS) THEN
      REWRITE_TAC[] THEN ANTS_TAC THENL
       [ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC THEN REAL_DIFF_TAC THEN
        REAL_ARITH_TAC;
        REWRITE_TAC[HAS_REAL_INTEGRAL_INTEGRABLE_INTEGRAL] THEN STRIP_TAC THEN
        ASM_REWRITE_TAC[] THEN MATCH_MP_TAC(REAL_ARITH
         `abs x <= &1 /\ abs y <= &1 ==> abs(--y - --x) <= &2`) THEN
        REWRITE_TAC[COS_BOUND]];
      RULE_ASSUM_TAC(REWRITE_RULE[REAL_NOT_LE]) THEN
      ASM_SIMP_TAC[REAL_INTEGRABLE_ON_NULL; REAL_INTEGRAL_NULL; REAL_LT_IMP_LE;
                   REAL_ABS_NUM; REAL_POS]]) in
  let lemma1 = prove
   (`!a b. &0 < a
           ==> (\x. sin x / x) real_integrable_on real_interval[a,b] /\
               abs(real_integral (real_interval[a,b])
                                 (\x. sin x / x)) <= &4 / a`,
    REPEAT GEN_TAC THEN DISCH_TAC THEN ASM_CASES_TAC `a <= b` THENL
     [MP_TAC(ISPECL [`\x. sin x`; `\x:real. --(inv x)`; `a:real`; `b:real`]
              REAL_SECOND_MEAN_VALUE_THEOREM_FULL) THEN
      ASM_REWRITE_TAC[REAL_INTERVAL_EQ_EMPTY; REAL_NOT_LT; lemma0] THEN
      ANTS_TAC THENL
       [REWRITE_TAC[REAL_LE_NEG2; IN_REAL_INTERVAL] THEN REPEAT STRIP_TAC THEN
        MATCH_MP_TAC REAL_LE_INV2 THEN ASM_REAL_ARITH_TAC;
        DISCH_THEN(X_CHOOSE_THEN `c:real`
         (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
        DISCH_THEN(MP_TAC o MATCH_MP HAS_REAL_INTEGRAL_NEG) THEN
        REWRITE_TAC[REAL_ARITH `--(--(inv y) * x):real = x / y`] THEN
        REWRITE_TAC[HAS_REAL_INTEGRAL_INTEGRABLE_INTEGRAL] THEN STRIP_TAC THEN
        ASM_REWRITE_TAC[REAL_NEG_ADD; REAL_MUL_LNEG; REAL_NEG_NEG] THEN
        MATCH_MP_TAC(REAL_ARITH
         `inv b <= inv a /\ abs x <= inv a * &2 /\ abs y <= inv b * &2
          ==> abs(x + y) <= &4 / a`) THEN
        ASM_SIMP_TAC[REAL_LE_INV2; REAL_ABS_MUL] THEN CONJ_TAC THEN
        MATCH_MP_TAC REAL_LE_MUL2 THEN REWRITE_TAC[REAL_ABS_POS; lemma0] THEN
        ASM_REWRITE_TAC[real_abs; REAL_LE_REFL; REAL_LE_INV_EQ] THEN
        ASM_REAL_ARITH_TAC];
      RULE_ASSUM_TAC(REWRITE_RULE[REAL_NOT_LE]) THEN
      ASM_SIMP_TAC[REAL_INTEGRABLE_ON_NULL; REAL_INTEGRAL_NULL; REAL_LT_IMP_LE;
                   REAL_ABS_NUM; REAL_POS] THEN
      MATCH_MP_TAC REAL_LE_DIV THEN ASM_REAL_ARITH_TAC]) in
  let lemma2 = prove
   (`!x. &0 <= x ==> sin(x) <= x`,
    REPEAT STRIP_TAC THEN ASM_CASES_TAC `x <= &1` THENL
     [ALL_TAC; ASM_MESON_TAC[SIN_BOUNDS; REAL_LE_TOTAL; REAL_LE_TRANS]] THEN
    MP_TAC(ISPECL [`1`; `Cx x`] TAYLOR_CSIN) THEN
    CONV_TAC(TOP_DEPTH_CONV num_CONV) THEN
    REWRITE_TAC[VSUM_CLAUSES_NUMSEG; GSYM CX_SIN] THEN
    CONV_TAC NUM_REDUCE_CONV THEN
    REWRITE_TAC[GSYM CX_POW; GSYM CX_MUL; GSYM CX_DIV; GSYM CX_NEG;
                GSYM CX_ADD; GSYM CX_SUB] THEN
    REWRITE_TAC[COMPLEX_NORM_CX; IM_CX; REAL_ABS_0; REAL_EXP_0] THEN
    SIMP_TAC[REAL_POW_1; REAL_DIV_1; real_pow;
             REAL_MUL_LNEG; REAL_MUL_LID] THEN
    MATCH_MP_TAC(REAL_ARITH
     `e <= t ==> abs(sin x - (x + --t)) <= e ==> sin x <= x`) THEN
    ASM_REWRITE_TAC[real_abs; REAL_ARITH
     `x pow 5 / &24 <= x pow 3 / &6 <=>
      x pow 3 * x pow 2 <= x pow 3 * &2 pow 2`] THEN
    MATCH_MP_TAC REAL_LE_LMUL THEN ASM_SIMP_TAC[REAL_POW_LE] THEN
    REWRITE_TAC[GSYM REAL_LE_SQUARE_ABS] THEN ASM_REAL_ARITH_TAC) in
  let lemma3 = prove
   (`!x. &0 <= x /\ x <= &2 ==> abs(sin x / x) <= &1`,
    GEN_TAC THEN STRIP_TAC THEN ASM_CASES_TAC `x = &0` THENL
     [ASM_SIMP_TAC[real_div; REAL_MUL_RZERO; REAL_INV_0;
                   REAL_ABS_NUM; REAL_POS];
      ASM_SIMP_TAC[REAL_ABS_DIV; REAL_LE_LDIV_EQ; REAL_MUL_LID;
                   REAL_ARITH `&0 <= x /\ ~(x = &0) ==> &0 < abs x`] THEN
      MATCH_MP_TAC(REAL_ARITH `s <= x /\ &0 <= s ==> abs s <= abs x`) THEN
      ASM_SIMP_TAC[lemma2] THEN MATCH_MP_TAC SIN_POS_PI_LE THEN
      MP_TAC PI_APPROX_32 THEN ASM_REAL_ARITH_TAC]) in
  let lemma4 = prove
   (`!a b. &0 <= a /\ b <= &2
           ==> (\x. sin x / x) real_integrable_on real_interval[a,b] /\
               abs(real_integral (real_interval[a,b])
                                 (\x. sin x / x)) <= &2`,
    REPEAT GEN_TAC THEN STRIP_TAC THEN ASM_CASES_TAC `a <= b` THENL
     [MATCH_MP_TAC(TAUT `a /\ (a ==> b) ==> a /\ b`) THEN CONJ_TAC THENL
       [MATCH_MP_TAC REAL_MEASURABLE_BOUNDED_BY_INTEGRABLE_IMP_INTEGRABLE THEN
        EXISTS_TAC `(\x. &1):real->real` THEN
        REWRITE_TAC[REAL_INTEGRABLE_CONST] THEN CONJ_TAC THENL
         [MATCH_MP_TAC REAL_MEASURABLE_ON_DIV THEN REPEAT CONJ_TAC THENL
           [MATCH_MP_TAC INTEGRABLE_IMP_REAL_MEASURABLE THEN
            GEN_REWRITE_TAC LAND_CONV [GSYM ETA_AX] THEN REWRITE_TAC[lemma0];
            MATCH_MP_TAC CONTINUOUS_IMP_REAL_MEASURABLE_ON THEN
            REWRITE_TAC[REAL_CONTINUOUS_ON_ID];
            REWRITE_TAC[SING_GSPEC; REAL_NEGLIGIBLE_SING]];
          REWRITE_TAC[IN_REAL_INTERVAL] THEN REPEAT STRIP_TAC THEN
          MATCH_MP_TAC lemma3 THEN ASM_REAL_ARITH_TAC];
        DISCH_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THEN
        EXISTS_TAC `real_integral (real_interval [a,b]) (\x. &1)` THEN
        CONJ_TAC THENL
         [MATCH_MP_TAC REAL_INTEGRAL_ABS_BOUND_INTEGRAL THEN
          ASM_REWRITE_TAC[REAL_INTEGRABLE_CONST] THEN
          REWRITE_TAC[IN_REAL_INTERVAL] THEN REPEAT STRIP_TAC THEN
          MATCH_MP_TAC lemma3 THEN ASM_REAL_ARITH_TAC;
          ASM_SIMP_TAC[REAL_INTEGRAL_CONST] THEN ASM_REAL_ARITH_TAC]];
      RULE_ASSUM_TAC(REWRITE_RULE[REAL_NOT_LE]) THEN
      ASM_SIMP_TAC[REAL_INTEGRABLE_ON_NULL; REAL_INTEGRAL_NULL; REAL_LT_IMP_LE;
                   REAL_ABS_NUM; REAL_POS]]) in
  let lemma5 = prove
   (`!a b. &0 <= a
           ==> (\x. sin x / x) real_integrable_on real_interval[a,b] /\
               abs(real_integral (real_interval[a,b]) (\x. sin x / x)) <= &4`,
    REPEAT GEN_TAC THEN DISCH_TAC THEN
    ASM_CASES_TAC `b <= &2` THENL
     [ASM_MESON_TAC[lemma4; REAL_ARITH `x <= &2 ==> x <= &4`]; ALL_TAC] THEN
    ASM_CASES_TAC `&2 <= a` THENL
     [MP_TAC(SPECL [`a:real`; `b:real`] lemma1) THEN
      ANTS_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
      MATCH_MP_TAC MONO_AND THEN REWRITE_TAC[] THEN
      MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ_ALT] REAL_LE_TRANS) THEN
      ASM_SIMP_TAC[REAL_LE_LDIV_EQ; REAL_ARITH `&2 <= a ==> &0 < a`] THEN
      ASM_REAL_ARITH_TAC;
      ALL_TAC] THEN
    RULE_ASSUM_TAC(REWRITE_RULE[REAL_NOT_LE]) THEN
    MP_TAC(ISPECL [`\x. sin x / x`; `a:real`; `b:real`; `&2`]
          REAL_INTEGRABLE_COMBINE) THEN
    ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN ANTS_TAC THENL
     [CONJ_TAC THENL
       [ASM_MESON_TAC[lemma4; REAL_LE_REFL];
        ASM_MESON_TAC[lemma1; REAL_ARITH `&0 < &2`]];
      DISCH_TAC] THEN
    MP_TAC(ISPECL [`\x. sin x / x`; `a:real`; `b:real`; `&2`]
          REAL_INTEGRAL_COMBINE) THEN
    ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN DISCH_THEN(SUBST1_TAC o SYM) THEN
    MATCH_MP_TAC(REAL_ARITH
     `abs(x) <= &2 /\ abs(y) <= &2 ==> abs(x + y) <= &4`) THEN
    CONJ_TAC THENL
     [ASM_MESON_TAC[lemma4; REAL_LE_REFL];
      GEN_REWRITE_TAC RAND_CONV [REAL_ARITH `&2 = &4 / &2`] THEN
      ASM_MESON_TAC[lemma1; REAL_ARITH `&0 < &2`]]) in
  REPEAT GEN_TAC THEN STRIP_TAC THEN ASM_CASES_TAC `a <= b` THENL
   [MP_TAC(ISPECL [`c * a:real`; `c * b:real`] lemma5) THEN
    ASM_SIMP_TAC[REAL_LE_MUL; REAL_LT_IMP_LE] THEN
    DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
    GEN_REWRITE_TAC LAND_CONV [HAS_REAL_INTEGRAL_INTEGRAL] THEN
    DISCH_THEN(MP_TAC o SPEC `c:real` o MATCH_MP (REWRITE_RULE[IMP_CONJ]
     HAS_REAL_INTEGRAL_STRETCH)) THEN
    ASM_SIMP_TAC[REAL_LT_IMP_NZ; REAL_ADD_RID; REAL_SUB_RZERO] THEN
    DISCH_THEN(MP_TAC o SPEC `c:real` o MATCH_MP HAS_REAL_INTEGRAL_LMUL) THEN
    ASM_SIMP_TAC[IMAGE_STRETCH_REAL_INTERVAL; REAL_LE_INV_EQ; REAL_LT_IMP_LE;
      REAL_FIELD `&0 < c ==> inv c * c * a = a`; REAL_INV_MUL; real_div;
      REAL_FIELD `&0 < c ==> c * s * inv c * inv x = s * inv x`;
      REAL_FIELD `&0 < c ==> c * inv c * i = i /\ abs c = c`] THEN
    REWRITE_TAC[GSYM real_div; REAL_INTERVAL_EQ_EMPTY] THEN
    ASM_SIMP_TAC[GSYM REAL_NOT_LE; REAL_LE_LMUL_EQ] THEN
    REWRITE_TAC[HAS_REAL_INTEGRAL_INTEGRABLE_INTEGRAL] THEN
    STRIP_TAC THEN ASM_REWRITE_TAC[];
    RULE_ASSUM_TAC(REWRITE_RULE[REAL_NOT_LE]) THEN
    ASM_SIMP_TAC[REAL_INTEGRABLE_ON_NULL; REAL_INTEGRAL_NULL; REAL_LT_IMP_LE;
                 REAL_ABS_NUM; REAL_POS]]);;  
let FOURIER_JORDAN_BOUNDED_VARIATION = prove
 (`!f x d.
        f 
absolutely_real_integrable_on real_interval[--pi,pi] /\
        (!x. f(x + &2 * pi) = f x) /\
        &0 < d /\
        f 
has_bounded_real_variation_on real_interval[x - d,x + d]
        ==> ((\n. sum (0..n)
                      (\k. 
fourier_coefficient f k * 
trigonometric_set k x))
             ---> ((reallim (atreal x within {l | l <= x}) f +
                    reallim (atreal x within {r | r >= x}) f) / &2))
            sequentially`,
  let lemma = prove
   (`!f l d. &0 < d
             ==> ((f ---> l) (atreal (&0) within real_interval[&0,d]) <=>
                  (f ---> l) (atreal (&0) within {x | &0 <= x}))`,
    REPEAT STRIP_TAC THEN MATCH_MP_TAC REALLIM_TRANSFORM_WITHINREAL_SET THEN
    REWRITE_TAC[EVENTUALLY_ATREAL] THEN EXISTS_TAC `d:real` THEN
    ASM_REWRITE_TAC[IN_ELIM_THM; IN_REAL_INTERVAL] THEN REAL_ARITH_TAC) in
  MAP_EVERY X_GEN_TAC [`f:real->real`; `t:real`; `d0:real`] THEN
  STRIP_TAC THEN
  ABBREV_TAC `s = (reallim (atreal t within {l | l <= t}) f +
                   reallim (atreal t within {r | r >= t}) f) / &2` THEN
  MP_TAC(SPECL [`f:real->real`; `t:real`; `s:real`; `min d0 pi`]
        FOURIER_SUM_LIMIT_SINE_PART) THEN
  ASM_REWRITE_TAC[REAL_LT_MIN; PI_POS; REAL_ARITH `min d0 pi <= pi`] THEN
  DISCH_THEN SUBST1_TAC THEN
  ABBREV_TAC `h = \u. ((f:real->real)(t + u) + f(t - u)) - &2 * s` THEN
  FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [FUN_EQ_THM]) THEN
  SIMP_TAC[] THEN DISCH_THEN(K ALL_TAC) THEN ABBREV_TAC `d = min d0 pi` THEN
  SUBGOAL_THEN `&0 < d` ASSUME_TAC THENL
   [MP_TAC PI_POS THEN ASM_REAL_ARITH_TAC; ALL_TAC] THEN
  SUBGOAL_THEN
   `h has_bounded_real_variation_on real_interval[&0,d]`
  ASSUME_TAC THENL
   [FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I
     [HAS_BOUNDED_REAL_VARIATION_DARBOUX]) THEN
    EXPAND_TAC "h" THEN REWRITE_TAC[HAS_BOUNDED_REAL_VARIATION_DARBOUX] THEN
    REWRITE_TAC[LEFT_IMP_EXISTS_THM; IN_REAL_INTERVAL] THEN
    MAP_EVERY X_GEN_TAC [`f1:real->real`; `f2:real->real`] THEN STRIP_TAC THEN
    EXISTS_TAC `\x. ((f1:real->real)(t + x) - f2(t - x)) - s` THEN
    EXISTS_TAC `\x. ((f2:real->real)(t + x) - f1(t - x)) + s` THEN
    ASM_REWRITE_TAC[REAL_ARITH `x - s <= y - s <=> x <= y`; REAL_LE_RADD] THEN
    REWRITE_TAC[CONJ_ASSOC] THEN CONJ_TAC THENL [ALL_TAC; REAL_ARITH_TAC] THEN
    REPEAT STRIP_TAC THEN MATCH_MP_TAC(REAL_ARITH
     `a <= a' /\ b' <= b ==> a - b <= a' - b'`) THEN
    CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REAL_ARITH_TAC;
    ALL_TAC] THEN
  SUBGOAL_THEN `(h ---> &0) (atreal(&0) within {x | &0 <= x})`
  ASSUME_TAC THENL
   [EXPAND_TAC "h" THEN EXPAND_TAC "s" THEN
    REWRITE_TAC[REAL_ARITH
     `(f' + f) - &2 * (l + l') / &2 = (f - l) + (f' - l')`] THEN
    MATCH_MP_TAC REALLIM_NULL_ADD THEN CONJ_TAC THENL
     [SUBGOAL_THEN
       `?l. (f ---> l) (atreal t within {l | l <= t})` MP_TAC
      THENL
       [MP_TAC(ISPECL [`f:real->real`; `t - d0:real`; `t + d0:real`; `t:real`]
         HAS_BOUNDED_REAL_VARIATION_LEFT_LIMIT) THEN
        ASM_REWRITE_TAC[IN_REAL_INTERVAL] THEN
        ANTS_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
        MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `l:real` THEN
        REWRITE_TAC[REALLIM_WITHINREAL] THEN
        MATCH_MP_TAC MONO_FORALL THEN X_GEN_TAC `e:real` THEN
        ASM_CASES_TAC `&0 < e` THEN
        ASM_REWRITE_TAC[IN_REAL_INTERVAL; IN_ELIM_THM] THEN
        DISCH_THEN(X_CHOOSE_THEN `d1:real` (fun th ->
          EXISTS_TAC `min d0 d1` THEN
          CONJUNCTS_THEN2 ASSUME_TAC MP_TAC th)) THEN
        ASM_REWRITE_TAC[REAL_LT_MIN] THEN
        MATCH_MP_TAC MONO_FORALL THEN ASM_REAL_ARITH_TAC;
        DISCH_THEN(MP_TAC o SELECT_RULE) THEN
        REWRITE_TAC[GSYM reallim] THEN
        REWRITE_TAC[REALLIM_WITHINREAL] THEN
        MATCH_MP_TAC MONO_FORALL THEN X_GEN_TAC `e:real` THEN
        ASM_CASES_TAC `&0 < e` THEN ASM_REWRITE_TAC[IN_ELIM_THM] THEN
        MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `d1:real` THEN
        DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
        ASM_REWRITE_TAC[] THEN DISCH_THEN(fun th ->
         X_GEN_TAC `x:real` THEN MP_TAC(SPEC `t - x:real` th)) THEN
        MATCH_MP_TAC MONO_IMP THEN REWRITE_TAC[REAL_SUB_RZERO] THEN
        REAL_ARITH_TAC];
      SUBGOAL_THEN
       `?l. (f ---> l) (atreal t within {r | r >= t})` MP_TAC
      THENL
       [MP_TAC(ISPECL [`f:real->real`; `t - d0:real`; `t + d0:real`; `t:real`]
         HAS_BOUNDED_REAL_VARIATION_RIGHT_LIMIT) THEN
        ASM_REWRITE_TAC[IN_REAL_INTERVAL] THEN
        ANTS_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
        MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `l:real` THEN
        REWRITE_TAC[REALLIM_WITHINREAL] THEN
        MATCH_MP_TAC MONO_FORALL THEN X_GEN_TAC `e:real` THEN
        ASM_CASES_TAC `&0 < e` THEN
        ASM_REWRITE_TAC[IN_REAL_INTERVAL; IN_ELIM_THM] THEN
        DISCH_THEN(X_CHOOSE_THEN `d1:real` (fun th ->
          EXISTS_TAC `min d0 d1` THEN
          CONJUNCTS_THEN2 ASSUME_TAC MP_TAC th)) THEN
        ASM_REWRITE_TAC[REAL_LT_MIN] THEN
        MATCH_MP_TAC MONO_FORALL THEN ASM_REAL_ARITH_TAC;
        DISCH_THEN(MP_TAC o SELECT_RULE) THEN
        REWRITE_TAC[GSYM reallim] THEN
        REWRITE_TAC[REALLIM_WITHINREAL] THEN
        MATCH_MP_TAC MONO_FORALL THEN X_GEN_TAC `e:real` THEN
        ASM_CASES_TAC `&0 < e` THEN ASM_REWRITE_TAC[IN_ELIM_THM] THEN
        MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `d1:real` THEN
        DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
        ASM_REWRITE_TAC[] THEN DISCH_THEN(fun th ->
         X_GEN_TAC `x:real` THEN MP_TAC(SPEC `t + x:real` th)) THEN
        MATCH_MP_TAC MONO_IMP THEN REWRITE_TAC[REAL_SUB_RZERO] THEN
        REAL_ARITH_TAC]];
    ALL_TAC] THEN
  REWRITE_TAC[REALLIM_SEQUENTIALLY] THEN X_GEN_TAC `e:real` THEN DISCH_TAC THEN
  SUBGOAL_THEN
   `?k. &0 < k /\ k < d /\
        !n. (\x. sin ((&n + &1 / &2) * x) * h x / x)
            real_integrable_on real_interval[&0,k] /\
            abs(real_integral (real_interval[&0,k])
                              (\x. sin ((&n + &1 / &2) * x) * h x / x))
              <= e / &2`
  STRIP_ASSUME_TAC THENL
   [SUBGOAL_THEN
     `?h1 h2.
         (!x y. x IN real_interval[&0,d] /\ y IN real_interval[&0,d] /\ x <= y
                ==> h1 x <= h1 y) /\
         (!x y. x IN real_interval[&0,d] /\ y IN real_interval[&0,d] /\ x <= y
                ==> h2 x <= h2 y) /\
         (h1 ---> &0) (atreal (&0) within {x | &0 <= x}) /\
         (h2 ---> &0) (atreal (&0) within {x | &0 <= x}) /\
         (!x. h x = h1 x - h2 x)`
    STRIP_ASSUME_TAC THENL
     [MP_TAC(ISPECL [`h:real->real`; `&0`; `d:real`]
          HAS_BOUNDED_REAL_VARIATION_DARBOUX) THEN
      ASM_REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
      MAP_EVERY X_GEN_TAC [`h1:real->real`; `h2:real->real`] THEN
      STRIP_TAC THEN
      MP_TAC(ISPECL [`h1:real->real`; `&0`; `d:real`; `&0`]
           INCREASING_RIGHT_LIMIT) THEN
      ASM_REWRITE_TAC[ENDS_IN_REAL_INTERVAL; REAL_INTERVAL_EQ_EMPTY] THEN
      ASM_SIMP_TAC[REAL_NOT_LT; REAL_LT_IMP_LE] THEN
      DISCH_THEN(X_CHOOSE_TAC `l:real`) THEN
      MP_TAC(ISPECL [`h2:real->real`; `&0`; `d:real`; `&0`]
           INCREASING_RIGHT_LIMIT) THEN
      ASM_REWRITE_TAC[ENDS_IN_REAL_INTERVAL; REAL_INTERVAL_EQ_EMPTY] THEN
      ASM_SIMP_TAC[REAL_NOT_LT; REAL_LT_IMP_LE] THEN
      DISCH_THEN(X_CHOOSE_TAC `l':real`) THEN
      SUBGOAL_THEN `l':real = l` SUBST_ALL_TAC THENL
       [CONV_TAC SYM_CONV THEN ONCE_REWRITE_TAC[GSYM REAL_SUB_0] THEN
        MATCH_MP_TAC(ISPEC `atreal (&0) within {x | &0 <= x}`
          REALLIM_UNIQUE) THEN
        EXISTS_TAC `h:real->real` THEN ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
         [W(MP_TAC o PART_MATCH (lhs o rand) TRIVIAL_LIMIT_WITHIN_REALINTERVAL o
            rand o snd) THEN
          REWRITE_TAC[is_realinterval; IN_ELIM_THM] THEN
          ANTS_TAC THENL [REAL_ARITH_TAC; DISCH_THEN SUBST1_TAC] THEN
          REWRITE_TAC[EXTENSION; NOT_FORALL_THM; IN_ELIM_THM; IN_SING] THEN
          EXISTS_TAC `&1` THEN REAL_ARITH_TAC;
          GEN_REWRITE_TAC (RATOR_CONV o LAND_CONV) [GSYM ETA_AX] THEN
          ASM_REWRITE_TAC[] THEN MATCH_MP_TAC REALLIM_SUB THEN
          MAP_EVERY UNDISCH_TAC
           [`(h1 ---> l) (atreal(&0) within real_interval[&0,d])`;
            `(h2 ---> l') (atreal(&0) within real_interval[&0,d])`] THEN
          ASM_SIMP_TAC[lemma]];
        EXISTS_TAC `\x. (h1:real->real)(x) - l` THEN
        EXISTS_TAC `\x. (h2:real->real)(x) - l` THEN
        ASM_REWRITE_TAC[REAL_ARITH `x - l <= y - l <=> x <= y`] THEN
        ASM_REWRITE_TAC[GSYM REALLIM_NULL] THEN
        MAP_EVERY UNDISCH_TAC
         [`(h1 ---> l) (atreal(&0) within real_interval[&0,d])`;
          `(h2 ---> l) (atreal(&0) within real_interval[&0,d])`] THEN
        ASM_SIMP_TAC[lemma] THEN REPEAT DISCH_TAC THEN REAL_ARITH_TAC];
      ALL_TAC] THEN
    SUBGOAL_THEN
     `?k. &0 < k /\ k < d /\ abs(h1 k) < e / &16 /\ abs(h2 k) < e / &16`
    MP_TAC THENL
     [UNDISCH_TAC `(h2 ---> &0) (atreal (&0) within {x | &0 <= x})` THEN
      UNDISCH_TAC `(h1 ---> &0) (atreal (&0) within {x | &0 <= x})` THEN
      REWRITE_TAC[REALLIM_WITHINREAL; IN_ELIM_THM; REAL_SUB_RZERO] THEN
      DISCH_THEN(MP_TAC o SPEC `e / &16`) THEN ANTS_TAC THENL
       [ASM_REAL_ARITH_TAC;
        DISCH_THEN(X_CHOOSE_THEN `k1:real` STRIP_ASSUME_TAC)] THEN
      DISCH_THEN(MP_TAC o SPEC `e / &16`) THEN ANTS_TAC THENL
       [ASM_REAL_ARITH_TAC;
        DISCH_THEN(X_CHOOSE_THEN `k2:real` STRIP_ASSUME_TAC)] THEN
      EXISTS_TAC `min d (min k1 k2) / &2` THEN
      REPLICATE_TAC 2 (CONJ_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC]) THEN
      CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REAL_ARITH_TAC;
      ALL_TAC] THEN
    MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `k:real` THEN
    STRIP_TAC THEN ASM_REWRITE_TAC[] THEN X_GEN_TAC `n:num` THEN
    MP_TAC(ISPECL [`\x. sin((&n + &1 / &2) * x) / x`; `h1:real->real`;
                     `&0`; `k:real`; `&0`; `(h1:real->real) k`]
      REAL_SECOND_MEAN_VALUE_THEOREM_GEN_FULL) THEN
    ASM_SIMP_TAC[REAL_INTERVAL_EQ_EMPTY; REAL_NOT_LT; REAL_LT_IMP_LE] THEN
    ASM_SIMP_TAC[REAL_INTEGRAL_SIN_OVER_X_BOUND; REAL_LE_REFL; REAL_ADD_LID;
                 REAL_ARITH `&0 < &n + &1 / &2`; REAL_MUL_LZERO] THEN
    ANTS_TAC THENL
     [CONJ_TAC THENL
       [X_GEN_TAC `x:real` THEN REWRITE_TAC[IN_REAL_INTERVAL] THEN
        REPEAT STRIP_TAC THENL
         [REWRITE_TAC[GSYM REAL_NOT_LT] THEN DISCH_TAC THEN
          UNDISCH_TAC `(h1 ---> &0) (atreal (&0) within {x | &0 <= x})` THEN
          REWRITE_TAC[REALLIM_WITHINREAL; IN_ELIM_THM; REAL_SUB_RZERO] THEN
          DISCH_THEN(MP_TAC o SPEC `--((h1:real->real) x)`) THEN
          REWRITE_TAC[NOT_IMP] THEN CONJ_TAC THENL
           [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
          DISCH_THEN(X_CHOOSE_THEN `dd:real` MP_TAC) THEN
          DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC
           (MP_TAC o SPEC `min d (min x dd) / &2`)) THEN
          REWRITE_TAC[NOT_IMP] THEN CONJ_TAC THENL
           [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
          FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH
           `h < &0 ==> h' <= h ==> ~(abs h' < --h)`));
          ALL_TAC] THEN
        FIRST_X_ASSUM MATCH_MP_TAC THEN
        REWRITE_TAC[IN_REAL_INTERVAL] THEN ASM_REAL_ARITH_TAC;
        REWRITE_TAC[IN_REAL_INTERVAL] THEN REPEAT STRIP_TAC THEN
        FIRST_X_ASSUM MATCH_MP_TAC THEN
        REWRITE_TAC[IN_REAL_INTERVAL] THEN ASM_REAL_ARITH_TAC];
      GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV)
       [REAL_ARITH `h * s / x:real = s * h / x`] THEN
      REWRITE_TAC[HAS_REAL_INTEGRAL_INTEGRABLE_INTEGRAL] THEN
      DISCH_THEN(X_CHOOSE_THEN `c1:real` STRIP_ASSUME_TAC)] THEN
    MP_TAC(ISPECL [`\x. sin((&n + &1 / &2) * x) / x`; `h2:real->real`;
                     `&0`; `k:real`; `&0`; `(h2:real->real) k`]
      REAL_SECOND_MEAN_VALUE_THEOREM_GEN_FULL) THEN
    ASM_SIMP_TAC[REAL_INTERVAL_EQ_EMPTY; REAL_NOT_LT; REAL_LT_IMP_LE] THEN
    ASM_SIMP_TAC[REAL_INTEGRAL_SIN_OVER_X_BOUND; REAL_LE_REFL; REAL_ADD_LID;
                 REAL_ARITH `&0 < &n + &1 / &2`; REAL_MUL_LZERO] THEN
    ANTS_TAC THENL
     [CONJ_TAC THENL
       [X_GEN_TAC `x:real` THEN REWRITE_TAC[IN_REAL_INTERVAL] THEN
        REPEAT STRIP_TAC THENL
         [REWRITE_TAC[GSYM REAL_NOT_LT] THEN DISCH_TAC THEN
          UNDISCH_TAC `(h2 ---> &0) (atreal (&0) within {x | &0 <= x})` THEN
          REWRITE_TAC[REALLIM_WITHINREAL; IN_ELIM_THM; REAL_SUB_RZERO] THEN
          DISCH_THEN(MP_TAC o SPEC `--((h2:real->real) x)`) THEN
          REWRITE_TAC[NOT_IMP] THEN CONJ_TAC THENL
           [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
          DISCH_THEN(X_CHOOSE_THEN `dd:real` MP_TAC) THEN
          DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC
           (MP_TAC o SPEC `min d (min x dd) / &2`)) THEN
          REWRITE_TAC[NOT_IMP] THEN CONJ_TAC THENL
           [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
          FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH
           `h < &0 ==> h' <= h ==> ~(abs h' < --h)`));
          ALL_TAC] THEN
        FIRST_X_ASSUM MATCH_MP_TAC THEN
        REWRITE_TAC[IN_REAL_INTERVAL] THEN ASM_REAL_ARITH_TAC;
        REWRITE_TAC[IN_REAL_INTERVAL] THEN REPEAT STRIP_TAC THEN
        FIRST_X_ASSUM MATCH_MP_TAC THEN
        REWRITE_TAC[IN_REAL_INTERVAL] THEN ASM_REAL_ARITH_TAC];
      GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV)
       [REAL_ARITH `h * s / x:real = s * h / x`] THEN
      REWRITE_TAC[HAS_REAL_INTEGRAL_INTEGRABLE_INTEGRAL] THEN
      DISCH_THEN(X_CHOOSE_THEN `c2:real` STRIP_ASSUME_TAC)] THEN
    REWRITE_TAC[REAL_ARITH
     `s * (h - h') / x:real = s * h / x - s * h' / x`] THEN
    ASM_SIMP_TAC[REAL_INTEGRABLE_SUB; REAL_INTEGRAL_SUB] THEN
    MATCH_MP_TAC(REAL_ARITH
     `abs(x) <= e / &16 * &4 /\ abs(y) <= e / &16 * &4
      ==> abs(x - y) <= e / &2`) THEN
    REWRITE_TAC[REAL_ABS_MUL] THEN CONJ_TAC THEN
    MATCH_MP_TAC REAL_LE_MUL2 THEN REWRITE_TAC[REAL_ABS_POS] THEN
    RULE_ASSUM_TAC(REWRITE_RULE[IN_REAL_INTERVAL]) THEN
    ASM_SIMP_TAC[REAL_INTEGRAL_SIN_OVER_X_BOUND; REAL_LT_IMP_LE;
                 REAL_ARITH `&0 < &n + &1 / &2`];
    ALL_TAC] THEN
  MP_TAC(ISPECL [`f:real->real`; `--pi`; `pi`; `t:real`]
      ABSOLUTELY_REAL_INTEGRABLE_PERIODIC_OFFSET) THEN
  ASM_REWRITE_TAC[REAL_ARITH `pi - --pi = &2 * pi`] THEN
  GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [REAL_ADD_SYM] THEN
  DISCH_THEN(fun th -> ASSUME_TAC th THEN MP_TAC th) THEN
  GEN_REWRITE_TAC LAND_CONV [absolutely_real_integrable_on] THEN
  GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV)
   [GSYM REAL_INTEGRABLE_REFLECT] THEN
  REWRITE_TAC[GSYM absolutely_real_integrable_on; GSYM real_sub] THEN
  REWRITE_TAC[REAL_NEG_NEG] THEN DISCH_TAC THEN
  SUBGOAL_THEN
   `(\x. h x / x) absolutely_real_integrable_on real_interval[k,d]`
  ASSUME_TAC THENL
   [REWRITE_TAC[ONCE_REWRITE_RULE[REAL_MUL_SYM] real_div] THEN
    MATCH_MP_TAC ABSOLUTELY_REAL_INTEGRABLE_BOUNDED_MEASURABLE_PRODUCT THEN
    REPEAT CONJ_TAC THENL
     [GEN_REWRITE_TAC LAND_CONV [GSYM ETA_AX] THEN
      MATCH_MP_TAC REAL_CONTINUOUS_IMP_REAL_MEASURABLE_ON_CLOSED_SUBSET THEN
      REWRITE_TAC[REAL_CLOSED_REAL_INTERVAL] THEN
      REWRITE_TAC[REAL_CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN] THEN
      REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_CONTINUOUS_INV_WITHINREAL THEN
      REWRITE_TAC[REAL_CONTINUOUS_WITHIN_ID] THEN
      RULE_ASSUM_TAC(REWRITE_RULE[IN_REAL_INTERVAL]) THEN ASM_REAL_ARITH_TAC;
      REWRITE_TAC[real_bounded; FORALL_IN_IMAGE; IN_REAL_INTERVAL] THEN
      EXISTS_TAC `inv k:real` THEN REPEAT STRIP_TAC THEN
      REWRITE_TAC[REAL_ABS_INV] THEN MATCH_MP_TAC REAL_LE_INV2 THEN
      ASM_REAL_ARITH_TAC;
      EXPAND_TAC "h" THEN MATCH_MP_TAC ABSOLUTELY_REAL_INTEGRABLE_SUB THEN
      REWRITE_TAC[ABSOLUTELY_REAL_INTEGRABLE_CONST] THEN
      MATCH_MP_TAC ABSOLUTELY_REAL_INTEGRABLE_ON_SUBINTERVAL THEN
      EXISTS_TAC `real_interval[--pi,pi]` THEN
      ASM_SIMP_TAC[ABSOLUTELY_REAL_INTEGRABLE_ADD] THEN
      REWRITE_TAC[SUBSET_REAL_INTERVAL] THEN ASM_REAL_ARITH_TAC];
    ALL_TAC] THEN
  SUBGOAL_THEN
   `!n. (\x. sin((&n + &1 / &2) * x) * h x / x) absolutely_real_integrable_on
        real_interval[k,d]`
  ASSUME_TAC THENL
   [GEN_TAC THEN
    MATCH_MP_TAC ABSOLUTELY_REAL_INTEGRABLE_BOUNDED_MEASURABLE_PRODUCT THEN
    ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
     [MATCH_MP_TAC REAL_CONTINUOUS_IMP_REAL_MEASURABLE_ON_CLOSED_SUBSET THEN
      REWRITE_TAC[REAL_CLOSED_UNIV; REAL_CLOSED_REAL_INTERVAL] THEN
      REWRITE_TAC[REAL_CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN] THEN
      REPEAT STRIP_TAC THEN
      MATCH_MP_TAC REAL_CONTINUOUS_ATREAL_WITHINREAL THEN
      MATCH_MP_TAC REAL_DIFFERENTIABLE_IMP_CONTINUOUS_ATREAL THEN
      REAL_DIFFERENTIABLE_TAC;
      REWRITE_TAC[real_bounded; FORALL_IN_IMAGE] THEN
      EXISTS_TAC `&1` THEN REWRITE_TAC[SIN_BOUND]];
    ALL_TAC] THEN
  MP_TAC(ISPEC `\x. if k <= x /\ x <= d then h x / x else &0`
        RIEMANN_LEBESGUE_SIN_HALF) THEN
  REWRITE_TAC[absolutely_real_integrable_on] THEN
  REWRITE_TAC[MESON[REAL_ABS_NUM]
   `abs(if p then x else &0) = if p then abs x else &0`] THEN
  ONCE_REWRITE_TAC[GSYM REAL_INTEGRAL_RESTRICT_UNIV; GSYM
                   REAL_INTEGRABLE_RESTRICT_UNIV] THEN
  REWRITE_TAC[MESON[REAL_MUL_RZERO]
   `(if P then s * (if Q then a else &0) else &0) =
    (if P /\ Q then s * a else &0)`] THEN
  REWRITE_TAC[IN_REAL_INTERVAL] THEN
  REWRITE_TAC[MESON[] `(if P then if Q then x else &0 else &0) =
                       (if P /\ Q then x else &0)`] THEN
  SUBGOAL_THEN `!x. (--pi <= x /\ x <= pi) /\ k <= x /\ x <= d <=>
                    k <= x /\ x <= d`
   (fun th -> REWRITE_TAC[th])
  THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
  REWRITE_TAC[GSYM IN_REAL_INTERVAL; REAL_INTEGRAL_RESTRICT_UNIV;
              REAL_INTEGRABLE_RESTRICT_UNIV] THEN
  ASM_REWRITE_TAC[GSYM absolutely_real_integrable_on] THEN
  REWRITE_TAC[REALLIM_SEQUENTIALLY] THEN
  DISCH_THEN(MP_TAC o SPEC `e / &2`) THEN ASM_REWRITE_TAC[REAL_HALF] THEN
  MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `N:num` THEN
  MATCH_MP_TAC MONO_FORALL THEN X_GEN_TAC `n:num` THEN
  MATCH_MP_TAC MONO_IMP THEN REWRITE_TAC[] THEN
  FIRST_X_ASSUM(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC o SPEC `n:num`) THEN
  MATCH_MP_TAC(REAL_ARITH
   `x + y = z ==> abs(x) <= e / &2 ==> abs(y) < e / &2 ==> abs(z) < e`) THEN
  REWRITE_TAC[REAL_SUB_RZERO] THEN MATCH_MP_TAC REAL_INTEGRAL_COMBINE THEN
  REPEAT(CONJ_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC]) THEN
  MATCH_MP_TAC REAL_INTEGRABLE_COMBINE THEN EXISTS_TAC `k:real` THEN
  ASM_SIMP_TAC[ABSOLUTELY_REAL_INTEGRABLE_IMP_INTEGRABLE] THEN
  ASM_REAL_ARITH_TAC);;