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