# HG changeset patch
# User Andreas Lochbihler
# Date 1423567042 -3600
# Node ID 40f570f9a284e6bc7b6468084ca237feb91a3435
# Parent  f71732294f299af6935bb469390b5a8a9a726fcb
add another lemma to split nn_integral over product count_space

diff -r f71732294f29 -r 40f570f9a284 src/HOL/Probability/Binary_Product_Measure.thy
--- a/src/HOL/Probability/Binary_Product_Measure.thy	Tue Feb 10 12:10:26 2015 +0100
+++ b/src/HOL/Probability/Binary_Product_Measure.thy	Tue Feb 10 12:17:22 2015 +0100
@@ -1041,6 +1041,21 @@
   "(\<integral>\<^sup>+ x. \<integral>\<^sup>+ y. f (x, y) \<partial>count_space UNIV \<partial>count_space UNIV) = integral\<^sup>N (count_space UNIV) f"
 by(subst (2 3) nn_integral_max_0[symmetric])(rule nn_integral_fst_count_space', simp)
 
+lemma nn_integral_snd_count_space:
+  "(\<integral>\<^sup>+ y. \<integral>\<^sup>+ x. f (x, y) \<partial>count_space UNIV \<partial>count_space UNIV) = integral\<^sup>N (count_space UNIV) f"
+  (is "?lhs = ?rhs")
+proof -
+  have "?lhs = (\<integral>\<^sup>+ y. \<integral>\<^sup>+ x. (\<lambda>(y, x). f (x, y)) (y, x) \<partial>count_space UNIV \<partial>count_space UNIV)"
+    by(simp)
+  also have "\<dots> = \<integral>\<^sup>+ yx. (\<lambda>(y, x). f (x, y)) yx \<partial>count_space UNIV"
+    by(rule nn_integral_fst_count_space)
+  also have "\<dots> = \<integral>\<^sup>+ xy. f xy \<partial>count_space ((\<lambda>(x, y). (y, x)) ` UNIV)"
+    by(subst nn_integral_bij_count_space[OF inj_on_imp_bij_betw, symmetric])
+      (simp_all add: inj_on_def split_def)
+  also have "\<dots> = ?rhs" by(rule nn_integral_count_space_eq) auto
+  finally show ?thesis .
+qed
+
 subsection {* Product of Borel spaces *}
 
 lemma borel_Times: