src/HOL/Probability/Probability_Space.thy
author hoelzl
Mon, 23 Aug 2010 19:35:57 +0200
changeset 38656 d5d342611edb
parent 36624 25153c08655e
child 39083 e46acc0ea1fe
permissions -rw-r--r--
Rewrite the Probability theory. Introduced pinfreal as real numbers with infinity. Use pinfreal as value for measures. Introduces Lebesgue Measure based on the integral in Multivariate Analysis. Proved Radon Nikodym for arbitrary sigma finite measure spaces.
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
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
     2
imports Lebesgue_Integration
35582
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
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
     5
lemma (in measure_space) measure_inter_full_set:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
     6
  assumes "S \<in> sets M" "T \<in> sets M" and not_\<omega>: "\<mu> (T - S) \<noteq> \<omega>"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
     7
  assumes T: "\<mu> T = \<mu> (space M)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
     8
  shows "\<mu> (S \<inter> T) = \<mu> S"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
     9
proof (rule antisym)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
    10
  show " \<mu> (S \<inter> T) \<le> \<mu> S"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
    11
    using assms by (auto intro!: measure_mono)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
    12
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
    13
  show "\<mu> S \<le> \<mu> (S \<inter> T)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
    14
  proof (rule ccontr)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
    15
    assume contr: "\<not> ?thesis"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
    16
    have "\<mu> (space M) = \<mu> ((T - S) \<union> (S \<inter> T))"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
    17
      unfolding T[symmetric] by (auto intro!: arg_cong[where f="\<mu>"])
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
    18
    also have "\<dots> \<le> \<mu> (T - S) + \<mu> (S \<inter> T)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
    19
      using assms by (auto intro!: measure_subadditive)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
    20
    also have "\<dots> < \<mu> (T - S) + \<mu> S"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
    21
      by (rule pinfreal_less_add[OF not_\<omega>]) (insert contr, auto)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
    22
    also have "\<dots> = \<mu> (T \<union> S)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
    23
      using assms by (subst measure_additive) auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
    24
    also have "\<dots> \<le> \<mu> (space M)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
    25
      using assms sets_into_space by (auto intro!: measure_mono)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
    26
    finally show False ..
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
    27
  qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
    28
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
    29
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
    30
lemma (in finite_measure) finite_measure_inter_full_set:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
    31
  assumes "S \<in> sets M" "T \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
    32
  assumes T: "\<mu> T = \<mu> (space M)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
    33
  shows "\<mu> (S \<inter> T) = \<mu> S"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
    34
  using measure_inter_full_set[OF assms(1,2) finite_measure assms(3)] assms
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
    35
  by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
    36
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
    37
locale prob_space = measure_space +
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
    38
  assumes measure_space_1: "\<mu> (space M) = 1"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
    39
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
    40
sublocale prob_space < finite_measure
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
    41
proof
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
    42
  from measure_space_1 show "\<mu> (space M) \<noteq> \<omega>" by simp
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
    43
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
    44
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
    45
context prob_space
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
    46
begin
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
    47
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
    48
abbreviation "events \<equiv> sets M"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
    49
abbreviation "prob \<equiv> \<lambda>A. real (\<mu> A)"
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
    50
abbreviation "prob_preserving \<equiv> measure_preserving"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
    51
abbreviation "random_variable \<equiv> \<lambda> s X. X \<in> measurable M s"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
    52
abbreviation "expectation \<equiv> integral"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
    53
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
    54
definition
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
    55
  "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
    56
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
    57
definition
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
    58
  "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
    59
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
    60
definition
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
    61
  "distribution X = (\<lambda>s. \<mu> ((X -` s) \<inter> (space M)))"
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
    62
36624
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
    63
abbreviation
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
    64
  "joint_distribution X Y \<equiv> distribution (\<lambda>x. (X x, Y x))"
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
    65
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
    66
lemma prob_space: "prob (space M) = 1"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
    67
  unfolding measure_space_1 by simp
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
    68
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
    69
lemma measure_le_1[simp, intro]:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
    70
  assumes "A \<in> events" shows "\<mu> A \<le> 1"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
    71
