(* 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 Pi_iff: "f \ Pi I X \ (\i\I. f i \ X i)" unfolding Pi_def by auto abbreviation "Pi\<^isub>E A B \ Pi A B \ extensional A" syntax "_PiE" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3PIE _:_./ _)" 10) syntax (xsymbols) "_PiE" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3\\<^isub>E _\_./ _)" 10) syntax (HTML output) "_PiE" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3\\<^isub>E _\_./ _)" 10) translations "PIE x:A. B" == "CONST Pi\<^isub>E A (%x. B)" abbreviation funcset_extensional :: "['a set, 'b set] => ('a => 'b) set" (infixr "->\<^isub>E" 60) where "A ->\<^isub>E B \ Pi\<^isub>E A (%_. B)" notation (xsymbols) funcset_extensional (infixr "\\<^isub>E" 60) lemma extensional_empty[simp]: "extensional {} = {\x. undefined}" by safe (auto simp add: extensional_def fun_eq_iff) lemma extensional_insert[intro, simp]: assumes "a \ extensional (insert i I)" shows "a(i := b) \ extensional (insert i I)" using assms unfolding extensional_def by auto lemma extensional_Int[simp]: "extensional I \ extensional I' = extensional (I \ I')" unfolding extensional_def by auto definition "merge I x J 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 x J y i = x i" "I \ J = {} \ i \ J \ merge I x J y i = y i" "J \ I = {} \ i \ I \ merge I x J y i = x i" "J \ I = {} \ i \ J \ merge I x J y i = y i" "i \ I \ i \ J \ merge I x J y i = undefined" unfolding merge_def by auto lemma merge_commute: "I \ J = {} \ merge I x J y = merge J y I x" by (auto simp: merge_def intro!: ext) lemma Pi_cancel_merge_range[simp]: "I \ J = {} \ x \ Pi I (merge I A J B) \ x \ Pi I A" "I \ J = {} \ x \ Pi I (merge J B I A) \ x \ Pi I A" "J \ I = {} \ x \ Pi I (merge I A J B) \ x \ Pi I A" "J \ I = {} \ x \ Pi I (merge J B I A) \ x \ Pi I A" by (auto simp: Pi_def) lemma Pi_cancel_merge[simp]: "I \ J = {} \ merge I x J y \ Pi I B \ x \ Pi I B" "J \ I = {} \ merge I x J y \ Pi I B \ x \ Pi I B" "I \ J = {} \ merge I x J y \ Pi J B \ y \ Pi J B" "J \ I = {} \ merge I x J y \ Pi J B \ y \ Pi J B" by (auto simp: Pi_def) lemma extensional_merge[simp]: "merge I x J y \ extensional (I \ J)" by (auto simp: extensional_def) lemma restrict_Pi_cancel: "restrict x I \ Pi I A \ x \ Pi I A" by (auto simp: restrict_def Pi_def) lemma restrict_merge[simp]: "I \ J = {} \ restrict (merge I x J y) I = restrict x I" "I \ J = {} \ restrict (merge I x J y) J = restrict y J" "J \ I = {} \ restrict (merge I x J y) I = restrict x I" "J \ I = {} \ restrict (merge I x J y) J = restrict y J" by (auto simp: restrict_def intro!: ext) lemma extensional_insert_undefined[intro, simp]: assumes "a \ extensional (insert i I)" shows "a(i := undefined) \ extensional I" using assms unfolding extensional_def by auto lemma extensional_insert_cancel[intro, simp]: assumes "a \ extensional I" shows "a \ extensional (insert i I)" using assms unfolding extensional_def by auto lemma merge_singleton[simp]: "i \ I \ merge I x {i} y = restrict (x(i := y i)) (insert i I)" unfolding merge_def by (auto simp: fun_eq_iff) lemma Pi_Int: "Pi I E \ Pi I F = (\ i\I. E i \ F i)" by auto lemma PiE_Int: "(Pi\<^isub>E I A) \ (Pi\<^isub>E I B) = Pi\<^isub>E I (\x. A x \ B x)" by auto lemma Pi_cancel_fupd_range[simp]: "i \ I \ x \ Pi I (B(i := b)) \ x \ Pi I B" by (auto simp: Pi_def) lemma Pi_split_insert_domain[simp]: "x \ Pi (insert i I) X \ x \ Pi I X \ x i \ X i" by (auto simp: Pi_def) lemma Pi_split_domain[simp]: "x \ Pi (I \ J) X \ x \ Pi I X \ x \ Pi J X" by (auto simp: Pi_def) lemma Pi_cancel_fupd[simp]: "i \ I \ x(i := a) \ Pi I B \ x \ Pi I B" by (auto simp: Pi_def) lemma restrict_vimage: assumes "I \ J = {}" shows "(\x. (restrict x I, restrict x J)) -` (Pi\<^isub>E I E \ Pi\<^isub>E J F) = Pi (I \ J) (merge I E J F)" using assms by (auto simp: restrict_Pi_cancel) lemma merge_vimage: assumes "I \ J = {}" shows "(\(x,y). merge I x J y) -` Pi\<^isub>E (I \ J) E = Pi I E \ Pi J E" using assms by (auto simp: restrict_Pi_cancel) lemma restrict_fupd[simp]: "i \ I \ restrict (f (i := x)) I = restrict f I" by (auto simp: restrict_def intro!: ext) 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) lemma merge_x_x_eq_restrict[simp]: "merge I x J x = restrict x (I \ J)" unfolding merge_def by (auto intro!: ext) lemma Pi_fupd_iff: "i \ I \ f \ Pi I (B(i := A)) \ f \ Pi (I - {i}) B \ f i \ A" apply auto apply (drule_tac x=x in Pi_mem) apply (simp_all split: split_if_asm) apply (drule_tac x=i in Pi_mem) apply (auto dest!: Pi_mem) done lemma Pi_UN: fixes A :: "nat \ 'i \ 'a set" assumes "finite I" and mono: "\i n m. i \ I \ n \ m \ A n i \ A m i" shows "(\n. Pi I (A n)) = (\ i\I. \n. A n i)" proof (intro set_eqI iffI) fix f assume "f \ (\ i\I. \n. A n i)" then have "\i\I. \n. f i \ A n i" by auto from bchoice[OF this] obtain n where n: "\i. i \ I \ f i \ (A (n i) i)" by auto obtain k where k: "\i. i \ I \ n i \ k" using `finite I` finite_nat_set_iff_bounded_le[of "n`I"] by auto have "f \ Pi I (A k)" proof (intro Pi_I) fix i assume "i \ I" from mono[OF this, of "n i" k] k[OF this] n[OF this] show "f i \ A k i" by auto qed then show "f \ (\n. Pi I (A n))" by auto qed auto lemma PiE_cong: assumes "\i. i\I \ A i = B i" shows "Pi\<^isub>E I A = Pi\<^isub>E I B" using assms by (auto intro!: Pi_cong) lemma restrict_upd[simp]: "i \ I \ (restrict f I)(i := y) = restrict (f(i := y)) (insert i I)" by (auto simp: fun_eq_iff) lemma Pi_eq_subset: assumes ne: "\i. i \ I \ F i \ {}" "\i. i \ I \ F' i \ {}" assumes eq: "Pi\<^isub>E I F = Pi\<^isub>E I F'" and "i \ I" shows "F i \ F' i" proof fix x assume "x \ F i" with ne have "\j. \y. ((j \ I \ y \ F j \ (i = j \ x = y)) \ (j \ I \ y = undefined))" by auto from choice[OF this] guess f .. note f = this then have "f \ Pi\<^isub>E I F" by (auto simp: extensional_def) then have "f \ Pi\<^isub>E I F'" using assms by simp then show "x \ F' i" using f `i \ I` by auto qed lemma Pi_eq_iff_not_empty: assumes ne: "\i. i \ I \ F i \ {}" "\i. i \ I \ F' i \ {}" shows "Pi\<^isub>E I F = Pi\<^isub>E I F' \ (\i\I. F i = F' i)" proof (intro iffI ballI) fix i assume eq: "Pi\<^isub>E I F = Pi\<^isub>E I F'" and i: "i \ I" show "F i = F' i" using Pi_eq_subset[of I F F', OF ne eq i] using Pi_eq_subset[of I F' F, OF ne(2,1) eq[symmetric] i] by auto qed auto lemma Pi_eq_empty_iff: "Pi\<^isub>E I F = {} \ (\i\I. F i = {})" proof assume "Pi\<^isub>E I F = {}" show "\i\I. F i = {}" proof (rule ccontr) assume "\ ?thesis" then have "\i. \y. (i \ I \ y \ F i) \ (i \ I \ y = undefined)" by auto from choice[OF this] guess f .. then have "f \ Pi\<^isub>E I F" by (auto simp: extensional_def) with `Pi\<^isub>E I F = {}` show False by auto qed qed auto lemma Pi_eq_iff: "Pi\<^isub>E I F = Pi\<^isub>E I F' \ (\i\I. F i = F' i) \ ((\i\I. F i = {}) \ (\i\I. F' i = {}))" proof (intro iffI disjCI) assume eq[simp]: "Pi\<^isub>E I F = Pi\<^isub>E I F'" assume "\ ((\i\I. F i = {}) \ (\i\I. F' i = {}))" then have "(\i\I. F i \ {}) \ (\i\I. F' i \ {})" using Pi_eq_empty_iff[of I F] Pi_eq_empty_iff[of I F'] by auto with Pi_eq_iff_not_empty[of I F F'] show "\i\I. F i = F' i" by auto next assume "(\i\I. F i = F' i) \ (\i\I. F i = {}) \ (\i\I. F' i = {})" then show "Pi\<^isub>E I F = Pi\<^isub>E I F'" using Pi_eq_empty_iff[of I F] Pi_eq_empty_iff[of I F'] by auto qed section "Finite product spaces" section "Products" locale product_sigma_algebra = fixes M :: "'i \ ('a, 'b) measure_space_scheme" assumes sigma_algebras: "\i. sigma_algebra (M i)" locale finite_product_sigma_algebra = product_sigma_algebra M for M :: "'i \ ('a, 'b) measure_space_scheme" + fixes I :: "'i set" assumes finite_index: "finite I" definition "product_algebra_generator I M = \ space = (\\<^isub>E i \ I. space (M i)), sets = Pi\<^isub>E I ` (\ i \ I. sets (M i)), measure = \A. (\i\I. measure (M i) ((SOME F. A = Pi\<^isub>E I F) i)) \" definition product_algebra_def: "Pi\<^isub>M I M = sigma (product_algebra_generator I M) \ measure := (SOME \. sigma_finite_measure (sigma (product_algebra_generator I M) \ measure := \ \) \ (\A\\ i\I. sets (M i). \ (Pi\<^isub>E I A) = (\i\I. measure (M i) (A i))))\" syntax "_PiM" :: "[pttrn, 'i set, ('a, 'b) measure_space_scheme] => ('i => 'a, 'b) measure_space_scheme" ("(3PIM _:_./ _)" 10) syntax (xsymbols) "_PiM" :: "[pttrn, 'i set, ('a, 'b) measure_space_scheme] => ('i => 'a, 'b) measure_space_scheme" ("(3\\<^isub>M _\_./ _)" 10) syntax (HTML output) "_PiM" :: "[pttrn, 'i set, ('a, 'b) measure_space_scheme] => ('i => 'a, 'b) measure_space_scheme" ("(3\\<^isub>M _\_./ _)" 10) translations "PIM x:I. M" == "CONST Pi\<^isub>M I (%x. M)" abbreviation (in finite_product_sigma_algebra) "G \ product_algebra_generator I M" abbreviation (in finite_product_sigma_algebra) "P \ Pi\<^isub>M I M" sublocale product_sigma_algebra \ M: sigma_algebra "M i" for i by (rule sigma_algebras) lemma sigma_into_space: assumes "sets M \ Pow (space M)" shows "sets (sigma M) \ Pow (space M)" using sigma_sets_into_sp[OF assms] unfolding sigma_def by auto lemma (in product_sigma_algebra) product_algebra_generator_into_space: "sets (product_algebra_generator I M) \ 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) \ 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 \ sigma_algebra P using sigma_algebra_product_algebra . lemma product_algebraE: assumes "A \ sets (product_algebra_generator I M)" obtains E where "A = Pi\<^isub>E I E" "E \ (\ i\I. sets (M i))" using assms unfolding product_algebra_generator_def by auto lemma product_algebra_generatorI[intro]: assumes "E \ (\ i\I. sets (M i))" shows "Pi\<^isub>E I E \ 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 (\i. space (M i))" unfolding product_algebra_generator_def by simp lemma space_product_algebra[simp]: "space (Pi\<^isub>M I M) = (\\<^isub>E i\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 product_algebra_generator_sets_into_space: assumes "\i. i\I \ sets (M i) \ Pow (space (M i))" shows "sets (product_algebra_generator I M) \ 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]: "\ \i. i \ I \ A i \ sets (M i) \ \ Pi\<^isub>E I A \ sets P" by (auto simp: sets_product_algebra) lemma Int_stable_product_algebra_generator: "(\i. i \ I \ Int_stable (M i)) \ Int_stable (product_algebra_generator I M)" by (auto simp add: product_algebra_generator_def Int_stable_def PiE_Int Pi_iff) section "Generating set generates also product algebra" lemma sigma_product_algebra_sigma_eq: assumes "finite I" assumes mono: "\i. i \ I \ incseq (S i)" assumes union: "\i. i \ I \ (\j. S i j) = space (E i)" assumes sets_into: "\i. i \ I \ range (S i) \ sets (E i)" and E: "\i. sets (E i) \ Pow (space (E i))" shows "sets (\\<^isub>M i\I. sigma (E i)) = sets (\\<^isub>M i\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 \ {}" interpret E: sigma_algebra "sigma (E i)" for i using E by (rule sigma_algebra_sigma) have into_space[intro]: "\i x A. A \ sets (E i) \ x i \ A \ x i \ 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 \ I" and A: "A \ sets (E i)" then have "(\x. x i) -` A \ space ?E = (\\<^isub>E j\I. if j = i then A else \n. S j n) \ space ?E" using mono union unfolding incseq_Suc_iff space_product_algebra by (auto dest: Pi_mem) also have "\ = (\n. (\\<^isub>E j\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 "\ \ sets ?E" using sets_into `A \ 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 "(\x. x i) -` A \ space ?E \ sets ?E" . } then have proj: "\i. i\I \ (\x. x i) \ measurable ?E (sigma (E i))" using E by (subst G.measurable_iff_sigma) (auto simp: sets_product_algebra sets_sigma) { fix A assume A: "\i. i \ I \ A i \ sets (sigma (E i))" with proj have basic: "\i. i \ I \ (\x. x i) -` (A i) \ space ?E \ sets ?E" unfolding measurable_def by simp have "Pi\<^isub>E I A = (\i\I. (\x. x i) -` (A i) \ space ?E)" using A E.sets_into_space `I \ {}` unfolding product_algebra_def by auto blast then have "Pi\<^isub>E I A \ sets ?E" using G.finite_INT[OF `finite I` `I \ {}` basic, of "\i. i"] by simp } then have "sigma_sets (space ?E) (sets (product_algebra_generator I (\i. sigma (E i)))) \ sets ?E" by (intro G.sigma_sets_subset) (auto simp add: product_algebra_generator_def) then have subset: "sets ?S \ sets ?E" by (simp add: sets_sigma sets_product_algebra) show "sets ?S = sets ?E" proof (intro set_eqI iffI) fix A assume "A \ sets ?E" then show "A \ 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 \ sets ?S" then show "A \ sets ?E" using subset by auto qed qed lemma product_algebraI[intro]: "E \ (\ i\I. sets (M i)) \ Pi\<^isub>E I E \ sets (Pi\<^isub>M I M)" using assms unfolding product_algebra_def by (auto intro: product_algebra_generatorI) lemma (in product_sigma_algebra) measurable_component_update: assumes "x \ space (Pi\<^isub>M I M)" and "i \ I" shows "(\v. x(i := v)) \ measurable (M i) (Pi\<^isub>M (insert i I) M)" (is "?f \ _") unfolding product_algebra_def apply simp proof (intro measurable_sigma) let ?G = "product_algebra_generator (insert i I) M" show "sets ?G \ Pow (space ?G)" using product_algebra_generator_into_space . show "?f \ space (M i) \ space ?G" using M.sets_into_space assms by auto fix A assume "A \ sets ?G" from product_algebraE[OF this] guess E . note E = this then have "?f -` A \ space (M i) = E i \ ?f -` A \ space (M i) = {}" using M.sets_into_space assms by auto then show "?f -` A \ space (M i) \ sets (M i)" using E by (auto intro!: product_algebraI) qed lemma (in product_sigma_algebra) measurable_add_dim: assumes "i \ I" shows "(\(f, y). f(i := y)) \ measurable (Pi\<^isub>M I M \\<^isub>M M i) (Pi\<^isub>M (insert i I) M)" proof - let ?f = "(\(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 \ measurable Ii.P (sigma ?G)" proof (rule Ii.measurable_sigma) show "sets ?G \ Pow (space ?G)" using product_algebra_generator_into_space . show "?f \ space (Pi\<^isub>M I M \\<^isub>M M i) \ space ?G" by (auto simp: space_pair_measure) next fix A assume "A \ sets ?G" then obtain F where "A = Pi\<^isub>E (insert i I) F" and F: "\j. j \ I \ F j \ sets (M j)" "F i \ sets (M i)" by (auto elim!: product_algebraE) then have "?f -` A \ space (Pi\<^isub>M I M \\<^isub>M M i) = Pi\<^isub>E I F \ (F i)" using sets_into_space `i \ I` by (auto simp add: space_pair_measure) blast+ then show "?f -` A \ space (Pi\<^isub>M I M \\<^isub>M M i) \ sets (Pi\<^isub>M I M \\<^isub>M M i)" using F by (auto intro!: pair_measureI) qed then show ?thesis by (simp add: product_algebra_def) qed lemma (in product_sigma_algebra) measurable_merge: assumes [simp]: "I \ J = {}" shows "(\(x, y). merge I x J y) \ measurable (Pi\<^isub>M I M \\<^isub>M Pi\<^isub>M J M) (Pi\<^isub>M (I \ J) M)" proof - let ?I = "Pi\<^isub>M I M" and ?J = "Pi\<^isub>M J M" interpret P: sigma_algebra "?I \\<^isub>M ?J" by (intro sigma_algebra_pair_measure product_algebra_into_space) let ?f = "\(x, y). merge I x J y" let ?G = "product_algebra_generator (I \ J) M" have "?f \ measurable (?I \\<^isub>M ?J) (sigma ?G)" proof (rule P.measurable_sigma) fix A assume "A \ sets ?G" from product_algebraE[OF this] obtain E where E: "A = Pi\<^isub>E (I \ J) E" "E \ (\ i\I \ J. sets (M i))" . then have *: "?f -` A \ space (?I \\<^isub>M ?J) = Pi\<^isub>E I E \ Pi\<^isub>E J E" using sets_into_space `I \ J = {}` by (auto simp add: space_pair_measure) fast+ then show "?f -` A \ space (?I \\<^isub>M ?J) \ sets (?I \\<^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 \ measurable (?I \\<^isub>M ?J) (Pi\<^isub>M (I \ J) M)" unfolding product_algebra_def[of "I \ J"] by simp qed lemma (in product_sigma_algebra) measurable_component_singleton: assumes "i \ I" shows "(\x. x i) \ measurable (Pi\<^isub>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\<^isub>M I M) = (\\<^isub>E j\I. if i = j then A else space (M j))" using M.sets_into_space `i \ I` by (fastsimp dest: Pi_mem split: split_if_asm) then show "(\x. x i) -` A \ space (Pi\<^isub>M I M) \ sets (Pi\<^isub>M I M)" using `A \ sets (M i)` by (auto intro!: product_algebraI) qed (insert `i \ I`, auto) lemma (in sigma_algebra) measurable_restrict: assumes I: "finite I" assumes "\i. i \ I \ sets (N i) \ Pow (space (N i))" assumes X: "\i. i \ I \ X i \ measurable M (N i)" shows "(\x. \i\I. X i x) \ measurable M (Pi\<^isub>M I N)" unfolding product_algebra_def proof (simp, rule measurable_sigma) show "sets (product_algebra_generator I N) \ Pow (space (product_algebra_generator I N))" by (rule product_algebra_generator_sets_into_space) fact show "(\x. \i\I. X i x) \ space M \ space (product_algebra_generator I N)" using X by (auto simp: measurable_def) fix E assume "E \ sets (product_algebra_generator I N)" then obtain F where "E = Pi\<^isub>E I F" and F: "\i. i \ I \ F i \ sets (N i)" by (auto simp: product_algebra_generator_def) then have "(\x. \i\I. X i x) -` E \ space M = (\i\I. X i -` F i \ space M) \ space M" by (auto simp: Pi_iff) also have "\ \ sets M" proof cases assume "I = {}" then show ?thesis by simp next assume "I \ {}" with X F I show ?thesis by (intro finite_INT measurable_sets Int) auto qed finally show "(\x. \i\I. X i x) -` E \ space M \ sets M" . qed locale product_sigma_finite = fixes M :: "'i \ ('a,'b) measure_space_scheme" assumes sigma_finite_measures: "\i. sigma_finite_measure (M i)" locale finite_product_sigma_finite = product_sigma_finite M for M :: "'i \ ('a,'b) measure_space_scheme" + fixes I :: "'i set" assumes finite_index'[intro]: "finite I" sublocale product_sigma_finite \ M: sigma_finite_measure "M i" for i by (rule sigma_finite_measures) sublocale product_sigma_finite \ product_sigma_algebra by default sublocale finite_product_sigma_finite \ finite_product_sigma_algebra by default (fact finite_index') lemma (in finite_product_sigma_finite) product_algebra_generator_measure: assumes "Pi\<^isub>E I F \ sets G" shows "measure G (Pi\<^isub>E I F) = (\i\I. M.\ i (F i))" proof cases assume ne: "\i\I. F i \ {}" have "\i\I. (SOME F'. Pi\<^isub>E I F = Pi\<^isub>E I F') i = F i" by (rule someI2[where P="\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: "\ (\j\I. F j \ {})" then have "(\j\I. M.\ j (F j)) = 0" by (auto simp: setprod_ereal_0 intro!: bexI) moreover have "\j\I. (SOME F'. Pi\<^isub>E I F = Pi\<^isub>E I F') j = {}" by (rule someI2[where P="\F'. Pi\<^isub>E I F = Pi\<^isub>E I F'"]) (insert empty, auto simp: Pi_eq_empty_iff[symmetric]) then have "(\j\I. M.\ 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 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. \ i (F i k) \ \) \ incseq (\k. \\<^isub>E i\I. F i k) \ (\k. \\<^isub>E i\I. F i k) = space G" proof - have "\i::'i. \F::nat \ 'a set. range F \ sets (M i) \ incseq F \ (\i. F i) = space (M i) \ (\k. \ i (F k) \ \)" using M.sigma_finite_up by simp 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. \ i (F i k) \ \" by auto let ?F = "\k. \\<^isub>E i\I. F i k" note space_product_algebra[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 "\ i (F i k) \ \" by fact next fix A assume "A \ (\i. ?F i)" then show "A \ space G" using `\i. range (F i) \ sets (M i)` M.sets_into_space by (force simp: image_subset_iff) next fix f assume "f \ space G" with Pi_UN[OF finite_index, of "\k i. F i k"] F show "f \ (\i. ?F i)" by (auto simp: incseq_def) next fix i show "?F i \ ?F (Suc i)" using `\i. incseq (F i)`[THEN incseq_SucD] by auto qed qed lemma sets_pair_cancel_measure[simp]: "sets (M1\measure := m1\ \\<^isub>M M2) = sets (M1 \\<^isub>M M2)" "sets (M1 \\<^isub>M M2\measure := m2\) = sets (M1 \\<^isub>M M2)" unfolding pair_measure_def pair_measure_generator_def sets_sigma by simp_all lemma measurable_pair_cancel_measure[simp]: "measurable (M1\measure := m1\ \\<^isub>M M2) M = measurable (M1 \\<^isub>M M2) M" "measurable (M1 \\<^isub>M M2\measure := m2\) M = measurable (M1 \\<^isub>M M2) M" "measurable M (M1\measure := m3\ \\<^isub>M M2) = measurable M (M1 \\<^isub>M M2)" "measurable M (M1 \\<^isub>M M2\measure := m4\) = measurable M (M1 \\<^isub>M M2)" unfolding measurable_def by (auto simp add: space_pair_measure) lemma (in product_sigma_finite) product_measure_exists: assumes "finite I" shows "\\. sigma_finite_measure (sigma (product_algebra_generator I M) \ measure := \ \) \ (\A\\ i\I. sets (M i). \ (Pi\<^isub>E I A) = (\i\I. M.\ i (A i)))" using `finite I` proof induct case empty interpret finite_product_sigma_finite M "{}" by default simp let ?\ = "(\A. if A = {} then 0 else 1) :: 'd set \ ereal" show ?case proof (intro exI conjI ballI) have "sigma_algebra (sigma G \measure := ?\\)" by (rule sigma_algebra_cong) (simp_all add: product_algebra_def) then have "measure_space (sigma G\measure := ?\\)" 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\measure := ?\\)" by (auto intro!: exI[of _ "\i. {\_. undefined}"] simp: sigma_finite_measure_def sigma_finite_measure_axioms_def product_algebra_generator_def) qed auto 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 \ where prod: "\A. A \ (\ i\I. sets (M i)) \ \ (Pi\<^isub>E I A) = (\i\I. M.\ i (A i))" and "sigma_finite_measure (sigma G\ measure := \ \)" by auto then interpret I: sigma_finite_measure "P\ measure := \\" unfolding product_algebra_def by simp interpret P: pair_sigma_finite "P\ measure := \\" "M i" .. let ?h = "(\(f, y). f(i := y))" let ?\ = "\A. P.\ (?h -` A \ space P.P)" have I': "sigma_algebra (I'.P\ measure := ?\ \)" by (rule I'.sigma_algebra_cong) simp_all interpret I'': measure_space "I'.P\ measure := ?\ \" using measurable_add_dim[OF `i \ I`] by (intro P.measure_space_vimage[OF I']) (auto simp add: measure_preserving_def) show ?case proof (intro exI[of _ ?\] conjI ballI) let "?m A" = "measure (Pi\<^isub>M I M\measure := \\ \\<^isub>M M i) (?h -` A \ space P.P)" { fix A assume A: "A \ (\ i\insert i I. sets (M i))" then have *: "?h -` Pi\<^isub>E (insert i I) A \ space P.P = Pi\<^isub>E I A \ A i" using `i \ I` M.sets_into_space by (auto simp: space_pair_measure space_product_algebra) blast show "?m (Pi\<^isub>E (insert i I) A) = (\i\insert i I. M.\ i (A i))" unfolding * using A apply (subst P.pair_measure_times) using A apply fastsimp using A apply fastsimp using `i \ I` `finite I` prod[of A] A by (auto simp: ac_simps) } note product = this have *: "sigma I'.G\ measure := ?\ \ = I'.P\ measure := ?\ \" by (simp add: product_algebra_def) show "sigma_finite_measure (sigma I'.G\ measure := ?\ \)" proof (unfold *, default, simp) from I'.sigma_finite_pairs guess F :: "'i \ nat \ 'a set" .. then have F: "\j. j \ insert i I \ range (F j) \ sets (M j)" "incseq (\k. \\<^isub>E j \ insert i I. F j k)" "(\k. \\<^isub>E j \ insert i I. F j k) = space I'.G" "\k. \j. j \ insert i I \ \ j (F j k) \ \" by blast+ let "?F k" = "\\<^isub>E j \ insert i I. F j k" show "\F::nat \ ('i \ 'a) set. range F \ sets I'.P \ (\i. F i) = (\\<^isub>E i\insert i I. space (M i)) \ (\i. ?m (F i) \ \)" proof (intro exI[of _ ?F] conjI allI) show "range ?F \ sets I'.P" using F(1) by auto next from F(3) show "(\i. ?F i) = (\\<^isub>E i\insert i I. space (M i))" by simp next fix j have "\k. k \ insert i I \ 0 \ measure (M k) (F k j)" using F(1) by auto with F `finite I` setprod_PInf[of "insert i I", OF this] show "?\ (?F j) \ \" by (subst product) auto qed qed qed qed sublocale finite_product_sigma_finite \ sigma_finite_measure P unfolding product_algebra_def using product_measure_exists[OF finite_index] by (rule someI2_ex) auto lemma (in finite_product_sigma_finite) measure_times: assumes "\i. i \ I \ A i \ sets (M i)" shows "\ (Pi\<^isub>E I A) = (\i\I. M.\ i (A i))" unfolding product_algebra_def using product_measure_exists[OF finite_index] proof (rule someI2_ex, elim conjE) fix \ assume *: "\A\\ i\I. sets (M i). \ (Pi\<^isub>E I A) = (\i\I. M.\ i (A i))" have "Pi\<^isub>E I A = Pi\<^isub>E I (\i\I. A i)" by (auto dest: Pi_mem) then have "\ (Pi\<^isub>E I A) = \ (Pi\<^isub>E I (\i\I. A i))" by simp also have "\ = (\i\I. M.\ i ((\i\I. A i) i))" using assms * by auto finally show "measure (sigma G\measure := \\) (Pi\<^isub>E I A) = (\i\I. M.\ i (A i))" by (simp add: sigma_def) qed lemma (in product_sigma_finite) product_measure_empty[simp]: "measure (Pi\<^isub>M {} M) {\x. undefined} = 1" proof - interpret finite_product_sigma_finite M "{}" by default auto from measure_times[of "\x. {}"] show ?thesis by simp qed lemma (in finite_product_sigma_algebra) P_empty: assumes "I = {}" shows "space P = {\k. undefined}" "sets P = { {}, {\k. undefined} }" unfolding product_algebra_def product_algebra_generator_def `I = {}` by (simp_all add: sigma_def image_constant) lemma (in product_sigma_finite) positive_integral_empty: assumes pos: "0 \ f (\k. undefined)" shows "integral\<^isup>P (Pi\<^isub>M {} M) f = f (\k. undefined)" proof - interpret finite_product_sigma_finite M "{}" by default (fact finite.emptyI) have "\A. measure (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_raw proof (simp add: P_empty, intro antisym) show "f (\k. undefined) \ (SUP f:{g. g \ max 0 \ f}. f (\k. undefined))" by (intro le_SUPI) (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_leI) (auto simp: le_fun_def simp: max_def split: split_if_asm) qed qed lemma (in product_sigma_finite) measure_fold: assumes IJ[simp]: "I \ J = {}" and fin: "finite I" "finite J" assumes A: "A \ sets (Pi\<^isub>M (I \ J) M)" shows "measure (Pi\<^isub>M (I \ J) M) A = measure (Pi\<^isub>M I M \\<^isub>M Pi\<^isub>M J M) ((\(x,y). merge I x J y) -` A \ space (Pi\<^isub>M I M \\<^isub>M Pi\<^isub>M J M))" 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 I.P J.P by default let ?g = "\(x,y). merge I x J y" let "?X S" = "?g -` S \ space P.P" from IJ.sigma_finite_pairs obtain F where F: "\i. i\ I \ J \ range (F i) \ sets (M i)" "incseq (\k. \\<^isub>E i\I \ J. F i k)" "(\k. \\<^isub>E i\I \ J. F i k) = space IJ.G" "\k. \i\I\J. \ i (F i k) \ \" by auto let ?F = "\k. \\<^isub>E i\I \ J. F i k" show "IJ.\ A = P.\ (?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 \ 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 \ sets IJ.G" using F by (simp add: image_subset_iff product_algebra_def product_algebra_generator_def) show "incseq ?F" "(\i. ?F i) = space IJ.G " by fact+ next fix k have "\j. j \ I \ J \ 0 \ measure (M j) (F j k)" using F(1) by auto with F `finite I` setprod_PInf[of "I \ J", OF this] show "IJ.\ (?F k) \ \" by (subst IJ.measure_times) auto next fix A assume "A \ sets IJ.G" then obtain F where A: "A = Pi\<^isub>E (I \ J) F" and F: "\i. i \ I \ J \ F i \ sets (M i)" by (auto simp: product_algebra_generator_def) then have X: "?X A = (Pi\<^isub>E I F \ Pi\<^isub>E J F)" using sets_into_space by (auto simp: space_pair_measure) blast+ then have "P.\ (?X A) = (\i\I. \ i (F i)) * (\i\J. \ i (F i))" using `finite J` `finite I` F by (simp add: P.pair_measure_times I.measure_times J.measure_times) also have "\ = (\i\I \ J. \ i (F i))" using `finite J` `finite I` `I \ J = {}` by (simp add: setprod_Un_one) also have "\ = IJ.\ A" using `finite J` `finite I` F unfolding A by (intro IJ.measure_times[symmetric]) auto finally show "IJ.\ A = P.\ (?X A)" by (rule sym) qed (rule measurable_merge[OF IJ]) qed lemma (in product_sigma_finite) measure_preserving_merge: assumes IJ: "I \ J = {}" and "finite I" "finite J" shows "(\(x,y). merge I x J y) \ measure_preserving (Pi\<^isub>M I M \\<^isub>M Pi\<^isub>M J M) (Pi\<^isub>M (I \ 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 \ J = {}" "finite I" "finite J" and f: "f \ borel_measurable (Pi\<^isub>M (I \ J) M)" shows "integral\<^isup>P (Pi\<^isub>M (I \ J) M) f = (\\<^isup>+ x. (\\<^isup>+ y. f (merge I x J y) \(Pi\<^isub>M J M)) \(Pi\<^isub>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\<^isub>M I M" "Pi\<^isub>M J M" by default interpret IJ: finite_product_sigma_finite M "I \ J" by default simp have P_borel: "(\x. f (case x of (x, y) \ merge I x J y)) \ borel_measurable P.P" 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 "(\(x, y). merge I x J y) \ measure_preserving P.P IJ.P" using IJ by (rule measure_preserving_merge) show "f \ borel_measurable IJ.P" using f by simp qed qed lemma (in product_sigma_finite) measure_preserving_component_singelton: "(\x. x i) \ measure_preserving (Pi\<^isub>M {i} M) (M i)" proof (intro measure_preservingI measurable_component_singleton) interpret I: finite_product_sigma_finite M "{i}" by default simp fix A let ?P = "(\x. x i) -` A \ space I.P" assume A: "A \ sets (M i)" then have *: "?P = {i} \\<^isub>E A" using sets_into_space by auto show "I.\ ?P = M.\ i A" unfolding * using A I.measure_times[of "\_. A"] by auto qed auto lemma (in product_sigma_finite) product_positive_integral_singleton: assumes f: "f \ borel_measurable (M i)" shows "integral\<^isup>P (Pi\<^isub>M {i} M) (\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 "(\x. x i) \ measure_preserving (Pi\<^isub>M {i} M) (M i)" by (rule measure_preserving_component_singelton) show "f \ borel_measurable (M i)" by fact qed qed lemma (in product_sigma_finite) product_positive_integral_insert: assumes [simp]: "finite I" "i \ I" and f: "f \ borel_measurable (Pi\<^isub>M (insert i I) M)" shows "integral\<^isup>P (Pi\<^isub>M (insert i I) M) f = (\\<^isup>+ x. (\\<^isup>+ y. f (x(i := y)) \(M i)) \(Pi\<^isub>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 interpret P: pair_sigma_algebra I.P i.P .. have IJ: "I \ {i} = {}" and insert: "I \ {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 \ space I.P" let "?f y" = "f (restrict (x(i := y)) (insert i I))" have f'_eq: "\y. ?f y = f (x(i := y))" using x by (auto intro!: arg_cong[where f=f] simp: fun_eq_iff extensional_def) show "?f \ borel_measurable (M i)" unfolding f'_eq using measurable_comp[OF measurable_component_update f] x `i \ I` by (simp add: comp_def) show "integral\<^isup>P (M i) ?f = \\<^isup>+ y. f (x(i:=y)) \M i" unfolding f'_eq by simp qed qed lemma (in product_sigma_finite) product_positive_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 "(\\<^isup>+ x. (\i\I. f i (x i)) \Pi\<^isub>M I M) = (\i\I. integral\<^isup>P (M i) (f i))" using assms proof induct case empty interpret finite_product_sigma_finite M "{}" by default auto then 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 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\<^isub>M J M)" using sets_into_space insert by (intro sigma_algebra.borel_measurable_ereal_setprod sigma_algebra_product_algebra 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) done qed lemma (in product_sigma_finite) product_integral_singleton: assumes f: "f \ borel_measurable (M i)" shows "(\x. f (x i) \Pi\<^isub>M {i} M) = integral\<^isup>L (M i) f" proof - interpret I: finite_product_sigma_finite M "{i}" by default simp have *: "(\x. ereal (f x)) \ borel_measurable (M i)" "(\x. ereal (- f x)) \ borel_measurable (M i)" using assms by auto show ?thesis unfolding lebesgue_integral_def *[THEN product_positive_integral_singleton] .. qed lemma (in product_sigma_finite) product_integral_fold: assumes IJ[simp]: "I \ J = {}" and fin: "finite I" "finite J" and f: "integrable (Pi\<^isub>M (I \ J) M) f" shows "integral\<^isup>L (Pi\<^isub>M (I \ J) M) f = (\x. (\y. f (merge I x J y) \Pi\<^isub>M J M) \Pi\<^isub>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 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 I.P J.P by default let ?M = "\(x, y). merge I x J y" let ?f = "\x. f (?M x)" show ?thesis proof (subst P.integrable_fst_measurable(2)[of ?f, simplified]) have 1: "sigma_algebra IJ.P" by default have 2: "?M \ measure_preserving P.P IJ.P" using measure_preserving_merge[OF assms(1,2,3)] . have 3: "integrable (Pi\<^isub>M (I \ J) M) f" by fact then have 4: "f \ borel_measurable (Pi\<^isub>M (I \ 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 qed lemma (in product_sigma_finite) product_integral_insert: assumes [simp]: "finite I" "i \ I" and f: "integrable (Pi\<^isub>M (insert i I) M) f" shows "integral\<^isup>L (Pi\<^isub>M (insert i I) M) f = (\x. (\y. f (x(i:=y)) \M i) \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 \ {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 \ space I.P" let "?f y" = "f (restrict (x(i := y)) (insert i I))" have f'_eq: "\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 \ borel_measurable I'.P" using f unfolding integrable_def by auto show "?f \ borel_measurable (M i)" unfolding measurable_cong[OF f'_eq] using measurable_comp[OF measurable_component_update f] x `i \ I` by (simp add: comp_def) show "integral\<^isup>L (M i) ?f = integral\<^isup>L (M i) (\y. f (x(i := y)))" unfolding f'_eq by simp qed qed lemma (in product_sigma_finite) product_integrable_setprod: fixes f :: "'i \ 'a \ real" assumes [simp]: "finite I" and integrable: "\i. i \ I \ integrable (M i) (f i)" shows "integrable (Pi\<^isub>M I M) (\x. (\i\I. f i (x i)))" (is "integrable _ ?f") proof - interpret finite_product_sigma_finite M I by default fact have f: "\i. i \ I \ f i \ borel_measurable (M i)" using integrable unfolding integrable_def by auto then have borel: "?f \ borel_measurable P" using measurable_comp[OF measurable_component_singleton f] by (auto intro!: borel_measurable_setprod simp: comp_def) moreover have "integrable (Pi\<^isub>M I M) (\x. \\i\I. f i (x i)\)" proof (unfold integrable_def, intro conjI) show "(\x. abs (?f x)) \ borel_measurable P" using borel by auto have "(\\<^isup>+x. ereal (abs (?f x)) \P) = (\\<^isup>+x. (\i\I. ereal (abs (f i (x i)))) \P)" by (simp add: setprod_ereal abs_setprod) also have "\ = (\i\I. (\\<^isup>+x. ereal (abs (f i x)) \M i))" using f by (subst product_positive_integral_setprod) auto also have "\ < \" using integrable[THEN M.integrable_abs] by (simp add: setprod_PInf integrable_def M.positive_integral_positive) finally show "(\\<^isup>+x. ereal (abs (?f x)) \P) \ \" by auto have "(\\<^isup>+x. ereal (- abs (?f x)) \P) = (\\<^isup>+x. 0 \P)" by (intro positive_integral_cong_pos) auto then show "(\\<^isup>+x. ereal (- abs (?f x)) \P) \ \" by simp qed ultimately show ?thesis by (rule integrable_abs_iff[THEN iffD1]) qed lemma (in product_sigma_finite) product_integral_setprod: fixes f :: "'i \ 'a \ real" assumes "finite I" "I \ {}" and integrable: "\i. i \ I \ integrable (M i) (f i)" shows "(\x. (\i\I. f i (x i)) \Pi\<^isub>M I M) = (\i\I. integral\<^isup>L (M i) (f i))" using assms proof (induct rule: finite_ne_induct) case (singleton i) then show ?case by (simp add: product_integral_singleton integrable_def) next case (insert i I) then have iI: "finite (insert i I)" by auto then have prod: "\J. J \ insert i I \ integrable (Pi\<^isub>M J M) (\x. (\i\J. f i (x i)))" by (intro product_integrable_setprod insert(5)) (auto intro: finite_subset) interpret I: finite_product_sigma_finite M I by default fact have *: "\x y. (\j\I. f j (if j = i then y else x j)) = (\j\I. f j (x j))" using `i \ 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) qed end