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