src/HOL/Probability/Sigma_Algebra.thy
author huffman
Sun Apr 01 16:09:58 2012 +0200 (2012-04-01)
changeset 47255 30a1692557b0
parent 46731 5302e932d1e5
child 47694 05663f75964c
permissions -rw-r--r--
removed Nat_Numeral.thy, moving all theorems elsewhere
     1 (*  Title:      HOL/Probability/Sigma_Algebra.thy
     2     Author:     Stefan Richter, Markus Wenzel, TU München
     3     Author:     Johannes Hölzl, TU München
     4     Plus material from the Hurd/Coble measure theory development,
     5     translated by Lawrence Paulson.
     6 *)
     7 
     8 header {* Sigma Algebras *}
     9 
    10 theory Sigma_Algebra
    11 imports
    12   Complex_Main
    13   "~~/src/HOL/Library/Countable"
    14   "~~/src/HOL/Library/FuncSet"
    15   "~~/src/HOL/Library/Indicator_Function"
    16 begin
    17 
    18 text {* Sigma algebras are an elementary concept in measure
    19   theory. To measure --- that is to integrate --- functions, we first have
    20   to measure sets. Unfortunately, when dealing with a large universe,
    21   it is often not possible to consistently assign a measure to every
    22   subset. Therefore it is necessary to define the set of measurable
    23   subsets of the universe. A sigma algebra is such a set that has
    24   three very natural and desirable properties. *}
    25 
    26 subsection {* Algebras *}
    27 
    28 record 'a algebra =
    29   space :: "'a set"
    30   sets :: "'a set set"
    31 
    32 locale subset_class =
    33   fixes M :: "('a, 'b) algebra_scheme"
    34   assumes space_closed: "sets M \<subseteq> Pow (space M)"
    35 
    36 lemma (in subset_class) sets_into_space: "x \<in> sets M \<Longrightarrow> x \<subseteq> space M"
    37   by (metis PowD contra_subsetD space_closed)
    38 
    39 locale ring_of_sets = subset_class +
    40   assumes empty_sets [iff]: "{} \<in> sets M"
    41      and  Diff [intro]: "\<And>a b. a \<in> sets M \<Longrightarrow> b \<in> sets M \<Longrightarrow> a - b \<in> sets M"
    42      and  Un [intro]: "\<And>a b. a \<in> sets M \<Longrightarrow> b \<in> sets M \<Longrightarrow> a \<union> b \<in> sets M"
    43 
    44 lemma (in ring_of_sets) Int [intro]:
    45   assumes a: "a \<in> sets M" and b: "b \<in> sets M" shows "a \<inter> b \<in> sets M"
    46 proof -
    47   have "a \<inter> b = a - (a - b)"
    48     by auto
    49   then show "a \<inter> b \<in> sets M"
    50     using a b by auto
    51 qed
    52 
    53 lemma (in ring_of_sets) finite_Union [intro]:
    54   "finite X \<Longrightarrow> X \<subseteq> sets M \<Longrightarrow> Union X \<in> sets M"
    55   by (induct set: finite) (auto simp add: Un)
    56 
    57 lemma (in ring_of_sets) finite_UN[intro]:
    58   assumes "finite I" and "\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets M"
    59   shows "(\<Union>i\<in>I. A i) \<in> sets M"
    60   using assms by induct auto
    61 
    62 lemma (in ring_of_sets) finite_INT[intro]:
    63   assumes "finite I" "I \<noteq> {}" "\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets M"
    64   shows "(\<Inter>i\<in>I. A i) \<in> sets M"
    65   using assms by (induct rule: finite_ne_induct) auto
    66 
    67 lemma (in ring_of_sets) insert_in_sets:
    68   assumes "{x} \<in> sets M" "A \<in> sets M" shows "insert x A \<in> sets M"
    69 proof -
    70   have "{x} \<union> A \<in> sets M" using assms by (rule Un)
    71   thus ?thesis by auto
    72 qed
    73 
    74 lemma (in ring_of_sets) Int_space_eq1 [simp]: "x \<in> sets M \<Longrightarrow> space M \<inter> x = x"
    75   by (metis Int_absorb1 sets_into_space)
    76 
    77 lemma (in ring_of_sets) Int_space_eq2 [simp]: "x \<in> sets M \<Longrightarrow> x \<inter> space M = x"
    78   by (metis Int_absorb2 sets_into_space)
    79 
    80 lemma (in ring_of_sets) sets_Collect_conj:
    81   assumes "{x\<in>space M. P x} \<in> sets M" "{x\<in>space M. Q x} \<in> sets M"
    82   shows "{x\<in>space M. Q x \<and> P x} \<in> sets M"
    83 proof -
    84   have "{x\<in>space M. Q x \<and> P x} = {x\<in>space M. Q x} \<inter> {x\<in>space M. P x}"
    85     by auto
    86   with assms show ?thesis by auto
    87 qed
    88 
    89 lemma (in ring_of_sets) sets_Collect_disj:
    90   assumes "{x\<in>space M. P x} \<in> sets M" "{x\<in>space M. Q x} \<in> sets M"
    91   shows "{x\<in>space M. Q x \<or> P x} \<in> sets M"
    92 proof -
    93   have "{x\<in>space M. Q x \<or> P x} = {x\<in>space M. Q x} \<union> {x\<in>space M. P x}"
    94     by auto
    95   with assms show ?thesis by auto
    96 qed
    97 
    98 lemma (in ring_of_sets) sets_Collect_finite_All:
    99   assumes "\<And>i. i \<in> S \<Longrightarrow> {x\<in>space M. P i x} \<in> sets M" "finite S" "S \<noteq> {}"
   100   shows "{x\<in>space M. \<forall>i\<in>S. P i x} \<in> sets M"
   101 proof -
   102   have "{x\<in>space M. \<forall>i\<in>S. P i x} = (\<Inter>i\<in>S. {x\<in>space M. P i x})"
   103     using `S \<noteq> {}` by auto
   104   with assms show ?thesis by auto
   105 qed
   106 
   107 lemma (in ring_of_sets) sets_Collect_finite_Ex:
   108   assumes "\<And>i. i \<in> S \<Longrightarrow> {x\<in>space M. P i x} \<in> sets M" "finite S"
   109   shows "{x\<in>space M. \<exists>i\<in>S. P i x} \<in> sets M"
   110 proof -
   111   have "{x\<in>space M. \<exists>i\<in>S. P i x} = (\<Union>i\<in>S. {x\<in>space M. P i x})"
   112     by auto
   113   with assms show ?thesis by auto
   114 qed
   115 
   116 locale algebra = ring_of_sets +
   117   assumes top [iff]: "space M \<in> sets M"
   118 
   119 lemma (in algebra) compl_sets [intro]:
   120   "a \<in> sets M \<Longrightarrow> space M - a \<in> sets M"
   121   by auto
   122 
   123 lemma algebra_iff_Un:
   124   "algebra M \<longleftrightarrow>
   125     sets M \<subseteq> Pow (space M) &
   126     {} \<in> sets M &
   127     (\<forall>a \<in> sets M. space M - a \<in> sets M) &
   128     (\<forall>a \<in> sets M. \<forall> b \<in> sets M. a \<union> b \<in> sets M)" (is "_ \<longleftrightarrow> ?Un")
   129 proof
   130   assume "algebra M"
   131   then interpret algebra M .
   132   show ?Un using sets_into_space by auto
   133 next
   134   assume ?Un
   135   show "algebra M"
   136   proof
   137     show space: "sets M \<subseteq> Pow (space M)" "{} \<in> sets M" "space M \<in> sets M"
   138       using `?Un` by auto
   139     fix a b assume a: "a \<in> sets M" and b: "b \<in> sets M"
   140     then show "a \<union> b \<in> sets M" using `?Un` by auto
   141     have "a - b = space M - ((space M - a) \<union> b)"
   142       using space a b by auto
   143     then show "a - b \<in> sets M"
   144       using a b  `?Un` by auto
   145   qed
   146 qed
   147 
   148 lemma algebra_iff_Int:
   149      "algebra M \<longleftrightarrow>
   150        sets M \<subseteq> Pow (space M) & {} \<in> sets M &
   151        (\<forall>a \<in> sets M. space M - a \<in> sets M) &
   152        (\<forall>a \<in> sets M. \<forall> b \<in> sets M. a \<inter> b \<in> sets M)" (is "_ \<longleftrightarrow> ?Int")
   153 proof
   154   assume "algebra M"
   155   then interpret algebra M .
   156   show ?Int using sets_into_space by auto
   157 next
   158   assume ?Int
   159   show "algebra M"
   160   proof (unfold algebra_iff_Un, intro conjI ballI)
   161     show space: "sets M \<subseteq> Pow (space M)" "{} \<in> sets M"
   162       using `?Int` by auto
   163     from `?Int` show "\<And>a. a \<in> sets M \<Longrightarrow> space M - a \<in> sets M" by auto
   164     fix a b assume sets: "a \<in> sets M" "b \<in> sets M"
   165     hence "a \<union> b = space M - ((space M - a) \<inter> (space M - b))"
   166       using space by blast
   167     also have "... \<in> sets M"
   168       using sets `?Int` by auto
   169     finally show "a \<union> b \<in> sets M" .
   170   qed
   171 qed
   172 
   173 lemma (in algebra) sets_Collect_neg:
   174   assumes "{x\<in>space M. P x} \<in> sets M"
   175   shows "{x\<in>space M. \<not> P x} \<in> sets M"
   176 proof -
   177   have "{x\<in>space M. \<not> P x} = space M - {x\<in>space M. P x}" by auto
   178   with assms show ?thesis by auto
   179 qed
   180 
   181 lemma (in algebra) sets_Collect_imp:
   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"
   183   unfolding imp_conv_disj by (intro sets_Collect_disj sets_Collect_neg)
   184 
   185 lemma (in algebra) sets_Collect_const:
   186   "{x\<in>space M. P} \<in> sets M"
   187   by (cases P) auto
   188 
   189 lemma algebra_single_set:
   190   assumes "X \<subseteq> S"
   191   shows "algebra \<lparr> space = S, sets = { {}, X, S - X, S }\<rparr>"
   192   by default (insert `X \<subseteq> S`, auto)
   193 
   194 section {* Restricted algebras *}
   195 
   196 abbreviation (in algebra)
   197   "restricted_space A \<equiv> \<lparr> space = A, sets = (\<lambda>S. (A \<inter> S)) ` sets M, \<dots> = more M \<rparr>"
   198 
   199 lemma (in algebra) restricted_algebra:
   200   assumes "A \<in> sets M" shows "algebra (restricted_space A)"
   201   using assms by unfold_locales auto
   202 
   203 subsection {* Sigma Algebras *}
   204 
   205 locale sigma_algebra = algebra +
   206   assumes countable_nat_UN [intro]:
   207          "!!A. range A \<subseteq> sets M \<Longrightarrow> (\<Union>i::nat. A i) \<in> sets M"
   208 
   209 lemma (in algebra) is_sigma_algebra:
   210   assumes "finite (sets M)"
   211   shows "sigma_algebra M"
   212 proof
   213   fix A :: "nat \<Rightarrow> 'a set" assume "range A \<subseteq> sets M"
   214   then have "(\<Union>i. A i) = (\<Union>s\<in>sets M \<inter> range A. s)"
   215     by auto
   216   also have "(\<Union>s\<in>sets M \<inter> range A. s) \<in> sets M"
   217     using `finite (sets M)` by auto
   218   finally show "(\<Union>i. A i) \<in> sets M" .
   219 qed
   220 
   221 lemma countable_UN_eq:
   222   fixes A :: "'i::countable \<Rightarrow> 'a set"
   223   shows "(range A \<subseteq> sets M \<longrightarrow> (\<Union>i. A i) \<in> sets M) \<longleftrightarrow>
   224     (range (A \<circ> from_nat) \<subseteq> sets M \<longrightarrow> (\<Union>i. (A \<circ> from_nat) i) \<in> sets M)"
   225 proof -
   226   let ?A' = "A \<circ> from_nat"
   227   have *: "(\<Union>i. ?A' i) = (\<Union>i. A i)" (is "?l = ?r")
   228   proof safe
   229     fix x i assume "x \<in> A i" thus "x \<in> ?l"
   230       by (auto intro!: exI[of _ "to_nat i"])
   231   next
   232     fix x i assume "x \<in> ?A' i" thus "x \<in> ?r"
   233       by (auto intro!: exI[of _ "from_nat i"])
   234   qed
   235   have **: "range ?A' = range A"
   236     using surj_from_nat
   237     by (auto simp: image_compose intro!: imageI)
   238   show ?thesis unfolding * ** ..
   239 qed
   240 
   241 lemma (in sigma_algebra) countable_UN[intro]:
   242   fixes A :: "'i::countable \<Rightarrow> 'a set"
   243   assumes "A`X \<subseteq> sets M"
   244   shows  "(\<Union>x\<in>X. A x) \<in> sets M"
   245 proof -
   246   let ?A = "\<lambda>i. if i \<in> X then A i else {}"
   247   from assms have "range ?A \<subseteq> sets M" by auto
   248   with countable_nat_UN[of "?A \<circ> from_nat"] countable_UN_eq[of ?A M]
   249   have "(\<Union>x. ?A x) \<in> sets M" by auto
   250   moreover have "(\<Union>x. ?A x) = (\<Union>x\<in>X. A x)" by (auto split: split_if_asm)
   251   ultimately show ?thesis by simp
   252 qed
   253 
   254 lemma (in sigma_algebra) countable_INT [intro]:
   255   fixes A :: "'i::countable \<Rightarrow> 'a set"
   256   assumes A: "A`X \<subseteq> sets M" "X \<noteq> {}"
   257   shows "(\<Inter>i\<in>X. A i) \<in> sets M"
   258 proof -
   259   from A have "\<forall>i\<in>X. A i \<in> sets M" by fast
   260   hence "space M - (\<Union>i\<in>X. space M - A i) \<in> sets M" by blast
   261   moreover
   262   have "(\<Inter>i\<in>X. A i) = space M - (\<Union>i\<in>X. space M - A i)" using space_closed A
   263     by blast
   264   ultimately show ?thesis by metis
   265 qed
   266 
   267 lemma ring_of_sets_Pow:
   268  "ring_of_sets \<lparr> space = sp, sets = Pow sp, \<dots> = X \<rparr>"
   269   by default auto
   270 
   271 lemma algebra_Pow:
   272   "algebra \<lparr> space = sp, sets = Pow sp, \<dots> = X \<rparr>"
   273   by default auto
   274 
   275 lemma sigma_algebra_Pow:
   276      "sigma_algebra \<lparr> space = sp, sets = Pow sp, \<dots> = X \<rparr>"
   277   by default auto
   278 
   279 lemma sigma_algebra_iff:
   280      "sigma_algebra M \<longleftrightarrow>
   281       algebra M \<and> (\<forall>A. range A \<subseteq> sets M \<longrightarrow> (\<Union>i::nat. A i) \<in> sets M)"
   282   by (simp add: sigma_algebra_def sigma_algebra_axioms_def)
   283 
   284 lemma (in sigma_algebra) sets_Collect_countable_All:
   285   assumes "\<And>i. {x\<in>space M. P i x} \<in> sets M"
   286   shows "{x\<in>space M. \<forall>i::'i::countable. P i x} \<in> sets M"
   287 proof -
   288   have "{x\<in>space M. \<forall>i::'i::countable. P i x} = (\<Inter>i. {x\<in>space M. P i x})" by auto
   289   with assms show ?thesis by auto
   290 qed
   291 
   292 lemma (in sigma_algebra) sets_Collect_countable_Ex:
   293   assumes "\<And>i. {x\<in>space M. P i x} \<in> sets M"
   294   shows "{x\<in>space M. \<exists>i::'i::countable. P i x} \<in> sets M"
   295 proof -
   296   have "{x\<in>space M. \<exists>i::'i::countable. P i x} = (\<Union>i. {x\<in>space M. P i x})" by auto
   297   with assms show ?thesis by auto
   298 qed
   299 
   300 lemmas (in sigma_algebra) sets_Collect =
   301   sets_Collect_imp sets_Collect_disj sets_Collect_conj sets_Collect_neg sets_Collect_const
   302   sets_Collect_countable_All sets_Collect_countable_Ex sets_Collect_countable_All
   303 
   304 lemma sigma_algebra_single_set:
   305   assumes "X \<subseteq> S"
   306   shows "sigma_algebra \<lparr> space = S, sets = { {}, X, S - X, S }\<rparr>"
   307   using algebra.is_sigma_algebra[OF algebra_single_set[OF `X \<subseteq> S`]] by simp
   308 
   309 subsection {* Binary Unions *}
   310 
   311 definition binary :: "'a \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a"
   312   where "binary a b =  (\<lambda>\<^isup>x. b)(0 := a)"
   313 
   314 lemma range_binary_eq: "range(binary a b) = {a,b}"
   315   by (auto simp add: binary_def)
   316 
   317 lemma Un_range_binary: "a \<union> b = (\<Union>i::nat. binary a b i)"
   318   by (simp add: SUP_def range_binary_eq)
   319 
   320 lemma Int_range_binary: "a \<inter> b = (\<Inter>i::nat. binary a b i)"
   321   by (simp add: INF_def range_binary_eq)
   322 
   323 lemma sigma_algebra_iff2:
   324      "sigma_algebra M \<longleftrightarrow>
   325        sets M \<subseteq> Pow (space M) \<and>
   326        {} \<in> sets M \<and> (\<forall>s \<in> sets M. space M - s \<in> sets M) \<and>
   327        (\<forall>A. range A \<subseteq> sets M \<longrightarrow> (\<Union>i::nat. A i) \<in> sets M)"
   328   by (auto simp add: range_binary_eq sigma_algebra_def sigma_algebra_axioms_def
   329          algebra_iff_Un Un_range_binary)
   330 
   331 subsection {* Initial Sigma Algebra *}
   332 
   333 text {*Sigma algebras can naturally be created as the closure of any set of
   334   sets with regard to the properties just postulated.  *}
   335 
   336 inductive_set
   337   sigma_sets :: "'a set \<Rightarrow> 'a set set \<Rightarrow> 'a set set"
   338   for sp :: "'a set" and A :: "'a set set"
   339   where
   340     Basic: "a \<in> A \<Longrightarrow> a \<in> sigma_sets sp A"
   341   | Empty: "{} \<in> sigma_sets sp A"
   342   | Compl: "a \<in> sigma_sets sp A \<Longrightarrow> sp - a \<in> sigma_sets sp A"
   343   | Union: "(\<And>i::nat. a i \<in> sigma_sets sp A) \<Longrightarrow> (\<Union>i. a i) \<in> sigma_sets sp A"
   344 
   345 definition
   346   "sigma M = \<lparr> space = space M, sets = sigma_sets (space M) (sets M), \<dots> = more M \<rparr>"
   347 
   348 lemma (in sigma_algebra) sigma_sets_subset:
   349   assumes a: "a \<subseteq> sets M"
   350   shows "sigma_sets (space M) a \<subseteq> sets M"
   351 proof
   352   fix x
   353   assume "x \<in> sigma_sets (space M) a"
   354   from this show "x \<in> sets M"
   355     by (induct rule: sigma_sets.induct, auto) (metis a subsetD)
   356 qed
   357 
   358 lemma sigma_sets_into_sp: "A \<subseteq> Pow sp \<Longrightarrow> x \<in> sigma_sets sp A \<Longrightarrow> x \<subseteq> sp"
   359   by (erule sigma_sets.induct, auto)
   360 
   361 lemma sigma_algebra_sigma_sets:
   362      "a \<subseteq> Pow (space M) \<Longrightarrow> sets M = sigma_sets (space M) a \<Longrightarrow> sigma_algebra M"
   363   by (auto simp add: sigma_algebra_iff2 dest: sigma_sets_into_sp
   364            intro!: sigma_sets.Union sigma_sets.Empty sigma_sets.Compl)
   365 
   366 lemma sigma_sets_least_sigma_algebra:
   367   assumes "A \<subseteq> Pow S"
   368   shows "sigma_sets S A = \<Inter>{B. A \<subseteq> B \<and> sigma_algebra \<lparr>space = S, sets = B\<rparr>}"
   369 proof safe
   370   fix B X assume "A \<subseteq> B" and sa: "sigma_algebra \<lparr> space = S, sets = B \<rparr>"
   371     and X: "X \<in> sigma_sets S A"
   372   from sigma_algebra.sigma_sets_subset[OF sa, simplified, OF `A \<subseteq> B`] X
   373   show "X \<in> B" by auto
   374 next
   375   fix X assume "X \<in> \<Inter>{B. A \<subseteq> B \<and> sigma_algebra \<lparr>space = S, sets = B\<rparr>}"
   376   then have [intro!]: "\<And>B. A \<subseteq> B \<Longrightarrow> sigma_algebra \<lparr>space = S, sets = B\<rparr> \<Longrightarrow> X \<in> B"
   377      by simp
   378   have "A \<subseteq> sigma_sets S A" using assms
   379     by (auto intro!: sigma_sets.Basic)
   380   moreover have "sigma_algebra \<lparr>space = S, sets = sigma_sets S A\<rparr>"
   381     using assms by (intro sigma_algebra_sigma_sets[of A]) auto
   382   ultimately show "X \<in> sigma_sets S A" by auto
   383 qed
   384 
   385 lemma sets_sigma: "sets (sigma M) = sigma_sets (space M) (sets M)"
   386   unfolding sigma_def by simp
   387 
   388 lemma space_sigma [simp]: "space (sigma M) = space M"
   389   by (simp add: sigma_def)
   390 
   391 lemma sigma_sets_top: "sp \<in> sigma_sets sp A"
   392   by (metis Diff_empty sigma_sets.Compl sigma_sets.Empty)
   393 
   394 lemma sigma_sets_Un:
   395   "a \<in> sigma_sets sp A \<Longrightarrow> b \<in> sigma_sets sp A \<Longrightarrow> a \<union> b \<in> sigma_sets sp A"
   396 apply (simp add: Un_range_binary range_binary_eq)
   397 apply (rule Union, simp add: binary_def)
   398 done
   399 
   400 lemma sigma_sets_Inter:
   401   assumes Asb: "A \<subseteq> Pow sp"
   402   shows "(\<And>i::nat. a i \<in> sigma_sets sp A) \<Longrightarrow> (\<Inter>i. a i) \<in> sigma_sets sp A"
   403 proof -
   404   assume ai: "\<And>i::nat. a i \<in> sigma_sets sp A"
   405   hence "\<And>i::nat. sp-(a i) \<in> sigma_sets sp A"
   406     by (rule sigma_sets.Compl)
   407   hence "(\<Union>i. sp-(a i)) \<in> sigma_sets sp A"
   408     by (rule sigma_sets.Union)
   409   hence "sp-(\<Union>i. sp-(a i)) \<in> sigma_sets sp A"
   410     by (rule sigma_sets.Compl)
   411   also have "sp-(\<Union>i. sp-(a i)) = sp Int (\<Inter>i. a i)"
   412     by auto
   413   also have "... = (\<Inter>i. a i)" using ai
   414     by (blast dest: sigma_sets_into_sp [OF Asb])
   415   finally show ?thesis .
   416 qed
   417 
   418 lemma sigma_sets_INTER:
   419   assumes Asb: "A \<subseteq> Pow sp"
   420       and ai: "\<And>i::nat. i \<in> S \<Longrightarrow> a i \<in> sigma_sets sp A" and non: "S \<noteq> {}"
   421   shows "(\<Inter>i\<in>S. a i) \<in> sigma_sets sp A"
   422 proof -
   423   from ai have "\<And>i. (if i\<in>S then a i else sp) \<in> sigma_sets sp A"
   424     by (simp add: sigma_sets.intros sigma_sets_top)
   425   hence "(\<Inter>i. (if i\<in>S then a i else sp)) \<in> sigma_sets sp A"
   426     by (rule sigma_sets_Inter [OF Asb])
   427   also have "(\<Inter>i. (if i\<in>S then a i else sp)) = (\<Inter>i\<in>S. a i)"
   428     by auto (metis ai non sigma_sets_into_sp subset_empty subset_iff Asb)+
   429   finally show ?thesis .
   430 qed
   431 
   432 lemma (in sigma_algebra) sigma_sets_eq:
   433      "sigma_sets (space M) (sets M) = sets M"
   434 proof
   435   show "sets M \<subseteq> sigma_sets (space M) (sets M)"
   436     by (metis Set.subsetI sigma_sets.Basic)
   437   next
   438   show "sigma_sets (space M) (sets M) \<subseteq> sets M"
   439     by (metis sigma_sets_subset subset_refl)
   440 qed
   441 
   442 lemma sigma_sets_eqI:
   443   assumes A: "\<And>a. a \<in> A \<Longrightarrow> a \<in> sigma_sets M B"
   444   assumes B: "\<And>b. b \<in> B \<Longrightarrow> b \<in> sigma_sets M A"
   445   shows "sigma_sets M A = sigma_sets M B"
   446 proof (intro set_eqI iffI)
   447   fix a assume "a \<in> sigma_sets M A"
   448   from this A show "a \<in> sigma_sets M B"
   449     by induct (auto intro!: sigma_sets.intros del: sigma_sets.Basic)
   450 next
   451   fix b assume "b \<in> sigma_sets M B"
   452   from this B show "b \<in> sigma_sets M A"
   453     by induct (auto intro!: sigma_sets.intros del: sigma_sets.Basic)
   454 qed
   455 
   456 lemma sigma_algebra_sigma:
   457     "sets M \<subseteq> Pow (space M) \<Longrightarrow> sigma_algebra (sigma M)"
   458   apply (rule sigma_algebra_sigma_sets)
   459   apply (auto simp add: sigma_def)
   460   done
   461 
   462 lemma (in sigma_algebra) sigma_subset:
   463     "sets N \<subseteq> sets M \<Longrightarrow> space N = space M \<Longrightarrow> sets (sigma N) \<subseteq> (sets M)"
   464   by (simp add: sigma_def sigma_sets_subset)
   465 
   466 lemma sigma_sets_subseteq: assumes "A \<subseteq> B" shows "sigma_sets X A \<subseteq> sigma_sets X B"
   467 proof
   468   fix x assume "x \<in> sigma_sets X A" then show "x \<in> sigma_sets X B"
   469     by induct (insert `A \<subseteq> B`, auto intro: sigma_sets.intros)
   470 qed
   471 
   472 lemma (in sigma_algebra) restriction_in_sets:
   473   fixes A :: "nat \<Rightarrow> 'a set"
   474   assumes "S \<in> sets M"
   475   and *: "range A \<subseteq> (\<lambda>A. S \<inter> A) ` sets M" (is "_ \<subseteq> ?r")
   476   shows "range A \<subseteq> sets M" "(\<Union>i. A i) \<in> (\<lambda>A. S \<inter> A) ` sets M"
   477 proof -
   478   { fix i have "A i \<in> ?r" using * by auto
   479     hence "\<exists>B. A i = B \<inter> S \<and> B \<in> sets M" by auto
   480     hence "A i \<subseteq> S" "A i \<in> sets M" using `S \<in> sets M` by auto }
   481   thus "range A \<subseteq> sets M" "(\<Union>i. A i) \<in> (\<lambda>A. S \<inter> A) ` sets M"
   482     by (auto intro!: image_eqI[of _ _ "(\<Union>i. A i)"])
   483 qed
   484 
   485 lemma (in sigma_algebra) restricted_sigma_algebra:
   486   assumes "S \<in> sets M"
   487   shows "sigma_algebra (restricted_space S)"
   488   unfolding sigma_algebra_def sigma_algebra_axioms_def
   489 proof safe
   490   show "algebra (restricted_space S)" using restricted_algebra[OF assms] .
   491 next
   492   fix A :: "nat \<Rightarrow> 'a set" assume "range A \<subseteq> sets (restricted_space S)"
   493   from restriction_in_sets[OF assms this[simplified]]
   494   show "(\<Union>i. A i) \<in> sets (restricted_space S)" by simp
   495 qed
   496 
   497 lemma sigma_sets_Int:
   498   assumes "A \<in> sigma_sets sp st" "A \<subseteq> sp"
   499   shows "op \<inter> A ` sigma_sets sp st = sigma_sets A (op \<inter> A ` st)"
   500 proof (intro equalityI subsetI)
   501   fix x assume "x \<in> op \<inter> A ` sigma_sets sp st"
   502   then obtain y where "y \<in> sigma_sets sp st" "x = y \<inter> A" by auto
   503   then have "x \<in> sigma_sets (A \<inter> sp) (op \<inter> A ` st)"
   504   proof (induct arbitrary: x)
   505     case (Compl a)
   506     then show ?case
   507       by (force intro!: sigma_sets.Compl simp: Diff_Int_distrib ac_simps)
   508   next
   509     case (Union a)
   510     then show ?case
   511       by (auto intro!: sigma_sets.Union
   512                simp add: UN_extend_simps simp del: UN_simps)
   513   qed (auto intro!: sigma_sets.intros)
   514   then show "x \<in> sigma_sets A (op \<inter> A ` st)"
   515     using `A \<subseteq> sp` by (simp add: Int_absorb2)
   516 next
   517   fix x assume "x \<in> sigma_sets A (op \<inter> A ` st)"
   518   then show "x \<in> op \<inter> A ` sigma_sets sp st"
   519   proof induct
   520     case (Compl a)
   521     then obtain x where "a = A \<inter> x" "x \<in> sigma_sets sp st" by auto
   522     then show ?case using `A \<subseteq> sp`
   523       by (force simp add: image_iff intro!: bexI[of _ "sp - x"] sigma_sets.Compl)
   524   next
   525     case (Union a)
   526     then have "\<forall>i. \<exists>x. x \<in> sigma_sets sp st \<and> a i = A \<inter> x"
   527       by (auto simp: image_iff Bex_def)
   528     from choice[OF this] guess f ..
   529     then show ?case
   530       by (auto intro!: bexI[of _ "(\<Union>x. f x)"] sigma_sets.Union
   531                simp add: image_iff)
   532   qed (auto intro!: sigma_sets.intros)
   533 qed
   534 
   535 lemma sigma_sets_single[simp]: "sigma_sets {X} {{X}} = {{}, {X}}"
   536 proof (intro set_eqI iffI)
   537   fix x assume "x \<in> sigma_sets {X} {{X}}"
   538   from sigma_sets_into_sp[OF _ this]
   539   show "x \<in> {{}, {X}}" by auto
   540 next
   541   fix x assume "x \<in> {{}, {X}}"
   542   then show "x \<in> sigma_sets {X} {{X}}"
   543     by (auto intro: sigma_sets.Empty sigma_sets_top)
   544 qed
   545 
   546 lemma (in sigma_algebra) sets_sigma_subset:
   547   assumes "space N = space M"
   548   assumes "sets N \<subseteq> sets M"
   549   shows "sets (sigma N) \<subseteq> sets M"
   550   by (unfold assms sets_sigma, rule sigma_sets_subset, rule assms)
   551 
   552 lemma in_sigma[intro, simp]: "A \<in> sets M \<Longrightarrow> A \<in> sets (sigma M)"
   553   unfolding sigma_def by (auto intro!: sigma_sets.Basic)
   554 
   555 lemma (in sigma_algebra) sigma_eq[simp]: "sigma M = M"
   556   unfolding sigma_def sigma_sets_eq by simp
   557 
   558 lemma sigma_sigma_eq:
   559   assumes "sets M \<subseteq> Pow (space M)"
   560   shows "sigma (sigma M) = sigma M"
   561   using sigma_algebra.sigma_eq[OF sigma_algebra_sigma, OF assms] .
   562 
   563 lemma sigma_sets_sigma_sets_eq:
   564   "M \<subseteq> Pow S \<Longrightarrow> sigma_sets S (sigma_sets S M) = sigma_sets S M"
   565   using sigma_sigma_eq[of "\<lparr> space = S, sets = M \<rparr>"]
   566   by (simp add: sigma_def)
   567 
   568 lemma sigma_sets_singleton:
   569   assumes "X \<subseteq> S"
   570   shows "sigma_sets S { X } = { {}, X, S - X, S }"
   571 proof -
   572   interpret sigma_algebra "\<lparr> space = S, sets = { {}, X, S - X, S }\<rparr>"
   573     by (rule sigma_algebra_single_set) fact
   574   have "sigma_sets S { X } \<subseteq> sigma_sets S { {}, X, S - X, S }"
   575     by (rule sigma_sets_subseteq) simp
   576   moreover have "\<dots> = { {}, X, S - X, S }"
   577     using sigma_eq unfolding sigma_def by simp
   578   moreover
   579   { fix A assume "A \<in> { {}, X, S - X, S }"
   580     then have "A \<in> sigma_sets S { X }"
   581       by (auto intro: sigma_sets.intros sigma_sets_top) }
   582   ultimately have "sigma_sets S { X } = sigma_sets S { {}, X, S - X, S }"
   583     by (intro antisym) auto
   584   with sigma_eq show ?thesis
   585     unfolding sigma_def by simp
   586 qed
   587 
   588 lemma restricted_sigma:
   589   assumes S: "S \<in> sets (sigma M)" and M: "sets M \<subseteq> Pow (space M)"
   590   shows "algebra.restricted_space (sigma M) S = sigma (algebra.restricted_space M S)"
   591 proof -
   592   from S sigma_sets_into_sp[OF M]
   593   have "S \<in> sigma_sets (space M) (sets M)" "S \<subseteq> space M"
   594     by (auto simp: sigma_def)
   595   from sigma_sets_Int[OF this]
   596   show ?thesis
   597     by (simp add: sigma_def)
   598 qed
   599 
   600 lemma sigma_sets_vimage_commute:
   601   assumes X: "X \<in> space M \<rightarrow> space M'"
   602   shows "{X -` A \<inter> space M |A. A \<in> sets (sigma M')}
   603        = sigma_sets (space M) {X -` A \<inter> space M |A. A \<in> sets M'}" (is "?L = ?R")
   604 proof
   605   show "?L \<subseteq> ?R"
   606   proof clarify
   607     fix A assume "A \<in> sets (sigma M')"
   608     then have "A \<in> sigma_sets (space M') (sets M')" by (simp add: sets_sigma)
   609     then show "X -` A \<inter> space M \<in> ?R"
   610     proof induct
   611       case (Basic B) then show ?case
   612         by (auto intro!: sigma_sets.Basic)
   613     next
   614       case Empty then show ?case
   615         by (auto intro!: sigma_sets.Empty)
   616     next
   617       case (Compl B)
   618       have [simp]: "X -` (space M' - B) \<inter> space M = space M - (X -` B \<inter> space M)"
   619         by (auto simp add: funcset_mem [OF X])
   620       with Compl show ?case
   621         by (auto intro!: sigma_sets.Compl)
   622     next
   623       case (Union F)
   624       then show ?case
   625         by (auto simp add: vimage_UN UN_extend_simps(4) simp del: UN_simps
   626                  intro!: sigma_sets.Union)
   627     qed
   628   qed
   629   show "?R \<subseteq> ?L"
   630   proof clarify
   631     fix A assume "A \<in> ?R"
   632     then show "\<exists>B. A = X -` B \<inter> space M \<and> B \<in> sets (sigma M')"
   633     proof induct
   634       case (Basic B) then show ?case by auto
   635     next
   636       case Empty then show ?case
   637         by (auto simp: sets_sigma intro!: sigma_sets.Empty exI[of _ "{}"])
   638     next
   639       case (Compl B)
   640       then obtain A where A: "B = X -` A \<inter> space M" "A \<in> sets (sigma M')" by auto
   641       then have [simp]: "space M - B = X -` (space M' - A) \<inter> space M"
   642         by (auto simp add: funcset_mem [OF X])
   643       with A(2) show ?case
   644         by (auto simp: sets_sigma intro: sigma_sets.Compl)
   645     next
   646       case (Union F)
   647       then have "\<forall>i. \<exists>B. F i = X -` B \<inter> space M \<and> B \<in> sets (sigma M')" by auto
   648       from choice[OF this] guess A .. note A = this
   649       with A show ?case
   650         by (auto simp: sets_sigma vimage_UN[symmetric] intro: sigma_sets.Union)
   651     qed
   652   qed
   653 qed
   654 
   655 section {* Measurable functions *}
   656 
   657 definition
   658   "measurable A B = {f \<in> space A -> space B. \<forall>y \<in> sets B. f -` y \<inter> space A \<in> sets A}"
   659 
   660 lemma (in sigma_algebra) measurable_sigma:
   661   assumes B: "sets N \<subseteq> Pow (space N)"
   662       and f: "f \<in> space M -> space N"
   663       and ba: "\<And>y. y \<in> sets N \<Longrightarrow> (f -` y) \<inter> space M \<in> sets M"
   664   shows "f \<in> measurable M (sigma N)"
   665 proof -
   666   have "sigma_sets (space N) (sets N) \<subseteq> {y . (f -` y) \<inter> space M \<in> sets M & y \<subseteq> space N}"
   667     proof clarify
   668       fix x
   669       assume "x \<in> sigma_sets (space N) (sets N)"
   670       thus "f -` x \<inter> space M \<in> sets M \<and> x \<subseteq> space N"
   671         proof induct
   672           case (Basic a)
   673           thus ?case
   674             by (auto simp add: ba) (metis B subsetD PowD)
   675         next
   676           case Empty
   677           thus ?case
   678             by auto
   679         next
   680           case (Compl a)
   681           have [simp]: "f -` space N \<inter> space M = space M"
   682             by (auto simp add: funcset_mem [OF f])
   683           thus ?case
   684             by (auto simp add: vimage_Diff Diff_Int_distrib2 compl_sets Compl)
   685         next
   686           case (Union a)
   687           thus ?case
   688             by (simp add: vimage_UN, simp only: UN_extend_simps(4)) blast
   689         qed
   690     qed
   691   thus ?thesis
   692     by (simp add: measurable_def sigma_algebra_axioms sigma_algebra_sigma B f)
   693        (auto simp add: sigma_def)
   694 qed
   695 
   696 lemma measurable_cong:
   697   assumes "\<And> w. w \<in> space M \<Longrightarrow> f w = g w"
   698   shows "f \<in> measurable M M' \<longleftrightarrow> g \<in> measurable M M'"
   699   unfolding measurable_def using assms
   700   by (simp cong: vimage_inter_cong Pi_cong)
   701 
   702 lemma measurable_space:
   703   "f \<in> measurable M A \<Longrightarrow> x \<in> space M \<Longrightarrow> f x \<in> space A"
   704    unfolding measurable_def by auto
   705 
   706 lemma measurable_sets:
   707   "f \<in> measurable M A \<Longrightarrow> S \<in> sets A \<Longrightarrow> f -` S \<inter> space M \<in> sets M"
   708    unfolding measurable_def by auto
   709 
   710 lemma (in sigma_algebra) measurable_subset:
   711      "(\<And>S. S \<in> sets A \<Longrightarrow> S \<subseteq> space A) \<Longrightarrow> measurable M A \<subseteq> measurable M (sigma A)"
   712   by (auto intro: measurable_sigma measurable_sets measurable_space)
   713 
   714 lemma measurable_eqI:
   715      "\<lbrakk> space m1 = space m1' ; space m2 = space m2' ;
   716         sets m1 = sets m1' ; sets m2 = sets m2' \<rbrakk>
   717       \<Longrightarrow> measurable m1 m2 = measurable m1' m2'"
   718   by (simp add: measurable_def sigma_algebra_iff2)
   719 
   720 lemma (in sigma_algebra) measurable_const[intro, simp]:
   721   assumes "c \<in> space M'"
   722   shows "(\<lambda>x. c) \<in> measurable M M'"
   723   using assms by (auto simp add: measurable_def)
   724 
   725 lemma (in sigma_algebra) measurable_If:
   726   assumes measure: "f \<in> measurable M M'" "g \<in> measurable M M'"
   727   assumes P: "{x\<in>space M. P x} \<in> sets M"
   728   shows "(\<lambda>x. if P x then f x else g x) \<in> measurable M M'"
   729   unfolding measurable_def
   730 proof safe
   731   fix x assume "x \<in> space M"
   732   thus "(if P x then f x else g x) \<in> space M'"
   733     using measure unfolding measurable_def by auto
   734 next
   735   fix A assume "A \<in> sets M'"
   736   hence *: "(\<lambda>x. if P x then f x else g x) -` A \<inter> space M =
   737     ((f -` A \<inter> space M) \<inter> {x\<in>space M. P x}) \<union>
   738     ((g -` A \<inter> space M) \<inter> (space M - {x\<in>space M. P x}))"
   739     using measure unfolding measurable_def by (auto split: split_if_asm)
   740   show "(\<lambda>x. if P x then f x else g x) -` A \<inter> space M \<in> sets M"
   741     using `A \<in> sets M'` measure P unfolding * measurable_def
   742     by (auto intro!: Un)
   743 qed
   744 
   745 lemma (in sigma_algebra) measurable_If_set:
   746   assumes measure: "f \<in> measurable M M'" "g \<in> measurable M M'"
   747   assumes P: "A \<in> sets M"
   748   shows "(\<lambda>x. if x \<in> A then f x else g x) \<in> measurable M M'"
   749 proof (rule measurable_If[OF measure])
   750   have "{x \<in> space M. x \<in> A} = A" using `A \<in> sets M` sets_into_space by auto
   751   thus "{x \<in> space M. x \<in> A} \<in> sets M" using `A \<in> sets M` by auto
   752 qed
   753 
   754 lemma (in ring_of_sets) measurable_ident[intro, simp]: "id \<in> measurable M M"
   755   by (auto simp add: measurable_def)
   756 
   757 lemma measurable_comp[intro]:
   758   fixes f :: "'a \<Rightarrow> 'b" and g :: "'b \<Rightarrow> 'c"
   759   shows "f \<in> measurable a b \<Longrightarrow> g \<in> measurable b c \<Longrightarrow> (g o f) \<in> measurable a c"
   760   apply (auto simp add: measurable_def vimage_compose)
   761   apply (subgoal_tac "f -` g -` y \<inter> space a = f -` (g -` y \<inter> space b) \<inter> space a")
   762   apply force+
   763   done
   764 
   765 lemma measurable_strong:
   766   fixes f :: "'a \<Rightarrow> 'b" and g :: "'b \<Rightarrow> 'c"
   767   assumes f: "f \<in> measurable a b" and g: "g \<in> (space b -> space c)"
   768       and a: "sigma_algebra a" and b: "sigma_algebra b" and c: "sigma_algebra c"
   769       and t: "f ` (space a) \<subseteq> t"
   770       and cb: "\<And>s. s \<in> sets c \<Longrightarrow> (g -` s) \<inter> t \<in> sets b"
   771   shows "(g o f) \<in> measurable a c"
   772 proof -
   773   have fab: "f \<in> (space a -> space b)"
   774    and ba: "\<And>y. y \<in> sets b \<Longrightarrow> (f -` y) \<inter> (space a) \<in> sets a" using f
   775      by (auto simp add: measurable_def)
   776   have eq: "f -` g -` y \<inter> space a = f -` (g -` y \<inter> t) \<inter> space a" using t
   777     by force
   778   show ?thesis
   779     apply (auto simp add: measurable_def vimage_compose a c)
   780     apply (metis funcset_mem fab g)
   781     apply (subst eq, metis ba cb)
   782     done
   783 qed
   784 
   785 lemma measurable_mono1:
   786      "a \<subseteq> b \<Longrightarrow> sigma_algebra \<lparr>space = X, sets = b\<rparr>
   787       \<Longrightarrow> measurable \<lparr>space = X, sets = a\<rparr> c \<subseteq> measurable \<lparr>space = X, sets = b\<rparr> c"
   788   by (auto simp add: measurable_def)
   789 
   790 lemma measurable_up_sigma:
   791   "measurable A M \<subseteq> measurable (sigma A) M"
   792   unfolding measurable_def
   793   by (auto simp: sigma_def intro: sigma_sets.Basic)
   794 
   795 lemma (in sigma_algebra) measurable_range_reduce:
   796    "\<lbrakk> f \<in> measurable M \<lparr>space = s, sets = Pow s\<rparr> ; s \<noteq> {} \<rbrakk>
   797     \<Longrightarrow> f \<in> measurable M \<lparr>space = s \<inter> (f ` space M), sets = Pow (s \<inter> (f ` space M))\<rparr>"
   798   by (simp add: measurable_def sigma_algebra_Pow del: Pow_Int_eq) blast
   799 
   800 lemma (in sigma_algebra) measurable_Pow_to_Pow:
   801    "(sets M = Pow (space M)) \<Longrightarrow> f \<in> measurable M \<lparr>space = UNIV, sets = Pow UNIV\<rparr>"
   802   by (auto simp add: measurable_def sigma_algebra_def sigma_algebra_axioms_def algebra_def)
   803 
   804 lemma (in sigma_algebra) measurable_Pow_to_Pow_image:
   805    "sets M = Pow (space M)
   806     \<Longrightarrow> f \<in> measurable M \<lparr>space = f ` space M, sets = Pow (f ` space M)\<rparr>"
   807   by (simp add: measurable_def sigma_algebra_Pow) intro_locales
   808 
   809 lemma (in sigma_algebra) measurable_iff_sigma:
   810   assumes "sets E \<subseteq> Pow (space E)" and "f \<in> space M \<rightarrow> space E"
   811   shows "f \<in> measurable M (sigma E) \<longleftrightarrow> (\<forall>A\<in>sets E. f -` A \<inter> space M \<in> sets M)"
   812   using measurable_sigma[OF assms]
   813   by (fastforce simp: measurable_def sets_sigma intro: sigma_sets.intros)
   814 
   815 section "Disjoint families"
   816 
   817 definition
   818   disjoint_family_on  where
   819   "disjoint_family_on A S \<longleftrightarrow> (\<forall>m\<in>S. \<forall>n\<in>S. m \<noteq> n \<longrightarrow> A m \<inter> A n = {})"
   820 
   821 abbreviation
   822   "disjoint_family A \<equiv> disjoint_family_on A UNIV"
   823 
   824 lemma range_subsetD: "range f \<subseteq> B \<Longrightarrow> f i \<in> B"
   825   by blast
   826 
   827 lemma Int_Diff_disjoint: "A \<inter> B \<inter> (A - B) = {}"
   828   by blast
   829 
   830 lemma Int_Diff_Un: "A \<inter> B \<union> (A - B) = A"
   831   by blast
   832 
   833 lemma disjoint_family_subset:
   834      "disjoint_family A \<Longrightarrow> (!!x. B x \<subseteq> A x) \<Longrightarrow> disjoint_family B"
   835   by (force simp add: disjoint_family_on_def)
   836 
   837 lemma disjoint_family_on_bisimulation:
   838   assumes "disjoint_family_on f S"
   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 = {}"
   840   shows "disjoint_family_on g S"
   841   using assms unfolding disjoint_family_on_def by auto
   842 
   843 lemma disjoint_family_on_mono:
   844   "A \<subseteq> B \<Longrightarrow> disjoint_family_on f B \<Longrightarrow> disjoint_family_on f A"
   845   unfolding disjoint_family_on_def by auto
   846 
   847 lemma disjoint_family_Suc:
   848   assumes Suc: "!!n. A n \<subseteq> A (Suc n)"
   849   shows "disjoint_family (\<lambda>i. A (Suc i) - A i)"
   850 proof -
   851   {
   852     fix m
   853     have "!!n. A n \<subseteq> A (m+n)"
   854     proof (induct m)
   855       case 0 show ?case by simp
   856     next
   857       case (Suc m) thus ?case
   858         by (metis Suc_eq_plus1 assms nat_add_commute nat_add_left_commute subset_trans)
   859     qed
   860   }
   861   hence "!!m n. m < n \<Longrightarrow> A m \<subseteq> A n"
   862     by (metis add_commute le_add_diff_inverse nat_less_le)
   863   thus ?thesis
   864     by (auto simp add: disjoint_family_on_def)
   865       (metis insert_absorb insert_subset le_SucE le_antisym not_leE)
   866 qed
   867 
   868 lemma setsum_indicator_disjoint_family:
   869   fixes f :: "'d \<Rightarrow> 'e::semiring_1"
   870   assumes d: "disjoint_family_on A P" and "x \<in> A j" and "finite P" and "j \<in> P"
   871   shows "(\<Sum>i\<in>P. f i * indicator (A i) x) = f j"
   872 proof -
   873   have "P \<inter> {i. x \<in> A i} = {j}"
   874     using d `x \<in> A j` `j \<in> P` unfolding disjoint_family_on_def
   875     by auto
   876   thus ?thesis
   877     unfolding indicator_def
   878     by (simp add: if_distrib setsum_cases[OF `finite P`])
   879 qed
   880 
   881 definition disjointed :: "(nat \<Rightarrow> 'a set) \<Rightarrow> nat \<Rightarrow> 'a set "
   882   where "disjointed A n = A n - (\<Union>i\<in>{0..<n}. A i)"
   883 
   884 lemma finite_UN_disjointed_eq: "(\<Union>i\<in>{0..<n}. disjointed A i) = (\<Union>i\<in>{0..<n}. A i)"
   885 proof (induct n)
   886   case 0 show ?case by simp
   887 next
   888   case (Suc n)
   889   thus ?case by (simp add: atLeastLessThanSuc disjointed_def)
   890 qed
   891 
   892 lemma UN_disjointed_eq: "(\<Union>i. disjointed A i) = (\<Union>i. A i)"
   893   apply (rule UN_finite2_eq [where k=0])
   894   apply (simp add: finite_UN_disjointed_eq)
   895   done
   896 
   897 lemma less_disjoint_disjointed: "m<n \<Longrightarrow> disjointed A m \<inter> disjointed A n = {}"
   898   by (auto simp add: disjointed_def)
   899 
   900 lemma disjoint_family_disjointed: "disjoint_family (disjointed A)"
   901   by (simp add: disjoint_family_on_def)
   902      (metis neq_iff Int_commute less_disjoint_disjointed)
   903 
   904 lemma disjointed_subset: "disjointed A n \<subseteq> A n"
   905   by (auto simp add: disjointed_def)
   906 
   907 lemma (in ring_of_sets) UNION_in_sets:
   908   fixes A:: "nat \<Rightarrow> 'a set"
   909   assumes A: "range A \<subseteq> sets M "
   910   shows  "(\<Union>i\<in>{0..<n}. A i) \<in> sets M"
   911 proof (induct n)
   912   case 0 show ?case by simp
   913 next
   914   case (Suc n)
   915   thus ?case
   916     by (simp add: atLeastLessThanSuc) (metis A Un UNIV_I image_subset_iff)
   917 qed
   918 
   919 lemma (in ring_of_sets) range_disjointed_sets:
   920   assumes A: "range A \<subseteq> sets M "
   921   shows  "range (disjointed A) \<subseteq> sets M"
   922 proof (auto simp add: disjointed_def)
   923   fix n
   924   show "A n - (\<Union>i\<in>{0..<n}. A i) \<in> sets M" using UNION_in_sets
   925     by (metis A Diff UNIV_I image_subset_iff)
   926 qed
   927 
   928 lemma (in algebra) range_disjointed_sets':
   929   "range A \<subseteq> sets M \<Longrightarrow> range (disjointed A) \<subseteq> sets M"
   930   using range_disjointed_sets .
   931 
   932 lemma disjointed_0[simp]: "disjointed A 0 = A 0"
   933   by (simp add: disjointed_def)
   934 
   935 lemma incseq_Un:
   936   "incseq A \<Longrightarrow> (\<Union>i\<le>n. A i) = A n"
   937   unfolding incseq_def by auto
   938 
   939 lemma disjointed_incseq:
   940   "incseq A \<Longrightarrow> disjointed A (Suc n) = A (Suc n) - A n"
   941   using incseq_Un[of A]
   942   by (simp add: disjointed_def atLeastLessThanSuc_atLeastAtMost atLeast0AtMost)
   943 
   944 lemma sigma_algebra_disjoint_iff:
   945      "sigma_algebra M \<longleftrightarrow>
   946       algebra M &
   947       (\<forall>A. range A \<subseteq> sets M \<longrightarrow> disjoint_family A \<longrightarrow>
   948            (\<Union>i::nat. A i) \<in> sets M)"
   949 proof (auto simp add: sigma_algebra_iff)
   950   fix A :: "nat \<Rightarrow> 'a set"
   951   assume M: "algebra M"
   952      and A: "range A \<subseteq> sets M"
   953      and UnA: "\<forall>A. range A \<subseteq> sets M \<longrightarrow>
   954                disjoint_family A \<longrightarrow> (\<Union>i::nat. A i) \<in> sets M"
   955   hence "range (disjointed A) \<subseteq> sets M \<longrightarrow>
   956          disjoint_family (disjointed A) \<longrightarrow>
   957          (\<Union>i. disjointed A i) \<in> sets M" by blast
   958   hence "(\<Union>i. disjointed A i) \<in> sets M"
   959     by (simp add: algebra.range_disjointed_sets' M A disjoint_family_disjointed)
   960   thus "(\<Union>i::nat. A i) \<in> sets M" by (simp add: UN_disjointed_eq)
   961 qed
   962 
   963 subsection {* Sigma algebra generated by function preimages *}
   964 
   965 definition (in sigma_algebra)
   966   "vimage_algebra S f = \<lparr> space = S, sets = (\<lambda>A. f -` A \<inter> S) ` sets M, \<dots> = more M \<rparr>"
   967 
   968 lemma (in sigma_algebra) in_vimage_algebra[simp]:
   969   "A \<in> sets (vimage_algebra S f) \<longleftrightarrow> (\<exists>B\<in>sets M. A = f -` B \<inter> S)"
   970   by (simp add: vimage_algebra_def image_iff)
   971 
   972 lemma (in sigma_algebra) space_vimage_algebra[simp]:
   973   "space (vimage_algebra S f) = S"
   974   by (simp add: vimage_algebra_def)
   975 
   976 lemma (in sigma_algebra) sigma_algebra_preimages:
   977   fixes f :: "'x \<Rightarrow> 'a"
   978   assumes "f \<in> A \<rightarrow> space M"
   979   shows "sigma_algebra \<lparr> space = A, sets = (\<lambda>M. f -` M \<inter> A) ` sets M \<rparr>"
   980     (is "sigma_algebra \<lparr> space = _, sets = ?F ` sets M \<rparr>")
   981 proof (simp add: sigma_algebra_iff2, safe)
   982   show "{} \<in> ?F ` sets M" by blast
   983 next
   984   fix S assume "S \<in> sets M"
   985   moreover have "A - ?F S = ?F (space M - S)"
   986     using assms by auto
   987   ultimately show "A - ?F S \<in> ?F ` sets M"
   988     by blast
   989 next
   990   fix S :: "nat \<Rightarrow> 'x set" assume *: "range S \<subseteq> ?F ` sets M"
   991   have "\<forall>i. \<exists>b. b \<in> sets M \<and> S i = ?F b"
   992   proof safe
   993     fix i
   994     have "S i \<in> ?F ` sets M" using * by auto
   995     then show "\<exists>b. b \<in> sets M \<and> S i = ?F b" by auto
   996   qed
   997   from choice[OF this] obtain b where b: "range b \<subseteq> sets M" "\<And>i. S i = ?F (b i)"
   998     by auto
   999   then have "(\<Union>i. S i) = ?F (\<Union>i. b i)" by auto
  1000   then show "(\<Union>i. S i) \<in> ?F ` sets M" using b(1) by blast
  1001 qed
  1002 
  1003 lemma (in sigma_algebra) sigma_algebra_vimage:
  1004   fixes S :: "'c set" assumes "f \<in> S \<rightarrow> space M"
  1005   shows "sigma_algebra (vimage_algebra S f)"
  1006 proof -
  1007   from sigma_algebra_preimages[OF assms]
  1008   show ?thesis unfolding vimage_algebra_def by (auto simp: sigma_algebra_iff2)
  1009 qed
  1010 
  1011 lemma (in sigma_algebra) measurable_vimage_algebra:
  1012   fixes S :: "'c set" assumes "f \<in> S \<rightarrow> space M"
  1013   shows "f \<in> measurable (vimage_algebra S f) M"
  1014     unfolding measurable_def using assms by force
  1015 
  1016 lemma (in sigma_algebra) measurable_vimage:
  1017   fixes g :: "'a \<Rightarrow> 'c" and f :: "'d \<Rightarrow> 'a"
  1018   assumes "g \<in> measurable M M2" "f \<in> S \<rightarrow> space M"
  1019   shows "(\<lambda>x. g (f x)) \<in> measurable (vimage_algebra S f) M2"
  1020 proof -
  1021   note measurable_vimage_algebra[OF assms(2)]
  1022   from measurable_comp[OF this assms(1)]
  1023   show ?thesis by (simp add: comp_def)
  1024 qed
  1025 
  1026 lemma sigma_sets_vimage:
  1027   assumes "f \<in> S' \<rightarrow> S" and "A \<subseteq> Pow S"
  1028   shows "sigma_sets S' ((\<lambda>X. f -` X \<inter> S') ` A) = (\<lambda>X. f -` X \<inter> S') ` sigma_sets S A"
  1029 proof (intro set_eqI iffI)
  1030   let ?F = "\<lambda>X. f -` X \<inter> S'"
  1031   fix X assume "X \<in> sigma_sets S' (?F ` A)"
  1032   then show "X \<in> ?F ` sigma_sets S A"
  1033   proof induct
  1034     case (Basic X) then obtain X' where "X = ?F X'" "X' \<in> A"
  1035       by auto
  1036     then show ?case by (auto intro!: sigma_sets.Basic)
  1037   next
  1038     case Empty then show ?case
  1039       by (auto intro!: image_eqI[of _ _ "{}"] sigma_sets.Empty)
  1040   next
  1041     case (Compl X) then obtain X' where X: "X = ?F X'" and "X' \<in> sigma_sets S A"
  1042       by auto
  1043     then have "S - X' \<in> sigma_sets S A"
  1044       by (auto intro!: sigma_sets.Compl)
  1045     then show ?case
  1046       using X assms by (auto intro!: image_eqI[where x="S - X'"])
  1047   next
  1048     case (Union F)
  1049     then have "\<forall>i. \<exists>F'.  F' \<in> sigma_sets S A \<and> F i = f -` F' \<inter> S'"
  1050       by (auto simp: image_iff Bex_def)
  1051     from choice[OF this] obtain F' where
  1052       "\<And>i. F' i \<in> sigma_sets S A" and "\<And>i. F i = f -` F' i \<inter> S'"
  1053       by auto
  1054     then show ?case
  1055       by (auto intro!: sigma_sets.Union image_eqI[where x="\<Union>i. F' i"])
  1056   qed
  1057 next
  1058   let ?F = "\<lambda>X. f -` X \<inter> S'"
  1059   fix X assume "X \<in> ?F ` sigma_sets S A"
  1060   then obtain X' where "X' \<in> sigma_sets S A" "X = ?F X'" by auto
  1061   then show "X \<in> sigma_sets S' (?F ` A)"
  1062   proof (induct arbitrary: X)
  1063     case (Basic X') then show ?case by (auto intro: sigma_sets.Basic)
  1064   next
  1065     case Empty then show ?case by (auto intro: sigma_sets.Empty)
  1066   next
  1067     case (Compl X')
  1068     have "S' - (S' - X) \<in> sigma_sets S' (?F ` A)"
  1069       apply (rule sigma_sets.Compl)
  1070       using assms by (auto intro!: Compl.hyps simp: Compl.prems)
  1071     also have "S' - (S' - X) = X"
  1072       using assms Compl by auto
  1073     finally show ?case .
  1074   next
  1075     case (Union F)
  1076     have "(\<Union>i. f -` F i \<inter> S') \<in> sigma_sets S' (?F ` A)"
  1077       by (intro sigma_sets.Union Union.hyps) simp
  1078     also have "(\<Union>i. f -` F i \<inter> S') = X"
  1079       using assms Union by auto
  1080     finally show ?case .
  1081   qed
  1082 qed
  1083 
  1084 section {* Conditional space *}
  1085 
  1086 definition (in algebra)
  1087   "image_space X = \<lparr> space = X`space M, sets = (\<lambda>S. X`S) ` sets M, \<dots> = more M \<rparr>"
  1088 
  1089 definition (in algebra)
  1090   "conditional_space X A = algebra.image_space (restricted_space A) X"
  1091 
  1092 lemma (in algebra) space_conditional_space:
  1093   assumes "A \<in> sets M" shows "space (conditional_space X A) = X`A"
  1094 proof -
  1095   interpret r: algebra "restricted_space A" using assms by (rule restricted_algebra)
  1096   show ?thesis unfolding conditional_space_def r.image_space_def
  1097     by simp
  1098 qed
  1099 
  1100 subsection {* A Two-Element Series *}
  1101 
  1102 definition binaryset :: "'a set \<Rightarrow> 'a set \<Rightarrow> nat \<Rightarrow> 'a set "
  1103   where "binaryset A B = (\<lambda>\<^isup>x. {})(0 := A, Suc 0 := B)"
  1104 
  1105 lemma range_binaryset_eq: "range(binaryset A B) = {A,B,{}}"
  1106   apply (simp add: binaryset_def)
  1107   apply (rule set_eqI)
  1108   apply (auto simp add: image_iff)
  1109   done
  1110 
  1111 lemma UN_binaryset_eq: "(\<Union>i. binaryset A B i) = A \<union> B"
  1112   by (simp add: SUP_def range_binaryset_eq)
  1113 
  1114 section {* Closed CDI *}
  1115 
  1116 definition
  1117   closed_cdi  where
  1118   "closed_cdi M \<longleftrightarrow>
  1119    sets M \<subseteq> Pow (space M) &
  1120    (\<forall>s \<in> sets M. space M - s \<in> sets M) &
  1121    (\<forall>A. (range A \<subseteq> sets M) & (A 0 = {}) & (\<forall>n. A n \<subseteq> A (Suc n)) \<longrightarrow>
  1122         (\<Union>i. A i) \<in> sets M) &
  1123    (\<forall>A. (range A \<subseteq> sets M) & disjoint_family A \<longrightarrow> (\<Union>i::nat. A i) \<in> sets M)"
  1124 
  1125 inductive_set
  1126   smallest_ccdi_sets :: "('a, 'b) algebra_scheme \<Rightarrow> 'a set set"
  1127   for M
  1128   where
  1129     Basic [intro]:
  1130       "a \<in> sets M \<Longrightarrow> a \<in> smallest_ccdi_sets M"
  1131   | Compl [intro]:
  1132       "a \<in> smallest_ccdi_sets M \<Longrightarrow> space M - a \<in> smallest_ccdi_sets M"
  1133   | Inc:
  1134       "range A \<in> Pow(smallest_ccdi_sets M) \<Longrightarrow> A 0 = {} \<Longrightarrow> (\<And>n. A n \<subseteq> A (Suc n))
  1135        \<Longrightarrow> (\<Union>i. A i) \<in> smallest_ccdi_sets M"
  1136   | Disj:
  1137       "range A \<in> Pow(smallest_ccdi_sets M) \<Longrightarrow> disjoint_family A
  1138        \<Longrightarrow> (\<Union>i::nat. A i) \<in> smallest_ccdi_sets M"
  1139 
  1140 
  1141 definition
  1142   smallest_closed_cdi  where
  1143   "smallest_closed_cdi M = (|space = space M, sets = smallest_ccdi_sets M|)"
  1144 
  1145 lemma space_smallest_closed_cdi [simp]:
  1146      "space (smallest_closed_cdi M) = space M"
  1147   by (simp add: smallest_closed_cdi_def)
  1148 
  1149 lemma (in algebra) smallest_closed_cdi1: "sets M \<subseteq> sets (smallest_closed_cdi M)"
  1150   by (auto simp add: smallest_closed_cdi_def)
  1151 
  1152 lemma (in algebra) smallest_ccdi_sets:
  1153      "smallest_ccdi_sets M \<subseteq> Pow (space M)"
  1154   apply (rule subsetI)
  1155   apply (erule smallest_ccdi_sets.induct)
  1156   apply (auto intro: range_subsetD dest: sets_into_space)
  1157   done
  1158 
  1159 lemma (in algebra) smallest_closed_cdi2: "closed_cdi (smallest_closed_cdi M)"
  1160   apply (auto simp add: closed_cdi_def smallest_closed_cdi_def smallest_ccdi_sets)
  1161   apply (blast intro: smallest_ccdi_sets.Inc smallest_ccdi_sets.Disj) +
  1162   done
  1163 
  1164 lemma (in algebra) smallest_closed_cdi3:
  1165      "sets (smallest_closed_cdi M) \<subseteq> Pow (space M)"
  1166   by (simp add: smallest_closed_cdi_def smallest_ccdi_sets)
  1167 
  1168 lemma closed_cdi_subset: "closed_cdi M \<Longrightarrow> sets M \<subseteq> Pow (space M)"
  1169   by (simp add: closed_cdi_def)
  1170 
  1171 lemma closed_cdi_Compl: "closed_cdi M \<Longrightarrow> s \<in> sets M \<Longrightarrow> space M - s \<in> sets M"
  1172   by (simp add: closed_cdi_def)
  1173 
  1174 lemma closed_cdi_Inc:
  1175      "closed_cdi M \<Longrightarrow> range A \<subseteq> sets M \<Longrightarrow> A 0 = {} \<Longrightarrow> (!!n. A n \<subseteq> A (Suc n)) \<Longrightarrow>
  1176         (\<Union>i. A i) \<in> sets M"
  1177   by (simp add: closed_cdi_def)
  1178 
  1179 lemma closed_cdi_Disj:
  1180      "closed_cdi M \<Longrightarrow> range A \<subseteq> sets M \<Longrightarrow> disjoint_family A \<Longrightarrow> (\<Union>i::nat. A i) \<in> sets M"
  1181   by (simp add: closed_cdi_def)
  1182 
  1183 lemma closed_cdi_Un:
  1184   assumes cdi: "closed_cdi M" and empty: "{} \<in> sets M"
  1185       and A: "A \<in> sets M" and B: "B \<in> sets M"
  1186       and disj: "A \<inter> B = {}"
  1187     shows "A \<union> B \<in> sets M"
  1188 proof -
  1189   have ra: "range (binaryset A B) \<subseteq> sets M"
  1190    by (simp add: range_binaryset_eq empty A B)
  1191  have di:  "disjoint_family (binaryset A B)" using disj
  1192    by (simp add: disjoint_family_on_def binaryset_def Int_commute)
  1193  from closed_cdi_Disj [OF cdi ra di]
  1194  show ?thesis
  1195    by (simp add: UN_binaryset_eq)
  1196 qed
  1197 
  1198 lemma (in algebra) smallest_ccdi_sets_Un:
  1199   assumes A: "A \<in> smallest_ccdi_sets M" and B: "B \<in> smallest_ccdi_sets M"
  1200       and disj: "A \<inter> B = {}"
  1201     shows "A \<union> B \<in> smallest_ccdi_sets M"
  1202 proof -
  1203   have ra: "range (binaryset A B) \<in> Pow (smallest_ccdi_sets M)"
  1204     by (simp add: range_binaryset_eq  A B smallest_ccdi_sets.Basic)
  1205   have di:  "disjoint_family (binaryset A B)" using disj
  1206     by (simp add: disjoint_family_on_def binaryset_def Int_commute)
  1207   from Disj [OF ra di]
  1208   show ?thesis
  1209     by (simp add: UN_binaryset_eq)
  1210 qed
  1211 
  1212 lemma (in algebra) smallest_ccdi_sets_Int1:
  1213   assumes a: "a \<in> sets M"
  1214   shows "b \<in> smallest_ccdi_sets M \<Longrightarrow> a \<inter> b \<in> smallest_ccdi_sets M"
  1215 proof (induct rule: smallest_ccdi_sets.induct)
  1216   case (Basic x)
  1217   thus ?case
  1218     by (metis a Int smallest_ccdi_sets.Basic)
  1219 next
  1220   case (Compl x)
  1221   have "a \<inter> (space M - x) = space M - ((space M - a) \<union> (a \<inter> x))"
  1222     by blast
  1223   also have "... \<in> smallest_ccdi_sets M"
  1224     by (metis smallest_ccdi_sets.Compl a Compl(2) Diff_Int2 Diff_Int_distrib2
  1225            Diff_disjoint Int_Diff Int_empty_right Un_commute
  1226            smallest_ccdi_sets.Basic smallest_ccdi_sets.Compl
  1227            smallest_ccdi_sets_Un)
  1228   finally show ?case .
  1229 next
  1230   case (Inc A)
  1231   have 1: "(\<Union>i. (\<lambda>i. a \<inter> A i) i) = a \<inter> (\<Union>i. A i)"
  1232     by blast
  1233   have "range (\<lambda>i. a \<inter> A i) \<in> Pow(smallest_ccdi_sets M)" using Inc
  1234     by blast
  1235   moreover have "(\<lambda>i. a \<inter> A i) 0 = {}"
  1236     by (simp add: Inc)
  1237   moreover have "!!n. (\<lambda>i. a \<inter> A i) n \<subseteq> (\<lambda>i. a \<inter> A i) (Suc n)" using Inc
  1238     by blast
  1239   ultimately have 2: "(\<Union>i. (\<lambda>i. a \<inter> A i) i) \<in> smallest_ccdi_sets M"
  1240     by (rule smallest_ccdi_sets.Inc)
  1241   show ?case
  1242     by (metis 1 2)
  1243 next
  1244   case (Disj A)
  1245   have 1: "(\<Union>i. (\<lambda>i. a \<inter> A i) i) = a \<inter> (\<Union>i. A i)"
  1246     by blast
  1247   have "range (\<lambda>i. a \<inter> A i) \<in> Pow(smallest_ccdi_sets M)" using Disj
  1248     by blast
  1249   moreover have "disjoint_family (\<lambda>i. a \<inter> A i)" using Disj
  1250     by (auto simp add: disjoint_family_on_def)
  1251   ultimately have 2: "(\<Union>i. (\<lambda>i. a \<inter> A i) i) \<in> smallest_ccdi_sets M"
  1252     by (rule smallest_ccdi_sets.Disj)
  1253   show ?case
  1254     by (metis 1 2)
  1255 qed
  1256 
  1257 
  1258 lemma (in algebra) smallest_ccdi_sets_Int:
  1259   assumes b: "b \<in> smallest_ccdi_sets M"
  1260   shows "a \<in> smallest_ccdi_sets M \<Longrightarrow> a \<inter> b \<in> smallest_ccdi_sets M"
  1261 proof (induct rule: smallest_ccdi_sets.induct)
  1262   case (Basic x)
  1263   thus ?case
  1264     by (metis b smallest_ccdi_sets_Int1)
  1265 next
  1266   case (Compl x)
  1267   have "(space M - x) \<inter> b = space M - (x \<inter> b \<union> (space M - b))"
  1268     by blast
  1269   also have "... \<in> smallest_ccdi_sets M"
  1270     by (metis Compl(2) Diff_disjoint Int_Diff Int_commute Int_empty_right b
  1271            smallest_ccdi_sets.Compl smallest_ccdi_sets_Un)
  1272   finally show ?case .
  1273 next
  1274   case (Inc A)
  1275   have 1: "(\<Union>i. (\<lambda>i. A i \<inter> b) i) = (\<Union>i. A i) \<inter> b"
  1276     by blast
  1277   have "range (\<lambda>i. A i \<inter> b) \<in> Pow(smallest_ccdi_sets M)" using Inc
  1278     by blast
  1279   moreover have "(\<lambda>i. A i \<inter> b) 0 = {}"
  1280     by (simp add: Inc)
  1281   moreover have "!!n. (\<lambda>i. A i \<inter> b) n \<subseteq> (\<lambda>i. A i \<inter> b) (Suc n)" using Inc
  1282     by blast
  1283   ultimately have 2: "(\<Union>i. (\<lambda>i. A i \<inter> b) i) \<in> smallest_ccdi_sets M"
  1284     by (rule smallest_ccdi_sets.Inc)
  1285   show ?case
  1286     by (metis 1 2)
  1287 next
  1288   case (Disj A)
  1289   have 1: "(\<Union>i. (\<lambda>i. A i \<inter> b) i) = (\<Union>i. A i) \<inter> b"
  1290     by blast
  1291   have "range (\<lambda>i. A i \<inter> b) \<in> Pow(smallest_ccdi_sets M)" using Disj
  1292     by blast
  1293   moreover have "disjoint_family (\<lambda>i. A i \<inter> b)" using Disj
  1294     by (auto simp add: disjoint_family_on_def)
  1295   ultimately have 2: "(\<Union>i. (\<lambda>i. A i \<inter> b) i) \<in> smallest_ccdi_sets M"
  1296     by (rule smallest_ccdi_sets.Disj)
  1297   show ?case
  1298     by (metis 1 2)
  1299 qed
  1300 
  1301 lemma (in algebra) sets_smallest_closed_cdi_Int:
  1302    "a \<in> sets (smallest_closed_cdi M) \<Longrightarrow> b \<in> sets (smallest_closed_cdi M)
  1303     \<Longrightarrow> a \<inter> b \<in> sets (smallest_closed_cdi M)"
  1304   by (simp add: smallest_ccdi_sets_Int smallest_closed_cdi_def)
  1305 
  1306 lemma (in algebra) sigma_property_disjoint_lemma:
  1307   assumes sbC: "sets M \<subseteq> C"
  1308       and ccdi: "closed_cdi (|space = space M, sets = C|)"
  1309   shows "sigma_sets (space M) (sets M) \<subseteq> C"
  1310 proof -
  1311   have "smallest_ccdi_sets M \<in> {B . sets M \<subseteq> B \<and> sigma_algebra (|space = space M, sets = B|)}"
  1312     apply (auto simp add: sigma_algebra_disjoint_iff algebra_iff_Int
  1313             smallest_ccdi_sets_Int)
  1314     apply (metis Union_Pow_eq Union_upper subsetD smallest_ccdi_sets)
  1315     apply (blast intro: smallest_ccdi_sets.Disj)
  1316     done
  1317   hence "sigma_sets (space M) (sets M) \<subseteq> smallest_ccdi_sets M"
  1318     by clarsimp
  1319        (drule sigma_algebra.sigma_sets_subset [where a="sets M"], auto)
  1320   also have "...  \<subseteq> C"
  1321     proof
  1322       fix x
  1323       assume x: "x \<in> smallest_ccdi_sets M"
  1324       thus "x \<in> C"
  1325         proof (induct rule: smallest_ccdi_sets.induct)
  1326           case (Basic x)
  1327           thus ?case
  1328             by (metis Basic subsetD sbC)
  1329         next
  1330           case (Compl x)
  1331           thus ?case
  1332             by (blast intro: closed_cdi_Compl [OF ccdi, simplified])
  1333         next
  1334           case (Inc A)
  1335           thus ?case
  1336                by (auto intro: closed_cdi_Inc [OF ccdi, simplified])
  1337         next
  1338           case (Disj A)
  1339           thus ?case
  1340                by (auto intro: closed_cdi_Disj [OF ccdi, simplified])
  1341         qed
  1342     qed
  1343   finally show ?thesis .
  1344 qed
  1345 
  1346 lemma (in algebra) sigma_property_disjoint:
  1347   assumes sbC: "sets M \<subseteq> C"
  1348       and compl: "!!s. s \<in> C \<inter> sigma_sets (space M) (sets M) \<Longrightarrow> space M - s \<in> C"
  1349       and inc: "!!A. range A \<subseteq> C \<inter> sigma_sets (space M) (sets M)
  1350                      \<Longrightarrow> A 0 = {} \<Longrightarrow> (!!n. A n \<subseteq> A (Suc n))
  1351                      \<Longrightarrow> (\<Union>i. A i) \<in> C"
  1352       and disj: "!!A. range A \<subseteq> C \<inter> sigma_sets (space M) (sets M)
  1353                       \<Longrightarrow> disjoint_family A \<Longrightarrow> (\<Union>i::nat. A i) \<in> C"
  1354   shows "sigma_sets (space M) (sets M) \<subseteq> C"
  1355 proof -
  1356   have "sigma_sets (space M) (sets M) \<subseteq> C \<inter> sigma_sets (space M) (sets M)"
  1357     proof (rule sigma_property_disjoint_lemma)
  1358       show "sets M \<subseteq> C \<inter> sigma_sets (space M) (sets M)"
  1359         by (metis Int_greatest Set.subsetI sbC sigma_sets.Basic)
  1360     next
  1361       show "closed_cdi \<lparr>space = space M, sets = C \<inter> sigma_sets (space M) (sets M)\<rparr>"
  1362         by (simp add: closed_cdi_def compl inc disj)
  1363            (metis PowI Set.subsetI le_infI2 sigma_sets_into_sp space_closed
  1364              IntE sigma_sets.Compl range_subsetD sigma_sets.Union)
  1365     qed
  1366   thus ?thesis
  1367     by blast
  1368 qed
  1369 
  1370 section {* Dynkin systems *}
  1371 
  1372 locale dynkin_system = subset_class +
  1373   assumes space: "space M \<in> sets M"
  1374     and   compl[intro!]: "\<And>A. A \<in> sets M \<Longrightarrow> space M - A \<in> sets M"
  1375     and   UN[intro!]: "\<And>A. disjoint_family A \<Longrightarrow> range A \<subseteq> sets M
  1376                            \<Longrightarrow> (\<Union>i::nat. A i) \<in> sets M"
  1377 
  1378 lemma (in dynkin_system) empty[intro, simp]: "{} \<in> sets M"
  1379   using space compl[of "space M"] by simp
  1380 
  1381 lemma (in dynkin_system) diff:
  1382   assumes sets: "D \<in> sets M" "E \<in> sets M" and "D \<subseteq> E"
  1383   shows "E - D \<in> sets M"
  1384 proof -
  1385   let ?f = "\<lambda>x. if x = 0 then D else if x = Suc 0 then space M - E else {}"
  1386   have "range ?f = {D, space M - E, {}}"
  1387     by (auto simp: image_iff)
  1388   moreover have "D \<union> (space M - E) = (\<Union>i. ?f i)"
  1389     by (auto simp: image_iff split: split_if_asm)
  1390   moreover
  1391   then have "disjoint_family ?f" unfolding disjoint_family_on_def
  1392     using `D \<in> sets M`[THEN sets_into_space] `D \<subseteq> E` by auto
  1393   ultimately have "space M - (D \<union> (space M - E)) \<in> sets M"
  1394     using sets by auto
  1395   also have "space M - (D \<union> (space M - E)) = E - D"
  1396     using assms sets_into_space by auto
  1397   finally show ?thesis .
  1398 qed
  1399 
  1400 lemma dynkin_systemI:
  1401   assumes "\<And> A. A \<in> sets M \<Longrightarrow> A \<subseteq> space M" "space M \<in> sets M"
  1402   assumes "\<And> A. A \<in> sets M \<Longrightarrow> space M - A \<in> sets M"
  1403   assumes "\<And> A. disjoint_family A \<Longrightarrow> range A \<subseteq> sets M
  1404           \<Longrightarrow> (\<Union>i::nat. A i) \<in> sets M"
  1405   shows "dynkin_system M"
  1406   using assms by (auto simp: dynkin_system_def dynkin_system_axioms_def subset_class_def)
  1407 
  1408 lemma dynkin_systemI':
  1409   assumes 1: "\<And> A. A \<in> sets M \<Longrightarrow> A \<subseteq> space M"
  1410   assumes empty: "{} \<in> sets M"
  1411   assumes Diff: "\<And> A. A \<in> sets M \<Longrightarrow> space M - A \<in> sets M"
  1412   assumes 2: "\<And> A. disjoint_family A \<Longrightarrow> range A \<subseteq> sets M
  1413           \<Longrightarrow> (\<Union>i::nat. A i) \<in> sets M"
  1414   shows "dynkin_system M"
  1415 proof -
  1416   from Diff[OF empty] have "space M \<in> sets M" by auto
  1417   from 1 this Diff 2 show ?thesis
  1418     by (intro dynkin_systemI) auto
  1419 qed
  1420 
  1421 lemma dynkin_system_trivial:
  1422   shows "dynkin_system \<lparr> space = A, sets = Pow A \<rparr>"
  1423   by (rule dynkin_systemI) auto
  1424 
  1425 lemma sigma_algebra_imp_dynkin_system:
  1426   assumes "sigma_algebra M" shows "dynkin_system M"
  1427 proof -
  1428   interpret sigma_algebra M by fact
  1429   show ?thesis using sets_into_space by (fastforce intro!: dynkin_systemI)
  1430 qed
  1431 
  1432 subsection "Intersection stable algebras"
  1433 
  1434 definition "Int_stable M \<longleftrightarrow> (\<forall> a \<in> sets M. \<forall> b \<in> sets M. a \<inter> b \<in> sets M)"
  1435 
  1436 lemma (in algebra) Int_stable: "Int_stable M"
  1437   unfolding Int_stable_def by auto
  1438 
  1439 lemma Int_stableI:
  1440   "(\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<inter> b \<in> A) \<Longrightarrow> Int_stable \<lparr> space = \<Omega>, sets = A \<rparr>"
  1441   unfolding Int_stable_def by auto
  1442 
  1443 lemma Int_stableD:
  1444   "Int_stable M \<Longrightarrow> a \<in> sets M \<Longrightarrow> b \<in> sets M \<Longrightarrow> a \<inter> b \<in> sets M"
  1445   unfolding Int_stable_def by auto
  1446 
  1447 lemma (in dynkin_system) sigma_algebra_eq_Int_stable:
  1448   "sigma_algebra M \<longleftrightarrow> Int_stable M"
  1449 proof
  1450   assume "sigma_algebra M" then show "Int_stable M"
  1451     unfolding sigma_algebra_def using algebra.Int_stable by auto
  1452 next
  1453   assume "Int_stable M"
  1454   show "sigma_algebra M"
  1455     unfolding sigma_algebra_disjoint_iff algebra_iff_Un
  1456   proof (intro conjI ballI allI impI)
  1457     show "sets M \<subseteq> Pow (space M)" using sets_into_space by auto
  1458   next
  1459     fix A B assume "A \<in> sets M" "B \<in> sets M"
  1460     then have "A \<union> B = space M - ((space M - A) \<inter> (space M - B))"
  1461               "space M - A \<in> sets M" "space M - B \<in> sets M"
  1462       using sets_into_space by auto
  1463     then show "A \<union> B \<in> sets M"
  1464       using `Int_stable M` unfolding Int_stable_def by auto
  1465   qed auto
  1466 qed
  1467 
  1468 subsection "Smallest Dynkin systems"
  1469 
  1470 definition dynkin where
  1471   "dynkin M = \<lparr> space = space M,
  1472      sets = \<Inter>{D. dynkin_system \<lparr> space = space M, sets = D \<rparr> \<and> sets M \<subseteq> D},
  1473      \<dots> = more M \<rparr>"
  1474 
  1475 lemma dynkin_system_dynkin:
  1476   assumes "sets M \<subseteq> Pow (space M)"
  1477   shows "dynkin_system (dynkin M)"
  1478 proof (rule dynkin_systemI)
  1479   fix A assume "A \<in> sets (dynkin M)"
  1480   moreover
  1481   { fix D assume "A \<in> D" and d: "dynkin_system \<lparr> space = space M, sets = D \<rparr>"
  1482     then have "A \<subseteq> space M" by (auto simp: dynkin_system_def subset_class_def) }
  1483   moreover have "{D. dynkin_system \<lparr> space = space M, sets = D\<rparr> \<and> sets M \<subseteq> D} \<noteq> {}"
  1484     using assms dynkin_system_trivial by fastforce
  1485   ultimately show "A \<subseteq> space (dynkin M)"
  1486     unfolding dynkin_def using assms
  1487     by simp (metis dynkin_system_def subset_class_def in_mono)
  1488 next
  1489   show "space (dynkin M) \<in> sets (dynkin M)"
  1490     unfolding dynkin_def using dynkin_system.space by fastforce
  1491 next
  1492   fix A assume "A \<in> sets (dynkin M)"
  1493   then show "space (dynkin M) - A \<in> sets (dynkin M)"
  1494     unfolding dynkin_def using dynkin_system.compl by force
  1495 next
  1496   fix A :: "nat \<Rightarrow> 'a set"
  1497   assume A: "disjoint_family A" "range A \<subseteq> sets (dynkin M)"
  1498   show "(\<Union>i. A i) \<in> sets (dynkin M)" unfolding dynkin_def
  1499   proof (simp, safe)
  1500     fix D assume "dynkin_system \<lparr>space = space M, sets = D\<rparr>" "sets M \<subseteq> D"
  1501     with A have "(\<Union>i. A i) \<in> sets \<lparr>space = space M, sets = D\<rparr>"
  1502       by (intro dynkin_system.UN) (auto simp: dynkin_def)
  1503     then show "(\<Union>i. A i) \<in> D" by auto
  1504   qed
  1505 qed
  1506 
  1507 lemma dynkin_Basic[intro]:
  1508   "A \<in> sets M \<Longrightarrow> A \<in> sets (dynkin M)"
  1509   unfolding dynkin_def by auto
  1510 
  1511 lemma dynkin_space[simp]:
  1512   "space (dynkin M) = space M"
  1513   unfolding dynkin_def by auto
  1514 
  1515 lemma (in dynkin_system) restricted_dynkin_system:
  1516   assumes "D \<in> sets M"
  1517   shows "dynkin_system \<lparr> space = space M,
  1518                          sets = {Q. Q \<subseteq> space M \<and> Q \<inter> D \<in> sets M} \<rparr>"
  1519 proof (rule dynkin_systemI, simp_all)
  1520   have "space M \<inter> D = D"
  1521     using `D \<in> sets M` sets_into_space by auto
  1522   then show "space M \<inter> D \<in> sets M"
  1523     using `D \<in> sets M` by auto
  1524 next
  1525   fix A assume "A \<subseteq> space M \<and> A \<inter> D \<in> sets M"
  1526   moreover have "(space M - A) \<inter> D = (space M - (A \<inter> D)) - (space M - D)"
  1527     by auto
  1528   ultimately show "space M - A \<subseteq> space M \<and> (space M - A) \<inter> D \<in> sets M"
  1529     using  `D \<in> sets M` by (auto intro: diff)
  1530 next
  1531   fix A :: "nat \<Rightarrow> 'a set"
  1532   assume "disjoint_family A" "range A \<subseteq> {Q. Q \<subseteq> space M \<and> Q \<inter> D \<in> sets M}"
  1533   then have "\<And>i. A i \<subseteq> space M" "disjoint_family (\<lambda>i. A i \<inter> D)"
  1534     "range (\<lambda>i. A i \<inter> D) \<subseteq> sets M" "(\<Union>x. A x) \<inter> D = (\<Union>x. A x \<inter> D)"
  1535     by ((fastforce simp: disjoint_family_on_def)+)
  1536   then show "(\<Union>x. A x) \<subseteq> space M \<and> (\<Union>x. A x) \<inter> D \<in> sets M"
  1537     by (auto simp del: UN_simps)
  1538 qed
  1539 
  1540 lemma (in dynkin_system) dynkin_subset:
  1541   assumes "sets N \<subseteq> sets M"
  1542   assumes "space N = space M"
  1543   shows "sets (dynkin N) \<subseteq> sets M"
  1544 proof -
  1545   have "dynkin_system M" by default
  1546   then have "dynkin_system \<lparr>space = space N, sets = sets M \<rparr>"
  1547     using assms unfolding dynkin_system_def dynkin_system_axioms_def subset_class_def by simp
  1548   with `sets N \<subseteq> sets M` show ?thesis by (auto simp add: dynkin_def)
  1549 qed
  1550 
  1551 lemma sigma_eq_dynkin:
  1552   assumes sets: "sets M \<subseteq> Pow (space M)"
  1553   assumes "Int_stable M"
  1554   shows "sigma M = dynkin M"
  1555 proof -
  1556   have "sets (dynkin M) \<subseteq> sigma_sets (space M) (sets M)"
  1557     using sigma_algebra_imp_dynkin_system
  1558     unfolding dynkin_def sigma_def sigma_sets_least_sigma_algebra[OF sets] by auto
  1559   moreover
  1560   interpret dynkin_system "dynkin M"
  1561     using dynkin_system_dynkin[OF sets] .
  1562   have "sigma_algebra (dynkin M)"
  1563     unfolding sigma_algebra_eq_Int_stable Int_stable_def
  1564   proof (intro ballI)
  1565     fix A B assume "A \<in> sets (dynkin M)" "B \<in> sets (dynkin M)"
  1566     let ?D = "\<lambda>E. \<lparr> space = space M,
  1567                     sets = {Q. Q \<subseteq> space M \<and> Q \<inter> E \<in> sets (dynkin M)} \<rparr>"
  1568     have "sets M \<subseteq> sets (?D B)"
  1569     proof
  1570       fix E assume "E \<in> sets M"
  1571       then have "sets M \<subseteq> sets (?D E)" "E \<in> sets (dynkin M)"
  1572         using sets_into_space `Int_stable M` by (auto simp: Int_stable_def)
  1573       then have "sets (dynkin M) \<subseteq> sets (?D E)"
  1574         using restricted_dynkin_system `E \<in> sets (dynkin M)`
  1575         by (intro dynkin_system.dynkin_subset) simp_all
  1576       then have "B \<in> sets (?D E)"
  1577         using `B \<in> sets (dynkin M)` by auto
  1578       then have "E \<inter> B \<in> sets (dynkin M)"
  1579         by (subst Int_commute) simp
  1580       then show "E \<in> sets (?D B)"
  1581         using sets `E \<in> sets M` by auto
  1582     qed
  1583     then have "sets (dynkin M) \<subseteq> sets (?D B)"
  1584       using restricted_dynkin_system `B \<in> sets (dynkin M)`
  1585       by (intro dynkin_system.dynkin_subset) simp_all
  1586     then show "A \<inter> B \<in> sets (dynkin M)"
  1587       using `A \<in> sets (dynkin M)` sets_into_space by auto
  1588   qed
  1589   from sigma_algebra.sigma_sets_subset[OF this, of "sets M"]
  1590   have "sigma_sets (space M) (sets M) \<subseteq> sets (dynkin M)" by auto
  1591   ultimately have "sigma_sets (space M) (sets M) = sets (dynkin M)" by auto
  1592   then show ?thesis
  1593     by (auto intro!: algebra.equality simp: sigma_def dynkin_def)
  1594 qed
  1595 
  1596 lemma (in dynkin_system) dynkin_idem:
  1597   "dynkin M = M"
  1598 proof -
  1599   have "sets (dynkin M) = sets M"
  1600   proof
  1601     show "sets M \<subseteq> sets (dynkin M)"
  1602       using dynkin_Basic by auto
  1603     show "sets (dynkin M) \<subseteq> sets M"
  1604       by (intro dynkin_subset) auto
  1605   qed
  1606   then show ?thesis
  1607     by (auto intro!: algebra.equality simp: dynkin_def)
  1608 qed
  1609 
  1610 lemma (in dynkin_system) dynkin_lemma:
  1611   assumes "Int_stable E"
  1612   and E: "sets E \<subseteq> sets M" "space E = space M" "sets M \<subseteq> sets (sigma E)"
  1613   shows "sets (sigma E) = sets M"
  1614 proof -
  1615   have "sets E \<subseteq> Pow (space E)"
  1616     using E sets_into_space by force
  1617   then have "sigma E = dynkin E"
  1618     using `Int_stable E` by (rule sigma_eq_dynkin)
  1619   moreover then have "sets (dynkin E) = sets M"
  1620     using assms dynkin_subset[OF E(1,2)] by simp
  1621   ultimately show ?thesis
  1622     using assms by (auto intro!: algebra.equality simp: dynkin_def)
  1623 qed
  1624 
  1625 subsection "Sigma algebras on finite sets"
  1626 
  1627 locale finite_sigma_algebra = sigma_algebra +
  1628   assumes finite_space: "finite (space M)"
  1629   and sets_eq_Pow[simp]: "sets M = Pow (space M)"
  1630 
  1631 lemma (in finite_sigma_algebra) sets_image_space_eq_Pow:
  1632   "sets (image_space X) = Pow (space (image_space X))"
  1633 proof safe
  1634   fix x S assume "S \<in> sets (image_space X)" "x \<in> S"
  1635   then show "x \<in> space (image_space X)"
  1636     using sets_into_space by (auto intro!: imageI simp: image_space_def)
  1637 next
  1638   fix S assume "S \<subseteq> space (image_space X)"
  1639   then obtain S' where "S = X`S'" "S'\<in>sets M"
  1640     by (auto simp: subset_image_iff image_space_def)
  1641   then show "S \<in> sets (image_space X)"
  1642     by (auto simp: image_space_def)
  1643 qed
  1644 
  1645 lemma measurable_sigma_sigma:
  1646   assumes M: "sets M \<subseteq> Pow (space M)" and N: "sets N \<subseteq> Pow (space N)"
  1647   shows "f \<in> measurable M N \<Longrightarrow> f \<in> measurable (sigma M) (sigma N)"
  1648   using sigma_algebra.measurable_subset[OF sigma_algebra_sigma[OF M], of N]
  1649   using measurable_up_sigma[of M N] N by auto
  1650 
  1651 lemma (in sigma_algebra) measurable_Least:
  1652   assumes meas: "\<And>i::nat. {x\<in>space M. P i x} \<in> sets M"
  1653   shows "(\<lambda>x. LEAST j. P j x) -` A \<inter> space M \<in> sets M"
  1654 proof -
  1655   { fix i have "(\<lambda>x. LEAST j. P j x) -` {i} \<inter> space M \<in> sets M"
  1656     proof cases
  1657       assume i: "(LEAST j. False) = i"
  1658       have "(\<lambda>x. LEAST j. P j x) -` {i} \<inter> space M =
  1659         {x\<in>space M. P i x} \<inter> (space M - (\<Union>j<i. {x\<in>space M. P j x})) \<union> (space M - (\<Union>i. {x\<in>space M. P i x}))"
  1660         by (simp add: set_eq_iff, safe)
  1661            (insert i, auto dest: Least_le intro: LeastI intro!: Least_equality)
  1662       with meas show ?thesis
  1663         by (auto intro!: Int)
  1664     next
  1665       assume i: "(LEAST j. False) \<noteq> i"
  1666       then have "(\<lambda>x. LEAST j. P j x) -` {i} \<inter> space M =
  1667         {x\<in>space M. P i x} \<inter> (space M - (\<Union>j<i. {x\<in>space M. P j x}))"
  1668       proof (simp add: set_eq_iff, safe)
  1669         fix x assume neq: "(LEAST j. False) \<noteq> (LEAST j. P j x)"
  1670         have "\<exists>j. P j x"
  1671           by (rule ccontr) (insert neq, auto)
  1672         then show "P (LEAST j. P j x) x" by (rule LeastI_ex)
  1673       qed (auto dest: Least_le intro!: Least_equality)
  1674       with meas show ?thesis
  1675         by (auto intro!: Int)
  1676     qed }
  1677   then have "(\<Union>i\<in>A. (\<lambda>x. LEAST j. P j x) -` {i} \<inter> space M) \<in> sets M"
  1678     by (intro countable_UN) auto
  1679   moreover have "(\<Union>i\<in>A. (\<lambda>x. LEAST j. P j x) -` {i} \<inter> space M) =
  1680     (\<lambda>x. LEAST j. P j x) -` A \<inter> space M" by auto
  1681   ultimately show ?thesis by auto
  1682 qed
  1683 
  1684 end