35582

1 
theory Probability_Space


2 
imports Lebesgue


3 
begin


4 


5 
locale prob_space = measure_space +


6 
assumes prob_space: "measure M (space M) = 1"


7 
begin


8 


9 
abbreviation "events \<equiv> sets M"


10 
abbreviation "prob \<equiv> measure M"


11 
abbreviation "prob_preserving \<equiv> measure_preserving"


12 
abbreviation "random_variable \<equiv> \<lambda> s X. X \<in> measurable M s"


13 
abbreviation "expectation \<equiv> integral"


14 


15 
definition


16 
"indep A B \<longleftrightarrow> A \<in> events \<and> B \<in> events \<and> prob (A \<inter> B) = prob A * prob B"


17 


18 
definition


19 
"indep_families F G \<longleftrightarrow> (\<forall> A \<in> F. \<forall> B \<in> G. indep A B)"


20 


21 
definition


22 
"distribution X = (\<lambda>s. prob ((X ` s) \<inter> (space M)))"


23 


24 
definition


25 
"probably e \<longleftrightarrow> e \<in> events \<and> prob e = 1"


26 


27 
definition


28 
"possibly e \<longleftrightarrow> e \<in> events \<and> prob e \<noteq> 0"


29 


30 
definition


31 
"joint_distribution X Y \<equiv> (\<lambda>a. prob ((\<lambda>x. (X x, Y x)) ` a \<inter> space M))"


32 


33 
definition


34 
"conditional_expectation X s \<equiv> THE f. random_variable borel_space f \<and>


35 
(\<forall> g \<in> s. integral (\<lambda>x. f x * indicator_fn g x) =


36 
integral (\<lambda>x. X x * indicator_fn g x))"


37 


38 
definition


39 
"conditional_prob e1 e2 \<equiv> conditional_expectation (indicator_fn e1) e2"


40 


41 
lemma positive: "positive M prob"


42 
unfolding positive_def using positive empty_measure by blast


43 


44 
lemma prob_compl:


45 
assumes "s \<in> events"


46 
shows "prob (space M  s) = 1  prob s"


47 
using assms


48 
proof 


49 
have "prob ((space M  s) \<union> s) = prob (space M  s) + prob s"


50 
using assms additive[unfolded additive_def] by blast


51 
thus ?thesis by (simp add:Un_absorb2[OF sets_into_space[OF assms]] prob_space)


52 
qed


53 


54 
lemma indep_space:


55 
assumes "s \<in> events"


56 
shows "indep (space M) s"


57 
using assms prob_space


58 
unfolding indep_def by auto


59 


60 


61 
lemma prob_space_increasing:


62 
"increasing M prob"


63 
by (rule additive_increasing[OF positive additive])


64 


65 
lemma prob_subadditive:


66 
assumes "s \<in> events" "t \<in> events"


67 
shows "prob (s \<union> t) \<le> prob s + prob t"


68 
using assms


69 
proof 


70 
have "prob (s \<union> t) = prob ((s  t) \<union> t)" by simp


71 
also have "\<dots> = prob (s  t) + prob t"


72 
using additive[unfolded additive_def, rule_format, of "st" "t"]


73 
assms by blast


74 
also have "\<dots> \<le> prob s + prob t"


75 
using prob_space_increasing[unfolded increasing_def, rule_format] assms


76 
by auto


77 
finally show ?thesis by simp


78 
qed


79 


80 
lemma prob_zero_union:


81 
assumes "s \<in> events" "t \<in> events" "prob t = 0"


82 
shows "prob (s \<union> t) = prob s"


83 
using assms


84 
proof 


85 
have "prob (s \<union> t) \<le> prob s"


86 
using prob_subadditive[of s t] assms by auto


87 
moreover have "prob (s \<union> t) \<ge> prob s"


88 
using prob_space_increasing[unfolded increasing_def, rule_format]


89 
assms by auto


90 
ultimately show ?thesis by simp


91 
qed


92 


93 
lemma prob_eq_compl:


94 
assumes "s \<in> events" "t \<in> events"


95 
assumes "prob (space M  s) = prob (space M  t)"


96 
shows "prob s = prob t"


97 
using assms prob_compl by auto


98 


99 
lemma prob_one_inter:


100 
assumes events:"s \<in> events" "t \<in> events"


