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