(* ========================================================================= *)
(* Lebsegue measure, measurable functions (defined via the gauge integral). *)
(* *)
(* (c) Copyright, John Harrison 1998-2008 *)
(* ========================================================================= *)
needs "Library/card.ml";;
needs "Library/permutations.ml";;
needs "Multivariate/integration.ml";;
needs "Multivariate/determinants.ml";;
prioritize_real();;
(* ------------------------------------------------------------------------- *)
(* Lebesgue measure in the case where the measure is finite. This is our *)
(* default notion of "measurable", but we also define "lebesgue_measurable" *)
(* further down. Note that in neither case do we assume the set is bounded. *)
(* ------------------------------------------------------------------------- *)
parse_as_infix("has_measure",(12,"right"));;
let MEASURE_INTERVAL = prove
(`(!a b:real^N. measure(interval[a,b]) = content(interval[a,b])) /\
(!a b:real^N. measure(interval(a,b)) = content(interval[a,b]))`,
let MEASURE_INTERVAL_1 = prove
(`(!a b:real^1. measure(interval[a,b]) =
if drop a <= drop b then drop b - drop a else &0) /\
(!a b:real^1. measure(interval(a,b)) =
if drop a <= drop b then drop b - drop a else &0)`,
let MEASURE_INTERVAL_1_ALT = prove
(`(!a b:real^1. measure(interval[a,b]) =
if drop a < drop b then drop b - drop a else &0) /\
(!a b:real^1. measure(interval(a,b)) =
if drop a < drop b then drop b - drop a else &0)`,
let MEASURE_INTERVAL_2 = prove
(`(!a b:real^2. measure(interval[a,b]) =
if a$1 <= b$1 /\ a$2 <= b$2
then (b$1 - a$1) * (b$2 - a$2)
else &0) /\
(!a b:real^2. measure(interval(a,b)) =
if a$1 <= b$1 /\ a$2 <= b$2
then (b$1 - a$1) * (b$2 - a$2)
else &0)`,
let MEASURE_INTERVAL_2_ALT = prove
(`(!a b:real^2. measure(interval[a,b]) =
if a$1 < b$1 /\ a$2 < b$2
then (b$1 - a$1) * (b$2 - a$2)
else &0) /\
(!a b:real^2. measure(interval(a,b)) =
if a$1 < b$1 /\ a$2 < b$2
then (b$1 - a$1) * (b$2 - a$2)
else &0)`,
let MEASURE_INTERVAL_3 = prove
(`(!a b:real^3. measure(interval[a,b]) =
if a$1 <= b$1 /\ a$2 <= b$2 /\ a$3 <= b$3
then (b$1 - a$1) * (b$2 - a$2) * (b$3 - a$3)
else &0) /\
(!a b:real^3. measure(interval(a,b)) =
if a$1 <= b$1 /\ a$2 <= b$2 /\ a$3 <= b$3
then (b$1 - a$1) * (b$2 - a$2) * (b$3 - a$3)
else &0)`,
let MEASURE_INTERVAL_3_ALT = prove
(`(!a b:real^3. measure(interval[a,b]) =
if a$1 < b$1 /\ a$2 < b$2 /\ a$3 < b$3
then (b$1 - a$1) * (b$2 - a$2) * (b$3 - a$3)
else &0) /\
(!a b:real^3. measure(interval(a,b)) =
if a$1 < b$1 /\ a$2 < b$2 /\ a$3 < b$3
then (b$1 - a$1) * (b$2 - a$2) * (b$3 - a$3)
else &0)`,
let MEASURE_INTERVAL_4 = prove
(`(!a b:real^4. measure(interval[a,b]) =
if a$1 <= b$1 /\ a$2 <= b$2 /\ a$3 <= b$3 /\ a$4 <= b$4
then (b$1 - a$1) * (b$2 - a$2) * (b$3 - a$3) * (b$4 - a$4)
else &0) /\
(!a b:real^4. measure(interval(a,b)) =
if a$1 <= b$1 /\ a$2 <= b$2 /\ a$3 <= b$3 /\ a$4 <= b$4
then (b$1 - a$1) * (b$2 - a$2) * (b$3 - a$3) * (b$4 - a$4)
else &0)`,
let MEASURE_INTERVAL_4_ALT = prove
(`(!a b:real^4. measure(interval[a,b]) =
if a$1 < b$1 /\ a$2 < b$2 /\ a$3 < b$3 /\ a$4 < b$4
then (b$1 - a$1) * (b$2 - a$2) * (b$3 - a$3) * (b$4 - a$4)
else &0) /\
(!a b:real^4. measure(interval(a,b)) =
if a$1 < b$1 /\ a$2 < b$2 /\ a$3 < b$3 /\ a$4 < b$4
then (b$1 - a$1) * (b$2 - a$2) * (b$3 - a$3) * (b$4 - a$4)
else &0)`,
let NEGLIGIBLE_INTERVAL = prove
(`(!a b. negligible(interval[a,b]) <=> interval(a,b) = {}) /\
(!a b. negligible(interval(a,b)) <=> interval(a,b) = {})`,
let MEASURABLE_DIFF = prove
(`!s t:real^N->bool. measurable s /\ measurable t ==> measurable (s
DIFF t)`,
SUBGOAL_THEN
`!s t:real^N->bool. measurable s /\ measurable t /\ t
SUBSET s
==> measurable (s
DIFF t)`
ASSUME_TAC THENL
[REWRITE_TAC[measurable] THEN MESON_TAC[
HAS_MEASURE_DIFF_SUBSET];
ONCE_REWRITE_TAC[SET_RULE `s
DIFF t = s
DIFF (s
INTER t)`] THEN
REPEAT STRIP_TAC THEN
FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_SIMP_TAC[
MEASURABLE_INTER] THEN
SET_TAC[]]);;
let MEASURABLE_INNER_OUTER = prove
(`!s:real^N->bool.
measurable s <=>
!e. &0 < e
==> ?t u. t
SUBSET s /\ s
SUBSET u /\
measurable t /\ measurable u /\
abs(measure t - measure u) < e`,
GEN_TAC THEN EQ_TAC THEN DISCH_TAC THENL
[GEN_TAC THEN DISCH_TAC THEN REPEAT(EXISTS_TAC `s:real^N->bool`) THEN
ASM_REWRITE_TAC[
SUBSET_REFL;
REAL_SUB_REFL;
REAL_ABS_NUM];
ALL_TAC] THEN
REWRITE_TAC[
MEASURABLE_INTEGRABLE] THEN MATCH_MP_TAC
INTEGRABLE_STRADDLE THEN
X_GEN_TAC `e:real` THEN DISCH_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPEC `e:real`) THEN
ASM_REWRITE_TAC[
LEFT_IMP_EXISTS_THM] THEN
MAP_EVERY X_GEN_TAC [`t:real^N->bool`; `u:real^N->bool`] THEN STRIP_TAC THEN
MAP_EVERY EXISTS_TAC
[`(\x. if x
IN t then vec 1 else vec 0):real^N->real^1`;
`(\x. if x
IN u then vec 1 else vec 0):real^N->real^1`;
`lift(measure(t:real^N->bool))`;
`lift(measure(u:real^N->bool))`] THEN
ASM_REWRITE_TAC[GSYM
HAS_MEASURE; GSYM
HAS_MEASURE_MEASURE] THEN
ASM_REWRITE_TAC[GSYM
LIFT_SUB;
NORM_LIFT] THEN REPEAT STRIP_TAC THEN
REPEAT(COND_CASES_TAC THEN
ASM_REWRITE_TAC[
DROP_VEC;
REAL_POS;
REAL_LE_REFL]) THEN
ASM SET_TAC[]);;
let HAS_MEASURE_INNER_OUTER = prove
(`!s:real^N->bool m.
s
has_measure m <=>
(!e. &0 < e ==> ?t. t
SUBSET s /\ measurable t /\
m - e < measure t) /\
(!e. &0 < e ==> ?u. s
SUBSET u /\ measurable u /\
measure u < m + e)`,
REPEAT GEN_TAC THEN
GEN_REWRITE_TAC LAND_CONV [
HAS_MEASURE_MEASURABLE_MEASURE] THEN EQ_TAC THENL
[REPEAT STRIP_TAC THEN EXISTS_TAC `s:real^N->bool` THEN
ASM_REWRITE_TAC[
SUBSET_REFL] THEN ASM_REAL_ARITH_TAC;
ALL_TAC] THEN
DISCH_THEN(CONJUNCTS_THEN2 (LABEL_TAC "t") (LABEL_TAC "u")) THEN
MATCH_MP_TAC(TAUT `a /\ (a ==> b) ==> a /\ b`) THEN CONJ_TAC THENL
[GEN_REWRITE_TAC I [
MEASURABLE_INNER_OUTER] THEN
X_GEN_TAC `e:real` THEN DISCH_TAC THEN
REMOVE_THEN "u" (MP_TAC o SPEC `e / &2`) THEN
REMOVE_THEN "t" (MP_TAC o SPEC `e / &2`) THEN
ASM_SIMP_TAC[
REAL_LT_DIV;
REAL_OF_NUM_LT; ARITH] THEN
REWRITE_TAC[IMP_IMP;
LEFT_AND_EXISTS_THM] THEN
REWRITE_TAC[
RIGHT_AND_EXISTS_THM] THEN
REPEAT(MATCH_MP_TAC
MONO_EXISTS THEN GEN_TAC) THEN
STRIP_TAC THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC(REAL_ARITH
`&0 < e /\ t <= u /\ m - e / &2 < t /\ u < m + e / &2
==> abs(t - u) < e`) THEN
ASM_REWRITE_TAC[] THEN MATCH_MP_TAC
MEASURE_SUBSET THEN
ASM_REWRITE_TAC[] THEN ASM SET_TAC[];
DISCH_TAC THEN MATCH_MP_TAC(REAL_ARITH
`~(&0 < x - y) /\ ~(&0 < y - x) ==> x = y`) THEN
CONJ_TAC THEN DISCH_TAC THENL
[REMOVE_THEN "u" (MP_TAC o SPEC `measure(s:real^N->bool) - m`) THEN
ASM_REWRITE_TAC[
REAL_SUB_ADD2; GSYM
REAL_NOT_LE];
REMOVE_THEN "t" (MP_TAC o SPEC `m - measure(s:real^N->bool)`) THEN
ASM_REWRITE_TAC[
REAL_SUB_SUB2; GSYM
REAL_NOT_LE]] THEN
ASM_MESON_TAC[
MEASURE_SUBSET]]);;
let MEASURE_LIMIT = prove
(`!s:real^N->bool e.
measurable s /\ &0 < e
==> ?B. &0 < B /\
!a b. ball(vec 0,B)
SUBSET interval[a,b]
==> abs(measure(s
INTER interval[a,b]) -
measure s) < e`,
let STRETCH_GALOIS = prove
(`!x:real^N y:real^N m.
(!k. 1 <= k /\ k <= dimindex(:N) ==> ~(m k = &0))
==> ((y = (lambda k. m k * x$k)) <=> (lambda k. inv(m k) * y$k) = x)`,
REPEAT GEN_TAC THEN SIMP_TAC[
CART_EQ;
LAMBDA_BETA] THEN
MATCH_MP_TAC(MESON[]
`(!x. p x ==> (q x <=> r x))
==> (!x. p x) ==> ((!x. q x) <=> (!x. r x))`) THEN
GEN_TAC THEN ASM_CASES_TAC `1 <= k /\ k <= dimindex(:N)` THEN
ASM_REWRITE_TAC[] THEN CONV_TAC REAL_FIELD);;
let HAS_MEASURE_NESTED_UNIONS = prove
(`!s:num->real^N->bool B.
(!n. measurable(s n)) /\
(!n. measure(s n) <= B) /\
(!n. s(n)
SUBSET s(SUC n))
==> measurable(
UNIONS { s(n) | n
IN (:num) }) /\
((\n. lift(measure(s n)))
--> lift(measure(
UNIONS { s(n) | n
IN (:num) })))
sequentially`,
let HAS_MEASURE_NESTED_INTERS = prove
(`!s:num->real^N->bool.
(!n. measurable(s n)) /\
(!n. s(SUC n)
SUBSET s(n))
==> measurable(
INTERS {s n | n
IN (:num)}) /\
((\n. lift(measure (s n))) -->
lift(measure (
INTERS {s n | n
IN (:num)}))) sequentially`,
GEN_TAC THEN STRIP_TAC THEN
MP_TAC(ISPECL
[`\n. (s:num->real^N->bool) 0
DIFF s n`; `measure(s 0:real^N->bool)`]
HAS_MEASURE_NESTED_UNIONS) THEN
ASM_SIMP_TAC[
MEASURABLE_DIFF] THEN ANTS_TAC THENL
[CONJ_TAC THEN X_GEN_TAC `n:num` THENL
[MATCH_MP_TAC
MEASURE_SUBSET THEN
ASM_SIMP_TAC[
MEASURABLE_DIFF;
SUBSET_DIFF] THEN SET_TAC[];
REPEAT(FIRST_X_ASSUM(MP_TAC o SPEC `n:num`)) THEN SET_TAC[]];
SUBGOAL_THEN
`
UNIONS {s 0
DIFF s n | n
IN (:num)} =
s 0
DIFF INTERS {s n :real^N->bool | n
IN (:num)}`
(fun th -> REWRITE_TAC[th])
THENL [REWRITE_TAC[
DIFF_INTERS] THEN SET_TAC[]; ALL_TAC] THEN
MATCH_MP_TAC MONO_AND THEN CONJ_TAC THENL
[DISCH_TAC THEN
SUBGOAL_THEN
`measurable(s 0
DIFF (s 0
DIFF INTERS {s n | n
IN (:num)})
:real^N->bool)`
MP_TAC THENL [ASM_SIMP_TAC[
MEASURABLE_DIFF]; ALL_TAC] THEN
MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC THEN MATCH_MP_TAC(SET_RULE
`t
SUBSET s ==> s
DIFF (s
DIFF t) = t`) THEN
REWRITE_TAC[
SUBSET;
INTERS_GSPEC;
IN_ELIM_THM] THEN SET_TAC[];
MP_TAC(ISPECL [`sequentially`; `lift(measure(s 0:real^N->bool))`]
LIM_CONST) THEN REWRITE_TAC[IMP_IMP] THEN
DISCH_THEN(MP_TAC o MATCH_MP
LIM_SUB) THEN
REWRITE_TAC[GSYM
LIFT_SUB] THEN MATCH_MP_TAC EQ_IMP THEN
AP_THM_TAC THEN BINOP_TAC THEN REWRITE_TAC[
LIFT_EQ;
FUN_EQ_THM] THEN
REPEAT GEN_TAC THEN
REWRITE_TAC[REAL_ARITH `s - m:real = n <=> m = s - n`] THEN
MATCH_MP_TAC
MEASURE_DIFF_SUBSET THEN
ASM_SIMP_TAC[
MEASURABLE_COUNTABLE_INTERS] THENL
[ALL_TAC; SET_TAC[]] THEN
MP_TAC(ISPEC `\m n:num. (s n :real^N->bool)
SUBSET (s m)`
TRANSITIVE_STEPWISE_LE) THEN
ASM_REWRITE_TAC[] THEN
ANTS_TAC THENL [SET_TAC[]; MESON_TAC[
LE_0]]]]);;
let MEASURE_FRONTIER = prove
(`!s:real^N->bool.
bounded s
==> measure(frontier s) = measure(closure s) - measure(interior s)`,
let MEASURE_CLOSURE = prove
(`!s:real^N->bool.
bounded s /\ negligible(frontier s)
==> measure(closure s) = measure s`,
let MEASURE_INTERIOR = prove
(`!s:real^N->bool.
bounded s /\ negligible(frontier s)
==> measure(interior s) = measure s`,
let STARLIKE_NEGLIGIBLE_BOUNDED_MEASURABLE = prove
(`!s. measurable s /\ bounded s /\
(!c x:real^N. &0 <= c /\ x
IN s /\ (c % x)
IN s ==> c = &1)
==> negligible s`,
REPEAT STRIP_TAC THEN
SUBGOAL_THEN `~(&0 < measure(s:real^N->bool))`
(fun th -> ASM_MESON_TAC[th;
MEASURABLE_MEASURE_POS_LT]) THEN
DISCH_TAC THEN
MP_TAC(SPEC `(vec 0:real^N)
INSERT s`
BOUNDED_SUBSET_CLOSED_INTERVAL_SYMMETRIC) THEN
ASM_SIMP_TAC[
BOUNDED_INSERT;
COMPACT_IMP_BOUNDED;
NOT_EXISTS_THM] THEN
X_GEN_TAC `a:real^N` THEN REWRITE_TAC[
INSERT_SUBSET] THEN STRIP_TAC THEN
SUBGOAL_THEN
`?N.
EVEN N /\ &0 < &N /\
measure(interval[--a:real^N,a])
< (&N * measure(s:real^N->bool)) / &4 pow dimindex (:N)`
STRIP_ASSUME_TAC THENL
[FIRST_ASSUM(MP_TAC o SPEC
`measure(interval[--a:real^N,a]) * &4 pow (dimindex(:N))` o
MATCH_MP
REAL_ARCH) THEN
SIMP_TAC[
REAL_LT_RDIV_EQ;
REAL_POW_LT;
REAL_OF_NUM_LT; ARITH] THEN
SIMP_TAC[GSYM
REAL_LT_LDIV_EQ; ASSUME `&0 < measure(s:real^N->bool)`] THEN
DISCH_THEN(X_CHOOSE_THEN `N:num` STRIP_ASSUME_TAC) THEN
EXISTS_TAC `2 * (N DIV 2 + 1)` THEN REWRITE_TAC[
EVEN_MULT; ARITH] THEN
CONJ_TAC THENL [ARITH_TAC; ALL_TAC] THEN
FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH
`x < a ==> a <= b ==> x < b`)) THEN
REWRITE_TAC[REAL_OF_NUM_LE] THEN ARITH_TAC;
ALL_TAC] THEN
MP_TAC(ISPECL [`
UNIONS (
IMAGE (\m.
IMAGE (\x:real^N. (&m / &N) % x) s)
(1..N))`;
`interval[--a:real^N,a]`]
MEASURE_SUBSET) THEN
MP_TAC(ISPECL [`measure:(real^N->bool)->real`;
`
IMAGE (\m.
IMAGE (\x:real^N. (&m / &N) % x) s) (1..N)`]
HAS_MEASURE_DISJOINT_UNIONS) THEN
SIMP_TAC[
FINITE_IMAGE;
FINITE_NUMSEG;
IMP_CONJ] THEN
REWRITE_TAC[
RIGHT_FORALL_IMP_THM;
FORALL_IN_IMAGE] THEN ANTS_TAC THENL
[REPEAT STRIP_TAC THEN REWRITE_TAC[GSYM
HAS_MEASURE_MEASURE] THEN
MATCH_MP_TAC
MEASURABLE_SCALING THEN ASM_REWRITE_TAC[];
ALL_TAC] THEN
REWRITE_TAC[
RIGHT_IMP_FORALL_THM; IMP_IMP] THEN
ONCE_REWRITE_TAC[TAUT `(a /\ b) /\ ~c ==> d <=> a /\ b /\ ~d ==> c`] THEN
SUBGOAL_THEN
`!m n. m
IN 1..N /\ n
IN 1..N /\
~(
DISJOINT (
IMAGE (\x:real^N. &m / &N % x) s)
(
IMAGE (\x. &n / &N % x) s))
==> m = n`
ASSUME_TAC THENL
[MAP_EVERY X_GEN_TAC [`m:num`; `n:num`] THEN
REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
REWRITE_TAC[
DISJOINT; GSYM
MEMBER_NOT_EMPTY] THEN
REWRITE_TAC[
EXISTS_IN_IMAGE;
IN_INTER] THEN
DISCH_THEN(X_CHOOSE_THEN `x:real^N`
(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
REWRITE_TAC[
IN_IMAGE] THEN
DISCH_THEN(X_CHOOSE_THEN `y:real^N`
(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC)) THEN
DISCH_THEN(MP_TAC o AP_TERM `(%) (&N / &m) :real^N->real^N`) THEN
SUBGOAL_THEN `~(&N = &0) /\ ~(&m = &0)` STRIP_ASSUME_TAC THENL
[REWRITE_TAC[REAL_OF_NUM_EQ] THEN
REPEAT(FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [
IN_NUMSEG])) THEN
ARITH_TAC;
ALL_TAC] THEN
FIRST_X_ASSUM(ASSUME_TAC o GEN_REWRITE_RULE (BINDER_CONV o BINDER_CONV)
[GSYM CONTRAPOS_THM]) THEN
ASM_SIMP_TAC[
VECTOR_MUL_ASSOC; REAL_FIELD
`~(x = &0) /\ ~(y = &0) ==> x / y * y / x = &1`] THEN
ASM_SIMP_TAC[REAL_FIELD
`~(x = &0) /\ ~(y = &0) ==> x / y * z / x = z / y`] THEN
REWRITE_TAC[
VECTOR_MUL_LID] THEN DISCH_THEN SUBST_ALL_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPECL [`&n / &m`; `y:real^N`]) THEN
ASM_SIMP_TAC[
REAL_LE_DIV;
REAL_POS; REAL_FIELD
`~(y = &0) ==> (x / y = &1 <=> x = y)`] THEN
REWRITE_TAC[REAL_OF_NUM_EQ;
EQ_SYM_EQ];
ALL_TAC] THEN
ANTS_TAC THENL [ASM_MESON_TAC[]; DISCH_TAC] THEN
REWRITE_TAC[NOT_IMP] THEN REPEAT CONJ_TAC THENL
[REWRITE_TAC[measurable] THEN ASM_MESON_TAC[];
REWRITE_TAC[
MEASURABLE_INTERVAL];
REWRITE_TAC[
UNIONS_SUBSET;
FORALL_IN_IMAGE] THEN
REWRITE_TAC[
SUBSET;
FORALL_IN_IMAGE] THEN
X_GEN_TAC `n:num` THEN DISCH_TAC THEN X_GEN_TAC `x:real^N` THEN
DISCH_TAC THEN
MP_TAC(ISPECL [`--a:real^N`; `a:real^N`]
CONVEX_INTERVAL) THEN
DISCH_THEN(MP_TAC o REWRITE_RULE[
CONVEX_ALT] o CONJUNCT1) THEN
DISCH_THEN(MP_TAC o SPECL [`vec 0:real^N`; `x:real^N`; `&n / &N`]) THEN
ASM_REWRITE_TAC[
VECTOR_MUL_RZERO;
VECTOR_ADD_LID] THEN
DISCH_THEN MATCH_MP_TAC THEN SIMP_TAC[
REAL_LE_DIV;
REAL_POS] THEN
CONJ_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [
IN_NUMSEG]) THEN
DISCH_THEN(MP_TAC o MATCH_MP (ARITH_RULE
`1 <= n /\ n <= N ==> 0 < N /\ n <= N`)) THEN
SIMP_TAC[GSYM REAL_OF_NUM_LE; GSYM
REAL_OF_NUM_LT;
REAL_LE_LDIV_EQ] THEN
SIMP_TAC[REAL_MUL_LID];
ALL_TAC] THEN
FIRST_X_ASSUM(SUBST1_TAC o MATCH_MP
MEASURE_UNIQUE) THEN
ASM_SIMP_TAC[
MEASURE_SCALING;
REAL_NOT_LE] THEN
FIRST_X_ASSUM(K ALL_TAC o SPEC `&0`) THEN
MATCH_MP_TAC
REAL_LTE_TRANS THEN EXISTS_TAC
`sum (1..N) (measure o (\m.
IMAGE (\x:real^N. &m / &N % x) s))` THEN
CONJ_TAC THENL
[ALL_TAC;
MATCH_MP_TAC
REAL_EQ_IMP_LE THEN CONV_TAC SYM_CONV THEN
MATCH_MP_TAC
SUM_IMAGE THEN REWRITE_TAC[] THEN
REPEAT STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
ASM_REWRITE_TAC[SET_RULE `
DISJOINT s s <=> s = {}`;
IMAGE_EQ_EMPTY] THEN
DISCH_THEN SUBST_ALL_TAC THEN
ASM_MESON_TAC[
REAL_LT_REFL;
MEASURE_EMPTY]] THEN
FIRST_X_ASSUM(K ALL_TAC o SPEC `0`) THEN
ASM_SIMP_TAC[
o_DEF;
MEASURE_SCALING;
SUM_RMUL] THEN
FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH
`x < a ==> a <= b ==> x < b`)) THEN
ASM_SIMP_TAC[
REAL_LE_LDIV_EQ;
REAL_POW_LT;
REAL_OF_NUM_LT; ARITH] THEN
ONCE_REWRITE_TAC[REAL_ARITH `(a * b) * c:real = (a * c) * b`] THEN
ASM_SIMP_TAC[
REAL_LE_RMUL_EQ] THEN REWRITE_TAC[GSYM
SUM_RMUL] THEN
REWRITE_TAC[GSYM
REAL_POW_MUL] THEN
REWRITE_TAC[
REAL_ABS_DIV;
REAL_ABS_NUM] THEN
FIRST_X_ASSUM(X_CHOOSE_THEN `M:num` SUBST_ALL_TAC o
GEN_REWRITE_RULE I [
EVEN_EXISTS]) THEN
REWRITE_TAC[GSYM REAL_OF_NUM_MUL] THEN
RULE_ASSUM_TAC(REWRITE_RULE[GSYM REAL_OF_NUM_MUL]) THEN
RULE_ASSUM_TAC(REWRITE_RULE[REAL_ARITH `&0 < &2 * x <=> &0 < x`]) THEN
ASM_SIMP_TAC[REAL_FIELD `&0 < y ==> x / (&2 * y) * &4 = x * &2 / y`] THEN
MATCH_MP_TAC
REAL_LE_TRANS THEN
EXISTS_TAC `sum(M..(2*M)) (\i. (&i * &2 / &M) pow dimindex (:N))` THEN
CONJ_TAC THENL
[ALL_TAC;
MATCH_MP_TAC
SUM_SUBSET_SIMPLE THEN
SIMP_TAC[
REAL_POW_LE;
REAL_LE_MUL;
REAL_LE_DIV;
REAL_POS] THEN
REWRITE_TAC[
IN_NUMSEG;
FINITE_NUMSEG;
SUBSET] THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [
REAL_OF_NUM_LT]) THEN
ARITH_TAC] THEN
MATCH_MP_TAC
REAL_LE_TRANS THEN
EXISTS_TAC `sum(M..(2*M)) (\i. &2)` THEN CONJ_TAC THENL
[REWRITE_TAC[
SUM_CONST_NUMSEG] THEN
REWRITE_TAC[ARITH_RULE `(2 * M + 1) - M = M + 1`] THEN
REWRITE_TAC[GSYM REAL_OF_NUM_ADD] THEN REAL_ARITH_TAC;
ALL_TAC] THEN
MATCH_MP_TAC
SUM_LE THEN REWRITE_TAC[
FINITE_NUMSEG;
IN_NUMSEG] THEN
X_GEN_TAC `n:num` THEN STRIP_TAC THEN
MATCH_MP_TAC
REAL_LE_TRANS THEN EXISTS_TAC `&2 pow (dimindex(:N))` THEN
CONJ_TAC THENL
[GEN_REWRITE_TAC LAND_CONV [GSYM
REAL_POW_1] THEN
MATCH_MP_TAC
REAL_POW_MONO THEN REWRITE_TAC[
DIMINDEX_GE_1] THEN
ARITH_TAC;
ALL_TAC] THEN
MATCH_MP_TAC
REAL_POW_LE2 THEN
REWRITE_TAC[
REAL_POS; ARITH;
real_div; REAL_MUL_ASSOC] THEN
ASM_SIMP_TAC[GSYM
real_div;
REAL_LE_RDIV_EQ] THEN
REWRITE_TAC[REAL_OF_NUM_MUL; REAL_OF_NUM_LE] THEN
UNDISCH_TAC `M:num <= n` THEN ARITH_TAC);;
let STARLIKE_NEGLIGIBLE_STRONG = prove
(`!s a. closed s /\
(!c x:real^N. &0 <= c /\ c < &1 /\ (a + x)
IN s
==> ~((a + c % x)
IN s))
==> negligible s`,
REPEAT GEN_TAC THEN STRIP_TAC THEN MATCH_MP_TAC
STARLIKE_NEGLIGIBLE THEN
EXISTS_TAC `a:real^N` THEN ASM_REWRITE_TAC[] THEN
MAP_EVERY X_GEN_TAC [`c:real`; `x:real^N`] THEN STRIP_TAC THEN
MATCH_MP_TAC(REAL_ARITH `~(x < y) /\ ~(y < x) ==> x = y`) THEN
STRIP_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN DISCH_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPECL [`inv c:real`; `c % x:real^N`]) THEN
ASM_REWRITE_TAC[
REAL_LE_INV_EQ;
VECTOR_MUL_ASSOC] THEN
ASM_SIMP_TAC[REAL_MUL_LINV; REAL_ARITH `&1 < c ==> ~(c = &0)`] THEN
ASM_REWRITE_TAC[
VECTOR_MUL_LID] THEN
GEN_REWRITE_TAC RAND_CONV [GSYM
REAL_INV_1] THEN
MATCH_MP_TAC
REAL_LT_INV2 THEN ASM_REWRITE_TAC[
REAL_LT_01]);;
let NEGLIGIBLE_HYPERPLANE = prove
(`!a b. ~(a = vec 0 /\ b = &0) ==> negligible {x:real^N | a dot x = b}`,
REPEAT GEN_TAC THEN ASM_CASES_TAC `a:real^N = vec 0` THEN
ASM_SIMP_TAC[
DOT_LZERO; SET_RULE `{x | F} = {}`;
NEGLIGIBLE_EMPTY] THEN
MATCH_MP_TAC
STARLIKE_NEGLIGIBLE THEN
SUBGOAL_THEN `?x:real^N. ~(a dot x = b)` MP_TAC THENL
[MATCH_MP_TAC(MESON[] `!a:real^N. P a \/ P(--a) ==> ?x. P x`) THEN
EXISTS_TAC `a:real^N` THEN REWRITE_TAC[
DOT_RNEG] THEN
MATCH_MP_TAC(REAL_ARITH `~(a = &0) ==> ~(a = b) \/ ~(--a = b)`) THEN
ASM_REWRITE_TAC[
DOT_EQ_0];
ALL_TAC] THEN
MATCH_MP_TAC
MONO_EXISTS THEN X_GEN_TAC `c:real^N` THEN DISCH_TAC THEN
REWRITE_TAC[
CLOSED_HYPERPLANE;
IN_ELIM_THM;
DOT_RADD;
DOT_RMUL] THEN
MAP_EVERY X_GEN_TAC [`t:real`; `y:real^N`] THEN
DISCH_THEN(MP_TAC o MATCH_MP (REAL_ARITH
`&0 <= t /\ ac + ay = b /\ ac + t * ay = b
==> ((ay = &0 ==> ac = b) /\ (t - &1) * ay = &0)`)) THEN
ASM_SIMP_TAC[
REAL_ENTIRE;
REAL_SUB_0] THEN CONV_TAC TAUT);;
let COVERING_LEMMA = prove
(`!a b:real^N s g.
s
SUBSET interval[a,b] /\ ~(interval(a,b) = {}) /\ gauge g
==> ?d.
COUNTABLE d /\
(!k. k
IN d ==> k
SUBSET interval[a,b] /\ ~(interior k = {}) /\
(?c d. k = interval[c,d])) /\
(!k1 k2. k1
IN d /\ k2
IN d /\ ~(k1 = k2)
==> interior k1
INTER interior k2 = {}) /\
(!k. k
IN d ==> ?x. x
IN (s
INTER k) /\ k
SUBSET g(x)) /\
(!u v. interval[u,v]
IN d
==> ?n. !i. 1 <= i /\ i <= dimindex(:N)
==> v$i - u$i = (b$i - a$i) / &2 pow n) /\
s
SUBSET UNIONS d`,
REPEAT STRIP_TAC THEN
SUBGOAL_THEN
`?d.
COUNTABLE d /\
(!k. k
IN d ==> k
SUBSET interval[a,b] /\ ~(interior k = {}) /\
(?c d:real^N. k = interval[c,d])) /\
(!k1 k2. k1
IN d /\ k2
IN d
==> k1
SUBSET k2 \/ k2
SUBSET k1 \/
interior k1
INTER interior k2 = {}) /\
(!x. x
IN s ==> ?k. k
IN d /\ x
IN k /\ k
SUBSET g(x)) /\
(!u v. interval[u,v]
IN d
==> ?n. !i. 1 <= i /\ i <= dimindex(:N)
==> v$i - u$i = (b$i - a$i) / &2 pow n) /\
(!k. k
IN d ==>
FINITE {l | l
IN d /\ k
SUBSET l})`
ASSUME_TAC THENL
[EXISTS_TAC
`
IMAGE (\(n,v).
interval[(lambda i. a$i + &(v$i) / &2 pow n *
((b:real^N)$i - (a:real^N)$i)):real^N,
(lambda i. a$i + (&(v$i) + &1) / &2 pow n * (b$i - a$i))])
{n,v | n
IN (:num) /\
v
IN {v:num^N | !i. 1 <= i /\ i <= dimindex(:N)
==> v$i < 2
EXP n}}` THEN
CONJ_TAC THENL
[MATCH_MP_TAC
COUNTABLE_IMAGE THEN
MATCH_MP_TAC
COUNTABLE_PRODUCT_DEPENDENT THEN
REWRITE_TAC[
NUM_COUNTABLE;
IN_UNIV] THEN
GEN_TAC THEN MATCH_MP_TAC
FINITE_IMP_COUNTABLE THEN
MATCH_MP_TAC
FINITE_CART THEN REWRITE_TAC[
FINITE_NUMSEG_LT];
ALL_TAC] THEN
CONJ_TAC THENL
[REWRITE_TAC[
FORALL_IN_IMAGE;
FORALL_PAIR_THM] THEN
MAP_EVERY X_GEN_TAC [`n:num`; `v:num^N`] THEN
REWRITE_TAC[
IN_ELIM_PAIR_THM] THEN
REWRITE_TAC[
IN_ELIM_THM;
IN_UNIV] THEN DISCH_TAC THEN
REWRITE_TAC[
CONJ_ASSOC] THEN CONJ_TAC THENL [ALL_TAC; MESON_TAC[]] THEN
REWRITE_TAC[
INTERIOR_CLOSED_INTERVAL] THEN
SIMP_TAC[
INTERVAL_NE_EMPTY;
SUBSET_INTERVAL;
LAMBDA_BETA] THEN
RULE_ASSUM_TAC(REWRITE_RULE[
INTERVAL_NE_EMPTY]) THEN
ASM_SIMP_TAC[
REAL_LE_LADD;
REAL_LE_RMUL_EQ;
REAL_SUB_LT;
REAL_LE_MUL_EQ;
REAL_LT_LADD;
REAL_LT_RMUL_EQ;
REAL_LE_ADDR; REAL_ARITH
`a + x * (b - a) <= b <=> &0 <= (&1 - x) * (b - a)`] THEN
SIMP_TAC[
REAL_LE_DIV2_EQ;
REAL_LT_DIV2_EQ;
REAL_LT_POW2] THEN
REWRITE_TAC[REAL_ARITH `x <= x + &1 /\ x < x + &1`] THEN
REWRITE_TAC[
REAL_SUB_LE] THEN
SIMP_TAC[
REAL_LE_LDIV_EQ;
REAL_LE_RDIV_EQ;
REAL_LT_POW2] THEN
REWRITE_TAC[
REAL_MUL_LZERO;
REAL_POS; REAL_MUL_LID] THEN
SIMP_TAC[REAL_OF_NUM_ADD;
REAL_OF_NUM_POW; REAL_OF_NUM_LE] THEN
ASM_SIMP_TAC[ARITH_RULE `x + 1 <= y <=> x < y`;
REAL_LT_IMP_LE];
ALL_TAC] THEN
CONJ_TAC THENL
[ONCE_REWRITE_TAC[
IMP_CONJ] THEN
REWRITE_TAC[
FORALL_IN_IMAGE;
FORALL_PAIR_THM;
RIGHT_FORALL_IMP_THM] THEN
REWRITE_TAC[
IN_ELIM_PAIR_THM;
IN_UNIV] THEN REWRITE_TAC[
IN_ELIM_THM] THEN
REWRITE_TAC[
RIGHT_IMP_FORALL_THM] THEN
GEN_REWRITE_TAC BINDER_CONV [
SWAP_FORALL_THM] THEN
MATCH_MP_TAC
WLOG_LE THEN CONJ_TAC THENL
[REPEAT GEN_TAC THEN
GEN_REWRITE_TAC RAND_CONV [
SWAP_FORALL_THM] THEN
REPEAT(AP_TERM_TAC THEN ABS_TAC) THEN SET_TAC[];
ALL_TAC] THEN
MAP_EVERY X_GEN_TAC [`m:num`; `n:num`] THEN DISCH_TAC THEN
MAP_EVERY X_GEN_TAC [`v:num^N`; `w:num^N`] THEN REPEAT DISCH_TAC THEN
REWRITE_TAC[
INTERIOR_CLOSED_INTERVAL;
SUBSET_INTERVAL] THEN
SIMP_TAC[
DISJOINT_INTERVAL;
LAMBDA_BETA] THEN
MATCH_MP_TAC(TAUT `p \/ q \/ r ==> (a ==> p) \/ (b ==> q) \/ r`) THEN
ONCE_REWRITE_TAC[TAUT `a /\ b /\ c <=> ~(a /\ b ==> ~c)`] THEN
RULE_ASSUM_TAC(REWRITE_RULE[
INTERVAL_NE_EMPTY]) THEN
ASM_SIMP_TAC[
REAL_LE_LADD;
REAL_LE_RMUL_EQ;
REAL_SUB_LT;
LAMBDA_BETA] THEN
REWRITE_TAC[NOT_IMP;
REAL_LE_LADD] THEN
ASM_SIMP_TAC[
REAL_LE_DIV2_EQ;
REAL_LT_POW2] THEN
REWRITE_TAC[REAL_ARITH `~(x + &1 <= x)`] THEN DISJ2_TAC THEN
MATCH_MP_TAC(MESON[]
`(!i. ~P i ==> Q i) ==> (!i. Q i) \/ (?i. P i)`) THEN
X_GEN_TAC `i:num` THEN
DISCH_THEN(fun th -> STRIP_TAC THEN MP_TAC th) THEN
ASM_REWRITE_TAC[DE_MORGAN_THM;
REAL_NOT_LE] THEN
UNDISCH_TAC `m:num <= n` THEN REWRITE_TAC[
LE_EXISTS] THEN
DISCH_THEN(X_CHOOSE_THEN `p:num` SUBST1_TAC) THEN
ONCE_REWRITE_TAC[
ADD_SYM] THEN
REWRITE_TAC[
REAL_POW_ADD;
real_div;
REAL_INV_MUL] THEN
REWRITE_TAC[REAL_MUL_ASSOC] THEN REWRITE_TAC[GSYM
real_div] THEN
ASM_SIMP_TAC[
REAL_LE_DIV2_EQ;
REAL_LT_POW2;
REAL_LT_DIV2_EQ] THEN
ASM_SIMP_TAC[
REAL_LE_LDIV_EQ;
REAL_LE_RDIV_EQ;
REAL_LT_POW2;
REAL_LT_LDIV_EQ;
REAL_LT_RDIV_EQ] THEN
SIMP_TAC[
REAL_LT_INTEGERS;
INTEGER_CLOSED] THEN REAL_ARITH_TAC;
ALL_TAC] THEN
CONJ_TAC THENL
[X_GEN_TAC `x:real^N` THEN DISCH_TAC THEN
SUBGOAL_THEN
`?e. &0 < e /\ !y. (!i. 1 <= i /\ i <= dimindex(:N)
==> abs((x:real^N)$i - (y:real^N)$i) <= e)
==> y
IN g(x)`
STRIP_ASSUME_TAC THENL
[FIRST_ASSUM(MP_TAC o SPEC `x:real^N` o GEN_REWRITE_RULE I [gauge]) THEN
STRIP_TAC THEN
FIRST_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
EXISTS_TAC `e / &2 / &(dimindex(:N))` THEN
ASM_SIMP_TAC[
REAL_LT_DIV;
REAL_OF_NUM_LT;
LE_1;
DIMINDEX_GE_1;
ARITH] THEN
X_GEN_TAC `y:real^N` THEN STRIP_TAC THEN
MATCH_MP_TAC(SET_RULE `!s. s
SUBSET t /\ x
IN s ==> x
IN t`) THEN
EXISTS_TAC `ball(x:real^N,e)` THEN ASM_REWRITE_TAC[
IN_BALL] THEN
MATCH_MP_TAC(REAL_ARITH `&0 < e /\ x <= e / &2 ==> x < e`) THEN
ASM_REWRITE_TAC[dist] THEN MATCH_MP_TAC
REAL_LE_TRANS THEN
EXISTS_TAC `sum(1..dimindex(:N)) (\i. abs((x - y:real^N)$i))` THEN
REWRITE_TAC[
NORM_LE_L1] THEN MATCH_MP_TAC
SUM_BOUND_GEN THEN
ASM_SIMP_TAC[
IN_NUMSEG;
FINITE_NUMSEG;
NUMSEG_EMPTY;
NOT_LT;
DIMINDEX_GE_1;
VECTOR_SUB_COMPONENT;
CARD_NUMSEG_1];
ALL_TAC] THEN
REWRITE_TAC[
EXISTS_IN_IMAGE;
EXISTS_PAIR_THM;
IN_ELIM_PAIR_THM] THEN
MP_TAC(SPECL [`&1 / &2`; `e / norm(b - a:real^N)`]
REAL_ARCH_POW_INV) THEN
SUBGOAL_THEN `&0 < norm(b - a:real^N)` ASSUME_TAC THENL
[ASM_MESON_TAC[
VECTOR_SUB_EQ;
NORM_POS_LT;
INTERVAL_SING]; ALL_TAC] THEN
CONV_TAC REAL_RAT_REDUCE_CONV THEN ASM_SIMP_TAC[
REAL_LT_DIV] THEN
MATCH_MP_TAC
MONO_EXISTS THEN X_GEN_TAC `n:num` THEN
REWRITE_TAC[
real_div; REAL_MUL_LID;
REAL_POW_INV] THEN DISCH_TAC THEN
SIMP_TAC[
IN_ELIM_THM;
IN_INTERVAL;
SUBSET;
LAMBDA_BETA] THEN
MATCH_MP_TAC(MESON[]
`(!x. Q x ==> R x) /\ (?x. P x /\ Q x) ==> ?x. P x /\ Q x /\ R x`) THEN
CONJ_TAC THENL
[REWRITE_TAC[
RIGHT_IMP_FORALL_THM] THEN
MAP_EVERY X_GEN_TAC [`w:num^N`; `y:real^N`] THEN
REWRITE_TAC[IMP_IMP;
AND_FORALL_THM] THEN
DISCH_THEN(fun th -> FIRST_X_ASSUM MATCH_MP_TAC THEN MP_TAC th) THEN
MATCH_MP_TAC
MONO_FORALL THEN X_GEN_TAC `i:num` THEN
DISCH_THEN(fun th -> STRIP_TAC THEN MP_TAC th) THEN
ASM_REWRITE_TAC[] THEN DISCH_THEN(MP_TAC o MATCH_MP (REAL_ARITH
`(a + n <= x /\ x <= a + m) /\
(a + n <= y /\ y <= a + m) ==> abs(x - y) <= m - n`)) THEN
MATCH_MP_TAC(REAL_ARITH
`y * z <= e
==> a <= ((x + &1) * y) * z - ((x * y) * z) ==> a <= e`) THEN
RULE_ASSUM_TAC(REWRITE_RULE[
INTERVAL_NE_EMPTY]) THEN
ASM_SIMP_TAC[GSYM
REAL_LE_RDIV_EQ;
REAL_SUB_LT] THEN
FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP
(REAL_ARITH `n < e * x ==> &0 <= e * (inv y - x) ==> n <= e / y`)) THEN
MATCH_MP_TAC
REAL_LE_MUL THEN ASM_SIMP_TAC[
REAL_LT_IMP_LE] THEN
REWRITE_TAC[
REAL_SUB_LE] THEN MATCH_MP_TAC
REAL_LE_INV2 THEN
ASM_SIMP_TAC[
REAL_SUB_LT] THEN
MP_TAC(SPECL [`b - a:real^N`; `i:num`]
COMPONENT_LE_NORM) THEN
ASM_SIMP_TAC[
VECTOR_SUB_COMPONENT] THEN REAL_ARITH_TAC;
ALL_TAC] THEN
REWRITE_TAC[
IN_UNIV;
AND_FORALL_THM] THEN
REWRITE_TAC[TAUT `(a ==> c) /\ (a ==> b) <=> a ==> b /\ c`] THEN
REWRITE_TAC[GSYM
LAMBDA_SKOLEM] THEN X_GEN_TAC `i:num` THEN
STRIP_TAC THEN
SUBGOAL_THEN `(x:real^N)
IN interval[a,b]` MP_TAC THENL
[ASM SET_TAC[]; ALL_TAC] THEN REWRITE_TAC[
IN_INTERVAL] THEN
DISCH_THEN(MP_TAC o SPEC `i:num`) THEN ASM_REWRITE_TAC[] THEN
RULE_ASSUM_TAC(REWRITE_RULE[
INTERVAL_NE_EMPTY]) THEN STRIP_TAC THEN
DISJ_CASES_TAC(MATCH_MP (REAL_ARITH `x <= y ==> x = y \/ x < y`)
(ASSUME `(x:real^N)$i <= (b:real^N)$i`))
THENL
[EXISTS_TAC `2
EXP n - 1` THEN
SIMP_TAC[GSYM
REAL_OF_NUM_SUB; GSYM
REAL_OF_NUM_LT;
EXP_LT_0;
LE_1; ARITH] THEN
ASM_REWRITE_TAC[
REAL_SUB_ADD; REAL_ARITH `a - &1 < a`] THEN
MATCH_MP_TAC(REAL_ARITH
`&1 * (b - a) = x /\ y <= x ==> a + y <= b /\ b <= a + x`) THEN
ASM_SIMP_TAC[
REAL_EQ_MUL_RCANCEL;
REAL_LT_IMP_NZ;
REAL_LE_RMUL_EQ;
REAL_SUB_LT;
REAL_LT_INV_EQ;
REAL_LT_POW2] THEN
SIMP_TAC[GSYM
REAL_OF_NUM_POW;
REAL_MUL_RINV;
REAL_POW_EQ_0;
REAL_OF_NUM_EQ;
ARITH_EQ] THEN REAL_ARITH_TAC;
ALL_TAC] THEN
MP_TAC(SPEC `&2 pow n * ((x:real^N)$i - (a:real^N)$i) /
((b:real^N)$i - (a:real^N)$i)`
FLOOR_POS) THEN
ANTS_TAC THENL
[ASM_MESON_TAC[
REAL_LE_MUL;
REAL_LE_MUL;
REAL_POW_LE;
REAL_POS;
REAL_SUB_LE;
REAL_LT_IMP_LE;
REAL_LE_DIV];
ALL_TAC] THEN
MATCH_MP_TAC
MONO_EXISTS THEN X_GEN_TAC `m:num` THEN
REWRITE_TAC[GSYM
REAL_OF_NUM_LT; GSYM
REAL_OF_NUM_POW] THEN
DISCH_THEN(SUBST_ALL_TAC o SYM) THEN
REWRITE_TAC[REAL_ARITH `a + b * c <= x /\ x <= a + b' * c <=>
b * c <= x - a /\ x - a <= b' * c`] THEN
ASM_SIMP_TAC[GSYM
REAL_LE_LDIV_EQ; GSYM
REAL_LE_RDIV_EQ;
REAL_SUB_LT; GSYM
real_div] THEN
ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
SIMP_TAC[
REAL_LE_LDIV_EQ;
REAL_LE_RDIV_EQ;
REAL_LT_POW2] THEN
SIMP_TAC[
FLOOR;
REAL_LT_IMP_LE] THEN MATCH_MP_TAC
REAL_LET_TRANS THEN
EXISTS_TAC `((x:real^N)$i - (a:real^N)$i) /
((b:real^N)$i - (a:real^N)$i) *
&2 pow n` THEN
REWRITE_TAC[
FLOOR] THEN GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_LID] THEN
ASM_SIMP_TAC[
REAL_LT_RMUL_EQ;
REAL_LT_POW2] THEN
ASM_SIMP_TAC[
REAL_LT_LDIV_EQ; REAL_MUL_LID;
REAL_SUB_LT] THEN
ASM_REAL_ARITH_TAC;
ALL_TAC] THEN
CONJ_TAC THENL
[REPEAT GEN_TAC THEN REWRITE_TAC[
IN_IMAGE;
EXISTS_PAIR_THM] THEN
REWRITE_TAC[
EQ_INTERVAL;
IN_ELIM_PAIR_THM] THEN
REWRITE_TAC[
INTERVAL_EQ_EMPTY;
IN_UNIV;
IN_ELIM_THM] THEN
SIMP_TAC[TAUT `a /\ b /\ c <=> ~(a /\ b ==> ~c)`;
LAMBDA_BETA] THEN
RULE_ASSUM_TAC(REWRITE_RULE[
INTERVAL_NE_EMPTY]) THEN
ASM_SIMP_TAC[
REAL_LT_LADD;
REAL_LT_RMUL_EQ;
REAL_SUB_LT;
REAL_LT_DIV2_EQ;
REAL_LT_POW2;
REAL_ARITH `~(v + &1 < v)`] THEN
MATCH_MP_TAC
MONO_EXISTS THEN X_GEN_TAC `n:num` THEN
STRIP_TAC THEN ASM_SIMP_TAC[
LAMBDA_BETA] THEN REAL_ARITH_TAC;
ALL_TAC] THEN
REWRITE_TAC[
FORALL_IN_IMAGE;
FORALL_PAIR_THM;
IN_ELIM_PAIR_THM] THEN
MAP_EVERY X_GEN_TAC [`n:num`; `v:num^N`] THEN
REWRITE_TAC[
IN_ELIM_THM;
IN_UNIV] THEN DISCH_TAC THEN
MATCH_MP_TAC
FINITE_SUBSET THEN EXISTS_TAC
`
IMAGE (\(n,v).
interval[(lambda i. a$i + &(v$i) / &2 pow n *
((b:real^N)$i - (a:real^N)$i)):real^N,
(lambda i. a$i + (&(v$i) + &1) / &2 pow n * (b$i - a$i))])
{m,v | m
IN 0..n /\
v
IN {v:num^N | !i. 1 <= i /\ i <= dimindex(:N)
==> v$i < 2
EXP m}}` THEN
CONJ_TAC THENL
[MATCH_MP_TAC
FINITE_IMAGE THEN
MATCH_MP_TAC
FINITE_PRODUCT_DEPENDENT THEN
REWRITE_TAC[
FINITE_NUMSEG] THEN REPEAT STRIP_TAC THEN
MATCH_MP_TAC
FINITE_CART THEN REWRITE_TAC[
FINITE_NUMSEG_LT];
ALL_TAC] THEN
GEN_REWRITE_TAC I [
SUBSET] THEN
REWRITE_TAC[
IN_ELIM_THM] THEN ONCE_REWRITE_TAC[
IMP_CONJ] THEN
REWRITE_TAC[
FORALL_IN_IMAGE;
FORALL_PAIR_THM;
IN_ELIM_PAIR_THM] THEN
MAP_EVERY X_GEN_TAC [`m:num`; `w:num^N`] THEN DISCH_TAC THEN
DISCH_TAC THEN SIMP_TAC[
IN_IMAGE;
EXISTS_PAIR_THM;
IN_ELIM_PAIR_THM] THEN
MAP_EVERY EXISTS_TAC [`m:num`; `w:num^N`] THEN ASM_REWRITE_TAC[] THEN
REWRITE_TAC[
IN_NUMSEG; GSYM
NOT_LT;
LT] THEN DISCH_TAC THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [
SUBSET_INTERVAL]) THEN
SIMP_TAC[NOT_IMP;
LAMBDA_BETA] THEN
RULE_ASSUM_TAC(REWRITE_RULE[
INTERVAL_NE_EMPTY]) THEN
ASM_SIMP_TAC[
REAL_LE_LADD;
REAL_LE_RMUL_EQ;
REAL_SUB_LT] THEN
ASM_SIMP_TAC[
REAL_LE_DIV2_EQ;
REAL_LT_POW2] THEN
REWRITE_TAC[REAL_ARITH `x <= x + &1`] THEN
DISCH_THEN(MP_TAC o SPEC `1`) THEN
REWRITE_TAC[
LE_REFL;
DIMINDEX_GE_1] THEN
DISCH_THEN(MP_TAC o MATCH_MP (REAL_ARITH
`w / m <= v / n /\ (v + &1) / n <= (w + &1) / m
==> inv n <= inv m`)) THEN
REWRITE_TAC[
REAL_NOT_LE] THEN MATCH_MP_TAC
REAL_LT_INV2 THEN
ASM_REWRITE_TAC[
REAL_LT_POW2] THEN MATCH_MP_TAC
REAL_POW_MONO_LT THEN
ASM_REWRITE_TAC[] THEN CONV_TAC REAL_RAT_REDUCE_CONV;
ALL_TAC] THEN
SUBGOAL_THEN
`?d.
COUNTABLE d /\
(!k. k
IN d ==> k
SUBSET interval[a,b] /\ ~(interior k = {}) /\
(?c d:real^N. k = interval[c,d])) /\
(!k1 k2. k1
IN d /\ k2
IN d
==> k1
SUBSET k2 \/ k2
SUBSET k1 \/
interior k1
INTER interior k2 = {}) /\
(!k. k
IN d ==> (?x. x
IN s
INTER k /\ k
SUBSET g x)) /\
(!u v. interval[u,v]
IN d
==> ?n. !i. 1 <= i /\ i <= dimindex(:N)
==> v$i - u$i = (b$i - a$i) / &2 pow n) /\
(!k. k
IN d ==>
FINITE {l | l
IN d /\ k
SUBSET l}) /\
s
SUBSET UNIONS d`
MP_TAC THENL
[FIRST_X_ASSUM(X_CHOOSE_THEN `d:(real^N->bool)->bool` STRIP_ASSUME_TAC) THEN
EXISTS_TAC
`{k:real^N->bool | k
IN d /\ ?x. x
IN (s
INTER k) /\ k
SUBSET g x}` THEN
ASM_SIMP_TAC[
IN_ELIM_THM] THEN REPEAT CONJ_TAC THENL
[MATCH_MP_TAC
COUNTABLE_SUBSET THEN
EXISTS_TAC `d:(real^N->bool)->bool` THEN
ASM_REWRITE_TAC[] THEN SET_TAC[];
X_GEN_TAC `k:real^N->bool` THEN REPEAT STRIP_TAC THEN
MATCH_MP_TAC
FINITE_SUBSET THEN
EXISTS_TAC `{l:real^N->bool | l
IN d /\ k
SUBSET l}` THEN
ASM_REWRITE_TAC[] THEN ASM SET_TAC[];
ASM SET_TAC[]];
ALL_TAC] THEN
DISCH_THEN(X_CHOOSE_THEN `d:(real^N->bool)->bool` STRIP_ASSUME_TAC) THEN
EXISTS_TAC
`{k:real^N->bool | k
IN d /\ !k'. k'
IN d /\ ~(k = k')
==> ~(k
SUBSET k')}` THEN
ASM_SIMP_TAC[
IN_ELIM_THM] THEN REPEAT CONJ_TAC THENL
[MATCH_MP_TAC
COUNTABLE_SUBSET THEN EXISTS_TAC `d:(real^N->bool)->bool` THEN
ASM_REWRITE_TAC[] THEN SET_TAC[];
ASM SET_TAC[];
ALL_TAC] THEN
FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP
(REWRITE_RULE[
IMP_CONJ]
SUBSET_TRANS)) THEN
GEN_REWRITE_TAC I [
SUBSET] THEN REWRITE_TAC[
FORALL_IN_UNIONS] THEN
MAP_EVERY X_GEN_TAC [`k:real^N->bool`; `x:real^N`] THEN DISCH_TAC THEN
REWRITE_TAC[
IN_UNIONS;
IN_ELIM_THM] THEN
MP_TAC(ISPEC `\k l:real^N->bool. k
IN d /\ l
IN d /\ l
SUBSET k /\ ~(k = l)`
WF_FINITE) THEN
REWRITE_TAC[
WF] THEN ANTS_TAC THENL
[CONJ_TAC THENL [SET_TAC[]; ALL_TAC] THEN X_GEN_TAC `l:real^N->bool` THEN
ASM_CASES_TAC `(l:real^N->bool)
IN d` THEN
ASM_REWRITE_TAC[
EMPTY_GSPEC;
FINITE_RULES] THEN
MATCH_MP_TAC
FINITE_SUBSET THEN
EXISTS_TAC `{m:real^N->bool | m
IN d /\ l
SUBSET m}` THEN
ASM_SIMP_TAC[] THEN SET_TAC[];
ALL_TAC] THEN
DISCH_THEN(MP_TAC o SPEC `\l:real^N->bool. l
IN d /\ x
IN l`) THEN
REWRITE_TAC[] THEN ANTS_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
MATCH_MP_TAC
MONO_EXISTS THEN ASM SET_TAC[]);;
let MEASURABLE_OUTER_INTERVALS_BOUNDED = prove
(`!s a b:real^N e.
measurable s /\ s
SUBSET interval[a,b] /\ &0 < e
==> ?d.
COUNTABLE d /\
(!k. k
IN d ==> k
SUBSET interval[a,b] /\ ~(k = {}) /\
(?c d. k = interval[c,d])) /\
(!k1 k2. k1
IN d /\ k2
IN d /\ ~(k1 = k2)
==> interior k1
INTER interior k2 = {}) /\
(!u v. interval[u,v]
IN d
==> ?n. !i. 1 <= i /\ i <= dimindex(:N)
==> v$i - u$i = (b$i - a$i) / &2 pow n) /\
(!k. k
IN d /\ ~(interval(a,b) = {}) ==> ~(interior k = {})) /\
s
SUBSET UNIONS d /\
measurable (
UNIONS d) /\
measure (
UNIONS d) <= measure s + e`,
let lemma = prove
(`(!x y. (x,y) IN IMAGE (\z. f z,g z) s ==> P x y) <=>
(!z. z IN s ==> P (f z) (g z))`,
REWRITE_TAC[IN_IMAGE; PAIR_EQ] THEN MESON_TAC[]) in
REPEAT GEN_TAC THEN
ASM_CASES_TAC `interval[a:real^N,b] = {}` THENL
[ASM_REWRITE_TAC[SUBSET_EMPTY] THEN STRIP_TAC THEN
EXISTS_TAC `{}:(real^N->bool)->bool` THEN
ASM_REWRITE_TAC[NOT_IN_EMPTY; UNIONS_0; MEASURE_EMPTY; REAL_ADD_LID;
SUBSET_REFL; COUNTABLE_EMPTY; MEASURABLE_EMPTY] THEN
ASM_SIMP_TAC[REAL_LT_IMP_LE];
ALL_TAC] THEN
STRIP_TAC THEN ASM_CASES_TAC `interval(a:real^N,b) = {}` THEN
ASM_REWRITE_TAC[] THENL
[EXISTS_TAC `{interval[a:real^N,b]}` THEN
REWRITE_TAC[UNIONS_1; COUNTABLE_SING] THEN
ASM_REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM; FORALL_IN_INSERT;
NOT_IN_EMPTY; SUBSET_REFL; MEASURABLE_INTERVAL] THEN
CONJ_TAC THENL [MESON_TAC[]; ALL_TAC] THEN CONJ_TAC THENL
[ASM_REWRITE_TAC[IN_SING; EQ_INTERVAL] THEN
REPEAT STRIP_TAC THEN EXISTS_TAC `0` THEN
ASM_REWRITE_TAC[real_pow; REAL_DIV_1];
SUBGOAL_THEN
`measure(interval[a:real^N,b]) = &0 /\ measure(s:real^N->bool) = &0`
(fun th -> ASM_SIMP_TAC[th; REAL_LT_IMP_LE; REAL_ADD_LID]) THEN
SUBGOAL_THEN
`interval[a:real^N,b] has_measure &0 /\
(s:real^N->bool) has_measure &0`
(fun th -> MESON_TAC[th; MEASURE_UNIQUE]) THEN
REWRITE_TAC[HAS_MEASURE_0] THEN
MATCH_MP_TAC(TAUT `a /\ (a ==> b) ==> a /\ b`) THEN CONJ_TAC THENL
[ASM_REWRITE_TAC[NEGLIGIBLE_INTERVAL];
ASM_MESON_TAC[NEGLIGIBLE_SUBSET]]];
ALL_TAC] THEN
FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [measurable]) THEN
DISCH_THEN(X_CHOOSE_TAC `m:real`) THEN
FIRST_ASSUM(ASSUME_TAC o MATCH_MP MEASURE_UNIQUE) THEN
SUBGOAL_THEN
`((\x:real^N. if x IN s then vec 1 else vec 0) has_integral (lift m))
(interval[a,b])`
ASSUME_TAC THENL
[ONCE_REWRITE_TAC[GSYM HAS_INTEGRAL_RESTRICT_UNIV] THEN
FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [HAS_MEASURE]) THEN
MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ] HAS_INTEGRAL_EQ) THEN
ASM SET_TAC[];
ALL_TAC] THEN
FIRST_ASSUM(ASSUME_TAC o MATCH_MP HAS_INTEGRAL_INTEGRABLE) THEN
FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [has_integral]) THEN
DISCH_THEN(MP_TAC o SPEC `e:real`) THEN ASM_REWRITE_TAC[] THEN
DISCH_THEN(X_CHOOSE_THEN `g:real^N->real^N->bool` STRIP_ASSUME_TAC) THEN
MP_TAC(SPECL [`a:real^N`; `b:real^N`; `s:real^N->bool`;
`g:real^N->real^N->bool`] COVERING_LEMMA) THEN
ASM_REWRITE_TAC[] THEN MATCH_MP_TAC MONO_EXISTS THEN
X_GEN_TAC `d:(real^N->bool)->bool` THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
CONJ_TAC THENL [ASM_MESON_TAC[INTERIOR_EMPTY]; ALL_TAC] THEN
CONJ_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
MP_TAC(ISPECL [`(\x. if x IN s then vec 1 else vec 0):real^N->real^1`;
`a:real^N`; `b:real^N`; `g:real^N->real^N->bool`;
`e:real`]
HENSTOCK_LEMMA_PART1) THEN
ASM_REWRITE_TAC[] THEN
FIRST_ASSUM(SUBST1_TAC o MATCH_MP INTEGRAL_UNIQUE) THEN
ASM_REWRITE_TAC[] THEN DISCH_THEN(LABEL_TAC "*") THEN
SUBGOAL_THEN
`!k l:real^N->bool. k IN d /\ l IN d /\ ~(k = l)
==> negligible(k INTER l)`
ASSUME_TAC THENL
[REPEAT STRIP_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPECL [`k:real^N->bool`; `l:real^N->bool`]) THEN
ASM_SIMP_TAC[] THEN
SUBGOAL_THEN
`?x y:real^N u v:real^N. k = interval[x,y] /\ l = interval[u,v]`
MP_TAC THENL [ASM_MESON_TAC[SUBSET]; ALL_TAC] THEN
DISCH_THEN(REPEAT_TCL CHOOSE_THEN (CONJUNCTS_THEN SUBST_ALL_TAC)) THEN
REWRITE_TAC[INTERIOR_CLOSED_INTERVAL] THEN DISCH_TAC THEN
MATCH_MP_TAC NEGLIGIBLE_SUBSET THEN
EXISTS_TAC `(interval[x:real^N,y] DIFF interval(x,y)) UNION
(interval[u:real^N,v] DIFF interval(u,v)) UNION
(interval (x,y) INTER interval (u,v))` THEN
CONJ_TAC THENL [ALL_TAC; SET_TAC[]] THEN
ASM_REWRITE_TAC[UNION_EMPTY] THEN
SIMP_TAC[NEGLIGIBLE_UNION; NEGLIGIBLE_FRONTIER_INTERVAL];
ALL_TAC] THEN
SUBGOAL_THEN
`!D. FINITE D /\ D SUBSET d
==> measurable(UNIONS D :real^N->bool) /\ measure(UNIONS D) <= m + e`
ASSUME_TAC THENL
[GEN_TAC THEN STRIP_TAC THEN
SUBGOAL_THEN
`?t:(real^N->bool)->real^N. !k. k IN D ==> t(k) IN (s INTER k) /\
k SUBSET (g(t k))`
(CHOOSE_THEN (LABEL_TAC "+")) THENL
[REWRITE_TAC[GSYM SKOLEM_THM] THEN ASM SET_TAC[]; ALL_TAC] THEN
REMOVE_THEN "*" (MP_TAC o SPEC
`IMAGE (\k. (t:(real^N->bool)->real^N) k,k) D`) THEN
ASM_SIMP_TAC[VSUM_IMAGE; PAIR_EQ] THEN REWRITE_TAC[o_DEF] THEN
ANTS_TAC THENL
[REWRITE_TAC[tagged_partial_division_of; fine] THEN
ASM_SIMP_TAC[FINITE_IMAGE; FORALL_IN_IMAGE] THEN
REWRITE_TAC[lemma; RIGHT_FORALL_IMP_THM; IMP_CONJ; PAIR_EQ] THEN
ASM_SIMP_TAC[] THEN
CONJ_TAC THENL [ASM SET_TAC[]; ASM_MESON_TAC[SUBSET]];
ALL_TAC] THEN
USE_THEN "+" (MP_TAC o REWRITE_RULE[IN_INTER]) THEN
SIMP_TAC[] THEN DISCH_THEN(K ALL_TAC) THEN
ASM_SIMP_TAC[VSUM_SUB] THEN
SUBGOAL_THEN `D division_of (UNIONS D:real^N->bool)` ASSUME_TAC THENL
[REWRITE_TAC[division_of] THEN ASM SET_TAC[]; ALL_TAC] THEN
FIRST_ASSUM(ASSUME_TAC o MATCH_MP MEASURABLE_ELEMENTARY) THEN
SUBGOAL_THEN `vsum D (\k:real^N->bool. content k % vec 1) =
lift(measure(UNIONS D))`
SUBST1_TAC THENL
[ONCE_REWRITE_TAC[GSYM DROP_EQ] THEN
ASM_SIMP_TAC[LIFT_DROP; DROP_VSUM; o_DEF; DROP_CMUL; DROP_VEC] THEN
SIMP_TAC[REAL_MUL_RID; ETA_AX] THEN ASM_MESON_TAC[MEASURE_ELEMENTARY];
ALL_TAC] THEN
SUBGOAL_THEN
`vsum D (\k. integral k (\x:real^N. if x IN s then vec 1 else vec 0)) =
lift(sum D (\k. measure(k INTER s)))`
SUBST1_TAC THENL
[ASM_SIMP_TAC[LIFT_SUM; o_DEF] THEN MATCH_MP_TAC VSUM_EQ THEN
X_GEN_TAC `k:real^N->bool` THEN DISCH_TAC THEN REWRITE_TAC[] THEN
SUBGOAL_THEN `measurable(k:real^N->bool)` ASSUME_TAC THENL
[ASM_MESON_TAC[SUBSET; MEASURABLE_INTERVAL]; ALL_TAC] THEN
ASM_SIMP_TAC[GSYM INTEGRAL_MEASURE_UNIV; MEASURABLE_INTER] THEN
REWRITE_TAC[MESON[IN_INTER]
`(if x IN k INTER s then a else b) =
(if x IN k then if x IN s then a else b else b)`] THEN
REWRITE_TAC[INTEGRAL_RESTRICT_UNIV];
ALL_TAC] THEN
ASM_REWRITE_TAC[GSYM LIFT_SUB; NORM_LIFT] THEN
MATCH_MP_TAC(REAL_ARITH `y <= m ==> abs(x - y) <= e ==> x <= m + e`) THEN
MATCH_MP_TAC REAL_LE_TRANS THEN
EXISTS_TAC `measure(UNIONS D INTER s:real^N->bool)` THEN
CONJ_TAC THENL
[ALL_TAC;
EXPAND_TAC "m" THEN MATCH_MP_TAC MEASURE_SUBSET THEN
ASM_REWRITE_TAC[] THEN CONJ_TAC THENL [ALL_TAC; SET_TAC[]] THEN
MATCH_MP_TAC MEASURABLE_INTER THEN ASM_REWRITE_TAC[]] THEN
REWRITE_TAC[INTER_UNIONS] THEN MATCH_MP_TAC REAL_EQ_IMP_LE THEN
ONCE_REWRITE_TAC[SIMPLE_IMAGE] THEN CONV_TAC SYM_CONV THEN
MATCH_MP_TAC MEASURE_NEGLIGIBLE_UNIONS_IMAGE_STRONG THEN
ASM_SIMP_TAC[FINITE_RESTRICT] THEN CONJ_TAC THENL
[ASM_MESON_TAC[SUBSET; MEASURABLE_INTERVAL; MEASURABLE_INTER];
ALL_TAC] THEN
MAP_EVERY X_GEN_TAC [`k:real^N->bool`; `l:real^N->bool`] THEN
STRIP_TAC THEN MATCH_MP_TAC NEGLIGIBLE_SUBSET THEN
EXISTS_TAC `k INTER l:real^N->bool` THEN ASM_SIMP_TAC[] THEN ASM SET_TAC[];
ALL_TAC] THEN
ASM_CASES_TAC `FINITE(d:(real^N->bool)->bool)` THENL
[ASM_MESON_TAC[SUBSET_REFL]; ALL_TAC] THEN
MP_TAC(ISPEC `d:(real^N->bool)->bool` COUNTABLE_AS_INJECTIVE_IMAGE) THEN
ASM_REWRITE_TAC[INFINITE] THEN
DISCH_THEN(X_CHOOSE_THEN `s:num->real^N->bool`
(CONJUNCTS_THEN2 SUBST_ALL_TAC ASSUME_TAC)) THEN
MP_TAC(ISPECL [`s:num->real^N->bool`; `m + e:real`]
HAS_MEASURE_COUNTABLE_NEGLIGIBLE_UNIONS) THEN
MATCH_MP_TAC(TAUT `a /\ (a /\ b ==> c) ==> (a ==> b) ==> c`) THEN
REWRITE_TAC[GSYM CONJ_ASSOC] THEN
RULE_ASSUM_TAC(REWRITE_RULE[IMP_CONJ; RIGHT_FORALL_IMP_THM;
FORALL_IN_IMAGE; IN_UNIV]) THEN
RULE_ASSUM_TAC(REWRITE_RULE[IMP_IMP; RIGHT_IMP_FORALL_THM]) THEN
REPEAT CONJ_TAC THENL
[ASM_MESON_TAC[MEASURABLE_INTERVAL; MEASURABLE_INTER];
ASM_MESON_TAC[];
X_GEN_TAC `n:num` THEN
FIRST_X_ASSUM(MP_TAC o SPEC `IMAGE (s:num->real^N->bool) (0..n)`) THEN
SIMP_TAC[FINITE_IMAGE; FINITE_NUMSEG; IMAGE_SUBSET; SUBSET_UNIV] THEN
DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
MATCH_MP_TAC(REAL_ARITH `x = y ==> x <= e ==> y <= e`) THEN
MATCH_MP_TAC MEASURE_NEGLIGIBLE_UNIONS_IMAGE THEN
ASM_MESON_TAC[FINITE_NUMSEG; MEASURABLE_INTERVAL];
ALL_TAC] THEN
ONCE_REWRITE_TAC[SIMPLE_IMAGE] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
GEN_REWRITE_TAC LAND_CONV [GSYM(CONJUNCT2 LIFT_DROP)] THEN
REWRITE_TAC[drop] THEN
MATCH_MP_TAC(ISPEC `sequentially` LIM_COMPONENT_UBOUND) THEN
EXISTS_TAC
`\n. vsum(from 0 INTER (0..n)) (\n. lift(measure(s n:real^N->bool)))` THEN
ASM_REWRITE_TAC[GSYM sums; TRIVIAL_LIMIT_SEQUENTIALLY] THEN
REWRITE_TAC[DIMINDEX_1; ARITH; EVENTUALLY_SEQUENTIALLY] THEN
SIMP_TAC[VSUM_COMPONENT; ARITH; DIMINDEX_1] THEN
ASM_REWRITE_TAC[GSYM drop; LIFT_DROP; FROM_INTER_NUMSEG]);;
let MEASURABLE_OUTER_CLOSED_INTERVALS = prove
(`!s:real^N->bool e.
measurable s /\ &0 < e
==> ?d.
COUNTABLE d /\
(!k. k
IN d ==> ~(k = {}) /\ (?a b. k = interval[a,b])) /\
(!k l. k
IN d /\ l
IN d /\ ~(k = l)
==> interior k
INTER interior l = {}) /\
s
SUBSET UNIONS d /\
measurable (
UNIONS d) /\
measure (
UNIONS d) <= measure s + e`,
let lemma = prove
(`UNIONS (UNIONS {d n | n IN (:num)}) =
UNIONS {UNIONS(d n) | n IN (:num)}`,
REWRITE_TAC[SIMPLE_IMAGE; UNIONS_IMAGE] THEN
GEN_REWRITE_TAC I [EXTENSION] THEN
REWRITE_TAC[IN_UNIONS; IN_ELIM_THM; IN_UNIV] THEN MESON_TAC[]) in
REPEAT STRIP_TAC THEN
SUBGOAL_THEN
`?d. COUNTABLE d /\
(!k. k IN d ==> ?a b:real^N. k = interval[a,b]) /\
s SUBSET UNIONS d /\
measurable (UNIONS d) /\
measure (UNIONS d) <= measure s + e`
MP_TAC THENL
[ALL_TAC;
DISCH_THEN(X_CHOOSE_THEN `d1:(real^N->bool)->bool` STRIP_ASSUME_TAC) THEN
MP_TAC(ISPEC `d1:(real^N->bool)->bool` COUNTABLE_ELEMENTARY_DIVISION) THEN
ASM_REWRITE_TAC[] THEN MATCH_MP_TAC MONO_EXISTS THEN
X_GEN_TAC `d:(real^N->bool)->bool` THEN
STRIP_TAC THEN FIRST_X_ASSUM(SUBST_ALL_TAC o SYM) THEN
ASM_REWRITE_TAC[]] THEN
MP_TAC(ISPECL
[`\n. s INTER (ball(vec 0:real^N,&n + &1) DIFF ball(vec 0,&n))`;
`measure(s:real^N->bool)`] HAS_MEASURE_COUNTABLE_NEGLIGIBLE_UNIONS) THEN
ASM_SIMP_TAC[MEASURABLE_INTER; MEASURABLE_DIFF; MEASURABLE_BALL] THEN
SUBGOAL_THEN
`!m n. ~(m = n)
==> (s INTER (ball(vec 0,&m + &1) DIFF ball(vec 0,&m))) INTER
(s INTER (ball(vec 0,&n + &1) DIFF ball(vec 0,&n))) =
({}:real^N->bool)`
ASSUME_TAC THENL
[MATCH_MP_TAC WLOG_LT THEN REWRITE_TAC[] THEN
CONJ_TAC THENL [MESON_TAC[INTER_COMM]; ALL_TAC] THEN
MAP_EVERY X_GEN_TAC [`m:num`; `n:num`] THEN REPEAT STRIP_TAC THEN
MATCH_MP_TAC(SET_RULE
`m1 SUBSET n
==> (s INTER (m1 DIFF m)) INTER (s INTER (n1 DIFF n)) = {}`) THEN
MATCH_MP_TAC SUBSET_BALL THEN
REWRITE_TAC[REAL_OF_NUM_ADD; REAL_OF_NUM_LE] THEN ASM_ARITH_TAC;
ALL_TAC] THEN
ANTS_TAC THENL
[ASM_SIMP_TAC[NEGLIGIBLE_EMPTY] THEN X_GEN_TAC `n:num` THEN
W(MP_TAC o PART_MATCH (rand o rand)
MEASURE_DISJOINT_UNIONS_IMAGE o lhand o snd) THEN
ASM_SIMP_TAC[FINITE_NUMSEG; DISJOINT] THEN
ASM_SIMP_TAC[MEASURABLE_INTER; MEASURABLE_DIFF; MEASURABLE_BALL] THEN
DISCH_THEN(SUBST1_TAC o SYM) THEN MATCH_MP_TAC MEASURE_SUBSET THEN
SIMP_TAC[SUBSET; FORALL_IN_UNIONS; IMP_CONJ; FORALL_IN_IMAGE;
RIGHT_FORALL_IMP_THM; IN_INTER] THEN
ASM_SIMP_TAC[MEASURABLE_UNIONS; FINITE_NUMSEG; FORALL_IN_IMAGE;
FINITE_IMAGE; MEASURABLE_INTER; MEASURABLE_DIFF; MEASURABLE_BALL];
ALL_TAC] THEN
SUBGOAL_THEN
`UNIONS {s INTER (ball(vec 0,&n + &1) DIFF ball(vec 0,&n)) | n IN (:num)} =
(s:real^N->bool)`
ASSUME_TAC THENL
[REWRITE_TAC[EXTENSION; IN_UNIONS; EXISTS_IN_GSPEC; IN_UNIV; IN_INTER] THEN
X_GEN_TAC `x:real^N` THEN
ASM_CASES_TAC `(x:real^N) IN s` THEN ASM_REWRITE_TAC[] THEN
SUBGOAL_THEN `?n. (x:real^N) IN ball(vec 0,&n)` MP_TAC THENL
[REWRITE_TAC[IN_BALL_0; REAL_ARCH_LT];
GEN_REWRITE_TAC LAND_CONV [num_WOP] THEN
DISCH_THEN(X_CHOOSE_THEN `n:num` MP_TAC) THEN ASM_CASES_TAC `n = 0` THENL
[ASM_REWRITE_TAC[IN_BALL_0; GSYM REAL_NOT_LE; NORM_POS_LE];
STRIP_TAC THEN EXISTS_TAC `n - 1` THEN REWRITE_TAC[IN_DIFF] THEN
ASM_SIMP_TAC[REAL_OF_NUM_ADD; SUB_ADD; LE_1] THEN
FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC]];
ASM_REWRITE_TAC[] THEN DISCH_TAC] THEN
MP_TAC(MATCH_MP MONO_FORALL (GEN `n:num`
(ISPECL
[`s INTER (ball(vec 0:real^N,&n + &1) DIFF ball(vec 0,&n))`;
`--(vec(n + 1)):real^N`; `vec(n + 1):real^N`;
`e / &2 / &2 pow n`]
MEASURABLE_OUTER_INTERVALS_BOUNDED))) THEN
ANTS_TAC THENL
[ASM_SIMP_TAC[REAL_LT_DIV; REAL_HALF; REAL_LT_POW2] THEN
ASM_SIMP_TAC[MEASURABLE_INTER; MEASURABLE_DIFF; MEASURABLE_BALL] THEN
REWRITE_TAC[SUBSET; IN_INTER; IN_INTERVAL; IN_BALL_0; IN_DIFF; REAL_NOT_LT;
REAL_OF_NUM_ADD; VECTOR_NEG_COMPONENT; VEC_COMPONENT; REAL_BOUNDS_LE] THEN
MESON_TAC[COMPONENT_LE_NORM; REAL_LET_TRANS; REAL_LT_IMP_LE];
REWRITE_TAC[SKOLEM_THM; LEFT_IMP_EXISTS_THM; FORALL_AND_THM]] THEN
X_GEN_TAC `d:num->(real^N->bool)->bool` THEN STRIP_TAC THEN
EXISTS_TAC `UNIONS {d n | n IN (:num)} :(real^N->bool)->bool` THEN
REWRITE_TAC[lemma] THEN CONJ_TAC THENL
[MATCH_MP_TAC COUNTABLE_UNIONS THEN
ASM_REWRITE_TAC[SIMPLE_IMAGE; FORALL_IN_IMAGE] THEN
SIMP_TAC[COUNTABLE_IMAGE; NUM_COUNTABLE];
ALL_TAC] THEN
CONJ_TAC THENL
[REWRITE_TAC[FORALL_IN_UNIONS; IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN
ASM_SIMP_TAC[FORALL_IN_GSPEC; IN_UNIV] THEN ASM_MESON_TAC[];
ALL_TAC] THEN
CONJ_TAC THENL
[FIRST_X_ASSUM(fun th -> GEN_REWRITE_TAC LAND_CONV [GSYM th]) THEN
REWRITE_TAC[SUBSET; FORALL_IN_UNIONS; IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN
ASM_SIMP_TAC[FORALL_IN_GSPEC; IN_UNIV; IN_UNIONS] THEN
REWRITE_TAC[EXISTS_IN_GSPEC] THEN ASM SET_TAC[];
ALL_TAC] THEN
MATCH_MP_TAC MEASURE_COUNTABLE_UNIONS_LE THEN ASM_REWRITE_TAC[] THEN
X_GEN_TAC `n:num` THEN
MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC
`sum(0..n) (\k. measure(s INTER (ball(vec 0:real^N,&k + &1) DIFF
ball(vec 0,&k))) + e / &2 / &2 pow k)` THEN
ASM_SIMP_TAC[SUM_LE_NUMSEG] THEN REWRITE_TAC[SUM_ADD_NUMSEG] THEN
MATCH_MP_TAC REAL_LE_ADD2 THEN CONJ_TAC THENL
[W(MP_TAC o PART_MATCH (rand o rand) MEASURE_DISJOINT_UNIONS_IMAGE o
lhand o snd) THEN
ASM_SIMP_TAC[DISJOINT; FINITE_NUMSEG; MEASURABLE_DIFF; MEASURABLE_INTER;
MEASURABLE_BALL] THEN
DISCH_THEN(SUBST1_TAC o SYM) THEN MATCH_MP_TAC MEASURE_SUBSET THEN
ASM_SIMP_TAC[MEASURABLE_UNIONS; FORALL_IN_IMAGE; FINITE_NUMSEG;
FINITE_IMAGE; MEASURABLE_DIFF; MEASURABLE_INTER; MEASURABLE_BALL] THEN
FIRST_X_ASSUM(fun th -> GEN_REWRITE_TAC RAND_CONV [GSYM th]) THEN
MATCH_MP_TAC SUBSET_UNIONS THEN REWRITE_TAC[SIMPLE_IMAGE] THEN
MATCH_MP_TAC IMAGE_SUBSET THEN REWRITE_TAC[SUBSET_UNIV];
REWRITE_TAC[real_div; SUM_LMUL; REAL_INV_POW; SUM_GP; LT] THEN
REWRITE_TAC[GSYM real_div] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
REWRITE_TAC[REAL_ARITH `e / &2 * (&1 - x) / (&1 / &2) <= e <=>
&0 <= e * x`] THEN
MATCH_MP_TAC REAL_LE_MUL THEN ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN
MATCH_MP_TAC REAL_POW_LE THEN CONV_TAC REAL_RAT_REDUCE_CONV]);;
let MEASURABLE_INNER_COMPACT = prove
(`!s:real^N->bool e.
measurable s /\ &0 < e
==> ?t. compact t /\ t
SUBSET s /\
measurable t /\ measure s < measure t + e`,
REPEAT STRIP_TAC THEN
FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [
HAS_MEASURE_MEASURE]) THEN
GEN_REWRITE_TAC LAND_CONV [
HAS_MEASURE_LIMIT] THEN
DISCH_THEN(MP_TAC o SPEC `e / &4`) THEN
ASM_SIMP_TAC[REAL_ARITH `&0 < e ==> &0 < e / &4`] THEN
DISCH_THEN(X_CHOOSE_THEN `B:real` (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
MP_TAC(ISPEC `ball(vec 0:real^N,B)`
BOUNDED_SUBSET_CLOSED_INTERVAL) THEN
REWRITE_TAC[
BOUNDED_BALL;
LEFT_IMP_EXISTS_THM] THEN
MAP_EVERY X_GEN_TAC [`a:real^N`; `b:real^N`] THEN DISCH_TAC THEN
DISCH_THEN(MP_TAC o SPECL [`a:real^N`; `b:real^N`]) THEN
ASM_REWRITE_TAC[
LEFT_IMP_EXISTS_THM] THEN
X_GEN_TAC `z:real` THEN STRIP_TAC THEN
MP_TAC(ISPECL [`interval[a:real^N,b]
DIFF s`; `e/ &4`]
MEASURABLE_OUTER_OPEN) THEN
ASM_SIMP_TAC[
MEASURABLE_DIFF;
MEASURABLE_INTERVAL;
REAL_ARITH `&0 < e ==> &0 < e / &4`] THEN
DISCH_THEN(X_CHOOSE_THEN `t:real^N->bool` STRIP_ASSUME_TAC) THEN
EXISTS_TAC `interval[a:real^N,b]
DIFF t` THEN REPEAT CONJ_TAC THENL
[REWRITE_TAC[
COMPACT_EQ_BOUNDED_CLOSED] THEN
ASM_SIMP_TAC[
CLOSED_DIFF;
CLOSED_INTERVAL;
BOUNDED_DIFF;
BOUNDED_INTERVAL];
ASM SET_TAC[];
ASM_SIMP_TAC[
MEASURABLE_DIFF;
MEASURABLE_INTERVAL];
MATCH_MP_TAC(REAL_ARITH
`&0 < e /\
measure(s) < measure(interval[a,b]
INTER s) + e / &4 /\
measure(t) < measure(interval[a,b]
DIFF s) + e / &4 /\
measure(interval[a,b]
INTER s) +
measure(interval[a,b]
DIFF s) = measure(interval[a,b]) /\
measure(interval[a,b]
INTER t) +
measure(interval[a,b]
DIFF t) = measure(interval[a,b]) /\
measure(interval[a,b]
INTER t) <= measure t
==> measure s < measure(interval[a,b]
DIFF t) + e`) THEN
ASM_SIMP_TAC[
MEASURE_SUBSET;
INTER_SUBSET;
MEASURABLE_INTER;
MEASURABLE_INTERVAL] THEN
CONJ_TAC THENL
[FIRST_ASSUM(SUBST_ALL_TAC o SYM o MATCH_MP
MEASURE_UNIQUE) THEN
ONCE_REWRITE_TAC[
INTER_COMM] THEN ASM_REAL_ARITH_TAC;
CONJ_TAC THEN MATCH_MP_TAC
MEASURE_DISJOINT_UNION_EQ THEN
ASM_SIMP_TAC[
MEASURABLE_INTER;
MEASURABLE_DIFF;
MEASURABLE_INTERVAL] THEN
SET_TAC[]]]);;
let HAS_MEASURE_LINEAR_SUFFICIENT = prove
(`!f:real^N->real^N m.
linear f /\
(!a b.
IMAGE f (interval[a,b])
has_measure
(m * measure(interval[a,b])))
==> !s. measurable s ==> (
IMAGE f s)
has_measure (m * measure s)`,
REPEAT GEN_TAC THEN STRIP_TAC THEN
DISJ_CASES_TAC(REAL_ARITH `m < &0 \/ &0 <= m`) THENL
[FIRST_X_ASSUM(MP_TAC o SPECL [`vec 0:real^N`; `vec 1:real^N`]) THEN
DISCH_THEN(MP_TAC o MATCH_MP
HAS_MEASURE_POS_LE) THEN
MATCH_MP_TAC(TAUT `~a ==> a ==> b`) THEN
MATCH_MP_TAC(REAL_ARITH `&0 < --m * x ==> ~(&0 <= m * x)`) THEN
MATCH_MP_TAC
REAL_LT_MUL THEN ASM_REWRITE_TAC[
REAL_NEG_GT0] THEN
REWRITE_TAC[
MEASURE_INTERVAL] THEN MATCH_MP_TAC
CONTENT_POS_LT THEN
SIMP_TAC[
VEC_COMPONENT;
REAL_LT_01];
ALL_TAC] THEN
ASM_CASES_TAC `!x y. (f:real^N->real^N) x = f y ==> x = y` THENL
[ALL_TAC;
SUBGOAL_THEN `!s. negligible(
IMAGE (f:real^N->real^N) s)` ASSUME_TAC THENL
[ASM_MESON_TAC[
NEGLIGIBLE_LINEAR_SINGULAR_IMAGE]; ALL_TAC] THEN
SUBGOAL_THEN `m * measure(interval[vec 0:real^N,vec 1]) = &0` MP_TAC THENL
[MATCH_MP_TAC(ISPEC `
IMAGE (f:real^N->real^N) (interval[vec 0,vec 1])`
HAS_MEASURE_UNIQUE) THEN
ASM_REWRITE_TAC[
HAS_MEASURE_0];
REWRITE_TAC[
REAL_ENTIRE;
MEASURE_INTERVAL] THEN
MATCH_MP_TAC(TAUT `~b /\ (a ==> c) ==> a \/ b ==> c`) THEN CONJ_TAC THENL
[SIMP_TAC[
CONTENT_EQ_0_INTERIOR;
INTERIOR_CLOSED_INTERVAL;
INTERVAL_NE_EMPTY;
VEC_COMPONENT;
REAL_LT_01];
ASM_SIMP_TAC[
REAL_MUL_LZERO;
HAS_MEASURE_0]]]] THEN
MP_TAC(ISPEC `f:real^N->real^N`
LINEAR_INJECTIVE_ISOMORPHISM) THEN
ASM_REWRITE_TAC[] THEN
DISCH_THEN(X_CHOOSE_THEN `h:real^N->real^N` STRIP_ASSUME_TAC) THEN
UNDISCH_THEN `!x y. (f:real^N->real^N) x = f y ==> x = y` (K ALL_TAC) THEN
SUBGOAL_THEN
`!s. bounded s /\ measurable s
==> (
IMAGE (f:real^N->real^N) s)
has_measure (m * measure s)`
ASSUME_TAC THENL
[REPEAT STRIP_TAC THEN
FIRST_ASSUM(MP_TAC o MATCH_MP
BOUNDED_SUBSET_CLOSED_INTERVAL) THEN
REWRITE_TAC[
LEFT_IMP_EXISTS_THM] THEN
MAP_EVERY X_GEN_TAC [`a:real^N`; `b:real^N`] THEN DISCH_TAC THEN
SUBGOAL_THEN
`!d.
COUNTABLE d /\
(!k. k
IN d ==> k
SUBSET interval[a,b] /\ ~(k = {}) /\
(?c d. k = interval[c,d])) /\
(!k1 k2. k1
IN d /\ k2
IN d /\ ~(k1 = k2)
==> interior k1
INTER interior k2 = {})
==>
IMAGE (f:real^N->real^N) (
UNIONS d)
has_measure
(m * measure(
UNIONS d))`
ASSUME_TAC THENL
[REWRITE_TAC[
IMAGE_UNIONS] THEN REPEAT STRIP_TAC THEN
SUBGOAL_THEN
`!g:real^N->real^N.
linear g
==> !k l. k
IN d /\ l
IN d /\ ~(k = l)
==> negligible((
IMAGE g k)
INTER (
IMAGE g l))`
MP_TAC THENL
[REPEAT STRIP_TAC THEN
ASM_CASES_TAC `!x y. (g:real^N->real^N) x = g y ==> x = y` THENL
[ALL_TAC;
ASM_MESON_TAC[
NEGLIGIBLE_LINEAR_SINGULAR_IMAGE;
NEGLIGIBLE_INTER]] THEN
MATCH_MP_TAC
NEGLIGIBLE_SUBSET THEN
EXISTS_TAC `frontier(
IMAGE (g:real^N->real^N) k
INTER IMAGE g l)
UNION
interior(
IMAGE g k
INTER IMAGE g l)` THEN
CONJ_TAC THENL
[ALL_TAC;
REWRITE_TAC[frontier] THEN MATCH_MP_TAC(SET_RULE
`s
SUBSET t ==> s
SUBSET (t
DIFF u)
UNION u`) THEN
REWRITE_TAC[
CLOSURE_SUBSET]] THEN
MATCH_MP_TAC
NEGLIGIBLE_UNION THEN CONJ_TAC THENL
[MATCH_MP_TAC
NEGLIGIBLE_CONVEX_FRONTIER THEN
MATCH_MP_TAC
CONVEX_INTER THEN CONJ_TAC THEN
MATCH_MP_TAC
CONVEX_LINEAR_IMAGE THEN ASM_MESON_TAC[
CONVEX_INTERVAL];
ALL_TAC] THEN
REWRITE_TAC[
INTERIOR_INTER] THEN MATCH_MP_TAC
NEGLIGIBLE_SUBSET THEN
EXISTS_TAC `
IMAGE (g:real^N->real^N) (interior k)
INTER
IMAGE g (interior l)` THEN
CONJ_TAC THENL
[MATCH_MP_TAC
NEGLIGIBLE_SUBSET THEN
EXISTS_TAC
`
IMAGE (g:real^N->real^N) (interior k
INTER interior l)` THEN
CONJ_TAC THENL
[ASM_SIMP_TAC[
IMAGE_CLAUSES;
NEGLIGIBLE_EMPTY]; ASM SET_TAC[]];
MATCH_MP_TAC(SET_RULE
`s
SUBSET u /\ t
SUBSET v ==> (s
INTER t)
SUBSET (u
INTER v)`) THEN
CONJ_TAC THEN MATCH_MP_TAC
INTERIOR_IMAGE_SUBSET THEN
ASM_MESON_TAC[
LINEAR_CONTINUOUS_AT]];
ALL_TAC] THEN
DISCH_THEN(fun th -> MP_TAC(SPEC `f:real^N->real^N` th) THEN
MP_TAC(SPEC `\x:real^N. x` th)) THEN
ASM_REWRITE_TAC[
LINEAR_ID; SET_RULE `
IMAGE (\x. x) s = s`] THEN
REPEAT STRIP_TAC THEN ASM_CASES_TAC `
FINITE(d:(real^N->bool)->bool)` THENL
[MP_TAC(ISPECL [`
IMAGE (f:real^N->real^N)`; `d:(real^N->bool)->bool`]
HAS_MEASURE_NEGLIGIBLE_UNIONS_IMAGE) THEN
ANTS_TAC THENL [ASM_MESON_TAC[measurable]; ALL_TAC] THEN
MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC THEN
MATCH_MP_TAC
EQ_TRANS THEN
EXISTS_TAC `sum d (\k:real^N->bool. m * measure k)` THEN CONJ_TAC THENL
[MATCH_MP_TAC
SUM_EQ THEN ASM_MESON_TAC[
MEASURE_UNIQUE]; ALL_TAC] THEN
REWRITE_TAC[
SUM_LMUL] THEN AP_TERM_TAC THEN
CONV_TAC SYM_CONV THEN MATCH_MP_TAC
MEASURE_NEGLIGIBLE_UNIONS THEN
ASM_REWRITE_TAC[GSYM
HAS_MEASURE_MEASURE] THEN
ASM_MESON_TAC[
MEASURABLE_INTERVAL];
ALL_TAC] THEN
MP_TAC(ISPEC `d:(real^N->bool)->bool`
COUNTABLE_AS_INJECTIVE_IMAGE) THEN
ASM_REWRITE_TAC[
INFINITE] THEN
DISCH_THEN(X_CHOOSE_THEN `s:num->real^N->bool`
(CONJUNCTS_THEN2 SUBST_ALL_TAC ASSUME_TAC)) THEN
MP_TAC(ISPEC `s:num->real^N->bool`
HAS_MEASURE_COUNTABLE_NEGLIGIBLE_UNIONS_BOUNDED) THEN
MP_TAC(ISPEC `\n:num.
IMAGE (f:real^N->real^N) (s n)`
HAS_MEASURE_COUNTABLE_NEGLIGIBLE_UNIONS_BOUNDED) THEN
RULE_ASSUM_TAC(REWRITE_RULE[
IMP_CONJ;
RIGHT_FORALL_IMP_THM;
FORALL_IN_IMAGE;
IN_UNIV]) THEN
RULE_ASSUM_TAC(REWRITE_RULE[IMP_IMP;
RIGHT_IMP_FORALL_THM]) THEN
ASM_SIMP_TAC[] THEN ONCE_REWRITE_TAC[
SIMPLE_IMAGE] THEN ANTS_TAC THENL
[REPEAT CONJ_TAC THENL
[ASM_MESON_TAC[
MEASURABLE_LINEAR_IMAGE_INTERVAL];
ASM_MESON_TAC[];
ONCE_REWRITE_TAC[GSYM
o_DEF] THEN
REWRITE_TAC[GSYM
IMAGE_UNIONS;
IMAGE_o] THEN
MATCH_MP_TAC
BOUNDED_LINEAR_IMAGE THEN ASM_REWRITE_TAC[] THEN
MATCH_MP_TAC
BOUNDED_SUBSET THEN REWRITE_TAC[
UNIONS_SUBSET] THEN
EXISTS_TAC `interval[a:real^N,b]` THEN
REWRITE_TAC[
BOUNDED_INTERVAL] THEN ASM SET_TAC[]];
ALL_TAC] THEN
STRIP_TAC THEN ANTS_TAC THENL
[REPEAT CONJ_TAC THENL
[ASM_MESON_TAC[
MEASURABLE_INTERVAL];
ASM_MESON_TAC[];
MATCH_MP_TAC
BOUNDED_SUBSET THEN REWRITE_TAC[
UNIONS_SUBSET] THEN
EXISTS_TAC `interval[a:real^N,b]` THEN
REWRITE_TAC[
BOUNDED_INTERVAL] THEN ASM SET_TAC[]];
ALL_TAC] THEN
STRIP_TAC THEN REWRITE_TAC[GSYM
IMAGE_o;
o_DEF] THEN
SUBGOAL_THEN `m * measure (
UNIONS (
IMAGE s (:num)):real^N->bool) =
measure(
UNIONS (
IMAGE (\x.
IMAGE f (s x)) (:num)):real^N->bool)`
(fun th -> ASM_REWRITE_TAC[GSYM
HAS_MEASURE_MEASURE; th]) THEN
ONCE_REWRITE_TAC[GSYM
LIFT_EQ] THEN
MATCH_MP_TAC
SERIES_UNIQUE THEN
EXISTS_TAC `\n:num. lift(measure(
IMAGE (f:real^N->real^N) (s n)))` THEN
EXISTS_TAC `from 0` THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC
SUMS_EQ THEN
EXISTS_TAC `\n:num. m % lift(measure(s n:real^N->bool))` THEN
CONJ_TAC THENL
[REWRITE_TAC[GSYM
LIFT_CMUL;
LIFT_EQ] THEN
ASM_MESON_TAC[
MEASURE_UNIQUE];
REWRITE_TAC[
LIFT_CMUL] THEN MATCH_MP_TAC
SERIES_CMUL THEN
ASM_REWRITE_TAC[]];
ALL_TAC] THEN
REWRITE_TAC[
HAS_MEASURE_INNER_OUTER_LE] THEN CONJ_TAC THEN
X_GEN_TAC `e:real` THEN DISCH_TAC THENL
[MP_TAC(ISPECL [`interval[a,b]
DIFF s:real^N->bool`; `a:real^N`;
`b:real^N`; `e / (&1 + abs m)`]
MEASURABLE_OUTER_INTERVALS_BOUNDED) THEN
ANTS_TAC THENL
[ASM_SIMP_TAC[
MEASURABLE_DIFF;
MEASURABLE_INTERVAL] THEN
ASM_SIMP_TAC[REAL_ARITH `&0 < &1 + abs x`;
REAL_LT_DIV] THEN SET_TAC[];
ALL_TAC] THEN
DISCH_THEN(X_CHOOSE_THEN `d:(real^N->bool)->bool` STRIP_ASSUME_TAC) THEN
EXISTS_TAC `
IMAGE f (interval[a,b])
DIFF
IMAGE (f:real^N->real^N) (
UNIONS d)` THEN
FIRST_X_ASSUM(MP_TAC o SPEC `d:(real^N->bool)->bool`) THEN
ASM_SIMP_TAC[
IMAGE_SUBSET] THEN DISCH_TAC THEN
CONJ_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN CONJ_TAC THENL
[ASM_MESON_TAC[
MEASURABLE_DIFF; measurable]; ALL_TAC] THEN
MATCH_MP_TAC
REAL_LE_TRANS THEN
EXISTS_TAC `measure(
IMAGE f (interval[a,b])) -
measure(
IMAGE (f:real^N->real^N) (
UNIONS d))` THEN
CONJ_TAC THENL
[ALL_TAC;
MATCH_MP_TAC
REAL_EQ_IMP_LE THEN CONV_TAC SYM_CONV THEN
MATCH_MP_TAC
MEASURE_DIFF_SUBSET THEN
REPEAT(CONJ_TAC THENL [ASM_MESON_TAC[measurable]; ALL_TAC]) THEN
MATCH_MP_TAC
IMAGE_SUBSET THEN ASM_SIMP_TAC[
UNIONS_SUBSET]] THEN
UNDISCH_TAC `!a b.
IMAGE (f:real^N->real^N) (interval [a,b])
has_measure m * measure (interval [a,b])` THEN
DISCH_THEN(ASSUME_TAC o SPECL [`a:real^N`; `b:real^N`]) THEN
REPEAT(FIRST_X_ASSUM(SUBST1_TAC o MATCH_MP
MEASURE_UNIQUE)) THEN
MATCH_MP_TAC
REAL_LE_TRANS THEN
EXISTS_TAC `m * measure(s:real^N->bool) - m * e / (&1 + abs m)` THEN
CONJ_TAC THENL
[REWRITE_TAC[REAL_ARITH `a - x <= a - y <=> y <= x`] THEN
REWRITE_TAC[
real_div; REAL_MUL_ASSOC] THEN
REWRITE_TAC[GSYM
real_div] THEN
ASM_SIMP_TAC[
REAL_LE_LDIV_EQ; REAL_ARITH `&0 < &1 + abs x`] THEN
GEN_REWRITE_TAC RAND_CONV [REAL_MUL_SYM] THEN
ASM_SIMP_TAC[
REAL_LE_RMUL_EQ] THEN REAL_ARITH_TAC;
ALL_TAC] THEN
REWRITE_TAC[GSYM
REAL_SUB_LDISTRIB] THEN MATCH_MP_TAC
REAL_LE_LMUL THEN
ASM_REWRITE_TAC[] THEN
FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH
`d <= a + e ==> a = i - s ==> s - e <= i - d`)) THEN
MATCH_MP_TAC
MEASURE_DIFF_SUBSET THEN
ASM_REWRITE_TAC[
MEASURABLE_INTERVAL];
MP_TAC(ISPECL [`s:real^N->bool`; `a:real^N`; `b:real^N`;
`e / (&1 + abs m)`]
MEASURABLE_OUTER_INTERVALS_BOUNDED) THEN
ASM_SIMP_TAC[
REAL_LT_DIV; REAL_ARITH `&0 < &1 + abs x`] THEN
DISCH_THEN(X_CHOOSE_THEN `d:(real^N->bool)->bool` STRIP_ASSUME_TAC) THEN
EXISTS_TAC `
IMAGE (f:real^N->real^N) (
UNIONS d)` THEN
FIRST_X_ASSUM(MP_TAC o SPEC `d:(real^N->bool)->bool`) THEN
ASM_SIMP_TAC[
IMAGE_SUBSET] THEN
SIMP_TAC[
HAS_MEASURE_MEASURABLE_MEASURE] THEN STRIP_TAC THEN
MATCH_MP_TAC
REAL_LE_TRANS THEN
EXISTS_TAC `m * measure(s:real^N->bool) + m * e / (&1 + abs m)` THEN
CONJ_TAC THENL
[REWRITE_TAC[GSYM REAL_ADD_LDISTRIB] THEN ASM_SIMP_TAC[
REAL_LE_LMUL];
REWRITE_TAC[
REAL_LE_LADD] THEN
REWRITE_TAC[
real_div; REAL_MUL_ASSOC] THEN
REWRITE_TAC[GSYM
real_div] THEN
ASM_SIMP_TAC[
REAL_LE_LDIV_EQ; REAL_ARITH `&0 < &1 + abs x`] THEN
GEN_REWRITE_TAC RAND_CONV [REAL_MUL_SYM] THEN
ASM_SIMP_TAC[
REAL_LE_RMUL_EQ] THEN REAL_ARITH_TAC]];
ALL_TAC] THEN
REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[
HAS_MEASURE_LIMIT] THEN
X_GEN_TAC `e:real` THEN DISCH_TAC THEN
FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [
HAS_MEASURE_MEASURE]) THEN
GEN_REWRITE_TAC LAND_CONV [
HAS_MEASURE_LIMIT] THEN
DISCH_THEN(MP_TAC o SPEC `e / (&1 + abs m)`) THEN
ASM_SIMP_TAC[
REAL_LT_DIV; REAL_ARITH `&0 < &1 + abs x`] THEN
DISCH_THEN(X_CHOOSE_THEN `B:real`
(CONJUNCTS_THEN2 ASSUME_TAC (LABEL_TAC "*"))) THEN
MP_TAC(ISPEC `ball(vec 0:real^N,B)`
BOUNDED_SUBSET_CLOSED_INTERVAL) THEN
REWRITE_TAC[
BOUNDED_BALL;
LEFT_IMP_EXISTS_THM] THEN
REMOVE_THEN "*" MP_TAC THEN
MATCH_MP_TAC
MONO_FORALL THEN X_GEN_TAC `c:real^N` THEN
MATCH_MP_TAC
MONO_FORALL THEN X_GEN_TAC `d:real^N` THEN
DISCH_THEN(fun th -> DISCH_TAC THEN MP_TAC th) THEN ASM_REWRITE_TAC[] THEN
DISCH_THEN(X_CHOOSE_THEN `z:real` STRIP_ASSUME_TAC) THEN
MP_TAC(ISPECL [`interval[c:real^N,d]`; `vec 0:real^N`]
BOUNDED_SUBSET_BALL) THEN
REWRITE_TAC[
BOUNDED_INTERVAL] THEN
DISCH_THEN(X_CHOOSE_THEN `D:real` STRIP_ASSUME_TAC) THEN
MP_TAC(ISPEC `f:real^N->real^N`
LINEAR_BOUNDED_POS) THEN
ASM_REWRITE_TAC[] THEN
DISCH_THEN(X_CHOOSE_THEN `C:real` STRIP_ASSUME_TAC) THEN
EXISTS_TAC `D * C:real` THEN ASM_SIMP_TAC[
REAL_LT_MUL] THEN
MAP_EVERY X_GEN_TAC [`a:real^N`; `b:real^N`] THEN DISCH_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPEC
`s
INTER (
IMAGE (h:real^N->real^N) (interval[a,b]))`) THEN
SUBGOAL_THEN
`
IMAGE (f:real^N->real^N) (s
INTER IMAGE h (interval [a,b])) =
(
IMAGE f s)
INTER interval[a,b]`
SUBST1_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN ANTS_TAC THENL
[ASM_SIMP_TAC[
BOUNDED_INTER;
BOUNDED_LINEAR_IMAGE;
BOUNDED_INTERVAL] THEN
ASM_SIMP_TAC[
MEASURABLE_INTER;
MEASURABLE_LINEAR_IMAGE_INTERVAL];
ALL_TAC] THEN
DISCH_TAC THEN EXISTS_TAC
`m * measure(s
INTER (
IMAGE (h:real^N->real^N) (interval[a,b])))` THEN
ASM_REWRITE_TAC[] THEN
MATCH_MP_TAC
REAL_LET_TRANS THEN EXISTS_TAC `m * e / (&1 + abs m)` THEN
CONJ_TAC THENL
[ALL_TAC;
REWRITE_TAC[
real_div; REAL_MUL_ASSOC] THEN REWRITE_TAC[GSYM
real_div] THEN
ASM_SIMP_TAC[
REAL_LT_LDIV_EQ; REAL_ARITH `&0 < &1 + abs x`] THEN
GEN_REWRITE_TAC RAND_CONV [REAL_MUL_SYM] THEN
ASM_SIMP_TAC[
REAL_LT_RMUL_EQ] THEN REAL_ARITH_TAC] THEN
REWRITE_TAC[GSYM
REAL_SUB_LDISTRIB;
REAL_ABS_MUL] THEN
GEN_REWRITE_TAC (LAND_CONV o LAND_CONV) [
real_abs] THEN
ASM_REWRITE_TAC[] THEN MATCH_MP_TAC
REAL_LE_LMUL THEN ASM_REWRITE_TAC[] THEN
FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH
`abs(z - m) < e ==> z <= w /\ w <= m ==> abs(w - m) <= e`)) THEN
SUBST1_TAC(SYM(MATCH_MP
MEASURE_UNIQUE
(ASSUME `s
INTER interval [c:real^N,d]
has_measure z`))) THEN
CONJ_TAC THEN MATCH_MP_TAC
MEASURE_SUBSET THEN
ASM_SIMP_TAC[
MEASURABLE_INTER;
MEASURABLE_LINEAR_IMAGE_INTERVAL;
MEASURABLE_INTERVAL;
INTER_SUBSET] THEN
MATCH_MP_TAC(SET_RULE
`!v. t
SUBSET v /\ v
SUBSET u ==> s
INTER t
SUBSET s
INTER u`) THEN
EXISTS_TAC `ball(vec 0:real^N,D)` THEN ASM_REWRITE_TAC[] THEN
MATCH_MP_TAC(SET_RULE
`!f. (!x. h(f x) = x) /\
IMAGE f s
SUBSET t ==> s
SUBSET IMAGE h t`) THEN
EXISTS_TAC `f:real^N->real^N` THEN ASM_REWRITE_TAC[] THEN
MATCH_MP_TAC
SUBSET_TRANS THEN EXISTS_TAC `ball(vec 0:real^N,D * C)` THEN
ASM_REWRITE_TAC[
SUBSET;
FORALL_IN_IMAGE;
IN_BALL_0] THEN
X_GEN_TAC `x:real^N` THEN DISCH_TAC THEN
MATCH_MP_TAC
REAL_LET_TRANS THEN EXISTS_TAC `C * norm(x:real^N)` THEN
ASM_REWRITE_TAC[] THEN GEN_REWRITE_TAC RAND_CONV [REAL_MUL_SYM] THEN
ASM_SIMP_TAC[
REAL_LT_LMUL_EQ]);;
let INDUCT_MATRIX_ROW_OPERATIONS = prove
(`!P:real^N^N->bool.
(!A i. 1 <= i /\ i <= dimindex(:N) /\ row i A = vec 0 ==> P A) /\
(!A. (!i j. 1 <= i /\ i <= dimindex(:N) /\
1 <= j /\ j <= dimindex(:N) /\ ~(i = j)
==> A$i$j = &0) ==> P A) /\
(!A m n. P A /\ 1 <= m /\ m <= dimindex(:N) /\
1 <= n /\ n <= dimindex(:N) /\ ~(m = n)
==> P(lambda i j. A$i$(swap(m,n) j))) /\
(!A m n c. P A /\ 1 <= m /\ m <= dimindex(:N) /\
1 <= n /\ n <= dimindex(:N) /\ ~(m = n)
==> P(lambda i. if i = m then row m A + c % row n A
else row i A))
==> !A. P A`,
GEN_TAC THEN
DISCH_THEN(CONJUNCTS_THEN2 (LABEL_TAC "zero_row") MP_TAC) THEN
DISCH_THEN(CONJUNCTS_THEN2 (LABEL_TAC "diagonal") MP_TAC) THEN
DISCH_THEN(CONJUNCTS_THEN2 (LABEL_TAC "swap_cols") (LABEL_TAC "row_op")) THEN
SUBGOAL_THEN
`!k A:real^N^N.
(!i j. 1 <= i /\ i <= dimindex(:N) /\
k <= j /\ j <= dimindex(:N) /\ ~(i = j)
==> A$i$j = &0)
==> P A`
(fun th -> GEN_TAC THEN MATCH_MP_TAC th THEN
EXISTS_TAC `dimindex(:N) + 1` THEN ARITH_TAC) THEN
MATCH_MP_TAC
num_INDUCTION THEN CONJ_TAC THENL
[REPEAT STRIP_TAC THEN USE_THEN "diagonal" MATCH_MP_TAC THEN
REPEAT STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
ASM_REWRITE_TAC[
LE_0];
ALL_TAC] THEN
X_GEN_TAC `k:num` THEN DISCH_THEN(LABEL_TAC "ind_hyp") THEN
DISJ_CASES_THEN2 SUBST1_TAC ASSUME_TAC (ARITH_RULE `k = 0 \/ 1 <= k`) THEN
ASM_REWRITE_TAC[ARITH] THEN
ASM_CASES_TAC `k <= dimindex(:N)` THENL
[ALL_TAC;
REPEAT STRIP_TAC THEN REMOVE_THEN "ind_hyp" MATCH_MP_TAC THEN
ASM_ARITH_TAC] THEN
SUBGOAL_THEN
`!A:real^N^N.
~(A$k$k = &0) /\
(!i j. 1 <= i /\ i <= dimindex (:N) /\
SUC k <= j /\ j <= dimindex (:N) /\ ~(i = j)
==> A$i$j = &0)
==> P A`
(LABEL_TAC "nonzero_hyp") THENL
[ALL_TAC;
X_GEN_TAC `A:real^N^N` THEN DISCH_TAC THEN
ASM_CASES_TAC `row k (A:real^N^N) = vec 0` THENL
[REMOVE_THEN "zero_row" MATCH_MP_TAC THEN ASM_MESON_TAC[];
ALL_TAC] THEN
FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE RAND_CONV [
CART_EQ]) THEN
SIMP_TAC[
VEC_COMPONENT; row;
LAMBDA_BETA] THEN
REWRITE_TAC[
NOT_FORALL_THM; NOT_IMP;
LEFT_IMP_EXISTS_THM] THEN
X_GEN_TAC `l:num` THEN STRIP_TAC THEN
ASM_CASES_TAC `l:num = k` THENL
[REMOVE_THEN "nonzero_hyp" MATCH_MP_TAC THEN ASM_MESON_TAC[];
ALL_TAC] THEN
REMOVE_THEN "swap_cols" (MP_TAC o SPECL
[`(lambda i j. (A:real^N^N)$i$swap(k,l) j):real^N^N`;
`k:num`; `l:num`]) THEN
ASM_SIMP_TAC[
LAMBDA_BETA] THEN ANTS_TAC THENL
[ALL_TAC;
MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC THEN
SIMP_TAC[
CART_EQ;
LAMBDA_BETA] THEN
REPEAT STRIP_TAC THEN REWRITE_TAC[swap] THEN
REPEAT(COND_CASES_TAC THEN ASM_SIMP_TAC[
LAMBDA_BETA])] THEN
REMOVE_THEN "nonzero_hyp" MATCH_MP_TAC THEN
ONCE_REWRITE_TAC[ARITH_RULE `SUC k <= i <=> 1 <= i /\ SUC k <= i`] THEN
ASM_SIMP_TAC[
LAMBDA_BETA] THEN
ASM_REWRITE_TAC[swap] THEN MAP_EVERY X_GEN_TAC [`i:num`; `j:num`] THEN
STRIP_TAC THEN SUBGOAL_THEN `l:num <= k` ASSUME_TAC THENL
[FIRST_X_ASSUM(MP_TAC o SPECL [`k:num`; `l:num`]) THEN
ASM_REWRITE_TAC[] THEN ARITH_TAC;
ALL_TAC] THEN
REPEAT(COND_CASES_TAC THEN ASM_REWRITE_TAC[]) THEN
FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN
ASM_ARITH_TAC] THEN
SUBGOAL_THEN
`!l A:real^N^N.
~(A$k$k = &0) /\
(!i j. 1 <= i /\ i <= dimindex (:N) /\
SUC k <= j /\ j <= dimindex (:N) /\ ~(i = j)
==> A$i$j = &0) /\
(!i. l <= i /\ i <= dimindex(:N) /\ ~(i = k) ==> A$i$k = &0)
==> P A`
MP_TAC THENL
[ALL_TAC;
DISCH_THEN(MP_TAC o SPEC `dimindex(:N) + 1`) THEN
REWRITE_TAC[
CONJ_ASSOC; ARITH_RULE `~(n + 1 <= i /\ i <= n)`]] THEN
MATCH_MP_TAC
num_INDUCTION THEN CONJ_TAC THENL
[GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
DISCH_THEN(CONJUNCTS_THEN2 (LABEL_TAC "main") (LABEL_TAC "aux")) THEN
USE_THEN "ind_hyp" MATCH_MP_TAC THEN
MAP_EVERY X_GEN_TAC [`i:num`; `j:num`] THEN STRIP_TAC THEN
ASM_CASES_TAC `j:num = k` THENL
[ASM_REWRITE_TAC[] THEN USE_THEN "aux" MATCH_MP_TAC THEN ASM_ARITH_TAC;
REMOVE_THEN "main" MATCH_MP_TAC THEN ASM_ARITH_TAC];
ALL_TAC] THEN
X_GEN_TAC `l:num` THEN DISCH_THEN(LABEL_TAC "inner_hyp") THEN
GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
DISCH_THEN(CONJUNCTS_THEN2 (LABEL_TAC "main") (LABEL_TAC "aux")) THEN
ASM_CASES_TAC `l:num = k` THENL
[REMOVE_THEN "inner_hyp" MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN
REPEAT STRIP_TAC THEN REMOVE_THEN "aux" MATCH_MP_TAC THEN ASM_ARITH_TAC;
ALL_TAC] THEN
DISJ_CASES_TAC(ARITH_RULE `l = 0 \/ 1 <= l`) THENL
[REMOVE_THEN "ind_hyp" MATCH_MP_TAC THEN
MAP_EVERY X_GEN_TAC [`i:num`; `j:num`] THEN STRIP_TAC THEN
ASM_CASES_TAC `j:num = k` THENL
[ASM_REWRITE_TAC[] THEN REMOVE_THEN "aux" MATCH_MP_TAC THEN ASM_ARITH_TAC;
REMOVE_THEN "main" MATCH_MP_TAC THEN ASM_ARITH_TAC];
ALL_TAC] THEN
ASM_CASES_TAC `l <= dimindex(:N)` THENL
[ALL_TAC;
REMOVE_THEN "inner_hyp" MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN
ASM_ARITH_TAC] THEN
REMOVE_THEN "inner_hyp" (MP_TAC o SPECL
[`(lambda i. if i = l then row l (A:real^N^N) + --(A$l$k/A$k$k) % row k A
else row i A):real^N^N`]) THEN
ANTS_TAC THENL
[SUBGOAL_THEN `!i. l <= i ==> 1 <= i` ASSUME_TAC THENL
[ASM_ARITH_TAC; ALL_TAC] THEN
ONCE_REWRITE_TAC[ARITH_RULE `SUC k <= j <=> 1 <= j /\ SUC k <= j`] THEN
ASM_SIMP_TAC[
LAMBDA_BETA; row;
COND_COMPONENT;
VECTOR_ADD_COMPONENT;
VECTOR_MUL_COMPONENT] THEN
ASM_SIMP_TAC[REAL_FIELD `~(y = &0) ==> x + --(x / y) * y = &0`] THEN
REWRITE_TAC[
AND_FORALL_THM] THEN X_GEN_TAC `i:num` THEN
ASM_CASES_TAC `i:num = l` THEN ASM_REWRITE_TAC[] THENL
[REPEAT STRIP_TAC THEN
MATCH_MP_TAC(REAL_RING `x = &0 /\ y = &0 ==> x + z * y = &0`) THEN
CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC;
REPEAT STRIP_TAC THEN REMOVE_THEN "aux" MATCH_MP_TAC THEN ASM_ARITH_TAC];
ALL_TAC] THEN
DISCH_TAC THEN REMOVE_THEN "row_op" (MP_TAC o SPECL
[`(lambda i. if i = l then row l A + --(A$l$k / A$k$k) % row k A
else row i (A:real^N^N)):real^N^N`;
`l:num`; `k:num`; `(A:real^N^N)$l$k / A$k$k`]) THEN
ASM_REWRITE_TAC[] THEN MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC THEN
ASM_SIMP_TAC[
CART_EQ;
LAMBDA_BETA;
VECTOR_ADD_COMPONENT;
VECTOR_MUL_COMPONENT; row;
COND_COMPONENT] THEN
REPEAT STRIP_TAC THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
REAL_ARITH_TAC);;
let INDUCT_MATRIX_ELEMENTARY = prove
(`!P:real^N^N->bool.
(!A B. P A /\ P B ==> P(A ** B)) /\
(!A i. 1 <= i /\ i <= dimindex(:N) /\ row i A = vec 0 ==> P A) /\
(!A. (!i j. 1 <= i /\ i <= dimindex(:N) /\
1 <= j /\ j <= dimindex(:N) /\ ~(i = j)
==> A$i$j = &0) ==> P A) /\
(!m n. 1 <= m /\ m <= dimindex(:N) /\
1 <= n /\ n <= dimindex(:N) /\ ~(m = n)
==> P(lambda i j. (mat 1:real^N^N)$i$(swap(m,n) j))) /\
(!m n c. 1 <= m /\ m <= dimindex(:N) /\
1 <= n /\ n <= dimindex(:N) /\ ~(m = n)
==> P(lambda i j. if i = m /\ j = n then c
else if i = j then &1 else &0))
==> !A. P A`,
let INDUCT_MATRIX_ELEMENTARY_ALT = prove
(`!P:real^N^N->bool.
(!A B. P A /\ P B ==> P(A ** B)) /\
(!A i. 1 <= i /\ i <= dimindex(:N) /\ row i A = vec 0 ==> P A) /\
(!A. (!i j. 1 <= i /\ i <= dimindex(:N) /\
1 <= j /\ j <= dimindex(:N) /\ ~(i = j)
==> A$i$j = &0) ==> P A) /\
(!m n. 1 <= m /\ m <= dimindex(:N) /\
1 <= n /\ n <= dimindex(:N) /\ ~(m = n)
==> P(lambda i j. (mat 1:real^N^N)$i$(swap(m,n) j))) /\
(!m n. 1 <= m /\ m <= dimindex(:N) /\
1 <= n /\ n <= dimindex(:N) /\ ~(m = n)
==> P(lambda i j. if i = m /\ j = n \/ i = j then &1 else &0))
==> !A. P A`,
GEN_TAC THEN STRIP_TAC THEN MATCH_MP_TAC
INDUCT_MATRIX_ELEMENTARY THEN
ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC THEN
ASM_CASES_TAC `c = &0` THENL
[FIRST_X_ASSUM(fun th -> MATCH_MP_TAC th THEN
MAP_EVERY X_GEN_TAC [`i:num`; `j:num`]) THEN
ASM_SIMP_TAC[
LAMBDA_BETA;
COND_ID];
ALL_TAC] THEN
SUBGOAL_THEN
`(lambda i j. if i = m /\ j = n then c else if i = j then &1 else &0) =
((lambda i j. if i = j then if j = n then inv c else &1 else &0):real^N^N) **
((lambda i j. if i = m /\ j = n \/ i = j then &1 else &0):real^N^N) **
((lambda i j. if i = j then if j = n then c else &1 else &0):real^N^N)`
SUBST1_TAC THENL
[ALL_TAC;
REPEAT(MATCH_MP_TAC(ASSUME `!A B:real^N^N. P A /\ P B ==> P(A ** B)`) THEN
CONJ_TAC) THEN
ASM_SIMP_TAC[] THEN FIRST_X_ASSUM(fun th -> MATCH_MP_TAC th THEN
MAP_EVERY X_GEN_TAC [`i:num`; `j:num`]) THEN
ASM_SIMP_TAC[
LAMBDA_BETA]] THEN
SIMP_TAC[
CART_EQ;
matrix_mul;
LAMBDA_BETA] THEN
X_GEN_TAC `i:num` THEN STRIP_TAC THEN
X_GEN_TAC `j:num` THEN STRIP_TAC THEN
ASM_SIMP_TAC[
SUM_DELTA;
IN_NUMSEG; REAL_ARITH
`(if p then &1 else &0) * (if q then c else &0) =
if q then if p then c else &0 else &0`] THEN
REWRITE_TAC[REAL_ARITH
`(if p then x else &0) * y = (if p then x * y else &0)`] THEN
GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [
EQ_SYM_EQ] THEN
ASM_SIMP_TAC[
SUM_DELTA;
IN_NUMSEG] THEN
ASM_CASES_TAC `i:num = m` THEN ASM_REWRITE_TAC[] THEN
ASM_CASES_TAC `j:num = n` THEN ASM_REWRITE_TAC[REAL_MUL_LID;
EQ_SYM_EQ] THEN
ASM_CASES_TAC `i:num = n` THEN
ASM_SIMP_TAC[REAL_MUL_LINV; REAL_MUL_LID;
REAL_MUL_RZERO]);;
let INDUCT_LINEAR_ELEMENTARY = prove
(`!P. (!f g. linear f /\ linear g /\ P f /\ P g ==> P(f o g)) /\
(!f i. linear f /\ 1 <= i /\ i <= dimindex(:N) /\ (!x. (f x)$i = &0)
==> P f) /\
(!c. P(\x. lambda i. c i * x$i)) /\
(!m n. 1 <= m /\ m <= dimindex(:N) /\
1 <= n /\ n <= dimindex(:N) /\ ~(m = n)
==> P(\x. lambda i. x$swap(m,n) i)) /\
(!m n. 1 <= m /\ m <= dimindex(:N) /\
1 <= n /\ n <= dimindex(:N) /\ ~(m = n)
==> P(\x. lambda i. if i = m then x$m + x$n else x$i))
==> !f:real^N->real^N. linear f ==> P f`,
GEN_TAC THEN
MP_TAC(ISPEC `\A:real^N^N. P(\x:real^N. A ** x):bool`
INDUCT_MATRIX_ELEMENTARY_ALT) THEN
REWRITE_TAC[] THEN MATCH_MP_TAC MONO_IMP THEN CONJ_TAC THENL
[ALL_TAC;
DISCH_TAC THEN X_GEN_TAC `f:real^N->real^N` THEN DISCH_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPEC `matrix(f:real^N->real^N)`) THEN
ASM_SIMP_TAC[
MATRIX_WORKS] THEN REWRITE_TAC[ETA_AX]] THEN
MATCH_MP_TAC MONO_AND THEN CONJ_TAC THENL
[DISCH_TAC THEN MAP_EVERY X_GEN_TAC [`A:real^N^N`; `B:real^N^N`] THEN
STRIP_TAC THEN FIRST_X_ASSUM(MP_TAC o SPECL
[`\x:real^N. (A:real^N^N) ** x`; `\x:real^N. (B:real^N^N) ** x`]) THEN
ASM_REWRITE_TAC[
MATRIX_VECTOR_MUL_LINEAR;
o_DEF] THEN
REWRITE_TAC[
MATRIX_VECTOR_MUL_ASSOC];
ALL_TAC] THEN
MATCH_MP_TAC MONO_AND THEN CONJ_TAC THENL
[DISCH_TAC THEN MAP_EVERY X_GEN_TAC [`A:real^N^N`; `m:num`] THEN
STRIP_TAC THEN FIRST_X_ASSUM(MP_TAC o SPECL
[`\x:real^N. (A:real^N^N) ** x`; `m:num`]) THEN
ASM_REWRITE_TAC[
MATRIX_VECTOR_MUL_LINEAR] THEN
DISCH_THEN MATCH_MP_TAC THEN
UNDISCH_TAC `row m (A:real^N^N) = vec 0` THEN
ASM_SIMP_TAC[
CART_EQ; row;
LAMBDA_BETA;
VEC_COMPONENT;
matrix_vector_mul;
REAL_MUL_LZERO;
SUM_0];
ALL_TAC] THEN
MATCH_MP_TAC MONO_AND THEN CONJ_TAC THENL
[DISCH_TAC THEN X_GEN_TAC `A:real^N^N` THEN STRIP_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPEC `\i. (A:real^N^N)$i$i`) THEN
MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC THEN
ASM_SIMP_TAC[
CART_EQ;
matrix_vector_mul;
FUN_EQ_THM;
LAMBDA_BETA] THEN
MAP_EVERY X_GEN_TAC [`x:real^N`; `i:num`] THEN STRIP_TAC THEN
MATCH_MP_TAC
EQ_TRANS THEN EXISTS_TAC
`sum(1..dimindex(:N)) (\j. if j = i then (A:real^N^N)$i$j * (x:real^N)$j
else &0)` THEN
CONJ_TAC THENL [ASM_SIMP_TAC[
SUM_DELTA;
IN_NUMSEG]; ALL_TAC] THEN
MATCH_MP_TAC
SUM_EQ_NUMSEG THEN X_GEN_TAC `j:num` THEN STRIP_TAC THEN
ASM_SIMP_TAC[] THEN COND_CASES_TAC THEN ASM_SIMP_TAC[
REAL_MUL_LZERO];
ALL_TAC] THEN
MATCH_MP_TAC MONO_AND THEN CONJ_TAC THEN
MATCH_MP_TAC
MONO_FORALL THEN X_GEN_TAC `m:num` THEN
MATCH_MP_TAC
MONO_FORALL THEN X_GEN_TAC `n:num` THEN
DISCH_THEN(fun th -> STRIP_TAC THEN MP_TAC th) THEN
ASM_REWRITE_TAC[] THEN MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC THEN
ASM_SIMP_TAC[
CART_EQ;
matrix_vector_mul;
FUN_EQ_THM;
LAMBDA_BETA;
mat;
IN_DIMINDEX_SWAP]
THENL
[ONCE_REWRITE_TAC[
SWAP_GALOIS] THEN ONCE_REWRITE_TAC[
COND_RAND] THEN
ONCE_REWRITE_TAC[
COND_RATOR] THEN
SIMP_TAC[
SUM_DELTA; REAL_MUL_LID;
REAL_MUL_LZERO;
IN_NUMSEG] THEN
REPEAT STRIP_TAC THEN REWRITE_TAC[swap] THEN
COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN ASM_ARITH_TAC;
MAP_EVERY X_GEN_TAC [`x:real^N`; `i:num`] THEN STRIP_TAC THEN
ASM_CASES_TAC `i:num = m` THEN ASM_REWRITE_TAC[] THEN
ONCE_REWRITE_TAC[
COND_RAND] THEN ONCE_REWRITE_TAC[
COND_RATOR] THEN
GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [
EQ_SYM_EQ] THEN
ASM_SIMP_TAC[
SUM_DELTA;
REAL_MUL_LZERO; REAL_MUL_LID;
IN_NUMSEG] THEN
MATCH_MP_TAC
EQ_TRANS THEN EXISTS_TAC
`sum {m,n} (\j. if n = j \/ j = m then (x:real^N)$j else &0)` THEN
CONJ_TAC THENL
[SIMP_TAC[
SUM_CLAUSES;
FINITE_RULES;
IN_INSERT;
NOT_IN_EMPTY] THEN
ASM_REWRITE_TAC[
REAL_ADD_RID];
CONV_TAC SYM_CONV THEN MATCH_MP_TAC
SUM_SUPERSET THEN
ASM_SIMP_TAC[
SUBSET;
IN_INSERT;
NOT_IN_EMPTY; DE_MORGAN_THM;
IN_NUMSEG;
REAL_MUL_LZERO] THEN
ASM_ARITH_TAC]]);;
let LAMBDA_SWAP_GALOIS = prove
(`!x:real^N y:real^N.
1 <= m /\ m <= dimindex(:N) /\ 1 <= n /\ n <= dimindex(:N)
==> (x = (lambda i. y$swap(m,n) i) <=>
(lambda i. x$swap(m,n) i) = y)`,
let LAMBDA_ADD_GALOIS = prove
(`!x:real^N y:real^N.
1 <= m /\ m <= dimindex(:N) /\ 1 <= n /\ n <= dimindex(:N) /\
~(m = n)
==> (x = (lambda i. if i = m then y$m + y$n else y$i) <=>
(lambda i. if i = m then x$m - x$n else x$i) = y)`,
SIMP_TAC[
CART_EQ;
LAMBDA_BETA] THEN
REPEAT GEN_TAC THEN STRIP_TAC THEN EQ_TAC THEN
DISCH_TAC THEN X_GEN_TAC `i:num` THEN STRIP_TAC THEN
FIRST_ASSUM(MP_TAC o SPEC `n:num`) THEN
FIRST_X_ASSUM(MP_TAC o SPEC `i:num`) THEN
ASM_REWRITE_TAC[] THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
REAL_ARITH_TAC);;
let HAS_MEASURE_SHEAR_INTERVAL = prove
(`!a b:real^N m n.
1 <= m /\ m <= dimindex(:N) /\
1 <= n /\ n <= dimindex(:N) /\
~(m = n) /\ ~(interval[a,b] = {}) /\
&0 <= a$n
==> (
IMAGE (\x. (lambda i. if i = m then x$m + x$n else x$i))
(interval[a,b]):real^N->bool)
has_measure measure (interval [a,b])`,
let HAS_MEASURE_LINEAR_IMAGE = prove
(`!f:real^N->real^N s.
linear f /\ measurable s
==> (
IMAGE f s)
has_measure (abs(det(matrix f)) * measure s)`,
REWRITE_TAC[
IMP_CONJ;
RIGHT_FORALL_IMP_THM] THEN
MATCH_MP_TAC
INDUCT_LINEAR_ELEMENTARY THEN REPEAT CONJ_TAC THENL
[MAP_EVERY X_GEN_TAC [`f:real^N->real^N`; `g:real^N->real^N`] THEN
REPLICATE_TAC 2 (DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
DISCH_THEN(fun th -> REPEAT STRIP_TAC THEN MP_TAC th) THEN
DISCH_THEN(CONJUNCTS_THEN2
(MP_TAC o SPEC `
IMAGE (g:real^N->real^N) s`)
(MP_TAC o SPEC `s:real^N->bool`)) THEN
ASM_REWRITE_TAC[] THEN
GEN_REWRITE_TAC LAND_CONV [
HAS_MEASURE_MEASURABLE_MEASURE] THEN
STRIP_TAC THEN ASM_SIMP_TAC[
MATRIX_COMPOSE;
DET_MUL;
REAL_ABS_MUL] THEN
REWRITE_TAC[
IMAGE_o; GSYM REAL_MUL_ASSOC];
MAP_EVERY X_GEN_TAC [`f:real^N->real^N`; `m:num`] THEN STRIP_TAC THEN
SUBGOAL_THEN `~(!x y. (f:real^N->real^N) x = f y ==> x = y)`
ASSUME_TAC THENL
[ASM_SIMP_TAC[
LINEAR_SINGULAR_INTO_HYPERPLANE] THEN
EXISTS_TAC `basis m:real^N` THEN
ASM_SIMP_TAC[
BASIS_NONZERO;
DOT_BASIS];
ALL_TAC] THEN
MP_TAC(ISPEC `matrix f:real^N^N`
INVERTIBLE_DET_NZ) THEN
ASM_SIMP_TAC[
INVERTIBLE_LEFT_INVERSE;
MATRIX_LEFT_INVERTIBLE_INJECTIVE;
MATRIX_WORKS;
REAL_ABS_NUM;
REAL_MUL_LZERO] THEN
DISCH_THEN(K ALL_TAC) THEN REWRITE_TAC[
HAS_MEASURE_0] THEN
ASM_SIMP_TAC[
NEGLIGIBLE_LINEAR_SINGULAR_IMAGE];
MAP_EVERY X_GEN_TAC [`c:num->real`; `s:real^N->bool`] THEN
DISCH_TAC THEN
FIRST_ASSUM(ASSUME_TAC o REWRITE_RULE[
HAS_MEASURE_MEASURE]) THEN
FIRST_ASSUM(MP_TAC o SPEC `c:num->real` o
MATCH_MP
HAS_MEASURE_STRETCH) THEN
MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC THEN
AP_THM_TAC THEN AP_TERM_TAC THEN AP_TERM_TAC THEN
SIMP_TAC[matrix;
LAMBDA_BETA] THEN
W(MP_TAC o PART_MATCH (lhs o rand)
DET_DIAGONAL o rand o snd) THEN
SIMP_TAC[
LAMBDA_BETA;
BASIS_COMPONENT;
REAL_MUL_RZERO] THEN
DISCH_THEN(K ALL_TAC) THEN MATCH_MP_TAC
PRODUCT_EQ_NUMSEG THEN
REWRITE_TAC[
REAL_MUL_RID];
MAP_EVERY X_GEN_TAC [`m:num`; `n:num`] THEN STRIP_TAC THEN
MATCH_MP_TAC
HAS_MEASURE_LINEAR_SUFFICIENT THEN
ASM_SIMP_TAC[linear;
LAMBDA_BETA;
IN_DIMINDEX_SWAP;
VECTOR_ADD_COMPONENT;
VECTOR_MUL_COMPONENT;
CART_EQ] THEN
MAP_EVERY X_GEN_TAC [`a:real^N`; `b:real^N`] THEN
SUBGOAL_THEN `matrix (\x:real^N. lambda i. x$swap (m,n) i):real^N^N =
transp(lambda i j. (mat 1:real^N^N)$i$swap (m,n) j)`
SUBST1_TAC THENL
[ASM_SIMP_TAC[
MATRIX_EQ;
LAMBDA_BETA;
IN_DIMINDEX_SWAP;
matrix_vector_mul;
CART_EQ; matrix; mat; basis;
COND_COMPONENT; transp] THEN
REWRITE_TAC[
EQ_SYM_EQ];
ALL_TAC] THEN
REWRITE_TAC[
DET_TRANSP] THEN
W(MP_TAC o PART_MATCH (lhs o rand)
DET_PERMUTE_COLUMNS o
rand o lhand o rand o snd) THEN
ASM_SIMP_TAC[
PERMUTES_SWAP;
IN_NUMSEG; ETA_AX] THEN
DISCH_THEN(K ALL_TAC) THEN
REWRITE_TAC[
DET_I;
REAL_ABS_SIGN;
REAL_MUL_RID; REAL_MUL_LID] THEN
ASM_CASES_TAC `interval[a:real^N,b] = {}` THENL
[ASM_SIMP_TAC[
IMAGE_CLAUSES;
HAS_MEASURE_EMPTY;
MEASURE_EMPTY];
ALL_TAC] THEN
SUBGOAL_THEN
`~(
IMAGE (\x:real^N. lambda i. x$swap (m,n) i)
(interval[a,b]):real^N->bool = {})`
MP_TAC THENL [ASM_REWRITE_TAC[
IMAGE_EQ_EMPTY]; ALL_TAC] THEN
SUBGOAL_THEN
`
IMAGE (\x:real^N. lambda i. x$swap (m,n) i)
(interval[a,b]):real^N->bool =
interval[(lambda i. a$swap (m,n) i),
(lambda i. b$swap (m,n) i)]`
SUBST1_TAC THENL
[REWRITE_TAC[
EXTENSION;
IN_INTERVAL;
IN_IMAGE] THEN
ASM_SIMP_TAC[
LAMBDA_SWAP_GALOIS;
UNWIND_THM1] THEN
SIMP_TAC[
LAMBDA_BETA] THEN GEN_TAC THEN EQ_TAC THEN
DISCH_TAC THEN X_GEN_TAC `i:num` THEN STRIP_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPEC `swap(m,n) (i:num)`) THEN
ASM_SIMP_TAC[
IN_DIMINDEX_SWAP] THEN
ASM_MESON_TAC[REWRITE_RULE[
FUN_EQ_THM;
o_THM;
I_THM]
SWAP_IDEMPOTENT];
ALL_TAC] THEN
REWRITE_TAC[
HAS_MEASURE_MEASURABLE_MEASURE;
MEASURABLE_INTERVAL] THEN
REWRITE_TAC[
MEASURE_INTERVAL] THEN
ASM_SIMP_TAC[
CONTENT_CLOSED_INTERVAL; GSYM
INTERVAL_NE_EMPTY] THEN
DISCH_THEN(K ALL_TAC) THEN SIMP_TAC[
LAMBDA_BETA] THEN
ASM_SIMP_TAC[GSYM
VECTOR_SUB_COMPONENT;
IN_DIMINDEX_SWAP] THEN
MP_TAC(ISPECL [`\i. (b - a:real^N)$i`; `swap(m:num,n)`; `1..dimindex(:N)`]
(GSYM
PRODUCT_PERMUTE)) THEN
REWRITE_TAC[
o_DEF] THEN DISCH_THEN MATCH_MP_TAC THEN
ASM_SIMP_TAC[
PERMUTES_SWAP;
IN_NUMSEG];
MAP_EVERY X_GEN_TAC [`m:num`; `n:num`] THEN STRIP_TAC THEN
MATCH_MP_TAC
HAS_MEASURE_LINEAR_SUFFICIENT THEN
MATCH_MP_TAC(TAUT `a /\ (a ==> b) ==> a /\ b`) THEN CONJ_TAC THENL
[ASM_SIMP_TAC[linear;
LAMBDA_BETA;
VECTOR_ADD_COMPONENT;
VECTOR_MUL_COMPONENT;
CART_EQ] THEN REAL_ARITH_TAC;
DISCH_TAC] THEN
MAP_EVERY X_GEN_TAC [`a:real^N`; `b:real^N`] THEN
SUBGOAL_THEN
`det(matrix(\x. lambda i. if i = m then (x:real^N)$m + x$n
else x$i):real^N^N) = &1`
SUBST1_TAC THENL
[ASM_SIMP_TAC[matrix; basis;
COND_COMPONENT;
LAMBDA_BETA] THEN
FIRST_ASSUM(DISJ_CASES_TAC o MATCH_MP (ARITH_RULE
`~(m:num = n) ==> m < n \/ n < m`))
THENL
[W(MP_TAC o PART_MATCH (lhs o rand)
DET_UPPERTRIANGULAR o lhs o snd);
W(MP_TAC o PART_MATCH (lhs o rand)
DET_LOWERTRIANGULAR o lhs o snd)]
THEN ASM_SIMP_TAC[
LAMBDA_BETA;
BASIS_COMPONENT;
COND_COMPONENT;
matrix;
REAL_ADD_RID;
COND_ID;
PRODUCT_CONST_NUMSEG;
REAL_POW_ONE] THEN
DISCH_THEN MATCH_MP_TAC THEN
REPEAT GEN_TAC THEN REPEAT(COND_CASES_TAC THEN ASM_REWRITE_TAC[]) THEN
ASM_ARITH_TAC;
ALL_TAC] THEN
REWRITE_TAC[
REAL_ABS_NUM; REAL_MUL_LID] THEN
ASM_CASES_TAC `interval[a:real^N,b] = {}` THENL
[ASM_SIMP_TAC[
IMAGE_CLAUSES;
HAS_MEASURE_EMPTY;
MEASURE_EMPTY];
ALL_TAC] THEN
SUBGOAL_THEN
`
IMAGE (\x. lambda i. if i = m then x$m + x$n else x$i) (interval [a,b]) =
IMAGE (\x:real^N. (lambda i. if i = m \/ i = n then a$n else &0) +
x)
(
IMAGE (\x:real^N. lambda i. if i = m then x$m + x$n else x$i)
(
IMAGE (\x. (lambda i. if i = n then --(a$n) else &0) + x)
(interval[a,b])))`
SUBST1_TAC THENL
[REWRITE_TAC[GSYM
IMAGE_o] THEN AP_THM_TAC THEN AP_TERM_TAC THEN
ASM_SIMP_TAC[
FUN_EQ_THM;
o_THM;
VECTOR_ADD_COMPONENT;
LAMBDA_BETA;
CART_EQ] THEN
MAP_EVERY X_GEN_TAC [`x:real^N`; `i:num`] THEN
STRIP_TAC THEN ASM_CASES_TAC `i:num = m` THEN ASM_REWRITE_TAC[] THEN
ASM_CASES_TAC `i:num = n` THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC;
ALL_TAC] THEN
MATCH_MP_TAC
HAS_MEASURE_TRANSLATION THEN
SUBGOAL_THEN
`measure(interval[a,b]) =
measure(
IMAGE (\x:real^N. (lambda i. if i = n then --(a$n) else &0) + x)
(interval[a,b]):real^N->bool)`
SUBST1_TAC THENL [REWRITE_TAC[
MEASURE_TRANSLATION]; ALL_TAC] THEN
SUBGOAL_THEN
`~(
IMAGE (\x:real^N. (lambda i. if i = n then --(a$n) else &0) + x)
(interval[a,b]):real^N->bool = {})`
MP_TAC THENL [ASM_SIMP_TAC[
IMAGE_EQ_EMPTY]; ALL_TAC] THEN
ONCE_REWRITE_TAC[VECTOR_ARITH `c + x:real^N = &1 % x + c`] THEN
ASM_REWRITE_TAC[
IMAGE_AFFINITY_INTERVAL;
REAL_POS] THEN
DISCH_TAC THEN MATCH_MP_TAC
HAS_MEASURE_SHEAR_INTERVAL THEN
ASM_SIMP_TAC[
LAMBDA_BETA;
VECTOR_ADD_COMPONENT;
VECTOR_MUL_COMPONENT] THEN
REAL_ARITH_TAC]);;
let CONGRUENT_IMAGE_STD_SIMPLEX = prove
(`!p. p permutes 1..dimindex(:N)
==> {x:real^N | &0 <= x$(p 1) /\ x$(p(dimindex(:N))) <= &1 /\
(!i. 1 <= i /\ i < dimindex(:N)
==> x$(p i) <= x$(p(i + 1)))} =
IMAGE (\x:real^N. lambda i. sum(1..inverse p(i)) (\j. x$j))
{x | (!i. 1 <= i /\ i <= dimindex (:N) ==> &0 <= x$i) /\
sum (1..dimindex (:N)) (\i. x$i) <= &1}`,
let HAS_MEASURE_IMAGE_STD_SIMPLEX = prove
(`!p. p permutes 1..dimindex(:N)
==> {x:real^N | &0 <= x$(p 1) /\ x$(p(dimindex(:N))) <= &1 /\
(!i. 1 <= i /\ i < dimindex(:N)
==> x$(p i) <= x$(p(i + 1)))}
has_measure
(measure (convex hull
(vec 0
INSERT {basis i:real^N | 1 <= i /\ i <= dimindex(:N)})))`,
let MEASURE_TRIANGLE = prove
(`!a b c:real^2.
measure(convex hull {a,b,c}) =
abs((b$1 - a$1) * (c$2 - a$2) - (b$2 - a$2) * (c$1 - a$1)) / &2`,
let HAS_MEASURE_TETRAHEDRON = prove
(`!a b c d:real^3.
convex hull {a,b,c,d}
has_measure
abs((b$1 - a$1) * (c$2 - a$2) * (d$3 - a$3) +
(b$2 - a$2) * (c$3 - a$3) * (d$1 - a$1) +
(b$3 - a$3) * (c$1 - a$1) * (d$2 - a$2) -
(b$1 - a$1) * (c$3 - a$3) * (d$2 - a$2) -
(b$2 - a$2) * (c$1 - a$1) * (d$3 - a$3) -
(b$3 - a$3) * (c$2 - a$2) * (d$1 - a$1)) /
&6`,
let MEASURE_TETRAHEDRON = prove
(`!a b c d:real^3.
measure(convex hull {a,b,c,d}) =
abs((b$1 - a$1) * (c$2 - a$2) * (d$3 - a$3) +
(b$2 - a$2) * (c$3 - a$3) * (d$1 - a$1) +
(b$3 - a$3) * (c$1 - a$1) * (d$2 - a$2) -
(b$1 - a$1) * (c$3 - a$3) * (d$2 - a$2) -
(b$2 - a$2) * (c$1 - a$1) * (d$3 - a$3) -
(b$3 - a$3) * (c$2 - a$2) * (d$1 - a$1)) / &6`,
let STEINHAUS = prove
(`!s:real^N->bool.
measurable s /\ &0 < measure s
==> ?d. &0 < d /\ ball(vec 0,d)
SUBSET {x - y | x
IN s /\ y
IN s}`,
REPEAT STRIP_TAC THEN
MP_TAC(ISPECL [`s:real^N->bool`; `measure(s:real^N->bool) / &3`]
MEASURABLE_INNER_COMPACT) THEN
MP_TAC(ISPECL [`s:real^N->bool`; `measure(s:real^N->bool) / &3`]
MEASURABLE_OUTER_OPEN) THEN
ASM_REWRITE_TAC[REAL_ARITH `&0 < x / &3 <=> &0 < x`] THEN
DISCH_THEN(X_CHOOSE_THEN `u:real^N->bool` STRIP_ASSUME_TAC) THEN
DISCH_THEN(X_CHOOSE_THEN `k:real^N->bool` STRIP_ASSUME_TAC) THEN
MP_TAC(ISPECL [`k:real^N->bool`; `(:real^N)
DIFF u`]
SEPARATE_COMPACT_CLOSED) THEN
ASM_REWRITE_TAC[GSYM
OPEN_CLOSED] THEN
ANTS_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
MATCH_MP_TAC
MONO_EXISTS THEN X_GEN_TAC `d:real` THEN STRIP_TAC THEN
ASM_REWRITE_TAC[] THEN
REWRITE_TAC[
SUBSET;
IN_BALL_0;
IN_ELIM_THM] THEN
X_GEN_TAC `v:real^N` THEN DISCH_TAC THEN
SUBGOAL_THEN `~((
IMAGE (\x:real^N. v + x) k)
INTER k = {})` MP_TAC THENL
[DISCH_TAC THEN
MP_TAC(ISPECL [`
IMAGE (\x:real^N. v + x) k`; `k:real^N->bool`]
MEASURE_UNION) THEN
ASM_REWRITE_TAC[
MEASURABLE_TRANSLATION_EQ;
MEASURE_EMPTY] THEN
REWRITE_TAC[
MEASURE_TRANSLATION;
REAL_SUB_RZERO] THEN
MATCH_MP_TAC(REAL_ARITH
`!s:real^N->bool u:real^N->bool.
measure u < measure s + measure s / &3 /\
measure s < measure k + measure s / &3 /\
measure x <= measure u
==> ~(measure x = measure k + measure k)`) THEN
MAP_EVERY EXISTS_TAC [`s:real^N->bool`; `u:real^N->bool`] THEN
ASM_REWRITE_TAC[] THEN MATCH_MP_TAC
MEASURE_SUBSET THEN
ASM_SIMP_TAC[
MEASURABLE_TRANSLATION_EQ;
MEASURABLE_UNION] THEN
ASM_REWRITE_TAC[
UNION_SUBSET] THEN
CONJ_TAC THENL [ALL_TAC; ASM SET_TAC[]] THEN
REWRITE_TAC[
SUBSET;
FORALL_IN_IMAGE] THEN
X_GEN_TAC `x:real^N` THEN DISCH_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPECL [`x:real^N`; `v + x:real^N`]) THEN
ASM_REWRITE_TAC[
IN_DIFF;
IN_UNIV; NORM_ARITH
`d <= dist(x:real^N,v + x) <=> ~(norm v < d)`];
REWRITE_TAC[
EXTENSION;
IN_INTER;
NOT_IN_EMPTY;
IN_IMAGE] THEN
REWRITE_TAC[VECTOR_ARITH `v:real^N = x - y <=> x = v + y`] THEN
ASM SET_TAC[]]);;
let INTEGRABLE_CCONTINUOUS_EXPLICIT = prove
(`!f:real^M->real^N.
(!a b. f
integrable_on interval[a,b])
==> ?k. negligible k /\
!x e. ~(x
IN k) /\ &0 < e
==> ?d. &0 < d /\
!h. &0 < h /\ h < d
==> norm(inv(content(interval[x,x + h % vec 1])) %
integral (interval[x,x + h % vec 1]) f -
f(x)) < e`,
REPEAT STRIP_TAC THEN REWRITE_TAC[
IN_UNIV] THEN
MAP_EVERY ABBREV_TAC
[`box = \h x. interval[x:real^M,x + h % vec 1]`;
`box2 = \h x. interval[x:real^M - h % vec 1,x + h % vec 1]`;
`i = \h:real x:real^M. inv(content(box h x)) %
integral (box h x) (f:real^M->real^N)`] THEN
SUBGOAL_THEN
`?k. negligible k /\
!x e. ~(x
IN k) /\ &0 < e
==> ?d. &0 < d /\
!h. &0 < h /\ h < d
==> norm(i h x - (f:real^M->real^N) x) < e`
MP_TAC THENL
[ALL_TAC; MAP_EVERY EXPAND_TAC ["i";
let INTEGRABLE_CCONTINUOUS_EXPLICIT_SYMMETRIC = prove
(`!f:real^M->real^N.
(!a b. f
integrable_on interval[a,b])
==> ?k. negligible k /\
!x e. ~(x
IN k) /\ &0 < e
==> ?d. &0 < d /\
!h. &0 < h /\ h < d
==> norm(inv(content(interval[x - h % vec 1,x + h % vec 1])) %
integral (interval[x - h % vec 1,x + h % vec 1]) f -
f(x)) < e`,
REPEAT STRIP_TAC THEN
MAP_EVERY ABBREV_TAC
[`box = \h x. interval[x - h % vec 1:real^M,x + h % vec 1]`;
`i = \h:real x:real^M. inv(content(box h x)) %
integral (box h x) (f:real^M->real^N)`] THEN
SUBGOAL_THEN
`?k. negligible k /\
!x e. ~(x
IN k) /\ &0 < e
==> ?d. &0 < d /\
!h. &0 < h /\ h < d
==> norm(i h x - (f:real^M->real^N) x) < e`
MP_TAC THENL
[ALL_TAC; MAP_EVERY EXPAND_TAC ["i";
let HAS_VECTOR_DERIVATIVE_INDEFINITE_INTEGRAL = prove
(`!f:real^1->real^N a b.
f
integrable_on interval[a,b]
==> ?k. negligible k /\
!x. x
IN interval[a,b]
DIFF k
==> ((\x. integral(interval[a,x]) f)
has_vector_derivative
f(x)) (at x within interval[a,b])`,
SUBGOAL_THEN
`!f:real^1->real^N a b.
f
integrable_on interval[a,b]
==> ?k. negligible k /\
!x e. x
IN interval[a,b]
DIFF k /\ & 0 < e
==> ?d. &0 < d /\
!x'. x'
IN interval[a,b] /\
drop x < drop x' /\ drop x' < drop x + d
==> norm(integral(interval[x,x']) f -
drop(x' - x) % f x) /
norm(x' - x) < e`
ASSUME_TAC THENL
[REPEAT STRIP_TAC THEN MP_TAC(ISPEC
`(\x. if x
IN interval[a,b] then f x else vec 0):real^1->real^N`
INTEGRABLE_CCONTINUOUS_EXPLICIT) THEN
REWRITE_TAC[] THEN ANTS_TAC THENL
[REPEAT GEN_TAC THEN MATCH_MP_TAC
INTEGRABLE_ON_SUBINTERVAL THEN
EXISTS_TAC `(:real^1)` THEN
ASM_REWRITE_TAC[
INTEGRABLE_RESTRICT_UNIV;
SUBSET_UNIV];
ALL_TAC] THEN
MATCH_MP_TAC
MONO_EXISTS THEN X_GEN_TAC `k:real^1->bool` THEN
STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
MAP_EVERY X_GEN_TAC [`x:real^1`; `e:real`] THEN
REWRITE_TAC[
IN_DIFF] THEN STRIP_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPECL [`x:real^1`; `e:real`]) THEN
ASM_REWRITE_TAC[] THEN
MATCH_MP_TAC
MONO_EXISTS THEN X_GEN_TAC `d:real` THEN
STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
X_GEN_TAC `y:real^1` THEN STRIP_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPEC `drop y - drop x`) THEN
ANTS_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
SUBGOAL_THEN `x + (drop y - drop x) % vec 1 = y` SUBST1_TAC THENL
[REWRITE_TAC[GSYM
DROP_EQ;
DROP_ADD;
DROP_CMUL;
DROP_VEC] THEN
REAL_ARITH_TAC;
ALL_TAC] THEN
ASM_SIMP_TAC[
CONTENT_1;
REAL_LT_IMP_LE] THEN
MATCH_MP_TAC(REAL_ARITH `x = y ==> x < e ==> y < e`) THEN
ASM_SIMP_TAC[
REAL_EQ_RDIV_EQ;
NORM_POS_LT;
VECTOR_SUB_EQ;
GSYM
DROP_EQ;
REAL_LT_IMP_NE] THEN
SUBGOAL_THEN `norm(y - x) = abs(drop y - drop x)` SUBST1_TAC THENL
[REWRITE_TAC[
NORM_REAL; GSYM drop;
DROP_SUB]; ALL_TAC] THEN
REWRITE_TAC[ONCE_REWRITE_RULE[REAL_MUL_SYM] (GSYM
NORM_MUL)] THEN
REWRITE_TAC[
VECTOR_SUB_LDISTRIB;
VECTOR_MUL_ASSOC] THEN
ASM_SIMP_TAC[REAL_FIELD `x < y ==> (y - x) * inv(y - x) = &1`] THEN
AP_TERM_TAC THEN REWRITE_TAC[
DROP_SUB;
VECTOR_MUL_LID] THEN
AP_THM_TAC THEN AP_TERM_TAC THEN MATCH_MP_TAC
INTEGRAL_EQ THEN
X_GEN_TAC `z:real^1` THEN REWRITE_TAC[
DIFF_EMPTY] THEN DISCH_TAC THEN
COND_CASES_TAC THEN REWRITE_TAC[] THEN
RULE_ASSUM_TAC(REWRITE_RULE[
IN_INTERVAL_1]) THEN ASM_REAL_ARITH_TAC;
ALL_TAC] THEN
REPEAT STRIP_TAC THEN
FIRST_X_ASSUM(fun th ->
MP_TAC(ISPECL [`f:real^1->real^N`; `a:real^1`; `b:real^1`] th) THEN
MP_TAC(ISPECL [`\x. (f:real^1->real^N) (--x)`; `--b:real^1`;
`--a:real^1`] th)) THEN
ASM_REWRITE_TAC[
INTEGRABLE_REFLECT] THEN
DISCH_THEN(X_CHOOSE_THEN `k2:real^1->bool`
(CONJUNCTS_THEN2 ASSUME_TAC (LABEL_TAC "2"))) THEN
DISCH_THEN(X_CHOOSE_THEN `k1:real^1->bool`
(CONJUNCTS_THEN2 ASSUME_TAC (LABEL_TAC "1"))) THEN
EXISTS_TAC `k1
UNION IMAGE (--) k2:real^1->bool` THEN CONJ_TAC THENL
[MATCH_MP_TAC
NEGLIGIBLE_UNION THEN ASM_REWRITE_TAC[] THEN
MATCH_MP_TAC
NEGLIGIBLE_LINEAR_IMAGE THEN ASM_REWRITE_TAC[linear] THEN
VECTOR_ARITH_TAC;
ALL_TAC] THEN
X_GEN_TAC `x:real^1` THEN REWRITE_TAC[
IN_DIFF;
IN_UNION; DE_MORGAN_THM] THEN
REWRITE_TAC[
IN_IMAGE; VECTOR_ARITH `x:real^1 = --x' <=> --x = x'`] THEN
REWRITE_TAC[
UNWIND_THM1] THEN STRIP_TAC THEN
REWRITE_TAC[
has_vector_derivative;
HAS_DERIVATIVE_WITHIN] THEN CONJ_TAC THENL
[REWRITE_TAC[linear;
DROP_ADD;
DROP_CMUL] THEN VECTOR_ARITH_TAC;
ALL_TAC] THEN
X_GEN_TAC `e:real` THEN DISCH_TAC THEN
REMOVE_THEN "2" (MP_TAC o SPECL [`--x:real^1`; `e:real`]) THEN
REMOVE_THEN "1" (MP_TAC o SPECL [`x:real^1`; `e:real`]) THEN
ASM_REWRITE_TAC[
IN_DIFF;
IN_INTERVAL_REFLECT] THEN
DISCH_THEN(X_CHOOSE_THEN `d1:real`
(CONJUNCTS_THEN2 ASSUME_TAC (LABEL_TAC "1"))) THEN
DISCH_THEN(X_CHOOSE_THEN `d2:real`
(CONJUNCTS_THEN2 ASSUME_TAC (LABEL_TAC "2"))) THEN
EXISTS_TAC `min d1 d2:real` THEN ASM_REWRITE_TAC[
REAL_LT_MIN] THEN
X_GEN_TAC `y:real^1` THEN REWRITE_TAC[
IN_INTERVAL_1] THEN
REWRITE_TAC[
NORM_REAL; GSYM drop;
DROP_SUB] THEN
RULE_ASSUM_TAC(REWRITE_RULE[
IN_INTERVAL_1]) THEN STRIP_TAC THEN
SUBGOAL_THEN `drop x < drop y \/ drop y < drop x` DISJ_CASES_TAC THENL
[ASM_REAL_ARITH_TAC;
REMOVE_THEN "1" (MP_TAC o SPEC `y:real^1`) THEN
ANTS_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
REWRITE_TAC[
NORM_REAL; GSYM drop;
DROP_SUB] THEN
MATCH_MP_TAC(REAL_ARITH `x = y ==> x < e ==> y < e`) THEN
AP_THM_TAC THEN AP_TERM_TAC THEN AP_TERM_TAC THEN
AP_THM_TAC THEN AP_TERM_TAC THEN
MATCH_MP_TAC(VECTOR_ARITH `c + a:real^N = b ==> a = b - c`) THEN
MATCH_MP_TAC
INTEGRAL_COMBINE THEN
REPEAT(CONJ_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC]) THEN
MATCH_MP_TAC
INTEGRABLE_SUBINTERVAL THEN
MAP_EVERY EXISTS_TAC [`a:real^1`; `b:real^1`] THEN
ASM_REWRITE_TAC[
SUBSET_INTERVAL_1] THEN ASM_REAL_ARITH_TAC;
REMOVE_THEN "2" (MP_TAC o SPEC `--y:real^1`) THEN
ANTS_TAC THENL [SIMP_TAC[
DROP_NEG] THEN ASM_REAL_ARITH_TAC; ALL_TAC] THEN
SUBGOAL_THEN `norm(--y - --x) = abs(drop y - drop x)` SUBST1_TAC THENL
[REWRITE_TAC[
NORM_REAL; GSYM drop;
DROP_SUB;
DROP_NEG] THEN
ASM_REAL_ARITH_TAC;
ALL_TAC] THEN
MATCH_MP_TAC(REAL_ARITH `x = y ==> x < e ==> y < e`) THEN
AP_THM_TAC THEN AP_TERM_TAC THEN REWRITE_TAC[
INTEGRAL_REFLECT] THEN
REWRITE_TAC[
VECTOR_NEG_NEG;
DROP_SUB;
DROP_NEG] THEN
ONCE_REWRITE_TAC[VECTOR_ARITH
`x - (--a - --b) % y:real^N = --(--x - (a - b) % y)`] THEN
REWRITE_TAC[
NORM_NEG] THEN AP_TERM_TAC THEN
AP_THM_TAC THEN AP_TERM_TAC THEN
MATCH_MP_TAC(VECTOR_ARITH `b + a = c ==> --a:real^N = b - c`) THEN
MATCH_MP_TAC
INTEGRAL_COMBINE THEN
REPEAT(CONJ_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC]) THEN
MATCH_MP_TAC
INTEGRABLE_SUBINTERVAL THEN
MAP_EVERY EXISTS_TAC [`a:real^1`; `b:real^1`] THEN
ASM_REWRITE_TAC[
SUBSET_INTERVAL_1] THEN ASM_REAL_ARITH_TAC]);;
let ABSOLUTELY_INTEGRABLE_LEBESGUE_POINTS = prove
(`!f:real^M->real^N.
(!a b. f
absolutely_integrable_on interval[a,b])
==> ?k. negligible k /\
!x e. ~(x
IN k) /\ &0 < e
==> ?d. &0 < d /\
!h. &0 < h /\ h < d
==> norm(inv(content(interval[x - h % vec 1,
x + h % vec 1])) %
integral (interval[x - h % vec 1,
x + h % vec 1])
(\t. lift(norm(f t - f x))))
< e`,
let MEASURABLE_ON_COMPOSE_CONTINUOUS_OPEN_INTERVAL = prove
(`!f:real^M->real^N g:real^N->real^P a b.
f
measurable_on (:real^M) /\
(!x. f(x)
IN interval(a,b)) /\
g
continuous_on interval(a,b)
==> (g o f)
measurable_on (:real^M)`,
REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
REWRITE_TAC[
measurable_on;
IN_UNIV] THEN
MATCH_MP_TAC
MONO_EXISTS THEN X_GEN_TAC `k:real^M->bool` THEN
DISCH_THEN(X_CHOOSE_THEN `h:num->real^M->real^N` STRIP_ASSUME_TAC) THEN
EXISTS_TAC
`(\n x. (g:real^N->real^P)
(lambda i. max ((a:real^N)$i + (b$i - a$i) / (&n + &2))
(min ((h n x:real^N)$i)
((b:real^N)$i - (b$i - a$i) / (&n + &2)))))
:num->real^M->real^P` THEN
ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
[X_GEN_TAC `n:num` THEN GEN_REWRITE_TAC LAND_CONV [GSYM
o_DEF] THEN
MATCH_MP_TAC
CONTINUOUS_ON_COMPOSE THEN CONJ_TAC THENL
[MP_TAC(ISPECL
[`(:real^M)`;
`(lambda i. (b:real^N)$i - (b$i - (a:real^N)$i) / (&n + &2)):real^N`]
CONTINUOUS_ON_CONST) THEN
FIRST_X_ASSUM(MP_TAC o SPEC `n:num`) THEN
REWRITE_TAC[IMP_IMP] THEN
DISCH_THEN(MP_TAC o MATCH_MP
CONTINUOUS_ON_MIN) THEN
MP_TAC(ISPECL
[`(:real^M)`;
`(lambda i. (a:real^N)$i + ((b:real^N)$i - a$i) / (&n + &2)):real^N`]
CONTINUOUS_ON_CONST) THEN
REWRITE_TAC[IMP_IMP] THEN
DISCH_THEN(MP_TAC o MATCH_MP
CONTINUOUS_ON_MAX) THEN
MATCH_MP_TAC EQ_IMP THEN AP_THM_TAC THEN AP_TERM_TAC THEN
SIMP_TAC[
FUN_EQ_THM;
CART_EQ;
LAMBDA_BETA];
MATCH_MP_TAC
CONTINUOUS_ON_SUBSET THEN
EXISTS_TAC `interval(a:real^N,b)` THEN
ASM_REWRITE_TAC[
SUBSET;
FORALL_IN_IMAGE;
IN_UNIV] THEN
X_GEN_TAC `x:real^M` THEN
FIRST_X_ASSUM(MP_TAC o SPEC `x:real^M` o CONJUNCT1) THEN
SIMP_TAC[
IN_INTERVAL;
LAMBDA_BETA] THEN
MATCH_MP_TAC
MONO_FORALL THEN X_GEN_TAC `i:num` THEN
MATCH_MP_TAC MONO_IMP THEN REWRITE_TAC[] THEN DISCH_TAC THEN
SUBGOAL_THEN
`&0 < ((b:real^N)$i - (a:real^N)$i) / (&n + &2) /\
((b:real^N)$i - (a:real^N)$i) / (&n + &2) <= (b$i - a$i) / &2` MP_TAC
THENL [ALL_TAC; REAL_ARITH_TAC] THEN
ASM_SIMP_TAC[
REAL_LT_RDIV_EQ;
REAL_LT_LDIV_EQ;
REAL_ARITH `&0 < &n + &2`] THEN
CONJ_TAC THENL [ASM_REAL_ARITH_TAC; REWRITE_TAC[
real_div]] THEN
MATCH_MP_TAC
REAL_LE_LMUL THEN CONJ_TAC THENL
[ASM_REAL_ARITH_TAC;
MATCH_MP_TAC
REAL_LE_INV2 THEN REAL_ARITH_TAC]];
X_GEN_TAC `x:real^M` THEN DISCH_TAC THEN
REWRITE_TAC[
o_DEF] THEN MATCH_MP_TAC
LIM_CONTINUOUS_FUNCTION THEN
CONJ_TAC THENL
[ASM_MESON_TAC[
CONTINUOUS_ON_EQ_CONTINUOUS_AT;
OPEN_INTERVAL];
ALL_TAC] THEN
SUBGOAL_THEN
`((\n. (lambda i. ((a:real^N)$i + ((b:real^N)$i - a$i) / (&n + &2))))
--> a) sequentially /\
((\n. (lambda i. ((b:real^N)$i - ((b:real^N)$i - a$i) / (&n + &2))))
--> b) sequentially`
MP_TAC THENL
[ONCE_REWRITE_TAC[
LIM_COMPONENTWISE_LIFT] THEN
SIMP_TAC[
LAMBDA_BETA] THEN
CONJ_TAC THEN X_GEN_TAC `j:num` THEN STRIP_TAC THEN
REWRITE_TAC[
real_sub] THEN
GEN_REWRITE_TAC LAND_CONV [GSYM
VECTOR_ADD_RID] THEN
REWRITE_TAC[
LIFT_ADD] THEN MATCH_MP_TAC
LIM_ADD THEN
REWRITE_TAC[
LIM_CONST;
LIFT_NEG;
real_div;
LIFT_CMUL] THEN
GEN_REWRITE_TAC LAND_CONV [GSYM
VECTOR_NEG_0] THEN
TRY(MATCH_MP_TAC
LIM_NEG) THEN REWRITE_TAC[
VECTOR_NEG_0] THEN
SUBST1_TAC(VECTOR_ARITH
`vec 0:real^1 = ((b:real^N)$j + --((a:real^N)$j)) % vec 0`) THEN
MATCH_MP_TAC
LIM_CMUL THEN
REWRITE_TAC[
LIM_SEQUENTIALLY;
DIST_0;
NORM_LIFT] THEN
X_GEN_TAC `e:real` THEN
GEN_REWRITE_TAC LAND_CONV [
REAL_ARCH_INV] THEN
MATCH_MP_TAC
MONO_EXISTS THEN X_GEN_TAC `N:num` THEN STRIP_TAC THEN
X_GEN_TAC `m:num` THEN DISCH_TAC THEN REWRITE_TAC[
REAL_ABS_INV] THEN
MATCH_MP_TAC
REAL_LET_TRANS THEN EXISTS_TAC `inv(&N)` THEN
ASM_REWRITE_TAC[] THEN MATCH_MP_TAC
REAL_LE_INV2 THEN
ASM_SIMP_TAC[REAL_OF_NUM_ADD;
REAL_OF_NUM_LT;
LE_1;
REAL_OF_NUM_LE;
REAL_ABS_NUM] THEN
ASM_ARITH_TAC;
ALL_TAC] THEN
FIRST_X_ASSUM(MP_TAC o SPEC `x:real^M`) THEN
ASM_REWRITE_TAC[TAUT `a ==> b /\ c ==> d <=> a /\ c ==> b ==> d`] THEN
DISCH_THEN(MP_TAC o MATCH_MP
LIM_MIN) THEN
REWRITE_TAC[GSYM
IMP_CONJ_ALT] THEN
DISCH_THEN(MP_TAC o MATCH_MP
LIM_MAX) THEN
MATCH_MP_TAC EQ_IMP THEN AP_THM_TAC THEN BINOP_TAC THEN
SIMP_TAC[
CART_EQ;
LAMBDA_BETA;
FUN_EQ_THM] THEN
RULE_ASSUM_TAC(REWRITE_RULE[
IN_INTERVAL]) THEN
ASM_MESON_TAC[REAL_ARITH `a < x /\ x < b ==> max a (min x b) = x`]]);;
let MEASURABLE_ON_PASTECART = prove
(`!f:real^M->real^N g:real^M->real^P s.
f
measurable_on s /\ g
measurable_on s
==> (\x. pastecart (f x) (g x))
measurable_on s`,
REPEAT GEN_TAC THEN REWRITE_TAC[
measurable_on] THEN
DISCH_THEN(CONJUNCTS_THEN2
(X_CHOOSE_THEN `k1:real^M->bool` MP_TAC)
(X_CHOOSE_THEN `k2:real^M->bool` MP_TAC)) THEN
DISCH_THEN(X_CHOOSE_THEN `g2:num->real^M->real^P` STRIP_ASSUME_TAC) THEN
DISCH_THEN(X_CHOOSE_THEN `g1:num->real^M->real^N` STRIP_ASSUME_TAC) THEN
EXISTS_TAC `k1
UNION k2:real^M->bool` THEN
ASM_SIMP_TAC[
NEGLIGIBLE_UNION] THEN
EXISTS_TAC `(\n x. pastecart (g1 n x) (g2 n x))
:num->real^M->real^(N,P)finite_sum` THEN
ASM_SIMP_TAC[
CONTINUOUS_ON_PASTECART; ETA_AX;
IN_UNION; DE_MORGAN_THM] THEN
X_GEN_TAC `x:real^M` THEN STRIP_TAC THEN
REPEAT(FIRST_X_ASSUM(MP_TAC o SPEC `x:real^M`)) THEN
ASM_CASES_TAC `(x:real^M)
IN s` THEN
REWRITE_TAC[GSYM
PASTECART_VEC] THEN ASM_SIMP_TAC[
LIM_PASTECART]);;
let NEGLIGIBLE_LOCALLY_LIPSCHITZ_IMAGE = prove
(`!f:real^M->real^N s.
dimindex(:M) <= dimindex(:N) /\ negligible s /\
(!x. x
IN s
==> ?t b. open t /\ x
IN t /\
!y. y
IN s
INTER t
==> norm(f y - f x) <= b * norm(y - x))
==> negligible(
IMAGE f s)`,
let lemma = prove
(`!f:real^M->real^N s B.
dimindex(:M) <= dimindex(:N) /\ bounded s /\ negligible s /\ &0 < B /\
(!x. x IN s
==> ?t. open t /\ x IN t /\
!y. y IN s INTER t
==> norm(f y - f x) <= B * norm(y - x))
==> negligible(IMAGE f s)`,
REPEAT STRIP_TAC THEN REWRITE_TAC[NEGLIGIBLE_OUTER] THEN
X_GEN_TAC `e:real` THEN DISCH_TAC THEN
MP_TAC(ISPECL [`s:real^M->bool`;
`e / &2 / (&2 * B * &(dimindex(:M))) pow (dimindex(:N))`]
MEASURABLE_OUTER_OPEN) THEN
ANTS_TAC THENL
[ASM_SIMP_TAC[NEGLIGIBLE_IMP_MEASURABLE] THEN
MATCH_MP_TAC REAL_LT_DIV THEN ASM_REWRITE_TAC[REAL_HALF] THEN
MATCH_MP_TAC REAL_POW_LT THEN
REPEAT(MATCH_MP_TAC REAL_LT_MUL THEN CONJ_TAC) THEN
ASM_SIMP_TAC[DIMINDEX_GE_1; REAL_OF_NUM_LT; ARITH; LE_1];
ALL_TAC] THEN
ASM_SIMP_TAC[NEGLIGIBLE_IMP_MEASURABLE; REAL_HALF; MEASURE_EQ_0] THEN
REWRITE_TAC[REAL_ADD_LID] THEN
DISCH_THEN(X_CHOOSE_THEN `t:real^M->bool` STRIP_ASSUME_TAC) THEN
SUBGOAL_THEN
`!x. ?r. &0 < r /\ r <= &1 / &2 /\
(x IN s
==> !y. norm(y - x:real^M) < r
==> y IN t /\
(y IN s
==> norm(f y - f x:real^N) <= B * norm(y - x)))`
MP_TAC THENL
[X_GEN_TAC `x:real^M` THEN ASM_CASES_TAC `(x:real^M) IN s` THEN
ASM_REWRITE_TAC[] THENL
[ALL_TAC; EXISTS_TAC `&1 / &4` THEN REAL_ARITH_TAC] THEN
FIRST_X_ASSUM(MP_TAC o SPEC `x:real^M`) THEN
ASM_REWRITE_TAC[IN_INTER] THEN
DISCH_THEN(X_CHOOSE_THEN `u:real^M->bool` STRIP_ASSUME_TAC) THEN
MP_TAC(ISPEC `t INTER u :real^M->bool` open_def) THEN
ASM_SIMP_TAC[OPEN_INTER; OPEN_BALL] THEN
DISCH_THEN(MP_TAC o SPEC `x:real^M`) THEN
ANTS_TAC THENL [ASM SET_TAC[]; REWRITE_TAC[IN_INTER; dist]] THEN
DISCH_THEN(X_CHOOSE_THEN `r:real` STRIP_ASSUME_TAC) THEN
EXISTS_TAC `min (&1 / &2) r` THEN
ASM_REWRITE_TAC[REAL_MIN_LE; REAL_LT_MIN] THEN
CONV_TAC REAL_RAT_REDUCE_CONV THEN ASM_MESON_TAC[];
FIRST_X_ASSUM(K ALL_TAC o check (is_forall o concl)) THEN
REWRITE_TAC[SKOLEM_THM; LEFT_IMP_EXISTS_THM; FORALL_AND_THM] THEN
REWRITE_TAC[RIGHT_IMP_FORALL_THM; IMP_IMP] THEN
X_GEN_TAC `r:real^M->real` THEN STRIP_TAC] THEN
SUBGOAL_THEN
`?c. s SUBSET interval[--(vec c):real^M,vec c] /\
~(interval(--(vec c):real^M,vec c) = {})`
STRIP_ASSUME_TAC THENL
[FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [bounded]) THEN
DISCH_THEN(X_CHOOSE_THEN `c:real` STRIP_ASSUME_TAC) THEN
MP_TAC(SPEC `abs c + &1` REAL_ARCH_SIMPLE) THEN
MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `n:num` THEN
DISCH_TAC THEN REWRITE_TAC[SUBSET; INTERVAL_NE_EMPTY] THEN
REWRITE_TAC[IN_INTERVAL; VEC_COMPONENT; VECTOR_NEG_COMPONENT] THEN
CONJ_TAC THENL [ALL_TAC; ASM_REAL_ARITH_TAC] THEN
X_GEN_TAC `x:real^M` THEN DISCH_TAC THEN X_GEN_TAC `i:num` THEN
STRIP_TAC THEN REWRITE_TAC[REAL_BOUNDS_LE] THEN W(MP_TAC o
PART_MATCH (lhand o rand) COMPONENT_LE_NORM o lhand o snd) THEN
REPEAT(FIRST_X_ASSUM(MP_TAC o SPEC `x:real^M`)) THEN
ASM_REWRITE_TAC[] THEN ASM_REAL_ARITH_TAC;
ALL_TAC] THEN
MP_TAC(ISPECL [`--(vec c):real^M`; `(vec c):real^M`; `s:real^M->bool`;
`\x:real^M. ball(x,r x)`] COVERING_LEMMA) THEN
ASM_REWRITE_TAC[gauge; OPEN_BALL; CENTRE_IN_BALL] THEN
REWRITE_TAC[VEC_COMPONENT; VECTOR_NEG_COMPONENT] THEN
DISCH_THEN(X_CHOOSE_THEN `D:(real^M->bool)->bool` STRIP_ASSUME_TAC) THEN
SUBGOAL_THEN
`!k. k IN D
==> ?u v z. k = interval[u,v] /\ ~(interval(u,v) = {}) /\
z IN s /\ z IN interval[u,v] /\
interval[u:real^M,v] SUBSET ball(z,r z)`
MP_TAC THENL
[X_GEN_TAC `d:real^M->bool` THEN DISCH_TAC THEN
SUBGOAL_THEN `?u v:real^M. d = interval[u,v]` MP_TAC THENL
[ASM_MESON_TAC[]; ALL_TAC] THEN
MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `u:real^M` THEN
MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `v:real^M` THEN
DISCH_THEN SUBST_ALL_TAC THEN
ASM_MESON_TAC[SUBSET; INTERIOR_CLOSED_INTERVAL; IN_INTER];
ALL_TAC] THEN
GEN_REWRITE_TAC (LAND_CONV o TOP_DEPTH_CONV) [RIGHT_IMP_EXISTS_THM] THEN
REWRITE_TAC[SKOLEM_THM; LEFT_IMP_EXISTS_THM] THEN MAP_EVERY X_GEN_TAC
[`u:(real^M->bool)->real^M`; `v:(real^M->bool)->real^M`;
`z:(real^M->bool)->real^M`] THEN
DISCH_THEN(LABEL_TAC "*") THEN EXISTS_TAC
`UNIONS(IMAGE (\d:real^M->bool.
interval[(f:real^M->real^N)(z d) -
(B * &(dimindex(:M)) *
((v(d):real^M)$1 - (u(d):real^M)$1)) % vec 1:real^N,
f(z d) +
(B * &(dimindex(:M)) * (v(d)$1 - u(d)$1)) % vec 1]) D)` THEN
CONJ_TAC THENL
[REWRITE_TAC[SUBSET; FORALL_IN_IMAGE] THEN
X_GEN_TAC `y:real^M` THEN DISCH_TAC THEN
SUBGOAL_THEN `(y:real^M) IN UNIONS D` MP_TAC THENL
[ASM_MESON_TAC[SUBSET]; REWRITE_TAC[UNIONS_IMAGE]] THEN
REWRITE_TAC[IN_UNIONS; IN_ELIM_THM] THEN MATCH_MP_TAC MONO_EXISTS THEN
X_GEN_TAC `d:real^M->bool` THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
SUBGOAL_THEN `(y:real^M) IN ball(z(d:real^M->bool),r(z d))` MP_TAC THENL
[ASM_MESON_TAC[SUBSET]; REWRITE_TAC[IN_BALL; dist]] THEN
ONCE_REWRITE_TAC[NORM_SUB] THEN DISCH_TAC THEN
SUBGOAL_THEN
`y IN t /\
norm((f:real^M->real^N) y - f(z d)) <= B * norm(y - z(d:real^M->bool))`
STRIP_ASSUME_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
REWRITE_TAC[IN_INTERVAL] THEN X_GEN_TAC `i:num` THEN STRIP_TAC THEN
REWRITE_TAC[VECTOR_ADD_COMPONENT; VECTOR_SUB_COMPONENT] THEN
REWRITE_TAC[REAL_ARITH
`z - b <= y /\ y <= z + b <=> abs(y - z) <= b`] THEN
REWRITE_TAC[GSYM VECTOR_SUB_COMPONENT] THEN W(MP_TAC o
PART_MATCH (lhand o rand) COMPONENT_LE_NORM o lhand o snd) THEN
ASM_REWRITE_TAC[] THEN
MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ_ALT] REAL_LE_TRANS) THEN
REWRITE_TAC[VECTOR_MUL_COMPONENT; VEC_COMPONENT; REAL_MUL_RID] THEN
FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REWRITE_RULE[IMP_CONJ]
REAL_LE_TRANS)) THEN
ASM_SIMP_TAC[REAL_LE_LMUL_EQ] THEN
W(MP_TAC o PART_MATCH lhand NORM_LE_L1 o lhand o snd) THEN
MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ_ALT] REAL_LE_TRANS) THEN
GEN_REWRITE_TAC (RAND_CONV o LAND_CONV o RAND_CONV)
[GSYM CARD_NUMSEG_1] THEN
SIMP_TAC[GSYM SUM_CONST; FINITE_NUMSEG] THEN
MATCH_MP_TAC SUM_LE_NUMSEG THEN X_GEN_TAC `j:num` THEN STRIP_TAC THEN
MATCH_MP_TAC REAL_LE_TRANS THEN
EXISTS_TAC `((v:(real^M->bool)->real^M) d - u d)$j` THEN
REWRITE_TAC[VECTOR_SUB_COMPONENT] THEN CONJ_TAC THENL
[SUBGOAL_THEN `y IN interval[(u:(real^M->bool)->real^M) d,v d] /\
(z d) IN interval[u d,v d]`
MP_TAC THENL [ASM_MESON_TAC[]; REWRITE_TAC[IN_INTERVAL]] THEN
DISCH_THEN(CONJUNCTS_THEN (MP_TAC o SPEC `j:num`)) THEN
ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC;
MATCH_MP_TAC REAL_EQ_IMP_LE THEN FIRST_X_ASSUM(MP_TAC o SPECL
[`(u:(real^M->bool)->real^M) d`; `(v:(real^M->bool)->real^M) d`]) THEN
ASM_MESON_TAC[DIMINDEX_GE_1; LE_REFL]];
ALL_TAC] THEN
MATCH_MP_TAC(MESON[]
`(x <= e / &2 ==> x < e) /\ P /\ x <= e / &2 ==> P /\ x < e`) THEN
CONJ_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
MATCH_MP_TAC MEASURE_COUNTABLE_UNIONS_LE_GEN THEN
ASM_SIMP_TAC[COUNTABLE_IMAGE; FORALL_IN_IMAGE; MEASURABLE_INTERVAL] THEN
ONCE_REWRITE_TAC[CONJ_SYM] THEN
REWRITE_TAC[FORALL_FINITE_SUBSET_IMAGE] THEN
X_GEN_TAC `D':(real^M->bool)->bool` THEN STRIP_TAC THEN
W(MP_TAC o PART_MATCH (lhand o rand) SUM_IMAGE_LE o lhand o snd) THEN
ASM_SIMP_TAC[MEASURE_POS_LE; MEASURABLE_INTERVAL] THEN
MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ_ALT] REAL_LE_TRANS) THEN
REWRITE_TAC[o_DEF] THEN
MATCH_MP_TAC REAL_LE_TRANS THEN
EXISTS_TAC `(&2 * B * &(dimindex(:M))) pow (dimindex(:N)) *
sum D' (\d:real^M->bool. measure d)` THEN
SUBGOAL_THEN `FINITE(D':(real^M->bool)->bool)` ASSUME_TAC THENL
[ASM_MESON_TAC[FINITE_SUBSET]; ALL_TAC] THEN
CONJ_TAC THENL
[REWRITE_TAC[GSYM SUM_LMUL] THEN MATCH_MP_TAC SUM_LE THEN
ASM_REWRITE_TAC[MEASURE_INTERVAL] THEN X_GEN_TAC `d:real^M->bool` THEN
DISCH_TAC THEN REWRITE_TAC[CONTENT_CLOSED_INTERVAL_CASES] THEN
REWRITE_TAC[VECTOR_ADD_COMPONENT; VECTOR_SUB_COMPONENT; REAL_ARITH
`(a - x <= a + x <=> &0 <= x) /\ (a + x) - (a - x) = &2 * x`] THEN
REWRITE_TAC[VECTOR_MUL_COMPONENT; VEC_COMPONENT; REAL_MUL_RID] THEN
ASM_SIMP_TAC[REAL_LE_MUL_EQ; REAL_OF_NUM_LT; LE_1; DIMINDEX_GE_1] THEN
SUBGOAL_THEN `d = interval[u d:real^M,v d]`
(fun th -> GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [th])
THENL [ASM_MESON_TAC[SUBSET]; ALL_TAC] THEN
REWRITE_TAC[MEASURE_INTERVAL; CONTENT_CLOSED_INTERVAL_CASES] THEN
SUBGOAL_THEN
`!i. 1 <= i /\ i <= dimindex(:M)
==> ((u:(real^M->bool)->real^M) d)$i <= (v d:real^M)$i`
MP_TAC THENL
[ASM_MESON_TAC[SUBSET; INTERVAL_NE_EMPTY; REAL_LT_IMP_LE]; ALL_TAC] THEN
SIMP_TAC[REAL_SUB_LE; DIMINDEX_GE_1; LE_REFL] THEN DISCH_TAC THEN
REWRITE_TAC[PRODUCT_CONST_NUMSEG; REAL_POW_MUL] THEN
ASM_SIMP_TAC[REAL_LE_LMUL_EQ; REAL_POW_LT; REAL_OF_NUM_LT; ARITH;
GSYM REAL_MUL_ASSOC; ADD_SUB; DIMINDEX_GE_1; LE_1] THEN
MATCH_MP_TAC REAL_LE_TRANS THEN
EXISTS_TAC `((v d:real^M)$1 - ((u:(real^M->bool)->real^M) d)$1)
pow (dimindex(:M))` THEN
CONJ_TAC THENL
[MATCH_MP_TAC REAL_POW_MONO_INV THEN
ASM_SIMP_TAC[REAL_SUB_LE; DIMINDEX_GE_1; LE_REFL] THEN
REWRITE_TAC[GSYM VECTOR_SUB_COMPONENT] THEN
MATCH_MP_TAC(REAL_ARITH `abs x <= a ==> x <= a`) THEN W(MP_TAC o
PART_MATCH (lhand o rand) COMPONENT_LE_NORM o lhand o snd) THEN
REWRITE_TAC[DIMINDEX_GE_1; LE_REFL] THEN
MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ_ALT] REAL_LE_TRANS) THEN
MATCH_MP_TAC(NORM_ARITH
`!z r. norm(z - u) < r /\ norm(z - v) < r /\ r <= &1 / &2
==> norm(v - u:real^M) <= &1`) THEN
MAP_EVERY EXISTS_TAC
[`(z:(real^M->bool)->real^M) d`;
`r((z:(real^M->bool)->real^M) d):real`] THEN
ASM_REWRITE_TAC[GSYM dist; GSYM IN_BALL] THEN
SUBGOAL_THEN
`(u:(real^M->bool)->real^M) d IN interval[u d,v d] /\
(v:(real^M->bool)->real^M) d IN interval[u d,v d]`
MP_TAC THENL [ALL_TAC; ASM_MESON_TAC[SUBSET]] THEN
ASM_REWRITE_TAC[ENDS_IN_INTERVAL; INTERVAL_NE_EMPTY];
GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [GSYM CARD_NUMSEG_1] THEN
SIMP_TAC[GSYM PRODUCT_CONST; FINITE_NUMSEG] THEN
MATCH_MP_TAC REAL_EQ_IMP_LE THEN MATCH_MP_TAC PRODUCT_EQ_NUMSEG THEN
FIRST_X_ASSUM(MP_TAC o SPECL
[`(u:(real^M->bool)->real^M) d`; `(v:(real^M->bool)->real^M) d`]) THEN
ASM_MESON_TAC[DIMINDEX_GE_1; LE_REFL; SUBSET]];
MATCH_MP_TAC REAL_LE_TRANS THEN
EXISTS_TAC `(&2 * B * &(dimindex(:M))) pow dimindex(:N) *
measure(t:real^M->bool)` THEN
CONJ_TAC THENL
[MATCH_MP_TAC REAL_LE_LMUL THEN
CONJ_TAC THENL [MATCH_MP_TAC REAL_LT_IMP_LE; ALL_TAC];
MATCH_MP_TAC REAL_LT_IMP_LE THEN ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
W(MP_TAC o PART_MATCH (rand o rand) REAL_LT_RDIV_EQ o snd)] THEN
ASM_SIMP_TAC[REAL_POW_LT; REAL_LT_MUL; LE_1; DIMINDEX_GE_1;
REAL_ARITH `&0 < &2 * B <=> &0 < B`; REAL_OF_NUM_LT] THEN
MATCH_MP_TAC REAL_LE_TRANS THEN
EXISTS_TAC `measure(UNIONS D':real^M->bool)` THEN CONJ_TAC THENL
[MP_TAC(ISPECL [`D':(real^M->bool)->bool`; `UNIONS D':real^M->bool`]
MEASURE_ELEMENTARY) THEN
ANTS_TAC THENL
[ASM_REWRITE_TAC[division_of] THEN
CONJ_TAC THENL [ALL_TAC; ASM_MESON_TAC[SUBSET]] THEN
GEN_TAC THEN DISCH_TAC THEN CONJ_TAC THENL
[ASM SET_TAC[]; ASM_MESON_TAC[SUBSET; INTERIOR_EMPTY]];
DISCH_THEN SUBST1_TAC THEN MATCH_MP_TAC REAL_EQ_IMP_LE THEN
MATCH_MP_TAC SUM_EQ THEN ASM_MESON_TAC[MEASURE_INTERVAL; SUBSET]];
MATCH_MP_TAC MEASURE_SUBSET THEN CONJ_TAC THENL
[MATCH_MP_TAC MEASURABLE_UNIONS THEN
ASM_MESON_TAC[MEASURABLE_INTERVAL; SUBSET];
ASM_REWRITE_TAC[] THEN MATCH_MP_TAC SUBSET_TRANS THEN
EXISTS_TAC `UNIONS D:real^M->bool` THEN
ASM_SIMP_TAC[SUBSET_UNIONS] THEN
REWRITE_TAC[SUBSET; FORALL_IN_UNIONS] THEN
X_GEN_TAC `d:real^M->bool` THEN
REWRITE_TAC[RIGHT_FORALL_IMP_THM; IMP_CONJ] THEN
DISCH_TAC THEN REWRITE_TAC[GSYM SUBSET] THEN
SUBGOAL_THEN `d SUBSET ball(z d:real^M,r(z d))` MP_TAC THENL
[ASM_MESON_TAC[];
REWRITE_TAC[SUBSET; IN_BALL; dist] THEN
ASM_MESON_TAC[NORM_SUB]]]]]) in
REPEAT STRIP_TAC THEN
SUBGOAL_THEN
`s = UNIONS
{{x | x IN s /\ norm(x:real^M) <= &n /\
?t. open t /\ x IN t /\
!y. y IN s INTER t
==> norm(f y - f x:real^N) <= (&n + &1) * norm(y - x)} |
n IN (:num)}`
SUBST1_TAC THENL
[REWRITE_TAC[EXTENSION; UNIONS_GSPEC; IN_ELIM_THM; IN_UNIV] THEN
X_GEN_TAC `x:real^M` THEN
ASM_CASES_TAC `(x:real^M) IN s` THEN ASM_REWRITE_TAC[] THEN
FIRST_X_ASSUM(MP_TAC o SPEC `x:real^M`) THEN ASM_REWRITE_TAC[] THEN
ONCE_REWRITE_TAC[SWAP_EXISTS_THM] THEN
REWRITE_TAC[RIGHT_AND_EXISTS_THM] THEN
ONCE_REWRITE_TAC[SWAP_EXISTS_THM] THEN MATCH_MP_TAC MONO_EXISTS THEN
X_GEN_TAC `t:real^M->bool` THEN
DISCH_THEN(X_CHOOSE_THEN `b:real` STRIP_ASSUME_TAC) THEN
MP_TAC(SPEC `max (norm(x:real^M)) b` REAL_ARCH_SIMPLE) THEN
MATCH_MP_TAC MONO_EXISTS THEN REWRITE_TAC[REAL_MAX_LE] THEN
X_GEN_TAC `n:num` THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
MATCH_MP_TAC REAL_LE_TRANS THEN
EXISTS_TAC `b * norm(y - x:real^M)` THEN ASM_SIMP_TAC[] THEN
MATCH_MP_TAC REAL_LE_RMUL THEN REWRITE_TAC[NORM_POS_LE] THEN
ASM_REAL_ARITH_TAC;
REWRITE_TAC[IMAGE_UNIONS] THEN
MATCH_MP_TAC NEGLIGIBLE_COUNTABLE_UNIONS_GEN THEN
REWRITE_TAC[FORALL_IN_IMAGE; FORALL_IN_GSPEC] THEN
ONCE_REWRITE_TAC[SIMPLE_IMAGE] THEN
ASM_SIMP_TAC[GSYM IMAGE_o; COUNTABLE_IMAGE; NUM_COUNTABLE] THEN
X_GEN_TAC `n:num` THEN REWRITE_TAC[IN_UNIV] THEN
MATCH_MP_TAC lemma THEN EXISTS_TAC `&n + &1` THEN ASM_REWRITE_TAC[] THEN
REPEAT CONJ_TAC THENL
[MATCH_MP_TAC BOUNDED_SUBSET THEN
EXISTS_TAC `cball(vec 0:real^M,&n)` THEN
SIMP_TAC[BOUNDED_CBALL; SUBSET; IN_CBALL_0; IN_ELIM_THM];
MATCH_MP_TAC NEGLIGIBLE_SUBSET THEN EXISTS_TAC `s:real^M->bool` THEN
ASM_REWRITE_TAC[] THEN SET_TAC[];
REAL_ARITH_TAC;
REWRITE_TAC[IN_ELIM_THM; IN_INTER] THEN MESON_TAC[]]]);;
let BABY_SARD = prove
(`!f:real^M->real^N f' s.
dimindex(:M) <= dimindex(:N) /\
(!x. x
IN s
==> (f
has_derivative f' x) (at x within s) /\
rank(matrix(f' x)) < dimindex(:N))
==> negligible(
IMAGE f s)`,
let lemma = prove
(`!p w e m.
dim p < dimindex(:N) /\ &0 <= m /\ &0 <= e
==> ?s. measurable s /\
{z:real^N | norm(z - w) <= m /\
?t. t IN p /\ norm(z - w - t) <= e}
SUBSET s /\
measure s <= (&2 * e) * (&2 * m) pow (dimindex(:N) - 1)`,
REPEAT GEN_TAC THEN GEN_GEOM_ORIGIN_TAC `w:real^N` ["t";
let semma = prove
(`!f:real^M->real^N f' s B.
dimindex(:M) <= dimindex(:N) /\ &0 < B /\ bounded s /\
(!x. x
IN s ==> (f
has_derivative f' x) (at x within s) /\
rank(matrix(f' x)) < dimindex(:N) /\ onorm(f' x) <= B)
==> negligible(
IMAGE f s)`,
REWRITE_TAC[TAUT `p ==> q /\ r <=> (p ==> q) /\ (p ==> r)`] THEN
REWRITE_TAC[
FORALL_AND_THM] THEN REPEAT STRIP_TAC THEN
SUBGOAL_THEN `!x. x
IN s ==> linear((f':real^M->real^M->real^N) x)`
ASSUME_TAC THENL [ASM_MESON_TAC[
has_derivative]; ALL_TAC] THEN
REPEAT STRIP_TAC THEN REWRITE_TAC[
NEGLIGIBLE_OUTER_LE] THEN
X_GEN_TAC `e:real` THEN DISCH_TAC THEN
SUBGOAL_THEN
`?c. s
SUBSET interval(--(vec c):real^M,vec c) /\
~(interval(--(vec c):real^M,vec c) = {})`
STRIP_ASSUME_TAC THENL
[FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [bounded]) THEN
DISCH_THEN(X_CHOOSE_THEN `c:real` STRIP_ASSUME_TAC) THEN
MP_TAC(SPEC `abs c + &1`
REAL_ARCH_SIMPLE) THEN
MATCH_MP_TAC
MONO_EXISTS THEN X_GEN_TAC `n:num` THEN
DISCH_TAC THEN REWRITE_TAC[
SUBSET;
INTERVAL_NE_EMPTY] THEN
REWRITE_TAC[
IN_INTERVAL;
VEC_COMPONENT;
VECTOR_NEG_COMPONENT] THEN
CONJ_TAC THENL [ALL_TAC; ASM_REAL_ARITH_TAC] THEN
X_GEN_TAC `x:real^M` THEN DISCH_TAC THEN X_GEN_TAC `i:num` THEN
STRIP_TAC THEN REWRITE_TAC[
REAL_BOUNDS_LT] THEN W(MP_TAC o
PART_MATCH (lhand o rand)
COMPONENT_LE_NORM o lhand o snd) THEN
REPEAT(FIRST_X_ASSUM(MP_TAC o SPEC `x:real^M`)) THEN
ASM_REWRITE_TAC[] THEN ASM_REAL_ARITH_TAC;
ALL_TAC] THEN
FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [
INTERVAL_NE_EMPTY]) THEN
DISCH_THEN(MP_TAC o SPEC `1`) THEN
REWRITE_TAC[
VEC_COMPONENT;
DIMINDEX_GE_1;
LE_REFL;
VECTOR_NEG_COMPONENT] THEN
REWRITE_TAC[REAL_ARITH `--x < x <=> &0 < &2 * x`; REAL_OF_NUM_MUL] THEN
DISCH_TAC THEN
SUBGOAL_THEN
`?d. &0 < d /\ d <= B /\
(d * &2) * (&4 * B) pow (dimindex(:N) - 1) <=
e / &(2 * c) pow dimindex(:M) / &(dimindex(:M)) pow dimindex(:M)`
STRIP_ASSUME_TAC THENL
[EXISTS_TAC
`min B (e / &(2 * c) pow dimindex(:M) /
&(dimindex(:M)) pow dimindex(:M) /
(&4 * B) pow (dimindex(:N) - 1) / &2)` THEN
ASM_REWRITE_TAC[
REAL_LT_MIN; REAL_ARITH `min x y <= x`] THEN
CONJ_TAC THENL
[REPEAT(MATCH_MP_TAC
REAL_LT_DIV THEN CONJ_TAC) THEN
ASM_SIMP_TAC[
REAL_POW_LT;
REAL_OF_NUM_LT;
DIMINDEX_GE_1;
LE_1;
REAL_ARITH `&0 < &4 * B <=> &0 < B`; ARITH];
ASM_SIMP_TAC[GSYM
REAL_LE_RDIV_EQ;
REAL_POW_LT;
REAL_ARITH `&0 < &4 * B <=> &0 < B`; ARITH] THEN
REAL_ARITH_TAC];
ALL_TAC] THEN
SUBGOAL_THEN
`!x. ?r. &0 < r /\ r <= &1 / &2 /\
(x
IN s
==> !y. y
IN s /\ norm(y - x) < r
==> norm((f:real^M->real^N) y - f x - f' x (y - x)) <=
d * norm(y - x))`
MP_TAC THENL
[X_GEN_TAC `x:real^M` THEN ASM_CASES_TAC `(x:real^M)
IN s` THEN
ASM_REWRITE_TAC[] THENL
[ALL_TAC; EXISTS_TAC `&1 / &4` THEN REAL_ARITH_TAC] THEN
UNDISCH_THEN
`!x. x
IN s ==> ((f:real^M->real^N)
has_derivative f' x) (at x within s)`
(MP_TAC o REWRITE_RULE[
HAS_DERIVATIVE_WITHIN_ALT]) THEN
ASM_SIMP_TAC[
RIGHT_IMP_FORALL_THM] THEN
DISCH_THEN(MP_TAC o SPECL [`x:real^M`; `d:real`]) THEN
ASM_REWRITE_TAC[] THEN
DISCH_THEN(X_CHOOSE_THEN `r:real` STRIP_ASSUME_TAC) THEN
EXISTS_TAC `min r (&1 / &2)` THEN
ASM_REWRITE_TAC[
REAL_LT_MIN;
REAL_MIN_LE;
REAL_LE_REFL] THEN
CONV_TAC REAL_RAT_REDUCE_CONV THEN ASM_MESON_TAC[];
REWRITE_TAC[
SKOLEM_THM;
LEFT_IMP_EXISTS_THM;
FORALL_AND_THM] THEN
X_GEN_TAC `r:real^M->real` THEN REWRITE_TAC[
RIGHT_IMP_FORALL_THM] THEN
REWRITE_TAC[IMP_IMP; GSYM
CONJ_ASSOC] THEN
REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
DISCH_THEN(LABEL_TAC "*")] THEN
MP_TAC(ISPECL [`--(vec c):real^M`; `(vec c):real^M`; `s:real^M->bool`;
`\x:real^M. ball(x,r x)`]
COVERING_LEMMA) THEN
ASM_REWRITE_TAC[gauge;
OPEN_BALL;
CENTRE_IN_BALL] THEN ANTS_TAC THENL
[ASM_MESON_TAC[
SUBSET_TRANS;
INTERVAL_OPEN_SUBSET_CLOSED]; ALL_TAC] THEN
REWRITE_TAC[
VEC_COMPONENT;
VECTOR_NEG_COMPONENT] THEN
DISCH_THEN(X_CHOOSE_THEN `D:(real^M->bool)->bool` STRIP_ASSUME_TAC) THEN
SUBGOAL_THEN
`!k:real^M->bool.
k
IN D
==> ?t. measurable(t) /\
IMAGE (f:real^M->real^N) (k
INTER s)
SUBSET t /\
measure t <= e / &(2 * c) pow (dimindex(:M)) * measure(k)`
MP_TAC THENL
[X_GEN_TAC `k:real^M->bool` THEN DISCH_TAC THEN
SUBGOAL_THEN `?u v:real^M. k = interval[u,v]`
(REPEAT_TCL CHOOSE_THEN SUBST_ALL_TAC)
THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
SUBGOAL_THEN `?x:real^M. x
IN (s
INTER interval[u,v]) /\
interval[u,v]
SUBSET ball(x,r x)`
MP_TAC THENL [ASM_MESON_TAC[]; REWRITE_TAC[
IN_INTER]] THEN
DISCH_THEN(X_CHOOSE_THEN `x:real^M` STRIP_ASSUME_TAC) THEN
MP_TAC(ISPECL [`
IMAGE ((f':real^M->real^M->real^N) x) (:real^M)`;
`(f:real^M->real^N) x`;
`d * norm(v - u:real^M)`;
`(&2 * B) * norm(v - u:real^M)`]
lemma) THEN
ANTS_TAC THENL
[ASM_SIMP_TAC[
REAL_LE_MUL;
REAL_POS;
NORM_POS_LE;
REAL_LT_IMP_LE] THEN
MP_TAC(ISPEC `matrix ((f':real^M->real^M->real^N) x)`
RANK_DIM_IM) THEN
ASM_SIMP_TAC[
MATRIX_WORKS] THEN REWRITE_TAC[ETA_AX] THEN
ASM_MESON_TAC[];
ALL_TAC] THEN
MATCH_MP_TAC
MONO_EXISTS THEN X_GEN_TAC `t:real^N->bool` THEN
REPEAT(MATCH_MP_TAC MONO_AND THEN REWRITE_TAC[]) THEN CONJ_TAC THENL
[MATCH_MP_TAC(REWRITE_RULE[
IMP_CONJ]
SUBSET_TRANS) THEN
REWRITE_TAC[
FORALL_IN_IMAGE;
SUBSET;
IN_ELIM_THM] THEN
X_GEN_TAC `y:real^M` THEN
REWRITE_TAC[
IN_INTER;
EXISTS_IN_IMAGE;
IN_UNIV] THEN
STRIP_TAC THEN REMOVE_THEN "*"
(MP_TAC o SPECL [`x:real^M`; `y:real^M`]) THEN
ANTS_TAC THENL
[ASM_MESON_TAC[
IN_BALL;
SUBSET;
NORM_SUB; dist]; ALL_TAC] THEN
DISCH_THEN(fun th -> CONJ_TAC THEN MP_TAC th) THENL
[REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN MATCH_MP_TAC(NORM_ARITH
`norm(z) <= B /\ d <= B
==> norm(y - x - z:real^N) <= d
==> norm(y - x) <= &2 * B`) THEN
CONJ_TAC THENL
[MP_TAC(ISPEC `(f':real^M->real^M->real^N) x`
ONORM) THEN
ASM_SIMP_TAC[] THEN
DISCH_THEN(MP_TAC o SPEC `y - x:real^M` o CONJUNCT1) THEN
MATCH_MP_TAC(REWRITE_RULE[
IMP_CONJ_ALT]
REAL_LE_TRANS) THEN
MATCH_MP_TAC
REAL_LE_MUL2 THEN
ASM_SIMP_TAC[
ONORM_POS_LE;
NORM_POS_LE];
MATCH_MP_TAC
REAL_LE_MUL2 THEN
ASM_SIMP_TAC[
REAL_LT_IMP_LE;
NORM_POS_LE]];
DISCH_THEN(fun th -> EXISTS_TAC `y - x:real^M` THEN MP_TAC th) THEN
MATCH_MP_TAC(REWRITE_RULE[
IMP_CONJ_ALT]
REAL_LE_TRANS) THEN
ASM_SIMP_TAC[
REAL_LE_LMUL_EQ]] THEN
MATCH_MP_TAC
NORM_LE_COMPONENTWISE THEN
REPEAT(FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [
IN_INTERVAL])) THEN
REWRITE_TAC[IMP_IMP;
AND_FORALL_THM] THEN
MATCH_MP_TAC
MONO_FORALL THEN GEN_TAC THEN
DISCH_THEN(fun th -> STRIP_TAC THEN MP_TAC th) THEN
ASM_REWRITE_TAC[
VECTOR_SUB_COMPONENT] THEN REAL_ARITH_TAC;
MATCH_MP_TAC(REWRITE_RULE[
IMP_CONJ_ALT]
REAL_LE_TRANS) THEN
REWRITE_TAC[REAL_ARITH `&2 * (&2 * B) * n = (&4 * B) * n`] THEN
GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [
REAL_POW_MUL] THEN
SIMP_TAC[REAL_ARITH `(&2 * d * n) * a * b = d * &2 * a * (n * b)`] THEN
REWRITE_TAC[GSYM(CONJUNCT2
real_pow)] THEN
SIMP_TAC[
DIMINDEX_GE_1; ARITH_RULE `1 <= n ==> SUC(n - 1) = n`] THEN
MATCH_MP_TAC
REAL_LE_TRANS THEN
EXISTS_TAC `e / &(2 * c) pow (dimindex(:M)) /
(&(dimindex(:M)) pow dimindex(:M)) *
norm(v - u:real^M) pow dimindex(:N)` THEN
CONJ_TAC THENL
[REWRITE_TAC[REAL_MUL_ASSOC] THEN MATCH_MP_TAC
REAL_LE_RMUL THEN
ASM_SIMP_TAC[
NORM_POS_LE;
REAL_POW_LE];
ALL_TAC] THEN
GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [
real_div] THEN
REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN MATCH_MP_TAC
REAL_LE_LMUL THEN
ASM_SIMP_TAC[
REAL_LE_DIV;
REAL_POW_LE;
REAL_LT_IMP_LE] THEN
REWRITE_TAC[ONCE_REWRITE_RULE[REAL_MUL_SYM] (GSYM
real_div)] THEN
SIMP_TAC[
REAL_LE_LDIV_EQ;
REAL_POW_LT;
REAL_OF_NUM_LT;
LE_1;
DIMINDEX_GE_1] THEN
MATCH_MP_TAC
REAL_LE_TRANS THEN
EXISTS_TAC `norm(v - u:real^M) pow dimindex(:M)` THEN CONJ_TAC THENL
[MATCH_MP_TAC
REAL_POW_MONO_INV THEN ASM_REWRITE_TAC[
NORM_POS_LE] THEN
SUBGOAL_THEN `u
IN ball(x:real^M,r x) /\ v
IN ball(x,r x)` MP_TAC
THENL
[ASM_MESON_TAC[
SUBSET;
ENDS_IN_INTERVAL;
INTERIOR_EMPTY];
REWRITE_TAC[
IN_BALL] THEN
SUBGOAL_THEN `(r:real^M->real) x <= &1 / &2` MP_TAC THENL
[ASM_REWRITE_TAC[]; CONV_TAC NORM_ARITH]];
REMOVE_THEN "*" (K ALL_TAC) THEN
FIRST_X_ASSUM(MP_TAC o SPECL [`u:real^M`; `v:real^M`]) THEN
ASM_REWRITE_TAC[REAL_ARITH `x - --x = &2 * x`] THEN
REWRITE_TAC[
LEFT_IMP_EXISTS_THM; REAL_OF_NUM_MUL] THEN
X_GEN_TAC `p:num` THEN DISCH_TAC THEN
MATCH_MP_TAC
REAL_LE_TRANS THEN
EXISTS_TAC `(sum(1..dimindex(:M)) (\i. abs((v - u:real^M)$i)))
pow (dimindex(:M))` THEN
CONJ_TAC THENL
[MATCH_MP_TAC
REAL_POW_LE2 THEN SIMP_TAC[
NORM_POS_LE;
NORM_LE_L1];
REWRITE_TAC[
MEASURE_INTERVAL;
CONTENT_CLOSED_INTERVAL_CASES] THEN
GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV)
[GSYM
REAL_SUB_LE] THEN
ASM_SIMP_TAC[
REAL_LT_IMP_LE;
REAL_LT_DIV;
REAL_LT_POW2] THEN
ASM_SIMP_TAC[
SUM_CONST_NUMSEG;
PRODUCT_CONST_NUMSEG;
VECTOR_SUB_COMPONENT;
ADD_SUB] THEN
REWRITE_TAC[
REAL_POW_MUL; REAL_MUL_SYM] THEN
MATCH_MP_TAC
REAL_EQ_IMP_LE THEN BINOP_TAC THEN REWRITE_TAC[] THEN
AP_THM_TAC THEN AP_TERM_TAC THEN SIMP_TAC[
REAL_ABS_REFL] THEN
ASM_SIMP_TAC[
REAL_LT_IMP_LE;
REAL_LT_DIV;
REAL_LT_POW2]]]];
GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [
RIGHT_IMP_EXISTS_THM] THEN
REWRITE_TAC[
SKOLEM_THM;
LEFT_IMP_EXISTS_THM] THEN
X_GEN_TAC `g:(real^M->bool)->(real^N->bool)` THEN DISCH_TAC THEN
EXISTS_TAC `
UNIONS (
IMAGE (g:(real^M->bool)->(real^N->bool)) D)` THEN
CONJ_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
MATCH_MP_TAC
MEASURE_COUNTABLE_UNIONS_LE_STRONG_GEN THEN
ASM_SIMP_TAC[
COUNTABLE_IMAGE;
FORALL_IN_IMAGE] THEN
ONCE_REWRITE_TAC[
CONJ_SYM] THEN
REWRITE_TAC[
FORALL_FINITE_SUBSET_IMAGE] THEN
X_GEN_TAC `D':(real^M->bool)->bool` THEN STRIP_TAC THEN
W(MP_TAC o PART_MATCH (lhand o rand)
MEASURE_UNIONS_LE_IMAGE o
lhand o snd) THEN
ANTS_TAC THENL [ASM_MESON_TAC[
SUBSET]; ALL_TAC] THEN
MATCH_MP_TAC(REWRITE_RULE[
IMP_CONJ_ALT]
REAL_LE_TRANS) THEN
MATCH_MP_TAC
REAL_LE_TRANS THEN
EXISTS_TAC
`sum D' (\k:real^M->bool.
e / &(2 * c) pow (dimindex(:M)) * measure k)` THEN CONJ_TAC
THENL [MATCH_MP_TAC
SUM_LE THEN ASM_MESON_TAC[
SUBSET]; ALL_TAC] THEN
REWRITE_TAC[
SUM_LMUL] THEN
REWRITE_TAC[REAL_ARITH `e / b * x:real = (e * x) / b`] THEN
ASM_SIMP_TAC[
REAL_POW_LT;
REAL_LE_LDIV_EQ;
REAL_LE_LMUL_EQ] THEN
MP_TAC(ISPECL [`D':(real^M->bool)->bool`; `
UNIONS D':real^M->bool`]
MEASURE_ELEMENTARY) THEN
ANTS_TAC THENL
[ASM_REWRITE_TAC[
division_of] THEN
CONJ_TAC THENL [ALL_TAC; ASM_MESON_TAC[
SUBSET]] THEN
GEN_TAC THEN DISCH_TAC THEN CONJ_TAC THENL
[ASM SET_TAC[]; ASM_MESON_TAC[
SUBSET;
INTERIOR_EMPTY]];
ALL_TAC] THEN
MATCH_MP_TAC(REAL_ARITH `y = z /\ x <= e ==> x = y ==> z <= e`) THEN
CONJ_TAC THENL
[MATCH_MP_TAC
SUM_EQ THEN ASM_MESON_TAC[
MEASURE_INTERVAL;
SUBSET];
ALL_TAC] THEN
MATCH_MP_TAC
REAL_LE_TRANS THEN
EXISTS_TAC `measure(interval[--(vec c):real^M,vec c])` THEN CONJ_TAC THENL
[MATCH_MP_TAC
MEASURE_SUBSET THEN REWRITE_TAC[
MEASURABLE_INTERVAL] THEN
CONJ_TAC THENL [MATCH_MP_TAC
MEASURABLE_UNIONS; ASM SET_TAC[]] THEN
ASM_MESON_TAC[
SUBSET;
MEASURABLE_INTERVAL];
SIMP_TAC[
MEASURE_INTERVAL;
CONTENT_CLOSED_INTERVAL_CASES] THEN
REWRITE_TAC[
VEC_COMPONENT;
VECTOR_NEG_COMPONENT; REAL_ARITH
`x - --x = &2 * x /\ (--x <= x <=> &0 <= &2 * x)`] THEN
ASM_SIMP_TAC[REAL_OF_NUM_MUL;
REAL_LT_IMP_LE] THEN
REWRITE_TAC[
PRODUCT_CONST_NUMSEG;
ADD_SUB;
REAL_LE_REFL]]]) in
REPEAT STRIP_TAC THEN
SUBGOAL_THEN
`s =
UNIONS
{{x | x
IN s /\ norm(x:real^M) <= &n /\
onorm((f':real^M->real^M->real^N) x) <= &n} |
n
IN (:num)}`
SUBST1_TAC THENL
[REWRITE_TAC[
EXTENSION;
UNIONS_GSPEC;
IN_ELIM_THM;
IN_UNIV] THEN
X_GEN_TAC `x:real^M` THEN
ASM_CASES_TAC `(x:real^M)
IN s` THEN ASM_REWRITE_TAC[] THEN
REWRITE_TAC[GSYM
REAL_MAX_LE;
REAL_ARCH_SIMPLE];
REWRITE_TAC[
IMAGE_UNIONS] THEN
MATCH_MP_TAC
NEGLIGIBLE_COUNTABLE_UNIONS_GEN THEN
REWRITE_TAC[
FORALL_IN_IMAGE;
FORALL_IN_GSPEC] THEN
ONCE_REWRITE_TAC[
SIMPLE_IMAGE] THEN
ASM_SIMP_TAC[GSYM
IMAGE_o;
COUNTABLE_IMAGE;
NUM_COUNTABLE] THEN
X_GEN_TAC `n:num` THEN REWRITE_TAC[
IN_UNIV] THEN
MATCH_MP_TAC semma THEN
MAP_EVERY EXISTS_TAC [`f':real^M->real^M->real^N`; `&n + &1:real`] THEN
ASM_REWRITE_TAC[] THEN CONJ_TAC THENL [REAL_ARITH_TAC; ALL_TAC] THEN
CONJ_TAC THENL
[MATCH_MP_TAC
BOUNDED_SUBSET THEN
EXISTS_TAC `cball(vec 0:real^M,&n)` THEN
SIMP_TAC[
BOUNDED_CBALL;
SUBSET;
IN_CBALL_0;
IN_ELIM_THM];
X_GEN_TAC `x:real^M` THEN REWRITE_TAC[
IN_ELIM_THM] THEN STRIP_TAC THEN
ASM_SIMP_TAC[REAL_ARITH `x <= n ==> x <= n + &1`] THEN
FIRST_X_ASSUM(MP_TAC o SPEC `x:real^M`) THEN ASM_REWRITE_TAC[] THEN
REPEAT STRIP_TAC THEN
FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REWRITE_RULE[
IMP_CONJ]
HAS_DERIVATIVE_WITHIN_SUBSET)) THEN SET_TAC[]]]);;
let NEGLIGIBLE_IMAGE_BOUNDED_VARIATION_INTERVAL = prove
(`!f:real^1->real^N a b.
2 <= dimindex(:N) /\ f
has_bounded_variation_on interval[a,b]
==> negligible(
IMAGE f (interval[a,b]))`,
REPEAT STRIP_TAC THEN
FIRST_ASSUM(MP_TAC o MATCH_MP (REWRITE_RULE[
IMP_CONJ]
HAS_BOUNDED_VECTOR_VARIATION_RIGHT_LIMIT)) THEN
FIRST_ASSUM(MP_TAC o MATCH_MP (REWRITE_RULE[
IMP_CONJ]
HAS_BOUNDED_VECTOR_VARIATION_LEFT_LIMIT)) THEN
REWRITE_TAC[
RIGHT_IMP_EXISTS_THM] THEN
REWRITE_TAC[
SKOLEM_THM;
LEFT_IMP_EXISTS_THM] THEN
X_GEN_TAC `l:real^1->real^N` THEN DISCH_TAC THEN
X_GEN_TAC `r:real^1->real^N` THEN DISCH_TAC THEN
REWRITE_TAC[
NEGLIGIBLE_OUTER_LE] THEN X_GEN_TAC `ee:real` THEN DISCH_TAC THEN
ABBREV_TAC
`e = min (&1) (ee /
(&2 pow (dimindex(:N)) *
vector_variation (interval[a,b]) (f:real^1->real^N) + &1))` THEN
SUBGOAL_THEN `&0 < e` ASSUME_TAC THENL
[EXPAND_TAC "e" THEN
MATCH_MP_TAC(REAL_ARITH `&0 < x ==> &0 < min (&1) x`) THEN
MATCH_MP_TAC
REAL_LT_DIV THEN ASM_REWRITE_TAC[] THEN
MATCH_MP_TAC(REAL_ARITH `&0 <= x ==> &0 < x + &1`) THEN
MATCH_MP_TAC
REAL_LE_MUL THEN ASM_SIMP_TAC[
VECTOR_VARIATION_POS_LE] THEN
MATCH_MP_TAC
REAL_POW_LE THEN REAL_ARITH_TAC;
ALL_TAC] THEN
SUBGOAL_THEN
`!c. ?d. &0 < d /\
(c
IN interval[a,b]
==> (!x. x
IN interval[a,c] /\ ~(x = c) /\ dist(x,c) < d
==> dist((f:real^1->real^N) x,l c) < e) /\
(!x. x
IN interval[c,b] /\ ~(x = c) /\ dist(x,c) < d
==> dist(f x,r c) < e))`
MP_TAC THENL
[X_GEN_TAC `c:real^1` THEN ASM_CASES_TAC `(c:real^1)
IN interval[a,b]` THENL
[ALL_TAC; EXISTS_TAC `&1` THEN ASM_REWRITE_TAC[
REAL_LT_01]] THEN
REPEAT(FIRST_X_ASSUM(MP_TAC o SPEC `c:real^1`)) THEN
ASM_REWRITE_TAC[
LIM_WITHIN; IMP_IMP;
AND_FORALL_THM] THEN
DISCH_THEN(MP_TAC o SPEC `e:real`) THEN ASM_REWRITE_TAC[GSYM
DIST_NZ] THEN
DISCH_THEN(CONJUNCTS_THEN2
(X_CHOOSE_THEN `d1:real` STRIP_ASSUME_TAC)
(X_CHOOSE_THEN `d2:real` STRIP_ASSUME_TAC)) THEN
EXISTS_TAC `min d1 d2:real` THEN ASM_SIMP_TAC[
REAL_LT_MIN];
REWRITE_TAC[
SKOLEM_THM;
FORALL_AND_THM;
LEFT_IMP_EXISTS_THM] THEN
X_GEN_TAC `d:real^1->real` THEN
DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC (LABEL_TAC "*"))] THEN
MP_TAC(ISPECL [`\x:real^1. ball(x,d x)`; `a:real^1`; `b:real^1`]
FINE_DIVISION_EXISTS) THEN
ASM_REWRITE_TAC[fine; gauge;
OPEN_BALL;
CENTRE_IN_BALL] THEN
DISCH_THEN(X_CHOOSE_THEN
`p:(real^1#(real^1->bool))->bool` STRIP_ASSUME_TAC) THEN
FIRST_ASSUM(ASSUME_TAC o MATCH_MP
TAGGED_DIVISION_OF_FINITE) THEN
EXISTS_TAC
`
UNIONS(
IMAGE (\(c,k).
(f c)
INSERT
(cball((l:real^1->real^N) c,
min e (
vector_variation (interval[
interval_lowerbound k,c])
(f:real^1->real^N)))
UNION
cball((r:real^1->real^N) c,
min e (
vector_variation (interval[c,
interval_upperbound k])
(f:real^1->real^N))))) p)` THEN
REPEAT CONJ_TAC THENL
[FIRST_ASSUM(SUBST1_TAC o MATCH_MP
TAGGED_DIVISION_UNION_IMAGE_SND) THEN
REWRITE_TAC[
IMAGE_UNIONS; GSYM
IMAGE_o] THEN
MATCH_MP_TAC
UNIONS_MONO_IMAGE THEN
REWRITE_TAC[
FORALL_PAIR_THM;
o_THM] THEN
MAP_EVERY X_GEN_TAC [`c:real^1`; `k:real^1->bool`] THEN DISCH_TAC THEN
SUBGOAL_THEN `?u v:real^1. k = interval[u,v]`
(REPEAT_TCL CHOOSE_THEN SUBST_ALL_TAC)
THENL [ASM_MESON_TAC[
TAGGED_DIVISION_OF]; ALL_TAC] THEN
SUBGOAL_THEN `drop u <= drop v` ASSUME_TAC THENL
[ASM_MESON_TAC[
TAGGED_DIVISION_OF;
INTERVAL_NE_EMPTY_1;
NOT_IN_EMPTY];
ASM_SIMP_TAC[
INTERVAL_LOWERBOUND_1;
INTERVAL_UPPERBOUND_1]] THEN
REWRITE_TAC[
SUBSET;
FORALL_IN_IMAGE] THEN
X_GEN_TAC `x:real^1` THEN REWRITE_TAC[
IN_INTERVAL_1] THEN STRIP_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPECL [`c:real^1`; `interval[u:real^1,v]`]) THEN
ASM_REWRITE_TAC[
SUBSET;
IN_INTERVAL_1;
IN_CBALL] THEN DISCH_TAC THEN
REWRITE_TAC[
IN_INSERT;
IN_UNION] THEN ASM_CASES_TAC `x:real^1 = c` THEN
ASM_REWRITE_TAC[] THEN DISJ2_TAC THEN
SIMP_TAC[
IN_CBALL;
REAL_LE_MIN] THEN ASM_CASES_TAC `drop x <= drop c` THENL
[DISJ1_TAC THEN CONJ_TAC THENL
[ONCE_REWRITE_TAC[
DIST_SYM] THEN MATCH_MP_TAC
REAL_LT_IMP_LE THEN
REMOVE_THEN "*" (MP_TAC o SPEC `c:real^1`) THEN ANTS_TAC THENL
[ASM_MESON_TAC[
TAGGED_DIVISION_OF;
SUBSET]; ALL_TAC] THEN
DISCH_THEN(MATCH_MP_TAC o CONJUNCT1) THEN ASM_REWRITE_TAC[] THEN
ASM_SIMP_TAC[GSYM(ONCE_REWRITE_RULE[
DIST_SYM]
IN_BALL)] THEN
ASM_MESON_TAC[
IN_INTERVAL_1;
SUBSET;
TAGGED_DIVISION_OF];
ALL_TAC] THEN
SUBGOAL_THEN `drop a <= drop u /\ drop x < drop c /\
drop c <= drop v /\ drop v <= drop b`
STRIP_ASSUME_TAC THENL
[ASM_REWRITE_TAC[
REAL_LT_LE;
DROP_EQ] THEN
ASM_MESON_TAC[
IN_INTERVAL_1;
SUBSET;
TAGGED_DIVISION_OF;
REAL_LE_TOTAL];
ALL_TAC] THEN
REWRITE_TAC[ONCE_REWRITE_RULE[
NORM_SUB] dist] THEN
MATCH_MP_TAC
(REWRITE_RULE[
LIFT_DROP;
FORALL_LIFT]
(ISPEC `at c within interval [u:real^1,c]`
LIM_DROP_UBOUND)) THEN
EXISTS_TAC `\y:real^1. lift(norm(f x - f y:real^N))` THEN
REWRITE_TAC[
TRIVIAL_LIMIT_WITHIN;
LIFT_DROP] THEN REPEAT CONJ_TAC THENL
[MATCH_MP_TAC
LIM_NORM THEN MATCH_MP_TAC
LIM_SUB THEN
ASM_SIMP_TAC[
IN_INTERVAL_1;
LIM_CONST] THEN
MATCH_MP_TAC
LIM_WITHIN_SUBSET THEN
EXISTS_TAC `interval[a:real^1,c]` THEN CONJ_TAC THENL
[FIRST_X_ASSUM MATCH_MP_TAC THEN REWRITE_TAC[
IN_INTERVAL_1] THEN
ASM_REAL_ARITH_TAC;
REWRITE_TAC[
SUBSET_INTERVAL_1] THEN ASM_REAL_ARITH_TAC];
W(MP_TAC o PART_MATCH (lhs o rand)
LIMPT_OF_CONVEX o snd) THEN
ANTS_TAC THENL
[SIMP_TAC[
CONVEX_INTERVAL;
ENDS_IN_INTERVAL;
INTERVAL_NE_EMPTY_1] THEN
ASM_REAL_ARITH_TAC;
DISCH_THEN SUBST1_TAC THEN MATCH_MP_TAC(SET_RULE
`(?y. ~(y = x) /\ y
IN s) ==> ~(s = {x})`) THEN
EXISTS_TAC `u:real^1` THEN
REWRITE_TAC[
IN_INTERVAL_1; GSYM
DROP_EQ] THEN ASM_REAL_ARITH_TAC];
REWRITE_TAC[
EVENTUALLY_WITHIN] THEN EXISTS_TAC `&1` THEN
REWRITE_TAC[
REAL_LT_01] THEN X_GEN_TAC `y:real^1` THEN
REWRITE_TAC[
IN_INTERVAL_1] THEN STRIP_TAC THEN
MATCH_MP_TAC
VECTOR_VARIATION_GE_NORM_FUNCTION THEN CONJ_TAC THENL
[FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REWRITE_RULE[
IMP_CONJ]
HAS_BOUNDED_VARIATION_ON_SUBSET)) THEN
REWRITE_TAC[
SUBSET_INTERVAL_1] THEN ASM_REAL_ARITH_TAC;
MATCH_MP_TAC(CONJUNCT1(SPEC_ALL
(REWRITE_RULE[
CONVEX_CONTAINS_SEGMENT]
CONVEX_INTERVAL))) THEN
REWRITE_TAC[
IN_INTERVAL_1] THEN ASM_REAL_ARITH_TAC]];
DISJ2_TAC THEN CONJ_TAC THENL
[ONCE_REWRITE_TAC[
DIST_SYM] THEN MATCH_MP_TAC
REAL_LT_IMP_LE THEN
REMOVE_THEN "*" (MP_TAC o SPEC `c:real^1`) THEN ANTS_TAC THENL
[ASM_MESON_TAC[
TAGGED_DIVISION_OF;
SUBSET]; ALL_TAC] THEN
DISCH_THEN(MATCH_MP_TAC o CONJUNCT2) THEN ASM_REWRITE_TAC[] THEN
ASM_SIMP_TAC[GSYM(ONCE_REWRITE_RULE[
DIST_SYM]
IN_BALL)] THEN
ASM_MESON_TAC[
IN_INTERVAL_1;
SUBSET;
TAGGED_DIVISION_OF;
REAL_LE_TOTAL];
ALL_TAC] THEN
SUBGOAL_THEN `drop a <= drop c /\ drop c < drop x /\
drop x <= drop v /\ drop v <= drop b`
STRIP_ASSUME_TAC THENL
[ASM_REWRITE_TAC[GSYM
REAL_NOT_LE] THEN
ASM_MESON_TAC[
IN_INTERVAL_1;
SUBSET;
TAGGED_DIVISION_OF;
REAL_LE_TOTAL];
ALL_TAC] THEN
REWRITE_TAC[ONCE_REWRITE_RULE[
NORM_SUB] dist] THEN
MATCH_MP_TAC
(REWRITE_RULE[
LIFT_DROP;
FORALL_LIFT]
(ISPEC `at c within interval [c:real^1,v]`
LIM_DROP_UBOUND)) THEN
EXISTS_TAC `\y:real^1. lift(norm(f x - f y:real^N))` THEN
REWRITE_TAC[
TRIVIAL_LIMIT_WITHIN;
LIFT_DROP] THEN REPEAT CONJ_TAC THENL
[MATCH_MP_TAC
LIM_NORM THEN MATCH_MP_TAC
LIM_SUB THEN
ASM_SIMP_TAC[
IN_INTERVAL_1;
LIM_CONST] THEN
MATCH_MP_TAC
LIM_WITHIN_SUBSET THEN
EXISTS_TAC `interval[c:real^1,b]` THEN CONJ_TAC THENL
[FIRST_X_ASSUM MATCH_MP_TAC THEN REWRITE_TAC[
IN_INTERVAL_1] THEN
ASM_REAL_ARITH_TAC;
REWRITE_TAC[
SUBSET_INTERVAL_1] THEN ASM_REAL_ARITH_TAC];
W(MP_TAC o PART_MATCH (lhs o rand)
LIMPT_OF_CONVEX o snd) THEN
ANTS_TAC THENL
[SIMP_TAC[
CONVEX_INTERVAL;
ENDS_IN_INTERVAL;
INTERVAL_NE_EMPTY_1] THEN
ASM_REAL_ARITH_TAC;
DISCH_THEN SUBST1_TAC THEN MATCH_MP_TAC(SET_RULE
`(?y. ~(y = x) /\ y
IN s) ==> ~(s = {x})`) THEN
EXISTS_TAC `v:real^1` THEN
REWRITE_TAC[
IN_INTERVAL_1; GSYM
DROP_EQ] THEN ASM_REAL_ARITH_TAC];
REWRITE_TAC[
EVENTUALLY_WITHIN] THEN EXISTS_TAC `&1` THEN
REWRITE_TAC[
REAL_LT_01] THEN X_GEN_TAC `y:real^1` THEN
REWRITE_TAC[
IN_INTERVAL_1] THEN STRIP_TAC THEN
MATCH_MP_TAC
VECTOR_VARIATION_GE_NORM_FUNCTION THEN CONJ_TAC THENL
[FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REWRITE_RULE[
IMP_CONJ]
HAS_BOUNDED_VARIATION_ON_SUBSET)) THEN
REWRITE_TAC[
SUBSET_INTERVAL_1] THEN ASM_REAL_ARITH_TAC;
MATCH_MP_TAC(CONJUNCT1(SPEC_ALL
(REWRITE_RULE[
CONVEX_CONTAINS_SEGMENT]
CONVEX_INTERVAL))) THEN
REWRITE_TAC[
IN_INTERVAL_1] THEN ASM_REAL_ARITH_TAC]]];
MATCH_MP_TAC
MEASURABLE_UNIONS THEN ASM_SIMP_TAC[
FINITE_IMAGE] THEN
REWRITE_TAC[
FORALL_IN_IMAGE;
FORALL_PAIR_THM] THEN
SIMP_TAC[
MEASURABLE_CBALL;
MEASURABLE_UNION;
MEASURABLE_INSERT];
W(MP_TAC o PART_MATCH (lhand o rand)
MEASURE_UNIONS_LE_IMAGE o
lhand o snd) THEN
ANTS_TAC THENL
[ASM_REWRITE_TAC[
FORALL_IN_IMAGE;
FORALL_PAIR_THM] THEN
SIMP_TAC[
MEASURABLE_CBALL;
MEASURABLE_UNION;
MEASURABLE_INSERT];
MATCH_MP_TAC(REWRITE_RULE[
IMP_CONJ_ALT]
REAL_LE_TRANS)] THEN
ONCE_REWRITE_TAC[
LAMBDA_PAIR_THM] THEN REWRITE_TAC[
MEASURE_INSERT] THEN
MATCH_MP_TAC
REAL_LE_TRANS THEN
EXISTS_TAC
`&2 pow (dimindex(:N)) *
e * sum p (\(x:real^1,k).
vector_variation k (f:real^1->real^N))` THEN
CONJ_TAC THENL
[REWRITE_TAC[GSYM
SUM_LMUL] THEN MATCH_MP_TAC
SUM_LE THEN
ASM_REWRITE_TAC[
FORALL_PAIR_THM] THEN
MAP_EVERY X_GEN_TAC [`c:real^1`; `k:real^1->bool`] THEN DISCH_TAC THEN
SUBGOAL_THEN `?u v:real^1. k = interval[u,v]`
(REPEAT_TCL CHOOSE_THEN SUBST_ALL_TAC)
THENL [ASM_MESON_TAC[
TAGGED_DIVISION_OF]; ALL_TAC] THEN
SUBGOAL_THEN `drop u <= drop v` ASSUME_TAC THENL
[ASM_MESON_TAC[
TAGGED_DIVISION_OF;
INTERVAL_NE_EMPTY_1;
NOT_IN_EMPTY];
ASM_SIMP_TAC[
INTERVAL_LOWERBOUND_1;
INTERVAL_UPPERBOUND_1]] THEN
SUBGOAL_THEN
`(f:real^1->real^N)
has_bounded_variation_on interval[u,c] /\
(f:real^1->real^N)
has_bounded_variation_on interval[c,v]`
STRIP_ASSUME_TAC THENL
[CONJ_TAC THEN FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP
(REWRITE_RULE[
IMP_CONJ]
HAS_BOUNDED_VARIATION_ON_SUBSET)) THEN
MATCH_MP_TAC
SUBSET_TRANS THEN EXISTS_TAC `interval[u:real^1,v]` THEN
(CONJ_TAC THENL [ALL_TAC; ASM_MESON_TAC[
TAGGED_DIVISION_OF]]) THEN
REWRITE_TAC[
SUBSET_INTERVAL_1;
REAL_LE_REFL] THEN
REWRITE_TAC[GSYM
IN_INTERVAL_1] THEN ASM_MESON_TAC[
TAGGED_DIVISION_OF];
ALL_TAC] THEN
SUBGOAL_THEN
`
vector_variation (interval [u,v]) (f:real^1->real^N) =
vector_variation (interval [u,c]) f +
vector_variation (interval [c,v]) f`
SUBST1_TAC THENL
[CONV_TAC SYM_CONV THEN MATCH_MP_TAC
VECTOR_VARIATION_COMBINE THEN
ASM_REWRITE_TAC[
CONJ_ASSOC; GSYM
IN_INTERVAL_1] THEN
CONJ_TAC THENL [ASM_MESON_TAC[
TAGGED_DIVISION_OF]; ALL_TAC] THEN
ASM_MESON_TAC[
TAGGED_DIVISION_OF;
HAS_BOUNDED_VARIATION_ON_SUBSET];
ALL_TAC] THEN
W(MP_TAC o PART_MATCH (lhand o rand)
MEASURE_UNION_LE o lhand o snd) THEN
REWRITE_TAC[
MEASURABLE_CBALL; REAL_ADD_LDISTRIB] THEN
MATCH_MP_TAC(REWRITE_RULE[
IMP_CONJ_ALT]
REAL_LE_TRANS) THEN
MATCH_MP_TAC
REAL_LE_ADD2 THEN CONJ_TAC THEN
W(MP_TAC o PART_MATCH (lhand o rand)
MEASURE_CBALL_BOUND o lhand o snd) THEN
ASM_SIMP_TAC[
REAL_LE_MIN;
REAL_LT_IMP_LE;
VECTOR_VARIATION_POS_LE] THEN
MATCH_MP_TAC(REWRITE_RULE[
IMP_CONJ_ALT]
REAL_LE_TRANS) THEN
REWRITE_TAC[
REAL_POW_MUL] THEN MATCH_MP_TAC
REAL_LE_LMUL THEN
SIMP_TAC[
REAL_POW_LE;
REAL_POS] THEN
(SUBGOAL_THEN `dimindex(:N) = (dimindex(:N) - 1) + 1` SUBST1_TAC THENL
[ASM_ARITH_TAC; REWRITE_TAC[
REAL_POW_ADD;
REAL_POW_1]]) THEN
MATCH_MP_TAC
REAL_LE_MUL2 THEN
ASM_SIMP_TAC[
REAL_LE_MIN;
REAL_LT_IMP_LE;
VECTOR_VARIATION_POS_LE;
REAL_POW_LE; REAL_ARITH `min e v <= v`] THEN
MATCH_MP_TAC
REAL_LE_TRANS THEN
EXISTS_TAC `(e:real) pow (dimindex(:N) - 1)` THEN
(CONJ_TAC THENL
[MATCH_MP_TAC
REAL_POW_LE2 THEN
ASM_SIMP_TAC[
REAL_LE_MIN;
REAL_LT_IMP_LE;
VECTOR_VARIATION_POS_LE] THEN
REAL_ARITH_TAC;
GEN_REWRITE_TAC RAND_CONV [GSYM
REAL_POW_1] THEN
MATCH_MP_TAC
REAL_POW_MONO_INV THEN
ASM_SIMP_TAC[
REAL_LT_IMP_LE] THEN EXPAND_TAC "e" THEN CONJ_TAC THENL
[ASM_REAL_ARITH_TAC; ASM_ARITH_TAC]]);
MATCH_MP_TAC
REAL_LE_TRANS THEN EXISTS_TAC
`&2 pow dimindex (:N) *
(ee / (&2 pow (dimindex(:N)) *
vector_variation (interval[a,b]) (f:real^1->real^N) + &1)) *
sum p (\(x:real^1,k).
vector_variation k f)` THEN
CONJ_TAC THENL
[MATCH_MP_TAC
REAL_LE_LMUL THEN SIMP_TAC[
REAL_POS;
REAL_POW_LE] THEN
MATCH_MP_TAC
REAL_LE_RMUL THEN CONJ_TAC THENL
[EXPAND_TAC "e" THEN REAL_ARITH_TAC; ALL_TAC] THEN
MATCH_MP_TAC
SUM_POS_LE THEN ASM_REWRITE_TAC[
FORALL_PAIR_THM] THEN
ASM_MESON_TAC[
HAS_BOUNDED_VARIATION_ON_SUBSET;
TAGGED_DIVISION_OF;
VECTOR_VARIATION_POS_LE];
ALL_TAC] THEN
REWRITE_TAC[REAL_ARITH `a * b / c * d:real = (b * a * d) / c`] THEN
W(MP_TAC o PART_MATCH (lhand o rand)
REAL_LE_LDIV_EQ o snd) THEN
ASM_SIMP_TAC[
REAL_LE_MUL;
REAL_POS;
REAL_POW_LE;
VECTOR_VARIATION_POS_LE;
REAL_ARITH `&0 <= x ==> &0 < x + &1`] THEN
DISCH_THEN SUBST1_TAC THEN
ASM_SIMP_TAC[
REAL_LE_LMUL_EQ; GSYM REAL_MUL_ASSOC] THEN
MATCH_MP_TAC(REAL_ARITH `x <= y ==> x <= y + &1`) THEN
MATCH_MP_TAC
REAL_LE_LMUL THEN SIMP_TAC[
REAL_POW_LE;
REAL_POS] THEN
FIRST_ASSUM(MP_TAC o MATCH_MP (REWRITE_RULE[
IMP_CONJ]
SUM_OVER_TAGGED_DIVISION_LEMMA)) THEN DISCH_THEN(fun th ->
W(MP_TAC o PART_MATCH (lhs o rand) th o lhand o snd)) THEN
SIMP_TAC[
VECTOR_VARIATION_ON_NULL;
BOUNDED_INTERVAL] THEN
DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[ETA_AX] THEN
MATCH_MP_TAC
REAL_EQ_IMP_LE THEN
MATCH_MP_TAC
VECTOR_VARIATION_ON_DIVISION THEN
ASM_SIMP_TAC[
DIVISION_OF_TAGGED_DIVISION]]]);;
let MEASURABLE_ON_LINEAR_IMAGE_EQ = prove
(`!f:real^N->real^N h:real^N->real^P s.
linear f /\ (!x y. f x = f y ==> x = y)
==> ((h o f)
measurable_on s <=> h
measurable_on (
IMAGE f s))`,
let lemma = prove
(`!f:real^N->real^P g:real^N->real^N h s.
linear g /\ linear h /\ (!x. h(g x) = x) /\ (!x. g(h x) = x)
==> (f o g) measurable_on s ==> f measurable_on (IMAGE g s)`,
REPEAT GEN_TAC THEN REWRITE_TAC[measurable_on] THEN
STRIP_TAC THEN DISCH_THEN(X_CHOOSE_THEN `k:real^N->bool`
(X_CHOOSE_THEN `G:num->real^N->real^P` STRIP_ASSUME_TAC)) THEN
EXISTS_TAC `IMAGE (g:real^N->real^N) k` THEN
EXISTS_TAC `\n x. (G:num->real^N->real^P) n ((h:real^N->real^N) x)` THEN
ASM_SIMP_TAC[NEGLIGIBLE_LINEAR_IMAGE] THEN CONJ_TAC THENL
[GEN_TAC THEN GEN_REWRITE_TAC LAND_CONV [GSYM o_DEF] THEN
MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN
ASM_MESON_TAC[LINEAR_CONTINUOUS_ON; CONTINUOUS_ON_SUBSET; SUBSET_UNIV];
X_GEN_TAC `y:real^N` THEN DISCH_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPEC `(h:real^N->real^N) y`) THEN
ANTS_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
MATCH_MP_TAC EQ_IMP THEN AP_THM_TAC THEN AP_TERM_TAC THEN
ASM_REWRITE_TAC[o_THM] THEN
AP_THM_TAC THEN AP_THM_TAC THEN AP_TERM_TAC THEN ASM SET_TAC[]]) in
REPEAT GEN_TAC THEN DISCH_TAC THEN
FIRST_ASSUM(MP_TAC o MATCH_MP LINEAR_INJECTIVE_IMP_SURJECTIVE) THEN
POP_ASSUM MP_TAC THEN REWRITE_TAC[IMP_IMP; GSYM CONJ_ASSOC] THEN
DISCH_TAC THEN
FIRST_ASSUM(X_CHOOSE_THEN `g:real^N->real^N` STRIP_ASSUME_TAC o
MATCH_MP LINEAR_BIJECTIVE_LEFT_RIGHT_INVERSE) THEN
EQ_TAC THENL [ASM_MESON_TAC[lemma]; DISCH_TAC] THEN
MP_TAC(ISPECL [`(h:real^N->real^P) o (f:real^N->real^N)`;
`g:real^N->real^N`; `f:real^N->real^N`;
`IMAGE (f:real^N->real^N) s`] lemma) THEN
ASM_REWRITE_TAC[GSYM IMAGE_o; o_DEF; IMAGE_ID; ETA_AX]);;
let lemma0 = prove
(`!f:real^M->real^1 n m.
integer m /\
m / &2 pow n <= drop(f x) /\
drop(f x) < (m + &1) / &2 pow n /\
abs(m) <= &2 pow (2 * n)
==> vsum {k | integer k /\ abs(k) <= &2 pow (2 * n)}
(\k. k / &2 pow n %
indicator {y:real^M | k / &2 pow n <= drop(f y) /\
drop(f y) < (k + &1) / &2 pow n}
x) =
lift(m / &2 pow n)`,