1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
4 (* Definitions: (General definitions file) *)
5 (* Chapter: Packings *)
6 (* Author: Thomas C. Hales *)
8 (* ========================================================================== *)
10 module Lemma_negligible = struct
14 let pos_lemma = prove_by_refinement(
15 `!Q. (?C. (&0 <= C /\ (!r. &1 <= r ==> Q r <= C * r pow 2))) <=>
16 (?C. ( (!r. &1 <= r ==> Q r <= C * r pow 2)))`,
25 REWRITE_TAC[REAL_ARITH `&0 <= abs C`];
27 ASSUME_TAC (REAL_ARITH `C <= abs C`);
28 MATCH_MP_TAC REAL_LE_TRANS;
29 EXISTS_TAC `C * r pow 2`;
32 MATCH_MP_TAC REAL_LE_RMUL_IMP;
33 ASM_REWRITE_TAC[Collect_geom.REAL_LE_POW_2];
36 let negligible_fun_any_C = prove(
37 `!f S. negligible_fun_0 f S <=>
38 (?C. (!r. &1 <= r ==> sum (S INTER ball ((vec 0),r)) f <= C * r pow 2))`,
39 REWRITE_TAC[Pack_defs.negligible_fun_0;Pack_defs.negligible_fun_p;pos_lemma]);;