development/thales/examples/lemma_negligible.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Definitions: (General definitions file)         *)
   5 (* Chapter: Packings                                                     *)
   6 (* Author: Thomas C. Hales                                                    *)
   7 (* Date: 2010-07-01                                                           *)
   8 (* ========================================================================== *)
   9
  10 module Lemma_negligible = struct
  11
  12   open Real_ext;;
  13
  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)))`,
  17 [
  18 GEN_TAC;
  19 EQ_TAC;
  20 REPEAT STRIP_TAC;
  21 EXISTS_TAC `C:real`;
  22 ASM_REWRITE_TAC[];
  23 REPEAT STRIP_TAC;
  24 EXISTS_TAC `abs(C)`;
  25 REWRITE_TAC[REAL_ARITH `&0 <= abs C`];
  26 REPEAT STRIP_TAC;
  27 ASSUME_TAC (REAL_ARITH `C <= abs C`);
  28 MATCH_MP_TAC REAL_LE_TRANS;
  29 EXISTS_TAC `C * r pow 2`;
  30 CONJ_TAC;
  31 ASM_SIMP_TAC[];
  32 MATCH_MP_TAC REAL_LE_RMUL_IMP;
  33 ASM_REWRITE_TAC[Collect_geom.REAL_LE_POW_2];
  34 ]);;
  35
  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]);;
  40
  41
  42 end;;