generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
authorhoelzl
Thu Dec 04 17:05:58 2014 +0100 (2014-12-04)
changeset 59088ff2bd4a14ddb
parent 59087 8535cfcfa493
child 59089 da2fef2faa83
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
src/HOL/Probability/Binary_Product_Measure.thy
src/HOL/Probability/Borel_Space.thy
src/HOL/Probability/Fin_Map.thy
src/HOL/Probability/Finite_Product_Measure.thy
src/HOL/Probability/Measurable.thy
src/HOL/Probability/Sigma_Algebra.thy
     1.1 --- a/src/HOL/Probability/Binary_Product_Measure.thy	Wed Dec 03 22:44:24 2014 +0100
     1.2 +++ b/src/HOL/Probability/Binary_Product_Measure.thy	Thu Dec 04 17:05:58 2014 +0100
     1.3 @@ -594,6 +594,65 @@
     1.4  
     1.5  subsection {* Products on counting spaces, densities and distributions *}
     1.6  
     1.7 +lemma sigma_prod:
     1.8 +  assumes X_cover: "\<exists>E\<subseteq>A. countable E \<and> X = \<Union>E" and A: "A \<subseteq> Pow X"
     1.9 +  assumes Y_cover: "\<exists>E\<subseteq>B. countable E \<and> Y = \<Union>E" and B: "B \<subseteq> Pow Y"
    1.10 +  shows "sigma X A \<Otimes>\<^sub>M sigma Y B = sigma (X \<times> Y) {a \<times> b | a b. a \<in> A \<and> b \<in> B}"
    1.11 +    (is "?P = ?S")
    1.12 +proof (rule measure_eqI)
    1.13 +  have [simp]: "snd \<in> X \<times> Y \<rightarrow> Y" "fst \<in> X \<times> Y \<rightarrow> X"
    1.14 +    by auto
    1.15 +  let ?XY = "{{fst -` a \<inter> X \<times> Y | a. a \<in> A}, {snd -` b \<inter> X \<times> Y | b. b \<in> B}}"
    1.16 +  have "sets ?P = 
    1.17 +    sets (\<Squnion>\<^sub>\<sigma> xy\<in>?XY. sigma (X \<times> Y) xy)"
    1.18 +    by (simp add: vimage_algebra_sigma sets_pair_eq_sets_fst_snd A B)
    1.19 +  also have "\<dots> = sets (sigma (X \<times> Y) (\<Union>?XY))"
    1.20 +    by (intro Sup_sigma_sigma arg_cong[where f=sets]) auto
    1.21 +  also have "\<dots> = sets ?S"
    1.22 +  proof (intro arg_cong[where f=sets] sigma_eqI sigma_sets_eqI) 
    1.23 +    show "\<Union>?XY \<subseteq> Pow (X \<times> Y)" "{a \<times> b |a b. a \<in> A \<and> b \<in> B} \<subseteq> Pow (X \<times> Y)"
    1.24 +      using A B by auto
    1.25 +  next
    1.26 +    interpret XY: sigma_algebra "X \<times> Y" "sigma_sets (X \<times> Y) {a \<times> b |a b. a \<in> A \<and> b \<in> B}"
    1.27 +      using A B by (intro sigma_algebra_sigma_sets) auto
    1.28 +    fix Z assume "Z \<in> \<Union>?XY"
    1.29 +    then show "Z \<in> sigma_sets (X \<times> Y) {a \<times> b |a b. a \<in> A \<and> b \<in> B}"
    1.30 +    proof safe
    1.31 +      fix a assume "a \<in> A"
    1.32 +      from Y_cover obtain E where E: "E \<subseteq> B" "countable E" and "Y = \<Union>E"
    1.33 +        by auto
    1.34 +      with `a \<in> A` A have eq: "fst -` a \<inter> X \<times> Y = (\<Union>e\<in>E. a \<times> e)"
    1.35 +        by auto
    1.36 +      show "fst -` a \<inter> X \<times> Y \<in> sigma_sets (X \<times> Y) {a \<times> b |a b. a \<in> A \<and> b \<in> B}"
    1.37 +        using `a \<in> A` E unfolding eq by (auto intro!: XY.countable_UN')
    1.38 +    next
    1.39 +      fix b assume "b \<in> B"
    1.40 +      from X_cover obtain E where E: "E \<subseteq> A" "countable E" and "X = \<Union>E"
    1.41 +        by auto
    1.42 +      with `b \<in> B` B have eq: "snd -` b \<inter> X \<times> Y = (\<Union>e\<in>E. e \<times> b)"
    1.43 +        by auto
    1.44 +      show "snd -` b \<inter> X \<times> Y \<in> sigma_sets (X \<times> Y) {a \<times> b |a b. a \<in> A \<and> b \<in> B}"
    1.45 +        using `b \<in> B` E unfolding eq by (auto intro!: XY.countable_UN')
    1.46 +    qed
    1.47 +  next
    1.48 +    fix Z assume "Z \<in> {a \<times> b |a b. a \<in> A \<and> b \<in> B}"
    1.49 +    then obtain a b where "Z = a \<times> b" and ab: "a \<in> A" "b \<in> B"
    1.50 +      by auto
    1.51 +    then have Z: "Z = (fst -` a \<inter> X \<times> Y) \<inter> (snd -` b \<inter> X \<times> Y)"
    1.52 +      using A B by auto
    1.53 +    interpret XY: sigma_algebra "X \<times> Y" "sigma_sets (X \<times> Y) (\<Union>?XY)"
    1.54 +      by (intro sigma_algebra_sigma_sets) auto
    1.55 +    show "Z \<in> sigma_sets (X \<times> Y) (\<Union>?XY)"
    1.56 +      unfolding Z by (rule XY.Int) (blast intro: ab)+
    1.57 +  qed
    1.58 +  finally show "sets ?P = sets ?S" .
    1.59 +next
    1.60 +  interpret finite_measure "sigma X A" for X A
    1.61 +    proof qed (simp add: emeasure_sigma)
    1.62 +  fix A assume "A \<in> sets ?P" then show "emeasure ?P A = emeasure ?S A"
    1.63 +    by (simp add: emeasure_pair_measure_alt emeasure_sigma)
    1.64 +qed
    1.65 +
    1.66  lemma sigma_sets_pair_measure_generator_finite:
    1.67    assumes "finite A" and "finite B"
    1.68    shows "sigma_sets (A \<times> B) { a \<times> b | a b. a \<subseteq> A \<and> b \<subseteq> B} = Pow (A \<times> B)"
    1.69 @@ -618,6 +677,18 @@
    1.70    show "a \<in> A" and "b \<in> B" by auto
    1.71  qed
    1.72  
    1.73 +lemma borel_prod:
    1.74 +  "(borel \<Otimes>\<^sub>M borel) = (borel :: ('a::second_countable_topology \<times> 'b::second_countable_topology) measure)"
    1.75 +  (is "?P = ?B")
    1.76 +proof -
    1.77 +  have "?B = sigma UNIV {A \<times> B | A B. open A \<and> open B}"
    1.78 +    by (rule second_countable_borel_measurable[OF open_prod_generated])
    1.79 +  also have "\<dots> = ?P"
    1.80 +    unfolding borel_def
    1.81 +    by (subst sigma_prod) (auto intro!: exI[of _ "{UNIV}"])
    1.82 +  finally show ?thesis ..
    1.83 +qed
    1.84 +
    1.85  lemma pair_measure_count_space:
    1.86    assumes A: "finite A" and B: "finite B"
    1.87    shows "count_space A \<Otimes>\<^sub>M count_space B = count_space (A \<times> B)" (is "?P = ?C")
    1.88 @@ -821,50 +892,6 @@
    1.89      by auto
    1.90  qed
    1.91  
    1.92 -lemma borel_prod: "sets (borel \<Otimes>\<^sub>M borel) =
    1.93 -    (sets borel :: ('a::second_countable_topology \<times> 'b::second_countable_topology) set set)"
    1.94 -  (is "?l = ?r")
    1.95 -proof -
    1.96 -  obtain A :: "'a set set" where A: "countable A" "topological_basis A"
    1.97 -    by (metis ex_countable_basis)
    1.98 -  moreover obtain B :: "'b set set" where B: "countable B" "topological_basis B"
    1.99 -    by (metis ex_countable_basis)
   1.100 -  ultimately have AB: "countable ((\<lambda>(a, b). a \<times> b) ` (A \<times> B))" "topological_basis ((\<lambda>(a, b). a \<times> b) ` (A \<times> B))"
   1.101 -    by (auto intro!: topological_basis_prod)
   1.102 -  have "sets (borel \<Otimes>\<^sub>M borel) = sigma_sets UNIV {a \<times> b |a b. a \<in> sigma_sets UNIV A \<and> b \<in> sigma_sets UNIV B}"
   1.103 -    by (simp add: sets_pair_measure
   1.104 -       borel_eq_countable_basis[OF A] borel_eq_countable_basis[OF B])
   1.105 -  also have "\<dots> \<supseteq> sigma_sets UNIV ((\<lambda>(a, b). a \<times> b) ` (A \<times> B))" (is "... \<supseteq> ?A")
   1.106 -    by (auto intro!: sigma_sets_mono)
   1.107 -  also (xtrans) have "?A = sets borel"
   1.108 -    by (simp add: borel_eq_countable_basis[OF AB])
   1.109 -  finally have "?r \<subseteq> ?l" .
   1.110 -  moreover have "?l \<subseteq> ?r"
   1.111 -  proof (simp add: sets_pair_measure, safe intro!: sigma_sets_mono)
   1.112 -    fix A::"('a \<times> 'b) set" assume "A \<in> sigma_sets UNIV {a \<times> b |a b. a \<in> sets borel \<and> b \<in> sets borel}"
   1.113 -    then show "A \<in> sets borel"
   1.114 -      by (induct A) (auto intro!: borel_Times)
   1.115 -  qed
   1.116 -  ultimately show ?thesis by auto
   1.117 -qed
   1.118 -
   1.119 -lemma borel_prod':
   1.120 -  "borel \<Otimes>\<^sub>M borel = (borel :: 
   1.121 -      ('a::second_countable_topology \<times> 'b::second_countable_topology) measure)"
   1.122 -proof (rule measure_eqI[OF borel_prod])
   1.123 -  interpret sigma_finite_measure "borel :: 'b measure"
   1.124 -    proof qed (intro exI[of _ "{UNIV}"], auto simp: borel_def emeasure_sigma)
   1.125 -  fix X :: "('a \<times> 'b) set" assume asm: "X \<in> sets (borel \<Otimes>\<^sub>M borel)"
   1.126 -  have "UNIV \<times> UNIV \<in> sets (borel \<Otimes>\<^sub>M borel :: ('a \<times> 'b) measure)" 
   1.127 -      by (simp add: borel_prod)
   1.128 -  moreover have "emeasure (borel \<Otimes>\<^sub>M borel) (UNIV \<times> UNIV :: ('a \<times> 'b) set) = 0"
   1.129 -      by (subst emeasure_pair_measure_Times, simp_all add: borel_def emeasure_sigma)
   1.130 -  moreover have "X \<subseteq> UNIV \<times> UNIV" by auto
   1.131 -  ultimately have "emeasure (borel \<Otimes>\<^sub>M borel) X = 0" by (rule emeasure_eq_0)
   1.132 -  thus "emeasure (borel \<Otimes>\<^sub>M borel) X = emeasure borel X"
   1.133 -      by (simp add: borel_def emeasure_sigma)
   1.134 -qed
   1.135 -
   1.136  lemma finite_measure_pair_measure:
   1.137    assumes "finite_measure M" "finite_measure N"
   1.138    shows "finite_measure (N  \<Otimes>\<^sub>M M)"
     2.1 --- a/src/HOL/Probability/Borel_Space.thy	Wed Dec 03 22:44:24 2014 +0100
     2.2 +++ b/src/HOL/Probability/Borel_Space.thy	Thu Dec 04 17:05:58 2014 +0100
     2.3 @@ -11,6 +11,17 @@
     2.4    "~~/src/HOL/Multivariate_Analysis/Multivariate_Analysis"
     2.5  begin
     2.6  
     2.7 +lemma topological_basis_trivial: "topological_basis {A. open A}"
     2.8 +  by (auto simp: topological_basis_def)
     2.9 +
    2.10 +lemma open_prod_generated: "open = generate_topology {A \<times> B | A B. open A \<and> open B}"
    2.11 +proof -
    2.12 +  have "{A \<times> B :: ('a \<times> 'b) set | A B. open A \<and> open B} = ((\<lambda>(a, b). a \<times> b) ` ({A. open A} \<times> {A. open A}))"
    2.13 +    by auto
    2.14 +  then show ?thesis
    2.15 +    by (auto intro: topological_basis_prod topological_basis_trivial topological_basis_imp_subbasis)  
    2.16 +qed
    2.17 +
    2.18  subsection {* Generic Borel spaces *}
    2.19  
    2.20  definition borel :: "'a::topological_space measure" where
    2.21 @@ -147,6 +158,50 @@
    2.22  lemma borel_compact: "compact (A::'a::t2_space set) \<Longrightarrow> A \<in> sets borel"
    2.23    by (auto intro: borel_closed dest!: compact_imp_closed)
    2.24  
    2.25 +lemma second_countable_borel_measurable:
    2.26 +  fixes X :: "'a::second_countable_topology set set"
    2.27 +  assumes eq: "open = generate_topology X"
    2.28 +  shows "borel = sigma UNIV X"
    2.29 +  unfolding borel_def
    2.30 +proof (intro sigma_eqI sigma_sets_eqI)
    2.31 +  interpret X: sigma_algebra UNIV "sigma_sets UNIV X"
    2.32 +    by (rule sigma_algebra_sigma_sets) simp
    2.33 +
    2.34 +  fix S :: "'a set" assume "S \<in> Collect open"
    2.35 +  then have "generate_topology X S"
    2.36 +    by (auto simp: eq)
    2.37 +  then show "S \<in> sigma_sets UNIV X"
    2.38 +  proof induction
    2.39 +    case (UN K)
    2.40 +    then have K: "\<And>k. k \<in> K \<Longrightarrow> open k"
    2.41 +      unfolding eq by auto
    2.42 +    from ex_countable_basis obtain B :: "'a set set" where
    2.43 +      B:  "\<And>b. b \<in> B \<Longrightarrow> open b" "\<And>X. open X \<Longrightarrow> \<exists>b\<subseteq>B. (\<Union>b) = X" and "countable B"
    2.44 +      by (auto simp: topological_basis_def)
    2.45 +    from B(2)[OF K] obtain m where m: "\<And>k. k \<in> K \<Longrightarrow> m k \<subseteq> B" "\<And>k. k \<in> K \<Longrightarrow> (\<Union>m k) = k"
    2.46 +      by metis
    2.47 +    def U \<equiv> "(\<Union>k\<in>K. m k)"
    2.48 +    with m have "countable U"
    2.49 +      by (intro countable_subset[OF _ `countable B`]) auto
    2.50 +    have "\<Union>U = (\<Union>A\<in>U. A)" by simp
    2.51 +    also have "\<dots> = \<Union>K"
    2.52 +      unfolding U_def UN_simps by (simp add: m)
    2.53 +    finally have "\<Union>U = \<Union>K" .
    2.54 +
    2.55 +    have "\<forall>b\<in>U. \<exists>k\<in>K. b \<subseteq> k"
    2.56 +      using m by (auto simp: U_def)
    2.57 +    then obtain u where u: "\<And>b. b \<in> U \<Longrightarrow> u b \<in> K" and "\<And>b. b \<in> U \<Longrightarrow> b \<subseteq> u b"
    2.58 +      by metis
    2.59 +    then have "(\<Union>b\<in>U. u b) \<subseteq> \<Union>K" "\<Union>U \<subseteq> (\<Union>b\<in>U. u b)"
    2.60 +      by auto
    2.61 +    then have "\<Union>K = (\<Union>b\<in>U. u b)"
    2.62 +      unfolding `\<Union>U = \<Union>K` by auto
    2.63 +    also have "\<dots> \<in> sigma_sets UNIV X"
    2.64 +      using u UN by (intro X.countable_UN' `countable U`) auto
    2.65 +    finally show "\<Union>K \<in> sigma_sets UNIV X" .
    2.66 +  qed auto
    2.67 +qed (auto simp: eq intro: generate_topology.Basis)
    2.68 +
    2.69  lemma borel_measurable_continuous_on_if:
    2.70    assumes A: "A \<in> sets borel" and f: "continuous_on A f" and g: "continuous_on (- A) g"
    2.71    shows "(\<lambda>x. if x \<in> A then f x else g x) \<in> borel_measurable borel"
    2.72 @@ -261,6 +316,145 @@
    2.73      unfolding eq by (rule borel_measurable_continuous_on[OF H]) auto
    2.74  qed
    2.75  
    2.76 +subsection {* Borel spaces on order topologies *}
    2.77 +
    2.78 +
    2.79 +lemma borel_Iio:
    2.80 +  "borel = sigma UNIV (range lessThan :: 'a::{linorder_topology, second_countable_topology} set set)"
    2.81 +  unfolding second_countable_borel_measurable[OF open_generated_order]
    2.82 +proof (intro sigma_eqI sigma_sets_eqI)
    2.83 +  from countable_dense_setE guess D :: "'a set" . note D = this
    2.84 +
    2.85 +  interpret L: sigma_algebra UNIV "sigma_sets UNIV (range lessThan)"
    2.86 +    by (rule sigma_algebra_sigma_sets) simp
    2.87 +
    2.88 +  fix A :: "'a set" assume "A \<in> range lessThan \<union> range greaterThan"
    2.89 +  then obtain y where "A = {y <..} \<or> A = {..< y}"
    2.90 +    by blast
    2.91 +  then show "A \<in> sigma_sets UNIV (range lessThan)"
    2.92 +  proof
    2.93 +    assume A: "A = {y <..}"
    2.94 +    show ?thesis
    2.95 +    proof cases
    2.96 +      assume "\<forall>x>y. \<exists>d. y < d \<and> d < x"
    2.97 +      with D(2)[of "{y <..< x}" for x] have "\<forall>x>y. \<exists>d\<in>D. y < d \<and> d < x"
    2.98 +        by (auto simp: set_eq_iff)
    2.99 +      then have "A = UNIV - (\<Inter>d\<in>{d\<in>D. y < d}. {..< d})"
   2.100 +        by (auto simp: A) (metis less_asym)
   2.101 +      also have "\<dots> \<in> sigma_sets UNIV (range lessThan)"
   2.102 +        using D(1) by (intro L.Diff L.top L.countable_INT'') auto
   2.103 +      finally show ?thesis .
   2.104 +    next
   2.105 +      assume "\<not> (\<forall>x>y. \<exists>d. y < d \<and> d < x)"
   2.106 +      then obtain x where "y < x"  "\<And>d. y < d \<Longrightarrow> \<not> d < x"
   2.107 +        by auto
   2.108 +      then have "A = UNIV - {..< x}"
   2.109 +        unfolding A by (auto simp: not_less[symmetric])
   2.110 +      also have "\<dots> \<in> sigma_sets UNIV (range lessThan)"
   2.111 +        by auto
   2.112 +      finally show ?thesis .
   2.113 +    qed
   2.114 +  qed auto
   2.115 +qed auto
   2.116 +
   2.117 +lemma borel_Ioi:
   2.118 +  "borel = sigma UNIV (range greaterThan :: 'a::{linorder_topology, second_countable_topology} set set)"
   2.119 +  unfolding second_countable_borel_measurable[OF open_generated_order]
   2.120 +proof (intro sigma_eqI sigma_sets_eqI)
   2.121 +  from countable_dense_setE guess D :: "'a set" . note D = this
   2.122 +
   2.123 +  interpret L: sigma_algebra UNIV "sigma_sets UNIV (range greaterThan)"
   2.124 +    by (rule sigma_algebra_sigma_sets) simp
   2.125 +
   2.126 +  fix A :: "'a set" assume "A \<in> range lessThan \<union> range greaterThan"
   2.127 +  then obtain y where "A = {y <..} \<or> A = {..< y}"
   2.128 +    by blast
   2.129 +  then show "A \<in> sigma_sets UNIV (range greaterThan)"
   2.130 +  proof
   2.131 +    assume A: "A = {..< y}"
   2.132 +    show ?thesis
   2.133 +    proof cases
   2.134 +      assume "\<forall>x<y. \<exists>d. x < d \<and> d < y"
   2.135 +      with D(2)[of "{x <..< y}" for x] have "\<forall>x<y. \<exists>d\<in>D. x < d \<and> d < y"
   2.136 +        by (auto simp: set_eq_iff)
   2.137 +      then have "A = UNIV - (\<Inter>d\<in>{d\<in>D. d < y}. {d <..})"
   2.138 +        by (auto simp: A) (metis less_asym)
   2.139 +      also have "\<dots> \<in> sigma_sets UNIV (range greaterThan)"
   2.140 +        using D(1) by (intro L.Diff L.top L.countable_INT'') auto
   2.141 +      finally show ?thesis .
   2.142 +    next
   2.143 +      assume "\<not> (\<forall>x<y. \<exists>d. x < d \<and> d < y)"
   2.144 +      then obtain x where "x < y"  "\<And>d. y > d \<Longrightarrow> x \<ge> d"
   2.145 +        by (auto simp: not_less[symmetric])
   2.146 +      then have "A = UNIV - {x <..}"
   2.147 +        unfolding A Compl_eq_Diff_UNIV[symmetric] by auto
   2.148 +      also have "\<dots> \<in> sigma_sets UNIV (range greaterThan)"
   2.149 +        by auto
   2.150 +      finally show ?thesis .
   2.151 +    qed
   2.152 +  qed auto
   2.153 +qed auto
   2.154 +
   2.155 +lemma borel_measurableI_less:
   2.156 +  fixes f :: "'a \<Rightarrow> 'b::{linorder_topology, second_countable_topology}"
   2.157 +  shows "(\<And>y. {x\<in>space M. f x < y} \<in> sets M) \<Longrightarrow> f \<in> borel_measurable M"
   2.158 +  unfolding borel_Iio
   2.159 +  by (rule measurable_measure_of) (auto simp: Int_def conj_commute)
   2.160 +
   2.161 +lemma borel_measurableI_greater:
   2.162 +  fixes f :: "'a \<Rightarrow> 'b::{linorder_topology, second_countable_topology}"
   2.163 +  shows "(\<And>y. {x\<in>space M. y < f x} \<in> sets M) \<Longrightarrow> f \<in> borel_measurable M"
   2.164 +  unfolding borel_Ioi
   2.165 +  by (rule measurable_measure_of) (auto simp: Int_def conj_commute)
   2.166 +
   2.167 +lemma borel_measurable_SUP[measurable (raw)]:
   2.168 +  fixes F :: "_ \<Rightarrow> _ \<Rightarrow> _::{complete_linorder, linorder_topology, second_countable_topology}"
   2.169 +  assumes [simp]: "countable I"
   2.170 +  assumes [measurable]: "\<And>i. i \<in> I \<Longrightarrow> F i \<in> borel_measurable M"
   2.171 +  shows "(\<lambda>x. SUP i:I. F i x) \<in> borel_measurable M"
   2.172 +  by (rule borel_measurableI_greater) (simp add: less_SUP_iff)
   2.173 +
   2.174 +lemma borel_measurable_INF[measurable (raw)]:
   2.175 +  fixes F :: "_ \<Rightarrow> _ \<Rightarrow> _::{complete_linorder, linorder_topology, second_countable_topology}"
   2.176 +  assumes [simp]: "countable I"
   2.177 +  assumes [measurable]: "\<And>i. i \<in> I \<Longrightarrow> F i \<in> borel_measurable M"
   2.178 +  shows "(\<lambda>x. INF i:I. F i x) \<in> borel_measurable M"
   2.179 +  by (rule borel_measurableI_less) (simp add: INF_less_iff)
   2.180 +
   2.181 +lemma borel_measurable_lfp[consumes 1, case_names continuity step]:
   2.182 +  fixes F :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b::{complete_linorder, linorder_topology, second_countable_topology})"
   2.183 +  assumes "Order_Continuity.continuous F"
   2.184 +  assumes *: "\<And>f. f \<in> borel_measurable M \<Longrightarrow> F f \<in> borel_measurable M"
   2.185 +  shows "lfp F \<in> borel_measurable M"
   2.186 +proof -
   2.187 +  { fix i have "((F ^^ i) bot) \<in> borel_measurable M"
   2.188 +      by (induct i) (auto intro!: *) }
   2.189 +  then have "(\<lambda>x. SUP i. (F ^^ i) bot x) \<in> borel_measurable M"
   2.190 +    by measurable
   2.191 +  also have "(\<lambda>x. SUP i. (F ^^ i) bot x) = (SUP i. (F ^^ i) bot)"
   2.192 +    by auto
   2.193 +  also have "(SUP i. (F ^^ i) bot) = lfp F"
   2.194 +    by (rule continuous_lfp[symmetric]) fact
   2.195 +  finally show ?thesis .
   2.196 +qed
   2.197 +
   2.198 +lemma borel_measurable_gfp[consumes 1, case_names continuity step]:
   2.199 +  fixes F :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b::{complete_linorder, linorder_topology, second_countable_topology})"
   2.200 +  assumes "Order_Continuity.down_continuous F"
   2.201 +  assumes *: "\<And>f. f \<in> borel_measurable M \<Longrightarrow> F f \<in> borel_measurable M"
   2.202 +  shows "gfp F \<in> borel_measurable M"
   2.203 +proof -
   2.204 +  { fix i have "((F ^^ i) top) \<in> borel_measurable M"
   2.205 +      by (induct i) (auto intro!: * simp: bot_fun_def) }
   2.206 +  then have "(\<lambda>x. INF i. (F ^^ i) top x) \<in> borel_measurable M"
   2.207 +    by measurable
   2.208 +  also have "(\<lambda>x. INF i. (F ^^ i) top x) = (INF i. (F ^^ i) top)"
   2.209 +    by auto
   2.210 +  also have "\<dots> = gfp F"
   2.211 +    by (rule down_continuous_gfp[symmetric]) fact
   2.212 +  finally show ?thesis .
   2.213 +qed
   2.214 +
   2.215  subsection {* Borel spaces on euclidean spaces *}
   2.216  
   2.217  lemma borel_measurable_inner[measurable (raw)]:
   2.218 @@ -1169,32 +1363,6 @@
   2.219    thus ?thesis using assms by induct auto
   2.220  qed simp
   2.221  
   2.222 -lemma borel_measurable_SUP[measurable (raw)]:
   2.223 -  fixes f :: "'d\<Colon>countable \<Rightarrow> 'a \<Rightarrow> ereal"
   2.224 -  assumes "\<And>i. i \<in> A \<Longrightarrow> f i \<in> borel_measurable M"
   2.225 -  shows "(\<lambda>x. SUP i : A. f i x) \<in> borel_measurable M" (is "?sup \<in> borel_measurable M")
   2.226 -  unfolding borel_measurable_ereal_iff_ge
   2.227 -proof
   2.228 -  fix a
   2.229 -  have "?sup -` {a<..} \<inter> space M = (\<Union>i\<in>A. {x\<in>space M. a < f i x})"
   2.230 -    by (auto simp: less_SUP_iff)
   2.231 -  then show "?sup -` {a<..} \<inter> space M \<in> sets M"
   2.232 -    using assms by auto
   2.233 -qed
   2.234 -
   2.235 -lemma borel_measurable_INF[measurable (raw)]:
   2.236 -  fixes f :: "'d :: countable \<Rightarrow> 'a \<Rightarrow> ereal"
   2.237 -  assumes "\<And>i. i \<in> A \<Longrightarrow> f i \<in> borel_measurable M"
   2.238 -  shows "(\<lambda>x. INF i : A. f i x) \<in> borel_measurable M" (is "?inf \<in> borel_measurable M")
   2.239 -  unfolding borel_measurable_ereal_iff_less
   2.240 -proof
   2.241 -  fix a
   2.242 -  have "?inf -` {..<a} \<inter> space M = (\<Union>i\<in>A. {x\<in>space M. f i x < a})"
   2.243 -    by (auto simp: INF_less_iff)
   2.244 -  then show "?inf -` {..<a} \<inter> space M \<in> sets M"
   2.245 -    using assms by auto
   2.246 -qed
   2.247 -
   2.248  lemma [measurable (raw)]:
   2.249    fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> ereal"
   2.250    assumes "\<And>i. f i \<in> borel_measurable M"
   2.251 @@ -1325,23 +1493,6 @@
   2.252      (\<lambda>x. sup (f x) (g x)::ereal) \<in> borel_measurable M"
   2.253    by simp
   2.254  
   2.255 -lemma borel_measurable_lfp[consumes 1, case_names continuity step]:
   2.256 -  fixes F :: "('a \<Rightarrow> ereal) \<Rightarrow> ('a \<Rightarrow> ereal)"
   2.257 -  assumes "Order_Continuity.continuous F"
   2.258 -  assumes *: "\<And>f. f \<in> borel_measurable M \<Longrightarrow> F f \<in> borel_measurable M"
   2.259 -  shows "lfp F \<in> borel_measurable M"
   2.260 -proof -
   2.261 -  { fix i have "((F ^^ i) (\<lambda>t. bot)) \<in> borel_measurable M"
   2.262 -      by (induct i) (auto intro!: * simp: bot_fun_def) }
   2.263 -  then have "(\<lambda>x. SUP i. (F ^^ i) (\<lambda>t. bot) x) \<in> borel_measurable M"
   2.264 -    by measurable
   2.265 -  also have "(\<lambda>x. SUP i. (F ^^ i) (\<lambda>t. bot) x) = (SUP i. (F ^^ i) bot)"
   2.266 -    by (auto simp add: bot_fun_def)
   2.267 -  also have "(SUP i. (F ^^ i) bot) = lfp F"
   2.268 -    by (rule continuous_lfp[symmetric]) fact
   2.269 -  finally show ?thesis .
   2.270 -qed
   2.271 -
   2.272  (* Proof by Jeremy Avigad and Luke Serafin *)
   2.273  lemma isCont_borel:
   2.274    fixes f :: "'b::metric_space \<Rightarrow> 'a::metric_space"
     3.1 --- a/src/HOL/Probability/Fin_Map.thy	Wed Dec 03 22:44:24 2014 +0100
     3.2 +++ b/src/HOL/Probability/Fin_Map.thy	Thu Dec 04 17:05:58 2014 +0100
     3.3 @@ -1005,7 +1005,7 @@
     3.4    then show "f \<in> (\<Union>n. Pi' I (A n))" by auto
     3.5  qed (auto simp: Pi'_def `finite I`)
     3.6  
     3.7 -text {* adapted from @{thm sigma_prod_algebra_sigma_eq} *}
     3.8 +text {* adapted from @{thm sets_PiM_sigma} *}
     3.9  
    3.10  lemma sigma_fprod_algebra_sigma_eq:
    3.11    fixes E :: "'i \<Rightarrow> 'a set set" and S :: "'i \<Rightarrow> nat \<Rightarrow> 'a set"
     4.1 --- a/src/HOL/Probability/Finite_Product_Measure.thy	Wed Dec 03 22:44:24 2014 +0100
     4.2 +++ b/src/HOL/Probability/Finite_Product_Measure.thy	Thu Dec 04 17:05:58 2014 +0100
     4.3 @@ -362,6 +362,101 @@
     4.4    apply (auto intro!: arg_cong2[where f=sigma_sets])
     4.5    done
     4.6  
     4.7 +lemma
     4.8 +  shows space_PiM_empty: "space (Pi\<^sub>M {} M) = {\<lambda>k. undefined}"
     4.9 +    and sets_PiM_empty: "sets (Pi\<^sub>M {} M) = { {}, {\<lambda>k. undefined} }"
    4.10 +  by (simp_all add: space_PiM sets_PiM_single image_constant sigma_sets_empty_eq)
    4.11 +
    4.12 +lemma sets_PiM_sigma:
    4.13 +  assumes \<Omega>_cover: "\<And>i. i \<in> I \<Longrightarrow> \<exists>S\<subseteq>E i. countable S \<and> \<Omega> i = \<Union>S"
    4.14 +  assumes E: "\<And>i. i \<in> I \<Longrightarrow> E i \<subseteq> Pow (\<Omega> i)"
    4.15 +  assumes J: "\<And>j. j \<in> J \<Longrightarrow> finite j" "\<Union>J = I"
    4.16 +  defines "P \<equiv> {{f\<in>(\<Pi>\<^sub>E i\<in>I. \<Omega> i). \<forall>i\<in>j. f i \<in> A i} | A j. j \<in> J \<and> A \<in> Pi j E}"
    4.17 +  shows "sets (\<Pi>\<^sub>M i\<in>I. sigma (\<Omega> i) (E i)) = sets (sigma (\<Pi>\<^sub>E i\<in>I. \<Omega> i) P)"
    4.18 +proof cases
    4.19 +  assume "I = {}" 
    4.20 +  with `\<Union>J = I` have "P = {{\<lambda>_. undefined}} \<or> P = {}"
    4.21 +    by (auto simp: P_def)
    4.22 +  with `I = {}` show ?thesis
    4.23 +    by (auto simp add: sets_PiM_empty sigma_sets_empty_eq)
    4.24 +next
    4.25 +  let ?F = "\<lambda>i. {(\<lambda>x. x i) -` A \<inter> Pi\<^sub>E I \<Omega> |A. A \<in> E i}"
    4.26 +  assume "I \<noteq> {}"
    4.27 +  then have "sets (Pi\<^sub>M I (\<lambda>i. sigma (\<Omega> i) (E i))) = 
    4.28 +      sets (\<Squnion>\<^sub>\<sigma> i\<in>I. vimage_algebra (\<Pi>\<^sub>E i\<in>I. \<Omega> i) (\<lambda>x. x i) (sigma (\<Omega> i) (E i)))"
    4.29 +    by (subst sets_PiM_eq_proj) (auto simp: space_measure_of_conv)
    4.30 +  also have "\<dots> = sets (\<Squnion>\<^sub>\<sigma> i\<in>I. sigma (Pi\<^sub>E I \<Omega>) (?F i))"
    4.31 +    using E by (intro SUP_sigma_cong arg_cong[where f=sets] vimage_algebra_sigma) auto
    4.32 +  also have "\<dots> = sets (sigma (Pi\<^sub>E I \<Omega>) (\<Union>i\<in>I. ?F i))"
    4.33 +    using `I \<noteq> {}` by (intro arg_cong[where f=sets] SUP_sigma_sigma) auto
    4.34 +  also have "\<dots> = sets (sigma (Pi\<^sub>E I \<Omega>) P)"
    4.35 +  proof (intro arg_cong[where f=sets] sigma_eqI sigma_sets_eqI)
    4.36 +    show "(\<Union>i\<in>I. ?F i) \<subseteq> Pow (Pi\<^sub>E I \<Omega>)" "P \<subseteq> Pow (Pi\<^sub>E I \<Omega>)"
    4.37 +      by (auto simp: P_def)
    4.38 +  next
    4.39 +    interpret P: sigma_algebra "\<Pi>\<^sub>E i\<in>I. \<Omega> i" "sigma_sets (\<Pi>\<^sub>E i\<in>I. \<Omega> i) P"
    4.40 +      by (auto intro!: sigma_algebra_sigma_sets simp: P_def)
    4.41 +
    4.42 +    fix Z assume "Z \<in> (\<Union>i\<in>I. ?F i)"
    4.43 +    then obtain i A where i: "i \<in> I" "A \<in> E i" and Z_def: "Z = (\<lambda>x. x i) -` A \<inter> Pi\<^sub>E I \<Omega>"
    4.44 +      by auto
    4.45 +    from `i \<in> I` J obtain j where j: "i \<in> j" "j \<in> J" "j \<subseteq> I" "finite j"
    4.46 +      by auto
    4.47 +    obtain S where S: "\<And>i. i \<in> j \<Longrightarrow> S i \<subseteq> E i" "\<And>i. i \<in> j \<Longrightarrow> countable (S i)"
    4.48 +      "\<And>i. i \<in> j \<Longrightarrow> \<Omega> i = \<Union>(S i)"
    4.49 +      by (metis subset_eq \<Omega>_cover `j \<subseteq> I`)
    4.50 +    def A' \<equiv> "\<lambda>n. n(i := A)"
    4.51 +    then have A'_i: "\<And>n. A' n i = A"
    4.52 +      by simp
    4.53 +    { fix n assume "n \<in> Pi\<^sub>E (j - {i}) S"
    4.54 +      then have "A' n \<in> Pi j E"
    4.55 +        unfolding PiE_def Pi_def using S(1) by (auto simp: A'_def `A \<in> E i` )
    4.56 +      with `j \<in> J` have "{f \<in> Pi\<^sub>E I \<Omega>. \<forall>i\<in>j. f i \<in> A' n i} \<in> P"
    4.57 +        by (auto simp: P_def) }
    4.58 +    note A'_in_P = this
    4.59 +
    4.60 +    { fix x assume "x i \<in> A" "x \<in> Pi\<^sub>E I \<Omega>"
    4.61 +      with S(3) `j \<subseteq> I` have "\<forall>i\<in>j. \<exists>s\<in>S i. x i \<in> s"
    4.62 +        by (auto simp: PiE_def Pi_def)
    4.63 +      then obtain s where s: "\<And>i. i \<in> j \<Longrightarrow> s i \<in> S i" "\<And>i. i \<in> j \<Longrightarrow> x i \<in> s i"
    4.64 +        by metis
    4.65 +      with `x i \<in> A` have "\<exists>n\<in>PiE (j-{i}) S. \<forall>i\<in>j. x i \<in> A' n i"
    4.66 +        by (intro bexI[of _ "restrict (s(i := A)) (j-{i})"]) (auto simp: A'_def split: if_splits) }
    4.67 +    then have "Z = (\<Union>n\<in>PiE (j-{i}) S. {f\<in>(\<Pi>\<^sub>E i\<in>I. \<Omega> i). \<forall>i\<in>j. f i \<in> A' n i})"
    4.68 +      unfolding Z_def
    4.69 +      by (auto simp add: set_eq_iff ball_conj_distrib `i\<in>j` A'_i dest: bspec[OF _ `i\<in>j`]
    4.70 +               cong: conj_cong)
    4.71 +    also have "\<dots> \<in> sigma_sets (\<Pi>\<^sub>E i\<in>I. \<Omega> i) P"
    4.72 +      using `finite j` S(2)
    4.73 +      by (intro P.countable_UN' countable_PiE) (simp_all add: image_subset_iff A'_in_P)
    4.74 +    finally show "Z \<in> sigma_sets (\<Pi>\<^sub>E i\<in>I. \<Omega> i) P" .
    4.75 +  next
    4.76 +    interpret F: sigma_algebra "\<Pi>\<^sub>E i\<in>I. \<Omega> i" "sigma_sets (\<Pi>\<^sub>E i\<in>I. \<Omega> i) (\<Union>i\<in>I. ?F i)"
    4.77 +      by (auto intro!: sigma_algebra_sigma_sets)
    4.78 +
    4.79 +    fix b assume "b \<in> P"
    4.80 +    then obtain A j where b: "b = {f\<in>(\<Pi>\<^sub>E i\<in>I. \<Omega> i). \<forall>i\<in>j. f i \<in> A i}" "j \<in> J" "A \<in> Pi j E"
    4.81 +      by (auto simp: P_def)
    4.82 +    show "b \<in> sigma_sets (Pi\<^sub>E I \<Omega>) (\<Union>i\<in>I. ?F i)"
    4.83 +    proof cases
    4.84 +      assume "j = {}"
    4.85 +      with b have "b = (\<Pi>\<^sub>E i\<in>I. \<Omega> i)"
    4.86 +        by auto
    4.87 +      then show ?thesis
    4.88 +        by blast
    4.89 +    next
    4.90 +      assume "j \<noteq> {}"
    4.91 +      with J b(2,3) have eq: "b = (\<Inter>i\<in>j. ((\<lambda>x. x i) -` A i \<inter> Pi\<^sub>E I \<Omega>))"
    4.92 +        unfolding b(1)
    4.93 +        by (auto simp: PiE_def Pi_def)
    4.94 +      show ?thesis
    4.95 +        unfolding eq using `A \<in> Pi j E` `j \<in> J` J(2)
    4.96 +        by (intro F.finite_INT J `j \<in> J` `j \<noteq> {}` sigma_sets.Basic) blast
    4.97 +    qed
    4.98 +  qed
    4.99 +  finally show "?thesis" .
   4.100 +qed
   4.101 +
   4.102  lemma sets_PiM_in_sets:
   4.103    assumes space: "space N = (\<Pi>\<^sub>E i\<in>I. space (M i))"
   4.104    assumes sets: "\<And>i A. i \<in> I \<Longrightarrow> A \<in> sets (M i) \<Longrightarrow> {x\<in>space N. x i \<in> A} \<in> sets N"
   4.105 @@ -600,11 +695,6 @@
   4.106    qed
   4.107  qed
   4.108  
   4.109 -lemma
   4.110 -  shows space_PiM_empty: "space (Pi\<^sub>M {} M) = {\<lambda>k. undefined}"
   4.111 -    and sets_PiM_empty: "sets (Pi\<^sub>M {} M) = { {}, {\<lambda>k. undefined} }"
   4.112 -  by (simp_all add: space_PiM sets_PiM_single image_constant sigma_sets_empty_eq)
   4.113 -
   4.114  lemma emeasure_PiM_empty[simp]: "emeasure (PiM {} M) {\<lambda>_. undefined} = 1"
   4.115  proof -
   4.116    let ?\<mu> = "\<lambda>A. if A = {} then 0 else (1::ereal)"
   4.117 @@ -927,116 +1017,6 @@
   4.118    "i \<in> I \<Longrightarrow> A \<in> sets (M i) \<Longrightarrow> { x \<in> space (Pi\<^sub>M I M). x i \<in> A } \<in> sets (Pi\<^sub>M I M)"
   4.119    by simp
   4.120  
   4.121 -lemma sigma_prod_algebra_sigma_eq_infinite:
   4.122 -  fixes E :: "'i \<Rightarrow> 'a set set"
   4.123 -  assumes S_union: "\<And>i. i \<in> I \<Longrightarrow> (\<Union>j. S i j) = space (M i)"
   4.124 -    and S_in_E: "\<And>i. i \<in> I \<Longrightarrow> range (S i) \<subseteq> E i"
   4.125 -  assumes E_closed: "\<And>i. i \<in> I \<Longrightarrow> E i \<subseteq> Pow (space (M i))"
   4.126 -    and E_generates: "\<And>i. i \<in> I \<Longrightarrow> sets (M i) = sigma_sets (space (M i)) (E i)"
   4.127 -  defines "P == {{f\<in>\<Pi>\<^sub>E i\<in>I. space (M i). f i \<in> A} | i A. i \<in> I \<and> A \<in> E i}"
   4.128 -  shows "sets (PiM I M) = sigma_sets (space (PiM I M)) P"
   4.129 -proof
   4.130 -  let ?P = "sigma (space (Pi\<^sub>M I M)) P"
   4.131 -  have P_closed: "P \<subseteq> Pow (space (Pi\<^sub>M I M))"
   4.132 -    using E_closed by (auto simp: space_PiM P_def subset_eq)
   4.133 -  then have space_P: "space ?P = (\<Pi>\<^sub>E i\<in>I. space (M i))"
   4.134 -    by (simp add: space_PiM)
   4.135 -  have "sets (PiM I M) =
   4.136 -      sigma_sets (space ?P) {{f \<in> \<Pi>\<^sub>E i\<in>I. space (M i). f i \<in> A} |i A. i \<in> I \<and> A \<in> sets (M i)}"
   4.137 -    using sets_PiM_single[of I M] by (simp add: space_P)
   4.138 -  also have "\<dots> \<subseteq> sets (sigma (space (PiM I M)) P)"
   4.139 -  proof (safe intro!: sets.sigma_sets_subset)
   4.140 -    fix i A assume "i \<in> I" and A: "A \<in> sets (M i)"
   4.141 -    then have "(\<lambda>x. x i) \<in> measurable ?P (sigma (space (M i)) (E i))"
   4.142 -      apply (subst measurable_iff_measure_of)
   4.143 -      apply (simp_all add: P_closed)
   4.144 -      using E_closed
   4.145 -      apply (force simp: subset_eq space_PiM)
   4.146 -      apply (force simp: subset_eq space_PiM)
   4.147 -      apply (auto simp: P_def intro!: sigma_sets.Basic exI[of _ i])
   4.148 -      apply (rule_tac x=Aa in exI)
   4.149 -      apply (auto simp: space_PiM)
   4.150 -      done
   4.151 -    from measurable_sets[OF this, of A] A `i \<in> I` E_closed
   4.152 -    have "(\<lambda>x. x i) -` A \<inter> space ?P \<in> sets ?P"
   4.153 -      by (simp add: E_generates)
   4.154 -    also have "(\<lambda>x. x i) -` A \<inter> space ?P = {f \<in> \<Pi>\<^sub>E i\<in>I. space (M i). f i \<in> A}"
   4.155 -      using P_closed by (auto simp: space_PiM)
   4.156 -    finally show "\<dots> \<in> sets ?P" .
   4.157 -  qed
   4.158 -  finally show "sets (PiM I M) \<subseteq> sigma_sets (space (PiM I M)) P"
   4.159 -    by (simp add: P_closed)
   4.160 -  show "sigma_sets (space (PiM I M)) P \<subseteq> sets (PiM I M)"
   4.161 -    unfolding P_def space_PiM[symmetric]
   4.162 -    by (intro sets.sigma_sets_subset) (auto simp: E_generates sets_Collect_single)
   4.163 -qed
   4.164 -
   4.165 -lemma sigma_prod_algebra_sigma_eq:
   4.166 -  fixes E :: "'i \<Rightarrow> 'a set set" and S :: "'i \<Rightarrow> nat \<Rightarrow> 'a set"
   4.167 -  assumes "finite I"
   4.168 -  assumes S_union: "\<And>i. i \<in> I \<Longrightarrow> (\<Union>j. S i j) = space (M i)"
   4.169 -    and S_in_E: "\<And>i. i \<in> I \<Longrightarrow> range (S i) \<subseteq> E i"
   4.170 -  assumes E_closed: "\<And>i. i \<in> I \<Longrightarrow> E i \<subseteq> Pow (space (M i))"
   4.171 -    and E_generates: "\<And>i. i \<in> I \<Longrightarrow> sets (M i) = sigma_sets (space (M i)) (E i)"
   4.172 -  defines "P == { Pi\<^sub>E I F | F. \<forall>i\<in>I. F i \<in> E i }"
   4.173 -  shows "sets (PiM I M) = sigma_sets (space (PiM I M)) P"
   4.174 -proof
   4.175 -  let ?P = "sigma (space (Pi\<^sub>M I M)) P"
   4.176 -  from `finite I`[THEN ex_bij_betw_finite_nat] guess T ..
   4.177 -  then have T: "\<And>i. i \<in> I \<Longrightarrow> T i < card I" "\<And>i. i\<in>I \<Longrightarrow> the_inv_into I T (T i) = i"
   4.178 -    by (auto simp add: bij_betw_def set_eq_iff image_iff the_inv_into_f_f)
   4.179 -  have P_closed: "P \<subseteq> Pow (space (Pi\<^sub>M I M))"
   4.180 -    using E_closed by (auto simp: space_PiM P_def subset_eq)
   4.181 -  then have space_P: "space ?P = (\<Pi>\<^sub>E i\<in>I. space (M i))"
   4.182 -    by (simp add: space_PiM)
   4.183 -  have "sets (PiM I M) =
   4.184 -      sigma_sets (space ?P) {{f \<in> \<Pi>\<^sub>E i\<in>I. space (M i). f i \<in> A} |i A. i \<in> I \<and> A \<in> sets (M i)}"
   4.185 -    using sets_PiM_single[of I M] by (simp add: space_P)
   4.186 -  also have "\<dots> \<subseteq> sets (sigma (space (PiM I M)) P)"
   4.187 -  proof (safe intro!: sets.sigma_sets_subset)
   4.188 -    fix i A assume "i \<in> I" and A: "A \<in> sets (M i)"
   4.189 -    have "(\<lambda>x. x i) \<in> measurable ?P (sigma (space (M i)) (E i))"
   4.190 -    proof (subst measurable_iff_measure_of)
   4.191 -      show "E i \<subseteq> Pow (space (M i))" using `i \<in> I` by fact
   4.192 -      from space_P `i \<in> I` show "(\<lambda>x. x i) \<in> space ?P \<rightarrow> space (M i)" by auto
   4.193 -      show "\<forall>A\<in>E i. (\<lambda>x. x i) -` A \<inter> space ?P \<in> sets ?P"
   4.194 -      proof
   4.195 -        fix A assume A: "A \<in> E i"
   4.196 -        then have "(\<lambda>x. x i) -` A \<inter> space ?P = (\<Pi>\<^sub>E j\<in>I. if i = j then A else space (M j))"
   4.197 -          using E_closed `i \<in> I` by (auto simp: space_P subset_eq split: split_if_asm)
   4.198 -        also have "\<dots> = (\<Pi>\<^sub>E j\<in>I. \<Union>n. if i = j then A else S j n)"
   4.199 -          by (intro PiE_cong) (simp add: S_union)
   4.200 -        also have "\<dots> = (\<Union>xs\<in>{xs. length xs = card I}. \<Pi>\<^sub>E j\<in>I. if i = j then A else S j (xs ! T j))"
   4.201 -          using T
   4.202 -          apply (auto simp: PiE_iff bchoice_iff)
   4.203 -          apply (rule_tac x="map (\<lambda>n. f (the_inv_into I T n)) [0..<card I]" in exI)
   4.204 -          apply (auto simp: bij_betw_def)
   4.205 -          done
   4.206 -        also have "\<dots> \<in> sets ?P"
   4.207 -        proof (safe intro!: sets.countable_UN)
   4.208 -          fix xs show "(\<Pi>\<^sub>E j\<in>I. if i = j then A else S j (xs ! T j)) \<in> sets ?P"
   4.209 -            using A S_in_E
   4.210 -            by (simp add: P_closed)
   4.211 -               (auto simp: P_def subset_eq intro!: exI[of _ "\<lambda>j. if i = j then A else S j (xs ! T j)"])
   4.212 -        qed
   4.213 -        finally show "(\<lambda>x. x i) -` A \<inter> space ?P \<in> sets ?P"
   4.214 -          using P_closed by simp
   4.215 -      qed
   4.216 -    qed
   4.217 -    from measurable_sets[OF this, of A] A `i \<in> I` E_closed
   4.218 -    have "(\<lambda>x. x i) -` A \<inter> space ?P \<in> sets ?P"
   4.219 -      by (simp add: E_generates)
   4.220 -    also have "(\<lambda>x. x i) -` A \<inter> space ?P = {f \<in> \<Pi>\<^sub>E i\<in>I. space (M i). f i \<in> A}"
   4.221 -      using P_closed by (auto simp: space_PiM)
   4.222 -    finally show "\<dots> \<in> sets ?P" .
   4.223 -  qed
   4.224 -  finally show "sets (PiM I M) \<subseteq> sigma_sets (space (PiM I M)) P"
   4.225 -    by (simp add: P_closed)
   4.226 -  show "sigma_sets (space (PiM I M)) P \<subseteq> sets (PiM I M)"
   4.227 -    using `finite I`
   4.228 -    by (auto intro!: sets.sigma_sets_subset sets_PiM_I_finite simp: E_generates P_def)
   4.229 -qed
   4.230 -
   4.231  lemma pair_measure_eq_distr_PiM:
   4.232    fixes M1 :: "'a measure" and M2 :: "'a measure"
   4.233    assumes "sigma_finite_measure M1" "sigma_finite_measure M2"
     5.1 --- a/src/HOL/Probability/Measurable.thy	Wed Dec 03 22:44:24 2014 +0100
     5.2 +++ b/src/HOL/Probability/Measurable.thy	Thu Dec 04 17:05:58 2014 +0100
     5.3 @@ -377,105 +377,129 @@
     5.4    qed
     5.5  qed rule
     5.6  
     5.7 +lemma measurable_pred_countable[measurable (raw)]:
     5.8 +  assumes "countable X"
     5.9 +  shows 
    5.10 +    "(\<And>i. i \<in> X \<Longrightarrow> Measurable.pred M (\<lambda>x. P x i)) \<Longrightarrow> Measurable.pred M (\<lambda>x. \<forall>i\<in>X. P x i)"
    5.11 +    "(\<And>i. i \<in> X \<Longrightarrow> Measurable.pred M (\<lambda>x. P x i)) \<Longrightarrow> Measurable.pred M (\<lambda>x. \<exists>i\<in>X. P x i)"
    5.12 +  unfolding pred_def
    5.13 +  by (auto intro!: sets.sets_Collect_countable_All' sets.sets_Collect_countable_Ex' assms)
    5.14 +
    5.15  subsection {* Measurability for (co)inductive predicates *}
    5.16  
    5.17 +lemma measurable_bot[measurable]: "bot \<in> measurable M (count_space UNIV)"
    5.18 +  by (simp add: bot_fun_def)
    5.19 +
    5.20 +lemma measurable_top[measurable]: "top \<in> measurable M (count_space UNIV)"
    5.21 +  by (simp add: top_fun_def)
    5.22 +
    5.23 +lemma measurable_SUP[measurable]:
    5.24 +  fixes F :: "'i \<Rightarrow> 'a \<Rightarrow> 'b::{complete_lattice, countable}"
    5.25 +  assumes [simp]: "countable I"
    5.26 +  assumes [measurable]: "\<And>i. i \<in> I \<Longrightarrow> F i \<in> measurable M (count_space UNIV)"
    5.27 +  shows "(\<lambda>x. SUP i:I. F i x) \<in> measurable M (count_space UNIV)"
    5.28 +  unfolding measurable_count_space_eq2_countable
    5.29 +proof (safe intro!: UNIV_I)
    5.30 +  fix a 
    5.31 +  have "(\<lambda>x. SUP i:I. F i x) -` {a} \<inter> space M =
    5.32 +    {x\<in>space M. (\<forall>i\<in>I. F i x \<le> a) \<and> (\<forall>b. (\<forall>i\<in>I. F i x \<le> b) \<longrightarrow> a \<le> b)}"
    5.33 +    unfolding SUP_le_iff[symmetric] by auto
    5.34 +  also have "\<dots> \<in> sets M"
    5.35 +    by measurable
    5.36 +  finally show "(\<lambda>x. SUP i:I. F i x) -` {a} \<inter> space M \<in> sets M" .
    5.37 +qed
    5.38 +
    5.39 +lemma measurable_INF[measurable]:
    5.40 +  fixes F :: "'i \<Rightarrow> 'a \<Rightarrow> 'b::{complete_lattice, countable}"
    5.41 +  assumes [simp]: "countable I"
    5.42 +  assumes [measurable]: "\<And>i. i \<in> I \<Longrightarrow> F i \<in> measurable M (count_space UNIV)"
    5.43 +  shows "(\<lambda>x. INF i:I. F i x) \<in> measurable M (count_space UNIV)"
    5.44 +  unfolding measurable_count_space_eq2_countable
    5.45 +proof (safe intro!: UNIV_I)
    5.46 +  fix a 
    5.47 +  have "(\<lambda>x. INF i:I. F i x) -` {a} \<inter> space M =
    5.48 +    {x\<in>space M. (\<forall>i\<in>I. a \<le> F i x) \<and> (\<forall>b. (\<forall>i\<in>I. b \<le> F i x) \<longrightarrow> b \<le> a)}"
    5.49 +    unfolding le_INF_iff[symmetric] by auto
    5.50 +  also have "\<dots> \<in> sets M"
    5.51 +    by measurable
    5.52 +  finally show "(\<lambda>x. INF i:I. F i x) -` {a} \<inter> space M \<in> sets M" .
    5.53 +qed
    5.54 +
    5.55 +lemma measurable_lfp_coinduct[consumes 1, case_names continuity step]:
    5.56 +  fixes F :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b::{complete_lattice, countable})"
    5.57 +  assumes "P M"
    5.58 +  assumes F: "Order_Continuity.continuous F"
    5.59 +  assumes *: "\<And>M A. P M \<Longrightarrow> (\<And>N. P N \<Longrightarrow> A \<in> measurable N (count_space UNIV)) \<Longrightarrow> F A \<in> measurable M (count_space UNIV)"
    5.60 +  shows "lfp F \<in> measurable M (count_space UNIV)"
    5.61 +proof -
    5.62 +  { fix i from `P M` have "((F ^^ i) bot) \<in> measurable M (count_space UNIV)"
    5.63 +      by (induct i arbitrary: M) (auto intro!: *) }
    5.64 +  then have "(\<lambda>x. SUP i. (F ^^ i) bot x) \<in> measurable M (count_space UNIV)"
    5.65 +    by measurable
    5.66 +  also have "(\<lambda>x. SUP i. (F ^^ i) bot x) = lfp F"
    5.67 +    by (subst continuous_lfp) (auto intro: F)
    5.68 +  finally show ?thesis .
    5.69 +qed
    5.70 +
    5.71  lemma measurable_lfp:
    5.72 -  assumes "Order_Continuity.continuous F"
    5.73 -  assumes *: "\<And>A. pred M A \<Longrightarrow> pred M (F A)"
    5.74 -  shows "pred M (lfp F)"
    5.75 +  fixes F :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b::{complete_lattice, countable})"
    5.76 +  assumes F: "Order_Continuity.continuous F"
    5.77 +  assumes *: "\<And>A. A \<in> measurable M (count_space UNIV) \<Longrightarrow> F A \<in> measurable M (count_space UNIV)"
    5.78 +  shows "lfp F \<in> measurable M (count_space UNIV)"
    5.79 +  by (coinduction rule: measurable_lfp_coinduct[OF _ F]) (blast intro: *)
    5.80 +
    5.81 +lemma measurable_gfp_coinduct[consumes 1, case_names continuity step]:
    5.82 +  fixes F :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b::{complete_lattice, countable})"
    5.83 +  assumes "P M"
    5.84 +  assumes F: "Order_Continuity.down_continuous F"
    5.85 +  assumes *: "\<And>M A. P M \<Longrightarrow> (\<And>N. P N \<Longrightarrow> A \<in> measurable N (count_space UNIV)) \<Longrightarrow> F A \<in> measurable M (count_space UNIV)"
    5.86 +  shows "gfp F \<in> measurable M (count_space UNIV)"
    5.87  proof -
    5.88 -  { fix i have "Measurable.pred M (\<lambda>x. (F ^^ i) (\<lambda>x. False) x)"
    5.89 -      by (induct i) (auto intro!: *) }
    5.90 -  then have "Measurable.pred M (\<lambda>x. \<exists>i. (F ^^ i) (\<lambda>x. False) x)"
    5.91 +  { fix i from `P M` have "((F ^^ i) top) \<in> measurable M (count_space UNIV)"
    5.92 +      by (induct i arbitrary: M) (auto intro!: *) }
    5.93 +  then have "(\<lambda>x. INF i. (F ^^ i) top x) \<in> measurable M (count_space UNIV)"
    5.94      by measurable
    5.95 -  also have "(\<lambda>x. \<exists>i. (F ^^ i) (\<lambda>x. False) x) = (SUP i. (F ^^ i) bot)"
    5.96 -    by (auto simp add: bot_fun_def)
    5.97 -  also have "\<dots> = lfp F"
    5.98 -    by (rule continuous_lfp[symmetric]) fact
    5.99 +  also have "(\<lambda>x. INF i. (F ^^ i) top x) = gfp F"
   5.100 +    by (subst down_continuous_gfp) (auto intro: F)
   5.101    finally show ?thesis .
   5.102  qed
   5.103  
   5.104  lemma measurable_gfp:
   5.105 -  assumes "Order_Continuity.down_continuous F"
   5.106 -  assumes *: "\<And>A. pred M A \<Longrightarrow> pred M (F A)"
   5.107 -  shows "pred M (gfp F)"
   5.108 -proof -
   5.109 -  { fix i have "Measurable.pred M (\<lambda>x. (F ^^ i) (\<lambda>x. True) x)"
   5.110 -      by (induct i) (auto intro!: *) }
   5.111 -  then have "Measurable.pred M (\<lambda>x. \<forall>i. (F ^^ i) (\<lambda>x. True) x)"
   5.112 -    by measurable
   5.113 -  also have "(\<lambda>x. \<forall>i. (F ^^ i) (\<lambda>x. True) x) = (INF i. (F ^^ i) top)"
   5.114 -    by (auto simp add: top_fun_def)
   5.115 -  also have "\<dots> = gfp F"
   5.116 -    by (rule down_continuous_gfp[symmetric]) fact
   5.117 -  finally show ?thesis .
   5.118 -qed
   5.119 -
   5.120 -lemma measurable_lfp_coinduct[consumes 1, case_names continuity step]:
   5.121 -  assumes "P M"
   5.122 -  assumes "Order_Continuity.continuous F"
   5.123 -  assumes *: "\<And>M A. P M \<Longrightarrow> (\<And>N. P N \<Longrightarrow> Measurable.pred N A) \<Longrightarrow> Measurable.pred M (F A)"
   5.124 -  shows "Measurable.pred M (lfp F)"
   5.125 -proof -
   5.126 -  { fix i from `P M` have "Measurable.pred M (\<lambda>x. (F ^^ i) (\<lambda>x. False) x)"
   5.127 -      by (induct i arbitrary: M) (auto intro!: *) }
   5.128 -  then have "Measurable.pred M (\<lambda>x. \<exists>i. (F ^^ i) (\<lambda>x. False) x)"
   5.129 -    by measurable
   5.130 -  also have "(\<lambda>x. \<exists>i. (F ^^ i) (\<lambda>x. False) x) = (SUP i. (F ^^ i) bot)"
   5.131 -    by (auto simp add: bot_fun_def)
   5.132 -  also have "\<dots> = lfp F"
   5.133 -    by (rule continuous_lfp[symmetric]) fact
   5.134 -  finally show ?thesis .
   5.135 -qed
   5.136 -
   5.137 -lemma measurable_gfp_coinduct[consumes 1, case_names continuity step]:
   5.138 -  assumes "P M"
   5.139 -  assumes "Order_Continuity.down_continuous F"
   5.140 -  assumes *: "\<And>M A. P M \<Longrightarrow> (\<And>N. P N \<Longrightarrow> Measurable.pred N A) \<Longrightarrow> Measurable.pred M (F A)"
   5.141 -  shows "Measurable.pred M (gfp F)"
   5.142 -proof -
   5.143 -  { fix i from `P M` have "Measurable.pred M (\<lambda>x. (F ^^ i) (\<lambda>x. True) x)"
   5.144 -      by (induct i arbitrary: M) (auto intro!: *) }
   5.145 -  then have "Measurable.pred M (\<lambda>x. \<forall>i. (F ^^ i) (\<lambda>x. True) x)"
   5.146 -    by measurable
   5.147 -  also have "(\<lambda>x. \<forall>i. (F ^^ i) (\<lambda>x. True) x) = (INF i. (F ^^ i) top)"
   5.148 -    by (auto simp add: top_fun_def)
   5.149 -  also have "\<dots> = gfp F"
   5.150 -    by (rule down_continuous_gfp[symmetric]) fact
   5.151 -  finally show ?thesis .
   5.152 -qed
   5.153 +  fixes F :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b::{complete_lattice, countable})"
   5.154 +  assumes F: "Order_Continuity.down_continuous F"
   5.155 +  assumes *: "\<And>A. A \<in> measurable M (count_space UNIV) \<Longrightarrow> F A \<in> measurable M (count_space UNIV)"
   5.156 +  shows "gfp F \<in> measurable M (count_space UNIV)"
   5.157 +  by (coinduction rule: measurable_gfp_coinduct[OF _ F]) (blast intro: *)
   5.158  
   5.159  lemma measurable_lfp2_coinduct[consumes 1, case_names continuity step]:
   5.160 +  fixes F :: "('a \<Rightarrow> 'c \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'c \<Rightarrow> 'b::{complete_lattice, countable})"
   5.161    assumes "P M s"
   5.162 -  assumes "Order_Continuity.continuous F"
   5.163 -  assumes *: "\<And>M A s. P M s \<Longrightarrow> (\<And>N t. P N t \<Longrightarrow> Measurable.pred N (A t)) \<Longrightarrow> Measurable.pred M (F A s)"
   5.164 -  shows "Measurable.pred M (lfp F s)"
   5.165 +  assumes F: "Order_Continuity.continuous F"
   5.166 +  assumes *: "\<And>M A s. P M s \<Longrightarrow> (\<And>N t. P N t \<Longrightarrow> A t \<in> measurable N (count_space UNIV)) \<Longrightarrow> F A s \<in> measurable M (count_space UNIV)"
   5.167 +  shows "lfp F s \<in> measurable M (count_space UNIV)"
   5.168  proof -
   5.169 -  { fix i from `P M s` have "Measurable.pred M (\<lambda>x. (F ^^ i) (\<lambda>t x. False) s x)"
   5.170 +  { fix i from `P M s` have "(\<lambda>x. (F ^^ i) bot s x) \<in> measurable M (count_space UNIV)"
   5.171        by (induct i arbitrary: M s) (auto intro!: *) }
   5.172 -  then have "Measurable.pred M (\<lambda>x. \<exists>i. (F ^^ i) (\<lambda>t x. False) s x)"
   5.173 +  then have "(\<lambda>x. SUP i. (F ^^ i) bot s x) \<in> measurable M (count_space UNIV)"
   5.174      by measurable
   5.175 -  also have "(\<lambda>x. \<exists>i. (F ^^ i) (\<lambda>t x. False) s x) = (SUP i. (F ^^ i) bot) s"
   5.176 -    by (auto simp add: bot_fun_def)
   5.177 -  also have "(SUP i. (F ^^ i) bot) = lfp F"
   5.178 -    by (rule continuous_lfp[symmetric]) fact
   5.179 +  also have "(\<lambda>x. SUP i. (F ^^ i) bot s x) = lfp F s"
   5.180 +    by (subst continuous_lfp) (auto simp: F)
   5.181    finally show ?thesis .
   5.182  qed
   5.183  
   5.184  lemma measurable_gfp2_coinduct[consumes 1, case_names continuity step]:
   5.185 +  fixes F :: "('a \<Rightarrow> 'c \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'c \<Rightarrow> 'b::{complete_lattice, countable})"
   5.186    assumes "P M s"
   5.187 -  assumes "Order_Continuity.down_continuous F"
   5.188 -  assumes *: "\<And>M A s. P M s \<Longrightarrow> (\<And>N t. P N t \<Longrightarrow> Measurable.pred N (A t)) \<Longrightarrow> Measurable.pred M (F A s)"
   5.189 -  shows "Measurable.pred M (gfp F s)"
   5.190 +  assumes F: "Order_Continuity.down_continuous F"
   5.191 +  assumes *: "\<And>M A s. P M s \<Longrightarrow> (\<And>N t. P N t \<Longrightarrow> A t \<in> measurable N (count_space UNIV)) \<Longrightarrow> F A s \<in> measurable M (count_space UNIV)"
   5.192 +  shows "gfp F s \<in> measurable M (count_space UNIV)"
   5.193  proof -
   5.194 -  { fix i from `P M s` have "Measurable.pred M (\<lambda>x. (F ^^ i) (\<lambda>t x. True) s x)"
   5.195 +  { fix i from `P M s` have "(\<lambda>x. (F ^^ i) top s x) \<in> measurable M (count_space UNIV)"
   5.196        by (induct i arbitrary: M s) (auto intro!: *) }
   5.197 -  then have "Measurable.pred M (\<lambda>x. \<forall>i. (F ^^ i) (\<lambda>t x. True) s x)"
   5.198 +  then have "(\<lambda>x. INF i. (F ^^ i) top s x) \<in> measurable M (count_space UNIV)"
   5.199      by measurable
   5.200 -  also have "(\<lambda>x. \<forall>i. (F ^^ i) (\<lambda>t x. True) s x) = (INF i. (F ^^ i) top) s"
   5.201 -    by (auto simp add: top_fun_def)
   5.202 -  also have "(INF i. (F ^^ i) top) = gfp F"
   5.203 -    by (rule down_continuous_gfp[symmetric]) fact
   5.204 +  also have "(\<lambda>x. INF i. (F ^^ i) top s x) = gfp F s"
   5.205 +    by (subst down_continuous_gfp) (auto simp: F)
   5.206    finally show ?thesis .
   5.207  qed
   5.208  
   5.209 @@ -531,14 +555,6 @@
   5.210    qed (simp add: fin)
   5.211  qed
   5.212  
   5.213 -lemma measurable_pred_countable[measurable (raw)]:
   5.214 -  assumes "countable X"
   5.215 -  shows 
   5.216 -    "(\<And>i. i \<in> X \<Longrightarrow> Measurable.pred M (\<lambda>x. P x i)) \<Longrightarrow> Measurable.pred M (\<lambda>x. \<forall>i\<in>X. P x i)"
   5.217 -    "(\<And>i. i \<in> X \<Longrightarrow> Measurable.pred M (\<lambda>x. P x i)) \<Longrightarrow> Measurable.pred M (\<lambda>x. \<exists>i\<in>X. P x i)"
   5.218 -  unfolding pred_def
   5.219 -  by (auto intro!: sets.sets_Collect_countable_All' sets.sets_Collect_countable_Ex' assms)
   5.220 -
   5.221  lemma measurable_THE:
   5.222    fixes P :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
   5.223    assumes [measurable]: "\<And>i. Measurable.pred M (P i)"
   5.224 @@ -565,12 +581,6 @@
   5.225    finally show "f -` X \<inter> space M \<in> sets M" .
   5.226  qed simp
   5.227  
   5.228 -lemma measurable_bot[measurable]: "Measurable.pred M bot"
   5.229 -  by (simp add: bot_fun_def)
   5.230 -
   5.231 -lemma measurable_top[measurable]: "Measurable.pred M top"
   5.232 -  by (simp add: top_fun_def)
   5.233 -
   5.234  lemma measurable_Ex1[measurable (raw)]:
   5.235    assumes [simp]: "countable I" and [measurable]: "\<And>i. i \<in> I \<Longrightarrow> Measurable.pred M (P i)"
   5.236    shows "Measurable.pred M (\<lambda>x. \<exists>!i\<in>I. P i x)"
     6.1 --- a/src/HOL/Probability/Sigma_Algebra.thy	Wed Dec 03 22:44:24 2014 +0100
     6.2 +++ b/src/HOL/Probability/Sigma_Algebra.thy	Thu Dec 04 17:05:58 2014 +0100
     6.3 @@ -364,6 +364,9 @@
     6.4    finally show ?thesis .
     6.5  qed
     6.6  
     6.7 +lemma (in sigma_algebra) countable_INT'':
     6.8 +  "UNIV \<in> M \<Longrightarrow> countable I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> F i \<in> M) \<Longrightarrow> (\<Inter>i\<in>I. F i) \<in> M"
     6.9 +  by (cases "I = {}") (auto intro: countable_INT')
    6.10  
    6.11  lemma (in sigma_algebra) countable:
    6.12    assumes "\<And>a. a \<in> A \<Longrightarrow> {a} \<in> M" "countable A"
    6.13 @@ -2285,6 +2288,30 @@
    6.14      using measurable_space[OF f] M by auto
    6.15  qed (auto intro: measurable_sets f dest: sets.sets_into_space)
    6.16  
    6.17 +lemma Sup_sigma_sigma:
    6.18 +  assumes [simp]: "M \<noteq> {}" and M: "\<And>m. m \<in> M \<Longrightarrow> m \<subseteq> Pow \<Omega>"
    6.19 +  shows "(\<Squnion>\<^sub>\<sigma> m\<in>M. sigma \<Omega> m) = sigma \<Omega> (\<Union>M)"
    6.20 +proof (rule measure_eqI)
    6.21 +  { fix a m assume "a \<in> sigma_sets \<Omega> m" "m \<in> M"
    6.22 +    then have "a \<in> sigma_sets \<Omega> (\<Union>M)"
    6.23 +     by induction (auto intro: sigma_sets.intros) }
    6.24 +  then show "sets (\<Squnion>\<^sub>\<sigma> m\<in>M. sigma \<Omega> m) = sets (sigma \<Omega> (\<Union>M))"
    6.25 +    apply (simp add: sets_Sup_sigma space_measure_of_conv M Union_least)
    6.26 +    apply (rule sigma_sets_eqI)
    6.27 +    apply auto
    6.28 +    done
    6.29 +qed (simp add: Sup_sigma_def emeasure_sigma)
    6.30 +
    6.31 +lemma SUP_sigma_sigma:
    6.32 +  assumes M: "M \<noteq> {}" "\<And>m. m \<in> M \<Longrightarrow> f m \<subseteq> Pow \<Omega>"
    6.33 +  shows "(\<Squnion>\<^sub>\<sigma> m\<in>M. sigma \<Omega> (f m)) = sigma \<Omega> (\<Union>m\<in>M. f m)"
    6.34 +proof -
    6.35 +  have "Sup_sigma (sigma \<Omega> ` f ` M) = sigma \<Omega> (\<Union>(f ` M))"
    6.36 +    using M by (intro Sup_sigma_sigma) auto
    6.37 +  then show ?thesis
    6.38 +    by (simp add: image_image)
    6.39 +qed
    6.40 +
    6.41  subsection {* The smallest $\sigma$-algebra regarding a function *}
    6.42  
    6.43  definition
    6.44 @@ -2332,10 +2359,20 @@
    6.45    finally show "g -` A \<inter> space N \<in> sets N" .
    6.46  qed (insert g, auto)
    6.47  
    6.48 +lemma vimage_algebra_sigma:
    6.49 +  assumes X: "X \<subseteq> Pow \<Omega>'" and f: "f \<in> \<Omega> \<rightarrow> \<Omega>'"
    6.50 +  shows "vimage_algebra \<Omega> f (sigma \<Omega>' X) = sigma \<Omega> {f -` A \<inter> \<Omega> | A. A \<in> X }" (is "?V = ?S")
    6.51 +proof (rule measure_eqI)
    6.52 +  have \<Omega>: "{f -` A \<inter> \<Omega> |A. A \<in> X} \<subseteq> Pow \<Omega>" by auto
    6.53 +  show "sets ?V = sets ?S"
    6.54 +    using sigma_sets_vimage_commute[OF f, of X]
    6.55 +    by (simp add: space_measure_of_conv f sets_vimage_algebra2 \<Omega> X)
    6.56 +qed (simp add: vimage_algebra_def emeasure_sigma)
    6.57 +
    6.58  lemma vimage_algebra_vimage_algebra_eq:
    6.59    assumes *: "f \<in> X \<rightarrow> Y" "g \<in> Y \<rightarrow> space M"
    6.60    shows "vimage_algebra X f (vimage_algebra Y g M) = vimage_algebra X (\<lambda>x. g (f x)) M"
    6.61 -  (is "?VV = ?V")
    6.62 +    (is "?VV = ?V")
    6.63  proof (rule measure_eqI)
    6.64    have "(\<lambda>x. g (f x)) \<in> X \<rightarrow> space M" "\<And>A. A \<inter> f -` Y \<inter> X = A \<inter> X"
    6.65      using * by auto