(* Title: HOL/Probability/Borel_Space.thy Author: Johannes Hölzl, TU München Author: Armin Heller, TU München *) header {*Borel spaces*} theory Borel_Space imports Sigma_Algebra "~~/src/HOL/Multivariate_Analysis/Multivariate_Analysis" begin section "Generic Borel spaces" definition "borel = sigma \ space = UNIV::'a::topological_space set, sets = {S. open S}\" abbreviation "borel_measurable M \ measurable M borel" interpretation borel: sigma_algebra borel by (auto simp: borel_def intro!: sigma_algebra_sigma) lemma in_borel_measurable: "f \ borel_measurable M \ (\S \ sets (sigma \ space = UNIV, sets = {S. open S}\). f -` S \ space M \ sets M)" by (auto simp add: measurable_def borel_def) lemma in_borel_measurable_borel: "f \ borel_measurable M \ (\S \ sets borel. f -` S \ space M \ sets M)" by (auto simp add: measurable_def borel_def) lemma space_borel[simp]: "space borel = UNIV" unfolding borel_def by auto lemma borel_open[simp]: assumes "open A" shows "A \ sets borel" proof - have "A \ {S. open S}" unfolding mem_Collect_eq using assms . thus ?thesis unfolding borel_def sigma_def by (auto intro!: sigma_sets.Basic) qed lemma borel_closed[simp]: assumes "closed A" shows "A \ sets borel" proof - have "space borel - (- A) \ sets borel" using assms unfolding closed_def by (blast intro: borel_open) thus ?thesis by simp qed lemma borel_comp[intro,simp]: "A \ sets borel \ - A \ sets borel" unfolding Compl_eq_Diff_UNIV by (intro borel.Diff) auto lemma (in sigma_algebra) borel_measurable_vimage: fixes f :: "'a \ 'x::t2_space" assumes borel: "f \ borel_measurable M" shows "f -` {x} \ space M \ sets M" proof (cases "x \ f ` space M") case True then obtain y where "x = f y" by auto from closed_singleton[of "f y"] have "{f y} \ 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} \ space M = {}" by auto thus ?thesis by auto qed lemma (in sigma_algebra) borel_measurableI: fixes f :: "'a \ 'x\topological_space" assumes "\S. open S \ f -` S \ space M \ sets M" shows "f \ borel_measurable M" unfolding borel_def proof (rule measurable_sigma, simp_all) fix S :: "'x set" assume "open S" thus "f -` S \ space M \ sets M" using assms[of S] by simp qed lemma borel_singleton[simp, intro]: fixes x :: "'a::t1_space" shows "A \ sets borel \ insert x A \ sets borel" proof (rule borel.insert_in_sets) show "{x} \ sets borel" using closed_singleton[of x] by (rule borel_closed) qed simp lemma (in sigma_algebra) borel_measurable_const[simp, intro]: "(\x. c) \ borel_measurable M" by (auto intro!: measurable_const) lemma (in sigma_algebra) borel_measurable_indicator[simp, intro!]: assumes A: "A \ sets M" shows "indicator A \ borel_measurable M" unfolding indicator_def_raw using A by (auto intro!: measurable_If_set borel_measurable_const) lemma (in sigma_algebra) borel_measurable_indicator_iff: "(indicator A :: 'a \ 'x::{t1_space, zero_neq_one}) \ borel_measurable M \ A \ space M \ sets M" (is "?I \ borel_measurable M \ _") proof assume "?I \ borel_measurable M" then have "?I -` {1} \ space M \ sets M" unfolding measurable_def by auto also have "?I -` {1} \ space M = A \ space M" unfolding indicator_def_raw by auto finally show "A \ space M \ sets M" . next assume "A \ space M \ sets M" moreover have "?I \ borel_measurable M \ (indicator (A \ space M) :: 'a \ 'x) \ borel_measurable M" by (intro measurable_cong) (auto simp: indicator_def) ultimately show "?I \ borel_measurable M" by auto qed lemma (in sigma_algebra) borel_measurable_restricted: fixes f :: "'a \ ereal" assumes "A \ sets M" shows "f \ borel_measurable (restricted_space A) \ (\x. f x * indicator A x) \ borel_measurable M" (is "f \ borel_measurable ?R \ ?f \ borel_measurable M") proof - interpret R: sigma_algebra ?R by (rule restricted_sigma_algebra[OF `A \ sets M`]) have *: "f \ borel_measurable ?R \ ?f \ borel_measurable ?R" by (auto intro!: measurable_cong) show ?thesis unfolding * unfolding in_borel_measurable_borel proof (simp, safe) fix S :: "ereal set" assume "S \ sets borel" "\S\sets borel. ?f -` S \ A \ op \ A ` sets M" then have "?f -` S \ A \ op \ A ` sets M" by auto then have f: "?f -` S \ A \ sets M" using `A \ sets M` sets_into_space by fastforce show "?f -` S \ space M \ sets M" proof cases assume "0 \ S" then have "?f -` S \ space M = ?f -` S \ A \ (space M - A)" using `A \ sets M` sets_into_space by auto then show ?thesis using f `A \ sets M` by (auto intro!: Un Diff) next assume "0 \ S" then have "?f -` S \ space M = ?f -` S \ A" using `A \ sets M` sets_into_space by (auto simp: indicator_def split: split_if_asm) then show ?thesis using f by auto qed next fix S :: "ereal set" assume "S \ sets borel" "\S\sets borel. ?f -` S \ space M \ sets M" then have f: "?f -` S \ space M \ sets M" by auto then show "?f -` S \ A \ op \ A ` sets M" using `A \ sets M` sets_into_space apply (simp add: image_iff) apply (rule bexI[OF _ f]) by auto qed qed lemma (in sigma_algebra) borel_measurable_subalgebra: assumes "sets N \ sets M" "space N = space M" "f \ borel_measurable N" shows "f \ borel_measurable M" using assms unfolding measurable_def by auto section "Borel spaces on euclidean spaces" lemma lessThan_borel[simp, intro]: fixes a :: "'a\ordered_euclidean_space" shows "{..< a} \ sets borel" by (blast intro: borel_open) lemma greaterThan_borel[simp, intro]: fixes a :: "'a\ordered_euclidean_space" shows "{a <..} \ sets borel" by (blast intro: borel_open) lemma greaterThanLessThan_borel[simp, intro]: fixes a b :: "'a\ordered_euclidean_space" shows "{a<.. sets borel" by (blast intro: borel_open) lemma atMost_borel[simp, intro]: fixes a :: "'a\ordered_euclidean_space" shows "{..a} \ sets borel" by (blast intro: borel_closed) lemma atLeast_borel[simp, intro]: fixes a :: "'a\ordered_euclidean_space" shows "{a..} \ sets borel" by (blast intro: borel_closed) lemma atLeastAtMost_borel[simp, intro]: fixes a b :: "'a\ordered_euclidean_space" shows "{a..b} \ sets borel" by (blast intro: borel_closed) lemma greaterThanAtMost_borel[simp, intro]: fixes a b :: "'a\ordered_euclidean_space" shows "{a<..b} \ sets borel" unfolding greaterThanAtMost_def by blast lemma atLeastLessThan_borel[simp, intro]: fixes a b :: "'a\ordered_euclidean_space" shows "{a.. sets borel" unfolding atLeastLessThan_def by blast lemma hafspace_less_borel[simp, intro]: fixes a :: real shows "{x::'a::euclidean_space. a < x $$ i} \ sets borel" by (auto intro!: borel_open open_halfspace_component_gt) lemma hafspace_greater_borel[simp, intro]: fixes a :: real shows "{x::'a::euclidean_space. x $$ i < a} \ sets borel" by (auto intro!: borel_open open_halfspace_component_lt) lemma hafspace_less_eq_borel[simp, intro]: fixes a :: real shows "{x::'a::euclidean_space. a \ x $$ i} \ 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 \ a} \ sets borel" by (auto intro!: borel_closed closed_halfspace_component_le) lemma (in sigma_algebra) borel_measurable_less[simp, intro]: fixes f :: "'a \ real" assumes f: "f \ borel_measurable M" assumes g: "g \ borel_measurable M" shows "{w \ space M. f w < g w} \ sets M" proof - have "{w \ space M. f w < g w} = (\r. (f -` {..< of_rat r} \ space M) \ (g -` {of_rat r <..} \ space M))" 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 (in sigma_algebra) borel_measurable_le[simp, intro]: fixes f :: "'a \ real" assumes f: "f \ borel_measurable M" assumes g: "g \ borel_measurable M" shows "{w \ space M. f w \ g w} \ sets M" proof - have "{w \ space M. f w \ g w} = space M - {w \ space M. g w < f w}" by auto thus ?thesis using f g by simp blast qed lemma (in sigma_algebra) borel_measurable_eq[simp, intro]: fixes f :: "'a \ real" assumes f: "f \ borel_measurable M" assumes g: "g \ borel_measurable M" shows "{w \ space M. f w = g w} \ sets M" proof - have "{w \ space M. f w = g w} = {w \ space M. f w \ g w} \ {w \ space M. g w \ f w}" by auto thus ?thesis using f g by auto qed lemma (in sigma_algebra) borel_measurable_neq[simp, intro]: fixes f :: "'a \ real" assumes f: "f \ borel_measurable M" assumes g: "g \ borel_measurable M" shows "{w \ space M. f w \ g w} \ sets M" proof - have "{w \ space M. f w \ g w} = space M - {w \ space M. f w = g w}" by auto thus ?thesis using f g by auto qed subsection "Borel space equals sigma algebras over intervals" lemma rational_boxes: fixes x :: "'a\ordered_euclidean_space" assumes "0 < e" shows "\a b. (\i. a $$ i \ \) \ (\i. b $$ i \ \) \ x \ {a <..< b} \ {a <..< b} \ ball x e" proof - def e' \ "e / (2 * sqrt (real (DIM ('a))))" then have e: "0 < e'" using assms by (auto intro!: divide_pos_pos) have "\i. \y. y \ \ \ y < x $$ i \ x $$ i - y < e'" (is "\i. ?th i") proof fix i from Rats_dense_in_real[of "x $$ i - e'" "x $$ i"] e show "?th i" by auto qed from choice[OF this] guess a .. note a = this have "\i. \y. y \ \ \ x $$ i < y \ y - x $$ i < e'" (is "\i. ?th i") proof fix i from Rats_dense_in_real[of "x $$ i" "x $$ i + e'"] e show "?th i" by auto qed from choice[OF this] guess b .. note b = this { fix y :: 'a assume *: "Chi a < y" "y < Chi b" have "dist x y = sqrt (\i)" unfolding setL2_def[symmetric] by (rule euclidean_dist_l2) also have "\ < sqrt (\i {.. y$$i < b i" using * i eucl_less[where 'a='a] by auto moreover have "a i < x$$i" "x$$i - a i < e'" using a by auto moreover have "x$$i < b i" "b i - x$$i < e'" using b by auto ultimately have "\x$$i - y$$i\ < 2 * e'" by auto then have "dist (x $$ i) (y $$ i) < e/sqrt (real (DIM('a)))" unfolding e'_def by (auto simp: dist_real_def) then have "(dist (x $$ i) (y $$ i))\ < (e/sqrt (real (DIM('a))))\" by (rule power_strict_mono) auto then show "(dist (x $$ i) (y $$ i))\ < e\ / real DIM('a)" by (simp add: power_divide) qed auto also have "\ = e" using `0 < e` by (simp add: real_eq_of_nat DIM_positive) finally have "dist x y < e" . } with a b show ?thesis apply (rule_tac exI[of _ "Chi a"]) apply (rule_tac exI[of _ "Chi b"]) using eucl_less[where 'a='a] by auto qed lemma ex_rat_list: fixes x :: "'a\ordered_euclidean_space" assumes "\ i. x $$ i \ \" shows "\ r. length r = DIM('a) \ (\ i < DIM('a). of_rat (r ! i) = x $$ i)" proof - have "\i. \r. x $$ i = of_rat r" using assms unfolding Rats_def by blast from choice[OF this] guess r .. then show ?thesis by (auto intro!: exI[of _ "map r [0 ..< DIM('a)]"]) qed lemma open_UNION: fixes M :: "'a\ordered_euclidean_space set" assumes "open M" shows "M = UNION {(a, b) | a b. {Chi (of_rat \ op ! a) <..< Chi (of_rat \ op ! b)} \ M} (\ (a, b). {Chi (of_rat \ op ! a) <..< Chi (of_rat \ op ! b)})" (is "M = UNION ?idx ?box") proof safe fix x assume "x \ M" obtain e where e: "e > 0" "ball x e \ M" using openE[OF assms `x \ M`] by auto then obtain a b where ab: "x \ {a <..< b}" "\i. a $$ i \ \" "\i. b $$ i \ \" "{a <..< b} \ ball x e" using rational_boxes[OF e(1)] by blast then obtain p q where pq: "length p = DIM ('a)" "length q = DIM ('a)" "\ i < DIM ('a). of_rat (p ! i) = a $$ i \ of_rat (q ! i) = b $$ i" using ex_rat_list[OF ab(2)] ex_rat_list[OF ab(3)] by blast hence p: "Chi (of_rat \ op ! p) = a" using euclidean_eq[of "Chi (of_rat \ op ! p)" a] unfolding o_def by auto from pq have q: "Chi (of_rat \ op ! q) = b" using euclidean_eq[of "Chi (of_rat \ op ! q)" b] unfolding o_def by auto have "x \ ?box (p, q)" using p q ab by auto thus "x \ UNION ?idx ?box" using ab e p q exI[of _ p] exI[of _ q] by auto qed auto lemma halfspace_span_open: "sigma_sets UNIV (range (\ (a, i). {x\'a\ordered_euclidean_space. x $$ i < a})) \ sets borel" by (auto intro!: borel.sigma_sets_subset[simplified] borel_open open_halfspace_component_lt) lemma halfspace_lt_in_halfspace: "{x\'a. x $$ i < a} \ sets (sigma \space=UNIV, sets=range (\ (a, i). {x\'a\ordered_euclidean_space. x $$ i < a})\)" by (auto intro!: sigma_sets.Basic simp: sets_sigma) lemma halfspace_gt_in_halfspace: "{x\'a. a < x $$ i} \ sets (sigma \space=UNIV, sets=range (\ (a, i). {x\'a\ordered_euclidean_space. x $$ i < a})\)" (is "?set \ sets ?SIGMA") proof - interpret sigma_algebra "?SIGMA" by (intro sigma_algebra_sigma_sets) (simp_all add: sets_sigma) have *: "?set = (\n. space ?SIGMA - {x\'a. x $$ i < a + 1 / real (Suc n)})" proof (safe, simp_all add: not_less) fix x 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) then show "\n. a + 1 / real (Suc n) \ x $$ i" by (blast intro: less_imp_le) next fix x n have "a < a + 1 / real (Suc n)" by auto also assume "\ \ x" finally show "a < x" . qed show "?set \ sets ?SIGMA" unfolding * by (safe intro!: countable_UN Diff halfspace_lt_in_halfspace) qed lemma open_span_halfspace: "sets borel \ sets (sigma \space=UNIV, sets=range (\ (a, i). {x::'a::ordered_euclidean_space. x $$ i < a})\)" (is "_ \ sets ?SIGMA") proof - have "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) simp then interpret sigma_algebra ?SIGMA . { fix S :: "'a set" assume "S \ {S. open S}" then have "open S" unfolding mem_Collect_eq . from open_UNION[OF this] obtain I where *: "S = (\(a, b)\I. (\ i op ! a)::'a) $$ i < x $$ i}) \ (\ i op ! b)::'a) $$ i}))" unfolding greaterThanLessThan_def unfolding eucl_greaterThan_eq_halfspaces[where 'a='a] unfolding eucl_lessThan_eq_halfspaces[where 'a='a] by blast have "S \ sets ?SIGMA" unfolding * by (auto intro!: countable_UN Int countable_INT halfspace_lt_in_halfspace halfspace_gt_in_halfspace) } then show ?thesis unfolding borel_def by (intro sets_sigma_subset) auto qed lemma halfspace_span_halfspace_le: "sets (sigma \space=UNIV, sets=range (\ (a, i). {x\'a\ordered_euclidean_space. x $$ i < a})\) \ sets (sigma \space=UNIV, sets=range (\ (a, i). {x. x $$ i \ a})\)" (is "_ \ sets ?SIGMA") proof - have "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto then interpret sigma_algebra ?SIGMA . { fix a i have *: "{x::'a. x$$i < a} = (\n. {x. x$$i \ a - 1/real (Suc n)})" proof (safe, simp_all) fix x::'a assume *: "x$$i < a" with reals_Archimedean[of "a - x$$i"] obtain n where "x $$ i < a - 1 / (real (Suc n))" by (auto simp: field_simps inverse_eq_divide) then show "\n. x $$ i \ a - 1 / (real (Suc n))" by (blast intro: less_imp_le) next fix x::'a and n assume "x$$i \ a - 1 / real (Suc n)" also have "\ < a" by auto finally show "x$$i < a" . qed have "{x. x$$i < a} \ sets ?SIGMA" unfolding * by (safe intro!: countable_UN) (auto simp: sets_sigma intro!: sigma_sets.Basic) } then show ?thesis by (intro sets_sigma_subset) auto qed lemma halfspace_span_halfspace_ge: "sets (sigma \space=UNIV, sets=range (\ (a, i). {x\'a\ordered_euclidean_space. x $$ i < a})\) \ sets (sigma \space=UNIV, sets=range (\ (a, i). {x. a \ x $$ i})\)" (is "_ \ sets ?SIGMA") proof - have "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto then interpret sigma_algebra ?SIGMA . { fix a i have *: "{x::'a. x$$i < a} = space ?SIGMA - {x::'a. a \ x$$i}" by auto have "{x. x$$i < a} \ sets ?SIGMA" unfolding * by (safe intro!: Diff) (auto simp: sets_sigma intro!: sigma_sets.Basic) } then show ?thesis by (intro sets_sigma_subset) auto qed lemma halfspace_le_span_halfspace_gt: "sets (sigma \space=UNIV, sets=range (\ (a, i). {x\'a\ordered_euclidean_space. x $$ i \ a})\) \ sets (sigma \space=UNIV, sets=range (\ (a, i). {x. a < x $$ i})\)" (is "_ \ sets ?SIGMA") proof - have "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto then interpret sigma_algebra ?SIGMA . { fix a i have *: "{x::'a. x$$i \ a} = space ?SIGMA - {x::'a. a < x$$i}" by auto have "{x. x$$i \ a} \ sets ?SIGMA" unfolding * by (safe intro!: Diff) (auto simp: sets_sigma intro!: sigma_sets.Basic) } then show ?thesis by (intro sets_sigma_subset) auto qed lemma halfspace_le_span_atMost: "sets (sigma \space=UNIV, sets=range (\ (a, i). {x\'a\ordered_euclidean_space. x $$ i \ a})\) \ sets (sigma \space=UNIV, sets=range (\a. {..a\'a\ordered_euclidean_space})\)" (is "_ \ sets ?SIGMA") proof - have "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto then interpret sigma_algebra ?SIGMA . have "\a i. {x. x$$i \ a} \ sets ?SIGMA" proof cases fix a i assume "i < DIM('a)" then have *: "{x::'a. x$$i \ a} = (\k::nat. {.. (\\ n. if n = i then a else real k)})" proof (safe, simp_all add: eucl_le[where 'a='a] split: split_if_asm) fix x from real_arch_simple[of "Max ((\i. x$$i)`{..i. i < DIM('a) \ x$$i \ real k" by (subst (asm) Max_le_iff) auto then show "\k::nat. \ia. ia \ i \ ia < DIM('a) \ x $$ ia \ real k" by (auto intro!: exI[of _ k]) qed show "{x. x$$i \ a} \ sets ?SIGMA" unfolding * by (safe intro!: countable_UN) (auto simp: sets_sigma intro!: sigma_sets.Basic) next fix a i assume "\ i < DIM('a)" then show "{x. x$$i \ a} \ sets ?SIGMA" using top by auto qed then show ?thesis by (intro sets_sigma_subset) auto qed lemma halfspace_le_span_greaterThan: "sets (sigma \space=UNIV, sets=range (\ (a, i). {x\'a\ordered_euclidean_space. x $$ i \ a})\) \ sets (sigma \space=UNIV, sets=range (\a. {a<..})\)" (is "_ \ sets ?SIGMA") proof - have "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto then interpret sigma_algebra ?SIGMA . have "\a i. {x. x$$i \ a} \ sets ?SIGMA" proof cases fix a i assume "i < DIM('a)" have "{x::'a. x$$i \ a} = space ?SIGMA - {x::'a. a < x$$i}" by auto also have *: "{x::'a. a < x$$i} = (\k::nat. {(\\ n. if n = i then a else -real k) <..})" using `i k::nat. \ia. ia \ i \ ia < DIM('a) \ -real k < x $$ ia" by (auto intro!: exI[of _ k]) qed finally show "{x. x$$i \ a} \ sets ?SIGMA" apply (simp only:) apply (safe intro!: countable_UN Diff) apply (auto simp: sets_sigma intro!: sigma_sets.Basic) done next fix a i assume "\ i < DIM('a)" then show "{x. x$$i \ a} \ sets ?SIGMA" using top by auto qed then show ?thesis by (intro sets_sigma_subset) auto qed lemma halfspace_le_span_lessThan: "sets (sigma \space=UNIV, sets=range (\ (a, i). {x\'a\ordered_euclidean_space. a \ x $$ i})\) \ sets (sigma \space=UNIV, sets=range (\a. {..)" (is "_ \ sets ?SIGMA") proof - have "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto then interpret sigma_algebra ?SIGMA . have "\a i. {x. a \ x$$i} \ sets ?SIGMA" proof cases fix a i assume "i < DIM('a)" have "{x::'a. a \ x$$i} = space ?SIGMA - {x::'a. x$$i < a}" by auto also have *: "{x::'a. x$$i < a} = (\k::nat. {..< (\\ n. if n = i then a else real k)})" using `i k::nat. \ia. ia \ i \ ia < DIM('a) \ x $$ ia < real k" by (auto intro!: exI[of _ k]) qed finally show "{x. a \ x$$i} \ sets ?SIGMA" apply (simp only:) apply (safe intro!: countable_UN Diff) apply (auto simp: sets_sigma intro!: sigma_sets.Basic) done next fix a i assume "\ i < DIM('a)" then show "{x. a \ x$$i} \ sets ?SIGMA" using top by auto qed then show ?thesis by (intro sets_sigma_subset) auto qed lemma atMost_span_atLeastAtMost: "sets (sigma \space=UNIV, sets=range (\a. {..a\'a\ordered_euclidean_space})\) \ sets (sigma \space=UNIV, sets=range (\(a,b). {a..b})\)" (is "_ \ sets ?SIGMA") proof - have "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto then interpret sigma_algebra ?SIGMA . { fix a::'a have *: "{..a} = (\n::nat. {- real n *\<^sub>R One .. a})" proof (safe, simp_all add: eucl_le[where 'a='a]) fix x from real_arch_simple[of "Max ((\i. - x$$i)`{.. real k" by (subst (asm) Max_le_iff) (auto simp: field_simps) then have "- real k \ x$$i" by simp } then show "\n::nat. \i x $$ i" by (auto intro!: exI[of _ k]) qed have "{..a} \ sets ?SIGMA" unfolding * by (safe intro!: countable_UN) (auto simp: sets_sigma intro!: sigma_sets.Basic) } then show ?thesis by (intro sets_sigma_subset) auto qed lemma borel_eq_atMost: "borel = (sigma \space=UNIV, sets=range (\ a. {.. a::'a\ordered_euclidean_space})\)" (is "_ = ?SIGMA") proof (intro algebra.equality antisym) show "sets borel \ sets ?SIGMA" using halfspace_le_span_atMost halfspace_span_halfspace_le open_span_halfspace by auto show "sets ?SIGMA \ sets borel" by (rule borel.sets_sigma_subset) auto qed auto lemma borel_eq_atLeastAtMost: "borel = (sigma \space=UNIV, sets=range (\ (a :: 'a\ordered_euclidean_space, b). {a .. b})\)" (is "_ = ?SIGMA") proof (intro algebra.equality antisym) show "sets borel \ sets ?SIGMA" using atMost_span_atLeastAtMost halfspace_le_span_atMost halfspace_span_halfspace_le open_span_halfspace by auto show "sets ?SIGMA \ sets borel" by (rule borel.sets_sigma_subset) auto qed auto lemma borel_eq_greaterThan: "borel = (sigma \space=UNIV, sets=range (\ (a :: 'a\ordered_euclidean_space). {a <..})\)" (is "_ = ?SIGMA") proof (intro algebra.equality antisym) show "sets borel \ sets ?SIGMA" using halfspace_le_span_greaterThan halfspace_span_halfspace_le open_span_halfspace by auto show "sets ?SIGMA \ sets borel" by (rule borel.sets_sigma_subset) auto qed auto lemma borel_eq_lessThan: "borel = (sigma \space=UNIV, sets=range (\ (a :: 'a\ordered_euclidean_space). {..< a})\)" (is "_ = ?SIGMA") proof (intro algebra.equality antisym) show "sets borel \ sets ?SIGMA" using halfspace_le_span_lessThan halfspace_span_halfspace_ge open_span_halfspace by auto show "sets ?SIGMA \ sets borel" by (rule borel.sets_sigma_subset) auto qed auto lemma borel_eq_greaterThanLessThan: "borel = (sigma \space=UNIV, sets=range (\ (a, b). {a <..< (b :: 'a \ ordered_euclidean_space)})\)" (is "_ = ?SIGMA") proof (intro algebra.equality antisym) show "sets ?SIGMA \ sets borel" by (rule borel.sets_sigma_subset) auto show "sets borel \ sets ?SIGMA" proof - have "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto then interpret sigma_algebra ?SIGMA . { fix M :: "'a set" assume "M \ {S. open S}" then have "open M" by simp have "M \ sets ?SIGMA" apply (subst open_UNION[OF `open M`]) apply (safe intro!: countable_UN) apply (auto simp add: sigma_def intro!: sigma_sets.Basic) done } then show ?thesis unfolding borel_def by (intro sets_sigma_subset) auto qed qed auto lemma borel_eq_atLeastLessThan: "borel = sigma \space=UNIV, sets=range (\(a, b). {a ..< b :: real})\" (is "_ = ?S") proof (intro algebra.equality antisym) interpret sigma_algebra ?S by (rule sigma_algebra_sigma) auto show "sets borel \ sets ?S" unfolding borel_eq_lessThan proof (intro sets_sigma_subset subsetI) have move_uminus: "\x y::real. -x \ y \ -y \ x" by auto fix A :: "real set" assume "A \ sets \space = UNIV, sets = range lessThan\" then obtain x where "A = {..< x}" by auto then have "A = (\i::nat. {-real i ..< x})" by (auto simp: move_uminus real_arch_simple) then show "A \ sets ?S" by (auto simp: sets_sigma intro!: sigma_sets.intros) qed simp show "sets ?S \ sets borel" by (intro borel.sets_sigma_subset) auto qed simp_all lemma borel_eq_halfspace_le: "borel = (sigma \space=UNIV, sets=range (\ (a, i). {x::'a::ordered_euclidean_space. x$$i \ a})\)" (is "_ = ?SIGMA") proof (intro algebra.equality antisym) show "sets borel \ sets ?SIGMA" using open_span_halfspace halfspace_span_halfspace_le by auto show "sets ?SIGMA \ sets borel" by (rule borel.sets_sigma_subset) auto qed auto lemma borel_eq_halfspace_less: "borel = (sigma \space=UNIV, sets=range (\ (a, i). {x::'a::ordered_euclidean_space. x$$i < a})\)" (is "_ = ?SIGMA") proof (intro algebra.equality antisym) show "sets borel \ sets ?SIGMA" using open_span_halfspace . show "sets ?SIGMA \ sets borel" by (rule borel.sets_sigma_subset) auto qed auto lemma borel_eq_halfspace_gt: "borel = (sigma \space=UNIV, sets=range (\ (a, i). {x::'a::ordered_euclidean_space. a < x$$i})\)" (is "_ = ?SIGMA") proof (intro algebra.equality antisym) show "sets borel \ sets ?SIGMA" using halfspace_le_span_halfspace_gt open_span_halfspace halfspace_span_halfspace_le by auto show "sets ?SIGMA \ sets borel" by (rule borel.sets_sigma_subset) auto qed auto lemma borel_eq_halfspace_ge: "borel = (sigma \space=UNIV, sets=range (\ (a, i). {x::'a::ordered_euclidean_space. a \ x$$i})\)" (is "_ = ?SIGMA") proof (intro algebra.equality antisym) show "sets borel \ sets ?SIGMA" using halfspace_span_halfspace_ge open_span_halfspace by auto show "sets ?SIGMA \ sets borel" by (rule borel.sets_sigma_subset) auto qed auto lemma (in sigma_algebra) borel_measurable_halfspacesI: fixes f :: "'a \ 'c\ordered_euclidean_space" assumes "borel = (sigma \space=UNIV, sets=range F\)" and "\a i. S a i = f -` F (a,i) \ space M" and "\a i. \ i < DIM('c) \ S a i \ sets M" shows "f \ borel_measurable M = (\ia::real. S a i \ sets M)" proof safe fix a :: real and i assume i: "i < DIM('c)" and f: "f \ borel_measurable M" then show "S a i \ sets M" unfolding assms by (auto intro!: measurable_sets sigma_sets.Basic simp: assms(1) sigma_def) next assume a: "\ia. S a i \ sets M" { fix a i have "S a i \ sets M" proof cases assume "i < DIM('c)" with a show ?thesis unfolding assms(2) by simp next assume "\ i < DIM('c)" from assms(3)[OF this] show ?thesis . qed } then have "f \ measurable M (sigma \space=UNIV, sets=range F\)" by (auto intro!: measurable_sigma simp: assms(2)) then show "f \ borel_measurable M" unfolding measurable_def unfolding assms(1) by simp qed lemma (in sigma_algebra) borel_measurable_iff_halfspace_le: fixes f :: "'a \ 'c\ordered_euclidean_space" shows "f \ borel_measurable M = (\ia. {w \ space M. f w $$ i \ a} \ sets M)" by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_le]) auto lemma (in sigma_algebra) borel_measurable_iff_halfspace_less: fixes f :: "'a \ 'c\ordered_euclidean_space" shows "f \ borel_measurable M \ (\ia. {w \ space M. f w $$ i < a} \ sets M)" by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_less]) auto lemma (in sigma_algebra) borel_measurable_iff_halfspace_ge: fixes f :: "'a \ 'c\ordered_euclidean_space" shows "f \ borel_measurable M = (\ia. {w \ space M. a \ f w $$ i} \ sets M)" by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_ge]) auto lemma (in sigma_algebra) borel_measurable_iff_halfspace_greater: fixes f :: "'a \ 'c\ordered_euclidean_space" shows "f \ borel_measurable M \ (\ia. {w \ space M. a < f w $$ i} \ sets M)" by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_gt]) auto lemma (in sigma_algebra) borel_measurable_iff_le: "(f::'a \ real) \ borel_measurable M = (\a. {w \ space M. f w \ a} \ sets M)" using borel_measurable_iff_halfspace_le[where 'c=real] by simp lemma (in sigma_algebra) borel_measurable_iff_less: "(f::'a \ real) \ borel_measurable M = (\a. {w \ space M. f w < a} \ sets M)" using borel_measurable_iff_halfspace_less[where 'c=real] by simp lemma (in sigma_algebra) borel_measurable_iff_ge: "(f::'a \ real) \ borel_measurable M = (\a. {w \ space M. a \ f w} \ sets M)" using borel_measurable_iff_halfspace_ge[where 'c=real] by simp lemma (in sigma_algebra) borel_measurable_iff_greater: "(f::'a \ real) \ borel_measurable M = (\a. {w \ space M. a < f w} \ sets M)" using borel_measurable_iff_halfspace_greater[where 'c=real] by simp lemma borel_measurable_euclidean_component: "(\x::'a::euclidean_space. x $$ i) \ borel_measurable borel" unfolding borel_def[where 'a=real] proof (rule borel.measurable_sigma, simp_all) fix S::"real set" assume "open S" from open_vimage_euclidean_component[OF this] show "(\x. x $$ i) -` S \ sets borel" by (auto intro: borel_open) qed lemma (in sigma_algebra) borel_measurable_euclidean_space: fixes f :: "'a \ 'c::ordered_euclidean_space" shows "f \ borel_measurable M \ (\ix. f x $$ i) \ borel_measurable M)" proof safe fix i assume "f \ borel_measurable M" then show "(\x. f x $$ i) \ borel_measurable M" using measurable_comp[of f _ _ "\x. x $$ i", unfolded comp_def] by (auto intro: borel_measurable_euclidean_component) next assume f: "\ix. f x $$ i) \ borel_measurable M" then show "f \ borel_measurable M" unfolding borel_measurable_iff_halfspace_le by auto qed subsection "Borel measurable operators" lemma (in sigma_algebra) affine_borel_measurable_vector: fixes f :: "'a \ 'x::real_normed_vector" assumes "f \ borel_measurable M" shows "(\x. a + b *\<^sub>R f x) \ borel_measurable M" proof (rule borel_measurableI) fix S :: "'x set" assume "open S" show "(\x. a + b *\<^sub>R f x) -` S \ space M \ sets M" proof cases assume "b \ 0" with `open S` have "open ((\x. (- a + x) /\<^sub>R b) ` S)" (is "open ?S") by (auto intro!: open_affinity simp: scaleR_add_right) hence "?S \ sets borel" unfolding borel_def by (auto simp: sigma_def intro!: sigma_sets.Basic) moreover from `b \ 0` have "(\x. a + b *\<^sub>R f x) -` S = f -` ?S" apply auto by (rule_tac x="a + b *\<^sub>R f x" in image_eqI, simp_all) ultimately show ?thesis using assms unfolding in_borel_measurable_borel by auto qed simp qed lemma (in sigma_algebra) affine_borel_measurable: fixes g :: "'a \ real" assumes g: "g \ borel_measurable M" shows "(\x. a + (g x) * b) \ borel_measurable M" using affine_borel_measurable_vector[OF assms] by (simp add: mult_commute) lemma (in sigma_algebra) borel_measurable_add[simp, intro]: fixes f :: "'a \ real" assumes f: "f \ borel_measurable M" assumes g: "g \ borel_measurable M" shows "(\x. f x + g x) \ borel_measurable M" proof - have 1: "\a. {w\space M. a \ f w + g w} = {w \ space M. a + g w * -1 \ f w}" by auto have "\a. (\w. a + (g w) * -1) \ borel_measurable M" by (rule affine_borel_measurable [OF g]) then have "\a. {w \ space M. (\w. a + (g w) * -1)(w) \ f w} \ sets M" using f by auto then have "\a. {w \ space M. a \ f w + g w} \ sets M" by (simp add: 1) then show ?thesis by (simp add: borel_measurable_iff_ge) qed lemma (in sigma_algebra) borel_measurable_setsum[simp, intro]: fixes f :: "'c \ 'a \ real" assumes "\i. i \ S \ f i \ borel_measurable M" shows "(\x. \i\S. f i x) \ borel_measurable M" proof cases assume "finite S" thus ?thesis using assms by induct auto qed simp lemma (in sigma_algebra) borel_measurable_square: fixes f :: "'a \ real" assumes f: "f \ borel_measurable M" shows "(\x. (f x)^2) \ borel_measurable M" proof - { fix a have "{w \ space M. (f w)\ \ a} \ sets M" proof (cases rule: linorder_cases [of a 0]) case less hence "{w \ space M. (f w)\ \ a} = {}" by auto (metis less order_le_less_trans power2_less_0) also have "... \ sets M" by (rule empty_sets) finally show ?thesis . next case equal hence "{w \ space M. (f w)\ \ a} = {w \ space M. f w \ 0} \ {w \ space M. 0 \ f w}" by auto also have "... \ sets M" apply (insert f) apply (rule Int) apply (simp add: borel_measurable_iff_le) apply (simp add: borel_measurable_iff_ge) done finally show ?thesis . next case greater have "\x. (f x ^ 2 \ sqrt a ^ 2) = (- sqrt a \ f x & f x \ sqrt a)" by (metis abs_le_interval_iff abs_of_pos greater real_sqrt_abs real_sqrt_le_iff real_sqrt_power) hence "{w \ space M. (f w)\ \ a} = {w \ space M. -(sqrt a) \ f w} \ {w \ space M. f w \ sqrt a}" using greater by auto also have "... \ sets M" apply (insert f) apply (rule Int) apply (simp add: borel_measurable_iff_ge) apply (simp add: borel_measurable_iff_le) done finally show ?thesis . qed } thus ?thesis by (auto simp add: borel_measurable_iff_le) qed lemma times_eq_sum_squares: fixes x::real shows"x*y = ((x+y)^2)/4 - ((x-y)^ 2)/4" by (simp add: power2_eq_square ring_distribs diff_divide_distrib [symmetric]) lemma (in sigma_algebra) borel_measurable_uminus[simp, intro]: fixes g :: "'a \ real" assumes g: "g \ borel_measurable M" shows "(\x. - g x) \ borel_measurable M" proof - have "(\x. - g x) = (\x. 0 + (g x) * -1)" by simp also have "... \ borel_measurable M" by (fast intro: affine_borel_measurable g) finally show ?thesis . qed lemma (in sigma_algebra) borel_measurable_times[simp, intro]: fixes f :: "'a \ real" assumes f: "f \ borel_measurable M" assumes g: "g \ borel_measurable M" shows "(\x. f x * g x) \ borel_measurable M" proof - have 1: "(\x. 0 + (f x + g x)\ * inverse 4) \ borel_measurable M" using assms by (fast intro: affine_borel_measurable borel_measurable_square) have "(\x. -((f x + -g x) ^ 2 * inverse 4)) = (\x. 0 + ((f x + -g x) ^ 2 * inverse -4))" by (simp add: minus_divide_right) also have "... \ borel_measurable M" using f g by (fast intro: affine_borel_measurable borel_measurable_square f g) finally have 2: "(\x. -((f x + -g x) ^ 2 * inverse 4)) \ borel_measurable M" . show ?thesis apply (simp add: times_eq_sum_squares diff_minus) using 1 2 by simp qed lemma (in sigma_algebra) borel_measurable_setprod[simp, intro]: fixes f :: "'c \ 'a \ real" assumes "\i. i \ S \ f i \ borel_measurable M" shows "(\x. \i\S. f i x) \ borel_measurable M" proof cases assume "finite S" thus ?thesis using assms by induct auto qed simp lemma (in sigma_algebra) borel_measurable_diff[simp, intro]: fixes f :: "'a \ real" assumes f: "f \ borel_measurable M" assumes g: "g \ borel_measurable M" shows "(\x. f x - g x) \ borel_measurable M" unfolding diff_minus using assms by fast lemma (in sigma_algebra) borel_measurable_inverse[simp, intro]: fixes f :: "'a \ real" assumes "f \ borel_measurable M" shows "(\x. inverse (f x)) \ borel_measurable M" unfolding borel_measurable_iff_ge unfolding inverse_eq_divide proof safe fix a :: real have *: "{w \ space M. a \ 1 / f w} = ({w \ space M. 0 < f w} \ {w \ space M. a * f w \ 1}) \ ({w \ space M. f w < 0} \ {w \ space M. 1 \ a * f w}) \ ({w \ space M. f w = 0} \ {w \ space M. a \ 0})" by (auto simp: le_divide_eq) show "{w \ space M. a \ 1 / f w} \ sets M" using assms unfolding * by (auto intro!: Int Un) qed lemma (in sigma_algebra) borel_measurable_divide[simp, intro]: fixes f :: "'a \ real" assumes "f \ borel_measurable M" and "g \ borel_measurable M" shows "(\x. f x / g x) \ borel_measurable M" unfolding field_divide_inverse by (rule borel_measurable_inverse borel_measurable_times assms)+ lemma (in sigma_algebra) borel_measurable_max[intro, simp]: fixes f g :: "'a \ real" assumes "f \ borel_measurable M" assumes "g \ borel_measurable M" shows "(\x. max (g x) (f x)) \ borel_measurable M" unfolding borel_measurable_iff_le proof safe fix a have "{x \ space M. max (g x) (f x) \ a} = {x \ space M. g x \ a} \ {x \ space M. f x \ a}" by auto thus "{x \ space M. max (g x) (f x) \ a} \ sets M" using assms unfolding borel_measurable_iff_le by (auto intro!: Int) qed lemma (in sigma_algebra) borel_measurable_min[intro, simp]: fixes f g :: "'a \ real" assumes "f \ borel_measurable M" assumes "g \ borel_measurable M" shows "(\x. min (g x) (f x)) \ borel_measurable M" unfolding borel_measurable_iff_ge proof safe fix a have "{x \ space M. a \ min (g x) (f x)} = {x \ space M. a \ g x} \ {x \ space M. a \ f x}" by auto thus "{x \ space M. a \ min (g x) (f x)} \ sets M" using assms unfolding borel_measurable_iff_ge by (auto intro!: Int) qed lemma (in sigma_algebra) borel_measurable_abs[simp, intro]: assumes "f \ borel_measurable M" shows "(\x. \f x :: real\) \ borel_measurable M" proof - have *: "\x. \f x\ = max 0 (f x) + max 0 (- f x)" by (simp add: max_def) show ?thesis unfolding * using assms by auto qed lemma borel_measurable_nth[simp, intro]: "(\x::real^'n. x $ i) \ borel_measurable borel" using borel_measurable_euclidean_component unfolding nth_conv_component by auto lemma borel_measurable_continuous_on1: fixes f :: "'a::topological_space \ 'b::t1_space" assumes "continuous_on UNIV f" shows "f \ borel_measurable borel" apply(rule borel.borel_measurableI) using continuous_open_preimage[OF assms] unfolding vimage_def by auto lemma borel_measurable_continuous_on: fixes f :: "'a::topological_space \ 'b::t1_space" assumes cont: "continuous_on A f" "open A" shows "(\x. if x \ A then f x else c) \ borel_measurable borel" (is "?f \ _") proof (rule borel.borel_measurableI) fix S :: "'b set" assume "open S" then have "open {x\A. f x \ S}" by (intro continuous_open_preimage[OF cont]) auto then have *: "{x\A. f x \ S} \ sets borel" by auto have "?f -` S \ space borel = {x\A. f x \ S} \ (if c \ S then space borel - A else {})" by (auto split: split_if_asm) also have "\ \ sets borel" using * `open A` by (auto simp del: space_borel intro!: borel.Un) finally show "?f -` S \ space borel \ sets borel" . qed lemma (in sigma_algebra) convex_measurable: fixes a b :: real assumes X: "X \ borel_measurable M" "X ` space M \ { a <..< b}" assumes q: "convex_on { a <..< b} q" shows "q \ X \ borel_measurable M" proof - have "(\x. if x \ {a <..< b} then q x else 0) \ borel_measurable borel" proof (rule borel_measurable_continuous_on) show "open {a<..x. if x \ {a <..< b} then q x else 0) \ X \ borel_measurable M" (is ?qX) using X by (intro measurable_comp) auto moreover have "?qX \ q \ X \ borel_measurable M" using X by (intro measurable_cong) auto ultimately show ?thesis by simp qed lemma borel_measurable_borel_log: assumes "1 < b" shows "log b \ borel_measurable borel" proof - { fix x :: real assume x: "x \ 0" { fix x::real assume "x \ 0" then have "\u. exp u = x \ False" by auto } from this[of x] x this[of 0] have "log b 0 = log b x" by (auto simp: ln_def log_def) } note log_imp = this have "(\x. if x \ {0<..} then log b x else log b 0) \ borel_measurable borel" proof (rule borel_measurable_continuous_on) show "continuous_on {0<..} (log b)" by (auto intro!: continuous_at_imp_continuous_on DERIV_log DERIV_isCont simp: continuous_isCont[symmetric]) show "open ({0<..}::real set)" by auto qed also have "(\x. if x \ {0<..} then log b x else log b 0) = log b" by (simp add: fun_eq_iff not_less log_imp) finally show ?thesis . qed lemma (in sigma_algebra) borel_measurable_log[simp,intro]: assumes f: "f \ borel_measurable M" and "1 < b" shows "(\x. log b (f x)) \ borel_measurable M" using measurable_comp[OF f borel_measurable_borel_log[OF `1 < b`]] by (simp add: comp_def) subsection "Borel space on the extended reals" lemma borel_measurable_ereal_borel: "ereal \ borel_measurable borel" unfolding borel_def[where 'a=ereal] proof (rule borel.measurable_sigma) fix X :: "ereal set" assume "X \ sets \space = UNIV, sets = {S. open S} \" then have "open X" by simp then have "open (ereal -` X \ space borel)" by (simp add: open_ereal_vimage) then show "ereal -` X \ space borel \ sets borel" by auto qed auto lemma (in sigma_algebra) borel_measurable_ereal[simp, intro]: assumes f: "f \ borel_measurable M" shows "(\x. ereal (f x)) \ borel_measurable M" using measurable_comp[OF f borel_measurable_ereal_borel] unfolding comp_def . lemma borel_measurable_real_of_ereal_borel: "(real :: ereal \ real) \ borel_measurable borel" unfolding borel_def[where 'a=real] proof (rule borel.measurable_sigma) fix B :: "real set" assume "B \ sets \space = UNIV, sets = {S. open S} \" then have "open B" by simp have *: "ereal -` real -` (B - {0}) = B - {0}" by auto have open_real: "open (real -` (B - {0}) :: ereal set)" unfolding open_ereal_def * using `open B` by auto show "(real -` B \ space borel :: ereal set) \ sets borel" proof cases assume "0 \ B" then have *: "real -` B = real -` (B - {0}) \ {-\, \, 0::ereal}" by (auto simp add: real_of_ereal_eq_0) then show "(real -` B :: ereal set) \ space borel \ sets borel" using open_real by auto next assume "0 \ B" then have *: "(real -` B :: ereal set) = real -` (B - {0})" by (auto simp add: real_of_ereal_eq_0) then show "(real -` B :: ereal set) \ space borel \ sets borel" using open_real by auto qed qed auto lemma (in sigma_algebra) borel_measurable_real_of_ereal[simp, intro]: assumes f: "f \ borel_measurable M" shows "(\x. real (f x :: ereal)) \ borel_measurable M" using measurable_comp[OF f borel_measurable_real_of_ereal_borel] unfolding comp_def . lemma (in sigma_algebra) borel_measurable_ereal_iff: shows "(\x. ereal (f x)) \ borel_measurable M \ f \ borel_measurable M" proof assume "(\x. ereal (f x)) \ borel_measurable M" from borel_measurable_real_of_ereal[OF this] show "f \ borel_measurable M" by auto qed auto lemma (in sigma_algebra) borel_measurable_ereal_iff_real: fixes f :: "'a \ ereal" shows "f \ borel_measurable M \ ((\x. real (f x)) \ borel_measurable M \ f -` {\} \ space M \ sets M \ f -` {-\} \ space M \ sets M)" proof safe assume *: "(\x. real (f x)) \ borel_measurable M" "f -` {\} \ space M \ sets M" "f -` {-\} \ space M \ sets M" have "f -` {\} \ space M = {x\space M. f x = \}" "f -` {-\} \ space M = {x\space M. f x = -\}" by auto with * have **: "{x\space M. f x = \} \ sets M" "{x\space M. f x = -\} \ sets M" by simp_all let ?f = "\x. if f x = \ then \ else if f x = -\ then -\ else ereal (real (f x))" have "?f \ borel_measurable M" using * ** by (intro measurable_If) auto also have "?f = f" by (auto simp: fun_eq_iff ereal_real) finally show "f \ borel_measurable M" . qed (auto intro: measurable_sets borel_measurable_real_of_ereal) lemma (in sigma_algebra) less_eq_ge_measurable: fixes f :: "'a \ 'c::linorder" shows "f -` {a <..} \ space M \ sets M \ f -` {..a} \ space M \ sets M" proof assume "f -` {a <..} \ space M \ sets M" moreover have "f -` {..a} \ space M = space M - f -` {a <..} \ space M" by auto ultimately show "f -` {..a} \ space M \ sets M" by auto next assume "f -` {..a} \ space M \ sets M" moreover have "f -` {a <..} \ space M = space M - f -` {..a} \ space M" by auto ultimately show "f -` {a <..} \ space M \ sets M" by auto qed lemma (in sigma_algebra) greater_eq_le_measurable: fixes f :: "'a \ 'c::linorder" shows "f -` {..< a} \ space M \ sets M \ f -` {a ..} \ space M \ sets M" proof assume "f -` {a ..} \ space M \ sets M" moreover have "f -` {..< a} \ space M = space M - f -` {a ..} \ space M" by auto ultimately show "f -` {..< a} \ space M \ sets M" by auto next assume "f -` {..< a} \ space M \ sets M" moreover have "f -` {a ..} \ space M = space M - f -` {..< a} \ space M" by auto ultimately show "f -` {a ..} \ space M \ sets M" by auto qed lemma (in sigma_algebra) borel_measurable_uminus_borel_ereal: "(uminus :: ereal \ ereal) \ borel_measurable borel" proof (subst borel_def, rule borel.measurable_sigma) fix X :: "ereal set" assume "X \ sets \space = UNIV, sets = {S. open S}\" then have "open X" by simp have "uminus -` X = uminus ` X" by (force simp: image_iff) then have "open (uminus -` X)" using `open X` ereal_open_uminus by auto then show "uminus -` X \ space borel \ sets borel" by auto qed auto lemma (in sigma_algebra) borel_measurable_uminus_ereal[intro]: assumes "f \ borel_measurable M" shows "(\x. - f x :: ereal) \ borel_measurable M" using measurable_comp[OF assms borel_measurable_uminus_borel_ereal] by (simp add: comp_def) lemma (in sigma_algebra) borel_measurable_uminus_eq_ereal[simp]: "(\x. - f x :: ereal) \ borel_measurable M \ f \ borel_measurable M" (is "?l = ?r") proof assume ?l from borel_measurable_uminus_ereal[OF this] show ?r by simp qed auto lemma (in sigma_algebra) borel_measurable_eq_atMost_ereal: fixes f :: "'a \ ereal" shows "f \ borel_measurable M \ (\a. f -` {..a} \ space M \ sets M)" proof (intro iffI allI) assume pos[rule_format]: "\a. f -` {..a} \ space M \ sets M" show "f \ borel_measurable M" unfolding borel_measurable_ereal_iff_real borel_measurable_iff_le proof (intro conjI allI) fix a :: real { fix x :: ereal assume *: "\i::nat. real i < x" have "x = \" proof (rule ereal_top) fix B from reals_Archimedean2[of B] guess n .. then have "ereal B < real n" by auto with * show "B \ x" by (metis less_trans less_imp_le) qed } then have "f -` {\} \ space M = space M - (\i::nat. f -` {.. real i} \ space M)" by (auto simp: not_le) then show "f -` {\} \ space M \ sets M" using pos by (auto simp del: UN_simps intro!: Diff) moreover have "{-\::ereal} = {..-\}" by auto then show "f -` {-\} \ space M \ sets M" using pos by auto moreover have "{x\space M. f x \ ereal a} \ sets M" using pos[of "ereal a"] by (simp add: vimage_def Int_def conj_commute) moreover have "{w \ space M. real (f w) \ a} = (if a < 0 then {w \ space M. f w \ ereal a} - f -` {-\} \ space M else {w \ space M. f w \ ereal a} \ (f -` {\} \ space M) \ (f -` {-\} \ space M))" (is "?l = ?r") proof (intro set_eqI) fix x show "x \ ?l \ x \ ?r" by (cases "f x") auto qed ultimately show "{w \ space M. real (f w) \ a} \ sets M" by auto qed qed (simp add: measurable_sets) lemma (in sigma_algebra) borel_measurable_eq_atLeast_ereal: "(f::'a \ ereal) \ borel_measurable M \ (\a. f -` {a..} \ space M \ sets M)" proof assume pos: "\a. f -` {a..} \ space M \ sets M" moreover have "\a. (\x. - f x) -` {..a} = f -` {-a ..}" by (auto simp: ereal_uminus_le_reorder) ultimately have "(\x. - f x) \ borel_measurable M" unfolding borel_measurable_eq_atMost_ereal by auto then show "f \ borel_measurable M" by simp qed (simp add: measurable_sets) lemma (in sigma_algebra) borel_measurable_ereal_iff_less: "(f::'a \ ereal) \ borel_measurable M \ (\a. f -` {..< a} \ space M \ sets M)" unfolding borel_measurable_eq_atLeast_ereal greater_eq_le_measurable .. lemma (in sigma_algebra) borel_measurable_ereal_iff_ge: "(f::'a \ ereal) \ borel_measurable M \ (\a. f -` {a <..} \ space M \ sets M)" unfolding borel_measurable_eq_atMost_ereal less_eq_ge_measurable .. lemma (in sigma_algebra) borel_measurable_ereal_eq_const: fixes f :: "'a \ ereal" assumes "f \ borel_measurable M" shows "{x\space M. f x = c} \ sets M" proof - have "{x\space M. f x = c} = (f -` {c} \ space M)" by auto then show ?thesis using assms by (auto intro!: measurable_sets) qed lemma (in sigma_algebra) borel_measurable_ereal_neq_const: fixes f :: "'a \ ereal" assumes "f \ borel_measurable M" shows "{x\space M. f x \ c} \ sets M" proof - have "{x\space M. f x \ c} = space M - (f -` {c} \ space M)" by auto then show ?thesis using assms by (auto intro!: measurable_sets) qed lemma (in sigma_algebra) borel_measurable_ereal_le[intro,simp]: fixes f g :: "'a \ ereal" assumes f: "f \ borel_measurable M" assumes g: "g \ borel_measurable M" shows "{x \ space M. f x \ g x} \ sets M" proof - have "{x \ space M. f x \ g x} = {x \ space M. real (f x) \ real (g x)} - (f -` {\, -\} \ space M \ g -` {\, -\} \ space M) \ f -` {-\} \ space M \ g -` {\} \ space M" (is "?l = ?r") proof (intro set_eqI) fix x show "x \ ?l \ x \ ?r" by (cases rule: ereal2_cases[of "f x" "g x"]) auto qed with f g show ?thesis by (auto intro!: Un simp: measurable_sets) qed lemma (in sigma_algebra) borel_measurable_ereal_less[intro,simp]: fixes f :: "'a \ ereal" assumes f: "f \ borel_measurable M" assumes g: "g \ borel_measurable M" shows "{x \ space M. f x < g x} \ sets M" proof - have "{x \ space M. f x < g x} = space M - {x \ space M. g x \ f x}" by auto then show ?thesis using g f by auto qed lemma (in sigma_algebra) borel_measurable_ereal_eq[intro,simp]: fixes f :: "'a \ ereal" assumes f: "f \ borel_measurable M" assumes g: "g \ borel_measurable M" shows "{w \ space M. f w = g w} \ sets M" proof - have "{x \ space M. f x = g x} = {x \ space M. g x \ f x} \ {x \ space M. f x \ g x}" by auto then show ?thesis using g f by auto qed lemma (in sigma_algebra) borel_measurable_ereal_neq[intro,simp]: fixes f :: "'a \ ereal" assumes f: "f \ borel_measurable M" assumes g: "g \ borel_measurable M" shows "{w \ space M. f w \ g w} \ sets M" proof - have "{w \ space M. f w \ g w} = space M - {w \ space M. f w = g w}" by auto thus ?thesis using f g by auto qed lemma (in sigma_algebra) split_sets: "{x\space M. P x \ Q x} = {x\space M. P x} \ {x\space M. Q x}" "{x\space M. P x \ Q x} = {x\space M. P x} \ {x\space M. Q x}" by auto lemma (in sigma_algebra) borel_measurable_ereal_add[intro, simp]: fixes f :: "'a \ ereal" assumes "f \ borel_measurable M" "g \ borel_measurable M" shows "(\x. f x + g x) \ borel_measurable M" proof - { fix x assume "x \ space M" then have "f x + g x = (if f x = \ \ g x = \ then \ else if f x = -\ \ g x = -\ then -\ else ereal (real (f x) + real (g x)))" by (cases rule: ereal2_cases[of "f x" "g x"]) auto } with assms show ?thesis by (auto cong: measurable_cong simp: split_sets intro!: Un measurable_If measurable_sets) qed lemma (in sigma_algebra) borel_measurable_ereal_setsum[simp, intro]: fixes f :: "'c \ 'a \ ereal" assumes "\i. i \ S \ f i \ borel_measurable M" shows "(\x. \i\S. f i x) \ borel_measurable M" proof cases assume "finite S" thus ?thesis using assms by induct auto qed (simp add: borel_measurable_const) lemma (in sigma_algebra) borel_measurable_ereal_abs[intro, simp]: fixes f :: "'a \ ereal" assumes "f \ borel_measurable M" shows "(\x. \f x\) \ borel_measurable M" proof - { fix x have "\f x\ = (if 0 \ f x then f x else - f x)" by auto } then show ?thesis using assms by (auto intro!: measurable_If) qed lemma (in sigma_algebra) borel_measurable_ereal_times[intro, simp]: fixes f :: "'a \ ereal" assumes "f \ borel_measurable M" "g \ borel_measurable M" shows "(\x. f x * g x) \ borel_measurable M" proof - { fix f g :: "'a \ ereal" assume b: "f \ borel_measurable M" "g \ borel_measurable M" and pos: "\x. 0 \ f x" "\x. 0 \ g x" { fix x have *: "f x * g x = (if f x = 0 \ g x = 0 then 0 else if f x = \ \ g x = \ then \ else ereal (real (f x) * real (g x)))" apply (cases rule: ereal2_cases[of "f x" "g x"]) using pos[of x] by auto } with b have "(\x. f x * g x) \ borel_measurable M" by (auto cong: measurable_cong simp: split_sets intro!: Un measurable_If measurable_sets) } note pos_times = this have *: "(\x. f x * g x) = (\x. if 0 \ f x \ 0 \ g x \ f x < 0 \ g x < 0 then \f x\ * \g x\ else - (\f x\ * \g x\))" by (auto simp: fun_eq_iff) show ?thesis using assms unfolding * by (intro measurable_If pos_times borel_measurable_uminus_ereal) (auto simp: split_sets intro!: Int) qed lemma (in sigma_algebra) borel_measurable_ereal_setprod[simp, intro]: fixes f :: "'c \ 'a \ ereal" assumes "\i. i \ S \ f i \ borel_measurable M" shows "(\x. \i\S. f i x) \ borel_measurable M" proof cases assume "finite S" thus ?thesis using assms by induct auto qed simp lemma (in sigma_algebra) borel_measurable_ereal_min[simp, intro]: fixes f g :: "'a \ ereal" assumes "f \ borel_measurable M" assumes "g \ borel_measurable M" shows "(\x. min (g x) (f x)) \ borel_measurable M" using assms unfolding min_def by (auto intro!: measurable_If) lemma (in sigma_algebra) borel_measurable_ereal_max[simp, intro]: fixes f g :: "'a \ ereal" assumes "f \ borel_measurable M" and "g \ borel_measurable M" shows "(\x. max (g x) (f x)) \ borel_measurable M" using assms unfolding max_def by (auto intro!: measurable_If) lemma (in sigma_algebra) borel_measurable_SUP[simp, intro]: fixes f :: "'d\countable \ 'a \ ereal" assumes "\i. i \ A \ f i \ borel_measurable M" shows "(\x. SUP i : A. f i x) \ borel_measurable M" (is "?sup \ borel_measurable M") unfolding borel_measurable_ereal_iff_ge proof fix a have "?sup -` {a<..} \ space M = (\i\A. {x\space M. a < f i x})" by (auto simp: less_SUP_iff SUP_apply) then show "?sup -` {a<..} \ space M \ sets M" using assms by auto qed lemma (in sigma_algebra) borel_measurable_INF[simp, intro]: fixes f :: "'d :: countable \ 'a \ ereal" assumes "\i. i \ A \ f i \ borel_measurable M" shows "(\x. INF i : A. f i x) \ borel_measurable M" (is "?inf \ borel_measurable M") unfolding borel_measurable_ereal_iff_less proof fix a have "?inf -` {.. space M = (\i\A. {x\space M. f i x < a})" by (auto simp: INF_less_iff INF_apply) then show "?inf -` {.. space M \ sets M" using assms by auto qed lemma (in sigma_algebra) borel_measurable_liminf[simp, intro]: fixes f :: "nat \ 'a \ ereal" assumes "\i. f i \ borel_measurable M" shows "(\x. liminf (\i. f i x)) \ borel_measurable M" unfolding liminf_SUPR_INFI using assms by auto lemma (in sigma_algebra) borel_measurable_limsup[simp, intro]: fixes f :: "nat \ 'a \ ereal" assumes "\i. f i \ borel_measurable M" shows "(\x. limsup (\i. f i x)) \ borel_measurable M" unfolding limsup_INFI_SUPR using assms by auto lemma (in sigma_algebra) borel_measurable_ereal_diff[simp, intro]: fixes f g :: "'a \ ereal" assumes "f \ borel_measurable M" assumes "g \ borel_measurable M" shows "(\x. f x - g x) \ borel_measurable M" unfolding minus_ereal_def using assms by auto lemma (in sigma_algebra) borel_measurable_psuminf[simp, intro]: fixes f :: "nat \ 'a \ ereal" assumes "\i. f i \ borel_measurable M" and pos: "\i x. x \ space M \ 0 \ f i x" shows "(\x. (\i. f i x)) \ borel_measurable M" apply (subst measurable_cong) apply (subst suminf_ereal_eq_SUPR) apply (rule pos) using assms by auto section "LIMSEQ is borel measurable" lemma (in sigma_algebra) borel_measurable_LIMSEQ: fixes u :: "nat \ 'a \ real" assumes u': "\x. x \ space M \ (\i. u i x) ----> u' x" and u: "\i. u i \ borel_measurable M" shows "u' \ borel_measurable M" proof - have "\x. x \ space M \ liminf (\n. ereal (u n x)) = ereal (u' x)" using u' by (simp add: lim_imp_Liminf) moreover from u have "(\x. liminf (\n. ereal (u n x))) \ borel_measurable M" by auto ultimately show ?thesis by (simp cong: measurable_cong add: borel_measurable_ereal_iff) qed end