proof -
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
    72
  have "\<mu> A \<le> \<mu> (space M)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
    73
    using assms sets_into_space by(auto intro!: measure_mono)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
    74
  also note measure_space_1
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
    75
  finally show ?thesis .
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
    76
qed
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
    77
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
    78
lemma measure_finite[simp, intro]:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
    79
  assumes "A \<in> events" shows "\<mu> A \<noteq> \<omega>"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
    80
  using measure_le_1[OF assms] by auto
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
    81
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
    82
lemma prob_compl:
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
    83
  assumes "A \<in> events"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
    84
  shows "prob (space M - A) = 1 - prob A"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
    85
  using `A \<in> events`[THEN sets_into_space] `A \<in> events` measure_space_1
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
    86
  by (subst real_finite_measure_Diff) auto
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
    87
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
    88
lemma indep_space:
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
    89
  assumes "s \<in> events"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
    90
  shows "indep (space M) s"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
    91
  using assms prob_space by (simp add: indep_def)
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
    92
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
    93
lemma prob_space_increasing: "increasing M prob"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
    94
  by (auto intro!: real_measure_mono simp: increasing_def)
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
    95
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
    96
lemma prob_zero_union:
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
    97
  assumes "s \<in> events" "t \<in> events" "prob t = 0"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
    98
  shows "prob (s \<union> t) = prob s"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
    99
using assms
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   100
proof -
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   101
  have "prob (s \<union> t) \<le> prob s"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   102
    using real_finite_measure_subadditive[of s t] assms by auto
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   103
  moreover have "prob (s \<union> t) \<ge> prob s"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   104
    using assms by (blast intro: real_measure_mono)
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   105
  ultimately show ?thesis by simp
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   106
qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   107
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   108
lemma prob_eq_compl:
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   109
  assumes "s \<in> events" "t \<in> events"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   110
  assumes "prob (space M - s) = prob (space M - t)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   111
  shows "prob s = prob t"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   112
  using assms prob_compl by auto
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   113
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   114
lemma prob_one_inter:
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   115
  assumes events:"s \<in> events" "t \<in> events"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   116
  assumes "prob t = 1"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   117
  shows "prob (s \<inter> t) = prob s"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   118
proof -
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   119
  have "prob ((space M - s) \<union> (space M - t)) = prob (space M - s)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   120
    using events assms  prob_compl[of "t"] by (auto intro!: prob_zero_union)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   121
  also have "(space M - s) \<union> (space M - t) = space M - (s \<inter> t)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   122
    by blast
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   123
  finally show "prob (s \<inter> t) = prob s"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   124
    using events by (auto intro!: prob_eq_compl[of "s \<inter> t" s])
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   125
qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   126
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   127
lemma prob_eq_bigunion_image:
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   128
  assumes "range f \<subseteq> events" "range g \<subseteq> events"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   129
  assumes "disjoint_family f" "disjoint_family g"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   130
  assumes "\<And> n :: nat. prob (f n) = prob (g n)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   131
  shows "(prob (\<Union> i. f i) = prob (\<Union> i. g i))"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   132
using assms
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   133
proof -
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   134
  have a: "(\<lambda> i. prob (f i)) sums (prob (\<Union> i. f i))"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   135
    by (rule real_finite_measure_UNION[OF assms(1,3)])
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   136
  have b: "(\<lambda> i. prob (g i)) sums (prob (\<Union> i. g i))"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   137
    by (rule real_finite_measure_UNION[OF assms(2,4)])
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   138
  show ?thesis using sums_unique[OF b] sums_unique[OF a] assms by simp
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   139
qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   140
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   141
lemma prob_countably_zero:
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   142
  assumes "range c \<subseteq> events"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   143
  assumes "\<And> i. prob (c i) = 0"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   144
  shows "prob (\<Union> i :: nat. c i) = 0"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   145
proof (rule antisym)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   146
  show "prob (\<Union> i :: nat. c i) \<le> 0"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   147
    using real_finite_measurable_countably_subadditive[OF assms(1)]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   148
    by (simp add: assms(2) suminf_zero summable_zero)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   149
  show "0 \<le> prob (\<Union> i :: nat. c i)" by (rule real_pinfreal_nonneg)
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   150
qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   151
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   152
lemma indep_sym:
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   153
   "indep a b \<Longrightarrow> indep b a"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   154
