# 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 \ 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 \ measurable (count_space A) (count_space B)" + using f unfolding Pi_def bij_betw_def by auto + fix X assume "X \ sets (distr (count_space A) (count_space B) f)" + then have X: "X \ sets (count_space B)" by auto + moreover then have "f -` X \ 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 \ A \ finite X \ 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 "(\\<^sup>+x. f (g x) \count_space A) = (\\<^sup>+x. f x \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 \ ereal" assumes f: "finite A" and nn: "\x. x \ A \ 0 \ f x" and [measurable]: "\a. a \ A \ {a} \ sets M"