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