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