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