101 
assumes "prob t = 1"


102 
shows "prob (s \<inter> t) = prob s"


103 
using assms


104 
proof 


105 
have "prob ((space M  s) \<union> (space M  t)) = prob (space M  s)"


106 
using prob_compl[of "t"] prob_zero_union assms by auto


107 
then show "prob (s \<inter> t) = prob s"


108 
using prob_eq_compl[of "s \<inter> t"] events by (simp only: Diff_Int) auto


109 
qed


110 


111 
lemma prob_eq_bigunion_image:


112 
assumes "range f \<subseteq> events" "range g \<subseteq> events"


113 
assumes "disjoint_family f" "disjoint_family g"


114 
assumes "\<And> n :: nat. prob (f n) = prob (g n)"


115 
shows "(prob (\<Union> i. f i) = prob (\<Union> i. g i))"


116 
using assms


117 
proof 


118 
have a: "(\<lambda> i. prob (f i)) sums (prob (\<Union> i. f i))"


119 
using ca[unfolded countably_additive_def] assms by blast


120 
have b: "(\<lambda> i. prob (g i)) sums (prob (\<Union> i. g i))"


121 
using ca[unfolded countably_additive_def] assms by blast


122 
show ?thesis using sums_unique[OF b] sums_unique[OF a] assms by simp


123 
qed


124 


125 
lemma prob_countably_subadditive:


126 
assumes "range f \<subseteq> events"


127 
assumes "summable (prob \<circ> f)"


128 
shows "prob (\<Union>i. f i) \<le> (\<Sum> i. prob (f i))"


129 
using assms


130 
proof 


131 
def f' == "\<lambda> i. f i  (\<Union> j \<in> {0 ..< i}. f j)"


132 
have "(\<Union> i. f' i) \<subseteq> (\<Union> i. f i)" unfolding f'_def by auto


133 
moreover have "(\<Union> i. f' i) \<supseteq> (\<Union> i. f i)"


134 
proof (rule subsetI)


135 
fix x assume "x \<in> (\<Union> i. f i)"


136 
then obtain k where "x \<in> f k" by blast


137 
hence k: "k \<in> {m. x \<in> f m}" by simp


138 
have "\<exists> l. x \<in> f l \<and> (\<forall> l' < l. x \<notin> f l')"


139 
using wfE_min[of "{(x, y). x < y}" "k" "{m. x \<in> f m}",


140 
OF wf_less k] by auto


141 
thus "x \<in> (\<Union> i. f' i)" unfolding f'_def by auto


142 
qed


143 
ultimately have uf'f: "(\<Union> i. f' i) = (\<Union> i. f i)" by (rule equalityI)


144 


145 
have df': "\<And> i j. i < j \<Longrightarrow> f' i \<inter> f' j = {}"


146 
unfolding f'_def by auto


147 
have "\<And> i j. i \<noteq> j \<Longrightarrow> f' i \<inter> f' j = {}"


148 
apply (drule iffD1[OF nat_neq_iff])


149 
using df' by auto


150 
hence df: "disjoint_family f'" unfolding disjoint_family_on_def by simp


151 


152 
have rf': "\<And> i. f' i \<in> events"


153 
proof 


154 
fix i :: nat


155 
have "(\<Union> {f j  j. j \<in> {0 ..< i}}) = (\<Union> j \<in> {0 ..< i}. f j)" by blast


156 
hence "(\<Union> {f j  j. j \<in> {0 ..< i}}) \<in> events


157 
\<Longrightarrow> (\<Union> j \<in> {0 ..< i}. f j) \<in> events" by auto


158 
thus "f' i \<in> events"


159 
unfolding f'_def


160 
using assms finite_union[of "{f j  j. j \<in> {0 ..< i}}"]


161 
Diff[of "f i" "\<Union> j \<in> {0 ..< i}. f j"] by auto


162 
qed


163 
hence uf': "(\<Union> range f') \<in> events" by auto


164 


165 
have "\<And> i. prob (f' i) \<le> prob (f i)"


