(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Definitions: (General definitions file)         *)
(* Chapter: Packings                                                     *)
(* Author: Thomas C. Hales                                                    *)
(* Date: 2010-07-01                                                           *)
(* ========================================================================== *)

module Lemma_negligible = struct

  open Real_ext;;

let pos_lemma = 
prove_by_refinement(
   `!Q. (?C. (&0 <= C /\  (!r. &1 <= r ==> Q r <= C * r pow 2))) <=> 
    (?C. (  (!r. &1 <= r ==> Q r <= C * r pow 2)))`,

[
GEN_TAC;
EQ_TAC;
REPEAT STRIP_TAC;
EXISTS_TAC `C:real`;
ASM_REWRITE_TAC[];
REPEAT STRIP_TAC;
EXISTS_TAC `abs(C)`;
REWRITE_TAC[REAL_ARITH `&0 <= abs C`];
REPEAT STRIP_TAC;
ASSUME_TAC (REAL_ARITH `C <= abs C`);
MATCH_MP_TAC REAL_LE_TRANS;
EXISTS_TAC `C * r pow 2`;
CONJ_TAC;
ASM_SIMP_TAC[];
MATCH_MP_TAC REAL_LE_RMUL_IMP;
ASM_REWRITE_TAC[Collect_geom.REAL_LE_POW_2];
]);;
let negligible_fun_any_C = 
prove(
   `!f S. negligible_fun_0 f S <=> 
    (?C.  (!r. &1 <= r ==> sum (S INTER ball ((vec 0),r)) f <= C * r pow 2))`,

  REWRITE_TAC[Pack_defs.negligible_fun_0;Pack_defs.negligible_fun_p;pos_lemma]);;

end;;