src/HOL/Probability/Sigma_Algebra.thy
author hoelzl
Wed, 01 Dec 2010 19:20:30 +0100
changeset 40859 de0b30e6c2d2
parent 40702 cf26dd7395e4
child 40869 251df82c0088
permissions -rw-r--r--
Support product spaces on sigma finite measures. Introduce the almost everywhere quantifier. Introduce 'morphism' theorems for most constants. Prove uniqueness of measures on cut stable generators. Prove uniqueness of the Radon-Nikodym derivative. Removed misleading suffix from borel_space and lebesgue_space. Use product spaces to introduce Fubini on the Lebesgue integral. Combine Euclidean_Lebesgue and Lebesgue_Measure. Generalize theorems about mutual information and entropy to arbitrary probability spaces. Remove simproc mult_log as it does not work with interpretations. Introduce completion of measure spaces. Change type of sigma. Introduce dynkin systems.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
33271
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
     1
(*  Title:      Sigma_Algebra.thy
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
     2
    Author:     Stefan Richter, Markus Wenzel, TU Muenchen
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
     3
    Plus material from the Hurd/Coble measure theory development,
33271
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
     4
    translated by Lawrence Paulson.
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
     5
*)
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
     6
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
     7
header {* Sigma Algebras *}
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
     8
39092
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39090
diff changeset
     9
theory Sigma_Algebra imports Main Countable FuncSet Indicator_Function begin
33271
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
    10
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
    11
text {* Sigma algebras are an elementary concept in measure
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
    12
  theory. To measure --- that is to integrate --- functions, we first have
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
    13
  to measure sets. Unfortunately, when dealing with a large universe,
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
    14
  it is often not possible to consistently assign a measure to every
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
    15
  subset. Therefore it is necessary to define the set of measurable
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
    16
  subsets of the universe. A sigma algebra is such a set that has
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
    17
  three very natural and desirable properties. *}
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
    18
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
    19
subsection {* Algebras *}
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
    20
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
    21
record 'a algebra =
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
    22
  space :: "'a set"
33271
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
    23
  sets :: "'a set set"
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
    24
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
    25
locale algebra =
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
    26
  fixes M :: "'a algebra"
33271
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
    27
  assumes space_closed: "sets M \<subseteq> Pow (space M)"
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
    28
     and  empty_sets [iff]: "{} \<in> sets M"
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
    29
     and  compl_sets [intro]: "!!a. a \<in> sets M \<Longrightarrow> space M - a \<in> sets M"
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
    30
     and  Un [intro]: "!!a b. a \<in> sets M \<Longrightarrow> b \<in> sets M \<Longrightarrow> a \<union> b \<in> sets M"
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
    31
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
    32
lemma (in algebra) top [iff]: "space M \<in> sets M"
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
    33
  by (metis Diff_empty compl_sets empty_sets)
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
    34
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
    35
lemma (in algebra) sets_into_space: "x \<in> sets M \<Longrightarrow> x \<subseteq> space M"
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
    36
  by (metis PowD contra_subsetD space_closed)
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
    37
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
    38
lemma (in algebra) Int [intro]:
33271
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
    39
  assumes a: "a \<in> sets M" and b: "b \<in> sets M" shows "a \<inter> b \<in> sets M"
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
    40
proof -
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
    41
  have "((space M - a) \<union> (space M - b)) \<in> sets M"
33271
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
    42
    by (metis a b compl_sets Un)
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
    43
  moreover
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
    44
  have "a \<inter> b = space M - ((space M - a) \<union> (space M - b))"
33271
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
    45
    using space_closed a b
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
    46
    by blast
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
    47
  ultimately show ?thesis
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
    48
    by (metis compl_sets)
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
    49
qed
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
    50
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
    51
lemma (in algebra) Diff [intro]:
33271
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
    52
  assumes a: "a \<in> sets M" and b: "b \<in> sets M" shows "a - b \<in> sets M"
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
    53
proof -
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
    54
  have "(a \<inter> (space M - b)) \<in> sets M"
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
    55
    by (metis a b compl_sets Int)
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
    56
  moreover
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
    57
  have "a - b = (a \<inter> (space M - b))"
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
    58
    by (metis Int_Diff Int_absorb1 Int_commute a sets_into_space)
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
    59
  ultimately show ?thesis
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
    60
    by metis
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
    61
qed
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
    62
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
    63
lemma (in algebra) finite_union [intro]:
33271
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
    64
  "finite X \<Longrightarrow> X \<subseteq> sets M \<Longrightarrow> Union X \<in> sets M"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
    65
  by (induct set: finite) (auto simp add: Un)
33271
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
    66
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
    67
lemma algebra_iff_Int:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
    68
     "algebra M \<longleftrightarrow>
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
    69
       sets M \<subseteq> Pow (space M) & {} \<in> sets M &
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
    70
       (\<forall>a \<in> sets M. space M - a \<in> sets M) &
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
    71
       (\<forall>a \<in> sets M. \<forall> b \<in> sets M. a \<inter> b \<in> sets M)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
    72
proof (auto simp add: algebra.Int, auto simp add: algebra_def)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
    73
  fix a b
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
    74
  assume ab: "sets M \<subseteq> Pow (space M)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
    75
             "\<forall>a\<in>sets M. space M - a \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
    76
             "\<forall>a\<in>sets M. \<forall>b\<in>sets M. a \<inter> b \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
    77
             "a \<in> sets M" "b \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
    78
  hence "a \<union> b = space M - ((space M - a) \<inter> (space M - b))"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
    79
    by blast
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
    80
  also have "... \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
    81
    by (metis ab)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
    82
  finally show "a \<union> b \<in> sets M" .
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
    83
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
    84
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
    85
lemma (in algebra) insert_in_sets:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
    86
  assumes "{x} \<in> sets M" "A \<in> sets M" shows "insert x A \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
    87
proof -
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
    88
  have "{x} \<union> A \<in> sets M" using assms by (rule Un)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
    89
  thus ?thesis by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
    90
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
    91
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
    92
lemma (in algebra) Int_space_eq1 [simp]: "x \<in> sets M \<Longrightarrow> space M \<inter> x = x"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
    93
  by (metis Int_absorb1 sets_into_space)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
    94
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
    95
lemma (in algebra) Int_space_eq2 [simp]: "x \<in> sets M \<Longrightarrow> x \<inter> space M = x"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
    96
  by (metis Int_absorb2 sets_into_space)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
    97
39092
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39090
diff changeset
    98
section {* Restricted algebras *}
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39090
diff changeset
    99
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39090
diff changeset
   100
abbreviation (in algebra)
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39090
diff changeset
   101
  "restricted_space A \<equiv> \<lparr> space = A, sets = (\<lambda>S. (A \<inter> S)) ` sets M \<rparr>"
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39090
diff changeset
   102
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   103
lemma (in algebra) restricted_algebra:
39092
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39090
diff changeset
   104
  assumes "A \<in> sets M" shows "algebra (restricted_space A)"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   105
  using assms by unfold_locales auto
33271
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   106
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   107
subsection {* Sigma Algebras *}
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   108
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   109
locale sigma_algebra = algebra +
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   110
  assumes countable_nat_UN [intro]:
33271
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   111
         "!!A. range A \<subseteq> sets M \<Longrightarrow> (\<Union>i::nat. A i) \<in> sets M"
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   112
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   113
lemma countable_UN_eq:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   114
  fixes A :: "'i::countable \<Rightarrow> 'a set"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   115
  shows "(range A \<subseteq> sets M \<longrightarrow> (\<Union>i. A i) \<in> sets M) \<longleftrightarrow>
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   116
    (range (A \<circ> from_nat) \<subseteq> sets M \<longrightarrow> (\<Union>i. (A \<circ> from_nat) i) \<in> sets M)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   117
proof -
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   118
  let ?A' = "A \<circ> from_nat"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   119
  have *: "(\<Union>i. ?A' i) = (\<Union>i. A i)" (is "?l = ?r")
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   120
  proof safe
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   121
    fix x i assume "x \<in> A i" thus "x \<in> ?l"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   122
      by (auto intro!: exI[of _ "to_nat i"])
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   123
  next
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   124
    fix x i assume "x \<in> ?A' i" thus "x \<in> ?r"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   125
      by (auto intro!: exI[of _ "from_nat i"])
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   126
  qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   127
  have **: "range ?A' = range A"
40702
cf26dd7395e4 Replace surj by abbreviation; remove surj_on.
hoelzl
parents: 39960
diff changeset
   128
    using surj_from_nat
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   129
    by (auto simp: image_compose intro!: imageI)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   130
  show ?thesis unfolding * ** ..
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   131
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   132
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   133
lemma (in sigma_algebra) countable_UN[intro]:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   134
  fixes A :: "'i::countable \<Rightarrow> 'a set"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   135
  assumes "A`X \<subseteq> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   136
  shows  "(\<Union>x\<in>X. A x) \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   137
proof -
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   138
  let "?A i" = "if i \<in> X then A i else {}"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   139
  from assms have "range ?A \<subseteq> sets M" by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   140
  with countable_nat_UN[of "?A \<circ> from_nat"] countable_UN_eq[of ?A M]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   141
  have "(\<Union>x. ?A x) \<in> sets M" by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   142
  moreover have "(\<Union>x. ?A x) = (\<Union>x\<in>X. A x)" by (auto split: split_if_asm)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   143
  ultimately show ?thesis by simp
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   144
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   145
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   146
lemma (in sigma_algebra) finite_UN:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   147
  assumes "finite I" and "\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   148
  shows "(\<Union>i\<in>I. A i) \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   149
  using assms by induct auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   150
33533
40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas
paulson
parents: 33271
diff changeset
   151
lemma (in sigma_algebra) countable_INT [intro]:
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   152
  fixes A :: "'i::countable \<Rightarrow> 'a set"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   153
  assumes A: "A`X \<subseteq> sets M" "X \<noteq> {}"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   154
  shows "(\<Inter>i\<in>X. A i) \<in> sets M"
