(* ========================================================================= *)
(* Some analytic concepts for R instead of R^1.                              *)
(*                                                                           *)
(*              (c) Copyright, John Harrison 1998-2008                       *)
(* ========================================================================= *)
needs "Library/binomial.ml";;
needs "Multivariate/measure.ml";;
needs "Multivariate/polytope.ml";;
needs "Multivariate/transcendentals.ml";;
(* ------------------------------------------------------------------------- *)
(* Open-ness and closedness of a set of reals.                               *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Compactness of a set of reals.                                            *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Limits of functions with real range.                                      *)
(* ------------------------------------------------------------------------- *)
parse_as_infix("--->",(12,"right"));;
let tendsto_real = new_definition
  `(f ---> l) net <=> !e. &0 < e ==> eventually (\x. abs(f(x) - l) < e) net`;;
let REALLIM_UNIQUE = prove
 (`!net f l l'.
         ~trivial_limit net /\ (f ---> l) net /\ (f ---> l') net ==> l = l'`,
 
let REALLIM_LMUL_EQ = prove
 (`!net f l c.
        ~(c = &0) ==> (((\x. c * f x) ---> c * l) net <=> (f ---> l) net)`,
  REPEAT STRIP_TAC THEN EQ_TAC THEN SIMP_TAC[
REALLIM_LMUL] THEN
  DISCH_THEN(MP_TAC o SPEC `inv c:real` o MATCH_MP 
REALLIM_LMUL) THEN
  ASM_SIMP_TAC[REAL_MUL_ASSOC; REAL_MUL_LINV; REAL_MUL_LID; ETA_AX]);;
 
let REALLIM_ADD = prove
 (`!net:(A)net f g l m.
    (f ---> l) net /\ (g ---> m) net ==> ((\x. f(x) + g(x)) ---> l + m) net`,
 
let REALLIM_SUB = prove
 (`!net:(A)net f g l m.
    (f ---> l) net /\ (g ---> m) net ==> ((\x. f(x) - g(x)) ---> l - m) net`,
 
let REALLIM_MUL = prove
 (`!net:(A)net f g l m.
    (f ---> l) net /\ (g ---> m) net ==> ((\x. f(x) * g(x)) ---> l * m) net`,
 
let REALLIM_INV = prove
 (`!net f l.
         (f ---> l) net /\ ~(l = &0) ==> ((\x. inv(f x)) ---> inv l) net`,
 
let REALLIM_DIV = prove
 (`!net:(A)net f g l m.
    (f ---> l) net /\ (g ---> m) net /\ ~(m = &0)
    ==> ((\x. f(x) / g(x)) ---> l / m) net`,
 
let REALLIM_ABS = prove
 (`!net f l. (f ---> l) net ==> ((\x. abs(f x)) ---> abs l) net`,
  REPEAT GEN_TAC THEN REWRITE_TAC[
tendsto_real] THEN
  MATCH_MP_TAC 
MONO_FORALL THEN X_GEN_TAC `e:real` THEN
  DISCH_THEN(fun th -> DISCH_TAC THEN MP_TAC th) THEN ASM_REWRITE_TAC[] THEN
  MATCH_MP_TAC(REWRITE_RULE[
IMP_CONJ] 
EVENTUALLY_MONO) THEN
  REWRITE_TAC[] THEN REAL_ARITH_TAC);;
 
let REALLIM_MAX = prove
 (`!net:(A)net f g l m.
    (f ---> l) net /\ (g ---> m) net
    ==> ((\x. max (f x) (g x)) ---> max l m) net`,
 
let REALLIM_MIN = prove
 (`!net:(A)net f g l m.
    (f ---> l) net /\ (g ---> m) net
    ==> ((\x. min (f x) (g x)) ---> min l m) net`,
 
let REALLIM_NULL_ADD = prove
 (`!net:(A)net f g.
    (f ---> &0) net /\ (g ---> &0) net ==> ((\x. f(x) + g(x)) ---> &0) net`,
  REPEAT GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP 
REALLIM_ADD) THEN
  REWRITE_TAC[REAL_ADD_LID]);;
 
let REALLIM_NULL_POW = prove
 (`!net f n. (f ---> &0) net /\ ~(n = 0) ==> ((\x. f x pow n) ---> &0) net`,
  REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2
   (MP_TAC o SPEC `n:num` o MATCH_MP 
REALLIM_POW) ASSUME_TAC) THEN
  ASM_REWRITE_TAC[
REAL_POW_ZERO]);;
 
let REALLIM_NULL_NEG = prove
 (`!net f. ((\x. --(f x)) ---> &0) net <=> (f ---> &0) net`,
  REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[REAL_ARITH `--x = --(&1) * x`] THEN
  MATCH_MP_TAC 
REALLIM_NULL_LMUL_EQ THEN CONV_TAC REAL_RAT_REDUCE_CONV);;
 
let REALLIM_TRANSFORM_STRADDLE = prove
 (`!f g h a.
        eventually (\n. f(n) <= g(n)) net /\ (f ---> a) net /\
        eventually (\n. g(n) <= h(n)) net /\ (h ---> a) net
        ==> (g ---> a) net`,
 
let REALLIM = prove
 (`(f ---> l) net <=>
        
trivial_limit net \/
        !e. &0 < e ==> ?y. (?x. netord(net) x y) /\
                           !x. netord(net) x y ==> abs(f(x) -l) < e`,
 
let REALLIM_WITHIN_LE = prove
 (`!f:real^N->real l a s.
        (f ---> l) (at a within s) <=>
           !e. &0 < e ==> ?d. &0 < d /\
                              !x. x 
IN s /\ &0 < dist(x,a) /\ dist(x,a) <= d
                                   ==> abs(f(x) - l) < e`,
 
let REALLIM_WITHIN = prove
 (`!f:real^N->real l a s.
      (f ---> l) (at a within s) <=>
        !e. &0 < e
            ==> ?d. &0 < d /\
                    !x. x 
IN s /\ &0 < dist(x,a) /\ dist(x,a) < d
                    ==> abs(f(x) - l) < e`,
 
let REALLIM_AT = prove
 (`!f l a:real^N.
      (f ---> l) (at a) <=>
              !e. &0 < e
                  ==> ?d. &0 < d /\ !x. &0 < dist(x,a) /\ dist(x,a) < d
                          ==> abs(f(x) - l) < e`,
 
let REALLIM_EVENTUALLY = prove
 (`!net f l. eventually (\x. f x = l) net ==> (f ---> l) net`,
  REWRITE_TAC[eventually; 
REALLIM] THEN
  MESON_TAC[REAL_ARITH `abs(x - x) = &0`]);;
 
let LIM_COMPONENTWISE = prove
 (`!net f:A->real^N.
        (f --> l) net <=>
        !i. 1 <= i /\ i <= dimindex(:N) ==> ((\x. (f x)$i) ---> l$i) net`,
 
let REALLIM_UBOUND = prove
 (`!(net:A net) f l b.
        (f ---> l) net /\
        ~trivial_limit net /\
        eventually (\x. f x <= b) net
        ==> l <= b`,
 
let REALLIM_LBOUND = prove
 (`!(net:A net) f l b.
        (f ---> l) net /\
        ~trivial_limit net /\
        eventually (\x. b <= f x) net
        ==> b <= l`,
 
let REALLIM_LE = prove
 (`!net f g l m.
           (f ---> l) net /\ (g ---> m) net /\
           ~trivial_limit net /\
           eventually (\x. f x <= g x) net
           ==> l <= m`,
 
let REALLIM_SUM = prove
 (`!net f:A->B->real l s.
        
FINITE s /\ (!i. i 
IN s ==> ((f i) ---> (l i)) net)
        ==> ((\x. sum s (\i. f i x)) ---> sum s l) net`,
 
let REAL_SUMS_FINITE_DIFF = prove
 (`!f t s l.
        t 
SUBSET s /\ 
FINITE t /\ (f 
real_sums l) s
        ==> (f 
real_sums (l - sum t f)) (s 
DIFF t)`,
  REPEAT GEN_TAC THEN
  REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
  FIRST_ASSUM(MP_TAC o ISPEC `f:num->real` o MATCH_MP 
REAL_SERIES_FINITE) THEN
  ONCE_REWRITE_TAC[GSYM 
REAL_SERIES_RESTRICT] THEN
  REWRITE_TAC[IMP_IMP] THEN ONCE_REWRITE_TAC[
CONJ_SYM] THEN
  DISCH_THEN(MP_TAC o MATCH_MP 
REAL_SERIES_SUB) 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 X_GEN_TAC `x:num` THEN REWRITE_TAC[
IN_DIFF] THEN
  FIRST_ASSUM(MP_TAC o SPEC `x:num` o GEN_REWRITE_RULE I [
SUBSET]) THEN
  MAP_EVERY ASM_CASES_TAC [`(x:num) 
IN s`; `(x:num) 
IN t`] THEN
  ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);;
 
let REAL_SERIES_CAUCHY_UNIFORM = prove
 (`!P:A->bool f k.
        (?l. !e. &0 < e
                 ==> ?N. !n x. N <= n /\ P x
                               ==> abs(sum(k 
INTER (0..n)) (f x) -
                                        l x) < e) <=>
        (!e. &0 < e ==> ?N. !m n x. N <= m /\ P x
                                    ==> abs(sum(k 
INTER (m..n)) (f x)) < e)`,
 
let ATREAL = prove
 (`!a x y.
        netord(atreal a) x y <=> &0 < abs(x - a) /\ abs(x - a) <= abs(y - a)`,
 
let TRIVIAL_LIMIT_ATREAL = prove
 (`!a. ~(
trivial_limit (atreal a))`,
  X_GEN_TAC `a:real` THEN SIMP_TAC[
trivial_limit; 
ATREAL; DE_MORGAN_THM] THEN
  CONJ_TAC THENL
   [DISCH_THEN(MP_TAC o SPECL [`&0`; `&1`]) THEN REAL_ARITH_TAC; ALL_TAC] THEN
  REWRITE_TAC[
NOT_EXISTS_THM] THEN
  MAP_EVERY X_GEN_TAC [`b:real`; `c:real`] THEN
  ASM_CASES_TAC `b:real = c` THEN ASM_REWRITE_TAC[] THEN
  REWRITE_TAC[GSYM DE_MORGAN_THM; GSYM 
NOT_EXISTS_THM] THEN
  SUBGOAL_THEN `~(b:real = a) \/ ~(c = a)` DISJ_CASES_TAC THENL
   [ASM_MESON_TAC[];
    EXISTS_TAC `(a + b) / &2` THEN ASM_REAL_ARITH_TAC;
    EXISTS_TAC `(a + c) / &2` THEN ASM_REAL_ARITH_TAC]);;
 
let EVENTUALLY_WITHINREAL_LE = prove
 (`!s a p.
     eventually p (atreal a within s) <=>
        ?d. &0 < d /\
            !x. x 
IN s /\ &0 < abs(x - a) /\ abs(x - a) <= d ==> p(x)`,
  REWRITE_TAC[eventually; 
ATREAL; 
WITHIN; 
trivial_limit] THEN
  REWRITE_TAC[MESON[
REAL_LT_01; 
REAL_LT_REFL] `~(!a b:real. a = b)`] THEN
  REPEAT GEN_TAC THEN EQ_TAC THENL
   [DISCH_THEN(DISJ_CASES_THEN(X_CHOOSE_THEN `b:real` MP_TAC)) THENL
     [DISCH_THEN(X_CHOOSE_THEN `c:real` STRIP_ASSUME_TAC) THEN
      FIRST_X_ASSUM(DISJ_CASES_TAC o MATCH_MP (REAL_ARITH
       `~(b = c) ==> &0 < abs(b - a) \/ &0 < abs(c - a)`)) THEN
      ASM_MESON_TAC[];
      MESON_TAC[
REAL_LTE_TRANS]];
    DISCH_THEN(X_CHOOSE_THEN `d:real` STRIP_ASSUME_TAC) THEN
    ASM_CASES_TAC `?x. x 
IN s /\ &0 < abs(x - a) /\ abs(x - a) <= d` THENL
     [DISJ2_TAC THEN FIRST_X_ASSUM(X_CHOOSE_TAC `b:real`) THEN
      EXISTS_TAC `b:real` THEN ASM_MESON_TAC[
REAL_LE_TRANS; 
REAL_LE_REFL];
      DISJ1_TAC THEN MAP_EVERY EXISTS_TAC [`a + d:real`; `a:real`] THEN
      ASM_SIMP_TAC[
REAL_ADD_SUB; 
REAL_EQ_ADD_LCANCEL_0; 
REAL_LT_IMP_NZ] THEN
      FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [
NOT_EXISTS_THM]) THEN
      MATCH_MP_TAC 
MONO_FORALL THEN X_GEN_TAC `x:real` THEN
      ASM_CASES_TAC `(x:real) 
IN s` THEN ASM_REWRITE_TAC[] THEN
      ASM_REAL_ARITH_TAC]]);;
 
let EVENTUALLY_ATREAL = prove
 (`!a p. eventually p (atreal a) <=>
         ?d. &0 < d /\ !x. &0 < abs(x - a) /\ abs(x - a) < d ==> p(x)`,
 
let LIM_WITHINREAL_LE = prove
 (`!f:real->real^N l a s.
        (f --> l) (atreal a within s) <=>
           !e. &0 < e ==> ?d. &0 < d /\
                              !x. x 
IN s /\ &0 < abs(x - a) /\ abs(x - a) <= d
                                   ==> dist(f(x),l) < e`,
 
let LIM_WITHINREAL = prove
 (`!f:real->real^N l a s.
      (f --> l) (atreal a within s) <=>
        !e. &0 < e
            ==> ?d. &0 < d /\
                    !x. x 
IN s /\ &0 < abs(x - a) /\ abs(x - a) < d
                    ==> dist(f(x),l) < e`,
 
let LIM_ATREAL = prove
 (`!f l:real^N a.
      (f --> l) (atreal a) <=>
              !e. &0 < e
                  ==> ?d. &0 < d /\ !x. &0 < abs(x - a) /\ abs(x - a) < d
                          ==> dist(f(x),l) < e`,
 
let REALLIM_WITHINREAL_LE = prove
 (`!f l a s.
        (f ---> l) (atreal a within s) <=>
           !e. &0 < e ==> ?d. &0 < d /\
                              !x. x 
IN s /\ &0 < abs(x - a) /\ abs(x - a) <= d
                                   ==> abs(f(x) - l) < e`,
 
let REALLIM_WITHINREAL = prove
 (`!f l a s.
      (f ---> l) (atreal a within s) <=>
        !e. &0 < e
            ==> ?d. &0 < d /\
                    !x. x 
IN s /\ &0 < abs(x - a) /\ abs(x - a) < d
                    ==> abs(f(x) - l) < e`,
 
let REALLIM_ATREAL = prove
 (`!f l a.
      (f ---> l) (atreal a) <=>
              !e. &0 < e
                  ==> ?d. &0 < d /\ !x. &0 < abs(x - a) /\ abs(x - a) < d
                          ==> abs(f(x) - l) < e`,
 
let LIM_TRANSFORM_WITHINREAL_SET = prove
 (`!f a s t.
        eventually (\x. x 
IN s <=> x 
IN t) (atreal a)
        ==> ((f --> l) (atreal a within s) <=> (f --> l) (atreal a within t))`,
  REPEAT GEN_TAC THEN REWRITE_TAC[
EVENTUALLY_ATREAL; 
LIM_WITHINREAL] THEN
  DISCH_THEN(X_CHOOSE_THEN `d:real` STRIP_ASSUME_TAC) THEN
  EQ_TAC THEN DISCH_TAC THEN X_GEN_TAC `e:real` THEN DISCH_TAC THEN
  FIRST_X_ASSUM(MP_TAC o SPEC `e:real`) THEN ASM_REWRITE_TAC[] THEN
  DISCH_THEN(X_CHOOSE_THEN `k:real` STRIP_ASSUME_TAC) THEN
  EXISTS_TAC `min d k:real` THEN ASM_REWRITE_TAC[
REAL_LT_MIN] THEN
  ASM_MESON_TAC[]);;
 
let REALLIM_TRANSFORM_WITHIN_SET = prove
 (`!f a s t.
        eventually (\x. x 
IN s <=> x 
IN t) (at a)
        ==> ((f ---> l) (at a within s) <=> (f ---> l) (at a within t))`,
  REPEAT GEN_TAC THEN REWRITE_TAC[
EVENTUALLY_AT; 
REALLIM_WITHIN] THEN
  DISCH_THEN(X_CHOOSE_THEN `d:real` STRIP_ASSUME_TAC) THEN
  EQ_TAC THEN DISCH_TAC THEN X_GEN_TAC `e:real` THEN DISCH_TAC THEN
  FIRST_X_ASSUM(MP_TAC o SPEC `e:real`) THEN ASM_REWRITE_TAC[] THEN
  DISCH_THEN(X_CHOOSE_THEN `k:real` STRIP_ASSUME_TAC) THEN
  EXISTS_TAC `min d k:real` THEN ASM_REWRITE_TAC[
REAL_LT_MIN] THEN
  ASM_MESON_TAC[]);;
 
let REALLIM_TRANSFORM_WITHINREAL_SET = prove
 (`!f a s t.
        eventually (\x. x 
IN s <=> x 
IN t) (atreal a)
        ==> ((f ---> l) (atreal a within s) <=>
             (f ---> l) (atreal a within t))`,
  REPEAT GEN_TAC THEN REWRITE_TAC[
EVENTUALLY_ATREAL; 
REALLIM_WITHINREAL] THEN
  DISCH_THEN(X_CHOOSE_THEN `d:real` STRIP_ASSUME_TAC) THEN
  EQ_TAC THEN DISCH_TAC THEN X_GEN_TAC `e:real` THEN DISCH_TAC THEN
  FIRST_X_ASSUM(MP_TAC o SPEC `e:real`) THEN ASM_REWRITE_TAC[] THEN
  DISCH_THEN(X_CHOOSE_THEN `k:real` STRIP_ASSUME_TAC) THEN
  EXISTS_TAC `min d k:real` THEN ASM_REWRITE_TAC[
REAL_LT_MIN] THEN
  ASM_MESON_TAC[]);;
 
let REALLIM_COMPOSE_WITHIN = prove
 (`!net:A net f g s y z.
    (f ---> y) net /\
    eventually (\w. f w 
IN s /\ (f w = y ==> g y = z)) net /\
    (g ---> z) (atreal y within s)
    ==> ((g o f) ---> z) net`,
  REPEAT GEN_TAC THEN REWRITE_TAC[
tendsto_real; 
CONJ_ASSOC] THEN
  ONCE_REWRITE_TAC[
LEFT_AND_FORALL_THM] THEN
  DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
  MATCH_MP_TAC 
MONO_FORALL THEN X_GEN_TAC `e:real` THEN
  ASM_CASES_TAC `&0 < e` THEN ASM_REWRITE_TAC[] THEN
  REWRITE_TAC[
EVENTUALLY_WITHINREAL; GSYM 
DIST_NZ; 
o_DEF] THEN
  DISCH_THEN(X_CHOOSE_THEN `d:real` ASSUME_TAC) THEN
  FIRST_X_ASSUM(MP_TAC o SPEC `d:real`) THEN
  ASM_REWRITE_TAC[GSYM 
EVENTUALLY_AND] THEN
  MATCH_MP_TAC(REWRITE_RULE[
IMP_CONJ] 
EVENTUALLY_MONO) THEN
  X_GEN_TAC `x:A` THEN
  ASM_CASES_TAC `(f:A->real) x = y` THEN
  ASM_MESON_TAC[REAL_ARITH `abs(x - y) = &0 <=> x = y`;
                REAL_ARITH `&0 < abs(x - y) <=> ~(x = y)`]);;
 
let REALLIM_COMPOSE_AT = prove
 (`!net:A net f g y z.
    (f ---> y) net /\
    eventually (\w. f w = y ==> g y = z) net /\
    (g ---> z) (atreal y)
    ==> ((g o f) ---> z) net`,
 
let TRIVIAL_LIMIT_WITHINREAL_WITHINCOMPLEX = prove
 (`
trivial_limit(atreal x within s) <=>
        
trivial_limit(at (Cx x) within (real 
INTER IMAGE Cx s))`,
  REWRITE_TAC[
trivial_limit; 
AT; 
WITHIN; 
ATREAL] THEN
  REWRITE_TAC[SET_RULE `x 
IN real 
INTER s <=> real x /\ x 
IN s`] THEN
  REWRITE_TAC[TAUT `~(p /\ x /\ q) /\ ~(r /\ x /\ s) <=>
                    x ==> ~(p /\ q) /\ ~(r /\ s)`] THEN
  REWRITE_TAC[
FORALL_REAL;
    MESON[
IN_IMAGE; 
CX_INJ] `Cx x 
IN IMAGE Cx s <=> x 
IN s`] THEN
  REWRITE_TAC[dist; GSYM 
CX_SUB; 
o_THM; 
RE_CX; 
COMPLEX_NORM_CX] THEN
  MATCH_MP_TAC(TAUT `~p /\ ~q /\ (r <=> s) ==> (p \/ r <=> q \/ s)`) THEN
  REPEAT CONJ_TAC THEN TRY EQ_TAC THEN REWRITE_TAC[
LEFT_IMP_EXISTS_THM] THENL
   [DISCH_THEN(MP_TAC o SPECL [`&0`; `&1`]) THEN CONV_TAC REAL_RING;
    DISCH_THEN(MP_TAC o SPECL [`Cx(&0)`; `Cx(&1)`]) THEN
    CONV_TAC COMPLEX_RING;
    MAP_EVERY X_GEN_TAC [`a:real`; `b:real`] THEN STRIP_TAC THEN
    MAP_EVERY EXISTS_TAC [`Cx a`; `Cx b`] THEN ASM_REWRITE_TAC[
CX_INJ] THEN
    ASM_REWRITE_TAC[GSYM 
CX_SUB; 
COMPLEX_NORM_CX];
    MAP_EVERY X_GEN_TAC [`a:complex`; `b:complex`] THEN STRIP_TAC THEN
    SUBGOAL_THEN
     `?d. &0 < d /\
          !z. &0 < abs(z - x) /\ abs(z - x) <= d ==> ~(z 
IN s)`
    STRIP_ASSUME_TAC THENL
     [MATCH_MP_TAC(MESON[] `!a b. P a \/ P b ==> ?x. P x`) THEN
      MAP_EVERY EXISTS_TAC [`norm(a - Cx x)`; `norm(b - Cx x)`] THEN
      ASM_REWRITE_TAC[TAUT `a ==> ~b <=> ~(a /\ b)`] THEN
      UNDISCH_TAC `~(a:complex = b)` THEN NORM_ARITH_TAC;
      ALL_TAC] THEN
    MAP_EVERY EXISTS_TAC [`x + d:real`; `x - d:real`] THEN
    ASM_SIMP_TAC[REAL_ARITH `&0 < d ==> ~(x + d = x - d)`;
                 REAL_ARITH `&0 < d ==> abs((x + d) - x) = d`;
                 REAL_ARITH `&0 < d ==> abs(x - d - x) = d`] THEN
    ASM_MESON_TAC[]]);;
 
let LIM_CONG_WITHINREAL = prove
 (`(!x. ~(x = a) ==> f x = g x)
   ==> (((\x. f x) --> l) (atreal a within s) <=>
        ((g --> l) (atreal a within s)))`,
 
let LIM_CONG_ATREAL = prove
 (`(!x. ~(x = a) ==> f x = g x)
   ==> (((\x. f x) --> l) (atreal a) <=> ((g --> l) (atreal a)))`,
 
let REALLIM_CONG_WITHIN = prove
 (`(!x. ~(x = a) ==> f x = g x)
   ==> (((\x. f x) ---> l) (at a within s) <=> ((g ---> l) (at a within s)))`,
 
let REALLIM_CONG_AT = prove
 (`(!x. ~(x = a) ==> f x = g x)
   ==> (((\x. f x) ---> l) (at a) <=> ((g ---> l) (at a)))`,
 
let continuous_withinreal = prove
 (`f continuous (atreal x within s) <=>
        !e. &0 < e
            ==> ?d. &0 < d /\
                    (!x'. x' 
IN s /\ abs(x' - x) < d ==> dist(f x',f x) < e)`,
  REWRITE_TAC[
CONTINUOUS_WITHINREAL; 
LIM_WITHINREAL] THEN
  REWRITE_TAC[REAL_ARITH `&0 < abs(x - y) <=> ~(x = y)`] THEN
  AP_TERM_TAC THEN REWRITE_TAC[
FUN_EQ_THM] THEN X_GEN_TAC `e:real` THEN
  ASM_CASES_TAC `&0 < e` THEN ASM_REWRITE_TAC[] THEN
  AP_TERM_TAC THEN REWRITE_TAC[
FUN_EQ_THM] THEN X_GEN_TAC `d:real` THEN
  ASM_CASES_TAC `&0 < d` THEN ASM_REWRITE_TAC[] THEN
  AP_TERM_TAC THEN ABS_TAC THEN ASM_MESON_TAC[
DIST_REFL]);;
 
let continuous_atreal = prove
 (`f continuous (atreal x) <=>
        !e. &0 < e
            ==> ?d. &0 < d /\
                    (!x'. abs(x' - x) < d ==> dist(f x',f x) < e)`,
 
let IS_REAL_INTERVAL_CASES = prove
 (`!s. 
is_realinterval s <=>
        s = {} \/
        s = (:real) \/
        (?a. s = {x | a < x}) \/
        (?a. s = {x | a <= x}) \/
        (?b. s = {x | x <= b}) \/
        (?b. s = {x | x < b}) \/
        (?a b. s = {x | a < x /\ x < b}) \/
        (?a b. s = {x | a < x /\ x <= b}) \/
        (?a b. s = {x | a <= x /\ x < b}) \/
        (?a b. s = {x | a <= x /\ x <= b})`,
 
let REAL_MIDPOINT_IN_CONVEX = prove
 (`!s x y. 
is_realinterval s /\ x 
IN s /\ y 
IN s ==> ((x + y) / &2) 
IN s`,
  REPEAT STRIP_TAC THEN
  REWRITE_TAC[REAL_ARITH `(x + y) / &2 = inv(&2) * x + inv(&2) * y`] THEN
  FIRST_X_ASSUM(MATCH_MP_TAC o GEN_REWRITE_RULE I [
REAL_CONVEX]) THEN
  CONV_TAC REAL_RAT_REDUCE_CONV THEN ASM_REWRITE_TAC[]);;
 
let REAL_DIFFERENTIABLE_AT_RPOW = prove
 (`!x y. ~(x = &0) ==> (\x. x rpow y) 
real_differentiable atreal x`,
  REPEAT GEN_TAC THEN
  REWRITE_TAC[REAL_ARITH `~(x = &0) <=> &0 < x \/ &0 < --x`] THEN
  STRIP_TAC THEN MATCH_MP_TAC 
REAL_DIFFERENTIABLE_TRANSFORM_ATREAL THEN
  REWRITE_TAC[] THEN ONCE_REWRITE_TAC[
SWAP_EXISTS_THM] THEN
  EXISTS_TAC `abs x` THENL
   [EXISTS_TAC `\x. exp(y * log x)` THEN
    ASM_SIMP_TAC[REAL_ARITH `&0 < x ==> &0 < abs x`] THEN CONJ_TAC THENL
     [X_GEN_TAC `z:real` THEN DISCH_TAC THEN
      SUBGOAL_THEN `&0 < z` (fun th -> REWRITE_TAC[rpow; th]) THEN
      ASM_REAL_ARITH_TAC;
      REAL_DIFFERENTIABLE_TAC THEN ASM_REAL_ARITH_TAC];
    ASM_CASES_TAC `?m n. 
ODD m /\ 
ODD n /\ abs y = &m / &n` THENL
     [EXISTS_TAC `\x. --(exp(y * log(--x)))`;
      EXISTS_TAC `\x. exp(y * log(--x))`] THEN
    (ASM_SIMP_TAC[REAL_ARITH `&0 < --x ==> &0 < abs x`] THEN CONJ_TAC THENL
      [X_GEN_TAC `z:real` THEN DISCH_TAC THEN
       SUBGOAL_THEN `~(&0 < z) /\ ~(z = &0)`
         (fun th -> ASM_REWRITE_TAC[rpow; th]) THEN
       ASM_REAL_ARITH_TAC;
       REAL_DIFFERENTIABLE_TAC THEN ASM_REAL_ARITH_TAC])]);;
 
let REALLIM_RPOW = prove
 (`!net f l n.
        (f ---> l) net /\ (l = &0 ==> &0 <= n)
        ==> ((\x. f x rpow n) ---> l rpow n) net`,
 
let LHOSPITAL = prove
 (`!f g f' g' c l d.
        &0 < d /\
        (!x. &0 < abs(x - c) /\ abs(x - c) < d
             ==> (f 
has_real_derivative f'(x)) (atreal x) /\
                 (g 
has_real_derivative g'(x)) (atreal x) /\
                 ~(g'(x) = &0)) /\
        (f ---> &0) (atreal c) /\ (g ---> &0) (atreal c) /\
        ((\x. f'(x) / g'(x)) ---> l) (atreal c)
        ==> ((\x. f(x) / g(x)) ---> l) (atreal c)`,
  SUBGOAL_THEN
    `!f g f' g' c l d.
        &0 < d /\
        (!x. &0 < abs(x - c) /\ abs(x - c) < d
             ==> (f 
has_real_derivative f'(x)) (atreal x) /\
                 (g 
has_real_derivative g'(x)) (atreal x) /\
                 ~(g'(x) = &0)) /\
        f(c) = &0 /\ g(c) = &0 /\
        (f ---> &0) (atreal c) /\ (g ---> &0) (atreal c) /\
        ((\x. f'(x) / g'(x)) ---> l) (atreal c)
        ==> ((\x. f(x) / g(x)) ---> l) (atreal c)`
  ASSUME_TAC THENL
   [REWRITE_TAC[TAUT `a ==> b /\ c <=> (a ==> b) /\ (a ==> c)`] THEN
    REWRITE_TAC[
FORALL_AND_THM] THEN REPEAT STRIP_TAC THEN
    SUBGOAL_THEN
     `(!x. abs(x - c) < d ==> f 
real_continuous atreal x) /\
      (!x. abs(x - c) < d ==> g 
real_continuous atreal x)`
    STRIP_ASSUME_TAC THENL
     [REWRITE_TAC[
AND_FORALL_THM] THEN X_GEN_TAC `x:real` THEN
      DISJ_CASES_TAC(REAL_ARITH `x = c \/ &0 < abs(x - c)`) THENL
       [ASM_REWRITE_TAC[
REAL_CONTINUOUS_ATREAL]; ALL_TAC] THEN
      REPEAT STRIP_TAC THEN
      MATCH_MP_TAC 
REAL_DIFFERENTIABLE_IMP_CONTINUOUS_ATREAL THEN
      REWRITE_TAC[
real_differentiable] THEN ASM_MESON_TAC[];
      ALL_TAC] THEN
    SUBGOAL_THEN
     `!x.  &0 < abs(x - c) /\ abs(x - c) < d ==> ~(g x = &0)`
    STRIP_ASSUME_TAC THENL
     [REPEAT STRIP_TAC THEN
      SUBGOAL_THEN `c < x \/ x < c` DISJ_CASES_TAC THENL
       [ASM_REAL_ARITH_TAC;
        MP_TAC(ISPECL [`g:real->real`; `g':real->real`; `c:real`; `x:real`]
          
REAL_ROLLE);
        MP_TAC(ISPECL [`g:real->real`; `g':real->real`; `x:real`; `c:real`]
          
REAL_ROLLE)] THEN
      ASM_REWRITE_TAC[NOT_IMP; 
NOT_EXISTS_THM] THEN
      (REPEAT CONJ_TAC THENL
        [REWRITE_TAC[
REAL_CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN] THEN
         REWRITE_TAC[
IN_REAL_INTERVAL] THEN REPEAT STRIP_TAC THEN
         MATCH_MP_TAC 
REAL_CONTINUOUS_ATREAL_WITHINREAL;
         REWRITE_TAC[
IN_REAL_INTERVAL] THEN REPEAT STRIP_TAC;
         X_GEN_TAC `y:real` THEN REWRITE_TAC[
IN_REAL_INTERVAL] THEN
         DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
         REWRITE_TAC[]] THEN
       FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REAL_ARITH_TAC);
      ALL_TAC] THEN
    UNDISCH_TAC `((\x. f' x / g' x) ---> l) (atreal c)` THEN
    REWRITE_TAC[
REALLIM_ATREAL] THEN MATCH_MP_TAC 
MONO_FORALL THEN
    X_GEN_TAC `e:real` THEN ASM_CASES_TAC `&0 < e` THEN ASM_REWRITE_TAC[] THEN
    DISCH_THEN(X_CHOOSE_THEN `k:real` STRIP_ASSUME_TAC) THEN
    EXISTS_TAC `min d k:real` THEN ASM_REWRITE_TAC[
REAL_LT_MIN] THEN
    X_GEN_TAC `x:real` THEN STRIP_TAC THEN
    SUBGOAL_THEN
     `?y. &0 < abs(y - c) /\ abs(y - c) < abs(x - c) /\
          (f:real->real) x / g x = f' y / g' y`
    STRIP_ASSUME_TAC THENL
     [ALL_TAC; ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[
REAL_LT_TRANS]] THEN
    SUBGOAL_THEN `c < x \/ x < c` DISJ_CASES_TAC THENL
     [ASM_REAL_ARITH_TAC;
      MP_TAC(ISPECL
       [`f:real->real`; `g:real->real`; `f':real->real`; `g':real->real`;
        `c:real`; `x:real`] 
REAL_MVT_CAUCHY);
      MP_TAC(ISPECL
       [`f:real->real`; `g:real->real`; `f':real->real`; `g':real->real`;
        `x:real`; `c:real`] 
REAL_MVT_CAUCHY)] THEN
    (ASM_REWRITE_TAC[
IN_REAL_INTERVAL] THEN ANTS_TAC THENL
      [REWRITE_TAC[
CONJ_ASSOC] THEN CONJ_TAC THENL
        [CONJ_TAC THEN
         REWRITE_TAC[
REAL_CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN] THEN
         REWRITE_TAC[
IN_REAL_INTERVAL] THEN REPEAT STRIP_TAC THEN
         MATCH_MP_TAC 
REAL_CONTINUOUS_ATREAL_WITHINREAL;
         REPEAT STRIP_TAC] THEN
       FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REAL_ARITH_TAC;
       MATCH_MP_TAC 
MONO_EXISTS THEN REWRITE_TAC[
REAL_SUB_RZERO] THEN
       GEN_TAC THEN STRIP_TAC THEN
        REPEAT(CONJ_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC]) THEN
       MATCH_MP_TAC(REAL_FIELD
        `f * g' = g * f' /\ ~(g = &0) /\ ~(g' = &0) ==> f / g = f' / g'`) THEN
       CONJ_TAC THENL [ASM_REAL_ARITH_TAC; CONJ_TAC] THEN
       FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REAL_ARITH_TAC]);
    REPEAT GEN_TAC THEN
    FIRST_X_ASSUM(MP_TAC o SPECL
     [`\x:real. if x = c then &0 else f(x)`;
                `\x:real. if x = c then &0 else g(x)`;
                `f':real->real`; `g':real->real`;
                `c:real`; `l:real`; `d:real`]) THEN
    REWRITE_TAC[] THEN MATCH_MP_TAC MONO_IMP THEN CONJ_TAC THEN
    REPEAT(MATCH_MP_TAC MONO_AND THEN CONJ_TAC) THEN
    TRY(SIMP_TAC[
REALLIM_ATREAL;REAL_ARITH `&0 < abs(x - c) ==> ~(x = c)`] THEN
        NO_TAC) THEN
    DISCH_TAC THEN X_GEN_TAC `x:real` THEN STRIP_TAC THEN
    FIRST_X_ASSUM(MP_TAC o SPEC `x:real`) THEN ASM_REWRITE_TAC[] THEN
    REPEAT(MATCH_MP_TAC MONO_AND THEN CONJ_TAC) THEN REWRITE_TAC[] THEN
    MATCH_MP_TAC(REWRITE_RULE[TAUT `a /\ b /\ c ==> d <=> a /\ b ==> c ==> d`]
          
HAS_REAL_DERIVATIVE_TRANSFORM_ATREAL) THEN
    EXISTS_TAC `abs(x - c)` THEN ASM_REAL_ARITH_TAC]);;
 
let REAL_SUM_INTEGRAL_UBOUND_DECREASING = prove
 (`!f g m n.
      m <= n /\
      (!x. x 
IN real_interval[&m - &1,&n]
           ==> (g 
has_real_derivative f(x))
               (atreal x within 
real_interval[&m - &1,&n])) /\
      (!x y. &m - &1 <= x /\ x <= y /\ y <= &n ==> f y <= f x)
      ==> sum(m..n) (\k. f(&k)) <= g(&n) - g(&m - &1)`,
  REPEAT STRIP_TAC THEN MATCH_MP_TAC 
REAL_LE_TRANS THEN
  EXISTS_TAC `sum(m..n) (\k. g(&(k + 1) - &1) - g(&k - &1))` THEN
  CONJ_TAC THENL
   [ALL_TAC;
    ASM_REWRITE_TAC[
SUM_DIFFS_ALT] THEN
    ASM_REWRITE_TAC[GSYM REAL_OF_NUM_ADD; REAL_ARITH `(x + &1) - &1 = x`] THEN
    REWRITE_TAC[
REAL_LE_REFL]] THEN
  MATCH_MP_TAC 
SUM_LE_NUMSEG THEN X_GEN_TAC `k:num` THEN STRIP_TAC THEN
  MP_TAC(ISPECL [`g:real->real`; `f:real->real`; `&k - &1`; `&k`]
                
REAL_MVT_SIMPLE) THEN
  ASM_REWRITE_TAC[REAL_ARITH `k - &1 < k`] THEN ANTS_TAC THENL
   [REPEAT STRIP_TAC THEN MATCH_MP_TAC 
HAS_REAL_DERIVATIVE_WITHIN_SUBSET THEN
    EXISTS_TAC `
real_interval[&m - &1,&n]` THEN CONJ_TAC THENL
     [FIRST_X_ASSUM MATCH_MP_TAC THEN
      FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [
IN_REAL_INTERVAL]);
      REWRITE_TAC[
SUBSET] THEN GEN_TAC] THEN
    REWRITE_TAC[
IN_REAL_INTERVAL] THEN
    RULE_ASSUM_TAC(REWRITE_RULE[GSYM REAL_OF_NUM_LE]) THEN ASM_REAL_ARITH_TAC;
    REWRITE_TAC[GSYM REAL_OF_NUM_ADD; REAL_ARITH `(a + &1) - &1 = a`] THEN
    DISCH_THEN(X_CHOOSE_THEN `t:real`
     (CONJUNCTS_THEN2 ASSUME_TAC SUBST1_TAC)) THEN
    REWRITE_TAC[REAL_ARITH `a * (x - (x - &1)) = a`] THEN
    FIRST_X_ASSUM MATCH_MP_TAC THEN
    FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [
IN_REAL_INTERVAL]) THEN
    RULE_ASSUM_TAC(REWRITE_RULE[GSYM REAL_OF_NUM_LE]) THEN
    ASM_REAL_ARITH_TAC]);;
 
let LIM_ZERO_POSINFINITY = prove
 (`!f l. ((\x. f(&1 / x)) --> l) (atreal (&0)) ==> (f --> l) 
at_posinfinity`,
  REPEAT GEN_TAC THEN REWRITE_TAC[
LIM_ATREAL; 
LIM_AT_POSINFINITY] THEN
  DISCH_TAC THEN X_GEN_TAC `e:real` THEN DISCH_TAC THEN
  FIRST_X_ASSUM(MP_TAC o SPEC `e:real`) THEN ASM_REWRITE_TAC[] THEN
  REWRITE_TAC[dist; 
REAL_SUB_RZERO; 
real_ge] THEN
  DISCH_THEN(X_CHOOSE_THEN `d:real` STRIP_ASSUME_TAC) THEN
  EXISTS_TAC `&2 / d` THEN X_GEN_TAC `z:real` THEN DISCH_TAC THEN
  FIRST_X_ASSUM(MP_TAC o SPEC `inv(z):real`) THEN
  REWRITE_TAC[
real_div; REAL_MUL_LINV; 
REAL_INV_INV] THEN
  REWRITE_TAC[REAL_MUL_LID] THEN DISCH_THEN MATCH_MP_TAC THEN
  ASM_REWRITE_TAC[
REAL_ABS_INV; 
REAL_LT_INV_EQ] THEN CONJ_TAC THENL
   [FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH
     `a <= z ==> &0 < a ==> &0 < abs z`));
    GEN_REWRITE_TAC RAND_CONV [GSYM 
REAL_INV_INV] THEN
    MATCH_MP_TAC 
REAL_LT_INV2 THEN ASM_REWRITE_TAC[
REAL_LT_INV_EQ] THEN
    FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH
     `&2 / d <= z ==> &0 < &2 / d ==> inv d < abs z`))] THEN
  ASM_SIMP_TAC[
REAL_LT_DIV; 
REAL_OF_NUM_LT; ARITH]);;
 
let LIM_ZERO_NEGINFINITY = prove
 (`!f l. ((\x. f(&1 / x)) --> l) (atreal (&0)) ==> (f --> l) 
at_neginfinity`,
  REPEAT GEN_TAC THEN REWRITE_TAC[
LIM_ATREAL; 
LIM_AT_NEGINFINITY] THEN
  DISCH_TAC THEN X_GEN_TAC `e:real` THEN DISCH_TAC THEN
  FIRST_X_ASSUM(MP_TAC o SPEC `e:real`) THEN ASM_REWRITE_TAC[] THEN
  REWRITE_TAC[dist; 
REAL_SUB_RZERO; 
real_ge] THEN
  DISCH_THEN(X_CHOOSE_THEN `d:real` STRIP_ASSUME_TAC) THEN
  EXISTS_TAC `--(&2 / d)` THEN X_GEN_TAC `z:real` THEN DISCH_TAC THEN
  FIRST_X_ASSUM(MP_TAC o SPEC `inv(z):real`) THEN
  REWRITE_TAC[
real_div; REAL_MUL_LINV; 
REAL_INV_INV] THEN
  REWRITE_TAC[REAL_MUL_LID] THEN DISCH_THEN MATCH_MP_TAC THEN
  ASM_REWRITE_TAC[
REAL_ABS_INV; 
REAL_LT_INV_EQ] THEN CONJ_TAC THENL
   [FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH
     `z <= --a ==> &0 < a ==> &0 < abs z`));
    GEN_REWRITE_TAC RAND_CONV [GSYM 
REAL_INV_INV] THEN
    MATCH_MP_TAC 
REAL_LT_INV2 THEN ASM_REWRITE_TAC[
REAL_LT_INV_EQ] THEN
    FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH
     `z <= --(&2 / d) ==> &0 < &2 / d ==> inv d < abs z`))] THEN
  ASM_SIMP_TAC[
REAL_LT_DIV; 
REAL_OF_NUM_LT; ARITH]);;
 
let real_convex_on = new_definition
  `(f:real->real) real_convex_on s <=>
        !x y u v. x IN s /\ y IN s /\ &0 <= u /\ &0 <= v /\ (u + v = &1)
                  ==> f(u * x + v * y) <= u * f(x) + v * f(y)`;;let AGM_GEN = prove
 (`!a x k:A->bool.
        
FINITE k /\ sum k a = &1 /\ (!i. i 
IN k ==> &0 <= a i /\ &0 <= x i)
        ==> product k (\i. x i rpow a i) <= sum k (\i. a i * x i)`,
 
let AGM_RPOW = prove
 (`!k:A->bool x n.
        k 
HAS_SIZE n /\ ~(n = 0) /\ (!i. i 
IN k ==> &0 <= x(i))
        ==> product k (\i. x(i) rpow (&1 / &n)) <= sum k (\i. x(i) / &n)`,
 
let AGM_ROOT = prove
 (`!k:A->bool x n.
        k 
HAS_SIZE n /\ ~(n = 0) /\ (!i. i 
IN k ==> &0 <= x(i))
        ==> root n (product k x) <= sum k x / &n`,
 
let AGM_SQRT = prove
 (`!x y. &0 <= x /\ &0 <= y ==> sqrt(x * y) <= (x + y) / &2`,
 
let AGM = prove
 (`!k:A->bool x n.
        k 
HAS_SIZE n /\ ~(n = 0) /\ (!i. i 
IN k ==> &0 <= x(i))
        ==> product k x <= (sum k x / &n) pow n`,
 
let AGM_2 = prove
 (`!x y u v.
        &0 <= x /\ &0 <= y /\ &0 <= u /\ &0 <= v /\ u + v = &1
        ==> x rpow u * y rpow v <= u * x + v * y`,
 
let YOUNG_INEQUALITY = prove
 (`!a b p q. &0 <= a /\ &0 <= b /\ &0 < p /\ &0 < q /\ inv(p) + inv(q) = &1
             ==> a * b <= a rpow p / p + b rpow q / q`,
 
let HOELDER = prove
 (`!k:A->bool a x y.
        
FINITE k /\ sum k a = &1 /\
        (!i. i 
IN k ==> &0 <= a i /\ &0 <= x i /\ &0 <= y i)
        ==> product k (\i. x i rpow a i) + product k (\i. y i rpow a i)
            <= product k (\i. (x i + y i) rpow a i)`,
  REPEAT STRIP_TAC THEN
  SUBGOAL_THEN `&0 <= product (k:A->bool) (\i. (x i + y i) rpow a i)`
  MP_TAC THENL
   [MATCH_MP_TAC 
PRODUCT_POS_LE THEN ASM_SIMP_TAC[
REAL_LE_ADD; 
RPOW_POS_LE];
    ALL_TAC] THEN
  REWRITE_TAC[REAL_ARITH `&0 <= x <=> x = &0 \/ &0 < x`] THEN
  ASM_SIMP_TAC[
PRODUCT_EQ_0; 
RPOW_EQ_0; TAUT `p /\ q <=> ~(p ==> ~q)`;
   REAL_ARITH `&0 <= x /\ &0 <= y ==> (x + y = &0 <=> x = &0 /\ y = &0)`] THEN
  REWRITE_TAC[NOT_IMP] THEN STRIP_TAC THENL
   [MATCH_MP_TAC(REAL_ARITH
     `x = &0 /\ y = &0 /\ z = &0 ==> x + y <= z`) THEN
    ASM_SIMP_TAC[
PRODUCT_EQ_0; 
RPOW_EQ_0] THEN ASM_MESON_TAC[REAL_ADD_LID];
    GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_LID]] THEN
  ASM_SIMP_TAC[GSYM 
REAL_LE_LDIV_EQ; GSYM 
PRODUCT_DIV; GSYM 
RPOW_DIV;
               REAL_ARITH `(x + y) / z:real = x / z + y / z`] THEN
  ASM_SIMP_TAC[GSYM 
RPOW_PRODUCT] THEN
  TRANS_TAC 
REAL_LE_TRANS
   `sum k (\i:A. a i * (x i / (x i + y i))) +
    sum k (\i. a i * (y i / (x i + y i)))` THEN
  CONJ_TAC THENL
   [MATCH_MP_TAC 
REAL_LE_ADD2 THEN CONJ_TAC THEN MATCH_MP_TAC 
AGM_GEN THEN
    ASM_SIMP_TAC[
REAL_LE_ADD; 
REAL_LE_DIV];
    ASM_SIMP_TAC[GSYM 
SUM_ADD]] THEN
  FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH
   `s = &1 ==> p = s ==> p <= &1`)) THEN
  MATCH_MP_TAC 
SUM_EQ THEN ASM_REWRITE_TAC[] THEN
  X_GEN_TAC `i:A` THEN DISCH_TAC THEN
  ASM_CASES_TAC `(a:A->real) i = &0` THEN
  ASM_REWRITE_TAC[
REAL_MUL_LZERO; REAL_ADD_LID] THEN
  FIRST_X_ASSUM(MP_TAC o MATCH_MP 
REAL_LT_IMP_NZ) THEN
  ASM_SIMP_TAC[
PRODUCT_EQ_0; 
RPOW_EQ_0; 
NOT_EXISTS_THM] THEN
  DISCH_THEN(MP_TAC o SPEC `i:A`) THEN ASM_REWRITE_TAC[] THEN
  CONV_TAC REAL_FIELD);;
 
let RPOW_MINUS1_QUOTIENT_LT = prove
 (`!a x y. &0 < a /\ ~(a = &1) /\ &0 < x /\ x < y
           ==> (a rpow x - &1) / x < (a rpow y - &1) / y`,
  REPEAT STRIP_TAC THEN
  MP_TAC(ISPECL [`\x. (a rpow x - &1) / x`;
                 `\x. log a * a rpow x / x - (a rpow x - &1) / x pow 2`;
                 `x:real`; `y:real`]
   
HAS_REAL_DERIVATIVE_STRICTLY_INCREASING_IMP) THEN
  ASM_REWRITE_TAC[
IN_REAL_INTERVAL] THEN DISCH_THEN MATCH_MP_TAC THEN
  CONJ_TAC THENL
   [ASM_SIMP_TAC[rpow] THEN REPEAT STRIP_TAC THEN REAL_DIFF_TAC THEN
    REPEAT(POP_ASSUM MP_TAC) THEN CONV_TAC REAL_FIELD;
    ALL_TAC] THEN
  X_GEN_TAC `z:real` THEN DISCH_TAC THEN
  SUBGOAL_THEN `&0 < z` ASSUME_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
  MATCH_MP_TAC 
REAL_LT_LCANCEL_IMP THEN
  EXISTS_TAC `(z:real) pow 2` THEN
  ASM_SIMP_TAC[
REAL_POW_LT; 
REAL_MUL_RZERO; REAL_FIELD
   `&0 < x ==> x pow 2 * (a * b / x - c / x pow 2) = a * b * x - c`] THEN
  REWRITE_TAC[REAL_ARITH `l * a * z - (a - &1) = a * (l * z - &1) + &1`] THEN
  MP_TAC(ISPECL [`\x. a rpow x * (log a * x - &1) + &1`;
                 `\x. log(a) pow 2 * x * a rpow x`;
                 `&0`; `z:real`]
   
HAS_REAL_DERIVATIVE_STRICTLY_INCREASING_IMP) THEN
  ASM_REWRITE_TAC[
RPOW_0] THEN
  ANTS_TAC THENL [ALL_TAC; REAL_ARITH_TAC] THEN CONJ_TAC THENL
   [REPEAT STRIP_TAC THEN REAL_DIFF_TAC THEN
    REPEAT(POP_ASSUM MP_TAC) THEN CONV_TAC REAL_FIELD;
    REWRITE_TAC[
IN_REAL_INTERVAL] THEN REPEAT STRIP_TAC THEN
    REPEAT(MATCH_MP_TAC 
REAL_LT_MUL THEN CONJ_TAC) THEN
    ASM_SIMP_TAC[
RPOW_POS_LT; 
REAL_LT_POW_2] THEN
    ASM_SIMP_TAC[GSYM 
LOG_1; 
LOG_INJ; 
REAL_LT_01]]);;
 
let REAL_LE_ABS_SINH = prove
 (`!x. abs x <= abs((exp x - inv(exp x)) / &2)`,
  GEN_TAC THEN ASM_CASES_TAC `&0 <= x` THENL
   [MATCH_MP_TAC(REAL_ARITH `&0 <= x /\ x <= y ==> abs x <= abs y`) THEN
    ASM_SIMP_TAC[
REAL_LE_X_SINH];
    MATCH_MP_TAC(REAL_ARITH `~(&0 <= x) /\ --x <= --y ==> abs x <= abs y`) THEN
    ASM_REWRITE_TAC[REAL_ARITH `--((a - b) / &2) = (b - a) / &2`] THEN
    MATCH_MP_TAC 
REAL_LE_TRANS THEN
    EXISTS_TAC `(exp(--x) - inv(exp(--x))) / &2` THEN
    ASM_SIMP_TAC[
REAL_LE_X_SINH; REAL_ARITH `~(&0 <= x) ==> &0 <= --x`] THEN
    REWRITE_TAC[
REAL_EXP_NEG; 
REAL_INV_INV] THEN REAL_ARITH_TAC]);;
 
let log_convex_on = new_definition
 `f log_convex_on (s:real^N->bool) <=>
        (!x y u v. x IN s /\ y IN s /\ &0 <= u /\ &0 <= v /\ u + v = &1
                   ==> &0 <= f(u % x + v % y) /\
                       f(u % x + v % y) <= f(x) rpow u * f(y) rpow v)`;;let LOG_CONVEX_ON_CONVEX = prove
 (`!f s:real^N->bool.
        convex s
        ==> (f 
log_convex_on s <=>
             (!x. x 
IN s ==> &0 <= f x) /\
             !x y u v. x 
IN s /\ y 
IN s /\ &0 <= u /\ &0 <= v /\ u + v = &1
                       ==> f(u % x + v % y) <= f(x) rpow u * f(y) rpow v)`,
 
let real_log_convex_on = new_definition
 `(f:real->real) real_log_convex_on s <=>
        (!x y u v. x IN s /\ y IN s /\ &0 <= u /\ &0 <= v /\ u + v = &1
                   ==> &0 <= f(u * x + v * y) /\
                       f(u * x + v * y) <= f(x) rpow u * f(y) rpow v)`;;let HAS_REAL_INTEGRAL_SUBSTITUTION_STRONG = prove
 (`!f g g' a b c d k.
        
COUNTABLE k /\
        f 
real_integrable_on real_interval[c,d] /\
        g 
real_continuous_on real_interval[a,b] /\
        
IMAGE g (
real_interval[a,b]) 
SUBSET real_interval[c,d] /\
        (!x. x 
IN real_interval[a,b] 
DIFF k
                  ==> (g 
has_real_derivative g'(x))
                       (atreal x within 
real_interval[a,b]) /\
                      f 
real_continuous
                        (atreal(g x)) within 
real_interval[c,d]) /\
        a <= b /\ c <= d /\ g a <= g b
        ==> ((\x. f(g x) * g'(x)) 
has_real_integral
             real_integral (
real_interval[g a,g b]) f) (
real_interval[a,b])`,
 
let DROPOUT_PUSHIN = prove
 (`!k t x.
        dimindex(:M) + 1 = dimindex(:N)
        ==> (dropout k:real^N->real^M) (pushin k t x) = x`,
  REPEAT GEN_TAC THEN DISCH_THEN(ASSUME_TAC o SYM) THEN
  ASM_SIMP_TAC[
CART_EQ; dropout; pushin; 
LAMBDA_BETA;
               ARITH_RULE `1 <= n + 1`; 
ADD_SUB;
               ARITH_RULE `m <= n ==> m <= n + 1 /\ m + 1 <= n + 1`] THEN
  ARITH_TAC);;
 
let PUSHIN_DROPOUT = prove
 (`!k x.
        dimindex(:M) + 1 = dimindex(:N) /\ 1 <= k /\ k <= dimindex(:N)
        ==> pushin k (x$k) ((dropout k:real^N->real^M) x) = x`,
  REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN(ASSUME_TAC o GSYM)) THEN
  ASM_SIMP_TAC[
CART_EQ; dropout; pushin; 
LAMBDA_BETA;
               ARITH_RULE `i <= n + 1 ==> i - 1 <= n`] THEN
  X_GEN_TAC `i:num` THEN STRIP_TAC THEN
  ASM_CASES_TAC `i:num = k` THEN ASM_REWRITE_TAC[
LT_REFL] THEN
  FIRST_X_ASSUM(DISJ_CASES_TAC o MATCH_MP (ARITH_RULE
   `~(i:num = k) ==> i < k \/ k < i`)) THEN
  ASM_SIMP_TAC[ARITH_RULE `i:num < k ==> ~(k < i)`] THEN
  W(MP_TAC o PART_MATCH (lhs o rand) 
LAMBDA_BETA o lhand o snd) THEN
  (ANTS_TAC THENL [ASM_ARITH_TAC; DISCH_THEN SUBST1_TAC]) THEN
  ASM_SIMP_TAC[ARITH_RULE `k < i ==> ~(i - 1 < k)`] THEN
  AP_TERM_TAC THEN ASM_ARITH_TAC);;
 
let DROPOUT_GALOIS = prove
 (`!k x:real^N y:real^M.
        dimindex(:M) + 1 = dimindex(:N) /\ 1 <= k /\ k <= dimindex(:N)
        ==> (y = dropout k x <=> (?t. x = pushin k t y))`,
  REPEAT STRIP_TAC THEN EQ_TAC THENL
   [DISCH_THEN SUBST1_TAC THEN
    EXISTS_TAC `(x:real^N)$k` THEN ASM_SIMP_TAC[
PUSHIN_DROPOUT];
    DISCH_THEN(X_CHOOSE_THEN `t:real` SUBST1_TAC) THEN
    ASM_SIMP_TAC[
DROPOUT_PUSHIN]]);;
 
let IN_IMAGE_DROPOUT = prove
 (`!x s.
        dimindex(:M) + 1 = dimindex(:N) /\ 1 <= k /\ k <= dimindex(:N)
        ==> (x 
IN IMAGE (dropout k:real^N->real^M) s <=>
             ?t. (pushin k t x) 
IN s)`,
 
let CLOSED_INTERVAL_DROPOUT = prove
 (`!k a b. dimindex(:M) + 1 = dimindex(:N) /\
           1 <= k /\ k <= dimindex(:N) /\
           a$k <= b$k
           ==> interval[dropout k a,dropout k b] =
               
IMAGE (dropout k:real^N->real^M) (interval[a,b])`,
  REPEAT STRIP_TAC THEN
  ASM_SIMP_TAC[
EXTENSION; 
IN_IMAGE_DROPOUT; 
IN_INTERVAL] THEN
  X_GEN_TAC `x:real^M` THEN
  SIMP_TAC[pushin; dropout; 
LAMBDA_BETA] THEN EQ_TAC THENL
   [DISCH_TAC THEN EXISTS_TAC `(a:real^N)$k` THEN X_GEN_TAC `i:num` THEN
    STRIP_TAC THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[] THENL
     [FIRST_X_ASSUM(MP_TAC o SPEC `i:num`) THEN ASM_REWRITE_TAC[] THEN
      DISCH_THEN MATCH_MP_TAC THEN ASM_ARITH_TAC;
      COND_CASES_TAC THEN ASM_REWRITE_TAC[
REAL_LE_REFL] THEN
      FIRST_X_ASSUM(MP_TAC o SPEC `i - 1`) THEN
      COND_CASES_TAC THENL [ASM_ARITH_TAC; ASM_REWRITE_TAC[]] THEN
      ANTS_TAC THENL [ASM_ARITH_TAC; ASM_SIMP_TAC[
SUB_ADD]]];
    DISCH_THEN(X_CHOOSE_TAC `t:real`) THEN X_GEN_TAC `i:num` THEN
    STRIP_TAC THEN COND_CASES_TAC THENL
     [FIRST_X_ASSUM(MP_TAC o SPEC `i:num`) THEN ASM_REWRITE_TAC[] THEN
      DISCH_THEN MATCH_MP_TAC THEN ASM_ARITH_TAC;
      FIRST_X_ASSUM(MP_TAC o SPEC `i + 1`) THEN
      ASM_REWRITE_TAC[] THEN ANTS_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN
      COND_CASES_TAC THEN ASM_REWRITE_TAC[] THENL [ASM_ARITH_TAC; ALL_TAC] THEN
      COND_CASES_TAC THEN ASM_REWRITE_TAC[] THENL [ASM_ARITH_TAC; ALL_TAC] THEN
      ASM_REWRITE_TAC[
ADD_SUB]]]);;
 
let IMAGE_DROPOUT_CLOSED_INTERVAL = prove
 (`!k a b. dimindex(:M) + 1 = dimindex(:N) /\
           1 <= k /\ k <= dimindex(:N)
           ==> 
IMAGE (dropout k:real^N->real^M) (interval[a,b]) =
                  if a$k <= b$k then interval[dropout k a,dropout k b]
                  else {}`,
 
let DROPOUT_EQ = prove
 (`!x y k. dimindex(:M) + 1 = dimindex(:N) /\ 1 <= k /\ k <= dimindex(:N) /\
           x$k = y$k /\ (dropout k:real^N->real^M) x = dropout k y
           ==> x = y`,
  SIMP_TAC[
CART_EQ; dropout; 
VEC_COMPONENT; 
LAMBDA_BETA; 
IN_ELIM_THM] THEN
  MAP_EVERY X_GEN_TAC [`x:real^N`; `y:real^N`; `k:num`] THEN
  STRIP_TAC THEN X_GEN_TAC `i:num` THEN STRIP_TAC THEN
  ASM_CASES_TAC `i:num = k` THEN ASM_REWRITE_TAC[] THEN
  FIRST_ASSUM(DISJ_CASES_TAC o MATCH_MP (ARITH_RULE
   `~(i:num = k) ==> i < k \/ k < i`))
  THENL
   [FIRST_X_ASSUM(MP_TAC o SPEC `i:num`) THEN ASM_SIMP_TAC[];
    FIRST_X_ASSUM(MP_TAC o SPEC `i - 1`) THEN
    ASM_SIMP_TAC[
SUB_ADD; ARITH_RULE `k < i ==> ~(i - 1 < k)`]] THEN
  DISCH_THEN MATCH_MP_TAC THEN ASM_ARITH_TAC);;
 
let DOT_DROPOUT = prove
 (`!k x y:real^N.
        dimindex(:M) + 1 = dimindex(:N) /\ 1 <= k /\ k <= dimindex(:N)
        ==> (dropout k x:real^M) dot (dropout k y) = x dot y - x$k * y$k`,
  REPEAT STRIP_TAC THEN SIMP_TAC[dot; dropout; 
LAMBDA_BETA] THEN
  REWRITE_TAC[TAUT `(if p then x else y:real) * (if p then a else b) =
                    (if p then x * a else y * b)`] THEN
  SIMP_TAC[
SUM_CASES; 
FINITE_NUMSEG] THEN
  SUBGOAL_THEN
   `(!i. i 
IN 1..dimindex(:M) /\ i < k <=> i 
IN 1..k-1) /\
    (!i.  i 
IN 1..dimindex(:M) /\ ~(i < k) <=> i 
IN k..dimindex(:M))`
  (fun th -> REWRITE_TAC[th])
  THENL [REWRITE_TAC[
IN_NUMSEG] THEN ASM_ARITH_TAC; ALL_TAC] THEN
  REWRITE_TAC[
SIMPLE_IMAGE; 
IMAGE_ID] THEN
  REWRITE_TAC[GSYM(SPEC `1` 
SUM_OFFSET)] THEN
  W(MP_TAC o PART_MATCH (rhs o rand) 
SUM_UNION o lhs o snd) THEN
  ANTS_TAC THENL
   [REWRITE_TAC[
FINITE_NUMSEG; 
DISJOINT_NUMSEG] THEN ARITH_TAC;
    DISCH_THEN(SUBST1_TAC o SYM)] THEN
  MP_TAC(ISPECL [`\i. (x:real^N)$i * (y:real^N)$i`;
                 `1..dimindex(:N)`;
                 `k:num`] 
SUM_DELETE) THEN
  ASM_REWRITE_TAC[
IN_NUMSEG; 
FINITE_NUMSEG] THEN
  DISCH_THEN(SUBST1_TAC o SYM) THEN
  AP_THM_TAC THEN AP_TERM_TAC THEN
  REWRITE_TAC[
EXTENSION; 
IN_NUMSEG; 
IN_UNION; 
IN_DELETE] THEN ASM_ARITH_TAC);;
 
let DOT_PUSHIN = prove
 (`!k a b x y:real^M.
        dimindex(:M) + 1 = dimindex(:N) /\ 1 <= k /\ k <= dimindex(:N)
        ==> (pushin k a x:real^N) dot (pushin k b y) = x dot y + a * b`,
  REPEAT STRIP_TAC THEN
  MATCH_MP_TAC 
EQ_TRANS THEN
  EXISTS_TAC `(dropout k (pushin k a (x:real^M):real^N):real^M) dot
              (dropout k (pushin k b (y:real^M):real^N):real^M) +
              a * b` THEN
  CONJ_TAC THENL [ALL_TAC; ASM_SIMP_TAC[
DROPOUT_PUSHIN]] THEN
  ASM_SIMP_TAC[
DOT_DROPOUT] THEN
  MATCH_MP_TAC(REAL_RING
   `a':real = a /\ b' = b ==> x = x - a' * b' + a * b`) THEN
  ASM_SIMP_TAC[pushin; 
LAMBDA_BETA; 
LT_REFL]);;
 
let IN_SLICE = prove
 (`!s:real^N->bool y:real^M.
        dimindex(:M) + 1 = dimindex(:N) /\ 1 <= k /\ k <= dimindex(:N)
        ==> (y 
IN slice k t s <=> pushin k t y 
IN s)`,
 
let INTERVAL_INTER_HYPERPLANE = prove
 (`!k t a b:real^N.
        1 <= k /\ k <= dimindex(:N)
        ==> interval[a,b] 
INTER {x | x$k = t} =
                if a$k <= t /\ t <= b$k
                then interval[(lambda i. if i = k then t else a$i),
                              (lambda i. if i = k then t else b$i)]
                else {}`,
  REPEAT STRIP_TAC THEN
  REWRITE_TAC[
EXTENSION; 
IN_INTER; 
IN_INTERVAL; 
IN_ELIM_THM] THEN
  X_GEN_TAC `x:real^N` THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[] THENL
   [ALL_TAC; ASM_MESON_TAC[
NOT_IN_EMPTY]] THEN
  SIMP_TAC[
IN_INTERVAL; 
LAMBDA_BETA] THEN
  EQ_TAC THEN STRIP_TAC THENL [ASM_MESON_TAC[REAL_LE_ANTISYM]; ALL_TAC] THEN
  CONJ_TAC THENL [ALL_TAC; ASM_MESON_TAC[REAL_LE_ANTISYM]] THEN
  X_GEN_TAC `i:num` THEN STRIP_TAC THEN
  FIRST_X_ASSUM(MP_TAC o SPEC `i:num`) THEN ASM_REWRITE_TAC[] THEN
  COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN ASM_REAL_ARITH_TAC);;
 
let SLICE_INTERVAL = prove
 (`!k a b t. dimindex(:M) + 1 = dimindex(:N) /\
             1 <= k /\ k <= dimindex(:N)
             ==> slice k t (interval[a,b]) =
                 if a$k <= t /\ t <= b$k
                 then interval[(dropout k:real^N->real^M) a,dropout k b]
                 else {}`,
 
let SLICE_DIFF = prove
 (`!k a s t.
        dimindex(:M) + 1 = dimindex(:N) /\ 1 <= k /\ k <= dimindex(:N)
        ==> (slice k a:(real^N->bool)->(real^M->bool)) (s 
DIFF t) =
             (slice k a s) 
DIFF (slice k a t)`,
 
let SLICE_UNIV = prove
 (`!k a. dimindex(:M) + 1 = dimindex(:N) /\ 1 <= k /\ k <= dimindex(:N)
        ==> slice k a (:real^N) = (:real^M)`,
 
let SLICE_UNION = prove
 (`!k a s t.
        dimindex(:M) + 1 = dimindex(:N) /\ 1 <= k /\ k <= dimindex(:N)
        ==> (slice k a:(real^N->bool)->(real^M->bool)) (s 
UNION t) =
             (slice k a s) 
UNION (slice k a t)`,
 
let SLICE_INTER = prove
 (`!k a s t.
        dimindex(:M) + 1 = dimindex(:N) /\ 1 <= k /\ k <= dimindex(:N)
        ==> (slice k a:(real^N->bool)->(real^M->bool)) (s 
INTER t) =
             (slice k a s) 
INTER (slice k a t)`,
 
let CONVEX_SLICE = prove
 (`!k t s. dimindex(:M) < dimindex(:N) /\ convex s
           ==> convex((slice k t:(real^N->bool)->(real^M->bool)) s)`,
 
let COMPACT_SLICE = prove
 (`!k t s. dimindex(:M) < dimindex(:N) /\ compact s
           ==> compact((slice k t:(real^N->bool)->(real^M->bool)) s)`,
 
let CLOSED_SLICE = prove
 (`!k t s. dimindex(:M) + 1 = dimindex(:N) /\ 1 <= k /\ k <= dimindex(:N) /\
           closed s
           ==> closed((slice k t:(real^N->bool)->(real^M->bool)) s)`,
 
let OPEN_SLICE = prove
 (`!k t s. dimindex(:M) + 1 = dimindex(:N) /\ 1 <= k /\ k <= dimindex(:N) /\
           open s
           ==> open((slice k t:(real^N->bool)->(real^M->bool)) s)`,
 
let BOUNDED_SLICE = prove
 (`!k t s. dimindex(:M) + 1 = dimindex(:N) /\ 1 <= k /\ k <= dimindex(:N) /\
           bounded s
           ==> bounded((slice k t:(real^N->bool)->(real^M->bool)) s)`,
 
let SLICE_CBALL = prove
 (`!k t x r.
        dimindex(:M) + 1 = dimindex(:N) /\ 1 <= k /\ k <= dimindex(:N)
        ==> (slice k t:(real^N->bool)->(real^M->bool)) (cball(x,r)) =
                if abs(t - x$k) <= r
                then cball(dropout k x,sqrt(r pow 2 - (t - x$k) pow 2))
                else {}`,
 
let SLICE_BALL = prove
 (`!k t x r.
        dimindex(:M) + 1 = dimindex(:N) /\ 1 <= k /\ k <= dimindex(:N)
        ==> (slice k t:(real^N->bool)->(real^M->bool)) (ball(x,r)) =
                if abs(t - x$k) < r
                then ball(dropout k x,sqrt(r pow 2 - (t - x$k) pow 2))
                else {}`,
 
let FUBINI_CLOSED_INTERVAL = prove
 (`!k a b:real^N.
        dimindex(:M) + 1 = dimindex(:N) /\
        1 <= k /\ k <= dimindex(:N) /\
        a$k <= b$k
        ==> ((\t. measure (slice k t (interval[a,b]) :real^M->bool))
             
has_real_integral
             (measure(interval[a,b]))) (:real)`,
 
let FUBINI_SIMPLE_LEMMA = prove
 (`!k s:real^N->bool e.
        &0 < e /\
        dimindex(:M) + 1 = dimindex(:N) /\
        1 <= k /\ k <= dimindex(:N) /\
        bounded s /\ measurable s /\
        (!t. measurable(slice k t s:real^M->bool)) /\
        (\t. measure (slice k t s:real^M->bool)) 
real_integrable_on (:real)
        ==> 
real_integral(:real) (\t. measure (slice k t s :real^M->bool))
                <= measure s + e`,
  REPEAT STRIP_TAC THEN
  FIRST_ASSUM(MP_TAC o MATCH_MP 
BOUNDED_SUBSET_CLOSED_INTERVAL) THEN
  REWRITE_TAC[
LEFT_IMP_EXISTS_THM] THEN
  MAP_EVERY X_GEN_TAC [`a:real^N`; `b:real^N`] THEN DISCH_TAC THEN
  MP_TAC(ISPECL [`s:real^N->bool`; `a:real^N`; `b:real^N`; `e:real`]
        
MEASURABLE_OUTER_INTERVALS_BOUNDED_EXPLICIT_SPECIAL) THEN
  ASM_REWRITE_TAC[] THEN ANTS_TAC THENL
   [SUBGOAL_THEN `1 <= dimindex(:M)` MP_TAC THENL
     [REWRITE_TAC[
DIMINDEX_GE_1]; ASM_ARITH_TAC];
    ALL_TAC] THEN
  DISCH_THEN(X_CHOOSE_THEN `d:num->(real^N->bool)` STRIP_ASSUME_TAC) THEN
  SUBGOAL_THEN `!t n:num. measurable((slice k t:(real^N->bool)->real^M->bool)
                                     (d n))`
  ASSUME_TAC THENL
   [MAP_EVERY X_GEN_TAC [`t:real`; `n:num`] THEN
    FIRST_X_ASSUM(STRIP_ASSUME_TAC o CONJUNCT2 o SPEC `n:num`) THEN
    ASM_SIMP_TAC[
SLICE_INTERVAL] THEN
    MESON_TAC[
MEASURABLE_EMPTY; 
MEASURABLE_INTERVAL];
    ALL_TAC] THEN
  MATCH_MP_TAC 
REAL_LE_TRANS THEN
  EXISTS_TAC `measure(
UNIONS {d n | n 
IN (:num)}:real^N->bool)` THEN
  ASM_REWRITE_TAC[] THEN
  MP_TAC(ISPECL
       [`\n t. sum(0..n)
           (\m. measure((slice k t:(real^N->bool)->real^M->bool)
                       (d m)))`;
        `\t. measure((slice k t:(real^N->bool)->real^M->bool)
                   (
UNIONS {d n | n 
IN (:num)}))`; `(:real)`]
         
REAL_MONOTONE_CONVERGENCE_INCREASING_AE) THEN
  REWRITE_TAC[] THEN ANTS_TAC THENL
   [CONJ_TAC THENL
     [X_GEN_TAC `i:num` THEN MATCH_MP_TAC 
REAL_INTEGRABLE_SUM THEN
      ASM_REWRITE_TAC[
FINITE_NUMSEG] THEN X_GEN_TAC `j:num` THEN
      DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o CONJUNCT2 o SPEC `j:num`) THEN
      REWRITE_TAC[
LEFT_IMP_EXISTS_THM] THEN
      MAP_EVERY X_GEN_TAC [`u:real^N`; `v:real^N`] THEN STRIP_TAC THEN
      MP_TAC(ISPECL [`k:num`; `u:real^N`; `v:real^N`]
        
FUBINI_CLOSED_INTERVAL) THEN
      ASM_REWRITE_TAC[] THEN MESON_TAC[
real_integrable_on];
      ALL_TAC] THEN
    CONJ_TAC THENL
     [REPEAT STRIP_TAC THEN REWRITE_TAC[
SUM_CLAUSES_NUMSEG; 
LE_0] THEN
      REWRITE_TAC[
REAL_LE_ADDR] THEN MATCH_MP_TAC 
MEASURE_POS_LE THEN
      ASM_REWRITE_TAC[];
      ALL_TAC] THEN
    CONJ_TAC THENL
     [ALL_TAC;
      REWRITE_TAC[
real_bounded; 
FORALL_IN_GSPEC; 
IN_UNIV] THEN
      EXISTS_TAC `measure(interval[a:real^N,b])` THEN X_GEN_TAC `i:num` THEN
      W(MP_TAC o PART_MATCH (lhand o rand) 
REAL_INTEGRAL_SUM o
        rand o lhand o snd) THEN
      ANTS_TAC THENL
       [REWRITE_TAC[
FINITE_NUMSEG] THEN X_GEN_TAC `j:num` THEN DISCH_TAC THEN
        SUBGOAL_THEN `?u v. u$k <= v$k /\
                            (d:num->real^N->bool) j = interval[u,v]`
        STRIP_ASSUME_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
        ASM_REWRITE_TAC[] THEN REWRITE_TAC[
real_integrable_on] THEN
        EXISTS_TAC `measure(interval[u:real^N,v])` THEN
        MATCH_MP_TAC 
FUBINI_CLOSED_INTERVAL THEN ASM_REWRITE_TAC[];
        ALL_TAC] THEN
      DISCH_THEN SUBST1_TAC THEN MATCH_MP_TAC 
REAL_LE_TRANS THEN
      EXISTS_TAC `abs(sum(0..i) (\m. measure(d m:real^N->bool)))` THEN
      CONJ_TAC THENL
       [MATCH_MP_TAC 
REAL_EQ_IMP_LE THEN AP_TERM_TAC THEN
        MATCH_MP_TAC 
SUM_EQ_NUMSEG THEN
        X_GEN_TAC `j:num` THEN STRIP_TAC THEN REWRITE_TAC[] THEN
        MATCH_MP_TAC 
REAL_INTEGRAL_UNIQUE THEN
        SUBGOAL_THEN `?u v. u$k <= v$k /\
                            (d:num->real^N->bool) j = interval[u,v]`
        STRIP_ASSUME_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
        ASM_REWRITE_TAC[] THEN
        MATCH_MP_TAC 
FUBINI_CLOSED_INTERVAL THEN ASM_REWRITE_TAC[];
        ALL_TAC] THEN
      MATCH_MP_TAC(REAL_ARITH `&0 <= x /\ x <= a ==> abs x <= a`) THEN
      CONJ_TAC THENL
       [MATCH_MP_TAC 
SUM_POS_LE THEN REWRITE_TAC[
FINITE_NUMSEG] THEN
        ASM_MESON_TAC[
MEASURE_POS_LE; 
MEASURABLE_INTERVAL];
        ALL_TAC] THEN
      W(MP_TAC o PART_MATCH (rhs o rand) 
MEASURE_NEGLIGIBLE_UNIONS_IMAGE o
        lhand o snd) THEN
      ANTS_TAC THENL
       [ASM_SIMP_TAC[
FINITE_NUMSEG] THEN ASM_MESON_TAC[
MEASURABLE_INTERVAL];
        ALL_TAC] THEN
      DISCH_THEN(SUBST1_TAC o SYM) THEN MATCH_MP_TAC 
MEASURE_SUBSET THEN
      REWRITE_TAC[
MEASURABLE_INTERVAL] THEN CONJ_TAC THENL
       [MATCH_MP_TAC 
MEASURABLE_UNIONS THEN
        ASM_SIMP_TAC[
FINITE_NUMSEG; 
FINITE_IMAGE; 
FORALL_IN_IMAGE] THEN
        ASM_MESON_TAC[
MEASURABLE_INTERVAL];
        REWRITE_TAC[
UNIONS_SUBSET; 
FORALL_IN_IMAGE] THEN ASM_MESON_TAC[]]] THEN
    EXISTS_TAC
     `(
IMAGE (\i. (
interval_lowerbound(d i):real^N)$k) (:num)) 
UNION
      (
IMAGE (\i. (
interval_upperbound(d i):real^N)$k) (:num))` THEN
    CONJ_TAC THENL
     [MATCH_MP_TAC 
REAL_NEGLIGIBLE_COUNTABLE THEN
      SIMP_TAC[
COUNTABLE_UNION; 
COUNTABLE_IMAGE; 
NUM_COUNTABLE];
      ALL_TAC] THEN
    X_GEN_TAC `t:real` THEN
    REWRITE_TAC[
IN_DIFF; 
IN_UNION; 
IN_IMAGE] THEN
    GEN_REWRITE_TAC (LAND_CONV o TOP_DEPTH_CONV) [
IN_UNIV] THEN
    REWRITE_TAC[DE_MORGAN_THM; 
NOT_EXISTS_THM] THEN DISCH_TAC THEN
    MP_TAC(ISPEC `\n:num. (slice k t:(real^N->bool)->real^M->bool)
                          (d n)`
       
HAS_MEASURE_COUNTABLE_NEGLIGIBLE_UNIONS_BOUNDED) THEN
    ASM_REWRITE_TAC[
SLICE_UNIONS] THEN ANTS_TAC THENL
     [ALL_TAC;
      DISCH_THEN(MP_TAC o CONJUNCT2) THEN
      GEN_REWRITE_TAC (LAND_CONV o RATOR_CONV o LAND_CONV) [GSYM 
o_DEF] THEN
      REWRITE_TAC[GSYM 
REAL_SUMS; 
real_sums; 
FROM_INTER_NUMSEG] THEN
      REWRITE_TAC[
SIMPLE_IMAGE; GSYM 
IMAGE_o; 
o_DEF]] THEN
    CONJ_TAC THENL
     [ALL_TAC;
      MATCH_MP_TAC 
BOUNDED_SUBSET THEN
      EXISTS_TAC `(slice k t:(real^N->bool)->real^M->bool) (interval[a,b])` THEN
      CONJ_TAC THENL
       [ASM_SIMP_TAC[
SLICE_INTERVAL] THEN
        MESON_TAC[
BOUNDED_INTERVAL; 
BOUNDED_EMPTY];
        REWRITE_TAC[
UNIONS_SUBSET; 
FORALL_IN_GSPEC] THEN
        ASM_MESON_TAC[
SLICE_SUBSET]]] THEN
    MAP_EVERY X_GEN_TAC [`i:num`; `j:num`] THEN DISCH_TAC THEN
    FIRST_X_ASSUM(MP_TAC o SPECL [`i:num`; `j:num`]) THEN
    ASM_REWRITE_TAC[] THEN
    ASM_CASES_TAC `(d:num->real^N->bool) i = {}` THENL
     [ASM_REWRITE_TAC[
INTER_EMPTY; 
NEGLIGIBLE_EMPTY; 
SLICE_EMPTY];
      UNDISCH_TAC `~((d:num->real^N->bool) i = {})`] THEN
    ASM_CASES_TAC `(d:num->real^N->bool) j = {}` THENL
     [ASM_REWRITE_TAC[
INTER_EMPTY; 
NEGLIGIBLE_EMPTY; 
SLICE_EMPTY];
      UNDISCH_TAC `~((d:num->real^N->bool) j = {})`] THEN
    FIRST_ASSUM(fun th ->
      MAP_EVERY (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)
       [SPEC `i:num` th; SPEC `j:num` th]) THEN
    REWRITE_TAC[
LEFT_IMP_EXISTS_THM] THEN
    MAP_EVERY X_GEN_TAC [`w:real^N`; `x:real^N`] THEN STRIP_TAC THEN
    MAP_EVERY X_GEN_TAC [`u:real^N`; `v:real^N`] THEN STRIP_TAC THEN
    ASM_SIMP_TAC[
SLICE_INTERVAL; 
INTERVAL_NE_EMPTY] THEN
    DISCH_TAC THEN DISCH_TAC THEN
    REPEAT(COND_CASES_TAC THEN
           ASM_REWRITE_TAC[
INTER_EMPTY; 
NEGLIGIBLE_EMPTY]) THEN
    REWRITE_TAC[
INTER_INTERVAL; 
NEGLIGIBLE_INTERVAL; 
INTERVAL_EQ_EMPTY] THEN
    ONCE_REWRITE_TAC[TAUT `a /\ b /\ c <=> ~(a /\ b ==> ~c)`] THEN
    SIMP_TAC[
LAMBDA_BETA] THEN REWRITE_TAC[NOT_IMP] THEN
    DISCH_THEN(X_CHOOSE_THEN `l:num` STRIP_ASSUME_TAC) THEN
    SUBGOAL_THEN `~(l:num = k)` ASSUME_TAC THENL
     [FIRST_X_ASSUM(CONJUNCTS_THEN
       (fun th -> MP_TAC(SPEC `i:num` th) THEN MP_TAC(SPEC `j:num` th))) THEN
      ASM_SIMP_TAC[
INTERVAL_LOWERBOUND; 
INTERVAL_UPPERBOUND] THEN
      REWRITE_TAC[IMP_IMP] THEN ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
      REWRITE_TAC[] THEN DISCH_THEN SUBST_ALL_TAC THEN ASM_REAL_ARITH_TAC;
      ALL_TAC] THEN
    FIRST_ASSUM(DISJ_CASES_TAC o MATCH_MP (ARITH_RULE
     `~(l:num = k) ==> l < k \/ k < l`))
    THENL
     [EXISTS_TAC `l:num` THEN
      MATCH_MP_TAC(TAUT `a /\ (a ==> b) ==> a /\ b`) THEN
      CONJ_TAC THENL [ASM_ARITH_TAC; SIMP_TAC[dropout; 
LAMBDA_BETA]] THEN
      ASM_REWRITE_TAC[];
      ALL_TAC] THEN
    EXISTS_TAC `l - 1` THEN
    MATCH_MP_TAC(TAUT `a /\ (a ==> b) ==> a /\ b`) THEN
    CONJ_TAC THENL [ASM_ARITH_TAC; SIMP_TAC[dropout; 
LAMBDA_BETA]] THEN
    ASM_SIMP_TAC[ARITH_RULE `k < l ==> ~(l - 1 < k)`] THEN
    ASM_SIMP_TAC[
SUB_ADD];
    ALL_TAC] THEN
  STRIP_TAC THEN MATCH_MP_TAC 
REAL_LE_TRANS THEN EXISTS_TAC
   `
real_integral (:real)
        (\t. measure ((slice k t :(real^N->bool)->real^M->bool)
                      (
UNIONS {d n | n 
IN (:num)})))` THEN
  CONJ_TAC THENL
   [MATCH_MP_TAC 
REAL_INTEGRAL_LE THEN ASM_REWRITE_TAC[] THEN
    X_GEN_TAC `t:real` THEN DISCH_TAC THEN MATCH_MP_TAC 
MEASURE_SUBSET THEN
    ASM_SIMP_TAC[
SLICE_SUBSET; 
SLICE_UNIONS] THEN
    ONCE_REWRITE_TAC[
SIMPLE_IMAGE] THEN REWRITE_TAC[GSYM 
IMAGE_o] THEN
    ONCE_REWRITE_TAC[GSYM 
SIMPLE_IMAGE] THEN
    MATCH_MP_TAC 
MEASURABLE_COUNTABLE_UNIONS_BOUNDED THEN
    ASM_REWRITE_TAC[
o_THM] THEN
    MATCH_MP_TAC 
BOUNDED_SUBSET THEN
    EXISTS_TAC `(slice k t:(real^N->bool)->real^M->bool) (interval[a,b])` THEN
    CONJ_TAC THENL
     [ASM_SIMP_TAC[
SLICE_INTERVAL] THEN
      MESON_TAC[
BOUNDED_INTERVAL; 
BOUNDED_EMPTY];
      REWRITE_TAC[
UNIONS_SUBSET; 
FORALL_IN_GSPEC] THEN
      ASM_MESON_TAC[
SLICE_SUBSET]];
    MATCH_MP_TAC 
REAL_EQ_IMP_LE THEN
    MATCH_MP_TAC(ISPEC `sequentially` 
REALLIM_UNIQUE) THEN
    EXISTS_TAC `\n. 
real_integral (:real)
       (\t. sum (0..n) (\m. measure((slice k t:(real^N->bool)->real^M->bool)
                         (d m))))` THEN
    ASM_REWRITE_TAC[
TRIVIAL_LIMIT_SEQUENTIALLY] THEN
    MP_TAC(ISPEC `d:num->(real^N->bool)`
     
HAS_MEASURE_COUNTABLE_NEGLIGIBLE_UNIONS_BOUNDED) THEN
    ANTS_TAC THENL
     [ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
       [ASM_MESON_TAC[
MEASURABLE_INTERVAL]; ALL_TAC] THEN
      MATCH_MP_TAC 
BOUNDED_SUBSET THEN EXISTS_TAC `interval[a:real^N,b]` THEN
      REWRITE_TAC[
BOUNDED_INTERVAL; 
UNIONS_SUBSET; 
IN_ELIM_THM] THEN
      ASM_MESON_TAC[];
      ALL_TAC] THEN
    ASM_REWRITE_TAC[] THEN
    GEN_REWRITE_TAC (LAND_CONV o RATOR_CONV o LAND_CONV) [GSYM 
o_DEF] THEN
    REWRITE_TAC[GSYM 
REAL_SUMS] THEN
    REWRITE_TAC[
real_sums; 
FROM_INTER_NUMSEG] THEN
    MATCH_MP_TAC EQ_IMP THEN AP_THM_TAC THEN AP_THM_TAC THEN
    AP_TERM_TAC THEN GEN_REWRITE_TAC I [
FUN_EQ_THM] THEN
    X_GEN_TAC `i:num` THEN REWRITE_TAC[] THEN
    W(MP_TAC o PART_MATCH (lhand o rand) 
REAL_INTEGRAL_SUM o rand o snd) THEN
    ANTS_TAC THENL
     [REWRITE_TAC[
FINITE_NUMSEG] THEN X_GEN_TAC `j:num` THEN DISCH_TAC THEN
      SUBGOAL_THEN `?u v. u$k <= v$k /\
                          (d:num->real^N->bool) j = interval[u,v]`
      STRIP_ASSUME_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
      ASM_REWRITE_TAC[] THEN REWRITE_TAC[
real_integrable_on] THEN
      EXISTS_TAC `measure(interval[u:real^N,v])` THEN
      MATCH_MP_TAC 
FUBINI_CLOSED_INTERVAL THEN ASM_REWRITE_TAC[];
      ALL_TAC] THEN
    DISCH_THEN SUBST1_TAC THEN MATCH_MP_TAC 
SUM_EQ_NUMSEG THEN
    X_GEN_TAC `j:num` THEN STRIP_TAC THEN REWRITE_TAC[] THEN
    CONV_TAC SYM_CONV THEN MATCH_MP_TAC 
REAL_INTEGRAL_UNIQUE THEN
    SUBGOAL_THEN `?u v. u$k <= v$k /\
                          (d:num->real^N->bool) j = interval[u,v]`
    STRIP_ASSUME_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
    ASM_REWRITE_TAC[] THEN
    MATCH_MP_TAC 
FUBINI_CLOSED_INTERVAL THEN ASM_REWRITE_TAC[]]);;
 
let FUBINI_SIMPLE = prove
 (`!k s:real^N->bool.
        dimindex(:M) + 1 = dimindex(:N) /\
        1 <= k /\ k <= dimindex(:N) /\
        bounded s /\
        measurable s /\
        (!t. measurable(slice k t s :real^M->bool)) /\
        (\t. measure (slice k t s :real^M->bool)) 
real_integrable_on (:real)
        ==> measure s =
              
real_integral(:real)(\t. measure (slice k t s :real^M->bool))`,
 
let FUBINI_SIMPLE_ALT = prove
 (`!k s:real^N->bool.
        dimindex(:M) + 1 = dimindex(:N) /\
        1 <= k /\ k <= dimindex(:N) /\
        bounded s /\
        measurable s /\
        (!t. measurable(slice k t s :real^M->bool)) /\
        ((\t. measure (slice k t s :real^M->bool)) 
has_real_integral B) (:real)
        ==> measure s = B`,
 
let FUBINI_SIMPLE_CONVEX = prove
 (`!k s:real^N->bool.
        dimindex(:M) + 1 = dimindex(:N) /\
        1 <= k /\ k <= dimindex(:N) /\
        bounded s /\ convex s /\
        ((\t. measure (slice k t s :real^M->bool)) 
has_real_integral B) (:real)
        ==> measure s = B`,
 
let FUBINI_SIMPLE_OPEN_STRONG = prove
 (`!k s:real^N->bool.
        dimindex(:M) + 1 = dimindex(:N) /\
        1 <= k /\ k <= dimindex(:N) /\
        bounded s /\ open s /\
        ((\t. measure (slice k t s :real^M->bool)) 
has_real_integral B) (:real)
        ==> measurable s /\ measure s = B`,
 
let FUBINI_SIMPLE_OPEN = prove
 (`!k s:real^N->bool.
        dimindex(:M) + 1 = dimindex(:N) /\
        1 <= k /\ k <= dimindex(:N) /\
        bounded s /\ open s /\
        ((\t. measure (slice k t s :real^M->bool)) 
has_real_integral B) (:real)
        ==> measure s = B`,
 
let OSTROWSKI_THEOREM = prove
 (`!f:real^M->real^N B s.
        (!x y. f(x + y) = f(x) + f(y)) /\
        (!x. x 
IN s ==> norm(f x) <= B) /\
        measurable s /\ &0 < measure s
        ==> linear f`,
  REPEAT GEN_TAC THEN
  REPLICATE_TAC 2 (DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
  DISCH_THEN(X_CHOOSE_THEN `d:real` STRIP_ASSUME_TAC o
    MATCH_MP 
STEINHAUS) THEN
  SUBGOAL_THEN `!x y. (f:real^M->real^N)(x - y) = f x - f y` ASSUME_TAC THENL
   [ASM_MESON_TAC[VECTOR_ARITH `x - y:real^M = z <=> x = y + z`];
    ALL_TAC] THEN
  SUBGOAL_THEN `!n x. &n % (f:real^M->real^N) x = f(&n % x)` ASSUME_TAC THENL
   [INDUCT_TAC THENL
     [ASM_MESON_TAC[
VECTOR_SUB_REFL; 
VECTOR_MUL_LZERO];
      ASM_REWRITE_TAC[GSYM 
REAL_OF_NUM_SUC; 
VECTOR_ADD_RDISTRIB] THEN
      REWRITE_TAC[
VECTOR_MUL_LID]];
    ALL_TAC] THEN
  MATCH_MP_TAC 
CONTINUOUS_ADDITIVE_IMP_LINEAR THEN ASM_REWRITE_TAC[] THEN
  SUBGOAL_THEN `!x. norm(x) < d ==> norm((f:real^M->real^N) x) <= &2 * B`
  ASSUME_TAC THENL
   [X_GEN_TAC `z:real^M` THEN DISCH_TAC THEN
    FIRST_X_ASSUM(MP_TAC o SPEC `z:real^M` o GEN_REWRITE_RULE I [
SUBSET]) THEN
    ASM_REWRITE_TAC[
IN_BALL_0] THEN SPEC_TAC(`z:real^M`,`z:real^M`) THEN
    ASM_REWRITE_TAC[
FORALL_IN_GSPEC] THEN REWRITE_TAC[
IN_ELIM_THM] THEN
    REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN(ANTE_RES_THEN MP_TAC)) THEN
    CONV_TAC NORM_ARITH;
    ALL_TAC] THEN
  REWRITE_TAC[
continuous_on; 
IN_UNIV; dist] THEN
  MAP_EVERY X_GEN_TAC [`x:real^M`; `e:real`] THEN DISCH_TAC THEN
  MP_TAC(SPEC `e:real` 
REAL_ARCH) THEN ASM_REWRITE_TAC[] THEN
  DISCH_THEN(X_CHOOSE_THEN `n:num` MP_TAC o SPEC `max (&1) (&2 * B)`) THEN
  ASM_CASES_TAC `n = 0` THEN ASM_REWRITE_TAC[] THENL
   [REAL_ARITH_TAC; DISCH_TAC] THEN
  EXISTS_TAC `d / &n` THEN
  ASM_SIMP_TAC[
REAL_LT_DIV; 
REAL_OF_NUM_LT; 
LE_1] THEN
  X_GEN_TAC `y:real^M` THEN DISCH_TAC THEN
  SUBGOAL_THEN `norm(&n % (f:real^M->real^N)(y - x)) <= &2 * B` MP_TAC THENL
   [ASM_REWRITE_TAC[] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
    SIMP_TAC[
NORM_MUL; 
REAL_ABS_NUM] THEN ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
    ASM_SIMP_TAC[GSYM 
REAL_LT_RDIV_EQ; 
REAL_OF_NUM_LT; 
LE_1];
    SIMP_TAC[
NORM_MUL; 
REAL_ABS_NUM] THEN ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
    ASM_SIMP_TAC[GSYM 
REAL_LE_RDIV_EQ; 
REAL_OF_NUM_LT; 
LE_1] THEN
    MATCH_MP_TAC(REWRITE_RULE[
IMP_CONJ_ALT] 
REAL_LET_TRANS) THEN
    ASM_SIMP_TAC[
REAL_LT_LDIV_EQ; 
REAL_OF_NUM_LT; 
LE_1] THEN
    ASM_REAL_ARITH_TAC]);;
 
let REAL_CONTINUOUS_ADDITIVE_IMP_LINEAR_INTERVAL = prove
 (`!f b. (f ---> &0) (atreal (&0) within {x | &0 <= x}) /\
         (!x y. &0 <= x /\ &0 <= y /\ x + y <= b ==> f(x + y) = f(x) + f(y))
         ==> !a x. &0 <= x /\ x <= b /\
                   &0 <= a * x /\ a * x <= b
                   ==> f(a * x) = a * f(x)`,
  SUBGOAL_THEN
   `!f. (f ---> &0) (atreal (&0) within {x | &0 <= x}) /\
        (!x y. &0 <= x /\ &0 <= y /\ x + y <= &1 ==> f(x + y) = f(x) + f(y))
        ==> !a x. &0 <= x /\ x <= &1 /\ &0 <= a * x /\ a * x <= &1
                  ==> f(a * x) = a * f(x)`
  ASSUME_TAC THENL
   [SUBGOAL_THEN
     `!f. f 
real_continuous_on real_interval[&0,&1] /\
          (!x y. &0 <= x /\ &0 <= y /\ x + y <= &1 ==> f(x + y) = f(x) + f(y))
          ==> !a x. &0 <= x /\ x <= &1 /\ &0 <= a * x /\ a * x <= &1
                    ==> f(a * x) = a * f(x)`
    (fun th -> GEN_TAC THEN STRIP_TAC THEN MATCH_MP_TAC th) THENL
     [REPEAT STRIP_TAC THEN
      MP_TAC(ISPEC `f:real->real` 
REAL_CONTINUOUS_ADDITIVE_EXTEND) THEN
      ASM_REWRITE_TAC[
IN_REAL_INTERVAL] THEN
      DISCH_THEN(X_CHOOSE_THEN `g:real->real` STRIP_ASSUME_TAC) THEN
      MP_TAC(ISPEC `g:real->real` 
REAL_CONTINUOUS_ADDITIVE_IMP_LINEAR) THEN
      ASM_MESON_TAC[];
      ASM_REWRITE_TAC[
real_continuous_on; 
IN_REAL_INTERVAL] THEN
      X_GEN_TAC `x:real` THEN STRIP_TAC THEN
      X_GEN_TAC `e:real` THEN DISCH_TAC THEN
      FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [
REALLIM_WITHINREAL]) THEN
      DISCH_THEN(MP_TAC o SPEC `e:real`) THEN
      ASM_REWRITE_TAC[
REAL_SUB_RZERO] THEN REWRITE_TAC[
IN_REAL_INTERVAL] THEN
      DISCH_THEN(X_CHOOSE_THEN `d:real` STRIP_ASSUME_TAC) THEN
      EXISTS_TAC `d:real` THEN ASM_SIMP_TAC[
REAL_LT_MUL] THEN
      X_GEN_TAC `y:real` THEN STRIP_TAC THEN
      REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC
       (REAL_ARITH `y = x \/ y < x \/ x < y`) THENL
       [ASM_REWRITE_TAC[
REAL_SUB_REFL; 
REAL_ABS_NUM];
        SUBGOAL_THEN `(f:real->real)(y + (x - y)) = f(y) + f(x - y)`
        MP_TAC THENL
         [FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REAL_ARITH_TAC;
          REWRITE_TAC[
REAL_SUB_ADD2] THEN DISCH_THEN SUBST1_TAC THEN
          REWRITE_TAC[
REAL_ADD_SUB2; 
REAL_ABS_NEG] THEN
          FIRST_X_ASSUM MATCH_MP_TAC THEN
          REWRITE_TAC[
IN_ELIM_THM] THEN ASM_REAL_ARITH_TAC];
        SUBGOAL_THEN `(f:real->real)(x + (y - x)) = f(x) + f(y - x)`
        MP_TAC THENL
         [FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REAL_ARITH_TAC;
          REWRITE_TAC[
REAL_SUB_ADD2] THEN DISCH_THEN SUBST1_TAC THEN
          REWRITE_TAC[
REAL_ADD_SUB] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
          REWRITE_TAC[
IN_ELIM_THM] THEN ASM_REAL_ARITH_TAC]]];
    REPEAT GEN_TAC THEN STRIP_TAC THEN REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC
     (REAL_ARITH `b < &0 \/ b = &0 \/ &0 < b`)
    THENL
     [ASM_REAL_ARITH_TAC;
      ASM_SIMP_TAC[REAL_ARITH
       `a <= x /\ x <= a /\ a <= y /\ y <= a <=> x = a /\ y = a`] THEN
      FIRST_X_ASSUM(MP_TAC o SPECL [`&0`; `&0`]) THEN
      ASM_REWRITE_TAC[REAL_ADD_LID; 
REAL_LE_REFL] THEN CONV_TAC REAL_RING;
      ALL_TAC] THEN
    FIRST_X_ASSUM(MP_TAC o ISPEC `(\x. f(b * x)):real->real`) THEN
    REWRITE_TAC[] THEN ANTS_TAC THENL
     [ALL_TAC;
      MATCH_MP_TAC 
MONO_FORALL THEN X_GEN_TAC `a:real` THEN
      DISCH_THEN(fun th -> X_GEN_TAC `x:real` THEN STRIP_TAC THEN
                           MP_TAC(ISPEC `x / b:real` th)) THEN
      ASM_SIMP_TAC[REAL_FIELD `&0 < b ==> b * a * x / b = a * x`;
                   
REAL_DIV_LMUL; 
REAL_LT_IMP_NZ] THEN
      DISCH_THEN MATCH_MP_TAC THEN
      REWRITE_TAC[REAL_ARITH `a * x / b:real = (a * x) / b`] THEN
      ASM_SIMP_TAC[
REAL_LE_RDIV_EQ; 
REAL_LE_LDIV_EQ] THEN
      ASM_REAL_ARITH_TAC] THEN
    CONJ_TAC THENL
     [ALL_TAC;
      REPEAT STRIP_TAC THEN REWRITE_TAC[REAL_ADD_LDISTRIB] THEN
      FIRST_X_ASSUM MATCH_MP_TAC THEN
      ASM_SIMP_TAC[REAL_ARITH `b * x + b * y <= b <=> &0 <= b * (&1 - (x + y))`;
                   
REAL_LE_MUL; 
REAL_LT_IMP_LE; 
REAL_SUB_LE]] THEN
    REWRITE_TAC[
REALLIM_WITHINREAL] THEN X_GEN_TAC `e:real` THEN DISCH_TAC THEN
    FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [
REALLIM_WITHINREAL]) THEN
    DISCH_THEN(MP_TAC o SPEC `e:real`) THEN ASM_REWRITE_TAC[
REAL_SUB_RZERO] THEN
    REWRITE_TAC[
REAL_SUB_RZERO; 
IN_ELIM_THM] THEN
    DISCH_THEN(X_CHOOSE_THEN `d:real` STRIP_ASSUME_TAC) THEN
    EXISTS_TAC `d / b:real` THEN ASM_SIMP_TAC[
REAL_LT_DIV] THEN
    REPEAT STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
    ASM_SIMP_TAC[
REAL_LE_MUL; 
REAL_LT_IMP_LE; 
REAL_ABS_MUL] THEN
    ASM_SIMP_TAC[REAL_ARITH `&0 < b ==> abs b * x = x * b`] THEN
    ASM_SIMP_TAC[
REAL_LT_MUL; GSYM 
REAL_LT_RDIV_EQ]]);;
 
let BERNSTEIN_LEMMA = prove
 (`!n x. sum(0..n) (\k. (&k - &n * x) pow 2 * bernstein n k x) =
         &n * x * (&1 - x)`,
  REPEAT STRIP_TAC THEN
  SUBGOAL_THEN
    `!x y. sum(0..n) (\k. &(binom(n,k)) * x pow k * y pow (n - k)) =
           (x + y) pow n`
  (LABEL_TAC "0") THENL [ASM_REWRITE_TAC[
REAL_BINOMIAL_THEOREM]; ALL_TAC] THEN
  SUBGOAL_THEN
   `!x y. sum(0..n) (\k. &k * &(binom(n,k)) * x pow (k - 1) * y pow (n - k)) =
          &n * (x + y) pow (n - 1)`
  (LABEL_TAC "1") THENL
   [REPEAT GEN_TAC THEN MATCH_MP_TAC 
REAL_DERIVATIVE_UNIQUE_ATREAL THEN
    MAP_EVERY EXISTS_TAC
     [`\x. sum(0..n) (\k. &(binom(n,k)) * x pow k * y pow (n - k))`;
      `x:real`] THEN
    CONJ_TAC THENL
     [MATCH_MP_TAC 
HAS_REAL_DERIVATIVE_SUM THEN REWRITE_TAC[
FINITE_NUMSEG];
      ASM_REWRITE_TAC[]] THEN
    REPEAT STRIP_TAC THEN REAL_DIFF_TAC THEN CONV_TAC REAL_RING;
    ALL_TAC] THEN
  SUBGOAL_THEN
   `!x y. sum(0..n)
        (\k. &k * &(k - 1) * &(binom(n,k)) * x pow (k - 2) * y pow (n - k)) =
          &n * &(n - 1) * (x + y) pow (n - 2)`
  (LABEL_TAC "2") THENL
   [REPEAT GEN_TAC THEN MATCH_MP_TAC 
REAL_DERIVATIVE_UNIQUE_ATREAL THEN
    MAP_EVERY EXISTS_TAC
     [`\x. sum(0..n) (\k. &k * &(binom(n,k)) * x pow (k - 1) * y pow (n - k))`;
      `x:real`] THEN
    CONJ_TAC THENL
     [MATCH_MP_TAC 
HAS_REAL_DERIVATIVE_SUM THEN REWRITE_TAC[
FINITE_NUMSEG];
      ASM_REWRITE_TAC[]] THEN
    REPEAT STRIP_TAC THEN REAL_DIFF_TAC THEN
    REWRITE_TAC[ARITH_RULE `n - 1 - 1 = n - 2`] THEN CONV_TAC REAL_RING;
    ALL_TAC] THEN
  REWRITE_TAC[REAL_ARITH
   `(a - b) pow 2 * x =
    a * (a - &1) * x + (&1 - &2 * b) * a * x + b * b * x`] THEN
  REWRITE_TAC[
SUM_ADD_NUMSEG; 
SUM_LMUL; 
SUM_BERNSTEIN] THEN
  SUBGOAL_THEN `sum(0..n) (\k. &k * bernstein n k x) = &n * x` SUBST1_TAC THENL
   [REMOVE_THEN "1" (MP_TAC o SPECL [`x:real`; `&1 - x`]) THEN
    REWRITE_TAC[
REAL_SUB_ADD2; 
REAL_POW_ONE; bernstein; 
REAL_MUL_RID] THEN
    DISCH_THEN(SUBST1_TAC o SYM) THEN REWRITE_TAC[GSYM 
SUM_RMUL] THEN
    MATCH_MP_TAC 
SUM_EQ_NUMSEG THEN X_GEN_TAC `k:num` THEN STRIP_TAC THEN
    REWRITE_TAC[REAL_ARITH
     `(k * b * xk * y) * x:real = k * b * (x * xk) * y`] THEN
    REWRITE_TAC[GSYM(CONJUNCT2 
real_pow)] THEN
    DISJ_CASES_TAC(ARITH_RULE `k = 0 \/ SUC(k - 1) = k`) THEN
    ASM_REWRITE_TAC[
REAL_MUL_LZERO];
    ALL_TAC] THEN
  SUBGOAL_THEN
  `sum(0..n) (\k. &k * (&k - &1) * bernstein n k x) = &n * (&n - &1) * x pow 2`
  SUBST1_TAC THENL [ALL_TAC; CONV_TAC REAL_RING] THEN
  REMOVE_THEN "2" (MP_TAC o SPECL [`x:real`; `&1 - x`]) THEN
  REWRITE_TAC[
REAL_SUB_ADD2; 
REAL_POW_ONE; bernstein; 
REAL_MUL_RID] THEN
  ASM_CASES_TAC `n = 0` THEN
  ASM_REWRITE_TAC[
SUM_SING_NUMSEG; 
REAL_MUL_LZERO] THEN
  ASM_SIMP_TAC[GSYM 
REAL_OF_NUM_SUB; 
LE_1; REAL_MUL_ASSOC] THEN
  DISCH_THEN(SUBST1_TAC o SYM) THEN REWRITE_TAC[GSYM 
SUM_RMUL] THEN
  MATCH_MP_TAC 
SUM_EQ_NUMSEG THEN X_GEN_TAC `k:num` THEN STRIP_TAC THEN
  REWRITE_TAC[REAL_ARITH `((((k * k1) * b) * xk) * y) * x2:real =
                            k * k1 * b * y * (x2 * xk)`] THEN
  REWRITE_TAC[GSYM 
REAL_POW_ADD; GSYM REAL_MUL_ASSOC] THEN
  REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC
   (ARITH_RULE `k = 0 \/ k = 1 \/ 1 <= k /\ 2 + k - 2 = k`) THEN
  ASM_REWRITE_TAC[
REAL_MUL_LZERO; REAL_MUL_LID; 
SUB_REFL; 
REAL_SUB_REFL] THEN
  ASM_SIMP_TAC[GSYM 
REAL_OF_NUM_SUB] THEN REWRITE_TAC[
REAL_MUL_AC]);;
 
let STONE_WEIERSTRASS_ALT = prove
 (`!(P:(real^N->real)->bool) (s:real^N->bool).
        compact s /\
        (!c. P(\x. c)) /\
        (!f g. P(f) /\ P(g) ==> P(\x. f x + g x)) /\
        (!f g. P(f) /\ P(g) ==> P(\x. f x * g x)) /\
        (!x y. x 
IN s /\ y 
IN s /\ ~(x = y)
               ==> ?f. (!x. x 
IN s ==> f 
real_continuous (at x within s)) /\
                       P(f) /\ ~(f x = f y))
        ==> !f e. (!x. x 
IN s ==> f 
real_continuous (at x within s)) /\ &0 < e
                  ==> ?g. P(g) /\ !x. x 
IN s ==> abs(f x - g x) < e`,
  REPEAT GEN_TAC THEN STRIP_TAC THEN MAP_EVERY ABBREV_TAC
   [`C = \f. !x:real^N. x 
IN s ==> f 
real_continuous at x within s`;
    `A = \f. C f /\
             !e. &0 < e
               ==> ?g. P(g) /\ !x:real^N. x 
IN s ==> abs(f x - g x) < e`] THEN
  SUBGOAL_THEN `!f:real^N->real. C(f) ==> A(f)` MP_TAC THENL
   [ALL_TAC; MAP_EVERY EXPAND_TAC ["A";
 
let STONE_WEIERSTRASS = prove
 (`!(P:(real^N->real)->bool) (s:real^N->bool).
        compact s /\
        (!f. P(f) ==> !x. x 
IN s ==> f 
real_continuous (at x within s)) /\
        (!c. P(\x. c)) /\
        (!f g. P(f) /\ P(g) ==> P(\x. f x + g x)) /\
        (!f g. P(f) /\ P(g) ==> P(\x. f x * g x)) /\
        (!x y. x 
IN s /\ y 
IN s /\ ~(x = y) ==> ?f. P(f) /\ ~(f x = f y))
        ==> !f e. (!x. x 
IN s ==> f 
real_continuous (at x within s)) /\ &0 < e
                  ==> ?g. P(g) /\ !x. x 
IN s ==> abs(f x - g x) < e`,
  REPEAT GEN_TAC THEN STRIP_TAC THEN
  MATCH_MP_TAC 
STONE_WEIERSTRASS_ALT THEN ASM_SIMP_TAC[] THEN
  MAP_EVERY X_GEN_TAC [`x:real^N`; `y:real^N`] THEN STRIP_TAC THEN
  FIRST_X_ASSUM(MP_TAC o SPECL [`x:real^N`; `y:real^N`]) THEN
  ASM_REWRITE_TAC[] THEN MATCH_MP_TAC 
MONO_EXISTS THEN ASM_MESON_TAC[]);;
 
let REAL_STONE_WEIERSTRASS = prove
 (`!P s. 
real_compact s /\
         (!f. P f ==> f 
real_continuous_on s) /\
         (!c. P (\x. c)) /\
         (!f g. P f /\ P g ==> P (\x. f x + g x)) /\
         (!f g. P f /\ P g ==> P (\x. f x * g x)) /\
         (!x y. x 
IN s /\ y 
IN s /\ ~(x = y) ==> ?f. P f /\ ~(f x = f y))
         ==> !f e. f 
real_continuous_on s /\ &0 < e
                   ==> ?g. P g /\ !x. x 
IN s ==> abs(f x - g x) < e`,
  REPEAT GEN_TAC THEN STRIP_TAC THEN
  MATCH_MP_TAC 
REAL_STONE_WEIERSTRASS_ALT THEN ASM_SIMP_TAC[] THEN
  MAP_EVERY X_GEN_TAC [`x:real`; `y:real`] THEN STRIP_TAC THEN
  FIRST_X_ASSUM(MP_TAC o SPECL [`x:real`; `y:real`]) THEN
  ASM_REWRITE_TAC[] THEN MATCH_MP_TAC 
MONO_EXISTS THEN ASM_MESON_TAC[]);;
 
let COMPLEX_STONE_WEIERSTRASS_ALT = prove
 (`!P s. compact s /\
         (!c. P (\x. c)) /\
         (!f. P f ==> P(\x. cnj(f x))) /\
         (!f g. P f /\ P g ==> P (\x. f x + g x)) /\
         (!f g. P f /\ P g ==> P (\x. f x * g x)) /\
         (!x y. x 
IN s /\ y 
IN s /\ ~(x = y)
                ==> ?f. P f /\ f 
continuous_on s /\ ~(f x = f y))
         ==> !f:real^N->complex e.
                f 
continuous_on s /\ &0 < e
                ==> ?g. P g /\ !x. x 
IN s ==> norm(f x - g x) < e`,
  REPEAT GEN_TAC THEN STRIP_TAC THEN
  SUBGOAL_THEN `!f. P f ==> P(\x:real^N. Cx(Re(f x)))` ASSUME_TAC THENL
   [ASM_SIMP_TAC[
CX_RE_CNJ; SIMPLE_COMPLEX_ARITH
     `x / Cx(&2) = inv(Cx(&2)) * x`];
    ALL_TAC] THEN
  SUBGOAL_THEN `!f. P f ==> P(\x:real^N. Cx(Im(f x)))` ASSUME_TAC THENL
   [ASM_SIMP_TAC[
CX_IM_CNJ; SIMPLE_COMPLEX_ARITH
     `x - y = x + --Cx(&1) * y /\ x / Cx(&2) = inv(Cx(&2)) * x`] THEN
    REPEAT STRIP_TAC THEN REPEAT(FIRST_ASSUM MATCH_MP_TAC ORELSE CONJ_TAC) THEN
    ASM_SIMP_TAC[];
    ALL_TAC] THEN
  MP_TAC(ISPECL [`\x. x 
IN {Re o f | P (f:real^N->complex)}`; `s:real^N->bool`]
        
STONE_WEIERSTRASS_ALT) THEN
  REWRITE_TAC[
IMP_CONJ; 
RIGHT_FORALL_IMP_THM; 
FORALL_IN_GSPEC] THEN
  REWRITE_TAC[
EXISTS_IN_GSPEC; IMP_IMP; GSYM 
CONJ_ASSOC] THEN ANTS_TAC THENL
   [ASM_REWRITE_TAC[IMP_IMP; 
RIGHT_IMP_FORALL_THM; 
IN_ELIM_THM] THEN
    REPEAT CONJ_TAC THENL
     [X_GEN_TAC `c:real` THEN EXISTS_TAC `\x:real^N. Cx(c)` THEN
      ASM_REWRITE_TAC[
FUN_EQ_THM; 
o_THM; 
RE_CX];
      MAP_EVERY X_GEN_TAC [`f:real^N->complex`; `g:real^N->complex`] THEN
      DISCH_TAC THEN EXISTS_TAC `(\x. f x + g x):real^N->complex` THEN
      ASM_SIMP_TAC[
o_THM; 
RE_ADD; 
FUN_EQ_THM];
      MAP_EVERY X_GEN_TAC [`f:real^N->complex`; `g:real^N->complex`] THEN
      STRIP_TAC THEN
      EXISTS_TAC `\x:real^N. Cx(Re(f x)) * Cx(Re(g x))` THEN
      ASM_SIMP_TAC[
FUN_EQ_THM; 
RE_CX; 
o_THM; 
RE_MUL_CX];
      MAP_EVERY X_GEN_TAC [`x:real^N`; `y:real^N`] THEN STRIP_TAC THEN
      FIRST_X_ASSUM(MP_TAC o SPECL  [`x:real^N`; `y:real^N`]) THEN
      ASM_REWRITE_TAC[
LEFT_IMP_EXISTS_THM] THEN
      X_GEN_TAC `f:real^N->complex` THEN
      REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
      GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [
COMPLEX_EQ] THEN
      REWRITE_TAC[DE_MORGAN_THM] THEN STRIP_TAC THENL
       [EXISTS_TAC `\x:real^N. Re(f x)` THEN ASM_REWRITE_TAC[
o_DEF] THEN
        CONJ_TAC THENL
         [ALL_TAC; EXISTS_TAC `f:real^N->complex` THEN ASM_REWRITE_TAC[]];
        EXISTS_TAC `\x:real^N. Im(f x)` THEN ASM_REWRITE_TAC[
o_DEF] THEN
        CONJ_TAC THENL
         [ALL_TAC;
          EXISTS_TAC `\x:real^N. Cx(Im(f x))` THEN ASM_SIMP_TAC[
RE_CX]]] THEN
      X_GEN_TAC `a:real^N` THEN DISCH_TAC THEN REWRITE_TAC[GSYM 
o_DEF] THEN
      MATCH_MP_TAC 
REAL_CONTINUOUS_CONTINUOUS_WITHIN_COMPOSE THEN
      SIMP_TAC[
REAL_CONTINUOUS_COMPLEX_COMPONENTS_AT;
               
REAL_CONTINUOUS_AT_WITHIN] THEN
      ASM_MESON_TAC[
CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN]];
    DISCH_THEN(LABEL_TAC "*") THEN X_GEN_TAC `f:real^N->complex` THEN
    DISCH_TAC THEN X_GEN_TAC `e:real` THEN DISCH_TAC THEN
    REMOVE_THEN "*"
     (fun th -> MP_TAC(ISPEC `Re o (f:real^N->complex)` th) THEN
                MP_TAC(ISPEC `Im o (f:real^N->complex)` th)) THEN
    MATCH_MP_TAC(TAUT `(p1 /\ p2) /\ (q1 /\ q2 ==> r)
                       ==> (p1 ==> q1) ==> (p2 ==> q2) ==> r`) THEN
    CONJ_TAC THENL
     [CONJ_TAC THEN X_GEN_TAC `a:real^N` THEN DISCH_TAC THEN
      MATCH_MP_TAC 
REAL_CONTINUOUS_CONTINUOUS_WITHIN_COMPOSE THEN
      SIMP_TAC[
REAL_CONTINUOUS_COMPLEX_COMPONENTS_AT;
               
REAL_CONTINUOUS_AT_WITHIN] THEN
      ASM_MESON_TAC[
CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN];
      ALL_TAC] THEN
    REWRITE_TAC[
AND_FORALL_THM] THEN
    DISCH_THEN(MP_TAC o SPEC `e / &2`) THEN
    ASM_REWRITE_TAC[
REAL_HALF; 
o_THM] THEN
    DISCH_THEN(CONJUNCTS_THEN2
     (X_CHOOSE_THEN `g:real^N->complex` STRIP_ASSUME_TAC)
     (X_CHOOSE_THEN `h:real^N->complex` STRIP_ASSUME_TAC)) THEN
    EXISTS_TAC `\x:real^N. Cx(Re(h x)) + ii * Cx(Re(g x))` THEN
    ASM_SIMP_TAC[] THEN X_GEN_TAC `x:real^N` THEN DISCH_TAC THEN
    GEN_REWRITE_TAC (LAND_CONV o RAND_CONV o LAND_CONV) [
COMPLEX_EXPAND] THEN
    MATCH_MP_TAC(NORM_ARITH
     `norm(x1 - x2) < e / &2 /\ norm(y1 - y2) < e / &2
      ==> norm((x1 + y1) - (x2 + y2)) < e`) THEN
    ASM_SIMP_TAC[GSYM 
CX_SUB; 
COMPLEX_NORM_CX; GSYM 
COMPLEX_SUB_LDISTRIB;
                 
COMPLEX_NORM_MUL; 
COMPLEX_NORM_II; REAL_MUL_LID]]);;
 
let COMPLEX_STONE_WEIERSTRASS = prove
 (`!P s. compact s /\
         (!f. P f ==> f 
continuous_on s) /\
         (!c. P (\x. c)) /\
         (!f. P f ==> P(\x. cnj(f x))) /\
         (!f g. P f /\ P g ==> P (\x. f x + g x)) /\
         (!f g. P f /\ P g ==> P (\x. f x * g x)) /\
         (!x y. x 
IN s /\ y 
IN s /\ ~(x = y) ==> ?f. P f /\ ~(f x = f y))
         ==> !f:real^N->complex e.
                f 
continuous_on s /\ &0 < e
                ==> ?g. P g /\ !x. x 
IN s ==> norm(f x - g x) < e`,
  REPEAT GEN_TAC THEN STRIP_TAC THEN
  MATCH_MP_TAC 
COMPLEX_STONE_WEIERSTRASS_ALT THEN ASM_SIMP_TAC[] THEN
  MAP_EVERY X_GEN_TAC [`x:real^N`; `y:real^N`] THEN STRIP_TAC THEN
  FIRST_X_ASSUM(MP_TAC o SPECL [`x:real^N`; `y:real^N`]) THEN
  ASM_REWRITE_TAC[] THEN MATCH_MP_TAC 
MONO_EXISTS THEN ASM_MESON_TAC[]);;
 
let LIPSCHITZ_REAL_POLYNOMIAL_FUNCTION = prove
 (`!f:real^N->real s.
        real_polynomial_function f /\ bounded s
        ==> ?B. &0 < B /\
                !x y. x 
IN s /\ y 
IN s ==> abs(f x - f y) <= B * norm(x - y)`,
  ONCE_REWRITE_TAC[
SWAP_FORALL_THM] THEN GEN_TAC THEN
  ASM_CASES_TAC `bounded(s:real^N->bool)` THEN ASM_REWRITE_TAC[] THEN
  ASM_CASES_TAC `s:real^N->bool = {}` THENL
   [ASM_REWRITE_TAC[
NOT_IN_EMPTY] THEN MESON_TAC[
REAL_LT_01]; ALL_TAC] THEN
  MATCH_MP_TAC real_polynomial_function_INDUCT THEN REPEAT CONJ_TAC THENL
   [REPEAT STRIP_TAC THEN EXISTS_TAC `&1` THEN REWRITE_TAC[
REAL_LT_01] THEN
    ASM_SIMP_TAC[REAL_MUL_LID; GSYM 
VECTOR_SUB_COMPONENT; 
COMPONENT_LE_NORM];
    GEN_TAC THEN EXISTS_TAC `&1` THEN
    SIMP_TAC[
REAL_LT_01; 
REAL_SUB_REFL; 
REAL_ABS_NUM; REAL_MUL_LID;
             
NORM_POS_LE];
    ALL_TAC; ALL_TAC] THEN
  MAP_EVERY X_GEN_TAC [`f:real^N->real`; `g:real^N->real`] THEN
  DISCH_THEN(CONJUNCTS_THEN2
    (X_CHOOSE_THEN `B1:real` STRIP_ASSUME_TAC)
    (X_CHOOSE_THEN `B2:real` STRIP_ASSUME_TAC))
  THENL
   [EXISTS_TAC `B1 + B2:real` THEN ASM_SIMP_TAC[
REAL_LT_ADD] THEN
    REPEAT STRIP_TAC THEN MATCH_MP_TAC(REAL_ARITH
     `abs(f - f') <= B1 * n /\ abs(g - g') <= B2 * n
      ==> abs((f + g) - (f' + g')) <= (B1 + B2) * n`) THEN
    ASM_SIMP_TAC[];
    FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM 
MEMBER_NOT_EMPTY]) THEN
    DISCH_THEN(X_CHOOSE_TAC `a:real^N`) THEN
    FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [
BOUNDED_POS]) THEN
    DISCH_THEN(X_CHOOSE_THEN `B:real` STRIP_ASSUME_TAC) THEN
    EXISTS_TAC `B1 * (abs(g(a:real^N)) + B2 * &2 * B) +
                B2 * (abs(f a) + B1 * &2 * B)` THEN
    CONJ_TAC THENL
     [MATCH_MP_TAC 
REAL_LT_ADD THEN CONJ_TAC THEN MATCH_MP_TAC 
REAL_LT_MUL THEN
      ASM_REWRITE_TAC[] THEN MATCH_MP_TAC(REAL_ARITH
       `&0 < x ==> &0 < abs a + x`) THEN
      MATCH_MP_TAC 
REAL_LT_MUL THEN ASM_REAL_ARITH_TAC;
      REPEAT STRIP_TAC THEN REWRITE_TAC[] THEN MATCH_MP_TAC(REAL_ARITH
       `abs((f - f') * g) <= a * n /\ abs((g - g') * f') <= b * n
        ==> abs(f * g - f' * g') <= (a + b) * n`) THEN
      ONCE_REWRITE_TAC[REAL_ARITH `(a * b) * c:real = (a * c) * b`] THEN
      REWRITE_TAC[
REAL_ABS_MUL] THEN
      CONJ_TAC THEN MATCH_MP_TAC 
REAL_LE_MUL2 THEN
      ASM_SIMP_TAC[
REAL_ABS_POS] THEN MATCH_MP_TAC(REAL_ARITH
       `abs(g x - g a) <= C * norm(x - a) /\
        C * norm(x - a:real^N) <= C * B ==> abs(g x) <= abs(g a) + C * B`) THEN
      ASM_SIMP_TAC[
REAL_LE_LMUL_EQ] THEN MATCH_MP_TAC(NORM_ARITH
       `norm x <= B /\ norm a <= B ==> norm(x - a:real^N) <= &2 * B`) THEN
      ASM_SIMP_TAC[]]]);;
 
let bernoulli = define
 `(!x. bernoulli 0 x = &1) /\
  (!n x. bernoulli (n + 1) x =
          x pow (n + 1) -
          sum(0..n) (\k. &(binom(n+2,k)) * bernoulli k x) / (&n + &2))`;;let lemma = prove
   (`(!n x. sum (0..n) (\k. &(binom(n,k)) * B k x) - B n x =
            &n * x pow (n - 1)) <=>
     (!x. B 0 x = &1) /\
     (!n x. B (n + 1) x =
            x pow (n + 1) -
            sum(0..n) (\k. &(binom(n+2,k)) * B k x) / (&n + &2))`,
    let cth = MESON[
num_CASES] `(!n. P n) <=> P 0 /\ (!n. P(SUC n))` in
    GEN_REWRITE_TAC LAND_CONV [cth] THEN
    GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [cth] THEN
    SIMP_TAC[
SUM_CLAUSES_NUMSEG; 
LE_0; 
BINOM_REFL; 
BINOM_PENULT; 
SUC_SUB1] THEN
    CONV_TAC NUM_REDUCE_CONV THEN
    REWRITE_TAC[REAL_MUL_LID; 
REAL_MUL_LZERO; 
REAL_SUB_REFL] THEN
    SIMP_TAC[
ADD1; ARITH_RULE `(n + 1) + 1 = n + 2`; GSYM REAL_OF_NUM_ADD] THEN
    BINOP_TAC THEN REPEAT(AP_TERM_TAC THEN ABS_TAC) THEN
    CONV_TAC REAL_FIELD) in
  REWRITE_TAC[lemma; bernoulli] THEN
  SUBGOAL_THEN
   `!n x. sum(0..n) (\k. &(binom(n,k)) *
                         sum (0..k)
                             (\l. &(binom(k,l)) *
                                  bernoulli l (&0) * x pow (k - l))) -
   sum(0..n) (\k. &(binom(n,k)) * bernoulli k (&0) * x pow (n - k)) =
   &n * x pow (n - 1)`
  MP_TAC THENL
   [REPEAT GEN_TAC THEN MP_TAC(ISPECL
     [`\n. bernoulli n (&0)`; `n:num`; `x:real`; `&1`] 
APPELL_SEQUENCE) THEN
    REWRITE_TAC[
REAL_POW_ONE; 
REAL_MUL_RID] THEN DISCH_THEN SUBST1_TAC THEN
    ONCE_REWRITE_TAC[REAL_ARITH `x + &1 = &1 + x`] THEN
    GEN_REWRITE_TAC (LAND_CONV o LAND_CONV) [GSYM 
APPELL_SEQUENCE] THEN
    REWRITE_TAC[
REAL_POW_ONE; 
REAL_MUL_RID; GSYM 
SUM_SUB_NUMSEG] THEN
    REWRITE_TAC[GSYM 
REAL_SUB_LDISTRIB; GSYM 
REAL_SUB_RDISTRIB] THEN
    REWRITE_TAC[REWRITE_RULE[GSYM lemma] bernoulli] THEN
    REWRITE_TAC[
REAL_POW_ZERO; 
COND_RAND; 
COND_RATOR] THEN
    REWRITE_TAC[ARITH_RULE `i - 1 = 0 <=> i = 0 \/ i = 1`] THEN
    REWRITE_TAC[MESON[]
     `(if p \/ q then x else y) = if q then x else if p then x else y`] THEN
    SIMP_TAC[
REAL_MUL_LZERO; 
REAL_MUL_RZERO; 
COND_ID; 
SUM_DELTA] THEN
    REWRITE_TAC[
IN_NUMSEG; 
LE_0; 
BINOM_1] THEN
    ASM_CASES_TAC `n = 0` THEN ASM_REWRITE_TAC[
REAL_MUL_LZERO] THEN
    ASM_SIMP_TAC[
LE_1] THEN REAL_ARITH_TAC;
    REWRITE_TAC[lemma] THEN STRIP_TAC THEN
     MATCH_MP_TAC 
num_WF THEN MATCH_MP_TAC 
num_INDUCTION THEN
    ASM_SIMP_TAC[
ADD1; bernoulli;
           ARITH_RULE `m < n + 1 <=> m <= n`]]);;
 
let BERNOULLI_ALT = prove
 (`!n x. sum(0..n) (\k. &(binom(n+1,k)) * bernoulli k x) =
         (&n + &1) * x pow n`,
 
let BERNOULLI_ADD = prove
 (`!n x y. bernoulli n (x + y) =
           sum(0..n) (\k. &(binom(n,k)) * bernoulli k x * y pow (n - k))`,
  REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[BERNOULLI_EXPANSION] THEN
  REWRITE_TAC[
APPELL_SEQUENCE]);;
 
let bernoulli_number = prove
 (`bernoulli 0 (&0) = &1 /\
  (!n. bernoulli (n + 1) (&0) =
       --sum(0..n) (\k. &(binom(n+2,k)) * bernoulli k (&0)) / (&n + &2))`,
 
let BERNOULLI_NUMBER = prove
 (`!n. sum (0..n) (\k. &(binom (n,k)) * bernoulli k (&0)) - bernoulli n (&0) =
       if n = 1 then &1 else &0`,
 
let BERNOULLI_1 = prove
 (`!n. bernoulli n (&1) =
       if n = 1 then bernoulli n (&0) + &1 else bernoulli n (&0)`,
  GEN_TAC THEN
  GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [GSYM REAL_ADD_LID] THEN
  COND_CASES_TAC THENL
   [REWRITE_TAC[REAL_ARITH `x = y + &1 <=> x - y = &1`];
    ONCE_REWRITE_TAC[GSYM 
REAL_SUB_0]] THEN
  REWRITE_TAC[
BERNOULLI_SUB_ADD1; 
REAL_POW_ZERO] THEN
  ASM_REWRITE_TAC[
SUB_REFL; 
REAL_MUL_RID] THEN
  ASM_CASES_TAC `n = 0` THEN ASM_REWRITE_TAC[
REAL_MUL_LZERO] THEN
  COND_CASES_TAC THEN REWRITE_TAC[] THEN ASM_ARITH_TAC);;
 
let SUM_OF_POWERS = prove
 (`!m n. sum(0..n) (\k. &k pow m) =
         (bernoulli (m + 1) (&n + &1) - bernoulli (m + 1) (&0)) / (&m + &1)`,
 
let BERNOULLI_HALF = prove
 (`!n. bernoulli n (&1 / &2) = (&2 / &2 pow n - &1) * bernoulli n (&0)`,
  GEN_TAC THEN
  MP_TAC(ISPECL [`n:num`; `&1`] 
BERNOULLI_RAABE_2) THEN
  CONV_TAC REAL_RAT_REDUCE_CONV THEN
  REWRITE_TAC[REAL_ARITH `a + b:real = c * a <=> b = (c - &1) * a`] THEN
  DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[
BERNOULLI_1] THEN
  COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);;
 
let REAL_EULER_MACLAURIN = prove
 (`!f m n p.
    m <= n /\
    (!k x. k <= 2 * p + 1 /\ x 
IN real_interval[&m,&n]
           ==> ((f k) 
has_real_derivative f (k + 1) x)
               (atreal x within 
real_interval [&m,&n]))
    ==> (\x. bernoulli (2 * p + 1) (frac x) * f (2 * p + 1) x)
        
real_integrable_on real_interval[&m,&n] /\
        sum(m..n) (\i. f 0 (&i)) =
        
real_integral (
real_interval [&m,&n]) (f 0) +
        (f 0 (&m) + f 0 (&n)) / &2 +
        sum (1..p) (\k. bernoulli (2 * k) (&0) / &(
FACT(2 * k)) *
                        (f (2 * k - 1) (&n) - f (2 * k - 1) (&m))) +
        
real_integral (
real_interval [&m,&n])
                      (\x. bernoulli (2 * p + 1) (frac x) * f (2 * p + 1) x) /
        &(
FACT(2 * p + 1))`,
  let lemma = prove
   (`!f k m n.
          f real_continuous_on real_interval[&m,&n] /\ m < n
          ==> ((\x. bernoulli k (frac x) * f x) has_real_integral
               sum(m..n-1) (\j. real_integral (real_interval[&j,&j + &1])
                                             (\x. bernoulli k (x - &j) * f x)))
              (real_interval[&m,&n])`,
    REPLICATE_TAC 3 GEN_TAC THEN INDUCT_TAC THEN REWRITE_TAC[CONJUNCT1 LT] THEN
    REWRITE_TAC[GSYM REAL_OF_NUM_SUC; LT_SUC_LE; SUC_SUB1] THEN STRIP_TAC THEN
    ASM_CASES_TAC `m:num = n` THENL
     [ASM_REWRITE_TAC[SUM_SING_NUMSEG] THEN (**** one ***) ALL_TAC;
      SUBGOAL_THEN `0 < n` ASSUME_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN
      ASM_SIMP_TAC[SUM_CLAUSES_RIGHT] THEN
      MATCH_MP_TAC HAS_REAL_INTEGRAL_COMBINE THEN EXISTS_TAC `&n` THEN
      ASM_REWRITE_TAC[REAL_OF_NUM_LE; REAL_ARITH `x <= x + &1`] THEN
      CONJ_TAC THENL
       [FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[LT_LE] THEN
        FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REWRITE_RULE[IMP_CONJ]
          REAL_CONTINUOUS_ON_SUBSET)) THEN
        REWRITE_TAC[SUBSET_REAL_INTERVAL] THEN
        ASM_REWRITE_TAC[REAL_OF_NUM_LE; REAL_ARITH `x <= x + &1`; LE_REFL];
        ALL_TAC]] THEN
    MATCH_MP_TAC(MESON[REAL_INTEGRAL_SPIKE; HAS_REAL_INTEGRAL_INTEGRAL;
                       REAL_INTEGRABLE_SPIKE]
     `!t. g real_integrable_on s /\ real_negligible t /\
          (!x. x IN s DIFF t ==> f x = g x)
          ==>  (f has_real_integral (real_integral s g)) s`) THEN
    EXISTS_TAC `{&n + &1}` THEN REWRITE_TAC[REAL_NEGLIGIBLE_SING] THEN
    (CONJ_TAC THENL
      [MATCH_MP_TAC REAL_INTEGRABLE_CONTINUOUS THEN
       MATCH_MP_TAC REAL_CONTINUOUS_ON_MUL THEN CONJ_TAC THENL
        [MATCH_MP_TAC REAL_DIFFERENTIABLE_ON_IMP_REAL_CONTINUOUS_ON THEN
         REWRITE_TAC[REAL_DIFFERENTIABLE_ON_DIFFERENTIABLE] THEN
         REPEAT STRIP_TAC THEN REAL_DIFFERENTIABLE_TAC;
         FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REWRITE_RULE[IMP_CONJ]
           REAL_CONTINUOUS_ON_SUBSET)) THEN
         REWRITE_TAC[SUBSET_REAL_INTERVAL] THEN
         REWRITE_TAC[REAL_OF_NUM_ADD; REAL_OF_NUM_LE] THEN ASM_ARITH_TAC];
       REWRITE_TAC[IN_DIFF; IN_SING; IN_REAL_INTERVAL] THEN
       X_GEN_TAC `x:real` THEN STRIP_TAC THEN AP_THM_TAC THEN AP_TERM_TAC THEN
       AP_TERM_TAC THEN     REWRITE_TAC[GSYM FRAC_UNIQUE] THEN
       REWRITE_TAC[REAL_ARITH `x - (x - &n) = &n`; INTEGER_CLOSED] THEN
       ASM_REAL_ARITH_TAC])) in
  let step = prove
   (`!f f' k m n.
          m < n /\
          (!x. x IN real_interval[&m,&n]
               ==> (f has_real_derivative f' x)
                   (atreal x within real_interval[&m,&n])) /\
          f' real_continuous_on real_interval[&m,&n]
          ==> real_integral (real_interval[&m,&n])
                            (\x. bernoulli (k + 1) (frac x) * f' x) =
              (bernoulli (k + 1) (&0) * (f(&n) - f(&m)) +
               (if k = 0 then sum(m+1..n) (\i. f(&i)) else &0)) -
              (&k + &1) *
              real_integral (real_interval[&m,&n])
                            (\x. bernoulli k (frac x) * f x)`,
    REPEAT STRIP_TAC THEN
    SUBGOAL_THEN `f real_continuous_on real_interval[&m,&n]` ASSUME_TAC THENL
     [ASM_MESON_TAC[REAL_DIFFERENTIABLE_ON_DIFFERENTIABLE;
                    real_differentiable;
                    REAL_DIFFERENTIABLE_ON_IMP_REAL_CONTINUOUS_ON];
      ASM_SIMP_TAC[REWRITE_RULE[HAS_REAL_INTEGRAL_INTEGRABLE_INTEGRAL]
       lemma]] THEN
    TRANS_TAC EQ_TRANS
      `sum(m..n-1)
          (\j. (bernoulli (k + 1) (&0) * (f (&j + &1) - f (&j)) +
                (if k = 0 then f (&j + &1) else &0)) -
               (&k + &1) *
               real_integral (real_interval[&j,&j + &1])
                             (\x. bernoulli k (x - &j) * f x))` THEN
    CONJ_TAC THENL
     [MATCH_MP_TAC SUM_EQ_NUMSEG THEN X_GEN_TAC `j:num` THEN STRIP_TAC THEN
      REWRITE_TAC[] THEN MATCH_MP_TAC REAL_INTEGRAL_UNIQUE THEN
      MATCH_MP_TAC(ONCE_REWRITE_RULE[REAL_MUL_SYM]
        REAL_INTEGRATION_BY_PARTS_SIMPLE) THEN
      MAP_EVERY EXISTS_TAC
       [`f:real->real`; `\x. (&k + &1) * bernoulli k (x - &j)`] THEN
      REWRITE_TAC[REAL_ADD_SUB; REAL_SUB_REFL; BERNOULLI_1] THEN
      REPEAT CONJ_TAC THENL
       [REAL_ARITH_TAC;
        X_GEN_TAC `x:real` THEN DISCH_TAC THEN
        CONJ_TAC THENL
         [FIRST_X_ASSUM(MP_TAC o SPEC `x:real`) THEN ANTS_TAC THENL
           [FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (SET_RULE
             `x IN s ==> s SUBSET t ==> x IN t`));
            MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ_ALT]
              HAS_REAL_DERIVATIVE_WITHIN_SUBSET)] THEN
          REWRITE_TAC[SUBSET_REAL_INTERVAL] THEN
          REWRITE_TAC[REAL_OF_NUM_LE; REAL_OF_NUM_ADD] THEN ASM_ARITH_TAC;
          REAL_DIFF_TAC THEN  REWRITE_TAC[GSYM REAL_OF_NUM_ADD; ADD_SUB] THEN
          REAL_ARITH_TAC];
        REWRITE_TAC[ARITH_RULE `k + 1 = 1 <=> k = 0`] THEN
        ASM_CASES_TAC `k = 0` THEN ASM_REWRITE_TAC[] THENL
         [REWRITE_TAC[REAL_ARITH
           `(b + &1) * f1 - b * f0 - ((b * (f1 - f0) + f1) - w):real = w`];
          REWRITE_TAC[REAL_ARITH
           `b * f1 - b * f0 - ((b * (f1 - f0) + &0) - w) = w`]] THEN
        REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN
        MATCH_MP_TAC HAS_REAL_INTEGRAL_LMUL THEN
        MATCH_MP_TAC REAL_INTEGRABLE_INTEGRAL THEN
        MATCH_MP_TAC REAL_INTEGRABLE_CONTINUOUS THEN
        MATCH_MP_TAC REAL_CONTINUOUS_ON_MUL THEN
        (CONJ_TAC THENL
          [MATCH_MP_TAC REAL_DIFFERENTIABLE_ON_IMP_REAL_CONTINUOUS_ON THEN
           REWRITE_TAC[REAL_DIFFERENTIABLE_ON_DIFFERENTIABLE] THEN
           REPEAT STRIP_TAC THEN REAL_DIFFERENTIABLE_TAC;
           FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REWRITE_RULE[IMP_CONJ]
             REAL_CONTINUOUS_ON_SUBSET)) THEN
           REWRITE_TAC[SUBSET_REAL_INTERVAL] THEN
           REWRITE_TAC[REAL_OF_NUM_LE; REAL_OF_NUM_ADD] THEN ASM_ARITH_TAC])];
      REWRITE_TAC[SUM_ADD_NUMSEG; SUM_LMUL; SUM_SUB_NUMSEG] THEN
      AP_THM_TAC THEN AP_TERM_TAC THEN BINOP_TAC THENL
       [AP_TERM_TAC THEN REWRITE_TAC[GSYM SUM_SUB_NUMSEG] THEN
        REWRITE_TAC[REAL_OF_NUM_ADD; SUM_DIFFS_ALT] THEN
        COND_CASES_TAC THENL [ALL_TAC; ASM_ARITH_TAC] THEN
        AP_THM_TAC THEN AP_TERM_TAC THEN AP_TERM_TAC THEN AP_TERM_TAC THEN
        ASM_ARITH_TAC;
        ASM_CASES_TAC `k = 0` THEN ASM_REWRITE_TAC[SUM_0] THEN
        REWRITE_TAC[GSYM(SPEC `1` SUM_OFFSET); REAL_OF_NUM_ADD] THEN
        AP_THM_TAC THEN AP_TERM_TAC THEN AP_TERM_TAC THEN ASM_ARITH_TAC]]) in
  REPEAT GEN_TAC THEN STRIP_TAC THEN
  FIRST_X_ASSUM(DISJ_CASES_TAC o MATCH_MP (ARITH_RULE
   `m:num <= n ==> m = n \/ m < n`))
  THENL
   [ASM_SIMP_TAC[REAL_INTEGRABLE_ON_NULL; REAL_LE_REFL] THEN
    ASM_REWRITE_TAC[SUM_SING_NUMSEG; REAL_SUB_REFL; REAL_MUL_LZERO] THEN
    SIMP_TAC[REAL_INTEGRAL_NULL; REAL_LE_REFL; REAL_ARITH `(x + x) / &2 = x`;
             REAL_MUL_RZERO; SUM_0; real_div; REAL_MUL_LZERO] THEN
    REAL_ARITH_TAC;
    ALL_TAC] THEN
  CONJ_TAC THENL
   [REWRITE_TAC[real_integrable_on] THEN
    MP_TAC(ISPECL [`f (2 * p + 1):real->real`; `2 * p + 1`; `m:num`; `n:num`]
        lemma) THEN
    ASM_REWRITE_TAC[] THEN ANTS_TAC THENL [ALL_TAC; MESON_TAC[]] THEN
    MATCH_MP_TAC REAL_DIFFERENTIABLE_ON_IMP_REAL_CONTINUOUS_ON THEN
    REWRITE_TAC[REAL_DIFFERENTIABLE_ON_DIFFERENTIABLE] THEN
    REWRITE_TAC[real_differentiable] THEN ASM_MESON_TAC[LE_REFL];
    ALL_TAC] THEN
  ASM_SIMP_TAC[SUM_CLAUSES_LEFT; LT_IMP_LE] THEN
  SUBGOAL_THEN
   `!k:num.  k <= 2 * p + 1
             ==> (f k) real_differentiable_on real_interval[&m,&n]`
  ASSUME_TAC THENL [ASM_MESON_TAC[real_differentiable_on]; ALL_TAC] THEN
  MP_TAC(ISPECL [`(f:num->real->real) 0`; `(f:num->real->real) (0 + 1)`;
                 `0`; `m:num`; `n:num`] step) THEN
  ASM_SIMP_TAC[REAL_DIFFERENTIABLE_ON_IMP_REAL_CONTINUOUS_ON;
               ARITH_RULE `0 + 1 <= 2 * p + 1`; LE_0] THEN
  CONV_TAC NUM_REDUCE_CONV THEN REWRITE_TAC[CONJUNCT1 bernoulli] THEN
  REWRITE_TAC[REAL_ADD_LID; REAL_MUL_LID; ETA_AX] THEN
  REWRITE_TAC[BERNOULLI_CONV `bernoulli 1 (&0)`] THEN
  MATCH_MP_TAC(REAL_ARITH
   `i' = r ==> i' = (-- &1 / &2 * (n - m) + s) - i
               ==> m + s = i + (m + n) / &2 + r`) THEN
  POP_ASSUM_LIST(MP_TAC o end_itlist CONJ o rev) THEN
  SPEC_TAC(`p:num`,`p:num`) THEN INDUCT_TAC THENL
   [REWRITE_TAC[SUM_CLAUSES_NUMSEG] THEN CONV_TAC NUM_REDUCE_CONV THEN
    REAL_ARITH_TAC;
    GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV)
     [ARITH_RULE `2 * SUC p + 1 = 2 * p + 3`] THEN
    FIRST_X_ASSUM(fun th -> STRIP_TAC THEN MP_TAC th) THEN
    ASM_SIMP_TAC[ARITH_RULE `k <= 2 * p + 1 ==> k <= 2 * p + 3`] THEN
    DISCH_TAC] THEN
  ASM_REWRITE_TAC[SUM_CLAUSES_NUMSEG; ARITH_RULE `1 <= SUC n`] THEN
  REWRITE_TAC[GSYM REAL_ADD_ASSOC] THEN AP_TERM_TAC THEN
  MP_TAC(ISPECL [`(f:num->real->real) (2 * p + 1)`;
                 `(f:num->real->real) ((2 * p + 1) + 1)`;
                 `2 * p + 1`; `m:num`; `n:num`] step) THEN
  ASM_SIMP_TAC[REAL_DIFFERENTIABLE_ON_IMP_REAL_CONTINUOUS_ON;
               ARITH_RULE `(2 * p + 1) + 1 <= 2 * p + 3`;
               ARITH_RULE `2 * p + 1 <= 2 * p + 3`] THEN
  REWRITE_TAC[ADD_EQ_0; ARITH_EQ; REAL_ADD_RID] THEN
  REWRITE_TAC[GSYM REAL_OF_NUM_ADD; GSYM REAL_OF_NUM_MUL] THEN
  REWRITE_TAC[REAL_FIELD
   `x = y - ((&2 * &p + &1) + &1) * z <=> z = (y - x) / (&2 * &p + &2)`] THEN
  DISCH_THEN SUBST1_TAC THEN
  REWRITE_TAC[ARITH_RULE `2 * SUC p - 1 = 2 * p + 1`] THEN
  REWRITE_TAC[ARITH_RULE `(2 * p + 1) + 1 = 2 * SUC p`] THEN
  REWRITE_TAC[ARITH_RULE `2 * SUC p = SUC(2 * p + 1)`] THEN
  REWRITE_TAC[ARITH_RULE `SUC(2 * p + 1) + 1 = SUC(SUC(2 * p + 1))`] THEN
  REWRITE_TAC[FACT; GSYM REAL_OF_NUM_MUL; GSYM REAL_OF_NUM_ADD;
              GSYM REAL_OF_NUM_SUC] THEN
  MATCH_MP_TAC(REAL_FIELD
   `~(t = &0) /\
    i2 = &0 - (&2 * &p + &3) * i1
    ==> (b * (fn - fm) - i1) / (&2 * &p + &2) / t =
        b / (((&2 * &p + &1) + &1) * t) * (fn - fm) +
        i2 / ((((&2 * &p + &1) + &1) + &1) * ((&2 * &p + &1) + &1) * t)`) THEN
  REWRITE_TAC[REAL_OF_NUM_EQ; FACT_NZ] THEN
  MP_TAC(ISPECL [`(f:num->real->real) (SUC(2 * p + 1))`;
                 `(f:num->real->real) (SUC(2 * p + 1) + 1)`;
                 `SUC(2 * p + 1)`; `m:num`; `n:num`] step) THEN
  ASM_SIMP_TAC[REAL_DIFFERENTIABLE_ON_IMP_REAL_CONTINUOUS_ON; NOT_SUC;
               ARITH_RULE `SUC(2 * p + 1) + 1 <= 2 * p + 3`;
               ARITH_RULE `SUC(2 * p + 1) <= 2 * p + 3`] THEN
  REWRITE_TAC[ADD1; GSYM ADD_ASSOC; REAL_OF_NUM_ADD] THEN
  CONV_TAC NUM_REDUCE_CONV THEN
  REWRITE_TAC[GSYM REAL_OF_NUM_ADD; REAL_ADD_RID; GSYM REAL_OF_NUM_MUL] THEN
  DISCH_THEN SUBST1_TAC THEN AP_THM_TAC THEN AP_TERM_TAC THEN
  REWRITE_TAC[REAL_ENTIRE] THEN DISJ1_TAC THEN
  REWRITE_TAC[BERNOULLI_NUMBER_EQ_0] THEN
  REWRITE_TAC[ODD_ADD; ODD_MULT; ARITH] THEN ARITH_TAC);;  
let REAL_EULER_MACLAURIN_ANTIDERIVATIVE = prove
 (`!f m n p.
     m <= n /\
     (!k x. k <= 2 * p + 2 /\ x 
IN real_interval[&m,&n]
            ==> ((f k) 
has_real_derivative f (k + 1) x)
                (atreal x within 
real_interval [&m,&n]))
     ==> ((\x. bernoulli (2 * p + 1) (frac x) * f (2 * p + 2) x)
          
real_integrable_on real_interval[&m,&n]) /\
         sum(m..n) (\i. f 1 (&i)) =
         (f 0 (&n) - f 0 (&m)) +
         (f 1 (&m) + f 1 (&n)) / &2 +
         sum (1..p) (\k. bernoulli (2 * k) (&0) / &(
FACT(2 * k)) *
                         (f (2 * k) (&n) - f (2 * k) (&m))) +
         
real_integral (
real_interval [&m,&n])
                       (\x. bernoulli (2 * p + 1) (frac x) * f (2 * p + 2) x) /
         &(
FACT(2 * p + 1))`,
  REPEAT GEN_TAC THEN STRIP_TAC THEN
  MP_TAC(ISPECL [`\n. (f:num->real->real)(SUC n)`; `m:num`; `n:num`; `p:num`]
        
REAL_EULER_MACLAURIN) THEN
  ASM_SIMP_TAC[ARITH_RULE `k <= 2 * p + 1 ==> SUC k <= 2 * p + 2`;
               ARITH_RULE `SUC(k + 1) = SUC k + 1`;
               ARITH_RULE `SUC(2 * p) + 1 = 2 * p + 2`] THEN
  CONV_TAC NUM_REDUCE_CONV THEN DISCH_THEN(SUBST1_TAC o CONJUNCT2) THEN
  MP_TAC(ISPECL
   [`f 0:real->real`; `f (0 + 1):real->real`; `&m`; `&n`]
        
REAL_FUNDAMENTAL_THEOREM_OF_CALCULUS) THEN
  ASM_SIMP_TAC[REAL_OF_NUM_LE; 
LE_0] THEN CONV_TAC NUM_REDUCE_CONV THEN
  DISCH_THEN(SUBST1_TAC o MATCH_MP 
REAL_INTEGRAL_UNIQUE) THEN
  AP_TERM_TAC THEN AP_TERM_TAC THEN
  REWRITE_TAC[ARITH_RULE `SUC(2 * p) + 1 = 2 * p + 2`] THEN
  AP_THM_TAC THEN AP_TERM_TAC THEN MATCH_MP_TAC 
SUM_EQ_NUMSEG THEN
  SIMP_TAC[ARITH_RULE `1 <= k ==> SUC(2 * k - 1) = 2 * k`]);;
 
let COMPLEX_EULER_MACLAURIN_ANTIDERIVATIVE = prove
 (`!f m n p.
     m <= n /\
     (!k x. k <= 2 * p + 2 /\ &m <= x /\ x <= &n
            ==> ((f k) 
has_complex_derivative f (k + 1) (Cx x)) (at(Cx x)))
     ==> (\x. Cx(bernoulli (2 * p + 1) (frac(drop x))) *
                       f (2 * p + 2) (Cx(drop x)))
         
integrable_on interval[lift(&m),lift(&n)] /\
         vsum(m..n) (\i. f 1 (Cx(&i))) =
         (f 0 (Cx(&n)) - f 0 (Cx(&m))) +
         (f 1 (Cx(&m)) + f 1 (Cx(&n))) / Cx(&2) +
         vsum (1..p) (\k. Cx(bernoulli (2 * k) (&0) / &(
FACT(2 * k))) *
                          (f (2 * k) (Cx(&n)) - f (2 * k) (Cx(&m)))) +
         integral (interval[lift(&m),lift(&n)])
                  (\x. Cx(bernoulli (2 * p + 1) (frac(drop x))) *
                       f (2 * p + 2) (Cx(drop x))) /
         Cx(&(
FACT(2 * p + 1)))`,
 
let REAL_SECOND_MEAN_VALUE_THEOREM_GEN_FULL = prove
 (`!f g a b u v.
        ~(
real_interval[a,b] = {}) /\
        f 
real_integrable_on real_interval[a,b] /\
        (!x. x 
IN real_interval(a,b) ==> u <= g x /\ g x <= v) /\
        (!x y. x 
IN real_interval[a,b] /\ y 
IN real_interval[a,b] /\ x <= y
               ==> g x <= g y)
        ==> ?c. c 
IN real_interval[a,b] /\
                ((\x. g x * f x) 
has_real_integral
                 (u * 
real_integral (
real_interval[a,c]) f +
                  v * 
real_integral (
real_interval[c,b]) f))
                (
real_interval[a,b])`,
 
let REAL_SECOND_MEAN_VALUE_THEOREM_GEN = prove
 (`!f g a b u v.
        ~(
real_interval[a,b] = {}) /\
        f 
real_integrable_on real_interval[a,b] /\
        (!x. x 
IN real_interval(a,b) ==> u <= g x /\ g x <= v) /\
        (!x y. x 
IN real_interval[a,b] /\ y 
IN real_interval[a,b] /\ x <= y
               ==> g x <= g y)
        ==> ?c. c 
IN real_interval[a,b] /\
                
real_integral (
real_interval[a,b]) (\x. g x * f x) =
                 u * 
real_integral (
real_interval[a,c]) f +
                 v * 
real_integral (
real_interval[c,b]) f`,
 
let HAS_BOUNDED_REAL_VARIATION_DARBOUX_STRONG = prove
 (`!f a b.
     f 
has_bounded_real_variation_on real_interval[a,b]
     ==> ?g h.
          (!x. f x = g x - h x) /\
          (!x y. x 
IN real_interval[a,b] /\ y 
IN real_interval[a,b] /\ x <= y
                 ==> g x <= g y) /\
          (!x y. x 
IN real_interval[a,b] /\ y 
IN real_interval[a,b] /\ x <= y
                 ==> h x <= h y) /\
          (!x y. x 
IN real_interval[a,b] /\ y 
IN real_interval[a,b] /\ x < y
                 ==> g x < g y) /\
          (!x y. x 
IN real_interval[a,b] /\ y 
IN real_interval[a,b] /\ x < y
                 ==> h x < h y) /\
          (!x. x 
IN real_interval[a,b] /\
               f 
real_continuous (atreal x within 
real_interval[a,x])
               ==> g 
real_continuous (atreal x within 
real_interval[a,x]) /\
                   h 
real_continuous (atreal x within 
real_interval[a,x])) /\
          (!x. x 
IN real_interval[a,b] /\
               f 
real_continuous (atreal x within 
real_interval[x,b])
               ==> g 
real_continuous (atreal x within 
real_interval[x,b]) /\
                   h 
real_continuous (atreal x within 
real_interval[x,b])) /\
          (!x. x 
IN real_interval[a,b] /\
               f 
real_continuous (atreal x within 
real_interval[a,b])
               ==> g 
real_continuous (atreal x within 
real_interval[a,b]) /\
                   h 
real_continuous (atreal x within 
real_interval[a,b]))`,