166 
using prob_space_increasing[unfolded increasing_def, rule_format, OF rf']


167 
assms rf' unfolding f'_def by blast


168 


169 
hence absinc: "\<And> i. \<bar> prob (f' i) \<bar> \<le> prob (f i)"


170 
using abs_of_nonneg positive[unfolded positive_def]


171 
assms rf' by auto


172 


173 
have "prob (\<Union> i. f i) = prob (\<Union> i. f' i)" using uf'f by simp


174 


175 
also have "\<dots> = (\<Sum> i. prob (f' i))"


176 
using ca[unfolded countably_additive_def, rule_format]


177 
sums_unique rf' uf' df


178 
by auto


179 


180 
also have "\<dots> \<le> (\<Sum> i. prob (f i))"


181 
using summable_le2[of "\<lambda> i. prob (f' i)" "\<lambda> i. prob (f i)",


182 
rule_format, OF absinc]


183 
assms[unfolded o_def] by auto


184 


185 
finally show ?thesis by auto


186 
qed


187 


188 
lemma prob_countably_zero:


189 
assumes "range c \<subseteq> events"


190 
assumes "\<And> i. prob (c i) = 0"


191 
shows "(prob (\<Union> i :: nat. c i) = 0)"


192 
using assms


193 
proof 


194 
have leq0: "0 \<le> prob (\<Union> i. c i)"


195 
using assms positive[unfolded positive_def, rule_format]


196 
by auto


197 


198 
have "prob (\<Union> i. c i) \<le> (\<Sum> i. prob (c i))"


199 
using prob_countably_subadditive[of c, unfolded o_def]


200 
assms sums_zero sums_summable by auto


201 


202 
also have "\<dots> = 0"


203 
using assms sums_zero


204 
sums_unique[of "\<lambda> i. prob (c i)" "0"] by auto


205 


206 
finally show "prob (\<Union> i. c i) = 0"


207 
using leq0 by auto


208 
qed


209 


210 
lemma indep_sym:


211 
"indep a b \<Longrightarrow> indep b a"


212 
unfolding indep_def using Int_commute[of a b] by auto


213 


214 
lemma indep_refl:


215 
assumes "a \<in> events"


216 
shows "indep a a = (prob a = 0) \<or> (prob a = 1)"


217 
using assms unfolding indep_def by auto


218 


219 
lemma prob_equiprobable_finite_unions:


220 
assumes "s \<in> events"


221 
assumes "\<And>x. x \<in> s \<Longrightarrow> {x} \<in> events"


222 
assumes "finite s"


223 
assumes "\<And> x y. \<lbrakk>x \<in> s; y \<in> s\<rbrakk> \<Longrightarrow> (prob {x} = prob {y})"


224 
shows "prob s = of_nat (card s) * prob {SOME x. x \<in> s}"


225 
using assms


226 
proof (cases "s = {}")


227 
case True thus ?thesis by simp


228 
next


229 
case False hence " \<exists> x. x \<in> s" by blast


230 
from someI_ex[OF this] assms


231 
have prob_some: "\<And> x. x \<in> s \<Longrightarrow> prob {x} = prob {SOME y. y \<in> s}" by blast


232 
have "prob s = (\<Sum> x \<in> s. prob {x})"


233 
using assms measure_real_sum_image by blast


234 
also have "\<dots> = (\<Sum> x \<in> s. prob {SOME y. y \<in> s})" using prob_some by auto


235 
also have "\<dots> = of_nat (card s) * prob {(SOME x. x \<in> s)}"


236 
using setsum_constant assms by auto


237 
finally show ?thesis by simp


238 
qed


239 


240 
lemma prob_real_sum_image_fn:


241 
assumes "e \<in> events"


242 
assumes "\<And> x. x \<in> s \<Longrightarrow> e \<inter> f x \<in> events"


243 
assumes "finite s"


244 
assumes "\<And> x y. \<lbrakk>x \<in> s ; y \<in> s ; x \<noteq> y\<rbrakk> \<Longrightarrow> f x \<inter> f y = {}"


245 
assumes "space M \<subseteq> (\<Union> i \<in> s. f i)"


246 
shows "prob e = (\<Sum> x \<in> s. prob (e \<inter> f x))"


247 
using assms


248 
proof 


249 
let ?S = "{0 ..< card s}"


250 
obtain g where "g ` ?S = s \<and> inj_on g ?S"


251 
using ex_bij_betw_nat_finite[unfolded bij_betw_def, of s] assms by auto


252 
moreover hence gs: "g ` ?S = s" by simp


253 
ultimately have ginj: "inj_on g ?S" by simp


254 
let ?f' = "\<lambda> i. e \<inter> f (g i)"


255 
have f': "?f' \<in> ?S \<rightarrow> events"


256 
using gs assms by blast


257 
hence "\<And> i j. \<lbrakk>i \<in> ?S ; j \<in> ?S ; i \<noteq> j\<rbrakk>


258 
\<Longrightarrow> ?f' i \<inter> ?f' j = {}" using assms ginj[unfolded inj_on_def] gs f' by blast


259 
hence df': "\<And> i j. \<lbrakk>i < card s ; j < card s ; i \<noteq> j\<rbrakk>


260 
\<Longrightarrow> ?f' i \<inter> ?f' j = {}" by simp


261 


262 
have "e = e \<inter> space M" using assms sets_into_space by simp


263 
also hence "\<dots> = e \<inter> (\<Union> x \<in> s. f x)" using assms by blast


264 
also have "\<dots> = (\<Union> x \<in> g ` ?S. e \<inter> f x)" using gs by simp


265 
also have "\<dots> = (\<Union> i \<in> ?S. ?f' i)" by simp


266 
finally have "prob e = prob (\<Union> i \<in> ?S. ?f' i)" by simp


267 
also have "\<dots> = (\<Sum> i \<in> ?S. prob (?f' i))"


268 
apply (subst measure_finitely_additive'')


269 
using f' df' assms by (auto simp: disjoint_family_on_def)


270 
also have "\<dots> = (\<Sum> x \<in> g ` ?S. prob (e \<inter> f x))"


271 
using setsum_reindex[of g "?S" "\<lambda> x. prob (e \<inter> f x)"]


272 
ginj by simp


273 
also have "\<dots> = (\<Sum> x \<in> s. prob (e \<inter> f x))" using gs by simp


274 
finally show ?thesis by simp


275 
qed


276 


277 
lemma distribution_prob_space:


278 
assumes "random_variable s X"


279 
shows "prob_space \<lparr>space = space s, sets = sets s, measure = distribution X\<rparr>"


280 
using assms


281 
proof 


282 
let ?N = "\<lparr>space = space s, sets = sets s, measure = distribution X\<rparr>"


283 
interpret s: sigma_algebra "s" using assms[unfolded measurable_def] by auto


284 
hence sigN: "sigma_algebra ?N" using s.sigma_algebra_extend by auto


285 


286 
have pos: "\<And> e. e \<in> sets s \<Longrightarrow> distribution X e \<ge> 0"


287 
unfolding distribution_def


288 
using positive[unfolded positive_def]


289 
assms[unfolded measurable_def] by auto


290 


291 
have cas: "countably_additive ?N (distribution X)"


292 
proof 


293 
{


294 
fix f :: "nat \<Rightarrow> 'c \<Rightarrow> bool"


295 
let ?g = "\<lambda> n. X ` f n \<inter> space M"


296 
assume asm: "range f \<subseteq> sets s" "UNION UNIV f \<in> sets s" "disjoint_family f"


297 
hence "range ?g \<subseteq> events"


298 
using assms unfolding measurable_def by blast


299 
from ca[unfolded countably_additive_def,


300 
rule_format, of ?g, OF this] countable_UN[OF this] asm


301 
have "(\<lambda> n. prob (?g n)) sums prob (UNION UNIV ?g)"


302 
unfolding disjoint_family_on_def by blast


303 
moreover have "(X ` (\<Union> n. f n)) = (\<Union> n. X ` f n)" by blast


304 
ultimately have "(\<lambda> n. distribution X (f n)) sums distribution X (UNION UNIV f)"


305 
unfolding distribution_def by simp


306 
} thus ?thesis unfolding countably_additive_def by simp


307 
qed


308 


309 
have ds0: "distribution X {} = 0"


310 
unfolding distribution_def by simp


311 


312 
have "X ` space s \<inter> space M = space M"


313 
using assms[unfolded measurable_def] by auto


314 
hence ds1: "distribution X (space s) = 1"


315 
unfolding measurable_def distribution_def using prob_space by simp


316 


317 
from ds0 ds1 cas pos sigN


318 
show "prob_space ?N"


319 
unfolding prob_space_def prob_space_axioms_def


320 
measure_space_def measure_space_axioms_def by simp


321 
qed


322 


323 
lemma distribution_lebesgue_thm1:


324 
assumes "random_variable s X"


325 
assumes "A \<in> sets s"


326 
shows "distribution X A = expectation (indicator_fn (X ` A \<inter> space M))"


327 
unfolding distribution_def


328 
using assms unfolding measurable_def


329 
using integral_indicator_fn by auto


330 


331 
lemma distribution_lebesgue_thm2:


332 
assumes "random_variable s X" "A \<in> sets s"


333 
shows "distribution X A = measure_space.integral \<lparr>space = space s, sets = sets s, measure = distribution X\<rparr> (indicator_fn A)"


334 
(is "_ = measure_space.integral ?M _")


335 
proof 


336 
interpret S: prob_space ?M using assms(1) by (rule distribution_prob_space)


337 


338 
show ?thesis


339 
using S.integral_indicator_fn(1)


340 
using assms unfolding distribution_def by auto


341 
qed


342 


343 
lemma finite_expectation1:


344 
assumes "finite (space M)" "random_variable borel_space X"


345 
shows "expectation X = (\<Sum> r \<in> X ` space M. r * prob (X ` {r} \<inter> space M))"


346 
using assms integral_finite measurable_def


347 
unfolding borel_measurable_def by auto


348 


349 
lemma finite_expectation:


350 
assumes "finite (space M) \<and> random_variable borel_space X"


351 
shows "expectation X = (\<Sum> r \<in> X ` (space M). r * distribution X {r})"


352 
using assms unfolding distribution_def using finite_expectation1 by auto


353 


354 
lemma finite_marginal_product_space_POW:


355 
assumes "Pow (space M) = events"


356 
assumes "random_variable \<lparr> space = X ` (space M), sets = Pow (X ` (space M))\<rparr> X"


357 
assumes "random_variable \<lparr> space = Y ` (space M), sets = Pow (Y ` (space M))\<rparr> Y"


358 
assumes "finite (space M)"


359 
shows "measure_space \<lparr> space = ((X ` (space M)) \<times> (Y ` (space M))),


360 
sets = Pow ((X ` (space M)) \<times> (Y ` (space M))),


361 
measure = (\<lambda>a. prob ((\<lambda>x. (X x,Y x)) ` a \<inter> space M))\<rparr>"


362 
using assms


363 
proof 


364 
let "?S" = "\<lparr> space = ((X ` (space M)) \<times> (Y ` (space M))),


365 
sets = Pow ((X ` (space M)) \<times> (Y ` (space M)))\<rparr>"


366 
let "?M" = "\<lparr> space = ((X ` (space M)) \<times> (Y ` (space M))),


367 
sets = Pow ((X ` (space M)) \<times> (Y ` (space M)))\<rparr>"


368 
have pos: "positive ?S (\<lambda>a. prob ((\<lambda>x. (X x,Y x)) ` a \<inter> space M))"


369 
unfolding positive_def using positive[unfolded positive_def] assms by auto


370 
{ fix x y


371 
have A: "((\<lambda>x. (X x, Y x)) ` x) \<inter> space M \<in> sets M" using assms by auto


372 
have B: "((\<lambda>x. (X x, Y x)) ` y) \<inter> space M \<in> sets M" using assms by auto


373 
assume "x \<inter> y = {}"


374 
from additive[unfolded additive_def, rule_format, OF A B] this


375 
have "prob (((\<lambda>x. (X x, Y x)) ` x \<union>


376 
(\<lambda>x. (X x, Y x)) ` y) \<inter> space M) =


377 
prob ((\<lambda>x. (X x, Y x)) ` x \<inter> space M) +


378 
prob ((\<lambda>x. (X x, Y x)) ` y \<inter> space M)"


379 
apply (subst Int_Un_distrib2)


380 
by auto }


381 
hence add: "additive ?S (\<lambda>a. prob ((\<lambda>x. (X x,Y x)) ` a \<inter> space M))"