33271
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   155
proof -
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   156
  from A have "\<forall>i\<in>X. A i \<in> sets M" by fast
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   157
  hence "space M - (\<Union>i\<in>X. space M - A i) \<in> sets M" by blast
33271
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   158
  moreover
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   159
  have "(\<Inter>i\<in>X. A i) = space M - (\<Union>i\<in>X. space M - A i)" using space_closed A
33271
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   160
    by blast
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   161
  ultimately show ?thesis by metis
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   162
qed
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   163
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   164
lemma (in sigma_algebra) finite_INT:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   165
  assumes "finite I" "I \<noteq> {}" "\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   166
  shows "(\<Inter>i\<in>I. A i) \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   167
  using assms by (induct rule: finite_ne_induct) auto
33271
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   168
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   169
lemma algebra_Pow:
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   170
     "algebra \<lparr> space = sp, sets = Pow sp, \<dots> = X \<rparr>"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   171
  by (auto simp add: algebra_def)
33271
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   172
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   173
lemma sigma_algebra_Pow:
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   174
     "sigma_algebra \<lparr> space = sp, sets = Pow sp, \<dots> = X \<rparr>"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   175
  by (auto simp add: sigma_algebra_def sigma_algebra_axioms_def algebra_Pow)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   176
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   177
lemma sigma_algebra_iff:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   178
     "sigma_algebra M \<longleftrightarrow>
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   179
      algebra M \<and> (\<forall>A. range A \<subseteq> sets M \<longrightarrow> (\<Union>i::nat. A i) \<in> sets M)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   180
  by (simp add: sigma_algebra_def sigma_algebra_axioms_def)
33271
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   181
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   182
subsection {* Binary Unions *}
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   183
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   184
definition binary :: "'a \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a"
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   185
  where "binary a b =  (\<lambda>\<^isup>x. b)(0 := a)"
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   186
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   187
lemma range_binary_eq: "range(binary a b) = {a,b}"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   188
  by (auto simp add: binary_def)
33271
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   189
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   190
lemma Un_range_binary: "a \<union> b = (\<Union>i::nat. binary a b i)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   191
  by (simp add: UNION_eq_Union_image range_binary_eq)
33271
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   192
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   193
lemma Int_range_binary: "a \<inter> b = (\<Inter>i::nat. binary a b i)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   194
  by (simp add: INTER_eq_Inter_image range_binary_eq)
33271
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   195
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   196
lemma sigma_algebra_iff2:
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   197
     "sigma_algebra M \<longleftrightarrow>
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   198
       sets M \<subseteq> Pow (space M) \<and>
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   199
       {} \<in> sets M \<and> (\<forall>s \<in> sets M. space M - s \<in> sets M) \<and>
33271
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   200
       (\<forall>A. range A \<subseteq> sets M \<longrightarrow> (\<Union>i::nat. A i) \<in> sets M)"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   201
  by (auto simp add: range_binary_eq sigma_algebra_def sigma_algebra_axioms_def
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   202
         algebra_def Un_range_binary)
33271
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   203
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   204
subsection {* Initial Sigma Algebra *}
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   205
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   206
text {*Sigma algebras can naturally be created as the closure of any set of
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   207
  sets with regard to the properties just postulated.  *}
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   208
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   209
inductive_set
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   210
  sigma_sets :: "'a set \<Rightarrow> 'a set set \<Rightarrow> 'a set set"
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   211
  for sp :: "'a set" and A :: "'a set set"
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   212
  where
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   213
    Basic: "a \<in> A \<Longrightarrow> a \<in> sigma_sets sp A"
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   214
  | Empty: "{} \<in> sigma_sets sp A"
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   215
  | Compl: "a \<in> sigma_sets sp A \<Longrightarrow> sp - a \<in> sigma_sets sp A"
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   216
  | Union: "(\<And>i::nat. a i \<in> sigma_sets sp A) \<Longrightarrow> (\<Union>i. a i) \<in> sigma_sets sp A"
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   217
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   218
definition
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   219
  "sigma M = (| space = space M, sets = sigma_sets (space M) (sets M) |)"
33271
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   220
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   221
lemma sets_sigma: "sets (sigma M) = sigma_sets (space M) (sets M)"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   222
  unfolding sigma_def by simp
33271
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   223
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   224
lemma space_sigma [simp]: "space (sigma M) = space M"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   225
  by (simp add: sigma_def)
33271
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   226
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   227
lemma sigma_sets_top: "sp \<in> sigma_sets sp A"
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   228
  by (metis Diff_empty sigma_sets.Compl sigma_sets.Empty)
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   229
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   230
lemma sigma_sets_into_sp: "A \<subseteq> Pow sp \<Longrightarrow> x \<in> sigma_sets sp A \<Longrightarrow> x \<subseteq> sp"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   231
  by (erule sigma_sets.induct, auto)
33271
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   232
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   233
lemma sigma_sets_Un:
33271
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   234
  "a \<in> sigma_sets sp A \<Longrightarrow> b \<in> sigma_sets sp A \<Longrightarrow> a \<union> b \<in> sigma_sets sp A"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   235
apply (simp add: Un_range_binary range_binary_eq)
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   236
apply (rule Union, simp add: binary_def)
33271
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   237
done
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   238
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   239
lemma sigma_sets_Inter:
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   240
  assumes Asb: "A \<subseteq> Pow sp"
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   241
  shows "(\<And>i::nat. a i \<in> sigma_sets sp A) \<Longrightarrow> (\<Inter>i. a i) \<in> sigma_sets sp A"
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   242
proof -
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   243
  assume ai: "\<And>i::nat. a i \<in> sigma_sets sp A"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   244
  hence "\<And>i::nat. sp-(a i) \<in> sigma_sets sp A"
33271
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   245
    by (rule sigma_sets.Compl)
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   246
  hence "(\<Union>i. sp-(a i)) \<in> sigma_sets sp A"
33271
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   247
    by (rule sigma_sets.Union)
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   248
  hence "sp-(\<Union>i. sp-(a i)) \<in> sigma_sets sp A"
33271
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   249
    by (rule sigma_sets.Compl)
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   250
  also have "sp-(\<Union>i. sp-(a i)) = sp Int (\<Inter>i. a i)"
33271
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   251
    by auto
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   252
  also have "... = (\<Inter>i. a i)" using ai
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   253
    by (blast dest: sigma_sets_into_sp [OF Asb])
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   254
  finally show ?thesis .
33271
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   255
qed
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   256
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   257
lemma sigma_sets_INTER:
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   258
  assumes Asb: "A \<subseteq> Pow sp"
33271
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   259
      and ai: "\<And>i::nat. i \<in> S \<Longrightarrow> a i \<in> sigma_sets sp A" and non: "S \<noteq> {}"
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   260
  shows "(\<Inter>i\<in>S. a i) \<in> sigma_sets sp A"
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   261
proof -
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   262
  from ai have "\<And>i. (if i\<in>S then a i else sp) \<in> sigma_sets sp A"
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   263
    by (simp add: sigma_sets.intros sigma_sets_top)
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   264
  hence "(\<Inter>i. (if i\<in>S then a i else sp)) \<in> sigma_sets sp A"
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   265
    by (rule sigma_sets_Inter [OF Asb])
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   266
  also have "(\<Inter>i. (if i\<in>S then a i else sp)) = (\<Inter>i\<in>S. a i)"
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   267
    by auto (metis ai non sigma_sets_into_sp subset_empty subset_iff Asb)+
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   268
  finally show ?thesis .
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   269
qed
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   270
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   271
lemma (in sigma_algebra) sigma_sets_subset:
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   272
  assumes a: "a \<subseteq> sets M"
33271
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   273
  shows "sigma_sets (space M) a \<subseteq> sets M"
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   274
proof
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   275
  fix x
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   276
  assume "x \<in> sigma_sets (space M) a"
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   277
  from this show "x \<in> sets M"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   278
    by (induct rule: sigma_sets.induct, auto) (metis a subsetD)
33271
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   279
qed
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   280
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   281
lemma (in sigma_algebra) sigma_sets_eq:
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   282
     "sigma_sets (space M) (sets M) = sets M"
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   283
proof
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   284
  show "sets M \<subseteq> sigma_sets (space M) (sets M)"
37032
58a0757031dd speed up some proofs and fix some warnings
huffman
parents: 33536
diff changeset
   285
    by (metis Set.subsetI sigma_sets.Basic)
33271
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   286
  next
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   287
  show "sigma_sets (space M) (sets M) \<subseteq> sets M"
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   288
    by (metis sigma_sets_subset subset_refl)
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   289
qed
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   290
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   291
lemma sigma_algebra_sigma_sets:
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   292
     "a \<subseteq> Pow (space M) \<Longrightarrow> sets M = sigma_sets (space M) a \<Longrightarrow> sigma_algebra M"
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   293
  apply (auto simp add: sigma_algebra_def sigma_algebra_axioms_def
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   294
      algebra_def sigma_sets.Empty sigma_sets.Compl sigma_sets_Un)
33271
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   295
  apply (blast dest: sigma_sets_into_sp)
37032
58a0757031dd speed up some proofs and fix some warnings
huffman
parents: 33536
diff changeset
   296
  apply (rule sigma_sets.Union, fast)
33271
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   297
  done
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   298
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   299
lemma sigma_algebra_sigma:
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   300
    "sets M \<subseteq> Pow (space M) \<Longrightarrow> sigma_algebra (sigma M)"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   301
  apply (rule sigma_algebra_sigma_sets)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   302
  apply (auto simp add: sigma_def)
33271
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   303
  done
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   304
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   305
lemma (in sigma_algebra) sigma_subset:
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   306
    "sets N \<subseteq> sets M \<Longrightarrow> space N = space M \<Longrightarrow> sets (sigma N) \<subseteq> (sets M)"
33271
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   307
  by (simp add: sigma_def sigma_sets_subset)
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents:
diff changeset
   308
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   309
lemma sigma_sets_least_sigma_algebra:
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   310
  assumes "A \<subseteq> Pow S"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   311
  shows "sigma_sets S A = \<Inter>{B. A \<subseteq> B \<and> sigma_algebra \<lparr>space = S, sets = B\<rparr>}"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   312
