--- 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
--- /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
--- 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
--- 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>
--- 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>
--- 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
--- 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