# HG changeset patch
# User hellerar
# Date 1282821337 -7200
# Node ID cae59dc0a0948bba6403551ef1217557ed088dd7
# Parent  7f69af169e879beb09cc8d79cba0e8b258337f0e
dynkin system

diff -r 7f69af169e87 -r cae59dc0a094 src/HOL/Probability/Product_Measure.thy
--- a/src/HOL/Probability/Product_Measure.thy	Wed Aug 25 18:46:22 2010 +0200
+++ b/src/HOL/Probability/Product_Measure.thy	Thu Aug 26 13:15:37 2010 +0200
@@ -2,6 +2,254 @@
 imports Lebesgue_Integration
 begin
 
+definition dynkin
+where "dynkin M =
+      ((\<forall> A \<in> sets M. A \<subseteq> space M) \<and>
+       space M \<in> sets M \<and> (\<forall> a \<in> sets M. \<forall> b \<in> sets M. b - a \<in> sets M) \<and>
+       (\<forall> a. (\<forall> i j :: nat. i \<noteq> j \<longrightarrow> a i \<inter> a j = {}) \<and>
+             (\<forall> i :: nat. a i \<in> sets M) \<longrightarrow> UNION UNIV a \<in> sets M))"
+
+lemma dynkinI:
+  assumes "\<And> A. A \<in> sets M \<Longrightarrow> A \<subseteq> space M"
+  assumes "space M \<in> sets M" and "\<forall> a \<in> sets M. \<forall> b \<in> sets M. b - a \<in> sets M"
+  assumes "\<And> a. (\<And> i j :: nat. i \<noteq> j \<Longrightarrow> a i \<inter> a j = {})
+          \<Longrightarrow> (\<And> i :: nat. a i \<in> sets M) \<Longrightarrow> UNION UNIV a \<in> sets M"
+  shows "dynkin M"
+using assms unfolding dynkin_def by auto
+
+lemma dynkin_subset:
+  assumes "dynkin M"
+  shows "\<And> A. A \<in> sets M \<Longrightarrow> A \<subseteq> space M"
+using assms unfolding dynkin_def by auto
+
+lemma dynkin_space:
+  assumes "dynkin M"
+  shows "space M \<in> sets M"
+using assms unfolding dynkin_def by auto
+
+lemma dynkin_diff:
+  assumes "dynkin M"
+  shows "\<And> a b. \<lbrakk> a \<in> sets M ; b \<in> sets M \<rbrakk> \<Longrightarrow> b - a \<in> sets M"
+using assms unfolding dynkin_def by auto
+
+lemma dynkin_UN:
+  assumes "dynkin M"
+  assumes "\<And> i j :: nat. i \<noteq> j \<Longrightarrow> a i \<inter> a j = {}"
+  assumes "\<forall> i :: nat. a i \<in> sets M"
+  shows "UNION UNIV a \<in> sets M"
+using assms unfolding dynkin_def by auto
+
+definition Int_stable
+where "Int_stable M = (\<forall> a \<in> sets M. (\<forall> b \<in> sets M. a \<inter> b \<in> sets M))"
+
+lemma dynkin_trivial:
+  shows "dynkin \<lparr> space = A, sets = Pow A \<rparr>"
+by (rule dynkinI) auto
+
+lemma
+  assumes stab: "Int_stable E"
+  and spac: "space E = space D"
+  and subsED: "sets E \<subseteq> sets D"
+  and subsDE: "sets D \<subseteq> sigma_sets (space E) (sets E)"
+  and dyn: "dynkin D"
+  shows "sigma (space E) (sets E) = D"
+proof -
+  def sets_\<delta>E == "\<Inter> {sets d | d :: 'a algebra. dynkin d \<and> space d = space E \<and> sets E \<subseteq> sets d}"
+  def \<delta>E == "\<lparr> space = space E, sets = sets_\<delta>E \<rparr>"
+  have "\<lparr> space = space E, sets = Pow (space E) \<rparr> \<in> {d | d. dynkin d \<and> space d = space E \<and> sets E \<subseteq> sets d}"
+    using dynkin_trivial spac subsED dynkin_subset[OF dyn] by fastsimp
+  hence not_empty: "{sets (d :: 'a algebra) | d. dynkin d \<and> space d = space E \<and> sets E \<subseteq> sets d} \<noteq> {}"
+    using exI[of "\<lambda> x. space x = space E \<and> dynkin x \<and> sets E \<subseteq> sets x" "\<lparr> space = space E, sets = Pow (space E) \<rparr>", simplified]
+    by auto
+
+  have "sets_\<delta>E \<subseteq> sets D"
+    unfolding sets_\<delta>E_def using assms by auto
+
+  have \<delta>ynkin: "dynkin \<delta>E"
+  proof (rule dynkinI, safe)
+    fix A x assume asm: "A \<in> sets \<delta>E" "x \<in> A"
+    { fix d :: "('a, 'b) algebra_scheme" assume "A \<in> sets d" "dynkin d \<and> space d = space E"
+      hence "A \<subseteq> space d"
+        using dynkin_subset by auto }
+    show "x \<in> space \<delta>E" using asm
+      unfolding \<delta>E_def sets_\<delta>E_def using not_empty
+    proof auto
+      fix x A fix d :: "'a algebra"
+      assume asm: "\<forall>x. (\<exists>d :: 'a algebra. x = sets d \<and>
+        dynkin d \<and>
+        space d = space E \<and>
+        sets E \<subseteq> sets d) \<longrightarrow>
+        A \<in> x" "x \<in> A"
+        and asm': "space d = space E" "dynkin d" "sets E \<subseteq> sets d"
+      have "A \<in> sets d"
+        apply (rule impE[OF spec[OF asm(1), of "sets d"]])
+        using exI[of _ d] asm' by auto
+      thus "x \<in> space E" using asm' dynkin_subset[OF asm'(2), of A] asm(2) by auto
+    qed
+  next
+    show "space \<delta>E \<in> sets \<delta>E"
+      unfolding \<delta>E_def sets_\<delta>E_def
+      using dynkin_space by fastsimp
+  next
+    fix a b assume "a \<in> sets \<delta>E" "b \<in> sets \<delta>E"
+    thus "b - a \<in> sets \<delta>E"
+      unfolding \<delta>E_def sets_\<delta>E_def by (auto intro:dynkin_diff)
+  next
+    fix a assume asm: "\<And>i j :: nat. i \<noteq> j \<Longrightarrow> a i \<inter> a j = {}" "\<And>i. a i \<in> sets \<delta>E"
+    thus "UNION UNIV a \<in> sets \<delta>E"
+      unfolding \<delta>E_def sets_\<delta>E_def apply (auto intro!:dynkin_UN[OF _ asm(1)])
+      by blast
+  qed
+  def Dy == "\<lambda> d. {A | A. A \<in> sets_\<delta>E \<and> A \<inter> d \<in> sets_\<delta>E}"
+  { fix d assume dasm: "d \<in> sets_\<delta>E"
+    have "dynkin \<lparr> space = space E, sets = Dy d \<rparr>"
+    proof (rule dynkinI, auto)
+      fix A x assume "A \<in> Dy d" "x \<in> A"
+      thus "x \<in> space E" unfolding Dy_def sets_\<delta>E_def using not_empty
+      proof auto fix x A fix da :: "'a algebra"
+        assume asm: "x \<in> A"
+          "\<forall>x. (\<exists>d :: 'a algebra. x = sets d \<and>
+          dynkin d \<and> space d = space E \<and>
+          sets E \<subseteq> sets d) \<longrightarrow> A \<in> x"
+          "\<forall>x. (\<exists>d. x = sets d \<and>
+          dynkin d \<and> space d = space E \<and>
+          sets E \<subseteq> sets d) \<longrightarrow> A \<inter> d \<in> x"
+          "space da = space E" "dynkin da"
+          "sets E \<subseteq> sets da"
+        have "A \<in> sets da"
+          apply (rule impE[OF spec[OF asm(2)], of "sets da"])
+          apply (rule exI[of _ da])
+          using exI[of _ da] asm(4,5,6) by auto
+        thus "x \<in> space E" using dynkin_subset[OF asm(5)] asm by auto
+      qed
+    next
+      show "space E \<in> Dy d"
+        unfolding Dy_def \<delta>E_def sets_\<delta>E_def
+      proof auto
+        fix d assume asm: "dynkin d" "space d = space E" "sets E \<subseteq> sets d"
+        hence "space d \<in> sets d" using dynkin_space[OF asm(1)] by auto
+        thus "space E \<in> sets d" using asm by auto
+      next
+        fix da :: "'a algebra" assume asm: "dynkin da" "space da = space E" "sets E \<subseteq> sets da"
+        have d: "d = space E \<inter> d"
+          using dasm dynkin_subset[OF asm(1)] asm(2) dynkin_subset[OF \<delta>ynkin]
+          unfolding \<delta>E_def by auto
+        hence "space E \<inter> d \<in> sets \<delta>E" unfolding \<delta>E_def
+          using dasm by auto
+        have "sets \<delta>E \<subseteq> sets da" unfolding \<delta>E_def sets_\<delta>E_def using asm
+          by auto
+        thus "space E \<inter> d \<in> sets da" using dasm asm d dynkin_subset[OF \<delta>ynkin]
+          unfolding \<delta>E_def by auto
+      qed
+    next
+      fix a b assume absm: "a \<in> Dy d" "b \<in> Dy d"
+      hence "a \<in> sets \<delta>E" "b \<in> sets \<delta>E"
+        unfolding Dy_def \<delta>E_def by auto
+      hence *: "b - a \<in> sets \<delta>E"
+        using dynkin_diff[OF \<delta>ynkin] by auto
+      have "a \<inter> d \<in> sets \<delta>E" "b \<inter> d \<in> sets \<delta>E"
+        using absm unfolding Dy_def \<delta>E_def by auto
+      hence "(b \<inter> d) - (a \<inter> d) \<in> sets \<delta>E"
+        using dynkin_diff[OF \<delta>ynkin] by auto
+      hence **: "(b - a) \<inter> d \<in> sets \<delta>E" by (auto simp add:Diff_Int_distrib2)
+      thus "b - a \<in> Dy d"
+        using * ** unfolding Dy_def \<delta>E_def by auto
+    next
+      fix a assume aasm: "\<And>i j :: nat. i \<noteq> j \<Longrightarrow> a i \<inter> a j = {}" "\<And>i. a i \<in> Dy d"
+      hence "\<forall> i. a i \<in> sets \<delta>E"
+        unfolding Dy_def \<delta>E_def by auto
+      from dynkin_UN[OF \<delta>ynkin aasm(1) this]
+      have *: "UNION UNIV a \<in> sets \<delta>E" by auto
+      from aasm
+      have aE: "\<forall> i. a i \<inter> d \<in> sets \<delta>E"
+        unfolding Dy_def \<delta>E_def by auto
+      from aasm
+      have "\<And>i j :: nat. i \<noteq> j \<Longrightarrow> (a i \<inter> d) \<inter> (a j \<inter> d) = {}" by auto
+      from dynkin_UN[OF \<delta>ynkin this]
+      have "UNION UNIV (\<lambda> i. a i \<inter> d) \<in> sets \<delta>E"
+        using aE by auto
+      hence **: "UNION UNIV a \<inter> d \<in> sets \<delta>E" by auto
+      from * ** show "UNION UNIV a \<in> Dy d" unfolding Dy_def \<delta>E_def by auto
+    qed } note Dy_nkin = this
+  have E_\<delta>E: "sets E \<subseteq> sets \<delta>E"
+    unfolding \<delta>E_def sets_\<delta>E_def by auto
+  { fix d assume dasm: "d \<in> sets \<delta>E"
+    { fix e assume easm: "e \<in> sets E"
+      hence deasm: "e \<in> sets \<delta>E"
+        unfolding \<delta>E_def sets_\<delta>E_def by auto
+      have subset: "Dy e \<subseteq> sets \<delta>E"
+        unfolding Dy_def \<delta>E_def by auto
+      { fix e' assume e'asm: "e' \<in> sets E"
+        have "e' \<inter> e \<in> sets E"
+          using easm e'asm stab unfolding Int_stable_def by auto
+        hence "e' \<inter> e \<in> sets \<delta>E"
+          unfolding \<delta>E_def sets_\<delta>E_def by auto
+        hence "e' \<in> Dy e" using e'asm unfolding Dy_def \<delta>E_def sets_\<delta>E_def by auto }
+      hence E_Dy: "sets E \<subseteq> Dy e" by auto
+      have "\<lparr> space = space E, sets = Dy e \<rparr> \<in> {d | d. dynkin d \<and> space d = space E \<and> sets E \<subseteq> sets d}"
+        using Dy_nkin[OF deasm[unfolded \<delta>E_def, simplified]] E_\<delta>E E_Dy by auto
+      hence "sets_\<delta>E \<subseteq> Dy e"
+        unfolding sets_\<delta>E_def
+      proof auto fix x
+        assume asm: "\<forall>xa. (\<exists>d :: 'a algebra. xa = sets d \<and>
+          dynkin d \<and>
+          space d = space E \<and>
+          sets E \<subseteq> sets d) \<longrightarrow>
+          x \<in> xa"
+          "dynkin \<lparr>space = space E, sets = Dy e\<rparr>"
+          "sets E \<subseteq> Dy e"
+        show "x \<in> Dy e"
+          apply (rule impE[OF spec[OF asm(1), of "Dy e"]])
+          apply (rule exI[of _ "\<lparr>space = space E, sets = Dy e\<rparr>"])
+          using asm by auto
+      qed
+      hence "sets \<delta>E = Dy e" using subset unfolding \<delta>E_def by auto
+      hence "d \<inter> e \<in> sets \<delta>E"
+        using dasm easm deasm unfolding Dy_def \<delta>E_def by auto
+      hence "e \<in> Dy d" using deasm
+        unfolding Dy_def \<delta>E_def
+        by (auto simp add:Int_commute) }
+    hence "sets E \<subseteq> Dy d" by auto
+    hence "sets \<delta>E \<subseteq> Dy d" using Dy_nkin[OF dasm[unfolded \<delta>E_def, simplified]]
+      unfolding \<delta>E_def sets_\<delta>E_def 
+    proof auto
+      fix x
+      assume asm: "sets E \<subseteq> Dy d"
+        "dynkin \<lparr>space = space E, sets = Dy d\<rparr>"
+        "\<forall>xa. (\<exists>d :: 'a algebra. xa = sets d \<and> dynkin d \<and>
+            space d = space E \<and> sets E \<subseteq> sets d) \<longrightarrow> x \<in> xa"
+      show "x \<in> Dy d"
+        apply (rule impE[OF spec[OF asm(3), of "Dy d"]])
+        apply (rule exI[of _ "\<lparr>space = space E, sets = Dy d\<rparr>"])
+        using asm by auto
+    qed
+    hence *: "sets \<delta>E = Dy d"
+      unfolding Dy_def \<delta>E_def by auto
+    fix a assume aasm: "a \<in> sets \<delta>E"
+    hence "a \<inter> d \<in> sets \<delta>E"
+      using * dasm unfolding Dy_def \<delta>E_def by auto } note \<delta>E_stab = this
+  have "sigma_algebra D"
+    apply unfold_locales
+    using dynkin_subset[OF dyn]
+    using dynkin_diff[OF dyn, of _ "space D", OF _ dynkin_space[OF dyn]]
+    using dynkin_diff[OF dyn, of "space D" "space D", OF dynkin_space[OF dyn] dynkin_space[OF dyn]]
+    using dynkin_space[OF dyn]
+  proof auto
+    fix A :: "nat \<Rightarrow> 'a set" assume Asm: "range A \<subseteq> sets D" "\<And>A. A \<in> sets D \<Longrightarrow> A \<subseteq> space D"
+      "\<And>a. a \<in> sets D \<Longrightarrow> space D - a \<in> sets D"
+    "{} \<in> sets D" "space D \<in> sets D"
+    let "?A i" = "A i - (\<Inter> j \<in> {..< i}. A j)"
+    { fix i :: nat assume "i > 0"
+      have "(\<Inter> j \<in> {..< i}. A j) \<in> sets \<delta>E"
+        apply (induct i)
+        apply auto
+    }
+    from dynkin_UN
+  qed
+qed
+
+lemma
+(*
 definition prod_sets where
   "prod_sets A B = {z. \<exists>x \<in> A. \<exists>y \<in> B. z = x \<times> y}"
 
@@ -153,4 +401,5 @@
   unfolding finite_prod_measure_space[OF N, symmetric]
   using finite_measure_space_finite_prod_measure[OF N] .
 
+*)
 end
\ No newline at end of file