src/HOL/Analysis/Ball_Volume.thy
 author eberlm Sun Dec 24 14:28:10 2017 +0100 (17 months ago) changeset 67278 c60e3d615b8c child 67399 eab6ce8368fa permissions -rw-r--r--
Removed Analysis/ex/Circle_Area; replaced by more general Analysis/Ball_Volume
```     1 (*
```
```     2    File:     HOL/Analysis/Gamma_Function.thy
```
```     3    Author:   Manuel Eberl, TU München
```
```     4
```
```     5    The volume (Lebesgue measure) of an n-dimensional ball.
```
```     6 *)
```
```     7 section \<open>The volume of an \$n\$-ball\<close>
```
```     8 theory Ball_Volume
```
```     9   imports Gamma_Function Lebesgue_Integral_Substitution
```
```    10 begin
```
```    11
```
```    12 text \<open>
```
```    13   We define the volume of the unit ball in terms of the Gamma function. Note that the
```
```    14   dimension need not be an integer; we also allow fractional dimensions, although we do
```
```    15   not use this case or prove anything about it for now.
```
```    16 \<close>
```
```    17 definition unit_ball_vol :: "real \<Rightarrow> real" where
```
```    18   "unit_ball_vol n = pi powr (n / 2) / Gamma (n / 2 + 1)"
```
```    19
```
```    20 lemma unit_ball_vol_nonneg [simp]: "n \<ge> 0 \<Longrightarrow> unit_ball_vol n \<ge> 0"
```
```    21   by (auto simp add: unit_ball_vol_def intro!: divide_nonneg_pos Gamma_real_pos)
```
```    22
```
```    23 text \<open>
```
```    24   We first need the value of the following integral, which is at the core of
```
```    25   computing the measure of an \$n+1\$-dimensional ball in terms of the measure of an
```
```    26   \$n\$-dimensional one.
```
```    27 \<close>
```
```    28 lemma emeasure_cball_aux_integral:
```
```    29   "(\<integral>\<^sup>+x. indicator {-1..1} x * sqrt (1 - x\<^sup>2) ^ n \<partial>lborel) =
```
```    30       ennreal (Beta (1 / 2) (real n / 2 + 1))"
```
```    31 proof -
```
```    32   have "((\<lambda>t. t powr (-1 / 2) * (1 - t) powr (real n / 2)) has_integral
```
```    33           Beta (1 / 2) (real n / 2 + 1)) {0..1}"
```
```    34     using has_integral_Beta_real[of "1/2" "n / 2 + 1"] by simp
```
```    35   from nn_integral_has_integral_lebesgue[OF _ this] have
```
```    36      "ennreal (Beta (1 / 2) (real n / 2 + 1)) =
```
```    37         nn_integral lborel (\<lambda>t. ennreal (t powr (-1 / 2) * (1 - t) powr (real n / 2) *
```
```    38                                 indicator {0^2..1^2} t))"
```
```    39     by (simp add: mult_ac ennreal_mult' ennreal_indicator)
```
```    40   also have "\<dots> = (\<integral>\<^sup>+ x. ennreal (x\<^sup>2 powr - (1 / 2) * (1 - x\<^sup>2) powr (real n / 2) * (2 * x) *
```
```    41                           indicator {0..1} x) \<partial>lborel)"
```
```    42     by (subst nn_integral_substitution[where g = "\<lambda>x. x ^ 2" and g' = "\<lambda>x. 2 * x"])
```
```    43        (auto intro!: derivative_eq_intros continuous_intros)
```
```    44   also have "\<dots> = (\<integral>\<^sup>+ x. 2 * ennreal ((1 - x\<^sup>2) powr (real n / 2) * indicator {0..1} x) \<partial>lborel)"
```
```    45     by (intro nn_integral_cong_AE AE_I[of _ _ "{0}"])
```
```    46        (auto simp: indicator_def powr_minus powr_half_sqrt divide_simps ennreal_mult' mult_ac)
```
```    47   also have "\<dots> = (\<integral>\<^sup>+ x. ennreal ((1 - x\<^sup>2) powr (real n / 2) * indicator {0..1} x) \<partial>lborel) +
```
```    48                     (\<integral>\<^sup>+ x. ennreal ((1 - x\<^sup>2) powr (real n / 2) * indicator {0..1} x) \<partial>lborel)"
```
```    49     (is "_ = ?I + _") by (simp add: mult_2 nn_integral_add)
```
```    50   also have "?I = (\<integral>\<^sup>+ x. ennreal ((1 - x\<^sup>2) powr (real n / 2) * indicator {-1..0} x) \<partial>lborel)"
```
```    51     by (subst nn_integral_real_affine[of _ "-1" 0])
```
```    52        (auto simp: indicator_def intro!: nn_integral_cong)
```
```    53   hence "?I + ?I = \<dots> + ?I" by simp
```
```    54   also have "\<dots> = (\<integral>\<^sup>+ x. ennreal ((1 - x\<^sup>2) powr (real n / 2) *
```
```    55                     (indicator {-1..0} x + indicator{0..1} x)) \<partial>lborel)"
```
```    56     by (subst nn_integral_add [symmetric]) (auto simp: algebra_simps)
```
```    57   also have "\<dots> = (\<integral>\<^sup>+ x. ennreal ((1 - x\<^sup>2) powr (real n / 2) * indicator {-1..1} x) \<partial>lborel)"
```
```    58     by (intro nn_integral_cong_AE AE_I[of _ _ "{0}"]) (auto simp: indicator_def)
```
```    59   also have "\<dots> = (\<integral>\<^sup>+ x. ennreal (indicator {-1..1} x * sqrt (1 - x\<^sup>2) ^ n) \<partial>lborel)"
```
```    60     by (intro nn_integral_cong_AE AE_I[of _ _ "{1, -1}"])
```
```    61        (auto simp: powr_half_sqrt [symmetric] indicator_def abs_square_le_1
```
```    62           abs_square_eq_1 powr_def exp_of_nat_mult [symmetric] emeasure_lborel_countable)
```
```    63   finally show ?thesis ..
```
```    64 qed
```
```    65
```
```    66 lemma real_sqrt_le_iff': "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> sqrt x \<le> y \<longleftrightarrow> x \<le> y ^ 2"
```
```    67   using real_le_lsqrt sqrt_le_D by blast
```
```    68
```
```    69 lemma power2_le_iff_abs_le: "y \<ge> 0 \<Longrightarrow> (x::real) ^ 2 \<le> y ^ 2 \<longleftrightarrow> abs x \<le> y"
```
```    70   by (subst real_sqrt_le_iff' [symmetric]) auto
```
```    71
```
```    72 text \<open>
```
```    73   Isabelle's type system makes it very difficult to do an induction over the dimension
```
```    74   of a Euclidean space type, because the type would change in the inductive step. To avoid
```
```    75   this problem, we instead formulate the problem in a more concrete way by unfolding the
```
```    76   definition of the Euclidean norm.
```
```    77 \<close>
```
```    78 lemma emeasure_cball_aux:
```
```    79   assumes "finite A" "r > 0"
```
```    80   shows   "emeasure (Pi\<^sub>M A (\<lambda>_. lborel))
```
```    81              ({f. sqrt (\<Sum>i\<in>A. (f i)\<^sup>2) \<le> r} \<inter> space (Pi\<^sub>M A (\<lambda>_. lborel))) =
```
```    82              ennreal (unit_ball_vol (real (card A)) * r ^ card A)"
```
```    83   using assms
```
```    84 proof (induction arbitrary: r)
```
```    85   case (empty r)
```
```    86   thus ?case
```
```    87     by (simp add: unit_ball_vol_def space_PiM)
```
```    88 next
```
```    89   case (insert i A r)
```
```    90   interpret product_sigma_finite "\<lambda>_. lborel"
```
```    91     by standard
```
```    92   have "emeasure (Pi\<^sub>M (insert i A) (\<lambda>_. lborel))
```
```    93             ({f. sqrt (\<Sum>i\<in>insert i A. (f i)\<^sup>2) \<le> r} \<inter> space (Pi\<^sub>M (insert i A) (\<lambda>_. lborel))) =
```
```    94         nn_integral (Pi\<^sub>M (insert i A) (\<lambda>_. lborel))
```
```    95           (indicator ({f. sqrt (\<Sum>i\<in>insert i A. (f i)\<^sup>2) \<le> r} \<inter>
```
```    96           space (Pi\<^sub>M (insert i A) (\<lambda>_. lborel))))"
```
```    97     by (subst nn_integral_indicator) auto
```
```    98   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>
```
```    99                                 space (Pi\<^sub>M (insert i A) (\<lambda>_. lborel))) (x(i := y))
```
```   100                    \<partial>Pi\<^sub>M A (\<lambda>_. lborel) \<partial>lborel)"
```
```   101     using insert.prems insert.hyps by (subst product_nn_integral_insert_rev) auto
```
```   102   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>
```
```   103                sqrt (r ^ 2 - y ^ 2)} \<inter> space (Pi\<^sub>M A (\<lambda>_. lborel))) x \<partial>Pi\<^sub>M A (\<lambda>_. lborel) \<partial>lborel)"
```
```   104   proof (intro nn_integral_cong, goal_cases)
```
```   105     case (1 y f)
```
```   106     have *: "y \<in> {-r..r}" if "y ^ 2 + c \<le> r ^ 2" "c \<ge> 0" for c
```
```   107     proof -
```
```   108       have "y ^ 2 \<le> y ^ 2 + c" using that by simp
```
```   109       also have "\<dots> \<le> r ^ 2" by fact
```
```   110       finally show ?thesis
```
```   111         using \<open>r > 0\<close> by (simp add: power2_le_iff_abs_le abs_if split: if_splits)
```
```   112     qed
```
```   113     have "(\<Sum>x\<in>A. (if x = i then y else f x)\<^sup>2) = (\<Sum>x\<in>A. (f x)\<^sup>2)"
```
```   114       using insert.hyps by (intro sum.cong) auto
```
```   115     thus ?case using 1 \<open>r > 0\<close>
```
```   116       by (auto simp: sum_nonneg real_sqrt_le_iff' indicator_def PiE_def space_PiM dest!: *)
```
```   117   qed
```
```   118   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))
```
```   119                                    \<le> sqrt (r ^ 2 - y ^ 2)} \<inter> space (Pi\<^sub>M A (\<lambda>_. lborel))) x
```
```   120                   \<partial>Pi\<^sub>M A (\<lambda>_. lborel)) \<partial>lborel)" by (subst nn_integral_cmult) auto
```
```   121   also have "\<dots> = (\<integral>\<^sup>+ (y::real). indicator {-r..r} y * emeasure (PiM A (\<lambda>_. lborel))
```
```   122       ({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)"
```
```   123     using \<open>finite A\<close> by (intro nn_integral_cong, subst nn_integral_indicator) auto
```
```   124   also have "\<dots> = (\<integral>\<^sup>+ (y::real). indicator {-r..r} y * ennreal (unit_ball_vol (real (card A)) *
```
```   125                                   (sqrt (r ^ 2 - y ^ 2)) ^ card A) \<partial>lborel)"
```
```   126   proof (intro nn_integral_cong_AE, goal_cases)
```
```   127     case 1
```
```   128     have "AE y in lborel. y \<notin> {-r,r}"
```
```   129       by (intro AE_not_in countable_imp_null_set_lborel) auto
```
```   130     thus ?case
```
```   131     proof eventually_elim
```
```   132       case (elim y)
```
```   133       show ?case
```
```   134       proof (cases "y \<in> {-r<..<r}")
```
```   135         case True
```
```   136         hence "y\<^sup>2 < r\<^sup>2" by (subst real_sqrt_less_iff [symmetric]) auto
```
```   137         thus ?thesis by (subst insert.IH) (auto simp: real_sqrt_less_iff)
```
```   138       qed (insert elim, auto)
```
```   139     qed
```
```   140   qed
```
```   141   also have "\<dots> = ennreal (unit_ball_vol (real (card A))) *
```
```   142                     (\<integral>\<^sup>+ (y::real). indicator {-r..r} y * (sqrt (r ^ 2 - y ^ 2)) ^ card A \<partial>lborel)"
```
```   143     by (subst nn_integral_cmult [symmetric])
```
```   144        (auto simp: mult_ac ennreal_mult' [symmetric] indicator_def intro!: nn_integral_cong)
```
```   145   also have "(\<integral>\<^sup>+ (y::real). indicator {-r..r} y * (sqrt (r ^ 2 - y ^ 2)) ^ card A \<partial>lborel) =
```
```   146                (\<integral>\<^sup>+ (y::real). r ^ card A * indicator {-1..1} y * (sqrt (1 - y ^ 2)) ^ card A
```
```   147                \<partial>(distr lborel borel (op * (1/r))))" using \<open>r > 0\<close>
```
```   148     by (subst nn_integral_distr)
```
```   149        (auto simp: indicator_def field_simps real_sqrt_divide intro!: nn_integral_cong)
```
```   150   also have "\<dots> = (\<integral>\<^sup>+ x. ennreal (r ^ Suc (card A)) *
```
```   151                (indicator {- 1..1} x * sqrt (1 - x\<^sup>2) ^ card A) \<partial>lborel)" using \<open>r > 0\<close>
```
```   152     by (subst lborel_distr_mult) (auto simp: nn_integral_density ennreal_mult' [symmetric] mult_ac)
```
```   153   also have "\<dots> = ennreal (r ^ Suc (card A)) * (\<integral>\<^sup>+ x. indicator {- 1..1} x *
```
```   154                     sqrt (1 - x\<^sup>2) ^ card A \<partial>lborel)"
```
```   155     by (subst nn_integral_cmult) auto
```
```   156   also note emeasure_cball_aux_integral
```
```   157   also have "ennreal (unit_ball_vol (real (card A))) * (ennreal (r ^ Suc (card A)) *
```
```   158                  ennreal (Beta (1/2) (card A / 2 + 1))) =
```
```   159                ennreal (unit_ball_vol (card A) * Beta (1/2) (card A / 2 + 1) * r ^ Suc (card A))"
```
```   160     using \<open>r > 0\<close> by (simp add: ennreal_mult' [symmetric] mult_ac)
```
```   161   also have "unit_ball_vol (card A) * Beta (1/2) (card A / 2 + 1) = unit_ball_vol (Suc (card A))"
```
```   162     by (auto simp: unit_ball_vol_def Beta_def Gamma_eq_zero_iff field_simps
```
```   163           Gamma_one_half_real powr_half_sqrt [symmetric] powr_add [symmetric])
```
```   164   also have "Suc (card A) = card (insert i A)" using insert.hyps by simp
```
```   165   finally show ?case .
```
```   166 qed
```
```   167
```
```   168
```
```   169 text \<open>
```
```   170   We now get the main theorem very easily by just applying the above lemma.
```
```   171 \<close>
```
```   172 context
```
```   173   fixes c :: "'a :: euclidean_space" and r :: real
```
```   174   assumes r: "r \<ge> 0"
```
```   175 begin
```
```   176
```
```   177 theorem emeasure_cball:
```
```   178   "emeasure lborel (cball c r) = ennreal (unit_ball_vol (DIM('a)) * r ^ DIM('a))"
```
```   179 proof (cases "r = 0")
```
```   180   case False
```
```   181   with r have r: "r > 0" by simp
```
```   182   have "(lborel :: 'a measure) =
```
```   183           distr (Pi\<^sub>M Basis (\<lambda>_. lborel)) borel (\<lambda>f. \<Sum>b\<in>Basis. f b *\<^sub>R b)"
```
```   184     by (rule lborel_eq)
```
```   185   also have "emeasure \<dots> (cball 0 r) =
```
```   186                emeasure (Pi\<^sub>M Basis (\<lambda>_. lborel))
```
```   187                ({y. dist 0 (\<Sum>b\<in>Basis. y b *\<^sub>R b :: 'a) \<le> r} \<inter> space (Pi\<^sub>M Basis (\<lambda>_. lborel)))"
```
```   188     by (subst emeasure_distr) (auto simp: cball_def)
```
```   189   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}"
```
```   190     by (subst euclidean_dist_l2) (auto simp: L2_set_def)
```
```   191   also have "emeasure (Pi\<^sub>M Basis (\<lambda>_. lborel)) (\<dots> \<inter> space (Pi\<^sub>M Basis (\<lambda>_. lborel))) =
```
```   192                ennreal (unit_ball_vol (real DIM('a)) * r ^ DIM('a))"
```
```   193     using r by (subst emeasure_cball_aux) simp_all
```
```   194   also have "emeasure lborel (cball 0 r :: 'a set) =
```
```   195                emeasure (distr lborel borel (\<lambda>x. c + x)) (cball c r)"
```
```   196     by (subst emeasure_distr) (auto simp: cball_def dist_norm norm_minus_commute)
```
```   197   also have "distr lborel borel (\<lambda>x. c + x) = lborel"
```
```   198     using lborel_affine[of 1 c] by (simp add: density_1)
```
```   199   finally show ?thesis .
```
```   200 qed auto
```
```   201
```
```   202 corollary content_cball:
```
```   203   "content (cball c r) = unit_ball_vol (DIM('a)) * r ^ DIM('a)"
```
```   204   by (simp add: measure_def emeasure_cball r)
```
```   205
```
```   206 corollary emeasure_ball:
```
```   207   "emeasure lborel (ball c r) = ennreal (unit_ball_vol (DIM('a)) * r ^ DIM('a))"
```
```   208 proof -
```
```   209   from negligible_sphere[of c r] have "sphere c r \<in> null_sets lborel"
```
```   210     by (auto simp: null_sets_completion_iff negligible_iff_null_sets negligible_convex_frontier)
```
```   211   hence "emeasure lborel (ball c r \<union> sphere c r :: 'a set) = emeasure lborel (ball c r :: 'a set)"
```
```   212     by (intro emeasure_Un_null_set) auto
```
```   213   also have "ball c r \<union> sphere c r = (cball c r :: 'a set)" by auto
```
```   214   also have "emeasure lborel \<dots> = ennreal (unit_ball_vol (real DIM('a)) * r ^ DIM('a))"
```
```   215     by (rule emeasure_cball)
```
```   216   finally show ?thesis ..
```
```   217 qed
```
```   218
```
```   219 corollary content_ball:
```
```   220   "content (ball c r) = unit_ball_vol (DIM('a)) * r ^ DIM('a)"
```
```   221   by (simp add: measure_def r emeasure_ball)
```
```   222
```
```   223 end
```
```   224
```
```   225
```
```   226 text \<open>
```
```   227   Lastly, we now prove some nicer explicit formulas for the volume of the unit balls in
```
```   228   the cases of even and odd integer dimensions.
```
```   229 \<close>
```
```   230 lemma unit_ball_vol_even:
```
```   231   "unit_ball_vol (real (2 * n)) = pi ^ n / fact n"
```
```   232   by (simp add: unit_ball_vol_def add_ac powr_realpow Gamma_fact)
```
```   233
```
```   234 lemma unit_ball_vol_odd':
```
```   235         "unit_ball_vol (real (2 * n + 1)) = pi ^ n / pochhammer (1 / 2) (Suc n)"
```
```   236   and unit_ball_vol_odd:
```
```   237         "unit_ball_vol (real (2 * n + 1)) =
```
```   238            (2 ^ (2 * Suc n) * fact (Suc n)) / fact (2 * Suc n) * pi ^ n"
```
```   239 proof -
```
```   240   have "unit_ball_vol (real (2 * n + 1)) =
```
```   241           pi powr (real n + 1 / 2) / Gamma (1 / 2 + real (Suc n))"
```
```   242     by (simp add: unit_ball_vol_def field_simps)
```
```   243   also have "pochhammer (1 / 2) (Suc n) = Gamma (1 / 2 + real (Suc n)) / Gamma (1 / 2)"
```
```   244     by (intro pochhammer_Gamma) auto
```
```   245   hence "Gamma (1 / 2 + real (Suc n)) = sqrt pi * pochhammer (1 / 2) (Suc n)"
```
```   246     by (simp add: Gamma_one_half_real)
```
```   247   also have "pi powr (real n + 1 / 2) / \<dots> = pi ^ n / pochhammer (1 / 2) (Suc n)"
```
```   248     by (simp add: powr_add powr_half_sqrt powr_realpow)
```
```   249   finally show "unit_ball_vol (real (2 * n + 1)) = \<dots>" .
```
```   250   also have "pochhammer (1 / 2 :: real) (Suc n) =
```
```   251                fact (2 * Suc n) / (2 ^ (2 * Suc n) * fact (Suc n))"
```
```   252     using fact_double[of "Suc n", where ?'a = real] by (simp add: divide_simps mult_ac)
```
```   253   also have "pi ^n / \<dots> = (2 ^ (2 * Suc n) * fact (Suc n)) / fact (2 * Suc n) * pi ^ n"
```
```   254     by simp
```
```   255   finally show "unit_ball_vol (real (2 * n + 1)) = \<dots>" .
```
```   256 qed
```
```   257
```
```   258 lemma unit_ball_vol_numeral:
```
```   259   "unit_ball_vol (numeral (Num.Bit0 n)) = pi ^ numeral n / fact (numeral n)" (is ?th1)
```
```   260   "unit_ball_vol (numeral (Num.Bit1 n)) = 2 ^ (2 * Suc (numeral n)) * fact (Suc (numeral n)) /
```
```   261     fact (2 * Suc (numeral n)) * pi ^ numeral n" (is ?th2)
```
```   262 proof -
```
```   263   have "numeral (Num.Bit0 n) = (2 * numeral n :: nat)"
```
```   264     by (simp only: numeral_Bit0 mult_2 ring_distribs)
```
```   265   also have "unit_ball_vol \<dots> = pi ^ numeral n / fact (numeral n)"
```
```   266     by (rule unit_ball_vol_even)
```
```   267   finally show ?th1 by simp
```
```   268 next
```
```   269   have "numeral (Num.Bit1 n) = (2 * numeral n + 1 :: nat)"
```
```   270     by (simp only: numeral_Bit1 mult_2)
```
```   271   also have "unit_ball_vol \<dots> = 2 ^ (2 * Suc (numeral n)) * fact (Suc (numeral n)) /
```
```   272                                   fact (2 * Suc (numeral n)) * pi ^ numeral n"
```
```   273     by (rule unit_ball_vol_odd)
```
```   274   finally show ?th2 by simp
```
```   275 qed
```
```   276
```
```   277 lemmas eval_unit_ball_vol = unit_ball_vol_numeral fact_numeral
```
```   278
```
```   279
```
```   280 text \<open>
```
```   281   Just for fun, we compute the volume of unit balls for a few dimensions.
```
```   282 \<close>
```
```   283 lemma unit_ball_vol_0 [simp]: "unit_ball_vol 0 = 1"
```
```   284   using unit_ball_vol_even[of 0] by simp
```
```   285
```
```   286 lemma unit_ball_vol_1 [simp]: "unit_ball_vol 1 = 2"
```
```   287   using unit_ball_vol_odd[of 0] by simp
```
```   288
```
```   289 corollary unit_ball_vol_2: "unit_ball_vol 2 = pi"
```
```   290       and unit_ball_vol_3: "unit_ball_vol 3 = 4 / 3 * pi"
```
```   291       and unit_ball_vol_4: "unit_ball_vol 4 = pi\<^sup>2 / 2"
```
```   292       and unit_ball_vol_5: "unit_ball_vol 5 = 8 / 15 * pi\<^sup>2"
```
```   293   by (simp_all add: eval_unit_ball_vol)
```
```   294
```
```   295 corollary circle_area: "r \<ge> 0 \<Longrightarrow> content (ball c r :: (real ^ 2) set) = r ^ 2 * pi"
```
```   296   by (simp add: content_ball unit_ball_vol_2)
```
```   297
```
```   298 corollary sphere_volume: "r \<ge> 0 \<Longrightarrow> content (ball c r :: (real ^ 3) set) = 4 / 3 * r ^ 3 * pi"
```
```   299   by (simp add: content_ball unit_ball_vol_3)
```
```   300
```
```   301 end
```