# HG changeset patch
# User hoelzl
# Date 1421934668 -3600
# Node ID c5e79df8cc21363647eb020efad99aa34bbe7874
# Parent  ca2336984f6a6b40280b974713265d9c53bc6b44
import general thms from Density_Compiler

diff -r ca2336984f6a -r c5e79df8cc21 src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Thu Jan 22 13:21:45 2015 +0100
+++ b/src/HOL/Library/Extended_Real.thy	Thu Jan 22 14:51:08 2015 +0100
@@ -1606,6 +1606,42 @@
     using zero_neq_one by blast
 qed
 
+lemma ereal_Sup:
+  assumes *: "\<bar>SUP a:A. ereal a\<bar> \<noteq> \<infinity>"
+  shows "ereal (Sup A) = (SUP a:A. ereal a)"
+proof (rule antisym)
+  obtain r where r: "ereal r = (SUP a:A. ereal a)" "A \<noteq> {}"
+    using * by (force simp: bot_ereal_def)
+  then have upper: "\<And>a. a \<in> A \<Longrightarrow> a \<le> r"
+    by (auto intro!: SUP_upper simp add: ereal_less_eq(3)[symmetric] simp del: ereal_less_eq)
+
+  show "ereal (Sup A) \<le> (SUP a:A. ereal a)"
+    using upper by (simp add: r[symmetric] cSup_least[OF `A \<noteq> {}`])
+  show "(SUP a:A. ereal a) \<le> ereal (Sup A)"
+    using upper `A \<noteq> {}` by (intro SUP_least) (auto intro!: cSup_upper bdd_aboveI)
+qed
+
+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))"
+  using ereal_Sup[of "f`A"] by auto
+  
+lemma ereal_Inf:
+  assumes *: "\<bar>INF a:A. ereal a\<bar> \<noteq> \<infinity>"
+  shows "ereal (Inf A) = (INF a:A. ereal a)"
+proof (rule antisym)
+  obtain r where r: "ereal r = (INF a:A. ereal a)" "A \<noteq> {}"
+    using * by (force simp: top_ereal_def)
+  then have lower: "\<And>a. a \<in> A \<Longrightarrow> r \<le> a"
+    by (auto intro!: INF_lower simp add: ereal_less_eq(3)[symmetric] simp del: ereal_less_eq)
+
+  show "(INF a:A. ereal a) \<le> ereal (Inf A)"
+    using lower by (simp add: r[symmetric] cInf_greatest[OF `A \<noteq> {}`])
+  show "ereal (Inf A) \<le> (INF a:A. ereal a)"
+    using lower `A \<noteq> {}` by (intro INF_greatest) (auto intro!: cInf_lower bdd_belowI)
+qed
+
+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))"
+  using ereal_Inf[of "f`A"] by auto
+
 lemma ereal_Sup_uminus_image_eq: "Sup (uminus ` S::ereal set) = - Inf S"
   by (auto intro!: SUP_eqI
            simp: Ball_def[symmetric] ereal_uminus_le_reorder le_Inf_iff
@@ -1705,28 +1741,37 @@
     using assms by (cases e) auto
 qed
 
+lemma SUP_PInfty:
+  fixes f :: "'a \<Rightarrow> ereal"
+  assumes "\<And>n::nat. \<exists>i\<in>A. ereal (real n) \<le> f i"
+  shows "(SUP i:A. f i) = \<infinity>"
+  unfolding SUP_def Sup_eq_top_iff[where 'a=ereal, unfolded top_ereal_def]
+  apply simp
+proof safe
+  fix x :: ereal
+  assume "x \<noteq> \<infinity>"
+  show "\<exists>i\<in>A. x < f i"
+  proof (cases x)
+    case PInf
+    with `x \<noteq> \<infinity>` show ?thesis
+      by simp
+  next
+    case MInf
+    with assms[of "0"] show ?thesis
+      by force
+  next
+    case (real r)
+    with less_PInf_Ex_of_nat[of x] obtain n :: nat where "x < ereal (real n)"
+      by auto
+    moreover obtain i where "i \<in> A" "ereal (real n) \<le> f i"
+      using assms ..
+    ultimately show ?thesis
+      by (auto intro!: bexI[of _ i])
+  qed
+qed
+
 lemma SUP_nat_Infty: "(SUP i::nat. ereal (real i)) = \<infinity>"
-proof -
-  {
-    fix x :: ereal
-    assume "x \<noteq> \<infinity>"
-    then have "\<exists>k::nat. x < ereal (real k)"
-    proof (cases x)
-      case MInf
-      then show ?thesis
-        by (intro exI[of _ 0]) auto
-    next
-      case (real r)
-      moreover obtain k :: nat where "r < real k"
-        using ex_less_of_nat by (auto simp: real_eq_of_nat)
-      ultimately show ?thesis
-        by auto
-    qed simp
-  }
-  then show ?thesis
-    using SUP_eq_top_iff[of UNIV "\<lambda>n::nat. ereal (real n)"]
-    by (auto simp: top_ereal_def)
-qed
+  by (rule SUP_PInfty) auto
 
 lemma Inf_less:
   fixes x :: ereal
@@ -1930,35 +1975,6 @@
   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"
   using SUP_ereal_add_left[of I f c] by (simp add: add_ac)
 
-lemma SUP_PInfty:
-  fixes f :: "'a \<Rightarrow> ereal"
-  assumes "\<And>n::nat. \<exists>i\<in>A. ereal (real n) \<le> f i"
-  shows "(SUP i:A. f i) = \<infinity>"
-  unfolding SUP_def Sup_eq_top_iff[where 'a=ereal, unfolded top_ereal_def]
-  apply simp
-proof safe
-  fix x :: ereal
-  assume "x \<noteq> \<infinity>"
-  show "\<exists>i\<in>A. x < f i"
-  proof (cases x)
-    case PInf
-    with `x \<noteq> \<infinity>` show ?thesis
-      by simp
-  next
-    case MInf
-    with assms[of "0"] show ?thesis
-      by force
-  next
-    case (real r)
-    with less_PInf_Ex_of_nat[of x] obtain n :: nat where "x < ereal (real n)"
-      by auto
-    moreover obtain i where "i \<in> A" "ereal (real n) \<le> f i"
-      using assms ..
-    ultimately show ?thesis
-      by (auto intro!: bexI[of _ i])
-  qed
-qed
-
 lemma Sup_countable_SUP:
   assumes "A \<noteq> {}"
   shows "\<exists>f::nat \<Rightarrow> ereal. range f \<subseteq> A \<and> Sup A = SUPREMUM UNIV f"
@@ -2664,13 +2680,6 @@
   by (cases rule: ereal3_cases[of a b c])
     (auto simp add: field_simps not_le mult_le_0_iff mult_less_0_iff)
 
-lemma ereal_pos_le_distrib:
-  fixes a b c :: ereal
-  assumes "c \<ge> 0"
-  shows "c * (a + b) \<le> c * a + c * b"
-  using assms
-  by (cases rule: ereal3_cases[of a b c]) (auto simp add: field_simps)
-
 lemma ereal_max_mono: "(a::ereal) \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> max a c \<le> max b d"
   by (metis sup_ereal_def sup_mono)
 
diff -r ca2336984f6a -r c5e79df8cc21 src/HOL/Library/FuncSet.thy
--- a/src/HOL/Library/FuncSet.thy	Thu Jan 22 13:21:45 2015 +0100
+++ b/src/HOL/Library/FuncSet.thy	Thu Jan 22 14:51:08 2015 +0100
@@ -405,16 +405,20 @@
 lemma fun_upd_in_PiE: "x \<notin> S \<Longrightarrow> f \<in> PiE (insert x S) T \<Longrightarrow> f(x := undefined) \<in> PiE S T"
   unfolding PiE_def extensional_def by auto
 
-lemma PiE_insert_eq:
-  assumes "x \<notin> S"
-  shows "PiE (insert x S) T = (\<lambda>(y, g). g(x := y)) ` (T x \<times> PiE S T)"
+lemma PiE_insert_eq: "PiE (insert x S) T = (\<lambda>(y, g). g(x := y)) ` (T x \<times> PiE S T)"
 proof -
   {
-    fix f assume "f \<in> PiE (insert x S) T"
+    fix f assume "f \<in> PiE (insert x S) T" "x \<notin> S"
     with assms have "f \<in> (\<lambda>(y, g). g(x := y)) ` (T x \<times> PiE S T)"
       by (auto intro!: image_eqI[where x="(f x, f(x := undefined))"] intro: fun_upd_in_PiE PiE_mem)
   }
-  then show ?thesis
+  moreover
+  {
+    fix f assume "f \<in> PiE (insert x S) T" "x \<in> S"
+    with assms have "f \<in> (\<lambda>(y, g). g(x := y)) ` (T x \<times> PiE S T)"
+      by (auto intro!: image_eqI[where x="(f x, f)"] intro: fun_upd_in_PiE PiE_mem simp: insert_absorb)
+  }
+  ultimately show ?thesis
     using assms by (auto intro: PiE_fun_upd)
 qed
 
diff -r ca2336984f6a -r c5e79df8cc21 src/HOL/Library/Product_Vector.thy
--- a/src/HOL/Library/Product_Vector.thy	Thu Jan 22 13:21:45 2015 +0100
+++ b/src/HOL/Library/Product_Vector.thy	Thu Jan 22 14:51:08 2015 +0100
@@ -538,4 +538,8 @@
 
 end
 
+lemma inner_Pair_0: "inner x (0, b) = inner (snd x) b" "inner x (a, 0) = inner (fst x) a"
+    by (cases x, simp)+
+
+
 end
diff -r ca2336984f6a -r c5e79df8cc21 src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
--- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Thu Jan 22 13:21:45 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Thu Jan 22 14:51:08 2015 +0100
@@ -1175,6 +1175,16 @@
 lemma suminf_ereal_finite: "summable f \<Longrightarrow> (\<Sum>i. ereal (f i)) \<noteq> \<infinity>"
   by (auto simp: sums_ereal[symmetric] summable_def sums_unique[symmetric])
 
+lemma suminf_ereal_finite_neg:
+  assumes "summable f"
+  shows "(\<Sum>x. ereal (f x)) \<noteq> -\<infinity>"
+proof-
+  from assms obtain x where "f sums x" by blast
+  hence "(\<lambda>x. ereal (f x)) sums ereal x" by (simp add: sums_ereal)
+  from sums_unique[OF this] have "(\<Sum>x. ereal (f x)) = ereal x" ..
+  thus "(\<Sum>x. ereal (f x)) \<noteq> -\<infinity>" by simp_all
+qed
+
 subsection {* monoset *}
 
 definition (in order) mono_set:
@@ -1364,4 +1374,8 @@
 lemma ereal_indicator_nonneg[simp, intro]: "0 \<le> (indicator A x ::ereal)"
   unfolding indicator_def by auto
 
+lemma indicator_inter_arith_ereal: "indicator A x * indicator B x = (indicator (A \<inter> B) x :: ereal)"
+  by (simp split: split_indicator)
+
+
 end
diff -r ca2336984f6a -r c5e79df8cc21 src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Thu Jan 22 13:21:45 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Thu Jan 22 14:51:08 2015 +0100
@@ -481,6 +481,35 @@
     and "interval_lowerbound (cbox a b) = a"
   using assms unfolding box_ne_empty by auto
 
+
+lemma interval_upperbound_Times: 
+  assumes "A \<noteq> {}" and "B \<noteq> {}"
+  shows "interval_upperbound (A \<times> B) = (interval_upperbound A, interval_upperbound B)"
+proof-
+  from assms have fst_image_times': "A = fst ` (A \<times> B)" by simp
+  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)"
+      by (subst (2) fst_image_times') (simp del: fst_image_times add: o_def inner_Pair_0)
+  moreover from assms have snd_image_times': "B = snd ` (A \<times> B)" by simp
+  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)"
+      by (subst (2) snd_image_times') (simp del: snd_image_times add: o_def inner_Pair_0)
+  ultimately show ?thesis unfolding interval_upperbound_def
+      by (subst setsum_Basis_prod_eq) (auto simp add: setsum_prod)
+qed
+
+lemma interval_lowerbound_Times: 
+  assumes "A \<noteq> {}" and "B \<noteq> {}"
+  shows "interval_lowerbound (A \<times> B) = (interval_lowerbound A, interval_lowerbound B)"
+proof-
+  from assms have fst_image_times': "A = fst ` (A \<times> B)" by simp
+  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)"
+      by (subst (2) fst_image_times') (simp del: fst_image_times add: o_def inner_Pair_0)
+  moreover from assms have snd_image_times': "B = snd ` (A \<times> B)" by simp
+  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)"
+      by (subst (2) snd_image_times') (simp del: snd_image_times add: o_def inner_Pair_0)
+  ultimately show ?thesis unfolding interval_lowerbound_def
+      by (subst setsum_Basis_prod_eq) (auto simp add: setsum_prod)
+qed
+
 subsection {* Content (length, area, volume...) of an interval. *}
 
 definition "content (s::('a::euclidean_space) set) =
@@ -619,6 +648,20 @@
 lemma content_lt_nz: "0 < content (cbox a b) \<longleftrightarrow> content (cbox a b) \<noteq> 0"
   unfolding content_pos_lt_eq content_eq_0 unfolding not_ex not_le by fastforce
 
+lemma content_times[simp]: "content (A \<times> B) = content A * content B"
+proof (cases "A \<times> B = {}")
+  let ?ub1 = "interval_upperbound" and ?lb1 = "interval_lowerbound"
+  let ?ub2 = "interval_upperbound" and ?lb2 = "interval_lowerbound"
+  assume nonempty: "A \<times> B \<noteq> {}"
+  hence "content (A \<times> B) = (\<Prod>i\<in>Basis. (?ub1 A, ?ub2 B) \<bullet> i - (?lb1 A, ?lb2 B) \<bullet> i)" 
+      unfolding content_def by (simp add: interval_upperbound_Times interval_lowerbound_Times)
+  also have "... = content A * content B" unfolding content_def using nonempty
+    apply (subst Basis_prod_def, subst setprod.union_disjoint, force, force, force, simp)
+    apply (subst (1 2) setprod.reindex, auto intro: inj_onI)
+    done
+  finally show ?thesis .
+qed (auto simp: content_def)
+
 
 subsection {* The notion of a gauge --- simply an open set containing the point. *}
 
diff -r ca2336984f6a -r c5e79df8cc21 src/HOL/Probability/Bochner_Integration.thy
--- a/src/HOL/Probability/Bochner_Integration.thy	Thu Jan 22 13:21:45 2015 +0100
+++ b/src/HOL/Probability/Bochner_Integration.thy	Thu Jan 22 14:51:08 2015 +0100
@@ -2059,6 +2059,41 @@
   by (subst lebesgue_integral_count_space_finite_support)
      (auto intro!: setsum.mono_neutral_cong_left)
 
+lemma integrable_count_space_nat_iff:
+  fixes f :: "nat \<Rightarrow> _::{banach,second_countable_topology}"
+  shows "integrable (count_space UNIV) f \<longleftrightarrow> summable (\<lambda>x. norm (f x))"
+  by (auto simp add: integrable_iff_bounded nn_integral_count_space_nat summable_ereal suminf_ereal_finite)
+
+lemma sums_integral_count_space_nat:
+  fixes f :: "nat \<Rightarrow> _::{banach,second_countable_topology}"
+  assumes *: "integrable (count_space UNIV) f"
+  shows "f sums (integral\<^sup>L (count_space UNIV) f)"
+proof -
+  let ?f = "\<lambda>n i. indicator {n} i *\<^sub>R f i"
+  have f': "\<And>n i. ?f n i = indicator {n} i *\<^sub>R f n"
+    by (auto simp: fun_eq_iff split: split_indicator)
+
+  have "(\<lambda>i. \<integral>n. ?f i n \<partial>count_space UNIV) sums \<integral> n. (\<Sum>i. ?f i n) \<partial>count_space UNIV"
+  proof (rule sums_integral)
+    show "\<And>i. integrable (count_space UNIV) (?f i)"
+      using * by (intro integrable_mult_indicator) auto
+    show "AE n in count_space UNIV. summable (\<lambda>i. norm (?f i n))"
+      using summable_finite[of "{n}" "\<lambda>i. norm (?f i n)" for n] by simp
+    show "summable (\<lambda>i. \<integral> n. norm (?f i n) \<partial>count_space UNIV)"
+      using * by (subst f') (simp add: integrable_count_space_nat_iff)
+  qed
+  also have "(\<integral> n. (\<Sum>i. ?f i n) \<partial>count_space UNIV) = (\<integral>n. f n \<partial>count_space UNIV)"
+    using suminf_finite[of "{n}" "\<lambda>i. ?f i n" for n] by (auto intro!: integral_cong)
+  also have "(\<lambda>i. \<integral>n. ?f i n \<partial>count_space UNIV) = f"
+    by (subst f') simp
+  finally show ?thesis .
+qed
+
+lemma integral_count_space_nat:
+  fixes f :: "nat \<Rightarrow> _::{banach,second_countable_topology}"
+  shows "integrable (count_space UNIV) f \<Longrightarrow> integral\<^sup>L (count_space UNIV) f = (\<Sum>x. f x)"
+  using sums_integral_count_space_nat by (rule sums_unique)
+
 subsection {* Point measure *}
 
 lemma lebesgue_integral_point_measure_finite:
@@ -2076,6 +2111,20 @@
   apply (auto simp: AE_count_space integrable_count_space)
   done
 
+subsection {* Lebesgue integration on @{const null_measure} *}
+
+lemma has_bochner_integral_null_measure_iff[iff]:
+  "has_bochner_integral (null_measure M) f 0 \<longleftrightarrow> f \<in> borel_measurable M"
+  by (auto simp add: has_bochner_integral.simps simple_bochner_integral_def[abs_def]
+           intro!: exI[of _ "\<lambda>n x. 0"] simple_bochner_integrable.intros)
+
+lemma integrable_null_measure_iff[iff]: "integrable (null_measure M) f \<longleftrightarrow> f \<in> borel_measurable M"
+  by (auto simp add: integrable.simps)
+
+lemma integral_null_measure[simp]: "integral\<^sup>L (null_measure M) f = 0"
+  by (cases "integrable (null_measure M) f")
+     (auto simp add: not_integrable_integral_eq has_bochner_integral_integral_eq)
+
 subsection {* Legacy lemmas for the real-valued Lebesgue integral *}
 
 lemma real_lebesgue_integral_def:
diff -r ca2336984f6a -r c5e79df8cc21 src/HOL/Probability/Finite_Product_Measure.thy
--- a/src/HOL/Probability/Finite_Product_Measure.thy	Thu Jan 22 13:21:45 2015 +0100
+++ b/src/HOL/Probability/Finite_Product_Measure.thy	Thu Jan 22 14:51:08 2015 +0100
@@ -180,6 +180,37 @@
 translations
   "PIM x:I. M" == "CONST PiM I (%x. M)"
 
+lemma extend_measure_cong:
+  assumes "\<Omega> = \<Omega>'" "I = I'" "G = G'" "\<And>i. i \<in> I' \<Longrightarrow> \<mu> i = \<mu>' i"
+  shows "extend_measure \<Omega> I G \<mu> = extend_measure \<Omega>' I' G' \<mu>'"
+  unfolding extend_measure_def by (auto simp add: assms)
+
+lemma Pi_cong_sets:
+    "\<lbrakk>I = J; \<And>x. x \<in> I \<Longrightarrow> M x = N x\<rbrakk> \<Longrightarrow> Pi I M = Pi J N"
+  unfolding Pi_def by auto 
+
+lemma PiM_cong:
+  assumes "I = J" "\<And>x. x \<in> I \<Longrightarrow> M x = N x"
+  shows "PiM I M = PiM J N"
+unfolding PiM_def
+proof (rule extend_measure_cong)
+  case goal1 show ?case using assms
+    by (subst assms(1), intro PiE_cong[of J "\<lambda>i. space (M i)" "\<lambda>i. space (N i)"]) simp_all
+next
+  case goal2
+  have "\<And>K. K \<subseteq> J \<Longrightarrow> (\<Pi> j\<in>K. sets (M j)) = (\<Pi> j\<in>K. sets (N j))"
+    using assms by (intro Pi_cong_sets) auto
+  thus ?case by (auto simp: assms)
+next
+  case goal3 show ?case using assms 
+    by (intro ext) (auto simp: prod_emb_def dest: PiE_mem)
+next
+  case (goal4 x)
+  thus ?case using assms 
+    by (auto intro!: setprod.cong split: split_if_asm)
+qed
+
+
 lemma prod_algebra_sets_into_space:
   "prod_algebra I M \<subseteq> Pow (\<Pi>\<^sub>E i\<in>I. space (M i))"
   by (auto simp: prod_emb_def prod_algebra_def)
@@ -624,6 +655,17 @@
 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)"
   by (intro measurable_restrict measurable_component_singleton) auto
 
+lemma measurable_restrict_subset':
+  assumes "J \<subseteq> L" "\<And>x. x \<in> J \<Longrightarrow> sets (M x) = sets (N x)"
+  shows "(\<lambda>f. restrict f J) \<in> measurable (Pi\<^sub>M L M) (Pi\<^sub>M J N)"
+proof-
+  from assms(1) have "(\<lambda>f. restrict f J) \<in> measurable (Pi\<^sub>M L M) (Pi\<^sub>M J M)"
+    by (rule measurable_restrict_subset)
+  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)"
+    by (intro sets_PiM_cong measurable_cong_sets) simp_all
+  finally show ?thesis .
+qed
+
 lemma measurable_prod_emb[intro, simp]:
   "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)"
   unfolding prod_emb_def space_PiM[symmetric]
@@ -945,6 +987,17 @@
   qed
 qed
 
+lemma (in product_sigma_finite) product_nn_integral_insert_rev:
+  assumes I[simp]: "finite I" "i \<notin> I"
+    and [measurable]: "f \<in> borel_measurable (Pi\<^sub>M (insert i I) M)"
+  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))"
+  apply (subst product_nn_integral_insert[OF assms])
+  apply (rule pair_sigma_finite.Fubini')
+  apply intro_locales []
+  apply (rule sigma_finite[OF I(1)])
+  apply measurable
+  done
+
 lemma (in product_sigma_finite) product_nn_integral_setprod:
   fixes f :: "'i \<Rightarrow> 'a \<Rightarrow> ereal"
   assumes "finite I" and borel: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> borel_measurable (M i)"
@@ -969,6 +1022,23 @@
     done
 qed (simp add: space_PiM)
 
+lemma (in product_sigma_finite) product_nn_integral_pair:
+  assumes [measurable]: "split f \<in> borel_measurable (M x \<Otimes>\<^sub>M M y)"
+  assumes xy: "x \<noteq> y"
+  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))"
+proof-
+  interpret psm: pair_sigma_finite "M x" "M y"
+    unfolding pair_sigma_finite_def using sigma_finite_measures by simp_all
+  have "{x, y} = {y, x}" by auto
+  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)"
+    using xy by (subst product_nn_integral_insert_rev) simp_all
+  also have "... = (\<integral>\<^sup>+y. \<integral>\<^sup>+x. f x y \<partial>M x \<partial>M y)"
+    by (intro nn_integral_cong, subst product_nn_integral_singleton) simp_all
+  also have "... = (\<integral>\<^sup>+z. f (fst z) (snd z) \<partial>(M x \<Otimes>\<^sub>M M y))"
+    by (subst psm.nn_integral_snd[symmetric]) simp_all
+  finally show ?thesis .
+qed
+
 lemma (in product_sigma_finite) distr_component:
   "distr (M i) (Pi\<^sub>M {i} M) (\<lambda>x. \<lambda>i\<in>{i}. x) = Pi\<^sub>M {i} M" (is "?D = ?P")
 proof (intro measure_eqI[symmetric])
