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