2 (* ========================================================================== *)
3 (* FLYSPECK - BOOK FORMALIZATION *)
5 (* Chapter: Local Fan *)
6 (* Author: Hoang Le Truong *)
8 (* ========================================================================= *)
13 module Lfjcixp = struct
20 open Prove_by_refinement;;
25 let LFJCIXP =prove(`(!y1 y2 y3 y4 y5 y6.
26 &2 <= y1 /\ y1<= #2.52
27 /\ &2 <= y2 /\ y2<= #2.52
28 /\ &2 <= y3 /\ y3<= #2.52
29 /\ &2 <= y4 /\ y4<= #4.52
32 ==> (y4 <= #3.915 \/ delta (y1 pow 2) (y2 pow 2) (y3 pow 2) (y4 pow 2) (y5 pow 2) (y6 pow 2)< &0))
33 /\ {v,u,w} SUBSET ball_annulus
38 /\ norm (u - w) <= #4.52
39 ==> norm(u-w)<= #3.915
42 THEN MRESAL_TAC Trigonometry.LBEVAKV[`vec 0:real^3`;`w:real^3`;`u:real^3`;`v:real^3`][dist;VECTOR_ARITH`a - vec 0= a`;NORM_NEG;NORM_SUB]
44 THEN ONCE_REWRITE_TAC[NORM_SUB]
45 THEN ASM_REWRITE_TAC[REAL_ARITH`&0<= a <=> ~(a< &0)`]
46 THEN MP_TAC(SET_RULE`{v, u, w} SUBSET ball_annulus
47 ==> v IN ball_annulus /\ u IN ball_annulus /\ w IN ball_annulus`)
48 THEN ASM_REWRITE_TAC[]
49 THEN REWRITE_TAC[IN_ELIM_THM;DIFF;ball_annulus;ball;cball;REAL_ARITH`~(a< &2)<=> &2<= a`;REAL_ARITH`&2 * #1.26= #2.52`;h0;dist;VECTOR_ARITH`a - vec 0= a`;NORM_NEG;NORM_SUB]
51 THEN DISCH_THEN(LABEL_TAC"YEU")
53 THEN FIND_ASSUM MP_TAC `packing {v,u,w:real^3}`
54 THEN REWRITE_TAC[packing]
56 THEN POP_ASSUM(fun th-> MRESAL_TAC th[`u:real^3`;`w:real^3`][SET_RULE`{v, u, w} u /\ {v, u, w} w`;dist])
57 THEN REMOVE_THEN"YEU"(fun th-> MRESA_TAC th[`norm(w:real^3)`;`norm(u:real^3)`;`norm (v:real^3)`;`norm(u-w:real^3)`;`&2`;`&2`]));;