diff -r ca2336984f6a -r c5e79df8cc21 src/HOL/Probability/Giry_Monad.thy
--- a/src/HOL/Probability/Giry_Monad.thy	Thu Jan 22 13:21:45 2015 +0100
+++ b/src/HOL/Probability/Giry_Monad.thy	Thu Jan 22 14:51:08 2015 +0100
@@ -32,6 +32,9 @@
   "prob_space M \<Longrightarrow> subprob_space M"
   by (rule subprob_spaceI) (simp_all add: prob_space.emeasure_space_1 prob_space.not_empty)
 
+lemma subprob_space_imp_sigma_finite: "subprob_space M \<Longrightarrow> sigma_finite_measure M"
+  unfolding subprob_space_def finite_measure_def by simp
+
 sublocale prob_space \<subseteq> subprob_space
   by (rule subprob_spaceI) (simp_all add: emeasure_space_1 not_empty)
 
@@ -123,6 +126,10 @@
     by (simp add: space_pair_measure)
 qed
 
+lemma subprob_space_null_measure_iff:
+    "subprob_space (null_measure M) \<longleftrightarrow> space M \<noteq> {}"
+  by (auto intro!: subprob_spaceI dest: subprob_space.subprob_not_empty)
+
 definition subprob_algebra :: "'a measure \<Rightarrow> 'a measure measure" where
   "subprob_algebra K =
     (\<Squnion>\<^sub>\<sigma> A\<in>sets K. vimage_algebra {M. subprob_space M \<and> sets M = sets K} (\<lambda>M. emeasure M A) borel)"
