(* Title: HOL/Probability/Binary_Product_Measure.thy Author: Johannes Hölzl, TU München *) header {*Binary product measures*} theory Binary_Product_Measure imports Lebesgue_Integration begin lemma times_eq_iff: "A \ B = C \ D \ A = C \ B = D \ ((A = {} \ B = {}) \ (C = {} \ D = {}))" by auto lemma times_Int_times: "A \ B \ C \ D = (A \ C) \ (B \ D)" by auto lemma Pair_vimage_times[simp]: "\A B x. Pair x -` (A \ B) = (if x \ A then B else {})" by auto lemma rev_Pair_vimage_times[simp]: "\A B y. (\x. (x, y)) -` (A \ B) = (if y \ B then A else {})" by auto lemma case_prod_distrib: "f (case x of (x, y) \ g x y) = (case x of (x, y) \ f (g x y))" by (cases x) simp lemma split_beta': "(\(x,y). f x y) = (\x. f (fst x) (snd x))" by (auto simp: fun_eq_iff) section "Binary products" definition pair_measure (infixr "\\<^isub>M" 80) where "A \\<^isub>M B = measure_of (space A \ space B) {a \ b | a b. a \ sets A \ b \ sets B} (\X. \\<^isup>+x. (\\<^isup>+y. indicator X (x,y) \B) \A)" lemma pair_measure_closed: "{a \ b | a b. a \ sets A \ b \ sets B} \ Pow (space A \ space B)" using space_closed[of A] space_closed[of B] by auto lemma space_pair_measure: "space (A \\<^isub>M B) = space A \ space B" unfolding pair_measure_def using pair_measure_closed[of A B] by (rule space_measure_of) lemma sets_pair_measure: "sets (A \\<^isub>M B) = sigma_sets (space A \ space B) {a \ b | a b. a \ sets A \ b \ sets B}" unfolding pair_measure_def using pair_measure_closed[of A B] by (rule sets_measure_of) lemma sets_pair_measure_cong[cong]: "sets M1 = sets M1' \ sets M2 = sets M2' \ sets (M1 \\<^isub>M M2) = sets (M1' \\<^isub>M M2')" unfolding sets_pair_measure by (simp cong: sets_eq_imp_space_eq) lemma pair_measureI[intro, simp]: "x \ sets A \ y \ sets B \ x \ y \ sets (A \\<^isub>M B)" by (auto simp: sets_pair_measure) lemma measurable_pair_measureI: assumes 1: "f \ space M \ space M1 \ space M2" assumes 2: "\A B. A \ sets M1 \ B \ sets M2 \ f -` (A \ B) \ space M \ sets M" shows "f \ measurable M (M1 \\<^isub>M M2)" unfolding pair_measure_def using 1 2 by (intro measurable_measure_of) (auto dest: sets_into_space) lemma measurable_Pair: assumes f: "f \ measurable M M1" and g: "g \ measurable M M2" shows "(\x. (f x, g x)) \ measurable M (M1 \\<^isub>M M2)" proof (rule measurable_pair_measureI) show "(\x. (f x, g x)) \ space M \ space M1 \ space M2" using f g by (auto simp: measurable_def) fix A B assume *: "A \ sets M1" "B \ sets M2" have "(\x. (f x, g x)) -` (A \ B) \ space M = (f -` A \ space M) \ (g -` B \ space M)" by auto also have "\ \ sets M" by (rule Int) (auto intro!: measurable_sets * f g) finally show "(\x. (f x, g x)) -` (A \ B) \ space M \ sets M" . qed lemma measurable_pair: assumes "(fst \ f) \ measurable M M1" "(snd \ f) \ measurable M M2" shows "f \ measurable M (M1 \\<^isub>M M2)" using measurable_Pair[OF assms] by simp lemma measurable_fst[intro!, simp]: "fst \ measurable (M1 \\<^isub>M M2) M1" by (auto simp: fst_vimage_eq_Times space_pair_measure sets_into_space times_Int_times measurable_def) lemma measurable_snd[intro!, simp]: "snd \ measurable (M1 \\<^isub>M M2) M2" by (auto simp: snd_vimage_eq_Times space_pair_measure sets_into_space times_Int_times measurable_def) lemma measurable_fst': "f \ measurable M (N \\<^isub>M P) \ (\x. fst (f x)) \ measurable M N" using measurable_comp[OF _ measurable_fst] by (auto simp: comp_def) lemma measurable_snd': "f \ measurable M (N \\<^isub>M P) \ (\x. snd (f x)) \ measurable M P" using measurable_comp[OF _ measurable_snd] by (auto simp: comp_def) lemma measurable_fst'': "f \ measurable M N \ (\x. f (fst x)) \ measurable (M \\<^isub>M P) N" using measurable_comp[OF measurable_fst _] by (auto simp: comp_def) lemma measurable_snd'': "f \ measurable M N \ (\x. f (snd x)) \ measurable (P \\<^isub>M M) N" using measurable_comp[OF measurable_snd _] by (auto simp: comp_def) lemma measurable_pair_iff: "f \ measurable M (M1 \\<^isub>M M2) \ (fst \ f) \ measurable M M1 \ (snd \ f) \ measurable M M2" using measurable_pair[of f M M1 M2] by auto lemma measurable_split_conv: "(\(x, y). f x y) \ measurable A B \ (\x. f (fst x) (snd x)) \ measurable A B" by (intro arg_cong2[where f="op \"]) auto lemma measurable_pair_swap': "(\(x,y). (y, x)) \ measurable (M1 \\<^isub>M M2) (M2 \\<^isub>M M1)" by (auto intro!: measurable_Pair simp: measurable_split_conv) lemma measurable_pair_swap: assumes f: "f \ measurable (M1 \\<^isub>M M2) M" shows "(\(x,y). f (y, x)) \ measurable (M2 \\<^isub>M M1) M" using measurable_comp[OF measurable_Pair f] by (auto simp: measurable_split_conv comp_def) lemma measurable_pair_swap_iff: "f \ measurable (M2 \\<^isub>M M1) M \ (\(x,y). f (y,x)) \ measurable (M1 \\<^isub>M M2) M" using measurable_pair_swap[of "\(x,y). f (y, x)"] by (auto intro!: measurable_pair_swap) lemma measurable_ident[intro, simp]: "(\x. x) \ measurable M M" unfolding measurable_def by auto lemma measurable_Pair1': "x \ space M1 \ Pair x \ measurable M2 (M1 \\<^isub>M M2)" by (auto intro!: measurable_Pair) lemma sets_Pair1: assumes A: "A \ sets (M1 \\<^isub>M M2)" shows "Pair x -` A \ sets M2" proof - have "Pair x -` A = (if x \ space M1 then Pair x -` A \ space M2 else {})" using A[THEN sets_into_space] by (auto simp: space_pair_measure) also have "\ \ sets M2" using A by (auto simp add: measurable_Pair1' intro!: measurable_sets split: split_if_asm) finally show ?thesis . qed lemma measurable_Pair2': "y \ space M2 \ (\x. (x, y)) \ measurable M1 (M1 \\<^isub>M M2)" by (auto intro!: measurable_Pair) lemma sets_Pair2: assumes A: "A \ sets (M1 \\<^isub>M M2)" shows "(\x. (x, y)) -` A \ sets M1" proof - have "(\x. (x, y)) -` A = (if y \ space M2 then (\x. (x, y)) -` A \ space M1 else {})" using A[THEN sets_into_space] by (auto simp: space_pair_measure) also have "\ \ sets M1" using A by (auto simp add: measurable_Pair2' intro!: measurable_sets split: split_if_asm) finally show ?thesis . qed lemma measurable_Pair2: assumes f: "f \ measurable (M1 \\<^isub>M M2) M" and x: "x \ space M1" shows "(\y. f (x, y)) \ measurable M2 M" using measurable_comp[OF measurable_Pair1' f, OF x] by (simp add: comp_def) lemma measurable_Pair1: assumes f: "f \ measurable (M1 \\<^isub>M M2) M" and y: "y \ space M2" shows "(\x. f (x, y)) \ measurable M1 M" using measurable_comp[OF measurable_Pair2' f, OF y] by (simp add: comp_def) lemma Int_stable_pair_measure_generator: "Int_stable {a \ b | a b. a \ sets A \ b \ sets B}" unfolding Int_stable_def by safe (auto simp add: times_Int_times) lemma (in finite_measure) finite_measure_cut_measurable: assumes "Q \ sets (N \\<^isub>M M)" shows "(\x. emeasure M (Pair x -` Q)) \ borel_measurable N" (is "?s Q \ _") using Int_stable_pair_measure_generator pair_measure_closed assms unfolding sets_pair_measure proof (induct rule: sigma_sets_induct_disjoint) case (compl A) with sets_into_space have "\x. emeasure M (Pair x -` ((space N \ space M) - A)) = (if x \ space N then emeasure M (space M) - ?s A x else 0)" unfolding sets_pair_measure[symmetric] by (auto intro!: emeasure_compl simp: vimage_Diff sets_Pair1) with compl top show ?case by (auto intro!: measurable_If simp: space_pair_measure) next case (union F) moreover then have "\x. emeasure M (\i. Pair x -` F i) = (\i. ?s (F i) x)" unfolding sets_pair_measure[symmetric] by (intro suminf_emeasure[symmetric]) (auto simp: disjoint_family_on_def sets_Pair1) ultimately show ?case by (auto simp: vimage_UN) qed (auto simp add: if_distrib Int_def[symmetric] intro!: measurable_If) lemma (in sigma_finite_measure) measurable_emeasure_Pair: assumes Q: "Q \ sets (N \\<^isub>M M)" shows "(\x. emeasure M (Pair x -` Q)) \ borel_measurable N" (is "?s Q \ _") proof - from sigma_finite_disjoint guess F . note F = this then have F_sets: "\i. F i \ sets M" by auto let ?C = "\x i. F i \ Pair x -` Q" { fix i have [simp]: "space N \ F i \ space N \ space M = space N \ F i" using F sets_into_space by auto let ?R = "density M (indicator (F i))" have "finite_measure ?R" using F by (intro finite_measureI) (auto simp: emeasure_restricted subset_eq) then have "(\x. emeasure ?R (Pair x -` (space N \ space ?R \ Q))) \ borel_measurable N" by (rule finite_measure.finite_measure_cut_measurable) (auto intro: Q) moreover have "\x. emeasure ?R (Pair x -` (space N \ space ?R \ Q)) = emeasure M (F i \ Pair x -` (space N \ space ?R \ Q))" using Q F_sets by (intro emeasure_restricted) (auto intro: sets_Pair1) moreover have "\x. F i \ Pair x -` (space N \ space ?R \ Q) = ?C x i" using sets_into_space[OF Q] by (auto simp: space_pair_measure) ultimately have "(\x. emeasure M (?C x i)) \ borel_measurable N" by simp } moreover { fix x have "(\i. emeasure M (?C x i)) = emeasure M (\i. ?C x i)" proof (intro suminf_emeasure) show "range (?C x) \ sets M" using F `Q \ sets (N \\<^isub>M M)` by (auto intro!: sets_Pair1) have "disjoint_family F" using F by auto show "disjoint_family (?C x)" by (rule disjoint_family_on_bisimulation[OF `disjoint_family F`]) auto qed also have "(\i. ?C x i) = Pair x -` Q" using F sets_into_space[OF `Q \ sets (N \\<^isub>M M)`] by (auto simp: space_pair_measure) finally have "emeasure M (Pair x -` Q) = (\i. emeasure M (?C x i))" by simp } ultimately show ?thesis using `Q \ sets (N \\<^isub>M M)` F_sets by auto qed lemma (in sigma_finite_measure) emeasure_pair_measure: assumes "X \ sets (N \\<^isub>M M)" shows "emeasure (N \\<^isub>M M) X = (\\<^isup>+ x. \\<^isup>+ y. indicator X (x, y) \M \N)" (is "_ = ?\ X") proof (rule emeasure_measure_of[OF pair_measure_def]) show "positive (sets (N \\<^isub>M M)) ?\" by (auto simp: positive_def positive_integral_positive) have eq[simp]: "\A x y. indicator A (x, y) = indicator (Pair x -` A) y" by (auto simp: indicator_def) show "countably_additive (sets (N \\<^isub>M M)) ?\" proof (rule countably_additiveI) fix F :: "nat \ ('b \ 'a) set" assume F: "range F \ sets (N \\<^isub>M M)" "disjoint_family F" from F have *: "\i. F i \ sets (N \\<^isub>M M)" "(\i. F i) \ sets (N \\<^isub>M M)" by auto moreover from F have "\i. (\x. emeasure M (Pair x -` F i)) \ borel_measurable N" by (intro measurable_emeasure_Pair) auto moreover have "\x. disjoint_family (\i. Pair x -` F i)" by (intro disjoint_family_on_bisimulation[OF F(2)]) auto moreover have "\x. range (\i. Pair x -` F i) \ sets M" using F by (auto simp: sets_Pair1) ultimately show "(\n. ?\ (F n)) = ?\ (\i. F i)" by (auto simp add: vimage_UN positive_integral_suminf[symmetric] suminf_emeasure subset_eq emeasure_nonneg sets_Pair1 intro!: positive_integral_cong positive_integral_indicator[symmetric]) qed show "{a \ b |a b. a \ sets N \ b \ sets M} \ Pow (space N \ space M)" using space_closed[of N] space_closed[of M] by auto qed fact lemma (in sigma_finite_measure) emeasure_pair_measure_alt: assumes X: "X \ sets (N \\<^isub>M M)" shows "emeasure (N \\<^isub>M M) X = (\\<^isup>+x. emeasure M (Pair x -` X) \N)" proof - have [simp]: "\x y. indicator X (x, y) = indicator (Pair x -` X) y" by (auto simp: indicator_def) show ?thesis using X by (auto intro!: positive_integral_cong simp: emeasure_pair_measure sets_Pair1) qed lemma (in sigma_finite_measure) emeasure_pair_measure_Times: assumes A: "A \ sets N" and B: "B \ sets M" shows "emeasure (N \\<^isub>M M) (A \ B) = emeasure N A * emeasure M B" proof - have "emeasure (N \\<^isub>M M) (A \ B) = (\\<^isup>+x. emeasure M B * indicator A x \N)" using A B by (auto intro!: positive_integral_cong simp: emeasure_pair_measure_alt) also have "\ = emeasure M B * emeasure N A" using A by (simp add: emeasure_nonneg positive_integral_cmult_indicator) finally show ?thesis by (simp add: ac_simps) qed subsection {* Binary products of $\sigma$-finite emeasure spaces *} locale pair_sigma_finite = M1: sigma_finite_measure M1 + M2: sigma_finite_measure M2 for M1 :: "'a measure" and M2 :: "'b measure" lemma (in pair_sigma_finite) measurable_emeasure_Pair1: "Q \ sets (M1 \\<^isub>M M2) \ (\x. emeasure M2 (Pair x -` Q)) \ borel_measurable M1" using M2.measurable_emeasure_Pair . lemma (in pair_sigma_finite) measurable_emeasure_Pair2: assumes Q: "Q \ sets (M1 \\<^isub>M M2)" shows "(\y. emeasure M1 ((\x. (x, y)) -` Q)) \ borel_measurable M2" proof - have "(\(x, y). (y, x)) -` Q \ space (M2 \\<^isub>M M1) \ sets (M2 \\<^isub>M M1)" using Q measurable_pair_swap' by (auto intro: measurable_sets) note M1.measurable_emeasure_Pair[OF this] moreover have "\y. Pair y -` ((\(x, y). (y, x)) -` Q \ space (M2 \\<^isub>M M1)) = (\x. (x, y)) -` Q" using Q[THEN sets_into_space] by (auto simp: space_pair_measure) ultimately show ?thesis by simp qed lemma (in pair_sigma_finite) sigma_finite_up_in_pair_measure_generator: defines "E \ {A \ B | A B. A \ sets M1 \ B \ sets M2}" shows "\F::nat \ ('a \ 'b) set. range F \ E \ incseq F \ (\i. F i) = space M1 \ space M2 \ (\i. emeasure (M1 \\<^isub>M M2) (F i) \ \)" proof - from M1.sigma_finite_incseq guess F1 . note F1 = this from M2.sigma_finite_incseq guess F2 . note F2 = this from F1 F2 have space: "space M1 = (\i. F1 i)" "space M2 = (\i. F2 i)" by auto let ?F = "\i. F1 i \ F2 i" show ?thesis proof (intro exI[of _ ?F] conjI allI) show "range ?F \ E" using F1 F2 by (auto simp: E_def) (metis range_subsetD) next have "space M1 \ space M2 \ (\i. ?F i)" proof (intro subsetI) fix x assume "x \ space M1 \ space M2" then obtain i j where "fst x \ F1 i" "snd x \ F2 j" by (auto simp: space) then have "fst x \ F1 (max i j)" "snd x \ F2 (max j i)" using `incseq F1` `incseq F2` unfolding incseq_def by (force split: split_max)+ then have "(fst x, snd x) \ F1 (max i j) \ F2 (max i j)" by (intro SigmaI) (auto simp add: min_max.sup_commute) then show "x \ (\i. ?F i)" by auto qed then show "(\i. ?F i) = space M1 \ space M2" using space by (auto simp: space) next fix i show "incseq (\i. F1 i \ F2 i)" using `incseq F1` `incseq F2` unfolding incseq_Suc_iff by auto next fix i from F1 F2 have "F1 i \ sets M1" "F2 i \ sets M2" by auto with F1 F2 emeasure_nonneg[of M1 "F1 i"] emeasure_nonneg[of M2 "F2 i"] show "emeasure (M1 \\<^isub>M M2) (F1 i \ F2 i) \ \" by (auto simp add: emeasure_pair_measure_Times) qed qed sublocale pair_sigma_finite \ sigma_finite_measure "M1 \\<^isub>M M2" proof from sigma_finite_up_in_pair_measure_generator guess F :: "nat \ ('a \ 'b) set" .. note F = this show "\F::nat \ ('a \ 'b) set. range F \ sets (M1 \\<^isub>M M2) \ (\i. F i) = space (M1 \\<^isub>M M2) \ (\i. emeasure (M1 \\<^isub>M M2) (F i) \ \)" proof (rule exI[of _ F], intro conjI) show "range F \ sets (M1 \\<^isub>M M2)" using F by (auto simp: pair_measure_def) show "(\i. F i) = space (M1 \\<^isub>M M2)" using F by (auto simp: space_pair_measure) show "\i. emeasure (M1 \\<^isub>M M2) (F i) \ \" using F by auto qed qed lemma sigma_finite_pair_measure: assumes A: "sigma_finite_measure A" and B: "sigma_finite_measure B" shows "sigma_finite_measure (A \\<^isub>M B)" proof - interpret A: sigma_finite_measure A by fact interpret B: sigma_finite_measure B by fact interpret AB: pair_sigma_finite A B .. show ?thesis .. qed lemma sets_pair_swap: assumes "A \ sets (M1 \\<^isub>M M2)" shows "(\(x, y). (y, x)) -` A \ space (M2 \\<^isub>M M1) \ sets (M2 \\<^isub>M M1)" using measurable_pair_swap' assms by (rule measurable_sets) lemma (in pair_sigma_finite) distr_pair_swap: "M1 \\<^isub>M M2 = distr (M2 \\<^isub>M M1) (M1 \\<^isub>M M2) (\(x, y). (y, x))" (is "?P = ?D") proof - from sigma_finite_up_in_pair_measure_generator guess F :: "nat \ ('a \ 'b) set" .. note F = this let ?E = "{a \ b |a b. a \ sets M1 \ b \ sets M2}" show ?thesis proof (rule measure_eqI_generator_eq[OF Int_stable_pair_measure_generator[of M1 M2]]) show "?E \ Pow (space ?P)" using space_closed[of M1] space_closed[of M2] by (auto simp: space_pair_measure) show "sets ?P = sigma_sets (space ?P) ?E" by (simp add: sets_pair_measure space_pair_measure) then show "sets ?D = sigma_sets (space ?P) ?E" by simp next show "range F \ ?E" "(\i. F i) = space ?P" "\i. emeasure ?P (F i) \ \" using F by (auto simp: space_pair_measure) next fix X assume "X \ ?E" then obtain A B where X[simp]: "X = A \ B" and A: "A \ sets M1" and B: "B \ sets M2" by auto have "(\(y, x). (x, y)) -` X \ space (M2 \\<^isub>M M1) = B \ A" using sets_into_space[OF A] sets_into_space[OF B] by (auto simp: space_pair_measure) with A B show "emeasure (M1 \\<^isub>M M2) X = emeasure ?D X" by (simp add: M2.emeasure_pair_measure_Times M1.emeasure_pair_measure_Times emeasure_distr measurable_pair_swap' ac_simps) qed qed lemma (in pair_sigma_finite) emeasure_pair_measure_alt2: assumes A: "A \ sets (M1 \\<^isub>M M2)" shows "emeasure (M1 \\<^isub>M M2) A = (\\<^isup>+y. emeasure M1 ((\x. (x, y)) -` A) \M2)" (is "_ = ?\ A") proof - have [simp]: "\y. (Pair y -` ((\(x, y). (y, x)) -` A \ space (M2 \\<^isub>M M1))) = (\x. (x, y)) -` A" using sets_into_space[OF A] by (auto simp: space_pair_measure) show ?thesis using A by (subst distr_pair_swap) (simp_all del: vimage_Int add: measurable_sets[OF measurable_pair_swap'] M1.emeasure_pair_measure_alt emeasure_distr[OF measurable_pair_swap' A]) qed lemma (in pair_sigma_finite) AE_pair: assumes "AE x in (M1 \\<^isub>M M2). Q x" shows "AE x in M1. (AE y in M2. Q (x, y))" proof - obtain N where N: "N \ sets (M1 \\<^isub>M M2)" "emeasure (M1 \\<^isub>M M2) N = 0" "{x\space (M1 \\<^isub>M M2). \ Q x} \ N" using assms unfolding eventually_ae_filter by auto show ?thesis proof (rule AE_I) from N measurable_emeasure_Pair1[OF `N \ sets (M1 \\<^isub>M M2)`] show "emeasure M1 {x\space M1. emeasure M2 (Pair x -` N) \ 0} = 0" by (auto simp: M2.emeasure_pair_measure_alt positive_integral_0_iff emeasure_nonneg) show "{x \ space M1. emeasure M2 (Pair x -` N) \ 0} \ sets M1" by (intro borel_measurable_ereal_neq_const measurable_emeasure_Pair1 N) { fix x assume "x \ space M1" "emeasure M2 (Pair x -` N) = 0" have "AE y in M2. Q (x, y)" proof (rule AE_I) show "emeasure M2 (Pair x -` N) = 0" by fact show "Pair x -` N \ sets M2" using N(1) by (rule sets_Pair1) show "{y \ space M2. \ Q (x, y)} \ Pair x -` N" using N `x \ space M1` unfolding space_pair_measure by auto qed } then show "{x \ space M1. \ (AE y in M2. Q (x, y))} \ {x \ space M1. emeasure M2 (Pair x -` N) \ 0}" by auto qed qed lemma (in pair_sigma_finite) AE_pair_measure: assumes "{x\space (M1 \\<^isub>M M2). P x} \ sets (M1 \\<^isub>M M2)" assumes ae: "AE x in M1. AE y in M2. P (x, y)" shows "AE x in M1 \\<^isub>M M2. P x" proof (subst AE_iff_measurable[OF _ refl]) show "{x\space (M1 \\<^isub>M M2). \ P x} \ sets (M1 \\<^isub>M M2)" by (rule sets_Collect) fact then have "emeasure (M1 \\<^isub>M M2) {x \ space (M1 \\<^isub>M M2). \ P x} = (\\<^isup>+ x. \\<^isup>+ y. indicator {x \ space (M1 \\<^isub>M M2). \ P x} (x, y) \M2 \M1)" by (simp add: M2.emeasure_pair_measure) also have "\ = (\\<^isup>+ x. \\<^isup>+ y. 0 \M2 \M1)" using ae apply (safe intro!: positive_integral_cong_AE) apply (intro AE_I2) apply (safe intro!: positive_integral_cong_AE) apply auto done finally show "emeasure (M1 \\<^isub>M M2) {x \ space (M1 \\<^isub>M M2). \ P x} = 0" by simp qed lemma (in pair_sigma_finite) AE_pair_iff: "{x\space (M1 \\<^isub>M M2). P (fst x) (snd x)} \ sets (M1 \\<^isub>M M2) \ (AE x in M1. AE y in M2. P x y) \ (AE x in (M1 \\<^isub>M M2). P (fst x) (snd x))" using AE_pair[of "\x. P (fst x) (snd x)"] AE_pair_measure[of "\x. P (fst x) (snd x)"] by auto lemma (in pair_sigma_finite) AE_commute: assumes P: "{x\space (M1 \\<^isub>M M2). P (fst x) (snd x)} \ sets (M1 \\<^isub>M M2)" shows "(AE x in M1. AE y in M2. P x y) \ (AE y in M2. AE x in M1. P x y)" proof - interpret Q: pair_sigma_finite M2 M1 .. have [simp]: "\x. (fst (case x of (x, y) \ (y, x))) = snd x" "\x. (snd (case x of (x, y) \ (y, x))) = fst x" by auto have "{x \ space (M2 \\<^isub>M M1). P (snd x) (fst x)} = (\(x, y). (y, x)) -` {x \ space (M1 \\<^isub>M M2). P (fst x) (snd x)} \ space (M2 \\<^isub>M M1)" by (auto simp: space_pair_measure) also have "\ \ sets (M2 \\<^isub>M M1)" by (intro sets_pair_swap P) finally show ?thesis apply (subst AE_pair_iff[OF P]) apply (subst distr_pair_swap) apply (subst AE_distr_iff[OF measurable_pair_swap' P]) apply (subst Q.AE_pair_iff) apply simp_all done qed section "Fubinis theorem" lemma (in pair_sigma_finite) simple_function_cut: assumes f: "simple_function (M1 \\<^isub>M M2) f" "\x. 0 \ f x" shows "(\x. \\<^isup>+y. f (x, y) \M2) \ borel_measurable M1" and "(\\<^isup>+ x. (\\<^isup>+ y. f (x, y) \M2) \M1) = integral\<^isup>P (M1 \\<^isub>M M2) f" proof - have f_borel: "f \ borel_measurable (M1 \\<^isub>M M2)" using f(1) by (rule borel_measurable_simple_function) let ?F = "\z. f -` {z} \ space (M1 \\<^isub>M M2)" let ?F' = "\x z. Pair x -` ?F z" { fix x assume "x \ space M1" have [simp]: "\z y. indicator (?F z) (x, y) = indicator (?F' x z) y" by (auto simp: indicator_def) have "\y. y \ space M2 \ (x, y) \ space (M1 \\<^isub>M M2)" using `x \ space M1` by (simp add: space_pair_measure) moreover have "\x z. ?F' x z \ sets M2" using f_borel by (rule sets_Pair1[OF measurable_sets]) auto ultimately have "simple_function M2 (\ y. f (x, y))" apply (rule_tac simple_function_cong[THEN iffD2, OF _]) apply (rule simple_function_indicator_representation[OF f(1)]) using `x \ space M1` by auto } note M2_sf = this { fix x assume x: "x \ space M1" then have "(\\<^isup>+y. f (x, y) \M2) = (\z\f ` space (M1 \\<^isub>M M2). z * emeasure M2 (?F' x z))" unfolding positive_integral_eq_simple_integral[OF M2_sf[OF x] f(2)] unfolding simple_integral_def proof (safe intro!: setsum_mono_zero_cong_left) from f(1) show "finite (f ` space (M1 \\<^isub>M M2))" by (rule simple_functionD) next fix y assume "y \ space M2" then show "f (x, y) \ f ` space (M1 \\<^isub>M M2)" using `x \ space M1` by (auto simp: space_pair_measure) next fix x' y assume "(x', y) \ space (M1 \\<^isub>M M2)" "f (x', y) \ (\y. f (x, y)) ` space M2" then have *: "?F' x (f (x', y)) = {}" by (force simp: space_pair_measure) show "f (x', y) * emeasure M2 (?F' x (f (x', y))) = 0" unfolding * by simp qed (simp add: vimage_compose[symmetric] comp_def space_pair_measure) } note eq = this moreover have "\z. ?F z \ sets (M1 \\<^isub>M M2)" by (auto intro!: f_borel borel_measurable_vimage) moreover then have "\z. (\x. emeasure M2 (?F' x z)) \ borel_measurable M1" by (auto intro!: measurable_emeasure_Pair1 simp del: vimage_Int) moreover have *: "\i x. 0 \ emeasure M2 (Pair x -` (f -` {i} \ space (M1 \\<^isub>M M2)))" using f(1)[THEN simple_functionD(2)] f(2) by (intro emeasure_nonneg) moreover { fix i assume "i \ f`space (M1 \\<^isub>M M2)" with * have "\x. 0 \ i * emeasure M2 (Pair x -` (f -` {i} \ space (M1 \\<^isub>M M2)))" using f(2) by auto } ultimately show "(\x. \\<^isup>+y. f (x, y) \M2) \ borel_measurable M1" and "(\\<^isup>+ x. (\\<^isup>+ y. f (x, y) \M2) \M1) = integral\<^isup>P (M1 \\<^isub>M M2) f" using f(2) by (auto simp del: vimage_Int cong: measurable_cong intro!: setsum_cong simp add: positive_integral_setsum simple_integral_def positive_integral_cmult positive_integral_cong[OF eq] positive_integral_eq_simple_integral[OF f] M2.emeasure_pair_measure_alt[symmetric]) qed lemma (in pair_sigma_finite) positive_integral_fst_measurable: assumes f: "f \ borel_measurable (M1 \\<^isub>M M2)" shows "(\x. \\<^isup>+ y. f (x, y) \M2) \ borel_measurable M1" (is "?C f \ borel_measurable M1") and "(\\<^isup>+ x. (\\<^isup>+ y. f (x, y) \M2) \M1) = integral\<^isup>P (M1 \\<^isub>M M2) f" proof - from borel_measurable_implies_simple_function_sequence'[OF f] guess F . note F = this then have F_borel: "\i. F i \ borel_measurable (M1 \\<^isub>M M2)" by (auto intro: borel_measurable_simple_function) note sf = simple_function_cut[OF F(1,5)] then have "(\x. SUP i. ?C (F i) x) \ borel_measurable M1" using F(1) by auto moreover { fix x assume "x \ space M1" from F measurable_Pair2[OF F_borel `x \ space M1`] have "(\\<^isup>+y. (SUP i. F i (x, y)) \M2) = (SUP i. ?C (F i) x)" by (intro positive_integral_monotone_convergence_SUP) (auto simp: incseq_Suc_iff le_fun_def) then have "(SUP i. ?C (F i) x) = ?C f x" unfolding F(4) positive_integral_max_0 by simp } note SUPR_C = this ultimately show "?C f \ borel_measurable M1" by (simp cong: measurable_cong) have "(\\<^isup>+x. (SUP i. F i x) \(M1 \\<^isub>M M2)) = (SUP i. integral\<^isup>P (M1 \\<^isub>M M2) (F i))" using F_borel F by (intro positive_integral_monotone_convergence_SUP) auto also have "(SUP i. integral\<^isup>P (M1 \\<^isub>M M2) (F i)) = (SUP i. \\<^isup>+ x. (\\<^isup>+ y. F i (x, y) \M2) \M1)" unfolding sf(2) by simp also have "\ = \\<^isup>+ x. (SUP i. \\<^isup>+ y. F i (x, y) \M2) \M1" using F sf(1) by (intro positive_integral_monotone_convergence_SUP[symmetric]) (auto intro!: positive_integral_mono positive_integral_positive simp: incseq_Suc_iff le_fun_def) also have "\ = \\<^isup>+ x. (\\<^isup>+ y. (SUP i. F i (x, y)) \M2) \M1" using F_borel F(2,5) by (auto intro!: positive_integral_cong positive_integral_monotone_convergence_SUP[symmetric] measurable_Pair2 simp: incseq_Suc_iff le_fun_def) finally show "(\\<^isup>+ x. (\\<^isup>+ y. f (x, y) \M2) \M1) = integral\<^isup>P (M1 \\<^isub>M M2) f" using F by (simp add: positive_integral_max_0) qed lemma (in pair_sigma_finite) positive_integral_snd_measurable: assumes f: "f \ borel_measurable (M1 \\<^isub>M M2)" shows "(\\<^isup>+ y. (\\<^isup>+ x. f (x, y) \M1) \M2) = integral\<^isup>P (M1 \\<^isub>M M2) f" proof - interpret Q: pair_sigma_finite M2 M1 by default note measurable_pair_swap[OF f] from Q.positive_integral_fst_measurable[OF this] have "(\\<^isup>+ y. (\\<^isup>+ x. f (x, y) \M1) \M2) = (\\<^isup>+ (x, y). f (y, x) \(M2 \\<^isub>M M1))" by simp also have "(\\<^isup>+ (x, y). f (y, x) \(M2 \\<^isub>M M1)) = integral\<^isup>P (M1 \\<^isub>M M2) f" by (subst distr_pair_swap) (auto simp: positive_integral_distr[OF measurable_pair_swap' f] intro!: positive_integral_cong) finally show ?thesis . qed lemma (in pair_sigma_finite) Fubini: assumes f: "f \ borel_measurable (M1 \\<^isub>M M2)" shows "(\\<^isup>+ y. (\\<^isup>+ x. f (x, y) \M1) \M2) = (\\<^isup>+ x. (\\<^isup>+ y. f (x, y) \M2) \M1)" unfolding positive_integral_snd_measurable[OF assms] unfolding positive_integral_fst_measurable[OF assms] .. lemma (in pair_sigma_finite) integrable_product_swap: assumes "integrable (M1 \\<^isub>M M2) f" shows "integrable (M2 \\<^isub>M M1) (\(x,y). f (y,x))" proof - interpret Q: pair_sigma_finite M2 M1 by default have *: "(\(x,y). f (y,x)) = (\x. f (case x of (x,y)\(y,x)))" by (auto simp: fun_eq_iff) show ?thesis unfolding * by (rule integrable_distr[OF measurable_pair_swap']) (simp add: distr_pair_swap[symmetric] assms) qed lemma (in pair_sigma_finite) integrable_product_swap_iff: "integrable (M2 \\<^isub>M M1) (\(x,y). f (y,x)) \ integrable (M1 \\<^isub>M M2) f" proof - interpret Q: pair_sigma_finite M2 M1 by default from Q.integrable_product_swap[of "\(x,y). f (y,x)"] integrable_product_swap[of f] show ?thesis by auto qed lemma (in pair_sigma_finite) integral_product_swap: assumes f: "f \ borel_measurable (M1 \\<^isub>M M2)" shows "(\(x,y). f (y,x) \(M2 \\<^isub>M M1)) = integral\<^isup>L (M1 \\<^isub>M M2) f" proof - have *: "(\(x,y). f (y,x)) = (\x. f (case x of (x,y)\(y,x)))" by (auto simp: fun_eq_iff) show ?thesis unfolding * by (simp add: integral_distr[symmetric, OF measurable_pair_swap' f] distr_pair_swap[symmetric]) qed lemma (in pair_sigma_finite) integrable_fst_measurable: assumes f: "integrable (M1 \\<^isub>M M2) f" shows "AE x in M1. integrable M2 (\ y. f (x, y))" (is "?AE") and "(\x. (\y. f (x, y) \M2) \M1) = integral\<^isup>L (M1 \\<^isub>M M2) f" (is "?INT") proof - have f_borel: "f \ borel_measurable (M1 \\<^isub>M M2)" using f by auto let ?pf = "\x. ereal (f x)" and ?nf = "\x. ereal (- f x)" have borel: "?nf \ borel_measurable (M1 \\<^isub>M M2)""?pf \ borel_measurable (M1 \\<^isub>M M2)" and int: "integral\<^isup>P (M1 \\<^isub>M M2) ?nf \ \" "integral\<^isup>P (M1 \\<^isub>M M2) ?pf \ \" using assms by auto have "(\\<^isup>+x. (\\<^isup>+y. ereal (f (x, y)) \M2) \M1) \ \" "(\\<^isup>+x. (\\<^isup>+y. ereal (- f (x, y)) \M2) \M1) \ \" using borel[THEN positive_integral_fst_measurable(1)] int unfolding borel[THEN positive_integral_fst_measurable(2)] by simp_all with borel[THEN positive_integral_fst_measurable(1)] have AE_pos: "AE x in M1. (\\<^isup>+y. ereal (f (x, y)) \M2) \ \" "AE x in M1. (\\<^isup>+y. ereal (- f (x, y)) \M2) \ \" by (auto intro!: positive_integral_PInf_AE ) then have AE: "AE x in M1. \\\<^isup>+y. ereal (f (x, y)) \M2\ \ \" "AE x in M1. \\\<^isup>+y. ereal (- f (x, y)) \M2\ \ \" by (auto simp: positive_integral_positive) from AE_pos show ?AE using assms by (simp add: measurable_Pair2[OF f_borel] integrable_def) { fix f have "(\\<^isup>+ x. - \\<^isup>+ y. ereal (f x y) \M2 \M1) = (\\<^isup>+x. 0 \M1)" using positive_integral_positive by (intro positive_integral_cong_pos) (auto simp: ereal_uminus_le_reorder) then have "(\\<^isup>+ x. - \\<^isup>+ y. ereal (f x y) \M2 \M1) = 0" by simp } note this[simp] { fix f assume borel: "(\x. ereal (f x)) \ borel_measurable (M1 \\<^isub>M M2)" and int: "integral\<^isup>P (M1 \\<^isub>M M2) (\x. ereal (f x)) \ \" and AE: "AE x in M1. (\\<^isup>+y. ereal (f (x, y)) \M2) \ \" have "integrable M1 (\x. real (\\<^isup>+y. ereal (f (x, y)) \M2))" (is "integrable M1 ?f") proof (intro integrable_def[THEN iffD2] conjI) show "?f \ borel_measurable M1" using borel by (auto intro!: positive_integral_fst_measurable) have "(\\<^isup>+x. ereal (?f x) \M1) = (\\<^isup>+x. (\\<^isup>+y. ereal (f (x, y)) \M2) \M1)" using AE positive_integral_positive[of M2] by (auto intro!: positive_integral_cong_AE simp: ereal_real) then show "(\\<^isup>+x. ereal (?f x) \M1) \ \" using positive_integral_fst_measurable[OF borel] int by simp have "(\\<^isup>+x. ereal (- ?f x) \M1) = (\\<^isup>+x. 0 \M1)" by (intro positive_integral_cong_pos) (simp add: positive_integral_positive real_of_ereal_pos) then show "(\\<^isup>+x. ereal (- ?f x) \M1) \ \" by simp qed } with this[OF borel(1) int(1) AE_pos(2)] this[OF borel(2) int(2) AE_pos(1)] show ?INT unfolding lebesgue_integral_def[of "M1 \\<^isub>M M2"] lebesgue_integral_def[of M2] borel[THEN positive_integral_fst_measurable(2), symmetric] using AE[THEN integral_real] by simp qed lemma (in pair_sigma_finite) integrable_snd_measurable: assumes f: "integrable (M1 \\<^isub>M M2) f" shows "AE y in M2. integrable M1 (\x. f (x, y))" (is "?AE") and "(\y. (\x. f (x, y) \M1) \M2) = integral\<^isup>L (M1 \\<^isub>M M2) f" (is "?INT") proof - interpret Q: pair_sigma_finite M2 M1 by default have Q_int: "integrable (M2 \\<^isub>M M1) (\(x, y). f (y, x))" using f unfolding integrable_product_swap_iff . show ?INT using Q.integrable_fst_measurable(2)[OF Q_int] using integral_product_swap[of f] f by auto show ?AE using Q.integrable_fst_measurable(1)[OF Q_int] by simp qed lemma (in pair_sigma_finite) positive_integral_fst_measurable': assumes f: "(\x. f (fst x) (snd x)) \ borel_measurable (M1 \\<^isub>M M2)" shows "(\x. \\<^isup>+ y. f x y \M2) \ borel_measurable M1" using positive_integral_fst_measurable(1)[OF f] by simp lemma (in pair_sigma_finite) integral_fst_measurable: "(\x. f (fst x) (snd x)) \ borel_measurable (M1 \\<^isub>M M2) \ (\x. \ y. f x y \M2) \ borel_measurable M1" by (auto simp: lebesgue_integral_def intro!: borel_measurable_diff positive_integral_fst_measurable') lemma (in pair_sigma_finite) positive_integral_snd_measurable': assumes f: "(\x. f (fst x) (snd x)) \ borel_measurable (M1 \\<^isub>M M2)" shows "(\y. \\<^isup>+ x. f x y \M1) \ borel_measurable M2" proof - interpret Q: pair_sigma_finite M2 M1 .. show ?thesis using measurable_pair_swap[OF f] by (intro Q.positive_integral_fst_measurable') (simp add: split_beta') qed lemma (in pair_sigma_finite) integral_snd_measurable: "(\x. f (fst x) (snd x)) \ borel_measurable (M1 \\<^isub>M M2) \ (\y. \ x. f x y \M1) \ borel_measurable M2" by (auto simp: lebesgue_integral_def intro!: borel_measurable_diff positive_integral_snd_measurable') lemma (in pair_sigma_finite) Fubini_integral: assumes f: "integrable (M1 \\<^isub>M M2) f" shows "(\y. (\x. f (x, y) \M1) \M2) = (\x. (\y. f (x, y) \M2) \M1)" unfolding integrable_snd_measurable[OF assms] unfolding integrable_fst_measurable[OF assms] .. section {* Products on counting spaces, densities and distributions *} lemma sigma_sets_pair_measure_generator_finite: assumes "finite A" and "finite B" shows "sigma_sets (A \ B) { a \ b | a b. a \ A \ b \ B} = Pow (A \ B)" (is "sigma_sets ?prod ?sets = _") proof safe have fin: "finite (A \ B)" using assms by (rule finite_cartesian_product) fix x assume subset: "x \ A \ B" hence "finite x" using fin by (rule finite_subset) from this subset show "x \ sigma_sets ?prod ?sets" proof (induct x) case empty show ?case by (rule sigma_sets.Empty) next case (insert a x) hence "{a} \ sigma_sets ?prod ?sets" by auto moreover have "x \ sigma_sets ?prod ?sets" using insert by auto ultimately show ?case unfolding insert_is_Un[of a x] by (rule sigma_sets_Un) qed next fix x a b assume "x \ sigma_sets ?prod ?sets" and "(a, b) \ x" from sigma_sets_into_sp[OF _ this(1)] this(2) show "a \ A" and "b \ B" by auto qed lemma pair_measure_count_space: assumes A: "finite A" and B: "finite B" shows "count_space A \\<^isub>M count_space B = count_space (A \ B)" (is "?P = ?C") proof (rule measure_eqI) interpret A: finite_measure "count_space A" by (rule finite_measure_count_space) fact interpret B: finite_measure "count_space B" by (rule finite_measure_count_space) fact interpret P: pair_sigma_finite "count_space A" "count_space B" by default show eq: "sets ?P = sets ?C" by (simp add: sets_pair_measure sigma_sets_pair_measure_generator_finite A B) fix X assume X: "X \ sets ?P" with eq have X_subset: "X \ A \ B" by simp with A B have fin_Pair: "\x. finite (Pair x -` X)" by (intro finite_subset[OF _ B]) auto have fin_X: "finite X" using X_subset by (rule finite_subset) (auto simp: A B) show "emeasure ?P X = emeasure ?C X" apply (subst B.emeasure_pair_measure_alt[OF X]) apply (subst emeasure_count_space) using X_subset apply auto [] apply (simp add: fin_Pair emeasure_count_space X_subset fin_X) apply (subst positive_integral_count_space) using A apply simp apply (simp del: real_of_nat_setsum add: real_of_nat_setsum[symmetric]) apply (subst card_gt_0_iff) apply (simp add: fin_Pair) apply (subst card_SigmaI[symmetric]) using A apply simp using fin_Pair apply simp using X_subset apply (auto intro!: arg_cong[where f=card]) done qed lemma pair_measure_density: assumes f: "f \ borel_measurable M1" "AE x in M1. 0 \ f x" assumes g: "g \ borel_measurable M2" "AE x in M2. 0 \ g x" assumes "sigma_finite_measure M1" "sigma_finite_measure M2" assumes "sigma_finite_measure (density M1 f)" "sigma_finite_measure (density M2 g)" shows "density M1 f \\<^isub>M density M2 g = density (M1 \\<^isub>M M2) (\(x,y). f x * g y)" (is "?L = ?R") proof (rule measure_eqI) interpret M1: sigma_finite_measure M1 by fact interpret M2: sigma_finite_measure M2 by fact interpret D1: sigma_finite_measure "density M1 f" by fact interpret D2: sigma_finite_measure "density M2 g" by fact interpret L: pair_sigma_finite "density M1 f" "density M2 g" .. interpret R: pair_sigma_finite M1 M2 .. fix A assume A: "A \ sets ?L" then have indicator_eq: "\x y. indicator A (x, y) = indicator (Pair x -` A) y" and Pair_A: "\x. Pair x -` A \ sets M2" by (auto simp: indicator_def sets_Pair1) have f_fst: "(\p. f (fst p)) \ borel_measurable (M1 \\<^isub>M M2)" using measurable_comp[OF measurable_fst f(1)] by (simp add: comp_def) have g_snd: "(\p. g (snd p)) \ borel_measurable (M1 \\<^isub>M M2)" using measurable_comp[OF measurable_snd g(1)] by (simp add: comp_def) have "(\x. \\<^isup>+ y. g (snd (x, y)) * indicator A (x, y) \M2) \ borel_measurable M1" using g_snd Pair_A A by (intro R.positive_integral_fst_measurable) auto then have int_g: "(\x. \\<^isup>+ y. g y * indicator A (x, y) \M2) \ borel_measurable M1" by simp show "emeasure ?L A = emeasure ?R A" apply (subst D2.emeasure_pair_measure[OF A]) apply (subst emeasure_density) using f_fst g_snd apply (simp add: split_beta') using A apply simp apply (subst positive_integral_density[OF g]) apply (simp add: indicator_eq Pair_A) apply (subst positive_integral_density[OF f]) apply (rule int_g) apply (subst R.positive_integral_fst_measurable(2)[symmetric]) using f g A Pair_A f_fst g_snd apply (auto intro!: positive_integral_cong_AE R.measurable_emeasure_Pair1 simp: positive_integral_cmult indicator_eq split_beta') apply (intro AE_I2 impI) apply (subst mult_assoc) apply (subst positive_integral_cmult) apply auto done qed simp lemma sigma_finite_measure_distr: assumes "sigma_finite_measure (distr M N f)" and f: "f \ measurable M N" shows "sigma_finite_measure M" proof - interpret sigma_finite_measure "distr M N f" by fact from sigma_finite_disjoint guess A . note A = this show ?thesis proof (unfold_locales, intro conjI exI allI) show "range (\i. f -` A i \ space M) \ sets M" using A f by (auto intro!: measurable_sets) show "(\i. f -` A i \ space M) = space M" using A(1) A(2)[symmetric] f by (auto simp: measurable_def Pi_def) fix i show "emeasure M (f -` A i \ space M) \ \" using f A(1,2) A(3)[of i] by (simp add: emeasure_distr subset_eq) qed qed lemma measurable_cong': assumes sets: "sets M = sets M'" "sets N = sets N'" shows "measurable M N = measurable M' N'" using sets[THEN sets_eq_imp_space_eq] sets by (simp add: measurable_def) lemma pair_measure_distr: assumes f: "f \ measurable M S" and g: "g \ measurable N T" assumes "sigma_finite_measure (distr M S f)" "sigma_finite_measure (distr N T g)" shows "distr M S f \\<^isub>M distr N T g = distr (M \\<^isub>M N) (S \\<^isub>M T) (\(x, y). (f x, g y))" (is "?P = ?D") proof (rule measure_eqI) show "sets ?P = sets ?D" by simp interpret S: sigma_finite_measure "distr M S f" by fact interpret T: sigma_finite_measure "distr N T g" by fact interpret ST: pair_sigma_finite "distr M S f" "distr N T g" .. interpret M: sigma_finite_measure M by (rule sigma_finite_measure_distr) fact+ interpret N: sigma_finite_measure N by (rule sigma_finite_measure_distr) fact+ interpret MN: pair_sigma_finite M N .. interpret SN: pair_sigma_finite "distr M S f" N .. have [simp]: "\f g. fst \ (\(x, y). (f x, g y)) = f \ fst" "\f g. snd \ (\(x, y). (f x, g y)) = g \ snd" by auto then have fg: "(\(x, y). (f x, g y)) \ measurable (M \\<^isub>M N) (S \\<^isub>M T)" using measurable_comp[OF measurable_fst f] measurable_comp[OF measurable_snd g] by (auto simp: measurable_pair_iff) fix A assume A: "A \ sets ?P" then have "emeasure ?P A = (\\<^isup>+x. emeasure (distr N T g) (Pair x -` A) \distr M S f)" by (rule T.emeasure_pair_measure_alt) also have "\ = (\\<^isup>+x. emeasure N (g -` (Pair x -` A) \ space N) \distr M S f)" using g A by (simp add: sets_Pair1 emeasure_distr) also have "\ = (\\<^isup>+x. emeasure N (g -` (Pair (f x) -` A) \ space N) \M)" using f g A ST.measurable_emeasure_Pair1[OF A] by (intro positive_integral_distr) (auto simp add: sets_Pair1 emeasure_distr) also have "\ = (\\<^isup>+x. emeasure N (Pair x -` ((\(x, y). (f x, g y)) -` A \ space (M \\<^isub>M N))) \M)" by (intro positive_integral_cong arg_cong2[where f=emeasure]) (auto simp: space_pair_measure) also have "\ = emeasure (M \\<^isub>M N) ((\(x, y). (f x, g y)) -` A \ space (M \\<^isub>M N))" using fg by (intro N.emeasure_pair_measure_alt[symmetric] measurable_sets[OF _ A]) (auto cong: measurable_cong') also have "\ = emeasure ?D A" using fg A by (subst emeasure_distr) auto finally show "emeasure ?P A = emeasure ?D A" . qed end