(* Title: HOL/Probability/Finite_Product_Measure.thy Author: Johannes Hölzl, TU München *) header {*Finite product measures*} theory Finite_Product_Measure imports Binary_Product_Measure begin lemma PiE_choice: "(\f\PiE I F. \i\I. P i (f i)) \ (\i\I. \x\F i. P i x)" by (auto simp: Bex_def PiE_iff Ball_def dest!: choice_iff'[THEN iffD1]) (force intro: exI[of _ "restrict f I" for f]) lemma split_const: "(\(i, j). c) = (\_. c)" by auto subsubsection {* More about Function restricted by @{const extensional} *} definition "merge I J = (\(x, y) i. if i \ I then x i else if i \ J then y i else undefined)" lemma merge_apply[simp]: "I \ J = {} \ i \ I \ merge I J (x, y) i = x i" "I \ J = {} \ i \ J \ merge I J (x, y) i = y i" "J \ I = {} \ i \ I \ merge I J (x, y) i = x i" "J \ I = {} \ i \ J \ merge I J (x, y) i = y i" "i \ I \ i \ J \ merge I J (x, y) i = undefined" unfolding merge_def by auto lemma merge_commute: "I \ J = {} \ merge I J (x, y) = merge J I (y, x)" by (force simp: merge_def) lemma Pi_cancel_merge_range[simp]: "I \ J = {} \ x \ Pi I (merge I J (A, B)) \ x \ Pi I A" "I \ J = {} \ x \ Pi I (merge J I (B, A)) \ x \ Pi I A" "J \ I = {} \ x \ Pi I (merge I J (A, B)) \ x \ Pi I A" "J \ I = {} \ x \ Pi I (merge J I (B, A)) \ x \ Pi I A" by (auto simp: Pi_def) lemma Pi_cancel_merge[simp]: "I \ J = {} \ merge I J (x, y) \ Pi I B \ x \ Pi I B" "J \ I = {} \ merge I J (x, y) \ Pi I B \ x \ Pi I B" "I \ J = {} \ merge I J (x, y) \ Pi J B \ y \ Pi J B" "J \ I = {} \ merge I J (x, y) \ Pi J B \ y \ Pi J B" by (auto simp: Pi_def) lemma extensional_merge[simp]: "merge I J (x, y) \ extensional (I \ J)" by (auto simp: extensional_def) lemma restrict_merge[simp]: "I \ J = {} \ restrict (merge I J (x, y)) I = restrict x I" "I \ J = {} \ restrict (merge I J (x, y)) J = restrict y J" "J \ I = {} \ restrict (merge I J (x, y)) I = restrict x I" "J \ I = {} \ restrict (merge I J (x, y)) J = restrict y J" by (auto simp: restrict_def) lemma split_merge: "P (merge I J (x,y) i) \ (i \ I \ P (x i)) \ (i \ J - I \ P (y i)) \ (i \ I \ J \ P undefined)" unfolding merge_def by auto lemma PiE_cancel_merge[simp]: "I \ J = {} \ merge I J (x, y) \ PiE (I \ J) B \ x \ Pi I B \ y \ Pi J B" by (auto simp: PiE_def restrict_Pi_cancel) lemma merge_singleton[simp]: "i \ I \ merge I {i} (x,y) = restrict (x(i := y i)) (insert i I)" unfolding merge_def by (auto simp: fun_eq_iff) lemma extensional_merge_sub: "I \ J \ K \ merge I J (x, y) \ extensional K" unfolding merge_def extensional_def by auto lemma merge_restrict[simp]: "merge I J (restrict x I, y) = merge I J (x, y)" "merge I J (x, restrict y J) = merge I J (x, y)" unfolding merge_def by auto lemma merge_x_x_eq_restrict[simp]: "merge I J (x, x) = restrict x (I \ J)" unfolding merge_def by auto lemma injective_vimage_restrict: assumes J: "J \ I" and sets: "A \ (\\<^sub>E i\J. S i)" "B \ (\\<^sub>E i\J. S i)" and ne: "(\\<^sub>E i\I. S i) \ {}" and eq: "(\x. restrict x J) -` A \ (\\<^sub>E i\I. S i) = (\x. restrict x J) -` B \ (\\<^sub>E i\I. S i)" shows "A = B" proof (intro set_eqI) fix x from ne obtain y where y: "\i. i \ I \ y i \ S i" by auto have "J \ (I - J) = {}" by auto show "x \ A \ x \ B" proof cases assume x: "x \ (\\<^sub>E i\J. S i)" have "x \ A \ merge J (I - J) (x,y) \ (\x. restrict x J) -` A \ (\\<^sub>E i\I. S i)" using y x `J \ I` PiE_cancel_merge[of "J" "I - J" x y S] by (auto simp del: PiE_cancel_merge simp add: Un_absorb1) then show "x \ A \ x \ B" using y x `J \ I` PiE_cancel_merge[of "J" "I - J" x y S] by (auto simp del: PiE_cancel_merge simp add: Un_absorb1 eq) qed (insert sets, auto) qed lemma restrict_vimage: "I \ J = {} \ (\x. (restrict x I, restrict x J)) -` (Pi\<^sub>E I E \ Pi\<^sub>E J F) = Pi (I \ J) (merge I J (E, F))" by (auto simp: restrict_Pi_cancel PiE_def) lemma merge_vimage: "I \ J = {} \ merge I J -` Pi\<^sub>E (I \ J) E = Pi I E \ Pi J E" by (auto simp: restrict_Pi_cancel PiE_def) subsection {* Finite product spaces *} subsubsection {* Products *} definition prod_emb where "prod_emb I M K X = (\x. restrict x K) -` X \ (PIE i:I. space (M i))" lemma prod_emb_iff: "f \ prod_emb I M K X \ f \ extensional I \ (restrict f K \ X) \ (\i\I. f i \ space (M i))" unfolding prod_emb_def PiE_def by auto lemma shows prod_emb_empty[simp]: "prod_emb M L K {} = {}" and prod_emb_Un[simp]: "prod_emb M L K (A \ B) = prod_emb M L K A \ prod_emb M L K B" and prod_emb_Int: "prod_emb M L K (A \ B) = prod_emb M L K A \ prod_emb M L K B" and prod_emb_UN[simp]: "prod_emb M L K (\i\I. F i) = (\i\I. prod_emb M L K (F i))" and prod_emb_INT[simp]: "I \ {} \ prod_emb M L K (\i\I. F i) = (\i\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) lemma prod_emb_PiE: "J \ I \ (\i. i \ J \ E i \ space (M i)) \ prod_emb I M J (\\<^sub>E i\J. E i) = (\\<^sub>E i\I. if i \ J then E i else space (M i))" by (force simp: prod_emb_def PiE_iff split_if_mem2) lemma prod_emb_PiE_same_index[simp]: "(\i. i \ I \ E i \ space (M i)) \ prod_emb I M I (Pi\<^sub>E I E) = Pi\<^sub>E I E" by (auto simp: prod_emb_def PiE_iff) lemma prod_emb_trans[simp]: "J \ K \ K \ L \ prod_emb L M K (prod_emb K M J X) = prod_emb L M J X" by (auto simp add: Int_absorb1 prod_emb_def PiE_def) lemma prod_emb_Pi: assumes "X \ (\ j\J. sets (M j))" "J \ K" shows "prod_emb K M J (Pi\<^sub>E J X) = (\\<^sub>E i\K. if i \ J then X i else space (M i))" using assms sets.space_closed by (auto simp: prod_emb_def PiE_iff split: split_if_asm) blast+ lemma prod_emb_id: "B \ (\\<^sub>E i\L. space (M i)) \ prod_emb L M L B = B" by (auto simp: prod_emb_def subset_eq extensional_restrict) lemma prod_emb_mono: "F \ G \ prod_emb A M B F \ prod_emb A M B G" by (auto simp: prod_emb_def) definition PiM :: "'i set \ ('i \ 'a measure) \ ('i \ 'a) measure" where "PiM I M = extend_measure (\\<^sub>E i\I. space (M i)) {(J, X). (J \ {} \ I = {}) \ finite J \ J \ I \ X \ (\ j\J. sets (M j))} (\(J, X). prod_emb I M J (\\<^sub>E j\J. X j)) (\(J, X). \j\J \ {i\I. emeasure (M i) (space (M i)) \ 1}. if j \ J then emeasure (M j) (X j) else emeasure (M j) (space (M j)))" definition prod_algebra :: "'i set \ ('i \ 'a measure) \ ('i \ 'a) set set" where "prod_algebra I M = (\(J, X). prod_emb I M J (\\<^sub>E j\J. X j)) ` {(J, X). (J \ {} \ I = {}) \ finite J \ J \ I \ X \ (\ j\J. sets (M j))}" abbreviation "Pi\<^sub>M I M \ PiM I M" syntax "_PiM" :: "pttrn \ 'i set \ 'a measure \ ('i => 'a) measure" ("(3PIM _:_./ _)" 10) syntax (xsymbols) "_PiM" :: "pttrn \ 'i set \ 'a measure \ ('i => 'a) measure" ("(3\\<^sub>M _\_./ _)" 10) syntax (HTML output) "_PiM" :: "pttrn \ 'i set \ 'a measure \ ('i => 'a) measure" ("(3\\<^sub>M _\_./ _)" 10) translations "PIM x:I. M" == "CONST PiM I (%x. M)" lemma prod_algebra_sets_into_space: "prod_algebra I M \ Pow (\\<^sub>E i\I. space (M i))" by (auto simp: prod_emb_def prod_algebra_def) lemma prod_algebra_eq_finite: assumes I: "finite I" shows "prod_algebra I M = {(\\<^sub>E i\I. X i) |X. X \ (\ j\I. sets (M j))}" (is "?L = ?R") proof (intro iffI set_eqI) fix A assume "A \ ?L" then obtain J E where J: "J \ {} \ I = {}" "finite J" "J \ I" "\i\J. E i \ sets (M i)" and A: "A = prod_emb I M J (PIE j:J. E j)" by (auto simp: prod_algebra_def) let ?A = "\\<^sub>E i\I. if i \ J then E i else space (M i)" have A: "A = ?A" unfolding A using J by (intro prod_emb_PiE sets.sets_into_space) auto show "A \ ?R" unfolding A using J sets.top by (intro CollectI exI[of _ "\i. if i \ J then E i else space (M i)"]) simp next fix A assume "A \ ?R" then obtain X where A: "A = (\\<^sub>E i\I. X i)" and X: "X \ (\ j\I. sets (M j))" by auto then have A: "A = prod_emb I M I (\\<^sub>E i\I. X i)" by (simp add: prod_emb_PiE_same_index[OF sets.sets_into_space] Pi_iff) from X I show "A \ ?L" unfolding A by (auto simp: prod_algebra_def) qed lemma prod_algebraI: "finite J \ (J \ {} \ I = {}) \ J \ I \ (\i. i \ J \ E i \ sets (M i)) \ prod_emb I M J (PIE j:J. E j) \ prod_algebra I M" by (auto simp: prod_algebra_def) lemma prod_algebraI_finite: "finite I \ (\i\I. E i \ sets (M i)) \ (Pi\<^sub>E I E) \ prod_algebra I M" using prod_algebraI[of I I E M] prod_emb_PiE_same_index[of I E M, OF sets.sets_into_space] by simp lemma Int_stable_PiE: "Int_stable {Pi\<^sub>E J E | E. \i\I. E i \ sets (M i)}" proof (safe intro!: Int_stableI) fix E F assume "\i\I. E i \ sets (M i)" "\i\I. F i \ sets (M i)" then show "\G. Pi\<^sub>E J E \ Pi\<^sub>E J F = Pi\<^sub>E J G \ (\i\I. G i \ sets (M i))" by (auto intro!: exI[of _ "\i. E i \ F i"] simp: PiE_Int) qed lemma prod_algebraE: assumes A: "A \ prod_algebra I M" obtains J E where "A = prod_emb I M J (PIE j:J. E j)" "finite J" "J \ {} \ I = {}" "J \ I" "\i. i \ J \ E i \ sets (M i)" using A by (auto simp: prod_algebra_def) lemma prod_algebraE_all: assumes A: "A \ prod_algebra I M" obtains E where "A = Pi\<^sub>E I E" "E \ (\ i\I. sets (M i))" proof - from A obtain E J where A: "A = prod_emb I M J (Pi\<^sub>E J E)" and J: "J \ I" and E: "E \ (\ i\J. sets (M i))" by (auto simp: prod_algebra_def) from E have "\i. i \ J \ E i \ space (M i)" using sets.sets_into_space by auto then have "A = (\\<^sub>E i\I. if i\J then E i else space (M i))" using A J by (auto simp: prod_emb_PiE) moreover have "(\i. if i\J then E i else space (M i)) \ (\ i\I. sets (M i))" using sets.top E by auto ultimately show ?thesis using that by auto qed lemma Int_stable_prod_algebra: "Int_stable (prod_algebra I M)" proof (unfold Int_stable_def, safe) fix A assume "A \ prod_algebra I M" from prod_algebraE[OF this] guess J E . note A = this fix B assume "B \ prod_algebra I M" from prod_algebraE[OF this] guess K F . note B = this have "A \ B = prod_emb I M (J \ K) (\\<^sub>E i\J \ K. (if i \ J then E i else space (M i)) \ (if i \ K then F i else space (M i)))" unfolding A B using A(2,3,4) A(5)[THEN sets.sets_into_space] B(2,3,4) B(5)[THEN sets.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 "\ \ prod_algebra I M" using A B by (auto intro!: prod_algebraI) finally show "A \ B \ prod_algebra I M" . qed lemma prod_algebra_mono: assumes space: "\i. i \ I \ space (E i) = space (F i)" assumes sets: "\i. i \ I \ sets (E i) \ sets (F i)" shows "prod_algebra I E \ prod_algebra I F" proof fix A assume "A \ prod_algebra I E" then obtain J G where J: "J \ {} \ I = {}" "finite J" "J \ I" and A: "A = prod_emb I E J (\\<^sub>E i\J. G i)" and G: "\i. i \ J \ G i \ sets (E i)" by (auto simp: prod_algebra_def) moreover from space have "(\\<^sub>E i\I. space (E i)) = (\\<^sub>E i\I. space (F i))" by (rule PiE_cong) with A have "A = prod_emb I F J (\\<^sub>E i\J. G i)" by (simp add: prod_emb_def) moreover from sets G J have "\i. i \ J \ G i \ sets (F i)" by auto ultimately show "A \ 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 prod_algebra_cong: assumes "I = J" and sets: "(\i. i \ I \ sets (M i) = sets (N i))" shows "prod_algebra I M = prod_algebra J N" proof - have space: "\i. i \ I \ space (M i) = space (N i)" using sets_eq_imp_space_eq[OF sets] by auto with sets show ?thesis unfolding `I = J` by (intro antisym prod_algebra_mono) auto qed lemma space_in_prod_algebra: "(\\<^sub>E i\I. space (M i)) \ prod_algebra I M" proof cases assume "I = {}" then show ?thesis by (auto simp add: prod_algebra_def image_iff prod_emb_def) next assume "I \ {}" then obtain i where "i \ I" by auto then have "(\\<^sub>E i\I. space (M i)) = prod_emb I M {i} (\\<^sub>E i\{i}. space (M i))" by (auto simp: prod_emb_def) also have "\ \ prod_algebra I M" using `i \ I` by (intro prod_algebraI) auto finally show ?thesis . qed lemma space_PiM: "space (\\<^sub>M i\I. M i) = (\\<^sub>E i\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 (\\<^sub>M i\I. M i) = sigma_sets (\\<^sub>E i\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 sets_PiM_single: "sets (PiM I M) = sigma_sets (\\<^sub>E i\I. space (M i)) {{f\\\<^sub>E i\I. space (M i). f i \ A} | i A. i \ I \ A \ sets (M i)}" (is "_ = sigma_sets ?\ ?R") unfolding sets_PiM proof (rule sigma_sets_eqI) interpret R: sigma_algebra ?\ "sigma_sets ?\ ?R" by (rule sigma_algebra_sigma_sets) auto fix A assume "A \ prod_algebra I M" from prod_algebraE[OF this] guess J X . note X = this show "A \ sigma_sets ?\ ?R" proof cases assume "I = {}" with X have "A = {\x. undefined}" by (auto simp: prod_emb_def) with `I = {}` show ?thesis by (auto intro!: sigma_sets_top) next assume "I \ {}" with X have "A = (\j\J. {f\(\\<^sub>E i\I. space (M i)). f j \ X j})" by (auto simp: prod_emb_def) also have "\ \ sigma_sets ?\ ?R" using X `I \ {}` by (intro R.finite_INT sigma_sets.Basic) auto finally show "A \ sigma_sets ?\ ?R" . qed next fix A assume "A \ ?R" then obtain i B where A: "A = {f\\\<^sub>E i\I. space (M i). f i \ B}" "i \ I" "B \ sets (M i)" by auto then have "A = prod_emb I M {i} (\\<^sub>E i\{i}. B)" by (auto simp: prod_emb_def) also have "\ \ sigma_sets ?\ (prod_algebra I M)" using A by (intro sigma_sets.Basic prod_algebraI) auto finally show "A \ sigma_sets ?\ (prod_algebra I M)" . qed lemma sets_PiM_I: assumes "finite J" "J \ I" "\i\J. E i \ sets (M i)" shows "prod_emb I M J (PIE j:J. E j) \ 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 \ {}" with assms show ?thesis by (force simp add: sets_PiM prod_algebra_def) qed lemma measurable_PiM: assumes space: "f \ space N \ (\\<^sub>E i\I. space (M i))" assumes sets: "\X J. J \ {} \ I = {} \ finite J \ J \ I \ (\i. i \ J \ X i \ sets (M i)) \ f -` prod_emb I M J (Pi\<^sub>E J X) \ space N \ sets N" shows "f \ measurable N (PiM I M)" using sets_PiM prod_algebra_sets_into_space space proof (rule measurable_sigma_sets) fix A assume "A \ prod_algebra I M" from prod_algebraE[OF this] guess J X . with sets[of J X] show "f -` A \ space N \ sets N" by auto qed lemma measurable_PiM_Collect: assumes space: "f \ space N \ (\\<^sub>E i\I. space (M i))" assumes sets: "\X J. J \ {} \ I = {} \ finite J \ J \ I \ (\i. i \ J \ X i \ sets (M i)) \ {\\space N. \i\J. f \ i \ X i} \ sets N" shows "f \ measurable N (PiM I M)" using sets_PiM prod_algebra_sets_into_space space proof (rule measurable_sigma_sets) fix A assume "A \ prod_algebra I M" from prod_algebraE[OF this] guess J X . note X = this then have "f -` A \ space N = {\ \ space N. \i\J. f \ i \ X i}" using space by (auto simp: prod_emb_def del: PiE_I) also have "\ \ sets N" using X(3,2,4,5) by (rule sets) finally show "f -` A \ space N \ sets N" . qed lemma measurable_PiM_single: assumes space: "f \ space N \ (\\<^sub>E i\I. space (M i))" assumes sets: "\A i. i \ I \ A \ sets (M i) \ {\ \ space N. f \ i \ A} \ sets N" shows "f \ measurable N (PiM I M)" using sets_PiM_single proof (rule measurable_sigma_sets) fix A assume "A \ {{f \ \\<^sub>E i\I. space (M i). f i \ A} |i A. i \ I \ A \ sets (M i)}" then obtain B i where "A = {f \ \\<^sub>E i\I. space (M i). f i \ B}" and B: "i \ I" "B \ sets (M i)" by auto with space have "f -` A \ space N = {\ \ space N. f \ i \ B}" by auto also have "\ \ sets N" using B by (rule sets) finally show "f -` A \ space N \ sets N" . qed (auto simp: space) lemma measurable_PiM_single': assumes f: "\i. i \ I \ f i \ measurable N (M i)" and "(\\ i. f i \) \ space N \ (\\<^sub>E i\I. space (M i))" shows "(\\ i. f i \) \ measurable N (Pi\<^sub>M I M)" proof (rule measurable_PiM_single) fix A i assume A: "i \ I" "A \ sets (M i)" then have "{\ \ space N. f i \ \ A} = f i -` A \ space N" by auto then show "{\ \ space N. f i \ \ A} \ sets N" using A f by (auto intro!: measurable_sets) qed fact lemma sets_PiM_I_finite[measurable]: assumes "finite I" and sets: "(\i. i \ I \ E i \ sets (M i))" shows "(PIE j:I. E j) \ sets (PIM i:I. M i)" using sets_PiM_I[of I I E M] sets.sets_into_space[OF sets] `finite I` sets by auto lemma measurable_component_singleton: assumes "i \ I" shows "(\x. x i) \ measurable (Pi\<^sub>M I M) (M i)" proof (unfold measurable_def, intro CollectI conjI ballI) fix A assume "A \ sets (M i)" then have "(\x. x i) -` A \ space (Pi\<^sub>M I M) = prod_emb I M {i} (\\<^sub>E j\{i}. A)" using sets.sets_into_space `i \ I` by (fastforce dest: Pi_mem simp: prod_emb_def space_PiM split: split_if_asm) then show "(\x. x i) -` A \ space (Pi\<^sub>M I M) \ sets (Pi\<^sub>M I M)" using `A \ sets (M i)` `i \ I` by (auto intro!: sets_PiM_I) qed (insert `i \ I`, auto simp: space_PiM) lemma measurable_component_singleton'[measurable_app]: assumes f: "f \ measurable N (Pi\<^sub>M I M)" assumes i: "i \ I" shows "(\x. (f x) i) \ measurable N (M i)" using measurable_compose[OF f measurable_component_singleton, OF i] . lemma measurable_PiM_component_rev[measurable (raw)]: "i \ I \ f \ measurable (M i) N \ (\x. f (x i)) \ measurable (PiM I M) N" by simp lemma measurable_case_nat[measurable (raw)]: assumes [measurable (raw)]: "i = 0 \ f \ measurable M N" "\j. i = Suc j \ (\x. g x j) \ measurable M N" shows "(\x. case_nat (f x) (g x) i) \ measurable M N" by (cases i) simp_all lemma measurable_case_nat'[measurable (raw)]: assumes fg[measurable]: "f \ measurable N M" "g \ measurable N (\\<^sub>M i\UNIV. M)" shows "(\x. case_nat (f x) (g x)) \ measurable N (\\<^sub>M i\UNIV. M)" using fg[THEN measurable_space] by (auto intro!: measurable_PiM_single' simp add: space_PiM PiE_iff split: nat.split) lemma measurable_add_dim[measurable]: "(\(f, y). f(i := y)) \ measurable (Pi\<^sub>M I M \\<^sub>M M i) (Pi\<^sub>M (insert i I) M)" (is "?f \ measurable ?P ?I") proof (rule measurable_PiM_single) fix j A assume j: "j \ insert i I" and A: "A \ sets (M j)" have "{\ \ space ?P. (\(f, x). fun_upd f i x) \ j \ A} = (if j = i then space (Pi\<^sub>M I M) \ A else ((\x. x j) \ fst) -` A \ space ?P)" using sets.sets_into_space[OF A] by (auto simp add: space_pair_measure space_PiM) also have "\ \ sets ?P" using A j by (auto intro!: measurable_sets[OF measurable_comp, OF _ measurable_component_singleton]) finally show "{\ \ space ?P. case_prod (\f. fun_upd f i) \ j \ A} \ sets ?P" . qed (auto simp: space_pair_measure space_PiM PiE_def) lemma measurable_component_update: "x \ space (Pi\<^sub>M I M) \ i \ I \ (\v. x(i := v)) \ measurable (M i) (Pi\<^sub>M (insert i I) M)" by simp lemma measurable_merge[measurable]: "merge I J \ measurable (Pi\<^sub>M I M \\<^sub>M Pi\<^sub>M J M) (Pi\<^sub>M (I \ J) M)" (is "?f \ measurable ?P ?U") proof (rule measurable_PiM_single) fix i A assume A: "A \ sets (M i)" "i \ I \ J" then have "{\ \ space ?P. merge I J \ i \ A} = (if i \ I then ((\x. x i) \ fst) -` A \ space ?P else ((\x. x i) \ snd) -` A \ space ?P)" by (auto simp: merge_def) also have "\ \ sets ?P" using A by (auto intro!: measurable_sets[OF measurable_comp, OF _ measurable_component_singleton]) finally show "{\ \ space ?P. merge I J \ i \ A} \ sets ?P" . qed (auto simp: space_pair_measure space_PiM PiE_iff merge_def extensional_def) lemma measurable_restrict[measurable (raw)]: assumes X: "\i. i \ I \ X i \ measurable N (M i)" shows "(\x. \i\I. X i x) \ measurable N (Pi\<^sub>M I M)" proof (rule measurable_PiM_single) fix A i assume A: "i \ I" "A \ sets (M i)" then have "{\ \ space N. (\i\I. X i \) i \ A} = X i -` A \ space N" by auto then show "{\ \ space N. (\i\I. X i \) i \ A} \ sets N" using A X by (auto intro!: measurable_sets) qed (insert X, auto simp add: PiE_def dest: measurable_space) lemma measurable_abs_UNIV: "(\n. (\\. f n \) \ measurable M (N n)) \ (\\ n. f n \) \ measurable M (PiM UNIV N)" by (intro measurable_PiM_single) (auto dest: measurable_space) lemma measurable_restrict_subset: "J \ L \ (\f. restrict f J) \ measurable (Pi\<^sub>M L M) (Pi\<^sub>M J M)" by (intro measurable_restrict measurable_component_singleton) auto lemma measurable_prod_emb[intro, simp]: "J \ L \ X \ sets (Pi\<^sub>M J M) \ prod_emb L M J X \ sets (Pi\<^sub>M L M)" unfolding prod_emb_def space_PiM[symmetric] by (auto intro!: measurable_sets measurable_restrict measurable_component_singleton) lemma sets_in_Pi_aux: "finite I \ (\j. j \ I \ {x\space (M j). x \ F j} \ sets (M j)) \ {x\space (PiM I M). x \ Pi I F} \ sets (PiM I M)" by (simp add: subset_eq Pi_iff) lemma sets_in_Pi[measurable (raw)]: "finite I \ f \ measurable N (PiM I M) \ (\j. j \ I \ {x\space (M j). x \ F j} \ sets (M j)) \ Measurable.pred N (\x. f x \ Pi I F)" unfolding pred_def by (rule measurable_sets_Collect[of f N "PiM I M", OF _ sets_in_Pi_aux]) auto lemma sets_in_extensional_aux: "{x\space (PiM I M). x \ extensional I} \ sets (PiM I M)" proof - have "{x\space (PiM I M). x \ extensional I} = space (PiM I M)" by (auto simp add: extensional_def space_PiM) then show ?thesis by simp qed lemma sets_in_extensional[measurable (raw)]: "f \ measurable N (PiM I M) \ Measurable.pred N (\x. f x \ extensional I)" unfolding pred_def by (rule measurable_sets_Collect[of f N "PiM I M", OF _ sets_in_extensional_aux]) auto locale product_sigma_finite = fixes M :: "'i \ 'a measure" assumes sigma_finite_measures: "\i. sigma_finite_measure (M i)" sublocale product_sigma_finite \ M: sigma_finite_measure "M i" for i by (rule sigma_finite_measures) locale finite_product_sigma_finite = product_sigma_finite M for M :: "'i \ 'a measure" + fixes I :: "'i set" assumes finite_index: "finite I" lemma (in finite_product_sigma_finite) sigma_finite_pairs: "\F::'i \ nat \ 'a set. (\i\I. range (F i) \ sets (M i)) \ (\k. \i\I. emeasure (M i) (F i k) \ \) \ incseq (\k. \\<^sub>E i\I. F i k) \ (\k. \\<^sub>E i\I. F i k) = space (PiM I M)" proof - have "\i::'i. \F::nat \ 'a set. range F \ sets (M i) \ incseq F \ (\i. F i) = space (M i) \ (\k. emeasure (M i) (F k) \ \)" using M.sigma_finite_incseq by metis from choice[OF this] guess F :: "'i \ nat \ 'a set" .. then have F: "\i. range (F i) \ sets (M i)" "\i. incseq (F i)" "\i. (\j. F i j) = space (M i)" "\i k. emeasure (M i) (F i k) \ \" by auto let ?F = "\k. \\<^sub>E i\I. F i k" 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) \ sets (M i)" by fact next fix i k show "emeasure (M i) (F i k) \ \" by fact next fix x assume "x \ (\i. ?F i)" with F(1) show "x \ space (PiM I M)" by (auto simp: PiE_def dest!: sets.sets_into_space) next fix f assume "f \ space (PiM I M)" with Pi_UN[OF finite_index, of "\k i. F i k"] F show "f \ (\i. ?F i)" by (auto simp: incseq_def PiE_def) next fix i show "?F i \ ?F (Suc i)" using `\i. incseq (F i)`[THEN incseq_SucD] by auto qed qed lemma shows space_PiM_empty: "space (Pi\<^sub>M {} M) = {\k. undefined}" and sets_PiM_empty: "sets (Pi\<^sub>M {} M) = { {}, {\k. undefined} }" by (simp_all add: space_PiM sets_PiM_single image_constant sigma_sets_empty_eq) lemma emeasure_PiM_empty[simp]: "emeasure (PiM {} M) {\_. undefined} = 1" proof - let ?\ = "\A. if A = {} then 0 else (1::ereal)" have "emeasure (Pi\<^sub>M {} M) (prod_emb {} M {} (\\<^sub>E i\{}. {})) = 1" proof (subst emeasure_extend_measure_Pair[OF PiM_def]) show "positive (PiM {} M) ?\" by (auto simp: positive_def) show "countably_additive (PiM {} M) ?\" by (rule sets.countably_additiveI_finite) (auto simp: additive_def positive_def sets_PiM_empty space_PiM_empty intro!: ) qed (auto simp: prod_emb_def) also have "(prod_emb {} M {} (\\<^sub>E i\{}. {})) = {\_. undefined}" by (auto simp: prod_emb_def) finally show ?thesis by simp qed lemma PiM_empty: "PiM {} M = count_space {\_. undefined}" by (rule measure_eqI) (auto simp add: sets_PiM_empty one_ereal_def) lemma (in product_sigma_finite) emeasure_PiM: "finite I \ (\i. i\I \ A i \ sets (M i)) \ emeasure (PiM I M) (Pi\<^sub>E I A) = (\i\I. emeasure (M i) (A i))" proof (induct I arbitrary: A rule: finite_induct) 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 let ?h = "(\(f, y). f(i := y))" let ?P = "distr (Pi\<^sub>M I M \\<^sub>M M i) (Pi\<^sub>M (insert i I) M) ?h" let ?\ = "emeasure ?P" let ?I = "{j \ insert i I. emeasure (M j) (space (M j)) \ 1}" let ?f = "\J E j. if j \ J then emeasure (M j) (E j) else emeasure (M j) (space (M j))" have "emeasure (Pi\<^sub>M (insert i I) M) (prod_emb (insert i I) M (insert i I) (Pi\<^sub>E (insert i I) A)) = (\i\insert i I. emeasure (M i) (A i))" proof (subst emeasure_extend_measure_Pair[OF PiM_def]) fix J E assume "(J \ {} \ insert i I = {}) \ finite J \ J \ insert i I \ E \ (\ j\J. sets (M j))" then have J: "J \ {}" "finite J" "J \ insert i I" and E: "\j\J. E j \ sets (M j)" by auto let ?p = "prod_emb (insert i I) M J (Pi\<^sub>E J E)" let ?p' = "prod_emb I M (J - {i}) (\\<^sub>E j\J-{i}. E j)" have "?\ ?p = emeasure (Pi\<^sub>M I M \\<^sub>M (M i)) (?h -` ?p \ space (Pi\<^sub>M I M \\<^sub>M M i))" by (intro emeasure_distr measurable_add_dim sets_PiM_I) fact+ also have "?h -` ?p \ space (Pi\<^sub>M I M \\<^sub>M M i) = ?p' \ (if i \ J then E i else space (M i))" using J E[rule_format, THEN sets.sets_into_space] by (force simp: space_pair_measure space_PiM prod_emb_iff PiE_def Pi_iff split: split_if_asm) also have "emeasure (Pi\<^sub>M I M \\<^sub>M (M i)) (?p' \ (if i \ J then E i else space (M i))) = emeasure (Pi\<^sub>M I M) ?p' * emeasure (M i) (if i \ 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' = (\\<^sub>E j\I. if j \ J-{i} then E j else space (M j))" using J E[rule_format, THEN sets.sets_into_space] by (auto simp: prod_emb_iff PiE_def Pi_iff split: split_if_asm) blast+ also have "emeasure (Pi\<^sub>M I M) (\\<^sub>E j\I. if j \ J-{i} then E j else space (M j)) = (\ j\I. if j \ 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 "(\j\I. if j \ J - {i} then emeasure (M j) (E j) else emeasure (M j) (space (M j))) * emeasure (M i) (if i \ J then E i else space (M i)) = (\j\insert i I. ?f J E j)" using insert by (auto simp: mult.commute intro!: arg_cong2[where f="op *"] setprod.cong) also have "\ = (\j\J \ ?I. ?f J E j)" using insert(1,2) J E by (intro setprod.mono_neutral_right) auto finally show "?\ ?p = \" . show "prod_emb (insert i I) M J (Pi\<^sub>E J E) \ Pow (\\<^sub>E i\insert i I. space (M i))" using J E[rule_format, THEN sets.sets_into_space] by (auto simp: prod_emb_iff PiE_def) next show "positive (sets (Pi\<^sub>M (insert i I) M)) ?\" "countably_additive (sets (Pi\<^sub>M (insert i I) M)) ?\" using emeasure_positive[of ?P] emeasure_countably_additive[of ?P] by simp_all next show "(insert i I \ {} \ insert i I = {}) \ finite (insert i I) \ insert i I \ insert i I \ A \ (\ j\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.sets_into_space) qed simp 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 obtain F where F: "\j. countable (F j)" "\j f. f \ F j \ f \ sets (M j)" "\j f. f \ F j \ emeasure (M j) f \ \" and in_space: "\j. space (M j) = (\F j)" using sigma_finite_countable by (metis subset_eq) moreover have "(\(PiE I ` PiE I F)) = space (Pi\<^sub>M I M)" using in_space by (auto simp: space_PiM PiE_iff intro!: PiE_choice[THEN iffD2]) ultimately show "\A. countable A \ A \ sets (Pi\<^sub>M I M) \ \A = space (Pi\<^sub>M I M) \ (\a\A. emeasure (Pi\<^sub>M I M) a \ \)" by (intro exI[of _ "PiE I ` PiE I F"]) (auto intro!: countable_PiE sets_PiM_I_finite simp: PiE_iff emeasure_PiM finite_index setprod_PInf emeasure_nonneg) qed sublocale finite_product_sigma_finite \ sigma_finite_measure "Pi\<^sub>M I M" using sigma_finite[OF finite_index] . lemma (in finite_product_sigma_finite) measure_times: "(\i. i \ I \ A i \ sets (M i)) \ emeasure (Pi\<^sub>M I M) (Pi\<^sub>E I A) = (\i\I. emeasure (M i) (A i))" using emeasure_PiM[OF finite_index] by auto lemma (in product_sigma_finite) nn_integral_empty: assumes pos: "0 \ f (\k. undefined)" shows "integral\<^sup>N (Pi\<^sub>M {} M) f = f (\k. undefined)" proof - interpret finite_product_sigma_finite M "{}" by default (fact finite.emptyI) have "\A. emeasure (Pi\<^sub>M {} M) (Pi\<^sub>E {} A) = 1" using assms by (subst measure_times) auto then show ?thesis unfolding nn_integral_def simple_function_def simple_integral_def[abs_def] proof (simp add: space_PiM_empty sets_PiM_empty, intro antisym) show "f (\k. undefined) \ (SUP f:{g. g \ max 0 \ f}. f (\k. undefined))" by (intro SUP_upper) (auto simp: le_fun_def split: split_max) show "(SUP f:{g. g \ max 0 \ f}. f (\k. undefined)) \ f (\k. undefined)" using pos by (intro SUP_least) (auto simp: le_fun_def simp: max_def split: split_if_asm) qed qed lemma (in product_sigma_finite) distr_merge: assumes IJ[simp]: "I \ J = {}" and fin: "finite I" "finite J" shows "distr (Pi\<^sub>M I M \\<^sub>M Pi\<^sub>M J M) (Pi\<^sub>M (I \ J) M) (merge I J) = Pi\<^sub>M (I \ 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 \ J)" using fin by auto interpret IJ: finite_product_sigma_finite M "I \ J" by default fact interpret P: pair_sigma_finite "Pi\<^sub>M I M" "Pi\<^sub>M J M" by default let ?g = "merge I J" from IJ.sigma_finite_pairs obtain F where F: "\i. i\ I \ J \ range (F i) \ sets (M i)" "incseq (\k. \\<^sub>E i\I \ J. F i k)" "(\k. \\<^sub>E i\I \ J. F i k) = space ?P" "\k. \i\I\J. emeasure (M i) (F i k) \ \" by auto let ?F = "\k. \\<^sub>E i\I \ J. F i k" show ?thesis proof (rule measure_eqI_generator_eq[symmetric]) show "Int_stable (prod_algebra (I \ J) M)" by (rule Int_stable_prod_algebra) show "prod_algebra (I \ J) M \ Pow (\\<^sub>E i \ I \ J. space (M i))" by (rule prod_algebra_sets_into_space) show "sets ?P = sigma_sets (\\<^sub>E i\I \ J. space (M i)) (prod_algebra (I \ J) M)" by (rule sets_PiM) then show "sets ?D = sigma_sets (\\<^sub>E i\I \ J. space (M i)) (prod_algebra (I \ J) M)" by simp show "range ?F \ prod_algebra (I \ J) M" using F using fin by (auto simp: prod_algebra_eq_finite) show "(\i. \\<^sub>E ia\I \ J. F ia i) = (\\<^sub>E i\I \ J. space (M i))" using F(3) by (simp add: space_PiM) next fix k from F `finite I` setprod_PInf[of "I \ J", OF emeasure_nonneg, of M] show "emeasure ?P (?F k) \ \" by (subst IJ.measure_times) auto next fix A assume A: "A \ prod_algebra (I \ J) M" with fin obtain F where A_eq: "A = (Pi\<^sub>E (I \ J) F)" and F: "\i\J. F i \ sets (M i)" "\i\I. F i \ sets (M i)" by (auto simp add: prod_algebra_eq_finite) let ?B = "Pi\<^sub>M I M \\<^sub>M Pi\<^sub>M J M" let ?X = "?g -` A \ space ?B" have "Pi\<^sub>E I F \ space (Pi\<^sub>M I M)" "Pi\<^sub>E J F \ space (Pi\<^sub>M J M)" using F[rule_format, THEN sets.sets_into_space] by (force simp: space_PiM)+ then have X: "?X = (Pi\<^sub>E I F \ Pi\<^sub>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 = (\i\I. emeasure (M i) (F i)) * (\i\J. emeasure (M i) (F i))" using `finite J` `finite I` F unfolding X by (simp add: J.emeasure_pair_measure_Times I.measure_times J.measure_times) also have "\ = (\i\I \ J. emeasure (M i) (F i))" using `finite J` `finite I` `I \ J = {}` by (simp add: setprod.union_inter_neutral) also have "\ = emeasure ?P (Pi\<^sub>E (I \ J) F)" using `finite J` `finite I` F unfolding A by (intro IJ.measure_times[symmetric]) auto finally show "emeasure ?P A = emeasure ?D A" using A_eq by simp qed qed lemma (in product_sigma_finite) product_nn_integral_fold: assumes IJ: "I \ J = {}" "finite I" "finite J" and f: "f \ borel_measurable (Pi\<^sub>M (I \ J) M)" shows "integral\<^sup>N (Pi\<^sub>M (I \ J) M) f = (\\<^sup>+ x. (\\<^sup>+ y. f (merge I J (x, y)) \(Pi\<^sub>M J M)) \(Pi\<^sub>M I M))" proof - 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\<^sub>M I M" "Pi\<^sub>M J M" by default have P_borel: "(\x. f (merge I J x)) \ borel_measurable (Pi\<^sub>M I M \\<^sub>M Pi\<^sub>M J M)" using measurable_comp[OF measurable_merge f] by (simp add: comp_def) show ?thesis apply (subst distr_merge[OF IJ, symmetric]) apply (subst nn_integral_distr[OF measurable_merge f]) apply (subst J.nn_integral_fst[symmetric, OF P_borel]) apply simp done qed lemma (in product_sigma_finite) distr_singleton: "distr (Pi\<^sub>M {i} M) (M i) (\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 assume A: "A \ sets (M i)" then have "(\x. x i) -` A \ space (Pi\<^sub>M {i} M) = (\\<^sub>E i\{i}. A)" using sets.sets_into_space by (auto simp: space_PiM) then show "emeasure (M i) A = emeasure ?D A" using A I.measure_times[of "\_. A"] by (simp add: emeasure_distr measurable_component_singleton) qed simp lemma (in product_sigma_finite) product_nn_integral_singleton: assumes f: "f \ borel_measurable (M i)" shows "integral\<^sup>N (Pi\<^sub>M {i} M) (\x. f (x i)) = integral\<^sup>N (M i) f" proof - interpret I: finite_product_sigma_finite M "{i}" by default simp from f show ?thesis apply (subst distr_singleton[symmetric]) apply (subst nn_integral_distr[OF measurable_component_singleton]) apply simp_all done qed lemma (in product_sigma_finite) product_nn_integral_insert: assumes I[simp]: "finite I" "i \ I" and f: "f \ borel_measurable (Pi\<^sub>M (insert i I) M)" shows "integral\<^sup>N (Pi\<^sub>M (insert i I) M) f = (\\<^sup>+ x. (\\<^sup>+ y. f (x(i := y)) \(M i)) \(Pi\<^sub>M I M))" proof - interpret I: finite_product_sigma_finite M I by default auto interpret i: finite_product_sigma_finite M "{i}" by default auto have IJ: "I \ {i} = {}" and insert: "I \ {i} = insert i I" using f by auto show ?thesis unfolding product_nn_integral_fold[OF IJ, unfolded insert, OF I(1) i.finite_index f] proof (rule nn_integral_cong, subst product_nn_integral_singleton[symmetric]) fix x assume x: "x \ space (Pi\<^sub>M I M)" let ?f = "\y. f (x(i := y))" show "?f \ borel_measurable (M i)" using measurable_comp[OF measurable_component_update f, OF x `i \ I`] unfolding comp_def . show "(\\<^sup>+ y. f (merge I {i} (x, y)) \Pi\<^sub>M {i} M) = (\\<^sup>+ y. f (x(i := y i)) \Pi\<^sub>M {i} M)" using x by (auto intro!: nn_integral_cong arg_cong[where f=f] simp add: space_PiM extensional_def PiE_def) qed qed lemma (in product_sigma_finite) product_nn_integral_setprod: fixes f :: "'i \ 'a \ ereal" assumes "finite I" and borel: "\i. i \ I \ f i \ borel_measurable (M i)" and pos: "\i x. i \ I \ 0 \ f i x" shows "(\\<^sup>+ x. (\i\I. f i (x i)) \Pi\<^sub>M I M) = (\i\I. integral\<^sup>N (M i) (f i))" using assms proof induct case (insert i I) note `finite I`[intro, simp] interpret I: finite_product_sigma_finite M I by default auto have *: "\x y. (\j\I. f j (if j = i then y else x j)) = (\j\I. f j (x j))" using insert by (auto intro!: setprod.cong) have prod: "\J. J \ insert i I \ (\x. (\i\J. f i (x i))) \ borel_measurable (Pi\<^sub>M J M)" using sets.sets_into_space insert by (intro borel_measurable_ereal_setprod measurable_comp[OF measurable_component_singleton, unfolded comp_def]) auto then show ?case apply (simp add: product_nn_integral_insert[OF insert(1,2) prod]) apply (simp add: insert(2-) * pos borel setprod_ereal_pos nn_integral_multc) apply (subst nn_integral_cmult) apply (auto simp add: pos borel insert(2-) setprod_ereal_pos nn_integral_nonneg) done qed (simp add: space_PiM) lemma (in product_sigma_finite) distr_component: "distr (M i) (Pi\<^sub>M {i} M) (\x. \i\{i}. x) = Pi\<^sub>M {i} M" (is "?D = ?P") proof (intro measure_eqI[symmetric]) interpret I: finite_product_sigma_finite M "{i}" by default simp have eq: "\x. x \ extensional {i} \ (\j\{i}. x i) = x" by (auto simp: extensional_def restrict_def) fix A assume A: "A \ sets ?P" then have "emeasure ?P A = (\\<^sup>+x. indicator A x \?P)" by simp also have "\ = (\\<^sup>+x. indicator ((\x. \i\{i}. x) -` A \ space (M i)) (x i) \PiM {i} M)" by (intro nn_integral_cong) (auto simp: space_PiM indicator_def PiE_def eq) also have "\ = emeasure ?D A" using A by (simp add: product_nn_integral_singleton emeasure_distr) finally show "emeasure (Pi\<^sub>M {i} M) A = emeasure ?D A" . qed simp lemma (in product_sigma_finite) assumes IJ: "I \ J = {}" "finite I" "finite J" and A: "A \ sets (Pi\<^sub>M (I \ J) M)" shows emeasure_fold_integral: "emeasure (Pi\<^sub>M (I \ J) M) A = (\\<^sup>+x. emeasure (Pi\<^sub>M J M) ((\y. merge I J (x, y)) -` A \ space (Pi\<^sub>M J M)) \Pi\<^sub>M I M)" (is ?I) and emeasure_fold_measurable: "(\x. emeasure (Pi\<^sub>M J M) ((\y. merge I J (x, y)) -` A \ space (Pi\<^sub>M J M))) \ borel_measurable (Pi\<^sub>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\<^sub>M I M" "Pi\<^sub>M J M" .. have merge: "merge I J -` A \ space (Pi\<^sub>M I M \\<^sub>M Pi\<^sub>M J M) \ sets (Pi\<^sub>M I M \\<^sub>M Pi\<^sub>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!: nn_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_comp comp_def space_pair_measure cong: measurable_cong) qed lemma sets_Collect_single: "i \ I \ A \ sets (M i) \ { x \ space (Pi\<^sub>M I M). x i \ A } \ sets (Pi\<^sub>M I M)" by simp lemma sigma_prod_algebra_sigma_eq_infinite: fixes E :: "'i \ 'a set set" assumes S_union: "\i. i \ I \ (\j. S i j) = space (M i)" and S_in_E: "\i. i \ I \ range (S i) \ E i" assumes E_closed: "\i. i \ I \ E i \ Pow (space (M i))" and E_generates: "\i. i \ I \ sets (M i) = sigma_sets (space (M i)) (E i)" defines "P == {{f\\\<^sub>E i\I. space (M i). f i \ A} | i A. i \ I \ A \ E i}" shows "sets (PiM I M) = sigma_sets (space (PiM I M)) P" proof let ?P = "sigma (space (Pi\<^sub>M I M)) P" have P_closed: "P \ Pow (space (Pi\<^sub>M I M))" using E_closed by (auto simp: space_PiM P_def subset_eq) then have space_P: "space ?P = (\\<^sub>E i\I. space (M i))" by (simp add: space_PiM) have "sets (PiM I M) = sigma_sets (space ?P) {{f \ \\<^sub>E i\I. space (M i). f i \ A} |i A. i \ I \ A \ sets (M i)}" using sets_PiM_single[of I M] by (simp add: space_P) also have "\ \ sets (sigma (space (PiM I M)) P)" proof (safe intro!: sets.sigma_sets_subset) fix i A assume "i \ I" and A: "A \ sets (M i)" then have "(\x. x i) \ 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 \ I` E_closed have "(\x. x i) -` A \ space ?P \ sets ?P" by (simp add: E_generates) also have "(\x. x i) -` A \ space ?P = {f \ \\<^sub>E i\I. space (M i). f i \ A}" using P_closed by (auto simp: space_PiM) finally show "\ \ sets ?P" . qed finally show "sets (PiM I M) \ sigma_sets (space (PiM I M)) P" by (simp add: P_closed) show "sigma_sets (space (PiM I M)) P \ sets (PiM I M)" unfolding P_def space_PiM[symmetric] by (intro sets.sigma_sets_subset) (auto simp: E_generates sets_Collect_single) qed lemma sigma_prod_algebra_sigma_eq: fixes E :: "'i \ 'a set set" and S :: "'i \ nat \ 'a set" assumes "finite I" assumes S_union: "\i. i \ I \ (\j. S i j) = space (M i)" and S_in_E: "\i. i \ I \ range (S i) \ E i" assumes E_closed: "\i. i \ I \ E i \ Pow (space (M i))" and E_generates: "\i. i \ I \ sets (M i) = sigma_sets (space (M i)) (E i)" defines "P == { Pi\<^sub>E I F | F. \i\I. F i \ E i }" shows "sets (PiM I M) = sigma_sets (space (PiM I M)) P" proof let ?P = "sigma (space (Pi\<^sub>M I M)) P" from `finite I`[THEN ex_bij_betw_finite_nat] guess T .. then have T: "\i. i \ I \ T i < card I" "\i. i\I \ the_inv_into I T (T i) = i" by (auto simp add: bij_betw_def set_eq_iff image_iff the_inv_into_f_f) have P_closed: "P \ Pow (space (Pi\<^sub>M I M))" using E_closed by (auto simp: space_PiM P_def subset_eq) then have space_P: "space ?P = (\\<^sub>E i\I. space (M i))" by (simp add: space_PiM) have "sets (PiM I M) = sigma_sets (space ?P) {{f \ \\<^sub>E i\I. space (M i). f i \ A} |i A. i \ I \ A \ sets (M i)}" using sets_PiM_single[of I M] by (simp add: space_P) also have "\ \ sets (sigma (space (PiM I M)) P)" proof (safe intro!: sets.sigma_sets_subset) fix i A assume "i \ I" and A: "A \ sets (M i)" have "(\x. x i) \ measurable ?P (sigma (space (M i)) (E i))" proof (subst measurable_iff_measure_of) show "E i \ Pow (space (M i))" using `i \ I` by fact from space_P `i \ I` show "(\x. x i) \ space ?P \ space (M i)" by auto show "\A\E i. (\x. x i) -` A \ space ?P \ sets ?P" proof fix A assume A: "A \ E i" then have "(\x. x i) -` A \ space ?P = (\\<^sub>E j\I. if i = j then A else space (M j))" using E_closed `i \ I` by (auto simp: space_P subset_eq split: split_if_asm) also have "\ = (\\<^sub>E j\I. \n. if i = j then A else S j n)" by (intro PiE_cong) (simp add: S_union) also have "\ = (\xs\{xs. length xs = card I}. \\<^sub>E j\I. if i = j then A else S j (xs ! T j))" using T apply (auto simp: PiE_iff bchoice_iff) apply (rule_tac x="map (\n. f (the_inv_into I T n)) [0.. \ sets ?P" proof (safe intro!: sets.countable_UN) fix xs show "(\\<^sub>E j\I. if i = j then A else S j (xs ! T j)) \ sets ?P" using A S_in_E by (simp add: P_closed) (auto simp: P_def subset_eq intro!: exI[of _ "\j. if i = j then A else S j (xs ! T j)"]) qed finally show "(\x. x i) -` A \ space ?P \ sets ?P" using P_closed by simp qed qed from measurable_sets[OF this, of A] A `i \ I` E_closed have "(\x. x i) -` A \ space ?P \ sets ?P" by (simp add: E_generates) also have "(\x. x i) -` A \ space ?P = {f \ \\<^sub>E i\I. space (M i). f i \ A}" using P_closed by (auto simp: space_PiM) finally show "\ \ sets ?P" . qed finally show "sets (PiM I M) \ sigma_sets (space (PiM I M)) P" by (simp add: P_closed) show "sigma_sets (space (PiM I M)) P \ sets (PiM I M)" using `finite I` by (auto intro!: sets.sigma_sets_subset sets_PiM_I_finite simp: E_generates P_def) qed lemma pair_measure_eq_distr_PiM: fixes M1 :: "'a measure" and M2 :: "'a measure" assumes "sigma_finite_measure M1" "sigma_finite_measure M2" shows "(M1 \\<^sub>M M2) = distr (Pi\<^sub>M UNIV (case_bool M1 M2)) (M1 \\<^sub>M M2) (\x. (x True, x False))" (is "?P = ?D") proof (rule pair_measure_eqI[OF assms]) interpret B: product_sigma_finite "case_bool M1 M2" unfolding product_sigma_finite_def using assms by (auto split: bool.split) let ?B = "Pi\<^sub>M UNIV (case_bool M1 M2)" have [simp]: "fst \ (\x. (x True, x False)) = (\x. x True)" "snd \ (\x. (x True, x False)) = (\x. x False)" by auto fix A B assume A: "A \ sets M1" and B: "B \ sets M2" have "emeasure M1 A * emeasure M2 B = (\ i\UNIV. emeasure (case_bool M1 M2 i) (case_bool A B i))" by (simp add: UNIV_bool ac_simps) also have "\ = emeasure ?B (Pi\<^sub>E UNIV (case_bool A B))" using A B by (subst B.emeasure_PiM) (auto split: bool.split) also have "Pi\<^sub>E UNIV (case_bool A B) = (\x. (x True, x False)) -` (A \ B) \ space ?B" using A[THEN sets.sets_into_space] B[THEN sets.sets_into_space] by (auto simp: PiE_iff all_bool_eq space_PiM split: bool.split) finally show "emeasure M1 A * emeasure M2 B = emeasure ?D (A \ B)" using A B measurable_component_singleton[of True UNIV "case_bool M1 M2"] measurable_component_singleton[of False UNIV "case_bool M1 M2"] by (subst emeasure_distr) (auto simp: measurable_pair_iff) qed simp end