100/circle.ml

   1 (* ========================================================================= *)
   2 (* Area of a circle.                                                         *)
   3 (* ========================================================================= *)
   4
   5 needs "Multivariate/measure.ml";;
   6 needs "Multivariate/realanalysis.ml";;
   7
   8 (* ------------------------------------------------------------------------- *)
   9 (* Circle area. Should maybe extend WLOG tactics for such scaling.           *)
  10 (* ------------------------------------------------------------------------- *)
  11
  12 let AREA_UNIT_CBALL = prove
  13  (`measure(cball(vec 0:real^2,&1)) = pi`,
  14   REPEAT STRIP_TAC THEN
  15   MATCH_MP_TAC(INST_TYPE[`:1`,`:M`; `:2`,`:N`] FUBINI_SIMPLE_COMPACT) THEN
  16   EXISTS_TAC `1` THEN
  17   SIMP_TAC[DIMINDEX_1; DIMINDEX_2; ARITH; COMPACT_CBALL; SLICE_CBALL] THEN
  18   REWRITE_TAC[VEC_COMPONENT; DROPOUT_0; REAL_SUB_RZERO] THEN
  19   ONCE_REWRITE_TAC[COND_RAND] THEN REWRITE_TAC[MEASURE_EMPTY] THEN
  20   SUBGOAL_THEN `!t. abs(t) <= &1 <=> t IN real_interval[-- &1,&1]`
  21    (fun th -> REWRITE_TAC[th])
  22   THENL [REWRITE_TAC[IN_REAL_INTERVAL] THEN REAL_ARITH_TAC; ALL_TAC] THEN
  23   REWRITE_TAC[HAS_REAL_INTEGRAL_RESTRICT_UNIV; BALL_1] THEN
  24   MATCH_MP_TAC HAS_REAL_INTEGRAL_EQ THEN
  25   EXISTS_TAC `\t. &2 * sqrt(&1 - t pow 2)` THEN CONJ_TAC THENL
  26    [X_GEN_TAC `t:real` THEN SIMP_TAC[IN_REAL_INTERVAL; MEASURE_INTERVAL] THEN
  27     REWRITE_TAC[REAL_BOUNDS_LE; VECTOR_ADD_LID; VECTOR_SUB_LZERO] THEN
  28     DISCH_TAC THEN
  29     W(MP_TAC o PART_MATCH (lhs o rand) CONTENT_1 o rand o snd) THEN
  30     REWRITE_TAC[LIFT_DROP; DROP_NEG] THEN
  31     ANTS_TAC THENL [ALL_TAC; SIMP_TAC[REAL_POW_ONE] THEN REAL_ARITH_TAC] THEN
  32     MATCH_MP_TAC(REAL_ARITH `&0 <= x ==> --x <= x`) THEN
  33     ASM_SIMP_TAC[SQRT_POS_LE; REAL_SUB_LE; GSYM REAL_LE_SQUARE_ABS;
  34                  REAL_ABS_NUM];
  35     ALL_TAC] THEN
  36   MP_TAC(ISPECL
  37    [`\x.  asn(x) + x * sqrt(&1 - x pow 2)`;
  38     `\x. &2 * sqrt(&1 - x pow 2)`;
  39     `-- &1`; `&1`] REAL_FUNDAMENTAL_THEOREM_OF_CALCULUS_INTERIOR) THEN
  40   REWRITE_TAC[ASN_1; ASN_NEG_1] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
  41   REWRITE_TAC[SQRT_0; REAL_MUL_RZERO; REAL_ADD_RID] THEN
  42   REWRITE_TAC[REAL_ARITH `x / &2 - --(x / &2) = x`] THEN
  43   DISCH_THEN MATCH_MP_TAC THEN CONJ_TAC THENL
  44    [MATCH_MP_TAC REAL_CONTINUOUS_ON_ADD THEN
  45     SIMP_TAC[REAL_CONTINUOUS_ON_ASN; IN_REAL_INTERVAL; REAL_BOUNDS_LE] THEN
  46     MATCH_MP_TAC REAL_CONTINUOUS_ON_MUL THEN
  47     REWRITE_TAC[REAL_CONTINUOUS_ON_ID] THEN
  48     GEN_REWRITE_TAC LAND_CONV [GSYM o_DEF] THEN
  49     MATCH_MP_TAC REAL_CONTINUOUS_ON_COMPOSE THEN
  50     SIMP_TAC[REAL_CONTINUOUS_ON_SUB; REAL_CONTINUOUS_ON_POW;
  51              REAL_CONTINUOUS_ON_ID; REAL_CONTINUOUS_ON_CONST] THEN
  52     MATCH_MP_TAC REAL_CONTINUOUS_ON_SQRT THEN
  53     REWRITE_TAC[FORALL_IN_IMAGE; IN_REAL_INTERVAL] THEN
  54     REWRITE_TAC[REAL_ARITH `&0 <= &1 - x <=> x <= &1 pow 2`] THEN
  55     REWRITE_TAC[GSYM REAL_LE_SQUARE_ABS; REAL_ABS_NUM] THEN
  56     REAL_ARITH_TAC;
  57     REWRITE_TAC[IN_REAL_INTERVAL; REAL_BOUNDS_LT] THEN REPEAT STRIP_TAC THEN
  58     REAL_DIFF_TAC THEN
  59     CONV_TAC NUM_REDUCE_CONV THEN
  60     REWRITE_TAC[REAL_MUL_LID; REAL_POW_1; REAL_MUL_RID] THEN
  61     REWRITE_TAC[REAL_SUB_LZERO; REAL_MUL_RNEG; REAL_INV_MUL] THEN
  62     ASM_REWRITE_TAC[REAL_SUB_LT; ABS_SQUARE_LT_1] THEN
  63     MATCH_MP_TAC(REAL_FIELD
  64      `s pow 2 = &1 - x pow 2 /\ x pow 2 < &1
  65       ==> (inv s + x * --(&2 * x) * inv (&2) * inv s + s) = &2 * s`) THEN
  66     ASM_SIMP_TAC[ABS_SQUARE_LT_1; SQRT_POW_2; REAL_SUB_LE; REAL_LT_IMP_LE]]);;
  67
  68 let AREA_CBALL = prove
  69  (`!z:real^2 r. &0 <= r ==> measure(cball(z,r)) = pi * r pow 2`,
  70   REPEAT STRIP_TAC THEN ASM_CASES_TAC `r = &0` THENL
  71    [ASM_SIMP_TAC[CBALL_SING; REAL_POW_2; REAL_MUL_RZERO] THEN
  72     MATCH_MP_TAC MEASURE_UNIQUE THEN
  73     REWRITE_TAC[HAS_MEASURE_0; NEGLIGIBLE_SING];
  74     ALL_TAC] THEN
  75   SUBGOAL_THEN `&0 < r` ASSUME_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
  76   MP_TAC(ISPECL [`cball(vec 0:real^2,&1)`; `r:real`; `z:real^2`; `pi`]
  77         HAS_MEASURE_AFFINITY) THEN
  78   REWRITE_TAC[HAS_MEASURE_MEASURABLE_MEASURE; MEASURABLE_CBALL;
  79               AREA_UNIT_CBALL] THEN
  80   ASM_REWRITE_TAC[real_abs; DIMINDEX_2] THEN
  81   DISCH_THEN(MP_TAC o CONJUNCT2) THEN
  82   GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [REAL_MUL_SYM] THEN
  83   DISCH_THEN(SUBST1_TAC o SYM) THEN AP_TERM_TAC THEN
  84   MATCH_MP_TAC SUBSET_ANTISYM THEN REWRITE_TAC[SUBSET; FORALL_IN_IMAGE] THEN
  85   REWRITE_TAC[IN_CBALL_0; IN_IMAGE] THEN REWRITE_TAC[IN_CBALL] THEN
  86   REWRITE_TAC[NORM_ARITH `dist(z,a + z) = norm a`; NORM_MUL] THEN
  87   ONCE_REWRITE_TAC[REAL_ARITH `abs r * x <= r <=> abs r * x <= r * &1`] THEN
  88   ASM_SIMP_TAC[real_abs; REAL_LE_LMUL; dist] THEN X_GEN_TAC `w:real^2` THEN
  89   DISCH_TAC THEN EXISTS_TAC `inv(r) % (w - z):real^2` THEN
  90   ASM_SIMP_TAC[VECTOR_MUL_ASSOC; REAL_MUL_RINV] THEN
  91   CONJ_TAC THENL [NORM_ARITH_TAC; ALL_TAC] THEN
  92   REWRITE_TAC[NORM_MUL; REAL_ABS_INV] THEN ASM_REWRITE_TAC[real_abs] THEN
  93   ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
  94   ASM_SIMP_TAC[GSYM real_div; REAL_LE_LDIV_EQ; REAL_MUL_LID] THEN
  95   ONCE_REWRITE_TAC[NORM_SUB] THEN ASM_REWRITE_TAC[]);;
  96
  97 let AREA_BALL = prove
  98  (`!z:real^2 r. &0 <= r ==> measure(ball(z,r)) = pi * r pow 2`,
  99   SIMP_TAC[GSYM INTERIOR_CBALL; GSYM AREA_CBALL] THEN
 100   REPEAT STRIP_TAC THEN MATCH_MP_TAC MEASURE_INTERIOR THEN
 101   SIMP_TAC[BOUNDED_CBALL; NEGLIGIBLE_CONVEX_FRONTIER; CONVEX_CBALL]);;
 102
 103 (* ------------------------------------------------------------------------- *)
 104 (* Volume of a ball too, just for fun.                                       *)
 105 (* ------------------------------------------------------------------------- *)
 106
 107 needs "Multivariate/wlog.ml";;
 108
 109 let VOLUME_CBALL = prove
 110  (`!z:real^3 r. &0 <= r ==> measure(cball(z,r)) = &4 / &3 * pi * r pow 3`,
 111   GEOM_ORIGIN_TAC `z:real^3` THEN REPEAT STRIP_TAC THEN
 112   MATCH_MP_TAC(INST_TYPE[`:2`,`:M`; `:3`,`:N`] FUBINI_SIMPLE_COMPACT) THEN
 113   EXISTS_TAC `1` THEN
 114   SIMP_TAC[DIMINDEX_2; DIMINDEX_3; ARITH; COMPACT_CBALL; SLICE_CBALL] THEN
 115   REWRITE_TAC[VEC_COMPONENT; DROPOUT_0; REAL_SUB_RZERO] THEN
 116   ONCE_REWRITE_TAC[COND_RAND] THEN REWRITE_TAC[MEASURE_EMPTY] THEN
 117   SUBGOAL_THEN `!t. abs(t) <= r <=> t IN real_interval[--r,r]`
 118    (fun th -> REWRITE_TAC[th])
 119   THENL [REWRITE_TAC[IN_REAL_INTERVAL] THEN REAL_ARITH_TAC; ALL_TAC] THEN
 120   REWRITE_TAC[HAS_REAL_INTEGRAL_RESTRICT_UNIV] THEN
 121   MATCH_MP_TAC HAS_REAL_INTEGRAL_EQ THEN
 122   EXISTS_TAC `\t. pi * (r pow 2 - t pow 2)` THEN CONJ_TAC THENL
 123    [X_GEN_TAC `t:real` THEN REWRITE_TAC[IN_REAL_INTERVAL; REAL_BOUNDS_LE] THEN
 124     SIMP_TAC[AREA_CBALL; SQRT_POS_LE; REAL_SUB_LE; GSYM REAL_LE_SQUARE_ABS;
 125              SQRT_POW_2; REAL_ARITH `abs x <= r ==> abs x <= abs r`];
 126     ALL_TAC] THEN
 127   MP_TAC(ISPECL
 128    [`\t. pi * (r pow 2 * t - &1 / &3 * t pow 3)`;
 129     `\t. pi * (r pow 2 - t pow 2)`;
 130     `--r:real`; `r:real`] REAL_FUNDAMENTAL_THEOREM_OF_CALCULUS) THEN
 131   REWRITE_TAC[] THEN ANTS_TAC THENL
 132    [CONJ_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
 133     REPEAT STRIP_TAC THEN REAL_DIFF_TAC THEN
 134     CONV_TAC NUM_REDUCE_CONV THEN CONV_TAC REAL_RING;
 135     MATCH_MP_TAC EQ_IMP THEN AP_THM_TAC THEN AP_TERM_TAC THEN
 136     CONV_TAC REAL_RING]);;
 137
 138 let VOLUME_BALL = prove
 139  (`!z:real^3 r. &0 <= r ==> measure(ball(z,r)) =  &4 / &3 * pi * r pow 3`,
 140   SIMP_TAC[GSYM INTERIOR_CBALL; GSYM VOLUME_CBALL] THEN
 141   REPEAT STRIP_TAC THEN MATCH_MP_TAC MEASURE_INTERIOR THEN
 142   SIMP_TAC[BOUNDED_CBALL; NEGLIGIBLE_CONVEX_FRONTIER; CONVEX_CBALL]);;