# HG changeset patch # User eberlm # 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 \The volume of an $n$-ball\ +theory Ball_Volume + imports Gamma_Function Lebesgue_Integral_Substitution +begin + +text \ + 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. +\ +definition unit_ball_vol :: "real \ real" where + "unit_ball_vol n = pi powr (n / 2) / Gamma (n / 2 + 1)" + +lemma unit_ball_vol_nonneg [simp]: "n \ 0 \ unit_ball_vol n \ 0" + by (auto simp add: unit_ball_vol_def intro!: divide_nonneg_pos Gamma_real_pos) + +text \ + 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. +\ +lemma emeasure_cball_aux_integral: + "(\\<^sup>+x. indicator {-1..1} x * sqrt (1 - x\<^sup>2) ^ n \lborel) = + ennreal (Beta (1 / 2) (real n / 2 + 1))" +proof - + have "((\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 (\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 "\ = (\\<^sup>+ x. ennreal (x\<^sup>2 powr - (1 / 2) * (1 - x\<^sup>2) powr (real n / 2) * (2 * x) * + indicator {0..1} x) \lborel)" + by (subst nn_integral_substitution[where g = "\x. x ^ 2" and g' = "\x. 2 * x"]) + (auto intro!: derivative_eq_intros continuous_intros) + also have "\ = (\\<^sup>+ x. 2 * ennreal ((1 - x\<^sup>2) powr (real n / 2) * indicator {0..1} x) \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 "\ = (\\<^sup>+ x. ennreal ((1 - x\<^sup>2) powr (real n / 2) * indicator {0..1} x) \lborel) + + (\\<^sup>+ x. ennreal ((1 - x\<^sup>2) powr (real n / 2) * indicator {0..1} x) \lborel)" + (is "_ = ?I + _") by (simp add: mult_2 nn_integral_add) + also have "?I = (\\<^sup>+ x. ennreal ((1 - x\<^sup>2) powr (real n / 2) * indicator {-1..0} x) \lborel)" + by (subst nn_integral_real_affine[of _ "-1" 0]) + (auto simp: indicator_def intro!: nn_integral_cong) + hence "?I + ?I = \ + ?I" by simp + also have "\ = (\\<^sup>+ x. ennreal ((1 - x\<^sup>2) powr (real n / 2) * + (indicator {-1..0} x + indicator{0..1} x)) \lborel)" + by (subst nn_integral_add [symmetric]) (auto simp: algebra_simps) + also have "\ = (\\<^sup>+ x. ennreal ((1 - x\<^sup>2) powr (real n / 2) * indicator {-1..1} x) \lborel)" + by (intro nn_integral_cong_AE AE_I[of _ _ "{0}"]) (auto simp: indicator_def) + also have "\ = (\\<^sup>+ x. ennreal (indicator {-1..1} x * sqrt (1 - x\<^sup>2) ^ n) \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 \ 0 \ y \ 0 \ sqrt x \ y \ x \ y ^ 2" + using real_le_lsqrt sqrt_le_D by blast + +lemma power2_le_iff_abs_le: "y \ 0 \ (x::real) ^ 2 \ y ^ 2 \ abs x \ y" + by (subst real_sqrt_le_iff' [symmetric]) auto + +text \ + 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. +\ +lemma emeasure_cball_aux: + assumes "finite A" "r > 0" + shows "emeasure (Pi\<^sub>M A (\_. lborel)) + ({f. sqrt (\i\A. (f i)\<^sup>2) \ r} \ space (Pi\<^sub>M A (\_. 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 "\_. lborel" + by standard + have "emeasure (Pi\<^sub>M (insert i A) (\_. lborel)) + ({f. sqrt (\i\insert i A. (f i)\<^sup>2) \ r} \ space (Pi\<^sub>M (insert i A) (\_. lborel))) = + nn_integral (Pi\<^sub>M (insert i A) (\_. lborel)) + (indicator ({f. sqrt (\i\insert i A. (f i)\<^sup>2) \ r} \ + space (Pi\<^sub>M (insert i A) (\_. lborel))))" + by (subst nn_integral_indicator) auto + also have "\ = (\\<^sup>+ y. \\<^sup>+ x. indicator ({f. sqrt ((f i)\<^sup>2 + (\i\A. (f i)\<^sup>2)) \ r} \ + space (Pi\<^sub>M (insert i A) (\_. lborel))) (x(i := y)) + \Pi\<^sub>M A (\_. lborel) \lborel)" + using insert.prems insert.hyps by (subst product_nn_integral_insert_rev) auto + also have "\ = (\\<^sup>+ (y::real). \\<^sup>+ x. indicator {-r..r} y * indicator ({f. sqrt ((\i\A. (f i)\<^sup>2)) \ + sqrt (r ^ 2 - y ^ 2)} \ space (Pi\<^sub>M A (\_. lborel))) x \Pi\<^sub>M A (\_. lborel) \lborel)" + proof (intro nn_integral_cong, goal_cases) + case (1 y f) + have *: "y \ {-r..r}" if "y ^ 2 + c \ r ^ 2" "c \ 0" for c + proof - + have "y ^ 2 \ y ^ 2 + c" using that by simp + also have "\ \ r ^ 2" by fact + finally show ?thesis + using \r > 0\ by (simp add: power2_le_iff_abs_le abs_if split: if_splits) + qed + have "(\x\A. (if x = i then y else f x)\<^sup>2) = (\x\A. (f x)\<^sup>2)" + using insert.hyps by (intro sum.cong) auto + thus ?case using 1 \r > 0\ + by (auto simp: sum_nonneg real_sqrt_le_iff' indicator_def PiE_def space_PiM dest!: *) + qed + also have "\ = (\\<^sup>+ (y::real). indicator {-r..r} y * (\\<^sup>+ x. indicator ({f. sqrt ((\i\A. (f i)\<^sup>2)) + \ sqrt (r ^ 2 - y ^ 2)} \ space (Pi\<^sub>M A (\_. lborel))) x + \Pi\<^sub>M A (\_. lborel)) \lborel)" by (subst nn_integral_cmult) auto + also have "\ = (\\<^sup>+ (y::real). indicator {-r..r} y * emeasure (PiM A (\_. lborel)) + ({f. sqrt ((\i\A. (f i)\<^sup>2)) \ sqrt (r ^ 2 - y ^ 2)} \ space (Pi\<^sub>M A (\_. lborel))) \lborel)" + using \finite A\ by (intro nn_integral_cong, subst nn_integral_indicator) auto + also have "\ = (\\<^sup>+ (y::real). indicator {-r..r} y * ennreal (unit_ball_vol (real (card A)) * + (sqrt (r ^ 2 - y ^ 2)) ^ card A) \lborel)" + proof (intro nn_integral_cong_AE, goal_cases) + case 1 + have "AE y in lborel. y \ {-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 \ {-r<..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 "\ = ennreal (unit_ball_vol (real (card A))) * + (\\<^sup>+ (y::real). indicator {-r..r} y * (sqrt (r ^ 2 - y ^ 2)) ^ card A \lborel)" + by (subst nn_integral_cmult [symmetric]) + (auto simp: mult_ac ennreal_mult' [symmetric] indicator_def intro!: nn_integral_cong) + also have "(\\<^sup>+ (y::real). indicator {-r..r} y * (sqrt (r ^ 2 - y ^ 2)) ^ card A \lborel) = + (\\<^sup>+ (y::real). r ^ card A * indicator {-1..1} y * (sqrt (1 - y ^ 2)) ^ card A + \(distr lborel borel (op * (1/r))))" using \r > 0\ + by (subst nn_integral_distr) + (auto simp: indicator_def field_simps real_sqrt_divide intro!: nn_integral_cong) + also have "\ = (\\<^sup>+ x. ennreal (r ^ Suc (card A)) * + (indicator {- 1..1} x * sqrt (1 - x\<^sup>2) ^ card A) \lborel)" using \r > 0\ + by (subst lborel_distr_mult) (auto simp: nn_integral_density ennreal_mult' [symmetric] mult_ac) + also have "\ = ennreal (r ^ Suc (card A)) * (\\<^sup>+ x. indicator {- 1..1} x * + sqrt (1 - x\<^sup>2) ^ card A \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 \r > 0\ 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 \ + We now get the main theorem very easily by just applying the above lemma. +\ +context + fixes c :: "'a :: euclidean_space" and r :: real + assumes r: "r \ 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 (\_. lborel)) borel (\f. \b\Basis. f b *\<^sub>R b)" + by (rule lborel_eq) + also have "emeasure \ (cball 0 r) = + emeasure (Pi\<^sub>M Basis (\_. lborel)) + ({y. dist 0 (\b\Basis. y b *\<^sub>R b :: 'a) \ r} \ space (Pi\<^sub>M Basis (\_. lborel)))" + by (subst emeasure_distr) (auto simp: cball_def) + also have "{f. dist 0 (\b\Basis. f b *\<^sub>R b :: 'a) \ r} = {f. sqrt (\i\Basis. (f i)\<^sup>2) \ r}" + by (subst euclidean_dist_l2) (auto simp: L2_set_def) + also have "emeasure (Pi\<^sub>M Basis (\_. lborel)) (\ \ space (Pi\<^sub>M Basis (\_. 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 (\x. c + x)) (cball c r)" + by (subst emeasure_distr) (auto simp: cball_def dist_norm norm_minus_commute) + also have "distr lborel borel (\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 \ null_sets lborel" + by (auto simp: null_sets_completion_iff negligible_iff_null_sets negligible_convex_frontier) + hence "emeasure lborel (ball c r \ sphere c r :: 'a set) = emeasure lborel (ball c r :: 'a set)" + by (intro emeasure_Un_null_set) auto + also have "ball c r \ sphere c r = (cball c r :: 'a set)" by auto + also have "emeasure lborel \ = 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 \ + Lastly, we now prove some nicer explicit formulas for the volume of the unit balls in + the cases of even and odd integer dimensions. +\ +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) / \ = 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)) = \" . + 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 / \ = (2 ^ (2 * Suc n) * fact (Suc n)) / fact (2 * Suc n) * pi ^ n" + by simp + finally show "unit_ball_vol (real (2 * n + 1)) = \" . +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 \ = 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 \ = 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 \ + Just for fun, we compute the volume of unit balls for a few dimensions. +\ +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 \ 0 \ content (ball c r :: (real ^ 2) set) = r ^ 2 * pi" + by (simp add: content_ball unit_ball_vol_2) + +corollary sphere_volume: "r \ 0 \ 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 \ measurable M borel" "g \ measurable M borel" + shows "(\x. f x powr g x :: real) \ measurable M borel" + using assms by (simp_all add: powr_def) + lemma measurable_of_bool[measurable]: "of_bool \ count_space UNIV \\<^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 \ measurable borel borel" +proof - + have *: "Ln (-of_real x) = of_real (ln x) + \ * 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)) + \ * pi" if "x < 0" for x + using *[of "-x"] that by simp + have cont: "set_borel_measurable borel (- \\<^sub>\\<^sub>0) Ln" + by (intro borel_measurable_continuous_on_indicator continuous_intros) auto + have "(\x. if x \ \\<^sub>\\<^sub>0 then ln (-Re x) + \ * pi else indicator (-\\<^sub>\\<^sub>0) x *\<^sub>R Ln x) \ borel \\<^sub>M borel" + (is "?f \ _") by (rule measurable_If_set[OF _ cont]) auto + hence "(\x. if x = 0 then Ln 0 else ?f x) \ borel \\<^sub>M borel" by measurable + also have "(\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 \ measurable M borel" "g \ measurable M borel" + shows "(\x. f x powr g x :: complex) \ measurable M borel" + using assms by (simp add: powr_def) + subsection\Relation between Ln and Arg, and hence continuity of Arg\ 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) \ Gamma x > 0" +lemma Gamma_real_pos [simp, intro]: "x > (0::real) \ Gamma x > 0" + by (simp add: Gamma_real_pos_exp) + +lemma Gamma_real_nonneg [simp, intro]: "x > (0::real) \ Gamma x \ 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 (\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} (\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) \ C" if "x \ {0..1/2}" for x + proof (cases "b < 1") + case False + with that have "(1 - x) powr (b - 1) \ (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) \ D" if "x \ {1/2..1}" for x + proof (cases "a < 1") + case False + with that have "x powr (a - 1) \ (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 \ 0" "D \ 0" by (simp_all add: C_def D_def) + + have I1: "set_integrable lborel {0..1 / 2} (\t. t powr (a - 1) * (1 - t) powr (b - 1))" + proof (rule Bochner_Integration.integrable_bound[OF _ _ AE_I2]) + have "(\t. t powr (a - 1)) integrable_on {0..1 / 2}" + by (rule integrable_on_powr_from_0) (use assms in auto) + hence "(\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} (\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) \ x powr (a - 1) * C" if "x \ {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))) \ + 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} (\t. t powr (a - 1) * (1 - t) powr (b - 1))" + proof (rule Bochner_Integration.integrable_bound[OF _ _ AE_I2]) + have "(\t. t powr (b - 1)) integrable_on {0..1/2}" + by (rule integrable_on_powr_from_0) (use assms in auto) + hence "(\t. t powr (b - 1)) integrable_on (cbox 0 (1/2))" by simp + from integrable_affinity[OF this, of "-1" 1] + have "(\t. (1 - t) powr (b - 1)) integrable_on {1/2..1}" by simp + hence "(\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} (\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) \ D * (1 - x) powr (b - 1)" if "x \ {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))) \ + 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} \ {1/2..1}) (\t. t powr (a - 1) * (1 - t) powr (b - 1))" + by (intro set_integrable_Un I1 I2) auto + also have "{0..1/2} \ {1/2..1} = {0..(1::real)}" by auto + finally show ?thesis . +qed + +lemma integrable_Beta': + assumes "a > 0" "b > (0::real)" + shows "(\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 "((\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} (\x. x powr (a - 1) * (1 - x) powr (b - 1))" + have [simp]: "B \ 0" unfolding B_def using a b + by (intro integral_nonneg integrable_Beta') auto + from a b have "ennreal (Gamma a * Gamma b) = + (\\<^sup>+ t. ennreal (indicator {0..} t * t powr (a - 1) / exp t) \lborel) * + (\\<^sup>+ t. ennreal (indicator {0..} t * t powr (b - 1) / exp t) \lborel)" + by (subst ennreal_mult') (simp_all add: Gamma_conv_nn_integral_real) + also have "\ = (\\<^sup>+t. \\<^sup>+u. ennreal (indicator {0..} t * t powr (a - 1) / exp t) * + ennreal (indicator {0..} u * u powr (b - 1) / exp u) \lborel \lborel)" + by (simp add: nn_integral_cmult nn_integral_multc) + also have "\ = (\\<^sup>+t. \\<^sup>+u. ennreal (indicator ({0..}\{0..}) (t,u) * t powr (a - 1) * u powr (b - 1) + / exp (t + u)) \lborel \lborel)" + by (intro nn_integral_cong) + (auto simp: indicator_def divide_ennreal ennreal_mult' [symmetric] exp_add) + also have "\ = (\\<^sup>+t. \\<^sup>+u. ennreal (indicator ({0..}\{t..}) (t,u) * t powr (a - 1) * + (u - t) powr (b - 1) / exp u) \lborel \lborel)" + proof (rule nn_integral_cong, goal_cases) + case (1 t) + have "(\\<^sup>+u. ennreal (indicator ({0..}\{0..}) (t,u) * t powr (a - 1) * + u powr (b - 1) / exp (t + u)) \distr lborel borel (op + (-t))) = + (\\<^sup>+u. ennreal (indicator ({0..}\{t..}) (t,u) * t powr (a - 1) * + (u - t) powr (b - 1) / exp u) \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 "\ = (\\<^sup>+u. \\<^sup>+t. ennreal (indicator ({0..}\{t..}) (t,u) * t powr (a - 1) * + (u - t) powr (b - 1) / exp u) \lborel \lborel)" + by (subst lborel_pair.Fubini') + (auto simp: case_prod_unfold indicator_def cong: measurable_cong_sets) + also have "\ = (\\<^sup>+u. \\<^sup>+t. ennreal (indicator {0..u} t * t powr (a - 1) * (u - t) powr (b - 1)) * + ennreal (indicator {0..} u / exp u) \lborel \lborel)" + by (intro nn_integral_cong) (auto simp: indicator_def ennreal_mult' [symmetric]) + also have "\ = (\\<^sup>+u. (\\<^sup>+t. ennreal (indicator {0..u} t * t powr (a - 1) * (u - t) powr (b - 1)) + \lborel) * ennreal (indicator {0..} u / exp u) \lborel)" + by (subst nn_integral_multc [symmetric]) auto + also have "\ = (\\<^sup>+u. (\\<^sup>+t. ennreal (indicator {0..u} t * t powr (a - 1) * (u - t) powr (b - 1)) + \lborel) * ennreal (indicator {0<..} u / exp u) \lborel)" + by (intro nn_integral_cong_AE eventually_mono[OF AE_lborel_singleton[of 0]]) + (auto simp: indicator_def) + also have "\ = (\\<^sup>+u. ennreal B * ennreal (indicator {0..} u / exp u * u powr (a + b - 1)) \lborel)" + proof (intro nn_integral_cong, goal_cases) + case (1 u) + show ?case + proof (cases "u > 0") + case True + have "(\\<^sup>+t. ennreal (indicator {0..u} t * t powr (a - 1) * (u - t) powr (b - 1)) \lborel) = + (\\<^sup>+t. ennreal (indicator {0..1} t * (u * t) powr (a - 1) * (u - u * t) powr (b - 1)) + \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 (\_. u)" + using \u > 0\ by (subst lborel_distr_mult) auto + also have "nn_integral \ ?f = (\\<^sup>+x. ennreal (indicator {0..1} x * (u * (u * x) powr (a - 1) * + (u * (1 - x)) powr (b - 1))) \lborel)" using \u > 0\ + by (subst nn_integral_density) (auto simp: ennreal_mult' [symmetric] algebra_simps) + also have "\ = (\\<^sup>+x. ennreal (u powr (a + b - 1)) * + ennreal (indicator {0..1} x * x powr (a - 1) * + (1 - x) powr (b - 1)) \lborel)" using \u > 0\ a b + by (intro nn_integral_cong) + (auto simp: indicator_def powr_mult powr_add powr_diff mult_ac ennreal_mult' [symmetric]) + also have "\ = ennreal (u powr (a + b - 1)) * + (\\<^sup>+x. ennreal (indicator {0..1} x * x powr (a - 1) * + (1 - x) powr (b - 1)) \lborel)" + by (subst nn_integral_cmult) auto + also have "((\x. x powr (a - 1) * (1 - x) powr (b - 1)) has_integral + integral {0..1} (\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 "(\\<^sup>+x. ennreal (indicator {0..1} x * x powr (a - 1) * + (1 - x) powr (b - 1)) \lborel) = B" by (simp add: mult_ac B_def) + finally show ?thesis using \u > 0\ by (simp add: ennreal_mult' [symmetric] mult_ac) + qed auto + qed + also have "\ = ennreal B * ennreal (Gamma (a + b))" + using a b by (subst nn_integral_cmult) (auto simp: Gamma_conv_nn_integral_real) + also have "\ = 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 "(\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 \The Weierstraß product formula for the sine\ 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\. -*) - -section \The area of a circle\ - -theory Circle_Area -imports Complex_Main "HOL-Analysis.Interval_Integral" -begin - -lemma plus_emeasure': - assumes "A \ sets M" "B \ sets M" "A \ B \ null_sets M" - shows "emeasure M A + emeasure M B = emeasure M (A \ B)" -proof- - let ?C = "A \ B" - have "A \ B = A \ (B - ?C)" by blast - with assms have "emeasure M (A \ 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 \ 0 \ 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 \ {-pi/2<.. 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 = "\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\real. norm z \ 1} = pi" (is "emeasure _ ?A = _") -proof- - let ?A1 = "{(x,y)\?A. y \ 0}" and ?A2 = "{(x,y)\?A. y \ 0}" - have [measurable]: "(\x. snd (x :: real \ real)) \ measurable borel borel" - by (simp add: borel_prod[symmetric]) - - have "?A1 = ?A \ {x\space lborel. snd x \ 0}" by auto - also have "?A \ {x\space lborel. snd x \ 0} \ sets borel" - by (intro sets.Int pred_Collect_borel) simp_all - finally have A1_in_sets: "?A1 \ sets lborel" by (subst sets_lborel) - - have "?A2 = ?A \ {x\space lborel. snd x \ 0}" by auto - also have "... \ sets borel" - by (intro sets.Int pred_Collect_borel) simp_all - finally have A2_in_sets: "?A2 \ sets lborel" by (subst sets_lborel) - - have A12: "?A = ?A1 \ ?A2" by auto - have sq_le_1_iff: "\x. x\<^sup>2 \ 1 \ abs (x::real) \ 1" - by (simp add: abs_square_le_1) - have "?A1 \ ?A2 = {x. abs x \ 1} \ {0}" by (auto simp: norm_Pair field_simps sq_le_1_iff) - also have "... \ 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 = \\<^sup>+x. \\<^sup>+y. indicator ?A1 (x,y) \lborel \lborel" - by (subst lborel_prod[symmetric], subst lborel.emeasure_pair_measure) - (simp_all only: lborel_prod A1_in_sets) - also have "emeasure lborel ?A2 = \\<^sup>+x. \\<^sup>+y. indicator ?A2 (x,y) \lborel \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 "(\\<^sup>+x. \\<^sup>+y. indicator ?A2 (x,y) \lborel \lborel) = - \\<^sup>+x. \\<^sup>+y. indicator ?A2 (x,y) \distr lborel lborel uminus \lborel" by simp - also have "... = \\<^sup>+x. \\<^sup>+y. indicator ?A2 (x,-y) \lborel \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 "... = \\<^sup>+x. \\<^sup>+y. indicator ?A1 (x,y) \lborel \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 "... = \\<^sup>+x. 2 * \\<^sup>+y. indicator ?A1 (x,y) \lborel \lborel" - by (subst nn_integral_cmult) simp_all - also { - fix x y :: real assume "x \ {-1..1}" - hence "abs x > 1" by auto - also have "norm (x,y) \ abs x" by (simp add: norm_Pair) - finally have "(x,y) \ ?A1" by auto - } - hence "... = \\<^sup>+x. 2 * (\\<^sup>+y. indicator ?A1 (x,y) \lborel) * indicator {-1..1} x \lborel" - by (intro nn_integral_cong) (auto split: split_indicator) - also { - fix x :: real assume "x \ {-1..1}" - hence x: "1 - x\<^sup>2 \ 0" by (simp add: field_simps sq_le_1_iff abs_real_def) - have "\y. (y::real) \ 0 \ norm (x,y) \ 1 \ y \ 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 "(\\<^sup>+y. indicator ?A1 (x,y) \lborel) = (\\<^sup>+y. indicator {0..sqrt (1-x\<^sup>2)} y \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 "(\\<^sup>+y. indicator ?A1 (x,y) \lborel) = sqrt (1-x\<^sup>2)" . - } - hence "(\\<^sup>+x. 2 * (\\<^sup>+y. indicator ?A1 (x,y) \lborel) * indicator {-1..1} x \lborel) = - \\<^sup>+x. 2 * sqrt (1-x\<^sup>2) * indicator {-1..1} x \lborel" - by (intro nn_integral_cong) (simp split: split_indicator add: ennreal_mult') - also have A: "\x. -1 \ x \ x \ 1 \ \x^2 > (1::real)" - by (subst not_less, subst sq_le_1_iff) (simp add: abs_real_def) - have "integrable lborel (\x. 2 * sqrt (1-x\<^sup>2) * indicator {-1..1::real} x)" - by (intro borel_integrable_atLeastAtMost continuous_intros) - hence "(\\<^sup>+x. 2 * sqrt (1-x\<^sup>2) * indicator {-1..1} x \lborel) = - ennreal (\x. 2 * sqrt (1-x\<^sup>2) * indicator {-1..1} x \lborel)" - by (intro nn_integral_eq_integral AE_I2) - (auto split: split_indicator simp: field_simps sq_le_1_iff) - also have "(\x. 2 * sqrt (1-x\<^sup>2) * indicator {-1..1} x \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 \ 0" - shows "emeasure lborel {z::real\real. norm z \ R} = R^2 * pi" (is "emeasure _ ?A = _") -proof (cases "R = 0") - assume "R \ 0" - with assms have R: "R > 0" by simp - let ?A' = "{z::real\real. norm z \ 1}" - have "emeasure lborel ?A = \\<^sup>+x. \\<^sup>+y. indicator ?A (x,y) \lborel \lborel" - by (subst lborel_prod[symmetric], subst lborel.emeasure_pair_measure, subst lborel_prod) - simp_all - also have "... = \\<^sup>+x. R * \\<^sup>+y. indicator ?A (x,R*y) \lborel \lborel" - proof (rule nn_integral_cong) - fix x from R show "(\\<^sup>+y. indicator ?A (x,y) \lborel) = R * \\<^sup>+y. indicator ?A (x,R*y) \lborel" - by (subst nn_integral_real_affine[OF _ \R \ 0\, of _ 0]) simp_all - qed - also have "... = R * \\<^sup>+x. \\<^sup>+y. indicator ?A (x,R*y) \lborel \lborel" - using R by (intro nn_integral_cmult) simp_all - also from R have "(\\<^sup>+x. \\<^sup>+y. indicator ?A (x,R*y) \lborel \lborel) = - R * \\<^sup>+x. \\<^sup>+y. indicator ?A (R*x,R*y) \lborel \lborel" - by (subst nn_integral_real_affine[OF _ \R \ 0\, 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) \ ?A \ (x, y) \ ?A'" by (auto simp: field_simps) - } - hence "(\\<^sup>+x. \\<^sup>+y. indicator ?A (R*x,R*y) \lborel \lborel) = - \\<^sup>+x. \\<^sup>+y. indicator ?A' (x,y) \lborel \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