# HG changeset patch
# User eberlm <eberlm@in.tum.de>
# Date 1514122090 -3600
# Node ID c60e3d615b8c1ac1390647a955de75add8d8f4fc
# Parent  7dda4a667e40c51dcc9f249a5b3a298e13c39fff
Removed Analysis/ex/Circle_Area; replaced by more general Analysis/Ball_Volume

diff -r 7dda4a667e40 -r c60e3d615b8c src/HOL/Analysis/Analysis.thy
--- a/src/HOL/Analysis/Analysis.thy	Sun Dec 24 14:46:26 2017 +0100
+++ b/src/HOL/Analysis/Analysis.thy	Sun Dec 24 14:28:10 2017 +0100
@@ -22,6 +22,7 @@
   FPS_Convergence
   Generalised_Binomial_Theorem
   Gamma_Function
+  Ball_Volume
 begin
 
 end
diff -r 7dda4a667e40 -r c60e3d615b8c src/HOL/Analysis/Ball_Volume.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Analysis/Ball_Volume.thy	Sun Dec 24 14:28:10 2017 +0100
@@ -0,0 +1,301 @@
+(*  
+   File:     HOL/Analysis/Gamma_Function.thy
+   Author:   Manuel Eberl, TU München
+
+   The volume (Lebesgue measure) of an n-dimensional ball.
+*)
+section \<open>The volume of an $n$-ball\<close>
+theory Ball_Volume
+  imports Gamma_Function Lebesgue_Integral_Substitution
+begin
+
+text \<open>
+  We define the volume of the unit ball in terms of the Gamma function. Note that the
+  dimension need not be an integer; we also allow fractional dimensions, although we do
+  not use this case or prove anything about it for now.
+\<close>
+definition unit_ball_vol :: "real \<Rightarrow> real" where
+  "unit_ball_vol n = pi powr (n / 2) / Gamma (n / 2 + 1)"
+
+lemma unit_ball_vol_nonneg [simp]: "n \<ge> 0 \<Longrightarrow> unit_ball_vol n \<ge> 0"
+  by (auto simp add: unit_ball_vol_def intro!: divide_nonneg_pos Gamma_real_pos)
+
+text \<open>
+  We first need the value of the following integral, which is at the core of
+  computing the measure of an $n+1$-dimensional ball in terms of the measure of an 
+  $n$-dimensional one.
+\<close>
+lemma emeasure_cball_aux_integral:
+  "(\<integral>\<^sup>+x. indicator {-1..1} x * sqrt (1 - x\<^sup>2) ^ n \<partial>lborel) = 
+      ennreal (Beta (1 / 2) (real n / 2 + 1))"
+proof -
+  have "((\<lambda>t. t powr (-1 / 2) * (1 - t) powr (real n / 2)) has_integral
+          Beta (1 / 2) (real n / 2 + 1)) {0..1}"
+    using has_integral_Beta_real[of "1/2" "n / 2 + 1"] by simp
+  from nn_integral_has_integral_lebesgue[OF _ this] have
+     "ennreal (Beta (1 / 2) (real n / 2 + 1)) =
+        nn_integral lborel (\<lambda>t. ennreal (t powr (-1 / 2) * (1 - t) powr (real n / 2) * 
+                                indicator {0^2..1^2} t))"
+    by (simp add: mult_ac ennreal_mult' ennreal_indicator)
+  also have "\<dots> = (\<integral>\<^sup>+ x. ennreal (x\<^sup>2 powr - (1 / 2) * (1 - x\<^sup>2) powr (real n / 2) * (2 * x) *
+                          indicator {0..1} x) \<partial>lborel)"
+    by (subst nn_integral_substitution[where g = "\<lambda>x. x ^ 2" and g' = "\<lambda>x. 2 * x"])
+       (auto intro!: derivative_eq_intros continuous_intros)
+  also have "\<dots> = (\<integral>\<^sup>+ x. 2 * ennreal ((1 - x\<^sup>2) powr (real n / 2) * indicator {0..1} x) \<partial>lborel)"
+    by (intro nn_integral_cong_AE AE_I[of _ _ "{0}"]) 
+       (auto simp: indicator_def powr_minus powr_half_sqrt divide_simps ennreal_mult' mult_ac)
+  also have "\<dots> = (\<integral>\<^sup>+ x. ennreal ((1 - x\<^sup>2) powr (real n / 2) * indicator {0..1} x) \<partial>lborel) +
+                    (\<integral>\<^sup>+ x. ennreal ((1 - x\<^sup>2) powr (real n / 2) * indicator {0..1} x) \<partial>lborel)"
+    (is "_ = ?I + _") by (simp add: mult_2 nn_integral_add)
+  also have "?I = (\<integral>\<^sup>+ x. ennreal ((1 - x\<^sup>2) powr (real n / 2) * indicator {-1..0} x) \<partial>lborel)"
+    by (subst nn_integral_real_affine[of _ "-1" 0])
+       (auto simp: indicator_def intro!: nn_integral_cong)
+  hence "?I + ?I = \<dots> + ?I" by simp
+  also have "\<dots> = (\<integral>\<^sup>+ x. ennreal ((1 - x\<^sup>2) powr (real n / 2) * 
+                    (indicator {-1..0} x + indicator{0..1} x)) \<partial>lborel)"
+    by (subst nn_integral_add [symmetric]) (auto simp: algebra_simps)
+  also have "\<dots> = (\<integral>\<^sup>+ x. ennreal ((1 - x\<^sup>2) powr (real n / 2) * indicator {-1..1} x) \<partial>lborel)"
+    by (intro nn_integral_cong_AE AE_I[of _ _ "{0}"]) (auto simp: indicator_def)
+  also have "\<dots> = (\<integral>\<^sup>+ x. ennreal (indicator {-1..1} x * sqrt (1 - x\<^sup>2) ^ n) \<partial>lborel)"
+    by (intro nn_integral_cong_AE AE_I[of _ _ "{1, -1}"])
+       (auto simp: powr_half_sqrt [symmetric] indicator_def abs_square_le_1
+          abs_square_eq_1 powr_def exp_of_nat_mult [symmetric] emeasure_lborel_countable)
+  finally show ?thesis ..
+qed
+
+lemma real_sqrt_le_iff': "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> sqrt x \<le> y \<longleftrightarrow> x \<le> y ^ 2"
+  using real_le_lsqrt sqrt_le_D by blast
+
+lemma power2_le_iff_abs_le: "y \<ge> 0 \<Longrightarrow> (x::real) ^ 2 \<le> y ^ 2 \<longleftrightarrow> abs x \<le> y"
+  by (subst real_sqrt_le_iff' [symmetric]) auto
+
+text \<open>
+  Isabelle's type system makes it very difficult to do an induction over the dimension 
+  of a Euclidean space type, because the type would change in the inductive step. To avoid 
+  this problem, we instead formulate the problem in a more concrete way by unfolding the 
+  definition of the Euclidean norm.
+\<close>
+lemma emeasure_cball_aux:
+  assumes "finite A" "r > 0"
+  shows   "emeasure (Pi\<^sub>M A (\<lambda>_. lborel))
+             ({f. sqrt (\<Sum>i\<in>A. (f i)\<^sup>2) \<le> r} \<inter> space (Pi\<^sub>M A (\<lambda>_. lborel))) =
+             ennreal (unit_ball_vol (real (card A)) * r ^ card A)"
+  using assms
+proof (induction arbitrary: r)
+  case (empty r)
+  thus ?case
+    by (simp add: unit_ball_vol_def space_PiM)
+next
+  case (insert i A r)
+  interpret product_sigma_finite "\<lambda>_. lborel"
+    by standard
+  have "emeasure (Pi\<^sub>M (insert i A) (\<lambda>_. lborel)) 
+            ({f. sqrt (\<Sum>i\<in>insert i A. (f i)\<^sup>2) \<le> r} \<inter> space (Pi\<^sub>M (insert i A) (\<lambda>_. lborel))) =
+        nn_integral (Pi\<^sub>M (insert i A) (\<lambda>_. lborel))
+          (indicator ({f. sqrt (\<Sum>i\<in>insert i A. (f i)\<^sup>2) \<le> r} \<inter>
+          space (Pi\<^sub>M (insert i A) (\<lambda>_. lborel))))"
+    by (subst nn_integral_indicator) auto
+  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> 
+                                space (Pi\<^sub>M (insert i A) (\<lambda>_. lborel))) (x(i := y)) 
+                   \<partial>Pi\<^sub>M A (\<lambda>_. lborel) \<partial>lborel)"
+    using insert.prems insert.hyps by (subst product_nn_integral_insert_rev) auto
+  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> 
+               sqrt (r ^ 2 - y ^ 2)} \<inter> space (Pi\<^sub>M A (\<lambda>_. lborel))) x \<partial>Pi\<^sub>M A (\<lambda>_. lborel) \<partial>lborel)"
+  proof (intro nn_integral_cong, goal_cases)
+    case (1 y f)
+    have *: "y \<in> {-r..r}" if "y ^ 2 + c \<le> r ^ 2" "c \<ge> 0" for c
+    proof -
+      have "y ^ 2 \<le> y ^ 2 + c" using that by simp
+      also have "\<dots> \<le> r ^ 2" by fact
+      finally show ?thesis
+        using \<open>r > 0\<close> by (simp add: power2_le_iff_abs_le abs_if split: if_splits)
+    qed
+    have "(\<Sum>x\<in>A. (if x = i then y else f x)\<^sup>2) = (\<Sum>x\<in>A. (f x)\<^sup>2)"
+      using insert.hyps by (intro sum.cong) auto
+    thus ?case using 1 \<open>r > 0\<close>
+      by (auto simp: sum_nonneg real_sqrt_le_iff' indicator_def PiE_def space_PiM dest!: *)
+  qed
+  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)) 
+                                   \<le> sqrt (r ^ 2 - y ^ 2)} \<inter> space (Pi\<^sub>M A (\<lambda>_. lborel))) x
+                  \<partial>Pi\<^sub>M A (\<lambda>_. lborel)) \<partial>lborel)" by (subst nn_integral_cmult) auto
+  also have "\<dots> = (\<integral>\<^sup>+ (y::real). indicator {-r..r} y * emeasure (PiM A (\<lambda>_. lborel)) 
+      ({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)"
+    using \<open>finite A\<close> by (intro nn_integral_cong, subst nn_integral_indicator) auto
+  also have "\<dots> = (\<integral>\<^sup>+ (y::real). indicator {-r..r} y * ennreal (unit_ball_vol (real (card A)) * 
+                                  (sqrt (r ^ 2 - y ^ 2)) ^ card A) \<partial>lborel)"
+  proof (intro nn_integral_cong_AE, goal_cases)
+    case 1
+    have "AE y in lborel. y \<notin> {-r,r}"
+      by (intro AE_not_in countable_imp_null_set_lborel) auto
+    thus ?case
+    proof eventually_elim
+      case (elim y)
+      show ?case
+      proof (cases "y \<in> {-r<..<r}")
+        case True
+        hence "y\<^sup>2 < r\<^sup>2" by (subst real_sqrt_less_iff [symmetric]) auto
+        thus ?thesis by (subst insert.IH) (auto simp: real_sqrt_less_iff)
+      qed (insert elim, auto)
+    qed
+  qed
+  also have "\<dots> = ennreal (unit_ball_vol (real (card A))) * 
+                    (\<integral>\<^sup>+ (y::real). indicator {-r..r} y * (sqrt (r ^ 2 - y ^ 2)) ^ card A \<partial>lborel)"
+    by (subst nn_integral_cmult [symmetric])
+       (auto simp: mult_ac ennreal_mult' [symmetric] indicator_def intro!: nn_integral_cong)
+  also have "(\<integral>\<^sup>+ (y::real). indicator {-r..r} y * (sqrt (r ^ 2 - y ^ 2)) ^ card A \<partial>lborel) =
+               (\<integral>\<^sup>+ (y::real). r ^ card A * indicator {-1..1} y * (sqrt (1 - y ^ 2)) ^ card A  
+               \<partial>(distr lborel borel (op * (1/r))))" using \<open>r > 0\<close>
+    by (subst nn_integral_distr)
+       (auto simp: indicator_def field_simps real_sqrt_divide intro!: nn_integral_cong)
+  also have "\<dots> = (\<integral>\<^sup>+ x. ennreal (r ^ Suc (card A)) * 
+               (indicator {- 1..1} x * sqrt (1 - x\<^sup>2) ^ card A) \<partial>lborel)" using \<open>r > 0\<close>
+    by (subst lborel_distr_mult) (auto simp: nn_integral_density ennreal_mult' [symmetric] mult_ac)
+  also have "\<dots> = ennreal (r ^ Suc (card A)) * (\<integral>\<^sup>+ x. indicator {- 1..1} x * 
+                    sqrt (1 - x\<^sup>2) ^ card A \<partial>lborel)"
+    by (subst nn_integral_cmult) auto
+  also note emeasure_cball_aux_integral
+  also have "ennreal (unit_ball_vol (real (card A))) * (ennreal (r ^ Suc (card A)) *
+                 ennreal (Beta (1/2) (card A / 2 + 1))) = 
+               ennreal (unit_ball_vol (card A) * Beta (1/2) (card A / 2 + 1) * r ^ Suc (card A))"
+    using \<open>r > 0\<close> by (simp add: ennreal_mult' [symmetric] mult_ac)
+  also have "unit_ball_vol (card A) * Beta (1/2) (card A / 2 + 1) = unit_ball_vol (Suc (card A))"
+    by (auto simp: unit_ball_vol_def Beta_def Gamma_eq_zero_iff field_simps 
+          Gamma_one_half_real powr_half_sqrt [symmetric] powr_add [symmetric])
+  also have "Suc (card A) = card (insert i A)" using insert.hyps by simp
+  finally show ?case .
+qed
+
+
+text \<open>
+  We now get the main theorem very easily by just applying the above lemma.
+\<close>
+context
+  fixes c :: "'a :: euclidean_space" and r :: real
+  assumes r: "r \<ge> 0"
+begin
+
+theorem emeasure_cball:
+  "emeasure lborel (cball c r) = ennreal (unit_ball_vol (DIM('a)) * r ^ DIM('a))"
+proof (cases "r = 0")
+  case False
+  with r have r: "r > 0" by simp
+  have "(lborel :: 'a measure) = 
+          distr (Pi\<^sub>M Basis (\<lambda>_. lborel)) borel (\<lambda>f. \<Sum>b\<in>Basis. f b *\<^sub>R b)"
+    by (rule lborel_eq)
+  also have "emeasure \<dots> (cball 0 r) = 
+               emeasure (Pi\<^sub>M Basis (\<lambda>_. lborel)) 
+               ({y. dist 0 (\<Sum>b\<in>Basis. y b *\<^sub>R b :: 'a) \<le> r} \<inter> space (Pi\<^sub>M Basis (\<lambda>_. lborel)))"
+    by (subst emeasure_distr) (auto simp: cball_def)
+  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}"
+    by (subst euclidean_dist_l2) (auto simp: L2_set_def)
+  also have "emeasure (Pi\<^sub>M Basis (\<lambda>_. lborel)) (\<dots> \<inter> space (Pi\<^sub>M Basis (\<lambda>_. lborel))) =
+               ennreal (unit_ball_vol (real DIM('a)) * r ^ DIM('a))"
+    using r by (subst emeasure_cball_aux) simp_all
+  also have "emeasure lborel (cball 0 r :: 'a set) =
+               emeasure (distr lborel borel (\<lambda>x. c + x)) (cball c r)"
+    by (subst emeasure_distr) (auto simp: cball_def dist_norm norm_minus_commute)
+  also have "distr lborel borel (\<lambda>x. c + x) = lborel"
+    using lborel_affine[of 1 c] by (simp add: density_1)
+  finally show ?thesis .
+qed auto
+
+corollary content_cball:
+  "content (cball c r) = unit_ball_vol (DIM('a)) * r ^ DIM('a)"
+  by (simp add: measure_def emeasure_cball r)
+
+corollary emeasure_ball:
+  "emeasure lborel (ball c r) = ennreal (unit_ball_vol (DIM('a)) * r ^ DIM('a))"
+proof -
+  from negligible_sphere[of c r] have "sphere c r \<in> null_sets lborel"
+    by (auto simp: null_sets_completion_iff negligible_iff_null_sets negligible_convex_frontier)
+  hence "emeasure lborel (ball c r \<union> sphere c r :: 'a set) = emeasure lborel (ball c r :: 'a set)"
+    by (intro emeasure_Un_null_set) auto
+  also have "ball c r \<union> sphere c r = (cball c r :: 'a set)" by auto
+  also have "emeasure lborel \<dots> = ennreal (unit_ball_vol (real DIM('a)) * r ^ DIM('a))"
+    by (rule emeasure_cball)
+  finally show ?thesis ..
+qed
+
+corollary content_ball:
+  "content (ball c r) = unit_ball_vol (DIM('a)) * r ^ DIM('a)"
+  by (simp add: measure_def r emeasure_ball)
+
+end
+
+
+text \<open>
+  Lastly, we now prove some nicer explicit formulas for the volume of the unit balls in 
+  the cases of even and odd integer dimensions.
+\<close>
+lemma unit_ball_vol_even:
+  "unit_ball_vol (real (2 * n)) = pi ^ n / fact n"
+  by (simp add: unit_ball_vol_def add_ac powr_realpow Gamma_fact)
+
+lemma unit_ball_vol_odd':
+        "unit_ball_vol (real (2 * n + 1)) = pi ^ n / pochhammer (1 / 2) (Suc n)"
+  and unit_ball_vol_odd:
+        "unit_ball_vol (real (2 * n + 1)) =
+           (2 ^ (2 * Suc n) * fact (Suc n)) / fact (2 * Suc n) * pi ^ n"
+proof -
+  have "unit_ball_vol (real (2 * n + 1)) = 
+          pi powr (real n + 1 / 2) / Gamma (1 / 2 + real (Suc n))"
+    by (simp add: unit_ball_vol_def field_simps)
+  also have "pochhammer (1 / 2) (Suc n) = Gamma (1 / 2 + real (Suc n)) / Gamma (1 / 2)"
+    by (intro pochhammer_Gamma) auto
+  hence "Gamma (1 / 2 + real (Suc n)) = sqrt pi * pochhammer (1 / 2) (Suc n)"
+    by (simp add: Gamma_one_half_real)
+  also have "pi powr (real n + 1 / 2) / \<dots> = pi ^ n / pochhammer (1 / 2) (Suc n)"
+    by (simp add: powr_add powr_half_sqrt powr_realpow)
+  finally show "unit_ball_vol (real (2 * n + 1)) = \<dots>" .
+  also have "pochhammer (1 / 2 :: real) (Suc n) = 
+               fact (2 * Suc n) / (2 ^ (2 * Suc n) * fact (Suc n))"
+    using fact_double[of "Suc n", where ?'a = real] by (simp add: divide_simps mult_ac)
+  also have "pi ^n / \<dots> = (2 ^ (2 * Suc n) * fact (Suc n)) / fact (2 * Suc n) * pi ^ n"
+    by simp
+  finally show "unit_ball_vol (real (2 * n + 1)) = \<dots>" .
+qed
+
+lemma unit_ball_vol_numeral:
+  "unit_ball_vol (numeral (Num.Bit0 n)) = pi ^ numeral n / fact (numeral n)" (is ?th1)
+  "unit_ball_vol (numeral (Num.Bit1 n)) = 2 ^ (2 * Suc (numeral n)) * fact (Suc (numeral n)) /
+    fact (2 * Suc (numeral n)) * pi ^ numeral n" (is ?th2)
+proof -
+  have "numeral (Num.Bit0 n) = (2 * numeral n :: nat)" 
+    by (simp only: numeral_Bit0 mult_2 ring_distribs)
+  also have "unit_ball_vol \<dots> = pi ^ numeral n / fact (numeral n)"
+    by (rule unit_ball_vol_even)
+  finally show ?th1 by simp
+next
+  have "numeral (Num.Bit1 n) = (2 * numeral n + 1 :: nat)"
+    by (simp only: numeral_Bit1 mult_2)
+  also have "unit_ball_vol \<dots> = 2 ^ (2 * Suc (numeral n)) * fact (Suc (numeral n)) /
+                                  fact (2 * Suc (numeral n)) * pi ^ numeral n"
+    by (rule unit_ball_vol_odd)
+  finally show ?th2 by simp
+qed
+
+lemmas eval_unit_ball_vol = unit_ball_vol_numeral fact_numeral
+
+
+text \<open>
+  Just for fun, we compute the volume of unit balls for a few dimensions.
+\<close>
+lemma unit_ball_vol_0 [simp]: "unit_ball_vol 0 = 1"
+  using unit_ball_vol_even[of 0] by simp
+
+lemma unit_ball_vol_1 [simp]: "unit_ball_vol 1 = 2"
+  using unit_ball_vol_odd[of 0] by simp
+
+corollary unit_ball_vol_2: "unit_ball_vol 2 = pi"
+      and unit_ball_vol_3: "unit_ball_vol 3 = 4 / 3 * pi"
+      and unit_ball_vol_4: "unit_ball_vol 4 = pi\<^sup>2 / 2"
+      and unit_ball_vol_5: "unit_ball_vol 5 = 8 / 15 * pi\<^sup>2"
+  by (simp_all add: eval_unit_ball_vol)
+
+corollary circle_area: "r \<ge> 0 \<Longrightarrow> content (ball c r :: (real ^ 2) set) = r ^ 2 * pi"
+  by (simp add: content_ball unit_ball_vol_2)
+
+corollary sphere_volume: "r \<ge> 0 \<Longrightarrow> content (ball c r :: (real ^ 3) set) = 4 / 3 * r ^ 3 * pi"
+  by (simp add: content_ball unit_ball_vol_3)
+
+end
diff -r 7dda4a667e40 -r c60e3d615b8c src/HOL/Analysis/Borel_Space.thy
--- a/src/HOL/Analysis/Borel_Space.thy	Sun Dec 24 14:46:26 2017 +0100
+++ b/src/HOL/Analysis/Borel_Space.thy	Sun Dec 24 14:28:10 2017 +0100
@@ -1515,6 +1515,11 @@
   apply auto
   done
 
+lemma powr_real_measurable [measurable]:
+  assumes "f \<in> measurable M borel" "g \<in> measurable M borel"
+  shows   "(\<lambda>x. f x powr g x :: real) \<in> measurable M borel"
+  using assms by (simp_all add: powr_def)
+
 lemma measurable_of_bool[measurable]: "of_bool \<in> count_space UNIV \<rightarrow>\<^sub>M borel"
   by simp
 
diff -r 7dda4a667e40 -r c60e3d615b8c src/HOL/Analysis/Complex_Transcendental.thy
--- a/src/HOL/Analysis/Complex_Transcendental.thy	Sun Dec 24 14:46:26 2017 +0100
+++ b/src/HOL/Analysis/Complex_Transcendental.thy	Sun Dec 24 14:28:10 2017 +0100
@@ -1489,6 +1489,27 @@
   finally show ?thesis .
 qed
 
+lemma Ln_measurable [measurable]: "Ln \<in> measurable borel borel"
+proof -
+  have *: "Ln (-of_real x) = of_real (ln x) + \<i> * pi" if "x > 0" for x
+    using that by (subst Ln_minus) (auto simp: Ln_of_real)
+  have **: "Ln (of_real x) = of_real (ln (-x)) + \<i> * pi" if "x < 0" for x
+    using *[of "-x"] that by simp
+  have cont: "set_borel_measurable borel (- \<real>\<^sub>\<le>\<^sub>0) Ln"
+    by (intro borel_measurable_continuous_on_indicator continuous_intros) auto
+  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"
+    (is "?f \<in> _") by (rule measurable_If_set[OF _ cont]) auto
+  hence "(\<lambda>x. if x = 0 then Ln 0 else ?f x) \<in> borel \<rightarrow>\<^sub>M borel" by measurable
+  also have "(\<lambda>x. if x = 0 then Ln 0 else ?f x) = Ln"
+    by (auto simp: fun_eq_iff ** nonpos_Reals_def)
+  finally show ?thesis .
+qed
+
+lemma powr_complex_measurable [measurable]:
+  assumes [measurable]: "f \<in> measurable M borel" "g \<in> measurable M borel"
+  shows   "(\<lambda>x. f x powr g x :: complex) \<in> measurable M borel"
+  using assms by (simp add: powr_def)
+
 
 subsection\<open>Relation between Ln and Arg, and hence continuity of Arg\<close>
 
diff -r 7dda4a667e40 -r c60e3d615b8c src/HOL/Analysis/Gamma_Function.thy
--- a/src/HOL/Analysis/Gamma_Function.thy	Sun Dec 24 14:46:26 2017 +0100
+++ b/src/HOL/Analysis/Gamma_Function.thy	Sun Dec 24 14:28:10 2017 +0100
@@ -1653,7 +1653,10 @@
   using Gamma_fact[of "n - 1", where 'a = real]
   by (simp add: ln_Gamma_real_pos of_nat_diff Ln_of_real [symmetric])
 
-lemma Gamma_real_pos: "x > (0::real) \<Longrightarrow> Gamma x > 0"
+lemma Gamma_real_pos [simp, intro]: "x > (0::real) \<Longrightarrow> Gamma x > 0"
+  by (simp add: Gamma_real_pos_exp)
+
+lemma Gamma_real_nonneg [simp, intro]: "x > (0::real) \<Longrightarrow> Gamma x \<ge> 0"
   by (simp add: Gamma_real_pos_exp)
 
 lemma has_field_derivative_ln_Gamma_real [derivative_intros]:
@@ -2985,6 +2988,170 @@
   finally show ?thesis .
 qed
 
+lemma Gamma_conv_nn_integral_real:
+  assumes "s > (0::real)"
+  shows   "Gamma s = nn_integral lborel (\<lambda>t. ennreal (indicator {0..} t * t powr (s - 1) / exp t))"
+  using nn_integral_has_integral_lebesgue[OF _ Gamma_integral_real[OF assms]] by simp
+
+lemma integrable_Beta:
+  assumes "a > 0" "b > (0::real)"
+  shows   "set_integrable lborel {0..1} (\<lambda>t. t powr (a - 1) * (1 - t) powr (b - 1))"
+proof -
+  define C where "C = max 1 ((1/2) powr (b - 1))"
+  define D where "D = max 1 ((1/2) powr (a - 1))"
+  have C: "(1 - x) powr (b - 1) \<le> C" if "x \<in> {0..1/2}" for x
+  proof (cases "b < 1")
+    case False
+    with that have "(1 - x) powr (b - 1) \<le> (1 powr (b - 1))" by (intro powr_mono2) auto
+    thus ?thesis by (auto simp: C_def)
+  qed (insert that, auto simp: max.coboundedI1 max.coboundedI2 powr_mono2' powr_mono2 C_def)
+  have D: "x powr (a - 1) \<le> D" if "x \<in> {1/2..1}" for x
+  proof (cases "a < 1")
+    case False
+    with that have "x powr (a - 1) \<le> (1 powr (a - 1))" by (intro powr_mono2) auto
+    thus ?thesis by (auto simp: D_def)
+  next
+    case True
+  qed (insert that, auto simp: max.coboundedI1 max.coboundedI2 powr_mono2' powr_mono2 D_def)
+  have [simp]: "C \<ge> 0" "D \<ge> 0" by (simp_all add: C_def D_def)
+
+  have I1: "set_integrable lborel {0..1 / 2} (\<lambda>t. t powr (a - 1) * (1 - t) powr (b - 1))"
+  proof (rule Bochner_Integration.integrable_bound[OF _ _ AE_I2])
+    have "(\<lambda>t. t powr (a - 1)) integrable_on {0..1 / 2}"
+      by (rule integrable_on_powr_from_0) (use assms in auto)
+    hence "(\<lambda>t. t powr (a - 1)) absolutely_integrable_on {0..1 / 2}"
+      by (subst absolutely_integrable_on_iff_nonneg) auto
+    from integrable_mult_right[OF this, of C]
+      show "set_integrable lborel {0..1 / 2} (\<lambda>t. C * t powr (a - 1))"
+      by (subst (asm) integrable_completion) (auto simp: mult_ac)
+  next
+    fix x :: real
+    have "x powr (a - 1) * (1 - x) powr (b - 1) \<le> x powr (a - 1) * C" if "x \<in> {0..1/2}"
+      using that by (intro mult_left_mono powr_mono2 C) auto
+    thus "norm (indicator {0..1/2} x *\<^sub>R (x powr (a - 1) * (1 - x) powr (b - 1))) \<le>
+            norm (indicator {0..1/2} x *\<^sub>R (C * x powr (a - 1)))"
+      by (auto simp: indicator_def abs_mult mult_ac)
+  qed (auto intro!: AE_I2 simp: indicator_def)
+
+  have I2: "set_integrable lborel {1 / 2..1} (\<lambda>t. t powr (a - 1) * (1 - t) powr (b - 1))"
+  proof (rule Bochner_Integration.integrable_bound[OF _ _ AE_I2])
+    have "(\<lambda>t. t powr (b - 1)) integrable_on {0..1/2}"
+      by (rule integrable_on_powr_from_0) (use assms in auto)
+    hence "(\<lambda>t. t powr (b - 1)) integrable_on (cbox 0 (1/2))" by simp
+    from integrable_affinity[OF this, of "-1" 1]
+      have "(\<lambda>t. (1 - t) powr (b - 1)) integrable_on {1/2..1}" by simp
+    hence "(\<lambda>t. (1 - t) powr (b - 1)) absolutely_integrable_on {1/2..1}"
+      by (subst absolutely_integrable_on_iff_nonneg) auto
+    from integrable_mult_right[OF this, of D]
+      show "set_integrable lborel {1 / 2..1} (\<lambda>t. D * (1 - t) powr (b - 1))"
+      by (subst (asm) integrable_completion) (auto simp: mult_ac)
+  next
+    fix x :: real
+    have "x powr (a - 1) * (1 - x) powr (b - 1) \<le> D * (1 - x) powr (b - 1)" if "x \<in> {1/2..1}"
+      using that by (intro mult_right_mono powr_mono2 D) auto
+    thus "norm (indicator {1/2..1} x *\<^sub>R (x powr (a - 1) * (1 - x) powr (b - 1))) \<le>
+            norm (indicator {1/2..1} x *\<^sub>R (D * (1 - x) powr (b - 1)))"
+      by (auto simp: indicator_def abs_mult mult_ac)
+  qed (auto intro!: AE_I2 simp: indicator_def)
+
+  have "set_integrable lborel ({0..1/2} \<union> {1/2..1}) (\<lambda>t. t powr (a - 1) * (1 - t) powr (b - 1))"
+    by (intro set_integrable_Un I1 I2) auto
+  also have "{0..1/2} \<union> {1/2..1} = {0..(1::real)}" by auto
+  finally show ?thesis .
+qed
+
+lemma integrable_Beta':
+  assumes "a > 0" "b > (0::real)"
+  shows   "(\<lambda>t. t powr (a - 1) * (1 - t) powr (b - 1)) integrable_on {0..1}"
+  using integrable_Beta[OF assms] by (rule set_borel_integral_eq_integral)
+
+lemma has_integral_Beta_real:
+  assumes a: "a > 0" and b: "b > (0 :: real)"
+  shows "((\<lambda>t. t powr (a - 1) * (1 - t) powr (b - 1)) has_integral Beta a b) {0..1}"
+proof -
+  define B where "B = integral {0..1} (\<lambda>x. x powr (a - 1) * (1 - x) powr (b - 1))"
+  have [simp]: "B \<ge> 0" unfolding B_def using a b
+    by (intro integral_nonneg integrable_Beta') auto
+  from a b have "ennreal (Gamma a * Gamma b) =
+    (\<integral>\<^sup>+ t. ennreal (indicator {0..} t * t powr (a - 1) / exp t) \<partial>lborel) *
+    (\<integral>\<^sup>+ t. ennreal (indicator {0..} t * t powr (b - 1) / exp t) \<partial>lborel)"
+    by (subst ennreal_mult') (simp_all add: Gamma_conv_nn_integral_real)
+  also have "\<dots> = (\<integral>\<^sup>+t. \<integral>\<^sup>+u. ennreal (indicator {0..} t * t powr (a - 1) / exp t) *
+                            ennreal (indicator {0..} u * u powr (b - 1) / exp u) \<partial>lborel \<partial>lborel)"
+    by (simp add: nn_integral_cmult nn_integral_multc)
+  also have "\<dots> = (\<integral>\<^sup>+t. \<integral>\<^sup>+u. ennreal (indicator ({0..}\<times>{0..}) (t,u) * t powr (a - 1) * u powr (b - 1)
+                            / exp (t + u)) \<partial>lborel \<partial>lborel)"
+    by (intro nn_integral_cong)
+       (auto simp: indicator_def divide_ennreal ennreal_mult' [symmetric] exp_add)
+  also have "\<dots> = (\<integral>\<^sup>+t. \<integral>\<^sup>+u. ennreal (indicator ({0..}\<times>{t..}) (t,u) * t powr (a - 1) * 
+                              (u - t) powr (b - 1) / exp u) \<partial>lborel \<partial>lborel)"
+  proof (rule nn_integral_cong, goal_cases)
+    case (1 t)
+    have "(\<integral>\<^sup>+u. ennreal (indicator ({0..}\<times>{0..}) (t,u) * t powr (a - 1) * 
+                              u powr (b - 1) / exp (t + u)) \<partial>distr lborel borel (op + (-t))) =
+               (\<integral>\<^sup>+u. ennreal (indicator ({0..}\<times>{t..}) (t,u) * t powr (a - 1) * 
+                              (u - t) powr (b - 1) / exp u) \<partial>lborel)"
+      by (subst nn_integral_distr) (auto intro!: nn_integral_cong simp: indicator_def)
+    thus ?case by (subst (asm) lborel_distr_plus)
+  qed
+  also have "\<dots> = (\<integral>\<^sup>+u. \<integral>\<^sup>+t. ennreal (indicator ({0..}\<times>{t..}) (t,u) * t powr (a - 1) * 
+                              (u - t) powr (b - 1) / exp u) \<partial>lborel \<partial>lborel)"
+    by (subst lborel_pair.Fubini')
+       (auto simp: case_prod_unfold indicator_def cong: measurable_cong_sets)
+  also have "\<dots> = (\<integral>\<^sup>+u. \<integral>\<^sup>+t. ennreal (indicator {0..u} t * t powr (a - 1) * (u - t) powr (b - 1)) *
+                              ennreal (indicator {0..} u / exp u) \<partial>lborel \<partial>lborel)"
+    by (intro nn_integral_cong) (auto simp: indicator_def ennreal_mult' [symmetric])
+  also have "\<dots> = (\<integral>\<^sup>+u. (\<integral>\<^sup>+t. ennreal (indicator {0..u} t * t powr (a - 1) * (u - t) powr (b - 1)) 
+                          \<partial>lborel) * ennreal (indicator {0..} u / exp u) \<partial>lborel)"
+    by (subst nn_integral_multc [symmetric]) auto 
+  also have "\<dots> = (\<integral>\<^sup>+u. (\<integral>\<^sup>+t. ennreal (indicator {0..u} t * t powr (a - 1) * (u - t) powr (b - 1)) 
+                          \<partial>lborel) * ennreal (indicator {0<..} u / exp u) \<partial>lborel)"
+    by (intro nn_integral_cong_AE eventually_mono[OF AE_lborel_singleton[of 0]]) 
+       (auto simp: indicator_def)
+  also have "\<dots> = (\<integral>\<^sup>+u. ennreal B * ennreal (indicator {0..} u / exp u * u powr (a + b - 1)) \<partial>lborel)"
+  proof (intro nn_integral_cong, goal_cases)
+    case (1 u)
+    show ?case
+    proof (cases "u > 0")
+      case True
+      have "(\<integral>\<^sup>+t. ennreal (indicator {0..u} t * t powr (a - 1) * (u - t) powr (b - 1)) \<partial>lborel) = 
+              (\<integral>\<^sup>+t. ennreal (indicator {0..1} t * (u * t) powr (a - 1) * (u - u * t) powr (b - 1)) 
+                \<partial>distr lborel borel (op * (1 / u)))" (is "_ = nn_integral _ ?f")
+        using True
+        by (subst nn_integral_distr) (auto simp: indicator_def field_simps intro!: nn_integral_cong)
+      also have "distr lborel borel (op * (1 / u)) = density lborel (\<lambda>_. u)"
+        using \<open>u > 0\<close> by (subst lborel_distr_mult) auto
+      also have "nn_integral \<dots> ?f = (\<integral>\<^sup>+x. ennreal (indicator {0..1} x * (u * (u * x) powr (a - 1) *
+                                              (u * (1 - x)) powr (b - 1))) \<partial>lborel)" using \<open>u > 0\<close>
+        by (subst nn_integral_density) (auto simp: ennreal_mult' [symmetric] algebra_simps)
+      also have "\<dots> = (\<integral>\<^sup>+x. ennreal (u powr (a + b - 1)) * 
+                            ennreal (indicator {0..1} x * x powr (a - 1) *
+                                       (1 - x) powr (b - 1)) \<partial>lborel)" using \<open>u > 0\<close> a b
+        by (intro nn_integral_cong)
+           (auto simp: indicator_def powr_mult powr_add powr_diff mult_ac ennreal_mult' [symmetric])
+      also have "\<dots> = ennreal (u powr (a + b - 1)) * 
+                        (\<integral>\<^sup>+x. ennreal (indicator {0..1} x * x powr (a - 1) *
+                                         (1 - x) powr (b - 1)) \<partial>lborel)"
+        by (subst nn_integral_cmult) auto
+      also have "((\<lambda>x. x powr (a - 1) * (1 - x) powr (b - 1)) has_integral 
+                   integral {0..1} (\<lambda>x. x powr (a - 1) * (1 - x) powr (b - 1))) {0..1}"
+        using a b by (intro integrable_integral integrable_Beta')
+      from nn_integral_has_integral_lebesgue[OF _ this] a b
+        have "(\<integral>\<^sup>+x. ennreal (indicator {0..1} x * x powr (a - 1) *
+                         (1 - x) powr (b - 1)) \<partial>lborel) = B" by (simp add: mult_ac B_def)
+      finally show ?thesis using \<open>u > 0\<close> by (simp add: ennreal_mult' [symmetric] mult_ac)
+    qed auto
+  qed
+  also have "\<dots> = ennreal B * ennreal (Gamma (a + b))"
+    using a b by (subst nn_integral_cmult) (auto simp: Gamma_conv_nn_integral_real)
+  also have "\<dots> = ennreal (B * Gamma (a + b))"
+    by (subst (1 2) mult.commute, intro ennreal_mult' [symmetric]) (use a b in auto)
+  finally have "B = Beta a b" using a b Gamma_real_pos[of "a + b"]
+    by (subst (asm) ennreal_inj) (auto simp: field_simps Beta_def Gamma_eq_zero_iff)
+  moreover have "(\<lambda>t. t powr (a - 1) * (1 - t) powr (b - 1)) integrable_on {0..1}"
+    by (intro integrable_Beta' a b)
+  ultimately show ?thesis by (simp add: has_integral_iff B_def)
+qed
 
 
 subsection \<open>The Weierstraß product formula for the sine\<close>
diff -r 7dda4a667e40 -r c60e3d615b8c src/HOL/Analysis/ex/Circle_Area.thy
--- a/src/HOL/Analysis/ex/Circle_Area.thy	Sun Dec 24 14:46:26 2017 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,183 +0,0 @@
-(*  Title:      HOL/Analysis/ex/Circle_Area.thy
-    Author:     Manuel Eberl, TU Muenchen
-
-A proof that the area of a circle with radius R is R\<^sup>2\<pi>.
-*)
-
-section \<open>The area of a circle\<close>
-
-theory Circle_Area
-imports Complex_Main "HOL-Analysis.Interval_Integral"
-begin
-
-lemma plus_emeasure':
-  assumes "A \<in> sets M" "B \<in> sets M" "A \<inter> B \<in> null_sets M"
-  shows "emeasure M A + emeasure M B = emeasure M (A \<union> B)"
-proof-
-  let ?C = "A \<inter> B"
-  have "A \<union> B = A \<union> (B - ?C)" by blast
-  with assms have "emeasure M (A \<union> B) = emeasure M A + emeasure M (B - ?C)"
-    by (subst plus_emeasure) auto
-  also from assms(3,2) have "emeasure M (B - ?C) = emeasure M B"
-    by (rule emeasure_Diff_null_set)
-  finally show ?thesis ..
-qed
-
-lemma real_sqrt_square:
-  "x \<ge> 0 \<Longrightarrow> sqrt (x^2) = (x::real)" by simp
-
-lemma unit_circle_area_aux:
-  "LBINT x=-1..1. 2 * sqrt (1 - x^2) = pi"
-proof-
-  have "LBINT x=-1..1. 2 * sqrt (1 - x^2) =
-            LBINT x=ereal (sin (-pi/2))..ereal (sin (pi/2)). 2 * sqrt (1 - x^2)"
-    by (simp_all add: one_ereal_def)
-  also have "... = LBINT x=-pi/2..pi/2. cos x *\<^sub>R (2 * sqrt (1 - (sin x)\<^sup>2))"
-    by (rule interval_integral_substitution_finite[symmetric])
-       (auto intro: DERIV_subset[OF DERIV_sin] intro!: continuous_intros)
-  also have "... = LBINT x=-pi/2..pi/2. 2 * cos x * sqrt ((cos x)^2)"
-    by (simp add: cos_squared_eq field_simps)
-  also {
-    fix x assume "x \<in> {-pi/2<..<pi/2}"
-    hence "cos x \<ge> 0" by (intro cos_ge_zero) simp_all
-    hence "sqrt ((cos x)^2) = cos x" by simp
-  } note A = this
-  have "LBINT x=-pi/2..pi/2. 2 * cos x * sqrt ((cos x)^2) = LBINT x=-pi/2..pi/2. 2 * (cos x)^2"
-    by (intro interval_integral_cong, subst A) (simp_all add: min_def max_def power2_eq_square)
-  also let ?F = "\<lambda>x. x + sin x * cos x"
-   {
-    fix x A
-    have "(?F has_real_derivative 1 - (sin x)^2 + (cos x)^2) (at x)"
-      by (auto simp: power2_eq_square intro!: derivative_eq_intros)
-    also have "1 - (sin x)^2 + (cos x)^2 = 2 * (cos x)^2" by (simp add: cos_squared_eq)
-    finally have "(?F has_real_derivative 2 * (cos x)^2) (at x within A)"
-      by (rule DERIV_subset) simp
-  }
-  hence "LBINT x=-pi/2..pi/2. 2 * (cos x)^2 = ?F (pi/2) - ?F (-pi/2)"
-    by (intro interval_integral_FTC_finite)
-       (auto simp: has_field_derivative_iff_has_vector_derivative intro!: continuous_intros)
-  also have "... = pi" by simp
-  finally show ?thesis .
-qed
-
-lemma unit_circle_area:
-  "emeasure lborel {z::real\<times>real. norm z \<le> 1} = pi" (is "emeasure _ ?A = _")
-proof-
-  let ?A1 = "{(x,y)\<in>?A. y \<ge> 0}" and ?A2 = "{(x,y)\<in>?A. y \<le> 0}"
-  have [measurable]: "(\<lambda>x. snd (x :: real \<times> real)) \<in> measurable borel borel"
-    by (simp add: borel_prod[symmetric])
-
-  have "?A1 = ?A \<inter> {x\<in>space lborel. snd x \<ge> 0}" by auto
-  also have "?A \<inter> {x\<in>space lborel. snd x \<ge> 0} \<in> sets borel"
-    by (intro sets.Int pred_Collect_borel) simp_all
-  finally have A1_in_sets: "?A1 \<in> sets lborel" by (subst sets_lborel)
-
-  have "?A2 = ?A \<inter> {x\<in>space lborel. snd x \<le> 0}" by auto
-  also have "... \<in> sets borel"
-    by (intro sets.Int pred_Collect_borel) simp_all
-  finally have A2_in_sets: "?A2 \<in> sets lborel" by (subst sets_lborel)
-
-  have A12: "?A = ?A1 \<union> ?A2" by auto
-  have sq_le_1_iff: "\<And>x. x\<^sup>2 \<le> 1 \<longleftrightarrow> abs (x::real) \<le> 1"
-    by (simp add: abs_square_le_1)
-  have "?A1 \<inter> ?A2 = {x. abs x \<le> 1} \<times> {0}" by (auto simp: norm_Pair field_simps sq_le_1_iff)
-  also have "... \<in> null_sets lborel"
-    by (subst lborel_prod[symmetric]) (auto simp: lborel.emeasure_pair_measure_Times)
-  finally have "emeasure lborel ?A = emeasure lborel ?A1 + emeasure lborel ?A2"
-    by (subst A12, rule plus_emeasure'[OF A1_in_sets A2_in_sets, symmetric])
-
-  also have "emeasure lborel ?A1 = \<integral>\<^sup>+x. \<integral>\<^sup>+y. indicator ?A1 (x,y) \<partial>lborel \<partial>lborel"
-    by (subst lborel_prod[symmetric], subst lborel.emeasure_pair_measure)
-       (simp_all only: lborel_prod A1_in_sets)
-  also have "emeasure lborel ?A2 = \<integral>\<^sup>+x. \<integral>\<^sup>+y. indicator ?A2 (x,y) \<partial>lborel \<partial>lborel"
-    by (subst lborel_prod[symmetric], subst lborel.emeasure_pair_measure)
-       (simp_all only: lborel_prod A2_in_sets)
-  also have "distr lborel lborel uminus = (lborel :: real measure)"
-    by (subst (3) lborel_real_affine[of "-1" 0])
-       (simp_all add: one_ereal_def[symmetric] density_1 cong: distr_cong)
-  hence "(\<integral>\<^sup>+x. \<integral>\<^sup>+y. indicator ?A2 (x,y) \<partial>lborel \<partial>lborel) =
-             \<integral>\<^sup>+x. \<integral>\<^sup>+y. indicator ?A2 (x,y) \<partial>distr lborel lborel uminus \<partial>lborel" by simp
-  also have "... = \<integral>\<^sup>+x. \<integral>\<^sup>+y. indicator ?A2 (x,-y) \<partial>lborel \<partial>lborel"
-    apply (intro nn_integral_cong nn_integral_distr, simp)
-    apply (intro measurable_compose[OF _ borel_measurable_indicator[OF A2_in_sets]], simp)
-    done
-  also have "... = \<integral>\<^sup>+x. \<integral>\<^sup>+y. indicator ?A1 (x,y) \<partial>lborel \<partial>lborel"
-    by (intro nn_integral_cong) (auto split: split_indicator simp: norm_Pair)
-  also have "... + ... = (1+1) * ..." by (subst ring_distribs) simp_all
-  also have "... = \<integral>\<^sup>+x. 2 * \<integral>\<^sup>+y. indicator ?A1 (x,y) \<partial>lborel \<partial>lborel"
-    by (subst nn_integral_cmult) simp_all
-  also {
-    fix x y :: real assume "x \<notin> {-1..1}"
-    hence "abs x > 1" by auto
-    also have "norm (x,y) \<ge> abs x" by (simp add: norm_Pair)
-    finally have "(x,y) \<notin> ?A1" by auto
-  }
-  hence "... = \<integral>\<^sup>+x. 2 * (\<integral>\<^sup>+y. indicator ?A1 (x,y) \<partial>lborel) * indicator {-1..1} x \<partial>lborel"
-    by (intro nn_integral_cong) (auto split: split_indicator)
-  also {
-    fix x :: real assume "x \<in> {-1..1}"
-    hence x: "1 - x\<^sup>2 \<ge> 0" by (simp add: field_simps sq_le_1_iff abs_real_def)
-    have "\<And>y. (y::real) \<ge> 0 \<Longrightarrow> norm (x,y) \<le> 1 \<longleftrightarrow> y \<le> sqrt (1-x\<^sup>2)"
-      by (subst (5) real_sqrt_square[symmetric], simp, subst real_sqrt_le_iff)
-         (simp_all add: norm_Pair field_simps)
-    hence "(\<integral>\<^sup>+y. indicator ?A1 (x,y) \<partial>lborel) = (\<integral>\<^sup>+y. indicator {0..sqrt (1-x\<^sup>2)} y \<partial>lborel)"
-      by (intro nn_integral_cong) (auto split: split_indicator)
-    also from x have "... = sqrt (1-x\<^sup>2)" using x by simp
-    finally have "(\<integral>\<^sup>+y. indicator ?A1 (x,y) \<partial>lborel) = sqrt (1-x\<^sup>2)" .
-  }
-  hence "(\<integral>\<^sup>+x. 2 * (\<integral>\<^sup>+y. indicator ?A1 (x,y) \<partial>lborel) * indicator {-1..1} x \<partial>lborel) =
-            \<integral>\<^sup>+x. 2 * sqrt (1-x\<^sup>2) * indicator {-1..1} x \<partial>lborel"
-    by (intro nn_integral_cong) (simp split: split_indicator add: ennreal_mult')
-  also have A: "\<And>x. -1 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> \<not>x^2 > (1::real)"
-    by (subst not_less, subst sq_le_1_iff) (simp add: abs_real_def)
-  have "integrable lborel (\<lambda>x. 2 * sqrt (1-x\<^sup>2) * indicator {-1..1::real} x)"
-    by (intro borel_integrable_atLeastAtMost continuous_intros)
-  hence "(\<integral>\<^sup>+x. 2 * sqrt (1-x\<^sup>2) * indicator {-1..1} x \<partial>lborel) =
-             ennreal (\<integral>x. 2 * sqrt (1-x\<^sup>2) * indicator {-1..1} x \<partial>lborel)"
-    by (intro nn_integral_eq_integral AE_I2)
-       (auto split: split_indicator simp: field_simps sq_le_1_iff)
-  also have "(\<integral>x. 2 * sqrt (1-x\<^sup>2) * indicator {-1..1} x \<partial>lborel) =
-               LBINT x:{-1..1}. 2 * sqrt (1-x\<^sup>2)" by (simp add: field_simps)
-  also have "... = LBINT x=-1..1. 2 * sqrt (1-x\<^sup>2)"
-    by (subst interval_integral_Icc[symmetric]) (simp_all add: one_ereal_def)
-  also have "... = pi" by (rule unit_circle_area_aux)
-  finally show ?thesis .
-qed
-
-lemma circle_area:
-  assumes "R \<ge> 0"
-  shows   "emeasure lborel {z::real\<times>real. norm z \<le> R} = R^2 * pi" (is "emeasure _ ?A = _")
-proof (cases "R = 0")
-  assume "R \<noteq> 0"
-  with assms have R: "R > 0" by simp
-  let ?A' = "{z::real\<times>real. norm z \<le> 1}"
-  have "emeasure lborel ?A = \<integral>\<^sup>+x. \<integral>\<^sup>+y. indicator ?A (x,y) \<partial>lborel \<partial>lborel"
-    by (subst lborel_prod[symmetric], subst lborel.emeasure_pair_measure, subst lborel_prod)
-       simp_all
-  also have "... = \<integral>\<^sup>+x. R * \<integral>\<^sup>+y. indicator ?A (x,R*y) \<partial>lborel \<partial>lborel"
-  proof (rule nn_integral_cong)
-    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"
-      by (subst nn_integral_real_affine[OF _ \<open>R \<noteq> 0\<close>, of _ 0]) simp_all
-  qed
-  also have "... = R * \<integral>\<^sup>+x. \<integral>\<^sup>+y. indicator ?A (x,R*y) \<partial>lborel \<partial>lborel"
-    using R by (intro nn_integral_cmult) simp_all
-  also from R have "(\<integral>\<^sup>+x. \<integral>\<^sup>+y. indicator ?A (x,R*y) \<partial>lborel \<partial>lborel) =
-                        R * \<integral>\<^sup>+x. \<integral>\<^sup>+y. indicator ?A (R*x,R*y) \<partial>lborel \<partial>lborel"
-    by (subst nn_integral_real_affine[OF _ \<open>R \<noteq> 0\<close>, of _ 0]) simp_all
-  also {
-    fix x y
-    have A: "(R*x, R*y) = R *\<^sub>R (x,y)" by simp
-    from R have "norm (R*x, R*y) = R * norm (x,y)" by (subst A, subst norm_scaleR) simp_all
-    with R have "(R*x, R*y) \<in> ?A \<longleftrightarrow> (x, y) \<in> ?A'" by (auto simp: field_simps)
-  }
-  hence "(\<integral>\<^sup>+x. \<integral>\<^sup>+y. indicator ?A (R*x,R*y) \<partial>lborel \<partial>lborel) =
-               \<integral>\<^sup>+x. \<integral>\<^sup>+y. indicator ?A' (x,y) \<partial>lborel \<partial>lborel"
-    by (intro nn_integral_cong) (simp split: split_indicator)
-  also have "... = emeasure lborel ?A'"
-    by (subst lborel_prod[symmetric], subst lborel.emeasure_pair_measure, subst lborel_prod)
-       simp_all
-  also have "... = pi" by (rule unit_circle_area)
-  finally show ?thesis using assms by (simp add: power2_eq_square ennreal_mult mult_ac)
-qed simp
-
-end
diff -r 7dda4a667e40 -r c60e3d615b8c src/HOL/ROOT
--- a/src/HOL/ROOT	Sun Dec 24 14:46:26 2017 +0100
+++ b/src/HOL/ROOT	Sun Dec 24 14:28:10 2017 +0100
@@ -69,7 +69,6 @@
 session "HOL-Analysis-ex" in "Analysis/ex" = "HOL-Analysis" +
   theories
     Approximations
-    Circle_Area
 
 session "HOL-Computational_Algebra" (main timing) in "Computational_Algebra" = "HOL-Library" +
   theories