import general thms from Density_Compiler
authorhoelzl
Thu Jan 22 14:51:08 2015 +0100 (2015-01-22)
changeset 59425c5e79df8cc21
parent 59424 ca2336984f6a
child 59426 6fca83e88417
child 59427 084330e2ec5e
import general thms from Density_Compiler
src/HOL/Library/Extended_Real.thy
src/HOL/Library/FuncSet.thy
src/HOL/Library/Product_Vector.thy
src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
src/HOL/Multivariate_Analysis/Integration.thy
src/HOL/Probability/Bochner_Integration.thy
src/HOL/Probability/Finite_Product_Measure.thy
src/HOL/Probability/Giry_Monad.thy
src/HOL/Probability/Lebesgue_Measure.thy
src/HOL/Probability/Measure_Space.thy
src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy
src/HOL/Probability/Probability_Mass_Function.thy
src/HOL/Probability/Probability_Measure.thy
     1.1 --- a/src/HOL/Library/Extended_Real.thy	Thu Jan 22 13:21:45 2015 +0100
     1.2 +++ b/src/HOL/Library/Extended_Real.thy	Thu Jan 22 14:51:08 2015 +0100
     1.3 @@ -1606,6 +1606,42 @@
     1.4      using zero_neq_one by blast
     1.5  qed
     1.6  
     1.7 +lemma ereal_Sup:
     1.8 +  assumes *: "\<bar>SUP a:A. ereal a\<bar> \<noteq> \<infinity>"
     1.9 +  shows "ereal (Sup A) = (SUP a:A. ereal a)"
    1.10 +proof (rule antisym)
    1.11 +  obtain r where r: "ereal r = (SUP a:A. ereal a)" "A \<noteq> {}"
    1.12 +    using * by (force simp: bot_ereal_def)
    1.13 +  then have upper: "\<And>a. a \<in> A \<Longrightarrow> a \<le> r"
    1.14 +    by (auto intro!: SUP_upper simp add: ereal_less_eq(3)[symmetric] simp del: ereal_less_eq)
    1.15 +
    1.16 +  show "ereal (Sup A) \<le> (SUP a:A. ereal a)"
    1.17 +    using upper by (simp add: r[symmetric] cSup_least[OF `A \<noteq> {}`])
    1.18 +  show "(SUP a:A. ereal a) \<le> ereal (Sup A)"
    1.19 +    using upper `A \<noteq> {}` by (intro SUP_least) (auto intro!: cSup_upper bdd_aboveI)
    1.20 +qed
    1.21 +
    1.22 +lemma ereal_SUP: "\<bar>SUP a:A. ereal (f a)\<bar> \<noteq> \<infinity> \<Longrightarrow> ereal (SUP a:A. f a) = (SUP a:A. ereal (f a))"
    1.23 +  using ereal_Sup[of "f`A"] by auto
    1.24 +  
    1.25 +lemma ereal_Inf:
    1.26 +  assumes *: "\<bar>INF a:A. ereal a\<bar> \<noteq> \<infinity>"
    1.27 +  shows "ereal (Inf A) = (INF a:A. ereal a)"
    1.28 +proof (rule antisym)
    1.29 +  obtain r where r: "ereal r = (INF a:A. ereal a)" "A \<noteq> {}"
    1.30 +    using * by (force simp: top_ereal_def)
    1.31 +  then have lower: "\<And>a. a \<in> A \<Longrightarrow> r \<le> a"
    1.32 +    by (auto intro!: INF_lower simp add: ereal_less_eq(3)[symmetric] simp del: ereal_less_eq)
    1.33 +
    1.34 +  show "(INF a:A. ereal a) \<le> ereal (Inf A)"
    1.35 +    using lower by (simp add: r[symmetric] cInf_greatest[OF `A \<noteq> {}`])
    1.36 +  show "ereal (Inf A) \<le> (INF a:A. ereal a)"
    1.37 +    using lower `A \<noteq> {}` by (intro INF_greatest) (auto intro!: cInf_lower bdd_belowI)
    1.38 +qed
    1.39 +
    1.40 +lemma ereal_INF: "\<bar>INF a:A. ereal (f a)\<bar> \<noteq> \<infinity> \<Longrightarrow> ereal (INF a:A. f a) = (INF a:A. ereal (f a))"
    1.41 +  using ereal_Inf[of "f`A"] by auto
    1.42 +
    1.43  lemma ereal_Sup_uminus_image_eq: "Sup (uminus ` S::ereal set) = - Inf S"
    1.44    by (auto intro!: SUP_eqI
    1.45             simp: Ball_def[symmetric] ereal_uminus_le_reorder le_Inf_iff
    1.46 @@ -1705,28 +1741,37 @@
    1.47      using assms by (cases e) auto
    1.48  qed
    1.49  
    1.50 +lemma SUP_PInfty:
    1.51 +  fixes f :: "'a \<Rightarrow> ereal"
    1.52 +  assumes "\<And>n::nat. \<exists>i\<in>A. ereal (real n) \<le> f i"
    1.53 +  shows "(SUP i:A. f i) = \<infinity>"
    1.54 +  unfolding SUP_def Sup_eq_top_iff[where 'a=ereal, unfolded top_ereal_def]
    1.55 +  apply simp
    1.56 +proof safe
    1.57 +  fix x :: ereal
    1.58 +  assume "x \<noteq> \<infinity>"
    1.59 +  show "\<exists>i\<in>A. x < f i"
    1.60 +  proof (cases x)
    1.61 +    case PInf
    1.62 +    with `x \<noteq> \<infinity>` show ?thesis
    1.63 +      by simp
    1.64 +  next
    1.65 +    case MInf
    1.66 +    with assms[of "0"] show ?thesis
    1.67 +      by force
    1.68 +  next
    1.69 +    case (real r)
    1.70 +    with less_PInf_Ex_of_nat[of x] obtain n :: nat where "x < ereal (real n)"
    1.71 +      by auto
    1.72 +    moreover obtain i where "i \<in> A" "ereal (real n) \<le> f i"
    1.73 +      using assms ..
    1.74 +    ultimately show ?thesis
    1.75 +      by (auto intro!: bexI[of _ i])
    1.76 +  qed
    1.77 +qed
    1.78 +
    1.79  lemma SUP_nat_Infty: "(SUP i::nat. ereal (real i)) = \<infinity>"
    1.80 -proof -
    1.81 -  {
    1.82 -    fix x :: ereal
    1.83 -    assume "x \<noteq> \<infinity>"
    1.84 -    then have "\<exists>k::nat. x < ereal (real k)"
    1.85 -    proof (cases x)
    1.86 -      case MInf
    1.87 -      then show ?thesis
    1.88 -        by (intro exI[of _ 0]) auto
    1.89 -    next
    1.90 -      case (real r)
    1.91 -      moreover obtain k :: nat where "r < real k"
    1.92 -        using ex_less_of_nat by (auto simp: real_eq_of_nat)
    1.93 -      ultimately show ?thesis
    1.94 -        by auto
    1.95 -    qed simp
    1.96 -  }
    1.97 -  then show ?thesis
    1.98 -    using SUP_eq_top_iff[of UNIV "\<lambda>n::nat. ereal (real n)"]
    1.99 -    by (auto simp: top_ereal_def)
   1.100 -qed
   1.101 +  by (rule SUP_PInfty) auto
   1.102  
   1.103  lemma Inf_less:
   1.104    fixes x :: ereal
   1.105 @@ -1930,35 +1975,6 @@
   1.106    shows "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i) \<Longrightarrow> 0 \<le> c \<Longrightarrow> (SUP i:I. c + f i) = c + SUPREMUM I f"
   1.107    using SUP_ereal_add_left[of I f c] by (simp add: add_ac)
   1.108  
   1.109 -lemma SUP_PInfty:
   1.110 -  fixes f :: "'a \<Rightarrow> ereal"
   1.111 -  assumes "\<And>n::nat. \<exists>i\<in>A. ereal (real n) \<le> f i"
   1.112 -  shows "(SUP i:A. f i) = \<infinity>"
   1.113 -  unfolding SUP_def Sup_eq_top_iff[where 'a=ereal, unfolded top_ereal_def]
   1.114 -  apply simp
   1.115 -proof safe
   1.116 -  fix x :: ereal
   1.117 -  assume "x \<noteq> \<infinity>"
   1.118 -  show "\<exists>i\<in>A. x < f i"
   1.119 -  proof (cases x)
   1.120 -    case PInf
   1.121 -    with `x \<noteq> \<infinity>` show ?thesis
   1.122 -      by simp
   1.123 -  next
   1.124 -    case MInf
   1.125 -    with assms[of "0"] show ?thesis
   1.126 -      by force
   1.127 -  next
   1.128 -    case (real r)
   1.129 -    with less_PInf_Ex_of_nat[of x] obtain n :: nat where "x < ereal (real n)"
   1.130 -      by auto
   1.131 -    moreover obtain i where "i \<in> A" "ereal (real n) \<le> f i"
   1.132 -      using assms ..
   1.133 -    ultimately show ?thesis
   1.134 -      by (auto intro!: bexI[of _ i])
   1.135 -  qed
   1.136 -qed
   1.137 -
   1.138  lemma Sup_countable_SUP:
   1.139    assumes "A \<noteq> {}"
   1.140    shows "\<exists>f::nat \<Rightarrow> ereal. range f \<subseteq> A \<and> Sup A = SUPREMUM UNIV f"
   1.141 @@ -2664,13 +2680,6 @@
   1.142    by (cases rule: ereal3_cases[of a b c])
   1.143      (auto simp add: field_simps not_le mult_le_0_iff mult_less_0_iff)
   1.144  
   1.145 -lemma ereal_pos_le_distrib:
   1.146 -  fixes a b c :: ereal
   1.147 -  assumes "c \<ge> 0"
   1.148 -  shows "c * (a + b) \<le> c * a + c * b"
   1.149 -  using assms
   1.150 -  by (cases rule: ereal3_cases[of a b c]) (auto simp add: field_simps)
   1.151 -
   1.152  lemma ereal_max_mono: "(a::ereal) \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> max a c \<le> max b d"
   1.153    by (metis sup_ereal_def sup_mono)
   1.154  
     2.1 --- a/src/HOL/Library/FuncSet.thy	Thu Jan 22 13:21:45 2015 +0100
     2.2 +++ b/src/HOL/Library/FuncSet.thy	Thu Jan 22 14:51:08 2015 +0100
     2.3 @@ -405,16 +405,20 @@
     2.4  lemma fun_upd_in_PiE: "x \<notin> S \<Longrightarrow> f \<in> PiE (insert x S) T \<Longrightarrow> f(x := undefined) \<in> PiE S T"
     2.5    unfolding PiE_def extensional_def by auto
     2.6  
     2.7 -lemma PiE_insert_eq:
     2.8 -  assumes "x \<notin> S"
     2.9 -  shows "PiE (insert x S) T = (\<lambda>(y, g). g(x := y)) ` (T x \<times> PiE S T)"
    2.10 +lemma PiE_insert_eq: "PiE (insert x S) T = (\<lambda>(y, g). g(x := y)) ` (T x \<times> PiE S T)"
    2.11  proof -
    2.12    {
    2.13 -    fix f assume "f \<in> PiE (insert x S) T"
    2.14 +    fix f assume "f \<in> PiE (insert x S) T" "x \<notin> S"
    2.15      with assms have "f \<in> (\<lambda>(y, g). g(x := y)) ` (T x \<times> PiE S T)"
    2.16        by (auto intro!: image_eqI[where x="(f x, f(x := undefined))"] intro: fun_upd_in_PiE PiE_mem)
    2.17    }
    2.18 -  then show ?thesis
    2.19 +  moreover
    2.20 +  {
    2.21 +    fix f assume "f \<in> PiE (insert x S) T" "x \<in> S"
    2.22 +    with assms have "f \<in> (\<lambda>(y, g). g(x := y)) ` (T x \<times> PiE S T)"
    2.23 +      by (auto intro!: image_eqI[where x="(f x, f)"] intro: fun_upd_in_PiE PiE_mem simp: insert_absorb)
    2.24 +  }
    2.25 +  ultimately show ?thesis
    2.26      using assms by (auto intro: PiE_fun_upd)
    2.27  qed
    2.28  
     3.1 --- a/src/HOL/Library/Product_Vector.thy	Thu Jan 22 13:21:45 2015 +0100
     3.2 +++ b/src/HOL/Library/Product_Vector.thy	Thu Jan 22 14:51:08 2015 +0100
     3.3 @@ -538,4 +538,8 @@
     3.4  
     3.5  end
     3.6  
     3.7 +lemma inner_Pair_0: "inner x (0, b) = inner (snd x) b" "inner x (a, 0) = inner (fst x) a"
     3.8 +    by (cases x, simp)+
     3.9 +
    3.10 +
    3.11  end
     4.1 --- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Thu Jan 22 13:21:45 2015 +0100
     4.2 +++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Thu Jan 22 14:51:08 2015 +0100
     4.3 @@ -1175,6 +1175,16 @@
     4.4  lemma suminf_ereal_finite: "summable f \<Longrightarrow> (\<Sum>i. ereal (f i)) \<noteq> \<infinity>"
     4.5    by (auto simp: sums_ereal[symmetric] summable_def sums_unique[symmetric])
     4.6  
     4.7 +lemma suminf_ereal_finite_neg:
     4.8 +  assumes "summable f"
     4.9 +  shows "(\<Sum>x. ereal (f x)) \<noteq> -\<infinity>"
    4.10 +proof-
    4.11 +  from assms obtain x where "f sums x" by blast
    4.12 +  hence "(\<lambda>x. ereal (f x)) sums ereal x" by (simp add: sums_ereal)
    4.13 +  from sums_unique[OF this] have "(\<Sum>x. ereal (f x)) = ereal x" ..
    4.14 +  thus "(\<Sum>x. ereal (f x)) \<noteq> -\<infinity>" by simp_all
    4.15 +qed
    4.16 +
    4.17  subsection {* monoset *}
    4.18  
    4.19  definition (in order) mono_set:
    4.20 @@ -1364,4 +1374,8 @@
    4.21  lemma ereal_indicator_nonneg[simp, intro]: "0 \<le> (indicator A x ::ereal)"
    4.22    unfolding indicator_def by auto
    4.23  
    4.24 +lemma indicator_inter_arith_ereal: "indicator A x * indicator B x = (indicator (A \<inter> B) x :: ereal)"
    4.25 +  by (simp split: split_indicator)
    4.26 +
    4.27 +
    4.28  end
     5.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Thu Jan 22 13:21:45 2015 +0100
     5.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Thu Jan 22 14:51:08 2015 +0100
     5.3 @@ -481,6 +481,35 @@
     5.4      and "interval_lowerbound (cbox a b) = a"
     5.5    using assms unfolding box_ne_empty by auto
     5.6  
     5.7 +
     5.8 +lemma interval_upperbound_Times: 
     5.9 +  assumes "A \<noteq> {}" and "B \<noteq> {}"
    5.10 +  shows "interval_upperbound (A \<times> B) = (interval_upperbound A, interval_upperbound B)"
    5.11 +proof-
    5.12 +  from assms have fst_image_times': "A = fst ` (A \<times> B)" by simp
    5.13 +  have "(\<Sum>i\<in>Basis. (SUP x:A \<times> B. x \<bullet> (i, 0)) *\<^sub>R i) = (\<Sum>i\<in>Basis. (SUP x:A. x \<bullet> i) *\<^sub>R i)"
    5.14 +      by (subst (2) fst_image_times') (simp del: fst_image_times add: o_def inner_Pair_0)
    5.15 +  moreover from assms have snd_image_times': "B = snd ` (A \<times> B)" by simp
    5.16 +  have "(\<Sum>i\<in>Basis. (SUP x:A \<times> B. x \<bullet> (0, i)) *\<^sub>R i) = (\<Sum>i\<in>Basis. (SUP x:B. x \<bullet> i) *\<^sub>R i)"
    5.17 +      by (subst (2) snd_image_times') (simp del: snd_image_times add: o_def inner_Pair_0)
    5.18 +  ultimately show ?thesis unfolding interval_upperbound_def
    5.19 +      by (subst setsum_Basis_prod_eq) (auto simp add: setsum_prod)
    5.20 +qed
    5.21 +
    5.22 +lemma interval_lowerbound_Times: 
    5.23 +  assumes "A \<noteq> {}" and "B \<noteq> {}"
    5.24 +  shows "interval_lowerbound (A \<times> B) = (interval_lowerbound A, interval_lowerbound B)"
    5.25 +proof-
    5.26 +  from assms have fst_image_times': "A = fst ` (A \<times> B)" by simp
    5.27 +  have "(\<Sum>i\<in>Basis. (INF x:A \<times> B. x \<bullet> (i, 0)) *\<^sub>R i) = (\<Sum>i\<in>Basis. (INF x:A. x \<bullet> i) *\<^sub>R i)"
    5.28 +      by (subst (2) fst_image_times') (simp del: fst_image_times add: o_def inner_Pair_0)
    5.29 +  moreover from assms have snd_image_times': "B = snd ` (A \<times> B)" by simp
    5.30 +  have "(\<Sum>i\<in>Basis. (INF x:A \<times> B. x \<bullet> (0, i)) *\<^sub>R i) = (\<Sum>i\<in>Basis. (INF x:B. x \<bullet> i) *\<^sub>R i)"
    5.31 +      by (subst (2) snd_image_times') (simp del: snd_image_times add: o_def inner_Pair_0)
    5.32 +  ultimately show ?thesis unfolding interval_lowerbound_def
    5.33 +      by (subst setsum_Basis_prod_eq) (auto simp add: setsum_prod)
    5.34 +qed
    5.35 +
    5.36  subsection {* Content (length, area, volume...) of an interval. *}
    5.37  
    5.38  definition "content (s::('a::euclidean_space) set) =
    5.39 @@ -619,6 +648,20 @@
    5.40  lemma content_lt_nz: "0 < content (cbox a b) \<longleftrightarrow> content (cbox a b) \<noteq> 0"
    5.41    unfolding content_pos_lt_eq content_eq_0 unfolding not_ex not_le by fastforce
    5.42  
    5.43 +lemma content_times[simp]: "content (A \<times> B) = content A * content B"
    5.44 +proof (cases "A \<times> B = {}")
    5.45 +  let ?ub1 = "interval_upperbound" and ?lb1 = "interval_lowerbound"
    5.46 +  let ?ub2 = "interval_upperbound" and ?lb2 = "interval_lowerbound"
    5.47 +  assume nonempty: "A \<times> B \<noteq> {}"
    5.48 +  hence "content (A \<times> B) = (\<Prod>i\<in>Basis. (?ub1 A, ?ub2 B) \<bullet> i - (?lb1 A, ?lb2 B) \<bullet> i)" 
    5.49 +      unfolding content_def by (simp add: interval_upperbound_Times interval_lowerbound_Times)
    5.50 +  also have "... = content A * content B" unfolding content_def using nonempty
    5.51 +    apply (subst Basis_prod_def, subst setprod.union_disjoint, force, force, force, simp)
    5.52 +    apply (subst (1 2) setprod.reindex, auto intro: inj_onI)
    5.53 +    done
    5.54 +  finally show ?thesis .
    5.55 +qed (auto simp: content_def)
    5.56 +
    5.57  
    5.58  subsection {* The notion of a gauge --- simply an open set containing the point. *}
    5.59  
     6.1 --- a/src/HOL/Probability/Bochner_Integration.thy	Thu Jan 22 13:21:45 2015 +0100
     6.2 +++ b/src/HOL/Probability/Bochner_Integration.thy	Thu Jan 22 14:51:08 2015 +0100
     6.3 @@ -2059,6 +2059,41 @@
     6.4    by (subst lebesgue_integral_count_space_finite_support)
     6.5       (auto intro!: setsum.mono_neutral_cong_left)
     6.6  
     6.7 +lemma integrable_count_space_nat_iff:
     6.8 +  fixes f :: "nat \<Rightarrow> _::{banach,second_countable_topology}"
     6.9 +  shows "integrable (count_space UNIV) f \<longleftrightarrow> summable (\<lambda>x. norm (f x))"
    6.10 +  by (auto simp add: integrable_iff_bounded nn_integral_count_space_nat summable_ereal suminf_ereal_finite)
    6.11 +
    6.12 +lemma sums_integral_count_space_nat:
    6.13 +  fixes f :: "nat \<Rightarrow> _::{banach,second_countable_topology}"
    6.14 +  assumes *: "integrable (count_space UNIV) f"
    6.15 +  shows "f sums (integral\<^sup>L (count_space UNIV) f)"
    6.16 +proof -
    6.17 +  let ?f = "\<lambda>n i. indicator {n} i *\<^sub>R f i"
    6.18 +  have f': "\<And>n i. ?f n i = indicator {n} i *\<^sub>R f n"
    6.19 +    by (auto simp: fun_eq_iff split: split_indicator)
    6.20 +
    6.21 +  have "(\<lambda>i. \<integral>n. ?f i n \<partial>count_space UNIV) sums \<integral> n. (\<Sum>i. ?f i n) \<partial>count_space UNIV"
    6.22 +  proof (rule sums_integral)
    6.23 +    show "\<And>i. integrable (count_space UNIV) (?f i)"
    6.24 +      using * by (intro integrable_mult_indicator) auto
    6.25 +    show "AE n in count_space UNIV. summable (\<lambda>i. norm (?f i n))"
    6.26 +      using summable_finite[of "{n}" "\<lambda>i. norm (?f i n)" for n] by simp
    6.27 +    show "summable (\<lambda>i. \<integral> n. norm (?f i n) \<partial>count_space UNIV)"
    6.28 +      using * by (subst f') (simp add: integrable_count_space_nat_iff)
    6.29 +  qed
    6.30 +  also have "(\<integral> n. (\<Sum>i. ?f i n) \<partial>count_space UNIV) = (\<integral>n. f n \<partial>count_space UNIV)"
    6.31 +    using suminf_finite[of "{n}" "\<lambda>i. ?f i n" for n] by (auto intro!: integral_cong)
    6.32 +  also have "(\<lambda>i. \<integral>n. ?f i n \<partial>count_space UNIV) = f"
    6.33 +    by (subst f') simp
    6.34 +  finally show ?thesis .
    6.35 +qed
    6.36 +
    6.37 +lemma integral_count_space_nat:
    6.38 +  fixes f :: "nat \<Rightarrow> _::{banach,second_countable_topology}"
    6.39 +  shows "integrable (count_space UNIV) f \<Longrightarrow> integral\<^sup>L (count_space UNIV) f = (\<Sum>x. f x)"
    6.40 +  using sums_integral_count_space_nat by (rule sums_unique)
    6.41 +
    6.42  subsection {* Point measure *}
    6.43  
    6.44  lemma lebesgue_integral_point_measure_finite:
    6.45 @@ -2076,6 +2111,20 @@
    6.46    apply (auto simp: AE_count_space integrable_count_space)
    6.47    done
    6.48  
    6.49 +subsection {* Lebesgue integration on @{const null_measure} *}
    6.50 +
    6.51 +lemma has_bochner_integral_null_measure_iff[iff]:
    6.52 +  "has_bochner_integral (null_measure M) f 0 \<longleftrightarrow> f \<in> borel_measurable M"
    6.53 +  by (auto simp add: has_bochner_integral.simps simple_bochner_integral_def[abs_def]
    6.54 +           intro!: exI[of _ "\<lambda>n x. 0"] simple_bochner_integrable.intros)
    6.55 +
    6.56 +lemma integrable_null_measure_iff[iff]: "integrable (null_measure M) f \<longleftrightarrow> f \<in> borel_measurable M"
    6.57 +  by (auto simp add: integrable.simps)
    6.58 +
    6.59 +lemma integral_null_measure[simp]: "integral\<^sup>L (null_measure M) f = 0"
    6.60 +  by (cases "integrable (null_measure M) f")
    6.61 +     (auto simp add: not_integrable_integral_eq has_bochner_integral_integral_eq)
    6.62 +
    6.63  subsection {* Legacy lemmas for the real-valued Lebesgue integral *}
    6.64  
    6.65  lemma real_lebesgue_integral_def:
     7.1 --- a/src/HOL/Probability/Finite_Product_Measure.thy	Thu Jan 22 13:21:45 2015 +0100
     7.2 +++ b/src/HOL/Probability/Finite_Product_Measure.thy	Thu Jan 22 14:51:08 2015 +0100
     7.3 @@ -180,6 +180,37 @@
     7.4  translations
     7.5    "PIM x:I. M" == "CONST PiM I (%x. M)"
     7.6  
     7.7 +lemma extend_measure_cong:
     7.8 +  assumes "\<Omega> = \<Omega>'" "I = I'" "G = G'" "\<And>i. i \<in> I' \<Longrightarrow> \<mu> i = \<mu>' i"
     7.9 +  shows "extend_measure \<Omega> I G \<mu> = extend_measure \<Omega>' I' G' \<mu>'"
    7.10 +  unfolding extend_measure_def by (auto simp add: assms)
    7.11 +
    7.12 +lemma Pi_cong_sets:
    7.13 +    "\<lbrakk>I = J; \<And>x. x \<in> I \<Longrightarrow> M x = N x\<rbrakk> \<Longrightarrow> Pi I M = Pi J N"
    7.14 +  unfolding Pi_def by auto 
    7.15 +
    7.16 +lemma PiM_cong:
    7.17 +  assumes "I = J" "\<And>x. x \<in> I \<Longrightarrow> M x = N x"
    7.18 +  shows "PiM I M = PiM J N"
    7.19 +unfolding PiM_def
    7.20 +proof (rule extend_measure_cong)
    7.21 +  case goal1 show ?case using assms
    7.22 +    by (subst assms(1), intro PiE_cong[of J "\<lambda>i. space (M i)" "\<lambda>i. space (N i)"]) simp_all
    7.23 +next
    7.24 +  case goal2
    7.25 +  have "\<And>K. K \<subseteq> J \<Longrightarrow> (\<Pi> j\<in>K. sets (M j)) = (\<Pi> j\<in>K. sets (N j))"
    7.26 +    using assms by (intro Pi_cong_sets) auto
    7.27 +  thus ?case by (auto simp: assms)
    7.28 +next
    7.29 +  case goal3 show ?case using assms 
    7.30 +    by (intro ext) (auto simp: prod_emb_def dest: PiE_mem)
    7.31 +next
    7.32 +  case (goal4 x)
    7.33 +  thus ?case using assms 
    7.34 +    by (auto intro!: setprod.cong split: split_if_asm)
    7.35 +qed
    7.36 +
    7.37 +
    7.38  lemma prod_algebra_sets_into_space:
    7.39    "prod_algebra I M \<subseteq> Pow (\<Pi>\<^sub>E i\<in>I. space (M i))"
    7.40    by (auto simp: prod_emb_def prod_algebra_def)
    7.41 @@ -624,6 +655,17 @@
    7.42  lemma measurable_restrict_subset: "J \<subseteq> L \<Longrightarrow> (\<lambda>f. restrict f J) \<in> measurable (Pi\<^sub>M L M) (Pi\<^sub>M J M)"
    7.43    by (intro measurable_restrict measurable_component_singleton) auto
    7.44  
    7.45 +lemma measurable_restrict_subset':
    7.46 +  assumes "J \<subseteq> L" "\<And>x. x \<in> J \<Longrightarrow> sets (M x) = sets (N x)"
    7.47 +  shows "(\<lambda>f. restrict f J) \<in> measurable (Pi\<^sub>M L M) (Pi\<^sub>M J N)"
    7.48 +proof-
    7.49 +  from assms(1) have "(\<lambda>f. restrict f J) \<in> measurable (Pi\<^sub>M L M) (Pi\<^sub>M J M)"
    7.50 +    by (rule measurable_restrict_subset)
    7.51 +  also from assms(2) have "measurable (Pi\<^sub>M L M) (Pi\<^sub>M J M) = measurable (Pi\<^sub>M L M) (Pi\<^sub>M J N)"
    7.52 +    by (intro sets_PiM_cong measurable_cong_sets) simp_all
    7.53 +  finally show ?thesis .
    7.54 +qed
    7.55 +
    7.56  lemma measurable_prod_emb[intro, simp]:
    7.57    "J \<subseteq> L \<Longrightarrow> X \<in> sets (Pi\<^sub>M J M) \<Longrightarrow> prod_emb L M J X \<in> sets (Pi\<^sub>M L M)"
    7.58    unfolding prod_emb_def space_PiM[symmetric]
    7.59 @@ -945,6 +987,17 @@
    7.60    qed
    7.61  qed
    7.62  
    7.63 +lemma (in product_sigma_finite) product_nn_integral_insert_rev:
    7.64 +  assumes I[simp]: "finite I" "i \<notin> I"
    7.65 +    and [measurable]: "f \<in> borel_measurable (Pi\<^sub>M (insert i I) M)"
    7.66 +  shows "integral\<^sup>N (Pi\<^sub>M (insert i I) M) f = (\<integral>\<^sup>+ y. (\<integral>\<^sup>+ x. f (x(i := y)) \<partial>(Pi\<^sub>M I M)) \<partial>(M i))"
    7.67 +  apply (subst product_nn_integral_insert[OF assms])
    7.68 +  apply (rule pair_sigma_finite.Fubini')
    7.69 +  apply intro_locales []
    7.70 +  apply (rule sigma_finite[OF I(1)])
    7.71 +  apply measurable
    7.72 +  done
    7.73 +
    7.74  lemma (in product_sigma_finite) product_nn_integral_setprod:
    7.75    fixes f :: "'i \<Rightarrow> 'a \<Rightarrow> ereal"
    7.76    assumes "finite I" and borel: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> borel_measurable (M i)"
    7.77 @@ -969,6 +1022,23 @@
    7.78      done
    7.79  qed (simp add: space_PiM)
    7.80  
    7.81 +lemma (in product_sigma_finite) product_nn_integral_pair:
    7.82 +  assumes [measurable]: "split f \<in> borel_measurable (M x \<Otimes>\<^sub>M M y)"
    7.83 +  assumes xy: "x \<noteq> y"
    7.84 +  shows "(\<integral>\<^sup>+\<sigma>. f (\<sigma> x) (\<sigma> y) \<partial>PiM {x, y} M) = (\<integral>\<^sup>+z. f (fst z) (snd z) \<partial>(M x \<Otimes>\<^sub>M M y))"
    7.85 +proof-
    7.86 +  interpret psm: pair_sigma_finite "M x" "M y"
    7.87 +    unfolding pair_sigma_finite_def using sigma_finite_measures by simp_all
    7.88 +  have "{x, y} = {y, x}" by auto
    7.89 +  also have "(\<integral>\<^sup>+\<sigma>. f (\<sigma> x) (\<sigma> y) \<partial>PiM {y, x} M) = (\<integral>\<^sup>+y. \<integral>\<^sup>+\<sigma>. f (\<sigma> x) y \<partial>PiM {x} M \<partial>M y)"
    7.90 +    using xy by (subst product_nn_integral_insert_rev) simp_all
    7.91 +  also have "... = (\<integral>\<^sup>+y. \<integral>\<^sup>+x. f x y \<partial>M x \<partial>M y)"
    7.92 +    by (intro nn_integral_cong, subst product_nn_integral_singleton) simp_all
    7.93 +  also have "... = (\<integral>\<^sup>+z. f (fst z) (snd z) \<partial>(M x \<Otimes>\<^sub>M M y))"
    7.94 +    by (subst psm.nn_integral_snd[symmetric]) simp_all
    7.95 +  finally show ?thesis .
    7.96 +qed
    7.97 +
    7.98  lemma (in product_sigma_finite) distr_component:
    7.99    "distr (M i) (Pi\<^sub>M {i} M) (\<lambda>x. \<lambda>i\<in>{i}. x) = Pi\<^sub>M {i} M" (is "?D = ?P")
   7.100  proof (intro measure_eqI[symmetric])
     8.1 --- a/src/HOL/Probability/Giry_Monad.thy	Thu Jan 22 13:21:45 2015 +0100
     8.2 +++ b/src/HOL/Probability/Giry_Monad.thy	Thu Jan 22 14:51:08 2015 +0100
     8.3 @@ -32,6 +32,9 @@
     8.4    "prob_space M \<Longrightarrow> subprob_space M"
     8.5    by (rule subprob_spaceI) (simp_all add: prob_space.emeasure_space_1 prob_space.not_empty)
     8.6  
     8.7 +lemma subprob_space_imp_sigma_finite: "subprob_space M \<Longrightarrow> sigma_finite_measure M"
     8.8 +  unfolding subprob_space_def finite_measure_def by simp
     8.9 +
    8.10  sublocale prob_space \<subseteq> subprob_space
    8.11    by (rule subprob_spaceI) (simp_all add: emeasure_space_1 not_empty)
    8.12  
    8.13 @@ -123,6 +126,10 @@
    8.14      by (simp add: space_pair_measure)
    8.15  qed
    8.16  
    8.17 +lemma subprob_space_null_measure_iff:
    8.18 +    "subprob_space (null_measure M) \<longleftrightarrow> space M \<noteq> {}"
    8.19 +  by (auto intro!: subprob_spaceI dest: subprob_space.subprob_not_empty)
    8.20 +
    8.21  definition subprob_algebra :: "'a measure \<Rightarrow> 'a measure measure" where
    8.22    "subprob_algebra K =
    8.23      (\<Squnion>\<^sub>\<sigma> A\<in>sets K. vimage_algebra {M. subprob_space M \<and> sets M = sets K} (\<lambda>M. emeasure M A) borel)"
    8.24 @@ -1250,4 +1257,18 @@
    8.25      by (simp add: emeasure_notin_sets)
    8.26  qed
    8.27  
    8.28 +lemma bind_return'': "sets M = sets N \<Longrightarrow> M \<guillemotright>= return N = M"
    8.29 +   by (cases "space M = {}")
    8.30 +      (simp_all add: bind_empty space_empty[symmetric] bind_nonempty join_return'
    8.31 +                cong: subprob_algebra_cong)
    8.32 +
    8.33 +lemma (in prob_space) distr_const[simp]:
    8.34 +  "c \<in> space N \<Longrightarrow> distr M N (\<lambda>x. c) = return N c"
    8.35 +  by (rule measure_eqI) (auto simp: emeasure_distr emeasure_space_1)
    8.36 +
    8.37 +lemma return_count_space_eq_density:
    8.38 +    "return (count_space M) x = density (count_space M) (indicator {x})"
    8.39 +  by (rule measure_eqI) 
    8.40 +     (auto simp: indicator_inter_arith_ereal emeasure_density split: split_indicator)
    8.41 +
    8.42  end
     9.1 --- a/src/HOL/Probability/Lebesgue_Measure.thy	Thu Jan 22 13:21:45 2015 +0100
     9.2 +++ b/src/HOL/Probability/Lebesgue_Measure.thy	Thu Jan 22 14:51:08 2015 +0100
     9.3 @@ -529,6 +529,23 @@
     9.4    thus ?thesis by (auto simp add: emeasure_le_0_iff)
     9.5  qed
     9.6  
     9.7 +lemma countable_imp_null_set_lborel: "countable A \<Longrightarrow> A \<in> null_sets lborel"
     9.8 +  by (simp add: null_sets_def emeasure_lborel_countable sets.countable)
     9.9 +
    9.10 +lemma finite_imp_null_set_lborel: "finite A \<Longrightarrow> A \<in> null_sets lborel"
    9.11 +  by (intro countable_imp_null_set_lborel countable_finite)
    9.12 +
    9.13 +lemma lborel_neq_count_space[simp]: "lborel \<noteq> count_space (A::('a::ordered_euclidean_space) set)"
    9.14 +proof
    9.15 +  assume asm: "lborel = count_space A"
    9.16 +  have "space lborel = UNIV" by simp
    9.17 +  hence [simp]: "A = UNIV" by (subst (asm) asm) (simp only: space_count_space)
    9.18 +  have "emeasure lborel {undefined::'a} = 1" 
    9.19 +      by (subst asm, subst emeasure_count_space_finite) auto
    9.20 +  moreover have "emeasure lborel {undefined} \<noteq> 1" by simp
    9.21 +  ultimately show False by contradiction
    9.22 +qed
    9.23 +
    9.24  subsection {* Affine transformation on the Lebesgue-Borel *}
    9.25  
    9.26  lemma lborel_eqI:
    9.27 @@ -651,11 +668,59 @@
    9.28    unfolding has_bochner_integral_iff lborel_integrable_real_affine_iff
    9.29    by (simp_all add: lborel_integral_real_affine[symmetric] divideR_right cong: conj_cong)
    9.30  
    9.31 +lemma lborel_distr_uminus: "distr lborel borel uminus = (lborel :: real measure)"
    9.32 +  by (subst lborel_real_affine[of "-1" 0]) 
    9.33 +     (auto simp: density_1 one_ereal_def[symmetric])
    9.34 +
    9.35 +lemma lborel_distr_mult: 
    9.36 +  assumes "(c::real) \<noteq> 0"
    9.37 +  shows "distr lborel borel (op * c) = density lborel (\<lambda>_. inverse \<bar>c\<bar>)"
    9.38 +proof-
    9.39 +  have "distr lborel borel (op * c) = distr lborel lborel (op * c)" by (simp cong: distr_cong)
    9.40 +  also from assms have "... = density lborel (\<lambda>_. inverse \<bar>c\<bar>)"
    9.41 +    by (subst lborel_real_affine[of "inverse c" 0]) (auto simp: o_def distr_density_distr)
    9.42 +  finally show ?thesis .
    9.43 +qed
    9.44 +
    9.45 +lemma lborel_distr_mult': 
    9.46 +  assumes "(c::real) \<noteq> 0"
    9.47 +  shows "lborel = density (distr lborel borel (op * c)) (\<lambda>_. abs c)"
    9.48 +proof-
    9.49 +  have "lborel = density lborel (\<lambda>_. 1)" by (rule density_1[symmetric])
    9.50 +  also from assms have "(\<lambda>_. 1 :: ereal) = (\<lambda>_. inverse (abs c) * abs c)" by (intro ext) simp
    9.51 +  also have "density lborel ... = density (density lborel (\<lambda>_. inverse (abs c))) (\<lambda>_. abs c)"
    9.52 +    by (subst density_density_eq) auto
    9.53 +  also from assms have "density lborel (\<lambda>_. inverse (abs c)) = distr lborel borel (op * c)"
    9.54 +    by (rule lborel_distr_mult[symmetric])
    9.55 +  finally show ?thesis .
    9.56 +qed
    9.57 +
    9.58 +lemma lborel_distr_plus: "distr lborel borel (op + c) = (lborel :: real measure)"
    9.59 +  by (subst lborel_real_affine[of 1 c]) (auto simp: density_1 one_ereal_def[symmetric])
    9.60 +
    9.61  interpretation lborel!: sigma_finite_measure lborel
    9.62    by (rule sigma_finite_lborel)
    9.63  
    9.64  interpretation lborel_pair: pair_sigma_finite lborel lborel ..
    9.65  
    9.66 +lemma lborel_prod:
    9.67 +  "lborel \<Otimes>\<^sub>M lborel = (lborel :: ('a::euclidean_space \<times> 'b::euclidean_space) measure)"
    9.68 +proof (rule lborel_eqI[symmetric], clarify)
    9.69 +  fix la ua :: 'a and lb ub :: 'b
    9.70 +  assume lu: "\<And>a b. (a, b) \<in> Basis \<Longrightarrow> (la, lb) \<bullet> (a, b) \<le> (ua, ub) \<bullet> (a, b)"
    9.71 +  have [simp]:
    9.72 +    "\<And>b. b \<in> Basis \<Longrightarrow> la \<bullet> b \<le> ua \<bullet> b"
    9.73 +    "\<And>b. b \<in> Basis \<Longrightarrow> lb \<bullet> b \<le> ub \<bullet> b"
    9.74 +    "inj_on (\<lambda>u. (u, 0)) Basis" "inj_on (\<lambda>u. (0, u)) Basis"
    9.75 +    "(\<lambda>u. (u, 0)) ` Basis \<inter> (\<lambda>u. (0, u)) ` Basis = {}"
    9.76 +    "box (la, lb) (ua, ub) = box la ua \<times> box lb ub"
    9.77 +    using lu[of _ 0] lu[of 0] by (auto intro!: inj_onI simp add: Basis_prod_def ball_Un box_def)
    9.78 +  show "emeasure (lborel \<Otimes>\<^sub>M lborel) (box (la, lb) (ua, ub)) =
    9.79 +      ereal (setprod (op \<bullet> ((ua, ub) - (la, lb))) Basis)"
    9.80 +    by (simp add: lborel.emeasure_pair_measure_Times Basis_prod_def setprod.union_disjoint
    9.81 +                  setprod.reindex)
    9.82 +qed (simp add: borel_prod[symmetric])
    9.83 +
    9.84  (* FIXME: conversion in measurable prover *)
    9.85  lemma lborelD_Collect[measurable (raw)]: "{x\<in>space borel. P x} \<in> sets borel \<Longrightarrow> {x\<in>space lborel. P x} \<in> sets lborel" by simp
    9.86  lemma lborelD[measurable (raw)]: "A \<in> sets borel \<Longrightarrow> A \<in> sets lborel" by simp
    10.1 --- a/src/HOL/Probability/Measure_Space.thy	Thu Jan 22 13:21:45 2015 +0100
    10.2 +++ b/src/HOL/Probability/Measure_Space.thy	Thu Jan 22 14:51:08 2015 +0100
    10.3 @@ -1928,5 +1928,23 @@
    10.4    finally show "emeasure M X = emeasure N X" .
    10.5  qed fact
    10.6  
    10.7 +subsection {* Null measure *}
    10.8 +
    10.9 +definition "null_measure M = sigma (space M) (sets M)"
   10.10 +
   10.11 +lemma space_null_measure[simp]: "space (null_measure M) = space M"
   10.12 +  by (simp add: null_measure_def)
   10.13 +
   10.14 +lemma sets_null_measure[simp, measurable_cong]: "sets (null_measure M) = sets M" 
   10.15 +  by (simp add: null_measure_def)
   10.16 +
   10.17 +lemma emeasure_null_measure[simp]: "emeasure (null_measure M) X = 0"
   10.18 +  by (cases "X \<in> sets M", rule emeasure_measure_of)
   10.19 +     (auto simp: positive_def countably_additive_def emeasure_notin_sets null_measure_def
   10.20 +           dest: sets.sets_into_space)
   10.21 +
   10.22 +lemma measure_null_measure[simp]: "measure (null_measure M) X = 0"
   10.23 +  by (simp add: measure_def)
   10.24 +
   10.25  end
   10.26  
    11.1 --- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Thu Jan 22 13:21:45 2015 +0100
    11.2 +++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Thu Jan 22 14:51:08 2015 +0100
    11.3 @@ -1951,6 +1951,11 @@
    11.4    shows "(\<integral>\<^sup>+x. f x \<partial>count_space X) = (\<integral>\<^sup>+x. f x * indicator X x \<partial>count_space UNIV)"
    11.5    by (simp add: nn_integral_restrict_space[symmetric] restrict_count_space)
    11.6  
    11.7 +lemma nn_integral_count_space_eq:
    11.8 +  "(\<And>x. x \<in> A - B \<Longrightarrow> f x = 0) \<Longrightarrow> (\<And>x. x \<in> B - A \<Longrightarrow> f x = 0) \<Longrightarrow>
    11.9 +    (\<integral>\<^sup>+x. f x \<partial>count_space A) = (\<integral>\<^sup>+x. f x \<partial>count_space B)"
   11.10 +  by (auto simp: nn_integral_count_space_indicator intro!: nn_integral_cong split: split_indicator)
   11.11 +
   11.12  lemma nn_integral_ge_point:
   11.13    assumes "x \<in> A"
   11.14    shows "p x \<le> \<integral>\<^sup>+ x. p x \<partial>count_space A"
   11.15 @@ -2194,6 +2199,23 @@
   11.16      using f g by (subst density_density_eq) auto
   11.17  qed
   11.18  
   11.19 +lemma density_1: "density M (\<lambda>_. 1) = M"
   11.20 +  by (intro measure_eqI) (auto simp: emeasure_density)
   11.21 +
   11.22 +lemma emeasure_density_add:
   11.23 +  assumes X: "X \<in> sets M" 
   11.24 +  assumes Mf[measurable]: "f \<in> borel_measurable M"
   11.25 +  assumes Mg[measurable]: "g \<in> borel_measurable M"
   11.26 +  assumes nonnegf: "\<And>x. x \<in> space M \<Longrightarrow> f x \<ge> 0"
   11.27 +  assumes nonnegg: "\<And>x. x \<in> space M \<Longrightarrow> g x \<ge> 0"
   11.28 +  shows "emeasure (density M f) X + emeasure (density M g) X = 
   11.29 +           emeasure (density M (\<lambda>x. f x + g x)) X"
   11.30 +  using assms
   11.31 +  apply (subst (1 2 3) emeasure_density, simp_all) []
   11.32 +  apply (subst nn_integral_add[symmetric], simp_all) []
   11.33 +  apply (intro nn_integral_cong, simp split: split_indicator)
   11.34 +  done
   11.35 +
   11.36  subsubsection {* Point measure *}
   11.37  
   11.38  definition point_measure :: "'a set \<Rightarrow> ('a \<Rightarrow> ereal) \<Rightarrow> 'a measure" where
   11.39 @@ -2351,6 +2373,21 @@
   11.40      unfolding uniform_measure_def by (simp add: AE_density)
   11.41  qed
   11.42  
   11.43 +subsubsection {* Null measure *}
   11.44 +
   11.45 +lemma null_measure_eq_density: "null_measure M = density M (\<lambda>_. 0)"
   11.46 +  by (intro measure_eqI) (simp_all add: emeasure_density)
   11.47 +
   11.48 +lemma nn_integral_null_measure[simp]: "(\<integral>\<^sup>+x. f x \<partial>null_measure M) = 0"
   11.49 +  by (auto simp add: nn_integral_def simple_integral_def SUP_constant bot_ereal_def le_fun_def
   11.50 +           intro!: exI[of _ "\<lambda>x. 0"])
   11.51 +
   11.52 +lemma density_null_measure[simp]: "density (null_measure M) f = null_measure M"
   11.53 +proof (intro measure_eqI)
   11.54 +  fix A show "emeasure (density (null_measure M) f) A = emeasure (null_measure M) A"
   11.55 +    by (simp add: density_def) (simp only: null_measure_def[symmetric] emeasure_null_measure)
   11.56 +qed simp
   11.57 +
   11.58  subsubsection {* Uniform count measure *}
   11.59  
   11.60  definition "uniform_count_measure A = point_measure A (\<lambda>x. 1 / card A)"
    12.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Thu Jan 22 13:21:45 2015 +0100
    12.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Thu Jan 22 14:51:08 2015 +0100
    12.3 @@ -12,16 +12,6 @@
    12.4    "~~/src/HOL/Library/Multiset"
    12.5  begin
    12.6  
    12.7 -lemma bind_return'': "sets M = sets N \<Longrightarrow> M \<guillemotright>= return N = M"
    12.8 -   by (cases "space M = {}")
    12.9 -      (simp_all add: bind_empty space_empty[symmetric] bind_nonempty join_return'
   12.10 -                cong: subprob_algebra_cong)
   12.11 -
   12.12 -
   12.13 -lemma (in prob_space) distr_const[simp]:
   12.14 -  "c \<in> space N \<Longrightarrow> distr M N (\<lambda>x. c) = return N c"
   12.15 -  by (rule measure_eqI) (auto simp: emeasure_distr emeasure_space_1)
   12.16 -
   12.17  lemma (in finite_measure) countable_support:
   12.18    "countable {x. measure M {x} \<noteq> 0}"
   12.19  proof cases
   12.20 @@ -214,8 +204,7 @@
   12.21    by (subst emeasure_eq_setsum_singleton) (auto simp: emeasure_pmf_single)
   12.22  
   12.23  lemma measure_measure_pmf_finite: "finite S \<Longrightarrow> measure (measure_pmf M) S = setsum (pmf M) S"
   12.24 -using emeasure_measure_pmf_finite[of S M]
   12.25 -by(simp add: measure_pmf.emeasure_eq_measure)
   12.26 +  using emeasure_measure_pmf_finite[of S M] by(simp add: measure_pmf.emeasure_eq_measure)
   12.27  
   12.28  lemma nn_integral_measure_pmf_support:
   12.29    fixes f :: "'a \<Rightarrow> ereal"
   12.30 @@ -759,33 +748,34 @@
   12.31                intro!: measure_pmf.integrable_const_bound[where B=1])
   12.32    done
   12.33  
   12.34 +
   12.35  lemma measurable_pair_restrict_pmf2:
   12.36    assumes "countable A"
   12.37 -  assumes "\<And>y. y \<in> A \<Longrightarrow> (\<lambda>x. f (x, y)) \<in> measurable M L"
   12.38 -  shows "f \<in> measurable (M \<Otimes>\<^sub>M restrict_space (measure_pmf N) A) L"
   12.39 -  apply (subst measurable_cong_sets)
   12.40 -  apply (rule sets_pair_measure_cong sets_restrict_space_cong sets_measure_pmf_count_space refl)+
   12.41 -  apply (simp_all add: restrict_count_space)
   12.42 -  apply (subst split_eta[symmetric])
   12.43 -  unfolding measurable_split_conv
   12.44 -  apply (rule measurable_compose_countable'[OF _ measurable_snd `countable A`])
   12.45 -  apply (rule measurable_compose[OF measurable_fst])
   12.46 -  apply fact
   12.47 -  done
   12.48 +  assumes [measurable]: "\<And>y. y \<in> A \<Longrightarrow> (\<lambda>x. f (x, y)) \<in> measurable M L"
   12.49 +  shows "f \<in> measurable (M \<Otimes>\<^sub>M restrict_space (measure_pmf N) A) L" (is "f \<in> measurable ?M _")
   12.50 +proof -
   12.51 +  have [measurable_cong]: "sets (restrict_space (count_space UNIV) A) = sets (count_space A)"
   12.52 +    by (simp add: restrict_count_space)
   12.53 +
   12.54 +  show ?thesis
   12.55 +    by (intro measurable_compose_countable'[where f="\<lambda>a b. f (fst b, a)" and g=snd and I=A,
   12.56 +                                            unfolded pair_collapse] assms)
   12.57 +        measurable
   12.58 +qed
   12.59  
   12.60  lemma measurable_pair_restrict_pmf1:
   12.61    assumes "countable A"
   12.62 -  assumes "\<And>x. x \<in> A \<Longrightarrow> (\<lambda>y. f (x, y)) \<in> measurable N L"
   12.63 +  assumes [measurable]: "\<And>x. x \<in> A \<Longrightarrow> (\<lambda>y. f (x, y)) \<in> measurable N L"
   12.64    shows "f \<in> measurable (restrict_space (measure_pmf M) A \<Otimes>\<^sub>M N) L"
   12.65 -  apply (subst measurable_cong_sets)
   12.66 -  apply (rule sets_pair_measure_cong sets_restrict_space_cong sets_measure_pmf_count_space refl)+
   12.67 -  apply (simp_all add: restrict_count_space)
   12.68 -  apply (subst split_eta[symmetric])
   12.69 -  unfolding measurable_split_conv
   12.70 -  apply (rule measurable_compose_countable'[OF _ measurable_fst `countable A`])
   12.71 -  apply (rule measurable_compose[OF measurable_snd])
   12.72 -  apply fact
   12.73 -  done
   12.74 +proof -
   12.75 +  have [measurable_cong]: "sets (restrict_space (count_space UNIV) A) = sets (count_space A)"
   12.76 +    by (simp add: restrict_count_space)
   12.77 +
   12.78 +  show ?thesis
   12.79 +    by (intro measurable_compose_countable'[where f="\<lambda>a b. f (a, snd b)" and g=fst and I=A,
   12.80 +                                            unfolded pair_collapse] assms)
   12.81 +        measurable
   12.82 +qed
   12.83                                  
   12.84  lemma bind_commute_pmf: "bind_pmf A (\<lambda>x. bind_pmf B (C x)) = bind_pmf B (\<lambda>y. bind_pmf A (\<lambda>x. C x y))"
   12.85    unfolding pmf_eq_iff pmf_bind
   12.86 @@ -993,11 +983,6 @@
   12.87       map_pmf fst pq = p; map_pmf snd pq = q \<rbrakk>
   12.88    \<Longrightarrow> rel_pmf R p q"
   12.89  
   12.90 -lemma nn_integral_count_space_eq:
   12.91 -  "(\<And>x. x \<in> A - B \<Longrightarrow> f x = 0) \<Longrightarrow> (\<And>x. x \<in> B - A \<Longrightarrow> f x = 0) \<Longrightarrow>
   12.92 -    (\<integral>\<^sup>+x. f x \<partial>count_space A) = (\<integral>\<^sup>+x. f x \<partial>count_space B)"
   12.93 -  by (auto simp: nn_integral_count_space_indicator intro!: nn_integral_cong split: split_indicator)
   12.94 -
   12.95  bnf pmf: "'a pmf" map: map_pmf sets: set_pmf bd : "natLeq" rel: rel_pmf
   12.96  proof -
   12.97    show "map_pmf id = id" by (rule map_pmf_id)
    13.1 --- a/src/HOL/Probability/Probability_Measure.thy	Thu Jan 22 13:21:45 2015 +0100
    13.2 +++ b/src/HOL/Probability/Probability_Measure.thy	Thu Jan 22 14:51:08 2015 +0100
    13.3 @@ -23,6 +23,9 @@
    13.4    show "prob_space M" by default fact
    13.5  qed
    13.6  
    13.7 +lemma prob_space_imp_sigma_finite: "prob_space M \<Longrightarrow> sigma_finite_measure M"
    13.8 +  unfolding prob_space_def finite_measure_def by simp
    13.9 +
   13.10  abbreviation (in prob_space) "events \<equiv> sets M"
   13.11  abbreviation (in prob_space) "prob \<equiv> measure M"
   13.12  abbreviation (in prob_space) "random_variable M' X \<equiv> X \<in> measurable M M'"