@@ -1250,4 +1257,18 @@
     by (simp add: emeasure_notin_sets)
 qed
 
+lemma bind_return'': "sets M = sets N \<Longrightarrow> M \<guillemotright>= return N = M"
+   by (cases "space M = {}")
+      (simp_all add: bind_empty space_empty[symmetric] bind_nonempty join_return'
+                cong: subprob_algebra_cong)
+
+lemma (in prob_space) distr_const[simp]:
+  "c \<in> space N \<Longrightarrow> distr M N (\<lambda>x. c) = return N c"
+  by (rule measure_eqI) (auto simp: emeasure_distr emeasure_space_1)
+
+lemma return_count_space_eq_density:
+    "return (count_space M) x = density (count_space M) (indicator {x})"
+  by (rule measure_eqI) 
+     (auto simp: indicator_inter_arith_ereal emeasure_density split: split_indicator)
+
 end
diff -r ca2336984f6a -r c5e79df8cc21 src/HOL/Probability/Lebesgue_Measure.thy
--- a/src/HOL/Probability/Lebesgue_Measure.thy	Thu Jan 22 13:21:45 2015 +0100
+++ b/src/HOL/Probability/Lebesgue_Measure.thy	Thu Jan 22 14:51:08 2015 +0100
@@ -529,6 +529,23 @@
   thus ?thesis by (auto simp add: emeasure_le_0_iff)
 qed
 
