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