382 
unfolding additive_def by auto


383 
interpret S: sigma_algebra "?S"


384 
unfolding sigma_algebra_def algebra_def


385 
sigma_algebra_axioms_def by auto


386 
show ?thesis


387 
using add pos S.finite_additivity_sufficient assms by auto


388 
qed


389 


390 
lemma finite_marginal_product_space_POW2:


391 
assumes "Pow (space M) = events"


392 
assumes "random_variable \<lparr>space = s1, sets = Pow s1\<rparr> X"


393 
assumes "random_variable \<lparr>space = s2, sets = Pow s2\<rparr> Y"


394 
assumes "finite (space M)"


395 
assumes "finite s1" "finite s2"


396 
shows "measure_space \<lparr> space = s1 \<times> s2, sets = Pow (s1 \<times> s2), measure = joint_distribution X Y\<rparr>"


397 
proof 


398 
let "?S" = "\<lparr> space = s1 \<times> s2, sets = Pow (s1 \<times> s2) \<rparr>"


399 
let "?M" = "\<lparr> space = s1 \<times> s2, sets = Pow (s1 \<times> s2), measure = joint_distribution X Y \<rparr>"


400 
have pos: "positive ?S (joint_distribution X Y)" using positive


401 
unfolding positive_def joint_distribution_def using assms by auto