proof safe
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   313
  fix B X assume "A \<subseteq> B" and sa: "sigma_algebra \<lparr> space = S, sets = B \<rparr>"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   314
    and X: "X \<in> sigma_sets S A"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   315
  from sigma_algebra.sigma_sets_subset[OF sa, simplified, OF `A \<subseteq> B`] X
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   316
  show "X \<in> B" by auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   317
next
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   318
  fix X assume "X \<in> \<Inter>{B. A \<subseteq> B \<and> sigma_algebra \<lparr>space = S, sets = B\<rparr>}"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   319
  then have [intro!]: "\<And>B. A \<subseteq> B \<Longrightarrow> sigma_algebra \<lparr>space = S, sets = B\<rparr> \<Longrightarrow> X \<in> B"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   320
     by simp
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   321
  have "A \<subseteq> sigma_sets S A" using assms
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   322
    by (auto intro!: sigma_sets.Basic)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   323
  moreover have "sigma_algebra \<lparr>space = S, sets = sigma_sets S A\<rparr>"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   324
    using assms by (intro sigma_algebra_sigma_sets[of A]) auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   325
  ultimately show "X \<in> sigma_sets S A" by auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   326
qed
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   327
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   328
lemma (in sigma_algebra) restriction_in_sets:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   329
  fixes A :: "nat \<Rightarrow> 'a set"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   330
  assumes "S \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   331
  and *: "range A \<subseteq> (\<lambda>A. S \<inter> A) ` sets M" (is "_ \<subseteq> ?r")
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   332
  shows "range A \<subseteq> sets M" "(\<Union>i. A i) \<in> (\<lambda>A. S \<inter> A) ` sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   333
proof -
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   334
  { fix i have "A i \<in> ?r" using * by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   335
    hence "\<exists>B. A i = B \<inter> S \<and> B \<in> sets M" by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   336
    hence "A i \<subseteq> S" "A i \<in> sets M" using `S \<in> sets M` by auto }
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   337
  thus "range A \<subseteq> sets M" "(\<Union>i. A i) \<in> (\<lambda>A. S \<inter> A) ` sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   338
    by (auto intro!: image_eqI[of _ _ "(\<Union>i. A i)"])
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   339
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   340
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   341
lemma (in sigma_algebra) restricted_sigma_algebra:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   342
  assumes "S \<in> sets M"
39092
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39090
diff changeset
   343
  shows "sigma_algebra (restricted_space S)"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   344
  unfolding sigma_algebra_def sigma_algebra_axioms_def
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   345
proof safe
39092
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39090
diff changeset
   346
  show "algebra (restricted_space S)" using restricted_algebra[OF assms] .
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   347
next
39092
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39090
diff changeset
   348
  fix A :: "nat \<Rightarrow> 'a set" assume "range A \<subseteq> sets (restricted_space S)"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   349
  from restriction_in_sets[OF assms this[simplified]]
39092
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39090
diff changeset
   350
  show "(\<Union>i. A i) \<in> sets (restricted_space S)" by simp
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   351
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   352
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   353
lemma sigma_sets_Int:
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   354
  assumes "A \<in> sigma_sets sp st"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   355
  shows "op \<inter> A ` sigma_sets sp st = sigma_sets (A \<inter> sp) (op \<inter> A ` st)"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   356
proof (intro equalityI subsetI)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   357
  fix x assume "x \<in> op \<inter> A ` sigma_sets sp st"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   358
  then obtain y where "y \<in> sigma_sets sp st" "x = y \<inter> A" by auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   359
  then show "x \<in> sigma_sets (A \<inter> sp) (op \<inter> A ` st)"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   360
  proof (induct arbitrary: x)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   361
    case (Compl a)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   362
    then show ?case
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   363
      by (force intro!: sigma_sets.Compl simp: Diff_Int_distrib ac_simps)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   364
  next
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   365
    case (Union a)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   366
    then show ?case
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   367
      by (auto intro!: sigma_sets.Union
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   368
               simp add: UN_extend_simps simp del: UN_simps)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   369
  qed (auto intro!: sigma_sets.intros)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   370
next
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   371
  fix x assume "x \<in> sigma_sets (A \<inter> sp) (op \<inter> A ` st)"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   372
  then show "x \<in> op \<inter> A ` sigma_sets sp st"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   373
  proof induct
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   374
    case (Compl a)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   375
    then obtain x where "a = A \<inter> x" "x \<in> sigma_sets sp st" by auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   376
    then show ?case
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   377
      by (force simp add: image_iff intro!: bexI[of _ "sp - x"] sigma_sets.Compl)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   378
  next
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   379
    case (Union a)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   380
    then have "\<forall>i. \<exists>x. x \<in> sigma_sets sp st \<and> a i = A \<inter> x"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   381
      by (auto simp: image_iff Bex_def)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   382
    from choice[OF this] guess f ..
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   383
    then show ?case
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   384
      by (auto intro!: bexI[of _ "(\<Union>x. f x)"] sigma_sets.Union
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   385
               simp add: image_iff)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   386
  qed (auto intro!: sigma_sets.intros)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   387
qed
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   388
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   389
lemma sigma_sets_single[simp]: "sigma_sets {X} {{X}} = {{}, {X}}"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   390
proof (intro set_eqI iffI)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   391
  fix x assume "x \<in> sigma_sets {X} {{X}}"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   392
  from sigma_sets_into_sp[OF _ this]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   393
  show "x \<in> {{}, {X}}" by auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   394
next
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   395
  fix x assume "x \<in> {{}, {X}}"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   396
  then show "x \<in> sigma_sets {X} {{X}}"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   397
    by (auto intro: sigma_sets.Empty sigma_sets_top)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   398
qed
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   399
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   400
section {* Measurable functions *}
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   401
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   402
definition
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   403
  "measurable A B = {f \<in> space A -> space B. \<forall>y \<in> sets B. f -` y \<inter> space A \<in> sets A}"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   404
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   405
lemma (in sigma_algebra) measurable_sigma:
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   406
  assumes B: "sets N \<subseteq> Pow (space N)"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   407
      and f: "f \<in> space M -> space N"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   408
      and ba: "\<And>y. y \<in> sets N \<Longrightarrow> (f -` y) \<inter> space M \<in> sets M"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   409
  shows "f \<in> measurable M (sigma N)"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   410
proof -
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   411
  have "sigma_sets (space N) (sets N) \<subseteq> {y . (f -` y) \<inter> space M \<in> sets M & y \<subseteq> space N}"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   412
    proof clarify
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   413
      fix x
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   414
      assume "x \<in> sigma_sets (space N) (sets N)"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   415
      thus "f -` x \<inter> space M \<in> sets M \<and> x \<subseteq> space N"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   416
        proof induct
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   417
          case (Basic a)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   418
          thus ?case
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   419
            by (auto simp add: ba) (metis B subsetD PowD)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   420
        next
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   421
          case Empty
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   422
          thus ?case
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   423
            by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   424
        next
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   425
          case (Compl a)
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   426
          have [simp]: "f -` space N \<inter> space M = space M"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   427
            by (auto simp add: funcset_mem [OF f])
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   428
          thus ?case
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   429
            by (auto simp add: vimage_Diff Diff_Int_distrib2 compl_sets Compl)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   430
        next
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   431
          case (Union a)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   432
          thus ?case
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   433
            by (simp add: vimage_UN, simp only: UN_extend_simps(4)) blast
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   434
        qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   435
    qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   436
  thus ?thesis
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   437
    by (simp add: measurable_def sigma_algebra_axioms sigma_algebra_sigma B f)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   438
       (auto simp add: sigma_def)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   439
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   440
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   441
lemma measurable_cong:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   442
  assumes "\<And> w. w \<in> space M \<Longrightarrow> f w = g w"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   443
  shows "f \<in> measurable M M' \<longleftrightarrow> g \<in> measurable M M'"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   444
  unfolding measurable_def using assms
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   445
  by (simp cong: vimage_inter_cong Pi_cong)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   446
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   447
lemma measurable_space:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   448
  "f \<in> measurable M A \<Longrightarrow> x \<in> space M \<Longrightarrow> f x \<in> space A"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   449
   unfolding measurable_def by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   450
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   451
lemma measurable_sets:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   452
  "f \<in> measurable M A \<Longrightarrow> S \<in> sets A \<Longrightarrow> f -` S \<inter> space M \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   453
   unfolding measurable_def by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   454
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   455
lemma (in sigma_algebra) measurable_subset:
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   456
     "(\<And>S. S \<in> sets A \<Longrightarrow> S \<subseteq> space A) \<Longrightarrow> measurable M A \<subseteq> measurable M (sigma A)"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   457
  by (auto intro: measurable_sigma measurable_sets measurable_space)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   458
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   459
lemma measurable_eqI:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   460
     "\<lbrakk> space m1 = space m1' ; space m2 = space m2' ;
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   461
        sets m1 = sets m1' ; sets m2 = sets m2' \<rbrakk>
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   462
      \<Longrightarrow> measurable m1 m2 = measurable m1' m2'"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   463
  by (simp add: measurable_def sigma_algebra_iff2)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   464
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   465
lemma (in sigma_algebra) measurable_const[intro, simp]:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   466
  assumes "c \<in> space M'"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   467
  shows "(\<lambda>x. c) \<in> measurable M M'"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   468
  using assms by (auto simp add: measurable_def)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   469
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   470
lemma (in sigma_algebra) measurable_If:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   471
  assumes measure: "f \<in> measurable M M'" "g \<in> measurable M M'"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   472
  assumes P: "{x\<in>space M. P x} \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   473
  shows "(\<lambda>x. if P x then f x else g x) \<in> measurable M M'"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   474
  unfolding measurable_def
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   475
proof safe
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   476
  fix x assume "x \<in> space M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   477
  thus "(if P x then f x else g x) \<in> space M'"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   478
    using measure unfolding measurable_def by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   479