+lemma countable_imp_null_set_lborel: "countable A \<Longrightarrow> A \<in> null_sets lborel"
+  by (simp add: null_sets_def emeasure_lborel_countable sets.countable)
+
+lemma finite_imp_null_set_lborel: "finite A \<Longrightarrow> A \<in> null_sets lborel"
+  by (intro countable_imp_null_set_lborel countable_finite)
+
+lemma lborel_neq_count_space[simp]: "lborel \<noteq> count_space (A::('a::ordered_euclidean_space) set)"
+proof
+  assume asm: "lborel = count_space A"
+  have "space lborel = UNIV" by simp
+  hence [simp]: "A = UNIV" by (subst (asm) asm) (simp only: space_count_space)
+  have "emeasure lborel {undefined::'a} = 1" 
+      by (subst asm, subst emeasure_count_space_finite) auto
+  moreover have "emeasure lborel {undefined} \<noteq> 1" by simp
+  ultimately show False by contradiction
+qed
+
 subsection {* Affine transformation on the Lebesgue-Borel *}
 
 lemma lborel_eqI:
@@ -651,11 +668,59 @@
   unfolding has_bochner_integral_iff lborel_integrable_real_affine_iff
   by (simp_all add: lborel_integral_real_affine[symmetric] divideR_right cong: conj_cong)
 
