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