generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
--- a/src/HOL/Probability/Binary_Product_Measure.thy Wed Dec 03 22:44:24 2014 +0100
+++ b/src/HOL/Probability/Binary_Product_Measure.thy Thu Dec 04 17:05:58 2014 +0100
@@ -594,6 +594,65 @@
subsection {* Products on counting spaces, densities and distributions *}
+lemma sigma_prod:
+ assumes X_cover: "\<exists>E\<subseteq>A. countable E \<and> X = \<Union>E" and A: "A \<subseteq> Pow X"
+ assumes Y_cover: "\<exists>E\<subseteq>B. countable E \<and> Y = \<Union>E" and B: "B \<subseteq> Pow Y"
+ 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}"
+ (is "?P = ?S")
+proof (rule measure_eqI)
+ have [simp]: "snd \<in> X \<times> Y \<rightarrow> Y" "fst \<in> X \<times> Y \<rightarrow> X"
+ by auto
+ let ?XY = "{{fst -` a \<inter> X \<times> Y | a. a \<in> A}, {snd -` b \<inter> X \<times> Y | b. b \<in> B}}"
+ have "sets ?P =
+ sets (\<Squnion>\<^sub>\<sigma> xy\<in>?XY. sigma (X \<times> Y) xy)"
+ by (simp add: vimage_algebra_sigma sets_pair_eq_sets_fst_snd A B)
+ also have "\<dots> = sets (sigma (X \<times> Y) (\<Union>?XY))"
+ by (intro Sup_sigma_sigma arg_cong[where f=sets]) auto
+ also have "\<dots> = sets ?S"
+ proof (intro arg_cong[where f=sets] sigma_eqI sigma_sets_eqI)
+ 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)"
+ using A B by auto
+ next
+ interpret XY: sigma_algebra "X \<times> Y" "sigma_sets (X \<times> Y) {a \<times> b |a b. a \<in> A \<and> b \<in> B}"
+ using A B by (intro sigma_algebra_sigma_sets) auto
+ fix Z assume "Z \<in> \<Union>?XY"
+ then show "Z \<in> sigma_sets (X \<times> Y) {a \<times> b |a b. a \<in> A \<and> b \<in> B}"
+ proof safe
+ fix a assume "a \<in> A"
+ from Y_cover obtain E where E: "E \<subseteq> B" "countable E" and "Y = \<Union>E"
+ by auto
+ with `a \<in> A` A have eq: "fst -` a \<inter> X \<times> Y = (\<Union>e\<in>E. a \<times> e)"
+ by auto
+ 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}"
+ using `a \<in> A` E unfolding eq by (auto intro!: XY.countable_UN')
+ next
+ fix b assume "b \<in> B"
+ from X_cover obtain E where E: "E \<subseteq> A" "countable E" and "X = \<Union>E"
+ by auto
+ with `b \<in> B` B have eq: "snd -` b \<inter> X \<times> Y = (\<Union>e\<in>E. e \<times> b)"
+ by auto
+ 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}"
+ using `b \<in> B` E unfolding eq by (auto intro!: XY.countable_UN')
+ qed
+ next
+ fix Z assume "Z \<in> {a \<times> b |a b. a \<in> A \<and> b \<in> B}"
+ then obtain a b where "Z = a \<times> b" and ab: "a \<in> A" "b \<in> B"
+ by auto
+ then have Z: "Z = (fst -` a \<inter> X \<times> Y) \<inter> (snd -` b \<inter> X \<times> Y)"
+ using A B by auto
+ interpret XY: sigma_algebra "X \<times> Y" "sigma_sets (X \<times> Y) (\<Union>?XY)"
+ by (intro sigma_algebra_sigma_sets) auto
+ show "Z \<in> sigma_sets (X \<times> Y) (\<Union>?XY)"
+ unfolding Z by (rule XY.Int) (blast intro: ab)+
+ qed
+ finally show "sets ?P = sets ?S" .
+next
+ interpret finite_measure "sigma X A" for X A
+ proof qed (simp add: emeasure_sigma)
+ fix A assume "A \<in> sets ?P" then show "emeasure ?P A = emeasure ?S A"
+ by (simp add: emeasure_pair_measure_alt emeasure_sigma)
+qed
+
lemma sigma_sets_pair_measure_generator_finite:
assumes "finite A" and "finite B"
shows "sigma_sets (A \<times> B) { a \<times> b | a b. a \<subseteq> A \<and> b \<subseteq> B} = Pow (A \<times> B)"
@@ -618,6 +677,18 @@
show "a \<in> A" and "b \<in> B" by auto
qed
+lemma borel_prod:
+ "(borel \<Otimes>\<^sub>M borel) = (borel :: ('a::second_countable_topology \<times> 'b::second_countable_topology) measure)"
+ (is "?P = ?B")
+proof -
+ have "?B = sigma UNIV {A \<times> B | A B. open A \<and> open B}"
+ by (rule second_countable_borel_measurable[OF open_prod_generated])
+ also have "\<dots> = ?P"
+ unfolding borel_def
+ by (subst sigma_prod) (auto intro!: exI[of _ "{UNIV}"])
+ finally show ?thesis ..
+qed
+
lemma pair_measure_count_space:
assumes A: "finite A" and B: "finite B"
shows "count_space A \<Otimes>\<^sub>M count_space B = count_space (A \<times> B)" (is "?P = ?C")
@@ -821,50 +892,6 @@
by auto
qed
-lemma borel_prod: "sets (borel \<Otimes>\<^sub>M borel) =
- (sets borel :: ('a::second_countable_topology \<times> 'b::second_countable_topology) set set)"
- (is "?l = ?r")
-proof -
- obtain A :: "'a set set" where A: "countable A" "topological_basis A"
- by (metis ex_countable_basis)
- moreover obtain B :: "'b set set" where B: "countable B" "topological_basis B"
- by (metis ex_countable_basis)
- ultimately have AB: "countable ((\<lambda>(a, b). a \<times> b) ` (A \<times> B))" "topological_basis ((\<lambda>(a, b). a \<times> b) ` (A \<times> B))"
- by (auto intro!: topological_basis_prod)
- 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}"
- by (simp add: sets_pair_measure
- borel_eq_countable_basis[OF A] borel_eq_countable_basis[OF B])
- also have "\<dots> \<supseteq> sigma_sets UNIV ((\<lambda>(a, b). a \<times> b) ` (A \<times> B))" (is "... \<supseteq> ?A")
- by (auto intro!: sigma_sets_mono)
- also (xtrans) have "?A = sets borel"
- by (simp add: borel_eq_countable_basis[OF AB])
- finally have "?r \<subseteq> ?l" .
- moreover have "?l \<subseteq> ?r"
- proof (simp add: sets_pair_measure, safe intro!: sigma_sets_mono)
- 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}"
- then show "A \<in> sets borel"
- by (induct A) (auto intro!: borel_Times)
- qed
- ultimately show ?thesis by auto
-qed
-
-lemma borel_prod':
- "borel \<Otimes>\<^sub>M borel = (borel ::
- ('a::second_countable_topology \<times> 'b::second_countable_topology) measure)"
-proof (rule measure_eqI[OF borel_prod])
- interpret sigma_finite_measure "borel :: 'b measure"
- proof qed (intro exI[of _ "{UNIV}"], auto simp: borel_def emeasure_sigma)
- fix X :: "('a \<times> 'b) set" assume asm: "X \<in> sets (borel \<Otimes>\<^sub>M borel)"
- have "UNIV \<times> UNIV \<in> sets (borel \<Otimes>\<^sub>M borel :: ('a \<times> 'b) measure)"
- by (simp add: borel_prod)
- moreover have "emeasure (borel \<Otimes>\<^sub>M borel) (UNIV \<times> UNIV :: ('a \<times> 'b) set) = 0"
- by (subst emeasure_pair_measure_Times, simp_all add: borel_def emeasure_sigma)
- moreover have "X \<subseteq> UNIV \<times> UNIV" by auto
- ultimately have "emeasure (borel \<Otimes>\<^sub>M borel) X = 0" by (rule emeasure_eq_0)
- thus "emeasure (borel \<Otimes>\<^sub>M borel) X = emeasure borel X"
- by (simp add: borel_def emeasure_sigma)
-qed
-
lemma finite_measure_pair_measure:
assumes "finite_measure M" "finite_measure N"
shows "finite_measure (N \<Otimes>\<^sub>M M)"
--- a/src/HOL/Probability/Borel_Space.thy Wed Dec 03 22:44:24 2014 +0100
+++ b/src/HOL/Probability/Borel_Space.thy Thu Dec 04 17:05:58 2014 +0100
@@ -11,6 +11,17 @@
"~~/src/HOL/Multivariate_Analysis/Multivariate_Analysis"
begin
+lemma topological_basis_trivial: "topological_basis {A. open A}"
+ by (auto simp: topological_basis_def)
+
+lemma open_prod_generated: "open = generate_topology {A \<times> B | A B. open A \<and> open B}"
+proof -
+ 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}))"
+ by auto
+ then show ?thesis
+ by (auto intro: topological_basis_prod topological_basis_trivial topological_basis_imp_subbasis)
+qed
+
subsection {* Generic Borel spaces *}
definition borel :: "'a::topological_space measure" where
@@ -147,6 +158,50 @@
lemma borel_compact: "compact (A::'a::t2_space set) \<Longrightarrow> A \<in> sets borel"
by (auto intro: borel_closed dest!: compact_imp_closed)
+lemma second_countable_borel_measurable:
+ fixes X :: "'a::second_countable_topology set set"
+ assumes eq: "open = generate_topology X"
+ shows "borel = sigma UNIV X"
+ unfolding borel_def
+proof (intro sigma_eqI sigma_sets_eqI)
+ interpret X: sigma_algebra UNIV "sigma_sets UNIV X"
+ by (rule sigma_algebra_sigma_sets) simp
+
+ fix S :: "'a set" assume "S \<in> Collect open"
+ then have "generate_topology X S"
+ by (auto simp: eq)
+ then show "S \<in> sigma_sets UNIV X"
+ proof induction
+ case (UN K)
+ then have K: "\<And>k. k \<in> K \<Longrightarrow> open k"
+ unfolding eq by auto
+ from ex_countable_basis obtain B :: "'a set set" where
+ B: "\<And>b. b \<in> B \<Longrightarrow> open b" "\<And>X. open X \<Longrightarrow> \<exists>b\<subseteq>B. (\<Union>b) = X" and "countable B"
+ by (auto simp: topological_basis_def)
+ 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"
+ by metis
+ def U \<equiv> "(\<Union>k\<in>K. m k)"
+ with m have "countable U"
+ by (intro countable_subset[OF _ `countable B`]) auto
+ have "\<Union>U = (\<Union>A\<in>U. A)" by simp
+ also have "\<dots> = \<Union>K"
+ unfolding U_def UN_simps by (simp add: m)
+ finally have "\<Union>U = \<Union>K" .
+
+ have "\<forall>b\<in>U. \<exists>k\<in>K. b \<subseteq> k"
+ using m by (auto simp: U_def)
+ 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"
+ by metis
+ then have "(\<Union>b\<in>U. u b) \<subseteq> \<Union>K" "\<Union>U \<subseteq> (\<Union>b\<in>U. u b)"
+ by auto
+ then have "\<Union>K = (\<Union>b\<in>U. u b)"
+ unfolding `\<Union>U = \<Union>K` by auto
+ also have "\<dots> \<in> sigma_sets UNIV X"
+ using u UN by (intro X.countable_UN' `countable U`) auto
+ finally show "\<Union>K \<in> sigma_sets UNIV X" .
+ qed auto
+qed (auto simp: eq intro: generate_topology.Basis)
+
lemma borel_measurable_continuous_on_if:
assumes A: "A \<in> sets borel" and f: "continuous_on A f" and g: "continuous_on (- A) g"
shows "(\<lambda>x. if x \<in> A then f x else g x) \<in> borel_measurable borel"
@@ -261,6 +316,145 @@
unfolding eq by (rule borel_measurable_continuous_on[OF H]) auto
qed
+subsection {* Borel spaces on order topologies *}
+
+
+lemma borel_Iio:
+ "borel = sigma UNIV (range lessThan :: 'a::{linorder_topology, second_countable_topology} set set)"
+ unfolding second_countable_borel_measurable[OF open_generated_order]
+proof (intro sigma_eqI sigma_sets_eqI)
+ from countable_dense_setE guess D :: "'a set" . note D = this
+
+ interpret L: sigma_algebra UNIV "sigma_sets UNIV (range lessThan)"
+ by (rule sigma_algebra_sigma_sets) simp
+
+ fix A :: "'a set" assume "A \<in> range lessThan \<union> range greaterThan"
+ then obtain y where "A = {y <..} \<or> A = {..< y}"
+ by blast
+ then show "A \<in> sigma_sets UNIV (range lessThan)"
+ proof
+ assume A: "A = {y <..}"
+ show ?thesis
+ proof cases
+ assume "\<forall>x>y. \<exists>d. y < d \<and> d < x"
+ with D(2)[of "{y <..< x}" for x] have "\<forall>x>y. \<exists>d\<in>D. y < d \<and> d < x"
+ by (auto simp: set_eq_iff)
+ then have "A = UNIV - (\<Inter>d\<in>{d\<in>D. y < d}. {..< d})"
+ by (auto simp: A) (metis less_asym)
+ also have "\<dots> \<in> sigma_sets UNIV (range lessThan)"
+ using D(1) by (intro L.Diff L.top L.countable_INT'') auto
+ finally show ?thesis .
+ next
+ assume "\<not> (\<forall>x>y. \<exists>d. y < d \<and> d < x)"
+ then obtain x where "y < x" "\<And>d. y < d \<Longrightarrow> \<not> d < x"
+ by auto
+ then have "A = UNIV - {..< x}"
+ unfolding A by (auto simp: not_less[symmetric])
+ also have "\<dots> \<in> sigma_sets UNIV (range lessThan)"
+ by auto
+ finally show ?thesis .
+ qed
+ qed auto
+qed auto
+
+lemma borel_Ioi:
+ "borel = sigma UNIV (range greaterThan :: 'a::{linorder_topology, second_countable_topology} set set)"
+ unfolding second_countable_borel_measurable[OF open_generated_order]
+proof (intro sigma_eqI sigma_sets_eqI)
+ from countable_dense_setE guess D :: "'a set" . note D = this
+
+ interpret L: sigma_algebra UNIV "sigma_sets UNIV (range greaterThan)"
+ by (rule sigma_algebra_sigma_sets) simp
+
+ fix A :: "'a set" assume "A \<in> range lessThan \<union> range greaterThan"
+ then obtain y where "A = {y <..} \<or> A = {..< y}"
+ by blast
+ then show "A \<in> sigma_sets UNIV (range greaterThan)"
+ proof
+ assume A: "A = {..< y}"
+ show ?thesis
+ proof cases
+ assume "\<forall>x<y. \<exists>d. x < d \<and> d < y"
+ with D(2)[of "{x <..< y}" for x] have "\<forall>x<y. \<exists>d\<in>D. x < d \<and> d < y"
+ by (auto simp: set_eq_iff)
+ then have "A = UNIV - (\<Inter>d\<in>{d\<in>D. d < y}. {d <..})"
+ by (auto simp: A) (metis less_asym)
+ also have "\<dots> \<in> sigma_sets UNIV (range greaterThan)"
+ using D(1) by (intro L.Diff L.top L.countable_INT'') auto
+ finally show ?thesis .
+ next
+ assume "\<not> (\<forall>x<y. \<exists>d. x < d \<and> d < y)"
+ then obtain x where "x < y" "\<And>d. y > d \<Longrightarrow> x \<ge> d"
+ by (auto simp: not_less[symmetric])
+ then have "A = UNIV - {x <..}"
+ unfolding A Compl_eq_Diff_UNIV[symmetric] by auto
+ also have "\<dots> \<in> sigma_sets UNIV (range greaterThan)"
+ by auto
+ finally show ?thesis .
+ qed
+ qed auto
+qed auto
+
+lemma borel_measurableI_less:
+ fixes f :: "'a \<Rightarrow> 'b::{linorder_topology, second_countable_topology}"
+ shows "(\<And>y. {x\<in>space M. f x < y} \<in> sets M) \<Longrightarrow> f \<in> borel_measurable M"
+ unfolding borel_Iio
+ by (rule measurable_measure_of) (auto simp: Int_def conj_commute)
+
+lemma borel_measurableI_greater:
+ fixes f :: "'a \<Rightarrow> 'b::{linorder_topology, second_countable_topology}"
+ shows "(\<And>y. {x\<in>space M. y < f x} \<in> sets M) \<Longrightarrow> f \<in> borel_measurable M"
+ unfolding borel_Ioi
+ by (rule measurable_measure_of) (auto simp: Int_def conj_commute)
+
+lemma borel_measurable_SUP[measurable (raw)]:
+ fixes F :: "_ \<Rightarrow> _ \<Rightarrow> _::{complete_linorder, linorder_topology, second_countable_topology}"
+ assumes [simp]: "countable I"
+ assumes [measurable]: "\<And>i. i \<in> I \<Longrightarrow> F i \<in> borel_measurable M"
+ shows "(\<lambda>x. SUP i:I. F i x) \<in> borel_measurable M"
+ by (rule borel_measurableI_greater) (simp add: less_SUP_iff)
+
+lemma borel_measurable_INF[measurable (raw)]:
+ fixes F :: "_ \<Rightarrow> _ \<Rightarrow> _::{complete_linorder, linorder_topology, second_countable_topology}"
+ assumes [simp]: "countable I"
+ assumes [measurable]: "\<And>i. i \<in> I \<Longrightarrow> F i \<in> borel_measurable M"
+ shows "(\<lambda>x. INF i:I. F i x) \<in> borel_measurable M"
+ by (rule borel_measurableI_less) (simp add: INF_less_iff)
+
+lemma borel_measurable_lfp[consumes 1, case_names continuity step]:
+ fixes F :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b::{complete_linorder, linorder_topology, second_countable_topology})"
+ assumes "Order_Continuity.continuous F"
+ assumes *: "\<And>f. f \<in> borel_measurable M \<Longrightarrow> F f \<in> borel_measurable M"
+ shows "lfp F \<in> borel_measurable M"
+proof -
+ { fix i have "((F ^^ i) bot) \<in> borel_measurable M"
+ by (induct i) (auto intro!: *) }
+ then have "(\<lambda>x. SUP i. (F ^^ i) bot x) \<in> borel_measurable M"
+ by measurable
+ also have "(\<lambda>x. SUP i. (F ^^ i) bot x) = (SUP i. (F ^^ i) bot)"
+ by auto
+ also have "(SUP i. (F ^^ i) bot) = lfp F"
+ by (rule continuous_lfp[symmetric]) fact
+ finally show ?thesis .
+qed
+
+lemma borel_measurable_gfp[consumes 1, case_names continuity step]:
+ fixes F :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b::{complete_linorder, linorder_topology, second_countable_topology})"
+ assumes "Order_Continuity.down_continuous F"
+ assumes *: "\<And>f. f \<in> borel_measurable M \<Longrightarrow> F f \<in> borel_measurable M"
+ shows "gfp F \<in> borel_measurable M"
+proof -
+ { fix i have "((F ^^ i) top) \<in> borel_measurable M"
+ by (induct i) (auto intro!: * simp: bot_fun_def) }
+ then have "(\<lambda>x. INF i. (F ^^ i) top x) \<in> borel_measurable M"
+ by measurable
+ also have "(\<lambda>x. INF i. (F ^^ i) top x) = (INF i. (F ^^ i) top)"
+ by auto
+ also have "\<dots> = gfp F"
+ by (rule down_continuous_gfp[symmetric]) fact
+ finally show ?thesis .
+qed
+
subsection {* Borel spaces on euclidean spaces *}
lemma borel_measurable_inner[measurable (raw)]:
@@ -1169,32 +1363,6 @@
thus ?thesis using assms by induct auto
qed simp
-lemma borel_measurable_SUP[measurable (raw)]:
- fixes f :: "'d\<Colon>countable \<Rightarrow> 'a \<Rightarrow> ereal"
- assumes "\<And>i. i \<in> A \<Longrightarrow> f i \<in> borel_measurable M"
- shows "(\<lambda>x. SUP i : A. f i x) \<in> borel_measurable M" (is "?sup \<in> borel_measurable M")
- unfolding borel_measurable_ereal_iff_ge
-proof
- fix a
- have "?sup -` {a<..} \<inter> space M = (\<Union>i\<in>A. {x\<in>space M. a < f i x})"
- by (auto simp: less_SUP_iff)
- then show "?sup -` {a<..} \<inter> space M \<in> sets M"
- using assms by auto
-qed
-
-lemma borel_measurable_INF[measurable (raw)]:
- fixes f :: "'d :: countable \<Rightarrow> 'a \<Rightarrow> ereal"
- assumes "\<And>i. i \<in> A \<Longrightarrow> f i \<in> borel_measurable M"
- shows "(\<lambda>x. INF i : A. f i x) \<in> borel_measurable M" (is "?inf \<in> borel_measurable M")
- unfolding borel_measurable_ereal_iff_less
-proof
- fix a
- have "?inf -` {..<a} \<inter> space M = (\<Union>i\<in>A. {x\<in>space M. f i x < a})"
- by (auto simp: INF_less_iff)
- then show "?inf -` {..<a} \<inter> space M \<in> sets M"
- using assms by auto
-qed
-
lemma [measurable (raw)]:
fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> ereal"
assumes "\<And>i. f i \<in> borel_measurable M"
@@ -1325,23 +1493,6 @@
(\<lambda>x. sup (f x) (g x)::ereal) \<in> borel_measurable M"
by simp
-lemma borel_measurable_lfp[consumes 1, case_names continuity step]:
- fixes F :: "('a \<Rightarrow> ereal) \<Rightarrow> ('a \<Rightarrow> ereal)"
- assumes "Order_Continuity.continuous F"
- assumes *: "\<And>f. f \<in> borel_measurable M \<Longrightarrow> F f \<in> borel_measurable M"
- shows "lfp F \<in> borel_measurable M"
-proof -
- { fix i have "((F ^^ i) (\<lambda>t. bot)) \<in> borel_measurable M"
- by (induct i) (auto intro!: * simp: bot_fun_def) }
- then have "(\<lambda>x. SUP i. (F ^^ i) (\<lambda>t. bot) x) \<in> borel_measurable M"
- by measurable
- also have "(\<lambda>x. SUP i. (F ^^ i) (\<lambda>t. bot) x) = (SUP i. (F ^^ i) bot)"
- by (auto simp add: bot_fun_def)
- also have "(SUP i. (F ^^ i) bot) = lfp F"
- by (rule continuous_lfp[symmetric]) fact
- finally show ?thesis .
-qed
-
(* Proof by Jeremy Avigad and Luke Serafin *)
lemma isCont_borel:
fixes f :: "'b::metric_space \<Rightarrow> 'a::metric_space"
--- a/src/HOL/Probability/Fin_Map.thy Wed Dec 03 22:44:24 2014 +0100
+++ b/src/HOL/Probability/Fin_Map.thy Thu Dec 04 17:05:58 2014 +0100
@@ -1005,7 +1005,7 @@
then show "f \<in> (\<Union>n. Pi' I (A n))" by auto
qed (auto simp: Pi'_def `finite I`)
-text {* adapted from @{thm sigma_prod_algebra_sigma_eq} *}
+text {* adapted from @{thm sets_PiM_sigma} *}
lemma sigma_fprod_algebra_sigma_eq:
fixes E :: "'i \<Rightarrow> 'a set set" and S :: "'i \<Rightarrow> nat \<Rightarrow> 'a set"
--- a/src/HOL/Probability/Finite_Product_Measure.thy Wed Dec 03 22:44:24 2014 +0100
+++ b/src/HOL/Probability/Finite_Product_Measure.thy Thu Dec 04 17:05:58 2014 +0100
@@ -362,6 +362,101 @@
apply (auto intro!: arg_cong2[where f=sigma_sets])
done
+lemma
+ shows space_PiM_empty: "space (Pi\<^sub>M {} M) = {\<lambda>k. undefined}"
+ and sets_PiM_empty: "sets (Pi\<^sub>M {} M) = { {}, {\<lambda>k. undefined} }"
+ by (simp_all add: space_PiM sets_PiM_single image_constant sigma_sets_empty_eq)
+
+lemma sets_PiM_sigma:
+ assumes \<Omega>_cover: "\<And>i. i \<in> I \<Longrightarrow> \<exists>S\<subseteq>E i. countable S \<and> \<Omega> i = \<Union>S"
+ assumes E: "\<And>i. i \<in> I \<Longrightarrow> E i \<subseteq> Pow (\<Omega> i)"
+ assumes J: "\<And>j. j \<in> J \<Longrightarrow> finite j" "\<Union>J = I"
+ 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}"
+ shows "sets (\<Pi>\<^sub>M i\<in>I. sigma (\<Omega> i) (E i)) = sets (sigma (\<Pi>\<^sub>E i\<in>I. \<Omega> i) P)"
+proof cases
+ assume "I = {}"
+ with `\<Union>J = I` have "P = {{\<lambda>_. undefined}} \<or> P = {}"
+ by (auto simp: P_def)
+ with `I = {}` show ?thesis
+ by (auto simp add: sets_PiM_empty sigma_sets_empty_eq)
+next
+ let ?F = "\<lambda>i. {(\<lambda>x. x i) -` A \<inter> Pi\<^sub>E I \<Omega> |A. A \<in> E i}"
+ assume "I \<noteq> {}"
+ then have "sets (Pi\<^sub>M I (\<lambda>i. sigma (\<Omega> i) (E i))) =
+ 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)))"
+ by (subst sets_PiM_eq_proj) (auto simp: space_measure_of_conv)
+ also have "\<dots> = sets (\<Squnion>\<^sub>\<sigma> i\<in>I. sigma (Pi\<^sub>E I \<Omega>) (?F i))"
+ using E by (intro SUP_sigma_cong arg_cong[where f=sets] vimage_algebra_sigma) auto
+ also have "\<dots> = sets (sigma (Pi\<^sub>E I \<Omega>) (\<Union>i\<in>I. ?F i))"
+ using `I \<noteq> {}` by (intro arg_cong[where f=sets] SUP_sigma_sigma) auto
+ also have "\<dots> = sets (sigma (Pi\<^sub>E I \<Omega>) P)"
+ proof (intro arg_cong[where f=sets] sigma_eqI sigma_sets_eqI)
+ show "(\<Union>i\<in>I. ?F i) \<subseteq> Pow (Pi\<^sub>E I \<Omega>)" "P \<subseteq> Pow (Pi\<^sub>E I \<Omega>)"
+ by (auto simp: P_def)
+ next
+ interpret P: sigma_algebra "\<Pi>\<^sub>E i\<in>I. \<Omega> i" "sigma_sets (\<Pi>\<^sub>E i\<in>I. \<Omega> i) P"
+ by (auto intro!: sigma_algebra_sigma_sets simp: P_def)
+
+ fix Z assume "Z \<in> (\<Union>i\<in>I. ?F i)"
+ 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>"
+ by auto
+ from `i \<in> I` J obtain j where j: "i \<in> j" "j \<in> J" "j \<subseteq> I" "finite j"
+ by auto
+ obtain S where S: "\<And>i. i \<in> j \<Longrightarrow> S i \<subseteq> E i" "\<And>i. i \<in> j \<Longrightarrow> countable (S i)"
+ "\<And>i. i \<in> j \<Longrightarrow> \<Omega> i = \<Union>(S i)"
+ by (metis subset_eq \<Omega>_cover `j \<subseteq> I`)
+ def A' \<equiv> "\<lambda>n. n(i := A)"
+ then have A'_i: "\<And>n. A' n i = A"
+ by simp
+ { fix n assume "n \<in> Pi\<^sub>E (j - {i}) S"
+ then have "A' n \<in> Pi j E"
+ unfolding PiE_def Pi_def using S(1) by (auto simp: A'_def `A \<in> E i` )
+ with `j \<in> J` have "{f \<in> Pi\<^sub>E I \<Omega>. \<forall>i\<in>j. f i \<in> A' n i} \<in> P"
+ by (auto simp: P_def) }
+ note A'_in_P = this
+
+ { fix x assume "x i \<in> A" "x \<in> Pi\<^sub>E I \<Omega>"
+ with S(3) `j \<subseteq> I` have "\<forall>i\<in>j. \<exists>s\<in>S i. x i \<in> s"
+ by (auto simp: PiE_def Pi_def)
+ 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"
+ by metis
+ with `x i \<in> A` have "\<exists>n\<in>PiE (j-{i}) S. \<forall>i\<in>j. x i \<in> A' n i"
+ by (intro bexI[of _ "restrict (s(i := A)) (j-{i})"]) (auto simp: A'_def split: if_splits) }
+ 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})"
+ unfolding Z_def
+ by (auto simp add: set_eq_iff ball_conj_distrib `i\<in>j` A'_i dest: bspec[OF _ `i\<in>j`]
+ cong: conj_cong)
+ also have "\<dots> \<in> sigma_sets (\<Pi>\<^sub>E i\<in>I. \<Omega> i) P"
+ using `finite j` S(2)
+ by (intro P.countable_UN' countable_PiE) (simp_all add: image_subset_iff A'_in_P)
+ finally show "Z \<in> sigma_sets (\<Pi>\<^sub>E i\<in>I. \<Omega> i) P" .
+ next
+ 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)"
+ by (auto intro!: sigma_algebra_sigma_sets)
+
+ fix b assume "b \<in> P"
+ 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"
+ by (auto simp: P_def)
+ show "b \<in> sigma_sets (Pi\<^sub>E I \<Omega>) (\<Union>i\<in>I. ?F i)"
+ proof cases
+ assume "j = {}"
+ with b have "b = (\<Pi>\<^sub>E i\<in>I. \<Omega> i)"
+ by auto
+ then show ?thesis
+ by blast
+ next
+ assume "j \<noteq> {}"
+ with J b(2,3) have eq: "b = (\<Inter>i\<in>j. ((\<lambda>x. x i) -` A i \<inter> Pi\<^sub>E I \<Omega>))"
+ unfolding b(1)
+ by (auto simp: PiE_def Pi_def)
+ show ?thesis
+ unfolding eq using `A \<in> Pi j E` `j \<in> J` J(2)
+ by (intro F.finite_INT J `j \<in> J` `j \<noteq> {}` sigma_sets.Basic) blast
+ qed
+ qed
+ finally show "?thesis" .
+qed
+
lemma sets_PiM_in_sets:
assumes space: "space N = (\<Pi>\<^sub>E i\<in>I. space (M i))"
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"
@@ -600,11 +695,6 @@
qed
qed
-lemma
- shows space_PiM_empty: "space (Pi\<^sub>M {} M) = {\<lambda>k. undefined}"
- and sets_PiM_empty: "sets (Pi\<^sub>M {} M) = { {}, {\<lambda>k. undefined} }"
- by (simp_all add: space_PiM sets_PiM_single image_constant sigma_sets_empty_eq)
-
lemma emeasure_PiM_empty[simp]: "emeasure (PiM {} M) {\<lambda>_. undefined} = 1"
proof -
let ?\<mu> = "\<lambda>A. if A = {} then 0 else (1::ereal)"
@@ -927,116 +1017,6 @@
"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)"
by simp
-lemma sigma_prod_algebra_sigma_eq_infinite:
- fixes E :: "'i \<Rightarrow> 'a set set"
- assumes S_union: "\<And>i. i \<in> I \<Longrightarrow> (\<Union>j. S i j) = space (M i)"
- and S_in_E: "\<And>i. i \<in> I \<Longrightarrow> range (S i) \<subseteq> E i"
- assumes E_closed: "\<And>i. i \<in> I \<Longrightarrow> E i \<subseteq> Pow (space (M i))"
- and E_generates: "\<And>i. i \<in> I \<Longrightarrow> sets (M i) = sigma_sets (space (M i)) (E i)"
- 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}"
- shows "sets (PiM I M) = sigma_sets (space (PiM I M)) P"
-proof
- let ?P = "sigma (space (Pi\<^sub>M I M)) P"
- have P_closed: "P \<subseteq> Pow (space (Pi\<^sub>M I M))"
- using E_closed by (auto simp: space_PiM P_def subset_eq)
- then have space_P: "space ?P = (\<Pi>\<^sub>E i\<in>I. space (M i))"
- by (simp add: space_PiM)
- have "sets (PiM I M) =
- 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)}"
- using sets_PiM_single[of I M] by (simp add: space_P)
- also have "\<dots> \<subseteq> sets (sigma (space (PiM I M)) P)"
- proof (safe intro!: sets.sigma_sets_subset)
- fix i A assume "i \<in> I" and A: "A \<in> sets (M i)"
- then have "(\<lambda>x. x i) \<in> measurable ?P (sigma (space (M i)) (E i))"
- apply (subst measurable_iff_measure_of)
- apply (simp_all add: P_closed)
- using E_closed
- apply (force simp: subset_eq space_PiM)
- apply (force simp: subset_eq space_PiM)
- apply (auto simp: P_def intro!: sigma_sets.Basic exI[of _ i])
- apply (rule_tac x=Aa in exI)
- apply (auto simp: space_PiM)
- done
- from measurable_sets[OF this, of A] A `i \<in> I` E_closed
- have "(\<lambda>x. x i) -` A \<inter> space ?P \<in> sets ?P"
- by (simp add: E_generates)
- 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}"
- using P_closed by (auto simp: space_PiM)
- finally show "\<dots> \<in> sets ?P" .
- qed
- finally show "sets (PiM I M) \<subseteq> sigma_sets (space (PiM I M)) P"
- by (simp add: P_closed)
- show "sigma_sets (space (PiM I M)) P \<subseteq> sets (PiM I M)"
- unfolding P_def space_PiM[symmetric]
- by (intro sets.sigma_sets_subset) (auto simp: E_generates sets_Collect_single)
-qed
-
-lemma sigma_prod_algebra_sigma_eq:
- fixes E :: "'i \<Rightarrow> 'a set set" and S :: "'i \<Rightarrow> nat \<Rightarrow> 'a set"
- assumes "finite I"
- assumes S_union: "\<And>i. i \<in> I \<Longrightarrow> (\<Union>j. S i j) = space (M i)"
- and S_in_E: "\<And>i. i \<in> I \<Longrightarrow> range (S i) \<subseteq> E i"
- assumes E_closed: "\<And>i. i \<in> I \<Longrightarrow> E i \<subseteq> Pow (space (M i))"
- and E_generates: "\<And>i. i \<in> I \<Longrightarrow> sets (M i) = sigma_sets (space (M i)) (E i)"
- defines "P == { Pi\<^sub>E I F | F. \<forall>i\<in>I. F i \<in> E i }"
- shows "sets (PiM I M) = sigma_sets (space (PiM I M)) P"
-proof
- let ?P = "sigma (space (Pi\<^sub>M I M)) P"
- from `finite I`[THEN ex_bij_betw_finite_nat] guess T ..
- 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"
- by (auto simp add: bij_betw_def set_eq_iff image_iff the_inv_into_f_f)
- have P_closed: "P \<subseteq> Pow (space (Pi\<^sub>M I M))"
- using E_closed by (auto simp: space_PiM P_def subset_eq)
- then have space_P: "space ?P = (\<Pi>\<^sub>E i\<in>I. space (M i))"
- by (simp add: space_PiM)
- have "sets (PiM I M) =
- 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)}"
- using sets_PiM_single[of I M] by (simp add: space_P)
- also have "\<dots> \<subseteq> sets (sigma (space (PiM I M)) P)"
- proof (safe intro!: sets.sigma_sets_subset)
- fix i A assume "i \<in> I" and A: "A \<in> sets (M i)"
- have "(\<lambda>x. x i) \<in> measurable ?P (sigma (space (M i)) (E i))"
- proof (subst measurable_iff_measure_of)
- show "E i \<subseteq> Pow (space (M i))" using `i \<in> I` by fact
- from space_P `i \<in> I` show "(\<lambda>x. x i) \<in> space ?P \<rightarrow> space (M i)" by auto
- show "\<forall>A\<in>E i. (\<lambda>x. x i) -` A \<inter> space ?P \<in> sets ?P"
- proof
- fix A assume A: "A \<in> E i"
- 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))"
- using E_closed `i \<in> I` by (auto simp: space_P subset_eq split: split_if_asm)
- also have "\<dots> = (\<Pi>\<^sub>E j\<in>I. \<Union>n. if i = j then A else S j n)"
- by (intro PiE_cong) (simp add: S_union)
- 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))"
- using T
- apply (auto simp: PiE_iff bchoice_iff)
- apply (rule_tac x="map (\<lambda>n. f (the_inv_into I T n)) [0..<card I]" in exI)
- apply (auto simp: bij_betw_def)
- done
- also have "\<dots> \<in> sets ?P"
- proof (safe intro!: sets.countable_UN)
- fix xs show "(\<Pi>\<^sub>E j\<in>I. if i = j then A else S j (xs ! T j)) \<in> sets ?P"
- using A S_in_E
- by (simp add: P_closed)
- (auto simp: P_def subset_eq intro!: exI[of _ "\<lambda>j. if i = j then A else S j (xs ! T j)"])
- qed
- finally show "(\<lambda>x. x i) -` A \<inter> space ?P \<in> sets ?P"
- using P_closed by simp
- qed
- qed
- from measurable_sets[OF this, of A] A `i \<in> I` E_closed
- have "(\<lambda>x. x i) -` A \<inter> space ?P \<in> sets ?P"
- by (simp add: E_generates)
- 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}"
- using P_closed by (auto simp: space_PiM)
- finally show "\<dots> \<in> sets ?P" .
- qed
- finally show "sets (PiM I M) \<subseteq> sigma_sets (space (PiM I M)) P"
- by (simp add: P_closed)
- show "sigma_sets (space (PiM I M)) P \<subseteq> sets (PiM I M)"
- using `finite I`
- by (auto intro!: sets.sigma_sets_subset sets_PiM_I_finite simp: E_generates P_def)
-qed
-
lemma pair_measure_eq_distr_PiM:
fixes M1 :: "'a measure" and M2 :: "'a measure"
assumes "sigma_finite_measure M1" "sigma_finite_measure M2"
--- a/src/HOL/Probability/Measurable.thy Wed Dec 03 22:44:24 2014 +0100
+++ b/src/HOL/Probability/Measurable.thy Thu Dec 04 17:05:58 2014 +0100
@@ -377,105 +377,129 @@
qed
qed rule
+lemma measurable_pred_countable[measurable (raw)]:
+ assumes "countable X"
+ shows
+ "(\<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)"
+ "(\<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)"
+ unfolding pred_def
+ by (auto intro!: sets.sets_Collect_countable_All' sets.sets_Collect_countable_Ex' assms)
+
subsection {* Measurability for (co)inductive predicates *}
+lemma measurable_bot[measurable]: "bot \<in> measurable M (count_space UNIV)"
+ by (simp add: bot_fun_def)
+
+lemma measurable_top[measurable]: "top \<in> measurable M (count_space UNIV)"
+ by (simp add: top_fun_def)
+
+lemma measurable_SUP[measurable]:
+ fixes F :: "'i \<Rightarrow> 'a \<Rightarrow> 'b::{complete_lattice, countable}"
+ assumes [simp]: "countable I"
+ assumes [measurable]: "\<And>i. i \<in> I \<Longrightarrow> F i \<in> measurable M (count_space UNIV)"
+ shows "(\<lambda>x. SUP i:I. F i x) \<in> measurable M (count_space UNIV)"
+ unfolding measurable_count_space_eq2_countable
+proof (safe intro!: UNIV_I)
+ fix a
+ have "(\<lambda>x. SUP i:I. F i x) -` {a} \<inter> space M =
+ {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)}"
+ unfolding SUP_le_iff[symmetric] by auto
+ also have "\<dots> \<in> sets M"
+ by measurable
+ finally show "(\<lambda>x. SUP i:I. F i x) -` {a} \<inter> space M \<in> sets M" .
+qed
+
+lemma measurable_INF[measurable]:
+ fixes F :: "'i \<Rightarrow> 'a \<Rightarrow> 'b::{complete_lattice, countable}"
+ assumes [simp]: "countable I"
+ assumes [measurable]: "\<And>i. i \<in> I \<Longrightarrow> F i \<in> measurable M (count_space UNIV)"
+ shows "(\<lambda>x. INF i:I. F i x) \<in> measurable M (count_space UNIV)"
+ unfolding measurable_count_space_eq2_countable
+proof (safe intro!: UNIV_I)
+ fix a
+ have "(\<lambda>x. INF i:I. F i x) -` {a} \<inter> space M =
+ {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)}"
+ unfolding le_INF_iff[symmetric] by auto
+ also have "\<dots> \<in> sets M"
+ by measurable
+ finally show "(\<lambda>x. INF i:I. F i x) -` {a} \<inter> space M \<in> sets M" .
+qed
+
+lemma measurable_lfp_coinduct[consumes 1, case_names continuity step]:
+ fixes F :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b::{complete_lattice, countable})"
+ assumes "P M"
+ assumes F: "Order_Continuity.continuous F"
+ 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)"
+ shows "lfp F \<in> measurable M (count_space UNIV)"
+proof -
+ { fix i from `P M` have "((F ^^ i) bot) \<in> measurable M (count_space UNIV)"
+ by (induct i arbitrary: M) (auto intro!: *) }
+ then have "(\<lambda>x. SUP i. (F ^^ i) bot x) \<in> measurable M (count_space UNIV)"
+ by measurable
+ also have "(\<lambda>x. SUP i. (F ^^ i) bot x) = lfp F"
+ by (subst continuous_lfp) (auto intro: F)
+ finally show ?thesis .
+qed
+
lemma measurable_lfp:
- assumes "Order_Continuity.continuous F"
- assumes *: "\<And>A. pred M A \<Longrightarrow> pred M (F A)"
- shows "pred M (lfp F)"
+ fixes F :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b::{complete_lattice, countable})"
+ assumes F: "Order_Continuity.continuous F"
+ assumes *: "\<And>A. A \<in> measurable M (count_space UNIV) \<Longrightarrow> F A \<in> measurable M (count_space UNIV)"
+ shows "lfp F \<in> measurable M (count_space UNIV)"
+ by (coinduction rule: measurable_lfp_coinduct[OF _ F]) (blast intro: *)
+
+lemma measurable_gfp_coinduct[consumes 1, case_names continuity step]:
+ fixes F :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b::{complete_lattice, countable})"
+ assumes "P M"
+ assumes F: "Order_Continuity.down_continuous F"
+ 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)"
+ shows "gfp F \<in> measurable M (count_space UNIV)"
proof -
- { fix i have "Measurable.pred M (\<lambda>x. (F ^^ i) (\<lambda>x. False) x)"
- by (induct i) (auto intro!: *) }
- then have "Measurable.pred M (\<lambda>x. \<exists>i. (F ^^ i) (\<lambda>x. False) x)"
+ { fix i from `P M` have "((F ^^ i) top) \<in> measurable M (count_space UNIV)"
+ by (induct i arbitrary: M) (auto intro!: *) }
+ then have "(\<lambda>x. INF i. (F ^^ i) top x) \<in> measurable M (count_space UNIV)"
by measurable
- also have "(\<lambda>x. \<exists>i. (F ^^ i) (\<lambda>x. False) x) = (SUP i. (F ^^ i) bot)"
- by (auto simp add: bot_fun_def)
- also have "\<dots> = lfp F"
- by (rule continuous_lfp[symmetric]) fact
+ also have "(\<lambda>x. INF i. (F ^^ i) top x) = gfp F"
+ by (subst down_continuous_gfp) (auto intro: F)
finally show ?thesis .
qed
lemma measurable_gfp:
- assumes "Order_Continuity.down_continuous F"
- assumes *: "\<And>A. pred M A \<Longrightarrow> pred M (F A)"
- shows "pred M (gfp F)"
-proof -
- { fix i have "Measurable.pred M (\<lambda>x. (F ^^ i) (\<lambda>x. True) x)"
- by (induct i) (auto intro!: *) }
- then have "Measurable.pred M (\<lambda>x. \<forall>i. (F ^^ i) (\<lambda>x. True) x)"
- by measurable
- also have "(\<lambda>x. \<forall>i. (F ^^ i) (\<lambda>x. True) x) = (INF i. (F ^^ i) top)"
- by (auto simp add: top_fun_def)
- also have "\<dots> = gfp F"
- by (rule down_continuous_gfp[symmetric]) fact
- finally show ?thesis .
-qed
-
-lemma measurable_lfp_coinduct[consumes 1, case_names continuity step]:
- assumes "P M"
- assumes "Order_Continuity.continuous F"
- assumes *: "\<And>M A. P M \<Longrightarrow> (\<And>N. P N \<Longrightarrow> Measurable.pred N A) \<Longrightarrow> Measurable.pred M (F A)"
- shows "Measurable.pred M (lfp F)"
-proof -
- { fix i from `P M` have "Measurable.pred M (\<lambda>x. (F ^^ i) (\<lambda>x. False) x)"
- by (induct i arbitrary: M) (auto intro!: *) }
- then have "Measurable.pred M (\<lambda>x. \<exists>i. (F ^^ i) (\<lambda>x. False) x)"
- by measurable
- also have "(\<lambda>x. \<exists>i. (F ^^ i) (\<lambda>x. False) x) = (SUP i. (F ^^ i) bot)"
- by (auto simp add: bot_fun_def)
- also have "\<dots> = lfp F"
- by (rule continuous_lfp[symmetric]) fact
- finally show ?thesis .
-qed
-
-lemma measurable_gfp_coinduct[consumes 1, case_names continuity step]:
- assumes "P M"
- assumes "Order_Continuity.down_continuous F"
- assumes *: "\<And>M A. P M \<Longrightarrow> (\<And>N. P N \<Longrightarrow> Measurable.pred N A) \<Longrightarrow> Measurable.pred M (F A)"
- shows "Measurable.pred M (gfp F)"
-proof -
- { fix i from `P M` have "Measurable.pred M (\<lambda>x. (F ^^ i) (\<lambda>x. True) x)"
- by (induct i arbitrary: M) (auto intro!: *) }
- then have "Measurable.pred M (\<lambda>x. \<forall>i. (F ^^ i) (\<lambda>x. True) x)"
- by measurable
- also have "(\<lambda>x. \<forall>i. (F ^^ i) (\<lambda>x. True) x) = (INF i. (F ^^ i) top)"
- by (auto simp add: top_fun_def)
- also have "\<dots> = gfp F"
- by (rule down_continuous_gfp[symmetric]) fact
- finally show ?thesis .
-qed
+ fixes F :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b::{complete_lattice, countable})"
+ assumes F: "Order_Continuity.down_continuous F"
+ assumes *: "\<And>A. A \<in> measurable M (count_space UNIV) \<Longrightarrow> F A \<in> measurable M (count_space UNIV)"
+ shows "gfp F \<in> measurable M (count_space UNIV)"
+ by (coinduction rule: measurable_gfp_coinduct[OF _ F]) (blast intro: *)
lemma measurable_lfp2_coinduct[consumes 1, case_names continuity step]:
+ fixes F :: "('a \<Rightarrow> 'c \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'c \<Rightarrow> 'b::{complete_lattice, countable})"
assumes "P M s"
- assumes "Order_Continuity.continuous F"
- 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)"
- shows "Measurable.pred M (lfp F s)"
+ assumes F: "Order_Continuity.continuous F"
+ 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)"
+ shows "lfp F s \<in> measurable M (count_space UNIV)"
proof -
- { fix i from `P M s` have "Measurable.pred M (\<lambda>x. (F ^^ i) (\<lambda>t x. False) s x)"
+ { fix i from `P M s` have "(\<lambda>x. (F ^^ i) bot s x) \<in> measurable M (count_space UNIV)"
by (induct i arbitrary: M s) (auto intro!: *) }
- then have "Measurable.pred M (\<lambda>x. \<exists>i. (F ^^ i) (\<lambda>t x. False) s x)"
+ then have "(\<lambda>x. SUP i. (F ^^ i) bot s x) \<in> measurable M (count_space UNIV)"
by measurable
- also have "(\<lambda>x. \<exists>i. (F ^^ i) (\<lambda>t x. False) s x) = (SUP i. (F ^^ i) bot) s"
- by (auto simp add: bot_fun_def)
- also have "(SUP i. (F ^^ i) bot) = lfp F"
- by (rule continuous_lfp[symmetric]) fact
+ also have "(\<lambda>x. SUP i. (F ^^ i) bot s x) = lfp F s"
+ by (subst continuous_lfp) (auto simp: F)
finally show ?thesis .
qed
lemma measurable_gfp2_coinduct[consumes 1, case_names continuity step]:
+ fixes F :: "('a \<Rightarrow> 'c \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'c \<Rightarrow> 'b::{complete_lattice, countable})"
assumes "P M s"
- assumes "Order_Continuity.down_continuous F"
- 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)"
- shows "Measurable.pred M (gfp F s)"
+ assumes F: "Order_Continuity.down_continuous F"
+ 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)"
+ shows "gfp F s \<in> measurable M (count_space UNIV)"
proof -
- { fix i from `P M s` have "Measurable.pred M (\<lambda>x. (F ^^ i) (\<lambda>t x. True) s x)"
+ { fix i from `P M s` have "(\<lambda>x. (F ^^ i) top s x) \<in> measurable M (count_space UNIV)"
by (induct i arbitrary: M s) (auto intro!: *) }
- then have "Measurable.pred M (\<lambda>x. \<forall>i. (F ^^ i) (\<lambda>t x. True) s x)"
+ then have "(\<lambda>x. INF i. (F ^^ i) top s x) \<in> measurable M (count_space UNIV)"
by measurable
- also have "(\<lambda>x. \<forall>i. (F ^^ i) (\<lambda>t x. True) s x) = (INF i. (F ^^ i) top) s"
- by (auto simp add: top_fun_def)
- also have "(INF i. (F ^^ i) top) = gfp F"
- by (rule down_continuous_gfp[symmetric]) fact
+ also have "(\<lambda>x. INF i. (F ^^ i) top s x) = gfp F s"
+ by (subst down_continuous_gfp) (auto simp: F)
finally show ?thesis .
qed
@@ -531,14 +555,6 @@
qed (simp add: fin)
qed
-lemma measurable_pred_countable[measurable (raw)]:
- assumes "countable X"
- shows
- "(\<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)"
- "(\<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)"
- unfolding pred_def
- by (auto intro!: sets.sets_Collect_countable_All' sets.sets_Collect_countable_Ex' assms)
-
lemma measurable_THE:
fixes P :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
assumes [measurable]: "\<And>i. Measurable.pred M (P i)"
@@ -565,12 +581,6 @@
finally show "f -` X \<inter> space M \<in> sets M" .
qed simp
-lemma measurable_bot[measurable]: "Measurable.pred M bot"
- by (simp add: bot_fun_def)
-
-lemma measurable_top[measurable]: "Measurable.pred M top"
- by (simp add: top_fun_def)
-
lemma measurable_Ex1[measurable (raw)]:
assumes [simp]: "countable I" and [measurable]: "\<And>i. i \<in> I \<Longrightarrow> Measurable.pred M (P i)"
shows "Measurable.pred M (\<lambda>x. \<exists>!i\<in>I. P i x)"
--- a/src/HOL/Probability/Sigma_Algebra.thy Wed Dec 03 22:44:24 2014 +0100
+++ b/src/HOL/Probability/Sigma_Algebra.thy Thu Dec 04 17:05:58 2014 +0100
@@ -364,6 +364,9 @@
finally show ?thesis .
qed
+lemma (in sigma_algebra) countable_INT'':
+ "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"
+ by (cases "I = {}") (auto intro: countable_INT')
lemma (in sigma_algebra) countable:
assumes "\<And>a. a \<in> A \<Longrightarrow> {a} \<in> M" "countable A"
@@ -2285,6 +2288,30 @@
using measurable_space[OF f] M by auto
qed (auto intro: measurable_sets f dest: sets.sets_into_space)
+lemma Sup_sigma_sigma:
+ assumes [simp]: "M \<noteq> {}" and M: "\<And>m. m \<in> M \<Longrightarrow> m \<subseteq> Pow \<Omega>"
+ shows "(\<Squnion>\<^sub>\<sigma> m\<in>M. sigma \<Omega> m) = sigma \<Omega> (\<Union>M)"
+proof (rule measure_eqI)
+ { fix a m assume "a \<in> sigma_sets \<Omega> m" "m \<in> M"
+ then have "a \<in> sigma_sets \<Omega> (\<Union>M)"
+ by induction (auto intro: sigma_sets.intros) }
+ then show "sets (\<Squnion>\<^sub>\<sigma> m\<in>M. sigma \<Omega> m) = sets (sigma \<Omega> (\<Union>M))"
+ apply (simp add: sets_Sup_sigma space_measure_of_conv M Union_least)
+ apply (rule sigma_sets_eqI)
+ apply auto
+ done
+qed (simp add: Sup_sigma_def emeasure_sigma)
+
+lemma SUP_sigma_sigma:
+ assumes M: "M \<noteq> {}" "\<And>m. m \<in> M \<Longrightarrow> f m \<subseteq> Pow \<Omega>"
+ shows "(\<Squnion>\<^sub>\<sigma> m\<in>M. sigma \<Omega> (f m)) = sigma \<Omega> (\<Union>m\<in>M. f m)"
+proof -
+ have "Sup_sigma (sigma \<Omega> ` f ` M) = sigma \<Omega> (\<Union>(f ` M))"
+ using M by (intro Sup_sigma_sigma) auto
+ then show ?thesis
+ by (simp add: image_image)
+qed
+
subsection {* The smallest $\sigma$-algebra regarding a function *}
definition
@@ -2332,10 +2359,20 @@
finally show "g -` A \<inter> space N \<in> sets N" .
qed (insert g, auto)
+lemma vimage_algebra_sigma:
+ assumes X: "X \<subseteq> Pow \<Omega>'" and f: "f \<in> \<Omega> \<rightarrow> \<Omega>'"
+ shows "vimage_algebra \<Omega> f (sigma \<Omega>' X) = sigma \<Omega> {f -` A \<inter> \<Omega> | A. A \<in> X }" (is "?V = ?S")
+proof (rule measure_eqI)
+ have \<Omega>: "{f -` A \<inter> \<Omega> |A. A \<in> X} \<subseteq> Pow \<Omega>" by auto
+ show "sets ?V = sets ?S"
+ using sigma_sets_vimage_commute[OF f, of X]
+ by (simp add: space_measure_of_conv f sets_vimage_algebra2 \<Omega> X)
+qed (simp add: vimage_algebra_def emeasure_sigma)
+
lemma vimage_algebra_vimage_algebra_eq:
assumes *: "f \<in> X \<rightarrow> Y" "g \<in> Y \<rightarrow> space M"
shows "vimage_algebra X f (vimage_algebra Y g M) = vimage_algebra X (\<lambda>x. g (f x)) M"
- (is "?VV = ?V")
+ (is "?VV = ?V")
proof (rule measure_eqI)
have "(\<lambda>x. g (f x)) \<in> X \<rightarrow> space M" "\<And>A. A \<inter> f -` Y \<inter> X = A \<inter> X"
using * by auto