(* ========================================================================== *)
(* 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;;