author eberlm Sun Dec 24 14:28:10 2017 +0100 (17 months ago) changeset 67278 c60e3d615b8c parent 67277 7dda4a667e40 child 67279 d327c11c9f3e
Removed Analysis/ex/Circle_Area; replaced by more general Analysis/Ball_Volume
 src/HOL/Analysis/Analysis.thy file | annotate | diff | revisions src/HOL/Analysis/Ball_Volume.thy file | annotate | diff | revisions src/HOL/Analysis/Borel_Space.thy file | annotate | diff | revisions src/HOL/Analysis/Complex_Transcendental.thy file | annotate | diff | revisions src/HOL/Analysis/Gamma_Function.thy file | annotate | diff | revisions src/HOL/Analysis/ex/Circle_Area.thy file | annotate | diff | revisions src/HOL/ROOT file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Analysis/Analysis.thy	Sun Dec 24 14:46:26 2017 +0100
1.2 +++ b/src/HOL/Analysis/Analysis.thy	Sun Dec 24 14:28:10 2017 +0100
1.3 @@ -22,6 +22,7 @@
1.4    FPS_Convergence
1.5    Generalised_Binomial_Theorem
1.6    Gamma_Function
1.7 +  Ball_Volume
1.8  begin
1.9
1.10  end
```
```     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/src/HOL/Analysis/Ball_Volume.thy	Sun Dec 24 14:28:10 2017 +0100
2.3 @@ -0,0 +1,301 @@
2.4 +(*
2.5 +   File:     HOL/Analysis/Gamma_Function.thy
2.6 +   Author:   Manuel Eberl, TU München
2.7 +
2.8 +   The volume (Lebesgue measure) of an n-dimensional ball.
2.9 +*)
2.10 +section \<open>The volume of an \$n\$-ball\<close>
2.11 +theory Ball_Volume
2.12 +  imports Gamma_Function Lebesgue_Integral_Substitution
2.13 +begin
2.14 +
2.15 +text \<open>
2.16 +  We define the volume of the unit ball in terms of the Gamma function. Note that the
2.17 +  dimension need not be an integer; we also allow fractional dimensions, although we do
2.18 +  not use this case or prove anything about it for now.
2.19 +\<close>
2.20 +definition unit_ball_vol :: "real \<Rightarrow> real" where
2.21 +  "unit_ball_vol n = pi powr (n / 2) / Gamma (n / 2 + 1)"
2.22 +
2.23 +lemma unit_ball_vol_nonneg [simp]: "n \<ge> 0 \<Longrightarrow> unit_ball_vol n \<ge> 0"
2.24 +  by (auto simp add: unit_ball_vol_def intro!: divide_nonneg_pos Gamma_real_pos)
2.25 +
2.26 +text \<open>
2.27 +  We first need the value of the following integral, which is at the core of
2.28 +  computing the measure of an \$n+1\$-dimensional ball in terms of the measure of an
2.29 +  \$n\$-dimensional one.
2.30 +\<close>
2.31 +lemma emeasure_cball_aux_integral:
2.32 +  "(\<integral>\<^sup>+x. indicator {-1..1} x * sqrt (1 - x\<^sup>2) ^ n \<partial>lborel) =
2.33 +      ennreal (Beta (1 / 2) (real n / 2 + 1))"
2.34 +proof -
2.35 +  have "((\<lambda>t. t powr (-1 / 2) * (1 - t) powr (real n / 2)) has_integral
2.36 +          Beta (1 / 2) (real n / 2 + 1)) {0..1}"
2.37 +    using has_integral_Beta_real[of "1/2" "n / 2 + 1"] by simp
2.38 +  from nn_integral_has_integral_lebesgue[OF _ this] have
2.39 +     "ennreal (Beta (1 / 2) (real n / 2 + 1)) =
2.40 +        nn_integral lborel (\<lambda>t. ennreal (t powr (-1 / 2) * (1 - t) powr (real n / 2) *
2.41 +                                indicator {0^2..1^2} t))"
2.42 +    by (simp add: mult_ac ennreal_mult' ennreal_indicator)
2.43 +  also have "\<dots> = (\<integral>\<^sup>+ x. ennreal (x\<^sup>2 powr - (1 / 2) * (1 - x\<^sup>2) powr (real n / 2) * (2 * x) *
2.44 +                          indicator {0..1} x) \<partial>lborel)"
2.45 +    by (subst nn_integral_substitution[where g = "\<lambda>x. x ^ 2" and g' = "\<lambda>x. 2 * x"])
2.46 +       (auto intro!: derivative_eq_intros continuous_intros)
2.47 +  also have "\<dots> = (\<integral>\<^sup>+ x. 2 * ennreal ((1 - x\<^sup>2) powr (real n / 2) * indicator {0..1} x) \<partial>lborel)"
2.48 +    by (intro nn_integral_cong_AE AE_I[of _ _ "{0}"])
2.49 +       (auto simp: indicator_def powr_minus powr_half_sqrt divide_simps ennreal_mult' mult_ac)
2.50 +  also have "\<dots> = (\<integral>\<^sup>+ x. ennreal ((1 - x\<^sup>2) powr (real n / 2) * indicator {0..1} x) \<partial>lborel) +
2.51 +                    (\<integral>\<^sup>+ x. ennreal ((1 - x\<^sup>2) powr (real n / 2) * indicator {0..1} x) \<partial>lborel)"
2.52 +    (is "_ = ?I + _") by (simp add: mult_2 nn_integral_add)
2.53 +  also have "?I = (\<integral>\<^sup>+ x. ennreal ((1 - x\<^sup>2) powr (real n / 2) * indicator {-1..0} x) \<partial>lborel)"
2.54 +    by (subst nn_integral_real_affine[of _ "-1" 0])
2.55 +       (auto simp: indicator_def intro!: nn_integral_cong)
2.56 +  hence "?I + ?I = \<dots> + ?I" by simp
2.57 +  also have "\<dots> = (\<integral>\<^sup>+ x. ennreal ((1 - x\<^sup>2) powr (real n / 2) *
2.58 +                    (indicator {-1..0} x + indicator{0..1} x)) \<partial>lborel)"
2.59 +    by (subst nn_integral_add [symmetric]) (auto simp: algebra_simps)
2.60 +  also have "\<dots> = (\<integral>\<^sup>+ x. ennreal ((1 - x\<^sup>2) powr (real n / 2) * indicator {-1..1} x) \<partial>lborel)"
2.61 +    by (intro nn_integral_cong_AE AE_I[of _ _ "{0}"]) (auto simp: indicator_def)
2.62 +  also have "\<dots> = (\<integral>\<^sup>+ x. ennreal (indicator {-1..1} x * sqrt (1 - x\<^sup>2) ^ n) \<partial>lborel)"
2.63 +    by (intro nn_integral_cong_AE AE_I[of _ _ "{1, -1}"])
2.64 +       (auto simp: powr_half_sqrt [symmetric] indicator_def abs_square_le_1
2.65 +          abs_square_eq_1 powr_def exp_of_nat_mult [symmetric] emeasure_lborel_countable)
2.66 +  finally show ?thesis ..
2.67 +qed
2.68 +
2.69 +lemma real_sqrt_le_iff': "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> sqrt x \<le> y \<longleftrightarrow> x \<le> y ^ 2"
2.70 +  using real_le_lsqrt sqrt_le_D by blast
2.71 +
2.72 +lemma power2_le_iff_abs_le: "y \<ge> 0 \<Longrightarrow> (x::real) ^ 2 \<le> y ^ 2 \<longleftrightarrow> abs x \<le> y"
2.73 +  by (subst real_sqrt_le_iff' [symmetric]) auto
2.74 +
2.75 +text \<open>
2.76 +  Isabelle's type system makes it very difficult to do an induction over the dimension
2.77 +  of a Euclidean space type, because the type would change in the inductive step. To avoid
2.78 +  this problem, we instead formulate the problem in a more concrete way by unfolding the
2.79 +  definition of the Euclidean norm.
2.80 +\<close>
2.81 +lemma emeasure_cball_aux:
2.82 +  assumes "finite A" "r > 0"
2.83 +  shows   "emeasure (Pi\<^sub>M A (\<lambda>_. lborel))
2.84 +             ({f. sqrt (\<Sum>i\<in>A. (f i)\<^sup>2) \<le> r} \<inter> space (Pi\<^sub>M A (\<lambda>_. lborel))) =
2.85 +             ennreal (unit_ball_vol (real (card A)) * r ^ card A)"
2.86 +  using assms
2.87 +proof (induction arbitrary: r)
2.88 +  case (empty r)
2.89 +  thus ?case
2.90 +    by (simp add: unit_ball_vol_def space_PiM)
2.91 +next
2.92 +  case (insert i A r)
2.93 +  interpret product_sigma_finite "\<lambda>_. lborel"
2.94 +    by standard
2.95 +  have "emeasure (Pi\<^sub>M (insert i A) (\<lambda>_. lborel))
2.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))) =
2.97 +        nn_integral (Pi\<^sub>M (insert i A) (\<lambda>_. lborel))
2.98 +          (indicator ({f. sqrt (\<Sum>i\<in>insert i A. (f i)\<^sup>2) \<le> r} \<inter>
2.99 +          space (Pi\<^sub>M (insert i A) (\<lambda>_. lborel))))"
2.100 +    by (subst nn_integral_indicator) auto
2.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>
2.102 +                                space (Pi\<^sub>M (insert i A) (\<lambda>_. lborel))) (x(i := y))
2.103 +                   \<partial>Pi\<^sub>M A (\<lambda>_. lborel) \<partial>lborel)"
2.104 +    using insert.prems insert.hyps by (subst product_nn_integral_insert_rev) auto
2.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>
2.106 +               sqrt (r ^ 2 - y ^ 2)} \<inter> space (Pi\<^sub>M A (\<lambda>_. lborel))) x \<partial>Pi\<^sub>M A (\<lambda>_. lborel) \<partial>lborel)"
2.107 +  proof (intro nn_integral_cong, goal_cases)
2.108 +    case (1 y f)
2.109 +    have *: "y \<in> {-r..r}" if "y ^ 2 + c \<le> r ^ 2" "c \<ge> 0" for c
2.110 +    proof -
2.111 +      have "y ^ 2 \<le> y ^ 2 + c" using that by simp
2.112 +      also have "\<dots> \<le> r ^ 2" by fact
2.113 +      finally show ?thesis
2.114 +        using \<open>r > 0\<close> by (simp add: power2_le_iff_abs_le abs_if split: if_splits)
2.115 +    qed
2.116 +    have "(\<Sum>x\<in>A. (if x = i then y else f x)\<^sup>2) = (\<Sum>x\<in>A. (f x)\<^sup>2)"
2.117 +      using insert.hyps by (intro sum.cong) auto
2.118 +    thus ?case using 1 \<open>r > 0\<close>
2.119 +      by (auto simp: sum_nonneg real_sqrt_le_iff' indicator_def PiE_def space_PiM dest!: *)
2.120 +  qed
2.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))
2.122 +                                   \<le> sqrt (r ^ 2 - y ^ 2)} \<inter> space (Pi\<^sub>M A (\<lambda>_. lborel))) x
2.123 +                  \<partial>Pi\<^sub>M A (\<lambda>_. lborel)) \<partial>lborel)" by (subst nn_integral_cmult) auto
2.124 +  also have "\<dots> = (\<integral>\<^sup>+ (y::real). indicator {-r..r} y * emeasure (PiM A (\<lambda>_. lborel))
2.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)"
2.126 +    using \<open>finite A\<close> by (intro nn_integral_cong, subst nn_integral_indicator) auto
2.127 +  also have "\<dots> = (\<integral>\<^sup>+ (y::real). indicator {-r..r} y * ennreal (unit_ball_vol (real (card A)) *
2.128 +                                  (sqrt (r ^ 2 - y ^ 2)) ^ card A) \<partial>lborel)"
2.129 +  proof (intro nn_integral_cong_AE, goal_cases)
2.130 +    case 1
2.131 +    have "AE y in lborel. y \<notin> {-r,r}"
2.132 +      by (intro AE_not_in countable_imp_null_set_lborel) auto
2.133 +    thus ?case
2.134 +    proof eventually_elim
2.135 +      case (elim y)
2.136 +      show ?case
2.137 +      proof (cases "y \<in> {-r<..<r}")
2.138 +        case True
2.139 +        hence "y\<^sup>2 < r\<^sup>2" by (subst real_sqrt_less_iff [symmetric]) auto
2.140 +        thus ?thesis by (subst insert.IH) (auto simp: real_sqrt_less_iff)
2.141 +      qed (insert elim, auto)
2.142 +    qed
2.143 +  qed
2.144 +  also have "\<dots> = ennreal (unit_ball_vol (real (card A))) *
2.145 +                    (\<integral>\<^sup>+ (y::real). indicator {-r..r} y * (sqrt (r ^ 2 - y ^ 2)) ^ card A \<partial>lborel)"
2.146 +    by (subst nn_integral_cmult [symmetric])
2.147 +       (auto simp: mult_ac ennreal_mult' [symmetric] indicator_def intro!: nn_integral_cong)
2.148 +  also have "(\<integral>\<^sup>+ (y::real). indicator {-r..r} y * (sqrt (r ^ 2 - y ^ 2)) ^ card A \<partial>lborel) =
2.149 +               (\<integral>\<^sup>+ (y::real). r ^ card A * indicator {-1..1} y * (sqrt (1 - y ^ 2)) ^ card A
2.150 +               \<partial>(distr lborel borel (op * (1/r))))" using \<open>r > 0\<close>
2.151 +    by (subst nn_integral_distr)
2.152 +       (auto simp: indicator_def field_simps real_sqrt_divide intro!: nn_integral_cong)
2.153 +  also have "\<dots> = (\<integral>\<^sup>+ x. ennreal (r ^ Suc (card A)) *
2.154 +               (indicator {- 1..1} x * sqrt (1 - x\<^sup>2) ^ card A) \<partial>lborel)" using \<open>r > 0\<close>
2.155 +    by (subst lborel_distr_mult) (auto simp: nn_integral_density ennreal_mult' [symmetric] mult_ac)
2.156 +  also have "\<dots> = ennreal (r ^ Suc (card A)) * (\<integral>\<^sup>+ x. indicator {- 1..1} x *
2.157 +                    sqrt (1 - x\<^sup>2) ^ card A \<partial>lborel)"
2.158 +    by (subst nn_integral_cmult) auto
2.159 +  also note emeasure_cball_aux_integral
2.160 +  also have "ennreal (unit_ball_vol (real (card A))) * (ennreal (r ^ Suc (card A)) *
2.161 +                 ennreal (Beta (1/2) (card A / 2 + 1))) =
2.162 +               ennreal (unit_ball_vol (card A) * Beta (1/2) (card A / 2 + 1) * r ^ Suc (card A))"
2.163 +    using \<open>r > 0\<close> by (simp add: ennreal_mult' [symmetric] mult_ac)
2.164 +  also have "unit_ball_vol (card A) * Beta (1/2) (card A / 2 + 1) = unit_ball_vol (Suc (card A))"
2.165 +    by (auto simp: unit_ball_vol_def Beta_def Gamma_eq_zero_iff field_simps
2.166 +          Gamma_one_half_real powr_half_sqrt [symmetric] powr_add [symmetric])
2.167 +  also have "Suc (card A) = card (insert i A)" using insert.hyps by simp
2.168 +  finally show ?case .
2.169 +qed
2.170 +
2.171 +
2.172 +text \<open>
2.173 +  We now get the main theorem very easily by just applying the above lemma.
2.174 +\<close>
2.175 +context
2.176 +  fixes c :: "'a :: euclidean_space" and r :: real
2.177 +  assumes r: "r \<ge> 0"
2.178 +begin
2.179 +
2.180 +theorem emeasure_cball:
2.181 +  "emeasure lborel (cball c r) = ennreal (unit_ball_vol (DIM('a)) * r ^ DIM('a))"
2.182 +proof (cases "r = 0")
2.183 +  case False
2.184 +  with r have r: "r > 0" by simp
2.185 +  have "(lborel :: 'a measure) =
2.186 +          distr (Pi\<^sub>M Basis (\<lambda>_. lborel)) borel (\<lambda>f. \<Sum>b\<in>Basis. f b *\<^sub>R b)"
2.187 +    by (rule lborel_eq)
2.188 +  also have "emeasure \<dots> (cball 0 r) =
2.189 +               emeasure (Pi\<^sub>M Basis (\<lambda>_. lborel))
2.190 +               ({y. dist 0 (\<Sum>b\<in>Basis. y b *\<^sub>R b :: 'a) \<le> r} \<inter> space (Pi\<^sub>M Basis (\<lambda>_. lborel)))"
2.191 +    by (subst emeasure_distr) (auto simp: cball_def)
2.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}"
2.193 +    by (subst euclidean_dist_l2) (auto simp: L2_set_def)
2.194 +  also have "emeasure (Pi\<^sub>M Basis (\<lambda>_. lborel)) (\<dots> \<inter> space (Pi\<^sub>M Basis (\<lambda>_. lborel))) =
2.195 +               ennreal (unit_ball_vol (real DIM('a)) * r ^ DIM('a))"
2.196 +    using r by (subst emeasure_cball_aux) simp_all
2.197 +  also have "emeasure lborel (cball 0 r :: 'a set) =
2.198 +               emeasure (distr lborel borel (\<lambda>x. c + x)) (cball c r)"
2.199 +    by (subst emeasure_distr) (auto simp: cball_def dist_norm norm_minus_commute)
2.200 +  also have "distr lborel borel (\<lambda>x. c + x) = lborel"
2.201 +    using lborel_affine[of 1 c] by (simp add: density_1)
2.202 +  finally show ?thesis .
2.203 +qed auto
2.204 +
2.205 +corollary content_cball:
2.206 +  "content (cball c r) = unit_ball_vol (DIM('a)) * r ^ DIM('a)"
2.207 +  by (simp add: measure_def emeasure_cball r)
2.208 +
2.209 +corollary emeasure_ball:
2.210 +  "emeasure lborel (ball c r) = ennreal (unit_ball_vol (DIM('a)) * r ^ DIM('a))"
2.211 +proof -
2.212 +  from negligible_sphere[of c r] have "sphere c r \<in> null_sets lborel"
2.213 +    by (auto simp: null_sets_completion_iff negligible_iff_null_sets negligible_convex_frontier)
2.214 +  hence "emeasure lborel (ball c r \<union> sphere c r :: 'a set) = emeasure lborel (ball c r :: 'a set)"
2.215 +    by (intro emeasure_Un_null_set) auto
2.216 +  also have "ball c r \<union> sphere c r = (cball c r :: 'a set)" by auto
2.217 +  also have "emeasure lborel \<dots> = ennreal (unit_ball_vol (real DIM('a)) * r ^ DIM('a))"
2.218 +    by (rule emeasure_cball)
2.219 +  finally show ?thesis ..
2.220 +qed
2.221 +
2.222 +corollary content_ball:
2.223 +  "content (ball c r) = unit_ball_vol (DIM('a)) * r ^ DIM('a)"
2.224 +  by (simp add: measure_def r emeasure_ball)
2.225 +
2.226 +end
2.227 +
2.228 +
2.229 +text \<open>
2.230 +  Lastly, we now prove some nicer explicit formulas for the volume of the unit balls in
2.231 +  the cases of even and odd integer dimensions.
2.232 +\<close>
2.233 +lemma unit_ball_vol_even:
2.234 +  "unit_ball_vol (real (2 * n)) = pi ^ n / fact n"
2.235 +  by (simp add: unit_ball_vol_def add_ac powr_realpow Gamma_fact)
2.236 +
2.237 +lemma unit_ball_vol_odd':
2.238 +        "unit_ball_vol (real (2 * n + 1)) = pi ^ n / pochhammer (1 / 2) (Suc n)"
2.239 +  and unit_ball_vol_odd:
2.240 +        "unit_ball_vol (real (2 * n + 1)) =
2.241 +           (2 ^ (2 * Suc n) * fact (Suc n)) / fact (2 * Suc n) * pi ^ n"
2.242 +proof -
2.243 +  have "unit_ball_vol (real (2 * n + 1)) =
2.244 +          pi powr (real n + 1 / 2) / Gamma (1 / 2 + real (Suc n))"
2.245 +    by (simp add: unit_ball_vol_def field_simps)
2.246 +  also have "pochhammer (1 / 2) (Suc n) = Gamma (1 / 2 + real (Suc n)) / Gamma (1 / 2)"
2.247 +    by (intro pochhammer_Gamma) auto
2.248 +  hence "Gamma (1 / 2 + real (Suc n)) = sqrt pi * pochhammer (1 / 2) (Suc n)"
2.249 +    by (simp add: Gamma_one_half_real)
2.250 +  also have "pi powr (real n + 1 / 2) / \<dots> = pi ^ n / pochhammer (1 / 2) (Suc n)"
2.251 +    by (simp add: powr_add powr_half_sqrt powr_realpow)
2.252 +  finally show "unit_ball_vol (real (2 * n + 1)) = \<dots>" .
2.253 +  also have "pochhammer (1 / 2 :: real) (Suc n) =
2.254 +               fact (2 * Suc n) / (2 ^ (2 * Suc n) * fact (Suc n))"
2.255 +    using fact_double[of "Suc n", where ?'a = real] by (simp add: divide_simps mult_ac)
2.256 +  also have "pi ^n / \<dots> = (2 ^ (2 * Suc n) * fact (Suc n)) / fact (2 * Suc n) * pi ^ n"
2.257 +    by simp
2.258 +  finally show "unit_ball_vol (real (2 * n + 1)) = \<dots>" .
2.259 +qed
2.260 +
2.261 +lemma unit_ball_vol_numeral:
2.262 +  "unit_ball_vol (numeral (Num.Bit0 n)) = pi ^ numeral n / fact (numeral n)" (is ?th1)
2.263 +  "unit_ball_vol (numeral (Num.Bit1 n)) = 2 ^ (2 * Suc (numeral n)) * fact (Suc (numeral n)) /
2.264 +    fact (2 * Suc (numeral n)) * pi ^ numeral n" (is ?th2)
2.265 +proof -
2.266 +  have "numeral (Num.Bit0 n) = (2 * numeral n :: nat)"
2.267 +    by (simp only: numeral_Bit0 mult_2 ring_distribs)
2.268 +  also have "unit_ball_vol \<dots> = pi ^ numeral n / fact (numeral n)"
2.269 +    by (rule unit_ball_vol_even)
2.270 +  finally show ?th1 by simp
2.271 +next
2.272 +  have "numeral (Num.Bit1 n) = (2 * numeral n + 1 :: nat)"
2.273 +    by (simp only: numeral_Bit1 mult_2)
2.274 +  also have "unit_ball_vol \<dots> = 2 ^ (2 * Suc (numeral n)) * fact (Suc (numeral n)) /
2.275 +                                  fact (2 * Suc (numeral n)) * pi ^ numeral n"
2.276 +    by (rule unit_ball_vol_odd)
2.277 +  finally show ?th2 by simp
2.278 +qed
2.279 +
2.280 +lemmas eval_unit_ball_vol = unit_ball_vol_numeral fact_numeral
2.281 +
2.282 +
2.283 +text \<open>
2.284 +  Just for fun, we compute the volume of unit balls for a few dimensions.
2.285 +\<close>
2.286 +lemma unit_ball_vol_0 [simp]: "unit_ball_vol 0 = 1"
2.287 +  using unit_ball_vol_even[of 0] by simp
2.288 +
2.289 +lemma unit_ball_vol_1 [simp]: "unit_ball_vol 1 = 2"
2.290 +  using unit_ball_vol_odd[of 0] by simp
2.291 +
2.292 +corollary unit_ball_vol_2: "unit_ball_vol 2 = pi"
2.293 +      and unit_ball_vol_3: "unit_ball_vol 3 = 4 / 3 * pi"
2.294 +      and unit_ball_vol_4: "unit_ball_vol 4 = pi\<^sup>2 / 2"
2.295 +      and unit_ball_vol_5: "unit_ball_vol 5 = 8 / 15 * pi\<^sup>2"
2.296 +  by (simp_all add: eval_unit_ball_vol)
2.297 +
2.298 +corollary circle_area: "r \<ge> 0 \<Longrightarrow> content (ball c r :: (real ^ 2) set) = r ^ 2 * pi"
2.299 +  by (simp add: content_ball unit_ball_vol_2)
2.300 +
2.301 +corollary sphere_volume: "r \<ge> 0 \<Longrightarrow> content (ball c r :: (real ^ 3) set) = 4 / 3 * r ^ 3 * pi"
2.302 +  by (simp add: content_ball unit_ball_vol_3)
2.303 +
2.304 +end
```
```     3.1 --- a/src/HOL/Analysis/Borel_Space.thy	Sun Dec 24 14:46:26 2017 +0100
3.2 +++ b/src/HOL/Analysis/Borel_Space.thy	Sun Dec 24 14:28:10 2017 +0100
3.3 @@ -1515,6 +1515,11 @@
3.4    apply auto
3.5    done
3.6
3.7 +lemma powr_real_measurable [measurable]:
3.8 +  assumes "f \<in> measurable M borel" "g \<in> measurable M borel"
3.9 +  shows   "(\<lambda>x. f x powr g x :: real) \<in> measurable M borel"
3.10 +  using assms by (simp_all add: powr_def)
3.11 +
3.12  lemma measurable_of_bool[measurable]: "of_bool \<in> count_space UNIV \<rightarrow>\<^sub>M borel"
3.13    by simp
3.14
```
```     4.1 --- a/src/HOL/Analysis/Complex_Transcendental.thy	Sun Dec 24 14:46:26 2017 +0100
4.2 +++ b/src/HOL/Analysis/Complex_Transcendental.thy	Sun Dec 24 14:28:10 2017 +0100
4.3 @@ -1489,6 +1489,27 @@
4.4    finally show ?thesis .
4.5  qed
4.6
4.7 +lemma Ln_measurable [measurable]: "Ln \<in> measurable borel borel"
4.8 +proof -
4.9 +  have *: "Ln (-of_real x) = of_real (ln x) + \<i> * pi" if "x > 0" for x
4.10 +    using that by (subst Ln_minus) (auto simp: Ln_of_real)
4.11 +  have **: "Ln (of_real x) = of_real (ln (-x)) + \<i> * pi" if "x < 0" for x
4.12 +    using *[of "-x"] that by simp
4.13 +  have cont: "set_borel_measurable borel (- \<real>\<^sub>\<le>\<^sub>0) Ln"
4.14 +    by (intro borel_measurable_continuous_on_indicator continuous_intros) auto
4.15 +  have "(\<lambda>x. if x \<in> \<real>\<^sub>\<le>\<^sub>0 then ln (-Re x) + \<i> * pi else indicator (-\<real>\<^sub>\<le>\<^sub>0) x *\<^sub>R Ln x) \<in> borel \<rightarrow>\<^sub>M borel"
4.16 +    (is "?f \<in> _") by (rule measurable_If_set[OF _ cont]) auto
4.17 +  hence "(\<lambda>x. if x = 0 then Ln 0 else ?f x) \<in> borel \<rightarrow>\<^sub>M borel" by measurable
4.18 +  also have "(\<lambda>x. if x = 0 then Ln 0 else ?f x) = Ln"
4.19 +    by (auto simp: fun_eq_iff ** nonpos_Reals_def)
4.20 +  finally show ?thesis .
4.21 +qed
4.22 +
4.23 +lemma powr_complex_measurable [measurable]:
4.24 +  assumes [measurable]: "f \<in> measurable M borel" "g \<in> measurable M borel"
4.25 +  shows   "(\<lambda>x. f x powr g x :: complex) \<in> measurable M borel"
4.26 +  using assms by (simp add: powr_def)
4.27 +
4.28
4.29  subsection\<open>Relation between Ln and Arg, and hence continuity of Arg\<close>
4.30
```
```     5.1 --- a/src/HOL/Analysis/Gamma_Function.thy	Sun Dec 24 14:46:26 2017 +0100
5.2 +++ b/src/HOL/Analysis/Gamma_Function.thy	Sun Dec 24 14:28:10 2017 +0100
5.3 @@ -1653,7 +1653,10 @@
5.4    using Gamma_fact[of "n - 1", where 'a = real]
5.5    by (simp add: ln_Gamma_real_pos of_nat_diff Ln_of_real [symmetric])
5.6
5.7 -lemma Gamma_real_pos: "x > (0::real) \<Longrightarrow> Gamma x > 0"
5.8 +lemma Gamma_real_pos [simp, intro]: "x > (0::real) \<Longrightarrow> Gamma x > 0"
5.9 +  by (simp add: Gamma_real_pos_exp)
5.10 +
5.11 +lemma Gamma_real_nonneg [simp, intro]: "x > (0::real) \<Longrightarrow> Gamma x \<ge> 0"
5.12    by (simp add: Gamma_real_pos_exp)
5.13
5.14  lemma has_field_derivative_ln_Gamma_real [derivative_intros]:
5.15 @@ -2985,6 +2988,170 @@
5.16    finally show ?thesis .
5.17  qed
5.18
5.19 +lemma Gamma_conv_nn_integral_real:
5.20 +  assumes "s > (0::real)"
5.21 +  shows   "Gamma s = nn_integral lborel (\<lambda>t. ennreal (indicator {0..} t * t powr (s - 1) / exp t))"
5.22 +  using nn_integral_has_integral_lebesgue[OF _ Gamma_integral_real[OF assms]] by simp
5.23 +
5.24 +lemma integrable_Beta:
5.25 +  assumes "a > 0" "b > (0::real)"
5.26 +  shows   "set_integrable lborel {0..1} (\<lambda>t. t powr (a - 1) * (1 - t) powr (b - 1))"
5.27 +proof -
5.28 +  define C where "C = max 1 ((1/2) powr (b - 1))"
5.29 +  define D where "D = max 1 ((1/2) powr (a - 1))"
5.30 +  have C: "(1 - x) powr (b - 1) \<le> C" if "x \<in> {0..1/2}" for x
5.31 +  proof (cases "b < 1")
5.32 +    case False
5.33 +    with that have "(1 - x) powr (b - 1) \<le> (1 powr (b - 1))" by (intro powr_mono2) auto
5.34 +    thus ?thesis by (auto simp: C_def)
5.35 +  qed (insert that, auto simp: max.coboundedI1 max.coboundedI2 powr_mono2' powr_mono2 C_def)
5.36 +  have D: "x powr (a - 1) \<le> D" if "x \<in> {1/2..1}" for x
5.37 +  proof (cases "a < 1")
5.38 +    case False
5.39 +    with that have "x powr (a - 1) \<le> (1 powr (a - 1))" by (intro powr_mono2) auto
5.40 +    thus ?thesis by (auto simp: D_def)
5.41 +  next
5.42 +    case True
5.43 +  qed (insert that, auto simp: max.coboundedI1 max.coboundedI2 powr_mono2' powr_mono2 D_def)
5.44 +  have [simp]: "C \<ge> 0" "D \<ge> 0" by (simp_all add: C_def D_def)
5.45 +
5.46 +  have I1: "set_integrable lborel {0..1 / 2} (\<lambda>t. t powr (a - 1) * (1 - t) powr (b - 1))"
5.47 +  proof (rule Bochner_Integration.integrable_bound[OF _ _ AE_I2])
5.48 +    have "(\<lambda>t. t powr (a - 1)) integrable_on {0..1 / 2}"
5.49 +      by (rule integrable_on_powr_from_0) (use assms in auto)
5.50 +    hence "(\<lambda>t. t powr (a - 1)) absolutely_integrable_on {0..1 / 2}"
5.51 +      by (subst absolutely_integrable_on_iff_nonneg) auto
5.52 +    from integrable_mult_right[OF this, of C]
5.53 +      show "set_integrable lborel {0..1 / 2} (\<lambda>t. C * t powr (a - 1))"
5.54 +      by (subst (asm) integrable_completion) (auto simp: mult_ac)
5.55 +  next
5.56 +    fix x :: real
5.57 +    have "x powr (a - 1) * (1 - x) powr (b - 1) \<le> x powr (a - 1) * C" if "x \<in> {0..1/2}"
5.58 +      using that by (intro mult_left_mono powr_mono2 C) auto
5.59 +    thus "norm (indicator {0..1/2} x *\<^sub>R (x powr (a - 1) * (1 - x) powr (b - 1))) \<le>
5.60 +            norm (indicator {0..1/2} x *\<^sub>R (C * x powr (a - 1)))"
5.61 +      by (auto simp: indicator_def abs_mult mult_ac)
5.62 +  qed (auto intro!: AE_I2 simp: indicator_def)
5.63 +
5.64 +  have I2: "set_integrable lborel {1 / 2..1} (\<lambda>t. t powr (a - 1) * (1 - t) powr (b - 1))"
5.65 +  proof (rule Bochner_Integration.integrable_bound[OF _ _ AE_I2])
5.66 +    have "(\<lambda>t. t powr (b - 1)) integrable_on {0..1/2}"
5.67 +      by (rule integrable_on_powr_from_0) (use assms in auto)
5.68 +    hence "(\<lambda>t. t powr (b - 1)) integrable_on (cbox 0 (1/2))" by simp
5.69 +    from integrable_affinity[OF this, of "-1" 1]
5.70 +      have "(\<lambda>t. (1 - t) powr (b - 1)) integrable_on {1/2..1}" by simp
5.71 +    hence "(\<lambda>t. (1 - t) powr (b - 1)) absolutely_integrable_on {1/2..1}"
5.72 +      by (subst absolutely_integrable_on_iff_nonneg) auto
5.73 +    from integrable_mult_right[OF this, of D]
5.74 +      show "set_integrable lborel {1 / 2..1} (\<lambda>t. D * (1 - t) powr (b - 1))"
5.75 +      by (subst (asm) integrable_completion) (auto simp: mult_ac)
5.76 +  next
5.77 +    fix x :: real
5.78 +    have "x powr (a - 1) * (1 - x) powr (b - 1) \<le> D * (1 - x) powr (b - 1)" if "x \<in> {1/2..1}"
5.79 +      using that by (intro mult_right_mono powr_mono2 D) auto
5.80 +    thus "norm (indicator {1/2..1} x *\<^sub>R (x powr (a - 1) * (1 - x) powr (b - 1))) \<le>
5.81 +            norm (indicator {1/2..1} x *\<^sub>R (D * (1 - x) powr (b - 1)))"
5.82 +      by (auto simp: indicator_def abs_mult mult_ac)
5.83 +  qed (auto intro!: AE_I2 simp: indicator_def)
5.84 +
5.85 +  have "set_integrable lborel ({0..1/2} \<union> {1/2..1}) (\<lambda>t. t powr (a - 1) * (1 - t) powr (b - 1))"
5.86 +    by (intro set_integrable_Un I1 I2) auto
5.87 +  also have "{0..1/2} \<union> {1/2..1} = {0..(1::real)}" by auto
5.88 +  finally show ?thesis .
5.89 +qed
5.90 +
5.91 +lemma integrable_Beta':
5.92 +  assumes "a > 0" "b > (0::real)"
5.93 +  shows   "(\<lambda>t. t powr (a - 1) * (1 - t) powr (b - 1)) integrable_on {0..1}"
5.94 +  using integrable_Beta[OF assms] by (rule set_borel_integral_eq_integral)
5.95 +
5.96 +lemma has_integral_Beta_real:
5.97 +  assumes a: "a > 0" and b: "b > (0 :: real)"
5.98 +  shows "((\<lambda>t. t powr (a - 1) * (1 - t) powr (b - 1)) has_integral Beta a b) {0..1}"
5.99 +proof -
5.100 +  define B where "B = integral {0..1} (\<lambda>x. x powr (a - 1) * (1 - x) powr (b - 1))"
5.101 +  have [simp]: "B \<ge> 0" unfolding B_def using a b
5.102 +    by (intro integral_nonneg integrable_Beta') auto
5.103 +  from a b have "ennreal (Gamma a * Gamma b) =
5.104 +    (\<integral>\<^sup>+ t. ennreal (indicator {0..} t * t powr (a - 1) / exp t) \<partial>lborel) *
5.105 +    (\<integral>\<^sup>+ t. ennreal (indicator {0..} t * t powr (b - 1) / exp t) \<partial>lborel)"
5.106 +    by (subst ennreal_mult') (simp_all add: Gamma_conv_nn_integral_real)
5.107 +  also have "\<dots> = (\<integral>\<^sup>+t. \<integral>\<^sup>+u. ennreal (indicator {0..} t * t powr (a - 1) / exp t) *
5.108 +                            ennreal (indicator {0..} u * u powr (b - 1) / exp u) \<partial>lborel \<partial>lborel)"
5.109 +    by (simp add: nn_integral_cmult nn_integral_multc)
5.110 +  also have "\<dots> = (\<integral>\<^sup>+t. \<integral>\<^sup>+u. ennreal (indicator ({0..}\<times>{0..}) (t,u) * t powr (a - 1) * u powr (b - 1)
5.111 +                            / exp (t + u)) \<partial>lborel \<partial>lborel)"
5.112 +    by (intro nn_integral_cong)
5.113 +       (auto simp: indicator_def divide_ennreal ennreal_mult' [symmetric] exp_add)
5.114 +  also have "\<dots> = (\<integral>\<^sup>+t. \<integral>\<^sup>+u. ennreal (indicator ({0..}\<times>{t..}) (t,u) * t powr (a - 1) *
5.115 +                              (u - t) powr (b - 1) / exp u) \<partial>lborel \<partial>lborel)"
5.116 +  proof (rule nn_integral_cong, goal_cases)
5.117 +    case (1 t)
5.118 +    have "(\<integral>\<^sup>+u. ennreal (indicator ({0..}\<times>{0..}) (t,u) * t powr (a - 1) *
5.119 +                              u powr (b - 1) / exp (t + u)) \<partial>distr lborel borel (op + (-t))) =
5.120 +               (\<integral>\<^sup>+u. ennreal (indicator ({0..}\<times>{t..}) (t,u) * t powr (a - 1) *
5.121 +                              (u - t) powr (b - 1) / exp u) \<partial>lborel)"
5.122 +      by (subst nn_integral_distr) (auto intro!: nn_integral_cong simp: indicator_def)
5.123 +    thus ?case by (subst (asm) lborel_distr_plus)
5.124 +  qed
5.125 +  also have "\<dots> = (\<integral>\<^sup>+u. \<integral>\<^sup>+t. ennreal (indicator ({0..}\<times>{t..}) (t,u) * t powr (a - 1) *
5.126 +                              (u - t) powr (b - 1) / exp u) \<partial>lborel \<partial>lborel)"
5.127 +    by (subst lborel_pair.Fubini')
5.128 +       (auto simp: case_prod_unfold indicator_def cong: measurable_cong_sets)
5.129 +  also have "\<dots> = (\<integral>\<^sup>+u. \<integral>\<^sup>+t. ennreal (indicator {0..u} t * t powr (a - 1) * (u - t) powr (b - 1)) *
5.130 +                              ennreal (indicator {0..} u / exp u) \<partial>lborel \<partial>lborel)"
5.131 +    by (intro nn_integral_cong) (auto simp: indicator_def ennreal_mult' [symmetric])
5.132 +  also have "\<dots> = (\<integral>\<^sup>+u. (\<integral>\<^sup>+t. ennreal (indicator {0..u} t * t powr (a - 1) * (u - t) powr (b - 1))
5.133 +                          \<partial>lborel) * ennreal (indicator {0..} u / exp u) \<partial>lborel)"
5.134 +    by (subst nn_integral_multc [symmetric]) auto
5.135 +  also have "\<dots> = (\<integral>\<^sup>+u. (\<integral>\<^sup>+t. ennreal (indicator {0..u} t * t powr (a - 1) * (u - t) powr (b - 1))
5.136 +                          \<partial>lborel) * ennreal (indicator {0<..} u / exp u) \<partial>lborel)"
5.137 +    by (intro nn_integral_cong_AE eventually_mono[OF AE_lborel_singleton[of 0]])
5.138 +       (auto simp: indicator_def)
5.139 +  also have "\<dots> = (\<integral>\<^sup>+u. ennreal B * ennreal (indicator {0..} u / exp u * u powr (a + b - 1)) \<partial>lborel)"
5.140 +  proof (intro nn_integral_cong, goal_cases)
5.141 +    case (1 u)
5.142 +    show ?case
5.143 +    proof (cases "u > 0")
5.144 +      case True
5.145 +      have "(\<integral>\<^sup>+t. ennreal (indicator {0..u} t * t powr (a - 1) * (u - t) powr (b - 1)) \<partial>lborel) =
5.146 +              (\<integral>\<^sup>+t. ennreal (indicator {0..1} t * (u * t) powr (a - 1) * (u - u * t) powr (b - 1))
5.147 +                \<partial>distr lborel borel (op * (1 / u)))" (is "_ = nn_integral _ ?f")
5.148 +        using True
5.149 +        by (subst nn_integral_distr) (auto simp: indicator_def field_simps intro!: nn_integral_cong)
5.150 +      also have "distr lborel borel (op * (1 / u)) = density lborel (\<lambda>_. u)"
5.151 +        using \<open>u > 0\<close> by (subst lborel_distr_mult) auto
5.152 +      also have "nn_integral \<dots> ?f = (\<integral>\<^sup>+x. ennreal (indicator {0..1} x * (u * (u * x) powr (a - 1) *
5.153 +                                              (u * (1 - x)) powr (b - 1))) \<partial>lborel)" using \<open>u > 0\<close>
5.154 +        by (subst nn_integral_density) (auto simp: ennreal_mult' [symmetric] algebra_simps)
5.155 +      also have "\<dots> = (\<integral>\<^sup>+x. ennreal (u powr (a + b - 1)) *
5.156 +                            ennreal (indicator {0..1} x * x powr (a - 1) *
5.157 +                                       (1 - x) powr (b - 1)) \<partial>lborel)" using \<open>u > 0\<close> a b
5.158 +        by (intro nn_integral_cong)
5.159 +           (auto simp: indicator_def powr_mult powr_add powr_diff mult_ac ennreal_mult' [symmetric])
5.160 +      also have "\<dots> = ennreal (u powr (a + b - 1)) *
5.161 +                        (\<integral>\<^sup>+x. ennreal (indicator {0..1} x * x powr (a - 1) *
5.162 +                                         (1 - x) powr (b - 1)) \<partial>lborel)"
5.163 +        by (subst nn_integral_cmult) auto
5.164 +      also have "((\<lambda>x. x powr (a - 1) * (1 - x) powr (b - 1)) has_integral
5.165 +                   integral {0..1} (\<lambda>x. x powr (a - 1) * (1 - x) powr (b - 1))) {0..1}"
5.166 +        using a b by (intro integrable_integral integrable_Beta')
5.167 +      from nn_integral_has_integral_lebesgue[OF _ this] a b
5.168 +        have "(\<integral>\<^sup>+x. ennreal (indicator {0..1} x * x powr (a - 1) *
5.169 +                         (1 - x) powr (b - 1)) \<partial>lborel) = B" by (simp add: mult_ac B_def)
5.170 +      finally show ?thesis using \<open>u > 0\<close> by (simp add: ennreal_mult' [symmetric] mult_ac)
5.171 +    qed auto
5.172 +  qed
5.173 +  also have "\<dots> = ennreal B * ennreal (Gamma (a + b))"
5.174 +    using a b by (subst nn_integral_cmult) (auto simp: Gamma_conv_nn_integral_real)
5.175 +  also have "\<dots> = ennreal (B * Gamma (a + b))"
5.176 +    by (subst (1 2) mult.commute, intro ennreal_mult' [symmetric]) (use a b in auto)
5.177 +  finally have "B = Beta a b" using a b Gamma_real_pos[of "a + b"]
5.178 +    by (subst (asm) ennreal_inj) (auto simp: field_simps Beta_def Gamma_eq_zero_iff)
5.179 +  moreover have "(\<lambda>t. t powr (a - 1) * (1 - t) powr (b - 1)) integrable_on {0..1}"
5.180 +    by (intro integrable_Beta' a b)
5.181 +  ultimately show ?thesis by (simp add: has_integral_iff B_def)
5.182 +qed
5.183
5.184
5.185  subsection \<open>The Weierstraß product formula for the sine\<close>
```
```     6.1 --- a/src/HOL/Analysis/ex/Circle_Area.thy	Sun Dec 24 14:46:26 2017 +0100
6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
6.3 @@ -1,183 +0,0 @@
6.4 -(*  Title:      HOL/Analysis/ex/Circle_Area.thy
6.5 -    Author:     Manuel Eberl, TU Muenchen
6.6 -
6.7 -A proof that the area of a circle with radius R is R\<^sup>2\<pi>.
6.8 -*)
6.9 -
6.10 -section \<open>The area of a circle\<close>
6.11 -
6.12 -theory Circle_Area
6.13 -imports Complex_Main "HOL-Analysis.Interval_Integral"
6.14 -begin
6.15 -
6.16 -lemma plus_emeasure':
6.17 -  assumes "A \<in> sets M" "B \<in> sets M" "A \<inter> B \<in> null_sets M"
6.18 -  shows "emeasure M A + emeasure M B = emeasure M (A \<union> B)"
6.19 -proof-
6.20 -  let ?C = "A \<inter> B"
6.21 -  have "A \<union> B = A \<union> (B - ?C)" by blast
6.22 -  with assms have "emeasure M (A \<union> B) = emeasure M A + emeasure M (B - ?C)"
6.23 -    by (subst plus_emeasure) auto
6.24 -  also from assms(3,2) have "emeasure M (B - ?C) = emeasure M B"
6.25 -    by (rule emeasure_Diff_null_set)
6.26 -  finally show ?thesis ..
6.27 -qed
6.28 -
6.29 -lemma real_sqrt_square:
6.30 -  "x \<ge> 0 \<Longrightarrow> sqrt (x^2) = (x::real)" by simp
6.31 -
6.32 -lemma unit_circle_area_aux:
6.33 -  "LBINT x=-1..1. 2 * sqrt (1 - x^2) = pi"
6.34 -proof-
6.35 -  have "LBINT x=-1..1. 2 * sqrt (1 - x^2) =
6.36 -            LBINT x=ereal (sin (-pi/2))..ereal (sin (pi/2)). 2 * sqrt (1 - x^2)"
6.37 -    by (simp_all add: one_ereal_def)
6.38 -  also have "... = LBINT x=-pi/2..pi/2. cos x *\<^sub>R (2 * sqrt (1 - (sin x)\<^sup>2))"
6.39 -    by (rule interval_integral_substitution_finite[symmetric])
6.40 -       (auto intro: DERIV_subset[OF DERIV_sin] intro!: continuous_intros)
6.41 -  also have "... = LBINT x=-pi/2..pi/2. 2 * cos x * sqrt ((cos x)^2)"
6.42 -    by (simp add: cos_squared_eq field_simps)
6.43 -  also {
6.44 -    fix x assume "x \<in> {-pi/2<..<pi/2}"
6.45 -    hence "cos x \<ge> 0" by (intro cos_ge_zero) simp_all
6.46 -    hence "sqrt ((cos x)^2) = cos x" by simp
6.47 -  } note A = this
6.48 -  have "LBINT x=-pi/2..pi/2. 2 * cos x * sqrt ((cos x)^2) = LBINT x=-pi/2..pi/2. 2 * (cos x)^2"
6.49 -    by (intro interval_integral_cong, subst A) (simp_all add: min_def max_def power2_eq_square)
6.50 -  also let ?F = "\<lambda>x. x + sin x * cos x"
6.51 -   {
6.52 -    fix x A
6.53 -    have "(?F has_real_derivative 1 - (sin x)^2 + (cos x)^2) (at x)"
6.54 -      by (auto simp: power2_eq_square intro!: derivative_eq_intros)
6.55 -    also have "1 - (sin x)^2 + (cos x)^2 = 2 * (cos x)^2" by (simp add: cos_squared_eq)
6.56 -    finally have "(?F has_real_derivative 2 * (cos x)^2) (at x within A)"
6.57 -      by (rule DERIV_subset) simp
6.58 -  }
6.59 -  hence "LBINT x=-pi/2..pi/2. 2 * (cos x)^2 = ?F (pi/2) - ?F (-pi/2)"
6.60 -    by (intro interval_integral_FTC_finite)
6.61 -       (auto simp: has_field_derivative_iff_has_vector_derivative intro!: continuous_intros)
6.62 -  also have "... = pi" by simp
6.63 -  finally show ?thesis .
6.64 -qed
6.65 -
6.66 -lemma unit_circle_area:
6.67 -  "emeasure lborel {z::real\<times>real. norm z \<le> 1} = pi" (is "emeasure _ ?A = _")
6.68 -proof-
6.69 -  let ?A1 = "{(x,y)\<in>?A. y \<ge> 0}" and ?A2 = "{(x,y)\<in>?A. y \<le> 0}"
6.70 -  have [measurable]: "(\<lambda>x. snd (x :: real \<times> real)) \<in> measurable borel borel"
6.71 -    by (simp add: borel_prod[symmetric])
6.72 -
6.73 -  have "?A1 = ?A \<inter> {x\<in>space lborel. snd x \<ge> 0}" by auto
6.74 -  also have "?A \<inter> {x\<in>space lborel. snd x \<ge> 0} \<in> sets borel"
6.75 -    by (intro sets.Int pred_Collect_borel) simp_all
6.76 -  finally have A1_in_sets: "?A1 \<in> sets lborel" by (subst sets_lborel)
6.77 -
6.78 -  have "?A2 = ?A \<inter> {x\<in>space lborel. snd x \<le> 0}" by auto
6.79 -  also have "... \<in> sets borel"
6.80 -    by (intro sets.Int pred_Collect_borel) simp_all
6.81 -  finally have A2_in_sets: "?A2 \<in> sets lborel" by (subst sets_lborel)
6.82 -
6.83 -  have A12: "?A = ?A1 \<union> ?A2" by auto
6.84 -  have sq_le_1_iff: "\<And>x. x\<^sup>2 \<le> 1 \<longleftrightarrow> abs (x::real) \<le> 1"
6.85 -    by (simp add: abs_square_le_1)
6.86 -  have "?A1 \<inter> ?A2 = {x. abs x \<le> 1} \<times> {0}" by (auto simp: norm_Pair field_simps sq_le_1_iff)
6.87 -  also have "... \<in> null_sets lborel"
6.88 -    by (subst lborel_prod[symmetric]) (auto simp: lborel.emeasure_pair_measure_Times)
6.89 -  finally have "emeasure lborel ?A = emeasure lborel ?A1 + emeasure lborel ?A2"
6.90 -    by (subst A12, rule plus_emeasure'[OF A1_in_sets A2_in_sets, symmetric])
6.91 -
6.92 -  also have "emeasure lborel ?A1 = \<integral>\<^sup>+x. \<integral>\<^sup>+y. indicator ?A1 (x,y) \<partial>lborel \<partial>lborel"
6.93 -    by (subst lborel_prod[symmetric], subst lborel.emeasure_pair_measure)
6.94 -       (simp_all only: lborel_prod A1_in_sets)
6.95 -  also have "emeasure lborel ?A2 = \<integral>\<^sup>+x. \<integral>\<^sup>+y. indicator ?A2 (x,y) \<partial>lborel \<partial>lborel"
6.96 -    by (subst lborel_prod[symmetric], subst lborel.emeasure_pair_measure)
6.97 -       (simp_all only: lborel_prod A2_in_sets)
6.98 -  also have "distr lborel lborel uminus = (lborel :: real measure)"
6.99 -    by (subst (3) lborel_real_affine[of "-1" 0])
6.100 -       (simp_all add: one_ereal_def[symmetric] density_1 cong: distr_cong)
6.101 -  hence "(\<integral>\<^sup>+x. \<integral>\<^sup>+y. indicator ?A2 (x,y) \<partial>lborel \<partial>lborel) =
6.102 -             \<integral>\<^sup>+x. \<integral>\<^sup>+y. indicator ?A2 (x,y) \<partial>distr lborel lborel uminus \<partial>lborel" by simp
6.103 -  also have "... = \<integral>\<^sup>+x. \<integral>\<^sup>+y. indicator ?A2 (x,-y) \<partial>lborel \<partial>lborel"
6.104 -    apply (intro nn_integral_cong nn_integral_distr, simp)
6.105 -    apply (intro measurable_compose[OF _ borel_measurable_indicator[OF A2_in_sets]], simp)
6.106 -    done
6.107 -  also have "... = \<integral>\<^sup>+x. \<integral>\<^sup>+y. indicator ?A1 (x,y) \<partial>lborel \<partial>lborel"
6.108 -    by (intro nn_integral_cong) (auto split: split_indicator simp: norm_Pair)
6.109 -  also have "... + ... = (1+1) * ..." by (subst ring_distribs) simp_all
6.110 -  also have "... = \<integral>\<^sup>+x. 2 * \<integral>\<^sup>+y. indicator ?A1 (x,y) \<partial>lborel \<partial>lborel"
6.111 -    by (subst nn_integral_cmult) simp_all
6.112 -  also {
6.113 -    fix x y :: real assume "x \<notin> {-1..1}"
6.114 -    hence "abs x > 1" by auto
6.115 -    also have "norm (x,y) \<ge> abs x" by (simp add: norm_Pair)
6.116 -    finally have "(x,y) \<notin> ?A1" by auto
6.117 -  }
6.118 -  hence "... = \<integral>\<^sup>+x. 2 * (\<integral>\<^sup>+y. indicator ?A1 (x,y) \<partial>lborel) * indicator {-1..1} x \<partial>lborel"
6.119 -    by (intro nn_integral_cong) (auto split: split_indicator)
6.120 -  also {
6.121 -    fix x :: real assume "x \<in> {-1..1}"
6.122 -    hence x: "1 - x\<^sup>2 \<ge> 0" by (simp add: field_simps sq_le_1_iff abs_real_def)
6.123 -    have "\<And>y. (y::real) \<ge> 0 \<Longrightarrow> norm (x,y) \<le> 1 \<longleftrightarrow> y \<le> sqrt (1-x\<^sup>2)"
6.124 -      by (subst (5) real_sqrt_square[symmetric], simp, subst real_sqrt_le_iff)
6.125 -         (simp_all add: norm_Pair field_simps)
6.126 -    hence "(\<integral>\<^sup>+y. indicator ?A1 (x,y) \<partial>lborel) = (\<integral>\<^sup>+y. indicator {0..sqrt (1-x\<^sup>2)} y \<partial>lborel)"
6.127 -      by (intro nn_integral_cong) (auto split: split_indicator)
6.128 -    also from x have "... = sqrt (1-x\<^sup>2)" using x by simp
6.129 -    finally have "(\<integral>\<^sup>+y. indicator ?A1 (x,y) \<partial>lborel) = sqrt (1-x\<^sup>2)" .
6.130 -  }
6.131 -  hence "(\<integral>\<^sup>+x. 2 * (\<integral>\<^sup>+y. indicator ?A1 (x,y) \<partial>lborel) * indicator {-1..1} x \<partial>lborel) =
6.132 -            \<integral>\<^sup>+x. 2 * sqrt (1-x\<^sup>2) * indicator {-1..1} x \<partial>lborel"
6.133 -    by (intro nn_integral_cong) (simp split: split_indicator add: ennreal_mult')
6.134 -  also have A: "\<And>x. -1 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> \<not>x^2 > (1::real)"
6.135 -    by (subst not_less, subst sq_le_1_iff) (simp add: abs_real_def)
6.136 -  have "integrable lborel (\<lambda>x. 2 * sqrt (1-x\<^sup>2) * indicator {-1..1::real} x)"
6.137 -    by (intro borel_integrable_atLeastAtMost continuous_intros)
6.138 -  hence "(\<integral>\<^sup>+x. 2 * sqrt (1-x\<^sup>2) * indicator {-1..1} x \<partial>lborel) =
6.139 -             ennreal (\<integral>x. 2 * sqrt (1-x\<^sup>2) * indicator {-1..1} x \<partial>lborel)"
6.140 -    by (intro nn_integral_eq_integral AE_I2)
6.141 -       (auto split: split_indicator simp: field_simps sq_le_1_iff)
6.142 -  also have "(\<integral>x. 2 * sqrt (1-x\<^sup>2) * indicator {-1..1} x \<partial>lborel) =
6.143 -               LBINT x:{-1..1}. 2 * sqrt (1-x\<^sup>2)" by (simp add: field_simps)
6.144 -  also have "... = LBINT x=-1..1. 2 * sqrt (1-x\<^sup>2)"
6.145 -    by (subst interval_integral_Icc[symmetric]) (simp_all add: one_ereal_def)
6.146 -  also have "... = pi" by (rule unit_circle_area_aux)
6.147 -  finally show ?thesis .
6.148 -qed
6.149 -
6.150 -lemma circle_area:
6.151 -  assumes "R \<ge> 0"
6.152 -  shows   "emeasure lborel {z::real\<times>real. norm z \<le> R} = R^2 * pi" (is "emeasure _ ?A = _")
6.153 -proof (cases "R = 0")
6.154 -  assume "R \<noteq> 0"
6.155 -  with assms have R: "R > 0" by simp
6.156 -  let ?A' = "{z::real\<times>real. norm z \<le> 1}"
6.157 -  have "emeasure lborel ?A = \<integral>\<^sup>+x. \<integral>\<^sup>+y. indicator ?A (x,y) \<partial>lborel \<partial>lborel"
6.158 -    by (subst lborel_prod[symmetric], subst lborel.emeasure_pair_measure, subst lborel_prod)
6.159 -       simp_all
6.160 -  also have "... = \<integral>\<^sup>+x. R * \<integral>\<^sup>+y. indicator ?A (x,R*y) \<partial>lborel \<partial>lborel"
6.161 -  proof (rule nn_integral_cong)
6.162 -    fix x from R show "(\<integral>\<^sup>+y. indicator ?A (x,y) \<partial>lborel) = R * \<integral>\<^sup>+y. indicator ?A (x,R*y) \<partial>lborel"
6.163 -      by (subst nn_integral_real_affine[OF _ \<open>R \<noteq> 0\<close>, of _ 0]) simp_all
6.164 -  qed
6.165 -  also have "... = R * \<integral>\<^sup>+x. \<integral>\<^sup>+y. indicator ?A (x,R*y) \<partial>lborel \<partial>lborel"
6.166 -    using R by (intro nn_integral_cmult) simp_all
6.167 -  also from R have "(\<integral>\<^sup>+x. \<integral>\<^sup>+y. indicator ?A (x,R*y) \<partial>lborel \<partial>lborel) =
6.168 -                        R * \<integral>\<^sup>+x. \<integral>\<^sup>+y. indicator ?A (R*x,R*y) \<partial>lborel \<partial>lborel"
6.169 -    by (subst nn_integral_real_affine[OF _ \<open>R \<noteq> 0\<close>, of _ 0]) simp_all
6.170 -  also {
6.171 -    fix x y
6.172 -    have A: "(R*x, R*y) = R *\<^sub>R (x,y)" by simp
6.173 -    from R have "norm (R*x, R*y) = R * norm (x,y)" by (subst A, subst norm_scaleR) simp_all
6.174 -    with R have "(R*x, R*y) \<in> ?A \<longleftrightarrow> (x, y) \<in> ?A'" by (auto simp: field_simps)
6.175 -  }
6.176 -  hence "(\<integral>\<^sup>+x. \<integral>\<^sup>+y. indicator ?A (R*x,R*y) \<partial>lborel \<partial>lborel) =
6.177 -               \<integral>\<^sup>+x. \<integral>\<^sup>+y. indicator ?A' (x,y) \<partial>lborel \<partial>lborel"
6.178 -    by (intro nn_integral_cong) (simp split: split_indicator)
6.179 -  also have "... = emeasure lborel ?A'"
6.180 -    by (subst lborel_prod[symmetric], subst lborel.emeasure_pair_measure, subst lborel_prod)
6.181 -       simp_all
6.182 -  also have "... = pi" by (rule unit_circle_area)
6.183 -  finally show ?thesis using assms by (simp add: power2_eq_square ennreal_mult mult_ac)
6.184 -qed simp
6.185 -
6.186 -end
```
```     7.1 --- a/src/HOL/ROOT	Sun Dec 24 14:46:26 2017 +0100
7.2 +++ b/src/HOL/ROOT	Sun Dec 24 14:28:10 2017 +0100
7.3 @@ -69,7 +69,6 @@
7.4  session "HOL-Analysis-ex" in "Analysis/ex" = "HOL-Analysis" +
7.5    theories
7.6      Approximations
7.7 -    Circle_Area
7.8
7.9  session "HOL-Computational_Algebra" (main timing) in "Computational_Algebra" = "HOL-Library" +
7.10    theories
```