1(* Title: HOL/Probability/Probability_Measure.thy 2 Author: Johannes H��lzl, TU M��nchen 3 Author: Armin Heller, TU M��nchen 4*) 5 6section \<open>Probability measure\<close> 7 8theory Probability_Measure 9 imports "HOL-Analysis.Analysis" 10begin 11 12locale prob_space = finite_measure + 13 assumes emeasure_space_1: "emeasure M (space M) = 1" 14 15lemma prob_spaceI[Pure.intro!]: 16 assumes *: "emeasure M (space M) = 1" 17 shows "prob_space M" 18proof - 19 interpret finite_measure M 20 proof 21 show "emeasure M (space M) \<noteq> \<infinity>" using * by simp 22 qed 23 show "prob_space M" by standard fact 24qed 25 26lemma prob_space_imp_sigma_finite: "prob_space M \<Longrightarrow> sigma_finite_measure M" 27 unfolding prob_space_def finite_measure_def by simp 28 29abbreviation (in prob_space) "events \<equiv> sets M" 30abbreviation (in prob_space) "prob \<equiv> measure M" 31abbreviation (in prob_space) "random_variable M' X \<equiv> X \<in> measurable M M'" 32abbreviation (in prob_space) "expectation \<equiv> integral\<^sup>L M" 33abbreviation (in prob_space) "variance X \<equiv> integral\<^sup>L M (\<lambda>x. (X x - expectation X)\<^sup>2)" 34 35lemma (in prob_space) finite_measure [simp]: "finite_measure M" 36 by unfold_locales 37 38lemma (in prob_space) prob_space_distr: 39 assumes f: "f \<in> measurable M M'" shows "prob_space (distr M M' f)" 40proof (rule prob_spaceI) 41 have "f -` space M' \<inter> space M = space M" using f by (auto dest: measurable_space) 42 with f show "emeasure (distr M M' f) (space (distr M M' f)) = 1" 43 by (auto simp: emeasure_distr emeasure_space_1) 44qed 45 46lemma prob_space_distrD: 47 assumes f: "f \<in> measurable M N" and M: "prob_space (distr M N f)" shows "prob_space M" 48proof 49 interpret M: prob_space "distr M N f" by fact 50 have "f -` space N \<inter> space M = space M" 51 using f[THEN measurable_space] by auto 52 then show "emeasure M (space M) = 1" 53 using M.emeasure_space_1 by (simp add: emeasure_distr[OF f]) 54qed 55 56lemma (in prob_space) prob_space: "prob (space M) = 1" 57 using emeasure_space_1 unfolding measure_def by (simp add: one_ennreal.rep_eq) 58 59lemma (in prob_space) prob_le_1[simp, intro]: "prob A \<le> 1" 60 using bounded_measure[of A] by (simp add: prob_space) 61 62lemma (in prob_space) not_empty: "space M \<noteq> {}" 63 using prob_space by auto 64 65lemma (in prob_space) emeasure_eq_1_AE: 66 "S \<in> sets M \<Longrightarrow> AE x in M. x \<in> S \<Longrightarrow> emeasure M S = 1" 67 by (subst emeasure_eq_AE[where B="space M"]) (auto simp: emeasure_space_1) 68 69lemma (in prob_space) emeasure_le_1: "emeasure M S \<le> 1" 70 unfolding ennreal_1[symmetric] emeasure_eq_measure by (subst ennreal_le_iff) auto 71 72lemma (in prob_space) emeasure_ge_1_iff: "emeasure M A \<ge> 1 \<longleftrightarrow> emeasure M A = 1" 73 by (rule iffI, intro antisym emeasure_le_1) simp_all 74 75lemma (in prob_space) AE_iff_emeasure_eq_1: 76 assumes [measurable]: "Measurable.pred M P" 77 shows "(AE x in M. P x) \<longleftrightarrow> emeasure M {x\<in>space M. P x} = 1" 78proof - 79 have *: "{x \<in> space M. \<not> P x} = space M - {x\<in>space M. P x}" 80 by auto 81 show ?thesis 82 by (auto simp add: ennreal_minus_eq_0 * emeasure_compl emeasure_space_1 AE_iff_measurable[OF _ refl] 83 intro: antisym emeasure_le_1) 84qed 85 86lemma (in prob_space) measure_le_1: "emeasure M X \<le> 1" 87 using emeasure_space[of M X] by (simp add: emeasure_space_1) 88 89lemma (in prob_space) measure_ge_1_iff: "measure M A \<ge> 1 \<longleftrightarrow> measure M A = 1" 90 by (auto intro!: antisym) 91 92lemma (in prob_space) AE_I_eq_1: 93 assumes "emeasure M {x\<in>space M. P x} = 1" "{x\<in>space M. P x} \<in> sets M" 94 shows "AE x in M. P x" 95proof (rule AE_I) 96 show "emeasure M (space M - {x \<in> space M. P x}) = 0" 97 using assms emeasure_space_1 by (simp add: emeasure_compl) 98qed (insert assms, auto) 99 100lemma prob_space_restrict_space: 101 "S \<in> sets M \<Longrightarrow> emeasure M S = 1 \<Longrightarrow> prob_space (restrict_space M S)" 102 by (intro prob_spaceI) 103 (simp add: emeasure_restrict_space space_restrict_space) 104 105lemma (in prob_space) prob_compl: 106 assumes A: "A \<in> events" 107 shows "prob (space M - A) = 1 - prob A" 108 using finite_measure_compl[OF A] by (simp add: prob_space) 109 110lemma (in prob_space) AE_in_set_eq_1: 111 assumes A[measurable]: "A \<in> events" shows "(AE x in M. x \<in> A) \<longleftrightarrow> prob A = 1" 112proof - 113 have *: "{x\<in>space M. x \<in> A} = A" 114 using A[THEN sets.sets_into_space] by auto 115 show ?thesis 116 by (subst AE_iff_emeasure_eq_1) (auto simp: emeasure_eq_measure *) 117qed 118 119lemma (in prob_space) AE_False: "(AE x in M. False) \<longleftrightarrow> False" 120proof 121 assume "AE x in M. False" 122 then have "AE x in M. x \<in> {}" by simp 123 then show False 124 by (subst (asm) AE_in_set_eq_1) auto 125qed simp 126 127lemma (in prob_space) AE_prob_1: 128 assumes "prob A = 1" shows "AE x in M. x \<in> A" 129proof - 130 from \<open>prob A = 1\<close> have "A \<in> events" 131 by (metis measure_notin_sets zero_neq_one) 132 with AE_in_set_eq_1 assms show ?thesis by simp 133qed 134 135lemma (in prob_space) AE_const[simp]: "(AE x in M. P) \<longleftrightarrow> P" 136 by (cases P) (auto simp: AE_False) 137 138lemma (in prob_space) ae_filter_bot: "ae_filter M \<noteq> bot" 139 by (simp add: trivial_limit_def) 140 141lemma (in prob_space) AE_contr: 142 assumes ae: "AE \<omega> in M. P \<omega>" "AE \<omega> in M. \<not> P \<omega>" 143 shows False 144proof - 145 from ae have "AE \<omega> in M. False" by eventually_elim auto 146 then show False by auto 147qed 148 149lemma (in prob_space) integral_ge_const: 150 fixes c :: real 151 shows "integrable M f \<Longrightarrow> (AE x in M. c \<le> f x) \<Longrightarrow> c \<le> (\<integral>x. f x \<partial>M)" 152 using integral_mono_AE[of M "\<lambda>x. c" f] prob_space by simp 153 154lemma (in prob_space) integral_le_const: 155 fixes c :: real 156 shows "integrable M f \<Longrightarrow> (AE x in M. f x \<le> c) \<Longrightarrow> (\<integral>x. f x \<partial>M) \<le> c" 157 using integral_mono_AE[of M f "\<lambda>x. c"] prob_space by simp 158 159lemma (in prob_space) nn_integral_ge_const: 160 "(AE x in M. c \<le> f x) \<Longrightarrow> c \<le> (\<integral>\<^sup>+x. f x \<partial>M)" 161 using nn_integral_mono_AE[of "\<lambda>x. c" f M] emeasure_space_1 162 by (simp split: if_split_asm) 163 164lemma (in prob_space) expectation_less: 165 fixes X :: "_ \<Rightarrow> real" 166 assumes [simp]: "integrable M X" 167 assumes gt: "AE x in M. X x < b" 168 shows "expectation X < b" 169proof - 170 have "expectation X < expectation (\<lambda>x. b)" 171 using gt emeasure_space_1 172 by (intro integral_less_AE_space) auto 173 then show ?thesis using prob_space by simp 174qed 175 176lemma (in prob_space) expectation_greater: 177 fixes X :: "_ \<Rightarrow> real" 178 assumes [simp]: "integrable M X" 179 assumes gt: "AE x in M. a < X x" 180 shows "a < expectation X" 181proof - 182 have "expectation (\<lambda>x. a) < expectation X" 183 using gt emeasure_space_1 184 by (intro integral_less_AE_space) auto 185 then show ?thesis using prob_space by simp 186qed 187 188lemma (in prob_space) jensens_inequality: 189 fixes q :: "real \<Rightarrow> real" 190 assumes X: "integrable M X" "AE x in M. X x \<in> I" 191 assumes I: "I = {a <..< b} \<or> I = {a <..} \<or> I = {..< b} \<or> I = UNIV" 192 assumes q: "integrable M (\<lambda>x. q (X x))" "convex_on I q" 193 shows "q (expectation X) \<le> expectation (\<lambda>x. q (X x))" 194proof - 195 let ?F = "\<lambda>x. Inf ((\<lambda>t. (q x - q t) / (x - t)) ` ({x<..} \<inter> I))" 196 from X(2) AE_False have "I \<noteq> {}" by auto 197 198 from I have "open I" by auto 199 200 note I 201 moreover 202 { assume "I \<subseteq> {a <..}" 203 with X have "a < expectation X" 204 by (intro expectation_greater) auto } 205 moreover 206 { assume "I \<subseteq> {..< b}" 207 with X have "expectation X < b" 208 by (intro expectation_less) auto } 209 ultimately have "expectation X \<in> I" 210 by (elim disjE) (auto simp: subset_eq) 211 moreover 212 { fix y assume y: "y \<in> I" 213 with q(2) \<open>open I\<close> have "Sup ((\<lambda>x. q x + ?F x * (y - x)) ` I) = q y" 214 by (auto intro!: cSup_eq_maximum convex_le_Inf_differential image_eqI [OF _ y] simp: interior_open) } 215 ultimately have "q (expectation X) = Sup ((\<lambda>x. q x + ?F x * (expectation X - x)) ` I)" 216 by simp 217 also have "\<dots> \<le> expectation (\<lambda>w. q (X w))" 218 proof (rule cSup_least) 219 show "(\<lambda>x. q x + ?F x * (expectation X - x)) ` I \<noteq> {}" 220 using \<open>I \<noteq> {}\<close> by auto 221 next 222 fix k assume "k \<in> (\<lambda>x. q x + ?F x * (expectation X - x)) ` I" 223 then guess x .. note x = this 224 have "q x + ?F x * (expectation X - x) = expectation (\<lambda>w. q x + ?F x * (X w - x))" 225 using prob_space by (simp add: X) 226 also have "\<dots> \<le> expectation (\<lambda>w. q (X w))" 227 using \<open>x \<in> I\<close> \<open>open I\<close> X(2) 228 apply (intro integral_mono_AE Bochner_Integration.integrable_add Bochner_Integration.integrable_mult_right Bochner_Integration.integrable_diff 229 integrable_const X q) 230 apply (elim eventually_mono) 231 apply (intro convex_le_Inf_differential) 232 apply (auto simp: interior_open q) 233 done 234 finally show "k \<le> expectation (\<lambda>w. q (X w))" using x by auto 235 qed 236 finally show "q (expectation X) \<le> expectation (\<lambda>x. q (X x))" . 237qed 238 239subsection \<open>Introduce binder for probability\<close> 240 241syntax 242 "_prob" :: "pttrn \<Rightarrow> logic \<Rightarrow> logic \<Rightarrow> logic" (\<open>('\<P>'((/_ in _./ _)'))\<close>) 243 244translations 245 "\<P>(x in M. P)" => "CONST measure M {x \<in> CONST space M. P}" 246 247print_translation \<open> 248 let 249 fun to_pattern (Const (\<^const_syntax>\<open>Pair\<close>, _) $ l $ r) = 250 Syntax.const \<^const_syntax>\<open>Pair\<close> :: to_pattern l @ to_pattern r 251 | to_pattern (t as (Const (\<^syntax_const>\<open>_bound\<close>, _)) $ _) = [t] 252 253 fun mk_pattern ((t, n) :: xs) = mk_patterns n xs |>> curry list_comb t 254 and mk_patterns 0 xs = ([], xs) 255 | mk_patterns n xs = 256 let 257 val (t, xs') = mk_pattern xs 258 val (ts, xs'') = mk_patterns (n - 1) xs' 259 in 260 (t :: ts, xs'') 261 end 262 263 fun unnest_tuples 264 (Const (\<^syntax_const>\<open>_pattern\<close>, _) $ 265 t1 $ 266 (t as (Const (\<^syntax_const>\<open>_pattern\<close>, _) $ _ $ _))) 267 = let 268 val (_ $ t2 $ t3) = unnest_tuples t 269 in 270 Syntax.const \<^syntax_const>\<open>_pattern\<close> $ 271 unnest_tuples t1 $ 272 (Syntax.const \<^syntax_const>\<open>_patterns\<close> $ t2 $ t3) 273 end 274 | unnest_tuples pat = pat 275 276 fun tr' [sig_alg, Const (\<^const_syntax>\<open>Collect\<close>, _) $ t] = 277 let 278 val bound_dummyT = Const (\<^syntax_const>\<open>_bound\<close>, dummyT) 279 280 fun go pattern elem 281 (Const (\<^const_syntax>\<open>conj\<close>, _) $ 282 (Const (\<^const_syntax>\<open>Set.member\<close>, _) $ elem' $ (Const (\<^const_syntax>\<open>space\<close>, _) $ sig_alg')) $ 283 u) 284 = let 285 val _ = if sig_alg aconv sig_alg' andalso to_pattern elem' = rev elem then () else raise Match; 286 val (pat, rest) = mk_pattern (rev pattern); 287 val _ = case rest of [] => () | _ => raise Match 288 in 289 Syntax.const \<^syntax_const>\<open>_prob\<close> $ unnest_tuples pat $ sig_alg $ u 290 end 291 | go pattern elem (Abs abs) = 292 let 293 val (x as (_ $ tx), t) = Syntax_Trans.atomic_abs_tr' abs 294 in 295 go ((x, 0) :: pattern) (bound_dummyT $ tx :: elem) t 296 end 297 | go pattern elem (Const (\<^const_syntax>\<open>case_prod\<close>, _) $ t) = 298 go 299 ((Syntax.const \<^syntax_const>\<open>_pattern\<close>, 2) :: pattern) 300 (Syntax.const \<^const_syntax>\<open>Pair\<close> :: elem) 301 t 302 in 303 go [] [] t 304 end 305 in 306 [(\<^const_syntax>\<open>Sigma_Algebra.measure\<close>, K tr')] 307 end 308\<close> 309 310definition 311 "cond_prob M P Q = \<P>(\<omega> in M. P \<omega> \<and> Q \<omega>) / \<P>(\<omega> in M. Q \<omega>)" 312 313syntax 314 "_conditional_prob" :: "pttrn \<Rightarrow> logic \<Rightarrow> logic \<Rightarrow> logic \<Rightarrow> logic" (\<open>('\<P>'(_ in _. _ \<bar>/ _'))\<close>) 315 316translations 317 "\<P>(x in M. P \<bar> Q)" => "CONST cond_prob M (\<lambda>x. P) (\<lambda>x. Q)" 318 319lemma (in prob_space) AE_E_prob: 320 assumes ae: "AE x in M. P x" 321 obtains S where "S \<subseteq> {x \<in> space M. P x}" "S \<in> events" "prob S = 1" 322proof - 323 from ae[THEN AE_E] guess N . 324 then show thesis 325 by (intro that[of "space M - N"]) 326 (auto simp: prob_compl prob_space emeasure_eq_measure measure_nonneg) 327qed 328 329lemma (in prob_space) prob_neg: "{x\<in>space M. P x} \<in> events \<Longrightarrow> \<P>(x in M. \<not> P x) = 1 - \<P>(x in M. P x)" 330 by (auto intro!: arg_cong[where f=prob] simp add: prob_compl[symmetric]) 331 332lemma (in prob_space) prob_eq_AE: 333 "(AE x in M. P x \<longleftrightarrow> Q x) \<Longrightarrow> {x\<in>space M. P x} \<in> events \<Longrightarrow> {x\<in>space M. Q x} \<in> events \<Longrightarrow> \<P>(x in M. P x) = \<P>(x in M. Q x)" 334 by (rule finite_measure_eq_AE) auto 335 336lemma (in prob_space) prob_eq_0_AE: 337 assumes not: "AE x in M. \<not> P x" shows "\<P>(x in M. P x) = 0" 338proof cases 339 assume "{x\<in>space M. P x} \<in> events" 340 with not have "\<P>(x in M. P x) = \<P>(x in M. False)" 341 by (intro prob_eq_AE) auto 342 then show ?thesis by simp 343qed (simp add: measure_notin_sets) 344 345lemma (in prob_space) prob_Collect_eq_0: 346 "{x \<in> space M. P x} \<in> sets M \<Longrightarrow> \<P>(x in M. P x) = 0 \<longleftrightarrow> (AE x in M. \<not> P x)" 347 using AE_iff_measurable[OF _ refl, of M "\<lambda>x. \<not> P x"] by (simp add: emeasure_eq_measure measure_nonneg) 348 349lemma (in prob_space) prob_Collect_eq_1: 350 "{x \<in> space M. P x} \<in> sets M \<Longrightarrow> \<P>(x in M. P x) = 1 \<longleftrightarrow> (AE x in M. P x)" 351 using AE_in_set_eq_1[of "{x\<in>space M. P x}"] by simp 352 353lemma (in prob_space) prob_eq_0: 354 "A \<in> sets M \<Longrightarrow> prob A = 0 \<longleftrightarrow> (AE x in M. x \<notin> A)" 355 using AE_iff_measurable[OF _ refl, of M "\<lambda>x. x \<notin> A"] 356 by (auto simp add: emeasure_eq_measure Int_def[symmetric] measure_nonneg) 357 358lemma (in prob_space) prob_eq_1: 359 "A \<in> sets M \<Longrightarrow> prob A = 1 \<longleftrightarrow> (AE x in M. x \<in> A)" 360 using AE_in_set_eq_1[of A] by simp 361 362lemma (in prob_space) prob_sums: 363 assumes P: "\<And>n. {x\<in>space M. P n x} \<in> events" 364 assumes Q: "{x\<in>space M. Q x} \<in> events" 365 assumes ae: "AE x in M. (\<forall>n. P n x \<longrightarrow> Q x) \<and> (Q x \<longrightarrow> (\<exists>!n. P n x))" 366 shows "(\<lambda>n. \<P>(x in M. P n x)) sums \<P>(x in M. Q x)" 367proof - 368 from ae[THEN AE_E_prob] guess S . note S = this 369 then have disj: "disjoint_family (\<lambda>n. {x\<in>space M. P n x} \<inter> S)" 370 by (auto simp: disjoint_family_on_def) 371 from S have ae_S: 372 "AE x in M. x \<in> {x\<in>space M. Q x} \<longleftrightarrow> x \<in> (\<Union>n. {x\<in>space M. P n x} \<inter> S)" 373 "\<And>n. AE x in M. x \<in> {x\<in>space M. P n x} \<longleftrightarrow> x \<in> {x\<in>space M. P n x} \<inter> S" 374 using ae by (auto dest!: AE_prob_1) 375 from ae_S have *: 376 "\<P>(x in M. Q x) = prob (\<Union>n. {x\<in>space M. P n x} \<inter> S)" 377 using P Q S by (intro finite_measure_eq_AE) auto 378 from ae_S have **: 379 "\<And>n. \<P>(x in M. P n x) = prob ({x\<in>space M. P n x} \<inter> S)" 380 using P Q S by (intro finite_measure_eq_AE) auto 381 show ?thesis 382 unfolding * ** using S P disj 383 by (intro finite_measure_UNION) auto 384qed 385 386lemma (in prob_space) prob_sum: 387 assumes [simp, intro]: "finite I" 388 assumes P: "\<And>n. n \<in> I \<Longrightarrow> {x\<in>space M. P n x} \<in> events" 389 assumes Q: "{x\<in>space M. Q x} \<in> events" 390 assumes ae: "AE x in M. (\<forall>n\<in>I. P n x \<longrightarrow> Q x) \<and> (Q x \<longrightarrow> (\<exists>!n\<in>I. P n x))" 391 shows "\<P>(x in M. Q x) = (\<Sum>n\<in>I. \<P>(x in M. P n x))" 392proof - 393 from ae[THEN AE_E_prob] guess S . note S = this 394 then have disj: "disjoint_family_on (\<lambda>n. {x\<in>space M. P n x} \<inter> S) I" 395 by (auto simp: disjoint_family_on_def) 396 from S have ae_S: 397 "AE x in M. x \<in> {x\<in>space M. Q x} \<longleftrightarrow> x \<in> (\<Union>n\<in>I. {x\<in>space M. P n x} \<inter> S)" 398 "\<And>n. n \<in> I \<Longrightarrow> AE x in M. x \<in> {x\<in>space M. P n x} \<longleftrightarrow> x \<in> {x\<in>space M. P n x} \<inter> S" 399 using ae by (auto dest!: AE_prob_1) 400 from ae_S have *: 401 "\<P>(x in M. Q x) = prob (\<Union>n\<in>I. {x\<in>space M. P n x} \<inter> S)" 402 using P Q S by (intro finite_measure_eq_AE) (auto intro!: sets.Int) 403 from ae_S have **: 404 "\<And>n. n \<in> I \<Longrightarrow> \<P>(x in M. P n x) = prob ({x\<in>space M. P n x} \<inter> S)" 405 using P Q S by (intro finite_measure_eq_AE) auto 406 show ?thesis 407 using S P disj 408 by (auto simp add: * ** simp del: UN_simps intro!: finite_measure_finite_Union) 409qed 410 411lemma (in prob_space) prob_EX_countable: 412 assumes sets: "\<And>i. i \<in> I \<Longrightarrow> {x\<in>space M. P i x} \<in> sets M" and I: "countable I" 413 assumes disj: "AE x in M. \<forall>i\<in>I. \<forall>j\<in>I. P i x \<longrightarrow> P j x \<longrightarrow> i = j" 414 shows "\<P>(x in M. \<exists>i\<in>I. P i x) = (\<integral>\<^sup>+i. \<P>(x in M. P i x) \<partial>count_space I)" 415proof - 416 let ?N= "\<lambda>x. \<exists>!i\<in>I. P i x" 417 have "ennreal (\<P>(x in M. \<exists>i\<in>I. P i x)) = \<P>(x in M. (\<exists>i\<in>I. P i x \<and> ?N x))" 418 unfolding ennreal_inj[OF measure_nonneg measure_nonneg] 419 proof (rule prob_eq_AE) 420 show "AE x in M. (\<exists>i\<in>I. P i x) = (\<exists>i\<in>I. P i x \<and> ?N x)" 421 using disj by eventually_elim blast 422 qed (auto intro!: sets.sets_Collect_countable_Ex' sets.sets_Collect_conj sets.sets_Collect_countable_Ex1' I sets)+ 423 also have "\<P>(x in M. (\<exists>i\<in>I. P i x \<and> ?N x)) = emeasure M (\<Union>i\<in>I. {x\<in>space M. P i x \<and> ?N x})" 424 unfolding emeasure_eq_measure by (auto intro!: arg_cong[where f=prob] simp: measure_nonneg) 425 also have "\<dots> = (\<integral>\<^sup>+i. emeasure M {x\<in>space M. P i x \<and> ?N x} \<partial>count_space I)" 426 by (rule emeasure_UN_countable) 427 (auto intro!: sets.sets_Collect_countable_Ex' sets.sets_Collect_conj sets.sets_Collect_countable_Ex1' I sets 428 simp: disjoint_family_on_def) 429 also have "\<dots> = (\<integral>\<^sup>+i. \<P>(x in M. P i x) \<partial>count_space I)" 430 unfolding emeasure_eq_measure using disj 431 by (intro nn_integral_cong ennreal_inj[THEN iffD2] prob_eq_AE) 432 (auto intro!: sets.sets_Collect_countable_Ex' sets.sets_Collect_conj sets.sets_Collect_countable_Ex1' I sets measure_nonneg)+ 433 finally show ?thesis . 434qed 435 436lemma (in prob_space) cond_prob_eq_AE: 437 assumes P: "AE x in M. Q x \<longrightarrow> P x \<longleftrightarrow> P' x" "{x\<in>space M. P x} \<in> events" "{x\<in>space M. P' x} \<in> events" 438 assumes Q: "AE x in M. Q x \<longleftrightarrow> Q' x" "{x\<in>space M. Q x} \<in> events" "{x\<in>space M. Q' x} \<in> events" 439 shows "cond_prob M P Q = cond_prob M P' Q'" 440 using P Q 441 by (auto simp: cond_prob_def intro!: arg_cong2[where f="(/)"] prob_eq_AE sets.sets_Collect_conj) 442 443 444lemma (in prob_space) joint_distribution_Times_le_fst: 445 "random_variable MX X \<Longrightarrow> random_variable MY Y \<Longrightarrow> A \<in> sets MX \<Longrightarrow> B \<in> sets MY 446 \<Longrightarrow> emeasure (distr M (MX \<Otimes>\<^sub>M MY) (\<lambda>x. (X x, Y x))) (A \<times> B) \<le> emeasure (distr M MX X) A" 447 by (auto simp: emeasure_distr measurable_pair_iff comp_def intro!: emeasure_mono measurable_sets) 448 449lemma (in prob_space) joint_distribution_Times_le_snd: 450 "random_variable MX X \<Longrightarrow> random_variable MY Y \<Longrightarrow> A \<in> sets MX \<Longrightarrow> B \<in> sets MY 451 \<Longrightarrow> emeasure (distr M (MX \<Otimes>\<^sub>M MY) (\<lambda>x. (X x, Y x))) (A \<times> B) \<le> emeasure (distr M MY Y) B" 452 by (auto simp: emeasure_distr measurable_pair_iff comp_def intro!: emeasure_mono measurable_sets) 453 454lemma (in prob_space) variance_eq: 455 fixes X :: "'a \<Rightarrow> real" 456 assumes [simp]: "integrable M X" 457 assumes [simp]: "integrable M (\<lambda>x. (X x)\<^sup>2)" 458 shows "variance X = expectation (\<lambda>x. (X x)\<^sup>2) - (expectation X)\<^sup>2" 459 by (simp add: field_simps prob_space power2_diff power2_eq_square[symmetric]) 460 461lemma (in prob_space) variance_positive: "0 \<le> variance (X::'a \<Rightarrow> real)" 462 by (intro integral_nonneg_AE) (auto intro!: integral_nonneg_AE) 463 464lemma (in prob_space) variance_mean_zero: 465 "expectation X = 0 \<Longrightarrow> variance X = expectation (\<lambda>x. (X x)^2)" 466 by simp 467 468locale pair_prob_space = pair_sigma_finite M1 M2 + M1: prob_space M1 + M2: prob_space M2 for M1 M2 469 470sublocale pair_prob_space \<subseteq> P?: prob_space "M1 \<Otimes>\<^sub>M M2" 471proof 472 show "emeasure (M1 \<Otimes>\<^sub>M M2) (space (M1 \<Otimes>\<^sub>M M2)) = 1" 473 by (simp add: M2.emeasure_pair_measure_Times M1.emeasure_space_1 M2.emeasure_space_1 space_pair_measure) 474qed 475 476locale product_prob_space = product_sigma_finite M for M :: "'i \<Rightarrow> 'a measure" + 477 fixes I :: "'i set" 478 assumes prob_space: "\<And>i. prob_space (M i)" 479 480sublocale product_prob_space \<subseteq> M?: prob_space "M i" for i 481 by (rule prob_space) 482 483locale finite_product_prob_space = finite_product_sigma_finite M I + product_prob_space M I for M I 484 485sublocale finite_product_prob_space \<subseteq> prob_space "\<Pi>\<^sub>M i\<in>I. M i" 486proof 487 show "emeasure (\<Pi>\<^sub>M i\<in>I. M i) (space (\<Pi>\<^sub>M i\<in>I. M i)) = 1" 488 by (simp add: measure_times M.emeasure_space_1 prod.neutral_const space_PiM) 489qed 490 491lemma (in finite_product_prob_space) prob_times: 492 assumes X: "\<And>i. i \<in> I \<Longrightarrow> X i \<in> sets (M i)" 493 shows "prob (\<Pi>\<^sub>E i\<in>I. X i) = (\<Prod>i\<in>I. M.prob i (X i))" 494proof - 495 have "ennreal (measure (\<Pi>\<^sub>M i\<in>I. M i) (\<Pi>\<^sub>E i\<in>I. X i)) = emeasure (\<Pi>\<^sub>M i\<in>I. M i) (\<Pi>\<^sub>E i\<in>I. X i)" 496 using X by (simp add: emeasure_eq_measure) 497 also have "\<dots> = (\<Prod>i\<in>I. emeasure (M i) (X i))" 498 using measure_times X by simp 499 also have "\<dots> = ennreal (\<Prod>i\<in>I. measure (M i) (X i))" 500 using X by (simp add: M.emeasure_eq_measure prod_ennreal measure_nonneg) 501 finally show ?thesis by (simp add: measure_nonneg prod_nonneg) 502qed 503 504subsection \<open>Distributions\<close> 505 506definition distributed :: "'a measure \<Rightarrow> 'b measure \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> ennreal) \<Rightarrow> bool" 507where 508 "distributed M N X f \<longleftrightarrow> 509 distr M N X = density N f \<and> f \<in> borel_measurable N \<and> X \<in> measurable M N" 510 511lemma 512 assumes "distributed M N X f" 513 shows distributed_distr_eq_density: "distr M N X = density N f" 514 and distributed_measurable: "X \<in> measurable M N" 515 and distributed_borel_measurable: "f \<in> borel_measurable N" 516 using assms by (simp_all add: distributed_def) 517 518lemma 519 assumes D: "distributed M N X f" 520 shows distributed_measurable'[measurable_dest]: 521 "g \<in> measurable L M \<Longrightarrow> (\<lambda>x. X (g x)) \<in> measurable L N" 522 and distributed_borel_measurable'[measurable_dest]: 523 "h \<in> measurable L N \<Longrightarrow> (\<lambda>x. f (h x)) \<in> borel_measurable L" 524 using distributed_measurable[OF D] distributed_borel_measurable[OF D] 525 by simp_all 526 527lemma distributed_real_measurable: 528 "(\<And>x. x \<in> space N \<Longrightarrow> 0 \<le> f x) \<Longrightarrow> distributed M N X (\<lambda>x. ennreal (f x)) \<Longrightarrow> f \<in> borel_measurable N" 529 by (simp_all add: distributed_def) 530 531lemma distributed_real_measurable': 532 "(\<And>x. x \<in> space N \<Longrightarrow> 0 \<le> f x) \<Longrightarrow> distributed M N X (\<lambda>x. ennreal (f x)) \<Longrightarrow> 533 h \<in> measurable L N \<Longrightarrow> (\<lambda>x. f (h x)) \<in> borel_measurable L" 534 using distributed_real_measurable[measurable] by simp 535 536lemma joint_distributed_measurable1: 537 "distributed M (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x)) f \<Longrightarrow> h1 \<in> measurable N M \<Longrightarrow> (\<lambda>x. X (h1 x)) \<in> measurable N S" 538 by simp 539 540lemma joint_distributed_measurable2: 541 "distributed M (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x)) f \<Longrightarrow> h2 \<in> measurable N M \<Longrightarrow> (\<lambda>x. Y (h2 x)) \<in> measurable N T" 542 by simp 543 544lemma distributed_count_space: 545 assumes X: "distributed M (count_space A) X P" and a: "a \<in> A" and A: "finite A" 546 shows "P a = emeasure M (X -` {a} \<inter> space M)" 547proof - 548 have "emeasure M (X -` {a} \<inter> space M) = emeasure (distr M (count_space A) X) {a}" 549 using X a A by (simp add: emeasure_distr) 550 also have "\<dots> = emeasure (density (count_space A) P) {a}" 551 using X by (simp add: distributed_distr_eq_density) 552 also have "\<dots> = (\<integral>\<^sup>+x. P a * indicator {a} x \<partial>count_space A)" 553 using X a by (auto simp add: emeasure_density distributed_def indicator_def intro!: nn_integral_cong) 554 also have "\<dots> = P a" 555 using X a by (subst nn_integral_cmult_indicator) (auto simp: distributed_def one_ennreal_def[symmetric] AE_count_space) 556 finally show ?thesis .. 557qed 558 559lemma distributed_cong_density: 560 "(AE x in N. f x = g x) \<Longrightarrow> g \<in> borel_measurable N \<Longrightarrow> f \<in> borel_measurable N \<Longrightarrow> 561 distributed M N X f \<longleftrightarrow> distributed M N X g" 562 by (auto simp: distributed_def intro!: density_cong) 563 564lemma (in prob_space) distributed_imp_emeasure_nonzero: 565 assumes X: "distributed M MX X Px" 566 shows "emeasure MX {x \<in> space MX. Px x \<noteq> 0} \<noteq> 0" 567proof 568 note Px = distributed_borel_measurable[OF X] 569 interpret X: prob_space "distr M MX X" 570 using distributed_measurable[OF X] by (rule prob_space_distr) 571 572 assume "emeasure MX {x \<in> space MX. Px x \<noteq> 0} = 0" 573 with Px have "AE x in MX. Px x = 0" 574 by (intro AE_I[OF subset_refl]) (auto simp: borel_measurable_ennreal_iff) 575 moreover 576 from X.emeasure_space_1 have "(\<integral>\<^sup>+x. Px x \<partial>MX) = 1" 577 unfolding distributed_distr_eq_density[OF X] using Px 578 by (subst (asm) emeasure_density) 579 (auto simp: borel_measurable_ennreal_iff intro!: integral_cong cong: nn_integral_cong) 580 ultimately show False 581 by (simp add: nn_integral_cong_AE) 582qed 583 584lemma subdensity: 585 assumes T: "T \<in> measurable P Q" 586 assumes f: "distributed M P X f" 587 assumes g: "distributed M Q Y g" 588 assumes Y: "Y = T \<circ> X" 589 shows "AE x in P. g (T x) = 0 \<longrightarrow> f x = 0" 590proof - 591 have "{x\<in>space Q. g x = 0} \<in> null_sets (distr M Q (T \<circ> X))" 592 using g Y by (auto simp: null_sets_density_iff distributed_def) 593 also have "distr M Q (T \<circ> X) = distr (distr M P X) Q T" 594 using T f[THEN distributed_measurable] by (rule distr_distr[symmetric]) 595 finally have "T -` {x\<in>space Q. g x = 0} \<inter> space P \<in> null_sets (distr M P X)" 596 using T by (subst (asm) null_sets_distr_iff) auto 597 also have "T -` {x\<in>space Q. g x = 0} \<inter> space P = {x\<in>space P. g (T x) = 0}" 598 using T by (auto dest: measurable_space) 599 finally show ?thesis 600 using f g by (auto simp add: null_sets_density_iff distributed_def) 601qed 602 603lemma subdensity_real: 604 fixes g :: "'a \<Rightarrow> real" and f :: "'b \<Rightarrow> real" 605 assumes T: "T \<in> measurable P Q" 606 assumes f: "distributed M P X f" 607 assumes g: "distributed M Q Y g" 608 assumes Y: "Y = T \<circ> X" 609 shows "(AE x in P. 0 \<le> g (T x)) \<Longrightarrow> (AE x in P. 0 \<le> f x) \<Longrightarrow> AE x in P. g (T x) = 0 \<longrightarrow> f x = 0" 610 using subdensity[OF T, of M X "\<lambda>x. ennreal (f x)" Y "\<lambda>x. ennreal (g x)"] assms 611 by auto 612 613lemma distributed_emeasure: 614 "distributed M N X f \<Longrightarrow> A \<in> sets N \<Longrightarrow> emeasure M (X -` A \<inter> space M) = (\<integral>\<^sup>+x. f x * indicator A x \<partial>N)" 615 by (auto simp: distributed_distr_eq_density[symmetric] emeasure_density[symmetric] emeasure_distr) 616 617lemma distributed_nn_integral: 618 "distributed M N X f \<Longrightarrow> g \<in> borel_measurable N \<Longrightarrow> (\<integral>\<^sup>+x. f x * g x \<partial>N) = (\<integral>\<^sup>+x. g (X x) \<partial>M)" 619 by (auto simp: distributed_distr_eq_density[symmetric] nn_integral_density[symmetric] nn_integral_distr) 620 621lemma distributed_integral: 622 "distributed M N X f \<Longrightarrow> g \<in> borel_measurable N \<Longrightarrow> (\<And>x. x \<in> space N \<Longrightarrow> 0 \<le> f x) \<Longrightarrow> 623 (\<integral>x. f x * g x \<partial>N) = (\<integral>x. g (X x) \<partial>M)" 624 supply distributed_real_measurable[measurable] 625 by (auto simp: distributed_distr_eq_density[symmetric] integral_real_density[symmetric] integral_distr) 626 627lemma distributed_transform_integral: 628 assumes Px: "distributed M N X Px" "\<And>x. x \<in> space N \<Longrightarrow> 0 \<le> Px x" 629 assumes "distributed M P Y Py" "\<And>x. x \<in> space P \<Longrightarrow> 0 \<le> Py x" 630 assumes Y: "Y = T \<circ> X" and T: "T \<in> measurable N P" and f: "f \<in> borel_measurable P" 631 shows "(\<integral>x. Py x * f x \<partial>P) = (\<integral>x. Px x * f (T x) \<partial>N)" 632proof - 633 have "(\<integral>x. Py x * f x \<partial>P) = (\<integral>x. f (Y x) \<partial>M)" 634 by (rule distributed_integral) fact+ 635 also have "\<dots> = (\<integral>x. f (T (X x)) \<partial>M)" 636 using Y by simp 637 also have "\<dots> = (\<integral>x. Px x * f (T x) \<partial>N)" 638 using measurable_comp[OF T f] Px by (intro distributed_integral[symmetric]) (auto simp: comp_def) 639 finally show ?thesis . 640qed 641 642lemma (in prob_space) distributed_unique: 643 assumes Px: "distributed M S X Px" 644 assumes Py: "distributed M S X Py" 645 shows "AE x in S. Px x = Py x" 646proof - 647 interpret X: prob_space "distr M S X" 648 using Px by (intro prob_space_distr) simp 649 have "sigma_finite_measure (distr M S X)" .. 650 with sigma_finite_density_unique[of Px S Py ] Px Py 651 show ?thesis 652 by (auto simp: distributed_def) 653qed 654 655lemma (in prob_space) distributed_jointI: 656 assumes "sigma_finite_measure S" "sigma_finite_measure T" 657 assumes X[measurable]: "X \<in> measurable M S" and Y[measurable]: "Y \<in> measurable M T" 658 assumes [measurable]: "f \<in> borel_measurable (S \<Otimes>\<^sub>M T)" and f: "AE x in S \<Otimes>\<^sub>M T. 0 \<le> f x" 659 assumes eq: "\<And>A B. A \<in> sets S \<Longrightarrow> B \<in> sets T \<Longrightarrow> 660 emeasure M {x \<in> space M. X x \<in> A \<and> Y x \<in> B} = (\<integral>\<^sup>+x. (\<integral>\<^sup>+y. f (x, y) * indicator B y \<partial>T) * indicator A x \<partial>S)" 661 shows "distributed M (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x)) f" 662 unfolding distributed_def 663proof safe 664 interpret S: sigma_finite_measure S by fact 665 interpret T: sigma_finite_measure T by fact 666 interpret ST: pair_sigma_finite S T .. 667 668 from ST.sigma_finite_up_in_pair_measure_generator guess F :: "nat \<Rightarrow> ('b \<times> 'c) set" .. note F = this 669 let ?E = "{a \<times> b |a b. a \<in> sets S \<and> b \<in> sets T}" 670 let ?P = "S \<Otimes>\<^sub>M T" 671 show "distr M ?P (\<lambda>x. (X x, Y x)) = density ?P f" (is "?L = ?R") 672 proof (rule measure_eqI_generator_eq[OF Int_stable_pair_measure_generator[of S T]]) 673 show "?E \<subseteq> Pow (space ?P)" 674 using sets.space_closed[of S] sets.space_closed[of T] by (auto simp: space_pair_measure) 675 show "sets ?L = sigma_sets (space ?P) ?E" 676 by (simp add: sets_pair_measure space_pair_measure) 677 then show "sets ?R = sigma_sets (space ?P) ?E" 678 by simp 679 next 680 interpret L: prob_space ?L 681 by (rule prob_space_distr) (auto intro!: measurable_Pair) 682 show "range F \<subseteq> ?E" "(\<Union>i. F i) = space ?P" "\<And>i. emeasure ?L (F i) \<noteq> \<infinity>" 683 using F by (auto simp: space_pair_measure) 684 next 685 fix E assume "E \<in> ?E" 686 then obtain A B where E[simp]: "E = A \<times> B" 687 and A[measurable]: "A \<in> sets S" and B[measurable]: "B \<in> sets T" by auto 688 have "emeasure ?L E = emeasure M {x \<in> space M. X x \<in> A \<and> Y x \<in> B}" 689 by (auto intro!: arg_cong[where f="emeasure M"] simp add: emeasure_distr measurable_Pair) 690 also have "\<dots> = (\<integral>\<^sup>+x. (\<integral>\<^sup>+y. (f (x, y) * indicator B y) * indicator A x \<partial>T) \<partial>S)" 691 using f by (auto simp add: eq nn_integral_multc intro!: nn_integral_cong) 692 also have "\<dots> = emeasure ?R E" 693 by (auto simp add: emeasure_density T.nn_integral_fst[symmetric] 694 intro!: nn_integral_cong split: split_indicator) 695 finally show "emeasure ?L E = emeasure ?R E" . 696 qed 697qed (auto simp: f) 698 699lemma (in prob_space) distributed_swap: 700 assumes "sigma_finite_measure S" "sigma_finite_measure T" 701 assumes Pxy: "distributed M (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x)) Pxy" 702 shows "distributed M (T \<Otimes>\<^sub>M S) (\<lambda>x. (Y x, X x)) (\<lambda>(x, y). Pxy (y, x))" 703proof - 704 interpret S: sigma_finite_measure S by fact 705 interpret T: sigma_finite_measure T by fact 706 interpret ST: pair_sigma_finite S T .. 707 interpret TS: pair_sigma_finite T S .. 708 709 note Pxy[measurable] 710 show ?thesis 711 apply (subst TS.distr_pair_swap) 712 unfolding distributed_def 713 proof safe 714 let ?D = "distr (S \<Otimes>\<^sub>M T) (T \<Otimes>\<^sub>M S) (\<lambda>(x, y). (y, x))" 715 show 1: "(\<lambda>(x, y). Pxy (y, x)) \<in> borel_measurable ?D" 716 by auto 717 show 2: "random_variable (distr (S \<Otimes>\<^sub>M T) (T \<Otimes>\<^sub>M S) (\<lambda>(x, y). (y, x))) (\<lambda>x. (Y x, X x))" 718 using Pxy by auto 719 { fix A assume A: "A \<in> sets (T \<Otimes>\<^sub>M S)" 720 let ?B = "(\<lambda>(x, y). (y, x)) -` A \<inter> space (S \<Otimes>\<^sub>M T)" 721 from sets.sets_into_space[OF A] 722 have "emeasure M ((\<lambda>x. (Y x, X x)) -` A \<inter> space M) = 723 emeasure M ((\<lambda>x. (X x, Y x)) -` ?B \<inter> space M)" 724 by (auto intro!: arg_cong2[where f=emeasure] simp: space_pair_measure) 725 also have "\<dots> = (\<integral>\<^sup>+ x. Pxy x * indicator ?B x \<partial>(S \<Otimes>\<^sub>M T))" 726 using Pxy A by (intro distributed_emeasure) auto 727 finally have "emeasure M ((\<lambda>x. (Y x, X x)) -` A \<inter> space M) = 728 (\<integral>\<^sup>+ x. Pxy x * indicator A (snd x, fst x) \<partial>(S \<Otimes>\<^sub>M T))" 729 by (auto intro!: nn_integral_cong split: split_indicator) } 730 note * = this 731 show "distr M ?D (\<lambda>x. (Y x, X x)) = density ?D (\<lambda>(x, y). Pxy (y, x))" 732 apply (intro measure_eqI) 733 apply (simp_all add: emeasure_distr[OF 2] emeasure_density[OF 1]) 734 apply (subst nn_integral_distr) 735 apply (auto intro!: * simp: comp_def split_beta) 736 done 737 qed 738qed 739 740lemma (in prob_space) distr_marginal1: 741 assumes "sigma_finite_measure S" "sigma_finite_measure T" 742 assumes Pxy: "distributed M (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x)) Pxy" 743 defines "Px \<equiv> \<lambda>x. (\<integral>\<^sup>+z. Pxy (x, z) \<partial>T)" 744 shows "distributed M S X Px" 745 unfolding distributed_def 746proof safe 747 interpret S: sigma_finite_measure S by fact 748 interpret T: sigma_finite_measure T by fact 749 interpret ST: pair_sigma_finite S T .. 750 751 note Pxy[measurable] 752 show X: "X \<in> measurable M S" by simp 753 754 show borel: "Px \<in> borel_measurable S" 755 by (auto intro!: T.nn_integral_fst simp: Px_def) 756 757 interpret Pxy: prob_space "distr M (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x))" 758 by (intro prob_space_distr) simp 759 760 show "distr M S X = density S Px" 761 proof (rule measure_eqI) 762 fix A assume A: "A \<in> sets (distr M S X)" 763 with X measurable_space[of Y M T] 764 have "emeasure (distr M S X) A = emeasure (distr M (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x))) (A \<times> space T)" 765 by (auto simp add: emeasure_distr intro!: arg_cong[where f="emeasure M"]) 766 also have "\<dots> = emeasure (density (S \<Otimes>\<^sub>M T) Pxy) (A \<times> space T)" 767 using Pxy by (simp add: distributed_def) 768 also have "\<dots> = \<integral>\<^sup>+ x. \<integral>\<^sup>+ y. Pxy (x, y) * indicator (A \<times> space T) (x, y) \<partial>T \<partial>S" 769 using A borel Pxy 770 by (simp add: emeasure_density T.nn_integral_fst[symmetric]) 771 also have "\<dots> = \<integral>\<^sup>+ x. Px x * indicator A x \<partial>S" 772 proof (rule nn_integral_cong) 773 fix x assume "x \<in> space S" 774 moreover have eq: "\<And>y. y \<in> space T \<Longrightarrow> indicator (A \<times> space T) (x, y) = indicator A x" 775 by (auto simp: indicator_def) 776 ultimately have "(\<integral>\<^sup>+ y. Pxy (x, y) * indicator (A \<times> space T) (x, y) \<partial>T) = (\<integral>\<^sup>+ y. Pxy (x, y) \<partial>T) * indicator A x" 777 by (simp add: eq nn_integral_multc cong: nn_integral_cong) 778 also have "(\<integral>\<^sup>+ y. Pxy (x, y) \<partial>T) = Px x" 779 by (simp add: Px_def) 780 finally show "(\<integral>\<^sup>+ y. Pxy (x, y) * indicator (A \<times> space T) (x, y) \<partial>T) = Px x * indicator A x" . 781 qed 782 finally show "emeasure (distr M S X) A = emeasure (density S Px) A" 783 using A borel Pxy by (simp add: emeasure_density) 784 qed simp 785qed 786 787lemma (in prob_space) distr_marginal2: 788 assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T" 789 assumes Pxy: "distributed M (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x)) Pxy" 790 shows "distributed M T Y (\<lambda>y. (\<integral>\<^sup>+x. Pxy (x, y) \<partial>S))" 791 using distr_marginal1[OF T S distributed_swap[OF S T]] Pxy by simp 792 793lemma (in prob_space) distributed_marginal_eq_joint1: 794 assumes T: "sigma_finite_measure T" 795 assumes S: "sigma_finite_measure S" 796 assumes Px: "distributed M S X Px" 797 assumes Pxy: "distributed M (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x)) Pxy" 798 shows "AE x in S. Px x = (\<integral>\<^sup>+y. Pxy (x, y) \<partial>T)" 799 using Px distr_marginal1[OF S T Pxy] by (rule distributed_unique) 800 801lemma (in prob_space) distributed_marginal_eq_joint2: 802 assumes T: "sigma_finite_measure T" 803 assumes S: "sigma_finite_measure S" 804 assumes Py: "distributed M T Y Py" 805 assumes Pxy: "distributed M (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x)) Pxy" 806 shows "AE y in T. Py y = (\<integral>\<^sup>+x. Pxy (x, y) \<partial>S)" 807 using Py distr_marginal2[OF S T Pxy] by (rule distributed_unique) 808 809lemma (in prob_space) distributed_joint_indep': 810 assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T" 811 assumes X[measurable]: "distributed M S X Px" and Y[measurable]: "distributed M T Y Py" 812 assumes indep: "distr M S X \<Otimes>\<^sub>M distr M T Y = distr M (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x))" 813 shows "distributed M (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x)) (\<lambda>(x, y). Px x * Py y)" 814 unfolding distributed_def 815proof safe 816 interpret S: sigma_finite_measure S by fact 817 interpret T: sigma_finite_measure T by fact 818 interpret ST: pair_sigma_finite S T .. 819 820 interpret X: prob_space "density S Px" 821 unfolding distributed_distr_eq_density[OF X, symmetric] 822 by (rule prob_space_distr) simp 823 have sf_X: "sigma_finite_measure (density S Px)" .. 824 825 interpret Y: prob_space "density T Py" 826 unfolding distributed_distr_eq_density[OF Y, symmetric] 827 by (rule prob_space_distr) simp 828 have sf_Y: "sigma_finite_measure (density T Py)" .. 829 830 show "distr M (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x)) = density (S \<Otimes>\<^sub>M T) (\<lambda>(x, y). Px x * Py y)" 831 unfolding indep[symmetric] distributed_distr_eq_density[OF X] distributed_distr_eq_density[OF Y] 832 using distributed_borel_measurable[OF X] 833 using distributed_borel_measurable[OF Y] 834 by (rule pair_measure_density[OF _ _ T sf_Y]) 835 836 show "random_variable (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x))" by auto 837 838 show Pxy: "(\<lambda>(x, y). Px x * Py y) \<in> borel_measurable (S \<Otimes>\<^sub>M T)" by auto 839qed 840 841lemma distributed_integrable: 842 "distributed M N X f \<Longrightarrow> g \<in> borel_measurable N \<Longrightarrow> (\<And>x. x \<in> space N \<Longrightarrow> 0 \<le> f x) \<Longrightarrow> 843 integrable N (\<lambda>x. f x * g x) \<longleftrightarrow> integrable M (\<lambda>x. g (X x))" 844 supply distributed_real_measurable[measurable] 845 by (auto simp: distributed_distr_eq_density[symmetric] integrable_real_density[symmetric] integrable_distr_eq) 846 847lemma distributed_transform_integrable: 848 assumes Px: "distributed M N X Px" "\<And>x. x \<in> space N \<Longrightarrow> 0 \<le> Px x" 849 assumes "distributed M P Y Py" "\<And>x. x \<in> space P \<Longrightarrow> 0 \<le> Py x" 850 assumes Y: "Y = (\<lambda>x. T (X x))" and T: "T \<in> measurable N P" and f: "f \<in> borel_measurable P" 851 shows "integrable P (\<lambda>x. Py x * f x) \<longleftrightarrow> integrable N (\<lambda>x. Px x * f (T x))" 852proof - 853 have "integrable P (\<lambda>x. Py x * f x) \<longleftrightarrow> integrable M (\<lambda>x. f (Y x))" 854 by (rule distributed_integrable) fact+ 855 also have "\<dots> \<longleftrightarrow> integrable M (\<lambda>x. f (T (X x)))" 856 using Y by simp 857 also have "\<dots> \<longleftrightarrow> integrable N (\<lambda>x. Px x * f (T x))" 858 using measurable_comp[OF T f] Px by (intro distributed_integrable[symmetric]) (auto simp: comp_def) 859 finally show ?thesis . 860qed 861 862lemma distributed_integrable_var: 863 fixes X :: "'a \<Rightarrow> real" 864 shows "distributed M lborel X (\<lambda>x. ennreal (f x)) \<Longrightarrow> (\<And>x. 0 \<le> f x) \<Longrightarrow> 865 integrable lborel (\<lambda>x. f x * x) \<Longrightarrow> integrable M X" 866 using distributed_integrable[of M lborel X f "\<lambda>x. x"] by simp 867 868lemma (in prob_space) distributed_variance: 869 fixes f::"real \<Rightarrow> real" 870 assumes D: "distributed M lborel X f" and [simp]: "\<And>x. 0 \<le> f x" 871 shows "variance X = (\<integral>x. x\<^sup>2 * f (x + expectation X) \<partial>lborel)" 872proof (subst distributed_integral[OF D, symmetric]) 873 show "(\<integral> x. f x * (x - expectation X)\<^sup>2 \<partial>lborel) = (\<integral> x. x\<^sup>2 * f (x + expectation X) \<partial>lborel)" 874 by (subst lborel_integral_real_affine[where c=1 and t="expectation X"]) (auto simp: ac_simps) 875qed simp_all 876 877lemma (in prob_space) variance_affine: 878 fixes f::"real \<Rightarrow> real" 879 assumes [arith]: "b \<noteq> 0" 880 assumes D[intro]: "distributed M lborel X f" 881 assumes [simp]: "prob_space (density lborel f)" 882 assumes I[simp]: "integrable M X" 883 assumes I2[simp]: "integrable M (\<lambda>x. (X x)\<^sup>2)" 884 shows "variance (\<lambda>x. a + b * X x) = b\<^sup>2 * variance X" 885 by (subst variance_eq) 886 (auto simp: power2_sum power_mult_distrib prob_space variance_eq right_diff_distrib) 887 888definition 889 "simple_distributed M X f \<longleftrightarrow> 890 (\<forall>x. 0 \<le> f x) \<and> 891 distributed M (count_space (X`space M)) X (\<lambda>x. ennreal (f x)) \<and> 892 finite (X`space M)" 893 894lemma simple_distributed_nonneg[dest]: "simple_distributed M X f \<Longrightarrow> 0 \<le> f x" 895 by (auto simp: simple_distributed_def) 896 897lemma simple_distributed: 898 "simple_distributed M X Px \<Longrightarrow> distributed M (count_space (X`space M)) X Px" 899 unfolding simple_distributed_def by auto 900 901lemma simple_distributed_finite[dest]: "simple_distributed M X P \<Longrightarrow> finite (X`space M)" 902 by (simp add: simple_distributed_def) 903 904lemma (in prob_space) distributed_simple_function_superset: 905 assumes X: "simple_function M X" "\<And>x. x \<in> X ` space M \<Longrightarrow> P x = measure M (X -` {x} \<inter> space M)" 906 assumes A: "X`space M \<subseteq> A" "finite A" 907 defines "S \<equiv> count_space A" and "P' \<equiv> (\<lambda>x. if x \<in> X`space M then P x else 0)" 908 shows "distributed M S X P'" 909 unfolding distributed_def 910proof safe 911 show "(\<lambda>x. ennreal (P' x)) \<in> borel_measurable S" unfolding S_def by simp 912 show "distr M S X = density S P'" 913 proof (rule measure_eqI_finite) 914 show "sets (distr M S X) = Pow A" "sets (density S P') = Pow A" 915 using A unfolding S_def by auto 916 show "finite A" by fact 917 fix a assume a: "a \<in> A" 918 then have "a \<notin> X`space M \<Longrightarrow> X -` {a} \<inter> space M = {}" by auto 919 with A a X have "emeasure (distr M S X) {a} = P' a" 920 by (subst emeasure_distr) 921 (auto simp add: S_def P'_def simple_functionD emeasure_eq_measure measurable_count_space_eq2 922 intro!: arg_cong[where f=prob]) 923 also have "\<dots> = (\<integral>\<^sup>+x. ennreal (P' a) * indicator {a} x \<partial>S)" 924 using A X a 925 by (subst nn_integral_cmult_indicator) 926 (auto simp: S_def P'_def simple_distributed_def simple_functionD measure_nonneg) 927 also have "\<dots> = (\<integral>\<^sup>+x. ennreal (P' x) * indicator {a} x \<partial>S)" 928 by (auto simp: indicator_def intro!: nn_integral_cong) 929 also have "\<dots> = emeasure (density S P') {a}" 930 using a A by (intro emeasure_density[symmetric]) (auto simp: S_def) 931 finally show "emeasure (distr M S X) {a} = emeasure (density S P') {a}" . 932 qed 933 show "random_variable S X" 934 using X(1) A by (auto simp: measurable_def simple_functionD S_def) 935qed 936 937lemma (in prob_space) simple_distributedI: 938 assumes X: "simple_function M X" 939 "\<And>x. 0 \<le> P x" 940 "\<And>x. x \<in> X ` space M \<Longrightarrow> P x = measure M (X -` {x} \<inter> space M)" 941 shows "simple_distributed M X P" 942 unfolding simple_distributed_def 943proof (safe intro!: X) 944 have "distributed M (count_space (X ` space M)) X (\<lambda>x. ennreal (if x \<in> X`space M then P x else 0))" 945 (is "?A") 946 using simple_functionD[OF X(1)] by (intro distributed_simple_function_superset[OF X(1,3)]) auto 947 also have "?A \<longleftrightarrow> distributed M (count_space (X ` space M)) X (\<lambda>x. ennreal (P x))" 948 by (rule distributed_cong_density) auto 949 finally show "\<dots>" . 950qed (rule simple_functionD[OF X(1)]) 951 952lemma simple_distributed_joint_finite: 953 assumes X: "simple_distributed M (\<lambda>x. (X x, Y x)) Px" 954 shows "finite (X ` space M)" "finite (Y ` space M)" 955proof - 956 have "finite ((\<lambda>x. (X x, Y x)) ` space M)" 957 using X by (auto simp: simple_distributed_def simple_functionD) 958 then have "finite (fst ` (\<lambda>x. (X x, Y x)) ` space M)" "finite (snd ` (\<lambda>x. (X x, Y x)) ` space M)" 959 by auto 960 then show fin: "finite (X ` space M)" "finite (Y ` space M)" 961 by (auto simp: image_image) 962qed 963 964lemma simple_distributed_joint2_finite: 965 assumes X: "simple_distributed M (\<lambda>x. (X x, Y x, Z x)) Px" 966 shows "finite (X ` space M)" "finite (Y ` space M)" "finite (Z ` space M)" 967proof - 968 have "finite ((\<lambda>x. (X x, Y x, Z x)) ` space M)" 969 using X by (auto simp: simple_distributed_def simple_functionD) 970 then have "finite (fst ` (\<lambda>x. (X x, Y x, Z x)) ` space M)" 971 "finite ((fst \<circ> snd) ` (\<lambda>x. (X x, Y x, Z x)) ` space M)" 972 "finite ((snd \<circ> snd) ` (\<lambda>x. (X x, Y x, Z x)) ` space M)" 973 by auto 974 then show fin: "finite (X ` space M)" "finite (Y ` space M)" "finite (Z ` space M)" 975 by (auto simp: image_image) 976qed 977 978lemma simple_distributed_simple_function: 979 "simple_distributed M X Px \<Longrightarrow> simple_function M X" 980 unfolding simple_distributed_def distributed_def 981 by (auto simp: simple_function_def measurable_count_space_eq2) 982 983lemma simple_distributed_measure: 984 "simple_distributed M X P \<Longrightarrow> a \<in> X`space M \<Longrightarrow> P a = measure M (X -` {a} \<inter> space M)" 985 using distributed_count_space[of M "X`space M" X P a, symmetric] 986 by (auto simp: simple_distributed_def measure_def) 987 988lemma (in prob_space) simple_distributed_joint: 989 assumes X: "simple_distributed M (\<lambda>x. (X x, Y x)) Px" 990 defines "S \<equiv> count_space (X`space M) \<Otimes>\<^sub>M count_space (Y`space M)" 991 defines "P \<equiv> (\<lambda>x. if x \<in> (\<lambda>x. (X x, Y x))`space M then Px x else 0)" 992 shows "distributed M S (\<lambda>x. (X x, Y x)) P" 993proof - 994 from simple_distributed_joint_finite[OF X, simp] 995 have S_eq: "S = count_space (X`space M \<times> Y`space M)" 996 by (simp add: S_def pair_measure_count_space) 997 show ?thesis 998 unfolding S_eq P_def 999 proof (rule distributed_simple_function_superset) 1000 show "simple_function M (\<lambda>x. (X x, Y x))" 1001 using X by (rule simple_distributed_simple_function) 1002 fix x assume "x \<in> (\<lambda>x. (X x, Y x)) ` space M" 1003 from simple_distributed_measure[OF X this] 1004 show "Px x = prob ((\<lambda>x. (X x, Y x)) -` {x} \<inter> space M)" . 1005 qed auto 1006qed 1007 1008lemma (in prob_space) simple_distributed_joint2: 1009 assumes X: "simple_distributed M (\<lambda>x. (X x, Y x, Z x)) Px" 1010 defines "S \<equiv> count_space (X`space M) \<Otimes>\<^sub>M count_space (Y`space M) \<Otimes>\<^sub>M count_space (Z`space M)" 1011 defines "P \<equiv> (\<lambda>x. if x \<in> (\<lambda>x. (X x, Y x, Z x))`space M then Px x else 0)" 1012 shows "distributed M S (\<lambda>x. (X x, Y x, Z x)) P" 1013proof - 1014 from simple_distributed_joint2_finite[OF X, simp] 1015 have S_eq: "S = count_space (X`space M \<times> Y`space M \<times> Z`space M)" 1016 by (simp add: S_def pair_measure_count_space) 1017 show ?thesis 1018 unfolding S_eq P_def 1019 proof (rule distributed_simple_function_superset) 1020 show "simple_function M (\<lambda>x. (X x, Y x, Z x))" 1021 using X by (rule simple_distributed_simple_function) 1022 fix x assume "x \<in> (\<lambda>x. (X x, Y x, Z x)) ` space M" 1023 from simple_distributed_measure[OF X this] 1024 show "Px x = prob ((\<lambda>x. (X x, Y x, Z x)) -` {x} \<inter> space M)" . 1025 qed auto 1026qed 1027 1028lemma (in prob_space) simple_distributed_sum_space: 1029 assumes X: "simple_distributed M X f" 1030 shows "sum f (X`space M) = 1" 1031proof - 1032 from X have "sum f (X`space M) = prob (\<Union>i\<in>X`space M. X -` {i} \<inter> space M)" 1033 by (subst finite_measure_finite_Union) 1034 (auto simp add: disjoint_family_on_def simple_distributed_measure simple_distributed_simple_function simple_functionD 1035 intro!: sum.cong arg_cong[where f="prob"]) 1036 also have "\<dots> = prob (space M)" 1037 by (auto intro!: arg_cong[where f=prob]) 1038 finally show ?thesis 1039 using emeasure_space_1 by (simp add: emeasure_eq_measure) 1040qed 1041 1042lemma (in prob_space) distributed_marginal_eq_joint_simple: 1043 assumes Px: "simple_function M X" 1044 assumes Py: "simple_distributed M Y Py" 1045 assumes Pxy: "simple_distributed M (\<lambda>x. (X x, Y x)) Pxy" 1046 assumes y: "y \<in> Y`space M" 1047 shows "Py y = (\<Sum>x\<in>X`space M. if (x, y) \<in> (\<lambda>x. (X x, Y x)) ` space M then Pxy (x, y) else 0)" 1048proof - 1049 note Px = simple_distributedI[OF Px measure_nonneg refl] 1050 have "AE y in count_space (Y ` space M). ennreal (Py y) = 1051 \<integral>\<^sup>+ x. ennreal (if (x, y) \<in> (\<lambda>x. (X x, Y x)) ` space M then Pxy (x, y) else 0) \<partial>count_space (X ` space M)" 1052 using sigma_finite_measure_count_space_finite sigma_finite_measure_count_space_finite 1053 simple_distributed[OF Py] simple_distributed_joint[OF Pxy] 1054 by (rule distributed_marginal_eq_joint2) 1055 (auto intro: Py Px simple_distributed_finite) 1056 then have "ennreal (Py y) = 1057 (\<Sum>x\<in>X`space M. ennreal (if (x, y) \<in> (\<lambda>x. (X x, Y x)) ` space M then Pxy (x, y) else 0))" 1058 using y Px[THEN simple_distributed_finite] 1059 by (auto simp: AE_count_space nn_integral_count_space_finite) 1060 also have "\<dots> = (\<Sum>x\<in>X`space M. if (x, y) \<in> (\<lambda>x. (X x, Y x)) ` space M then Pxy (x, y) else 0)" 1061 using Pxy by (intro sum_ennreal) auto 1062 finally show ?thesis 1063 using simple_distributed_nonneg[OF Py] simple_distributed_nonneg[OF Pxy] 1064 by (subst (asm) ennreal_inj) (auto intro!: sum_nonneg) 1065qed 1066 1067lemma distributedI_real: 1068 fixes f :: "'a \<Rightarrow> real" 1069 assumes gen: "sets M1 = sigma_sets (space M1) E" and "Int_stable E" 1070 and A: "range A \<subseteq> E" "(\<Union>i::nat. A i) = space M1" "\<And>i. emeasure (distr M M1 X) (A i) \<noteq> \<infinity>" 1071 and X: "X \<in> measurable M M1" 1072 and f: "f \<in> borel_measurable M1" "AE x in M1. 0 \<le> f x" 1073 and eq: "\<And>A. A \<in> E \<Longrightarrow> emeasure M (X -` A \<inter> space M) = (\<integral>\<^sup>+ x. f x * indicator A x \<partial>M1)" 1074 shows "distributed M M1 X f" 1075 unfolding distributed_def 1076proof (intro conjI) 1077 show "distr M M1 X = density M1 f" 1078 proof (rule measure_eqI_generator_eq[where A=A]) 1079 { fix A assume A: "A \<in> E" 1080 then have "A \<in> sigma_sets (space M1) E" by auto 1081 then have "A \<in> sets M1" 1082 using gen by simp 1083 with f A eq[of A] X show "emeasure (distr M M1 X) A = emeasure (density M1 f) A" 1084 by (auto simp add: emeasure_distr emeasure_density ennreal_indicator 1085 intro!: nn_integral_cong split: split_indicator) } 1086 note eq_E = this 1087 show "Int_stable E" by fact 1088 { fix e assume "e \<in> E" 1089 then have "e \<in> sigma_sets (space M1) E" by auto 1090 then have "e \<in> sets M1" unfolding gen . 1091 then have "e \<subseteq> space M1" by (rule sets.sets_into_space) } 1092 then show "E \<subseteq> Pow (space M1)" by auto 1093 show "sets (distr M M1 X) = sigma_sets (space M1) E" 1094 "sets (density M1 (\<lambda>x. ennreal (f x))) = sigma_sets (space M1) E" 1095 unfolding gen[symmetric] by auto 1096 qed fact+ 1097qed (insert X f, auto) 1098 1099lemma distributedI_borel_atMost: 1100 fixes f :: "real \<Rightarrow> real" 1101 assumes [measurable]: "X \<in> borel_measurable M" 1102 and [measurable]: "f \<in> borel_measurable borel" and f[simp]: "AE x in lborel. 0 \<le> f x" 1103 and g_eq: "\<And>a. (\<integral>\<^sup>+x. f x * indicator {..a} x \<partial>lborel) = ennreal (g a)" 1104 and M_eq: "\<And>a. emeasure M {x\<in>space M. X x \<le> a} = ennreal (g a)" 1105 shows "distributed M lborel X f" 1106proof (rule distributedI_real) 1107 show "sets (lborel::real measure) = sigma_sets (space lborel) (range atMost)" 1108 by (simp add: borel_eq_atMost) 1109 show "Int_stable (range atMost :: real set set)" 1110 by (auto simp: Int_stable_def) 1111 have vimage_eq: "\<And>a. (X -` {..a} \<inter> space M) = {x\<in>space M. X x \<le> a}" by auto 1112 define A where "A i = {.. real i}" for i :: nat 1113 then show "range A \<subseteq> range atMost" "(\<Union>i. A i) = space lborel" 1114 "\<And>i. emeasure (distr M lborel X) (A i) \<noteq> \<infinity>" 1115 by (auto simp: real_arch_simple emeasure_distr vimage_eq M_eq) 1116 1117 fix A :: "real set" assume "A \<in> range atMost" 1118 then obtain a where A: "A = {..a}" by auto 1119 show "emeasure M (X -` A \<inter> space M) = (\<integral>\<^sup>+x. f x * indicator A x \<partial>lborel)" 1120 unfolding vimage_eq A M_eq g_eq .. 1121qed auto 1122 1123lemma (in prob_space) uniform_distributed_params: 1124 assumes X: "distributed M MX X (\<lambda>x. indicator A x / measure MX A)" 1125 shows "A \<in> sets MX" "measure MX A \<noteq> 0" 1126proof - 1127 interpret X: prob_space "distr M MX X" 1128 using distributed_measurable[OF X] by (rule prob_space_distr) 1129 1130 show "measure MX A \<noteq> 0" 1131 proof 1132 assume "measure MX A = 0" 1133 with X.emeasure_space_1 X.prob_space distributed_distr_eq_density[OF X] 1134 show False 1135 by (simp add: emeasure_density zero_ennreal_def[symmetric]) 1136 qed 1137 with measure_notin_sets[of A MX] show "A \<in> sets MX" 1138 by blast 1139qed 1140 1141lemma prob_space_uniform_measure: 1142 assumes A: "emeasure M A \<noteq> 0" "emeasure M A \<noteq> \<infinity>" 1143 shows "prob_space (uniform_measure M A)" 1144proof 1145 show "emeasure (uniform_measure M A) (space (uniform_measure M A)) = 1" 1146 using emeasure_uniform_measure[OF emeasure_neq_0_sets[OF A(1)], of "space M"] 1147 using sets.sets_into_space[OF emeasure_neq_0_sets[OF A(1)]] A 1148 by (simp add: Int_absorb2 less_top) 1149qed 1150 1151lemma prob_space_uniform_count_measure: "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> prob_space (uniform_count_measure A)" 1152 by standard (auto simp: emeasure_uniform_count_measure space_uniform_count_measure one_ennreal_def) 1153 1154lemma (in prob_space) measure_uniform_measure_eq_cond_prob: 1155 assumes [measurable]: "Measurable.pred M P" "Measurable.pred M Q" 1156 shows "\<P>(x in uniform_measure M {x\<in>space M. Q x}. P x) = \<P>(x in M. P x \<bar> Q x)" 1157proof cases 1158 assume Q: "measure M {x\<in>space M. Q x} = 0" 1159 then have *: "AE x in M. \<not> Q x" 1160 by (simp add: prob_eq_0) 1161 then have "density M (\<lambda>x. indicator {x \<in> space M. Q x} x / emeasure M {x \<in> space M. Q x}) = density M (\<lambda>x. 0)" 1162 by (intro density_cong) auto 1163 with * show ?thesis 1164 unfolding uniform_measure_def 1165 by (simp add: emeasure_density measure_def cond_prob_def emeasure_eq_0_AE) 1166next 1167 assume Q: "measure M {x\<in>space M. Q x} \<noteq> 0" 1168 then show "\<P>(x in uniform_measure M {x \<in> space M. Q x}. P x) = cond_prob M P Q" 1169 by (subst measure_uniform_measure) 1170 (auto simp: emeasure_eq_measure cond_prob_def measure_nonneg intro!: arg_cong[where f=prob]) 1171qed 1172 1173lemma prob_space_point_measure: 1174 "finite S \<Longrightarrow> (\<And>s. s \<in> S \<Longrightarrow> 0 \<le> p s) \<Longrightarrow> (\<Sum>s\<in>S. p s) = 1 \<Longrightarrow> prob_space (point_measure S p)" 1175 by (rule prob_spaceI) (simp add: space_point_measure emeasure_point_measure_finite) 1176 1177lemma (in prob_space) distr_pair_fst: "distr (N \<Otimes>\<^sub>M M) N fst = N" 1178proof (intro measure_eqI) 1179 fix A assume A: "A \<in> sets (distr (N \<Otimes>\<^sub>M M) N fst)" 1180 from A have "emeasure (distr (N \<Otimes>\<^sub>M M) N fst) A = emeasure (N \<Otimes>\<^sub>M M) (A \<times> space M)" 1181 by (auto simp add: emeasure_distr space_pair_measure dest: sets.sets_into_space intro!: arg_cong2[where f=emeasure]) 1182 with A show "emeasure (distr (N \<Otimes>\<^sub>M M) N fst) A = emeasure N A" 1183 by (simp add: emeasure_pair_measure_Times emeasure_space_1) 1184qed simp 1185 1186lemma (in product_prob_space) distr_reorder: 1187 assumes "inj_on t J" "t \<in> J \<rightarrow> K" "finite K" 1188 shows "distr (PiM K M) (Pi\<^sub>M J (\<lambda>x. M (t x))) (\<lambda>\<omega>. \<lambda>n\<in>J. \<omega> (t n)) = PiM J (\<lambda>x. M (t x))" 1189proof (rule product_sigma_finite.PiM_eqI) 1190 show "product_sigma_finite (\<lambda>x. M (t x))" .. 1191 have "t`J \<subseteq> K" using assms by auto 1192 then show [simp]: "finite J" 1193 by (rule finite_imageD[OF finite_subset]) fact+ 1194 fix A assume A: "\<And>i. i \<in> J \<Longrightarrow> A i \<in> sets (M (t i))" 1195 moreover have "((\<lambda>\<omega>. \<lambda>n\<in>J. \<omega> (t n)) -` Pi\<^sub>E J A \<inter> space (Pi\<^sub>M K M)) = 1196 (\<Pi>\<^sub>E i\<in>K. if i \<in> t`J then A (the_inv_into J t i) else space (M i))" 1197 using A A[THEN sets.sets_into_space] \<open>t \<in> J \<rightarrow> K\<close> \<open>inj_on t J\<close> 1198 by (subst prod_emb_Pi[symmetric]) (auto simp: space_PiM PiE_iff the_inv_into_f_f prod_emb_def) 1199 ultimately show "distr (Pi\<^sub>M K M) (Pi\<^sub>M J (\<lambda>x. M (t x))) (\<lambda>\<omega>. \<lambda>n\<in>J. \<omega> (t n)) (Pi\<^sub>E J A) = (\<Prod>i\<in>J. M (t i) (A i))" 1200 using assms 1201 apply (subst emeasure_distr) 1202 apply (auto intro!: sets_PiM_I_finite simp: Pi_iff) 1203 apply (subst emeasure_PiM) 1204 apply (auto simp: the_inv_into_f_f \<open>inj_on t J\<close> prod.reindex[OF \<open>inj_on t J\<close>] 1205 if_distrib[where f="emeasure (M _)"] prod.If_cases emeasure_space_1 Int_absorb1 \<open>t`J \<subseteq> K\<close>) 1206 done 1207qed simp 1208 1209lemma (in product_prob_space) distr_restrict: 1210 "J \<subseteq> K \<Longrightarrow> finite K \<Longrightarrow> (\<Pi>\<^sub>M i\<in>J. M i) = distr (\<Pi>\<^sub>M i\<in>K. M i) (\<Pi>\<^sub>M i\<in>J. M i) (\<lambda>f. restrict f J)" 1211 using distr_reorder[of "\<lambda>x. x" J K] by (simp add: Pi_iff subset_eq) 1212 1213lemma (in product_prob_space) emeasure_prod_emb[simp]: 1214 assumes L: "J \<subseteq> L" "finite L" and X: "X \<in> sets (Pi\<^sub>M J M)" 1215 shows "emeasure (Pi\<^sub>M L M) (prod_emb L M J X) = emeasure (Pi\<^sub>M J M) X" 1216 by (subst distr_restrict[OF L]) 1217 (simp add: prod_emb_def space_PiM emeasure_distr measurable_restrict_subset L X) 1218 1219lemma emeasure_distr_restrict: 1220 assumes "I \<subseteq> K" and Q[measurable_cong]: "sets Q = sets (PiM K M)" and A[measurable]: "A \<in> sets (PiM I M)" 1221 shows "emeasure (distr Q (PiM I M) (\<lambda>\<omega>. restrict \<omega> I)) A = emeasure Q (prod_emb K M I A)" 1222 using \<open>I\<subseteq>K\<close> sets_eq_imp_space_eq[OF Q] 1223 by (subst emeasure_distr) 1224 (auto simp: measurable_cong_sets[OF Q] prod_emb_def space_PiM[symmetric] intro!: measurable_restrict) 1225 1226lemma (in prob_space) prob_space_completion: "prob_space (completion M)" 1227 by (rule prob_spaceI) (simp add: emeasure_space_1) 1228 1229end 1230