next
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   480
  fix A assume "A \<in> sets M'"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   481
  hence *: "(\<lambda>x. if P x then f x else g x) -` A \<inter> space M =
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   482
    ((f -` A \<inter> space M) \<inter> {x\<in>space M. P x}) \<union>
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   483
    ((g -` A \<inter> space M) \<inter> (space M - {x\<in>space M. P x}))"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   484
    using measure unfolding measurable_def by (auto split: split_if_asm)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   485
  show "(\<lambda>x. if P x then f x else g x) -` A \<inter> space M \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   486
    using `A \<in> sets M'` measure P unfolding * measurable_def
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   487
    by (auto intro!: Un)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   488
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   489
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   490
lemma (in sigma_algebra) measurable_If_set:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   491
  assumes measure: "f \<in> measurable M M'" "g \<in> measurable M M'"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   492
  assumes P: "A \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   493
  shows "(\<lambda>x. if x \<in> A then f x else g x) \<in> measurable M M'"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   494
proof (rule measurable_If[OF measure])
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   495
  have "{x \<in> space M. x \<in> A} = A" using `A \<in> sets M` sets_into_space by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   496
  thus "{x \<in> space M. x \<in> A} \<in> sets M" using `A \<in> sets M` by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   497
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   498
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   499
lemma (in algebra) measurable_ident[intro, simp]: "id \<in> measurable M M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   500
  by (auto simp add: measurable_def)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   501
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   502
lemma measurable_comp[intro]:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   503
  fixes f :: "'a \<Rightarrow> 'b" and g :: "'b \<Rightarrow> 'c"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   504
  shows "f \<in> measurable a b \<Longrightarrow> g \<in> measurable b c \<Longrightarrow> (g o f) \<in> measurable a c"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   505
  apply (auto simp add: measurable_def vimage_compose)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   506
  apply (subgoal_tac "f -` g -` y \<inter> space a = f -` (g -` y \<inter> space b) \<inter> space a")
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   507
  apply force+
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   508
  done
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   509
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   510
lemma measurable_strong:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   511
  fixes f :: "'a \<Rightarrow> 'b" and g :: "'b \<Rightarrow> 'c"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   512
  assumes f: "f \<in> measurable a b" and g: "g \<in> (space b -> space c)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   513
      and a: "sigma_algebra a" and b: "sigma_algebra b" and c: "sigma_algebra c"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   514
      and t: "f ` (space a) \<subseteq> t"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   515
      and cb: "\<And>s. s \<in> sets c \<Longrightarrow> (g -` s) \<inter> t \<in> sets b"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   516
  shows "(g o f) \<in> measurable a c"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   517
proof -
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   518
  have fab: "f \<in> (space a -> space b)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   519
   and ba: "\<And>y. y \<in> sets b \<Longrightarrow> (f -` y) \<inter> (space a) \<in> sets a" using f
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   520
     by (auto simp add: measurable_def)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   521
  have eq: "f -` g -` y \<inter> space a = f -` (g -` y \<inter> t) \<inter> space a" using t
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   522
    by force
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   523
  show ?thesis
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   524
    apply (auto simp add: measurable_def vimage_compose a c)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   525
    apply (metis funcset_mem fab g)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   526
    apply (subst eq, metis ba cb)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   527
    done
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   528
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   529
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   530
lemma measurable_mono1:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   531
     "a \<subseteq> b \<Longrightarrow> sigma_algebra \<lparr>space = X, sets = b\<rparr>
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   532
      \<Longrightarrow> measurable \<lparr>space = X, sets = a\<rparr> c \<subseteq> measurable \<lparr>space = X, sets = b\<rparr> c"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   533
  by (auto simp add: measurable_def)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   534
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   535
lemma measurable_up_sigma:
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   536
  "measurable A M \<subseteq> measurable (sigma A) M"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   537
  unfolding measurable_def
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   538
  by (auto simp: sigma_def intro: sigma_sets.Basic)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   539
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   540
lemma (in sigma_algebra) measurable_range_reduce:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   541
   "\<lbrakk> f \<in> measurable M \<lparr>space = s, sets = Pow s\<rparr> ; s \<noteq> {} \<rbrakk>
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   542
    \<Longrightarrow> f \<in> measurable M \<lparr>space = s \<inter> (f ` space M), sets = Pow (s \<inter> (f ` space M))\<rparr>"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   543
  by (simp add: measurable_def sigma_algebra_Pow del: Pow_Int_eq) blast
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   544
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   545
lemma (in sigma_algebra) measurable_Pow_to_Pow:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   546
   "(sets M = Pow (space M)) \<Longrightarrow> f \<in> measurable M \<lparr>space = UNIV, sets = Pow UNIV\<rparr>"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   547
  by (auto simp add: measurable_def sigma_algebra_def sigma_algebra_axioms_def algebra_def)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   548
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   549
lemma (in sigma_algebra) measurable_Pow_to_Pow_image:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   550
   "sets M = Pow (space M)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   551
    \<Longrightarrow> f \<in> measurable M \<lparr>space = f ` space M, sets = Pow (f ` space M)\<rparr>"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   552
  by (simp add: measurable_def sigma_algebra_Pow) intro_locales
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   553
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   554
lemma (in sigma_algebra) measurable_iff_sigma:
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   555
  assumes "sets E \<subseteq> Pow (space E)" and "f \<in> space M \<rightarrow> space E"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   556
  shows "f \<in> measurable M (sigma E) \<longleftrightarrow> (\<forall>A\<in>sets E. f -` A \<inter> space M \<in> sets M)"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   557
  using measurable_sigma[OF assms]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   558
  by (fastsimp simp: measurable_def sets_sigma intro: sigma_sets.intros)
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   559
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   560
section "Disjoint families"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   561
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   562
definition
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   563
  disjoint_family_on  where
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   564
  "disjoint_family_on A S \<longleftrightarrow> (\<forall>m\<in>S. \<forall>n\<in>S. m \<noteq> n \<longrightarrow> A m \<inter> A n = {})"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   565
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   566
abbreviation
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   567
  "disjoint_family A \<equiv> disjoint_family_on A UNIV"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   568
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   569
lemma range_subsetD: "range f \<subseteq> B \<Longrightarrow> f i \<in> B"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   570
  by blast
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   571
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   572
lemma Int_Diff_disjoint: "A \<inter> B \<inter> (A - B) = {}"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   573
  by blast
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   574
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   575
lemma Int_Diff_Un: "A \<inter> B \<union> (A - B) = A"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   576
  by blast
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   577
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   578
lemma disjoint_family_subset:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   579
     "disjoint_family A \<Longrightarrow> (!!x. B x \<subseteq> A x) \<Longrightarrow> disjoint_family B"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   580
  by (force simp add: disjoint_family_on_def)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   581
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   582
lemma disjoint_family_on_bisimulation:
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   583
  assumes "disjoint_family_on f S"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   584
  and "\<And>n m. n \<in> S \<Longrightarrow> m \<in> S \<Longrightarrow> n \<noteq> m \<Longrightarrow> f n \<inter> f m = {} \<Longrightarrow> g n \<inter> g m = {}"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   585
  shows "disjoint_family_on g S"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   586
  using assms unfolding disjoint_family_on_def by auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   587
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   588
lemma disjoint_family_on_mono:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   589
  "A \<subseteq> B \<Longrightarrow> disjoint_family_on f B \<Longrightarrow> disjoint_family_on f A"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   590
  unfolding disjoint_family_on_def by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   591
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   592
lemma disjoint_family_Suc:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   593
  assumes Suc: "!!n. A n \<subseteq> A (Suc n)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   594
  shows "disjoint_family (\<lambda>i. A (Suc i) - A i)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   595
proof -
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   596
  {
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   597
    fix m
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   598
    have "!!n. A n \<subseteq> A (m+n)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   599
    proof (induct m)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   600
      case 0 show ?case by simp
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   601
    next
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   602
      case (Suc m) thus ?case
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   603
        by (metis Suc_eq_plus1 assms nat_add_commute nat_add_left_commute subset_trans)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   604
    qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   605
  }
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   606
  hence "!!m n. m < n \<Longrightarrow> A m \<subseteq> A n"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   607
    by (metis add_commute le_add_diff_inverse nat_less_le)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   608
  thus ?thesis
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   609
    by (auto simp add: disjoint_family_on_def)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   610
      (metis insert_absorb insert_subset le_SucE le_antisym not_leE)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   611
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   612
39092
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39090
diff changeset
   613
lemma setsum_indicator_disjoint_family:
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39090
diff changeset
   614
  fixes f :: "'d \<Rightarrow> 'e::semiring_1"
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39090
diff changeset
   615
  assumes d: "disjoint_family_on A P" and "x \<in> A j" and "finite P" and "j \<in> P"
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39090
diff changeset
   616
  shows "(\<Sum>i\<in>P. f i * indicator (A i) x) = f j"
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39090
diff changeset
   617
proof -
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39090
diff changeset
   618
  have "P \<inter> {i. x \<in> A i} = {j}"
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39090
diff changeset
   619
    using d `x \<in> A j` `j \<in> P` unfolding disjoint_family_on_def
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39090
diff changeset
   620
    by auto
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39090
diff changeset
   621
  thus ?thesis
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39090
diff changeset
   622
    unfolding indicator_def
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39090
diff changeset
   623
    by (simp add: if_distrib setsum_cases[OF `finite P`])
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39090
diff changeset
   624