unfolding indep_def using Int_commute[of a b] by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   155
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   156
lemma indep_refl:
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   157
  assumes "a \<in> events"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   158
  shows "indep a a = (prob a = 0) \<or> (prob a = 1)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   159
using assms unfolding indep_def by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   160
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   161
lemma prob_equiprobable_finite_unions:
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   162
  assumes "s \<in> events"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   163
  assumes s_finite: "finite s" "\<And>x. x \<in> s \<Longrightarrow> {x} \<in> events"
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   164
  assumes "\<And> x y. \<lbrakk>x \<in> s; y \<in> s\<rbrakk> \<Longrightarrow> (prob {x} = prob {y})"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   165
  shows "prob s = real (card s) * prob {SOME x. x \<in> s}"
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   166
proof (cases "s = {}")
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   167
  case False hence "\<exists> x. x \<in> s" by blast
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   168
  from someI_ex[OF this] assms
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   169
  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
   170
  have "prob s = (\<Sum> x \<in> s. prob {x})"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   171
    using real_finite_measure_finite_singelton[OF s_finite] by simp
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   172
  also have "\<dots> = (\<Sum> x \<in> s. prob {SOME y. y \<in> s})" using prob_some by auto
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   173
  also have "\<dots> = real (card s) * prob {(SOME x. x \<in> s)}"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   174
    using setsum_constant assms by (simp add: real_eq_of_nat)
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   175
  finally show ?thesis by simp
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   176
qed simp
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   177
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   178
lemma prob_real_sum_image_fn:
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   179
  assumes "e \<in> events"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   180
  assumes "\<And> x. x \<in> s \<Longrightarrow> e \<inter> f x \<in> events"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   181
  assumes "finite s"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   182
  assumes disjoint: "\<And> x y. \<lbrakk>x \<in> s ; y \<in> s ; x \<noteq> y\<rbrakk> \<Longrightarrow> f x \<inter> f y = {}"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   183
  assumes upper: "space M \<subseteq> (\<Union> i \<in> s. f i)"
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   184
  shows "prob e = (\<Sum> x \<in> s. prob (e \<inter> f x))"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   185
proof -
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   186
  have e: "e = (\<Union> i \<in> s. e \<inter> f i)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   187
    using `e \<in> events` sets_into_space upper by blast
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   188
  hence "prob e = prob (\<Union> i \<in> s. e \<inter> f i)" by simp
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   189
  also have "\<dots> = (\<Sum> x \<in> s. prob (e \<inter> f x))"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   190
  proof (rule real_finite_measure_finite_Union)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   191
    show "finite s" by fact
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   192
    show "\<And>i. i \<in> s \<Longrightarrow> e \<inter> f i \<in> events" by fact
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   193
    show "disjoint_family_on (\<lambda>i. e \<inter> f i) s"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   194
      using disjoint by (auto simp: disjoint_family_on_def)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   195
  qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   196
  finally show ?thesis .
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   197
qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   198
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   199
lemma distribution_prob_space:
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   200
  fixes S :: "('c, 'd) algebra_scheme"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   201
  assumes "sigma_algebra S" "random_variable S X"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   202
  shows "prob_space S (distribution X)"
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   203
proof -
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   204
  interpret S: sigma_algebra S by fact
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   205
  show ?thesis
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   206
  proof
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   207
    show "distribution X {} = 0" unfolding distribution_def by simp
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   208
    have "X -` space S \<inter> space M = space M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   209
      using `random_variable S X` by (auto simp: measurable_def)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   210
    then show "distribution X (space S) = 1" using measure_space_1 by (simp add: distribution_def)
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   211
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   212
    show "countably_additive S (distribution X)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   213
    proof (unfold countably_additive_def, safe)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   214
      fix A :: "nat \<Rightarrow> 'c set" assume "range A \<subseteq> sets S" "disjoint_family A"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   215
      hence *: "\<And>i. X -` A i \<inter> space M \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   216
        using `random_variable S X` by (auto simp: measurable_def)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   217
      moreover hence "\<And>i. \<mu> (X -` A i \<inter> space M) \<noteq> \<omega>"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   218
        using finite_measure by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   219
      moreover have "(\<Union>i. X -`  A i \<inter> space M) \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   220
        using * by blast
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   221
      moreover hence "\<mu> (\<Union>i. X -` A i \<inter> space M) \<noteq> \<omega>"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   222
        using finite_measure by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   223
      moreover have **: "disjoint_family (\<lambda>i. X -` A i \<inter> space M)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   224
        using `disjoint_family A` by (auto simp: disjoint_family_on_def)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   225
      ultimately show "(\<Sum>\<^isub>\<infinity> i. distribution X (A i)) = distribution X (\<Union>i. A i)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   226
        using measure_countably_additive[OF _ **]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   227
        by (auto simp: distribution_def Real_real comp_def vimage_UN)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   228
    qed
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   229
  qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   230
qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   231
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   232
lemma distribution_lebesgue_thm1:
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   233
  assumes "random_variable s X"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   234
  assumes "A \<in> sets s"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   235
  shows "real (distribution X A) = expectation (indicator (X -` A \<inter> space M))"
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   236
unfolding distribution_def
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   237
using assms unfolding measurable_def
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   238
using integral_indicator by auto
35582
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 distribution_lebesgue_thm2:
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   241
  assumes "sigma_algebra S" "random_variable S X" and "A \<in> sets S"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   242
  shows "distribution X A =
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   243
    measure_space.positive_integral S (distribution X) (indicator A)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   244
  (is "_ = measure_space.positive_integral _ ?D _")
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   245
proof -
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   246
  interpret S: prob_space S "distribution X" using assms(1,2) by (rule distribution_prob_space)
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   247
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   248
  show ?thesis
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   249
    using S.positive_integral_indicator(1)
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   250
    using assms unfolding distribution_def by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   251
qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   252
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   253
lemma finite_expectation1:
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   254
  assumes "finite (X`space M)" and rv: "random_variable borel_space X"
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   255
  shows "expectation X = (\<Sum> r \<in> X ` space M. r * prob (X -` {r} \<inter> space M))"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   256
proof (rule integral_on_finite(2)[OF assms(2,1)])
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   257
  fix x have "X -` {x} \<inter> space M \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   258
    using rv unfolding measurable_def by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   259
  thus "\<mu> (X -` {x} \<inter> space M) \<noteq> \<omega>" using finite_measure by simp
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   260
qed
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   261
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   262
lemma finite_expectation:
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   263
  assumes "finite (space M)" "random_variable borel_space X"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   264
  shows "expectation X = (\<Sum> r \<in> X ` (space M). r * real (distribution X {r}))"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   265
  using assms unfolding distribution_def using finite_expectation1 by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   266
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   267
lemma prob_x_eq_1_imp_prob_y_eq_0:
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   268
  assumes "{x} \<in> events"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   269
  assumes "prob {x} = 1"
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   270
  assumes "{y} \<in> events"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   271
  assumes "y \<noteq> x"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   272
  shows "prob {y} = 0"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   273
  using prob_one_inter[of "{y}" "{x}"] assms by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   274
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   275
lemma distribution_empty[simp]: "distribution X {} = 0"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   276
  unfolding distribution_def by simp
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   277
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   278
lemma distribution_space[simp]: "distribution X (X ` space M) = 1"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   279
proof -
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   280
  have "X -` X ` space M \<inter> space M = space M" by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   281
  thus ?thesis unfolding distribution_def by (simp add: measure_space_1)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   282
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   283
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   284
lemma distribution_one:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   285
  assumes "random_variable M X" and "A \<in> events"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   286
  shows "distribution X A \<le> 1"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   287
proof -
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   288
  have "distribution X A \<le> \<mu> (space M)" unfolding distribution_def
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   289
    using assms[unfolded measurable_def] by (auto intro!: measure_mono)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   290
  thus ?thesis by (simp add: measure_space_1)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   291
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   292
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   293
lemma distribution_finite:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   294
  assumes "random_variable M X" and "A \<in> events"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   295
  shows "distribution X A \<noteq> \<omega>"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   296
  using distribution_one[OF assms] by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   297
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   298
lemma distribution_x_eq_1_imp_distribution_y_eq_0:
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   299
  assumes X: "random_variable \<lparr>space = X ` (space M), sets = Pow (X ` (space M))\<rparr> X"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   300
    (is "random_variable ?S X")
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   301
  assumes "distribution X {x} = 1"
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   302
  assumes "y \<noteq> x"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   303
  shows "distribution X {y} = 0"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   304
