(* ========================================================================= *) (* Elementary topology in Euclidean space. *) (* ========================================================================= *) parse_as_infix ("open_in",(12,"right"));; parse_as_infix ("closed_in",(12,"right"));; let open_in = new_definition `s open_in u <=> s SUBSET u /\ !x. x IN s ==> ?e. &0 < e /\ !x'. x' IN u /\ dist(x',x) < e ==> x' IN s`;; let closed_in = new_definition `s closed_in u <=> s SUBSET u /\ (u DIFF s) open_in u`;; let OPEN_IN_SUBSET = prove (`!s u. s open_in u ==> s SUBSET u`, SIMP_TAC[open_in]);; let OPEN_IN_EMPTY = prove (`!u. {} open_in u`, REWRITE_TAC[open_in; EMPTY_SUBSET; NOT_IN_EMPTY]);; let OPEN_IN_REFL = prove (`!u. u open_in u`, SIMP_TAC[open_in; SUBSET_REFL] THEN MESON_TAC[REAL_LT_01]);; let OPEN_IN_UNIONS = prove (`!u. (!s. s IN f ==> s open_in u) ==> (UNIONS f) open_in u`, REWRITE_TAC[open_in; SUBSET; IN_UNIONS] THEN MESON_TAC[]);; let OPEN_IN_UNION = prove (`!s t u. s open_in u /\ t open_in u ==> (s UNION t) open_in u`, REWRITE_TAC[open_in; IN_UNION; SUBSET] THEN MESON_TAC[]);; let OPEN_IN_INTER = prove (`!s t u. s open_in u /\ t open_in u ==> (s INTER t) open_in u`, REPEAT GEN_TAC THEN REWRITE_TAC[open_in; IN_INTER] THEN MATCH_MP_TAC(TAUT `(a /\ c ==> e) /\ (b /\ d ==> f) ==> (a /\ b) /\ (c /\ d) ==> e /\ f`) THEN CONJ_TAC THENL [SET_TAC[]; ALL_TAC] THEN REWRITE_TAC[AND_FORALL_THM] THEN MATCH_MP_TAC MONO_FORALL THEN GEN_TAC THEN DISCH_THEN(fun th -> STRIP_TAC THEN MP_TAC th) THEN ASM_REWRITE_TAC[] THEN DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_TAC `d1:real`) (X_CHOOSE_TAC `d2:real`)) THEN MP_TAC(SPECL [`d1:real`; `d2:real`] REAL_DOWN2) THEN ASM_MESON_TAC[REAL_LT_TRANS]);; let OPEN_IN_SUBOPEN = prove (`!s u. s open_in u <=> !x. x IN s ==> ?t. t open_in u /\ x IN t /\ t SUBSET s`, REPEAT GEN_TAC THEN EQ_TAC THENL [MESON_TAC[SUBSET_REFL]; REWRITE_TAC[open_in; SUBSET] THEN MESON_TAC[]]);; let CLOSED_IN_SUBSET = prove (`!s u. s closed_in u ==> s SUBSET u`, SIMP_TAC[closed_in]);; let CLOSED_IN_EMPTY = prove (`!u. {} closed_in u`, REWRITE_TAC[closed_in; EMPTY_SUBSET; DIFF_EMPTY; OPEN_IN_REFL]);; let CLOSED_IN_REFL = prove (`!u. u closed_in u`, REWRITE_TAC[closed_in; SUBSET_REFL; DIFF_EQ_EMPTY; OPEN_IN_EMPTY]);; let CLOSED_IN_UNION = prove (`!s t u. s closed_in u /\ t closed_in u ==> (s UNION t) closed_in u`, let lemma = prove (`s DIFF (t UNION u) = (s DIFF t) INTER (s DIFF u)`,SET_TAC[]) in SIMP_TAC[closed_in; lemma; OPEN_IN_INTER] THEN SET_TAC[]);; let CLOSED_IN_INTER = prove (`!s t u. s closed_in u /\ t closed_in u ==> (s INTER t) closed_in u`, let lemma = prove (`s DIFF (t INTER u) = (s DIFF t) UNION (s DIFF u)`,SET_TAC[]) in SIMP_TAC[closed_in; lemma; OPEN_IN_UNION] THEN SET_TAC[]);; let CLOSED_IN_INTERS = prove (`!u. ~(f = {}) /\ (!s. s IN f ==> s closed_in u) ==> (INTERS f) closed_in u`, let lemma = prove (`s DIFF (INTERS f) = UNIONS {t | ?u. u IN f /\ (t = s DIFF u)}`, GEN_REWRITE_TAC I [EXTENSION] THEN REWRITE_TAC[IN_DIFF; IN_UNIONS; IN_INTERS; IN_ELIM_THM] THEN MESON_TAC[IN_DIFF]) in REWRITE_TAC[closed_in; lemma] THEN REPEAT STRIP_TAC THEN ASM_SIMP_TAC[OPEN_IN_UNIONS; IN_ELIM_THM; LEFT_IMP_EXISTS_THM] THEN POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN SET_TAC[]);; let OPEN_IN_CLOSED_IN = prove (`!s u. s SUBSET u ==> (s open_in u <=> (u DIFF s) closed_in u)`, REPEAT GEN_TAC THEN REWRITE_TAC[closed_in; SUBSET_DIFF] THEN REWRITE_TAC[open_in; IN_DIFF; IN_DIFF; SUBSET] THEN MESON_TAC[]);; let OPEN_IN_CLOSED_IN_EQ = prove (`!s u. s open_in u <=> s SUBSET u /\ (u DIFF s) closed_in u`, MESON_TAC[OPEN_IN_CLOSED_IN; OPEN_IN_SUBSET]);; let OPEN_IN_DIFF = prove (`!s t u. s open_in u /\ t closed_in u ==> (s DIFF t) open_in u`, let lemma = prove (`s SUBSET u ==> ((s DIFF t) = s INTER (u DIFF t))`,SET_TAC[]) in SIMP_TAC[OPEN_IN_SUBSET; lemma; closed_in; OPEN_IN_INTER]);; let CLOSED_IN_DIFF = prove (`!s t u. s closed_in u /\ t open_in u ==> (s DIFF t) closed_in u`, let lemma = prove (`s SUBSET u ==> ((s DIFF t) = s INTER (u DIFF t))`,SET_TAC[]) in SIMP_TAC[CLOSED_IN_SUBSET; lemma] THEN SIMP_TAC[CLOSED_IN_INTER; GSYM OPEN_IN_CLOSED_IN; OPEN_IN_SUBSET]);; (* ------------------------------------------------------------------------- *) (* The "universal" versions are what we use most of the time. *) (* ------------------------------------------------------------------------- *) let open_def_fan = new_definition `open_fan s <=> !x. x IN s ==> ?e. &0 < e /\ !x'. dist(x',x) < e ==> x' IN s`;; let closed_fan = new_definition `closed_fan(s:real^N->bool) <=> open_fan(UNIV DIFF s)`;; let OPEN_IN_FAN = prove (`!s:real^N->bool. open_fan s <=> s open_in UNIV`, REWRITE_TAC[open_def_fan; open_in; SUBSET_UNIV; IN_UNIV]);; let CLOSED_IN_FAN = prove (`!s:real^N->bool. closed_fan s <=> s closed_in UNIV`, REWRITE_TAC[closed_fan; closed_in; SUBSET_UNIV; OPEN_IN_FAN]);; let OPEN_EMPTY_FAN = prove (`open_fan {}`, REWRITE_TAC[OPEN_IN_FAN; OPEN_IN_EMPTY]);; let OPEN_UNIV_FAN = prove (`open_fan(UNIV:real^N->bool)`, REWRITE_TAC[OPEN_IN_FAN; OPEN_IN_REFL]);; let OPEN_UNIONS_FAN = prove (`(!s. s IN f ==> open_fan s) ==> open_fan(UNIONS f)`, REWRITE_TAC[OPEN_IN_FAN; OPEN_IN_UNIONS]);; let OPEN_UNION_FAN = prove (`!s t. open_fan s /\ open_fan t ==> open_fan(s UNION t)`, REWRITE_TAC[OPEN_IN_FAN; OPEN_IN_UNION]);; let OPEN_INTER_FAN = prove (`!s t. open_fan s /\ open_fan t ==> open_fan(s INTER t)`, REWRITE_TAC[OPEN_IN_FAN; OPEN_IN_INTER]);; let OPEN_SUBOPEN_FAN = prove (`!s. open_fan s <=> !x. x IN s ==> ?t. open_fan t /\ x IN t /\ t SUBSET s`, REWRITE_TAC[OPEN_IN_FAN; GSYM OPEN_IN_SUBOPEN]);; let CLOSED_EMPTY_FAN = prove (`closed_fan {}`, REWRITE_TAC[CLOSED_IN_FAN; CLOSED_IN_EMPTY]);; let CLOSED_UNIV_FAN = prove (`closed_fan(UNIV:real^N->bool)`, REWRITE_TAC[CLOSED_IN_FAN; CLOSED_IN_REFL]);; let CLOSED_UNION_FAN = prove (`!s t. closed_fan s /\ closed_fan t ==> closed_fan(s UNION t)`, REWRITE_TAC[CLOSED_IN_FAN; CLOSED_IN_UNION]);; let CLOSED_INTER_FAN = prove (`!s t. closed_fan s /\ closed_fan t ==> closed_fan(s INTER t)`, REWRITE_TAC[CLOSED_IN_FAN; CLOSED_IN_INTER]);; let lemma_closed_inters_fan1 = prove (`s DIFF (INTERS f) = UNIONS {t | ?u. u IN f /\ (t = s DIFF u)}`, GEN_REWRITE_TAC I [EXTENSION] THEN REWRITE_TAC[IN_DIFF; IN_UNIONS; IN_INTERS; IN_ELIM_THM] THEN MESON_TAC[IN_DIFF]);; let CLOSED_INTERS_FAN = prove( `!f. (!s:real^N->bool. s IN f ==> closed_fan s) ==> closed_fan(INTERS f)`, REWRITE_TAC[closed_fan; lemma_closed_inters_fan1] THEN REPEAT STRIP_TAC THEN ASM_SIMP_TAC[OPEN_UNIONS_FAN; IN_ELIM_THM; LEFT_IMP_EXISTS_THM]);; let OPEN_CLOSED_FAN = prove (`!s:real^N->bool. open_fan s <=> closed_fan(UNIV DIFF s)`, SIMP_TAC[OPEN_IN_FAN; CLOSED_IN_FAN; OPEN_IN_CLOSED_IN; SUBSET_UNIV]);; let OPEN_DIFF_FAN = prove (`!s t. open_fan s /\ closed_fan t ==> open_fan(s DIFF t)`, REWRITE_TAC[OPEN_IN_FAN; CLOSED_IN_FAN; OPEN_IN_DIFF]);; let CLOSED_DIFF_FAN = prove (`!s t. closed_fan s /\ open_fan t ==> closed_fan(s DIFF t)`, REWRITE_TAC[OPEN_IN_FAN; CLOSED_IN_FAN; CLOSED_IN_DIFF]);; let OPEN_INTERS_FAN = prove (`!s. FINITE s /\ (!t. t IN s ==> open_fan t) ==> open_fan(INTERS s)`, REWRITE_TAC[GSYM IMP_IMP] THEN MATCH_MP_TAC FINITE_INDUCT_STRONG THEN REWRITE_TAC[INTERS_INSERT; INTERS_0; OPEN_UNIV_FAN; IN_INSERT] THEN MESON_TAC[OPEN_INTER_FAN]);; let CLOSED_UNIONS_FAN = prove (`!s. FINITE s /\ (!t. t IN s ==> closed_fan t) ==> closed_fan(UNIONS s)`, REWRITE_TAC[GSYM IMP_IMP] THEN MATCH_MP_TAC FINITE_INDUCT_STRONG THEN REWRITE_TAC[UNIONS_INSERT; UNIONS_0; CLOSED_EMPTY_FAN; IN_INSERT] THEN MESON_TAC[CLOSED_UNION_FAN]);; (* ------------------------------------------------------------------------- *) (* Open balls. *) (* ------------------------------------------------------------------------- *) let ball_fan = new_definition `ball_fan(x,e) = { y | dist(x,y) < e}`;; let IN_BALL_FAN = prove (`!x y e. y IN (ball_fan(x,e)) <=> dist(x,y) < e`, REWRITE_TAC[ball_fan; IN_ELIM_THM]);; let OPEN_BALL_FAN = prove (`!x e. open_fan(ball_fan(x,e))`, REWRITE_TAC[open_def_fan; ball_fan; IN_ELIM_THM] THEN ONCE_REWRITE_TAC[DIST_SYM] THEN MESON_TAC[REAL_SUB_LT; REAL_LT_SUB_LADD; REAL_ADD_SYM; REAL_LET_TRANS; DIST_TRIANGLE_ALT]);; let CENTRE_IN_BALL = prove (`!x e. x IN ball_fan(x,e) <=> &0 < e`, MESON_TAC[IN_BALL_FAN; DIST_REFL]);; let OPEN_CONTAINS_BALL_FAN = prove (`!s. open_fan s <=> !x. x IN s ==> ?e. &0 < e /\ ball_fan(x,e) SUBSET s`, REWRITE_TAC[open_def_fan; SUBSET; IN_BALL_FAN] THEN REWRITE_TAC[DIST_SYM]);; let BALL_EQ_EMPTY_FAN = prove (`!x e. (ball_fan(x,e) = {}) <=> e <= &0`, REWRITE_TAC[EXTENSION; IN_BALL_FAN; NOT_IN_EMPTY; REAL_NOT_LT] THEN MESON_TAC[DIST_POS_LE; REAL_LE_TRANS; DIST_REFL]);; (* ------------------------------------------------------------------------- *) (* Basic "localization" results are handy for connectedness. *) (* ------------------------------------------------------------------------- *) let OPEN_IN_OPEN_FAN = prove (`!s:real^N->bool u. s open_in u <=> ?t. open_fan t /\ (s = u INTER t)`, REPEAT GEN_TAC THEN EQ_TAC THENL [REWRITE_TAC[open_in] THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC); DISCH_THEN(CHOOSE_THEN(CONJUNCTS_THEN2 MP_TAC SUBST_ALL_TAC)) THEN REWRITE_TAC[open_def_fan; open_in; SUBSET; IN_INTER] THEN MESON_TAC[]] THEN GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [RIGHT_IMP_EXISTS_THM] THEN REWRITE_TAC[SKOLEM_THM] THEN DISCH_THEN(X_CHOOSE_TAC `d:real^N->real`) THEN EXISTS_TAC `UNIONS {b | ?x:real^N. (b = ball_fan(x,d x)) /\ x IN s}` THEN CONJ_TAC THENL [MATCH_MP_TAC OPEN_UNIONS_FAN THEN ASM_SIMP_TAC[IN_ELIM_THM; LEFT_IMP_EXISTS_THM; OPEN_BALL_FAN]; GEN_REWRITE_TAC I [EXTENSION] THEN REWRITE_TAC[IN_INTER; IN_UNIONS; IN_ELIM_THM] THEN ASM_MESON_TAC[SUBSET; DIST_REFL; DIST_SYM; IN_BALL_FAN]]);; let CLOSED_IN_CLOSED_FAN = prove (`!s:real^N->bool u. s closed_in u <=> ?t. closed_fan t /\ (s = u INTER t)`, REPEAT GEN_TAC THEN REWRITE_TAC[closed_in; closed_fan; OPEN_IN_OPEN_FAN] THEN GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [GSYM EXISTS_DIFF] THEN REWRITE_TAC[RIGHT_AND_EXISTS_THM] THEN AP_TERM_TAC THEN ABS_TAC THEN SET_TAC[]);; (* ------------------------------------------------------------------------- *) (* These "transitivity" results are handy too. *) (* ------------------------------------------------------------------------- *) let OPEN_IN_TRANS_FAN = prove (`!s t u. s open_in t /\ t open_in u ==> s open_in u`, ASM_MESON_TAC[OPEN_IN_OPEN_FAN; OPEN_INTER_FAN; INTER_ASSOC]);; let OPEN_IN_OPEN_TRANS_FAN = prove (`!s t. s open_in t /\ open_fan t ==> open_fan s`, MESON_TAC[OPEN_IN_FAN; OPEN_IN_TRANS_FAN; OPEN_UNIV_FAN]);; let CLOSED_IN_TRANS_FAN = prove (`!s t u. s closed_in t /\ t closed_in u ==> s closed_in u`, ASM_MESON_TAC[CLOSED_IN_CLOSED_FAN; CLOSED_INTER_FAN; INTER_ASSOC]);; let CLOSED_IN_CLOSED_TRANS_FAN = prove (`!s t. s closed_in t /\ closed_fan t ==> closed_fan s`, MESON_TAC[CLOSED_IN_FAN; CLOSED_IN_TRANS_FAN; CLOSED_UNIV_FAN]);; (* ------------------------------------------------------------------------- *) (* Connectedness. *) (* ------------------------------------------------------------------------- *) let connected_fan = new_definition `connected_fan s <=> ~(?e1 e2. open_fan e1 /\ open_fan e2 /\ s SUBSET (e1 UNION e2) /\ (e1 INTER e2 INTER s = {}) /\ ~(e1 INTER s = {}) /\ ~(e2 INTER s = {}))`;; (* error in old file*) let CONNECTED_CLOPEN_FAN = prove (`!s. connected_fan s <=> !t. t open_in s /\ t closed_in s ==> (t = {}) \/ (t = s)`, GEN_TAC THEN REWRITE_TAC[connected_fan; OPEN_IN_OPEN_FAN; CLOSED_IN_CLOSED_FAN] THEN GEN_REWRITE_TAC (LAND_CONV o RAND_CONV o BINDER_CONV) [GSYM EXISTS_DIFF] THEN ONCE_REWRITE_TAC[TAUT `(~a <=> b) <=> (a <=> ~b)`] THEN REWRITE_TAC[NOT_FORALL_THM; NOT_IMP; GSYM CONJ_ASSOC; DE_MORGAN_THM] THEN ONCE_REWRITE_TAC[TAUT `a /\ b /\ c /\ d <=> b /\ a /\ c /\ d`] THEN REWRITE_TAC[LEFT_AND_EXISTS_THM] THEN REWRITE_TAC[GSYM closed] THEN ONCE_REWRITE_TAC[SWAP_EXISTS_THM] THEN AP_TERM_TAC THEN ABS_TAC THEN REWRITE_TAC[LEFT_AND_EXISTS_THM; RIGHT_AND_EXISTS_THM] THEN ONCE_REWRITE_TAC[SWAP_EXISTS_THM] THEN AP_TERM_TAC THEN ABS_TAC THEN REWRITE_TAC[TAUT `(a /\ b) /\ (c /\ d) /\ e <=> a /\ c /\ b /\ d /\ e`] THEN REWRITE_TAC[RIGHT_EXISTS_AND_THM; UNWIND_THM2; closed_fan] THEN AP_TERM_TAC THEN AP_TERM_TAC THEN SET_TAC[]);; let CONNECTED_EMPTY_FAN = prove (`connected_fan {}`, REWRITE_TAC[connected_fan; INTER_EMPTY]);; (* ------------------------------------------------------------------------- *) (* Limit points. *) (* ------------------------------------------------------------------------- *) parse_as_infix ("limit_point_of_fan",(12,"right"));; let limit_point_of_fan = new_definition `x limit_point_of_fan s <=> !t. x IN t /\ open_fan t ==> ?y. ~(y = x) /\ y IN s /\ y IN t`;; let LIMPT_APPROACHABLE_FAN = prove (`!x s. x limit_point_of_fan s <=> !e. &0 < e ==> ?x'. x' IN s /\ ~(x' = x) /\ dist(x',x) < e`, REPEAT GEN_TAC THEN REWRITE_TAC[limit_point_of_fan] THEN MESON_TAC[open_def_fan; DIST_SYM; OPEN_BALL_FAN; CENTRE_IN_BALL; IN_BALL_FAN]);; let LIMPT_APPROACHABLE_LE_FAN = prove (`!x s. x limit_point_of_fan s <=> !e. &0 < e ==> ?x'. x' IN s /\ ~(x' = x) /\ dist(x',x) <= e`, REPEAT GEN_TAC THEN REWRITE_TAC[LIMPT_APPROACHABLE_FAN] THEN MATCH_MP_TAC(TAUT `(~a <=> ~b) ==> (a <=> b)`) THEN REWRITE_TAC[NOT_FORALL_THM; NOT_IMP; NOT_EXISTS_THM] THEN REWRITE_TAC[TAUT `~(a /\ b /\ c) <=> c ==> ~(a /\ b)`; APPROACHABLE_LT_LE]);; let LIMPT_UNIV_FAN = prove (`!x:real^N. x limit_point_of_fan UNIV`, GEN_TAC THEN REWRITE_TAC[LIMPT_APPROACHABLE_FAN; IN_UNIV] THEN X_GEN_TAC `e:real` THEN DISCH_TAC THEN SUBGOAL_THEN `?c:real^N. norm(c) = e / &2` CHOOSE_TAC THENL [ASM_SIMP_TAC[VECTOR_CHOOSE_SIZE; REAL_HALF; REAL_LT_IMP_LE]; ALL_TAC] THEN EXISTS_TAC `x + c:real^N` THEN REWRITE_TAC[dist; VECTOR_EQ_ADDR] THEN ASM_REWRITE_TAC[VECTOR_ADD_SUB] THEN SUBGOAL_THEN `&0 < e / &2 /\ e / &2 < e` (fun th -> ASM_MESON_TAC[th; NORM_0; REAL_LT_REFL]) THEN SIMP_TAC[REAL_LT_LDIV_EQ; REAL_LT_RDIV_EQ; REAL_OF_NUM_LT; ARITH] THEN UNDISCH_TAC `&0 < e` THEN REAL_ARITH_TAC);; let CLOSED_LIMPT_FAN = prove (`!s. closed_fan s <=> !x. x limit_point_of_fan s ==> x IN s`, REWRITE_TAC[closed_fan] THEN ONCE_REWRITE_TAC[OPEN_SUBOPEN_FAN] THEN REWRITE_TAC[limit_point_of_fan; IN_DIFF; IN_UNIV; SUBSET] THEN MESON_TAC[]);; let LIMPT_SUBSET_FAN = prove (`!x s t. x limit_point_of_fan s /\ s SUBSET t ==> x limit_point_of_fan t`, REWRITE_TAC[limit_point_of_fan; SUBSET] THEN MESON_TAC[]);; let LIMPT_EMPTY_FAN = prove (`!x. ~(x limit_point_of_fan {})`, REWRITE_TAC[LIMPT_APPROACHABLE_FAN; NOT_IN_EMPTY] THEN MESON_TAC[REAL_LT_01]);; let CLOSED_POSITIVE_ORTHANT_FAN = prove (`closed_fan {x:real^N | !i. 1 <= i /\ i <= dimindex(:N) ==> &0 <= x$i}`, REWRITE_TAC[CLOSED_LIMPT_FAN; LIMPT_APPROACHABLE_FAN] THEN REWRITE_TAC[IN_ELIM_THM] THEN X_GEN_TAC `x:real^N` THEN DISCH_TAC THEN X_GEN_TAC `i:num` THEN STRIP_TAC THEN REWRITE_TAC[GSYM REAL_NOT_LT] THEN DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC `--(x:real^N $ i)`) THEN ASM_REWRITE_TAC[REAL_LT_RNEG; REAL_ADD_LID; NOT_EXISTS_THM] THEN X_GEN_TAC `y:real^N` THEN MATCH_MP_TAC(TAUT `(a ==> ~c) ==> ~(a /\ b /\ c)`) THEN DISCH_TAC THEN MATCH_MP_TAC(REAL_ARITH `!b. abs x <= b /\ b <= a ==> ~(a + x < &0)`) THEN EXISTS_TAC `abs((y - x :real^N)$i)` THEN ASM_SIMP_TAC[dist; COMPONENT_LE_NORM] THEN ASM_SIMP_TAC[VECTOR_SUB_COMPONENT; REAL_ARITH `x < &0 /\ &0 <= y ==> abs(x) <= abs(y - x)`]);; (* ------------------------------------------------------------------------- *) (* Interior of a set. *) (* ------------------------------------------------------------------------- *) let interior_fan = new_definition `interior_fan s = {x | ?t. open_fan t /\ x IN t /\ t SUBSET s}`;; let INTERIOR_EQ_FAN = prove (`!s. (interior_fan s = s) <=> open_fan s`, GEN_TAC THEN REWRITE_TAC[EXTENSION; interior_fan; IN_ELIM_THM] THEN GEN_REWRITE_TAC RAND_CONV [OPEN_SUBOPEN_FAN] THEN MESON_TAC[SUBSET]);; let INTERIOR_OPEN_FAN = prove (`!s. open_fan s ==> (interior_fan s = s)`, MESON_TAC[INTERIOR_EQ_FAN]);; let OPEN_INTERIOR_FAN = prove (`!s. open_fan(interior_fan s)`, GEN_TAC THEN REWRITE_TAC[interior_fan] THEN GEN_REWRITE_TAC I [OPEN_SUBOPEN_FAN] THEN REWRITE_TAC[SUBSET; IN_ELIM_THM] THEN MESON_TAC[]);; let INTERIOR_INTERIOR_FAN = prove (`!s. interior_fan(interior_fan s) = interior_fan s`, MESON_TAC[INTERIOR_EQ_FAN; OPEN_INTERIOR_FAN]);; let INTERIOR_SUBSET_FAN = prove (`!s. (interior_fan s) SUBSET s`, REWRITE_TAC[SUBSET; interior_fan; IN_ELIM_THM] THEN MESON_TAC[]);; let SUBSET_INTERIOR_FAN = prove (`!s t. s SUBSET t ==> (interior_fan s) SUBSET (interior_fan t)`, REWRITE_TAC[interior_fan; SUBSET; IN_ELIM_THM] THEN MESON_TAC[]);; let INTERIOR_MAXIMAL_FAN = prove (`!s t. t SUBSET s /\ open_fan t ==> t SUBSET (interior_fan s)`, REWRITE_TAC[interior_fan; SUBSET; IN_ELIM_THM] THEN MESON_TAC[]);; let INTERIOR_UNIQUE_FAN = prove (`!s t. t SUBSET s /\ open_fan t /\ (!t'. t' SUBSET s /\ open_fan t' ==> t' SUBSET t) ==> (interior_fan s = t)`, MESON_TAC[SUBSET_ANTISYM; INTERIOR_MAXIMAL_FAN; INTERIOR_SUBSET_FAN; OPEN_INTERIOR_FAN]);; let IN_INTERIOR_FAN = prove (`!x s. x IN interior_fan s <=> ?e. &0 < e /\ ball_fan(x,e) SUBSET s`, REWRITE_TAC[interior_fan; IN_ELIM_THM] THEN MESON_TAC[OPEN_CONTAINS_BALL_FAN; SUBSET_TRANS; CENTRE_IN_BALL; OPEN_BALL_FAN]);; (* ------------------------------------------------------------------------- *) (* Closure of a set. *) (* ------------------------------------------------------------------------- *) let closure_fan = new_definition `closure_fan s = s UNION {x | x limit_point_of_fan s}`;; let CLOSURE_INTERIOR_FAN = prove (`!s:real^N->bool. closure_fan s = UNIV DIFF (interior_fan (UNIV DIFF s))`, REWRITE_TAC[EXTENSION; closure_fan; IN_UNION; IN_DIFF; IN_UNIV; interior_fan; IN_ELIM_THM; limit_point_of_fan; SUBSET] THEN MESON_TAC[]);; let lemma_interior_closure = prove(`!s t. UNIV DIFF (UNIV DIFF t) = t`,SET_TAC[]);; let INTERIOR_CLOSURE_FAN = prove (`!s:real^N->bool. interior_fan s = UNIV DIFF (closure_fan (UNIV DIFF s))`, REWRITE_TAC[CLOSURE_INTERIOR_FAN; lemma_interior_closure]);; let lemma_closed_closure = prove(`UNIV DIFF (UNIV DIFF s) = s`,SET_TAC[]);; let CLOSED_CLOSURE_FAN = prove (`!s. closed_fan(closure_fan s)`, REWRITE_TAC[closed_fan; CLOSURE_INTERIOR_FAN; lemma_closed_closure; OPEN_INTERIOR_FAN]);; let CLOSURE_HULL_FAN = prove (`!s. closure_fan s = closed_fan hull s`, GEN_TAC THEN MATCH_MP_TAC(GSYM HULL_UNIQUE) THEN REWRITE_TAC[CLOSED_CLOSURE_FAN; SUBSET] THEN REWRITE_TAC[closure_fan; IN_UNION; IN_ELIM_THM; CLOSED_LIMPT_FAN] THEN MESON_TAC[limit_point_of_fan]);; let CLOSURE_EQ_FAN = prove (`(closure_fan s = s) <=> closed_fan s`, SIMP_TAC[CLOSURE_HULL_FAN; HULL_EQ; CLOSED_INTERS_FAN]);; let CLOSURE_CLOSED_FAN = prove (`!s. closed_fan s ==> (closure_fan s = s)`, MESON_TAC[CLOSURE_EQ_FAN]);; let CLOSURE_CLOSURE_FAN = prove (`!s. closure_fan (closure_fan s) = closure_fan s`, REWRITE_TAC[CLOSURE_HULL_FAN; HULL_HULL]);; let CLOSURE_SUBSET_FAN = prove (`!s. s SUBSET (closure_fan s)`, REWRITE_TAC[CLOSURE_HULL_FAN; HULL_SUBSET]);; let SUBSET_CLOSURE_FAN = prove (`!s t. s SUBSET t ==> (closure_fan s) SUBSET (closure_fan t)`, REWRITE_TAC[CLOSURE_HULL_FAN; HULL_MONO]);; let CLOSURE_MINIMAL_FAN = prove (`!s t. s SUBSET t /\ closed_fan t ==> (closure_fan s) SUBSET t`, REWRITE_TAC[HULL_MINIMAL; CLOSURE_HULL_FAN]);; let CLOSURE_UNIQUE_FAN = prove (`!s t. s SUBSET t /\ closed_fan t /\ (!t'. s SUBSET t' /\ closed_fan t' ==> t SUBSET t') ==> (closure_fan s = t)`, REWRITE_TAC[CLOSURE_HULL_FAN; HULL_UNIQUE]);; (* ------------------------------------------------------------------------- *) (* Frontier (aka boundary). *) (* ------------------------------------------------------------------------- *) let frontier_fan = new_definition `frontier_fan s = (closure_fan s) DIFF (interior_fan s)`;; let FRONTIER_CLOSED_FAN = prove (`!s. closed_fan(frontier_fan s)`, SIMP_TAC[frontier_fan; CLOSED_DIFF_FAN; CLOSED_CLOSURE_FAN; OPEN_INTERIOR_FAN]);; let frotier_closures_fan = prove(`s DIFF (UNIV DIFF t) = s INTER t`,SET_TAC[]);; let FRONTIER_CLOSURES_FAN = prove (`!s:real^N->bool. frontier_fan s = (closure_fan s) INTER (closure_fan(UNIV DIFF s))`, REWRITE_TAC[frontier_fan; INTERIOR_CLOSURE_FAN; frotier_closures_fan]);; let FRONTIER_STRADDLE_FAN = prove (`!a:real^N s. a IN frontier_fan s <=> !e. &0 < e ==> (?x. x IN s /\ dist(a,x) < e) /\ (?x. ~(x IN s) /\ dist(a,x) < e)`, REPEAT GEN_TAC THEN REWRITE_TAC[FRONTIER_CLOSURES_FAN; IN_INTER] THEN REWRITE_TAC[closure_fan; IN_UNION; IN_ELIM_THM; limit_point_of_fan; IN_UNIV; IN_DIFF] THEN ASM_MESON_TAC[IN_BALL_FAN; SUBSET; OPEN_CONTAINS_BALL_FAN; CENTRE_IN_BALL; OPEN_BALL_FAN; DIST_REFL]);; let FRONTIER_SUBSET_CLOSED_FAN = prove (`!s. closed_fan s ==> (frontier_fan s) SUBSET s`, MESON_TAC[frontier_fan; CLOSURE_CLOSED_FAN; SUBSET_DIFF]);; (* ------------------------------------------------------------------------- *) (* A variant of nets (slightly non-standard but good for our purposes). *) (* ------------------------------------------------------------------------- *) let net_tybij_fan = new_type_definition "net_fan" ("mk_net_fan","netord_fan") (prove (`?g:A->A->bool. !x y. (!z. g z x ==> g z y) \/ (!z. g z y ==> g z x)`, EXISTS_TAC `\x:A y:A. F` THEN REWRITE_TAC[]));; let NET_FAN = prove (`!n x y. (!z. netord_fan n z x ==> netord_fan n z y) \/ (!z. netord_fan n z y ==> netord_fan n z x)`, REWRITE_TAC[net_tybij_fan; ETA_AX]);; let OLDNET_FAN = prove (`!n x y. netord_fan n x x /\ netord_fan n y y ==> ?z. netord_fan n z z /\ !w. netord_fan n w z ==> netord_fan n w x /\ netord_fan n w y`, MESON_TAC[NET_FAN]);; (* ------------------------------------------------------------------------- *) (* Common nets and the "within" modifier for nets. *) (* ------------------------------------------------------------------------- *) parse_as_infix("within_fan",(14,"right"));; parse_as_infix("in_direction_fan",(14,"right"));; let at_fan = new_definition `at_fan a = mk_net_fan(\x y. &0 < dist(x,a) /\ dist(x,a) <= dist(y,a))`;; let at_infinity_fan = new_definition `at_infinity_fan = mk_net_fan(\x y. norm(x) >= norm(y))`;; let sequentially_fan = new_definition `sequentially_fan = mk_net_fan(\m:num n. m >= n)`;; let within_fan = new_definition `net_fan within_fan s = mk_net_fan(\x y. netord_fan net_fan x y /\ x IN s)`;; let in_direction_fan = new_definition `a in_direction_fan v = (at_fan a) within_fan {b | ?c. &0 <= c /\ (b - a = c % v)}`;; (* ------------------------------------------------------------------------- *) (* Prove that they are all nets. *) (* ------------------------------------------------------------------------- *) let NET_PROVE_FAN_TAC[def] = REWRITE_TAC[GSYM FUN_EQ_THM; def] THEN REWRITE_TAC[ETA_AX] THEN ASM_SIMP_TAC[GSYM(CONJUNCT2 net_tybij_fan)];; let AT_FAN = prove (`!a:real^N x y. netord_fan(at_fan a) x y <=> &0 < dist(x,a) /\ dist(x,a) <= dist(y,a)`, GEN_TAC THEN NET_PROVE_FAN_TAC[at_fan] THEN MESON_TAC[REAL_LE_TOTAL; REAL_LE_REFL; REAL_LE_TRANS; REAL_LET_TRANS]);; let AT_INFINITY_FAN = prove (`!a:real^N x y. netord_fan at_infinity_fan x y <=> norm(x) >= norm(y)`, GEN_TAC THEN NET_PROVE_FAN_TAC[at_infinity_fan] THEN REWRITE_TAC[real_ge; REAL_LE_REFL] THEN MESON_TAC[REAL_LE_TOTAL; REAL_LE_REFL; REAL_LE_TRANS]);; let SEQUENTIALLY_FAN = prove (`!m n. netord_fan sequentially_fan m n <=> m >= n`, NET_PROVE_FAN_TAC[sequentially_fan] THEN REWRITE_TAC[GE; LE_REFL] THEN MESON_TAC[LE_CASES; LE_REFL; LE_TRANS]);; let WITHIN_FAN = prove (`!n s x y. netord_fan(n within_fan s) x y <=> netord_fan n x y /\ x IN s`, GEN_TAC THEN GEN_TAC THEN REWRITE_TAC[within_fan; GSYM FUN_EQ_THM] THEN REWRITE_TAC[GSYM(CONJUNCT2 net_tybij_fan); ETA_AX] THEN MESON_TAC[NET_FAN]);; let IN_DIRECTION_FAN = prove (`!a v x y. netord_fan(a in_direction_fan v) x y <=> &0 < dist(x,a) /\ dist(x,a) <= dist(y,a) /\ ?c. &0 <= c /\ (x - a = c % v)`, REWRITE_TAC[WITHIN_FAN; AT_FAN; in_direction_fan; IN_ELIM_THM; CONJ_ACI]);; let WITHIN_UNIV_FAN = prove (`!x:real^N. at_fan x within_fan UNIV = at_fan x`, REWRITE_TAC[within_fan; at_fan; IN_UNIV] THEN REWRITE_TAC[ETA_AX; net_tybij_fan]);; (* ------------------------------------------------------------------------- *) (* Identify trivial limits, where we can't approach arbitrarily closely. *) (* ------------------------------------------------------------------------- *) let trivial_limit_fan = new_definition `trivial_limit_fan net_fan <=> (!a:A b. a = b) \/ ?a:A b. ~(a = b) /\ !x. ~(netord_fan(net_fan) x a) /\ ~(netord_fan(net_fan) x b)`;; let TRIVIAL_LIMIT_WITHIN_FAN = prove (`!a:real^N. trivial_limit_fan (at_fan a within_fan s) <=> ~(a limit_point_of_fan s)`, REWRITE_TAC[trivial_limit_fan; LIMPT_APPROACHABLE_LE_FAN; WITHIN_FAN; AT_FAN; DIST_NZ] THEN REPEAT GEN_TAC THEN EQ_TAC THENL [DISCH_THEN(DISJ_CASES_THEN MP_TAC) THENL [MESON_TAC[REAL_LT_01; REAL_LT_REFL; VECTOR_CHOOSE_DIST; DIST_REFL; REAL_LT_IMP_LE]; DISCH_THEN(X_CHOOSE_THEN `b:real^N` (X_CHOOSE_THEN `c:real^N` STRIP_ASSUME_TAC)) THEN SUBGOAL_THEN `&0 < dist(a,b:real^N) \/ &0 < dist(a,c:real^N)` MP_TAC THEN ASM_MESON_TAC[DIST_TRIANGLE; DIST_SYM; GSYM DIST_NZ; GSYM DIST_EQ_0; REAL_ARITH `x <= &0 + &0 ==> ~(&0 < x)`]]; REWRITE_TAC[NOT_FORALL_THM; NOT_IMP; LEFT_IMP_EXISTS_THM] THEN X_GEN_TAC `e:real` THEN DISCH_TAC THEN DISJ2_TAC THEN EXISTS_TAC `a:real^N` THEN SUBGOAL_THEN `?b:real^N. dist(a,b) = e` MP_TAC THENL [ASM_SIMP_TAC[VECTOR_CHOOSE_DIST; REAL_LT_IMP_LE]; ALL_TAC] THEN MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `b:real^N` THEN DISCH_THEN(SUBST_ALL_TAC o SYM) THEN ASM_MESON_TAC[REAL_NOT_LE; DIST_REFL; DIST_NZ; DIST_SYM]]);; let TRIVIAL_LIMIT_AT_FAN = prove (`!a. ~(trivial_limit_fan (at_fan a))`, ONCE_REWRITE_TAC[GSYM WITHIN_UNIV_FAN] THEN REWRITE_TAC[TRIVIAL_LIMIT_WITHIN_FAN; LIMPT_UNIV_FAN]);; let TRIVIAL_LIMIT_AT_INFINITY_FAN = prove (`~(trivial_limit_fan at_infinity_fan)`, REWRITE_TAC[trivial_limit_fan; AT_INFINITY_FAN; real_ge] THEN MESON_TAC[REAL_LE_REFL; VECTOR_CHOOSE_SIZE; REAL_LT_01; REAL_LT_LE]);; let TRIVIAL_LIMIT_SEQUENTIALLY_FAN = prove (`~(trivial_limit_fan sequentially_fan)`, REWRITE_TAC[trivial_limit_fan; SEQUENTIALLY_FAN] THEN MESON_TAC[GE_REFL; NOT_SUC]);; (* ------------------------------------------------------------------------- *) (* Limits, defined as vacuously true when the limit is trivial. *) (* ------------------------------------------------------------------------- *) parse_as_infix("-->",(12,"right"));; let lim_fan = new_definition `(f --> l) net_fan <=> trivial_limit_fan net_fan \/ !e. &0 < e ==> ?y. (?x. netord_fan(net_fan) x y) /\ !x. netord_fan(net_fan) x y ==> dist(f(x),l) < e`;; (* ------------------------------------------------------------------------- *) (* Show that they yield usual definitions in the various cases. *) (* ------------------------------------------------------------------------- *) let LIM_WITHIN_LE_FAN = prove (`!f:real^M->real^N l a s. (f --> l)(at_fan a within_fan s) <=> !e. &0 < e ==> ?d. &0 < d /\ !x. x IN s /\ &0 < dist(x,a) /\ dist(x,a) <= d ==> dist(f(x),l) < e`, REPEAT GEN_TAC THEN REWRITE_TAC[lim_fan; AT_FAN; WITHIN_FAN; TRIVIAL_LIMIT_WITHIN_FAN] THEN REWRITE_TAC[LIMPT_APPROACHABLE_LE_FAN; DIST_NZ] THEN EQ_TAC THENL [DISCH_THEN(DISJ_CASES_THEN MP_TAC) THENL [ALL_TAC; MATCH_MP_TAC MONO_FORALL] THEN MESON_TAC[REAL_LTE_TRANS]; MATCH_MP_TAC(TAUT `(b ==> a ==> c) ==> (a ==> ~b \/ c)`) THEN DISCH_TAC 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 `d:real` STRIP_ASSUME_TAC) THEN SUBGOAL_THEN `?b:real^M. dist(a,b) = d` MP_TAC THENL [ASM_SIMP_TAC[VECTOR_CHOOSE_DIST; REAL_LT_IMP_LE]; ALL_TAC] THEN MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `b:real^M` THEN DISCH_THEN(SUBST_ALL_TAC o SYM) THEN ASM_MESON_TAC[REAL_NOT_LE; DIST_REFL; DIST_NZ; DIST_SYM]]);; let LIM_WITHIN_FAN = prove (`!f:real^M->real^N l a s. (f --> l) (at_fan a within_fan s) <=> !e. &0 < e ==> ?d. &0 < d /\ !x. x IN s /\ &0 < dist(x,a) /\ dist(x,a) < d ==> dist(f(x),l) < e`, REWRITE_TAC[LIM_WITHIN_LE_FAN] THEN ONCE_REWRITE_TAC[TAUT `a /\ b /\ c ==> d <=> c ==> a /\ b ==> d`] THEN REWRITE_TAC[APPROACHABLE_LT_LE]);; let LIM_AT_FAN = prove (`!f l:real^N a:real^M. (f --> l) (at_fan a) <=> !e. &0 < e ==> ?d. &0 < d /\ !x. &0 < dist(x,a) /\ dist(x,a) < d ==> dist(f(x),l) < e`, ONCE_REWRITE_TAC[GSYM WITHIN_UNIV_FAN] THEN REWRITE_TAC[LIM_WITHIN_FAN; IN_UNIV]);; let LIM_AT_INFINITY_FAN = prove (`!f l. (f --> l) at_infinity_fan <=> !e. &0 < e ==> ?b. !x. norm(x) >= b ==> dist(f(x),l) < e`, REWRITE_TAC[lim_fan; AT_INFINITY_FAN; TRIVIAL_LIMIT_AT_INFINITY_FAN] THEN REPEAT GEN_TAC THEN EQ_TAC THENL [MESON_TAC[REAL_LE_REFL]; ALL_TAC] THEN MATCH_MP_TAC MONO_FORALL THEN MESON_TAC[real_ge; REAL_LE_REFL; VECTOR_CHOOSE_SIZE; REAL_ARITH `&0 <= b \/ (!x. x >= &0 ==> x >= b)`]);; let LIM_SEQUENTIALLY_FAN = prove (`!s l. (s --> l) sequentially_fan <=> !e. &0 < e ==> ?N. !n. N <= n ==> dist(s(n),l) < e`, REWRITE_TAC[lim_fan; SEQUENTIALLY_FAN; GE; LE_REFL; TRIVIAL_LIMIT_SEQUENTIALLY_FAN] THEN MESON_TAC[LE_REFL]);; (* ------------------------------------------------------------------------- *) (* The expected monotonicity property. *) (* ------------------------------------------------------------------------- *) let LIM_WITHIN_SUBSET_FAN = prove (`!f l a s. (f --> l) (at_fan a within_fan s) /\ t SUBSET s ==> (f --> l) (at_fan a within_fan t)`, REWRITE_TAC[LIM_WITHIN_FAN; SUBSET] THEN MESON_TAC[]);; (* ------------------------------------------------------------------------- *) (* Interrelations between restricted and unrestricted limits. *) (* ------------------------------------------------------------------------- *) let LIM_AT_WITHIN_FAN = prove (`!f l a s. (f --> l)(at_fan a) ==> (f --> l)(at_fan a within_fan s)`, REWRITE_TAC[LIM_AT_FAN; LIM_WITHIN_FAN] THEN MESON_TAC[]);; let LIM_WITHIN_OPEN_FAN = prove (`!f l a:real^M s. a IN s /\ open_fan s ==> ((f --> l)(at_fan a within_fan s) <=> (f --> l)(at_fan a))`, REPEAT STRIP_TAC THEN EQ_TAC THEN SIMP_TAC[LIM_AT_WITHIN_FAN] THEN REWRITE_TAC[LIM_AT_FAN; LIM_WITHIN_FAN] 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_fan]) 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]);; (* ------------------------------------------------------------------------- *) (* Another limit point characterization. *) (* ------------------------------------------------------------------------- *) let LIMPT_SEQUENTIAL_FAN = prove (`!x:real^N s. x limit_point_of_fan s <=> ?f. (!n. f(n) IN (s DELETE x)) /\ (f --> x) sequentially_fan`, REPEAT GEN_TAC THEN REWRITE_TAC[LIMPT_APPROACHABLE_FAN; LIM_SEQUENTIALLY_FAN; IN_DELETE] THEN EQ_TAC THENL [ALL_TAC; MESON_TAC[GE; LE_REFL]] THEN DISCH_THEN(MP_TAC o GEN `n:num` o SPEC `inv(&n + &1)`) THEN SIMP_TAC[REAL_LT_INV_EQ; REAL_ARITH `&0 <= x ==> &0 < x + &1`; REAL_POS] THEN REWRITE_TAC[SKOLEM_THM] THEN MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `f:num->real^N` THEN REWRITE_TAC[FORALL_AND_THM] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC FORALL_POS_MONO_1 THEN CONJ_TAC THENL [MESON_TAC[REAL_LT_TRANS]; ALL_TAC] THEN X_GEN_TAC `n:num` THEN EXISTS_TAC `n:num` THEN REWRITE_TAC[GSYM GE] THEN MATCH_MP_TAC SEQ_MONO_LEMMA THEN ASM_REWRITE_TAC[] THEN SIMP_TAC[REAL_LE_INV2; GE; REAL_OF_NUM_LE; REAL_LE_RADD; GE_REFL; REAL_POS; REAL_ARITH `&0 <= x ==> &0 < x + &1`]);; (* ------------------------------------------------------------------------- *) (* Basic arithmetical combining theorems for limits. *) (* ------------------------------------------------------------------------- *) let NET_DILEMMA_FAN = prove (`!net. (?a. (?x. netord_fan net_fan x a) /\ (!x. netord_fan net_fan x a ==> P x)) /\ (?b. (?x. netord_fan net_fan x b) /\ (!x. netord_fan net_fan x b ==> Q x)) ==> ?c. (?x. netord_fan net_fan x c) /\ (!x. netord_fan net_fan x c ==> P x /\ Q x)`, MESON_TAC[NET_FAN]);; let LIM_LINEAR_FAN = prove (`!net_fan:(A)net_fan h f l. (f --> l) net_fan /\ linear h ==> ((\x. h(f x)) --> h l) net_fan`, REPEAT GEN_TAC THEN REWRITE_TAC[lim_fan] THEN ASM_CASES_TAC `trivial_limit_fan (net_fan:(A)net_fan)` THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN FIRST_ASSUM(X_CHOOSE_THEN `B:real` STRIP_ASSUME_TAC o MATCH_MP LINEAR_BOUNDED_POS) THEN X_GEN_TAC `e:real` THEN DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC `e / B`) THEN ASM_SIMP_TAC[REAL_LT_DIV; dist; GSYM LINEAR_SUB; REAL_LT_RDIV_EQ] THEN ASM_MESON_TAC[REAL_LET_TRANS; REAL_MUL_SYM]);; let LIM_CONST_FAN = prove (`!net_fan a:real^N. ((\x. a) --> a) net_fan`, SIMP_TAC[lim_fan; DIST_REFL; trivial_limit_fan] THEN MESON_TAC[]);; let LIM_CMUL_FAN = prove (`!f l c. (f --> l) net_fan ==> ((\x. c % f x) --> c % l) net_fan`, REPEAT STRIP_TAC THEN MATCH_MP_TAC LIM_LINEAR_FAN THEN ASM_REWRITE_TAC[REWRITE_RULE[ETA_AX] (MATCH_MP LINEAR_COMPOSE_CMUL LINEAR_ID)]);; let LIM_NEG_FAN = prove (`!f l:real^N. (f --> l) net_fan ==> ((\x. --(f x)) --> --l) net_fan`, REPEAT GEN_TAC THEN REWRITE_TAC[lim_fan; dist] THEN REWRITE_TAC[VECTOR_ARITH `--x - --y = --(x - y:real^N)`; NORM_NEG]);; (* error in old file*) let LIM_ADD_FAN = prove (`!net_fan:(A)net_fan f g l m. (f --> l) net_fan /\ (g --> m) net_fan ==> ((\x. f(x) + g(x)) --> l + m) net_fan`, REPEAT GEN_TAC THEN REWRITE_TAC[lim_fan] THEN ASM_CASES_TAC `trivial_limit_fan (net_fan:(A)net_fan)` THEN ASM_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_FAN) THEN REWRITE_TAC[MONO_EXISTS] THEN MESON_TAC[REAL_HALF; DIST_TRIANGLE_ADD; REAL_LT_ADD2; REAL_LET_TRANS]);; let LIM_SUB_FAN = prove (`!net_fan:(A)net_fan f g l m. (f --> l) net_fan /\ (g --> m) net_fan ==> ((\x. f(x) - g(x)) --> l - m) net_fan`, REWRITE_TAC[real_sub; VECTOR_SUB] THEN ASM_SIMP_TAC[LIM_ADD_FAN; LIM_NEG_FAN]);; let LIM_NULL_FAN = prove (`!net_fan f l. (f --> l) net_fan <=> ((\x. f(x) - l) --> vec 0) net_fan`, REWRITE_TAC[lim_fan; dist; VECTOR_SUB_RZERO]);; (* ------------------------------------------------------------------------- *) (* We need some non-triviality conditions on these two. *) (* ------------------------------------------------------------------------- *) let LIM_NORM_BOUND_FAN = prove (`!f (l:real^N) net_fan:(A)net_fan. ~(trivial_limit_fan net_fan) /\ (f --> l) net_fan /\ (?y. (?x. netord_fan net_fan x y) /\ !x. netord_fan net_fan x y ==> norm(f x) <= e) ==> norm(l) <= e`, REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN ASM_REWRITE_TAC[lim_fan] THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN STRIP_TAC THEN REWRITE_TAC[GSYM REAL_NOT_LT] THEN ONCE_REWRITE_TAC[GSYM REAL_SUB_LT] THEN DISCH_TAC THEN SUBGOAL_THEN `?x:A. dist(f(x):real^N,l) < norm(l:real^N) - e /\ norm(f x) <= e` (CHOOSE_THEN MP_TAC) THENL [ASM_MESON_TAC[NET_FAN]; ALL_TAC] THEN REWRITE_TAC[REAL_NOT_LT; REAL_LE_SUB_RADD; DE_MORGAN_THM; dist] THEN ASM_MESON_TAC[NORM_TRIANGLE; NORM_SUB; VECTOR_SUB_ADD; REAL_ARITH `nl <= nd + nx /\ nx <= e ==> nl <= nd + e`]);; let LIM_UNIQUE_FAN = prove (`!net_fan:(A)net_fan f l:real^N l'. ~(trivial_limit_fan net_fan) /\ (f --> l) net_fan /\ (f --> l') net_fan ==> (l = l')`, REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN DISCH_THEN(ASSUME_TAC o REWRITE_RULE[VECTOR_SUB_REFL] o MATCH_MP LIM_SUB_FAN) THEN SUBGOAL_THEN `!e. &0 < e ==> norm(l:real^N - l') <= e` MP_TAC THENL [GEN_TAC THEN DISCH_TAC THEN MATCH_MP_TAC LIM_NORM_BOUND_FAN THEN MAP_EVERY EXISTS_TAC [`\x:A. vec 0 : real^N`; `net_fan:(A)net_fan`] THEN ASM_SIMP_TAC[NORM_0; REAL_LT_IMP_LE] THEN ASM_MESON_TAC[trivial_limit_fan]; ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN REWRITE_TAC[DIST_NZ; dist] THEN DISCH_TAC THEN DISCH_THEN(MP_TAC o SPEC `norm(l - l':real^N) / &2`) THEN ASM_SIMP_TAC[REAL_LT_RDIV_EQ; REAL_LE_RDIV_EQ; REAL_OF_NUM_LT; ARITH] THEN UNDISCH_TAC `&0 < norm(l - l':real^N)` THEN REAL_ARITH_TAC]);; (* ------------------------------------------------------------------------- *) (* Limit under bilinear function (surprisingly tedious, but important). *) (* ------------------------------------------------------------------------- *) let NORM_BOUND_LEMMA_FAN = prove (`!x:real^M y:real^N e. &0 < e ==> ?d. &0 < d /\ !x' y'. norm(x' - x) < d /\ norm(y' - y) < d ==> norm(x') * norm(y' - y) + norm(x' - x) * norm(y) < e`, REPEAT STRIP_TAC THEN EXISTS_TAC `min (&1) (e / &2 / (norm(x:real^M) + norm(y:real^N) + &1))` THEN ASM_SIMP_TAC[REAL_LT_MIN; REAL_LT_DIV; REAL_OF_NUM_LT; NORM_POS_LE; ARITH; REAL_LT_RDIV_EQ; REAL_ARITH `&0 <= x /\ &0 <= y ==> &0 < x + y + &1`] THEN REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC `(norm(x:real^M) + &1) * norm(y' - y) + norm(x' - x) * norm(y:real^N)` THEN CONJ_TAC THENL [REWRITE_TAC[REAL_LE_RADD; GSYM REAL_ADD_RDISTRIB] THEN MATCH_MP_TAC REAL_LE_RMUL THEN REWRITE_TAC[NORM_POS_LE] THEN ASM_MESON_TAC[NORM_TRIANGLE_SUB; REAL_ARITH `x' <= x + d /\ d < &1 ==> x' <= x + &1`]; MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC `(norm(x:real^M) + norm(y:real^N) + &1) * (norm(x' - x) + norm(y' - y))` THEN CONJ_TAC THENL [ALL_TAC; REPEAT(POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC] THEN MATCH_MP_TAC(REAL_ARITH `y * xd <= p * xd /\ x * yd <= p * yd ==> x * yd + xd * y <= p * (xd + yd)`) THEN CONJ_TAC THEN MATCH_MP_TAC REAL_LE_RMUL THEN REWRITE_TAC[NORM_POS_LE] THENL [MP_TAC(ISPEC `x:real^M` NORM_POS_LE); MP_TAC(ISPEC `y:real^N` NORM_POS_LE)] THEN REAL_ARITH_TAC]);; (*let LIM_BILINEAR_FAN = prove (;; g`!net_fan:(A)net_fan (h:real^M->real^N->real^P) f g l m. (f --> l) net_fan /\ (g --> m) net_fan /\ bilinear h ==> ((\x. h (f x) (g x)) --> (h l m)) net_fan`;; ,;; e( REPEAT GEN_TAC THEN REWRITE_TAC[lim_fan] THEN ASM_CASES_TAC `trivial_limit_fan (net_fan:(A)net_fan)` THEN ASM_REWRITE_TAC[AND_FORALL_THM; CONJ_ASSOC] THEN STRIP_TAC THEN X_GEN_TAC `e:real` THEN DISCH_TAC THEN FIRST_ASSUM(X_CHOOSE_THEN `B:real` STRIP_ASSUME_TAC o MATCH_MP BILINEAR_BOUNDED_POS) THEN MP_TAC(ISPECL [`l:real^M`; `m:real^N`; `e / B`] NORM_BOUND_LEMMA_FAN) THEN ASM_SIMP_TAC[REAL_LT_RDIV_EQ; REAL_MUL_LZERO] THEN DISCH_THEN(X_CHOOSE_THEN `d:real` STRIP_ASSUME_TAC) THEN FIRST_X_ASSUM(MP_TAC o SPEC `d:real`) THEN ASM_REWRITE_TAC[] THEN DISCH_THEN(MP_TAC o MATCH_MP NET_DILEMMA_FAN));; THEN ;; e(REWRITE_TAC[MONO_EXISTS]);; THEN;; e(X_GEN_TAC `c:A`);; MONO_AND;; e(DISCH_TAC);; e( MATCH_MP_TAC MONO_AND);; THEN REWRITE_TAC[] THEN MATCH_MP_TAC MONO_FORALL THEN X_GEN_TAC `a:A` THEN MATCH_MP_TAC MONO_IMP THEN REWRITE_TAC[dist] THEN DISCH_THEN(fun th -> FIRST_X_ASSUM(ASSUME_TAC o C MATCH_MP th)) THEN ONCE_REWRITE_TAC[VECTOR_ARITH `h a b - h c d :real^N = (h a b - h a d) + (h a d - h c d)`] THEN MATCH_MP_TAC NORM_TRIANGLE_LT THEN ASM_SIMP_TAC[GSYM BILINEAR_LSUB; GSYM BILINEAR_RSUB] THEN FIRST_X_ASSUM(fun th -> MP_TAC(SPECL [`(f:A->real^M) a`; `(g:A->real^N) a - m`] th) THEN MP_TAC(SPECL [`(f:A->real^M) a - l`; `m:real^N`] th)) THEN REPEAT(POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC);; *) (* ------------------------------------------------------------------------- *) (* These are special for limits out of the same vector space. *) (* ------------------------------------------------------------------------- *) let LIM_WITHIN_ID_FAN = prove (`!a s. ((\x. x) --> a) (at_fan a within_fan s)`, REWRITE_TAC[LIM_WITHIN_FAN] THEN MESON_TAC[]);; let LIM_AT_ID_FAN = prove (`!a. ((\x. x) --> a) (at_fan a)`, ONCE_REWRITE_TAC[GSYM WITHIN_UNIV_FAN] THEN REWRITE_TAC[LIM_WITHIN_ID_FAN]);; let LIM_AT_ZERO_FAN = prove (`!f:real^M->real^N l a. (f --> l) (at_fan a) <=> ((\x. f(a + x)) --> l) (at_fan(vec 0))`, REPEAT GEN_TAC THEN REWRITE_TAC[LIM_AT_FAN] 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]]);; (* ------------------------------------------------------------------------- *) (* It's also sometimes useful to extract the limit point from the net. *) (* ------------------------------------------------------------------------- *) let netlimit_fan = new_definition `netlimit_fan net_fan = @a. !x. ~(netord_fan net_fan x a)`;; let NETLIMIT_WITHIN_FAN = prove (`!a:real^N s. ~(trivial_limit_fan (at_fan a within_fan s)) ==> (netlimit_fan (at_fan a within_fan s) = a)`, REWRITE_TAC[trivial_limit_fan; netlimit_fan; AT_FAN; WITHIN_FAN; DE_MORGAN_THM] THEN REPEAT STRIP_TAC THEN MATCH_MP_TAC SELECT_UNIQUE THEN REWRITE_TAC[] THEN SUBGOAL_THEN `!x:real^N. ~(&0 < dist(x,a) /\ dist(x,a) <= dist(a,a) /\ x IN s)` ASSUME_TAC THENL [ASM_MESON_TAC[DIST_REFL; REAL_NOT_LT]; ASM_MESON_TAC[]]);; (* ------------------------------------------------------------------------- *) (* Useful lemmas on closure and set of possible sequential limits. *) (* ------------------------------------------------------------------------- *) let CLOSURE_SEQUENTIAL_FAN = prove (`!s l:real^N. l IN closure_fan(s) <=> ?x. (!n. x(n) IN s) /\ (x --> l) sequentially_fan`, REWRITE_TAC[closure_fan; IN_UNION; LIMPT_SEQUENTIAL_FAN; IN_ELIM_THM; IN_DELETE] THEN REPEAT GEN_TAC THEN MATCH_MP_TAC(TAUT `((b ==> c) /\ (~a /\ c ==> b)) /\ (a ==> c) ==> (a \/ b <=> c)`) THEN CONJ_TAC THENL [MESON_TAC[]; ALL_TAC] THEN DISCH_TAC THEN EXISTS_TAC `\n:num. l:real^N` THEN ASM_REWRITE_TAC[LIM_CONST_FAN]);; let CLOSED_SEQUENTIAL_LIMITS_FAN = prove (`!s. closed_fan s <=> !x l. (!n. x(n) IN s) /\ (x --> l) sequentially_fan ==> l IN s`, MESON_TAC[CLOSURE_SEQUENTIAL_FAN; CLOSURE_CLOSED_FAN; CLOSED_LIMPT_FAN; LIMPT_SEQUENTIAL_FAN; IN_DELETE]);; let CLOSURE_APPROACHABLE_FAN = prove (`!x s. x IN closure_fan(s) <=> !e. &0 < e ==> ?y. y IN s /\ dist(y,x) < e`, REWRITE_TAC[closure_fan; LIMPT_APPROACHABLE_FAN; IN_UNION; IN_ELIM_THM] THEN MESON_TAC[DIST_REFL]);; let CLOSED_APPROACHABLE_FAN = prove (`!x s. closed_fan s ==> ((!e. &0 < e ==> ?y. y IN s /\ dist(y,x) < e) <=> x IN s)`, MESON_TAC[CLOSURE_CLOSED_FAN; CLOSURE_APPROACHABLE_FAN]);; (* ------------------------------------------------------------------------- *) (* Closed balls. *) (* ------------------------------------------------------------------------- *) let cball_fan = new_definition `cball_fan(x,e) = { y | dist(x,y) <= e}`;; let IN_CBALL_FAN = prove (`!x y e. y IN cball_fan(x,e) <=> dist(x,y) <= e`, REWRITE_TAC[cball_fan; IN_ELIM_THM]);; let CLOSED_CBALL_FAN = prove (`!x:real^N e. closed_fan(cball_fan(x,e))`, REWRITE_TAC[CLOSED_SEQUENTIAL_LIMITS_FAN; IN_CBALL_FAN; dist] THEN GEN_TAC THEN GEN_TAC THEN X_GEN_TAC `s:num->real^N` THEN X_GEN_TAC `y:real^N` THEN STRIP_TAC THEN MATCH_MP_TAC(ISPEC `\n. x - (s:num->real^N) n` LIM_NORM_BOUND_FAN) THEN EXISTS_TAC `sequentially_fan` THEN REWRITE_TAC[TRIVIAL_LIMIT_SEQUENTIALLY_FAN] THEN ASM_SIMP_TAC[LIM_SUB_FAN; LIM_CONST_FAN; SEQUENTIALLY_FAN] THEN MESON_TAC[GE_REFL]);; let CENTRE_IN_CBALL_FAN = prove (`!x e. x IN cball_fan(x,e) <=> &0 <= e`, MESON_TAC[IN_CBALL_FAN; DIST_REFL]);; let BALL_SUBSET_CBALL_FAN = prove (`!x e. ball_fan(x,e) SUBSET cball_fan(x,e)`, REWRITE_TAC[IN_BALL_FAN; IN_CBALL_FAN; SUBSET] THEN REAL_ARITH_TAC);; let OPEN_CONTAINS_CBALL_FAN = prove (`!s. open_fan s <=> !x. x IN s ==> ?e. &0 < e /\ cball_fan(x,e) SUBSET s`, GEN_TAC THEN REWRITE_TAC[OPEN_CONTAINS_BALL_FAN] THEN EQ_TAC THENL [ALL_TAC; ASM_MESON_TAC[SUBSET_TRANS; BALL_SUBSET_CBALL_FAN]] THEN MATCH_MP_TAC MONO_FORALL THEN GEN_TAC THEN MATCH_MP_TAC MONO_IMP THEN REWRITE_TAC[SUBSET; IN_BALL_FAN; IN_CBALL_FAN] THEN DISCH_THEN(X_CHOOSE_THEN `e:real` STRIP_ASSUME_TAC) THEN EXISTS_TAC `e / &2` THEN ASM_REWRITE_TAC[REAL_HALF] THEN SUBGOAL_THEN `e / &2 < e` (fun th -> ASM_MESON_TAC[th; REAL_LET_TRANS]) THEN ASM_SIMP_TAC[REAL_LT_LDIV_EQ; REAL_OF_NUM_LT; ARITH] THEN UNDISCH_TAC `&0 < e` THEN REAL_ARITH_TAC);; let IN_INTERIOR_CBALL_FAN = prove (`!x s. x IN interior_fan s <=> ?e. &0 < e /\ cball_fan(x,e) SUBSET s`, REWRITE_TAC[interior_fan; IN_ELIM_THM] THEN MESON_TAC[OPEN_CONTAINS_CBALL_FAN; SUBSET_TRANS; BALL_SUBSET_CBALL_FAN; CENTRE_IN_BALL; OPEN_BALL_FAN]);; let LIMPT_BALL_FAN = prove (`!x:real^N y e. y limit_point_of_fan ball_fan(x,e) <=> &0 < e /\ y IN cball_fan(x,e)`, REPEAT GEN_TAC THEN ASM_CASES_TAC `&0 < e` THENL [ALL_TAC; ASM_MESON_TAC[LIMPT_EMPTY_FAN; REAL_NOT_LT; BALL_EQ_EMPTY_FAN]] THEN ASM_REWRITE_TAC[] THEN EQ_TAC THENL [MESON_TAC[CLOSED_CBALL_FAN; CLOSED_LIMPT_FAN; LIMPT_SUBSET_FAN; BALL_SUBSET_CBALL_FAN]; REWRITE_TAC[IN_CBALL_FAN; LIMPT_APPROACHABLE_FAN; IN_BALL_FAN]] THEN DISCH_TAC THEN X_GEN_TAC `d:real` THEN DISCH_TAC THEN ASM_CASES_TAC `y:real^N = x` THEN ASM_REWRITE_TAC[DIST_NZ] THENL [MP_TAC(SPECL [`d:real`; `e:real`] REAL_DOWN2) THEN ASM_REWRITE_TAC[] THEN GEN_MESON_TAC 0 40 1 [VECTOR_CHOOSE_DIST; DIST_SYM; REAL_LT_IMP_LE]; ALL_TAC] THEN MP_TAC(SPECL [`norm(y:real^N - x)`; `d:real`] REAL_DOWN2) THEN RULE_ASSUM_TAC(REWRITE_RULE[DIST_NZ; dist]) THEN ASM_REWRITE_TAC[] THEN DISCH_THEN(X_CHOOSE_THEN `k:real` STRIP_ASSUME_TAC) THEN EXISTS_TAC `(y:real^N) - (k / dist(y,x)) % (y - x)` THEN REWRITE_TAC[dist; VECTOR_ARITH `(y - c % z) - y = --c % z`] THEN REWRITE_TAC[NORM_MUL; REAL_ABS_DIV; REAL_ABS_NORM; REAL_ABS_NEG] THEN ASM_SIMP_TAC[REAL_DIV_RMUL; REAL_LT_IMP_NZ] THEN REWRITE_TAC[VECTOR_ARITH `x - (y - k % (y - x)) = (&1 - k) % (x - y)`] THEN ASM_SIMP_TAC[REAL_ARITH `&0 < k ==> &0 < abs k`; NORM_MUL] THEN ASM_SIMP_TAC[REAL_ARITH `&0 < k /\ k < d ==> abs k < d`] THEN MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC `norm(x:real^N - y)` THEN ASM_REWRITE_TAC[] THEN GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_LID] THEN MATCH_MP_TAC REAL_LT_RMUL THEN CONJ_TAC THENL [ALL_TAC; ASM_MESON_TAC[NORM_SUB]] THEN MATCH_MP_TAC(REAL_ARITH `&0 < k /\ k < &1 ==> abs(&1 - k) < &1`) THEN ASM_SIMP_TAC[REAL_LT_LDIV_EQ; REAL_LT_RDIV_EQ; REAL_MUL_LZERO; REAL_MUL_LID]);; let CLOSURE_BALL_FAN = prove (`!x:real^N e. &0 < e ==> (closure_fan(ball_fan(x,e)) = cball_fan(x,e))`, SIMP_TAC[EXTENSION; closure_fan; IN_ELIM_THM; IN_UNION; LIMPT_BALL_FAN] THEN REWRITE_TAC[IN_BALL_FAN; IN_CBALL_FAN] THEN REAL_ARITH_TAC);; let INTERIOR_CBALL_FAN = prove (`!x:real^N e. &0 <= e ==> (interior_fan(cball_fan(x,e)) = ball_fan(x,e))`, REPEAT STRIP_TAC THEN MATCH_MP_TAC INTERIOR_UNIQUE_FAN THEN REWRITE_TAC[BALL_SUBSET_CBALL_FAN; OPEN_BALL_FAN] THEN X_GEN_TAC `t:real^N->bool` THEN SIMP_TAC[SUBSET; IN_CBALL_FAN; IN_BALL_FAN; REAL_LT_LE] THEN STRIP_TAC THEN X_GEN_TAC `z:real^N` THEN DISCH_TAC THEN DISCH_THEN(SUBST_ALL_TAC o SYM) THEN FIRST_X_ASSUM(MP_TAC o SPEC `z:real^N` o GEN_REWRITE_RULE I [open_def_fan]) THEN ASM_REWRITE_TAC[] THEN DISCH_THEN(X_CHOOSE_THEN `d:real` MP_TAC) THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN ASM_CASES_TAC `z:real^N = x` THENL [FIRST_X_ASSUM SUBST_ALL_TAC THEN FIRST_X_ASSUM(X_CHOOSE_TAC `k:real` o MATCH_MP REAL_DOWN) THEN SUBGOAL_THEN `?w:real^N. dist(w,x) = k` STRIP_ASSUME_TAC THENL [ASM_MESON_TAC[VECTOR_CHOOSE_DIST; DIST_SYM; REAL_LT_IMP_LE]; ASM_MESON_TAC[REAL_NOT_LE; DIST_REFL; DIST_SYM]]; RULE_ASSUM_TAC(REWRITE_RULE[DIST_NZ]) THEN DISCH_THEN(MP_TAC o SPEC `z + ((d / &2) / dist(z,x)) % (z - x:real^N)`) THEN REWRITE_TAC[dist; VECTOR_ADD_SUB; NORM_MUL; REAL_ABS_DIV; REAL_ABS_NORM; REAL_ABS_NUM] THEN ASM_SIMP_TAC[REAL_DIV_RMUL; GSYM dist; REAL_LT_IMP_NZ] THEN ASM_SIMP_TAC[REAL_LT_LDIV_EQ; REAL_OF_NUM_LT; ARITH] THEN ASM_REWRITE_TAC[REAL_ARITH `abs d < d * &2 <=> &0 < d`] THEN DISCH_THEN(ANTE_RES_THEN MP_TAC) THEN REWRITE_TAC[dist] THEN REWRITE_TAC[VECTOR_ARITH `x - (z + k % (z - x)) = (&1 + k) % (x - z)`] THEN REWRITE_TAC[REAL_NOT_LE; NORM_MUL] THEN GEN_REWRITE_TAC LAND_CONV [GSYM REAL_MUL_LID] THEN ONCE_REWRITE_TAC[NORM_SUB] THEN ASM_SIMP_TAC[REAL_LT_RMUL_EQ; GSYM dist] THEN MATCH_MP_TAC(REAL_ARITH `&0 < x ==> &1 < abs(&1 + x)`) THEN ONCE_REWRITE_TAC[DIST_SYM] THEN ASM_SIMP_TAC[REAL_LT_DIV; REAL_OF_NUM_LT; ARITH]]);; let FRONTIER_BALL_FAN = prove (`!a e. &0 < e ==> (frontier_fan(ball_fan(a,e)) = {x | dist(a,x) = e})`, SIMP_TAC[frontier_fan; CLOSURE_BALL_FAN; INTERIOR_OPEN_FAN; OPEN_BALL_FAN; REAL_LT_IMP_LE] THEN REWRITE_TAC[EXTENSION; IN_DIFF; IN_ELIM_THM; IN_BALL_FAN; IN_CBALL_FAN] THEN REAL_ARITH_TAC);; let FRONTIER_CBALL_FAN = prove (`!a e. &0 < e ==> (frontier_fan(cball_fan(a,e)) = {x | dist(a,x) = e})`, SIMP_TAC[frontier_fan; INTERIOR_CBALL_FAN; CLOSED_CBALL_FAN; CLOSURE_CLOSED_FAN; REAL_LT_IMP_LE] THEN REWRITE_TAC[EXTENSION; IN_DIFF; IN_ELIM_THM; IN_BALL_FAN; IN_CBALL_FAN] THEN REAL_ARITH_TAC);; let SUBSET_BALL_FAN = prove (`!x d e. d <= e ==> ball_fan(x,d) SUBSET ball_fan(x,e)`, REWRITE_TAC[SUBSET; IN_BALL_FAN] THEN MESON_TAC[REAL_LTE_TRANS]);; let SUBSET_CBALL_FAN = prove (`!x d e. d <= e ==> cball_fan(x,d) SUBSET cball_fan(x,e)`, REWRITE_TAC[SUBSET; IN_CBALL_FAN] THEN MESON_TAC[REAL_LE_TRANS]);; (* ------------------------------------------------------------------------- *) (* Boundedness. *) (* ------------------------------------------------------------------------- *) let bounded_fan = new_definition `bounded_fan s <=> ?a. !x:real^N. x IN s ==> norm(x) <= a`;; let BOUNDED_EMPTY_FAN = prove (`bounded_fan {}`, REWRITE_TAC[bounded_fan; NOT_IN_EMPTY]);; let BOUNDED_SUBSET_FAN = prove (`!s t. bounded_fan t /\ s SUBSET t ==> bounded_fan s`, MESON_TAC[bounded_fan; SUBSET]);; let BOUNDED_CLOSURE_FAN = prove (`!s:real^N->bool. bounded_fan s ==> bounded_fan(closure_fan s)`, REWRITE_TAC[bounded_fan; CLOSURE_SEQUENTIAL_FAN] THEN MESON_TAC[LIM_NORM_BOUND_FAN; TRIVIAL_LIMIT_SEQUENTIALLY_FAN; trivial_limit_fan]);; let BOUNDED_CBALL_FAN = prove (`!x:real^N e. bounded_fan(cball_fan(x,e))`, REPEAT GEN_TAC THEN REWRITE_TAC[bounded_fan] THEN EXISTS_TAC `norm(x:real^N) + e` THEN REWRITE_TAC[IN_CBALL_FAN; dist] THEN MESON_TAC[NORM_SUB; NORM_TRIANGLE_SUB; REAL_ARITH `b <= c + a ==> a <= e ==> b <= c + e`]);; let BOUNDED_BALL_FAN = prove (`!x e. bounded_fan(ball_fan(x,e))`, MESON_TAC[BALL_SUBSET_CBALL_FAN; BOUNDED_CBALL_FAN; BOUNDED_SUBSET_FAN]);; let FINITE_IMP_BOUNDED_FAN = prove (`!s:real^N->bool. FINITE s ==> bounded_fan s`, MATCH_MP_TAC FINITE_INDUCT_STRONG THEN REWRITE_TAC[BOUNDED_EMPTY_FAN] THEN REWRITE_TAC[bounded_fan; IN_INSERT] THEN X_GEN_TAC `x:real^N` THEN GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_TAC `B:real`) STRIP_ASSUME_TAC) THEN EXISTS_TAC `norm(x:real^N) + abs B` THEN REPEAT STRIP_TAC THEN ASM_MESON_TAC[NORM_POS_LE; REAL_ARITH `(y <= b /\ &0 <= x ==> y <= x + abs b) /\ x <= x + abs b`]);; let BOUNDED_UNION_FAN = prove (`!s t. bounded_fan (s UNION t) <=> bounded_fan s /\ bounded_fan t`, REWRITE_TAC[bounded_fan; IN_UNION] THEN MESON_TAC[REAL_LE_MAX]);; let BOUNDED_POS_FAN = prove (`!s. bounded_fan s <=> ?b. &0 < b /\ !x. x IN s ==> norm(x) <= b`, REWRITE_TAC[bounded_fan] THEN MESON_TAC[REAL_ARITH `&0 < &1 + abs(y) /\ (x <= y ==> x <= &1 + abs(y))`]);; let BOUNDED_INTER_FAN = prove (`!s t. bounded_fan s \/ bounded_fan t ==> bounded_fan (s INTER t)`, MESON_TAC[BOUNDED_SUBSET_FAN; INTER_SUBSET]);; (* ------------------------------------------------------------------------- *) (* Compactness (the definition is the one based on convegent subsequences). *) (* ------------------------------------------------------------------------- *) let compact_fan = new_definition `compact_fan s <=> !f:num->real^N. (!n. f(n) IN s) ==> ?l r. l IN s /\ (!m n:num. m < n ==> r(m) < r(n)) /\ ((f o r) --> l) sequentially_fan`;; let MONOTONE_BIGGER_FAN = 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 LIM_SUBSEQUENCE_FAN = prove (`!s r. (!m n. m < n ==> r(m) < r(n)) /\ (s --> l) sequentially_fan ==> (s o r --> l) sequentially_fan`, REWRITE_TAC[LIM_SEQUENTIALLY_FAN; o_THM] THEN MESON_TAC[MONOTONE_BIGGER_FAN; LE_TRANS]);; let MONOTONE_SUBSEQUENCE_FAN = 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_FAN = 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_FAN = 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`, REPEAT STRIP_TAC THENL [ASM_MESON_TAC[CONVERGENT_BOUNDED_INCREASING_FAN]; ALL_TAC] THEN MP_TAC(SPEC `\n. --((s:num->real) n)` CONVERGENT_BOUNDED_INCREASING_FAN) THEN ASM_REWRITE_TAC[REAL_LE_NEG2; REAL_ABS_NEG] THEN ASM_MESON_TAC[REAL_ARITH `abs(x - --l) = abs(--x - l)`]);; let COMPACT_REAL_LEMMA_FAN = 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`, REPEAT GEN_TAC THEN DISCH_TAC THEN ONCE_REWRITE_TAC[SWAP_EXISTS_THM] THEN MP_TAC(SPEC `s:num->real` MONOTONE_SUBSEQUENCE_FAN) THEN MATCH_MP_TAC MONO_EXISTS THEN GEN_TAC THEN DISCH_TAC THEN ASM_SIMP_TAC[] THEN MATCH_MP_TAC CONVERGENT_BOUNDED_MONOTONE_FAN THEN ASM_MESON_TAC[]);; let COMPACT_LEMMA_FAN = prove (`!s. bounded_fan 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_fan] 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_FAN) 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_FAN; 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 BOUNDED_CLOSED_IMP_COMPACT_FAN = prove (`!s:real^N->bool. bounded_fan s /\ closed_fan s ==> compact_fan s`, REPEAT STRIP_TAC THEN REWRITE_TAC[compact_fan] THEN X_GEN_TAC `x:num->real^N` THEN DISCH_TAC THEN MP_TAC(ISPEC `s:real^N->bool` COMPACT_LEMMA_FAN) THEN ASM_REWRITE_TAC[] THEN DISCH_THEN(MP_TAC o SPEC `dimindex(:N)`) THEN REWRITE_TAC[LE_REFL] THEN MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `l:real^N` THEN MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `r:num->num` THEN ASM_SIMP_TAC[] THEN STRIP_TAC THEN MATCH_MP_TAC(TAUT `(b ==> a) /\ b ==> a /\ b`) THEN REPEAT STRIP_TAC THENL [FIRST_ASSUM(MATCH_MP_TAC o REWRITE_RULE[CLOSED_SEQUENTIAL_LIMITS_FAN]) THEN EXISTS_TAC `(x:num->real^N) o (r:num->num)` THEN ASM_REWRITE_TAC[o_THM]; ALL_TAC] THEN REWRITE_TAC[LIM_SEQUENTIALLY_FAN] THEN X_GEN_TAC `e:real` THEN DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC `e / &2 / &(dimindex(:N))`) THEN ASM_SIMP_TAC[REAL_LT_DIV; REAL_OF_NUM_LT; DIMINDEX_NONZERO; REAL_HALF; ARITH_RULE `0 < n <=> ~(n = 0)`] THEN MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `N:num` THEN REWRITE_TAC[dist] THEN REPEAT STRIP_TAC THEN MATCH_MP_TAC(MATCH_MP (REAL_ARITH `a <= b ==> b < e ==> a < e`) (SPEC_ALL NORM_LE_L1)) THEN MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC `sum (1..dimindex(:N)) (\k. e / &2 / &(dimindex(:N)))` THEN CONJ_TAC THENL [MATCH_MP_TAC SUM_LE_NUMSEG THEN SIMP_TAC[o_THM; LAMBDA_BETA; vector_sub] THEN ASM_MESON_TAC[REAL_LT_IMP_LE; LE_TRANS]; ASM_SIMP_TAC[SUM_CONST_NUMSEG; ADD_SUB; REAL_DIV_LMUL; REAL_OF_NUM_EQ; DIMINDEX_NONZERO; REAL_LE_REFL; REAL_LT_LDIV_EQ; ARITH; REAL_OF_NUM_LT; REAL_ARITH `x < x * &2 <=> &0 < x`]]);; (* ------------------------------------------------------------------------- *) (* Completeness. *) (* ------------------------------------------------------------------------- *) let cauchy_fan = new_definition `cauchy_fan (s:num->real^N) <=> !e. &0 < e ==> ?N. !m n. m >= N /\ n >= N ==> dist(s m,s n) < e`;; let complete_fan = new_definition `complete_fan s <=> !f:num->real^N. (!n. f n IN s) /\ cauchy_fan f ==> ?l. l IN s /\ (f --> l) sequentially_fan`;; let CAUCHY_FAN = prove (`!s:num->real^N. cauchy_fan s <=> !e. &0 < e ==> ?N. !n. n >= N ==> dist(s n,s N) < e`, REPEAT GEN_TAC THEN REWRITE_TAC[cauchy_fan; 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 CONVERGENT_IMP_CAUCHY_FAN = prove (`!s l. (s --> l) sequentially_fan ==> cauchy_fan s`, REWRITE_TAC[LIM_SEQUENTIALLY_FAN; cauchy_fan] THEN REPEAT GEN_TAC THEN DISCH_TAC THEN X_GEN_TAC `e:real` THEN DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC `e / &2`) THEN ASM_SIMP_TAC[REAL_LT_DIV; REAL_OF_NUM_LT; ARITH] THEN ASM_MESON_TAC[GE; LE_REFL; DIST_TRIANGLE_HALF_L]);; let CAUCHY_IMP_BOUNDED_FAN = prove (`!s:num->real^N. cauchy_fan s ==> bounded_fan {y | ?n. y = s n}`, REWRITE_TAC[cauchy_fan; bounded_fan; IN_ELIM_THM] THEN GEN_TAC THEN DISCH_THEN(MP_TAC o SPEC `&1`) THEN REWRITE_TAC[REAL_LT_01] THEN DISCH_THEN(X_CHOOSE_THEN `N:num` (MP_TAC o SPEC `N:num`)) THEN REWRITE_TAC[GE_REFL] THEN DISCH_TAC THEN SUBGOAL_THEN `!n:num. N <= n ==> norm(s n :real^N) <= norm(s N) + &1` ASSUME_TAC THENL [ASM_MESON_TAC[GE; dist; DIST_SYM; NORM_TRIANGLE_SUB; REAL_ARITH `a <= b + c /\ c < &1 ==> a <= b + &1`]; MP_TAC(ISPECL [`\n:num. norm(s n :real^N)`; `0..N`] UPPER_BOUND_FINITE_SET_REAL) THEN SIMP_TAC[FINITE_NUMSEG; IN_NUMSEG; LE_0; LEFT_IMP_EXISTS_THM] THEN ASM_MESON_TAC[LE_CASES; REAL_ARITH `x <= a \/ x <= b ==> x <= abs a + abs b`]]);; let COMPACT_IMP_COMPLETE_FAN = prove (`!s:real^N->bool. compact_fan s ==> complete_fan s`, GEN_TAC THEN REWRITE_TAC[complete_fan; compact_fan] THEN MATCH_MP_TAC MONO_FORALL THEN X_GEN_TAC `f:num->real^N` THEN DISCH_THEN(fun th -> STRIP_TAC THEN MP_TAC th)THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC MONO_EXISTS THEN GEN_TAC THEN DISCH_THEN(X_CHOOSE_THEN `r:num->num` STRIP_ASSUME_TAC) THEN FIRST_X_ASSUM(MP_TAC o MATCH_MP (REWRITE_RULE[IMP_CONJ] LIM_ADD_FAN)) THEN DISCH_THEN(MP_TAC o SPEC `\n. (f:num->real^N)(n) - f(r n)`) THEN DISCH_THEN(MP_TAC o SPEC `vec 0: real^N`) THEN ASM_REWRITE_TAC[o_THM] THEN REWRITE_TAC[VECTOR_ADD_RID; VECTOR_SUB_ADD2; ETA_AX] THEN DISCH_THEN MATCH_MP_TAC THEN FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [cauchy_fan]) THEN REWRITE_TAC[GE; lim_fan; SEQUENTIALLY_FAN; dist; VECTOR_SUB_RZERO] THEN SUBGOAL_THEN `!n:num. n <= r(n)` MP_TAC THENL [INDUCT_TAC; ALL_TAC] THEN ASM_MESON_TAC[ LE_TRANS; LE_REFL; LT; LET_TRANS; LE_0; LE_SUC_LT]);; let COMPLETE_UNIV_FAN = prove (`complete_fan(:real^N)`, REWRITE_TAC[complete_fan; IN_UNIV] THEN X_GEN_TAC `x:num->real^N` THEN DISCH_TAC THEN FIRST_ASSUM(MP_TAC o MATCH_MP CAUCHY_IMP_BOUNDED_FAN) THEN DISCH_THEN(ASSUME_TAC o MATCH_MP BOUNDED_CLOSURE_FAN) THEN MP_TAC(ISPEC `closure_fan {y:real^N | ?n:num. y = x n}` COMPACT_IMP_COMPLETE_FAN) THEN ASM_SIMP_TAC[BOUNDED_CLOSED_IMP_COMPACT_FAN; CLOSED_CLOSURE_FAN; complete_fan] THEN DISCH_THEN(MP_TAC o SPEC `x:num->real^N`) THEN ANTS_TAC THENL [ALL_TAC; MESON_TAC[]] THEN ASM_REWRITE_TAC[closure_fan; IN_ELIM_THM; IN_UNION] THEN MESON_TAC[]);; let COMPLETE_EQ_CLOSED_FAN = prove (`!s:real^N->bool. complete_fan s <=> closed_fan s`, GEN_TAC THEN EQ_TAC THENL [REWRITE_TAC[complete_fan; CLOSED_LIMPT_FAN; LIMPT_SEQUENTIAL_FAN] THEN REWRITE_TAC[RIGHT_IMP_FORALL_THM] THEN GEN_TAC THEN REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN MATCH_MP_TAC MONO_FORALL THEN MESON_TAC[CONVERGENT_IMP_CAUCHY_FAN; IN_DELETE; LIM_UNIQUE_FAN; TRIVIAL_LIMIT_SEQUENTIALLY_FAN]; REWRITE_TAC[complete_fan; CLOSED_SEQUENTIAL_LIMITS_FAN] THEN DISCH_TAC THEN X_GEN_TAC `f:num->real^N` THEN STRIP_TAC THEN MP_TAC(REWRITE_RULE[complete_fan] COMPLETE_UNIV_FAN) THEN DISCH_THEN(MP_TAC o SPEC `f:num->real^N`) THEN ASM_REWRITE_TAC[IN_UNIV] THEN ASM_MESON_TAC[]]);; let CONVERGENT_EQ_CAUCHY_FAN = prove (`!s. (?l. (s --> l) sequentially_fan) <=> cauchy_fan s`, GEN_TAC THEN EQ_TAC THENL [REWRITE_TAC[LEFT_IMP_EXISTS_THM; CONVERGENT_IMP_CAUCHY_FAN]; REWRITE_TAC[REWRITE_RULE[complete_fan; IN_UNIV] COMPLETE_UNIV_FAN]]);; (* ------------------------------------------------------------------------- *) (* Total boundedness. *) (* ------------------------------------------------------------------------- *) let COMPACT_IMP_TOTALLY_BOUNDED_FAN = prove (`!s:real^N->bool. compact_fan s ==> !e. &0 < e ==> ?k. FINITE k /\ k SUBSET s /\ s SUBSET (UNIONS(IMAGE (\x. ball_fan(x,e)) k))`, GEN_TAC THEN ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN REWRITE_TAC[NOT_FORALL_THM; NOT_IMP; NOT_EXISTS_THM] THEN REWRITE_TAC[TAUT `~(a /\ b /\ c) <=> a /\ b ==> ~c`; SUBSET] THEN DISCH_THEN(X_CHOOSE_THEN `e:real` STRIP_ASSUME_TAC) THEN SUBGOAL_THEN `?x:num->real^N. !n. x(n) IN s /\ !m. m < n ==> ~(dist(x(m),x(n)) < e)` MP_TAC THENL [SUBGOAL_THEN `?x:num->real^N. !n. x(n) = @y. y IN s /\ !m. m < n ==> ~(dist(x(m),y) < e)` MP_TAC THENL [MATCH_MP_TAC(MATCH_MP WF_REC WF_num) THEN SIMP_TAC[]; ALL_TAC] THEN MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `x:num->real^N` THEN DISCH_TAC THEN MATCH_MP_TAC num_WF THEN X_GEN_TAC `n:num` THEN FIRST_X_ASSUM(SUBST1_TAC o SPEC `n:num`) THEN STRIP_TAC THEN CONV_TAC SELECT_CONV THEN FIRST_X_ASSUM(MP_TAC o SPEC `IMAGE (x:num->real^N) {m | m < n}`) THEN SIMP_TAC[FINITE_IMAGE; FINITE_NUMSEG_LT; NOT_FORALL_THM; NOT_IMP] THEN REWRITE_TAC[IN_UNIONS; IN_IMAGE; IN_ELIM_THM] THEN ASM_MESON_TAC[IN_BALL_FAN]; ALL_TAC] THEN REWRITE_TAC[compact_fan; NOT_FORALL_THM] THEN MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `x:num->real^N` THEN REWRITE_TAC[NOT_IMP; FORALL_AND_THM] THEN STRIP_TAC THEN ASM_REWRITE_TAC[NOT_EXISTS_THM] THEN REPEAT STRIP_TAC THEN FIRST_X_ASSUM(MP_TAC o MATCH_MP CONVERGENT_IMP_CAUCHY_FAN) THEN REWRITE_TAC[cauchy_fan] THEN DISCH_THEN(MP_TAC o SPEC `e:real`) THEN ASM_REWRITE_TAC[o_THM; NOT_EXISTS_THM; NOT_IMP; NOT_FORALL_THM; NOT_IMP] THEN X_GEN_TAC `N:num` THEN MAP_EVERY EXISTS_TAC [`N:num`; `SUC N`] THEN CONJ_TAC THENL [ARITH_TAC; ASM_MESON_TAC[LT]]);; (* ------------------------------------------------------------------------- *) (* Heine-Borel theorem (following Burkill & Burkill vol. 2) *) (* ------------------------------------------------------------------------- *) let HEINE_BOREL_LEMMA_FAN = prove (`!s:real^N->bool. compact_fan s ==> !t. s SUBSET (UNIONS t) /\ (!b. b IN t ==> open_fan b) ==> ?e. &0 < e /\ !x. x IN s ==> ?b. b IN t /\ ball_fan(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_fan] 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_fan]; ALL_TAC] THEN FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [LIM_SEQUENTIALLY_FAN]) 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_FAN]) 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_FAN; LT_IMP_LE; LE_TRANS]);; let COMPACT_IMP_HEINE_BOREL_FAN = prove (`!s. compact_fan (s:real^N->bool) ==> !f. (!t. t IN f ==> open_fan t) /\ s SUBSET (UNIONS f) ==> ?f'. f' SUBSET f /\ FINITE f' /\ s SUBSET (UNIONS f')`, REPEAT STRIP_TAC THEN FIRST_ASSUM(MP_TAC o SPEC `f:(real^N->bool)->bool` o MATCH_MP HEINE_BOREL_LEMMA_FAN) THEN ASM_REWRITE_TAC[] THEN DISCH_THEN(X_CHOOSE_THEN `e:real` (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [RIGHT_IMP_EXISTS_THM] THEN REWRITE_TAC[SKOLEM_THM; SUBSET; IN_BALL_FAN] THEN DISCH_THEN(X_CHOOSE_TAC `B:real^N->real^N->bool`) THEN FIRST_ASSUM(MP_TAC o SPEC `e:real` o MATCH_MP COMPACT_IMP_TOTALLY_BOUNDED_FAN) THEN ASM_REWRITE_TAC[SUBSET; IN_UNIONS; IN_IMAGE; IN_BALL_FAN] THEN REWRITE_TAC[LEFT_AND_EXISTS_THM] THEN ONCE_REWRITE_TAC[SWAP_EXISTS_THM] THEN REWRITE_TAC[GSYM CONJ_ASSOC; UNWIND_THM2] THEN DISCH_THEN(X_CHOOSE_THEN `k:real^N->bool` STRIP_ASSUME_TAC) THEN EXISTS_TAC `IMAGE (B:real^N->real^N->bool) k` THEN ASM_SIMP_TAC[FINITE_IMAGE; SUBSET; IN_IMAGE; LEFT_IMP_EXISTS_THM] THEN ASM_MESON_TAC[IN_BALL_FAN]);; (* ------------------------------------------------------------------------- *) (* Bolzano-Weierstrass property. *) (* ------------------------------------------------------------------------- *) let HEINE_BOREL_IMP_BOLZANO_WEIERSTRASS_FAN = prove (`!s:real^N->bool. (!f. (!t. t IN f ==> open_fan t) /\ s SUBSET (UNIONS f) ==> ?f'. f' SUBSET f /\ FINITE f' /\ s SUBSET (UNIONS f')) ==> !t. INFINITE t /\ t SUBSET s ==> ?x. x IN s /\ x limit_point_of_fan t`, REWRITE_TAC[RIGHT_IMP_FORALL_THM; limit_point_of_fan] THEN REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[TAUT `a ==> b /\ c ==> d <=> c ==> ~d ==> a ==> ~b`] THEN REWRITE_TAC[NOT_FORALL_THM; NOT_EXISTS_THM; RIGHT_AND_FORALL_THM] THEN DISCH_TAC THEN REWRITE_TAC[SKOLEM_THM] THEN DISCH_THEN(X_CHOOSE_TAC `f:real^N->real^N->bool`) THEN DISCH_THEN(MP_TAC o SPEC `{t:real^N->bool | ?x:real^N. x IN s /\ (t = f x)}`) THEN REWRITE_TAC[INFINITE; SUBSET; IN_ELIM_THM; IN_UNIONS; NOT_IMP] THEN ANTS_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN DISCH_THEN(X_CHOOSE_THEN `g:(real^N->bool)->bool` STRIP_ASSUME_TAC) THEN MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC `{x:real^N | x IN t /\ (f(x):real^N->bool) IN g}` THEN CONJ_TAC THENL [MATCH_MP_TAC FINITE_IMAGE_INJ_GENERAL THEN ASM_MESON_TAC[SUBSET]; SIMP_TAC[SUBSET; IN_ELIM_THM] THEN X_GEN_TAC `u:real^N` THEN DISCH_TAC THEN SUBGOAL_THEN `(u:real^N) IN s` ASSUME_TAC THEN ASM_MESON_TAC[SUBSET]]);; (* ------------------------------------------------------------------------- *) (* Complete the chain of compactness variants. *) (* ------------------------------------------------------------------------- *) let BOLZANO_WEIERSTRASS_IMP_BOUNDED_FAN = prove (`!s:real^N->bool. (!t. INFINITE t /\ t SUBSET s ==> ?x. x IN s /\ x limit_point_of_fan t) ==> bounded_fan s`, GEN_TAC THEN ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN SIMP_TAC[compact_fan; bounded_fan] THEN REWRITE_TAC[NOT_FORALL_THM; NOT_EXISTS_THM; SKOLEM_THM; NOT_IMP] THEN REWRITE_TAC[REAL_NOT_LE] THEN DISCH_THEN(X_CHOOSE_TAC `beyond:real->real^N`) THEN (MP_TAC o prove_recursive_functions_exist num_RECURSION) `(f(0) = beyond(&0)) /\ (!n. f(SUC n) = beyond(norm(f n) + &1):real^N)` THEN DISCH_THEN(X_CHOOSE_THEN `x:num->real^N` STRIP_ASSUME_TAC) THEN EXISTS_TAC `IMAGE (x:num->real^N) UNIV` THEN SUBGOAL_THEN `!m n. m < n ==> norm((x:num->real^N) m) + &1 < norm(x n)` ASSUME_TAC THENL [GEN_TAC THEN INDUCT_TAC THEN ASM_REWRITE_TAC[LT] THEN ASM_MESON_TAC[REAL_LT_TRANS; REAL_ARITH `b < b + &1`]; ALL_TAC] THEN SUBGOAL_THEN `!m n. ~(m = n) ==> &1 < dist((x:num->real^N) m,x n)` ASSUME_TAC THENL [REPEAT GEN_TAC THEN REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC (SPECL [`m:num`; `n:num`] LT_CASES) THEN ASM_MESON_TAC[dist; LT_CASES; NORM_TRIANGLE_SUB; NORM_SUB; REAL_ARITH `x + &1 < y /\ y <= x + d ==> &1 < d`]; ALL_TAC] THEN REPEAT CONJ_TAC THENL [ASM_MESON_TAC[INFINITE_IMAGE_INJ; num_INFINITE; DIST_REFL; REAL_ARITH `~(&1 < &0)`]; REWRITE_TAC[SUBSET; IN_IMAGE; IN_UNIV; LEFT_IMP_EXISTS_THM] THEN GEN_TAC THEN INDUCT_TAC THEN ASM_MESON_TAC[]; ALL_TAC] THEN X_GEN_TAC `l:real^N` THEN REWRITE_TAC[LIMPT_APPROACHABLE_FAN] THEN REWRITE_TAC[IN_IMAGE; IN_UNIV; LEFT_AND_EXISTS_THM] THEN ONCE_REWRITE_TAC[SWAP_EXISTS_THM] THEN REWRITE_TAC[UNWIND_THM2] THEN STRIP_TAC THEN FIRST_ASSUM(MP_TAC o SPEC `&1 / &2`) THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN DISCH_THEN(X_CHOOSE_THEN `k:num` STRIP_ASSUME_TAC) THEN FIRST_X_ASSUM(MP_TAC o SPEC `dist((x:num->real^N) k,l)`) THEN ASM_SIMP_TAC[DIST_POS_LT] THEN DISCH_THEN(X_CHOOSE_THEN `m:num` STRIP_ASSUME_TAC) THEN ASM_CASES_TAC `m:num = k` THEN ASM_MESON_TAC[DIST_TRIANGLE_HALF_L; REAL_LT_TRANS; REAL_LT_REFL]);; let SEQUENCE_INFINITE_LEMMA_FAN = prove (`!f l. (!n. ~(f(n) = l)) /\ (f --> l) sequentially_fan ==> INFINITE {y:real^N | ?n. y = f n}`, REWRITE_TAC[INFINITE] THEN REPEAT STRIP_TAC THEN MP_TAC(ISPEC `IMAGE (\y:real^N. dist(y,l)) {y | ?n:num. y = f n}` INF_FINITE) THEN ASM_SIMP_TAC[GSYM MEMBER_NOT_EMPTY; IN_IMAGE; FINITE_IMAGE; IN_ELIM_THM] THEN ASM_MESON_TAC[LIM_SEQUENTIALLY_FAN; LE_REFL; REAL_NOT_LE; DIST_POS_LT]);; let SEQUENCE_UNIQUE_LIMPT_FAN = prove (`!f l. (!n. ~(f(n) = l)) /\ (f --> l) sequentially_fan ==> !l'. l' limit_point_of_fan {y:real^N | ?n. y = f n} ==> (l' = l)`, REWRITE_TAC[LIMPT_APPROACHABLE_FAN; IN_ELIM_THM; LEFT_AND_EXISTS_THM] THEN ONCE_REWRITE_TAC[SWAP_EXISTS_THM] THEN REWRITE_TAC[UNWIND_THM2] THEN REPEAT STRIP_TAC THEN ABBREV_TAC `e = dist(l':real^N,l)` 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_FAN]) THEN DISCH_THEN(MP_TAC o SPEC `e / &2`) THEN ASM_REWRITE_TAC[REAL_HALF] THEN DISCH_THEN(X_CHOOSE_TAC `N:num`) THEN MP_TAC(ISPEC `(e / &2) INSERT (IMAGE (\n. if dist((f:num->real^N) n,l') = &0 then e / &2 else dist((f:num->real^N) n,l')) {n | n < N})` INF_FINITE) THEN ASM_SIMP_TAC[FINITE_RULES; FINITE_IMAGE; FINITE_NUMSEG_LT; NOT_EMPTY_INSERT] THEN ABBREV_TAC(mk_eq(`d:real`,mk_comb(`inf`, `(e / &2) INSERT (IMAGE (\n. if dist((f:num->real^N) n,l') = &0 then e / &2 else dist((f:num->real^N) n,l')) {n | n < N})` ))) THEN REWRITE_TAC[IN_INSERT; IN_IMAGE; IN_ELIM_THM] THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN SUBGOAL_THEN `&0 < d` ASSUME_TAC THENL [FIRST_X_ASSUM(DISJ_CASES_THEN STRIP_ASSUME_TAC) THEN ASM_REWRITE_TAC[] THEN REPEAT COND_CASES_TAC THEN ASM_MESON_TAC[REAL_HALF; REAL_LT_LE; DIST_POS_LE]; ALL_TAC] THEN FIRST_X_ASSUM(MP_TAC o SPEC `d:real`) THEN ASM_REWRITE_TAC[] THEN DISCH_THEN(X_CHOOSE_THEN `k:num` STRIP_ASSUME_TAC) THEN DISCH_THEN(fun th -> MP_TAC(SPEC `e / &2` th) THEN MP_TAC(SPEC `dist((f:num->real^N) k,l')` th)) THEN ASM_REWRITE_TAC[GSYM REAL_NOT_LT; DE_MORGAN_THM] THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN REWRITE_TAC[NOT_EXISTS_THM] THEN DISCH_THEN(MP_TAC o SPEC `k:num`) THEN ASM_REWRITE_TAC[DIST_EQ_0; NOT_LT; GSYM REAL_NOT_LE] THEN ASM_MESON_TAC[DIST_TRIANGLE_HALF_R; REAL_LT_REFL; REAL_LTE_TRANS]);; let BOLZANO_WEIERSTRASS_IMP_CLOSED_FAN = prove (`!s:real^N->bool. (!t. INFINITE t /\ t SUBSET s ==> ?x. x IN s /\ x limit_point_of_fan t) ==> closed_fan s`, REPEAT STRIP_TAC THEN REWRITE_TAC[CLOSED_SEQUENTIAL_LIMITS_FAN] THEN MAP_EVERY X_GEN_TAC [`f:num->real^N`; `l:real^N`] THEN DISCH_TAC THEN MAP_EVERY (MP_TAC o ISPECL [`f:num->real^N`; `l:real^N`]) [SEQUENCE_UNIQUE_LIMPT_FAN; SEQUENCE_INFINITE_LEMMA_FAN] THEN MATCH_MP_TAC(TAUT `(~d ==> a /\ ~(b /\ c)) ==> (a ==> b) ==> (a ==> c) ==> d`) THEN DISCH_TAC THEN CONJ_TAC THENL [ASM_MESON_TAC[]; STRIP_TAC] THEN FIRST_X_ASSUM(MP_TAC o SPEC `{y:real^N | ?n:num. y = f n}`) THEN ASM_REWRITE_TAC[NOT_IMP] THEN CONJ_TAC THENL [REWRITE_TAC[SUBSET; IN_ELIM_THM]; ABBREV_TAC `t = {y:real^N | ?n:num. y = f n}`] THEN ASM_MESON_TAC[]);; (* ------------------------------------------------------------------------- *) (* Hence express everything as an equivalence. *) (* ------------------------------------------------------------------------- *) let COMPACT_EQ_HEINE_BOREL_FAN = prove (`!s:real^N->bool. compact_fan s <=> !f. (!t. t IN f ==> open_fan t) /\ s SUBSET (UNIONS f) ==> ?f'. f' SUBSET f /\ FINITE f' /\ s SUBSET (UNIONS f')`, GEN_TAC THEN EQ_TAC THEN SIMP_TAC[COMPACT_IMP_HEINE_BOREL_FAN] THEN DISCH_THEN(MP_TAC o MATCH_MP HEINE_BOREL_IMP_BOLZANO_WEIERSTRASS_FAN) THEN DISCH_TAC THEN MATCH_MP_TAC BOUNDED_CLOSED_IMP_COMPACT_FAN THEN ASM_SIMP_TAC[BOLZANO_WEIERSTRASS_IMP_BOUNDED_FAN; BOLZANO_WEIERSTRASS_IMP_CLOSED_FAN]);; let COMPACT_EQ_BOLZANO_WEIERSTRASS_FAN = prove (`!s:real^N->bool. compact_fan s <=> !t. INFINITE t /\ t SUBSET s ==> ?x. x IN s /\ x limit_point_of_fan t`, GEN_TAC THEN EQ_TAC THENL [SIMP_TAC[COMPACT_EQ_HEINE_BOREL_FAN; HEINE_BOREL_IMP_BOLZANO_WEIERSTRASS_FAN]; SIMP_TAC[BOLZANO_WEIERSTRASS_IMP_BOUNDED_FAN; BOLZANO_WEIERSTRASS_IMP_CLOSED_FAN; BOUNDED_CLOSED_IMP_COMPACT_FAN]]);; let COMPACT_EQ_BOUNDED_CLOSED_FAN = prove (`!s:real^N->bool. compact_fan s <=> bounded_fan s /\ closed_fan s`, GEN_TAC THEN EQ_TAC THEN REWRITE_TAC[BOUNDED_CLOSED_IMP_COMPACT_FAN] THEN SIMP_TAC[COMPACT_EQ_BOLZANO_WEIERSTRASS_FAN; BOLZANO_WEIERSTRASS_IMP_BOUNDED_FAN; BOLZANO_WEIERSTRASS_IMP_CLOSED_FAN]);; let COMPACT_IMP_BOUNDED_FAN = prove (`!s. compact_fan s ==> bounded_fan s`, SIMP_TAC[COMPACT_EQ_BOUNDED_CLOSED_FAN]);; let COMPACT_IMP_CLOSED_FAN = prove (`!s. compact_fan s ==> closed_fan s`, SIMP_TAC[COMPACT_EQ_BOUNDED_CLOSED_FAN]);; (* ------------------------------------------------------------------------- *) (* In particular, some common special cases. *) (* ------------------------------------------------------------------------- *) let COMPACT_EMPTY_FAN = prove (`compact_fan {}`, REWRITE_TAC[compact_fan; NOT_IN_EMPTY]);; let COMPACT_UNION_FAN = prove (`!s t. compact_fan s /\ compact_fan t ==> compact_fan (s UNION t)`, SIMP_TAC[COMPACT_EQ_BOUNDED_CLOSED_FAN; BOUNDED_UNION_FAN; CLOSED_UNION_FAN]);; let COMPACT_INTER_FAN = prove (`!s t. compact_fan s /\ compact_fan t ==> compact_fan (s INTER t)`, SIMP_TAC[COMPACT_EQ_BOUNDED_CLOSED_FAN; BOUNDED_INTER_FAN; CLOSED_INTER_FAN]);; let COMPACT_INTER_CLOSED_FAN = prove (`!s t. compact_fan s /\ closed_fan t ==> compact_fan (s INTER t)`, SIMP_TAC[COMPACT_EQ_BOUNDED_CLOSED_FAN; CLOSED_INTER_FAN] THEN MESON_TAC[BOUNDED_SUBSET_FAN; INTER_SUBSET]);; let CLOSED_INTER_COMPACT_FAN = prove (`!s t. closed_fan s /\ compact_fan t ==> compact_fan (s INTER t)`, MESON_TAC[COMPACT_INTER_CLOSED_FAN; INTER_COMM]);; let FINITE_IMP_CLOSED_FAN = prove (`!s. FINITE s ==> closed_fan s`, MESON_TAC[BOLZANO_WEIERSTRASS_IMP_CLOSED_FAN; INFINITE; FINITE_SUBSET]);; let FINITE_IMP_COMPACT_FAN = prove (`!s. FINITE s ==> compact_fan s`, SIMP_TAC[COMPACT_EQ_BOUNDED_CLOSED_FAN; FINITE_IMP_CLOSED_FAN; FINITE_IMP_BOUNDED_FAN]);; let COMPACT_SING_FAN = prove (`!a. compact_fan {a}`, SIMP_TAC[FINITE_IMP_COMPACT_FAN; FINITE_RULES]);; let CLOSED_SING_FAN = prove (`!a. closed_fan {a}`, MESON_TAC[COMPACT_EQ_BOUNDED_CLOSED_FAN; COMPACT_SING_FAN]);; let COMPACT_CBALL_FAN = prove (`!x e. compact_fan(cball_fan(x,e))`, REWRITE_TAC[COMPACT_EQ_BOUNDED_CLOSED_FAN; BOUNDED_CBALL_FAN; CLOSED_CBALL_FAN]);; let COMPACT_FRONTIER_BOUNDED_FAN = prove (`!s. bounded_fan s ==> compact_fan(frontier_fan s)`, SIMP_TAC[frontier_fan; COMPACT_EQ_BOUNDED_CLOSED_FAN; CLOSED_DIFF_FAN; OPEN_INTERIOR_FAN; CLOSED_CLOSURE_FAN] THEN MESON_TAC[SUBSET_DIFF; BOUNDED_SUBSET_FAN; BOUNDED_CLOSURE_FAN]);; let COMPACT_FRONTIER_FAN = prove (`!s. compact_fan s ==> compact_fan (frontier_fan s)`, MESON_TAC[COMPACT_EQ_BOUNDED_CLOSED_FAN; COMPACT_FRONTIER_BOUNDED_FAN]);; let FRONTIER_SUBSET_COMPACT_FAN = prove (`!s. compact_fan s ==> frontier_fan s SUBSET s`, MESON_TAC[FRONTIER_SUBSET_CLOSED_FAN; COMPACT_EQ_BOUNDED_CLOSED_FAN]);; let open_delete_fan = prove(`s DELETE x = s DIFF {x}`,SET_TAC[]);; let OPEN_DELETE_FAN = prove (`!s x. open_fan s ==> open_fan(s DELETE x)`, SIMP_TAC[ open_delete_fan; OPEN_DIFF_FAN; CLOSED_SING_FAN]);; (* ------------------------------------------------------------------------- *) (* Finite intersection property. I could make it an equivalence in fact. *) (* ------------------------------------------------------------------------- *) let compact_imp_fip_fan = prove(`(s = UNIV DIFF t) <=> (UNIV DIFF s = t)`,SET_TAC[]);; let COMPACT_IMP_FIP_FAN = prove (`!s:real^N->bool f. compact_fan s /\ (!t. t IN f ==> closed_fan t) /\ (!f'. FINITE f' /\ f' SUBSET f ==> ~(s INTER (INTERS f') = {})) ==> ~(s INTER (INTERS f) = {})`, REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [COMPACT_EQ_HEINE_BOREL_FAN]) THEN DISCH_THEN(MP_TAC o SPEC `IMAGE (\t:real^N->bool. UNIV DIFF t) f`) THEN ASM_SIMP_TAC[FORALL_IN_IMAGE] THEN DISCH_THEN(fun th -> REPEAT STRIP_TAC THEN MP_TAC th) THEN ASM_SIMP_TAC[OPEN_DIFF_FAN; CLOSED_DIFF_FAN; OPEN_UNIV_FAN; CLOSED_UNIV_FAN; NOT_IMP] THEN CONJ_TAC THENL [UNDISCH_TAC `(s:real^N->bool) INTER INTERS f = {}` THEN ONCE_REWRITE_TAC[SUBSET; EXTENSION] THEN REWRITE_TAC[IN_UNIONS; EXISTS_IN_IMAGE] THEN SET_TAC[]; DISCH_THEN(X_CHOOSE_THEN `g:(real^N->bool)->bool` MP_TAC) THEN FIRST_X_ASSUM(MP_TAC o SPEC `IMAGE (\t:real^N->bool. UNIV DIFF t) g`) THEN ASM_CASES_TAC `FINITE(g:(real^N->bool)->bool)` THEN ASM_SIMP_TAC[FINITE_IMAGE] THEN ONCE_REWRITE_TAC[SUBSET; EXTENSION] THEN REWRITE_TAC[FORALL_IN_IMAGE; IN_INTER; IN_INTERS; IN_IMAGE; IN_DIFF; IN_UNIV; NOT_IN_EMPTY; compact_imp_fip_fan; UNWIND_THM1; IN_UNIONS] THEN SET_TAC[]]);; (* ------------------------------------------------------------------------- *) (* Bounded closed nest property (proof does not use Heine-Borel). *) (* ------------------------------------------------------------------------- *) let BOUNDED_CLOSED_NEST_FAN = prove (`!s. (!n. closed_fan(s n)) /\ (!n. ~(s n = {})) /\ (!m n. m <= n ==> s(n) SUBSET s(m)) /\ bounded_fan(s 0) ==> ?a:real^N. !n:num. a IN s(n)`, GEN_TAC THEN REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; SKOLEM_THM] THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_TAC `a:num->real^N`) STRIP_ASSUME_TAC) THEN SUBGOAL_THEN `compact_fan(s 0:real^N->bool)` MP_TAC THENL [ASM_MESON_TAC[BOUNDED_CLOSED_IMP_COMPACT_FAN]; ALL_TAC] THEN REWRITE_TAC[compact_fan] THEN DISCH_THEN(MP_TAC o SPEC `a:num->real^N`) THEN ANTS_TAC THENL [ASM_MESON_TAC[SUBSET; LE_0]; ALL_TAC] THEN MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `l:real^N` THEN REWRITE_TAC[LIM_SEQUENTIALLY_FAN; o_THM] THEN DISCH_THEN(X_CHOOSE_THEN `r:num->num` STRIP_ASSUME_TAC) THEN GEN_REWRITE_TAC I [TAUT `p <=> ~(~p)`] THEN GEN_REWRITE_TAC RAND_CONV [NOT_FORALL_THM] THEN DISCH_THEN(X_CHOOSE_THEN `N:num` MP_TAC) THEN MP_TAC(ISPECL [`l:real^N`; `(s:num->real^N->bool) N`] CLOSED_APPROACHABLE_FAN) THEN ASM_MESON_TAC[SUBSET; LE_REFL; LE_TRANS; LE_CASES; MONOTONE_BIGGER_FAN]);; (* ------------------------------------------------------------------------- *) (* Decreasing case does not even need compactness, just completeness. *) (* ------------------------------------------------------------------------- *) let DECREASING_CLOSED_NEST_FAN = prove (`!s. (!n. closed_fan(s n)) /\ (!n. ~(s n = {})) /\ (!m n. m <= n ==> s(n) SUBSET s(m)) /\ (!e. &0 < e ==> ?n. !x y. x IN s(n) /\ y IN s(n) ==> dist(x,y) < e) ==> ?a:real^N. !n:num. a IN s(n)`, GEN_TAC THEN REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; SKOLEM_THM] THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_TAC `a:num->real^N`) STRIP_ASSUME_TAC) THEN SUBGOAL_THEN `?l:real^N. (a --> l) sequentially_fan` MP_TAC THENL [ASM_MESON_TAC[cauchy_fan; GE; SUBSET; LE_TRANS; LE_REFL; complete_fan; COMPLETE_UNIV_FAN; IN_UNIV]; ASM_MESON_TAC[LIM_SEQUENTIALLY_FAN; CLOSED_APPROACHABLE_FAN; SUBSET; LE_REFL; LE_TRANS; LE_CASES]]);; (* ------------------------------------------------------------------------- *) (* Strengthen it to the intersection actually being a singleton. *) (* ------------------------------------------------------------------------- *) let DECREASING_CLOSED_NEST_SING_FAN = prove (`!s. (!n. closed_fan(s n)) /\ (!n. ~(s n = {})) /\ (!m n. m <= n ==> s(n) SUBSET s(m)) /\ (!e. &0 < e ==> ?n. !x y. x IN s(n) /\ y IN s(n) ==> dist(x,y) < e) ==> ?a:real^N. INTERS {t | ?n:num. t = s n} = {a}`, GEN_TAC THEN DISCH_TAC THEN FIRST_ASSUM(MP_TAC o MATCH_MP DECREASING_CLOSED_NEST_FAN) THEN MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `a:real^N` THEN DISCH_TAC THEN REWRITE_TAC[EXTENSION; IN_INTERS; IN_SING; IN_ELIM_THM] THEN ASM_MESON_TAC[DIST_POS_LT; REAL_LT_REFL; SUBSET; LE_CASES]);; (* ------------------------------------------------------------------------- *) (* Define continuity over a net to take in restrictions of the set. *) (* ------------------------------------------------------------------------- *) parse_as_infix ("continuous_fan",(12,"right"));; let continuous_fan = new_definition `f continuous_fan net_fan <=> (f --> f(netlimit_fan net_fan)) net_fan`;; let CONTINUOUS_WITHIN_FAN = prove (`!f x:real^M. f continuous_fan (at_fan x within_fan s) <=> (f --> f(x)) (at_fan x within_fan s)`, REPEAT GEN_TAC THEN REWRITE_TAC[continuous_fan] THEN ASM_CASES_TAC `trivial_limit_fan(at_fan (x:real^M) within_fan s)` THENL [ASM_REWRITE_TAC[lim_fan]; ASM_SIMP_TAC[NETLIMIT_WITHIN_FAN]]);; let CONTINUOUS_AT_FAN = prove (`!f (x:real^N). f continuous_fan (at_fan x) <=> (f --> f(x)) (at_fan x)`, ONCE_REWRITE_TAC[GSYM WITHIN_UNIV_FAN] THEN REWRITE_TAC[CONTINUOUS_WITHIN_FAN; IN_UNIV]);; (* ------------------------------------------------------------------------- *) (* Derive the epsilon-delta forms, which we often use as "definitions" *) (* ------------------------------------------------------------------------- *) let continuous_within_fan = prove (`f continuous_fan (at_fan x within_fan s) <=> !e. &0 < e ==> ?d. &0 < d /\ !x'. x' IN s /\ dist(x',x) < d ==> dist(f(x'),f(x)) < e`, REWRITE_TAC[CONTINUOUS_WITHIN_FAN; LIM_WITHIN_FAN] THEN REWRITE_TAC[GSYM DIST_NZ] THEN MESON_TAC[DIST_REFL]);; let continuous_at_fan = prove (`f continuous_fan (at_fan x) <=> !e. &0 < e ==> ?d. &0 < d /\ !x'. dist(x',x) < d ==> dist(f(x'),f(x)) < e`, ONCE_REWRITE_TAC[GSYM WITHIN_UNIV_FAN] THEN REWRITE_TAC[continuous_within_fan; IN_UNIV]);; (* ------------------------------------------------------------------------- *) (* For setwise continuity, just start from the epsilon-delta definitions. *) (* ------------------------------------------------------------------------- *) parse_as_infix ("continuous_on_fan",(12,"right"));; parse_as_infix ("uniformly_continuous_on_fan",(12,"right"));; let continuous_on_fan = new_definition `f continuous_on_fan s <=> !x. x IN s ==> !e. &0 < e ==> ?d. &0 < d /\ !x'. x' IN s /\ dist(x',x) < d ==> dist(f(x'),f(x)) < e`;; let uniformly_continuous_on_fan = new_definition `f uniformly_continuous_on_fan s <=> !e. &0 < e ==> ?d. &0 < d /\ !x x'. x IN s /\ x' IN s /\ dist(x',x) < d ==> dist(f(x'),f(x)) < e`;; (* ------------------------------------------------------------------------- *) (* Some simple consequential lemmas. *) (* ------------------------------------------------------------------------- *) let UNIFORMLY_CONTINUOUS_IMP_CONTINUOUS_FAN = prove (`!f s. f uniformly_continuous_on_fan s ==> f continuous_on_fan s`, REWRITE_TAC[uniformly_continuous_on_fan; continuous_on_fan] THEN MESON_TAC[]);; let CONTINUOUS_AT_IMP_CONTINUOUS_WITHIN_FAN = prove (`!f s x. f continuous_fan (at_fan x) ==> f continuous_fan (at_fan x within_fan s)`, SIMP_TAC[LIM_AT_WITHIN_FAN; CONTINUOUS_AT_FAN; CONTINUOUS_WITHIN_FAN]);; let CONTINUOUS_AT_IMP_CONTINUOUS_ON_FAN = prove (`!f s. (!x. x IN s ==> f continuous_fan (at_fan x)) ==> f continuous_on_fan s`, REWRITE_TAC[continuous_at_fan; continuous_on_fan] THEN MESON_TAC[]);; let CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN_FAN = prove (`!f s. f continuous_on_fan s <=> !x. x IN s ==> f continuous_fan (at_fan x within_fan s)`, REWRITE_TAC[continuous_on_fan; continuous_within_fan]);; let CONTINUOUS_ON_FAN = prove (`!f (s:real^N->bool). f continuous_on_fan s <=> !x. x IN s ==> (f --> f(x)) (at_fan x within_fan s)`, REWRITE_TAC[CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN_FAN; CONTINUOUS_WITHIN_FAN]);; let CONTINUOUS_ON_EQ_CONTINUOUS_AT_FAN = prove (`!f:real^M->real^N s. open_fan s ==> (f continuous_on_fan s <=> (!x. x IN s ==> f continuous_fan (at_fan x)))`, SIMP_TAC[CONTINUOUS_ON_FAN; CONTINUOUS_AT_FAN; LIM_WITHIN_OPEN_FAN]);; let CONTINUOUS_WITHIN_SUBSET_FAN = prove (`!f s t x. f continuous_fan (at_fan x within_fan s) /\ t SUBSET s ==> f continuous_fan (at_fan x within_fan t)`, REWRITE_TAC[CONTINUOUS_WITHIN_FAN] THEN MESON_TAC[LIM_WITHIN_SUBSET_FAN]);; let CONTINUOUS_ON_SUBSET_FAN = prove (`!f s t. f continuous_on_fan s /\ t SUBSET s ==> f continuous_on_fan t`, REWRITE_TAC[CONTINUOUS_ON_FAN] THEN MESON_TAC[SUBSET; LIM_WITHIN_SUBSET_FAN]);; let CONTINUOUS_ON_INTERIOR_FAN = prove (`!f:real^M->real^N s x. f continuous_on_fan s /\ x IN interior_fan(s) ==> f continuous_fan at_fan x`, REWRITE_TAC[interior_fan; IN_ELIM_THM] THEN MESON_TAC[CONTINUOUS_ON_EQ_CONTINUOUS_AT_FAN; CONTINUOUS_ON_SUBSET_FAN]);; (* ------------------------------------------------------------------------- *) (* Characterization of various kinds of continuity in terms of sequences. *) (* ------------------------------------------------------------------------- *) let CONTINUOUS_WITHIN_SEQUENTIALLY_FAN = prove (`!f a:real^N. f continuous_fan (at_fan a within_fan s) <=> !x. (!n. x(n) IN s) /\ (x --> a) sequentially_fan ==> ((f o x) --> f(a)) sequentially_fan`, REPEAT GEN_TAC THEN REWRITE_TAC[continuous_within_fan] THEN EQ_TAC THENL [REWRITE_TAC[LIM_SEQUENTIALLY_FAN; o_THM] THEN MESON_TAC[]; ALL_TAC] THEN ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN REWRITE_TAC[NOT_FORALL_THM; NOT_IMP; NOT_EXISTS_THM] THEN DISCH_THEN(X_CHOOSE_THEN `e:real` (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_OF_NUM_LT; REAL_OF_NUM_LE; REAL_POS; ARITH; REAL_ARITH `&0 <= n ==> &0 < n + &1`; NOT_FORALL_THM; SKOLEM_THM] THEN MATCH_MP_TAC MONO_EXISTS THEN REWRITE_TAC[NOT_IMP; FORALL_AND_THM] THEN X_GEN_TAC `y:num->real^N` THEN REWRITE_TAC[LIM_SEQUENTIALLY_FAN; o_THM] THEN STRIP_TAC THEN CONJ_TAC THENL [ALL_TAC; ASM_MESON_TAC[LE_REFL]] THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC FORALL_POS_MONO_1 THEN CONJ_TAC THENL [ASM_MESON_TAC[REAL_LT_TRANS]; ALL_TAC] THEN X_GEN_TAC `n:num` THEN EXISTS_TAC `n:num` THEN X_GEN_TAC `m:num` THEN DISCH_TAC THEN MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC `&1 / (&m + &1)` THEN ASM_REWRITE_TAC[] THEN ASM_SIMP_TAC[REAL_LE_INV2; real_div; REAL_ARITH `&0 <= x ==> &0 < x + &1`; REAL_POS; REAL_MUL_LID; REAL_LE_RADD; REAL_OF_NUM_LE]);; let CONTINUOUS_AT_SEQUENTIALLY_FAN = prove (`!f a:real^N. f continuous_fan (at_fan a) <=> !x. (x --> a) sequentially_fan ==> ((f o x) --> f(a)) sequentially_fan`, ONCE_REWRITE_TAC[GSYM WITHIN_UNIV_FAN] THEN REWRITE_TAC[CONTINUOUS_WITHIN_SEQUENTIALLY_FAN; IN_UNIV]);; let CONTINUOUS_ON_SEQUENTIALLY_FAN = prove (`!f s:real^N->bool. f continuous_on_fan s <=> !x a. a IN s /\ (!n. x(n) IN s) /\ (x --> a) sequentially_fan ==> ((f o x) --> f(a)) sequentially_fan`, REWRITE_TAC[CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN_FAN; CONTINUOUS_WITHIN_SEQUENTIALLY_FAN] THEN MESON_TAC[]);; let UNIFORMLY_CONTINUOUS_ON_SEQUENTIALLY_FAN = prove (`!f s:real^N->bool. f uniformly_continuous_on_fan s <=> !x y. (!n. x(n) IN s) /\ (!n. y(n) IN s) /\ ((\n. x(n) - y(n)) --> vec 0) sequentially_fan ==> ((\n. f(x(n)) - f(y(n))) --> vec 0) sequentially_fan`, REPEAT GEN_TAC THEN REWRITE_TAC[uniformly_continuous_on_fan] THEN REWRITE_TAC[LIM_SEQUENTIALLY_FAN; dist; VECTOR_SUB_RZERO] THEN EQ_TAC THENL [MESON_TAC[]; ALL_TAC] THEN ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN REWRITE_TAC[NOT_FORALL_THM; NOT_IMP; NOT_EXISTS_THM] THEN DISCH_THEN(X_CHOOSE_THEN `e:real` (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_OF_NUM_LT; REAL_OF_NUM_LE; REAL_POS; ARITH; REAL_ARITH `&0 <= n ==> &0 < n + &1`; NOT_FORALL_THM; SKOLEM_THM] THEN MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `x:num->real^N` THEN MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `y:num->real^N` THEN REWRITE_TAC[NOT_IMP; FORALL_AND_THM] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC[NORM_SUB] THEN CONJ_TAC THENL [MATCH_MP_TAC FORALL_POS_MONO_1 THEN CONJ_TAC THENL [ASM_MESON_TAC[REAL_LT_TRANS]; ALL_TAC] THEN X_GEN_TAC `n:num` THEN EXISTS_TAC `n:num` THEN X_GEN_TAC `m:num` THEN DISCH_TAC THEN MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC `&1 / (&m + &1)` THEN ASM_REWRITE_TAC[] THEN ASM_SIMP_TAC[REAL_LE_INV2; real_div; REAL_ARITH `&0 <= x ==> &0 < x + &1`; REAL_POS; REAL_MUL_LID; REAL_LE_RADD; REAL_OF_NUM_LE]; EXISTS_TAC `e:real` THEN ASM_REWRITE_TAC[] THEN EXISTS_TAC `\x:num. x` THEN ASM_REWRITE_TAC[LE_REFL]]);; (* ------------------------------------------------------------------------- *) (* Combination results for pointwise continuity. *) (* ------------------------------------------------------------------------- *) let CONTINUOUS_CONST_FAN = prove (`!net c. (\x. c) continuous_fan net_fan`, REWRITE_TAC[continuous_fan; LIM_CONST_FAN]);; let CONTINUOUS_CMUL_FAN = prove (`!f c net. f continuous_fan net_fan ==> (\x. c % f(x)) continuous_fan net_fan`, REWRITE_TAC[continuous_fan; LIM_CMUL_FAN]);; let CONTINUOUS_NEG_FAN = prove (`!f net. f continuous_fan net_fan ==> (\x. --(f x)) continuous_fan net_fan`, REWRITE_TAC[continuous_fan; LIM_NEG_FAN]);; let CONTINUOUS_ADD_FAN = prove (`!f g net. f continuous_fan net_fan /\ g continuous_fan net_fan ==> (\x. f(x) + g(x)) continuous_fan net_fan`, REWRITE_TAC[continuous_fan; LIM_ADD_FAN]);; let CONTINUOUS_SUB_FAN = prove (`!f g net. f continuous_fan net_fan /\ g continuous_fan net_fan ==> (\x. f(x) - g(x)) continuous_fan net_fan`, REWRITE_TAC[continuous_fan; LIM_SUB_FAN]);; (* ------------------------------------------------------------------------- *) (* Same thing for setwise continuity. *) (* ------------------------------------------------------------------------- *) let CONTINUOUS_ON_CONST_FAN = prove (`!s c. (\x. c) continuous_on_fan s`, SIMP_TAC[CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN_FAN; CONTINUOUS_CONST_FAN]);; let CONTINUOUS_ON_CMUL_FAN = prove (`!f c s. f continuous_on_fan s ==> (\x. c % f(x)) continuous_on_fan s`, SIMP_TAC[CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN_FAN; CONTINUOUS_CMUL_FAN]);; let CONTINUOUS_ON_NEG_FAN = prove (`!f s. f continuous_on_fan s ==> (\x. --(f x)) continuous_on_fan s`, SIMP_TAC[CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN_FAN; CONTINUOUS_NEG_FAN]);; let CONTINUOUS_ON_ADD_FAN = prove (`!f g s. f continuous_on_fan s /\ g continuous_on_fan s ==> (\x. f(x) + g(x)) continuous_on_fan s`, SIMP_TAC[CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN_FAN; CONTINUOUS_ADD_FAN]);; let CONTINUOUS_ON_SUB_FAN = prove (`!f g s. f continuous_on_fan s /\ g continuous_on_fan s ==> (\x. f(x) - g(x)) continuous_on_fan s`, SIMP_TAC[CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN_FAN; CONTINUOUS_SUB_FAN]);; (* ------------------------------------------------------------------------- *) (* Same thing for uniform continuity, using sequential formulations. *) (* ------------------------------------------------------------------------- *) let UNIFORMLY_CONTINUOUS_ON_CONST_FAN = prove (`!s c. (\x. c) uniformly_continuous_on_fan s`, REWRITE_TAC[UNIFORMLY_CONTINUOUS_ON_SEQUENTIALLY_FAN; o_DEF; VECTOR_SUB_REFL; LIM_CONST_FAN]);; let UNIFORMLY_CONTINUOUS_ON_CMUL_FAN = prove (`!f c s. f uniformly_continuous_on_fan s ==> (\x. c % f(x)) uniformly_continuous_on_fan s`, REPEAT GEN_TAC THEN REWRITE_TAC[UNIFORMLY_CONTINUOUS_ON_SEQUENTIALLY_FAN] THEN REPEAT(MATCH_MP_TAC MONO_FORALL THEN GEN_TAC) THEN DISCH_THEN(fun th -> DISCH_TAC THEN MP_TAC th) THEN ASM_REWRITE_TAC[] THEN DISCH_THEN(MP_TAC o MATCH_MP LIM_CMUL_FAN) THEN ASM_SIMP_TAC[VECTOR_SUB_LDISTRIB; VECTOR_MUL_RZERO]);; let UNIFORMLY_CONTINUOUS_ON_NEG_FAN = prove (`!f s. f uniformly_continuous_on_fan s ==> (\x. --(f x)) uniformly_continuous_on_fan s`, ONCE_REWRITE_TAC[VECTOR_NEG_MINUS1] THEN REWRITE_TAC[UNIFORMLY_CONTINUOUS_ON_CMUL_FAN]);; let UNIFORMLY_CONTINUOUS_ON_ADD_FAN = prove (`!f g s. f uniformly_continuous_on_fan s /\ g uniformly_continuous_on_fan s ==> (\x. f(x) + g(x)) uniformly_continuous_on_fan s`, REPEAT GEN_TAC THEN REWRITE_TAC[UNIFORMLY_CONTINUOUS_ON_SEQUENTIALLY_FAN] THEN REWRITE_TAC[AND_FORALL_THM] THEN REPEAT(MATCH_MP_TAC MONO_FORALL THEN GEN_TAC) THEN DISCH_THEN(fun th -> DISCH_TAC THEN MP_TAC th) THEN ASM_REWRITE_TAC[o_DEF] THEN DISCH_THEN(MP_TAC o MATCH_MP LIM_ADD_FAN) THEN MATCH_MP_TAC EQ_IMP THEN REWRITE_TAC[VECTOR_ADD_LID] THEN AP_THM_TAC THEN BINOP_TAC THEN REWRITE_TAC[FUN_EQ_THM] THEN VECTOR_ARITH_TAC);; let UNIFORMLY_CONTINUOUS_ON_SUB_FAN = prove (`!f g s. f uniformly_continuous_on_fan s /\ g uniformly_continuous_on_fan s ==> (\x. f(x) - g(x)) uniformly_continuous_on_fan s`, REWRITE_TAC[VECTOR_SUB] THEN SIMP_TAC[UNIFORMLY_CONTINUOUS_ON_NEG_FAN; UNIFORMLY_CONTINUOUS_ON_ADD_FAN]);; (* ------------------------------------------------------------------------- *) (* Identity function is continuous in every sense. *) (* ------------------------------------------------------------------------- *) let CONTINUOUS_WITHIN_ID_FAN = prove (`!net_fan a s. (\x. x) continuous_fan (at_fan a within_fan s)`, REWRITE_TAC[continuous_within_fan] THEN MESON_TAC[]);; let CONTINUOUS_AT_ID_FAN = prove (`!net_fan s. (\x. x) continuous_fan (at_fan a)`, REWRITE_TAC[continuous_at_fan] THEN MESON_TAC[]);; let CONTINUOUS_ON_ID_FAN = prove (`!s. (\x. x) continuous_on_fan s`, REWRITE_TAC[continuous_on_fan] THEN MESON_TAC[]);; let UNIFORMLY_CONTINUOUS_ON_ID_FAN = prove (`!s. (\x. x) uniformly_continuous_on_fan s`, REWRITE_TAC[uniformly_continuous_on_fan] THEN MESON_TAC[]);; (* ------------------------------------------------------------------------- *) (* Continuity of all kinds is preserved under composition. *) (* ------------------------------------------------------------------------- *) let CONTINUOUS_WITHIN_COMPOSE_FAN = prove (`!f g x s. f continuous_fan (at_fan x within_fan s) /\ g continuous_fan (at_fan (f x) within_fan IMAGE f s) ==> (g o f) continuous_fan (at_fan x within_fan s)`, REPEAT GEN_TAC THEN REWRITE_TAC[continuous_within_fan; o_THM; IN_IMAGE] THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN MATCH_MP_TAC MONO_FORALL THEN X_GEN_TAC `e:real` THEN ASM_MESON_TAC[]);; let CONTINUOUS_AT_COMPOSE_FAN = prove (`!f g x. f continuous_fan (at_fan x) /\ g continuous_fan (at_fan (f x)) ==> (g o f) continuous_fan (at_fan x)`, ONCE_REWRITE_TAC[GSYM WITHIN_UNIV_FAN] THEN MESON_TAC[CONTINUOUS_WITHIN_COMPOSE_FAN; IN_IMAGE; CONTINUOUS_WITHIN_SUBSET_FAN; SUBSET_UNIV; IN_UNIV]);; let CONTINUOUS_ON_COMPOSE_FAN = prove (`!f g s. f continuous_on_fan s /\ g continuous_on_fan (IMAGE f s) ==> (g o f) continuous_on_fan s`, REWRITE_TAC[CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN_FAN] THEN MESON_TAC[IN_IMAGE; CONTINUOUS_WITHIN_COMPOSE_FAN]);; let UNIFORMLY_CONTINUOUS_ON_COMPOSE_FAN = prove (`!f g s. f uniformly_continuous_on_fan s /\ g uniformly_continuous_on_fan (IMAGE f s) ==> (g o f) uniformly_continuous_on_fan s`, (let lemma1 = prove (`(!y. ((?x. (y = f x) /\ P x) /\ Q y ==> R y)) <=> (!x. P x /\ Q (f x) ==> R (f x))`, MESON_TAC[]) in REPEAT GEN_TAC THEN REWRITE_TAC[uniformly_continuous_on_fan; o_THM; IN_IMAGE] THEN ONCE_REWRITE_TAC[SWAP_FORALL_THM] THEN REWRITE_TAC[lemma1] THEN ONCE_REWRITE_TAC[TAUT `a /\ b /\ c <=> b /\ a /\ c`] THEN ONCE_REWRITE_TAC[SWAP_FORALL_THM] THEN REWRITE_TAC[lemma1] 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 ASM_MESON_TAC[]));; (* ------------------------------------------------------------------------- *) (* Continuity in terms of open preimages. *) (* ------------------------------------------------------------------------- *) let CONTINUOUS_AT_OPEN_FAN = prove (`!f:real^M->real^N x. f continuous_fan (at_fan x) <=> !t. open_fan t /\ f(x) IN t ==> ?s. open_fan s /\ x IN s /\ !x'. x' IN s ==> f(x') IN t`, REPEAT GEN_TAC THEN REWRITE_TAC[continuous_at_fan] THEN EQ_TAC THENL [DISCH_TAC THEN X_GEN_TAC `t:real^N->bool` THEN DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN GEN_REWRITE_TAC LAND_CONV [open_def_fan] THEN DISCH_THEN(MP_TAC o SPEC `(f:real^M->real^N) x`) THEN ASM_MESON_TAC[IN_BALL_FAN; DIST_SYM; OPEN_BALL_FAN; CENTRE_IN_BALL]; DISCH_TAC THEN X_GEN_TAC `e:real` THEN DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC `ball_fan((f:real^M->real^N) x,e)`) THEN ASM_SIMP_TAC[OPEN_BALL_FAN; CENTRE_IN_BALL] THEN MESON_TAC[open_def_fan; IN_BALL_FAN; REAL_LT_TRANS; DIST_SYM]]);; let CONTINUOUS_ON_OPEN_FAN = prove (`!f:real^M->real^N s. f continuous_on_fan s <=> !t. t open_in (IMAGE f s) ==> {x | x IN s /\ f(x) IN t} open_in s`, REPEAT GEN_TAC THEN REWRITE_TAC[continuous_on_fan] THEN EQ_TAC THENL [REWRITE_TAC[open_in; SUBSET; IN_ELIM_THM] THEN DISCH_TAC THEN X_GEN_TAC `t:real^N->bool` THEN STRIP_TAC THEN CONJ_TAC THENL [ASM_MESON_TAC[DIST_REFL]; ALL_TAC] THEN X_GEN_TAC `x:real^M` THEN STRIP_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC `(f:real^M->real^N) x`) THEN ASM_REWRITE_TAC[IN_IMAGE] THEN ASM_MESON_TAC[]; DISCH_TAC THEN X_GEN_TAC `x:real^M` THEN DISCH_TAC THEN X_GEN_TAC `e:real` THEN DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC `ball_fan((f:real^M->real^N) x,e) INTER (IMAGE f s)`) THEN ANTS_TAC THENL [ASM_MESON_TAC[OPEN_IN_OPEN_FAN; INTER_COMM; OPEN_BALL_FAN]; ALL_TAC] THEN REWRITE_TAC[open_in; SUBSET; IN_INTER; IN_ELIM_THM; IN_BALL_FAN; IN_IMAGE] THEN REWRITE_TAC[AND_FORALL_THM] THEN DISCH_THEN(MP_TAC o SPEC `x:real^M`) THEN ASM_MESON_TAC[DIST_REFL; DIST_SYM]]);; (* ------------------------------------------------------------------------- *) (* Similarly in terms of closed sets. *) (* ------------------------------------------------------------------------- *) let CONTINUOUS_ON_CLOSED_FAN = prove (`!f:real^M->real^N s. f continuous_on_fan s <=> !t. t closed_in (IMAGE f s) ==> {x | x IN s /\ f(x) IN t} closed_in s`, REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[CONTINUOUS_ON_OPEN_FAN] THEN EQ_TAC THEN DISCH_TAC THEN X_GEN_TAC `t:real^N->bool` THEN FIRST_X_ASSUM(MP_TAC o SPEC `IMAGE (f:real^M->real^N) s DIFF t`) THENL [REWRITE_TAC[closed_in]; REWRITE_TAC[OPEN_IN_CLOSED_IN_EQ]] THEN MATCH_MP_TAC(TAUT`d /\ (b <=> e) ==> ((a ==> b) ==> c /\ a ==> d /\ e)`) THEN (CONJ_TAC THENL [SIMP_TAC[SUBSET; IN_ELIM_THM]; ALL_TAC] THEN AP_THM_TAC THEN AP_TERM_TAC THEN REWRITE_TAC[EXTENSION; IN_DIFF; IN_IMAGE; IN_ELIM_THM] THEN MESON_TAC[]));; (* ------------------------------------------------------------------------- *) (* The "global" cases. *) (* ------------------------------------------------------------------------- *) let CONTINOUS_OPEN_PREIMAGE_FAN = prove (`!f:real^M->real^N s. (!x. f continuous_fan (at_fan x)) /\ s SUBSET (IMAGE f UNIV) /\ open_fan s ==> open_fan {x | f(x) IN s}`, REPEAT STRIP_TAC THEN MP_TAC(SPECL [`f:real^M->real^N`; `(:real^M)`] CONTINUOUS_ON_OPEN_FAN) THEN ASM_SIMP_TAC[CONTINUOUS_AT_IMP_CONTINUOUS_ON_FAN; IN_UNIV; GSYM OPEN_IN_FAN] THEN DISCH_THEN MATCH_MP_TAC THEN UNDISCH_TAC `open_fan(s:real^N->bool)` THEN REWRITE_TAC[open_def_fan; open_in] THEN ASM_MESON_TAC[]);; let OPEN_TRANSLATION_FAN = prove (`!s a:real^N. open_fan s ==> open_fan(IMAGE (\x. a + x) s)`, REPEAT STRIP_TAC THEN MP_TAC(ISPECL [`\x:real^N. x - a`; `s:real^N->bool`] CONTINOUS_OPEN_PREIMAGE_FAN) THEN ASM_SIMP_TAC[CONTINUOUS_SUB_FAN; CONTINUOUS_AT_ID_FAN; CONTINUOUS_CONST_FAN] THEN MATCH_MP_TAC(TAUT `a /\ b = c ==> (a ==> b) ==> c`) THEN CONJ_TAC THENL [REWRITE_TAC[SUBSET]; AP_TERM_TAC THEN REWRITE_TAC[EXTENSION]] THEN REWRITE_TAC[IN_ELIM_THM; IN_IMAGE; IN_UNIV] THEN ASM_MESON_TAC[VECTOR_ARITH `(a + x) - a = x:real^N`; VECTOR_ARITH `a + (x - a) = x:real^N`]);; (* ------------------------------------------------------------------------- *) (* Preservation of compactness and connectedness under continuous function. *) (* ------------------------------------------------------------------------- *) let COMPACT_CONTINUOUS_IMAGE_FAN = prove (`!f:real^M->real^N s. f continuous_on_fan s /\ compact_fan s ==> compact_fan(IMAGE f s)`, REPEAT GEN_TAC THEN REWRITE_TAC[continuous_on_fan; compact_fan] 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_FAN] 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_FAN]) THEN DISCH_THEN(MP_TAC o SPEC `d:real`) THEN ASM_REWRITE_TAC[o_THM] THEN ASM_MESON_TAC[]);; let CONNECTED_CONTINUOUS_IMAGE_FAN = prove (`!f:real^M->real^N s. f continuous_on_fan s /\ connected_fan s ==> connected_fan(IMAGE f s)`, REPEAT GEN_TAC THEN REWRITE_TAC[CONTINUOUS_ON_OPEN_FAN] THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN REWRITE_TAC[CONNECTED_CLOPEN_FAN; NOT_FORALL_THM; NOT_IMP; DE_MORGAN_THM] THEN REWRITE_TAC[closed_in] THEN DISCH_THEN(X_CHOOSE_THEN `t:real^N->bool` STRIP_ASSUME_TAC) THEN FIRST_X_ASSUM(fun th -> MP_TAC(SPEC `t:real^N->bool` th) THEN MP_TAC(SPEC `IMAGE (f:real^M->real^N) s DIFF t` th)) THEN ASM_REWRITE_TAC[] THEN SUBGOAL_THEN `{x | x IN s /\ (f:real^M->real^N) x IN IMAGE f s DIFF t} = s DIFF {x | x IN s /\ f x IN t}` SUBST1_TAC THENL [UNDISCH_TAC `t SUBSET IMAGE (f:real^M->real^N) s` THEN REWRITE_TAC[EXTENSION; IN_IMAGE; IN_DIFF; IN_ELIM_THM; SUBSET] THEN MESON_TAC[]; REPEAT STRIP_TAC THEN EXISTS_TAC `{x | x IN s /\ (f:real^M->real^N) x IN t}` THEN ASM_REWRITE_TAC[] THEN POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN REWRITE_TAC[IN_IMAGE; SUBSET; IN_ELIM_THM; NOT_IN_EMPTY; EXTENSION] THEN MESON_TAC[]]);; (* ------------------------------------------------------------------------- *) (* Continuity implies uniform continuity on a compact domain. *) (* ------------------------------------------------------------------------- *) let COMPACT_UNIFORMLY_CONTINUOUS_FAN = prove (`!f:real^M->real^N s. f continuous_on_fan s /\ compact_fan s ==> f uniformly_continuous_on_fan s`, REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN REWRITE_TAC[continuous_on_fan; RIGHT_IMP_EXISTS_THM; SKOLEM_THM] THEN DISCH_THEN(X_CHOOSE_TAC `d:real^M->real->real`) THEN REWRITE_TAC[uniformly_continuous_on_fan] THEN X_GEN_TAC `e:real` THEN DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o MATCH_MP HEINE_BOREL_LEMMA_FAN) THEN DISCH_THEN(MP_TAC o SPEC `{b | ?x:real^M. x IN s /\ (b = ball_fan(x,d x (e / &2)))}`) THEN REWRITE_TAC[SUBSET; IN_UNIONS; IN_ELIM_THM; IN_BALL_FAN] THEN ANTS_TAC THENL [ASM_MESON_TAC[CENTRE_IN_BALL; REAL_HALF; OPEN_BALL_FAN]; 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 [`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 REWRITE_TAC[IN_BALL_FAN] THEN ONCE_REWRITE_TAC[DIST_SYM] THEN REPEAT DISCH_TAC THEN MATCH_MP_TAC DIST_TRIANGLE_HALF_L THEN ASM_MESON_TAC[REAL_HALF]);; (* ------------------------------------------------------------------------- *) (* Continuity of inverse function on compact domain. *) (* ------------------------------------------------------------------------- *) let CONTINUOUS_ON_INVERSE_FAN = prove (`!f:real^M->real^N g s. f continuous_on_fan s /\ compact_fan s /\ (!x. x IN s ==> (g(f(x)) = x)) ==> g continuous_on_fan (IMAGE f s)`, REPEAT STRIP_TAC THEN REWRITE_TAC[CONTINUOUS_ON_CLOSED_FAN] THEN SUBGOAL_THEN `IMAGE g (IMAGE (f:real^M->real^N) s) = s` SUBST1_TAC THENL [REWRITE_TAC[EXTENSION; IN_IMAGE] THEN ASM_MESON_TAC[]; ALL_TAC] THEN X_GEN_TAC `t:real^M->bool` THEN DISCH_TAC THEN REWRITE_TAC[CLOSED_IN_CLOSED_FAN] THEN EXISTS_TAC `IMAGE (f:real^M->real^N) t` THEN CONJ_TAC THENL [ASM_MESON_TAC[COMPACT_EQ_BOUNDED_CLOSED_FAN; BOUNDED_SUBSET_FAN; CLOSED_IN_SUBSET; CONTINUOUS_ON_SUBSET_FAN; CLOSED_IN_CLOSED_TRANS_FAN; COMPACT_CONTINUOUS_IMAGE_FAN]; REWRITE_TAC[EXTENSION; IN_INTER; IN_ELIM_THM; IN_IMAGE] THEN ASM_MESON_TAC[CLOSED_IN_SUBSET; SUBSET]]);; (* ------------------------------------------------------------------------- *) (* Topological properties of linear functions. *) (* ------------------------------------------------------------------------- *) let LINEAR_LIM_0_FAN = prove (`!f. linear f ==> (f --> vec 0) (at_fan (vec 0))`, REPEAT STRIP_TAC THEN REWRITE_TAC[LIM_AT_FAN] THEN FIRST_X_ASSUM(MP_TAC o MATCH_MP LINEAR_BOUNDED_POS) THEN DISCH_THEN(X_CHOOSE_THEN `B:real` STRIP_ASSUME_TAC) THEN X_GEN_TAC `e:real` THEN DISCH_TAC THEN EXISTS_TAC `e / B` THEN ASM_SIMP_TAC[REAL_LT_DIV] THEN REWRITE_TAC[dist; VECTOR_SUB_RZERO] THEN ASM_MESON_TAC[REAL_MUL_SYM; REAL_LET_TRANS; REAL_LT_RDIV_EQ]);; (*error in old file*) let LINEAR_CONTINUOUS_AT_FAN = prove (`!f:real^M->real^N a. linear f ==> f continuous_fan (at_fan a)`, REPEAT STRIP_TAC THEN MP_TAC(ISPEC `\x. (f:real^M->real^N) (a + x) - f(a)` LINEAR_LIM_0_FAN) THEN ANTS_TAC THENL [POP_ASSUM MP_TAC THEN SIMP_TAC[linear] THEN REPEAT STRIP_TAC THEN VECTOR_ARITH_TAC; ALL_TAC THEN REWRITE_TAC[GSYM LIM_NULL_FAN; CONTINUOUS_AT_FAN]THEN GEN_REWRITE_TAC RAND_CONV [LIM_AT_ZERO_FAN] THEN SIMP_TAC[]]);; let LINEAR_CONTINUOUS_WITHIN_FAN = prove (`!f:real^M->real^N s a. linear f ==> f continuous_fan (at_fan x within_fan s)`, SIMP_TAC[CONTINUOUS_AT_IMP_CONTINUOUS_WITHIN_FAN; LINEAR_CONTINUOUS_AT_FAN]);; let LINEAR_CONTINUOUS_ON_FAN = prove (`!f:real^M->real^N s. linear f ==> f continuous_on_fan s`, MESON_TAC[LINEAR_CONTINUOUS_AT_FAN; CONTINUOUS_AT_IMP_CONTINUOUS_ON_FAN]);; (* ------------------------------------------------------------------------- *) (* Topological stuff lifted from and dropped to R *) (* ------------------------------------------------------------------------- *) let OPEN_LIFT_FAN = prove (`!s. open_fan(IMAGE lift s) <=> !x. x IN s ==> ?e. &0 < e /\ !x'. abs(x' - x) < e ==> x' IN s`, REWRITE_TAC[open_def_fan; FORALL_LIFT; LIFT_IN_IMAGE_LIFT; DIST_LIFT]);; let BOUNDED_LIFT_FAN = prove (`!s. bounded_fan(IMAGE lift s) <=> ?a. !x. x IN s ==> abs(x) <= a`, REWRITE_TAC[bounded_fan; FORALL_LIFT; NORM_LIFT; LIFT_IN_IMAGE_LIFT]);; let LIMPT_APPROACHABLE_LIFT_FAN = prove (`!x s. (lift x) limit_point_of_fan (IMAGE lift s) <=> !e. &0 < e ==> ?x'. x' IN s /\ ~(x' = x) /\ abs(x' - x) < e`, REWRITE_TAC[LIMPT_APPROACHABLE_FAN; EXISTS_LIFT; LIFT_IN_IMAGE_LIFT; LIFT_EQ; DIST_LIFT]);; let CLOSED_LIFT_FAN = prove (`!s. closed_fan (IMAGE lift s) <=> !x. (!e. &0 < e ==> ?x'. x' IN s /\ ~(x' = x) /\ abs(x' - x) < e) ==> x IN s`, GEN_TAC THEN REWRITE_TAC[CLOSED_LIMPT_FAN; LIMPT_APPROACHABLE_FAN] THEN ONCE_REWRITE_TAC[FORALL_LIFT] THEN REWRITE_TAC[LIMPT_APPROACHABLE_LIFT_FAN; LIFT_EQ; DIST_LIFT; EXISTS_LIFT; LIFT_IN_IMAGE_LIFT]);; let CONTINUOUS_AT_LIFT_RANGE_FAN = prove (`!f x. (lift o f) continuous_fan (at_fan x) <=> !e. &0 < e ==> ?d. &0 < d /\ (!x'. norm(x' - x) < d ==> abs(f x' - f x) < e)`, REWRITE_TAC[continuous_at_fan; o_THM; DIST_LIFT] THEN REWRITE_TAC[dist]);; let CONTINUOUS_ON_LIFT_RANGE_FAN = prove (`!f s. (lift o f) continuous_on_fan s <=> !x. x IN s ==> !e. &0 < e ==> ?d. &0 < d /\ (!x'. x' IN s /\ norm(x' - x) < d ==> abs(f x' - f x) < e)`, REWRITE_TAC[continuous_on_fan; o_THM; DIST_LIFT] THEN REWRITE_TAC[dist]);; let CONTINUOUS_AT_LIFT_NORM_FAN = prove (`!x. (lift o norm) continuous_fan (at_fan x)`, REWRITE_TAC[CONTINUOUS_AT_LIFT_RANGE_FAN; NORM_LIFT] THEN MESON_TAC[REAL_ABS_SUB_NORM; REAL_LET_TRANS]);; let CONTINUOUS_ON_LIFT_NORM_FAN = prove (`!s. (lift o norm) continuous_on_fan s`, REWRITE_TAC[CONTINUOUS_ON_LIFT_RANGE_FAN; NORM_LIFT] THEN MESON_TAC[REAL_ABS_SUB_NORM; REAL_LET_TRANS]);; let CONTINUOUS_AT_LIFT_COMPONENT_FAN = prove (`!i a. 1 <= i /\ i <= dimindex(:N) ==> (\x:real^N. lift(x$i)) continuous_fan (at_fan a)`, SIMP_TAC[continuous_at_fan; DIST_LIFT; GSYM VECTOR_SUB_COMPONENT] THEN MESON_TAC[dist; REAL_LET_TRANS; COMPONENT_LE_NORM]);; let CONTINUOUS_ON_LIFT_COMPONENT_FAN = prove (`!i s. 1 <= i /\ i <= dimindex(:N) ==> (\x:real^N. lift(x$i)) continuous_on_fan s`, SIMP_TAC[continuous_on_fan; DIST_LIFT; GSYM VECTOR_SUB_COMPONENT] THEN MESON_TAC[dist; REAL_LET_TRANS; COMPONENT_LE_NORM]);; (* ------------------------------------------------------------------------- *) (* Hence some handy theorems on distance, diameter etc. of/from a set. *) (* ------------------------------------------------------------------------- *) let BOUNDED_HAS_SUP_FAN = prove (`!s. bounded_fan(IMAGE lift s) /\ ~(s = {}) ==> (!x. x IN s ==> x <= sup s) /\ (!b. (!x. x IN s ==> x <= b) ==> sup s <= b)`, REWRITE_TAC[BOUNDED_LIFT_FAN; IMAGE_EQ_EMPTY] THEN MESON_TAC[SUP; REAL_ARITH `abs(x) <= a ==> x <= a`]);; let BOUNDED_HAS_INF_FAN = prove (`!s. bounded_fan(IMAGE lift s) /\ ~(s = {}) ==> (!x. x IN s ==> inf s <= x) /\ (!b. (!x. x IN s ==> b <= x) ==> b <= inf s)`, REWRITE_TAC[BOUNDED_LIFT_FAN; IMAGE_EQ_EMPTY] THEN MESON_TAC[INF; REAL_ARITH `abs(x) <= a ==> --a <= x`]);; let COMPACT_ATTAINS_SUP_FAN = prove (`!s. compact_fan (IMAGE lift s) /\ ~(s = {}) ==> ?x. x IN s /\ !y. y IN s ==> y <= x`, REWRITE_TAC[COMPACT_EQ_BOUNDED_CLOSED_FAN] THEN REPEAT STRIP_TAC THEN MP_TAC(SPEC `s:real->bool` BOUNDED_HAS_SUP_FAN) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN EXISTS_TAC `sup s` THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[CLOSED_LIFT_FAN; REAL_ARITH `s <= s - e <=> ~(&0 < e)`; REAL_ARITH `x <= s /\ ~(x <= s - e) ==> abs(x - s) < e`]);; let COMPACT_ATTAINS_INF_FAN = prove (`!s. compact_fan (IMAGE lift s) /\ ~(s = {}) ==> ?x. x IN s /\ !y. y IN s ==> x <= y`, REWRITE_TAC[COMPACT_EQ_BOUNDED_CLOSED_FAN] THEN REPEAT STRIP_TAC THEN MP_TAC(SPEC `s:real->bool` BOUNDED_HAS_INF_FAN) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN EXISTS_TAC `inf s` THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[CLOSED_LIFT_FAN; REAL_ARITH `s + e <= s <=> ~(&0 < e)`; REAL_ARITH `s <= x /\ ~(s + e <= x) ==> abs(x - s) < e`]);; let CONTINUOUS_ATTAINS_SUP_FAN = prove (`!f:real^N->real s. compact_fan s /\ ~(s = {}) /\ (lift o f) continuous_on_fan s ==> ?x. x IN s /\ !y. y IN s ==> f(y) <= f(x)`, REPEAT STRIP_TAC THEN MP_TAC(SPEC `IMAGE (f:real^N->real) s` COMPACT_ATTAINS_SUP_FAN) THEN ASM_SIMP_TAC[GSYM IMAGE_o; COMPACT_CONTINUOUS_IMAGE_FAN; IMAGE_EQ_EMPTY] THEN MESON_TAC[IN_IMAGE]);; let CONTINUOUS_ATTAINS_INF_FAN = prove (`!f:real^N->real s. compact_fan s /\ ~(s = {}) /\ (lift o f) continuous_on_fan s ==> ?x. x IN s /\ !y. y IN s ==> f(x) <= f(y)`, REPEAT STRIP_TAC THEN MP_TAC(SPEC `IMAGE (f:real^N->real) s` COMPACT_ATTAINS_INF_FAN) THEN ASM_SIMP_TAC[GSYM IMAGE_o; COMPACT_CONTINUOUS_IMAGE_FAN; IMAGE_EQ_EMPTY] THEN MESON_TAC[IN_IMAGE]);; let DISTANCE_ATTAINS_SUP_FAN = prove (`!s a. compact_fan s /\ ~(s = {}) ==> ?x. x IN s /\ !y. y IN s ==> dist(a,y) <= dist(a,x)`, REPEAT STRIP_TAC THEN MATCH_MP_TAC CONTINUOUS_ATTAINS_SUP_FAN THEN ASM_REWRITE_TAC[CONTINUOUS_ON_LIFT_RANGE_FAN] THEN REWRITE_TAC[dist] THEN ASM_MESON_TAC[REAL_LET_TRANS; REAL_ABS_SUB_NORM; NORM_NEG; VECTOR_ARITH `(a - x) - (a - y) = --(x - y):real^N`]);; (* ------------------------------------------------------------------------- *) (* For *minimal* distance, we only need closure, not compactness. *) (* ------------------------------------------------------------------------- *) let DISTANCE_ATTAINS_INF_FAN = prove (`!s a:real^N. closed_fan s /\ ~(s = {}) ==> ?x. x IN s /\ !y. y IN s ==> dist(a,x) <= dist(a,y)`, REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN REWRITE_TAC[GSYM MEMBER_NOT_EMPTY] THEN DISCH_THEN(X_CHOOSE_TAC `b:real^N`) THEN MP_TAC(ISPECL [`\x:real^N. dist(a,x)`; `cball_fan(a:real^N,dist(b,a)) INTER s`] CONTINUOUS_ATTAINS_INF_FAN) THEN ANTS_TAC THENL [ASM_SIMP_TAC[COMPACT_EQ_BOUNDED_CLOSED_FAN; CLOSED_INTER_FAN; BOUNDED_INTER_FAN; BOUNDED_CBALL_FAN; CLOSED_CBALL_FAN; GSYM MEMBER_NOT_EMPTY] THEN REWRITE_TAC[dist; CONTINUOUS_ON_LIFT_RANGE_FAN; IN_INTER; IN_CBALL_FAN] THEN ASM_MESON_TAC[REAL_LET_TRANS; REAL_ABS_SUB_NORM; NORM_NEG; REAL_LE_REFL; NORM_SUB; VECTOR_ARITH `(a - x) - (a - y) = --(x - y):real^N`]; MATCH_MP_TAC MONO_EXISTS THEN REWRITE_TAC[IN_INTER; IN_CBALL_FAN] THEN ASM_MESON_TAC[DIST_SYM; REAL_LE_TOTAL; REAL_LE_TRANS]]);; (* ------------------------------------------------------------------------- *) (* And so we have continuity of inverse. *) (* ------------------------------------------------------------------------- *) let LIM_INV_FAN = prove (`!net_fan:(A)net_fan f l. ((lift o f) --> lift l) net_fan /\ ~(l = &0) ==> ((lift o inv o f) --> lift(inv l)) net_fan`, REPEAT GEN_TAC THEN REWRITE_TAC[lim_fan] THEN ASM_CASES_TAC `trivial_limit_fan(net_fan:(A)net_fan)` THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[o_THM; DIST_LIFT] THEN STRIP_TAC THEN X_GEN_TAC `e:real` THEN DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC `min (abs(l) / &2) ((l pow 2 * e) / &2)`) THEN REWRITE_TAC[REAL_LT_MIN] THEN ANTS_TAC THENL [ASM_SIMP_TAC[GSYM REAL_ABS_NZ; REAL_LT_DIV; REAL_OF_NUM_LT; ARITH] THEN MATCH_MP_TAC REAL_LT_DIV THEN REWRITE_TAC[REAL_OF_NUM_LT; ARITH] THEN ONCE_REWRITE_TAC[GSYM REAL_POW2_ABS] THEN ASM_SIMP_TAC[REAL_LT_MUL; GSYM REAL_ABS_NZ; REAL_POW_LT]; ALL_TAC] THEN MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `a:A` THEN MATCH_MP_TAC MONO_AND THEN REWRITE_TAC[] THEN MATCH_MP_TAC MONO_FORALL THEN X_GEN_TAC `b:A` THEN MATCH_MP_TAC MONO_IMP THEN REWRITE_TAC[] THEN SIMP_TAC[REAL_LT_RDIV_EQ; REAL_OF_NUM_LT; ARITH] THEN STRIP_TAC THEN FIRST_ASSUM(ASSUME_TAC o MATCH_MP (REAL_ARITH `abs(x - l) * &2 < abs l ==> ~(x = &0)`)) THEN ASM_SIMP_TAC[REAL_SUB_INV; REAL_ABS_DIV; REAL_LT_LDIV_EQ; GSYM REAL_ABS_NZ; REAL_ENTIRE] THEN FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH `abs(x - y) * &2 < b * c ==> c * b <= d * &2 ==> abs(y - x) < d`)) THEN ASM_SIMP_TAC[GSYM REAL_MUL_ASSOC; REAL_LE_LMUL_EQ] THEN ONCE_REWRITE_TAC[GSYM REAL_POW2_ABS] THEN ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN ASM_SIMP_TAC[REAL_ABS_MUL; REAL_POW_2; REAL_MUL_ASSOC; GSYM REAL_ABS_NZ; REAL_LE_RMUL_EQ] THEN ASM_SIMP_TAC[REAL_ARITH `abs(x - y) * &2 < abs y ==> abs y <= &2 * abs x`]);; let CONTINUOUS_INV_FAN = prove (`!net f. (lift o f) continuous_fan net_fan /\ ~(f(netlimit_fan net_fan) = &0) ==> (lift o inv o f) continuous_fan net_fan`, REWRITE_TAC[continuous_fan; LIM_INV_FAN; o_THM]);; let CONTINUOUS_AT_WITHIN_INV_FAN = prove (`!f s a:real^N. (lift o f) continuous_fan (at_fan a within_fan s) /\ ~(f a = &0) ==> (lift o inv o f) continuous_fan (at_fan a within_fan s)`, REPEAT GEN_TAC THEN ASM_CASES_TAC `trivial_limit_fan (at_fan (a:real^N) within_fan s)` THENL [ASM_REWRITE_TAC[continuous_fan; lim_fan]; ASM_SIMP_TAC[NETLIMIT_WITHIN_FAN; CONTINUOUS_INV_FAN]]);; let CONTINUOUS_AT_INV_FAN = prove (`!f a. (lift o f) continuous_fan at_fan a /\ ~(f a = &0) ==> (lift o inv o f) continuous_fan at_fan a`, ONCE_REWRITE_TAC[GSYM WITHIN_UNIV_FAN] THEN REWRITE_TAC[CONTINUOUS_AT_WITHIN_INV_FAN]);; (* ------------------------------------------------------------------------- *) (* Preservation properties for pasted sets. *) (* ------------------------------------------------------------------------- *) let BOUNDED_PASTECART_FAN = prove (`!s:real^M->bool t:real^N->bool. bounded_fan s /\ bounded_fan t ==> bounded_fan {pastecart x y | x IN s /\ y IN t}`, REPEAT GEN_TAC THEN REWRITE_TAC[bounded_fan; IN_ELIM_THM] THEN ASM_MESON_TAC[NORM_PASTECART; REAL_LE_ADD2; REAL_LE_TRANS]);; let CLOSED_PASTECART_FAN = prove (`!s:real^M->bool t:real^N->bool. closed_fan s /\ closed_fan t ==> closed_fan {pastecart x y | x IN s /\ y IN t}`, REPEAT GEN_TAC THEN REWRITE_TAC[CLOSED_SEQUENTIAL_LIMITS_FAN] THEN REWRITE_TAC[LIM_SEQUENTIALLY_FAN; IN_ELIM_THM; dist] THEN STRIP_TAC THEN MAP_EVERY X_GEN_TAC [`z:num->real^(M,N)finite_sum`; `l:real^(M,N)finite_sum`] THEN DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN REWRITE_TAC[SKOLEM_THM; LEFT_IMP_EXISTS_THM] THEN MAP_EVERY X_GEN_TAC [`x:num->real^M`; `y:num->real^N`] THEN REWRITE_TAC[FORALL_AND_THM] THEN STRIP_TAC THEN MAP_EVERY EXISTS_TAC [`fstcart(l:real^(M,N)finite_sum)`; `sndcart(l:real^(M,N)finite_sum)`] THEN REWRITE_TAC[PASTECART_FST_SND] THEN CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THENL [EXISTS_TAC `x:num->real^M`; EXISTS_TAC `y:num->real^N`] THEN ASM_REWRITE_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 MATCH_MP_TAC MONO_EXISTS THEN ASM_REWRITE_TAC[] THEN GEN_TAC THEN MATCH_MP_TAC MONO_FORALL THEN GEN_TAC THEN MATCH_MP_TAC MONO_IMP THEN REWRITE_TAC[] THEN MATCH_MP_TAC(REAL_ARITH `x <= y ==> y < a ==> x < a`) THEN MESON_TAC[NORM_FSTCART; FSTCART_SUB; FSTCART_PASTECART; NORM_SNDCART; SNDCART_SUB; SNDCART_PASTECART]);; let COMPACT_PASTECART_FAN = prove (`!s:real^M->bool t:real^N->bool. compact_fan s /\ compact_fan t ==> compact_fan {pastecart x y | x IN s /\ y IN t}`, SIMP_TAC[COMPACT_EQ_BOUNDED_CLOSED_FAN; BOUNDED_PASTECART_FAN; CLOSED_PASTECART_FAN]);; (* ------------------------------------------------------------------------- *) (* Hence some useful properties follow quite easily. *) (* ------------------------------------------------------------------------- *) let COMPACT_MULTIPLES_FAN = prove (`!s:real^N->bool c. compact_fan s ==> compact_fan (IMAGE (\x. c % x) s)`, REPEAT STRIP_TAC THEN MATCH_MP_TAC COMPACT_CONTINUOUS_IMAGE_FAN THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC CONTINUOUS_AT_IMP_CONTINUOUS_ON_FAN THEN REPEAT STRIP_TAC THEN MATCH_MP_TAC LINEAR_CONTINUOUS_AT_FAN THEN REWRITE_TAC[linear] THEN CONJ_TAC THEN VECTOR_ARITH_TAC);; let COMPACT_NEGATIONS_FAN = prove (`!s:real^N->bool. compact_fan s ==> compact_fan (IMAGE (--) s)`, REPEAT STRIP_TAC THEN MATCH_MP_TAC COMPACT_CONTINUOUS_IMAGE_FAN THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC CONTINUOUS_AT_IMP_CONTINUOUS_ON_FAN THEN REPEAT STRIP_TAC THEN MATCH_MP_TAC LINEAR_CONTINUOUS_AT_FAN THEN REWRITE_TAC[linear] THEN CONJ_TAC THEN VECTOR_ARITH_TAC);; let COMPACT_SUMS_FAN = prove (`!s:real^N->bool t. compact_fan s /\ compact_fan t ==> compact_fan {x + y | x IN s /\ y IN t}`, REPEAT STRIP_TAC THEN SUBGOAL_THEN `{x + y | x IN s /\ y IN t} = IMAGE (\z. fstcart z + sndcart z :real^N) {pastecart x y | x IN s /\ y IN t}` SUBST1_TAC THENL [REWRITE_TAC[EXTENSION; IN_ELIM_THM; IN_IMAGE] THEN GEN_TAC THEN EQ_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[FSTCART_PASTECART; SNDCART_PASTECART; PASTECART_FST_SND]; ALL_TAC] THEN MATCH_MP_TAC COMPACT_CONTINUOUS_IMAGE_FAN THEN ASM_SIMP_TAC[COMPACT_PASTECART_FAN] THEN MATCH_MP_TAC CONTINUOUS_AT_IMP_CONTINUOUS_ON_FAN THEN REPEAT STRIP_TAC THEN MATCH_MP_TAC LINEAR_CONTINUOUS_AT_FAN THEN REWRITE_TAC[linear; FSTCART_ADD; FSTCART_CMUL; SNDCART_ADD; SNDCART_CMUL] THEN CONJ_TAC THEN VECTOR_ARITH_TAC);; let COMPACT_DIFFERENCES_FAN = prove (`!s:real^N->bool t. compact_fan s /\ compact_fan t ==> compact_fan {x - y | x IN s /\ y IN t}`, REPEAT STRIP_TAC THEN SUBGOAL_THEN `{x - y | x:real^N IN s /\ y IN t} = {x + y | x IN s /\ y IN (IMAGE (--) t)}` (fun th -> ASM_SIMP_TAC[th; COMPACT_SUMS_FAN; COMPACT_NEGATIONS_FAN]) THEN REWRITE_TAC[EXTENSION; IN_ELIM_THM; IN_IMAGE] THEN ONCE_REWRITE_TAC[VECTOR_ARITH `(x:real^N = --y) <=> (y = --x)`] THEN SIMP_TAC[VECTOR_SUB; GSYM CONJ_ASSOC; UNWIND_THM2] THEN MESON_TAC[VECTOR_NEG_NEG]);; let COMPACT_TRANSLATION_FAN = prove (`!s a:real^N. compact_fan s ==> compact_fan (IMAGE (\x. a + x) s)`, REPEAT STRIP_TAC THEN MP_TAC(ISPECL [`{a:real^N}`; `s:real^N->bool`] COMPACT_SUMS_FAN) THEN ASM_REWRITE_TAC[COMPACT_SING_FAN] THEN MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC THEN REWRITE_TAC[EXTENSION; IN_ELIM_THM; IN_SING; IN_IMAGE] THEN MESON_TAC[]);; let COMPACT_AFFINITY_FAN = prove (`!s a:real^N c. compact_fan s ==> compact_fan (IMAGE (\x. a + c % x) s)`, REPEAT STRIP_TAC THEN SUBGOAL_THEN `(\x:real^N. a + c % x) = (\x. a + x) o (\x. c % x)` SUBST1_TAC THENL [REWRITE_TAC[o_DEF]; ALL_TAC] THEN ASM_SIMP_TAC[IMAGE_o; COMPACT_TRANSLATION_FAN; COMPACT_MULTIPLES_FAN]);; (* ------------------------------------------------------------------------- *) (* Hence we get the following. *) (* ------------------------------------------------------------------------- *) let COMPACT_SUP_MAXDISTANCE_FAN = prove (`!s:real^N->bool. compact_fan s /\ ~(s = {}) ==> ?x y. x IN s /\ y IN s /\ !u v. u IN s /\ v IN s ==> norm(u - v) <= norm(x - y)`, REPEAT STRIP_TAC THEN MP_TAC(ISPECL [`{x - y:real^N | x IN s /\ y IN s}`; `vec 0:real^N`] DISTANCE_ATTAINS_SUP_FAN) THEN ANTS_TAC THENL [ASM_SIMP_TAC[COMPACT_DIFFERENCES_FAN] THEN REWRITE_TAC[EXTENSION; IN_ELIM_THM; NOT_IN_EMPTY] THEN ASM_MESON_TAC[MEMBER_NOT_EMPTY]; REWRITE_TAC[IN_ELIM_THM; dist; VECTOR_SUB_RZERO; VECTOR_SUB_LZERO; NORM_NEG] THEN MESON_TAC[]]);; (* ------------------------------------------------------------------------- *) (* We can state this in terms of diameter of a set. *) (* ------------------------------------------------------------------------- *) let diameter_fan = new_definition `diameter_fan s = if s = {} then &0 else sup {norm(x - y) | x IN s /\ y IN s}`;; let DIAMETER_BOUNDED_FAN = prove (`!s. bounded_fan s ==> (!x:real^N y. x IN s /\ y IN s ==> norm(x - y) <= diameter_fan s) /\ (!d. &0 <= d /\ d < diameter_fan s ==> ?x y. x IN s /\ y IN s /\ norm(x - y) > d)`, GEN_TAC THEN DISCH_TAC THEN ASM_CASES_TAC `s:real^N->bool = {}` THEN ASM_REWRITE_TAC[diameter_fan; NOT_IN_EMPTY; REAL_LET_ANTISYM] THEN MP_TAC(SPEC `{norm(x - y:real^N) | x IN s /\ y IN s}` SUP) THEN ABBREV_TAC `b = sup {norm(x - y:real^N) | x IN s /\ y IN s}` THEN REWRITE_TAC[EXTENSION; IN_ELIM_THM] THEN REWRITE_TAC[NOT_IN_EMPTY; real_gt] THEN ANTS_TAC THENL [CONJ_TAC THENL [ASM_MESON_TAC[MEMBER_NOT_EMPTY]; ALL_TAC]; MESON_TAC[REAL_NOT_LE]] THEN SIMP_TAC[VECTOR_SUB; LEFT_IMP_EXISTS_THM] THEN FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [bounded_fan]) THEN MESON_TAC[REAL_ARITH `x <= y + z /\ y <= b /\ z<= b ==> x <= b + b`; NORM_TRIANGLE; NORM_NEG]);; let DIAMETER_BOUNDED_BOUND_FAN = prove (`!s x y. bounded_fan s /\ x IN s /\ y IN s ==> norm(x - y) <= diameter_fan s`, MESON_TAC[DIAMETER_BOUNDED_FAN]);; let DIAMETER_COMPACT_ATTAINED_FAN = prove (`!s:real^N->bool. compact_fan s /\ ~(s = {}) ==> ?x y. x IN s /\ y IN s /\ (norm(x - y) = diameter_fan s)`, GEN_TAC THEN DISCH_TAC THEN FIRST_ASSUM(MP_TAC o MATCH_MP COMPACT_SUP_MAXDISTANCE_FAN) THEN REPEAT(MATCH_MP_TAC MONO_EXISTS THEN GEN_TAC) THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN MP_TAC(SPEC `s:real^N->bool` DIAMETER_BOUNDED_FAN) THEN RULE_ASSUM_TAC(REWRITE_RULE[COMPACT_EQ_BOUNDED_CLOSED_FAN]) THEN ASM_REWRITE_TAC[real_gt] THEN STRIP_TAC THEN REWRITE_TAC[GSYM REAL_LE_ANTISYM] THEN ASM_MESON_TAC[NORM_POS_LE; REAL_NOT_LT]);; (* ------------------------------------------------------------------------- *) (* Related results with closure as the conclusion. *) (* ------------------------------------------------------------------------- *) let CLOSED_MULTIPLES_FAN = prove (`!s:real^N->bool c. closed_fan s ==> closed_fan (IMAGE (\x. c % x) s)`, REPEAT GEN_TAC THEN ASM_CASES_TAC `s :real^N->bool = {}` THEN ASM_REWRITE_TAC[CLOSED_EMPTY_FAN; IMAGE_CLAUSES] THEN ASM_CASES_TAC `c = &0` THENL [SUBGOAL_THEN `IMAGE (\x:real^N. c % x) s = {(vec 0)}` (fun th -> REWRITE_TAC[th; CLOSED_SING_FAN]) THEN ASM_REWRITE_TAC[EXTENSION; IN_IMAGE; IN_SING; VECTOR_MUL_LZERO] THEN ASM_MESON_TAC[MEMBER_NOT_EMPTY]; ALL_TAC] THEN REWRITE_TAC[CLOSED_SEQUENTIAL_LIMITS_FAN; IN_IMAGE; SKOLEM_THM] THEN STRIP_TAC THEN X_GEN_TAC `x:num->real^N` THEN X_GEN_TAC `l:real^N` THEN DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN DISCH_THEN(X_CHOOSE_THEN `y:num->real^N` MP_TAC) THEN REWRITE_TAC[FORALL_AND_THM] THEN STRIP_TAC THEN EXISTS_TAC `inv(c) % l :real^N` THEN ASM_SIMP_TAC[VECTOR_MUL_ASSOC; REAL_MUL_RINV; VECTOR_MUL_LID] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN EXISTS_TAC `\n:num. inv(c) % x n:real^N` THEN ASM_REWRITE_TAC[] THEN CONJ_TAC THENL [ASM_SIMP_TAC[VECTOR_MUL_ASSOC; REAL_MUL_LINV; VECTOR_MUL_LID]; MATCH_MP_TAC LIM_CMUL_FAN THEN FIRST_ASSUM(fun th -> REWRITE_TAC[SYM(SPEC_ALL th)]) THEN ASM_REWRITE_TAC[ETA_AX]]);; let CLOSED_NEGATIONS_FAN = prove (`!s:real^N->bool. closed_fan s ==> closed_fan (IMAGE (--) s)`, REPEAT GEN_TAC THEN SUBGOAL_THEN `IMAGE (--) s = IMAGE (\x:real^N. --(&1) % x) s` SUBST1_TAC THEN SIMP_TAC[CLOSED_MULTIPLES_FAN] THEN REWRITE_TAC[VECTOR_ARITH `--(&1) % x = --x`] THEN REWRITE_TAC[ETA_AX]);; (* ------------------------------------------------------------------------- *) (* A cute way of denoting open and closed intervals using overloading. *) (* ------------------------------------------------------------------------- *) let open_interval_fan = new_definition `open_interval_fan(a:real^N,b:real^N) = {x:real^N | !i. 1 <= i /\ i <= dimindex(:N) ==> a$i < x$i /\ x$i < b$i}`;; let closed_interval_fan = new_definition `closed_interval_fan(l:(real^N#real^N)list) = {x:real^N | !i. 1 <= i /\ i <= dimindex(:N) ==> FST(HD l)$i <= x$i /\ x$i <= SND(HD l)$i}`;; make_overloadable "interval_fan" `:A`;; overload_interface("interval_fan",`open_interval_fan`);; overload_interface("interval_fan",`closed_interval_fan`);; let interval_fan = prove (`(interval_fan (a,b) = {x:real^N | !i. 1 <= i /\ i <= dimindex(:N) ==> a$i < x$i /\ x$i < b$i}) /\ (interval_fan [a,b] = {x:real^N | !i. 1 <= i /\ i <= dimindex(:N) ==> a$i <= x$i /\ x$i <= b$i})`, REWRITE_TAC[open_interval_fan; closed_interval_fan; HD; FST; SND]);; let IN_INTERVAL_FAN = prove (`(!x:real^N. x IN interval_fan (a,b) <=> !i. 1 <= i /\ i <= dimindex(:N) ==> a$i < x$i /\ x$i < b$i) /\ (!x:real^N. x IN interval_fan [a,b] <=> !i. 1 <= i /\ i <= dimindex(:N) ==> a$i <= x$i /\ x$i <= b$i)`, REWRITE_TAC[interval_fan; IN_ELIM_THM]);; (* ------------------------------------------------------------------------- *) (* Some stuff for half-infinite intervals too; maybe I need a notation? *) (* ------------------------------------------------------------------------- *) let CLOSED_INTERVAL_LEFT_FAN = prove (`!b:real^N. closed_fan {x:real^N | !i. 1 <= i /\ i <= dimindex(:N) ==> x$i <= b$i}`, REWRITE_TAC[CLOSED_LIMPT_FAN; LIMPT_APPROACHABLE_FAN; IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN REWRITE_TAC[GSYM REAL_NOT_LT] THEN DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC `(x:real^N)$i - (b:real^N)$i`) THEN ASM_REWRITE_TAC[REAL_SUB_LT] THEN DISCH_THEN(X_CHOOSE_THEN `z:real^N` MP_TAC) THEN REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN REWRITE_TAC[dist; REAL_NOT_LT] THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `abs((z - x :real^N)$i)` THEN ASM_SIMP_TAC[COMPONENT_LE_NORM] THEN ASM_SIMP_TAC[VECTOR_SUB_COMPONENT] THEN ASM_SIMP_TAC[REAL_ARITH `z <= b /\ b < x ==> x - b <= abs(z - x)`]);; let CLOSED_INTERVAL_RIGHT_FAN = prove (`!a:real^N. closed_fan {x:real^N | !i. 1 <= i /\ i <= dimindex(:N) ==> a$i <= x$i}`, REWRITE_TAC[CLOSED_LIMPT_FAN; LIMPT_APPROACHABLE_FAN; IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN REWRITE_TAC[GSYM REAL_NOT_LT] THEN DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC `(a:real^N)$i - (x:real^N)$i`) THEN ASM_REWRITE_TAC[REAL_SUB_LT] THEN DISCH_THEN(X_CHOOSE_THEN `z:real^N` MP_TAC) THEN REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN REWRITE_TAC[dist; REAL_NOT_LT] THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `abs((z - x :real^N)$i)` THEN ASM_SIMP_TAC[COMPONENT_LE_NORM] THEN ASM_SIMP_TAC[VECTOR_SUB_COMPONENT] THEN ASM_SIMP_TAC[REAL_ARITH `x < a /\ a <= z ==> a - x <= abs(z - x)`]);; (* ------------------------------------------------------------------------- *) (* Closure of halfspaces and hyperplanes. *) (* ------------------------------------------------------------------------- *) let LIM_LIFT_DOT_FAN = prove (`!f:real^M->real^N a. (f --> l) net_fan ==> ((lift o (\y. a dot f(y))) --> lift(a dot l)) net_fan`, REPEAT GEN_TAC THEN ASM_CASES_TAC `a = vec 0:real^N` THENL [ASM_REWRITE_TAC[DOT_LZERO; LIFT_NUM; o_DEF; LIM_CONST_FAN]; ALL_TAC] THEN REWRITE_TAC[lim_fan] THEN MATCH_MP_TAC MONO_OR THEN REWRITE_TAC[] THEN DISCH_TAC THEN X_GEN_TAC `e:real` THEN DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC `e / norm(a:real^N)`) THEN ASM_SIMP_TAC[REAL_LT_DIV; NORM_POS_LT; REAL_LT_RDIV_EQ] THEN REWRITE_TAC[dist; o_THM; GSYM LIFT_SUB; GSYM DOT_RSUB; NORM_LIFT] THEN ONCE_REWRITE_TAC[DOT_SYM] THEN MESON_TAC[NORM_CAUCHY_SCHWARZ_ABS; REAL_MUL_SYM; REAL_LET_TRANS]);; let CONTINUOUS_AT_LIFT_DOT_FAN = prove (`!a:real^N x. (lift o (\y. a dot y)) continuous_fan at_fan x`, REPEAT GEN_TAC THEN REWRITE_TAC[CONTINUOUS_AT_FAN; o_THM] THEN MATCH_MP_TAC LIM_LIFT_DOT_FAN THEN REWRITE_TAC[LIM_AT_FAN] THEN MESON_TAC[]);; let CONTINUOUS_ON_LIFT_DOT_FAN = prove (`!s x. (lift o (\y. a dot y)) continuous_on_fan s`, SIMP_TAC[CONTINUOUS_AT_IMP_CONTINUOUS_ON_FAN; CONTINUOUS_AT_LIFT_DOT_FAN]);; let CLOSED_HALFSPACE_LE_FAN = prove (`!a:real^N b. closed_fan {x | a dot x <= b}`, REPEAT GEN_TAC THEN MP_TAC(ISPECL [`(:real^N)`; `a:real^N`] CONTINUOUS_ON_LIFT_DOT_FAN) THEN REWRITE_TAC[CONTINUOUS_ON_CLOSED_FAN; GSYM CLOSED_IN_FAN] THEN DISCH_THEN(MP_TAC o SPEC `IMAGE lift {r | ?x:real^N. (a dot x = r) /\ r <= b}`) THEN ANTS_TAC THENL [ALL_TAC; MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC THEN REWRITE_TAC[EXTENSION; IN_ELIM_THM; IN_IMAGE; IN_UNIV] THEN REWRITE_TAC[o_DEF] THEN MESON_TAC[LIFT_DROP]] THEN REWRITE_TAC[CLOSED_IN_CLOSED_FAN] THEN EXISTS_TAC `{x | !i. 1 <= i /\ i <= dimindex(:1) ==> (x:real^1)$i <= (lift b)$i}` THEN REWRITE_TAC[CLOSED_INTERVAL_LEFT_FAN] THEN SIMP_TAC[EXTENSION; IN_IMAGE; IN_UNIV; IN_ELIM_THM; IN_INTER; IN_INTERVAL_FAN; VEC_COMPONENT; DIMINDEX_1; LAMBDA_BETA; o_THM] THEN SIMP_TAC[ARITH_RULE `1 <= i /\ i <= 1 <=> (i = 1)`] THEN REWRITE_TAC[GSYM drop; LEFT_FORALL_IMP_THM; EXISTS_REFL] THEN MESON_TAC[LIFT_DROP]);; let CLOSED_HALFSPACE_GE_FAN = prove (`!a:real^N b. closed_fan {x | a dot x >= b}`, REWRITE_TAC[REAL_ARITH `a >= b <=> --a <= --b`] THEN REWRITE_TAC[GSYM DOT_LNEG; CLOSED_HALFSPACE_LE_FAN]);; let CLOSED_HYPERPLANE_FAN = prove (`!a b. closed_fan {x | a dot x = b}`, REPEAT GEN_TAC THEN REWRITE_TAC[GSYM REAL_LE_ANTISYM] THEN REWRITE_TAC[REAL_ARITH `b <= a dot x <=> a dot x >= b`] THEN REWRITE_TAC[SET_RULE `{x | P x /\ Q x} = {x | P x} INTER {x | Q x}`] THEN SIMP_TAC[CLOSED_INTER_FAN; CLOSED_HALFSPACE_LE_FAN; CLOSED_HALFSPACE_GE_FAN]);;