src/HOL/Probability/Probability_Space.thy
author hoelzl
Mon May 03 14:35:10 2010 +0200 (2010-05-03)
changeset 36624 25153c08655e
parent 35977 30d42bfd0174
child 38656 d5d342611edb
permissions -rw-r--r--
Cleanup information theory
hoelzl@35582
     1
theory Probability_Space
hoelzl@35582
     2
imports Lebesgue
hoelzl@35582
     3
begin
hoelzl@35582
     4
hoelzl@35582
     5
locale prob_space = measure_space +
hoelzl@35582
     6
  assumes prob_space: "measure M (space M) = 1"
hoelzl@35582
     7
begin
hoelzl@35582
     8
hoelzl@35582
     9
abbreviation "events \<equiv> sets M"
hoelzl@35582
    10
abbreviation "prob \<equiv> measure M"
hoelzl@35582
    11
abbreviation "prob_preserving \<equiv> measure_preserving"
hoelzl@35582
    12
abbreviation "random_variable \<equiv> \<lambda> s X. X \<in> measurable M s"
hoelzl@35582
    13
abbreviation "expectation \<equiv> integral"
hoelzl@35582
    14
hoelzl@35582
    15
definition
hoelzl@35582
    16
  "indep A B \<longleftrightarrow> A \<in> events \<and> B \<in> events \<and> prob (A \<inter> B) = prob A * prob B"
hoelzl@35582
    17
hoelzl@35582
    18
definition
hoelzl@35582
    19
  "indep_families F G \<longleftrightarrow> (\<forall> A \<in> F. \<forall> B \<in> G. indep A B)"
hoelzl@35582
    20
hoelzl@35582
    21
definition
hoelzl@35582
    22
  "distribution X = (\<lambda>s. prob ((X -` s) \<inter> (space M)))"
hoelzl@35582
    23
hoelzl@36624
    24
abbreviation
hoelzl@36624
    25
  "joint_distribution X Y \<equiv> distribution (\<lambda>x. (X x, Y x))"
hoelzl@35582
    26
hoelzl@36624
    27
(*
hoelzl@36624
    28
definition probably :: "('a \<Rightarrow> bool) \<Rightarrow> bool" (binder "\<forall>\<^sup>*" 10) where
hoelzl@36624
    29
  "probably P \<longleftrightarrow> { x. P x } \<in> events \<and> prob { x. P x } = 1"
hoelzl@36624
    30
definition possibly :: "('a \<Rightarrow> bool) \<Rightarrow> bool" (binder "\<exists>\<^sup>*" 10) where
hoelzl@36624
    31
  "possibly P \<longleftrightarrow> { x. P x } \<in> events \<and> prob { x. P x } \<noteq> 0"
hoelzl@36624
    32
*)
hoelzl@35582
    33
hoelzl@35582
    34
definition
hoelzl@36624
    35
  "conditional_expectation X M' \<equiv> SOME f. f \<in> measurable M' borel_space \<and>