proof -
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   305
  have "sigma_algebra ?S" by (rule sigma_algebra_Pow)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   306
  from distribution_prob_space[OF this X]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   307
  interpret S: prob_space ?S "distribution X" by simp
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   308
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   309
  have x: "{x} \<in> sets ?S"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   310
  proof (rule ccontr)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   311
    assume "{x} \<notin> sets ?S"
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   312
    hence "X -` {x} \<inter> space M = {}" by auto
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   313
    thus "False" using assms unfolding distribution_def by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   314
  qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   315
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   316
  have [simp]: "{y} \<inter> {x} = {}" "{x} - {y} = {x}" using `y \<noteq> x` by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   317
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   318
  show ?thesis
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   319
  proof cases
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   320
    assume "{y} \<in> sets ?S"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   321
    with `{x} \<in> sets ?S` assms show "distribution X {y} = 0"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   322
      using S.measure_inter_full_set[of "{y}" "{x}"]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   323
      by simp
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   324
  next
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   325
    assume "{y} \<notin> sets ?S"
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   326
    hence "X -` {y} \<inter> space M = {}" by auto
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   327
    thus "distribution X {y} = 0" unfolding distribution_def by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   328
  qed
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   329
qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   330
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   331
end
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   332
35977
30d42bfd0174 Added finite measure space.
hoelzl
parents: 35929
diff changeset
   333
locale finite_prob_space = prob_space + finite_measure_space
30d42bfd0174 Added finite measure space.
hoelzl
parents: 35929
diff changeset
   334
36624
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   335
lemma finite_prob_space_eq:
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   336
  "finite_prob_space M \<mu> \<longleftrightarrow> finite_measure_space M \<mu> \<and> \<mu> (space M) = 1"
36624
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   337
  unfolding finite_prob_space_def finite_measure_space_def prob_space_def prob_space_axioms_def
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   338
  by auto
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   339
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   340
lemma (in prob_space) not_empty: "space M \<noteq> {}"
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   341
  using prob_space empty_measure by auto
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   342
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   343
lemma (in finite_prob_space) sum_over_space_eq_1: "(\<Sum>x\<in>space M. \<mu> {x}) = 1"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   344
  using measure_space_1 sum_over_space by simp
36624
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   345
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   346
lemma (in finite_prob_space) positive_distribution: "0 \<le> distribution X x"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   347
  unfolding distribution_def by simp
