--- a/src/HOL/Analysis/Set_Integral.thy Thu Apr 12 12:16:34 2018 +0100
+++ b/src/HOL/Analysis/Set_Integral.thy Fri Apr 13 15:58:27 2018 +0100
@@ -67,6 +67,9 @@
by (subst (asm) sets_restrict_space_iff) (auto simp: space_restrict_space)
qed
+lemma set_lebesgue_integral_zero [simp]: "set_lebesgue_integral M A (\<lambda>x. 0) = 0"
+ by (auto simp: set_lebesgue_integral_def)
+
lemma set_lebesgue_integral_cong:
assumes "A \<in> sets M" and "\<forall>x. x \<in> A \<longrightarrow> f x = g x"
shows "(LINT x:A|M. f x) = (LINT x:A|M. g x)"
--- a/src/HOL/Probability/Characteristic_Functions.thy Thu Apr 12 12:16:34 2018 +0100
+++ b/src/HOL/Probability/Characteristic_Functions.thy Fri Apr 13 15:58:27 2018 +0100
@@ -274,7 +274,8 @@
have *: "\<And>a b. interval_lebesgue_integrable lborel a b f \<Longrightarrow> interval_lebesgue_integrable lborel a b g \<Longrightarrow>
\<bar>LBINT s=a..b. f s\<bar> \<le> \<bar>LBINT s=a..b. g s\<bar>"
if f: "\<And>s. 0 \<le> f s" and g: "\<And>s. f s \<le> g s" for f g :: "_ \<Rightarrow> real"
- using order_trans[OF f g] f g unfolding interval_lebesgue_integral_def interval_lebesgue_integrable_def
+ using order_trans[OF f g] f g
+ unfolding interval_lebesgue_integral_def interval_lebesgue_integrable_def set_lebesgue_integral_def set_integrable_def
by (auto simp: integral_nonneg_AE[OF AE_I2] intro!: integral_mono mult_mono)
have "iexp x - (\<Sum>k \<le> Suc n. (\<i> * x)^k / fact k) =
--- a/src/HOL/Probability/Conditional_Expectation.thy Thu Apr 12 12:16:34 2018 +0100
+++ b/src/HOL/Probability/Conditional_Expectation.thy Fri Apr 13 15:58:27 2018 +0100
@@ -739,7 +739,8 @@
proof -
have "A \<in> sets M" by (meson assms(2) subalg subalgebra_def subsetD)
have "integrable M (\<lambda>x. indicator A x * f x)" using integrable_mult_indicator[OF \<open>A \<in> sets M\<close> assms(1)] by auto
- then show ?thesis using real_cond_exp_intg(2)[where ?f = "indicator A" and ?g = f, symmetric] by auto
+ then show ?thesis using real_cond_exp_intg(2)[where ?f = "indicator A" and ?g = f, symmetric]
+ unfolding set_lebesgue_integral_def by auto
qed
lemma real_cond_exp_int [intro]:
@@ -760,14 +761,14 @@
then have [measurable]: "A \<in> sets F" using sets_restr_to_subalg[OF subalg] by simp
then have a [measurable]: "A \<in> sets M" by (meson subalg subalgebra_def subsetD)
have "(\<integral>x \<in> A. g x \<partial> ?MF) = (\<integral>x \<in> A. g x \<partial>M)"
- by (simp add: integral_subalgebra2 subalg)
+ unfolding set_lebesgue_integral_def by (simp add: integral_subalgebra2 subalg)
also have "... = (\<integral>x \<in> A. f x \<partial>M)" using assms(1) by simp
- also have "... = (\<integral>x. indicator A x * f x \<partial>M)" by (simp add: mult.commute)
+ also have "... = (\<integral>x. indicator A x * f x \<partial>M)" by (simp add: mult.commute set_lebesgue_integral_def)
also have "... = (\<integral>x. indicator A x * real_cond_exp M F f x \<partial>M)"
apply (rule real_cond_exp_intg(2)[symmetric]) using integrable_mult_indicator[OF a assms(2)] by (auto simp add: assms)
- also have "... = (\<integral>x \<in> A. real_cond_exp M F f x \<partial>M)" by (simp add: mult.commute)
+ also have "... = (\<integral>x \<in> A. real_cond_exp M F f x \<partial>M)" by (simp add: mult.commute set_lebesgue_integral_def)
also have "... = (\<integral>x \<in> A. real_cond_exp M F f x \<partial> ?MF)"
- by (simp add: integral_subalgebra2 subalg)
+ by (simp add: integral_subalgebra2 subalg set_lebesgue_integral_def)
finally show "(\<integral>x \<in> A. g x \<partial> ?MF) = (\<integral>x \<in> A. real_cond_exp M F f x \<partial> ?MF)" by simp
next
have "integrable M (real_cond_exp M F f)" by (rule real_cond_exp_int(1)[OF assms(2)])
@@ -791,12 +792,12 @@
then have [measurable]: "(\<lambda>x. f x * indicator A x) \<in> borel_measurable F" by measurable
have [measurable]: "A \<in> sets M" using subalg by (meson \<open>A \<in> sets F\<close> subalgebra_def subsetD)
have "\<integral>x\<in>A. (f x * g x) \<partial>M = \<integral>x. (f x * indicator A x) * g x \<partial>M"
- by (simp add: mult.commute mult.left_commute)
+ by (simp add: mult.commute mult.left_commute set_lebesgue_integral_def)
also have "... = \<integral>x. (f x * indicator A x) * real_cond_exp M F g x \<partial>M"
apply (rule real_cond_exp_intg(2)[symmetric], auto simp add: assms)
using integrable_mult_indicator[OF \<open>A \<in> sets M\<close> assms(3)] by (simp add: mult.commute mult.left_commute)
also have "... = \<integral>x\<in>A. (f x * real_cond_exp M F g x)\<partial>M"
- by (simp add: mult.commute mult.left_commute)
+ by (simp add: mult.commute mult.left_commute set_lebesgue_integral_def)
finally show "\<integral>x\<in>A. (f x * g x) \<partial>M = \<integral>x\<in>A. (f x * real_cond_exp M F g x)\<partial>M" by simp
qed (auto simp add: real_cond_exp_intg(1) assms)
@@ -817,17 +818,17 @@
using integrable_mult_indicator[OF \<open>A \<in> sets M\<close> assms(2)] by auto
have "\<integral>x\<in>A. (real_cond_exp M F f x + real_cond_exp M F g x)\<partial>M = (\<integral>x\<in>A. real_cond_exp M F f x \<partial>M) + (\<integral>x\<in>A. real_cond_exp M F g x \<partial>M)"
- apply (rule set_integral_add, auto simp add: assms)
+ apply (rule set_integral_add, auto simp add: assms set_integrable_def)
using integrable_mult_indicator[OF \<open>A \<in> sets M\<close> real_cond_exp_int(1)[OF assms(1)]]
integrable_mult_indicator[OF \<open>A \<in> sets M\<close> real_cond_exp_int(1)[OF assms(2)]] by simp_all
also have "... = (\<integral>x. indicator A x * real_cond_exp M F f x \<partial>M) + (\<integral>x. indicator A x * real_cond_exp M F g x \<partial>M)"
- by auto
+ unfolding set_lebesgue_integral_def by auto
also have "... = (\<integral>x. indicator A x * f x \<partial>M) + (\<integral>x. indicator A x * g x \<partial>M)"
using real_cond_exp_intg(2) assms \<open>A \<in> sets F\<close> intAf intAg by auto
also have "... = (\<integral>x\<in>A. f x \<partial>M) + (\<integral>x\<in>A. g x \<partial>M)"
- by auto
+ unfolding set_lebesgue_integral_def by auto
also have "... = \<integral>x\<in>A. (f x + g x)\<partial>M"
- by (rule set_integral_add(2)[symmetric]) (auto simp add: assms \<open>A \<in> sets M\<close> intAf intAg)
+ by (rule set_integral_add(2)[symmetric]) (auto simp add: assms set_integrable_def \<open>A \<in> sets M\<close> intAf intAg)
finally show "\<integral>x\<in>A. (f x + g x)\<partial>M = \<integral>x\<in>A. (real_cond_exp M F f x + real_cond_exp M F g x)\<partial>M"
by simp
qed (auto simp add: assms)
@@ -911,7 +912,7 @@
lemma real_cond_exp_gr_c:
assumes [measurable]: "integrable M f"
- and "AE x in M. f x > c"
+ and AE: "AE x in M. f x > c"
shows "AE x in M. real_cond_exp M F f x > c"
proof -
define X where "X = {x \<in> space M. real_cond_exp M F f x \<le> c}"
@@ -931,24 +932,33 @@
then have [measurable]: "A \<in> sets F" using subalg sets_restr_to_subalg by blast
then have [measurable]: "A \<in> sets M" using sets_restr_to_subalg subalg subalgebra_def by blast
have Ic: "set_integrable M A (\<lambda>x. c)"
+ unfolding set_integrable_def
using \<open>emeasure (restr_to_subalg M F) A < \<infinity>\<close> emeasure_restr_to_subalg subalg by fastforce
have If: "set_integrable M A f"
+ unfolding set_integrable_def
by (rule integrable_mult_indicator, auto simp add: \<open>integrable M f\<close>)
- have *: "(\<integral>x\<in>A. c \<partial>M) = (\<integral>x\<in>A. f x \<partial>M)"
- proof (rule antisym)
- show "(\<integral>x\<in>A. c \<partial>M) \<le> (\<integral>x\<in>A. f x \<partial>M)"
- apply (rule set_integral_mono_AE) using Ic If assms(2) by auto
- have "(\<integral>x\<in>A. f x \<partial>M) = (\<integral>x\<in>A. real_cond_exp M F f x \<partial>M)"
- by (rule real_cond_exp_intA, auto simp add: \<open>integrable M f\<close>)
- also have "... \<le> (\<integral>x\<in>A. c \<partial>M)"
- apply (rule set_integral_mono)
- apply (rule integrable_mult_indicator, simp, simp add: real_cond_exp_int(1)[OF \<open>integrable M f\<close>])
- using Ic X_def \<open>A \<subseteq> X\<close> by auto
- finally show "(\<integral>x\<in>A. f x \<partial>M) \<le> (\<integral>x\<in>A. c \<partial>M)" by simp
- qed
have "AE x in M. indicator A x * c = indicator A x * f x"
- apply (rule integral_ineq_eq_0_then_AE) using Ic If * apply auto
- using assms(2) unfolding indicator_def by auto
+ proof (rule integral_ineq_eq_0_then_AE)
+ have "(\<integral>x\<in>A. c \<partial>M) = (\<integral>x\<in>A. f x \<partial>M)"
+ proof (rule antisym)
+ show "(\<integral>x\<in>A. c \<partial>M) \<le> (\<integral>x\<in>A. f x \<partial>M)"
+ apply (rule set_integral_mono_AE) using Ic If assms(2) by auto
+ have "(\<integral>x\<in>A. f x \<partial>M) = (\<integral>x\<in>A. real_cond_exp M F f x \<partial>M)"
+ by (rule real_cond_exp_intA, auto simp add: \<open>integrable M f\<close>)
+ also have "... \<le> (\<integral>x\<in>A. c \<partial>M)"
+ apply (rule set_integral_mono)
+ unfolding set_integrable_def
+ apply (rule integrable_mult_indicator, simp, simp add: real_cond_exp_int(1)[OF \<open>integrable M f\<close>])
+ using Ic X_def \<open>A \<subseteq> X\<close> by (auto simp: set_integrable_def)
+ finally show "(\<integral>x\<in>A. f x \<partial>M) \<le> (\<integral>x\<in>A. c \<partial>M)" by simp
+ qed
+ then have "measure M A * c = LINT x|M. indicat_real A x * f x"
+ by (auto simp: set_lebesgue_integral_def)
+ then show "LINT x|M. indicat_real A x * c = LINT x|M. indicat_real A x * f x"
+ by auto
+ show "AE x in M. indicat_real A x * c \<le> indicat_real A x * f x"
+ using AE unfolding indicator_def by auto
+ qed (use Ic If in \<open>auto simp: set_integrable_def\<close>)
then have "AE x\<in>A in M. c = f x" by auto
then have "AE x\<in>A in M. False" using assms(2) by auto
have "A \<in> null_sets M" unfolding ae_filter_def by (meson AE_iff_null_sets \<open>A \<in> sets M\<close> \<open>AE x\<in>A in M. False\<close>)
@@ -1045,7 +1055,7 @@
by (rule real_cond_exp_intg(2)[symmetric], auto simp add: *)
have "(\<integral>x\<in>A. (\<Sum>i\<in>I. f i x)\<partial>M) = (\<integral>x. (\<Sum>i\<in>I. indicator A x * f i x)\<partial>M)"
- by (simp add: sum_distrib_left)
+ by (simp add: sum_distrib_left set_lebesgue_integral_def)
also have "... = (\<Sum>i\<in>I. (\<integral>x. indicator A x * f i x \<partial>M))"
by (rule Bochner_Integration.integral_sum, simp add: *)
also have "... = (\<Sum>i\<in>I. (\<integral>x. indicator A x * real_cond_exp M F (f i) x \<partial>M))"
@@ -1053,7 +1063,7 @@
also have "... = (\<integral>x. (\<Sum>i\<in>I. indicator A x * real_cond_exp M F (f i) x)\<partial>M)"
by (rule Bochner_Integration.integral_sum[symmetric], simp add: **)
also have "... = (\<integral>x\<in>A. (\<Sum>i\<in>I. real_cond_exp M F (f i) x)\<partial>M)"
- by (simp add: sum_distrib_left)
+ by (simp add: sum_distrib_left set_lebesgue_integral_def)
finally show "(\<integral>x\<in>A. (\<Sum>i\<in>I. f i x)\<partial>M) = (\<integral>x\<in>A. (\<Sum>i\<in>I. real_cond_exp M F (f i) x)\<partial>M)" by auto
qed (auto simp add: assms real_cond_exp_int(1)[OF assms(1)])
--- a/src/HOL/Probability/Distributions.thy Thu Apr 12 12:16:34 2018 +0100
+++ b/src/HOL/Probability/Distributions.thy Fri Apr 13 15:58:27 2018 +0100
@@ -955,12 +955,13 @@
by (rule integral_by_parts')
(auto intro!: derivative_eq_intros b
simp: diff_Suc of_nat_Suc field_simps split: nat.split)
- also have "(\<integral>x. indicator {0..b} x *\<^sub>R (- 2 * x * exp (- x\<^sup>2) * x ^ (Suc k)) \<partial>lborel) =
- (\<integral>x. indicator {0..b} x *\<^sub>R (- 2 * (exp (- x\<^sup>2) * x ^ (k + 2))) \<partial>lborel)"
- by (intro Bochner_Integration.integral_cong) auto
+ also have "... = exp (- b\<^sup>2) * b ^ (Suc k) - (\<integral>x. indicator {0..b} x *\<^sub>R (- 2 * (exp (- x\<^sup>2) * x ^ (k + 2))) \<partial>lborel)"
+ by (auto simp: intro!: Bochner_Integration.integral_cong)
+ also have "... = exp (- b\<^sup>2) * b ^ (Suc k) + 2 * (\<integral>x. indicator {0..b} x *\<^sub>R ?M (k + 2) x \<partial>lborel)"
+ unfolding Bochner_Integration.integral_mult_right_zero [symmetric]
+ by (simp del: real_scaleR_def)
finally have "Suc k * (\<integral>x. indicator {0..b} x *\<^sub>R ?M k x \<partial>lborel) =
- exp (- b\<^sup>2) * b ^ (Suc k) + 2 * (\<integral>x. indicator {0..b} x *\<^sub>R ?M (k + 2) x \<partial>lborel)"
- by (simp del: real_scaleR_def integral_mult_right add: integral_mult_right[symmetric])
+ exp (- b\<^sup>2) * b ^ (Suc k) + 2 * (\<integral>x. indicator {0..b} x *\<^sub>R ?M (k + 2) x \<partial>lborel)" .
then show "(k + 1) / 2 * (\<integral>x. indicator {..b} x *\<^sub>R (indicator {0..} x *\<^sub>R ?M k x)\<partial>lborel) - exp (- b\<^sup>2) * b ^ (k + 1) / 2 = ?f b"
by (simp add: field_simps atLeastAtMost_def indicator_inter_arith)
qed
--- a/src/HOL/Probability/Levy.thy Thu Apr 12 12:16:34 2018 +0100
+++ b/src/HOL/Probability/Levy.thy Fri Apr 13 15:58:27 2018 +0100
@@ -90,12 +90,12 @@
{ fix x
have 1: "complex_interval_lebesgue_integrable lborel u v (\<lambda>t. ?f t x)" for u v :: real
using Levy_Inversion_aux2[of "x - b" "x - a"]
- apply (simp add: interval_lebesgue_integrable_def del: times_divide_eq_left)
+ apply (simp add: interval_lebesgue_integrable_def set_integrable_def del: times_divide_eq_left)
apply (intro integrableI_bounded_set_indicator[where B="b - a"] conjI impI)
apply (auto intro!: AE_I [of _ _ "{0}"] simp: assms)
done
have "(CLBINT t. ?f' (t, x)) = (CLBINT t=-T..T. ?f t x)"
- using \<open>T \<ge> 0\<close> by (simp add: interval_lebesgue_integral_def)
+ using \<open>T \<ge> 0\<close> by (simp add: interval_lebesgue_integral_def set_lebesgue_integral_def)
also have "\<dots> = (CLBINT t=-T..(0 :: real). ?f t x) + (CLBINT t=(0 :: real)..T. ?f t x)"
(is "_ = _ + ?t")
using 1 by (intro interval_integral_sum[symmetric]) (simp add: min_absorb1 max_absorb2 \<open>T \<ge> 0\<close>)
@@ -130,7 +130,7 @@
} note main_eq = this
have "(CLBINT t=-T..T. ?F t * \<phi> t) =
(CLBINT t. (CLINT x | M. ?F t * iexp (t * x) * indicator {-T<..<T} t))"
- using \<open>T \<ge> 0\<close> unfolding \<phi>_def char_def interval_lebesgue_integral_def
+ using \<open>T \<ge> 0\<close> unfolding \<phi>_def char_def interval_lebesgue_integral_def set_lebesgue_integral_def
by (auto split: split_indicator intro!: Bochner_Integration.integral_cong)
also have "\<dots> = (CLBINT t. (CLINT x | M. ?f' (t, x)))"
by (auto intro!: Bochner_Integration.integral_cong simp: field_simps exp_diff exp_minus split: split_indicator)
@@ -323,6 +323,7 @@
by (rule Mn.integrable_const_bound [where B = 1], auto)
have Mn3: "set_integrable (M n \<Otimes>\<^sub>M lborel) (UNIV \<times> {- u..u}) (\<lambda>a. 1 - exp (\<i> * complex_of_real (snd a * fst a)))"
using \<open>0 < u\<close>
+ unfolding set_integrable_def
by (intro integrableI_bounded_set_indicator [where B="2"])
(auto simp: lborel.emeasure_pair_measure_Times ennreal_mult_less_top not_less top_unique
split: split_indicator
@@ -331,9 +332,10 @@
(CLBINT t:{-u..u}. (CLINT x | M n. 1 - iexp (t * x)))"
unfolding char_def by (rule set_lebesgue_integral_cong, auto simp del: of_real_mult)
also have "\<dots> = (CLBINT t. (CLINT x | M n. indicator {-u..u} t *\<^sub>R (1 - iexp (t * x))))"
+ unfolding set_lebesgue_integral_def
by (rule Bochner_Integration.integral_cong) (auto split: split_indicator)
also have "\<dots> = (CLINT x | M n. (CLBINT t:{-u..u}. 1 - iexp (t * x)))"
- using Mn3 by (subst P.Fubini_integral) (auto simp: indicator_times split_beta')
+ using Mn3 by (subst P.Fubini_integral) (auto simp: indicator_times split_beta' set_integrable_def set_lebesgue_integral_def)
also have "\<dots> = (CLINT x | M n. (if x = 0 then 0 else 2 * (u - sin (u * x) / x)))"
using \<open>u > 0\<close> by (intro Bochner_Integration.integral_cong, auto simp add: * simp del: of_real_mult)
also have "\<dots> = (LINT x | M n. (if x = 0 then 0 else 2 * (u - sin (u * x) / x)))"
@@ -343,9 +345,12 @@
also have "\<dots> \<ge> (LINT x : {x. abs x \<ge> 2 / u} | M n. u)"
proof -
have "complex_integrable (M n) (\<lambda>x. CLBINT t:{-u..u}. 1 - iexp (snd (x, t) * fst (x, t)))"
- using Mn3 by (intro P.integrable_fst) (simp add: indicator_times split_beta')
+ using Mn3 unfolding set_integrable_def set_lebesgue_integral_def
+ by (intro P.integrable_fst) (simp add: indicator_times split_beta')
hence "complex_integrable (M n) (\<lambda>x. if x = 0 then 0 else 2 * (u - sin (u * x) / x))"
- using \<open>u > 0\<close> by (subst integrable_cong) (auto simp add: * simp del: of_real_mult)
+ using \<open>u > 0\<close>
+ unfolding set_integrable_def
+ by (subst integrable_cong) (auto simp add: * simp del: of_real_mult)
hence **: "integrable (M n) (\<lambda>x. if x = 0 then 0 else 2 * (u - sin (u * x) / x))"
unfolding complex_of_real_integrable_eq .
have "2 * sin x \<le> x" if "2 \<le> x" for x :: real
@@ -355,13 +360,13 @@
moreover have "x < 0 \<Longrightarrow> x \<le> sin x" for x :: real
using sin_x_le_x[of "-x"] by simp
ultimately show ?thesis
- using \<open>u > 0\<close>
+ using \<open>u > 0\<close> unfolding set_lebesgue_integral_def
by (intro integral_mono [OF _ **])
(auto simp: divide_simps sin_x_le_x mult.commute[of u] mult_neg_pos top_unique less_top[symmetric]
split: split_indicator)
qed
- also (xtrans) have "(LINT x : {x. abs x \<ge> 2 / u} | M n. u) =
- u * measure (M n) {x. abs x \<ge> 2 / u}"
+ also (xtrans) have "(LINT x : {x. abs x \<ge> 2 / u} | M n. u) = u * measure (M n) {x. abs x \<ge> 2 / u}"
+ unfolding set_lebesgue_integral_def
by (simp add: Mn.emeasure_eq_measure)
finally show "Re (CLBINT t:{-u..u}. 1 - char (M n) t) \<ge> u * measure (M n) {x. abs x \<ge> 2 / u}" .
qed
@@ -380,13 +385,16 @@
have 1: "\<And>x. cmod (1 - char M' x) \<le> 2"
by (rule order_trans [OF norm_triangle_ineq4], auto simp add: M'.cmod_char_le_1)
then have 2: "\<And>u v. complex_set_integrable lborel {u..v} (\<lambda>x. 1 - char M' x)"
+ unfolding set_integrable_def
by (intro integrableI_bounded_set_indicator[where B=2]) (auto simp: emeasure_lborel_Icc_eq)
- have 3: "\<And>u v. set_integrable lborel {u..v} (\<lambda>x. cmod (1 - char M' x))"
+ have 3: "\<And>u v. integrable lborel (\<lambda>x. indicat_real {u..v} x *\<^sub>R cmod (1 - char M' x))"
by (intro borel_integrable_compact[OF compact_Icc] continuous_at_imp_continuous_on
continuous_intros ballI M'.isCont_char continuous_intros)
have "cmod (CLBINT t:{-d/2..d/2}. 1 - char M' t) \<le> LBINT t:{-d/2..d/2}. cmod (1 - char M' t)"
+ unfolding set_lebesgue_integral_def
using integral_norm_bound[of _ "\<lambda>x. indicator {u..v} x *\<^sub>R (1 - char M' x)" for u v] by simp
also have 4: "\<dots> \<le> LBINT t:{-d/2..d/2}. \<epsilon> / 4"
+ unfolding set_lebesgue_integral_def
apply (rule integral_mono [OF 3])
apply (simp add: emeasure_lborel_Icc_eq)
apply (case_tac "x \<in> {-d/2..d/2}")
@@ -397,11 +405,12 @@
using d0 apply auto
done
also from d0 4 have "\<dots> = d * \<epsilon> / 4"
- by simp
+ unfolding set_lebesgue_integral_def by simp
finally have bound: "cmod (CLBINT t:{-d/2..d/2}. 1 - char M' t) \<le> d * \<epsilon> / 4" .
have "cmod (1 - char (M n) x) \<le> 2" for n x
by (rule order_trans [OF norm_triangle_ineq4], auto simp add: Mn.cmod_char_le_1)
then have "(\<lambda>n. CLBINT t:{-d/2..d/2}. 1 - char (M n) t) \<longlonglongrightarrow> (CLBINT t:{-d/2..d/2}. 1 - char M' t)"
+ unfolding set_lebesgue_integral_def
apply (intro integral_dominated_convergence[where w="\<lambda>x. indicator {-d/2..d/2} x *\<^sub>R 2"])
apply (auto intro!: char_conv tendsto_intros
simp: emeasure_lborel_Icc_eq
--- a/src/HOL/Probability/Probability_Mass_Function.thy Thu Apr 12 12:16:34 2018 +0100
+++ b/src/HOL/Probability/Probability_Mass_Function.thy Fri Apr 13 15:58:27 2018 +0100
@@ -541,7 +541,7 @@
shows "infsetsum (pmf p) A = 1"
proof -
have "infsetsum (pmf p) A = lebesgue_integral (count_space UNIV) (pmf p)"
- using assms unfolding infsetsum_altdef
+ using assms unfolding infsetsum_altdef set_lebesgue_integral_def
by (intro Bochner_Integration.integral_cong) (auto simp: indicator_def set_pmf_eq)
also have "\<dots> = 1"
by (subst integral_eq_nn_integral) (auto simp: nn_integral_pmf)
--- a/src/HOL/Probability/Sinc_Integral.thy Thu Apr 12 12:16:34 2018 +0100
+++ b/src/HOL/Probability/Sinc_Integral.thy Fri Apr 13 15:58:27 2018 +0100
@@ -33,12 +33,12 @@
lemma integrable_I0i_exp_mscale: "0 < (u::real) \<Longrightarrow> set_integrable lborel {0 <..} (\<lambda>x. exp (-(x * u)))"
using lborel_integrable_real_affine_iff[of u "\<lambda>x. indicator {0 <..} x *\<^sub>R exp (- x)" 0]
has_bochner_integral_I0i_power_exp_m[of 0]
- by (simp add: indicator_def zero_less_mult_iff mult_ac integrable.intros)
+ by (simp add: indicator_def zero_less_mult_iff mult_ac integrable.intros set_integrable_def)
lemma LBINT_I0i_exp_mscale: "0 < (u::real) \<Longrightarrow> LBINT x=0..\<infinity>. exp (-(x * u)) = 1 / u"
using lborel_integral_real_affine[of u "\<lambda>x. indicator {0<..} x *\<^sub>R exp (- x)" 0]
has_bochner_integral_I0i_power_exp_m[of 0]
- by (auto simp: indicator_def zero_less_mult_iff interval_lebesgue_integral_0_infty field_simps
+ by (auto simp: indicator_def zero_less_mult_iff interval_lebesgue_integral_0_infty set_lebesgue_integral_def field_simps
dest!: has_bochner_integral_integral_eq)
lemma LBINT_I0c_exp_mscale_sin:
@@ -83,11 +83,11 @@
show "LBINT x=-\<infinity>..\<infinity>. inverse (1 + x^2) = pi"
by (subst interval_integral_substitution_nonneg[of "-pi/2" "pi/2" tan "\<lambda>x. 1 + (tan x)^2"])
(auto intro: derivative_eq_intros 1 2 filterlim_tan_at_right
- simp add: ereal_tendsto_simps filterlim_tan_at_left add_nonneg_eq_0_iff)
+ simp add: ereal_tendsto_simps filterlim_tan_at_left add_nonneg_eq_0_iff set_integrable_def)
show "set_integrable lborel (einterval (-\<infinity>) \<infinity>) (\<lambda>x. inverse (1 + x^2))"
by (subst interval_integral_substitution_nonneg[of "-pi/2" "pi/2" tan "\<lambda>x. 1 + (tan x)^2"])
(auto intro: derivative_eq_intros 1 2 filterlim_tan_at_right
- simp add: ereal_tendsto_simps filterlim_tan_at_left add_nonneg_eq_0_iff)
+ simp add: ereal_tendsto_simps filterlim_tan_at_left add_nonneg_eq_0_iff set_integrable_def)
qed
lemma
@@ -103,12 +103,12 @@
show "LBINT x=0..\<infinity>. 1 / (1 + x^2) = pi / 2"
by (subst interval_integral_substitution_nonneg[of "0" "pi/2" tan "\<lambda>x. 1 + (tan x)^2"])
(auto intro: derivative_eq_intros 1 2 tendsto_eq_intros
- simp add: ereal_tendsto_simps filterlim_tan_at_left zero_ereal_def add_nonneg_eq_0_iff)
+ simp add: ereal_tendsto_simps filterlim_tan_at_left zero_ereal_def add_nonneg_eq_0_iff set_integrable_def)
show "interval_lebesgue_integrable lborel 0 \<infinity> (\<lambda>x. 1 / (1 + x^2))"
unfolding interval_lebesgue_integrable_def
by (subst interval_integral_substitution_nonneg[of "0" "pi/2" tan "\<lambda>x. 1 + (tan x)^2"])
(auto intro: derivative_eq_intros 1 2 tendsto_eq_intros
- simp add: ereal_tendsto_simps filterlim_tan_at_left zero_ereal_def add_nonneg_eq_0_iff)
+ simp add: ereal_tendsto_simps filterlim_tan_at_left zero_ereal_def add_nonneg_eq_0_iff set_integrable_def)
qed
section \<open>The sinc function, and the sine integral (Si)\<close>
@@ -212,10 +212,12 @@
have int: "set_integrable lborel {0<..} (\<lambda>x. exp (- x) * (x + 1) :: real)"
unfolding distrib_left
using has_bochner_integral_I0i_power_exp_m[of 0] has_bochner_integral_I0i_power_exp_m[of 1]
- by (intro set_integral_add) (auto dest!: integrable.intros simp: ac_simps)
+ by (intro set_integral_add) (auto dest!: integrable.intros simp: ac_simps set_integrable_def)
have "((\<lambda>t::real. LBINT x:{0<..}. ?F x t) \<longlongrightarrow> LBINT x::real:{0<..}. 0) at_top"
- proof (rule integral_dominated_convergence_at_top[OF _ _ int], simp_all del: abs_divide split: split_indicator)
+ unfolding set_lebesgue_integral_def
+ proof (rule integral_dominated_convergence_at_top[OF _ _ int [unfolded set_integrable_def]],
+ simp_all del: abs_divide split: split_indicator)
have *: "0 < x \<Longrightarrow> \<bar>x * sin t + cos t\<bar> / (1 + x\<^sup>2) \<le> (x * 1 + 1) / 1" for x t :: real
by (intro frac_le abs_triangle_ineq[THEN order_trans] add_mono)
(auto simp add: abs_mult simp del: mult_1_right intro!: mult_mono)
@@ -241,7 +243,7 @@
qed
qed
then show "((\<lambda>t. (LBINT x=0..\<infinity>. exp (-(x * t)) * (x * sin t + cos t) / (1 + x^2))) \<longlongrightarrow> 0) at_top"
- by (simp add: interval_lebesgue_integral_0_infty)
+ by (simp add: interval_lebesgue_integral_0_infty set_lebesgue_integral_def)
qed
lemma Si_at_top_integrable:
@@ -258,10 +260,10 @@
have "set_integrable lborel {0<..} (\<lambda>x. (exp (- x) * x) * (sin t/t) + exp (- x) * cos t)"
using has_bochner_integral_I0i_power_exp_m[of 0] has_bochner_integral_I0i_power_exp_m[of 1]
by (intro set_integral_add set_integrable_mult_left)
- (auto dest!: integrable.intros simp: ac_simps)
- from lborel_integrable_real_affine[OF this, of t 0]
+ (auto dest!: integrable.intros simp: ac_simps set_integrable_def)
+ from lborel_integrable_real_affine[OF this [unfolded set_integrable_def], of t 0]
show ?thesis
- unfolding interval_lebesgue_integral_0_infty
+ unfolding interval_lebesgue_integral_0_infty set_integrable_def
by (rule Bochner_Integration.integrable_bound) (auto simp: field_simps * split: split_indicator)
qed
@@ -275,9 +277,10 @@
unfolding Si_def using \<open>0 \<le> t\<close>
by (intro interval_integral_discrete_difference[where X="{0}"]) (auto simp: LBINT_I0i_exp_mscale)
also have "\<dots> = LBINT x. (LBINT u=ereal 0..\<infinity>. indicator {0 <..< t} x *\<^sub>R sin x * exp (-(u * x)))"
- using \<open>0\<le>t\<close> by (simp add: zero_ereal_def interval_lebesgue_integral_le_eq mult_ac)
+ using \<open>0\<le>t\<close> by (simp add: zero_ereal_def interval_lebesgue_integral_le_eq mult_ac set_lebesgue_integral_def)
also have "\<dots> = LBINT x. (LBINT u. indicator ({0<..} \<times> {0 <..< t}) (u, x) *\<^sub>R (sin x * exp (-(u * x))))"
- by (subst interval_integral_Ioi) (simp_all add: indicator_times ac_simps)
+ apply (subst interval_integral_Ioi)
+ unfolding set_lebesgue_integral_def by(simp_all add: indicator_times ac_simps )
also have "\<dots> = LBINT u. (LBINT x. indicator ({0<..} \<times> {0 <..< t}) (u, x) *\<^sub>R (sin x * exp (-(u * x))))"
proof (intro lborel_pair.Fubini_integral[symmetric] lborel_pair.Fubini_integrable)
show "(\<lambda>(x, y). indicator ({0<..} \<times> {0<..<t}) (y, x) *\<^sub>R (sin x * exp (- (y * x))))
@@ -293,7 +296,7 @@
by (intro Bochner_Integration.integral_cong) (auto split: split_indicator simp: abs_mult)
also have "\<dots> = \<bar>sin x\<bar> * indicator {0<..<t} x * (LBINT y=0..\<infinity>. exp (- (y * x)))"
by (cases "x > 0")
- (auto simp: field_simps interval_lebesgue_integral_0_infty split: split_indicator)
+ (auto simp: field_simps interval_lebesgue_integral_0_infty set_lebesgue_integral_def split: split_indicator)
also have "\<dots> = \<bar>sin x\<bar> * indicator {0<..<t} x * (1 / x)"
by (cases "x > 0") (auto simp add: LBINT_I0i_exp_mscale)
also have "\<dots> = indicator {0..t} x *\<^sub>R \<bar>sinc x\<bar>"
@@ -301,7 +304,7 @@
finally show "indicator {0..t} x *\<^sub>R abs (sinc x) = LBINT y. norm (?f (x, y))"
by simp
qed
- moreover have "set_integrable lborel {0 .. t} (\<lambda>x. abs (sinc x))"
+ moreover have "integrable lborel (\<lambda>x. indicat_real {0..t} x *\<^sub>R \<bar>sinc x\<bar>)"
by (auto intro!: borel_integrable_compact continuous_intros simp del: real_scaleR_def)
ultimately show "integrable lborel (\<lambda>x. LBINT y. norm (?f (x, y)))"
by (rule integrable_cong_AE_imp[rotated 2]) simp
@@ -309,11 +312,11 @@
have "0 < x \<Longrightarrow> set_integrable lborel {0<..} (\<lambda>y. sin x * exp (- (y * x)))" for x :: real
by (intro set_integrable_mult_right integrable_I0i_exp_mscale)
then show "AE x in lborel. integrable lborel (\<lambda>y. ?f (x, y))"
- by (intro AE_I2) (auto simp: indicator_times split: split_indicator)
+ by (intro AE_I2) (auto simp: indicator_times set_integrable_def split: split_indicator)
qed
also have "... = LBINT u=0..\<infinity>. (LBINT x=0..t. exp (-(u * x)) * sin x)"
using \<open>0\<le>t\<close>
- by (auto simp: interval_lebesgue_integral_def zero_ereal_def ac_simps
+ by (auto simp: interval_lebesgue_integral_def set_lebesgue_integral_def zero_ereal_def ac_simps
split: split_indicator intro!: Bochner_Integration.integral_cong)
also have "\<dots> = LBINT u=0..\<infinity>. 1 / (1 + u\<^sup>2) - 1 / (1 + u\<^sup>2) * (exp (- (u * t)) * (u * sin t + cos t))"
by (auto simp: divide_simps LBINT_I0c_exp_mscale_sin intro!: interval_integral_cong)
@@ -369,12 +372,12 @@
hence "LBINT x. indicator {0<..<T} x * sin (x * \<theta>) / x =
LBINT x. indicator {0<..<T * \<theta>} x * sin x / x"
using assms \<open>0 < \<theta>\<close> unfolding interval_lebesgue_integral_def einterval_eq zero_ereal_def
- by (auto simp: ac_simps)
+ by (auto simp: ac_simps set_lebesgue_integral_def)
} note aux1 = this
{ assume "0 > \<theta>"
have [simp]: "integrable lborel (\<lambda>x. sin (x * \<theta>) * indicator {0<..<T} x / x)"
using integrable_sinc' [of T \<theta>] assms
- by (simp add: interval_lebesgue_integrable_def ac_simps)
+ by (simp add: interval_lebesgue_integrable_def set_integrable_def ac_simps)
have "(LBINT t=ereal 0..T. sin (t * -\<theta>) / t) = (LBINT t=ereal 0..T. -\<theta> *\<^sub>R sinc (t * -\<theta>))"
by (rule interval_integral_discrete_difference[of "{0}"]) auto
also have "\<dots> = (LBINT t=ereal (0 * -\<theta>)..T * -\<theta>. sinc t)"
@@ -388,10 +391,10 @@
hence "LBINT x. indicator {0<..<T} x * sin (x * \<theta>) / x =
- (LBINT x. indicator {0<..<- (T * \<theta>)} x * sin x / x)"
using assms \<open>0 > \<theta>\<close> unfolding interval_lebesgue_integral_def einterval_eq zero_ereal_def
- by (auto simp add: field_simps mult_le_0_iff split: if_split_asm)
+ by (auto simp add: field_simps mult_le_0_iff set_lebesgue_integral_def split: if_split_asm)
} note aux2 = this
show ?thesis
- using assms unfolding Si_def interval_lebesgue_integral_def sgn_real_def einterval_eq zero_ereal_def
+ using assms unfolding Si_def interval_lebesgue_integral_def set_lebesgue_integral_def sgn_real_def einterval_eq zero_ereal_def
apply auto
apply (erule aux1)
apply (rule aux2)