3 let pos_lemma = prove_by_refinement(
4 `!Q. (?C. (&0 <= C /\ (!r. &1 <= r ==> Q r <= C * r pow 2))) <=>
5 (?C. ( (!r. &1 <= r ==> Q r <= C * r pow 2)))`,
13 EXISTS_TAC `abs(C)`;search[`negligible_fun_0`];;
14 REWRITE_TAC[REAL_ARITH `&0 <= abs C`];
16 ASSUME_TAC (REAL_ARITH `C <= abs C`);
17 MATCH_MP_TAC REAL_LE_TRANS;
18 EXISTS_TAC `C * r pow 2`;
21 MATCH_MP_TAC REAL_LE_RMUL_IMP;
22 ASM_REWRITE_TAC[Collect_geom.REAL_LE_POW_2];
25 let negligible_fun_any_C = prove(
26 `!f S. negligible_fun_0 f S <=>
27 (?C. (!r. &1 <= r ==> sum (S INTER ball ((vec 0),r)) f <= C * r pow 2))`,
28 REWRITE_TAC[Pack_defs.negligible_fun_0;Pack_defs.negligible_fun_p;pos_lemma]);;