(* ========================================================================= *)
(* Elementary topology in Euclidean space. *)
(* *)
(* (c) Copyright, John Harrison 1998-2008 *)
(* (c) Copyright, Valentina Bruno 2010 *)
(* ========================================================================= *)
needs "Library/card.ml";;
needs "Multivariate/determinants.ml";;
(* ------------------------------------------------------------------------- *)
(* General notion of a topology. *)
(* ------------------------------------------------------------------------- *)
let topology_tybij =
new_type_definition "topology" ("topology","open_in") topology_tybij_th;;
let TOPOLOGY_EQ = prove
(`!top1 top2. top1 = top2 <=> !s.
open_in top1 s <=>
open_in top2 s`,
REPEAT GEN_TAC THEN GEN_REWRITE_TAC RAND_CONV [GSYM
FUN_EQ_THM] THEN
REWRITE_TAC[ETA_AX] THEN MESON_TAC[topology_tybij]);;
let open_def = new_definition
`open s <=> !x. x IN s ==> ?e. &0 < e /\ !x'. dist(x',x) < e ==> x' IN s`;;
let OPEN_EXISTS_IN = prove
(`!P Q:A->real^N->bool.
(!a. P a ==> open {x | Q a x}) ==> open {x | ?a. P a /\ Q a x}`,
REPEAT STRIP_TAC THEN
SUBGOAL_THEN `open(
UNIONS {{x | Q (a:A) (x:real^N)} | P a})` MP_TAC THENL
[MATCH_MP_TAC
OPEN_UNIONS THEN ASM_REWRITE_TAC[
FORALL_IN_GSPEC];
MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC THEN REWRITE_TAC[
UNIONS_GSPEC] THEN
SET_TAC[]]);;
let OPEN_EXISTS = prove
(`!Q:A->real^N->bool. (!a. open {x | Q a x}) ==> open {x | ?a. Q a x}`,
let CONNECTED_UNIONS = prove
(`!P:(real^N->bool)->bool.
(!s. s
IN P ==>
connected s) /\ ~(
INTERS P = {})
==>
connected(
UNIONS P)`,
GEN_TAC THEN REWRITE_TAC[
connected;
NOT_EXISTS_THM] THEN STRIP_TAC THEN
MAP_EVERY X_GEN_TAC [`e1:real^N->bool`; `e2:real^N->bool`] THEN
STRIP_TAC THEN UNDISCH_TAC `~(
INTERS P :real^N->bool = {})` THEN
PURE_REWRITE_TAC[GSYM
MEMBER_NOT_EMPTY;
IN_INTERS] THEN
DISCH_THEN(X_CHOOSE_THEN `a:real^N` STRIP_ASSUME_TAC) THEN
SUBGOAL_THEN `(a:real^N)
IN e1 \/ a
IN e2` STRIP_ASSUME_TAC THENL
[ASM SET_TAC[];
UNDISCH_TAC `~(e2
INTER UNIONS P:real^N->bool = {})`;
UNDISCH_TAC `~(e1
INTER UNIONS P:real^N->bool = {})`] THEN
PURE_REWRITE_TAC[GSYM
MEMBER_NOT_EMPTY;
IN_INTER;
IN_UNIONS] THEN
DISCH_THEN(X_CHOOSE_THEN `b:real^N`
(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
DISCH_THEN(X_CHOOSE_THEN `s:real^N->bool` STRIP_ASSUME_TAC) THEN
UNDISCH_TAC `!t:real^N->bool. t
IN P ==> a
IN t` THEN
DISCH_THEN(MP_TAC o SPEC `s:real^N->bool`) THEN
ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPEC `s:real^N->bool`) THEN
ASM_REWRITE_TAC[] THEN
DISCH_THEN(MP_TAC o SPECL [`e1:real^N->bool`; `e2:real^N->bool`]) THEN
ASM SET_TAC[]);;
let CONNECTED_DIFF_OPEN_FROM_CLOSED = prove
(`!s t u:real^N->bool.
s
SUBSET t /\ t
SUBSET u /\
open s /\
closed t /\
connected u /\
connected(t
DIFF s)
==>
connected(u
DIFF s)`,
REPEAT STRIP_TAC THEN REWRITE_TAC[
connected;
NOT_EXISTS_THM] THEN
MAP_EVERY X_GEN_TAC [`v:real^N->bool`; `w:real^N->bool`] THEN STRIP_TAC THEN
UNDISCH_TAC `
connected(t
DIFF s:real^N->bool)` THEN SIMP_TAC[
connected] THEN
MAP_EVERY EXISTS_TAC [`v:real^N->bool`; `w:real^N->bool`] THEN
ASM_REWRITE_TAC[] THEN
REPLICATE_TAC 2 (CONJ_TAC THENL [ASM SET_TAC[]; ALL_TAC]) THEN
POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN
MAP_EVERY (fun t -> SPEC_TAC(t,t)) [`v:real^N->bool`; `w:real^N->bool`] THEN
MATCH_MP_TAC(MESON[]
`(!v w. P v w ==> P w v) /\ (!w v. P v w /\ Q w ==> F)
==> !w v. P v w ==> ~(Q v) /\ ~(Q w)`) THEN
CONJ_TAC THENL [SIMP_TAC[
CONJ_ACI;
INTER_ACI;
UNION_ACI]; ALL_TAC] THEN
REPEAT STRIP_TAC THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [
connected]) THEN SIMP_TAC[] THEN
MAP_EVERY EXISTS_TAC [`v
UNION s:real^N->bool`; `w
DIFF t:real^N->bool`] THEN
ASM_SIMP_TAC[
OPEN_UNION;
OPEN_DIFF] THEN ASM SET_TAC[]);;
let CONNECTED_DISJOINT_UNIONS_OPEN_UNIQUE = prove
(`!f:(real^N->bool)->bool f'.
pairwise DISJOINT f /\
pairwise DISJOINT f' /\
(!s. s
IN f ==> open s /\
connected s /\ ~(s = {})) /\
(!s. s
IN f' ==> open s /\
connected s /\ ~(s = {})) /\
UNIONS f =
UNIONS f'
==> f = f'`,
GEN_REWRITE_TAC (funpow 2 BINDER_CONV o RAND_CONV) [
EXTENSION] THEN
MATCH_MP_TAC(MESON[]
`(!s t. P s t ==> P t s) /\ (!s t x. P s t /\ x
IN s ==> x
IN t)
==> (!s t. P s t ==> (!x. x
IN s <=> x
IN t))`) THEN
CONJ_TAC THENL [MESON_TAC[]; ALL_TAC] THEN
GEN_TAC THEN GEN_TAC THEN X_GEN_TAC `s:real^N->bool` THEN STRIP_TAC THEN
SUBGOAL_THEN
`?t a:real^N. t
IN f' /\ a
IN s /\ a
IN t` STRIP_ASSUME_TAC
THENL [ASM SET_TAC[]; ALL_TAC] THEN
SUBGOAL_THEN `s:real^N->bool = t` (fun
th -> ASM_REWRITE_TAC[
th]) THEN
REWRITE_TAC[
EXTENSION] THEN POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN
MAP_EVERY (fun t -> SPEC_TAC(t,t))
[`s:real^N->bool`; `t:real^N->bool`;
`f:(real^N->bool)->bool`; `f':(real^N->bool)->bool`] THEN
MATCH_MP_TAC(MESON[]
`(!f f' s t. P f f' s t ==> P f' f t s) /\
(!f f' s t x. P f f' s t /\ x
IN s ==> x
IN t)
==> (!f' f t s. P f f' s t ==> (!x. x
IN s <=> x
IN t))`) THEN
CONJ_TAC THENL [MESON_TAC[]; ALL_TAC] THEN
REPLICATE_TAC 4 GEN_TAC THEN X_GEN_TAC `b:real^N` THEN STRIP_TAC THEN
UNDISCH_TAC
`!s:real^N->bool. s
IN f ==> open s /\
connected s /\ ~(s = {})` THEN
DISCH_THEN(MP_TAC o SPEC `s:real^N->bool`) THEN ASM_REWRITE_TAC[] THEN
STRIP_TAC THEN ASM_CASES_TAC `(b:real^N)
IN t` THEN
ASM_REWRITE_TAC[] THEN
UNDISCH_TAC `
connected(s:real^N->bool)` THEN
REWRITE_TAC[
connected] THEN
MAP_EVERY EXISTS_TAC
[`t:real^N->bool`; `
UNIONS(f'
DELETE (t:real^N->bool))`] THEN
REPEAT STRIP_TAC THENL
[ASM_SIMP_TAC[];
MATCH_MP_TAC
OPEN_UNIONS THEN ASM_SIMP_TAC[
IN_DELETE];
REWRITE_TAC[GSYM
UNIONS_INSERT] THEN ASM SET_TAC[];
MATCH_MP_TAC(SET_RULE `t
INTER u = {} ==> t
INTER u
INTER s = {}`) THEN
REWRITE_TAC[
INTER_UNIONS;
EMPTY_UNIONS;
FORALL_IN_GSPEC] THEN
REWRITE_TAC[
IN_DELETE; GSYM
DISJOINT] THEN ASM_MESON_TAC[
pairwise];
ASM SET_TAC[];
ASM SET_TAC[]]);;
let FINITE_SET_AVOID = prove
(`!a:real^N s. FINITE s
==> ?d. &0 < d /\ !x. x
IN s /\ ~(x = a) ==> d <=
dist(a,x)`,
GEN_TAC THEN MATCH_MP_TAC
FINITE_INDUCT_STRONG THEN
REWRITE_TAC[
NOT_IN_EMPTY] THEN
CONJ_TAC THENL [MESON_TAC[
REAL_LT_01]; ALL_TAC] THEN
MAP_EVERY X_GEN_TAC [`x:real^N`; `s:real^N->bool`] THEN
DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN
FIRST_X_ASSUM(X_CHOOSE_THEN `d:real` STRIP_ASSUME_TAC) THEN
ASM_CASES_TAC `x:real^N = a` THEN REWRITE_TAC[
IN_INSERT] THENL
[ASM_MESON_TAC[]; ALL_TAC] THEN
EXISTS_TAC `min d (
dist(a:real^N,x))` THEN
ASM_REWRITE_TAC[
REAL_LT_MIN; GSYM
DIST_NZ;
REAL_MIN_LE] THEN
ASM_MESON_TAC[
REAL_LE_REFL]);;
let DISCRETE_IMP_CLOSED = prove
(`!s:real^N->bool e.
&0 < e /\
(!x y. x
IN s /\ y
IN s /\
norm(y - x) < e ==> y = x)
==>
closed s`,
REPEAT STRIP_TAC THEN
SUBGOAL_THEN `!x:real^N. ~(x
limit_point_of s)`
(fun
th -> MESON_TAC[
th;
CLOSED_LIMPT]) THEN
GEN_TAC THEN REWRITE_TAC[
LIMPT_APPROACHABLE] THEN DISCH_TAC THEN
FIRST_ASSUM(MP_TAC o SPEC `e / &2`) THEN
REWRITE_TAC[
REAL_HALF; ASSUME `&0 < e`] THEN
DISCH_THEN(X_CHOOSE_THEN `y:real^N` STRIP_ASSUME_TAC) THEN
FIRST_X_ASSUM(MP_TAC o SPEC `min (e / &2) (
dist(x:real^N,y))`) THEN
ASM_SIMP_TAC[
REAL_LT_MIN;
DIST_POS_LT;
REAL_HALF] THEN
DISCH_THEN(X_CHOOSE_THEN `z:real^N` STRIP_ASSUME_TAC) THEN
FIRST_X_ASSUM(MP_TAC o SPECL [`y:real^N`; `z:real^N`]) THEN
ASM_REWRITE_TAC[] THEN ASM_NORM_ARITH_TAC);;
let LIMPT_OF_OPEN_IN = prove
(`!s t x:real^N.
open_in (
subtopology euclidean s) t /\ x
limit_point_of s /\ x
IN t
==> x
limit_point_of t`,
REWRITE_TAC[
open_in;
SUBSET;
LIMPT_APPROACHABLE] THEN
REPEAT GEN_TAC THEN STRIP_TAC THEN X_GEN_TAC `e:real` THEN DISCH_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPEC `x:real^N`) THEN ASM_REWRITE_TAC[] THEN
DISCH_THEN(X_CHOOSE_THEN `d:real` STRIP_ASSUME_TAC) THEN
FIRST_X_ASSUM(MP_TAC o SPEC `min d e / &2`) THEN
ANTS_TAC THENL [ASM_REAL_ARITH_TAC; MATCH_MP_TAC
MONO_EXISTS] THEN
GEN_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN CONJ_TAC THEN
TRY(FIRST_X_ASSUM MATCH_MP_TAC) THEN ASM_REWRITE_TAC[] THEN
ASM_REAL_ARITH_TAC);;
let NET = prove
(`!n x y. (!z. netord n z x ==> netord n z y) \/
(!z. netord n z y ==> netord n z x)`,
REWRITE_TAC[net_tybij; ETA_AX]);;
let OLDNET = prove
(`!n x y. netord n x x /\ netord n y y
==> ?z. netord n z z /\
!w. netord n w z ==> netord n w x /\ netord n w y`,
let NET_DILEMMA = prove
(`!net. (?a. (?x. netord net x a) /\ (!x. netord net x a ==> P x)) /\
(?b. (?x. netord net x b) /\ (!x. netord net x b ==> Q x))
==> ?c. (?x. netord net x c) /\ (!x. netord net x c ==> P x /\ Q x)`,
let within = new_definition
`net within s = mk_net(\x y. netord net x y /\ x IN s)`;;
let WITHIN = prove
(`!n s x y. netord(n
within s) x y <=> netord n x y /\ x
IN s`,
GEN_TAC THEN GEN_TAC THEN REWRITE_TAC[
within; GSYM
FUN_EQ_THM] THEN
REWRITE_TAC[GSYM(CONJUNCT2 net_tybij); ETA_AX] THEN
MESON_TAC[
NET]);;
let lim = new_definition
`lim net f = @l. (f --> l) net`;;
let LIM = prove
(`(f --> l) net <=>
trivial_limit net \/
!e. &0 < e ==> ?y. (?x. netord(net) x y) /\
!x. netord(net) x y ==>
dist(f(x),l) < e`,
let LIM_AT = prove
(`!f l:real^N a:real^M.
(f --> l) (
at a) <=>
!e. &0 < e
==> ?d. &0 < d /\ !x. &0 <
dist(x,a) /\
dist(x,a) < d
==>
dist(f(x),l) < e`,
let LIM_COMPOSE_AT = prove
(`!net f:real^M->real^N g:real^N->real^P y z.
(f --> y) net /\
eventually (\w. f w = y ==> g y = z) net /\
(g --> z) (
at y)
==> ((g o f) --> z) net`,
REPEAT STRIP_TAC THEN
MP_TAC(ISPECL [`net:(real^M)net`; `f:real^M->real^N`; `g:real^N->real^P`;
`(:real^N)`; `y:real^N`; `z:real^P`]
LIM_COMPOSE_WITHIN) THEN
ASM_REWRITE_TAC[
IN_UNIV;
WITHIN_UNIV]);;
let LIM_WITHIN_OPEN = prove
(`!f l a:real^M s.
a
IN s /\ open s ==> ((f --> l)(
at a
within s) <=> (f --> l)(
at a))`,
REPEAT STRIP_TAC THEN EQ_TAC THEN SIMP_TAC[
LIM_AT_WITHIN] THEN
REWRITE_TAC[
LIM_AT;
LIM_WITHIN] 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 `d1:real` STRIP_ASSUME_TAC) THEN
FIRST_X_ASSUM(MP_TAC o SPEC `a:real^M` o GEN_REWRITE_RULE I [
open_def]) THEN
ASM_REWRITE_TAC[] THEN
DISCH_THEN(X_CHOOSE_THEN `d2:real` STRIP_ASSUME_TAC) THEN
MP_TAC(SPECL [`d1:real`; `d2:real`]
REAL_DOWN2) THEN ASM_REWRITE_TAC[] THEN
ASM_MESON_TAC[
REAL_LT_TRANS]);;
let LIM_CMUL = prove
(`!f l c. (f --> l) net ==> ((\x. c % f x) --> c % l) net`,
let LIM_CMUL_EQ = prove
(`!net f l c.
~(c = &0) ==> (((\x. c % f x) --> c % l) net <=> (f --> l) net)`,
let LIM_NEG = prove
(`!net f l:real^N. (f --> l) net ==> ((\x. --(f x)) --> --l) net`,
REPEAT GEN_TAC THEN REWRITE_TAC[
LIM;
dist] THEN
REWRITE_TAC[VECTOR_ARITH `--x - --y = --(x - y:real^N)`;
NORM_NEG]);;
let LIM_NEG_EQ = prove
(`!net f l:real^N. ((\x. --(f x)) --> --l) net <=> (f --> l) net`,
REPEAT GEN_TAC THEN EQ_TAC THEN
DISCH_THEN(MP_TAC o MATCH_MP
LIM_NEG) THEN
REWRITE_TAC[
VECTOR_NEG_NEG; ETA_AX]);;
let LIM_ADD = prove
(`!net:(A)net f g l m.
(f --> l) net /\ (g --> m) net ==> ((\x. f(x) + g(x)) --> l + m) net`,
let LIM_ABS = prove
(`!net:(A)net f:A->real^N l.
(f --> l) net
==> ((\x.
lambda i. (abs(f(x)$i))) --> (
lambda i. abs(l$i)):real^N) net`,
let LIM_SUB = prove
(`!net:(A)net f g l m.
(f --> l) net /\ (g --> m) net ==> ((\x. f(x) - g(x)) --> l - m) net`,
let LIM_MAX = prove
(`!net:(A)net f g l:real^N m:real^N.
(f --> l) net /\ (g --> m) net
==> ((\x.
lambda i. max (f(x)$i) (g(x)$i))
--> (
lambda i. max (l$i) (m$i)):real^N) net`,
let LIM_MIN = prove
(`!net:(A)net f g l:real^N m:real^N.
(f --> l) net /\ (g --> m) net
==> ((\x.
lambda i. min (f(x)$i) (g(x)$i))
--> (
lambda i. min (l$i) (m$i)):real^N) net`,
let LIM_VSUM = prove
(`!f:A->B->real^N s.
FINITE s /\ (!i. i
IN s ==> ((f i) --> (l i)) net)
==> ((\x.
vsum s (\i. f i x)) -->
vsum s l) net`,
let LIM_CONST_EQ = prove
(`!net:(A net) c d:real^N.
((\x. c) --> d) net <=>
trivial_limit net \/ c = d`,
REPEAT GEN_TAC THEN
ASM_CASES_TAC `
trivial_limit (net:A net)` THEN ASM_REWRITE_TAC[] THENL
[ASM_REWRITE_TAC[
LIM]; ALL_TAC] THEN
EQ_TAC THEN SIMP_TAC[
LIM_CONST] THEN DISCH_TAC THEN
MATCH_MP_TAC(SPEC `net:A net`
LIM_UNIQUE) THEN
EXISTS_TAC `(\x. c):A->real^N` THEN ASM_REWRITE_TAC[
LIM_CONST]);;
let LIM_BILINEAR = prove
(`!net:(A)net (h:real^M->real^N->real^P) f g l m.
(f --> l) net /\ (g --> m) net /\
bilinear h
==> ((\x. h (f x) (g x)) --> (h l m)) net`,
REPEAT STRIP_TAC THEN
MP_TAC(ISPECL
[`net:(A)net`; `\x:one. T`; `h:real^M->real^N->real^P`;
`\n:one. (f:A->real^M)`; `\n:one. (g:A->real^N)`;
`\n:one. (l:real^M)`; `\n:one. (m:real^N)`;
`
norm(l:real^M)`; `
norm(m:real^N)`]
UNIFORM_LIM_BILINEAR) THEN
ASM_REWRITE_TAC[
REAL_LE_REFL;
EVENTUALLY_TRUE] THEN
ASM_REWRITE_TAC[GSYM
dist; GSYM
tendsto]);;
let LIM_AT_ZERO = prove
(`!f:real^M->real^N l a.
(f --> l) (
at a) <=> ((\x. f(a + x)) --> l) (
at(
vec 0))`,
REPEAT GEN_TAC THEN REWRITE_TAC[
LIM_AT] THEN
AP_TERM_TAC THEN ABS_TAC THEN
ASM_CASES_TAC `&0 < e` THEN ASM_REWRITE_TAC[] THEN
AP_TERM_TAC THEN ABS_TAC THEN
ASM_CASES_TAC `&0 < d` THEN ASM_REWRITE_TAC[] THEN
EQ_TAC THEN DISCH_TAC THEN X_GEN_TAC `x:real^M` THENL
[FIRST_X_ASSUM(MP_TAC o SPEC `a + x:real^M`) THEN
REWRITE_TAC[
dist;
VECTOR_ADD_SUB;
VECTOR_SUB_RZERO];
FIRST_X_ASSUM(MP_TAC o SPEC `x - a:real^M`) THEN
REWRITE_TAC[
dist;
VECTOR_SUB_RZERO;
VECTOR_SUB_ADD2]]);;
let LIM_TRANSFORM = prove
(`!net f g l.
((\x. f x - g x) -->
vec 0) net /\ (f --> l) net ==> (g --> l) net`,
REPEAT GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP
LIM_SUB) THEN
DISCH_THEN(MP_TAC o MATCH_MP
LIM_NEG) THEN MATCH_MP_TAC EQ_IMP THEN
AP_THM_TAC THEN BINOP_TAC THEN REWRITE_TAC[
FUN_EQ_THM] THEN
VECTOR_ARITH_TAC);;
let LIM_TRANSFORM_EQ = prove
(`!net f:A->real^N g l.
((\x. f x - g x) -->
vec 0) net ==> ((f --> l) net <=> (g --> l) net)`,
REPEAT STRIP_TAC THEN EQ_TAC THEN
DISCH_TAC THEN MATCH_MP_TAC
LIM_TRANSFORM THENL
[EXISTS_TAC `f:A->real^N` THEN ASM_REWRITE_TAC[];
EXISTS_TAC `g:A->real^N` THEN ASM_REWRITE_TAC[] THEN
ONCE_REWRITE_TAC[GSYM
LIM_NEG_EQ] THEN
ASM_REWRITE_TAC[
VECTOR_NEG_SUB;
VECTOR_NEG_0]]);;
let LIM_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;
LIM_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 SPHERE_EQ_SING = prove
(`!a:real^N r x.
sphere(a,r) = {x} <=> x = a /\ r = &0`,
REPEAT GEN_TAC THEN EQ_TAC THEN SIMP_TAC[
SPHERE_SING] THEN
ASM_CASES_TAC `r < &0` THEN ASM_SIMP_TAC[
SPHERE_EMPTY;
NOT_INSERT_EMPTY] THEN
ASM_CASES_TAC `r = &0` THEN ASM_SIMP_TAC[
SPHERE_SING] THENL
[ASM SET_TAC[]; ALL_TAC] THEN
MATCH_MP_TAC(SET_RULE
`!y. (x
IN s ==> y
IN s /\ ~(y = x)) ==> ~(s = {x})`) THEN
EXISTS_TAC `a - (x - a):real^N` THEN REWRITE_TAC[
IN_SPHERE] THEN
REPEAT(POP_ASSUM MP_TAC) THEN CONV_TAC NORM_ARITH);;
let BOUNDED_TRANSLATION = prove
(`!a:real^N s.
bounded s ==>
bounded (
IMAGE (\x. a + x) s)`,
REPEAT GEN_TAC THEN REWRITE_TAC[
BOUNDED_POS;
FORALL_IN_IMAGE] THEN
DISCH_THEN(X_CHOOSE_TAC `B:real`) THEN
EXISTS_TAC `B +
norm(a:real^N)` THEN POP_ASSUM MP_TAC THEN
MATCH_MP_TAC MONO_AND THEN CONJ_TAC THENL [NORM_ARITH_TAC; ALL_TAC] THEN
MATCH_MP_TAC
MONO_FORALL THEN GEN_TAC THEN MATCH_MP_TAC MONO_IMP THEN
REWRITE_TAC[] THEN NORM_ARITH_TAC);;
let BOUNDED_DIFFS = prove
(`!s t:real^N->bool.
bounded s /\
bounded t ==>
bounded {x - y | x
IN s /\ y
IN t}`,
REPEAT GEN_TAC THEN REWRITE_TAC[
BOUNDED_POS] THEN
DISCH_THEN(CONJUNCTS_THEN2
(X_CHOOSE_TAC `B:real`) (X_CHOOSE_TAC `C:real`)) THEN
EXISTS_TAC `B + C:real` THEN REWRITE_TAC[
IN_ELIM_THM] THEN
CONJ_TAC THENL [ASM_REAL_ARITH_TAC; REPEAT STRIP_TAC] THEN
ASM_REWRITE_TAC[] THEN MATCH_MP_TAC(NORM_ARITH
`
norm x <= a /\
norm y <= b ==>
norm(x - y) <= a + b`) THEN
ASM_SIMP_TAC[]);;
let BOUNDED_SUMS = prove
(`!s t:real^N->bool.
bounded s /\
bounded t ==>
bounded {x + y | x
IN s /\ y
IN t}`,
REPEAT GEN_TAC THEN REWRITE_TAC[
BOUNDED_POS] THEN
DISCH_THEN(CONJUNCTS_THEN2
(X_CHOOSE_TAC `B:real`) (X_CHOOSE_TAC `C:real`)) THEN
EXISTS_TAC `B + C:real` THEN REWRITE_TAC[
IN_ELIM_THM] THEN
CONJ_TAC THENL [ASM_REAL_ARITH_TAC; REPEAT STRIP_TAC] THEN
ASM_REWRITE_TAC[] THEN MATCH_MP_TAC(NORM_ARITH
`
norm x <= a /\
norm y <= b ==>
norm(x + y) <= a + b`) THEN
ASM_SIMP_TAC[]);;
let BOUNDED_SUBSET_BALL = prove
(`!s x:real^N.
bounded(s) ==> ?r. &0 < r /\ s
SUBSET ball(x,r)`,
REPEAT GEN_TAC THEN REWRITE_TAC[
BOUNDED_POS] THEN
DISCH_THEN(X_CHOOSE_THEN `B:real` STRIP_ASSUME_TAC) THEN
EXISTS_TAC `&2 * B +
norm(x:real^N)` THEN
ASM_SIMP_TAC[
NORM_POS_LE; REAL_ARITH
`&0 < B /\ &0 <= x ==> &0 < &2 * B + x`] THEN
REWRITE_TAC[
SUBSET] THEN X_GEN_TAC `y:real^N` THEN DISCH_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPEC `y:real^N`) THEN ASM_REWRITE_TAC[
IN_BALL] THEN
UNDISCH_TAC `&0 < B` THEN NORM_ARITH_TAC);;
let SUBSET_BALLS = prove
(`(!a a':real^N r r'.
ball(a,r)
SUBSET ball(a',r') <=>
dist(a,a') + r <= r' \/ r <= &0) /\
(!a a':real^N r r'.
ball(a,r)
SUBSET cball(a',r') <=>
dist(a,a') + r <= r' \/ r <= &0) /\
(!a a':real^N r r'.
cball(a,r)
SUBSET ball(a',r') <=>
dist(a,a') + r < r' \/ r < &0) /\
(!a a':real^N r r'.
cball(a,r)
SUBSET cball(a',r') <=>
dist(a,a') + r <= r' \/ r < &0)`,
let MONOTONE_BIGGER = prove
(`!r. (!m n. m < n ==> r(m) < r(n)) ==> !n:num. n <= r(n)`,
GEN_TAC THEN DISCH_TAC THEN INDUCT_TAC THEN
ASM_MESON_TAC[
LE_0; ARITH_RULE `n <= m /\ m < p ==> SUC n <= p`;
LT]);;
let MONOTONE_SUBSEQUENCE = prove
(`!s:num->real. ?r:num->num.
(!m n. m < n ==> r(m) < r(n)) /\
((!m n. m <= n ==> s(r(m)) <= s(r(n))) \/
(!m n. m <= n ==> s(r(n)) <= s(r(m))))`,
GEN_TAC THEN
ASM_CASES_TAC `!n:num. ?p. n < p /\ !m. p <= m ==> s(m) <= s(p)` THEN
POP_ASSUM MP_TAC THEN
REWRITE_TAC[
NOT_FORALL_THM;
NOT_EXISTS_THM; NOT_IMP; DE_MORGAN_THM] THEN
REWRITE_TAC[
RIGHT_OR_EXISTS_THM;
SKOLEM_THM;
REAL_NOT_LE;
REAL_NOT_LT] THENL
[ABBREV_TAC `N = 0`; DISCH_THEN(X_CHOOSE_THEN `N:num` MP_TAC)] THEN
DISCH_THEN(X_CHOOSE_THEN `next:num->num` STRIP_ASSUME_TAC) THEN
(MP_TAC o prove_recursive_functions_exist num_RECURSION)
`(r 0 =
next(SUC N)) /\ (!n. r(SUC n) =
next(r n))` THEN
MATCH_MP_TAC
MONO_EXISTS THEN GEN_TAC THEN STRIP_TAC THENL
[SUBGOAL_THEN `!m:num n:num. r n <= m ==> s(m) <= s(r n):real`
ASSUME_TAC THEN TRY CONJ_TAC THEN TRY DISJ2_TAC THEN
GEN_TAC THEN INDUCT_TAC THEN ASM_REWRITE_TAC[
LT;
LE] THEN
ASM_MESON_TAC[
REAL_LE_TRANS;
REAL_LE_REFL;
LT_IMP_LE;
LT_TRANS];
SUBGOAL_THEN `!n. N < (r:num->num) n` ASSUME_TAC THEN
TRY(CONJ_TAC THENL [GEN_TAC; DISJ1_TAC THEN GEN_TAC]) THEN
INDUCT_TAC THEN ASM_REWRITE_TAC[
LT;
LE] THEN
TRY STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
ASM_MESON_TAC[
REAL_LT_REFL;
LT_LE;
LTE_TRANS;
REAL_LE_REFL;
REAL_LT_LE;
REAL_LE_TRANS;
LT]]);;
let CONVERGENT_BOUNDED_INCREASING = prove
(`!s:num->
real b. (!m n. m <= n ==> s m <= s n) /\ (!n. abs(s n) <= b)
==> ?l. !e. &0 < e ==> ?N. !n. N <= n ==> abs(s n - l) < e`,
REPEAT STRIP_TAC THEN
MP_TAC(SPEC `\x. ?n. (s:num->
real) n = x`
REAL_COMPLETE) THEN
REWRITE_TAC[] THEN ANTS_TAC THENL
[ASM_MESON_TAC[REAL_ARITH `abs(x) <= b ==> x <= b`]; ALL_TAC] THEN
MATCH_MP_TAC
MONO_EXISTS THEN X_GEN_TAC `l:real` THEN STRIP_TAC THEN
X_GEN_TAC `e:real` THEN STRIP_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPEC `l - e`) THEN
ASM_MESON_TAC[REAL_ARITH `&0 < e ==> ~(l <= l - e)`;
REAL_ARITH `x <= y /\ y <= l /\ ~(x <= l - e) ==> abs(y - l) < e`]);;
let CONVERGENT_BOUNDED_MONOTONE = prove
(`!s:num->
real b. (!n. abs(s n) <= b) /\
((!m n. m <= n ==> s m <= s n) \/
(!m n. m <= n ==> s n <= s m))
==> ?l. !e. &0 < e ==> ?N. !n. N <= n ==> abs(s n - l) < e`,
let COMPACT_REAL_LEMMA = prove
(`!s b. (!n:num. abs(s n) <= b)
==> ?l r. (!m n:num. m < n ==> r(m) < r(n)) /\
!e. &0 < e ==> ?N. !n. N <= n ==> abs(s(r n) - l) < e`,
let COMPACT_LEMMA = prove
(`!s.
bounded s /\ (!n. (x:num->real^N) n
IN s)
==> !d. d <=
dimindex(:N)
==> ?l:real^N r. (!m n. m < n ==> r m < (r:num->num) n) /\
!e. &0 < e
==> ?N. !n i. 1 <= i /\ i <= d
==> N <= n
==> abs(x(r n)$i - l$i) < e`,
GEN_TAC THEN REWRITE_TAC[
bounded] THEN
DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_TAC `b:real`) ASSUME_TAC) THEN
INDUCT_TAC THENL
[REWRITE_TAC[ARITH_RULE `1 <= i /\ i <= 0 <=> F`;
CONJ_ASSOC] THEN
DISCH_TAC THEN EXISTS_TAC `\n:num. n` THEN REWRITE_TAC[];
ALL_TAC] THEN
DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o check (is_imp o concl)) THEN
ASM_SIMP_TAC[ARITH_RULE `SUC d <= n ==> d <= n`] THEN STRIP_TAC THEN
MP_TAC(SPECL [`\n:num. (x:num->real^N) (r n) $ (SUC d)`; `b:real`]
COMPACT_REAL_LEMMA) THEN
REWRITE_TAC[] THEN ANTS_TAC THENL
[ASM_MESON_TAC[
REAL_LE_TRANS;
COMPONENT_LE_NORM; ARITH_RULE `1 <= SUC n`];
ALL_TAC] THEN
DISCH_THEN(X_CHOOSE_THEN `y:real` (X_CHOOSE_THEN `s:num->num`
STRIP_ASSUME_TAC)) THEN
MAP_EVERY EXISTS_TAC
[`(
lambda k. if k = SUC d then y else (l:real^N)$k):real^N`;
`(r:num->num) o (s:num->num)`] THEN
ASM_SIMP_TAC[
o_THM] THEN X_GEN_TAC `e:real` THEN DISCH_TAC THEN
REPEAT(FIRST_ASSUM(C UNDISCH_THEN (MP_TAC o SPEC `e:real`) o concl)) THEN
ASM_REWRITE_TAC[] THEN DISCH_THEN(X_CHOOSE_TAC `N1:num`) THEN
DISCH_THEN(X_CHOOSE_TAC `N2:num`) THEN EXISTS_TAC `N1 + N2:num` THEN
FIRST_ASSUM(fun
th -> SIMP_TAC[
LAMBDA_BETA; MATCH_MP(ARITH_RULE
`SUC d <= n ==> !i. 1 <= i /\ i <= SUC d ==> 1 <= i /\ i <= n`)
th]) THEN
REWRITE_TAC[
LE] THEN REPEAT STRIP_TAC THEN
ASM_REWRITE_TAC[] THEN TRY COND_CASES_TAC THEN
ASM_MESON_TAC[
MONOTONE_BIGGER;
LE_TRANS;
ARITH_RULE `N1 + N2 <= n ==> N2 <= n:num /\ N1 <= n`;
ARITH_RULE `1 <= i /\ i <= d /\ SUC d <= n
==> ~(i = SUC d) /\ 1 <= SUC d /\ d <= n /\ i <= n`]);;
let cauchy = new_definition
`cauchy (s:num->real^N) <=>
!e. &0 < e ==> ?N. !m n. m >= N /\ n >= N ==> dist(s m,s n) < e`;;let CAUCHY = prove
(`!s:num->real^N.
cauchy s <=> !e. &0 < e ==> ?N. !n. n >= N ==>
dist(s n,s N) < e`,
REPEAT GEN_TAC THEN REWRITE_TAC[
cauchy;
GE] THEN EQ_TAC THENL
[MESON_TAC[
LE_REFL]; DISCH_TAC] THEN
X_GEN_TAC `e:real` THEN DISCH_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPEC `e / &2`) THEN ASM_REWRITE_TAC[
REAL_HALF] THEN
MESON_TAC[
DIST_TRIANGLE_HALF_L]);;
let HEINE_BOREL_LEMMA = prove
(`!s:real^N->bool.
compact s
==> !t. s
SUBSET (
UNIONS t) /\ (!b. b
IN t ==> open b)
==> ?e. &0 < e /\
!x. x
IN s ==> ?b. b
IN t /\
ball(x,e)
SUBSET b`,
GEN_TAC THEN ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
REWRITE_TAC[
NOT_FORALL_THM; NOT_IMP;
NOT_EXISTS_THM] THEN
DISCH_THEN(CHOOSE_THEN (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
DISCH_THEN(MP_TAC o GEN `n:num` o SPEC `&1 / (&n + &1)`) THEN
SIMP_TAC[
REAL_LT_DIV;
REAL_LT_01; REAL_ARITH `x <= y ==> x < y + &1`;
FORALL_AND_THM;
REAL_POS;
NOT_FORALL_THM; NOT_IMP;
SKOLEM_THM;
compact] THEN
MATCH_MP_TAC
MONO_EXISTS THEN GEN_TAC THEN REWRITE_TAC[
NOT_EXISTS_THM] THEN
DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN ASM_REWRITE_TAC[] THEN
DISCH_TAC THEN MAP_EVERY X_GEN_TAC [`l:real^N`; `r:num->num`] THEN
STRIP_TAC THEN
SUBGOAL_THEN `?b:real^N->bool. l
IN b /\ b
IN t` STRIP_ASSUME_TAC THENL
[ASM_MESON_TAC[
SUBSET;
IN_UNIONS]; ALL_TAC] THEN
SUBGOAL_THEN `?e. &0 < e /\ !z:real^N.
dist(z,l) < e ==> z
IN b`
STRIP_ASSUME_TAC THENL [ASM_MESON_TAC[
open_def]; ALL_TAC] THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [
LIM_SEQUENTIALLY]) THEN
DISCH_THEN(MP_TAC o SPEC `e / &2`) THEN
SUBGOAL_THEN `&0 < e / &2` (fun
th ->
REWRITE_TAC[
th;
o_THM] THEN MP_TAC(GEN_REWRITE_RULE I [
REAL_ARCH_INV]
th))
THENL [ASM_REWRITE_TAC[
REAL_HALF]; ALL_TAC] THEN
DISCH_THEN(X_CHOOSE_THEN `N1:num` STRIP_ASSUME_TAC) THEN
DISCH_THEN(X_CHOOSE_THEN `N2:num` STRIP_ASSUME_TAC) THEN
FIRST_X_ASSUM(MP_TAC o SPECL
[`(r:num->num)(N1 + N2)`; `b:real^N->bool`]) THEN
ASM_REWRITE_TAC[
SUBSET] THEN X_GEN_TAC `x:real^N` THEN DISCH_TAC THEN
FIRST_X_ASSUM MATCH_MP_TAC THEN MATCH_MP_TAC
DIST_TRIANGLE_HALF_R THEN
EXISTS_TAC `(f:num->real^N)(r(N1 + N2:num))` THEN CONJ_TAC THENL
[ALL_TAC; FIRST_X_ASSUM MATCH_MP_TAC THEN ARITH_TAC] THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [
IN_BALL]) THEN
MATCH_MP_TAC(REAL_ARITH `a <= b ==> x < a ==> x < b`) THEN
MATCH_MP_TAC
REAL_LE_TRANS THEN EXISTS_TAC `inv(&N1)` THEN
ASM_SIMP_TAC[
REAL_LT_IMP_LE] THEN REWRITE_TAC[
real_div; REAL_MUL_LID] THEN
MATCH_MP_TAC
REAL_LE_INV2 THEN
REWRITE_TAC[REAL_OF_NUM_ADD; REAL_OF_NUM_LE;
REAL_OF_NUM_LT] THEN
ASM_MESON_TAC[ARITH_RULE `(~(n = 0) ==> 0 < n)`;
LE_ADD;
MONOTONE_BIGGER;
LT_IMP_LE;
LE_TRANS]);;
let BOUNDED_CLOSED_CHAIN = prove
(`!f b:real^N->bool.
(!s. s
IN f ==>
closed s /\ ~(s = {})) /\
(!s t. s
IN f /\ t
IN f ==> s
SUBSET t \/ t
SUBSET s) /\
b
IN f /\
bounded b
==> ~(
INTERS f = {})`,
REPEAT GEN_TAC THEN STRIP_TAC THEN
SUBGOAL_THEN `~(b
INTER (
INTERS f):real^N->bool = {})` MP_TAC THENL
[ALL_TAC; SET_TAC[]] THEN
MATCH_MP_TAC
COMPACT_IMP_FIP THEN
ASM_SIMP_TAC[
COMPACT_EQ_BOUNDED_CLOSED] THEN
X_GEN_TAC `u:(real^N->bool)->bool` THEN STRIP_TAC THEN
SUBGOAL_THEN `?s:real^N->bool. s
IN f /\ !t. t
IN u ==> s
SUBSET t`
MP_TAC THENL [ALL_TAC; ASM SET_TAC[]] THEN
UNDISCH_TAC `(u:(real^N->bool)->bool)
SUBSET f` THEN
UNDISCH_TAC `FINITE(u:(real^N->bool)->bool)` THEN
SPEC_TAC(`u:(real^N->bool)->bool`,`u:(real^N->bool)->bool`) THEN
MATCH_MP_TAC
FINITE_INDUCT_STRONG THEN
CONJ_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
MAP_EVERY X_GEN_TAC [`t:real^N->bool`; `u:(real^N->bool)->bool`] THEN
REWRITE_TAC[
INSERT_SUBSET] THEN
DISCH_THEN(fun
th -> STRIP_TAC THEN MP_TAC
th) THEN
ASM_REWRITE_TAC[] THEN
DISCH_THEN(CONJUNCTS_THEN2 MP_TAC STRIP_ASSUME_TAC) THEN
DISCH_THEN(X_CHOOSE_THEN `s:real^N->bool` STRIP_ASSUME_TAC) THEN
FIRST_X_ASSUM(MP_TAC o SPECL [`s:real^N->bool`; `t:real^N->bool`]) THEN
ASM SET_TAC[]);;
let UNIFORMLY_CONVERGENT_EQ_CAUCHY = prove
(`!P s:num->A->real^N.
(?l. !e. &0 < e
==> ?N. !n x. N <= n /\ P x ==>
dist(s n x,l x) < e) <=>
(!e. &0 < e
==> ?N. !m n x. N <= m /\ N <= n /\ P x
==>
dist(s m x,s n x) < e)`,
REPEAT GEN_TAC THEN EQ_TAC THENL
[DISCH_THEN(X_CHOOSE_TAC `l:A->real^N`) THEN X_GEN_TAC `e:real` THEN
DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC `e / &2`) THEN
ASM_REWRITE_TAC[
REAL_HALF] THEN MESON_TAC[
DIST_TRIANGLE_HALF_L];
ALL_TAC] THEN
DISCH_TAC THEN
SUBGOAL_THEN `!x:A. P x ==>
cauchy (\n. s n x :real^N)` MP_TAC THENL
[REWRITE_TAC[
cauchy;
GE] THEN ASM_MESON_TAC[]; ALL_TAC] THEN
REWRITE_TAC[GSYM
CONVERGENT_EQ_CAUCHY;
LIM_SEQUENTIALLY] THEN
GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [
RIGHT_IMP_EXISTS_THM] THEN
REWRITE_TAC[
SKOLEM_THM] THEN MATCH_MP_TAC
MONO_EXISTS THEN
X_GEN_TAC `l:A->real^N` THEN DISCH_TAC THEN X_GEN_TAC `e:real` THEN
DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC `e / &2`) THEN
ASM_REWRITE_TAC[
REAL_HALF] THEN MATCH_MP_TAC
MONO_EXISTS THEN
X_GEN_TAC `N:num` THEN STRIP_TAC THEN
MAP_EVERY X_GEN_TAC [`n:num`; `x:A`] THEN STRIP_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPEC `x:A`) THEN ASM_REWRITE_TAC[] THEN
DISCH_THEN(MP_TAC o SPEC `e / &2`) THEN ASM_REWRITE_TAC[
REAL_HALF] THEN
DISCH_THEN(X_CHOOSE_TAC `M:num`) THEN
FIRST_X_ASSUM(MP_TAC o SPECL [`n:num`; `N + M:num`; `x:A`]) THEN
ASM_REWRITE_TAC[
LE_ADD] THEN ONCE_REWRITE_TAC[
ADD_SYM] THEN
FIRST_X_ASSUM(MP_TAC o SPEC `M + N:num`) THEN REWRITE_TAC[
LE_ADD] THEN
ASM_MESON_TAC[
DIST_TRIANGLE_HALF_L;
DIST_SYM]);;
let CONTINUOUS_OPEN_PREIMAGE = prove
(`!f:real^M->real^N s t.
f
continuous_on s /\ open s /\ open t
==> open {x | x
IN s /\ f(x)
IN t}`,
REPEAT STRIP_TAC THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [
CONTINUOUS_ON_OPEN]) THEN
REWRITE_TAC [
OPEN_IN_OPEN] THEN
DISCH_THEN(MP_TAC o SPEC `
IMAGE (f:real^M->real^N) s
INTER t`) THEN
ANTS_TAC THENL
[EXISTS_TAC `t:real^N->bool` THEN ASM_REWRITE_TAC [];
STRIP_TAC THEN
SUBGOAL_THEN `{x | x
IN s /\ (f:real^M->real^N) x
IN t} =
s
INTER t'` SUBST1_TAC THENL
[ASM SET_TAC []; ASM_MESON_TAC [
OPEN_INTER]]]);;
let CONTINUOUS_ON_CLOSURE = prove
(`!f:real^M->real^N s.
f
continuous_on closure s <=>
!x e. x
IN closure s /\ &0 < e
==> ?d. &0 < d /\
!y. y
IN s /\
dist(y,x) < d ==>
dist(f y,f x) < e`,
REPEAT GEN_TAC THEN REWRITE_TAC[
continuous_on] THEN
EQ_TAC THENL [MESON_TAC[REWRITE_RULE[
SUBSET]
CLOSURE_SUBSET]; ALL_TAC] THEN
DISCH_TAC THEN X_GEN_TAC `x:real^M` THEN DISCH_TAC THEN
X_GEN_TAC `e:real` THEN DISCH_TAC THEN
FIRST_ASSUM(MP_TAC o SPECL [`x:real^M`; `e / &2`]) THEN
ANTS_TAC THENL [ASM_REWRITE_TAC[
REAL_HALF]; ALL_TAC] THEN
DISCH_THEN(X_CHOOSE_THEN `d:real` STRIP_ASSUME_TAC) THEN
EXISTS_TAC `d / &2` THEN ASM_REWRITE_TAC[
REAL_HALF] THEN
X_GEN_TAC `y:real^M` THEN STRIP_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPECL [`y:real^M`; `e / &2`]) THEN
ASM_REWRITE_TAC[
REAL_HALF] THEN
DISCH_THEN(X_CHOOSE_THEN `k:real` STRIP_ASSUME_TAC) THEN
MP_TAC(ISPECL [`y:real^M`; `s:real^M->bool`]
CLOSURE_APPROACHABLE) THEN
ASM_REWRITE_TAC[] THEN DISCH_THEN(MP_TAC o SPEC `min k (d / &2)`) THEN
ASM_REWRITE_TAC[
REAL_HALF;
REAL_LT_MIN] THEN
ASM_MESON_TAC[
DIST_SYM; NORM_ARITH
`
dist(a,b) < e / &2 /\
dist(b,c) < e / &2 ==>
dist(a,c) < e`]);;
let UNIFORMLY_CONTINUOUS_ON_CLOSURE = prove
(`!f:real^M->real^N s.
f
uniformly_continuous_on s /\ f
continuous_on closure s
==> f
uniformly_continuous_on closure s`,
REPEAT GEN_TAC THEN
REWRITE_TAC[
uniformly_continuous_on] THEN STRIP_TAC THEN
X_GEN_TAC `e:real` THEN DISCH_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPEC `e / &3`) THEN
ANTS_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
DISCH_THEN(X_CHOOSE_THEN `d:real` STRIP_ASSUME_TAC) THEN
EXISTS_TAC `d / &3` THEN CONJ_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
MAP_EVERY X_GEN_TAC [`x:real^M`; `y:real^M`] THEN STRIP_TAC THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [
continuous_on]) THEN
DISCH_THEN(fun
th ->
MP_TAC(SPEC `y:real^M`
th) THEN MP_TAC(SPEC `x:real^M`
th)) THEN
ASM_REWRITE_TAC[] THEN
DISCH_THEN(MP_TAC o SPEC `e / &3`) THEN
ANTS_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
DISCH_THEN(X_CHOOSE_THEN `d1:real` (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
MP_TAC(ISPECL [`x:real^M`; `s:real^M->bool`]
CLOSURE_APPROACHABLE) THEN
ASM_REWRITE_TAC[] THEN DISCH_THEN(MP_TAC o SPEC `min d1 (d / &3)`) THEN
ANTS_TAC THENL [ASM_REAL_ARITH_TAC; REWRITE_TAC[
REAL_LT_MIN]] THEN
DISCH_THEN(X_CHOOSE_THEN `x':real^M` STRIP_ASSUME_TAC) THEN
DISCH_THEN(MP_TAC o SPEC `x':real^M`) THEN
ASM_SIMP_TAC[REWRITE_RULE[
SUBSET]
CLOSURE_SUBSET] THEN DISCH_TAC THEN
DISCH_THEN(MP_TAC o SPEC `e / &3`) THEN
ANTS_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
DISCH_THEN(X_CHOOSE_THEN `d2:real` (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
MP_TAC(ISPECL [`y:real^M`; `s:real^M->bool`]
CLOSURE_APPROACHABLE) THEN
ASM_REWRITE_TAC[] THEN DISCH_THEN(MP_TAC o SPEC `min d2 (d / &3)`) THEN
ANTS_TAC THENL [ASM_REAL_ARITH_TAC; REWRITE_TAC[
REAL_LT_MIN]] THEN
DISCH_THEN(X_CHOOSE_THEN `y':real^M` STRIP_ASSUME_TAC) THEN
DISCH_THEN(MP_TAC o SPEC `y':real^M`) THEN
ASM_SIMP_TAC[REWRITE_RULE[
SUBSET]
CLOSURE_SUBSET] THEN DISCH_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPECL [`x':real^M`; `y':real^M`]) THEN
ASM_MESON_TAC[
DIST_SYM; NORM_ARITH
`
dist(y,x) < d / &3 /\
dist(x',x) < d / &3 /\
dist(y',y) < d / &3
==>
dist(y',x') < d`]);;
let CAUCHY_CONTINUOUS_UNIQUENESS_LEMMA = prove
(`!f:real^M->real^N s.
(!x.
cauchy x /\ (!n. (x n)
IN s) ==>
cauchy(f o x))
==> !a x. (!n. (x n)
IN s) /\ (x --> a)
sequentially
==> ?l. ((f o x) --> l)
sequentially /\
!y. (!n. (y n)
IN s) /\ (y --> a)
sequentially
==> ((f o y) --> l)
sequentially`,
REPEAT STRIP_TAC THEN
FIRST_ASSUM(MP_TAC o SPEC `x:num->real^M`) THEN
ANTS_TAC THENL [ASM_MESON_TAC[
CONVERGENT_IMP_CAUCHY]; ALL_TAC] THEN
REWRITE_TAC[GSYM
CONVERGENT_EQ_CAUCHY] THEN MATCH_MP_TAC
MONO_EXISTS THEN
X_GEN_TAC `l:real^N` THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
X_GEN_TAC `y:num->real^M` THEN STRIP_TAC THEN
FIRST_ASSUM(MP_TAC o SPEC `y:num->real^M`) THEN
ANTS_TAC THENL [ASM_MESON_TAC[
CONVERGENT_IMP_CAUCHY]; ALL_TAC] THEN
REWRITE_TAC[GSYM
CONVERGENT_EQ_CAUCHY] THEN
DISCH_THEN(X_CHOOSE_THEN `m:real^N` STRIP_ASSUME_TAC) THEN
SUBGOAL_THEN `l:real^N = m` (fun
th -> ASM_REWRITE_TAC[
th]) THEN
ONCE_REWRITE_TAC[GSYM
VECTOR_SUB_EQ] THEN
MATCH_MP_TAC(ISPEC `
sequentially`
LIM_UNIQUE) THEN
EXISTS_TAC `\n:num. (f:real^M->real^N)(x n) - f(y n)` THEN
RULE_ASSUM_TAC(REWRITE_RULE[
o_DEF]) THEN
ASM_SIMP_TAC[
LIM_SUB;
TRIVIAL_LIMIT_SEQUENTIALLY] THEN
FIRST_X_ASSUM(MP_TAC o SPEC
`\n. if
EVEN n then x(n DIV 2):real^M else y(n DIV 2)`) THEN
REWRITE_TAC[
cauchy;
o_THM;
LIM_SEQUENTIALLY] THEN ANTS_TAC THENL
[CONJ_TAC THENL [ALL_TAC; ASM_MESON_TAC[]] THEN
X_GEN_TAC `e:real` THEN DISCH_TAC THEN MAP_EVERY UNDISCH_TAC
[`((y:num->real^M) --> a)
sequentially`;
`((x:num->real^M) --> a)
sequentially`] THEN
REPEAT(FIRST_X_ASSUM(K ALL_TAC o check (is_forall o concl))) THEN
REWRITE_TAC[
LIM_SEQUENTIALLY] THEN
DISCH_THEN(MP_TAC o SPEC `e / &2`) THEN ASM_REWRITE_TAC[
REAL_HALF] THEN
DISCH_THEN(X_CHOOSE_TAC `N1:num`) THEN
DISCH_THEN(MP_TAC o SPEC `e / &2`) THEN ASM_REWRITE_TAC[
REAL_HALF] THEN
DISCH_THEN(X_CHOOSE_TAC `N2:num`) THEN
EXISTS_TAC `2 * (N1 + N2)` THEN
MAP_EVERY X_GEN_TAC [`m:num`; `n:num`] THEN STRIP_TAC THEN
REPEAT(FIRST_X_ASSUM(fun
th ->
MP_TAC(SPEC `m DIV 2`
th) THEN MP_TAC(SPEC `n DIV 2`
th))) THEN
REPEAT(ANTS_TAC THENL [ASM_ARITH_TAC; DISCH_TAC]) THEN
REPEAT(COND_CASES_TAC THEN ASM_REWRITE_TAC[]) THEN
REPEAT(FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM
REAL_NOT_LE])) THEN
CONV_TAC NORM_ARITH;
MATCH_MP_TAC
MONO_FORALL THEN X_GEN_TAC `e:real` THEN
ASM_CASES_TAC `&0 < e` THEN ASM_REWRITE_TAC[] THEN
MATCH_MP_TAC
MONO_EXISTS THEN X_GEN_TAC `N:num` THEN DISCH_TAC THEN
X_GEN_TAC `n:num` THEN DISCH_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPECL [`2 * n`; `2 * n + 1`]) THEN
ANTS_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN
REWRITE_TAC[
EVEN_ADD;
EVEN_MULT;
ARITH_EVEN] THEN
REWRITE_TAC[ARITH_RULE `(2 * n) DIV 2 = n /\ (2 * n + 1) DIV 2 = n`] THEN
REWRITE_TAC[
dist;
VECTOR_SUB_RZERO]]);;
let OPEN_SUMS = prove
(`!s t:real^N->bool.
open s \/ open t ==> open {x + y | x
IN s /\ y
IN t}`,
REPEAT GEN_TAC THEN REWRITE_TAC[
open_def] THEN STRIP_TAC THEN
REWRITE_TAC[
FORALL_IN_GSPEC] THEN
MAP_EVERY X_GEN_TAC [`x:real^N`; `y:real^N`] THEN STRIP_TAC THENL
[FIRST_X_ASSUM(MP_TAC o SPEC `x:real^N`);
FIRST_X_ASSUM(MP_TAC o SPEC `y:real^N`)] THEN
ASM_REWRITE_TAC[] THEN MATCH_MP_TAC
MONO_EXISTS THEN
X_GEN_TAC `e:real` THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
X_GEN_TAC `z:real^N` THEN DISCH_TAC THEN REWRITE_TAC[
IN_ELIM_THM] THEN
ASM_MESON_TAC[
VECTOR_ADD_SYM; VECTOR_ARITH `(z - y) + y:real^N = z`;
NORM_ARITH `
dist(z:real^N,x + y) < e ==>
dist(z - y,x) < e`]);;
let COMPACT_CONTINUOUS_IMAGE = prove
(`!f:real^M->real^N s.
f
continuous_on s /\
compact s ==>
compact(
IMAGE f s)`,
REPEAT GEN_TAC THEN REWRITE_TAC[
continuous_on;
compact] THEN
STRIP_TAC THEN X_GEN_TAC `y:num->real^N` THEN
REWRITE_TAC[
IN_IMAGE;
SKOLEM_THM;
FORALL_AND_THM] THEN
DISCH_THEN(X_CHOOSE_THEN `x:num->real^M` STRIP_ASSUME_TAC) THEN
FIRST_X_ASSUM(MP_TAC o SPEC `x:num->real^M`) THEN ASM_REWRITE_TAC[] THEN
ONCE_REWRITE_TAC[
SWAP_EXISTS_THM] THEN MATCH_MP_TAC
MONO_EXISTS THEN
X_GEN_TAC `r:num->num` THEN
DISCH_THEN(X_CHOOSE_THEN `l:real^M` STRIP_ASSUME_TAC) THEN
EXISTS_TAC `(f:real^M->real^N) l` THEN ASM_REWRITE_TAC[] THEN
CONJ_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
REWRITE_TAC[
LIM_SEQUENTIALLY] THEN
FIRST_X_ASSUM(MP_TAC o SPEC `l:real^M`) THEN
ASM_REWRITE_TAC[] 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
DISCH_THEN(X_CHOOSE_THEN `d:real` STRIP_ASSUME_TAC) THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [
LIM_SEQUENTIALLY]) THEN
DISCH_THEN(MP_TAC o SPEC `d:real`) THEN ASM_REWRITE_TAC[
o_THM] THEN
ASM_MESON_TAC[]);;
let COMPONENTS_UNIQUE = prove
(`!s:real^N->bool k.
UNIONS k = s /\
(!c. c
IN k
==>
connected c /\ ~(c = {}) /\
!c'.
connected c' /\ c
SUBSET c' /\ c'
SUBSET s ==> c' = c)
==>
components s = k`,
REPEAT STRIP_TAC THEN GEN_REWRITE_TAC I [
EXTENSION] THEN
X_GEN_TAC `c:real^N->bool` THEN REWRITE_TAC[
IN_COMPONENTS] THEN
EQ_TAC THENL
[DISCH_THEN(X_CHOOSE_THEN `x:real^N`
(CONJUNCTS_THEN2 ASSUME_TAC SUBST1_TAC)) THEN
FIRST_ASSUM(MP_TAC o SPEC `x:real^N` o GEN_REWRITE_RULE I [
EXTENSION]) THEN
REWRITE_TAC[
IN_UNIONS] THEN ASM_REWRITE_TAC[
LEFT_IMP_EXISTS_THM] THEN
X_GEN_TAC `c:real^N->bool` THEN STRIP_TAC THEN
SUBGOAL_THEN `
connected_component s (x:real^N) = c`
(fun
th -> ASM_REWRITE_TAC[
th]) THEN
MATCH_MP_TAC
CONNECTED_COMPONENT_UNIQUE THEN
FIRST_X_ASSUM(MP_TAC o SPEC `c:real^N->bool`) THEN
ASM_REWRITE_TAC[] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
CONJ_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
X_GEN_TAC `c':real^N->bool` THEN STRIP_TAC THEN
REWRITE_TAC[SET_RULE `c'
SUBSET c <=> c'
UNION c = c`] THEN
FIRST_X_ASSUM MATCH_MP_TAC THEN CONJ_TAC THENL
[MATCH_MP_TAC
CONNECTED_UNION; ASM SET_TAC[]] THEN
ASM SET_TAC[];
DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC `c:real^N->bool`) THEN
ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM
MEMBER_NOT_EMPTY]) THEN
MATCH_MP_TAC
MONO_EXISTS THEN X_GEN_TAC `x:real^N` THEN STRIP_TAC THEN
CONJ_TAC THENL [ASM SET_TAC[]; CONV_TAC SYM_CONV] THEN
FIRST_X_ASSUM MATCH_MP_TAC THEN
REWRITE_TAC[
CONNECTED_CONNECTED_COMPONENT;
CONNECTED_COMPONENT_SUBSET] THEN
MATCH_MP_TAC
CONNECTED_COMPONENT_MAXIMAL THEN
ASM_REWRITE_TAC[] THEN ASM SET_TAC[]]);;
let COMPACT_UNIFORMLY_EQUICONTINUOUS = prove
(`!(fs:(real^M->real^N)->bool) s.
(!x e. x
IN s /\ &0 < e
==> ?d. &0 < d /\
(!f x'. f
IN fs /\ x'
IN s /\
dist (x',x) < d
==>
dist (f x',f x) < e)) /\
compact s
==> !e. &0 < e
==> ?d. &0 < d /\
!f x x'. f
IN fs /\ x
IN s /\ x'
IN s /\
dist (x',x) < d
==>
dist(f x',f x) < e`,
REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
GEN_REWRITE_TAC (LAND_CONV o TOP_DEPTH_CONV) [
RIGHT_IMP_EXISTS_THM] THEN
REWRITE_TAC[
SKOLEM_THM;
LEFT_IMP_EXISTS_THM] THEN
X_GEN_TAC `d:real^M->real->
real` THEN DISCH_TAC THEN X_GEN_TAC `e:real` THEN
DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o MATCH_MP
HEINE_BOREL_LEMMA) THEN
DISCH_THEN(MP_TAC o SPEC
`{
ball(x:real^M,d x (e / &2)) | x
IN s}`) THEN
SIMP_TAC[
FORALL_IN_GSPEC;
OPEN_BALL;
UNIONS_GSPEC;
SUBSET;
IN_ELIM_THM] THEN
ANTS_TAC THENL [ASM_MESON_TAC[
CENTRE_IN_BALL;
REAL_HALF]; ALL_TAC] THEN
MATCH_MP_TAC
MONO_EXISTS THEN X_GEN_TAC `k:real` THEN STRIP_TAC THEN
ASM_REWRITE_TAC[] THEN
MAP_EVERY X_GEN_TAC [`f:real^M->real^N`; `u:real^M`; `v:real^M`] THEN
STRIP_TAC THEN FIRST_X_ASSUM(fun
th -> MP_TAC(SPEC `v:real^M`
th) THEN
ASM_REWRITE_TAC[] THEN DISCH_THEN(CHOOSE_THEN MP_TAC)) THEN
DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
DISCH_THEN(fun
th ->
MP_TAC(SPEC `u:real^M`
th) THEN MP_TAC(SPEC `v:real^M`
th)) THEN
ASM_REWRITE_TAC[
DIST_REFL] THEN
FIRST_X_ASSUM(X_CHOOSE_THEN `w:real^M` (CONJUNCTS_THEN2 ASSUME_TAC
SUBST_ALL_TAC)) THEN
ASM_REWRITE_TAC[
CENTRE_IN_BALL] THEN ASM_REWRITE_TAC[
IN_BALL] THEN
ONCE_REWRITE_TAC[
DIST_SYM] THEN REPEAT STRIP_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPECL [`w:real^M`; `e / &2`]) THEN
ASM_REWRITE_TAC[
REAL_HALF] THEN
DISCH_THEN(MP_TAC o SPEC `f:real^M->real^N` o CONJUNCT2) THEN
DISCH_THEN(fun
th -> MP_TAC(SPEC `u:real^M`
th) THEN
MP_TAC(SPEC `v:real^M`
th)) THEN
ASM_REWRITE_TAC[] THEN CONV_TAC NORM_ARITH);;
let CONTINUOUS_UNIFORM_LIMIT = prove
(`!net f:A->real^M->real^N g s.
~(
trivial_limit net) /\
eventually (\n. (f n)
continuous_on s) net /\
(!e. &0 < e
==>
eventually (\n. !x. x
IN s ==>
norm(f n x - g x) < e) net)
==> g
continuous_on s`,
REWRITE_TAC[
continuous_on] THEN REPEAT GEN_TAC THEN STRIP_TAC THEN
X_GEN_TAC `x:real^M` THEN STRIP_TAC THEN
X_GEN_TAC `e:real` THEN DISCH_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPEC `e / &3`) THEN
ASM_SIMP_TAC[
REAL_LT_DIV;
REAL_OF_NUM_LT; ARITH] THEN
FIRST_X_ASSUM(fun
th -> MP_TAC
th THEN REWRITE_TAC[IMP_IMP] THEN
GEN_REWRITE_TAC LAND_CONV [GSYM
EVENTUALLY_AND]) THEN
DISCH_THEN(MP_TAC o MATCH_MP
EVENTUALLY_HAPPENS) THEN
ASM_REWRITE_TAC[
LEFT_IMP_EXISTS_THM] THEN X_GEN_TAC `a:A` THEN
DISCH_THEN(CONJUNCTS_THEN2 (MP_TAC o SPEC `x:real^M`) ASSUME_TAC) THEN
ASM_REWRITE_TAC[] THEN DISCH_THEN(MP_TAC o SPEC `e / &3`) THEN
ASM_SIMP_TAC[
REAL_LT_DIV;
REAL_OF_NUM_LT; ARITH] THEN
MATCH_MP_TAC
MONO_EXISTS THEN X_GEN_TAC `d:real` THEN
MATCH_MP_TAC MONO_AND THEN REWRITE_TAC[] THEN
MATCH_MP_TAC
MONO_FORALL THEN X_GEN_TAC `y:real^M` THEN
DISCH_THEN(fun
th -> STRIP_TAC THEN MP_TAC
th) THEN ASM_REWRITE_TAC[] THEN
FIRST_X_ASSUM(fun
th ->
MP_TAC(SPEC `x:real^M`
th) THEN MP_TAC(SPEC `y:real^M`
th)) THEN
ASM_REWRITE_TAC[] THEN MATCH_MP_TAC(REAL_ARITH
`w <= x + y + z
==> x < e / &3 ==> y < e / &3 ==> z < e / &3 ==> w < e`) THEN
REWRITE_TAC[
dist] THEN
SUBST1_TAC(VECTOR_ARITH
`(g:real^M->real^N) y - g x =
--(f (a:A) y - g y) + (f a x - g x) + (f a y - f a x)`) THEN
MATCH_MP_TAC
NORM_TRIANGLE_LE THEN REWRITE_TAC[
NORM_NEG;
REAL_LE_LADD] THEN
MATCH_MP_TAC
NORM_TRIANGLE_LE THEN REWRITE_TAC[
NORM_NEG;
REAL_LE_REFL]);;
let LIM_MUL = prove
(`!net:(A)net f l:real^N c d.
((
lift o c) -->
lift d) net /\ (f --> l) net
==> ((\x. c(x) % f(x)) --> (d % l)) net`,
let LIM_PASTECART = prove
(`!net f:A->real^M g:A->real^N.
(f --> a) net /\ (g --> b) net
==> ((\x.
pastecart (f x) (g x)) -->
pastecart a b) net`,
REPEAT GEN_TAC THEN REWRITE_TAC[
LIM] THEN
ASM_CASES_TAC `
trivial_limit(net:(A)net)` THEN ASM_REWRITE_TAC[] THEN
REWRITE_TAC[
AND_FORALL_THM] THEN DISCH_TAC THEN X_GEN_TAC `e:real` THEN
DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC `e / &2`) THEN
ASM_REWRITE_TAC[
REAL_HALF] THEN
DISCH_THEN(MP_TAC o MATCH_MP
NET_DILEMMA) THEN
MATCH_MP_TAC
MONO_EXISTS THEN GEN_TAC THEN MATCH_MP_TAC MONO_AND THEN
REWRITE_TAC[] THEN MATCH_MP_TAC
MONO_FORALL THEN GEN_TAC THEN
MATCH_MP_TAC MONO_IMP THEN REWRITE_TAC[] THEN
REWRITE_TAC[
dist;
PASTECART_SUB] THEN
MATCH_MP_TAC(REAL_ARITH
`z <= x + y ==> x < e / &2 /\ y < e / &2 ==> z < e`) THEN
REWRITE_TAC[
NORM_PASTECART_LE]);;
let DIAMETER_POS_LE = prove
(`!s:real^N->bool.
bounded s ==> &0 <=
diameter s`,
REPEAT STRIP_TAC THEN REWRITE_TAC[
diameter] THEN
COND_CASES_TAC THEN ASM_REWRITE_TAC[
REAL_LE_REFL] THEN
MP_TAC(SPEC `{
norm(x - y:real^N) | x
IN s /\ y
IN s}`
SUP) THEN
REWRITE_TAC[
FORALL_IN_GSPEC] THEN ANTS_TAC THENL
[CONJ_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
FIRST_X_ASSUM(X_CHOOSE_TAC `B:real` o GEN_REWRITE_RULE I [
BOUNDED_POS]) THEN
EXISTS_TAC `&2 * B` THEN
ASM_SIMP_TAC[NORM_ARITH
`
norm x <= B /\
norm y <= B ==>
norm(x - y) <= &2 * B`];
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM
MEMBER_NOT_EMPTY]) THEN
DISCH_THEN(X_CHOOSE_TAC `a:real^N`) THEN
DISCH_THEN(MP_TAC o SPECL [`a:real^N`; `a:real^N`] o CONJUNCT1) THEN
ASM_REWRITE_TAC[
VECTOR_SUB_REFL;
NORM_0]]);;
let DIAMETER_EQ_0 = prove
(`!s:real^N->bool.
bounded s ==> (
diameter s = &0 <=> s = {} \/ ?a. s = {a})`,
REPEAT STRIP_TAC THEN EQ_TAC THEN STRIP_TAC THEN
ASM_REWRITE_TAC[
DIAMETER_EMPTY;
DIAMETER_SING] THEN
REWRITE_TAC[SET_RULE
`s = {} \/ (?a. s = {a}) <=> !a b. a
IN s /\ b
IN s ==> a = b`] THEN
MAP_EVERY X_GEN_TAC [`a:real^N`; `b:real^N`] THEN STRIP_TAC THEN
MP_TAC(ISPECL [`s:real^N->bool`; `a:real^N`; `b:real^N`]
DIAMETER_BOUNDED_BOUND) THEN
ASM_REWRITE_TAC[] THEN NORM_ARITH_TAC);;
let LEBESGUE_COVERING_LEMMA = prove
(`!s:real^N->bool c.
compact s /\ ~(c = {}) /\ s
SUBSET UNIONS c /\ (!b. b
IN c ==> open b)
==> ?d. &0 < d /\
!t. t
SUBSET s /\
diameter t <= d
==> ?b. b
IN c /\ t
SUBSET b`,
REPEAT STRIP_TAC THEN
FIRST_ASSUM(MP_TAC o MATCH_MP
HEINE_BOREL_LEMMA) THEN
DISCH_THEN(MP_TAC o SPEC `c:(real^N->bool)->bool`) THEN ASM_SIMP_TAC[] THEN
ASM_REWRITE_TAC[
LEFT_IMP_EXISTS_THM] THEN X_GEN_TAC `e:real` THEN
STRIP_TAC THEN EXISTS_TAC `e / &2` THEN ASM_REWRITE_TAC[
REAL_HALF] THEN
X_GEN_TAC `t:real^N->bool` THEN STRIP_TAC THEN
ASM_CASES_TAC `t:real^N->bool = {}` THENL [ASM SET_TAC[]; ALL_TAC] THEN
MP_TAC(ISPEC `t:real^N->bool`
DIAMETER_SUBSET_CBALL_NONEMPTY) THEN
ANTS_TAC THENL
[ASM_MESON_TAC[
BOUNDED_SUBSET;
COMPACT_IMP_BOUNDED]; ALL_TAC] THEN
DISCH_THEN(X_CHOOSE_THEN `x:real^N` STRIP_ASSUME_TAC) THEN
FIRST_X_ASSUM(MP_TAC o SPEC `x:real^N`) THEN
ANTS_TAC THENL [ASM SET_TAC[]; MATCH_MP_TAC
MONO_EXISTS] THEN
X_GEN_TAC `b:real^N->bool` THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
MATCH_MP_TAC
SUBSET_TRANS THEN
EXISTS_TAC `
cball(x:real^N,
diameter(t:real^N->bool))` THEN
ASM_REWRITE_TAC[] THEN MATCH_MP_TAC
SUBSET_TRANS THEN
EXISTS_TAC `
ball(x:real^N,e)` THEN ASM_REWRITE_TAC[] THEN
REWRITE_TAC[
SUBSET;
IN_CBALL;
IN_BALL] THEN
MAP_EVERY UNDISCH_TAC [`&0 < e`; `
diameter(t:real^N->bool) <= e / &2`] THEN
NORM_ARITH_TAC);;
let COMPACT_CLOSED_SUMS = prove
(`!s:real^N->bool t.
compact s /\
closed t ==>
closed {x + y | x
IN s /\ y
IN t}`,
REPEAT GEN_TAC THEN
REWRITE_TAC[
compact;
IN_ELIM_THM;
CLOSED_SEQUENTIAL_LIMITS] THEN
STRIP_TAC THEN X_GEN_TAC `f:num->real^N` THEN X_GEN_TAC `l:real^N` THEN
REWRITE_TAC[
SKOLEM_THM;
FORALL_AND_THM] THEN
DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
DISCH_THEN(X_CHOOSE_THEN `a:num->real^N` MP_TAC) THEN
DISCH_THEN(X_CHOOSE_THEN `b:num->real^N` STRIP_ASSUME_TAC) THEN
FIRST_X_ASSUM(MP_TAC o check(is_imp o concl) o SPEC `a:num->real^N`) THEN
ASM_REWRITE_TAC[] THEN
DISCH_THEN(X_CHOOSE_THEN `la:real^N` (X_CHOOSE_THEN `sub:num->num`
STRIP_ASSUME_TAC)) THEN
MAP_EVERY EXISTS_TAC [`la:real^N`; `l - la:real^N`] THEN
ASM_REWRITE_TAC[VECTOR_ARITH `a + (b - a) = b:real^N`] THEN
FIRST_X_ASSUM MATCH_MP_TAC THEN
EXISTS_TAC `\n. (f o (sub:num->num)) n - (a o sub) n:real^N` THEN
CONJ_TAC THENL [ASM_REWRITE_TAC[
VECTOR_ADD_SUB;
o_THM]; ALL_TAC] THEN
MATCH_MP_TAC
LIM_SUB THEN ASM_SIMP_TAC[
LIM_SUBSEQUENCE; ETA_AX]);;
let SUBSET_INTERVAL = prove
(`(
interval[c,d]
SUBSET interval[a:real^N,b] <=>
(!i. 1 <= i /\ i <=
dimindex(:N) ==> c$i <= d$i)
==> (!i. 1 <= i /\ i <=
dimindex(:N) ==> a$i <= c$i /\ d$i <= b$i)) /\
(
interval[c,d]
SUBSET interval(a:real^N,b) <=>
(!i. 1 <= i /\ i <=
dimindex(:N) ==> c$i <= d$i)
==> (!i. 1 <= i /\ i <=
dimindex(:N) ==> a$i < c$i /\ d$i < b$i)) /\
(
interval(c,d)
SUBSET interval[a:real^N,b] <=>
(!i. 1 <= i /\ i <=
dimindex(:N) ==> c$i < d$i)
==> (!i. 1 <= i /\ i <=
dimindex(:N) ==> a$i <= c$i /\ d$i <= b$i)) /\
(
interval(c,d)
SUBSET interval(a:real^N,b) <=>
(!i. 1 <= i /\ i <=
dimindex(:N) ==> c$i < d$i)
==> (!i. 1 <= i /\ i <=
dimindex(:N) ==> a$i <= c$i /\ d$i <= b$i))`,
let lemma = prove
(`(!x:real^N. (!i. 1 <= i /\ i <= dimindex(:N) ==> Q i (x$i))
==> (!i. 1 <= i /\ i <= dimindex(:N) ==> R i (x$i)))
==> (!i. 1 <= i /\ i <= dimindex(:N) ==> ?y. Q i y)
==> !i y. 1 <= i /\ i <= dimindex(:N) /\ Q i y ==> R i y`,
DISCH_TAC THEN REWRITE_TAC[RIGHT_IMP_EXISTS_THM; SKOLEM_THM] THEN
DISCH_THEN(X_CHOOSE_THEN `f:num->real` STRIP_ASSUME_TAC) THEN
REPEAT STRIP_TAC THEN FIRST_X_ASSUM(MP_TAC o
SPEC `(lambda j. if j = i then y else f j):real^N`) THEN
SIMP_TAC[LAMBDA_BETA] THEN ASM_MESON_TAC[]) in
REPEAT STRIP_TAC THEN
(MATCH_MP_TAC(TAUT
`(~q ==> p) /\ (q ==> (p <=> r)) ==> (p <=> q ==> r)`) THEN
CONJ_TAC THENL
[DISCH_TAC THEN MATCH_MP_TAC(SET_RULE `s = {} ==> s SUBSET t`) THEN
REWRITE_TAC[INTERVAL_EQ_EMPTY] THEN ASM_MESON_TAC[REAL_NOT_LT];
ALL_TAC] THEN
DISCH_TAC THEN EQ_TAC THEN REWRITE_TAC[SUBSET_INTERVAL_IMP] THEN
REWRITE_TAC[SUBSET; IN_INTERVAL] THEN
DISCH_THEN(MP_TAC o MATCH_MP lemma) THEN ANTS_TAC THENL
[ASM_MESON_TAC[REAL_LT_BETWEEN; REAL_LE_BETWEEN]; ALL_TAC] THEN
MATCH_MP_TAC MONO_FORALL THEN X_GEN_TAC `i:num` THEN
DISCH_THEN(fun th -> STRIP_TAC THEN MP_TAC th) THEN ASM_REWRITE_TAC[] THEN
FIRST_X_ASSUM(MP_TAC o SPEC `i:num`) THEN
ASM_REWRITE_TAC[] THEN POP_ASSUM_LIST(K ALL_TAC) THEN STRIP_TAC)
THENL
[ASM_MESON_TAC[REAL_LE_TRANS; REAL_LE_REFL];
ASM_MESON_TAC[REAL_LE_TRANS; REAL_LE_REFL];
ALL_TAC; ALL_TAC] THEN
(REPEAT STRIP_TAC THENL
[FIRST_X_ASSUM(MP_TAC o SPEC
`((c:real^N)$i + min ((a:real^N)$i) ((d:real^N)$i)) / &2`) THEN
POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
FIRST_X_ASSUM(MP_TAC o SPEC
`(max ((b:real^N)$i) ((c:real^N)$i) + (d:real^N)$i) / &2`) THEN
POP_ASSUM MP_TAC THEN REAL_ARITH_TAC]));;
let OPEN_INTERVAL_LEMMA = prove
(`!a b x. a < x /\ x < b
==> ?d. &0 < d /\ !x'. abs(x' - x) < d ==> a < x' /\ x' < b`,
REPEAT STRIP_TAC THEN
EXISTS_TAC `min (x - a) (b - x)` THEN REWRITE_TAC[
REAL_LT_MIN] THEN
ASM_REAL_ARITH_TAC);;
let SUMS_INTERVALS = prove
(`(!a b c d:real^N.
~(
interval[a,b] = {}) /\ ~(
interval[c,d] = {})
==> {x + y | x
IN interval[a,b] /\ y
IN interval[c,d]} =
interval[a+c,b+d]) /\
(!a b c d:real^N.
~(
interval(a,b) = {}) /\ ~(
interval(c,d) = {})
==> {x + y | x
IN interval(a,b) /\ y
IN interval(c,d)} =
interval(a+c,b+d))`,
CONJ_TAC THEN REPEAT GEN_TAC THEN REWRITE_TAC[
INTERVAL_NE_EMPTY] THEN
STRIP_TAC THEN REWRITE_TAC[
EXTENSION;
IN_INTERVAL;
IN_ELIM_THM] THEN
REWRITE_TAC[TAUT `(a /\ b) /\ c <=> c /\ a /\ b`] THEN
REWRITE_TAC[VECTOR_ARITH `x:real^N = y + z <=> z = x - y`] THEN
REWRITE_TAC[
UNWIND_THM2;
VECTOR_ADD_COMPONENT;
VECTOR_SUB_COMPONENT] THEN
(X_GEN_TAC `x:real^N` THEN EQ_TAC THENL
[DISCH_THEN(X_CHOOSE_THEN `y:real^N` STRIP_ASSUME_TAC);
DISCH_TAC THEN
REWRITE_TAC[
AND_FORALL_THM; GSYM
LAMBDA_SKOLEM;
TAUT `(p ==> q) /\ (p ==> r) <=> p ==> q /\ r`] THEN
REWRITE_TAC[REAL_ARITH
`((a <= y /\ y <= b) /\ c <= x - y /\ x - y <= d <=>
max a (x - d) <= y /\ y <= min b (x - c)) /\
((a < y /\ y < b) /\ c < x - y /\ x - y < d <=>
max a (x - d) < y /\ y < min b (x - c))`] THEN
REWRITE_TAC[GSYM
REAL_LE_BETWEEN; GSYM
REAL_LT_BETWEEN]] THEN
X_GEN_TAC `i:num` THEN STRIP_TAC THEN
REPEAT(FIRST_X_ASSUM(MP_TAC o SPEC `i:num`)) THEN
ASM_REWRITE_TAC[] THEN ASM_REAL_ARITH_TAC));;
let is_interval = new_definition
`is_interval(s:real^N->bool) <=>
!a b x. a IN s /\ b IN s /\
(!i. 1 <= i /\ i <= dimindex(:N)
==> (a$i <= x$i /\ x$i <= b$i) \/
(b$i <= x$i /\ x$i <= a$i))
==> x IN s`;;let IS_INTERVAL_POINTWISE = prove
(`!s:real^N->bool x.
is_interval s /\
(!i. 1 <= i /\ i <=
dimindex(:N) ==> ?a. a
IN s /\ a$i = x$i)
==> x
IN s`,
REWRITE_TAC[
is_interval] THEN REPEAT STRIP_TAC THEN
SUBGOAL_THEN
`!n. ?y:real^N. (!i. 1 <= i /\ i <= n ==> y$i = (x:real^N)$i) /\ y
IN s`
MP_TAC THENL
[INDUCT_TAC THEN REWRITE_TAC[ARITH_RULE `~(1 <= i /\ i <= 0)`] THENL
[ASM_MESON_TAC[
DIMINDEX_GE_1;
LE_REFL]; ALL_TAC] THEN
FIRST_X_ASSUM(X_CHOOSE_TAC `y:real^N`) THEN
ASM_CASES_TAC `SUC n <=
dimindex(:N)` THENL
[FIRST_X_ASSUM(MP_TAC o SPEC `SUC n`) THEN
ANTS_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN
DISCH_THEN(X_CHOOSE_THEN `z:real^N` STRIP_ASSUME_TAC) THEN
EXISTS_TAC
`(
lambda i. if i <= n then (y:real^N)$i else (z:real^N)$i):real^N` THEN
CONJ_TAC THENL
[X_GEN_TAC `i:num` THEN STRIP_TAC THEN
SUBGOAL_THEN `i <=
dimindex(:N)` ASSUME_TAC THENL
[ASM_ARITH_TAC; ASM_SIMP_TAC[
LAMBDA_BETA]] THEN
COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
SUBGOAL_THEN `i = SUC n` (fun
th -> ASM_REWRITE_TAC[
th]) THEN
ASM_ARITH_TAC;
FIRST_X_ASSUM(ASSUME_TAC o CONJUNCT2) THEN
FIRST_X_ASSUM MATCH_MP_TAC THEN
MAP_EVERY EXISTS_TAC [`y:real^N`; `z:real^N`] THEN
ASM_SIMP_TAC[
LAMBDA_BETA] THEN REAL_ARITH_TAC];
EXISTS_TAC `y:real^N` THEN ASM_REWRITE_TAC[] THEN
SUBGOAL_THEN `y:real^N = x` (fun
th -> REWRITE_TAC[
th]) THEN
REWRITE_TAC[
CART_EQ] THEN
ASM_MESON_TAC[ARITH_RULE `i <= N /\ ~(SUC n <= N) ==> i <= n`]];
DISCH_THEN(MP_TAC o SPEC `
dimindex(:N)`) THEN
REWRITE_TAC[GSYM
CART_EQ] THEN MESON_TAC[]]);;
let IS_INTERVAL_PCROSS_EQ = prove
(`!s:real^M->bool t:real^N->bool.
is_interval(s
PCROSS t) <=>
s = {} \/ t = {} \/
is_interval s /\
is_interval t`,
REPEAT GEN_TAC THEN
ASM_CASES_TAC `s:real^M->bool = {}` THEN
ASM_REWRITE_TAC[
PCROSS_EMPTY;
IS_INTERVAL_EMPTY] THEN
ASM_CASES_TAC `t:real^N->bool = {}` THEN
ASM_REWRITE_TAC[
PCROSS_EMPTY;
IS_INTERVAL_EMPTY] THEN
EQ_TAC THEN REWRITE_TAC[
IS_INTERVAL_PCROSS] THEN
REWRITE_TAC[
is_interval] THEN
REWRITE_TAC[
FORALL_PASTECART;
PASTECART_IN_PCROSS] THEN
STRIP_TAC THEN CONJ_TAC THENL
[MAP_EVERY X_GEN_TAC [`a:real^M`; `b:real^M`; `x:real^M`] THEN
STRIP_TAC THEN UNDISCH_TAC `~(t:real^N->bool = {})` THEN
REWRITE_TAC[GSYM
MEMBER_NOT_EMPTY] THEN
DISCH_THEN(X_CHOOSE_TAC `y:real^N`) THEN
FIRST_X_ASSUM(MP_TAC o SPECL
[`a:real^M`; `y:real^N`; `b:real^M`;
`y:real^N`; `x:real^M`; `y:real^N`]);
MAP_EVERY X_GEN_TAC [`a:real^N`; `b:real^N`; `x:real^N`] THEN
STRIP_TAC THEN UNDISCH_TAC `~(s:real^M->bool = {})` THEN
REWRITE_TAC[GSYM
MEMBER_NOT_EMPTY] THEN
DISCH_THEN(X_CHOOSE_TAC `w:real^M`) THEN
FIRST_X_ASSUM(MP_TAC o SPECL
[`w:real^M`; `a:real^N`; `w:real^M`;
`b:real^N`; `w:real^M`; `x:real^N`])] THEN
ASM_REWRITE_TAC[] THEN DISCH_THEN MATCH_MP_TAC THEN
SIMP_TAC[
pastecart;
LAMBDA_BETA] THEN
REPEAT STRIP_TAC THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[
REAL_LE_REFL] THEN
ASM_MESON_TAC[
DIMINDEX_FINITE_SUM; ARITH_RULE
`1 <= i /\ i <= m + n /\ ~(i <= m) ==> 1 <= i - m /\ i - m <= n`]);;
let IS_INTERVAL_SUMS = prove
(`!s t:real^N->bool.
is_interval s /\
is_interval t
==>
is_interval {x + y | x
IN s /\ y
IN t}`,
REPEAT GEN_TAC THEN REWRITE_TAC[
is_interval] THEN
REWRITE_TAC[
IMP_CONJ;
RIGHT_FORALL_IMP_THM] THEN
REWRITE_TAC[
FORALL_IN_GSPEC] THEN
REWRITE_TAC[
RIGHT_IMP_FORALL_THM] THEN
REWRITE_TAC[IMP_IMP; GSYM
CONJ_ASSOC] THEN
MAP_EVERY X_GEN_TAC
[`a:real^N`; `a':real^N`; `b:real^N`; `b':real^N`; `y:real^N`] THEN
DISCH_THEN(CONJUNCTS_THEN2
(MP_TAC o SPECL [`a:real^N`; `b:real^N`]) MP_TAC) THEN
DISCH_THEN(CONJUNCTS_THEN2
(MP_TAC o SPECL [`a':real^N`; `b':real^N`]) STRIP_ASSUME_TAC) THEN
ASM_REWRITE_TAC[IMP_IMP;
IN_ELIM_THM] THEN ONCE_REWRITE_TAC[
CONJ_SYM] THEN
ONCE_REWRITE_TAC[VECTOR_ARITH `z:real^N = x + y <=> y = z - x`] THEN
REWRITE_TAC[
UNWIND_THM2] THEN MATCH_MP_TAC(MESON[]
`(?x. P x /\ Q(f x))
==> (!x. P x ==> x
IN s) /\ (!x. Q x ==> x
IN t)
==> ?x. x
IN s /\ f x
IN t`) THEN
REWRITE_TAC[
VECTOR_SUB_COMPONENT;
AND_FORALL_THM;
TAUT `(p ==> q) /\ (p ==> r) <=> p ==> q /\ r`] THEN
REWRITE_TAC[GSYM
LAMBDA_SKOLEM] THEN
X_GEN_TAC `i:num` THEN STRIP_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPEC `i:num`) THEN
ASM_REWRITE_TAC[
VECTOR_ADD_COMPONENT] THEN
REWRITE_TAC[REAL_ARITH
`c <= y - x /\ y - x <= d <=> y - d <= x /\ x <= y - c`] THEN
REWRITE_TAC[REAL_ARITH
`a <= x /\ x <= b \/ b <= x /\ x <= a <=> min a b <= x /\ x <= max a b`] THEN
ONCE_REWRITE_TAC[TAUT `(p /\ q) /\ (r /\ s) <=> (p /\ r) /\ (q /\ s)`] THEN
REWRITE_TAC[GSYM
REAL_LE_MIN; GSYM
REAL_MAX_LE] THEN
REWRITE_TAC[GSYM
REAL_LE_BETWEEN] THEN REAL_ARITH_TAC);;
let IN_SEGMENT = prove
(`!a b x:real^N.
(x
IN segment[a,b] <=>
?u. &0 <= u /\ u <= &1 /\ x = (&1 - u) % a + u % b) /\
(x
IN segment(a,b) <=>
~(a = b) /\ ?u. &0 < u /\ u < &1 /\ x = (&1 - u) % a + u % b)`,
let SEGMENT_SYM = prove
(`(!a b:real^N.
segment[a,b] =
segment[b,a]) /\
(!a b:real^N.
segment(a,b) =
segment(b,a))`,
MATCH_MP_TAC(TAUT `a /\ (a ==> b) ==> a /\ b`) THEN
SIMP_TAC[
open_segment] THEN
CONJ_TAC THENL [ALL_TAC; SIMP_TAC[
INSERT_AC]] THEN
REWRITE_TAC[
EXTENSION;
IN_SEGMENT] THEN REPEAT GEN_TAC THEN EQ_TAC THEN
DISCH_THEN(X_CHOOSE_TAC `u:real`) THEN EXISTS_TAC `&1 - u` THEN
ASM_REWRITE_TAC[] THEN
REPEAT CONJ_TAC THEN TRY ASM_ARITH_TAC THEN VECTOR_ARITH_TAC);;
let FINITE_INTER_COLLINEAR_OPEN_SEGMENTS = prove
(`!a b c d:real^N.
collinear{a,b,c}
==> (FINITE(
segment(a,b)
INTER segment(c,d)) <=>
segment(a,b)
INTER segment(c,d) = {})`,
REPEAT GEN_TAC THEN ABBREV_TAC `m:real^N = b - a` THEN POP_ASSUM MP_TAC THEN
GEOM_NORMALIZE_TAC `m:real^N` THEN
SIMP_TAC[
VECTOR_SUB_EQ;
SEGMENT_REFL;
INTER_EMPTY;
FINITE_EMPTY] THEN
X_GEN_TAC `m:real^N` THEN DISCH_TAC THEN REPEAT GEN_TAC THEN
DISCH_THEN(SUBST_ALL_TAC o SYM) THEN POP_ASSUM MP_TAC THEN
GEOM_ORIGIN_TAC `a:real^N` THEN GEOM_BASIS_MULTIPLE_TAC 1 `b:real^N` THEN
X_GEN_TAC `b:real` THEN DISCH_TAC THEN
MAP_EVERY X_GEN_TAC [`x:real^N`; `y:real^N`] THEN
SIMP_TAC[
VECTOR_SUB_RZERO;
NORM_MUL;
NORM_BASIS;
DIMINDEX_GE_1;
LE_REFL] THEN
ASM_REWRITE_TAC[
real_abs;
REAL_MUL_RID] THEN DISCH_THEN SUBST_ALL_TAC THEN
POP_ASSUM(K ALL_TAC) THEN
ASM_CASES_TAC `
collinear{
vec 0:real^N,&1 %
basis 1,y}` THENL
[POP_ASSUM MP_TAC THEN
SIMP_TAC[
COLLINEAR_LEMMA_ALT;
BASIS_NONZERO;
DIMINDEX_GE_1;
LE_REFL] THEN
MATCH_MP_TAC(TAUT
`~a /\ (b ==> c ==> d) ==> a \/ b ==> a \/ c ==> d`) THEN
CONJ_TAC THENL
[SIMP_TAC[
VECTOR_MUL_LID;
BASIS_NONZERO;
DIMINDEX_GE_1;
LE_REFL];
REWRITE_TAC[
LEFT_IMP_EXISTS_THM]] THEN
X_GEN_TAC `b:real` THEN DISCH_THEN SUBST_ALL_TAC THEN
X_GEN_TAC `a:real` THEN DISCH_THEN SUBST_ALL_TAC THEN
REWRITE_TAC[
VECTOR_MUL_ASSOC;
REAL_MUL_RID] THEN
SUBST1_TAC(VECTOR_ARITH `
vec 0:real^N = &0 %
basis 1`) THEN
SIMP_TAC[
SEGMENT_SCALAR_MULTIPLE;
BASIS_NONZERO;
DIMINDEX_GE_1;
LE_REFL;
VECTOR_MUL_RCANCEL;
IMAGE_EQ_EMPTY;
FINITE_IMAGE_INJ_EQ; SET_RULE
`(!x y. x % v = y % v <=> x = y)
==> {x % v | P x}
INTER {x % v | Q x} =
IMAGE (\x. x % v) {x | P x /\ Q x}`] THEN
REWRITE_TAC[REAL_ARITH `(&0 < x /\ x < &1 \/ &1 < x /\ x < &0) /\
(b < x /\ x < a \/ a < x /\ x < b) <=>
max (&0) (min a b) < x /\ x < min (&1) (max a b)`] THEN
SIMP_TAC[
FINITE_REAL_INTERVAL;
EXTENSION;
NOT_IN_EMPTY;
IN_ELIM_THM] THEN
SIMP_TAC[GSYM
REAL_LT_BETWEEN; GSYM
NOT_EXISTS_THM] THEN REAL_ARITH_TAC;
DISCH_TAC THEN ASM_CASES_TAC
`
segment(
vec 0:real^N,&1 %
basis 1)
INTER segment (x,y) = {}` THEN
ASM_REWRITE_TAC[
FINITE_EMPTY] THEN DISCH_THEN(K ALL_TAC) THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM
MEMBER_NOT_EMPTY]) THEN
REWRITE_TAC[
open_segment;
IN_DIFF;
NOT_IN_EMPTY;
DE_MORGAN_THM;
IN_INTER;
IN_INSERT] THEN
DISCH_THEN(X_CHOOSE_THEN `p:real^N` STRIP_ASSUME_TAC) THEN
UNDISCH_TAC `~collinear{
vec 0:real^N,&1 %
basis 1, y}` THEN
RULE_ASSUM_TAC(REWRITE_RULE[
VECTOR_MUL_LID]) THEN
REWRITE_TAC[
VECTOR_MUL_LID] THEN
MATCH_MP_TAC
COLLINEAR_SUBSET THEN
EXISTS_TAC `{p,x:real^N, y,
vec 0,
basis 1}` THEN
CONJ_TAC THENL [ALL_TAC; SET_TAC[]] THEN
MP_TAC(ISPECL [`{y:real^N,
vec 0,
basis 1}`; `p:real^N`; `x:real^N`]
COLLINEAR_TRIPLES) THEN
ASM_REWRITE_TAC[] THEN DISCH_THEN SUBST1_TAC THEN
REWRITE_TAC[
FORALL_IN_INSERT;
NOT_IN_EMPTY] THEN CONJ_TAC THENL
[ONCE_REWRITE_TAC[SET_RULE `{p,x,y} = {x,p,y}`] THEN
MATCH_MP_TAC
BETWEEN_IMP_COLLINEAR THEN
ASM_REWRITE_TAC[
BETWEEN_IN_SEGMENT];
ALL_TAC] THEN
ASM_SIMP_TAC[GSYM
COLLINEAR_4_3] THEN
ONCE_REWRITE_TAC[SET_RULE `{p,x,z,w} = {w,z,p,x}`] THEN
SIMP_TAC[
COLLINEAR_4_3;
BASIS_NONZERO;
DIMINDEX_GE_1; ARITH] THEN
REPEAT(FIRST_X_ASSUM(MP_TAC o MATCH_MP
BETWEEN_IMP_COLLINEAR o
GEN_REWRITE_RULE I [GSYM
BETWEEN_IN_SEGMENT])) THEN
REPEAT(POP_ASSUM MP_TAC) THEN SIMP_TAC[
INSERT_AC]]);;
let AFFINITY_INVERSES = prove
(`!m c. ~(m = &0)
==> (\x. m % x + c) o (\x. inv(m) % x + (--(inv(m) % c))) = I /\
(\x. inv(m) % x + (--(inv(m) % c))) o (\x. m % x + c) = I`,
let REAL_AFFINITY_LE = prove
(`!m c x y. &0 < m ==> (m * x + c <= y <=> x <= inv(m) * y + --(c / m))`,
REWRITE_TAC[REAL_ARITH `m * x + c <= y <=> x * m <= y - c`] THEN
SIMP_TAC[GSYM
REAL_LE_RDIV_EQ] THEN REAL_ARITH_TAC);;
let REAL_LE_AFFINITY = prove
(`!m c x y. &0 < m ==> (y <= m * x + c <=> inv(m) * y + --(c / m) <= x)`,
REWRITE_TAC[REAL_ARITH `y <= m * x + c <=> y - c <= x * m`] THEN
SIMP_TAC[GSYM
REAL_LE_LDIV_EQ] THEN REAL_ARITH_TAC);;
let REAL_AFFINITY_EQ = prove
(`!m c x y. ~(m = &0) ==> (m * x + c = y <=> x = inv(m) * y + --(c / m))`,
CONV_TAC REAL_FIELD);;
let REAL_EQ_AFFINITY = prove
(`!m c x y. ~(m = &0) ==> (y = m * x + c <=> inv(m) * y + --(c / m) = x)`,
CONV_TAC REAL_FIELD);;
let SUMS_IFF = prove
(`!f g k. (!x. x
IN k ==> f x = g x) ==> ((f
sums l) k <=> (g
sums l) k)`,
REPEAT STRIP_TAC THEN REWRITE_TAC[
sums] THEN
AP_THM_TAC THEN AP_THM_TAC THEN AP_TERM_TAC THEN ABS_TAC THEN
MATCH_MP_TAC
VSUM_EQ THEN ASM_SIMP_TAC[
IN_INTER]);;
let SERIES_SUBSET = prove
(`!x s t l.
s
SUBSET t /\
((\i. if i
IN s then x i else
vec 0)
sums l) t
==> (x
sums l) s`,
REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
REWRITE_TAC[
sums] THEN MATCH_MP_TAC EQ_IMP THEN
AP_THM_TAC THEN AP_THM_TAC THEN AP_TERM_TAC THEN ABS_TAC THEN
ASM_SIMP_TAC[GSYM
VSUM_RESTRICT_SET;
FINITE_INTER_NUMSEG] THEN
AP_THM_TAC THEN AP_TERM_TAC THEN POP_ASSUM MP_TAC THEN SET_TAC[]);;
let SUMS_FINITE_DIFF = prove
(`!f:num->real^N t s l.
t
SUBSET s /\ FINITE t /\ (f
sums l) s
==> (f
sums (l -
vsum 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^N` o MATCH_MP
SERIES_FINITE) THEN
ONCE_REWRITE_TAC[GSYM
SERIES_RESTRICT] THEN
REWRITE_TAC[IMP_IMP] THEN ONCE_REWRITE_TAC[
CONJ_SYM] THEN
DISCH_THEN(MP_TAC o MATCH_MP
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 VECTOR_ARITH_TAC);;
let SUMS_FINITE_UNION = prove
(`!f:num->real^N s t l.
FINITE t /\ (f
sums l) s
==> (f
sums (l +
vsum (t
DIFF s) f)) (s
UNION t)`,
REPEAT GEN_TAC THEN
REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
FIRST_ASSUM(MP_TAC o SPEC `s:num->bool` o MATCH_MP
FINITE_DIFF) THEN
DISCH_THEN(MP_TAC o ISPEC `f:num->real^N` o MATCH_MP
SERIES_FINITE) THEN
ONCE_REWRITE_TAC[GSYM
SERIES_RESTRICT] THEN
REWRITE_TAC[IMP_IMP] THEN ONCE_REWRITE_TAC[
CONJ_SYM] THEN
DISCH_THEN(MP_TAC o MATCH_MP
SERIES_ADD) 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;
IN_UNION] THEN
MAP_EVERY ASM_CASES_TAC [`(x:num)
IN s`; `(x:num)
IN t`] THEN
ASM_REWRITE_TAC[] THEN VECTOR_ARITH_TAC);;
let SERIES_CAUCHY = prove
(`!f s. (?l. (f
sums l) s) =
!e. &0 < e
==> ?N. !m n. m >= N
==>
norm(
vsum(s
INTER (m..n)) f) < e`,
REPEAT GEN_TAC THEN REWRITE_TAC[
sums;
CONVERGENT_EQ_CAUCHY;
cauchy] THEN
REWRITE_TAC[
SEQUENCE_CAUCHY_WLOG] THEN ONCE_REWRITE_TAC[
DIST_SYM] THEN
SIMP_TAC[
dist;
VSUM_DIFF_LEMMA;
NORM_VSUM_TRIVIAL_LEMMA] THEN
REWRITE_TAC[
GE; TAUT `a ==> b \/ c <=> a /\ ~b ==> c`] THEN
REWRITE_TAC[
NOT_LT; ARITH_RULE
`(N <= m /\ N <= n /\ m <= n) /\ m + 1 <= n <=>
N + 1 <= m + 1 /\ m + 1 <= n`] 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
EQ_TAC THEN DISCH_THEN(X_CHOOSE_TAC `N:num`) THENL
[EXISTS_TAC `N + 1`; EXISTS_TAC `N:num`] THEN
REPEAT STRIP_TAC THEN
ASM_SIMP_TAC[ARITH_RULE `N + 1 <= m + 1 ==> N <= m + 1`] THEN
FIRST_X_ASSUM(MP_TAC o SPECL [`m - 1`; `n:num`]) THEN
SUBGOAL_THEN `m - 1 + 1 = m` SUBST_ALL_TAC THENL
[ALL_TAC; ANTS_TAC THEN SIMP_TAC[]] THEN
ASM_ARITH_TAC);;
let SUMMABLE_IFF_EVENTUALLY = prove
(`!f g k. (?N. !n. N <= n /\ n
IN k ==> f n = g n)
==> (
summable k f <=>
summable k g)`,
REWRITE_TAC[
summable;
SERIES_CAUCHY] THEN REPEAT GEN_TAC THEN
DISCH_THEN(X_CHOOSE_THEN `N0:num` STRIP_ASSUME_TAC) THEN
AP_TERM_TAC THEN REWRITE_TAC[
FUN_EQ_THM] THEN X_GEN_TAC `e:real` THEN
AP_TERM_TAC THEN EQ_TAC THEN
DISCH_THEN(X_CHOOSE_THEN `N1:num`
(fun
th -> EXISTS_TAC `N0 + N1:num` THEN MP_TAC
th)) THEN
REPEAT(MATCH_MP_TAC
MONO_FORALL THEN GEN_TAC) THEN
DISCH_THEN(fun
th -> DISCH_TAC THEN MP_TAC
th) THEN
(ANTS_TAC THENL [ASM_ARITH_TAC; ALL_TAC]) THEN
MATCH_MP_TAC EQ_IMP THEN AP_THM_TAC THEN AP_TERM_TAC THEN AP_TERM_TAC THEN
MATCH_MP_TAC
VSUM_EQ THEN ASM_SIMP_TAC[
IN_INTER;
IN_NUMSEG] THEN
REPEAT STRIP_TAC THENL [ALL_TAC; CONV_TAC SYM_CONV] THEN
FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN
ASM_ARITH_TAC);;
let SERIES_CAUCHY_UNIFORM = prove
(`!P f:A->num->real^N k.
(?l. !e. &0 < e
==> ?N. !n x. N <= n /\ P x
==>
dist(
vsum(k
INTER (0..n)) (f x),
l x) < e) <=>
(!e. &0 < e ==> ?N. !m n x. N <= m /\ P x
==>
norm(
vsum(k
INTER (m..n)) (f x)) < e)`,
REPEAT GEN_TAC THEN
REWRITE_TAC[
sums;
UNIFORMLY_CONVERGENT_EQ_CAUCHY;
cauchy] THEN
ONCE_REWRITE_TAC[MESON[]
`(!m n:num y. N <= m /\ N <= n /\ P y ==> Q m n y) <=>
(!y. P y ==> !m n. N <= m /\ N <= n ==> Q m n y)`] THEN
REWRITE_TAC[
SEQUENCE_CAUCHY_WLOG] THEN ONCE_REWRITE_TAC[
DIST_SYM] THEN
SIMP_TAC[
dist;
VSUM_DIFF_LEMMA;
NORM_VSUM_TRIVIAL_LEMMA] THEN
REWRITE_TAC[
GE; TAUT `a ==> b \/ c <=> a /\ ~b ==> c`] THEN
REWRITE_TAC[
NOT_LT; ARITH_RULE
`(N <= m /\ N <= n /\ m <= n) /\ m + 1 <= n <=>
N + 1 <= m + 1 /\ m + 1 <= n`] 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
EQ_TAC THEN DISCH_THEN(X_CHOOSE_TAC `N:num`) THENL
[EXISTS_TAC `N + 1`; EXISTS_TAC `N:num`] THEN
REPEAT STRIP_TAC THEN
ASM_SIMP_TAC[ARITH_RULE `N + 1 <= m + 1 ==> N <= m + 1`] THEN
FIRST_X_ASSUM(MP_TAC o SPEC `x:A`) THEN ASM_REWRITE_TAC[] THEN
DISCH_THEN(MP_TAC o SPECL [`m - 1`; `n:num`]) THEN
SUBGOAL_THEN `m - 1 + 1 = m` SUBST_ALL_TAC THENL
[ALL_TAC; ANTS_TAC THEN SIMP_TAC[]] THEN
ASM_ARITH_TAC);;
let SUMMABLE_IMP_TOZERO = prove
(`!f:num->real^N k.
summable k f
==> ((\n. if n
IN k then f(n) else
vec 0) -->
vec 0)
sequentially`,
REPEAT GEN_TAC THEN GEN_REWRITE_TAC LAND_CONV [GSYM
SUMMABLE_RESTRICT] THEN
REWRITE_TAC[
summable;
LIM_SEQUENTIALLY;
INTER_UNIV;
sums] THEN
DISCH_THEN(X_CHOOSE_TAC `l:real^N`) THEN X_GEN_TAC `e:real` THEN
DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC `e / &2`) THEN
ASM_REWRITE_TAC[
REAL_HALF;
LEFT_IMP_EXISTS_THM] THEN
X_GEN_TAC `N:num` THEN DISCH_TAC THEN EXISTS_TAC `N + 1` THEN
X_GEN_TAC `n:num` THEN DISCH_TAC THEN
FIRST_X_ASSUM(fun
th ->
MP_TAC(SPEC `n - 1`
th) THEN MP_TAC(SPEC `n:num`
th)) THEN
ASM_SIMP_TAC[ARITH_RULE `N + 1 <= n ==> N <= n /\ N <= n - 1`] THEN
ABBREV_TAC `m = n - 1` THEN
SUBGOAL_THEN `n = SUC m` SUBST1_TAC THENL
[ASM_ARITH_TAC; ALL_TAC] THEN
REWRITE_TAC[
VSUM_CLAUSES_NUMSEG;
LE_0] THEN
REWRITE_TAC[NORM_ARITH `
dist(x,
vec 0) =
norm x`] THEN
COND_CASES_TAC THEN ASM_REWRITE_TAC[
NORM_0] THEN CONV_TAC NORM_ARITH);;
let SERIES_COMPARISON = prove
(`!f g s. (?l. ((
lift o g)
sums l) s) /\
(?N. !n. n >= N /\ n
IN s ==>
norm(f n) <= g n)
==> ?l:real^N. (f
sums l) s`,
REPEAT GEN_TAC THEN REWRITE_TAC[
SERIES_CAUCHY] THEN
DISCH_THEN(CONJUNCTS_THEN2 MP_TAC (X_CHOOSE_TAC `N1:num`)) THEN
MATCH_MP_TAC
MONO_FORALL THEN X_GEN_TAC `e:real` THEN
MATCH_MP_TAC MONO_IMP THEN REWRITE_TAC[] THEN
DISCH_THEN(X_CHOOSE_TAC `N2:num`) THEN
EXISTS_TAC `N1 + N2:num` THEN
MAP_EVERY X_GEN_TAC [`m:num`; `n:num`] THEN DISCH_TAC THEN
MATCH_MP_TAC
REAL_LET_TRANS THEN
EXISTS_TAC `
norm (
vsum (s
INTER (m .. n)) (
lift o g))` THEN CONJ_TAC THENL
[SIMP_TAC[GSYM
LIFT_SUM;
FINITE_INTER_NUMSEG;
NORM_LIFT] THEN
MATCH_MP_TAC(REAL_ARITH `x <= a ==> x <= abs(a)`) THEN
MATCH_MP_TAC
VSUM_NORM_LE THEN
REWRITE_TAC[
FINITE_INTER_NUMSEG;
IN_INTER;
IN_NUMSEG] THEN
ASM_MESON_TAC[ARITH_RULE `m >= N1 + N2:num /\ m <= x ==> x >= N1`];
ASM_MESON_TAC[ARITH_RULE `m >= N1 + N2:num ==> m >= N2`]]);;
let BANACH_FIX = prove
(`!f s c.
complete s /\ ~(s = {}) /\
&0 <= c /\ c < &1 /\
(
IMAGE f s)
SUBSET s /\
(!x y. x
IN s /\ y
IN s ==>
dist(f(x),f(y)) <= c *
dist(x,y))
==> ?!x:real^N. x
IN s /\ (f x = x)`,
REPEAT STRIP_TAC THEN REWRITE_TAC[
EXISTS_UNIQUE_THM] THEN CONJ_TAC THENL
[ALL_TAC;
MAP_EVERY X_GEN_TAC [`x:real^N`; `y:real^N`] THEN STRIP_TAC THEN
SUBGOAL_THEN `
dist((f:real^N->real^N) x,f y) <= c *
dist(x,y)` MP_TAC THENL
[ASM_MESON_TAC[]; ALL_TAC] THEN
ASM_REWRITE_TAC[REAL_ARITH `a <= c * a <=> &0 <= --a * (&1 - c)`] THEN
ASM_SIMP_TAC[GSYM
REAL_LE_LDIV_EQ;
REAL_SUB_LT;
real_div] THEN
REWRITE_TAC[
REAL_MUL_LZERO; REAL_ARITH `&0 <= --x <=> ~(&0 < x)`] THEN
MESON_TAC[
DIST_POS_LT]] THEN
STRIP_ASSUME_TAC(prove_recursive_functions_exist num_RECURSION
`(z 0 = @x:real^N. x
IN s) /\ (!n. z(SUC n) = f(z n))`) THEN
SUBGOAL_THEN `!n. (z:num->real^N) n
IN s` ASSUME_TAC THENL
[INDUCT_TAC THEN ASM_REWRITE_TAC[] THEN
ASM_MESON_TAC[
MEMBER_NOT_EMPTY;
SUBSET;
IN_IMAGE];
ALL_TAC] THEN
UNDISCH_THEN `z 0 = @x:real^N. x
IN s` (K ALL_TAC) THEN
SUBGOAL_THEN `?x:real^N. x
IN s /\ (z --> x)
sequentially` MP_TAC THENL
[ALL_TAC;
MATCH_MP_TAC
MONO_EXISTS THEN X_GEN_TAC `a:real^N` THEN
STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
ABBREV_TAC `e =
dist(f(a:real^N),a)` THEN
SUBGOAL_THEN `~(&0 < e)` (fun
th -> ASM_MESON_TAC[
th;
DIST_POS_LT]) THEN
DISCH_TAC THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [
LIM_SEQUENTIALLY]) THEN
DISCH_THEN(MP_TAC o SPEC `e / &2`) THEN
ASM_REWRITE_TAC[
REAL_HALF] THEN DISCH_THEN(X_CHOOSE_TAC `N:num`) THEN
SUBGOAL_THEN
`
dist(f(z N),a:real^N) < e / &2 /\
dist(f(z(N:num)),f(a)) < e / &2`
(fun
th -> ASM_MESON_TAC[
th;
DIST_TRIANGLE_HALF_R;
REAL_LT_REFL]) THEN
CONJ_TAC THENL [ASM_MESON_TAC[ARITH_RULE `N <= SUC N`]; ALL_TAC] THEN
MATCH_MP_TAC
REAL_LET_TRANS THEN
EXISTS_TAC `c *
dist((z:num->real^N) N,a)` THEN ASM_SIMP_TAC[] THEN
MATCH_MP_TAC(REAL_ARITH `x < y /\ c * x <= &1 * x ==> c * x < y`) THEN
ASM_SIMP_TAC[
LE_REFL;
REAL_LE_RMUL;
DIST_POS_LE;
REAL_LT_IMP_LE]] THEN
FIRST_ASSUM(MATCH_MP_TAC o GEN_REWRITE_RULE I [
complete]) THEN
ASM_REWRITE_TAC[
CAUCHY] THEN
SUBGOAL_THEN `!n.
dist(z(n):real^N,z(SUC n)) <= c pow n *
dist(z(0),z(1))`
ASSUME_TAC THENL
[INDUCT_TAC THEN
REWRITE_TAC[
real_pow; ARITH; REAL_MUL_LID;
REAL_LE_REFL] THEN
MATCH_MP_TAC
REAL_LE_TRANS THEN
EXISTS_TAC `c *
dist(z(n):real^N,z(SUC n))` THEN
CONJ_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN ASM_SIMP_TAC[
REAL_LE_LMUL];
ALL_TAC] THEN
SUBGOAL_THEN
`!m n:num. (&1 - c) *
dist(z(m):real^N,z(m+n))
<= c pow m *
dist(z(0),z(1)) * (&1 - c pow n)`
ASSUME_TAC THENL
[GEN_TAC THEN INDUCT_TAC THENL
[REWRITE_TAC[
ADD_CLAUSES;
DIST_REFL;
REAL_MUL_RZERO] THEN
MATCH_MP_TAC
REAL_LE_MUL THEN
ASM_SIMP_TAC[
REAL_LE_MUL;
REAL_POW_LE;
DIST_POS_LE;
REAL_SUB_LE;
REAL_POW_1_LE;
REAL_LT_IMP_LE];
ALL_TAC] THEN
MATCH_MP_TAC
REAL_LE_TRANS THEN EXISTS_TAC
`(&1 - c) * (
dist(z m:real^N,z(m + n)) +
dist(z(m + n),z(m + SUC n)))` THEN
ASM_SIMP_TAC[
REAL_LE_LMUL;
REAL_SUB_LE;
REAL_LT_IMP_LE;
DIST_TRIANGLE] THEN
FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH
`c * x <= y ==> c * x' + y <= y' ==> c * (x + x') <= y'`)) THEN
REWRITE_TAC[REAL_ARITH
`q + a * b * (&1 - x) <= a * b * (&1 - y) <=> q <= a * b * (x - y)`] THEN
REWRITE_TAC[
ADD_CLAUSES;
real_pow] THEN
REWRITE_TAC[REAL_ARITH `a * b * (d - c * d) = (&1 - c) * a * d * b`] THEN
MATCH_MP_TAC
REAL_LE_LMUL THEN
ASM_SIMP_TAC[
REAL_SUB_LE;
REAL_LT_IMP_LE] THEN
REWRITE_TAC[GSYM
REAL_POW_ADD; REAL_MUL_ASSOC] THEN ASM_MESON_TAC[];
ALL_TAC] THEN
X_GEN_TAC `e:real` THEN DISCH_TAC THEN
ASM_CASES_TAC `(z:num->real^N) 0 = z 1` THENL
[FIRST_X_ASSUM SUBST_ALL_TAC THEN EXISTS_TAC `0` THEN
REWRITE_TAC[
GE;
LE_0] THEN X_GEN_TAC `n:num` THEN
FIRST_X_ASSUM(MP_TAC o SPECL [`0`; `n:num`]) THEN
REWRITE_TAC[
ADD_CLAUSES;
DIST_REFL;
REAL_MUL_LZERO;
REAL_MUL_RZERO] THEN
ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
ASM_CASES_TAC `(z:num->real^N) 0 = z n` THEN
ASM_REWRITE_TAC[
DIST_REFL;
REAL_NOT_LE] THEN
ASM_SIMP_TAC[
REAL_LT_MUL;
DIST_POS_LT;
REAL_SUB_LT];
ALL_TAC] THEN
MP_TAC(SPECL [`c:real`; `e * (&1 - c) /
dist((z:num->real^N) 0,z 1)`]
REAL_ARCH_POW_INV) THEN
ASM_SIMP_TAC[
REAL_LT_MUL;
REAL_LT_DIV;
REAL_SUB_LT;
DIST_POS_LT] THEN
MATCH_MP_TAC
MONO_EXISTS THEN X_GEN_TAC `N:num` THEN
REWRITE_TAC[
real_div;
GE; REAL_MUL_ASSOC] THEN
ASM_SIMP_TAC[
REAL_LT_RDIV_EQ; GSYM
real_div;
DIST_POS_LT] THEN
ASM_SIMP_TAC[GSYM
REAL_LT_LDIV_EQ;
REAL_SUB_LT] THEN DISCH_TAC THEN
REWRITE_TAC[
LE_EXISTS;
LEFT_IMP_EXISTS_THM] THEN
GEN_TAC THEN X_GEN_TAC `d:num` THEN DISCH_THEN SUBST_ALL_TAC THEN
ONCE_REWRITE_TAC[
DIST_SYM] THEN
FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP(REAL_ARITH
`d < e ==> x <= d ==> x < e`)) THEN
ASM_SIMP_TAC[
REAL_LE_RDIV_EQ;
REAL_SUB_LT] THEN
FIRST_X_ASSUM(MP_TAC o SPECL [`N:num`; `d:num`]) THEN
MATCH_MP_TAC(REAL_ARITH
`(c * d) * e <= (c * d) * &1 ==> x * y <= c * d * e ==> y * x <= c * d`) THEN
MATCH_MP_TAC
REAL_LE_LMUL THEN
ASM_SIMP_TAC[
REAL_LE_MUL;
REAL_POW_LE;
DIST_POS_LE; REAL_ARITH
`&0 <= x ==> &1 - x <= &1`]);;
let EDELSTEIN_FIX = prove
(`!f s.
compact s /\ ~(s = {}) /\ (
IMAGE f s)
SUBSET s /\
(!x y. x
IN s /\ y
IN s /\ ~(x = y) ==>
dist(f(x),f(y)) <
dist(x,y))
==> ?!x:real^N. x
IN s /\ f x = x`,
MAP_EVERY X_GEN_TAC [`g:real^N->real^N`; `s:real^N->bool`] THEN
REPEAT STRIP_TAC THEN REWRITE_TAC[
EXISTS_UNIQUE_THM] THEN CONJ_TAC THENL
[ALL_TAC; ASM_MESON_TAC[
REAL_LT_REFL]] THEN
SUBGOAL_THEN
`!x y. x
IN s /\ y
IN s ==>
dist((g:real^N->real^N)(x),g(y)) <=
dist(x,y)`
ASSUME_TAC THENL
[REPEAT STRIP_TAC THEN ASM_CASES_TAC `x:real^N = y` THEN
ASM_SIMP_TAC[
DIST_REFL;
REAL_LE_LT];
ALL_TAC] THEN
ASM_CASES_TAC `?x:real^N. x
IN s /\ ~(g x = x)` THENL
[ALL_TAC; ASM SET_TAC[]] THEN
FIRST_X_ASSUM(X_CHOOSE_THEN `x:real^N` STRIP_ASSUME_TAC) THEN
ABBREV_TAC `y = (g:real^N->real^N) x` THEN
SUBGOAL_THEN `(y:real^N)
IN s` ASSUME_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
FIRST_ASSUM(MP_TAC o MATCH_MP
COMPACT_PCROSS o W CONJ) THEN
REWRITE_TAC[
compact;
PCROSS] THEN
(STRIP_ASSUME_TAC o prove_general_recursive_function_exists)
`?f:num->real^N->real^N.
(!z. f 0 z = z) /\ (!z n. f (SUC n) z = g(f n z))` THEN
SUBGOAL_THEN `!n z. z
IN s ==> (f:num->real^N->real^N) n z
IN s`
STRIP_ASSUME_TAC THENL [INDUCT_TAC THEN ASM SET_TAC[]; ALL_TAC] THEN
SUBGOAL_THEN
`!m n w z. m <= n /\ w
IN s /\ z
IN s
==>
dist((f:num->real^N->real^N) n w,f n z) <=
dist(f m w,f m z)`
ASSUME_TAC THENL
[REWRITE_TAC[
RIGHT_FORALL_IMP_THM;
IMP_CONJ] THEN
MATCH_MP_TAC
TRANSITIVE_STEPWISE_LE THEN
RULE_ASSUM_TAC(REWRITE_RULE[
SUBSET;
FORALL_IN_IMAGE]) THEN
ASM_SIMP_TAC[
REAL_LE_REFL] THEN MESON_TAC[
REAL_LE_TRANS];
ALL_TAC] THEN
DISCH_THEN(MP_TAC o SPEC
`\n:num.
pastecart (f n (x:real^N)) (f n y:real^N)`) THEN
ANTS_TAC THENL [ASM SET_TAC[]; REWRITE_TAC[
LEFT_IMP_EXISTS_THM]] THEN
MAP_EVERY X_GEN_TAC [`l:real^(N,N)finite_sum`; `s:num->num`] THEN
REWRITE_TAC[
o_DEF;
IN_ELIM_THM] THEN
DISCH_THEN(CONJUNCTS_THEN2 MP_TAC STRIP_ASSUME_TAC) THEN
REWRITE_TAC[
LEFT_IMP_EXISTS_THM] THEN
MAP_EVERY X_GEN_TAC [`a:real^N`; `b:real^N`] THEN
DISCH_THEN(CONJUNCTS_THEN2 STRIP_ASSUME_TAC SUBST_ALL_TAC) THEN
SUBGOAL_THEN
`(\x:real^(N,N)finite_sum.
fstcart x)
continuous_on UNIV /\
(\x:real^(N,N)finite_sum.
sndcart x)
continuous_on UNIV`
MP_TAC THENL
[CONJ_TAC THEN MATCH_MP_TAC
LINEAR_CONTINUOUS_ON THEN
REWRITE_TAC[ETA_AX;
LINEAR_FSTCART;
LINEAR_SNDCART];
ALL_TAC] THEN
REWRITE_TAC[
CONTINUOUS_ON_SEQUENTIALLY;
IN_UNIV] THEN
DISCH_THEN(CONJUNCTS_THEN(fun
th -> FIRST_ASSUM(MP_TAC o MATCH_MP
th))) THEN
REWRITE_TAC[
o_DEF;
FSTCART_PASTECART;
SNDCART_PASTECART; IMP_IMP] THEN
ONCE_REWRITE_TAC[
CONJ_SYM] THEN
DISCH_THEN(fun
th -> CONJUNCTS_THEN2 (LABEL_TAC "A") (LABEL_TAC "B")
th THEN
MP_TAC(MATCH_MP
LIM_SUB th)) THEN
REWRITE_TAC[] THEN DISCH_THEN(LABEL_TAC "AB") THEN
SUBGOAL_THEN
`!n.
dist(a:real^N,b) <=
dist((f:num->real^N->real^N) n x,f n y)`
STRIP_ASSUME_TAC THENL
[X_GEN_TAC `N:num` THEN REWRITE_TAC[GSYM
REAL_NOT_LT] THEN
ONCE_REWRITE_TAC[GSYM
REAL_SUB_LT] THEN DISCH_TAC THEN
USE_THEN "AB" (MP_TAC o REWRITE_RULE[
LIM_SEQUENTIALLY]) THEN
DISCH_THEN(fun
th -> FIRST_X_ASSUM(MP_TAC o MATCH_MP
th)) THEN
REWRITE_TAC[
NOT_EXISTS_THM] THEN X_GEN_TAC `M:num` THEN
DISCH_THEN(MP_TAC o SPEC `M + N:num`) THEN REWRITE_TAC[
LE_ADD] THEN
MATCH_MP_TAC(NORM_ARITH
`
dist(fx,fy) <=
dist(x,y)
==> ~(
dist(fx - fy,a - b) <
dist(a,b) -
dist(x,y))`) THEN
FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN
FIRST_X_ASSUM(MP_TAC o SPEC `M + N:num` o MATCH_MP
MONOTONE_BIGGER) THEN
ARITH_TAC;
ALL_TAC] THEN
SUBGOAL_THEN `b:real^N = a` SUBST_ALL_TAC THENL
[MATCH_MP_TAC(TAUT `(~p ==> F) ==> p`) THEN DISCH_TAC THEN
ABBREV_TAC `e =
dist(a,b) -
dist((g:real^N->real^N) a,g b)` THEN
SUBGOAL_THEN `&0 < e` ASSUME_TAC THENL
[ASM_MESON_TAC[
REAL_SUB_LT]; ALL_TAC] THEN
SUBGOAL_THEN
`?n.
dist((f:num->real^N->real^N) n x,a) < e / &2 /\
dist(f n y,b) < e / &2`
STRIP_ASSUME_TAC THENL
[MAP_EVERY (fun s -> USE_THEN s (MP_TAC o SPEC `e / &2` o
REWRITE_RULE[
LIM_SEQUENTIALLY])) ["A";
let URYSOHN_LOCAL_STRONG = prove
(`!s t u a b.
closed_in (
subtopology euclidean u) s /\
closed_in (
subtopology euclidean u) t /\
s
INTER t = {} /\ ~(a = b)
==> ?f:real^N->real^M.
f
continuous_on u /\
(!x. x
IN u ==> f(x)
IN segment[a,b]) /\
(!x. x
IN u ==> (f x = a <=> x
IN s)) /\
(!x. x
IN u ==> (f x = b <=> x
IN t))`,
let lemma = prove
(`!s t u a b.
closed_in (subtopology euclidean u) s /\
closed_in (subtopology euclidean u) t /\
s INTER t = {} /\ ~(s = {}) /\ ~(t = {}) /\ ~(a = b)
==> ?f:real^N->real^M.
f continuous_on u /\
(!x. x IN u ==> f(x) IN segment[a,b]) /\
(!x. x IN u ==> (f x = a <=> x IN s)) /\
(!x. x IN u ==> (f x = b <=> x IN t))`,
REPEAT STRIP_TAC THEN EXISTS_TAC
`\x:real^N. a + setdist({x},s) / (setdist({x},s) + setdist({x},t)) %
(b - a:real^M)` THEN REWRITE_TAC[] THEN
SUBGOAL_THEN
`(!x:real^N. x IN u ==> (setdist({x},s) = &0 <=> x IN s)) /\
(!x:real^N. x IN u ==> (setdist({x},t) = &0 <=> x IN t))`
STRIP_ASSUME_TAC THENL
[ASM_REWRITE_TAC[SETDIST_EQ_0_SING] THEN CONJ_TAC THENL
[MP_TAC(ISPEC `s:real^N->bool` CLOSED_IN_CLOSED);
MP_TAC(ISPEC `t:real^N->bool` CLOSED_IN_CLOSED)] THEN
DISCH_THEN(MP_TAC o SPEC `u:real^N->bool`) THEN
ASM_REWRITE_TAC[] THEN DISCH_THEN(X_CHOOSE_THEN `v:real^N->bool`
(CONJUNCTS_THEN2 ASSUME_TAC SUBST_ALL_TAC)) THEN
ASM_MESON_TAC[CLOSURE_CLOSED; INTER_SUBSET; SUBSET_CLOSURE; SUBSET;
IN_INTER; CLOSURE_SUBSET];
ALL_TAC] THEN
SUBGOAL_THEN `!x:real^N. x IN u ==> &0 < setdist({x},s) + setdist({x},t)`
ASSUME_TAC THENL
[REPEAT STRIP_TAC THEN MATCH_MP_TAC(REAL_ARITH
`&0 <= x /\ &0 <= y /\ ~(x = &0 /\ y = &0) ==> &0 < x + y`) THEN
REWRITE_TAC[SETDIST_POS_LE] THEN ASM SET_TAC[];
ALL_TAC] THEN
REPEAT CONJ_TAC THENL
[MATCH_MP_TAC CONTINUOUS_ON_ADD THEN REWRITE_TAC[CONTINUOUS_ON_CONST] THEN
REWRITE_TAC[real_div; GSYM VECTOR_MUL_ASSOC] THEN
REPEAT(MATCH_MP_TAC CONTINUOUS_ON_MUL THEN CONJ_TAC) THEN
REWRITE_TAC[CONTINUOUS_ON_CONST; o_DEF] THEN
REWRITE_TAC[CONTINUOUS_ON_LIFT_SETDIST] THEN
MATCH_MP_TAC(REWRITE_RULE[o_DEF] CONTINUOUS_ON_INV) THEN
ASM_SIMP_TAC[REAL_LT_IMP_NZ] THEN
REWRITE_TAC[LIFT_ADD] THEN MATCH_MP_TAC CONTINUOUS_ON_ADD THEN
REWRITE_TAC[CONTINUOUS_ON_LIFT_SETDIST];
X_GEN_TAC `x:real^N` THEN DISCH_TAC THEN
REWRITE_TAC[segment; IN_ELIM_THM] THEN
REWRITE_TAC[VECTOR_MUL_EQ_0; LEFT_OR_DISTRIB; VECTOR_ARITH
`a + x % (b - a):real^N = (&1 - u) % a + u % b <=>
(x - u) % (b - a) = vec 0`;
EXISTS_OR_THM] THEN
DISJ1_TAC THEN ONCE_REWRITE_TAC[CONJ_SYM] THEN
REWRITE_TAC[REAL_SUB_0; UNWIND_THM1] THEN
ASM_SIMP_TAC[REAL_LE_DIV; REAL_LE_ADD; SETDIST_POS_LE; REAL_LE_LDIV_EQ;
REAL_ARITH `a <= &1 * (a + b) <=> &0 <= b`];
REWRITE_TAC[VECTOR_ARITH `a + x:real^N = a <=> x = vec 0`];
REWRITE_TAC[VECTOR_ARITH `a + x % (b - a):real^N = b <=>
(x - &1) % (b - a) = vec 0`]] THEN
ASM_REWRITE_TAC[VECTOR_MUL_EQ_0; VECTOR_SUB_EQ] THEN
ASM_SIMP_TAC[REAL_SUB_0; REAL_EQ_LDIV_EQ;
REAL_MUL_LZERO; REAL_MUL_LID] THEN
REWRITE_TAC[REAL_ARITH `x:real = x + y <=> y = &0`] THEN
ASM_REWRITE_TAC[]) in
MATCH_MP_TAC(MESON[]
`(!s t. P s t <=> P t s) /\
(!s t. ~(s = {}) /\ ~(t = {}) ==> P s t) /\
P {} {} /\ (!t. ~(t = {}) ==> P {} t)
==> !s t. P s t`) THEN
REPEAT CONJ_TAC THENL
[REPEAT GEN_TAC THEN
GEN_REWRITE_TAC (RAND_CONV o BINDER_CONV) [SWAP_FORALL_THM] THEN
REPEAT(AP_TERM_TAC THEN ABS_TAC) THEN
REWRITE_TAC[SEGMENT_SYM; INTER_COMM; CONJ_ACI; EQ_SYM_EQ];
SIMP_TAC[lemma];
REPEAT STRIP_TAC THEN EXISTS_TAC `(\x. midpoint(a,b)):real^N->real^M` THEN
ASM_SIMP_TAC[NOT_IN_EMPTY; CONTINUOUS_ON_CONST; MIDPOINT_IN_SEGMENT] THEN
REWRITE_TAC[midpoint] THEN CONJ_TAC THEN GEN_TAC THEN DISCH_TAC THEN
UNDISCH_TAC `~(a:real^M = b)` THEN REWRITE_TAC[CONTRAPOS_THM] THEN
VECTOR_ARITH_TAC;
REPEAT STRIP_TAC THEN ASM_CASES_TAC `t:real^N->bool = u` THENL
[EXISTS_TAC `(\x. b):real^N->real^M` THEN
ASM_REWRITE_TAC[NOT_IN_EMPTY; ENDS_IN_SEGMENT; IN_UNIV;
CONTINUOUS_ON_CONST];
SUBGOAL_THEN `?c:real^N. c IN u /\ ~(c IN t)` STRIP_ASSUME_TAC THENL
[REPEAT(FIRST_X_ASSUM(MP_TAC o MATCH_MP CLOSED_IN_SUBSET)) THEN
REWRITE_TAC[TOPSPACE_EUCLIDEAN_SUBTOPOLOGY] THEN ASM SET_TAC[];
ALL_TAC] THEN
MP_TAC(ISPECL [`{c:real^N}`; `t:real^N->bool`; `u:real^N->bool`;
`midpoint(a,b):real^M`; `b:real^M`] lemma) THEN
ASM_REWRITE_TAC[CLOSED_IN_SING; MIDPOINT_EQ_ENDPOINT] THEN
ANTS_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
MATCH_MP_TAC MONO_EXISTS THEN SIMP_TAC[NOT_IN_EMPTY] THEN
X_GEN_TAC `f:real^N->real^M` THEN STRIP_TAC THEN CONJ_TAC THENL
[SUBGOAL_THEN
`segment[midpoint(a,b):real^M,b] SUBSET segment[a,b]` MP_TAC
THENL
[REWRITE_TAC[SUBSET; IN_SEGMENT; midpoint] THEN GEN_TAC THEN
DISCH_THEN(X_CHOOSE_THEN `u:real` STRIP_ASSUME_TAC) THEN
EXISTS_TAC `(&1 + u) / &2` THEN ASM_REWRITE_TAC[] THEN
REPEAT(CONJ_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC]) THEN
VECTOR_ARITH_TAC;
ASM SET_TAC[]];
SUBGOAL_THEN `~(a IN segment[midpoint(a,b):real^M,b])` MP_TAC THENL
[ALL_TAC; ASM_MESON_TAC[]] THEN
DISCH_THEN(MP_TAC o CONJUNCT2 o MATCH_MP DIST_IN_CLOSED_SEGMENT) THEN
REWRITE_TAC[DIST_MIDPOINT] THEN
UNDISCH_TAC `~(a:real^M = b)` THEN NORM_ARITH_TAC]]]);;
let BROUWER_REDUCTION_THEOREM_GEN = prove
(`!P s:real^N->bool.
(!f. (!n.
closed(f n) /\ P(f n)) /\ (!n. f(SUC n)
SUBSET f(n))
==> P(
INTERS {f n | n
IN (:num)})) /\
closed s /\ P s
==> ?t. t
SUBSET s /\
closed t /\ P t /\
(!u. u
SUBSET s /\
closed u /\ P u ==> ~(u
PSUBSET t))`,
REPEAT STRIP_TAC THEN
SUBGOAL_THEN
`?b:num->real^N->bool.
(!m n. b m = b n <=> m = n) /\
(!n. open (b n)) /\
(!s. open s ==> (?k. s =
UNIONS {b n | n
IN k}))`
STRIP_ASSUME_TAC THENL
[REWRITE_TAC[
UNIV_SECOND_COUNTABLE_SEQUENCE]; ALL_TAC] THEN
X_CHOOSE_THEN `a:num->real^N->bool` MP_TAC
(prove_recursive_functions_exist num_RECURSION
`a 0 = (s:real^N->bool) /\
(!n. a(SUC n) =
if ?u. u
SUBSET a(n) /\
closed u /\ P u /\ u
INTER (b n) = {}
then @u. u
SUBSET a(n) /\
closed u /\ P u /\ u
INTER (b n) = {}
else a(n))`) THEN
DISCH_THEN(CONJUNCTS_THEN2 (LABEL_TAC "base") (LABEL_TAC "step")) THEN
EXISTS_TAC `
INTERS {a n :real^N->bool | n
IN (:num)}` THEN
SUBGOAL_THEN `!n. (a:num->real^N->bool)(SUC n)
SUBSET a(n)` ASSUME_TAC THENL
[GEN_TAC THEN ASM_REWRITE_TAC[] THEN
COND_CASES_TAC THEN REWRITE_TAC[
SUBSET_REFL] THEN
FIRST_X_ASSUM(MP_TAC o SELECT_RULE) THEN MESON_TAC[];
ALL_TAC] THEN
SUBGOAL_THEN `!n. (a:num->real^N->bool) n
SUBSET s` ASSUME_TAC THENL
[INDUCT_TAC THEN ASM_MESON_TAC[
SUBSET_REFL;
SUBSET_TRANS]; ALL_TAC] THEN
SUBGOAL_THEN `!n.
closed((a:num->real^N->bool) n) /\ P(a n)` ASSUME_TAC THENL
[INDUCT_TAC THEN ASM_REWRITE_TAC[] THEN
COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
FIRST_X_ASSUM(MP_TAC o SELECT_RULE) THEN MESON_TAC[];
ALL_TAC] THEN
REPEAT CONJ_TAC THENL
[ASM SET_TAC[];
MATCH_MP_TAC
CLOSED_INTERS THEN
ASM_REWRITE_TAC[
FORALL_IN_GSPEC;
IN_UNIV] THEN SET_TAC[];
FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[];
X_GEN_TAC `t:real^N->bool` THEN STRIP_TAC THEN
REWRITE_TAC[
PSUBSET_ALT] THEN
DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
REWRITE_TAC[
INTERS_GSPEC;
EXISTS_IN_GSPEC;
IN_UNIV] THEN
DISCH_THEN(X_CHOOSE_THEN `x:real^N` STRIP_ASSUME_TAC) THEN
SUBGOAL_THEN
`?n. x
IN (b:num->real^N->bool)(n) /\ t
INTER b n = {}`
STRIP_ASSUME_TAC THENL
[MP_TAC(ISPEC `(:real^N)
DIFF t`
OPEN_CONTAINS_BALL) THEN
ASM_REWRITE_TAC[GSYM
closed] THEN
DISCH_THEN(MP_TAC o SPEC `x:real^N`) THEN
ASM_REWRITE_TAC[
IN_DIFF;
IN_UNIV;
LEFT_IMP_EXISTS_THM] THEN
REWRITE_TAC[SET_RULE `s
SUBSET UNIV DIFF t <=> t
INTER s = {}`] THEN
X_GEN_TAC `e:real` THEN
DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
MP_TAC(ISPECL [`x:real^N`; `e:real`]
CENTRE_IN_BALL) THEN
FIRST_X_ASSUM(MP_TAC o SPEC `
ball(x:real^N,e)`) THEN
ASM_REWRITE_TAC[
OPEN_BALL;
LEFT_IMP_EXISTS_THM] THEN
X_GEN_TAC `k:num->bool` THEN DISCH_THEN SUBST1_TAC THEN
REWRITE_TAC[
IN_UNIONS;
INTER_UNIONS;
EMPTY_UNIONS;
FORALL_IN_GSPEC] THEN
SET_TAC[];
REMOVE_THEN "step" (MP_TAC o SPEC `n:num`) THEN
COND_CASES_TAC THENL
[DISCH_THEN(ASSUME_TAC o SYM) THEN
FIRST_X_ASSUM(MP_TAC o SELECT_RULE) THEN ASM_REWRITE_TAC[] THEN
ASM SET_TAC[];
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [
NOT_EXISTS_THM]) THEN
DISCH_THEN(MP_TAC o SPEC `t:real^N->bool`) THEN ASM_REWRITE_TAC[] THEN
ASM SET_TAC[]]]]);;
let SUBSEQUENCE_DIAGONALIZATION_LEMMA = prove
(`!P:num->(num->A)->bool.
(!i r:num->A. ?k. (!m n. m < n ==> k m < k n) /\ P i (r o k)) /\
(!i r:num->A k1 k2 N.
P i (r o k1) /\ (!j. N <= j ==> ?j'. j <= j' /\ k2 j = k1 j')
==> P i (r o k2))
==> !r:num->A. ?k. (!m n. m < n ==> k m < k n) /\ (!i. P i (r o k))`,
REPEAT GEN_TAC THEN
DISCH_THEN(CONJUNCTS_THEN2 MP_TAC STRIP_ASSUME_TAC) THEN
GEN_REWRITE_TAC (LAND_CONV o TOP_DEPTH_CONV) [
SKOLEM_THM] THEN
REWRITE_TAC[
FORALL_AND_THM; TAUT
`(p ==> q /\ r) <=> (p ==> q) /\ (p ==> r)`] THEN
DISCH_THEN(X_CHOOSE_THEN
`kk:num->(num->A)->num->num` STRIP_ASSUME_TAC) THEN
X_GEN_TAC `r:num->A` THEN
(STRIP_ASSUME_TAC o prove_recursive_functions_exist num_RECURSION)
`(rr 0 = (kk:num->(num->A)->num->num) 0 r) /\
(!n. rr(SUC n) = rr n o kk (SUC n) (r o rr n))` THEN
EXISTS_TAC `\n. (rr:num->num->num) n n` THEN REWRITE_TAC[ETA_AX] THEN
SUBGOAL_THEN
`(!i. (!m n. m < n ==> (rr:num->num->num) i m < rr i n)) /\
(!i. (P:num->(num->A)->bool) i (r o rr i))`
STRIP_ASSUME_TAC THENL
[REWRITE_TAC[
AND_FORALL_THM] THEN
INDUCT_TAC THEN ASM_REWRITE_TAC[
o_ASSOC] THEN
REWRITE_TAC[
o_THM] THEN ASM_MESON_TAC[];
ALL_TAC] THEN
SUBGOAL_THEN `!i j n. i <= j ==> (rr:num->num->num) i n <= rr j n`
ASSUME_TAC THENL
[REPEAT GEN_TAC THEN GEN_REWRITE_TAC LAND_CONV [
LE_EXISTS] THEN
SIMP_TAC[
LEFT_IMP_EXISTS_THM] THEN SPEC_TAC(`j:num`,`j:num`) THEN
ONCE_REWRITE_TAC[
SWAP_FORALL_THM] THEN SIMP_TAC[
FORALL_UNWIND_THM2] THEN
INDUCT_TAC THEN REWRITE_TAC[
ADD_CLAUSES;
LE_REFL] THEN
ASM_REWRITE_TAC[] THEN FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP
(REWRITE_RULE[
IMP_CONJ]
LE_TRANS)) THEN REWRITE_TAC[
o_THM] THEN
FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP
(MESON[
LE_LT]
`!f:num->num.
(!m n. m < n ==> f m < f n) ==> (!m n. m <= n ==> f m <= f n)`) o
SPEC `i + d:num`) THEN
SPEC_TAC(`n:num`,`n:num`) THEN MATCH_MP_TAC
MONOTONE_BIGGER THEN
ASM_SIMP_TAC[];
ALL_TAC] THEN
CONJ_TAC THENL
[MAP_EVERY X_GEN_TAC [`m:num`; `n:num`] THEN DISCH_TAC THEN
MATCH_MP_TAC
LET_TRANS THEN
EXISTS_TAC `(rr:num->num->num) n m` THEN
ASM_MESON_TAC[
LT_IMP_LE];
ALL_TAC] THEN
SUBGOAL_THEN
`!m n i. n <= m ==> ?j. i <= j /\ (rr:num->num->num) m i = rr n j`
ASSUME_TAC THENL
[ALL_TAC;
X_GEN_TAC `i:num` THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
EXISTS_TAC `(rr:num->num->num) i` THEN ASM_REWRITE_TAC[] THEN
EXISTS_TAC `i:num` THEN ASM_MESON_TAC[]] THEN
SUBGOAL_THEN
`!p d i. ?j. i <= j /\ (rr:num->num->num) (p + d) i = rr p j`
(fun
th -> MESON_TAC[
LE_EXISTS;
th]) THEN
X_GEN_TAC `p:num` THEN MATCH_MP_TAC
num_INDUCTION THEN
ASM_REWRITE_TAC[
ADD_CLAUSES] THEN CONJ_TAC THENL
[MESON_TAC[
LE_REFL]; ALL_TAC] THEN
X_GEN_TAC `d:num` THEN DISCH_THEN(LABEL_TAC "+") THEN
X_GEN_TAC `i:num` THEN ASM_REWRITE_TAC[
o_THM] THEN
REMOVE_THEN "+" (MP_TAC o SPEC
`(kk:num->(num->A)->num->num) (SUC(p + d))
((r:num->A) o (rr:num->num->num) (p + d)) i`) THEN
MATCH_MP_TAC
MONO_EXISTS THEN X_GEN_TAC `j:num` THEN
MATCH_MP_TAC MONO_AND THEN REWRITE_TAC[] THEN
MATCH_MP_TAC(REWRITE_RULE[
IMP_CONJ]
LE_TRANS) THEN
SPEC_TAC(`i:num`,`i:num`) THEN MATCH_MP_TAC
MONOTONE_BIGGER THEN
ASM_REWRITE_TAC[
o_THM] THEN ASM_MESON_TAC[]);;
let ARZELA_ASCOLI = prove
(`!f:num->real^M->real^N s M.
compact s /\
(!n x. x
IN s ==>
norm(f n x) <= M) /\
(!x e. x
IN s /\ &0 < e
==> ?d. &0 < d /\
!n y. y
IN s /\
norm(x - y) < d
==>
norm(f n x - f n y) < e)
==> ?g. g
continuous_on s /\
?r. (!m n:num. m < n ==> r m < r n) /\
!e. &0 < e
==> ?N. !n x. n >= N /\ x
IN s
==>
norm(f(r n) x - g x) < e`,