legacy/oldvolume/ch_volume/volume_temp.hl

   1 let TXIWYHI=prove( `!(x:real^3)(k1:real)(k2:real).
   2     (&0< k1 /\ &0< k2 ) ==> ?(C:real). !r.  ( k2 <= r) ==>
   3      &(CARD (integer_point (ball(x,r+ k1) DIFF ball(x,r- k2))))<= C* r pow 2`,
   4   REPEAT GEN_TAC THEN
   5   SIMP_TAC[eq_def_intball] THEN
   6   STRIP_TAC THEN
   7   DISJ_CASES_TAC(REAL_ARITH `(r:real)< k2+ sqrt(&3) \/ (k2+ sqrt(&3)<= r)`)
   8
   9
  10   THENL [ASM_MESON_TAC[bdt7_finiteness];ASM_MESON_TAC[bdt5_finiteness]]);;
  11
  12 bdt7_finiteness;;
  13 bdt5_finiteness;;