# HG changeset patch # User hoelzl # Date 1268753248 -3600 # Node ID 7b7ae5aa396dde63e180cbed80511d54659c3ae3 # Parent 1dac16f00cd2ae85e9200be2d1b3984481ebd318 Added product measure space diff -r 1dac16f00cd2 -r 7b7ae5aa396d src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Thu Mar 18 14:52:11 2010 +0100 +++ b/src/HOL/IsaMakefile Tue Mar 16 16:27:28 2010 +0100 @@ -1093,6 +1093,7 @@ Probability/Borel.thy \ Probability/Measure.thy \ Probability/Lebesgue.thy \ + Probability/Product_Measure.thy \ Probability/Probability_Space.thy @$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Probability diff -r 1dac16f00cd2 -r 7b7ae5aa396d src/HOL/Probability/Lebesgue.thy --- a/src/HOL/Probability/Lebesgue.thy Thu Mar 18 14:52:11 2010 +0100 +++ b/src/HOL/Probability/Lebesgue.thy Tue Mar 16 16:27:28 2010 +0100 @@ -1389,6 +1389,7 @@ qed lemma integral_on_countable: + fixes enum :: "nat \ real" assumes borel: "f \ borel_measurable M" and bij: "bij_betw enum S (f ` space M)" and enum_zero: "enum ` (-S) \ {0}" diff -r 1dac16f00cd2 -r 7b7ae5aa396d src/HOL/Probability/Probability.thy --- a/src/HOL/Probability/Probability.thy Thu Mar 18 14:52:11 2010 +0100 +++ b/src/HOL/Probability/Probability.thy Tue Mar 16 16:27:28 2010 +0100 @@ -1,5 +1,5 @@ theory Probability -imports Probability_Space +imports Probability_Space Product_Measure begin end diff -r 1dac16f00cd2 -r 7b7ae5aa396d src/HOL/Probability/Product_Measure.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Probability/Product_Measure.thy Tue Mar 16 16:27:28 2010 +0100 @@ -0,0 +1,160 @@ +theory Product_Measure +imports "~~/src/HOL/Probability/Lebesgue" +begin + +definition + "prod_measure M M' = (\a. measure_space.integral M (\s0. measure M' ((\s1. (s0, s1)) -` a)))" + +definition + "prod_measure_space M M' \ + \ space = space M \ space M', + sets = sets (sigma (space M \ space M') (prod_sets (sets M) (sets M'))), + measure = prod_measure M M' \" + +lemma prod_measure_times: + assumes "measure_space M" and "measure_space M'" and a: "a \ sets M" + shows "prod_measure M M' (a \ a') = measure M a * measure M' a'" +proof - + interpret M: measure_space M by fact + interpret M': measure_space M' by fact + + { fix \ + have "(\\'. (\, \')) -` (a \ a') = (if \ \ a then a' else {})" + by auto + hence "measure M' ((\\'. (\, \')) -` (a \ a')) = + measure M' a' * indicator_fn a \" + unfolding indicator_fn_def by auto } + note vimage_eq_indicator = this + + show ?thesis + unfolding prod_measure_def vimage_eq_indicator + M.integral_cmul_indicator(1)[OF `a \ sets M`] + by simp +qed + + + +lemma measure_space_finite_prod_measure: + fixes M :: "('a, 'b) measure_space_scheme" + and M' :: "('c, 'd) measure_space_scheme" + assumes "measure_space M" and "measure_space M'" + and finM: "finite (space M)" "Pow (space M) = sets M" + and finM': "finite (space M')" "Pow (space M') = sets M'" + shows "measure_space (prod_measure_space M M')" +proof (rule finite_additivity_sufficient) + interpret M: measure_space M by fact + interpret M': measure_space M' by fact + + have measure: "measure_space.measure (prod_measure_space M M') = prod_measure M M'" + unfolding prod_measure_space_def by simp + + have prod_sets: "prod_sets (sets M) (sets M') \ Pow (space M \ space M')" + using M.sets_into_space M'.sets_into_space unfolding prod_sets_def by auto + show sigma: "sigma_algebra (prod_measure_space M M')" unfolding prod_measure_space_def + by (rule sigma_algebra_sigma_sets[where a="prod_sets (sets M) (sets M')"]) + (simp_all add: sigma_def prod_sets) + + then interpret sa: sigma_algebra "prod_measure_space M M'" . + + { fix x y assume "y \ sets (prod_measure_space M M')" and "x \ space M" + hence "y \ space M \ space M'" + using sa.sets_into_space unfolding prod_measure_space_def by simp + hence "Pair x -` y \ sets M'" + using `x \ space M` unfolding finM'(2)[symmetric] by auto } + note Pair_in_sets = this + + show "additive (prod_measure_space M M') (measure (prod_measure_space M M'))" + unfolding measure additive_def + proof safe + fix x y assume x: "x \ sets (prod_measure_space M M')" and y: "y \ sets (prod_measure_space M M')" + and disj_x_y: "x \ y = {}" + { fix z have "Pair z -` x \ Pair z -` y = {}" using disj_x_y by auto } + note Pair_disj = this + + from M'.measure_additive[OF Pair_in_sets[OF x] Pair_in_sets[OF y] Pair_disj, symmetric] + show "prod_measure M M' (x \ y) = prod_measure M M' x + prod_measure M M' y" + unfolding prod_measure_def + apply (subst (1 2 3) M.integral_finite_singleton[OF finM]) + by (simp_all add: setsum_addf[symmetric] field_simps) + qed + + show "finite (space (prod_measure_space M M'))" + unfolding prod_measure_space_def using finM finM' by simp + + have singletonM: "\x. x \ space M \ {x} \ sets M" + unfolding finM(2)[symmetric] by simp + + show "positive (prod_measure_space M M') (measure (prod_measure_space M M'))" + unfolding positive_def + proof (safe, simp add: M.integral_zero prod_measure_space_def prod_measure_def) + fix Q assume "Q \ sets (prod_measure_space M M')" + from Pair_in_sets[OF this] + show "0 \ measure (prod_measure_space M M') Q" + unfolding prod_measure_space_def prod_measure_def + apply (subst M.integral_finite_singleton[OF finM]) + using M.positive M'.positive singletonM + by (auto intro!: setsum_nonneg mult_nonneg_nonneg) + qed +qed + +lemma measure_space_finite_prod_measure_alterantive: + assumes "measure_space M" and "measure_space M'" + and finM: "finite (space M)" "Pow (space M) = sets M" + and finM': "finite (space M')" "Pow (space M') = sets M'" + shows "measure_space \ space = space M \ space M', + sets = Pow (space M \ space M'), + measure = prod_measure M M' \" + (is "measure_space ?space") +proof (rule finite_additivity_sufficient) + interpret M: measure_space M by fact + interpret M': measure_space M' by fact + + show "sigma_algebra ?space" + using sigma_algebra.sigma_algebra_extend[where M="\ space = space M \ space M', sets = Pow (space M \ space M') \"] + by (auto intro!: sigma_algebra_Pow) + then interpret sa: sigma_algebra ?space . + + have measure: "measure_space.measure (prod_measure_space M M') = prod_measure M M'" + unfolding prod_measure_space_def by simp + + { fix x y assume "y \ sets ?space" and "x \ space M" + hence "y \ space M \ space M'" + using sa.sets_into_space by simp + hence "Pair x -` y \ sets M'" + using `x \ space M` unfolding finM'(2)[symmetric] by auto } + note Pair_in_sets = this + + show "additive ?space (measure ?space)" + unfolding measure additive_def + proof safe + fix x y assume x: "x \ sets ?space" and y: "y \ sets ?space" + and disj_x_y: "x \ y = {}" + { fix z have "Pair z -` x \ Pair z -` y = {}" using disj_x_y by auto } + note Pair_disj = this + + from M'.measure_additive[OF Pair_in_sets[OF x] Pair_in_sets[OF y] Pair_disj, symmetric] + show "measure ?space (x \ y) = measure ?space x + measure ?space y" + apply (simp add: prod_measure_def) + apply (subst (1 2 3) M.integral_finite_singleton[OF finM]) + by (simp_all add: setsum_addf[symmetric] field_simps) + qed + + show "finite (space ?space)" using finM finM' by simp + + have singletonM: "\x. x \ space M \ {x} \ sets M" + unfolding finM(2)[symmetric] by simp + + show "positive ?space (measure ?space)" + unfolding positive_def + proof (safe, simp add: M.integral_zero prod_measure_def) + fix Q assume "Q \ sets ?space" + from Pair_in_sets[OF this] + show "0 \ measure ?space Q" + unfolding prod_measure_space_def prod_measure_def + apply (subst M.integral_finite_singleton[OF finM]) + using M.positive M'.positive singletonM + by (auto intro!: setsum_nonneg mult_nonneg_nonneg) + qed +qed + +end \ No newline at end of file