--- a/src/HOL/Probability/Borel_Space.thy Fri Nov 02 14:00:39 2012 +0100
+++ b/src/HOL/Probability/Borel_Space.thy Fri Nov 02 14:23:40 2012 +0100
@@ -30,14 +30,20 @@
lemma space_borel[simp]: "space borel = UNIV"
unfolding borel_def by auto
-lemma borel_open[simp]:
+lemma space_in_borel[measurable]: "UNIV \<in> sets borel"
+ unfolding borel_def by auto
+
+lemma pred_Collect_borel[measurable (raw)]: "Sigma_Algebra.pred borel P \<Longrightarrow> {x. P x} \<in> sets borel"
+ unfolding borel_def pred_def by auto
+
+lemma borel_open[simp, measurable (raw generic)]:
assumes "open A" shows "A \<in> sets borel"
proof -
have "A \<in> {S. open S}" unfolding mem_Collect_eq using assms .
thus ?thesis unfolding borel_def by auto
qed
-lemma borel_closed[simp]:
+lemma borel_closed[simp, measurable (raw generic)]:
assumes "closed A" shows "A \<in> sets borel"
proof -
have "space borel - (- A) \<in> sets borel"
@@ -45,23 +51,18 @@
thus ?thesis by simp
qed
-lemma borel_comp[intro,simp]: "A \<in> sets borel \<Longrightarrow> - A \<in> sets borel"
- unfolding Compl_eq_Diff_UNIV by (intro Diff) auto
+lemma borel_insert[measurable]:
+ "A \<in> sets borel \<Longrightarrow> insert x A \<in> sets (borel :: 'a::t2_space measure)"
+ unfolding insert_def by (rule Un) auto
+
+lemma borel_comp[intro, simp, measurable]: "A \<in> sets borel \<Longrightarrow> - A \<in> sets borel"
+ unfolding Compl_eq_Diff_UNIV by simp
lemma borel_measurable_vimage:
fixes f :: "'a \<Rightarrow> 'x::t2_space"
- assumes borel: "f \<in> borel_measurable M"
+ assumes borel[measurable]: "f \<in> borel_measurable M"
shows "f -` {x} \<inter> space M \<in> sets M"
-proof (cases "x \<in> f ` space M")
- case True then obtain y where "x = f y" by auto
- from closed_singleton[of "f y"]
- have "{f y} \<in> sets borel" by (rule borel_closed)
- with assms show ?thesis
- unfolding in_borel_measurable_borel `x = f y` by auto
-next
- case False hence "f -` {x} \<inter> space M = {}" by auto
- thus ?thesis by auto
-qed
+ by simp
lemma borel_measurableI:
fixes f :: "'a \<Rightarrow> 'x\<Colon>topological_space"
@@ -81,7 +82,7 @@
using closed_singleton[of x] by (rule borel_closed)
qed simp
-lemma borel_measurable_const[simp, intro]:
+lemma borel_measurable_const[simp, intro, measurable (raw)]:
"(\<lambda>x. c) \<in> borel_measurable M"
by auto
@@ -91,7 +92,7 @@
unfolding indicator_def [abs_def] using A
by (auto intro!: measurable_If_set)
-lemma borel_measurable_indicator':
+lemma borel_measurable_indicator'[measurable]:
"{x\<in>space M. x \<in> A} \<in> sets M \<Longrightarrow> indicator A \<in> borel_measurable M"
unfolding indicator_def[abs_def]
by (auto intro!: measurable_If)
@@ -119,115 +120,63 @@
shows "f \<in> borel_measurable M"
using assms unfolding measurable_def by auto
+lemma borel_measurable_continuous_on1:
+ fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
+ assumes "continuous_on UNIV f"
+ shows "f \<in> borel_measurable borel"
+ apply(rule borel_measurableI)
+ using continuous_open_preimage[OF assms] unfolding vimage_def by auto
+
section "Borel spaces on euclidean spaces"
-lemma lessThan_borel[simp, intro]:
- fixes a :: "'a\<Colon>ordered_euclidean_space"
- shows "{..< a} \<in> sets borel"
- by (blast intro: borel_open)
-
-lemma greaterThan_borel[simp, intro]:
- fixes a :: "'a\<Colon>ordered_euclidean_space"
- shows "{a <..} \<in> sets borel"
- by (blast intro: borel_open)
-
-lemma greaterThanLessThan_borel[simp, intro]:
- fixes a b :: "'a\<Colon>ordered_euclidean_space"
- shows "{a<..<b} \<in> sets borel"
- by (blast intro: borel_open)
+lemma borel_measurable_euclidean_component'[measurable]:
+ "(\<lambda>x::'a::euclidean_space. x $$ i) \<in> borel_measurable borel"
+ by (intro continuous_on_euclidean_component continuous_on_id borel_measurable_continuous_on1)
-lemma atMost_borel[simp, intro]:
- fixes a :: "'a\<Colon>ordered_euclidean_space"
- shows "{..a} \<in> sets borel"
- by (blast intro: borel_closed)
-
-lemma atLeast_borel[simp, intro]:
- fixes a :: "'a\<Colon>ordered_euclidean_space"
- shows "{a..} \<in> sets borel"
- by (blast intro: borel_closed)
-
-lemma atLeastAtMost_borel[simp, intro]:
- fixes a b :: "'a\<Colon>ordered_euclidean_space"
- shows "{a..b} \<in> sets borel"
- by (blast intro: borel_closed)
+lemma borel_measurable_euclidean_component:
+ "(f :: 'a \<Rightarrow> 'b::euclidean_space) \<in> borel_measurable M \<Longrightarrow>(\<lambda>x. f x $$ i) \<in> borel_measurable M"
+ by simp
-lemma greaterThanAtMost_borel[simp, intro]:
- fixes a b :: "'a\<Colon>ordered_euclidean_space"
- shows "{a<..b} \<in> sets borel"
- unfolding greaterThanAtMost_def by blast
-
-lemma atLeastLessThan_borel[simp, intro]:
+lemma [simp, intro, measurable]:
fixes a b :: "'a\<Colon>ordered_euclidean_space"
- shows "{a..<b} \<in> sets borel"
- unfolding atLeastLessThan_def by blast
-
-lemma hafspace_less_borel[simp, intro]:
- fixes a :: real
- shows "{x::'a::euclidean_space. a < x $$ i} \<in> sets borel"
- by (auto intro!: borel_open open_halfspace_component_gt)
+ shows lessThan_borel: "{..< a} \<in> sets borel"
+ and greaterThan_borel: "{a <..} \<in> sets borel"
+ and greaterThanLessThan_borel: "{a<..<b} \<in> sets borel"
+ and atMost_borel: "{..a} \<in> sets borel"
+ and atLeast_borel: "{a..} \<in> sets borel"
+ and atLeastAtMost_borel: "{a..b} \<in> sets borel"
+ and greaterThanAtMost_borel: "{a<..b} \<in> sets borel"
+ and atLeastLessThan_borel: "{a..<b} \<in> sets borel"
+ unfolding greaterThanAtMost_def atLeastLessThan_def
+ by (blast intro: borel_open borel_closed)+
-lemma hafspace_greater_borel[simp, intro]:
- fixes a :: real
- shows "{x::'a::euclidean_space. x $$ i < a} \<in> sets borel"
- by (auto intro!: borel_open open_halfspace_component_lt)
+lemma
+ shows hafspace_less_borel[simp, intro]: "{x::'a::euclidean_space. a < x $$ i} \<in> sets borel"
+ and hafspace_greater_borel[simp, intro]: "{x::'a::euclidean_space. x $$ i < a} \<in> sets borel"
+ and hafspace_less_eq_borel[simp, intro]: "{x::'a::euclidean_space. a \<le> x $$ i} \<in> sets borel"
+ and hafspace_greater_eq_borel[simp, intro]: "{x::'a::euclidean_space. x $$ i \<le> a} \<in> sets borel"
+ by simp_all
-lemma hafspace_less_eq_borel[simp, intro]:
- fixes a :: real
- shows "{x::'a::euclidean_space. a \<le> x $$ i} \<in> sets borel"
- by (auto intro!: borel_closed closed_halfspace_component_ge)
-
-lemma hafspace_greater_eq_borel[simp, intro]:
- fixes a :: real
- shows "{x::'a::euclidean_space. x $$ i \<le> a} \<in> sets borel"
- by (auto intro!: borel_closed closed_halfspace_component_le)
-
-lemma borel_measurable_less[simp, intro]:
+lemma borel_measurable_less[simp, intro, measurable]:
fixes f :: "'a \<Rightarrow> real"
assumes f: "f \<in> borel_measurable M"
assumes g: "g \<in> borel_measurable M"
shows "{w \<in> space M. f w < g w} \<in> sets M"
proof -
- have "{w \<in> space M. f w < g w} =
- (\<Union>r. (f -` {..< of_rat r} \<inter> space M) \<inter> (g -` {of_rat r <..} \<inter> space M))"
+ have "{w \<in> space M. f w < g w} = {x \<in> space M. \<exists>r. f x < of_rat r \<and> of_rat r < g x}"
using Rats_dense_in_real by (auto simp add: Rats_def)
- then show ?thesis using f g
- by simp (blast intro: measurable_sets)
-qed
-
-lemma borel_measurable_le[simp, intro]:
- fixes f :: "'a \<Rightarrow> real"
- assumes f: "f \<in> borel_measurable M"
- assumes g: "g \<in> borel_measurable M"
- shows "{w \<in> space M. f w \<le> g w} \<in> sets M"
-proof -
- have "{w \<in> space M. f w \<le> g w} = space M - {w \<in> space M. g w < f w}"
- by auto
- thus ?thesis using f g
- by simp blast
+ with f g show ?thesis
+ by simp
qed
-lemma borel_measurable_eq[simp, intro]:
+lemma [simp, intro]:
fixes f :: "'a \<Rightarrow> real"
- assumes f: "f \<in> borel_measurable M"
- assumes g: "g \<in> borel_measurable M"
- shows "{w \<in> space M. f w = g w} \<in> sets M"
-proof -
- have "{w \<in> space M. f w = g w} =
- {w \<in> space M. f w \<le> g w} \<inter> {w \<in> space M. g w \<le> f w}"
- by auto
- thus ?thesis using f g by auto
-qed
-
-lemma borel_measurable_neq[simp, intro]:
- fixes f :: "'a \<Rightarrow> real"
- assumes f: "f \<in> borel_measurable M"
- assumes g: "g \<in> borel_measurable M"
- shows "{w \<in> space M. f w \<noteq> g w} \<in> sets M"
-proof -
- have "{w \<in> space M. f w \<noteq> g w} = space M - {w \<in> space M. f w = g w}"
- by auto
- thus ?thesis using f g by auto
-qed
+ assumes f[measurable]: "f \<in> borel_measurable M"
+ assumes g[measurable]: "g \<in> borel_measurable M"
+ shows borel_measurable_le[measurable]: "{w \<in> space M. f w \<le> g w} \<in> sets M"
+ and borel_measurable_eq[measurable]: "{w \<in> space M. f w = g w} \<in> sets M"
+ and borel_measurable_neq: "{w \<in> space M. f w \<noteq> g w} \<in> sets M"
+ unfolding eq_iff not_less[symmetric] by measurable+
subsection "Borel space equals sigma algebras over intervals"
@@ -377,7 +326,7 @@
by (intro sigma_algebra_sigma_sets) simp_all
have *: "?set = (\<Union>n. UNIV - {x\<Colon>'a. x $$ i < a + 1 / real (Suc n)})"
proof (safe, simp_all add: not_less)
- fix x assume "a < x $$ i"
+ fix x :: 'a assume "a < x $$ i"
with reals_Archimedean[of "x $$ i - a"]
obtain n where "a + 1 / real (Suc n) < x $$ i"
by (auto simp: inverse_eq_divide field_simps)
@@ -390,7 +339,7 @@
finally show "a < x" .
qed
show "?set \<in> ?SIGMA" unfolding *
- by (auto intro!: Diff)
+ by (auto del: Diff intro!: Diff)
qed
lemma borel_eq_halfspace_less:
@@ -631,27 +580,13 @@
lemma borel_measurable_iff_ge:
"(f::'a \<Rightarrow> real) \<in> borel_measurable M = (\<forall>a. {w \<in> space M. a \<le> f w} \<in> sets M)"
- using borel_measurable_iff_halfspace_ge[where 'c=real] by simp
+ using borel_measurable_iff_halfspace_ge[where 'c=real]
+ by simp
lemma borel_measurable_iff_greater:
"(f::'a \<Rightarrow> real) \<in> borel_measurable M = (\<forall>a. {w \<in> space M. a < f w} \<in> sets M)"
using borel_measurable_iff_halfspace_greater[where 'c=real] by simp
-lemma borel_measurable_euclidean_component':
- "(\<lambda>x::'a::euclidean_space. x $$ i) \<in> borel_measurable borel"
-proof (rule borel_measurableI)
- fix S::"real set" assume "open S"
- from open_vimage_euclidean_component[OF this]
- show "(\<lambda>x. x $$ i) -` S \<inter> space borel \<in> sets borel"
- by (auto intro: borel_open)
-qed
-
-lemma borel_measurable_euclidean_component:
- fixes f :: "'a \<Rightarrow> 'b::euclidean_space"
- assumes f: "f \<in> borel_measurable M"
- shows "(\<lambda>x. f x $$ i) \<in> borel_measurable M"
- using measurable_comp[OF f borel_measurable_euclidean_component'] by (simp add: comp_def)
-
lemma borel_measurable_euclidean_space:
fixes f :: "'a \<Rightarrow> 'c::ordered_euclidean_space"
shows "f \<in> borel_measurable M \<longleftrightarrow> (\<forall>i<DIM('c). (\<lambda>x. f x $$ i) \<in> borel_measurable M)"
@@ -667,13 +602,6 @@
subsection "Borel measurable operators"
-lemma borel_measurable_continuous_on1:
- fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
- assumes "continuous_on UNIV f"
- shows "f \<in> borel_measurable borel"
- apply(rule borel_measurableI)
- using continuous_open_preimage[OF assms] unfolding vimage_def by auto
-
lemma borel_measurable_continuous_on:
fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
assumes f: "continuous_on UNIV f" and g: "g \<in> borel_measurable M"
@@ -693,7 +621,7 @@
{x\<in>A. f x \<in> S} \<union> (if c \<in> S then space borel - A else {})"
by (auto split: split_if_asm)
also have "\<dots> \<in> sets borel"
- using * `open A` by (auto simp del: space_borel intro!: Un)
+ using * `open A` by auto
finally show "?f -` S \<inter> space borel \<in> sets borel" .
qed
@@ -705,7 +633,7 @@
using measurable_comp[OF g borel_measurable_continuous_on_open'[OF cont], of c]
by (simp add: comp_def)
-lemma borel_measurable_uminus[simp, intro]:
+lemma borel_measurable_uminus[simp, intro, measurable (raw)]:
fixes g :: "'a \<Rightarrow> real"
assumes g: "g \<in> borel_measurable M"
shows "(\<lambda>x. - g x) \<in> borel_measurable M"
@@ -716,7 +644,7 @@
shows "x $$ i = (if i < DIM('a) then fst x $$ i else snd x $$ (i - DIM('a)))"
unfolding euclidean_component_def basis_prod_def inner_prod_def by auto
-lemma borel_measurable_Pair[simp, intro]:
+lemma borel_measurable_Pair[simp, intro, measurable (raw)]:
fixes f :: "'a \<Rightarrow> 'b::ordered_euclidean_space" and g :: "'a \<Rightarrow> 'c::ordered_euclidean_space"
assumes f: "f \<in> borel_measurable M"
assumes g: "g \<in> borel_measurable M"
@@ -726,7 +654,7 @@
have [simp]: "\<And>P A B C. {w. (P \<longrightarrow> A w \<and> B w) \<and> (\<not> P \<longrightarrow> A w \<and> C w)} =
{w. A w \<and> (P \<longrightarrow> B w) \<and> (\<not> P \<longrightarrow> C w)}" by auto
from i f g show "{w \<in> space M. (f w, g w) $$ i \<le> a} \<in> sets M"
- by (auto simp: euclidean_component_prod intro!: sets_Collect borel_measurable_euclidean_component)
+ by (auto simp: euclidean_component_prod)
qed
lemma continuous_on_fst: "continuous_on UNIV fst"
@@ -757,7 +685,7 @@
unfolding eq by (rule borel_measurable_continuous_on[OF H]) auto
qed
-lemma borel_measurable_add[simp, intro]:
+lemma borel_measurable_add[simp, intro, measurable (raw)]:
fixes f g :: "'a \<Rightarrow> 'c::ordered_euclidean_space"
assumes f: "f \<in> borel_measurable M"
assumes g: "g \<in> borel_measurable M"
@@ -766,7 +694,7 @@
by (rule borel_measurable_continuous_Pair)
(auto intro: continuous_on_fst continuous_on_snd continuous_on_add)
-lemma borel_measurable_setsum[simp, intro]:
+lemma borel_measurable_setsum[simp, intro, measurable (raw)]:
fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> real"
assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
shows "(\<lambda>x. \<Sum>i\<in>S. f i x) \<in> borel_measurable M"
@@ -775,14 +703,14 @@
thus ?thesis using assms by induct auto
qed simp
-lemma borel_measurable_diff[simp, intro]:
+lemma borel_measurable_diff[simp, intro, measurable (raw)]:
fixes f :: "'a \<Rightarrow> real"
assumes f: "f \<in> borel_measurable M"
assumes g: "g \<in> borel_measurable M"
shows "(\<lambda>x. f x - g x) \<in> borel_measurable M"
unfolding diff_minus using assms by fast
-lemma borel_measurable_times[simp, intro]:
+lemma borel_measurable_times[simp, intro, measurable (raw)]:
fixes f :: "'a \<Rightarrow> real"
assumes f: "f \<in> borel_measurable M"
assumes g: "g \<in> borel_measurable M"
@@ -796,7 +724,7 @@
shows "continuous_on A f \<Longrightarrow> continuous_on A g \<Longrightarrow> continuous_on A (\<lambda>x. dist (f x) (g x))"
unfolding continuous_on_eq_continuous_within by (auto simp: continuous_dist)
-lemma borel_measurable_dist[simp, intro]:
+lemma borel_measurable_dist[simp, intro, measurable (raw)]:
fixes g f :: "'a \<Rightarrow> 'b::ordered_euclidean_space"
assumes f: "f \<in> borel_measurable M"
assumes g: "g \<in> borel_measurable M"
@@ -805,6 +733,14 @@
by (rule borel_measurable_continuous_Pair)
(intro continuous_on_dist continuous_on_fst continuous_on_snd)
+lemma borel_measurable_scaleR[measurable (raw)]:
+ fixes g :: "'a \<Rightarrow> 'b::ordered_euclidean_space"
+ assumes f: "f \<in> borel_measurable M"
+ assumes g: "g \<in> borel_measurable M"
+ shows "(\<lambda>x. f x *\<^sub>R g x) \<in> borel_measurable M"
+ by (rule borel_measurable_continuous_Pair[OF f g])
+ (auto intro!: continuous_on_scaleR continuous_on_fst continuous_on_snd)
+
lemma affine_borel_measurable_vector:
fixes f :: "'a \<Rightarrow> 'x::real_normed_vector"
assumes "f \<in> borel_measurable M"
@@ -825,13 +761,15 @@
qed simp
qed
-lemma affine_borel_measurable:
- fixes g :: "'a \<Rightarrow> real"
- assumes g: "g \<in> borel_measurable M"
- shows "(\<lambda>x. a + (g x) * b) \<in> borel_measurable M"
- using affine_borel_measurable_vector[OF assms] by (simp add: mult_commute)
+lemma borel_measurable_const_scaleR[measurable (raw)]:
+ "f \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. b *\<^sub>R f x ::'a::real_normed_vector) \<in> borel_measurable M"
+ using affine_borel_measurable_vector[of f M 0 b] by simp
-lemma borel_measurable_setprod[simp, intro]:
+lemma borel_measurable_const_add[measurable (raw)]:
+ "f \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. a + f x ::'a::real_normed_vector) \<in> borel_measurable M"
+ using affine_borel_measurable_vector[of f M a 1] by simp
+
+lemma borel_measurable_setprod[simp, intro, measurable (raw)]:
fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> real"
assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
shows "(\<lambda>x. \<Prod>i\<in>S. f i x) \<in> borel_measurable M"
@@ -840,7 +778,7 @@
thus ?thesis using assms by induct auto
qed simp
-lemma borel_measurable_inverse[simp, intro]:
+lemma borel_measurable_inverse[simp, intro, measurable (raw)]:
fixes f :: "'a \<Rightarrow> real"
assumes f: "f \<in> borel_measurable M"
shows "(\<lambda>x. inverse (f x)) \<in> borel_measurable M"
@@ -853,7 +791,7 @@
done
qed
-lemma borel_measurable_divide[simp, intro]:
+lemma borel_measurable_divide[simp, intro, measurable (raw)]:
fixes f :: "'a \<Rightarrow> real"
assumes "f \<in> borel_measurable M"
and "g \<in> borel_measurable M"
@@ -861,21 +799,21 @@
unfolding field_divide_inverse
by (rule borel_measurable_inverse borel_measurable_times assms)+
-lemma borel_measurable_max[intro, simp]:
+lemma borel_measurable_max[intro, simp, measurable (raw)]:
fixes f g :: "'a \<Rightarrow> real"
assumes "f \<in> borel_measurable M"
assumes "g \<in> borel_measurable M"
shows "(\<lambda>x. max (g x) (f x)) \<in> borel_measurable M"
unfolding max_def by (auto intro!: assms measurable_If)
-lemma borel_measurable_min[intro, simp]:
+lemma borel_measurable_min[intro, simp, measurable (raw)]:
fixes f g :: "'a \<Rightarrow> real"
assumes "f \<in> borel_measurable M"
assumes "g \<in> borel_measurable M"
shows "(\<lambda>x. min (g x) (f x)) \<in> borel_measurable M"
unfolding min_def by (auto intro!: assms measurable_If)
-lemma borel_measurable_abs[simp, intro]:
+lemma borel_measurable_abs[simp, intro, measurable (raw)]:
assumes "f \<in> borel_measurable M"
shows "(\<lambda>x. \<bar>f x :: real\<bar>) \<in> borel_measurable M"
proof -
@@ -883,7 +821,7 @@
show ?thesis unfolding * using assms by auto
qed
-lemma borel_measurable_nth[simp, intro]:
+lemma borel_measurable_nth[simp, intro, measurable (raw)]:
"(\<lambda>x::real^'n. x $ i) \<in> borel_measurable borel"
using borel_measurable_euclidean_component'
unfolding nth_conv_component by auto
@@ -900,12 +838,12 @@
from this q show "continuous_on {a<..<b} q"
by (rule convex_on_continuous)
qed
- moreover have "?qX \<longleftrightarrow> (\<lambda>x. q (X x)) \<in> borel_measurable M"
+ also have "?qX \<longleftrightarrow> (\<lambda>x. q (X x)) \<in> borel_measurable M"
using X by (intro measurable_cong) auto
- ultimately show ?thesis by simp
+ finally show ?thesis .
qed
-lemma borel_measurable_ln[simp,intro]:
+lemma borel_measurable_ln[simp, intro, measurable (raw)]:
assumes f: "f \<in> borel_measurable M"
shows "(\<lambda>x. ln (f x)) \<in> borel_measurable M"
proof -
@@ -926,39 +864,55 @@
finally show ?thesis .
qed
-lemma borel_measurable_log[simp,intro]:
- "f \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. log b (f x)) \<in> borel_measurable M"
+lemma borel_measurable_log[simp, intro, measurable (raw)]:
+ "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. log (g x) (f x)) \<in> borel_measurable M"
unfolding log_def by auto
-lemma borel_measurable_real_floor:
- "(\<lambda>x::real. real \<lfloor>x\<rfloor>) \<in> borel_measurable borel"
- unfolding borel_measurable_iff_ge
-proof (intro allI)
- fix a :: real
- { fix x have "a \<le> real \<lfloor>x\<rfloor> \<longleftrightarrow> real \<lceil>a\<rceil> \<le> x"
- using le_floor_eq[of "\<lceil>a\<rceil>" x] ceiling_le_iff[of a "\<lfloor>x\<rfloor>"]
- unfolding real_eq_of_int by simp }
- then have "{w::real \<in> space borel. a \<le> real \<lfloor>w\<rfloor>} = {real \<lceil>a\<rceil>..}" by auto
- then show "{w::real \<in> space borel. a \<le> real \<lfloor>w\<rfloor>} \<in> sets borel" by auto
+lemma measurable_count_space_eq2_countable:
+ fixes f :: "'a => 'c::countable"
+ shows "f \<in> measurable M (count_space A) \<longleftrightarrow> (f \<in> space M \<rightarrow> A \<and> (\<forall>a\<in>A. f -` {a} \<inter> space M \<in> sets M))"
+proof -
+ { fix X assume "X \<subseteq> A" "f \<in> space M \<rightarrow> A"
+ then have "f -` X \<inter> space M = (\<Union>a\<in>X. f -` {a} \<inter> space M)"
+ by auto
+ moreover assume "\<And>a. a\<in>A \<Longrightarrow> f -` {a} \<inter> space M \<in> sets M"
+ ultimately have "f -` X \<inter> space M \<in> sets M"
+ using `X \<subseteq> A` by (simp add: subset_eq del: UN_simps) }
+ then show ?thesis
+ unfolding measurable_def by auto
qed
-lemma borel_measurable_real_natfloor[intro, simp]:
- assumes "f \<in> borel_measurable M"
- shows "(\<lambda>x. real (natfloor (f x))) \<in> borel_measurable M"
+lemma measurable_real_floor[measurable]:
+ "(floor :: real \<Rightarrow> int) \<in> measurable borel (count_space UNIV)"
proof -
- have "\<And>x. real (natfloor (f x)) = max 0 (real \<lfloor>f x\<rfloor>)"
- by (auto simp: max_def natfloor_def)
- with borel_measurable_max[OF measurable_comp[OF assms borel_measurable_real_floor] borel_measurable_const]
- show ?thesis by (simp add: comp_def)
+ have "\<And>a x. \<lfloor>x\<rfloor> = a \<longleftrightarrow> (real a \<le> x \<and> x < real (a + 1))"
+ by (auto intro: floor_eq2)
+ then show ?thesis
+ by (auto simp: vimage_def measurable_count_space_eq2_countable)
qed
+lemma measurable_real_natfloor[measurable]:
+ "(natfloor :: real \<Rightarrow> nat) \<in> measurable borel (count_space UNIV)"
+ by (simp add: natfloor_def[abs_def])
+
+lemma measurable_real_ceiling[measurable]:
+ "(ceiling :: real \<Rightarrow> int) \<in> measurable borel (count_space UNIV)"
+ unfolding ceiling_def[abs_def] by simp
+
+lemma borel_measurable_real_floor: "(\<lambda>x::real. real \<lfloor>x\<rfloor>) \<in> borel_measurable borel"
+ by simp
+
+lemma borel_measurable_real_natfloor[intro, simp]:
+ "f \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. real (natfloor (f x))) \<in> borel_measurable M"
+ by simp
+
subsection "Borel space on the extended reals"
-lemma borel_measurable_ereal[simp, intro]:
+lemma borel_measurable_ereal[simp, intro, measurable (raw)]:
assumes f: "f \<in> borel_measurable M" shows "(\<lambda>x. ereal (f x)) \<in> borel_measurable M"
using continuous_on_ereal f by (rule borel_measurable_continuous_on)
-lemma borel_measurable_real_of_ereal[simp, intro]:
+lemma borel_measurable_real_of_ereal[simp, intro, measurable (raw)]:
fixes f :: "'a \<Rightarrow> ereal"
assumes f: "f \<in> borel_measurable M"
shows "(\<lambda>x. real (f x)) \<in> borel_measurable M"
@@ -977,20 +931,16 @@
assumes H: "(\<lambda>x. H (ereal (real (f x)))) \<in> borel_measurable M"
shows "(\<lambda>x. H (f x)) \<in> borel_measurable M"
proof -
- let ?F = "\<lambda>x. if x \<in> f -` {\<infinity>} then H \<infinity> else if x \<in> f -` {-\<infinity>} then H (-\<infinity>) else H (ereal (real (f x)))"
+ let ?F = "\<lambda>x. if f x = \<infinity> then H \<infinity> else if f x = - \<infinity> then H (-\<infinity>) else H (ereal (real (f x)))"
{ fix x have "H (f x) = ?F x" by (cases "f x") auto }
- moreover
- have "?F \<in> borel_measurable M"
- by (intro measurable_If_set f measurable_sets[OF f] H) auto
- ultimately
- show ?thesis by simp
+ with f H show ?thesis by simp
qed
lemma
fixes f :: "'a \<Rightarrow> ereal" assumes f[simp]: "f \<in> borel_measurable M"
- shows borel_measurable_ereal_abs[intro, simp]: "(\<lambda>x. \<bar>f x\<bar>) \<in> borel_measurable M"
- and borel_measurable_ereal_inverse[simp, intro]: "(\<lambda>x. inverse (f x) :: ereal) \<in> borel_measurable M"
- and borel_measurable_uminus_ereal[intro]: "(\<lambda>x. - f x :: ereal) \<in> borel_measurable M"
+ shows borel_measurable_ereal_abs[intro, simp, measurable(raw)]: "(\<lambda>x. \<bar>f x\<bar>) \<in> borel_measurable M"
+ and borel_measurable_ereal_inverse[simp, intro, measurable(raw)]: "(\<lambda>x. inverse (f x) :: ereal) \<in> borel_measurable M"
+ and borel_measurable_uminus_ereal[intro, measurable(raw)]: "(\<lambda>x. - f x :: ereal) \<in> borel_measurable M"
by (auto simp del: abs_real_of_ereal simp: borel_measurable_ereal_cases[OF f] measurable_If)
lemma borel_measurable_uminus_eq_ereal[simp]:
@@ -999,44 +949,32 @@
assume ?l from borel_measurable_uminus_ereal[OF this] show ?r by simp
qed auto
-lemma sets_Collect_If_set:
- assumes "A \<inter> space M \<in> sets M" "{x \<in> space M. P x} \<in> sets M" "{x \<in> space M. Q x} \<in> sets M"
- shows "{x \<in> space M. if x \<in> A then P x else Q x} \<in> sets M"
-proof -
- have *: "{x \<in> space M. if x \<in> A then P x else Q x} =
- {x \<in> space M. if x \<in> A \<inter> space M then P x else Q x}" by auto
- show ?thesis unfolding * unfolding if_bool_eq_conj using assms
- by (auto intro!: sets_Collect simp: Int_def conj_commute)
-qed
-
lemma set_Collect_ereal2:
fixes f g :: "'a \<Rightarrow> ereal"
assumes f: "f \<in> borel_measurable M"
assumes g: "g \<in> borel_measurable M"
assumes H: "{x \<in> space M. H (ereal (real (f x))) (ereal (real (g x)))} \<in> sets M"
- "{x \<in> space M. H (-\<infinity>) (ereal (real (g x)))} \<in> sets M"
- "{x \<in> space M. H (\<infinity>) (ereal (real (g x)))} \<in> sets M"
- "{x \<in> space M. H (ereal (real (f x))) (-\<infinity>)} \<in> sets M"
- "{x \<in> space M. H (ereal (real (f x))) (\<infinity>)} \<in> sets M"
+ "{x \<in> space borel. H (-\<infinity>) (ereal x)} \<in> sets borel"
+ "{x \<in> space borel. H (\<infinity>) (ereal x)} \<in> sets borel"
+ "{x \<in> space borel. H (ereal x) (-\<infinity>)} \<in> sets borel"
+ "{x \<in> space borel. H (ereal x) (\<infinity>)} \<in> sets borel"
shows "{x \<in> space M. H (f x) (g x)} \<in> sets M"
proof -
- let ?G = "\<lambda>y x. if x \<in> g -` {\<infinity>} then H y \<infinity> else if x \<in> g -` {-\<infinity>} then H y (-\<infinity>) else H y (ereal (real (g x)))"
- let ?F = "\<lambda>x. if x \<in> f -` {\<infinity>} then ?G \<infinity> x else if x \<in> f -` {-\<infinity>} then ?G (-\<infinity>) x else ?G (ereal (real (f x))) x"
+ let ?G = "\<lambda>y x. if g x = \<infinity> then H y \<infinity> else if g x = -\<infinity> then H y (-\<infinity>) else H y (ereal (real (g x)))"
+ let ?F = "\<lambda>x. if f x = \<infinity> then ?G \<infinity> x else if f x = -\<infinity> then ?G (-\<infinity>) x else ?G (ereal (real (f x))) x"
{ fix x have "H (f x) (g x) = ?F x" by (cases "f x" "g x" rule: ereal2_cases) auto }
- moreover
- have "{x \<in> space M. ?F x} \<in> sets M"
- by (intro sets_Collect H measurable_sets[OF f] measurable_sets[OF g] sets_Collect_If_set) auto
- ultimately
- show ?thesis by simp
+ note * = this
+ from assms show ?thesis
+ by (subst *) (simp del: space_borel split del: split_if)
qed
lemma
fixes f g :: "'a \<Rightarrow> ereal"
assumes f: "f \<in> borel_measurable M"
assumes g: "g \<in> borel_measurable M"
- shows borel_measurable_ereal_le[intro,simp]: "{x \<in> space M. f x \<le> g x} \<in> sets M"
- and borel_measurable_ereal_less[intro,simp]: "{x \<in> space M. f x < g x} \<in> sets M"
- and borel_measurable_ereal_eq[intro,simp]: "{w \<in> space M. f w = g w} \<in> sets M"
+ shows borel_measurable_ereal_le[intro,simp,measurable(raw)]: "{x \<in> space M. f x \<le> g x} \<in> sets M"
+ and borel_measurable_ereal_less[intro,simp,measurable(raw)]: "{x \<in> space M. f x < g x} \<in> sets M"
+ and borel_measurable_ereal_eq[intro,simp,measurable(raw)]: "{w \<in> space M. f w = g w} \<in> sets M"
and borel_measurable_ereal_neq[intro,simp]: "{w \<in> space M. f w \<noteq> g w} \<in> sets M"
using f g by (auto simp: f g set_Collect_ereal2[OF f g] intro!: sets_Collect_neg)
@@ -1060,7 +998,7 @@
have "?f \<in> borel_measurable M" using * ** by (intro measurable_If) auto
also have "?f = f" by (auto simp: fun_eq_iff ereal_real)
finally show "f \<in> borel_measurable M" .
-qed (auto intro: measurable_sets borel_measurable_real_of_ereal)
+qed simp_all
lemma borel_measurable_eq_atMost_ereal:
fixes f :: "'a \<Rightarrow> ereal"
@@ -1080,7 +1018,8 @@
qed }
then have "f -` {\<infinity>} \<inter> space M = space M - (\<Union>i::nat. f -` {.. real i} \<inter> space M)"
by (auto simp: not_le)
- then show "f -` {\<infinity>} \<inter> space M \<in> sets M" using pos by (auto simp del: UN_simps intro!: Diff)
+ then show "f -` {\<infinity>} \<inter> space M \<in> sets M" using pos
+ by (auto simp del: UN_simps)
moreover
have "{-\<infinity>::ereal} = {..-\<infinity>}" by auto
then show "f -` {-\<infinity>} \<inter> space M \<in> sets M" using pos by auto
@@ -1150,14 +1089,11 @@
"(\<lambda>x. H (ereal (real (f x))) (\<infinity>)) \<in> borel_measurable M"
shows "(\<lambda>x. H (f x) (g x)) \<in> borel_measurable M"
proof -
- let ?G = "\<lambda>y x. if x \<in> g -` {\<infinity>} then H y \<infinity> else if x \<in> g -` {-\<infinity>} then H y (-\<infinity>) else H y (ereal (real (g x)))"
- let ?F = "\<lambda>x. if x \<in> f -` {\<infinity>} then ?G \<infinity> x else if x \<in> f -` {-\<infinity>} then ?G (-\<infinity>) x else ?G (ereal (real (f x))) x"
+ let ?G = "\<lambda>y x. if g x = \<infinity> then H y \<infinity> else if g x = - \<infinity> then H y (-\<infinity>) else H y (ereal (real (g x)))"
+ let ?F = "\<lambda>x. if f x = \<infinity> then ?G \<infinity> x else if f x = - \<infinity> then ?G (-\<infinity>) x else ?G (ereal (real (f x))) x"
{ fix x have "H (f x) (g x) = ?F x" by (cases "f x" "g x" rule: ereal2_cases) auto }
- moreover
- have "?F \<in> borel_measurable M"
- by (intro measurable_If_set measurable_sets[OF f] measurable_sets[OF g] H) auto
- ultimately
- show ?thesis by simp
+ note * = this
+ from assms show ?thesis unfolding * by simp
qed
lemma
@@ -1166,29 +1102,24 @@
and borel_measurable_ereal_neq_const: "{x\<in>space M. f x \<noteq> c} \<in> sets M"
using f by auto
-lemma split_sets:
- "{x\<in>space M. P x \<or> Q x} = {x\<in>space M. P x} \<union> {x\<in>space M. Q x}"
- "{x\<in>space M. P x \<and> Q x} = {x\<in>space M. P x} \<inter> {x\<in>space M. Q x}"
- by auto
-
-lemma
+lemma [intro, simp, measurable(raw)]:
fixes f :: "'a \<Rightarrow> ereal"
assumes [simp]: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
- shows borel_measurable_ereal_add[intro, simp]: "(\<lambda>x. f x + g x) \<in> borel_measurable M"
- and borel_measurable_ereal_times[intro, simp]: "(\<lambda>x. f x * g x) \<in> borel_measurable M"
- and borel_measurable_ereal_min[simp, intro]: "(\<lambda>x. min (g x) (f x)) \<in> borel_measurable M"
- and borel_measurable_ereal_max[simp, intro]: "(\<lambda>x. max (g x) (f x)) \<in> borel_measurable M"
+ shows borel_measurable_ereal_add: "(\<lambda>x. f x + g x) \<in> borel_measurable M"
+ and borel_measurable_ereal_times: "(\<lambda>x. f x * g x) \<in> borel_measurable M"
+ and borel_measurable_ereal_min: "(\<lambda>x. min (g x) (f x)) \<in> borel_measurable M"
+ and borel_measurable_ereal_max: "(\<lambda>x. max (g x) (f x)) \<in> borel_measurable M"
by (auto simp add: borel_measurable_ereal2 measurable_If min_def max_def)
-lemma
+lemma [simp, intro, measurable(raw)]:
fixes f g :: "'a \<Rightarrow> ereal"
assumes "f \<in> borel_measurable M"
assumes "g \<in> borel_measurable M"
- shows borel_measurable_ereal_diff[simp, intro]: "(\<lambda>x. f x - g x) \<in> borel_measurable M"
- and borel_measurable_ereal_divide[simp, intro]: "(\<lambda>x. f x / g x) \<in> borel_measurable M"
+ shows borel_measurable_ereal_diff: "(\<lambda>x. f x - g x) \<in> borel_measurable M"
+ and borel_measurable_ereal_divide: "(\<lambda>x. f x / g x) \<in> borel_measurable M"
unfolding minus_ereal_def divide_ereal_def using assms by auto
-lemma borel_measurable_ereal_setsum[simp, intro]:
+lemma borel_measurable_ereal_setsum[simp, intro,measurable (raw)]:
fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> ereal"
assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
shows "(\<lambda>x. \<Sum>i\<in>S. f i x) \<in> borel_measurable M"
@@ -1198,7 +1129,7 @@
by induct auto
qed simp
-lemma borel_measurable_ereal_setprod[simp, intro]:
+lemma borel_measurable_ereal_setprod[simp, intro,measurable (raw)]:
fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> ereal"
assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
shows "(\<lambda>x. \<Prod>i\<in>S. f i x) \<in> borel_measurable M"
@@ -1207,7 +1138,7 @@
thus ?thesis using assms by induct auto
qed simp
-lemma borel_measurable_SUP[simp, intro]:
+lemma borel_measurable_SUP[simp, intro,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")
@@ -1220,7 +1151,7 @@
using assms by auto
qed
-lemma borel_measurable_INF[simp, intro]:
+lemma borel_measurable_INF[simp, intro,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")
@@ -1233,11 +1164,11 @@
using assms by auto
qed
-lemma
+lemma [simp, intro, measurable (raw)]:
fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> ereal"
assumes "\<And>i. f i \<in> borel_measurable M"
- shows borel_measurable_liminf[simp, intro]: "(\<lambda>x. liminf (\<lambda>i. f i x)) \<in> borel_measurable M"
- and borel_measurable_limsup[simp, intro]: "(\<lambda>x. limsup (\<lambda>i. f i x)) \<in> borel_measurable M"
+ shows borel_measurable_liminf: "(\<lambda>x. liminf (\<lambda>i. f i x)) \<in> borel_measurable M"
+ and borel_measurable_limsup: "(\<lambda>x. limsup (\<lambda>i. f i x)) \<in> borel_measurable M"
unfolding liminf_SUPR_INFI limsup_INFI_SUPR using assms by auto
lemma borel_measurable_ereal_LIMSEQ:
@@ -1251,7 +1182,7 @@
then show ?thesis by (simp add: u cong: measurable_cong)
qed
-lemma borel_measurable_psuminf[simp, intro]:
+lemma borel_measurable_psuminf[simp, intro, measurable (raw)]:
fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> ereal"
assumes "\<And>i. f i \<in> borel_measurable M" and pos: "\<And>i x. x \<in> space M \<Longrightarrow> 0 \<le> f i x"
shows "(\<lambda>x. (\<Sum>i. f i x)) \<in> borel_measurable M"
@@ -1275,38 +1206,38 @@
ultimately show ?thesis by (simp cong: measurable_cong add: borel_measurable_ereal_iff)
qed
-lemma sets_Collect_Cauchy:
+lemma sets_Collect_Cauchy[measurable]:
fixes f :: "nat \<Rightarrow> 'a => real"
- assumes f: "\<And>i. f i \<in> borel_measurable M"
+ assumes f[measurable]: "\<And>i. f i \<in> borel_measurable M"
shows "{x\<in>space M. Cauchy (\<lambda>i. f i x)} \<in> sets M"
- unfolding Cauchy_iff2 using f by (auto intro!: sets_Collect)
+ unfolding Cauchy_iff2 using f by auto
-lemma borel_measurable_lim:
+lemma borel_measurable_lim[measurable (raw)]:
fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> real"
- assumes f: "\<And>i. f i \<in> borel_measurable M"
+ assumes f[measurable]: "\<And>i. f i \<in> borel_measurable M"
shows "(\<lambda>x. lim (\<lambda>i. f i x)) \<in> borel_measurable M"
proof -
- have *: "\<And>x. lim (\<lambda>i. f i x) =
- (if Cauchy (\<lambda>i. f i x) then lim (\<lambda>i. if Cauchy (\<lambda>i. f i x) then f i x else 0) else (THE x. False))"
+ def u' \<equiv> "\<lambda>x. lim (\<lambda>i. if Cauchy (\<lambda>i. f i x) then f i x else 0)"
+ then have *: "\<And>x. lim (\<lambda>i. f i x) = (if Cauchy (\<lambda>i. f i x) then u' x else (THE x. False))"
by (auto simp: lim_def convergent_eq_cauchy[symmetric])
- { fix x have "convergent (\<lambda>i. if Cauchy (\<lambda>i. f i x) then f i x else 0)"
+ have "u' \<in> borel_measurable M"
+ proof (rule borel_measurable_LIMSEQ)
+ fix x
+ have "convergent (\<lambda>i. if Cauchy (\<lambda>i. f i x) then f i x else 0)"
by (cases "Cauchy (\<lambda>i. f i x)")
- (auto simp add: convergent_eq_cauchy[symmetric] convergent_def) }
- note convergent = this
- show ?thesis
- unfolding *
- apply (intro measurable_If sets_Collect_Cauchy f borel_measurable_const)
- apply (rule borel_measurable_LIMSEQ)
- apply (rule convergent_LIMSEQ_iff[THEN iffD1, OF convergent])
- apply (intro measurable_If sets_Collect_Cauchy f borel_measurable_const)
- done
+ (auto simp add: convergent_eq_cauchy[symmetric] convergent_def)
+ then show "(\<lambda>i. if Cauchy (\<lambda>i. f i x) then f i x else 0) ----> u' x"
+ unfolding u'_def
+ by (rule convergent_LIMSEQ_iff[THEN iffD1])
+ qed measurable
+ then show ?thesis
+ unfolding * by measurable
qed
-lemma borel_measurable_suminf:
+lemma borel_measurable_suminf[measurable (raw)]:
fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> real"
- assumes f: "\<And>i. f i \<in> borel_measurable M"
+ assumes f[measurable]: "\<And>i. f i \<in> borel_measurable M"
shows "(\<lambda>x. suminf (\<lambda>i. f i x)) \<in> borel_measurable M"
- unfolding suminf_def sums_def[abs_def] lim_def[symmetric]
- by (simp add: f borel_measurable_lim)
+ unfolding suminf_def sums_def[abs_def] lim_def[symmetric] by simp
end
--- a/src/HOL/Probability/Sigma_Algebra.thy Fri Nov 02 14:00:39 2012 +0100
+++ b/src/HOL/Probability/Sigma_Algebra.thy Fri Nov 02 14:23:40 2012 +0100
@@ -100,7 +100,7 @@
with assms show ?thesis by auto
qed
-lemma (in semiring_of_sets) sets_Collect_finite_All:
+lemma (in semiring_of_sets) sets_Collect_finite_All':
assumes "\<And>i. i \<in> S \<Longrightarrow> {x\<in>\<Omega>. P i x} \<in> M" "finite S" "S \<noteq> {}"
shows "{x\<in>\<Omega>. \<forall>i\<in>S. P i x} \<in> M"
proof -
@@ -1209,6 +1209,15 @@
"f \<in> measurable M A \<Longrightarrow> S \<in> sets A \<Longrightarrow> f -` S \<inter> space M \<in> sets M"
unfolding measurable_def by auto
+lemma measurable_sets_Collect:
+ assumes f: "f \<in> measurable M N" and P: "{x\<in>space N. P x} \<in> sets N" shows "{x\<in>space M. P (f x)} \<in> sets M"
+proof -
+ have "f -` {x \<in> space N. P x} \<inter> space M = {x\<in>space M. P (f x)}"
+ using measurable_space[OF f] by auto
+ with measurable_sets[OF f P] show ?thesis
+ by simp
+qed
+
lemma measurable_sigma_sets:
assumes B: "sets N = sigma_sets \<Omega> A" "A \<subseteq> Pow \<Omega>"
and f: "f \<in> space M \<rightarrow> \<Omega>"
@@ -1302,6 +1311,9 @@
lemma measurable_ident[intro, simp]: "id \<in> measurable M M"
by (auto simp add: measurable_def)
+lemma measurable_ident'[intro, simp]: "(\<lambda>x. x) \<in> measurable M M"
+ by (auto simp add: measurable_def)
+
lemma measurable_comp[intro]:
fixes f :: "'a \<Rightarrow> 'b" and g :: "'b \<Rightarrow> 'c"
shows "f \<in> measurable a b \<Longrightarrow> g \<in> measurable b c \<Longrightarrow> (g o f) \<in> measurable a c"
@@ -1314,7 +1326,7 @@
"f \<in> measurable M N \<Longrightarrow> g \<in> measurable N L \<Longrightarrow> (\<lambda>x. g (f x)) \<in> measurable M L"
using measurable_comp[of f M N g L] by (simp add: comp_def)
-lemma measurable_Least:
+lemma sets_Least:
assumes meas: "\<And>i::nat. {x\<in>space M. P i x} \<in> M"
shows "(\<lambda>x. LEAST j. P j x) -` A \<inter> space M \<in> sets M"
proof -
@@ -1371,6 +1383,368 @@
measurable (measure_of \<Omega> M \<mu>) N \<subseteq> measurable (measure_of \<Omega> M' \<mu>') N"
using measure_of_subset[of M' \<Omega> M] by (auto simp add: measurable_def)
+section {* Counting space *}
+
+definition count_space :: "'a set \<Rightarrow> 'a measure" where
+ "count_space \<Omega> = measure_of \<Omega> (Pow \<Omega>) (\<lambda>A. if finite A then ereal (card A) else \<infinity>)"
+
+lemma
+ shows space_count_space[simp]: "space (count_space \<Omega>) = \<Omega>"
+ and sets_count_space[simp]: "sets (count_space \<Omega>) = Pow \<Omega>"
+ using sigma_sets_into_sp[of "Pow \<Omega>" \<Omega>]
+ by (auto simp: count_space_def)
+
+lemma measurable_count_space_eq1[simp]:
+ "f \<in> measurable (count_space A) M \<longleftrightarrow> f \<in> A \<rightarrow> space M"
+ unfolding measurable_def by simp
+
+lemma measurable_count_space_eq2:
+ assumes "finite A"
+ shows "f \<in> measurable M (count_space A) \<longleftrightarrow> (f \<in> space M \<rightarrow> A \<and> (\<forall>a\<in>A. f -` {a} \<inter> space M \<in> sets M))"
+proof -
+ { fix X assume "X \<subseteq> A" "f \<in> space M \<rightarrow> A"
+ with `finite A` have "f -` X \<inter> space M = (\<Union>a\<in>X. f -` {a} \<inter> space M)" "finite X"
+ by (auto dest: finite_subset)
+ moreover assume "\<forall>a\<in>A. f -` {a} \<inter> space M \<in> sets M"
+ ultimately have "f -` X \<inter> space M \<in> sets M"
+ using `X \<subseteq> A` by (auto intro!: finite_UN simp del: UN_simps) }
+ then show ?thesis
+ unfolding measurable_def by auto
+qed
+
+lemma measurable_compose_countable:
+ assumes f: "\<And>i::'i::countable. (\<lambda>x. f i x) \<in> measurable M N" and g: "g \<in> measurable M (count_space UNIV)"
+ shows "(\<lambda>x. f (g x) x) \<in> measurable M N"
+ unfolding measurable_def
+proof safe
+ fix x assume "x \<in> space M" then show "f (g x) x \<in> space N"
+ using f[THEN measurable_space] g[THEN measurable_space] by auto
+next
+ fix A assume A: "A \<in> sets N"
+ have "(\<lambda>x. f (g x) x) -` A \<inter> space M = (\<Union>i. (g -` {i} \<inter> space M) \<inter> (f i -` A \<inter> space M))"
+ by auto
+ also have "\<dots> \<in> sets M" using f[THEN measurable_sets, OF A] g[THEN measurable_sets]
+ by (auto intro!: countable_UN measurable_sets)
+ finally show "(\<lambda>x. f (g x) x) -` A \<inter> space M \<in> sets M" .
+qed
+
+subsection {* Measurable method *}
+
+lemma (in algebra) sets_Collect_finite_All:
+ assumes "\<And>i. i \<in> S \<Longrightarrow> {x\<in>\<Omega>. P i x} \<in> M" "finite S"
+ shows "{x\<in>\<Omega>. \<forall>i\<in>S. P i x} \<in> M"
+proof -
+ have "{x\<in>\<Omega>. \<forall>i\<in>S. P i x} = (if S = {} then \<Omega> else \<Inter>i\<in>S. {x\<in>\<Omega>. P i x})"
+ by auto
+ with assms show ?thesis by (auto intro!: sets_Collect_finite_All')
+qed
+
+abbreviation "pred M P \<equiv> P \<in> measurable M (count_space (UNIV::bool set))"
+
+lemma pred_def: "pred M P \<longleftrightarrow> {x\<in>space M. P x} \<in> sets M"
+proof
+ assume "pred M P"
+ then have "P -` {True} \<inter> space M \<in> sets M"
+ by (auto simp: measurable_count_space_eq2)
+ also have "P -` {True} \<inter> space M = {x\<in>space M. P x}" by auto
+ finally show "{x\<in>space M. P x} \<in> sets M" .
+next
+ assume P: "{x\<in>space M. P x} \<in> sets M"
+ moreover
+ { fix X
+ have "X \<in> Pow (UNIV :: bool set)" by simp
+ then have "P -` X \<inter> space M = {x\<in>space M. ((X = {True} \<longrightarrow> P x) \<and> (X = {False} \<longrightarrow> \<not> P x) \<and> X \<noteq> {})}"
+ unfolding UNIV_bool Pow_insert Pow_empty by auto
+ then have "P -` X \<inter> space M \<in> sets M"
+ by (auto intro!: sets_Collect_neg sets_Collect_imp sets_Collect_conj sets_Collect_const P) }
+ then show "pred M P"
+ by (auto simp: measurable_def)
+qed
+
+lemma pred_sets1: "{x\<in>space M. P x} \<in> sets M \<Longrightarrow> f \<in> measurable N M \<Longrightarrow> pred N (\<lambda>x. P (f x))"
+ by (rule measurable_compose[where f=f and N=M]) (auto simp: pred_def)
+
+lemma pred_sets2: "A \<in> sets N \<Longrightarrow> f \<in> measurable M N \<Longrightarrow> pred M (\<lambda>x. f x \<in> A)"
+ by (rule measurable_compose[where f=f and N=N]) (auto simp: pred_def Int_def[symmetric])
+
+lemma measurable_count_space_const:
+ "(\<lambda>x. c) \<in> measurable M (count_space UNIV)"
+ by auto
+
+lemma measurable_count_space:
+ "f \<in> measurable (count_space A) (count_space UNIV)"
+ by simp
+
+lemma measurable_compose_rev:
+ assumes f: "f \<in> measurable L N" and g: "g \<in> measurable M L"
+ shows "(\<lambda>x. f (g x)) \<in> measurable M N"
+ using measurable_compose[OF g f] .
+
+ML {*
+
+structure Measurable =
+struct
+
+datatype level = Concrete | Generic;
+
+structure Data = Generic_Data
+(
+ type T = thm list * thm list;
+ val empty = ([], []);
+ val extend = I;
+ val merge = fn ((a, b), (c, d)) => (a @ c, b @ d);
+);
+
+val debug =
+ Attrib.setup_config_bool @{binding measurable_debug} (K false)
+
+val backtrack =
+ Attrib.setup_config_int @{binding measurable_backtrack} (K 40)
+
+fun get lv = (case lv of Concrete => fst | Generic => snd) o Data.get o Context.Proof;
+fun get_all ctxt = get Concrete ctxt @ get Generic ctxt;
+
+fun update f lv = Data.map (case lv of Concrete => apfst f | Generic => apsnd f);
+fun add thms' = update (fn thms => thms @ thms');
+
+fun TRYALL' tacs = fold_rev (curry op APPEND') tacs (K no_tac);
+
+fun is_too_generic thm =
+ let
+ val concl = concl_of thm
+ val concl' = HOLogic.dest_Trueprop concl handle TERM _ => concl
+ in is_Var (head_of concl') end
+
+fun import_theorem thm = if is_too_generic thm then [] else
+ [thm] @ map_filter (try (fn th' => thm RS th'))
+ [@{thm measurable_compose_rev}, @{thm pred_sets1}, @{thm pred_sets2}, @{thm sets_into_space}];
+
+fun add_thm (raw, lv) thm = add (if raw then [thm] else import_theorem thm) lv;
+
+fun debug_tac ctxt msg f = if Config.get ctxt debug then K (print_tac (msg ())) THEN' f else f
+
+fun TAKE n f thm = Seq.take n (f thm)
+
+fun nth_hol_goal thm i =
+ HOLogic.dest_Trueprop (Logic.strip_imp_concl (strip_all_body (nth (prems_of thm) (i - 1))))
+
+fun dest_measurable_fun t =
+ (case t of
+ (Const (@{const_name "Set.member"}, _) $ f $ (Const (@{const_name "measurable"}, _) $ _ $ _)) => f
+ | _ => raise (TERM ("not a measurability predicate", [t])))
+
+fun indep (Bound i) t b = i < b orelse t <= i
+ | indep (f $ t) top bot = indep f top bot andalso indep t top bot
+ | indep (Abs (_,_,t)) top bot = indep t (top + 1) (bot + 1)
+ | indep _ _ _ = true;
+
+fun cnt_prefixes ctxt (Abs (n, T, t)) = let
+ fun is_countable t = Type.of_sort (Proof_Context.tsig_of ctxt) (t, @{sort countable})
+ fun cnt_walk (Abs (ns, T, t)) Ts =
+ map (fn (t', t'') => (Abs (ns, T, t'), t'')) (cnt_walk t (T::Ts))
+ | cnt_walk (f $ g) Ts = let
+ val n = length Ts - 1
+ in
+ map (fn (f', t) => (f' $ g, t)) (cnt_walk f Ts) @
+ map (fn (g', t) => (f $ g', t)) (cnt_walk g Ts) @
+ (if is_countable (fastype_of1 (Ts, g)) andalso loose_bvar1 (g, n)
+ andalso indep g n 0 andalso g <> Bound n
+ then [(f $ Bound (n + 1), incr_boundvars (~ n) g)]
+ else [])
+ end
+ | cnt_walk _ _ = []
+ in map (fn (t1, t2) => let
+ val T1 = fastype_of1 ([T], t2)
+ val T2 = fastype_of1 ([T], t)
+ in ([SOME (Abs (n, T1, Abs (n, T, t1))), NONE, NONE, SOME (Abs (n, T, t2))],
+ [SOME T1, SOME T, SOME T2])
+ end) (cnt_walk t [T])
+ end
+ | cnt_prefixes _ _ = []
+
+val split_fun_tac =
+ Subgoal.FOCUS (fn {context = ctxt, ...} => SUBGOAL (fn (t, i) =>
+ let
+ val f = dest_measurable_fun (HOLogic.dest_Trueprop t)
+ fun cert f = map (Option.map (f (Proof_Context.theory_of ctxt)))
+ fun inst t (ts, Ts) = Drule.instantiate' (cert ctyp_of Ts) (cert cterm_of ts) t
+ val cps = cnt_prefixes ctxt f |> map (inst @{thm measurable_compose_countable})
+ in if null cps then no_tac else debug_tac ctxt (K "split fun") (resolve_tac cps) i end
+ handle TERM _ => no_tac) 1)
+
+fun single_measurable_tac ctxt facts =
+ debug_tac ctxt (fn () => "single + " ^ Pretty.str_of (Pretty.block (map (Syntax.pretty_term ctxt o prop_of) facts)))
+ (resolve_tac ((maps (import_theorem o Simplifier.norm_hhf) facts) @ get_all ctxt)
+ APPEND' (split_fun_tac ctxt));
+
+fun is_cond_formlua n thm = if length (prems_of thm) < n then false else
+ (case nth_hol_goal thm n of
+ (Const (@{const_name "Set.member"}, _) $ _ $ (Const (@{const_name "sets"}, _) $ _)) => false
+ | (Const (@{const_name "Set.member"}, _) $ _ $ (Const (@{const_name "measurable"}, _) $ _ $ _)) => false
+ | _ => true)
+ handle TERM _ => true;
+
+fun measurable_tac' ctxt ss facts n =
+ TAKE (Config.get ctxt backtrack)
+ ((single_measurable_tac ctxt facts THEN'
+ REPEAT o (single_measurable_tac ctxt facts APPEND'
+ SOLVED' (fn n => COND (is_cond_formlua n) (debug_tac ctxt (K "simp") (asm_full_simp_tac ss) n) no_tac))) n);
+
+fun measurable_tac ctxt = measurable_tac' ctxt (simpset_of ctxt);
+
+val attr_add = Thm.declaration_attribute o add_thm;
+
+val attr : attribute context_parser =
+ Scan.lift (Scan.optional (Args.parens (Scan.optional (Args.$$$ "raw" >> K true) false --
+ Scan.optional (Args.$$$ "generic" >> K Generic) Concrete)) (false, Concrete) >> attr_add);
+
+val method : (Proof.context -> Method.method) context_parser =
+ Scan.lift (Scan.succeed (fn ctxt => METHOD (fn facts => measurable_tac ctxt facts 1)));
+
+fun simproc ss redex = let
+ val ctxt = Simplifier.the_context ss;
+ val t = HOLogic.mk_Trueprop (term_of redex);
+ fun tac {context = ctxt, ...} =
+ SOLVE (measurable_tac' ctxt ss (Simplifier.prems_of ss) 1);
+ in try (fn () => Goal.prove ctxt [] [] t tac RS @{thm Eq_TrueI}) () end;
+
+end
+
+*}
+
+attribute_setup measurable = {* Measurable.attr *} "declaration of measurability theorems"
+method_setup measurable = {* Measurable.method *} "measurability prover"
+simproc_setup measurable ("A \<in> sets M" | "f \<in> measurable M N") = {* K Measurable.simproc *}
+
+declare
+ top[measurable]
+ empty_sets[measurable (raw)]
+ Un[measurable (raw)]
+ Diff[measurable (raw)]
+
+declare
+ measurable_count_space[measurable (raw)]
+ measurable_ident[measurable (raw)]
+ measurable_ident'[measurable (raw)]
+ measurable_count_space_const[measurable (raw)]
+ measurable_const[measurable (raw)]
+ measurable_If[measurable (raw)]
+ measurable_comp[measurable (raw)]
+ measurable_sets[measurable (raw)]
+
+lemma predE[measurable (raw)]:
+ "pred M P \<Longrightarrow> {x\<in>space M. P x} \<in> sets M"
+ unfolding pred_def .
+
+lemma pred_intros_imp'[measurable (raw)]:
+ "(K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. K \<longrightarrow> P x)"
+ by (cases K) auto
+
+lemma pred_intros_conj1'[measurable (raw)]:
+ "(K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. K \<and> P x)"
+ by (cases K) auto
+
+lemma pred_intros_conj2'[measurable (raw)]:
+ "(K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. P x \<and> K)"
+ by (cases K) auto
+
+lemma pred_intros_disj1'[measurable (raw)]:
+ "(\<not> K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. K \<or> P x)"
+ by (cases K) auto
+
+lemma pred_intros_disj2'[measurable (raw)]:
+ "(\<not> K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. P x \<or> K)"
+ by (cases K) auto
+
+lemma pred_intros_logic[measurable (raw)]:
+ "pred M (\<lambda>x. x \<in> space M)"
+ "pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. \<not> P x)"
+ "pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x \<and> P x)"
+ "pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x \<longrightarrow> P x)"
+ "pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x \<or> P x)"
+ "pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x = P x)"
+ "pred M (\<lambda>x. f x \<in> UNIV)"
+ "pred M (\<lambda>x. f x \<in> {})"
+ "pred M (\<lambda>x. f x \<in> (B x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> - (B x))"
+ "pred M (\<lambda>x. f x \<in> (A x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (B x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (A x) - (B x))"
+ "pred M (\<lambda>x. f x \<in> (A x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (B x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (A x) \<inter> (B x))"
+ "pred M (\<lambda>x. f x \<in> (A x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (B x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (A x) \<union> (B x))"
+ "pred M (\<lambda>x. g x (f x) \<in> (X x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (g x) -` (X x))"
+ by (auto intro!: sets_Collect simp: iff_conv_conj_imp pred_def)
+
+lemma pred_intros_countable[measurable (raw)]:
+ fixes P :: "'a \<Rightarrow> 'i :: countable \<Rightarrow> bool"
+ shows
+ "(\<And>i. pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<forall>i. P x i)"
+ "(\<And>i. pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<exists>i. P x i)"
+ by (auto intro!: sets_Collect_countable_All sets_Collect_countable_Ex simp: pred_def)
+
+lemma pred_intros_countable_bounded[measurable (raw)]:
+ fixes X :: "'i :: countable set"
+ shows
+ "(\<And>i. i \<in> X \<Longrightarrow> pred M (\<lambda>x. x \<in> N x i)) \<Longrightarrow> pred M (\<lambda>x. x \<in> (\<Inter>i\<in>X. N x i))"
+ "(\<And>i. i \<in> X \<Longrightarrow> pred M (\<lambda>x. x \<in> N x i)) \<Longrightarrow> pred M (\<lambda>x. x \<in> (\<Union>i\<in>X. N x i))"
+ "(\<And>i. i \<in> X \<Longrightarrow> pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<forall>i\<in>X. P x i)"
+ "(\<And>i. i \<in> X \<Longrightarrow> pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<exists>i\<in>X. P x i)"
+ by (auto simp: Bex_def Ball_def)
+
+lemma pred_intros_finite[measurable (raw)]:
+ "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> pred M (\<lambda>x. x \<in> N x i)) \<Longrightarrow> pred M (\<lambda>x. x \<in> (\<Inter>i\<in>I. N x i))"
+ "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> pred M (\<lambda>x. x \<in> N x i)) \<Longrightarrow> pred M (\<lambda>x. x \<in> (\<Union>i\<in>I. N x i))"
+ "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<forall>i\<in>I. P x i)"
+ "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<exists>i\<in>I. P x i)"
+ by (auto intro!: sets_Collect_finite_Ex sets_Collect_finite_All simp: iff_conv_conj_imp pred_def)
+
+lemma countable_Un_Int[measurable (raw)]:
+ "(\<And>i :: 'i :: countable. i \<in> I \<Longrightarrow> N i \<in> sets M) \<Longrightarrow> (\<Union>i\<in>I. N i) \<in> sets M"
+ "I \<noteq> {} \<Longrightarrow> (\<And>i :: 'i :: countable. i \<in> I \<Longrightarrow> N i \<in> sets M) \<Longrightarrow> (\<Inter>i\<in>I. N i) \<in> sets M"
+ by auto
+
+declare
+ finite_UN[measurable (raw)]
+ finite_INT[measurable (raw)]
+
+lemma sets_Int_pred[measurable (raw)]:
+ assumes space: "A \<inter> B \<subseteq> space M" and [measurable]: "pred M (\<lambda>x. x \<in> A)" "pred M (\<lambda>x. x \<in> B)"
+ shows "A \<inter> B \<in> sets M"
+proof -
+ have "{x\<in>space M. x \<in> A \<inter> B} \<in> sets M" by auto
+ also have "{x\<in>space M. x \<in> A \<inter> B} = A \<inter> B"
+ using space by auto
+ finally show ?thesis .
+qed
+
+lemma [measurable (raw generic)]:
+ assumes f: "f \<in> measurable M N" and c: "{c} \<in> sets N"
+ shows pred_eq_const1: "pred M (\<lambda>x. f x = c)"
+ and pred_eq_const2: "pred M (\<lambda>x. c = f x)"
+ using measurable_sets[OF f c] by (auto simp: Int_def conj_commute eq_commute pred_def)
+
+lemma pred_le_const[measurable (raw generic)]:
+ assumes f: "f \<in> measurable M N" and c: "{.. c} \<in> sets N" shows "pred M (\<lambda>x. f x \<le> c)"
+ using measurable_sets[OF f c]
+ by (auto simp: Int_def conj_commute eq_commute pred_def)
+
+lemma pred_const_le[measurable (raw generic)]:
+ assumes f: "f \<in> measurable M N" and c: "{c ..} \<in> sets N" shows "pred M (\<lambda>x. c \<le> f x)"
+ using measurable_sets[OF f c]
+ by (auto simp: Int_def conj_commute eq_commute pred_def)
+
+lemma pred_less_const[measurable (raw generic)]:
+ assumes f: "f \<in> measurable M N" and c: "{..< c} \<in> sets N" shows "pred M (\<lambda>x. f x < c)"
+ using measurable_sets[OF f c]
+ by (auto simp: Int_def conj_commute eq_commute pred_def)
+
+lemma pred_const_less[measurable (raw generic)]:
+ assumes f: "f \<in> measurable M N" and c: "{c <..} \<in> sets N" shows "pred M (\<lambda>x. c < f x)"
+ using measurable_sets[OF f c]
+ by (auto simp: Int_def conj_commute eq_commute pred_def)
+
+declare
+ Int[measurable (raw)]
+
+hide_const (open) pred
+
subsection {* Extend measure *}
definition "extend_measure \<Omega> I G \<mu> =