Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Uniform_Limit.thy Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/Analysis/Sigma_Algebra.thy
    Author:     Stefan Richter, Markus Wenzel, TU München
    Author:     Johannes Hölzl, TU München
    Plus material from the Hurd/Coble measure theory development,
    translated by Lawrence Paulson.
*)

chapter \<open>Measure and Integration Theory\<close>

theory Sigma_Algebra
imports
  Complex_Main
  "HOL-Library.Countable_Set"
  "HOL-Library.FuncSet"
  "HOL-Library.Indicator_Function"
  "HOL-Library.Extended_Nonnegative_Real"
  "HOL-Library.Disjoint_Sets"
begin

section \<open>Sigma Algebra\<close>

text \<open>Sigma algebras are an elementary concept in measure
  theory. To measure --- that is to integrate --- functions, we first have
  to measure sets. Unfortunately, when dealing with a large universe,
  it is often not possible to consistently assign a measure to every
  subset. Therefore it is necessary to define the set of measurable
  subsets of the universe. A sigma algebra is such a set that has
  three very natural and desirable properties.\<close>

subsection \<open>Families of sets\<close>

locale\<^marker>\<open>tag important\<close> subset_class =
  fixes \<Omega> :: "'a set" and M :: "'a set set"
  assumes space_closed: "M \ Pow \"

lemma (in subset_class) sets_into_space: "x \ M \ x \ \"
  by (metis PowD contra_subsetD space_closed)

subsubsection \<open>Semiring of sets\<close>

locale\<^marker>\<open>tag important\<close> semiring_of_sets = subset_class +
  assumes empty_sets[iff]: "{} \ M"
  assumes Int[intro]: "\a b. a \ M \ b \ M \ a \ b \ M"
  assumes Diff_cover:
    "\a b. a \ M \ b \ M \ \C\M. finite C \ disjoint C \ a - b = \C"

lemma (in semiring_of_sets) finite_INT[intro]:
  assumes "finite I" "I \ {}" "\i. i \ I \ A i \ M"
  shows "(\i\I. A i) \ M"
  using assms by (induct rule: finite_ne_induct) auto

lemma (in semiring_of_sets) Int_space_eq1 [simp]: "x \ M \ \ \ x = x"
  by (metis Int_absorb1 sets_into_space)

lemma (in semiring_of_sets) Int_space_eq2 [simp]: "x \ M \ x \ \ = x"
  by (metis Int_absorb2 sets_into_space)

lemma (in semiring_of_sets) sets_Collect_conj:
  assumes "{x\\. P x} \ M" "{x\\. Q x} \ M"
  shows "{x\\. Q x \ P x} \ M"
proof -
  have "{x\\. Q x \ P x} = {x\\. Q x} \ {x\\. P x}"
    by auto
  with assms show ?thesis by auto
qed

lemma (in semiring_of_sets) sets_Collect_finite_All':
  assumes "\i. i \ S \ {x\\. P i x} \ M" "finite S" "S \ {}"
  shows "{x\\. \i\S. P i x} \ M"
proof -
  have "{x\\. \i\S. P i x} = (\i\S. {x\\. P i x})"
    using \<open>S \<noteq> {}\<close> by auto
  with assms show ?thesis by auto
qed

subsubsection \<open>Ring of sets\<close>

locale\<^marker>\<open>tag important\<close> ring_of_sets = semiring_of_sets +
  assumes Un [intro]: "\a b. a \ M \ b \ M \ a \ b \ M"

lemma (in ring_of_sets) finite_Union [intro]:
  "finite X \ X \ M \ \X \ M"
  by (induct set: finite) (auto simp add: Un)

lemma (in ring_of_sets) finite_UN[intro]:
  assumes "finite I" and "\i. i \ I \ A i \ M"
  shows "(\i\I. A i) \ M"
  using assms by induct auto

lemma (in ring_of_sets) Diff [intro]:
  assumes "a \ M" "b \ M" shows "a - b \ M"
  using Diff_cover[OF assms] by auto

lemma ring_of_setsI:
  assumes space_closed: "M \ Pow \"
  assumes empty_sets[iff]: "{} \ M"
  assumes Un[intro]: "\a b. a \ M \ b \ M \ a \ b \ M"
  assumes Diff[intro]: "\a b. a \ M \ b \ M \ a - b \ M"
  shows "ring_of_sets \ M"
proof
  fix a b assume ab: "a \ M" "b \ M"
  from ab show "\C\M. finite C \ disjoint C \ a - b = \C"
    by (intro exI[of _ "{a - b}"]) (auto simp: disjoint_def)
  have "a \ b = a - (a - b)" by auto
  also have "\ \ M" using ab by auto
  finally show "a \ b \ M" .
qed fact+

lemma ring_of_sets_iff: "ring_of_sets \ M \ M \ Pow \ \ {} \ M \ (\a\M. \b\M. a \ b \ M) \ (\a\M. \b\M. a - b \ M)"
proof
  assume "ring_of_sets \ M"
  then interpret ring_of_sets \<Omega> M .
  show "M \ Pow \ \ {} \ M \ (\a\M. \b\M. a \ b \ M) \ (\a\M. \b\M. a - b \ M)"
    using space_closed by auto
qed (auto intro!: ring_of_setsI)

lemma (in ring_of_sets) insert_in_sets:
  assumes "{x} \ M" "A \ M" shows "insert x A \ M"
proof -
  have "{x} \ A \ M" using assms by (rule Un)
  thus ?thesis by auto
qed

lemma (in ring_of_sets) sets_Collect_disj:
  assumes "{x\\. P x} \ M" "{x\\. Q x} \ M"
  shows "{x\\. Q x \ P x} \ M"
proof -
  have "{x\\. Q x \ P x} = {x\\. Q x} \ {x\\. P x}"
    by auto
  with assms show ?thesis by auto
qed

lemma (in ring_of_sets) sets_Collect_finite_Ex:
  assumes "\i. i \ S \ {x\\. P i x} \ M" "finite S"
  shows "{x\\. \i\S. P i x} \ M"
proof -
  have "{x\\. \i\S. P i x} = (\i\S. {x\\. P i x})"
    by auto
  with assms show ?thesis by auto
qed

subsubsection \<open>Algebra of sets\<close>

locale\<^marker>\<open>tag important\<close> algebra = ring_of_sets +
  assumes top [iff]: "\ \ M"

lemma (in algebra) compl_sets [intro]:
  "a \ M \ \ - a \ M"
  by auto

proposition algebra_iff_Un:
  "algebra \ M \
    M \<subseteq> Pow \<Omega> \<and>
    {} \<in> M \<and>
    (\<forall>a \<in> M. \<Omega> - a \<in> M) \<and>
    (\<forall>a \<in> M. \<forall> b \<in> M. a \<union> b \<in> M)" (is "_ \<longleftrightarrow> ?Un")
proof
  assume "algebra \ M"
  then interpret algebra \<Omega> M .
  show ?Un using sets_into_space by auto
next
  assume ?Un
  then have "\ \ M" by auto
  interpret ring_of_sets \<Omega> M
  proof (rule ring_of_setsI)
    show \<Omega>: "M \<subseteq> Pow \<Omega>" "{} \<in> M"
      using \<open>?Un\<close> by auto
    fix a b assume a: "a \ M" and b: "b \ M"
    then show "a \ b \ M" using \?Un\ by auto
    have "a - b = \ - ((\ - a) \ b)"
      using \<Omega> a b by auto
    then show "a - b \ M"
      using a b  \<open>?Un\<close> by auto
  qed
  show "algebra \ M" proof qed fact
qed

proposition algebra_iff_Int:
     "algebra \ M \
       M \<subseteq> Pow \<Omega> & {} \<in> M &
       (\<forall>a \<in> M. \<Omega> - a \<in> M) &
       (\<forall>a \<in> M. \<forall> b \<in> M. a \<inter> b \<in> M)" (is "_ \<longleftrightarrow> ?Int")
proof
  assume "algebra \ M"
  then interpret algebra \<Omega> M .
  show ?Int using sets_into_space by auto
next
  assume ?Int
  show "algebra \ M"
  proof (unfold algebra_iff_Un, intro conjI ballI)
    show \<Omega>: "M \<subseteq> Pow \<Omega>" "{} \<in> M"
      using \<open>?Int\<close> by auto
    from \<open>?Int\<close> show "\<And>a. a \<in> M \<Longrightarrow> \<Omega> - a \<in> M" by auto
    fix a b assume M: "a \ M" "b \ M"
    hence "a \ b = \ - ((\ - a) \ (\ - b))"
      using \<Omega> by blast
    also have "... \ M"
      using M \<open>?Int\<close> by auto
    finally show "a \ b \ M" .
  qed
qed

lemma (in algebra) sets_Collect_neg:
  assumes "{x\\. P x} \ M"
  shows "{x\\. \ P x} \ M"
proof -
  have "{x\\. \ P x} = \ - {x\\. P x}" by auto
  with assms show ?thesis by auto