402 
{ fix x y


403 
have A: "((\<lambda>x. (X x, Y x)) ` x) \<inter> space M \<in> sets M" using assms by auto


404 
have B: "((\<lambda>x. (X x, Y x)) ` y) \<inter> space M \<in> sets M" using assms by auto


405 
assume "x \<inter> y = {}"


406 
from additive[unfolded additive_def, rule_format, OF A B] this


407 
have "prob (((\<lambda>x. (X x, Y x)) ` x \<union>


408 
(\<lambda>x. (X x, Y x)) ` y) \<inter> space M) =


409 
prob ((\<lambda>x. (X x, Y x)) ` x \<inter> space M) +


410 
prob ((\<lambda>x. (X x, Y x)) ` y \<inter> space M)"


411 
apply (subst Int_Un_distrib2)


412 
by auto }


413 
hence add: "additive ?S (joint_distribution X Y)"


414 
unfolding additive_def joint_distribution_def by auto


415 
interpret S: sigma_algebra "?S"


416 
unfolding sigma_algebra_def algebra_def


417 
sigma_algebra_axioms_def by auto


418 
show ?thesis


419 
using add pos S.finite_additivity_sufficient assms by auto


420 
qed


421 


422 
lemma prob_x_eq_1_imp_prob_y_eq_0:


423 
assumes "{x} \<in> events"


424 
assumes "(prob {x} = 1)"


425 
assumes "{y} \<in> events"


426 
assumes "y \<noteq> x"


427 
shows "prob {y} = 0"


428 
using prob_one_inter[of "{y}" "{x}"] assms by auto


429 


430 
lemma distribution_x_eq_1_imp_distribution_y_eq_0:


431 
assumes X: "random_variable \<lparr>space = X ` (space M), sets = Pow (X ` (space M))\<rparr> X"


432 
assumes "(distribution X {x} = 1)"


433 
assumes "y \<noteq> x"


434 
shows "distribution X {y} = 0"


435 
proof 


436 
let ?S = "\<lparr>space = X ` (space M), sets = Pow (X ` (space M))\<rparr>"


437 
let ?M = "\<lparr>space = X ` (space M), sets = Pow (X ` (space M)), measure = distribution X\<rparr>"


438 
interpret S: prob_space ?M


439 
using distribution_prob_space[OF X] by auto


440 
{ assume "{x} \<notin> sets ?M"


441 
hence "x \<notin> X ` space M" by auto


442 
hence "X ` {x} \<inter> space M = {}" by auto


443 
hence "distribution X {x} = 0" unfolding distribution_def by auto


444 
hence "False" using assms by auto }


445 
hence x: "{x} \<in> sets ?M" by auto


446 
{ assume "{y} \<notin> sets ?M"


447 
hence "y \<notin> X ` space M" by auto


448 
hence "X ` {y} \<inter> space M = {}" by auto


449 
hence "distribution X {y} = 0" unfolding distribution_def by auto }


450 
moreover


451 
{ assume "{y} \<in> sets ?M"


452 
hence "distribution X {y} = 0" using assms S.prob_x_eq_1_imp_prob_y_eq_0[OF x] by auto }


453 
ultimately show ?thesis by auto


454 
qed


455 


456 
end


457 


458 
end