qed
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39090
diff changeset
   625
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   626
definition disjointed :: "(nat \<Rightarrow> 'a set) \<Rightarrow> nat \<Rightarrow> 'a set "
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   627
  where "disjointed A n = A n - (\<Union>i\<in>{0..<n}. A i)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   628
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   629
lemma finite_UN_disjointed_eq: "(\<Union>i\<in>{0..<n}. disjointed A i) = (\<Union>i\<in>{0..<n}. A i)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   630
proof (induct n)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   631
  case 0 show ?case by simp
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   632
next
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   633
  case (Suc n)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   634
  thus ?case by (simp add: atLeastLessThanSuc disjointed_def)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   635
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   636
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   637
lemma UN_disjointed_eq: "(\<Union>i. disjointed A i) = (\<Union>i. A i)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   638
  apply (rule UN_finite2_eq [where k=0])
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   639
  apply (simp add: finite_UN_disjointed_eq)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   640
  done
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   641
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   642
lemma less_disjoint_disjointed: "m<n \<Longrightarrow> disjointed A m \<inter> disjointed A n = {}"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   643
  by (auto simp add: disjointed_def)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   644
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   645
lemma disjoint_family_disjointed: "disjoint_family (disjointed A)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   646
  by (simp add: disjoint_family_on_def)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   647
     (metis neq_iff Int_commute less_disjoint_disjointed)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   648
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   649
lemma disjointed_subset: "disjointed A n \<subseteq> A n"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   650
  by (auto simp add: disjointed_def)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   651
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   652
lemma (in algebra) UNION_in_sets:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   653
  fixes A:: "nat \<Rightarrow> 'a set"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   654
  assumes A: "range A \<subseteq> sets M "
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   655
  shows  "(\<Union>i\<in>{0..<n}. A i) \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   656
proof (induct n)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   657
  case 0 show ?case by simp
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   658
next
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   659
  case (Suc n)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   660
  thus ?case
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   661
    by (simp add: atLeastLessThanSuc) (metis A Un UNIV_I image_subset_iff)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   662
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   663
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   664
lemma (in algebra) range_disjointed_sets:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   665
  assumes A: "range A \<subseteq> sets M "
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   666
  shows  "range (disjointed A) \<subseteq> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   667
proof (auto simp add: disjointed_def)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   668
  fix n
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   669
  show "A n - (\<Union>i\<in>{0..<n}. A i) \<in> sets M" using UNION_in_sets
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   670
    by (metis A Diff UNIV_I image_subset_iff)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   671
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   672
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   673
lemma sigma_algebra_disjoint_iff:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   674
     "sigma_algebra M \<longleftrightarrow>
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   675
      algebra M &
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   676
      (\<forall>A. range A \<subseteq> sets M \<longrightarrow> disjoint_family A \<longrightarrow>
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   677
           (\<Union>i::nat. A i) \<in> sets M)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   678
proof (auto simp add: sigma_algebra_iff)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   679
  fix A :: "nat \<Rightarrow> 'a set"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   680
  assume M: "algebra M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   681
     and A: "range A \<subseteq> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   682
     and UnA: "\<forall>A. range A \<subseteq> sets M \<longrightarrow>
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   683
               disjoint_family A \<longrightarrow> (\<Union>i::nat. A i) \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   684
  hence "range (disjointed A) \<subseteq> sets M \<longrightarrow>
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   685
         disjoint_family (disjointed A) \<longrightarrow>
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   686
         (\<Union>i. disjointed A i) \<in> sets M" by blast
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   687
  hence "(\<Union>i. disjointed A i) \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   688
    by (simp add: algebra.range_disjointed_sets M A disjoint_family_disjointed)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   689
  thus "(\<Union>i::nat. A i) \<in> sets M" by (simp add: UN_disjointed_eq)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   690
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   691
39090
a2d38b8b693e Introduced sigma algebra generated by function preimages.
hoelzl
parents: 38656
diff changeset
   692
subsection {* Sigma algebra generated by function preimages *}
a2d38b8b693e Introduced sigma algebra generated by function preimages.
hoelzl
parents: 38656
diff changeset
   693
a2d38b8b693e Introduced sigma algebra generated by function preimages.
hoelzl
parents: 38656
diff changeset
   694
definition (in sigma_algebra)
a2d38b8b693e Introduced sigma algebra generated by function preimages.
hoelzl
parents: 38656
diff changeset
   695
  "vimage_algebra S f = \<lparr> space = S, sets = (\<lambda>A. f -` A \<inter> S) ` sets M \<rparr>"
a2d38b8b693e Introduced sigma algebra generated by function preimages.
hoelzl
parents: 38656
diff changeset
   696
a2d38b8b693e Introduced sigma algebra generated by function preimages.
hoelzl
parents: 38656
diff changeset
   697
lemma (in sigma_algebra) in_vimage_algebra[simp]:
a2d38b8b693e Introduced sigma algebra generated by function preimages.
hoelzl
parents: 38656
diff changeset
   698
  "A \<in> sets (vimage_algebra S f) \<longleftrightarrow> (\<exists>B\<in>sets M. A = f -` B \<inter> S)"
a2d38b8b693e Introduced sigma algebra generated by function preimages.
hoelzl
parents: 38656
diff changeset
   699
  by (simp add: vimage_algebra_def image_iff)
a2d38b8b693e Introduced sigma algebra generated by function preimages.
hoelzl
parents: 38656
diff changeset
   700
a2d38b8b693e Introduced sigma algebra generated by function preimages.
hoelzl
parents: 38656
diff changeset
   701
lemma (in sigma_algebra) space_vimage_algebra[simp]:
a2d38b8b693e Introduced sigma algebra generated by function preimages.
hoelzl
parents: 38656
diff changeset
   702
  "space (vimage_algebra S f) = S"
a2d38b8b693e Introduced sigma algebra generated by function preimages.
hoelzl
parents: 38656
diff changeset
   703
  by (simp add: vimage_algebra_def)
a2d38b8b693e Introduced sigma algebra generated by function preimages.
hoelzl
parents: 38656
diff changeset
   704
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   705
lemma (in sigma_algebra) sigma_algebra_preimages:
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   706
  fixes f :: "'x \<Rightarrow> 'a"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   707
  assumes "f \<in> A \<rightarrow> space M"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   708
  shows "sigma_algebra \<lparr> space = A, sets = (\<lambda>M. f -` M \<inter> A) ` sets M \<rparr>"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   709
    (is "sigma_algebra \<lparr> space = _, sets = ?F ` sets M \<rparr>")
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   710
proof (simp add: sigma_algebra_iff2, safe)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   711
  show "{} \<in> ?F ` sets M" by blast
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   712
next
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   713
  fix S assume "S \<in> sets M"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   714
  moreover have "A - ?F S = ?F (space M - S)"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   715
    using assms by auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   716
  ultimately show "A - ?F S \<in> ?F ` sets M"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   717
    by blast
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   718
next
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   719
  fix S :: "nat \<Rightarrow> 'x set" assume *: "range S \<subseteq> ?F ` sets M"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   720
  have "\<forall>i. \<exists>b. b \<in> sets M \<and> S i = ?F b"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   721
  proof safe
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   722
    fix i
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   723
    have "S i \<in> ?F ` sets M" using * by auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   724
    then show "\<exists>b. b \<in> sets M \<and> S i = ?F b" by auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   725
  qed
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   726
  from choice[OF this] obtain b where b: "range b \<subseteq> sets M" "\<And>i. S i = ?F (b i)"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   727
    by auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   728
  then have "(\<Union>i. S i) = ?F (\<Union>i. b i)" by auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   729
  then show "(\<Union>i. S i) \<in> ?F ` sets M" using b(1) by blast
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   730
qed
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   731
39090
a2d38b8b693e Introduced sigma algebra generated by function preimages.
hoelzl
parents: 38656
diff changeset
   732
lemma (in sigma_algebra) sigma_algebra_vimage:
a2d38b8b693e Introduced sigma algebra generated by function preimages.
hoelzl
parents: 38656
diff changeset
   733
  fixes S :: "'c set" assumes "f \<in> S \<rightarrow> space M"
a2d38b8b693e Introduced sigma algebra generated by function preimages.
hoelzl
parents: 38656
diff changeset
   734
  shows "sigma_algebra (vimage_algebra S f)"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   735
proof -
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   736
  from sigma_algebra_preimages[OF assms]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   737
  show ?thesis unfolding vimage_algebra_def by (auto simp: sigma_algebra_iff2)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   738
qed
39090
a2d38b8b693e Introduced sigma algebra generated by function preimages.
hoelzl
parents: 38656
diff changeset
   739
a2d38b8b693e Introduced sigma algebra generated by function preimages.
hoelzl
parents: 38656
diff changeset
   740
lemma (in sigma_algebra) measurable_vimage_algebra:
a2d38b8b693e Introduced sigma algebra generated by function preimages.
hoelzl
parents: 38656
diff changeset
   741
  fixes S :: "'c set" assumes "f \<in> S \<rightarrow> space M"
a2d38b8b693e Introduced sigma algebra generated by function preimages.
hoelzl
parents: 38656
diff changeset
   742
  shows "f \<in> measurable (vimage_algebra S f) M"
a2d38b8b693e Introduced sigma algebra generated by function preimages.
hoelzl
parents: 38656
diff changeset
   743
    unfolding measurable_def using assms by force
a2d38b8b693e Introduced sigma algebra generated by function preimages.
hoelzl
parents: 38656
diff changeset
   744
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   745
lemma (in sigma_algebra) measurable_vimage:
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   746
  fixes g :: "'a \<Rightarrow> 'c" and f :: "'d \<Rightarrow> 'a"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   747
  assumes "g \<in> measurable M M2" "f \<in> S \<rightarrow> space M"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   748
  shows "(\<lambda>x. g (f x)) \<in> measurable (vimage_algebra S f) M2"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   749
proof -
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   750
  note measurable_vimage_algebra[OF assms(2)]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   751
  from measurable_comp[OF this assms(1)]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   752
  show ?thesis by (simp add: comp_def)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   753
qed
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   754
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   755
lemma (in sigma_algebra) vimage_vimage_inv:
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   756
  assumes f: "bij_betw f S (space M)"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   757
  assumes [simp]: "\<And>x. x \<in> space M \<Longrightarrow> f (g x) = x" and g: "g \<in> space M \<rightarrow> S"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   758
  shows "sigma_algebra.vimage_algebra (vimage_algebra S f) (space M) g = M"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   759