qed

lemma (in algebra) sets_Collect_imp:
  "{x\\. P x} \ M \ {x\\. Q x} \ M \ {x\\. Q x \ P x} \ M"
  unfolding imp_conv_disj by (intro sets_Collect_disj sets_Collect_neg)

lemma (in algebra) sets_Collect_const:
  "{x\\. P} \ M"
  by (cases P) auto

lemma algebra_single_set:
  "X \ S \ algebra S { {}, X, S - X, S }"
  by (auto simp: algebra_iff_Int)

subsubsection\<^marker>\<open>tag unimportant\<close> \<open>Restricted algebras\<close>

abbreviation (in algebra)
  "restricted_space A \ ((\) A) ` M"

lemma (in algebra) restricted_algebra:
  assumes "A \ M" shows "algebra A (restricted_space A)"
  using assms by (auto simp: algebra_iff_Int)

subsubsection \<open>Sigma Algebras\<close>

locale\<^marker>\<open>tag important\<close> sigma_algebra = algebra +
  assumes countable_nat_UN [intro]: "\A. range A \ M \ (\i::nat. A i) \ M"

lemma (in algebra) is_sigma_algebra:
  assumes "finite M"
  shows "sigma_algebra \ M"
proof
  fix A :: "nat \ 'a set" assume "range A \ M"
  then have "(\i. A i) = (\s\M \ range A. s)"
    by auto
  also have "(\s\M \ range A. s) \ M"
    using \<open>finite M\<close> by auto
  finally show "(\i. A i) \ M" .
qed

lemma countable_UN_eq:
  fixes A :: "'i::countable \ 'a set"
  shows "(range A \ M \ (\i. A i) \ M) \
    (range (A \<circ> from_nat) \<subseteq> M \<longrightarrow> (\<Union>i. (A \<circ> from_nat) i) \<in> M)"
proof -
  let ?A' = "A \ from_nat"
  have *: "(\i. ?A' i) = (\i. A i)" (is "?l = ?r")
  proof safe
    fix x i assume "x \ A i" thus "x \ ?l"
      by (auto intro!: exI[of _ "to_nat i"])
  next
    fix x i assume "x \ ?A' i" thus "x \ ?r"
      by (auto intro!: exI[of _ "from_nat i"])
  qed
  have "A ` range from_nat = range A"
    using surj_from_nat by simp
  then have **: "range ?A' = range A"
    by (simp only: image_comp [symmetric])
  show ?thesis unfolding * ** ..
qed

lemma (in sigma_algebra) countable_Union [intro]:
  assumes "countable X" "X \ M" shows "\X \ M"
proof cases
  assume "X \ {}"
  hence "\X = (\n. from_nat_into X n)"
    using assms by (auto cong del: SUP_cong)
  also have "\ \ M" using assms
    by (auto intro!: countable_nat_UN) (metis \<open>X \<noteq> {}\<close> from_nat_into subsetD)
  finally show ?thesis .
qed simp

lemma (in sigma_algebra) countable_UN[intro]:
  fixes A :: "'i::countable \ 'a set"
  assumes "A`X \ M"
  shows  "(\x\X. A x) \ M"
proof -
  let ?A = "\i. if i \ X then A i else {}"
  from assms have "range ?A \ M" by auto
  with countable_nat_UN[of "?A \ from_nat"] countable_UN_eq[of ?A M]
  have "(\x. ?A x) \ M" by auto
  moreover have "(\x. ?A x) = (\x\X. A x)" by (auto split: if_split_asm)
  ultimately show ?thesis by simp
qed

lemma (in sigma_algebra) countable_UN':
  fixes A :: "'i \ 'a set"
  assumes X: "countable X"
  assumes A: "A`X \ M"
  shows  "(\x\X. A x) \ M"
proof -
  have "(\x\X. A x) = (\i\to_nat_on X ` X. A (from_nat_into X i))"
    using X by auto
  also have "\ \ M"
    using A X
    by (intro countable_UN) auto
  finally show ?thesis .
qed

lemma (in sigma_algebra) countable_UN'':
  "\ countable X; \x y. x \ X \ A x \ M \ \ (\x\X. A x) \ M"
