(* ========================================================================= *)
(* 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`,
(* ------------------------------------------------------------------------- *)
(* Real series. *)
(* ------------------------------------------------------------------------- *)
parse_as_infix("real_sums",(12,"right"));;
(* ------------------------------------------------------------------------- *)
(* Similar combining theorems just for summability. *)
(* ------------------------------------------------------------------------- *)
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);;
(* ------------------------------------------------------------------------- *)
(* Similar combining theorems for infsum. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Convergence tests for real series. *)
(* ------------------------------------------------------------------------- *)
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)`,
(* ------------------------------------------------------------------------- *)
(* Nets for real limit. *)
(* ------------------------------------------------------------------------- *)
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)`,
(* ------------------------------------------------------------------------- *)
(* Usual limit results with real domain and either vector or real range. *)
(* ------------------------------------------------------------------------- *)
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`,
(* ------------------------------------------------------------------------- *)
(* Some real limits involving transcendentals. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Relations between limits at real and complex limit points. *)
(* ------------------------------------------------------------------------- *)
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[]]);;
(* ------------------------------------------------------------------------- *)
(* Simpler theorems relating limits in real and real^1. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Additional congruence rules for simplifying limits. *)
(* ------------------------------------------------------------------------- *)
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)))`,
extend_basic_congs [LIM_CONG_WITHINREAL; LIM_CONG_ATREAL];;
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)))`,
extend_basic_congs [REALLIM_CONG_WITHIN; REALLIM_CONG_AT];;
extend_basic_congs [REALLIM_CONG_WITHINREAL; REALLIM_CONG_ATREAL];;
(* ------------------------------------------------------------------------- *)
(* Real version of Abel limit theorem. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Continuity of a function into the reals. *)
(* ------------------------------------------------------------------------- *)
parse_as_infix ("real_continuous",(12,"right"));;
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)`,
(* ------------------------------------------------------------------------- *)
(* Arithmetic combining theorems. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Some of these without netlimit, but with many different cases. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Composition of (real->real) o (real->real) functions. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Composition of (real->real) o (real^N->real) functions. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Composition of (real^N->real) o (real^M->real^N) functions. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Composition of (real^N->real) o (real->real^N) functions. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Composition of (real->real^N) o (real->real) functions. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Composition of (real^M->real^N) o (real->real^M) functions. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Composition of (real->real^N) o (real^M->real) functions. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Continuity of a real->real function on a set. *)
(* ------------------------------------------------------------------------- *)
parse_as_infix ("real_continuous_on",(12,"right"));;
(* ------------------------------------------------------------------------- *)
(* Real version of uniform continuity. *)
(* ------------------------------------------------------------------------- *)
parse_as_infix ("real_uniformly_continuous_on",(12,"right"));;
(* ------------------------------------------------------------------------- *)
(* Continuity versus componentwise continuity. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Derivative of real->real function. *)
(* ------------------------------------------------------------------------- *)
parse_as_infix ("has_real_derivative",(12,"right"));;
parse_as_infix ("real_differentiable",(12,"right"));;
parse_as_infix ("real_differentiable_on",(12,"right"));;
(* ------------------------------------------------------------------------- *)
(* Basic limit definitions in the useful cases. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Relation to Frechet derivative. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Relation to complex derivative. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Caratheodory characterization. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Property of being an interval (equivalent to convex or connected). *)
(* ------------------------------------------------------------------------- *)
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[]);;
(* ------------------------------------------------------------------------- *)
(* Some relations with the complex numbers can also be useful. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* The same tricks to define closed and open intervals. *)
(* ------------------------------------------------------------------------- *)
make_overloadable "real_interval" `:A`;;
overload_interface("real_interval",`open_real_interval`);;
overload_interface("real_interval",`closed_real_interval`);;
(* ------------------------------------------------------------------------- *)
(* Real continuity and differentiability. *)
(* ------------------------------------------------------------------------- *)
add_translation_invariants [REAL_CONTINUOUS_AT_TRANSLATION];;
add_linear_invariants [REAL_CONTINUOUS_AT_LINEAR_IMAGE];;
(* ------------------------------------------------------------------------- *)
(* More basics about real derivatives. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Some handy theorems about the actual differentition function. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Arithmetical combining theorems. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Same thing just for real differentiability. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Same again for being differentiable on a set. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Derivative (and continuity) theorems for real transcendental functions. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Hence differentiation of the norm. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Some somewhat sharper continuity theorems including endpoints. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Differentiation conversion. *)
(* ------------------------------------------------------------------------- *)
let real_differentiation_theorems = ref [];;
let add_real_differentiation_theorems =
add_real_differentiation_theorems
([HAS_REAL_DERIVATIVE_LMUL_WITHIN; HAS_REAL_DERIVATIVE_LMUL_ATREAL;
HAS_REAL_DERIVATIVE_RMUL_WITHIN; HAS_REAL_DERIVATIVE_RMUL_ATREAL;
HAS_REAL_DERIVATIVE_CDIV_WITHIN; HAS_REAL_DERIVATIVE_CDIV_ATREAL;
HAS_REAL_DERIVATIVE_ID;
HAS_REAL_DERIVATIVE_CONST;
HAS_REAL_DERIVATIVE_NEG;
HAS_REAL_DERIVATIVE_ADD;
HAS_REAL_DERIVATIVE_SUB;
HAS_REAL_DERIVATIVE_MUL_WITHIN; HAS_REAL_DERIVATIVE_MUL_ATREAL;
HAS_REAL_DERIVATIVE_DIV_WITHIN; HAS_REAL_DERIVATIVE_DIV_ATREAL;
HAS_REAL_DERIVATIVE_POW_WITHIN; HAS_REAL_DERIVATIVE_POW_ATREAL;
HAS_REAL_DERIVATIVE_INV_WITHIN; HAS_REAL_DERIVATIVE_INV_ATREAL] @
(CONJUNCTS(REWRITE_RULE[FORALL_AND_THM]
(MATCH_MP HAS_REAL_DERIVATIVE_CHAIN_UNIV
HAS_REAL_DERIVATIVE_EXP))) @
(CONJUNCTS(REWRITE_RULE[FORALL_AND_THM]
(MATCH_MP HAS_REAL_DERIVATIVE_CHAIN_UNIV
HAS_REAL_DERIVATIVE_SIN))) @
(CONJUNCTS(REWRITE_RULE[FORALL_AND_THM]
(MATCH_MP HAS_REAL_DERIVATIVE_CHAIN_UNIV
HAS_REAL_DERIVATIVE_COS))) @
(CONJUNCTS(REWRITE_RULE[FORALL_AND_THM]
(MATCH_MP HAS_REAL_DERIVATIVE_CHAIN
HAS_REAL_DERIVATIVE_TAN))) @
(CONJUNCTS(REWRITE_RULE[FORALL_AND_THM]
(MATCH_MP HAS_REAL_DERIVATIVE_CHAIN
HAS_REAL_DERIVATIVE_LOG))) @
(CONJUNCTS(REWRITE_RULE[FORALL_AND_THM]
(MATCH_MP HAS_REAL_DERIVATIVE_CHAIN
HAS_REAL_DERIVATIVE_SQRT))) @
(CONJUNCTS(REWRITE_RULE[FORALL_AND_THM]
(MATCH_MP HAS_REAL_DERIVATIVE_CHAIN_UNIV
HAS_REAL_DERIVATIVE_ATN))) @
(CONJUNCTS(REWRITE_RULE[FORALL_AND_THM]
(MATCH_MP HAS_REAL_DERIVATIVE_CHAIN
HAS_REAL_DERIVATIVE_ASN))) @
(CONJUNCTS(REWRITE_RULE[FORALL_AND_THM]
(MATCH_MP HAS_REAL_DERIVATIVE_CHAIN
HAS_REAL_DERIVATIVE_ACS))));;
let rec REAL_DIFF_CONV =
let partfn tm = let l,r = dest_comb tm in mk_pair(lhand l,r)
and is_deriv = can (term_match [] `(f has_real_derivative f') net`) in
let rec REAL_DIFF_CONV tm =
try tryfind (fun th -> PART_MATCH partfn th (partfn tm))
(!real_differentiation_theorems)
with Failure _ ->
let ith = tryfind (fun th ->
PART_MATCH (partfn o repeat (snd o dest_imp)) th (partfn tm))
(!real_differentiation_theorems) in
REAL_DIFF_ELIM ith
and REAL_DIFF_ELIM th =
let tm = concl th in
if not(is_imp tm) then th else
let t = lhand tm in
if not(is_deriv t) then UNDISCH th
else REAL_DIFF_ELIM (MATCH_MP th (REAL_DIFF_CONV t)) in
REAL_DIFF_CONV;;
(* ------------------------------------------------------------------------- *)
(* Hence a tactic. *)
(* ------------------------------------------------------------------------- *)
let REAL_DIFF_TAC =
let pth = MESON[]
`(f has_real_derivative f') net
==> f' = g'
==> (f has_real_derivative g') net` in
W(fun (asl,w) -> let th = MATCH_MP pth (REAL_DIFF_CONV w) in
MATCH_MP_TAC(repeat (GEN_REWRITE_RULE I [IMP_IMP]) (DISCH_ALL th)));;
let REAL_DIFFERENTIABLE_TAC =
let DISCH_FIRST th = DISCH (hd(hyp th)) th in
GEN_REWRITE_TAC I [real_differentiable] THEN
W(fun (asl,w) ->
let th = REAL_DIFF_CONV(snd(dest_exists w)) in
let f' = rand(rator(concl th)) in
EXISTS_TAC f' THEN
(if hyp th = [] then MATCH_ACCEPT_TAC th else
let th' = repeat (GEN_REWRITE_RULE I [IMP_IMP] o DISCH_FIRST)
(DISCH_FIRST th) in
MATCH_MP_TAC th'));;
(* ------------------------------------------------------------------------- *)
(* Analytic results for real power function. *)
(* ------------------------------------------------------------------------- *)
add_real_differentiation_theorems
(CONJUNCTS(REWRITE_RULE[FORALL_AND_THM]
(GEN `y:real` (MATCH_MP HAS_REAL_DERIVATIVE_CHAIN
(SPEC `y:real`
(ONCE_REWRITE_RULE[SWAP_FORALL_THM] HAS_REAL_DERIVATIVE_RPOW))))));;
add_real_differentiation_theorems
(CONJUNCTS(REWRITE_RULE[FORALL_AND_THM]
(MATCH_MP HAS_REAL_DERIVATIVE_CHAIN
(SPEC `a:real` HAS_REAL_DERIVATIVE_RPOW_RIGHT))));;
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`,
(* ------------------------------------------------------------------------- *)
(* Analytic result for "frac". *)
(* ------------------------------------------------------------------------- *)
add_real_differentiation_theorems
(CONJUNCTS(REWRITE_RULE[FORALL_AND_THM]
(MATCH_MP HAS_REAL_DERIVATIVE_CHAIN HAS_REAL_DERIVATIVE_FRAC)));;
(* ------------------------------------------------------------------------- *)
(* Polynomials are differentiable and continuous. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Intermediate Value Theorem. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Zeroness (or sign at boundary) of derivative at local extremum. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Rolle and Mean Value Theorem. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Cauchy MVT and l'Hospital's rule. *)
(* ------------------------------------------------------------------------- *)
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]);;
(* ------------------------------------------------------------------------- *)
(* Darboux's theorem (intermediate value property for derivatives). *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Continuity and differentiability of inverse functions. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Real differentiation of sequences and series. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Comparing sums and "integrals" via real antiderivatives. *)
(* ------------------------------------------------------------------------- *)
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]);;
(* ------------------------------------------------------------------------- *)
(* Relating different kinds of real limits. *)
(* ------------------------------------------------------------------------- *)
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]);;
(* ------------------------------------------------------------------------- *)
(* Real segments (bidirectional intervals). *)
(* ------------------------------------------------------------------------- *)
make_overloadable "real_segment" `:A`;;
overload_interface("real_segment",`open_real_segment`);;
overload_interface("real_segment",`closed_real_segment`);;
(* ------------------------------------------------------------------------- *)
(* Convex real->real functions. *)
(* ------------------------------------------------------------------------- *)
parse_as_infix ("real_convex_on",(12,"right"));;
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)`;;
(* ------------------------------------------------------------------------- *)
(* Some convexity-derived inequalities including AGM and Young's inequality. *)
(* ------------------------------------------------------------------------- *)
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);;
(* ------------------------------------------------------------------------- *)
(* Some other inequalities where it's handy just to use calculus. *)
(* ------------------------------------------------------------------------- *)
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]);;
(* ------------------------------------------------------------------------- *)
(* Log-convex functions. *)
(* ------------------------------------------------------------------------- *)
parse_as_infix("log_convex_on",(12,"right"));;
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)`,
(* ------------------------------------------------------------------------- *)
(* Real log-convex functions. *)
(* ------------------------------------------------------------------------- *)
parse_as_infix("real_log_convex_on",(12,"right"));;
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)`;;
(* ------------------------------------------------------------------------- *)
(* Integrals of real->real functions; measures of real sets. *)
(* ------------------------------------------------------------------------- *)
parse_as_infix("has_real_integral",(12,"right"));;
parse_as_infix("real_integrable_on",(12,"right"));;
parse_as_infix("absolutely_real_integrable_on",(12,"right"));;
parse_as_infix("has_real_measure",(12,"right"));;
(* ------------------------------------------------------------------------- *)
(* Integration by parts. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Change of variable in real integral (one that we know exists). *)
(* ------------------------------------------------------------------------- *)
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])`,
(* ------------------------------------------------------------------------- *)
(* Drop the k'th coordinate, or insert t at the k'th coordinate. *)
(* ------------------------------------------------------------------------- *)
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]);;
(* ------------------------------------------------------------------------- *)
(* Take slice of set s at x$k = t and drop the k'th coordinate. *)
(* ------------------------------------------------------------------------- *)
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 {}`,
(* ------------------------------------------------------------------------- *)
(* Weak but useful versions of Fubini's theorem. *)
(* ------------------------------------------------------------------------- *)
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`,
(* ------------------------------------------------------------------------- *)
(* Scaled integer, and hence rational, values are dense in the reals. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Hence a criterion for two functions to agree. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Various sufficient conditions for additivity to imply linearity. *)
(* ------------------------------------------------------------------------- *)
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]);;
(* ------------------------------------------------------------------------- *)
(* Extending a continuous function in a periodic way. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* A variant of REAL_CONTINUOUS_ADDITIVE_IMP_LINEAR for intervals. *)
(* ------------------------------------------------------------------------- *)
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]]);;
(* ------------------------------------------------------------------------- *)
(* More Steinhaus variants. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Bernstein polynomials. *)
(* ------------------------------------------------------------------------- *)
let BERNSTEIN_CONV =
GEN_REWRITE_CONV I [bernstein] THENC
COMB2_CONV (RAND_CONV(RAND_CONV NUM_BINOM_CONV))
(RAND_CONV(RAND_CONV NUM_SUB_CONV)) THENC
REAL_POLY_CONV;;
(* ------------------------------------------------------------------------- *)
(* Lemmas about Bernstein polynomials. *)
(* ------------------------------------------------------------------------- *)
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]);;
(* ------------------------------------------------------------------------- *)
(* Explicit Bernstein version of 1D Weierstrass approximation theorem *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* General Stone-Weierstrass theorem. *)
(* ------------------------------------------------------------------------- *)
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";
"C"] THEN SIMP_TAC[]] THEN
SUBGOAL_THEN `!c:real. A(\x:real^N. c)` (LABEL_TAC "const") THENL
[MAP_EVERY EXPAND_TAC ["A"; "C"] THEN X_GEN_TAC `c:real` THEN
ASM_REWRITE_TAC[REAL_CONTINUOUS_CONST] THEN X_GEN_TAC `e:real` THEN
DISCH_TAC THEN EXISTS_TAC `(\x. c):real^N->real` THEN
ASM_REWRITE_TAC[REAL_SUB_REFL; REAL_ABS_0];
ALL_TAC] THEN
SUBGOAL_THEN `!f g:real^N->real. A(f) /\ A(g) ==> A(\x. f x + g x)`
(LABEL_TAC "add") THENL
[MAP_EVERY EXPAND_TAC ["A"; "C"] THEN SIMP_TAC[REAL_CONTINUOUS_ADD] THEN
MAP_EVERY X_GEN_TAC [`f:real^N->real`; `g:real^N->real`] THEN
DISCH_THEN(fun th -> REPEAT STRIP_TAC THEN MP_TAC th) THEN
DISCH_THEN(CONJUNCTS_THEN (MP_TAC o SPEC `e / &2` o CONJUNCT2)) THEN
ASM_REWRITE_TAC[REAL_HALF; LEFT_IMP_EXISTS_THM] THEN
X_GEN_TAC `g':real^N->real` THEN STRIP_TAC THEN
X_GEN_TAC `f':real^N->real` THEN STRIP_TAC THEN
EXISTS_TAC `(\x. f' x + g' x):real^N->real` THEN
ASM_SIMP_TAC[REAL_ARITH
`abs(f - f') < e / &2 /\ abs(g - g') < e / &2
==> abs((f + g) - (f' + g')) < e`];
ALL_TAC] THEN
SUBGOAL_THEN `!f:real^N->real. A(f) ==> C(f)` (LABEL_TAC "AC") THENL
[EXPAND_TAC "A" THEN SIMP_TAC[]; ALL_TAC] THEN
SUBGOAL_THEN `!f:real^N->real. C(f) ==> real_bounded(IMAGE f s)`
(LABEL_TAC "bound") THENL
[GEN_TAC THEN EXPAND_TAC "C" THEN
REWRITE_TAC[REAL_BOUNDED; GSYM IMAGE_o] THEN
REWRITE_TAC[REAL_CONTINUOUS_CONTINUOUS1] THEN
REWRITE_TAC[GSYM CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN] THEN
ASM_SIMP_TAC[COMPACT_IMP_BOUNDED; COMPACT_CONTINUOUS_IMAGE];
ALL_TAC] THEN
SUBGOAL_THEN `!f g:real^N->real. A(f) /\ A(g) ==> A(\x. f x * g x)`
(LABEL_TAC "mul") THENL
[MAP_EVERY X_GEN_TAC [`f:real^N->real`; `g:real^N->real`] THEN
DISCH_THEN(fun th -> STRIP_ASSUME_TAC th THEN MP_TAC th) THEN
MAP_EVERY EXPAND_TAC ["A"; "C"] THEN SIMP_TAC[REAL_CONTINUOUS_MUL] THEN
REWRITE_TAC[IMP_CONJ] THEN
MAP_EVERY (DISCH_THEN o LABEL_TAC) ["cf"; "af"; "cg"; "ag"] THEN
SUBGOAL_THEN
`real_bounded(IMAGE (f:real^N->real) s) /\
real_bounded(IMAGE (g:real^N->real) s)`
MP_TAC THENL
[ASM_SIMP_TAC[]; REWRITE_TAC[REAL_BOUNDED_POS_LT; FORALL_IN_IMAGE]] THEN
DISCH_THEN(CONJUNCTS_THEN2
(X_CHOOSE_THEN `Bf:real` STRIP_ASSUME_TAC)
(X_CHOOSE_THEN `Bg:real` STRIP_ASSUME_TAC)) THEN
X_GEN_TAC `e:real` THEN DISCH_TAC THEN
REMOVE_THEN "ag" (MP_TAC o SPEC `e / &2 / Bf`) THEN
ASM_SIMP_TAC[REAL_HALF; REAL_LT_DIV; LEFT_IMP_EXISTS_THM] THEN
X_GEN_TAC `g':real^N->real` THEN STRIP_TAC THEN
REMOVE_THEN "af" (MP_TAC o SPEC `e / &2 / (Bg + e / &2 / Bf)`) THEN
ASM_SIMP_TAC[REAL_HALF; REAL_LT_DIV; REAL_LT_ADD] THEN
DISCH_THEN(X_CHOOSE_THEN `f':real^N->real` STRIP_ASSUME_TAC) THEN
EXISTS_TAC `(\x. f'(x) * g'(x)):real^N->real` THEN
ASM_SIMP_TAC[REAL_ARITH
`f * g - f' * g':real = f * (g - g') + g' * (f - f')`] THEN
X_GEN_TAC `x:real^N` THEN DISCH_TAC THEN
SUBGOAL_THEN `e = Bf * e / &2 / Bf +
(Bg + e / &2 / Bf) * e / &2 / (Bg + e / &2 / Bf)`
SUBST1_TAC THENL
[MATCH_MP_TAC(REAL_ARITH `a = e / &2 /\ b = e / &2 ==> e = a + b`) THEN
CONJ_TAC THEN MAP_EVERY MATCH_MP_TAC [REAL_DIV_LMUL; REAL_LT_IMP_NZ] THEN
ASM_SIMP_TAC[REAL_LT_DIV; REAL_LT_ADD; REAL_HALF];
MATCH_MP_TAC(REAL_ARITH
`abs a < c /\ abs b < d ==> abs(a + b) < c + d`) THEN
REWRITE_TAC[REAL_ABS_MUL] THEN CONJ_TAC THEN
MATCH_MP_TAC REAL_LT_MUL2 THEN ASM_SIMP_TAC[REAL_ABS_POS] THEN
MATCH_MP_TAC(REAL_ARITH
`!g. abs(g) < Bg /\ abs(g - g') < e ==> abs(g') < Bg + e`) THEN
EXISTS_TAC `(g:real^N->real) x` THEN ASM_SIMP_TAC[]];
ALL_TAC] THEN
SUBGOAL_THEN
`!x y. x IN s /\ y IN s /\ ~(x = y)
==> ?f:real^N->real. A(f) /\ ~(f x = f y)`
(LABEL_TAC "sep") THENL
[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
MAP_EVERY EXPAND_TAC ["A"; "C"] THEN
ASM_MESON_TAC[REAL_SUB_REFL; REAL_ABS_0];
ALL_TAC] THEN
SUBGOAL_THEN `!f. A(f) ==> A(\x:real^N. abs(f x))` (LABEL_TAC "abs") THENL
[SUBGOAL_THEN `!f. A(f) /\ (!x. x IN s ==> abs(f x) <= &1 / &4)
==> A(\x:real^N. abs(f x))`
ASSUME_TAC THENL
[ALL_TAC;
REPEAT STRIP_TAC THEN
SUBGOAL_THEN `real_bounded(IMAGE (f:real^N->real) s)` MP_TAC THENL
[ASM_SIMP_TAC[]; REWRITE_TAC[REAL_BOUNDED_POS_LT; FORALL_IN_IMAGE]] THEN
DISCH_THEN(X_CHOOSE_THEN `B:real` STRIP_ASSUME_TAC) THEN
SUBGOAL_THEN `A(\x:real^N. (&4 * B) * abs(inv(&4 * B) * f x)):bool`
MP_TAC THENL
[USE_THEN "mul" MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN
FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_SIMP_TAC[REAL_ABS_MUL] THEN
ASM_SIMP_TAC[REAL_ARITH `&0 < B ==> abs(B) = B`;
REAL_LT_INV_EQ; REAL_LT_MUL; REAL_OF_NUM_LT; ARITH] THEN
ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
ASM_SIMP_TAC[GSYM real_div; REAL_LE_LDIV_EQ; REAL_LT_MUL;
REAL_OF_NUM_LT; ARITH; REAL_MUL_ASSOC] THEN
CONV_TAC REAL_RAT_REDUCE_CONV THEN
ASM_SIMP_TAC[REAL_MUL_LID; REAL_LT_IMP_LE];
ASM_SIMP_TAC[REAL_ABS_MUL; REAL_ARITH `&0 < B ==> abs(B) = B`;
REAL_LT_INV_EQ; REAL_LT_MUL; REAL_OF_NUM_LT; ARITH] THEN
ASM_SIMP_TAC[REAL_MUL_ASSOC; REAL_MUL_RINV; REAL_MUL_LID;
REAL_ARITH `&0 < B ==> ~(&4 * B = &0)`]]] THEN
X_GEN_TAC `f:real^N->real` THEN MAP_EVERY EXPAND_TAC ["A"; "C"] THEN
DISCH_THEN(fun th -> CONJ_TAC THEN MP_TAC th) THENL
[DISCH_THEN(MP_TAC o CONJUNCT1 o CONJUNCT1) THEN
MATCH_MP_TAC MONO_FORALL THEN GEN_TAC THEN MATCH_MP_TAC MONO_IMP THEN
REWRITE_TAC[] THEN
MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ_ALT; o_DEF]
REAL_CONTINUOUS_WITHIN_COMPOSE) THEN
REWRITE_TAC[real_continuous_withinreal] THEN
MESON_TAC[ARITH_RULE `abs(x - y) < d ==> abs(abs x - abs y) < d`];
ALL_TAC] THEN
DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
DISCH_THEN(fun t -> X_GEN_TAC `e:real` THEN DISCH_TAC THEN MP_TAC t) THEN
DISCH_THEN(MP_TAC o SPEC `min (e / &2) (&1 / &4)`) THEN
ANTS_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
REWRITE_TAC[REAL_LT_MIN; FORALL_AND_THM;
TAUT `(a ==> b /\ c) <=> (a ==> b) /\ (a ==> c)`] THEN
DISCH_THEN(X_CHOOSE_THEN `p:real^N->real` STRIP_ASSUME_TAC) THEN
MP_TAC(ISPECL [`\x. abs(x - &1 / &2)`; `e / &2`]
BERNSTEIN_WEIERSTRASS) THEN
REWRITE_TAC[] THEN ANTS_TAC THENL
[ASM_REWRITE_TAC[real_continuous_on; REAL_HALF] THEN
MESON_TAC[ARITH_RULE
`abs(x - y) < d ==> abs(abs(x - a) - abs(y - a)) < d`];
ALL_TAC] THEN
DISCH_THEN(X_CHOOSE_THEN `n:num` (MP_TAC o SPEC `n:num`)) THEN
REWRITE_TAC[LE_REFL] THEN DISCH_TAC THEN
EXISTS_TAC `\x:real^N. sum(0..n) (\k. abs(&k / &n - &1 / &2) *
bernstein n k (&1 / &2 + p x))` THEN
REWRITE_TAC[] THEN CONJ_TAC THENL
[SUBGOAL_THEN
`!m c z. P(\x:real^N.
sum(0..m) (\k. c k * bernstein (z m) k (&1 / &2 + p x)))`
(fun th -> REWRITE_TAC[th]) THEN
SUBGOAL_THEN
`!m k. P(\x:real^N. bernstein m k (&1 / &2 + p x))`
ASSUME_TAC THENL
[ALL_TAC; INDUCT_TAC THEN ASM_SIMP_TAC[SUM_CLAUSES_NUMSEG; LE_0]] THEN
REPEAT GEN_TAC THEN REWRITE_TAC[bernstein] THEN
REWRITE_TAC[REAL_ARITH `&1 - (&1 / &2 + p) = &1 / &2 + -- &1 * p`] THEN
REPEAT(FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]) THEN
SUBGOAL_THEN
`!f:real^N->real k. P(f) ==> P(\x. f(x) pow k)`
(fun th -> ASM_SIMP_TAC[th]) THEN
GEN_TAC THEN INDUCT_TAC THEN ASM_SIMP_TAC[real_pow];
REPEAT STRIP_TAC THEN MATCH_MP_TAC(REAL_ARITH
`!p. abs(abs(p x) - s) < e / &2 /\
abs(f x - p x) < e / &2
==> abs(abs(f x) - s) < e`) THEN
EXISTS_TAC `p:real^N->real` THEN ASM_SIMP_TAC[] THEN
GEN_REWRITE_TAC (PAT_CONV `\x. abs(abs x - a) < e`)
[REAL_ARITH `x = (&1 / &2 + x) - &1 / &2`] THEN
FIRST_X_ASSUM MATCH_MP_TAC THEN REWRITE_TAC[IN_REAL_INTERVAL] THEN
MATCH_MP_TAC(REAL_ARITH
`!f. abs(f) <= &1 / &4 /\ abs(f - p) < &1 / &4
==> &0 <= &1 / &2 + p /\ &1 / &2 + p <= &1`) THEN
EXISTS_TAC `(f:real^N->real) x` THEN ASM_SIMP_TAC[]];
ALL_TAC] THEN
SUBGOAL_THEN `!f:real^N->real g. A(f) /\ A(g) ==> A(\x. max (f x) (g x))`
(LABEL_TAC "max") THENL
[REPEAT STRIP_TAC THEN REWRITE_TAC[REAL_ARITH
`max a b = inv(&2) * (a + b + abs(a + -- &1 * b))`] THEN
REPEAT(FIRST_ASSUM MATCH_MP_TAC THEN ASM_SIMP_TAC[]);
ALL_TAC] THEN
SUBGOAL_THEN `!f:real^N->real g. A(f) /\ A(g) ==> A(\x. min (f x) (g x))`
(LABEL_TAC "min") THENL
[ASM_SIMP_TAC[REAL_ARITH `min a b = -- &1 * (max(-- &1 * a) (-- &1 * b))`];
ALL_TAC] THEN
SUBGOAL_THEN
`!t. FINITE t /\ (!f. f IN t ==> A(f)) ==> A(\x:real^N. sup {f(x) | f IN t})`
(LABEL_TAC "sup") THENL
[REWRITE_TAC[IMP_CONJ] THEN MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
ASM_SIMP_TAC[FORALL_IN_INSERT; SIMPLE_IMAGE; IMAGE_CLAUSES] THEN
ASM_SIMP_TAC[SUP_INSERT_FINITE; FINITE_IMAGE; IMAGE_EQ_EMPTY] THEN
MAP_EVERY X_GEN_TAC [`f:real^N->real`; `t:(real^N->real)->bool`] THEN
ASM_CASES_TAC `t:(real^N->real)->bool = {}` THEN ASM_SIMP_TAC[ETA_AX];
ALL_TAC] THEN
SUBGOAL_THEN
`!t. FINITE t /\ (!f. f IN t ==> A(f)) ==> A(\x:real^N. inf {f(x) | f IN t})`
(LABEL_TAC "inf") THENL
[REWRITE_TAC[IMP_CONJ] THEN MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
ASM_SIMP_TAC[FORALL_IN_INSERT; SIMPLE_IMAGE; IMAGE_CLAUSES] THEN
ASM_SIMP_TAC[INF_INSERT_FINITE; FINITE_IMAGE; IMAGE_EQ_EMPTY] THEN
MAP_EVERY X_GEN_TAC [`f:real^N->real`; `t:(real^N->real)->bool`] THEN
ASM_CASES_TAC `t:(real^N->real)->bool = {}` THEN ASM_SIMP_TAC[ETA_AX];
ALL_TAC] THEN
SUBGOAL_THEN
`!f:real^N->real e.
C(f) /\ &0 < e ==> ?g. A(g) /\ !x. x IN s ==> abs(f x - g x) < e`
ASSUME_TAC THENL
[ALL_TAC;
X_GEN_TAC `f:real^N->real` THEN DISCH_TAC THEN EXPAND_TAC "A" THEN
CONJ_TAC THENL [FIRST_X_ASSUM ACCEPT_TAC; ALL_TAC] THEN
X_GEN_TAC `e:real` THEN DISCH_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPECL [`f:real^N->real`; `e / &2`]) THEN
ASM_REWRITE_TAC[REAL_HALF; LEFT_IMP_EXISTS_THM] THEN
X_GEN_TAC `h:real^N->real` THEN EXPAND_TAC "A" THEN
DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
DISCH_THEN(MP_TAC o SPEC `e / &2` o CONJUNCT2) THEN
ASM_REWRITE_TAC[REAL_HALF] THEN MATCH_MP_TAC MONO_EXISTS THEN
ASM_MESON_TAC[REAL_ARITH
`abs(f - h) < e / &2 /\ abs(h - g) < e / &2 ==> abs(f - g) < e`]] THEN
MAP_EVERY X_GEN_TAC [`f:real^N->real`; `e:real`] THEN EXPAND_TAC "C" THEN
STRIP_TAC THEN
SUBGOAL_THEN
`!x y. x IN s /\ y IN s
==> ?h:real^N->real. A(h) /\ h(x) = f(x) /\ h(y) = f(y)`
MP_TAC THENL
[REPEAT STRIP_TAC THEN ASM_CASES_TAC `y:real^N = x` THENL
[EXISTS_TAC `\z:real^N. (f:real^N->real) x` THEN ASM_SIMP_TAC[];
SUBGOAL_THEN `?h:real^N->real. A(h) /\ ~(h x = h y)`
STRIP_ASSUME_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
EXISTS_TAC `\z. (f y - f x) / (h y - h x) * (h:real^N->real)(z) +
(f x - (f y - f x) / (h y - h x) * h(x))` THEN
ASM_SIMP_TAC[] THEN
UNDISCH_TAC `~((h:real^N->real) x = h y)` THEN CONV_TAC REAL_FIELD];
ALL_TAC] THEN
GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [RIGHT_IMP_EXISTS_THM] THEN
REWRITE_TAC[SKOLEM_THM; LEFT_IMP_EXISTS_THM] THEN
X_GEN_TAC `f2:real^N->real^N->real^N->real` THEN DISCH_TAC THEN
ABBREV_TAC `G = \x y.
{z | z IN s /\ (f2:real^N->real^N->real^N->real) x y z < f(z) + e}` THEN
SUBGOAL_THEN `!x y:real^N. x IN s /\ y IN s ==> x IN G x y /\ y IN G x y`
ASSUME_TAC THENL
[EXPAND_TAC "G" THEN REWRITE_TAC[IN_ELIM_THM] THEN
ASM_SIMP_TAC[REAL_LT_ADDR];
ALL_TAC] THEN
SUBGOAL_THEN
`!x. x IN s ==> ?f1. A(f1) /\ f1 x = f x /\
!y:real^N. y IN s ==> f1 y < f y + e`
MP_TAC THENL
[REPEAT STRIP_TAC THEN FIRST_ASSUM(MP_TAC o
GEN_REWRITE_RULE I [COMPACT_EQ_HEINE_BOREL_SUBTOPOLOGY]) THEN
DISCH_THEN(MP_TAC o SPEC
`{(G:real^N->real^N->real^N->bool) x y | y IN s}`) THEN
REWRITE_TAC[SIMPLE_IMAGE; UNIONS_IMAGE; FORALL_IN_IMAGE; ETA_AX] THEN
ANTS_TAC THENL
[CONJ_TAC THENL [ALL_TAC; ASM SET_TAC[]] THEN
EXPAND_TAC "G" THEN REWRITE_TAC[] THEN X_GEN_TAC `w:real^N` THEN
DISCH_TAC THEN
MP_TAC(ISPECL [`lift o (\z:real^N. f2 (x:real^N) (w:real^N) z - f z)`;
`s:real^N->bool`;
`{x:real^1 | x$1 < e}`] CONTINUOUS_OPEN_IN_PREIMAGE) THEN
REWRITE_TAC[OPEN_HALFSPACE_COMPONENT_LT; IN_ELIM_THM] THEN
REWRITE_TAC[GSYM drop; LIFT_DROP; o_DEF] THEN
REWRITE_TAC[LIFT_SUB; GSYM REAL_CONTINUOUS_CONTINUOUS1;
REAL_ARITH `x < y + e <=> x - y < e`] THEN
DISCH_THEN MATCH_MP_TAC THEN MATCH_MP_TAC CONTINUOUS_ON_SUB THEN
ONCE_REWRITE_TAC[GSYM o_DEF] THEN
REWRITE_TAC[CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN] THEN
REWRITE_TAC[GSYM REAL_CONTINUOUS_CONTINUOUS1; ETA_AX] THEN
ASM_MESON_TAC[];
ALL_TAC] THEN
ONCE_REWRITE_TAC[TAUT `a /\ b /\ c <=> b /\ a /\ c`] THEN
REWRITE_TAC[EXISTS_FINITE_SUBSET_IMAGE; UNIONS_IMAGE] THEN
DISCH_THEN(X_CHOOSE_THEN `t:real^N->bool` STRIP_ASSUME_TAC) THEN
EXISTS_TAC `\z:real^N. inf {f2 (x:real^N) (y:real^N) z | y IN t}` THEN
REWRITE_TAC[] THEN REPEAT CONJ_TAC THENL
[GEN_REWRITE_TAC RAND_CONV [REAL_ARITH `x = min x x`] THEN
REWRITE_TAC[REAL_MIN_INF; INSERT_AC] THEN AP_TERM_TAC THEN ASM SET_TAC[];
REMOVE_THEN "inf" (MP_TAC o SPEC
`IMAGE (\y z. (f2:real^N->real^N->real^N->real) x y z) t`) THEN
ASM_SIMP_TAC[FINITE_IMAGE; FORALL_IN_IMAGE] THEN
REWRITE_TAC[SIMPLE_IMAGE; ETA_AX] THEN
ANTS_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
REWRITE_TAC[GSYM IMAGE_o; o_DEF];
SUBGOAL_THEN `~(t:real^N->bool = {})` ASSUME_TAC THENL
[ASM SET_TAC[]; ALL_TAC] THEN
ASM_SIMP_TAC[REAL_INF_LT_FINITE; SIMPLE_IMAGE;
FINITE_IMAGE; IMAGE_EQ_EMPTY] THEN
REWRITE_TAC[EXISTS_IN_IMAGE] THEN
X_GEN_TAC `y:real^N` THEN DISCH_TAC THEN
UNDISCH_TAC
`s SUBSET {y:real^N | ?z:real^N. z IN t /\ y IN G (x:real^N) z}` THEN
REWRITE_TAC[SUBSET; IN_ELIM_THM] THEN
DISCH_THEN(MP_TAC o SPEC `y:real^N`) THEN ASM_REWRITE_TAC[] THEN
EXPAND_TAC "G" THEN REWRITE_TAC[IN_ELIM_THM] THEN ASM_REWRITE_TAC[]];
GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV)
[RIGHT_IMP_EXISTS_THM] THEN
REWRITE_TAC[SKOLEM_THM; LEFT_IMP_EXISTS_THM] THEN
X_GEN_TAC `f1:real^N->real^N->real` THEN DISCH_TAC] THEN
ABBREV_TAC `H = \x:real^N. {z:real^N | z IN s /\ f z - e < f1 x z}` THEN
SUBGOAL_THEN `!x:real^N. x IN s ==> x IN (H x)` ASSUME_TAC THENL
[EXPAND_TAC "H" THEN REWRITE_TAC[IN_ELIM_THM] THEN
ASM_SIMP_TAC[REAL_ARITH `x - e < x <=> &0 < e`];
ALL_TAC] THEN
FIRST_ASSUM(MP_TAC o
GEN_REWRITE_RULE I [COMPACT_EQ_HEINE_BOREL_SUBTOPOLOGY]) THEN
DISCH_THEN(MP_TAC o SPEC
`{(H:real^N->real^N->bool) x | x IN s}`) THEN
REWRITE_TAC[SIMPLE_IMAGE; UNIONS_IMAGE; FORALL_IN_IMAGE; ETA_AX] THEN
ANTS_TAC THENL
[CONJ_TAC THENL [ALL_TAC; ASM SET_TAC[]] THEN EXPAND_TAC "H" THEN
REWRITE_TAC[] THEN X_GEN_TAC `x:real^N` THEN DISCH_TAC THEN
MP_TAC(ISPECL [`lift o (\z:real^N. f z - f1 (x:real^N) z)`;
`s:real^N->bool`;
`{x:real^1 | x$1 < e}`] CONTINUOUS_OPEN_IN_PREIMAGE) THEN
REWRITE_TAC[OPEN_HALFSPACE_COMPONENT_LT; IN_ELIM_THM] THEN
REWRITE_TAC[GSYM drop; LIFT_DROP; o_DEF] THEN
GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV)
[REAL_ARITH `x - y < z <=> x - z < y`] THEN
DISCH_THEN MATCH_MP_TAC THEN
REWRITE_TAC[LIFT_SUB; GSYM REAL_CONTINUOUS_CONTINUOUS1;
REAL_ARITH `x < y + e <=> x - y < e`] THEN
MATCH_MP_TAC CONTINUOUS_ON_SUB THEN
ONCE_REWRITE_TAC[GSYM o_DEF] THEN
REWRITE_TAC[CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN] THEN
REWRITE_TAC[GSYM REAL_CONTINUOUS_CONTINUOUS1; ETA_AX] THEN
ASM_MESON_TAC[];
ALL_TAC] THEN
ONCE_REWRITE_TAC[TAUT `a /\ b /\ c <=> b /\ a /\ c`] THEN
REWRITE_TAC[EXISTS_FINITE_SUBSET_IMAGE; UNIONS_IMAGE] THEN
DISCH_THEN(X_CHOOSE_THEN `t:real^N->bool` STRIP_ASSUME_TAC) THEN
EXISTS_TAC `\z:real^N. sup {f1 (x:real^N) z | x IN t}` THEN
REWRITE_TAC[] THEN CONJ_TAC THENL
[REMOVE_THEN "sup" (MP_TAC o SPEC `IMAGE (f1:real^N->real^N->real) t`) THEN
ASM_SIMP_TAC[FINITE_IMAGE; FORALL_IN_IMAGE] THEN
REWRITE_TAC[SIMPLE_IMAGE; ETA_AX] THEN
ANTS_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
REWRITE_TAC[GSYM IMAGE_o; o_DEF];
ALL_TAC] THEN
X_GEN_TAC `x:real^N` THEN DISCH_TAC THEN
SUBGOAL_THEN `~(t:real^N->bool = {})` ASSUME_TAC THENL
[ASM SET_TAC[]; ALL_TAC] THEN
REWRITE_TAC[SIMPLE_IMAGE; REAL_ARITH
`abs(f - s) < e <=> f - e < s /\ s < f + e`] THEN
ASM_SIMP_TAC[REAL_SUP_LT_FINITE; REAL_LT_SUP_FINITE;
FINITE_IMAGE; IMAGE_EQ_EMPTY] THEN
REWRITE_TAC[EXISTS_IN_IMAGE; FORALL_IN_IMAGE] THEN
CONJ_TAC THENL [ALL_TAC; ASM SET_TAC[]] THEN
UNDISCH_TAC `s SUBSET {y:real^N | ?x:real^N. x IN t /\ y IN H x}` THEN
REWRITE_TAC[SUBSET; IN_ELIM_THM] THEN
DISCH_THEN(MP_TAC o SPEC `x:real^N`) THEN ASM_REWRITE_TAC[] THEN
EXPAND_TAC "H" THEN REWRITE_TAC[IN_ELIM_THM] THEN ASM_REWRITE_TAC[]);;
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[]);;
(* ------------------------------------------------------------------------- *)
(* Real and complex versions of Stone-Weierstrass theorem. *)
(* ------------------------------------------------------------------------- *)
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[]);;
(* ------------------------------------------------------------------------- *)
(* Stone-Weierstrass for R^n -> R polynomials. *)
(* ------------------------------------------------------------------------- *)
let real_polynomial_function_RULES,
real_polynomial_function_INDUCT,
real_polynomial_function_CASES = new_inductive_definition
`(!i. 1 <= i /\ i <= dimindex(:N)
==> real_polynomial_function(\x:real^N. x$i)) /\
(!c. real_polynomial_function(\x:real^N. c)) /\
(!f g. real_polynomial_function f /\ real_polynomial_function g
==> real_polynomial_function(\x:real^N. f x + g x)) /\
(!f g. real_polynomial_function f /\ real_polynomial_function g
==> real_polynomial_function(\x:real^N. f x * g x))`;;
(* ------------------------------------------------------------------------- *)
(* Stone-Weierstrass for real^M->real^N polynomials. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* One application is to pick a smooth approximation to a path, or just pick *)
(* a smooth path anyway in an open connected set. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Lipschitz property for real and vector polynomials. *)
(* ------------------------------------------------------------------------- *)
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[]]]);;
(* ------------------------------------------------------------------------- *)
(* Differentiability of real and vector polynomial functions. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Non-trivial algebraic variety has empty interior. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Bernoulli polynomials, defined recursively. We don't explicitly introduce *)
(* a definition for Bernoulli numbers, but use "bernoulli n (&0)" for that. *)
(* ------------------------------------------------------------------------- *)
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 BERNOULLI_CONV =
let btm = `bernoulli` in
let rec bernoullis n =
if n < 0 then [] else
if n = 0 then [CONJUNCT1 bernoulli] else
let ths = bernoullis (n - 1) in
let th1 = SPEC(mk_small_numeral (n - 1)) (CONJUNCT2 bernoulli) in
let th2 =
CONV_RULE(BINDER_CONV (COMB2_CONV (RAND_CONV(LAND_CONV NUM_ADD_CONV))
(RAND_CONV(LAND_CONV EXPAND_SUM_CONV) THENC
NUM_REDUCE_CONV THENC
ONCE_DEPTH_CONV NUM_BINOM_CONV THENC
REWRITE_CONV ths THENC
REAL_POLY_CONV))) th1 in
th2::ths in
fun tm -> match tm with
Comb(Comb(b,n),x) when b = btm ->
let th = hd(bernoullis(dest_small_numeral n)) in
(REWR_CONV th THENC REAL_POLY_CONV) tm
| _ -> failwith "BERNOULLI_CONV";;
let BERNOULLI,BERNOULLI_EXPANSION = (CONJ_PAIR o prove)
(`(!n x. sum(0..n) (\k. &(binom(n,k)) * bernoulli k x) - bernoulli n x =
&n * x pow (n - 1)) /\
(!n x. bernoulli n x =
sum(0..n) (\k. &(binom(n,k)) * bernoulli k (&0) * x pow (n - k)))`,
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)`,
add_real_differentiation_theorems
(CONJUNCTS(REWRITE_RULE[FORALL_AND_THM]
(MATCH_MP HAS_REAL_DERIVATIVE_CHAIN_UNIV
(SPEC `n:num` HAS_REAL_DERIVATIVE_BERNOULLI))));;
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);;
(* ------------------------------------------------------------------------- *)
(* This is a simple though sub-optimal bound (we can actually get *)
(* |B_{2n+1}(x)| <= (2n + 1) / (2 pi) * |B_{2n}(0)| with more work). *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Absolutely integrable functions remain so modified by Bernolli sawtooth. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* The Euler-Maclaurin summation formula for real and complex functions. *)
(* ------------------------------------------------------------------------- *)
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)))`,
(* ------------------------------------------------------------------------- *)
(* Specific properties of complex measurable functions. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Measurable real->real functions. *)
(* ------------------------------------------------------------------------- *)
parse_as_infix("real_measurable_on",(12,"right"));;
(* ------------------------------------------------------------------------- *)
(* Properties of real Lebesgue measurable sets. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Various common equivalent forms of function measurability. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Continuity of measure within a halfspace w.r.t. to the boundary. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Second mean value theorem and monotone integrability. *)
(* ------------------------------------------------------------------------- *)
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`,
(* ------------------------------------------------------------------------- *)
(* Measurability and absolute integrability of monotone functions. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Real functions of bounded variation. *)
(* ------------------------------------------------------------------------- *)
parse_as_infix("has_bounded_real_variation_on",(12,"right"));;
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]))`,
(* ------------------------------------------------------------------------- *)
(* Lebesgue density theorem. This isn't about R specifically, but it's most *)
(* naturally stated as a real limit so it ends up here in this file. *)
(* ------------------------------------------------------------------------- *)