(* ========================================================================= *)
(* 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`]);;
let AFFINE_ALT = prove
(`affine s <=> !x y u. x
IN s /\ y
IN s ==> ((&1 - u) % x + u % y)
IN s`,
REWRITE_TAC[affine] THEN
MESON_TAC[REAL_ARITH `(u + v = &1) <=> (u = &1 - v)`]);;
let AFFINE_SCALING = prove
(`!s c. affine s ==> affine (
IMAGE (\x. c % x) s)`,
REWRITE_TAC[affine;
IN_IMAGE] THEN REPEAT STRIP_TAC THEN
ASM_REWRITE_TAC[VECTOR_ARITH
`u % c % x + v % c % y = c % (u % x + v % y)`] THEN
ASM_MESON_TAC[]);;
let AFFINE_NEGATIONS = prove
(`!s. affine s ==> affine (
IMAGE (--) s)`,
REWRITE_TAC[affine;
IN_IMAGE] THEN REPEAT STRIP_TAC THEN
ASM_REWRITE_TAC[VECTOR_ARITH
`u % --x + v % --y = --(u % x + v % y)`] THEN
ASM_MESON_TAC[]);;
let AFFINE_SUMS = prove
(`!s t. affine s /\ affine t ==> affine {x + y | x
IN s /\ y
IN t}`,
REWRITE_TAC[affine;
IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN
ASM_REWRITE_TAC[VECTOR_ARITH
`u % (a + b) + v % (c + d) = (u % a + v % c) + (u % b + v % d)`] THEN
ASM_MESON_TAC[]);;
let AFFINE_DIFFERENCES = prove
(`!s t. affine s /\ affine t ==> affine {x - y | x
IN s /\ y
IN t}`,
REWRITE_TAC[affine;
IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN
ASM_REWRITE_TAC[VECTOR_ARITH
`u % (a - b) + v % (c - d) = (u % a + v % c) - (u % b + v % d)`] THEN
ASM_MESON_TAC[]);;
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);;
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_HULL_INDEXED = prove
(`!s. affine hull s =
{y:real^N | ?k u x. (!i. 1 <= i /\ i <= k ==> x i
IN s) /\
(sum (1..k) u = &1) /\
(vsum (1..k) (\i. u i % x i) = y)}`,
let AFFINE = prove
(`!V:real^N->bool.
affine V <=>
!(s:real^N->bool) (u:real^N->real).
FINITE s /\ ~(s = {}) /\ s
SUBSET V /\ sum s u = &1
==> vsum s (\x. u x % x)
IN V`,
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);;
let AFFINE_HULL_FINITE = prove
(`!s:real^N->bool.
affine hull s = {y | ?u. sum s u = &1 /\ vsum s (\v. u v % v) = y}`,
GEN_TAC THEN GEN_REWRITE_TAC I [
EXTENSION] THEN
REWRITE_TAC[
AFFINE_HULL_EXPLICIT;
IN_ELIM_THM] THEN
X_GEN_TAC `x:real^N` THEN EQ_TAC THEN REWRITE_TAC[
LEFT_IMP_EXISTS_THM] THENL
[MAP_EVERY X_GEN_TAC [`t:real^N->bool`; `f:real^N->real`] THEN
STRIP_TAC THEN
EXISTS_TAC `\x:real^N. if x
IN t then f x else &0` THEN
REWRITE_TAC[
COND_RAND;
COND_RATOR;
VECTOR_MUL_LZERO] THEN
REWRITE_TAC[GSYM
SUM_RESTRICT_SET; GSYM
VSUM_RESTRICT_SET] THEN
ASM_SIMP_TAC[SET_RULE `t
SUBSET s ==> {x | x
IN s /\ x
IN t} = t`];
X_GEN_TAC `f:real^N->real` THEN
ASM_CASES_TAC `s:real^N->bool = {}` THEN
ASM_REWRITE_TAC[
SUM_CLAUSES; REAL_OF_NUM_EQ; ARITH] THEN STRIP_TAC THEN
EXISTS_TAC `support (+) (f:real^N->real) s` THEN
EXISTS_TAC `f:real^N->real` THEN
MP_TAC(ASSUME `sum s (f:real^N->real) = &1`) THEN
GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [sum] THEN
REWRITE_TAC[iterate] THEN COND_CASES_TAC THEN
ASM_REWRITE_TAC[
NEUTRAL_REAL_ADD; REAL_OF_NUM_EQ; ARITH] THEN
DISCH_THEN(K ALL_TAC) THEN
UNDISCH_TAC `sum s (f:real^N->real) = &1` THEN
GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [GSYM
SUM_SUPPORT] THEN
ASM_CASES_TAC `support (+) (f:real^N->real) s = {}` THEN
ASM_SIMP_TAC[
SUM_CLAUSES; REAL_OF_NUM_EQ; ARITH] THEN
DISCH_TAC THEN REWRITE_TAC[
SUPPORT_SUBSET] THEN
FIRST_X_ASSUM(fun th -> GEN_REWRITE_TAC RAND_CONV [GSYM th]) THEN
CONV_TAC SYM_CONV THEN MATCH_MP_TAC
VSUM_SUPERSET THEN
REWRITE_TAC[
SUPPORT_SUBSET] THEN
REWRITE_TAC[support;
IN_ELIM_THM;
NEUTRAL_REAL_ADD] THEN
MESON_TAC[
VECTOR_MUL_LZERO]]);;
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]]]);;
let AFFINE_HULL_FINITE_STEP = prove
(`((?u. sum {} u = w /\ vsum {} (\x. u(x) % x) = y) <=>
w = &0 /\ y = vec 0) /\
(
FINITE(s:real^N->bool)
==> ((?u. sum (a
INSERT s) u = w /\
vsum (a
INSERT s) (\x. u(x) % x) = y) <=>
?v u. sum s u = w - v /\
vsum s (\x. u(x) % x) = y - v % a))`,
let AFFINE_HULL_EQ_SING = prove
(`!s a:real^N. affine hull s = {a} <=> s = {a}`,
REPEAT GEN_TAC THEN ASM_CASES_TAC `s:real^N->bool = {}` THEN
ASM_REWRITE_TAC[
AFFINE_HULL_EMPTY] THEN
EQ_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[
AFFINE_HULL_SING] THEN
MATCH_MP_TAC(SET_RULE `~(s = {}) /\ s
SUBSET {a} ==> s = {a}`) THEN
ASM_REWRITE_TAC[] THEN FIRST_X_ASSUM(SUBST1_TAC o SYM) THEN
REWRITE_TAC[
HULL_SUBSET]);;
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]);;
let CONVEX_VSUM = prove
(`!s k u x:A->real^N.
FINITE k /\ convex s /\ sum k u = &1 /\
(!i. i
IN k ==> &0 <= u i /\ x i
IN s)
==> vsum k (\i. u i % x i)
IN s`,
let CONVEX_VSUM_STRONG = prove
(`!s k u x:A->real^N.
FINITE k /\
convex s /\
sum k u = &1 /\
(!i. i
IN k ==> &0 <= u i /\ (u i = &0 \/ x i
IN s))
==> vsum k (\i. u i % x i)
IN s`,
REPEAT STRIP_TAC THEN
SUBGOAL_THEN
`vsum k (\i. u i % (x:A->real^N) i) =
vsum {i | i
IN k /\ ~(u i = &0)} (\i. u i % x i)`
SUBST1_TAC THENL
[MATCH_MP_TAC
VSUM_SUPERSET THEN REWRITE_TAC[
VECTOR_MUL_EQ_0] THEN
SET_TAC[];
MATCH_MP_TAC
CONVEX_VSUM THEN
ASM_SIMP_TAC[
FINITE_RESTRICT;
IN_ELIM_THM] THEN
CONJ_TAC THENL [ALL_TAC; ASM_MESON_TAC[]] THEN
FIRST_X_ASSUM(SUBST1_TAC o SYM) THEN
CONV_TAC SYM_CONV THEN MATCH_MP_TAC
SUM_SUPERSET THEN ASM SET_TAC[]]);;
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);;
let CONIC_CONTAINS_0 = prove
(`!s:real^N->bool. conic s ==> (vec 0
IN s <=> ~(s = {}))`,
REPEAT STRIP_TAC THEN EQ_TAC THENL [SET_TAC[]; ALL_TAC] THEN
REWRITE_TAC[GSYM
MEMBER_NOT_EMPTY] THEN
DISCH_THEN(X_CHOOSE_TAC `x:real^N`) THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [conic]) THEN
DISCH_THEN(MP_TAC o SPECL [`x:real^N`; `&0`]) THEN
ASM_REWRITE_TAC[
REAL_POS;
VECTOR_MUL_LZERO]);;
let SEPARATE_CLOSED_CONES = prove
(`!c d:real^N->bool.
conic c /\ closed c /\ conic d /\ closed d /\ c
INTER d
SUBSET {vec 0}
==> ?e. &0 < e /\
!x y. x
IN c /\ y
IN d
==> dist(x,y) >= e * max (norm x) (norm y)`,
SUBGOAL_THEN
`!c d:real^N->bool.
conic c /\ closed c /\ conic d /\ closed d /\ c
INTER d
SUBSET {vec 0}
==> ?e. &0 < e /\
!x y. x
IN c /\ y
IN d ==> dist(x,y)
>= e * norm x`
ASSUME_TAC THENL
[REPEAT STRIP_TAC THEN REWRITE_TAC[
real_ge] THEN
MP_TAC(ISPECL [`c
INTER sphere(vec 0:real^N,&1)`; `d:real^N->bool`]
SEPARATE_COMPACT_CLOSED) THEN
ASM_SIMP_TAC[
CLOSED_INTER_COMPACT;
COMPACT_SPHERE] THEN ANTS_TAC THENL
[FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (SET_RULE
`c
INTER d
SUBSET {a} ==> ~(a
IN s) ==> (c
INTER s)
INTER d = {}`)) THEN
REWRITE_TAC[
IN_SPHERE_0;
NORM_0] THEN REAL_ARITH_TAC;
MATCH_MP_TAC
MONO_EXISTS THEN X_GEN_TAC `e:real` THEN
REWRITE_TAC[
IN_INTER;
IN_SPHERE_0] THEN STRIP_TAC THEN
ASM_REWRITE_TAC[] THEN
MAP_EVERY X_GEN_TAC [`x:real^N`; `y:real^N`] THEN STRIP_TAC THEN
ASM_CASES_TAC `x:real^N = vec 0` THEN
ASM_REWRITE_TAC[
DIST_POS_LE;
REAL_MUL_RZERO;
NORM_0] THEN
FIRST_X_ASSUM(MP_TAC o SPECL
[`inv(norm x) % x:real^N`; `inv(norm(x:real^N)) % y:real^N`]) THEN
REWRITE_TAC[dist;
NORM_MUL; GSYM
VECTOR_SUB_LDISTRIB] THEN
REWRITE_TAC[REAL_ARITH `abs x * a = a * abs x`] THEN
REWRITE_TAC[
REAL_ABS_INV; GSYM
real_div;
REAL_ABS_NORM] THEN
ASM_SIMP_TAC[
REAL_LE_RDIV_EQ;
NORM_POS_LT] THEN
DISCH_THEN MATCH_MP_TAC THEN
ASM_SIMP_TAC[
REAL_DIV_REFL;
NORM_EQ_0] THEN
RULE_ASSUM_TAC(REWRITE_RULE[conic]) THEN
CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
ASM_SIMP_TAC[
REAL_LE_INV_EQ;
NORM_POS_LE]];
REPEAT STRIP_TAC THEN FIRST_X_ASSUM(fun th ->
MP_TAC(SPECL [`c:real^N->bool`; `d:real^N->bool`] th) THEN
MP_TAC(SPECL [`d:real^N->bool`; `c:real^N->bool`] th)) THEN
ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC[
INTER_COMM] THEN
ASM_REWRITE_TAC[
LEFT_IMP_EXISTS_THM;
real_ge] THEN
X_GEN_TAC `d:real` THEN STRIP_TAC THEN
X_GEN_TAC `e:real` THEN STRIP_TAC THEN
EXISTS_TAC `min d e:real` THEN ASM_REWRITE_TAC[
REAL_LT_MIN] THEN
MAP_EVERY X_GEN_TAC [`x:real^N`; `y:real^N`] THEN STRIP_TAC THEN
REWRITE_TAC[
real_max] THEN COND_CASES_TAC THEN
MATCH_MP_TAC
REAL_LE_TRANS THENL
[EXISTS_TAC `d * norm(y:real^N)` THEN ONCE_REWRITE_TAC[
DIST_SYM];
EXISTS_TAC `e * norm(x:real^N)`] THEN
ASM_SIMP_TAC[] THEN MATCH_MP_TAC
REAL_LE_RMUL THEN NORM_ARITH_TAC]);;
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]);;
let COPLANAR_LINEAR_IMAGE = prove
(`!f:real^M->real^N s. coplanar s /\ linear f ==> coplanar(
IMAGE f s)`,
REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
REWRITE_TAC[coplanar;
LEFT_IMP_EXISTS_THM] THEN
MAP_EVERY X_GEN_TAC [`a:real^M`; `b:real^M`; `c:real^M`] THEN STRIP_TAC THEN
MAP_EVERY EXISTS_TAC
[`(f:real^M->real^N) a`; `(f:real^M->real^N) b`; `(f:real^M->real^N) c`] THEN
REWRITE_TAC[SET_RULE `{f a,f b,f c} =
IMAGE f {a,b,c}`] THEN
ASM_SIMP_TAC[
AFFINE_HULL_LINEAR_IMAGE;
IMAGE_SUBSET]);;
let COLLINEAR_3_IN_AFFINE_HULL = prove
(`!v0 v1 x:real^N.
~(v1 = v0)
==> (collinear {v0,v1,x} <=> x
IN affine hull {v0,v1})`,
REPEAT GEN_TAC THEN GEOM_ORIGIN_TAC `v0:real^N` THEN
REWRITE_TAC[
COLLINEAR_LEMMA;
AFFINE_HULL_2] THEN REPEAT STRIP_TAC THEN
ASM_REWRITE_TAC[
VECTOR_MUL_RZERO;
VECTOR_ADD_LID;
IN_ELIM_THM] THEN
ASM_CASES_TAC `x:real^N = vec 0` THEN ASM_REWRITE_TAC[] THENL
[MAP_EVERY EXISTS_TAC [`&1`; `&0`] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
VECTOR_ARITH_TAC;
MESON_TAC[REAL_ARITH `u + v = &1 <=> u = &1 - v`]]);;
let CLOPEN = prove
(`!s. closed s /\ open s <=> s = {} \/ s = (:real^N)`,
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 CLOSED_INTERVAL_EQ = prove
(`(!a b:real^N. closed(interval[a,b])) /\
(!a b:real^N. closed(interval(a,b)) <=> interval(a,b) = {})`,
let OPEN_INTERVAL_EQ = prove
(`(!a b:real^N. open(interval[a,b]) <=> interval[a,b] = {}) /\
(!a b:real^N. open(interval(a,b)))`,
let COMPACT_INTERVAL_EQ = prove
(`(!a b:real^N. compact(interval[a,b])) /\
(!a b:real^N. compact(interval(a,b)) <=> interval(a,b) = {})`,
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)`,
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`]);;
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)`]);;
let CONNECTED_UNION_CLOPEN_IN_COMPLEMENT = prove
(`!s t u:real^N->bool.
connected s /\ connected u /\ s
SUBSET u /\
open_in (subtopology euclidean (u
DIFF s)) t /\
closed_in (subtopology euclidean (u
DIFF s)) t
==> connected (s
UNION t)`,
MAP_EVERY X_GEN_TAC
[`c:real^N->bool`; `h:real^N->bool`; `s:real^N->bool`] THEN
STRIP_TAC THEN
REWRITE_TAC[
CONNECTED_CLOSED_IN_EQ;
NOT_EXISTS_THM] THEN
MATCH_MP_TAC(MESON[]
`!Q. (!x y. P x y <=> P y x) /\
(!x y. P x y ==> Q x \/ Q y) /\
(!x y. P x y /\ Q x ==> F)
==> (!x y. ~(P x y))`) THEN
EXISTS_TAC `\x:real^N->bool. c
SUBSET x` THEN
CONJ_TAC THENL [MESON_TAC[
INTER_COMM;
UNION_COMM]; ALL_TAC] THEN
REWRITE_TAC[] THEN CONJ_TAC THEN
MAP_EVERY X_GEN_TAC [`h1:real^N->bool`; `h2:real^N->bool`] THENL
[STRIP_TAC THEN UNDISCH_TAC `connected(c:real^N->bool)` THEN
REWRITE_TAC[
CONNECTED_CLOSED_IN;
NOT_EXISTS_THM] THEN
DISCH_THEN(MP_TAC o
SPECL [`c
INTER h1:real^N->bool`; `c
INTER h2:real^N->bool`]) THEN
MATCH_MP_TAC(TAUT
`(p /\ q) /\ (~r ==> s) ==> ~(p /\ q /\ r) ==> s`) THEN
CONJ_TAC THENL [ALL_TAC; ASM SET_TAC[]] THEN CONJ_TAC THENL
[UNDISCH_TAC
`
closed_in(subtopology euclidean (c
UNION h)) (h1:real^N->bool)`;
UNDISCH_TAC
`
closed_in(subtopology euclidean (c
UNION h)) (h2:real^N->bool)`] THEN
REWRITE_TAC[
CLOSED_IN_CLOSED] THEN MATCH_MP_TAC
MONO_EXISTS THEN
ASM SET_TAC[];
STRIP_TAC THEN
FIRST_ASSUM(ASSUME_TAC o CONJUNCT1 o GEN_REWRITE_RULE I [
open_in]) THEN
SUBGOAL_THEN `(h2:real^N->bool)
SUBSET h` ASSUME_TAC THENL
[ASM SET_TAC[]; ALL_TAC] THEN
UNDISCH_TAC `connected(s:real^N->bool)` THEN
REWRITE_TAC[
CONNECTED_CLOPEN] THEN
DISCH_THEN(MP_TAC o SPEC `h2:real^N->bool`) THEN REWRITE_TAC[NOT_IMP] THEN
CONJ_TAC THENL [ALL_TAC; ASM SET_TAC[]] THEN
SUBGOAL_THEN `s:real^N->bool = (s
DIFF c)
UNION (c
UNION h)`
SUBST1_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN CONJ_TAC THENL
[MATCH_MP_TAC
OPEN_IN_SUBTOPOLOGY_UNION THEN
MATCH_MP_TAC(TAUT `q /\ (q ==> p) ==> p /\ q`) THEN CONJ_TAC THENL
[REWRITE_TAC[
OPEN_IN_CLOSED_IN_EQ;
TOPSPACE_EUCLIDEAN_SUBTOPOLOGY] THEN
CONJ_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
SUBGOAL_THEN `(c
UNION h)
DIFF h2:real^N->bool = h1`
(fun th -> ASM_REWRITE_TAC[th]) THEN ASM SET_TAC[];
DISCH_TAC THEN MATCH_MP_TAC
OPEN_IN_TRANS THEN
EXISTS_TAC `h:real^N->bool` THEN ASM_REWRITE_TAC[] THEN
UNDISCH_TAC
`
open_in(subtopology euclidean (c
UNION h)) (h2:real^N->bool)` THEN
REWRITE_TAC[
OPEN_IN_OPEN] THEN MATCH_MP_TAC
MONO_EXISTS THEN
ASM SET_TAC[]];
MATCH_MP_TAC
CLOSED_IN_SUBTOPOLOGY_UNION THEN ASM_REWRITE_TAC[] THEN
MATCH_MP_TAC
CLOSED_IN_TRANS THEN EXISTS_TAC `h:real^N->bool` THEN
ASM_REWRITE_TAC[] THEN
UNDISCH_TAC
`
closed_in(subtopology euclidean (c
UNION h)) (h2:real^N->bool)` THEN
REWRITE_TAC[
CLOSED_IN_CLOSED] THEN MATCH_MP_TAC
MONO_EXISTS THEN
ASM SET_TAC[]]]);;
let CONVEX_SCALING = prove
(`!s c. convex s ==> convex (
IMAGE (\x. c % x) s)`,
REWRITE_TAC[convex;
IN_IMAGE] THEN REPEAT STRIP_TAC THEN
ASM_REWRITE_TAC[VECTOR_ARITH
`u % c % x + v % c % y = c % (u % x + v % y)`] THEN
ASM_MESON_TAC[]);;
let CONVEX_NEGATIONS = prove
(`!s. convex s ==> convex (
IMAGE (--) s)`,
REWRITE_TAC[convex;
IN_IMAGE] THEN REPEAT STRIP_TAC THEN
ASM_REWRITE_TAC[VECTOR_ARITH
`u % --x + v % --y = --(u % x + v % y)`] THEN
ASM_MESON_TAC[]);;
let CONVEX_SUMS = prove
(`!s t. convex s /\ convex t ==> convex {x + y | x
IN s /\ y
IN t}`,
REWRITE_TAC[convex;
IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN
ASM_REWRITE_TAC[VECTOR_ARITH
`u % (a + b) + v % (c + d) = (u % a + v % c) + (u % b + v % d)`] THEN
ASM_MESON_TAC[]);;
let CONVEX_DIFFERENCES = prove
(`!s t. convex s /\ convex t ==> convex {x - y | x
IN s /\ y
IN t}`,
REWRITE_TAC[convex;
IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN
ASM_REWRITE_TAC[VECTOR_ARITH
`u % (a - b) + v % (c - d) = (u % a + v % c) - (u % b + v % d)`] THEN
ASM_MESON_TAC[]);;
let CONVEX_HULL_EQ_SING = prove
(`!s a:real^N. convex hull s = {a} <=> s = {a}`,
REPEAT GEN_TAC THEN ASM_CASES_TAC `s:real^N->bool = {}` THEN
ASM_REWRITE_TAC[
CONVEX_HULL_EMPTY] THEN
EQ_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[
CONVEX_HULL_SING] THEN
MATCH_MP_TAC(SET_RULE `~(s = {}) /\ s
SUBSET {a} ==> s = {a}`) THEN
ASM_REWRITE_TAC[] THEN FIRST_X_ASSUM(SUBST1_TAC o SYM) THEN
REWRITE_TAC[
HULL_SUBSET]);;
let CONVEX_HULL_INSERT = prove
(`!s a. ~(s = {})
==> (convex hull (a
INSERT s) =
{x:real^N | ?u v b. &0 <= u /\ &0 <= v /\ (u + v = &1) /\
b
IN (convex hull s) /\
(x = u % a + v % b)})`,
let CONVEX_HULL_INDEXED = prove
(`!s. convex hull s =
{y:real^N | ?k u x. (!i. 1 <= i /\ i <= k ==> &0 <= u i /\ x i
IN s) /\
(sum (1..k) u = &1) /\
(vsum (1..k) (\i. u i % x i) = y)}`,
let CONVEX_HULL_FINITE = prove
(`!s:real^N->bool.
convex hull s =
{y | ?u. (!x. x
IN s ==> &0 <= u x) /\
sum s u = &1 /\
vsum s (\x. u x % x) = y}`,
GEN_TAC THEN GEN_REWRITE_TAC I [
EXTENSION] THEN
REWRITE_TAC[
CONVEX_HULL_EXPLICIT;
IN_ELIM_THM] THEN
X_GEN_TAC `x:real^N` THEN EQ_TAC THEN REWRITE_TAC[
LEFT_IMP_EXISTS_THM] THENL
[MAP_EVERY X_GEN_TAC [`t:real^N->bool`; `f:real^N->real`] THEN
STRIP_TAC THEN
EXISTS_TAC `\x:real^N. if x
IN t then f x else &0` THEN
REWRITE_TAC[
COND_RAND;
COND_RATOR;
VECTOR_MUL_LZERO] THEN
REWRITE_TAC[GSYM
SUM_RESTRICT_SET; GSYM
VSUM_RESTRICT_SET] THEN
ASM_SIMP_TAC[SET_RULE `t
SUBSET s ==> {x | x
IN s /\ x
IN t} = t`] THEN
REWRITE_TAC[
REAL_LE_REFL;
COND_ID];
X_GEN_TAC `f:real^N->real` THEN
ASM_CASES_TAC `s:real^N->bool = {}` THEN
ASM_REWRITE_TAC[
SUM_CLAUSES; REAL_OF_NUM_EQ; ARITH] THEN STRIP_TAC THEN
EXISTS_TAC `support (+) (f:real^N->real) s` THEN
EXISTS_TAC `f:real^N->real` THEN
MP_TAC(ASSUME `sum s (f:real^N->real) = &1`) THEN
GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [sum] THEN
REWRITE_TAC[iterate] THEN COND_CASES_TAC THEN
ASM_REWRITE_TAC[
NEUTRAL_REAL_ADD; REAL_OF_NUM_EQ; ARITH] THEN
DISCH_THEN(K ALL_TAC) THEN
UNDISCH_TAC `sum s (f:real^N->real) = &1` THEN
GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [GSYM
SUM_SUPPORT] THEN
ASM_CASES_TAC `support (+) (f:real^N->real) s = {}` THEN
ASM_SIMP_TAC[
SUM_CLAUSES; REAL_OF_NUM_EQ; ARITH] THEN
DISCH_TAC THEN REWRITE_TAC[
SUPPORT_SUBSET] THEN CONJ_TAC THENL
[ASM_SIMP_TAC[support;
IN_ELIM_THM]; ALL_TAC] THEN
FIRST_X_ASSUM(fun th -> GEN_REWRITE_TAC RAND_CONV [GSYM th]) THEN
CONV_TAC SYM_CONV THEN MATCH_MP_TAC
VSUM_SUPERSET THEN
REWRITE_TAC[
SUPPORT_SUBSET] THEN
REWRITE_TAC[support;
IN_ELIM_THM;
NEUTRAL_REAL_ADD] THEN
MESON_TAC[
VECTOR_MUL_LZERO]]);;
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))`,
let CONVEX_HULL_2 = prove
(`!a b. convex hull {a,b} =
{u % a + v % b | &0 <= u /\ &0 <= v /\ u + v = &1}`,
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 = prove
(`convex hull {a,b,c} =
{ u % a + v % b + w % c |
&0 <= u /\ &0 <= v /\ &0 <= w /\ u + v + w = &1}`,
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 lemma1 = prove
(`!u v x y:real^M z:real^N.
u + v = &1
==> pastecart z (u % x + v % y) =
u % pastecart z x + v % pastecart z y /\
pastecart (u % x + v % y) z =
u % pastecart x z + v % pastecart y z`,
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]);;
let AFFINE_HULL_EQ_SPAN = prove
(`!s:real^N->bool. (vec 0)
IN affine hull s ==> affine hull s = span s`,
GEN_TAC THEN DISCH_TAC THEN MATCH_MP_TAC
SUBSET_ANTISYM THEN
REWRITE_TAC[
AFFINE_HULL_SUBSET_SPAN] THEN
REWRITE_TAC[
SUBSET] THEN MATCH_MP_TAC
SPAN_INDUCT THEN
ASM_REWRITE_TAC[
SUBSET; subspace;
IN_ELIM_THM;
HULL_INC] THEN
REPEAT STRIP_TAC THENL
[SUBST1_TAC(VECTOR_ARITH
`x + y:real^N = &2 % (&1 / &2 % x + &1 / &2 % y) + --(&1) % vec 0`) THEN
MATCH_MP_TAC(REWRITE_RULE[affine]
AFFINE_AFFINE_HULL) THEN
CONV_TAC REAL_RAT_REDUCE_CONV THEN ASM_REWRITE_TAC[] THEN
MATCH_MP_TAC(REWRITE_RULE[affine]
AFFINE_AFFINE_HULL) THEN
CONV_TAC REAL_RAT_REDUCE_CONV THEN ASM_REWRITE_TAC[];
SUBST1_TAC(VECTOR_ARITH
`c % x:real^N = c % x + (&1 - c) % vec 0`) THEN
MATCH_MP_TAC(REWRITE_RULE[affine]
AFFINE_AFFINE_HULL) THEN
ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC]);;
let DEPENDENT_IMP_AFFINE_DEPENDENT = prove
(`!a:real^N s. dependent {x - a | x
IN s} /\ ~(a
IN s)
==>
affine_dependent(a
INSERT s)`,
REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
REWRITE_TAC[
DEPENDENT_EXPLICIT;
AFFINE_DEPENDENT_EXPLICIT] THEN
REWRITE_TAC[
SIMPLE_IMAGE;
CONJ_ASSOC;
FINITE_SUBSET_IMAGE] THEN
REWRITE_TAC[
LEFT_AND_EXISTS_THM] THEN REWRITE_TAC[GSYM
CONJ_ASSOC] THEN
GEN_REWRITE_TAC LAND_CONV [
SWAP_EXISTS_THM] THEN
GEN_REWRITE_TAC (LAND_CONV o BINDER_CONV) [
SWAP_EXISTS_THM] THEN
REWRITE_TAC[TAUT `a /\ x =
IMAGE f s /\ b <=> x =
IMAGE f s /\ a /\ b`] THEN
REWRITE_TAC[
UNWIND_THM2;
EXISTS_IN_IMAGE] THEN
DISCH_THEN(X_CHOOSE_THEN `u:real^N->real` (X_CHOOSE_THEN `t:real^N->bool`
STRIP_ASSUME_TAC)) THEN
FIRST_X_ASSUM(MP_TAC o check (is_eq o concl)) THEN
ASM_SIMP_TAC[
VSUM_IMAGE; VECTOR_ARITH `x - a:real^N = y - a <=> x = y`] THEN
ASM_SIMP_TAC[
o_DEF;
VECTOR_SUB_LDISTRIB;
VSUM_SUB;
VSUM_RMUL] THEN
STRIP_TAC THEN
MAP_EVERY EXISTS_TAC
[`(a:real^N)
INSERT t`;
`\x. if x = a then --sum t (\x. u (x - a))
else (u:real^N->real) (x - a)`] THEN
ASM_REWRITE_TAC[
FINITE_INSERT;
SUBSET_REFL] THEN
ASM_SIMP_TAC[
SUM_CLAUSES;
VSUM_CLAUSES] THEN
CONJ_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
COND_CASES_TAC THEN ASM_REWRITE_TAC[] THENL [ASM SET_TAC[]; ALL_TAC] THEN
REPEAT CONJ_TAC THENL
[MATCH_MP_TAC(REAL_ARITH `x = y ==> --x + y = &0`) THEN
MATCH_MP_TAC
SUM_EQ THEN ASM_MESON_TAC[];
EXISTS_TAC `x:real^N` THEN CONJ_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[];
MATCH_MP_TAC(VECTOR_ARITH
`!s. s - t % a = vec 0 /\ s = u ==> --t % a + u = vec 0`) THEN
EXISTS_TAC `vsum t (\x:real^N. u(x - a) % x)` THEN
ASM_REWRITE_TAC[] THEN MATCH_MP_TAC
VSUM_EQ THEN
REPEAT STRIP_TAC THEN REWRITE_TAC[] THEN COND_CASES_TAC THEN
ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[]]);;
let AFFINE_TRANSLATION_UNIQUE_SUBSPACE = prove
(`!t:real^N->bool.
affine t /\ ~(t = {}) <=>
?!s. ?a. subspace s /\ t =
IMAGE (\x. a + x) s`,
GEN_TAC THEN REWRITE_TAC[
AFFINE_TRANSLATION_SUBSPACE] THEN
MATCH_MP_TAC(MESON[]
`(!a a' s s'. P s a /\ P s' a' ==> s = s')
==> ((?a s. P s a) <=> (?!s. ?a. P s a))`) THEN
REPEAT GEN_TAC THEN
REPEAT(DISCH_THEN(CONJUNCTS_THEN2 STRIP_ASSUME_TAC MP_TAC)) THEN
DISCH_THEN(fun th -> ASSUME_TAC th THEN MP_TAC th) THEN
ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC[
TRANSLATION_GALOIS] THEN
DISCH_THEN SUBST1_TAC THEN CONV_TAC SYM_CONV THEN
REWRITE_TAC[GSYM
IMAGE_o;
o_DEF;
VECTOR_ADD_ASSOC] THEN
MATCH_MP_TAC
SUBSPACE_TRANSLATION_SELF THEN ASM_REWRITE_TAC[] THEN
ONCE_REWRITE_TAC[VECTOR_ARITH `--a' + a:real^N = --(a' - a)`] THEN
MATCH_MP_TAC
SUBSPACE_NEG THEN ASM_REWRITE_TAC[] THEN
UNDISCH_TAC `t =
IMAGE (\x:real^N. a' + x) s'` THEN
DISCH_THEN(MP_TAC o AP_TERM `\s. (a':real^N)
IN s`) THEN
REWRITE_TAC[
IN_IMAGE; VECTOR_ARITH `a:real^N = a + x <=> x = vec 0`] THEN
ASM_SIMP_TAC[
UNWIND_THM2;
SUBSPACE_0] THEN
REWRITE_TAC[
IN_IMAGE; VECTOR_ARITH `a':real^N = a + x <=> x = a' - a`] THEN
REWRITE_TAC[
UNWIND_THM2]);;
let AFFINE_PARALLEL_SLICE = prove
(`!s a:real^N b.
affine s
==> s
INTER {x | a dot x <= b} = {} \/ s
SUBSET {x | a dot x <= b} \/
?a' b'. ~(a' = vec 0) /\
s
INTER {x | a' dot x <= b'} = s
INTER {x | a dot x <= b} /\
s
INTER {x | a' dot x = b'} = s
INTER {x | a dot x = b} /\
!w. w
IN s ==> (w + a')
IN s`,
REPEAT STRIP_TAC THEN
ASM_CASES_TAC `s
INTER {x:real^N | a dot x = b} = {}` THENL
[MATCH_MP_TAC(TAUT `~(~p /\ ~q) ==> p \/ q \/ r`) THEN
REPEAT STRIP_TAC THEN SUBGOAL_THEN
`?u v:real^N. u
IN s /\ v
IN s /\
a dot u <= b /\ ~(a dot v <= b)`
STRIP_ASSUME_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
SUBGOAL_THEN `(a:real^N) dot u < b` ASSUME_TAC THENL
[ASM_REWRITE_TAC[
REAL_LT_LE] THEN ASM SET_TAC[]; ALL_TAC] THEN
RULE_ASSUM_TAC(REWRITE_RULE[
REAL_NOT_LE]) THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [
EXTENSION]) THEN
REWRITE_TAC[
NOT_IN_EMPTY;
IN_INTER;
NOT_FORALL_THM;
IN_ELIM_THM] THEN
EXISTS_TAC
`u + (b - a dot u) / (a dot v - a dot u) % (v - u):real^N` THEN
ASM_SIMP_TAC[
IN_AFFINE_ADD_MUL_DIFF] THEN
REWRITE_TAC[
DOT_RADD;
DOT_RMUL;
DOT_RSUB] THEN
REPEAT(POP_ASSUM MP_TAC) THEN CONV_TAC REAL_FIELD;
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM
MEMBER_NOT_EMPTY]) THEN
DISCH_THEN(X_CHOOSE_THEN `z:real^N` MP_TAC) THEN
REWRITE_TAC[
IN_INTER;
IN_ELIM_THM] THEN POP_ASSUM MP_TAC THEN
GEN_GEOM_ORIGIN_TAC `z:real^N` ["a";
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);;
let DIM_OPEN = prove
(`!s:real^N->bool. open s /\ ~(s = {}) ==> dim s = dimindex(:N)`,
let RIGID_TRANSFORMATION_BETWEEN_CONGRUENT_SETS = prove
(`!x:A->real^N y:A->real^N s.
(!i j. i
IN s /\ j
IN s ==> dist(x i,x j) = dist(y i,y j))
==> ?a f.
orthogonal_transformation f /\
!i. i
IN s ==> y i = a + f(x i)`,
let lemma = prove
(`!x:(real^N)^M y:(real^N)^M.
(!i j. 1 <= i /\ i <= dimindex(:M) /\
1 <= j /\ j <= dimindex(:M)
==> dist(x$i,x$j) = dist(y$i,y$j))
==> ?a f. orthogonal_transformation f /\
!i. 1 <= i /\ i <= dimindex(:M)
==> y$i = a + f(x$i)`,
REPEAT STRIP_TAC THEN
ABBREV_TAC `(X:real^M^N) = lambda i j. (x:real^N^M)$j$i - x$1$i` THEN
ABBREV_TAC `(Y:real^M^N) = lambda i j. (y:real^N^M)$j$i - y$1$i` THEN
SUBGOAL_THEN `transp(X:real^M^N) ** X = transp(Y:real^M^N) ** Y`
ASSUME_TAC THENL
[REWRITE_TAC[MATRIX_MUL_LTRANSP_DOT_COLUMN] THEN
MAP_EVERY EXPAND_TAC ["X";
let RIGID_TRANSFORMATION_BETWEEN_CONGRUENT_SETS_STRONG = prove
(`!x:A->real^N y:A->real^N s t.
t
SUBSET s /\ affine hull (
IMAGE y t) = affine hull (
IMAGE y s) /\
(!i j. i
IN s /\ j
IN t ==> dist(x i,x j) = dist(y i,y j))
==> ?a f.
orthogonal_transformation f /\
!i. i
IN s ==> y i = a + f(x i)`,
REPEAT STRIP_TAC THEN
MP_TAC(ISPECL [`x:A->real^N`; `y:A->real^N`; `t:A->bool`]
RIGID_TRANSFORMATION_BETWEEN_CONGRUENT_SETS) THEN
ANTS_TAC THENL [ASM_MESON_TAC[
SUBSET]; ALL_TAC] 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 `i:A` THEN DISCH_TAC THEN
SUBGOAL_THEN
`!z. z
IN affine hull (
IMAGE (y:A->real^N) t)
==> dist(z,y i) = dist(z,a + (f:real^N->real^N)(x i))`
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:A` THEN STRIP_TAC THEN MATCH_MP_TAC
EQ_TRANS THEN
EXISTS_TAC `dist(a + f(x(j:A):real^N):real^N,a + f(x i))` THEN
CONJ_TAC THENL [ALL_TAC; ASM_MESON_TAC[]] THEN
REWRITE_TAC[NORM_ARITH `dist(a + x:real^N,a + y) = dist(x,y)`] THEN
ASM_MESON_TAC[
ORTHOGONAL_TRANSFORMATION_ISOMETRY;
DIST_SYM];
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] THEN ASM_MESON_TAC[]]);;
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]);;
let IN_CONVEX_HULL_EXCHANGE_UNIQUE = prove
(`!s t t' a x:real^N.
~(
affine_dependent s) /\
a
IN convex hull s /\
t
SUBSET s /\ t'
SUBSET s /\
x
IN convex hull (a
INSERT t) /\
x
IN convex hull (a
INSERT t')
==> x
IN convex hull (a
INSERT (t
INTER t'))`,
REPEAT GEN_TAC THEN ASM_CASES_TAC `(a:real^N)
IN s` THENL
[REPEAT STRIP_TAC THEN REWRITE_TAC[SET_RULE
`a
INSERT (s
INTER t) = (a
INSERT s)
INTER (a
INSERT t)`] THEN
W(MP_TAC o PART_MATCH (rand o rand) CONVEX_HULL_INTER o rand o snd) THEN
ANTS_TAC THENL
[UNDISCH_TAC `~(
affine_dependent(s:real^N->bool))` THEN
REWRITE_TAC[CONTRAPOS_THM] THEN
MATCH_MP_TAC(REWRITE_RULE[
IMP_CONJ_ALT]
AFFINE_DEPENDENT_MONO);
DISCH_THEN(SUBST1_TAC o SYM)] THEN
ASM SET_TAC[];
ALL_TAC] THEN
DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
FIRST_ASSUM(ASSUME_TAC o MATCH_MP
AFFINE_INDEPENDENT_IMP_FINITE) THEN
REWRITE_TAC[
CONVEX_HULL_FINITE;
IN_ELIM_THM] THEN
DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_THEN `b:real^N->real` STRIP_ASSUME_TAC)
MP_TAC) THEN
REPLICATE_TAC 2 (DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
SUBGOAL_THEN `~((a:real^N)
IN t) /\ ~(a
IN t')` STRIP_ASSUME_TAC THENL
[ASM SET_TAC[]; ALL_TAC] THEN
SUBGOAL_THEN `
FINITE(t:real^N->bool) /\
FINITE(t':real^N->bool)`
STRIP_ASSUME_TAC THENL [ASM_MESON_TAC[
FINITE_SUBSET]; ALL_TAC] THEN
ASM_SIMP_TAC[
AFFINE_HULL_FINITE_STEP_GEN;
REAL_LE_ADD;
REAL_ARITH `&0 <= a / &2 <=> &0 <= a`] THEN
REWRITE_TAC[
IMP_CONJ;
LEFT_IMP_EXISTS_THM] THEN
MAP_EVERY X_GEN_TAC [`u':real`; `u:real^N->real`] THEN REPEAT DISCH_TAC THEN
MAP_EVERY X_GEN_TAC [`v':real`; `v:real^N->real`] THEN REPEAT DISCH_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:real^N->bool`) THEN
ASM_REWRITE_TAC[
SUBSET_REFL] THEN
DISCH_THEN(MP_TAC o SPEC
`\x:real^N. (if x
IN t then u x else &0) - (if x
IN t' then v x else &0) +
(u' - v') * b x`) THEN
ASM_SIMP_TAC[
SUM_ADD;
VSUM_ADD;
SUM_LMUL;
VSUM_LMUL;
VECTOR_ADD_RDISTRIB] THEN
ASM_SIMP_TAC[
SUM_SUB;
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;
SUM_0;
VSUM_0] THEN
ASM_SIMP_TAC[SET_RULE `t
SUBSET s ==> {x | x
IN s /\ x
IN t} = t`] THEN
ASM_SIMP_TAC[
SUM_ADD;
SUM_LMUL;
VSUM_ADD;
VSUM_LMUL;
VECTOR_ADD_RDISTRIB;
GSYM
VECTOR_MUL_ASSOC] 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
SUBGOAL_THEN
`(!x. x
IN s ==> (if x
IN t then u x else &0) <=
(if x
IN t' then v x else &0)) \/
(!x:real^N. x
IN s ==> (if x
IN t' then v x else &0) <=
(if x
IN t then u x else &0))`
(DISJ_CASES_THEN(LABEL_TAC "*")) THENL
[MP_TAC(REAL_ARITH `&0 <= (u' - v') \/ &0 <= (v' - u')`) THEN
MATCH_MP_TAC MONO_OR THEN CONJ_TAC THEN
DISCH_TAC THEN X_GEN_TAC `y:real^N` THEN DISCH_TAC THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [
NOT_EXISTS_THM]) THEN
DISCH_THEN(MP_TAC o SPEC `y:real^N`) THEN ASM_REWRITE_TAC[] THENL
[MATCH_MP_TAC(REAL_ARITH `&0 <= c ==> a - b + c = &0 ==> a <= b`);
MATCH_MP_TAC(REAL_ARITH `&0 <= --c ==> a - b + c = &0 ==> b <= a`)] THEN
ASM_SIMP_TAC[
REAL_LE_MUL; GSYM
REAL_MUL_LNEG;
REAL_NEG_SUB];
EXISTS_TAC `(\x. if x = a then u' else u x):real^N->real`;
EXISTS_TAC `(\x. if x = a then v' else v x):real^N->real`] THEN
ASM_SIMP_TAC[
FORALL_IN_INSERT] THEN
(CONJ_TAC THENL [ASM_MESON_TAC[
IN_INTER]; ALL_TAC]) THEN
ASM_SIMP_TAC[
SUM_CLAUSES;
VSUM_CLAUSES;
FINITE_INTER] THEN
ASM_REWRITE_TAC[
IN_INTER] THEN
REWRITE_TAC[REAL_ARITH `u' + u = &1 <=> u = &1 - u'`;
VECTOR_ARITH `u' + u:real^N = y <=> u = y - u'`] THEN
(CONJ_TAC THEN
FIRST_X_ASSUM(fun th -> GEN_REWRITE_TAC RAND_CONV [GSYM th]) 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
(CONJ_TAC THENL [ASM SET_TAC[]; ALL_TAC]) THEN
X_GEN_TAC `y:real^N` THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
ASM_REWRITE_TAC[
VECTOR_MUL_EQ_0] THEN DISCH_TAC THEN
REMOVE_THEN "*" (MP_TAC o SPEC `y:real^N`) THEN ASM_REWRITE_TAC[] THEN
REWRITE_TAC[GSYM REAL_LE_ANTISYM] THEN ASM SET_TAC[]);;
let SUBSET_HYPERPLANES = prove
(`!a b a' b'.
{x | a dot x = b}
SUBSET {x | a' dot x = b'} <=>
{x | a dot x = b} = {} \/ {x | a' dot x = b'} = (:real^N) \/
{x | a dot x = b} = {x | a' dot x = b'}`,
REPEAT GEN_TAC THEN
ASM_CASES_TAC `{x:real^N | a dot x = b} = {}` THEN
ASM_REWRITE_TAC[
EMPTY_SUBSET] THEN
ASM_CASES_TAC `{x | a' dot x = b'} = (:real^N)` THEN
ASM_REWRITE_TAC[
SUBSET_UNIV] THEN
RULE_ASSUM_TAC(REWRITE_RULE
[
HYPERPLANE_EQ_EMPTY;
HYPERPLANE_EQ_UNIV]) THEN
REWRITE_TAC[GSYM
SUBSET_ANTISYM_EQ] THEN
ASM_CASES_TAC `{x:real^N | a dot x = b}
SUBSET {x | a' dot x = b'}` THEN
ASM_REWRITE_TAC[] THEN
MP_TAC(ISPECL [`{x:real^N | a dot x = b}`; `{x:real^N | a' dot x = b'}`]
AFF_DIM_PSUBSET) THEN
ASM_SIMP_TAC[
PSUBSET;
REWRITE_RULE[GSYM
AFFINE_HULL_EQ]
AFFINE_HYPERPLANE] THEN
ASM_CASES_TAC `{x:real^N | a dot x = b} = {x | a' dot x = b'}` THEN
ASM_REWRITE_TAC[
SUBSET_REFL] THEN ASM_CASES_TAC `a':real^N = vec 0` THENL
[ASM_CASES_TAC `b' = &0` THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
ASM_REWRITE_TAC[
DOT_LZERO] THEN SET_TAC[];
ALL_TAC] THEN
ASM_CASES_TAC `a:real^N = vec 0` THENL
[ASM_CASES_TAC `b = &0` THENL [ALL_TAC; ASM_MESON_TAC[]] THEN
ASM_REWRITE_TAC[
DOT_LZERO] THEN SET_TAC[];
ALL_TAC] THEN
ASM_SIMP_TAC[
AFF_DIM_HYPERPLANE;
INT_LT_REFL]);;
let OPEN_CONVEX_HULL = prove
(`!s:real^N->bool. open s ==> open(convex hull s)`,
REPEAT GEN_TAC THEN
REWRITE_TAC[
CONVEX_HULL_EXPLICIT;
OPEN_CONTAINS_CBALL] THEN
REWRITE_TAC[
IN_ELIM_THM;
SUBSET;
LEFT_IMP_EXISTS_THM] THEN DISCH_TAC THEN
MAP_EVERY X_GEN_TAC [`a:real^N`; `t:real^N->bool`; `u:real^N->real`] THEN
STRIP_TAC THEN
SUBGOAL_THEN `?b. !x:real^N. x
IN t ==> &0 < b(x) /\ cball(x,b(x))
SUBSET s`
STRIP_ASSUME_TAC THENL
[REWRITE_TAC[GSYM
SKOLEM_THM] THEN ASM_MESON_TAC[
SUBSET]; ALL_TAC] THEN
ABBREV_TAC `i =
IMAGE (b:real^N->real) t` THEN
EXISTS_TAC `inf i` THEN MP_TAC(SPEC `i:real->bool`
INF_FINITE) THEN
EXPAND_TAC "i" THEN ASM_REWRITE_TAC[
FORALL_IN_IMAGE;
IN_IMAGE] THEN
ANTS_TAC THENL
[EXPAND_TAC "i" THEN CONJ_TAC THENL
[ASM_SIMP_TAC[
FINITE_IMAGE]; ALL_TAC] THEN
REWRITE_TAC[
IMAGE_EQ_EMPTY] THEN
ASM_MESON_TAC[
SUM_CLAUSES; REAL_ARITH `~(&1 = &0)`];
ALL_TAC] THEN
STRIP_TAC THEN CONJ_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
X_GEN_TAC `y:real^N` THEN REWRITE_TAC[
IN_CBALL; dist] THEN
DISCH_TAC THEN EXISTS_TAC `
IMAGE (\v:real^N. v + (y - a)) t` THEN
EXISTS_TAC `\v. (u:real^N->real)(v - (y - a))` THEN
ASM_SIMP_TAC[
FINITE_IMAGE;
FORALL_IN_IMAGE;
SUM_IMAGE;
VSUM_IMAGE;
VECTOR_ARITH `v + a:real^N = w + a <=> v = w`] THEN
ASM_REWRITE_TAC[
o_DEF; VECTOR_ARITH `(v + a) - a:real^N = v`] THEN
ASM_REWRITE_TAC[
VECTOR_ADD_LDISTRIB; ETA_AX] THEN
ASM_SIMP_TAC[
VSUM_ADD;
VSUM_RMUL] THEN
CONJ_TAC THENL [ALL_TAC; VECTOR_ARITH_TAC] THEN
X_GEN_TAC `z:real^N` THEN STRIP_TAC THEN
SUBGOAL_THEN `z + (y - a)
IN cball(z:real^N,b z)`
(fun th -> ASM_MESON_TAC[th;
SUBSET]) THEN
REWRITE_TAC[
IN_CBALL; dist; NORM_ARITH
`norm(z - (z + a - y)) = norm(y - a)`] THEN
ASM_MESON_TAC[
REAL_LE_TRANS]);;
let SIMPLEX_FURTHEST_LT = prove
(`!a:real^N s.
FINITE s
==> !x. x
IN (convex hull s) /\ ~(x
IN s)
==> ?y. y
IN (convex hull s) /\ norm(x - a) < norm(y - a)`,
GEN_TAC THEN MATCH_MP_TAC
FINITE_INDUCT_STRONG THEN
REWRITE_TAC[
CONVEX_HULL_EMPTY;
NOT_IN_EMPTY] THEN
MAP_EVERY X_GEN_TAC [`x:real^N`; `s:real^N->bool`] THEN
ASM_CASES_TAC `s:real^N->bool = {}` THENL
[ASM_REWRITE_TAC[
CONVEX_HULL_SING;
IN_SING] THEN MESON_TAC[];
ALL_TAC] THEN
ASM_SIMP_TAC[
CONVEX_HULL_INSERT] THEN
STRIP_TAC THEN X_GEN_TAC `y:real^N` THEN
REWRITE_TAC[
IN_ELIM_THM;
LEFT_AND_EXISTS_THM;
LEFT_IMP_EXISTS_THM] THEN
MAP_EVERY X_GEN_TAC [`u:real`; `v:real`; `b:real^N`] THEN
ASM_CASES_TAC `y:real^N
IN (convex hull s)` THENL
[REWRITE_TAC[
IN_INSERT; DE_MORGAN_THM] THEN STRIP_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPEC `y:real^N`) THEN
ASM_REWRITE_TAC[] THEN MATCH_MP_TAC
MONO_EXISTS THEN
X_GEN_TAC `c:real^N` THEN STRIP_TAC THEN
MAP_EVERY EXISTS_TAC [`&0`; `&1`; `c:real^N`] THEN
ASM_REWRITE_TAC[REAL_ADD_LID;
REAL_POS] THEN VECTOR_ARITH_TAC;
ALL_TAC] THEN
ASM_CASES_TAC `u = &0` THENL
[ASM_SIMP_TAC[REAL_ADD_LID;
VECTOR_MUL_LZERO;
VECTOR_ADD_LID] THEN
ASM_MESON_TAC[
VECTOR_MUL_LID];
ALL_TAC] THEN
ASM_CASES_TAC `v = &0` THENL
[ASM_SIMP_TAC[
REAL_ADD_RID;
VECTOR_MUL_LZERO;
VECTOR_ADD_RID] THEN
ASM_CASES_TAC `u = &1` THEN ASM_REWRITE_TAC[
VECTOR_MUL_LID] THEN
ASM_CASES_TAC `y = a:real^N` THEN ASM_REWRITE_TAC[
IN_INSERT] THEN
ASM_MESON_TAC[];
ALL_TAC] THEN
REWRITE_TAC[
IN_INSERT; DE_MORGAN_THM] THEN STRIP_TAC THEN
MP_TAC(SPECL [`u:real`; `v:real`]
REAL_DOWN2) THEN ANTS_TAC THENL
[ASM_REWRITE_TAC[
REAL_LT_LE]; ALL_TAC] THEN
DISCH_THEN(X_CHOOSE_THEN `w:real` STRIP_ASSUME_TAC) THEN
MP_TAC(ISPECL [`a:real^N`; `y:real^N`; `w % (x - b):real^N`]
DIST_INCREASES_ONLINE) THEN
ANTS_TAC THENL
[ASM_SIMP_TAC[
VECTOR_MUL_EQ_0;
REAL_LT_IMP_NZ] THEN
REWRITE_TAC[VECTOR_ARITH `(x - y = vec 0) <=> (x = y)`] THEN
DISCH_THEN SUBST_ALL_TAC THEN
UNDISCH_TAC `~(y:real^N
IN convex hull s)` THEN
ASM_REWRITE_TAC[GSYM
VECTOR_ADD_RDISTRIB;
VECTOR_MUL_LID];
ALL_TAC] THEN
ASM_REWRITE_TAC[dist;
real_gt] THEN
REWRITE_TAC[VECTOR_ARITH
`((u % x + v % b) + w % (x - b) = (u + w) % x + (v - w) % b) /\
((u % x + v % b) - w % (x - b) = (u - w) % x + (v + w) % b)`] THEN
STRIP_TAC THENL
[MAP_EVERY EXISTS_TAC
[`(u + w) % x + (v - w) % b:real^N`; `u + w`; `v - w`; `b:real^N`];
MAP_EVERY EXISTS_TAC
[`(u - w) % x + (v + w) % b:real^N`; `u - w`; `v + w`; `b:real^N`]] THEN
ONCE_REWRITE_TAC[
NORM_SUB] THEN ASM_REWRITE_TAC[] THEN
ASM_SIMP_TAC[
REAL_LE_ADD;
REAL_LT_IMP_LE;
REAL_SUB_LE] THEN
UNDISCH_TAC `u + v = &1` THEN REAL_ARITH_TAC);;
let DIAMETER_CONVEX_HULL = prove
(`!s:real^N->bool. diameter(convex hull s) = diameter s`,
let lemma = prove
(`!a b s. (!x. x IN s ==> dist(a,x) <= b)
==> (!x. x IN convex hull s ==> dist(a,x) <= b)`,
REPEAT GEN_TAC THEN DISCH_TAC THEN
MATCH_MP_TAC HULL_INDUCT THEN ASM_REWRITE_TAC[GSYM cball; CONVEX_CBALL]) in
GEN_TAC THEN REWRITE_TAC[diameter; CONVEX_HULL_EQ_EMPTY] THEN
COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC SUP_EQ THEN
REWRITE_TAC[FORALL_IN_GSPEC] THEN X_GEN_TAC `b:real` THEN
EQ_TAC THENL [MESON_TAC[SUBSET; HULL_SUBSET]; ALL_TAC] THEN
MATCH_MP_TAC(TAUT `!b. (a ==> b) /\ (b ==> c) ==> a ==> c`) THEN
EXISTS_TAC `!x:real^N y. x IN s /\ y IN convex hull s ==> norm(x - y) <= b`
THEN CONJ_TAC THENL
[MATCH_MP_TAC MONO_FORALL THEN X_GEN_TAC `x:real^N` THEN
ASM_CASES_TAC `(x:real^N) IN s` THEN ASM_REWRITE_TAC[] THEN
REWRITE_TAC[GSYM dist; lemma];
ONCE_REWRITE_TAC[SWAP_FORALL_THM] THEN
MATCH_MP_TAC MONO_FORALL THEN X_GEN_TAC `y:real^N` THEN
ASM_CASES_TAC `(y:real^N) IN convex hull s` THEN ASM_REWRITE_TAC[] THEN
REWRITE_TAC[GSYM(ONCE_REWRITE_RULE[DIST_SYM] dist); lemma]]);;
let CLOSER_POINT_LEMMA = prove
(`!x y z. (y - x) dot (z - x) > &0
==> ?u. &0 < u /\ u <= &1 /\ dist(x + u % (z - x),y) < dist(x,y)`,
REPEAT STRIP_TAC THEN FIRST_ASSUM(MP_TAC o MATCH_MP
CLOSER_POINTS_LEMMA) THEN
ONCE_REWRITE_TAC[
DIST_SYM] THEN REWRITE_TAC[dist;
NORM_LT] THEN
REWRITE_TAC[VECTOR_ARITH
`(y - (x + z)) dot (y - (x + z)) = (z - (y - x)) dot (z - (y - x))`] THEN
DISCH_THEN(X_CHOOSE_THEN `u:real` STRIP_ASSUME_TAC) THEN
EXISTS_TAC `min u (&1)` THEN
ASM_SIMP_TAC[
REAL_LT_MIN;
REAL_MIN_LE;
REAL_LT_01;
REAL_LE_REFL]);;
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]);;
let ANY_CLOSEST_POINT_AFFINE_ORTHOGONAL = prove
(`!s a b:real^N.
affine s /\ b
IN s /\ (!x. x
IN s ==> dist(a,b) <= dist(a,x))
==> (!x. x
IN s ==> orthogonal (x - b) (a - b))`,
REPEAT GEN_TAC THEN GEOM_ORIGIN_TAC `b:real^N` THEN
REWRITE_TAC[
DIST_0;
VECTOR_SUB_RZERO; orthogonal; dist;
NORM_LE] THEN
REWRITE_TAC[
DOT_LSUB] THEN REWRITE_TAC[
DOT_RSUB] THEN
REWRITE_TAC[
DOT_SYM; REAL_ARITH `a <= a - y - (y - x) <=> &2 * y <= x`] THEN
REPEAT STRIP_TAC THEN ASM_CASES_TAC `x:real^N = vec 0` THEN
ASM_REWRITE_TAC[
DOT_RZERO] THEN FIRST_X_ASSUM(fun th ->
MP_TAC(SPEC `vec 0 + --((a dot x) / (x dot x)) % (x - vec 0:real^N)` th) THEN
MP_TAC(SPEC `vec 0 + (a dot x) / (x dot x) % (x - vec 0:real^N)` th)) THEN
ASM_SIMP_TAC[
IN_AFFINE_ADD_MUL_DIFF] THEN
REWRITE_TAC[
VECTOR_SUB_RZERO;
VECTOR_ADD_LID;
DOT_RMUL] THEN
REWRITE_TAC[
DOT_LMUL; IMP_IMP] THEN DISCH_THEN(MP_TAC o MATCH_MP (REAL_ARITH
`&2 * x * a <= b * c * z /\ &2 * --x * a <= --b * --c * z
==> &2 * abs(x * a) <= b * c * z`)) THEN
ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN DISCH_TAC THEN
ASM_SIMP_TAC[
REAL_NOT_LE;
REAL_DIV_RMUL;
DOT_EQ_0] THEN
MATCH_MP_TAC(REAL_ARITH `~(x = &0) ==> x < &2 * abs x`) THEN
RULE_ASSUM_TAC(REWRITE_RULE[GSYM
DOT_EQ_0]) THEN
REPEAT(POP_ASSUM MP_TAC) THEN CONV_TAC REAL_FIELD);;
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]);;
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`]);;
let RADON_V_LEMMA = prove
(`!(s:A->bool) f g.
FINITE s /\ vsum s f = vec 0 /\ (!x. g x = &0 ==> f x = vec 0)
==> (vsum {x | x
IN s /\ &0 < g x} f) :real^N =
-- vsum {x | x
IN s /\ g x < &0} f`,
let RADON_PARTITION = prove
(`!(c:real^N->bool).
FINITE c /\
affine_dependent c
==> ?(m:real^N->bool) (p:real^N->bool).
(
DISJOINT m p) /\
(m
UNION p = c) /\
~(
DISJOINT (convex hull m) (convex hull p))`,
REPEAT STRIP_TAC THEN
MP_TAC (ISPEC `c:real^N->bool`
RADON_EX_LEMMA) THEN
ASM_REWRITE_TAC[] THEN
REPEAT STRIP_TAC THEN
MAP_EVERY EXISTS_TAC [`{v:real^N | v
IN c /\ u v <= &0}`;
`{v:real^N | v
IN c /\ u v > &0}`] THEN
REPEAT CONJ_TAC THENL
[REWRITE_TAC[
DISJOINT;
INTER;
IN_ELIM_THM;REAL_ARITH `x <= &0 <=> ~(x > &0)`] THEN
SET_TAC[];
REWRITE_TAC[
UNION;
IN_ELIM_THM;REAL_ARITH `x <= &0 <=> ~(x > &0)`] THEN
SET_TAC[];
ALL_TAC] THEN
SUBGOAL_THEN `~(sum {x:real^N | x
IN c /\ u x > &0} u = &0)` ASSUME_TAC THENL
[MATCH_MP_TAC (REAL_ARITH `a > &0 ==> ~(a = &0)`) THEN
REWRITE_TAC[REAL_ARITH `a > &0 <=> &0 < a`] THEN
MATCH_MP_TAC (REWRITE_RULE[
SUM_0] (ISPEC `\x. &0`
SUM_LT_ALL)) THEN
ASM_SIMP_TAC[
FINITE_RESTRICT;
IN_ELIM_THM;
EXTENSION;
NOT_IN_EMPTY] THEN
REWRITE_TAC[MESON[]`~(!x. ~(P x /\ Q x)) = ?x. P x /\ Q x`] THEN
ASM_CASES_TAC `&0 < u (v:real^N)` THENL
[ASM SET_TAC[];ALL_TAC] THEN
POP_ASSUM MP_TAC THEN POP_ASSUM (K ALL_TAC) THEN POP_ASSUM MP_TAC THEN
REWRITE_TAC[IMP_IMP;REAL_ARITH `~(a = &0) /\ ~(&0 < a) <=> a < &0`] THEN
DISCH_TAC THEN
REWRITE_TAC[MESON[
REAL_NOT_LT]
`(?x:real^N. P x /\ &0 < u x) <=> (!x. P x ==> u x <= &0) ==> F`] THEN
DISCH_TAC THEN
MP_TAC (ISPECL [`u:real^N->real`;`\x:real^N. &0`;`c:real^N->bool`]
SUM_LT) THEN
ASM_REWRITE_TAC[
SUM_0;REAL_ARITH `~(&0 < &0)`] THEN
ASM_MESON_TAC[];ALL_TAC] THEN
REWRITE_TAC[SET_RULE `~DISJOINT a b <=> ?y. y
IN a /\ y
IN b`] THEN
EXISTS_TAC `&1 / (sum {x:real^N | x
IN c /\ u x > &0} u) %
vsum {x:real^N | x
IN c /\ u x > &0} (\x. u x % x)` THEN
REWRITE_TAC[
CONVEX_HULL_EXPLICIT;
IN_ELIM_THM] THEN
CONJ_TAC THENL
[MAP_EVERY EXISTS_TAC [`{v:real^N | v
IN c /\ u v < &0}`;
`\y:real^N.
&1 / (sum {x:real^N | x
IN c /\ u x > &0} u) *
(--(u y))`] THEN
ASM_SIMP_TAC[
FINITE_RESTRICT;
SUBSET;
IN_ELIM_THM] THEN
REPEAT CONJ_TAC THENL
[REAL_ARITH_TAC;
REPEAT STRIP_TAC THEN
MATCH_MP_TAC
REAL_LE_MUL THEN
CONJ_TAC THENL [ALL_TAC;
ASM_REWRITE_TAC[
REAL_NEG_GE0;
REAL_LE_LT]] THEN
MATCH_MP_TAC
REAL_LE_DIV THEN
REWRITE_TAC[
REAL_LE_01] THEN
MATCH_MP_TAC
SUM_POS_LE THEN
ASM_SIMP_TAC[
FINITE_RESTRICT;
IN_ELIM_THM] THEN
REAL_ARITH_TAC;
ASM_SIMP_TAC[
FINITE_RESTRICT;
SUM_LMUL] THEN
MATCH_MP_TAC (REAL_FIELD `!a. ~(a = &0) /\ a * b = a * c ==> b = c`) THEN
EXISTS_TAC `sum {x:real^N | x
IN c /\ u x > &0} u` THEN
REWRITE_TAC[
SUM_LMUL] THEN
ASM_SIMP_TAC[REAL_FIELD `~(a = &0) ==> a * &1 / a * b = b`] THEN
REWRITE_TAC[
SUM_NEG;
REAL_MUL_RID] THEN
REWRITE_TAC[REAL_ARITH `a > &0 <=> &0 < a`] THEN
MATCH_MP_TAC (GSYM
RADON_S_LEMMA) THEN
ASM_REWRITE_TAC[];
ALL_TAC] THEN
REWRITE_TAC[GSYM
VECTOR_MUL_ASSOC;
VSUM_LMUL;
VECTOR_MUL_LCANCEL] THEN
REWRITE_TAC[
VECTOR_MUL_LNEG;
VSUM_NEG] THEN
DISJ2_TAC THEN
MATCH_MP_TAC (REWRITE_RULE[REAL_ARITH `&0 < a <=> a > &0`]
(GSYM
RADON_V_LEMMA)) THEN
ASM_REWRITE_TAC[] THEN
MESON_TAC[
VECTOR_MUL_LZERO];ALL_TAC] THEN
MAP_EVERY EXISTS_TAC [`{v:real^N | v
IN c /\ u v > &0}`;
`\y:real^N.
&1 / (sum {x:real^N | x
IN c /\ u x > &0} u) *
(u y)`] THEN
ASM_SIMP_TAC[
FINITE_RESTRICT;
SUBSET;
IN_ELIM_THM] THEN
REPEAT CONJ_TAC THENL
[REPEAT STRIP_TAC THEN
MATCH_MP_TAC
REAL_LE_MUL THEN
CONJ_TAC THENL [ALL_TAC;
ASM_SIMP_TAC[REAL_ARITH `a > &0 ==> &0 <= a`]] THEN
MATCH_MP_TAC
REAL_LE_DIV THEN
REWRITE_TAC[
REAL_LE_01] THEN
MATCH_MP_TAC
SUM_POS_LE THEN
ASM_SIMP_TAC[
FINITE_RESTRICT;
IN_ELIM_THM] THEN
REAL_ARITH_TAC;
ASM_SIMP_TAC[
FINITE_RESTRICT;
SUM_LMUL] THEN
MATCH_MP_TAC (REAL_FIELD `!a. ~(a = &0) /\ a * b = a * c ==> b = c`) THEN
EXISTS_TAC `sum {x:real^N | x
IN c /\ u x > &0} u` THEN
REWRITE_TAC[
SUM_LMUL] THEN
ASM_SIMP_TAC[REAL_FIELD `~(a = &0) ==> a * &1 / a * b = b`] THEN
REWRITE_TAC[
SUM_NEG;
REAL_MUL_RID] THEN
REWRITE_TAC[REAL_ARITH `a > &0 <=> &0 < a`] THEN
MATCH_MP_TAC (GSYM
RADON_S_LEMMA) THEN
ASM_REWRITE_TAC[];
ALL_TAC] THEN
REWRITE_TAC[GSYM
VECTOR_MUL_ASSOC;
VSUM_LMUL;
VECTOR_MUL_LCANCEL] THEN
REWRITE_TAC[
VECTOR_MUL_LNEG;
VSUM_NEG] THEN
DISJ2_TAC THEN
MATCH_MP_TAC (REWRITE_RULE[REAL_ARITH `&0 < a <=> a > &0`]
(GSYM
RADON_V_LEMMA)) THEN
ASM_REWRITE_TAC[] THEN
MESON_TAC[
VECTOR_MUL_LZERO]);;
let RADON = prove
(`!(c:real^N->bool).
affine_dependent c
==> ?(m:real^N->bool) (p:real^N->bool).
m
SUBSET c /\
p
SUBSET c /\
DISJOINT m p /\
~(
DISJOINT (convex hull m) (convex hull p))`,
REPEAT STRIP_TAC THEN MP_TAC
(ISPEC `c:real^N->bool`
AFFINE_DEPENDENT_EXPLICIT) THEN
ASM_SIMP_TAC[] THEN REPEAT STRIP_TAC THEN MP_TAC
(ISPEC `s:real^N->bool`
RADON_PARTITION) THEN
ANTS_TAC THENL
[ASM_SIMP_TAC[
AFFINE_DEPENDENT_EXPLICIT] THEN
MAP_EVERY EXISTS_TAC [`s:real^N->bool`;`u:real^N->real`] THEN
ASM SET_TAC[];ALL_TAC] THEN
DISCH_THEN STRIP_ASSUME_TAC THEN
MAP_EVERY EXISTS_TAC [`m:real^N->bool`;`p:real^N->bool`] THEN
ASM SET_TAC[]);;
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_ALT = prove
(`!f:(real^N->bool)->bool.
(!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
DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN
MATCH_MP_TAC
CLOSED_FIP THEN ASM_SIMP_TAC[] THEN
X_GEN_TAC `g:(real^N->bool)->bool` THEN STRIP_TAC THEN
MATCH_MP_TAC
HELLY_ALT THEN ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
[ASM SET_TAC[];
ASM_MESON_TAC[
SUBSET_TRANS;
FINITE_SUBSET]]);;
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]);;
let KIRCHBERGER = prove
(`!s t:real^N->bool.
compact s /\ compact t /\
(!s' t'. s'
SUBSET s /\ t'
SUBSET t /\
FINITE s' /\
FINITE t' /\
CARD(s') +
CARD(t') <= dimindex(:N) + 2
==> ?a b. (!x. x
IN s' ==> a dot x < b) /\
(!x. x
IN t' ==> a dot x > b))
==> ?a b. ~(a = vec 0) /\
(!x. x
IN s ==> a dot x < b) /\
(!x. x
IN t ==> a dot x > b)`,
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[]]]]);;
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]);;
let SUBSPACE_CONVEX_CONE_SYMMETRIC = prove
(`!s:real^N->bool.
subspace s <=>
convex_cone s /\ (!x. x
IN s ==> --x
IN s)`,
GEN_TAC THEN REWRITE_TAC[subspace;
CONVEX_CONE] THEN
EQ_TAC THEN STRIP_TAC THEN ASM_SIMP_TAC[] THENL
[ASM_MESON_TAC[VECTOR_ARITH `--x:real^N = -- &1 % x`];
MAP_EVERY X_GEN_TAC [`c:real`; `x:real^N`] THEN DISCH_TAC THEN
DISJ_CASES_TAC(SPEC `c:real`
REAL_LE_NEGTOTAL) THEN ASM_SIMP_TAC[] THEN
ASM_MESON_TAC[VECTOR_ARITH `c % x:real^N = --(--c % x)`]]);;
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]);;
let CONVEX_ON_JENSEN = prove
(`!f:real^N->real s.
convex s
==> (f
convex_on s <=>
!k u x.
(!i:num. 1 <= i /\ i <= k ==> &0 <= u(i) /\ x(i)
IN s) /\
(sum (1..k) u = &1)
==> f(vsum (1..k) (\i. u(i) % x(i)))
<= sum (1..k) (\i. u(i) * f(x(i))))`,
let IVT_INCREASING_COMPONENT_1 = prove
(`!f:real^1->real^N a b y k.
drop a <= drop b /\ 1 <= k /\ k <= dimindex(:N) /\
(!x. x
IN interval[a,b] ==> f continuous at x) /\
f(a)$k <= y /\ y <= f(b)$k
==> ?x. x
IN interval[a,b] /\ f(x)$k = y`,
let IVT_DECREASING_COMPONENT_1 = prove
(`!f:real^1->real^N a b y k.
drop a <= drop b /\ 1 <= k /\ k <= dimindex(:N) /\
(!x. x
IN interval[a,b] ==> f continuous at x) /\
f(b)$k <= y /\ y <= f(a)$k
==> ?x. x
IN interval[a,b] /\ f(x)$k = y`,
let CONVEX_ON_BOUNDED_CONTINUOUS = prove
(`!f:real^N->real s b.
open s /\ f
convex_on s /\ (!x. x
IN s ==> abs(f x) <= b)
==> (lift o f)
continuous_on s`,
REPEAT STRIP_TAC THEN MATCH_MP_TAC
CONTINUOUS_AT_IMP_CONTINUOUS_ON THEN
X_GEN_TAC `x:real^N` THEN DISCH_TAC THEN
REWRITE_TAC[
CONTINUOUS_AT_LIFT_RANGE] THEN
ABBREV_TAC `B = abs(b) + &1` THEN
SUBGOAL_THEN `&0 < B /\ !x:real^N. x
IN s ==> abs(f x) <= B`
STRIP_ASSUME_TAC THENL
[EXPAND_TAC "B" THEN CONJ_TAC THENL [REAL_ARITH_TAC; ALL_TAC] THEN
ASM_MESON_TAC[REAL_ARITH `x <= b ==> x <= abs b + &1`];
ALL_TAC] THEN
X_GEN_TAC `e:real` THEN DISCH_TAC THEN
REWRITE_TAC[REAL_ARITH `abs(x - y) < e <=> x - y < e /\ y - x < e`] THEN
FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [
OPEN_CONTAINS_CBALL]) THEN
DISCH_THEN(MP_TAC o SPEC `x:real^N`) THEN REWRITE_TAC[
SUBSET;
IN_CBALL] THEN
ASM_REWRITE_TAC[] THEN
DISCH_THEN(X_CHOOSE_THEN `k:real` STRIP_ASSUME_TAC) THEN
EXISTS_TAC `min (k / &2) (e / (&2 * B) * k)` THEN
ASM_SIMP_TAC[
REAL_LT_MIN;
REAL_LT_DIV;
REAL_LT_MUL;
REAL_OF_NUM_LT; ARITH] THEN
X_GEN_TAC `y:real^N` THEN
ASM_CASES_TAC `y:real^N = x` THEN ASM_REWRITE_TAC[
REAL_SUB_REFL] THEN
STRIP_TAC THEN
ABBREV_TAC `t = k / norm(y - x:real^N)` THEN
SUBGOAL_THEN `&2 < t` ASSUME_TAC THENL
[EXPAND_TAC "t" THEN
ASM_SIMP_TAC[
REAL_LT_RDIV_EQ;
NORM_POS_LT;
VECTOR_SUB_EQ] THEN
ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
ASM_SIMP_TAC[GSYM
REAL_LT_RDIV_EQ;
REAL_OF_NUM_LT; ARITH];
ALL_TAC] THEN
FIRST_ASSUM(STRIP_ASSUME_TAC o MATCH_MP (REAL_ARITH
`&2 < t ==> &0 < t /\ ~(t = &0) /\ &0 < t - &1 /\
&0 < &1 + t /\ ~(&1 + t = &0)`)) THEN
SUBGOAL_THEN `y:real^N
IN s` ASSUME_TAC THENL
[FIRST_ASSUM MATCH_MP_TAC THEN REWRITE_TAC[dist] THEN
ONCE_REWRITE_TAC[
NORM_SUB] THEN
FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH
`x < k / &2 ==> k / &2 <= k ==> x <= k`)) THEN
ASM_SIMP_TAC[
REAL_LE_LDIV_EQ;
REAL_OF_NUM_LT; ARITH] THEN
UNDISCH_TAC `&0 < k` THEN REAL_ARITH_TAC;
ALL_TAC] THEN
CONJ_TAC THENL
[ABBREV_TAC `w:real^N = x + t % (y - x)` THEN
SUBGOAL_THEN `w:real^N
IN s` STRIP_ASSUME_TAC THENL
[FIRST_ASSUM MATCH_MP_TAC THEN EXPAND_TAC "w" THEN
REWRITE_TAC[dist; VECTOR_ARITH `x - (x + t) = --t:real^N`] THEN
EXPAND_TAC "t" THEN REWRITE_TAC[
NORM_NEG;
NORM_MUL;
REAL_ABS_DIV] THEN
REWRITE_TAC[
REAL_ABS_NORM;
real_div; GSYM REAL_MUL_ASSOC] THEN
ASM_SIMP_TAC[REAL_MUL_LINV;
REAL_LT_IMP_NZ;
NORM_POS_LT;
VECTOR_SUB_EQ;
REAL_MUL_RID; REAL_ARITH `&0 < x ==> abs(x) <= x`];
ALL_TAC] THEN
SUBGOAL_THEN `(&1 / t) % w + (t - &1) / t % x = y:real^N` ASSUME_TAC THENL
[EXPAND_TAC "w" THEN
REWRITE_TAC[VECTOR_ARITH
`b % (x + c % (y - x)) + a % x =
(a + b - b * c) % x + (b * c) % y`] THEN
ASM_SIMP_TAC[
REAL_DIV_RMUL;
VECTOR_MUL_LID] THEN
ASM_SIMP_TAC[
real_div;
REAL_MUL_RINV;
REAL_SUB_REFL;
VECTOR_MUL_LZERO;
VECTOR_ADD_LID;
REAL_ARITH `(a - &1) * b + &1 * b - &1 = a * b - &1`];
ALL_TAC] THEN
FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [
convex_on]) THEN
DISCH_THEN(MP_TAC o SPECL
[`w:real^N`; `x:real^N`; `&1 / t`; `(t - &1) / t`]) THEN
ASM_SIMP_TAC[
REAL_LT_IMP_LE;
REAL_LT_DIV;
REAL_LT_01] THEN
REWRITE_TAC[
real_div; GSYM
REAL_ADD_RDISTRIB] THEN
ASM_SIMP_TAC[
REAL_SUB_ADD2;
REAL_MUL_RINV] THEN
MATCH_MP_TAC(REAL_ARITH
`a * fw + (b - &1) * fx < e
==> fy <= a * fw + b * fx ==> fy - fx < e`) THEN
ASM_SIMP_TAC[
real_div;
REAL_SUB_RDISTRIB;
REAL_MUL_RINV; REAL_MUL_LID;
REAL_ARITH `a * x + y - a * y - y = a * (x - y)`] THEN
ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
ASM_SIMP_TAC[GSYM
real_div;
REAL_LT_LDIV_EQ] THEN
MATCH_MP_TAC(REAL_ARITH
`!b. abs(x) <= b /\ abs(y) <= b /\ &2 * b < z ==> x - y < z`) THEN
EXISTS_TAC `B:real` THEN ASM_SIMP_TAC[] THEN EXPAND_TAC "t" THEN
REWRITE_TAC[
real_div; REAL_MUL_ASSOC] THEN REWRITE_TAC[GSYM
real_div] THEN
ASM_SIMP_TAC[
REAL_LT_RDIV_EQ;
NORM_POS_LT;
VECTOR_SUB_EQ] THEN
ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
ASM_SIMP_TAC[GSYM
REAL_LT_RDIV_EQ;
REAL_LT_MUL;
REAL_OF_NUM_LT; ARITH] THEN
REWRITE_TAC[
real_div; REAL_ARITH `(a * b) * inv c = (b * inv c) * a`] THEN
ASM_REWRITE_TAC[GSYM
real_div];
ABBREV_TAC `w:real^N = x - t % (y - x)` THEN
SUBGOAL_THEN `w:real^N
IN s` STRIP_ASSUME_TAC THENL
[FIRST_ASSUM MATCH_MP_TAC THEN EXPAND_TAC "w" THEN
REWRITE_TAC[dist; VECTOR_ARITH `x - (x - t) = t:real^N`] THEN
EXPAND_TAC "t" THEN REWRITE_TAC[
NORM_MUL;
REAL_ABS_DIV] THEN
REWRITE_TAC[
REAL_ABS_NORM;
real_div; GSYM REAL_MUL_ASSOC] THEN
ASM_SIMP_TAC[REAL_MUL_LINV;
REAL_LT_IMP_NZ;
NORM_POS_LT;
VECTOR_SUB_EQ;
REAL_MUL_RID; REAL_ARITH `&0 < x ==> abs(x) <= x`];
ALL_TAC] THEN
SUBGOAL_THEN `(&1 / (&1 + t)) % w + t / (&1 + t) % y = x:real^N`
ASSUME_TAC THENL
[EXPAND_TAC "w" THEN
REWRITE_TAC[VECTOR_ARITH
`b % (x - c % (y - x)) + a % y =
(b * (&1 + c)) % x + (a - b * c) % y`] THEN
ASM_SIMP_TAC[
REAL_DIV_RMUL;
VECTOR_MUL_LID] THEN
REWRITE_TAC[
real_div;
REAL_MUL_AC; REAL_MUL_LID;
REAL_MUL_RID] THEN
REWRITE_TAC[
REAL_SUB_REFL;
VECTOR_MUL_LZERO;
VECTOR_ADD_RID];
ALL_TAC] THEN
FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [
convex_on]) THEN
DISCH_THEN(MP_TAC o SPECL
[`w:real^N`; `y:real^N`; `&1 / (&1 + t)`; `t / (&1 + t)`]) THEN
ASM_SIMP_TAC[
REAL_LT_IMP_LE;
REAL_LT_DIV;
REAL_LT_01] THEN
REWRITE_TAC[
real_div; GSYM
REAL_ADD_RDISTRIB] THEN
ASM_SIMP_TAC[
REAL_SUB_ADD2;
REAL_MUL_RINV] THEN
MATCH_MP_TAC(REAL_ARITH
`a * fw + (b - &1) * fx < e
==> fy <= a * fw + b * fx ==> fy - fx < e`) THEN
SUBGOAL_THEN `t * inv(&1 + t) - &1 = --(inv(&1 + t))` SUBST1_TAC THENL
[REWRITE_TAC[REAL_ARITH `(a * b - &1 = --b) <=> ((&1 + a) * b = &1)`] THEN
ASM_SIMP_TAC[
REAL_MUL_RINV];
ALL_TAC] THEN
REWRITE_TAC[REAL_ARITH `(&1 * a) * x + --a * y = a * (x - y)`] THEN
ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
ASM_SIMP_TAC[GSYM
real_div;
REAL_LT_LDIV_EQ] THEN
MATCH_MP_TAC(REAL_ARITH
`!b. abs(x) <= b /\ abs(y) <= b /\ &2 * b < z ==> x - y < z`) THEN
EXISTS_TAC `B:real` THEN ASM_SIMP_TAC[] THEN
MATCH_MP_TAC(REAL_ARITH `&0 < e /\ x < e * k ==> x < e * (&1 + k)`) THEN
EXPAND_TAC "t" THEN REWRITE_TAC[
real_div; REAL_MUL_ASSOC] THEN
REWRITE_TAC[GSYM
real_div] THEN
ASM_SIMP_TAC[
REAL_LT_RDIV_EQ;
NORM_POS_LT;
VECTOR_SUB_EQ] THEN
ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
ASM_SIMP_TAC[GSYM
REAL_LT_RDIV_EQ;
REAL_LT_MUL;
REAL_OF_NUM_LT; ARITH] THEN
REWRITE_TAC[
real_div; REAL_ARITH `(a * b) * inv c = (b * inv c) * a`] THEN
ASM_REWRITE_TAC[GSYM
real_div]]);;
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);;
let SEGMENT_BOUND = prove
(`!a b x:real^N.
x
IN segment[a,b] ==> norm(x - a) <= norm(b - a) /\
norm(x - b) <= norm(b - a)`,
let BETWEEN_TRANSLATION = prove
(`!a x y. between (a + x) (a + y,a + z) <=> between x (y,z)`,
REWRITE_TAC[between] THEN NORM_ARITH_TAC);;
let STARLIKE_CLOSURE = prove
(`!s:real^N->bool. starlike s ==> starlike(closure s)`,
GEN_TAC THEN REWRITE_TAC[starlike;
SUBSET; segment;
FORALL_IN_GSPEC] THEN
MATCH_MP_TAC
MONO_EXISTS THEN X_GEN_TAC `a:real^N` THEN
STRIP_TAC THEN ASM_SIMP_TAC[REWRITE_RULE[
SUBSET]
CLOSURE_SUBSET] THEN
X_GEN_TAC `x:real^N` THEN REWRITE_TAC[
SUBSET;
CLOSURE_APPROACHABLE] THEN
DISCH_TAC THEN X_GEN_TAC `u:real` THEN STRIP_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 `y:real^N` STRIP_ASSUME_TAC) THEN
EXISTS_TAC `(&1 - u) % a + u % y:real^N` THEN
ASM_SIMP_TAC[dist;
NORM_MUL; VECTOR_ARITH
`(v % a + u % y) - (v % a + u % z):real^N = u % (y - z)`] THEN
FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REWRITE_RULE[
IMP_CONJ_ALT]
REAL_LET_TRANS)) THEN
REWRITE_TAC[dist; REAL_ARITH `u * n <= n <=> &0 <= n * (&1 - u)`] THEN
MATCH_MP_TAC
REAL_LE_MUL THEN REWRITE_TAC[
NORM_POS_LE] THEN
ASM_REAL_ARITH_TAC);;
let BETWEEN_DIST_LT = prove
(`!r a b c:real^N.
dist(c,a) < r /\ dist(c,b) < r /\ between x (a,b) ==> dist(c,x) < r`,
let BETWEEN_DIST_LE = prove
(`!r a b c:real^N.
dist(c,a) <= r /\ dist(c,b) <= r /\ between x (a,b) ==> dist(c,x) <= r`,
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]]));;
let RAY_TO_FRONTIER = prove
(`!s a l:real^N.
bounded s /\ a
IN interior s /\ ~(l = vec 0)
==> ?d. &0 < d /\ (a + d % l)
IN frontier s /\
!e. &0 <= e /\ e < d ==> (a + e % l)
IN interior s`,
let HOMEOMORPHIC_CONVEX_COMPACT = prove
(`!s:real^N->bool t:real^N->bool.
convex s /\ compact s /\ ~(interior s = {}) /\
convex t /\ compact t /\ ~(interior t = {})
==> s homeomorphic t`,
let AFF_DIM_INTERVAL = prove
(`(!a b:real^N.
aff_dim(interval[a,b]) =
if interval[a,b] = {} then --(&1)
else &(
CARD {i | 1 <= i /\ i <= dimindex(:N) /\ a$i < b$i})) /\
(!a b:real^N.
aff_dim(interval(a,b)) =
if interval(a,b) = {} then --(&1)
else &(dimindex(:N)))`,
let MIDPOINT_CONVEX_DYADIC_RATIONALS = prove
(`!f:real^N->real s.
(!x y. x
IN s /\ y
IN s
==> midpoint(x,y)
IN s /\
f(midpoint(x,y)) <= (f(x) + f(y)) / &2)
==> !n m p x y.
x
IN s /\ y
IN s /\ m + p = 2
EXP n
==> (&m / &2 pow n % x + &p / &2 pow n % y)
IN s /\
f(&m / &2 pow n % x + &p / &2 pow n % y)
<= &m / &2 pow n * f x + &p / &2 pow n * f y`,
REPEAT GEN_TAC THEN DISCH_TAC THEN INDUCT_TAC THENL
[REWRITE_TAC[ARITH_RULE
`m + p = 2
EXP 0 <=> m = 0 /\ p = 1 \/ m = 1 /\ p = 0`] THEN
REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
CONV_TAC REAL_RAT_REDUCE_CONV THEN
ASM_REWRITE_TAC[
VECTOR_MUL_LID;
VECTOR_MUL_LZERO;
VECTOR_ADD_LID;
VECTOR_ADD_RID] THEN
REAL_ARITH_TAC;
MATCH_MP_TAC
WLOG_LE THEN CONJ_TAC THENL
[REWRITE_TAC[
VECTOR_ADD_SYM; REAL_ADD_SYM;
ADD_SYM] THEN MESON_TAC[];
ALL_TAC] THEN
MAP_EVERY X_GEN_TAC [`m:num`; `p:num`] THEN DISCH_TAC THEN
REPEAT GEN_TAC THEN REWRITE_TAC[
EXP;
real_pow] THEN STRIP_TAC THEN
REWRITE_TAC[
real_div;
REAL_INV_MUL] THEN
ONCE_REWRITE_TAC[REAL_ARITH `x * inv(&2) * y = inv(&2) * x * y`] THEN
ONCE_REWRITE_TAC[GSYM REAL_MUL_ASSOC; GSYM
VECTOR_MUL_ASSOC] THEN
REWRITE_TAC[GSYM REAL_ADD_LDISTRIB; GSYM
VECTOR_ADD_LDISTRIB] THEN
SUBGOAL_THEN `2
EXP n <= p` ASSUME_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN
SUBGOAL_THEN `&p * inv(&2 pow n) = &(p - 2
EXP n) * inv(&2 pow n) + &1`
SUBST1_TAC THENL
[ASM_SIMP_TAC[GSYM
REAL_OF_NUM_SUB; GSYM
REAL_OF_NUM_POW] THEN
ASM_SIMP_TAC[
REAL_SUB_RDISTRIB;
REAL_MUL_RINV;
REAL_LT_IMP_NZ;
REAL_LT_POW2] THEN REAL_ARITH_TAC;
REWRITE_TAC[
VECTOR_ADD_RDISTRIB;
REAL_ADD_RDISTRIB] THEN
REWRITE_TAC[
VECTOR_MUL_LID; REAL_MUL_LID] THEN
REWRITE_TAC[
VECTOR_ADD_ASSOC; REAL_ADD_ASSOC] THEN
REWRITE_TAC[GSYM midpoint; GSYM
real_div] THEN FIRST_X_ASSUM(fun th ->
W(MP_TAC o PART_MATCH (lhand o rand) th o lhand o snd)) THEN
FIRST_X_ASSUM(fun th ->
W(MP_TAC o PART_MATCH (lhand o rand) th o funpow 3 lhand o snd)) THEN
ASM_REWRITE_TAC[] THEN ANTS_TAC THENL
[ASM_ARITH_TAC; SIMP_TAC[] THEN REAL_ARITH_TAC]]]);;
let UNBOUNDED_CONVEX_CLOSED_CONTAINS_RAY = prove
(`!s a:real^N.
convex s /\ ~bounded s /\ closed s /\ a
IN s
==> ?l. ~(l = vec 0) /\ !t. &0 <= t ==> (a + t % l)
IN s`,
GEN_GEOM_ORIGIN_TAC `a:real^N` ["l"] THEN
REWRITE_TAC[
VECTOR_ADD_LID] THEN REPEAT STRIP_TAC THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE RAND_CONV [
BOUNDED_POS]) THEN
REWRITE_TAC[
NOT_EXISTS_THM; TAUT `~(p /\ q) <=> p ==> ~q`] THEN
DISCH_THEN(MP_TAC o GEN `n:num` o SPEC `&n + &1:real`) THEN
REWRITE_TAC[
NOT_FORALL_THM; NOT_IMP; REAL_ARITH `&0 < &n + &1`] THEN
REWRITE_TAC[
REAL_NOT_LE;
SKOLEM_THM;
LEFT_IMP_EXISTS_THM] THEN
X_GEN_TAC `x:num->real^N` THEN REWRITE_TAC[
FORALL_AND_THM] THEN
STRIP_TAC THEN
SUBGOAL_THEN `!n. ~((x:num->real^N) n = vec 0)` ASSUME_TAC THENL
[ASM_MESON_TAC[NORM_ARITH `~(&n + &1 < norm(vec 0:real^N))`]; ALL_TAC] THEN
MP_TAC(ISPEC `sphere(vec 0:real^N,&1)` compact) THEN
REWRITE_TAC[
COMPACT_SPHERE] THEN
DISCH_THEN(MP_TAC o SPEC `\n. inv(norm(x n)) % (x:num->real^N) n`) THEN
ASM_SIMP_TAC[
IN_SPHERE_0;
NORM_MUL;
REAL_ABS_INV;
REAL_ABS_NORM;
REAL_MUL_LINV;
NORM_EQ_0;
o_DEF] THEN
MATCH_MP_TAC
MONO_EXISTS THEN X_GEN_TAC `l:real^N` THEN
DISCH_THEN(X_CHOOSE_THEN `r:num->num` STRIP_ASSUME_TAC) THEN CONJ_TAC THENL
[ASM_MESON_TAC[NORM_ARITH `~(norm(vec 0:real^N) = &1)`]; ALL_TAC] THEN
X_GEN_TAC `t:real` THEN DISCH_TAC THEN
MATCH_MP_TAC
CLOSED_CONTAINS_SEQUENTIAL_LIMIT THEN
SUBGOAL_THEN
`?N:num. !n. N <= n ==> t / norm(x n:real^N) <= &1`
STRIP_ASSUME_TAC THENL
[ASM_SIMP_TAC[
REAL_LE_LDIV_EQ;
NORM_POS_LT] THEN
MP_TAC(SPEC `t:real`
REAL_ARCH_SIMPLE) THEN
MATCH_MP_TAC
MONO_EXISTS THEN
REWRITE_TAC[GSYM REAL_OF_NUM_LE; REAL_MUL_LID] THEN
ASM_MESON_TAC[REAL_ARITH `t <= m /\ m <= n /\ n + &1 < x ==> t <= x`];
EXISTS_TAC `\n:num. t / norm((x:num->real^N)(r(N + n))) % x(r(N + n))` THEN
ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
[X_GEN_TAC `n:num` THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [
CONVEX_ALT]) THEN
DISCH_THEN(MP_TAC o SPEC `vec 0:real^N`) THEN
ASM_REWRITE_TAC[
VECTOR_MUL_RZERO;
VECTOR_ADD_LID] THEN
DISCH_THEN MATCH_MP_TAC THEN ASM_SIMP_TAC[
REAL_LE_DIV;
NORM_POS_LE] THEN
FIRST_X_ASSUM MATCH_MP_TAC THEN
FIRST_ASSUM(MP_TAC o SPEC `N + n:num` o MATCH_MP
MONOTONE_BIGGER) THEN
ARITH_TAC;
REWRITE_TAC[
real_div; GSYM
VECTOR_MUL_ASSOC] THEN
MATCH_MP_TAC
LIM_CMUL THEN ONCE_REWRITE_TAC[
ADD_SYM] THEN
FIRST_ASSUM(MP_TAC o SPEC `N:num` o MATCH_MP
SEQ_OFFSET) THEN
ASM_REWRITE_TAC[]]]);;
let INTERIOR_CONVEX_HULL_EXPLICIT = prove
(`!s:real^N->bool.
~(
affine_dependent s)
==> interior(convex hull s) =
if
CARD(s) <= dimindex(:N) then {}
else {y | ?u. (!x. x
IN s ==> &0 < u x /\ u x < &1) /\
sum s u = &1 /\
vsum s (\x. u x % x) = y}`,
REPEAT STRIP_TAC THEN
ASM_SIMP_TAC[
INTERIOR_CONVEX_HULL_EXPLICIT_MINIMAL] THEN
COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
REWRITE_TAC[
EXTENSION;
IN_ELIM_THM] THEN X_GEN_TAC `v:real^N` THEN
AP_TERM_TAC THEN REWRITE_TAC[
FUN_EQ_THM] THEN X_GEN_TAC `u:real^N->real` THEN
EQ_TAC THEN STRIP_TAC THEN ASM_SIMP_TAC[] THEN
X_GEN_TAC `x:real^N` THEN DISCH_TAC THEN
MP_TAC(ISPEC `s:real^N->bool`
CHOOSE_SUBSET) THEN
ASM_SIMP_TAC[
AFFINE_INDEPENDENT_IMP_FINITE] THEN
DISCH_THEN(MP_TAC o SPEC `2`) THEN ANTS_TAC THENL
[FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (ARITH_RULE
`~(c <= n) ==> 1 <= n ==> 2 <= c`)) THEN
REWRITE_TAC[
DIMINDEX_GE_1];
ALL_TAC] THEN
CONV_TAC(ONCE_DEPTH_CONV HAS_SIZE_CONV) THEN
REWRITE_TAC[
SUBSET] THEN
DISCH_THEN(X_CHOOSE_THEN `t:real^N->bool` (CONJUNCTS_THEN2 ASSUME_TAC
MP_TAC)) THEN
DISCH_THEN(X_CHOOSE_THEN `a:real^N` (X_CHOOSE_THEN `b:real^N`
STRIP_ASSUME_TAC)) THEN
SUBGOAL_THEN `?y:real^N. y
IN s /\ ~(y = x)` STRIP_ASSUME_TAC THENL
[ASM SET_TAC[]; ALL_TAC] THEN
SUBGOAL_THEN `sum {x,y} u <= sum s (u:real^N->real)` MP_TAC THENL
[MATCH_MP_TAC
SUM_SUBSET_SIMPLE THEN
ASM_SIMP_TAC[
AFFINE_INDEPENDENT_IMP_FINITE;
REAL_LT_IMP_LE;
IN_DIFF] THEN
ASM SET_TAC[];
ALL_TAC] THEN
ASM_SIMP_TAC[
SUM_CLAUSES;
FINITE_INSERT;
FINITE_EMPTY] THEN
ASM_REWRITE_TAC[
IN_INSERT;
NOT_IN_EMPTY] THEN
MATCH_MP_TAC(REAL_ARITH `&0 < y ==> x + y + &0 <= &1 ==> x < &1`) THEN
ASM_SIMP_TAC[]);;
let INTERIOR_CONVEX_HULL_3_MINIMAL = prove
(`!a b c:real^2.
~collinear{a,b,c}
==> interior(convex hull {a,b,c}) =
{v | ?x y z. &0 < x /\
&0 < y /\
&0 < z /\
x + y + z = &1 /\
x % a + y % b + z % c = v}`,
let INTERIOR_CONVEX_HULL_3 = prove
(`!a b c:real^2.
~collinear{a,b,c}
==> interior(convex hull {a,b,c}) =
{v | ?x y z. &0 < x /\ x < &1 /\
&0 < y /\ y < &1 /\
&0 < z /\ z < &1 /\
x + y + z = &1 /\
x % a + y % b + z % c = v}`,
let SIMPLEX_EXPLICIT = prove
(`!s:real^N->bool.
FINITE s /\ ~(vec 0
IN s)
==> convex hull (vec 0
INSERT s) =
{ y | ?u. (!x. x
IN s ==> &0 <= u x) /\
sum s u <= &1 /\
vsum s (\x. u x % x) = y}`,
REPEAT STRIP_TAC THEN ASM_SIMP_TAC[
CONVEX_HULL_FINITE;
FINITE_INSERT] THEN
REWRITE_TAC[
EXTENSION;
IN_ELIM_THM] THEN X_GEN_TAC `y:real^N` THEN
ASM_SIMP_TAC[
SUM_CLAUSES;
VSUM_CLAUSES;
IN_INSERT] THEN
REWRITE_TAC[
VECTOR_MUL_RZERO;
VECTOR_ADD_LID] THEN
EQ_TAC THEN DISCH_THEN(X_CHOOSE_THEN `u:real^N->real` STRIP_ASSUME_TAC) THENL
[EXISTS_TAC `u:real^N->real` THEN ASM_SIMP_TAC[
REAL_LE_REFL] THEN
FIRST_X_ASSUM(MP_TAC o SPEC `vec 0:real^N`) THEN REWRITE_TAC[] THEN
ASM_REAL_ARITH_TAC;
EXISTS_TAC `\x:real^N. if x = vec 0 then &1 - sum (s:real^N->bool) u
else u(x)` THEN
ASM_REWRITE_TAC[] THEN REPEAT CONJ_TAC THENL
[X_GEN_TAC `x:real^N` THEN ASM_CASES_TAC `x:real^N = vec 0` THEN
ASM_REWRITE_TAC[
REAL_SUB_LE];
MATCH_MP_TAC(REAL_ARITH `s = t ==> &1 - s + t = &1`) THEN
MATCH_MP_TAC
SUM_EQ THEN ASM_MESON_TAC[];
FIRST_X_ASSUM(SUBST1_TAC o SYM) THEN
MATCH_MP_TAC
VSUM_EQ THEN ASM_MESON_TAC[]]]);;
let STD_SIMPLEX = prove
(`convex hull (vec 0
INSERT { basis i | 1 <= i /\ i <= dimindex(:N)}) =
{x:real^N | (!i. 1 <= i /\ i <= dimindex(:N) ==> &0 <= x$i) /\
sum (1..dimindex(:N)) (\i. x$i) <= &1 }`,
let INTERIOR_STD_SIMPLEX = prove
(`interior
(convex hull (vec 0
INSERT { basis i | 1 <= i /\ i <= dimindex(:N)})) =
{x:real^N | (!i. 1 <= i /\ i <= dimindex(:N) ==> &0 < x$i) /\
sum (1..dimindex(:N)) (\i. x$i) < &1 }`,