src/HOL/Probability/Probability_Space.thy
author hoelzl
Wed Dec 01 19:20:30 2010 +0100 (2010-12-01)
changeset 40859 de0b30e6c2d2
parent 39302 d7728f65b353
child 41023 9118eb4eb8dc
permissions -rw-r--r--
Support product spaces on sigma finite measures.
Introduce the almost everywhere quantifier.
Introduce 'morphism' theorems for most constants.
Prove uniqueness of measures on cut stable generators.
Prove uniqueness of the Radon-Nikodym derivative.
Removed misleading suffix from borel_space and lebesgue_space.
Use product spaces to introduce Fubini on the Lebesgue integral.
Combine Euclidean_Lebesgue and Lebesgue_Measure.
Generalize theorems about mutual information and entropy to arbitrary probability spaces.
Remove simproc mult_log as it does not work with interpretations.
Introduce completion of measure spaces.
Change type of sigma.
Introduce dynkin systems.
hoelzl@35582
     1
theory Probability_Space
hoelzl@40859
     2
imports Lebesgue_Integration Radon_Nikodym Product_Measure
hoelzl@35582
     3
begin
hoelzl@35582
     4
hoelzl@40859
     5
lemma real_of_pinfreal_inverse[simp]:
hoelzl@40859
     6
  fixes X :: pinfreal
hoelzl@40859
     7
  shows "real (inverse X) = 1 / real X"
hoelzl@40859
     8
  by (cases X) (auto simp: inverse_eq_divide)
hoelzl@40859
     9
hoelzl@40859
    10
lemma real_of_pinfreal_le_0[simp]: "real (X :: pinfreal) \<le> 0 \<longleftrightarrow> (X = 0 \<or> X = \<omega>)"
hoelzl@40859
    11
  by (cases X) auto
hoelzl@40859
    12
hoelzl@40859
    13
lemma real_of_pinfreal_less_0[simp]: "\<not> (real (X :: pinfreal) < 0)"
hoelzl@40859
    14
  by (cases X) auto
hoelzl@40859
    15
hoelzl@35582
    16
locale prob_space = measure_space +
hoelzl@38656
    17
  assumes measure_space_1: "\<mu> (space M) = 1"
hoelzl@38656
    18
hoelzl@40859
    19
lemma abs_real_of_pinfreal[simp]: "\<bar>real (X :: pinfreal)\<bar> = real X"
hoelzl@40859
    20
  by simp
hoelzl@40859
    21
hoelzl@40859
    22
lemma zero_less_real_of_pinfreal: "0 < real (X :: pinfreal) \<longleftrightarrow> X \<noteq> 0 \<and> X \<noteq> \<omega>"
hoelzl@40859
    23
  by (cases X) auto
hoelzl@40859
    24
hoelzl@38656
    25
sublocale prob_space < finite_measure
hoelzl@38656
    26
proof
hoelzl@38656
    27
  from measure_space_1 show "\<mu> (space M) \<noteq> \<omega>" by simp
hoelzl@38656
    28
qed
hoelzl@38656
    29
hoelzl@40859
    30
abbreviation (in prob_space) "events \<equiv> sets M"
hoelzl@40859
    31
abbreviation (in prob_space) "prob \<equiv> \<lambda>A. real (\<mu> A)"
hoelzl@40859
    32
abbreviation (in prob_space) "prob_preserving \<equiv> measure_preserving"
hoelzl@40859
    33
abbreviation (in prob_space) "random_variable M' X \<equiv> sigma_algebra M' \<and> X \<in> measurable M M'"
hoelzl@40859
    34
abbreviation (in prob_space) "expectation \<equiv> integral"
hoelzl@35582
    35
hoelzl@40859
    36
definition (in prob_space)
hoelzl@35582
    37
  "indep A B \<longleftrightarrow> A \<in> events \<and> B \<in> events \<and> prob (A \<inter> B) = prob A * prob B"
hoelzl@35582
    38
hoelzl@40859
    39
definition (in prob_space)
hoelzl@35582
    40
  "indep_families F G \<longleftrightarrow> (\<forall> A \<in> F. \<forall> B \<in> G. indep A B)"
hoelzl@35582
    41
hoelzl@40859
    42
definition (in prob_space)
hoelzl@38656
    43
  "distribution X = (\<lambda>s. \<mu> ((X -` s) \<inter> (space M)))"
hoelzl@35582
    44
hoelzl@40859
    45
abbreviation (in prob_space)
hoelzl@36624
    46
  "joint_distribution X Y \<equiv> distribution (\<lambda>x. (X x, Y x))"
hoelzl@35582
    47
hoelzl@39097
    48
lemma (in prob_space) distribution_cong:
hoelzl@39097
    49
  assumes "\<And>x. x \<in> space M \<Longrightarrow> X x = Y x"
hoelzl@39097
    50
  shows "distribution X = distribution Y"
nipkow@39302
    51
  unfolding distribution_def fun_eq_iff
hoelzl@39097
    52
  using assms by (auto intro!: arg_cong[where f="\<mu>"])
hoelzl@39097
    53
hoelzl@39097
    54
lemma (in prob_space) joint_distribution_cong:
hoelzl@39097
    55
  assumes "\<And>x. x \<in> space M \<Longrightarrow> X x = X' x"
hoelzl@39097
    56
  assumes "\<And>x. x \<in> space M \<Longrightarrow> Y x = Y' x"
hoelzl@39097
    57
  shows "joint_distribution X Y = joint_distribution X' Y'"
nipkow@39302
    58
  unfolding distribution_def fun_eq_iff
hoelzl@39097
    59
  using assms by (auto intro!: arg_cong[where f="\<mu>"])
hoelzl@39097
    60
hoelzl@40859
    61
lemma (in prob_space) distribution_id[simp]:
hoelzl@40859
    62
  assumes "N \<in> sets M" shows "distribution (\<lambda>x. x) N = \<mu> N"
hoelzl@40859
    63
  using assms by (auto simp: distribution_def intro!: arg_cong[where f=\<mu>])
hoelzl@40859
    64
hoelzl@40859
    65
lemma (in prob_space) prob_space: "prob (space M) = 1"
hoelzl@38656
    66
  unfolding measure_space_1 by simp
hoelzl@35582
    67
hoelzl@40859
    68
lemma (in prob_space) measure_le_1[simp, intro]:
hoelzl@38656
    69
  assumes "A \<in> events" shows "\<mu> A \<le> 1"
hoelzl@38656
    70
proof -
hoelzl@38656
    71
  have "\<mu> A \<le> \<mu> (space M)"
hoelzl@38656
    72
    using assms sets_into_space by(auto intro!: measure_mono)
hoelzl@38656
    73
  also note measure_space_1
hoelzl@38656
    74
  finally show ?thesis .
hoelzl@38656
    75
qed
hoelzl@35582
    76
hoelzl@40859
    77
lemma (in prob_space) prob_compl:
hoelzl@38656
    78
  assumes "A \<in> events"
hoelzl@38656
    79
  shows "prob (space M - A) = 1 - prob A"
hoelzl@38656
    80
  using `A \<in> events`[THEN sets_into_space] `A \<in> events` measure_space_1
hoelzl@38656
    81
  by (subst real_finite_measure_Diff) auto
hoelzl@35582
    82
hoelzl@40859
    83
lemma (in prob_space) indep_space:
hoelzl@35582
    84
  assumes "s \<in> events"
hoelzl@35582
    85
  shows "indep (space M) s"
hoelzl@38656
    86
  using assms prob_space by (simp add: indep_def)
hoelzl@35582
    87
hoelzl@40859
    88
lemma (in prob_space) prob_space_increasing: "increasing M prob"
hoelzl@38656
    89
  by (auto intro!: real_measure_mono simp: increasing_def)
hoelzl@35582
    90
hoelzl@40859
    91
lemma (in prob_space) prob_zero_union:
hoelzl@35582
    92
  assumes "s \<in> events" "t \<in> events" "prob t = 0"
hoelzl@35582
    93
  shows "prob (s \<union> t) = prob s"
hoelzl@38656
    94
using assms
hoelzl@35582
    95
proof -
hoelzl@35582
    96
  have "prob (s \<union> t) \<le> prob s"
hoelzl@38656
    97
    using real_finite_measure_subadditive[of s t] assms by auto
hoelzl@35582
    98
  moreover have "prob (s \<union> t) \<ge> prob s"
hoelzl@38656
    99
    using assms by (blast intro: real_measure_mono)
hoelzl@35582
   100
  ultimately show ?thesis by simp
hoelzl@35582
   101
qed
hoelzl@35582
   102
hoelzl@40859
   103
lemma (in prob_space) prob_eq_compl:
hoelzl@35582
   104
  assumes "s \<in> events" "t \<in> events"
hoelzl@35582
   105
  assumes "prob (space M - s) = prob (space M - t)"
hoelzl@35582
   106
  shows "prob s = prob t"
hoelzl@38656
   107
  using assms prob_compl by auto
hoelzl@35582
   108
hoelzl@40859
   109
lemma (in prob_space) prob_one_inter:
hoelzl@35582
   110
  assumes events:"s \<in> events" "t \<in> events"
hoelzl@35582
   111
  assumes "prob t = 1"
hoelzl@35582
   112
  shows "prob (s \<inter> t) = prob s"
hoelzl@35582
   113
proof -
hoelzl@38656
   114
  have "prob ((space M - s) \<union> (space M - t)) = prob (space M - s)"
hoelzl@38656
   115
    using events assms  prob_compl[of "t"] by (auto intro!: prob_zero_union)
hoelzl@38656
   116
  also have "(space M - s) \<union> (space M - t) = space M - (s \<inter> t)"
hoelzl@38656
   117
    by blast
hoelzl@38656
   118
  finally show "prob (s \<inter> t) = prob s"
hoelzl@38656
   119
    using events by (auto intro!: prob_eq_compl[of "s \<inter> t" s])
hoelzl@35582
   120
qed
hoelzl@35582
   121
hoelzl@40859
   122
lemma (in prob_space) prob_eq_bigunion_image:
hoelzl@35582
   123
  assumes "range f \<subseteq> events" "range g \<subseteq> events"
hoelzl@35582
   124
  assumes "disjoint_family f" "disjoint_family g"
hoelzl@35582
   125
  assumes "\<And> n :: nat. prob (f n) = prob (g n)"
hoelzl@35582
   126
  shows "(prob (\<Union> i. f i) = prob (\<Union> i. g i))"
hoelzl@35582
   127
using assms
hoelzl@35582
   128
proof -
hoelzl@38656
   129
  have a: "(\<lambda> i. prob (f i)) sums (prob (\<Union> i. f i))"
hoelzl@38656
   130
    by (rule real_finite_measure_UNION[OF assms(1,3)])
hoelzl@38656
   131
  have b: "(\<lambda> i. prob (g i)) sums (prob (\<Union> i. g i))"
hoelzl@38656
   132
    by (rule real_finite_measure_UNION[OF assms(2,4)])
hoelzl@38656
   133
  show ?thesis using sums_unique[OF b] sums_unique[OF a] assms by simp
hoelzl@35582
   134
qed
hoelzl@35582
   135
hoelzl@40859
   136
lemma (in prob_space) prob_countably_zero:
hoelzl@35582
   137
  assumes "range c \<subseteq> events"
hoelzl@35582
   138
  assumes "\<And> i. prob (c i) = 0"
hoelzl@38656
   139
  shows "prob (\<Union> i :: nat. c i) = 0"
hoelzl@38656
   140
proof (rule antisym)
hoelzl@38656
   141
  show "prob (\<Union> i :: nat. c i) \<le> 0"
hoelzl@40859
   142
    using real_finite_measure_countably_subadditive[OF assms(1)]
