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