by(erule countable_UN')(auto)

lemma (in sigma_algebra) countable_INT [intro]:
  fixes A :: "'i::countable \ 'a set"
  assumes A: "A`X \ M" "X \ {}"
  shows "(\i\X. A i) \ M"
proof -
  from A have "\i\X. A i \ M" by fast
  hence "\ - (\i\X. \ - A i) \ M" by blast
  moreover
  have "(\i\X. A i) = \ - (\i\X. \ - A i)" using space_closed A
    by blast
  ultimately show ?thesis by metis
qed

lemma (in sigma_algebra) countable_INT':
  fixes A :: "'i \ 'a set"
  assumes X: "countable X" "X \ {}"
  assumes A: "A`X \ M"
  shows  "(\x\X. A x) \ M"
proof -
  have "(\x\X. A x) = (\i\to_nat_on X ` X. A (from_nat_into X i))"
    using X by auto
  also have "\ \ M"
    using A X
    by (intro countable_INT) auto
  finally show ?thesis .
qed

lemma (in sigma_algebra) countable_INT'':
  "UNIV \ M \ countable I \ (\i. i \ I \ F i \ M) \ (\i\I. F i) \ M"
  by (cases "I = {}") (auto intro: countable_INT')

lemma (in sigma_algebra) countable:
  assumes "\a. a \ A \ {a} \ M" "countable A"
  shows "A \ M"
proof -
  have "(\a\A. {a}) \ M"
    using assms by (intro countable_UN') auto
  also have "(\a\A. {a}) = A" by auto
  finally show ?thesis by auto
qed

lemma ring_of_sets_Pow: "ring_of_sets sp (Pow sp)"
  by (auto simp: ring_of_sets_iff)

lemma algebra_Pow: "algebra sp (Pow sp)"
  by (auto simp: algebra_iff_Un)

lemma sigma_algebra_iff:
  "sigma_algebra \ M \
    algebra \<Omega> M \<and> (\<forall>A. range A \<subseteq> M \<longrightarrow> (\<Union>i::nat. A i) \<in> M)"
  by (simp add: sigma_algebra_def sigma_algebra_axioms_def)

lemma sigma_algebra_Pow: "sigma_algebra sp (Pow sp)"
  by (auto simp: sigma_algebra_iff algebra_iff_Int)

lemma (in sigma_algebra) sets_Collect_countable_All:
  assumes "\i. {x\\. P i x} \ M"
  shows "{x\\. \i::'i::countable. P i x} \ M"
proof -
  have "{x\\. \i::'i::countable. P i x} = (\i. {x\\. P i x})" by auto
  with assms show ?thesis by auto
qed

lemma (in sigma_algebra) sets_Collect_countable_Ex:
  assumes "\i. {x\\. P i x} \ M"
  shows "{x\\. \i::'i::countable. P i x} \ M"
proof -
  have "{x\\. \i::'i::countable. P i x} = (\i. {x\\. P i x})" by auto
  with assms show ?thesis by auto
qed

lemma (in sigma_algebra) sets_Collect_countable_Ex':
  assumes "\i. i \ I \ {x\\. P i x} \ M"
  assumes "countable I"
  shows "{x\\. \i\I. P i x} \ M"
proof -
  have "{x\\. \i\I. P i x} = (\i\I. {x\\. P i x})" by auto
  with assms show ?thesis
    by (auto intro!: countable_UN')
qed

lemma (in sigma_algebra) sets_Collect_countable_All':
  assumes "\i. i \ I \ {x\\. P i x} \ M"
  assumes "countable I"
  shows "{x\\. \i\I. P i x} \ M"
proof -
  have "{x\\. \i\I. P i x} = (\i\I. {x\\. P i x}) \ \" by auto
  with assms show ?thesis
    by (cases "I = {}") (auto intro!: countable_INT')
qed

lemma (in sigma_algebra) sets_Collect_countable_Ex1':
  assumes "\i. i \ I \ {x\\. P i x} \ M"
  assumes "countable I"
  shows "{x\\. \!i\I. P i x} \ M"
proof -
  have "{x\\. \!i\I. P i x} = {x\\. \i\I. P i x \ (\j\I. P j x \ i = j)}"
    by auto
  with assms show ?thesis
    by (auto intro!: sets_Collect_countable_All' sets_Collect_countable_Ex' sets_Collect_conj sets_Collect_imp sets_Collect_const)
qed

lemmas (in sigma_algebra) sets_Collect =
  sets_Collect_imp sets_Collect_disj sets_Collect_conj sets_Collect_neg sets_Collect_const
  sets_Collect_countable_All sets_Collect_countable_Ex sets_Collect_countable_All

lemma (in sigma_algebra) sets_Collect_countable_Ball:
  assumes "\i. {x\\. P i x} \ M"
  shows "{x\\. \i::'i::countable\X. P i x} \ M"
  unfolding Ball_def by (intro sets_Collect assms)

lemma (in sigma_algebra) sets_Collect_countable_Bex:
  assumes "\i. {x\\. P i x} \ M"
  shows "{x\\. \i::'i::countable\X. P i x} \ M"
  unfolding Bex_def by (intro sets_Collect assms)

lemma sigma_algebra_single_set:
  assumes "X \ S"
  shows "sigma_algebra S { {}, X, S - X, S }"
  using algebra.is_sigma_algebra[OF algebra_single_set[OF \<open>X \<subseteq> S\<close>]] by simp

subsubsection\<^marker>\<open>tag unimportant\<close> \<open>Binary Unions\<close>

definition binary :: "'a \ 'a \ nat \ 'a"
  where "binary a b = (\x. b)(0 := a)"

lemma range_binary_eq: "range(binary a b) = {a,b}"
  by (auto simp add: binary_def)

lemma Un_range_binary: "a \ b = (\i::nat. binary a b i)"
  by (simp add: range_binary_eq cong del: SUP_cong_simp)

lemma Int_range_binary: "a \ b = (\i::nat. binary a b i)"
  by (simp add: range_binary_eq cong del: INF_cong_simp)

lemma sigma_algebra_iff2:
  "sigma_algebra \ M \
    M \<subseteq> Pow \<Omega> \<and> {} \<in> M \<and> (\<forall>s \<in> M. \<Omega> - s \<in> M)
    \<and> (\<forall>A. range A \<subseteq> M \<longrightarrow>(\<Union> i::nat. A i) \<in> M)" (is "?P \<longleftrightarrow> ?R \<and> ?S \<and> ?V \<and> ?W")
proof
  assume ?P
  then interpret sigma_algebra \<Omega> M .
  from space_closed show "?R \ ?S \ ?V \ ?W"
    by auto
next
  assume "?R \ ?S \ ?V \ ?W"
  then have ?R ?S ?V ?W
    by simp_all
  show ?P
  proof (rule sigma_algebra.intro)
    show "sigma_algebra_axioms M"
      by standard (use \<open>?W\<close> in simp)
    from \<open>?W\<close> have *: "range (binary a b) \<subseteq> M \<Longrightarrow> \<Union> (range (binary a b)) \<in> M" for a b
      by auto
    show "algebra \ M"
      unfolding algebra_iff_Un using \<open>?R\<close> \<open>?S\<close> \<open>?V\<close> *
      by (auto simp add: range_binary_eq)
  qed
qed

subsubsection \<open>Initial Sigma Algebra\<close>

text\<^marker>\<open>tag important\<close> \<open>Sigma algebras can naturally be created as the closure of any set of
  M with regard to the properties just postulated.\<close>

inductive_set\<^marker>\<open>tag important\<close> sigma_sets :: "'a set \<Rightarrow> 'a set set \<Rightarrow> 'a set set"
  for sp :: "'a set" and A :: "'a set set"
  where
    Basic[intro, simp]: "a \ A \ a \ sigma_sets sp A"
  | Empty: "{} \ sigma_sets sp A"
  | Compl: "a \ sigma_sets sp A \ sp - a \ sigma_sets sp A"
  | Union: "(\i::nat. a i \ sigma_sets sp A) \ (\i. a i) \ sigma_sets sp A"

lemma (in sigma_algebra) sigma_sets_subset:
  assumes a: "a \ M"
  shows "sigma_sets \ a \ M"
proof
  fix x
  assume "x \ sigma_sets \ a"
  from this show "x \ M"
    by (induct rule: sigma_sets.induct, auto) (metis a subsetD)
qed

lemma sigma_sets_into_sp: "A \ Pow sp \ x \ sigma_sets sp A \ x \ sp"
  by (erule sigma_sets.induct, auto)

lemma sigma_algebra_sigma_sets:
     "a \ Pow \ \ sigma_algebra \ (sigma_sets \ a)"
  by (auto simp add: sigma_algebra_iff2 dest: sigma_sets_into_sp
           intro!: sigma_sets.Union sigma_sets.Empty sigma_sets.Compl)

lemma sigma_sets_least_sigma_algebra:
  assumes "A \ Pow S"
  shows "sigma_sets S A = \{B. A \ B \ sigma_algebra S B}"
proof safe
  fix B X assume "A \ B" and sa: "sigma_algebra S B"
    and X: "X \ sigma_sets S A"
  from sigma_algebra.sigma_sets_subset[OF sa, simplified, OF \<open>A \<subseteq> B\<close>] X
  show "X \ B" by auto
next
  fix X assume "X \ \{B. A \ B \ sigma_algebra S B}"
  then have [intro!]: "\B. A \ B \ sigma_algebra S B \ X \ B"
     by simp
  have "A \ sigma_sets S A" using assms by auto
  moreover have "sigma_algebra S (sigma_sets S A)"
    using assms by (intro sigma_algebra_sigma_sets[of A]) auto
  ultimately show "X \ sigma_sets S A" by auto
qed

lemma sigma_sets_top: "sp \ sigma_sets sp A"
  by (metis Diff_empty sigma_sets.Compl sigma_sets.Empty)

lemma binary_in_sigma_sets:
  "binary a b i \ sigma_sets sp A" if "a \ sigma_sets sp A" and "b \ sigma_sets sp A"
  using that by (simp add: binary_def)

lemma sigma_sets_Un:
  "a \ b \ sigma_sets sp A" if "a \ sigma_sets sp A" and "b \ sigma_sets sp A"
  using that by (simp add: Un_range_binary binary_in_sigma_sets Union)

lemma sigma_sets_Inter:
  assumes Asb: "A \ Pow sp"
  shows "(\i::nat. a i \ sigma_sets sp A) \ (\i. a i) \ sigma_sets sp A"
proof -
  assume ai: "\i::nat. a i \ sigma_sets sp A"
  hence "\i::nat. sp-(a i) \ sigma_sets sp A"
    by (rule sigma_sets.Compl)
  hence "(\i. sp-(a i)) \ sigma_sets sp A"
    by (rule sigma_sets.Union)
  hence "sp-(\i. sp-(a i)) \ sigma_sets sp A"
    by (rule sigma_sets.Compl)
  also have "sp-(\i. sp-(a i)) = sp Int (\i. a i)"
    by auto
  also have "... = (\i. a i)" using ai
    by (blast dest: sigma_sets_into_sp [OF Asb])
  finally show ?thesis .
qed

lemma sigma_sets_INTER:
  assumes Asb: "A \ Pow sp"
      and ai: "\i::nat. i \ S \ a i \ sigma_sets sp A" and non: "S \ {}"
  shows "(\i\S. a i) \ sigma_sets sp A"
proof -
  from ai have "\i. (if i\S then a i else sp) \ sigma_sets sp A"
    by (simp add: sigma_sets.intros(2-) sigma_sets_top)
  hence "(\i. (if i\S then a i else sp)) \ sigma_sets sp A"
    by (rule sigma_sets_Inter [OF Asb])
  also have "(\i. (if i\S then a i else sp)) = (\i\S. a i)"
    by auto (metis ai non sigma_sets_into_sp subset_empty subset_iff Asb)+
  finally show ?thesis .
qed

lemma sigma_sets_UNION:
  "countable B \ (\b. b \ B \ b \ sigma_sets X A) \ \ B \ sigma_sets X A"
  using from_nat_into [of B] range_from_nat_into [of B] sigma_sets.Union [of "from_nat_into B" X A]
  by (cases "B = {}") (simp_all add: sigma_sets.Empty cong del: SUP_cong)

lemma (in sigma_algebra) sigma_sets_eq:
     "sigma_sets \ M = M"
proof
  show "M \ sigma_sets \ M"
    by (metis Set.subsetI sigma_sets.Basic)
  next
  show "sigma_sets \ M \ M"
    by (metis sigma_sets_subset subset_refl)
qed

lemma sigma_sets_eqI:
  assumes A: "\a. a \ A \ a \ sigma_sets M B"
  assumes B: "\b. b \ B \ b \ sigma_sets M A"
  shows "sigma_sets M A = sigma_sets M B"
proof (intro set_eqI iffI)
  fix a assume "a \ sigma_sets M A"
  from this A show "a \ sigma_sets M B"
    by induct (auto intro!: sigma_sets.intros(2-) del: sigma_sets.Basic)
next
  fix b assume "b \ sigma_sets M B"
  from this B show "b \ sigma_sets M A"
    by induct (auto intro!: sigma_sets.intros(2-) del: sigma_sets.Basic)
qed

lemma sigma_sets_subseteq: assumes "A \ B" shows "sigma_sets X A \ sigma_sets X B"
proof
  fix x assume "x \ sigma_sets X A" then show "x \ sigma_sets X B"
    by induct (insert \<open>A \<subseteq> B\<close>, auto intro: sigma_sets.intros(2-))
qed

lemma sigma_sets_mono: assumes "A \ sigma_sets X B" shows "sigma_sets X A \ sigma_sets X B"
proof
  fix x assume "x \ sigma_sets X A" then show "x \ sigma_sets X B"
    by induct (insert \<open>A \<subseteq> sigma_sets X B\<close>, auto intro: sigma_sets.intros(2-))
qed

lemma sigma_sets_mono': assumes "A \ B" shows "sigma_sets X A \ sigma_sets X B"
proof
  fix x assume "x \ sigma_sets X A" then show "x \ sigma_sets X B"
    by induct (insert \<open>A \<subseteq> B\<close>, auto intro: sigma_sets.intros(2-))
qed

lemma sigma_sets_superset_generator: "A \ sigma_sets X A"
  by (auto intro: sigma_sets.Basic)

lemma (in sigma_algebra) restriction_in_sets:
  fixes A :: "nat \ 'a set"
  assumes "S \ M"
  and *: "range A \ (\A. S \ A) ` M" (is "_ \ ?r")
  shows "range A \ M" "(\i. A i) \ (\A. S \ A) ` M"
proof -
  { fix i have "A i \ ?r" using * by auto
    hence "\B. A i = B \ S \ B \ M" by auto
    hence "A i \ S" "A i \ M" using \S \ M\ by auto }
  thus "range A \ M" "(\i. A i) \ (\A. S \ A) ` M"
    by (auto intro!: image_eqI[of _ _ "(\i. A i)"])
qed

lemma (in sigma_algebra) restricted_sigma_algebra:
  assumes "S \ M"
  shows "sigma_algebra S (restricted_space S)"
  unfolding sigma_algebra_def sigma_algebra_axioms_def
proof safe
  show "algebra S (restricted_space S)" using restricted_algebra[OF assms] .
next
  fix A :: "nat \ 'a set" assume "range A \ restricted_space S"
  from restriction_in_sets[OF assms this[simplified]]
  show "(\i. A i) \ restricted_space S" by simp
qed

lemma sigma_sets_Int:
  assumes "A \ sigma_sets sp st" "A \ sp"
  shows "(\) A ` sigma_sets sp st = sigma_sets A ((\) A ` st)"
proof (intro equalityI subsetI)
  fix x assume "x \ (\) A ` sigma_sets sp st"
  then obtain y where "y \ sigma_sets sp st" "x = y \ A" by auto
  then have "x \ sigma_sets (A \ sp) ((\) A ` st)"
  proof (induct arbitrary: x)
    case (Compl a)
    then show ?case
      by (force intro!: sigma_sets.Compl simp: Diff_Int_distrib ac_simps)
  next
    case (Union a)
    then show ?case
      by (auto intro!: sigma_sets.Union
               simp add: UN_extend_simps simp del: UN_simps)
  qed (auto intro!: sigma_sets.intros(2-))
  then show "x \ sigma_sets A ((\) A ` st)"
    using \<open>A \<subseteq> sp\<close> by (simp add: Int_absorb2)
next
  fix x assume "x \ sigma_sets A ((\) A ` st)"
  then show "x \ (\) A ` sigma_sets sp st"
  proof induct
    case (Compl a)
    then obtain x where "a = A \ x" "x \ sigma_sets sp st" by auto
    then show ?case using \<open>A \<subseteq> sp\<close>
      by (force simp add: image_iff intro!: bexI[of _ "sp - x"] sigma_sets.Compl)
  next
    case (Union a)
    then have "\i. \x. x \ sigma_sets sp st \ a i = A \ x"
      by (auto simp: image_iff Bex_def)
    from choice[OF this] guess f ..
    then show ?case
      by (auto intro!: bexI[of _ "(\x. f x)"] sigma_sets.Union
               simp add: image_iff)
  qed (auto intro!: sigma_sets.intros(2-))
qed

lemma sigma_sets_empty_eq: "sigma_sets A {} = {{}, A}"
proof (intro set_eqI iffI)
  fix a assume "a \ sigma_sets A {}" then show "a \ {{}, A}"
    by induct blast+
qed (auto intro: sigma_sets.Empty sigma_sets_top)

lemma sigma_sets_single[simp]: "sigma_sets A {A} = {{}, A}"
proof (intro set_eqI iffI)
  fix x assume "x \ sigma_sets A {A}"
  then show "x \ {{}, A}"
    by induct blast+
next
  fix x assume "x \ {{}, A}"
  then show "x \ sigma_sets A {A}"
    by (auto intro: sigma_sets.Empty sigma_sets_top)
qed

lemma sigma_sets_sigma_sets_eq:
  "M \ Pow S \ sigma_sets S (sigma_sets S M) = sigma_sets S M"
  by (rule sigma_algebra.sigma_sets_eq[OF sigma_algebra_sigma_sets, of M S]) auto

lemma sigma_sets_singleton:
  assumes "X \ S"
  shows "sigma_sets S { X } = { {}, X, S - X, S }"
proof -
  interpret sigma_algebra S "{ {}, X, S - X, S }"
    by (rule sigma_algebra_single_set) fact
  have "sigma_sets S { X } \ sigma_sets S { {}, X, S - X, S }"
    by (rule sigma_sets_subseteq) simp
  moreover have "\ = { {}, X, S - X, S }"
    using sigma_sets_eq by simp
  moreover
  { fix A assume "A \ { {}, X, S - X, S }"
    then have "A \ sigma_sets S { X }"
      by (auto intro: sigma_sets.intros(2-) sigma_sets_top) }
  ultimately have "sigma_sets S { X } = sigma_sets S { {}, X, S - X, S }"
    by (intro antisym) auto
  with sigma_sets_eq show ?thesis by simp
qed

lemma restricted_sigma:
  assumes S: "S \ sigma_sets \ M" and M: "M \ Pow \"
  shows "algebra.restricted_space (sigma_sets \ M) S =
    sigma_sets S (algebra.restricted_space M S)"
proof -
  from S sigma_sets_into_sp[OF M]
  have "S \ sigma_sets \ M" "S \ \" by auto
  from sigma_sets_Int[OF this]
  show ?thesis by simp
qed

lemma sigma_sets_vimage_commute:
  assumes X: "X \ \ \ \'"
  shows "{X -` A \ \ |A. A \ sigma_sets \' M'}
       = sigma_sets \<Omega> {X -` A \<inter> \<Omega> |A. A \<in> M'}" (is "?L = ?R")
proof
  show "?L \ ?R"
  proof clarify
    fix A assume "A \ sigma_sets \' M'"
    then show "X -` A \ \ \ ?R"
    proof induct
      case Empty then show ?case
        by (auto intro!: sigma_sets.Empty)
    next
      case (Compl B)
      have [simp]: "X -` (\' - B) \ \ = \ - (X -` B \ \)"
        by (auto simp add: funcset_mem [OF X])
      with Compl show ?case
        by (auto intro!: sigma_sets.Compl)
    next
      case (Union F)
      then show ?case
        by (auto simp add: vimage_UN UN_extend_simps(4) simp del: UN_simps
                 intro!: sigma_sets.Union)
    qed auto
  qed
  show "?R \ ?L"
  proof clarify
    fix A assume "A \ ?R"
    then show "\B. A = X -` B \ \ \ B \ sigma_sets \' M'"
    proof induct
      case (Basic B) then show ?case by auto
    next
      case Empty then show ?case
        by (auto intro!: sigma_sets.Empty exI[of _ "{}"])
    next
      case (Compl B)
      then obtain A where A: "B = X -` A \ \" "A \ sigma_sets \' M'" by auto
      then have [simp]: "\ - B = X -` (\' - A) \ \"
        by (auto simp add: funcset_mem [OF X])
      with A(2) show ?case
        by (auto intro: sigma_sets.Compl)
    next
      case (Union F)
      then have "\i. \B. F i = X -` B \ \ \ B \ sigma_sets \' M'" by auto
      from choice[OF this] guess A .. note A = this
      with A show ?case
        by (auto simp: vimage_UN[symmetric] intro: sigma_sets.Union)
    qed
  qed
qed

lemma (in ring_of_sets) UNION_in_sets:
  fixes A:: "nat \ 'a set"
  assumes A: "range A \ M"
  shows  "(\i\{0.. M"
proof (induct n)
  case 0 show ?case by simp
next
  case (Suc n)
  thus ?case
    by (simp add: atLeastLessThanSuc) (metis A Un UNIV_I image_subset_iff)
qed

lemma (in ring_of_sets) range_disjointed_sets:
  assumes A: "range A \ M"
  shows  "range (disjointed A) \ M"
proof (auto simp add: disjointed_def)
  fix n
  show "A n - (\i\{0.. M" using UNION_in_sets
    by (metis A Diff UNIV_I image_subset_iff)
qed

lemma (in algebra) range_disjointed_sets':
  "range A \ M \ range (disjointed A) \ M"
  using range_disjointed_sets .

lemma sigma_algebra_disjoint_iff:
  "sigma_algebra \ M \ algebra \ M \
    (\<forall>A. range A \<subseteq> M \<longrightarrow> disjoint_family A \<longrightarrow> (\<Union>i::nat. A i) \<in> M)"
proof (auto simp add: sigma_algebra_iff)
  fix A :: "nat \ 'a set"
  assume M: "algebra \ M"
     and A: "range A \ M"
     and UnA: "\A. range A \ M \ disjoint_family A \ (\i::nat. A i) \ M"
  hence "range (disjointed A) \ M \
         disjoint_family (disjointed A) \<longrightarrow>
         (\<Union>i. disjointed A i) \<in> M" by blast
  hence "(\i. disjointed A i) \ M"
    by (simp add: algebra.range_disjointed_sets'[of \] M A disjoint_family_disjointed)
  thus "(\i::nat. A i) \ M" by (simp add: UN_disjointed_eq)
qed

subsubsection\<^marker>\<open>tag unimportant\<close> \<open>Ring generated by a semiring\<close>

definition (in semiring_of_sets) generated_ring :: "'a set set" where
  "generated_ring = { \C | C. C \ M \ finite C \ disjoint C }"

lemma (in semiring_of_sets) generated_ringE[elim?]:
  assumes "a \ generated_ring"
  obtains C where "finite C" "disjoint C" "C \ M" "a = \C"
  using assms unfolding generated_ring_def by auto

lemma (in semiring_of_sets) generated_ringI[intro?]:
  assumes "finite C" "disjoint C" "C \ M" "a = \C"
  shows "a \ generated_ring"
  using assms unfolding generated_ring_def by auto

lemma (in semiring_of_sets) generated_ringI_Basic:
  "A \ M \ A \ generated_ring"
  by (rule generated_ringI[of "{A}"]) (auto simp: disjoint_def)

lemma (in semiring_of_sets) generated_ring_disjoint_Un[intro]:
  assumes a: "a \ generated_ring" and b: "b \ generated_ring"
  and "a \ b = {}"
  shows "a \ b \ generated_ring"
proof -
  from a guess Ca .. note Ca = this
  from b guess Cb .. note Cb = this
  show ?thesis
  proof
    show "disjoint (Ca \ Cb)"
      using \<open>a \<inter> b = {}\<close> Ca Cb by (auto intro!: disjoint_union)
  qed (insert Ca Cb, auto)
qed

lemma (in semiring_of_sets) generated_ring_empty: "{} \ generated_ring"
  by (auto simp: generated_ring_def disjoint_def)

lemma (in semiring_of_sets) generated_ring_disjoint_Union:
  assumes "finite A" shows "A \ generated_ring \ disjoint A \ \A \ generated_ring"
  using assms by (induct A) (auto simp: disjoint_def intro!: generated_ring_disjoint_Un generated_ring_empty)

lemma (in semiring_of_sets) generated_ring_disjoint_UNION:
  "finite I \ disjoint (A ` I) \ (\i. i \ I \ A i \ generated_ring) \ \(A ` I) \ generated_ring"
  by (intro generated_ring_disjoint_Union) auto

lemma (in semiring_of_sets) generated_ring_Int:
  assumes a: "a \ generated_ring" and b: "b \ generated_ring"
  shows "a \ b \ generated_ring"
proof -
  from a guess Ca .. note Ca = this
  from b guess Cb .. note Cb = this
  define C where "C = (\(a,b). a \ b)` (Ca\Cb)"
  show ?thesis
  proof
    show "disjoint C"
    proof (simp add: disjoint_def C_def, intro ballI impI)
      fix a1 b1 a2 b2 assume sets: "a1 \ Ca" "b1 \ Cb" "a2 \ Ca" "b2 \ Cb"
      assume "a1 \ b1 \ a2 \ b2"
      then have "a1 \ a2 \ b1 \ b2" by auto
      then show "(a1 \ b1) \ (a2 \ b2) = {}"
      proof
        assume "a1 \ a2"
        with sets Ca have "a1 \ a2 = {}"
          by (auto simp: disjoint_def)
        then show ?thesis by auto
      next
        assume "b1 \ b2"
        with sets Cb have "b1 \ b2 = {}"
          by (auto simp: disjoint_def)
        then show ?thesis by auto
      qed
    qed
  qed (insert Ca Cb, auto simp: C_def)
qed

lemma (in semiring_of_sets) generated_ring_Inter:
  assumes "finite A" "A \ {}" shows "A \ generated_ring \ \A \ generated_ring"
  using assms by (induct A rule: finite_ne_induct) (auto intro: generated_ring_Int)

lemma (in semiring_of_sets) generated_ring_INTER:
  "finite I \ I \ {} \ (\i. i \ I \ A i \ generated_ring) \ \(A ` I) \ generated_ring"
  by (intro generated_ring_Inter) auto

lemma (in semiring_of_sets) generating_ring:
  "ring_of_sets \ generated_ring"
proof (rule ring_of_setsI)
  let ?R = generated_ring
  show "?R \ Pow \"
    using sets_into_space by (auto simp: generated_ring_def generated_ring_empty)
  show "{} \ ?R" by (rule generated_ring_empty)

  { fix a assume a: "a \ ?R" then guess Ca .. note Ca = this
    fix b assume b: "b \ ?R" then guess Cb .. note Cb = this

    show "a - b \ ?R"
    proof cases
      assume "Cb = {}" with Cb \<open>a \<in> ?R\<close> show ?thesis
        by simp
    next
      assume "Cb \ {}"
      with Ca Cb have "a - b = (\a'\Ca. \b'\Cb. a' - b')" by auto
      also have "\ \ ?R"
      proof (intro generated_ring_INTER generated_ring_disjoint_UNION)
        fix a b assume "a \ Ca" "b \ Cb"
        with Ca Cb Diff_cover[of a b] show "a - b \ ?R"
          by (auto simp add: generated_ring_def)
            (metis DiffI Diff_eq_empty_iff empty_iff)
      next
        show "disjoint ((\a'. \b'\Cb. a' - b')`Ca)"
          using Ca by (auto simp add: disjoint_def \<open>Cb \<noteq> {}\<close>)
      next
        show "finite Ca" "finite Cb" "Cb \ {}" by fact+
      qed
      finally show "a - b \ ?R" .
    qed }
  note Diff = this

  fix a b assume sets: "a \ ?R" "b \ ?R"
  have "a \ b = (a - b) \ (a \ b) \ (b - a)" by auto
  also have "\ \ ?R"
    by (intro sets generated_ring_disjoint_Un generated_ring_Int Diff) auto
  finally show "a \ b \ ?R" .
qed

lemma (in semiring_of_sets) sigma_sets_generated_ring_eq: "sigma_sets \ generated_ring = sigma_sets \ M"
proof
  interpret M: sigma_algebra \<Omega> "sigma_sets \<Omega> M"
    using space_closed by (rule sigma_algebra_sigma_sets)
  show "sigma_sets \ generated_ring \ sigma_sets \ M"
    by (blast intro!: sigma_sets_mono elim: generated_ringE)
qed (auto intro!: generated_ringI_Basic sigma_sets_mono)

subsubsection\<^marker>\<open>tag unimportant\<close> \<open>A Two-Element Series\<close>

definition binaryset :: "'a set \ 'a set \ nat \ 'a set"
  where "binaryset A B = (\x. {})(0 := A, Suc 0 := B)"

lemma range_binaryset_eq: "range(binaryset A B) = {A,B,{}}"
  apply (simp add: binaryset_def)
  apply (rule set_eqI)
  apply (auto simp add: image_iff)
  done

lemma UN_binaryset_eq: "(\i. binaryset A B i) = A \ B"
  by (simp add: range_binaryset_eq cong del: SUP_cong_simp)

subsubsection \<open>Closed CDI\<close>

definition\<^marker>\<open>tag important\<close> closed_cdi :: "'a set \<Rightarrow> 'a set set \<Rightarrow> bool" where
  "closed_cdi \ M \
   M \<subseteq> Pow \<Omega> &
   (\<forall>s \<in> M. \<Omega> - s \<in> M) &
   (\<forall>A. (range A \<subseteq> M) & (A 0 = {}) & (\<forall>n. A n \<subseteq> A (Suc n)) \<longrightarrow>
        (\<Union>i. A i) \<in> M) &
   (\<forall>A. (range A \<subseteq> M) & disjoint_family A \<longrightarrow> (\<Union>i::nat. A i) \<in> M)"

inductive_set
  smallest_ccdi_sets :: "'a set \ 'a set set \ 'a set set"
  for \<Omega> M
  where
    Basic [intro]:
      "a \ M \ a \ smallest_ccdi_sets \ M"
  | Compl [intro]:
      "a \ smallest_ccdi_sets \ M \ \ - a \ smallest_ccdi_sets \ M"
  | Inc:
      "range A \ Pow(smallest_ccdi_sets \ M) \ A 0 = {} \ (\n. A n \ A (Suc n))
       \<Longrightarrow> (\<Union>i. A i) \<in> smallest_ccdi_sets \<Omega> M"
  | Disj:
      "range A \ Pow(smallest_ccdi_sets \ M) \ disjoint_family A
       \<Longrightarrow> (\<Union>i::nat. A i) \<in> smallest_ccdi_sets \<Omega> M"

lemma (in subset_class) smallest_closed_cdi1: "M \ smallest_ccdi_sets \ M"
  by auto

lemma (in subset_class) smallest_ccdi_sets: "smallest_ccdi_sets \ M \ Pow \"
  apply (rule subsetI)
  apply (erule smallest_ccdi_sets.induct)
  apply (auto intro: range_subsetD dest: sets_into_space)
  done

lemma (in subset_class) smallest_closed_cdi2: "closed_cdi \ (smallest_ccdi_sets \ M)"
  apply (auto simp add: closed_cdi_def smallest_ccdi_sets)
  apply (blast intro: smallest_ccdi_sets.Inc smallest_ccdi_sets.Disj) +
  done

lemma closed_cdi_subset: "closed_cdi \ M \ M \ Pow \"
  by (simp add: closed_cdi_def)

lemma closed_cdi_Compl: "closed_cdi \ M \ s \ M \ \ - s \ M"
  by (simp add: closed_cdi_def)

lemma closed_cdi_Inc:
  "closed_cdi \ M \ range A \ M \ A 0 = {} \ (!!n. A n \ A (Suc n)) \ (\i. A i) \ M"
  by (simp add: closed_cdi_def)

lemma closed_cdi_Disj:
  "closed_cdi \ M \ range A \ M \ disjoint_family A \ (\i::nat. A i) \ M"
  by (simp add: closed_cdi_def)

lemma closed_cdi_Un:
  assumes cdi: "closed_cdi \ M" and empty: "{} \ M"
      and A: "A \ M" and B: "B \ M"
      and disj: "A \ B = {}"
    shows "A \ B \ M"
proof -
  have ra: "range (binaryset A B) \ M"
   by (simp add: range_binaryset_eq empty A B)
have di:  "disjoint_family (binaryset A B)" using disj
   by (simp add: disjoint_family_on_def binaryset_def Int_commute)
from closed_cdi_Disj [OF cdi ra di]
show ?thesis
   by (simp add: UN_binaryset_eq)
qed

lemma (in algebra) smallest_ccdi_sets_Un:
  assumes A: "A \ smallest_ccdi_sets \ M" and B: "B \ smallest_ccdi_sets \ M"
      and disj: "A \ B = {}"
    shows "A \ B \ smallest_ccdi_sets \ M"
proof -
  have ra: "range (binaryset A B) \ Pow (smallest_ccdi_sets \ M)"
    by (simp add: range_binaryset_eq  A B smallest_ccdi_sets.Basic)
  have di:  "disjoint_family (binaryset A B)" using disj
    by (simp add: disjoint_family_on_def binaryset_def Int_commute)
  from Disj [OF ra di]
  show ?thesis
    by (simp add: UN_binaryset_eq)
qed

lemma (in algebra) smallest_ccdi_sets_Int1:
  assumes a: "a \ M"
  shows "b \ smallest_ccdi_sets \ M \ a \ b \ smallest_ccdi_sets \ M"
proof (induct rule: smallest_ccdi_sets.induct)
  case (Basic x)
  thus ?case
    by (metis a Int smallest_ccdi_sets.Basic)
next
  case (Compl x)
  have "a \ (\ - x) = \ - ((\ - a) \ (a \ x))"
    by blast
  also have "... \ smallest_ccdi_sets \ M"
    by (metis smallest_ccdi_sets.Compl a Compl(2) Diff_Int2 Diff_Int_distrib2
           Diff_disjoint Int_Diff Int_empty_right smallest_ccdi_sets_Un
           smallest_ccdi_sets.Basic smallest_ccdi_sets.Compl)
  finally show ?case .
next
  case (Inc A)
  have 1: "(\i. (\i. a \ A i) i) = a \ (\i. A i)"
    by blast
  have "range (\i. a \ A i) \ Pow(smallest_ccdi_sets \ M)" using Inc
    by blast
  moreover have "(\i. a \ A i) 0 = {}"
    by (simp add: Inc)
  moreover have "!!n. (\i. a \ A i) n \ (\i. a \ A i) (Suc n)" using Inc
    by blast
  ultimately have 2: "(\i. (\i. a \ A i) i) \ smallest_ccdi_sets \ M"
    by (rule smallest_ccdi_sets.Inc)
  show ?case
    by (metis 1 2)
next
  case (Disj A)
  have 1: "(\i. (\i. a \ A i) i) = a \ (\i. A i)"
    by blast
  have "range (\i. a \ A i) \ Pow(smallest_ccdi_sets \ M)" using Disj
    by blast
  moreover have "disjoint_family (\i. a \ A i)" using Disj
    by (auto simp add: disjoint_family_on_def)
  ultimately have 2: "(\i. (\i. a \ A i) i) \ smallest_ccdi_sets \ M"
    by (rule smallest_ccdi_sets.Disj)
  show ?case
    by (metis 1 2)
qed

lemma (in algebra) smallest_ccdi_sets_Int:
  assumes b: "b \ smallest_ccdi_sets \ M"
  shows "a \ smallest_ccdi_sets \ M \ a \ b \ smallest_ccdi_sets \ M"
proof (induct rule: smallest_ccdi_sets.induct)
  case (Basic x)
  thus ?case
    by (metis b smallest_ccdi_sets_Int1)
next
  case (Compl x)
  have "(\ - x) \ b = \ - (x \ b \ (\ - b))"
    by blast
  also have "... \ smallest_ccdi_sets \ M"
    by (metis Compl(2) Diff_disjoint Int_Diff Int_commute Int_empty_right b
           smallest_ccdi_sets.Compl smallest_ccdi_sets_Un)
  finally show ?case .
next
  case (Inc A)
  have 1: "(\i. (\i. A i \ b) i) = (\i. A i) \ b"
    by blast
  have "range (\i. A i \ b) \ Pow(smallest_ccdi_sets \ M)" using Inc
    by blast
  moreover have "(\i. A i \ b) 0 = {}"
    by (simp add: Inc)
  moreover have "!!n. (\i. A i \ b) n \ (\i. A i \ b) (Suc n)" using Inc
    by blast
  ultimately have 2: "(\i. (\i. A i \ b) i) \ smallest_ccdi_sets \ M"
    by (rule smallest_ccdi_sets.Inc)
  show ?case
    by (metis 1 2)
next
  case (Disj A)
  have 1: "(\i. (\i. A i \ b) i) = (\i. A i) \ b"
    by blast
  have "range (\i. A i \ b) \ Pow(smallest_ccdi_sets \ M)" using Disj
    by blast
  moreover have "disjoint_family (\i. A i \ b)" using Disj
    by (auto simp add: disjoint_family_on_def)
  ultimately have 2: "(\i. (\i. A i \ b) i) \ smallest_ccdi_sets \ M"
    by (rule smallest_ccdi_sets.Disj)
  show ?case
    by (metis 1 2)
qed

lemma (in algebra) sigma_property_disjoint_lemma:
  assumes sbC: "M \ C"
      and ccdi: "closed_cdi \ C"
  shows "sigma_sets \ M \ C"
proof -
  have "smallest_ccdi_sets \ M \ {B . M \ B \ sigma_algebra \ B}"
    apply (auto simp add: sigma_algebra_disjoint_iff algebra_iff_Int
            smallest_ccdi_sets_Int)
    apply (metis Union_Pow_eq Union_upper subsetD smallest_ccdi_sets)
    apply (blast intro: smallest_ccdi_sets.Disj)
    done
  hence "sigma_sets (\) (M) \ smallest_ccdi_sets \ M"
    by clarsimp
       (drule sigma_algebra.sigma_sets_subset [where a="M"], auto)
  also have "... \ C"
    proof
      fix x
      assume x: "x \ smallest_ccdi_sets \ M"
      thus "x \ C"
        proof (induct rule: smallest_ccdi_sets.induct)
          case (Basic x)
          thus ?case
            by (metis Basic subsetD sbC)
        next
          case (Compl x)
          thus ?case
            by (blast intro: closed_cdi_Compl [OF ccdi, simplified])
        next
          case (Inc A)
          thus ?case
               by (auto intro: closed_cdi_Inc [OF ccdi, simplified])
        next
          case (Disj A)
          thus ?case
               by (auto intro: closed_cdi_Disj [OF ccdi, simplified])
        qed
    qed
  finally show ?thesis .
qed

lemma (in algebra) sigma_property_disjoint:
  assumes sbC: "M \ C"
      and compl: "!!s. s \ C \ sigma_sets (\) (M) \ \ - s \ C"
      and inc: "!!A. range A \ C \ sigma_sets (\) (M)
                     \<Longrightarrow> A 0 = {} \<Longrightarrow> (!!n. A n \<subseteq> A (Suc n))
                     \<Longrightarrow> (\<Union>i. A i) \<in> C"
      and disj: "!!A. range A \ C \ sigma_sets (\) (M)
                      \<Longrightarrow> disjoint_family A \<Longrightarrow> (\<Union>i::nat. A i) \<in> C"
  shows "sigma_sets (\) (M) \ C"
proof -
  have "sigma_sets (\) (M) \ C \ sigma_sets (\) (M)"
    proof (rule sigma_property_disjoint_lemma)
      show "M \ C \ sigma_sets (\) (M)"
        by (metis Int_greatest Set.subsetI sbC sigma_sets.Basic)
    next
      show "closed_cdi \ (C \ sigma_sets (\) (M))"
        by (simp add: closed_cdi_def compl inc disj)
           (metis PowI Set.subsetI le_infI2 sigma_sets_into_sp space_closed
             IntE sigma_sets.Compl range_subsetD sigma_sets.Union)
    qed
  thus ?thesis
    by blast
qed

subsubsection \<open>Dynkin systems\<close>

locale\<^marker>\<open>tag important\<close> Dynkin_system = subset_class +
  assumes space: "\ \ M"
    and   compl[intro!]: "\A. A \ M \ \ - A \ M"
    and   UN[intro!]: "\A. disjoint_family A \ range A \ M
                           \<Longrightarrow> (\<Union>i::nat. A i) \<in> M"

lemma (in Dynkin_system) empty[intro, simp]: "{} \ M"
  using space compl[of "\"] by simp

lemma (in Dynkin_system) diff:
  assumes sets: "D \ M" "E \ M" and "D \ E"
  shows "E - D \ M"
proof -
  let ?f = "\x. if x = 0 then D else if x = Suc 0 then \ - E else {}"
  have "range ?f = {D, \ - E, {}}"
    by (auto simp: image_iff)
  moreover have "D \ (\ - E) = (\i. ?f i)"
    by (auto simp: image_iff split: if_split_asm)
  moreover
  have "disjoint_family ?f" unfolding disjoint_family_on_def
    using \<open>D \<in> M\<close>[THEN sets_into_space] \<open>D \<subseteq> E\<close> by auto
  ultimately have "\ - (D \ (\ - E)) \ M"
    using sets UN by auto fastforce
  also have "\ - (D \ (\ - E)) = E - D"
    using assms sets_into_space by auto
  finally show ?thesis .
qed

lemma Dynkin_systemI:
  assumes "\ A. A \ M \ A \ \" "\ \ M"
  assumes "\ A. A \ M \ \ - A \ M"
  assumes "\ A. disjoint_family A \ range A \ M
          \<Longrightarrow> (\<Union>i::nat. A i) \<in> M"
  shows "Dynkin_system \ M"
  using assms by (auto simp: Dynkin_system_def Dynkin_system_axioms_def subset_class_def)

lemma Dynkin_systemI':
  assumes 1: "\ A. A \ M \ A \ \"
  assumes empty: "{} \ M"
  assumes Diff: "\ A. A \ M \ \ - A \ M"
  assumes 2: "\ A. disjoint_family A \ range A \ M
          \<Longrightarrow> (\<Union>i::nat. A i) \<in> M"
  shows "Dynkin_system \ M"
proof -
  from Diff[OF empty] have "\ \ M" by auto
  from 1 this Diff 2 show ?thesis
    by (intro Dynkin_systemI) auto
qed

lemma Dynkin_system_trivial:
  shows "Dynkin_system A (Pow A)"
  by (rule Dynkin_systemI) auto

lemma sigma_algebra_imp_Dynkin_system:
  assumes "sigma_algebra \ M" shows "Dynkin_system \ M"
proof -
  interpret sigma_algebra \<Omega> M by fact
  show ?thesis using sets_into_space by (fastforce intro!: Dynkin_systemI)
qed

subsubsection "Intersection sets systems"

definition\<^marker>\<open>tag important\<close> Int_stable :: "'a set set \<Rightarrow> bool" where
"Int_stable M \ (\ a \ M. \ b \ M. a \ b \ M)"

lemma (in algebra) Int_stable: "Int_stable M"
  unfolding Int_stable_def by auto

lemma Int_stableI_image:
  "(\i j. i \ I \ j \ I \ \k\I. A i \ A j = A k) \ Int_stable (A ` I)"
  by (auto simp: Int_stable_def image_def)

lemma Int_stableI:
  "(\a b. a \ A \ b \ A \ a \ b \ A) \ Int_stable A"
  unfolding Int_stable_def by auto

lemma Int_stableD:
  "Int_stable M \ a \ M \ b \ M \ a \ b \ M"
  unfolding Int_stable_def by auto

lemma (in Dynkin_system) sigma_algebra_eq_Int_stable:
  "sigma_algebra \ M \ Int_stable M"
proof
  assume "sigma_algebra \ M" then show "Int_stable M"
    unfolding sigma_algebra_def using algebra.Int_stable by auto
next
  assume "Int_stable M"
  show "sigma_algebra \ M"
    unfolding sigma_algebra_disjoint_iff algebra_iff_Un
  proof (intro conjI ballI allI impI)
    show "M \ Pow (\)" using sets_into_space by auto
  next
    fix A B assume "A \ M" "B \ M"
    then have "A \ B = \ - ((\ - A) \ (\ - B))"
              "\ - A \ M" "\ - B \ M"
      using sets_into_space by auto
    then show "A \ B \ M"
      using \<open>Int_stable M\<close> unfolding Int_stable_def by auto
  qed auto
qed

subsubsection "Smallest Dynkin systems"

definition\<^marker>\<open>tag important\<close> Dynkin :: "'a set \<Rightarrow> 'a set set \<Rightarrow> 'a set set" where
  "Dynkin \ M = (\{D. Dynkin_system \ D \ M \ D})"

lemma Dynkin_system_Dynkin:
  assumes "M \ Pow (\)"
  shows "Dynkin_system \ (Dynkin \ M)"
proof (rule Dynkin_systemI)
  fix A assume "A \ Dynkin \ M"
  moreover
  { fix D assume "A \ D" and d: "Dynkin_system \ D"
    then have "A \ \" by (auto simp: Dynkin_system_def subset_class_def) }
  moreover have "{D. Dynkin_system \ D \ M \ D} \ {}"
    using assms Dynkin_system_trivial by fastforce
  ultimately show "A \ \"
    unfolding Dynkin_def using assms
    by auto
next
  show "\ \ Dynkin \ M"
    unfolding Dynkin_def using Dynkin_system.space by fastforce
next
  fix A assume "A \ Dynkin \ M"
  then show "\ - A \ Dynkin \ M"
    unfolding Dynkin_def using Dynkin_system.compl by force
next
  fix A :: "nat \ 'a set"
  assume A: "disjoint_family A" "range A \ Dynkin \ M"
  show "(\i. A i) \ Dynkin \ M" unfolding Dynkin_def
  proof (simp, safe)
    fix D assume "Dynkin_system \ D" "M \ D"
    with A have "(\i. A i) \ D"
      by (intro Dynkin_system.UN) (auto simp: Dynkin_def)
    then show "(\i. A i) \ D" by auto
  qed
qed

lemma Dynkin_Basic[intro]: "A \ M \ A \ Dynkin \ M"
  unfolding Dynkin_def by auto

lemma (in Dynkin_system) restricted_Dynkin_system:
  assumes "D \ M"
  shows "Dynkin_system \ {Q. Q \ \ \ Q \ D \ M}"
proof (rule Dynkin_systemI, simp_all)
  have "\ \ D = D"
    using \<open>D \<in> M\<close> sets_into_space by auto
  then show "\ \ D \ M"
    using \<open>D \<in> M\<close> by auto
next
  fix A assume "A \ \ \ A \ D \ M"
  moreover have "(\ - A) \ D = (\ - (A \ D)) - (\ - D)"
    by auto
  ultimately show "(\ - A) \ D \ M"
    using  \<open>D \<in> M\<close> by (auto intro: diff)
next
  fix A :: "nat \ 'a set"
  assume "disjoint_family A" "range A \ {Q. Q \ \ \ Q \ D \ M}"
  then have "\i. A i \ \" "disjoint_family (\i. A i \ D)"
    "range (\i. A i \ D) \ M" "(\x. A x) \ D = (\x. A x \ D)"
    by ((fastforce simp: disjoint_family_on_def)+)
  then show "(\x. A x) \ \ \ (\x. A x) \ D \ M"
    by (auto simp del: UN_simps)
qed

lemma (in Dynkin_system) Dynkin_subset:
  assumes "N \ M"
  shows "Dynkin \ N \ M"
proof -
  have "Dynkin_system \ M" ..
  then have "Dynkin_system \ M"
    using assms unfolding Dynkin_system_def Dynkin_system_axioms_def subset_class_def by simp
  with \<open>N \<subseteq> M\<close> show ?thesis by (auto simp add: Dynkin_def)
qed

lemma sigma_eq_Dynkin:
  assumes sets: "M \ Pow \"
  assumes "Int_stable M"
  shows "sigma_sets \ M = Dynkin \ M"
proof -
  have "Dynkin \ M \ sigma_sets (\) (M)"
    using sigma_algebra_imp_Dynkin_system
    unfolding Dynkin_def sigma_sets_least_sigma_algebra[OF sets] by auto
  moreover
  interpret Dynkin_system \<Omega> "Dynkin \<Omega> M"
    using Dynkin_system_Dynkin[OF sets] .
  have "sigma_algebra \ (Dynkin \ M)"
    unfolding sigma_algebra_eq_Int_stable Int_stable_def
  proof (intro ballI)
    fix A B assume "A \ Dynkin \ M" "B \ Dynkin \ M"
    let ?D = "\E. {Q. Q \ \ \ Q \ E \ Dynkin \ M}"
    have "M \ ?D B"
    proof
      fix E assume "E \ M"
      then have "M \ ?D E" "E \ Dynkin \ M"
        using sets_into_space \<open>Int_stable M\<close> by (auto simp: Int_stable_def)
      then have "Dynkin \ M \ ?D E"
        using restricted_Dynkin_system \<open>E \<in> Dynkin \<Omega> M\<close>
        by (intro Dynkin_system.Dynkin_subset) simp_all
      then have "B \ ?D E"
        using \<open>B \<in> Dynkin \<Omega> M\<close> by auto
      then have "E \ B \ Dynkin \ M"
        by (subst Int_commute) simp
      then show "E \ ?D B"
        using sets \<open>E \<in> M\<close> by auto
    qed
    then have "Dynkin \ M \ ?D B"
      using restricted_Dynkin_system \<open>B \<in> Dynkin \<Omega> M\<close>
      by (intro Dynkin_system.Dynkin_subset) simp_all
    then show "A \ B \ Dynkin \ M"
      using \<open>A \<in> Dynkin \<Omega> M\<close> sets_into_space by auto
  qed
  from sigma_algebra.sigma_sets_subset[OF this, of "M"]
  have "sigma_sets (\) (M) \ Dynkin \ M" by auto
  ultimately have "sigma_sets (\) (M) = Dynkin \ M" by auto
  then show ?thesis
    by (auto simp: Dynkin_def)
qed

lemma (in Dynkin_system) Dynkin_idem:
  "Dynkin \ M = M"
proof -
  have "Dynkin \ M = M"
  proof
    show "M \ Dynkin \ M"
      using Dynkin_Basic by auto
    show "Dynkin \ M \ M"
      by (intro Dynkin_subset) auto
  qed
  then show ?thesis
    by (auto simp: Dynkin_def)
qed

lemma (in Dynkin_system) Dynkin_lemma:
  assumes "Int_stable E"
  and E: "E \ M" "M \ sigma_sets \ E"
  shows "sigma_sets \ E = M"
proof -
  have "E \ Pow \"
    using E sets_into_space by force
  then have *: "sigma_sets \ E = Dynkin \ E"
    using \<open>Int_stable E\<close> by (rule sigma_eq_Dynkin)
  then have "Dynkin \ E = M"
    using assms Dynkin_subset[OF E(1)] by simp
  with * show ?thesis
    using assms by (auto simp: Dynkin_def)
qed

subsubsection \<open>Induction rule for intersection-stable generators\<close>

text\<^marker>\<open>tag important\<close> \<open>The reason to introduce Dynkin-systems is the following induction rules for \<open>\<sigma>\<close>-algebras
generated by a generator closed under intersection.\<close>

proposition sigma_sets_induct_disjoint[consumes 3, case_names basic empty compl union]:
  assumes "Int_stable G"
    and closed: "G \ Pow \"
    and A: "A \ sigma_sets \ G"
  assumes basic: "\A. A \ G \ P A"
    and empty: "P {}"
    and compl: "\A. A \ sigma_sets \ G \ P A \ P (\ - A)"
    and union: "\A. disjoint_family A \ range A \ sigma_sets \ G \ (\i. P (A i)) \ P (\i::nat. A i)"
  shows "P A"
proof -
  let ?D = "{ A \ sigma_sets \ G. P A }"
  interpret sigma_algebra \<Omega> "sigma_sets \<Omega> G"
    using closed by (rule sigma_algebra_sigma_sets)
  from compl[OF _ empty] closed have space: "P \" by simp
  interpret Dynkin_system \<Omega> ?D
    by standard (auto dest: sets_into_space intro!: space compl union)
  have "sigma_sets \ G = ?D"
    by (rule Dynkin_lemma) (auto simp: basic \<open>Int_stable G\<close>)
  with A show ?thesis by auto
qed

subsection \<open>Measure type\<close>

definition\<^marker>\<open>tag important\<close> positive :: "'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> bool" where
  "positive M \ \ \ {} = 0"

definition\<^marker>\<open>tag important\<close> countably_additive :: "'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> bool" where
"countably_additive M f \
  (\<forall>A. range A \<subseteq> M \<longrightarrow> disjoint_family A \<longrightarrow> (\<Union>i. A i) \<in> M \<longrightarrow>
    (\<Sum>i. f (A i)) = f (\<Union>i. A i))"

definition\<^marker>\<open>tag important\<close> measure_space :: "'a set \<Rightarrow> 'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> bool" where
"measure_space \ A \ \
  sigma_algebra \<Omega> A \<and> positive A \<mu> \<and> countably_additive A \<mu>"

typedef\<^marker>\<open>tag important\<close> 'a measure =
  "{(\::'a set, A, \). (\a\-A. \ a = 0) \ measure_space \ A \ }"
proof
  have "sigma_algebra UNIV {{}, UNIV}"
    by (auto simp: sigma_algebra_iff2)
  then show "(UNIV, {{}, UNIV}, \A. 0) \ {(\, A, \). (\a\-A. \ a = 0) \ measure_space \ A \} "
    by (auto simp: measure_space_def positive_def countably_additive_def)
qed

definition\<^marker>\<open>tag important\<close> space :: "'a measure \<Rightarrow> 'a set" where
  "space M = fst (Rep_measure M)"

definition\<^marker>\<open>tag important\<close> sets :: "'a measure \<Rightarrow> 'a set set" where
  "sets M = fst (snd (Rep_measure M))"

definition\<^marker>\<open>tag important\<close> emeasure :: "'a measure \<Rightarrow> 'a set \<Rightarrow> ennreal" where
  "emeasure M = snd (snd (Rep_measure M))"

definition\<^marker>\<open>tag important\<close> measure :: "'a measure \<Rightarrow> 'a set \<Rightarrow> real" where
  "measure M A = enn2real (emeasure M A)"

declare [[coercion sets]]

declare [[coercion measure]]

declare [[coercion emeasure]]

lemma measure_space: "measure_space (space M) (sets M) (emeasure M)"
  by (cases M) (auto simp: space_def sets_def emeasure_def Abs_measure_inverse)

interpretation sets: sigma_algebra "space M" "sets M" for M :: "'a measure"
  using measure_space[of M] by (auto simp: measure_space_def)

definition\<^marker>\<open>tag important\<close> measure_of :: "'a set \<Rightarrow> 'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> 'a measure"
  where
"measure_of \ A \ =
  Abs_measure (\<Omega>, if A \<subseteq> Pow \<Omega> then sigma_sets \<Omega> A else {{}, \<Omega>},
    \<lambda>a. if a \<in> sigma_sets \<Omega> A \<and> measure_space \<Omega> (sigma_sets \<Omega> A) \<mu> then \<mu> a else 0)"

abbreviation "sigma \ A \ measure_of \ A (\x. 0)"

lemma measure_space_0: "A \ Pow \ \ measure_space \ (sigma_sets \ A) (\x. 0)"
  unfolding measure_space_def
  by (auto intro!: sigma_algebra_sigma_sets simp: positive_def countably_additive_def)

lemma sigma_algebra_trivial: "sigma_algebra \ {{}, \}"
by unfold_locales(fastforce intro: exI[where x="{{}}"] exI[where x="{\}"])+

lemma measure_space_0': "measure_space \ {{}, \} (\x. 0)"
by(simp add: measure_space_def positive_def countably_additive_def sigma_algebra_trivial)

lemma measure_space_closed:
  assumes "measure_space \ M \"
  shows "M \ Pow \"
proof -
  interpret sigma_algebra \<Omega> M using assms by(simp add: measure_space_def)
  show ?thesis by(rule space_closed)
qed

lemma (in ring_of_sets) positive_cong_eq:
  "(\a. a \ M \ \' a = \ a) \ positive M \' = positive M \"
  by (auto simp add: positive_def)

lemma (in sigma_algebra) countably_additive_eq:
  "(\a. a \ M \ \' a = \ a) \ countably_additive M \' = countably_additive M \"
  unfolding countably_additive_def
  by (intro arg_cong[where f=All] ext) (auto simp add: countably_additive_def subset_eq)

lemma measure_space_eq:
  assumes closed: "A \ Pow \" and eq: "\a. a \ sigma_sets \ A \ \ a = \' a"
--> --------------------

--> maximum size reached

--> --------------------

¤ Dauer der Verarbeitung: 0.80 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.