(* ========================================================================= *)
(* Area of a circle.                                                         *)
(* ========================================================================= *)

needs "Multivariate/measure.ml";;
needs "Multivariate/realanalysis.ml";;

(* ------------------------------------------------------------------------- *)
(* Circle area. Should maybe extend WLOG tactics for such scaling.           *)
(* ------------------------------------------------------------------------- *)

let AREA_UNIT_CBALL = 
prove (`measure(cball(vec 0:real^2,&1)) = pi`,
REPEAT STRIP_TAC THEN MATCH_MP_TAC(INST_TYPE[`:1`,`:M`; `:2`,`:N`] FUBINI_SIMPLE_COMPACT) THEN EXISTS_TAC `1` THEN SIMP_TAC[DIMINDEX_1; DIMINDEX_2; ARITH; COMPACT_CBALL; SLICE_CBALL] THEN REWRITE_TAC[VEC_COMPONENT; DROPOUT_0; REAL_SUB_RZERO] THEN ONCE_REWRITE_TAC[COND_RAND] THEN REWRITE_TAC[MEASURE_EMPTY] THEN SUBGOAL_THEN `!t. abs(t) <= &1 <=> t IN real_interval[-- &1,&1]` (fun th -> REWRITE_TAC[th]) THENL [REWRITE_TAC[IN_REAL_INTERVAL] THEN REAL_ARITH_TAC; ALL_TAC] THEN REWRITE_TAC[HAS_REAL_INTEGRAL_RESTRICT_UNIV; BALL_1] THEN MATCH_MP_TAC HAS_REAL_INTEGRAL_EQ THEN EXISTS_TAC `\t. &2 * sqrt(&1 - t pow 2)` THEN CONJ_TAC THENL [X_GEN_TAC `t:real` THEN SIMP_TAC[IN_REAL_INTERVAL; MEASURE_INTERVAL] THEN REWRITE_TAC[REAL_BOUNDS_LE; VECTOR_ADD_LID; VECTOR_SUB_LZERO] THEN DISCH_TAC THEN W(MP_TAC o PART_MATCH (lhs o rand) CONTENT_1 o rand o snd) THEN REWRITE_TAC[LIFT_DROP; DROP_NEG] THEN ANTS_TAC THENL [ALL_TAC; SIMP_TAC[REAL_POW_ONE] THEN REAL_ARITH_TAC] THEN MATCH_MP_TAC(REAL_ARITH `&0 <= x ==> --x <= x`) THEN ASM_SIMP_TAC[SQRT_POS_LE; REAL_SUB_LE; GSYM REAL_LE_SQUARE_ABS; REAL_ABS_NUM]; ALL_TAC] THEN MP_TAC(ISPECL [`\x. asn(x) + x * sqrt(&1 - x pow 2)`; `\x. &2 * sqrt(&1 - x pow 2)`; `-- &1`; `&1`] REAL_FUNDAMENTAL_THEOREM_OF_CALCULUS_INTERIOR) THEN REWRITE_TAC[ASN_1; ASN_NEG_1] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN REWRITE_TAC[SQRT_0; REAL_MUL_RZERO; REAL_ADD_RID] THEN REWRITE_TAC[REAL_ARITH `x / &2 - --(x / &2) = x`] THEN DISCH_THEN MATCH_MP_TAC THEN CONJ_TAC THENL [MATCH_MP_TAC REAL_CONTINUOUS_ON_ADD THEN SIMP_TAC[REAL_CONTINUOUS_ON_ASN; IN_REAL_INTERVAL; REAL_BOUNDS_LE] THEN MATCH_MP_TAC REAL_CONTINUOUS_ON_MUL THEN REWRITE_TAC[REAL_CONTINUOUS_ON_ID] THEN GEN_REWRITE_TAC LAND_CONV [GSYM o_DEF] THEN MATCH_MP_TAC REAL_CONTINUOUS_ON_COMPOSE THEN SIMP_TAC[REAL_CONTINUOUS_ON_SUB; REAL_CONTINUOUS_ON_POW; REAL_CONTINUOUS_ON_ID; REAL_CONTINUOUS_ON_CONST] THEN MATCH_MP_TAC REAL_CONTINUOUS_ON_SQRT THEN REWRITE_TAC[FORALL_IN_IMAGE; IN_REAL_INTERVAL] THEN REWRITE_TAC[REAL_ARITH `&0 <= &1 - x <=> x <= &1 pow 2`] THEN REWRITE_TAC[GSYM REAL_LE_SQUARE_ABS; REAL_ABS_NUM] THEN REAL_ARITH_TAC; REWRITE_TAC[IN_REAL_INTERVAL; REAL_BOUNDS_LT] THEN REPEAT STRIP_TAC THEN REAL_DIFF_TAC THEN CONV_TAC NUM_REDUCE_CONV THEN REWRITE_TAC[REAL_MUL_LID; REAL_POW_1; REAL_MUL_RID] THEN REWRITE_TAC[REAL_SUB_LZERO; REAL_MUL_RNEG; REAL_INV_MUL] THEN ASM_REWRITE_TAC[REAL_SUB_LT; ABS_SQUARE_LT_1] THEN MATCH_MP_TAC(REAL_FIELD `s pow 2 = &1 - x pow 2 /\ x pow 2 < &1 ==> (inv s + x * --(&2 * x) * inv (&2) * inv s + s) = &2 * s`) THEN ASM_SIMP_TAC[ABS_SQUARE_LT_1; SQRT_POW_2; REAL_SUB_LE; REAL_LT_IMP_LE]]);;
let AREA_CBALL = 
prove (`!z:real^2 r. &0 <= r ==> measure(cball(z,r)) = pi * r pow 2`,
REPEAT STRIP_TAC THEN ASM_CASES_TAC `r = &0` THENL [ASM_SIMP_TAC[CBALL_SING; REAL_POW_2; REAL_MUL_RZERO] THEN MATCH_MP_TAC MEASURE_UNIQUE THEN REWRITE_TAC[HAS_MEASURE_0; NEGLIGIBLE_SING]; ALL_TAC] THEN SUBGOAL_THEN `&0 < r` ASSUME_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN MP_TAC(ISPECL [`cball(vec 0:real^2,&1)`; `r:real`; `z:real^2`; `pi`] HAS_MEASURE_AFFINITY) THEN REWRITE_TAC[HAS_MEASURE_MEASURABLE_MEASURE; MEASURABLE_CBALL; AREA_UNIT_CBALL] THEN ASM_REWRITE_TAC[real_abs; DIMINDEX_2] THEN DISCH_THEN(MP_TAC o CONJUNCT2) THEN GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [REAL_MUL_SYM] THEN DISCH_THEN(SUBST1_TAC o SYM) THEN AP_TERM_TAC THEN MATCH_MP_TAC SUBSET_ANTISYM THEN REWRITE_TAC[SUBSET; FORALL_IN_IMAGE] THEN REWRITE_TAC[IN_CBALL_0; IN_IMAGE] THEN REWRITE_TAC[IN_CBALL] THEN REWRITE_TAC[NORM_ARITH `dist(z,a + z) = norm a`; NORM_MUL] THEN ONCE_REWRITE_TAC[REAL_ARITH `abs r * x <= r <=> abs r * x <= r * &1`] THEN ASM_SIMP_TAC[real_abs; REAL_LE_LMUL; dist] THEN X_GEN_TAC `w:real^2` THEN DISCH_TAC THEN EXISTS_TAC `inv(r) % (w - z):real^2` THEN ASM_SIMP_TAC[VECTOR_MUL_ASSOC; REAL_MUL_RINV] THEN CONJ_TAC THENL [NORM_ARITH_TAC; ALL_TAC] THEN REWRITE_TAC[NORM_MUL; REAL_ABS_INV] THEN ASM_REWRITE_TAC[real_abs] THEN ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN ASM_SIMP_TAC[GSYM real_div; REAL_LE_LDIV_EQ; REAL_MUL_LID] THEN ONCE_REWRITE_TAC[NORM_SUB] THEN ASM_REWRITE_TAC[]);;
let AREA_BALL = 
prove (`!z:real^2 r. &0 <= r ==> measure(ball(z,r)) = pi * r pow 2`,
SIMP_TAC[GSYM INTERIOR_CBALL; GSYM AREA_CBALL] THEN REPEAT STRIP_TAC THEN MATCH_MP_TAC MEASURE_INTERIOR THEN SIMP_TAC[BOUNDED_CBALL; NEGLIGIBLE_CONVEX_FRONTIER; CONVEX_CBALL]);;
(* ------------------------------------------------------------------------- *) (* Volume of a ball too, just for fun. *) (* ------------------------------------------------------------------------- *) needs "Multivariate/wlog.ml";;
let VOLUME_CBALL = 
prove (`!z:real^3 r. &0 <= r ==> measure(cball(z,r)) = &4 / &3 * pi * r pow 3`,
GEOM_ORIGIN_TAC `z:real^3` THEN REPEAT STRIP_TAC THEN MATCH_MP_TAC(INST_TYPE[`:2`,`:M`; `:3`,`:N`] FUBINI_SIMPLE_COMPACT) THEN EXISTS_TAC `1` THEN SIMP_TAC[DIMINDEX_2; DIMINDEX_3; ARITH; COMPACT_CBALL; SLICE_CBALL] THEN REWRITE_TAC[VEC_COMPONENT; DROPOUT_0; REAL_SUB_RZERO] THEN ONCE_REWRITE_TAC[COND_RAND] THEN REWRITE_TAC[MEASURE_EMPTY] THEN SUBGOAL_THEN `!t. abs(t) <= r <=> t IN real_interval[--r,r]` (fun th -> REWRITE_TAC[th]) THENL [REWRITE_TAC[IN_REAL_INTERVAL] THEN REAL_ARITH_TAC; ALL_TAC] THEN REWRITE_TAC[HAS_REAL_INTEGRAL_RESTRICT_UNIV] THEN MATCH_MP_TAC HAS_REAL_INTEGRAL_EQ THEN EXISTS_TAC `\t. pi * (r pow 2 - t pow 2)` THEN CONJ_TAC THENL [X_GEN_TAC `t:real` THEN REWRITE_TAC[IN_REAL_INTERVAL; REAL_BOUNDS_LE] THEN SIMP_TAC[AREA_CBALL; SQRT_POS_LE; REAL_SUB_LE; GSYM REAL_LE_SQUARE_ABS; SQRT_POW_2; REAL_ARITH `abs x <= r ==> abs x <= abs r`]; ALL_TAC] THEN MP_TAC(ISPECL [`\t. pi * (r pow 2 * t - &1 / &3 * t pow 3)`; `\t. pi * (r pow 2 - t pow 2)`; `--r:real`; `r:real`] REAL_FUNDAMENTAL_THEOREM_OF_CALCULUS) THEN REWRITE_TAC[] THEN ANTS_TAC THENL [CONJ_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN REPEAT STRIP_TAC THEN REAL_DIFF_TAC THEN CONV_TAC NUM_REDUCE_CONV THEN CONV_TAC REAL_RING; MATCH_MP_TAC EQ_IMP THEN AP_THM_TAC THEN AP_TERM_TAC THEN CONV_TAC REAL_RING]);;
let VOLUME_BALL = 
prove (`!z:real^3 r. &0 <= r ==> measure(ball(z,r)) = &4 / &3 * pi * r pow 3`,
SIMP_TAC[GSYM INTERIOR_CBALL; GSYM VOLUME_CBALL] THEN REPEAT STRIP_TAC THEN MATCH_MP_TAC MEASURE_INTERIOR THEN SIMP_TAC[BOUNDED_CBALL; NEGLIGIBLE_CONVEX_FRONTIER; CONVEX_CBALL]);;