proof -
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   760
  interpret T: sigma_algebra "vimage_algebra S f"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   761
    using f by (safe intro!: sigma_algebra_vimage bij_betw_imp_funcset)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   762
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   763
  have inj: "inj_on f S" and [simp]: "f`S = space M"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   764
    using f unfolding bij_betw_def by auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   765
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   766
  { fix A assume A: "A \<in> sets M"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   767
    have "g -` f -` A \<inter> g -` S \<inter> space M = (f \<circ> g) -` A \<inter> space M"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   768
      using g by auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   769
    also have "\<dots> = A"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   770
      using `A \<in> sets M`[THEN sets_into_space] by auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   771
    finally have "g -` f -` A \<inter> g -` S \<inter> space M = A" . }
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   772
  note X = this
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   773
  show ?thesis
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   774
    unfolding T.vimage_algebra_def unfolding vimage_algebra_def
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   775
    by (simp add: image_compose[symmetric] comp_def X cong: image_cong)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   776
qed
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   777
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   778
lemma (in sigma_algebra) measurable_vimage_iff:
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   779
  fixes f :: "'b \<Rightarrow> 'a" assumes f: "bij_betw f S (space M)"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   780
  shows "g \<in> measurable M M' \<longleftrightarrow> (g \<circ> f) \<in> measurable (vimage_algebra S f) M'"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   781