+lemma lborel_distr_uminus: "distr lborel borel uminus = (lborel :: real measure)"
+  by (subst lborel_real_affine[of "-1" 0]) 
+     (auto simp: density_1 one_ereal_def[symmetric])
+
+lemma lborel_distr_mult: 
+  assumes "(c::real) \<noteq> 0"
+  shows "distr lborel borel (op * c) = density lborel (\<lambda>_. inverse \<bar>c\<bar>)"
+proof-
+  have "distr lborel borel (op * c) = distr lborel lborel (op * c)" by (simp cong: distr_cong)
+  also from assms have "... = density lborel (\<lambda>_. inverse \<bar>c\<bar>)"
+    by (subst lborel_real_affine[of "inverse c" 0]) (auto simp: o_def distr_density_distr)
+  finally show ?thesis .
+qed
+
+lemma lborel_distr_mult': 
+  assumes "(c::real) \<noteq> 0"
+  shows "lborel = density (distr lborel borel (op * c)) (\<lambda>_. abs c)"
+proof-
+  have "lborel = density lborel (\<lambda>_. 1)" by (rule density_1[symmetric])
+  also from assms have "(\<lambda>_. 1 :: ereal) = (\<lambda>_. inverse (abs c) * abs c)" by (intro ext) simp
+  also have "density lborel ... = density (density lborel (\<lambda>_. inverse (abs c))) (\<lambda>_. abs c)"
+    by (subst density_density_eq) auto
+  also from assms have "density lborel (\<lambda>_. inverse (abs c)) = distr lborel borel (op * c)"
+    by (rule lborel_distr_mult[symmetric])
+  finally show ?thesis .
+qed
+
+lemma lborel_distr_plus: "distr lborel borel (op + c) = (lborel :: real measure)"
+  by (subst lborel_real_affine[of 1 c]) (auto simp: density_1 one_ereal_def[symmetric])
+
 interpretation lborel!: sigma_finite_measure lborel
   by (rule sigma_finite_lborel)
 
 interpretation lborel_pair: pair_sigma_finite lborel lborel ..
 
