Removed Analysis/ex/Circle_Area; replaced by more general Analysis/Ball_Volume
authoreberlm <eberlm@in.tum.de>
Sun Dec 24 14:28:10 2017 +0100 (17 months ago)
changeset 67278c60e3d615b8c
parent 67277 7dda4a667e40
child 67279 d327c11c9f3e
Removed Analysis/ex/Circle_Area; replaced by more general Analysis/Ball_Volume
src/HOL/Analysis/Analysis.thy
src/HOL/Analysis/Ball_Volume.thy
src/HOL/Analysis/Borel_Space.thy
src/HOL/Analysis/Complex_Transcendental.thy
src/HOL/Analysis/Gamma_Function.thy
src/HOL/Analysis/ex/Circle_Area.thy
src/HOL/ROOT
     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