hoelzl@38656
   143
    by (simp add: assms(2) suminf_zero summable_zero)
hoelzl@38656
   144
  show "0 \<le> prob (\<Union> i :: nat. c i)" by (rule real_pinfreal_nonneg)
hoelzl@35582
   145
qed
hoelzl@35582
   146
hoelzl@40859
   147
lemma (in prob_space) indep_sym:
hoelzl@35582
   148
   "indep a b \<Longrightarrow> indep b a"
hoelzl@35582
   149
unfolding indep_def using Int_commute[of a b] by auto
hoelzl@35582
   150
hoelzl@40859
   151
lemma (in prob_space) indep_refl:
hoelzl@35582
   152
  assumes "a \<in> events"
hoelzl@35582
   153
  shows "indep a a = (prob a = 0) \<or> (prob a = 1)"
hoelzl@35582
   154
using assms unfolding indep_def by auto
hoelzl@35582
   155
hoelzl@40859
   156
lemma (in prob_space) prob_equiprobable_finite_unions:
hoelzl@38656
   157
  assumes "s \<in> events"
hoelzl@38656
   158
  assumes s_finite: "finite s" "\<And>x. x \<in> s \<Longrightarrow> {x} \<in> events"
hoelzl@35582
   159
  assumes "\<And> x y. \<lbrakk>x \<in> s; y \<in> s\<rbrakk> \<Longrightarrow> (prob {x} = prob {y})"
hoelzl@38656
   160
  shows "prob s = real (card s) * prob {SOME x. x \<in> s}"
hoelzl@35582
   161
proof (cases "s = {}")
hoelzl@38656
   162
  case False hence "\<exists> x. x \<in> s" by blast
hoelzl@35582
   163
  from someI_ex[OF this] assms
hoelzl@35582
   164
  have prob_some: "\<And> x. x \<in> s \<Longrightarrow> prob {x} = prob {SOME y. y \<in> s}" by blast
hoelzl@35582
   165
  have "prob s = (\<Sum> x \<in> s. prob {x})"
hoelzl@38656
   166
    using real_finite_measure_finite_singelton[OF s_finite] by simp
hoelzl@35582
   167
  also have "\<dots> = (\<Sum> x \<in> s. prob {SOME y. y \<in> s})" using prob_some by auto
hoelzl@38656
   168
  also have "\<dots> = real (card s) * prob {(SOME x. x \<in> s)}"
hoelzl@38656
   169
    using setsum_constant assms by (simp add: real_eq_of_nat)
hoelzl@35582
   170
  finally show ?thesis by simp
hoelzl@38656
   171
qed simp
hoelzl@35582
   172
hoelzl@40859
   173
lemma (in prob_space) prob_real_sum_image_fn:
hoelzl@35582
   174
  assumes "e \<in> events"
hoelzl@35582
   175
  assumes "\<And> x. x \<in> s \<Longrightarrow> e \<inter> f x \<in> events"
hoelzl@35582
   176
  assumes "finite s"
hoelzl@38656
   177
  assumes disjoint: "\<And> x y. \<lbrakk>x \<in> s ; y \<in> s ; x \<noteq> y\<rbrakk> \<Longrightarrow> f x \<inter> f y = {}"
hoelzl@38656
   178
  assumes upper: "space M \<subseteq> (\<Union> i \<in> s. f i)"
hoelzl@35582
   179
  shows "prob e = (\<Sum> x \<in> s. prob (e \<inter> f x))"
hoelzl@35582
   180
proof -
hoelzl@38656
   181
  have e: "e = (\<Union> i \<in> s. e \<inter> f i)"
hoelzl@38656
   182
    using `e \<in> events` sets_into_space upper by blast
hoelzl@38656
   183
  hence "prob e = prob (\<Union> i \<in> s. e \<inter> f i)" by simp
hoelzl@38656
   184
  also have "\<dots> = (\<Sum> x \<in> s. prob (e \<inter> f x))"
hoelzl@38656
   185
  proof (rule real_finite_measure_finite_Union)
hoelzl@38656
   186
    show "finite s" by fact
hoelzl@38656
   187
    show "\<And>i. i \<in> s \<Longrightarrow> e \<inter> f i \<in> events" by fact
hoelzl@38656
   188
    show "disjoint_family_on (\<lambda>i. e \<inter> f i) s"
hoelzl@38656
   189
      using disjoint by (auto simp: disjoint_family_on_def)
hoelzl@38656
   190
  qed
hoelzl@38656
   191
  finally show ?thesis .
hoelzl@35582
   192
qed
hoelzl@35582
   193
hoelzl@40859
   194
lemma (in prob_space) distribution_prob_space:
hoelzl@40859
   195
  assumes "random_variable S X"
hoelzl@38656
   196
  shows "prob_space S (distribution X)"
hoelzl@35582
   197
proof -
hoelzl@39089
   198
  interpret S: measure_space S "distribution X"
hoelzl@40859
   199
    using measure_space_vimage[of X S] assms unfolding distribution_def by simp
hoelzl@38656
   200
  show ?thesis
hoelzl@38656
   201
  proof
hoelzl@38656
   202
    have "X -` space S \<inter> space M = space M"
hoelzl@38656
   203
      using `random_variable S X` by (auto simp: measurable_def)
hoelzl@39089
   204
    then show "distribution X (space S) = 1"
hoelzl@39089
   205
      using measure_space_1 by (simp add: distribution_def)
hoelzl@35582
   206
  qed
hoelzl@35582
   207
qed
hoelzl@35582
   208
hoelzl@40859
   209
lemma (in prob_space) AE_distribution:
hoelzl@40859
   210
  assumes X: "random_variable MX X" and "measure_space.almost_everywhere MX (distribution X) (\<lambda>x. Q x)"
hoelzl@40859
   211
  shows "AE x. Q (X x)"
hoelzl@40859
   212
proof -
hoelzl@40859
   213
  interpret X: prob_space MX "distribution X" using X by (rule distribution_prob_space)
hoelzl@40859
   214
  obtain N where N: "N \<in> sets MX" "distribution X N = 0" "{x\<in>space MX. \<not> Q x} \<subseteq> N"
hoelzl@40859
   215
    using assms unfolding X.almost_everywhere_def by auto
hoelzl@40859
   216
  show "AE x. Q (X x)"
hoelzl@40859
   217
    using X[unfolded measurable_def] N unfolding distribution_def
