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