src/HOL/Analysis/Ball_Volume.thy
author paulson <lp15@cam.ac.uk>
Sun Apr 15 13:57:00 2018 +0100 (13 months ago)
changeset 67982 7643b005b29a
parent 67976 75b94eb58c3d
child 68624 205d352ed727
permissions -rw-r--r--
various new results on measures, integrals, etc., and some simplified proofs
eberlm@67278
     1
(*  
eberlm@67278
     2
   File:     HOL/Analysis/Gamma_Function.thy
eberlm@67278
     3
   Author:   Manuel Eberl, TU M√ľnchen
lp15@67982
     4
*)
eberlm@67278
     5
lp15@67982
     6
section \<open>The volume (Lebesgue measure) of an $n$-dimensional ball\<close>
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 \<open>
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
\<close>
eberlm@67278
    17
definition unit_ball_vol :: "real \<Rightarrow> 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 \<ge> 0 \<Longrightarrow> 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 \<ge> 0 \<Longrightarrow> unit_ball_vol n \<ge> 0"
lp15@67719
    24
  by (simp add: dual_order.strict_implies_order)
eberlm@67278
    25
eberlm@67278
    26
text \<open>
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
\<close>
eberlm@67278
    31
lemma emeasure_cball_aux_integral:
eberlm@67278
    32
  "(\<integral>\<^sup>+x. indicator {-1..1} x * sqrt (1 - x\<^sup>2) ^ n \<partial>lborel) = 
eberlm@67278
    33
      ennreal (Beta (1 / 2) (real n / 2 + 1))"
eberlm@67278
    34
proof -
eberlm@67278
    35
  have "((\<lambda>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 (\<lambda>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 "\<dots> = (\<integral>\<^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) \<partial>lborel)"
eberlm@67278
    45
    by (subst nn_integral_substitution[where g = "\<lambda>x. x ^ 2" and g' = "\<lambda>x. 2 * x"])
lp15@67976
    46
       (auto intro!: derivative_eq_intros continuous_intros simp: set_borel_measurable_def)
eberlm@67278
    47
  also have "\<dots> = (\<integral>\<^sup>+ x. 2 * ennreal ((1 - x\<^sup>2) powr (real n / 2) * indicator {0..1} x) \<partial>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 "\<dots> = (\<integral>\<^sup>+ x. ennreal ((1 - x\<^sup>2) powr (real n / 2) * indicator {0..1} x) \<partial>lborel) +
eberlm@67278
    51
                    (\<integral>\<^sup>+ x. ennreal ((1 - x\<^sup>2) powr (real n / 2) * indicator {0..1} x) \<partial>lborel)"
eberlm@67278
    52
    (is "_ = ?I + _") by (simp add: mult_2 nn_integral_add)
eberlm@67278
    53
  also have "?I = (\<integral>\<^sup>+ x. ennreal ((1 - x\<^sup>2) powr (real n / 2) * indicator {-1..0} x) \<partial>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 = \<dots> + ?I" by simp
eberlm@67278
    57
  also have "\<dots> = (\<integral>\<^sup>+ x. ennreal ((1 - x\<^sup>2) powr (real n / 2) * 
eberlm@67278
    58
                    (indicator {-1..0} x + indicator{0..1} x)) \<partial>lborel)"
eberlm@67278
    59
    by (subst nn_integral_add [symmetric]) (auto simp: algebra_simps)
eberlm@67278
    60
  also have "\<dots> = (\<integral>\<^sup>+ x. ennreal ((1 - x\<^sup>2) powr (real n / 2) * indicator {-1..1} x) \<partial>lborel)"
eberlm@67278
    61
    by (intro nn_integral_cong_AE AE_I[of _ _ "{0}"]) (auto simp: indicator_def)
