(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION *)
(* *)
(* Chapter: Volume *)
(* Author: Nguyen Tat Thang *)
(* Date: 2010-02-09 *)
(* ========================================================================== *)
flyspeck_needs "general/prove_by_refinement.hl";;
(* flyspeck_needs "trigonometry/trig2.hl";; *)
module Vol1 = struct
let prove_by_refinement = Prove_by_refinement.prove_by_refinement;;
let BY = Hales_tactic.BY;;
(* DEPRECATED 2013-05-25.
let sphere= new_definition`sphere x=(?(v:real^3)(r:real). (r> &0)/\ (x={w:real^3 | norm (w-v)= r}))`;;
*)
(* old definitions added by thales Nov 11, 2009 *)
(*
let radial_norm = new_definition `radial_norm r (x:real^A) C <=> (C SUBSET normball x r) /\ (!u. (x+u) IN C ==> (!t.(t> &0) /\ (t* norm u < r)==>(x+ t % u) IN C))`;;
*)
(* }}} *)
(*
let eventually_radial_norm = new_definition
`eventually_radial_norm x C <=> (?r. (r> &0) /\ radial_norm r x (C INTER normball x r))`;;
*)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(*----------------------------------------------------------*)
(*To prove Lemma 4.2*)
let th1= prove(`!a b c. [a; b; c]= CONS a (CONS b [c])`,REPEAT GEN_TAC THEN MESON_TAC[]);;
let identity_scale=prove(`scale (vec 1)= I`,REWRITE_TAC[
FUN_EQ_THM] THEN GEN_TAC THEN REWRITE_TAC[
I_THM] THEN REWRITE_TAC[
scale] THEN REWRITE_TAC[
vector] THEN SIMP_TAC[dodai] THEN REWRITE_TAC[
CART_EQ] THEN REWRITE_TAC[DIMINDEX_3] THEN GEN_TAC THEN DISCH_TAC THEN ASM_SIMP_TAC[
LAMBDA_BETA;DIMINDEX_3] THEN MP_TAC (ARITH_RULE `(1 <= i /\ i <= 3) <=> ( i=1 \/ i=2 \/ i=3)`) THEN ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC THENL [ASM_REWRITE_TAC[];ASM_REWRITE_TAC[];ASM_REWRITE_TAC[]] THENL [ASM_REWRITE_TAC[ARITH_RULE `1-1=0`];REWRITE_TAC[ARITH_RULE `2-1= SUC 0 `];REWRITE_TAC[ARITH_RULE `3-1= SUC 1 `]] THENL [REWRITE_TAC[
EL];REWRITE_TAC[
EL];REWRITE_TAC[
EL]] THENL [REWRITE_TAC[
HD];REWRITE_TAC[
HD;
TL];REWRITE_TAC[ARITH_RULE `1= SUC 0 `;
EL]] THENL [SIMP_TAC[
th3;ARITH_RULE `1<=1 /\ 1<=3`];SIMP_TAC[
th3;ARITH_RULE `1<=2 /\ 2<=3`];REWRITE_TAC[
HD;
TL]] THENL [ARITH_TAC;ARITH_TAC;REWRITE_TAC[ARITH_RULE `SUC 0=1`]] THEN SIMP_TAC[
th3;ARITH_RULE `1<=3 /\ 3<=3`] THEN ARITH_TAC);;
let SET_EQ=prove(`(A: real^3 -> bool) = B <=> (!a. a IN A ==> a IN B) /\ (!a. a IN B ==> a IN A)`,SET_TAC[]);;
let scale_mul=prove(`!(s:real) t x. (scale (s%(t:real^3)) (x:real^3):real^3) = s% scale t x`,REPEAT GEN_TAC THEN REWRITE_TAC[
scale] THEN REWRITE_TAC[
vector] THEN SIMP_TAC[dodai] THEN REWRITE_TAC[
CART_EQ] THEN REWRITE_TAC[DIMINDEX_3] THEN ASM_REWRITE_TAC[ARITH_RULE `(1 <= i /\ i <=3) <=> i =1 \/ i=2 \/ i=3`] THEN GEN_TAC THEN STRIP_TAC THENL [ASM_REWRITE_TAC[
LAMBDA_BETA];ASM_REWRITE_TAC[];ASM_REWRITE_TAC[]] THENL [SIMP_TAC[
LAMBDA_BETA;DIMINDEX_3;ARITH_RULE `1<=1 /\ 1<=3`];SIMP_TAC[
VECTOR_MUL_COMPONENT;
LAMBDA_BETA;DIMINDEX_3;ARITH_RULE `1<=2 /\ 2<=3`];SIMP_TAC[
VECTOR_MUL_COMPONENT;
LAMBDA_BETA;DIMINDEX_3;ARITH_RULE `1<=3 /\ 3<=3`]] THENL [SIMP_TAC[
VECTOR_MUL_COMPONENT;DIMINDEX_3;ARITH_RULE `1<=1 /\ 1<=3`
];REWRITE_TAC[
EL;ARITH_RULE `2-1=SUC 0`];REWRITE_TAC[
EL;ARITH_RULE `3-1=SUC 1`]] THENL [SIMP_TAC[
LAMBDA_BETA;DIMINDEX_3;ARITH_RULE `1<=1 /\ 1<=3`];REWRITE_TAC[
HD;
TL];REWRITE_TAC[
EL;ARITH_RULE `1=SUC 0`]] THENL [REWRITE_TAC[ARITH_RULE `1-1=0`;
EL];ARITH_TAC;REWRITE_TAC[
HD;
TL]] THENL[REWRITE_TAC[
HD];ARITH_TAC] THEN ARITH_TAC);;
let rsduong=prove(`!(s:real) (r:real). (s> &0) /\ (s<r)==> r/s> &0`,REPEAT GEN_TAC THEN STRIP_TAC THEN UNDISCH_TAC `(s> &0):bool` THEN REWRITE_TAC[ARITH_RULE `s> &0 <=> &0 <s`] THEN SIMP_TAC[
REAL_LT_RDIV_EQ] THEN REWRITE_TAC[ARITH_RULE `&0*s= &0`] THEN ASM_REAL_ARITH_TAC);;
let rsnon_zero=prove(`!(s:real) (r:real). (s> &0) /\ (s<r)==> ~(r/s= &0)`,REPEAT GEN_TAC THEN STRIP_TAC THEN SUBGOAL_THEN `r/s> &0` MP_TAC THENL[ASM_SIMP_TAC[rsduong];REAL_ARITH_TAC]);;
let rduong=prove(`!(s:real) (r:real). (s> &0) /\ (s<r)==> (r> &0)`,REPEAT GEN_TAC THEN STRIP_TAC THEN UNDISCH_TAC `(s<r):bool` THEN UNDISCH_TAC `(s> &0):bool`THEN REAL_ARITH_TAC);;
let rnon_zero=prove(`!(s:real) (r:real). (s> &0) /\ (s<r)==> ~(r= &0)`,REPEAT GEN_TAC THEN STRIP_TAC THEN SUBGOAL_THEN `r> &0` MP_TAC THENL[UNDISCH_TAC `(s<r):bool`THEN UNDISCH_TAC `(s> &0):bool`THEN REWRITE_TAC[TAUT `A==>B ==> C <=> A/\B==>C`];REAL_ARITH_TAC] THEN ASM_REWRITE_TAC[rduong]);;
let rs_sr_unit= prove(`!(s:real) (r:real). (s> &0) /\ (s<r)==> (s / r * r / s= &1)`,
REPEAT GEN_TAC THEN STRIP_TAC THEN SUBGOAL_THEN `~(r/s= &0)` MP_TAC
THENL [UNDISCH_TAC `(s<r):bool`THEN UNDISCH_TAC `(s> &0):bool`THEN REWRITE_TAC[TAUT `A==>B ==> C <=> A/\B==>C`];STRIP_TAC]
THENL [ASM_REWRITE_TAC[
rsnon_zero];SUBGOAL_THEN `r/s= inv(s/r)` MP_TAC]
THENL [UNDISCH_TAC `~(r / s = &0):bool`;SIMP_TAC[]]
THENL [ASM_SIMP_TAC[
REAL_INV_DIV];DISCH_TAC]
THEN SUBGOAL_THEN `~(s/r= &0)` MP_TAC
THENL [MP_TAC(ARITH_RULE `s> &0 ==> ~(s= &0)`);SIMP_TAC[
REAL_MUL_RINV]]
THEN ASM_REWRITE_TAC[] THEN SIMP_TAC[CONTRAPOS_THM]
THEN DISCH_TAC THEN SUBGOAL_THEN `r*s/r = r* &0` MP_TAC
THENL [REWRITE_TAC[ARITH_RULE `r * s / r = r * &0 <=> r * s / r - r * &0 = &0`];SUBGOAL_THEN `~(r= &0)` MP_TAC]
THENL [REWRITE_TAC[ARITH_RULE `r * s / r - r * &0 = r*(s/r- &0)`];UNDISCH_TAC `(s<r):bool`THEN UNDISCH_TAC `(s> &0):bool`THEN REWRITE_TAC[TAUT `A==>B ==> C <=> A/\B==>C`];ASM_SIMP_TAC[
REAL_DIV_LMUL]]
THENL [ASM_REWRITE_TAC[];ASM_REWRITE_TAC[
rnon_zero];REAL_ARITH_TAC]
THEN ARITH_TAC);;
let SQRT_MUL_POW_2= prove(`!(a:real) b. (a>= &0) /\ (b>= &0) ==> sqrt((a*a)*b)= a* sqrt(b)`,
REPEAT GEN_TAC THEN STRIP_TAC THEN SUBGOAL_THEN `a*a>= &0` MP_TAC
THENL [REWRITE_TAC[ARITH_RULE `s>= &0 <=> &0<= s`];DISCH_TAC THEN UNDISCH_TAC `(b>= &0):bool`]
THENL [SIMP_TAC[
REAL_LE_SQUARE];REWRITE_TAC[ARITH_RULE `s>= &0 <=> &0<= s`]]
THEN UNDISCH_TAC `(a * a >= &0):bool` THEN REWRITE_TAC[ARITH_RULE `a*a>= &0 <=> &0 <= a*a`]
THEN REWRITE_TAC[TAUT `A==>B ==>C <=> A/\ B ==> C`]
THEN SIMP_TAC[
SQRT_MUL] THEN SUBGOAL_THEN `
sqrt(a*a)= a` MP_TAC
THENL [UNDISCH_TAC `(a>= &0):bool`;MESON_TAC[]]
THEN REWRITE_TAC[ARITH_RULE `s>= &0 <=> &0<= s`]
THEN SIMP_TAC[
SQRT_MUL] THEN SIMP_TAC[
SQRT_POW_2] THEN MESON_TAC[REAL_POW_2;
SQRT_POW_2]);;
(*
g `!r s (x:real^3) C. radial_norm r x C /\ (s > &0) /\ (s < r) ==> (C INTER normball x s = IMAGE ((+) x) (IMAGE (scale (s/r % (vec 1)))(IMAGE ((+) (--x)) (C INTER normball x r))))`;;
e (REPEAT GEN_TAC THEN STRIP_TAC);;
e (REWRITE_TAC[SET_EQ] THEN CONJ_TAC THEN GEN_TAC);;
e (REWRITE_TAC[IN_INTER;IN_IMAGE]);;
e (STRIP_TAC);;
e (EXISTS_TAC `a-x:real^3`);;
e (REWRITE_TAC[VECTOR_ARITH `(a:real^3)= x+a-x`]);;
e (EXISTS_TAC `scale (r/s% vec 1)(a-x):real^3`);;
e (SIMP_TAC[scale_mul] THEN SIMP_TAC[identity_scale] THEN REWRITE_TAC[I_THM]);;
e (REWRITE_TAC[VECTOR_MUL_ASSOC]);;
e (UNDISCH_TAC `(s> &0):bool` THEN UNDISCH_TAC `(s<r):bool` THEN REWRITE_TAC[TAUT `A==>B==>C <=> A/\B==>C`]);;
e (SIMP_TAC[rs_sr_unit]);;
e (STRIP_TAC);;
e (CONJ_TAC);;
e (VECTOR_ARITH_TAC);;
e (EXISTS_TAC `(x+r / s % (a - x)):real^3`);;
e (CONJ_TAC);;
e (VECTOR_ARITH_TAC);;
e (CONJ_TAC);;
e (SUBGOAL_THEN `(x:real^3)+(a-x) IN (C:real^3->bool)` MP_TAC);;
e (UNDISCH_TAC `(a:real^3 IN (C:real^3->bool)):bool`);;
e (MP_TAC(VECTOR_ARITH `(a:real^3)=x+(a-x)`));;
e (REWRITE_TAC[TAUT `A==>B==>C <=> A/\B==>C`]);;
e (SET_TAC[]);;
e (DISCH_TAC);;
e (SUBGOAL_THEN `(r/s)> &0 /\ (r/s) * (norm (a:real^3-x):real)< r` MP_TAC);;
e (UNDISCH_TAC `(s> &0):bool` THEN UNDISCH_TAC `(s<r):bool` THEN REWRITE_TAC[TAUT `A==>B==>C <=> A/\B==>C`]);;
e (SIMP_TAC[rsduong]);;
e (STRIP_TAC);;
e (UNDISCH_TAC `(a:real^3 IN normball x s):bool`);;
e (REWRITE_TAC[normball]);;
e (REWRITE_TAC[IN_ELIM_THM;dist]);;
e (ABBREV_TAC `c= norm(a:real^3 -x)`);;
e (DISCH_TAC);;
e (SUBGOAL_THEN `r/s> &0` MP_TAC);;
e (UNDISCH_TAC `(s<r):bool` THEN UNDISCH_TAC `(s> &0):bool` THEN REWRITE_TAC[TAUT `A==>B==>C <=> A/\B==>C`]);;
e (SIMP_TAC[rsduong]);;
e (REWRITE_TAC[ARITH_RULE `s> &0 <=> &0< s`]);;
e (DISCH_TAC);;
e (SUBGOAL_THEN `r/s*c < r/s*s` MP_TAC);;
e (UNDISCH_TAC `(c < s):bool` THEN UNDISCH_TAC `(&0< r/s):bool` THEN REWRITE_TAC[TAUT `A==>B==>C <=> A/\B==>C`]);;
e (REWRITE_TAC[TAUT `A/\B==>C <=> B/\A==>C`] THEN REWRITE_TAC[ARITH_RULE `r / s * c < r / s * s <=> c*r/s < s*r/s`]);;
e (REWRITE_TAC[REAL_LT_RMUL]);;
e (MP_TAC(ARITH_RULE `s> &0 ==> ~(s= &0)`));;
e (ASM_REWRITE_TAC[]);;
e (REWRITE_TAC[TAUT `A==>B==>C <=>A/\B==>C`]);;
e (SIMP_TAC[]);;
e (MESON_TAC[REAL_DIV_RMUL]);;
e (ASM_MESON_TAC[radial_norm]);;
e (REWRITE_TAC[normball;IN_ELIM_THM;dist]);;
e (REWRITE_TAC[VECTOR_ARITH `((x:real^3) + r / s % (a - x)) - x= r / s % (a - x)`]);;
e (REWRITE_TAC[vector_norm]);;
e (REWRITE_TAC[VECTOR_ARITH `r / s % ((a:real^3) - x) dot r / s % (a - x)= (r/s *r/s) * (a-x) dot (a-x)`]);;
e (SUBGOAL_THEN `r/s> &0` MP_TAC);;
e (UNDISCH_TAC `(s<r):bool` THEN UNDISCH_TAC `(s> &0):bool` THEN REWRITE_TAC[TAUT `A==>B==>C <=> A/\B==>C`]);;
e (REWRITE_TAC[rsduong]);;
e (DISCH_TAC);;
e (UNDISCH_TAC `(a IN normball (x:real^3) s):bool`);;
e (REWRITE_TAC[normball;IN_ELIM_THM;dist]);;
e (REWRITE_TAC[vector_norm]);;
e (ABBREV_TAC `q2= (a:real^3 - x) dot (a - x)`);;
e (DISCH_TAC);;
e (UNDISCH_TAC `(sqrt q2 < s):bool`);;
e (DISCH_TAC);;
e (SUBGOAL_THEN `q2>= &0` MP_TAC);;
e (REWRITE_TAC[ARITH_RULE `q2>= &0 <=> &0<= q2`]);;
e (ASM_MESON_TAC[DOT_POS_LE]);;
e (MP_TAC(ARITH_RULE `r/s> &0 ==> r/s>= &0`));;
e (ASM_REWRITE_TAC[]);;
e (REWRITE_TAC[TAUT `A==>B==>C <=> A/\B==>C`]);;
e (SIMP_TAC[SQRT_MUL_POW_2]);;
e (STRIP_TAC);;
e (SUBGOAL_THEN `r/s*sqrt q2<r/s * s` MP_TAC);;
e (REWRITE_TAC[ARITH_RULE `r / s * sqrt q2 < r / s * s<=> sqrt q2* r/s< s* r/s`]);;
e (UNDISCH_TAC `(r / s > &0):bool` THEN REWRITE_TAC[ARITH_RULE `r / s > &0<=> &0< r/s`] THEN UNDISCH_TAC `(sqrt q2 < s):bool`);;
e (REWRITE_TAC[TAUT `A==>B==>C <=> A/\B==>C`]);;
e (SIMP_TAC[REAL_LT_RMUL]);;
e (MP_TAC(ARITH_RULE `s> &0==> ~(s= &0)`));;
e (ASM_REWRITE_TAC[]);;
e (MESON_TAC[REAL_DIV_RMUL]);;
e (REWRITE_TAC[IN_IMAGE;IN_INTER]);;
e (REWRITE_TAC[scale_mul;identity_scale;I_THM]);;
e(STRIP_TAC THEN CONJ_TAC);;
e (ASM_SIMP_TAC[]);;
e (SUBGOAL_THEN `(x:real^3) + (--x + x''') IN C` MP_TAC);;
e (MP_TAC(VECTOR_ARITH `x'''= (x:real^3)+ (--x + x''')`));;
e (ABBREV_TAC `u1= (x:real^3) + --x + x'''`);;
e (UNDISCH_TAC `(x''' IN (C:real^3->bool)):bool`);;
e (REWRITE_TAC[TAUT `A==>B==>C <=> A/\B==>C`]);;
e (SET_TAC[]);;
e (SUBGOAL_THEN `s/r> &0 /\s/r* norm (--x+ x''':real^3)< r` MP_TAC);;
e (CONJ_TAC);;
e (MP_TAC(ARITH_RULE `s<r /\ s> &0 ==> r> &0`));;
e (ASM_REWRITE_TAC[]);;
e (REWRITE_TAC[ARITH_RULE `a> &0 <=> &0<a`]);;
e (REWRITE_TAC[REAL_LT_LDIV_EQ]);;
e (REWRITE_TAC[REAL_LT_RDIV_EQ]);;
e (SIMP_TAC[REAL_LT_RDIV_EQ]);;
e (REWRITE_TAC[ARITH_RULE `&0*r= &0`]);;
e (DISCH_TAC);;
e (ASM_REWRITE_TAC[]);;
e (REWRITE_TAC[ARITH_RULE `&0< s <=> s> &0`]);;
e (ASM_REWRITE_TAC[]);;
e (SUBGOAL_THEN `s/r> &0` ASSUME_TAC);;
e (MP_TAC(ARITH_RULE `s<r /\ s> &0 ==> r> &0`) THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[ARITH_RULE `a> &0 <=> &0<a`] THEN REWRITE_TAC[REAL_LT_LDIV_EQ] THEN REWRITE_TAC[REAL_LT_RDIV_EQ] THEN SIMP_TAC[REAL_LT_RDIV_EQ] THEN REWRITE_TAC[ARITH_RULE `&0*r= &0`] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[ARITH_RULE `&0< s <=> s> &0`] THEN ASM_REWRITE_TAC[]);;
e (SUBGOAL_THEN `s/r< &1` ASSUME_TAC);;
e (MP_TAC(ARITH_RULE `s<r /\ s> &0 ==> r> &0`));;
e (ASM_REWRITE_TAC[]);;
e (REWRITE_TAC[ARITH_RULE `r> &0 <=> &0 <r`]);;
e (REWRITE_TAC[ARITH_RULE `&1 * r= r`]);;
e (DISCH_TAC);;
e (ASM_REWRITE_TAC[]);;
e (UNDISCH_TAC `( &0<r):bool`);;
e (SIMP_TAC[REAL_LT_LDIV_EQ]);;
e (REWRITE_TAC[ARITH_RULE `&1*r=r`]);;
e (DISCH_TAC);;
e (ASM_REWRITE_TAC[]);;
e (UNDISCH_TAC `(x''':real^3 IN normball x r):bool`);;
e (REWRITE_TAC[normball;IN_ELIM_THM;dist]);;
e (SUBGOAL_THEN `norm (x''':real^3 - x)= norm (--x + x''')` ASSUME_TAC);;
e (MP_TAC(VECTOR_ARITH `x''':real^3 - x = --x + x'''`));;
e (ABBREV_TAC `v1= x''':real^3 - x`);;
e (MESON_TAC[]);;
e (ASM_SIMP_TAC[]);;
e (SUBGOAL_THEN `&0<= norm (--x + x''':real^3)` MP_TAC);;
e (SIMP_TAC[NORM_POS_LE]);;
e (REWRITE_TAC[TAUT `A==>B==>C <=> A/\B==>C`]);;
e (MP_TAC(ARITH_RULE `s/r> &0 /\ s/r< &1==> &0<= s/r /\ s/r< &1`));;
e (ASM_REWRITE_TAC[]);;
e (REWRITE_TAC[TAUT `A==>B/\C==>D <=> A/\B/\C==>D`]);;
e (ABBREV_TAC `y= norm (--x + x''':real^3)`);;
e (UNDISCH_TAC `(s / r < &1):bool`);;
e (REWRITE_TAC[TAUT `A==>B/\C/\D==>E <=> (B/\A/\C/\D==>E)`]);;
e (DISCH_TAC);;
e (SUBGOAL_THEN `s/r*y< &1*r` MP_TAC);;
e (UNDISCH_TAC `(&0 <= s / r /\ s / r < &1 /\ &0 <= y /\ y < r):bool`);;
e (MESON_TAC[REAL_LT_MUL2]);;
e (MESON_TAC[ARITH_RULE `&1*r= r`]);;
e (REWRITE_TAC[TAUT `A/\B==>C==>D <=> A/\B/\C==>D`]);;
e (ASM_MESON_TAC[radial_norm]);;
e (ASM_REWRITE_TAC[]);;
e (REWRITE_TAC[normball;IN_ELIM_THM;dist]);;
e (REWRITE_TAC[VECTOR_ARITH `(x + s / r % (--x + x''')) - x= s / r % (--x + x''')`]);;
e (SIMP_TAC[NORM_MUL]);;
e (SUBGOAL_THEN `s/r> &0` ASSUME_TAC);;
e (MP_TAC(ARITH_RULE `s<r /\ s> &0 ==> r> &0`) THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[ARITH_RULE `a> &0 <=> &0<a`] THEN REWRITE_TAC[REAL_LT_LDIV_EQ] THEN REWRITE_TAC[REAL_LT_RDIV_EQ] THEN SIMP_TAC[REAL_LT_RDIV_EQ] THEN REWRITE_TAC[ARITH_RULE `&0*r= &0`] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[ARITH_RULE `&0< s <=> s> &0`] THEN ASM_REWRITE_TAC[]);;
e (MP_TAC(ARITH_RULE `s/r> &0==> s/r>= &0`));;
e (ASM_REWRITE_TAC[]);;
e (REWRITE_TAC[ARITH_RULE `s/r>= &0 <=> &0<= s/r`]);;
e (DISCH_TAC);;
e (SUBGOAL_THEN `abs (s / r)= s/r` MP_TAC);;
e (ASM_SIMP_TAC[REAL_ABS_REFL]);;
e (SIMP_TAC[]);;
e (DISCH_TAC);;
e (UNDISCH_TAC `(x''':real^3 IN normball x r):bool`);;
e (REWRITE_TAC[normball;IN_ELIM_THM;dist]);;
e (SUBGOAL_THEN `norm (x''':real^3 - x)= norm (--x + x''')` ASSUME_TAC);;
e (MP_TAC(VECTOR_ARITH `x''':real^3 - x = --x + x'''`));;
e (ABBREV_TAC `v2= x''':real^3 - x`);;
e (MESON_TAC[]);;
e (ASM_SIMP_TAC[]);;
e (ABBREV_TAC `p= norm (--x + x''':real^3)`);;
e (DISCH_TAC);;
e (SUBGOAL_THEN `p*s/r< r*s/r` MP_TAC);;
e (MP_TAC(ARITH_RULE `s / r > &0 ==> &0< s/r`));;
e (ASM_REWRITE_TAC[]);;
e (UNDISCH_TAC `(p < r):bool` THEN REWRITE_TAC[TAUT `A==>B==>C <=> A/\B==>C`]);;
e (SIMP_TAC[REAL_LT_RMUL]);;
e (REWRITE_TAC[ARITH_RULE `s/r*p<s <=> p*s/r< s`]);;
e (MP_TAC(ARITH_RULE `s<r/\s> &0 ==> ~(r= &0)`));;
e (ASM_REWRITE_TAC[]);;
e (REWRITE_TAC[TAUT `A==>B==>C <=> A/\B==>C`]);;
e (MESON_TAC[REAL_DIV_LMUL]);;
let trans_strech_trans_radial=top_thm();;
*)
let trans_strech_trans_radial = prove_by_refinement(
`!r s (x:real^3) C. radial_norm r x C /\ (s > &0) /\ (s < r) ==> (C INTER normball x s = IMAGE ((+) x) (IMAGE (scale (s/r % (vec 1)))(IMAGE ((+) (--x)) (C INTER normball x r))))`,
(* {{{ proof *)
[
(REPEAT GEN_TAC THEN STRIP_TAC);
(REWRITE_TAC[
SET_EQ] THEN CONJ_TAC THEN GEN_TAC);
(REWRITE_TAC[
IN_INTER;
IN_IMAGE]);
(STRIP_TAC);
(EXISTS_TAC `a-x:real^3`);
(REWRITE_TAC[VECTOR_ARITH `(a:real^3)= x+a-x`]);
(EXISTS_TAC `
scale (r/s%
vec 1)(a-x):real^3`);
(SIMP_TAC[
scale_mul] THEN SIMP_TAC[
identity_scale] THEN REWRITE_TAC[
I_THM]);
(REWRITE_TAC[
VECTOR_MUL_ASSOC]);
(UNDISCH_TAC `(s> &0):bool` THEN UNDISCH_TAC `(s<r):bool` THEN REWRITE_TAC[TAUT `A==>B==>C <=> A/\B==>C`]);
(SIMP_TAC[
rs_sr_unit]);
(STRIP_TAC);
(CONJ_TAC);
BY((VECTOR_ARITH_TAC));
(EXISTS_TAC `(x+r / s % (a - x)):real^3`);
(CONJ_TAC);
BY((VECTOR_ARITH_TAC));
(CONJ_TAC);
(SUBGOAL_THEN `(x:real^3)+(a-x)
IN (C:real^3->bool)` MP_TAC);
(UNDISCH_TAC `(a:real^3
IN (C:real^3->bool)):bool`);
(MP_TAC(VECTOR_ARITH `(a:real^3)=x+(a-x)`));
(REWRITE_TAC[TAUT `A==>B==>C <=> A/\B==>C`]);
BY((SET_TAC[]));
(DISCH_TAC);
(SUBGOAL_THEN `(r/s)> &0 /\ (r/s) * (
norm (a:real^3-x):real)< r` MP_TAC);
(UNDISCH_TAC `(s> &0):bool` THEN UNDISCH_TAC `(s<r):bool` THEN REWRITE_TAC[TAUT `A==>B==>C <=> A/\B==>C`]);
(SIMP_TAC[rsduong]);
(STRIP_TAC);
(UNDISCH_TAC `(a:real^3
IN normball x s):bool`);
(REWRITE_TAC[
normball]);
(REWRITE_TAC[
IN_ELIM_THM;
dist]);
(ABBREV_TAC `c=
norm(a:real^3 -x)`);
(DISCH_TAC);
(SUBGOAL_THEN `r/s> &0` MP_TAC);
(UNDISCH_TAC `(s<r):bool` THEN UNDISCH_TAC `(s> &0):bool` THEN REWRITE_TAC[TAUT `A==>B==>C <=> A/\B==>C`]);
BY((SIMP_TAC[rsduong]));
(REWRITE_TAC[ARITH_RULE `s> &0 <=> &0< s`]);
(DISCH_TAC);
(SUBGOAL_THEN `r/s*c < r/s*s` MP_TAC);
(UNDISCH_TAC `(c < s):bool` THEN UNDISCH_TAC `(&0< r/s):bool` THEN REWRITE_TAC[TAUT `A==>B==>C <=> A/\B==>C`]);
(REWRITE_TAC[TAUT `A/\B==>C <=> B/\A==>C`] THEN REWRITE_TAC[ARITH_RULE `r / s * c < r / s * s <=> c*r/s < s*r/s`]);
BY((REWRITE_TAC[
REAL_LT_RMUL]));
(MP_TAC(ARITH_RULE `s> &0 ==> ~(s= &0)`));
(ASM_REWRITE_TAC[]);
(REWRITE_TAC[TAUT `A==>B==>C <=>A/\B==>C`]);
(SIMP_TAC[]);
BY((MESON_TAC[
REAL_DIV_RMUL]));
BY((ASM_MESON_TAC[
radial_norm]));
(REWRITE_TAC[
normball;
IN_ELIM_THM;
dist]);
(REWRITE_TAC[VECTOR_ARITH `((x:real^3) + r / s % (a - x)) - x= r / s % (a - x)`]);
(REWRITE_TAC[
vector_norm]);
(REWRITE_TAC[VECTOR_ARITH `r / s % ((a:real^3) - x)
dot r / s % (a - x)= (r/s *r/s) * (a-x)
dot (a-x)`]);
(SUBGOAL_THEN `r/s> &0` MP_TAC);
(UNDISCH_TAC `(s<r):bool` THEN UNDISCH_TAC `(s> &0):bool` THEN REWRITE_TAC[TAUT `A==>B==>C <=> A/\B==>C`]);
BY((REWRITE_TAC[rsduong]));
(DISCH_TAC);
(UNDISCH_TAC `(a
IN normball (x:real^3) s):bool`);
(REWRITE_TAC[
normball;
IN_ELIM_THM;
dist]);
(REWRITE_TAC[
vector_norm]);
(ABBREV_TAC `q2= (a:real^3 - x)
dot (a - x)`);
(DISCH_TAC);
(UNDISCH_TAC `(
sqrt q2 < s):bool`);
(DISCH_TAC);
(SUBGOAL_THEN `q2>= &0` MP_TAC);
(REWRITE_TAC[ARITH_RULE `q2>= &0 <=> &0<= q2`]);
BY((ASM_MESON_TAC[
DOT_POS_LE]));
(MP_TAC(ARITH_RULE `r/s> &0 ==> r/s>= &0`));
(ASM_REWRITE_TAC[]);
(REWRITE_TAC[TAUT `A==>B==>C <=> A/\B==>C`]);
(SIMP_TAC[
SQRT_MUL_POW_2]);
(STRIP_TAC);
(SUBGOAL_THEN `r/s*sqrt q2<r/s * s` MP_TAC);
(REWRITE_TAC[ARITH_RULE `r / s *
sqrt q2 < r / s * s<=>
sqrt q2* r/s< s* r/s`]);
(UNDISCH_TAC `(r / s > &0):bool` THEN REWRITE_TAC[ARITH_RULE `r / s > &0<=> &0< r/s`] THEN UNDISCH_TAC `(
sqrt q2 < s):bool`);
(REWRITE_TAC[TAUT `A==>B==>C <=> A/\B==>C`]);
BY((SIMP_TAC[
REAL_LT_RMUL]));
(MP_TAC(ARITH_RULE `s> &0==> ~(s= &0)`));
(ASM_REWRITE_TAC[]);
BY((MESON_TAC[
REAL_DIV_RMUL]));
(REWRITE_TAC[
IN_IMAGE;
IN_INTER]);
(REWRITE_TAC[
scale_mul;
identity_scale;
I_THM]);
(STRIP_TAC THEN CONJ_TAC);
(ASM_SIMP_TAC[]);
(SUBGOAL_THEN `(x:real^3) + (--x + x''')
IN C` MP_TAC);
(MP_TAC(VECTOR_ARITH `x'''= (x:real^3)+ (--x + x''')`));
(ABBREV_TAC `u1= (x:real^3) + --x + x'''`);
(UNDISCH_TAC `(x'''
IN (C:real^3->bool)):bool`);
(REWRITE_TAC[TAUT `A==>B==>C <=> A/\B==>C`]);
BY((SET_TAC[]));
(SUBGOAL_THEN `s/r> &0 /\s/r*
norm (--x+ x''':real^3)< r` MP_TAC);
(CONJ_TAC);
(MP_TAC(ARITH_RULE `s<r /\ s> &0 ==> r> &0`));
(ASM_REWRITE_TAC[]);
(REWRITE_TAC[ARITH_RULE `a> &0 <=> &0<a`]);
(REWRITE_TAC[
REAL_LT_LDIV_EQ]);
(REWRITE_TAC[
REAL_LT_RDIV_EQ]);
(SIMP_TAC[
REAL_LT_RDIV_EQ]);
(REWRITE_TAC[ARITH_RULE `&0*r= &0`]);
(DISCH_TAC);
(ASM_REWRITE_TAC[]);
(REWRITE_TAC[ARITH_RULE `&0< s <=> s> &0`]);
BY((ASM_REWRITE_TAC[]));
(SUBGOAL_THEN `s/r> &0` ASSUME_TAC);
BY((MP_TAC(ARITH_RULE `s<r /\ s> &0 ==> r> &0`) THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[ARITH_RULE `a> &0 <=> &0<a`] THEN REWRITE_TAC[
REAL_LT_LDIV_EQ] THEN REWRITE_TAC[
REAL_LT_RDIV_EQ] THEN SIMP_TAC[
REAL_LT_RDIV_EQ] THEN REWRITE_TAC[ARITH_RULE `&0*r= &0`] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[ARITH_RULE `&0< s <=> s> &0`] THEN ASM_REWRITE_TAC[]));
(SUBGOAL_THEN `s/r< &1` ASSUME_TAC);
(MP_TAC(ARITH_RULE `s<r /\ s> &0 ==> r> &0`));
(ASM_REWRITE_TAC[]);
(REWRITE_TAC[ARITH_RULE `r> &0 <=> &0 <r`]);
(REWRITE_TAC[ARITH_RULE `&1 * r= r`]);
(DISCH_TAC);
(ASM_REWRITE_TAC[]);
(UNDISCH_TAC `( &0<r):bool`);
(SIMP_TAC[
REAL_LT_LDIV_EQ]);
(REWRITE_TAC[ARITH_RULE `&1*r=r`]);
(DISCH_TAC);
BY((ASM_REWRITE_TAC[]));
(UNDISCH_TAC `(x''':real^3
IN normball x r):bool`);
(REWRITE_TAC[
normball;
IN_ELIM_THM;
dist]);
(SUBGOAL_THEN `
norm (x''':real^3 - x)=
norm (--x + x''')` ASSUME_TAC);
(MP_TAC(VECTOR_ARITH `x''':real^3 - x = --x + x'''`));
(ABBREV_TAC `v1= x''':real^3 - x`);
BY((MESON_TAC[]));
(ASM_SIMP_TAC[]);
(SUBGOAL_THEN `&0<=
norm (--x + x''':real^3)` MP_TAC);
BY((SIMP_TAC[
NORM_POS_LE]));
(REWRITE_TAC[TAUT `A==>B==>C <=> A/\B==>C`]);
(MP_TAC(ARITH_RULE `s/r> &0 /\ s/r< &1==> &0<= s/r /\ s/r< &1`));
(ASM_REWRITE_TAC[]);
(REWRITE_TAC[TAUT `A==>B/\C==>D <=> A/\B/\C==>D`]);
(ABBREV_TAC `y=
norm (--x + x''':real^3)`);
(UNDISCH_TAC `(s / r < &1):bool`);
(REWRITE_TAC[TAUT `A==>B/\C/\D==>E <=> (B/\A/\C/\D==>E)`]);
(DISCH_TAC);
(SUBGOAL_THEN `s/r*y< &1*r` MP_TAC);
(UNDISCH_TAC `(&0 <= s / r /\ s / r < &1 /\ &0 <= y /\ y < r):bool`);
BY((MESON_TAC[
REAL_LT_MUL2]));
BY((MESON_TAC[ARITH_RULE `&1*r= r`]));
(REWRITE_TAC[TAUT `A/\B==>C==>D <=> A/\B/\C==>D`]);
BY((ASM_MESON_TAC[
radial_norm]));
(ASM_REWRITE_TAC[]);
(REWRITE_TAC[
normball;
IN_ELIM_THM;
dist]);
(REWRITE_TAC[VECTOR_ARITH `(x + s / r % (--x + x''')) - x= s / r % (--x + x''')`]);
(SIMP_TAC[
NORM_MUL]);
(SUBGOAL_THEN `s/r> &0` ASSUME_TAC);
BY((MP_TAC(ARITH_RULE `s<r /\ s> &0 ==> r> &0`) THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[ARITH_RULE `a> &0 <=> &0<a`] THEN REWRITE_TAC[
REAL_LT_LDIV_EQ] THEN REWRITE_TAC[
REAL_LT_RDIV_EQ] THEN SIMP_TAC[
REAL_LT_RDIV_EQ] THEN REWRITE_TAC[ARITH_RULE `&0*r= &0`] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[ARITH_RULE `&0< s <=> s> &0`] THEN ASM_REWRITE_TAC[]));
(MP_TAC(ARITH_RULE `s/r> &0==> s/r>= &0`));
(ASM_REWRITE_TAC[]);
(REWRITE_TAC[ARITH_RULE `s/r>= &0 <=> &0<= s/r`]);
(DISCH_TAC);
(SUBGOAL_THEN `abs (s / r)= s/r` MP_TAC);
BY((ASM_SIMP_TAC[
REAL_ABS_REFL]));
(SIMP_TAC[]);
(DISCH_TAC);
(UNDISCH_TAC `(x''':real^3
IN normball x r):bool`);
(REWRITE_TAC[
normball;
IN_ELIM_THM;
dist]);
(SUBGOAL_THEN `
norm (x''':real^3 - x)=
norm (--x + x''')` ASSUME_TAC);
(MP_TAC(VECTOR_ARITH `x''':real^3 - x = --x + x'''`));
(ABBREV_TAC `v2= x''':real^3 - x`);
BY((MESON_TAC[]));
(ASM_SIMP_TAC[]);
(ABBREV_TAC `p=
norm (--x + x''':real^3)`);
(DISCH_TAC);
(SUBGOAL_THEN `p*s/r< r*s/r` MP_TAC);
(MP_TAC(ARITH_RULE `s / r > &0 ==> &0< s/r`));
(ASM_REWRITE_TAC[]);
(UNDISCH_TAC `(p < r):bool` THEN REWRITE_TAC[TAUT `A==>B==>C <=> A/\B==>C`]);
BY((SIMP_TAC[
REAL_LT_RMUL]));
(REWRITE_TAC[ARITH_RULE `s/r*p<s <=> p*s/r< s`]);
(MP_TAC(ARITH_RULE `s<r/\s> &0 ==> ~(r= &0)`));
(ASM_REWRITE_TAC[]);
(REWRITE_TAC[TAUT `A==>B==>C <=> A/\B==>C`]);
BY((MESON_TAC[
REAL_DIV_LMUL]))
]);;
(* }}} *)
(*----------------------------------------------*)
(* Lemma 4.2*)
(* changed volume_props to volume_prop in the rest of this file. volume_props uses ball in the definition and volume_prop
uses normball in the definition*)
(*
let volume_prop = new_definition `volume_prop (vol:(real^3->bool)->real) =
( (!C. vol C >= &0) /\
(!Z. NULLSET Z ==> (vol Z = &0)) /\
(!X Y. measurable X /\ measurable Y /\ NULLSET (SDIFF X Y) ==> (vol X = vol Y)) /\
(!X t. (measurable X) /\ (measurable (IMAGE (scale t) X)) ==> (vol (IMAGE (scale t) X) = abs(t$1 * t$2 * t$3)*vol(X))) /\
(!X v. measurable X ==> (vol (IMAGE ((+) v) X) = vol X)) /\
(!v0 v1 v2 v3 r. (r > &0) /\ (~(collinear {v0,v1,v2})) /\ ~(collinear {v0,v1,v3}) ==> vol (solid_triangle v0 {v1,v2,v3} r) = vol_solid_triangle v0 v1 v2 v3 r) /\
(!v0 v1 v2 v3. vol(conv0 {v0,v1,v2,v3}) = vol_conv v0 v1 v2 v3) /\
(!v0 v1 v2 v3 h a. ~(collinear {v0,v1,v2}) /\ ~(collinear {v0,v1,v3}) /\ (h >= &0) /\ (a > &0) /\ (a <= &1) ==> vol(frustt v0 v1 h a INTER wedge v0 v1 v2 v3) = vol_frustt_wedge v0 v1 v2 v3 h a) /\
(!v0 v1 v2 v3 r c. ~(collinear {v0,v1,v2}) /\ ~(collinear {v0,v1,v3}) /\ (r >= &0) /\ (c >= -- (&1)) /\ (c <= &1) ==> (vol(conic_cap v0 v1 r c INTER wedge v0 v1 v2 v3) = vol_conic_cap_wedge v0 v1 v2 v3 r c)) /\
(!(a:real^3) (b:real^3). vol(rect a b) = vol_rect a b) /\
(!v0 v1 v2 v3 r. ~(collinear {v0,v1,v2}) /\ ~(collinear {v0,v1,v3}) /\ (r >= &0) ==> (vol(normball v0 r INTER wedge v0 v1 v2 v3) = vol_ball_wedge v0 v1 v2 v3 r)))`;;
*)
let volume_prop_fix = new_definition `volume_prop_fix (vol:(real^3->bool)->real) =
( (!C. measurable C ==> vol C >= &0) /\
(!Z. NULLSET Z ==> (vol Z = &0)) /\
(!X Y. measurable X /\ measurable Y /\ NULLSET (SDIFF X Y) ==> (vol X = vol Y)) /\
(!X t. (measurable X) /\ (measurable (IMAGE (scale t) X)) ==> (vol (IMAGE (scale t) X) = abs(t$1 * t$2 * t$3)*vol(X))) /\
(!X v. measurable X ==> (vol (IMAGE ((+) v) X) = vol X)) /\
(!v0 v1 v2 v3 r. (r > &0) /\ ~coplanar {v0, v1, v2, v3} ==> vol (solid_triangle v0 {v1,v2,v3} r) = vol_solid_triangle v0 v1 v2 v3 r) /\
(!v0 v1 v2 v3. vol(conv0 {v0,v1,v2,v3}) = vol_conv v0 v1 v2 v3) /\
(!v0 v1 v2 v3 h a. ~(collinear {v0,v1,v2}) /\ ~(collinear {v0,v1,v3}) /\ (h >= &0) /\ (a > &0) /\ (a <= &1) ==> vol(frustt v0 v1 h a INTER wedge v0 v1 v2 v3) = vol_frustt_wedge v0 v1 v2 v3 h a) /\
(!v0 v1 v2 v3 r c. ~(collinear {v0,v1,v2}) /\ ~(collinear {v0,v1,v3}) /\ (r >= &0) /\ (c >= -- (&1)) /\ (c <= &1) ==> (vol(conic_cap v0 v1 r c INTER wedge v0 v1 v2 v3) = vol_conic_cap_wedge v0 v1 v2 v3 r c)) /\
(!(a:real^3) (b:real^3). vol(rect a b) = vol_rect a b) /\
(!v0 v1 v2 v3 r. ~(collinear {v0,v1,v2}) /\ ~(collinear {v0,v1,v3}) /\ (r >= &0) ==> (vol(normball v0 r INTER wedge v0 v1 v2 v3) = vol_ball_wedge v0 v1 v2 v3 r)))`;;
let lemma_r_r' = prove_by_refinement(`! (C:real^3->bool) (x:real^3) r s. measurable C /\ volume_prop_fix (vol) /\ radial_norm r x C /\ (s > &0) /\ (s < r) ==> measurable (C INTER normball x s) /\ vol (C INTER normball x s)= vol (C) *(s/r) pow 3`,
[
REPEAT GEN_TAC THEN STRIP_TAC THEN CONJ_TAC;
ASM_MESON_TAC[
MEASURABLE_RULES;
measurable_normball];
SUBGOAL_THEN `C
INTER normball x s =
IMAGE ((+) x) (
IMAGE (
scale (s/r % (
vec 1)))(
IMAGE ((+) (--x)) (C
INTER normball x r)))` ASSUME_TAC;
ASM_SIMP_TAC[
trans_strech_trans_radial];
ASM_REWRITE_TAC[];
SUBGOAL_THEN `
measurable ((C:real^3->bool)
INTER normball x r)` ASSUME_TAC;
ASM_MESON_TAC[
MEASURABLE_RULES;
measurable_normball];
SUBGOAL_THEN `
measurable (
IMAGE ((+) (--x)) ((C:real^3->bool)
INTER normball x r))` ASSUME_TAC;
ASM_MESON_TAC[
MEASURABLE_RULES];
SUBGOAL_THEN `
measurable (
IMAGE (
scale (s / r %
vec 1)) (
IMAGE ((+) (--x)) (C
INTER normball x r)))` ASSUME_TAC;
ASM_MESON_TAC[
MEASURABLE_RULES];
SUBGOAL_THEN `
measurable (
IMAGE ((+) x) (
IMAGE (
scale (s / r %
vec 1)) (
IMAGE ((+) (--x)) (C
INTER normball x r))))` ASSUME_TAC;
ASM_MESON_TAC[
MEASURABLE_RULES];
ABBREV_TAC `A2:real^3->bool= (
IMAGE (
scale (s / r %
vec 1)) (
IMAGE ((+) (--x)) (C
INTER normball x r)))`;
SUBGOAL_THEN `vol (
IMAGE ((+) x) A2)=vol (A2)` MP_TAC;
UNDISCH_TAC `(
volume_prop_fix vol):bool`;
UNDISCH_TAC `(
measurable (A2:real^3->bool)):bool`;
REWRITE_TAC[TAUT `A==>B==>C <=> A/\B==>C`];
SIMP_TAC[
volume_prop_fix];
SIMP_TAC[];
DISCH_TAC;
UNDISCH_TAC `(
IMAGE (
scale (s / r %
vec 1)) (
IMAGE ((+) (--x)) (C
INTER normball x r)):real^3->bool = A2):bool`;
REWRITE_TAC[SET_RULE `
IMAGE (
scale (s / r %
vec 1)) (
IMAGE ((+) (--x)) (C
INTER normball x r)) = A2:real^3->bool <=> A2=
IMAGE (
scale (s / r %
vec 1)) (
IMAGE ((+) (--x)) (C
INTER normball x r))`];
SIMP_TAC[];
DISCH_TAC;
ABBREV_TAC `M1:real^3->bool= (
IMAGE ((+) (--x)) (C
INTER normball x r))`;
ABBREV_TAC `w:real^3= s / r %
vec 1`;
SUBGOAL_THEN `vol (
IMAGE (
scale (w:real^3)) M1)= abs (w$1*w$2*w$3)*vol (M1)` MP_TAC;
SUBGOAL_THEN `
measurable (
IMAGE (
scale w) M1)` MP_TAC;
UNDISCH_TAC `(A2 =
IMAGE (
scale w) M1:real^3->bool):bool`;
REWRITE_TAC[SET_RULE `A2 =
IMAGE (
scale w) M1 <=>
IMAGE (
scale w) M1= A2`];
SIMP_TAC[];
ASM_MESON_TAC[];
UNDISCH_TAC `(
volume_prop_fix vol):bool`;
UNDISCH_TAC `(
measurable (M1:real^3->bool)):bool`;
REWRITE_TAC[TAUT `P1 ==> P2 ==> P3 ==> P4 <=> P1 /\ P2 /\ P3 ==> P4`];
SIMP_TAC[
volume_prop_fix];
SIMP_TAC[];
DISCH_TAC;
SUBGOAL_THEN `((w:real^3)$1 = s/r)/\ (w$2 = s/r) /\ (w$3 = s/r)` MP_TAC;
REPEAT STRIP_TAC;
UNDISCH_TAC `(s / r %
vec 1 = w:real^3):bool`;
REWRITE_TAC[VECTOR_ARITH `s / r %
vec 1 = w:real^3 <=> w= s / r %
vec 1`];
SIMP_TAC[];
DISCH_TAC;
SIMP_TAC[
VECTOR_MUL_COMPONENT;DIMINDEX_3;ARITH_RULE `1<=1 /\ 1<=3`];
SIMP_TAC[
VEC_COMPONENT;DIMINDEX_3;ARITH_RULE `1<=1 /\ 1<= 3`];
ARITH_TAC;
UNDISCH_TAC `(s / r %
vec 1 = w:real^3):bool`;
REWRITE_TAC[VECTOR_ARITH `s / r %
vec 1 = w:real^3 <=> w= s / r %
vec 1`];
SIMP_TAC[];
DISCH_TAC;
SIMP_TAC[
VECTOR_MUL_COMPONENT;DIMINDEX_3;ARITH_RULE `1<=2 /\ 2<=3`];
SIMP_TAC[
VEC_COMPONENT;DIMINDEX_3;ARITH_RULE `1<=2 /\ 2<= 3`];
ARITH_TAC;
UNDISCH_TAC `(s / r %
vec 1 = w:real^3):bool`;
REWRITE_TAC[VECTOR_ARITH `s / r %
vec 1 = w:real^3 <=> w= s / r %
vec 1`];
SIMP_TAC[];
DISCH_TAC;
SIMP_TAC[
VECTOR_MUL_COMPONENT;DIMINDEX_3;ARITH_RULE `1<=3 /\ 3<=3`];
SIMP_TAC[
VEC_COMPONENT;DIMINDEX_3;ARITH_RULE `1<=3 /\ 3<= 3`];
ARITH_TAC;
SIMP_TAC[];
REWRITE_TAC[ARITH_RULE `s / r * s / r * s / r= (s/r) pow 3`];
DISCH_TAC;
SUBGOAL_THEN `s/r > &0` MP_TAC;
SUBGOAL_THEN `r> &0` MP_TAC;
UNDISCH_TAC `(s < r):bool` THEN UNDISCH_TAC `(s > &0):bool`;
REWRITE_TAC[TAUT `A==>B==>C <=> A/\B==>C`];
MESON_TAC[rduong];
REWRITE_TAC[ARITH_RULE `(r> &0 <=> &0< r) /\ (s / r > &0 <=> &0 < s/r)`];
SIMP_TAC[
REAL_LT_RDIV_EQ];
DISCH_TAC;
REWRITE_TAC[ARITH_RULE `&0*r= &0`];
ASM_REWRITE_TAC[ARITH_RULE `&0< s<=> s> &0`];
DISCH_TAC;
SUBGOAL_THEN `&0<= s/r` MP_TAC;
REWRITE_TAC[ARITH_RULE `&0 <= s / r <=> s/r >= &0`];
UNDISCH_TAC `(s / r > &0):bool`;
ARITH_TAC;
DISCH_TAC;
SUBGOAL_THEN `&0<= (s / r) pow 3` MP_TAC;
UNDISCH_TAC `(&0<=s / r):bool`;
MP_TAC(ARITH_RULE `&0 <= &0`);
REWRITE_TAC[TAUT `a==>b==>c <=> a/\b==>c`];
DISCH_TAC;
REWRITE_TAC[ARITH_RULE `&0<= (s/r) pow 3 <=> &0 pow 3<= (s/r) pow 3`];
UNDISCH_TAC `(&0 <= &0 /\ &0 <= s / r):bool`;
MP_TAC(ARITH_RULE `~(3= 0)`);
REWRITE_TAC[TAUT `a==>b==>c <=> a/\b==>c`];
SIMP_TAC[
REAL_POW_LE2];
DISCH_TAC;
SUBGOAL_THEN `abs ((s / r) pow 3)=(s / r) pow 3` MP_TAC;
SIMP_TAC[
REAL_ABS_REFL];
ASM_MESON_TAC[];
SIMP_TAC[];
DISCH_TAC;
REWRITE_TAC[ARITH_RULE `(s / r) pow 3 * vol M1= vol M1 * (s / r) pow 3`];
SUBGOAL_THEN `vol M1= vol C` MP_TAC;
UNDISCH_TAC `(
IMAGE ((+) (--x:real^3)) ((C:real^3->bool)
INTER normball x r) = (M1:real^3->bool)):bool`;
REWRITE_TAC[SET_RULE `
IMAGE ((+) (--x)) ((C:real^3->bool)
INTER normball x r) = M1 <=> M1=
IMAGE ((+) (--x)) ((C:real^3->bool)
INTER normball x r)`];
SIMP_TAC[];
DISCH_TAC;
SUBGOAL_THEN `vol (
IMAGE ((+) (--x)) (C
INTER normball x r))= vol (C
INTER normball (x:real^3) r)` MP_TAC;
UNDISCH_TAC `(
volume_prop_fix vol):bool`;
UNDISCH_TAC `(
measurable ((C:real^3->bool)
INTER normball x r)):bool`;
REWRITE_TAC[TAUT `A==>B==>C <=> A/\B==>C`];
SIMP_TAC[
volume_prop_fix];
SIMP_TAC[];
DISCH_TAC;
SUBGOAL_THEN `C
INTER normball (x:real^3) r= C` MP_TAC;
UNDISCH_TAC `(
radial_norm r (x:real^3) C):bool`;
REWRITE_TAC[
radial_norm];
REPEAT STRIP_TAC;
UNDISCH_TAC `((C:real^3->bool)
SUBSET normball (x:real^3) r):bool`;
SIMP_TAC[
SUBSET_INTER_ABSORPTION];
DISCH_TAC;
ABBREV_TAC `(E:real^3->bool)= C
INTER normball x r`;
ASM_MESON_TAC[];
ABBREV_TAC `a:real= (s / r) pow 3`;
ABBREV_TAC `a1:real= vol M1` THEN ABBREV_TAC `a2:real= vol C`;
SIMP_TAC[]
]);;
let lemma_r_r'_fix = REWRITE_RULE[VOLUME_FIX] lemma_r_r';;
(*
(* start old lemma_r_r' here *)
g `! (C:real^3->bool) (x:real^3) r s. measurable C /\ volume_prop (vol) /\ radial_norm r x C /\ (s > &0) /\ (s < r) ==> measurable (C INTER normball x s) /\ vol (C INTER normball x s)= vol (C) *(s/r) pow 3`;;
e (REPEAT GEN_TAC THEN STRIP_TAC THEN CONJ_TAC);;
e (ASM_MESON_TAC[MEASURABLE_RULES;measurable_normball]);;
e (SUBGOAL_THEN `C INTER normball x s = IMAGE ((+) x) (IMAGE (scale (s/r % (vec 1)))(IMAGE ((+) (--x)) (C INTER normball x r)))` ASSUME_TAC);;
e (ASM_SIMP_TAC[trans_strech_trans_radial]);;
e (ASM_REWRITE_TAC[]);;
e (SUBGOAL_THEN `measurable ((C:real^3->bool) INTER normball x r)` ASSUME_TAC);;
e (ASM_MESON_TAC[MEASURABLE_RULES;measurable_normball]);;
e (SUBGOAL_THEN `measurable (IMAGE ((+) (--x)) ((C:real^3->bool) INTER normball x r))` ASSUME_TAC);;
e (ASM_MESON_TAC[MEASURABLE_RULES]);;
e (SUBGOAL_THEN `measurable (IMAGE (scale (s / r % vec 1)) (IMAGE ((+) (--x)) (C INTER normball x r)))` ASSUME_TAC);;
e (ASM_MESON_TAC[MEASURABLE_RULES]);;
e (SUBGOAL_THEN `measurable (IMAGE ((+) x)
(IMAGE (scale (s / r % vec 1)) (IMAGE ((+) (--x)) (C INTER normball x r))))` ASSUME_TAC);;
e (ASM_MESON_TAC[MEASURABLE_RULES]);;
e (ABBREV_TAC `A2:real^3->bool= (IMAGE (scale (s / r % vec 1))
(IMAGE ((+) (--x)) (C INTER normball x r)))`);;
e (SUBGOAL_THEN `vol (IMAGE ((+) x) A2)=vol (A2)` MP_TAC);;
e (UNDISCH_TAC `(volume_prop vol):bool`);;
e (UNDISCH_TAC `(measurable (A2:real^3->bool)):bool`);;
e (REWRITE_TAC[TAUT `A==>B==>C <=> A/\B==>C`]);;
e (SIMP_TAC[volume_prop]);;
e (SIMP_TAC[]);;
e (DISCH_TAC);;
e (UNDISCH_TAC `(IMAGE (scale (s / r % vec 1))
(IMAGE ((+) (--x)) (C INTER normball x r)):real^3->bool =
A2):bool`);;
e (REWRITE_TAC[SET_RULE `IMAGE (scale (s / r % vec 1)) (IMAGE ((+) (--x)) (C INTER normball x r)) =
A2:real^3->bool <=> A2= IMAGE (scale (s / r % vec 1)) (IMAGE ((+) (--x)) (C INTER normball x r))`]);;
e (SIMP_TAC[]);;
e (DISCH_TAC);;
e (ABBREV_TAC `M1:real^3->bool= (IMAGE ((+) (--x)) (C INTER normball x r))`);;
e (ABBREV_TAC `w:real^3= s / r % vec 1`);;
e (SUBGOAL_THEN `vol (IMAGE (scale (w:real^3)) M1)= abs (w$1*w$2*w$3)*vol (M1)` MP_TAC);;
e (SUBGOAL_THEN `measurable (IMAGE (scale w) M1)` MP_TAC);;
e (UNDISCH_TAC `(A2 = IMAGE (scale w) M1:real^3->bool):bool`);;
e (REWRITE_TAC[SET_RULE `A2 = IMAGE (scale w) M1 <=> IMAGE (scale w) M1= A2`]);;
e (SIMP_TAC[]);;
e (ASM_MESON_TAC[]);;
e (UNDISCH_TAC `(volume_prop vol):bool`);;
e (UNDISCH_TAC `(measurable (M1:real^3->bool)):bool`);;
e (REWRITE_TAC[TAUT `P1 ==> P2 ==> P3 ==> P4 <=> P1 /\ P2 /\ P3 ==> P4`]);;
e (SIMP_TAC[volume_prop]);;
e (SIMP_TAC[]);;
e (DISCH_TAC);;
e (SUBGOAL_THEN `((w:real^3)$1 = s/r)/\ (w$2 = s/r) /\ (w$3 = s/r)` MP_TAC);;
e (REPEAT STRIP_TAC);;
e (UNDISCH_TAC `(s / r % vec 1 = w:real^3):bool`);;
e (REWRITE_TAC[VECTOR_ARITH `s / r % vec 1 = w:real^3 <=> w= s / r % vec 1`]);;
e (SIMP_TAC[]);;
e (DISCH_TAC);;
e (SIMP_TAC[VECTOR_MUL_COMPONENT;DIMINDEX_3;ARITH_RULE `1<=1 /\ 1<=3`]);;
e (SIMP_TAC[VEC_COMPONENT;DIMINDEX_3;ARITH_RULE `1<=1 /\ 1<= 3`]);;
e (ARITH_TAC);;
e (UNDISCH_TAC `(s / r % vec 1 = w:real^3):bool`);;
e (REWRITE_TAC[VECTOR_ARITH `s / r % vec 1 = w:real^3 <=> w= s / r % vec 1`]);;
e (SIMP_TAC[]);;
e (DISCH_TAC);;
e (SIMP_TAC[VECTOR_MUL_COMPONENT;DIMINDEX_3;ARITH_RULE `1<=2 /\ 2<=3`]);;
e (SIMP_TAC[VEC_COMPONENT;DIMINDEX_3;ARITH_RULE `1<=2 /\ 2<= 3`]);;
e (ARITH_TAC);;
e (UNDISCH_TAC `(s / r % vec 1 = w:real^3):bool`);;
e (REWRITE_TAC[VECTOR_ARITH `s / r % vec 1 = w:real^3 <=> w= s / r % vec 1`]);;
e (SIMP_TAC[]);;
e (DISCH_TAC);;
e (SIMP_TAC[VECTOR_MUL_COMPONENT;DIMINDEX_3;ARITH_RULE `1<=3 /\ 3<=3`]);;
e (SIMP_TAC[VEC_COMPONENT;DIMINDEX_3;ARITH_RULE `1<=3 /\ 3<= 3`]);;
e (ARITH_TAC);;
e (SIMP_TAC[]);;
e (REWRITE_TAC[ARITH_RULE `s / r * s / r * s / r= (s/r) pow 3`]);;
e (DISCH_TAC);;
e (SUBGOAL_THEN `s/r > &0` MP_TAC);;
e (SUBGOAL_THEN `r> &0` MP_TAC);;
e (UNDISCH_TAC `(s < r):bool` THEN UNDISCH_TAC `(s > &0):bool`);;
e (REWRITE_TAC[TAUT `A==>B==>C <=> A/\B==>C`]);;
e (MESON_TAC[rduong]);;
e (REWRITE_TAC[ARITH_RULE `(r> &0 <=> &0< r) /\ (s / r > &0 <=> &0 < s/r)`]);;
e (SIMP_TAC[REAL_LT_RDIV_EQ]);;
e (DISCH_TAC);;
e (REWRITE_TAC[ARITH_RULE `&0*r= &0`]);;
e (ASM_REWRITE_TAC[ARITH_RULE `&0< s<=> s> &0`]);;
e (DISCH_TAC);;
e (SUBGOAL_THEN `&0<= s/r` MP_TAC);;
e (REWRITE_TAC[ARITH_RULE `&0 <= s / r <=> s/r >= &0`]);;
e (UNDISCH_TAC `(s / r > &0):bool`);;
e (ARITH_TAC);;
e (DISCH_TAC);;
e (SUBGOAL_THEN `&0<= (s / r) pow 3` MP_TAC);;
e (UNDISCH_TAC `(&0<=s / r):bool`);;
e (MP_TAC(ARITH_RULE `&0 <= &0`));;
e (REWRITE_TAC[TAUT `a==>b==>c <=> a/\b==>c`]);;
e (DISCH_TAC);;
e (REWRITE_TAC[ARITH_RULE `&0<= (s/r) pow 3 <=> &0 pow 3<= (s/r) pow 3`]);;
e (UNDISCH_TAC `(&0 <= &0 /\ &0 <= s / r):bool`);;
e (MP_TAC(ARITH_RULE `~(3= 0)`));;
e (REWRITE_TAC[TAUT `a==>b==>c <=> a/\b==>c`]);;
e (SIMP_TAC[REAL_POW_LE2]);;
e (DISCH_TAC);;
e (SUBGOAL_THEN `abs ((s / r) pow 3)=(s / r) pow 3` MP_TAC);;
e (SIMP_TAC[REAL_ABS_REFL]);;
e (ASM_MESON_TAC[]);;
e (SIMP_TAC[]);;
e (DISCH_TAC);;
e (REWRITE_TAC[ARITH_RULE `(s / r) pow 3 * vol M1= vol M1 * (s / r) pow 3`]);;
e (SUBGOAL_THEN `vol M1= vol C` MP_TAC);;
e (UNDISCH_TAC `(IMAGE ((+) (--x:real^3)) ((C:real^3->bool) INTER normball x r) = (M1:real^3->bool)):bool`);;
e (REWRITE_TAC[SET_RULE `IMAGE ((+) (--x)) ((C:real^3->bool) INTER normball x r) = M1 <=> M1= IMAGE ((+) (--x)) ((C:real^3->bool) INTER normball x r)`]);;
e (SIMP_TAC[]);;
e (DISCH_TAC);;
e (SUBGOAL_THEN `vol (IMAGE ((+) (--x)) (C INTER normball x r))= vol (C INTER normball (x:real^3) r)` MP_TAC);;
e (UNDISCH_TAC `(volume_prop vol):bool`);;
e (UNDISCH_TAC `(measurable ((C:real^3->bool) INTER normball x r)):bool`);;
e (REWRITE_TAC[TAUT `A==>B==>C <=> A/\B==>C`]);;
e (SIMP_TAC[volume_prop]);;
e (SIMP_TAC[]);;
e (DISCH_TAC);;
e (SUBGOAL_THEN `C INTER normball (x:real^3) r= C` MP_TAC);;
e (UNDISCH_TAC `(radial_norm r (x:real^3) C):bool`);;
e (REWRITE_TAC[radial_norm]);;
e (REPEAT STRIP_TAC);;
e (UNDISCH_TAC `((C:real^3->bool) SUBSET normball (x:real^3) r):bool`);;
e (SIMP_TAC[SUBSET_INTER_ABSORPTION]);;
e (DISCH_TAC);;
e (ABBREV_TAC `(E:real^3->bool)= C INTER normball x r`);;
e (ASM_MESON_TAC[]);;
e (ABBREV_TAC `a:real= (s / r) pow 3`);;
e (ABBREV_TAC `a1:real= vol M1` THEN ABBREV_TAC `a2:real= vol C`);;
e (SIMP_TAC[]);;
let lemma_r_r'=top_thm();;
*)
(*------------------------ Definition of Solid angle ---------------------------------------------------------*)
(* redone by thales below on 2010-06-06 :
let pre_def1_4_3=prove(`!(C:real^3->bool)(x:real^3). volume_prop_fix (vol) /\ measurable C /\ eventually_radial_norm x C ==> (?s. ?c. (c > &0) /\ (!r. (r > &0) /\ (r < c) ==> (s= &3 * vol(C INTER normball x r)/(r pow 3)))) `,
(REPEAT GEN_TAC)
THEN (REWRITE_TAC[eventually_radial_norm])
THEN (REPEAT STRIP_TAC)
THEN (EXISTS_TAC `(&3* vol (C INTER normball x r) / r pow 3):real`)
THEN (EXISTS_TAC `(r:real)`)
THEN (ASM_REWRITE_TAC[])
THEN (GEN_TAC)
THEN (REPEAT STRIP_TAC)
THEN (REWRITE_TAC[REAL_ARITH `&3 * vol (C INTER normball x r) / r pow 3 = &3 * vol (C INTER normball x r') / r' pow 3 <=> vol (C INTER normball x r) / r pow 3 = vol (C INTER normball x r') / r' pow 3`])
THEN (SUBGOAL_THEN `(C:real^3->bool) INTER normball x r'= (C INTER normball x r) INTER normball x r'` MP_TAC)
THENL[ASM_MESON_TAC[normball_eq];SIMP_TAC[]]
THEN DISCH_TAC
THEN (SUBGOAL_THEN `measurable ((C:real^3->bool) INTER normball x r)` ASSUME_TAC)
THENL[ASM_MESON_TAC[MEASURABLE_RULES;measurable_normball];(SUBGOAL_THEN `vol ((C INTER normball x r) INTER normball x r')= vol (C INTER normball x r) * (r'/r) pow 3` MP_TAC)]
THENL[ASM_MESON_TAC[lemma_r_r'];ABBREV_TAC `(a:real)=vol (C INTER normball x r)`]
THEN ABBREV_TAC `(b:real)=vol ((C INTER normball x r) INTER normball x r')`
THEN SIMP_TAC[]
THEN DISCH_TAC
THEN SIMP_TAC[REAL_POW_DIV]
THEN MP_TAC(REAL_ARITH `r'> &0 ==> ~(r'= &0)`)
THEN ASM_REWRITE_TAC[]
THEN DISCH_TAC
THEN MP_TAC(MESON[REAL_POW_NZ] `~(r'= &0)==> ~(r' pow 3= &0)`)
THEN ASM_REWRITE_TAC[]
THEN DISCH_TAC
THEN REWRITE_TAC[REAL_ARITH `(a * r' pow 3 / r pow 3) / r' pow 3= (a * r' pow 3/ r' pow 3)/ r pow 3`]
THEN MP_TAC(MESON[REAL_DIV_REFL] `~(r' pow 3 = &0)==> r' pow 3 / r' pow 3= &1`)
THEN ASM_REWRITE_TAC[]
THEN SIMP_TAC[]
THEN DISCH_TAC
THEN ARITH_TAC);;
let pre_def_4_3=REWRITE_RULE[VOLUME_FIX] (prove(`?(s:(real^3->bool)->real^3 -> real). !C x. volume_prop_fix vol /\ measurable C /\ eventually_radial_norm x C ==> (?r'.r' > &0 /\(!r. r > &0 /\ r < r' ==> s C x = &3 * vol (C INTER normball x r) / r pow 3))`,MESON_TAC[SKOLEM_THM;pre_def1_4_3]));;
let sol= new_specification ["sol"] pre_def_4_3;;
*)
(*
A big part of the proof is devoted to this identity
`(b = a * (r'/r) pow 3 ) /\ (r > &0) /\ (r' > &0) ==> a / r pow 3 = b / r' pow 3`;; *)
(*
let pre_def1_4_3=prove_by_refinement(
` !(C:real^3->bool) x.
volume_prop_fix vol /\
(?r. r > &0 /\
measurable (C INTER normball x r) /\
radial_norm r x (C INTER normball x r))
==> (?s c.
c > &0 /\
(!r. r > &0 /\ r < c
==> s = &3 * vol (C INTER normball x r) / r pow 3))`,
[
(REPEAT STRIP_TAC) ;
(EXISTS_TAC `(&3* vol (C INTER normball x r) / r pow 3):real`) ;
(EXISTS_TAC `(r:real)`) ;
(ASM_REWRITE_TAC[]) ;
(REPEAT STRIP_TAC) ;
(REWRITE_TAC[REAL_ARITH `(&3 * x = &3 *y) = (x = y)`]) ;
(SUBGOAL_THEN `(C:real^3->bool) INTER normball x r'= (C INTER normball x r) INTER normball x r'` MP_TAC) THENL[ASM_MESON_TAC[normball_eq];SIMP_TAC[]] ;
DISCH_TAC ;
(* (SUBGOAL_THEN `measurable ((C:real^3->bool) INTER normball x r)` ASSUME_TAC) THENL[ASM_MESON_TAC[MEASURABLE_RULES;measurable_normball]; *)
(SUBGOAL_THEN `vol ((C INTER normball x r) INTER normball x r')= vol (C INTER normball x r) * (r'/r) pow 3` MP_TAC);
ASM_MESON_TAC[lemma_r_r';radial_normball];
ABBREV_TAC `(a:real)=vol (C INTER normball x r)`;
ABBREV_TAC `(b:real)=vol ((C INTER normball x r) INTER normball x r')` ;
SIMP_TAC[] ;
DISCH_TAC ;
SIMP_TAC[REAL_POW_DIV] ;
MP_TAC(REAL_ARITH `r'> &0 ==> ~(r'= &0)`) ;
ASM_REWRITE_TAC[] ;
DISCH_TAC ;
MP_TAC(MESON[REAL_POW_NZ] `~(r'= &0)==> ~(r' pow 3= &0)`) ;
ASM_REWRITE_TAC[] ;
DISCH_TAC ;
REWRITE_TAC[REAL_ARITH `(a * r' pow 3 / r pow 3) / r' pow 3= (a * r' pow 3/ r' pow 3)/ r pow 3`] ;
MP_TAC(MESON[REAL_DIV_REFL] `~(r' pow 3 = &0)==> r' pow 3 / r' pow 3= &1`) ;
ASM_REWRITE_TAC[] ;
SIMP_TAC[] ;
DISCH_TAC ;
ARITH_TAC;
]);;
*)
(*
A big part of the proof of pre_def1_4_3 is devoted to this identity
*)
let pow3_identity = prove_by_refinement(
`(b = a * (r'/r) pow 3 ) /\ (r > &0) /\ (r' > &0) ==> a / r pow 3 = b / r' pow 3`,
[
SIMP_TAC[
REAL_POW_DIV] ;
MP_TAC(REAL_ARITH `r'> &0 ==> ~(r'= &0)`) ;
MP_TAC(MESON[
REAL_POW_NZ;
REAL_DIV_REFL] `~(r'= &0)==> r' pow 3 / r' pow 3= &1`) ;
REWRITE_TAC[REAL_ARITH `(a * b / c) / b= (a * b/ b)/ c`] ;
SIMP_TAC[] ;
ARITH_TAC;
]);;
(*
let pre_def1_4_3=prove_by_refinement(
` !(C:real^3->bool) x.
volume_prop_fix vol /\
(?r. r > &0 /\
measurable (C INTER normball x r) /\
radial_norm r x (C INTER normball x r))
==> (?s c.
c > &0 /\
(!r. r > &0 /\ r < c
==> s = &3 * vol (C INTER normball x r) / r pow 3))`,
[
(REPEAT STRIP_TAC) ;
(EXISTS_TAC `(&3* vol (C INTER normball x r) / r pow 3):real`) ;
(EXISTS_TAC `(r:real)`) ;
(ASM_REWRITE_TAC[]) ;
(REPEAT STRIP_TAC) ;
(REWRITE_TAC[REAL_ARITH `(&3 * x = &3 *y) = (x = y)`]) ;
(SUBGOAL_THEN `(C:real^3->bool) INTER normball x r'= (C INTER normball x r) INTER normball x r'` MP_TAC) THENL[ASM_MESON_TAC[normball_eq];SIMP_TAC[]] ;
DISCH_TAC ;
(SUBGOAL_THEN `vol ((C INTER normball x r) INTER normball x r')= vol (C INTER normball x r) * (r'/r) pow 3` MP_TAC);
ASM_MESON_TAC[lemma_r_r';radial_normball];
DISCH_TAC THEN ASM_REWRITE_TAC[];
ASM_MESON_TAC[pow3_identity];
]);;
*)
radial_normball];
DISCH_TAC THEN ASM_REWRITE_TAC[];
ASM_MESON_TAC[pow3_identity];
FIRST_X_ASSUM DISJ_CASES_TAC;
(SUBGOAL_THEN `(C:real^3->bool) INTER normball x r= (C INTER normball x t) INTER normball x r` MP_TAC) THENL[ASM_MESON_TAC[normball_eq];SIMP_TAC[]] ;
DISCH_TAC ;
(SUBGOAL_THEN `vol ((C INTER normball x t) INTER normball x r)= vol (C INTER normball x t) * (r/t) pow 3` MP_TAC);
ASM_MESON_TAC[lemma_r_r';radial_normball];
DISCH_TAC THEN ASM_REWRITE_TAC[];
ASM_MESON_TAC[pow3_identity];
ASM_REWRITE_TAC[];
]);;
(*
let pre_def_4_3=REWRITE_RULE[VOLUME_FIX] (prove(`?(s:(real^3->bool)->real^3 -> real). !C x. (?r. (r > &0) /\ measurable (C INTER normball x r) /\ radial_norm r x (C INTER normball x r)) ==> (?r'.r' > &0 /\(!r. r > &0 /\ r < r' ==> s C x = &3 * vol (C INTER normball x r) / r pow 3))`,MESON_TAC[VOLUME_FIX;SKOLEM_THM;pre_def1_4_3]));;
*)
let pre_def_4_3b=REWRITE_RULE[VOLUME_FIX;SKOLEM_THM]
pre_def1_4_3b;;
(* }}} *)
(*
let sol= new_specification ["sol"] pre_def_4_3b;;
*)
(* }}} *)
let AFF_GT_1_3=prove(`!x u v w.
DISJOINT {x} {u, v, w}
==> aff_gt {x} {u, v, w} =
{y | ?t1 t2 t3 t4.
&0 < t2 /\
&0 < t3 /\
&0 < t4 /\
t1 + t2 + t3 +t4= &1 /\
y = t1 % x + t2 %u + t3 % v + t4 % w}`,
AFF_TAC);;
(* insert in vol1.hl after solid angle *)
let aff_gt_radial = prove_by_refinement(`!x u v w r.
(DISJOINT {(x:real^B)} {u,v,w} /\ (r > &0) ) ==>
radial_norm r x (aff_gt {x} {u,v,w} INTER normball x r)`,
[
REWRITE_TAC[
radial_norm];
REPEAT STRIP_TAC;
SET_TAC[];
UNDISCH_TAC `(x:real^B) + u'
IN aff_gt {x} {u, v, w}
INTER normball x r`;
ASM_SIMP_TAC[
AFF_GT_1_3];
REWRITE_TAC[
IN_ELIM_THM;
IN_INTER];
REPEAT STRIP_TAC;
EXISTS_TAC `&1 + (t:real) *
t1 - t`;
EXISTS_TAC `(t:real) * t2`;
EXISTS_TAC `(t:real) * t3`;
EXISTS_TAC `(t:real) * t4`;
SUBGOAL_THEN `&0 < t * t2 /\ &0 < t * t3 /\ &0 < t * t4` (fun t -> REWRITE_TAC[t]);
ASM_MESON_TAC[
REAL_MUL_POS_LT;REAL_ARITH `r > &0 <=> &0 < r`];
CONJ_TAC;
SUBGOAL_THEN `(&1 + t *
t1 - t) + t * t2 + t * t3 + t * t4 = &1 - t + t * (
t1 + t2 + t3 + t4)` (fun t-> ASM_REWRITE_TAC[t]);
REAL_ARITH_TAC;
REAL_ARITH_TAC;
ONCE_REWRITE_TAC[ VECTOR_ARITH `( &1 + t *
t1 - t) % (x:real^B) + (t * t2) % u + (t * t3) % v + (t * t4) % w = x - t % x + t % (
t1 % x + t2 % u + t3 % v + t4 % w)`];
UNDISCH_TAC `(x:real^B) + u' =
t1 % x + t2 % u + t3 % v + t4 % w`;
DISCH_THEN(fun
thm -> ONCE_REWRITE_TAC[GSYM
thm]);
VECTOR_ARITH_TAC;
MATCH_MP_TAC
aff_normball;
ASM_REWRITE_TAC[];
]);;
(*---------------------------------------------------------------------------------------------------------------*)
(*Lemma 4.3*)
(*4.2.11 combining solid angle and volume*)
(* removed by thales, nov 11, 2008. Conflicts with definition of phi already provided *)
(*
let phi=new_definition `phi(h:real,t:real,l:real^2)= l$1*t*h*(t+h)/ &6 + l$2`;;
let A=new_definition `A(h:real,t:real,l:real^2)=(&1-h/t)*(phi (h,t,l)-phi (t,t,l))`;;
*)
(*-------------------------------------------------------------------------------------*)
(* Finiteness *)
(*-------------------------------------------------------------------------------------*)
(*------------------------------------------------------*)
(* Useful definitions *)
(*------------------------------------------------------*)
(*
let hinhcau=new_definition `hinhcau (x:real^3) (r:real)={y: real^3 | norm ( x - y ) < r } `;;
*)
(* }}} *)
(*
let map0=new_definition `map0 = \(c:real^3). cube c`;;
*)
(*
let map0 = new_definition `map0 = cube`;;
*)
(*-------------------------------------------------------*)
(* Somes lemmas *)
(*-------------------------------------------------------*)
let component_hinhcau_bound=prove(`! (p:real^3) (r:real) x. x IN hinhcau p r ==> (!i. (1 <= i) /\ ( i <= 3 ) ==> ( p$i - r <= x$i ) /\ ( x$i <= p$i + r))`,REPEAT GEN_TAC THEN REWRITE_TAC[hinhcau] THEN REWRITE_TAC[
IN_ELIM_THM] THEN REWRITE_TAC[REAL_ARITH `(p$i):real - r <= x$i <=> p$i - x$i <= r`; REAL_ARITH `a:real <= b+c <=> -- c <= b-a`] THEN REWRITE_TAC[MESON[] `C/\B <=> B/\ C`] THEN REWRITE_TAC[GSYM
REAL_ABS_BOUNDS] THEN REWRITE_TAC[MESON[] `C/\B <=> B/\ C`] THEN REPEAT STRIP_TAC THEN MP_TAC(SPECL [`p - x:real^3`; `i:num`]
COMPONENT_LE_NORM_3) THEN ASM_REWRITE_TAC[] THEN UNDISCH_TAC `(
norm (p:real^3 - x) < r):bool` THEN REWRITE_TAC[
VECTOR_SUB_COMPONENT] THEN REAL_ARITH_TAC);;
(*
let finite_int_interval=prove(`! a:real b. FINITE (int_interval a b)`,REPEAT GEN_TAC THEN ASSUME_TAC (GSYM INTEGER_IS_INT) THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[INTEGER_IS_INT;FINITE_INTSEG] THEN REWRITE_TAC[int_interval] THEN ASM_REWRITE_TAC[] THEN SIMP_TAC[FINITE_INTSEG]);;
*)
let trip_eq=prove(`! (x:real^3) (y:real^3). x$1, x$2, x$3= y$1,y$2,y$3 <=> !i. 1<= i /\ i<=3 ==> x$i= y$i `,REPEAT GEN_TAC THEN REWRITE_TAC[
PAIR_EQ] THEN REWRITE_TAC[ARITH_RULE `1<=i /\ i<= 3 <=> i=1 \/ i=2 \/ i=3`] THEN MESON_TAC[]);;
let FINITE_IMAGE_INJ=prove(`! (h:real^3->B) (s:real^3 ->bool) t. (!(x:real^3). x IN s ==> h x IN t) /\ INJ h s t /\ FINITE t ==> FINITE s`,
REPEAT GEN_TAC THEN REWRITE_TAC[
INJ] THEN SIMP_TAC[MESON[] `p /\ (p /\ q) /\ w <=> p /\ q /\ w`] THEN STRIP_TAC
THEN SUBGOAL_THEN `s= { x:real^3 | x
IN s /\ (h:real^3->B) x
IN t}` ASSUME_TAC
THENL [REWRITE_TAC[GSYM
SUBSET_ANTISYM_EQ];ASM_MESON_TAC[
FINITE_IMAGE_INJ_GENERAL]]
THEN REWRITE_TAC[SET_RULE `{x | x
IN s /\ (h:real^3->B) x
IN t}
SUBSET s`] THEN REWRITE_TAC[
SUBSET] THEN REWRITE_TAC[
IN_ELIM_THM] THEN ASM_SIMP_TAC[]);;
(*----------------------------------------------------------*)
(* Finiteness of integer points in a ball *)
(*----------------------------------------------------------*)
(*----------------------------------------------------------*)
(* Needed lemmas *)
(*----------------------------------------------------------*)
let disjoint_line_interval=prove(`!(x:real) (y:real). integer x /\ integer y /\ (? (z:real). x< z /\ z< x+ &1 /\ y<z /\ z< y+ &1) ==> x= y`,
(*
REPEAT GEN_TAC THEN SIMP_TAC[GSYM INTEGER_IS_INT] THEN REPEAT STRIP_TAC THEN MP_TAC(SPECL [`x:real`;`y:real`] REAL_LE_CASES_INTEGERS)
-- 2/16/2011. *)
REPEAT GEN_TAC THEN SIMP_TAC[] THEN REPEAT STRIP_TAC THEN MP_TAC(SPECL [`x:real`;`y:real`]
REAL_LE_CASES_INTEGERS)
THEN ASM_SIMP_TAC[] THEN ASM_SIMP_TAC[SPECL [`x:real`;`y:real`]
REAL_LE_INTEGERS] THEN SIMP_TAC[MESON[] `(((P\/Q)\/R ==> P) <=> (Q\/R ==> P))`]
THEN STRIP_TAC
THENL [UNDISCH_TAC `(y:real <z):bool` THEN UNDISCH_TAC `(z:real< x+ &1):bool`;UNDISCH_TAC `(x:real <z):bool` THEN UNDISCH_TAC `(z:real< y+ &1):bool`]
THENL [REWRITE_TAC[MESON[] `P ==> Q ==> R <=> Q /\ P ==> R`] THEN DISCH_TAC THEN MP_TAC(REAL_ARITH ` (y:real) < z /\ (z:real) < x+ &1 ==> y< x+ &1 `);REWRITE_TAC[MESON[] `P ==> Q ==> R <=> Q /\ P ==> R`] THEN DISCH_TAC THEN MP_TAC(REAL_ARITH ` (x:real) < z /\ (z:real) < y+ &1 ==> x< y+ &1 `)]
THENL [ASM_SIMP_TAC[];ASM_SIMP_TAC[]]
THENL [UNDISCH_TAC `(x + &1 <= y:real):bool` THEN REWRITE_TAC[MESON[] `P ==> Q ==> R <=> Q /\ P ==> R`];UNDISCH_TAC `(y + &1 <= x:real):bool` THEN REWRITE_TAC[MESON[] `P ==> Q ==> R <=> Q /\ P ==> R`]]
THENL [MESON_TAC[REAL_ARITH `a:real < b /\ b<= a ==> F`];MESON_TAC[REAL_ARITH `a:real < b /\ b<= a ==> F`]]);;
let vector_eq2=prove(`!(x:real^3) (y:real^3). (!i. 1 <= i /\ i <= 3 ==> x$i = y$i) ==> x = y `,
(*-----------------------------------------------------------*)
(* Bijectivity of map from int_ball to set_of_cube *)
(*-----------------------------------------------------------*)
(*-----------------------------------------------------------*)
(* in line 997 changed t to emoi, esusick 11/12 *)
let product_3=prove(`!(f:num -> real). product (1..3) f= f 1 * f 2 * f 3 `, let emoi= CONJUNCT2
PRODUCT_CLAUSES in
GEN_TAC THEN MP_TAC(GSYM (SPECL [`1:num`;`3:num`]
NUMSEG_RREC))
THEN SIMP_TAC[ARITH_RULE `1<= 3`;ARITH_RULE `3-1 = 2`]
THEN REPEAT DISCH_TAC
THEN MP_TAC(ISPECL [`3:num`;`f:num ->
real`;`((1..2)):num ->bool`] emoi)
THEN SIMP_TAC[MESON[
NUMSEG_RREC;
FINITE_NUMSEG] `FINITE (1..2)`]
THEN SIMP_TAC[MESON[
IN_NUMSEG;ARITH_RULE `~ (3<=2)`] ` ~( 3
IN (1..2))`]
THEN DISCH_TAC
THEN MP_TAC(GSYM (SPECL [`1:num`;`2:num`]
NUMSEG_RREC))
THEN SIMP_TAC[ARITH_RULE `1<=2`;ARITH_RULE `2-1=1`]
THEN MP_TAC(ISPECL [`2:num`;`f:num ->
real`;`((1..1)):num ->bool`] emoi)
THEN SIMP_TAC[MESON[
NUMSEG_RREC;
FINITE_NUMSEG] `FINITE (1..1)`]
THEN SIMP_TAC[MESON[
IN_NUMSEG;ARITH_RULE `~ (2<=1)`] ` ~( 2
IN (1..1))`]
THEN SIMP_TAC[SPECL [`f : num ->
real`;`1:num`]
PRODUCT_SING_NUMSEG] THEN REAL_ARITH_TAC);;
(*------------------------------------------------------------------*)
(* Measures of cube and union of cubes *)
(*------------------------------------------------------------------*)
(*Negligiblity of intersection of cubes *)
(*There are two different theorems about SUM_CONST*)
(*-----------------------------------------------------------------*)
(* Union of cubes is contained in ball *)
(*-----------------------------------------------------------------*)
let pow_lesthan_1=prove( `!(a:real). &0 < a /\ a < &1 ==> a*a < &1`,REPEAT STRIP_TAC THEN MP_TAC(SPECL [`a:real`;`a:real`;`&1:real`]
REAL_LT_LMUL) THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[REAL_ARITH `(x:real)* &1= x`;REAL_ARITH `a:real <b /\ b< c ==> a< c`]);;
let cube_to_ball=prove(`!(x:real^3) (y:real^3). y IN cube x ==> norm (x-y)< sqrt(&3)`,
REPEAT STRIP_TAC THEN MP_TAC(ISPEC `(x-y):real^3`
NORM_POS_LE)
THEN MP_TAC (SPEC `&3:real`
SQRT_POS_LE) THEN ASM_REWRITE_TAC[REAL_ARITH `&0<= &3`;REAL_ARITH `&0<A ==> A= abs (A)`]
THEN ONCE_REWRITE_TAC[GSYM
REAL_ABS_REFL]
THEN ONCE_REWRITE_TAC[MESON[] `a= b <=> b=a`]
THEN REWRITE_TAC[MESON[] `((a:real) = b ==> (c:real) = d ==> c< a ) <=> ((a:real) = b ==> (c:real) = d ==> d< b )`]
THEN REWRITE_TAC[
REAL_LT_SQUARE_ABS] THEN SIMP_TAC[
SQRT_POW_2; REAL_ARITH `&0<= &3`]
THEN SIMP_TAC[
NORM_POW_2;
DOT_3] THEN REWRITE_TAC[
VECTOR_SUB_COMPONENT] THEN UNDISCH_TAC `(y
IN cube (x:real^3)):bool`
THEN REWRITE_TAC[cube;
IN_ELIM_THM] THEN REWRITE_TAC[
FORALL_3]
THEN REWRITE_TAC[REAL_ARITH `(a:real) <b /\ b< a+ &1 <=> &0< b-a /\ b-a < &1`]
THEN ONCE_REWRITE_TAC[REAL_FIELD `((x:real^3)$1 - (y:real^3)$1) * (x$1 - y$1) +
(x$2 - y$2) * (x$2 - y$2) +
(x$3 - y$3) * (x$3 - y$3)= (y$1 - x$1) * (y$1 - x$1) +
(y$2 - x$2) * (y$2 - x$2) +
(y$3 - x$3) * (y$3 - x$3)`]
THEN REPEAT STRIP_TAC THEN MP_TAC(MESON[
pow_lesthan_1] `&0 < (y:real^3)$1 - (x:real^3)$1 /\ y$1 - x$1 < &1 ==> (y$1 - x$1) * (y$1 - x$1)< &1`)
THEN ASM_REWRITE_TAC[]
THEN MP_TAC(MESON[
pow_lesthan_1] `&0 < (y:real^3)$2 - (x:real^3)$2 /\ y$2 - x$2 < &1 ==> (y$2 - x$2) * (y$2 - x$2)< &1`) THEN ASM_REWRITE_TAC[]
THEN MP_TAC(MESON[
pow_lesthan_1] `&0 < (y:real^3)$3 - (x:real^3)$3 /\ y$3 - x$3 < &1 ==> (y$3 - x$3) * (y$3 - x$3)< &1`) THEN ASM_REWRITE_TAC[]
THEN MESON_TAC[REAL_ARITH `(a:real)< &1 /\ b< &1 /\c < &1 ==> a+b+c < &3`]);;
let unions_cube_subset_ball=prove(`!(x:real^3) (r:real). UNIONS (set_of_cube (int_ball x r)) SUBSET (hinhcau x (r+ sqrt (&3)))`,REPEAT GEN_TAC THEN REWRITE_TAC[
SUBSET;
UNIONS]
THEN GEN_TAC THEN REWRITE_TAC[hinhcau;
IN_ELIM_THM]
THEN DISCH_TAC THEN FIRST_X_ASSUM CHOOSE_TAC
THEN UNDISCH_TAC `(u
IN set_of_cube (
int_ball x r) /\ (x':real^3)
IN u):bool`
THEN REWRITE_TAC[
set_of_cube] THEN REWRITE_TAC[
IN_ELIM_THM] THEN REPEAT STRIP_TAC
THEN UNDISCH_TAC `((x':real^3)
IN u):bool` THEN ASM_REWRITE_TAC[]
THEN DISCH_TAC THEN MP_TAC(SPECL [`x'':real^3`;`x':real^3`]
cube_to_ball) THEN ASM_REWRITE_TAC[]
THEN UNDISCH_TAC `(x''
IN int_ball (x:real^3) r):bool`
THEN REWRITE_TAC[
int_ball;
IN_INTER] THEN STRIP_TAC
THEN MP_TAC(MESON[hinhcau;
IN_ELIM_THM] `(x'':real^3)
IN (hinhcau x r) ==>
norm (x - x'') < r`) THEN ASM_REWRITE_TAC[]
THEN ONCE_REWRITE_TAC[MESON[VECTOR_ARITH `(x:real^3)- x' = (x - x'') + (x'' - x')`] `
norm ((x:real^3) - x') < r +
sqrt (&3) <=>
norm ((x - x'') + (x'' - x')) < r +
sqrt (&3)`]
THEN MESON_TAC[ISPECL [`(x - x''):real^3`;`(x'' - x'):real^3`]
NORM_TRIANGLE;REAL_ARITH `((e:real) <= (a + c)) /\a <b /\ c< d ==> e < b+ d`]);;
(*-----------------------------------------------------------------*)
(*-----------------------------------------------------------------------*)
(*Lemma 2.14 [WQZISRI]:Upperbound for number of integer points in a ball *)
(*-----------------------------------------------------------------------*)
(*------------------------------------------------------------------------*)
(* There are two different theorems about SUM_EQ and sum *)
REAL_LE_SQUARE_ABS;;
REAL_ABS_REFL;;
let pow_lesthan_eq_1=prove( `!(a:real). &0 <= a /\ a <= &1 ==> a*a <= &1`,REPEAT STRIP_TAC THEN MP_TAC(SPECL [`a:real`;`a:real`;`&1:real`]
REAL_LE_LMUL) THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[REAL_ARITH `(x:real)* &1= x`;REAL_ARITH `a:real <=b /\ b<= c ==> a<= c`]);;
let ccube_to_ball=prove(`!(x:real^3) (y:real^3). y IN ccube x ==> norm (x-y)<= sqrt(&3)`,
REPEAT STRIP_TAC THEN MP_TAC(ISPEC `((x:real^3)-y):real^3`
NORM_POS_LE)
THEN MP_TAC (SPEC `&3:real`
SQRT_POS_LE) THEN ASM_REWRITE_TAC[REAL_ARITH `&0<= &3`;REAL_ARITH `&0<A ==> A= abs (A)`]
THEN ONCE_REWRITE_TAC[GSYM
REAL_ABS_REFL]
THEN ONCE_REWRITE_TAC[MESON[] `(a:real)= b <=> b=a`]
THEN REWRITE_TAC[MESON[] `((a:real) = b ==> (c:real) = d ==> c<= a ) <=> ((a:real) = b ==> (c:real) = d ==> d<= b )`]
THEN REWRITE_TAC[
REAL_LE_SQUARE_ABS] THEN SIMP_TAC[
SQRT_POW_2; REAL_ARITH `&0<= &3`]
THEN SIMP_TAC[
NORM_POW_2;
DOT_3] THEN REWRITE_TAC[
VECTOR_SUB_COMPONENT] THEN UNDISCH_TAC `(y
IN ccube (x:real^3)):bool`
THEN REWRITE_TAC[ccube;
IN_ELIM_THM] THEN REWRITE_TAC[
FORALL_3]
THEN REWRITE_TAC[REAL_ARITH `(a:real) <=b /\ b<= a+ &1 <=> &0<= b-a /\ b-a <= &1`]
THEN ONCE_REWRITE_TAC[REAL_FIELD `((x:real^3)$1 - (y:real^3)$1) * (x$1 - y$1) +
(x$2 - y$2) * (x$2 - y$2) +
(x$3 - y$3) * (x$3 - y$3)= (y$1 - x$1) * (y$1 - x$1) +
(y$2 - x$2) * (y$2 - x$2) +
(y$3 - x$3) * (y$3 - x$3)`]
THEN REPEAT STRIP_TAC THEN MP_TAC(MESON[
pow_lesthan_eq_1] `&0 <= (y:real^3)$1 - (x:real^3)$1 /\ y$1 - x$1 <= &1 ==> (y$1 - x$1) * (y$1 - x$1)<= &1`)
THEN ASM_REWRITE_TAC[]
THEN MP_TAC(MESON[
pow_lesthan_eq_1] `&0 <= (y:real^3)$2 - (x:real^3)$2 /\ y$2 - x$2 <= &1 ==> (y$2 - x$2) * (y$2 - x$2)<= &1`) THEN ASM_REWRITE_TAC[]
THEN MP_TAC(MESON[
pow_lesthan_eq_1] `&0 <= (y:real^3)$3 - (x:real^3)$3 /\ y$3 - x$3 <= &1 ==> (y$3 - x$3) * (y$3 - x$3)<= &1`) THEN ASM_REWRITE_TAC[] THEN MESON_TAC[REAL_ARITH `(a:real)<= &1 /\ b<= &1 /\c <= &1 ==> a+b+c <= &3`]);;
(*-----------------------------------------------------------------------*)
(* Lemma 2.15 [PWVIIOL] lower bound for number of integer points in ball *)
(*-----------------------------------------------------------------------*)
(*-----------------------------------------------------------------------*)
let card_int_ball_le=prove( `!(x:real^3)(k1:real)(k2:real)(r:real).(&0<k1 /\ &0<k2 /\ k2+ sqrt(&3)<= r) ==> &(CARD (int_ball x (r + k1))) <=
&4 / &3 * pi * ((r + k1) + sqrt (&3)) pow 3`,REPEAT STRIP_TAC THEN MP_TAC(SPECL [`x:real^3`;`r+ k1:real`]
WQZISRI) THEN MP_TAC(REAL_ARITH `&0<k1 /\ &0<k2 /\ k2+
sqrt(&3)<= r ==>
sqrt(&3)< r+k1`) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN MP_TAC(MESON[SPEC `&3:real`
SQRT_POS_LE;REAL_ARITH `&0 <= &3`] `&0<=
sqrt(&3)`) THEN DISCH_TAC THEN MP_TAC(REAL_ARITH `&0 <=
sqrt (&3) /\ (
sqrt (&3) < r + k1) ==> &0<= r+ k1`) THEN ASM_REWRITE_TAC[] THEN SIMP_TAC[]);;
let card_int_ball_le2=prove( `!(x:real^3)(k1:real)(r:real).(&0<=k1 /\ &0<= r) ==> &(CARD (int_ball x (r + k1))) <=
&4 / &3 * pi * ((r + k1) + sqrt (&3)) pow 3`,REPEAT STRIP_TAC THEN MP_TAC(SPECL [`x:real^3`;`r+ k1:real`]
WQZISRI) THEN MP_TAC(REAL_ARITH `&0<=k1 /\ &0<= r ==> &0<= r+k1`) THEN ASM_REWRITE_TAC[] THEN MESON_TAC[]);;
let card_int_ball_pos=prove(`!(x:real^3)(k1:real)(k2:real)(r:real).(&0<k1 /\ &0<k2 /\ k2+ sqrt(&3)<= r) ==> &4 / &3 * pi * ((r - k2) - sqrt (&3)) pow 3 <= &(CARD (int_ball x (r - k2)))`,REPEAT STRIP_TAC THEN MP_TAC(SPECL [`x:real^3`;`r- k2:real`]
PWVIIOL) THEN MP_TAC(REAL_ARITH `k2 +
sqrt (&3) <= r ==>
sqrt(&3)<= r- k2`) THEN ASM_REWRITE_TAC[] THEN SIMP_TAC[]);;
let bdt1_finiteness=prove(`!(r:real)(k:real). &0<r ==> &4*pi*r*k <= &4*pi*r* abs k`,REPEAT STRIP_TAC
THEN ASSUME_TAC
PI_POS THEN MP_TAC(MESON[
REAL_LT_LMUL;REAL_ARITH `&0* r= &0`;REAL_ARITH `pi* r= r*
pi`;REAL_ARITH `&0< e ==> &0< &4* e`] `&0< r /\ &0<
pi ==> &0< &4*pi*r`) THEN ASM_REWRITE_TAC[]
THEN REWRITE_TAC[REAL_ARITH `(a:real) *b*C*d= (a*b*C)*d`]
THEN MP_TAC(SPEC `k:real`
REAL_ABS_LE) THEN MESON_TAC[REAL_ARITH `&0 < &4 *
pi * r ==> &0<= &4 *
pi * r`;
REAL_LE_LMUL]);;
let bdt2_finiteness=prove( `!(r:real)(k:real)(i:num).(&0< k /\ k<= r ==> &1 <= r pow i / k pow i)`,REPEAT STRIP_TAC
THEN MP_TAC(SPECL [`k:real`;`i:num`]
REAL_POW_LT) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
THEN ASM_SIMP_TAC[GSYM (ISPECL [`&1:real`;`(r pow i/ k pow i):real`;`(k pow i):real`]
REAL_LE_RMUL_EQ)] THEN MP_TAC(REAL_ARITH ` &0 < k pow i ==> ~ (&0= k pow i)`) THEN ASM_REWRITE_TAC[]
THEN SIMP_TAC[
REAL_DIV_RMUL] THEN ASM_SIMP_TAC[REAL_ARITH ` &1 * a= a`;REAL_ARITH `a< b ==> a<= b`] THEN ASM_MESON_TAC[
REAL_POW_LE2;REAL_ARITH `&0< k ==> &0 <= k`]);;
let bdt3_finiteness=prove( `!(r:real)(k1:real)(k2:real) (k:real). ( &0 < r/\ &0 < k1 /\ &0< k2) ==>( &0<= &4 * pi *r* (abs k) /\ &0 <= &4/ &3 *pi*( (k1 + sqrt (&3)) pow 3 + (k2 + sqrt (&3)) pow 3))`,
REPEAT STRIP_TAC THENL [ASM_MESON_TAC[REAL_ARITH `&0< A==> &0<= A`;
PI_POS_LE;
REAL_ABS_POS;
REAL_LE_MUL;REAL_ARITH `&0<= &4`];MP_TAC(MESON[REAL_ARITH `&0< k1 ==>
sqrt(&3)<= k1 +
sqrt(&3)`;
SQRT_POS_LE;REAL_ARITH `&0<= &3`;REAL_ARITH `a<= b /\ b<=c ==> a<= c`] `&0< k1 ==> &0<= k1 +
sqrt (&3)`) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN MP_TAC(MESON[REAL_ARITH `&0< k2 ==>
sqrt(&3)<= k2 +
sqrt(&3)`;
SQRT_POS_LE;REAL_ARITH `&0<= &3`;REAL_ARITH `a<= b /\ b<=c ==> a<= c`] `&0< k2 ==> &0<= k2 +
sqrt (&3)`) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN MP_TAC(SPECL [`k1 +
sqrt (&3):real`;` 3:num`]
REAL_POW_LE) THEN ASM_REWRITE_TAC[]
THEN MP_TAC(SPECL [`k2 +
sqrt (&3):real`;` 3:num`]
REAL_POW_LE) THEN ASM_REWRITE_TAC[]
THEN REPEAT DISCH_TAC THEN MP_TAC(REAL_ARITH `&0 <= (k2 +
sqrt (&3)) pow 3 /\ &0 <= (k1 +
sqrt (&3)) pow 3 ==> &0<= (k1 +
sqrt (&3)) pow 3+ (k2 +
sqrt (&3)) pow 3`) THEN ASM_REWRITE_TAC[] THEN MESON_TAC[
REAL_LE_MUL;REAL_ARITH `&0<= &4/ &3`;
PI_POS_LE]]);;
let bdt4_finiteness = prove(`!(k1:real)(k2:real) (r:real). (&0< k1 /\ &0< k2 /\ k2 + sqrt (&3) <= r) ==> (&4 / &3 * pi * ((r + k1) + sqrt (&3)) pow 3)- (&4 / &3 * pi * (r - k2 - sqrt (&3)) pow 3)<= (&4/ &3* pi*( &3*(k1+ k2+ &2*sqrt(&3)) +((k1 + sqrt (&3)) pow 3 + (k2 + sqrt (&3)) pow 3) /((k2 + sqrt (&3)) pow 2) + &3 * abs(((k1 + sqrt (&3)) pow 2 - (k2 + sqrt (&3)) pow 2)) / (k2 + sqrt (&3)))) *r pow 2`, REPEAT STRIP_TAC THEN REWRITE_TAC[REAL_FIELD `&4 / &3 *
pi * ((r + k1) +
sqrt (&3)) pow 3 -
&4 / &3 *
pi * (r - k2 -
sqrt (&3)) pow 3= ( &4*pi*r pow 2 * (k1+k2+ &2*sqrt(&3)) + &4*pi*r* ((k1+
sqrt(&3))pow 2 - (k2+
sqrt(&3)) pow 2)+ &4/ &3*pi*((k1+
sqrt(&3))pow 3 + (k2+
sqrt(&3)) pow 3))`]
THEN REWRITE_TAC[REAL_FIELD ` (&4/ &3 * pi*( &3* (k1+k2+ &2*sqrt(&3)) +
((k1 +
sqrt (&3)) pow 3 + (k2 +
sqrt (&3)) pow 3) / ((k2 +
sqrt (&3)) pow 2) +
&3 *
abs (((k1 +
sqrt (&3)) pow 2 - (k2 +
sqrt (&3)) pow 2)) / (k2 +
sqrt (&3)))) *
r pow 2= (&4 *
pi * r pow 2 * (k1 + k2 + &2 *
sqrt (&3))+ &4*pi*r pow 2* abs (((k1 +
sqrt (&3)) pow 2 - (k2 +
sqrt (&3)) pow 2)) / (k2 +
sqrt (&3))+ &4/ &3*pi* r pow 2* ((k1 +
sqrt (&3)) pow 3 + (k2 +
sqrt (&3)) pow 3) / ((k2 +
sqrt (&3)) pow 2))`]
THEN REWRITE_TAC[REAL_ARITH `(a:real) + b+ c <= a + d + e <=> b+c <= d+ e`]
THEN MATCH_MP_TAC(REAL_ARITH `&4 *
pi * r * ((k1 +
sqrt (&3)) pow 2 - (k2 +
sqrt (&3)) pow 2)<= &4 *
pi *
r pow 2 *
abs ((k1 +
sqrt (&3)) pow 2 - (k2 +
sqrt (&3)) pow 2) / (k2 +
sqrt (&3)) /\ &4 / &3 *
pi * ((k1 +
sqrt (&3)) pow 3 + (k2 +
sqrt (&3)) pow 3)<= &4 / &3 *
pi *
r pow 2 *
((k1 +
sqrt (&3)) pow 3 + (k2 +
sqrt (&3)) pow 3) / ((k2 +
sqrt (&3)) pow 2) ==> &4 *
pi * r * ((k1 +
sqrt (&3)) pow 2 - (k2 +
sqrt (&3)) pow 2) +
&4 / &3 *
pi * ((k1 +
sqrt (&3)) pow 3 + (k2 +
sqrt (&3)) pow 3) <=
&4 *
pi *
r pow 2 *
abs ((k1 +
sqrt (&3)) pow 2 - (k2 +
sqrt (&3)) pow 2) / (k2 +
sqrt (&3)) +
&4 / &3 *
pi *
r pow 2 *
((k1 +
sqrt (&3)) pow 3 + (k2 +
sqrt (&3)) pow 3) / ((k2 +
sqrt (&3)) pow 2)`)
THEN MATCH_MP_TAC(REAL_ARITH `&4 *
pi * r * ((k1 +
sqrt (&3)) pow 2 - (k2 +
sqrt (&3)) pow 2) <= &4*pi* r * abs ((k1 +
sqrt (&3)) pow 2 - (k2 +
sqrt (&3)) pow 2) /\ &4*pi* r * abs ((k1 +
sqrt (&3)) pow 2 - (k2 +
sqrt (&3)) pow 2)<= &4 *
pi *
r pow 2 *
abs ((k1 +
sqrt (&3)) pow 2 - (k2 +
sqrt (&3)) pow 2) / (k2 +
sqrt (&3)) /\ &4 / &3 *
pi * ((k1 +
sqrt (&3)) pow 3 + (k2 +
sqrt (&3)) pow 3) <=
&4 / &3 *
pi *
r pow 2 *
((k1 +
sqrt (&3)) pow 3 + (k2 +
sqrt (&3)) pow 3) / ((k2 +
sqrt (&3)) pow 2) ==> &4 *
pi * r * ((k1 +
sqrt (&3)) pow 2 - (k2 +
sqrt (&3)) pow 2) <=
&4 *
pi *
r pow 2 *
abs ((k1 +
sqrt (&3)) pow 2 - (k2 +
sqrt (&3)) pow 2) / (k2 +
sqrt (&3)) /\
&4 / &3 *
pi * ((k1 +
sqrt (&3)) pow 3 + (k2 +
sqrt (&3)) pow 3) <=
&4 / &3 *
pi *
r pow 2 *
((k1 +
sqrt (&3)) pow 3 + (k2 +
sqrt (&3)) pow 3) / ((k2 +
sqrt (&3)) pow 2) `)
THEN MP_TAC(MESON[REAL_ARITH `&0 < k2 /\ k2 +
sqrt (&3) <= r ==>
sqrt(&3)< r`;MESON[
SQRT_POS_LT;REAL_ARITH `&0< &3`] `&0<
sqrt( &3)`;REAL_ARITH `a:real <b/\ b< c ==> a< c`] `&0 < k2 /\ k2 +
sqrt (&3) <= r ==> &0< r`)
THEN ASM_SIMP_TAC[
bdt1_finiteness] THEN DISCH_TAC THEN REWRITE_TAC[
bdt1_finiteness] THEN MP_TAC(REAL_ARITH `&0< k2 ==> &0 <=k2`) THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[REAL_FIELD `&4 *
pi *
r pow 2 *
abs
((k1 +
sqrt (&3)) pow 2 - (k2 +
sqrt (&3)) pow 2) / (k2 +
sqrt (&3))= ( &4*pi* r* abs
((k1 +
sqrt (&3)) pow 2 - (k2 +
sqrt (&3)) pow 2))*(r/ (k2+
sqrt(&3)))`] THEN REWRITE_TAC[REAL_FIELD `&4 / &3 *
pi *
r pow 2 *
((k1 +
sqrt (&3)) pow 3 + (k2 +
sqrt (&3)) pow 3) /
((k2 +
sqrt (&3)) pow 2) = (&4 / &3 *
pi *((k1 +
sqrt (&3)) pow 3 + (k2 +
sqrt (&3)) pow 3))*(r pow 2/ ((k2 +
sqrt (&3)) pow 2))`]
THEN DISCH_TAC THEN MP_TAC(SPECL [`r:real`;`k2+
sqrt(&3):real`;`1:num`]
bdt2_finiteness)
THEN MP_TAC(MESON[MESON[
SQRT_POS_LT;REAL_ARITH `&0< &3`] `&0<
sqrt( &3)`;REAL_ARITH `&0 < k2
==>
sqrt(&3)< k2 +
sqrt(&3)`;REAL_ARITH `a:real <b/\ b< c ==> a< c`] `&0 < k2
==> &0< k2 +
sqrt(&3)`) THEN ASM_REWRITE_TAC[] THEN SIMP_TAC[REAL_ARITH `(x:real) pow 1= x`]
THEN DISCH_TAC THEN MP_TAC(SPECL [`r:real`;`k2+
sqrt(&3):real`;`2:num`]
bdt2_finiteness) THEN ASM_REWRITE_TAC[]
THEN REPEAT DISCH_TAC THEN MP_TAC(SPECL [`r:real`;`k1:real`;`k2:real`;`((k1 +
sqrt (&3)) pow 2 - (k2 +
sqrt (&3)) pow 2):real`]
bdt3_finiteness) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN ASM_MESON_TAC[
REAL_LE_LMUL;REAL_ARITH ` a* &1= a`]);;
let bdt6_finiteness=prove(`!(x:real^3)(k1:real)(k2:real) (r:real). (&0< k1 /\ &0<r) ==> &(CARD ((int_ball x (r+ k1)) DIFF (int_ball x (r- k2)))) <= &4/ &3*pi*(r+k1+ sqrt(&3))pow 3`,REPEAT STRIP_TAC THEN MP_TAC(GSYM (SPECL [`
CARD (
int_ball x (r + k1)
DIFF int_ball x (r - k2)):num`;`
CARD (
int_ball x (r+ k1)):num`] REAL_OF_NUM_LE)) THEN SIMP_TAC[
card_diff_ineq]
THEN MP_TAC(SPECL [`x:real^3`;`k1:real`;`r:real`]
card_int_ball_le2) THEN ASM_SIMP_TAC[REAL_ARITH `&0< k1 /\ &0< r ==> &0<= k1 /\ &0<= r`] THEN ASM_SIMP_TAC[REAL_ARITH `&0< a ==> &0<= a`] THEN MESON_TAC[REAL_ARITH `a<= b /\ c<=a ==> c<= b`; REAL_ARITH `r + k1 +
sqrt (&3)= (r + k1) +
sqrt (&3)`]);;
(* Quantifiers corrected by thales below.
let bdt5_finiteness=prove(`!(x:real^3)(k1:real)(k2:real) (r:real). (&0< k1 /\ &0< k2 /\ k2 + sqrt (&3) <= r) ==> ?(C:real). &(CARD ((int_ball x (r+ k1)) DIFF (int_ball x (r- k2))))<= C* r pow 2`,REPEAT STRIP_TAC THEN EXISTS_TAC `(&4 / &3 *
pi *
(&3 * (k1 + k2 + &2 * sqrt (&3)) +
((k1 + sqrt (&3)) pow 3 + (k2 + sqrt (&3)) pow 3) / (k2 + sqrt (&3)) pow 2 +
&3 *
abs ((k1 + sqrt (&3)) pow 2 - (k2 + sqrt (&3)) pow 2) / (k2 + sqrt (&3)))):real`
THEN MP_TAC(ISPECL [`int_ball x (r + k1):real^3 -> bool`;`int_ball x (r - k2):real^3 -> bool`] CARD_DIFF)
THEN REWRITE_TAC[finite_int_ball] THEN MP_TAC(REAL_ARITH `&0<k1 /\ &0< k2 ==> r:real -k2 < r + k1`)
THEN ASM_REWRITE_TAC[] THEN SIMP_TAC[int_ball_subset]
THEN DISCH_TAC THEN MP_TAC(SPECL [`x:real^3`;`r-k2:real`;`r+k1:real`] card_int_ball_ineq)
THEN ASM_SIMP_TAC[GSYM REAL_OF_NUM_SUB] THEN REPEAT DISCH_TAC
THEN MP_TAC(SPECL [`x:real^3`;`k1:real`;`k2:real`;`r:real`] card_int_ball_le) THEN ASM_REWRITE_TAC[]
THEN MP_TAC(SPECL [`x:real^3`;`k1:real`;`k2:real`;`r:real`] card_int_ball_pos) THEN ASM_REWRITE_TAC[]
THEN MP_TAC(SPECL [`k1:real`;`k2:real`;`r:real`] bdt4_finiteness) THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);;
*)
let bdt5_finiteness=prove(`!(x:real^3)(k1:real)(k2:real) .
(&0< k1 /\ &0< k2) ==> ( ?(C:real). !r. ( k2 + sqrt (&3) <= r) ==> (&(CARD ((int_ball x (r+ k1)) DIFF (int_ball x (r- k2))))<= C* r pow 2))`,
REPEAT STRIP_TAC THEN
EXISTS_TAC `(&4 / &3 *
pi * (&3 * (k1 + k2 + &2 *
sqrt (&3)) + ((k1 +
sqrt (&3)) pow 3 + (k2 +
sqrt (&3)) pow 3) / (k2 +
sqrt (&3)) pow 2 + &3 * abs ((k1 +
sqrt (&3)) pow 2 - (k2 +
sqrt (&3)) pow 2) / (k2 +
sqrt (&3)))):real` THEN
STRIP_TAC THEN
MP_TAC(ISPECL [`
int_ball x (r + k1):real^3 -> bool`;`
int_ball x (r - k2):real^3 -> bool`]
CARD_DIFF) THEN
REWRITE_TAC[
finite_int_ball] THEN MP_TAC(REAL_ARITH `&0<k1 /\ &0< k2 ==> r:real -k2 < r + k1`) THEN
ASM_REWRITE_TAC[] THEN SIMP_TAC[
int_ball_subset] THEN
DISCH_TAC THEN MP_TAC(SPECL [`x:real^3`;`r-k2:real`;`r+k1:real`]
card_int_ball_ineq) THEN
ASM_SIMP_TAC[GSYM
REAL_OF_NUM_SUB] THEN REPEAT DISCH_TAC THEN
MP_TAC(SPECL [`x:real^3`;`k1:real`;`k2:real`;`r:real`]
card_int_ball_le) THEN
ASM_REWRITE_TAC[] THEN
MP_TAC(SPECL [`x:real^3`;`k1:real`;`k2:real`;`r:real`]
card_int_ball_pos) THEN
ASM_REWRITE_TAC[] THEN
MP_TAC(SPECL [`k1:real`;`k2:real`;`r:real`]
bdt4_finiteness) THEN
ASM_REWRITE_TAC[] THEN
REAL_ARITH_TAC);;
(* fixed quantifier order -thales
let bdt7_finiteness=prove(`!(x:real^3)(k1:real)(k2:real) (r:real). (&0< k1 /\ &0< k2 /\ r< k2 + sqrt (&3) /\ k2 <= r) ==> ?(C:real). &(CARD ((int_ball x (r+ k1)) DIFF (int_ball x (r- k2))))<= C* r pow 2`,
REPEAT STRIP_TAC THEN EXISTS_TAC `(&4/ &3*pi*(k2+k1+ &2*sqrt(&3)) pow 3/ (k2 pow 2)):real`
THEN MATCH_MP_TAC(REAL_ARITH `&(CARD (int_ball x (r + k1) DIFF int_ball x (r - k2)))
<= &4/ &3*pi*(r+k1+ sqrt(&3))pow 3 /\ &4/ &3*pi*(r+k1+ sqrt(&3))pow 3 <= (&4 / &3 * pi * (k2 + k1 + &2 * sqrt (&3)) pow 3 / k2 pow 2) * r pow 2 ==> &(CARD (int_ball x (r + k1) DIFF int_ball x (r - k2))) <= ( &4 / &3 * pi * (k2 + k1 + &2 * sqrt (&3)) pow 3 / k2 pow 2) * r pow 2`) THEN MP_TAC(REAL_ARITH `&0< k2 /\ k2<= r ==> &0< r`) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
THEN ASM_SIMP_TAC[SPECL [`x:real^3`;`k1:real`;`k2:real`; `r:real`] bdt6_finiteness]
THEN MATCH_MP_TAC(REAL_ARITH `&4 / &3 * pi * (r + k1 + sqrt (&3)) pow 3
<= &4 / &3 * pi * (k2 + k1 + &2*sqrt (&3)) pow 3 /\ &4 / &3 * pi * (k2 + k1 + &2*sqrt (&3)) pow 3
<= (&4 / &3 * pi * (k2 + k1 + &2 * sqrt (&3)) pow 3 / k2 pow 2) * r pow 2 ==> &4 / &3 * pi * (r + k1 + sqrt (&3)) pow 3 <=
(&4 / &3 * pi * (k2 + k1 + &2 * sqrt (&3)) pow 3 / k2 pow 2) * r pow 2`)
THEN MP_TAC(MESON[REAL_ARITH `&0<k1 /\ &0< r ==> sqrt(&3)<= r+k1+ sqrt(&3)`;SPEC `&3:real` SQRT_POS_LE;
REAL_ARITH `&0<= &3`;REAL_ARITH `a<=b /\ b<= c ==> a<= c`] `&0<k1 /\ &0< r ==> &0<= r+k1+ sqrt(&3)`)
THEN ASM_REWRITE_TAC[] THEN MP_TAC(REAL_ARITH `r < k2 + sqrt (&3) ==> r+ k1+ sqrt(&3) <= k2+ k1+ &2* sqrt(&3)`) THEN ASM_REWRITE_TAC[] THEN MP_TAC(MESON[PI_POS_LE;REAL_ARITH `&0<= &4/ &3`;REAL_LE_MUL] `&0<= &4/ &3*pi`)
THEN REPEAT DISCH_TAC THEN MP_TAC(ISPECL [`3:num`;`r + k1 + sqrt (&3):real`;`k2 + k1 + &2 * sqrt (&3):real`] REAL_POW_LE2) THEN ASM_REWRITE_TAC[] THEN ASM_SIMP_TAC[REAL_ARITH `(a:real)*b*c = (a*b)*c`;REAL_LE_LMUL]
THEN DISCH_TAC THEN REWRITE_TAC[REAL_FIELD `((&4 / &3 * pi) * (k2 + k1 + &2 * sqrt (&3)) pow 3 / k2 pow 2) * r pow 2= ((&4 / &3 * pi)*((k2 + k1 + &2 * sqrt (&3)) pow 3))*(r pow 2/ k2 pow 2)`]
THEN MP_TAC(MESON[MESON[REAL_POW_LE] `&0 <= r + k1 + sqrt (&3) ==> &0 <= (r + k1 + sqrt (&3)) pow 3`;REAL_ARITH `a<= b /\ b<= c ==> a<= c`] `&0 <= r + k1 + sqrt (&3) /\ (r + k1 + sqrt (&3)) pow 3 <= (k2 + k1 + &2 * sqrt (&3)) pow 3 ==> &0<= (k2 + k1 + &2 * sqrt (&3)) pow 3`) THEN ASM_REWRITE_TAC[] THEN MP_TAC(SPECL [`r:real`;`k2:real`;`2:num`] bdt2_finiteness) THEN ASM_REWRITE_TAC[]
THEN REPEAT DISCH_TAC THEN MP_TAC(MESON[REAL_LE_MUL] `&0 <= &4 / &3 * pi /\ &0 <= (k2 + k1 + &2 * sqrt (&3)) pow 3 ==> &0<= (&4 / &3 * pi) * (k2 + k1 + &2 * sqrt (&3)) pow 3`) THEN ASM_REWRITE_TAC[]
THEN ASM_MESON_TAC[REAL_LE_LMUL;REAL_ARITH ` a* &1= a`]);;
*)
let bdt7_finiteness=prove(`!(x:real^3)(k1:real)(k2:real) (r:real).
(&0< k1 /\ &0< k2) ==>
?(C:real). !r. ( r< k2 + sqrt (&3) /\ k2 <= r) ==> &(CARD ((int_ball x (r+ k1)) DIFF (int_ball x (r- k2))))<= C* r pow 2`,
REPEAT STRIP_TAC THEN
EXISTS_TAC `(&4/ &3*pi*(k2+k1+ &2*sqrt(&3)) pow 3/ (k2 pow 2)):real` THEN
REPEAT STRIP_TAC THEN
MATCH_MP_TAC(REAL_ARITH `&(
CARD (
int_ball x (r + k1)
DIFF int_ball x (r - k2))) <= &4/ &3*pi*(r+k1+
sqrt(&3))pow 3 /\ &4/ &3*pi*(r+k1+
sqrt(&3))pow 3 <= (&4 / &3 *
pi * (k2 + k1 + &2 *
sqrt (&3)) pow 3 / k2 pow 2) * r pow 2 ==> &(
CARD (
int_ball x (r + k1)
DIFF int_ball x (r - k2))) <= ( &4 / &3 *
pi * (k2 + k1 + &2 *
sqrt (&3)) pow 3 / k2 pow 2) * r pow 2`) THEN
MP_TAC(REAL_ARITH `&0< k2 /\ k2<= r ==> &0< r`) THEN
ASM_REWRITE_TAC[] THEN
DISCH_TAC THEN
ASM_SIMP_TAC[SPECL [`x:real^3`;`k1:real`;`k2:real`; `r:real`]
bdt6_finiteness] THEN
MATCH_MP_TAC(REAL_ARITH `&4 / &3 *
pi * (r + k1 +
sqrt (&3)) pow 3 <= &4 / &3 *
pi * (k2 + k1 + &2*sqrt (&3)) pow 3 /\ &4 / &3 *
pi * (k2 + k1 + &2*sqrt (&3)) pow 3 <= (&4 / &3 *
pi * (k2 + k1 + &2 *
sqrt (&3)) pow 3 / k2 pow 2) * r pow 2 ==> &4 / &3 *
pi * (r + k1 +
sqrt (&3)) pow 3 <= (&4 / &3 *
pi * (k2 + k1 + &2 *
sqrt (&3)) pow 3 / k2 pow 2) * r pow 2`) THEN
MP_TAC(MESON[REAL_ARITH `&0<k1 /\ &0< r ==>
sqrt(&3)<= r+k1+
sqrt(&3)`;SPEC `&3:real`
SQRT_POS_LE; REAL_ARITH `&0<= &3`;REAL_ARITH `a<=b /\ b<= c ==> a<= c`] `&0<k1 /\ &0< r ==> &0<= r+k1+
sqrt(&3)`) THEN
ASM_REWRITE_TAC[] THEN
MP_TAC(REAL_ARITH `r < k2 +
sqrt (&3) ==> r+ k1+
sqrt(&3) <= k2+ k1+ &2*
sqrt(&3)`) THEN
ASM_REWRITE_TAC[] THEN
MP_TAC(MESON[
PI_POS_LE;REAL_ARITH `&0<= &4/ &3`;
REAL_LE_MUL] `&0<= &4/ &3*pi`) THEN
REPEAT DISCH_TAC THEN
MP_TAC(ISPECL [`3:num`;`r + k1 +
sqrt (&3):real`;`k2 + k1 + &2 *
sqrt (&3):real`]
REAL_POW_LE2) THEN
ASM_REWRITE_TAC[] THEN
ASM_SIMP_TAC[REAL_ARITH `(a:real)*b*c = (a*b)*c`;
REAL_LE_LMUL] THEN
DISCH_TAC THEN
REWRITE_TAC[REAL_FIELD `((&4 / &3 *
pi) * (k2 + k1 + &2 *
sqrt (&3)) pow 3 / k2 pow 2) * r pow 2= ((&4 / &3 *
pi)*((k2 + k1 + &2 *
sqrt (&3)) pow 3))*(r pow 2/ k2 pow 2)`] THEN
MP_TAC(MESON[MESON[
REAL_POW_LE] `&0 <= r + k1 +
sqrt (&3) ==> &0 <= (r + k1 +
sqrt (&3)) pow 3`;REAL_ARITH `a<= b /\ b<= c ==> a<= c`] `&0 <= r + k1 +
sqrt (&3) /\ (r + k1 +
sqrt (&3)) pow 3 <= (k2 + k1 + &2 *
sqrt (&3)) pow 3 ==> &0<= (k2 + k1 + &2 *
sqrt (&3)) pow 3`) THEN
ASM_REWRITE_TAC[] THEN
MP_TAC(SPECL [`r:real`;`k2:real`;`2:num`]
bdt2_finiteness) THEN
ASM_REWRITE_TAC[] THEN
REPEAT DISCH_TAC THEN
MP_TAC(MESON[
REAL_LE_MUL] `&0 <= &4 / &3 *
pi /\ &0 <= (k2 + k1 + &2 *
sqrt (&3)) pow 3 ==> &0<= (&4 / &3 *
pi) * (k2 + k1 + &2 *
sqrt (&3)) pow 3`) THEN
ASM_REWRITE_TAC[] THEN
ASM_MESON_TAC[
REAL_LE_LMUL;REAL_ARITH ` a* &1= a`]);;
let REAL_LE_SQUARE_POW =
MESON[REAL_POW_2; REAL_LE_SQUARE]`! x. &0 <= x pow 2 `;;
(*--------------------------------------------------------------------*)
(*Lemma 2.16 [TXIWYHI] Bound of number of int points between two balls*)
(*--------------------------------------------------------------------*)
let TXIWYHI=prove( `!(x:real^3)(k1:real)(k2:real) (r:real).
(&0< k1 /\ &0< k2) ==> ?(C:real). !r. (k2 <= r) ==>
&(CARD (integer_point (ball(x,r+ k1) DIFF ball(x,r- k2))))<= C* r pow 2`,
REPEAT GEN_TAC THEN SIMP_TAC[
eq_def_intball] THEN
REPEAT STRIP_TAC THEN
SUBGOAL_THEN `?C. !r. k2+sqrt(&3) <= r ==> &(
CARD (
int_ball x (r + k1)
DIFF int_ball x (r - k2))) <= C * r pow 2` ASSUME_TAC THENL
[ASM_MESON_TAC[
bdt5_finiteness];ALL_TAC] THEN
SUBGOAL_THEN `(?C. !r. r < k2 +
sqrt (&3) /\ k2 <= r ==> &(
CARD (
int_ball x (r + k1)
DIFF int_ball x (r - k2))) <= C * r pow 2)` ASSUME_TAC THENL
[ASM_MESON_TAC[
bdt7_finiteness];ALL_TAC] THEN
FIRST_X_ASSUM CHOOSE_TAC THEN
FIRST_X_ASSUM CHOOSE_TAC THEN
EXISTS_TAC `(abs(C:real)+abs(C':real))` THEN
GEN_TAC THEN
STRIP_TAC THEN
MATCH_MP_TAC (REAL_ARITH `(?b. (a<=b /\ b<=c) ) ==> (a <= c)`) THEN
SUBGOAL_THEN `(C*r pow 2 <= (abs(C)+abs(C'))* r pow 2) /\ (C'*r pow 2 <= (abs(C)+abs(C')) * r pow 2)` MP_TAC THENL
[CONJ_TAC THEN MATCH_MP_TAC
REAL_LE_RMUL THEN REWRITE_TAC[
REAL_LE_SQUARE_POW] THEN REAL_ARITH_TAC;ALL_TAC] THEN
REPEAT STRIP_TAC THEN
DISJ_CASES_TAC(REAL_ARITH `(r:real)< k2+
sqrt(&3) \/ (k2+
sqrt(&3)<= r)`) THEN
ASM_MESON_TAC[]
);;
(* old version with reversed quantifiers -thales
let TXIWYHI=prove( `!(x:real^3)(k1:real)(k2:real) (r:real).
(&0< k1 /\ &0< k2 /\ k2 <= r) ==> ?(C:real).
&(CARD (integer_point (ball(x,r+ k1) DIFF ball(x,r- k2))))<= C* r pow 2`,
REPEAT GEN_TAC THEN SIMP_TAC[eq_def_intball]
THEN STRIP_TAC THEN DISJ_CASES_TAC(REAL_ARITH `(r:real)< k2+ sqrt(&3) \/ (k2+ sqrt(&3)<= r)`)
THENL [ASM_MESON_TAC[bdt7_finiteness];ASM_MESON_TAC[bdt5_finiteness]]);;
*)
(*--------------------------------------------------------------------*)
end;;