(* Title: HOL/Analysis/Finite_Product_Measure.thy Author: Johannes Hölzl, TU München *) section ‹Finite Product Measure› theory Finite_Product_Measure imports Binary_Product_Measure Function_Topology begin lemma Pi_choice: "(∀i∈I. ∃x∈F i. P i x) ⟷ (∃f∈Pi I F. ∀i∈I. P i (f i))" by (metis Pi_iff) lemma PiE_choice: "(∀i∈I. ∃x∈F i. P i x) ⟷(∃f∈Pi⇩_{E}I F. ∀i∈I. P i (f i))" unfolding Pi_choice by (metis Int_iff PiE_def restrict_PiE restrict_apply) lemma case_prod_const: "(λ(i, j). c) = (λ_. c)" by auto subsection✐‹tag unimportant› ‹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) ∈ Pi⇩_{E}(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 ⊆ (Π⇩_{E}i∈J. S i)" "B ⊆ (Π⇩_{E}i∈J. S i)" and ne: "(Π⇩_{E}i∈I. S i) ≠ {}" and eq: "(λx. restrict x J) -` A ∩ (Π⇩_{E}i∈I. S i) = (λx. restrict x J) -` B ∩ (Π⇩_{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 ∈ (Π⇩_{E}i∈J. S i)" have "x ∈ A ⟷ merge J (I - J) (x,y) ∈ (λx. restrict x J) -` A ∩ (Π⇩_{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 (use sets in auto) qed lemma restrict_vimage: "I ∩ J = {} ⟹ (λx. (restrict x I, restrict x J)) -` (Pi⇩_{E}I E × Pi⇩_{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⇩_{E}(I ∪ J) E = Pi I E × Pi J E" by (auto simp: restrict_Pi_cancel PiE_def) subsection ‹Finite product spaces› definition✐‹tag important› prod_emb where "prod_emb I M K X = (λx. restrict x K) -` X ∩ (Π⇩_{E}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 (Π⇩_{E}i∈J. E i) = (Π⇩_{E}i∈I. if i ∈ J then E i else space (M i))" by (force simp: prod_emb_def PiE_iff if_split_mem2) lemma prod_emb_PiE_same_index[simp]: "(⋀i. i ∈ I ⟹ E i ⊆ space (M i)) ⟹ prod_emb I M I (Pi⇩_{E}I E) = Pi⇩_{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⇩_{E}J X) = (Π⇩_{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: if_split_asm) blast+ lemma prod_emb_id: "B ⊆ (Π⇩_{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✐‹tag important› PiM :: "'i set ⇒ ('i ⇒ 'a measure) ⇒ ('i ⇒ 'a) measure" where "PiM I M = extend_measure (Π⇩_{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 (Π⇩_{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✐‹tag important› prod_algebra :: "'i set ⇒ ('i ⇒ 'a measure) ⇒ ('i ⇒ 'a) set set" where "prod_algebra I M = (λ(J, X). prod_emb I M J (Π⇩_{E}j∈J. X j)) ` {(J, X). (J ≠ {} ∨ I = {}) ∧ finite J ∧ J ⊆ I ∧ X ∈ (Π j∈J. sets (M j))}" abbreviation "Pi⇩_{M}I M ≡ PiM I M" syntax "_PiM" :: "pttrn ⇒ 'i set ⇒ 'a measure ⇒ ('i => 'a) measure" ("(3Π⇩_{M}_∈_./ _)" 10) translations "Π⇩_{M}x∈I. M" == "CONST PiM I (%x. M)" lemma extend_measure_cong: assumes "Ω = Ω'" "I = I'" "G = G'" "⋀i. i ∈ I' ⟹ μ i = μ' i" shows "extend_measure Ω I G μ = extend_measure Ω' I' G' μ'" unfolding extend_measure_def by (auto simp add: assms) lemma Pi_cong_sets: "⟦I = J; ⋀x. x ∈ I ⟹ M x = N x⟧ ⟹ Pi I M = Pi J N" by auto lemma PiM_cong: assumes "I = J" "⋀x. x ∈ I ⟹ M x = N x" shows "PiM I M = PiM J N" unfolding PiM_def proof (rule extend_measure_cong, goal_cases) case 1 show ?case using assms by (subst assms(1), intro PiE_cong[of J "λi. space (M i)" "λi. space (N i)"]) simp_all next case 2 have "⋀K. K ⊆ J ⟹ (Π j∈K. sets (M j)) = (Π j∈K. sets (N j))" using assms by (intro Pi_cong_sets) auto thus ?case by (auto simp: assms) next case 3 show ?case using assms by (intro ext) (auto simp: prod_emb_def dest: PiE_mem) next case (4 x) thus ?case using assms by (auto intro!: prod.cong split: if_split_asm) qed lemma prod_algebra_sets_into_space: "prod_algebra I M ⊆ Pow (Π⇩_{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 = {(Π⇩_{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 (Π⇩_{E}j∈J. E j)" by (auto simp: prod_algebra_def) let ?A = "Π⇩_{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 = (Π⇩_{E}i∈I. X i)" and X: "X ∈ (Π j∈I. sets (M j))" by auto then have A: "A = prod_emb I M I (Π⇩_{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 (Π⇩_{E}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⇩_{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⇩_{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⇩_{E}J E ∩ Pi⇩_{E}J F = Pi⇩_{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 (Π⇩_{E}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⇩_{E}I E" "E ∈ (Π i∈I. sets (M i))" proof - from A obtain E J where A: "A = prod_emb I M J (Pi⇩_{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 = (Π⇩_{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)" unfolding Int_stable_def proof safe fix A assume "A ∈ prod_algebra I M" from prod_algebraE[OF this] obtain J E where A: "A = prod_emb I M J (Pi⇩_{E}J E)" "finite J" "J ≠ {} ∨ I = {}" "J ⊆ I" "⋀i. i ∈ J ⟹ E i ∈ sets (M i)" by auto fix B assume "B ∈ prod_algebra I M" from prod_algebraE[OF this] obtain K F where B: "B = prod_emb I M K (Pi⇩_{E}K F)" "finite K" "K ≠ {} ∨ I = {}" "K ⊆ I" "⋀i. i ∈ K ⟹ F i ∈ sets (M i)" by auto have "A ∩ B = prod_emb I M (J ∪ K) (Π⇩_{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 proposition 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 (Π⇩_{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 "(Π⇩_{E}i∈I. space (E i)) = (Π⇩_{E}i∈I. space (F i))" by (rule PiE_cong) with A have "A = prod_emb I F J (Π⇩_{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 proposition prod_algebra_cong: assumes "I = J" and "(⋀i. i ∈ I ⟹ sets (M i) = sets (N i))" shows "prod_algebra I M = prod_algebra J N" by (metis assms prod_algebra_mono sets_eq_imp_space_eq subsetI subset_antisym) lemma space_in_prod_algebra: "(Π⇩_{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 "(Π⇩_{E}i∈I. space (M i)) = prod_emb I M {i} (Π⇩_{E}i∈{i}. space (M i))" by (auto simp: prod_emb_def) then show ?thesis by (simp add: ‹i ∈ I› prod_algebraI) qed lemma space_PiM: "space (Π⇩_{M}i∈I. M i) = (Π⇩_{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 prod_emb_subset_PiM[simp]: "prod_emb I M K X ⊆ space (PiM I M)" by (auto simp: prod_emb_def space_PiM) lemma space_PiM_empty_iff[simp]: "space (PiM I M) = {} ⟷ (∃i∈I. space (M i) = {})" by (auto simp: space_PiM PiE_eq_empty_iff) lemma undefined_in_PiM_empty[simp]: "(λx. undefined) ∈ space (PiM {} M)" by (auto simp: space_PiM) lemma sets_PiM: "sets (Π⇩_{M}i∈I. M i) = sigma_sets (Π⇩_{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 proposition sets_PiM_single: "sets (PiM I M) = sigma_sets (Π⇩_{E}i∈I. space (M i)) {{f∈Π⇩_{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] obtain J X where X: "A = prod_emb I M J (Pi⇩_{E}J X)" "finite J" "J ≠ {} ∨ I = {}" "J ⊆ I" "⋀i. i ∈ J ⟹ X i ∈ sets (M i)" by auto show "A ∈ sigma_sets ?Ω ?R" proof cases assume "I = {}" with X show ?thesis by (metis (no_types, lifting) PiE_cong R.top empty_iff prod_emb_PiE subset_eq) next assume "I ≠ {}" with X have "A = (⋂j∈J. {f∈(Π⇩_{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∈Π⇩_{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} (Π⇩_{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_eq_proj: assumes "I ≠ {}" shows "sets (PiM I M) = sets (SUP i∈I. vimage_algebra (Π⇩_{E}i∈I. space (M i)) (λx. x i) (M i))" (is "?lhs = ?rhs") proof - have "?lhs = sigma_sets (Π⇩_{E}i∈I. space (M i)) {{f ∈ Π⇩_{E}i∈I. space (M i). f i ∈ A} |i A. i ∈ I ∧ A ∈ sets (M i)}" by (simp add: sets_PiM_single) also have "… = sigma_sets (Π⇩_{E}i∈I. space (M i)) (⋃x∈I. sets (vimage_algebra (Π⇩_{E}i∈I. space (M i)) (λxa. xa x) (M x)))" apply (subst arg_cong [of _ _ Sup, OF image_cong, OF refl]) apply (rule sets_vimage_algebra2) by (auto intro!: arg_cong2[where f=sigma_sets]) also have "... = sigma_sets (Π⇩_{E}i∈I. space (M i)) (⋃ (sets ` (λi. vimage_algebra (Π⇩_{E}i∈I. space (M i)) (λx. x i) (M i)) ` I))" by simp also have "... = ?rhs" by (subst sets_Sup_eq[where X="Π⇩_{E}i∈I. space (M i)"]) (use assms in auto) finally show ?thesis . qed lemma shows space_PiM_empty: "space (Pi⇩_{M}{} M) = {λk. undefined}" and sets_PiM_empty: "sets (Pi⇩_{M}{} M) = { {}, {λk. undefined} }" by (simp_all add: space_PiM sets_PiM_single image_constant sigma_sets_empty_eq) proposition sets_PiM_sigma: assumes Ω_cover: "⋀i. i ∈ I ⟹ ∃S⊆E i. countable S ∧ Ω i = ⋃S" assumes E: "⋀i. i ∈ I ⟹ E i ⊆ Pow (Ω i)" assumes J: "⋀j. j ∈ J ⟹ finite j" "⋃J = I" defines "P ≡ {{f∈(Π⇩_{E}i∈I. Ω i). ∀i∈j. f i ∈ A i} | A j. j ∈ J ∧ A ∈ Pi j E}" shows "sets (Π⇩_{M}i∈I. sigma (Ω i) (E i)) = sets (sigma (Π⇩_{E}i∈I. Ω i) P)" proof cases assume "I = {}" with ‹⋃J = I› have "P = {{λ_. undefined}} ∨ P = {}" by (auto simp: P_def) with ‹I = {}› show ?thesis by (auto simp add: sets_PiM_empty sigma_sets_empty_eq) next let ?F = "λi. {(λx. x i) -` A ∩ Pi⇩_{E}I Ω |A. A ∈ E i}" assume "I ≠ {}" then have "sets (Pi⇩_{M}I (λi. sigma (Ω i) (E i))) = sets (SUP i∈I. vimage_algebra (Π⇩_{E}i∈I. Ω i) (λx. x i) (sigma (Ω i) (E i)))" by (subst sets_PiM_eq_proj) (auto simp: space_measure_of_conv) also have "… = sets (SUP i∈I. sigma (Pi⇩_{E}I Ω) (?F i))" using E by (intro sets_SUP_cong arg_cong[where f=sets] vimage_algebra_sigma) auto also have "… = sets (sigma (Pi⇩_{E}I Ω) (⋃i∈I. ?F i))" using ‹I ≠ {}› by (intro arg_cong[where f=sets] SUP_sigma_sigma) auto also have "… = sets (sigma (Pi⇩_{E}I Ω) P)" proof (intro arg_cong[where f=sets] sigma_eqI sigma_sets_eqI) show "(⋃i∈I. ?F i) ⊆ Pow (Pi⇩_{E}I Ω)" "P ⊆ Pow (Pi⇩_{E}I Ω)" by (auto simp: P_def) next interpret P: sigma_algebra "Π⇩_{E}i∈I. Ω i" "sigma_sets (Π⇩_{E}i∈I. Ω i) P" by (auto intro!: sigma_algebra_sigma_sets simp: P_def) fix Z assume "Z ∈ (⋃i∈I. ?F i)" then obtain i A where i: "i ∈ I" "A ∈ E i" and Z_def: "Z = (λx. x i) -` A ∩ Pi⇩_{E}I Ω" by auto from ‹i ∈ I› J obtain j where j: "i ∈ j" "j ∈ J" "j ⊆ I" "finite j" by auto obtain S where S: "⋀i. i ∈ j ⟹ S i ⊆ E i" "⋀i. i ∈ j ⟹ countable (S i)" "⋀i. i ∈ j ⟹ Ω i = ⋃(S i)" by (metis subset_eq Ω_cover ‹j ⊆ I›) define A' where "A' n = n(i := A)" for n then have A'_i: "⋀n. A' n i = A" by simp { fix n assume "n ∈ Pi⇩_{E}(j - {i}) S" then have "A' n ∈ Pi j E" unfolding PiE_def Pi_def using S(1) by (auto simp: A'_def ‹A ∈ E i› ) with ‹j ∈ J› have "{f ∈ Pi⇩_{E}I Ω. ∀i∈j. f i ∈ A' n i} ∈ P" by (auto simp: P_def) } note A'_in_P = this { fix x assume "x i ∈ A" "x ∈ Pi⇩_{E}I Ω" with S(3) ‹j ⊆ I› have "∀i∈j. ∃s∈S i. x i ∈ s" by (auto simp: PiE_def Pi_def) then obtain s where s: "⋀i. i ∈ j ⟹ s i ∈ S i" "⋀i. i ∈ j ⟹ x i ∈ s i" by metis with ‹x i ∈ A› have "∃n∈Pi⇩_{E}(j-{i}) S. ∀i∈j. x i ∈ A' n i" by (intro bexI[of _ "restrict (s(i := A)) (j-{i})"]) (auto simp: A'_def split: if_splits) } then have "Z = (⋃n∈Pi⇩_{E}(j-{i}) S. {f∈(Π⇩_{E}i∈I. Ω i). ∀i∈j. f i ∈ A' n i})" unfolding Z_def by (auto simp add: set_eq_iff ball_conj_distrib ‹i∈j› A'_i dest: bspec[OF _ ‹i∈j›] cong: conj_cong) also have "… ∈ sigma_sets (Π⇩_{E}i∈I. Ω i) P" using ‹finite j› S(2) by (intro P.countable_UN' countable_PiE) (simp_all add: image_subset_iff A'_in_P) finally show "Z ∈ sigma_sets (Π⇩_{E}i∈I. Ω i) P" . next interpret F: sigma_algebra "Π⇩_{E}i∈I. Ω i" "sigma_sets (Π⇩_{E}i∈I. Ω i) (⋃i∈I. ?F i)" by (auto intro!: sigma_algebra_sigma_sets) fix b assume "b ∈ P" then obtain A j where b: "b = {f∈(Π⇩_{E}i∈I. Ω i). ∀i∈j. f i ∈ A i}" "j ∈ J" "A ∈ Pi j E" by (auto simp: P_def) show "b ∈ sigma_sets (Pi⇩_{E}I Ω) (⋃i∈I. ?F i)" proof cases assume "j = {}" with b have "b = (Π⇩_{E}i∈I. Ω i)" by auto then show ?thesis by blast next assume "j ≠ {}" with J b(2,3) have eq: "b = (⋂i∈j. ((λx. x i) -` A i ∩ Pi⇩_{E}I Ω))" unfolding b(1) by (auto simp: PiE_def Pi_def) show ?thesis unfolding eq using ‹A ∈ Pi j E› ‹j ∈ J› J(2) by (intro F.finite_INT J ‹j ∈ J› ‹j ≠ {}› sigma_sets.Basic) blast qed qed finally show "?thesis" . qed lemma sets_PiM_in_sets: assumes space: "space N = (Π⇩_{E}i∈I. space (M i))" assumes sets: "⋀i A. i ∈ I ⟹ A ∈ sets (M i) ⟹ {x∈space N. x i ∈ A} ∈ sets N" shows "sets (Π⇩_{M}i ∈ I. M i) ⊆ sets N" unfolding sets_PiM_single space[symmetric] by (intro sets.sigma_sets_subset subsetI) (auto intro: sets) lemma sets_PiM_cong[measurable_cong]: assumes "I = J" "⋀i. i ∈ J ⟹ sets (M i) = sets (N i)" shows "sets (PiM I M) = sets (PiM J N)" using assms sets_eq_imp_space_eq[OF assms(2)] by (simp add: sets_PiM_single cong: PiE_cong conj_cong) lemma sets_PiM_I: assumes "finite J" "J ⊆ I" "∀i∈J. E i ∈ sets (M i)" shows "prod_emb I M J (Π⇩_{E}j∈J. E j) ∈ sets (Π⇩_{M}i∈I. M i)" proof cases assume "J = {}" then have "prod_emb I M J (Π⇩_{E}j∈J. E j) = (Π⇩_{E}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 proposition measurable_PiM: assumes space: "f ∈ space N → (Π⇩_{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⇩_{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] obtain J X where "A = prod_emb I M J (Pi⇩_{E}J X)" "finite J" "J ≠ {} ∨ I = {}" "J ⊆ I" "⋀i. i ∈ J ⟹ X i ∈ sets (M i)" by auto with sets[of J X] show "f -` A ∩ space N ∈ sets N" by auto qed lemma measurable_PiM_Collect: assumes space: "f ∈ space N → (Π⇩_{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] obtain J X where X: "A = prod_emb I M J (Pi⇩_{E}J X)" "finite J" "J ≠ {} ∨ I = {}" "J ⊆ I" "⋀i. i ∈ J ⟹ X i ∈ sets (M i)" by auto 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 → (Π⇩_{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 ∈ Π⇩_{E}i∈I. space (M i). f i ∈ A} |i A. i ∈ I ∧ A ∈ sets (M i)}" then obtain B i where "A = {f ∈ Π⇩_{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 → (Π⇩_{E}i∈I. space (M i))" shows "(λω i. f i ω) ∈ measurable N (Pi⇩_{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 "(Π⇩_{E}j∈I. E j) ∈ sets (Π⇩_{M}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[measurable (raw)]: assumes "i ∈ I" shows "(λx. x i) ∈ measurable (Pi⇩_{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⇩_{M}I M) = prod_emb I M {i} (Π⇩_{E}j∈{i}. A)" using sets.sets_into_space ‹i ∈ I› by (fastforce dest: Pi_mem simp: prod_emb_def space_PiM split: if_split_asm) then show "(λx. x i) -` A ∩ space (Pi⇩_{M}I M) ∈ sets (Pi⇩_{M}I M)" using ‹A ∈ sets (M i)› ‹i ∈ I› by (auto intro!: sets_PiM_I) qed (use ‹i ∈ I› in ‹auto simp: space_PiM›) lemma measurable_component_singleton'[measurable_dest]: assumes f: "f ∈ measurable N (Pi⇩_{M}I M)" assumes g: "g ∈ measurable L N" assumes i: "i ∈ I" shows "(λx. (f (g x)) i) ∈ measurable L (M i)" using measurable_compose[OF measurable_compose[OF g f] measurable_component_singleton, OF i] . lemma measurable_PiM_component_rev: "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 (Π⇩_{M}i∈UNIV. M)" shows "(λx. case_nat (f x) (g x)) ∈ measurable N (Π⇩_{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⇩_{M}I M ⨂⇩_{M}M i) (Pi⇩_{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⇩_{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) proposition measurable_fun_upd: assumes I: "I = J ∪ {i}" assumes f[measurable]: "f ∈ measurable N (PiM J M)" assumes h[measurable]: "h ∈ measurable N (M i)" shows "(λx. (f x) (i := h x)) ∈ measurable N (PiM I M)" proof (intro measurable_PiM_single') fix j assume "j ∈ I" then show "(λω. ((f ω)(i := h ω)) j) ∈ measurable N (M j)" unfolding I by (cases "j = i") auto next show "(λx. (f x)(i := h x)) ∈ space N → (Π⇩_{E}i∈I. space (M i))" using I f[THEN measurable_space] h[THEN measurable_space] by (auto simp: space_PiM PiE_iff extensional_def) qed lemma measurable_component_update: "x ∈ space (Pi⇩_{M}I M) ⟹ i ∉ I ⟹ (λv. x(i := v)) ∈ measurable (M i) (Pi⇩_{M}(insert i I) M)" by simp lemma measurable_merge[measurable]: "merge I J ∈ measurable (Pi⇩_{M}I M ⨂⇩_{M}Pi⇩_{M}J M) (Pi⇩_{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⇩_{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) next show "(λx. λi∈I. X i x) ∈ space N → (Π⇩_{E}i∈I. space (M i))" using X by (auto simp add: PiE_def dest: measurable_space) qed 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⇩_{M}L M) (Pi⇩_{M}J M)" by (intro measurable_restrict measurable_component_singleton) auto lemma measurable_restrict_subset': assumes "J ⊆ L" "⋀x. x ∈ J ⟹ sets (M x) = sets (N x)" shows "(λf. restrict f J) ∈ measurable (Pi⇩_{M}L M) (Pi⇩_{M}J N)" by (metis (no_types) assms measurable_cong_sets measurable_restrict_subset sets_PiM_cong) lemma measurable_prod_emb[intro, simp]: "J ⊆ L ⟹ X ∈ sets (Pi⇩_{M}J M) ⟹ prod_emb L M J X ∈ sets (Pi⇩_{M}L M)" unfolding prod_emb_def space_PiM[symmetric] by (auto intro!: measurable_sets measurable_restrict measurable_component_singleton) lemma merge_in_prod_emb: assumes "y ∈ space (PiM I M)" "x ∈ X" and X: "X ∈ sets (Pi⇩_{M}J M)" and "J ⊆ I" shows "merge J I (x, y) ∈ prod_emb I M J X" using assms sets.sets_into_space[OF X] by (simp add: merge_def prod_emb_def subset_eq space_PiM PiE_def extensional_restrict Pi_iff cong: if_cong restrict_cong) (simp add: extensional_def) lemma prod_emb_eq_emptyD: assumes J: "J ⊆ I" and ne: "space (PiM I M) ≠ {}" and X: "X ∈ sets (Pi⇩_{M}J M)" and *: "prod_emb I M J X = {}" shows "X = {}" proof safe fix x assume "x ∈ X" obtain ω where "ω ∈ space (PiM I M)" using ne by blast from merge_in_prod_emb[OF this ‹x∈X› X J] * show "x ∈ {}" by auto qed 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)" by (smt (verit) PiE_iff mem_Collect_eq sets.top space_PiM subsetI subset_antisym) 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 lemma sets_PiM_I_countable: assumes I: "countable I" and E: "⋀i. i ∈ I ⟹ E i ∈ sets (M i)" shows "Pi⇩_{E}I E ∈ sets (Pi⇩_{M}I M)" proof cases assume "I ≠ {}" then have "Pi⇩_{E}I E = (⋂i∈I. prod_emb I M {i} (Pi⇩_{E}{i} E))" using E[THEN sets.sets_into_space] by (auto simp: PiE_iff prod_emb_def fun_eq_iff) also have "… ∈ sets (PiM I M)" using I ‹I ≠ {}› by (simp add: E sets.countable_INT' sets_PiM_I subset_eq) finally show ?thesis . qed (simp add: sets_PiM_empty) lemma sets_PiM_D_countable: assumes A: "A ∈ PiM I M" shows "∃J⊆I. ∃X∈PiM J M. countable J ∧ A = prod_emb I M J X" using A[unfolded sets_PiM_single] proof induction case (Basic A) then obtain i X where *: "i ∈ I" "X ∈ sets (M i)" and "A = {f ∈ Π⇩_{E}i∈I. space (M i). f i ∈ X}" by auto then have A: "A = prod_emb I M {i} (Π⇩_{E}_∈{i}. X)" by (auto simp: prod_emb_def) then show ?case by (intro exI[of _ "{i}"] conjI bexI[of _ "Π⇩_{E}_∈{i}. X"]) (auto intro: countable_finite * sets_PiM_I_finite) next case Empty then show ?case by (intro exI[of _ "{}"] conjI bexI[of _ "{}"]) auto next case (Compl A) then obtain J X where "J ⊆ I" "X ∈ sets (Pi⇩_{M}J M)" "countable J" "A = prod_emb I M J X" by auto then show ?case by (intro exI[of _ J] bexI[of _ "space (PiM J M) - X"] conjI) (auto simp add: space_PiM prod_emb_PiE intro!: sets_PiM_I_countable) next case (Union K) obtain J X where J: "⋀i. J i ⊆ I" "⋀i. countable (J i)" and X: "⋀i. X i ∈ sets (Pi⇩_{M}(J i) M)" and K: "⋀i. K i = prod_emb I M (J i) (X i)" by (metis Union.IH) show ?case proof (intro exI bexI conjI) show "(⋃i. J i) ⊆ I" "countable (⋃i. J i)" using J by auto with J show "⋃(K ` UNIV) = prod_emb I M (⋃i. J i) (⋃i. prod_emb (⋃i. J i) M (J i) (X i))" by (simp add: K[abs_def] SUP_upper) qed(auto intro: X) qed proposition measure_eqI_PiM_finite: assumes [simp]: "finite I" "sets P = PiM I M" "sets Q = PiM I M" assumes eq: "⋀A. (⋀i. i ∈ I ⟹ A i ∈ sets (M i)) ⟹ P (Pi⇩_{E}I A) = Q (Pi⇩_{E}I A)" assumes A: "range A ⊆ prod_algebra I M" "(⋃i. A i) = space (PiM I M)" "⋀i::nat. P (A i) ≠ ∞" shows "P = Q" proof (rule measure_eqI_generator_eq[OF Int_stable_prod_algebra prod_algebra_sets_into_space]) show "range A ⊆ prod_algebra I M" "(⋃i. A i) = (Π⇩_{E}i∈I. space (M i))" "⋀i. P (A i) ≠ ∞" unfolding space_PiM[symmetric] by fact+ fix X assume "X ∈ prod_algebra I M" then obtain J E where X: "X = prod_emb I M J (Π⇩_{E}j∈J. E j)" and J: "finite J" "J ⊆ I" "⋀j. j ∈ J ⟹ E j ∈ sets (M j)" by (force elim!: prod_algebraE) then show "emeasure P X = emeasure Q X" unfolding X by (subst (1 2) prod_emb_Pi) (auto simp: eq) qed (simp_all add: sets_PiM) proposition measure_eqI_PiM_infinite: assumes [simp]: "sets P = PiM I M" "sets Q = PiM I M" assumes eq: "⋀A J. finite J ⟹ J ⊆ I ⟹ (⋀i. i ∈ J ⟹ A i ∈ sets (M i)) ⟹ P (prod_emb I M J (Pi⇩_{E}J A)) = Q (prod_emb I M J (Pi⇩_{E}J A))" assumes A: "finite_measure P" shows "P = Q" proof (rule measure_eqI_generator_eq[OF Int_stable_prod_algebra prod_algebra_sets_into_space]) interpret finite_measure P by fact define i where "i = (SOME i. i ∈ I)" have i: "I ≠ {} ⟹ i ∈ I" unfolding i_def by (rule someI_ex) auto define A where "A n = (if I = {} then prod_emb I M {} (Π⇩_{E}i∈{}. {}) else prod_emb I M {i} (Π⇩_{E}i∈{i}. space (M i)))" for n :: nat then show "range A ⊆ prod_algebra I M" using prod_algebraI[of "{}" I "λi. space (M i)" M] by (auto intro!: prod_algebraI i) have "⋀i. A i = space (PiM I M)" by (auto simp: prod_emb_def space_PiM PiE_iff A_def i ex_in_conv[symmetric] exI) then show "(⋃i. A i) = (Π⇩_{E}i∈I. space (M i))" "⋀i. emeasure P (A i) ≠ ∞" by (auto simp: space_PiM) next fix X assume X: "X ∈ prod_algebra I M" then obtain J E where X: "X = prod_emb I M J (Π⇩_{E}j∈J. E j)" and J: "finite J" "J ⊆ I" "⋀j. j ∈ J ⟹ E j ∈ sets (M j)" by (force elim!: prod_algebraE) then show "emeasure P X = emeasure Q X" by (auto intro!: eq) qed (auto simp: sets_PiM) locale✐‹tag unimportant› product_sigma_finite = fixes M :: "'i ⇒ 'a measure" assumes sigma_finite_measures: "⋀i. sigma_finite_measure (M i)" sublocale✐‹tag unimportant› product_sigma_finite ⊆ M?: sigma_finite_measure "M i" for i by (rule sigma_finite_measures) locale✐‹tag unimportant› finite_product_sigma_finite = product_sigma_finite M for M :: "'i ⇒ 'a measure" + fixes I :: "'i set" assumes finite_index: "finite I" proposition (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. Π⇩_{E}i∈I. F i k) ∧ (⋃k. Π⇩_{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 then obtain F :: "'i ⇒ nat ⇒ 'a set" where "∀x. range (F x) ⊆ sets (M x) ∧ incseq (F x) ∧ ⋃ (range (F x)) = space (M x) ∧ (∀k. emeasure (M x) (F x k) ≠ ∞)" by metis 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. Π⇩_{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 emeasure_PiM_empty[simp]: "emeasure (PiM {} M) {λ_. undefined} = 1" proof - let ?μ = "λA. if A = {} then 0 else (1::ennreal)" have "emeasure (Pi⇩_{M}{} M) (prod_emb {} M {} (Π⇩_{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 {} (Π⇩_{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) lemma (in product_sigma_finite) emeasure_PiM: "finite I ⟹ (⋀i. i∈I ⟹ A i ∈ sets (M i)) ⟹ emeasure (PiM I M) (Pi⇩_{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 standard fact have "finite (insert i I)" using ‹finite I› by auto interpret I': finite_product_sigma_finite M "insert i I" by standard fact let ?h = "(λ(f, y). f(i := y))" let ?P = "distr (Pi⇩_{M}I M ⨂⇩_{M}M i) (Pi⇩_{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⇩_{M}(insert i I) M) (prod_emb (insert i I) M (insert i I) (Pi⇩_{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⇩_{E}J E)" let ?p' = "prod_emb I M (J - {i}) (Π⇩_{E}j∈J-{i}. E j)" have "?μ ?p = emeasure (Pi⇩_{M}I M ⨂⇩_{M}(M i)) (?h -` ?p ∩ space (Pi⇩_{M}I M ⨂⇩_{M}M i))" by (intro emeasure_distr measurable_add_dim sets_PiM_I) fact+ also have "?h -` ?p ∩ space (Pi⇩_{M}I M ⨂⇩_{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: if_split_asm) also have "emeasure (Pi⇩_{M}I M ⨂⇩_{M}(M i)) (?p' × (if i ∈ J then E i else space (M i))) = emeasure (Pi⇩_{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' = (Π⇩_{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: if_split_asm) blast+ also have "emeasure (Pi⇩_{M}I M) (Π⇩_{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!: prod.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="(*)"] prod.cong) also have "… = (∏j∈J ∪ ?I. ?f J E j)" using insert(1,2) J E by (intro prod.mono_neutral_right) auto finally show "?μ ?p = …" . show "prod_emb (insert i I) M J (Pi⇩_{E}J E) ∈ Pow (Π⇩_{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⇩_{M}(insert i I) M)) ?μ" "countably_additive (sets (Pi⇩_{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!: prod.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) PiM_eqI: assumes I[simp]: "finite I" and P: "sets P = PiM I M" assumes eq: "⋀A. (⋀i. i ∈ I ⟹ A i ∈ sets (M i)) ⟹ P (Pi⇩_{E}I A) = (∏i∈I. emeasure (M i) (A i))" shows "P = PiM I M" proof - interpret finite_product_sigma_finite M I by standard fact from sigma_finite_pairs obtain C where C: "∀i∈I. range (C i) ⊆ sets (M i)" "∀k. ∀i∈I. emeasure (M i) (C i k) ≠ ∞" "incseq (λk. Π⇩_{E}i∈I. C i k)" "(⋃k. Π⇩_{E}i∈I. C i k) = space (Pi⇩_{M}I M)" by auto show ?thesis proof (rule measure_eqI_PiM_finite[OF I refl P, symmetric]) show "(⋀i. i ∈ I ⟹ A i ∈ sets (M i)) ⟹ (Pi⇩_{M}I M) (Pi⇩_{E}I A) = P (Pi⇩_{E}I A)" for A by (simp add: eq emeasure_PiM) define A where "A n = (Π⇩_{E}i∈I. C i n)" for n with C show "range A ⊆ prod_algebra I M" "⋀i. emeasure (Pi⇩_{M}I M) (A i) ≠ ∞" "(⋃i. A i) = space (PiM I M)" by (auto intro!: prod_algebraI_finite simp: emeasure_PiM subset_eq ennreal_prod_eq_top) qed qed 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 standard 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 "(⋃(Pi⇩_{E}I ` Pi⇩_{E}I F)) = space (Pi⇩_{M}I M)" using in_space by (auto simp: space_PiM PiE_iff intro!: PiE_choice[THEN iffD1]) ultimately show "∃A. countable A ∧ A ⊆ sets (Pi⇩_{M}I M) ∧ ⋃A = space (Pi⇩_{M}I M) ∧ (∀a∈A. emeasure (Pi⇩_{M}I M) a ≠ ∞)" by (intro exI[of _ "Pi⇩_{E}I ` Pi⇩_{E}I F"]) (auto intro!: countable_PiE sets_PiM_I_finite simp: PiE_iff emeasure_PiM finite_index ennreal_prod_eq_top) qed sublocale finite_product_sigma_finite ⊆ sigma_finite_measure "Pi⇩_{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⇩_{M}I M) (Pi⇩_{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: "0 ≤ f (λk. undefined) ⟹ integral⇧^{N}(Pi⇩_{M}{} M) f = f (λk. undefined)" by (simp add: PiM_empty nn_integral_count_space_finite max.absorb2) lemma✐‹tag important› (in product_sigma_finite) distr_merge: assumes IJ[simp]: "I ∩ J = {}" and fin: "finite I" "finite J" shows "distr (Pi⇩_{M}I M ⨂⇩_{M}Pi⇩_{M}J M) (Pi⇩_{M}(I ∪ J) M) (merge I J) = Pi⇩_{M}(I ∪ J) M" (is "?D = ?P") proof (rule PiM_eqI) interpret I: finite_product_sigma_finite M I by standard fact interpret J: finite_product_sigma_finite M J by standard fact fix A assume A: "⋀i. i ∈ I ∪ J ⟹ A i ∈ sets (M i)" have *: "(merge I J -` Pi⇩_{E}(I ∪ J) A ∩ space (Pi⇩_{M}I M ⨂⇩_{M}Pi⇩_{M}J M)) = Pi⇩_{E}I A × Pi⇩_{E}J A" using A[THEN sets.sets_into_space] by (auto simp: space_PiM space_pair_measure) from A fin show "emeasure (distr (Pi⇩_{M}I M ⨂⇩_{M}Pi⇩_{M}J M) (Pi⇩_{M}(I ∪ J) M) (merge I J)) (Pi⇩_{E}(I ∪ J) A) = (∏i∈I ∪ J. emeasure (M i) (A i))" by (subst emeasure_distr) (auto simp: * J.emeasure_pair_measure_Times I.measure_times J.measure_times prod.union_disjoint) qed (use fin in simp_all) proposition (in product_sigma_finite) product_nn_integral_fold: assumes IJ: "I ∩ J = {}" "finite I" "finite J" and f[measurable]: "f ∈ borel_measurable (Pi⇩_{M}(I ∪ J) M)" shows "integral⇧^{N}(Pi⇩_{M}(I ∪ J) M) f = (∫⇧^{+}x. (∫⇧^{+}y. f (merge I J (x, y)) ∂(Pi⇩_{M}J M)) ∂(Pi⇩_{M}I M))" (is "?lhs = ?rhs") proof - interpret I: finite_product_sigma_finite M I by standard fact interpret J: finite_product_sigma_finite M J by standard fact interpret P: pair_sigma_finite "Pi⇩_{M}I M" "Pi⇩_{M}J M" by standard have P_borel: "(λx. f (merge I J x)) ∈ borel_measurable (Pi⇩_{M}I M ⨂⇩_{M}Pi⇩_{M}J M)" using measurable_comp[OF measurable_merge f] by (simp add: comp_def) have "?lhs = integral⇧^{N}(distr (Pi⇩_{M}I M ⨂⇩_{M}Pi⇩_{M}J M) (Pi⇩_{M}(I ∪ J) M) (merge I J)) f" by (simp add: I.finite_index J.finite_index assms(1) distr_merge) also have "... = ∫⇧^{+}x. f (merge I J x) ∂(Pi⇩_{M}I M ⨂⇩_{M}Pi⇩_{M}J M)" by (simp add: nn_integral_distr) also have "... = ?rhs" using P.Fubini P.nn_integral_snd by force finally show ?thesis . qed lemma (in product_sigma_finite) distr_singleton: "distr (Pi⇩_{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 standard simp fix A assume A: "A ∈ sets (M i)" then have "(λx. x i) -` A ∩ space (Pi⇩_{M}{i} M) = (Π⇩_{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⇧^{N}(Pi⇩_{M}{i} M) (λx. f (x i)) = integral⇧^{N}(M i) f" proof - interpret I: finite_product_sigma_finite M "{i}" by standard simp from f show ?thesis by (metis distr_singleton insert_iff measurable_component_singleton nn_integral_distr) qed proposition (in product_sigma_finite) product_nn_integral_insert: assumes I[simp]: "finite I" "i ∉ I" and f: "f ∈ borel_measurable (Pi⇩_{M}(insert i I) M)" shows "integral⇧^{N}(Pi⇩_{M}(insert i I) M) f = (∫⇧^{+}x. (∫⇧^{+}y. f (x(i := y)) ∂(M i)) ∂(Pi⇩_{M}I M))" proof - interpret I: finite_product_sigma_finite M I by standard auto interpret i: finite_product_sigma_finite M "{i}" by standard 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⇩_{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 "(∫⇧^{+}y. f (merge I {i} (x, y)) ∂Pi⇩_{M}{i} M) = (∫⇧^{+}y. f (x(i := y i)) ∂Pi⇩_{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_insert_rev: assumes I[simp]: "finite I" "i ∉ I" and [measurable]: