src/HOL/Probability/Probability_Measure.thy
author haftmann
Sun Jun 23 21:16:07 2013 +0200 (2013-06-23)
changeset 52435 6646bb548c6b
parent 51683 baefa3b461c2
child 53015 a1119cf551e8
permissions -rw-r--r--
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
     1 (*  Title:      HOL/Probability/Probability_Measure.thy
     2     Author:     Johannes Hölzl, TU München
     3     Author:     Armin Heller, TU München
     4 *)
     5 
     6 header {*Probability measure*}
     7 
     8 theory Probability_Measure
     9   imports Lebesgue_Measure Radon_Nikodym
    10 begin
    11 
    12 locale prob_space = finite_measure +
    13   assumes emeasure_space_1: "emeasure M (space M) = 1"
    14 
    15 lemma prob_spaceI[Pure.intro!]:
    16   assumes *: "emeasure M (space M) = 1"
    17   shows "prob_space M"
    18 proof -
    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 default fact
    24 qed
    25 
    26 abbreviation (in prob_space) "events \<equiv> sets M"
    27 abbreviation (in prob_space) "prob \<equiv> measure M"
    28 abbreviation (in prob_space) "random_variable M' X \<equiv> X \<in> measurable M M'"
    29 abbreviation (in prob_space) "expectation \<equiv> integral\<^isup>L M"
    30 
    31 lemma (in prob_space) prob_space_distr:
    32   assumes f: "f \<in> measurable M M'" shows "prob_space (distr M M' f)"
    33 proof (rule prob_spaceI)
    34   have "f -` space M' \<inter> space M = space M" using f by (auto dest: measurable_space)
    35   with f show "emeasure (distr M M' f) (space (distr M M' f)) = 1"
    36     by (auto simp: emeasure_distr emeasure_space_1)
    37 qed
    38 
    39 lemma (in prob_space) prob_space: "prob (space M) = 1"
    40   using emeasure_space_1 unfolding measure_def by (simp add: one_ereal_def)
    41 
    42 lemma (in prob_space) prob_le_1[simp, intro]: "prob A \<le> 1"
    43   using bounded_measure[of A] by (simp add: prob_space)
    44 
    45 lemma (in prob_space) not_empty: "space M \<noteq> {}"
    46   using prob_space by auto
    47 
    48 lemma (in prob_space) measure_le_1: "emeasure M X \<le> 1"
    49   using emeasure_space[of M X] by (simp add: emeasure_space_1)
    50 
    51 lemma (in prob_space) AE_I_eq_1:
    52   assumes "emeasure M {x\<in>space M. P x} = 1" "{x\<in>space M. P x} \<in> sets M"
    53   shows "AE x in M. P x"
    54 proof (rule AE_I)
    55   show "emeasure M (space M - {x \<in> space M. P x}) = 0"
    56     using assms emeasure_space_1 by (simp add: emeasure_compl)
    57 qed (insert assms, auto)
    58 
    59 lemma (in prob_space) prob_compl:
    60   assumes A: "A \<in> events"
    61   shows "prob (space M - A) = 1 - prob A"
    62   using finite_measure_compl[OF A] by (simp add: prob_space)
    63 
    64 lemma (in prob_space) AE_in_set_eq_1:
    65   assumes "A \<in> events" shows "(AE x in M. x \<in> A) \<longleftrightarrow> prob A = 1"
    66 proof
    67   assume ae: "AE x in M. x \<in> A"
    68   have "{x \<in> space M. x \<in> A} = A" "{x \<in> space M. x \<notin> A} = space M - A"
    69     using `A \<in> events`[THEN sets.sets_into_space] by auto
    70   with AE_E2[OF ae] `A \<in> events` have "1 - emeasure M A = 0"
    71     by (simp add: emeasure_compl emeasure_space_1)
    72   then show "prob A = 1"
    73     using `A \<in> events` by (simp add: emeasure_eq_measure one_ereal_def)
    74 next
    75   assume prob: "prob A = 1"
    76   show "AE x in M. x \<in> A"
    77   proof (rule AE_I)
    78     show "{x \<in> space M. x \<notin> A} \<subseteq> space M - A" by auto
    79     show "emeasure M (space M - A) = 0"
    80       using `A \<in> events` prob
    81       by (simp add: prob_compl emeasure_space_1 emeasure_eq_measure one_ereal_def)
    82     show "space M - A \<in> events"
    83       using `A \<in> events` by auto
    84   qed
    85 qed
    86 
    87 lemma (in prob_space) AE_False: "(AE x in M. False) \<longleftrightarrow> False"
    88 proof
    89   assume "AE x in M. False"
    90   then have "AE x in M. x \<in> {}" by simp
    91   then show False
    92     by (subst (asm) AE_in_set_eq_1) auto
    93 qed simp
    94 
    95 lemma (in prob_space) AE_prob_1:
    96   assumes "prob A = 1" shows "AE x in M. x \<in> A"
    97 proof -
    98   from `prob A = 1` have "A \<in> events"
    99     by (metis measure_notin_sets zero_neq_one)
   100   with AE_in_set_eq_1 assms show ?thesis by simp
   101 qed
   102 
   103 lemma (in prob_space) AE_const[simp]: "(AE x in M. P) \<longleftrightarrow> P"
   104   by (cases P) (auto simp: AE_False)
   105 
   106 lemma (in prob_space) AE_contr:
   107   assumes ae: "AE \<omega> in M. P \<omega>" "AE \<omega> in M. \<not> P \<omega>"
   108   shows False
   109 proof -
   110   from ae have "AE \<omega> in M. False" by eventually_elim auto
   111   then show False by auto
   112 qed
   113 
   114 lemma (in prob_space) expectation_less:
   115   assumes [simp]: "integrable M X"
   116   assumes gt: "AE x in M. X x < b"
   117   shows "expectation X < b"
   118 proof -
   119   have "expectation X < expectation (\<lambda>x. b)"
   120     using gt emeasure_space_1
   121     by (intro integral_less_AE_space) auto
   122   then show ?thesis using prob_space by simp
   123 qed
   124 
   125 lemma (in prob_space) expectation_greater:
   126   assumes [simp]: "integrable M X"
   127   assumes gt: "AE x in M. a < X x"
   128   shows "a < expectation X"
   129 proof -
   130   have "expectation (\<lambda>x. a) < expectation X"
   131     using gt emeasure_space_1
   132     by (intro integral_less_AE_space) auto
   133   then show ?thesis using prob_space by simp
   134 qed
   135 
   136 lemma (in prob_space) jensens_inequality:
   137   fixes a b :: real
   138   assumes X: "integrable M X" "AE x in M. X x \<in> I"
   139   assumes I: "I = {a <..< b} \<or> I = {a <..} \<or> I = {..< b} \<or> I = UNIV"
   140   assumes q: "integrable M (\<lambda>x. q (X x))" "convex_on I q"
   141   shows "q (expectation X) \<le> expectation (\<lambda>x. q (X x))"
   142 proof -
   143   let ?F = "\<lambda>x. Inf ((\<lambda>t. (q x - q t) / (x - t)) ` ({x<..} \<inter> I))"
   144   from X(2) AE_False have "I \<noteq> {}" by auto
   145 
   146   from I have "open I" by auto
   147 
   148   note I
   149   moreover
   150   { assume "I \<subseteq> {a <..}"
   151     with X have "a < expectation X"
   152       by (intro expectation_greater) auto }
   153   moreover
   154   { assume "I \<subseteq> {..< b}"
   155     with X have "expectation X < b"
   156       by (intro expectation_less) auto }
   157   ultimately have "expectation X \<in> I"
   158     by (elim disjE)  (auto simp: subset_eq)
   159   moreover
   160   { fix y assume y: "y \<in> I"
   161     with q(2) `open I` have "Sup ((\<lambda>x. q x + ?F x * (y - x)) ` I) = q y"
   162       by (auto intro!: cSup_eq_maximum convex_le_Inf_differential image_eqI[OF _ y] simp: interior_open) }
   163   ultimately have "q (expectation X) = Sup ((\<lambda>x. q x + ?F x * (expectation X - x)) ` I)"
   164     by simp
   165   also have "\<dots> \<le> expectation (\<lambda>w. q (X w))"
   166   proof (rule cSup_least)
   167     show "(\<lambda>x. q x + ?F x * (expectation X - x)) ` I \<noteq> {}"
   168       using `I \<noteq> {}` by auto
   169   next
   170     fix k assume "k \<in> (\<lambda>x. q x + ?F x * (expectation X - x)) ` I"
   171     then guess x .. note x = this
   172     have "q x + ?F x * (expectation X  - x) = expectation (\<lambda>w. q x + ?F x * (X w - x))"
   173       using prob_space by (simp add: X)
   174     also have "\<dots> \<le> expectation (\<lambda>w. q (X w))"
   175       using `x \<in> I` `open I` X(2)
   176       apply (intro integral_mono_AE integral_add integral_cmult integral_diff
   177                 lebesgue_integral_const X q)
   178       apply (elim eventually_elim1)
   179       apply (intro convex_le_Inf_differential)
   180       apply (auto simp: interior_open q)
   181       done
   182     finally show "k \<le> expectation (\<lambda>w. q (X w))" using x by auto
   183   qed
   184   finally show "q (expectation X) \<le> expectation (\<lambda>x. q (X x))" .
   185 qed
   186 
   187 subsection  {* Introduce binder for probability *}
   188 
   189 syntax
   190   "_prob" :: "pttrn \<Rightarrow> logic \<Rightarrow> logic \<Rightarrow> logic" ("('\<P>'(_ in _. _'))")
   191 
   192 translations
   193   "\<P>(x in M. P)" => "CONST measure M {x \<in> CONST space M. P}"
   194 
   195 definition
   196   "cond_prob M P Q = \<P>(\<omega> in M. P \<omega> \<and> Q \<omega>) / \<P>(\<omega> in M. Q \<omega>)"
   197 
   198 syntax
   199   "_conditional_prob" :: "pttrn \<Rightarrow> logic \<Rightarrow> logic \<Rightarrow> logic \<Rightarrow> logic" ("('\<P>'(_ in _. _ \<bar>/ _'))")
   200 
   201 translations
   202   "\<P>(x in M. P \<bar> Q)" => "CONST cond_prob M (\<lambda>x. P) (\<lambda>x. Q)"
   203 
   204 lemma (in prob_space) AE_E_prob:
   205   assumes ae: "AE x in M. P x"
   206   obtains S where "S \<subseteq> {x \<in> space M. P x}" "S \<in> events" "prob S = 1"
   207 proof -
   208   from ae[THEN AE_E] guess N .
   209   then show thesis
   210     by (intro that[of "space M - N"])
   211        (auto simp: prob_compl prob_space emeasure_eq_measure)
   212 qed
   213 
   214 lemma (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)"
   215   by (auto intro!: arg_cong[where f=prob] simp add: prob_compl[symmetric])
   216 
   217 lemma (in prob_space) prob_eq_AE:
   218   "(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)"
   219   by (rule finite_measure_eq_AE) auto
   220 
   221 lemma (in prob_space) prob_eq_0_AE:
   222   assumes not: "AE x in M. \<not> P x" shows "\<P>(x in M. P x) = 0"
   223 proof cases
   224   assume "{x\<in>space M. P x} \<in> events"
   225   with not have "\<P>(x in M. P x) = \<P>(x in M. False)"
   226     by (intro prob_eq_AE) auto
   227   then show ?thesis by simp
   228 qed (simp add: measure_notin_sets)
   229 
   230 lemma (in prob_space) prob_Collect_eq_0:
   231   "{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)"
   232   using AE_iff_measurable[OF _ refl, of M "\<lambda>x. \<not> P x"] by (simp add: emeasure_eq_measure)
   233 
   234 lemma (in prob_space) prob_Collect_eq_1:
   235   "{x \<in> space M. P x} \<in> sets M \<Longrightarrow> \<P>(x in M. P x) = 1 \<longleftrightarrow> (AE x in M. P x)"
   236   using AE_in_set_eq_1[of "{x\<in>space M. P x}"] by simp
   237 
   238 lemma (in prob_space) prob_eq_0:
   239   "A \<in> sets M \<Longrightarrow> prob A = 0 \<longleftrightarrow> (AE x in M. x \<notin> A)"
   240   using AE_iff_measurable[OF _ refl, of M "\<lambda>x. x \<notin> A"]
   241   by (auto simp add: emeasure_eq_measure Int_def[symmetric])
   242 
   243 lemma (in prob_space) prob_eq_1:
   244   "A \<in> sets M \<Longrightarrow> prob A = 1 \<longleftrightarrow> (AE x in M. x \<in> A)"
   245   using AE_in_set_eq_1[of A] by simp
   246 
   247 lemma (in prob_space) prob_sums:
   248   assumes P: "\<And>n. {x\<in>space M. P n x} \<in> events"
   249   assumes Q: "{x\<in>space M. Q x} \<in> events"
   250   assumes ae: "AE x in M. (\<forall>n. P n x \<longrightarrow> Q x) \<and> (Q x \<longrightarrow> (\<exists>!n. P n x))"
   251   shows "(\<lambda>n. \<P>(x in M. P n x)) sums \<P>(x in M. Q x)"
   252 proof -
   253   from ae[THEN AE_E_prob] guess S . note S = this
   254   then have disj: "disjoint_family (\<lambda>n. {x\<in>space M. P n x} \<inter> S)"
   255     by (auto simp: disjoint_family_on_def)
   256   from S have ae_S:
   257     "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)"
   258     "\<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"
   259     using ae by (auto dest!: AE_prob_1)
   260   from ae_S have *:
   261     "\<P>(x in M. Q x) = prob (\<Union>n. {x\<in>space M. P n x} \<inter> S)"
   262     using P Q S by (intro finite_measure_eq_AE) auto
   263   from ae_S have **:
   264     "\<And>n. \<P>(x in M. P n x) = prob ({x\<in>space M. P n x} \<inter> S)"
   265     using P Q S by (intro finite_measure_eq_AE) auto
   266   show ?thesis
   267     unfolding * ** using S P disj
   268     by (intro finite_measure_UNION) auto
   269 qed
   270 
   271 lemma (in prob_space) cond_prob_eq_AE:
   272   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"
   273   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"
   274   shows "cond_prob M P Q = cond_prob M P' Q'"
   275   using P Q
   276   by (auto simp: cond_prob_def intro!: arg_cong2[where f="op /"] prob_eq_AE sets.sets_Collect_conj)
   277 
   278 
   279 lemma (in prob_space) joint_distribution_Times_le_fst:
   280   "random_variable MX X \<Longrightarrow> random_variable MY Y \<Longrightarrow> A \<in> sets MX \<Longrightarrow> B \<in> sets MY
   281     \<Longrightarrow> emeasure (distr M (MX \<Otimes>\<^isub>M MY) (\<lambda>x. (X x, Y x))) (A \<times> B) \<le> emeasure (distr M MX X) A"
   282   by (auto simp: emeasure_distr measurable_pair_iff comp_def intro!: emeasure_mono measurable_sets)
   283 
   284 lemma (in prob_space) joint_distribution_Times_le_snd:
   285   "random_variable MX X \<Longrightarrow> random_variable MY Y \<Longrightarrow> A \<in> sets MX \<Longrightarrow> B \<in> sets MY
   286     \<Longrightarrow> emeasure (distr M (MX \<Otimes>\<^isub>M MY) (\<lambda>x. (X x, Y x))) (A \<times> B) \<le> emeasure (distr M MY Y) B"
   287   by (auto simp: emeasure_distr measurable_pair_iff comp_def intro!: emeasure_mono measurable_sets)
   288 
   289 locale pair_prob_space = pair_sigma_finite M1 M2 + M1: prob_space M1 + M2: prob_space M2 for M1 M2
   290 
   291 sublocale pair_prob_space \<subseteq> P: prob_space "M1 \<Otimes>\<^isub>M M2"
   292 proof
   293   show "emeasure (M1 \<Otimes>\<^isub>M M2) (space (M1 \<Otimes>\<^isub>M M2)) = 1"
   294     by (simp add: M2.emeasure_pair_measure_Times M1.emeasure_space_1 M2.emeasure_space_1 space_pair_measure)
   295 qed
   296 
   297 locale product_prob_space = product_sigma_finite M for M :: "'i \<Rightarrow> 'a measure" +
   298   fixes I :: "'i set"
   299   assumes prob_space: "\<And>i. prob_space (M i)"
   300 
   301 sublocale product_prob_space \<subseteq> M: prob_space "M i" for i
   302   by (rule prob_space)
   303 
   304 locale finite_product_prob_space = finite_product_sigma_finite M I + product_prob_space M I for M I
   305 
   306 sublocale finite_product_prob_space \<subseteq> prob_space "\<Pi>\<^isub>M i\<in>I. M i"
   307 proof
   308   show "emeasure (\<Pi>\<^isub>M i\<in>I. M i) (space (\<Pi>\<^isub>M i\<in>I. M i)) = 1"
   309     by (simp add: measure_times M.emeasure_space_1 setprod_1 space_PiM)
   310 qed
   311 
   312 lemma (in finite_product_prob_space) prob_times:
   313   assumes X: "\<And>i. i \<in> I \<Longrightarrow> X i \<in> sets (M i)"
   314   shows "prob (\<Pi>\<^isub>E i\<in>I. X i) = (\<Prod>i\<in>I. M.prob i (X i))"
   315 proof -
   316   have "ereal (measure (\<Pi>\<^isub>M i\<in>I. M i) (\<Pi>\<^isub>E i\<in>I. X i)) = emeasure (\<Pi>\<^isub>M i\<in>I. M i) (\<Pi>\<^isub>E i\<in>I. X i)"
   317     using X by (simp add: emeasure_eq_measure)
   318   also have "\<dots> = (\<Prod>i\<in>I. emeasure (M i) (X i))"
   319     using measure_times X by simp
   320   also have "\<dots> = ereal (\<Prod>i\<in>I. measure (M i) (X i))"
   321     using X by (simp add: M.emeasure_eq_measure setprod_ereal)
   322   finally show ?thesis by simp
   323 qed
   324 
   325 section {* Distributions *}
   326 
   327 definition "distributed M N X f \<longleftrightarrow> distr M N X = density N f \<and> 
   328   f \<in> borel_measurable N \<and> (AE x in N. 0 \<le> f x) \<and> X \<in> measurable M N"
   329 
   330 lemma
   331   assumes "distributed M N X f"
   332   shows distributed_distr_eq_density: "distr M N X = density N f"
   333     and distributed_measurable: "X \<in> measurable M N"
   334     and distributed_borel_measurable: "f \<in> borel_measurable N"
   335     and distributed_AE: "(AE x in N. 0 \<le> f x)"
   336   using assms by (simp_all add: distributed_def)
   337 
   338 lemma
   339   assumes D: "distributed M N X f"
   340   shows distributed_measurable'[measurable_dest]:
   341       "g \<in> measurable L M \<Longrightarrow> (\<lambda>x. X (g x)) \<in> measurable L N"
   342     and distributed_borel_measurable'[measurable_dest]:
   343       "h \<in> measurable L N \<Longrightarrow> (\<lambda>x. f (h x)) \<in> borel_measurable L"
   344   using distributed_measurable[OF D] distributed_borel_measurable[OF D]
   345   by simp_all
   346 
   347 lemma
   348   shows distributed_real_measurable: "distributed M N X (\<lambda>x. ereal (f x)) \<Longrightarrow> f \<in> borel_measurable N"
   349     and distributed_real_AE: "distributed M N X (\<lambda>x. ereal (f x)) \<Longrightarrow> (AE x in N. 0 \<le> f x)"
   350   by (simp_all add: distributed_def borel_measurable_ereal_iff)
   351 
   352 lemma
   353   assumes D: "distributed M N X (\<lambda>x. ereal (f x))"
   354   shows distributed_real_measurable'[measurable_dest]:
   355       "h \<in> measurable L N \<Longrightarrow> (\<lambda>x. f (h x)) \<in> borel_measurable L"
   356   using distributed_real_measurable[OF D]
   357   by simp_all
   358 
   359 lemma
   360   assumes D: "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) f"
   361   shows joint_distributed_measurable1[measurable_dest]:
   362       "h1 \<in> measurable N M \<Longrightarrow> (\<lambda>x. X (h1 x)) \<in> measurable N S"
   363     and joint_distributed_measurable2[measurable_dest]:
   364       "h2 \<in> measurable N M \<Longrightarrow> (\<lambda>x. Y (h2 x)) \<in> measurable N T"
   365   using measurable_compose[OF distributed_measurable[OF D] measurable_fst]
   366   using measurable_compose[OF distributed_measurable[OF D] measurable_snd]
   367   by auto
   368 
   369 lemma distributed_count_space:
   370   assumes X: "distributed M (count_space A) X P" and a: "a \<in> A" and A: "finite A"
   371   shows "P a = emeasure M (X -` {a} \<inter> space M)"
   372 proof -
   373   have "emeasure M (X -` {a} \<inter> space M) = emeasure (distr M (count_space A) X) {a}"
   374     using X a A by (simp add: emeasure_distr)
   375   also have "\<dots> = emeasure (density (count_space A) P) {a}"
   376     using X by (simp add: distributed_distr_eq_density)
   377   also have "\<dots> = (\<integral>\<^isup>+x. P a * indicator {a} x \<partial>count_space A)"
   378     using X a by (auto simp add: emeasure_density distributed_def indicator_def intro!: positive_integral_cong)
   379   also have "\<dots> = P a"
   380     using X a by (subst positive_integral_cmult_indicator) (auto simp: distributed_def one_ereal_def[symmetric] AE_count_space)
   381   finally show ?thesis ..
   382 qed
   383 
   384 lemma distributed_cong_density:
   385   "(AE x in N. f x = g x) \<Longrightarrow> g \<in> borel_measurable N \<Longrightarrow> f \<in> borel_measurable N \<Longrightarrow>
   386     distributed M N X f \<longleftrightarrow> distributed M N X g"
   387   by (auto simp: distributed_def intro!: density_cong)
   388 
   389 lemma subdensity:
   390   assumes T: "T \<in> measurable P Q"
   391   assumes f: "distributed M P X f"
   392   assumes g: "distributed M Q Y g"
   393   assumes Y: "Y = T \<circ> X"
   394   shows "AE x in P. g (T x) = 0 \<longrightarrow> f x = 0"
   395 proof -
   396   have "{x\<in>space Q. g x = 0} \<in> null_sets (distr M Q (T \<circ> X))"
   397     using g Y by (auto simp: null_sets_density_iff distributed_def)
   398   also have "distr M Q (T \<circ> X) = distr (distr M P X) Q T"
   399     using T f[THEN distributed_measurable] by (rule distr_distr[symmetric])
   400   finally have "T -` {x\<in>space Q. g x = 0} \<inter> space P \<in> null_sets (distr M P X)"
   401     using T by (subst (asm) null_sets_distr_iff) auto
   402   also have "T -` {x\<in>space Q. g x = 0} \<inter> space P = {x\<in>space P. g (T x) = 0}"
   403     using T by (auto dest: measurable_space)
   404   finally show ?thesis
   405     using f g by (auto simp add: null_sets_density_iff distributed_def)
   406 qed
   407 
   408 lemma subdensity_real:
   409   fixes g :: "'a \<Rightarrow> real" and f :: "'b \<Rightarrow> real"
   410   assumes T: "T \<in> measurable P Q"
   411   assumes f: "distributed M P X f"
   412   assumes g: "distributed M Q Y g"
   413   assumes Y: "Y = T \<circ> X"
   414   shows "AE x in P. g (T x) = 0 \<longrightarrow> f x = 0"
   415   using subdensity[OF T, of M X "\<lambda>x. ereal (f x)" Y "\<lambda>x. ereal (g x)"] assms by auto
   416 
   417 lemma distributed_emeasure:
   418   "distributed M N X f \<Longrightarrow> A \<in> sets N \<Longrightarrow> emeasure M (X -` A \<inter> space M) = (\<integral>\<^isup>+x. f x * indicator A x \<partial>N)"
   419   by (auto simp: distributed_AE
   420                  distributed_distr_eq_density[symmetric] emeasure_density[symmetric] emeasure_distr)
   421 
   422 lemma distributed_positive_integral:
   423   "distributed M N X f \<Longrightarrow> g \<in> borel_measurable N \<Longrightarrow> (\<integral>\<^isup>+x. f x * g x \<partial>N) = (\<integral>\<^isup>+x. g (X x) \<partial>M)"
   424   by (auto simp: distributed_AE
   425                  distributed_distr_eq_density[symmetric] positive_integral_density[symmetric] positive_integral_distr)
   426 
   427 lemma distributed_integral:
   428   "distributed M N X f \<Longrightarrow> g \<in> borel_measurable N \<Longrightarrow> (\<integral>x. f x * g x \<partial>N) = (\<integral>x. g (X x) \<partial>M)"
   429   by (auto simp: distributed_real_AE
   430                  distributed_distr_eq_density[symmetric] integral_density[symmetric] integral_distr)
   431   
   432 lemma distributed_transform_integral:
   433   assumes Px: "distributed M N X Px"
   434   assumes "distributed M P Y Py"
   435   assumes Y: "Y = T \<circ> X" and T: "T \<in> measurable N P" and f: "f \<in> borel_measurable P"
   436   shows "(\<integral>x. Py x * f x \<partial>P) = (\<integral>x. Px x * f (T x) \<partial>N)"
   437 proof -
   438   have "(\<integral>x. Py x * f x \<partial>P) = (\<integral>x. f (Y x) \<partial>M)"
   439     by (rule distributed_integral) fact+
   440   also have "\<dots> = (\<integral>x. f (T (X x)) \<partial>M)"
   441     using Y by simp
   442   also have "\<dots> = (\<integral>x. Px x * f (T x) \<partial>N)"
   443     using measurable_comp[OF T f] Px by (intro distributed_integral[symmetric]) (auto simp: comp_def)
   444   finally show ?thesis .
   445 qed
   446 
   447 lemma (in prob_space) distributed_unique:
   448   assumes Px: "distributed M S X Px"
   449   assumes Py: "distributed M S X Py"
   450   shows "AE x in S. Px x = Py x"
   451 proof -
   452   interpret X: prob_space "distr M S X"
   453     using Px by (intro prob_space_distr) simp
   454   have "sigma_finite_measure (distr M S X)" ..
   455   with sigma_finite_density_unique[of Px S Py ] Px Py
   456   show ?thesis
   457     by (auto simp: distributed_def)
   458 qed
   459 
   460 lemma (in prob_space) distributed_jointI:
   461   assumes "sigma_finite_measure S" "sigma_finite_measure T"
   462   assumes X[measurable]: "X \<in> measurable M S" and Y[measurable]: "Y \<in> measurable M T"
   463   assumes [measurable]: "f \<in> borel_measurable (S \<Otimes>\<^isub>M T)" and f: "AE x in S \<Otimes>\<^isub>M T. 0 \<le> f x"
   464   assumes eq: "\<And>A B. A \<in> sets S \<Longrightarrow> B \<in> sets T \<Longrightarrow> 
   465     emeasure M {x \<in> space M. X x \<in> A \<and> Y x \<in> B} = (\<integral>\<^isup>+x. (\<integral>\<^isup>+y. f (x, y) * indicator B y \<partial>T) * indicator A x \<partial>S)"
   466   shows "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) f"
   467   unfolding distributed_def
   468 proof safe
   469   interpret S: sigma_finite_measure S by fact
   470   interpret T: sigma_finite_measure T by fact
   471   interpret ST: pair_sigma_finite S T by default
   472 
   473   from ST.sigma_finite_up_in_pair_measure_generator guess F :: "nat \<Rightarrow> ('b \<times> 'c) set" .. note F = this
   474   let ?E = "{a \<times> b |a b. a \<in> sets S \<and> b \<in> sets T}"
   475   let ?P = "S \<Otimes>\<^isub>M T"
   476   show "distr M ?P (\<lambda>x. (X x, Y x)) = density ?P f" (is "?L = ?R")
   477   proof (rule measure_eqI_generator_eq[OF Int_stable_pair_measure_generator[of S T]])
   478     show "?E \<subseteq> Pow (space ?P)"
   479       using sets.space_closed[of S] sets.space_closed[of T] by (auto simp: space_pair_measure)
   480     show "sets ?L = sigma_sets (space ?P) ?E"
   481       by (simp add: sets_pair_measure space_pair_measure)
   482     then show "sets ?R = sigma_sets (space ?P) ?E"
   483       by simp
   484   next
   485     interpret L: prob_space ?L
   486       by (rule prob_space_distr) (auto intro!: measurable_Pair)
   487     show "range F \<subseteq> ?E" "(\<Union>i. F i) = space ?P" "\<And>i. emeasure ?L (F i) \<noteq> \<infinity>"
   488       using F by (auto simp: space_pair_measure)
   489   next
   490     fix E assume "E \<in> ?E"
   491     then obtain A B where E[simp]: "E = A \<times> B"
   492       and A[measurable]: "A \<in> sets S" and B[measurable]: "B \<in> sets T" by auto
   493     have "emeasure ?L E = emeasure M {x \<in> space M. X x \<in> A \<and> Y x \<in> B}"
   494       by (auto intro!: arg_cong[where f="emeasure M"] simp add: emeasure_distr measurable_Pair)
   495     also have "\<dots> = (\<integral>\<^isup>+x. (\<integral>\<^isup>+y. (f (x, y) * indicator B y) * indicator A x \<partial>T) \<partial>S)"
   496       using f by (auto simp add: eq positive_integral_multc intro!: positive_integral_cong)
   497     also have "\<dots> = emeasure ?R E"
   498       by (auto simp add: emeasure_density T.positive_integral_fst_measurable(2)[symmetric]
   499                intro!: positive_integral_cong split: split_indicator)
   500     finally show "emeasure ?L E = emeasure ?R E" .
   501   qed
   502 qed (auto simp: f)
   503 
   504 lemma (in prob_space) distributed_swap:
   505   assumes "sigma_finite_measure S" "sigma_finite_measure T"
   506   assumes Pxy: "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) Pxy"
   507   shows "distributed M (T \<Otimes>\<^isub>M S) (\<lambda>x. (Y x, X x)) (\<lambda>(x, y). Pxy (y, x))"
   508 proof -
   509   interpret S: sigma_finite_measure S by fact
   510   interpret T: sigma_finite_measure T by fact
   511   interpret ST: pair_sigma_finite S T by default
   512   interpret TS: pair_sigma_finite T S by default
   513 
   514   note Pxy[measurable]
   515   show ?thesis 
   516     apply (subst TS.distr_pair_swap)
   517     unfolding distributed_def
   518   proof safe
   519     let ?D = "distr (S \<Otimes>\<^isub>M T) (T \<Otimes>\<^isub>M S) (\<lambda>(x, y). (y, x))"
   520     show 1: "(\<lambda>(x, y). Pxy (y, x)) \<in> borel_measurable ?D"
   521       by auto
   522     with Pxy
   523     show "AE x in distr (S \<Otimes>\<^isub>M T) (T \<Otimes>\<^isub>M S) (\<lambda>(x, y). (y, x)). 0 \<le> (case x of (x, y) \<Rightarrow> Pxy (y, x))"
   524       by (subst AE_distr_iff)
   525          (auto dest!: distributed_AE
   526                simp: measurable_split_conv split_beta
   527                intro!: measurable_Pair)
   528     show 2: "random_variable (distr (S \<Otimes>\<^isub>M T) (T \<Otimes>\<^isub>M S) (\<lambda>(x, y). (y, x))) (\<lambda>x. (Y x, X x))"
   529       using Pxy by auto
   530     { fix A assume A: "A \<in> sets (T \<Otimes>\<^isub>M S)"
   531       let ?B = "(\<lambda>(x, y). (y, x)) -` A \<inter> space (S \<Otimes>\<^isub>M T)"
   532       from sets.sets_into_space[OF A]
   533       have "emeasure M ((\<lambda>x. (Y x, X x)) -` A \<inter> space M) =
   534         emeasure M ((\<lambda>x. (X x, Y x)) -` ?B \<inter> space M)"
   535         by (auto intro!: arg_cong2[where f=emeasure] simp: space_pair_measure)
   536       also have "\<dots> = (\<integral>\<^isup>+ x. Pxy x * indicator ?B x \<partial>(S \<Otimes>\<^isub>M T))"
   537         using Pxy A by (intro distributed_emeasure) auto
   538       finally have "emeasure M ((\<lambda>x. (Y x, X x)) -` A \<inter> space M) =
   539         (\<integral>\<^isup>+ x. Pxy x * indicator A (snd x, fst x) \<partial>(S \<Otimes>\<^isub>M T))"
   540         by (auto intro!: positive_integral_cong split: split_indicator) }
   541     note * = this
   542     show "distr M ?D (\<lambda>x. (Y x, X x)) = density ?D (\<lambda>(x, y). Pxy (y, x))"
   543       apply (intro measure_eqI)
   544       apply (simp_all add: emeasure_distr[OF 2] emeasure_density[OF 1])
   545       apply (subst positive_integral_distr)
   546       apply (auto intro!: * simp: comp_def split_beta)
   547       done
   548   qed
   549 qed
   550 
   551 lemma (in prob_space) distr_marginal1:
   552   assumes "sigma_finite_measure S" "sigma_finite_measure T"
   553   assumes Pxy: "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) Pxy"
   554   defines "Px \<equiv> \<lambda>x. (\<integral>\<^isup>+z. Pxy (x, z) \<partial>T)"
   555   shows "distributed M S X Px"
   556   unfolding distributed_def
   557 proof safe
   558   interpret S: sigma_finite_measure S by fact
   559   interpret T: sigma_finite_measure T by fact
   560   interpret ST: pair_sigma_finite S T by default
   561 
   562   note Pxy[measurable]
   563   show X: "X \<in> measurable M S" by simp
   564 
   565   show borel: "Px \<in> borel_measurable S"
   566     by (auto intro!: T.positive_integral_fst_measurable simp: Px_def)
   567 
   568   interpret Pxy: prob_space "distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))"
   569     by (intro prob_space_distr) simp
   570   have "(\<integral>\<^isup>+ x. max 0 (- Pxy x) \<partial>(S \<Otimes>\<^isub>M T)) = (\<integral>\<^isup>+ x. 0 \<partial>(S \<Otimes>\<^isub>M T))"
   571     using Pxy
   572     by (intro positive_integral_cong_AE) (auto simp: max_def dest: distributed_AE)
   573 
   574   show "distr M S X = density S Px"
   575   proof (rule measure_eqI)
   576     fix A assume A: "A \<in> sets (distr M S X)"
   577     with X measurable_space[of Y M T]
   578     have "emeasure (distr M S X) A = emeasure (distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))) (A \<times> space T)"
   579       by (auto simp add: emeasure_distr intro!: arg_cong[where f="emeasure M"])
   580     also have "\<dots> = emeasure (density (S \<Otimes>\<^isub>M T) Pxy) (A \<times> space T)"
   581       using Pxy by (simp add: distributed_def)
   582     also have "\<dots> = \<integral>\<^isup>+ x. \<integral>\<^isup>+ y. Pxy (x, y) * indicator (A \<times> space T) (x, y) \<partial>T \<partial>S"
   583       using A borel Pxy
   584       by (simp add: emeasure_density T.positive_integral_fst_measurable(2)[symmetric])
   585     also have "\<dots> = \<integral>\<^isup>+ x. Px x * indicator A x \<partial>S"
   586       apply (rule positive_integral_cong_AE)
   587       using Pxy[THEN distributed_AE, THEN ST.AE_pair] AE_space
   588     proof eventually_elim
   589       fix x assume "x \<in> space S" "AE y in T. 0 \<le> Pxy (x, y)"
   590       moreover have eq: "\<And>y. y \<in> space T \<Longrightarrow> indicator (A \<times> space T) (x, y) = indicator A x"
   591         by (auto simp: indicator_def)
   592       ultimately have "(\<integral>\<^isup>+ y. Pxy (x, y) * indicator (A \<times> space T) (x, y) \<partial>T) = (\<integral>\<^isup>+ y. Pxy (x, y) \<partial>T) * indicator A x"
   593         by (simp add: eq positive_integral_multc cong: positive_integral_cong)
   594       also have "(\<integral>\<^isup>+ y. Pxy (x, y) \<partial>T) = Px x"
   595         by (simp add: Px_def ereal_real positive_integral_positive)
   596       finally show "(\<integral>\<^isup>+ y. Pxy (x, y) * indicator (A \<times> space T) (x, y) \<partial>T) = Px x * indicator A x" .
   597     qed
   598     finally show "emeasure (distr M S X) A = emeasure (density S Px) A"
   599       using A borel Pxy by (simp add: emeasure_density)
   600   qed simp
   601   
   602   show "AE x in S. 0 \<le> Px x"
   603     by (simp add: Px_def positive_integral_positive real_of_ereal_pos)
   604 qed
   605 
   606 lemma (in prob_space) distr_marginal2:
   607   assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T"
   608   assumes Pxy: "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) Pxy"
   609   shows "distributed M T Y (\<lambda>y. (\<integral>\<^isup>+x. Pxy (x, y) \<partial>S))"
   610   using distr_marginal1[OF T S distributed_swap[OF S T]] Pxy by simp
   611 
   612 lemma (in prob_space) distributed_marginal_eq_joint1:
   613   assumes T: "sigma_finite_measure T"
   614   assumes S: "sigma_finite_measure S"
   615   assumes Px: "distributed M S X Px"
   616   assumes Pxy: "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) Pxy"
   617   shows "AE x in S. Px x = (\<integral>\<^isup>+y. Pxy (x, y) \<partial>T)"
   618   using Px distr_marginal1[OF S T Pxy] by (rule distributed_unique)
   619 
   620 lemma (in prob_space) distributed_marginal_eq_joint2:
   621   assumes T: "sigma_finite_measure T"
   622   assumes S: "sigma_finite_measure S"
   623   assumes Py: "distributed M T Y Py"
   624   assumes Pxy: "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) Pxy"
   625   shows "AE y in T. Py y = (\<integral>\<^isup>+x. Pxy (x, y) \<partial>S)"
   626   using Py distr_marginal2[OF S T Pxy] by (rule distributed_unique)
   627 
   628 lemma (in prob_space) distributed_joint_indep':
   629   assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T"
   630   assumes X[measurable]: "distributed M S X Px" and Y[measurable]: "distributed M T Y Py"
   631   assumes indep: "distr M S X \<Otimes>\<^isub>M distr M T Y = distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))"
   632   shows "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) (\<lambda>(x, y). Px x * Py y)"
   633   unfolding distributed_def
   634 proof safe
   635   interpret S: sigma_finite_measure S by fact
   636   interpret T: sigma_finite_measure T by fact
   637   interpret ST: pair_sigma_finite S T by default
   638 
   639   interpret X: prob_space "density S Px"
   640     unfolding distributed_distr_eq_density[OF X, symmetric]
   641     by (rule prob_space_distr) simp
   642   have sf_X: "sigma_finite_measure (density S Px)" ..
   643 
   644   interpret Y: prob_space "density T Py"
   645     unfolding distributed_distr_eq_density[OF Y, symmetric]
   646     by (rule prob_space_distr) simp
   647   have sf_Y: "sigma_finite_measure (density T Py)" ..
   648 
   649   show "distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) = density (S \<Otimes>\<^isub>M T) (\<lambda>(x, y). Px x * Py y)"
   650     unfolding indep[symmetric] distributed_distr_eq_density[OF X] distributed_distr_eq_density[OF Y]
   651     using distributed_borel_measurable[OF X] distributed_AE[OF X]
   652     using distributed_borel_measurable[OF Y] distributed_AE[OF Y]
   653     by (rule pair_measure_density[OF _ _ _ _ T sf_Y])
   654 
   655   show "random_variable (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))" by auto
   656 
   657   show Pxy: "(\<lambda>(x, y). Px x * Py y) \<in> borel_measurable (S \<Otimes>\<^isub>M T)" by auto
   658 
   659   show "AE x in S \<Otimes>\<^isub>M T. 0 \<le> (case x of (x, y) \<Rightarrow> Px x * Py y)"
   660     apply (intro ST.AE_pair_measure borel_measurable_le Pxy borel_measurable_const)
   661     using distributed_AE[OF X]
   662     apply eventually_elim
   663     using distributed_AE[OF Y]
   664     apply eventually_elim
   665     apply auto
   666     done
   667 qed
   668 
   669 definition
   670   "simple_distributed M X f \<longleftrightarrow> distributed M (count_space (X`space M)) X (\<lambda>x. ereal (f x)) \<and>
   671     finite (X`space M)"
   672 
   673 lemma simple_distributed:
   674   "simple_distributed M X Px \<Longrightarrow> distributed M (count_space (X`space M)) X Px"
   675   unfolding simple_distributed_def by auto
   676 
   677 lemma simple_distributed_finite[dest]: "simple_distributed M X P \<Longrightarrow> finite (X`space M)"
   678   by (simp add: simple_distributed_def)
   679 
   680 lemma (in prob_space) distributed_simple_function_superset:
   681   assumes X: "simple_function M X" "\<And>x. x \<in> X ` space M \<Longrightarrow> P x = measure M (X -` {x} \<inter> space M)"
   682   assumes A: "X`space M \<subseteq> A" "finite A"
   683   defines "S \<equiv> count_space A" and "P' \<equiv> (\<lambda>x. if x \<in> X`space M then P x else 0)"
   684   shows "distributed M S X P'"
   685   unfolding distributed_def
   686 proof safe
   687   show "(\<lambda>x. ereal (P' x)) \<in> borel_measurable S" unfolding S_def by simp
   688   show "AE x in S. 0 \<le> ereal (P' x)"
   689     using X by (auto simp: S_def P'_def simple_distributed_def intro!: measure_nonneg)
   690   show "distr M S X = density S P'"
   691   proof (rule measure_eqI_finite)
   692     show "sets (distr M S X) = Pow A" "sets (density S P') = Pow A"
   693       using A unfolding S_def by auto
   694     show "finite A" by fact
   695     fix a assume a: "a \<in> A"
   696     then have "a \<notin> X`space M \<Longrightarrow> X -` {a} \<inter> space M = {}" by auto
   697     with A a X have "emeasure (distr M S X) {a} = P' a"
   698       by (subst emeasure_distr)
   699          (auto simp add: S_def P'_def simple_functionD emeasure_eq_measure measurable_count_space_eq2
   700                intro!: arg_cong[where f=prob])
   701     also have "\<dots> = (\<integral>\<^isup>+x. ereal (P' a) * indicator {a} x \<partial>S)"
   702       using A X a
   703       by (subst positive_integral_cmult_indicator)
   704          (auto simp: S_def P'_def simple_distributed_def simple_functionD measure_nonneg)
   705     also have "\<dots> = (\<integral>\<^isup>+x. ereal (P' x) * indicator {a} x \<partial>S)"
   706       by (auto simp: indicator_def intro!: positive_integral_cong)
   707     also have "\<dots> = emeasure (density S P') {a}"
   708       using a A by (intro emeasure_density[symmetric]) (auto simp: S_def)
   709     finally show "emeasure (distr M S X) {a} = emeasure (density S P') {a}" .
   710   qed
   711   show "random_variable S X"
   712     using X(1) A by (auto simp: measurable_def simple_functionD S_def)
   713 qed
   714 
   715 lemma (in prob_space) simple_distributedI:
   716   assumes X: "simple_function M X" "\<And>x. x \<in> X ` space M \<Longrightarrow> P x = measure M (X -` {x} \<inter> space M)"
   717   shows "simple_distributed M X P"
   718   unfolding simple_distributed_def
   719 proof
   720   have "distributed M (count_space (X ` space M)) X (\<lambda>x. ereal (if x \<in> X`space M then P x else 0))"
   721     (is "?A")
   722     using simple_functionD[OF X(1)] by (intro distributed_simple_function_superset[OF X]) auto
   723   also have "?A \<longleftrightarrow> distributed M (count_space (X ` space M)) X (\<lambda>x. ereal (P x))"
   724     by (rule distributed_cong_density) auto
   725   finally show "\<dots>" .
   726 qed (rule simple_functionD[OF X(1)])
   727 
   728 lemma simple_distributed_joint_finite:
   729   assumes X: "simple_distributed M (\<lambda>x. (X x, Y x)) Px"
   730   shows "finite (X ` space M)" "finite (Y ` space M)"
   731 proof -
   732   have "finite ((\<lambda>x. (X x, Y x)) ` space M)"
   733     using X by (auto simp: simple_distributed_def simple_functionD)
   734   then have "finite (fst ` (\<lambda>x. (X x, Y x)) ` space M)" "finite (snd ` (\<lambda>x. (X x, Y x)) ` space M)"
   735     by auto
   736   then show fin: "finite (X ` space M)" "finite (Y ` space M)"
   737     by (auto simp: image_image)
   738 qed
   739 
   740 lemma simple_distributed_joint2_finite:
   741   assumes X: "simple_distributed M (\<lambda>x. (X x, Y x, Z x)) Px"
   742   shows "finite (X ` space M)" "finite (Y ` space M)" "finite (Z ` space M)"
   743 proof -
   744   have "finite ((\<lambda>x. (X x, Y x, Z x)) ` space M)"
   745     using X by (auto simp: simple_distributed_def simple_functionD)
   746   then have "finite (fst ` (\<lambda>x. (X x, Y x, Z x)) ` space M)"
   747     "finite ((fst \<circ> snd) ` (\<lambda>x. (X x, Y x, Z x)) ` space M)"
   748     "finite ((snd \<circ> snd) ` (\<lambda>x. (X x, Y x, Z x)) ` space M)"
   749     by auto
   750   then show fin: "finite (X ` space M)" "finite (Y ` space M)" "finite (Z ` space M)"
   751     by (auto simp: image_image)
   752 qed
   753 
   754 lemma simple_distributed_simple_function:
   755   "simple_distributed M X Px \<Longrightarrow> simple_function M X"
   756   unfolding simple_distributed_def distributed_def
   757   by (auto simp: simple_function_def measurable_count_space_eq2)
   758 
   759 lemma simple_distributed_measure:
   760   "simple_distributed M X P \<Longrightarrow> a \<in> X`space M \<Longrightarrow> P a = measure M (X -` {a} \<inter> space M)"
   761   using distributed_count_space[of M "X`space M" X P a, symmetric]
   762   by (auto simp: simple_distributed_def measure_def)
   763 
   764 lemma simple_distributed_nonneg: "simple_distributed M X f \<Longrightarrow> x \<in> space M \<Longrightarrow> 0 \<le> f (X x)"
   765   by (auto simp: simple_distributed_measure measure_nonneg)
   766 
   767 lemma (in prob_space) simple_distributed_joint:
   768   assumes X: "simple_distributed M (\<lambda>x. (X x, Y x)) Px"
   769   defines "S \<equiv> count_space (X`space M) \<Otimes>\<^isub>M count_space (Y`space M)"
   770   defines "P \<equiv> (\<lambda>x. if x \<in> (\<lambda>x. (X x, Y x))`space M then Px x else 0)"
   771   shows "distributed M S (\<lambda>x. (X x, Y x)) P"
   772 proof -
   773   from simple_distributed_joint_finite[OF X, simp]
   774   have S_eq: "S = count_space (X`space M \<times> Y`space M)"
   775     by (simp add: S_def pair_measure_count_space)
   776   show ?thesis
   777     unfolding S_eq P_def
   778   proof (rule distributed_simple_function_superset)
   779     show "simple_function M (\<lambda>x. (X x, Y x))"
   780       using X by (rule simple_distributed_simple_function)
   781     fix x assume "x \<in> (\<lambda>x. (X x, Y x)) ` space M"
   782     from simple_distributed_measure[OF X this]
   783     show "Px x = prob ((\<lambda>x. (X x, Y x)) -` {x} \<inter> space M)" .
   784   qed auto
   785 qed
   786 
   787 lemma (in prob_space) simple_distributed_joint2:
   788   assumes X: "simple_distributed M (\<lambda>x. (X x, Y x, Z x)) Px"
   789   defines "S \<equiv> count_space (X`space M) \<Otimes>\<^isub>M count_space (Y`space M) \<Otimes>\<^isub>M count_space (Z`space M)"
   790   defines "P \<equiv> (\<lambda>x. if x \<in> (\<lambda>x. (X x, Y x, Z x))`space M then Px x else 0)"
   791   shows "distributed M S (\<lambda>x. (X x, Y x, Z x)) P"
   792 proof -
   793   from simple_distributed_joint2_finite[OF X, simp]
   794   have S_eq: "S = count_space (X`space M \<times> Y`space M \<times> Z`space M)"
   795     by (simp add: S_def pair_measure_count_space)
   796   show ?thesis
   797     unfolding S_eq P_def
   798   proof (rule distributed_simple_function_superset)
   799     show "simple_function M (\<lambda>x. (X x, Y x, Z x))"
   800       using X by (rule simple_distributed_simple_function)
   801     fix x assume "x \<in> (\<lambda>x. (X x, Y x, Z x)) ` space M"
   802     from simple_distributed_measure[OF X this]
   803     show "Px x = prob ((\<lambda>x. (X x, Y x, Z x)) -` {x} \<inter> space M)" .
   804   qed auto
   805 qed
   806 
   807 lemma (in prob_space) simple_distributed_setsum_space:
   808   assumes X: "simple_distributed M X f"
   809   shows "setsum f (X`space M) = 1"
   810 proof -
   811   from X have "setsum f (X`space M) = prob (\<Union>i\<in>X`space M. X -` {i} \<inter> space M)"
   812     by (subst finite_measure_finite_Union)
   813        (auto simp add: disjoint_family_on_def simple_distributed_measure simple_distributed_simple_function simple_functionD
   814              intro!: setsum_cong arg_cong[where f="prob"])
   815   also have "\<dots> = prob (space M)"
   816     by (auto intro!: arg_cong[where f=prob])
   817   finally show ?thesis
   818     using emeasure_space_1 by (simp add: emeasure_eq_measure one_ereal_def)
   819 qed
   820 
   821 lemma (in prob_space) distributed_marginal_eq_joint_simple:
   822   assumes Px: "simple_function M X"
   823   assumes Py: "simple_distributed M Y Py"
   824   assumes Pxy: "simple_distributed M (\<lambda>x. (X x, Y x)) Pxy"
   825   assumes y: "y \<in> Y`space M"
   826   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)"
   827 proof -
   828   note Px = simple_distributedI[OF Px refl]
   829   have *: "\<And>f A. setsum (\<lambda>x. max 0 (ereal (f x))) A = ereal (setsum (\<lambda>x. max 0 (f x)) A)"
   830     by (simp add: setsum_ereal[symmetric] zero_ereal_def)
   831   from distributed_marginal_eq_joint2[OF
   832     sigma_finite_measure_count_space_finite
   833     sigma_finite_measure_count_space_finite
   834     simple_distributed[OF Py] simple_distributed_joint[OF Pxy],
   835     OF Py[THEN simple_distributed_finite] Px[THEN simple_distributed_finite]]
   836     y
   837     Px[THEN simple_distributed_finite]
   838     Py[THEN simple_distributed_finite]
   839     Pxy[THEN simple_distributed, THEN distributed_real_AE]
   840   show ?thesis
   841     unfolding AE_count_space
   842     apply (auto simp add: positive_integral_count_space_finite * intro!: setsum_cong split: split_max)
   843     done
   844 qed
   845 
   846 lemma distributedI_real:
   847   fixes f :: "'a \<Rightarrow> real"
   848   assumes gen: "sets M1 = sigma_sets (space M1) E" and "Int_stable E"
   849     and A: "range A \<subseteq> E" "(\<Union>i::nat. A i) = space M1" "\<And>i. emeasure (distr M M1 X) (A i) \<noteq> \<infinity>"
   850     and X: "X \<in> measurable M M1"
   851     and f: "f \<in> borel_measurable M1" "AE x in M1. 0 \<le> f x"
   852     and eq: "\<And>A. A \<in> E \<Longrightarrow> emeasure M (X -` A \<inter> space M) = (\<integral>\<^isup>+ x. f x * indicator A x \<partial>M1)"
   853   shows "distributed M M1 X f"
   854   unfolding distributed_def
   855 proof (intro conjI)
   856   show "distr M M1 X = density M1 f"
   857   proof (rule measure_eqI_generator_eq[where A=A])
   858     { fix A assume A: "A \<in> E"
   859       then have "A \<in> sigma_sets (space M1) E" by auto
   860       then have "A \<in> sets M1"
   861         using gen by simp
   862       with f A eq[of A] X show "emeasure (distr M M1 X) A = emeasure (density M1 f) A"
   863         by (simp add: emeasure_distr emeasure_density borel_measurable_ereal
   864                       times_ereal.simps[symmetric] ereal_indicator
   865                  del: times_ereal.simps) }
   866     note eq_E = this
   867     show "Int_stable E" by fact
   868     { fix e assume "e \<in> E"
   869       then have "e \<in> sigma_sets (space M1) E" by auto
   870       then have "e \<in> sets M1" unfolding gen .
   871       then have "e \<subseteq> space M1" by (rule sets.sets_into_space) }
   872     then show "E \<subseteq> Pow (space M1)" by auto
   873     show "sets (distr M M1 X) = sigma_sets (space M1) E"
   874       "sets (density M1 (\<lambda>x. ereal (f x))) = sigma_sets (space M1) E"
   875       unfolding gen[symmetric] by auto
   876   qed fact+
   877 qed (insert X f, auto)
   878 
   879 lemma distributedI_borel_atMost:
   880   fixes f :: "real \<Rightarrow> real"
   881   assumes [measurable]: "X \<in> borel_measurable M"
   882     and [measurable]: "f \<in> borel_measurable borel" and f[simp]: "AE x in lborel. 0 \<le> f x"
   883     and g_eq: "\<And>a. (\<integral>\<^isup>+x. f x * indicator {..a} x \<partial>lborel)  = ereal (g a)"
   884     and M_eq: "\<And>a. emeasure M {x\<in>space M. X x \<le> a} = ereal (g a)"
   885   shows "distributed M lborel X f"
   886 proof (rule distributedI_real)
   887   show "sets lborel = sigma_sets (space lborel) (range atMost)"
   888     by (simp add: borel_eq_atMost)
   889   show "Int_stable (range atMost :: real set set)"
   890     by (auto simp: Int_stable_def)
   891   have vimage_eq: "\<And>a. (X -` {..a} \<inter> space M) = {x\<in>space M. X x \<le> a}" by auto
   892   def A \<equiv> "\<lambda>i::nat. {.. real i}"
   893   then show "range A \<subseteq> range atMost" "(\<Union>i. A i) = space lborel"
   894     "\<And>i. emeasure (distr M lborel X) (A i) \<noteq> \<infinity>"
   895     by (auto simp: real_arch_simple emeasure_distr vimage_eq M_eq)
   896 
   897   fix A :: "real set" assume "A \<in> range atMost"
   898   then obtain a where A: "A = {..a}" by auto
   899   show "emeasure M (X -` A \<inter> space M) = (\<integral>\<^isup>+x. f x * indicator A x \<partial>lborel)"
   900     unfolding vimage_eq A M_eq g_eq ..
   901 qed auto
   902 
   903 lemma (in prob_space) uniform_distributed_params:
   904   assumes X: "distributed M MX X (\<lambda>x. indicator A x / measure MX A)"
   905   shows "A \<in> sets MX" "measure MX A \<noteq> 0"
   906 proof -
   907   interpret X: prob_space "distr M MX X"
   908     using distributed_measurable[OF X] by (rule prob_space_distr)
   909 
   910   show "measure MX A \<noteq> 0"
   911   proof
   912     assume "measure MX A = 0"
   913     with X.emeasure_space_1 X.prob_space distributed_distr_eq_density[OF X]
   914     show False
   915       by (simp add: emeasure_density zero_ereal_def[symmetric])
   916   qed
   917   with measure_notin_sets[of A MX] show "A \<in> sets MX"
   918     by blast
   919 qed
   920 
   921 lemma prob_space_uniform_measure:
   922   assumes A: "emeasure M A \<noteq> 0" "emeasure M A \<noteq> \<infinity>"
   923   shows "prob_space (uniform_measure M A)"
   924 proof
   925   show "emeasure (uniform_measure M A) (space (uniform_measure M A)) = 1"
   926     using emeasure_uniform_measure[OF emeasure_neq_0_sets[OF A(1)], of "space M"]
   927     using sets.sets_into_space[OF emeasure_neq_0_sets[OF A(1)]] A
   928     by (simp add: Int_absorb2 emeasure_nonneg)
   929 qed
   930 
   931 lemma prob_space_uniform_count_measure: "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> prob_space (uniform_count_measure A)"
   932   by default (auto simp: emeasure_uniform_count_measure space_uniform_count_measure one_ereal_def)
   933 
   934 end