eberlm@67278
    62
  also have "\<dots> = (\<integral>\<^sup>+ x. ennreal (indicator {-1..1} x * sqrt (1 - x\<^sup>2) ^ n) \<partial>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 \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> sqrt x \<le> y \<longleftrightarrow> x \<le> 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 \<ge> 0 \<Longrightarrow> (x::real) ^ 2 \<le> y ^ 2 \<longleftrightarrow> abs x \<le> y"
eberlm@67278
    73
  by (subst real_sqrt_le_iff' [symmetric]) auto
eberlm@67278
    74
eberlm@67278
    75
text \<open>
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
\<close>
eberlm@67278
    81
lemma emeasure_cball_aux:
eberlm@67278
    82
  assumes "finite A" "r > 0"
eberlm@67278
    83
  shows   "emeasure (Pi\<^sub>M A (\<lambda>_. lborel))
eberlm@67278
    84
             ({f. sqrt (\<Sum>i\<in>A. (f i)\<^sup>2) \<le> r} \<inter> space (Pi\<^sub>M A (\<lambda>_. 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 "\<lambda>_. lborel"
eberlm@67278
    94
    by standard
eberlm@67278
    95
  have "emeasure (Pi\<^sub>M (insert i A) (\<lambda>_. lborel)) 
eberlm@67278
    96
            ({f. sqrt (\<Sum>i\<in>insert i A. (f i)\<^sup>2) \<le> r} \<inter> space (Pi\<^sub>M (insert i A) (\<lambda>_. lborel))) =
eberlm@67278
    97
        nn_integral (Pi\<^sub>M (insert i A) (\<lambda>_. lborel))
eberlm@67278
    98
          (indicator ({f. sqrt (\<Sum>i\<in>insert i A. (f i)\<^sup>2) \<le> r} \<inter>
eberlm@67278
    99
          space (Pi\<^sub>M (insert i A) (\<lambda>_. lborel))))"
eberlm@67278
   100
    by (subst nn_integral_indicator) auto
eberlm@67278
   101
  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> 
eberlm@67278
   102
                                space (Pi\<^sub>M (insert i A) (\<lambda>_. lborel))) (x(i := y)) 
eberlm@67278
   103
                   \<partial>Pi\<^sub>M A (\<lambda>_. lborel) \<partial>lborel)"
eberlm@67278
   104
    using insert.prems insert.hyps by (subst product_nn_integral_insert_rev) auto
eberlm@67278
   105
  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> 
eberlm@67278
   106
               sqrt (r ^ 2 - y ^ 2)} \<inter> space (Pi\<^sub>M A (\<lambda>_. lborel))) x \<partial>Pi\<^sub>M A (\<lambda>_. lborel) \<partial>lborel)"
eberlm@67278
   107
  proof (intro nn_integral_cong, goal_cases)
eberlm@67278
   108
    case (1 y f)
eberlm@67278
   109
    have *: "y \<in> {-r..r}" if "y ^ 2 + c \<le> r ^ 2" "c \<ge> 0" for c
eberlm@67278
   110
    proof -
eberlm@67278
   111
      have "y ^ 2 \<le> y ^ 2 + c" using that by simp
eberlm@67278
   112
      also have "\<dots> \<le> r ^ 2" by fact
eberlm@67278
   113
      finally show ?thesis
eberlm@67278
   114
        using \<open>r > 0\<close> by (simp add: power2_le_iff_abs_le abs_if split: if_splits)
eberlm@67278
   115
    qed
eberlm@67278
   116
    have "(\<Sum>x\<in>A. (if x = i then y else f x)\<^sup>2) = (\<Sum>x\<in>A. (f x)\<^sup>2)"
eberlm@67278
   117
      using insert.hyps by (intro sum.cong) auto
eberlm@67278
   118
    thus ?case using 1 \<open>r > 0\<close>
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 "\<dots> = (\<integral>\<^sup>+ (y::real). indicator {-r..r} y * (\<integral>\<^sup>+ x. indicator ({f. sqrt ((\<Sum>i\<in>A. (f i)\<^sup>2)) 
eberlm@67278
   122
                                   \<le> sqrt (r ^ 2 - y ^ 2)} \<inter> space (Pi\<^sub>M A (\<lambda>_. lborel))) x