+lemma lborel_prod:
+  "lborel \<Otimes>\<^sub>M lborel = (lborel :: ('a::euclidean_space \<times> 'b::euclidean_space) measure)"
+proof (rule lborel_eqI[symmetric], clarify)
+  fix la ua :: 'a and lb ub :: 'b
+  assume lu: "\<And>a b. (a, b) \<in> Basis \<Longrightarrow> (la, lb) \<bullet> (a, b) \<le> (ua, ub) \<bullet> (a, b)"
+  have [simp]:
+    "\<And>b. b \<in> Basis \<Longrightarrow> la \<bullet> b \<le> ua \<bullet> b"
+    "\<And>b. b \<in> Basis \<Longrightarrow> lb \<bullet> b \<le> ub \<bullet> b"
+    "inj_on (\<lambda>u. (u, 0)) Basis" "inj_on (\<lambda>u. (0, u)) Basis"
+    "(\<lambda>u. (u, 0)) ` Basis \<inter> (\<lambda>u. (0, u)) ` Basis = {}"
+    "box (la, lb) (ua, ub) = box la ua \<times> box lb ub"
+    using lu[of _ 0] lu[of 0] by (auto intro!: inj_onI simp add: Basis_prod_def ball_Un box_def)
+  show "emeasure (lborel \<Otimes>\<^sub>M lborel) (box (la, lb) (ua, ub)) =
+      ereal (setprod (op \<bullet> ((ua, ub) - (la, lb))) Basis)"
+    by (simp add: lborel.emeasure_pair_measure_Times Basis_prod_def setprod.union_disjoint
+                  setprod.reindex)
+qed (simp add: borel_prod[symmetric])
+
 (* FIXME: conversion in measurable prover *)
 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
 lemma lborelD[measurable (raw)]: "A \<in> sets borel \<Longrightarrow> A \<in> sets lborel" by simp
diff -r ca2336984f6a -r c5e79df8cc21 src/HOL/Probability/Measure_Space.thy
--- a/src/HOL/Probability/Measure_Space.thy	Thu Jan 22 13:21:45 2015 +0100
+++ b/src/HOL/Probability/Measure_Space.thy	Thu Jan 22 14:51:08 2015 +0100
@@ -1928,5 +1928,23 @@
   finally show "emeasure M X = emeasure N X" .
 qed fact
 
