--- a/src/HOL/Probability/Binary_Product_Measure.thy Wed Oct 10 12:12:17 2012 +0200
+++ b/src/HOL/Probability/Binary_Product_Measure.thy Wed Oct 10 12:12:18 2012 +0200
@@ -43,6 +43,10 @@
unfolding pair_measure_def using space_closed[of A] space_closed[of B]
by (intro sets_measure_of) auto
+lemma sets_pair_measure_cong[cong]:
+ "sets M1 = sets M1' \<Longrightarrow> sets M2 = sets M2' \<Longrightarrow> sets (M1 \<Otimes>\<^isub>M M2) = sets (M1' \<Otimes>\<^isub>M M2')"
+ unfolding sets_pair_measure by (simp cong: sets_eq_imp_space_eq)
+
lemma pair_measureI[intro, simp]:
"x \<in> sets A \<Longrightarrow> y \<in> sets B \<Longrightarrow> x \<times> y \<in> sets (A \<Otimes>\<^isub>M B)"
by (auto simp: sets_pair_measure)
@@ -54,21 +58,30 @@
unfolding pair_measure_def using 1 2
by (intro measurable_measure_of) (auto dest: sets_into_space)
+lemma measurable_Pair:
+ assumes f: "f \<in> measurable M M1" and g: "g \<in> measurable M M2"
+ shows "(\<lambda>x. (f x, g x)) \<in> measurable M (M1 \<Otimes>\<^isub>M M2)"
+proof (rule measurable_pair_measureI)
+ show "(\<lambda>x. (f x, g x)) \<in> space M \<rightarrow> space M1 \<times> space M2"
+ using f g by (auto simp: measurable_def)
+ fix A B assume *: "A \<in> sets M1" "B \<in> sets M2"
+ have "(\<lambda>x. (f x, g x)) -` (A \<times> B) \<inter> space M = (f -` A \<inter> space M) \<inter> (g -` B \<inter> space M)"
+ by auto
+ also have "\<dots> \<in> sets M"
+ by (rule Int) (auto intro!: measurable_sets * f g)
+ finally show "(\<lambda>x. (f x, g x)) -` (A \<times> B) \<inter> space M \<in> sets M" .
+qed
+
+lemma measurable_pair:
+ assumes "(fst \<circ> f) \<in> measurable M M1" "(snd \<circ> f) \<in> measurable M M2"
+ shows "f \<in> measurable M (M1 \<Otimes>\<^isub>M M2)"
+ using measurable_Pair[OF assms] by simp
+
lemma measurable_fst[intro!, simp]: "fst \<in> measurable (M1 \<Otimes>\<^isub>M M2) M1"
- unfolding measurable_def
-proof safe
- fix A assume A: "A \<in> sets M1"
- from this[THEN sets_into_space] have "fst -` A \<inter> space M1 \<times> space M2 = A \<times> space M2" by auto
- with A show "fst -` A \<inter> space (M1 \<Otimes>\<^isub>M M2) \<in> sets (M1 \<Otimes>\<^isub>M M2)" by (simp add: space_pair_measure)
-qed (simp add: space_pair_measure)
+ by (auto simp: fst_vimage_eq_Times space_pair_measure sets_into_space times_Int_times measurable_def)
lemma measurable_snd[intro!, simp]: "snd \<in> measurable (M1 \<Otimes>\<^isub>M M2) M2"
- unfolding measurable_def
-proof safe
- fix A assume A: "A \<in> sets M2"
- from this[THEN sets_into_space] have "snd -` A \<inter> space M1 \<times> space M2 = space M1 \<times> A" by auto
- with A show "snd -` A \<inter> space (M1 \<Otimes>\<^isub>M M2) \<in> sets (M1 \<Otimes>\<^isub>M M2)" by (simp add: space_pair_measure)
-qed (simp add: space_pair_measure)
+ by (auto simp: snd_vimage_eq_Times space_pair_measure sets_into_space times_Int_times measurable_def)
lemma measurable_fst': "f \<in> measurable M (N \<Otimes>\<^isub>M P) \<Longrightarrow> (\<lambda>x. fst (f x)) \<in> measurable M N"
using measurable_comp[OF _ measurable_fst] by (auto simp: comp_def)
@@ -84,55 +97,29 @@
lemma measurable_pair_iff:
"f \<in> measurable M (M1 \<Otimes>\<^isub>M M2) \<longleftrightarrow> (fst \<circ> f) \<in> measurable M M1 \<and> (snd \<circ> f) \<in> measurable M M2"
-proof safe
- assume f: "(fst \<circ> f) \<in> measurable M M1" and s: "(snd \<circ> f) \<in> measurable M M2"
- show "f \<in> measurable M (M1 \<Otimes>\<^isub>M M2)"
- proof (rule measurable_pair_measureI)
- show "f \<in> space M \<rightarrow> space M1 \<times> space M2"
- using f s by (auto simp: mem_Times_iff measurable_def comp_def)
- fix A B assume "A \<in> sets M1" "B \<in> sets M2"
- moreover have "(fst \<circ> f) -` A \<inter> space M \<in> sets M" "(snd \<circ> f) -` B \<inter> space M \<in> sets M"
- using f `A \<in> sets M1` s `B \<in> sets M2` by (auto simp: measurable_sets)
- moreover have "f -` (A \<times> B) \<inter> space M = ((fst \<circ> f) -` A \<inter> space M) \<inter> ((snd \<circ> f) -` B \<inter> space M)"
- by (auto simp: vimage_Times)
- ultimately show "f -` (A \<times> B) \<inter> space M \<in> sets M" by auto
- qed
-qed auto
+ using measurable_pair[of f M M1 M2] by auto
-lemma measurable_pair:
- "(fst \<circ> f) \<in> measurable M M1 \<Longrightarrow> (snd \<circ> f) \<in> measurable M M2 \<Longrightarrow> f \<in> measurable M (M1 \<Otimes>\<^isub>M M2)"
- unfolding measurable_pair_iff by simp
+lemma measurable_split_conv:
+ "(\<lambda>(x, y). f x y) \<in> measurable A B \<longleftrightarrow> (\<lambda>x. f (fst x) (snd x)) \<in> measurable A B"
+ by (intro arg_cong2[where f="op \<in>"]) auto
lemma measurable_pair_swap': "(\<lambda>(x,y). (y, x)) \<in> measurable (M1 \<Otimes>\<^isub>M M2) (M2 \<Otimes>\<^isub>M M1)"
-proof (rule measurable_pair_measureI)
- fix A B assume "A \<in> sets M2" "B \<in> sets M1"
- moreover then have "(\<lambda>(x, y). (y, x)) -` (A \<times> B) \<inter> space (M1 \<Otimes>\<^isub>M M2) = B \<times> A"
- by (auto dest: sets_into_space simp: space_pair_measure)
- ultimately show "(\<lambda>(x, y). (y, x)) -` (A \<times> B) \<inter> space (M1 \<Otimes>\<^isub>M M2) \<in> sets (M1 \<Otimes>\<^isub>M M2)"
- by auto
-qed (auto simp add: space_pair_measure)
+ by (auto intro!: measurable_Pair simp: measurable_split_conv)
lemma measurable_pair_swap:
assumes f: "f \<in> measurable (M1 \<Otimes>\<^isub>M M2) M" shows "(\<lambda>(x,y). f (y, x)) \<in> measurable (M2 \<Otimes>\<^isub>M M1) M"
-proof -
- have "(\<lambda>x. f (case x of (x, y) \<Rightarrow> (y, x))) = (\<lambda>(x, y). f (y, x))" by auto
- then show ?thesis
- using measurable_comp[OF measurable_pair_swap' f] by (simp add: comp_def)
-qed
+ using measurable_comp[OF measurable_Pair f] by (auto simp: measurable_split_conv comp_def)
lemma measurable_pair_swap_iff:
"f \<in> measurable (M2 \<Otimes>\<^isub>M M1) M \<longleftrightarrow> (\<lambda>(x,y). f (y,x)) \<in> measurable (M1 \<Otimes>\<^isub>M M2) M"
using measurable_pair_swap[of "\<lambda>(x,y). f (y, x)"]
by (auto intro!: measurable_pair_swap)
+lemma measurable_ident[intro, simp]: "(\<lambda>x. x) \<in> measurable M M"
+ unfolding measurable_def by auto
+
lemma measurable_Pair1': "x \<in> space M1 \<Longrightarrow> Pair x \<in> measurable M2 (M1 \<Otimes>\<^isub>M M2)"
-proof (rule measurable_pair_measureI)
- fix A B assume "A \<in> sets M1" "B \<in> sets M2"
- moreover then have "Pair x -` (A \<times> B) \<inter> space M2 = (if x \<in> A then B else {})"
- by (auto dest: sets_into_space simp: space_pair_measure)
- ultimately show "Pair x -` (A \<times> B) \<inter> space M2 \<in> sets M2"
- by auto
-qed (auto simp add: space_pair_measure)
+ by (auto intro!: measurable_Pair)
lemma sets_Pair1: assumes A: "A \<in> sets (M1 \<Otimes>\<^isub>M M2)" shows "Pair x -` A \<in> sets M2"
proof -
@@ -144,8 +131,7 @@
qed
lemma measurable_Pair2': "y \<in> space M2 \<Longrightarrow> (\<lambda>x. (x, y)) \<in> measurable M1 (M1 \<Otimes>\<^isub>M M2)"
- using measurable_comp[OF measurable_Pair1' measurable_pair_swap', of y M2 M1]
- by (simp add: comp_def)
+ by (auto intro!: measurable_Pair)
lemma sets_Pair2: assumes A: "A \<in> sets (M1 \<Otimes>\<^isub>M M2)" shows "(\<lambda>x. (x, y)) -` A \<in> sets M1"
proof -
@@ -172,46 +158,131 @@
unfolding Int_stable_def
by safe (auto simp add: times_Int_times)
-lemma finite_measure_cut_measurable:
- assumes "sigma_finite_measure M1" "finite_measure M2"
- assumes "Q \<in> sets (M1 \<Otimes>\<^isub>M M2)"
- shows "(\<lambda>x. emeasure M2 (Pair x -` Q)) \<in> borel_measurable M1"
+lemma (in finite_measure) finite_measure_cut_measurable:
+ assumes "Q \<in> sets (N \<Otimes>\<^isub>M M)"
+ shows "(\<lambda>x. emeasure M (Pair x -` Q)) \<in> borel_measurable N"
(is "?s Q \<in> _")
proof -
- interpret M1: sigma_finite_measure M1 by fact
- interpret M2: finite_measure M2 by fact
- let ?\<Omega> = "space M1 \<times> space M2" and ?D = "{A\<in>sets (M1 \<Otimes>\<^isub>M M2). ?s A \<in> borel_measurable M1}"
+ let ?\<Omega> = "space N \<times> space M" and ?D = "{A\<in>sets (N \<Otimes>\<^isub>M M). ?s A \<in> borel_measurable N}"
note space_pair_measure[simp]
interpret dynkin_system ?\<Omega> ?D
proof (intro dynkin_systemI)
fix A assume "A \<in> ?D" then show "A \<subseteq> ?\<Omega>"
- using sets_into_space[of A "M1 \<Otimes>\<^isub>M M2"] by simp
+ using sets_into_space[of A "N \<Otimes>\<^isub>M M"] by simp
next
from top show "?\<Omega> \<in> ?D"
by (auto simp add: if_distrib intro!: measurable_If)
next
fix A assume "A \<in> ?D"
- with sets_into_space have "\<And>x. emeasure M2 (Pair x -` (?\<Omega> - A)) =
- (if x \<in> space M1 then emeasure M2 (space M2) - ?s A x else 0)"
+ with sets_into_space have "\<And>x. emeasure M (Pair x -` (?\<Omega> - A)) =
+ (if x \<in> space N then emeasure M (space M) - ?s A x else 0)"
by (auto intro!: emeasure_compl simp: vimage_Diff sets_Pair1)
with `A \<in> ?D` top show "?\<Omega> - A \<in> ?D"
by (auto intro!: measurable_If)
next
- fix F :: "nat \<Rightarrow> ('a\<times>'b) set" assume "disjoint_family F" "range F \<subseteq> ?D"
- moreover then have "\<And>x. emeasure M2 (\<Union>i. Pair x -` F i) = (\<Sum>i. ?s (F i) x)"
+ fix F :: "nat \<Rightarrow> ('b\<times>'a) set" assume "disjoint_family F" "range F \<subseteq> ?D"
+ moreover then have "\<And>x. emeasure M (\<Union>i. Pair x -` F i) = (\<Sum>i. ?s (F i) x)"
by (intro suminf_emeasure[symmetric]) (auto simp: disjoint_family_on_def sets_Pair1)
ultimately show "(\<Union>i. F i) \<in> ?D"
by (auto simp: vimage_UN intro!: borel_measurable_psuminf)
qed
- let ?G = "{a \<times> b | a b. a \<in> sets M1 \<and> b \<in> sets M2}"
+ let ?G = "{a \<times> b | a b. a \<in> sets N \<and> b \<in> sets M}"
have "sigma_sets ?\<Omega> ?G = ?D"
proof (rule dynkin_lemma)
show "?G \<subseteq> ?D"
by (auto simp: if_distrib Int_def[symmetric] intro!: measurable_If)
qed (auto simp: sets_pair_measure Int_stable_pair_measure_generator)
- with `Q \<in> sets (M1 \<Otimes>\<^isub>M M2)` have "Q \<in> ?D"
+ with `Q \<in> sets (N \<Otimes>\<^isub>M M)` have "Q \<in> ?D"
by (simp add: sets_pair_measure[symmetric])
- then show "?s Q \<in> borel_measurable M1" by simp
+ then show "?s Q \<in> borel_measurable N" by simp
+qed
+
+lemma (in sigma_finite_measure) measurable_emeasure_Pair:
+ assumes Q: "Q \<in> sets (N \<Otimes>\<^isub>M M)" shows "(\<lambda>x. emeasure M (Pair x -` Q)) \<in> borel_measurable N" (is "?s Q \<in> _")
+proof -
+ from sigma_finite_disjoint guess F . note F = this
+ then have F_sets: "\<And>i. F i \<in> sets M" by auto
+ let ?C = "\<lambda>x i. F i \<inter> Pair x -` Q"
+ { fix i
+ have [simp]: "space N \<times> F i \<inter> space N \<times> space M = space N \<times> F i"
+ using F sets_into_space by auto
+ let ?R = "density M (indicator (F i))"
+ have "finite_measure ?R"
+ using F by (intro finite_measureI) (auto simp: emeasure_restricted subset_eq)
+ then have "(\<lambda>x. emeasure ?R (Pair x -` (space N \<times> space ?R \<inter> Q))) \<in> borel_measurable N"
+ by (rule finite_measure.finite_measure_cut_measurable) (auto intro: Q)
+ moreover have "\<And>x. emeasure ?R (Pair x -` (space N \<times> space ?R \<inter> Q))
+ = emeasure M (F i \<inter> Pair x -` (space N \<times> space ?R \<inter> Q))"
+ using Q F_sets by (intro emeasure_restricted) (auto intro: sets_Pair1)
+ moreover have "\<And>x. F i \<inter> Pair x -` (space N \<times> space ?R \<inter> Q) = ?C x i"
+ using sets_into_space[OF Q] by (auto simp: space_pair_measure)
+ ultimately have "(\<lambda>x. emeasure M (?C x i)) \<in> borel_measurable N"
+ by simp }
+ moreover
+ { fix x
+ have "(\<Sum>i. emeasure M (?C x i)) = emeasure M (\<Union>i. ?C x i)"
+ proof (intro suminf_emeasure)
+ show "range (?C x) \<subseteq> sets M"
+ using F `Q \<in> sets (N \<Otimes>\<^isub>M M)` by (auto intro!: sets_Pair1)
+ have "disjoint_family F" using F by auto
+ show "disjoint_family (?C x)"
+ by (rule disjoint_family_on_bisimulation[OF `disjoint_family F`]) auto
+ qed
+ also have "(\<Union>i. ?C x i) = Pair x -` Q"
+ using F sets_into_space[OF `Q \<in> sets (N \<Otimes>\<^isub>M M)`]
+ by (auto simp: space_pair_measure)
+ finally have "emeasure M (Pair x -` Q) = (\<Sum>i. emeasure M (?C x i))"
+ by simp }
+ ultimately show ?thesis using `Q \<in> sets (N \<Otimes>\<^isub>M M)` F_sets
+ by auto
+qed
+
+lemma (in sigma_finite_measure) emeasure_pair_measure:
+ assumes "X \<in> sets (N \<Otimes>\<^isub>M M)"
+ shows "emeasure (N \<Otimes>\<^isub>M M) X = (\<integral>\<^isup>+ x. \<integral>\<^isup>+ y. indicator X (x, y) \<partial>M \<partial>N)" (is "_ = ?\<mu> X")
+proof (rule emeasure_measure_of[OF pair_measure_def])
+ show "positive (sets (N \<Otimes>\<^isub>M M)) ?\<mu>"
+ by (auto simp: positive_def positive_integral_positive)
+ have eq[simp]: "\<And>A x y. indicator A (x, y) = indicator (Pair x -` A) y"
+ by (auto simp: indicator_def)
+ show "countably_additive (sets (N \<Otimes>\<^isub>M M)) ?\<mu>"
+ proof (rule countably_additiveI)
+ fix F :: "nat \<Rightarrow> ('b \<times> 'a) set" assume F: "range F \<subseteq> sets (N \<Otimes>\<^isub>M M)" "disjoint_family F"
+ from F have *: "\<And>i. F i \<in> sets (N \<Otimes>\<^isub>M M)" "(\<Union>i. F i) \<in> sets (N \<Otimes>\<^isub>M M)" by auto
+ moreover from F have "\<And>i. (\<lambda>x. emeasure M (Pair x -` F i)) \<in> borel_measurable N"
+ by (intro measurable_emeasure_Pair) auto
+ moreover have "\<And>x. disjoint_family (\<lambda>i. Pair x -` F i)"
+ by (intro disjoint_family_on_bisimulation[OF F(2)]) auto
+ moreover have "\<And>x. range (\<lambda>i. Pair x -` F i) \<subseteq> sets M"
+ using F by (auto simp: sets_Pair1)
+ ultimately show "(\<Sum>n. ?\<mu> (F n)) = ?\<mu> (\<Union>i. F i)"
+ by (auto simp add: vimage_UN positive_integral_suminf[symmetric] suminf_emeasure subset_eq emeasure_nonneg sets_Pair1
+ intro!: positive_integral_cong positive_integral_indicator[symmetric])
+ qed
+ show "{a \<times> b |a b. a \<in> sets N \<and> b \<in> sets M} \<subseteq> Pow (space N \<times> space M)"
+ using space_closed[of N] space_closed[of M] by auto
+qed fact
+
+lemma (in sigma_finite_measure) emeasure_pair_measure_alt:
+ assumes X: "X \<in> sets (N \<Otimes>\<^isub>M M)"
+ shows "emeasure (N \<Otimes>\<^isub>M M) X = (\<integral>\<^isup>+x. emeasure M (Pair x -` X) \<partial>N)"
+proof -
+ have [simp]: "\<And>x y. indicator X (x, y) = indicator (Pair x -` X) y"
+ by (auto simp: indicator_def)
+ show ?thesis
+ using X by (auto intro!: positive_integral_cong simp: emeasure_pair_measure sets_Pair1)
+qed
+
+lemma (in sigma_finite_measure) emeasure_pair_measure_Times:
+ assumes A: "A \<in> sets N" and B: "B \<in> sets M"
+ shows "emeasure (N \<Otimes>\<^isub>M M) (A \<times> B) = emeasure N A * emeasure M B"
+proof -
+ have "emeasure (N \<Otimes>\<^isub>M M) (A \<times> B) = (\<integral>\<^isup>+x. emeasure M B * indicator A x \<partial>N)"
+ using A B by (auto intro!: positive_integral_cong simp: emeasure_pair_measure_alt)
+ also have "\<dots> = emeasure M B * emeasure N A"
+ using A by (simp add: emeasure_nonneg positive_integral_cmult_indicator)
+ finally show ?thesis
+ by (simp add: ac_simps)
qed
subsection {* Binary products of $\sigma$-finite emeasure spaces *}
@@ -219,114 +290,21 @@
locale pair_sigma_finite = M1: sigma_finite_measure M1 + M2: sigma_finite_measure M2
for M1 :: "'a measure" and M2 :: "'b measure"
-lemma sets_pair_measure_cong[cong]:
- "sets M1 = sets M1' \<Longrightarrow> sets M2 = sets M2' \<Longrightarrow> sets (M1 \<Otimes>\<^isub>M M2) = sets (M1' \<Otimes>\<^isub>M M2')"
- unfolding sets_pair_measure by (simp cong: sets_eq_imp_space_eq)
-
lemma (in pair_sigma_finite) measurable_emeasure_Pair1:
- assumes Q: "Q \<in> sets (M1 \<Otimes>\<^isub>M M2)" shows "(\<lambda>x. emeasure M2 (Pair x -` Q)) \<in> borel_measurable M1" (is "?s Q \<in> _")
-proof -
- from M2.sigma_finite_disjoint guess F . note F = this
- then have F_sets: "\<And>i. F i \<in> sets M2" by auto
- have M1: "sigma_finite_measure M1" ..
- let ?C = "\<lambda>x i. F i \<inter> Pair x -` Q"
- { fix i
- have [simp]: "space M1 \<times> F i \<inter> space M1 \<times> space M2 = space M1 \<times> F i"
- using F sets_into_space by auto
- let ?R = "density M2 (indicator (F i))"
- have "(\<lambda>x. emeasure ?R (Pair x -` (space M1 \<times> space ?R \<inter> Q))) \<in> borel_measurable M1"
- proof (intro finite_measure_cut_measurable[OF M1])
- show "finite_measure ?R"
- using F by (intro finite_measureI) (auto simp: emeasure_restricted subset_eq)
- show "(space M1 \<times> space ?R) \<inter> Q \<in> sets (M1 \<Otimes>\<^isub>M ?R)"
- using Q by (simp add: Int)
- qed
- moreover have "\<And>x. emeasure ?R (Pair x -` (space M1 \<times> space ?R \<inter> Q))
- = emeasure M2 (F i \<inter> Pair x -` (space M1 \<times> space ?R \<inter> Q))"
- using Q F_sets by (intro emeasure_restricted) (auto intro: sets_Pair1)
- moreover have "\<And>x. F i \<inter> Pair x -` (space M1 \<times> space ?R \<inter> Q) = ?C x i"
- using sets_into_space[OF Q] by (auto simp: space_pair_measure)
- ultimately have "(\<lambda>x. emeasure M2 (?C x i)) \<in> borel_measurable M1"
- by simp }
- moreover
- { fix x
- have "(\<Sum>i. emeasure M2 (?C x i)) = emeasure M2 (\<Union>i. ?C x i)"
- proof (intro suminf_emeasure)
- show "range (?C x) \<subseteq> sets M2"
- using F `Q \<in> sets (M1 \<Otimes>\<^isub>M M2)` by (auto intro!: sets_Pair1)
- have "disjoint_family F" using F by auto
- show "disjoint_family (?C x)"
- by (rule disjoint_family_on_bisimulation[OF `disjoint_family F`]) auto
- qed
- also have "(\<Union>i. ?C x i) = Pair x -` Q"
- using F sets_into_space[OF `Q \<in> sets (M1 \<Otimes>\<^isub>M M2)`]
- by (auto simp: space_pair_measure)
- finally have "emeasure M2 (Pair x -` Q) = (\<Sum>i. emeasure M2 (?C x i))"
- by simp }
- ultimately show ?thesis using `Q \<in> sets (M1 \<Otimes>\<^isub>M M2)` F_sets
- by auto
-qed
+ "Q \<in> sets (M1 \<Otimes>\<^isub>M M2) \<Longrightarrow> (\<lambda>x. emeasure M2 (Pair x -` Q)) \<in> borel_measurable M1"
+ using M2.measurable_emeasure_Pair .
lemma (in pair_sigma_finite) measurable_emeasure_Pair2:
assumes Q: "Q \<in> sets (M1 \<Otimes>\<^isub>M M2)" shows "(\<lambda>y. emeasure M1 ((\<lambda>x. (x, y)) -` Q)) \<in> borel_measurable M2"
proof -
- interpret Q: pair_sigma_finite M2 M1 by default
have "(\<lambda>(x, y). (y, x)) -` Q \<inter> space (M2 \<Otimes>\<^isub>M M1) \<in> sets (M2 \<Otimes>\<^isub>M M1)"
using Q measurable_pair_swap' by (auto intro: measurable_sets)
- note Q.measurable_emeasure_Pair1[OF this]
+ note M1.measurable_emeasure_Pair[OF this]
moreover have "\<And>y. Pair y -` ((\<lambda>(x, y). (y, x)) -` Q \<inter> space (M2 \<Otimes>\<^isub>M M1)) = (\<lambda>x. (x, y)) -` Q"
using Q[THEN sets_into_space] by (auto simp: space_pair_measure)
ultimately show ?thesis by simp
qed
-lemma (in pair_sigma_finite) emeasure_pair_measure:
- assumes "X \<in> sets (M1 \<Otimes>\<^isub>M M2)"
- shows "emeasure (M1 \<Otimes>\<^isub>M M2) X = (\<integral>\<^isup>+ x. \<integral>\<^isup>+ y. indicator X (x, y) \<partial>M2 \<partial>M1)" (is "_ = ?\<mu> X")
-proof (rule emeasure_measure_of[OF pair_measure_def])
- show "positive (sets (M1 \<Otimes>\<^isub>M M2)) ?\<mu>"
- by (auto simp: positive_def positive_integral_positive)
- have eq[simp]: "\<And>A x y. indicator A (x, y) = indicator (Pair x -` A) y"
- by (auto simp: indicator_def)
- show "countably_additive (sets (M1 \<Otimes>\<^isub>M M2)) ?\<mu>"
- proof (rule countably_additiveI)
- fix F :: "nat \<Rightarrow> ('a \<times> 'b) set" assume F: "range F \<subseteq> sets (M1 \<Otimes>\<^isub>M M2)" "disjoint_family F"
- from F have *: "\<And>i. F i \<in> sets (M1 \<Otimes>\<^isub>M M2)" "(\<Union>i. F i) \<in> sets (M1 \<Otimes>\<^isub>M M2)" by auto
- moreover from F have "\<And>i. (\<lambda>x. emeasure M2 (Pair x -` F i)) \<in> borel_measurable M1"
- by (intro measurable_emeasure_Pair1) auto
- moreover have "\<And>x. disjoint_family (\<lambda>i. Pair x -` F i)"
- by (intro disjoint_family_on_bisimulation[OF F(2)]) auto
- moreover have "\<And>x. range (\<lambda>i. Pair x -` F i) \<subseteq> sets M2"
- using F by (auto simp: sets_Pair1)
- ultimately show "(\<Sum>n. ?\<mu> (F n)) = ?\<mu> (\<Union>i. F i)"
- by (auto simp add: vimage_UN positive_integral_suminf[symmetric] suminf_emeasure subset_eq emeasure_nonneg sets_Pair1
- intro!: positive_integral_cong positive_integral_indicator[symmetric])
- qed
- show "{a \<times> b |a b. a \<in> sets M1 \<and> b \<in> sets M2} \<subseteq> Pow (space M1 \<times> space M2)"
- using space_closed[of M1] space_closed[of M2] by auto
-qed fact
-
-lemma (in pair_sigma_finite) emeasure_pair_measure_alt:
- assumes X: "X \<in> sets (M1 \<Otimes>\<^isub>M M2)"
- shows "emeasure (M1 \<Otimes>\<^isub>M M2) X = (\<integral>\<^isup>+x. emeasure M2 (Pair x -` X) \<partial>M1)"
-proof -
- have [simp]: "\<And>x y. indicator X (x, y) = indicator (Pair x -` X) y"
- by (auto simp: indicator_def)
- show ?thesis
- using X by (auto intro!: positive_integral_cong simp: emeasure_pair_measure sets_Pair1)
-qed
-
-lemma (in pair_sigma_finite) emeasure_pair_measure_Times:
- assumes A: "A \<in> sets M1" and B: "B \<in> sets M2"
- shows "emeasure (M1 \<Otimes>\<^isub>M M2) (A \<times> B) = emeasure M1 A * emeasure M2 B"
-proof -
- have "emeasure (M1 \<Otimes>\<^isub>M M2) (A \<times> B) = (\<integral>\<^isup>+x. emeasure M2 B * indicator A x \<partial>M1)"
- using A B by (auto intro!: positive_integral_cong simp: emeasure_pair_measure_alt)
- also have "\<dots> = emeasure M2 B * emeasure M1 A"
- using A by (simp add: emeasure_nonneg positive_integral_cmult_indicator)
- finally show ?thesis
- by (simp add: ac_simps)
-qed
-
lemma (in pair_sigma_finite) sigma_finite_up_in_pair_measure_generator:
defines "E \<equiv> {A \<times> B | A B. A \<in> sets M1 \<and> B \<in> sets M2}"
shows "\<exists>F::nat \<Rightarrow> ('a \<times> 'b) set. range F \<subseteq> E \<and> incseq F \<and> (\<Union>i. F i) = space M1 \<times> space M2 \<and>
@@ -396,7 +374,6 @@
lemma (in pair_sigma_finite) distr_pair_swap:
"M1 \<Otimes>\<^isub>M M2 = distr (M2 \<Otimes>\<^isub>M M1) (M1 \<Otimes>\<^isub>M M2) (\<lambda>(x, y). (y, x))" (is "?P = ?D")
proof -
- interpret Q: pair_sigma_finite M2 M1 by default
from sigma_finite_up_in_pair_measure_generator guess F :: "nat \<Rightarrow> ('a \<times> 'b) set" .. note F = this
let ?E = "{a \<times> b |a b. a \<in> sets M1 \<and> b \<in> sets M2}"
show ?thesis
@@ -416,7 +393,7 @@
have "(\<lambda>(y, x). (x, y)) -` X \<inter> space (M2 \<Otimes>\<^isub>M M1) = B \<times> A"
using sets_into_space[OF A] sets_into_space[OF B] by (auto simp: space_pair_measure)
with A B show "emeasure (M1 \<Otimes>\<^isub>M M2) X = emeasure ?D X"
- by (simp add: emeasure_pair_measure_Times Q.emeasure_pair_measure_Times emeasure_distr
+ by (simp add: M2.emeasure_pair_measure_Times M1.emeasure_pair_measure_Times emeasure_distr
measurable_pair_swap' ac_simps)
qed
qed
@@ -426,13 +403,84 @@
shows "emeasure (M1 \<Otimes>\<^isub>M M2) A = (\<integral>\<^isup>+y. emeasure M1 ((\<lambda>x. (x, y)) -` A) \<partial>M2)"
(is "_ = ?\<nu> A")
proof -
- interpret Q: pair_sigma_finite M2 M1 by default
have [simp]: "\<And>y. (Pair y -` ((\<lambda>(x, y). (y, x)) -` A \<inter> space (M2 \<Otimes>\<^isub>M M1))) = (\<lambda>x. (x, y)) -` A"
using sets_into_space[OF A] by (auto simp: space_pair_measure)
show ?thesis using A
by (subst distr_pair_swap)
(simp_all del: vimage_Int add: measurable_sets[OF measurable_pair_swap']
- Q.emeasure_pair_measure_alt emeasure_distr[OF measurable_pair_swap' A])
+ M1.emeasure_pair_measure_alt emeasure_distr[OF measurable_pair_swap' A])
+qed
+
+lemma (in pair_sigma_finite) AE_pair:
+ assumes "AE x in (M1 \<Otimes>\<^isub>M M2). Q x"
+ shows "AE x in M1. (AE y in M2. Q (x, y))"
+proof -
+ obtain N where N: "N \<in> sets (M1 \<Otimes>\<^isub>M M2)" "emeasure (M1 \<Otimes>\<^isub>M M2) N = 0" "{x\<in>space (M1 \<Otimes>\<^isub>M M2). \<not> Q x} \<subseteq> N"
+ using assms unfolding eventually_ae_filter by auto
+ show ?thesis
+ proof (rule AE_I)
+ from N measurable_emeasure_Pair1[OF `N \<in> sets (M1 \<Otimes>\<^isub>M M2)`]
+ show "emeasure M1 {x\<in>space M1. emeasure M2 (Pair x -` N) \<noteq> 0} = 0"
+ by (auto simp: M2.emeasure_pair_measure_alt positive_integral_0_iff emeasure_nonneg)
+ show "{x \<in> space M1. emeasure M2 (Pair x -` N) \<noteq> 0} \<in> sets M1"
+ by (intro borel_measurable_ereal_neq_const measurable_emeasure_Pair1 N)
+ { fix x assume "x \<in> space M1" "emeasure M2 (Pair x -` N) = 0"
+ have "AE y in M2. Q (x, y)"
+ proof (rule AE_I)
+ show "emeasure M2 (Pair x -` N) = 0" by fact
+ show "Pair x -` N \<in> sets M2" using N(1) by (rule sets_Pair1)
+ show "{y \<in> space M2. \<not> Q (x, y)} \<subseteq> Pair x -` N"
+ using N `x \<in> space M1` unfolding space_pair_measure by auto
+ qed }
+ then show "{x \<in> space M1. \<not> (AE y in M2. Q (x, y))} \<subseteq> {x \<in> space M1. emeasure M2 (Pair x -` N) \<noteq> 0}"
+ by auto
+ qed
+qed
+
+lemma (in pair_sigma_finite) AE_pair_measure:
+ assumes "{x\<in>space (M1 \<Otimes>\<^isub>M M2). P x} \<in> sets (M1 \<Otimes>\<^isub>M M2)"
+ assumes ae: "AE x in M1. AE y in M2. P (x, y)"
+ shows "AE x in M1 \<Otimes>\<^isub>M M2. P x"
+proof (subst AE_iff_measurable[OF _ refl])
+ show "{x\<in>space (M1 \<Otimes>\<^isub>M M2). \<not> P x} \<in> sets (M1 \<Otimes>\<^isub>M M2)"
+ by (rule sets_Collect) fact
+ then have "emeasure (M1 \<Otimes>\<^isub>M M2) {x \<in> space (M1 \<Otimes>\<^isub>M M2). \<not> P x} =
+ (\<integral>\<^isup>+ x. \<integral>\<^isup>+ y. indicator {x \<in> space (M1 \<Otimes>\<^isub>M M2). \<not> P x} (x, y) \<partial>M2 \<partial>M1)"
+ by (simp add: M2.emeasure_pair_measure)
+ also have "\<dots> = (\<integral>\<^isup>+ x. \<integral>\<^isup>+ y. 0 \<partial>M2 \<partial>M1)"
+ using ae
+ apply (safe intro!: positive_integral_cong_AE)
+ apply (intro AE_I2)
+ apply (safe intro!: positive_integral_cong_AE)
+ apply auto
+ done
+ finally show "emeasure (M1 \<Otimes>\<^isub>M M2) {x \<in> space (M1 \<Otimes>\<^isub>M M2). \<not> P x} = 0" by simp
+qed
+
+lemma (in pair_sigma_finite) AE_pair_iff:
+ "{x\<in>space (M1 \<Otimes>\<^isub>M M2). P (fst x) (snd x)} \<in> sets (M1 \<Otimes>\<^isub>M M2) \<Longrightarrow>
+ (AE x in M1. AE y in M2. P x y) \<longleftrightarrow> (AE x in (M1 \<Otimes>\<^isub>M M2). P (fst x) (snd x))"
+ using AE_pair[of "\<lambda>x. P (fst x) (snd x)"] AE_pair_measure[of "\<lambda>x. P (fst x) (snd x)"] by auto
+
+lemma (in pair_sigma_finite) AE_commute:
+ assumes P: "{x\<in>space (M1 \<Otimes>\<^isub>M M2). P (fst x) (snd x)} \<in> sets (M1 \<Otimes>\<^isub>M M2)"
+ shows "(AE x in M1. AE y in M2. P x y) \<longleftrightarrow> (AE y in M2. AE x in M1. P x y)"
+proof -
+ interpret Q: pair_sigma_finite M2 M1 ..
+ have [simp]: "\<And>x. (fst (case x of (x, y) \<Rightarrow> (y, x))) = snd x" "\<And>x. (snd (case x of (x, y) \<Rightarrow> (y, x))) = fst x"
+ by auto
+ have "{x \<in> space (M2 \<Otimes>\<^isub>M M1). P (snd x) (fst x)} =
+ (\<lambda>(x, y). (y, x)) -` {x \<in> space (M1 \<Otimes>\<^isub>M M2). P (fst x) (snd x)} \<inter> space (M2 \<Otimes>\<^isub>M M1)"
+ by (auto simp: space_pair_measure)
+ also have "\<dots> \<in> sets (M2 \<Otimes>\<^isub>M M1)"
+ by (intro sets_pair_swap P)
+ finally show ?thesis
+ apply (subst AE_pair_iff[OF P])
+ apply (subst distr_pair_swap)
+ apply (subst AE_distr_iff[OF measurable_pair_swap' P])
+ apply (subst Q.AE_pair_iff)
+ apply simp_all
+ done
qed
section "Fubinis theorem"
@@ -494,7 +542,7 @@
positive_integral_cmult
positive_integral_cong[OF eq]
positive_integral_eq_simple_integral[OF f]
- emeasure_pair_measure_alt[symmetric])
+ M2.emeasure_pair_measure_alt[symmetric])
qed
lemma (in pair_sigma_finite) positive_integral_fst_measurable:
@@ -558,96 +606,6 @@
unfolding positive_integral_snd_measurable[OF assms]
unfolding positive_integral_fst_measurable[OF assms] ..
-lemma (in pair_sigma_finite) AE_pair:
- assumes "AE x in (M1 \<Otimes>\<^isub>M M2). Q x"
- shows "AE x in M1. (AE y in M2. Q (x, y))"
-proof -
- obtain N where N: "N \<in> sets (M1 \<Otimes>\<^isub>M M2)" "emeasure (M1 \<Otimes>\<^isub>M M2) N = 0" "{x\<in>space (M1 \<Otimes>\<^isub>M M2). \<not> Q x} \<subseteq> N"
- using assms unfolding eventually_ae_filter by auto
- show ?thesis
- proof (rule AE_I)
- from N measurable_emeasure_Pair1[OF `N \<in> sets (M1 \<Otimes>\<^isub>M M2)`]
- show "emeasure M1 {x\<in>space M1. emeasure M2 (Pair x -` N) \<noteq> 0} = 0"
- by (auto simp: emeasure_pair_measure_alt positive_integral_0_iff emeasure_nonneg)
- show "{x \<in> space M1. emeasure M2 (Pair x -` N) \<noteq> 0} \<in> sets M1"
- by (intro borel_measurable_ereal_neq_const measurable_emeasure_Pair1 N)
- { fix x assume "x \<in> space M1" "emeasure M2 (Pair x -` N) = 0"
- have "AE y in M2. Q (x, y)"
- proof (rule AE_I)
- show "emeasure M2 (Pair x -` N) = 0" by fact
- show "Pair x -` N \<in> sets M2" using N(1) by (rule sets_Pair1)
- show "{y \<in> space M2. \<not> Q (x, y)} \<subseteq> Pair x -` N"
- using N `x \<in> space M1` unfolding space_pair_measure by auto
- qed }
- then show "{x \<in> space M1. \<not> (AE y in M2. Q (x, y))} \<subseteq> {x \<in> space M1. emeasure M2 (Pair x -` N) \<noteq> 0}"
- by auto
- qed
-qed
-
-lemma (in pair_sigma_finite) AE_pair_measure:
- assumes "{x\<in>space (M1 \<Otimes>\<^isub>M M2). P x} \<in> sets (M1 \<Otimes>\<^isub>M M2)"
- assumes ae: "AE x in M1. AE y in M2. P (x, y)"
- shows "AE x in M1 \<Otimes>\<^isub>M M2. P x"
-proof (subst AE_iff_measurable[OF _ refl])
- show "{x\<in>space (M1 \<Otimes>\<^isub>M M2). \<not> P x} \<in> sets (M1 \<Otimes>\<^isub>M M2)"
- by (rule sets_Collect) fact
- then have "emeasure (M1 \<Otimes>\<^isub>M M2) {x \<in> space (M1 \<Otimes>\<^isub>M M2). \<not> P x} =
- (\<integral>\<^isup>+ x. \<integral>\<^isup>+ y. indicator {x \<in> space (M1 \<Otimes>\<^isub>M M2). \<not> P x} (x, y) \<partial>M2 \<partial>M1)"
- by (simp add: emeasure_pair_measure)
- also have "\<dots> = (\<integral>\<^isup>+ x. \<integral>\<^isup>+ y. 0 \<partial>M2 \<partial>M1)"
- using ae
- apply (safe intro!: positive_integral_cong_AE)
- apply (intro AE_I2)
- apply (safe intro!: positive_integral_cong_AE)
- apply auto
- done
- finally show "emeasure (M1 \<Otimes>\<^isub>M M2) {x \<in> space (M1 \<Otimes>\<^isub>M M2). \<not> P x} = 0" by simp
-qed
-
-lemma (in pair_sigma_finite) AE_pair_iff:
- "{x\<in>space (M1 \<Otimes>\<^isub>M M2). P (fst x) (snd x)} \<in> sets (M1 \<Otimes>\<^isub>M M2) \<Longrightarrow>
- (AE x in M1. AE y in M2. P x y) \<longleftrightarrow> (AE x in (M1 \<Otimes>\<^isub>M M2). P (fst x) (snd x))"
- using AE_pair[of "\<lambda>x. P (fst x) (snd x)"] AE_pair_measure[of "\<lambda>x. P (fst x) (snd x)"] by auto
-
-lemma AE_distr_iff:
- assumes f: "f \<in> measurable M N" and P: "{x \<in> space N. P x} \<in> sets N"
- shows "(AE x in distr M N f. P x) \<longleftrightarrow> (AE x in M. P (f x))"
-proof (subst (1 2) AE_iff_measurable[OF _ refl])
- from P show "{x \<in> space (distr M N f). \<not> P x} \<in> sets (distr M N f)"
- by (auto intro!: sets_Collect_neg)
- moreover
- have "f -` {x \<in> space N. P x} \<inter> space M = {x \<in> space M. P (f x)}"
- using f by (auto dest: measurable_space)
- then show "{x \<in> space M. \<not> P (f x)} \<in> sets M"
- using measurable_sets[OF f P] by (auto intro!: sets_Collect_neg)
- moreover have "f -` {x\<in>space N. \<not> P x} \<inter> space M = {x \<in> space M. \<not> P (f x)}"
- using f by (auto dest: measurable_space)
- ultimately show "(emeasure (distr M N f) {x \<in> space (distr M N f). \<not> P x} = 0) =
- (emeasure M {x \<in> space M. \<not> P (f x)} = 0)"
- using f by (simp add: emeasure_distr)
-qed
-
-lemma (in pair_sigma_finite) AE_commute:
- assumes P: "{x\<in>space (M1 \<Otimes>\<^isub>M M2). P (fst x) (snd x)} \<in> sets (M1 \<Otimes>\<^isub>M M2)"
- shows "(AE x in M1. AE y in M2. P x y) \<longleftrightarrow> (AE y in M2. AE x in M1. P x y)"
-proof -
- interpret Q: pair_sigma_finite M2 M1 ..
- have [simp]: "\<And>x. (fst (case x of (x, y) \<Rightarrow> (y, x))) = snd x" "\<And>x. (snd (case x of (x, y) \<Rightarrow> (y, x))) = fst x"
- by auto
- have "{x \<in> space (M2 \<Otimes>\<^isub>M M1). P (snd x) (fst x)} =
- (\<lambda>(x, y). (y, x)) -` {x \<in> space (M1 \<Otimes>\<^isub>M M2). P (fst x) (snd x)} \<inter> space (M2 \<Otimes>\<^isub>M M1)"
- by (auto simp: space_pair_measure)
- also have "\<dots> \<in> sets (M2 \<Otimes>\<^isub>M M1)"
- by (intro sets_pair_swap P)
- finally show ?thesis
- apply (subst AE_pair_iff[OF P])
- apply (subst distr_pair_swap)
- apply (subst AE_distr_iff[OF measurable_pair_swap' P])
- apply (subst Q.AE_pair_iff)
- apply simp_all
- done
-qed
-
lemma (in pair_sigma_finite) integrable_product_swap:
assumes "integrable (M1 \<Otimes>\<^isub>M M2) f"
shows "integrable (M2 \<Otimes>\<^isub>M M1) (\<lambda>(x,y). f (y,x))"
@@ -817,7 +775,7 @@
by (intro finite_subset[OF _ B]) auto
have fin_X: "finite X" using X_subset by (rule finite_subset) (auto simp: A B)
show "emeasure ?P X = emeasure ?C X"
- apply (subst P.emeasure_pair_measure_alt[OF X])
+ apply (subst B.emeasure_pair_measure_alt[OF X])
apply (subst emeasure_count_space)
using X_subset apply auto []
apply (simp add: fin_Pair emeasure_count_space X_subset fin_X)
@@ -861,7 +819,7 @@
by simp
show "emeasure ?L A = emeasure ?R A"
- apply (subst L.emeasure_pair_measure[OF A])
+ apply (subst D2.emeasure_pair_measure[OF A])
apply (subst emeasure_density)
using f_fst g_snd apply (simp add: split_beta')
using A apply simp
@@ -924,7 +882,7 @@
by (auto simp: measurable_pair_iff)
fix A assume A: "A \<in> sets ?P"
then have "emeasure ?P A = (\<integral>\<^isup>+x. emeasure (distr N T g) (Pair x -` A) \<partial>distr M S f)"
- by (rule ST.emeasure_pair_measure_alt)
+ by (rule T.emeasure_pair_measure_alt)
also have "\<dots> = (\<integral>\<^isup>+x. emeasure N (g -` (Pair x -` A) \<inter> space N) \<partial>distr M S f)"
using g A by (simp add: sets_Pair1 emeasure_distr)
also have "\<dots> = (\<integral>\<^isup>+x. emeasure N (g -` (Pair (f x) -` A) \<inter> space N) \<partial>M)"
@@ -933,7 +891,7 @@
also have "\<dots> = (\<integral>\<^isup>+x. emeasure N (Pair x -` ((\<lambda>(x, y). (f x, g y)) -` A \<inter> space (M \<Otimes>\<^isub>M N))) \<partial>M)"
by (intro positive_integral_cong arg_cong2[where f=emeasure]) (auto simp: space_pair_measure)
also have "\<dots> = emeasure (M \<Otimes>\<^isub>M N) ((\<lambda>(x, y). (f x, g y)) -` A \<inter> space (M \<Otimes>\<^isub>M N))"
- using fg by (intro MN.emeasure_pair_measure_alt[symmetric] measurable_sets[OF _ A])
+ using fg by (intro N.emeasure_pair_measure_alt[symmetric] measurable_sets[OF _ A])
(auto cong: measurable_cong')
also have "\<dots> = emeasure ?D A"
using fg A by (subst emeasure_distr) auto
--- a/src/HOL/Probability/Finite_Product_Measure.thy Wed Oct 10 12:12:17 2012 +0200
+++ b/src/HOL/Probability/Finite_Product_Measure.thy Wed Oct 10 12:12:18 2012 +0200
@@ -504,8 +504,7 @@
qed (insert `i \<in> I`, auto simp: space_PiM)
lemma measurable_add_dim:
- assumes "i \<notin> I"
- shows "(\<lambda>(f, y). f(i := y)) \<in> measurable (Pi\<^isub>M I M \<Otimes>\<^isub>M M i) (Pi\<^isub>M (insert i I) M)"
+ "(\<lambda>(f, y). f(i := y)) \<in> measurable (Pi\<^isub>M I M \<Otimes>\<^isub>M M i) (Pi\<^isub>M (insert i I) M)"
(is "?f \<in> measurable ?P ?I")
proof (rule measurable_PiM_single)
fix j A assume j: "j \<in> insert i I" and A: "A \<in> sets (M j)"
@@ -519,19 +518,18 @@
qed (auto simp: space_pair_measure space_PiM)
lemma measurable_merge:
- assumes "I \<inter> J = {}"
- shows "(\<lambda>(x, y). merge I x J y) \<in> measurable (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M) (Pi\<^isub>M (I \<union> J) M)"
+ "(\<lambda>(x, y). merge I x J y) \<in> measurable (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M) (Pi\<^isub>M (I \<union> J) M)"
(is "?f \<in> measurable ?P ?U")
proof (rule measurable_PiM_single)
fix i A assume A: "A \<in> sets (M i)" "i \<in> I \<union> J"
- then have "{\<omega> \<in> space ?P. prod_case (\<lambda>x. merge I x J) \<omega> i \<in> A} =
+ then have "{\<omega> \<in> space ?P. prod_case (\<lambda>x y. merge I x J y) \<omega> i \<in> A} =
(if i \<in> I then ((\<lambda>x. x i) \<circ> fst) -` A \<inter> space ?P else ((\<lambda>x. x i) \<circ> snd) -` A \<inter> space ?P)"
- using `I \<inter> J = {}` by auto
+ by (auto simp: merge_def)
also have "\<dots> \<in> sets ?P"
using A
by (auto intro!: measurable_sets[OF measurable_comp, OF _ measurable_component_singleton])
- finally show "{\<omega> \<in> space ?P. prod_case (\<lambda>x. merge I x J) \<omega> i \<in> A} \<in> sets ?P" .
-qed (insert assms, auto simp: space_pair_measure space_PiM)
+ finally show "{\<omega> \<in> space ?P. prod_case (\<lambda>x y. merge I x J y) \<omega> i \<in> A} \<in> sets ?P" .
+qed (auto simp: space_pair_measure space_PiM Pi_iff merge_def extensional_def)
lemma measurable_restrict:
assumes X: "\<And>i. i \<in> I \<Longrightarrow> X i \<in> measurable N (M i)"
@@ -587,12 +585,9 @@
qed
qed
-lemma (in product_sigma_finite)
- assumes "finite I"
- shows sigma_finite: "sigma_finite_measure (PiM I M)"
- and emeasure_PiM:
- "\<And>A. (\<And>i. i\<in>I \<Longrightarrow> A i \<in> sets (M i)) \<Longrightarrow> emeasure (PiM I M) (Pi\<^isub>E I A) = (\<Prod>i\<in>I. emeasure (M i) (A i))"
-using `finite I` proof induct
+lemma (in product_sigma_finite) emeasure_PiM:
+ "finite I \<Longrightarrow> (\<And>i. i\<in>I \<Longrightarrow> A i \<in> sets (M i)) \<Longrightarrow> emeasure (PiM I M) (Pi\<^isub>E I A) = (\<Prod>i\<in>I. emeasure (M i) (A i))"
+proof (induct I arbitrary: A rule: finite_induct)
case empty
let ?\<mu> = "\<lambda>A. if A = {} then 0 else (1::ereal)"
have "prod_algebra {} M = {{\<lambda>_. undefined}}"
@@ -610,21 +605,13 @@
qed (auto simp: prod_emb_def)
also have *: "(prod_emb {} M {} (\<Pi>\<^isub>E i\<in>{}. {})) = {\<lambda>_. undefined}"
by (auto simp: prod_emb_def)
- finally have emeasure_eq: "emeasure (Pi\<^isub>M {} M) {\<lambda>_. undefined} = 1" .
-
- interpret finite_measure "PiM {} M"
- by default (simp add: space_PiM emeasure_eq)
- case 1 show ?case ..
-
- case 2 show ?case
- using emeasure_eq * by simp
+ finally show ?case
+ using * by simp
next
case (insert i I)
interpret finite_product_sigma_finite M I by default fact
have "finite (insert i I)" using `finite I` by auto
interpret I': finite_product_sigma_finite M "insert i I" by default fact
- interpret I: sigma_finite_measure "PiM I M" by fact
- interpret P: pair_sigma_finite "PiM I M" "M i" ..
let ?h = "(\<lambda>(f, y). f(i := y))"
let ?P = "distr (Pi\<^isub>M I M \<Otimes>\<^isub>M M i) (Pi\<^isub>M (insert i I) M) ?h"
@@ -632,67 +619,73 @@
let ?I = "{j \<in> insert i I. emeasure (M j) (space (M j)) \<noteq> 1}"
let ?f = "\<lambda>J E j. if j \<in> J then emeasure (M j) (E j) else emeasure (M j) (space (M j))"
- { case 2
- have "emeasure (Pi\<^isub>M (insert i I) M) (prod_emb (insert i I) M (insert i I) (Pi\<^isub>E (insert i I) A)) =
- (\<Prod>i\<in>insert i I. emeasure (M i) (A i))"
- proof (subst emeasure_extend_measure_Pair[OF PiM_def])
- fix J E assume "(J \<noteq> {} \<or> insert i I = {}) \<and> finite J \<and> J \<subseteq> insert i I \<and> E \<in> (\<Pi> j\<in>J. sets (M j))"
- then have J: "J \<noteq> {}" "finite J" "J \<subseteq> insert i I" and E: "\<forall>j\<in>J. E j \<in> sets (M j)" by auto
- let ?p = "prod_emb (insert i I) M J (Pi\<^isub>E J E)"
- let ?p' = "prod_emb I M (J - {i}) (\<Pi>\<^isub>E j\<in>J-{i}. E j)"
- have "?\<mu> ?p =
- emeasure (Pi\<^isub>M I M \<Otimes>\<^isub>M (M i)) (?h -` ?p \<inter> space (Pi\<^isub>M I M \<Otimes>\<^isub>M M i))"
- by (intro emeasure_distr measurable_add_dim sets_PiM_I) fact+
- also have "?h -` ?p \<inter> space (Pi\<^isub>M I M \<Otimes>\<^isub>M M i) = ?p' \<times> (if i \<in> J then E i else space (M i))"
- using J E[rule_format, THEN sets_into_space]
- by (force simp: space_pair_measure space_PiM Pi_iff prod_emb_iff split: split_if_asm)
- also have "emeasure (Pi\<^isub>M I M \<Otimes>\<^isub>M (M i)) (?p' \<times> (if i \<in> J then E i else space (M i))) =
- emeasure (Pi\<^isub>M I M) ?p' * emeasure (M i) (if i \<in> J then (E i) else space (M i))"
- using J E by (intro P.emeasure_pair_measure_Times sets_PiM_I) auto
- also have "?p' = (\<Pi>\<^isub>E j\<in>I. if j \<in> J-{i} then E j else space (M j))"
- using J E[rule_format, THEN sets_into_space]
- by (auto simp: prod_emb_iff Pi_iff split: split_if_asm) blast+
- also have "emeasure (Pi\<^isub>M I M) (\<Pi>\<^isub>E j\<in>I. if j \<in> J-{i} then E j else space (M j)) =
- (\<Prod> j\<in>I. if j \<in> J-{i} then emeasure (M j) (E j) else emeasure (M j) (space (M j)))"
- using E by (subst insert) (auto intro!: setprod_cong)
- also have "(\<Prod>j\<in>I. if j \<in> J - {i} then emeasure (M j) (E j) else emeasure (M j) (space (M j))) *
- emeasure (M i) (if i \<in> J then E i else space (M i)) = (\<Prod>j\<in>insert i I. ?f J E j)"
- using insert by (auto simp: mult_commute intro!: arg_cong2[where f="op *"] setprod_cong)
- also have "\<dots> = (\<Prod>j\<in>J \<union> ?I. ?f J E j)"
- using insert(1,2) J E by (intro setprod_mono_one_right) auto
- finally show "?\<mu> ?p = \<dots>" .
+ have "emeasure (Pi\<^isub>M (insert i I) M) (prod_emb (insert i I) M (insert i I) (Pi\<^isub>E (insert i I) A)) =
+ (\<Prod>i\<in>insert i I. emeasure (M i) (A i))"
+ proof (subst emeasure_extend_measure_Pair[OF PiM_def])
+ fix J E assume "(J \<noteq> {} \<or> insert i I = {}) \<and> finite J \<and> J \<subseteq> insert i I \<and> E \<in> (\<Pi> j\<in>J. sets (M j))"
+ then have J: "J \<noteq> {}" "finite J" "J \<subseteq> insert i I" and E: "\<forall>j\<in>J. E j \<in> sets (M j)" by auto
+ let ?p = "prod_emb (insert i I) M J (Pi\<^isub>E J E)"
+ let ?p' = "prod_emb I M (J - {i}) (\<Pi>\<^isub>E j\<in>J-{i}. E j)"
+ have "?\<mu> ?p =
+ emeasure (Pi\<^isub>M I M \<Otimes>\<^isub>M (M i)) (?h -` ?p \<inter> space (Pi\<^isub>M I M \<Otimes>\<^isub>M M i))"
+ by (intro emeasure_distr measurable_add_dim sets_PiM_I) fact+
+ also have "?h -` ?p \<inter> space (Pi\<^isub>M I M \<Otimes>\<^isub>M M i) = ?p' \<times> (if i \<in> J then E i else space (M i))"
+ using J E[rule_format, THEN sets_into_space]
+ by (force simp: space_pair_measure space_PiM Pi_iff prod_emb_iff split: split_if_asm)
+ also have "emeasure (Pi\<^isub>M I M \<Otimes>\<^isub>M (M i)) (?p' \<times> (if i \<in> J then E i else space (M i))) =
+ emeasure (Pi\<^isub>M I M) ?p' * emeasure (M i) (if i \<in> J then (E i) else space (M i))"
+ using J E by (intro M.emeasure_pair_measure_Times sets_PiM_I) auto
+ also have "?p' = (\<Pi>\<^isub>E j\<in>I. if j \<in> J-{i} then E j else space (M j))"
+ using J E[rule_format, THEN sets_into_space]
+ by (auto simp: prod_emb_iff Pi_iff split: split_if_asm) blast+
+ also have "emeasure (Pi\<^isub>M I M) (\<Pi>\<^isub>E j\<in>I. if j \<in> J-{i} then E j else space (M j)) =
+ (\<Prod> j\<in>I. if j \<in> J-{i} then emeasure (M j) (E j) else emeasure (M j) (space (M j)))"
+ using E by (subst insert) (auto intro!: setprod_cong)
+ also have "(\<Prod>j\<in>I. if j \<in> J - {i} then emeasure (M j) (E j) else emeasure (M j) (space (M j))) *
+ emeasure (M i) (if i \<in> J then E i else space (M i)) = (\<Prod>j\<in>insert i I. ?f J E j)"
+ using insert by (auto simp: mult_commute intro!: arg_cong2[where f="op *"] setprod_cong)
+ also have "\<dots> = (\<Prod>j\<in>J \<union> ?I. ?f J E j)"
+ using insert(1,2) J E by (intro setprod_mono_one_right) auto
+ finally show "?\<mu> ?p = \<dots>" .
- show "prod_emb (insert i I) M J (Pi\<^isub>E J E) \<in> Pow (\<Pi>\<^isub>E i\<in>insert i I. space (M i))"
- using J E[rule_format, THEN sets_into_space] by (auto simp: prod_emb_iff)
- next
- show "positive (sets (Pi\<^isub>M (insert i I) M)) ?\<mu>" "countably_additive (sets (Pi\<^isub>M (insert i I) M)) ?\<mu>"
- using emeasure_positive[of ?P] emeasure_countably_additive[of ?P] by simp_all
- next
- show "(insert i I \<noteq> {} \<or> insert i I = {}) \<and> finite (insert i I) \<and>
- insert i I \<subseteq> insert i I \<and> A \<in> (\<Pi> j\<in>insert i I. sets (M j))"
- using insert(1,2) 2 by auto
- qed (auto intro!: setprod_cong)
- with 2[THEN sets_into_space] show ?case by (subst (asm) prod_emb_PiE_same_index) auto }
- note product = this
+ show "prod_emb (insert i I) M J (Pi\<^isub>E J E) \<in> Pow (\<Pi>\<^isub>E i\<in>insert i I. space (M i))"
+ using J E[rule_format, THEN sets_into_space] by (auto simp: prod_emb_iff)
+ next
+ show "positive (sets (Pi\<^isub>M (insert i I) M)) ?\<mu>" "countably_additive (sets (Pi\<^isub>M (insert i I) M)) ?\<mu>"
+ using emeasure_positive[of ?P] emeasure_countably_additive[of ?P] by simp_all
+ next
+ show "(insert i I \<noteq> {} \<or> insert i I = {}) \<and> finite (insert i I) \<and>
+ insert i I \<subseteq> insert i I \<and> A \<in> (\<Pi> j\<in>insert i I. sets (M j))"
+ using insert by auto
+ qed (auto intro!: setprod_cong)
+ with insert show ?case
+ by (subst (asm) prod_emb_PiE_same_index) (auto intro!: sets_into_space)
+qed
- from I'.sigma_finite_pairs guess F :: "'i \<Rightarrow> nat \<Rightarrow> 'a set" ..
- then have F: "\<And>j. j \<in> insert i I \<Longrightarrow> range (F j) \<subseteq> sets (M j)"
- "incseq (\<lambda>k. \<Pi>\<^isub>E j \<in> insert i I. F j k)"
- "(\<Union>k. \<Pi>\<^isub>E j \<in> insert i I. F j k) = space (Pi\<^isub>M (insert i I) M)"
- "\<And>k. \<And>j. j \<in> insert i I \<Longrightarrow> emeasure (M j) (F j k) \<noteq> \<infinity>"
+lemma (in product_sigma_finite) sigma_finite:
+ assumes "finite I"
+ shows "sigma_finite_measure (PiM I M)"
+proof -
+ interpret finite_product_sigma_finite M I by default fact
+
+ from sigma_finite_pairs guess F :: "'i \<Rightarrow> nat \<Rightarrow> 'a set" ..
+ then have F: "\<And>j. j \<in> I \<Longrightarrow> range (F j) \<subseteq> sets (M j)"
+ "incseq (\<lambda>k. \<Pi>\<^isub>E j \<in> I. F j k)"
+ "(\<Union>k. \<Pi>\<^isub>E j \<in> I. F j k) = space (Pi\<^isub>M I M)"
+ "\<And>k. \<And>j. j \<in> I \<Longrightarrow> emeasure (M j) (F j k) \<noteq> \<infinity>"
by blast+
- let ?F = "\<lambda>k. \<Pi>\<^isub>E j \<in> insert i I. F j k"
+ let ?F = "\<lambda>k. \<Pi>\<^isub>E j \<in> I. F j k"
- case 1 show ?case
+ show ?thesis
proof (unfold_locales, intro exI[of _ ?F] conjI allI)
- show "range ?F \<subseteq> sets (Pi\<^isub>M (insert i I) M)" using F(1) insert(1,2) by auto
+ show "range ?F \<subseteq> sets (Pi\<^isub>M I M)" using F(1) `finite I` by auto
next
- from F(3) show "(\<Union>i. ?F i) = space (Pi\<^isub>M (insert i I) M)" by simp
+ from F(3) show "(\<Union>i. ?F i) = space (Pi\<^isub>M I M)" by simp
next
fix j
- from F `finite I` setprod_PInf[of "insert i I", OF emeasure_nonneg, of M]
- show "emeasure (\<Pi>\<^isub>M i\<in>insert i I. M i) (?F j) \<noteq> \<infinity>"
- by (subst product) auto
+ from F `finite I` setprod_PInf[of I, OF emeasure_nonneg, of M]
+ show "emeasure (\<Pi>\<^isub>M i\<in>I. M i) (?F j) \<noteq> \<infinity>"
+ by (subst emeasure_PiM) auto
qed
qed
@@ -786,7 +779,7 @@
using A by (intro emeasure_distr measurable_merge) (auto simp: sets_PiM)
also have "emeasure ?B ?X = (\<Prod>i\<in>I. emeasure (M i) (F i)) * (\<Prod>i\<in>J. emeasure (M i) (F i))"
using `finite J` `finite I` F X
- by (simp add: P.emeasure_pair_measure_Times I.measure_times J.measure_times Pi_iff)
+ by (simp add: J.emeasure_pair_measure_Times I.measure_times J.measure_times Pi_iff)
also have "\<dots> = (\<Prod>i\<in>I \<union> J. emeasure (M i) (F i))"
using `finite J` `finite I` `I \<inter> J = {}` by (simp add: setprod_Un_one)
also have "\<dots> = emeasure ?P (Pi\<^isub>E (I \<union> J) F)"
@@ -806,10 +799,10 @@
interpret J: finite_product_sigma_finite M J by default fact
interpret P: pair_sigma_finite "Pi\<^isub>M I M" "Pi\<^isub>M J M" by default
have P_borel: "(\<lambda>x. f (case x of (x, y) \<Rightarrow> merge I x J y)) \<in> borel_measurable (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M)"
- using measurable_comp[OF measurable_merge[OF IJ(1)] f] by (simp add: comp_def)
+ using measurable_comp[OF measurable_merge f] by (simp add: comp_def)
show ?thesis
apply (subst distr_merge[OF IJ, symmetric])
- apply (subst positive_integral_distr[OF measurable_merge f, OF IJ(1)])
+ apply (subst positive_integral_distr[OF measurable_merge f])
apply (subst P.positive_integral_fst_measurable(2)[symmetric, OF P_borel])
apply simp
done
@@ -914,17 +907,42 @@
from f have f_borel: "f \<in> borel_measurable (Pi\<^isub>M (I \<union> J) M)"
by auto
have P_borel: "(\<lambda>x. f (case x of (x, y) \<Rightarrow> merge I x J y)) \<in> borel_measurable (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M)"
- using measurable_comp[OF measurable_merge[OF IJ(1)] f_borel] by (simp add: comp_def)
+ using measurable_comp[OF measurable_merge f_borel] by (simp add: comp_def)
have f_int: "integrable (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M) ?f"
- by (rule integrable_distr[OF measurable_merge[OF IJ]]) (simp add: distr_merge[OF IJ fin] f)
+ by (rule integrable_distr[OF measurable_merge]) (simp add: distr_merge[OF IJ fin] f)
show ?thesis
apply (subst distr_merge[symmetric, OF IJ fin])
- apply (subst integral_distr[OF measurable_merge[OF IJ] f_borel])
+ apply (subst integral_distr[OF measurable_merge f_borel])
apply (subst P.integrable_fst_measurable(2)[symmetric, OF f_int])
apply simp
done
qed
+lemma (in product_sigma_finite)
+ assumes IJ: "I \<inter> J = {}" "finite I" "finite J" and A: "A \<in> sets (Pi\<^isub>M (I \<union> J) M)"
+ shows emeasure_fold_integral:
+ "emeasure (Pi\<^isub>M (I \<union> J) M) A = (\<integral>\<^isup>+x. emeasure (Pi\<^isub>M J M) (merge I x J -` A \<inter> space (Pi\<^isub>M J M)) \<partial>Pi\<^isub>M I M)" (is ?I)
+ and emeasure_fold_measurable:
+ "(\<lambda>x. emeasure (Pi\<^isub>M J M) (merge I x J -` A \<inter> space (Pi\<^isub>M J M))) \<in> borel_measurable (Pi\<^isub>M I M)" (is ?B)
+proof -
+ interpret I: finite_product_sigma_finite M I by default fact
+ interpret J: finite_product_sigma_finite M J by default fact
+ interpret IJ: pair_sigma_finite "Pi\<^isub>M I M" "Pi\<^isub>M J M" ..
+ have merge: "(\<lambda>(x, y). merge I x J y) -` A \<inter> space (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M) \<in> sets (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M)"
+ by (intro measurable_sets[OF _ A] measurable_merge assms)
+
+ show ?I
+ apply (subst distr_merge[symmetric, OF IJ])
+ apply (subst emeasure_distr[OF measurable_merge A])
+ apply (subst J.emeasure_pair_measure_alt[OF merge])
+ apply (auto intro!: positive_integral_cong arg_cong2[where f=emeasure] simp: space_pair_measure)
+ done
+
+ show ?B
+ using IJ.measurable_emeasure_Pair1[OF merge]
+ by (simp add: vimage_compose[symmetric] comp_def space_pair_measure cong: measurable_cong)
+qed
+
lemma (in product_sigma_finite) product_integral_insert:
assumes I: "finite I" "i \<notin> I"
and f: "integrable (Pi\<^isub>M (insert i I) M) f"
@@ -999,6 +1017,56 @@
by (simp add: * insert integral_multc integral_cmult[OF prod] subset_insertI)
qed
+lemma sets_Collect_single:
+ "i \<in> I \<Longrightarrow> A \<in> sets (M i) \<Longrightarrow> { x \<in> space (Pi\<^isub>M I M). x i \<in> A } \<in> sets (Pi\<^isub>M I M)"
+ unfolding sets_PiM_single
+ by (auto intro!: sigma_sets.Basic exI[of _ i] exI[of _ A]) (auto simp: space_PiM)
+
+lemma sigma_prod_algebra_sigma_eq_infinite:
+ fixes E :: "'i \<Rightarrow> 'a set set"
+ assumes S_mono: "\<And>i. i \<in> I \<Longrightarrow> incseq (S i)"
+ and S_union: "\<And>i. i \<in> I \<Longrightarrow> (\<Union>j. S i j) = space (M i)"
+ and S_in_E: "\<And>i. i \<in> I \<Longrightarrow> range (S i) \<subseteq> E i"
+ assumes E_closed: "\<And>i. i \<in> I \<Longrightarrow> E i \<subseteq> Pow (space (M i))"
+ and E_generates: "\<And>i. i \<in> I \<Longrightarrow> sets (M i) = sigma_sets (space (M i)) (E i)"
+ defines "P == {{f\<in>\<Pi>\<^isub>E i\<in>I. space (M i). f i \<in> A} | i A. i \<in> I \<and> A \<in> E i}"
+ shows "sets (PiM I M) = sigma_sets (space (PiM I M)) P"
+proof
+ let ?P = "sigma (space (Pi\<^isub>M I M)) P"
+ have P_closed: "P \<subseteq> Pow (space (Pi\<^isub>M I M))"
+ using E_closed by (auto simp: space_PiM P_def Pi_iff subset_eq)
+ then have space_P: "space ?P = (\<Pi>\<^isub>E i\<in>I. space (M i))"
+ by (simp add: space_PiM)
+ have "sets (PiM I M) =
+ sigma_sets (space ?P) {{f \<in> \<Pi>\<^isub>E i\<in>I. space (M i). f i \<in> A} |i A. i \<in> I \<and> A \<in> sets (M i)}"
+ using sets_PiM_single[of I M] by (simp add: space_P)
+ also have "\<dots> \<subseteq> sets (sigma (space (PiM I M)) P)"
+ proof (safe intro!: sigma_sets_subset)
+ fix i A assume "i \<in> I" and A: "A \<in> sets (M i)"
+ then have "(\<lambda>x. x i) \<in> measurable ?P (sigma (space (M i)) (E i))"
+ apply (subst measurable_iff_measure_of)
+ apply (simp_all add: P_closed)
+ using E_closed
+ apply (force simp: subset_eq space_PiM)
+ apply (force simp: subset_eq space_PiM)
+ apply (auto simp: P_def intro!: sigma_sets.Basic exI[of _ i])
+ apply (rule_tac x=Aa in exI)
+ apply (auto simp: space_PiM)
+ done
+ from measurable_sets[OF this, of A] A `i \<in> I` E_closed
+ have "(\<lambda>x. x i) -` A \<inter> space ?P \<in> sets ?P"
+ by (simp add: E_generates)
+ also have "(\<lambda>x. x i) -` A \<inter> space ?P = {f \<in> \<Pi>\<^isub>E i\<in>I. space (M i). f i \<in> A}"
+ using P_closed by (auto simp: space_PiM)
+ finally show "\<dots> \<in> sets ?P" .
+ qed
+ finally show "sets (PiM I M) \<subseteq> sigma_sets (space (PiM I M)) P"
+ by (simp add: P_closed)
+ show "sigma_sets (space (PiM I M)) P \<subseteq> sets (PiM I M)"
+ unfolding P_def space_PiM[symmetric]
+ by (intro sigma_sets_subset) (auto simp: E_generates sets_Collect_single)
+qed
+
lemma sigma_prod_algebra_sigma_eq:
fixes E :: "'i \<Rightarrow> 'a set set"
assumes "finite I"
--- a/src/HOL/Probability/Independent_Family.thy Wed Oct 10 12:12:17 2012 +0200
+++ b/src/HOL/Probability/Independent_Family.thy Wed Oct 10 12:12:18 2012 +0200
@@ -1035,7 +1035,7 @@
fix X assume "X \<in> ?E"
then obtain A B where X[simp]: "X = A \<times> B" and A: "A \<in> sets M1" and B: "B \<in> sets M2" by auto
then have "emeasure ?P X = emeasure M1 A * emeasure M2 B"
- by (simp add: emeasure_pair_measure_Times)
+ by (simp add: M2.emeasure_pair_measure_Times)
also have "\<dots> = emeasure M (A \<times> B)"
using A B emeasure by auto
finally show "emeasure ?P X = emeasure M X"
@@ -1143,7 +1143,7 @@
also have "\<dots> = emeasure (?S \<Otimes>\<^isub>M ?T) (A \<times> B)"
unfolding `?S \<Otimes>\<^isub>M ?T = ?J` ..
also have "\<dots> = emeasure ?S A * emeasure ?T B"
- using ab by (simp add: XY.emeasure_pair_measure_Times)
+ using ab by (simp add: Y.emeasure_pair_measure_Times)
finally show "prob ((X -` A \<inter> space M) \<inter> (Y -` B \<inter> space M)) =
prob (X -` A \<inter> space M) * prob (Y -` B \<inter> space M)"
using rvs ab by (simp add: emeasure_eq_measure emeasure_distr)
--- a/src/HOL/Probability/Infinite_Product_Measure.thy Wed Oct 10 12:12:17 2012 +0200
+++ b/src/HOL/Probability/Infinite_Product_Measure.thy Wed Oct 10 12:12:18 2012 +0200
@@ -8,31 +8,6 @@
imports Probability_Measure Caratheodory
begin
-lemma (in product_sigma_finite)
- assumes IJ: "I \<inter> J = {}" "finite I" "finite J" and A: "A \<in> sets (Pi\<^isub>M (I \<union> J) M)"
- shows emeasure_fold_integral:
- "emeasure (Pi\<^isub>M (I \<union> J) M) A = (\<integral>\<^isup>+x. emeasure (Pi\<^isub>M J M) (merge I x J -` A \<inter> space (Pi\<^isub>M J M)) \<partial>Pi\<^isub>M I M)" (is ?I)
- and emeasure_fold_measurable:
- "(\<lambda>x. emeasure (Pi\<^isub>M J M) (merge I x J -` A \<inter> space (Pi\<^isub>M J M))) \<in> borel_measurable (Pi\<^isub>M I M)" (is ?B)
-proof -
- interpret I: finite_product_sigma_finite M I by default fact
- interpret J: finite_product_sigma_finite M J by default fact
- interpret IJ: pair_sigma_finite "Pi\<^isub>M I M" "Pi\<^isub>M J M" ..
- have merge: "(\<lambda>(x, y). merge I x J y) -` A \<inter> space (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M) \<in> sets (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M)"
- by (intro measurable_sets[OF _ A] measurable_merge assms)
-
- show ?I
- apply (subst distr_merge[symmetric, OF IJ])
- apply (subst emeasure_distr[OF measurable_merge[OF IJ(1)] A])
- apply (subst IJ.emeasure_pair_measure_alt[OF merge])
- apply (auto intro!: positive_integral_cong arg_cong2[where f=emeasure] simp: space_pair_measure)
- done
-
- show ?B
- using IJ.measurable_emeasure_Pair1[OF merge]
- by (simp add: vimage_compose[symmetric] comp_def space_pair_measure cong: measurable_cong)
-qed
-
lemma restrict_extensional_sub[intro]: "A \<subseteq> B \<Longrightarrow> restrict f A \<in> extensional B"
unfolding restrict_def extensional_def by auto
--- a/src/HOL/Probability/Information.thy Wed Oct 10 12:12:17 2012 +0200
+++ b/src/HOL/Probability/Information.thy Wed Oct 10 12:12:18 2012 +0200
@@ -194,7 +194,7 @@
unfolding KL_divergence_def
proof (subst integral_density)
show "entropy_density b M (density M (\<lambda>x. ereal (f x))) \<in> borel_measurable M"
- using f `1 < b`
+ using f
by (auto simp: comp_def entropy_density_def intro!: borel_measurable_log borel_measurable_RN_deriv_density)
have "density M (RN_deriv M (density M f)) = density M f"
using f by (intro density_RN_deriv_density) auto
--- a/src/HOL/Probability/Probability_Measure.thy Wed Oct 10 12:12:17 2012 +0200
+++ b/src/HOL/Probability/Probability_Measure.thy Wed Oct 10 12:12:18 2012 +0200
@@ -407,7 +407,7 @@
sublocale pair_prob_space \<subseteq> P: prob_space "M1 \<Otimes>\<^isub>M M2"
proof
show "emeasure (M1 \<Otimes>\<^isub>M M2) (space (M1 \<Otimes>\<^isub>M M2)) = 1"
- by (simp add: emeasure_pair_measure_Times M1.emeasure_space_1 M2.emeasure_space_1 space_pair_measure)
+ by (simp add: M2.emeasure_pair_measure_Times M1.emeasure_space_1 M2.emeasure_space_1 space_pair_measure)
qed
locale product_prob_space = product_sigma_finite M for M :: "'i \<Rightarrow> 'a measure" +