# HG changeset patch # User paulson # Date 1523531794 -3600 # Node ID 75b94eb58c3d85d353d190ccc1e0baab7a91faa0 # Parent 27c8692825f6b1b2e6a2be59ce67b754f1596d53 Analysis builds using set_borel_measurable_def, etc. diff -r 27c8692825f6 -r 75b94eb58c3d src/HOL/Analysis/Ball_Volume.thy --- a/src/HOL/Analysis/Ball_Volume.thy Wed Apr 11 16:34:52 2018 +0100 +++ b/src/HOL/Analysis/Ball_Volume.thy Thu Apr 12 12:16:34 2018 +0100 @@ -43,7 +43,7 @@ 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) + (auto intro!: derivative_eq_intros continuous_intros simp: set_borel_measurable_def) 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) diff -r 27c8692825f6 -r 75b94eb58c3d src/HOL/Analysis/Complex_Transcendental.thy --- a/src/HOL/Analysis/Complex_Transcendental.thy Wed Apr 11 16:34:52 2018 +0100 +++ b/src/HOL/Analysis/Complex_Transcendental.thy Thu Apr 12 12:16:34 2018 +0100 @@ -1545,7 +1545,7 @@ 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" + have cont: "(\x. indicat_real (- \\<^sub>\\<^sub>0) x *\<^sub>R Ln x) \ borel_measurable borel" 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 diff -r 27c8692825f6 -r 75b94eb58c3d src/HOL/Analysis/Gamma_Function.thy --- a/src/HOL/Analysis/Gamma_Function.thy Wed Apr 11 16:34:52 2018 +0100 +++ b/src/HOL/Analysis/Gamma_Function.thy Thu Apr 12 12:16:34 2018 +0100 @@ -876,9 +876,9 @@ using of_nat_neq_0[of "2*n"] by (simp only: of_nat_Suc) (simp add: add_ac) hence nz': "of_nat n + (1/2::'a) \ 0" by (simp add: field_simps) have "Digamma (of_nat (Suc n) + 1/2 :: 'a) = Digamma (of_nat n + 1/2 + 1)" by simp - also from nz' have "\ = Digamma (of_nat n + 1 / 2) + 1 / (of_nat n + 1 / 2)" + also from nz' have "\ = Digamma (of_nat n + 1/2) + 1 / (of_nat n + 1/2)" by (rule Digamma_plus1) - also from nz nz' have "1 / (of_nat n + 1 / 2 :: 'a) = 2 / (2 * of_nat n + 1)" + also from nz nz' have "1 / (of_nat n + 1/2 :: 'a) = 2 / (2 * of_nat n + 1)" by (subst divide_eq_eq) simp_all also note Suc finally show ?case by (simp add: add_ac) @@ -2048,7 +2048,7 @@ from assms double_in_nonpos_Ints_imp[of z] have z': "2 * z \ \\<^sub>\\<^sub>0" by auto from fraction_not_in_ints[of 2 1] have "(1/2 :: 'a) \ \\<^sub>\\<^sub>0" by (intro not_in_Ints_imp_not_in_nonpos_Ints) simp_all - with lim[of "1/2 :: 'a"] have "?h \ 2 * Gamma (1 / 2 :: 'a)" by (simp add: exp_of_real) + with lim[of "1/2 :: 'a"] have "?h \ 2 * Gamma (1/2 :: 'a)" by (simp add: exp_of_real) from LIMSEQ_unique[OF this lim[OF assms]] z' show ?thesis by (simp add: divide_simps Gamma_eq_zero_iff ring_distribs exp_diff exp_of_real ac_simps) qed @@ -2735,11 +2735,12 @@ have "?f absolutely_integrable_on ({0<..x0} \ {x0..})" proof (rule set_integrable_Un) show "?f absolutely_integrable_on {0<..x0}" + unfolding set_integrable_def proof (rule Bochner_Integration.integrable_bound [OF _ _ AE_I2]) - show "set_integrable lebesgue {0<..x0} (\x. x powr (Re z - 1))" using x0(1) assms - by (intro nonnegative_absolutely_integrable_1 integrable_on_powr_from_0') auto - show "set_borel_measurable lebesgue {0<..x0} - (\x. complex_of_real x powr (z - 1) / complex_of_real (exp (a * x)))" + show "integrable lebesgue (\x. indicat_real {0<..x0} x *\<^sub>R x powr (Re z - 1))" + using x0(1) assms + by (intro nonnegative_absolutely_integrable_1 [unfolded set_integrable_def] integrable_on_powr_from_0') auto + show "(\x. indicat_real {0<..x0} x *\<^sub>R (x powr (z - 1) / exp (a * x))) \ borel_measurable lebesgue" by (intro measurable_completion) (auto intro!: borel_measurable_continuous_on_indicator continuous_intros) fix x :: real @@ -2751,11 +2752,11 @@ qed next show "?f absolutely_integrable_on {x0..}" + unfolding set_integrable_def proof (rule Bochner_Integration.integrable_bound [OF _ _ AE_I2]) - show "set_integrable lebesgue {x0..} (\x. exp (-(a/2) * x))" using assms - by (intro nonnegative_absolutely_integrable_1 integrable_on_exp_minus_to_infinity) auto - show "set_borel_measurable lebesgue {x0..} - (\x. complex_of_real x powr (z - 1) / complex_of_real (exp (a * x)))" using x0(1) + show "integrable lebesgue (\x. indicat_real {x0..} x *\<^sub>R exp (- (a / 2) * x))" using assms + by (intro nonnegative_absolutely_integrable_1 [unfolded set_integrable_def] integrable_on_exp_minus_to_infinity) auto + show "(\x. indicat_real {x0..} x *\<^sub>R (x powr (z - 1) / exp (a * x))) \ borel_measurable lebesgue" using x0(1) by (intro measurable_completion) (auto intro!: borel_measurable_continuous_on_indicator continuous_intros) fix x :: real @@ -3015,14 +3016,15 @@ 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))" + have I1: "set_integrable lborel {0..1/2} (\t. t powr (a - 1) * (1 - t) powr (b - 1))" + unfolding set_integrable_def proof (rule Bochner_Integration.integrable_bound[OF _ _ AE_I2]) - have "(\t. t powr (a - 1)) integrable_on {0..1 / 2}" + 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}" + 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))" + from integrable_mult_right[OF this [unfolded set_integrable_def], of C] + show "integrable lborel (\x. indicat_real {0..1/2} x *\<^sub>R (C * x powr (a - 1)))" by (subst (asm) integrable_completion) (auto simp: mult_ac) next fix x :: real @@ -3033,7 +3035,8 @@ 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))" + have I2: "set_integrable lborel {1/2..1} (\t. t powr (a - 1) * (1 - t) powr (b - 1))" + unfolding set_integrable_def 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) @@ -3042,8 +3045,8 @@ 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))" + from integrable_mult_right[OF this [unfolded set_integrable_def], of D] + show "integrable lborel (\x. indicat_real {1/2..1} x *\<^sub>R (D * (1 - x) powr (b - 1)))" by (subst (asm) integrable_completion) (auto simp: mult_ac) next fix x :: real @@ -3204,9 +3207,9 @@ proof - from tendsto_inverse[OF tendsto_mult[OF sin_product_formula_real[of "1/2"] tendsto_const[of "2/pi"]]] - have "(\n. (\k=1..n. inverse (1 - (1 / 2)\<^sup>2 / (real k)\<^sup>2))) \ pi/2" + have "(\n. (\k=1..n. inverse (1 - (1/2)\<^sup>2 / (real k)\<^sup>2))) \ pi/2" by (simp add: prod_inversef [symmetric]) - also have "(\n. (\k=1..n. inverse (1 - (1 / 2)\<^sup>2 / (real k)\<^sup>2))) = + also have "(\n. (\k=1..n. inverse (1 - (1/2)\<^sup>2 / (real k)\<^sup>2))) = (\n. (\k=1..n. (4*real k^2)/(4*real k^2 - 1)))" by (intro ext prod.cong refl) (simp add: divide_simps) finally show ?thesis . diff -r 27c8692825f6 -r 75b94eb58c3d src/HOL/Analysis/Lebesgue_Integral_Substitution.thy --- a/src/HOL/Analysis/Lebesgue_Integral_Substitution.thy Wed Apr 11 16:34:52 2018 +0100 +++ b/src/HOL/Analysis/Lebesgue_Integral_Substitution.thy Thu Apr 12 12:16:34 2018 +0100 @@ -74,10 +74,12 @@ (g has_vector_derivative g' x) (at x within {min u' v'..max u' v'})" by (simp only: u'v' max_absorb2 min_absorb1) (auto simp: has_field_derivative_iff_has_vector_derivative) - have "integrable lborel (\x. indicator ({a..b} \ g -` {u..v}) x *\<^sub>R g' x)" - by (rule set_integrable_subset[OF borel_integrable_atLeastAtMost'[OF contg']]) simp_all + have "integrable lborel (\x. indicator ({a..b} \ g -` {u..v}) x *\<^sub>R g' x)" + using set_integrable_subset borel_integrable_atLeastAtMost'[OF contg'] + by (metis \{u'..v'} \ {a..b}\ eucl_ivals(5) set_integrable_def sets_lborel u'v'(1)) hence "(\\<^sup>+x. ennreal (g' x) * indicator ({a..b} \ g-` {u..v}) x \lborel) = LBINT x:{a..b} \ g-`{u..v}. g' x" + unfolding set_lebesgue_integral_def by (subst nn_integral_eq_integral[symmetric]) (auto intro!: derivg_nonneg nn_integral_cong split: split_indicator) also from interval_integral_FTC_finite[OF A B] @@ -129,28 +131,29 @@ also have "... = \\<^sup>+ x. indicator (g-`A \ {a..b}) x * ennreal (g' x * indicator {a..b} x) \lborel" (is "_ = ?I") by (subst compl.IH, intro nn_integral_cong) (simp split: split_indicator) also have "g b - g a = LBINT x:{a..b}. g' x" using derivg' + unfolding set_lebesgue_integral_def by (intro integral_FTC_atLeastAtMost[symmetric]) (auto intro: continuous_on_subset[OF contg'] has_field_derivative_subset[OF derivg] has_vector_derivative_at_within) also have "ennreal ... = \\<^sup>+ x. g' x * indicator {a..b} x \lborel" - using borel_integrable_atLeastAtMost'[OF contg'] + using borel_integrable_atLeastAtMost'[OF contg'] unfolding set_lebesgue_integral_def by (subst nn_integral_eq_integral) - (simp_all add: mult.commute derivg_nonneg split: split_indicator) + (simp_all add: mult.commute derivg_nonneg set_integrable_def split: split_indicator) also have Mg'': "(\x. indicator (g -` A \ {a..b}) x * ennreal (g' x * indicator {a..b} x)) \ borel_measurable borel" using Mg' by (intro borel_measurable_times_ennreal borel_measurable_indicator) - (simp_all add: mult.commute) + (simp_all add: mult.commute set_borel_measurable_def) have le: "(\\<^sup>+x. indicator (g-`A \ {a..b}) x * ennreal (g' x * indicator {a..b} x) \lborel) \ (\\<^sup>+x. ennreal (g' x) * indicator {a..b} x \lborel)" by (intro nn_integral_mono) (simp split: split_indicator add: derivg_nonneg) note integrable = borel_integrable_atLeastAtMost'[OF contg'] with le have notinf: "(\\<^sup>+x. indicator (g-`A \ {a..b}) x * ennreal (g' x * indicator {a..b} x) \lborel) \ top" - by (auto simp: real_integrable_def nn_integral_set_ennreal mult.commute top_unique) + by (auto simp: real_integrable_def nn_integral_set_ennreal mult.commute top_unique set_integrable_def) have "(\\<^sup>+ x. g' x * indicator {a..b} x \lborel) - ?I = \\<^sup>+ x. ennreal (g' x * indicator {a..b} x) - indicator (g -` A \ {a..b}) x * ennreal (g' x * indicator {a..b} x) \lborel" apply (intro nn_integral_diff[symmetric]) - apply (insert Mg', simp add: mult.commute) [] + apply (insert Mg', simp add: mult.commute set_borel_measurable_def) [] apply (insert Mg'', simp) [] apply (simp split: split_indicator add: derivg_nonneg) apply (rule notinf) @@ -185,7 +188,7 @@ also have "(\i. ... i) = \\<^sup>+ x. (\i. ennreal (g' x * indicator {a..b} x) * indicator ({a..b} \ g -` f i) x) \lborel" using Mg' apply (intro nn_integral_suminf[symmetric]) - apply (rule borel_measurable_times_ennreal, simp add: mult.commute) + apply (rule borel_measurable_times_ennreal, simp add: mult.commute set_borel_measurable_def) apply (rule borel_measurable_indicator, subst sets_lborel) apply (simp_all split: split_indicator add: derivg_nonneg) done @@ -209,7 +212,7 @@ let ?I = "indicator {a..b}" have "(\x. f (g x * ?I x) * ennreal (g' x * ?I x)) \ borel_measurable borel" using Mg Mg' by (intro borel_measurable_times_ennreal measurable_compose[OF _ Mf]) - (simp_all add: mult.commute) + (simp_all add: mult.commute set_borel_measurable_def) also have "(\x. f (g x * ?I x) * ennreal (g' x * ?I x)) = (\x. f (g x) * ennreal (g' x) * ?I x)" by (intro ext) (simp split: split_indicator) finally have Mf': "(\x. f (g x) * ennreal (g' x) * ?I x) \ borel_measurable borel" . @@ -223,7 +226,7 @@ fix f :: "real \ ennreal" assume Mf: "f \ borel_measurable borel" have "(\x. f (g x * ?I x) * ennreal (g' x * ?I x)) \ borel_measurable borel" using Mg Mg' by (intro borel_measurable_times_ennreal measurable_compose[OF _ Mf]) - (simp_all add: mult.commute) + (simp_all add: mult.commute set_borel_measurable_def) also have "(\x. f (g x * ?I x) * ennreal (g' x * ?I x)) = (\x. f (g x) * ennreal (g' x) * ?I x)" by (intro ext) (simp split: split_indicator) finally have "(\x. f (g x) * ennreal (g' x) * ?I x) \ borel_measurable borel" . @@ -250,7 +253,7 @@ let ?I = "indicator {a..b}" have "(\x. F i (g x * ?I x) * ennreal (g' x * ?I x)) \ borel_measurable borel" using Mg Mg' by (rule_tac borel_measurable_times_ennreal, rule_tac measurable_compose[OF _ sup.hyps(1)]) - (simp_all add: mult.commute) + (simp_all add: mult.commute set_borel_measurable_def) also have "(\x. F i (g x * ?I x) * ennreal (g' x * ?I x)) = (\x. F i (g x) * ennreal (g' x) * ?I x)" by (intro ext) (simp split: split_indicator) finally have "... \ borel_measurable borel" . @@ -306,7 +309,7 @@ (auto split: split_indicator split_max simp: zero_ennreal.rep_eq ennreal_neg) also have "... = \\<^sup>+ x. ?f' (g x) * ennreal (g' x) * indicator {a..b} x \lborel" using Mf by (subst nn_integral_substitution_aux[OF _ _ derivg contg' derivg_nonneg \a < b\]) - (auto simp add: mult.commute) + (auto simp add: mult.commute set_borel_measurable_def) also have "... = \\<^sup>+ x. f (g x) * ennreal (g' x) * indicator {a..b} x \lborel" by (intro nn_integral_cong) (auto split: split_indicator simp: max_def dest: bounds) also have "... = \\<^sup>+x. ennreal (f (g x) * g' x * indicator {a..b} x) \lborel" @@ -334,13 +337,14 @@ (\x. ennreal (f x * indicator {g a..g b} x))" by (intro ext) (simp split: split_indicator) with integrable have M1: "(\x. f x * indicator {g a..g b} x) \ borel_measurable borel" - unfolding real_integrable_def by (force simp: mult.commute) + by (force simp: mult.commute set_integrable_def) from integrable have M2: "(\x. -f x * indicator {g a..g b} x) \ borel_measurable borel" - unfolding real_integrable_def by (force simp: mult.commute) + by (force simp: mult.commute set_integrable_def) have "LBINT x. (f x :: real) * indicator {g a..g b} x = enn2real (\\<^sup>+ x. ennreal (f x) * indicator {g a..g b} x \lborel) - enn2real (\\<^sup>+ x. ennreal (- (f x)) * indicator {g a..g b} x \lborel)" using integrable + unfolding set_integrable_def by (subst real_lebesgue_integral_def) (simp_all add: nn_integral_set_ennreal mult.commute) also have *: "(\\<^sup>+x. ennreal (f x) * indicator {g a..g b} x \lborel) = (\\<^sup>+x. ennreal (f x * indicator {g a..g b} x) \lborel)" @@ -348,32 +352,33 @@ also from M1 * have A: "(\\<^sup>+ x. ennreal (f x * indicator {g a..g b} x) \lborel) = (\\<^sup>+ x. ennreal (f (g x) * g' x * indicator {a..b} x) \lborel)" by (subst nn_integral_substitution[OF _ derivg contg' derivg_nonneg \a \ b\]) - (auto simp: nn_integral_set_ennreal mult.commute) + (auto simp: nn_integral_set_ennreal mult.commute set_borel_measurable_def) also have **: "(\\<^sup>+ x. ennreal (- (f x)) * indicator {g a..g b} x \lborel) = (\\<^sup>+ x. ennreal (- (f x) * indicator {g a..g b} x) \lborel)" by (intro nn_integral_cong) (simp split: split_indicator) also from M2 ** have B: "(\\<^sup>+ x. ennreal (- (f x) * indicator {g a..g b} x) \lborel) = (\\<^sup>+ x. ennreal (- (f (g x)) * g' x * indicator {a..b} x) \lborel)" by (subst nn_integral_substitution[OF _ derivg contg' derivg_nonneg \a \ b\]) - (auto simp: nn_integral_set_ennreal mult.commute) + (auto simp: nn_integral_set_ennreal mult.commute set_borel_measurable_def) also { from integrable have Mf: "set_borel_measurable borel {g a..g b} f" - unfolding real_integrable_def by simp - from borel_measurable_times[OF measurable_compose[OF Mg Mf] Mg'] - have "(\x. f (g x * indicator {a..b} x) * indicator {g a..g b} (g x * indicator {a..b} x) * + unfolding set_borel_measurable_def set_integrable_def by simp + from measurable_compose Mg Mf Mg' borel_measurable_times + have "(\x. f (g x * indicator {a..b} x) * indicator {g a..g b} (g x * indicator {a..b} x) * (g' x * indicator {a..b} x)) \ borel_measurable borel" (is "?f \ _") - by (simp add: mult.commute) + by (simp add: mult.commute set_borel_measurable_def) also have "?f = (\x. f (g x) * g' x * indicator {a..b} x)" using monog by (intro ext) (auto split: split_indicator) finally show "set_integrable lborel {a..b} (\x. f (g x) * g' x)" - using A B integrable unfolding real_integrable_def + using A B integrable unfolding real_integrable_def set_integrable_def by (simp_all add: nn_integral_set_ennreal mult.commute) } note integrable' = this have "enn2real (\\<^sup>+ x. ennreal (f (g x) * g' x * indicator {a..b} x) \lborel) - enn2real (\\<^sup>+ x. ennreal (-f (g x) * g' x * indicator {a..b} x) \lborel) = - (LBINT x. f (g x) * g' x * indicator {a..b} x)" using integrable' + (LBINT x. f (g x) * g' x * indicator {a..b} x)" + using integrable' unfolding set_integrable_def by (subst real_lebesgue_integral_def) (simp_all add: field_simps) finally show "(LBINT x. f x * indicator {g a..g b} x) = (LBINT x. f (g x) * g' x * indicator {a..b} x)" . @@ -391,11 +396,11 @@ apply (subst (1 2) interval_integral_Icc, fact) apply (rule deriv_nonneg_imp_mono[OF derivg derivg_nonneg], simp, simp, fact) using integral_substitution(2)[OF assms] - apply (simp add: mult.commute) + apply (simp add: mult.commute set_lebesgue_integral_def) done -lemma set_borel_integrable_singleton[simp]: - "set_integrable lborel {x} (f :: real \ real)" +lemma set_borel_integrable_singleton[simp]: "set_integrable lborel {x} (f :: real \ real)" + unfolding set_integrable_def by (subst integrable_discrete_difference[where X="{x}" and g="\_. 0"]) auto end