+subsection {* Null measure *}
+
+definition "null_measure M = sigma (space M) (sets M)"
+
+lemma space_null_measure[simp]: "space (null_measure M) = space M"
+  by (simp add: null_measure_def)
+
+lemma sets_null_measure[simp, measurable_cong]: "sets (null_measure M) = sets M" 
+  by (simp add: null_measure_def)
+
+lemma emeasure_null_measure[simp]: "emeasure (null_measure M) X = 0"
+  by (cases "X \<in> sets M", rule emeasure_measure_of)
+     (auto simp: positive_def countably_additive_def emeasure_notin_sets null_measure_def
+           dest: sets.sets_into_space)
+
+lemma measure_null_measure[simp]: "measure (null_measure M) X = 0"
+  by (simp add: measure_def)
+
 end
 
diff -r ca2336984f6a -r c5e79df8cc21 src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy
--- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Thu Jan 22 13:21:45 2015 +0100
+++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Thu Jan 22 14:51:08 2015 +0100
@@ -1951,6 +1951,11 @@
   shows "(\<integral>\<^sup>+x. f x \<partial>count_space X) = (\<integral>\<^sup>+x. f x * indicator X x \<partial>count_space UNIV)"
   by (simp add: nn_integral_restrict_space[symmetric] restrict_count_space)
 
+lemma nn_integral_count_space_eq:
+  "(\<And>x. x \<in> A - B \<Longrightarrow> f x = 0) \<Longrightarrow> (\<And>x. x \<in> B - A \<Longrightarrow> f x = 0) \<Longrightarrow>
+    (\<integral>\<^sup>+x. f x \<partial>count_space A) = (\<integral>\<^sup>+x. f x \<partial>count_space B)"
+  by (auto simp: nn_integral_count_space_indicator intro!: nn_integral_cong split: split_indicator)
+
 lemma nn_integral_ge_point:
   assumes "x \<in> A"
   shows "p x \<le> \<integral>\<^sup>+ x. p x \<partial>count_space A"
@@ -2194,6 +2199,23 @@
     using f g by (subst density_density_eq) auto
 qed
 
+lemma density_1: "density M (\<lambda>_. 1) = M"
+  by (intro measure_eqI) (auto simp: emeasure_density)
+
+lemma emeasure_density_add:
+  assumes X: "X \<in> sets M" 
+  assumes Mf[measurable]: "f \<in> borel_measurable M"
+  assumes Mg[measurable]: "g \<in> borel_measurable M"
+  assumes nonnegf: "\<And>x. x \<in> space M \<Longrightarrow> f x \<ge> 0"
+  assumes nonnegg: "\<And>x. x \<in> space M \<Longrightarrow> g x \<ge> 0"
+  shows "emeasure (density M f) X + emeasure (density M g) X = 
+           emeasure (density M (\<lambda>x. f x + g x)) X"
+  using assms
+  apply (subst (1 2 3) emeasure_density, simp_all) []
+  apply (subst nn_integral_add[symmetric], simp_all) []
+  apply (intro nn_integral_cong, simp split: split_indicator)
+  done
+
 subsubsection {* Point measure *}
 
 definition point_measure :: "'a set \<Rightarrow> ('a \<Rightarrow> ereal) \<Rightarrow> 'a measure" where
@@ -2351,6 +2373,21 @@
     unfolding uniform_measure_def by (simp add: AE_density)
 qed
 
+subsubsection {* Null measure *}
+
+lemma null_measure_eq_density: "null_measure M = density M (\<lambda>_. 0)"
+  by (intro measure_eqI) (simp_all add: emeasure_density)
+
+lemma nn_integral_null_measure[simp]: "(\<integral>\<^sup>+x. f x \<partial>null_measure M) = 0"
+  by (auto simp add: nn_integral_def simple_integral_def SUP_constant bot_ereal_def le_fun_def
+           intro!: exI[of _ "\<lambda>x. 0"])
+
+lemma density_null_measure[simp]: "density (null_measure M) f = null_measure M"
+proof (intro measure_eqI)
+  fix A show "emeasure (density (null_measure M) f) A = emeasure (null_measure M) A"
+    by (simp add: density_def) (simp only: null_measure_def[symmetric] emeasure_null_measure)
+qed simp
+
 subsubsection {* Uniform count measure *}
 
 definition "uniform_count_measure A = point_measure A (\<lambda>x. 1 / card A)"
diff -r ca2336984f6a -r c5e79df8cc21 src/HOL/Probability/Probability_Mass_Function.thy
--- a/src/HOL/Probability/Probability_Mass_Function.thy	Thu Jan 22 13:21:45 2015 +0100
+++ b/src/HOL/Probability/Probability_Mass_Function.thy	Thu Jan 22 14:51:08 2015 +0100
@@ -12,16 +12,6 @@
   "~~/src/HOL/Library/Multiset"
 begin
 
-lemma bind_return'': "sets M = sets N \<Longrightarrow> M \<guillemotright>= return N = M"
-   by (cases "space M = {}")
-      (simp_all add: bind_empty space_empty[symmetric] bind_nonempty join_return'
-                cong: subprob_algebra_cong)
-
-
-lemma (in prob_space) distr_const[simp]:
-  "c \<in> space N \<Longrightarrow> distr M N (\<lambda>x. c) = return N c"
-  by (rule measure_eqI) (auto simp: emeasure_distr emeasure_space_1)
-
 lemma (in finite_measure) countable_support:
   "countable {x. measure M {x} \<noteq> 0}"
 proof cases