36624
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   348
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   349
lemma (in finite_prob_space) joint_distribution_restriction_fst:
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   350
  "joint_distribution X Y A \<le> distribution X (fst ` A)"
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   351
  unfolding distribution_def
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   352
proof (safe intro!: measure_mono)
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   353
  fix x assume "x \<in> space M" and *: "(X x, Y x) \<in> A"
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   354
  show "x \<in> X -` fst ` A"
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   355
    by (auto intro!: image_eqI[OF _ *])
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   356
qed (simp_all add: sets_eq_Pow)
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   357
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   358
lemma (in finite_prob_space) joint_distribution_restriction_snd:
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   359
  "joint_distribution X Y A \<le> distribution Y (snd ` A)"
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   360
  unfolding distribution_def
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   361
proof (safe intro!: measure_mono)
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   362
  fix x assume "x \<in> space M" and *: "(X x, Y x) \<in> A"
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   363
  show "x \<in> Y -` snd ` A"
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   364
    by (auto intro!: image_eqI[OF _ *])
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   365
qed (simp_all add: sets_eq_Pow)
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   366
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   367
lemma (in finite_prob_space) distribution_order:
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   368
  shows "0 \<le> distribution X x'"
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   369
  and "(distribution X x' \<noteq> 0) \<longleftrightarrow> (0 < distribution X x')"
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   370
  and "r \<le> joint_distribution X Y {(x, y)} \<Longrightarrow> r \<le> distribution X {x}"
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   371
  and "r \<le> joint_distribution X Y {(x, y)} \<Longrightarrow> r \<le> distribution Y {y}"
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   372
  and "r < joint_distribution X Y {(x, y)} \<Longrightarrow> r < distribution X {x}"
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   373
  and "r < joint_distribution X Y {(x, y)} \<Longrightarrow> r < distribution Y {y}"
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   374
  and "distribution X {x} = 0 \<Longrightarrow> joint_distribution X Y {(x, y)} = 0"
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   375
  and "distribution Y {y} = 0 \<Longrightarrow> joint_distribution X Y {(x, y)} = 0"
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   376
  using positive_distribution[of X x']
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   377
    positive_distribution[of "\<lambda>x. (X x, Y x)" "{(x, y)}"]
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   378
    joint_distribution_restriction_fst[of X Y "{(x, y)}"]
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   379
    joint_distribution_restriction_snd[of X Y "{(x, y)}"]
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   380
  by auto
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   381
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   382
lemma (in finite_prob_space) finite_product_measure_space:
35977
30d42bfd0174 Added finite measure space.
hoelzl
parents: 35929
diff changeset
   383
  assumes "finite s1" "finite s2"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   384
  shows "finite_measure_space \<lparr> space = s1 \<times> s2, sets = Pow (s1 \<times> s2)\<rparr> (joint_distribution X Y)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   385
    (is "finite_measure_space ?M ?D")
35977
30d42bfd0174 Added finite measure space.
hoelzl
parents: 35929
diff changeset
   386
proof (rule finite_Pow_additivity_sufficient)
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   387
  show "positive ?D"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   388
    unfolding positive_def using assms sets_eq_Pow
36624
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   389
    by (simp add: distribution_def)
35977
30d42bfd0174 Added finite measure space.
hoelzl
parents: 35929
diff changeset
   390
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   391
  show "additive ?M ?D" unfolding additive_def
35977
30d42bfd0174 Added finite measure space.
hoelzl
parents: 35929
diff changeset
   392
  proof safe
30d42bfd0174 Added finite measure space.
hoelzl
parents: 35929
diff changeset
   393
    fix x y
30d42bfd0174 Added finite measure space.
hoelzl
parents: 35929
diff changeset
   394
    have A: "((\<lambda>x. (X x, Y x)) -` x) \<inter> space M \<in> sets M" using assms sets_eq_Pow by auto
30d42bfd0174 Added finite measure space.
hoelzl
parents: 35929
diff changeset
   395
    have B: "((\<lambda>x. (X x, Y x)) -` y) \<inter> space M \<in> sets M" using assms sets_eq_Pow by auto
30d42bfd0174 Added finite measure space.
hoelzl
parents: 35929
diff changeset
   396
    assume "x \<inter> y = {}"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   397
    hence "(\<lambda>x. (X x, Y x)) -` x \<inter> space M \<inter> ((\<lambda>x. (X x, Y x)) -` y \<inter> space M) = {}"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   398
      by auto
35977
30d42bfd0174 Added finite measure space.
hoelzl
parents: 35929
diff changeset
   399
    from additive[unfolded additive_def, rule_format, OF A B] this
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   400
      finite_measure[OF A] finite_measure[OF B]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   401
    show "?D (x \<union> y) = ?D x + ?D y"
36624
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   402
      apply (simp add: distribution_def)
35977
30d42bfd0174 Added finite measure space.
hoelzl
parents: 35929
diff changeset
   403
      apply (subst Int_Un_distrib2)
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   404
      by (auto simp: real_of_pinfreal_add)
35977
30d42bfd0174 Added finite measure space.
hoelzl
parents: 35929
diff changeset
   405
  qed
30d42bfd0174 Added finite measure space.
hoelzl
parents: 35929
diff changeset
   406
30d42bfd0174 Added finite measure space.
hoelzl
parents: 35929
diff changeset
   407
  show "finite (space ?M)"
30d42bfd0174 Added finite measure space.
hoelzl
parents: 35929
diff changeset
   408
    using assms by auto
30d42bfd0174 Added finite measure space.
hoelzl
parents: 35929
diff changeset
   409
30d42bfd0174 Added finite measure space.
hoelzl
parents: 35929
diff changeset
   410
  show "sets ?M = Pow (space ?M)"
30d42bfd0174 Added finite measure space.
hoelzl
parents: 35929
diff changeset
   411
    by simp
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   412
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   413
  { fix x assume "x \<in> space ?M" thus "?D {x} \<noteq> \<omega>"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   414
    unfolding distribution_def by (auto intro!: finite_measure simp: sets_eq_Pow) }
35977
30d42bfd0174 Added finite measure space.
hoelzl
parents: 35929
diff changeset
   415
qed
30d42bfd0174 Added finite measure space.
hoelzl
parents: 35929
diff changeset
   416
36624
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   417
lemma (in finite_prob_space) finite_product_measure_space_of_images:
35977
30d42bfd0174 Added finite measure space.
hoelzl
parents: 35929
diff changeset
   418
  shows "finite_measure_space \<lparr> space = X ` space M \<times> Y ` space M,
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   419
                                sets = Pow (X ` space M \<times> Y ` space M) \<rparr>
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   420
                              (joint_distribution X Y)"
36624
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   421
  using finite_space by (auto intro!: finite_product_measure_space)
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   422
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   423
lemma (in finite_prob_space) finite_measure_space:
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   424
  shows "finite_measure_space \<lparr>space = X ` space M, sets = Pow (X ` space M)\<rparr> (distribution X)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   425
    (is "finite_measure_space ?S _")
36624
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   426
proof (rule finite_Pow_additivity_sufficient, simp_all)
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   427
  show "finite (X ` space M)" using finite_space by simp
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   428
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   429
  show "positive (distribution X)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   430
    unfolding distribution_def positive_def using sets_eq_Pow by auto
36624
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   431
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   432
  show "additive ?S (distribution X)" unfolding additive_def distribution_def
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   433
  proof (simp, safe)
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   434
    fix x y
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   435
    have x: "(X -` x) \<inter> space M \<in> sets M"
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   436
      and y: "(X -` y) \<inter> space M \<in> sets M" using sets_eq_Pow by auto
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   437
    assume "x \<inter> y = {}"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   438
    hence "X -` x \<inter> space M \<inter> (X -` y \<inter> space M) = {}" by auto
36624
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   439
    from additive[unfolded additive_def, rule_format, OF x y] this
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   440
      finite_measure[OF x] finite_measure[OF y]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   441
    have "\<mu> (((X -` x) \<union> (X -` y)) \<inter> space M) =
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   442
      \<mu> ((X -` x) \<inter> space M) + \<mu> ((X -` y) \<inter> space M)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   443
      by (subst Int_Un_distrib2) auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   444
    thus "\<mu> ((X -` x \<union> X -` y) \<inter> space M) = \<mu> (X -` x \<inter> space M) + \<mu> (X -` y \<inter> space M)"
36624
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   445
      by auto
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   446
  qed
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   447
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   448
  { fix x assume "x \<in> X ` space M" thus "distribution X {x} \<noteq> \<omega>"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   449
    unfolding distribution_def by (auto intro!: finite_measure simp: sets_eq_Pow) }
36624
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   450
qed
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   451
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   452
lemma (in finite_prob_space) finite_prob_space_of_images:
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   453
  "finite_prob_space \<lparr> space = X ` space M, sets = Pow (X ` space M)\<rparr> (distribution X)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   454
  by (simp add: finite_prob_space_eq finite_measure_space)
36624
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   455
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   456
lemma (in finite_prob_space) finite_product_prob_space_of_images:
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   457
  "finite_prob_space \<lparr> space = X ` space M \<times> Y ` space M, sets = Pow (X ` space M \<times> Y ` space M)\<rparr>
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   458
                     (joint_distribution X Y)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   459
  (is "finite_prob_space ?S _")
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   460
proof (simp add: finite_prob_space_eq finite_product_measure_space_of_images)
36624
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   461
  have "X -` X ` space M \<inter> Y -` Y ` space M \<inter> space M = space M" by auto
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   462
  thus "joint_distribution X Y (X ` space M \<times> Y ` space M) = 1"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   463
    by (simp add: distribution_def prob_space vimage_Times comp_def measure_space_1)
36624
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   464
qed
35977
30d42bfd0174 Added finite measure space.
hoelzl
parents: 35929
diff changeset
   465
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   466
end