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