# HG changeset patch
# User hoelzl
# Date 1416244746 -3600
# Node ID 4902a2fec4348159d51392d8731528b86f5fb253
# Parent  ec2b4270a50286783807d82201cacb07ff53ff5d
add reindex rules for distr and nn_integral on count_space

diff -r ec2b4270a502 -r 4902a2fec434 src/HOL/Probability/Measure_Space.thy
--- a/src/HOL/Probability/Measure_Space.thy	Mon Nov 17 14:55:34 2014 +0100
+++ b/src/HOL/Probability/Measure_Space.thy	Mon Nov 17 18:19:06 2014 +0100
@@ -1304,7 +1304,6 @@
   by (auto simp add: emeasure_distr measurable_space
            intro!: arg_cong[where f="emeasure M"] measure_eqI)
 
-
 subsection {* Real measure values *}
 
 lemma measure_nonneg: "0 \<le> measure M A"
@@ -1731,6 +1730,25 @@
   qed
 qed
 
+lemma distr_bij_count_space:
+  assumes f: "bij_betw f A B"
+  shows "distr (count_space A) (count_space B) f = count_space B"
+proof (rule measure_eqI)
+  have f': "f \<in> measurable (count_space A) (count_space B)"
+    using f unfolding Pi_def bij_betw_def by auto
+  fix X assume "X \<in> sets (distr (count_space A) (count_space B) f)"
+  then have X: "X \<in> sets (count_space B)" by auto
+  moreover then have "f -` X \<inter> A = the_inv_into A f ` X"
+    using f by (auto simp: bij_betw_def subset_image_iff image_iff the_inv_into_f_f intro: the_inv_into_f_f[symmetric])
+  moreover have "inj_on (the_inv_into A f) B"
+    using X f by (auto simp: bij_betw_def inj_on_the_inv_into)
+  with X have "inj_on (the_inv_into A f) X"
+    by (auto intro: subset_inj_on)
+  ultimately show "emeasure (distr (count_space A) (count_space B) f) X = emeasure (count_space B) X"
+    using f unfolding emeasure_distr[OF f' X]
+    by (subst (1 2) emeasure_count_space) (auto simp: card_image dest: finite_imageD)
+qed simp
+
 lemma emeasure_count_space_finite[simp]:
   "X \<subseteq> A \<Longrightarrow> finite X \<Longrightarrow> emeasure (count_space A) X = ereal (card X)"
   using emeasure_count_space[of X A] by simp
diff -r ec2b4270a502 -r 4902a2fec434 src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy
--- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Mon Nov 17 14:55:34 2014 +0100
+++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Mon Nov 17 18:19:06 2014 +0100
@@ -1705,6 +1705,13 @@
   finally show ?thesis .
 qed
 
+lemma nn_integral_bij_count_space:
+  assumes g: "bij_betw g A B"
+  shows "(\<integral>\<^sup>+x. f (g x) \<partial>count_space A) = (\<integral>\<^sup>+x. f x \<partial>count_space B)"
+  using g[THEN bij_betw_imp_funcset]
+  by (subst distr_bij_count_space[OF g, symmetric])
+     (auto intro!: nn_integral_distr[symmetric])
+
 lemma nn_integral_indicator_finite:
   fixes f :: "'a \<Rightarrow> ereal"
   assumes f: "finite A" and nn: "\<And>x. x \<in> A \<Longrightarrow> 0 \<le> f x" and [measurable]: "\<And>a. a \<in> A \<Longrightarrow> {a} \<in> sets M"