eberlm@67278
   123
                  \<partial>Pi\<^sub>M A (\<lambda>_. lborel)) \<partial>lborel)" by (subst nn_integral_cmult) auto
eberlm@67278
   124
  also have "\<dots> = (\<integral>\<^sup>+ (y::real). indicator {-r..r} y * emeasure (PiM A (\<lambda>_. lborel)) 
eberlm@67278
   125
      ({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)"
eberlm@67278
   126
    using \<open>finite A\<close> by (intro nn_integral_cong, subst nn_integral_indicator) auto
eberlm@67278
   127
  also have "\<dots> = (\<integral>\<^sup>+ (y::real). indicator {-r..r} y * ennreal (unit_ball_vol (real (card A)) * 
eberlm@67278
   128
                                  (sqrt (r ^ 2 - y ^ 2)) ^ card A) \<partial>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 \<notin> {-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 \<in> {-r<..<r}")
eberlm@67278
   138
        case True
eberlm@67278
   139
        hence "y\<^sup>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 "\<dots> = ennreal (unit_ball_vol (real (card A))) * 
eberlm@67278
   145
                    (\<integral>\<^sup>+ (y::real). indicator {-r..r} y * (sqrt (r ^ 2 - y ^ 2)) ^ card A \<partial>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 "(\<integral>\<^sup>+ (y::real). indicator {-r..r} y * (sqrt (r ^ 2 - y ^ 2)) ^ card A \<partial>lborel) =
eberlm@67278
   149
               (\<integral>\<^sup>+ (y::real). r ^ card A * indicator {-1..1} y * (sqrt (1 - y ^ 2)) ^ card A  
nipkow@67399
   150
               \<partial>(distr lborel borel (( * ) (1/r))))" using \<open>r > 0\<close>
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 "\<dots> = (\<integral>\<^sup>+ x. ennreal (r ^ Suc (card A)) * 
eberlm@67278
   154
               (indicator {- 1..1} x * sqrt (1 - x\<^sup>2) ^ card A) \<partial>lborel)" using \<open>r > 0\<close>
eberlm@67278
   155
    by (subst lborel_distr_mult) (auto simp: nn_integral_density ennreal_mult' [symmetric] mult_ac)
eberlm@67278
   156
  also have "\<dots> = ennreal (r ^ Suc (card A)) * (\<integral>\<^sup>+ x. indicator {- 1..1} x * 
eberlm@67278
   157
                    sqrt (1 - x\<^sup>2) ^ card A \<partial>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 \<open>r > 0\<close> 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 \<open>
eberlm@67278
   173
  We now get the main theorem very easily by just applying the above lemma.
eberlm@67278
   174
\<close>
eberlm@67278
   175
context
eberlm@67278
   176
  fixes c :: "'a :: euclidean_space" and r :: real
eberlm@67278
   177
  assumes r: "r \<ge> 0"
eberlm@67278
   178
begin
eberlm@67278
   179
eberlm@67278
   180
theorem 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 (\<lambda>_. lborel)) borel (\<lambda>f. \<Sum>b\<in>Basis. f b *\<^sub>R b)"
eberlm@67278
   187
    by (rule lborel_eq)
eberlm@67278
   188
  also have "emeasure \<dots> (cball 0 r) = 
eberlm@67278
   189
               emeasure (Pi\<^sub>M Basis (\<lambda>_. lborel)) 
eberlm@67278
   190
               ({y. dist 0 (\<Sum>b\<in>Basis. y b *\<^sub>R b :: 'a) \<le> r} \<inter> space (Pi\<^sub>M Basis (\<lambda>_. lborel)))"
eberlm@67278
   191
    by (subst emeasure_distr) (auto simp: cball_def)
eberlm@67278
   192
  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}"
eberlm@67278
   193
    by (subst euclidean_dist_l2) (auto simp: L2_set_def)
eberlm@67278
   194
  also have "emeasure (Pi\<^sub>M Basis (\<lambda>_. lborel)) (\<dots> \<inter> space (Pi\<^sub>M Basis (\<lambda>_. 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 (\<lambda>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 (\<lambda>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@67278
   205
corollary 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@67278
   209
corollary 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 \<in> 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 \<union> 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 \<union> sphere c r = (cball c r :: 'a set)" by auto
eberlm@67278
   217
  also have "emeasure lborel \<dots> = 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@67278
   222
corollary 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 \<open>
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
\<close>
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) / \<dots> = 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)) = \<dots>" .
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 / \<dots> = (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)) = \<dots>" .
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 \<dots> = 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 \<dots> = 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 \<open>
eberlm@67278
   284
  Just for fun, we compute the volume of unit balls for a few dimensions.
eberlm@67278
   285
\<close>
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@67278
   292
corollary unit_ball_vol_2: "unit_ball_vol 2 = pi"
eberlm@67278
   293
      and unit_ball_vol_3: "unit_ball_vol 3 = 4 / 3 * pi"
eberlm@67278
   294
      and unit_ball_vol_4: "unit_ball_vol 4 = pi\<^sup>2 / 2"
eberlm@67278
   295
      and unit_ball_vol_5: "unit_ball_vol 5 = 8 / 15 * pi\<^sup>2"
eberlm@67278
   296
  by (simp_all add: eval_unit_ball_vol)
eberlm@67278
   297
eberlm@67278
   298
corollary circle_area: "r \<ge> 0 \<Longrightarrow> content (ball c r :: (real ^ 2) set) = r ^ 2 * pi"
eberlm@67278
   299
  by (simp add: content_ball unit_ball_vol_2)
eberlm@67278
   300
eberlm@67278
   301
corollary sphere_volume: "r \<ge> 0 \<Longrightarrow> content (ball c r :: (real ^ 3) set) = 4 / 3 * r ^ 3 * pi"
eberlm@67278
   302
  by (simp add: content_ball unit_ball_vol_3)
eberlm@67278
   303
lp15@67982
   304
text \<open>
lp15@67982
   305
  Useful equivalent forms
lp15@67982
   306
\<close>
lp15@67982
   307
corollary content_ball_eq_0_iff [simp]: "content (ball c r) = 0 \<longleftrightarrow> r \<le> 0"
lp15@67982
   308
proof -
lp15@67982
   309
  have "r > 0 \<Longrightarrow> content (ball c r) > 0"
lp15@67982
   310
    by (simp add: content_ball unit_ball_vol_def)
lp15@67982
   311
  then show ?thesis
lp15@67982
   312
    by (fastforce simp: ball_empty)
lp15@67982
   313
qed
lp15@67982
   314
lp15@67982
   315
corollary content_ball_gt_0_iff [simp]: "0 < content (ball z r) \<longleftrightarrow> 0 < r"
lp15@67982
   316
  by (auto simp: zero_less_measure_iff)
lp15@67982
   317
lp15@67982
   318
corollary content_cball_eq_0_iff [simp]: "content (cball c r) = 0 \<longleftrightarrow> r \<le> 0"
lp15@67982
   319
proof (cases "r = 0")
lp15@67982
   320
  case False
lp15@67982
   321
  moreover have "r > 0 \<Longrightarrow> content (cball c r) > 0"
lp15@67982
   322
    by (simp add: content_cball unit_ball_vol_def)
lp15@67982
   323
  ultimately show ?thesis
lp15@67982
   324
    by fastforce
lp15@67982
   325
qed auto
lp15@67982
   326
lp15@67982
   327
corollary content_cball_gt_0_iff [simp]: "0 < content (cball z r) \<longleftrightarrow> 0 < r"
lp15@67982
   328
  by (auto simp: zero_less_measure_iff)
lp15@67982
   329
eberlm@67278
   330
end