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