author hoelzl Thu Dec 04 17:05:58 2014 +0100 (2014-12-04) changeset 59088 ff2bd4a14ddb parent 59087 8535cfcfa493 child 59089 da2fef2faa83
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
     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.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