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