@@ -214,8 +204,7 @@
   by (subst emeasure_eq_setsum_singleton) (auto simp: emeasure_pmf_single)
 
 lemma measure_measure_pmf_finite: "finite S \<Longrightarrow> measure (measure_pmf M) S = setsum (pmf M) S"
-using emeasure_measure_pmf_finite[of S M]
-by(simp add: measure_pmf.emeasure_eq_measure)
+  using emeasure_measure_pmf_finite[of S M] by(simp add: measure_pmf.emeasure_eq_measure)
 
 lemma nn_integral_measure_pmf_support:
   fixes f :: "'a \<Rightarrow> ereal"
@@ -759,33 +748,34 @@
               intro!: measure_pmf.integrable_const_bound[where B=1])
   done
 
+
 lemma measurable_pair_restrict_pmf2:
   assumes "countable A"
-  assumes "\<And>y. y \<in> A \<Longrightarrow> (\<lambda>x. f (x, y)) \<in> measurable M L"
-  shows "f \<in> measurable (M \<Otimes>\<^sub>M restrict_space (measure_pmf N) A) L"
-  apply (subst measurable_cong_sets)
-  apply (rule sets_pair_measure_cong sets_restrict_space_cong sets_measure_pmf_count_space refl)+
-  apply (simp_all add: restrict_count_space)
-  apply (subst split_eta[symmetric])
-  unfolding measurable_split_conv
-  apply (rule measurable_compose_countable'[OF _ measurable_snd `countable A`])
-  apply (rule measurable_compose[OF measurable_fst])
-  apply fact
-  done
+  assumes [measurable]: "\<And>y. y \<in> A \<Longrightarrow> (\<lambda>x. f (x, y)) \<in> measurable M L"
+  shows "f \<in> measurable (M \<Otimes>\<^sub>M restrict_space (measure_pmf N) A) L" (is "f \<in> measurable ?M _")
+proof -
+  have [measurable_cong]: "sets (restrict_space (count_space UNIV) A) = sets (count_space A)"
+    by (simp add: restrict_count_space)
+
+  show ?thesis
+    by (intro measurable_compose_countable'[where f="\<lambda>a b. f (fst b, a)" and g=snd and I=A,
+                                            unfolded pair_collapse] assms)
+        measurable
+qed
 
 lemma measurable_pair_restrict_pmf1:
   assumes "countable A"
-  assumes "\<And>x. x \<in> A \<Longrightarrow> (\<lambda>y. f (x, y)) \<in> measurable N L"
+  assumes [measurable]: "\<And>x. x \<in> A \<Longrightarrow> (\<lambda>y. f (x, y)) \<in> measurable N L"
   shows "f \<in> measurable (restrict_space (measure_pmf M) A \<Otimes>\<^sub>M N) L"
-  apply (subst measurable_cong_sets)
-  apply (rule sets_pair_measure_cong sets_restrict_space_cong sets_measure_pmf_count_space refl)+
-  apply (simp_all add: restrict_count_space)
-  apply (subst split_eta[symmetric])
-  unfolding measurable_split_conv
-  apply (rule measurable_compose_countable'[OF _ measurable_fst `countable A`])
-  apply (rule measurable_compose[OF measurable_snd])
-  apply fact
-  done
+proof -
+  have [measurable_cong]: "sets (restrict_space (count_space UNIV) A) = sets (count_space A)"
+    by (simp add: restrict_count_space)
+
+  show ?thesis
+    by (intro measurable_compose_countable'[where f="\<lambda>a b. f (a, snd b)" and g=fst and I=A,
+                                            unfolded pair_collapse] assms)
+        measurable
+qed
                                 
 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))"
   unfolding pmf_eq_iff pmf_bind
@@ -993,11 +983,6 @@
      map_pmf fst pq = p; map_pmf snd pq = q \<rbrakk>
   \<Longrightarrow> rel_pmf R p q"
 
-lemma nn_integral_count_space_eq:
-  "(\<And>x. x \<in> A - B \<Longrightarrow> f x = 0) \<Longrightarrow> (\<And>x. x \<in> B - A \<Longrightarrow> f x = 0) \<Longrightarrow>
-    (\<integral>\<^sup>+x. f x \<partial>count_space A) = (\<integral>\<^sup>+x. f x \<partial>count_space B)"
-  by (auto simp: nn_integral_count_space_indicator intro!: nn_integral_cong split: split_indicator)
-
 bnf pmf: "'a pmf" map: map_pmf sets: set_pmf bd : "natLeq" rel: rel_pmf
 proof -
   show "map_pmf id = id" by (rule map_pmf_id)
diff -r ca2336984f6a -r c5e79df8cc21 src/HOL/Probability/Probability_Measure.thy
--- a/src/HOL/Probability/Probability_Measure.thy	Thu Jan 22 13:21:45 2015 +0100
+++ b/src/HOL/Probability/Probability_Measure.thy	Thu Jan 22 14:51:08 2015 +0100
@@ -23,6 +23,9 @@
   show "prob_space M" by default fact
 qed
 
+lemma prob_space_imp_sigma_finite: "prob_space M \<Longrightarrow> sigma_finite_measure M"
+  unfolding prob_space_def finite_measure_def by simp
+
 abbreviation (in prob_space) "events \<equiv> sets M"
 abbreviation (in prob_space) "prob \<equiv> measure M"
 abbreviation (in prob_space) "random_variable M' X \<equiv> X \<in> measurable M M'"