(* ========================================================================= *)
(* FLYSPECK - BOOK FORMALIZATION *)
(* *)
(* Authour : VU KHAC KY *)
(* Book lemma: UPFZBZM *)
(* Chaper : Packing (Clusters) *)
(* *)
(* ========================================================================= *)
(* ========================================================================= *)
(* FILES NEED TO BE LOADED *)
(* sum_beta_bump.hl *)
(* sum_gammaX_lmfun_estimate.hl *)
(* ========================================================================= *)
let UPFZBZM_concl =
`!V. saturated V /\ packing V /\ cell_cluster_estimate V /\
TSKAJXY_statement /\
lmfun_inequality V ==>
(?G. negligible_fun_0 G V /\ fcc_compatible G V)`;;
let FCC_COMPATABILITY_FUNC_concl =
`!V. saturated V /\ packing V /\ cell_cluster_estimate V /\
TSKAJXY_statement /\
lmfun_inequality V /\ G = (\u. --vol(voronoi_open V u) +
&8 * mm1 - &8 * mm2 * sum { v | v IN V /\ ~(u=v) /\ dist(u,v) <= &2*h0 }
(\v. lmfun (hl [u;v])))
==> fcc_compatible G V`;;
let NEGLIGIBLE_FUNC_concl =
`!V. saturated V /\
packing V /\
cell_cluster_estimate V /\
TSKAJXY_statement /\
lmfun_inequality V /\
G =
(\u. --vol (voronoi_open V u) +
&8 * mm1 -
&8 *
mm2 *
sum {v | v IN V /\ ~(u = v) /\ dist (u,v) <= &2 * h0}
(\v. lmfun (hl [u; v])))
==> negligible_fun_0 G V`;;
(* ========================================================================= *)
(* THE THEOREM *)
(* ========================================================================= *)
(* PART 1 OF THE LEMMA *)
let FCC_COMPATABILITY_FUNC = prove_by_refinement (
FCC_COMPATABILITY_FUNC_concl,
[(REWRITE_TAC[lmfun_inequality;fcc_compatible]);
(REPEAT STRIP_TAC);
(ASM_REWRITE_TAC[Pack2.MEASURE_VORONOI_CLOSED_OPEN]);
(ASM_REWRITE_TAC[REAL_ARITH `a + --a + b - c = b - c`]);
(MATCH_MP_TAC (REAL_ARITH
`x = &8 * mm1 - &8 * (&12 * mm2) /\ y <= &8 * (&12 * mm2) ==>
x <= &8 * mm1 - y`));
(STRIP_TAC);
(REWRITE_TAC[SQRT_OF_32_lemma]);
(REWRITE_TAC[REAL_ARITH `a * b - a * c = a * (b - c)`]);
(REWRITE_TAC[m1_minus_12m2]);
(MATCH_MP_TAC REAL_LE_LMUL);
(REWRITE_TAC[REAL_ARITH `&0 <= &8`]);
(REWRITE_TAC[REAL_ARITH `&12 * mm2 = mm2 * &12`]);
(MATCH_MP_TAC REAL_LE_LMUL);
(REWRITE_TAC[ZERO_LE_MM2_LEMMA]);
(ASM_MESON_TAC[])]);;
let NEGLIGIBLE_FUNC = prove_by_refinement (
NEGLIGIBLE_FUNC_concl,
[(REWRITE_TAC[negligible_fun_0; negligible_fun_any_C]);
(REPEAT STRIP_TAC);
(MP_TAC (SPEC `V:real^3->bool` KIZHLTL1));
(STRIP_TAC);
(MP_TAC (SPEC `V:real^3->bool` KIZHLTL2));
(STRIP_TAC);
(MP_TAC (SPEC `V:real^3->bool` KIZHLTL4));
(STRIP_TAC);
(MP_TAC (SPEC `V:real^3->bool` SUM_GAMMAX_LMFUN_ESTIMATE));
(STRIP_TAC);
(NEW_GOAL
`!r. saturated V /\ packing V /\ &1 <= r
==> c''' * r pow 2 <=
sum {X | X SUBSET ball (vec 0,r) /\ mcell_set V X}
(\X. gammaX V X lmfun)`);
(REPEAT STRIP_TAC);
(FIRST_ASSUM MATCH_MP_TAC);
(ASM_REWRITE_TAC[]);
(UP_ASM_TAC THEN REWRITE_TAC[gammaX] THEN STRIP_TAC);
(EXISTS_TAC `--c''' - c - c' - c''`);
(REPEAT STRIP_TAC);
(ABBREV_TAC `f1 = (\u:real^3. --vol (voronoi_open V u))`);
(ABBREV_TAC `f2 = (\u:real^3. &8 * mm1 - &8 * mm2 *
sum {v | v IN V /\ ~(u = v) /\ dist (u,v) <= &2 * h0}
(\v. lmfun (hl [u; v])))`);
(REWRITE_WITH `sum ((V:real^3->bool) INTER ball (vec 0,r)) G =
sum (V INTER ball (vec 0,r)) f1 +
sum (V INTER ball (vec 0,r)) f2`);
(ASM_REWRITE_TAC[] THEN EXPAND_TAC "f1" THEN EXPAND_TAC "f2");
(MATCH_MP_TAC SUM_ADD);
(ASM_SIMP_TAC[FINITE_PACK_LEMMA]);
(ABBREV_TAC `f3 = (\u:real^3. &8 * mm1)`);
(ABBREV_TAC `f4 = (\u:real^3. &8 * mm2 *
sum {v | v IN V /\ ~(u = v) /\ dist (u,v) <= &2 * h0}
(\v. lmfun (hl [u; v])))`);
(REWRITE_WITH `sum ((V:real^3->bool) INTER ball (vec 0,r)) f2 =
sum (V INTER ball (vec 0,r)) f3 -
sum (V INTER ball (vec 0,r)) f4`);
(EXPAND_TAC "f2" THEN EXPAND_TAC "f3" THEN EXPAND_TAC "f4");
(MATCH_MP_TAC SUM_SUB);
(ASM_SIMP_TAC[FINITE_PACK_LEMMA]);
(EXPAND_TAC "f4" THEN DEL_TAC THEN
ASM_SIMP_TAC[SUM_NEG;SUM_CONST;SUM_LMUL;FINITE_PACK_LEMMA]);
(ABBREV_TAC `f5 = (\u:real^3.
sum {v | v IN V /\ ~(u = v) /\ dist (u,v) <= &2 * h0}
(\v. lmfun (hl [u; v])))`);
(ABBREV_TAC `B = {X | X SUBSET ball (vec 0, r) /\ mcell_set V X}`);
(ABBREV_TAC `T1 = sum B vol`);
(ABBREV_TAC `T2 = --(&2 * mm1 / pi) * sum B (total_solid V)`);
(ABBREV_TAC `T3 = (&8 * mm2 / pi) * sum B (\X. sum (edgeX V X)
(\({u, v}). if {u, v} IN edgeX V X
then dihX V X (u,v) * lmfun (hl [u; v])
else &0))`);
(NEW_GOAL `sum (V:real^3->bool INTER ball (vec 0,r)) f1 <= --T1 - c * r pow 2`);
(EXPAND_TAC "T1" THEN EXPAND_TAC "B");
(EXPAND_TAC "f1");
(REWRITE_TAC[SUM_NEG; REAL_ARITH `-- a <= --b - c <=> b + c <= a`]);
(FIRST_ASSUM MATCH_MP_TAC);
(ASM_REWRITE_TAC[]);
(NEW_GOAL
`sum (V:real^3->bool INTER ball (vec 0,r)) f3 <= --T2 - c' * r pow 2`);
(EXPAND_TAC "T2" THEN EXPAND_TAC "B");
(EXPAND_TAC "f3");
(REWRITE_TAC[SUM_NEG; REAL_ARITH `a <= --(-- b * d) - c<=> a + c <= b * d`]);
(REWRITE_WITH `sum (V INTER ball (vec 0,r)) (\u:real^3. &8 * mm1) =
&(CARD (V INTER ball (vec 0,r))) * (&8 * mm1)`);
(MATCH_MP_TAC SUM_CONST);
(ASM_SIMP_TAC[FINITE_PACK_LEMMA]);
(FIRST_ASSUM MATCH_MP_TAC);
(ASM_REWRITE_TAC[]);
(NEW_GOAL `T3 + c'' * r pow 2 <=
&8 * mm2 * sum (V:real^3->bool INTER ball (vec 0,r)) f5`);
(EXPAND_TAC "T3" THEN EXPAND_TAC "B");
(FIRST_ASSUM MATCH_MP_TAC);
(ASM_REWRITE_TAC[]);
(MATCH_MP_TAC (REAL_ARITH `(?s. A <= s /\ s <= b) ==> A <= b`));
(EXISTS_TAC `--T1 + --T2 + --T3 - (c + c' + c'') * r pow 2`);
(STRIP_TAC);
(ASM_REAL_ARITH_TAC);
(REWRITE_TAC[REAL_ARITH
`--T1 + --T2 + --T3 - (c + c' + c'') * r pow 2 <=
(--c''' - c - c' - c'') * r pow 2
<=> c''' * r pow 2 <= T1 + T2 + T3`]);
(REWRITE_WITH `T1 + T2 + T3 =
sum {X | X SUBSET ball (vec 0,r) /\ mcell_set V X}
(\X. gammaX V X lmfun)`);
(ASM_REWRITE_TAC[]);
(REWRITE_TAC[gammaX]);
(NEW_GOAL `FINITE (B:(real^3->bool)->bool)`);
(EXPAND_TAC "B");
(ASM_SIMP_TAC [FINITE_MCELL_SET_LEMMA]);
(ASM_SIMP_TAC[SUM_ADD; SUM_SUB; SUM_LMUL; ETA_AX]);
(EXPAND_TAC "T2");
(REAL_ARITH_TAC);
(FIRST_ASSUM MATCH_MP_TAC);
(ASM_REWRITE_TAC[])]);;