hoelzl@40859
   218
    by (intro AE_I'[where N="X -` N \<inter> space M"]) auto
hoelzl@40859
   219
qed
hoelzl@40859
   220
hoelzl@40859
   221
lemma (in prob_space) distribution_lebesgue_thm1:
hoelzl@35582
   222
  assumes "random_variable s X"
hoelzl@35582
   223
  assumes "A \<in> sets s"
hoelzl@38656
   224
  shows "real (distribution X A) = expectation (indicator (X -` A \<inter> space M))"
hoelzl@35582
   225
unfolding distribution_def
hoelzl@35582
   226
using assms unfolding measurable_def
hoelzl@38656
   227
using integral_indicator by auto
hoelzl@35582
   228
hoelzl@40859
   229
lemma (in prob_space) distribution_lebesgue_thm2:
hoelzl@40859
   230
  assumes "random_variable S X" and "A \<in> sets S"
hoelzl@38656
   231
  shows "distribution X A =
hoelzl@38656
   232
    measure_space.positive_integral S (distribution X) (indicator A)"
hoelzl@38656
   233
  (is "_ = measure_space.positive_integral _ ?D _")
hoelzl@35582
   234
proof -
hoelzl@40859
   235
  interpret S: prob_space S "distribution X" using assms(1) by (rule distribution_prob_space)
hoelzl@35582
   236
hoelzl@35582
   237
  show ?thesis
hoelzl@38656
   238
    using S.positive_integral_indicator(1)
hoelzl@35582
   239
    using assms unfolding distribution_def by auto
hoelzl@35582
   240
qed
hoelzl@35582
   241
hoelzl@40859
   242
lemma (in prob_space) finite_expectation1:
hoelzl@40859
   243
  assumes f: "finite (X`space M)" and rv: "random_variable borel X"
hoelzl@35582
   244
  shows "expectation X = (\<Sum> r \<in> X ` space M. r * prob (X -` {r} \<inter> space M))"
hoelzl@40859
   245
proof (rule integral_on_finite(2)[OF rv[THEN conjunct2] f])
hoelzl@38656
   246
  fix x have "X -` {x} \<inter> space M \<in> sets M"
hoelzl@38656
   247
    using rv unfolding measurable_def by auto
hoelzl@38656
   248
  thus "\<mu> (X -` {x} \<inter> space M) \<noteq> \<omega>" using finite_measure by simp
hoelzl@38656
   249
qed
hoelzl@35582
   250
hoelzl@40859
   251
lemma (in prob_space) finite_expectation:
hoelzl@40859
   252
  assumes "finite (space M)" "random_variable borel X"
hoelzl@38656
   253
  shows "expectation X = (\<Sum> r \<in> X ` (space M). r * real (distribution X {r}))"
hoelzl@38656
   254
  using assms unfolding distribution_def using finite_expectation1 by auto
hoelzl@38656
   255
hoelzl@40859
   256
lemma (in prob_space) prob_x_eq_1_imp_prob_y_eq_0:
hoelzl@35582
   257
  assumes "{x} \<in> events"
hoelzl@38656
   258
  assumes "prob {x} = 1"
hoelzl@35582
   259
  assumes "{y} \<in> events"
hoelzl@35582
   260
  assumes "y \<noteq> x"
hoelzl@35582
   261
  shows "prob {y} = 0"
hoelzl@35582
   262
  using prob_one_inter[of "{y}" "{x}"] assms by auto
hoelzl@35582
   263
hoelzl@40859
   264
lemma (in prob_space) distribution_empty[simp]: "distribution X {} = 0"
hoelzl@38656
   265
  unfolding distribution_def by simp
hoelzl@38656
   266
hoelzl@40859
   267
lemma (in prob_space) distribution_space[simp]: "distribution X (X ` space M) = 1"
hoelzl@38656
   268
proof -
hoelzl@38656
   269
  have "X -` X ` space M \<inter> space M = space M" by auto
hoelzl@38656
   270
  thus ?thesis unfolding distribution_def by (simp add: measure_space_1)
hoelzl@38656
   271
qed
hoelzl@38656
   272
hoelzl@40859
   273
lemma (in prob_space) distribution_one:
hoelzl@40859
   274
  assumes "random_variable M' X" and "A \<in> sets M'"
hoelzl@38656
   275
  shows "distribution X A \<le> 1"
hoelzl@38656
   276
proof -
hoelzl@38656
   277
  have "distribution X A \<le> \<mu> (space M)" unfolding distribution_def
hoelzl@38656
   278
    using assms[unfolded measurable_def] by (auto intro!: measure_mono)
hoelzl@38656
   279
  thus ?thesis by (simp add: measure_space_1)
hoelzl@38656
   280
qed
hoelzl@38656
   281
hoelzl@40859
   282
lemma (in prob_space) distribution_finite:
hoelzl@40859
   283
  assumes "random_variable M' X" and "A \<in> sets M'"
hoelzl@38656
   284
  shows "distribution X A \<noteq> \<omega>"
hoelzl@38656
   285
  using distribution_one[OF assms] by auto
hoelzl@38656
   286
hoelzl@40859
   287
lemma (in prob_space) distribution_x_eq_1_imp_distribution_y_eq_0:
hoelzl@35582
   288
  assumes X: "random_variable \<lparr>space = X ` (space M), sets = Pow (X ` (space M))\<rparr> X"
hoelzl@38656
   289
    (is "random_variable ?S X")
hoelzl@38656
   290
  assumes "distribution X {x} = 1"
hoelzl@35582
   291
  assumes "y \<noteq> x"
hoelzl@35582
   292
  shows "distribution X {y} = 0"
hoelzl@35582
   293
proof -
hoelzl@40859
   294
  from distribution_prob_space[OF X]
hoelzl@38656
   295
  interpret S: prob_space ?S "distribution X" by simp
hoelzl@38656
   296
  have x: "{x} \<in> sets ?S"
hoelzl@38656
   297
  proof (rule ccontr)
hoelzl@38656
   298
    assume "{x} \<notin> sets ?S"
hoelzl@35582
   299
    hence "X -` {x} \<inter> space M = {}" by auto
hoelzl@38656
   300
    thus "False" using assms unfolding distribution_def by auto
hoelzl@38656
   301
  qed
hoelzl@38656
   302
  have [simp]: "{y} \<inter> {x} = {}" "{x} - {y} = {x}" using `y \<noteq> x` by auto
hoelzl@38656
   303
  show ?thesis
hoelzl@38656
   304
  proof cases
hoelzl@38656
   305
    assume "{y} \<in> sets ?S"
hoelzl@38656
   306
    with `{x} \<in> sets ?S` assms show "distribution X {y} = 0"
hoelzl@38656
   307
      using S.measure_inter_full_set[of "{y}" "{x}"]
hoelzl@38656
   308
      by simp
hoelzl@38656
   309
  next
hoelzl@38656
   310
    assume "{y} \<notin> sets ?S"
hoelzl@35582
   311
    hence "X -` {y} \<inter> space M = {}" by auto
hoelzl@38656
   312
    thus "distribution X {y} = 0" unfolding distribution_def by auto
hoelzl@38656
   313
  qed
hoelzl@35582
   314
qed
hoelzl@35582
   315
hoelzl@40859
   316
lemma (in prob_space) joint_distribution_Times_le_fst:
hoelzl@40859
   317
  assumes X: "random_variable MX X" and Y: "random_variable MY Y"
hoelzl@40859
   318
    and A: "A \<in> sets MX" and B: "B \<in> sets MY"
hoelzl@40859
   319
  shows "joint_distribution X Y (A \<times> B) \<le> distribution X A"
hoelzl@40859
   320
  unfolding distribution_def
hoelzl@40859
   321
proof (intro measure_mono)
hoelzl@40859
   322
  show "(\<lambda>x. (X x, Y x)) -` (A \<times> B) \<inter> space M \<subseteq> X -` A \<inter> space M" by force
hoelzl@40859
   323
  show "X -` A \<inter> space M \<in> events"
hoelzl@40859
   324
    using X A unfolding measurable_def by simp
hoelzl@40859
   325
  have *: "(\<lambda>x. (X x, Y x)) -` (A \<times> B) \<inter> space M =
hoelzl@40859
   326
    (X -` A \<inter> space M) \<inter> (Y -` B \<inter> space M)" by auto
hoelzl@40859
   327
  show "(\<lambda>x. (X x, Y x)) -` (A \<times> B) \<inter> space M \<in> events"
hoelzl@40859
   328
    unfolding * apply (rule Int)
hoelzl@40859
   329
    using assms unfolding measurable_def by auto
hoelzl@40859
   330
qed
hoelzl@40859
   331
hoelzl@40859
   332
lemma (in prob_space) joint_distribution_commute:
hoelzl@40859
   333
  "joint_distribution X Y x = joint_distribution Y X ((\<lambda>(x,y). (y,x))`x)"
hoelzl@40859
   334
  unfolding distribution_def by (auto intro!: arg_cong[where f=\<mu>])
hoelzl@40859
   335
hoelzl@40859
   336
lemma (in prob_space) joint_distribution_Times_le_snd:
hoelzl@40859
   337
  assumes X: "random_variable MX X" and Y: "random_variable MY Y"
hoelzl@40859
   338
    and A: "A \<in> sets MX" and B: "B \<in> sets MY"
hoelzl@40859
   339
  shows "joint_distribution X Y (A \<times> B) \<le> distribution Y B"
hoelzl@40859
   340
  using assms
hoelzl@40859
   341
  by (subst joint_distribution_commute)
hoelzl@40859
   342
     (simp add: swap_product joint_distribution_Times_le_fst)
hoelzl@40859
   343
hoelzl@40859
   344
lemma (in prob_space) random_variable_pairI:
hoelzl@40859
   345
  assumes "random_variable MX X"
hoelzl@40859
   346
  assumes "random_variable MY Y"
hoelzl@40859
   347
  shows "random_variable (sigma (pair_algebra MX MY)) (\<lambda>x. (X x, Y x))"
hoelzl@40859
   348
proof
hoelzl@40859
   349
  interpret MX: sigma_algebra MX using assms by simp
hoelzl@40859
   350
  interpret MY: sigma_algebra MY using assms by simp
hoelzl@40859
   351
  interpret P: pair_sigma_algebra MX MY by default
hoelzl@40859
   352
  show "sigma_algebra (sigma (pair_algebra MX MY))" by default
hoelzl@40859
   353
  have sa: "sigma_algebra M" by default
hoelzl@40859
   354
  show "(\<lambda>x. (X x, Y x)) \<in> measurable M (sigma (pair_algebra MX MY))"
hoelzl@40859
   355
    unfolding P.measurable_pair[OF sa] using assms by (simp add: comp_def)
hoelzl@40859
   356
qed
hoelzl@40859
   357
hoelzl@40859
   358
lemma (in prob_space) distribution_order:
hoelzl@40859
   359
  assumes "random_variable MX X" "random_variable MY Y"
hoelzl@40859
   360
  assumes "{x} \<in> sets MX" "{y} \<in> sets MY"
hoelzl@40859
   361
  shows "r \<le> joint_distribution X Y {(x, y)} \<Longrightarrow> r \<le> distribution X {x}"
hoelzl@40859
   362
    and "r \<le> joint_distribution X Y {(x, y)} \<Longrightarrow> r \<le> distribution Y {y}"
hoelzl@40859
   363
    and "r < joint_distribution X Y {(x, y)} \<Longrightarrow> r < distribution X {x}"
hoelzl@40859
   364
    and "r < joint_distribution X Y {(x, y)} \<Longrightarrow> r < distribution Y {y}"
hoelzl@40859
   365
    and "distribution X {x} = 0 \<Longrightarrow> joint_distribution X Y {(x, y)} = 0"
hoelzl@40859
   366
    and "distribution Y {y} = 0 \<Longrightarrow> joint_distribution X Y {(x, y)} = 0"
hoelzl@40859
   367
  using joint_distribution_Times_le_snd[OF assms]
hoelzl@40859
   368
  using joint_distribution_Times_le_fst[OF assms]
hoelzl@40859
   369
  by auto
hoelzl@40859
   370
hoelzl@40859
   371
lemma (in prob_space) joint_distribution_commute_singleton:
hoelzl@40859
   372
  "joint_distribution X Y {(x, y)} = joint_distribution Y X {(y, x)}"
hoelzl@40859
   373
  unfolding distribution_def by (auto intro!: arg_cong[where f=\<mu>])
hoelzl@40859
   374
hoelzl@40859
   375
lemma (in prob_space) joint_distribution_assoc_singleton:
hoelzl@40859
   376
  "joint_distribution X (\<lambda>x. (Y x, Z x)) {(x, y, z)} =
hoelzl@40859
   377
   joint_distribution (\<lambda>x. (X x, Y x)) Z {((x, y), z)}"
hoelzl@40859
   378
  unfolding distribution_def by (auto intro!: arg_cong[where f=\<mu>])
hoelzl@40859
   379
hoelzl@40859
   380
locale pair_prob_space = M1: prob_space M1 p1 + M2: prob_space M2 p2 for M1 p1 M2 p2
hoelzl@40859
   381
hoelzl@40859
   382
sublocale pair_prob_space \<subseteq> pair_sigma_finite M1 p1 M2 p2 by default
hoelzl@40859
   383
hoelzl@40859
   384
sublocale pair_prob_space \<subseteq> P: prob_space P pair_measure
hoelzl@40859
   385
proof
hoelzl@40859
   386
  show "pair_measure (space P) = 1"
hoelzl@40859
   387
    by (simp add: pair_algebra_def pair_measure_times M1.measure_space_1 M2.measure_space_1)
hoelzl@40859
   388
qed
hoelzl@40859
   389
hoelzl@40859
   390
lemma countably_additiveI[case_names countably]:
hoelzl@40859
   391
  assumes "\<And>A. \<lbrakk> range A \<subseteq> sets M ; disjoint_family A ; (\<Union>i. A i) \<in> sets M\<rbrakk> \<Longrightarrow>
hoelzl@40859
   392
    (\<Sum>\<^isub>\<infinity>n. \<mu> (A n)) = \<mu> (\<Union>i. A i)"
hoelzl@40859
   393
  shows "countably_additive M \<mu>"
hoelzl@40859
   394
  using assms unfolding countably_additive_def by auto
hoelzl@40859
   395
hoelzl@40859
   396
lemma (in prob_space) joint_distribution_prob_space:
hoelzl@40859
   397
  assumes "random_variable MX X" "random_variable MY Y"
hoelzl@40859
   398
  shows "prob_space (sigma (pair_algebra MX MY)) (joint_distribution X Y)"
hoelzl@40859
   399
proof -
hoelzl@40859
   400
  interpret X: prob_space MX "distribution X" by (intro distribution_prob_space assms)
hoelzl@40859
   401
  interpret Y: prob_space MY "distribution Y" by (intro distribution_prob_space assms)
hoelzl@40859
   402
  interpret XY: pair_sigma_finite MX "distribution X" MY "distribution Y" by default
hoelzl@40859
   403
  show ?thesis
hoelzl@40859
   404
  proof
hoelzl@40859
   405
    let "?X A" = "(\<lambda>x. (X x, Y x)) -` A \<inter> space M"
hoelzl@40859
   406
    show "joint_distribution X Y {} = 0" by (simp add: distribution_def)
hoelzl@40859
   407
    show "countably_additive XY.P (joint_distribution X Y)"
hoelzl@40859
   408
    proof (rule countably_additiveI)
hoelzl@40859
   409
      fix A :: "nat \<Rightarrow> ('b \<times> 'c) set"
hoelzl@40859
   410
      assume A: "range A \<subseteq> sets XY.P" and df: "disjoint_family A"
hoelzl@40859
   411
      have "(\<Sum>\<^isub>\<infinity>n. \<mu> (?X (A n))) = \<mu> (\<Union>x. ?X (A x))"
hoelzl@40859
   412
      proof (intro measure_countably_additive)
hoelzl@40859
   413
        from assms have *: "(\<lambda>x. (X x, Y x)) \<in> measurable M XY.P"
hoelzl@40859
   414
          by (intro XY.measurable_prod_sigma) (simp_all add: comp_def, default)
hoelzl@40859
   415
        show "range (\<lambda>n. ?X (A n)) \<subseteq> events"
hoelzl@40859
   416
          using measurable_sets[OF *] A by auto
hoelzl@40859
   417
        show "disjoint_family (\<lambda>n. ?X (A n))"
hoelzl@40859
   418
          by (intro disjoint_family_on_bisimulation[OF df]) auto
hoelzl@40859
   419
      qed
hoelzl@40859
   420
      then show "(\<Sum>\<^isub>\<infinity>n. joint_distribution X Y (A n)) = joint_distribution X Y (\<Union>i. A i)"
hoelzl@40859
   421
        by (simp add: distribution_def vimage_UN)
hoelzl@40859
   422
    qed
hoelzl@40859
   423
    have "?X (space MX \<times> space MY) = space M"
hoelzl@40859
   424
      using assms by (auto simp: measurable_def)
hoelzl@40859
   425
    then show "joint_distribution X Y (space XY.P) = 1"
hoelzl@40859
   426
      by (simp add: space_pair_algebra distribution_def measure_space_1)
hoelzl@40859
   427
  qed
hoelzl@40859
   428
qed
hoelzl@40859
   429
hoelzl@40859
   430
section "Probability spaces on finite sets"
hoelzl@35582
   431
hoelzl@35977
   432
locale finite_prob_space = prob_space + finite_measure_space
hoelzl@35977
   433
hoelzl@40859
   434
abbreviation (in prob_space) "finite_random_variable M' X \<equiv> finite_sigma_algebra M' \<and> X \<in> measurable M M'"
hoelzl@40859
   435
hoelzl@40859
   436
lemma (in prob_space) finite_random_variableD:
hoelzl@40859
   437
  assumes "finite_random_variable M' X" shows "random_variable M' X"
hoelzl@40859
   438
proof -
hoelzl@40859
   439
  interpret M': finite_sigma_algebra M' using assms by simp
hoelzl@40859
   440
  then show "random_variable M' X" using assms by simp default
hoelzl@40859
   441
qed
hoelzl@40859
   442
hoelzl@40859
   443
lemma (in prob_space) distribution_finite_prob_space:
hoelzl@40859
   444
  assumes "finite_random_variable MX X"
hoelzl@40859
   445
  shows "finite_prob_space MX (distribution X)"
hoelzl@40859
   446
proof -
hoelzl@40859
   447
  interpret X: prob_space MX "distribution X"
hoelzl@40859
   448
    using assms[THEN finite_random_variableD] by (rule distribution_prob_space)
hoelzl@40859
   449
  interpret MX: finite_sigma_algebra MX
hoelzl@40859
   450
    using assms by simp
hoelzl@40859
   451
  show ?thesis
hoelzl@40859
   452
  proof
hoelzl@40859
   453
    fix x assume "x \<in> space MX"
hoelzl@40859
   454
    then have "X -` {x} \<inter> space M \<in> sets M"
hoelzl@40859
   455
      using assms unfolding measurable_def by simp
hoelzl@40859
   456
    then show "distribution X {x} \<noteq> \<omega>"
hoelzl@40859
   457
      unfolding distribution_def by simp
hoelzl@40859
   458
  qed
hoelzl@40859
   459
qed
hoelzl@40859
   460
hoelzl@40859
   461
lemma (in prob_space) simple_function_imp_finite_random_variable[simp, intro]:
hoelzl@40859
   462
  assumes "simple_function X"
hoelzl@40859
   463
  shows "finite_random_variable \<lparr> space = X`space M, sets = Pow (X`space M) \<rparr> X"
hoelzl@40859
   464
proof (intro conjI)
hoelzl@40859
   465
  have [simp]: "finite (X ` space M)" using assms unfolding simple_function_def by simp
hoelzl@40859
   466
  interpret X: sigma_algebra "\<lparr>space = X ` space M, sets = Pow (X ` space M)\<rparr>"
hoelzl@40859
   467
    by (rule sigma_algebra_Pow)
hoelzl@40859
   468
  show "finite_sigma_algebra \<lparr>space = X ` space M, sets = Pow (X ` space M)\<rparr>"
hoelzl@40859
   469
    by default auto
hoelzl@40859
   470
  show "X \<in> measurable M \<lparr>space = X ` space M, sets = Pow (X ` space M)\<rparr>"
hoelzl@40859
   471
  proof (unfold measurable_def, clarsimp)
hoelzl@40859
   472
    fix A assume A: "A \<subseteq> X`space M"
hoelzl@40859
   473
    then have "finite A" by (rule finite_subset) simp
hoelzl@40859
   474
    then have "X -` (\<Union>a\<in>A. {a}) \<inter> space M \<in> events"
hoelzl@40859
   475
      unfolding vimage_UN UN_extend_simps
hoelzl@40859
   476
      apply (rule finite_UN)
hoelzl@40859
   477
      using A assms unfolding simple_function_def by auto
hoelzl@40859
   478
    then show "X -` A \<inter> space M \<in> events" by simp
hoelzl@40859
   479
  qed
hoelzl@40859
   480
qed
hoelzl@40859
   481
hoelzl@40859
   482
lemma (in prob_space) simple_function_imp_random_variable[simp, intro]:
hoelzl@40859
   483
  assumes "simple_function X"
hoelzl@40859
   484
  shows "random_variable \<lparr> space = X`space M, sets = Pow (X`space M) \<rparr> X"
hoelzl@40859
   485
  using simple_function_imp_finite_random_variable[OF assms]
hoelzl@40859
   486
  by (auto dest!: finite_random_variableD)
hoelzl@40859
   487
hoelzl@40859
   488
lemma (in prob_space) sum_over_space_real_distribution:
hoelzl@40859
   489
  "simple_function X \<Longrightarrow> (\<Sum>x\<in>X`space M. real (distribution X {x})) = 1"
hoelzl@40859
   490
  unfolding distribution_def prob_space[symmetric]
hoelzl@40859
   491
  by (subst real_finite_measure_finite_Union[symmetric])
hoelzl@40859
   492
     (auto simp add: disjoint_family_on_def simple_function_def
hoelzl@40859
   493
           intro!: arg_cong[where f=prob])
hoelzl@40859
   494
hoelzl@40859
   495
lemma (in prob_space) finite_random_variable_pairI:
hoelzl@40859
   496
  assumes "finite_random_variable MX X"
hoelzl@40859
   497
  assumes "finite_random_variable MY Y"
hoelzl@40859
   498
  shows "finite_random_variable (sigma (pair_algebra MX MY)) (\<lambda>x. (X x, Y x))"
hoelzl@40859
   499
proof
hoelzl@40859
   500
  interpret MX: finite_sigma_algebra MX using assms by simp
hoelzl@40859
   501
  interpret MY: finite_sigma_algebra MY using assms by simp
hoelzl@40859
   502
  interpret P: pair_finite_sigma_algebra MX MY by default
hoelzl@40859
   503
  show "finite_sigma_algebra (sigma (pair_algebra MX MY))" by default
hoelzl@40859
   504
  have sa: "sigma_algebra M" by default
hoelzl@40859
   505
  show "(\<lambda>x. (X x, Y x)) \<in> measurable M (sigma (pair_algebra MX MY))"
hoelzl@40859
   506
    unfolding P.measurable_pair[OF sa] using assms by (simp add: comp_def)
hoelzl@40859
   507
qed
hoelzl@40859
   508
hoelzl@40859
   509
lemma (in prob_space) finite_random_variable_imp_sets:
hoelzl@40859
   510
  "finite_random_variable MX X \<Longrightarrow> x \<in> space MX \<Longrightarrow> {x} \<in> sets MX"
hoelzl@40859
   511
  unfolding finite_sigma_algebra_def finite_sigma_algebra_axioms_def by simp
hoelzl@40859
   512
hoelzl@40859
   513
lemma (in prob_space) finite_random_variable_vimage:
hoelzl@40859
   514
  assumes X: "finite_random_variable MX X" shows "X -` A \<inter> space M \<in> events"
hoelzl@40859
   515
proof -
hoelzl@40859
   516
  interpret X: finite_sigma_algebra MX using X by simp
hoelzl@40859
   517
  from X have vimage: "\<And>A. A \<subseteq> space MX \<Longrightarrow> X -` A \<inter> space M \<in> events" and
hoelzl@40859
   518
    "X \<in> space M \<rightarrow> space MX"
hoelzl@40859
   519
    by (auto simp: measurable_def)
hoelzl@40859
   520
  then have *: "X -` A \<inter> space M = X -` (A \<inter> space MX) \<inter> space M"
hoelzl@40859
   521
    by auto
hoelzl@40859
   522
  show "X -` A \<inter> space M \<in> events"
hoelzl@40859
   523
    unfolding * by (intro vimage) auto
hoelzl@40859
   524
qed
hoelzl@40859
   525
hoelzl@40859
   526
lemma (in prob_space) joint_distribution_finite_Times_le_fst:
hoelzl@40859
   527
  assumes X: "finite_random_variable MX X" and Y: "finite_random_variable MY Y"
hoelzl@40859
   528
  shows "joint_distribution X Y (A \<times> B) \<le> distribution X A"
hoelzl@40859
   529
  unfolding distribution_def
hoelzl@40859
   530
proof (intro measure_mono)
hoelzl@40859
   531
  show "(\<lambda>x. (X x, Y x)) -` (A \<times> B) \<inter> space M \<subseteq> X -` A \<inter> space M" by force
hoelzl@40859
   532
  show "X -` A \<inter> space M \<in> events"
hoelzl@40859
   533
    using finite_random_variable_vimage[OF X] .
hoelzl@40859
   534
  have *: "(\<lambda>x. (X x, Y x)) -` (A \<times> B) \<inter> space M =
hoelzl@40859
   535
    (X -` A \<inter> space M) \<inter> (Y -` B \<inter> space M)" by auto
hoelzl@40859
   536
  show "(\<lambda>x. (X x, Y x)) -` (A \<times> B) \<inter> space M \<in> events"
hoelzl@40859
   537
    unfolding * apply (rule Int)
hoelzl@40859
   538
    using assms[THEN finite_random_variable_vimage] by auto
hoelzl@40859
   539
qed
hoelzl@40859
   540
hoelzl@40859
   541
lemma (in prob_space) joint_distribution_finite_Times_le_snd:
hoelzl@40859
   542
  assumes X: "finite_random_variable MX X" and Y: "finite_random_variable MY Y"
hoelzl@40859
   543
  shows "joint_distribution X Y (A \<times> B) \<le> distribution Y B"
hoelzl@40859
   544
  using assms
hoelzl@40859
   545
  by (subst joint_distribution_commute)
hoelzl@40859
   546
     (simp add: swap_product joint_distribution_finite_Times_le_fst)
hoelzl@40859
   547
hoelzl@40859
   548
lemma (in prob_space) finite_distribution_order:
hoelzl@40859
   549
  assumes "finite_random_variable MX X" "finite_random_variable MY Y"
hoelzl@40859
   550
  shows "r \<le> joint_distribution X Y {(x, y)} \<Longrightarrow> r \<le> distribution X {x}"
hoelzl@40859
   551
    and "r \<le> joint_distribution X Y {(x, y)} \<Longrightarrow> r \<le> distribution Y {y}"
hoelzl@40859
   552
    and "r < joint_distribution X Y {(x, y)} \<Longrightarrow> r < distribution X {x}"
hoelzl@40859
   553
    and "r < joint_distribution X Y {(x, y)} \<Longrightarrow> r < distribution Y {y}"
hoelzl@40859
   554
    and "distribution X {x} = 0 \<Longrightarrow> joint_distribution X Y {(x, y)} = 0"
hoelzl@40859
   555
    and "distribution Y {y} = 0 \<Longrightarrow> joint_distribution X Y {(x, y)} = 0"
hoelzl@40859
   556
  using joint_distribution_finite_Times_le_snd[OF assms, of "{x}" "{y}"]
hoelzl@40859
   557
  using joint_distribution_finite_Times_le_fst[OF assms, of "{x}" "{y}"]
hoelzl@40859
   558
  by auto
hoelzl@40859
   559
hoelzl@40859
   560
lemma (in prob_space) finite_distribution_finite:
hoelzl@40859
   561
  assumes "finite_random_variable M' X"
hoelzl@40859
   562
  shows "distribution X {x} \<noteq> \<omega>"
hoelzl@40859
   563
proof -
hoelzl@40859
   564
  have "distribution X {x} \<le> \<mu> (space M)"
hoelzl@40859
   565
    unfolding distribution_def
hoelzl@40859
   566
    using finite_random_variable_vimage[OF assms]
hoelzl@40859
   567
    by (intro measure_mono) auto
hoelzl@40859
   568
  then show ?thesis
hoelzl@40859
   569
    by auto
hoelzl@40859
   570
qed
hoelzl@40859
   571
hoelzl@40859
   572
lemma (in prob_space) setsum_joint_distribution:
hoelzl@40859
   573
  assumes X: "finite_random_variable MX X"
hoelzl@40859
   574
  assumes Y: "random_variable MY Y" "B \<in> sets MY"
hoelzl@40859
   575
  shows "(\<Sum>a\<in>space MX. joint_distribution X Y ({a} \<times> B)) = distribution Y B"
hoelzl@40859
   576
  unfolding distribution_def
hoelzl@40859
   577
proof (subst measure_finitely_additive'')
hoelzl@40859
   578
  interpret MX: finite_sigma_algebra MX using X by auto
hoelzl@40859
   579
  show "finite (space MX)" using MX.finite_space .
hoelzl@40859
   580
  let "?d i" = "(\<lambda>x. (X x, Y x)) -` ({i} \<times> B) \<inter> space M"
hoelzl@40859
   581
  { fix i assume "i \<in> space MX"
hoelzl@40859
   582
    moreover have "?d i = (X -` {i} \<inter> space M) \<inter> (Y -` B \<inter> space M)" by auto
hoelzl@40859
   583
    ultimately show "?d i \<in> events"
hoelzl@40859
   584
      using measurable_sets[of X M MX] measurable_sets[of Y M MY B] X Y
hoelzl@40859
   585
      using MX.sets_eq_Pow by auto }
hoelzl@40859
   586
  show "disjoint_family_on ?d (space MX)" by (auto simp: disjoint_family_on_def)
hoelzl@40859
   587
  show "\<mu> (\<Union>i\<in>space MX. ?d i) = \<mu> (Y -` B \<inter> space M)"
hoelzl@40859
   588
    using X[unfolded measurable_def]
hoelzl@40859
   589
    by (auto intro!: arg_cong[where f=\<mu>])
hoelzl@40859
   590
qed
hoelzl@40859
   591
hoelzl@40859
   592
lemma (in prob_space) setsum_joint_distribution_singleton:
hoelzl@40859
   593
  assumes X: "finite_random_variable MX X"
hoelzl@40859
   594
  assumes Y: "finite_random_variable MY Y" "b \<in> space MY"
hoelzl@40859
   595
  shows "(\<Sum>a\<in>space MX. joint_distribution X Y {(a, b)}) = distribution Y {b}"
hoelzl@40859
   596
  using setsum_joint_distribution[OF X
hoelzl@40859
   597
    finite_random_variableD[OF Y(1)]
hoelzl@40859
   598
    finite_random_variable_imp_sets[OF Y]] by simp
hoelzl@40859
   599
hoelzl@40859
   600
lemma (in prob_space) setsum_real_joint_distribution:
hoelzl@40859
   601
  assumes X: "finite_random_variable MX X"
hoelzl@40859
   602
  assumes Y: "random_variable MY Y" "B \<in> sets MY"
hoelzl@40859
   603
  shows "(\<Sum>a\<in>space MX. real (joint_distribution X Y ({a} \<times> B))) = real (distribution Y B)"
hoelzl@40859
   604
proof -
hoelzl@40859
   605
  interpret MX: finite_sigma_algebra MX using X by auto
hoelzl@40859
   606
  show ?thesis
hoelzl@40859
   607
    unfolding setsum_joint_distribution[OF assms, symmetric]
hoelzl@40859
   608
    using distribution_finite[OF random_variable_pairI[OF finite_random_variableD[OF X] Y(1)]] Y(2)
hoelzl@40859
   609
    by (simp add: space_pair_algebra in_sigma pair_algebraI MX.sets_eq_Pow real_of_pinfreal_setsum)
hoelzl@40859
   610
qed
hoelzl@40859
   611
hoelzl@40859
   612
lemma (in prob_space) setsum_real_joint_distribution_singleton:
hoelzl@40859
   613
  assumes X: "finite_random_variable MX X"
hoelzl@40859
   614
  assumes Y: "finite_random_variable MY Y" "b \<in> space MY"
hoelzl@40859
   615
  shows "(\<Sum>a\<in>space MX. real (joint_distribution X Y {(a,b)})) = real (distribution Y {b})"
hoelzl@40859
   616
  using setsum_real_joint_distribution[OF X
hoelzl@40859
   617
    finite_random_variableD[OF Y(1)]
hoelzl@40859
   618
    finite_random_variable_imp_sets[OF Y]] by simp
hoelzl@40859
   619
hoelzl@40859
   620
locale pair_finite_prob_space = M1: finite_prob_space M1 p1 + M2: finite_prob_space M2 p2 for M1 p1 M2 p2
hoelzl@40859
   621
hoelzl@40859
   622
sublocale pair_finite_prob_space \<subseteq> pair_prob_space M1 p1 M2 p2 by default
hoelzl@40859
   623
sublocale pair_finite_prob_space \<subseteq> pair_finite_space M1 p1 M2 p2  by default
hoelzl@40859
   624
sublocale pair_finite_prob_space \<subseteq> finite_prob_space P pair_measure by default
hoelzl@40859
   625
hoelzl@40859
   626
lemma (in prob_space) joint_distribution_finite_prob_space:
hoelzl@40859
   627
  assumes X: "finite_random_variable MX X"
hoelzl@40859
   628
  assumes Y: "finite_random_variable MY Y"
hoelzl@40859
   629
  shows "finite_prob_space (sigma (pair_algebra MX MY)) (joint_distribution X Y)"
hoelzl@40859
   630
proof -
hoelzl@40859
   631
  interpret X: finite_prob_space MX "distribution X"
hoelzl@40859
   632
    using X by (rule distribution_finite_prob_space)
hoelzl@40859
   633
  interpret Y: finite_prob_space MY "distribution Y"
hoelzl@40859
   634
    using Y by (rule distribution_finite_prob_space)
hoelzl@40859
   635
  interpret P: prob_space "sigma (pair_algebra MX MY)" "joint_distribution X Y"
hoelzl@40859
   636
    using assms[THEN finite_random_variableD] by (rule joint_distribution_prob_space)
hoelzl@40859
   637
  interpret XY: pair_finite_prob_space MX "distribution X" MY "distribution Y"
hoelzl@40859
   638
    by default
hoelzl@40859
   639
  show ?thesis
hoelzl@40859
   640
  proof
hoelzl@40859
   641
    fix x assume "x \<in> space XY.P"
hoelzl@40859
   642
    moreover have "(\<lambda>x. (X x, Y x)) \<in> measurable M XY.P"
hoelzl@40859
   643
      using X Y by (subst XY.measurable_pair) (simp_all add: o_def, default)
hoelzl@40859
   644
    ultimately have "(\<lambda>x. (X x, Y x)) -` {x} \<inter> space M \<in> sets M"
hoelzl@40859
   645
      unfolding measurable_def by simp
hoelzl@40859
   646
    then show "joint_distribution X Y {x} \<noteq> \<omega>"
hoelzl@40859
   647
      unfolding distribution_def by simp
hoelzl@40859
   648
  qed
hoelzl@40859
   649
qed
hoelzl@40859
   650
hoelzl@36624
   651
lemma finite_prob_space_eq:
hoelzl@38656
   652
  "finite_prob_space M \<mu> \<longleftrightarrow> finite_measure_space M \<mu> \<and> \<mu> (space M) = 1"
hoelzl@36624
   653
  unfolding finite_prob_space_def finite_measure_space_def prob_space_def prob_space_axioms_def
hoelzl@36624
   654
  by auto
hoelzl@36624
   655
hoelzl@36624
   656
lemma (in prob_space) not_empty: "space M \<noteq> {}"
hoelzl@36624
   657
  using prob_space empty_measure by auto
hoelzl@36624
   658
hoelzl@38656
   659
lemma (in finite_prob_space) sum_over_space_eq_1: "(\<Sum>x\<in>space M. \<mu> {x}) = 1"
hoelzl@38656
   660
  using measure_space_1 sum_over_space by simp
hoelzl@36624
   661
hoelzl@36624
   662
lemma (in finite_prob_space) positive_distribution: "0 \<le> distribution X x"
hoelzl@38656
   663
  unfolding distribution_def by simp
hoelzl@36624
   664
hoelzl@36624
   665
lemma (in finite_prob_space) joint_distribution_restriction_fst:
hoelzl@36624
   666
  "joint_distribution X Y A \<le> distribution X (fst ` A)"
hoelzl@36624
   667
  unfolding distribution_def
hoelzl@36624
   668
proof (safe intro!: measure_mono)
hoelzl@36624
   669
  fix x assume "x \<in> space M" and *: "(X x, Y x) \<in> A"
hoelzl@36624
   670
  show "x \<in> X -` fst ` A"
hoelzl@36624
   671
    by (auto intro!: image_eqI[OF _ *])
hoelzl@36624
   672
qed (simp_all add: sets_eq_Pow)
hoelzl@36624
   673
hoelzl@36624
   674
lemma (in finite_prob_space) joint_distribution_restriction_snd:
hoelzl@36624
   675
  "joint_distribution X Y A \<le> distribution Y (snd ` A)"
hoelzl@36624
   676
  unfolding distribution_def
hoelzl@36624
   677
proof (safe intro!: measure_mono)
hoelzl@36624
   678
  fix x assume "x \<in> space M" and *: "(X x, Y x) \<in> A"
hoelzl@36624
   679
  show "x \<in> Y -` snd ` A"
hoelzl@36624
   680
    by (auto intro!: image_eqI[OF _ *])
hoelzl@36624
   681
qed (simp_all add: sets_eq_Pow)
hoelzl@36624
   682
hoelzl@36624
   683
lemma (in finite_prob_space) distribution_order:
hoelzl@36624
   684
  shows "0 \<le> distribution X x'"
hoelzl@36624
   685
  and "(distribution X x' \<noteq> 0) \<longleftrightarrow> (0 < distribution X x')"
hoelzl@36624
   686
  and "r \<le> joint_distribution X Y {(x, y)} \<Longrightarrow> r \<le> distribution X {x}"
hoelzl@36624
   687
  and "r \<le> joint_distribution X Y {(x, y)} \<Longrightarrow> r \<le> distribution Y {y}"
hoelzl@36624
   688
  and "r < joint_distribution X Y {(x, y)} \<Longrightarrow> r < distribution X {x}"
hoelzl@36624
   689
  and "r < joint_distribution X Y {(x, y)} \<Longrightarrow> r < distribution Y {y}"
hoelzl@36624
   690
  and "distribution X {x} = 0 \<Longrightarrow> joint_distribution X Y {(x, y)} = 0"
hoelzl@36624
   691
  and "distribution Y {y} = 0 \<Longrightarrow> joint_distribution X Y {(x, y)} = 0"
hoelzl@36624
   692
  using positive_distribution[of X x']
hoelzl@36624
   693
    positive_distribution[of "\<lambda>x. (X x, Y x)" "{(x, y)}"]
hoelzl@36624
   694
    joint_distribution_restriction_fst[of X Y "{(x, y)}"]
hoelzl@36624
   695
    joint_distribution_restriction_snd[of X Y "{(x, y)}"]
hoelzl@36624
   696
  by auto
hoelzl@36624
   697
hoelzl@39097
   698
lemma (in finite_prob_space) distribution_mono:
hoelzl@39097
   699
  assumes "\<And>t. \<lbrakk> t \<in> space M ; X t \<in> x \<rbrakk> \<Longrightarrow> Y t \<in> y"
hoelzl@39097
   700
  shows "distribution X x \<le> distribution Y y"
hoelzl@39097
   701
  unfolding distribution_def
hoelzl@39097
   702
  using assms by (auto simp: sets_eq_Pow intro!: measure_mono)
hoelzl@39097
   703
hoelzl@39097
   704
lemma (in finite_prob_space) distribution_mono_gt_0:
hoelzl@39097
   705
  assumes gt_0: "0 < distribution X x"
hoelzl@39097
   706
  assumes *: "\<And>t. \<lbrakk> t \<in> space M ; X t \<in> x \<rbrakk> \<Longrightarrow> Y t \<in> y"
hoelzl@39097
   707
  shows "0 < distribution Y y"
hoelzl@39097
   708
  by (rule less_le_trans[OF gt_0 distribution_mono]) (rule *)
hoelzl@39097
   709
hoelzl@39097
   710
lemma (in finite_prob_space) sum_over_space_distrib:
hoelzl@39097
   711
  "(\<Sum>x\<in>X`space M. distribution X {x}) = 1"
hoelzl@39097
   712
  unfolding distribution_def measure_space_1[symmetric] using finite_space
hoelzl@39097
   713
  by (subst measure_finitely_additive'')
hoelzl@39097
   714
     (auto simp add: disjoint_family_on_def sets_eq_Pow intro!: arg_cong[where f=\<mu>])
hoelzl@39097
   715
hoelzl@39097
   716
lemma (in finite_prob_space) sum_over_space_real_distribution:
hoelzl@39097
   717
  "(\<Sum>x\<in>X`space M. real (distribution X {x})) = 1"
hoelzl@39097
   718
  unfolding distribution_def prob_space[symmetric] using finite_space
hoelzl@39097
   719
  by (subst real_finite_measure_finite_Union[symmetric])
hoelzl@39097
   720
     (auto simp add: disjoint_family_on_def sets_eq_Pow intro!: arg_cong[where f=prob])
hoelzl@39097
   721
hoelzl@39097
   722
lemma (in finite_prob_space) finite_sum_over_space_eq_1:
hoelzl@39097
   723
  "(\<Sum>x\<in>space M. real (\<mu> {x})) = 1"
hoelzl@39097
   724
  using sum_over_space_eq_1 finite_measure by (simp add: real_of_pinfreal_setsum sets_eq_Pow)
hoelzl@39097
   725
hoelzl@39097
   726
lemma (in finite_prob_space) distribution_finite:
hoelzl@39097
   727
  "distribution X A \<noteq> \<omega>"
hoelzl@39097
   728
  using finite_measure[of "X -` A \<inter> space M"]
hoelzl@39097
   729
  unfolding distribution_def sets_eq_Pow by auto
hoelzl@39097
   730
hoelzl@39097
   731
lemma (in finite_prob_space) real_distribution_gt_0[simp]:
hoelzl@39097
   732
  "0 < real (distribution Y y) \<longleftrightarrow>  0 < distribution Y y"
hoelzl@39097
   733
  using assms by (auto intro!: real_pinfreal_pos distribution_finite)
hoelzl@39097
   734
hoelzl@39097
   735
lemma (in finite_prob_space) real_distribution_mult_pos_pos:
hoelzl@39097
   736
  assumes "0 < distribution Y y"
hoelzl@39097
   737
  and "0 < distribution X x"
hoelzl@39097
   738
  shows "0 < real (distribution Y y * distribution X x)"
hoelzl@39097
   739
  unfolding real_of_pinfreal_mult[symmetric]
hoelzl@39097
   740
  using assms by (auto intro!: mult_pos_pos)
hoelzl@39097
   741
hoelzl@39097
   742
lemma (in finite_prob_space) real_distribution_divide_pos_pos:
hoelzl@39097
   743
  assumes "0 < distribution Y y"
hoelzl@39097
   744
  and "0 < distribution X x"
hoelzl@39097
   745
  shows "0 < real (distribution Y y / distribution X x)"
hoelzl@39097
   746
  unfolding divide_pinfreal_def real_of_pinfreal_mult[symmetric]
hoelzl@39097
   747
  using assms distribution_finite[of X x] by (cases "distribution X x") (auto intro!: mult_pos_pos)
hoelzl@39097
   748
hoelzl@39097
   749
lemma (in finite_prob_space) real_distribution_mult_inverse_pos_pos:
hoelzl@39097
   750
  assumes "0 < distribution Y y"
hoelzl@39097
   751
  and "0 < distribution X x"
hoelzl@39097
   752
  shows "0 < real (distribution Y y * inverse (distribution X x))"
hoelzl@39097
   753
  unfolding divide_pinfreal_def real_of_pinfreal_mult[symmetric]
hoelzl@39097
   754
  using assms distribution_finite[of X x] by (cases "distribution X x") (auto intro!: mult_pos_pos)
hoelzl@39097
   755
hoelzl@39097
   756
lemma (in prob_space) distribution_remove_const:
hoelzl@39097
   757
  shows "joint_distribution X (\<lambda>x. ()) {(x, ())} = distribution X {x}"
hoelzl@39097
   758
  and "joint_distribution (\<lambda>x. ()) X {((), x)} = distribution X {x}"
hoelzl@39097
   759
  and "joint_distribution X (\<lambda>x. (Y x, ())) {(x, y, ())} = joint_distribution X Y {(x, y)}"
hoelzl@39097
   760
  and "joint_distribution X (\<lambda>x. ((), Y x)) {(x, (), y)} = joint_distribution X Y {(x, y)}"
hoelzl@39097
   761
  and "distribution (\<lambda>x. ()) {()} = 1"
hoelzl@39097
   762
  unfolding measure_space_1[symmetric]
hoelzl@39097
   763
  by (auto intro!: arg_cong[where f="\<mu>"] simp: distribution_def)
hoelzl@35977
   764
hoelzl@39097
   765
lemma (in finite_prob_space) setsum_distribution_gen:
hoelzl@39097
   766
  assumes "Z -` {c} \<inter> space M = (\<Union>x \<in> X`space M. Y -` {f x}) \<inter> space M"
hoelzl@39097
   767
  and "inj_on f (X`space M)"
hoelzl@39097
   768
  shows "(\<Sum>x \<in> X`space M. distribution Y {f x}) = distribution Z {c}"
hoelzl@39097
   769
  unfolding distribution_def assms
hoelzl@39097
   770
  using finite_space assms
hoelzl@39097
   771
  by (subst measure_finitely_additive'')
hoelzl@39097
   772
     (auto simp add: disjoint_family_on_def sets_eq_Pow inj_on_def
hoelzl@39097
   773
      intro!: arg_cong[where f=prob])
hoelzl@39097
   774
hoelzl@39097
   775
lemma (in finite_prob_space) setsum_distribution:
hoelzl@39097
   776
  "(\<Sum>x \<in> X`space M. joint_distribution X Y {(x, y)}) = distribution Y {y}"
hoelzl@39097
   777
  "(\<Sum>y \<in> Y`space M. joint_distribution X Y {(x, y)}) = distribution X {x}"
hoelzl@39097
   778
  "(\<Sum>x \<in> X`space M. joint_distribution X (\<lambda>x. (Y x, Z x)) {(x, y, z)}) = joint_distribution Y Z {(y, z)}"
hoelzl@39097
   779
  "(\<Sum>y \<in> Y`space M. joint_distribution X (\<lambda>x. (Y x, Z x)) {(x, y, z)}) = joint_distribution X Z {(x, z)}"
hoelzl@39097
   780
  "(\<Sum>z \<in> Z`space M. joint_distribution X (\<lambda>x. (Y x, Z x)) {(x, y, z)}) = joint_distribution X Y {(x, y)}"
hoelzl@39097
   781
  by (auto intro!: inj_onI setsum_distribution_gen)
hoelzl@39097
   782
hoelzl@39097
   783
lemma (in finite_prob_space) setsum_real_distribution_gen:
hoelzl@39097
   784
  assumes "Z -` {c} \<inter> space M = (\<Union>x \<in> X`space M. Y -` {f x}) \<inter> space M"
hoelzl@39097
   785
  and "inj_on f (X`space M)"
hoelzl@39097
   786
  shows "(\<Sum>x \<in> X`space M. real (distribution Y {f x})) = real (distribution Z {c})"
hoelzl@39097
   787
  unfolding distribution_def assms
hoelzl@39097
   788
  using finite_space assms
hoelzl@39097
   789
  by (subst real_finite_measure_finite_Union[symmetric])
hoelzl@39097
   790
     (auto simp add: disjoint_family_on_def sets_eq_Pow inj_on_def
hoelzl@39097
   791
        intro!: arg_cong[where f=prob])
hoelzl@39097
   792
hoelzl@39097
   793
lemma (in finite_prob_space) setsum_real_distribution:
hoelzl@39097
   794
  "(\<Sum>x \<in> X`space M. real (joint_distribution X Y {(x, y)})) = real (distribution Y {y})"
hoelzl@39097
   795
  "(\<Sum>y \<in> Y`space M. real (joint_distribution X Y {(x, y)})) = real (distribution X {x})"
hoelzl@39097
   796
  "(\<Sum>x \<in> X`space M. real (joint_distribution X (\<lambda>x. (Y x, Z x)) {(x, y, z)})) = real (joint_distribution Y Z {(y, z)})"
hoelzl@39097
   797
  "(\<Sum>y \<in> Y`space M. real (joint_distribution X (\<lambda>x. (Y x, Z x)) {(x, y, z)})) = real (joint_distribution X Z {(x, z)})"
hoelzl@39097
   798
  "(\<Sum>z \<in> Z`space M. real (joint_distribution X (\<lambda>x. (Y x, Z x)) {(x, y, z)})) = real (joint_distribution X Y {(x, y)})"
hoelzl@39097
   799
  by (auto intro!: inj_onI setsum_real_distribution_gen)
hoelzl@39097
   800
hoelzl@39097
   801
lemma (in finite_prob_space) real_distribution_order:
hoelzl@39097
   802
  shows "r \<le> real (joint_distribution X Y {(x, y)}) \<Longrightarrow> r \<le> real (distribution X {x})"
hoelzl@39097
   803
  and "r \<le> real (joint_distribution X Y {(x, y)}) \<Longrightarrow> r \<le> real (distribution Y {y})"
hoelzl@39097
   804
  and "r < real (joint_distribution X Y {(x, y)}) \<Longrightarrow> r < real (distribution X {x})"
hoelzl@39097
   805
  and "r < real (joint_distribution X Y {(x, y)}) \<Longrightarrow> r < real (distribution Y {y})"
hoelzl@39097
   806
  and "distribution X {x} = 0 \<Longrightarrow> real (joint_distribution X Y {(x, y)}) = 0"
hoelzl@39097
   807
  and "distribution Y {y} = 0 \<Longrightarrow> real (joint_distribution X Y {(x, y)}) = 0"
hoelzl@39097
   808
  using real_of_pinfreal_mono[OF distribution_finite joint_distribution_restriction_fst, of X Y "{(x, y)}"]
hoelzl@39097
   809
  using real_of_pinfreal_mono[OF distribution_finite joint_distribution_restriction_snd, of X Y "{(x, y)}"]
hoelzl@39097
   810
  using real_pinfreal_nonneg[of "joint_distribution X Y {(x, y)}"]
hoelzl@39097
   811
  by auto
hoelzl@39097
   812
hoelzl@39097
   813
lemma (in prob_space) joint_distribution_remove[simp]:
hoelzl@39097
   814
    "joint_distribution X X {(x, x)} = distribution X {x}"
hoelzl@39097
   815
  unfolding distribution_def by (auto intro!: arg_cong[where f="\<mu>"])
hoelzl@39097
   816
hoelzl@39097
   817
lemma (in finite_prob_space) distribution_1:
hoelzl@39097
   818
  "distribution X A \<le> 1"
hoelzl@39097
   819
  unfolding distribution_def measure_space_1[symmetric]
hoelzl@39097
   820
  by (auto intro!: measure_mono simp: sets_eq_Pow)
hoelzl@39097
   821
hoelzl@39097
   822
lemma (in finite_prob_space) real_distribution_1:
hoelzl@39097
   823
  "real (distribution X A) \<le> 1"
hoelzl@39097
   824
  unfolding real_pinfreal_1[symmetric]
hoelzl@39097
   825
  by (rule real_of_pinfreal_mono[OF _ distribution_1]) simp
hoelzl@39097
   826
hoelzl@39097
   827
lemma (in finite_prob_space) uniform_prob:
hoelzl@39097
   828
  assumes "x \<in> space M"
hoelzl@39097
   829
  assumes "\<And> x y. \<lbrakk>x \<in> space M ; y \<in> space M\<rbrakk> \<Longrightarrow> prob {x} = prob {y}"
hoelzl@39097
   830
  shows "prob {x} = 1 / real (card (space M))"
hoelzl@39097
   831
proof -
hoelzl@39097
   832
  have prob_x: "\<And> y. y \<in> space M \<Longrightarrow> prob {y} = prob {x}"
hoelzl@39097
   833
    using assms(2)[OF _ `x \<in> space M`] by blast
hoelzl@39097
   834
  have "1 = prob (space M)"
hoelzl@39097
   835
    using prob_space by auto
hoelzl@39097
   836
  also have "\<dots> = (\<Sum> x \<in> space M. prob {x})"
hoelzl@39097
   837
    using real_finite_measure_finite_Union[of "space M" "\<lambda> x. {x}", simplified]
hoelzl@39097
   838
      sets_eq_Pow inj_singleton[unfolded inj_on_def, rule_format]
hoelzl@39097
   839
      finite_space unfolding disjoint_family_on_def  prob_space[symmetric]
hoelzl@39097
   840
    by (auto simp add:setsum_restrict_set)
hoelzl@39097
   841
  also have "\<dots> = (\<Sum> y \<in> space M. prob {x})"
hoelzl@39097
   842
    using prob_x by auto
hoelzl@39097
   843
  also have "\<dots> = real_of_nat (card (space M)) * prob {x}" by simp
hoelzl@39097
   844
  finally have one: "1 = real (card (space M)) * prob {x}"
hoelzl@39097
   845
    using real_eq_of_nat by auto
hoelzl@39097
   846
  hence two: "real (card (space M)) \<noteq> 0" by fastsimp 
hoelzl@39097
   847
  from one have three: "prob {x} \<noteq> 0" by fastsimp
hoelzl@39097
   848
  thus ?thesis using one two three divide_cancel_right
hoelzl@39097
   849
    by (auto simp:field_simps)
hoelzl@39092
   850
qed
hoelzl@35977
   851
hoelzl@39092
   852
lemma (in prob_space) prob_space_subalgebra:
hoelzl@39092
   853
  assumes "N \<subseteq> sets M" "sigma_algebra (M\<lparr> sets := N \<rparr>)"
hoelzl@39092
   854
  shows "prob_space (M\<lparr> sets := N \<rparr>) \<mu>"
hoelzl@39092
   855
proof -
hoelzl@39092
   856
  interpret N: measure_space "M\<lparr> sets := N \<rparr>" \<mu>
hoelzl@39092
   857
    using measure_space_subalgebra[OF assms] .
hoelzl@39092
   858
  show ?thesis
hoelzl@39092
   859
    proof qed (simp add: measure_space_1)
hoelzl@35977
   860
qed
hoelzl@35977
   861
hoelzl@39092
   862
lemma (in prob_space) prob_space_of_restricted_space:
hoelzl@39092
   863
  assumes "\<mu> A \<noteq> 0" "\<mu> A \<noteq> \<omega>" "A \<in> sets M"
hoelzl@39092
   864
  shows "prob_space (restricted_space A) (\<lambda>S. \<mu> S / \<mu> A)"
hoelzl@39092
   865
  unfolding prob_space_def prob_space_axioms_def
hoelzl@39092
   866
proof
hoelzl@39092
   867
  show "\<mu> (space (restricted_space A)) / \<mu> A = 1"
hoelzl@39092
   868
    using `\<mu> A \<noteq> 0` `\<mu> A \<noteq> \<omega>` by (auto simp: pinfreal_noteq_omega_Ex)
hoelzl@39092
   869
  have *: "\<And>S. \<mu> S / \<mu> A = inverse (\<mu> A) * \<mu> S" by (simp add: mult_commute)
hoelzl@39092
   870
  interpret A: measure_space "restricted_space A" \<mu>
hoelzl@39092
   871
    using `A \<in> sets M` by (rule restricted_measure_space)
hoelzl@39092
   872
  show "measure_space (restricted_space A) (\<lambda>S. \<mu> S / \<mu> A)"
hoelzl@39092
   873
  proof
hoelzl@39092
   874
    show "\<mu> {} / \<mu> A = 0" by auto
hoelzl@39092
   875
    show "countably_additive (restricted_space A) (\<lambda>S. \<mu> S / \<mu> A)"
hoelzl@39092
   876
        unfolding countably_additive_def psuminf_cmult_right *
hoelzl@39092
   877
        using A.measure_countably_additive by auto
hoelzl@39092
   878
  qed
hoelzl@39092
   879
qed
hoelzl@39092
   880
hoelzl@39092
   881
lemma finite_prob_spaceI:
hoelzl@39092
   882
  assumes "finite (space M)" "sets M = Pow(space M)" "\<mu> (space M) = 1" "\<mu> {} = 0"
hoelzl@39092
   883
    and "\<And>A B. A\<subseteq>space M \<Longrightarrow> B\<subseteq>space M \<Longrightarrow> A \<inter> B = {} \<Longrightarrow> \<mu> (A \<union> B) = \<mu> A + \<mu> B"
hoelzl@39092
   884
  shows "finite_prob_space M \<mu>"
hoelzl@39092
   885
  unfolding finite_prob_space_eq
hoelzl@39092
   886
proof
hoelzl@39092
   887
  show "finite_measure_space M \<mu>" using assms
hoelzl@39092
   888
     by (auto intro!: finite_measure_spaceI)
hoelzl@39092
   889
  show "\<mu> (space M) = 1" by fact
hoelzl@39092
   890
qed
hoelzl@36624
   891
hoelzl@36624
   892
lemma (in finite_prob_space) finite_measure_space:
hoelzl@39097
   893
  fixes X :: "'a \<Rightarrow> 'x"
hoelzl@38656
   894
  shows "finite_measure_space \<lparr>space = X ` space M, sets = Pow (X ` space M)\<rparr> (distribution X)"
hoelzl@38656
   895
    (is "finite_measure_space ?S _")
hoelzl@39092
   896
proof (rule finite_measure_spaceI, simp_all)
hoelzl@36624
   897
  show "finite (X ` space M)" using finite_space by simp
hoelzl@39097
   898
next
hoelzl@39097
   899
  fix A B :: "'x set" assume "A \<inter> B = {}"
hoelzl@39097
   900
  then show "distribution X (A \<union> B) = distribution X A + distribution X B"
hoelzl@39097
   901
    unfolding distribution_def
hoelzl@39097
   902
    by (subst measure_additive)
hoelzl@39097
   903
       (auto intro!: arg_cong[where f=\<mu>] simp: sets_eq_Pow)
hoelzl@36624
   904
qed
hoelzl@36624
   905
hoelzl@39097
   906
lemma (in finite_prob_space) finite_prob_space_of_images:
hoelzl@39097
   907
  "finite_prob_space \<lparr> space = X ` space M, sets = Pow (X ` space M)\<rparr> (distribution X)"
hoelzl@39097
   908
  by (simp add: finite_prob_space_eq finite_measure_space)
hoelzl@39097
   909
hoelzl@39097
   910
lemma (in finite_prob_space) real_distribution_order':
hoelzl@39097
   911
  shows "real (distribution X {x}) = 0 \<Longrightarrow> real (joint_distribution X Y {(x, y)}) = 0"
hoelzl@39097
   912
  and "real (distribution Y {y}) = 0 \<Longrightarrow> real (joint_distribution X Y {(x, y)}) = 0"
hoelzl@39097
   913
  using real_of_pinfreal_mono[OF distribution_finite joint_distribution_restriction_fst, of X Y "{(x, y)}"]
hoelzl@39097
   914
  using real_of_pinfreal_mono[OF distribution_finite joint_distribution_restriction_snd, of X Y "{(x, y)}"]
hoelzl@39097
   915
  using real_pinfreal_nonneg[of "joint_distribution X Y {(x, y)}"]
hoelzl@39097
   916
  by auto
hoelzl@39097
   917
hoelzl@39096
   918
lemma (in finite_prob_space) finite_product_measure_space:
hoelzl@39097
   919
  fixes X :: "'a \<Rightarrow> 'x" and Y :: "'a \<Rightarrow> 'y"
hoelzl@39096
   920
  assumes "finite s1" "finite s2"
hoelzl@39096
   921
  shows "finite_measure_space \<lparr> space = s1 \<times> s2, sets = Pow (s1 \<times> s2)\<rparr> (joint_distribution X Y)"
hoelzl@39096
   922
    (is "finite_measure_space ?M ?D")
hoelzl@39097
   923
proof (rule finite_measure_spaceI, simp_all)
hoelzl@39097
   924
  show "finite (s1 \<times> s2)"
hoelzl@39096
   925
    using assms by auto
hoelzl@39097
   926
  show "joint_distribution X Y (s1\<times>s2) \<noteq> \<omega>"
hoelzl@39097
   927
    using distribution_finite .
hoelzl@39097
   928
next
hoelzl@39097
   929
  fix A B :: "('x*'y) set" assume "A \<inter> B = {}"
hoelzl@39097
   930
  then show "joint_distribution X Y (A \<union> B) = joint_distribution X Y A + joint_distribution X Y B"
hoelzl@39097
   931
    unfolding distribution_def
hoelzl@39097
   932
    by (subst measure_additive)
hoelzl@39097
   933
       (auto intro!: arg_cong[where f=\<mu>] simp: sets_eq_Pow)
hoelzl@39096
   934
qed
hoelzl@39096
   935
hoelzl@39097
   936
lemma (in finite_prob_space) finite_product_measure_space_of_images:
hoelzl@39096
   937
  shows "finite_measure_space \<lparr> space = X ` space M \<times> Y ` space M,
hoelzl@39096
   938
                                sets = Pow (X ` space M \<times> Y ` space M) \<rparr>
hoelzl@39096
   939
                              (joint_distribution X Y)"
hoelzl@39096
   940
  using finite_space by (auto intro!: finite_product_measure_space)
hoelzl@39096
   941
hoelzl@40859
   942
lemma (in finite_prob_space) finite_product_prob_space_of_images:
hoelzl@40859
   943
  "finite_prob_space \<lparr> space = X ` space M \<times> Y ` space M, sets = Pow (X ` space M \<times> Y ` space M)\<rparr>
hoelzl@40859
   944
                     (joint_distribution X Y)"
hoelzl@40859
   945
  (is "finite_prob_space ?S _")
hoelzl@40859
   946
proof (simp add: finite_prob_space_eq finite_product_measure_space_of_images)
hoelzl@40859
   947
  have "X -` X ` space M \<inter> Y -` Y ` space M \<inter> space M = space M" by auto
hoelzl@40859
   948
  thus "joint_distribution X Y (X ` space M \<times> Y ` space M) = 1"
hoelzl@40859
   949
    by (simp add: distribution_def prob_space vimage_Times comp_def measure_space_1)
hoelzl@40859
   950
qed
hoelzl@40859
   951
hoelzl@39085
   952
section "Conditional Expectation and Probability"
hoelzl@39085
   953
hoelzl@39085
   954
lemma (in prob_space) conditional_expectation_exists:
hoelzl@39083
   955
  fixes X :: "'a \<Rightarrow> pinfreal"
hoelzl@39083
   956
  assumes borel: "X \<in> borel_measurable M"
hoelzl@39083
   957
  and N_subalgebra: "N \<subseteq> sets M" "sigma_algebra (M\<lparr> sets := N \<rparr>)"
hoelzl@39083
   958
  shows "\<exists>Y\<in>borel_measurable (M\<lparr> sets := N \<rparr>). \<forall>C\<in>N.
hoelzl@39083
   959
      positive_integral (\<lambda>x. Y x * indicator C x) = positive_integral (\<lambda>x. X x * indicator C x)"
hoelzl@39083
   960
proof -
hoelzl@39083
   961
  interpret P: prob_space "M\<lparr> sets := N \<rparr>" \<mu>
hoelzl@39083
   962
    using prob_space_subalgebra[OF N_subalgebra] .
hoelzl@39083
   963
hoelzl@39083
   964
  let "?f A" = "\<lambda>x. X x * indicator A x"
hoelzl@39083
   965
  let "?Q A" = "positive_integral (?f A)"
hoelzl@39083
   966
hoelzl@39083
   967
  from measure_space_density[OF borel]
hoelzl@39083
   968
  have Q: "measure_space (M\<lparr> sets := N \<rparr>) ?Q"
hoelzl@39083
   969
    by (rule measure_space.measure_space_subalgebra[OF _ N_subalgebra])
hoelzl@39083
   970
  then interpret Q: measure_space "M\<lparr> sets := N \<rparr>" ?Q .
hoelzl@39083
   971
hoelzl@39083
   972
  have "P.absolutely_continuous ?Q"
hoelzl@39083
   973
    unfolding P.absolutely_continuous_def
hoelzl@39083
   974
  proof (safe, simp)
hoelzl@39083
   975
    fix A assume "A \<in> N" "\<mu> A = 0"
hoelzl@39083
   976
    moreover then have f_borel: "?f A \<in> borel_measurable M"
hoelzl@39083
   977
      using borel N_subalgebra by (auto intro: borel_measurable_indicator)
hoelzl@39083
   978
    moreover have "{x\<in>space M. ?f A x \<noteq> 0} = (?f A -` {0<..} \<inter> space M) \<inter> A"
hoelzl@39083
   979
      by (auto simp: indicator_def)
hoelzl@39083
   980
    moreover have "\<mu> \<dots> \<le> \<mu> A"
hoelzl@39083
   981
      using `A \<in> N` N_subalgebra f_borel
hoelzl@39083
   982
      by (auto intro!: measure_mono Int[of _ A] measurable_sets)
hoelzl@39083
   983
    ultimately show "?Q A = 0"
hoelzl@39083
   984
      by (simp add: positive_integral_0_iff)
hoelzl@39083
   985
  qed
hoelzl@39083
   986
  from P.Radon_Nikodym[OF Q this]
hoelzl@39083
   987
  obtain Y where Y: "Y \<in> borel_measurable (M\<lparr>sets := N\<rparr>)"
hoelzl@39083
   988
    "\<And>A. A \<in> sets (M\<lparr>sets:=N\<rparr>) \<Longrightarrow> ?Q A = P.positive_integral (\<lambda>x. Y x * indicator A x)"
hoelzl@39083
   989
    by blast
hoelzl@39084
   990
  with N_subalgebra show ?thesis
hoelzl@39084
   991
    by (auto intro!: bexI[OF _ Y(1)])
hoelzl@39083
   992
qed
hoelzl@39083
   993
hoelzl@39085
   994
definition (in prob_space)
hoelzl@39085
   995
  "conditional_expectation N X = (SOME Y. Y\<in>borel_measurable (M\<lparr>sets:=N\<rparr>)
hoelzl@39085
   996
    \<and> (\<forall>C\<in>N. positive_integral (\<lambda>x. Y x * indicator C x) = positive_integral (\<lambda>x. X x * indicator C x)))"
hoelzl@39085
   997
hoelzl@39085
   998
abbreviation (in prob_space)
hoelzl@39092
   999
  "conditional_prob N A \<equiv> conditional_expectation N (indicator A)"
hoelzl@39085
  1000
hoelzl@39085
  1001
lemma (in prob_space)
hoelzl@39085
  1002
  fixes X :: "'a \<Rightarrow> pinfreal"
hoelzl@39085
  1003
  assumes borel: "X \<in> borel_measurable M"
hoelzl@39085
  1004
  and N_subalgebra: "N \<subseteq> sets M" "sigma_algebra (M\<lparr> sets := N \<rparr>)"
hoelzl@39085
  1005
  shows borel_measurable_conditional_expectation:
hoelzl@39085
  1006
    "conditional_expectation N X \<in> borel_measurable (M\<lparr> sets := N \<rparr>)"
hoelzl@39085
  1007
  and conditional_expectation: "\<And>C. C \<in> N \<Longrightarrow>
hoelzl@39085
  1008
      positive_integral (\<lambda>x. conditional_expectation N X x * indicator C x) =
hoelzl@39085
  1009
      positive_integral (\<lambda>x. X x * indicator C x)"
hoelzl@39085
  1010
   (is "\<And>C. C \<in> N \<Longrightarrow> ?eq C")
hoelzl@39085
  1011
proof -
hoelzl@39085
  1012
  note CE = conditional_expectation_exists[OF assms, unfolded Bex_def]
hoelzl@39085
  1013
  then show "conditional_expectation N X \<in> borel_measurable (M\<lparr> sets := N \<rparr>)"
hoelzl@39085
  1014
    unfolding conditional_expectation_def by (rule someI2_ex) blast
hoelzl@39085
  1015
hoelzl@39085
  1016
  from CE show "\<And>C. C\<in>N \<Longrightarrow> ?eq C"
hoelzl@39085
  1017
    unfolding conditional_expectation_def by (rule someI2_ex) blast
hoelzl@39085
  1018
qed
hoelzl@39085
  1019
hoelzl@39091
  1020
lemma (in sigma_algebra) factorize_measurable_function:
hoelzl@39091
  1021
  fixes Z :: "'a \<Rightarrow> pinfreal" and Y :: "'a \<Rightarrow> 'c"
hoelzl@39091
  1022
  assumes "sigma_algebra M'" and "Y \<in> measurable M M'" "Z \<in> borel_measurable M"
hoelzl@39091
  1023
  shows "Z \<in> borel_measurable (sigma_algebra.vimage_algebra M' (space M) Y)
hoelzl@39091
  1024
    \<longleftrightarrow> (\<exists>g\<in>borel_measurable M'. \<forall>x\<in>space M. Z x = g (Y x))"
hoelzl@39091
  1025
proof safe
hoelzl@39091
  1026
  interpret M': sigma_algebra M' by fact
hoelzl@39091
  1027
  have Y: "Y \<in> space M \<rightarrow> space M'" using assms unfolding measurable_def by auto
hoelzl@39091
  1028
  from M'.sigma_algebra_vimage[OF this]
hoelzl@39091
  1029
  interpret va: sigma_algebra "M'.vimage_algebra (space M) Y" .
hoelzl@39091
  1030
hoelzl@39091
  1031
  { fix g :: "'c \<Rightarrow> pinfreal" assume "g \<in> borel_measurable M'"
hoelzl@39091
  1032
    with M'.measurable_vimage_algebra[OF Y]
hoelzl@39091
  1033
    have "g \<circ> Y \<in> borel_measurable (M'.vimage_algebra (space M) Y)"
hoelzl@39091
  1034
      by (rule measurable_comp)
hoelzl@39091
  1035
    moreover assume "\<forall>x\<in>space M. Z x = g (Y x)"
hoelzl@39091
  1036
    then have "Z \<in> borel_measurable (M'.vimage_algebra (space M) Y) \<longleftrightarrow>
hoelzl@39091
  1037
       g \<circ> Y \<in> borel_measurable (M'.vimage_algebra (space M) Y)"
hoelzl@39091
  1038
       by (auto intro!: measurable_cong)
hoelzl@39091
  1039
    ultimately show "Z \<in> borel_measurable (M'.vimage_algebra (space M) Y)"
hoelzl@39091
  1040
      by simp }
hoelzl@39091
  1041
hoelzl@39091
  1042
  assume "Z \<in> borel_measurable (M'.vimage_algebra (space M) Y)"
hoelzl@39091
  1043
  from va.borel_measurable_implies_simple_function_sequence[OF this]
hoelzl@39091
  1044
  obtain f where f: "\<And>i. va.simple_function (f i)" and "f \<up> Z" by blast
hoelzl@39091
  1045
hoelzl@39091
  1046
  have "\<forall>i. \<exists>g. M'.simple_function g \<and> (\<forall>x\<in>space M. f i x = g (Y x))"
hoelzl@39091
  1047
  proof
hoelzl@39091
  1048
    fix i
hoelzl@39091
  1049
    from f[of i] have "finite (f i`space M)" and B_ex:
hoelzl@39091
  1050
      "\<forall>z\<in>(f i)`space M. \<exists>B. B \<in> sets M' \<and> (f i) -` {z} \<inter> space M = Y -` B \<inter> space M"
hoelzl@39091
  1051
      unfolding va.simple_function_def by auto
hoelzl@39091
  1052
    from B_ex[THEN bchoice] guess B .. note B = this
hoelzl@39091
  1053
hoelzl@39091
  1054
    let ?g = "\<lambda>x. \<Sum>z\<in>f i`space M. z * indicator (B z) x"
hoelzl@39091
  1055
hoelzl@39091
  1056
    show "\<exists>g. M'.simple_function g \<and> (\<forall>x\<in>space M. f i x = g (Y x))"
hoelzl@39091
  1057
    proof (intro exI[of _ ?g] conjI ballI)
hoelzl@39091
  1058
      show "M'.simple_function ?g" using B by auto
hoelzl@39091
  1059
hoelzl@39091
  1060
      fix x assume "x \<in> space M"
hoelzl@39091
  1061
      then have "\<And>z. z \<in> f i`space M \<Longrightarrow> indicator (B z) (Y x) = (indicator (f i -` {z} \<inter> space M) x::pinfreal)"
hoelzl@39091
  1062
        unfolding indicator_def using B by auto
hoelzl@39091
  1063
      then show "f i x = ?g (Y x)" using `x \<in> space M` f[of i]
hoelzl@39091
  1064
        by (subst va.simple_function_indicator_representation) auto
hoelzl@39091
  1065
    qed
hoelzl@39091
  1066
  qed
hoelzl@39091
  1067
  from choice[OF this] guess g .. note g = this
hoelzl@39091
  1068
hoelzl@39091
  1069
  show "\<exists>g\<in>borel_measurable M'. \<forall>x\<in>space M. Z x = g (Y x)"
hoelzl@39091
  1070
  proof (intro ballI bexI)
hoelzl@39091
  1071
    show "(SUP i. g i) \<in> borel_measurable M'"
hoelzl@39091
  1072
      using g by (auto intro: M'.borel_measurable_simple_function)
hoelzl@39091
  1073
    fix x assume "x \<in> space M"
hoelzl@39091
  1074
    have "Z x = (SUP i. f i) x" using `f \<up> Z` unfolding isoton_def by simp
hoelzl@39091
  1075
    also have "\<dots> = (SUP i. g i) (Y x)" unfolding SUPR_fun_expand
hoelzl@39091
  1076
      using g `x \<in> space M` by simp
hoelzl@39091
  1077
    finally show "Z x = (SUP i. g i) (Y x)" .
hoelzl@39091
  1078
  qed
hoelzl@39091
  1079
qed
hoelzl@39090
  1080
hoelzl@35582
  1081
end