(* ========================================================================= *)
(* Convex sets, functions and related things. *)
(* *)
(* (c) Copyright, John Harrison 1998-2008 *)
(* (c) Copyright, Lars Schewe 2007 *)
(* (c) Copyright, Valentina Bruno 2010 *)
(* ========================================================================= *)
needs "Multivariate/topology.ml";;
(* ------------------------------------------------------------------------- *)
(* Some miscelleneous things that are convenient to prove here. *)
(* ------------------------------------------------------------------------- *)
let TRANSLATION_GALOIS = prove
(`!s t a:real^N. s =
IMAGE (\x. a + x) t <=> t =
IMAGE (\x. --a + x) s`,
REPEAT STRIP_TAC THEN EQ_TAC THEN DISCH_TAC THEN
ASM_REWRITE_TAC[GSYM
IMAGE_o;
o_DEF] THEN
REWRITE_TAC[VECTOR_ARITH `--a + a + x:real^N = x`;
VECTOR_ARITH `a + --a + x:real^N = x`] THEN
REWRITE_TAC[
IMAGE_ID]);;
let TRANSLATION_EQ_IMP = prove
(`!P:(real^N->bool)->bool.
(!a s. P(
IMAGE (\x. a + x) s) <=> P s) <=>
(!a s. P s ==> P (
IMAGE (\x. a + x) s))`,
REPEAT GEN_TAC THEN EQ_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
MAP_EVERY X_GEN_TAC [`a:real^N`; `s:real^N->bool`] THEN
EQ_TAC THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN FIRST_X_ASSUM
(MP_TAC o SPECL [`--a:real^N`; `
IMAGE (\x:real^N. a + x) s`]) THEN
ASM_REWRITE_TAC[GSYM
IMAGE_o;
o_DEF;
IMAGE_ID;
VECTOR_ARITH `--a + a + x:real^N = x`]);;
(* ------------------------------------------------------------------------- *)
(* Affine set and affine hull. *)
(* ------------------------------------------------------------------------- *)
let affine = new_definition
`affine s <=> !x y u v. x IN s /\ y IN s /\ (u + v = &1)
==> (u % x + v % y) IN s`;;
add_translation_invariants [AFFINE_TRANSLATION_EQ];;
add_linear_invariants [AFFINE_LINEAR_IMAGE_EQ];;
add_translation_invariants [AFFINE_HULL_TRANSLATION];;
add_linear_invariants [AFFINE_HULL_LINEAR_IMAGE];;
(* ------------------------------------------------------------------------- *)
(* Some convenient lemmas about common affine combinations. *)
(* ------------------------------------------------------------------------- *)
let IN_AFFINE_ADD_MUL = prove
(`!s a x:real^N d.
affine s /\ a
IN s /\ (a + x)
IN s ==> (a + d % x)
IN s`,
REWRITE_TAC[
affine] THEN REPEAT STRIP_TAC THEN
SUBST1_TAC(VECTOR_ARITH `a + d % x:real^N = (&1 - d) % a + d % (a + x)`) THEN
FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);;
let IN_AFFINE_ADD_MUL_DIFF = prove
(`!s a x y z:real^N.
affine s /\ x
IN s /\ y
IN s /\ z
IN s ==> (x + a % (y - z))
IN s`,
REWRITE_TAC[
affine] THEN REPEAT STRIP_TAC THEN
REWRITE_TAC[VECTOR_ARITH
`x + a % (y - z):real^N =
&1 / &2 % ((&1 - &2 * a) % x + (&2 * a) % y) +
&1 / &2 % ((&1 + &2 * a) % x + (-- &2 * a) % z)`] THEN
FIRST_ASSUM MATCH_MP_TAC THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
CONJ_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN
REAL_ARITH_TAC);;
(* ------------------------------------------------------------------------- *)
(* Explicit formulations for affine combinations. *)
(* ------------------------------------------------------------------------- *)
let AFFINE_VSUM = prove
(`!s k u x:A->real^N.
FINITE k /\
affine s /\
sum k u = &1 /\ (!i. i
IN k ==> x i
IN s)
==>
vsum k (\i. u i % x i)
IN s`,
REPEAT GEN_TAC THEN ASM_CASES_TAC `s:real^N->bool = {}` THENL
[ASM_REWRITE_TAC[
NOT_IN_EMPTY; GSYM
NOT_EXISTS_THM;
MEMBER_NOT_EMPTY] THEN
ASM_CASES_TAC `k:A->bool = {}` THEN ASM_REWRITE_TAC[
SUM_CLAUSES] THEN
REAL_ARITH_TAC;
ALL_TAC] THEN
STRIP_TAC THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM
MEMBER_NOT_EMPTY]) THEN
DISCH_THEN(X_CHOOSE_TAC `a:real^N`) THEN
MP_TAC(ISPECL [`s:real^N->bool`; `a:real^N`]
AFFINE_DIFFS_SUBSPACE) THEN
ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
MP_TAC(ISPECL [`{x - a:real^N | x
IN s}`;
`(\i. u i % (x i - a)):A->real^N`;
`k:A->bool`]
SUBSPACE_VSUM) THEN
ANTS_TAC THENL
[ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC THEN
MATCH_MP_TAC
SUBSPACE_MUL THEN ASM_REWRITE_TAC[] THEN ASM SET_TAC[];
ASM_SIMP_TAC[
VSUM_SUB;
IN_ELIM_THM;
VECTOR_SUB_LDISTRIB;
VSUM_RMUL] THEN
REWRITE_TAC[VECTOR_ARITH `x - &1 % a:real^N = y - a <=> x = y`] THEN
ASM_MESON_TAC[]]);;
let AFFINE_INDEXED = prove
(`!s:real^N->bool.
affine s <=>
!k u x. (!i:num. 1 <= i /\ i <= k ==> x(i)
IN s) /\
(
sum (1..k) u = &1)
==>
vsum (1..k) (\i. u(i) % x(i))
IN s`,
REPEAT GEN_TAC THEN EQ_TAC THENL
[REPEAT STRIP_TAC THEN MATCH_MP_TAC
AFFINE_VSUM THEN
ASM_REWRITE_TAC[
IN_NUMSEG;
FINITE_NUMSEG];
DISCH_TAC THEN REWRITE_TAC[
affine] THEN
MAP_EVERY X_GEN_TAC [`x:real^N`; `y:real^N`; `u:real`; `v:real`] THEN
STRIP_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC `2`) THEN
DISCH_THEN(MP_TAC o SPEC `\n. if n = 1 then u else v:real`) THEN
DISCH_THEN(MP_TAC o SPEC `\n. if n = 1 then x else y:real^N`) THEN
REWRITE_TAC[num_CONV `2`;
SUM_CLAUSES_NUMSEG;
VSUM_CLAUSES_NUMSEG;
NUMSEG_SING;
VSUM_SING;
SUM_SING] THEN REWRITE_TAC[ARITH] THEN
ASM_MESON_TAC[]]);;
let AFFINE_EXPLICIT = prove
(`!s:real^N->bool.
affine s <=>
!t u. FINITE t /\ t
SUBSET s /\
sum t u = &1
==>
vsum t (\x. u(x) % x)
IN s`,
GEN_TAC THEN REWRITE_TAC[
AFFINE] THEN
AP_TERM_TAC THEN GEN_REWRITE_TAC I [
FUN_EQ_THM] THEN
X_GEN_TAC `t:real^N->bool` THEN REWRITE_TAC[] THEN
AP_TERM_TAC THEN ABS_TAC THEN
ASM_CASES_TAC `t:real^N->bool = {}` THEN
ASM_REWRITE_TAC[
SUM_CLAUSES] THEN CONV_TAC REAL_RAT_REDUCE_CONV);;
(* ------------------------------------------------------------------------- *)
(* Stepping theorems and hence small special cases. *)
(* ------------------------------------------------------------------------- *)
let AFFINE_HULL_FINITE_STEP_GEN = prove
(`!P:real^N->real->bool.
((?u. (!x. x
IN {} ==> P x (u x)) /\
sum {} u = w /\
vsum {} (\x. u(x) % x) = y) <=>
w = &0 /\ y =
vec 0) /\
(FINITE(s:real^N->bool) /\
(!y. a
IN s /\ P a y ==> P a (y / &2)) /\
(!x y. a
IN s /\ P a x /\ P a y ==> P a (x + y))
==> ((?u. (!x. x
IN (a
INSERT s) ==> P x (u x)) /\
sum (a
INSERT s) u = w /\
vsum (a
INSERT s) (\x. u(x) % x) = y) <=>
?v u. P a v /\ (!x. x
IN s ==> P x (u x)) /\
sum s u = w - v /\
vsum s (\x. u(x) % x) = y - v % a))`,
GEN_TAC THEN SIMP_TAC[
SUM_CLAUSES;
VSUM_CLAUSES;
NOT_IN_EMPTY] THEN
CONJ_TAC THENL [MESON_TAC[]; ALL_TAC] THEN DISCH_TAC THEN
ASM_CASES_TAC `(a:real^N)
IN s` THEN ASM_REWRITE_TAC[] THENL
[ASM_SIMP_TAC[SET_RULE `a
IN s ==> a
INSERT s = s`] THEN EQ_TAC THEN
REWRITE_TAC[
LEFT_IMP_EXISTS_THM] THENL
[X_GEN_TAC `u:real^N->
real` THEN STRIP_TAC THEN
EXISTS_TAC `(u:real^N->
real) a / &2` THEN
EXISTS_TAC `\x:real^N. if x = a then u x / &2 else u x`;
MAP_EVERY X_GEN_TAC [`v:real`; `u:real^N->
real`] THEN
STRIP_TAC THEN
EXISTS_TAC `\x:real^N. if x = a then u x + v else u x`] THEN
ASM_SIMP_TAC[] THEN (CONJ_TAC THENL [ASM_MESON_TAC[]; ALL_TAC]) THEN
ONCE_REWRITE_TAC[
COND_RAND] THEN ONCE_REWRITE_TAC[
COND_RATOR] THEN
ASM_SIMP_TAC[
VSUM_CASES;
SUM_CASES] THEN
ASM_SIMP_TAC[GSYM
DELETE;
SUM_DELETE;
VSUM_DELETE] THEN
ASM_SIMP_TAC[SET_RULE `a
IN s ==> {x | x
IN s /\ x = a} = {a}`] THEN
REWRITE_TAC[
SUM_SING;
VSUM_SING] THEN
(CONJ_TAC THENL [REAL_ARITH_TAC; VECTOR_ARITH_TAC]);
EQ_TAC THEN REWRITE_TAC[
LEFT_IMP_EXISTS_THM] THENL
[X_GEN_TAC `u:real^N->
real` THEN STRIP_TAC THEN
EXISTS_TAC `(u:real^N->
real) a` THEN
EXISTS_TAC `u:real^N->
real` THEN ASM_SIMP_TAC[
IN_INSERT] THEN
REPEAT(FIRST_X_ASSUM(SUBST1_TAC o SYM)) THEN
CONJ_TAC THENL [REAL_ARITH_TAC; VECTOR_ARITH_TAC];
MAP_EVERY X_GEN_TAC [`v:real`; `u:real^N->
real`] THEN
STRIP_TAC THEN
EXISTS_TAC `\x:real^N. if x = a then v:real else u x` THEN
ASM_SIMP_TAC[
IN_INSERT] THEN CONJ_TAC THENL
[ASM_MESON_TAC[]; ALL_TAC] THEN
ONCE_REWRITE_TAC[
COND_RAND] THEN ONCE_REWRITE_TAC[
COND_RATOR] THEN
ASM_SIMP_TAC[
VSUM_CASES;
SUM_CASES] THEN
ASM_SIMP_TAC[GSYM
DELETE;
SUM_DELETE;
VSUM_DELETE] THEN
ASM_SIMP_TAC[SET_RULE `~(a
IN s) ==> {x | x
IN s /\ x = a} = {}`] THEN
ASM_SIMP_TAC[SET_RULE `~(a
IN s) ==> s
DELETE a = s`] THEN
REWRITE_TAC[
SUM_CLAUSES;
VSUM_CLAUSES] THEN
CONJ_TAC THENL [REAL_ARITH_TAC; VECTOR_ARITH_TAC]]]);;
(* ------------------------------------------------------------------------- *)
(* Some relations between affine hull and subspaces. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Convexity. *)
(* ------------------------------------------------------------------------- *)
let convex = new_definition
`convex s <=>
!x y u v. x IN s /\ y IN s /\ &0 <= u /\ &0 <= v /\ (u + v = &1)
==> (u % x + v % y) IN s`;;
let CONVEX_ALT = prove
(`
convex s <=> !x y u. x
IN s /\ y
IN s /\ &0 <= u /\ u <= &1
==> ((&1 - u) % x + u % y)
IN s`,
REWRITE_TAC[
convex] THEN
MESON_TAC[REAL_ARITH `&0 <= u /\ &0 <= v /\ (u + v = &1)
==> v <= &1 /\ (u = &1 - v)`;
REAL_ARITH `u <= &1 ==> &0 <= &1 - u /\ ((&1 - u) + u = &1)`]);;
let LIMPT_OF_CONVEX = prove
(`!s x:real^N.
convex s /\ x
IN s ==> (x
limit_point_of s <=> ~(s = {x}))`,
REPEAT STRIP_TAC THEN
ASM_CASES_TAC `s = {x:real^N}` THEN ASM_REWRITE_TAC[
LIMPT_SING] THEN
SUBGOAL_THEN `?y:real^N. y
IN s /\ ~(y = x)` STRIP_ASSUME_TAC THENL
[ASM SET_TAC[]; ALL_TAC] THEN
REWRITE_TAC[
LIMPT_APPROACHABLE] THEN X_GEN_TAC `e:real` THEN DISCH_TAC THEN
ABBREV_TAC `u = min (&1 / &2) (e / &2 /
norm(y - x:real^N))` THEN
SUBGOAL_THEN `&0 < u /\ u < &1` STRIP_ASSUME_TAC THENL
[EXPAND_TAC "u" THEN REWRITE_TAC[
REAL_LT_MIN;
REAL_MIN_LT] THEN
CONV_TAC REAL_RAT_REDUCE_CONV THEN
ASM_SIMP_TAC[
REAL_HALF;
REAL_LT_DIV;
NORM_POS_LT;
VECTOR_SUB_EQ];
ALL_TAC] THEN
EXISTS_TAC `(&1 - u) % x + u % y:real^N` THEN REPEAT CONJ_TAC THENL
[FIRST_ASSUM(MATCH_MP_TAC o GEN_REWRITE_RULE I [
CONVEX_ALT]) THEN
ASM_SIMP_TAC[
REAL_LT_IMP_LE];
ASM_REWRITE_TAC[
VECTOR_MUL_EQ_0;
VECTOR_SUB_EQ; VECTOR_ARITH
`(&1 - u) % x + u % y:real^N = x <=> u % (y - x) =
vec 0`] THEN
ASM_REAL_ARITH_TAC;
REWRITE_TAC[
dist;
NORM_MUL; VECTOR_ARITH
`((&1 - u) % x + u % y) - x:real^N = u % (y - x)`] THEN
ASM_SIMP_TAC[REAL_ARITH `&0 < u ==> abs u = u`] THEN
MATCH_MP_TAC(REAL_ARITH `x <= e / &2 /\ &0 < e ==> x < e`) THEN
ASM_SIMP_TAC[GSYM
REAL_LE_RDIV_EQ;
NORM_POS_LT;
VECTOR_SUB_EQ] THEN
ASM_REAL_ARITH_TAC]);;
(* ------------------------------------------------------------------------- *)
(* Some invariance theorems for convex sets. *)
(* ------------------------------------------------------------------------- *)
add_translation_invariants [CONVEX_TRANSLATION_EQ];;
add_linear_invariants [CONVEX_LINEAR_IMAGE_EQ];;
(* ------------------------------------------------------------------------- *)
(* Explicit expressions for convexity in terms of arbitrary sums. *)
(* ------------------------------------------------------------------------- *)
let CONVEX_INDEXED = prove
(`!s:real^N->bool.
convex s <=>
!k u x. (!i:num. 1 <= i /\ i <= k ==> &0 <= u(i) /\ x(i)
IN s) /\
(
sum (1..k) u = &1)
==>
vsum (1..k) (\i. u(i) % x(i))
IN s`,
REPEAT GEN_TAC THEN EQ_TAC THENL
[REPEAT STRIP_TAC THEN MATCH_MP_TAC
CONVEX_VSUM THEN
ASM_REWRITE_TAC[
IN_NUMSEG;
FINITE_NUMSEG];
DISCH_TAC THEN REWRITE_TAC[
convex] THEN
MAP_EVERY X_GEN_TAC [`x:real^N`; `y:real^N`; `u:real`; `v:real`] THEN
STRIP_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC `2`) THEN
DISCH_THEN(MP_TAC o SPEC `\n. if n = 1 then u else v:real`) THEN
DISCH_THEN(MP_TAC o SPEC `\n. if n = 1 then x else y:real^N`) THEN
REWRITE_TAC[num_CONV `2`;
SUM_CLAUSES_NUMSEG;
VSUM_CLAUSES_NUMSEG;
NUMSEG_SING;
VSUM_SING;
SUM_SING] THEN REWRITE_TAC[ARITH] THEN
ASM_MESON_TAC[]]);;
let CONVEX = prove
(`!V:real^N->bool.
convex V <=>
!(s:real^N->bool) (u:real^N->
real).
FINITE s /\ ~(s = {}) /\ s
SUBSET V /\
(!x. x
IN s ==> &0 <= u x) /\
sum s u = &1
==>
vsum s (\x. u x % x)
IN V`,
GEN_TAC THEN REWRITE_TAC[
CONVEX_EXPLICIT] THEN
AP_TERM_TAC THEN GEN_REWRITE_TAC I [
FUN_EQ_THM] THEN
X_GEN_TAC `t:real^N->bool` THEN REWRITE_TAC[] THEN
AP_TERM_TAC THEN ABS_TAC THEN
ASM_CASES_TAC `t:real^N->bool = {}` THEN
ASM_REWRITE_TAC[
SUM_CLAUSES] THEN CONV_TAC REAL_RAT_REDUCE_CONV);;
(* ------------------------------------------------------------------------- *)
(* Conic sets and conic hull. *)
(* ------------------------------------------------------------------------- *)
add_linear_invariants [CONIC_LINEAR_IMAGE_EQ];;
add_linear_invariants [CONIC_HULL_LINEAR_IMAGE];;
(* ------------------------------------------------------------------------- *)
(* Affine dependence and consequential theorems (from Lars Schewe). *)
(* ------------------------------------------------------------------------- *)
add_translation_invariants [AFFINE_DEPENDENT_TRANSLATION_EQ];;
add_linear_invariants [AFFINE_DEPENDENT_LINEAR_IMAGE_EQ];;
(* ------------------------------------------------------------------------- *)
(* Coplanarity, and collinearity in terms of affine hull. *)
(* ------------------------------------------------------------------------- *)
let COLLINEAR_AFFINE_HULL = prove
(`!s:real^N->bool.
collinear s <=> ?u v. s
SUBSET affine hull {u,v}`,
GEN_TAC THEN REWRITE_TAC[
collinear;
AFFINE_HULL_2] THEN EQ_TAC THEN
REWRITE_TAC[
SUBSET;
IN_ELIM_THM;
LEFT_IMP_EXISTS_THM] THEN
REWRITE_TAC[REAL_ARITH `u + v = &1 <=> &1 - u = v`;
UNWIND_THM1] THENL
[X_GEN_TAC `u:real^N` THEN DISCH_TAC THEN
ASM_CASES_TAC `s:real^N->bool = {}` THEN
ASM_REWRITE_TAC[
NOT_IN_EMPTY] THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM
MEMBER_NOT_EMPTY]) THEN
MATCH_MP_TAC
MONO_EXISTS THEN X_GEN_TAC `x:real^N` THEN
DISCH_TAC THEN EXISTS_TAC `x + u:real^N` THEN X_GEN_TAC `y:real^N` THEN
DISCH_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPECL [`x:real^N`; `y:real^N`]) THEN
ASM_REWRITE_TAC[VECTOR_ARITH `x - y:real^N = z <=> x = y + z`] THEN
DISCH_THEN(X_CHOOSE_THEN `c:real` SUBST1_TAC) THEN
EXISTS_TAC `&1 + c` THEN VECTOR_ARITH_TAC;
MAP_EVERY X_GEN_TAC [`a:real^N`; `b:real^N`] THEN DISCH_TAC THEN
EXISTS_TAC `b - a:real^N` THEN
MAP_EVERY X_GEN_TAC [`x:real^N`; `y:real^N`] THEN STRIP_TAC THEN
FIRST_X_ASSUM(fun
th ->
MP_TAC(SPEC `y:real^N`
th) THEN MP_TAC(SPEC `x:real^N`
th)) THEN
ASM_REWRITE_TAC[
LEFT_IMP_EXISTS_THM] THEN
X_GEN_TAC `r:real` THEN DISCH_THEN SUBST1_TAC THEN
X_GEN_TAC `s:real` THEN DISCH_THEN SUBST1_TAC THEN
EXISTS_TAC `s - r:real` THEN VECTOR_ARITH_TAC]);;
add_translation_invariants [COPLANAR_TRANSLATION_EQ];;
add_linear_invariants [COPLANAR_LINEAR_IMAGE_EQ];;
(* ------------------------------------------------------------------------- *)
(* A general lemma. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Various topological facts are queued up here, just because they rely on *)
(* CONNECTED_UNIV, which is a trivial consequence of CONVEX_UNIV. It would *)
(* be fairly easy to prove it earlier and move these back to the topology.ml *)
(* file, which is a bit tidier intellectually. *)
(* ------------------------------------------------------------------------- *)
let EQ_INTERVAL = prove
(`(!a b c d:real^N.
interval[a,b] =
interval[c,d] <=>
interval[a,b] = {} /\
interval[c,d] = {} \/ a = c /\ b = d) /\
(!a b c d:real^N.
interval[a,b] =
interval(c,d) <=>
interval[a,b] = {} /\
interval(c,d) = {}) /\
(!a b c d:real^N.
interval(a,b) =
interval[c,d] <=>
interval(a,b) = {} /\
interval[c,d] = {}) /\
(!a b c d:real^N.
interval(a,b) =
interval(c,d) <=>
interval(a,b) = {} /\
interval(c,d) = {} \/ a = c /\ b = d)`,
let EQ_BALLS = prove
(`(!a a':real^N r r'.
ball(a,r) =
ball(a',r') <=> a = a' /\ r = r' \/ r <= &0 /\ r' <= &0) /\
(!a a':real^N r r'.
ball(a,r) =
cball(a',r') <=> r <= &0 /\ r' < &0) /\
(!a a':real^N r r'.
cball(a,r) =
ball(a',r') <=> r < &0 /\ r' <= &0) /\
(!a a':real^N r r'.
cball(a,r) =
cball(a',r') <=> a = a' /\ r = r' \/ r < &0 /\ r' < &0)`,
(* ------------------------------------------------------------------------- *)
(* Convex functions into the reals. *)
(* ------------------------------------------------------------------------- *)
parse_as_infix ("convex_on",(12,"right"));;
let convex_on = new_definition
`f convex_on s <=>
!x y u v. x IN s /\ y IN s /\ &0 <= u /\ &0 <= v /\ (u + v = &1)
==> f(u % x + v % y) <= u * f(x) + v * f(y)`;;
let CONVEX_LOCAL_GLOBAL_MINIMUM = prove
(`!f s t x:real^N.
f
convex_on s /\ x
IN t /\ open t /\ t
SUBSET s /\
(!y. y
IN t ==> f(x) <= f(y))
==> !y. y
IN s ==> f(x) <= f(y)`,
REPEAT STRIP_TAC THEN REWRITE_TAC[GSYM
REAL_NOT_LT] THEN DISCH_TAC THEN
SUBGOAL_THEN `&0 <
dist(x:real^N,y)` ASSUME_TAC THENL
[ASM_MESON_TAC[
DIST_POS_LT;
REAL_LT_REFL]; ALL_TAC] THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [
OPEN_CONTAINS_BALL]) THEN
DISCH_THEN(MP_TAC o SPEC `x:real^N`) THEN ASM_REWRITE_TAC[] THEN
DISCH_THEN(X_CHOOSE_THEN `e:real` STRIP_ASSUME_TAC) THEN
MP_TAC(SPECL [`&1`; `e /
dist(x:real^N,y)`]
REAL_DOWN2) THEN
ANTS_TAC THENL [ASM_SIMP_TAC[
REAL_LT_DIV;
REAL_LT_01]; ALL_TAC] THEN
DISCH_THEN(X_CHOOSE_THEN `u:real` STRIP_ASSUME_TAC) THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [
convex_on]) THEN
DISCH_THEN(MP_TAC o
SPECL [`x:real^N`; `y:real^N`; `&1 - u`; `u:real`]) THEN
ANTS_TAC THENL
[ASM_SIMP_TAC[
REAL_SUB_ADD;
REAL_SUB_LE;
REAL_LT_IMP_LE] THEN
ASM_MESON_TAC[
CENTRE_IN_BALL;
SUBSET];
ALL_TAC] THEN
REWRITE_TAC[
REAL_NOT_LE] THEN MATCH_MP_TAC
REAL_LTE_TRANS THEN
EXISTS_TAC `(&1 - u) * f(x) + u * f(x:real^N):real` THEN
ASM_SIMP_TAC[
REAL_LT_LADD;
REAL_LT_LMUL] THEN
REWRITE_TAC[REAL_ARITH `(&1 - x) * a + x * a = a`] THEN
FIRST_X_ASSUM MATCH_MP_TAC THEN
FIRST_X_ASSUM(MATCH_MP_TAC o GEN_REWRITE_RULE I [
SUBSET]) THEN
REWRITE_TAC[
IN_BALL;
dist] THEN
REWRITE_TAC[VECTOR_ARITH `x - ((&1 - u) % x + u % y):real^N =
u % (x - y)`] THEN
REWRITE_TAC[
NORM_MUL; GSYM
dist] THEN
ASM_SIMP_TAC[GSYM
REAL_LT_RDIV_EQ;
REAL_ARITH `&0 < x /\ x < b ==> abs x < b`]);;
(* ------------------------------------------------------------------------- *)
(* Open and closed balls are convex and hence connected. *)
(* ------------------------------------------------------------------------- *)
let CONVEX_CBALL = prove
(`!x:real^N e.
convex(
cball(x,e))`,
REWRITE_TAC[
convex;
IN_CBALL;
dist] THEN MAP_EVERY X_GEN_TAC
[`x:real^N`; `e:real`; `y:real^N`; `z:real^N`; `u:real`; `v:real`] THEN
STRIP_TAC THEN ONCE_REWRITE_TAC[VECTOR_ARITH `a - b = &1 % a - b`] THEN
FIRST_ASSUM(SUBST1_TAC o SYM) THEN
REWRITE_TAC[VECTOR_ARITH
`(a + b) % x - (a % y + b % z) = a % (x - y) + b % (x - z)`] THEN
MATCH_MP_TAC
REAL_LE_TRANS THEN
EXISTS_TAC `
norm(u % (x - y)) +
norm(v % (x - z):real^N)` THEN
REWRITE_TAC[
NORM_TRIANGLE;
NORM_MUL] THEN
MATCH_MP_TAC
REAL_CONVEX_BOUND_LE THEN ASM_REWRITE_TAC[
REAL_ABS_POS] THEN
ASM_SIMP_TAC[REAL_ARITH
`&0 <= u /\ &0 <= v /\ (u + v = &1) ==> (abs(u) + abs(v) = &1)`]);;
(* ------------------------------------------------------------------------- *)
(* A couple of lemmas about components (see Newman IV, 3.3 and 3.4). *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Sura-Bura's result about components of closed sets. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Condition for an open map's image to contain a ball. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Arithmetic operations on sets preserve convexity. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Convex hull. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Stepping theorems for convex hulls of finite sets. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Explicit expression for convex hull. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Another formulation from Lars Schewe. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* A stepping theorem for that expansion. *)
(* ------------------------------------------------------------------------- *)
let CONVEX_HULL_FINITE_STEP = prove
(`((?u. (!x. x
IN {} ==> &0 <= u x) /\
sum {} u = w /\
vsum {} (\x. u(x) % x) = y) <=> w = &0 /\ y =
vec 0) /\
(FINITE(s:real^N->bool)
==> ((?u. (!x. x
IN (a
INSERT s) ==> &0 <= u x) /\
sum (a
INSERT s) u = w /\
vsum (a
INSERT s) (\x. u(x) % x) = y) <=>
?v. &0 <= v /\
?u. (!x. x
IN s ==> &0 <= u x) /\
sum s u = w - v /\
vsum s (\x. u(x) % x) = y - v % a))`,
(* ------------------------------------------------------------------------- *)
(* Hence some special cases. *)
(* ------------------------------------------------------------------------- *)
let CONVEX_HULL_2_ALT = prove
(`!a b.
convex hull {a,b} = {a + u % (b - a) | &0 <= u /\ u <= &1}`,
ONCE_REWRITE_TAC[SET_RULE `{a,b} = {b,a}`] THEN
REWRITE_TAC[
CONVEX_HULL_2;
EXTENSION;
IN_ELIM_THM] THEN
REWRITE_TAC[REAL_ADD_ASSOC;
CONJ_ASSOC] THEN
REWRITE_TAC[TAUT `(a /\ x + y = &1) /\ b <=> x + y = &1 /\ a /\ b`] THEN
REWRITE_TAC[REAL_ARITH `x + y = &1 <=> y = &1 - x`;
UNWIND_THM2] THEN
REPEAT GEN_TAC THEN REPEAT(AP_TERM_TAC THEN ABS_TAC) THEN
BINOP_TAC THENL [REAL_ARITH_TAC; VECTOR_ARITH_TAC]);;
let CONVEX_HULL_3_ALT = prove
(`!a b c.
convex hull {a,b,c} =
{a + u % (b - a) + v % (c - a) |
&0 <= u /\ &0 <= v /\ u + v <= &1}`,
ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {b,c,a}`] THEN
REWRITE_TAC[
CONVEX_HULL_3;
EXTENSION;
IN_ELIM_THM] THEN
REWRITE_TAC[REAL_ADD_ASSOC;
CONJ_ASSOC] THEN
REWRITE_TAC[TAUT `(a /\ x + y = &1) /\ b <=> x + y = &1 /\ a /\ b`] THEN
REWRITE_TAC[REAL_ARITH `x + y = &1 <=> y = &1 - x`;
UNWIND_THM2] THEN
REPEAT GEN_TAC THEN REPEAT(AP_TERM_TAC THEN ABS_TAC) THEN
BINOP_TAC THENL [REAL_ARITH_TAC; VECTOR_ARITH_TAC]);;
let AFFINE_HULL_PCROSS,CONVEX_HULL_PCROSS = (CONJ_PAIR o prove)
(`(!s:real^M->bool t:real^N->bool.
affine hull (s PCROSS t) =
(affine hull s) PCROSS (affine hull t)) /\
(!s:real^M->bool t:real^N->bool.
convex hull (s PCROSS t) =
(convex hull s) PCROSS (convex hull t))`,
(* ------------------------------------------------------------------------- *)
(* Relations among closure notions and corresponding hulls. *)
(* ------------------------------------------------------------------------- *)
let AFFINE_EQ_SUBSPACE = prove
(`!s:real^N->bool.
vec 0
IN s ==> (
affine s <=>
subspace s)`,
REPEAT STRIP_TAC THEN EQ_TAC THEN ASM_SIMP_TAC[
subspace;
affine] THEN
DISCH_TAC THEN MATCH_MP_TAC(TAUT `b /\ (b ==> a) ==> a /\ b`) THEN
CONJ_TAC THENL
[MAP_EVERY X_GEN_TAC [`c:real`; `x:real^N`] THEN STRIP_TAC THEN
SUBST1_TAC(VECTOR_ARITH `c % x:real^N = c % x + (&1 - c) %
vec 0`) THEN
FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC;
DISCH_TAC THEN MAP_EVERY X_GEN_TAC [`x:real^N`; `y:real^N`] THEN
STRIP_TAC THEN SUBST1_TAC(VECTOR_ARITH
`x + y:real^N = &2 % (&1 / &2 % x + &1 / &2 % y)`) THEN
FIRST_X_ASSUM MATCH_MP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC]);;
(* ------------------------------------------------------------------------- *)
(* Nonempty affine sets are translates of (unique) subspaces. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* If we take a slice out of a set, we can do it perpendicularly, *)
(* with the normal vector to the slice parallel to the affine hull. *)
(* ------------------------------------------------------------------------- *)
"a'"; "b'"; "w"] THEN
REPEAT STRIP_TAC THEN FIRST_X_ASSUM(SUBST1_TAC o SYM) THEN
REWRITE_TAC[VECTOR_ADD_RID; FORALL_IN_IMAGE] THEN
REWRITE_TAC[DOT_RADD; REAL_ARITH `a + x <= a <=> x <= &0`] THEN
SUBGOAL_THEN `subspace(s:real^N->bool) /\ span s = s`
STRIP_ASSUME_TAC THENL
[ASM_MESON_TAC[AFFINE_IMP_SUBSPACE; SPAN_EQ_SELF]; ALL_TAC] THEN
MP_TAC(ISPECL [`s:real^N->bool`; `a:real^N`]
ORTHOGONAL_SUBSPACE_DECOMP_EXISTS) THEN
ASM_REWRITE_TAC[LEFT_IMP_EXISTS_THM; orthogonal] THEN
MAP_EVERY X_GEN_TAC [`a':real^N`; `a'':real^N`] THEN
ASM_CASES_TAC `a':real^N = vec 0` THENL
[ASM_REWRITE_TAC[VECTOR_ADD_LID] THEN
ASM_CASES_TAC `a'':real^N = a` THEN ASM_REWRITE_TAC[] THEN
SIMP_TAC[SUBSET; IN_ELIM_THM; REAL_LE_REFL];
ALL_TAC] THEN
STRIP_TAC THEN REPEAT DISJ2_TAC THEN
EXISTS_TAC `a':real^N` THEN ASM_REWRITE_TAC[] THEN
EXISTS_TAC `(a':real^N) dot z` THEN
REPEAT(CONJ_TAC THENL
[MATCH_MP_TAC(SET_RULE
`(!x. x IN s ==> (p x <=> q x))
==> s INTER {x | p x} = s INTER {x | q x}`) THEN
ASM_SIMP_TAC[DOT_LADD] THEN REAL_ARITH_TAC;
ALL_TAC]) THEN
X_GEN_TAC `x:real^N` THEN DISCH_TAC THEN REWRITE_TAC[IN_IMAGE] THEN
EXISTS_TAC `x + a':real^N` THEN
ASM_SIMP_TAC[SUBSPACE_ADD; VECTOR_ADD_ASSOC]]);;
(* ------------------------------------------------------------------------- *)
(* Affine dimension. *)
(* ------------------------------------------------------------------------- *)
add_translation_invariants [AFF_DIM_TRANSLATION_EQ];;
add_linear_invariants [AFF_DIM_INJECTIVE_LINEAR_IMAGE];;
let AFF_DIM_EQ_0 = prove
(`!s:real^N->bool.
aff_dim s = &0 <=> ?a. s = {a}`,
GEN_TAC THEN EQ_TAC THEN SIMP_TAC[
AFF_DIM_SING;
LEFT_IMP_EXISTS_THM] THEN
ASM_CASES_TAC `s:real^N->bool = {}` THEN ASM_REWRITE_TAC[
AFF_DIM_EMPTY] THEN
CONV_TAC INT_REDUCE_CONV THEN DISCH_TAC THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM
MEMBER_NOT_EMPTY]) THEN
MATCH_MP_TAC
MONO_EXISTS THEN X_GEN_TAC `a:real^N` THEN
MATCH_MP_TAC(SET_RULE
`(!b. ~(b = a) /\ {a,b}
SUBSET s ==> F) ==> a
IN s ==> s = {a}`) THEN
X_GEN_TAC `b:real^N` THEN STRIP_TAC THEN
FIRST_ASSUM(MP_TAC o MATCH_MP
AFF_DIM_SUBSET) THEN
MP_TAC(ISPECL [`a:real^N`; `b:real^N`]
AFF_DIM_2) THEN
ASM_SIMP_TAC[] THEN INT_ARITH_TAC);;
(* ------------------------------------------------------------------------- *)
(* Existence of a rigid transform between congruent sets. *)
(* ------------------------------------------------------------------------- *)
"Y"] THEN
SIMP_TAC[CART_EQ; column; LAMBDA_BETA; dot] THEN
REWRITE_TAC[GSYM VECTOR_SUB_COMPONENT; GSYM dot] THEN
REWRITE_TAC[DOT_NORM_SUB; VECTOR_ARITH
`(x - a) - (y - a):real^N = x - y`] THEN
ASM_SIMP_TAC[GSYM dist; DIMINDEX_GE_1; LE_REFL];
ALL_TAC] THEN
SUBGOAL_THEN
`?M:real^N^N. orthogonal_matrix M /\ (Y:real^M^N) = M ** (X:real^M^N)`
(CHOOSE_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THENL
[ALL_TAC;
GEN_REWRITE_TAC (LAND_CONV o TOP_DEPTH_CONV) [CART_EQ] THEN
MAP_EVERY EXPAND_TAC ["X"; "Y"] THEN
SIMP_TAC[LAMBDA_BETA; matrix_mul] THEN
REWRITE_TAC[REAL_ARITH `x - y:real = z <=> x = y + z`] THEN STRIP_TAC THEN
EXISTS_TAC `(y:real^N^M)$1 - (M:real^N^N) ** (x:real^N^M)$1` THEN
EXISTS_TAC `\x:real^N. (M:real^N^N) ** x` THEN
ASM_SIMP_TAC[ORTHOGONAL_TRANSFORMATION_MATRIX;
MATRIX_OF_MATRIX_VECTOR_MUL; MATRIX_VECTOR_MUL_LINEAR] THEN
SIMP_TAC[CART_EQ; matrix_vector_mul; LAMBDA_BETA;
VECTOR_ADD_COMPONENT] THEN
ASM_SIMP_TAC[REAL_SUB_LDISTRIB; SUM_SUB_NUMSEG] THEN
REWRITE_TAC[VECTOR_SUB_COMPONENT; REAL_ARITH
`a + y - b:real = a - z + y <=> z = b`] THEN
SIMP_TAC[LAMBDA_BETA]] THEN
MP_TAC(ISPEC `transp(X:real^M^N) ** X`
SYMMETRIC_MATRIX_DIAGONALIZABLE_EXPLICIT) THEN
REWRITE_TAC[MATRIX_TRANSP_MUL; TRANSP_TRANSP; LEFT_IMP_EXISTS_THM] THEN
MAP_EVERY X_GEN_TAC [`P:real^M^M`; `d:num->real`] THEN
DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
DISCH_THEN(fun th -> MP_TAC th THEN ASM_REWRITE_TAC[] THEN MP_TAC th) THEN
REWRITE_TAC[MATRIX_MUL_ASSOC; GSYM MATRIX_TRANSP_MUL] THEN
REWRITE_TAC[GSYM MATRIX_MUL_ASSOC; LEFT_IMP_EXISTS_THM] THEN
REWRITE_TAC[IMP_IMP] THEN
GEN_REWRITE_TAC (LAND_CONV o TOP_DEPTH_CONV) [CART_EQ] THEN
SIMP_TAC[MATRIX_MUL_LTRANSP_DOT_COLUMN; LAMBDA_BETA] THEN STRIP_TAC THEN
MP_TAC(ISPECL [`\i. column i ((X:real^M^N) ** (P:real^M^M))`;
`\i. column i ((Y:real^M^N) ** (P:real^M^M))`;
`1..dimindex(:M)`]
ORTHOGONAL_TRANSFORMATION_BETWEEN_ORTHOGONAL_SETS) THEN
REWRITE_TAC[IN_NUMSEG] THEN ANTS_TAC THENL
[ASM_SIMP_TAC[pairwise; IN_NUMSEG; NORM_EQ; orthogonal]; ALL_TAC] THEN
DISCH_THEN(X_CHOOSE_THEN `f:real^N->real^N` (STRIP_ASSUME_TAC o GSYM)) THEN
EXISTS_TAC `matrix(f:real^N->real^N)` THEN CONJ_TAC THENL
[ASM_MESON_TAC[ORTHOGONAL_TRANSFORMATION_MATRIX]; ALL_TAC] THEN
SUBGOAL_THEN
`!M:real^M^N. M = M ** (P:real^M^M) ** transp P`
(fun th -> GEN_REWRITE_TAC BINOP_CONV [th])
THENL
[ASM_MESON_TAC[orthogonal_matrix; MATRIX_MUL_RID];
REWRITE_TAC[MATRIX_MUL_ASSOC] THEN AP_THM_TAC THEN AP_TERM_TAC] THEN
REWRITE_TAC[GSYM MATRIX_MUL_ASSOC] THEN
ASM_SIMP_TAC[MATRIX_EQUAL_COLUMNS] THEN
X_GEN_TAC `i:num` THEN STRIP_TAC THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [orthogonal_transformation]) THEN
DISCH_THEN(ASSUME_TAC o GSYM o MATCH_MP MATRIX_WORKS o CONJUNCT1) THEN
ASM_REWRITE_TAC[] THEN
SIMP_TAC[CART_EQ; matrix_vector_mul; column; LAMBDA_BETA] THEN
X_GEN_TAC `j:num` THEN STRIP_TAC THEN
GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [matrix_mul] THEN
ASM_SIMP_TAC[LAMBDA_BETA]) in
REPEAT GEN_TAC THEN ASM_CASES_TAC `s:A->bool = {}` THENL
[REPEAT STRIP_TAC THEN
MAP_EVERY EXISTS_TAC [`vec 0:real^N`; `\x:real^N. x`] THEN
ASM_REWRITE_TAC[NOT_IN_EMPTY; ORTHOGONAL_TRANSFORMATION_ID];
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM MEMBER_NOT_EMPTY]) THEN
DISCH_THEN(X_CHOOSE_TAC `m:A`) THEN DISCH_TAC] THEN
SUBGOAL_THEN
`?r. IMAGE r (1..dimindex(:(N,1)finite_sum)) SUBSET s /\
affine hull (IMAGE (y o r) (1..dimindex(:(N,1)finite_sum))) =
affine hull (IMAGE (y:A->real^N) s)`
MP_TAC THENL
[REWRITE_TAC[GSYM SUBSET_ANTISYM_EQ] THEN
SIMP_TAC[IMAGE_o; TAUT `p /\ q <=> ~(p ==> ~q)`;
HULL_MONO; IMAGE_SUBSET] THEN REWRITE_TAC[NOT_IMP] THEN
MP_TAC(ISPEC `IMAGE (y:A->real^N) s` AFFINE_BASIS_EXISTS) THEN
DISCH_THEN(X_CHOOSE_THEN `b:real^N->bool` STRIP_ASSUME_TAC) THEN
FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [AFFINE_INDEPENDENT_IFF_CARD]) THEN
STRIP_TAC THEN
FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [FINITE_INDEX_NUMSEG]) THEN
DISCH_THEN(X_CHOOSE_THEN `f:num->real^N` STRIP_ASSUME_TAC) THEN
SUBGOAL_THEN `CARD(b:real^N->bool) <= dimindex(:(N,1)finite_sum)`
ASSUME_TAC THENL
[REWRITE_TAC[GSYM INT_OF_NUM_LE] THEN
FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (INT_ARITH
`a:int = c - &1 ==> a + &1 <= n ==> c <= n`)) THEN
REWRITE_TAC[DIMINDEX_FINITE_SUM; DIMINDEX_1; GSYM INT_OF_NUM_ADD] THEN
REWRITE_TAC[INT_LE_RADD; AFF_DIM_LE_UNIV];
ALL_TAC] THEN
UNDISCH_TAC `b SUBSET IMAGE (y:A->real^N) s` THEN
ONCE_ASM_REWRITE_TAC[] THEN REWRITE_TAC[SUBSET; FORALL_IN_IMAGE] THEN
REWRITE_TAC[IN_IMAGE] THEN
GEN_REWRITE_TAC (LAND_CONV o DEPTH_CONV) [RIGHT_IMP_EXISTS_THM] THEN
REWRITE_TAC[SKOLEM_THM; IN_NUMSEG] THEN
DISCH_THEN(X_CHOOSE_THEN `r:num->A` STRIP_ASSUME_TAC) THEN
EXISTS_TAC `\i. if i <= CARD(b:real^N->bool) then r i else (m:A)` THEN
CONJ_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
UNDISCH_THEN `affine hull b:real^N->bool = affine hull IMAGE y (s:A->bool)`
(SUBST1_TAC o SYM) THEN
REWRITE_TAC[GSYM SUBSET] THEN MATCH_MP_TAC HULL_MONO THEN
ONCE_ASM_REWRITE_TAC[] THEN
REWRITE_TAC[SUBSET; FORALL_IN_IMAGE; IN_NUMSEG] THEN
X_GEN_TAC `i:num` THEN STRIP_TAC THEN REWRITE_TAC[GSYM IMAGE_o] THEN
REWRITE_TAC[IN_IMAGE; IN_NUMSEG] THEN EXISTS_TAC `i:num` THEN
ASM_REWRITE_TAC[o_THM] THEN ASM_MESON_TAC[LE_TRANS];
REWRITE_TAC[SUBSET; IN_NUMSEG; FORALL_IN_IMAGE] THEN
STRIP_TAC THEN MP_TAC(ISPECL
[`(lambda i. x(r i:A)):real^N^(N,1)finite_sum`;
`(lambda i. y(r i:A)):real^N^(N,1)finite_sum`] lemma) THEN
ASM_SIMP_TAC[LAMBDA_BETA] THEN
MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `a:real^N` THEN
MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `f:real^N->real^N` THEN
STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
X_GEN_TAC `k:A` THEN STRIP_TAC THEN
SUBGOAL_THEN
`!z. z IN
affine hull IMAGE (y o (r:num->A)) (1..dimindex(:(N,1)finite_sum))
==> dist(z,y k) = dist(z,a + (f:real^N->real^N)(x k))`
MP_TAC THENL
[MATCH_MP_TAC SAME_DISTANCES_TO_AFFINE_HULL THEN
REWRITE_TAC[FORALL_IN_IMAGE; o_THM; IN_NUMSEG] THEN
X_GEN_TAC `j:num` THEN STRIP_TAC THEN MATCH_MP_TAC EQ_TRANS THEN
EXISTS_TAC `dist(x(r(j:num)),(x:A->real^N) k)` THEN CONJ_TAC THENL
[CONV_TAC SYM_CONV THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_SIMP_TAC[];
REWRITE_TAC[dist] THEN ASM_SIMP_TAC[NORM_ARITH
`(a + x) - (a + y):real^N = x - y`] THEN
ASM_MESON_TAC[ORTHOGONAL_TRANSFORMATION; LINEAR_SUB]];
ASM_SIMP_TAC[NORM_ARITH
`a:real^N = b <=> dist(a:real^N,a) = dist(a,b)`] THEN
DISCH_THEN MATCH_MP_TAC THEN MATCH_MP_TAC HULL_INC THEN
REWRITE_TAC[IN_IMAGE; IN_NUMSEG] THEN ASM_MESON_TAC[]]]);;
(* ------------------------------------------------------------------------- *)
(* Caratheodory's theorem. *)
(* ------------------------------------------------------------------------- *)
let CONVEX_HULL_CARATHEODORY_AFF_DIM = prove
(`!p.
convex hull p =
{y:real^N | ?s u. FINITE s /\ s
SUBSET p /\
&(
CARD s) <=
aff_dim p + &1 /\
(!x. x
IN s ==> &0 <= u x) /\
sum s u = &1 /\
vsum s (\v. u v % v) = y}`,
GEN_TAC THEN REWRITE_TAC[
CONVEX_HULL_EXPLICIT] THEN
REWRITE_TAC[
EXTENSION;
IN_ELIM_THM] THEN X_GEN_TAC `y:real^N` THEN
EQ_TAC THENL [ALL_TAC; MESON_TAC[]] THEN
MATCH_MP_TAC(TAUT `!q. (p ==> q) /\ (q ==> r) ==> (p ==> r)`) THEN
EXISTS_TAC `?n s u.
CARD s = n /\
FINITE s /\ s
SUBSET p /\
(!x. x
IN s ==> &0 <= u x) /\
sum s u = &1 /\
vsum s (\v. u v % v) = (y:real^N)` THEN
CONJ_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
GEN_REWRITE_TAC LAND_CONV [
num_WOP] THEN
DISCH_THEN(X_CHOOSE_THEN `n:num` MP_TAC) THEN
DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
REPEAT(MATCH_MP_TAC
MONO_EXISTS THEN GEN_TAC) THEN
STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
GEN_REWRITE_TAC I [GSYM
INT_NOT_LT] THEN DISCH_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPEC `n - 1`) THEN REWRITE_TAC[NOT_IMP] THEN
CONJ_TAC THENL
[MATCH_MP_TAC(ARITH_RULE `~(n = 0) ==> n - 1 < n`) THEN
DISCH_THEN SUBST_ALL_TAC THEN
UNDISCH_TAC `
aff_dim(p:real^N->bool) + &1 < &0` THEN
REWRITE_TAC[INT_ARITH `p + &1:int < &0 <=> ~(-- &1 <= p)`] THEN
REWRITE_TAC[
AFF_DIM_GE];
ALL_TAC] THEN
MP_TAC(ISPEC `s:real^N->bool`
AFF_DIM_AFFINE_INDEPENDENT) THEN
ASM_REWRITE_TAC[] THEN
SUBGOAL_THEN `~(
aff_dim(s:real^N->bool) = &n - &1)` ASSUME_TAC THENL
[FIRST_ASSUM(MP_TAC o MATCH_MP
AFF_DIM_SUBSET) THEN
UNDISCH_TAC `
aff_dim(p:real^N->bool) + &1 < &n` THEN
INT_ARITH_TAC;
ALL_TAC] THEN
ASM_SIMP_TAC[
AFFINE_DEPENDENT_EXPLICIT_FINITE] THEN
DISCH_THEN(X_CHOOSE_THEN `w:real^N->
real` STRIP_ASSUME_TAC) THEN
SUBGOAL_THEN
`?t. (!v:real^N. v
IN s ==> u(v) + t * w(v) >= &0) /\
?a. a
IN s /\ u(a) + t * w(a) = &0`
STRIP_ASSUME_TAC THENL
[ABBREV_TAC
`i =
IMAGE (\v. u(v) / --w(v)) {v:real^N | v
IN s /\ w v < &0}` THEN
EXISTS_TAC `
inf i` THEN MP_TAC(SPEC `i:real->bool`
INF_FINITE) THEN
ANTS_TAC THENL
[EXPAND_TAC "i" THEN
ASM_SIMP_TAC[
FINITE_IMAGE;
FINITE_RESTRICT;
IMAGE_EQ_EMPTY] THEN
REWRITE_TAC[GSYM
MEMBER_NOT_EMPTY;
IN_ELIM_THM] THEN
MP_TAC(ISPECL [`w:real^N->
real`; `s:real^N->bool`]
SUM_ZERO_EXISTS) THEN
ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[];
ALL_TAC] THEN
ABBREV_TAC `t =
inf i` THEN
EXPAND_TAC "i" THEN REWRITE_TAC[
FORALL_IN_IMAGE] THEN
REWRITE_TAC[
IN_IMAGE;
IN_ELIM_THM] THEN
DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_THEN `a:real^N`
STRIP_ASSUME_TAC) MP_TAC) THEN
SIMP_TAC[
REAL_LE_RDIV_EQ; REAL_ARITH `x < &0 ==> &0 < --x`;
real_ge] THEN
REWRITE_TAC[REAL_ARITH `t * --w <= u <=> &0 <= u + t * w`] THEN
STRIP_TAC THEN CONJ_TAC THENL
[X_GEN_TAC `x:real^N` THEN DISCH_TAC THEN
DISJ_CASES_TAC(REAL_ARITH `(w:real^N->
real) x < &0 \/ &0 <= w x`) THEN
ASM_SIMP_TAC[] THEN MATCH_MP_TAC
REAL_LE_ADD THEN ASM_SIMP_TAC[] THEN
MATCH_MP_TAC
REAL_LE_MUL THEN ASM_REWRITE_TAC[] THEN
MATCH_MP_TAC
REAL_LE_DIV THEN ASM_SIMP_TAC[] THEN
MATCH_MP_TAC(REAL_ARITH `w < &0 ==> &0 <= --w`) THEN ASM_REWRITE_TAC[];
EXISTS_TAC `a:real^N` THEN ASM_REWRITE_TAC[] THEN
UNDISCH_TAC `w(a:real^N) < &0` THEN CONV_TAC REAL_FIELD];
ALL_TAC] THEN
MAP_EVERY EXISTS_TAC
[`s
DELETE (a:real^N)`; `(\v. u(v) + t * w(v)):real^N->
real`] THEN
ASM_SIMP_TAC[
SUM_DELETE;
VSUM_DELETE;
CARD_DELETE;
FINITE_DELETE] THEN
ASM_SIMP_TAC[
SUM_ADD;
VECTOR_ADD_RDISTRIB;
VSUM_ADD] THEN
ASM_SIMP_TAC[GSYM
VECTOR_MUL_ASSOC;
SUM_LMUL;
VSUM_LMUL] THEN
REPEAT CONJ_TAC THENL
[ASM SET_TAC[]; ASM SET_TAC[
real_ge]; REAL_ARITH_TAC; VECTOR_ARITH_TAC]);;
(* ------------------------------------------------------------------------- *)
(* Some results on decomposing convex hulls, e.g. simplicial subdivision. *)
(* ------------------------------------------------------------------------- *)
let AFFINE_HULL_INTER,CONVEX_HULL_INTER = (CONJ_PAIR o prove)
(`(!s t:real^N->bool.
~(affine_dependent(s UNION t))
==> affine hull s INTER affine hull t = affine hull (s INTER t)) /\
(!s t:real^N->bool.
~(affine_dependent (s UNION t))
==> convex hull s INTER convex hull t = convex hull (s INTER t))`,
CONJ_TAC THEN
(REPEAT STRIP_TAC THEN
FIRST_ASSUM(MP_TAC o MATCH_MP AFFINE_INDEPENDENT_IMP_FINITE) THEN
REWRITE_TAC[FINITE_UNION] THEN STRIP_TAC THEN
MATCH_MP_TAC SUBSET_ANTISYM THEN REWRITE_TAC[SUBSET_INTER] THEN
SIMP_TAC[HULL_MONO; INTER_SUBSET] THEN
REWRITE_TAC[SUBSET; AFFINE_HULL_FINITE; CONVEX_HULL_FINITE;
IN_ELIM_THM; IN_INTER] THEN
X_GEN_TAC `y:real^N` THEN DISCH_THEN(CONJUNCTS_THEN2
(X_CHOOSE_THEN `u:real^N->real` STRIP_ASSUME_TAC)
(X_CHOOSE_THEN `v:real^N->real` STRIP_ASSUME_TAC)) THEN
FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE RAND_CONV
[AFFINE_DEPENDENT_EXPLICIT]) THEN
REWRITE_TAC[NOT_EXISTS_THM] THEN
DISCH_THEN(MP_TAC o SPEC `(s UNION t):real^N->bool`) THEN
ASM_REWRITE_TAC[SUBSET_REFL] THEN
DISCH_THEN(MP_TAC o SPEC
`\x:real^N. (if x IN s then u x else &0) -
(if x IN t then v x else &0)`) THEN
ASM_SIMP_TAC[SUM_SUB; FINITE_UNION; VSUM_SUB; VECTOR_SUB_RDISTRIB] THEN
REWRITE_TAC[MESON[]
`(if p then a else b) % x = (if p then a % x else b % x)`] THEN
ASM_SIMP_TAC[SUM_CASES; VSUM_CASES; VECTOR_MUL_LZERO; FINITE_UNION] THEN
ASM_REWRITE_TAC[SUM_0; VSUM_0;
SET_RULE `{x | x IN (s UNION t) /\ x IN s} = s`;
SET_RULE `{x | x IN (s UNION t) /\ x IN t} = t`] THEN
MATCH_MP_TAC(TAUT `a /\ c /\ (~b ==> d) ==> ~(a /\ b /\ c) ==> d`) THEN
REPEAT CONJ_TAC THENL [REAL_ARITH_TAC; VECTOR_ARITH_TAC; ALL_TAC] THEN
DISCH_TAC THEN EXISTS_TAC `u:real^N->real` THEN ASM_SIMP_TAC[] THEN
CONJ_TAC THEN MATCH_MP_TAC EQ_TRANS THENL
[EXISTS_TAC `sum s (u:real^N->real)`;
EXISTS_TAC `vsum s (\x. (u:real^N->real) x % x)`] THEN
(CONJ_TAC THENL [ALL_TAC; FIRST_X_ASSUM ACCEPT_TAC]) THEN
CONV_TAC SYM_CONV THENL
[MATCH_MP_TAC SUM_EQ_SUPERSET; MATCH_MP_TAC VSUM_EQ_SUPERSET] THEN
ASM_SIMP_TAC[FINITE_INTER; INTER_SUBSET; IN_INTER] THEN
X_GEN_TAC `x:real^N` THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
ASM_REWRITE_TAC[VECTOR_MUL_EQ_0] THEN DISCH_TAC THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [NOT_EXISTS_THM]) THEN
DISCH_THEN(MP_TAC o SPEC `x:real^N`) THEN
ASM_REWRITE_TAC[REAL_SUB_RZERO] THEN ASM SET_TAC[]));;
(* ------------------------------------------------------------------------- *)
(* Representing affine hull as hyperplane or finite intersection of them. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* An additional lemma about hyperplanes. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Openness and compactness are preserved by convex hull operation. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Extremal points of a simplex are some vertices. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Closest point of a convex set is unique, with a continuous projection. *)
(* ------------------------------------------------------------------------- *)
let ANY_CLOSEST_POINT_DOT = prove
(`!s a x y:real^N.
convex s /\
closed s /\ x
IN s /\ y
IN s /\
(!z. z
IN s ==>
dist(a,x) <=
dist(a,z))
==> (a - x)
dot (y - x) <= &0`,
REPEAT STRIP_TAC THEN REWRITE_TAC[REAL_ARITH `x <= &0 <=> ~(x > &0)`] THEN
DISCH_THEN(MP_TAC o MATCH_MP
CLOSER_POINT_LEMMA) THEN
DISCH_THEN(X_CHOOSE_THEN `u:real` (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
REWRITE_TAC[
REAL_NOT_LT] THEN ONCE_REWRITE_TAC[
DIST_SYM] THEN
FIRST_X_ASSUM MATCH_MP_TAC THEN
REWRITE_TAC[VECTOR_ARITH `x + u % (y - x) = (&1 - u) % x + u % y`] THEN
MATCH_MP_TAC
IN_CONVEX_SET THEN ASM_SIMP_TAC[
REAL_LT_IMP_LE]);;
(* ------------------------------------------------------------------------- *)
(* Relating closest points and orthogonality. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Various point-to-set separating/supporting hyperplane theorems. *)
(* ------------------------------------------------------------------------- *)
let SUPPORTING_HYPERPLANE_CLOSED_POINT = prove
(`!s z:real^N.
convex s /\
closed s /\ ~(s = {}) /\ ~(z
IN s)
==> ?a b y. a
dot z < b /\ y
IN s /\ (a
dot y = b) /\
(!x. x
IN s ==> a
dot x >= b)`,
REPEAT STRIP_TAC THEN
MP_TAC(ISPECL [`s:real^N->bool`; `z:real^N`]
DISTANCE_ATTAINS_INF) THEN
ASM_REWRITE_TAC[] THEN
DISCH_THEN(X_CHOOSE_THEN `y:real^N` STRIP_ASSUME_TAC) THEN
EXISTS_TAC `y - z:real^N` THEN EXISTS_TAC `(y - z:real^N)
dot y` THEN
EXISTS_TAC `y:real^N` THEN ONCE_REWRITE_TAC[GSYM
REAL_SUB_LT] THEN
ASM_REWRITE_TAC[GSYM
DOT_RSUB;
DOT_POS_LT;
VECTOR_SUB_EQ] THEN
CONJ_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN X_GEN_TAC `x:real^N` THEN
DISCH_TAC THEN SUBGOAL_THEN
`!u. &0 <= u /\ u <= &1 ==>
dist(z:real^N,y) <=
dist(z,(&1 - u) % y + u % x)`
MP_TAC THENL [ASM_MESON_TAC[
CONVEX_ALT]; ALL_TAC] THEN
ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN ONCE_REWRITE_TAC[
DIST_SYM] THEN
REWRITE_TAC[
real_ge;
REAL_NOT_LE;
NOT_FORALL_THM; NOT_IMP] THEN
GEN_REWRITE_TAC LAND_CONV [REAL_ARITH `x < y <=> y - x > &0`] THEN
REWRITE_TAC[VECTOR_ARITH
`(a - b)
dot x - (a - b)
dot y = (b - a)
dot (y - x)`] THEN
DISCH_THEN(MP_TAC o MATCH_MP
CLOSER_POINT_LEMMA) THEN
REWRITE_TAC[VECTOR_ARITH `y + u % (x - y) = (&1 - u) % y + u % x`] THEN
MESON_TAC[
REAL_LT_IMP_LE]);;
(* ------------------------------------------------------------------------- *)
(* Now set-to-set for closed/compact sets. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* General case without assuming closure and getting non-strict separation. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* More convexity generalities. *)
(* ------------------------------------------------------------------------- *)
let CONVEX_CLOSURE = prove
(`!s:real^N->bool.
convex s ==>
convex(
closure s)`,
REWRITE_TAC[
convex;
CLOSURE_SEQUENTIAL] THEN
GEN_TAC THEN DISCH_TAC THEN
MAP_EVERY X_GEN_TAC [`x:real^N`; `y:real^N`; `u:real`; `v:real`] THEN
DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_TAC `a:num->real^N`) MP_TAC) THEN
DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_TAC `b:num->real^N`) MP_TAC) THEN
STRIP_TAC THEN EXISTS_TAC `\n:num. u % a(n) + v % b(n) :real^N` THEN
ASM_SIMP_TAC[
LIM_ADD;
LIM_CMUL]);;
let CONVEX_INTERIOR = prove
(`!s:real^N->bool.
convex s ==>
convex(
interior s)`,
REWRITE_TAC[
CONVEX_ALT;
IN_INTERIOR;
SUBSET;
IN_BALL;
dist] THEN
REPEAT GEN_TAC THEN STRIP_TAC THEN REPEAT GEN_TAC THEN
DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_TAC `d:real`) MP_TAC) THEN
DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_TAC `e:real`) STRIP_ASSUME_TAC) THEN
EXISTS_TAC `min d e` THEN ASM_REWRITE_TAC[
REAL_LT_MIN] THEN
X_GEN_TAC `z:real^N` THEN STRIP_TAC THEN
SUBST1_TAC(VECTOR_ARITH `z:real^N =
(&1 - u) % (z - u % (y - x)) + u % (z + (&1 - u) % (y - x))`) THEN
FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN
ASM_MESON_TAC[VECTOR_ARITH `x - (z - u % (y - x)) =
((&1 - u) % x + u % y) - z:real^N`;
VECTOR_ARITH `y - (z + (&1 - u) % (y - x)) =
((&1 - u) % x + u % y) - z:real^N`]);;
(* ------------------------------------------------------------------------- *)
(* Moving and scaling convex hulls. *)
(* ------------------------------------------------------------------------- *)
add_translation_invariants [CONVEX_HULL_TRANSLATION];;
(* ------------------------------------------------------------------------- *)
(* Convex set as intersection of halfspaces. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Radon's theorem (from Lars Schewe). *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Helly's theorem. *)
(* ------------------------------------------------------------------------- *)
let HELLY_INDUCT = prove
(`!n f. f
HAS_SIZE n /\ n >=
dimindex(:N) + 1 /\
(!s:real^N->bool. s
IN f ==>
convex s) /\
(!t. t
SUBSET f /\
CARD(t) =
dimindex(:N) + 1
==> ~(
INTERS t = {}))
==> ~(
INTERS f = {})`,
INDUCT_TAC THEN REWRITE_TAC[ARITH_RULE `~(0 >= n + 1)`] THEN GEN_TAC THEN
POP_ASSUM(LABEL_TAC "*") THEN STRIP_TAC THEN
FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [
HAS_SIZE_SUC]) THEN
STRIP_TAC THEN RULE_ASSUM_TAC(REWRITE_RULE[
HAS_SIZE]) THEN
FIRST_X_ASSUM(DISJ_CASES_TAC o MATCH_MP (ARITH_RULE
`SUC n >= m + 1 ==> m = n \/ n >= m + 1`))
THENL
[FIRST_X_ASSUM MATCH_MP_TAC THEN RULE_ASSUM_TAC(REWRITE_RULE[
HAS_SIZE]) THEN
ASM_SIMP_TAC[
CARD_CLAUSES;
SUBSET_REFL] THEN ARITH_TAC;
ALL_TAC] THEN
SUBGOAL_THEN
`?X. !s:real^N->bool. s
IN f ==> X(s)
IN INTERS (f
DELETE s)`
STRIP_ASSUME_TAC THENL
[REWRITE_TAC[GSYM
SKOLEM_THM;
MEMBER_NOT_EMPTY;
RIGHT_EXISTS_IMP_THM] THEN
GEN_TAC THEN STRIP_TAC THEN REMOVE_THEN "*" MATCH_MP_TAC THEN
ASM_SIMP_TAC[
FINITE_DELETE;
CARD_DELETE] THEN ASM SET_TAC[];
ALL_TAC] THEN
ASM_CASES_TAC
`?s t:real^N->bool. s
IN f /\ t
IN f /\ ~(s = t) /\ X s:real^N = X t`
THENL
[FIRST_X_ASSUM(CHOOSE_THEN STRIP_ASSUME_TAC) THEN
REWRITE_TAC[GSYM
MEMBER_NOT_EMPTY] THEN
EXISTS_TAC `(X:(real^N->bool)->real^N) t` THEN
FIRST_X_ASSUM(fun
th -> GEN_REWRITE_TAC ONCE_DEPTH_CONV
[MATCH_MP
(SET_RULE`~(s = t)
==>
INTERS f =
INTERS(f
DELETE s)
INTER INTERS(f
DELETE t)`)
th]) THEN
REWRITE_TAC[
IN_INTER] THEN ASM_MESON_TAC[];
ALL_TAC] THEN
MP_TAC(ISPEC `
IMAGE (X:(real^N->bool)->real^N) f`
RADON_PARTITION) THEN
ANTS_TAC THENL
[ASM_SIMP_TAC[
FINITE_IMAGE] THEN
MATCH_MP_TAC
AFFINE_DEPENDENT_BIGGERSET THEN
ASM_SIMP_TAC[
FINITE_IMAGE] THEN
MATCH_MP_TAC(ARITH_RULE
`!f n. n >= d + 1 /\ f = SUC n /\ c = f ==> c >= d + 2`) THEN
MAP_EVERY EXISTS_TAC [`
CARD(f:(real^N->bool)->bool)`; `n:num`] THEN
REPEAT(CONJ_TAC THENL [ASM_MESON_TAC[]; ALL_TAC]) THEN
MATCH_MP_TAC
CARD_IMAGE_INJ THEN ASM_MESON_TAC[];
ALL_TAC] THEN
ONCE_REWRITE_TAC[SET_RULE
`P /\ m
UNION p = s /\ Q <=>
m
SUBSET s /\ p
SUBSET s /\ m
UNION p = s /\ P /\ Q`] THEN
REWRITE_TAC[
SUBSET_IMAGE;
DISJOINT] THEN
REWRITE_TAC[MESON[]
`(?m p. (?u. P u /\ m = t u) /\ (?u. P u /\ p = t u) /\ Q m p) ==> r <=>
(!u v. P u /\ P v /\ Q (t u) (t v) ==> r)`] THEN
MAP_EVERY X_GEN_TAC [`g:(real^N->bool)->bool`; `h:(real^N->bool)->bool`] THEN
REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
SUBGOAL_THEN `(f:(real^N->bool)->bool) = h
UNION g` SUBST1_TAC THENL
[MATCH_MP_TAC
SUBSET_ANTISYM THEN ASM_REWRITE_TAC[
UNION_SUBSET] THEN
REWRITE_TAC[
SUBSET;
IN_UNION] THEN X_GEN_TAC `s:real^N->bool` THEN
DISCH_THEN(fun
th -> ASSUME_TAC
th THEN MP_TAC
th) THEN
DISCH_THEN(MP_TAC o ISPEC `X:(real^N->bool)->real^N` o
MATCH_MP
FUN_IN_IMAGE) THEN
FIRST_X_ASSUM(fun
th ->
GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [GSYM
th]) THEN
ONCE_REWRITE_TAC[
DISJ_SYM] THEN REWRITE_TAC[
IN_UNION;
IN_IMAGE] THEN
MATCH_MP_TAC MONO_OR THEN ASM_MESON_TAC[
SUBSET];
ALL_TAC] THEN
MATCH_MP_TAC(SET_RULE
`g
SUBSET INTERS g' /\ h
SUBSET INTERS h'
==> ~(g
INTER h = {}) ==> ~(
INTERS(g'
UNION h') = {})`) THEN
FIRST_X_ASSUM(ASSUME_TAC o MATCH_MP (SET_RULE
`
IMAGE X s
INTER IMAGE X t = {} ==> s
INTER t = {}`)) THEN
CONJ_TAC THEN MATCH_MP_TAC
HULL_MINIMAL THEN
(CONJ_TAC THENL [ALL_TAC; ASM_MESON_TAC[
SUBSET;
CONVEX_INTERS]]) THEN
REWRITE_TAC[
SUBSET;
IN_INTERS;
FORALL_IN_IMAGE] THEN ASM SET_TAC[]);;
let HELLY_CLOSED = prove
(`!f:(real^N->bool)->bool.
(FINITE f ==>
CARD f >=
dimindex (:N) + 1) /\
(!s. s
IN f ==>
convex s /\
closed s) /\ (?s. s
IN f /\
bounded s) /\
(!t. t
SUBSET f /\ FINITE t /\
CARD(t) =
dimindex(:N) + 1
==> ~(
INTERS t = {}))
==> ~(
INTERS f = {})`,
GEN_TAC THEN REWRITE_TAC[
GE] THEN
DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN
MATCH_MP_TAC
HELLY_CLOSED_ALT THEN ASM_REWRITE_TAC[] THEN
X_GEN_TAC `g:(real^N->bool)->bool` THEN STRIP_TAC THEN
MP_TAC(ISPECL [`
dimindex(:N) + 1`; `g:(real^N->bool)->bool`;
`f:(real^N->bool)->bool`]
CHOOSE_SUBSET_BETWEEN) THEN
ASM_REWRITE_TAC[] THEN
DISCH_THEN(X_CHOOSE_THEN `h:(real^N->bool)->bool` STRIP_ASSUME_TAC) THEN
MATCH_MP_TAC(SET_RULE `!s. s
SUBSET t /\ ~(s = {}) ==> ~(t = {})`) THEN
EXISTS_TAC `
INTERS h: real^N->bool` THEN
CONJ_TAC THENL [ASM SET_TAC[]; FIRST_X_ASSUM MATCH_MP_TAC] THEN
ASM_MESON_TAC[
HAS_SIZE]);;
(* ------------------------------------------------------------------------- *)
(* Kirchberger's theorem *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Convex hull is "preserved" by a linear function. *)
(* ------------------------------------------------------------------------- *)
add_linear_invariants [CONVEX_HULL_LINEAR_IMAGE];;
(* ------------------------------------------------------------------------- *)
(* Convexity of general and special intervals. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* On real^1, is_interval, convex and connected are all equivalent. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Jung's theorem. *)
(* Proof taken from http://cstheory.wordpress.com/2010/08/07/jungs-theorem/ *)
(* ------------------------------------------------------------------------- *)
let JUNG = prove
(`!s:real^N->bool r.
bounded s /\
sqrt(&(
dimindex(:N)) / &(2 *
dimindex(:N) + 2)) *
diameter s <= r
==> ?a. s
SUBSET cball(a,r)`,
let lemma = prove
(`&0 < x /\ x <= y ==> (x - &1) / x <= (y - &1) / y`,
SIMP_TAC[REAL_LE_LDIV_EQ] THEN REPEAT STRIP_TAC THEN
ONCE_REWRITE_TAC[REAL_ARITH `x / y * z:real = (x * z) / y`] THEN
SUBGOAL_THEN `&0 < y` ASSUME_TAC THENL
[ASM_REAL_ARITH_TAC; ASM_SIMP_TAC[REAL_LE_RDIV_EQ]] THEN
ASM_REAL_ARITH_TAC) in
REPEAT STRIP_TAC THEN
SUBGOAL_THEN `&0 <= r` ASSUME_TAC THENL
[FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REWRITE_RULE[IMP_CONJ_ALT]
REAL_LE_TRANS)) THEN
MATCH_MP_TAC REAL_LE_MUL THEN ASM_SIMP_TAC[DIAMETER_POS_LE] THEN
SIMP_TAC[SQRT_POS_LE; REAL_LE_DIV; REAL_POS];
ALL_TAC] THEN
MP_TAC(ISPEC `IMAGE (\x:real^N. cball(x,r)) s` HELLY_COMPACT_ALT) THEN
REWRITE_TAC[FORALL_IN_IMAGE; COMPACT_CBALL; CONVEX_CBALL] THEN
REWRITE_TAC[TAUT `p /\ q /\ r ==> s <=> q /\ p ==> r ==> s`] THEN
REWRITE_TAC[FORALL_FINITE_SUBSET_IMAGE] THEN
REWRITE_TAC[INTERS_IMAGE; GSYM MEMBER_NOT_EMPTY] THEN
REWRITE_TAC[SUBSET; IN_CBALL; IN_ELIM_THM] THEN
ANTS_TAC THENL [ALL_TAC; MESON_TAC[DIST_SYM]] THEN
X_GEN_TAC `t:real^N->bool` THEN REWRITE_TAC[GSYM SUBSET] THEN
STRIP_TAC THEN
ASM_SIMP_TAC[CARD_IMAGE_INJ; EQ_BALLS; GSYM REAL_NOT_LE] THEN
UNDISCH_TAC `FINITE(t:real^N->bool)` THEN
SUBGOAL_THEN `bounded(t:real^N->bool)` MP_TAC THENL
[ASM_MESON_TAC[BOUNDED_SUBSET]; ALL_TAC] THEN
UNDISCH_TAC `&0 <= r` THEN
SUBGOAL_THEN
`sqrt(&(dimindex(:N)) / &(2 * dimindex(:N) + 2)) *
diameter(t:real^N->bool) <= r`
MP_TAC THENL
[FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REWRITE_RULE[IMP_CONJ_ALT]
REAL_LE_TRANS)) THEN
MATCH_MP_TAC REAL_LE_LMUL THEN
ASM_SIMP_TAC[DIAMETER_SUBSET; SQRT_POS_LE; REAL_POS; REAL_LE_DIV];
POP_ASSUM_LIST(K ALL_TAC) THEN
SPEC_TAC(`t:real^N->bool`,`s:real^N->bool`) THEN
REPEAT STRIP_TAC] THEN
ASM_CASES_TAC `s:real^N->bool = {}` THEN ASM_REWRITE_TAC[NOT_IN_EMPTY] THEN
MP_TAC(ISPEC `{d | &0 <= d /\ ?a:real^N. s SUBSET cball(a,d)}` INF) THEN
ABBREV_TAC `d = inf {d | &0 <= d /\ ?a:real^N. s SUBSET cball(a,d)}` THEN
REWRITE_TAC[IN_ELIM_THM] THEN ANTS_TAC THENL
[REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; IN_ELIM_THM] THEN
ASM_MESON_TAC[BOUNDED_SUBSET_CBALL; REAL_LT_IMP_LE];
DISCH_THEN(CONJUNCTS_THEN2 (LABEL_TAC "P") (LABEL_TAC "M"))] THEN
SUBGOAL_THEN `&0 <= d` ASSUME_TAC THENL
[ASM_MESON_TAC[REAL_LE_REFL]; ALL_TAC] THEN
SUBGOAL_THEN `?a:real^N. s SUBSET cball(a,d)` MP_TAC THENL
[SUBGOAL_THEN
`!n. ?a:real^N. s SUBSET cball(a,d + inv(&n + &1))`
MP_TAC THENL
[X_GEN_TAC `n:num` THEN
REMOVE_THEN "M" (MP_TAC o SPEC `d + inv(&n + &1)`) THEN
REWRITE_TAC[REAL_ARITH `d + i <= d <=> ~(&0 < i)`] THEN
REWRITE_TAC[REAL_LT_INV_EQ; REAL_ARITH `&0 < &n + &1`] THEN
REWRITE_TAC[NOT_FORALL_THM; NOT_IMP; REAL_NOT_LE] THEN
MESON_TAC[SUBSET_CBALL; REAL_LT_IMP_LE; SUBSET_TRANS];
ALL_TAC] THEN
REWRITE_TAC[LEFT_IMP_EXISTS_THM; SKOLEM_THM] THEN
X_GEN_TAC `aa:num->real^N` THEN DISCH_TAC THEN
SUBGOAL_THEN `?t. compact t /\ !n. (aa:num->real^N) n IN t` MP_TAC THENL
[FIRST_X_ASSUM(MP_TAC o SPEC `vec 0:real^N` o
MATCH_MP BOUNDED_SUBSET_CBALL) THEN
REWRITE_TAC[LEFT_IMP_EXISTS_THM; SUBSET; IN_CBALL_0] THEN
X_GEN_TAC `B:real` THEN STRIP_TAC THEN
EXISTS_TAC `cball(vec 0:real^N,B + d + &1)` THEN
REWRITE_TAC[COMPACT_CBALL; IN_CBALL_0] THEN X_GEN_TAC `n:num` THEN
RULE_ASSUM_TAC(REWRITE_RULE[SUBSET; IN_CBALL]) THEN
MATCH_MP_TAC(NORM_ARITH
`(?x:real^N. norm(x) <= B /\ dist(a,x) <= d) ==> norm(a) <= B + d`) THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM MEMBER_NOT_EMPTY]) THEN
MATCH_MP_TAC MONO_EXISTS THEN REPEAT STRIP_TAC THEN ASM_SIMP_TAC[] THEN
MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `d + inv(&n + &1)` THEN
ASM_SIMP_TAC[REAL_LE_LADD] THEN
MATCH_MP_TAC REAL_INV_LE_1 THEN REAL_ARITH_TAC;
ALL_TAC] THEN
REWRITE_TAC[compact; LEFT_IMP_EXISTS_THM] THEN
X_GEN_TAC `t:real^N->bool` THEN
DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
DISCH_THEN(MP_TAC o SPEC `aa:num->real^N`) THEN ASM_REWRITE_TAC[] THEN
MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `a:real^N` THEN
DISCH_THEN(X_CHOOSE_THEN `r:num->num` STRIP_ASSUME_TAC) THEN
REWRITE_TAC[SUBSET; IN_CBALL] THEN X_GEN_TAC `x:real^N` THEN DISCH_TAC THEN
REWRITE_TAC[GSYM REAL_NOT_LT] THEN DISCH_TAC THEN
MP_TAC(SPEC `(dist(a:real^N,x) - d) / &2` REAL_ARCH_INV) THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [LIM_SEQUENTIALLY]) THEN
DISCH_THEN(MP_TAC o SPEC `(dist(a:real^N,x) - d) / &2`) THEN
ASM_SIMP_TAC[REAL_SUB_LT; REAL_HALF; o_THM] THEN
DISCH_THEN(X_CHOOSE_THEN `N1:num` STRIP_ASSUME_TAC) THEN
DISCH_THEN(X_CHOOSE_THEN `N2:num` STRIP_ASSUME_TAC) THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE BINDER_CONV [SUBSET]) THEN
DISCH_THEN(MP_TAC o SPECL [`(r:num->num)(N1 + N2)`; `x:real^N`]) THEN
ASM_REWRITE_TAC[IN_CBALL; REAL_NOT_LE] THEN
FIRST_X_ASSUM(MP_TAC o SPEC `N1 + N2:num`) THEN
ASM_REWRITE_TAC[LE_ADD] THEN
SUBGOAL_THEN `inv(&(r (N1 + N2:num)) + &1) < (dist(a:real^N,x) - d) / &2`
MP_TAC THENL [ALL_TAC; NORM_ARITH_TAC] THEN
MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC `inv(&N2)` THEN
ASM_REWRITE_TAC[] THEN MATCH_MP_TAC REAL_LE_INV2 THEN
CONJ_TAC THENL [ASM_MESON_TAC[REAL_LT_INV_EQ]; ALL_TAC] THEN
REWRITE_TAC[REAL_OF_NUM_LE; REAL_OF_NUM_ADD] THEN
MATCH_MP_TAC(ARITH_RULE
`N1 + N2 <= r(N1 + N2) ==> N2 <= r(N1 + N2) + 1`) THEN
ASM_MESON_TAC[MONOTONE_BIGGER];
ALL_TAC] THEN
MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `a:real^N` THEN
ONCE_REWRITE_TAC[DIST_SYM] THEN
REWRITE_TAC[GSYM IN_CBALL; GSYM SUBSET] THEN
DISCH_THEN(fun th -> ASSUME_TAC th THEN MP_TAC th) THEN
MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ_ALT] SUBSET_TRANS) THEN
MATCH_MP_TAC SUBSET_CBALL THEN
FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH
`a * s <= r ==> d <= a * s ==> d <= r`)) THEN
UNDISCH_THEN `&0 <= r` (K ALL_TAC) THEN REMOVE_THEN "M" (K ALL_TAC) THEN
FIRST_X_ASSUM(K ALL_TAC o SYM) THEN REMOVE_THEN "P" MP_TAC THEN
REWRITE_TAC[RIGHT_AND_EXISTS_THM; LEFT_IMP_EXISTS_THM] THEN
ABBREV_TAC `n = CARD(s:real^N->bool)` THEN
SUBGOAL_THEN `(s:real^N->bool) HAS_SIZE n` MP_TAC THENL
[ASM_REWRITE_TAC[HAS_SIZE]; ALL_TAC] THEN
UNDISCH_THEN `CARD(s:real^N->bool) = n` (K ALL_TAC) THEN
POP_ASSUM_LIST(MP_TAC o end_itlist CONJ o rev) THEN
SPEC_TAC(`d:real`,`r:real`) THEN GEN_TAC THEN
GEOM_ORIGIN_TAC `a:real^N` THEN SIMP_TAC[HAS_SIZE] THEN
REPEAT STRIP_TAC THEN FIRST_X_ASSUM(SUBST_ALL_TAC o SYM) THEN
ABBREV_TAC `t = {x:real^N | x IN s /\ norm(x) = r}` THEN
SUBGOAL_THEN `FINITE(t:real^N->bool)` ASSUME_TAC THENL
[EXPAND_TAC "t" THEN ASM_SIMP_TAC[FINITE_RESTRICT]; ALL_TAC] THEN
SUBGOAL_THEN `(vec 0:real^N) IN convex hull t` MP_TAC THENL
[MATCH_MP_TAC(TAUT `(~p ==> F) ==> p`) THEN DISCH_TAC THEN
MP_TAC(ISPEC `convex hull t:real^N->bool`
SEPARATING_HYPERPLANE_CLOSED_0) THEN
ASM_SIMP_TAC[CONVEX_CONVEX_HULL; NOT_IMP; COMPACT_CONVEX_HULL;
FINITE_IMP_COMPACT; COMPACT_IMP_CLOSED] THEN
REWRITE_TAC[NOT_EXISTS_THM; TAUT `~(p /\ q) <=> p ==> ~q`] THEN
X_GEN_TAC `v:real^N` THEN
ABBREV_TAC `k = CARD(s:real^N->bool)` THEN
SUBGOAL_THEN `(s:real^N->bool) HAS_SIZE k` MP_TAC THENL
[ASM_REWRITE_TAC[HAS_SIZE]; ALL_TAC] THEN
UNDISCH_THEN `CARD(s:real^N->bool) = k` (K ALL_TAC) THEN
POP_ASSUM_LIST(MP_TAC o end_itlist CONJ o rev) THEN
GEOM_BASIS_MULTIPLE_TAC 1 `v:real^N` THEN X_GEN_TAC `m:real` THEN
GEN_REWRITE_TAC LAND_CONV [REAL_ARITH `&0 <= x <=> x = &0 \/ &0 < x`] THEN
STRIP_TAC THEN ASM_REWRITE_TAC[VECTOR_MUL_EQ_0] THEN
ASM_SIMP_TAC[BASIS_NONZERO; DIMINDEX_GE_1; LE_REFL; REAL_LT_IMP_NZ] THEN
REPEAT GEN_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[HAS_SIZE] THEN
DISCH_THEN(SUBST_ALL_TAC o SYM) THEN X_GEN_TAC `b:real` THEN DISCH_TAC THEN
ASM_SIMP_TAC[DOT_LMUL; DOT_BASIS; DIMINDEX_GE_1; LE_REFL] THEN
ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
ASM_SIMP_TAC[real_gt; GSYM REAL_LT_LDIV_EQ] THEN
SUBGOAL_THEN `&0 < b / m` MP_TAC THENL
[ASM_SIMP_TAC[REAL_LT_DIV];
UNDISCH_THEN `&0 < b` (K ALL_TAC) THEN
SPEC_TAC(`b / m:real`,`b:real`)] THEN
X_GEN_TAC `b:real` THEN DISCH_TAC THEN DISCH_TAC THEN
SUBGOAL_THEN
`!x:real^N e. &0 < e /\ e < b /\ x IN t ==> norm(x - e % basis 1) < r`
ASSUME_TAC THENL
[MAP_EVERY X_GEN_TAC [`x:real^N`; `e:real`] THEN STRIP_TAC THEN
SUBGOAL_THEN `r = norm(x:real^N)` SUBST1_TAC THENL
[ASM SET_TAC[]; REWRITE_TAC[NORM_LT; dot]] THEN
SIMP_TAC[SUM_CLAUSES_LEFT; DIMINDEX_GE_1] THEN
SIMP_TAC[VECTOR_SUB_COMPONENT; VECTOR_MUL_COMPONENT;
BASIS_COMPONENT; DIMINDEX_GE_1; LE_REFL;
ARITH_RULE `2 <= n ==> 1 <= n /\ ~(n = 1)`; ARITH] THEN
REWRITE_TAC[REAL_MUL_RZERO; REAL_SUB_RZERO; REAL_LT_RADD] THEN
REWRITE_TAC[GSYM REAL_POW_2; GSYM REAL_LT_SQUARE_ABS] THEN
MATCH_MP_TAC(REAL_ARITH
`!b. &0 < e /\ e < b /\ b < x ==> abs(x - e * &1) < abs x`) THEN
EXISTS_TAC `b:real` THEN ASM_REWRITE_TAC[] THEN
ASM_MESON_TAC[HULL_INC];
ALL_TAC] THEN
SUBGOAL_THEN
`?d. &0 < d /\
!x:real^N a. x IN (s DIFF t) /\ norm(a) < d ==> norm(x - a) < r`
STRIP_ASSUME_TAC THENL
[ASM_CASES_TAC `s DIFF t:real^N->bool = {}` THENL
[ASM_REWRITE_TAC[NOT_IN_EMPTY] THEN MESON_TAC[REAL_LT_01]; ALL_TAC] THEN
EXISTS_TAC `inf (IMAGE (\x:real^N. r - norm x) (s DIFF t))` THEN
SUBGOAL_THEN `FINITE(s DIFF t:real^N->bool)` ASSUME_TAC THENL
[ASM_MESON_TAC[FINITE_DIFF]; ALL_TAC] THEN
ASM_SIMP_TAC[REAL_LT_INF_FINITE; FINITE_IMAGE; IMAGE_EQ_EMPTY] THEN
REWRITE_TAC[FORALL_IN_IMAGE] THEN SIMP_TAC
[NORM_ARITH `norm a < r - norm x ==> norm(x - a:real^N) < r`] THEN
EXPAND_TAC "t" THEN REWRITE_TAC[IN_DIFF; IN_ELIM_THM; REAL_SUB_LT] THEN
RULE_ASSUM_TAC(REWRITE_RULE[SUBSET; IN_CBALL_0]) THEN
ASM_MESON_TAC[REAL_LT_LE];
ALL_TAC] THEN
SUBGOAL_THEN
`?a. !x. x IN s ==> norm(x - a:real^N) < r`
STRIP_ASSUME_TAC THENL
[EXISTS_TAC `min (b / &2) (d / &2) % basis 1:real^N` THEN
X_GEN_TAC `x:real^N` THEN DISCH_TAC THEN
ASM_CASES_TAC `(x:real^N) IN t` THENL
[MATCH_MP_TAC(ASSUME
`!x:real^N e. &0 < e /\ e < b /\ x IN t
==> norm (x - e % basis 1) < r`) THEN
ASM_REWRITE_TAC[] THEN ASM_REAL_ARITH_TAC;
MATCH_MP_TAC(ASSUME
`!x:real^N a. x IN s DIFF t /\ norm a < d ==> norm (x - a) < r`) THEN
ASM_SIMP_TAC[IN_DIFF; NORM_MUL; LE_REFL; NORM_BASIS;
DIMINDEX_GE_1] THEN
ASM_REAL_ARITH_TAC];
SUBGOAL_THEN `&0 < r` ASSUME_TAC THENL
[ASM_MESON_TAC[MEMBER_NOT_EMPTY; NORM_ARITH
`norm(x:real^N) < r ==> &0 < r`];
ALL_TAC] THEN
UNDISCH_THEN
`!x a:real^N. &0 <= x /\ s SUBSET cball (a,x) ==> r <= x` (MP_TAC o
SPECL [`max (&0) (r - inf (IMAGE (\x:real^N. r - norm(x - a)) s))`;
`a:real^N`]) THEN
ASM_SIMP_TAC[REAL_ARITH `&0 < r ==> (r <= max (&0) a <=> r <= a)`] THEN
REWRITE_TAC[SUBSET; IN_CBALL; REAL_ARITH `a <= max a b`] THEN
REWRITE_TAC[NOT_IMP; REAL_ARITH `~(r <= r - x) <=> &0 < x`] THEN
ASM_SIMP_TAC[REAL_LT_INF_FINITE; FINITE_IMAGE; IMAGE_EQ_EMPTY] THEN
ASM_REWRITE_TAC[FORALL_IN_IMAGE; REAL_SUB_LT] THEN
X_GEN_TAC `x:real^N` THEN DISCH_TAC THEN
MATCH_MP_TAC(REAL_ARITH `d <= b ==> d <= max a b`) THEN
ONCE_REWRITE_TAC[REAL_ARITH `a <= b - c <=> c <= b - a`] THEN
ASM_SIMP_TAC[REAL_INF_LE_FINITE; FINITE_IMAGE; IMAGE_EQ_EMPTY] THEN
REWRITE_TAC[EXISTS_IN_IMAGE; ONCE_REWRITE_RULE[NORM_SUB] dist] THEN
ASM_MESON_TAC[REAL_LE_REFL]];
ALL_TAC] THEN
ASM_CASES_TAC `t:real^N->bool = {}` THEN
ASM_REWRITE_TAC[CONVEX_HULL_EMPTY; NOT_IN_EMPTY] THEN
REWRITE_TAC[CONVEX_HULL_FINITE; IN_ELIM_THM] THEN
DISCH_THEN(X_CHOOSE_THEN `l:real^N->real` STRIP_ASSUME_TAC) THEN
MATCH_MP_TAC REAL_LE_TRANS THEN
EXISTS_TAC `sqrt((&(dimindex (:N)) / &(2 * dimindex (:N) + 2)) *
diameter(s:real^N->bool) pow 2)` THEN
CONJ_TAC THENL
[MATCH_MP_TAC REAL_LE_RSQRT;
ASM_SIMP_TAC[SQRT_MUL; DIAMETER_POS_LE; REAL_POW_LE; REAL_LE_DIV;
REAL_POS; POW_2_SQRT; REAL_LE_REFL]] THEN
SUBGOAL_THEN
`sum t (\y:real^N. &2 * r pow 2) <=
sum t (\y. (&1 - l y) * diameter(s:real^N->bool) pow 2)`
MP_TAC THENL
[MATCH_MP_TAC SUM_LE THEN ASM_REWRITE_TAC[] THEN
X_GEN_TAC `x:real^N` THEN DISCH_TAC THEN
MATCH_MP_TAC REAL_LE_TRANS THEN
EXISTS_TAC `sum (t DELETE x) (\x:real^N. l(x)) *
diameter(s:real^N->bool) pow 2` THEN CONJ_TAC THENL
[ALL_TAC; ASM_SIMP_TAC[SUM_DELETE; ETA_AX; REAL_LE_REFL]] THEN
REWRITE_TAC[GSYM SUM_RMUL] THEN MATCH_MP_TAC REAL_LE_TRANS THEN
EXISTS_TAC `sum (t DELETE x) (\y:real^N. l y * norm(y - x) pow 2)` THEN
CONJ_TAC THENL
[ALL_TAC;
MATCH_MP_TAC SUM_LE THEN ASM_REWRITE_TAC[FINITE_DELETE; IN_DELETE] THEN
X_GEN_TAC `y:real^N` THEN STRIP_TAC THEN MATCH_MP_TAC REAL_LE_LMUL THEN
ASM_SIMP_TAC[] THEN MATCH_MP_TAC REAL_POW_LE2 THEN
REWRITE_TAC[NORM_POS_LE] THEN
MATCH_MP_TAC DIAMETER_BOUNDED_BOUND THEN ASM SET_TAC[]] THEN
MATCH_MP_TAC REAL_LE_TRANS THEN
EXISTS_TAC `sum t (\y:real^N. l y * norm (y - x) pow 2)` THEN
CONJ_TAC THENL
[ALL_TAC;
MATCH_MP_TAC REAL_EQ_IMP_LE THEN MATCH_MP_TAC SUM_EQ_SUPERSET THEN
ASM_REWRITE_TAC[FINITE_DELETE] THEN
CONJ_TAC THENL [SET_TAC[]; REWRITE_TAC[IN_DELETE]] THEN
SIMP_TAC[TAUT `p /\ ~(p /\ ~q) <=> p /\ q`] THEN
REWRITE_TAC[VECTOR_SUB_REFL; NORM_0] THEN REAL_ARITH_TAC] THEN
REWRITE_TAC[NORM_POW_2; VECTOR_ARITH
`(y - x:real^N) dot (y - x) = (x dot x + y dot y) - &2 * x dot y`] THEN
MATCH_MP_TAC REAL_LE_TRANS THEN
EXISTS_TAC `sum t (\y:real^N. l y * (&2 * r pow 2 - &2 * (x dot y)))` THEN
CONJ_TAC THENL
[ALL_TAC;
MATCH_MP_TAC REAL_EQ_IMP_LE THEN MATCH_MP_TAC SUM_EQ THEN
UNDISCH_TAC `(x:real^N) IN t` THEN EXPAND_TAC "t" THEN
REWRITE_TAC[IN_DELETE; IN_ELIM_THM] THEN
SIMP_TAC[NORM_EQ_SQUARE; NORM_POW_2] THEN REAL_ARITH_TAC] THEN
REWRITE_TAC[REAL_ARITH `x * (&2 * y - &2 * z) = &2 * (x * y - x * z)`] THEN
REWRITE_TAC[SUM_LMUL] THEN MATCH_MP_TAC REAL_LE_LMUL THEN
REWRITE_TAC[REAL_POS] THEN
ASM_SIMP_TAC[SUM_SUB; FINITE_DELETE; SUM_RMUL] THEN
REWRITE_TAC[GSYM DOT_RMUL] THEN
ASM_SIMP_TAC[GSYM DOT_RSUM; DOT_RZERO] THEN REAL_ARITH_TAC;
ASM_SIMP_TAC[SUM_CONST; SUM_RMUL; SUM_SUB] THEN
REWRITE_TAC[REAL_OF_NUM_MUL; MULT_CLAUSES] THEN
GEN_REWRITE_TAC (LAND_CONV o LAND_CONV) [REAL_MUL_SYM] THEN
SUBGOAL_THEN `&0 < &(CARD(t:real^N->bool) * 2)` ASSUME_TAC THENL
[REWRITE_TAC[REAL_OF_NUM_LT; ARITH_RULE `0 < n * 2 <=> ~(n = 0)`] THEN
ASM_SIMP_TAC[CARD_EQ_0];
ASM_SIMP_TAC[GSYM REAL_LE_RDIV_EQ] THEN
MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ_ALT] REAL_LE_TRANS) THEN
REWRITE_TAC[REAL_ARITH `(a * b) / c:real = a / c * b`] THEN
MATCH_MP_TAC REAL_LE_RMUL THEN REWRITE_TAC[REAL_LE_POW_2] THEN
REWRITE_TAC[ARITH_RULE `2 * n + 2 = (n + 1) * 2`; GSYM REAL_OF_NUM_MUL;
real_div; REAL_INV_MUL; REAL_MUL_ASSOC] THEN
MATCH_MP_TAC REAL_LE_RMUL THEN REWRITE_TAC[GSYM real_div] THEN
CONV_TAC REAL_RAT_REDUCE_CONV THEN
SUBGOAL_THEN `&(dimindex(:N)) = &(dimindex(:N) + 1) - &1`
SUBST1_TAC THENL
[REWRITE_TAC[GSYM REAL_OF_NUM_ADD] THEN REAL_ARITH_TAC;
MATCH_MP_TAC lemma THEN
ASM_SIMP_TAC[REAL_OF_NUM_LE; REAL_OF_NUM_LT; CARD_EQ_0;
ARITH_RULE `0 < n <=> ~(n = 0)`] THEN
MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `CARD(s:real^N->bool)` THEN
ASM_REWRITE_TAC[] THEN MATCH_MP_TAC CARD_SUBSET THEN
ASM SET_TAC[]]]]);;
(* ------------------------------------------------------------------------- *)
(* Convex cones and corresponding hulls. *)
(* ------------------------------------------------------------------------- *)
let CONVEX_CONE = prove
(`!s:real^N->bool.
convex_cone s <=>
vec 0
IN s /\
(!x y. x
IN s /\ y
IN s ==> (x + y)
IN s) /\
(!x c. x
IN s /\ &0 <= c ==> (c % x)
IN s)`,
GEN_TAC THEN REWRITE_TAC[
convex_cone; GSYM
conic] THEN
ASM_CASES_TAC `
conic(s:real^N->bool)` THEN
ASM_SIMP_TAC[
CONIC_CONTAINS_0] THEN AP_TERM_TAC THEN
RULE_ASSUM_TAC(REWRITE_RULE[
conic]) THEN
REWRITE_TAC[
convex] THEN EQ_TAC THEN
ASM_SIMP_TAC[
REAL_SUB_LE] THEN DISCH_TAC THEN
MAP_EVERY X_GEN_TAC [`x:real^N`; `y:real^N`] THEN STRIP_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPECL
[`&2 % (x:real^N)`; `&2 % (y:real^N)`; `&1 / &2`; `&1 / &2`]) THEN
REWRITE_TAC[
VECTOR_MUL_ASSOC] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
ASM_SIMP_TAC[
VECTOR_MUL_LID;
REAL_POS]);;
add_linear_invariants [CONVEX_CONE_LINEAR_IMAGE_EQ];;
add_linear_invariants [CONVEX_CONE_HULL_LINEAR_IMAGE];;
(* ------------------------------------------------------------------------- *)
(* Epigraphs of convex functions. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Use this to derive general bound property of convex function. *)
(* ------------------------------------------------------------------------- *)
let FORALL_OF_DROP = prove
(`(!v. P (
drop o v)) <=> (!x:A->real. P x)`,
EQ_TAC THENL [ALL_TAC; MESON_TAC[]] THEN REPEAT STRIP_TAC THEN
FIRST_ASSUM(MP_TAC o SPEC `\a:A.
lift(x a)`) THEN
REWRITE_TAC[
o_DEF;
LIFT_DROP; ETA_AX]);;
(* ------------------------------------------------------------------------- *)
(* Another intermediate value theorem formulation. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* A bound within a convex hull, and so an interval. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Representation of any interval as a finite convex hull. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Bounded convex function on open set is continuous. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Upper bound on a ball implies upper and lower bounds. *)
(* ------------------------------------------------------------------------- *)
let CONVEX_BOUNDS_LEMMA = prove
(`!f x:real^N e.
f
convex_on cball(x,e) /\
(!y. y
IN cball(x,e) ==> f(y) <= b)
==> !y. y
IN cball(x,e) ==> abs(f(y)) <= b + &2 * abs(f(x))`,
REPEAT GEN_TAC THEN ASM_CASES_TAC `&0 <= e` THENL
[ALL_TAC;
REWRITE_TAC[
IN_CBALL] THEN ASM_MESON_TAC[
DIST_POS_LE;
REAL_LE_TRANS]] THEN
REPEAT STRIP_TAC THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [
convex_on]) THEN
DISCH_THEN(MP_TAC o SPECL
[`y:real^N`; `&2 % x - y:real^N`; `&1 / &2`; `&1 / &2`]) THEN
REWRITE_TAC[GSYM
VECTOR_ADD_LDISTRIB; GSYM REAL_ADD_LDISTRIB] THEN
REWRITE_TAC[VECTOR_ARITH `y + x - y = x:real^N`] THEN
REWRITE_TAC[
VECTOR_MUL_ASSOC] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
ABBREV_TAC `z = &2 % x - y:real^N` THEN
SUBGOAL_THEN `z:real^N
IN cball(x,e)` ASSUME_TAC THENL
[UNDISCH_TAC `y:real^N
IN cball(x,e)` THEN
EXPAND_TAC "z" THEN REWRITE_TAC[
dist;
IN_CBALL] THEN
REWRITE_TAC[VECTOR_ARITH `x - (&2 % x - y) = y - x`] THEN
REWRITE_TAC[
NORM_SUB];
ALL_TAC] THEN
ASM_REWRITE_TAC[
VECTOR_MUL_LID] THEN ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
REWRITE_TAC[
real_div; REAL_MUL_LID] THEN REWRITE_TAC[GSYM
real_div] THEN
ASM_SIMP_TAC[
REAL_LE_RDIV_EQ;
REAL_OF_NUM_LT; ARITH] THEN
FIRST_X_ASSUM(fun
th ->
MAP_EVERY (MP_TAC o C SPEC
th) [`y:real^N`; `z:real^N`]) THEN
ASM_REWRITE_TAC[
CENTRE_IN_CBALL] THEN REAL_ARITH_TAC);;
(* ------------------------------------------------------------------------- *)
(* Hence a convex function on an open set is continuous. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Characterizations of convex functions in terms of sequents. *)
(* ------------------------------------------------------------------------- *)
let CONVEX_ON_LEFT_SECANT_MUL,CONVEX_ON_RIGHT_SECANT_MUL = (CONJ_PAIR o prove)
(`(!f s:real^N->bool.
f convex_on s <=>
!a b x. a IN s /\ b IN s /\ x IN segment[a,b]
==> (f x - f a) * norm(b - a) <= (f b - f a) * norm(x - a)) /\
(!f s:real^N->bool.
f convex_on s <=>
!a b x. a IN s /\ b IN s /\ x IN segment[a,b]
==> (f b - f a) * norm(b - x) <= (f b - f x) * norm(b - a))`,
CONJ_TAC THEN
REPEAT GEN_TAC THEN REWRITE_TAC[convex_on] THEN
AP_TERM_TAC THEN GEN_REWRITE_TAC I [FUN_EQ_THM] THEN
X_GEN_TAC `a:real^N` THEN REWRITE_TAC[] THEN
AP_TERM_TAC THEN GEN_REWRITE_TAC I [FUN_EQ_THM] THEN
X_GEN_TAC `b:real^N` THEN REWRITE_TAC[] THEN
ASM_CASES_TAC `(a:real^N) IN s` THEN ASM_REWRITE_TAC[] THEN
ASM_CASES_TAC `(b:real^N) IN s` THEN ASM_REWRITE_TAC[] THEN
REWRITE_TAC[IN_SEGMENT; LEFT_IMP_EXISTS_THM] THEN
ONCE_REWRITE_TAC[SWAP_FORALL_THM] THEN
AP_TERM_TAC THEN GEN_REWRITE_TAC I [FUN_EQ_THM] THEN
X_GEN_TAC `u:real` THEN REWRITE_TAC[] THEN
REWRITE_TAC[TAUT `a /\ x = y <=> x = y /\ a`;
TAUT `a /\ x = y /\ b <=> x = y /\ a /\ b`] THEN
REWRITE_TAC[REAL_ARITH `v + u = &1 <=> v = &1 - u`] THEN
REWRITE_TAC[FORALL_UNWIND_THM2; IMP_CONJ] THEN
REWRITE_TAC[REAL_SUB_LE] THEN
ASM_CASES_TAC `&0 <= u` THEN ASM_REWRITE_TAC[] THEN
ASM_CASES_TAC `u <= &1` THEN ASM_REWRITE_TAC[] THEN
REWRITE_TAC[VECTOR_ARITH `((&1 - u) % a + u % b) - a:real^N = u % (b - a)`;
VECTOR_ARITH `b - ((&1 - u) % a + u % b):real^N = (&1 - u) % (b - a)`] THEN
REWRITE_TAC[NORM_MUL; REAL_MUL_ASSOC] THEN
(ASM_CASES_TAC `b:real^N = a` THENL
[ASM_REWRITE_TAC[VECTOR_SUB_REFL; REAL_SUB_REFL;
VECTOR_ARITH `(&1 - u) % a + u % a:real^N = a`] THEN
REAL_ARITH_TAC;
ASM_SIMP_TAC[REAL_LE_RMUL_EQ; NORM_POS_LT; VECTOR_SUB_EQ] THEN
ASM_SIMP_TAC[REAL_ARITH
`&0 <= u /\ u <= &1 ==> abs u = u /\ abs(&1 - u) = &1 - u`] THEN
REAL_ARITH_TAC]));;
let CONVEX_ON_LEFT_SECANT,CONVEX_ON_RIGHT_SECANT = (CONJ_PAIR o prove)
(`(!f s:real^N->bool.
f convex_on s <=>
!a b x. a IN s /\ b IN s /\ x IN segment(a,b)
==> (f x - f a) / norm(x - a) <= (f b - f a) / norm(b - a)) /\
(!f s:real^N->bool.
f convex_on s <=>
!a b x. a IN s /\ b IN s /\ x IN segment(a,b)
==> (f b - f a) / norm(b - a) <= (f b - f x) / norm(b - x))`,
CONJ_TAC THEN REPEAT GEN_TAC THENL
[REWRITE_TAC[CONVEX_ON_LEFT_SECANT_MUL];
REWRITE_TAC[CONVEX_ON_RIGHT_SECANT_MUL]] THEN
AP_TERM_TAC THEN GEN_REWRITE_TAC I [FUN_EQ_THM] THEN
X_GEN_TAC `a:real^N` THEN REWRITE_TAC[] THEN
AP_TERM_TAC THEN GEN_REWRITE_TAC I [FUN_EQ_THM] THEN
X_GEN_TAC `b:real^N` THEN REWRITE_TAC[] THEN
ASM_CASES_TAC `(a:real^N) IN s` THEN ASM_REWRITE_TAC[] THEN
ASM_CASES_TAC `(b:real^N) IN s` THEN ASM_REWRITE_TAC[] THEN
ASM_CASES_TAC `a:real^N = b` THEN
ASM_REWRITE_TAC[SEGMENT_REFL; NOT_IN_EMPTY; REAL_SUB_REFL; VECTOR_SUB_REFL;
NORM_0; REAL_MUL_LZERO; REAL_MUL_RZERO; REAL_LE_REFL] THEN
AP_TERM_TAC THEN GEN_REWRITE_TAC I [FUN_EQ_THM] THEN
X_GEN_TAC `x:real^N` THEN REWRITE_TAC[] THEN
REWRITE_TAC[open_segment; IN_DIFF; IN_INSERT; NOT_IN_EMPTY] THEN
MAP_EVERY ASM_CASES_TAC [`x:real^N = a`; `x:real^N = b`] THEN
ASM_REWRITE_TAC[REAL_LE_REFL; REAL_SUB_REFL; VECTOR_SUB_REFL; NORM_0;
REAL_MUL_LZERO; REAL_MUL_RZERO] THEN
ASM_SIMP_TAC[REAL_LE_RDIV_EQ; GSYM REAL_LE_LDIV_EQ; NORM_POS_LT;
VECTOR_SUB_EQ] THEN
AP_TERM_TAC THEN REAL_ARITH_TAC);;
(* ------------------------------------------------------------------------- *)
(* Starlike sets and more stuff about line segments. *)
(* ------------------------------------------------------------------------- *)
add_linear_invariants [STARLIKE_LINEAR_IMAGE_EQ];;
add_translation_invariants [STARLIKE_TRANSLATION_EQ];;
add_linear_invariants [BETWEEN_LINEAR_IMAGE_EQ];;
add_translation_invariants [STARLIKE_TRANSLATION_EQ];;
(* ------------------------------------------------------------------------- *)
(* Shrinking towards the interior of a convex set. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Relative interior of a set. *)
(* ------------------------------------------------------------------------- *)
add_translation_invariants [RELATIVE_INTERIOR_TRANSLATION];;
add_translation_invariants [RELATIVE_FRONTIER_TRANSLATION];;
add_linear_invariants [RELATIVE_INTERIOR_INJECTIVE_LINEAR_IMAGE];;
add_linear_invariants [RELATIVE_FRONTIER_INJECTIVE_LINEAR_IMAGE];;
let CONVEX_RELATIVE_INTERIOR = prove
(`!s:real^N->bool.
convex s ==>
convex(
relative_interior s)`,
REWRITE_TAC[
CONVEX_ALT;
IN_RELATIVE_INTERIOR;
IN_INTER;
SUBSET;
IN_BALL;
dist] THEN
GEN_TAC THEN DISCH_TAC THEN REPEAT GEN_TAC THEN
REWRITE_TAC[TAUT `(a /\ b) /\ (c /\ d) /\ e ==> f <=>
a /\ c /\ e ==> b /\ d ==> f`] THEN
STRIP_TAC THEN ASM_SIMP_TAC[] THEN
MATCH_MP_TAC(MESON[] `(!d e. P d /\ Q e ==> R(min d e))
==> (?e. P e) /\ (?e. Q e) ==> (?e. R e)`) THEN
REPEAT GEN_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[
REAL_LT_MIN] THEN
X_GEN_TAC `z:real^N` THEN STRIP_TAC THEN
SUBST1_TAC(VECTOR_ARITH `z:real^N =
(&1 - u) % (z - u % (y - x)) + u % (z + (&1 - u) % (y - x))`) THEN
FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN
FIRST_X_ASSUM(CONJUNCTS_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
REWRITE_TAC[GSYM
IMP_CONJ_ALT] THEN MATCH_MP_TAC MONO_AND THEN
CONJ_TAC THEN DISCH_THEN MATCH_MP_TAC THEN
(CONJ_TAC THENL
[FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH
`
norm x < e ==>
norm x = y ==> y < e`)) THEN
AP_TERM_TAC THEN VECTOR_ARITH_TAC;
REWRITE_TAC[VECTOR_ARITH `a - b % c:real^N = a + --b % c`] THEN
MATCH_MP_TAC
IN_AFFINE_ADD_MUL_DIFF THEN
ASM_SIMP_TAC[
AFFINE_AFFINE_HULL;
HULL_INC]]));;
(* ------------------------------------------------------------------------- *)
(* Interior, relative interior and closure interrelations. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Homeomorphism of all convex compact sets with same affine dimension, and *)
(* in particular all those with nonempty interior. *)
(* ------------------------------------------------------------------------- *)
"usph"] THEN
REWRITE_TAC[SUBSET; IN_ELIM_THM] 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 STRIP_TAC THEN
MP_TAC(ISPECL [`s:real^N->bool`; `vec 0:real^N`; `x:real^N`]
RAY_TO_RELATIVE_FRONTIER) THEN
REWRITE_TAC[relative_frontier] THEN
ASM_SIMP_TAC[COMPACT_IMP_BOUNDED; CLOSURE_CLOSED; COMPACT_IMP_CLOSED;
VECTOR_ADD_LID] THEN
DISCH_THEN(X_CHOOSE_THEN `d:real` STRIP_ASSUME_TAC) THEN
EXPAND_TAC "proj" THEN REWRITE_TAC[IN_IMAGE] THEN
EXISTS_TAC `d % x:real^N` THEN ASM_REWRITE_TAC[NORM_MUL] THEN
ASM_SIMP_TAC[REAL_MUL_RID; real_abs; REAL_LT_IMP_LE] THEN
ASM_SIMP_TAC[VECTOR_MUL_ASSOC; REAL_MUL_LINV; REAL_LT_IMP_NZ;
VECTOR_MUL_LID]];
MAP_EVERY X_GEN_TAC [`x:real^N`; `y:real^N`] THEN
REWRITE_TAC[IN_DIFF] THEN STRIP_TAC THEN
ASM_CASES_TAC `x:real^N = vec 0` THENL [ASM SET_TAC[]; ALL_TAC] THEN
ASM_CASES_TAC `y:real^N = vec 0` THENL [ASM SET_TAC[]; ALL_TAC] THEN
UNDISCH_TAC `(proj:real^N->real^N) x = proj y` THEN
EXPAND_TAC "proj" THEN
REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC (REAL_ARITH
`norm(x:real^N) = norm(y:real^N) \/
norm x < norm y \/ norm y < norm x`)
THENL
[ASM_REWRITE_TAC[VECTOR_MUL_LCANCEL; REAL_INV_EQ_0; NORM_EQ_0];
DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o SPECL
[`y:real^N`; `norm(x:real^N) / norm(y:real^N)`]);
DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o SPECL
[`x:real^N`; `norm(y:real^N) / norm(x:real^N)`])] THEN
ASM_SIMP_TAC[REAL_LE_DIV; NORM_POS_LE; REAL_LT_LDIV_EQ; NORM_POS_LT;
REAL_MUL_LID] THEN
ASM_REWRITE_TAC[real_div; GSYM VECTOR_MUL_ASSOC] THENL
[FIRST_X_ASSUM(SUBST1_TAC o SYM); ALL_TAC] THEN
ASM_SIMP_TAC[VECTOR_MUL_ASSOC; REAL_MUL_RINV; NORM_EQ_0] THEN
ASM_REWRITE_TAC[VECTOR_MUL_LID]];
DISCH_THEN(fun th ->
CONJ_TAC THENL
[MESON_TAC[homeomorphic; th];
ONCE_REWRITE_TAC[HOMEOMORPHIC_SYM] THEN
MATCH_MP_TAC HOMEOMORPHIC_COMPACT THEN
SIMP_TAC[COMPACT_INTER_CLOSED; CLOSED_AFFINE_HULL; COMPACT_CBALL] THEN
MP_TAC th]) THEN
REWRITE_TAC[HOMEOMORPHISM; LEFT_IMP_EXISTS_THM] THEN
X_GEN_TAC `surf:real^N->real^N` THEN STRIP_TAC THEN
EXISTS_TAC `\x:real^N. norm(x) % (surf:real^N->real^N)(proj(x))` THEN
REWRITE_TAC[]] THEN
UNDISCH_THEN
`(proj:real^N->real^N) continuous_on s DIFF relative_interior s`
(K ALL_TAC) THEN
REWRITE_TAC[] THEN CONJ_TAC THENL
[REWRITE_TAC[CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN; IN_INTER] THEN
X_GEN_TAC `x:real^N` THEN STRIP_TAC THEN
ASM_CASES_TAC `x = vec 0:real^N` THENL
[ASM_REWRITE_TAC[CONTINUOUS_WITHIN; VECTOR_MUL_LZERO; NORM_0] THEN
MATCH_MP_TAC LIM_NULL_VMUL_BOUNDED THEN
FIRST_ASSUM(MP_TAC o MATCH_MP COMPACT_IMP_BOUNDED) THEN
REWRITE_TAC[BOUNDED_POS] THEN MATCH_MP_TAC MONO_EXISTS THEN
REPEAT STRIP_TAC THENL
[REWRITE_TAC[LIM_WITHIN; o_THM; DIST_0; NORM_LIFT; REAL_ABS_NORM] THEN
MESON_TAC[];
REWRITE_TAC[EVENTUALLY_WITHIN] THEN EXISTS_TAC `&1` THEN
REWRITE_TAC[REAL_LT_01; IN_INTER; DIST_0; NORM_POS_LT] THEN
ASM SET_TAC[]];
MATCH_MP_TAC CONTINUOUS_WITHIN_SUBSET THEN
EXISTS_TAC `affine hull s:real^N->bool` THEN
REWRITE_TAC[INTER_SUBSET] THEN MATCH_MP_TAC CONTINUOUS_MUL THEN
SIMP_TAC[CONTINUOUS_LIFT_NORM_COMPOSE; CONTINUOUS_WITHIN_ID; o_DEF] THEN
SUBGOAL_THEN
`((surf:real^N->real^N) o (proj:real^N->real^N)) continuous_on
(affine hull s DELETE vec 0)`
MP_TAC THENL
[MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN
ASM_REWRITE_TAC[] THEN CONJ_TAC THEN
FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REWRITE_RULE[IMP_CONJ]
CONTINUOUS_ON_SUBSET)) THEN
SIMP_TAC[SUBSET; IN_DELETE; IN_UNIV; FORALL_IN_IMAGE] THEN
EXPAND_TAC "usph" THEN ASM_SIMP_TAC[IN_ELIM_THM];
SIMP_TAC[CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN] THEN
DISCH_THEN(MP_TAC o SPEC `x:real^N`) THEN ASM_SIMP_TAC[IN_DELETE] THEN
REWRITE_TAC[CONTINUOUS_WITHIN; o_DEF] THEN MATCH_MP_TAC EQ_IMP THEN
MATCH_MP_TAC LIM_TRANSFORM_WITHIN_SET THEN
REWRITE_TAC[EVENTUALLY_AT] THEN EXISTS_TAC `norm(x:real^N)` THEN
ASM_REWRITE_TAC[IN_DELETE; IN_INTER; IN_CBALL; NORM_POS_LT] THEN
X_GEN_TAC `y:real^N` THEN
ASM_CASES_TAC `(y:real^N) IN affine hull s` THEN ASM_REWRITE_TAC[] THEN
CONV_TAC NORM_ARITH]];
ALL_TAC] THEN
SUBGOAL_THEN
`!a x. &0 < a ==> (proj:real^N->real^N)(a % x) = proj x`
ASSUME_TAC THENL
[REPEAT GEN_TAC THEN EXPAND_TAC "proj" THEN
REWRITE_TAC[NORM_MUL; REAL_INV_MUL; VECTOR_MUL_ASSOC] THEN
SIMP_TAC[REAL_FIELD `&0 < a ==> (inv(a) * x) * a = x`; real_abs;
REAL_LT_IMP_LE];
ALL_TAC] THEN
CONJ_TAC THENL
[ALL_TAC;
MAP_EVERY X_GEN_TAC [`x:real^N`; `y:real^N`] THEN
ASM_CASES_TAC `y:real^N = vec 0` THENL
[ASM_SIMP_TAC[VECTOR_MUL_LZERO; VECTOR_MUL_EQ_0; NORM_0; NORM_EQ_0] THEN
ASM SET_TAC[];
ALL_TAC] THEN
ASM_CASES_TAC `x:real^N = vec 0` THENL
[CONV_TAC(ONCE_DEPTH_CONV SYM_CONV) THEN
ASM_SIMP_TAC[VECTOR_MUL_LZERO; VECTOR_MUL_EQ_0; NORM_0; NORM_EQ_0] THEN
ASM SET_TAC[];
ALL_TAC] THEN
REWRITE_TAC[IN_INTER; IN_CBALL_0] THEN
REPEAT(DISCH_THEN(CONJUNCTS_THEN2 STRIP_ASSUME_TAC MP_TAC)) THEN
DISCH_THEN(fun th -> MP_TAC th THEN
MP_TAC(AP_TERM `proj:real^N->real^N` th)) THEN
ASM_SIMP_TAC[NORM_POS_LT; VECTOR_MUL_RCANCEL] THEN ASM SET_TAC[]] THEN
MATCH_MP_TAC SUBSET_ANTISYM THEN CONJ_TAC THENL
[REWRITE_TAC[SUBSET; FORALL_IN_IMAGE; IN_INTER; IN_CBALL_0] THEN
X_GEN_TAC `x:real^N` THEN ASM_CASES_TAC `x:real^N = vec 0` THEN
ASM_REWRITE_TAC[NORM_0; VECTOR_MUL_LZERO; IN_INTER] THEN
REWRITE_TAC[IN_CBALL_0; REAL_LE_LT] THEN STRIP_TAC THENL
[MATCH_MP_TAC(REWRITE_RULE[SUBSET] RELATIVE_INTERIOR_SUBSET) THEN
FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[NORM_POS_LE] THEN
ASM SET_TAC[];
ASM_REWRITE_TAC[VECTOR_MUL_LID] THEN ASM SET_TAC[]];
ALL_TAC] THEN
REWRITE_TAC[SUBSET; IN_IMAGE; IN_CBALL_0; IN_INTER] THEN
X_GEN_TAC `x:real^N` THEN DISCH_TAC THEN
ASM_CASES_TAC `x:real^N = vec 0` THENL
[EXISTS_TAC `vec 0:real^N` THEN
ASM_SIMP_TAC[NORM_0; VECTOR_MUL_LZERO; HULL_INC; REAL_POS];
ALL_TAC] THEN
SUBGOAL_THEN
`!x. x IN usph ==> ~((surf:real^N->real^N) x = vec 0)`
ASSUME_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
EXISTS_TAC `inv(norm(surf(proj x:real^N):real^N)) % x:real^N` THEN
FIRST_ASSUM(fun th -> GEN_REWRITE_TAC LAND_CONV [GSYM th]) THEN
REWRITE_TAC[GSYM CONJ_ASSOC] THEN
ASM (CONV_TAC o GEN_SIMPLIFY_CONV TOP_DEPTH_SQCONV (basic_ss []) 5)
[NORM_POS_LT; REAL_LT_INV_EQ; HULL_INC; REAL_LT_MUL; NORM_MUL;
REAL_ABS_INV; REAL_ABS_NORM] THEN
REPEAT CONJ_TAC THENL
[MATCH_MP_TAC(REAL_FIELD `~(y = &0) ==> x = (inv y * x) * y`) THEN
ASM_SIMP_TAC[NORM_EQ_0; HULL_INC];
ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
ASM (CONV_TAC o GEN_SIMPLIFY_CONV TOP_DEPTH_SQCONV (basic_ss []) 5)
[GSYM real_div; REAL_LE_LDIV_EQ; NORM_POS_LT; HULL_INC; REAL_MUL_LID] THEN
FIRST_X_ASSUM(MP_TAC o SPECL
[`x:real^N`; `norm(surf(proj x:real^N):real^N) / norm(x:real^N)`]) THEN
ASM_SIMP_TAC[REAL_LE_DIV; NORM_POS_LE; REAL_LT_LDIV_EQ; NORM_POS_LT] THEN
GEN_REWRITE_TAC LAND_CONV [GSYM CONTRAPOS_THM] THEN
REWRITE_TAC[REAL_NOT_LT; REAL_MUL_LID] THEN DISCH_THEN MATCH_MP_TAC THEN
SUBGOAL_THEN
`norm(surf(proj x)) / norm x % x:real^N = surf(proj x:real^N)`
SUBST1_TAC THENL
[FIRST_X_ASSUM(fun th -> GEN_REWRITE_TAC I [GSYM th]) THEN
ASM (CONV_TAC o GEN_SIMPLIFY_CONV TOP_DEPTH_SQCONV (basic_ss []) 5)
[NORM_POS_LT; REAL_LT_INV_EQ; HULL_INC; REAL_LT_MUL; NORM_MUL;
REAL_ABS_INV; REAL_ABS_NORM; REAL_ABS_DIV; REAL_LT_DIV;
REAL_DIV_RMUL; NORM_EQ_0];
FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (SET_RULE
`IMAGE f s SUBSET t DIFF u ==> x IN s ==> ~(f x IN u)`)) THEN
ASM_SIMP_TAC[HULL_INC]];
GEN_REWRITE_TAC LAND_CONV [GSYM VECTOR_ADD_LID] THEN
MATCH_MP_TAC IN_AFFINE_ADD_MUL THEN
ASM_SIMP_TAC[AFFINE_AFFINE_HULL; VECTOR_ADD_LID; HULL_INC]]);;
let HOMEOMORPHIC_CONVEX_COMPACT_SETS,
HOMEOMORPHIC_RELATIVE_FRONTIERS_CONVEX_BOUNDED_SETS = (CONJ_PAIR o prove)
(`(!s:real^M->bool t:real^N->bool.
convex s /\ compact s /\ convex t /\ compact t /\ aff_dim s = aff_dim t
==> s homeomorphic t) /\
(!s:real^M->bool t:real^N->bool.
convex s /\ bounded s /\ convex t /\ bounded t /\ aff_dim s = aff_dim t
==> relative_frontier s homeomorphic relative_frontier t)`,
(* ------------------------------------------------------------------------- *)
(* More about affine dimension of special sets. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Deducing convexity from midpoint convexity in common cases. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Slightly shaper separating/supporting hyperplane results. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Containment of rays in unbounded convex sets. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Explicit formulas for interior and relative interior of convex hull. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Similar results for closure and (relative or absolute) frontier. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Similar things in special case (could use above as lemmas here instead). *)
(* ------------------------------------------------------------------------- *)