hoelzl@36624
    36
    (\<forall> g \<in> sets M'. measure_space.integral M' (\<lambda>x. f x * indicator_fn g x) =
hoelzl@36624
    37
                    measure_space.integral M' (\<lambda>x. X x * indicator_fn g x))"
hoelzl@35582
    38
hoelzl@35582
    39
definition
hoelzl@36624
    40
  "conditional_prob E M' \<equiv> conditional_expectation (indicator_fn E) M'"
hoelzl@35582
    41
hoelzl@35929
    42
lemma positive': "positive M prob"
hoelzl@35582
    43
  unfolding positive_def using positive empty_measure by blast
hoelzl@35582
    44
hoelzl@35582
    45
lemma prob_compl:
hoelzl@35582
    46
  assumes "s \<in> events"
hoelzl@35582
    47
  shows "prob (space M - s) = 1 - prob s"
hoelzl@35582
    48
using assms
hoelzl@35582
    49
proof -
hoelzl@35582
    50
  have "prob ((space M - s) \<union> s) = prob (space M - s) + prob s"
hoelzl@35582
    51
    using assms additive[unfolded additive_def] by blast
hoelzl@35582
    52
  thus ?thesis by (simp add:Un_absorb2[OF sets_into_space[OF assms]] prob_space)
hoelzl@35582
    53
qed
hoelzl@35582
    54
hoelzl@35582
    55
lemma indep_space:
hoelzl@35582
    56
  assumes "s \<in> events"
hoelzl@35582
    57
  shows "indep (space M) s"
hoelzl@35582
    58
using assms prob_space
hoelzl@35582
    59
unfolding indep_def by auto
hoelzl@35582
    60
hoelzl@35582
    61
hoelzl@35582
    62
lemma prob_space_increasing:
hoelzl@35582
    63
  "increasing M prob"
hoelzl@35929
    64
by (rule additive_increasing[OF positive' additive])
hoelzl@35582
    65
hoelzl@35582
    66
lemma prob_subadditive:
hoelzl@35582
    67
  assumes "s \<in> events" "t \<in> events"
hoelzl@35582
    68
  shows "prob (s \<union> t) \<le> prob s + prob t"
hoelzl@35582
    69
using assms
hoelzl@35582
    70
proof -
hoelzl@35582
    71
  have "prob (s \<union> t) = prob ((s - t) \<union> t)" by simp
hoelzl@35582
    72
  also have "\<dots> = prob (s - t) + prob t"
hoelzl@35582
    73
    using additive[unfolded additive_def, rule_format, of "s-t" "t"] 
hoelzl@35582
    74
      assms by blast
hoelzl@35582
    75
  also have "\<dots> \<le> prob s + prob t"
hoelzl@35582
    76
    using prob_space_increasing[unfolded increasing_def, rule_format] assms
hoelzl@35582
    77
    by auto
hoelzl@35582
    78
  finally show ?thesis by simp
hoelzl@35582
    79
qed
hoelzl@35582
    80
hoelzl@35582
    81
lemma prob_zero_union:
hoelzl@35582
    82
  assumes "s \<in> events" "t \<in> events" "prob t = 0"
hoelzl@35582
    83
  shows "prob (s \<union> t) = prob s"
hoelzl@35582
    84
using assms 
hoelzl@35582
    85
proof -
hoelzl@35582
    86
  have "prob (s \<union> t) \<le> prob s"
hoelzl@35582
    87
    using prob_subadditive[of s t] assms by auto
hoelzl@35582
    88
  moreover have "prob (s \<union> t) \<ge> prob s"
hoelzl@35582
    89
    using prob_space_increasing[unfolded increasing_def, rule_format] 
hoelzl@35582
    90
      assms by auto
hoelzl@35582
    91
  ultimately show ?thesis by simp
hoelzl@35582
    92
qed
hoelzl@35582
    93
hoelzl@35582
    94
lemma prob_eq_compl:
hoelzl@35582
    95
  assumes "s \<in> events" "t \<in> events"
hoelzl@35582
    96
  assumes "prob (space M - s) = prob (space M - t)"
hoelzl@35582
    97
  shows "prob s = prob t"
hoelzl@35582
    98
using assms prob_compl by auto
hoelzl@35582
    99
hoelzl@35582
   100
lemma prob_one_inter:
hoelzl@35582
   101
  assumes events:"s \<in> events" "t \<in> events"
hoelzl@35582
   102
  assumes "prob t = 1"
hoelzl@35582
   103
  shows "prob (s \<inter> t) = prob s"
hoelzl@35582
   104
using assms
hoelzl@35582
   105
proof -
hoelzl@35582
   106
  have "prob ((space M - s) \<union> (space M - t)) = prob (space M - s)" 
hoelzl@35582
   107
    using prob_compl[of "t"] prob_zero_union assms by auto
hoelzl@35582
   108
  then show "prob (s \<inter> t) = prob s" 
hoelzl@35582
   109
    using prob_eq_compl[of "s \<inter> t"] events by (simp only: Diff_Int) auto
hoelzl@35582
   110
qed
hoelzl@35582
   111
hoelzl@35582
   112
lemma prob_eq_bigunion_image:
hoelzl@35582
   113
  assumes "range f \<subseteq> events" "range g \<subseteq> events"
hoelzl@35582
   114
  assumes "disjoint_family f" "disjoint_family g"
hoelzl@35582
   115
  assumes "\<And> n :: nat. prob (f n) = prob (g n)"
hoelzl@35582
   116
  shows "(prob (\<Union> i. f i) = prob (\<Union> i. g i))"
hoelzl@35582
   117
using assms 
hoelzl@35582
   118
proof -
hoelzl@35582
   119
  have a: "(\<lambda> i. prob (f i)) sums (prob (\<Union> i. f i))" 
hoelzl@35582
   120
    using ca[unfolded countably_additive_def] assms by blast
hoelzl@35582
   121
  have b: "(\<lambda> i. prob (g i)) sums (prob (\<Union> i. g i))"
hoelzl@35582
   122
    using ca[unfolded countably_additive_def] assms by blast
hoelzl@35582
   123
  show ?thesis using sums_unique[OF b] sums_unique[OF a] assms by simp
hoelzl@35582
   124
qed
hoelzl@35582
   125
hoelzl@35582
   126
lemma prob_countably_subadditive: 
hoelzl@35582
   127
  assumes "range f \<subseteq> events" 
hoelzl@35582
   128
  assumes "summable (prob \<circ> f)"
hoelzl@35582
   129
  shows "prob (\<Union>i. f i) \<le> (\<Sum> i. prob (f i))"
hoelzl@35582
   130
using assms
hoelzl@35582
   131
proof -
hoelzl@35582
   132
  def f' == "\<lambda> i. f i - (\<Union> j \<in> {0 ..< i}. f j)"
hoelzl@35582
   133
  have "(\<Union> i. f' i) \<subseteq> (\<Union> i. f i)" unfolding f'_def by auto
hoelzl@35582
   134
  moreover have "(\<Union> i. f' i) \<supseteq> (\<Union> i. f i)"
hoelzl@35582
   135
  proof (rule subsetI)
hoelzl@35582
   136
    fix x assume "x \<in> (\<Union> i. f i)"
hoelzl@35582
   137
    then obtain k where "x \<in> f k" by blast
hoelzl@35582
   138
    hence k: "k \<in> {m. x \<in> f m}" by simp
hoelzl@35582
   139
    have "\<exists> l. x \<in> f l \<and> (\<forall> l' < l. x \<notin> f l')"
hoelzl@35582
   140
      using wfE_min[of "{(x, y). x < y}" "k" "{m. x \<in> f m}", 
hoelzl@35582
   141
        OF wf_less k] by auto
hoelzl@35582
   142
    thus "x \<in> (\<Union> i. f' i)" unfolding f'_def by auto
hoelzl@35582
   143
  qed
hoelzl@35582
   144
  ultimately have uf'f: "(\<Union> i. f' i) = (\<Union> i. f i)" by (rule equalityI)
hoelzl@35582
   145
hoelzl@35582
   146
  have df': "\<And> i j. i < j \<Longrightarrow> f' i \<inter> f' j = {}"
hoelzl@35582
   147
    unfolding f'_def by auto
hoelzl@35582
   148
  have "\<And> i j. i \<noteq> j \<Longrightarrow> f' i \<inter> f' j = {}"
hoelzl@35582
   149
    apply (drule iffD1[OF nat_neq_iff])
hoelzl@35582
   150
    using df' by auto
hoelzl@35582
   151
  hence df: "disjoint_family f'" unfolding disjoint_family_on_def by simp
hoelzl@35582
   152
hoelzl@35582
   153
  have rf': "\<And> i. f' i \<in> events"
hoelzl@35582
   154
  proof -
hoelzl@35582
   155
    fix i :: nat
hoelzl@35582
   156
    have "(\<Union> {f j | j. j \<in> {0 ..< i}}) = (\<Union> j \<in> {0 ..< i}. f j)" by blast
hoelzl@35582
   157
    hence "(\<Union> {f j | j. j \<in> {0 ..< i}}) \<in> events 
hoelzl@35582
   158
      \<Longrightarrow> (\<Union> j \<in> {0 ..< i}. f j) \<in> events" by auto
hoelzl@35582
   159
    thus "f' i \<in> events" 
hoelzl@35582
   160
      unfolding f'_def 
hoelzl@35582
   161
      using assms finite_union[of "{f j | j. j \<in> {0 ..< i}}"]
hoelzl@35582
   162
        Diff[of "f i" "\<Union> j \<in> {0 ..< i}. f j"] by auto
hoelzl@35582
   163
  qed
hoelzl@35582
   164
  hence uf': "(\<Union> range f') \<in> events" by auto
hoelzl@35582
   165
  
hoelzl@35582
   166
  have "\<And> i. prob (f' i) \<le> prob (f i)"
hoelzl@35582
   167
    using prob_space_increasing[unfolded increasing_def, rule_format, OF rf']
hoelzl@35582
   168
      assms rf' unfolding f'_def by blast
hoelzl@35582
   169
hoelzl@35582
   170
  hence absinc: "\<And> i. \<bar> prob (f' i) \<bar> \<le> prob (f i)"
hoelzl@35929
   171
    using abs_of_nonneg positive'[unfolded positive_def]
hoelzl@35582
   172
      assms rf' by auto
hoelzl@35582
   173
hoelzl@35582
   174
  have "prob (\<Union> i. f i) = prob (\<Union> i. f' i)" using uf'f by simp
hoelzl@35582
   175
hoelzl@35582
   176
  also have "\<dots> = (\<Sum> i. prob (f' i))"
hoelzl@35582
   177
    using ca[unfolded countably_additive_def, rule_format]
hoelzl@35582
   178
    sums_unique rf' uf' df
hoelzl@35582
   179
    by auto
hoelzl@35582
   180
  
hoelzl@35582
   181
  also have "\<dots> \<le> (\<Sum> i. prob (f i))"
hoelzl@35582
   182
    using summable_le2[of "\<lambda> i. prob (f' i)" "\<lambda> i. prob (f i)", 
hoelzl@35582
   183
      rule_format, OF absinc]
hoelzl@35582
   184
      assms[unfolded o_def] by auto
hoelzl@35582
   185
hoelzl@35582
   186
  finally show ?thesis by auto
hoelzl@35582
   187
qed
hoelzl@35582
   188
hoelzl@35582
   189
lemma prob_countably_zero:
hoelzl@35582
   190
  assumes "range c \<subseteq> events"
hoelzl@35582
   191
  assumes "\<And> i. prob (c i) = 0"
hoelzl@35582
   192
  shows "(prob (\<Union> i :: nat. c i) = 0)"
hoelzl@35582
   193
  using assms
hoelzl@35582
   194
proof -
hoelzl@35582
   195
  have leq0: "0 \<le> prob (\<Union> i. c i)"
hoelzl@35929
   196
    using assms positive'[unfolded positive_def, rule_format] 
hoelzl@35582
   197
    by auto
hoelzl@35582
   198
hoelzl@35582
   199
  have "prob (\<Union> i. c i) \<le> (\<Sum> i. prob (c i))"
hoelzl@35582
   200
    using prob_countably_subadditive[of c, unfolded o_def]
hoelzl@35582
   201
      assms sums_zero sums_summable by auto
hoelzl@35582
   202
hoelzl@35582
   203
  also have "\<dots> = 0"
hoelzl@35582
   204
    using assms sums_zero 
hoelzl@35582
   205
      sums_unique[of "\<lambda> i. prob (c i)" "0"] by auto
hoelzl@35582
   206
hoelzl@35582
   207
  finally show "prob (\<Union> i. c i) = 0"
hoelzl@35582
   208
    using leq0 by auto
hoelzl@35582
   209
qed
hoelzl@35582
   210
hoelzl@35582
   211
lemma indep_sym:
hoelzl@35582
   212
   "indep a b \<Longrightarrow> indep b a"
hoelzl@35582
   213
unfolding indep_def using Int_commute[of a b] by auto
hoelzl@35582
   214
hoelzl@35582
   215
lemma indep_refl:
hoelzl@35582
   216
  assumes "a \<in> events"
hoelzl@35582
   217
  shows "indep a a = (prob a = 0) \<or> (prob a = 1)"
hoelzl@35582
   218
using assms unfolding indep_def by auto
hoelzl@35582
   219
hoelzl@35582
   220
lemma prob_equiprobable_finite_unions:
hoelzl@35582
   221
  assumes "s \<in> events" 
hoelzl@35582
   222
  assumes "\<And>x. x \<in> s \<Longrightarrow> {x} \<in> events"
hoelzl@35582
   223
  assumes "finite s"
hoelzl@35582
   224
  assumes "\<And> x y. \<lbrakk>x \<in> s; y \<in> s\<rbrakk> \<Longrightarrow> (prob {x} = prob {y})"
hoelzl@35582
   225
  shows "prob s = of_nat (card s) * prob {SOME x. x \<in> s}"
hoelzl@35582
   226
using assms
hoelzl@35582
   227
proof (cases "s = {}")
hoelzl@35582
   228
  case True thus ?thesis by simp
hoelzl@35582
   229
next
hoelzl@35582
   230
  case False hence " \<exists> x. x \<in> s" by blast
hoelzl@35582
   231
  from someI_ex[OF this] assms
hoelzl@35582
   232
  have prob_some: "\<And> x. x \<in> s \<Longrightarrow> prob {x} = prob {SOME y. y \<in> s}" by blast
hoelzl@35582
   233
  have "prob s = (\<Sum> x \<in> s. prob {x})"
hoelzl@35582
   234
    using assms measure_real_sum_image by blast
hoelzl@35582
   235
  also have "\<dots> = (\<Sum> x \<in> s. prob {SOME y. y \<in> s})" using prob_some by auto
hoelzl@35582
   236
  also have "\<dots> = of_nat (card s) * prob {(SOME x. x \<in> s)}"
hoelzl@35582
   237
    using setsum_constant assms by auto
hoelzl@35582
   238
  finally show ?thesis by simp
hoelzl@35582
   239
qed
hoelzl@35582
   240
hoelzl@35582
   241
lemma prob_real_sum_image_fn:
hoelzl@35582
   242
  assumes "e \<in> events"
hoelzl@35582
   243
  assumes "\<And> x. x \<in> s \<Longrightarrow> e \<inter> f x \<in> events"
hoelzl@35582
   244
  assumes "finite s"
hoelzl@35582
   245
  assumes "\<And> x y. \<lbrakk>x \<in> s ; y \<in> s ; x \<noteq> y\<rbrakk> \<Longrightarrow> f x \<inter> f y = {}"
hoelzl@35582
   246
  assumes "space M \<subseteq> (\<Union> i \<in> s. f i)"
hoelzl@35582
   247
  shows "prob e = (\<Sum> x \<in> s. prob (e \<inter> f x))"
hoelzl@35582
   248
using assms
hoelzl@35582
   249
proof -
hoelzl@35582
   250
  let ?S = "{0 ..< card s}"
hoelzl@35582
   251
  obtain g where "g ` ?S = s \<and> inj_on g ?S"
hoelzl@35582
   252
    using ex_bij_betw_nat_finite[unfolded bij_betw_def, of s] assms by auto
hoelzl@35582
   253
  moreover hence gs: "g ` ?S = s" by simp
hoelzl@35582
   254
  ultimately have ginj: "inj_on g ?S" by simp
hoelzl@35582
   255
  let ?f' = "\<lambda> i. e \<inter> f (g i)"
hoelzl@35582
   256
  have f': "?f' \<in> ?S \<rightarrow> events"
hoelzl@35582
   257
    using gs assms by blast
hoelzl@35582
   258
  hence "\<And> i j. \<lbrakk>i \<in> ?S ; j \<in> ?S ; i \<noteq> j\<rbrakk> 
hoelzl@35582
   259
    \<Longrightarrow> ?f' i \<inter> ?f' j = {}" using assms ginj[unfolded inj_on_def] gs f' by blast
hoelzl@35582
   260
  hence df': "\<And> i j. \<lbrakk>i < card s ; j < card s ; i \<noteq> j\<rbrakk> 
hoelzl@35582
   261
    \<Longrightarrow> ?f' i \<inter> ?f' j = {}" by simp
hoelzl@35582
   262
hoelzl@35582
   263
  have "e = e \<inter> space M" using assms sets_into_space by simp
hoelzl@35582
   264
  also hence "\<dots> = e \<inter> (\<Union> x \<in> s. f x)" using assms by blast
hoelzl@35582
   265
  also have "\<dots> = (\<Union> x \<in> g ` ?S. e \<inter> f x)" using gs by simp
hoelzl@35582
   266
  also have "\<dots> = (\<Union> i \<in> ?S. ?f' i)" by simp
hoelzl@35582
   267
  finally have "prob e = prob (\<Union> i \<in> ?S. ?f' i)" by simp
hoelzl@35582
   268
  also have "\<dots> = (\<Sum> i \<in> ?S. prob (?f' i))"
hoelzl@35582
   269
    apply (subst measure_finitely_additive'')
hoelzl@35582
   270
    using f' df' assms by (auto simp: disjoint_family_on_def)
hoelzl@35582
   271
  also have "\<dots> = (\<Sum> x \<in> g ` ?S. prob (e \<inter> f x))" 
hoelzl@35582
   272
    using setsum_reindex[of g "?S" "\<lambda> x. prob (e \<inter> f x)"]
hoelzl@35582
   273
      ginj by simp
hoelzl@35582
   274
  also have "\<dots> = (\<Sum> x \<in> s. prob (e \<inter> f x))" using gs by simp
hoelzl@35582
   275
  finally show ?thesis by simp
hoelzl@35582
   276
qed
hoelzl@35582
   277
hoelzl@35582
   278
lemma distribution_prob_space:
hoelzl@35582
   279
  assumes "random_variable s X"
hoelzl@35582
   280
  shows "prob_space \<lparr>space = space s, sets = sets s, measure = distribution X\<rparr>"
hoelzl@35582
   281
using assms
hoelzl@35582
   282
proof -
hoelzl@35582
   283
  let ?N = "\<lparr>space = space s, sets = sets s, measure = distribution X\<rparr>"
hoelzl@35582
   284
  interpret s: sigma_algebra "s" using assms[unfolded measurable_def] by auto
hoelzl@35582
   285
  hence sigN: "sigma_algebra ?N" using s.sigma_algebra_extend by auto
hoelzl@35582
   286
hoelzl@35582
   287
  have pos: "\<And> e. e \<in> sets s \<Longrightarrow> distribution X e \<ge> 0"
hoelzl@35582
   288
    unfolding distribution_def
hoelzl@35929
   289
    using positive'[unfolded positive_def]
hoelzl@35582
   290
    assms[unfolded measurable_def] by auto
hoelzl@35582
   291
hoelzl@35582
   292
  have cas: "countably_additive ?N (distribution X)"
hoelzl@35582
   293
  proof -
hoelzl@35582
   294
    {
hoelzl@35582
   295
      fix f :: "nat \<Rightarrow> 'c \<Rightarrow> bool"
hoelzl@35582
   296
      let ?g = "\<lambda> n. X -` f n \<inter> space M"
hoelzl@35582
   297
      assume asm: "range f \<subseteq> sets s" "UNION UNIV f \<in> sets s" "disjoint_family f"
hoelzl@35582
   298
      hence "range ?g \<subseteq> events" 
hoelzl@35582
   299
        using assms unfolding measurable_def by blast
hoelzl@35582
   300
      from ca[unfolded countably_additive_def, 
hoelzl@35582
   301
        rule_format, of ?g, OF this] countable_UN[OF this] asm
hoelzl@35582
   302
      have "(\<lambda> n. prob (?g n)) sums prob (UNION UNIV ?g)"
hoelzl@35582
   303
        unfolding disjoint_family_on_def by blast
hoelzl@35582
   304
      moreover have "(X -` (\<Union> n. f n)) = (\<Union> n. X -` f n)" by blast
hoelzl@35582
   305
      ultimately have "(\<lambda> n. distribution X (f n)) sums distribution X (UNION UNIV f)"
hoelzl@35582
   306
        unfolding distribution_def by simp
hoelzl@35582
   307
    } thus ?thesis unfolding countably_additive_def by simp
hoelzl@35582
   308
  qed
hoelzl@35582
   309
hoelzl@35582
   310
  have ds0: "distribution X {} = 0"
hoelzl@35582
   311
    unfolding distribution_def by simp
hoelzl@35582
   312
hoelzl@35582
   313
  have "X -` space s \<inter> space M = space M"
hoelzl@35582
   314
    using assms[unfolded measurable_def] by auto
hoelzl@35582
   315
  hence ds1: "distribution X (space s) = 1"
hoelzl@35582
   316
    unfolding measurable_def distribution_def using prob_space by simp
hoelzl@35582
   317
hoelzl@35582
   318
  from ds0 ds1 cas pos sigN
hoelzl@35582
   319
  show "prob_space ?N"
hoelzl@35582
   320
    unfolding prob_space_def prob_space_axioms_def
hoelzl@35582
   321
    measure_space_def measure_space_axioms_def by simp
hoelzl@35582
   322
qed
hoelzl@35582
   323
hoelzl@35582
   324
lemma distribution_lebesgue_thm1:
hoelzl@35582
   325
  assumes "random_variable s X"
hoelzl@35582
   326
  assumes "A \<in> sets s"
hoelzl@35582
   327
  shows "distribution X A = expectation (indicator_fn (X -` A \<inter> space M))"
hoelzl@35582
   328
unfolding distribution_def
hoelzl@35582
   329
using assms unfolding measurable_def
hoelzl@35582
   330
using integral_indicator_fn by auto
hoelzl@35582
   331
hoelzl@35582
   332
lemma distribution_lebesgue_thm2:
hoelzl@35582
   333
  assumes "random_variable s X" "A \<in> sets s"
hoelzl@35582
   334
  shows "distribution X A = measure_space.integral \<lparr>space = space s, sets = sets s, measure = distribution X\<rparr> (indicator_fn A)"
hoelzl@35582
   335
  (is "_ = measure_space.integral ?M _")
hoelzl@35582
   336
proof -
hoelzl@35582
   337
  interpret S: prob_space ?M using assms(1) by (rule distribution_prob_space)
hoelzl@35582
   338
hoelzl@35582
   339
  show ?thesis
hoelzl@35582
   340
    using S.integral_indicator_fn(1)
hoelzl@35582
   341
    using assms unfolding distribution_def by auto
hoelzl@35582
   342
qed
hoelzl@35582
   343
hoelzl@35582
   344
lemma finite_expectation1:
hoelzl@35582
   345
  assumes "finite (space M)" "random_variable borel_space X"
hoelzl@35582
   346
  shows "expectation X = (\<Sum> r \<in> X ` space M. r * prob (X -` {r} \<inter> space M))"
hoelzl@35582
   347
  using assms integral_finite measurable_def
hoelzl@35582
   348
  unfolding borel_measurable_def by auto
hoelzl@35582
   349
hoelzl@35582
   350
lemma finite_expectation:
hoelzl@35582
   351
  assumes "finite (space M) \<and> random_variable borel_space X"
hoelzl@35582
   352
  shows "expectation X = (\<Sum> r \<in> X ` (space M). r * distribution X {r})"
hoelzl@35582
   353
using assms unfolding distribution_def using finite_expectation1 by auto
hoelzl@35582
   354
lemma prob_x_eq_1_imp_prob_y_eq_0:
hoelzl@35582
   355
  assumes "{x} \<in> events"
hoelzl@35582
   356
  assumes "(prob {x} = 1)"
hoelzl@35582
   357
  assumes "{y} \<in> events"
hoelzl@35582
   358
  assumes "y \<noteq> x"
hoelzl@35582
   359
  shows "prob {y} = 0"
hoelzl@35582
   360
  using prob_one_inter[of "{y}" "{x}"] assms by auto
hoelzl@35582
   361
hoelzl@35582
   362
lemma distribution_x_eq_1_imp_distribution_y_eq_0:
hoelzl@35582
   363
  assumes X: "random_variable \<lparr>space = X ` (space M), sets = Pow (X ` (space M))\<rparr> X"
hoelzl@35582
   364
  assumes "(distribution X {x} = 1)"
hoelzl@35582
   365
  assumes "y \<noteq> x"
hoelzl@35582
   366
  shows "distribution X {y} = 0"
hoelzl@35582
   367
proof -
hoelzl@35582
   368
  let ?S = "\<lparr>space = X ` (space M), sets = Pow (X ` (space M))\<rparr>"
hoelzl@35582
   369
  let ?M = "\<lparr>space = X ` (space M), sets = Pow (X ` (space M)), measure = distribution X\<rparr>"
hoelzl@35582
   370
  interpret S: prob_space ?M
hoelzl@35582
   371
    using distribution_prob_space[OF X] by auto
hoelzl@35582
   372
  { assume "{x} \<notin> sets ?M"
hoelzl@35582
   373
    hence "x \<notin> X ` space M" by auto
hoelzl@35582
   374
    hence "X -` {x} \<inter> space M = {}" by auto
hoelzl@35582
   375
    hence "distribution X {x} = 0" unfolding distribution_def by auto
hoelzl@35582
   376
    hence "False" using assms by auto }
hoelzl@35582
   377
  hence x: "{x} \<in> sets ?M" by auto
hoelzl@35582
   378
  { assume "{y} \<notin> sets ?M"
hoelzl@35582
   379
    hence "y \<notin> X ` space M" by auto
hoelzl@35582
   380
    hence "X -` {y} \<inter> space M = {}" by auto
hoelzl@35582
   381
    hence "distribution X {y} = 0" unfolding distribution_def by auto }
hoelzl@35582
   382
  moreover
hoelzl@35582
   383
  { assume "{y} \<in> sets ?M"
hoelzl@35582
   384
    hence "distribution X {y} = 0" using assms S.prob_x_eq_1_imp_prob_y_eq_0[OF x] by auto }
hoelzl@35582
   385
  ultimately show ?thesis by auto
hoelzl@35582
   386
qed
hoelzl@35582
   387
hoelzl@35977
   388
hoelzl@35582
   389
end
hoelzl@35582
   390
hoelzl@35977
   391
locale finite_prob_space = prob_space + finite_measure_space
hoelzl@35977
   392
hoelzl@36624
   393
lemma finite_prob_space_eq:
hoelzl@36624
   394
  "finite_prob_space M \<longleftrightarrow> finite_measure_space M \<and> measure M (space M) = 1"
hoelzl@36624
   395
  unfolding finite_prob_space_def finite_measure_space_def prob_space_def prob_space_axioms_def
hoelzl@36624
   396
  by auto
hoelzl@36624
   397
hoelzl@36624
   398
lemma (in prob_space) not_empty: "space M \<noteq> {}"
hoelzl@36624
   399
  using prob_space empty_measure by auto
hoelzl@36624
   400
hoelzl@36624
   401
lemma (in finite_prob_space) sum_over_space_eq_1: "(\<Sum>x\<in>space M. measure M {x}) = 1"
hoelzl@36624
   402
  using prob_space sum_over_space by simp
hoelzl@36624
   403
hoelzl@36624
   404
lemma (in finite_prob_space) positive_distribution: "0 \<le> distribution X x"
hoelzl@36624
   405
  unfolding distribution_def using positive sets_eq_Pow by simp
hoelzl@36624
   406
hoelzl@36624
   407
lemma (in finite_prob_space) joint_distribution_restriction_fst:
hoelzl@36624
   408
  "joint_distribution X Y A \<le> distribution X (fst ` A)"
hoelzl@36624
   409
  unfolding distribution_def
hoelzl@36624
   410
proof (safe intro!: measure_mono)
hoelzl@36624
   411
  fix x assume "x \<in> space M" and *: "(X x, Y x) \<in> A"
hoelzl@36624
   412
  show "x \<in> X -` fst ` A"
hoelzl@36624
   413
    by (auto intro!: image_eqI[OF _ *])
hoelzl@36624
   414
qed (simp_all add: sets_eq_Pow)
hoelzl@36624
   415
hoelzl@36624
   416
lemma (in finite_prob_space) joint_distribution_restriction_snd:
hoelzl@36624
   417
  "joint_distribution X Y A \<le> distribution Y (snd ` A)"
hoelzl@36624
   418
  unfolding distribution_def
hoelzl@36624
   419
proof (safe intro!: measure_mono)
hoelzl@36624
   420
  fix x assume "x \<in> space M" and *: "(X x, Y x) \<in> A"
hoelzl@36624
   421
  show "x \<in> Y -` snd ` A"
hoelzl@36624
   422
    by (auto intro!: image_eqI[OF _ *])
hoelzl@36624
   423
qed (simp_all add: sets_eq_Pow)
hoelzl@36624
   424
hoelzl@36624
   425
lemma (in finite_prob_space) distribution_order:
hoelzl@36624
   426
  shows "0 \<le> distribution X x'"
hoelzl@36624
   427
  and "(distribution X x' \<noteq> 0) \<longleftrightarrow> (0 < distribution X x')"
hoelzl@36624
   428
  and "r \<le> joint_distribution X Y {(x, y)} \<Longrightarrow> r \<le> distribution X {x}"
hoelzl@36624
   429
  and "r \<le> joint_distribution X Y {(x, y)} \<Longrightarrow> r \<le> distribution Y {y}"
hoelzl@36624
   430
  and "r < joint_distribution X Y {(x, y)} \<Longrightarrow> r < distribution X {x}"
hoelzl@36624
   431
  and "r < joint_distribution X Y {(x, y)} \<Longrightarrow> r < distribution Y {y}"
hoelzl@36624
   432
  and "distribution X {x} = 0 \<Longrightarrow> joint_distribution X Y {(x, y)} = 0"
hoelzl@36624
   433
  and "distribution Y {y} = 0 \<Longrightarrow> joint_distribution X Y {(x, y)} = 0"
hoelzl@36624
   434
  using positive_distribution[of X x']
hoelzl@36624
   435
    positive_distribution[of "\<lambda>x. (X x, Y x)" "{(x, y)}"]
hoelzl@36624
   436
    joint_distribution_restriction_fst[of X Y "{(x, y)}"]
hoelzl@36624
   437
    joint_distribution_restriction_snd[of X Y "{(x, y)}"]
hoelzl@36624
   438
  by auto
hoelzl@36624
   439
hoelzl@36624
   440
lemma (in finite_prob_space) finite_product_measure_space:
hoelzl@35977
   441
  assumes "finite s1" "finite s2"
hoelzl@35977
   442
  shows "finite_measure_space \<lparr> space = s1 \<times> s2, sets = Pow (s1 \<times> s2), measure = joint_distribution X Y\<rparr>"
hoelzl@35977
   443
    (is "finite_measure_space ?M")
hoelzl@35977
   444
proof (rule finite_Pow_additivity_sufficient)
hoelzl@35977
   445
  show "positive ?M (measure ?M)"
hoelzl@35977
   446
    unfolding positive_def using positive'[unfolded positive_def] assms sets_eq_Pow
hoelzl@36624
   447
    by (simp add: distribution_def)
hoelzl@35977
   448
hoelzl@35977
   449
  show "additive ?M (measure ?M)" unfolding additive_def
hoelzl@35977
   450
  proof safe
hoelzl@35977
   451
    fix x y
hoelzl@35977
   452
    have A: "((\<lambda>x. (X x, Y x)) -` x) \<inter> space M \<in> sets M" using assms sets_eq_Pow by auto
hoelzl@35977
   453
    have B: "((\<lambda>x. (X x, Y x)) -` y) \<inter> space M \<in> sets M" using assms sets_eq_Pow by auto
hoelzl@35977
   454
    assume "x \<inter> y = {}"
hoelzl@35977
   455
    from additive[unfolded additive_def, rule_format, OF A B] this
hoelzl@35977
   456
    show "measure ?M (x \<union> y) = measure ?M x + measure ?M y"
hoelzl@36624
   457
      apply (simp add: distribution_def)
hoelzl@35977
   458
      apply (subst Int_Un_distrib2)
hoelzl@35977
   459
      by auto
hoelzl@35977
   460
  qed
hoelzl@35977
   461
hoelzl@35977
   462
  show "finite (space ?M)"
hoelzl@35977
   463
    using assms by auto
hoelzl@35977
   464
hoelzl@35977
   465
  show "sets ?M = Pow (space ?M)"
hoelzl@35977
   466
    by simp
hoelzl@35977
   467
qed
hoelzl@35977
   468
hoelzl@36624
   469
lemma (in finite_prob_space) finite_product_measure_space_of_images:
hoelzl@35977
   470
  shows "finite_measure_space \<lparr> space = X ` space M \<times> Y ` space M,
hoelzl@35977
   471
                                sets = Pow (X ` space M \<times> Y ` space M),
hoelzl@35977
   472
                                measure = joint_distribution X Y\<rparr>"
hoelzl@35977
   473
    (is "finite_measure_space ?M")
hoelzl@36624
   474
  using finite_space by (auto intro!: finite_product_measure_space)
hoelzl@36624
   475
hoelzl@36624
   476
lemma (in finite_prob_space) finite_measure_space:
hoelzl@36624
   477
  shows "finite_measure_space \<lparr> space = X ` space M, sets = Pow (X ` space M), measure = distribution X\<rparr>"
hoelzl@36624
   478
    (is "finite_measure_space ?S")
hoelzl@36624
   479
proof (rule finite_Pow_additivity_sufficient, simp_all)
hoelzl@36624
   480
  show "finite (X ` space M)" using finite_space by simp
hoelzl@36624
   481
hoelzl@36624
   482
  show "positive ?S (distribution X)" unfolding distribution_def
hoelzl@36624
   483
    unfolding positive_def using positive'[unfolded positive_def] sets_eq_Pow by auto
hoelzl@36624
   484
hoelzl@36624
   485
  show "additive ?S (distribution X)" unfolding additive_def distribution_def
hoelzl@36624
   486
  proof (simp, safe)
hoelzl@36624
   487
    fix x y
hoelzl@36624
   488
    have x: "(X -` x) \<inter> space M \<in> sets M"
hoelzl@36624
   489
      and y: "(X -` y) \<inter> space M \<in> sets M" using sets_eq_Pow by auto
hoelzl@36624
   490
    assume "x \<inter> y = {}"
hoelzl@36624
   491
    from additive[unfolded additive_def, rule_format, OF x y] this
hoelzl@36624
   492
    have "prob (((X -` x) \<union> (X -` y)) \<inter> space M) =
hoelzl@36624
   493
      prob ((X -` x) \<inter> space M) + prob ((X -` y) \<inter> space M)"
hoelzl@36624
   494
      apply (subst Int_Un_distrib2)
hoelzl@36624
   495
      by auto
hoelzl@36624
   496
    thus "prob ((X -` x \<union> X -` y) \<inter> space M) = prob (X -` x \<inter> space M) + prob (X -` y \<inter> space M)"
hoelzl@36624
   497
      by auto
hoelzl@36624
   498
  qed
hoelzl@36624
   499
qed
hoelzl@36624
   500
hoelzl@36624
   501
lemma (in finite_prob_space) finite_prob_space_of_images:
hoelzl@36624
   502
  "finite_prob_space \<lparr> space = X ` space M, sets = Pow (X ` space M), measure = distribution X\<rparr>"
hoelzl@36624
   503
  (is "finite_prob_space ?S")
hoelzl@36624
   504
proof (simp add: finite_prob_space_eq, safe)
hoelzl@36624
   505
  show "finite_measure_space ?S" by (rule finite_measure_space)
hoelzl@36624
   506
  have "X -` X ` space M \<inter> space M = space M" by auto
hoelzl@36624
   507
  thus "distribution X (X`space M) = 1"
hoelzl@36624
   508
    by (simp add: distribution_def prob_space)
hoelzl@36624
   509
qed
hoelzl@36624
   510
hoelzl@36624
   511
lemma (in finite_prob_space) finite_product_prob_space_of_images:
hoelzl@36624
   512
  "finite_prob_space \<lparr> space = X ` space M \<times> Y ` space M, sets = Pow (X ` space M \<times> Y ` space M), 
hoelzl@36624
   513
    measure = joint_distribution X Y\<rparr>"
hoelzl@36624
   514
  (is "finite_prob_space ?S")
hoelzl@36624
   515
proof (simp add: finite_prob_space_eq, safe)
hoelzl@36624
   516
  show "finite_measure_space ?S" by (rule finite_product_measure_space_of_images)
hoelzl@36624
   517
hoelzl@36624
   518
  have "X -` X ` space M \<inter> Y -` Y ` space M \<inter> space M = space M" by auto
hoelzl@36624
   519
  thus "joint_distribution X Y (X ` space M \<times> Y ` space M) = 1"
hoelzl@36624
   520
    by (simp add: distribution_def prob_space vimage_Times comp_def)
hoelzl@36624
   521
qed
hoelzl@35977
   522
hoelzl@35582
   523
end