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