(* ========================================================================= *)
(* Some analytic concepts for R instead of R^1. *)
(* *)
(* (c) Copyright, John Harrison 1998-2008 *)
(* ========================================================================= *)
needs "Library/binomial.ml";;
needs "Multivariate/measure.ml";;
needs "Multivariate/polytope.ml";;
needs "Multivariate/transcendentals.ml";;
(* ------------------------------------------------------------------------- *)
(* Open-ness and closedness of a set of reals. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Compactness of a set of reals. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Limits of functions with real range. *)
(* ------------------------------------------------------------------------- *)
parse_as_infix("--->",(12,"right"));;
let REALLIM_UNIQUE = prove
(`!net f l l'.
~trivial_limit net /\ (f ---> l) net /\ (f ---> l') net ==> l = l'`,
let REALLIM_LMUL_EQ = prove
(`!net f l c.
~(c = &0) ==> (((\x. c * f x) ---> c * l) net <=> (f ---> l) net)`,
REPEAT STRIP_TAC THEN EQ_TAC THEN SIMP_TAC[
REALLIM_LMUL] THEN
DISCH_THEN(MP_TAC o SPEC `inv c:real` o MATCH_MP
REALLIM_LMUL) THEN
ASM_SIMP_TAC[REAL_MUL_ASSOC; REAL_MUL_LINV; REAL_MUL_LID; ETA_AX]);;
let REALLIM_ADD = prove
(`!net:(A)net f g l m.
(f ---> l) net /\ (g ---> m) net ==> ((\x. f(x) + g(x)) ---> l + m) net`,
let REALLIM_SUB = prove
(`!net:(A)net f g l m.
(f ---> l) net /\ (g ---> m) net ==> ((\x. f(x) - g(x)) ---> l - m) net`,
let REALLIM_MUL = prove
(`!net:(A)net f g l m.
(f ---> l) net /\ (g ---> m) net ==> ((\x. f(x) * g(x)) ---> l * m) net`,
let REALLIM_INV = prove
(`!net f l.
(f ---> l) net /\ ~(l = &0) ==> ((\x. inv(f x)) ---> inv l) net`,
let REALLIM_DIV = prove
(`!net:(A)net f g l m.
(f ---> l) net /\ (g ---> m) net /\ ~(m = &0)
==> ((\x. f(x) / g(x)) ---> l / m) net`,
let REALLIM_ABS = prove
(`!net f l. (f ---> l) net ==> ((\x. abs(f x)) ---> abs l) net`,
REPEAT GEN_TAC THEN REWRITE_TAC[
tendsto_real] THEN
MATCH_MP_TAC
MONO_FORALL THEN X_GEN_TAC `e:real` THEN
DISCH_THEN(fun
th -> DISCH_TAC THEN MP_TAC
th) THEN ASM_REWRITE_TAC[] THEN
MATCH_MP_TAC(REWRITE_RULE[
IMP_CONJ]
EVENTUALLY_MONO) THEN
REWRITE_TAC[] THEN REAL_ARITH_TAC);;
let REALLIM_MAX = prove
(`!net:(A)net f g l m.
(f ---> l) net /\ (g ---> m) net
==> ((\x. max (f x) (g x)) ---> max l m) net`,
let REALLIM_MIN = prove
(`!net:(A)net f g l m.
(f ---> l) net /\ (g ---> m) net
==> ((\x. min (f x) (g x)) ---> min l m) net`,
let REALLIM_NULL_ADD = prove
(`!net:(A)net f g.
(f ---> &0) net /\ (g ---> &0) net ==> ((\x. f(x) + g(x)) ---> &0) net`,
REPEAT GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP
REALLIM_ADD) THEN
REWRITE_TAC[REAL_ADD_LID]);;
let REALLIM_NULL_POW = prove
(`!net f n. (f ---> &0) net /\ ~(n = 0) ==> ((\x. f x pow n) ---> &0) net`,
REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2
(MP_TAC o SPEC `n:num` o MATCH_MP
REALLIM_POW) ASSUME_TAC) THEN
ASM_REWRITE_TAC[
REAL_POW_ZERO]);;
let REALLIM = prove
(`(f ---> l) net <=>
trivial_limit net \/
!e. &0 < e ==> ?y. (?x. netord(net) x y) /\
!x. netord(net) x y ==> abs(f(x) -l) < e`,
let REALLIM_AT = prove
(`!f l a:real^N.
(f ---> l) (
at a) <=>
!e. &0 < e
==> ?d. &0 < d /\ !x. &0 <
dist(x,a) /\
dist(x,a) < d
==> abs(f(x) - l) < e`,
let REALLIM_LE = prove
(`!net f g l m.
(f ---> l) net /\ (g ---> m) net /\
~trivial_limit net /\
eventually (\x. f x <= g x) net
==> l <= m`,
(* ------------------------------------------------------------------------- *)
(* Real series. *)
(* ------------------------------------------------------------------------- *)
parse_as_infix("real_sums",(12,"right"));;
(* ------------------------------------------------------------------------- *)
(* Similar combining theorems just for summability. *)
(* ------------------------------------------------------------------------- *)
let REAL_SUMS_FINITE_DIFF = prove
(`!f t s l.
t
SUBSET s /\ FINITE t /\ (f
real_sums l) s
==> (f
real_sums (l -
sum t f)) (s
DIFF t)`,
REPEAT GEN_TAC THEN
REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
FIRST_ASSUM(MP_TAC o ISPEC `f:num->
real` o MATCH_MP
REAL_SERIES_FINITE) THEN
ONCE_REWRITE_TAC[GSYM
REAL_SERIES_RESTRICT] THEN
REWRITE_TAC[IMP_IMP] THEN ONCE_REWRITE_TAC[
CONJ_SYM] THEN
DISCH_THEN(MP_TAC o MATCH_MP
REAL_SERIES_SUB) THEN
MATCH_MP_TAC EQ_IMP THEN AP_THM_TAC THEN AP_THM_TAC THEN AP_TERM_TAC THEN
REWRITE_TAC[
FUN_EQ_THM] THEN X_GEN_TAC `x:num` THEN REWRITE_TAC[
IN_DIFF] THEN
FIRST_ASSUM(MP_TAC o SPEC `x:num` o GEN_REWRITE_RULE I [
SUBSET]) THEN
MAP_EVERY ASM_CASES_TAC [`(x:num)
IN s`; `(x:num)
IN t`] THEN
ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);;
(* ------------------------------------------------------------------------- *)
(* Similar combining theorems for infsum. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Convergence tests for real series. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Some real limits involving transcendentals. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Nets for real limit. *)
(* ------------------------------------------------------------------------- *)
let atreal = new_definition
`atreal a = mk_net(\x y. &0 < abs(x - a) /\ abs(x - a) <= abs(y - a))`;;
let TRIVIAL_LIMIT_ATREAL = prove
(`!a. ~(
trivial_limit (
atreal a))`,
X_GEN_TAC `a:real` THEN SIMP_TAC[
trivial_limit;
ATREAL; DE_MORGAN_THM] THEN
CONJ_TAC THENL
[DISCH_THEN(MP_TAC o SPECL [`&0`; `&1`]) THEN REAL_ARITH_TAC; ALL_TAC] THEN
REWRITE_TAC[
NOT_EXISTS_THM] THEN
MAP_EVERY X_GEN_TAC [`b:real`; `c:real`] THEN
ASM_CASES_TAC `b:real = c` THEN ASM_REWRITE_TAC[] THEN
REWRITE_TAC[GSYM DE_MORGAN_THM; GSYM
NOT_EXISTS_THM] THEN
SUBGOAL_THEN `~(b:real = a) \/ ~(c = a)` DISJ_CASES_TAC THENL
[ASM_MESON_TAC[];
EXISTS_TAC `(a + b) / &2` THEN ASM_REAL_ARITH_TAC;
EXISTS_TAC `(a + c) / &2` THEN ASM_REAL_ARITH_TAC]);;
let EVENTUALLY_WITHINREAL_LE = prove
(`!s a p.
eventually p (
atreal a
within s) <=>
?d. &0 < d /\
!x. x
IN s /\ &0 < abs(x - a) /\ abs(x - a) <= d ==> p(x)`,
REWRITE_TAC[
eventually;
ATREAL;
WITHIN;
trivial_limit] THEN
REWRITE_TAC[MESON[
REAL_LT_01;
REAL_LT_REFL] `~(!a b:real. a = b)`] THEN
REPEAT GEN_TAC THEN EQ_TAC THENL
[DISCH_THEN(DISJ_CASES_THEN(X_CHOOSE_THEN `b:real` MP_TAC)) THENL
[DISCH_THEN(X_CHOOSE_THEN `c:real` STRIP_ASSUME_TAC) THEN
FIRST_X_ASSUM(DISJ_CASES_TAC o MATCH_MP (REAL_ARITH
`~(b = c) ==> &0 < abs(b - a) \/ &0 < abs(c - a)`)) THEN
ASM_MESON_TAC[];
MESON_TAC[
REAL_LTE_TRANS]];
DISCH_THEN(X_CHOOSE_THEN `d:real` STRIP_ASSUME_TAC) THEN
ASM_CASES_TAC `?x. x
IN s /\ &0 < abs(x - a) /\ abs(x - a) <= d` THENL
[DISJ2_TAC THEN FIRST_X_ASSUM(X_CHOOSE_TAC `b:real`) THEN
EXISTS_TAC `b:real` THEN ASM_MESON_TAC[
REAL_LE_TRANS;
REAL_LE_REFL];
DISJ1_TAC THEN MAP_EVERY EXISTS_TAC [`a + d:real`; `a:real`] THEN
ASM_SIMP_TAC[
REAL_ADD_SUB;
REAL_EQ_ADD_LCANCEL_0;
REAL_LT_IMP_NZ] THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [
NOT_EXISTS_THM]) THEN
MATCH_MP_TAC
MONO_FORALL THEN X_GEN_TAC `x:real` THEN
ASM_CASES_TAC `(x:real)
IN s` THEN ASM_REWRITE_TAC[] THEN
ASM_REAL_ARITH_TAC]]);;
(* ------------------------------------------------------------------------- *)
(* Usual limit results with real domain and either vector or real range. *)
(* ------------------------------------------------------------------------- *)
let LIM_ATREAL = prove
(`!f l:real^N a.
(f --> l) (
atreal a) <=>
!e. &0 < e
==> ?d. &0 < d /\ !x. &0 < abs(x - a) /\ abs(x - a) < d
==>
dist(f(x),l) < e`,
let REALLIM_ATREAL = prove
(`!f l a.
(f ---> l) (
atreal a) <=>
!e. &0 < e
==> ?d. &0 < d /\ !x. &0 < abs(x - a) /\ abs(x - a) < d
==> abs(f(x) - l) < e`,
let REALLIM_TRANSFORM_WITHIN_SET = prove
(`!f a s t.
eventually (\x. x
IN s <=> x
IN t) (
at a)
==> ((f ---> l) (
at a
within s) <=> (f ---> l) (
at a
within t))`,
REPEAT GEN_TAC THEN REWRITE_TAC[
EVENTUALLY_AT;
REALLIM_WITHIN] THEN
DISCH_THEN(X_CHOOSE_THEN `d:real` STRIP_ASSUME_TAC) THEN
EQ_TAC THEN DISCH_TAC THEN X_GEN_TAC `e:real` THEN DISCH_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPEC `e:real`) THEN ASM_REWRITE_TAC[] THEN
DISCH_THEN(X_CHOOSE_THEN `k:real` STRIP_ASSUME_TAC) THEN
EXISTS_TAC `min d k:real` THEN ASM_REWRITE_TAC[
REAL_LT_MIN] THEN
ASM_MESON_TAC[]);;
(* ------------------------------------------------------------------------- *)
(* Relations between limits at real and complex limit points. *)
(* ------------------------------------------------------------------------- *)
let TRIVIAL_LIMIT_WITHINREAL_WITHINCOMPLEX = prove
(`
trivial_limit(
atreal x
within s) <=>
trivial_limit(
at (Cx x)
within (
real INTER IMAGE Cx s))`,
REWRITE_TAC[
trivial_limit;
AT;
WITHIN;
ATREAL] THEN
REWRITE_TAC[SET_RULE `x
IN real INTER s <=>
real x /\ x
IN s`] THEN
REWRITE_TAC[TAUT `~(p /\ x /\ q) /\ ~(r /\ x /\ s) <=>
x ==> ~(p /\ q) /\ ~(r /\ s)`] THEN
REWRITE_TAC[
FORALL_REAL;
MESON[
IN_IMAGE;
CX_INJ] `Cx x
IN IMAGE Cx s <=> x
IN s`] THEN
REWRITE_TAC[
dist; GSYM
CX_SUB;
o_THM;
RE_CX;
COMPLEX_NORM_CX] THEN
MATCH_MP_TAC(TAUT `~p /\ ~q /\ (r <=> s) ==> (p \/ r <=> q \/ s)`) THEN
REPEAT CONJ_TAC THEN TRY EQ_TAC THEN REWRITE_TAC[
LEFT_IMP_EXISTS_THM] THENL
[DISCH_THEN(MP_TAC o SPECL [`&0`; `&1`]) THEN CONV_TAC REAL_RING;
DISCH_THEN(MP_TAC o SPECL [`Cx(&0)`; `Cx(&1)`]) THEN
CONV_TAC COMPLEX_RING;
MAP_EVERY X_GEN_TAC [`a:real`; `b:real`] THEN STRIP_TAC THEN
MAP_EVERY EXISTS_TAC [`Cx a`; `Cx b`] THEN ASM_REWRITE_TAC[
CX_INJ] THEN
ASM_REWRITE_TAC[GSYM
CX_SUB;
COMPLEX_NORM_CX];
MAP_EVERY X_GEN_TAC [`a:complex`; `b:complex`] THEN STRIP_TAC THEN
SUBGOAL_THEN
`?d. &0 < d /\
!z. &0 < abs(z - x) /\ abs(z - x) <= d ==> ~(z
IN s)`
STRIP_ASSUME_TAC THENL
[MATCH_MP_TAC(MESON[] `!a b. P a \/ P b ==> ?x. P x`) THEN
MAP_EVERY EXISTS_TAC [`
norm(a - Cx x)`; `
norm(b - Cx x)`] THEN
ASM_REWRITE_TAC[TAUT `a ==> ~b <=> ~(a /\ b)`] THEN
UNDISCH_TAC `~(a:complex = b)` THEN NORM_ARITH_TAC;
ALL_TAC] THEN
MAP_EVERY EXISTS_TAC [`x + d:real`; `x - d:real`] THEN
ASM_SIMP_TAC[REAL_ARITH `&0 < d ==> ~(x + d = x - d)`;
REAL_ARITH `&0 < d ==> abs((x + d) - x) = d`;
REAL_ARITH `&0 < d ==> abs(x - d - x) = d`] THEN
ASM_MESON_TAC[]]);;
(* ------------------------------------------------------------------------- *)
(* Simpler theorems relating limits in real and real^1. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Additional congruence rules for simplifying limits. *)
(* ------------------------------------------------------------------------- *)
extend_basic_congs [LIM_CONG_WITHINREAL; LIM_CONG_ATREAL];;
extend_basic_congs [REALLIM_CONG_WITHIN; REALLIM_CONG_AT];;
extend_basic_congs [REALLIM_CONG_WITHINREAL; REALLIM_CONG_ATREAL];;
(* ------------------------------------------------------------------------- *)
(* Real version of Abel limit theorem. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Continuity of a function into the reals. *)
(* ------------------------------------------------------------------------- *)
parse_as_infix ("real_continuous",(12,"right"));;
(* ------------------------------------------------------------------------- *)
(* Arithmetic combining theorems. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Some of these without netlimit, but with many different cases. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Composition of (real->real) o (real->real) functions. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Composition of (real->real) o (real^N->real) functions. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Composition of (real^N->real) o (real^M->real^N) functions. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Composition of (real^N->real) o (real->real^N) functions. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Composition of (real->real^N) o (real->real) functions. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Composition of (real^M->real^N) o (real->real^M) functions. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Composition of (real->real^N) o (real^M->real) functions. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Continuity of a real->real function on a set. *)
(* ------------------------------------------------------------------------- *)
parse_as_infix ("real_continuous_on",(12,"right"));;
(* ------------------------------------------------------------------------- *)
(* Real version of uniform continuity. *)
(* ------------------------------------------------------------------------- *)
parse_as_infix ("real_uniformly_continuous_on",(12,"right"));;
(* ------------------------------------------------------------------------- *)
(* Continuity versus componentwise continuity. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Derivative of real->real function. *)
(* ------------------------------------------------------------------------- *)
parse_as_infix ("has_real_derivative",(12,"right"));;
parse_as_infix ("real_differentiable",(12,"right"));;
parse_as_infix ("real_differentiable_on",(12,"right"));;
(* ------------------------------------------------------------------------- *)
(* Basic limit definitions in the useful cases. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Relation to Frechet derivative. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Relation to complex derivative. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Caratheodory characterization. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Property of being an interval (equivalent to convex or connected). *)
(* ------------------------------------------------------------------------- *)
let IS_REAL_INTERVAL_CASES = prove
(`!s.
is_realinterval s <=>
s = {} \/
s = (:real) \/
(?a. s = {x | a < x}) \/
(?a. s = {x | a <= x}) \/
(?b. s = {x | x <= b}) \/
(?b. s = {x | x < b}) \/
(?a b. s = {x | a < x /\ x < b}) \/
(?a b. s = {x | a < x /\ x <= b}) \/
(?a b. s = {x | a <= x /\ x < b}) \/
(?a b. s = {x | a <= x /\ x <= b})`,
(* ------------------------------------------------------------------------- *)
(* Some relations with the complex numbers can also be useful. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* The same tricks to define closed and open intervals. *)
(* ------------------------------------------------------------------------- *)
make_overloadable "real_interval" `:A`;;
overload_interface("real_interval",`open_real_interval`);;
overload_interface("real_interval",`closed_real_interval`);;
(* ------------------------------------------------------------------------- *)
(* Real continuity and differentiability. *)
(* ------------------------------------------------------------------------- *)
add_translation_invariants [REAL_CONTINUOUS_AT_TRANSLATION];;
add_linear_invariants [REAL_CONTINUOUS_AT_LINEAR_IMAGE];;
(* ------------------------------------------------------------------------- *)
(* More basics about real derivatives. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Some handy theorems about the actual differentition function. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Arithmetical combining theorems. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Same thing just for real differentiability. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Same again for being differentiable on a set. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Derivative (and continuity) theorems for real transcendental functions. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Hence differentiation of the norm. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Some somewhat sharper continuity theorems including endpoints. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Differentiation conversion. *)
(* ------------------------------------------------------------------------- *)
let real_differentiation_theorems = ref [];;
let add_real_differentiation_theorems =
add_real_differentiation_theorems
([HAS_REAL_DERIVATIVE_LMUL_WITHIN; HAS_REAL_DERIVATIVE_LMUL_ATREAL;
HAS_REAL_DERIVATIVE_RMUL_WITHIN; HAS_REAL_DERIVATIVE_RMUL_ATREAL;
HAS_REAL_DERIVATIVE_CDIV_WITHIN; HAS_REAL_DERIVATIVE_CDIV_ATREAL;
HAS_REAL_DERIVATIVE_ID;
HAS_REAL_DERIVATIVE_CONST;
HAS_REAL_DERIVATIVE_NEG;
HAS_REAL_DERIVATIVE_ADD;
HAS_REAL_DERIVATIVE_SUB;
HAS_REAL_DERIVATIVE_MUL_WITHIN; HAS_REAL_DERIVATIVE_MUL_ATREAL;
HAS_REAL_DERIVATIVE_DIV_WITHIN; HAS_REAL_DERIVATIVE_DIV_ATREAL;
HAS_REAL_DERIVATIVE_POW_WITHIN; HAS_REAL_DERIVATIVE_POW_ATREAL;
HAS_REAL_DERIVATIVE_INV_WITHIN; HAS_REAL_DERIVATIVE_INV_ATREAL] @
(CONJUNCTS(REWRITE_RULE[FORALL_AND_THM]
(MATCH_MP HAS_REAL_DERIVATIVE_CHAIN_UNIV
HAS_REAL_DERIVATIVE_EXP))) @
(CONJUNCTS(REWRITE_RULE[FORALL_AND_THM]
(MATCH_MP HAS_REAL_DERIVATIVE_CHAIN_UNIV
HAS_REAL_DERIVATIVE_SIN))) @
(CONJUNCTS(REWRITE_RULE[FORALL_AND_THM]
(MATCH_MP HAS_REAL_DERIVATIVE_CHAIN_UNIV
HAS_REAL_DERIVATIVE_COS))) @
(CONJUNCTS(REWRITE_RULE[FORALL_AND_THM]
(MATCH_MP HAS_REAL_DERIVATIVE_CHAIN
HAS_REAL_DERIVATIVE_TAN))) @
(CONJUNCTS(REWRITE_RULE[FORALL_AND_THM]
(MATCH_MP HAS_REAL_DERIVATIVE_CHAIN
HAS_REAL_DERIVATIVE_LOG))) @
(CONJUNCTS(REWRITE_RULE[FORALL_AND_THM]
(MATCH_MP HAS_REAL_DERIVATIVE_CHAIN
HAS_REAL_DERIVATIVE_SQRT))) @
(CONJUNCTS(REWRITE_RULE[FORALL_AND_THM]
(MATCH_MP HAS_REAL_DERIVATIVE_CHAIN_UNIV
HAS_REAL_DERIVATIVE_ATN))) @
(CONJUNCTS(REWRITE_RULE[FORALL_AND_THM]
(MATCH_MP HAS_REAL_DERIVATIVE_CHAIN
HAS_REAL_DERIVATIVE_ASN))) @
(CONJUNCTS(REWRITE_RULE[FORALL_AND_THM]
(MATCH_MP HAS_REAL_DERIVATIVE_CHAIN
HAS_REAL_DERIVATIVE_ACS))));;
let rec REAL_DIFF_CONV =
let partfn tm = let l,r = dest_comb tm in mk_pair(lhand l,r)
and is_deriv = can (term_match [] `(f has_real_derivative f') net`) in
let rec REAL_DIFF_CONV tm =
try tryfind (fun th -> PART_MATCH partfn th (partfn tm))
(!real_differentiation_theorems)
with Failure _ ->
let ith = tryfind (fun th ->
PART_MATCH (partfn o repeat (snd o dest_imp)) th (partfn tm))
(!real_differentiation_theorems) in
REAL_DIFF_ELIM ith
and REAL_DIFF_ELIM th =
let tm = concl th in
if not(is_imp tm) then th else
let t = lhand tm in
if not(is_deriv t) then UNDISCH th
else REAL_DIFF_ELIM (MATCH_MP th (REAL_DIFF_CONV t)) in
REAL_DIFF_CONV;;
(* ------------------------------------------------------------------------- *)
(* Hence a tactic. *)
(* ------------------------------------------------------------------------- *)
let REAL_DIFF_TAC =
let pth = MESON[]
`(f has_real_derivative f') net
==> f' = g'
==> (f has_real_derivative g') net` in
W(fun (asl,w) -> let th = MATCH_MP pth (REAL_DIFF_CONV w) in
MATCH_MP_TAC(repeat (GEN_REWRITE_RULE I [IMP_IMP]) (DISCH_ALL th)));;
let REAL_DIFFERENTIABLE_TAC =
let DISCH_FIRST th = DISCH (hd(hyp th)) th in
GEN_REWRITE_TAC I [real_differentiable] THEN
W(fun (asl,w) ->
let th = REAL_DIFF_CONV(snd(dest_exists w)) in
let f' = rand(rator(concl th)) in
EXISTS_TAC f' THEN
(if hyp th = [] then MATCH_ACCEPT_TAC th else
let th' = repeat (GEN_REWRITE_RULE I [IMP_IMP] o DISCH_FIRST)
(DISCH_FIRST th) in
MATCH_MP_TAC th'));;
(* ------------------------------------------------------------------------- *)
(* Analytic results for real power function. *)
(* ------------------------------------------------------------------------- *)
add_real_differentiation_theorems
(CONJUNCTS(REWRITE_RULE[FORALL_AND_THM]
(GEN `y:real` (MATCH_MP HAS_REAL_DERIVATIVE_CHAIN
(SPEC `y:real`
(ONCE_REWRITE_RULE[SWAP_FORALL_THM] HAS_REAL_DERIVATIVE_RPOW))))));;
let REAL_DIFFERENTIABLE_AT_RPOW = prove
(`!x y. ~(x = &0) ==> (\x. x
rpow y)
real_differentiable atreal x`,
REPEAT GEN_TAC THEN
REWRITE_TAC[REAL_ARITH `~(x = &0) <=> &0 < x \/ &0 < --x`] THEN
STRIP_TAC THEN MATCH_MP_TAC
REAL_DIFFERENTIABLE_TRANSFORM_ATREAL THEN
REWRITE_TAC[] THEN ONCE_REWRITE_TAC[
SWAP_EXISTS_THM] THEN
EXISTS_TAC `abs x` THENL
[EXISTS_TAC `\x.
exp(y * log x)` THEN
ASM_SIMP_TAC[REAL_ARITH `&0 < x ==> &0 < abs x`] THEN CONJ_TAC THENL
[X_GEN_TAC `z:real` THEN DISCH_TAC THEN
SUBGOAL_THEN `&0 < z` (fun
th -> REWRITE_TAC[
rpow;
th]) THEN
ASM_REAL_ARITH_TAC;
REAL_DIFFERENTIABLE_TAC THEN ASM_REAL_ARITH_TAC];
ASM_CASES_TAC `?m n.
ODD m /\
ODD n /\ abs y = &m / &n` THENL
[EXISTS_TAC `\x. --(
exp(y * log(--x)))`;
EXISTS_TAC `\x.
exp(y * log(--x))`] THEN
(ASM_SIMP_TAC[REAL_ARITH `&0 < --x ==> &0 < abs x`] THEN CONJ_TAC THENL
[X_GEN_TAC `z:real` THEN DISCH_TAC THEN
SUBGOAL_THEN `~(&0 < z) /\ ~(z = &0)`
(fun
th -> ASM_REWRITE_TAC[
rpow;
th]) THEN
ASM_REAL_ARITH_TAC;
REAL_DIFFERENTIABLE_TAC THEN ASM_REAL_ARITH_TAC])]);;
(* ------------------------------------------------------------------------- *)
(* Intermediate Value Theorem. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Zeroness (or sign at boundary) of derivative at local extremum. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Rolle and Mean Value Theorem. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Cauchy MVT and l'Hospital's rule. *)
(* ------------------------------------------------------------------------- *)
let LHOSPITAL = prove
(`!f g f' g' c l d.
&0 < d /\
(!x. &0 < abs(x - c) /\ abs(x - c) < d
==> (f
has_real_derivative f'(x)) (
atreal x) /\
(g
has_real_derivative g'(x)) (
atreal x) /\
~(g'(x) = &0)) /\
(f ---> &0) (
atreal c) /\ (g ---> &0) (
atreal c) /\
((\x. f'(x) / g'(x)) ---> l) (
atreal c)
==> ((\x. f(x) / g(x)) ---> l) (
atreal c)`,
SUBGOAL_THEN
`!f g f' g' c l d.
&0 < d /\
(!x. &0 < abs(x - c) /\ abs(x - c) < d
==> (f
has_real_derivative f'(x)) (
atreal x) /\
(g
has_real_derivative g'(x)) (
atreal x) /\
~(g'(x) = &0)) /\
f(c) = &0 /\ g(c) = &0 /\
(f ---> &0) (
atreal c) /\ (g ---> &0) (
atreal c) /\
((\x. f'(x) / g'(x)) ---> l) (
atreal c)
==> ((\x. f(x) / g(x)) ---> l) (
atreal c)`
ASSUME_TAC THENL
[REWRITE_TAC[TAUT `a ==> b /\ c <=> (a ==> b) /\ (a ==> c)`] THEN
REWRITE_TAC[
FORALL_AND_THM] THEN REPEAT STRIP_TAC THEN
SUBGOAL_THEN
`(!x. abs(x - c) < d ==> f
real_continuous atreal x) /\
(!x. abs(x - c) < d ==> g
real_continuous atreal x)`
STRIP_ASSUME_TAC THENL
[REWRITE_TAC[
AND_FORALL_THM] THEN X_GEN_TAC `x:real` THEN
DISJ_CASES_TAC(REAL_ARITH `x = c \/ &0 < abs(x - c)`) THENL
[ASM_REWRITE_TAC[
REAL_CONTINUOUS_ATREAL]; ALL_TAC] THEN
REPEAT STRIP_TAC THEN
MATCH_MP_TAC
REAL_DIFFERENTIABLE_IMP_CONTINUOUS_ATREAL THEN
REWRITE_TAC[
real_differentiable] THEN ASM_MESON_TAC[];
ALL_TAC] THEN
SUBGOAL_THEN
`!x. &0 < abs(x - c) /\ abs(x - c) < d ==> ~(g x = &0)`
STRIP_ASSUME_TAC THENL
[REPEAT STRIP_TAC THEN
SUBGOAL_THEN `c < x \/ x < c` DISJ_CASES_TAC THENL
[ASM_REAL_ARITH_TAC;
MP_TAC(ISPECL [`g:real->
real`; `g':real->
real`; `c:real`; `x:real`]
REAL_ROLLE);
MP_TAC(ISPECL [`g:real->
real`; `g':real->
real`; `x:real`; `c:real`]
REAL_ROLLE)] THEN
ASM_REWRITE_TAC[NOT_IMP;
NOT_EXISTS_THM] THEN
(REPEAT CONJ_TAC THENL
[REWRITE_TAC[
REAL_CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN] THEN
REWRITE_TAC[
IN_REAL_INTERVAL] THEN REPEAT STRIP_TAC THEN
MATCH_MP_TAC
REAL_CONTINUOUS_ATREAL_WITHINREAL;
REWRITE_TAC[
IN_REAL_INTERVAL] THEN REPEAT STRIP_TAC;
X_GEN_TAC `y:real` THEN REWRITE_TAC[
IN_REAL_INTERVAL] THEN
DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
REWRITE_TAC[]] THEN
FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REAL_ARITH_TAC);
ALL_TAC] THEN
UNDISCH_TAC `((\x. f' x / g' x) ---> l) (
atreal c)` THEN
REWRITE_TAC[
REALLIM_ATREAL] THEN MATCH_MP_TAC
MONO_FORALL THEN
X_GEN_TAC `e:real` THEN ASM_CASES_TAC `&0 < e` THEN ASM_REWRITE_TAC[] THEN
DISCH_THEN(X_CHOOSE_THEN `k:real` STRIP_ASSUME_TAC) THEN
EXISTS_TAC `min d k:real` THEN ASM_REWRITE_TAC[
REAL_LT_MIN] THEN
X_GEN_TAC `x:real` THEN STRIP_TAC THEN
SUBGOAL_THEN
`?y. &0 < abs(y - c) /\ abs(y - c) < abs(x - c) /\
(f:real->
real) x / g x = f' y / g' y`
STRIP_ASSUME_TAC THENL
[ALL_TAC; ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[
REAL_LT_TRANS]] THEN
SUBGOAL_THEN `c < x \/ x < c` DISJ_CASES_TAC THENL
[ASM_REAL_ARITH_TAC;
MP_TAC(ISPECL
[`f:real->
real`; `g:real->
real`; `f':real->
real`; `g':real->
real`;
`c:real`; `x:real`]
REAL_MVT_CAUCHY);
MP_TAC(ISPECL
[`f:real->
real`; `g:real->
real`; `f':real->
real`; `g':real->
real`;
`x:real`; `c:real`]
REAL_MVT_CAUCHY)] THEN
(ASM_REWRITE_TAC[
IN_REAL_INTERVAL] THEN ANTS_TAC THENL
[REWRITE_TAC[
CONJ_ASSOC] THEN CONJ_TAC THENL
[CONJ_TAC THEN
REWRITE_TAC[
REAL_CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN] THEN
REWRITE_TAC[
IN_REAL_INTERVAL] THEN REPEAT STRIP_TAC THEN
MATCH_MP_TAC
REAL_CONTINUOUS_ATREAL_WITHINREAL;
REPEAT STRIP_TAC] THEN
FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REAL_ARITH_TAC;
MATCH_MP_TAC
MONO_EXISTS THEN REWRITE_TAC[
REAL_SUB_RZERO] THEN
GEN_TAC THEN STRIP_TAC THEN
REPEAT(CONJ_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC]) THEN
MATCH_MP_TAC(REAL_FIELD
`f * g' = g * f' /\ ~(g = &0) /\ ~(g' = &0) ==> f / g = f' / g'`) THEN
CONJ_TAC THENL [ASM_REAL_ARITH_TAC; CONJ_TAC] THEN
FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REAL_ARITH_TAC]);
REPEAT GEN_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPECL
[`\x:real. if x = c then &0 else f(x)`;
`\x:real. if x = c then &0 else g(x)`;
`f':real->
real`; `g':real->
real`;
`c:real`; `l:real`; `d:real`]) THEN
REWRITE_TAC[] THEN MATCH_MP_TAC MONO_IMP THEN CONJ_TAC THEN
REPEAT(MATCH_MP_TAC MONO_AND THEN CONJ_TAC) THEN
TRY(SIMP_TAC[
REALLIM_ATREAL;REAL_ARITH `&0 < abs(x - c) ==> ~(x = c)`] THEN
NO_TAC) THEN
DISCH_TAC THEN X_GEN_TAC `x:real` THEN STRIP_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPEC `x:real`) THEN ASM_REWRITE_TAC[] THEN
REPEAT(MATCH_MP_TAC MONO_AND THEN CONJ_TAC) THEN REWRITE_TAC[] THEN
MATCH_MP_TAC(REWRITE_RULE[TAUT `a /\ b /\ c ==> d <=> a /\ b ==> c ==> d`]
HAS_REAL_DERIVATIVE_TRANSFORM_ATREAL) THEN
EXISTS_TAC `abs(x - c)` THEN ASM_REAL_ARITH_TAC]);;
(* ------------------------------------------------------------------------- *)
(* Darboux's theorem (intermediate value property for derivatives). *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Continuity and differentiability of inverse functions. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Real differentiation of sequences and series. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Comparing sums and "integrals" via real antiderivatives. *)
(* ------------------------------------------------------------------------- *)
let REAL_SUM_INTEGRAL_UBOUND_DECREASING = prove
(`!f g m n.
m <= n /\
(!x. x
IN real_interval[&m - &1,&n]
==> (g
has_real_derivative f(x))
(
atreal x
within real_interval[&m - &1,&n])) /\
(!x y. &m - &1 <= x /\ x <= y /\ y <= &n ==> f y <= f x)
==>
sum(m..n) (\k. f(&k)) <= g(&n) - g(&m - &1)`,
REPEAT STRIP_TAC THEN MATCH_MP_TAC
REAL_LE_TRANS THEN
EXISTS_TAC `
sum(m..n) (\k. g(&(k + 1) - &1) - g(&k - &1))` THEN
CONJ_TAC THENL
[ALL_TAC;
ASM_REWRITE_TAC[
SUM_DIFFS_ALT] THEN
ASM_REWRITE_TAC[GSYM REAL_OF_NUM_ADD; REAL_ARITH `(x + &1) - &1 = x`] THEN
REWRITE_TAC[
REAL_LE_REFL]] THEN
MATCH_MP_TAC
SUM_LE_NUMSEG THEN X_GEN_TAC `k:num` THEN STRIP_TAC THEN
MP_TAC(ISPECL [`g:real->
real`; `f:real->
real`; `&k - &1`; `&k`]
REAL_MVT_SIMPLE) THEN
ASM_REWRITE_TAC[REAL_ARITH `k - &1 < k`] THEN ANTS_TAC THENL
[REPEAT STRIP_TAC THEN MATCH_MP_TAC
HAS_REAL_DERIVATIVE_WITHIN_SUBSET THEN
EXISTS_TAC `
real_interval[&m - &1,&n]` THEN CONJ_TAC THENL
[FIRST_X_ASSUM MATCH_MP_TAC THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [
IN_REAL_INTERVAL]);
REWRITE_TAC[
SUBSET] THEN GEN_TAC] THEN
REWRITE_TAC[
IN_REAL_INTERVAL] THEN
RULE_ASSUM_TAC(REWRITE_RULE[GSYM REAL_OF_NUM_LE]) THEN ASM_REAL_ARITH_TAC;
REWRITE_TAC[GSYM REAL_OF_NUM_ADD; REAL_ARITH `(a + &1) - &1 = a`] THEN
DISCH_THEN(X_CHOOSE_THEN `t:real`
(CONJUNCTS_THEN2 ASSUME_TAC SUBST1_TAC)) THEN
REWRITE_TAC[REAL_ARITH `a * (x - (x - &1)) = a`] THEN
FIRST_X_ASSUM MATCH_MP_TAC THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [
IN_REAL_INTERVAL]) THEN
RULE_ASSUM_TAC(REWRITE_RULE[GSYM REAL_OF_NUM_LE]) THEN
ASM_REAL_ARITH_TAC]);;
(* ------------------------------------------------------------------------- *)
(* Relating different kinds of real limits. *)
(* ------------------------------------------------------------------------- *)
let LIM_ZERO_POSINFINITY = prove
(`!f l. ((\x. f(&1 / x)) --> l) (
atreal (&0)) ==> (f --> l)
at_posinfinity`,
REPEAT GEN_TAC THEN REWRITE_TAC[
LIM_ATREAL;
LIM_AT_POSINFINITY] THEN
DISCH_TAC THEN X_GEN_TAC `e:real` THEN DISCH_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPEC `e:real`) THEN ASM_REWRITE_TAC[] THEN
REWRITE_TAC[
dist;
REAL_SUB_RZERO;
real_ge] THEN
DISCH_THEN(X_CHOOSE_THEN `d:real` STRIP_ASSUME_TAC) THEN
EXISTS_TAC `&2 / d` THEN X_GEN_TAC `z:real` THEN DISCH_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPEC `inv(z):real`) THEN
REWRITE_TAC[
real_div; REAL_MUL_LINV;
REAL_INV_INV] THEN
REWRITE_TAC[REAL_MUL_LID] THEN DISCH_THEN MATCH_MP_TAC THEN
ASM_REWRITE_TAC[
REAL_ABS_INV;
REAL_LT_INV_EQ] THEN CONJ_TAC THENL
[FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH
`a <= z ==> &0 < a ==> &0 < abs z`));
GEN_REWRITE_TAC RAND_CONV [GSYM
REAL_INV_INV] THEN
MATCH_MP_TAC
REAL_LT_INV2 THEN ASM_REWRITE_TAC[
REAL_LT_INV_EQ] THEN
FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH
`&2 / d <= z ==> &0 < &2 / d ==> inv d < abs z`))] THEN
ASM_SIMP_TAC[
REAL_LT_DIV;
REAL_OF_NUM_LT; ARITH]);;
let LIM_ZERO_NEGINFINITY = prove
(`!f l. ((\x. f(&1 / x)) --> l) (
atreal (&0)) ==> (f --> l)
at_neginfinity`,
REPEAT GEN_TAC THEN REWRITE_TAC[
LIM_ATREAL;
LIM_AT_NEGINFINITY] THEN
DISCH_TAC THEN X_GEN_TAC `e:real` THEN DISCH_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPEC `e:real`) THEN ASM_REWRITE_TAC[] THEN
REWRITE_TAC[
dist;
REAL_SUB_RZERO;
real_ge] THEN
DISCH_THEN(X_CHOOSE_THEN `d:real` STRIP_ASSUME_TAC) THEN
EXISTS_TAC `--(&2 / d)` THEN X_GEN_TAC `z:real` THEN DISCH_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPEC `inv(z):real`) THEN
REWRITE_TAC[
real_div; REAL_MUL_LINV;
REAL_INV_INV] THEN
REWRITE_TAC[REAL_MUL_LID] THEN DISCH_THEN MATCH_MP_TAC THEN
ASM_REWRITE_TAC[
REAL_ABS_INV;
REAL_LT_INV_EQ] THEN CONJ_TAC THENL
[FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH
`z <= --a ==> &0 < a ==> &0 < abs z`));
GEN_REWRITE_TAC RAND_CONV [GSYM
REAL_INV_INV] THEN
MATCH_MP_TAC
REAL_LT_INV2 THEN ASM_REWRITE_TAC[
REAL_LT_INV_EQ] THEN
FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH
`z <= --(&2 / d) ==> &0 < &2 / d ==> inv d < abs z`))] THEN
ASM_SIMP_TAC[
REAL_LT_DIV;
REAL_OF_NUM_LT; ARITH]);;
(* ------------------------------------------------------------------------- *)
(* Real segments (bidirectional intervals). *)
(* ------------------------------------------------------------------------- *)
make_overloadable "real_segment" `:A`;;
overload_interface("real_segment",`open_real_segment`);;
overload_interface("real_segment",`closed_real_segment`);;
(* ------------------------------------------------------------------------- *)
(* Convex real->real functions. *)
(* ------------------------------------------------------------------------- *)
parse_as_infix ("real_convex_on",(12,"right"));;
(* ------------------------------------------------------------------------- *)
(* A couple of simple bounds that it's convenient to get this way. *)
(* ------------------------------------------------------------------------- *)
let REAL_LE_ABS_SINH = prove
(`!x. abs x <= abs((
exp x - inv(
exp x)) / &2)`,
GEN_TAC THEN ASM_CASES_TAC `&0 <= x` THENL
[MATCH_MP_TAC(REAL_ARITH `&0 <= x /\ x <= y ==> abs x <= abs y`) THEN
ASM_SIMP_TAC[
REAL_LE_X_SINH];
MATCH_MP_TAC(REAL_ARITH `~(&0 <= x) /\ --x <= --y ==> abs x <= abs y`) THEN
ASM_REWRITE_TAC[REAL_ARITH `--((a - b) / &2) = (b - a) / &2`] THEN
MATCH_MP_TAC
REAL_LE_TRANS THEN
EXISTS_TAC `(
exp(--x) - inv(
exp(--x))) / &2` THEN
ASM_SIMP_TAC[
REAL_LE_X_SINH; REAL_ARITH `~(&0 <= x) ==> &0 <= --x`] THEN
REWRITE_TAC[
REAL_EXP_NEG;
REAL_INV_INV] THEN REAL_ARITH_TAC]);;
(* ------------------------------------------------------------------------- *)
(* Integrals of real->real functions; measures of real sets. *)
(* ------------------------------------------------------------------------- *)
parse_as_infix("has_real_integral",(12,"right"));;
parse_as_infix("real_integrable_on",(12,"right"));;
parse_as_infix("absolutely_real_integrable_on",(12,"right"));;
parse_as_infix("has_real_measure",(12,"right"));;
(* ------------------------------------------------------------------------- *)
(* Drop the k'th coordinate, or insert t at the k'th coordinate. *)
(* ------------------------------------------------------------------------- *)
let dropout = new_definition
`(dropout:num->real^N->real^M) k x =
lambda i. if i < k then x$i else x$(i + 1)`;;
let pushin = new_definition
`pushin k t x = lambda i. if i < k then x$i
else if i = k then t
else x$(i - 1)`;;
let PUSHIN_DROPOUT = prove
(`!k x.
dimindex(:M) + 1 =
dimindex(:N) /\ 1 <= k /\ k <=
dimindex(:N)
==>
pushin k (x$k) ((
dropout k:real^N->real^M) x) = x`,
REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN(ASSUME_TAC o GSYM)) THEN
ASM_SIMP_TAC[
CART_EQ;
dropout;
pushin;
LAMBDA_BETA;
ARITH_RULE `i <= n + 1 ==> i - 1 <= n`] THEN
X_GEN_TAC `i:num` THEN STRIP_TAC THEN
ASM_CASES_TAC `i:num = k` THEN ASM_REWRITE_TAC[
LT_REFL] THEN
FIRST_X_ASSUM(DISJ_CASES_TAC o MATCH_MP (ARITH_RULE
`~(i:num = k) ==> i < k \/ k < i`)) THEN
ASM_SIMP_TAC[ARITH_RULE `i:num < k ==> ~(k < i)`] THEN
W(MP_TAC o PART_MATCH (lhs o rand)
LAMBDA_BETA o lhand o snd) THEN
(ANTS_TAC THENL [ASM_ARITH_TAC; DISCH_THEN SUBST1_TAC]) THEN
ASM_SIMP_TAC[ARITH_RULE `k < i ==> ~(i - 1 < k)`] THEN
AP_TERM_TAC THEN ASM_ARITH_TAC);;
let CLOSED_INTERVAL_DROPOUT = prove
(`!k a b.
dimindex(:M) + 1 =
dimindex(:N) /\
1 <= k /\ k <=
dimindex(:N) /\
a$k <= b$k
==>
interval[
dropout k a,
dropout k b] =
IMAGE (
dropout k:real^N->real^M) (
interval[a,b])`,
REPEAT STRIP_TAC THEN
ASM_SIMP_TAC[
EXTENSION;
IN_IMAGE_DROPOUT;
IN_INTERVAL] THEN
X_GEN_TAC `x:real^M` THEN
SIMP_TAC[
pushin;
dropout;
LAMBDA_BETA] THEN EQ_TAC THENL
[DISCH_TAC THEN EXISTS_TAC `(a:real^N)$k` THEN X_GEN_TAC `i:num` THEN
STRIP_TAC THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[] THENL
[FIRST_X_ASSUM(MP_TAC o SPEC `i:num`) THEN ASM_REWRITE_TAC[] THEN
DISCH_THEN MATCH_MP_TAC THEN ASM_ARITH_TAC;
COND_CASES_TAC THEN ASM_REWRITE_TAC[
REAL_LE_REFL] THEN
FIRST_X_ASSUM(MP_TAC o SPEC `i - 1`) THEN
COND_CASES_TAC THENL [ASM_ARITH_TAC; ASM_REWRITE_TAC[]] THEN
ANTS_TAC THENL [ASM_ARITH_TAC; ASM_SIMP_TAC[
SUB_ADD]]];
DISCH_THEN(X_CHOOSE_TAC `t:real`) THEN X_GEN_TAC `i:num` THEN
STRIP_TAC THEN COND_CASES_TAC THENL
[FIRST_X_ASSUM(MP_TAC o SPEC `i:num`) THEN ASM_REWRITE_TAC[] THEN
DISCH_THEN MATCH_MP_TAC THEN ASM_ARITH_TAC;
FIRST_X_ASSUM(MP_TAC o SPEC `i + 1`) THEN
ASM_REWRITE_TAC[] THEN ANTS_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN
COND_CASES_TAC THEN ASM_REWRITE_TAC[] THENL [ASM_ARITH_TAC; ALL_TAC] THEN
COND_CASES_TAC THEN ASM_REWRITE_TAC[] THENL [ASM_ARITH_TAC; ALL_TAC] THEN
ASM_REWRITE_TAC[
ADD_SUB]]]);;
let DROPOUT_EQ = prove
(`!x y k.
dimindex(:M) + 1 =
dimindex(:N) /\ 1 <= k /\ k <=
dimindex(:N) /\
x$k = y$k /\ (
dropout k:real^N->real^M) x =
dropout k y
==> x = y`,
SIMP_TAC[
CART_EQ;
dropout;
VEC_COMPONENT;
LAMBDA_BETA;
IN_ELIM_THM] THEN
MAP_EVERY X_GEN_TAC [`x:real^N`; `y:real^N`; `k:num`] THEN
STRIP_TAC THEN X_GEN_TAC `i:num` THEN STRIP_TAC THEN
ASM_CASES_TAC `i:num = k` THEN ASM_REWRITE_TAC[] THEN
FIRST_ASSUM(DISJ_CASES_TAC o MATCH_MP (ARITH_RULE
`~(i:num = k) ==> i < k \/ k < i`))
THENL
[FIRST_X_ASSUM(MP_TAC o SPEC `i:num`) THEN ASM_SIMP_TAC[];
FIRST_X_ASSUM(MP_TAC o SPEC `i - 1`) THEN
ASM_SIMP_TAC[
SUB_ADD; ARITH_RULE `k < i ==> ~(i - 1 < k)`]] THEN
DISCH_THEN MATCH_MP_TAC THEN ASM_ARITH_TAC);;
(* ------------------------------------------------------------------------- *)
(* Take slice of set s at x$k = t and drop the k'th coordinate. *)
(* ------------------------------------------------------------------------- *)
let INTERVAL_INTER_HYPERPLANE = prove
(`!k t a b:real^N.
1 <= k /\ k <=
dimindex(:N)
==>
interval[a,b]
INTER {x | x$k = t} =
if a$k <= t /\ t <= b$k
then
interval[(
lambda i. if i = k then t else a$i),
(
lambda i. if i = k then t else b$i)]
else {}`,
REPEAT STRIP_TAC THEN
REWRITE_TAC[
EXTENSION;
IN_INTER;
IN_INTERVAL;
IN_ELIM_THM] THEN
X_GEN_TAC `x:real^N` THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[] THENL
[ALL_TAC; ASM_MESON_TAC[
NOT_IN_EMPTY]] THEN
SIMP_TAC[
IN_INTERVAL;
LAMBDA_BETA] THEN
EQ_TAC THEN STRIP_TAC THENL [ASM_MESON_TAC[REAL_LE_ANTISYM]; ALL_TAC] THEN
CONJ_TAC THENL [ALL_TAC; ASM_MESON_TAC[REAL_LE_ANTISYM]] THEN
X_GEN_TAC `i:num` THEN STRIP_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPEC `i:num`) THEN ASM_REWRITE_TAC[] THEN
COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN ASM_REAL_ARITH_TAC);;
(* ------------------------------------------------------------------------- *)
(* Weak but useful versions of Fubini's theorem. *)
(* ------------------------------------------------------------------------- *)
let FUBINI_SIMPLE_LEMMA = prove
(`!k s:real^N->bool e.
&0 < e /\
dimindex(:M) + 1 =
dimindex(:N) /\
1 <= k /\ k <=
dimindex(:N) /\
bounded s /\
measurable s /\
(!t.
measurable(
slice k t s:real^M->bool)) /\
(\t.
measure (
slice k t s:real^M->bool))
real_integrable_on (:real)
==>
real_integral(:real) (\t.
measure (
slice k t s :real^M->bool))
<=
measure s + e`,
REPEAT STRIP_TAC THEN
FIRST_ASSUM(MP_TAC o MATCH_MP
BOUNDED_SUBSET_CLOSED_INTERVAL) THEN
REWRITE_TAC[
LEFT_IMP_EXISTS_THM] THEN
MAP_EVERY X_GEN_TAC [`a:real^N`; `b:real^N`] THEN DISCH_TAC THEN
MP_TAC(ISPECL [`s:real^N->bool`; `a:real^N`; `b:real^N`; `e:real`]
MEASURABLE_OUTER_INTERVALS_BOUNDED_EXPLICIT_SPECIAL) THEN
ASM_REWRITE_TAC[] THEN ANTS_TAC THENL
[SUBGOAL_THEN `1 <=
dimindex(:M)` MP_TAC THENL
[REWRITE_TAC[
DIMINDEX_GE_1]; ASM_ARITH_TAC];
ALL_TAC] THEN
DISCH_THEN(X_CHOOSE_THEN `d:num->(real^N->bool)` STRIP_ASSUME_TAC) THEN
SUBGOAL_THEN `!t n:num.
measurable((
slice k t:(real^N->bool)->real^M->bool)
(d n))`
ASSUME_TAC THENL
[MAP_EVERY X_GEN_TAC [`t:real`; `n:num`] THEN
FIRST_X_ASSUM(STRIP_ASSUME_TAC o CONJUNCT2 o SPEC `n:num`) THEN
ASM_SIMP_TAC[
SLICE_INTERVAL] THEN
MESON_TAC[
MEASURABLE_EMPTY;
MEASURABLE_INTERVAL];
ALL_TAC] THEN
MATCH_MP_TAC
REAL_LE_TRANS THEN
EXISTS_TAC `
measure(
UNIONS {d n | n
IN (:num)}:real^N->bool)` THEN
ASM_REWRITE_TAC[] THEN
MP_TAC(ISPECL
[`\n t.
sum(0..n)
(\m.
measure((
slice k t:(real^N->bool)->real^M->bool)
(d m)))`;
`\t.
measure((
slice k t:(real^N->bool)->real^M->bool)
(
UNIONS {d n | n
IN (:num)}))`; `(:real)`]
REAL_MONOTONE_CONVERGENCE_INCREASING_AE) THEN
REWRITE_TAC[] THEN ANTS_TAC THENL
[CONJ_TAC THENL
[X_GEN_TAC `i:num` THEN MATCH_MP_TAC
REAL_INTEGRABLE_SUM THEN
ASM_REWRITE_TAC[
FINITE_NUMSEG] THEN X_GEN_TAC `j:num` THEN
DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o CONJUNCT2 o SPEC `j:num`) THEN
REWRITE_TAC[
LEFT_IMP_EXISTS_THM] THEN
MAP_EVERY X_GEN_TAC [`u:real^N`; `v:real^N`] THEN STRIP_TAC THEN
MP_TAC(ISPECL [`k:num`; `u:real^N`; `v:real^N`]
FUBINI_CLOSED_INTERVAL) THEN
ASM_REWRITE_TAC[] THEN MESON_TAC[
real_integrable_on];
ALL_TAC] THEN
CONJ_TAC THENL
[REPEAT STRIP_TAC THEN REWRITE_TAC[
SUM_CLAUSES_NUMSEG;
LE_0] THEN
REWRITE_TAC[
REAL_LE_ADDR] THEN MATCH_MP_TAC
MEASURE_POS_LE THEN
ASM_REWRITE_TAC[];
ALL_TAC] THEN
CONJ_TAC THENL
[ALL_TAC;
REWRITE_TAC[
real_bounded;
FORALL_IN_GSPEC;
IN_UNIV] THEN
EXISTS_TAC `
measure(
interval[a:real^N,b])` THEN X_GEN_TAC `i:num` THEN
W(MP_TAC o PART_MATCH (lhand o rand)
REAL_INTEGRAL_SUM o
rand o lhand o snd) THEN
ANTS_TAC THENL
[REWRITE_TAC[
FINITE_NUMSEG] THEN X_GEN_TAC `j:num` THEN DISCH_TAC THEN
SUBGOAL_THEN `?u v. u$k <= v$k /\
(d:num->real^N->bool) j =
interval[u,v]`
STRIP_ASSUME_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
ASM_REWRITE_TAC[] THEN REWRITE_TAC[
real_integrable_on] THEN
EXISTS_TAC `
measure(
interval[u:real^N,v])` THEN
MATCH_MP_TAC
FUBINI_CLOSED_INTERVAL THEN ASM_REWRITE_TAC[];
ALL_TAC] THEN
DISCH_THEN SUBST1_TAC THEN MATCH_MP_TAC
REAL_LE_TRANS THEN
EXISTS_TAC `abs(
sum(0..i) (\m.
measure(d m:real^N->bool)))` THEN
CONJ_TAC THENL
[MATCH_MP_TAC
REAL_EQ_IMP_LE THEN AP_TERM_TAC THEN
MATCH_MP_TAC
SUM_EQ_NUMSEG THEN
X_GEN_TAC `j:num` THEN STRIP_TAC THEN REWRITE_TAC[] THEN
MATCH_MP_TAC
REAL_INTEGRAL_UNIQUE THEN
SUBGOAL_THEN `?u v. u$k <= v$k /\
(d:num->real^N->bool) j =
interval[u,v]`
STRIP_ASSUME_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
ASM_REWRITE_TAC[] THEN
MATCH_MP_TAC
FUBINI_CLOSED_INTERVAL THEN ASM_REWRITE_TAC[];
ALL_TAC] THEN
MATCH_MP_TAC(REAL_ARITH `&0 <= x /\ x <= a ==> abs x <= a`) THEN
CONJ_TAC THENL
[MATCH_MP_TAC
SUM_POS_LE THEN REWRITE_TAC[
FINITE_NUMSEG] THEN
ASM_MESON_TAC[
MEASURE_POS_LE;
MEASURABLE_INTERVAL];
ALL_TAC] THEN
W(MP_TAC o PART_MATCH (rhs o rand)
MEASURE_NEGLIGIBLE_UNIONS_IMAGE o
lhand o snd) THEN
ANTS_TAC THENL
[ASM_SIMP_TAC[
FINITE_NUMSEG] THEN ASM_MESON_TAC[
MEASURABLE_INTERVAL];
ALL_TAC] THEN
DISCH_THEN(SUBST1_TAC o SYM) THEN MATCH_MP_TAC
MEASURE_SUBSET THEN
REWRITE_TAC[
MEASURABLE_INTERVAL] THEN CONJ_TAC THENL
[MATCH_MP_TAC
MEASURABLE_UNIONS THEN
ASM_SIMP_TAC[
FINITE_NUMSEG;
FINITE_IMAGE;
FORALL_IN_IMAGE] THEN
ASM_MESON_TAC[
MEASURABLE_INTERVAL];
REWRITE_TAC[
UNIONS_SUBSET;
FORALL_IN_IMAGE] THEN ASM_MESON_TAC[]]] THEN
EXISTS_TAC
`(
IMAGE (\i. (
interval_lowerbound(d i):real^N)$k) (:num))
UNION
(
IMAGE (\i. (
interval_upperbound(d i):real^N)$k) (:num))` THEN
CONJ_TAC THENL
[MATCH_MP_TAC
REAL_NEGLIGIBLE_COUNTABLE THEN
SIMP_TAC[
COUNTABLE_UNION;
COUNTABLE_IMAGE;
NUM_COUNTABLE];
ALL_TAC] THEN
X_GEN_TAC `t:real` THEN
REWRITE_TAC[
IN_DIFF;
IN_UNION;
IN_IMAGE] THEN
GEN_REWRITE_TAC (LAND_CONV o TOP_DEPTH_CONV) [
IN_UNIV] THEN
REWRITE_TAC[DE_MORGAN_THM;
NOT_EXISTS_THM] THEN DISCH_TAC THEN
MP_TAC(ISPEC `\n:num. (
slice k t:(real^N->bool)->real^M->bool)
(d n)`
HAS_MEASURE_COUNTABLE_NEGLIGIBLE_UNIONS_BOUNDED) THEN
ASM_REWRITE_TAC[
SLICE_UNIONS] THEN ANTS_TAC THENL
[ALL_TAC;
DISCH_THEN(MP_TAC o CONJUNCT2) THEN
GEN_REWRITE_TAC (LAND_CONV o RATOR_CONV o LAND_CONV) [GSYM
o_DEF] THEN
REWRITE_TAC[GSYM
REAL_SUMS;
real_sums;
FROM_INTER_NUMSEG] THEN
REWRITE_TAC[
SIMPLE_IMAGE; GSYM
IMAGE_o;
o_DEF]] THEN
CONJ_TAC THENL
[ALL_TAC;
MATCH_MP_TAC
BOUNDED_SUBSET THEN
EXISTS_TAC `(
slice k t:(real^N->bool)->real^M->bool) (
interval[a,b])` THEN
CONJ_TAC THENL
[ASM_SIMP_TAC[
SLICE_INTERVAL] THEN
MESON_TAC[
BOUNDED_INTERVAL;
BOUNDED_EMPTY];
REWRITE_TAC[
UNIONS_SUBSET;
FORALL_IN_GSPEC] THEN
ASM_MESON_TAC[
SLICE_SUBSET]]] THEN
MAP_EVERY X_GEN_TAC [`i:num`; `j:num`] THEN DISCH_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPECL [`i:num`; `j:num`]) THEN
ASM_REWRITE_TAC[] THEN
ASM_CASES_TAC `(d:num->real^N->bool) i = {}` THENL
[ASM_REWRITE_TAC[
INTER_EMPTY;
NEGLIGIBLE_EMPTY;
SLICE_EMPTY];
UNDISCH_TAC `~((d:num->real^N->bool) i = {})`] THEN
ASM_CASES_TAC `(d:num->real^N->bool) j = {}` THENL
[ASM_REWRITE_TAC[
INTER_EMPTY;
NEGLIGIBLE_EMPTY;
SLICE_EMPTY];
UNDISCH_TAC `~((d:num->real^N->bool) j = {})`] THEN
FIRST_ASSUM(fun
th ->
MAP_EVERY (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)
[SPEC `i:num`
th; SPEC `j:num`
th]) THEN
REWRITE_TAC[
LEFT_IMP_EXISTS_THM] THEN
MAP_EVERY X_GEN_TAC [`w:real^N`; `x:real^N`] THEN STRIP_TAC THEN
MAP_EVERY X_GEN_TAC [`u:real^N`; `v:real^N`] THEN STRIP_TAC THEN
ASM_SIMP_TAC[
SLICE_INTERVAL;
INTERVAL_NE_EMPTY] THEN
DISCH_TAC THEN DISCH_TAC THEN
REPEAT(COND_CASES_TAC THEN
ASM_REWRITE_TAC[
INTER_EMPTY;
NEGLIGIBLE_EMPTY]) THEN
REWRITE_TAC[
INTER_INTERVAL;
NEGLIGIBLE_INTERVAL;
INTERVAL_EQ_EMPTY] THEN
ONCE_REWRITE_TAC[TAUT `a /\ b /\ c <=> ~(a /\ b ==> ~c)`] THEN
SIMP_TAC[
LAMBDA_BETA] THEN REWRITE_TAC[NOT_IMP] THEN
DISCH_THEN(X_CHOOSE_THEN `l:num` STRIP_ASSUME_TAC) THEN
SUBGOAL_THEN `~(l:num = k)` ASSUME_TAC THENL
[FIRST_X_ASSUM(CONJUNCTS_THEN
(fun
th -> MP_TAC(SPEC `i:num`
th) THEN MP_TAC(SPEC `j:num`
th))) THEN
ASM_SIMP_TAC[
INTERVAL_LOWERBOUND;
INTERVAL_UPPERBOUND] THEN
REWRITE_TAC[IMP_IMP] THEN ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
REWRITE_TAC[] THEN DISCH_THEN SUBST_ALL_TAC THEN ASM_REAL_ARITH_TAC;
ALL_TAC] THEN
FIRST_ASSUM(DISJ_CASES_TAC o MATCH_MP (ARITH_RULE
`~(l:num = k) ==> l < k \/ k < l`))
THENL
[EXISTS_TAC `l:num` THEN
MATCH_MP_TAC(TAUT `a /\ (a ==> b) ==> a /\ b`) THEN
CONJ_TAC THENL [ASM_ARITH_TAC; SIMP_TAC[
dropout;
LAMBDA_BETA]] THEN
ASM_REWRITE_TAC[];
ALL_TAC] THEN
EXISTS_TAC `l - 1` THEN
MATCH_MP_TAC(TAUT `a /\ (a ==> b) ==> a /\ b`) THEN
CONJ_TAC THENL [ASM_ARITH_TAC; SIMP_TAC[
dropout;
LAMBDA_BETA]] THEN
ASM_SIMP_TAC[ARITH_RULE `k < l ==> ~(l - 1 < k)`] THEN
ASM_SIMP_TAC[
SUB_ADD];
ALL_TAC] THEN
STRIP_TAC THEN MATCH_MP_TAC
REAL_LE_TRANS THEN EXISTS_TAC
`
real_integral (:real)
(\t.
measure ((
slice k t :(real^N->bool)->real^M->bool)
(
UNIONS {d n | n
IN (:num)})))` THEN
CONJ_TAC THENL
[MATCH_MP_TAC
REAL_INTEGRAL_LE THEN ASM_REWRITE_TAC[] THEN
X_GEN_TAC `t:real` THEN DISCH_TAC THEN MATCH_MP_TAC
MEASURE_SUBSET THEN
ASM_SIMP_TAC[
SLICE_SUBSET;
SLICE_UNIONS] THEN
ONCE_REWRITE_TAC[
SIMPLE_IMAGE] THEN REWRITE_TAC[GSYM
IMAGE_o] THEN
ONCE_REWRITE_TAC[GSYM
SIMPLE_IMAGE] THEN
MATCH_MP_TAC
MEASURABLE_COUNTABLE_UNIONS_BOUNDED THEN
ASM_REWRITE_TAC[
o_THM] THEN
MATCH_MP_TAC
BOUNDED_SUBSET THEN
EXISTS_TAC `(
slice k t:(real^N->bool)->real^M->bool) (
interval[a,b])` THEN
CONJ_TAC THENL
[ASM_SIMP_TAC[
SLICE_INTERVAL] THEN
MESON_TAC[
BOUNDED_INTERVAL;
BOUNDED_EMPTY];
REWRITE_TAC[
UNIONS_SUBSET;
FORALL_IN_GSPEC] THEN
ASM_MESON_TAC[
SLICE_SUBSET]];
MATCH_MP_TAC
REAL_EQ_IMP_LE THEN
MATCH_MP_TAC(ISPEC `
sequentially`
REALLIM_UNIQUE) THEN
EXISTS_TAC `\n.
real_integral (:real)
(\t.
sum (0..n) (\m.
measure((
slice k t:(real^N->bool)->real^M->bool)
(d m))))` THEN
ASM_REWRITE_TAC[
TRIVIAL_LIMIT_SEQUENTIALLY] THEN
MP_TAC(ISPEC `d:num->(real^N->bool)`
HAS_MEASURE_COUNTABLE_NEGLIGIBLE_UNIONS_BOUNDED) THEN
ANTS_TAC THENL
[ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
[ASM_MESON_TAC[
MEASURABLE_INTERVAL]; ALL_TAC] THEN
MATCH_MP_TAC
BOUNDED_SUBSET THEN EXISTS_TAC `
interval[a:real^N,b]` THEN
REWRITE_TAC[
BOUNDED_INTERVAL;
UNIONS_SUBSET;
IN_ELIM_THM] THEN
ASM_MESON_TAC[];
ALL_TAC] THEN
ASM_REWRITE_TAC[] THEN
GEN_REWRITE_TAC (LAND_CONV o RATOR_CONV o LAND_CONV) [GSYM
o_DEF] THEN
REWRITE_TAC[GSYM
REAL_SUMS] THEN
REWRITE_TAC[
real_sums;
FROM_INTER_NUMSEG] THEN
MATCH_MP_TAC EQ_IMP THEN AP_THM_TAC THEN AP_THM_TAC THEN
AP_TERM_TAC THEN GEN_REWRITE_TAC I [
FUN_EQ_THM] THEN
X_GEN_TAC `i:num` THEN REWRITE_TAC[] THEN
W(MP_TAC o PART_MATCH (lhand o rand)
REAL_INTEGRAL_SUM o rand o snd) THEN
ANTS_TAC THENL
[REWRITE_TAC[
FINITE_NUMSEG] THEN X_GEN_TAC `j:num` THEN DISCH_TAC THEN
SUBGOAL_THEN `?u v. u$k <= v$k /\
(d:num->real^N->bool) j =
interval[u,v]`
STRIP_ASSUME_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
ASM_REWRITE_TAC[] THEN REWRITE_TAC[
real_integrable_on] THEN
EXISTS_TAC `
measure(
interval[u:real^N,v])` THEN
MATCH_MP_TAC
FUBINI_CLOSED_INTERVAL THEN ASM_REWRITE_TAC[];
ALL_TAC] THEN
DISCH_THEN SUBST1_TAC THEN MATCH_MP_TAC
SUM_EQ_NUMSEG THEN
X_GEN_TAC `j:num` THEN STRIP_TAC THEN REWRITE_TAC[] THEN
CONV_TAC SYM_CONV THEN MATCH_MP_TAC
REAL_INTEGRAL_UNIQUE THEN
SUBGOAL_THEN `?u v. u$k <= v$k /\
(d:num->real^N->bool) j =
interval[u,v]`
STRIP_ASSUME_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
ASM_REWRITE_TAC[] THEN
MATCH_MP_TAC
FUBINI_CLOSED_INTERVAL THEN ASM_REWRITE_TAC[]]);;
(* ------------------------------------------------------------------------- *)
(* Scaled integer, and hence rational, values are dense in the reals. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Hence a criterion for two functions to agree. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Various sufficient conditions for additivity to imply linearity. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Extending a continuous function in a periodic way. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* A variant of REAL_CONTINUOUS_ADDITIVE_IMP_LINEAR for intervals. *)
(* ------------------------------------------------------------------------- *)
let REAL_CONTINUOUS_ADDITIVE_IMP_LINEAR_INTERVAL = prove
(`!f b. (f ---> &0) (
atreal (&0)
within {x | &0 <= x}) /\
(!x y. &0 <= x /\ &0 <= y /\ x + y <= b ==> f(x + y) = f(x) + f(y))
==> !a x. &0 <= x /\ x <= b /\
&0 <= a * x /\ a * x <= b
==> f(a * x) = a * f(x)`,
SUBGOAL_THEN
`!f. (f ---> &0) (
atreal (&0)
within {x | &0 <= x}) /\
(!x y. &0 <= x /\ &0 <= y /\ x + y <= &1 ==> f(x + y) = f(x) + f(y))
==> !a x. &0 <= x /\ x <= &1 /\ &0 <= a * x /\ a * x <= &1
==> f(a * x) = a * f(x)`
ASSUME_TAC THENL
[SUBGOAL_THEN
`!f. f
real_continuous_on real_interval[&0,&1] /\
(!x y. &0 <= x /\ &0 <= y /\ x + y <= &1 ==> f(x + y) = f(x) + f(y))
==> !a x. &0 <= x /\ x <= &1 /\ &0 <= a * x /\ a * x <= &1
==> f(a * x) = a * f(x)`
(fun
th -> GEN_TAC THEN STRIP_TAC THEN MATCH_MP_TAC
th) THENL
[REPEAT STRIP_TAC THEN
MP_TAC(ISPEC `f:real->
real`
REAL_CONTINUOUS_ADDITIVE_EXTEND) THEN
ASM_REWRITE_TAC[
IN_REAL_INTERVAL] THEN
DISCH_THEN(X_CHOOSE_THEN `g:real->
real` STRIP_ASSUME_TAC) THEN
MP_TAC(ISPEC `g:real->
real`
REAL_CONTINUOUS_ADDITIVE_IMP_LINEAR) THEN
ASM_MESON_TAC[];
ASM_REWRITE_TAC[
real_continuous_on;
IN_REAL_INTERVAL] THEN
X_GEN_TAC `x:real` THEN STRIP_TAC THEN
X_GEN_TAC `e:real` THEN DISCH_TAC THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [
REALLIM_WITHINREAL]) THEN
DISCH_THEN(MP_TAC o SPEC `e:real`) THEN
ASM_REWRITE_TAC[
REAL_SUB_RZERO] THEN REWRITE_TAC[
IN_REAL_INTERVAL] THEN
DISCH_THEN(X_CHOOSE_THEN `d:real` STRIP_ASSUME_TAC) THEN
EXISTS_TAC `d:real` THEN ASM_SIMP_TAC[
REAL_LT_MUL] THEN
X_GEN_TAC `y:real` THEN STRIP_TAC THEN
REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC
(REAL_ARITH `y = x \/ y < x \/ x < y`) THENL
[ASM_REWRITE_TAC[
REAL_SUB_REFL;
REAL_ABS_NUM];
SUBGOAL_THEN `(f:real->
real)(y + (x - y)) = f(y) + f(x - y)`
MP_TAC THENL
[FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REAL_ARITH_TAC;
REWRITE_TAC[
REAL_SUB_ADD2] THEN DISCH_THEN SUBST1_TAC THEN
REWRITE_TAC[
REAL_ADD_SUB2;
REAL_ABS_NEG] THEN
FIRST_X_ASSUM MATCH_MP_TAC THEN
REWRITE_TAC[
IN_ELIM_THM] THEN ASM_REAL_ARITH_TAC];
SUBGOAL_THEN `(f:real->
real)(x + (y - x)) = f(x) + f(y - x)`
MP_TAC THENL
[FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REAL_ARITH_TAC;
REWRITE_TAC[
REAL_SUB_ADD2] THEN DISCH_THEN SUBST1_TAC THEN
REWRITE_TAC[
REAL_ADD_SUB] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
REWRITE_TAC[
IN_ELIM_THM] THEN ASM_REAL_ARITH_TAC]]];
REPEAT GEN_TAC THEN STRIP_TAC THEN REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC
(REAL_ARITH `b < &0 \/ b = &0 \/ &0 < b`)
THENL
[ASM_REAL_ARITH_TAC;
ASM_SIMP_TAC[REAL_ARITH
`a <= x /\ x <= a /\ a <= y /\ y <= a <=> x = a /\ y = a`] THEN
FIRST_X_ASSUM(MP_TAC o SPECL [`&0`; `&0`]) THEN
ASM_REWRITE_TAC[REAL_ADD_LID;
REAL_LE_REFL] THEN CONV_TAC REAL_RING;
ALL_TAC] THEN
FIRST_X_ASSUM(MP_TAC o ISPEC `(\x. f(b * x)):real->
real`) THEN
REWRITE_TAC[] THEN ANTS_TAC THENL
[ALL_TAC;
MATCH_MP_TAC
MONO_FORALL THEN X_GEN_TAC `a:real` THEN
DISCH_THEN(fun
th -> X_GEN_TAC `x:real` THEN STRIP_TAC THEN
MP_TAC(ISPEC `x / b:real`
th)) THEN
ASM_SIMP_TAC[REAL_FIELD `&0 < b ==> b * a * x / b = a * x`;
REAL_DIV_LMUL;
REAL_LT_IMP_NZ] THEN
DISCH_THEN MATCH_MP_TAC THEN
REWRITE_TAC[REAL_ARITH `a * x / b:real = (a * x) / b`] THEN
ASM_SIMP_TAC[
REAL_LE_RDIV_EQ;
REAL_LE_LDIV_EQ] THEN
ASM_REAL_ARITH_TAC] THEN
CONJ_TAC THENL
[ALL_TAC;
REPEAT STRIP_TAC THEN REWRITE_TAC[REAL_ADD_LDISTRIB] THEN
FIRST_X_ASSUM MATCH_MP_TAC THEN
ASM_SIMP_TAC[REAL_ARITH `b * x + b * y <= b <=> &0 <= b * (&1 - (x + y))`;
REAL_LE_MUL;
REAL_LT_IMP_LE;
REAL_SUB_LE]] THEN
REWRITE_TAC[
REALLIM_WITHINREAL] THEN X_GEN_TAC `e:real` THEN DISCH_TAC THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [
REALLIM_WITHINREAL]) THEN
DISCH_THEN(MP_TAC o SPEC `e:real`) THEN ASM_REWRITE_TAC[
REAL_SUB_RZERO] THEN
REWRITE_TAC[
REAL_SUB_RZERO;
IN_ELIM_THM] THEN
DISCH_THEN(X_CHOOSE_THEN `d:real` STRIP_ASSUME_TAC) THEN
EXISTS_TAC `d / b:real` THEN ASM_SIMP_TAC[
REAL_LT_DIV] THEN
REPEAT STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
ASM_SIMP_TAC[
REAL_LE_MUL;
REAL_LT_IMP_LE;
REAL_ABS_MUL] THEN
ASM_SIMP_TAC[REAL_ARITH `&0 < b ==> abs b * x = x * b`] THEN
ASM_SIMP_TAC[
REAL_LT_MUL; GSYM
REAL_LT_RDIV_EQ]]);;
(* ------------------------------------------------------------------------- *)
(* More Steinhaus variants. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Bernstein polynomials. *)
(* ------------------------------------------------------------------------- *)
let BERNSTEIN_CONV =
GEN_REWRITE_CONV I [bernstein] THENC
COMB2_CONV (RAND_CONV(RAND_CONV NUM_BINOM_CONV))
(RAND_CONV(RAND_CONV NUM_SUB_CONV)) THENC
REAL_POLY_CONV;;
(* ------------------------------------------------------------------------- *)
(* Lemmas about Bernstein polynomials. *)
(* ------------------------------------------------------------------------- *)
let BERNSTEIN_LEMMA = prove
(`!n x.
sum(0..n) (\k. (&k - &n * x) pow 2 *
bernstein n k x) =
&n * x * (&1 - x)`,
REPEAT STRIP_TAC THEN
SUBGOAL_THEN
`!x y.
sum(0..n) (\k. &(
binom(n,k)) * x pow k * y pow (n - k)) =
(x + y) pow n`
(LABEL_TAC "0") THENL [ASM_REWRITE_TAC[
REAL_BINOMIAL_THEOREM]; ALL_TAC] THEN
SUBGOAL_THEN
`!x y.
sum(0..n) (\k. &k * &(
binom(n,k)) * x pow (k - 1) * y pow (n - k)) =
&n * (x + y) pow (n - 1)`
(LABEL_TAC "1") THENL
[REPEAT GEN_TAC THEN MATCH_MP_TAC
REAL_DERIVATIVE_UNIQUE_ATREAL THEN
MAP_EVERY EXISTS_TAC
[`\x.
sum(0..n) (\k. &(
binom(n,k)) * x pow k * y pow (n - k))`;
`x:real`] THEN
CONJ_TAC THENL
[MATCH_MP_TAC
HAS_REAL_DERIVATIVE_SUM THEN REWRITE_TAC[
FINITE_NUMSEG];
ASM_REWRITE_TAC[]] THEN
REPEAT STRIP_TAC THEN REAL_DIFF_TAC THEN CONV_TAC REAL_RING;
ALL_TAC] THEN
SUBGOAL_THEN
`!x y.
sum(0..n)
(\k. &k * &(k - 1) * &(
binom(n,k)) * x pow (k - 2) * y pow (n - k)) =
&n * &(n - 1) * (x + y) pow (n - 2)`
(LABEL_TAC "2") THENL
[REPEAT GEN_TAC THEN MATCH_MP_TAC
REAL_DERIVATIVE_UNIQUE_ATREAL THEN
MAP_EVERY EXISTS_TAC
[`\x.
sum(0..n) (\k. &k * &(
binom(n,k)) * x pow (k - 1) * y pow (n - k))`;
`x:real`] THEN
CONJ_TAC THENL
[MATCH_MP_TAC
HAS_REAL_DERIVATIVE_SUM THEN REWRITE_TAC[
FINITE_NUMSEG];
ASM_REWRITE_TAC[]] THEN
REPEAT STRIP_TAC THEN REAL_DIFF_TAC THEN
REWRITE_TAC[ARITH_RULE `n - 1 - 1 = n - 2`] THEN CONV_TAC REAL_RING;
ALL_TAC] THEN
REWRITE_TAC[REAL_ARITH
`(a - b) pow 2 * x =
a * (a - &1) * x + (&1 - &2 * b) * a * x + b * b * x`] THEN
REWRITE_TAC[
SUM_ADD_NUMSEG;
SUM_LMUL;
SUM_BERNSTEIN] THEN
SUBGOAL_THEN `
sum(0..n) (\k. &k *
bernstein n k x) = &n * x` SUBST1_TAC THENL
[REMOVE_THEN "1" (MP_TAC o SPECL [`x:real`; `&1 - x`]) THEN
REWRITE_TAC[
REAL_SUB_ADD2;
REAL_POW_ONE;
bernstein;
REAL_MUL_RID] THEN
DISCH_THEN(SUBST1_TAC o SYM) THEN REWRITE_TAC[GSYM
SUM_RMUL] THEN
MATCH_MP_TAC
SUM_EQ_NUMSEG THEN X_GEN_TAC `k:num` THEN STRIP_TAC THEN
REWRITE_TAC[REAL_ARITH
`(k * b * xk * y) * x:real = k * b * (x * xk) * y`] THEN
REWRITE_TAC[GSYM(CONJUNCT2
real_pow)] THEN
DISJ_CASES_TAC(ARITH_RULE `k = 0 \/ SUC(k - 1) = k`) THEN
ASM_REWRITE_TAC[
REAL_MUL_LZERO];
ALL_TAC] THEN
SUBGOAL_THEN
`
sum(0..n) (\k. &k * (&k - &1) *
bernstein n k x) = &n * (&n - &1) * x pow 2`
SUBST1_TAC THENL [ALL_TAC; CONV_TAC REAL_RING] THEN
REMOVE_THEN "2" (MP_TAC o SPECL [`x:real`; `&1 - x`]) THEN
REWRITE_TAC[
REAL_SUB_ADD2;
REAL_POW_ONE;
bernstein;
REAL_MUL_RID] THEN
ASM_CASES_TAC `n = 0` THEN
ASM_REWRITE_TAC[
SUM_SING_NUMSEG;
REAL_MUL_LZERO] THEN
ASM_SIMP_TAC[GSYM
REAL_OF_NUM_SUB;
LE_1; REAL_MUL_ASSOC] THEN
DISCH_THEN(SUBST1_TAC o SYM) THEN REWRITE_TAC[GSYM
SUM_RMUL] THEN
MATCH_MP_TAC
SUM_EQ_NUMSEG THEN X_GEN_TAC `k:num` THEN STRIP_TAC THEN
REWRITE_TAC[REAL_ARITH `((((k * k1) * b) * xk) * y) * x2:real =
k * k1 * b * y * (x2 * xk)`] THEN
REWRITE_TAC[GSYM
REAL_POW_ADD; GSYM REAL_MUL_ASSOC] THEN
REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC
(ARITH_RULE `k = 0 \/ k = 1 \/ 1 <= k /\ 2 + k - 2 = k`) THEN
ASM_REWRITE_TAC[
REAL_MUL_LZERO; REAL_MUL_LID;
SUB_REFL;
REAL_SUB_REFL] THEN
ASM_SIMP_TAC[GSYM
REAL_OF_NUM_SUB] THEN REWRITE_TAC[
REAL_MUL_AC]);;
(* ------------------------------------------------------------------------- *)
(* Explicit Bernstein version of 1D Weierstrass approximation theorem *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* General Stone-Weierstrass theorem. *)
(* ------------------------------------------------------------------------- *)
let STONE_WEIERSTRASS_ALT = prove
(`!(P:(real^N->
real)->bool) (s:real^N->bool).
compact s /\
(!c. P(\x. c)) /\
(!f g. P(f) /\ P(g) ==> P(\x. f x + g x)) /\
(!f g. P(f) /\ P(g) ==> P(\x. f x * g x)) /\
(!x y. x
IN s /\ y
IN s /\ ~(x = y)
==> ?f. (!x. x
IN s ==> f
real_continuous (
at x
within s)) /\
P(f) /\ ~(f x = f y))
==> !f e. (!x. x
IN s ==> f
real_continuous (
at x
within s)) /\ &0 < e
==> ?g. P(g) /\ !x. x
IN s ==> abs(f x - g x) < e`,
REPEAT GEN_TAC THEN STRIP_TAC THEN MAP_EVERY ABBREV_TAC
[`C = \f. !x:real^N. x
IN s ==> f
real_continuous at x
within s`;
`A = \f. C f /\
!e. &0 < e
==> ?g. P(g) /\ !x:real^N. x
IN s ==> abs(f x - g x) < e`] THEN
SUBGOAL_THEN `!f:real^N->real. C(f) ==> A(f)` MP_TAC THENL
[ALL_TAC; MAP_EVERY EXPAND_TAC ["A";
"C"] THEN SIMP_TAC[]] THEN
SUBGOAL_THEN `!c:real. A(\x:real^N. c)` (LABEL_TAC "const") THENL
[MAP_EVERY EXPAND_TAC ["A"; "C"] THEN X_GEN_TAC `c:real` THEN
ASM_REWRITE_TAC[REAL_CONTINUOUS_CONST] THEN X_GEN_TAC `e:real` THEN
DISCH_TAC THEN EXISTS_TAC `(\x. c):real^N->real` THEN
ASM_REWRITE_TAC[REAL_SUB_REFL; REAL_ABS_0];
ALL_TAC] THEN
SUBGOAL_THEN `!f g:real^N->real. A(f) /\ A(g) ==> A(\x. f x + g x)`
(LABEL_TAC "add") THENL
[MAP_EVERY EXPAND_TAC ["A"; "C"] THEN SIMP_TAC[REAL_CONTINUOUS_ADD] THEN
MAP_EVERY X_GEN_TAC [`f:real^N->real`; `g:real^N->real`] THEN
DISCH_THEN(fun th -> REPEAT STRIP_TAC THEN MP_TAC th) THEN
DISCH_THEN(CONJUNCTS_THEN (MP_TAC o SPEC `e / &2` o CONJUNCT2)) THEN
ASM_REWRITE_TAC[REAL_HALF; LEFT_IMP_EXISTS_THM] THEN
X_GEN_TAC `g':real^N->real` THEN STRIP_TAC THEN
X_GEN_TAC `f':real^N->real` THEN STRIP_TAC THEN
EXISTS_TAC `(\x. f' x + g' x):real^N->real` THEN
ASM_SIMP_TAC[REAL_ARITH
`abs(f - f') < e / &2 /\ abs(g - g') < e / &2
==> abs((f + g) - (f' + g')) < e`];
ALL_TAC] THEN
SUBGOAL_THEN `!f:real^N->real. A(f) ==> C(f)` (LABEL_TAC "AC") THENL
[EXPAND_TAC "A" THEN SIMP_TAC[]; ALL_TAC] THEN
SUBGOAL_THEN `!f:real^N->real. C(f) ==> real_bounded(IMAGE f s)`
(LABEL_TAC "bound") THENL
[GEN_TAC THEN EXPAND_TAC "C" THEN
REWRITE_TAC[REAL_BOUNDED; GSYM IMAGE_o] THEN
REWRITE_TAC[REAL_CONTINUOUS_CONTINUOUS1] THEN
REWRITE_TAC[GSYM CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN] THEN
ASM_SIMP_TAC[COMPACT_IMP_BOUNDED; COMPACT_CONTINUOUS_IMAGE];
ALL_TAC] THEN
SUBGOAL_THEN `!f g:real^N->real. A(f) /\ A(g) ==> A(\x. f x * g x)`
(LABEL_TAC "mul") THENL
[MAP_EVERY X_GEN_TAC [`f:real^N->real`; `g:real^N->real`] THEN
DISCH_THEN(fun th -> STRIP_ASSUME_TAC th THEN MP_TAC th) THEN
MAP_EVERY EXPAND_TAC ["A"; "C"] THEN SIMP_TAC[REAL_CONTINUOUS_MUL] THEN
REWRITE_TAC[IMP_CONJ] THEN
MAP_EVERY (DISCH_THEN o LABEL_TAC) ["cf"; "af"; "cg"; "ag"] THEN
SUBGOAL_THEN
`real_bounded(IMAGE (f:real^N->real) s) /\
real_bounded(IMAGE (g:real^N->real) s)`
MP_TAC THENL
[ASM_SIMP_TAC[]; REWRITE_TAC[REAL_BOUNDED_POS_LT; FORALL_IN_IMAGE]] THEN
DISCH_THEN(CONJUNCTS_THEN2
(X_CHOOSE_THEN `Bf:real` STRIP_ASSUME_TAC)
(X_CHOOSE_THEN `Bg:real` STRIP_ASSUME_TAC)) THEN
X_GEN_TAC `e:real` THEN DISCH_TAC THEN
REMOVE_THEN "ag" (MP_TAC o SPEC `e / &2 / Bf`) THEN
ASM_SIMP_TAC[REAL_HALF; REAL_LT_DIV; LEFT_IMP_EXISTS_THM] THEN
X_GEN_TAC `g':real^N->real` THEN STRIP_TAC THEN
REMOVE_THEN "af" (MP_TAC o SPEC `e / &2 / (Bg + e / &2 / Bf)`) THEN
ASM_SIMP_TAC[REAL_HALF; REAL_LT_DIV; REAL_LT_ADD] THEN
DISCH_THEN(X_CHOOSE_THEN `f':real^N->real` STRIP_ASSUME_TAC) THEN
EXISTS_TAC `(\x. f'(x) * g'(x)):real^N->real` THEN
ASM_SIMP_TAC[REAL_ARITH
`f * g - f' * g':real = f * (g - g') + g' * (f - f')`] THEN
X_GEN_TAC `x:real^N` THEN DISCH_TAC THEN
SUBGOAL_THEN `e = Bf * e / &2 / Bf +
(Bg + e / &2 / Bf) * e / &2 / (Bg + e / &2 / Bf)`
SUBST1_TAC THENL
[MATCH_MP_TAC(REAL_ARITH `a = e / &2 /\ b = e / &2 ==> e = a + b`) THEN
CONJ_TAC THEN MAP_EVERY MATCH_MP_TAC [REAL_DIV_LMUL; REAL_LT_IMP_NZ] THEN
ASM_SIMP_TAC[REAL_LT_DIV; REAL_LT_ADD; REAL_HALF];
MATCH_MP_TAC(REAL_ARITH
`abs a < c /\ abs b < d ==> abs(a + b) < c + d`) THEN
REWRITE_TAC[REAL_ABS_MUL] THEN CONJ_TAC THEN
MATCH_MP_TAC REAL_LT_MUL2 THEN ASM_SIMP_TAC[REAL_ABS_POS] THEN
MATCH_MP_TAC(REAL_ARITH
`!g. abs(g) < Bg /\ abs(g - g') < e ==> abs(g') < Bg + e`) THEN
EXISTS_TAC `(g:real^N->real) x` THEN ASM_SIMP_TAC[]];
ALL_TAC] THEN
SUBGOAL_THEN
`!x y. x IN s /\ y IN s /\ ~(x = y)
==> ?f:real^N->real. A(f) /\ ~(f x = f y)`
(LABEL_TAC "sep") THENL
[MAP_EVERY X_GEN_TAC [`x:real^N`; `y:real^N`] THEN STRIP_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPECL [`x:real^N`; `y:real^N`]) THEN
ASM_REWRITE_TAC[] THEN MATCH_MP_TAC MONO_EXISTS THEN
MAP_EVERY EXPAND_TAC ["A"; "C"] THEN
ASM_MESON_TAC[REAL_SUB_REFL; REAL_ABS_0];
ALL_TAC] THEN
SUBGOAL_THEN `!f. A(f) ==> A(\x:real^N. abs(f x))` (LABEL_TAC "abs") THENL
[SUBGOAL_THEN `!f. A(f) /\ (!x. x IN s ==> abs(f x) <= &1 / &4)
==> A(\x:real^N. abs(f x))`
ASSUME_TAC THENL
[ALL_TAC;
REPEAT STRIP_TAC THEN
SUBGOAL_THEN `real_bounded(IMAGE (f:real^N->real) s)` MP_TAC THENL
[ASM_SIMP_TAC[]; REWRITE_TAC[REAL_BOUNDED_POS_LT; FORALL_IN_IMAGE]] THEN
DISCH_THEN(X_CHOOSE_THEN `B:real` STRIP_ASSUME_TAC) THEN
SUBGOAL_THEN `A(\x:real^N. (&4 * B) * abs(inv(&4 * B) * f x)):bool`
MP_TAC THENL
[USE_THEN "mul" MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN
FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_SIMP_TAC[REAL_ABS_MUL] THEN
ASM_SIMP_TAC[REAL_ARITH `&0 < B ==> abs(B) = B`;
REAL_LT_INV_EQ; REAL_LT_MUL; REAL_OF_NUM_LT; ARITH] THEN
ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
ASM_SIMP_TAC[GSYM real_div; REAL_LE_LDIV_EQ; REAL_LT_MUL;
REAL_OF_NUM_LT; ARITH; REAL_MUL_ASSOC] THEN
CONV_TAC REAL_RAT_REDUCE_CONV THEN
ASM_SIMP_TAC[REAL_MUL_LID; REAL_LT_IMP_LE];
ASM_SIMP_TAC[REAL_ABS_MUL; REAL_ARITH `&0 < B ==> abs(B) = B`;
REAL_LT_INV_EQ; REAL_LT_MUL; REAL_OF_NUM_LT; ARITH] THEN
ASM_SIMP_TAC[REAL_MUL_ASSOC; REAL_MUL_RINV; REAL_MUL_LID;
REAL_ARITH `&0 < B ==> ~(&4 * B = &0)`]]] THEN
X_GEN_TAC `f:real^N->real` THEN MAP_EVERY EXPAND_TAC ["A"; "C"] THEN
DISCH_THEN(fun th -> CONJ_TAC THEN MP_TAC th) THENL
[DISCH_THEN(MP_TAC o CONJUNCT1 o CONJUNCT1) THEN
MATCH_MP_TAC MONO_FORALL THEN GEN_TAC THEN MATCH_MP_TAC MONO_IMP THEN
REWRITE_TAC[] THEN
MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ_ALT; o_DEF]
REAL_CONTINUOUS_WITHIN_COMPOSE) THEN
REWRITE_TAC[real_continuous_withinreal] THEN
MESON_TAC[ARITH_RULE `abs(x - y) < d ==> abs(abs x - abs y) < d`];
ALL_TAC] THEN
DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
DISCH_THEN(fun t -> X_GEN_TAC `e:real` THEN DISCH_TAC THEN MP_TAC t) THEN
DISCH_THEN(MP_TAC o SPEC `min (e / &2) (&1 / &4)`) THEN
ANTS_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
REWRITE_TAC[REAL_LT_MIN; FORALL_AND_THM;
TAUT `(a ==> b /\ c) <=> (a ==> b) /\ (a ==> c)`] THEN
DISCH_THEN(X_CHOOSE_THEN `p:real^N->real` STRIP_ASSUME_TAC) THEN
MP_TAC(ISPECL [`\x. abs(x - &1 / &2)`; `e / &2`]
BERNSTEIN_WEIERSTRASS) THEN
REWRITE_TAC[] THEN ANTS_TAC THENL
[ASM_REWRITE_TAC[real_continuous_on; REAL_HALF] THEN
MESON_TAC[ARITH_RULE
`abs(x - y) < d ==> abs(abs(x - a) - abs(y - a)) < d`];
ALL_TAC] THEN
DISCH_THEN(X_CHOOSE_THEN `n:num` (MP_TAC o SPEC `n:num`)) THEN
REWRITE_TAC[LE_REFL] THEN DISCH_TAC THEN
EXISTS_TAC `\x:real^N. sum(0..n) (\k. abs(&k / &n - &1 / &2) *
bernstein n k (&1 / &2 + p x))` THEN
REWRITE_TAC[] THEN CONJ_TAC THENL
[SUBGOAL_THEN
`!m c z. P(\x:real^N.
sum(0..m) (\k. c k * bernstein (z m) k (&1 / &2 + p x)))`
(fun th -> REWRITE_TAC[th]) THEN
SUBGOAL_THEN
`!m k. P(\x:real^N. bernstein m k (&1 / &2 + p x))`
ASSUME_TAC THENL
[ALL_TAC; INDUCT_TAC THEN ASM_SIMP_TAC[SUM_CLAUSES_NUMSEG; LE_0]] THEN
REPEAT GEN_TAC THEN REWRITE_TAC[bernstein] THEN
REWRITE_TAC[REAL_ARITH `&1 - (&1 / &2 + p) = &1 / &2 + -- &1 * p`] THEN
REPEAT(FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]) THEN
SUBGOAL_THEN
`!f:real^N->real k. P(f) ==> P(\x. f(x) pow k)`
(fun th -> ASM_SIMP_TAC[th]) THEN
GEN_TAC THEN INDUCT_TAC THEN ASM_SIMP_TAC[real_pow];
REPEAT STRIP_TAC THEN MATCH_MP_TAC(REAL_ARITH
`!p. abs(abs(p x) - s) < e / &2 /\
abs(f x - p x) < e / &2
==> abs(abs(f x) - s) < e`) THEN
EXISTS_TAC `p:real^N->real` THEN ASM_SIMP_TAC[] THEN
GEN_REWRITE_TAC (PAT_CONV `\x. abs(abs x - a) < e`)
[REAL_ARITH `x = (&1 / &2 + x) - &1 / &2`] THEN
FIRST_X_ASSUM MATCH_MP_TAC THEN REWRITE_TAC[IN_REAL_INTERVAL] THEN
MATCH_MP_TAC(REAL_ARITH
`!f. abs(f) <= &1 / &4 /\ abs(f - p) < &1 / &4
==> &0 <= &1 / &2 + p /\ &1 / &2 + p <= &1`) THEN
EXISTS_TAC `(f:real^N->real) x` THEN ASM_SIMP_TAC[]];
ALL_TAC] THEN
SUBGOAL_THEN `!f:real^N->real g. A(f) /\ A(g) ==> A(\x. max (f x) (g x))`
(LABEL_TAC "max") THENL
[REPEAT STRIP_TAC THEN REWRITE_TAC[REAL_ARITH
`max a b = inv(&2) * (a + b + abs(a + -- &1 * b))`] THEN
REPEAT(FIRST_ASSUM MATCH_MP_TAC THEN ASM_SIMP_TAC[]);
ALL_TAC] THEN
SUBGOAL_THEN `!f:real^N->real g. A(f) /\ A(g) ==> A(\x. min (f x) (g x))`
(LABEL_TAC "min") THENL
[ASM_SIMP_TAC[REAL_ARITH `min a b = -- &1 * (max(-- &1 * a) (-- &1 * b))`];
ALL_TAC] THEN
SUBGOAL_THEN
`!t. FINITE t /\ (!f. f IN t ==> A(f)) ==> A(\x:real^N. sup {f(x) | f IN t})`
(LABEL_TAC "sup") THENL
[REWRITE_TAC[IMP_CONJ] THEN MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
ASM_SIMP_TAC[FORALL_IN_INSERT; SIMPLE_IMAGE; IMAGE_CLAUSES] THEN
ASM_SIMP_TAC[SUP_INSERT_FINITE; FINITE_IMAGE; IMAGE_EQ_EMPTY] THEN
MAP_EVERY X_GEN_TAC [`f:real^N->real`; `t:(real^N->real)->bool`] THEN
ASM_CASES_TAC `t:(real^N->real)->bool = {}` THEN ASM_SIMP_TAC[ETA_AX];
ALL_TAC] THEN
SUBGOAL_THEN
`!t. FINITE t /\ (!f. f IN t ==> A(f)) ==> A(\x:real^N. inf {f(x) | f IN t})`
(LABEL_TAC "inf") THENL
[REWRITE_TAC[IMP_CONJ] THEN MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
ASM_SIMP_TAC[FORALL_IN_INSERT; SIMPLE_IMAGE; IMAGE_CLAUSES] THEN
ASM_SIMP_TAC[INF_INSERT_FINITE; FINITE_IMAGE; IMAGE_EQ_EMPTY] THEN
MAP_EVERY X_GEN_TAC [`f:real^N->real`; `t:(real^N->real)->bool`] THEN
ASM_CASES_TAC `t:(real^N->real)->bool = {}` THEN ASM_SIMP_TAC[ETA_AX];
ALL_TAC] THEN
SUBGOAL_THEN
`!f:real^N->real e.
C(f) /\ &0 < e ==> ?g. A(g) /\ !x. x IN s ==> abs(f x - g x) < e`
ASSUME_TAC THENL
[ALL_TAC;
X_GEN_TAC `f:real^N->real` THEN DISCH_TAC THEN EXPAND_TAC "A" THEN
CONJ_TAC THENL [FIRST_X_ASSUM ACCEPT_TAC; ALL_TAC] THEN
X_GEN_TAC `e:real` THEN DISCH_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPECL [`f:real^N->real`; `e / &2`]) THEN
ASM_REWRITE_TAC[REAL_HALF; LEFT_IMP_EXISTS_THM] THEN
X_GEN_TAC `h:real^N->real` THEN EXPAND_TAC "A" THEN
DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
DISCH_THEN(MP_TAC o SPEC `e / &2` o CONJUNCT2) THEN
ASM_REWRITE_TAC[REAL_HALF] THEN MATCH_MP_TAC MONO_EXISTS THEN
ASM_MESON_TAC[REAL_ARITH
`abs(f - h) < e / &2 /\ abs(h - g) < e / &2 ==> abs(f - g) < e`]] THEN
MAP_EVERY X_GEN_TAC [`f:real^N->real`; `e:real`] THEN EXPAND_TAC "C" THEN
STRIP_TAC THEN
SUBGOAL_THEN
`!x y. x IN s /\ y IN s
==> ?h:real^N->real. A(h) /\ h(x) = f(x) /\ h(y) = f(y)`
MP_TAC THENL
[REPEAT STRIP_TAC THEN ASM_CASES_TAC `y:real^N = x` THENL
[EXISTS_TAC `\z:real^N. (f:real^N->real) x` THEN ASM_SIMP_TAC[];
SUBGOAL_THEN `?h:real^N->real. A(h) /\ ~(h x = h y)`
STRIP_ASSUME_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
EXISTS_TAC `\z. (f y - f x) / (h y - h x) * (h:real^N->real)(z) +
(f x - (f y - f x) / (h y - h x) * h(x))` THEN
ASM_SIMP_TAC[] THEN
UNDISCH_TAC `~((h:real^N->real) x = h y)` THEN CONV_TAC REAL_FIELD];
ALL_TAC] THEN
GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [RIGHT_IMP_EXISTS_THM] THEN
REWRITE_TAC[SKOLEM_THM; LEFT_IMP_EXISTS_THM] THEN
X_GEN_TAC `f2:real^N->real^N->real^N->real` THEN DISCH_TAC THEN
ABBREV_TAC `G = \x y.
{z | z IN s /\ (f2:real^N->real^N->real^N->real) x y z < f(z) + e}` THEN
SUBGOAL_THEN `!x y:real^N. x IN s /\ y IN s ==> x IN G x y /\ y IN G x y`
ASSUME_TAC THENL
[EXPAND_TAC "G" THEN REWRITE_TAC[IN_ELIM_THM] THEN
ASM_SIMP_TAC[REAL_LT_ADDR];
ALL_TAC] THEN
SUBGOAL_THEN
`!x. x IN s ==> ?f1. A(f1) /\ f1 x = f x /\
!y:real^N. y IN s ==> f1 y < f y + e`
MP_TAC THENL
[REPEAT STRIP_TAC THEN FIRST_ASSUM(MP_TAC o
GEN_REWRITE_RULE I [COMPACT_EQ_HEINE_BOREL_SUBTOPOLOGY]) THEN
DISCH_THEN(MP_TAC o SPEC
`{(G:real^N->real^N->real^N->bool) x y | y IN s}`) THEN
REWRITE_TAC[SIMPLE_IMAGE; UNIONS_IMAGE; FORALL_IN_IMAGE; ETA_AX] THEN
ANTS_TAC THENL
[CONJ_TAC THENL [ALL_TAC; ASM SET_TAC[]] THEN
EXPAND_TAC "G" THEN REWRITE_TAC[] THEN X_GEN_TAC `w:real^N` THEN
DISCH_TAC THEN
MP_TAC(ISPECL [`lift o (\z:real^N. f2 (x:real^N) (w:real^N) z - f z)`;
`s:real^N->bool`;
`{x:real^1 | x$1 < e}`] CONTINUOUS_OPEN_IN_PREIMAGE) THEN
REWRITE_TAC[OPEN_HALFSPACE_COMPONENT_LT; IN_ELIM_THM] THEN
REWRITE_TAC[GSYM drop; LIFT_DROP; o_DEF] THEN
REWRITE_TAC[LIFT_SUB; GSYM REAL_CONTINUOUS_CONTINUOUS1;
REAL_ARITH `x < y + e <=> x - y < e`] THEN
DISCH_THEN MATCH_MP_TAC THEN MATCH_MP_TAC CONTINUOUS_ON_SUB THEN
ONCE_REWRITE_TAC[GSYM o_DEF] THEN
REWRITE_TAC[CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN] THEN
REWRITE_TAC[GSYM REAL_CONTINUOUS_CONTINUOUS1; ETA_AX] THEN
ASM_MESON_TAC[];
ALL_TAC] THEN
ONCE_REWRITE_TAC[TAUT `a /\ b /\ c <=> b /\ a /\ c`] THEN
REWRITE_TAC[EXISTS_FINITE_SUBSET_IMAGE; UNIONS_IMAGE] THEN
DISCH_THEN(X_CHOOSE_THEN `t:real^N->bool` STRIP_ASSUME_TAC) THEN
EXISTS_TAC `\z:real^N. inf {f2 (x:real^N) (y:real^N) z | y IN t}` THEN
REWRITE_TAC[] THEN REPEAT CONJ_TAC THENL
[GEN_REWRITE_TAC RAND_CONV [REAL_ARITH `x = min x x`] THEN
REWRITE_TAC[REAL_MIN_INF; INSERT_AC] THEN AP_TERM_TAC THEN ASM SET_TAC[];
REMOVE_THEN "inf" (MP_TAC o SPEC
`IMAGE (\y z. (f2:real^N->real^N->real^N->real) x y z) t`) THEN
ASM_SIMP_TAC[FINITE_IMAGE; FORALL_IN_IMAGE] THEN
REWRITE_TAC[SIMPLE_IMAGE; ETA_AX] THEN
ANTS_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
REWRITE_TAC[GSYM IMAGE_o; o_DEF];
SUBGOAL_THEN `~(t:real^N->bool = {})` ASSUME_TAC THENL
[ASM SET_TAC[]; ALL_TAC] THEN
ASM_SIMP_TAC[REAL_INF_LT_FINITE; SIMPLE_IMAGE;
FINITE_IMAGE; IMAGE_EQ_EMPTY] THEN
REWRITE_TAC[EXISTS_IN_IMAGE] THEN
X_GEN_TAC `y:real^N` THEN DISCH_TAC THEN
UNDISCH_TAC
`s SUBSET {y:real^N | ?z:real^N. z IN t /\ y IN G (x:real^N) z}` THEN
REWRITE_TAC[SUBSET; IN_ELIM_THM] THEN
DISCH_THEN(MP_TAC o SPEC `y:real^N`) THEN ASM_REWRITE_TAC[] THEN
EXPAND_TAC "G" THEN REWRITE_TAC[IN_ELIM_THM] THEN ASM_REWRITE_TAC[]];
GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV)
[RIGHT_IMP_EXISTS_THM] THEN
REWRITE_TAC[SKOLEM_THM; LEFT_IMP_EXISTS_THM] THEN
X_GEN_TAC `f1:real^N->real^N->real` THEN DISCH_TAC] THEN
ABBREV_TAC `H = \x:real^N. {z:real^N | z IN s /\ f z - e < f1 x z}` THEN
SUBGOAL_THEN `!x:real^N. x IN s ==> x IN (H x)` ASSUME_TAC THENL
[EXPAND_TAC "H" THEN REWRITE_TAC[IN_ELIM_THM] THEN
ASM_SIMP_TAC[REAL_ARITH `x - e < x <=> &0 < e`];
ALL_TAC] THEN
FIRST_ASSUM(MP_TAC o
GEN_REWRITE_RULE I [COMPACT_EQ_HEINE_BOREL_SUBTOPOLOGY]) THEN
DISCH_THEN(MP_TAC o SPEC
`{(H:real^N->real^N->bool) x | x IN s}`) THEN
REWRITE_TAC[SIMPLE_IMAGE; UNIONS_IMAGE; FORALL_IN_IMAGE; ETA_AX] THEN
ANTS_TAC THENL
[CONJ_TAC THENL [ALL_TAC; ASM SET_TAC[]] THEN EXPAND_TAC "H" THEN
REWRITE_TAC[] THEN X_GEN_TAC `x:real^N` THEN DISCH_TAC THEN
MP_TAC(ISPECL [`lift o (\z:real^N. f z - f1 (x:real^N) z)`;
`s:real^N->bool`;
`{x:real^1 | x$1 < e}`] CONTINUOUS_OPEN_IN_PREIMAGE) THEN
REWRITE_TAC[OPEN_HALFSPACE_COMPONENT_LT; IN_ELIM_THM] THEN
REWRITE_TAC[GSYM drop; LIFT_DROP; o_DEF] THEN
GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV)
[REAL_ARITH `x - y < z <=> x - z < y`] THEN
DISCH_THEN MATCH_MP_TAC THEN
REWRITE_TAC[LIFT_SUB; GSYM REAL_CONTINUOUS_CONTINUOUS1;
REAL_ARITH `x < y + e <=> x - y < e`] THEN
MATCH_MP_TAC CONTINUOUS_ON_SUB THEN
ONCE_REWRITE_TAC[GSYM o_DEF] THEN
REWRITE_TAC[CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN] THEN
REWRITE_TAC[GSYM REAL_CONTINUOUS_CONTINUOUS1; ETA_AX] THEN
ASM_MESON_TAC[];
ALL_TAC] THEN
ONCE_REWRITE_TAC[TAUT `a /\ b /\ c <=> b /\ a /\ c`] THEN
REWRITE_TAC[EXISTS_FINITE_SUBSET_IMAGE; UNIONS_IMAGE] THEN
DISCH_THEN(X_CHOOSE_THEN `t:real^N->bool` STRIP_ASSUME_TAC) THEN
EXISTS_TAC `\z:real^N. sup {f1 (x:real^N) z | x IN t}` THEN
REWRITE_TAC[] THEN CONJ_TAC THENL
[REMOVE_THEN "sup" (MP_TAC o SPEC `IMAGE (f1:real^N->real^N->real) t`) THEN
ASM_SIMP_TAC[FINITE_IMAGE; FORALL_IN_IMAGE] THEN
REWRITE_TAC[SIMPLE_IMAGE; ETA_AX] THEN
ANTS_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
REWRITE_TAC[GSYM IMAGE_o; o_DEF];
ALL_TAC] THEN
X_GEN_TAC `x:real^N` THEN DISCH_TAC THEN
SUBGOAL_THEN `~(t:real^N->bool = {})` ASSUME_TAC THENL
[ASM SET_TAC[]; ALL_TAC] THEN
REWRITE_TAC[SIMPLE_IMAGE; REAL_ARITH
`abs(f - s) < e <=> f - e < s /\ s < f + e`] THEN
ASM_SIMP_TAC[REAL_SUP_LT_FINITE; REAL_LT_SUP_FINITE;
FINITE_IMAGE; IMAGE_EQ_EMPTY] THEN
REWRITE_TAC[EXISTS_IN_IMAGE; FORALL_IN_IMAGE] THEN
CONJ_TAC THENL [ALL_TAC; ASM SET_TAC[]] THEN
UNDISCH_TAC `s SUBSET {y:real^N | ?x:real^N. x IN t /\ y IN H x}` THEN
REWRITE_TAC[SUBSET; IN_ELIM_THM] THEN
DISCH_THEN(MP_TAC o SPEC `x:real^N`) THEN ASM_REWRITE_TAC[] THEN
EXPAND_TAC "H" THEN REWRITE_TAC[IN_ELIM_THM] THEN ASM_REWRITE_TAC[]);;
let STONE_WEIERSTRASS = prove
(`!(P:(real^N->
real)->bool) (s:real^N->bool).
compact s /\
(!f. P(f) ==> !x. x
IN s ==> f
real_continuous (
at x
within s)) /\
(!c. P(\x. c)) /\
(!f g. P(f) /\ P(g) ==> P(\x. f x + g x)) /\
(!f g. P(f) /\ P(g) ==> P(\x. f x * g x)) /\
(!x y. x
IN s /\ y
IN s /\ ~(x = y) ==> ?f. P(f) /\ ~(f x = f y))
==> !f e. (!x. x
IN s ==> f
real_continuous (
at x
within s)) /\ &0 < e
==> ?g. P(g) /\ !x. x
IN s ==> abs(f x - g x) < e`,
REPEAT GEN_TAC THEN STRIP_TAC THEN
MATCH_MP_TAC
STONE_WEIERSTRASS_ALT THEN ASM_SIMP_TAC[] THEN
MAP_EVERY X_GEN_TAC [`x:real^N`; `y:real^N`] THEN STRIP_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPECL [`x:real^N`; `y:real^N`]) THEN
ASM_REWRITE_TAC[] THEN MATCH_MP_TAC
MONO_EXISTS THEN ASM_MESON_TAC[]);;
(* ------------------------------------------------------------------------- *)
(* Real and complex versions of Stone-Weierstrass theorem. *)
(* ------------------------------------------------------------------------- *)
let REAL_STONE_WEIERSTRASS = prove
(`!P s.
real_compact s /\
(!f. P f ==> f
real_continuous_on s) /\
(!c. P (\x. c)) /\
(!f g. P f /\ P g ==> P (\x. f x + g x)) /\
(!f g. P f /\ P g ==> P (\x. f x * g x)) /\
(!x y. x
IN s /\ y
IN s /\ ~(x = y) ==> ?f. P f /\ ~(f x = f y))
==> !f e. f
real_continuous_on s /\ &0 < e
==> ?g. P g /\ !x. x
IN s ==> abs(f x - g x) < e`,
REPEAT GEN_TAC THEN STRIP_TAC THEN
MATCH_MP_TAC
REAL_STONE_WEIERSTRASS_ALT THEN ASM_SIMP_TAC[] THEN
MAP_EVERY X_GEN_TAC [`x:real`; `y:real`] THEN STRIP_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPECL [`x:real`; `y:real`]) THEN
ASM_REWRITE_TAC[] THEN MATCH_MP_TAC
MONO_EXISTS THEN ASM_MESON_TAC[]);;
let COMPLEX_STONE_WEIERSTRASS = prove
(`!P s.
compact s /\
(!f. P f ==> f
continuous_on s) /\
(!c. P (\x. c)) /\
(!f. P f ==> P(\x.
cnj(f x))) /\
(!f g. P f /\ P g ==> P (\x. f x + g x)) /\
(!f g. P f /\ P g ==> P (\x. f x * g x)) /\
(!x y. x
IN s /\ y
IN s /\ ~(x = y) ==> ?f. P f /\ ~(f x = f y))
==> !f:real^N->
complex e.
f
continuous_on s /\ &0 < e
==> ?g. P g /\ !x. x
IN s ==>
norm(f x - g x) < e`,
REPEAT GEN_TAC THEN STRIP_TAC THEN
MATCH_MP_TAC
COMPLEX_STONE_WEIERSTRASS_ALT THEN ASM_SIMP_TAC[] THEN
MAP_EVERY X_GEN_TAC [`x:real^N`; `y:real^N`] THEN STRIP_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPECL [`x:real^N`; `y:real^N`]) THEN
ASM_REWRITE_TAC[] THEN MATCH_MP_TAC
MONO_EXISTS THEN ASM_MESON_TAC[]);;
(* ------------------------------------------------------------------------- *)
(* Stone-Weierstrass for R^n -> R polynomials. *)
(* ------------------------------------------------------------------------- *)
let real_polynomial_function_RULES,
real_polynomial_function_INDUCT,
real_polynomial_function_CASES = new_inductive_definition
`(!i. 1 <= i /\ i <= dimindex(:N)
==> real_polynomial_function(\x:real^N. x$i)) /\
(!c. real_polynomial_function(\x:real^N. c)) /\
(!f g. real_polynomial_function f /\ real_polynomial_function g
==> real_polynomial_function(\x:real^N. f x + g x)) /\
(!f g. real_polynomial_function f /\ real_polynomial_function g
==> real_polynomial_function(\x:real^N. f x * g x))`;;
(* ------------------------------------------------------------------------- *)
(* Stone-Weierstrass for real^M->real^N polynomials. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* One application is to pick a smooth approximation to a path, or just pick *)
(* a smooth path anyway in an open connected set. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Lipschitz property for real and vector polynomials. *)
(* ------------------------------------------------------------------------- *)
let LIPSCHITZ_REAL_POLYNOMIAL_FUNCTION = prove
(`!f:real^N->
real s.
real_polynomial_function f /\
bounded s
==> ?B. &0 < B /\
!x y. x
IN s /\ y
IN s ==> abs(f x - f y) <= B *
norm(x - y)`,
ONCE_REWRITE_TAC[
SWAP_FORALL_THM] THEN GEN_TAC THEN
ASM_CASES_TAC `
bounded(s:real^N->bool)` THEN ASM_REWRITE_TAC[] THEN
ASM_CASES_TAC `s:real^N->bool = {}` THENL
[ASM_REWRITE_TAC[
NOT_IN_EMPTY] THEN MESON_TAC[
REAL_LT_01]; ALL_TAC] THEN
MATCH_MP_TAC real_polynomial_function_INDUCT THEN REPEAT CONJ_TAC THENL
[REPEAT STRIP_TAC THEN EXISTS_TAC `&1` THEN REWRITE_TAC[
REAL_LT_01] THEN
ASM_SIMP_TAC[REAL_MUL_LID; GSYM
VECTOR_SUB_COMPONENT;
COMPONENT_LE_NORM];
GEN_TAC THEN EXISTS_TAC `&1` THEN
SIMP_TAC[
REAL_LT_01;
REAL_SUB_REFL;
REAL_ABS_NUM; REAL_MUL_LID;
NORM_POS_LE];
ALL_TAC; ALL_TAC] THEN
MAP_EVERY X_GEN_TAC [`f:real^N->
real`; `g:real^N->
real`] THEN
DISCH_THEN(CONJUNCTS_THEN2
(X_CHOOSE_THEN `B1:real` STRIP_ASSUME_TAC)
(X_CHOOSE_THEN `B2:real` STRIP_ASSUME_TAC))
THENL
[EXISTS_TAC `B1 + B2:real` THEN ASM_SIMP_TAC[
REAL_LT_ADD] THEN
REPEAT STRIP_TAC THEN MATCH_MP_TAC(REAL_ARITH
`abs(f - f') <= B1 * n /\ abs(g - g') <= B2 * n
==> abs((f + g) - (f' + g')) <= (B1 + B2) * n`) THEN
ASM_SIMP_TAC[];
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM
MEMBER_NOT_EMPTY]) THEN
DISCH_THEN(X_CHOOSE_TAC `a:real^N`) THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [
BOUNDED_POS]) THEN
DISCH_THEN(X_CHOOSE_THEN `B:real` STRIP_ASSUME_TAC) THEN
EXISTS_TAC `B1 * (abs(g(a:real^N)) + B2 * &2 * B) +
B2 * (abs(f a) + B1 * &2 * B)` THEN
CONJ_TAC THENL
[MATCH_MP_TAC
REAL_LT_ADD THEN CONJ_TAC THEN MATCH_MP_TAC
REAL_LT_MUL THEN
ASM_REWRITE_TAC[] THEN MATCH_MP_TAC(REAL_ARITH
`&0 < x ==> &0 < abs a + x`) THEN
MATCH_MP_TAC
REAL_LT_MUL THEN ASM_REAL_ARITH_TAC;
REPEAT STRIP_TAC THEN REWRITE_TAC[] THEN MATCH_MP_TAC(REAL_ARITH
`abs((f - f') * g) <= a * n /\ abs((g - g') * f') <= b * n
==> abs(f * g - f' * g') <= (a + b) * n`) THEN
ONCE_REWRITE_TAC[REAL_ARITH `(a * b) * c:real = (a * c) * b`] THEN
REWRITE_TAC[
REAL_ABS_MUL] THEN
CONJ_TAC THEN MATCH_MP_TAC
REAL_LE_MUL2 THEN
ASM_SIMP_TAC[
REAL_ABS_POS] THEN MATCH_MP_TAC(REAL_ARITH
`abs(g x - g a) <= C *
norm(x - a) /\
C *
norm(x - a:real^N) <= C * B ==> abs(g x) <= abs(g a) + C * B`) THEN
ASM_SIMP_TAC[
REAL_LE_LMUL_EQ] THEN MATCH_MP_TAC(NORM_ARITH
`
norm x <= B /\
norm a <= B ==>
norm(x - a:real^N) <= &2 * B`) THEN
ASM_SIMP_TAC[]]]);;
(* ------------------------------------------------------------------------- *)
(* Differentiability of real and vector polynomial functions. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Specific properties of complex measurable functions. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Measurable real->real functions. *)
(* ------------------------------------------------------------------------- *)
parse_as_infix("real_measurable_on",(12,"right"));;
(* ------------------------------------------------------------------------- *)
(* Properties of real Lebesgue measurable sets. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Various common equivalent forms of function measurability. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Continuity of measure within a halfspace w.r.t. to the boundary. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Second mean value theorem and monotone integrability. *)
(* ------------------------------------------------------------------------- *)
let REAL_SECOND_MEAN_VALUE_THEOREM_GEN_FULL = prove
(`!f g a b u v.
~(
real_interval[a,b] = {}) /\
f
real_integrable_on real_interval[a,b] /\
(!x. x
IN real_interval(a,b) ==> u <= g x /\ g x <= v) /\
(!x y. x
IN real_interval[a,b] /\ y
IN real_interval[a,b] /\ x <= y
==> g x <= g y)
==> ?c. c
IN real_interval[a,b] /\
((\x. g x * f x)
has_real_integral
(u *
real_integral (
real_interval[a,c]) f +
v *
real_integral (
real_interval[c,b]) f))
(
real_interval[a,b])`,
let REAL_SECOND_MEAN_VALUE_THEOREM_GEN = prove
(`!f g a b u v.
~(
real_interval[a,b] = {}) /\
f
real_integrable_on real_interval[a,b] /\
(!x. x
IN real_interval(a,b) ==> u <= g x /\ g x <= v) /\
(!x y. x
IN real_interval[a,b] /\ y
IN real_interval[a,b] /\ x <= y
==> g x <= g y)
==> ?c. c
IN real_interval[a,b] /\
real_integral (
real_interval[a,b]) (\x. g x * f x) =
u *
real_integral (
real_interval[a,c]) f +
v *
real_integral (
real_interval[c,b]) f`,
(* ------------------------------------------------------------------------- *)
(* Measurability and absolute integrability of monotone functions. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Real functions of bounded variation. *)
(* ------------------------------------------------------------------------- *)
parse_as_infix("has_bounded_real_variation_on",(12,"right"));;
let HAS_BOUNDED_REAL_VARIATION_DARBOUX_STRONG = prove
(`!f a b.
f
has_bounded_real_variation_on real_interval[a,b]
==> ?g h.
(!x. f x = g x - h x) /\
(!x y. x
IN real_interval[a,b] /\ y
IN real_interval[a,b] /\ x <= y
==> g x <= g y) /\
(!x y. x
IN real_interval[a,b] /\ y
IN real_interval[a,b] /\ x <= y
==> h x <= h y) /\
(!x y. x
IN real_interval[a,b] /\ y
IN real_interval[a,b] /\ x < y
==> g x < g y) /\
(!x y. x
IN real_interval[a,b] /\ y
IN real_interval[a,b] /\ x < y
==> h x < h y) /\
(!x. x
IN real_interval[a,b] /\
f
real_continuous (
atreal x
within real_interval[a,x])
==> g
real_continuous (
atreal x
within real_interval[a,x]) /\
h
real_continuous (
atreal x
within real_interval[a,x])) /\
(!x. x
IN real_interval[a,b] /\
f
real_continuous (
atreal x
within real_interval[x,b])
==> g
real_continuous (
atreal x
within real_interval[x,b]) /\
h
real_continuous (
atreal x
within real_interval[x,b])) /\
(!x. x
IN real_interval[a,b] /\
f
real_continuous (
atreal x
within real_interval[a,b])
==> g
real_continuous (
atreal x
within real_interval[a,b]) /\
h
real_continuous (
atreal x
within real_interval[a,b]))`,
(* ------------------------------------------------------------------------- *)
(* Lebesgue density theorem. This isn't about R specifically, but it's most *)
(* naturally stated as a real limit so it ends up here in this file. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Injective map into R is also an open map w.r.t. the universe, and this *)
(* is actually an implication in both directions for an interval. Compare *)
(* the local form in INJECTIVE_INTO_1D_IMP_OPEN_MAP (not a bi-implication). *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Map f:S^m->S^n for m < n is nullhomotopic. *)
(* ------------------------------------------------------------------------- *)
let INESSENTIAL_SPHEREMAP_LOWDIM_GEN = prove
(`!f:real^M->real^N s t.
convex s /\
bounded s /\
convex t /\
bounded t /\
aff_dim s <
aff_dim t /\
f
continuous_on relative_frontier s /\
IMAGE f (
relative_frontier s)
SUBSET (
relative_frontier t)
==> ?c.
homotopic_with (\z. T)
(
relative_frontier s,
relative_frontier t) f (\x. c)`,
let lemma1 = prove
(`!f:real^N->real^N s t.
subspace s /\ subspace t /\ dim s < dim t /\ s SUBSET t /\
f differentiable_on sphere(vec 0,&1) INTER s
==> ~(IMAGE f (sphere(vec 0,&1) INTER s) = sphere(vec 0,&1) INTER t)`,
REPEAT STRIP_TAC THEN
ABBREV_TAC
`(g:real^N->real^N) =
\x. norm(x) % (f:real^N->real^N)(inv(norm x) % x)` THEN
SUBGOAL_THEN
`(g:real^N->real^N) differentiable_on s DELETE (vec 0)`
ASSUME_TAC THENL
[EXPAND_TAC "g" THEN MATCH_MP_TAC DIFFERENTIABLE_ON_MUL THEN
SIMP_TAC[o_DEF; DIFFERENTIABLE_ON_NORM; IN_DELETE] THEN
GEN_REWRITE_TAC LAND_CONV [GSYM o_DEF] THEN
MATCH_MP_TAC DIFFERENTIABLE_ON_COMPOSE THEN CONJ_TAC THENL
[MATCH_MP_TAC DIFFERENTIABLE_ON_MUL THEN
REWRITE_TAC[DIFFERENTIABLE_ON_ID] THEN
SUBGOAL_THEN
`lift o (\x:real^N. inv(norm x)) =
(lift o inv o drop) o (\x. lift(norm x))`
SUBST1_TAC THENL [REWRITE_TAC[o_DEF; LIFT_DROP]; ALL_TAC] THEN
MATCH_MP_TAC DIFFERENTIABLE_ON_COMPOSE THEN
SIMP_TAC[DIFFERENTIABLE_ON_NORM; IN_DELETE] THEN
MATCH_MP_TAC DIFFERENTIABLE_AT_IMP_DIFFERENTIABLE_ON THEN
SIMP_TAC[FORALL_IN_IMAGE; IN_DELETE; GSYM REAL_DIFFERENTIABLE_AT] THEN
REPEAT STRIP_TAC THEN GEN_REWRITE_TAC LAND_CONV [GSYM ETA_AX] THEN
MATCH_MP_TAC REAL_DIFFERENTIABLE_INV_ATREAL THEN
ASM_REWRITE_TAC[REAL_DIFFERENTIABLE_ID; NORM_EQ_0];
FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REWRITE_RULE[IMP_CONJ]
DIFFERENTIABLE_ON_SUBSET)) THEN
ASM_SIMP_TAC[SUBSET; FORALL_IN_IMAGE; IN_SPHERE_0; IN_INTER;
SUBSPACE_MUL; NORM_MUL; IN_DELETE] THEN
SIMP_TAC[REAL_ABS_INV; REAL_ABS_NORM; REAL_MUL_LINV; NORM_EQ_0]];
ALL_TAC] THEN
SUBGOAL_THEN
`IMAGE (g:real^N->real^N) (s DELETE vec 0) = t DELETE (vec 0)`
ASSUME_TAC THENL
[UNDISCH_TAC `IMAGE (f:real^N->real^N) (sphere (vec 0,&1) INTER s) =
sphere (vec 0,&1) INTER t` THEN
REWRITE_TAC[GSYM SUBSET_ANTISYM_EQ] THEN
REWRITE_TAC[SUBSET; FORALL_IN_IMAGE; IN_DELETE;
IN_INTER; IN_SPHERE_0] THEN
EXPAND_TAC "g" THEN REWRITE_TAC[IN_IMAGE; IN_INTER; IN_SPHERE_0] THEN
SIMP_TAC[IN_DELETE; VECTOR_MUL_EQ_0; NORM_EQ_0] THEN
MATCH_MP_TAC(TAUT
`(p ==> r) /\ (p ==> q ==> s) ==> p /\ q ==> r /\ s`) THEN
CONJ_TAC THENL [ALL_TAC; DISCH_TAC] THEN
DISCH_THEN(fun th -> X_GEN_TAC `x:real^N` THEN STRIP_TAC THEN
MP_TAC(SPEC `inv(norm x) % x:real^N` th)) THEN
ASM_SIMP_TAC[SUBSPACE_MUL; NORM_MUL; REAL_ABS_INV; REAL_ABS_NORM;
REAL_MUL_LINV; NORM_EQ_0;
NORM_ARITH `norm x = &1 ==> ~(x:real^N = vec 0)`] THEN
DISCH_THEN(X_CHOOSE_THEN `y:real^N` STRIP_ASSUME_TAC) THEN
EXISTS_TAC `norm(x:real^N) % y:real^N` THEN
ASM_SIMP_TAC[SUBSPACE_MUL; NORM_MUL; REAL_ABS_NORM; REAL_MUL_RID] THEN
ASM_SIMP_TAC[VECTOR_MUL_ASSOC; REAL_MUL_LINV; NORM_EQ_0] THEN
ASM_REWRITE_TAC[VECTOR_MUL_LID; VECTOR_MUL_EQ_0; NORM_EQ_0] THEN
ASM_SIMP_TAC[NORM_ARITH `norm x = &1 ==> ~(x:real^N = vec 0)`] THEN
UNDISCH_THEN `inv(norm x) % x = (f:real^N->real^N) y`
(SUBST1_TAC o SYM) THEN
ASM_SIMP_TAC[VECTOR_MUL_ASSOC; REAL_MUL_RINV; NORM_EQ_0] THEN
REWRITE_TAC[VECTOR_MUL_LID];
ALL_TAC] THEN
MP_TAC(ISPECL [`t:real^N->bool`; `(:real^N)`]
DIM_SUBSPACE_ORTHOGONAL_TO_VECTORS) THEN
ASM_REWRITE_TAC[SUBSPACE_UNIV; DIM_UNIV; IN_UNIV; SUBSET_UNIV] THEN
ABBREV_TAC `t' = {y:real^N | !x. x IN t ==> orthogonal x y}` THEN
DISCH_TAC THEN
SUBGOAL_THEN `subspace(t':real^N->bool)` ASSUME_TAC THENL
[EXPAND_TAC "t'" THEN REWRITE_TAC[SUBSPACE_ORTHOGONAL_TO_VECTORS];
ALL_TAC] THEN
SUBGOAL_THEN
`?fst snd. linear fst /\ linear snd /\
(!z. fst(z) IN t /\ snd z IN t' /\ fst z + snd z = z) /\
(!x y:real^N. x IN t /\ y IN t'
==> fst(x + y) = x /\ snd(x + y) = y)`
STRIP_ASSUME_TAC THENL
[MP_TAC(ISPEC `t:real^N->bool` ORTHOGONAL_SUBSPACE_DECOMP_EXISTS) THEN
REWRITE_TAC[SKOLEM_THM] THEN
MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `fst:real^N->real^N` THEN
MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `snd:real^N->real^N` THEN
DISCH_THEN(MP_TAC o GSYM) THEN
ASM_SIMP_TAC[SPAN_OF_SUBSPACE; FORALL_AND_THM] THEN STRIP_TAC THEN
MATCH_MP_TAC(TAUT `r /\ (r ==> p /\ q /\ s) ==> p /\ q /\ r /\ s`) THEN
CONJ_TAC THENL
[EXPAND_TAC "t'" THEN REWRITE_TAC[IN_ELIM_THM] THEN
ASM_MESON_TAC[ORTHOGONAL_SYM];
DISCH_TAC] THEN
MATCH_MP_TAC(TAUT `r /\ (r ==> p /\ q) ==> p /\ q /\ r`) THEN
CONJ_TAC THENL
[REPEAT GEN_TAC THEN STRIP_TAC THEN
MATCH_MP_TAC ORTHOGONAL_SUBSPACE_DECOMP_UNIQUE THEN
MAP_EVERY EXISTS_TAC [`t:real^N->bool`; `t':real^N->bool`] THEN
ASM_SIMP_TAC[SPAN_OF_SUBSPACE] THEN ASM SET_TAC[];
DISCH_TAC] THEN
REWRITE_TAC[linear] THEN
MATCH_MP_TAC(TAUT `(p /\ r) /\ (q /\ s) ==> (p /\ q) /\ (r /\ s)`) THEN
REWRITE_TAC[AND_FORALL_THM] THEN CONJ_TAC THEN REPEAT GEN_TAC THEN
MATCH_MP_TAC ORTHOGONAL_SUBSPACE_DECOMP_UNIQUE THEN
MAP_EVERY EXISTS_TAC [`t:real^N->bool`; `t':real^N->bool`] THEN
ASM_SIMP_TAC[SPAN_OF_SUBSPACE; SUBSPACE_ADD; SUBSPACE_MUL] THEN
(CONJ_TAC THENL [ASM SET_TAC[]; ALL_TAC]) THEN
ASM_REWRITE_TAC[GSYM VECTOR_ADD_LDISTRIB] THEN
ONCE_REWRITE_TAC[VECTOR_ARITH
`(x + y) + (x' + y'):real^N = (x + x') + (y + y')`] THEN
ASM_REWRITE_TAC[];
ALL_TAC] THEN
MP_TAC(ISPECL
[`\x:real^N. (g:real^N->real^N)(fst x) + snd x`;
`{x + y:real^N | x IN (s DELETE vec 0) /\ y IN t'}`]
NEGLIGIBLE_DIFFERENTIABLE_IMAGE_NEGLIGIBLE) THEN
REWRITE_TAC[LE_REFL; NOT_IMP] THEN REPEAT CONJ_TAC THENL
[MATCH_MP_TAC NEGLIGIBLE_LOWDIM THEN
MP_TAC(ISPECL [`s:real^N->bool`; `t':real^N->bool`] DIM_SUMS_INTER) THEN
ASM_REWRITE_TAC[IN_DELETE] THEN
FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP (ARITH_RULE
`t' + t = n ==> s < t /\ d' <= d /\ i = 0
==> d + i = s + t' ==> d' < n`)) THEN
ASM_REWRITE_TAC[DIM_EQ_0] THEN CONJ_TAC THENL
[MATCH_MP_TAC DIM_SUBSET THEN SET_TAC[]; EXPAND_TAC "t'"] THEN
REWRITE_TAC[SUBSET; IN_INTER; IN_SING; IN_ELIM_THM] THEN
ASM_MESON_TAC[SUBSET; ORTHOGONAL_REFL];
MATCH_MP_TAC DIFFERENTIABLE_ON_ADD THEN
ASM_SIMP_TAC[DIFFERENTIABLE_ON_LINEAR] THEN
GEN_REWRITE_TAC LAND_CONV [GSYM o_DEF] THEN
MATCH_MP_TAC DIFFERENTIABLE_ON_COMPOSE THEN
ASM_SIMP_TAC[DIFFERENTIABLE_ON_LINEAR] THEN
FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REWRITE_RULE[IMP_CONJ]
DIFFERENTIABLE_ON_SUBSET)) THEN
REWRITE_TAC[SUBSET; FORALL_IN_IMAGE; FORALL_IN_GSPEC] THEN
RULE_ASSUM_TAC(REWRITE_RULE[SUBSET]) THEN ASM_SIMP_TAC[IN_DELETE];
SUBGOAL_THEN
`~negligible {x + y | x IN IMAGE (g:real^N->real^N) (s DELETE vec 0) /\
y IN t'}`
MP_TAC THENL
[ASM_REWRITE_TAC[] THEN
SUBGOAL_THEN `negligible(t':real^N->bool)` MP_TAC THENL
[MATCH_MP_TAC NEGLIGIBLE_LOWDIM THEN ASM_ARITH_TAC;
REWRITE_TAC[TAUT `p ==> ~q <=> ~(p /\ q)`]] THEN
REWRITE_TAC[GSYM NEGLIGIBLE_UNION_EQ] THEN
MP_TAC NOT_NEGLIGIBLE_UNIV THEN MATCH_MP_TAC EQ_IMP THEN
AP_TERM_TAC THEN AP_TERM_TAC THEN
REWRITE_TAC[EXTENSION; IN_UNION; IN_UNIV; IN_ELIM_THM; IN_DELETE] THEN
X_GEN_TAC `z:real^N` THEN
REWRITE_TAC[TAUT `p \/ q <=> ~p ==> q`] THEN DISCH_TAC THEN
EXISTS_TAC `(fst:real^N->real^N) z` THEN
EXISTS_TAC `(snd:real^N->real^N) z` THEN
ASM_SIMP_TAC[] THEN ASM_MESON_TAC[VECTOR_ADD_LID];
REWRITE_TAC[CONTRAPOS_THM] THEN
MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ_ALT] NEGLIGIBLE_SUBSET) THEN
REWRITE_TAC[SUBSET; FORALL_IN_GSPEC; IMP_CONJ; RIGHT_FORALL_IMP_THM;
FORALL_IN_IMAGE; IN_DELETE] THEN
X_GEN_TAC `x:real^N` THEN REPEAT DISCH_TAC THEN
X_GEN_TAC `y:real^N` THEN DISCH_TAC THEN
REWRITE_TAC[IN_IMAGE] THEN EXISTS_TAC `x + y:real^N` THEN
RULE_ASSUM_TAC(REWRITE_RULE[SUBSET]) THEN ASM_SIMP_TAC[] THEN ASM
SET_TAC[]]]) in
let lemma2 = prove
(`!f:real^N->real^N s t.
subspace s /\ subspace t /\ dim s < dim t /\ s SUBSET t /\
f continuous_on sphere(vec 0,&1) INTER s /\
IMAGE f (sphere(vec 0,&1) INTER s) SUBSET sphere(vec 0,&1) INTER t
==> ?c. homotopic_with (\x. T)
(sphere(vec 0,&1) INTER s,sphere(vec 0,&1) INTER t)
f (\x. c)`,
REPEAT STRIP_TAC THEN
MP_TAC(ISPECL [`f:real^N->real^N`; `sphere(vec 0:real^N,&1) INTER s`;
`&1 / &2`; `t:real^N->bool`;]
STONE_WEIERSTRASS_VECTOR_POLYNOMIAL_FUNCTION_SUBSPACE) THEN
CONV_TAC REAL_RAT_REDUCE_CONV THEN
ASM_SIMP_TAC[COMPACT_INTER_CLOSED; COMPACT_SPHERE; CLOSED_SUBSPACE] THEN
ANTS_TAC THENL [ASM SET_TAC[]; REWRITE_TAC[SUBSET; FORALL_IN_IMAGE]] THEN
DISCH_THEN(X_CHOOSE_THEN `g:real^N->real^N` STRIP_ASSUME_TAC) THEN
SUBGOAL_THEN
`!x. x IN sphere(vec 0,&1) INTER s ==> ~((g:real^N->real^N) x = vec 0)`
ASSUME_TAC THENL
[X_GEN_TAC `x:real^N` THEN STRIP_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPEC `x:real^N`) THEN ASM_REWRITE_TAC[] THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [SUBSET]) THEN
REWRITE_TAC[FORALL_IN_IMAGE; IN_SPHERE_0] THEN
RULE_ASSUM_TAC(REWRITE_RULE[IN_SPHERE_0]) THEN
DISCH_THEN(MP_TAC o SPEC `x:real^N`) THEN
ASM_REWRITE_TAC[] THEN REWRITE_TAC[IN_INTER; IN_SPHERE_0] THEN
CONV_TAC NORM_ARITH;
ALL_TAC] THEN
SUBGOAL_THEN `(g:real^N->real^N) differentiable_on
sphere(vec 0,&1) INTER s`
ASSUME_TAC THENL
[ASM_SIMP_TAC[DIFFERENTIABLE_ON_VECTOR_POLYNOMIAL_FUNCTION]; ALL_TAC] THEN
ABBREV_TAC `(h:real^N->real^N) = \x. inv(norm(g x)) % g x` THEN
SUBGOAL_THEN
`!x. x IN sphere(vec 0,&1) INTER s
==> (h:real^N->real^N) x IN sphere(vec 0,&1) INTER t`
ASSUME_TAC THENL
[REPEAT STRIP_TAC THEN EXPAND_TAC "h" THEN
ASM_SIMP_TAC[SUBSPACE_MUL; IN_INTER; IN_SPHERE_0; NORM_MUL] THEN
REWRITE_TAC[REAL_ABS_INV; REAL_ABS_NORM] THEN
ASM_SIMP_TAC[REAL_MUL_LINV; NORM_EQ_0; GSYM IN_SPHERE_0];
ALL_TAC] THEN
SUBGOAL_THEN
`(h:real^N->real^N) differentiable_on sphere(vec 0,&1) INTER s`
ASSUME_TAC THENL
[EXPAND_TAC "h" THEN MATCH_MP_TAC DIFFERENTIABLE_ON_MUL THEN
ASM_SIMP_TAC[DIFFERENTIABLE_ON_VECTOR_POLYNOMIAL_FUNCTION; o_DEF] THEN
SUBGOAL_THEN
`(\x. lift(inv(norm((g:real^N->real^N) x)))) =
(lift o inv o drop) o (\x. lift(norm x)) o (g:real^N->real^N)`
SUBST1_TAC THENL [REWRITE_TAC[o_DEF; LIFT_DROP]; ALL_TAC] THEN
MATCH_MP_TAC DIFFERENTIABLE_ON_COMPOSE THEN CONJ_TAC THENL
[MATCH_MP_TAC DIFFERENTIABLE_ON_COMPOSE THEN
ASM_SIMP_TAC[DIFFERENTIABLE_ON_VECTOR_POLYNOMIAL_FUNCTION] THEN
MATCH_MP_TAC DIFFERENTIABLE_ON_NORM THEN
ASM_REWRITE_TAC[SET_RULE
`~(z IN IMAGE f s) <=> !x. x IN s ==> ~(f x = z)`];
MATCH_MP_TAC DIFFERENTIABLE_AT_IMP_DIFFERENTIABLE_ON THEN
REWRITE_TAC[GSYM REAL_DIFFERENTIABLE_AT] THEN
REWRITE_TAC[FORALL_IN_IMAGE; IN_SPHERE_0] THEN
X_GEN_TAC `x:real^N` THEN
ASM_CASES_TAC `x:real^N = vec 0` THEN
ASM_REWRITE_TAC[NORM_0; REAL_OF_NUM_EQ; ARITH_EQ] THEN DISCH_TAC THEN
REWRITE_TAC[GSYM REAL_DIFFERENTIABLE_AT; o_THM] THEN
GEN_REWRITE_TAC LAND_CONV [GSYM ETA_AX] THEN
MATCH_MP_TAC REAL_DIFFERENTIABLE_INV_ATREAL THEN
ASM_SIMP_TAC[REAL_DIFFERENTIABLE_ID; NORM_EQ_0; IN_SPHERE_0]];
ALL_TAC] THEN
SUBGOAL_THEN
`?c. homotopic_with (\z. T)
(sphere(vec 0,&1) INTER s,sphere(vec 0,&1) INTER t)
(h:real^N->real^N) (\x. c)`
MP_TAC THENL
[ALL_TAC;
MATCH_MP_TAC MONO_EXISTS THEN GEN_TAC THEN
MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ] HOMOTOPIC_WITH_TRANS) THEN
SUBGOAL_THEN
`homotopic_with (\z. T)
(sphere(vec 0:real^N,&1) INTER s,t DELETE (vec 0:real^N))
f g`
MP_TAC THENL
[MATCH_MP_TAC HOMOTOPIC_WITH_LINEAR THEN
ASM_SIMP_TAC[CONTINUOUS_ON_VECTOR_POLYNOMIAL_FUNCTION] THEN
X_GEN_TAC `x:real^N` THEN DISCH_TAC THEN REWRITE_TAC[SET_RULE
`s SUBSET t DELETE v <=> s SUBSET t /\ ~(v IN s)`] THEN
CONJ_TAC THENL
[REWRITE_TAC[SEGMENT_CONVEX_HULL] THEN MATCH_MP_TAC HULL_MINIMAL THEN
ASM_SIMP_TAC[SUBSPACE_IMP_CONVEX] THEN ASM SET_TAC[];
DISCH_THEN(MP_TAC o MATCH_MP SEGMENT_BOUND) THEN
SUBGOAL_THEN
`(f:real^N->real^N) x IN sphere(vec 0,&1) /\
norm(f x - g x) < &1/ &2`
MP_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
REWRITE_TAC[IN_SPHERE_0] THEN CONV_TAC NORM_ARITH];
DISCH_THEN(MP_TAC o
ISPECL [`\y:real^N. inv(norm y) % y`;
`sphere(vec 0:real^N,&1) INTER t`] o
MATCH_MP (ONCE_REWRITE_RULE[IMP_CONJ]
HOMOTOPIC_COMPOSE_CONTINUOUS_LEFT)) THEN
ASM_REWRITE_TAC[o_DEF] THEN ANTS_TAC THENL
[CONJ_TAC THENL
[MATCH_MP_TAC CONTINUOUS_ON_MUL THEN
REWRITE_TAC[o_DEF; CONTINUOUS_ON_ID] THEN
MATCH_MP_TAC(REWRITE_RULE[o_DEF] CONTINUOUS_ON_INV) THEN
SIMP_TAC[IN_DELETE; NORM_EQ_0] THEN
REWRITE_TAC[REWRITE_RULE[o_DEF] CONTINUOUS_ON_LIFT_NORM];
REWRITE_TAC[SUBSET; FORALL_IN_IMAGE; IN_DELETE; IN_INTER] THEN
ASM_SIMP_TAC[SUBSPACE_MUL; IN_SPHERE_0; NORM_MUL; REAL_ABS_MUL] THEN
SIMP_TAC[REAL_ABS_INV; REAL_ABS_NORM; REAL_MUL_LINV; NORM_EQ_0]];
MATCH_MP_TAC(ONCE_REWRITE_RULE[IMP_CONJ_ALT] HOMOTOPIC_WITH_EQ) THEN
RULE_ASSUM_TAC(REWRITE_RULE
[SUBSET; IN_INTER; FORALL_IN_IMAGE; IN_SPHERE_0]) THEN
ASM_SIMP_TAC[IN_SPHERE_0; IN_INTER;
REAL_INV_1; VECTOR_MUL_LID]]]] THEN
SUBGOAL_THEN
`?c. c IN (sphere(vec 0,&1) INTER t) DIFF
(IMAGE (h:real^N->real^N) (sphere(vec 0,&1) INTER s))`
MP_TAC THENL
[MATCH_MP_TAC(SET_RULE
`t SUBSET s /\ ~(t = s) ==> ?a. a IN s DIFF t`) THEN
CONJ_TAC THENL [ASM SET_TAC[]; MATCH_MP_TAC lemma1] THEN
ASM_REWRITE_TAC[];
REWRITE_TAC[LEFT_IMP_EXISTS_THM; IN_INTER; IN_DIFF; IN_IMAGE] THEN
REWRITE_TAC[SET_RULE
`~(?x. P x /\ x IN s /\ x IN t) <=>
(!x. x IN s INTER t ==> ~(P x))`] THEN
X_GEN_TAC `c:real^N` THEN STRIP_TAC] THEN
EXISTS_TAC `--c:real^N` THEN
SUBGOAL_THEN
`homotopic_with (\z. T)
(sphere(vec 0:real^N,&1) INTER s,t DELETE (vec 0:real^N))
h (\x. --c)`
MP_TAC THENL
[MATCH_MP_TAC HOMOTOPIC_WITH_LINEAR THEN
ASM_SIMP_TAC[DIFFERENTIABLE_IMP_CONTINUOUS_ON; CONTINUOUS_ON_CONST] THEN
X_GEN_TAC `x:real^N` THEN DISCH_TAC THEN REWRITE_TAC[SET_RULE
`s SUBSET t DELETE v <=> s SUBSET t /\ ~(v IN s)`] THEN
CONJ_TAC THENL
[REWRITE_TAC[SEGMENT_CONVEX_HULL] THEN MATCH_MP_TAC HULL_MINIMAL THEN
ASM_SIMP_TAC[SUBSPACE_IMP_CONVEX; INSERT_SUBSET; SUBSPACE_NEG] THEN
ASM SET_TAC[];
DISCH_TAC THEN MP_TAC(ISPECL
[`(h:real^N->real^N) x`; `vec 0:real^N`; `--c:real^N`]
MIDPOINT_BETWEEN) THEN
ASM_REWRITE_TAC[BETWEEN_IN_SEGMENT; DIST_0; NORM_NEG] THEN
SUBGOAL_THEN `((h:real^N->real^N) x) IN sphere(vec 0,&1) /\
(c:real^N) IN sphere(vec 0,&1)`
MP_TAC THENL [ASM SET_TAC[]; SIMP_TAC[IN_SPHERE_0]] THEN
STRIP_TAC THEN REWRITE_TAC[midpoint; VECTOR_ARITH
`vec 0:real^N = inv(&2) % (x + --y) <=> x = y`] THEN
ASM SET_TAC[]];
DISCH_THEN(MP_TAC o
ISPECL [`\y:real^N. inv(norm y) % y`;
`sphere(vec 0:real^N,&1) INTER t`] o
MATCH_MP (ONCE_REWRITE_RULE[IMP_CONJ]
HOMOTOPIC_COMPOSE_CONTINUOUS_LEFT)) THEN
ASM_REWRITE_TAC[o_DEF] THEN ANTS_TAC THENL
[CONJ_TAC THENL
[MATCH_MP_TAC CONTINUOUS_ON_MUL THEN
REWRITE_TAC[o_DEF; CONTINUOUS_ON_ID] THEN
MATCH_MP_TAC(REWRITE_RULE[o_DEF] CONTINUOUS_ON_INV) THEN
SIMP_TAC[IN_DELETE; NORM_EQ_0] THEN
REWRITE_TAC[REWRITE_RULE[o_DEF] CONTINUOUS_ON_LIFT_NORM];
REWRITE_TAC[SUBSET; FORALL_IN_IMAGE; IN_DELETE; IN_INTER] THEN
ASM_SIMP_TAC[SUBSPACE_MUL; IN_SPHERE_0; NORM_MUL; REAL_ABS_MUL] THEN
SIMP_TAC[REAL_ABS_INV; REAL_ABS_NORM; REAL_MUL_LINV; NORM_EQ_0]];
MATCH_MP_TAC(ONCE_REWRITE_RULE[IMP_CONJ_ALT] HOMOTOPIC_WITH_EQ) THEN
RULE_ASSUM_TAC(REWRITE_RULE
[SUBSET; IN_INTER; FORALL_IN_IMAGE; IN_SPHERE_0]) THEN
ASM_SIMP_TAC[IN_SPHERE_0; IN_INTER; REAL_INV_1; VECTOR_MUL_LID;
NORM_NEG]]]) in
let lemma3 = prove
(`!s:real^M->bool u:real^N->bool.
bounded s /\ convex s /\ subspace u /\ aff_dim s <= &(dim u)
==> ?t. subspace t /\ t SUBSET u /\
(~(s = {}) ==> aff_dim t = aff_dim s) /\
(relative_frontier s) homeomorphic
(sphere(vec 0,&1) INTER t)`,
REPEAT GEN_TAC THEN ASM_CASES_TAC `s:real^M->bool = {}` THENL
[STRIP_TAC THEN EXISTS_TAC `{vec 0:real^N}` THEN
ASM_REWRITE_TAC[SUBSPACE_TRIVIAL; RELATIVE_FRONTIER_EMPTY] THEN
ASM_SIMP_TAC[HOMEOMORPHIC_EMPTY;
SET_RULE `s INTER {a} = {} <=> ~(a IN s)`;
IN_SPHERE_0; NORM_0; SING_SUBSET; SUBSPACE_0] THEN
CONV_TAC REAL_RAT_REDUCE_CONV;
FIRST_X_ASSUM(X_CHOOSE_THEN `a:real^M` MP_TAC o
GEN_REWRITE_RULE I [GSYM MEMBER_NOT_EMPTY]) THEN
GEOM_ORIGIN_TAC `a:real^M` THEN
SIMP_TAC[AFF_DIM_DIM_0; HULL_INC; INT_OF_NUM_LE; GSYM DIM_UNIV] THEN
REPEAT STRIP_TAC] THEN
FIRST_ASSUM(MP_TAC o MATCH_MP CHOOSE_SUBSPACE_OF_SUBSPACE) THEN
MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `t:real^N->bool` THEN
ASM_SIMP_TAC[SPAN_OF_SUBSPACE; AFF_DIM_DIM_SUBSPACE; INT_OF_NUM_EQ] THEN
STRIP_TAC THEN
TRANS_TAC HOMEOMORPHIC_TRANS
`relative_frontier(ball(vec 0:real^N,&1) INTER t)` THEN
CONJ_TAC THENL
[MATCH_MP_TAC HOMEOMORPHIC_RELATIVE_FRONTIERS_CONVEX_BOUNDED_SETS THEN
ASM_SIMP_TAC[CONVEX_INTER; BOUNDED_INTER; BOUNDED_BALL;
SUBSPACE_IMP_CONVEX; CONVEX_BALL] THEN
ONCE_REWRITE_TAC[INTER_COMM] THEN
FIRST_ASSUM(ASSUME_TAC o MATCH_MP SUBSPACE_0) THEN
SUBGOAL_THEN `~(t INTER ball(vec 0:real^N,&1) = {})` ASSUME_TAC THENL
[REWRITE_TAC[GSYM MEMBER_NOT_EMPTY] THEN EXISTS_TAC `vec 0:real^N` THEN
ASM_REWRITE_TAC[IN_INTER; CENTRE_IN_BALL; REAL_LT_01];
ASM_SIMP_TAC[AFF_DIM_CONVEX_INTER_OPEN; OPEN_BALL;
SUBSPACE_IMP_CONVEX] THEN
ASM_SIMP_TAC[AFF_DIM_DIM_0; HULL_INC]];
MATCH_MP_TAC(MESON[HOMEOMORPHIC_REFL] `s = t ==> s homeomorphic t`) THEN
SIMP_TAC[GSYM FRONTIER_BALL; REAL_LT_01] THEN
MATCH_MP_TAC RELATIVE_FRONTIER_CONVEX_INTER_AFFINE THEN
ASM_SIMP_TAC[CONVEX_BALL; SUBSPACE_IMP_AFFINE;
GSYM MEMBER_NOT_EMPTY] THEN
EXISTS_TAC `vec 0:real^N` THEN
ASM_SIMP_TAC[CENTRE_IN_BALL; INTERIOR_OPEN; OPEN_BALL;
SUBSPACE_0; IN_INTER; REAL_LT_01]]) in
ONCE_REWRITE_TAC[MESON[] `(!a b c. P a b c) <=> (!b c a. P a b c)`] THEN
REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN
REWRITE_TAC[IMP_IMP] THEN ONCE_REWRITE_TAC[RIGHT_IMP_FORALL_THM] THEN
REWRITE_TAC[IMP_IMP; GSYM CONJ_ASSOC] THEN REPEAT GEN_TAC THEN
ASM_CASES_TAC `s:real^M->bool = {}` THENL
[ASM_SIMP_TAC[HOMOTOPIC_WITH; RELATIVE_FRONTIER_EMPTY; PCROSS_EMPTY;
NOT_IN_EMPTY; IMAGE_CLAUSES; CONTINUOUS_ON_EMPTY];
ALL_TAC] THEN
ASM_CASES_TAC `t:real^N->bool = {}` THEN
ASM_SIMP_TAC[AFF_DIM_EMPTY; GSYM INT_NOT_LE; AFF_DIM_GE] THEN
STRIP_TAC THEN
MP_TAC(ISPECL [`t:real^N->bool`; `(:real^N)`] lemma3) THEN
ASM_REWRITE_TAC[DIM_UNIV; SUBSPACE_UNIV; AFF_DIM_LE_UNIV] THEN
DISCH_THEN(X_CHOOSE_THEN `t':real^N->bool` STRIP_ASSUME_TAC) THEN
FIRST_ASSUM(MP_TAC o MATCH_MP HOMEOMORPHIC_IMP_HOMOTOPY_EQUIVALENT) THEN
DISCH_THEN(fun th -> REWRITE_TAC[MATCH_MP
HOMOTOPY_EQUIVALENT_HOMOTOPIC_TRIVIALITY_NULL th]) THEN
MP_TAC(ISPECL [`s:real^M->bool`; `t':real^N->bool`] lemma3) THEN
ASM_SIMP_TAC[GSYM AFF_DIM_DIM_SUBSPACE] THEN
ANTS_TAC THENL [ASM_INT_ARITH_TAC; ALL_TAC] THEN
DISCH_THEN(X_CHOOSE_THEN `s':real^N->bool` STRIP_ASSUME_TAC) THEN
FIRST_ASSUM(MP_TAC o MATCH_MP HOMEOMORPHIC_IMP_HOMOTOPY_EQUIVALENT) THEN
DISCH_THEN(fun th -> REWRITE_TAC[MATCH_MP
HOMOTOPY_EQUIVALENT_COHOMOTOPIC_TRIVIALITY_NULL th]) THEN
REPEAT STRIP_TAC THEN MATCH_MP_TAC lemma2 THEN
ASM_SIMP_TAC[GSYM INT_OF_NUM_LT; GSYM AFF_DIM_DIM_SUBSPACE] THEN
ASM_INT_ARITH_TAC);;
let HOMEOMORPHIC_SPHERES_EQ,HOMOTOPY_EQUIVALENT_SPHERES_EQ =
(CONJ_PAIR o prove)
(`(!a:real^M b:real^N r s.
sphere(a,r) homeomorphic sphere(b,s) <=>
r < &0 /\ s < &0 \/ r = &0 /\ s = &0 \/
&0 < r /\ &0 < s /\ dimindex(:M) = dimindex(:N)) /\
(!a:real^M b:real^N r s.
sphere(a,r) homotopy_equivalent sphere(b,s) <=>
r < &0 /\ s < &0 \/ r = &0 /\ s = &0 \/
&0 < r /\ &0 < s /\ dimindex(:M) = dimindex(:N))`,
let lemma = prove
(`!a:real^M r b:real^N s.
dimindex(:M) <
dimindex(:N) /\ &0 < r /\ &0 < s
==> ~(
sphere(a,r)
homotopy_equivalent sphere(b,s))`,
REPEAT STRIP_TAC THEN
FIRST_ASSUM(MP_TAC o ISPEC `
sphere(a:real^M,r)` o
MATCH_MP
HOMOTOPY_EQUIVALENT_HOMOTOPIC_TRIVIALITY) THEN
MATCH_MP_TAC(TAUT `~p /\ q ==> (p <=> q) ==> F`) THEN CONJ_TAC THENL
[SUBGOAL_THEN `~(
sphere(a:real^M,r) = {})` MP_TAC THENL
[REWRITE_TAC[
SPHERE_EQ_EMPTY] THEN ASM_REAL_ARITH_TAC;
REWRITE_TAC[GSYM
MEMBER_NOT_EMPTY;
LEFT_IMP_EXISTS_THM]] THEN
X_GEN_TAC `c:real^M` THEN DISCH_TAC THEN
DISCH_THEN(MP_TAC o SPECL[`\a:real^M. a`; `(\a. c):real^M->real^M`]) THEN
SIMP_TAC[
CONTINUOUS_ON_CONST;
CONTINUOUS_ON_ID;
IMAGE_ID;
SUBSET_REFL] THEN
REWRITE_TAC[NOT_IMP] THEN CONJ_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
SUBGOAL_THEN `~(
contractible(
sphere(a:real^M,r)))` MP_TAC THENL
[REWRITE_TAC[
CONTRACTIBLE_SPHERE] THEN ASM_REAL_ARITH_TAC;
REWRITE_TAC[
contractible] THEN MESON_TAC[]];
MAP_EVERY X_GEN_TAC [`f:real^M->real^N`; `g:real^M->real^N`] THEN
STRIP_TAC THEN
MP_TAC(ISPEC `g:real^M->real^N`
INESSENTIAL_SPHEREMAP_LOWDIM) THEN
MP_TAC(ISPEC `f:real^M->real^N`
INESSENTIAL_SPHEREMAP_LOWDIM) THEN
ASM_REWRITE_TAC[IMP_IMP;
AND_FORALL_THM] THEN DISCH_THEN
(MP_TAC o SPECL [`a:real^M`; `r:real`; `b:real^N`; `s:real`]) THEN
ASM_REWRITE_TAC[
LEFT_IMP_EXISTS_THM;
IMP_CONJ;
RIGHT_IMP_FORALL_THM] THEN
REPEAT GEN_TAC THEN REWRITE_TAC[IMP_IMP] THEN DISCH_THEN
(fun
th -> CONJUNCTS_THEN (ASSUME_TAC o MATCH_MP
HOMOTOPIC_WITH_IMP_SUBSET)
th THEN
MP_TAC
th) THEN
MATCH_MP_TAC(MESON[
HOMOTOPIC_WITH_TRANS;
HOMOTOPIC_WITH_SYM]
`
homotopic_with p (s,t) c d
==>
homotopic_with p (s,t) f c /\
homotopic_with p (s,t) g d
==>
homotopic_with p (s,t) f g`) THEN
REWRITE_TAC[
HOMOTOPIC_CONSTANT_MAPS] THEN DISJ2_TAC THEN
MP_TAC(ISPECL [`b:real^N`; `s:real`]
PATH_CONNECTED_SPHERE) THEN
ANTS_TAC THENL
[FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP (ARITH_RULE
`m < n ==> 1 <= m ==> 2 <= n`)) THEN REWRITE_TAC[
DIMINDEX_GE_1];
REWRITE_TAC[
PATH_CONNECTED_IFF_PATH_COMPONENT] THEN
DISCH_THEN MATCH_MP_TAC THEN
SUBGOAL_THEN `~(
sphere(a:real^M,r) = {})` MP_TAC THENL
[REWRITE_TAC[
SPHERE_EQ_EMPTY] THEN ASM_REAL_ARITH_TAC;
ASM SET_TAC[]]]]) in
REWRITE_TAC[
AND_FORALL_THM] THEN REPEAT GEN_TAC THEN
MATCH_MP_TAC(TAUT
`(r ==> p) /\ (q ==> r) /\ (p ==> q) ==> (r <=> q) /\ (p <=> q)`) THEN
REWRITE_TAC[
HOMEOMORPHIC_IMP_HOMOTOPY_EQUIVALENT] THEN
ASM_CASES_TAC `r < &0` THEN
ASM_SIMP_TAC[
SPHERE_EMPTY;
SPHERE_EQ_EMPTY;
HOMEOMORPHIC_EMPTY;
HOMOTOPY_EQUIVALENT_EMPTY]
THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
ASM_CASES_TAC `s < &0` THEN
ASM_SIMP_TAC[
SPHERE_EMPTY;
SPHERE_EQ_EMPTY;
HOMEOMORPHIC_EMPTY;
HOMOTOPY_EQUIVALENT_EMPTY]
THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
ASM_CASES_TAC `r = &0` THEN
ASM_SIMP_TAC[
SPHERE_SING;
REAL_LT_REFL;
HOMEOMORPHIC_SING;
HOMOTOPY_EQUIVALENT_SING;
CONTRACTIBLE_SPHERE;
ONCE_REWRITE_RULE[
HOMOTOPY_EQUIVALENT_SYM]
HOMOTOPY_EQUIVALENT_SING]
THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
ASM_CASES_TAC `s = &0` THEN
ASM_SIMP_TAC[
SPHERE_SING;
REAL_LT_REFL;
HOMEOMORPHIC_SING;
HOMOTOPY_EQUIVALENT_SING;
CONTRACTIBLE_SPHERE;
ONCE_REWRITE_RULE[
HOMOTOPY_EQUIVALENT_SYM]
HOMOTOPY_EQUIVALENT_SING]
THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
SUBGOAL_THEN `&0 < r /\ &0 < s` STRIP_ASSUME_TAC THENL
[ASM_REAL_ARITH_TAC; ASM_REWRITE_TAC[]] THEN
CONJ_TAC THENL
[DISCH_THEN(fun
th ->
let t = `?a:real^M b:real^N. ~(
sphere(a,r)
homeomorphic sphere(b,s))` in
MP_TAC(DISCH t (GEOM_EQUAL_DIMENSION_RULE
th (ASSUME t)))) THEN
ASM_SIMP_TAC[HOMEOMORPHIC_SPHERES] THEN MESON_TAC[];
ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
REWRITE_TAC[ARITH_RULE `~(m:num = n) <=> m < n \/ n < m`] THEN
STRIP_TAC THENL [ALL_TAC; ONCE_REWRITE_TAC[
HOMOTOPY_EQUIVALENT_SYM]] THEN
ASM_SIMP_TAC[
lemma]]);;
(* ------------------------------------------------------------------------- *)
(* Some technical lemmas about extending maps from cell complexes. *)
(* ------------------------------------------------------------------------- *)
let EXTEND_MAP_CELL_COMPLEX_TO_SPHERE,
EXTEND_MAP_CELL_COMPLEX_TO_SPHERE_COFINITE = (CONJ_PAIR o prove)
(`(!f:real^M->real^N m s t.
FINITE m /\ (!c. c IN m ==> polytope c /\ aff_dim c < aff_dim t) /\
(!c1 c2. c1 IN m /\ c2 IN m
==> c1 INTER c2 face_of c1 /\ c1 INTER c2 face_of c2) /\
s SUBSET UNIONS m /\ closed s /\ convex t /\ bounded t /\
f continuous_on s /\ IMAGE f s SUBSET relative_frontier t
==> ?g. g continuous_on UNIONS m /\
IMAGE g (UNIONS m) SUBSET relative_frontier t /\
!x. x IN s ==> g x = f x) /\
(!f:real^M->real^N m s t.
FINITE m /\ (!c. c IN m ==> polytope c /\ aff_dim c <= aff_dim t) /\
(!c1 c2. c1 IN m /\ c2 IN m
==> c1 INTER c2 face_of c1 /\ c1 INTER c2 face_of c2) /\
s SUBSET UNIONS m /\ closed s /\ convex t /\ bounded t /\
f continuous_on s /\ IMAGE f s SUBSET relative_frontier t
==> ?k g. FINITE k /\ DISJOINT k s /\
g continuous_on (UNIONS m DIFF k) /\
IMAGE g (UNIONS m DIFF k) SUBSET relative_frontier t /\
!x. x IN s ==> g x = f x)`,
(* ------------------------------------------------------------------------- *)
(* Special cases and corollaries involving spheres. *)
(* ------------------------------------------------------------------------- *)
let EXTEND_MAP_AFFINE_TO_SPHERE_COFINITE_SIMPLE = prove
(`!f:real^M->real^N s t u.
compact s /\
convex u /\
bounded u /\
aff_dim t <=
aff_dim u /\
s
SUBSET t /\ f
continuous_on s /\
IMAGE f s
SUBSET relative_frontier u
==> ?k g. FINITE k /\ k
SUBSET t /\
DISJOINT k s /\
g
continuous_on (t
DIFF k) /\
IMAGE g (t
DIFF k)
SUBSET relative_frontier u /\
!x. x
IN s ==> g x = f x`,
let lemma = prove
(`!f:A->B->bool P k.
INFINITE {x | P x} /\ FINITE k /\
(!x y. P x /\ P y /\ ~(x = y) ==> DISJOINT (f x) (f y))
==> ?x. P x /\ DISJOINT k (f x)`,
REWRITE_TAC[INFINITE] THEN REPEAT STRIP_TAC THEN
REWRITE_TAC[SET_RULE `(?x. P x /\ DISJOINT k (f x)) <=>
~(!x. ?y. P x ==> y IN k /\ y IN f x)`] THEN
REWRITE_TAC[SKOLEM_THM] THEN
DISCH_THEN(X_CHOOSE_TAC `g:A->B`) THEN
MP_TAC(ISPECL [`g:A->B`; `{x:A | P x}`] FINITE_IMAGE_INJ_EQ) THEN
ASM_REWRITE_TAC[IN_ELIM_THM; NOT_IMP] THEN
CONJ_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP
(REWRITE_RULE[IMP_CONJ] FINITE_SUBSET)) THEN
ASM SET_TAC[]) in
SUBGOAL_THEN
`!f:real^M->real^N s t u.
compact s /\ convex u /\ bounded u /\ aff_dim t <= aff_dim u /\
s SUBSET t /\ f continuous_on s /\ IMAGE f s SUBSET relative_frontier u
==> ?k g. FINITE k /\ DISJOINT k s /\
g continuous_on (t DIFF k) /\
IMAGE g (t DIFF k) SUBSET relative_frontier u /\
!x. x IN s ==> g x = f x`
MP_TAC THENL
[ALL_TAC;
REPEAT(MATCH_MP_TAC MONO_FORALL THEN GEN_TAC) THEN
DISCH_THEN(fun th -> STRIP_TAC THEN MP_TAC th) THEN
ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC[SWAP_EXISTS_THM] THEN
MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `g:real^M->real^N` THEN
DISCH_THEN(X_CHOOSE_THEN `k:real^M->bool` STRIP_ASSUME_TAC) THEN
EXISTS_TAC `k INTER t:real^M->bool` THEN
ASM_SIMP_TAC[FINITE_INTER; INTER_SUBSET] THEN
REPEAT CONJ_TAC THENL [ASM SET_TAC[]; ALL_TAC; ASM SET_TAC[]] THEN
FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REWRITE_RULE[IMP_CONJ]
CONTINUOUS_ON_SUBSET)) THEN ASM SET_TAC[]] THEN
SUBGOAL_THEN
`!f:real^M->real^N s t u.
compact s /\ s SUBSET t /\ affine t /\
convex u /\ bounded u /\ aff_dim t <= aff_dim u /\
f continuous_on s /\ IMAGE f s SUBSET relative_frontier u
==> ?k g. FINITE k /\ DISJOINT k s /\
g continuous_on (t DIFF k) /\
IMAGE g (t DIFF k) SUBSET relative_frontier u /\
!x. x IN s ==> g x = f x`
ASSUME_TAC THENL
[ALL_TAC;
REPEAT STRIP_TAC THEN
SUBGOAL_THEN
`?k g. FINITE k /\ DISJOINT k s /\
g continuous_on (affine hull t DIFF k) /\
IMAGE g (affine hull t DIFF k) SUBSET relative_frontier u /\
!x. x IN s ==> g x = (f:real^M->real^N) x`
MP_TAC THENL
[FIRST_X_ASSUM MATCH_MP_TAC THEN
ASM_SIMP_TAC[AFF_DIM_AFFINE_HULL; AFFINE_AFFINE_HULL] THEN
TRANS_TAC SUBSET_TRANS `t:real^M->bool` THEN
ASM_REWRITE_TAC[HULL_SUBSET];
REPEAT(MATCH_MP_TAC MONO_EXISTS THEN GEN_TAC) THEN
STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
CONJ_TAC THENL
[FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REWRITE_RULE[IMP_CONJ]
CONTINUOUS_ON_SUBSET));
FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REWRITE_RULE[IMP_CONJ_ALT]
SUBSET_TRANS)) THEN
MATCH_MP_TAC IMAGE_SUBSET] THEN
MATCH_MP_TAC(SET_RULE `s SUBSET t ==> s DIFF k SUBSET t DIFF k`) THEN
REWRITE_TAC[HULL_SUBSET]]] THEN
REPEAT STRIP_TAC THEN ASM_CASES_TAC `s:real^M->bool = {}` THENL
[ASM_CASES_TAC `relative_frontier(u:real^N->bool) = {}` THENL
[RULE_ASSUM_TAC(REWRITE_RULE[RELATIVE_FRONTIER_EQ_EMPTY]) THEN
UNDISCH_TAC `bounded(u:real^N->bool)` THEN
ASM_SIMP_TAC[AFFINE_BOUNDED_EQ_LOWDIM] THEN DISCH_TAC THEN
SUBGOAL_THEN `aff_dim(t:real^M->bool) <= &0` MP_TAC THENL
[ASM_INT_ARITH_TAC; ALL_TAC] THEN
SIMP_TAC[AFF_DIM_GE; INT_ARITH
`--(&1):int <= x ==> (x <= &0 <=> x = --(&1) \/ x = &0)`] THEN
REWRITE_TAC[AFF_DIM_EQ_MINUS1; AFF_DIM_EQ_0] THEN
DISCH_THEN(DISJ_CASES_THEN2 ASSUME_TAC (X_CHOOSE_TAC `a:real^M`)) THEN
EXISTS_TAC `{a:real^M}` THEN
ASM_REWRITE_TAC[DISJOINT_EMPTY; FINITE_SING; NOT_IN_EMPTY;
EMPTY_DIFF; DIFF_EQ_EMPTY; IMAGE_CLAUSES;
CONTINUOUS_ON_EMPTY; EMPTY_SUBSET];
EXISTS_TAC `{}:real^M->bool` THEN
FIRST_X_ASSUM(X_CHOOSE_TAC `y:real^N` o
GEN_REWRITE_RULE I [GSYM MEMBER_NOT_EMPTY]) THEN
ASM_SIMP_TAC[FINITE_EMPTY; DISJOINT_EMPTY; NOT_IN_EMPTY; DIFF_EMPTY] THEN
EXISTS_TAC `(\x. y):real^M->real^N` THEN
REWRITE_TAC[CONTINUOUS_ON_CONST] THEN ASM SET_TAC[]];
ALL_TAC] THEN
FIRST_ASSUM(MP_TAC o MATCH_MP COMPACT_IMP_BOUNDED) THEN
DISCH_THEN(MP_TAC o MATCH_MP BOUNDED_SUBSET_CLOSED_INTERVAL_SYMMETRIC) THEN
REWRITE_TAC[INSERT_SUBSET] THEN
DISCH_THEN(X_CHOOSE_THEN `b:real^M` STRIP_ASSUME_TAC) THEN
MP_TAC(ISPECL
[`f:real^M->real^N`;
`{interval[--(b + vec 1):real^M,b + vec 1] INTER t}`;
`s:real^M->bool`; `u:real^N->bool`]
EXTEND_MAP_CELL_COMPLEX_TO_SPHERE_COFINITE) THEN
SUBGOAL_THEN
`interval[--b,b] SUBSET interval[--(b + vec 1):real^M,b + vec 1]`
ASSUME_TAC THENL
[REWRITE_TAC[SUBSET_INTERVAL; VECTOR_ADD_COMPONENT; VECTOR_NEG_COMPONENT;
VEC_COMPONENT] THEN
REAL_ARITH_TAC;
ALL_TAC] THEN
ASM_REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM; FINITE_SING] THEN
REWRITE_TAC[FORALL_IN_INSERT; NOT_IN_EMPTY; IMP_IMP] THEN
REWRITE_TAC[INTER_IDEMPOT; UNIONS_1; FACE_OF_REFL_EQ; SUBSET_INTER] THEN
ANTS_TAC THENL
[ASM_SIMP_TAC[HULL_SUBSET; COMPACT_IMP_CLOSED] THEN REPEAT CONJ_TAC THENL
[MATCH_MP_TAC POLYTOPE_INTER_POLYHEDRON THEN
ASM_SIMP_TAC[POLYTOPE_INTERVAL; AFFINE_IMP_POLYHEDRON];
TRANS_TAC INT_LE_TRANS `aff_dim(t:real^M->bool)` THEN
ASM_SIMP_TAC[AFF_DIM_SUBSET; INTER_SUBSET];
ASM_SIMP_TAC[CONVEX_INTER; CONVEX_INTERVAL; AFFINE_IMP_CONVEX];
ASM SET_TAC[]];
REWRITE_TAC[LEFT_IMP_EXISTS_THM]] THEN
MAP_EVERY X_GEN_TAC [`k:real^M->bool`; `g:real^M->real^N`] THEN
STRIP_TAC THEN EXISTS_TAC `k:real^M->bool` THEN ASM_REWRITE_TAC[] THEN
SUBGOAL_THEN
`?d:real. (&1 / &2 <= d /\ d <= &1) /\
DISJOINT k (frontier(interval[--(b + lambda i. d):real^M,
(b + lambda i. d)]))`
STRIP_ASSUME_TAC THENL
[MATCH_MP_TAC lemma THEN
ASM_SIMP_TAC[INFINITE; FINITE_REAL_INTERVAL; REAL_NOT_LE] THEN
CONV_TAC REAL_RAT_REDUCE_CONV THEN
MATCH_MP_TAC REAL_WLOG_LT THEN REWRITE_TAC[] THEN
CONJ_TAC THENL [SET_TAC[]; ALL_TAC] THEN
MAP_EVERY X_GEN_TAC [`x:real`; `y:real`] THEN REPEAT STRIP_TAC THEN
REWRITE_TAC[frontier] THEN MATCH_MP_TAC(SET_RULE
`c SUBSET i' ==> DISJOINT (c DIFF i) (c' DIFF i')`) THEN
REWRITE_TAC[INTERIOR_INTERVAL; CLOSURE_INTERVAL] THEN
SIMP_TAC[SUBSET_INTERVAL; VECTOR_NEG_COMPONENT; VECTOR_ADD_COMPONENT;
LAMBDA_BETA] THEN
ASM_REAL_ARITH_TAC;
ALL_TAC] THEN
ABBREV_TAC `c:real^M = b + lambda i. d` THEN SUBGOAL_THEN
`interval[--b:real^M,b] SUBSET interval(--c,c) /\
interval[--b:real^M,b] SUBSET interval[--c,c] /\
interval[--c,c] SUBSET interval[--(b + vec 1):real^M,b + vec 1]`
STRIP_ASSUME_TAC THENL
[REWRITE_TAC[SUBSET_INTERVAL] THEN EXPAND_TAC "c" THEN REPEAT CONJ_TAC THEN
SIMP_TAC[VECTOR_NEG_COMPONENT; VECTOR_ADD_COMPONENT; LAMBDA_BETA] THEN
MATCH_MP_TAC MONO_FORALL THEN GEN_TAC THEN MATCH_MP_TAC MONO_IMP THEN
REWRITE_TAC[VEC_COMPONENT] THEN ASM_REAL_ARITH_TAC;
ALL_TAC] THEN
EXISTS_TAC
`(g:real^M->real^N) o
closest_point (interval[--c,c] INTER t)` THEN
REPEAT CONJ_TAC THENL
[MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN CONJ_TAC THENL
[MATCH_MP_TAC CONTINUOUS_ON_CLOSEST_POINT THEN
ASM_SIMP_TAC[CONVEX_INTER; CLOSED_INTER; CLOSED_INTERVAL; CLOSED_AFFINE;
AFFINE_IMP_CONVEX; AFFINE_AFFINE_HULL; CONVEX_INTERVAL] THEN
ASM SET_TAC[];
FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REWRITE_RULE[IMP_CONJ]
CONTINUOUS_ON_SUBSET))];
REWRITE_TAC[IMAGE_o] THEN
FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP (REWRITE_RULE[IMP_CONJ_ALT]
SUBSET_TRANS)) THEN
MATCH_MP_TAC IMAGE_SUBSET;
X_GEN_TAC `x:real^M` THEN DISCH_TAC THEN REWRITE_TAC[o_THM] THEN
TRANS_TAC EQ_TRANS `(g:real^M->real^N) x` THEN
CONJ_TAC THENL [AP_TERM_TAC; ASM SET_TAC[]] THEN
MATCH_MP_TAC CLOSEST_POINT_SELF THEN
ASM_SIMP_TAC[IN_INTER; HULL_INC] THEN ASM SET_TAC[]] THEN
(REWRITE_TAC[SUBSET; FORALL_IN_IMAGE; IN_DIFF] THEN
X_GEN_TAC `x:real^M` THEN STRIP_TAC THEN CONJ_TAC THENL
[MATCH_MP_TAC(SET_RULE
`closest_point s x IN s /\ s SUBSET u ==> closest_point s x IN u`) THEN
CONJ_TAC THENL [MATCH_MP_TAC CLOSEST_POINT_IN_SET; ASM SET_TAC[]] THEN
ASM_SIMP_TAC[CLOSED_INTER; CLOSED_INTERVAL; CLOSED_AFFINE] THEN
ASM SET_TAC[];
ALL_TAC] THEN
ASM_CASES_TAC `x IN interval[--c:real^M,c]` THEN
ASM_SIMP_TAC[CLOSEST_POINT_SELF; IN_INTER] THEN
MATCH_MP_TAC(SET_RULE
`closest_point s x IN relative_frontier s /\
DISJOINT k (relative_frontier s)
==> ~(closest_point s x IN k)`) THEN
CONJ_TAC THENL
[MATCH_MP_TAC CLOSEST_POINT_IN_RELATIVE_FRONTIER THEN
ASM_SIMP_TAC[CLOSED_INTER; CLOSED_AFFINE; CLOSED_INTERVAL] THEN
CONJ_TAC THENL [ASM SET_TAC[]; REWRITE_TAC[IN_DIFF]] THEN CONJ_TAC THENL
[ALL_TAC; ASM_MESON_TAC[SUBSET; RELATIVE_INTERIOR_SUBSET; IN_INTER]] THEN
ONCE_REWRITE_TAC[INTER_COMM] THEN
W(MP_TAC o PART_MATCH (lhs o rand)
AFFINE_HULL_CONVEX_INTER_NONEMPTY_INTERIOR o rand o snd) THEN
ASM_SIMP_TAC[HULL_HULL; AFFINE_AFFINE_HULL; AFFINE_IMP_CONVEX] THEN
ASM_SIMP_TAC[HULL_P] THEN ANTS_TAC THENL [ALL_TAC; ASM SET_TAC[]] THEN
REWRITE_TAC[INTERIOR_INTERVAL] THEN ASM SET_TAC[];
W(MP_TAC o PART_MATCH (lhs o rand) RELATIVE_FRONTIER_CONVEX_INTER_AFFINE o
rand o snd) THEN
ANTS_TAC THENL [ALL_TAC; ASM SET_TAC[]] THEN
REWRITE_TAC[CONVEX_INTERVAL; AFFINE_AFFINE_HULL; INTERIOR_INTERVAL] THEN
ASM SET_TAC[]]));;
let EXTEND_MAP_AFFINE_TO_SPHERE_COFINITE_GEN = prove
(`!f:real^M->real^N s t u p.
compact s /\
convex u /\
bounded u /\
affine t /\
aff_dim t <=
aff_dim u /\ s
SUBSET t /\
f
continuous_on s /\
IMAGE f s
SUBSET relative_frontier u /\
(!c. c
IN components(t
DIFF s) /\
bounded c ==> ~(c
INTER p = {}))
==> ?k g. FINITE k /\ k
SUBSET p /\ k
SUBSET t /\
DISJOINT k s /\
g
continuous_on (t
DIFF k) /\
IMAGE g (t
DIFF k)
SUBSET relative_frontier u /\
!x. x
IN s ==> g x = f x`,
let lemma0 = prove
(`!u t s v. closed_in (subtopology euclidean u) v /\ t SUBSET u /\
s = v INTER t
==> closed_in (subtopology euclidean t) s`,
REPEAT GEN_TAC THEN REWRITE_TAC[CLOSED_IN_CLOSED; LEFT_AND_EXISTS_THM] THEN
MATCH_MP_TAC MONO_EXISTS THEN SET_TAC[]) in
let lemma1 = prove
(`!f:A->B->bool P k.
INFINITE {x | P x} /\ FINITE k /\
(!x y. P x /\ P y /\ ~(x = y) ==> DISJOINT (f x) (f y))
==> ?x. P x /\ DISJOINT k (f x)`,
REWRITE_TAC[INFINITE] THEN REPEAT STRIP_TAC THEN
REWRITE_TAC[SET_RULE `(?x. P x /\ DISJOINT k (f x)) <=>
~(!x. ?y. P x ==> y IN k /\ y IN f x)`] THEN
REWRITE_TAC[SKOLEM_THM] THEN
DISCH_THEN(X_CHOOSE_TAC `g:A->B`) THEN
MP_TAC(ISPECL [`g:A->B`; `{x:A | P x}`] FINITE_IMAGE_INJ_EQ) THEN
ASM_REWRITE_TAC[IN_ELIM_THM; NOT_IMP] THEN
CONJ_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP
(REWRITE_RULE[IMP_CONJ] FINITE_SUBSET)) THEN
ASM SET_TAC[]) in
let lemma2 = prove
(`!f:real^M->real^N s t k p u.
FINITE k /\ affine u /\
f continuous_on ((u:real^M->bool) DIFF k) /\
IMAGE f ((u:real^M->bool) DIFF k) SUBSET t /\
(!c. c IN components((u:real^M->bool) DIFF s) /\ ~(c INTER k = {})
==> ~(c INTER p = {})) /\
closed_in (subtopology euclidean u) s /\ DISJOINT k s /\ k SUBSET u
==> ?g. g continuous_on ((u:real^M->bool) DIFF p) /\
IMAGE g ((u:real^M->bool) DIFF p) SUBSET t /\
!x. x IN s ==> g x = f x`,
REPEAT GEN_TAC THEN ASM_CASES_TAC `k:real^M->bool = {}` THENL
[ASM_REWRITE_TAC[DIFF_EMPTY] THEN REPEAT STRIP_TAC THEN
EXISTS_TAC `f:real^M->real^N` THEN REWRITE_TAC[] THEN CONJ_TAC THENL
[ASM_MESON_TAC[CONTINUOUS_ON_SUBSET; SUBSET_DIFF]; ASM SET_TAC[]];
STRIP_TAC] THEN
FIRST_ASSUM(ASSUME_TAC o MATCH_MP CLOSED_IN_IMP_SUBSET) THEN
SUBGOAL_THEN `~(((u:real^M->bool) DIFF s) INTER k = {})` MP_TAC THENL
[ASM SET_TAC[]; ALL_TAC] THEN
GEN_REWRITE_TAC (LAND_CONV o RAND_CONV o LAND_CONV o LAND_CONV)
[UNIONS_COMPONENTS] THEN
REWRITE_TAC[INTER_UNIONS; EMPTY_UNIONS; FORALL_IN_GSPEC] THEN
REWRITE_TAC[NOT_FORALL_THM; NOT_IMP; LEFT_IMP_EXISTS_THM] THEN
X_GEN_TAC `co:real^M->bool` THEN STRIP_TAC THEN
SUBGOAL_THEN `locally connected (u:real^M->bool)` ASSUME_TAC THENL
[ASM_SIMP_TAC[AFFINE_IMP_CONVEX; CONVEX_IMP_LOCALLY_CONNECTED];
ALL_TAC] THEN
SUBGOAL_THEN
`!c. c IN components ((u:real^M->bool) DIFF s) /\ ~(c INTER k = {})
==> ?a g. a IN c /\ a IN p /\
g continuous_on (s UNION (c DELETE a)) /\
IMAGE g (s UNION (c DELETE a)) SUBSET t /\
!x. x IN s ==> g x = (f:real^M->real^N) x`
MP_TAC THENL
[X_GEN_TAC `c:real^M->bool` THEN STRIP_TAC THEN
FIRST_ASSUM(ASSUME_TAC o MATCH_MP IN_COMPONENTS_SUBSET) THEN
FIRST_X_ASSUM(MP_TAC o SPEC `c:real^M->bool`) THEN
ASM_REWRITE_TAC[] THEN REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; IN_INTER] THEN
MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `a:real^M` THEN
STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
SUBGOAL_THEN `open_in (subtopology euclidean u) (c:real^M->bool)`
MP_TAC THENL
[MATCH_MP_TAC OPEN_IN_TRANS THEN
EXISTS_TAC `u DIFF s:real^M->bool` THEN
ASM_SIMP_TAC[OPEN_IN_DIFF; OPEN_IN_REFL] THEN
MATCH_MP_TAC OPEN_IN_COMPONENTS_LOCALLY_CONNECTED THEN
ASM_REWRITE_TAC[] THEN MATCH_MP_TAC LOCALLY_OPEN_SUBSET THEN
EXISTS_TAC `u:real^M->bool` THEN
ASM_SIMP_TAC[OPEN_IN_DIFF; OPEN_IN_REFL];
DISCH_THEN(fun th -> ASSUME_TAC th THEN MP_TAC th)] THEN
REWRITE_TAC[OPEN_IN_CONTAINS_CBALL] THEN
DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC (MP_TAC o SPEC `a:real^M`)) THEN
ASM_REWRITE_TAC[] THEN
DISCH_THEN(X_CHOOSE_THEN `d:real` STRIP_ASSUME_TAC) THEN
SUBGOAL_THEN `ball(a:real^M,d) INTER u SUBSET c` ASSUME_TAC THENL
[ASM_MESON_TAC[BALL_SUBSET_CBALL; SUBSET_TRANS;
SET_RULE `b SUBSET c ==> b INTER u SUBSET c INTER u`];
ALL_TAC] THEN
MP_TAC(ISPECL
[`ball(a:real^M,d) INTER u`; `c:real^M->bool`;
`s UNION c:real^M->bool`; `c INTER k:real^M->bool`]
HOMEOMORPHISM_GROUPING_POINTS_EXISTS_GEN) THEN
ASM_REWRITE_TAC[INTER_SUBSET; SUBSET_UNION; UNION_SUBSET] THEN
ANTS_TAC THENL
[REPEAT CONJ_TAC THENL
[MATCH_MP_TAC OPEN_IN_SUBSET_TRANS THEN
EXISTS_TAC `u:real^M->bool` THEN
ASM_SIMP_TAC[HULL_MINIMAL; HULL_SUBSET];
MP_TAC(ISPECL [`c:real^M->bool`; `u:real^M->bool`]
AFFINE_HULL_OPEN_IN) THEN
ASM_SIMP_TAC[HULL_P] THEN ASM SET_TAC[];
REWRITE_TAC[HULL_SUBSET];
ASM_MESON_TAC[IN_COMPONENTS_CONNECTED];
ASM_MESON_TAC[FINITE_SUBSET; INTER_SUBSET];
MATCH_MP_TAC OPEN_IN_SUBSET_TRANS THEN
EXISTS_TAC `u:real^M->bool` THEN
ASM_REWRITE_TAC[] THEN
ASM_MESON_TAC[OPEN_IN_OPEN_INTER; OPEN_BALL; INTER_COMM];
REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; IN_INTER] THEN
EXISTS_TAC `a:real^M` THEN REWRITE_TAC[CENTRE_IN_BALL] THEN
ASM SET_TAC[]];
REWRITE_TAC[IN_INTER; LEFT_IMP_EXISTS_THM]] THEN
MAP_EVERY X_GEN_TAC [`h:real^M->real^M`; `k:real^M->real^M`] THEN
REWRITE_TAC[homeomorphism] THEN STRIP_TAC THEN
MP_TAC(ISPECL [`cball(a:real^M,d) INTER u`; `a:real^M`]
RELATIVE_FRONTIER_RETRACT_OF_PUNCTURED_AFFINE_HULL) THEN
MP_TAC(ISPECL [`cball(a:real^M,d)`; `u:real^M->bool`]
RELATIVE_INTERIOR_CONVEX_INTER_AFFINE) THEN
MP_TAC(ISPECL [`cball(a:real^M,d)`; `u:real^M->bool`]
RELATIVE_FRONTIER_CONVEX_INTER_AFFINE) THEN
MP_TAC(ISPECL [`u:real^M->bool`; `cball(a:real^M,d)`]
(ONCE_REWRITE_RULE[INTER_COMM]
AFFINE_HULL_AFFINE_INTER_NONEMPTY_INTERIOR)) THEN
ASM_SIMP_TAC[CONVEX_CBALL; FRONTIER_CBALL; INTERIOR_CBALL] THEN
SUBGOAL_THEN `a IN ball(a:real^M,d) INTER u` ASSUME_TAC THENL
[ASM_REWRITE_TAC[CENTRE_IN_BALL; IN_INTER] THEN ASM SET_TAC[];
ALL_TAC] THEN
REPLICATE_TAC 3
(ANTS_TAC THENL [ASM SET_TAC[]; DISCH_THEN SUBST1_TAC]) THEN
ASM_SIMP_TAC[CONVEX_INTER; CONVEX_CBALL; AFFINE_IMP_CONVEX] THEN
ANTS_TAC THENL
[ASM_MESON_TAC[BOUNDED_SUBSET; INTER_SUBSET; BOUNDED_CBALL];
ALL_TAC] THEN
ASM_REWRITE_TAC[retract_of; retraction] THEN
DISCH_THEN(X_CHOOSE_THEN `r:real^M->real^M` STRIP_ASSUME_TAC) THEN
EXISTS_TAC
`(f:real^M->real^N) o (k:real^M->real^M) o
(\x. if x IN ball(a,d) then r x else x)` THEN
REWRITE_TAC[CONJ_ASSOC] THEN CONJ_TAC THENL
[ALL_TAC;
X_GEN_TAC `x:real^M` THEN DISCH_TAC THEN REWRITE_TAC[o_THM] THEN
COND_CASES_TAC THENL
[ASM SET_TAC[]; AP_TERM_TAC THEN ASM SET_TAC[]]] THEN
ABBREV_TAC `j = \x:real^M. if x IN ball(a,d) then r x else x` THEN
SUBGOAL_THEN
`(j:real^M->real^M) continuous_on ((u:real^M->bool) DELETE a)`
ASSUME_TAC THENL
[EXPAND_TAC "j" THEN
SUBGOAL_THEN
`u DELETE (a:real^M) =
(cball(a,d) DELETE a) INTER u UNION
((u:real^M->bool) DIFF ball(a,d))`
(fun th -> SUBST1_TAC th THEN
MATCH_MP_TAC CONTINUOUS_ON_CASES_LOCAL THEN
SUBST1_TAC(SYM th))
THENL
[MP_TAC(ISPECL [`a:real^M`; `d:real`] BALL_SUBSET_CBALL) THEN
ASM SET_TAC[];
ALL_TAC] THEN
REWRITE_TAC[IN_DIFF; IN_INTER; IN_DELETE; CONTINUOUS_ON_ID] THEN
REPEAT CONJ_TAC THENL
[ALL_TAC; ALL_TAC;
FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REWRITE_RULE[IMP_CONJ]
CONTINUOUS_ON_SUBSET)) THEN ASM SET_TAC[];
REWRITE_TAC[GSYM BALL_UNION_SPHERE] THEN ASM SET_TAC[]] THEN
REWRITE_TAC[CLOSED_IN_CLOSED] THENL
[EXISTS_TAC `cball(a:real^M,d)` THEN REWRITE_TAC[CLOSED_CBALL];
EXISTS_TAC `(:real^M) DIFF ball(a,d)` THEN
REWRITE_TAC[GSYM OPEN_CLOSED; OPEN_BALL]] THEN
MP_TAC(ISPECL [`a:real^M`; `d:real`] BALL_SUBSET_CBALL) THEN
MP_TAC(ISPECL [`a:real^M`; `d:real`] CENTRE_IN_BALL) THEN
ASM SET_TAC[];
ALL_TAC] THEN
SUBGOAL_THEN
`IMAGE (j:real^M->real^M) (s UNION c DELETE a) SUBSET
(s UNION c DIFF ball(a,d))`
ASSUME_TAC THENL
[EXPAND_TAC "j" THEN REWRITE_TAC[SUBSET; FORALL_IN_IMAGE] THEN
X_GEN_TAC `x:real^M` THEN DISCH_TAC THEN
COND_CASES_TAC THENL [ALL_TAC; ASM SET_TAC[]] THEN
SUBGOAL_THEN `(r:real^M->real^M) x IN sphere(a,d)` MP_TAC THENL
[MP_TAC(ISPECL [`a:real^M`; `d:real`] CENTRE_IN_BALL) THEN
ASM SET_TAC[];
REWRITE_TAC[GSYM CBALL_DIFF_BALL] THEN ASM SET_TAC[]];
ALL_TAC] THEN
CONJ_TAC THENL
[REPEAT(MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN CONJ_TAC) THEN
FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REWRITE_RULE[IMP_CONJ]
CONTINUOUS_ON_SUBSET))
THENL [ASM SET_TAC[]; ASM SET_TAC[]; ALL_TAC];
ONCE_REWRITE_TAC[IMAGE_o] THEN FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP
(SET_RULE `IMAGE f u SUBSET t
==> s SUBSET u ==> IMAGE f s SUBSET t`))] THEN
REWRITE_TAC[IMAGE_o] THEN
FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (SET_RULE
`s SUBSET u ==> IMAGE f u SUBSET t ==> IMAGE f s SUBSET t`)) THEN
REWRITE_TAC[SUBSET; IN_UNIV; IN_DIFF; FORALL_IN_IMAGE] THEN
ASM SET_TAC[];
ALL_TAC] THEN
GEN_REWRITE_TAC (LAND_CONV o TOP_DEPTH_CONV) [RIGHT_IMP_EXISTS_THM] THEN
REWRITE_TAC[SKOLEM_THM; LEFT_IMP_EXISTS_THM] THEN
MAP_EVERY X_GEN_TAC
[`a:(real^M->bool)->real^M`; `h:(real^M->bool)->real^M->real^N`] THEN
DISCH_TAC THEN MP_TAC(ISPECL
[`h:(real^M->bool)->real^M->real^N`;
`\c:real^M->bool. s UNION (c DELETE (a c))`;
`s UNION UNIONS
{ c DELETE (a c) |
c IN components ((u:real^M->bool) DIFF s) /\ ~(c INTER k = {})}`;
`{c | c IN components ((u:real^M->bool) DIFF s) /\ ~(c INTER k = {})}`]
PASTING_LEMMA_EXISTS_CLOSED) THEN
SUBGOAL_THEN
`FINITE {c | c IN components((u:real^M->bool) DIFF s) /\
~(c INTER k = {})}`
ASSUME_TAC THENL
[MP_TAC(ISPECL
[`\c:real^M->bool. c INTER k`;
`{c | c IN components ((u:real^M->bool) DIFF s) /\ ~(c INTER k = {})}`]
FINITE_IMAGE_INJ_EQ) THEN
REWRITE_TAC[IN_ELIM_THM] THEN ANTS_TAC THENL
[MESON_TAC[COMPONENTS_EQ;
SET_RULE
`s INTER k = t INTER k /\ ~(s INTER k = {})
==> ~(s INTER t = {})`];
DISCH_THEN(SUBST1_TAC o SYM) THEN
REWRITE_TAC[GSYM SIMPLE_IMAGE; IN_ELIM_THM]] THEN
MP_TAC(ISPEC
`{c INTER k |c| c IN components((u:real^M->bool) DIFF s) /\
~(c INTER k = {})}`
FINITE_UNIONS) THEN
MATCH_MP_TAC(TAUT `p ==> (p <=> q /\ r) ==> q`) THEN
FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REWRITE_RULE[IMP_CONJ]
FINITE_SUBSET)) THEN
REWRITE_TAC[UNIONS_GSPEC] THEN ASM SET_TAC[];
ALL_TAC] THEN
ASM_REWRITE_TAC[IN_ELIM_THM] THEN ANTS_TAC THENL
[REPEAT CONJ_TAC THENL
[REWRITE_TAC[UNIONS_GSPEC] THEN ASM SET_TAC[];
X_GEN_TAC `c:real^M->bool` THEN DISCH_TAC THEN ASM_SIMP_TAC[] THEN
MATCH_MP_TAC lemma0 THEN
MAP_EVERY EXISTS_TAC [`u:real^M->bool`; `s UNION c:real^M->bool`] THEN
REPEAT CONJ_TAC THENL
[MATCH_MP_TAC CLOSED_IN_UNION_COMPLEMENT_COMPONENT THEN
ASM_REWRITE_TAC[];
ASM_REWRITE_TAC[UNION_SUBSET; UNIONS_SUBSET; FORALL_IN_GSPEC] THEN
MESON_TAC[IN_COMPONENTS_SUBSET;
SET_RULE `c SUBSET u DIFF s ==> c DELETE a SUBSET u`];
ASM_SIMP_TAC[CLOSED_UNION_COMPLEMENT_COMPONENT; UNIONS_GSPEC] THEN
MATCH_MP_TAC(SET_RULE
`~(a IN t) /\ c DELETE a SUBSET t
==> s UNION c DELETE a = (s UNION c) INTER (s UNION t)`) THEN
CONJ_TAC THENL [ALL_TAC; ASM SET_TAC[]] THEN
REWRITE_TAC[IN_ELIM_THM; IN_DELETE] THEN
DISCH_THEN(X_CHOOSE_THEN `c':real^M->bool` STRIP_ASSUME_TAC) THEN
MP_TAC(ISPECL [`(u:real^M->bool) DIFF s`;
`c:real^M->bool`; `c':real^M->bool`]
COMPONENTS_EQ) THEN
ASM_CASES_TAC `c':real^M->bool = c` THENL
[ASM_MESON_TAC[]; ALL_TAC] THEN
ASM SET_TAC[]];
MAP_EVERY X_GEN_TAC
[`c1:real^M->bool`; `c2:real^M->bool`; `x:real^M`] THEN
STRIP_TAC THEN ASM_CASES_TAC `c2:real^M->bool = c1` THEN
ASM_REWRITE_TAC[] THEN FIRST_ASSUM(MP_TAC o MATCH_MP (SET_RULE
`x IN u INTER (s UNION c1 DELETE a) INTER (s UNION c2 DELETE b)
==> (c1 INTER c2 = {}) ==> x IN s`)) THEN
ANTS_TAC THENL [ASM_MESON_TAC[COMPONENTS_EQ]; ASM_SIMP_TAC[]]];
DISCH_THEN(X_CHOOSE_THEN `g:real^M->real^N` STRIP_ASSUME_TAC)] THEN
MP_TAC
(ISPECL [`\x. x IN s UNION
UNIONS {c | c IN components((u:real^M->bool) DIFF s) /\
c INTER k = {}}`;
`f:real^M->real^N`;
`g:real^M->real^N`;
`s UNION
UNIONS {c | c IN components((u:real^M->bool) DIFF s) /\
c INTER k = {}}`;
`s UNION
UNIONS { c DELETE (a c) |
c IN components((u:real^M->bool) DIFF s) /\
~(c INTER k = {})}`]
CONTINUOUS_ON_CASES_LOCAL) THEN
ASM_REWRITE_TAC[] THEN ANTS_TAC THENL
[REPEAT CONJ_TAC THENL
[MATCH_MP_TAC lemma0 THEN EXISTS_TAC `u:real^M->bool` THEN
EXISTS_TAC `u DIFF
UNIONS {c DELETE a c |
c IN components ((u:real^M->bool) DIFF s) /\
~(c INTER k = {})}` THEN
REPEAT CONJ_TAC THENL
[MATCH_MP_TAC CLOSED_IN_DIFF THEN REWRITE_TAC[CLOSED_IN_REFL] THEN
MATCH_MP_TAC OPEN_IN_UNIONS THEN REWRITE_TAC[FORALL_IN_GSPEC] THEN
X_GEN_TAC `c:real^M->bool` THEN DISCH_TAC THEN
MATCH_MP_TAC OPEN_IN_DELETE THEN MATCH_MP_TAC OPEN_IN_TRANS THEN
EXISTS_TAC `u DIFF s:real^M->bool` THEN
ASM_SIMP_TAC[OPEN_IN_DIFF; OPEN_IN_REFL] THEN
MATCH_MP_TAC OPEN_IN_COMPONENTS_LOCALLY_CONNECTED THEN
ASM_REWRITE_TAC[] THEN MATCH_MP_TAC LOCALLY_OPEN_SUBSET THEN
EXISTS_TAC `u:real^M->bool` THEN
ASM_SIMP_TAC[OPEN_IN_DIFF; OPEN_IN_REFL];
ASM_REWRITE_TAC[UNION_SUBSET] THEN
REWRITE_TAC[UNIONS_SUBSET; IN_ELIM_THM] THEN
MESON_TAC[IN_COMPONENTS_SUBSET;
SET_RULE `c SUBSET u DIFF s ==> c DELETE a SUBSET u /\
c SUBSET u`];
REWRITE_TAC[SET_RULE
`(s UNION t) UNION (s UNION u) = (s UNION t) UNION u`] THEN
MATCH_MP_TAC(SET_RULE
`s SUBSET u /\ t INTER s = {}
==> s = (u DIFF t) INTER (s UNION t)`) THEN
CONJ_TAC THENL
[ASM_REWRITE_TAC[UNION_SUBSET] THEN
REWRITE_TAC[UNIONS_SUBSET; IN_ELIM_THM] THEN
MESON_TAC[IN_COMPONENTS_SUBSET;
SET_RULE `c SUBSET u DIFF s ==> c DELETE a SUBSET u /\
c SUBSET u`];
ALL_TAC] THEN
REWRITE_TAC[EMPTY_UNION; SET_RULE
`c INTER (s UNION t) = (s INTER c) UNION (c INTER t)`] THEN
CONJ_TAC THENL
[MATCH_MP_TAC(SET_RULE
`t SUBSET UNIV DIFF s ==> s INTER t = {}`) THEN
REWRITE_TAC[UNIONS_SUBSET; FORALL_IN_GSPEC] THEN GEN_TAC THEN
DISCH_THEN(CONJUNCTS_THEN2
(MP_TAC o MATCH_MP IN_COMPONENTS_SUBSET)
MP_TAC) THEN ASM SET_TAC[];
REWRITE_TAC[INTER_UNIONS; EMPTY_UNIONS; FORALL_IN_GSPEC] THEN
X_GEN_TAC `c:real^M->bool` THEN STRIP_TAC THEN
X_GEN_TAC `c':real^M->bool` THEN STRIP_TAC THEN
MP_TAC(ISPECL [`(u:real^M->bool) DIFF s`;
`c:real^M->bool`; `c':real^M->bool`]
COMPONENTS_EQ) THEN
ASM_CASES_TAC `c':real^M->bool = c` THENL
[ASM_MESON_TAC[]; ASM SET_TAC[]]]];
MATCH_MP_TAC lemma0 THEN EXISTS_TAC `u:real^M->bool` THEN
EXISTS_TAC
`UNIONS {s UNION c |c| c IN components ((u:real^M->bool) DIFF s) /\
~(c INTER k = {})}` THEN
REPEAT CONJ_TAC THENL
[MATCH_MP_TAC CLOSED_IN_UNIONS THEN REWRITE_TAC[FORALL_IN_GSPEC] THEN
ONCE_REWRITE_TAC[SIMPLE_IMAGE_GEN] THEN
ASM_SIMP_TAC[FINITE_IMAGE] THEN REPEAT STRIP_TAC THEN
MATCH_MP_TAC CLOSED_IN_UNION_COMPLEMENT_COMPONENT THEN
ASM_REWRITE_TAC[];
ASM_REWRITE_TAC[UNION_SUBSET] THEN
REWRITE_TAC[UNIONS_SUBSET; IN_ELIM_THM] THEN
MESON_TAC[IN_COMPONENTS_SUBSET;
SET_RULE `c SUBSET u DIFF s ==> c DELETE a SUBSET u /\
c SUBSET u`];
MATCH_MP_TAC(SET_RULE
`t SUBSET u /\ u INTER s SUBSET t ==> t = u INTER (s UNION t)`) THEN
CONJ_TAC THENL
[REWRITE_TAC[UNIONS_GSPEC] THEN ASM SET_TAC[]; ALL_TAC] THEN
MATCH_MP_TAC(SET_RULE
`u INTER t SUBSET s ==> u INTER (s UNION t) SUBSET s UNION v`) THEN
MATCH_MP_TAC(SET_RULE
`((UNIV DIFF s) INTER t) INTER u SUBSET s
==> t INTER u SUBSET s`) THEN
GEN_REWRITE_TAC (LAND_CONV o LAND_CONV o TOP_DEPTH_CONV)
[INTER_UNIONS] THEN
REWRITE_TAC[SET_RULE
`{g x | x IN {f y | P y}} = {g(f y) | P y}`] THEN
REWRITE_TAC[SET_RULE
`(UNIV DIFF s) INTER (s UNION c) = c DIFF s`] THEN
REWRITE_TAC[SET_RULE
`t INTER u SUBSET s <=> t INTER ((UNIV DIFF s) INTER u) = {}`] THEN
ONCE_REWRITE_TAC[INTER_UNIONS] THEN
REWRITE_TAC[EMPTY_UNIONS; FORALL_IN_GSPEC; INTER_UNIONS] THEN
X_GEN_TAC `c:real^M->bool` THEN STRIP_TAC THEN
X_GEN_TAC `c':real^M->bool` THEN STRIP_TAC THEN
MP_TAC(ISPECL [`(u:real^M->bool) DIFF s`;
`c:real^M->bool`; `c':real^M->bool`]
COMPONENTS_EQ) THEN
ASM_CASES_TAC `c':real^M->bool = c` THENL
[ASM_MESON_TAC[]; ASM SET_TAC[]]];
FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REWRITE_RULE[IMP_CONJ]
CONTINUOUS_ON_SUBSET)) THEN
REWRITE_TAC[UNION_SUBSET] THEN
CONJ_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
REWRITE_TAC[UNIONS_SUBSET; IN_ELIM_THM] THEN
GEN_TAC THEN
DISCH_THEN(CONJUNCTS_THEN2 (MP_TAC o MATCH_MP IN_COMPONENTS_SUBSET)
MP_TAC) THEN ASM SET_TAC[];
REWRITE_TAC[TAUT `p /\ ~p <=> F`] THEN X_GEN_TAC `x:real^M` THEN
REWRITE_TAC[IN_UNION] THEN
ASM_CASES_TAC `(x:real^M) IN s` THEN ASM_REWRITE_TAC[] THENL
[ASM SET_TAC[]; ALL_TAC] THEN
REWRITE_TAC[UNIONS_GSPEC; IN_ELIM_THM; IN_DELETE] THEN
DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_TAC `c:real^M->bool`)
(X_CHOOSE_TAC `c':real^M->bool`)) THEN
MP_TAC(ISPECL [`(u:real^M->bool) DIFF s`;
`c:real^M->bool`; `c':real^M->bool`]
COMPONENTS_EQ) THEN
ASM_CASES_TAC `c':real^M->bool = c` THENL
[ASM_MESON_TAC[]; ASM SET_TAC[]]];
MATCH_MP_TAC(MESON[CONTINUOUS_ON_SUBSET]
`t SUBSET s /\ P f
==> f continuous_on s ==> ?g. g continuous_on t /\ P g`) THEN
REWRITE_TAC[] THEN CONJ_TAC THENL
[REWRITE_TAC[SET_RULE
`(s UNION t) UNION (s UNION u) = s UNION (t UNION u)`] THEN
MATCH_MP_TAC(SET_RULE
`(u DIFF s) DIFF p SUBSET t
==> u DIFF p SUBSET s UNION t`) THEN
GEN_REWRITE_TAC (LAND_CONV o LAND_CONV) [UNIONS_COMPONENTS] THEN
REWRITE_TAC[UNIONS_GSPEC] THEN ASM SET_TAC[];
SIMP_TAC[IN_UNION]] THEN
REWRITE_TAC[SUBSET; FORALL_IN_IMAGE; IN_DIFF; IN_UNION; IN_UNIV] THEN
X_GEN_TAC `x:real^M` THEN DISCH_TAC THEN
ASM_CASES_TAC `(x:real^M) IN s` THENL [ASM SET_TAC[]; ALL_TAC] THEN
ASM_REWRITE_TAC[IN_UNIONS; IN_ELIM_THM] THEN COND_CASES_TAC THENL
[ASM SET_TAC[]; ALL_TAC] THEN
SUBGOAL_THEN
`x IN ((u:real^M->bool) DIFF s)` MP_TAC THENL
[ASM SET_TAC[]; ALL_TAC] THEN
GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [UNIONS_COMPONENTS] THEN
REWRITE_TAC[IN_UNIONS] THEN
DISCH_THEN(X_CHOOSE_THEN `c:real^M->bool` STRIP_ASSUME_TAC) THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [NOT_EXISTS_THM]) THEN
DISCH_THEN(MP_TAC o SPEC `c:real^M->bool`) THEN ASM_REWRITE_TAC[] THEN
DISCH_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPECL [`x:real^M`; `c:real^M->bool`]) THEN
ASM_REWRITE_TAC[UNIONS_GSPEC] THEN ASM SET_TAC[]]) in
let lemma3 = prove
(`!f:real^M->real^N s t u p.
compact s /\ convex u /\ bounded u /\
affine t /\ aff_dim t <= aff_dim u /\ s SUBSET t /\
f continuous_on s /\ IMAGE f s SUBSET relative_frontier u /\
(!c. c IN components(t DIFF s) ==> ~(c INTER p = {}))
==> ?k g. FINITE k /\ k SUBSET p /\ k SUBSET t /\ DISJOINT k s /\
g continuous_on (t DIFF k) /\
IMAGE g (t DIFF k) SUBSET relative_frontier u /\
!x. x IN s ==> g x = f x`,
REPEAT STRIP_TAC THEN
MP_TAC(ISPECL [`f:real^M->real^N`; `s:real^M->bool`;
`t:real^M->bool`; `u:real^N->bool`]
EXTEND_MAP_AFFINE_TO_SPHERE_COFINITE_SIMPLE) THEN
ASM_REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
MAP_EVERY X_GEN_TAC [`k:real^M->bool`; `g:real^M->real^N`] THEN
STRIP_TAC THEN
SUBGOAL_THEN
`!x. ?y. x IN k
==> ?c. c IN components (t DIFF s:real^M->bool) /\
x IN c /\ y IN c /\ y IN p`
MP_TAC THENL
[X_GEN_TAC `x:real^M` THEN REWRITE_TAC[RIGHT_EXISTS_IMP_THM] THEN
DISCH_TAC THEN
SUBGOAL_THEN `(x:real^M) IN (t DIFF s)` MP_TAC THENL
[ASM SET_TAC[]; ALL_TAC] THEN
GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [UNIONS_COMPONENTS] THEN
ONCE_REWRITE_TAC[SWAP_EXISTS_THM] THEN
REWRITE_TAC[IN_UNIONS; RIGHT_EXISTS_AND_THM] THEN
MATCH_MP_TAC MONO_EXISTS THEN ASM SET_TAC[];
REWRITE_TAC[SKOLEM_THM] THEN
DISCH_THEN(X_CHOOSE_THEN `h:real^M->real^M` (LABEL_TAC "*"))] THEN
EXISTS_TAC `IMAGE (h:real^M->real^M) k` THEN
MP_TAC(ISPECL
[`g:real^M->real^N`; `s:real^M->bool`;
`relative_frontier u:real^N->bool`; `k:real^M->bool`;
`IMAGE (h:real^M->real^M) k`; `t:real^M->bool`] lemma2) THEN
ASM_SIMP_TAC[AFFINE_AFFINE_HULL; FINITE_IMAGE] THEN ANTS_TAC THENL
[CONJ_TAC THENL
[X_GEN_TAC `c:real^M->bool` THEN STRIP_TAC THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM MEMBER_NOT_EMPTY]) THEN
ONCE_REWRITE_TAC[INTER_COMM] THEN
REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; EXISTS_IN_IMAGE; IN_INTER] THEN
MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `x:real^M` THEN
STRIP_TAC THEN REMOVE_THEN "*" (MP_TAC o SPEC `x:real^M`) THEN
ASM_REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
X_GEN_TAC `c':real^M->bool` THEN STRIP_TAC THEN
MP_TAC(ISPECL [`(t:real^M->bool) DIFF s`;
`c:real^M->bool`; `c':real^M->bool`]
COMPONENTS_EQ) THEN
ASM_CASES_TAC `c':real^M->bool = c` THENL [ALL_TAC; ASM SET_TAC[]] THEN
ASM_REWRITE_TAC[] THEN ASM SET_TAC[];
MATCH_MP_TAC CLOSED_IN_SUBSET_TRANS THEN
EXISTS_TAC `(:real^M)` THEN
ASM_REWRITE_TAC[SUBTOPOLOGY_UNIV; GSYM CLOSED_IN] THEN
ASM_SIMP_TAC[COMPACT_IMP_CLOSED; SUBSET_UNIV]];
MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `h:real^M->real^N` THEN
STRIP_TAC THEN ASM_SIMP_TAC[] THEN
REWRITE_TAC[SET_RULE `DISJOINT s t <=> !x. x IN s ==> ~(x IN t)`] THEN
ASM_REWRITE_TAC[SUBSET; FORALL_IN_IMAGE] THEN
ASM_MESON_TAC[IN_COMPONENTS_SUBSET; SUBSET; IN_DIFF]]) in
REPEAT STRIP_TAC THEN ASM_CASES_TAC `s:real^M->bool = {}` THENL
[ASM_CASES_TAC `relative_frontier(u:real^N->bool) = {}` THENL
[RULE_ASSUM_TAC(REWRITE_RULE[RELATIVE_FRONTIER_EQ_EMPTY]) THEN
UNDISCH_TAC `bounded(u:real^N->bool)` THEN
ASM_SIMP_TAC[AFFINE_BOUNDED_EQ_LOWDIM] THEN DISCH_TAC THEN
SUBGOAL_THEN `aff_dim(t:real^M->bool) <= &0` MP_TAC THENL
[ASM_INT_ARITH_TAC; ALL_TAC] THEN
SIMP_TAC[AFF_DIM_GE; INT_ARITH
`--(&1):int <= x ==> (x <= &0 <=> x = --(&1) \/ x = &0)`] THEN
REWRITE_TAC[AFF_DIM_EQ_MINUS1; AFF_DIM_EQ_0] THEN
DISCH_THEN(DISJ_CASES_THEN2 ASSUME_TAC (X_CHOOSE_TAC `a:real^M`)) THENL
[EXISTS_TAC `{}:real^M->bool` THEN
ASM_REWRITE_TAC[EMPTY_DIFF; FINITE_EMPTY; CONTINUOUS_ON_EMPTY;
IMAGE_CLAUSES; NOT_IN_EMPTY] THEN
SET_TAC[];
FIRST_X_ASSUM(MP_TAC o SPEC `{a:real^M}`) THEN
ASM_REWRITE_TAC[DIFF_EMPTY; IN_COMPONENTS_SELF] THEN
REWRITE_TAC[CONNECTED_SING; NOT_INSERT_EMPTY; BOUNDED_SING] THEN
DISCH_TAC THEN EXISTS_TAC `{a:real^M}` THEN
ASM_REWRITE_TAC[DIFF_EQ_EMPTY; CONTINUOUS_ON_EMPTY; NOT_IN_EMPTY;
FINITE_SING; IMAGE_CLAUSES; EMPTY_SUBSET] THEN
ASM SET_TAC[]];
EXISTS_TAC `{}:real^M->bool` THEN
FIRST_X_ASSUM(X_CHOOSE_TAC `y:real^N` o
GEN_REWRITE_RULE I [GSYM MEMBER_NOT_EMPTY]) THEN
ASM_SIMP_TAC[FINITE_EMPTY; DISJOINT_EMPTY; NOT_IN_EMPTY; DIFF_EMPTY] THEN
EXISTS_TAC `(\x. y):real^M->real^N` THEN
REWRITE_TAC[CONTINUOUS_ON_CONST] THEN ASM SET_TAC[]];
ALL_TAC] THEN
FIRST_ASSUM(MP_TAC o MATCH_MP COMPACT_IMP_BOUNDED) THEN
DISCH_THEN(MP_TAC o MATCH_MP BOUNDED_SUBSET_CLOSED_INTERVAL_SYMMETRIC) THEN
REWRITE_TAC[INSERT_SUBSET] THEN
DISCH_THEN(X_CHOOSE_THEN `b:real^M` STRIP_ASSUME_TAC) THEN
MP_TAC(ISPECL
[`f:real^M->real^N`; `s:real^M->bool`;
`t:real^M->bool`; `u:real^N->bool`;
`p UNION (UNIONS {c | c IN components (t DIFF s) /\ ~bounded c} DIFF
interval[--(b + vec 1):real^M,b + vec 1])`]
lemma3) THEN
ASM_REWRITE_TAC[] THEN ANTS_TAC THENL
[X_GEN_TAC `c:real^M->bool` THEN STRIP_TAC THEN
ASM_CASES_TAC `bounded(c:real^M->bool)` THENL
[FIRST_X_ASSUM(MP_TAC o SPEC `c:real^M->bool`) THEN
ASM_REWRITE_TAC[] THEN ASM SET_TAC[];
ALL_TAC] THEN
SUBGOAL_THEN
`~(c SUBSET interval[--(b + vec 1):real^M,b + vec 1])`
MP_TAC THENL [ALL_TAC; ASM SET_TAC[]] THEN
ASM_MESON_TAC[BOUNDED_SUBSET; BOUNDED_INTERVAL];
ALL_TAC] THEN
REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
MAP_EVERY X_GEN_TAC [`k:real^M->bool`; `g:real^M->real^N`] THEN
STRIP_TAC THEN
EXISTS_TAC `k INTER interval[--(b + vec 1):real^M,b + vec 1]` THEN
ASM_SIMP_TAC[FINITE_INTER; RIGHT_EXISTS_AND_THM] THEN
REPEAT(CONJ_TAC THENL [ASM SET_TAC[]; ALL_TAC]) THEN
SUBGOAL_THEN
`interval[--b,b] SUBSET interval[--(b + vec 1):real^M,b + vec 1]`
ASSUME_TAC THENL
[REWRITE_TAC[SUBSET_INTERVAL; VECTOR_ADD_COMPONENT; VECTOR_NEG_COMPONENT;
VEC_COMPONENT] THEN
REAL_ARITH_TAC;
ALL_TAC] THEN
SUBGOAL_THEN
`?d:real. (&1 / &2 <= d /\ d <= &1) /\
DISJOINT k (frontier(interval[--(b + lambda i. d):real^M,
(b + lambda i. d)]))`
STRIP_ASSUME_TAC THENL
[MATCH_MP_TAC lemma1 THEN
ASM_SIMP_TAC[INFINITE; FINITE_REAL_INTERVAL; REAL_NOT_LE] THEN
CONV_TAC REAL_RAT_REDUCE_CONV THEN
MATCH_MP_TAC REAL_WLOG_LT THEN REWRITE_TAC[] THEN
CONJ_TAC THENL [SET_TAC[]; ALL_TAC] THEN
MAP_EVERY X_GEN_TAC [`x:real`; `y:real`] THEN REPEAT STRIP_TAC THEN
REWRITE_TAC[frontier] THEN MATCH_MP_TAC(SET_RULE
`c SUBSET i' ==> DISJOINT (c DIFF i) (c' DIFF i')`) THEN
REWRITE_TAC[INTERIOR_INTERVAL; CLOSURE_INTERVAL] THEN
SIMP_TAC[SUBSET_INTERVAL; VECTOR_NEG_COMPONENT; VECTOR_ADD_COMPONENT;
LAMBDA_BETA] THEN
ASM_REAL_ARITH_TAC;
ALL_TAC] THEN
ABBREV_TAC `c:real^M = b + lambda i. d` THEN SUBGOAL_THEN
`interval[--b:real^M,b] SUBSET interval(--c,c) /\
interval[--b:real^M,b] SUBSET interval[--c,c] /\
interval[--c,c] SUBSET interval[--(b + vec 1):real^M,b + vec 1]`
STRIP_ASSUME_TAC THENL
[REWRITE_TAC[SUBSET_INTERVAL] THEN EXPAND_TAC "c" THEN REPEAT CONJ_TAC THEN
SIMP_TAC[VECTOR_NEG_COMPONENT; VECTOR_ADD_COMPONENT; LAMBDA_BETA] THEN
MATCH_MP_TAC MONO_FORALL THEN GEN_TAC THEN MATCH_MP_TAC MONO_IMP THEN
REWRITE_TAC[VEC_COMPONENT] THEN ASM_REAL_ARITH_TAC;
ALL_TAC] THEN
EXISTS_TAC
`(g:real^M->real^N) o
closest_point (interval[--c,c] INTER t)` THEN
REPEAT CONJ_TAC THENL
[MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN CONJ_TAC THENL
[MATCH_MP_TAC CONTINUOUS_ON_CLOSEST_POINT THEN
ASM_SIMP_TAC[CONVEX_INTER; CLOSED_INTER; CLOSED_INTERVAL; CLOSED_AFFINE;
AFFINE_IMP_CONVEX; AFFINE_AFFINE_HULL; CONVEX_INTERVAL] THEN
ASM SET_TAC[];
FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REWRITE_RULE[IMP_CONJ]
CONTINUOUS_ON_SUBSET))];
REWRITE_TAC[IMAGE_o] THEN
FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP (REWRITE_RULE[IMP_CONJ_ALT]
SUBSET_TRANS)) THEN
MATCH_MP_TAC IMAGE_SUBSET;
X_GEN_TAC `x:real^M` THEN DISCH_TAC THEN REWRITE_TAC[o_THM] THEN
TRANS_TAC EQ_TRANS `(g:real^M->real^N) x` THEN
CONJ_TAC THENL [AP_TERM_TAC; ASM SET_TAC[]] THEN
MATCH_MP_TAC CLOSEST_POINT_SELF THEN
ASM_SIMP_TAC[IN_INTER; HULL_INC] THEN ASM SET_TAC[]] THEN
(REWRITE_TAC[SUBSET; FORALL_IN_IMAGE; IN_DIFF] THEN
X_GEN_TAC `x:real^M` THEN STRIP_TAC THEN CONJ_TAC THENL
[MATCH_MP_TAC(SET_RULE
`closest_point s x IN s /\ s SUBSET u ==> closest_point s x IN u`) THEN
CONJ_TAC THENL [MATCH_MP_TAC CLOSEST_POINT_IN_SET; ASM SET_TAC[]] THEN
ASM_SIMP_TAC[CLOSED_INTER; CLOSED_INTERVAL; CLOSED_AFFINE] THEN
ASM SET_TAC[];
ALL_TAC] THEN
ASM_CASES_TAC `x IN interval[--c:real^M,c]` THEN
ASM_SIMP_TAC[CLOSEST_POINT_SELF; IN_INTER] THENL
[ASM SET_TAC[]; ALL_TAC] THEN
MATCH_MP_TAC(SET_RULE
`closest_point s x IN relative_frontier s /\
DISJOINT k (relative_frontier s)
==> ~(closest_point s x IN k)`) THEN
CONJ_TAC THENL
[MATCH_MP_TAC CLOSEST_POINT_IN_RELATIVE_FRONTIER THEN
ASM_SIMP_TAC[CLOSED_INTER; CLOSED_AFFINE; CLOSED_INTERVAL] THEN
CONJ_TAC THENL [ASM SET_TAC[]; REWRITE_TAC[IN_DIFF]] THEN CONJ_TAC THENL
[ALL_TAC; ASM_MESON_TAC[SUBSET; RELATIVE_INTERIOR_SUBSET; IN_INTER]] THEN
ONCE_REWRITE_TAC[INTER_COMM] THEN
W(MP_TAC o PART_MATCH (lhs o rand)
AFFINE_HULL_CONVEX_INTER_NONEMPTY_INTERIOR o rand o snd) THEN
ASM_SIMP_TAC[HULL_HULL; AFFINE_AFFINE_HULL; AFFINE_IMP_CONVEX] THEN
ASM_SIMP_TAC[HULL_P] THEN ANTS_TAC THENL [ALL_TAC; ASM SET_TAC[]] THEN
REWRITE_TAC[INTERIOR_INTERVAL] THEN ASM SET_TAC[];
W(MP_TAC o PART_MATCH (lhs o rand) RELATIVE_FRONTIER_CONVEX_INTER_AFFINE o
rand o snd) THEN
ANTS_TAC THENL [ALL_TAC; ASM SET_TAC[]] THEN
REWRITE_TAC[CONVEX_INTERVAL; AFFINE_AFFINE_HULL; INTERIOR_INTERVAL] THEN
ASM SET_TAC[]]));;
(* ------------------------------------------------------------------------- *)
(* Borsuk-style characterization of separation. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Invariance of domain and corollaries. *)
(* ------------------------------------------------------------------------- *)
let INVARIANCE_OF_DOMAIN = prove
(`!f:real^N->real^N s.
f
continuous_on s /\ open s /\
(!x y. x
IN s /\ y
IN s /\ f x = f y ==> x = y)
==> open(
IMAGE f s)`,
let lemma = prove
(`!f:real^N->real^N a r.
f continuous_on cball(a,r) /\ &0 < r /\
(!x y. x IN cball(a,r) /\ y IN cball(a,r) /\ f x = f y ==> x = y)
==> open(IMAGE f (ball(a,r)))`,
REPEAT STRIP_TAC THEN ASM_CASES_TAC `dimindex(:N) = 1` THENL
[MP_TAC(ISPECL [`(:real^N)`; `(:real^1)`] ISOMETRIES_SUBSPACES) THEN
ASM_SIMP_TAC[SUBSPACE_UNIV; DIM_UNIV; DIMINDEX_1;
LEFT_IMP_EXISTS_THM] THEN
MAP_EVERY X_GEN_TAC [`h:real^N->real^1`; `k:real^1->real^N`] THEN
REWRITE_TAC[IN_UNIV] THEN STRIP_TAC THEN
MP_TAC(ISPECL [`(h:real^N->real^1) o f o (k:real^1->real^N)`;
`IMAGE (h:real^N->real^1) (cball(a,r))`]
INJECTIVE_EQ_1D_OPEN_MAP_UNIV) THEN
MATCH_MP_TAC(TAUT
`p /\ q /\ r /\ (s ==> t)
==> (p /\ q ==> (r <=> s)) ==> t`) THEN
REPEAT CONJ_TAC THENL
[REPEAT(MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN CONJ_TAC) THEN
ASM_SIMP_TAC[LINEAR_CONTINUOUS_ON; GSYM IMAGE_o] THEN
ASM_REWRITE_TAC[o_DEF; IMAGE_ID];
REWRITE_TAC[IS_INTERVAL_CONNECTED_1] THEN
MATCH_MP_TAC CONNECTED_CONTINUOUS_IMAGE THEN
ASM_SIMP_TAC[LINEAR_CONTINUOUS_ON; CONNECTED_CBALL];
ASM_SIMP_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM;
FORALL_IN_IMAGE; o_DEF] THEN
ASM SET_TAC[];
DISCH_THEN(MP_TAC o SPEC `IMAGE (h:real^N->real^1) (ball(a,r))`) THEN
ASM_SIMP_TAC[IMAGE_SUBSET; BALL_SUBSET_CBALL; GSYM IMAGE_o] THEN
ANTS_TAC THENL
[MP_TAC(ISPECL [`a:real^N`; `r:real`] OPEN_BALL); ALL_TAC] THEN
MATCH_MP_TAC EQ_IMP THENL
[CONV_TAC SYM_CONV;
REWRITE_TAC[GSYM o_ASSOC] THEN ONCE_REWRITE_TAC[IMAGE_o] THEN
ASM_REWRITE_TAC[o_DEF; ETA_AX]] THEN
MATCH_MP_TAC OPEN_BIJECTIVE_LINEAR_IMAGE_EQ THEN
ASM_MESON_TAC[]];
FIRST_ASSUM(MP_TAC o MATCH_MP (ARITH_RULE
`~(n = 1) ==> 1 <= n ==> 2 <= n`)) THEN
REWRITE_TAC[DIMINDEX_GE_1] THEN DISCH_TAC] THEN
REPEAT STRIP_TAC THEN
MP_TAC(ISPECL [`IMAGE (f:real^N->real^N) (sphere(a,r))`;
`a:real^N`; `r:real`]
JORDAN_BROUWER_SEPARATION) THEN
ASM_REWRITE_TAC[] THEN ANTS_TAC THENL
[ONCE_REWRITE_TAC[HOMEOMORPHIC_SYM] THEN
MATCH_MP_TAC HOMEOMORPHIC_COMPACT THEN EXISTS_TAC `f:real^N->real^N` THEN
ASM_MESON_TAC[CONTINUOUS_ON_SUBSET; SUBSET; SPHERE_SUBSET_CBALL;
COMPACT_SPHERE];
DISCH_TAC] THEN
MP_TAC(ISPEC `(:real^N) DIFF IMAGE f (sphere(a:real^N,r))`
COBOUNDED_HAS_BOUNDED_COMPONENT) THEN
ASM_REWRITE_TAC[SET_RULE `UNIV DIFF (UNIV DIFF s) = s`] THEN
ANTS_TAC THENL
[ASM_MESON_TAC[CONTINUOUS_ON_SUBSET; SUBSET; SPHERE_SUBSET_CBALL;
COMPACT_SPHERE; COMPACT_CONTINUOUS_IMAGE; COMPACT_IMP_BOUNDED];
DISCH_THEN(X_CHOOSE_THEN `c:real^N->bool` STRIP_ASSUME_TAC)] THEN
SUBGOAL_THEN
`IMAGE (f:real^N->real^N) (ball(a,r)) = c`
SUBST1_TAC THENL
[ALL_TAC;
FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP (REWRITE_RULE[IMP_CONJ_ALT]
OPEN_COMPONENTS)) THEN
REWRITE_TAC[GSYM closed] THEN
ASM_MESON_TAC[CONTINUOUS_ON_SUBSET; SUBSET; SPHERE_SUBSET_CBALL;
COMPACT_SPHERE; COMPACT_CONTINUOUS_IMAGE; COMPACT_IMP_CLOSED]] THEN
MATCH_MP_TAC(SET_RULE
`~(c = {}) /\ (~(c INTER t = {}) ==> t SUBSET c) /\ c SUBSET t
==> t = c`) THEN
REPEAT STRIP_TAC THENL
[ASM_MESON_TAC[IN_COMPONENTS_NONEMPTY];
FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP (ONCE_REWRITE_RULE[IMP_CONJ]
COMPONENTS_MAXIMAL)) THEN
ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
[MATCH_MP_TAC CONNECTED_CONTINUOUS_IMAGE THEN
REWRITE_TAC[CONNECTED_BALL] THEN
ASM_MESON_TAC[CONTINUOUS_ON_SUBSET; BALL_SUBSET_CBALL];
REWRITE_TAC[GSYM CBALL_DIFF_SPHERE] THEN
MP_TAC(ISPECL [`a:real^N`; `r:real`] SPHERE_SUBSET_CBALL) THEN
ASM SET_TAC[]];
FIRST_ASSUM(MP_TAC o MATCH_MP IN_COMPONENTS_SUBSET) THEN
FIRST_ASSUM(MP_TAC o SPEC `(:real^N) DIFF IMAGE f (cball(a:real^N,r))` o
MATCH_MP (ONCE_REWRITE_RULE[IMP_CONJ] COMPONENTS_MAXIMAL)) THEN
SIMP_TAC[SET_RULE `UNIV DIFF t SUBSET UNIV DIFF s <=> s SUBSET t`;
IMAGE_SUBSET; SPHERE_SUBSET_CBALL] THEN
MATCH_MP_TAC(TAUT `p /\ ~r /\ (~q ==> s) ==> (p /\ q ==> r) ==> s`) THEN
REWRITE_TAC[] THEN REPEAT CONJ_TAC THENL
[MATCH_MP_TAC(INST_TYPE [`:N`,`:M`]
CONNECTED_COMPLEMENT_HOMEOMORPHIC_CONVEX_COMPACT) THEN
EXISTS_TAC `cball(a:real^N,r)` THEN
ASM_REWRITE_TAC[CONVEX_CBALL; COMPACT_CBALL] THEN
ONCE_REWRITE_TAC[HOMEOMORPHIC_SYM] THEN
MATCH_MP_TAC HOMEOMORPHIC_COMPACT THEN
EXISTS_TAC `f:real^N->real^N` THEN ASM_REWRITE_TAC[COMPACT_CBALL];
DISCH_THEN(MP_TAC o
MATCH_MP(REWRITE_RULE[IMP_CONJ_ALT] BOUNDED_SUBSET)) THEN
ASM_REWRITE_TAC[] THEN MATCH_MP_TAC COBOUNDED_IMP_UNBOUNDED THEN
REWRITE_TAC[SET_RULE `UNIV DIFF (UNIV DIFF s) = s`] THEN
ASM_MESON_TAC[COMPACT_IMP_BOUNDED; COMPACT_CONTINUOUS_IMAGE;
COMPACT_CBALL];
REWRITE_TAC[GSYM CBALL_DIFF_SPHERE] THEN ASM SET_TAC[]]]) in
REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[OPEN_SUBOPEN] THEN
REWRITE_TAC[FORALL_IN_IMAGE] THEN X_GEN_TAC `a:real^N` THEN DISCH_TAC THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [OPEN_CONTAINS_CBALL]) THEN
DISCH_THEN(MP_TAC o SPEC `a:real^N`) THEN
ASM_REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
X_GEN_TAC `r:real` THEN STRIP_TAC THEN
EXISTS_TAC `IMAGE (f:real^N->real^N) (ball(a,r))` THEN
REPEAT CONJ_TAC THENL
[MATCH_MP_TAC lemma THEN ASM_MESON_TAC[SUBSET; CONTINUOUS_ON_SUBSET];
ASM_SIMP_TAC[FUN_IN_IMAGE; CENTRE_IN_BALL];
MATCH_MP_TAC IMAGE_SUBSET THEN
ASM_MESON_TAC[BALL_SUBSET_CBALL; SUBSET_TRANS]]);;
let HOMEOMORPHIC_INTERVALS_EQ = prove
(`(!a b:real^M c d:real^N.
interval[a,b]
homeomorphic interval[c,d] <=>
aff_dim(
interval[a,b]) =
aff_dim(
interval[c,d])) /\
(!a b:real^M c d:real^N.
interval[a,b]
homeomorphic interval(c,d) <=>
interval[a,b] = {} /\
interval(c,d) = {}) /\
(!a b:real^M c d:real^N.
interval(a,b)
homeomorphic interval[c,d] <=>
interval(a,b) = {} /\
interval[c,d] = {}) /\
(!a b:real^M c d:real^N.
interval(a,b)
homeomorphic interval(c,d) <=>
interval(a,b) = {} /\
interval(c,d) = {} \/
~(
interval(a,b) = {}) /\ ~(
interval(c,d) = {}) /\
dimindex(:M) =
dimindex(:N))`,
(* ------------------------------------------------------------------------- *)
(* Dimension-based conditions for various homeomorphisms. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* The power, squaring and exponential functions as covering maps. *)
(* ------------------------------------------------------------------------- *)
let COVERING_SPACE_POW_PUNCTURED_PLANE = prove
(`!n. 0 < n
==>
covering_space ((:complex)
DIFF {Cx(&0)},(\z. z pow n))
((:complex)
DIFF {Cx (&0)})`,
let lemma = prove
(`!n. 0 < n
==> ?e. &0 < e /\
!w z. norm(w - z) < e * norm(z)
==> (w pow n = z pow n <=> w = z)`,
REPEAT STRIP_TAC THEN
FIRST_ASSUM(DISJ_CASES_TAC o MATCH_MP (ARITH_RULE
`0 < n ==> n = 1 \/ 2 <= n`)) THEN
ASM_SIMP_TAC[COMPLEX_POW_1] THENL [MESON_TAC[REAL_LT_01]; ALL_TAC] THEN
EXISTS_TAC `&2 * sin(pi / &n)` THEN CONJ_TAC THENL
[REWRITE_TAC[REAL_ARITH `&0 < &2 * x <=> &0 < x`] THEN
MATCH_MP_TAC SIN_POS_PI THEN
ASM_SIMP_TAC[REAL_LT_DIV; PI_POS; REAL_OF_NUM_LT] THEN
REWRITE_TAC[REAL_ARITH `x / y < x <=> &0 < x * (&1 - inv y)`] THEN
MATCH_MP_TAC REAL_LT_MUL THEN REWRITE_TAC[PI_POS; REAL_SUB_LT] THEN
MATCH_MP_TAC REAL_INV_LT_1 THEN REWRITE_TAC[REAL_OF_NUM_LT] THEN
ASM_ARITH_TAC;
ALL_TAC] THEN
REPEAT GEN_TAC THEN ASM_CASES_TAC `z = Cx(&0)` THENL
[ASM_REWRITE_TAC[COMPLEX_NORM_0; COMPLEX_SUB_RZERO] THEN
CONV_TAC REAL_RAT_REDUCE_CONV THEN REWRITE_TAC[] THEN
SIMP_TAC[NORM_ARITH `norm(w) < x * &0 <=> F`];
ALL_TAC] THEN
ASM_SIMP_TAC[GSYM REAL_LT_LDIV_EQ; COMPLEX_NORM_NZ] THEN
ASM_SIMP_TAC[COMPLEX_POW_EQ_0; COMPLEX_FIELD
`~(z = Cx(&0)) ==> (w = z <=> w / z = Cx(&1))`] THEN
REWRITE_TAC[GSYM COMPLEX_NORM_DIV; GSYM COMPLEX_POW_DIV] THEN
ASM_SIMP_TAC[COMPLEX_FIELD
`~(z = Cx(&0)) ==> (w - z) / z = w / z - Cx(&1)`] THEN
ASM_CASES_TAC `w / z = Cx(&0)` THENL
[ASM_REWRITE_TAC[COMPLEX_SUB_LZERO; NORM_NEG; COMPLEX_NORM_CX] THEN
ASM_SIMP_TAC[COMPLEX_POW_ZERO; LE_1];
UNDISCH_TAC `~(w / z = Cx(&0))` THEN
UNDISCH_THEN `~(z = Cx(&0))` (K ALL_TAC) THEN
REPEAT(POP_ASSUM MP_TAC) THEN
SPEC_TAC(`w / z:complex`,`z:complex`) THEN REPEAT STRIP_TAC] THEN
EQ_TAC THEN SIMP_TAC[COMPLEX_POW_ONE] THEN DISCH_TAC THEN
UNDISCH_TAC `norm(z - Cx(&1)) < &2 * sin (pi / &n)` THEN
ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN REWRITE_TAC[REAL_NOT_LT] THEN
DISCH_TAC THEN MP_TAC(SPEC `n:num` COMPLEX_ROOTS_UNITY) THEN
ASM_SIMP_TAC[LE_1; EXTENSION; IN_ELIM_THM] THEN
DISCH_THEN(MP_TAC o SPEC `z:complex`) THEN ASM_REWRITE_TAC[] THEN
DISCH_THEN(X_CHOOSE_THEN `j:num` MP_TAC) THEN
REWRITE_TAC[COMPLEX_RING `t * p * ii * q = ii * (t * p * q)`] THEN
REWRITE_TAC[GSYM CX_MUL] THEN ASM_CASES_TAC `j = 0` THENL
[ASM_REWRITE_TAC[real_div; REAL_MUL_LZERO; REAL_MUL_RZERO; CEXP_0;
COMPLEX_MUL_RZERO];
STRIP_TAC THEN ASM_REWRITE_TAC[DIST_CEXP_II_1]] THEN
MATCH_MP_TAC(REAL_ARITH `x <= y ==> &2 * x <= &2 * abs y`) THEN
REWRITE_TAC[REAL_ARITH `(&2 * x) / &2 = x`] THEN
ASM_CASES_TAC `&j / &n <= &1 / &2` THENL
[ALL_TAC;
SUBGOAL_THEN `sin(pi * &j / &n) = sin(pi * &(n - j) / &n)`
SUBST1_TAC THENL
[ASM_SIMP_TAC[GSYM REAL_OF_NUM_SUB; LT_IMP_LE; REAL_OF_NUM_LT;
REAL_FIELD `&0 < n ==> pi * (n - j) / n = pi - pi * j / n`] THEN
REWRITE_TAC[SIN_SUB; COS_PI; SIN_PI] THEN REAL_ARITH_TAC;
ALL_TAC]] THEN
MATCH_MP_TAC SIN_MONO_LE THEN
REWRITE_TAC[REAL_ARITH `--(pi / &2) = pi * --(&1 / &2)`; real_div] THEN
SIMP_TAC[REAL_LE_LMUL_EQ; PI_POS] THEN
ASM_SIMP_TAC[GSYM real_div; REAL_LE_RDIV_EQ; REAL_MUL_LINV; REAL_LT_IMP_NZ;
REAL_LE_LDIV_EQ; REAL_OF_NUM_LT; REAL_OF_NUM_LT; LE_1;
ARITH_RULE `j < n ==> 1 <= n - j`; REAL_OF_NUM_LE;
REAL_ARITH `&0 <= x ==> --(&1 / &2) <= x`;
REAL_POS; REAL_LE_INV_EQ] THEN
ASM_SIMP_TAC[GSYM REAL_OF_NUM_SUB; LT_IMP_LE] THEN
REWRITE_TAC[REAL_ARITH `n - j <= inv(&2) * n <=> inv(&2) * n <= j`] THEN
ASM_SIMP_TAC[GSYM REAL_LE_LDIV_EQ; GSYM REAL_LE_RDIV_EQ;
REAL_OF_NUM_LT] THEN
ASM_REAL_ARITH_TAC) in
REPEAT STRIP_TAC THEN
SIMP_TAC[covering_space; CONTINUOUS_ON_COMPLEX_POW; CONTINUOUS_ON_ID] THEN
SIMP_TAC[OPEN_IN_OPEN_EQ; OPEN_DIFF; OPEN_UNIV; CLOSED_SING] THEN
MATCH_MP_TAC(TAUT `p /\ (p ==> q) ==> p /\ q`) THEN CONJ_TAC THENL
[REWRITE_TAC[EXTENSION; IN_IMAGE; IN_DIFF; IN_UNIV; IN_SING] THEN
ASM_MESON_TAC[COMPLEX_POW_EQ_0; EXISTS_COMPLEX_ROOT; LE_1];
DISCH_THEN(fun th -> GEN_REWRITE_TAC
(BINDER_CONV o LAND_CONV o RAND_CONV) [GSYM th])] THEN
REWRITE_TAC[FORALL_IN_IMAGE; IN_UNIV; IN_DIFF; IN_SING] THEN
SIMP_TAC[SUBSET_UNIV; SET_RULE `s SUBSET UNIV DIFF {a} <=> ~(a IN s)`] THEN
X_GEN_TAC `z:complex` THEN DISCH_TAC THEN
MP_TAC(SPEC `n:num` lemma) THEN ASM_REWRITE_TAC[] THEN
DISCH_THEN(X_CHOOSE_THEN `e:real` STRIP_ASSUME_TAC) THEN
ABBREV_TAC `d = (min (&1 / &2) (e / &4)) * norm(z:complex)` THEN
SUBGOAL_THEN `&0 < d` ASSUME_TAC THENL
[EXPAND_TAC "d" THEN MATCH_MP_TAC REAL_LT_MUL THEN
ASM_REWRITE_TAC[COMPLEX_NORM_NZ] THEN ASM_REAL_ARITH_TAC;
ALL_TAC] THEN
SUBGOAL_THEN
`!w x y. w pow n = z pow n /\ x IN ball(w,d) /\ y IN ball(w,d)
==> (x pow n = y pow n <=> x = y)`
ASSUME_TAC THENL
[REWRITE_TAC[IN_BALL] THEN REPEAT STRIP_TAC THEN
FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN
SUBGOAL_THEN `norm(z pow n) = norm(w pow n)` MP_TAC THENL
[ASM_MESON_TAC[]; REWRITE_TAC[COMPLEX_NORM_POW]] THEN
DISCH_THEN(MP_TAC o MATCH_MP (ONCE_REWRITE_RULE[IMP_CONJ_ALT]
(REWRITE_RULE[CONJ_ASSOC] REAL_POW_EQ))) THEN
ASM_SIMP_TAC[LE_1; NORM_POS_LE] THEN
ASM_CASES_TAC `w = Cx(&0)` THENL
[ASM_MESON_TAC[COMPLEX_NORM_ZERO]; DISCH_THEN SUBST_ALL_TAC] THEN
MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC `&2 * d` THEN CONJ_TAC THENL
[MAP_EVERY UNDISCH_TAC
[`dist(w:complex,x) < d`; `dist(w:complex,y) < d`] THEN
CONV_TAC NORM_ARITH;
ALL_TAC] THEN
EXPAND_TAC "d" THEN MATCH_MP_TAC REAL_LE_TRANS THEN
EXISTS_TAC `&2 * e / &4 * norm(w:complex)` THEN CONJ_TAC THENL
[MATCH_MP_TAC REAL_LE_LMUL THEN REWRITE_TAC[REAL_POS] THEN
MATCH_MP_TAC REAL_LE_RMUL THEN REWRITE_TAC[NORM_POS_LE] THEN
REAL_ARITH_TAC;
ALL_TAC] THEN
ASM_SIMP_TAC[REAL_LE_LMUL_EQ; REAL_ARITH
`&2 * e / &4 * x <= e * y <=> e * x <= e * &2 * y`] THEN
FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (NORM_ARITH
`dist(z,y) < d ==> d <= &1 / &2 * norm(z)
==> norm(z) <= &2 * norm y`)) THEN
EXPAND_TAC "d" THEN MATCH_MP_TAC REAL_LE_RMUL THEN
REWRITE_TAC[NORM_POS_LE] THEN REAL_ARITH_TAC;
ALL_TAC] THEN
EXISTS_TAC `IMAGE (\w. w pow n) (ball(z,d))` THEN REPEAT CONJ_TAC THENL
[REWRITE_TAC[IN_IMAGE] THEN ASM_MESON_TAC[CENTRE_IN_BALL];
MATCH_MP_TAC INVARIANCE_OF_DOMAIN THEN
SIMP_TAC[OPEN_BALL; CONTINUOUS_ON_COMPLEX_POW; CONTINUOUS_ON_ID] THEN
ASM_MESON_TAC[];
REWRITE_TAC[SET_RULE
`~(z IN IMAGE f s) <=> (!x. x IN s ==> ~(f x = z))`] THEN
X_GEN_TAC `w:complex` THEN
ASM_SIMP_TAC[IN_BALL; COMPLEX_POW_EQ_0; LE_1] THEN
ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
SIMP_TAC[GSYM COMPLEX_VEC_0; DIST_0] THEN DISCH_TAC THEN
EXPAND_TAC "d" THEN
REWRITE_TAC[REAL_ARITH `~(z < e * z) <=> &0 <= z * (&1 - e)`] THEN
MATCH_MP_TAC REAL_LE_MUL THEN CONV_TAC NORM_ARITH;
ALL_TAC] THEN
SUBGOAL_THEN
`!z'. z' pow n = z pow n
==> IMAGE (\w. w pow n) (ball(z',d)) =
IMAGE (\w. w pow n) (ball(z,d))`
ASSUME_TAC THENL
[REWRITE_TAC[EXTENSION; IN_IMAGE; IN_BALL] THEN
X_GEN_TAC `w:complex` THEN DISCH_TAC THEN
ASM_CASES_TAC `w = Cx(&0)` THENL
[ASM_MESON_TAC[COMPLEX_POW_EQ_0; LE_1]; ALL_TAC] THEN
X_GEN_TAC `x:complex` THEN EQ_TAC THEN
DISCH_THEN(X_CHOOSE_THEN `y:complex` STRIP_ASSUME_TAC) THENL
[EXISTS_TAC `z / w * y:complex`;
EXISTS_TAC `w / z * y:complex`] THEN
ASM_SIMP_TAC[COMPLEX_POW_MUL; COMPLEX_POW_DIV; COMPLEX_DIV_REFL;
COMPLEX_POW_EQ_0; LE_1; COMPLEX_MUL_LID; dist] THEN
ASM_SIMP_TAC[COMPLEX_FIELD
`~(w = Cx(&0)) ==> z - z / w * y = z / w * (w - y)`] THEN
REWRITE_TAC[COMPLEX_NORM_MUL; COMPLEX_NORM_DIV] THEN
(SUBGOAL_THEN `norm(z pow n) = norm(w pow n)` MP_TAC THENL
[ASM_MESON_TAC[]; REWRITE_TAC[COMPLEX_NORM_POW]]) THEN
DISCH_THEN(MP_TAC o MATCH_MP (ONCE_REWRITE_RULE[IMP_CONJ_ALT]
(REWRITE_RULE[CONJ_ASSOC] REAL_POW_EQ))) THEN
ASM_SIMP_TAC[LE_1; NORM_POS_LE; REAL_DIV_REFL; COMPLEX_NORM_ZERO] THEN
ASM_REWRITE_TAC[REAL_MUL_LID; GSYM dist];
ALL_TAC] THEN
EXISTS_TAC `{ ball(z',d) | z' pow n = z pow n}` THEN
REWRITE_TAC[FORALL_IN_GSPEC] THEN REPEAT CONJ_TAC THENL
[REWRITE_TAC[UNIONS_GSPEC; EXTENSION; IN_ELIM_THM] THEN
X_GEN_TAC `x:complex` THEN EQ_TAC THENL
[DISCH_THEN(X_CHOOSE_THEN `w:complex` STRIP_ASSUME_TAC) THEN
CONJ_TAC THENL
[DISCH_TAC THEN UNDISCH_TAC `x IN ball(w:complex,d)` THEN
ASM_REWRITE_TAC[IN_BALL; GSYM COMPLEX_VEC_0; DIST_0] THEN
SUBGOAL_THEN `norm(w pow n) = norm(z pow n)` MP_TAC THENL
[ASM_MESON_TAC[]; REWRITE_TAC[COMPLEX_NORM_POW]] THEN
DISCH_THEN(MP_TAC o MATCH_MP (ONCE_REWRITE_RULE[IMP_CONJ_ALT]
(REWRITE_RULE[CONJ_ASSOC] REAL_POW_EQ))) THEN
ASM_SIMP_TAC[LE_1; NORM_POS_LE; REAL_NOT_LT] THEN DISCH_TAC THEN
EXPAND_TAC "d" THEN REWRITE_TAC[REAL_ARITH
`e * z <= z <=> &0 <= z * (&1 - e)`] THEN
MATCH_MP_TAC REAL_LE_MUL THEN CONV_TAC NORM_ARITH;
SUBGOAL_THEN `IMAGE (\w. w pow n) (ball(z,d)) =
IMAGE (\w. w pow n) (ball(w,d))`
SUBST1_TAC THENL [ASM_MESON_TAC[]; ASM SET_TAC[]]];
STRIP_TAC THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [IN_IMAGE]) THEN
REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN X_GEN_TAC `y:complex` THEN
REWRITE_TAC[IN_BALL] THEN STRIP_TAC THEN
ASM_CASES_TAC `y = Cx(&0)` THENL
[ASM_MESON_TAC[COMPLEX_POW_EQ_0; LE_1]; ALL_TAC] THEN
EXISTS_TAC `x / y * z:complex` THEN
REWRITE_TAC[COMPLEX_NORM_MUL; COMPLEX_NORM_DIV] THEN
ASM_SIMP_TAC[COMPLEX_POW_MUL; COMPLEX_POW_DIV; COMPLEX_DIV_REFL;
COMPLEX_POW_EQ_0; LE_1; COMPLEX_MUL_LID; dist] THEN
ASM_SIMP_TAC[COMPLEX_FIELD
`~(y = Cx(&0)) ==> x / y * z - x = x / y * (z - y)`] THEN
REWRITE_TAC[COMPLEX_NORM_MUL; COMPLEX_NORM_DIV] THEN
SUBGOAL_THEN `norm(y pow n) = norm(x pow n)` MP_TAC THENL
[ASM_MESON_TAC[]; REWRITE_TAC[COMPLEX_NORM_POW]] THEN
REWRITE_TAC[COMPLEX_POW_MUL; COMPLEX_POW_DIV] THEN
DISCH_THEN(MP_TAC o MATCH_MP (ONCE_REWRITE_RULE[IMP_CONJ_ALT]
(REWRITE_RULE[CONJ_ASSOC] REAL_POW_EQ))) THEN
ASM_SIMP_TAC[LE_1; NORM_POS_LE; REAL_DIV_REFL; COMPLEX_NORM_ZERO] THEN
ASM_REWRITE_TAC[REAL_MUL_LID; GSYM dist]];
X_GEN_TAC `w:complex` THEN DISCH_TAC THEN
REWRITE_TAC[OPEN_BALL; IN_BALL; REAL_NOT_LT; dist; COMPLEX_SUB_RZERO] THEN
SUBGOAL_THEN `norm(w pow n) = norm(z pow n)` MP_TAC THENL
[ASM_MESON_TAC[]; REWRITE_TAC[COMPLEX_NORM_POW]] THEN
DISCH_THEN(MP_TAC o MATCH_MP (ONCE_REWRITE_RULE[IMP_CONJ_ALT]
(REWRITE_RULE[CONJ_ASSOC] REAL_POW_EQ))) THEN
ASM_SIMP_TAC[LE_1; NORM_POS_LE] THEN DISCH_THEN SUBST1_TAC THEN
EXPAND_TAC "d" THEN
REWRITE_TAC[REAL_ARITH `e * z <= z <=> &0 <= z * (&1 - e)`] THEN
MATCH_MP_TAC REAL_LE_MUL THEN CONV_TAC NORM_ARITH;
REWRITE_TAC[pairwise; IMP_CONJ; FORALL_IN_GSPEC; RIGHT_FORALL_IMP_THM] THEN
X_GEN_TAC `u:complex` THEN DISCH_TAC THEN
X_GEN_TAC `v:complex` THEN DISCH_TAC THEN
ASM_CASES_TAC `v:complex = u` THEN ASM_REWRITE_TAC[] THEN
DISCH_THEN(K ALL_TAC) THEN
REWRITE_TAC[SET_RULE `DISJOINT s t <=> !x. x IN s /\ x IN t ==> F`] THEN
X_GEN_TAC `x:complex` THEN REWRITE_TAC[IN_BALL] THEN
DISCH_THEN(MP_TAC o MATCH_MP (NORM_ARITH
`dist(u,x) < d /\ dist(v,x) < d ==> dist(u,v) < &2 * d`)) THEN
REWRITE_TAC[REAL_NOT_LT] THEN MATCH_MP_TAC REAL_LE_TRANS THEN
EXISTS_TAC `e * norm(z:complex)` THEN CONJ_TAC THENL
[EXPAND_TAC "d" THEN REWRITE_TAC[REAL_MUL_ASSOC] THEN
MATCH_MP_TAC REAL_LE_RMUL THEN
REWRITE_TAC[NORM_POS_LE] THEN ASM_REAL_ARITH_TAC;
ONCE_REWRITE_TAC[GSYM REAL_NOT_LT] THEN REWRITE_TAC[dist]] THEN
SUBGOAL_THEN `norm(z pow n) = norm(v pow n)` MP_TAC THENL
[ASM_MESON_TAC[]; REWRITE_TAC[COMPLEX_NORM_POW]] THEN
DISCH_THEN(MP_TAC o MATCH_MP (ONCE_REWRITE_RULE[IMP_CONJ_ALT]
(REWRITE_RULE[CONJ_ASSOC] REAL_POW_EQ))) THEN
ASM_SIMP_TAC[LE_1; NORM_POS_LE] THEN ASM_MESON_TAC[];
X_GEN_TAC `w:complex` THEN DISCH_TAC THEN
SUBGOAL_THEN `IMAGE (\w. w pow n) (ball(z,d)) =
IMAGE (\w. w pow n) (ball(w,d))`
SUBST1_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
MATCH_MP_TAC INVARIANCE_OF_DOMAIN_HOMEOMORPHISM THEN
SIMP_TAC[LE_REFL; OPEN_BALL; CONTINUOUS_ON_COMPLEX_POW;
CONTINUOUS_ON_ID] THEN
ASM_MESON_TAC[]]);;
(* ------------------------------------------------------------------------- *)
(* Hence the Borsukian results about mappings into circle. *)
(* ------------------------------------------------------------------------- *)
let HOMOTOPIC_CIRCLEMAPS_DIV,HOMOTOPIC_CIRCLEMAPS_DIV_1 = (CONJ_PAIR o prove)
(`(!f g:real^N->real^2 s.
homotopic_with (\x. T) (s,sphere(vec 0,&1)) f g <=>
f continuous_on s /\ IMAGE f s SUBSET sphere(vec 0,&1) /\
g continuous_on s /\ IMAGE g s SUBSET sphere(vec 0,&1) /\
?c. homotopic_with (\x. T) (s,sphere(vec 0,&1)) (\x. f x / g x) (\x. c)) /\
(!f g:real^N->real^2 s.
homotopic_with (\x. T) (s,sphere(vec 0,&1)) f g <=>
f continuous_on s /\ IMAGE f s SUBSET sphere(vec 0,&1) /\
g continuous_on s /\ IMAGE g s SUBSET sphere(vec 0,&1) /\
homotopic_with (\x. T) (s,sphere(vec 0,&1)) (\x. f x / g x) (\x. Cx(&1)))`,
(* ------------------------------------------------------------------------- *)
(* In particular, complex logs exist on various "well-behaved" sets. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Analogously, holomorphic logarithms and square roots. *)
(* ------------------------------------------------------------------------- *)
let CONTRACTIBLE_IMP_HOLOMORPHIC_LOG,SIMPLY_CONNECTED_IMP_HOLOMORPHIC_LOG =
(CONJ_PAIR o prove)
(`(!s:complex->bool.
contractible s
==> !f. f holomorphic_on s /\ (!z. z IN s ==> ~(f z = Cx(&0)))
==> ?g. g holomorphic_on s /\ !z. z IN s ==> f z = cexp(g z)) /\
(!s:complex->bool.
simply_connected s /\ locally path_connected s
==> !f. f holomorphic_on s /\ (!z. z IN s ==> ~(f z = Cx(&0)))
==> ?g. g holomorphic_on s /\ !z. z IN s ==> f z = cexp(g z))`,
REPEAT STRIP_TAC THENL
[MP_TAC(ISPECL [`f:complex->complex`; `s:complex->bool`]
CONTINUOUS_LOGARITHM_ON_CONTRACTIBLE);
MP_TAC(ISPECL [`f:complex->complex`; `s:complex->bool`]
CONTINUOUS_LOGARITHM_ON_SIMPLY_CONNECTED)] THEN
ASM_SIMP_TAC[HOLOMORPHIC_ON_IMP_CONTINUOUS_ON] THEN
(MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `g:complex->complex` THEN
STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
UNDISCH_TAC `f holomorphic_on s` THEN
REWRITE_TAC[holomorphic_on] THEN MATCH_MP_TAC MONO_FORALL THEN
X_GEN_TAC `z:complex` THEN ASM_CASES_TAC `(z:complex) IN s` THEN
ASM_REWRITE_TAC[HAS_COMPLEX_DERIVATIVE_WITHIN] THEN
DISCH_THEN(X_CHOOSE_THEN `f':complex` MP_TAC) THEN
DISCH_THEN(MP_TAC o
ISPECL [`\x. (cexp(g x) - cexp(g z)) / (x - z)`; `&1`] o
MATCH_MP (REWRITE_RULE [TAUT `p /\ q /\ r ==> s <=> r ==> p /\ q ==> s`]
LIM_TRANSFORM_WITHIN)) THEN
ASM_SIMP_TAC[REAL_LT_01] THEN
DISCH_THEN(MP_TAC o
SPECL [`\x:complex. if g x = g z then cexp(g z)
else (cexp(g x) - cexp(g z)) / (g x - g z)`;
`cexp(g(z:complex))`] o
MATCH_MP (REWRITE_RULE[IMP_CONJ] LIM_COMPLEX_DIV)) THEN
REWRITE_TAC[CEXP_NZ] THEN ANTS_TAC THENL
[SUBGOAL_THEN
`(\x. if g x = g z then cexp(g z)
else (cexp(g x) - cexp(g(z:complex))) / (g x - g z)) =
(\y. if y = g z then cexp(g z) else (cexp y - cexp(g z)) / (y - g z)) o g`
SUBST1_TAC THENL [REWRITE_TAC[o_DEF]; ALL_TAC] THEN
MATCH_MP_TAC LIM_COMPOSE_AT THEN
EXISTS_TAC `(g:complex->complex) z` THEN REPEAT CONJ_TAC THENL
[ASM_MESON_TAC[CONTINUOUS_ON];
REWRITE_TAC[EVENTUALLY_TRUE];
ONCE_REWRITE_TAC[LIM_AT_ZERO] THEN
SIMP_TAC[COMPLEX_VEC_0; COMPLEX_ADD_SUB; COMPLEX_EQ_ADD_LCANCEL_0] THEN
MP_TAC(SPEC `cexp(g(z:complex))` (MATCH_MP LIM_COMPLEX_LMUL
LIM_CEXP_MINUS_1)) THEN REWRITE_TAC[COMPLEX_MUL_RID] THEN
MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ] LIM_TRANSFORM_EVENTUALLY) THEN
SIMP_TAC[EVENTUALLY_AT; GSYM DIST_NZ; CEXP_ADD] THEN
EXISTS_TAC `&1` THEN REWRITE_TAC[REAL_LT_01] THEN
SIMPLE_COMPLEX_ARITH_TAC];
DISCH_THEN(fun th ->
EXISTS_TAC `f' / cexp(g(z:complex))` THEN MP_TAC th) THEN
MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ]
LIM_TRANSFORM_EVENTUALLY) THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I
[CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN]) THEN
DISCH_THEN(MP_TAC o SPEC `z:complex`) THEN ASM_REWRITE_TAC[] THEN
REWRITE_TAC[CONTINUOUS_WITHIN; tendsto] THEN
DISCH_THEN(MP_TAC o SPEC `&2 * pi`) THEN
REWRITE_TAC[REAL_ARITH `&0 < &2 * x <=> &0 < x`; PI_POS] THEN
MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ] EVENTUALLY_MONO) THEN
X_GEN_TAC `w:complex` THEN REWRITE_TAC[dist] THEN DISCH_TAC THEN
COND_CASES_TAC THENL
[ASM_REWRITE_TAC[COMPLEX_SUB_REFL; complex_div; COMPLEX_MUL_LZERO];
ASM_CASES_TAC `w:complex = z` THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
SUBGOAL_THEN `~(cexp(g(w:complex)) = cexp(g z))` MP_TAC THENL
[UNDISCH_TAC `~((g:complex->complex) w = g z)` THEN
REWRITE_TAC[CONTRAPOS_THM] THEN
MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ] COMPLEX_EQ_CEXP) THEN
FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REWRITE_RULE[IMP_CONJ_ALT]
REAL_LET_TRANS)) THEN
REWRITE_TAC[GSYM IM_SUB; COMPLEX_NORM_GE_RE_IM];
REPEAT(FIRST_X_ASSUM(MP_TAC o check(is_neg o concl))) THEN
CONV_TAC COMPLEX_FIELD]]]));;
let CONTRACTIBLE_IMP_HOLOMORPHIC_SQRT,SIMPLY_CONNECTED_IMP_HOLOMORPHIC_SQRT =
(CONJ_PAIR o prove)
(`(!s:complex->bool.
contractible s
==> !f. f holomorphic_on s /\ (!z. z IN s ==> ~(f z = Cx(&0)))
==> ?g. g holomorphic_on s /\ !z. z IN s ==> f z = g z pow 2) /\
(!s:complex->bool.
simply_connected s /\ locally path_connected s
==> !f. f holomorphic_on s /\ (!z. z IN s ==> ~(f z = Cx(&0)))
==> ?g. g holomorphic_on s /\ !z. z IN s ==> f z = g z pow 2)`,
CONJ_TAC THEN GEN_TAC THENL
[DISCH_THEN(ASSUME_TAC o MATCH_MP CONTRACTIBLE_IMP_HOLOMORPHIC_LOG);
DISCH_THEN(ASSUME_TAC o
MATCH_MP SIMPLY_CONNECTED_IMP_HOLOMORPHIC_LOG)] THEN
REPEAT STRIP_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPEC `f:complex->complex`) THEN ASM_SIMP_TAC[] THEN
DISCH_THEN(X_CHOOSE_THEN `g:complex->complex` STRIP_ASSUME_TAC) THEN
EXISTS_TAC `\z:complex. cexp(g z / Cx(&2))` THEN
ASM_SIMP_TAC[GSYM CEXP_N; COMPLEX_RING `Cx(&2) * z / Cx(&2) = z`] THEN
GEN_REWRITE_TAC LAND_CONV [GSYM o_DEF] THEN
MATCH_MP_TAC HOLOMORPHIC_ON_COMPOSE THEN
REWRITE_TAC[HOLOMORPHIC_ON_CEXP] THEN
MATCH_MP_TAC HOLOMORPHIC_ON_DIV THEN
ASM_SIMP_TAC[HOLOMORPHIC_ON_CONST] THEN
CONV_TAC COMPLEX_RING);;
(* ------------------------------------------------------------------------- *)
(* Related theorems about holomorphic inverse cosines. *)
(* ------------------------------------------------------------------------- *)
let CONTRACTIBLE_IMP_HOLOMORPHIC_ACS = prove
(`!f s. f
holomorphic_on s /\
contractible s /\
(!z. z
IN s ==> ~(f z = Cx(&1)) /\ ~(f z = --Cx(&1)))
==> ?g. g
holomorphic_on s /\ !z. z
IN s ==> f z =
ccos(g z)`,
REPEAT STRIP_TAC THEN
FIRST_ASSUM(MP_TAC o SPEC `\z:complex. Cx(&1) - f(z) pow 2` o
MATCH_MP CONTRACTIBLE_IMP_HOLOMORPHIC_SQRT) THEN
ASM_SIMP_TAC[
HOLOMORPHIC_ON_SUB;
HOLOMORPHIC_ON_CONST;
HOLOMORPHIC_ON_POW;
COMPLEX_RING `~(Cx(&1) - z pow 2 = Cx(&0)) <=>
~(z = Cx(&1)) /\ ~(z = --Cx(&1))`] THEN
REWRITE_TAC[COMPLEX_RING
`Cx(&1) - w pow 2 = z pow 2 <=>
(w +
ii * z) * (w -
ii * z) = Cx(&1)`] THEN
DISCH_THEN(X_CHOOSE_THEN `g:complex->
complex` STRIP_ASSUME_TAC) THEN
FIRST_ASSUM(MP_TAC o SPEC `\z:complex. f(z) +
ii * g(z)` o
MATCH_MP CONTRACTIBLE_IMP_HOLOMORPHIC_LOG) THEN
ASM_SIMP_TAC[
HOLOMORPHIC_ON_ADD;
HOLOMORPHIC_ON_MUL;
HOLOMORPHIC_ON_CONST;
COMPLEX_RING `(a + b) * (a - b) = Cx(&1) ==> ~(a + b = Cx(&0))`] THEN
DISCH_THEN(X_CHOOSE_THEN `h:complex->
complex` STRIP_ASSUME_TAC) THEN
EXISTS_TAC `\z:complex. --ii * h(z)` THEN
ASM_SIMP_TAC[
HOLOMORPHIC_ON_MUL;
HOLOMORPHIC_ON_CONST;
ccos] THEN
X_GEN_TAC `z:complex` THEN
DISCH_TAC THEN REPEAT(FIRST_X_ASSUM(MP_TAC o SPEC `z:complex`)) THEN
ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC THEN
FIRST_X_ASSUM(MP_TAC o MATCH_MP (COMPLEX_FIELD
`a * b = Cx(&1) ==> b = inv a`)) THEN
ASM_SIMP_TAC[GSYM
CEXP_NEG] THEN
FIRST_X_ASSUM(ASSUME_TAC o SYM) THEN DISCH_THEN(ASSUME_TAC o SYM) THEN
ASM_REWRITE_TAC[COMPLEX_RING `
ii * --ii * z = z`;
COMPLEX_RING `--ii * --ii * z = --z`] THEN
CONV_TAC COMPLEX_RING);;
(* ------------------------------------------------------------------------- *)
(* Another interesting equivalent of an inessential mapping into C-{0} *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Unicoherence. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Another simple case where sphere maps are nullhomotopic. *)
(* ------------------------------------------------------------------------- *)
let INESSENTIAL_SPHEREMAP_2 = prove
(`!f:real^M->real^N a r b s.
2 <
dimindex(:M) /\
dimindex(:N) = 2 /\
f
continuous_on sphere(a,r) /\
IMAGE f (
sphere(a,r))
SUBSET (
sphere(b,s))
==> ?c.
homotopic_with (\z. T) (
sphere(a,r),
sphere(b,s)) f (\x. c)`,
let lemma = prove
(`!f:real^N->real^2 a r.
2 < dimindex(:N) /\
f continuous_on sphere(a,r) /\
IMAGE f (sphere(a,r)) SUBSET (sphere(vec 0,&1))
==> ?c. homotopic_with (\z. T) (sphere(a,r),sphere(vec 0,&1))
f (\x. c)`,
REPEAT STRIP_TAC THEN
REWRITE_TAC[INESSENTIAL_EQ_CONTINUOUS_LOGARITHM_CIRCLE] THEN
MP_TAC(ISPECL [`f:real^N->real^2`; `sphere(a:real^N,r)`]
CONTINUOUS_LOGARITHM_ON_SIMPLY_CONNECTED) THEN
ASM_SIMP_TAC[SIMPLY_CONNECTED_SPHERE_EQ; LOCALLY_PATH_CONNECTED_SPHERE] THEN
ANTS_TAC THENL
[ASM_REWRITE_TAC[ARITH_RULE `3 <= n <=> 2 < n`] THEN FIRST_X_ASSUM
(MATCH_MP_TAC o MATCH_MP (SET_RULE
`IMAGE f s SUBSET t ==> (!x. P x ==> ~(x IN t))
==> !x. x IN s ==> ~P(f x)`)) THEN
SIMP_TAC[COMPLEX_NORM_0; IN_SPHERE_0] THEN REAL_ARITH_TAC;
DISCH_THEN(X_CHOOSE_THEN `g:real^N->real^2` STRIP_ASSUME_TAC) THEN
EXISTS_TAC `Im o (g:real^N->real^2)` THEN CONJ_TAC THENL
[REWRITE_TAC[o_ASSOC] THEN MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN
ASM_REWRITE_TAC[CONTINUOUS_ON_CX_IM];
X_GEN_TAC `x:real^N` THEN DISCH_TAC THEN
ASM_SIMP_TAC[] THEN AP_TERM_TAC THEN
REWRITE_TAC[o_DEF; COMPLEX_EQ; RE_MUL_II; IM_MUL_II; RE_CX; IM_CX] THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [SUBSET]) THEN
REWRITE_TAC[FORALL_IN_IMAGE] THEN
DISCH_THEN(MP_TAC o SPEC `x:real^N`) THEN
ASM_SIMP_TAC[IN_SPHERE_0; NORM_CEXP; REAL_EXP_EQ_1] THEN
REAL_ARITH_TAC]])
and hslemma = prove
(`!a:real^M r b:real^N s.
dimindex(:M) = dimindex(:N) /\ &0 < r /\ &0 < s
==> (sphere(a,r) homeomorphic sphere(b,s))`,
REPEAT STRIP_TAC THEN FIRST_ASSUM(fun th ->
let t = `?a:real^M b:real^N. ~(sphere(a,r) homeomorphic sphere(b,s))` in
MP_TAC(DISCH t (GEOM_EQUAL_DIMENSION_RULE th (ASSUME t)))) THEN
ASM_SIMP_TAC[HOMEOMORPHIC_SPHERES] THEN MESON_TAC[]) in
REPEAT STRIP_TAC THEN ASM_CASES_TAC `s <= &0` THEN
ASM_SIMP_TAC[NULLHOMOTOPIC_INTO_CONTRACTIBLE; CONTRACTIBLE_SPHERE] THEN
RULE_ASSUM_TAC(REWRITE_RULE[REAL_NOT_LE]) THEN
SUBGOAL_THEN
`(sphere(b:real^N,s)) homeomorphic (sphere(vec 0:real^2,&1))`
MP_TAC THENL
[ASM_SIMP_TAC[hslemma; REAL_LT_01; DIMINDEX_2];
REWRITE_TAC[homeomorphic; LEFT_IMP_EXISTS_THM]] THEN
MAP_EVERY X_GEN_TAC [`h:real^N->real^2`; `k:real^2->real^N`] THEN
REWRITE_TAC[homeomorphism] THEN STRIP_TAC THEN
MP_TAC(ISPECL
[`(h:real^N->real^2) o (f:real^M->real^N)`;
`a:real^M`; `r:real`] lemma) THEN
ASM_REWRITE_TAC[IMAGE_o] THEN ANTS_TAC THENL
[CONJ_TAC THENL [MATCH_MP_TAC CONTINUOUS_ON_COMPOSE; ASM SET_TAC[]] THEN
ASM_MESON_TAC[CONTINUOUS_ON_SUBSET];
DISCH_THEN(X_CHOOSE_THEN `c:real^2` (fun th ->
EXISTS_TAC `(k:real^2->real^N) c` THEN MP_TAC th)) THEN
DISCH_THEN(MP_TAC o ISPEC `k:real^2->real^N` o MATCH_MP
(ONCE_REWRITE_RULE[IMP_CONJ] HOMOTOPIC_COMPOSE_CONTINUOUS_LEFT)) THEN
DISCH_THEN(MP_TAC o SPEC `sphere(b:real^N,s)`) THEN
ASM_REWRITE_TAC[SUBSET_REFL] THEN
MATCH_MP_TAC(ONCE_REWRITE_RULE[IMP_CONJ_ALT] HOMOTOPIC_WITH_EQ) THEN
REWRITE_TAC[o_DEF] THEN ASM SET_TAC[]]);;
(* ------------------------------------------------------------------------- *)
(* Janiszewski's theorem. *)
(* ------------------------------------------------------------------------- *)