--- a/src/HOL/Probability/Finite_Product_Measure.thy Mon Apr 23 12:23:23 2012 +0100
+++ b/src/HOL/Probability/Finite_Product_Measure.thy Mon Apr 23 12:14:35 2012 +0200
@@ -8,6 +8,9 @@
imports Binary_Product_Measure
begin
+lemma split_const: "(\<lambda>(i, j). c) = (\<lambda>_. c)"
+ by auto
+
lemma Pi_iff: "f \<in> Pi I X \<longleftrightarrow> (\<forall>i\<in>I. f i \<in> X i)"
unfolding Pi_def by auto
@@ -34,9 +37,6 @@
notation (xsymbols)
funcset_extensional (infixr "\<rightarrow>\<^isub>E" 60)
-lemma extensional_empty[simp]: "extensional {} = {\<lambda>x. undefined}"
- by safe (auto simp add: extensional_def fun_eq_iff)
-
lemma extensional_insert[intro, simp]:
assumes "a \<in> extensional (insert i I)"
shows "a(i := b) \<in> extensional (insert i I)"
@@ -86,7 +86,7 @@
"I \<inter> J = {} \<Longrightarrow> restrict (merge I x J y) J = restrict y J"
"J \<inter> I = {} \<Longrightarrow> restrict (merge I x J y) I = restrict x I"
"J \<inter> I = {} \<Longrightarrow> restrict (merge I x J y) J = restrict y J"
- by (auto simp: restrict_def intro!: ext)
+ by (auto simp: restrict_def)
lemma extensional_insert_undefined[intro, simp]:
assumes "a \<in> extensional (insert i I)"
@@ -130,16 +130,16 @@
using assms by (auto simp: restrict_Pi_cancel)
lemma restrict_fupd[simp]: "i \<notin> I \<Longrightarrow> restrict (f (i := x)) I = restrict f I"
- by (auto simp: restrict_def intro!: ext)
+ by (auto simp: restrict_def)
lemma merge_restrict[simp]:
"merge I (restrict x I) J y = merge I x J y"
"merge I x J (restrict y J) = merge I x J y"
- unfolding merge_def by (auto intro!: ext)
+ unfolding merge_def by auto
lemma merge_x_x_eq_restrict[simp]:
"merge I x J x = restrict x (I \<union> J)"
- unfolding merge_def by (auto intro!: ext)
+ unfolding merge_def by auto
lemma Pi_fupd_iff: "i \<in> I \<Longrightarrow> f \<in> Pi I (B(i := A)) \<longleftrightarrow> f \<in> Pi (I - {i}) B \<and> f i \<in> A"
apply auto
@@ -233,339 +233,355 @@
section "Products"
-locale product_sigma_algebra =
- fixes M :: "'i \<Rightarrow> ('a, 'b) measure_space_scheme"
- assumes sigma_algebras: "\<And>i. sigma_algebra (M i)"
+definition prod_emb where
+ "prod_emb I M K X = (\<lambda>x. restrict x K) -` X \<inter> (PIE i:I. space (M i))"
+
+lemma prod_emb_iff:
+ "f \<in> prod_emb I M K X \<longleftrightarrow> f \<in> extensional I \<and> (restrict f K \<in> X) \<and> (\<forall>i\<in>I. f i \<in> space (M i))"
+ unfolding prod_emb_def by auto
-locale finite_product_sigma_algebra = product_sigma_algebra M
- for M :: "'i \<Rightarrow> ('a, 'b) measure_space_scheme" +
- fixes I :: "'i set"
- assumes finite_index[simp, intro]: "finite I"
+lemma
+ shows prod_emb_empty[simp]: "prod_emb M L K {} = {}"
+ and prod_emb_Un[simp]: "prod_emb M L K (A \<union> B) = prod_emb M L K A \<union> prod_emb M L K B"
+ and prod_emb_Int: "prod_emb M L K (A \<inter> B) = prod_emb M L K A \<inter> prod_emb M L K B"
+ and prod_emb_UN[simp]: "prod_emb M L K (\<Union>i\<in>I. F i) = (\<Union>i\<in>I. prod_emb M L K (F i))"
+ and prod_emb_INT[simp]: "I \<noteq> {} \<Longrightarrow> prod_emb M L K (\<Inter>i\<in>I. F i) = (\<Inter>i\<in>I. prod_emb M L K (F i))"
+ and prod_emb_Diff[simp]: "prod_emb M L K (A - B) = prod_emb M L K A - prod_emb M L K B"
+ by (auto simp: prod_emb_def)
-definition
- "product_algebra_generator I M = \<lparr> space = (\<Pi>\<^isub>E i \<in> I. space (M i)),
- sets = Pi\<^isub>E I ` (\<Pi> i \<in> I. sets (M i)),
- measure = \<lambda>A. (\<Prod>i\<in>I. measure (M i) ((SOME F. A = Pi\<^isub>E I F) i)) \<rparr>"
+lemma prod_emb_PiE: "J \<subseteq> I \<Longrightarrow> (\<And>i. i \<in> J \<Longrightarrow> E i \<subseteq> space (M i)) \<Longrightarrow>
+ prod_emb I M J (\<Pi>\<^isub>E i\<in>J. E i) = (\<Pi>\<^isub>E i\<in>I. if i \<in> J then E i else space (M i))"
+ by (force simp: prod_emb_def Pi_iff split_if_mem2)
+
+lemma prod_emb_PiE_same_index[simp]: "(\<And>i. i \<in> I \<Longrightarrow> E i \<subseteq> space (M i)) \<Longrightarrow> prod_emb I M I (Pi\<^isub>E I E) = Pi\<^isub>E I E"
+ by (auto simp: prod_emb_def Pi_iff)
-definition product_algebra_def:
- "Pi\<^isub>M I M = sigma (product_algebra_generator I M)
- \<lparr> measure := (SOME \<mu>. sigma_finite_measure (sigma (product_algebra_generator I M) \<lparr> measure := \<mu> \<rparr>) \<and>
- (\<forall>A\<in>\<Pi> i\<in>I. sets (M i). \<mu> (Pi\<^isub>E I A) = (\<Prod>i\<in>I. measure (M i) (A i))))\<rparr>"
+definition PiM :: "'i set \<Rightarrow> ('i \<Rightarrow> 'a measure) \<Rightarrow> ('i \<Rightarrow> 'a) measure" where
+ "PiM I M = extend_measure (\<Pi>\<^isub>E i\<in>I. space (M i))
+ {(J, X). (J \<noteq> {} \<or> I = {}) \<and> finite J \<and> J \<subseteq> I \<and> X \<in> (\<Pi> j\<in>J. sets (M j))}
+ (\<lambda>(J, X). prod_emb I M J (\<Pi>\<^isub>E j\<in>J. X j))
+ (\<lambda>(J, X). \<Prod>j\<in>J \<union> {i\<in>I. emeasure (M i) (space (M i)) \<noteq> 1}. if j \<in> J then emeasure (M j) (X j) else emeasure (M j) (space (M j)))"
+
+definition prod_algebra :: "'i set \<Rightarrow> ('i \<Rightarrow> 'a measure) \<Rightarrow> ('i \<Rightarrow> 'a) set set" where
+ "prod_algebra I M = (\<lambda>(J, X). prod_emb I M J (\<Pi>\<^isub>E j\<in>J. X j)) `
+ {(J, X). (J \<noteq> {} \<or> I = {}) \<and> finite J \<and> J \<subseteq> I \<and> X \<in> (\<Pi> j\<in>J. sets (M j))}"
+
+abbreviation
+ "Pi\<^isub>M I M \<equiv> PiM I M"
syntax
- "_PiM" :: "[pttrn, 'i set, ('a, 'b) measure_space_scheme] =>
- ('i => 'a, 'b) measure_space_scheme" ("(3PIM _:_./ _)" 10)
+ "_PiM" :: "pttrn \<Rightarrow> 'i set \<Rightarrow> 'a measure \<Rightarrow> ('i => 'a) measure" ("(3PIM _:_./ _)" 10)
syntax (xsymbols)
- "_PiM" :: "[pttrn, 'i set, ('a, 'b) measure_space_scheme] =>
- ('i => 'a, 'b) measure_space_scheme" ("(3\<Pi>\<^isub>M _\<in>_./ _)" 10)
+ "_PiM" :: "pttrn \<Rightarrow> 'i set \<Rightarrow> 'a measure \<Rightarrow> ('i => 'a) measure" ("(3\<Pi>\<^isub>M _\<in>_./ _)" 10)
syntax (HTML output)
- "_PiM" :: "[pttrn, 'i set, ('a, 'b) measure_space_scheme] =>
- ('i => 'a, 'b) measure_space_scheme" ("(3\<Pi>\<^isub>M _\<in>_./ _)" 10)
+ "_PiM" :: "pttrn \<Rightarrow> 'i set \<Rightarrow> 'a measure \<Rightarrow> ('i => 'a) measure" ("(3\<Pi>\<^isub>M _\<in>_./ _)" 10)
translations
- "PIM x:I. M" == "CONST Pi\<^isub>M I (%x. M)"
-
-abbreviation (in finite_product_sigma_algebra) "G \<equiv> product_algebra_generator I M"
-abbreviation (in finite_product_sigma_algebra) "P \<equiv> Pi\<^isub>M I M"
-
-sublocale product_sigma_algebra \<subseteq> M: sigma_algebra "M i" for i by (rule sigma_algebras)
-
-lemma sigma_into_space:
- assumes "sets M \<subseteq> Pow (space M)"
- shows "sets (sigma M) \<subseteq> Pow (space M)"
- using sigma_sets_into_sp[OF assms] unfolding sigma_def by auto
+ "PIM x:I. M" == "CONST PiM I (%x. M)"
-lemma (in product_sigma_algebra) product_algebra_generator_into_space:
- "sets (product_algebra_generator I M) \<subseteq> Pow (space (product_algebra_generator I M))"
- using M.sets_into_space unfolding product_algebra_generator_def
- by auto blast
-
-lemma (in product_sigma_algebra) product_algebra_into_space:
- "sets (Pi\<^isub>M I M) \<subseteq> Pow (space (Pi\<^isub>M I M))"
- using product_algebra_generator_into_space
- by (auto intro!: sigma_into_space simp add: product_algebra_def)
-
-lemma (in product_sigma_algebra) sigma_algebra_product_algebra: "sigma_algebra (Pi\<^isub>M I M)"
- using product_algebra_generator_into_space unfolding product_algebra_def
- by (rule sigma_algebra.sigma_algebra_cong[OF sigma_algebra_sigma]) simp_all
-
-sublocale finite_product_sigma_algebra \<subseteq> sigma_algebra P
- using sigma_algebra_product_algebra .
+lemma prod_algebra_sets_into_space:
+ "prod_algebra I M \<subseteq> Pow (\<Pi>\<^isub>E i\<in>I. space (M i))"
+ using assms by (auto simp: prod_emb_def prod_algebra_def)
-lemma product_algebraE:
- assumes "A \<in> sets (product_algebra_generator I M)"
- obtains E where "A = Pi\<^isub>E I E" "E \<in> (\<Pi> i\<in>I. sets (M i))"
- using assms unfolding product_algebra_generator_def by auto
-
-lemma product_algebra_generatorI[intro]:
- assumes "E \<in> (\<Pi> i\<in>I. sets (M i))"
- shows "Pi\<^isub>E I E \<in> sets (product_algebra_generator I M)"
- using assms unfolding product_algebra_generator_def by auto
-
-lemma space_product_algebra_generator[simp]:
- "space (product_algebra_generator I M) = Pi\<^isub>E I (\<lambda>i. space (M i))"
- unfolding product_algebra_generator_def by simp
+lemma prod_algebra_eq_finite:
+ assumes I: "finite I"
+ shows "prod_algebra I M = {(\<Pi>\<^isub>E i\<in>I. X i) |X. X \<in> (\<Pi> j\<in>I. sets (M j))}" (is "?L = ?R")
+proof (intro iffI set_eqI)
+ fix A assume "A \<in> ?L"
+ then obtain J E where J: "J \<noteq> {} \<or> I = {}" "finite J" "J \<subseteq> I" "\<forall>i\<in>J. E i \<in> sets (M i)"
+ and A: "A = prod_emb I M J (PIE j:J. E j)"
+ by (auto simp: prod_algebra_def)
+ let ?A = "\<Pi>\<^isub>E i\<in>I. if i \<in> J then E i else space (M i)"
+ have A: "A = ?A"
+ unfolding A using J by (intro prod_emb_PiE sets_into_space) auto
+ show "A \<in> ?R" unfolding A using J top
+ by (intro CollectI exI[of _ "\<lambda>i. if i \<in> J then E i else space (M i)"]) simp
+next
+ fix A assume "A \<in> ?R"
+ then obtain X where "A = (\<Pi>\<^isub>E i\<in>I. X i)" and X: "X \<in> (\<Pi> j\<in>I. sets (M j))" by auto
+ then have A: "A = prod_emb I M I (\<Pi>\<^isub>E i\<in>I. X i)"
+ using sets_into_space by (force simp: prod_emb_def Pi_iff)
+ from X I show "A \<in> ?L" unfolding A
+ by (auto simp: prod_algebra_def)
+qed
-lemma space_product_algebra[simp]:
- "space (Pi\<^isub>M I M) = (\<Pi>\<^isub>E i\<in>I. space (M i))"
- unfolding product_algebra_def product_algebra_generator_def by simp
-
-lemma sets_product_algebra:
- "sets (Pi\<^isub>M I M) = sets (sigma (product_algebra_generator I M))"
- unfolding product_algebra_def sigma_def by simp
+lemma prod_algebraI:
+ "finite J \<Longrightarrow> (J \<noteq> {} \<or> I = {}) \<Longrightarrow> J \<subseteq> I \<Longrightarrow> (\<And>i. i \<in> J \<Longrightarrow> E i \<in> sets (M i))
+ \<Longrightarrow> prod_emb I M J (PIE j:J. E j) \<in> prod_algebra I M"
+ by (auto simp: prod_algebra_def Pi_iff)
-lemma product_algebra_generator_sets_into_space:
- assumes "\<And>i. i\<in>I \<Longrightarrow> sets (M i) \<subseteq> Pow (space (M i))"
- shows "sets (product_algebra_generator I M) \<subseteq> Pow (space (product_algebra_generator I M))"
- using assms by (auto simp: product_algebra_generator_def) blast
-
-lemma (in finite_product_sigma_algebra) in_P[simp, intro]:
- "\<lbrakk> \<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (M i) \<rbrakk> \<Longrightarrow> Pi\<^isub>E I A \<in> sets P"
- by (auto simp: sets_product_algebra)
-
-lemma Int_stable_product_algebra_generator:
- "(\<And>i. i \<in> I \<Longrightarrow> Int_stable (M i)) \<Longrightarrow> Int_stable (product_algebra_generator I M)"
- by (auto simp add: product_algebra_generator_def Int_stable_def PiE_Int Pi_iff)
+lemma prod_algebraE:
+ assumes A: "A \<in> prod_algebra I M"
+ obtains J E where "A = prod_emb I M J (PIE j:J. E j)"
+ "finite J" "J \<noteq> {} \<or> I = {}" "J \<subseteq> I" "\<And>i. i \<in> J \<Longrightarrow> E i \<in> sets (M i)"
+ using A by (auto simp: prod_algebra_def)
-section "Generating set generates also product algebra"
+lemma prod_algebraE_all:
+ assumes A: "A \<in> prod_algebra I M"
+ obtains E where "A = Pi\<^isub>E I E" "E \<in> (\<Pi> i\<in>I. sets (M i))"
+proof -
+ from A obtain E J where A: "A = prod_emb I M J (Pi\<^isub>E J E)"
+ and J: "J \<subseteq> I" and E: "E \<in> (\<Pi> i\<in>J. sets (M i))"
+ by (auto simp: prod_algebra_def)
+ from E have "\<And>i. i \<in> J \<Longrightarrow> E i \<subseteq> space (M i)"
+ using sets_into_space by auto
+ then have "A = (\<Pi>\<^isub>E i\<in>I. if i\<in>J then E i else space (M i))"
+ using A J by (auto simp: prod_emb_PiE)
+ moreover then have "(\<lambda>i. if i\<in>J then E i else space (M i)) \<in> (\<Pi> i\<in>I. sets (M i))"
+ using top E by auto
+ ultimately show ?thesis using that by auto
+qed
-lemma sigma_product_algebra_sigma_eq:
- assumes "finite I"
- assumes mono: "\<And>i. i \<in> I \<Longrightarrow> incseq (S i)"
- assumes union: "\<And>i. i \<in> I \<Longrightarrow> (\<Union>j. S i j) = space (E i)"
- assumes sets_into: "\<And>i. i \<in> I \<Longrightarrow> range (S i) \<subseteq> sets (E i)"
- and E: "\<And>i. sets (E i) \<subseteq> Pow (space (E i))"
- shows "sets (\<Pi>\<^isub>M i\<in>I. sigma (E i)) = sets (\<Pi>\<^isub>M i\<in>I. E i)"
- (is "sets ?S = sets ?E")
-proof cases
- assume "I = {}" then show ?thesis
- by (simp add: product_algebra_def product_algebra_generator_def)
-next
- assume "I \<noteq> {}"
- interpret E: sigma_algebra "sigma (E i)" for i
- using E by (rule sigma_algebra_sigma)
- have into_space[intro]: "\<And>i x A. A \<in> sets (E i) \<Longrightarrow> x i \<in> A \<Longrightarrow> x i \<in> space (E i)"
- using E by auto
- interpret G: sigma_algebra ?E
- unfolding product_algebra_def product_algebra_generator_def using E
- by (intro sigma_algebra.sigma_algebra_cong[OF sigma_algebra_sigma]) (auto dest: Pi_mem)
- { fix A i assume "i \<in> I" and A: "A \<in> sets (E i)"
- then have "(\<lambda>x. x i) -` A \<inter> space ?E = (\<Pi>\<^isub>E j\<in>I. if j = i then A else \<Union>n. S j n) \<inter> space ?E"
- using mono union unfolding incseq_Suc_iff space_product_algebra
- by (auto dest: Pi_mem)
- also have "\<dots> = (\<Union>n. (\<Pi>\<^isub>E j\<in>I. if j = i then A else S j n))"
- unfolding space_product_algebra
- apply simp
- apply (subst Pi_UN[OF `finite I`])
- using mono[THEN incseqD] apply simp
- apply (simp add: PiE_Int)
- apply (intro PiE_cong)
- using A sets_into by (auto intro!: into_space)
- also have "\<dots> \<in> sets ?E"
- using sets_into `A \<in> sets (E i)`
- unfolding sets_product_algebra sets_sigma
- by (intro sigma_sets.Union)
- (auto simp: image_subset_iff intro!: sigma_sets.Basic)
- finally have "(\<lambda>x. x i) -` A \<inter> space ?E \<in> sets ?E" . }
- then have proj:
- "\<And>i. i\<in>I \<Longrightarrow> (\<lambda>x. x i) \<in> measurable ?E (sigma (E i))"
- using E by (subst G.measurable_iff_sigma)
- (auto simp: sets_product_algebra sets_sigma)
- { fix A assume A: "\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (sigma (E i))"
- with proj have basic: "\<And>i. i \<in> I \<Longrightarrow> (\<lambda>x. x i) -` (A i) \<inter> space ?E \<in> sets ?E"
- unfolding measurable_def by simp
- have "Pi\<^isub>E I A = (\<Inter>i\<in>I. (\<lambda>x. x i) -` (A i) \<inter> space ?E)"
- using A E.sets_into_space `I \<noteq> {}` unfolding product_algebra_def by auto blast
- then have "Pi\<^isub>E I A \<in> sets ?E"
- using G.finite_INT[OF `finite I` `I \<noteq> {}` basic, of "\<lambda>i. i"] by simp }
- then have "sigma_sets (space ?E) (sets (product_algebra_generator I (\<lambda>i. sigma (E i)))) \<subseteq> sets ?E"
- by (intro G.sigma_sets_subset) (auto simp add: product_algebra_generator_def)
- then have subset: "sets ?S \<subseteq> sets ?E"
- by (simp add: sets_sigma sets_product_algebra)
- show "sets ?S = sets ?E"
- proof (intro set_eqI iffI)
- fix A assume "A \<in> sets ?E" then show "A \<in> sets ?S"
- unfolding sets_sigma sets_product_algebra
- proof induct
- case (Basic A) then show ?case
- by (auto simp: sets_sigma product_algebra_generator_def intro: sigma_sets.Basic)
- qed (auto intro: sigma_sets.intros simp: product_algebra_generator_def)
- next
- fix A assume "A \<in> sets ?S" then show "A \<in> sets ?E" using subset by auto
- qed
+lemma Int_stable_prod_algebra: "Int_stable (prod_algebra I M)"
+proof (unfold Int_stable_def, safe)
+ fix A assume "A \<in> prod_algebra I M"
+ from prod_algebraE[OF this] guess J E . note A = this
+ fix B assume "B \<in> prod_algebra I M"
+ from prod_algebraE[OF this] guess K F . note B = this
+ have "A \<inter> B = prod_emb I M (J \<union> K) (\<Pi>\<^isub>E i\<in>J \<union> K. (if i \<in> J then E i else space (M i)) \<inter>
+ (if i \<in> K then F i else space (M i)))"
+ unfolding A B using A(2,3,4) A(5)[THEN sets_into_space] B(2,3,4) B(5)[THEN sets_into_space]
+ apply (subst (1 2 3) prod_emb_PiE)
+ apply (simp_all add: subset_eq PiE_Int)
+ apply blast
+ apply (intro PiE_cong)
+ apply auto
+ done
+ also have "\<dots> \<in> prod_algebra I M"
+ using A B by (auto intro!: prod_algebraI)
+ finally show "A \<inter> B \<in> prod_algebra I M" .
+qed
+
+lemma prod_algebra_mono:
+ assumes space: "\<And>i. i \<in> I \<Longrightarrow> space (E i) = space (F i)"
+ assumes sets: "\<And>i. i \<in> I \<Longrightarrow> sets (E i) \<subseteq> sets (F i)"
+ shows "prod_algebra I E \<subseteq> prod_algebra I F"
+proof
+ fix A assume "A \<in> prod_algebra I E"
+ then obtain J G where J: "J \<noteq> {} \<or> I = {}" "finite J" "J \<subseteq> I"
+ and A: "A = prod_emb I E J (\<Pi>\<^isub>E i\<in>J. G i)"
+ and G: "\<And>i. i \<in> J \<Longrightarrow> G i \<in> sets (E i)"
+ by (auto simp: prod_algebra_def)
+ moreover
+ from space have "(\<Pi>\<^isub>E i\<in>I. space (E i)) = (\<Pi>\<^isub>E i\<in>I. space (F i))"
+ by (rule PiE_cong)
+ with A have "A = prod_emb I F J (\<Pi>\<^isub>E i\<in>J. G i)"
+ by (simp add: prod_emb_def)
+ moreover
+ from sets G J have "\<And>i. i \<in> J \<Longrightarrow> G i \<in> sets (F i)"
+ by auto
+ ultimately show "A \<in> prod_algebra I F"
+ apply (simp add: prod_algebra_def image_iff)
+ apply (intro exI[of _ J] exI[of _ G] conjI)
+ apply auto
+ done
qed
-lemma product_algebraI[intro]:
- "E \<in> (\<Pi> i\<in>I. sets (M i)) \<Longrightarrow> Pi\<^isub>E I E \<in> sets (Pi\<^isub>M I M)"
- using assms unfolding product_algebra_def by (auto intro: product_algebra_generatorI)
+lemma space_PiM: "space (\<Pi>\<^isub>M i\<in>I. M i) = (\<Pi>\<^isub>E i\<in>I. space (M i))"
+ using prod_algebra_sets_into_space unfolding PiM_def prod_algebra_def by (intro space_extend_measure) simp
+
+lemma sets_PiM: "sets (\<Pi>\<^isub>M i\<in>I. M i) = sigma_sets (\<Pi>\<^isub>E i\<in>I. space (M i)) (prod_algebra I M)"
+ using prod_algebra_sets_into_space unfolding PiM_def prod_algebra_def by (intro sets_extend_measure) simp
-lemma (in product_sigma_algebra) measurable_component_update:
- assumes "x \<in> space (Pi\<^isub>M I M)" and "i \<notin> I"
- shows "(\<lambda>v. x(i := v)) \<in> measurable (M i) (Pi\<^isub>M (insert i I) M)" (is "?f \<in> _")
- unfolding product_algebra_def apply simp
-proof (intro measurable_sigma)
- let ?G = "product_algebra_generator (insert i I) M"
- show "sets ?G \<subseteq> Pow (space ?G)" using product_algebra_generator_into_space .
- show "?f \<in> space (M i) \<rightarrow> space ?G"
- using M.sets_into_space assms by auto
- fix A assume "A \<in> sets ?G"
- from product_algebraE[OF this] guess E . note E = this
- then have "?f -` A \<inter> space (M i) = E i \<or> ?f -` A \<inter> space (M i) = {}"
- using M.sets_into_space assms by auto
- then show "?f -` A \<inter> space (M i) \<in> sets (M i)"
- using E by (auto intro!: product_algebraI)
+lemma sets_PiM_single: "sets (PiM I M) =
+ sigma_sets (\<Pi>\<^isub>E i\<in>I. space (M i)) {{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)}"
+ (is "_ = sigma_sets ?\<Omega> ?R")
+ unfolding sets_PiM
+proof (rule sigma_sets_eqI)
+ interpret R: sigma_algebra ?\<Omega> "sigma_sets ?\<Omega> ?R" by (rule sigma_algebra_sigma_sets) auto
+ fix A assume "A \<in> prod_algebra I M"
+ from prod_algebraE[OF this] guess J X . note X = this
+ show "A \<in> sigma_sets ?\<Omega> ?R"
+ proof cases
+ assume "I = {}"
+ with X have "A = {\<lambda>x. undefined}" by (auto simp: prod_emb_def)
+ with `I = {}` show ?thesis by (auto intro!: sigma_sets_top)
+ next
+ assume "I \<noteq> {}"
+ with X have "A = (\<Inter>j\<in>J. {f\<in>(\<Pi>\<^isub>E i\<in>I. space (M i)). f j \<in> X j})"
+ using sets_into_space[OF X(5)]
+ by (auto simp: prod_emb_PiE[OF _ sets_into_space] Pi_iff split: split_if_asm) blast
+ also have "\<dots> \<in> sigma_sets ?\<Omega> ?R"
+ using X `I \<noteq> {}` by (intro R.finite_INT sigma_sets.Basic) auto
+ finally show "A \<in> sigma_sets ?\<Omega> ?R" .
+ qed
+next
+ fix A assume "A \<in> ?R"
+ then obtain i B where A: "A = {f\<in>\<Pi>\<^isub>E i\<in>I. space (M i). f i \<in> B}" "i \<in> I" "B \<in> sets (M i)"
+ by auto
+ then have "A = prod_emb I M {i} (\<Pi>\<^isub>E i\<in>{i}. B)"
+ using sets_into_space[OF A(3)]
+ apply (subst prod_emb_PiE)
+ apply (auto simp: Pi_iff split: split_if_asm)
+ apply blast
+ done
+ also have "\<dots> \<in> sigma_sets ?\<Omega> (prod_algebra I M)"
+ using A by (intro sigma_sets.Basic prod_algebraI) auto
+ finally show "A \<in> sigma_sets ?\<Omega> (prod_algebra I M)" .
+qed
+
+lemma sets_PiM_I:
+ assumes "finite J" "J \<subseteq> I" "\<forall>i\<in>J. E i \<in> sets (M i)"
+ shows "prod_emb I M J (PIE j:J. E j) \<in> sets (PIM i:I. M i)"
+proof cases
+ assume "J = {}"
+ then have "prod_emb I M J (PIE j:J. E j) = (PIE j:I. space (M j))"
+ by (auto simp: prod_emb_def)
+ then show ?thesis
+ by (auto simp add: sets_PiM intro!: sigma_sets_top)
+next
+ assume "J \<noteq> {}" with assms show ?thesis
+ by (auto simp add: sets_PiM prod_algebra_def intro!: sigma_sets.Basic)
qed
-lemma (in product_sigma_algebra) 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)"
-proof -
- let ?f = "(\<lambda>(f, y). f(i := y))" and ?G = "product_algebra_generator (insert i I) M"
- interpret Ii: pair_sigma_algebra "Pi\<^isub>M I M" "M i"
- unfolding pair_sigma_algebra_def
- by (intro sigma_algebra_product_algebra sigma_algebras conjI)
- have "?f \<in> measurable Ii.P (sigma ?G)"
- proof (rule Ii.measurable_sigma)
- show "sets ?G \<subseteq> Pow (space ?G)"
- using product_algebra_generator_into_space .
- show "?f \<in> space (Pi\<^isub>M I M \<Otimes>\<^isub>M M i) \<rightarrow> space ?G"
- by (auto simp: space_pair_measure)
- next
- fix A assume "A \<in> sets ?G"
- then obtain F where "A = Pi\<^isub>E (insert i I) F"
- and F: "\<And>j. j \<in> I \<Longrightarrow> F j \<in> sets (M j)" "F i \<in> sets (M i)"
- by (auto elim!: product_algebraE)
- then have "?f -` A \<inter> space (Pi\<^isub>M I M \<Otimes>\<^isub>M M i) = Pi\<^isub>E I F \<times> (F i)"
- using sets_into_space `i \<notin> I`
- by (auto simp add: space_pair_measure) blast+
- then show "?f -` A \<inter> space (Pi\<^isub>M I M \<Otimes>\<^isub>M M i) \<in> sets (Pi\<^isub>M I M \<Otimes>\<^isub>M M i)"
- using F by (auto intro!: pair_measureI)
- qed
- then show ?thesis
- by (simp add: product_algebra_def)
+lemma measurable_PiM:
+ assumes space: "f \<in> space N \<rightarrow> (\<Pi>\<^isub>E i\<in>I. space (M i))"
+ assumes sets: "\<And>X J. J \<noteq> {} \<or> I = {} \<Longrightarrow> finite J \<Longrightarrow> J \<subseteq> I \<Longrightarrow> (\<And>i. i \<in> J \<Longrightarrow> X i \<in> sets (M i)) \<Longrightarrow>
+ f -` prod_emb I M J (Pi\<^isub>E J X) \<inter> space N \<in> sets N"
+ shows "f \<in> measurable N (PiM I M)"
+ using sets_PiM prod_algebra_sets_into_space space
+proof (rule measurable_sigma_sets)
+ fix A assume "A \<in> prod_algebra I M"
+ from prod_algebraE[OF this] guess J X .
+ with sets[of J X] show "f -` A \<inter> space N \<in> sets N" by auto
+qed
+
+lemma measurable_PiM_Collect:
+ assumes space: "f \<in> space N \<rightarrow> (\<Pi>\<^isub>E i\<in>I. space (M i))"
+ assumes sets: "\<And>X J. J \<noteq> {} \<or> I = {} \<Longrightarrow> finite J \<Longrightarrow> J \<subseteq> I \<Longrightarrow> (\<And>i. i \<in> J \<Longrightarrow> X i \<in> sets (M i)) \<Longrightarrow>
+ {\<omega>\<in>space N. \<forall>i\<in>J. f \<omega> i \<in> X i} \<in> sets N"
+ shows "f \<in> measurable N (PiM I M)"
+ using sets_PiM prod_algebra_sets_into_space space
+proof (rule measurable_sigma_sets)
+ fix A assume "A \<in> prod_algebra I M"
+ from prod_algebraE[OF this] guess J X . note X = this
+ have "f -` A \<inter> space N = {\<omega> \<in> space N. \<forall>i\<in>J. f \<omega> i \<in> X i}"
+ using sets_into_space[OF X(5)] X(2-) space unfolding X(1)
+ by (subst prod_emb_PiE) (auto simp: Pi_iff split: split_if_asm)
+ also have "\<dots> \<in> sets N" using X(3,2,4,5) by (rule sets)
+ finally show "f -` A \<inter> space N \<in> sets N" .
qed
-lemma (in product_sigma_algebra) measurable_merge:
- assumes [simp]: "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)"
-proof -
- let ?I = "Pi\<^isub>M I M" and ?J = "Pi\<^isub>M J M"
- interpret P: sigma_algebra "?I \<Otimes>\<^isub>M ?J"
- by (intro sigma_algebra_pair_measure product_algebra_into_space)
- let ?f = "\<lambda>(x, y). merge I x J y"
- let ?G = "product_algebra_generator (I \<union> J) M"
- have "?f \<in> measurable (?I \<Otimes>\<^isub>M ?J) (sigma ?G)"
- proof (rule P.measurable_sigma)
- fix A assume "A \<in> sets ?G"
- from product_algebraE[OF this]
- obtain E where E: "A = Pi\<^isub>E (I \<union> J) E" "E \<in> (\<Pi> i\<in>I \<union> J. sets (M i))" .
- then have *: "?f -` A \<inter> space (?I \<Otimes>\<^isub>M ?J) = Pi\<^isub>E I E \<times> Pi\<^isub>E J E"
- using sets_into_space `I \<inter> J = {}`
- by (auto simp add: space_pair_measure) fast+
- then show "?f -` A \<inter> space (?I \<Otimes>\<^isub>M ?J) \<in> sets (?I \<Otimes>\<^isub>M ?J)"
- using E unfolding * by (auto intro!: pair_measureI in_sigma product_algebra_generatorI
- simp: product_algebra_def)
- qed (insert product_algebra_generator_into_space, auto simp: space_pair_measure)
- then show "?f \<in> measurable (?I \<Otimes>\<^isub>M ?J) (Pi\<^isub>M (I \<union> J) M)"
- unfolding product_algebra_def[of "I \<union> J"] by simp
-qed
+lemma measurable_PiM_single:
+ assumes space: "f \<in> space N \<rightarrow> (\<Pi>\<^isub>E i\<in>I. space (M i))"
+ assumes sets: "\<And>A i. i \<in> I \<Longrightarrow> A \<in> sets (M i) \<Longrightarrow> {\<omega> \<in> space N. f \<omega> i \<in> A} \<in> sets N"
+ shows "f \<in> measurable N (PiM I M)"
+ using sets_PiM_single
+proof (rule measurable_sigma_sets)
+ fix A assume "A \<in> {{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)}"
+ then obtain B i where "A = {f \<in> \<Pi>\<^isub>E i\<in>I. space (M i). f i \<in> B}" and B: "i \<in> I" "B \<in> sets (M i)"
+ by auto
+ with space have "f -` A \<inter> space N = {\<omega> \<in> space N. f \<omega> i \<in> B}" by auto
+ also have "\<dots> \<in> sets N" using B by (rule sets)
+ finally show "f -` A \<inter> space N \<in> sets N" .
+qed (auto simp: space)
-lemma (in product_sigma_algebra) measurable_component_singleton:
+lemma sets_PiM_I_finite[simp, intro]:
+ assumes "finite I" and sets: "(\<And>i. i \<in> I \<Longrightarrow> E i \<in> sets (M i))"
+ shows "(PIE j:I. E j) \<in> sets (PIM i:I. M i)"
+ using sets_PiM_I[of I I E M] sets_into_space[OF sets] `finite I` sets by auto
+
+lemma measurable_component_update:
+ assumes "x \<in> space (Pi\<^isub>M I M)" and "i \<notin> I"
+ shows "(\<lambda>v. x(i := v)) \<in> measurable (M i) (Pi\<^isub>M (insert i I) M)" (is "?f \<in> _")
+proof (intro measurable_PiM_single)
+ fix j A assume "j \<in> insert i I" "A \<in> sets (M j)"
+ moreover have "{\<omega> \<in> space (M i). (x(i := \<omega>)) j \<in> A} =
+ (if i = j then space (M i) \<inter> A else if x j \<in> A then space (M i) else {})"
+ by auto
+ ultimately show "{\<omega> \<in> space (M i). (x(i := \<omega>)) j \<in> A} \<in> sets (M i)"
+ by auto
+qed (insert sets_into_space assms, auto simp: space_PiM)
+
+lemma measurable_component_singleton:
assumes "i \<in> I" shows "(\<lambda>x. x i) \<in> measurable (Pi\<^isub>M I M) (M i)"
proof (unfold measurable_def, intro CollectI conjI ballI)
fix A assume "A \<in> sets (M i)"
- then have "(\<lambda>x. x i) -` A \<inter> space (Pi\<^isub>M I M) = (\<Pi>\<^isub>E j\<in>I. if i = j then A else space (M j))"
- using M.sets_into_space `i \<in> I` by (fastforce dest: Pi_mem split: split_if_asm)
+ then have "(\<lambda>x. x i) -` A \<inter> space (Pi\<^isub>M I M) = prod_emb I M {i} (\<Pi>\<^isub>E j\<in>{i}. A)"
+ using sets_into_space `i \<in> I`
+ by (fastforce dest: Pi_mem simp: prod_emb_def space_PiM split: split_if_asm)
then show "(\<lambda>x. x i) -` A \<inter> space (Pi\<^isub>M I M) \<in> sets (Pi\<^isub>M I M)"
- using `A \<in> sets (M i)` by (auto intro!: product_algebraI)
-qed (insert `i \<in> I`, auto)
+ using `A \<in> sets (M i)` `i \<in> I` by (auto intro!: sets_PiM_I)
+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)"
+ (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)"
+ have "{\<omega> \<in> space ?P. (\<lambda>(f, x). fun_upd f i x) \<omega> j \<in> A} =
+ (if j = i then space (Pi\<^isub>M I M) \<times> A else ((\<lambda>x. x j) \<circ> fst) -` A \<inter> space ?P)"
+ using sets_into_space[OF A] by (auto simp add: space_pair_measure space_PiM)
+ also have "\<dots> \<in> sets ?P"
+ using A j
+ by (auto intro!: measurable_sets[OF measurable_comp, OF _ measurable_component_singleton])
+ finally show "{\<omega> \<in> space ?P. prod_case (\<lambda>f. fun_upd f i) \<omega> j \<in> A} \<in> sets ?P" .
+qed (auto simp: space_pair_measure space_PiM)
-lemma (in sigma_algebra) measurable_restrict:
- assumes I: "finite I"
- assumes "\<And>i. i \<in> I \<Longrightarrow> sets (N i) \<subseteq> Pow (space (N i))"
- assumes X: "\<And>i. i \<in> I \<Longrightarrow> X i \<in> measurable M (N i)"
- shows "(\<lambda>x. \<lambda>i\<in>I. X i x) \<in> measurable M (Pi\<^isub>M I N)"
- unfolding product_algebra_def
-proof (simp, rule measurable_sigma)
- show "sets (product_algebra_generator I N) \<subseteq> Pow (space (product_algebra_generator I N))"
- by (rule product_algebra_generator_sets_into_space) fact
- show "(\<lambda>x. \<lambda>i\<in>I. X i x) \<in> space M \<rightarrow> space (product_algebra_generator I N)"
- using X by (auto simp: measurable_def)
- fix E assume "E \<in> sets (product_algebra_generator I N)"
- then obtain F where "E = Pi\<^isub>E I F" and F: "\<And>i. i \<in> I \<Longrightarrow> F i \<in> sets (N i)"
- by (auto simp: product_algebra_generator_def)
- then have "(\<lambda>x. \<lambda>i\<in>I. X i x) -` E \<inter> space M = (\<Inter>i\<in>I. X i -` F i \<inter> space M) \<inter> space M"
- by (auto simp: Pi_iff)
- also have "\<dots> \<in> sets M"
- proof cases
- assume "I = {}" then show ?thesis by simp
- next
- assume "I \<noteq> {}" with X F I show ?thesis
- by (intro finite_INT measurable_sets Int) auto
- qed
- finally show "(\<lambda>x. \<lambda>i\<in>I. X i x) -` E \<inter> space M \<in> sets M" .
-qed
+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)"
+ (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} =
+ (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
+ 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)
-locale product_sigma_finite = product_sigma_algebra M
- for M :: "'i \<Rightarrow> ('a,'b) measure_space_scheme" +
+lemma measurable_restrict:
+ assumes X: "\<And>i. i \<in> I \<Longrightarrow> X i \<in> measurable N (M i)"
+ shows "(\<lambda>x. \<lambda>i\<in>I. X i x) \<in> measurable N (Pi\<^isub>M I M)"
+proof (rule measurable_PiM_single)
+ fix A i assume A: "i \<in> I" "A \<in> sets (M i)"
+ then have "{\<omega> \<in> space N. (\<lambda>i\<in>I. X i \<omega>) i \<in> A} = X i -` A \<inter> space N"
+ by auto
+ then show "{\<omega> \<in> space N. (\<lambda>i\<in>I. X i \<omega>) i \<in> A} \<in> sets N"
+ using A X by (auto intro!: measurable_sets)
+qed (insert X, auto dest: measurable_space)
+
+locale product_sigma_finite =
+ fixes M :: "'i \<Rightarrow> 'a measure"
assumes sigma_finite_measures: "\<And>i. sigma_finite_measure (M i)"
sublocale product_sigma_finite \<subseteq> M: sigma_finite_measure "M i" for i
by (rule sigma_finite_measures)
-locale finite_product_sigma_finite = finite_product_sigma_algebra M I + product_sigma_finite M
- for M :: "'i \<Rightarrow> ('a,'b) measure_space_scheme" and I :: "'i set"
-
-lemma (in finite_product_sigma_finite) product_algebra_generator_measure:
- assumes "Pi\<^isub>E I F \<in> sets G"
- shows "measure G (Pi\<^isub>E I F) = (\<Prod>i\<in>I. M.\<mu> i (F i))"
-proof cases
- assume ne: "\<forall>i\<in>I. F i \<noteq> {}"
- have "\<forall>i\<in>I. (SOME F'. Pi\<^isub>E I F = Pi\<^isub>E I F') i = F i"
- by (rule someI2[where P="\<lambda>F'. Pi\<^isub>E I F = Pi\<^isub>E I F'"])
- (insert ne, auto simp: Pi_eq_iff)
- then show ?thesis
- unfolding product_algebra_generator_def by simp
-next
- assume empty: "\<not> (\<forall>j\<in>I. F j \<noteq> {})"
- then have "(\<Prod>j\<in>I. M.\<mu> j (F j)) = 0"
- by (auto simp: setprod_ereal_0 intro!: bexI)
- moreover
- have "\<exists>j\<in>I. (SOME F'. Pi\<^isub>E I F = Pi\<^isub>E I F') j = {}"
- by (rule someI2[where P="\<lambda>F'. Pi\<^isub>E I F = Pi\<^isub>E I F'"])
- (insert empty, auto simp: Pi_eq_empty_iff[symmetric])
- then have "(\<Prod>j\<in>I. M.\<mu> j ((SOME F'. Pi\<^isub>E I F = Pi\<^isub>E I F') j)) = 0"
- by (auto simp: setprod_ereal_0 intro!: bexI)
- ultimately show ?thesis
- unfolding product_algebra_generator_def by simp
-qed
+locale finite_product_sigma_finite = product_sigma_finite M for M :: "'i \<Rightarrow> 'a measure" +
+ fixes I :: "'i set"
+ assumes finite_index: "finite I"
lemma (in finite_product_sigma_finite) sigma_finite_pairs:
"\<exists>F::'i \<Rightarrow> nat \<Rightarrow> 'a set.
(\<forall>i\<in>I. range (F i) \<subseteq> sets (M i)) \<and>
- (\<forall>k. \<forall>i\<in>I. \<mu> i (F i k) \<noteq> \<infinity>) \<and> incseq (\<lambda>k. \<Pi>\<^isub>E i\<in>I. F i k) \<and>
- (\<Union>k. \<Pi>\<^isub>E i\<in>I. F i k) = space G"
+ (\<forall>k. \<forall>i\<in>I. emeasure (M i) (F i k) \<noteq> \<infinity>) \<and> incseq (\<lambda>k. \<Pi>\<^isub>E i\<in>I. F i k) \<and>
+ (\<Union>k. \<Pi>\<^isub>E i\<in>I. F i k) = space (PiM I M)"
proof -
- have "\<forall>i::'i. \<exists>F::nat \<Rightarrow> 'a set. range F \<subseteq> sets (M i) \<and> incseq F \<and> (\<Union>i. F i) = space (M i) \<and> (\<forall>k. \<mu> i (F k) \<noteq> \<infinity>)"
- using M.sigma_finite_up by simp
+ have "\<forall>i::'i. \<exists>F::nat \<Rightarrow> 'a set. range F \<subseteq> sets (M i) \<and> incseq F \<and> (\<Union>i. F i) = space (M i) \<and> (\<forall>k. emeasure (M i) (F k) \<noteq> \<infinity>)"
+ using M.sigma_finite_incseq by metis
from choice[OF this] guess F :: "'i \<Rightarrow> nat \<Rightarrow> 'a set" ..
- then have F: "\<And>i. range (F i) \<subseteq> sets (M i)" "\<And>i. incseq (F i)" "\<And>i. (\<Union>j. F i j) = space (M i)" "\<And>i k. \<mu> i (F i k) \<noteq> \<infinity>"
+ then have F: "\<And>i. range (F i) \<subseteq> sets (M i)" "\<And>i. incseq (F i)" "\<And>i. (\<Union>j. F i j) = space (M i)" "\<And>i k. emeasure (M i) (F i k) \<noteq> \<infinity>"
by auto
let ?F = "\<lambda>k. \<Pi>\<^isub>E i\<in>I. F i k"
- note space_product_algebra[simp]
+ note space_PiM[simp]
show ?thesis
proof (intro exI[of _ F] conjI allI incseq_SucI set_eqI iffI ballI)
fix i show "range (F i) \<subseteq> sets (M i)" by fact
next
- fix i k show "\<mu> i (F i k) \<noteq> \<infinity>" by fact
+ fix i k show "emeasure (M i) (F i k) \<noteq> \<infinity>" by fact
next
- fix A assume "A \<in> (\<Union>i. ?F i)" then show "A \<in> space G"
- using `\<And>i. range (F i) \<subseteq> sets (M i)` M.sets_into_space
- by (force simp: image_subset_iff)
+ fix A assume "A \<in> (\<Union>i. ?F i)" then show "A \<in> space (PiM I M)"
+ using `\<And>i. range (F i) \<subseteq> sets (M i)` sets_into_space
+ by auto blast
next
- fix f assume "f \<in> space G"
+ fix f assume "f \<in> space (PiM I M)"
with Pi_UN[OF finite_index, of "\<lambda>k i. F i k"] F
show "f \<in> (\<Union>i. ?F i)" by (auto simp: incseq_def)
next
@@ -574,140 +590,144 @@
qed
qed
-lemma sets_pair_cancel_measure[simp]:
- "sets (M1\<lparr>measure := m1\<rparr> \<Otimes>\<^isub>M M2) = sets (M1 \<Otimes>\<^isub>M M2)"
- "sets (M1 \<Otimes>\<^isub>M M2\<lparr>measure := m2\<rparr>) = sets (M1 \<Otimes>\<^isub>M M2)"
- unfolding pair_measure_def pair_measure_generator_def sets_sigma
- by simp_all
-
-lemma measurable_pair_cancel_measure[simp]:
- "measurable (M1\<lparr>measure := m1\<rparr> \<Otimes>\<^isub>M M2) M = measurable (M1 \<Otimes>\<^isub>M M2) M"
- "measurable (M1 \<Otimes>\<^isub>M M2\<lparr>measure := m2\<rparr>) M = measurable (M1 \<Otimes>\<^isub>M M2) M"
- "measurable M (M1\<lparr>measure := m3\<rparr> \<Otimes>\<^isub>M M2) = measurable M (M1 \<Otimes>\<^isub>M M2)"
- "measurable M (M1 \<Otimes>\<^isub>M M2\<lparr>measure := m4\<rparr>) = measurable M (M1 \<Otimes>\<^isub>M M2)"
- unfolding measurable_def by (auto simp add: space_pair_measure)
-
-lemma (in product_sigma_finite) product_measure_exists:
+lemma (in product_sigma_finite)
assumes "finite I"
- shows "\<exists>\<nu>. sigma_finite_measure (sigma (product_algebra_generator I M) \<lparr> measure := \<nu> \<rparr>) \<and>
- (\<forall>A\<in>\<Pi> i\<in>I. sets (M i). \<nu> (Pi\<^isub>E I A) = (\<Prod>i\<in>I. M.\<mu> i (A 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
case empty
- interpret finite_product_sigma_finite M "{}" by default simp
- let ?\<nu> = "(\<lambda>A. if A = {} then 0 else 1) :: 'd set \<Rightarrow> ereal"
- show ?case
- proof (intro exI conjI ballI)
- have "sigma_algebra (sigma G \<lparr>measure := ?\<nu>\<rparr>)"
- by (rule sigma_algebra_cong) (simp_all add: product_algebra_def)
- then have "measure_space (sigma G\<lparr>measure := ?\<nu>\<rparr>)"
- by (rule finite_additivity_sufficient)
- (simp_all add: positive_def additive_def sets_sigma
- product_algebra_generator_def image_constant)
- then show "sigma_finite_measure (sigma G\<lparr>measure := ?\<nu>\<rparr>)"
- by (auto intro!: exI[of _ "\<lambda>i. {\<lambda>_. undefined}"]
- simp: sigma_finite_measure_def sigma_finite_measure_axioms_def
- product_algebra_generator_def)
- qed auto
+ let ?\<mu> = "\<lambda>A. if A = {} then 0 else (1::ereal)"
+ have "prod_algebra {} M = {{\<lambda>_. undefined}}"
+ by (auto simp: prod_algebra_def prod_emb_def intro!: image_eqI)
+ then have sets_empty: "sets (PiM {} M) = {{}, {\<lambda>_. undefined}}"
+ by (simp add: sets_PiM)
+ have "emeasure (Pi\<^isub>M {} M) (prod_emb {} M {} (\<Pi>\<^isub>E i\<in>{}. {})) = 1"
+ proof (subst emeasure_extend_measure_Pair[OF PiM_def])
+ have "finite (space (PiM {} M))"
+ by (simp add: space_PiM)
+ moreover show "positive (PiM {} M) ?\<mu>"
+ by (auto simp: positive_def)
+ ultimately show "countably_additive (PiM {} M) ?\<mu>"
+ by (rule countably_additiveI_finite) (auto simp: additive_def space_PiM sets_empty)
+ 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
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
- from insert obtain \<nu> where
- prod: "\<And>A. A \<in> (\<Pi> i\<in>I. sets (M i)) \<Longrightarrow> \<nu> (Pi\<^isub>E I A) = (\<Prod>i\<in>I. M.\<mu> i (A i))" and
- "sigma_finite_measure (sigma G\<lparr> measure := \<nu> \<rparr>)" by auto
- then interpret I: sigma_finite_measure "P\<lparr> measure := \<nu>\<rparr>" unfolding product_algebra_def by simp
- interpret P: pair_sigma_finite "P\<lparr> measure := \<nu>\<rparr>" "M i" ..
+ 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 ?\<nu> = "\<lambda>A. P.\<mu> (?h -` A \<inter> space P.P)"
- have I': "sigma_algebra (I'.P\<lparr> measure := ?\<nu> \<rparr>)"
- by (rule I'.sigma_algebra_cong) simp_all
- interpret I'': measure_space "I'.P\<lparr> measure := ?\<nu> \<rparr>"
- using measurable_add_dim[OF `i \<notin> I`]
- by (intro P.measure_space_vimage[OF I']) (auto simp add: measure_preserving_def)
- show ?case
- proof (intro exI[of _ ?\<nu>] conjI ballI)
- let ?m = "\<lambda>A. measure (Pi\<^isub>M I M\<lparr>measure := \<nu>\<rparr> \<Otimes>\<^isub>M M i) (?h -` A \<inter> space P.P)"
- { fix A assume A: "A \<in> (\<Pi> i\<in>insert i I. sets (M i))"
- then have *: "?h -` Pi\<^isub>E (insert i I) A \<inter> space P.P = Pi\<^isub>E I A \<times> A i"
- using `i \<notin> I` M.sets_into_space by (auto simp: space_pair_measure space_product_algebra) blast
- show "?m (Pi\<^isub>E (insert i I) A) = (\<Prod>i\<in>insert i I. M.\<mu> i (A i))"
- unfolding * using A
- apply (subst P.pair_measure_times)
- using A apply fastforce
- using A apply fastforce
- using `i \<notin> I` `finite I` prod[of A] A by (auto simp: ac_simps) }
- note product = this
- have *: "sigma I'.G\<lparr> measure := ?\<nu> \<rparr> = I'.P\<lparr> measure := ?\<nu> \<rparr>"
- by (simp add: product_algebra_def)
- show "sigma_finite_measure (sigma I'.G\<lparr> measure := ?\<nu> \<rparr>)"
- proof (unfold *, default, simp)
- 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 I'.G"
- "\<And>k. \<And>j. j \<in> insert i I \<Longrightarrow> \<mu> j (F j k) \<noteq> \<infinity>"
- by blast+
- let ?F = "\<lambda>k. \<Pi>\<^isub>E j \<in> insert i I. F j k"
- show "\<exists>F::nat \<Rightarrow> ('i \<Rightarrow> 'a) set. range F \<subseteq> sets I'.P \<and>
- (\<Union>i. F i) = (\<Pi>\<^isub>E i\<in>insert i I. space (M i)) \<and> (\<forall>i. ?m (F i) \<noteq> \<infinity>)"
- proof (intro exI[of _ ?F] conjI allI)
- show "range ?F \<subseteq> sets I'.P" using F(1) by auto
- next
- from F(3) show "(\<Union>i. ?F i) = (\<Pi>\<^isub>E i\<in>insert i I. space (M i))" by simp
- next
- fix j
- have "\<And>k. k \<in> insert i I \<Longrightarrow> 0 \<le> measure (M k) (F k j)"
- using F(1) by auto
- with F `finite I` setprod_PInf[of "insert i I", OF this] show "?\<nu> (?F j) \<noteq> \<infinity>"
- by (subst product) auto
- qed
- qed
+
+ let ?P = "distr (Pi\<^isub>M I M \<Otimes>\<^isub>M M i) (Pi\<^isub>M (insert i I) M) ?h"
+ let ?\<mu> = "emeasure ?P"
+ 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>" .
+
+ 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
+
+ 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>"
+ by blast+
+ let ?F = "\<lambda>k. \<Pi>\<^isub>E j \<in> insert i I. F j k"
+
+ case 1 show ?case
+ 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
+ next
+ from F(3) show "(\<Union>i. ?F i) = space (Pi\<^isub>M (insert i 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
qed
qed
-sublocale finite_product_sigma_finite \<subseteq> sigma_finite_measure P
- unfolding product_algebra_def
- using product_measure_exists[OF finite_index]
- by (rule someI2_ex) auto
+sublocale finite_product_sigma_finite \<subseteq> sigma_finite_measure "Pi\<^isub>M I M"
+ using sigma_finite[OF finite_index] .
lemma (in finite_product_sigma_finite) measure_times:
- assumes "\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (M i)"
- shows "\<mu> (Pi\<^isub>E I A) = (\<Prod>i\<in>I. M.\<mu> i (A i))"
- unfolding product_algebra_def
- using product_measure_exists[OF finite_index]
- proof (rule someI2_ex, elim conjE)
- fix \<nu> assume *: "\<forall>A\<in>\<Pi> i\<in>I. sets (M i). \<nu> (Pi\<^isub>E I A) = (\<Prod>i\<in>I. M.\<mu> i (A i))"
- have "Pi\<^isub>E I A = Pi\<^isub>E I (\<lambda>i\<in>I. A i)" by (auto dest: Pi_mem)
- then have "\<nu> (Pi\<^isub>E I A) = \<nu> (Pi\<^isub>E I (\<lambda>i\<in>I. A i))" by simp
- also have "\<dots> = (\<Prod>i\<in>I. M.\<mu> i ((\<lambda>i\<in>I. A i) i))" using assms * by auto
- finally show "measure (sigma G\<lparr>measure := \<nu>\<rparr>) (Pi\<^isub>E I A) = (\<Prod>i\<in>I. M.\<mu> i (A i))"
- by (simp add: sigma_def)
- qed
+ "(\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (M i)) \<Longrightarrow> emeasure (Pi\<^isub>M I M) (Pi\<^isub>E I A) = (\<Prod>i\<in>I. emeasure (M i) (A i))"
+ using emeasure_PiM[OF finite_index] by auto
lemma (in product_sigma_finite) product_measure_empty[simp]:
- "measure (Pi\<^isub>M {} M) {\<lambda>x. undefined} = 1"
+ "emeasure (Pi\<^isub>M {} M) {\<lambda>x. undefined} = 1"
proof -
interpret finite_product_sigma_finite M "{}" by default auto
from measure_times[of "\<lambda>x. {}"] show ?thesis by simp
qed
-lemma (in finite_product_sigma_algebra) P_empty:
- assumes "I = {}"
- shows "space P = {\<lambda>k. undefined}" "sets P = { {}, {\<lambda>k. undefined} }"
- unfolding product_algebra_def product_algebra_generator_def `I = {}`
- by (simp_all add: sigma_def image_constant)
+lemma
+ shows space_PiM_empty: "space (Pi\<^isub>M {} M) = {\<lambda>k. undefined}"
+ and sets_PiM_empty: "sets (Pi\<^isub>M {} M) = { {}, {\<lambda>k. undefined} }"
+ by (simp_all add: space_PiM sets_PiM_single image_constant sigma_sets_empty_eq)
lemma (in product_sigma_finite) positive_integral_empty:
assumes pos: "0 \<le> f (\<lambda>k. undefined)"
shows "integral\<^isup>P (Pi\<^isub>M {} M) f = f (\<lambda>k. undefined)"
proof -
interpret finite_product_sigma_finite M "{}" by default (fact finite.emptyI)
- have "\<And>A. measure (Pi\<^isub>M {} M) (Pi\<^isub>E {} A) = 1"
+ have "\<And>A. emeasure (Pi\<^isub>M {} M) (Pi\<^isub>E {} A) = 1"
using assms by (subst measure_times) auto
then show ?thesis
- unfolding positive_integral_def simple_function_def simple_integral_def [abs_def]
- proof (simp add: P_empty, intro antisym)
+ unfolding positive_integral_def simple_function_def simple_integral_def[abs_def]
+ proof (simp add: space_PiM_empty sets_PiM_empty, intro antisym)
show "f (\<lambda>k. undefined) \<le> (SUP f:{g. g \<le> max 0 \<circ> f}. f (\<lambda>k. undefined))"
by (intro SUP_upper) (auto simp: le_fun_def split: split_max)
show "(SUP f:{g. g \<le> max 0 \<circ> f}. f (\<lambda>k. undefined)) \<le> f (\<lambda>k. undefined)" using pos
@@ -715,71 +735,72 @@
qed
qed
-lemma (in product_sigma_finite) measure_fold:
+lemma (in product_sigma_finite) distr_merge:
assumes IJ[simp]: "I \<inter> J = {}" and fin: "finite I" "finite J"
- assumes A: "A \<in> sets (Pi\<^isub>M (I \<union> J) M)"
- shows "measure (Pi\<^isub>M (I \<union> J) M) A =
- measure (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M) ((\<lambda>(x,y). merge I x J y) -` A \<inter> space (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M))"
+ shows "distr (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) = Pi\<^isub>M (I \<union> J) M"
+ (is "?D = ?P")
proof -
interpret I: finite_product_sigma_finite M I by default fact
interpret J: finite_product_sigma_finite M J by default fact
have "finite (I \<union> J)" using fin by auto
interpret IJ: finite_product_sigma_finite M "I \<union> J" by default fact
- interpret P: pair_sigma_finite I.P J.P by default
+ interpret P: pair_sigma_finite "Pi\<^isub>M I M" "Pi\<^isub>M J M" by default
let ?g = "\<lambda>(x,y). merge I x J y"
- let ?X = "\<lambda>S. ?g -` S \<inter> space P.P"
+
from IJ.sigma_finite_pairs obtain F where
F: "\<And>i. i\<in> I \<union> J \<Longrightarrow> range (F i) \<subseteq> sets (M i)"
"incseq (\<lambda>k. \<Pi>\<^isub>E i\<in>I \<union> J. F i k)"
- "(\<Union>k. \<Pi>\<^isub>E i\<in>I \<union> J. F i k) = space IJ.G"
- "\<And>k. \<forall>i\<in>I\<union>J. \<mu> i (F i k) \<noteq> \<infinity>"
+ "(\<Union>k. \<Pi>\<^isub>E i\<in>I \<union> J. F i k) = space ?P"
+ "\<And>k. \<forall>i\<in>I\<union>J. emeasure (M i) (F i k) \<noteq> \<infinity>"
by auto
let ?F = "\<lambda>k. \<Pi>\<^isub>E i\<in>I \<union> J. F i k"
- show "IJ.\<mu> A = P.\<mu> (?X A)"
- proof (rule measure_unique_Int_stable_vimage)
- show "measure_space IJ.P" "measure_space P.P" by default
- show "sets (sigma IJ.G) = sets IJ.P" "space IJ.G = space IJ.P" "A \<in> sets (sigma IJ.G)"
- using A unfolding product_algebra_def by auto
- next
- show "Int_stable IJ.G"
- by (rule Int_stable_product_algebra_generator)
- (auto simp: Int_stable_def)
- show "range ?F \<subseteq> sets IJ.G" using F
- by (simp add: image_subset_iff product_algebra_def
- product_algebra_generator_def)
- show "incseq ?F" "(\<Union>i. ?F i) = space IJ.G " by fact+
+
+ show ?thesis
+ proof (rule measure_eqI_generator_eq[symmetric])
+ show "Int_stable (prod_algebra (I \<union> J) M)"
+ by (rule Int_stable_prod_algebra)
+ show "prod_algebra (I \<union> J) M \<subseteq> Pow (\<Pi>\<^isub>E i \<in> I \<union> J. space (M i))"
+ by (rule prod_algebra_sets_into_space)
+ show "sets ?P = sigma_sets (\<Pi>\<^isub>E i\<in>I \<union> J. space (M i)) (prod_algebra (I \<union> J) M)"
+ by (rule sets_PiM)
+ then show "sets ?D = sigma_sets (\<Pi>\<^isub>E i\<in>I \<union> J. space (M i)) (prod_algebra (I \<union> J) M)"
+ by simp
+
+ show "range ?F \<subseteq> prod_algebra (I \<union> J) M" using F
+ using fin by (auto simp: prod_algebra_eq_finite)
+ show "incseq ?F" by fact
+ show "(\<Union>i. \<Pi>\<^isub>E ia\<in>I \<union> J. F ia i) = (\<Pi>\<^isub>E i\<in>I \<union> J. space (M i))"
+ using F(3) by (simp add: space_PiM)
next
fix k
- have "\<And>j. j \<in> I \<union> J \<Longrightarrow> 0 \<le> measure (M j) (F j k)"
- using F(1) by auto
- with F `finite I` setprod_PInf[of "I \<union> J", OF this]
- show "IJ.\<mu> (?F k) \<noteq> \<infinity>" by (subst IJ.measure_times) auto
+ from F `finite I` setprod_PInf[of "I \<union> J", OF emeasure_nonneg, of M]
+ show "emeasure ?P (?F k) \<noteq> \<infinity>" by (subst IJ.measure_times) auto
next
- fix A assume "A \<in> sets IJ.G"
- then obtain F where A: "A = Pi\<^isub>E (I \<union> J) F"
- and F: "\<And>i. i \<in> I \<union> J \<Longrightarrow> F i \<in> sets (M i)"
- by (auto simp: product_algebra_generator_def)
- then have X: "?X A = (Pi\<^isub>E I F \<times> Pi\<^isub>E J F)"
- using sets_into_space by (auto simp: space_pair_measure) blast+
- then have "P.\<mu> (?X A) = (\<Prod>i\<in>I. \<mu> i (F i)) * (\<Prod>i\<in>J. \<mu> i (F i))"
- using `finite J` `finite I` F
- by (simp add: P.pair_measure_times I.measure_times J.measure_times)
- also have "\<dots> = (\<Prod>i\<in>I \<union> J. \<mu> i (F i))"
+ fix A assume A: "A \<in> prod_algebra (I \<union> J) M"
+ with fin obtain F where A_eq: "A = (Pi\<^isub>E (I \<union> J) F)" and F: "\<forall>i\<in>I \<union> J. F i \<in> sets (M i)"
+ by (auto simp add: prod_algebra_eq_finite)
+ let ?B = "Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M"
+ let ?X = "?g -` A \<inter> space ?B"
+ have "Pi\<^isub>E I F \<subseteq> space (Pi\<^isub>M I M)" "Pi\<^isub>E J F \<subseteq> space (Pi\<^isub>M J M)"
+ using F[rule_format, THEN sets_into_space] by (auto simp: space_PiM)
+ then have X: "?X = (Pi\<^isub>E I F \<times> Pi\<^isub>E J F)"
+ unfolding A_eq by (subst merge_vimage) (auto simp: space_pair_measure space_PiM)
+ have "emeasure ?D A = emeasure ?B ?X"
+ 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)
+ 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> = IJ.\<mu> A"
+ also have "\<dots> = emeasure ?P (Pi\<^isub>E (I \<union> J) F)"
using `finite J` `finite I` F unfolding A
by (intro IJ.measure_times[symmetric]) auto
- finally show "IJ.\<mu> A = P.\<mu> (?X A)" by (rule sym)
- qed (rule measurable_merge[OF IJ])
+ finally show "emeasure ?P A = emeasure ?D A" using A_eq by simp
+ qed
qed
-lemma (in product_sigma_finite) measure_preserving_merge:
- assumes IJ: "I \<inter> J = {}" and "finite I" "finite J"
- shows "(\<lambda>(x,y). merge I x J y) \<in> measure_preserving (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M) (Pi\<^isub>M (I \<union> J) M)"
- by (intro measure_preservingI measurable_merge[OF IJ] measure_fold[symmetric] assms)
-
lemma (in product_sigma_finite) product_positive_integral_fold:
- assumes IJ[simp]: "I \<inter> J = {}" "finite I" "finite J"
+ assumes IJ: "I \<inter> J = {}" "finite I" "finite J"
and f: "f \<in> borel_measurable (Pi\<^isub>M (I \<union> J) M)"
shows "integral\<^isup>P (Pi\<^isub>M (I \<union> J) M) f =
(\<integral>\<^isup>+ x. (\<integral>\<^isup>+ y. f (merge I x J y) \<partial>(Pi\<^isub>M J M)) \<partial>(Pi\<^isub>M I M))"
@@ -787,42 +808,38 @@
interpret I: finite_product_sigma_finite M I by default fact
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
- interpret IJ: finite_product_sigma_finite M "I \<union> J" by default simp
- have P_borel: "(\<lambda>x. f (case x of (x, y) \<Rightarrow> merge I x J y)) \<in> borel_measurable P.P"
+ 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)
show ?thesis
- unfolding P.positive_integral_fst_measurable[OF P_borel, simplified]
- proof (rule P.positive_integral_vimage)
- show "sigma_algebra IJ.P" by default
- show "(\<lambda>(x, y). merge I x J y) \<in> measure_preserving P.P IJ.P"
- using IJ by (rule measure_preserving_merge)
- show "f \<in> borel_measurable IJ.P" using f by simp
- qed
+ apply (subst distr_merge[OF IJ, symmetric])
+ apply (subst positive_integral_distr[OF measurable_merge f, OF IJ(1)])
+ apply (subst P.positive_integral_fst_measurable(2)[symmetric, OF P_borel])
+ apply simp
+ done
qed
-lemma (in product_sigma_finite) measure_preserving_component_singelton:
- "(\<lambda>x. x i) \<in> measure_preserving (Pi\<^isub>M {i} M) (M i)"
-proof (intro measure_preservingI measurable_component_singleton)
+lemma (in product_sigma_finite) distr_singleton:
+ "distr (Pi\<^isub>M {i} M) (M i) (\<lambda>x. x i) = M i" (is "?D = _")
+proof (intro measure_eqI[symmetric])
interpret I: finite_product_sigma_finite M "{i}" by default simp
- fix A let ?P = "(\<lambda>x. x i) -` A \<inter> space I.P"
- assume A: "A \<in> sets (M i)"
- then have *: "?P = {i} \<rightarrow>\<^isub>E A" using sets_into_space by auto
- show "I.\<mu> ?P = M.\<mu> i A" unfolding *
- using A I.measure_times[of "\<lambda>_. A"] by auto
-qed auto
+ fix A assume A: "A \<in> sets (M i)"
+ moreover then have "(\<lambda>x. x i) -` A \<inter> space (Pi\<^isub>M {i} M) = (\<Pi>\<^isub>E i\<in>{i}. A)"
+ using sets_into_space by (auto simp: space_PiM)
+ ultimately show "emeasure (M i) A = emeasure ?D A"
+ using A I.measure_times[of "\<lambda>_. A"]
+ by (simp add: emeasure_distr measurable_component_singleton)
+qed simp
lemma (in product_sigma_finite) product_positive_integral_singleton:
assumes f: "f \<in> borel_measurable (M i)"
shows "integral\<^isup>P (Pi\<^isub>M {i} M) (\<lambda>x. f (x i)) = integral\<^isup>P (M i) f"
proof -
interpret I: finite_product_sigma_finite M "{i}" by default simp
- show ?thesis
- proof (rule I.positive_integral_vimage[symmetric])
- show "sigma_algebra (M i)" by (rule sigma_algebras)
- show "(\<lambda>x. x i) \<in> measure_preserving (Pi\<^isub>M {i} M) (M i)"
- by (rule measure_preserving_component_singelton)
- show "f \<in> borel_measurable (M i)" by fact
- qed
+ from f show ?thesis
+ apply (subst distr_singleton[symmetric])
+ apply (subst positive_integral_distr[OF measurable_component_singleton])
+ apply simp_all
+ done
qed
lemma (in product_sigma_finite) product_positive_integral_insert:
@@ -832,19 +849,18 @@
proof -
interpret I: finite_product_sigma_finite M I by default auto
interpret i: finite_product_sigma_finite M "{i}" by default auto
- interpret P: pair_sigma_algebra I.P i.P ..
have IJ: "I \<inter> {i} = {}" and insert: "I \<union> {i} = insert i I"
using f by auto
show ?thesis
unfolding product_positive_integral_fold[OF IJ, unfolded insert, simplified, OF f]
- proof (rule I.positive_integral_cong, subst product_positive_integral_singleton)
- fix x assume x: "x \<in> space I.P"
+ proof (rule positive_integral_cong, subst product_positive_integral_singleton)
+ fix x assume x: "x \<in> space (Pi\<^isub>M I M)"
let ?f = "\<lambda>y. f (restrict (x(i := y)) (insert i I))"
have f'_eq: "\<And>y. ?f y = f (x(i := y))"
- using x by (auto intro!: arg_cong[where f=f] simp: fun_eq_iff extensional_def)
+ using x by (auto intro!: arg_cong[where f=f] simp: fun_eq_iff extensional_def space_PiM)
show "?f \<in> borel_measurable (M i)" unfolding f'_eq
- using measurable_comp[OF measurable_component_update f] x `i \<notin> I`
- by (simp add: comp_def)
+ using measurable_comp[OF measurable_component_update f, OF x `i \<notin> I`]
+ unfolding comp_def .
show "integral\<^isup>P (M i) ?f = \<integral>\<^isup>+ y. f (x(i:=y)) \<partial>M i"
unfolding f'_eq by simp
qed
@@ -856,10 +872,6 @@
and pos: "\<And>i x. i \<in> I \<Longrightarrow> 0 \<le> f i x"
shows "(\<integral>\<^isup>+ x. (\<Prod>i\<in>I. f i (x i)) \<partial>Pi\<^isub>M I M) = (\<Prod>i\<in>I. integral\<^isup>P (M i) (f i))"
using assms proof induct
- case empty
- interpret finite_product_sigma_finite M "{}" by default auto
- show ?case by simp
-next
case (insert i I)
note `finite I`[intro, simp]
interpret I: finite_product_sigma_finite M I by default auto
@@ -867,16 +879,16 @@
using insert by (auto intro!: setprod_cong)
have prod: "\<And>J. J \<subseteq> insert i I \<Longrightarrow> (\<lambda>x. (\<Prod>i\<in>J. f i (x i))) \<in> borel_measurable (Pi\<^isub>M J M)"
using sets_into_space insert
- by (intro sigma_algebra.borel_measurable_ereal_setprod sigma_algebra_product_algebra
+ by (intro borel_measurable_ereal_setprod
measurable_comp[OF measurable_component_singleton, unfolded comp_def])
auto
then show ?case
apply (simp add: product_positive_integral_insert[OF insert(1,2) prod])
- apply (simp add: insert * pos borel setprod_ereal_pos M.positive_integral_multc)
- apply (subst I.positive_integral_cmult)
- apply (auto simp add: pos borel insert setprod_ereal_pos positive_integral_positive)
+ apply (simp add: insert(2-) * pos borel setprod_ereal_pos positive_integral_multc)
+ apply (subst positive_integral_cmult)
+ apply (auto simp add: pos borel insert(2-) setprod_ereal_pos positive_integral_positive)
done
-qed
+qed (simp add: space_PiM)
lemma (in product_sigma_finite) product_integral_singleton:
assumes f: "f \<in> borel_measurable (M i)"
@@ -899,48 +911,44 @@
interpret J: finite_product_sigma_finite M J by default fact
have "finite (I \<union> J)" using fin by auto
interpret IJ: finite_product_sigma_finite M "I \<union> J" by default fact
- interpret P: pair_sigma_finite I.P J.P by default
+ interpret P: pair_sigma_finite "Pi\<^isub>M I M" "Pi\<^isub>M J M" by default
let ?M = "\<lambda>(x, y). merge I x J y"
let ?f = "\<lambda>x. f (?M x)"
+ 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)
+ 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)
show ?thesis
- proof (subst P.integrable_fst_measurable(2)[of ?f, simplified])
- have 1: "sigma_algebra IJ.P" by default
- have 2: "?M \<in> measure_preserving P.P IJ.P" using measure_preserving_merge[OF assms(1,2,3)] .
- have 3: "integrable (Pi\<^isub>M (I \<union> J) M) f" by fact
- then have 4: "f \<in> borel_measurable (Pi\<^isub>M (I \<union> J) M)"
- by (simp add: integrable_def)
- show "integrable P.P ?f"
- by (rule P.integrable_vimage[where f=f, OF 1 2 3])
- show "integral\<^isup>L IJ.P f = integral\<^isup>L P.P ?f"
- by (rule P.integral_vimage[where f=f, OF 1 2 4])
- qed
+ apply (subst distr_merge[symmetric, OF IJ fin])
+ apply (subst integral_distr[OF measurable_merge[OF IJ] f_borel])
+ apply (subst P.integrable_fst_measurable(2)[symmetric, OF f_int])
+ apply simp
+ done
qed
lemma (in product_sigma_finite) product_integral_insert:
- assumes [simp]: "finite I" "i \<notin> I"
+ assumes I: "finite I" "i \<notin> I"
and f: "integrable (Pi\<^isub>M (insert i I) M) f"
shows "integral\<^isup>L (Pi\<^isub>M (insert i I) M) f = (\<integral>x. (\<integral>y. f (x(i:=y)) \<partial>M i) \<partial>Pi\<^isub>M I M)"
proof -
- interpret I: finite_product_sigma_finite M I by default auto
- interpret I': finite_product_sigma_finite M "insert i I" by default auto
- interpret i: finite_product_sigma_finite M "{i}" by default auto
- interpret P: pair_sigma_finite I.P i.P ..
- have IJ: "I \<inter> {i} = {}" by auto
- show ?thesis
- unfolding product_integral_fold[OF IJ, simplified, OF f]
- proof (rule I.integral_cong, subst product_integral_singleton)
- fix x assume x: "x \<in> space I.P"
- let ?f = "\<lambda>y. f (restrict (x(i := y)) (insert i I))"
- have f'_eq: "\<And>y. ?f y = f (x(i := y))"
- using x by (auto intro!: arg_cong[where f=f] simp: fun_eq_iff extensional_def)
- have f: "f \<in> borel_measurable I'.P" using f unfolding integrable_def by auto
- show "?f \<in> borel_measurable (M i)"
- unfolding measurable_cong[OF f'_eq]
- using measurable_comp[OF measurable_component_update f] x `i \<notin> I`
- by (simp add: comp_def)
- show "integral\<^isup>L (M i) ?f = integral\<^isup>L (M i) (\<lambda>y. f (x(i := y)))"
- unfolding f'_eq by simp
+ have "integral\<^isup>L (Pi\<^isub>M (insert i I) M) f = integral\<^isup>L (Pi\<^isub>M (I \<union> {i}) M) f"
+ by simp
+ also have "\<dots> = (\<integral>x. (\<integral>y. f (merge I x {i} y) \<partial>Pi\<^isub>M {i} M) \<partial>Pi\<^isub>M I M)"
+ using f I by (intro product_integral_fold) auto
+ also have "\<dots> = (\<integral>x. (\<integral>y. f (x(i := y)) \<partial>M i) \<partial>Pi\<^isub>M I M)"
+ proof (rule integral_cong, subst product_integral_singleton[symmetric])
+ fix x assume x: "x \<in> space (Pi\<^isub>M I M)"
+ have f_borel: "f \<in> borel_measurable (Pi\<^isub>M (insert i I) M)"
+ using f by auto
+ show "(\<lambda>y. f (x(i := y))) \<in> borel_measurable (M i)"
+ using measurable_comp[OF measurable_component_update f_borel, OF x `i \<notin> I`]
+ unfolding comp_def .
+ from x I show "(\<integral> y. f (merge I x {i} y) \<partial>Pi\<^isub>M {i} M) = (\<integral> xa. f (x(i := xa i)) \<partial>Pi\<^isub>M {i} M)"
+ by (auto intro!: integral_cong arg_cong[where f=f] simp: merge_def space_PiM extensional_def)
qed
+ finally show ?thesis .
qed
lemma (in product_sigma_finite) product_integrable_setprod:
@@ -951,24 +959,23 @@
interpret finite_product_sigma_finite M I by default fact
have f: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> borel_measurable (M i)"
using integrable unfolding integrable_def by auto
- then have borel: "?f \<in> borel_measurable P"
- using measurable_comp[OF measurable_component_singleton f]
- by (auto intro!: borel_measurable_setprod simp: comp_def)
+ have borel: "?f \<in> borel_measurable (Pi\<^isub>M I M)"
+ using measurable_comp[OF measurable_component_singleton[of _ I M] f] by (auto simp: comp_def)
moreover have "integrable (Pi\<^isub>M I M) (\<lambda>x. \<bar>\<Prod>i\<in>I. f i (x i)\<bar>)"
proof (unfold integrable_def, intro conjI)
- show "(\<lambda>x. abs (?f x)) \<in> borel_measurable P"
+ show "(\<lambda>x. abs (?f x)) \<in> borel_measurable (Pi\<^isub>M I M)"
using borel by auto
- have "(\<integral>\<^isup>+x. ereal (abs (?f x)) \<partial>P) = (\<integral>\<^isup>+x. (\<Prod>i\<in>I. ereal (abs (f i (x i)))) \<partial>P)"
+ have "(\<integral>\<^isup>+x. ereal (abs (?f x)) \<partial>Pi\<^isub>M I M) = (\<integral>\<^isup>+x. (\<Prod>i\<in>I. ereal (abs (f i (x i)))) \<partial>Pi\<^isub>M I M)"
by (simp add: setprod_ereal abs_setprod)
also have "\<dots> = (\<Prod>i\<in>I. (\<integral>\<^isup>+x. ereal (abs (f i x)) \<partial>M i))"
using f by (subst product_positive_integral_setprod) auto
also have "\<dots> < \<infinity>"
- using integrable[THEN M.integrable_abs]
- by (simp add: setprod_PInf integrable_def M.positive_integral_positive)
- finally show "(\<integral>\<^isup>+x. ereal (abs (?f x)) \<partial>P) \<noteq> \<infinity>" by auto
- have "(\<integral>\<^isup>+x. ereal (- abs (?f x)) \<partial>P) = (\<integral>\<^isup>+x. 0 \<partial>P)"
+ using integrable[THEN integrable_abs]
+ by (simp add: setprod_PInf integrable_def positive_integral_positive)
+ finally show "(\<integral>\<^isup>+x. ereal (abs (?f x)) \<partial>(Pi\<^isub>M I M)) \<noteq> \<infinity>" by auto
+ have "(\<integral>\<^isup>+x. ereal (- abs (?f x)) \<partial>(Pi\<^isub>M I M)) = (\<integral>\<^isup>+x. 0 \<partial>(Pi\<^isub>M I M))"
by (intro positive_integral_cong_pos) auto
- then show "(\<integral>\<^isup>+x. ereal (- abs (?f x)) \<partial>P) \<noteq> \<infinity>" by simp
+ then show "(\<integral>\<^isup>+x. ereal (- abs (?f x)) \<partial>(Pi\<^isub>M I M)) \<noteq> \<infinity>" by simp
qed
ultimately show ?thesis
by (rule integrable_abs_iff[THEN iffD1])
@@ -992,7 +999,69 @@
using `i \<notin> I` by (auto intro!: setprod_cong)
show ?case
unfolding product_integral_insert[OF insert(1,3) prod[OF subset_refl]]
- by (simp add: * insert integral_multc I.integral_cmult[OF prod] subset_insertI)
+ by (simp add: * insert integral_multc integral_cmult[OF prod] subset_insertI)
qed
-end
\ No newline at end of file
+lemma sigma_prod_algebra_sigma_eq:
+ fixes E :: "'i \<Rightarrow> 'a set set"
+ assumes "finite I"
+ 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 == { Pi\<^isub>E I F | F. \<forall>i\<in>I. F i \<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)"
+ have "(\<lambda>x. x i) \<in> measurable ?P (sigma (space (M i)) (E i))"
+ proof (subst measurable_iff_measure_of)
+ show "E i \<subseteq> Pow (space (M i))" using `i \<in> I` by fact
+ from space_P `i \<in> I` show "(\<lambda>x. x i) \<in> space ?P \<rightarrow> space (M i)"
+ by (auto simp: Pi_iff)
+ show "\<forall>A\<in>E i. (\<lambda>x. x i) -` A \<inter> space ?P \<in> sets ?P"
+ proof
+ fix A assume A: "A \<in> E i"
+ then have "(\<lambda>x. x i) -` A \<inter> space ?P = (\<Pi>\<^isub>E j\<in>I. if i = j then A else space (M j))"
+ using E_closed `i \<in> I` by (auto simp: space_P Pi_iff subset_eq split: split_if_asm)
+ also have "\<dots> = (\<Pi>\<^isub>E j\<in>I. \<Union>n. if i = j then A else S j n)"
+ by (intro PiE_cong) (simp add: S_union)
+ also have "\<dots> = (\<Union>n. \<Pi>\<^isub>E j\<in>I. if i = j then A else S j n)"
+ using S_mono
+ by (subst Pi_UN[symmetric, OF `finite I`]) (auto simp: incseq_def)
+ also have "\<dots> \<in> sets ?P"
+ proof (safe intro!: countable_UN)
+ fix n show "(\<Pi>\<^isub>E j\<in>I. if i = j then A else S j n) \<in> sets ?P"
+ using A S_in_E
+ by (simp add: P_closed)
+ (auto simp: P_def subset_eq intro!: exI[of _ "\<lambda>j. if i = j then A else S j n"])
+ qed
+ finally show "(\<lambda>x. x i) -` A \<inter> space ?P \<in> sets ?P"
+ using P_closed by simp
+ qed
+ qed
+ 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)"
+ using `finite I`
+ by (auto intro!: sigma_sets_subset simp: E_generates P_def)
+qed
+
+end