(* ========================================================================= *)
(* 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_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)`,
(* ------------------------------------------------------------------------- *)
(* Properties of measure under simple affine transformations. *)
(* ------------------------------------------------------------------------- *)
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);;
add_translation_invariants [HAS_MEASURE_TRANSLATION_EQ];;
add_translation_invariants [MEASURE_TRANSLATION];;
add_translation_invariants [NEGLIGIBLE_TRANSLATION_EQ];;
add_translation_invariants [MEASURABLE_TRANSLATION_EQ];;
(* ------------------------------------------------------------------------- *)
(* Measurability of countable unions and intersections of various kinds. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Measurability of compact and bounded open sets. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* A nice lemma for negligibility proofs. *)
(* ------------------------------------------------------------------------- *)
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]);;
(* ------------------------------------------------------------------------- *)
(* In particular. *)
(* ------------------------------------------------------------------------- *)
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);;
(* ------------------------------------------------------------------------- *)
(* Measurability of bounded convex sets. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Various special cases. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Crude upper bounds for measure of balls. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Negligibility of image under non-injective linear map. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Some technical lemmas used in the approximation results that follow. *)
(* Proof of the covering lemma is an obvious multidimensional generalization *)
(* of Lemma 3, p65 of Swartz's "Introduction to Gauge Integrals". *)
(* ------------------------------------------------------------------------- *)
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[]);;
(* ------------------------------------------------------------------------- *)
(* Outer and inner approximation of measurable set by well-behaved sets. *)
(* ------------------------------------------------------------------------- *)
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[]]]);;
(* ------------------------------------------------------------------------- *)
(* Hence for linear transformation, suffices to check compact intervals. *)
(* ------------------------------------------------------------------------- *)
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]);;
(* ------------------------------------------------------------------------- *)
(* Some inductions by expressing mapping in terms of elementary matrices. *)
(* ------------------------------------------------------------------------- *)
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]);;
(* ------------------------------------------------------------------------- *)
(* The same thing in mapping form (might have been easier all along). *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Hence the effect of an arbitrary linear map on a measurable set. *)
(* ------------------------------------------------------------------------- *)
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_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]);;
add_linear_invariants [MEASURABLE_LINEAR_IMAGE_EQ];;
add_linear_invariants [NEGLIGIBLE_LINEAR_IMAGE_EQ];;
add_linear_invariants
[REWRITE_RULE[ORTHOGONAL_TRANSFORMATION] HAS_MEASURE_ORTHOGONAL_IMAGE_EQ];;
add_linear_invariants
[REWRITE_RULE[ORTHOGONAL_TRANSFORMATION] MEASURE_ORTHOGONAL_IMAGE_EQ];;
(* ------------------------------------------------------------------------- *)
(* Measure of a standard simplex. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Hence the measure of a general simplex. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Area of a triangle. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Volume of a tetrahedron. *)
(* ------------------------------------------------------------------------- *)
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`,
(* ------------------------------------------------------------------------- *)
(* Steinhaus's theorem. (Stromberg's proof as given on Wikipedia.) *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* A measurable set with cardinality less than c is negligible. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Austin's Lemma. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Some differentiability-like properties of the indefinite integral. *)
(* The first two proofs are minor variants of each other, but it was more *)
(* work to derive one from the other. *)
(* ------------------------------------------------------------------------- *)
"box"] THEN REWRITE_TAC[]] THEN
EXISTS_TAC
`{x | ~(!e. &0 < e
==> ?d. &0 < d /\
!h. &0 < h /\ h < d
==> norm(i h x - (f:real^M->real^N) x) < e)}` THEN
SIMP_TAC[IN_ELIM_THM] THEN
REWRITE_TAC[LIM_SEQUENTIALLY] THEN
REWRITE_TAC[NOT_FORALL_THM; NOT_IMP; NOT_EXISTS_THM] THEN
MATCH_MP_TAC NEGLIGIBLE_SUBSET THEN
EXISTS_TAC
`UNIONS {{x | !d. &0 < d
==> ?h. &0 < h /\ h < d /\
inv(&k + &1) <= dist(i h x,(f:real^M->real^N) x)}
| k IN (:num)}` THEN
CONJ_TAC THENL
[ALL_TAC;
REWRITE_TAC[SUBSET; IN_ELIM_THM; LEFT_IMP_EXISTS_THM] THEN
REWRITE_TAC[NOT_FORALL_THM; NOT_IMP; LEFT_IMP_EXISTS_THM] THEN
MAP_EVERY X_GEN_TAC [`y:real^M`; `e:real`] THEN STRIP_TAC THEN
REWRITE_TAC[SIMPLE_IMAGE; UNIONS_IMAGE] THEN
REWRITE_TAC[IN_ELIM_THM; IN_UNIV] THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [REAL_ARCH_INV]) THEN
MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `k:num` THEN DISCH_TAC THEN
X_GEN_TAC `d:real` THEN DISCH_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPEC `d:real`) THEN
ASM_REWRITE_TAC[NOT_FORALL_THM; NOT_IMP; REAL_NOT_LT] THEN
MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `h:real` THEN
DISCH_THEN(CONJUNCTS_THEN2 STRIP_ASSUME_TAC MP_TAC) THEN
ASM_REWRITE_TAC[dist] THEN
MATCH_MP_TAC (REWRITE_RULE[IMP_CONJ] REAL_LE_TRANS) THEN
MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `inv(&k)` THEN
CONJ_TAC THENL [ALL_TAC; ASM_REAL_ARITH_TAC] THEN
MATCH_MP_TAC REAL_LE_INV2 THEN
ASM_REWRITE_TAC[REAL_OF_NUM_ADD; REAL_OF_NUM_LE; REAL_OF_NUM_LT] THEN
ASM_ARITH_TAC] THEN
MATCH_MP_TAC NEGLIGIBLE_COUNTABLE_UNIONS THEN
X_GEN_TAC `jj:num` THEN
SUBGOAL_THEN `&0 < inv(&jj + &1)` MP_TAC THENL
[REWRITE_TAC[REAL_LT_INV_EQ] THEN REAL_ARITH_TAC;
SPEC_TAC(`inv(&jj + &1)`,`mu:real`) THEN GEN_TAC THEN DISCH_TAC] THEN
ONCE_REWRITE_TAC[NEGLIGIBLE_ON_INTERVALS] THEN
MAP_EVERY X_GEN_TAC [`a:real^M`; `b:real^M`] THEN
ASM_CASES_TAC `negligible(interval[a:real^M,b])` THENL
[ASM_MESON_TAC[NEGLIGIBLE_SUBSET; INTER_SUBSET]; ALL_TAC] THEN
RULE_ASSUM_TAC(REWRITE_RULE[NEGLIGIBLE_INTERVAL]) THEN
RULE_ASSUM_TAC(REWRITE_RULE[INTERVAL_NE_EMPTY]) THEN
REWRITE_TAC[NEGLIGIBLE_OUTER_LE] THEN
X_GEN_TAC `e:real` THEN DISCH_TAC THEN
MP_TAC(ISPECL [`f:real^M->real^N`; `a - vec 1:real^M`; `b + vec 1:real^M`]
HENSTOCK_LEMMA) THEN
ANTS_TAC THENL
[ASM_MESON_TAC[INTEGRABLE_ON_SUBINTERVAL; SUBSET_UNIV]; ALL_TAC] THEN
DISCH_THEN(MP_TAC o SPEC `(e * mu) / &2 / &6 pow (dimindex(:M))`) THEN
ASM_SIMP_TAC[REAL_HALF; REAL_LT_DIV; REAL_LT_MUL;
REAL_POW_LT; REAL_OF_NUM_LT; ARITH] THEN
DISCH_THEN(X_CHOOSE_THEN `g:real^M->real^M->bool` STRIP_ASSUME_TAC) THEN
REWRITE_TAC[SET_RULE `{x | P x} INTER s = {x | x IN s /\ P x}`] THEN
ABBREV_TAC
`E = {x | x IN interval[a,b] /\
!d. &0 < d
==> ?h. &0 < h /\ h < d /\
mu <= dist(i h x,(f:real^M->real^N) x)}` THEN
SUBGOAL_THEN
`!x. x IN E
==> ?h. &0 < h /\
(box h x:real^M->bool) SUBSET (g x) /\
(box h x:real^M->bool) SUBSET interval[a - vec 1,b + vec 1] /\
mu <= dist(i h x,(f:real^M->real^N) x)`
MP_TAC THENL
[X_GEN_TAC `x:real^M` THEN EXPAND_TAC "E" THEN REWRITE_TAC[IN_ELIM_THM] THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [gauge]) THEN
DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC o SPEC `x:real^M`) THEN
REWRITE_TAC[OPEN_CONTAINS_BALL] THEN
DISCH_THEN(MP_TAC o SPEC `x:real^M`) THEN ASM_REWRITE_TAC[] THEN
DISCH_THEN(X_CHOOSE_THEN `d:real` STRIP_ASSUME_TAC) THEN
DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC
(MP_TAC o SPEC `min (&1) (d / &(dimindex(:M)))`)) THEN
REWRITE_TAC[REAL_LT_MIN; REAL_LT_01; GSYM CONJ_ASSOC] THEN
ASM_SIMP_TAC[REAL_LT_DIV; DIMINDEX_GE_1; LE_1; REAL_OF_NUM_LT] THEN
MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `h:real` THEN
STRIP_TAC THEN ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
[MATCH_MP_TAC SUBSET_TRANS THEN
EXISTS_TAC `ball(x:real^M,d)` THEN ASM_REWRITE_TAC[] THEN
EXPAND_TAC "box" THEN
REWRITE_TAC[SUBSET; IN_INTERVAL; IN_BALL] THEN
X_GEN_TAC `y:real^M` THEN
REWRITE_TAC[VECTOR_SUB_COMPONENT; VECTOR_ADD_COMPONENT; dist;
VECTOR_MUL_COMPONENT; VEC_COMPONENT; REAL_MUL_RID] THEN
DISCH_TAC THEN MATCH_MP_TAC REAL_LET_TRANS THEN
EXISTS_TAC `sum(1..dimindex(:M)) (\i. abs((x - y:real^M)$i))` THEN
REWRITE_TAC[NORM_LE_L1] THEN MATCH_MP_TAC SUM_BOUND_LT_GEN THEN
REWRITE_TAC[FINITE_NUMSEG; NUMSEG_EMPTY; IN_NUMSEG] THEN
SIMP_TAC[NOT_LT; DIMINDEX_GE_1; CARD_NUMSEG_1; VECTOR_SUB_COMPONENT] THEN
X_GEN_TAC `i:num` THEN STRIP_TAC THEN
REPEAT(FIRST_X_ASSUM(MP_TAC o SPEC `i:num`)) THEN
ASM_REWRITE_TAC[] THEN ASM_REAL_ARITH_TAC;
UNDISCH_TAC `(x:real^M) IN interval[a,b]` THEN
EXPAND_TAC "box" THEN REWRITE_TAC[SUBSET; IN_INTERVAL] THEN
DISCH_THEN(fun th -> X_GEN_TAC `y:real^M` THEN MP_TAC th) THEN
REWRITE_TAC[IMP_IMP; AND_FORALL_THM] 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
REWRITE_TAC[VECTOR_SUB_COMPONENT; VECTOR_ADD_COMPONENT; dist;
VECTOR_MUL_COMPONENT; VEC_COMPONENT; REAL_MUL_RID] THEN
ASM_REAL_ARITH_TAC];
ALL_TAC] THEN
GEN_REWRITE_TAC (LAND_CONV o TOP_DEPTH_CONV) [RIGHT_IMP_EXISTS_THM] THEN
REWRITE_TAC[SKOLEM_THM; LEFT_IMP_EXISTS_THM] THEN
X_GEN_TAC `uv:real^M->real` THEN
REWRITE_TAC[TAUT `(a ==> b /\ c) <=> (a ==> b) /\ (a ==> c)`] THEN
REWRITE_TAC[FORALL_AND_THM] THEN STRIP_TAC THEN
MP_TAC(ISPECL [`a:real^M`; `b:real^M`; `E:real^M->bool`;
`\x:real^M. if x IN E then ball(x,uv x) else g(x)`]
COVERING_LEMMA) THEN
REWRITE_TAC[] THEN ANTS_TAC THENL
[ASM_REWRITE_TAC[INTERVAL_NE_EMPTY] THEN CONJ_TAC THENL
[EXPAND_TAC "E" THEN SET_TAC[]; ALL_TAC] THEN
REWRITE_TAC[gauge] THEN GEN_TAC THEN
COND_CASES_TAC THEN ASM_SIMP_TAC[OPEN_BALL; CENTRE_IN_BALL] THEN
RULE_ASSUM_TAC(REWRITE_RULE[gauge]) THEN ASM_REWRITE_TAC[];
ALL_TAC] THEN
DISCH_THEN(X_CHOOSE_TAC `D:(real^M->bool)->bool`) THEN
EXISTS_TAC `UNIONS D:real^M->bool` THEN ASM_REWRITE_TAC[] THEN
SUBGOAL_THEN
`measurable(UNIONS D:real^M->bool) /\
measure(UNIONS D) <= measure(interval[a:real^M,b])`
STRIP_ASSUME_TAC THENL
[MATCH_MP_TAC MEASURE_COUNTABLE_UNIONS_LE_STRONG_GEN THEN
ASM_REWRITE_TAC[] THEN
CONJ_TAC THENL [ASM_MESON_TAC[SUBSET; MEASURABLE_INTERVAL]; ALL_TAC] THEN
REPEAT STRIP_TAC THEN MATCH_MP_TAC MEASURE_SUBSET THEN
REWRITE_TAC[MEASURABLE_INTERVAL] THEN
CONJ_TAC THENL [ALL_TAC; ASM SET_TAC[]] THEN
MATCH_MP_TAC MEASURABLE_UNIONS THEN
ASM_MESON_TAC[SUBSET; MEASURABLE_INTERVAL];
ALL_TAC] THEN
ASM_REWRITE_TAC[] THEN
SUBGOAL_THEN
`?d. d SUBSET D /\ FINITE d /\
measure(UNIONS D:real^M->bool) <= &2 * measure(UNIONS d)`
STRIP_ASSUME_TAC THENL
[ASM_CASES_TAC `measure(UNIONS D:real^M->bool) = &0` THENL
[EXISTS_TAC `{}:(real^M->bool)->bool` THEN
ASM_REWRITE_TAC[FINITE_EMPTY; EMPTY_SUBSET; MEASURE_EMPTY; UNIONS_0] THEN
CONV_TAC REAL_RAT_REDUCE_CONV;
MP_TAC(ISPECL [`D:(real^M->bool)->bool`; `measure(interval[a:real^M,b])`;
`measure(UNIONS D:real^M->bool) / &2`]
MEASURE_COUNTABLE_UNIONS_APPROACHABLE) THEN
ASM_REWRITE_TAC[] THEN ANTS_TAC THENL
[ASM_SIMP_TAC[MEASURABLE_MEASURE_POS_LT; REAL_HALF] THEN
ASM_SIMP_TAC[GSYM MEASURABLE_MEASURE_EQ_0] THEN
CONJ_TAC THENL [ASM_MESON_TAC[MEASURABLE_INTERVAL]; ALL_TAC] THEN
REPEAT STRIP_TAC THEN MATCH_MP_TAC MEASURE_SUBSET THEN
REPEAT(CONJ_TAC THENL
[ASM_MESON_TAC[SUBSET; MEASURABLE_INTERVAL; MEASURABLE_UNIONS];
ALL_TAC]) THEN
ASM SET_TAC[];
MATCH_MP_TAC MONO_EXISTS THEN SIMP_TAC[] THEN REAL_ARITH_TAC]];
ALL_TAC] THEN
FIRST_ASSUM(MP_TAC o el 3 o CONJUNCTS) THEN
REWRITE_TAC[RIGHT_IMP_EXISTS_THM; SKOLEM_THM] THEN
ONCE_REWRITE_TAC[TAUT `a /\ b <=> ~(a ==> ~b)`] THEN
SIMP_TAC[IN_INTER] THEN REWRITE_TAC[NOT_IMP; GSYM CONJ_ASSOC] THEN
DISCH_THEN(X_CHOOSE_TAC `tag:(real^M->bool)->real^M`) THEN
FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH
`D <= &2 * d ==> d <= e / &2 ==> D <= e`)) THEN
MP_TAC(ISPEC
`IMAGE (\k:real^M->bool. (box2:real->real^M->real^M->bool)
(uv(tag k):real) ((tag k:real^M))) d`
AUSTIN_LEMMA) THEN
ASM_SIMP_TAC[FINITE_IMAGE; FORALL_IN_IMAGE] THEN ANTS_TAC THENL
[X_GEN_TAC `k:real^M->bool` THEN DISCH_TAC THEN EXPAND_TAC "box2" THEN
EXISTS_TAC `&2 * uv((tag:(real^M->bool)->real^M) k):real` THEN
EXISTS_TAC `(tag:(real^M->bool)->real^M) k - uv(tag k) % vec 1:real^M` THEN
EXISTS_TAC `(tag:(real^M->bool)->real^M) k + uv(tag k) % vec 1:real^M` THEN
REWRITE_TAC[VECTOR_SUB_COMPONENT; VECTOR_ADD_COMPONENT; dist;
VECTOR_MUL_COMPONENT; VEC_COMPONENT; REAL_MUL_RID] THEN
ASM_REAL_ARITH_TAC;
ALL_TAC] THEN
REWRITE_TAC[EXISTS_SUBSET_IMAGE; real_ge] THEN
SIMP_TAC[REAL_LE_LDIV_EQ; REAL_POW_LT; REAL_OF_NUM_LT; ARITH] THEN
DISCH_THEN(X_CHOOSE_THEN `p:(real^M->bool)->bool` MP_TAC) THEN
REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
MATCH_MP_TAC(REAL_ARITH
`d <= d' /\ p <= e ==> d' <= p ==> d <= e`) THEN
CONJ_TAC THENL
[MATCH_MP_TAC MEASURE_SUBSET THEN REPEAT CONJ_TAC THENL
[MATCH_MP_TAC MEASURABLE_UNIONS THEN
ASM_MESON_TAC[SUBSET; MEASURABLE_INTERVAL];
MATCH_MP_TAC MEASURABLE_UNIONS THEN
ASM_SIMP_TAC[FINITE_IMAGE; FORALL_IN_IMAGE] THEN
EXPAND_TAC "box2" THEN REWRITE_TAC[MEASURABLE_INTERVAL];
REWRITE_TAC[SUBSET; IN_UNIONS; EXISTS_IN_IMAGE] THEN
X_GEN_TAC `z:real^M` THEN MATCH_MP_TAC MONO_EXISTS THEN
X_GEN_TAC `k:real^M->bool` THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
UNDISCH_TAC `(z:real^M) IN k` THEN SPEC_TAC(`z:real^M`,`z:real^M`) THEN
REWRITE_TAC[GSYM SUBSET] THEN MATCH_MP_TAC SUBSET_TRANS THEN
EXISTS_TAC `ball(tag k:real^M,uv(tag(k:real^M->bool)))` THEN
CONJ_TAC THENL [ASM_MESON_TAC[SUBSET]; ALL_TAC] THEN
EXPAND_TAC "box2" THEN REWRITE_TAC[SUBSET; IN_BALL; IN_INTERVAL] THEN
X_GEN_TAC `z:real^M` THEN REWRITE_TAC[dist] THEN DISCH_TAC THEN
REWRITE_TAC[VECTOR_SUB_COMPONENT; VECTOR_ADD_COMPONENT; dist;
VECTOR_MUL_COMPONENT; VEC_COMPONENT; REAL_MUL_RID] THEN
SIMP_TAC[REAL_ARITH `x - h <= y /\ y <= x + h <=> abs(x - y) <= h`] THEN
REWRITE_TAC[GSYM VECTOR_SUB_COMPONENT] THEN
ASM_MESON_TAC[COMPONENT_LE_NORM; REAL_LT_IMP_LE; REAL_LE_TRANS]];
ALL_TAC] THEN
MATCH_MP_TAC REAL_LE_TRANS THEN
EXISTS_TAC `measure(UNIONS (IMAGE (\k:real^M->bool.
(box:real->real^M->real^M->bool)
(uv(tag k):real) ((tag k:real^M))) p)) *
&6 pow dimindex (:M)` THEN
CONJ_TAC THENL
[SUBGOAL_THEN
`!box. IMAGE (\k:real^M->bool. (box:real->real^M->real^M->bool)
(uv(tag k):real) ((tag k:real^M))) p =
IMAGE (\t. box (uv t) t) (IMAGE tag p)`
(fun th -> REWRITE_TAC[th])
THENL [REWRITE_TAC[GSYM IMAGE_o; o_DEF]; ALL_TAC] THEN
W(MP_TAC o PART_MATCH (lhs o rand) MEASURE_NEGLIGIBLE_UNIONS_IMAGE o
lhand o rand o snd) THEN
W(MP_TAC o PART_MATCH (lhs o rand) MEASURE_NEGLIGIBLE_UNIONS_IMAGE o
lhand o lhand o rand o snd) THEN
MATCH_MP_TAC(TAUT
`fp /\ (mb /\ mb') /\ (db /\ db') /\ (m1 /\ m2 ==> p)
==> (fp /\ mb /\ db ==> m1) ==> (fp /\ mb' /\ db' ==> m2) ==> p`) THEN
SUBGOAL_THEN `FINITE(p:(real^M->bool)->bool)` ASSUME_TAC THENL
[ASM_MESON_TAC[FINITE_SUBSET]; ASM_SIMP_TAC[FINITE_IMAGE]] THEN
ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
[MAP_EVERY EXPAND_TAC ["box"; "box2"] THEN
REWRITE_TAC[MEASURABLE_INTERVAL];
ALL_TAC] THEN
CONJ_TAC THENL
[REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM; FORALL_IN_IMAGE] THEN
REWRITE_TAC[IMP_IMP; RIGHT_IMP_FORALL_THM; AND_FORALL_THM] THEN
MAP_EVERY X_GEN_TAC [`k1:real^M->bool`; `k2:real^M->bool`] THEN
MATCH_MP_TAC(TAUT
`(q ==> r) /\ (p ==> q) ==> (p ==> q) /\ (p ==> r)`) THEN
CONJ_TAC THENL
[MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ_ALT] NEGLIGIBLE_SUBSET) THEN
MATCH_MP_TAC(SET_RULE
`s SUBSET s' /\ t SUBSET t' ==> (s INTER t) SUBSET (s' INTER t')`) THEN
CONJ_TAC THEN MAP_EVERY EXPAND_TAC ["box"; "box2"] THEN
REWRITE_TAC[SUBSET_INTERVAL] THEN
REWRITE_TAC[VECTOR_SUB_COMPONENT; VECTOR_ADD_COMPONENT; dist;
VECTOR_MUL_COMPONENT; VEC_COMPONENT; REAL_MUL_RID] 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 REAL_ARITH_TAC;
ALL_TAC] THEN
STRIP_TAC THEN
MATCH_MP_TAC(MESON[NEGLIGIBLE_EMPTY] `s = {} ==> negligible s`) THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [pairwise]) THEN
REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM; FORALL_IN_IMAGE] THEN
DISCH_THEN(MP_TAC o SPEC `k1:real^M->bool`) THEN
ASM_REWRITE_TAC[] THEN
DISCH_THEN(MP_TAC o SPEC `k2:real^M->bool`) THEN
ASM_REWRITE_TAC[] THEN ANTS_TAC THENL
[EXPAND_TAC "box2" THEN REWRITE_TAC[GSYM SUBSET_ANTISYM_EQ] THEN
REWRITE_TAC[SUBSET_INTERVAL] THEN
REWRITE_TAC[VECTOR_SUB_COMPONENT; VECTOR_ADD_COMPONENT; dist;
VECTOR_MUL_COMPONENT; VEC_COMPONENT; REAL_MUL_RID] THEN
REWRITE_TAC[REAL_ARITH `x - e <= x + e <=> &0 <= e`] THEN
SUBGOAL_THEN `&0 <= uv((tag:(real^M->bool)->real^M) k1) /\
&0 <= uv((tag:(real^M->bool)->real^M) k2)`
STRIP_ASSUME_TAC THENL
[ASM_MESON_TAC[SUBSET; REAL_LT_IMP_LE]; ASM_REWRITE_TAC[]] THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE RAND_CONV [CART_EQ]) THEN
MATCH_MP_TAC MONO_NOT THEN REWRITE_TAC[AND_FORALL_THM] 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 REAL_ARITH_TAC;
SET_TAC[]];
ALL_TAC] THEN
DISCH_THEN(CONJUNCTS_THEN SUBST1_TAC) THEN
REWRITE_TAC[GSYM SUM_RMUL] THEN
MATCH_MP_TAC REAL_EQ_IMP_LE THEN MATCH_MP_TAC SUM_EQ THEN
X_GEN_TAC `t:real^M` THEN DISCH_THEN(K ALL_TAC) THEN
SUBST1_TAC(REAL_ARITH `&6 = &2 * &3`) THEN
REWRITE_TAC[REAL_POW_MUL; REAL_MUL_ASSOC] THEN
AP_THM_TAC THEN AP_TERM_TAC THEN
MAP_EVERY EXPAND_TAC ["box"; "box2"] THEN
REWRITE_TAC[MEASURE_INTERVAL; CONTENT_CLOSED_INTERVAL_CASES] THEN
REWRITE_TAC[VECTOR_SUB_COMPONENT; VECTOR_ADD_COMPONENT; dist;
VECTOR_MUL_COMPONENT; VEC_COMPONENT; REAL_MUL_RID] THEN
REWRITE_TAC[REAL_ARITH `a <= a + x <=> &0 <= x`;
REAL_ARITH `a - x <= a + x <=> &0 <= x`] THEN
COND_CASES_TAC THEN REWRITE_TAC[REAL_MUL_LZERO] THEN
REWRITE_TAC[REAL_ARITH `(t + h) - (t - h):real = &2 * h`;
REAL_ARITH `(t + h) - t:real = h`] THEN
REWRITE_TAC[PRODUCT_MUL_NUMSEG; PRODUCT_CONST_NUMSEG] THEN
REWRITE_TAC[ADD_SUB; REAL_MUL_AC];
ALL_TAC] THEN
SIMP_TAC[GSYM REAL_LE_RDIV_EQ; REAL_POW_LT; REAL_OF_NUM_LT; ARITH] THEN
SUBGOAL_THEN `FINITE(p:(real^M->bool)->bool)` ASSUME_TAC THENL
[ASM_MESON_TAC[FINITE_SUBSET]; ALL_TAC] THEN
MATCH_MP_TAC REAL_LE_LCANCEL_IMP THEN
EXISTS_TAC `mu:real` THEN ASM_REWRITE_TAC[] THEN
FIRST_X_ASSUM(MP_TAC o SPEC
`IMAGE (\k. (tag:(real^M->bool)->real^M) k,
(box(uv(tag k):real) (tag k):real^M->bool)) p`) THEN
ANTS_TAC THENL
[REWRITE_TAC[tagged_partial_division_of; fine] THEN
REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN
REWRITE_TAC[IN_IMAGE; PAIR_EQ] THEN
REWRITE_TAC[MESON[]
`(!x j. (?k. (x = tag k /\ j = g k) /\ k IN d) ==> P x j) <=>
(!k. k IN d ==> P (tag k) (g k))`] THEN
ASM_SIMP_TAC[FINITE_IMAGE] THEN REPEAT CONJ_TAC THENL
[X_GEN_TAC `k:real^M->bool` THEN DISCH_TAC THEN REPEAT CONJ_TAC THENL
[EXPAND_TAC "box" THEN REWRITE_TAC[IN_INTERVAL] THEN
REWRITE_TAC[VECTOR_SUB_COMPONENT; VECTOR_ADD_COMPONENT; dist;
VECTOR_MUL_COMPONENT; VEC_COMPONENT; REAL_MUL_RID] THEN
GEN_TAC THEN STRIP_TAC THEN MATCH_MP_TAC(REAL_ARITH
`&0 < u ==> x <= x /\ x <= x + u`) THEN ASM_MESON_TAC[SUBSET];
ASM_MESON_TAC[SUBSET];
EXPAND_TAC "box" THEN MESON_TAC[]];
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [pairwise]) THEN
REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM; FORALL_IN_IMAGE] THEN
MATCH_MP_TAC MONO_FORALL THEN X_GEN_TAC `k1:real^M->bool` THEN
ASM_CASES_TAC `(k1:real^M->bool) IN p` THEN ASM_REWRITE_TAC[] THEN
MATCH_MP_TAC MONO_FORALL THEN X_GEN_TAC `k2:real^M->bool` THEN
ASM_CASES_TAC `(k2:real^M->bool) IN p` THEN ASM_REWRITE_TAC[] THEN
ASM_CASES_TAC `(tag:(real^M->bool)->real^M) k1 = tag k2` THEN
ASM_REWRITE_TAC[] THEN ANTS_TAC THENL
[EXPAND_TAC "box2" THEN REWRITE_TAC[GSYM SUBSET_ANTISYM_EQ] THEN
REWRITE_TAC[SUBSET_INTERVAL] THEN
REWRITE_TAC[VECTOR_SUB_COMPONENT; VECTOR_ADD_COMPONENT; dist;
VECTOR_MUL_COMPONENT; VEC_COMPONENT; REAL_MUL_RID] THEN
REWRITE_TAC[REAL_ARITH `x - e <= x + e <=> &0 <= e`] THEN
SUBGOAL_THEN `&0 <= uv((tag:(real^M->bool)->real^M) k1) /\
&0 <= uv((tag:(real^M->bool)->real^M) k2)`
STRIP_ASSUME_TAC THENL
[ASM_MESON_TAC[SUBSET; REAL_LT_IMP_LE]; ASM_REWRITE_TAC[]] THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE RAND_CONV [CART_EQ]) THEN
MATCH_MP_TAC MONO_NOT THEN REWRITE_TAC[AND_FORALL_THM] 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 REAL_ARITH_TAC;
MATCH_MP_TAC(SET_RULE
`i1 SUBSET s1 /\ i2 SUBSET s2
==> DISJOINT s1 s2 ==> i1 INTER i2 = {}`) THEN
CONJ_TAC THEN MATCH_MP_TAC(MESON[INTERIOR_SUBSET; SUBSET_TRANS]
`s SUBSET t ==> interior s SUBSET t`) THEN
MAP_EVERY EXPAND_TAC ["box"; "box2"] THEN
REWRITE_TAC[SUBSET_INTERVAL] THEN
REWRITE_TAC[VECTOR_SUB_COMPONENT; VECTOR_ADD_COMPONENT; dist;
VECTOR_MUL_COMPONENT; VEC_COMPONENT; REAL_MUL_RID] 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 REAL_ARITH_TAC];
ASM_MESON_TAC[SUBSET]];
ALL_TAC] THEN
MATCH_MP_TAC(REAL_ARITH `e = e' /\ y <= x ==> x < e ==> y <= e'`) THEN
CONJ_TAC THENL [REWRITE_TAC[real_div; REAL_MUL_AC]; ALL_TAC] THEN
ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN ASM_SIMP_TAC[GSYM REAL_LE_RDIV_EQ] THEN
W(MP_TAC o PART_MATCH (lhand o rand) MEASURE_UNIONS_LE o lhand o snd) THEN
ANTS_TAC THENL
[ASM_SIMP_TAC[FINITE_IMAGE; FORALL_IN_IMAGE] THEN
EXPAND_TAC "box" THEN REWRITE_TAC[MEASURABLE_INTERVAL];
ALL_TAC] THEN
MATCH_MP_TAC(REAL_ARITH `a' <= e ==> a <= a' ==> a <= e`) THEN
ASM_SIMP_TAC[REAL_LE_RDIV_EQ; GSYM SUM_RMUL] THEN
MATCH_MP_TAC SUM_LE_INCLUDED THEN
ASM_SIMP_TAC[FORALL_IN_IMAGE; RIGHT_EXISTS_AND_THM; FINITE_IMAGE] THEN
REWRITE_TAC[NORM_POS_LE; EXISTS_IN_IMAGE] THEN
EXISTS_TAC `SND:real^M#(real^M->bool)->real^M->bool` THEN
X_GEN_TAC `k:real^M->bool` THEN DISCH_TAC THEN
EXISTS_TAC `k:real^M->bool` THEN ASM_REWRITE_TAC[] THEN
SUBGOAL_THEN
`&0 < uv(tag(k:real^M->bool):real^M):real` ASSUME_TAC
THENL [ASM_MESON_TAC[SUBSET]; ALL_TAC] THEN
SUBGOAL_THEN
`&0 < measure(box(uv(tag(k:real^M->bool):real^M):real) (tag k):real^M->bool)`
MP_TAC THENL
[EXPAND_TAC "box" THEN
REWRITE_TAC[MEASURE_INTERVAL; CONTENT_CLOSED_INTERVAL_CASES] THEN
REWRITE_TAC[VECTOR_SUB_COMPONENT; VECTOR_ADD_COMPONENT; dist;
VECTOR_MUL_COMPONENT; VEC_COMPONENT; REAL_MUL_RID] THEN
ASM_SIMP_TAC[REAL_ARITH `&0 < x ==> a <= a + x`] THEN
MATCH_MP_TAC PRODUCT_POS_LT_NUMSEG THEN
REWRITE_TAC[] THEN ASM_REAL_ARITH_TAC;
ALL_TAC] THEN
ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN SIMP_TAC[GSYM REAL_LE_RDIV_EQ] THEN
DISCH_THEN(fun th ->
GEN_REWRITE_TAC (funpow 2 RAND_CONV)
[MATCH_MP(REAL_ARITH `&0 < x ==> x = abs x`) th] THEN
ASSUME_TAC th) THEN
REWRITE_TAC[real_div; GSYM REAL_ABS_INV] THEN
ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN REWRITE_TAC[GSYM NORM_MUL] THEN
SUBGOAL_THEN
`mu <= dist(i (uv(tag(k:real^M->bool):real^M):real) (tag k):real^N,
f(tag k))`
MP_TAC THENL [ASM_MESON_TAC[SUBSET]; ALL_TAC] THEN
MATCH_MP_TAC(REAL_ARITH `x = y ==> m <= x ==> m <= y`) THEN
ONCE_REWRITE_TAC[DIST_SYM] THEN EXPAND_TAC "i" THEN
REWRITE_TAC[dist; VECTOR_SUB_LDISTRIB] THEN
UNDISCH_TAC
`&0 < measure(box(uv(tag(k:real^M->bool):real^M):real)
(tag k):real^M->bool)` THEN
EXPAND_TAC "box" THEN REWRITE_TAC[MEASURE_INTERVAL] THEN
SIMP_TAC[VECTOR_MUL_ASSOC; REAL_LT_IMP_NZ; REAL_MUL_LINV] THEN
REWRITE_TAC[VECTOR_MUL_LID]);;
"box"] THEN REWRITE_TAC[]] THEN
EXISTS_TAC
`{x | ~(!e. &0 < e
==> ?d. &0 < d /\
!h. &0 < h /\ h < d
==> norm(i h x - (f:real^M->real^N) x) < e)}` THEN
SIMP_TAC[IN_ELIM_THM] THEN
REWRITE_TAC[LIM_SEQUENTIALLY] THEN
REWRITE_TAC[NOT_FORALL_THM; NOT_IMP; NOT_EXISTS_THM] THEN
MATCH_MP_TAC NEGLIGIBLE_SUBSET THEN
EXISTS_TAC
`UNIONS {{x | !d. &0 < d
==> ?h. &0 < h /\ h < d /\
inv(&k + &1) <= dist(i h x,(f:real^M->real^N) x)}
| k IN (:num)}` THEN
CONJ_TAC THENL
[ALL_TAC;
REWRITE_TAC[SUBSET; IN_ELIM_THM; LEFT_IMP_EXISTS_THM] THEN
REWRITE_TAC[NOT_FORALL_THM; NOT_IMP; LEFT_IMP_EXISTS_THM] THEN
MAP_EVERY X_GEN_TAC [`y:real^M`; `e:real`] THEN STRIP_TAC THEN
REWRITE_TAC[SIMPLE_IMAGE; UNIONS_IMAGE] THEN
REWRITE_TAC[IN_ELIM_THM; IN_UNIV] THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [REAL_ARCH_INV]) THEN
MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `k:num` THEN DISCH_TAC THEN
X_GEN_TAC `d:real` THEN DISCH_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPEC `d:real`) THEN
ASM_REWRITE_TAC[NOT_FORALL_THM; NOT_IMP; REAL_NOT_LT] THEN
MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `h:real` THEN
DISCH_THEN(CONJUNCTS_THEN2 STRIP_ASSUME_TAC MP_TAC) THEN
ASM_REWRITE_TAC[dist] THEN
MATCH_MP_TAC (REWRITE_RULE[IMP_CONJ] REAL_LE_TRANS) THEN
MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `inv(&k)` THEN
CONJ_TAC THENL [ALL_TAC; ASM_REAL_ARITH_TAC] THEN
MATCH_MP_TAC REAL_LE_INV2 THEN
ASM_REWRITE_TAC[REAL_OF_NUM_ADD; REAL_OF_NUM_LE; REAL_OF_NUM_LT] THEN
ASM_ARITH_TAC] THEN
MATCH_MP_TAC NEGLIGIBLE_COUNTABLE_UNIONS THEN
X_GEN_TAC `jj:num` THEN
SUBGOAL_THEN `&0 < inv(&jj + &1)` MP_TAC THENL
[REWRITE_TAC[REAL_LT_INV_EQ] THEN REAL_ARITH_TAC;
SPEC_TAC(`inv(&jj + &1)`,`mu:real`) THEN GEN_TAC THEN DISCH_TAC] THEN
ONCE_REWRITE_TAC[NEGLIGIBLE_ON_INTERVALS] THEN
MAP_EVERY X_GEN_TAC [`a:real^M`; `b:real^M`] THEN
ASM_CASES_TAC `negligible(interval[a:real^M,b])` THENL
[ASM_MESON_TAC[NEGLIGIBLE_SUBSET; INTER_SUBSET]; ALL_TAC] THEN
RULE_ASSUM_TAC(REWRITE_RULE[NEGLIGIBLE_INTERVAL]) THEN
RULE_ASSUM_TAC(REWRITE_RULE[INTERVAL_NE_EMPTY]) THEN
REWRITE_TAC[NEGLIGIBLE_OUTER_LE] THEN
X_GEN_TAC `e:real` THEN DISCH_TAC THEN
MP_TAC(ISPECL [`f:real^M->real^N`; `a - vec 1:real^M`; `b + vec 1:real^M`]
HENSTOCK_LEMMA) THEN
ANTS_TAC THENL
[ASM_MESON_TAC[INTEGRABLE_ON_SUBINTERVAL; SUBSET_UNIV]; ALL_TAC] THEN
DISCH_THEN(MP_TAC o SPEC `(e * mu) / &2 / &3 pow (dimindex(:M))`) THEN
ASM_SIMP_TAC[REAL_HALF; REAL_LT_DIV; REAL_LT_MUL;
REAL_POW_LT; REAL_OF_NUM_LT; ARITH] THEN
DISCH_THEN(X_CHOOSE_THEN `g:real^M->real^M->bool` STRIP_ASSUME_TAC) THEN
REWRITE_TAC[SET_RULE `{x | P x} INTER s = {x | x IN s /\ P x}`] THEN
ABBREV_TAC
`E = {x | x IN interval[a,b] /\
!d. &0 < d
==> ?h. &0 < h /\ h < d /\
mu <= dist(i h x,(f:real^M->real^N) x)}` THEN
SUBGOAL_THEN
`!x. x IN E
==> ?h. &0 < h /\
(box h x:real^M->bool) SUBSET (g x) /\
(box h x:real^M->bool) SUBSET interval[a - vec 1,b + vec 1] /\
mu <= dist(i h x,(f:real^M->real^N) x)`
MP_TAC THENL
[X_GEN_TAC `x:real^M` THEN EXPAND_TAC "E" THEN REWRITE_TAC[IN_ELIM_THM] THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [gauge]) THEN
DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC o SPEC `x:real^M`) THEN
REWRITE_TAC[OPEN_CONTAINS_BALL] THEN
DISCH_THEN(MP_TAC o SPEC `x:real^M`) THEN ASM_REWRITE_TAC[] THEN
DISCH_THEN(X_CHOOSE_THEN `d:real` STRIP_ASSUME_TAC) THEN
DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC
(MP_TAC o SPEC `min (&1) (d / &(dimindex(:M)))`)) THEN
REWRITE_TAC[REAL_LT_MIN; REAL_LT_01; GSYM CONJ_ASSOC] THEN
ASM_SIMP_TAC[REAL_LT_DIV; DIMINDEX_GE_1; LE_1; REAL_OF_NUM_LT] THEN
MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `h:real` THEN
STRIP_TAC THEN ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
[MATCH_MP_TAC SUBSET_TRANS THEN
EXISTS_TAC `ball(x:real^M,d)` THEN ASM_REWRITE_TAC[] THEN
EXPAND_TAC "box" THEN
REWRITE_TAC[SUBSET; IN_INTERVAL; IN_BALL] THEN
X_GEN_TAC `y:real^M` THEN
REWRITE_TAC[VECTOR_SUB_COMPONENT; VECTOR_ADD_COMPONENT; dist;
VECTOR_MUL_COMPONENT; VEC_COMPONENT; REAL_MUL_RID] THEN
SIMP_TAC[REAL_ARITH `x - h <= y /\ y <= x + h <=> abs(x - y) <= h`] THEN
DISCH_TAC THEN MATCH_MP_TAC REAL_LET_TRANS THEN
EXISTS_TAC `sum(1..dimindex(:M)) (\i. abs((x - y:real^M)$i))` THEN
REWRITE_TAC[NORM_LE_L1] THEN MATCH_MP_TAC SUM_BOUND_LT_GEN THEN
REWRITE_TAC[FINITE_NUMSEG; NUMSEG_EMPTY; IN_NUMSEG] THEN
SIMP_TAC[NOT_LT; DIMINDEX_GE_1; CARD_NUMSEG_1; VECTOR_SUB_COMPONENT] THEN
ASM_MESON_TAC[REAL_LET_TRANS];
UNDISCH_TAC `(x:real^M) IN interval[a,b]` THEN
EXPAND_TAC "box" THEN REWRITE_TAC[SUBSET; IN_INTERVAL] THEN
DISCH_THEN(fun th -> X_GEN_TAC `y:real^M` THEN MP_TAC th) THEN
REWRITE_TAC[IMP_IMP; AND_FORALL_THM] 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
REWRITE_TAC[VECTOR_SUB_COMPONENT; VECTOR_ADD_COMPONENT; dist;
VECTOR_MUL_COMPONENT; VEC_COMPONENT; REAL_MUL_RID] THEN
ASM_REAL_ARITH_TAC];
ALL_TAC] THEN
GEN_REWRITE_TAC (LAND_CONV o TOP_DEPTH_CONV) [RIGHT_IMP_EXISTS_THM] THEN
REWRITE_TAC[SKOLEM_THM; LEFT_IMP_EXISTS_THM] THEN
X_GEN_TAC `uv:real^M->real` THEN
REWRITE_TAC[TAUT `(a ==> b /\ c) <=> (a ==> b) /\ (a ==> c)`] THEN
REWRITE_TAC[FORALL_AND_THM] THEN STRIP_TAC THEN
MP_TAC(ISPECL [`a:real^M`; `b:real^M`; `E:real^M->bool`;
`\x:real^M. if x IN E then ball(x,uv x) else g(x)`]
COVERING_LEMMA) THEN
REWRITE_TAC[] THEN ANTS_TAC THENL
[ASM_REWRITE_TAC[INTERVAL_NE_EMPTY] THEN CONJ_TAC THENL
[EXPAND_TAC "E" THEN SET_TAC[]; ALL_TAC] THEN
REWRITE_TAC[gauge] THEN GEN_TAC THEN
COND_CASES_TAC THEN ASM_SIMP_TAC[OPEN_BALL; CENTRE_IN_BALL] THEN
RULE_ASSUM_TAC(REWRITE_RULE[gauge]) THEN ASM_REWRITE_TAC[];
ALL_TAC] THEN
DISCH_THEN(X_CHOOSE_TAC `D:(real^M->bool)->bool`) THEN
EXISTS_TAC `UNIONS D:real^M->bool` THEN ASM_REWRITE_TAC[] THEN
SUBGOAL_THEN
`measurable(UNIONS D:real^M->bool) /\
measure(UNIONS D) <= measure(interval[a:real^M,b])`
STRIP_ASSUME_TAC THENL
[MATCH_MP_TAC MEASURE_COUNTABLE_UNIONS_LE_STRONG_GEN THEN
ASM_REWRITE_TAC[] THEN
CONJ_TAC THENL [ASM_MESON_TAC[SUBSET; MEASURABLE_INTERVAL]; ALL_TAC] THEN
REPEAT STRIP_TAC THEN MATCH_MP_TAC MEASURE_SUBSET THEN
REWRITE_TAC[MEASURABLE_INTERVAL] THEN
CONJ_TAC THENL [ALL_TAC; ASM SET_TAC[]] THEN
MATCH_MP_TAC MEASURABLE_UNIONS THEN
ASM_MESON_TAC[SUBSET; MEASURABLE_INTERVAL];
ALL_TAC] THEN
ASM_REWRITE_TAC[] THEN
SUBGOAL_THEN
`?d. d SUBSET D /\ FINITE d /\
measure(UNIONS D:real^M->bool) <= &2 * measure(UNIONS d)`
STRIP_ASSUME_TAC THENL
[ASM_CASES_TAC `measure(UNIONS D:real^M->bool) = &0` THENL
[EXISTS_TAC `{}:(real^M->bool)->bool` THEN
ASM_REWRITE_TAC[FINITE_EMPTY; EMPTY_SUBSET; MEASURE_EMPTY; UNIONS_0] THEN
CONV_TAC REAL_RAT_REDUCE_CONV;
MP_TAC(ISPECL [`D:(real^M->bool)->bool`; `measure(interval[a:real^M,b])`;
`measure(UNIONS D:real^M->bool) / &2`]
MEASURE_COUNTABLE_UNIONS_APPROACHABLE) THEN
ASM_REWRITE_TAC[] THEN ANTS_TAC THENL
[ASM_SIMP_TAC[MEASURABLE_MEASURE_POS_LT; REAL_HALF] THEN
ASM_SIMP_TAC[GSYM MEASURABLE_MEASURE_EQ_0] THEN
CONJ_TAC THENL [ASM_MESON_TAC[MEASURABLE_INTERVAL]; ALL_TAC] THEN
REPEAT STRIP_TAC THEN MATCH_MP_TAC MEASURE_SUBSET THEN
REPEAT(CONJ_TAC THENL
[ASM_MESON_TAC[SUBSET; MEASURABLE_INTERVAL; MEASURABLE_UNIONS];
ALL_TAC]) THEN
ASM SET_TAC[];
MATCH_MP_TAC MONO_EXISTS THEN SIMP_TAC[] THEN REAL_ARITH_TAC]];
ALL_TAC] THEN
FIRST_ASSUM(MP_TAC o el 3 o CONJUNCTS) THEN
REWRITE_TAC[RIGHT_IMP_EXISTS_THM; SKOLEM_THM] THEN
ONCE_REWRITE_TAC[TAUT `a /\ b <=> ~(a ==> ~b)`] THEN
SIMP_TAC[IN_INTER] THEN REWRITE_TAC[NOT_IMP; GSYM CONJ_ASSOC] THEN
DISCH_THEN(X_CHOOSE_TAC `tag:(real^M->bool)->real^M`) THEN
FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH
`D <= &2 * d ==> d <= e / &2 ==> D <= e`)) THEN
MP_TAC(ISPEC
`IMAGE (\k:real^M->bool. (box:real->real^M->real^M->bool)
(uv(tag k):real) ((tag k:real^M))) d`
AUSTIN_LEMMA) THEN
ASM_SIMP_TAC[FINITE_IMAGE; FORALL_IN_IMAGE] THEN ANTS_TAC THENL
[X_GEN_TAC `k:real^M->bool` THEN DISCH_TAC THEN EXPAND_TAC "box" THEN
EXISTS_TAC `&2 * uv((tag:(real^M->bool)->real^M) k):real` THEN
EXISTS_TAC `(tag:(real^M->bool)->real^M) k - uv(tag k) % vec 1:real^M` THEN
EXISTS_TAC `(tag:(real^M->bool)->real^M) k + uv(tag k) % vec 1:real^M` THEN
REWRITE_TAC[VECTOR_SUB_COMPONENT; VECTOR_ADD_COMPONENT; dist;
VECTOR_MUL_COMPONENT; VEC_COMPONENT; REAL_MUL_RID] THEN
ASM_REAL_ARITH_TAC;
ALL_TAC] THEN
REWRITE_TAC[EXISTS_SUBSET_IMAGE; real_ge] THEN
SIMP_TAC[REAL_LE_LDIV_EQ; REAL_POW_LT; REAL_OF_NUM_LT; ARITH] THEN
DISCH_THEN(X_CHOOSE_THEN `p:(real^M->bool)->bool` MP_TAC) THEN
REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
MATCH_MP_TAC(REAL_ARITH
`d <= d' /\ p <= e ==> d' <= p ==> d <= e`) THEN
CONJ_TAC THENL
[MATCH_MP_TAC MEASURE_SUBSET THEN REPEAT CONJ_TAC THENL
[MATCH_MP_TAC MEASURABLE_UNIONS THEN
ASM_MESON_TAC[SUBSET; MEASURABLE_INTERVAL];
MATCH_MP_TAC MEASURABLE_UNIONS THEN
ASM_SIMP_TAC[FINITE_IMAGE; FORALL_IN_IMAGE] THEN
EXPAND_TAC "box" THEN REWRITE_TAC[MEASURABLE_INTERVAL];
REWRITE_TAC[SUBSET; IN_UNIONS; EXISTS_IN_IMAGE] THEN
X_GEN_TAC `z:real^M` THEN MATCH_MP_TAC MONO_EXISTS THEN
X_GEN_TAC `k:real^M->bool` THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
UNDISCH_TAC `(z:real^M) IN k` THEN SPEC_TAC(`z:real^M`,`z:real^M`) THEN
REWRITE_TAC[GSYM SUBSET] THEN MATCH_MP_TAC SUBSET_TRANS THEN
EXISTS_TAC `ball(tag k:real^M,uv(tag(k:real^M->bool)))` THEN
CONJ_TAC THENL [ASM_MESON_TAC[SUBSET]; ALL_TAC] THEN
EXPAND_TAC "box" THEN REWRITE_TAC[SUBSET; IN_BALL; IN_INTERVAL] THEN
X_GEN_TAC `z:real^M` THEN REWRITE_TAC[dist] THEN DISCH_TAC THEN
REWRITE_TAC[VECTOR_SUB_COMPONENT; VECTOR_ADD_COMPONENT; dist;
VECTOR_MUL_COMPONENT; VEC_COMPONENT; REAL_MUL_RID] THEN
SIMP_TAC[REAL_ARITH `x - h <= y /\ y <= x + h <=> abs(x - y) <= h`] THEN
REWRITE_TAC[GSYM VECTOR_SUB_COMPONENT] THEN
ASM_MESON_TAC[COMPONENT_LE_NORM; REAL_LT_IMP_LE; REAL_LE_TRANS]];
ALL_TAC] THEN
SIMP_TAC[GSYM REAL_LE_RDIV_EQ; REAL_POW_LT; REAL_OF_NUM_LT; ARITH] THEN
SUBGOAL_THEN `FINITE(p:(real^M->bool)->bool)` ASSUME_TAC THENL
[ASM_MESON_TAC[FINITE_SUBSET]; ALL_TAC] THEN
MATCH_MP_TAC REAL_LE_LCANCEL_IMP THEN
EXISTS_TAC `mu:real` THEN ASM_REWRITE_TAC[] THEN
FIRST_X_ASSUM(MP_TAC o SPEC
`IMAGE (\k. (tag:(real^M->bool)->real^M) k,
(box(uv(tag k):real) (tag k):real^M->bool)) p`) THEN
ANTS_TAC THENL
[REWRITE_TAC[tagged_partial_division_of; fine] THEN
REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN
REWRITE_TAC[IN_IMAGE; PAIR_EQ] THEN
REWRITE_TAC[MESON[]
`(!x j. (?k. (x = tag k /\ j = g k) /\ k IN d) ==> P x j) <=>
(!k. k IN d ==> P (tag k) (g k))`] THEN
ASM_SIMP_TAC[FINITE_IMAGE] THEN REPEAT CONJ_TAC THENL
[X_GEN_TAC `k:real^M->bool` THEN DISCH_TAC THEN REPEAT CONJ_TAC THENL
[EXPAND_TAC "box" THEN REWRITE_TAC[IN_INTERVAL] THEN
REWRITE_TAC[VECTOR_SUB_COMPONENT; VECTOR_ADD_COMPONENT; dist;
VECTOR_MUL_COMPONENT; VEC_COMPONENT; REAL_MUL_RID] THEN
GEN_TAC THEN STRIP_TAC THEN MATCH_MP_TAC(REAL_ARITH
`&0 < u ==> x - u <= x /\ x <= x + u`) THEN ASM_MESON_TAC[SUBSET];
ASM_MESON_TAC[SUBSET];
EXPAND_TAC "box" THEN MESON_TAC[]];
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [pairwise]) THEN
REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM; FORALL_IN_IMAGE] THEN
MATCH_MP_TAC MONO_FORALL THEN X_GEN_TAC `k1:real^M->bool` THEN
ASM_CASES_TAC `(k1:real^M->bool) IN p` THEN ASM_REWRITE_TAC[] THEN
MATCH_MP_TAC MONO_FORALL THEN X_GEN_TAC `k2:real^M->bool` THEN
ASM_CASES_TAC `(k2:real^M->bool) IN p` THEN ASM_REWRITE_TAC[] THEN
ASM_CASES_TAC `(tag:(real^M->bool)->real^M) k1 = tag k2` THEN
ASM_REWRITE_TAC[] THEN ANTS_TAC THENL
[EXPAND_TAC "box" THEN REWRITE_TAC[GSYM SUBSET_ANTISYM_EQ] THEN
REWRITE_TAC[SUBSET_INTERVAL] THEN
REWRITE_TAC[VECTOR_SUB_COMPONENT; VECTOR_ADD_COMPONENT; dist;
VECTOR_MUL_COMPONENT; VEC_COMPONENT; REAL_MUL_RID] THEN
REWRITE_TAC[REAL_ARITH `x - e <= x + e <=> &0 <= e`] THEN
SUBGOAL_THEN `&0 <= uv((tag:(real^M->bool)->real^M) k1) /\
&0 <= uv((tag:(real^M->bool)->real^M) k2)`
STRIP_ASSUME_TAC THENL
[ASM_MESON_TAC[SUBSET; REAL_LT_IMP_LE]; ASM_REWRITE_TAC[]] THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE RAND_CONV [CART_EQ]) THEN
MATCH_MP_TAC MONO_NOT THEN REWRITE_TAC[AND_FORALL_THM] 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 REAL_ARITH_TAC;
MATCH_MP_TAC(SET_RULE
`i1 SUBSET s1 /\ i2 SUBSET s2
==> DISJOINT s1 s2 ==> i1 INTER i2 = {}`) THEN
REWRITE_TAC[INTERIOR_SUBSET]];
ASM_MESON_TAC[SUBSET]];
ALL_TAC] THEN
MATCH_MP_TAC(REAL_ARITH `e = e' /\ y <= x ==> x < e ==> y <= e'`) THEN
CONJ_TAC THENL [REWRITE_TAC[real_div; REAL_MUL_AC]; ALL_TAC] THEN
ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN ASM_SIMP_TAC[GSYM REAL_LE_RDIV_EQ] THEN
W(MP_TAC o PART_MATCH (lhand o rand) MEASURE_UNIONS_LE o lhand o snd) THEN
ANTS_TAC THENL
[ASM_SIMP_TAC[FINITE_IMAGE; FORALL_IN_IMAGE] THEN
EXPAND_TAC "box" THEN REWRITE_TAC[MEASURABLE_INTERVAL];
ALL_TAC] THEN
MATCH_MP_TAC(REAL_ARITH `a' <= e ==> a <= a' ==> a <= e`) THEN
ASM_SIMP_TAC[REAL_LE_RDIV_EQ; GSYM SUM_RMUL] THEN
MATCH_MP_TAC SUM_LE_INCLUDED THEN
ASM_SIMP_TAC[FORALL_IN_IMAGE; RIGHT_EXISTS_AND_THM; FINITE_IMAGE] THEN
REWRITE_TAC[NORM_POS_LE; EXISTS_IN_IMAGE] THEN
EXISTS_TAC `SND:real^M#(real^M->bool)->real^M->bool` THEN
X_GEN_TAC `k:real^M->bool` THEN DISCH_TAC THEN
EXISTS_TAC `k:real^M->bool` THEN ASM_REWRITE_TAC[] THEN
SUBGOAL_THEN
`&0 < uv(tag(k:real^M->bool):real^M):real` ASSUME_TAC
THENL [ASM_MESON_TAC[SUBSET]; ALL_TAC] THEN
SUBGOAL_THEN
`&0 < measure(box(uv(tag(k:real^M->bool):real^M):real) (tag
k):real^M->bool)`
MP_TAC THENL
[EXPAND_TAC "box" THEN
REWRITE_TAC[MEASURE_INTERVAL; CONTENT_CLOSED_INTERVAL_CASES] THEN
REWRITE_TAC[VECTOR_SUB_COMPONENT; VECTOR_ADD_COMPONENT; dist;
VECTOR_MUL_COMPONENT; VEC_COMPONENT; REAL_MUL_RID] THEN
ASM_SIMP_TAC[REAL_ARITH `&0 < x ==> a - x <= a + x`] THEN
MATCH_MP_TAC PRODUCT_POS_LT_NUMSEG THEN
REWRITE_TAC[] THEN ASM_REAL_ARITH_TAC;
ALL_TAC] THEN
ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN SIMP_TAC[GSYM REAL_LE_RDIV_EQ] THEN
DISCH_THEN(fun th ->
GEN_REWRITE_TAC (funpow 2 RAND_CONV)
[MATCH_MP(REAL_ARITH `&0 < x ==> x = abs x`) th] THEN
ASSUME_TAC th) THEN
REWRITE_TAC[real_div; GSYM REAL_ABS_INV] THEN
ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN REWRITE_TAC[GSYM NORM_MUL] THEN
SUBGOAL_THEN
`mu <= dist(i (uv(tag(k:real^M->bool):real^M):real) (tag k):real^N,
f(tag k))`
MP_TAC THENL [ASM_MESON_TAC[SUBSET]; ALL_TAC] THEN
MATCH_MP_TAC(REAL_ARITH `x = y ==> m <= x ==> m <= y`) THEN
ONCE_REWRITE_TAC[DIST_SYM] THEN EXPAND_TAC "i" THEN
REWRITE_TAC[dist; VECTOR_SUB_LDISTRIB] THEN
UNDISCH_TAC
`&0 < measure(box(uv(tag(k:real^M->bool):real^M):real)
(tag k):real^M->bool)` THEN
EXPAND_TAC "box" THEN REWRITE_TAC[MEASURE_INTERVAL] THEN
SIMP_TAC[VECTOR_MUL_ASSOC; REAL_LT_IMP_NZ; REAL_MUL_LINV] THEN
REWRITE_TAC[VECTOR_MUL_LID]);;
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]);;
(* ------------------------------------------------------------------------- *)
(* Measurability of a function on a set (not necessarily itself measurable). *)
(* ------------------------------------------------------------------------- *)
parse_as_infix("measurable_on",(12,"right"));;
(* ------------------------------------------------------------------------- *)
(* Lebesgue measurability (like "measurable" but allowing infinite measure) *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Relation between measurability and integrability. *)
(* ------------------------------------------------------------------------- *)
"box"] THEN REWRITE_TAC[dist] THEN
FIRST_X_ASSUM MATCH_MP_TAC THEN
REWRITE_TAC[REAL_LT_INV_EQ; REAL_ARITH `&0 < &n + &1`] THEN
MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC `inv(&N)` THEN
ASM_REWRITE_TAC[] THEN MATCH_MP_TAC REAL_LE_INV2 THEN
REWRITE_TAC[REAL_OF_NUM_ADD; REAL_OF_NUM_LE; REAL_OF_NUM_LT] THEN
ASM_ARITH_TAC]);;
(* ------------------------------------------------------------------------- *)
(* Composing continuous and measurable functions; a few variants. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Basic closure properties of measurable functions. *)
(* ------------------------------------------------------------------------- *)
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]);;
(* ------------------------------------------------------------------------- *)
(* Natural closure properties of measurable functions; the intersection *)
(* one is actually quite tedious since we end up reinventing cube roots *)
(* before they actually get introduced in transcendentals.ml *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Negligibility of a Lipschitz image of a negligible set. *)
(* ------------------------------------------------------------------------- *)
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[]]]);;
(* ------------------------------------------------------------------------- *)
(* Simplest case of Sard's theorem (we don't need continuity of derivative). *)
(* ------------------------------------------------------------------------- *)
"p"] THEN
REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[IMP_CONJ] THEN
DISCH_THEN(MP_TAC o MATCH_MP LOWDIM_SUBSET_HYPERPLANE) THEN
REWRITE_TAC[VECTOR_SUB_RZERO; LEFT_IMP_EXISTS_THM] THEN
X_GEN_TAC `a:real^N` THEN GEOM_BASIS_MULTIPLE_TAC 1 `a:real^N` THEN
X_GEN_TAC `a:real` THEN GEN_REWRITE_TAC LAND_CONV [REAL_LE_LT] THEN
ASM_CASES_TAC `a = &0` THEN ASM_REWRITE_TAC[VECTOR_MUL_LZERO] THEN
REPEAT STRIP_TAC THEN
EXISTS_TAC
`interval[--(lambda i. if i = 1 then e else m):real^N,
(lambda i. if i = 1 then e else m)]` THEN
REWRITE_TAC[MEASURABLE_INTERVAL] THEN CONJ_TAC THENL
[REWRITE_TAC[SUBSET; IN_ELIM_THM; IN_INTERVAL] THEN
SIMP_TAC[VECTOR_NEG_COMPONENT; LAMBDA_BETA] THEN
X_GEN_TAC `x:real^N` THEN DISCH_THEN(CONJUNCTS_THEN ASSUME_TAC) THEN
REWRITE_TAC[REAL_BOUNDS_LE] THEN X_GEN_TAC `i:num` THEN STRIP_TAC THEN
COND_CASES_TAC THENL
[ALL_TAC; ASM_MESON_TAC[COMPONENT_LE_NORM; REAL_LE_TRANS]] THEN
FIRST_X_ASSUM(X_CHOOSE_THEN `y:real^N` STRIP_ASSUME_TAC) THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [SUBSET]) THEN
DISCH_THEN(MP_TAC o SPEC `y:real^N`) THEN
ASM_SIMP_TAC[SPAN_SUPERSET; IN_ELIM_THM; DOT_BASIS; DOT_LMUL;
DIMINDEX_GE_1; LE_REFL; REAL_ENTIRE; REAL_LT_IMP_NZ] THEN
MP_TAC(ISPECL [`x - y:real^N`; `1`] COMPONENT_LE_NORM) THEN
REWRITE_TAC[VECTOR_SUB_COMPONENT; ARITH; DIMINDEX_GE_1] THEN
ASM_REAL_ARITH_TAC;
REWRITE_TAC[MEASURE_INTERVAL; CONTENT_CLOSED_INTERVAL_CASES] THEN
SIMP_TAC[VECTOR_NEG_COMPONENT; LAMBDA_BETA] THEN
COND_CASES_TAC THEN ASM_SIMP_TAC[REAL_LE_MUL; REAL_POW_LE; REAL_POS] THEN
REWRITE_TAC[REAL_ARITH `x - --x = &2 * x`] THEN
SIMP_TAC[PRODUCT_CLAUSES_LEFT; DIMINDEX_GE_1] THEN
MATCH_MP_TAC REAL_LE_LMUL THEN ASM_SIMP_TAC[REAL_LE_MUL; REAL_POS] THEN
SIMP_TAC[ARITH; ARITH_RULE `2 <= n ==> ~(n = 1)`] THEN
SIMP_TAC[PRODUCT_CONST_NUMSEG; DIMINDEX_GE_1; REAL_LE_REFL; ARITH_RULE
`1 <= n ==> (n + 1) - 2 = n - 1`]]) in
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[]]]);;
(* ------------------------------------------------------------------------- *)
(* Also negligibility of BV low-dimensional image. *)
(* ------------------------------------------------------------------------- *)
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]]]);;
(* ------------------------------------------------------------------------- *)
(* Properties of Lebesgue measurable sets. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Invariance theorems for Lebesgue measurability. *)
(* ------------------------------------------------------------------------- *)
add_translation_invariants [LEBESGUE_MEASURABLE_TRANSLATION];;
add_linear_invariants [LEBESGUE_MEASURABLE_LINEAR_IMAGE_EQ];;
(* ------------------------------------------------------------------------- *)
(* Various common equivalent forms of function measurability. *)
(* ------------------------------------------------------------------------- *)
let (MEASURABLE_ON_PREIMAGE_OPEN_HALFSPACE_COMPONENT_LT,
MEASURABLE_ON_SIMPLE_FUNCTION_LIMIT) = (CONJ_PAIR o prove)
(`(!f:real^M->real^N.
f measurable_on (:real^M) <=>
!a k. 1 <= k /\ k <= dimindex(:N)
==> lebesgue_measurable {x | f(x)$k < a}) /\
(!f:real^M->real^N.
f measurable_on (:real^M) <=>
?g. (!n. (g n) measurable_on (:real^M)) /\
(!n. FINITE(IMAGE (g n) (:real^M))) /\
(!x. ((\n. g n x) --> f x) sequentially))`,
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)`,
let (MEASURABLE_ON_PREIMAGE_OPEN_INTERVAL,
MEASURABLE_ON_PREIMAGE_OPEN) = (CONJ_PAIR o prove)
(`(!f:real^M->real^N.
f measurable_on (:real^M) <=>
!a b. lebesgue_measurable {x | f(x) IN interval(a,b)}) /\
(!f:real^M->real^N.
f measurable_on (:real^M) <=>
!t. open t ==> lebesgue_measurable {x | f(x) IN t})`,
(* ------------------------------------------------------------------------- *)
(* More connections with measure where Lebesgue measurability is useful. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Localized variants of function measurability equivalents. *)
(* ------------------------------------------------------------------------- *)
let [MEASURABLE_ON_LEBESGUE_MEASURABLE_PREIMAGE_CLOSED;
MEASURABLE_ON_LEBESGUE_MEASURABLE_PREIMAGE_CLOSED_INTERVAL;
MEASURABLE_ON_LEBESGUE_MEASURABLE_PREIMAGE_OPEN;
MEASURABLE_ON_LEBESGUE_MEASURABLE_PREIMAGE_OPEN_HALFSPACE_COMPONENT_GE;
MEASURABLE_ON_LEBESGUE_MEASURABLE_PREIMAGE_OPEN_HALFSPACE_COMPONENT_GT;
MEASURABLE_ON_LEBESGUE_MEASURABLE_PREIMAGE_OPEN_HALFSPACE_COMPONENT_LE;
MEASURABLE_ON_LEBESGUE_MEASURABLE_PREIMAGE_OPEN_HALFSPACE_COMPONENT_LT;
MEASURABLE_ON_LEBESGUE_MEASURABLE_PREIMAGE_OPEN_INTERVAL] =
(CONJUNCTS o prove)
(`(!f:real^M->real^N s.
lebesgue_measurable s
==> (f measurable_on s <=>
!t. closed t ==> lebesgue_measurable {x | x IN s /\ f x IN t})) /\
(!f:real^M->real^N s.
lebesgue_measurable s
==> (f measurable_on s <=>
!a b. lebesgue_measurable {x | x IN s /\ f x IN interval[a,b]})) /\
(!f:real^M->real^N s.
lebesgue_measurable s
==> (f measurable_on s <=>
!t. open t ==> lebesgue_measurable {x | x IN s /\ f x IN t})) /\
(!f:real^M->real^N s.
lebesgue_measurable s
==> (f measurable_on s <=>
!a k. 1 <= k /\ k <= dimindex(:N)
==> lebesgue_measurable {x | x IN s /\ (f x)$k >= a})) /\
(!f:real^M->real^N s.
lebesgue_measurable s
==> (f measurable_on s <=>
!a k. 1 <= k /\ k <= dimindex(:N)
==> lebesgue_measurable {x | x IN s /\ (f x)$k > a})) /\
(!f:real^M->real^N s.
lebesgue_measurable s
==> (f measurable_on s <=>
!a k. 1 <= k /\ k <= dimindex(:N)
==> lebesgue_measurable {x | x IN s /\ (f x)$k <= a})) /\
(!f:real^M->real^N s.
lebesgue_measurable s
==> (f measurable_on s <=>
!a k. 1 <= k /\ k <= dimindex(:N)
==> lebesgue_measurable {x | x IN s /\ (f x)$k < a})) /\
(!f:real^M->real^N s.
lebesgue_measurable s
==> (f measurable_on s <=>
!a b. lebesgue_measurable {x | x IN s /\ f x IN interval(a,b)}))`,
let [MEASURABLE_ON_MEASURABLE_PREIMAGE_CLOSED;
MEASURABLE_ON_MEASURABLE_PREIMAGE_CLOSED_INTERVAL;
MEASURABLE_ON_MEASURABLE_PREIMAGE_OPEN;
MEASURABLE_ON_MEASURABLE_PREIMAGE_OPEN_HALFSPACE_COMPONENT_GE;
MEASURABLE_ON_MEASURABLE_PREIMAGE_OPEN_HALFSPACE_COMPONENT_GT;
MEASURABLE_ON_MEASURABLE_PREIMAGE_OPEN_HALFSPACE_COMPONENT_LE;
MEASURABLE_ON_MEASURABLE_PREIMAGE_OPEN_HALFSPACE_COMPONENT_LT;
MEASURABLE_ON_MEASURABLE_PREIMAGE_OPEN_INTERVAL] =
(CONJUNCTS o prove)
(`(!f:real^M->real^N s.
measurable s
==> (f measurable_on s <=>
!t. closed t ==> measurable {x | x IN s /\ f x IN t})) /\
(!f:real^M->real^N s.
measurable s
==> (f measurable_on s <=>
!a b. measurable {x | x IN s /\ f x IN interval[a,b]})) /\
(!f:real^M->real^N s.
measurable s
==> (f measurable_on s <=>
!t. open t ==> measurable {x | x IN s /\ f x IN t})) /\
(!f:real^M->real^N s.
measurable s
==> (f measurable_on s <=>
!a k. 1 <= k /\ k <= dimindex(:N)
==> measurable {x | x IN s /\ (f x)$k >= a})) /\
(!f:real^M->real^N s.
measurable s
==> (f measurable_on s <=>
!a k. 1 <= k /\ k <= dimindex(:N)
==> measurable {x | x IN s /\ (f x)$k > a})) /\
(!f:real^M->real^N s.
measurable s
==> (f measurable_on s <=>
!a k. 1 <= k /\ k <= dimindex(:N)
==> measurable {x | x IN s /\ (f x)$k <= a})) /\
(!f:real^M->real^N s.
measurable s
==> (f measurable_on s <=>
!a k. 1 <= k /\ k <= dimindex(:N)
==> measurable {x | x IN s /\ (f x)$k < a})) /\
(!f:real^M->real^N s.
measurable s
==> (f measurable_on s <=>
!a b. measurable {x | x IN s /\ f x IN interval(a,b)}))`,
REPEAT STRIP_TAC THEN
FIRST_ASSUM(ASSUME_TAC o MATCH_MP MEASURABLE_IMP_LEBESGUE_MEASURABLE) THENL
[ASM_SIMP_TAC[MEASURABLE_ON_LEBESGUE_MEASURABLE_PREIMAGE_CLOSED];
ASM_SIMP_TAC[MEASURABLE_ON_LEBESGUE_MEASURABLE_PREIMAGE_CLOSED_INTERVAL];
ASM_SIMP_TAC[MEASURABLE_ON_LEBESGUE_MEASURABLE_PREIMAGE_OPEN];
ASM_SIMP_TAC
[MEASURABLE_ON_LEBESGUE_MEASURABLE_PREIMAGE_OPEN_HALFSPACE_COMPONENT_GE];
ASM_SIMP_TAC
[MEASURABLE_ON_LEBESGUE_MEASURABLE_PREIMAGE_OPEN_HALFSPACE_COMPONENT_GT];
ASM_SIMP_TAC
[MEASURABLE_ON_LEBESGUE_MEASURABLE_PREIMAGE_OPEN_HALFSPACE_COMPONENT_LE];
ASM_SIMP_TAC
[MEASURABLE_ON_LEBESGUE_MEASURABLE_PREIMAGE_OPEN_HALFSPACE_COMPONENT_LT];
ASM_SIMP_TAC
[MEASURABLE_ON_LEBESGUE_MEASURABLE_PREIMAGE_OPEN_INTERVAL]] THEN
EQ_TAC THEN SIMP_TAC[MEASURABLE_IMP_LEBESGUE_MEASURABLE] THEN
REPEAT STRIP_TAC THEN MATCH_MP_TAC MEASURABLE_LEGESGUE_MEASURABLE_SUBSET THEN
EXISTS_TAC `s:real^M->bool` THEN ASM_SIMP_TAC[] THEN SET_TAC[]);;
(* ------------------------------------------------------------------------- *)
(* Regularity properties and Steinhaus, this time for Lebesgue measure. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Existence of nonmeasurable subsets of any set of positive measure. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Preserving Lebesgue measurability vs. preserving negligibility. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Measurability of continuous functions. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Measurability of a.e. derivatives. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Approximation of L_1 functions by bounded continuous ones. *)
(* Note that 100/fourier.ml has some generalizations to L_p spaces. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Luzin's theorem (Talvila and Loeb's proof from Marius Junge's notes). *)
(* ------------------------------------------------------------------------- *)
let LUZIN_EQ,LUZIN_EQ_ALT = (CONJ_PAIR o prove)
(`(!f:real^M->real^N s.
measurable s
==> (f measurable_on s <=>
!e. &0 < e
==> ?k. compact k /\ k SUBSET s /\
measure(s DIFF k) < e /\ f continuous_on k)) /\
(!f:real^M->real^N s.
measurable s
==> (f measurable_on s <=>
!e. &0 < e
==> ?k g. compact k /\ k SUBSET s /\
measure(s DIFF k) < e /\
g continuous_on (:real^M) /\
(!x. x IN k ==> g x = f x)))`,
REWRITE_TAC[AND_FORALL_THM] THEN REPEAT GEN_TAC THEN
ASM_CASES_TAC `measurable(s:real^M->bool)` THEN ASM_REWRITE_TAC[] THEN
MATCH_MP_TAC(TAUT
`(p ==> q) /\ (q ==> r) /\ (r ==> p) ==> (p <=> q) /\ (p <=> r)`) THEN
REPEAT CONJ_TAC THENL
[ASM_MESON_TAC[LUZIN];
MATCH_MP_TAC MONO_FORALL THEN X_GEN_TAC `e:real` THEN
ASM_CASES_TAC `&0 < e` THEN ASM_REWRITE_TAC[] THEN
MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `k:real^M->bool` THEN
STRIP_TAC THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC TIETZE_UNBOUNDED THEN
ASM_SIMP_TAC[COMPACT_IMP_CLOSED; SUBTOPOLOGY_UNIV; GSYM CLOSED_IN];
DISCH_THEN(MP_TAC o GEN `n:num` o SPEC `inv(&2 pow n)`) THEN
REWRITE_TAC[REAL_LT_INV_EQ; REAL_LT_POW2] THEN
REWRITE_TAC[SKOLEM_THM; LEFT_IMP_EXISTS_THM; FORALL_AND_THM] THEN
MAP_EVERY X_GEN_TAC [`k:num->real^M->bool`; `g:num->real^M->real^N`] THEN
STRIP_TAC THEN MATCH_MP_TAC MEASURABLE_ON_LIMIT THEN MAP_EVERY EXISTS_TAC
[`g:num->real^M->real^N`;
`s DIFF UNIONS {INTERS {k m | n <= m} | n IN (:num)}:real^M->bool`] THEN
REPEAT CONJ_TAC THENL
[X_GEN_TAC `n:num` THEN
MATCH_MP_TAC CONTINUOUS_IMP_MEASURABLE_ON_LEBESGUE_MEASURABLE_SUBSET THEN
ASM_MESON_TAC[MEASURABLE_IMP_LEBESGUE_MEASURABLE; CONTINUOUS_ON_SUBSET;
SUBSET_UNIV];
SIMP_TAC[DIFF_UNIONS_NONEMPTY; SET_RULE `~({f x | x IN UNIV} = {})`] THEN
REWRITE_TAC[NEGLIGIBLE_OUTER] THEN X_GEN_TAC `e:real` THEN DISCH_TAC THEN
MP_TAC(SPECL [`inv(&2)`; `e / &4`] REAL_ARCH_POW_INV) THEN
ANTS_TAC THENL [ASM_REAL_ARITH_TAC; REWRITE_TAC[REAL_POW_INV]] THEN
DISCH_THEN(X_CHOOSE_THEN `n:num` STRIP_ASSUME_TAC) THEN
EXISTS_TAC `s DIFF INTERS {k m | n:num <= m}:real^M->bool` THEN
REPEAT CONJ_TAC THENL
[REWRITE_TAC[INTERS_GSPEC; FORALL_IN_GSPEC] THEN ASM SET_TAC[];
MATCH_MP_TAC MEASURABLE_DIFF THEN ASM_REWRITE_TAC[] THEN
MATCH_MP_TAC MEASURABLE_COUNTABLE_INTERS_GEN THEN
ASM_SIMP_TAC[FORALL_IN_GSPEC; MEASURABLE_COMPACT] THEN
CONJ_TAC THENL [ALL_TAC; ASM SET_TAC[LE_REFL]] THEN
ONCE_REWRITE_TAC[SIMPLE_IMAGE_GEN] THEN
MATCH_MP_TAC COUNTABLE_IMAGE THEN
MESON_TAC[NUM_COUNTABLE; COUNTABLE_SUBSET; SUBSET_UNIV];
REWRITE_TAC[DIFF_INTERS] THEN
MATCH_MP_TAC(REAL_ARITH `&0 < e /\ x <= e / &2 ==> x < e`) THEN
ASM_REWRITE_TAC[] THEN MATCH_MP_TAC
(MESON[] `measurable s /\ measure s <= b ==> measure s <= b`) THEN
MATCH_MP_TAC MEASURE_COUNTABLE_UNIONS_LE_GEN THEN
ASM_SIMP_TAC[FORALL_IN_GSPEC; MEASURABLE_COMPACT; MEASURABLE_DIFF] THEN
CONJ_TAC THENL
[ONCE_REWRITE_TAC[SIMPLE_IMAGE_GEN] THEN
MATCH_MP_TAC COUNTABLE_IMAGE THEN
REWRITE_TAC[SET_RULE `{x | x IN s} = s`] THEN
ONCE_REWRITE_TAC[SIMPLE_IMAGE_GEN] THEN
MATCH_MP_TAC COUNTABLE_IMAGE THEN
MESON_TAC[NUM_COUNTABLE; COUNTABLE_SUBSET; SUBSET_UNIV];
REWRITE_TAC[SIMPLE_IMAGE] THEN ONCE_REWRITE_TAC[CONJ_SYM] THEN
REWRITE_TAC[FORALL_FINITE_SUBSET_IMAGE] THEN
ONCE_REWRITE_TAC[SIMPLE_IMAGE_GEN] THEN
REWRITE_TAC[FORALL_FINITE_SUBSET_IMAGE] THEN
X_GEN_TAC `ns:num->bool` THEN REWRITE_TAC[SUBSET; IN_ELIM_THM] THEN
STRIP_TAC THEN REWRITE_TAC[GSYM IMAGE_o] THEN
W(MP_TAC o PART_MATCH (lhand o rand) SUM_IMAGE_LE o lhand o snd) THEN
ASM_SIMP_TAC[o_DEF; MEASURE_POS_LE; MEASURABLE_DIFF;
MEASURABLE_COMPACT] THEN
MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ_ALT] REAL_LE_TRANS) THEN
FIRST_ASSUM(MP_TAC o SPEC `\x:num. x` o
MATCH_MP UPPER_BOUND_FINITE_SET) THEN
REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN X_GEN_TAC `m:num` THEN
STRIP_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THEN
EXISTS_TAC `sum (n..m) (\i. measure(s DIFF k i:real^M->bool))` THEN
CONJ_TAC THENL
[MATCH_MP_TAC SUM_SUBSET_SIMPLE THEN
ASM_SIMP_TAC[MEASURE_POS_LE; MEASURABLE_DIFF; MEASURABLE_COMPACT;
FINITE_NUMSEG; SUBSET; IN_NUMSEG];
ALL_TAC] THEN
MATCH_MP_TAC REAL_LE_TRANS THEN
EXISTS_TAC `sum (n..m) (\i. inv(&2 pow i))` THEN
ASM_SIMP_TAC[SUM_LE_NUMSEG; REAL_LT_IMP_LE] THEN
REWRITE_TAC[REAL_INV_POW; SUM_GP; LT] THEN
COND_CASES_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
CONV_TAC REAL_RAT_REDUCE_CONV THEN MATCH_MP_TAC(REAL_ARITH
`a <= e / &4 /\ &0 <= b
==> (a - b) / (&1 / &2) <= e / &2`) THEN
REWRITE_TAC[real_div; REAL_MUL_LID; REAL_POW_INV] THEN
ASM_SIMP_TAC[GSYM real_div; REAL_LT_IMP_LE; REAL_LE_INV_EQ;
REAL_LT_POW2]]];
REWRITE_TAC[SET_RULE `s DIFF (s DIFF t) = s INTER t`] THEN
X_GEN_TAC `x:real^M` THEN REWRITE_TAC[UNIONS_GSPEC; IN_INTER] THEN
REWRITE_TAC[IN_UNIV; IN_ELIM_THM; INTERS_GSPEC] THEN
STRIP_TAC THEN MATCH_MP_TAC LIM_EVENTUALLY THEN
REWRITE_TAC[EVENTUALLY_SEQUENTIALLY] THEN ASM_MESON_TAC[]]]);;