proof
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   782
  assume "g \<in> measurable M M'"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   783
  from measurable_vimage[OF this f[THEN bij_betw_imp_funcset]]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   784
  show "(g \<circ> f) \<in> measurable (vimage_algebra S f) M'" unfolding comp_def .
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   785
next
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   786
  interpret v: sigma_algebra "vimage_algebra S f"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   787
    using f[THEN bij_betw_imp_funcset] by (rule sigma_algebra_vimage)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   788
  note f' = f[THEN bij_betw_the_inv_into]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   789
  assume "g \<circ> f \<in> measurable (vimage_algebra S f) M'"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   790
  from v.measurable_vimage[OF this, unfolded space_vimage_algebra, OF f'[THEN bij_betw_imp_funcset]]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   791
  show "g \<in> measurable M M'"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   792
    using f f'[THEN bij_betw_imp_funcset] f[unfolded bij_betw_def]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   793
    by (subst (asm) vimage_vimage_inv)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   794
       (simp_all add: f_the_inv_into_f cong: measurable_cong)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   795
qed
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   796
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   797
lemma (in sigma_algebra) measurable_vimage_iff_inv:
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   798
  fixes f :: "'b \<Rightarrow> 'a" assumes f: "bij_betw f S (space M)"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   799
  shows "g \<in> measurable (vimage_algebra S f) M' \<longleftrightarrow> (g \<circ> the_inv_into S f) \<in> measurable M M'"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   800
  unfolding measurable_vimage_iff[OF f]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   801
  using f[unfolded bij_betw_def]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   802
  by (auto intro!: measurable_cong simp add: the_inv_into_f_f)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   803
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   804
lemma sigma_sets_vimage:
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   805
  assumes "f \<in> S' \<rightarrow> S" and "A \<subseteq> Pow S"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   806
  shows "sigma_sets S' ((\<lambda>X. f -` X \<inter> S') ` A) = (\<lambda>X. f -` X \<inter> S') ` sigma_sets S A"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   807
proof (intro set_eqI iffI)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   808
  let ?F = "\<lambda>X. f -` X \<inter> S'"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   809
  fix X assume "X \<in> sigma_sets S' (?F ` A)"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   810
  then show "X \<in> ?F ` sigma_sets S A"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   811
  proof induct
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   812
    case (Basic X) then obtain X' where "X = ?F X'" "X' \<in> A"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   813
      by auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   814
    then show ?case by (auto intro!: sigma_sets.Basic)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   815
  next
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   816
    case Empty then show ?case
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   817
      by (auto intro!: image_eqI[of _ _ "{}"] sigma_sets.Empty)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   818
  next
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   819
    case (Compl X) then obtain X' where X: "X = ?F X'" and "X' \<in> sigma_sets S A"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   820
      by auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   821
    then have "S - X' \<in> sigma_sets S A"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   822
      by (auto intro!: sigma_sets.Compl)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   823
    then show ?case
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   824
      using X assms by (auto intro!: image_eqI[where x="S - X'"])
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   825
  next
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   826
    case (Union F)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   827
    then have "\<forall>i. \<exists>F'.  F' \<in> sigma_sets S A \<and> F i = f -` F' \<inter> S'"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   828
      by (auto simp: image_iff Bex_def)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   829
    from choice[OF this] obtain F' where
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   830
      "\<And>i. F' i \<in> sigma_sets S A" and "\<And>i. F i = f -` F' i \<inter> S'"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   831
      by auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   832
    then show ?case
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   833
      by (auto intro!: sigma_sets.Union image_eqI[where x="\<Union>i. F' i"])
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   834
  qed
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   835
next
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   836
  let ?F = "\<lambda>X. f -` X \<inter> S'"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   837
  fix X assume "X \<in> ?F ` sigma_sets S A"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   838
  then obtain X' where "X' \<in> sigma_sets S A" "X = ?F X'" by auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   839
  then show "X \<in> sigma_sets S' (?F ` A)"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   840
  proof (induct arbitrary: X)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   841
    case (Basic X') then show ?case by (auto intro: sigma_sets.Basic)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   842
  next
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   843
    case Empty then show ?case by (auto intro: sigma_sets.Empty)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   844
  next
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   845
    case (Compl X')
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   846
    have "S' - (S' - X) \<in> sigma_sets S' (?F ` A)"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   847
      apply (rule sigma_sets.Compl)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   848
      using assms by (auto intro!: Compl.hyps simp: Compl.prems)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   849
    also have "S' - (S' - X) = X"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   850
      using assms Compl by auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   851
    finally show ?case .
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   852
  next
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   853
    case (Union F)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   854
    have "(\<Union>i. f -` F i \<inter> S') \<in> sigma_sets S' (?F ` A)"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   855
      by (intro sigma_sets.Union Union.hyps) simp
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   856
    also have "(\<Union>i. f -` F i \<inter> S') = X"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   857
      using assms Union by auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   858
    finally show ?case .
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   859
  qed
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   860
qed
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
   861
39092
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39090
diff changeset
   862
section {* Conditional space *}
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39090
diff changeset
   863
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39090
diff changeset
   864
definition (in algebra)
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39090
diff changeset
   865
  "image_space X = \<lparr> space = X`space M, sets = (\<lambda>S. X`S) ` sets M \<rparr>"
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39090
diff changeset
   866
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39090
diff changeset
   867
definition (in algebra)
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39090
diff changeset
   868
  "conditional_space X A = algebra.image_space (restricted_space A) X"
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39090
diff changeset
   869
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39090
diff changeset
   870
lemma (in algebra) space_conditional_space:
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39090
diff changeset
   871
  assumes "A \<in> sets M" shows "space (conditional_space X A) = X`A"
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39090
diff changeset
   872
proof -
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39090
diff changeset
   873
  interpret r: algebra "restricted_space A" using assms by (rule restricted_algebra)
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39090
diff changeset
   874
  show ?thesis unfolding conditional_space_def r.image_space_def
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39090
diff changeset
   875
    by simp
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39090
diff changeset
   876
qed
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39090
diff changeset
   877
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   878
subsection {* A Two-Element Series *}
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   879
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   880
definition binaryset :: "'a set \<Rightarrow> 'a set \<Rightarrow> nat \<Rightarrow> 'a set "
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   881
  where "binaryset A B = (\<lambda>\<^isup>x. {})(0 := A, Suc 0 := B)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   882
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   883
lemma range_binaryset_eq: "range(binaryset A B) = {A,B,{}}"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   884
  apply (simp add: binaryset_def)
39302
d7728f65b353 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents: 39092
diff changeset
   885
  apply (rule set_eqI)
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   886
  apply (auto simp add: image_iff)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   887
  done
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   888
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   889
lemma UN_binaryset_eq: "(\<Union>i. binaryset A B i) = A \<union> B"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   890
  by (simp add: UNION_eq_Union_image range_binaryset_eq)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   891
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   892
section {* Closed CDI *}
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   893
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   894
definition
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   895
  closed_cdi  where
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   896
  "closed_cdi M \<longleftrightarrow>
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   897
   sets M \<subseteq> Pow (space M) &
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   898
   (\<forall>s \<in> sets M. space M - s \<in> sets M) &
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   899
   (\<forall>A. (range A \<subseteq> sets M) & (A 0 = {}) & (\<forall>n. A n \<subseteq> A (Suc n)) \<longrightarrow>
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   900
        (\<Union>i. A i) \<in> sets M) &
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   901
   (\<forall>A. (range A \<subseteq> sets M) & disjoint_family A \<longrightarrow> (\<Union>i::nat. A i) \<in> sets M)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   902
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   903
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   904
inductive_set
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   905
  smallest_ccdi_sets :: "('a, 'b) algebra_scheme \<Rightarrow> 'a set set"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   906
  for M
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   907
  where
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   908
    Basic [intro]:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   909
      "a \<in> sets M \<Longrightarrow> a \<in> smallest_ccdi_sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   910
  | Compl [intro]:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   911
      "a \<in> smallest_ccdi_sets M \<Longrightarrow> space M - a \<in> smallest_ccdi_sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   912
  | Inc:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   913
      "range A \<in> Pow(smallest_ccdi_sets M) \<Longrightarrow> A 0 = {} \<Longrightarrow> (\<And>n. A n \<subseteq> A (Suc n))
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   914
       \<Longrightarrow> (\<Union>i. A i) \<in> smallest_ccdi_sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   915
  | Disj:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   916
      "range A \<in> Pow(smallest_ccdi_sets M) \<Longrightarrow> disjoint_family A
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   917
       \<Longrightarrow> (\<Union>i::nat. A i) \<in> smallest_ccdi_sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   918
  monos Pow_mono
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   919
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   920
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   921
definition
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   922
  smallest_closed_cdi  where
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   923
  "smallest_closed_cdi M = (|space = space M, sets = smallest_ccdi_sets M|)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   924
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   925
lemma space_smallest_closed_cdi [simp]:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   926
     "space (smallest_closed_cdi M) = space M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   927
  by (simp add: smallest_closed_cdi_def)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   928
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   929
lemma (in algebra) smallest_closed_cdi1: "sets M \<subseteq> sets (smallest_closed_cdi M)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   930
  by (auto simp add: smallest_closed_cdi_def)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   931
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   932
lemma (in algebra) smallest_ccdi_sets:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   933
     "smallest_ccdi_sets M \<subseteq> Pow (space M)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   934
  apply (rule subsetI)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   935
  apply (erule smallest_ccdi_sets.induct)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   936
  apply (auto intro: range_subsetD dest: sets_into_space)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   937
  done
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   938
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   939
lemma (in algebra) smallest_closed_cdi2: "closed_cdi (smallest_closed_cdi M)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   940
  apply (auto simp add: closed_cdi_def smallest_closed_cdi_def smallest_ccdi_sets)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   941
  apply (blast intro: smallest_ccdi_sets.Inc smallest_ccdi_sets.Disj) +
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   942
  done
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   943
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   944
lemma (in algebra) smallest_closed_cdi3:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   945
     "sets (smallest_closed_cdi M) \<subseteq> Pow (space M)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   946
  by (simp add: smallest_closed_cdi_def smallest_ccdi_sets)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   947
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   948
lemma closed_cdi_subset: "closed_cdi M \<Longrightarrow> sets M \<subseteq> Pow (space M)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   949
  by (simp add: closed_cdi_def)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   950
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   951
lemma closed_cdi_Compl: "closed_cdi M \<Longrightarrow> s \<in> sets M \<Longrightarrow> space M - s \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   952
  by (simp add: closed_cdi_def)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   953
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   954
lemma closed_cdi_Inc:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   955
     "closed_cdi M \<Longrightarrow> range A \<subseteq> sets M \<Longrightarrow> A 0 = {} \<Longrightarrow> (!!n. A n \<subseteq> A (Suc n)) \<Longrightarrow>
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   956
        (\<Union>i. A i) \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   957
  by (simp add: closed_cdi_def)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   958
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   959
lemma closed_cdi_Disj:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   960
     "closed_cdi M \<Longrightarrow> range A \<subseteq> sets M \<Longrightarrow> disjoint_family A \<Longrightarrow> (\<Union>i::nat. A i) \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   961
  by (simp add: closed_cdi_def)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   962
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   963
lemma closed_cdi_Un:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   964
  assumes cdi: "closed_cdi M" and empty: "{} \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   965
      and A: "A \<in> sets M" and B: "B \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   966
      and disj: "A \<inter> B = {}"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   967
    shows "A \<union> B \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   968
proof -
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   969
  have ra: "range (binaryset A B) \<subseteq> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   970
   by (simp add: range_binaryset_eq empty A B)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   971
 have di:  "disjoint_family (binaryset A B)" using disj
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   972
   by (simp add: disjoint_family_on_def binaryset_def Int_commute)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   973
 from closed_cdi_Disj [OF cdi ra di]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   974
 show ?thesis
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   975
   by (simp add: UN_binaryset_eq)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   976
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   977
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   978
lemma (in algebra) smallest_ccdi_sets_Un:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   979
  assumes A: "A \<in> smallest_ccdi_sets M" and B: "B \<in> smallest_ccdi_sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   980
      and disj: "A \<inter> B = {}"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   981
    shows "A \<union> B \<in> smallest_ccdi_sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   982
proof -
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   983
  have ra: "range (binaryset A B) \<in> Pow (smallest_ccdi_sets M)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   984
    by (simp add: range_binaryset_eq  A B smallest_ccdi_sets.Basic)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   985
  have di:  "disjoint_family (binaryset A B)" using disj
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   986
    by (simp add: disjoint_family_on_def binaryset_def Int_commute)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   987
  from Disj [OF ra di]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   988
  show ?thesis
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   989
    by (simp add: UN_binaryset_eq)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   990
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   991
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   992
lemma (in algebra) smallest_ccdi_sets_Int1:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   993
  assumes a: "a \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   994
  shows "b \<in> smallest_ccdi_sets M \<Longrightarrow> a \<inter> b \<in> smallest_ccdi_sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   995
proof (induct rule: smallest_ccdi_sets.induct)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   996
  case (Basic x)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   997
  thus ?case
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   998
    by (metis a Int smallest_ccdi_sets.Basic)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
   999
next
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1000
  case (Compl x)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1001
  have "a \<inter> (space M - x) = space M - ((space M - a) \<union> (a \<inter> x))"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1002
    by blast
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1003
  also have "... \<in> smallest_ccdi_sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1004
    by (metis smallest_ccdi_sets.Compl a Compl(2) Diff_Int2 Diff_Int_distrib2
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1005
           Diff_disjoint Int_Diff Int_empty_right Un_commute
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1006
           smallest_ccdi_sets.Basic smallest_ccdi_sets.Compl
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1007
           smallest_ccdi_sets_Un)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1008
  finally show ?case .
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1009
next
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1010
  case (Inc A)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1011
  have 1: "(\<Union>i. (\<lambda>i. a \<inter> A i) i) = a \<inter> (\<Union>i. A i)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1012
    by blast
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1013
  have "range (\<lambda>i. a \<inter> A i) \<in> Pow(smallest_ccdi_sets M)" using Inc
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1014
    by blast
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1015
  moreover have "(\<lambda>i. a \<inter> A i) 0 = {}"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1016
    by (simp add: Inc)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1017
  moreover have "!!n. (\<lambda>i. a \<inter> A i) n \<subseteq> (\<lambda>i. a \<inter> A i) (Suc n)" using Inc
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1018
    by blast
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1019
  ultimately have 2: "(\<Union>i. (\<lambda>i. a \<inter> A i) i) \<in> smallest_ccdi_sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1020
    by (rule smallest_ccdi_sets.Inc)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1021
  show ?case
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1022
    by (metis 1 2)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1023
next
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1024
  case (Disj A)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1025
  have 1: "(\<Union>i. (\<lambda>i. a \<inter> A i) i) = a \<inter> (\<Union>i. A i)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1026
    by blast
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1027
  have "range (\<lambda>i. a \<inter> A i) \<in> Pow(smallest_ccdi_sets M)" using Disj
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1028
    by blast
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1029
  moreover have "disjoint_family (\<lambda>i. a \<inter> A i)" using Disj
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1030
    by (auto simp add: disjoint_family_on_def)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1031
  ultimately have 2: "(\<Union>i. (\<lambda>i. a \<inter> A i) i) \<in> smallest_ccdi_sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1032
    by (rule smallest_ccdi_sets.Disj)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1033
  show ?case
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1034
    by (metis 1 2)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1035
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1036
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1037
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1038
lemma (in algebra) smallest_ccdi_sets_Int:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1039
  assumes b: "b \<in> smallest_ccdi_sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1040
  shows "a \<in> smallest_ccdi_sets M \<Longrightarrow> a \<inter> b \<in> smallest_ccdi_sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1041
proof (induct rule: smallest_ccdi_sets.induct)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1042
  case (Basic x)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1043
  thus ?case
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1044
    by (metis b smallest_ccdi_sets_Int1)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1045
next
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1046
  case (Compl x)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1047
  have "(space M - x) \<inter> b = space M - (x \<inter> b \<union> (space M - b))"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1048
    by blast
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1049
  also have "... \<in> smallest_ccdi_sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1050
    by (metis Compl(2) Diff_disjoint Int_Diff Int_commute Int_empty_right b
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1051
           smallest_ccdi_sets.Compl smallest_ccdi_sets_Un)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1052
  finally show ?case .
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1053
next
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1054
  case (Inc A)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1055
  have 1: "(\<Union>i. (\<lambda>i. A i \<inter> b) i) = (\<Union>i. A i) \<inter> b"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1056
    by blast
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1057
  have "range (\<lambda>i. A i \<inter> b) \<in> Pow(smallest_ccdi_sets M)" using Inc
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1058
    by blast
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1059
  moreover have "(\<lambda>i. A i \<inter> b) 0 = {}"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1060
    by (simp add: Inc)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1061
  moreover have "!!n. (\<lambda>i. A i \<inter> b) n \<subseteq> (\<lambda>i. A i \<inter> b) (Suc n)" using Inc
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1062
    by blast
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1063
  ultimately have 2: "(\<Union>i. (\<lambda>i. A i \<inter> b) i) \<in> smallest_ccdi_sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1064
    by (rule smallest_ccdi_sets.Inc)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1065
  show ?case
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1066
    by (metis 1 2)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1067
next
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1068
  case (Disj A)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1069
  have 1: "(\<Union>i. (\<lambda>i. A i \<inter> b) i) = (\<Union>i. A i) \<inter> b"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1070
    by blast
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1071
  have "range (\<lambda>i. A i \<inter> b) \<in> Pow(smallest_ccdi_sets M)" using Disj
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1072
    by blast
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1073
  moreover have "disjoint_family (\<lambda>i. A i \<inter> b)" using Disj
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1074
    by (auto simp add: disjoint_family_on_def)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1075
  ultimately have 2: "(\<Union>i. (\<lambda>i. A i \<inter> b) i) \<in> smallest_ccdi_sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1076
    by (rule smallest_ccdi_sets.Disj)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1077
  show ?case
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1078
    by (metis 1 2)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1079
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1080
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1081
lemma (in algebra) sets_smallest_closed_cdi_Int:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1082
   "a \<in> sets (smallest_closed_cdi M) \<Longrightarrow> b \<in> sets (smallest_closed_cdi M)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1083
    \<Longrightarrow> a \<inter> b \<in> sets (smallest_closed_cdi M)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1084
  by (simp add: smallest_ccdi_sets_Int smallest_closed_cdi_def)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1085
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1086
lemma (in algebra) sigma_property_disjoint_lemma:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1087
  assumes sbC: "sets M \<subseteq> C"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1088
      and ccdi: "closed_cdi (|space = space M, sets = C|)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1089
  shows "sigma_sets (space M) (sets M) \<subseteq> C"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1090
proof -
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1091
  have "smallest_ccdi_sets M \<in> {B . sets M \<subseteq> B \<and> sigma_algebra (|space = space M, sets = B|)}"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1092
    apply (auto simp add: sigma_algebra_disjoint_iff algebra_iff_Int
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1093
            smallest_ccdi_sets_Int)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1094
    apply (metis Union_Pow_eq Union_upper subsetD smallest_ccdi_sets)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1095
    apply (blast intro: smallest_ccdi_sets.Disj)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1096
    done
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1097
  hence "sigma_sets (space M) (sets M) \<subseteq> smallest_ccdi_sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1098
    by clarsimp
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1099
       (drule sigma_algebra.sigma_sets_subset [where a="sets M"], auto)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1100
  also have "...  \<subseteq> C"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1101
    proof
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1102
      fix x
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1103
      assume x: "x \<in> smallest_ccdi_sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1104
      thus "x \<in> C"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1105
        proof (induct rule: smallest_ccdi_sets.induct)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1106
          case (Basic x)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1107
          thus ?case
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1108
            by (metis Basic subsetD sbC)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1109
        next
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1110
          case (Compl x)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1111
          thus ?case
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1112
            by (blast intro: closed_cdi_Compl [OF ccdi, simplified])
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1113
        next
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1114
          case (Inc A)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1115
          thus ?case
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1116
               by (auto intro: closed_cdi_Inc [OF ccdi, simplified])
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1117
        next
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1118
          case (Disj A)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1119
          thus ?case
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1120
               by (auto intro: closed_cdi_Disj [OF ccdi, simplified])
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1121
        qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1122
    qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1123
  finally show ?thesis .
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1124
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1125
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1126
lemma (in algebra) sigma_property_disjoint:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1127
  assumes sbC: "sets M \<subseteq> C"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1128
      and compl: "!!s. s \<in> C \<inter> sigma_sets (space M) (sets M) \<Longrightarrow> space M - s \<in> C"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1129
      and inc: "!!A. range A \<subseteq> C \<inter> sigma_sets (space M) (sets M)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1130
                     \<Longrightarrow> A 0 = {} \<Longrightarrow> (!!n. A n \<subseteq> A (Suc n))
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1131
                     \<Longrightarrow> (\<Union>i. A i) \<in> C"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1132
      and disj: "!!A. range A \<subseteq> C \<inter> sigma_sets (space M) (sets M)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1133
                      \<Longrightarrow> disjoint_family A \<Longrightarrow> (\<Union>i::nat. A i) \<in> C"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1134
  shows "sigma_sets (space M) (sets M) \<subseteq> C"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1135
proof -
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1136
  have "sigma_sets (space M) (sets M) \<subseteq> C \<inter> sigma_sets (space M) (sets M)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1137
    proof (rule sigma_property_disjoint_lemma)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1138
      show "sets M \<subseteq> C \<inter> sigma_sets (space M) (sets M)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1139
        by (metis Int_greatest Set.subsetI sbC sigma_sets.Basic)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1140
    next
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1141
      show "closed_cdi \<lparr>space = space M, sets = C \<inter> sigma_sets (space M) (sets M)\<rparr>"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1142
        by (simp add: closed_cdi_def compl inc disj)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1143
           (metis PowI Set.subsetI le_infI2 sigma_sets_into_sp space_closed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1144
             IntE sigma_sets.Compl range_subsetD sigma_sets.Union)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1145
    qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1146
  thus ?thesis
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1147
    by blast
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1148
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 37032
diff changeset
  1149
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1150
section {* Dynkin systems *}
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1151
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1152
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1153
locale dynkin_system =
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1154
  fixes M :: "'a algebra"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1155
  assumes space_closed: "sets M \<subseteq> Pow (space M)"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1156
    and   space: "space M \<in> sets M"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1157
    and   compl[intro!]: "\<And>A. A \<in> sets M \<Longrightarrow> space M - A \<in> sets M"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1158
    and   UN[intro!]: "\<And>A. disjoint_family A \<Longrightarrow> range A \<subseteq> sets M
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1159
                           \<Longrightarrow> (\<Union>i::nat. A i) \<in> sets M"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1160
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1161
lemma (in dynkin_system) sets_into_space: "\<And> A. A \<in> sets M \<Longrightarrow> A \<subseteq> space M"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1162
  using space_closed by auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1163
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1164
lemma (in dynkin_system) empty[intro, simp]: "{} \<in> sets M"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1165
  using space compl[of "space M"] by simp
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1166
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1167
lemma (in dynkin_system) diff:
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1168
  assumes sets: "D \<in> sets M" "E \<in> sets M" and "D \<subseteq> E"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1169
  shows "E - D \<in> sets M"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1170
proof -
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1171
  let ?f = "\<lambda>x. if x = 0 then D else if x = Suc 0 then space M - E else {}"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1172
  have "range ?f = {D, space M - E, {}}"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1173
    by (auto simp: image_iff)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1174
  moreover have "D \<union> (space M - E) = (\<Union>i. ?f i)"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1175
    by (auto simp: image_iff split: split_if_asm)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1176
  moreover
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1177
  then have "disjoint_family ?f" unfolding disjoint_family_on_def
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1178
    using `D \<in> sets M`[THEN sets_into_space] `D \<subseteq> E` by auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1179
  ultimately have "space M - (D \<union> (space M - E)) \<in> sets M"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1180
    using sets by auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1181
  also have "space M - (D \<union> (space M - E)) = E - D"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1182
    using assms sets_into_space by auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1183
  finally show ?thesis .
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1184
qed
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1185
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1186
lemma dynkin_systemI:
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1187
  assumes "\<And> A. A \<in> sets M \<Longrightarrow> A \<subseteq> space M" "space M \<in> sets M"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1188
  assumes "\<And> A. A \<in> sets M \<Longrightarrow> space M - A \<in> sets M"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1189
  assumes "\<And> A. disjoint_family A \<Longrightarrow> range A \<subseteq> sets M
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1190
          \<Longrightarrow> (\<Union>i::nat. A i) \<in> sets M"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1191
  shows "dynkin_system M"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1192
  using assms by (auto simp: dynkin_system_def)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1193
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1194
lemma dynkin_system_trivial:
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1195
  shows "dynkin_system \<lparr> space = A, sets = Pow A \<rparr>"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1196
  by (rule dynkin_systemI) auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1197
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1198
lemma sigma_algebra_imp_dynkin_system:
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1199
  assumes "sigma_algebra M" shows "dynkin_system M"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1200
proof -
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1201
  interpret sigma_algebra M by fact
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1202
  show ?thesis using sets_into_space by (fastsimp intro!: dynkin_systemI)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1203
qed
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1204
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1205
subsection "Intersection stable algebras"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1206
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1207
definition "Int_stable M \<longleftrightarrow> (\<forall> a \<in> sets M. \<forall> b \<in> sets M. a \<inter> b \<in> sets M)"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1208
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1209
lemma (in algebra) Int_stable: "Int_stable M"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1210
  unfolding Int_stable_def by auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1211
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1212
lemma (in dynkin_system) sigma_algebra_eq_Int_stable:
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1213
  "sigma_algebra M \<longleftrightarrow> Int_stable M"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1214
proof
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1215
  assume "sigma_algebra M" then show "Int_stable M"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1216
    unfolding sigma_algebra_def using algebra.Int_stable by auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1217
next
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1218
  assume "Int_stable M"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1219
  show "sigma_algebra M"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1220
    unfolding sigma_algebra_disjoint_iff algebra_def
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1221
  proof (intro conjI ballI allI impI)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1222
    show "sets M \<subseteq> Pow (space M)" using sets_into_space by auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1223
  next
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1224
    fix A B assume "A \<in> sets M" "B \<in> sets M"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1225
    then have "A \<union> B = space M - ((space M - A) \<inter> (space M - B))"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1226
              "space M - A \<in> sets M" "space M - B \<in> sets M"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1227
      using sets_into_space by auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1228
    then show "A \<union> B \<in> sets M"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1229
      using `Int_stable M` unfolding Int_stable_def by auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1230
  qed auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1231
qed
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1232
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1233
subsection "Smallest Dynkin systems"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1234
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1235
definition dynkin :: "'a algebra \<Rightarrow> 'a algebra" where
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1236
  "dynkin M = \<lparr> space = space M,
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1237
     sets =  \<Inter>{D. dynkin_system \<lparr> space = space M, sets = D\<rparr> \<and> sets M \<subseteq> D}\<rparr>"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1238
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1239
lemma dynkin_system_dynkin:
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1240
  fixes M :: "'a algebra"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1241
  assumes "sets M \<subseteq> Pow (space M)"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1242
  shows "dynkin_system (dynkin M)"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1243
proof (rule dynkin_systemI)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1244
  fix A assume "A \<in> sets (dynkin M)"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1245
  moreover
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1246
  { fix D assume "A \<in> D" and d: "dynkin_system \<lparr> space = space M, sets = D \<rparr>"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1247
    from dynkin_system.sets_into_space[OF d] `A \<in> D`
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1248
    have "A \<subseteq> space M" by auto }
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1249
  moreover have "{D. dynkin_system \<lparr> space = space M, sets = D\<rparr> \<and> sets M \<subseteq> D} \<noteq> {}"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1250
    using assms dynkin_system_trivial by fastsimp
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1251
  ultimately show "A \<subseteq> space (dynkin M)"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1252
    unfolding dynkin_def using assms
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1253
    by simp (metis dynkin_system.sets_into_space in_mono mem_def)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1254
next
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1255
  show "space (dynkin M) \<in> sets (dynkin M)"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1256
    unfolding dynkin_def using dynkin_system.space by fastsimp
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1257
next
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1258
  fix A assume "A \<in> sets (dynkin M)"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1259
  then show "space (dynkin M) - A \<in> sets (dynkin M)"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1260
    unfolding dynkin_def using dynkin_system.compl by force
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1261
next
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1262
  fix A :: "nat \<Rightarrow> 'a set"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1263
  assume A: "disjoint_family A" "range A \<subseteq> sets (dynkin M)"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1264
  show "(\<Union>i. A i) \<in> sets (dynkin M)" unfolding dynkin_def
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 40702
diff changeset
  1265
  proof (simp, safe)