src/HOL/Analysis/Ball_Volume.thy
changeset 67278 c60e3d615b8c
child 67399 eab6ce8368fa
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Analysis/Ball_Volume.thy	Sun Dec 24 14:28:10 2017 +0100
     1.3 @@ -0,0 +1,301 @@
     1.4 +(*  
     1.5 +   File:     HOL/Analysis/Gamma_Function.thy
     1.6 +   Author:   Manuel Eberl, TU M√ľnchen
     1.7 +
     1.8 +   The volume (Lebesgue measure) of an n-dimensional ball.
     1.9 +*)
    1.10 +section \<open>The volume of an $n$-ball\<close>
    1.11 +theory Ball_Volume
    1.12 +  imports Gamma_Function Lebesgue_Integral_Substitution
    1.13 +begin
    1.14 +
    1.15 +text \<open>
    1.16 +  We define the volume of the unit ball in terms of the Gamma function. Note that the
    1.17 +  dimension need not be an integer; we also allow fractional dimensions, although we do
    1.18 +  not use this case or prove anything about it for now.
    1.19 +\<close>
    1.20 +definition unit_ball_vol :: "real \<Rightarrow> real" where
    1.21 +  "unit_ball_vol n = pi powr (n / 2) / Gamma (n / 2 + 1)"
    1.22 +
    1.23 +lemma unit_ball_vol_nonneg [simp]: "n \<ge> 0 \<Longrightarrow> unit_ball_vol n \<ge> 0"
    1.24 +  by (auto simp add: unit_ball_vol_def intro!: divide_nonneg_pos Gamma_real_pos)
    1.25 +
    1.26 +text \<open>
    1.27 +  We first need the value of the following integral, which is at the core of
    1.28 +  computing the measure of an $n+1$-dimensional ball in terms of the measure of an 
    1.29 +  $n$-dimensional one.
    1.30 +\<close>
    1.31 +lemma emeasure_cball_aux_integral:
    1.32 +  "(\<integral>\<^sup>+x. indicator {-1..1} x * sqrt (1 - x\<^sup>2) ^ n \<partial>lborel) = 
    1.33 +      ennreal (Beta (1 / 2) (real n / 2 + 1))"
    1.34 +proof -
    1.35 +  have "((\<lambda>t. t powr (-1 / 2) * (1 - t) powr (real n / 2)) has_integral
    1.36 +          Beta (1 / 2) (real n / 2 + 1)) {0..1}"
    1.37 +    using has_integral_Beta_real[of "1/2" "n / 2 + 1"] by simp
    1.38 +  from nn_integral_has_integral_lebesgue[OF _ this] have
    1.39 +     "ennreal (Beta (1 / 2) (real n / 2 + 1)) =
    1.40 +        nn_integral lborel (\<lambda>t. ennreal (t powr (-1 / 2) * (1 - t) powr (real n / 2) * 
    1.41 +                                indicator {0^2..1^2} t))"
    1.42 +    by (simp add: mult_ac ennreal_mult' ennreal_indicator)
    1.43 +  also have "\<dots> = (\<integral>\<^sup>+ x. ennreal (x\<^sup>2 powr - (1 / 2) * (1 - x\<^sup>2) powr (real n / 2) * (2 * x) *
    1.44 +                          indicator {0..1} x) \<partial>lborel)"
    1.45 +    by (subst nn_integral_substitution[where g = "\<lambda>x. x ^ 2" and g' = "\<lambda>x. 2 * x"])
    1.46 +       (auto intro!: derivative_eq_intros continuous_intros)
    1.47 +  also have "\<dots> = (\<integral>\<^sup>+ x. 2 * ennreal ((1 - x\<^sup>2) powr (real n / 2) * indicator {0..1} x) \<partial>lborel)"
    1.48 +    by (intro nn_integral_cong_AE AE_I[of _ _ "{0}"]) 
    1.49 +       (auto simp: indicator_def powr_minus powr_half_sqrt divide_simps ennreal_mult' mult_ac)
    1.50 +  also have "\<dots> = (\<integral>\<^sup>+ x. ennreal ((1 - x\<^sup>2) powr (real n / 2) * indicator {0..1} x) \<partial>lborel) +
    1.51 +                    (\<integral>\<^sup>+ x. ennreal ((1 - x\<^sup>2) powr (real n / 2) * indicator {0..1} x) \<partial>lborel)"
    1.52 +    (is "_ = ?I + _") by (simp add: mult_2 nn_integral_add)
    1.53 +  also have "?I = (\<integral>\<^sup>+ x. ennreal ((1 - x\<^sup>2) powr (real n / 2) * indicator {-1..0} x) \<partial>lborel)"
    1.54 +    by (subst nn_integral_real_affine[of _ "-1" 0])
    1.55 +       (auto simp: indicator_def intro!: nn_integral_cong)
    1.56 +  hence "?I + ?I = \<dots> + ?I" by simp
    1.57 +  also have "\<dots> = (\<integral>\<^sup>+ x. ennreal ((1 - x\<^sup>2) powr (real n / 2) * 
    1.58 +                    (indicator {-1..0} x + indicator{0..1} x)) \<partial>lborel)"
    1.59 +    by (subst nn_integral_add [symmetric]) (auto simp: algebra_simps)
    1.60 +  also have "\<dots> = (\<integral>\<^sup>+ x. ennreal ((1 - x\<^sup>2) powr (real n / 2) * indicator {-1..1} x) \<partial>lborel)"
    1.61 +    by (intro nn_integral_cong_AE AE_I[of _ _ "{0}"]) (auto simp: indicator_def)
    1.62 +  also have "\<dots> = (\<integral>\<^sup>+ x. ennreal (indicator {-1..1} x * sqrt (1 - x\<^sup>2) ^ n) \<partial>lborel)"
    1.63 +    by (intro nn_integral_cong_AE AE_I[of _ _ "{1, -1}"])
    1.64 +       (auto simp: powr_half_sqrt [symmetric] indicator_def abs_square_le_1
    1.65 +          abs_square_eq_1 powr_def exp_of_nat_mult [symmetric] emeasure_lborel_countable)
    1.66 +  finally show ?thesis ..
    1.67 +qed
    1.68 +
    1.69 +lemma real_sqrt_le_iff': "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> sqrt x \<le> y \<longleftrightarrow> x \<le> y ^ 2"
    1.70 +  using real_le_lsqrt sqrt_le_D by blast
    1.71 +
    1.72 +lemma power2_le_iff_abs_le: "y \<ge> 0 \<Longrightarrow> (x::real) ^ 2 \<le> y ^ 2 \<longleftrightarrow> abs x \<le> y"
    1.73 +  by (subst real_sqrt_le_iff' [symmetric]) auto
    1.74 +
    1.75 +text \<open>
    1.76 +  Isabelle's type system makes it very difficult to do an induction over the dimension 
    1.77 +  of a Euclidean space type, because the type would change in the inductive step. To avoid 
    1.78 +  this problem, we instead formulate the problem in a more concrete way by unfolding the 
    1.79 +  definition of the Euclidean norm.
    1.80 +\<close>
    1.81 +lemma emeasure_cball_aux:
    1.82 +  assumes "finite A" "r > 0"
    1.83 +  shows   "emeasure (Pi\<^sub>M A (\<lambda>_. lborel))
    1.84 +             ({f. sqrt (\<Sum>i\<in>A. (f i)\<^sup>2) \<le> r} \<inter> space (Pi\<^sub>M A (\<lambda>_. lborel))) =
    1.85 +             ennreal (unit_ball_vol (real (card A)) * r ^ card A)"
    1.86 +  using assms
    1.87 +proof (induction arbitrary: r)
    1.88 +  case (empty r)
    1.89 +  thus ?case
    1.90 +    by (simp add: unit_ball_vol_def space_PiM)
    1.91 +next
    1.92 +  case (insert i A r)
    1.93 +  interpret product_sigma_finite "\<lambda>_. lborel"
    1.94 +    by standard
    1.95 +  have "emeasure (Pi\<^sub>M (insert i A) (\<lambda>_. lborel)) 
    1.96 +            ({f. sqrt (\<Sum>i\<in>insert i A. (f i)\<^sup>2) \<le> r} \<inter> space (Pi\<^sub>M (insert i A) (\<lambda>_. lborel))) =
    1.97 +        nn_integral (Pi\<^sub>M (insert i A) (\<lambda>_. lborel))
    1.98 +          (indicator ({f. sqrt (\<Sum>i\<in>insert i A. (f i)\<^sup>2) \<le> r} \<inter>
    1.99 +          space (Pi\<^sub>M (insert i A) (\<lambda>_. lborel))))"
   1.100 +    by (subst nn_integral_indicator) auto
   1.101 +  also have "\<dots> = (\<integral>\<^sup>+ y. \<integral>\<^sup>+ x. indicator ({f. sqrt ((f i)\<^sup>2 + (\<Sum>i\<in>A. (f i)\<^sup>2)) \<le> r} \<inter> 
   1.102 +                                space (Pi\<^sub>M (insert i A) (\<lambda>_. lborel))) (x(i := y)) 
   1.103 +                   \<partial>Pi\<^sub>M A (\<lambda>_. lborel) \<partial>lborel)"
   1.104 +    using insert.prems insert.hyps by (subst product_nn_integral_insert_rev) auto
   1.105 +  also have "\<dots> = (\<integral>\<^sup>+ (y::real). \<integral>\<^sup>+ x. indicator {-r..r} y * indicator ({f. sqrt ((\<Sum>i\<in>A. (f i)\<^sup>2)) \<le> 
   1.106 +               sqrt (r ^ 2 - y ^ 2)} \<inter> space (Pi\<^sub>M A (\<lambda>_. lborel))) x \<partial>Pi\<^sub>M A (\<lambda>_. lborel) \<partial>lborel)"
   1.107 +  proof (intro nn_integral_cong, goal_cases)
   1.108 +    case (1 y f)
   1.109 +    have *: "y \<in> {-r..r}" if "y ^ 2 + c \<le> r ^ 2" "c \<ge> 0" for c
   1.110 +    proof -
   1.111 +      have "y ^ 2 \<le> y ^ 2 + c" using that by simp
   1.112 +      also have "\<dots> \<le> r ^ 2" by fact
   1.113 +      finally show ?thesis
   1.114 +        using \<open>r > 0\<close> by (simp add: power2_le_iff_abs_le abs_if split: if_splits)
   1.115 +    qed
   1.116 +    have "(\<Sum>x\<in>A. (if x = i then y else f x)\<^sup>2) = (\<Sum>x\<in>A. (f x)\<^sup>2)"
   1.117 +      using insert.hyps by (intro sum.cong) auto
   1.118 +    thus ?case using 1 \<open>r > 0\<close>
   1.119 +      by (auto simp: sum_nonneg real_sqrt_le_iff' indicator_def PiE_def space_PiM dest!: *)
   1.120 +  qed
   1.121 +  also have "\<dots> = (\<integral>\<^sup>+ (y::real). indicator {-r..r} y * (\<integral>\<^sup>+ x. indicator ({f. sqrt ((\<Sum>i\<in>A. (f i)\<^sup>2)) 
   1.122 +                                   \<le> sqrt (r ^ 2 - y ^ 2)} \<inter> space (Pi\<^sub>M A (\<lambda>_. lborel))) x
   1.123 +                  \<partial>Pi\<^sub>M A (\<lambda>_. lborel)) \<partial>lborel)" by (subst nn_integral_cmult) auto
   1.124 +  also have "\<dots> = (\<integral>\<^sup>+ (y::real). indicator {-r..r} y * emeasure (PiM A (\<lambda>_. lborel)) 
   1.125 +      ({f. sqrt ((\<Sum>i\<in>A. (f i)\<^sup>2)) \<le> sqrt (r ^ 2 - y ^ 2)} \<inter> space (Pi\<^sub>M A (\<lambda>_. lborel))) \<partial>lborel)"
   1.126 +    using \<open>finite A\<close> by (intro nn_integral_cong, subst nn_integral_indicator) auto
   1.127 +  also have "\<dots> = (\<integral>\<^sup>+ (y::real). indicator {-r..r} y * ennreal (unit_ball_vol (real (card A)) * 
   1.128 +                                  (sqrt (r ^ 2 - y ^ 2)) ^ card A) \<partial>lborel)"
   1.129 +  proof (intro nn_integral_cong_AE, goal_cases)
   1.130 +    case 1
   1.131 +    have "AE y in lborel. y \<notin> {-r,r}"
   1.132 +      by (intro AE_not_in countable_imp_null_set_lborel) auto
   1.133 +    thus ?case
   1.134 +    proof eventually_elim
   1.135 +      case (elim y)
   1.136 +      show ?case
   1.137 +      proof (cases "y \<in> {-r<..<r}")
   1.138 +        case True
   1.139 +        hence "y\<^sup>2 < r\<^sup>2" by (subst real_sqrt_less_iff [symmetric]) auto
   1.140 +        thus ?thesis by (subst insert.IH) (auto simp: real_sqrt_less_iff)
   1.141 +      qed (insert elim, auto)
   1.142 +    qed
   1.143 +  qed
   1.144 +  also have "\<dots> = ennreal (unit_ball_vol (real (card A))) * 
   1.145 +                    (\<integral>\<^sup>+ (y::real). indicator {-r..r} y * (sqrt (r ^ 2 - y ^ 2)) ^ card A \<partial>lborel)"
   1.146 +    by (subst nn_integral_cmult [symmetric])
   1.147 +       (auto simp: mult_ac ennreal_mult' [symmetric] indicator_def intro!: nn_integral_cong)
   1.148 +  also have "(\<integral>\<^sup>+ (y::real). indicator {-r..r} y * (sqrt (r ^ 2 - y ^ 2)) ^ card A \<partial>lborel) =
   1.149 +               (\<integral>\<^sup>+ (y::real). r ^ card A * indicator {-1..1} y * (sqrt (1 - y ^ 2)) ^ card A  
   1.150 +               \<partial>(distr lborel borel (op * (1/r))))" using \<open>r > 0\<close>
   1.151 +    by (subst nn_integral_distr)
   1.152 +       (auto simp: indicator_def field_simps real_sqrt_divide intro!: nn_integral_cong)
   1.153 +  also have "\<dots> = (\<integral>\<^sup>+ x. ennreal (r ^ Suc (card A)) * 
   1.154 +               (indicator {- 1..1} x * sqrt (1 - x\<^sup>2) ^ card A) \<partial>lborel)" using \<open>r > 0\<close>
   1.155 +    by (subst lborel_distr_mult) (auto simp: nn_integral_density ennreal_mult' [symmetric] mult_ac)
   1.156 +  also have "\<dots> = ennreal (r ^ Suc (card A)) * (\<integral>\<^sup>+ x. indicator {- 1..1} x * 
   1.157 +                    sqrt (1 - x\<^sup>2) ^ card A \<partial>lborel)"
   1.158 +    by (subst nn_integral_cmult) auto
   1.159 +  also note emeasure_cball_aux_integral
   1.160 +  also have "ennreal (unit_ball_vol (real (card A))) * (ennreal (r ^ Suc (card A)) *
   1.161 +                 ennreal (Beta (1/2) (card A / 2 + 1))) = 
   1.162 +               ennreal (unit_ball_vol (card A) * Beta (1/2) (card A / 2 + 1) * r ^ Suc (card A))"
   1.163 +    using \<open>r > 0\<close> by (simp add: ennreal_mult' [symmetric] mult_ac)
   1.164 +  also have "unit_ball_vol (card A) * Beta (1/2) (card A / 2 + 1) = unit_ball_vol (Suc (card A))"
   1.165 +    by (auto simp: unit_ball_vol_def Beta_def Gamma_eq_zero_iff field_simps 
   1.166 +          Gamma_one_half_real powr_half_sqrt [symmetric] powr_add [symmetric])
   1.167 +  also have "Suc (card A) = card (insert i A)" using insert.hyps by simp
   1.168 +  finally show ?case .
   1.169 +qed
   1.170 +
   1.171 +
   1.172 +text \<open>
   1.173 +  We now get the main theorem very easily by just applying the above lemma.
   1.174 +\<close>
   1.175 +context
   1.176 +  fixes c :: "'a :: euclidean_space" and r :: real
   1.177 +  assumes r: "r \<ge> 0"
   1.178 +begin
   1.179 +
   1.180 +theorem emeasure_cball:
   1.181 +  "emeasure lborel (cball c r) = ennreal (unit_ball_vol (DIM('a)) * r ^ DIM('a))"
   1.182 +proof (cases "r = 0")
   1.183 +  case False
   1.184 +  with r have r: "r > 0" by simp
   1.185 +  have "(lborel :: 'a measure) = 
   1.186 +          distr (Pi\<^sub>M Basis (\<lambda>_. lborel)) borel (\<lambda>f. \<Sum>b\<in>Basis. f b *\<^sub>R b)"
   1.187 +    by (rule lborel_eq)
   1.188 +  also have "emeasure \<dots> (cball 0 r) = 
   1.189 +               emeasure (Pi\<^sub>M Basis (\<lambda>_. lborel)) 
   1.190 +               ({y. dist 0 (\<Sum>b\<in>Basis. y b *\<^sub>R b :: 'a) \<le> r} \<inter> space (Pi\<^sub>M Basis (\<lambda>_. lborel)))"
   1.191 +    by (subst emeasure_distr) (auto simp: cball_def)
   1.192 +  also have "{f. dist 0 (\<Sum>b\<in>Basis. f b *\<^sub>R b :: 'a) \<le> r} = {f. sqrt (\<Sum>i\<in>Basis. (f i)\<^sup>2) \<le> r}"
   1.193 +    by (subst euclidean_dist_l2) (auto simp: L2_set_def)
   1.194 +  also have "emeasure (Pi\<^sub>M Basis (\<lambda>_. lborel)) (\<dots> \<inter> space (Pi\<^sub>M Basis (\<lambda>_. lborel))) =
   1.195 +               ennreal (unit_ball_vol (real DIM('a)) * r ^ DIM('a))"
   1.196 +    using r by (subst emeasure_cball_aux) simp_all
   1.197 +  also have "emeasure lborel (cball 0 r :: 'a set) =
   1.198 +               emeasure (distr lborel borel (\<lambda>x. c + x)) (cball c r)"
   1.199 +    by (subst emeasure_distr) (auto simp: cball_def dist_norm norm_minus_commute)
   1.200 +  also have "distr lborel borel (\<lambda>x. c + x) = lborel"
   1.201 +    using lborel_affine[of 1 c] by (simp add: density_1)
   1.202 +  finally show ?thesis .
   1.203 +qed auto
   1.204 +
   1.205 +corollary content_cball:
   1.206 +  "content (cball c r) = unit_ball_vol (DIM('a)) * r ^ DIM('a)"
   1.207 +  by (simp add: measure_def emeasure_cball r)
   1.208 +
   1.209 +corollary emeasure_ball:
   1.210 +  "emeasure lborel (ball c r) = ennreal (unit_ball_vol (DIM('a)) * r ^ DIM('a))"
   1.211 +proof -
   1.212 +  from negligible_sphere[of c r] have "sphere c r \<in> null_sets lborel"
   1.213 +    by (auto simp: null_sets_completion_iff negligible_iff_null_sets negligible_convex_frontier)
   1.214 +  hence "emeasure lborel (ball c r \<union> sphere c r :: 'a set) = emeasure lborel (ball c r :: 'a set)"
   1.215 +    by (intro emeasure_Un_null_set) auto
   1.216 +  also have "ball c r \<union> sphere c r = (cball c r :: 'a set)" by auto
   1.217 +  also have "emeasure lborel \<dots> = ennreal (unit_ball_vol (real DIM('a)) * r ^ DIM('a))"
   1.218 +    by (rule emeasure_cball)
   1.219 +  finally show ?thesis ..
   1.220 +qed
   1.221 +
   1.222 +corollary content_ball:
   1.223 +  "content (ball c r) = unit_ball_vol (DIM('a)) * r ^ DIM('a)"
   1.224 +  by (simp add: measure_def r emeasure_ball)
   1.225 +
   1.226 +end
   1.227 +
   1.228 +
   1.229 +text \<open>
   1.230 +  Lastly, we now prove some nicer explicit formulas for the volume of the unit balls in 
   1.231 +  the cases of even and odd integer dimensions.
   1.232 +\<close>
   1.233 +lemma unit_ball_vol_even:
   1.234 +  "unit_ball_vol (real (2 * n)) = pi ^ n / fact n"
   1.235 +  by (simp add: unit_ball_vol_def add_ac powr_realpow Gamma_fact)
   1.236 +
   1.237 +lemma unit_ball_vol_odd':
   1.238 +        "unit_ball_vol (real (2 * n + 1)) = pi ^ n / pochhammer (1 / 2) (Suc n)"
   1.239 +  and unit_ball_vol_odd:
   1.240 +        "unit_ball_vol (real (2 * n + 1)) =
   1.241 +           (2 ^ (2 * Suc n) * fact (Suc n)) / fact (2 * Suc n) * pi ^ n"
   1.242 +proof -
   1.243 +  have "unit_ball_vol (real (2 * n + 1)) = 
   1.244 +          pi powr (real n + 1 / 2) / Gamma (1 / 2 + real (Suc n))"
   1.245 +    by (simp add: unit_ball_vol_def field_simps)
   1.246 +  also have "pochhammer (1 / 2) (Suc n) = Gamma (1 / 2 + real (Suc n)) / Gamma (1 / 2)"
   1.247 +    by (intro pochhammer_Gamma) auto
   1.248 +  hence "Gamma (1 / 2 + real (Suc n)) = sqrt pi * pochhammer (1 / 2) (Suc n)"
   1.249 +    by (simp add: Gamma_one_half_real)
   1.250 +  also have "pi powr (real n + 1 / 2) / \<dots> = pi ^ n / pochhammer (1 / 2) (Suc n)"
   1.251 +    by (simp add: powr_add powr_half_sqrt powr_realpow)
   1.252 +  finally show "unit_ball_vol (real (2 * n + 1)) = \<dots>" .
   1.253 +  also have "pochhammer (1 / 2 :: real) (Suc n) = 
   1.254 +               fact (2 * Suc n) / (2 ^ (2 * Suc n) * fact (Suc n))"
   1.255 +    using fact_double[of "Suc n", where ?'a = real] by (simp add: divide_simps mult_ac)
   1.256 +  also have "pi ^n / \<dots> = (2 ^ (2 * Suc n) * fact (Suc n)) / fact (2 * Suc n) * pi ^ n"
   1.257 +    by simp
   1.258 +  finally show "unit_ball_vol (real (2 * n + 1)) = \<dots>" .
   1.259 +qed
   1.260 +
   1.261 +lemma unit_ball_vol_numeral:
   1.262 +  "unit_ball_vol (numeral (Num.Bit0 n)) = pi ^ numeral n / fact (numeral n)" (is ?th1)
   1.263 +  "unit_ball_vol (numeral (Num.Bit1 n)) = 2 ^ (2 * Suc (numeral n)) * fact (Suc (numeral n)) /
   1.264 +    fact (2 * Suc (numeral n)) * pi ^ numeral n" (is ?th2)
   1.265 +proof -
   1.266 +  have "numeral (Num.Bit0 n) = (2 * numeral n :: nat)" 
   1.267 +    by (simp only: numeral_Bit0 mult_2 ring_distribs)
   1.268 +  also have "unit_ball_vol \<dots> = pi ^ numeral n / fact (numeral n)"
   1.269 +    by (rule unit_ball_vol_even)
   1.270 +  finally show ?th1 by simp
   1.271 +next
   1.272 +  have "numeral (Num.Bit1 n) = (2 * numeral n + 1 :: nat)"
   1.273 +    by (simp only: numeral_Bit1 mult_2)
   1.274 +  also have "unit_ball_vol \<dots> = 2 ^ (2 * Suc (numeral n)) * fact (Suc (numeral n)) /
   1.275 +                                  fact (2 * Suc (numeral n)) * pi ^ numeral n"
   1.276 +    by (rule unit_ball_vol_odd)
   1.277 +  finally show ?th2 by simp
   1.278 +qed
   1.279 +
   1.280 +lemmas eval_unit_ball_vol = unit_ball_vol_numeral fact_numeral
   1.281 +
   1.282 +
   1.283 +text \<open>
   1.284 +  Just for fun, we compute the volume of unit balls for a few dimensions.
   1.285 +\<close>
   1.286 +lemma unit_ball_vol_0 [simp]: "unit_ball_vol 0 = 1"
   1.287 +  using unit_ball_vol_even[of 0] by simp
   1.288 +
   1.289 +lemma unit_ball_vol_1 [simp]: "unit_ball_vol 1 = 2"
   1.290 +  using unit_ball_vol_odd[of 0] by simp
   1.291 +
   1.292 +corollary unit_ball_vol_2: "unit_ball_vol 2 = pi"
   1.293 +      and unit_ball_vol_3: "unit_ball_vol 3 = 4 / 3 * pi"
   1.294 +      and unit_ball_vol_4: "unit_ball_vol 4 = pi\<^sup>2 / 2"
   1.295 +      and unit_ball_vol_5: "unit_ball_vol 5 = 8 / 15 * pi\<^sup>2"
   1.296 +  by (simp_all add: eval_unit_ball_vol)
   1.297 +
   1.298 +corollary circle_area: "r \<ge> 0 \<Longrightarrow> content (ball c r :: (real ^ 2) set) = r ^ 2 * pi"
   1.299 +  by (simp add: content_ball unit_ball_vol_2)
   1.300 +
   1.301 +corollary sphere_volume: "r \<ge> 0 \<Longrightarrow> content (ball c r :: (real ^ 3) set) = 4 / 3 * r ^ 3 * pi"
   1.302 +  by (simp add: content_ball unit_ball_vol_3)
   1.303 +
   1.304 +end