src/HOL/Analysis/Ball_Volume.thy
 changeset 68624 205d352ed727 parent 67982 7643b005b29a child 69064 5840724b1d71
```     1.1 --- a/src/HOL/Analysis/Ball_Volume.thy	Fri Jul 13 15:42:18 2018 +0200
1.2 +++ b/src/HOL/Analysis/Ball_Volume.thy	Fri Jul 13 16:54:36 2018 +0100
1.3 @@ -1,9 +1,9 @@
1.4  (*
1.5 -   File:     HOL/Analysis/Gamma_Function.thy
1.6 +   File:     HOL/Analysis/Ball_Volume.thy
1.7     Author:   Manuel Eberl, TU München
1.8  *)
1.9
1.10 -section \<open>The volume (Lebesgue measure) of an \$n\$-dimensional ball\<close>
1.11 +section \<open>The volume of an \$n\$-dimensional ball\<close>
1.12
1.13  theory Ball_Volume
1.14    imports Gamma_Function Lebesgue_Integral_Substitution
1.15 @@ -14,7 +14,7 @@
1.16    dimension need not be an integer; we also allow fractional dimensions, although we do
1.17    not use this case or prove anything about it for now.
1.18  \<close>
1.19 -definition unit_ball_vol :: "real \<Rightarrow> real" where
1.20 +definition%important unit_ball_vol :: "real \<Rightarrow> real" where
1.21    "unit_ball_vol n = pi powr (n / 2) / Gamma (n / 2 + 1)"
1.22
1.23  lemma unit_ball_vol_pos [simp]: "n \<ge> 0 \<Longrightarrow> unit_ball_vol n > 0"
1.24 @@ -177,7 +177,7 @@
1.25    assumes r: "r \<ge> 0"
1.26  begin
1.27
1.28 -theorem emeasure_cball:
1.29 +theorem%unimportant emeasure_cball:
1.30    "emeasure lborel (cball c r) = ennreal (unit_ball_vol (DIM('a)) * r ^ DIM('a))"
1.31  proof (cases "r = 0")
1.32    case False
1.33 @@ -202,11 +202,11 @@
1.34    finally show ?thesis .
1.35  qed auto
1.36
1.37 -corollary content_cball:
1.38 +corollary%unimportant content_cball:
1.39    "content (cball c r) = unit_ball_vol (DIM('a)) * r ^ DIM('a)"
1.40    by (simp add: measure_def emeasure_cball r)
1.41
1.42 -corollary emeasure_ball:
1.43 +corollary%unimportant emeasure_ball:
1.44    "emeasure lborel (ball c r) = ennreal (unit_ball_vol (DIM('a)) * r ^ DIM('a))"
1.45  proof -
1.46    from negligible_sphere[of c r] have "sphere c r \<in> null_sets lborel"
1.47 @@ -219,7 +219,7 @@
1.48    finally show ?thesis ..
1.49  qed
1.50
1.51 -corollary content_ball:
1.52 +corollary%important content_ball:
1.53    "content (ball c r) = unit_ball_vol (DIM('a)) * r ^ DIM('a)"
1.54    by (simp add: measure_def r emeasure_ball)
1.55
1.56 @@ -289,22 +289,25 @@
1.57  lemma unit_ball_vol_1 [simp]: "unit_ball_vol 1 = 2"
1.58    using unit_ball_vol_odd[of 0] by simp
1.59
1.60 -corollary unit_ball_vol_2: "unit_ball_vol 2 = pi"
1.61 +corollary%unimportant
1.62 +          unit_ball_vol_2: "unit_ball_vol 2 = pi"
1.63        and unit_ball_vol_3: "unit_ball_vol 3 = 4 / 3 * pi"
1.64        and unit_ball_vol_4: "unit_ball_vol 4 = pi\<^sup>2 / 2"
1.65        and unit_ball_vol_5: "unit_ball_vol 5 = 8 / 15 * pi\<^sup>2"
1.66    by (simp_all add: eval_unit_ball_vol)
1.67
1.68 -corollary circle_area: "r \<ge> 0 \<Longrightarrow> content (ball c r :: (real ^ 2) set) = r ^ 2 * pi"
1.69 +corollary%unimportant circle_area:
1.70 +  "r \<ge> 0 \<Longrightarrow> content (ball c r :: (real ^ 2) set) = r ^ 2 * pi"
1.71    by (simp add: content_ball unit_ball_vol_2)
1.72
1.73 -corollary sphere_volume: "r \<ge> 0 \<Longrightarrow> content (ball c r :: (real ^ 3) set) = 4 / 3 * r ^ 3 * pi"
1.74 +corollary%unimportant sphere_volume:
1.75 +  "r \<ge> 0 \<Longrightarrow> content (ball c r :: (real ^ 3) set) = 4 / 3 * r ^ 3 * pi"
1.76    by (simp add: content_ball unit_ball_vol_3)
1.77
1.78  text \<open>
1.79    Useful equivalent forms
1.80  \<close>
1.81 -corollary content_ball_eq_0_iff [simp]: "content (ball c r) = 0 \<longleftrightarrow> r \<le> 0"
1.82 +corollary%unimportant content_ball_eq_0_iff [simp]: "content (ball c r) = 0 \<longleftrightarrow> r \<le> 0"
1.83  proof -
1.84    have "r > 0 \<Longrightarrow> content (ball c r) > 0"
1.85      by (simp add: content_ball unit_ball_vol_def)
1.86 @@ -312,10 +315,10 @@
1.87      by (fastforce simp: ball_empty)
1.88  qed
1.89
1.90 -corollary content_ball_gt_0_iff [simp]: "0 < content (ball z r) \<longleftrightarrow> 0 < r"
1.91 +corollary%unimportant content_ball_gt_0_iff [simp]: "0 < content (ball z r) \<longleftrightarrow> 0 < r"
1.92    by (auto simp: zero_less_measure_iff)
1.93
1.94 -corollary content_cball_eq_0_iff [simp]: "content (cball c r) = 0 \<longleftrightarrow> r \<le> 0"
1.95 +corollary%unimportant content_cball_eq_0_iff [simp]: "content (cball c r) = 0 \<longleftrightarrow> r \<le> 0"
1.96  proof (cases "r = 0")
1.97    case False
1.98    moreover have "r > 0 \<Longrightarrow> content (cball c r) > 0"
1.99 @@ -324,7 +327,7 @@
1.100      by fastforce
1.101  qed auto
1.102
1.103 -corollary content_cball_gt_0_iff [simp]: "0 < content (cball z r) \<longleftrightarrow> 0 < r"
1.104 +corollary%unimportant content_cball_gt_0_iff [simp]: "0 < content (cball z r) \<longleftrightarrow> 0 < r"
1.105    by (auto simp: zero_less_measure_iff)
1.106
1.107  end
```