(* Author: Armin Heller, Johannes Hoelzl, TU Muenchen *) header {*Borel spaces*} theory Borel imports Sigma_Algebra Positive_Infinite_Real Multivariate_Analysis begin lemma LIMSEQ_max: "u ----> (x::real) \ (\i. max (u i) 0) ----> max x 0" by (fastsimp intro!: LIMSEQ_I dest!: LIMSEQ_D) section "Generic Borel spaces" definition "borel_space = sigma (UNIV::'a::topological_space set) open" abbreviation "borel_measurable M \ measurable M borel_space" interpretation borel_space: sigma_algebra borel_space using sigma_algebra_sigma by (auto simp: borel_space_def) lemma in_borel_measurable: "f \ borel_measurable M \ (\S \ sets (sigma UNIV open). f -` S \ space M \ sets M)" by (auto simp add: measurable_def borel_space_def) lemma in_borel_measurable_borel_space: "f \ borel_measurable M \ (\S \ sets borel_space. f -` S \ space M \ sets M)" by (auto simp add: measurable_def borel_space_def) lemma space_borel_space[simp]: "space borel_space = UNIV" unfolding borel_space_def by auto lemma borel_space_open[simp]: assumes "open A" shows "A \ sets borel_space" proof - have "A \ open" unfolding mem_def using assms . thus ?thesis unfolding borel_space_def sigma_def by (auto intro!: sigma_sets.Basic) qed lemma borel_space_closed[simp]: assumes "closed A" shows "A \ sets borel_space" proof - have "space borel_space - (- A) \ sets borel_space" using assms unfolding closed_def by (blast intro: borel_space_open) thus ?thesis by simp qed 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_sing[of "f y"] have "{f y} \ sets borel_space" by (rule borel_space_closed) with assms show ?thesis unfolding in_borel_measurable_borel_space `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_space_def proof (rule measurable_sigma) fix S :: "'x set" assume "S \ open" thus "f -` S \ space M \ sets M" using assms[of S] by (simp add: mem_def) qed simp_all lemma borel_space_singleton[simp, intro]: fixes x :: "'a::t1_space" shows "A \ sets borel_space \ insert x A \ sets borel_space" proof (rule borel_space.insert_in_sets) show "{x} \ sets borel_space" using closed_sing[of x] by (rule borel_space_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 borel_measurable_translate: assumes "A \ sets borel_space" and trans: "\B. open B \ f -` B \ sets borel_space" shows "f -` A \ sets borel_space" proof - have "A \ sigma_sets UNIV open" using assms by (simp add: borel_space_def sigma_def) thus ?thesis proof (induct rule: sigma_sets.induct) case (Basic a) thus ?case using trans[of a] by (simp add: mem_def) next case (Compl a) moreover have "UNIV \ sets borel_space" by (metis borel_space.top borel_space_def_raw mem_def space_sigma) ultimately show ?case by (auto simp: vimage_Diff borel_space.Diff) qed (auto simp add: vimage_UN) qed lemma (in sigma_algebra) borel_measurable_restricted: fixes f :: "'a \ 'x\{topological_space, semiring_1}" 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_space proof (simp, safe) fix S :: "'x set" assume "S \ sets borel_space" "\S\sets borel_space. ?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 fastsimp 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 :: "'x set" assume "S \ sets borel_space" "\S\sets borel_space. ?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 "N \ sets M" "f \ borel_measurable (M\sets:=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_space" by (blast intro: borel_space_open) lemma greaterThan_borel[simp, intro]: fixes a :: "'a\ordered_euclidean_space" shows "{a <..} \ sets borel_space" by (blast intro: borel_space_open) lemma greaterThanLessThan_borel[simp, intro]: fixes a b :: "'a\ordered_euclidean_space" shows "{a<.. sets borel_space" by (blast intro: borel_space_open) lemma atMost_borel[simp, intro]: fixes a :: "'a\ordered_euclidean_space" shows "{..a} \ sets borel_space" by (blast intro: borel_space_closed) lemma atLeast_borel[simp, intro]: fixes a :: "'a\ordered_euclidean_space" shows "{a..} \ sets borel_space" by (blast intro: borel_space_closed) lemma atLeastAtMost_borel[simp, intro]: fixes a b :: "'a\ordered_euclidean_space" shows "{a..b} \ sets borel_space" by (blast intro: borel_space_closed) lemma greaterThanAtMost_borel[simp, intro]: fixes a b :: "'a\ordered_euclidean_space" shows "{a<..b} \ sets borel_space" unfolding greaterThanAtMost_def by blast lemma atLeastLessThan_borel[simp, intro]: fixes a b :: "'a\ordered_euclidean_space" shows "{a.. sets borel_space" unfolding atLeastLessThan_def by blast lemma hafspace_less_borel[simp, intro]: fixes a :: real shows "{x::'a::euclidean_space. a < x $$ i} \ sets borel_space" by (auto intro!: borel_space_open open_halfspace_component_gt) lemma hafspace_greater_borel[simp, intro]: fixes a :: real shows "{x::'a::euclidean_space. x $$ i < a} \ sets borel_space" by (auto intro!: borel_space_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_space" by (auto intro!: borel_space_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_space" by (auto intro!: borel_space_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: "sets (sigma UNIV (range (\ (a, i). {x\'a\ordered_euclidean_space. x $$ i < a}))) \ sets borel_space" by (auto intro!: borel_space.sigma_sets_subset[simplified] borel_space_open open_halfspace_component_lt simp: sets_sigma) lemma halfspace_lt_in_halfspace: "{x\'a. x $$ i < a} \ sets (sigma UNIV (range (\ (a, i). {x\'a\ordered_euclidean_space. x $$ i < a})))" unfolding sets_sigma by (rule sigma_sets.Basic) auto lemma halfspace_gt_in_halfspace: "{x\'a. a < x $$ i} \ sets (sigma UNIV (range (\ (a, i). {x\'a\ordered_euclidean_space. x $$ i < a})))" (is "?set \ sets ?SIGMA") proof - interpret sigma_algebra ?SIGMA by (rule sigma_algebra_sigma) simp 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 (in sigma_algebra) sets_sigma_subset: assumes "A = space M" assumes "B \ sets M" shows "sets (sigma A B) \ sets M" by (unfold assms sets_sigma, rule sigma_sets_subset, rule assms) lemma open_span_halfspace: "sets borel_space \ sets (sigma UNIV (range (\ (a, i). {x::'a::ordered_euclidean_space. x $$ i < a})))" (is "_ \ sets ?SIGMA") proof (unfold borel_space_def, rule sigma_algebra.sets_sigma_subset, safe) show "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) simp then interpret sigma_algebra ?SIGMA . fix S :: "'a set" assume "S \ open" then have "open S" unfolding mem_def . 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 show "S \ sets ?SIGMA" unfolding * by (auto intro!: countable_UN Int countable_INT halfspace_lt_in_halfspace halfspace_gt_in_halfspace) qed auto lemma halfspace_span_halfspace_le: "sets (sigma UNIV (range (\ (a, i). {x\'a\ordered_euclidean_space. x $$ i < a}))) \ sets (sigma UNIV (range (\ (a, i). {x. x $$ i \ a})))" (is "_ \ sets ?SIGMA") proof (rule sigma_algebra.sets_sigma_subset, safe) show "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 show "{x. x$$i < a} \ sets ?SIGMA" unfolding * by (safe intro!: countable_UN) (auto simp: sets_sigma intro!: sigma_sets.Basic) qed auto lemma halfspace_span_halfspace_ge: "sets (sigma UNIV (range (\ (a, i). {x\'a\ordered_euclidean_space. x $$ i < a}))) \ sets (sigma UNIV (range (\ (a, i). {x. a \ x $$ i})))" (is "_ \ sets ?SIGMA") proof (rule sigma_algebra.sets_sigma_subset, safe) show "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 show "{x. x$$i < a} \ sets ?SIGMA" unfolding * by (safe intro!: Diff) (auto simp: sets_sigma intro!: sigma_sets.Basic) qed auto lemma halfspace_le_span_halfspace_gt: "sets (sigma UNIV (range (\ (a, i). {x\'a\ordered_euclidean_space. x $$ i \ a}))) \ sets (sigma UNIV (range (\ (a, i). {x. a < x $$ i})))" (is "_ \ sets ?SIGMA") proof (rule sigma_algebra.sets_sigma_subset, safe) show "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 show "{x. x$$i \ a} \ sets ?SIGMA" unfolding * by (safe intro!: Diff) (auto simp: sets_sigma intro!: sigma_sets.Basic) qed auto lemma halfspace_le_span_atMost: "sets (sigma UNIV (range (\ (a, i). {x\'a\ordered_euclidean_space. x $$ i \ a}))) \ sets (sigma UNIV (range (\a. {..a\'a\ordered_euclidean_space})))" (is "_ \ sets ?SIGMA") proof (rule sigma_algebra.sets_sigma_subset, safe) show "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto then interpret sigma_algebra ?SIGMA . fix a i show "{x. x$$i \ a} \ sets ?SIGMA" proof cases 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 assume "\ i < DIM('a)" then show "{x. x$$i \ a} \ sets ?SIGMA" using top by auto qed qed auto lemma halfspace_le_span_greaterThan: "sets (sigma UNIV (range (\ (a, i). {x\'a\ordered_euclidean_space. x $$ i \ a}))) \ sets (sigma UNIV (range (\a. {a<..})))" (is "_ \ sets ?SIGMA") proof (rule sigma_algebra.sets_sigma_subset, safe) show "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto then interpret sigma_algebra ?SIGMA . fix a i show "{x. x$$i \ a} \ sets ?SIGMA" proof cases 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) by (auto simp: sets_sigma intro!: sigma_sets.Basic) next assume "\ i < DIM('a)" then show "{x. x$$i \ a} \ sets ?SIGMA" using top by auto qed qed auto lemma atMost_span_atLeastAtMost: "sets (sigma UNIV (range (\a. {..a\'a\ordered_euclidean_space}))) \ sets (sigma UNIV (range (\(a,b). {a..b})))" (is "_ \ sets ?SIGMA") proof (rule sigma_algebra.sets_sigma_subset, safe) show "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 show "{..a} \ sets ?SIGMA" unfolding * by (safe intro!: countable_UN) (auto simp: sets_sigma intro!: sigma_sets.Basic) qed auto lemma borel_space_eq_greaterThanLessThan: "sets borel_space = sets (sigma UNIV (range (\ (a, b). {a <..< (b :: 'a \ ordered_euclidean_space)})))" (is "_ = sets ?SIGMA") proof (rule antisym) show "sets ?SIGMA \ sets borel_space" by (rule borel_space.sets_sigma_subset) auto show "sets borel_space \ sets ?SIGMA" unfolding borel_space_def proof (rule sigma_algebra.sets_sigma_subset, safe) show "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto then interpret sigma_algebra ?SIGMA . fix M :: "'a set" assume "M \ open" then have "open M" by (simp add: mem_def) show "M \ sets ?SIGMA" apply (subst open_UNION[OF `open M`]) apply (safe intro!: countable_UN) by (auto simp add: sigma_def intro!: sigma_sets.Basic) qed auto qed lemma borel_space_eq_atMost: "sets borel_space = sets (sigma UNIV (range (\ a. {.. a::'a\ordered_euclidean_space})))" (is "_ = sets ?SIGMA") proof (rule antisym) show "sets borel_space \ sets ?SIGMA" using halfspace_le_span_atMost halfspace_span_halfspace_le open_span_halfspace by auto show "sets ?SIGMA \ sets borel_space" by (rule borel_space.sets_sigma_subset) auto qed lemma borel_space_eq_atLeastAtMost: "sets borel_space = sets (sigma UNIV (range (\ (a :: 'a\ordered_euclidean_space, b). {a .. b})))" (is "_ = sets ?SIGMA") proof (rule antisym) show "sets borel_space \ sets ?SIGMA" using atMost_span_atLeastAtMost halfspace_le_span_atMost halfspace_span_halfspace_le open_span_halfspace by auto show "sets ?SIGMA \ sets borel_space" by (rule borel_space.sets_sigma_subset) auto qed lemma borel_space_eq_greaterThan: "sets borel_space = sets (sigma UNIV (range (\ (a :: 'a\ordered_euclidean_space). {a <..})))" (is "_ = sets ?SIGMA") proof (rule antisym) show "sets borel_space \ sets ?SIGMA" using halfspace_le_span_greaterThan halfspace_span_halfspace_le open_span_halfspace by auto show "sets ?SIGMA \ sets borel_space" by (rule borel_space.sets_sigma_subset) auto qed lemma borel_space_eq_halfspace_le: "sets borel_space = sets (sigma UNIV (range (\ (a, i). {x::'a::ordered_euclidean_space. x$$i \ a})))" (is "_ = sets ?SIGMA") proof (rule antisym) show "sets borel_space \ sets ?SIGMA" using open_span_halfspace halfspace_span_halfspace_le by auto show "sets ?SIGMA \ sets borel_space" by (rule borel_space.sets_sigma_subset) auto qed lemma borel_space_eq_halfspace_less: "sets borel_space = sets (sigma UNIV (range (\ (a, i). {x::'a::ordered_euclidean_space. x$$i < a})))" (is "_ = sets ?SIGMA") proof (rule antisym) show "sets borel_space \ sets ?SIGMA" using open_span_halfspace . show "sets ?SIGMA \ sets borel_space" by (rule borel_space.sets_sigma_subset) auto qed lemma borel_space_eq_halfspace_gt: "sets borel_space = sets (sigma UNIV (range (\ (a, i). {x::'a::ordered_euclidean_space. a < x$$i})))" (is "_ = sets ?SIGMA") proof (rule antisym) show "sets borel_space \ sets ?SIGMA" using halfspace_le_span_halfspace_gt open_span_halfspace halfspace_span_halfspace_le by auto show "sets ?SIGMA \ sets borel_space" by (rule borel_space.sets_sigma_subset) auto qed lemma borel_space_eq_halfspace_ge: "sets borel_space = sets (sigma UNIV (range (\ (a, i). {x::'a::ordered_euclidean_space. a \ x$$i})))" (is "_ = sets ?SIGMA") proof (rule antisym) show "sets borel_space \ sets ?SIGMA" using halfspace_span_halfspace_ge open_span_halfspace by auto show "sets ?SIGMA \ sets borel_space" by (rule borel_space.sets_sigma_subset) auto qed lemma (in sigma_algebra) borel_measurable_halfspacesI: fixes f :: "'a \ 'c\ordered_euclidean_space" assumes "sets borel_space = sets (sigma UNIV (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 UNIV (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_space_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_space_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_space_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_space_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_measureable_euclidean_component: "(\x::'a::euclidean_space. x $$ i) \ borel_measurable borel_space" unfolding borel_space_def[where 'a=real] proof (rule borel_space.measurable_sigma) fix S::"real set" assume "S \ open" then have "open S" unfolding mem_def . from open_vimage_euclidean_component[OF this] show "(\x. x $$ i) -` S \ space borel_space \ sets borel_space" by (auto intro: borel_space_open) qed auto lemma (in sigma_algebra) borel_measureable_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_measureable_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 "((\x. (- a + x) /\<^sub>R b) ` S) \ open" (is "?S \ open") by (auto intro!: open_affinity simp: scaleR.add_right mem_def) hence "?S \ sets borel_space" unfolding borel_space_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_space 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_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_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_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_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 section "Borel space over the real line with infinity" lemma borel_space_Real_measurable: "A \ sets borel_space \ Real -` A \ sets borel_space" proof (rule borel_measurable_translate) fix B :: "pinfreal set" assume "open B" then obtain T x where T: "open T" "Real ` (T \ {0..}) = B - {\}" and x: "\ \ B \ 0 \ x" "\ \ B \ {Real x <..} \ B" unfolding open_pinfreal_def by blast have "Real -` B = Real -` (B - {\})" by auto also have "\ = Real -` (Real ` (T \ {0..}))" using T by simp also have "\ = (if 0 \ T then T \ {.. 0} else T \ {0..})" apply (auto simp add: Real_eq_Real image_iff) apply (rule_tac x="max 0 x" in bexI) by (auto simp: max_def) finally show "Real -` B \ sets borel_space" using `open T` by auto qed simp lemma borel_space_real_measurable: "A \ sets borel_space \ (real -` A :: pinfreal set) \ sets borel_space" proof (rule borel_measurable_translate) fix B :: "real set" assume "open B" { fix x have "0 < real x \ (\r>0. x = Real r)" by (cases x) auto } note Ex_less_real = this have *: "real -` B = (if 0 \ B then real -` (B \ {0 <..}) \ {0, \} else real -` (B \ {0 <..}))" by (force simp: Ex_less_real) have "open (real -` (B \ {0 <..}) :: pinfreal set)" unfolding open_pinfreal_def using `open B` by (auto intro!: open_Int exI[of _ "B \ {0 <..}"] simp: image_iff Ex_less_real) then show "(real -` B :: pinfreal set) \ sets borel_space" unfolding * by auto qed simp lemma (in sigma_algebra) borel_measurable_Real[intro, simp]: assumes "f \ borel_measurable M" shows "(\x. Real (f x)) \ borel_measurable M" unfolding in_borel_measurable_borel_space proof safe fix S :: "pinfreal set" assume "S \ sets borel_space" from borel_space_Real_measurable[OF this] have "(Real \ f) -` S \ space M \ sets M" using assms unfolding vimage_compose in_borel_measurable_borel_space by auto thus "(\x. Real (f x)) -` S \ space M \ sets M" by (simp add: comp_def) qed lemma (in sigma_algebra) borel_measurable_real[intro, simp]: fixes f :: "'a \ pinfreal" assumes "f \ borel_measurable M" shows "(\x. real (f x)) \ borel_measurable M" unfolding in_borel_measurable_borel_space proof safe fix S :: "real set" assume "S \ sets borel_space" from borel_space_real_measurable[OF this] have "(real \ f) -` S \ space M \ sets M" using assms unfolding vimage_compose in_borel_measurable_borel_space by auto thus "(\x. real (f x)) -` S \ space M \ sets M" by (simp add: comp_def) qed lemma (in sigma_algebra) borel_measurable_Real_eq: assumes "\x. x \ space M \ 0 \ f x" shows "(\x. Real (f x)) \ borel_measurable M \ f \ borel_measurable M" proof have [simp]: "(\x. Real (f x)) -` {\} \ space M = {}" by auto assume "(\x. Real (f x)) \ borel_measurable M" hence "(\x. real (Real (f x))) \ borel_measurable M" by (rule borel_measurable_real) moreover have "\x. x \ space M \ real (Real (f x)) = f x" using assms by auto ultimately show "f \ borel_measurable M" by (simp cong: measurable_cong) qed auto lemma (in sigma_algebra) borel_measurable_pinfreal_eq_real: "f \ borel_measurable M \ ((\x. real (f x)) \ borel_measurable M \ f -` {\} \ space M \ sets M)" proof safe assume "f \ borel_measurable M" then show "(\x. real (f x)) \ borel_measurable M" "f -` {\} \ space M \ sets M" by (auto intro: borel_measurable_vimage borel_measurable_real) next assume *: "(\x. real (f x)) \ borel_measurable M" "f -` {\} \ space M \ sets M" have "f -` {\} \ space M = {x\space M. f x = \}" by auto with * have **: "{x\space M. f x = \} \ sets M" by simp have f: "f = (\x. if f x = \ then \ else Real (real (f x)))" by (simp add: expand_fun_eq Real_real) show "f \ borel_measurable M" apply (subst f) apply (rule measurable_If) using * ** by auto qed lemma (in sigma_algebra) less_eq_ge_measurable: fixes f :: "'a \ 'c::linorder" shows "{x\space M. a < f x} \ sets M \ {x\space M. f x \ a} \ sets M" proof assume "{x\space M. f x \ a} \ sets M" moreover have "{x\space M. a < f x} = space M - {x\space M. f x \ a}" by auto ultimately show "{x\space M. a < f x} \ sets M" by auto next assume "{x\space M. a < f x} \ sets M" moreover have "{x\space M. f x \ a} = space M - {x\space M. a < f x}" by auto ultimately show "{x\space M. f x \ a} \ sets M" by auto qed lemma (in sigma_algebra) greater_eq_le_measurable: fixes f :: "'a \ 'c::linorder" shows "{x\space M. f x < a} \ sets M \ {x\space M. a \ f x} \ sets M" proof assume "{x\space M. a \ f x} \ sets M" moreover have "{x\space M. f x < a} = space M - {x\space M. a \ f x}" by auto ultimately show "{x\space M. f x < a} \ sets M" by auto next assume "{x\space M. f x < a} \ sets M" moreover have "{x\space M. a \ f x} = space M - {x\space M. f x < a}" by auto ultimately show "{x\space M. a \ f x} \ sets M" by auto qed lemma (in sigma_algebra) less_eq_le_pinfreal_measurable: fixes f :: "'a \ pinfreal" shows "(\a. {x\space M. a < f x} \ sets M) \ (\a. {x\space M. a \ f x} \ sets M)" proof assume a: "\a. {x\space M. a \ f x} \ sets M" show "\a. {x \ space M. a < f x} \ sets M" proof fix a show "{x \ space M. a < f x} \ sets M" proof (cases a) case (preal r) have "{x\space M. a < f x} = (\i. {x\space M. a + inverse (of_nat (Suc i)) \ f x})" proof safe fix x assume "a < f x" and [simp]: "x \ space M" with ex_pinfreal_inverse_of_nat_Suc_less[of "f x - a"] obtain n where "a + inverse (of_nat (Suc n)) < f x" by (cases "f x", auto simp: pinfreal_minus_order) then have "a + inverse (of_nat (Suc n)) \ f x" by simp then show "x \ (\i. {x \ space M. a + inverse (of_nat (Suc i)) \ f x})" by auto next fix i x assume [simp]: "x \ space M" have "a < a + inverse (of_nat (Suc i))" using preal by auto also assume "a + inverse (of_nat (Suc i)) \ f x" finally show "a < f x" . qed with a show ?thesis by auto qed simp qed next assume a': "\a. {x \ space M. a < f x} \ sets M" then have a: "\a. {x \ space M. f x \ a} \ sets M" unfolding less_eq_ge_measurable . show "\a. {x \ space M. a \ f x} \ sets M" unfolding greater_eq_le_measurable[symmetric] proof fix a show "{x \ space M. f x < a} \ sets M" proof (cases a) case (preal r) show ?thesis proof cases assume "a = 0" then show ?thesis by simp next assume "a \ 0" have "{x\space M. f x < a} = (\i. {x\space M. f x \ a - inverse (of_nat (Suc i))})" proof safe fix x assume "f x < a" and [simp]: "x \ space M" with ex_pinfreal_inverse_of_nat_Suc_less[of "a - f x"] obtain n where "inverse (of_nat (Suc n)) < a - f x" using preal by (cases "f x") auto then have "f x \ a - inverse (of_nat (Suc n)) " using preal by (cases "f x") (auto split: split_if_asm) then show "x \ (\i. {x \ space M. f x \ a - inverse (of_nat (Suc i))})" by auto next fix i x assume [simp]: "x \ space M" assume "f x \ a - inverse (of_nat (Suc i))" also have "\ < a" using `a \ 0` preal by auto finally show "f x < a" . qed with a show ?thesis by auto qed next case infinite have "f -` {\} \ space M = (\n. {x\space M. of_nat n < f x})" proof (safe, simp_all, safe) fix x assume *: "\n::nat. Real (real n) < f x" show "f x = \" proof (rule ccontr) assume "f x \ \" with real_arch_lt[of "real (f x)"] obtain n where "f x < of_nat n" by (auto simp: pinfreal_noteq_omega_Ex) with *[THEN spec, of n] show False by auto qed qed with a' have \: "f -` {\} \ space M \ sets M" by auto moreover have "{x \ space M. f x < a} = space M - f -` {\} \ space M" using infinite by auto ultimately show ?thesis by auto qed qed qed lemma (in sigma_algebra) borel_measurable_pinfreal_iff_greater: "(f::'a \ pinfreal) \ borel_measurable M \ (\a. {x\space M. a < f x} \ sets M)" proof safe fix a assume f: "f \ borel_measurable M" have "{x\space M. a < f x} = f -` {a <..} \ space M" by auto with f show "{x\space M. a < f x} \ sets M" by (auto intro!: measurable_sets) next assume *: "\a. {x\space M. a < f x} \ sets M" hence **: "\a. {x\space M. f x < a} \ sets M" unfolding less_eq_le_pinfreal_measurable unfolding greater_eq_le_measurable . show "f \ borel_measurable M" unfolding borel_measurable_pinfreal_eq_real borel_measurable_iff_greater proof safe have "f -` {\} \ space M = space M - {x\space M. f x < \}" by auto then show \: "f -` {\} \ space M \ sets M" using ** by auto fix a have "{w \ space M. a < real (f w)} = (if 0 \ a then {w\space M. Real a < f w} - (f -` {\} \ space M) else space M)" proof (split split_if, safe del: notI) fix x assume "0 \ a" { assume "a < real (f x)" then show "Real a < f x" "x \ f -` {\} \ space M" using `0 \ a` by (cases "f x", auto) } { assume "Real a < f x" "x \ f -` {\}" then show "a < real (f x)" using `0 \ a` by (cases "f x", auto) } next fix x assume "\ 0 \ a" then show "a < real (f x)" by (cases "f x") auto qed then show "{w \ space M. a < real (f w)} \ sets M" using \ * by (auto intro!: Diff) qed qed lemma (in sigma_algebra) borel_measurable_pinfreal_iff_less: "(f::'a \ pinfreal) \ borel_measurable M \ (\a. {x\space M. f x < a} \ sets M)" using borel_measurable_pinfreal_iff_greater unfolding less_eq_le_pinfreal_measurable greater_eq_le_measurable . lemma (in sigma_algebra) borel_measurable_pinfreal_iff_le: "(f::'a \ pinfreal) \ borel_measurable M \ (\a. {x\space M. f x \ a} \ sets M)" using borel_measurable_pinfreal_iff_greater unfolding less_eq_ge_measurable . lemma (in sigma_algebra) borel_measurable_pinfreal_iff_ge: "(f::'a \ pinfreal) \ borel_measurable M \ (\a. {x\space M. a \ f x} \ sets M)" using borel_measurable_pinfreal_iff_greater unfolding less_eq_le_pinfreal_measurable . lemma (in sigma_algebra) borel_measurable_pinfreal_eq_const: fixes f :: "'a \ pinfreal" 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_pinfreal_neq_const: fixes f :: "'a \ pinfreal" 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_pinfreal_less[intro,simp]: fixes f g :: "'a \ pinfreal" 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. real (f x)) \ borel_measurable M" "(\x. real (g x)) \ borel_measurable M" using assms by (auto intro!: borel_measurable_real) from borel_measurable_less[OF this] have "{x \ space M. real (f x) < real (g x)} \ sets M" . moreover have "{x \ space M. f x \ \} \ sets M" using f by (rule borel_measurable_pinfreal_neq_const) moreover have "{x \ space M. g x = \} \ sets M" using g by (rule borel_measurable_pinfreal_eq_const) moreover have "{x \ space M. g x \ \} \ sets M" using g by (rule borel_measurable_pinfreal_neq_const) moreover have "{x \ space M. f x < g x} = ({x \ space M. g x = \} \ {x \ space M. f x \ \}) \ ({x \ space M. g x \ \} \ {x \ space M. f x \ \} \ {x \ space M. real (f x) < real (g x)})" by (auto simp: real_of_pinfreal_strict_mono_iff) ultimately show ?thesis by auto qed lemma (in sigma_algebra) borel_measurable_pinfreal_le[intro,simp]: fixes f :: "'a \ pinfreal" 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_pinfreal_eq[intro,simp]: fixes f :: "'a \ pinfreal" 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_pinfreal_neq[intro,simp]: fixes f :: "'a \ pinfreal" 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) borel_measurable_pinfreal_add[intro, simp]: fixes f :: "'a \ pinfreal" assumes measure: "f \ borel_measurable M" "g \ borel_measurable M" shows "(\x. f x + g x) \ borel_measurable M" proof - have *: "(\x. f x + g x) = (\x. if f x = \ then \ else if g x = \ then \ else Real (real (f x) + real (g x)))" by (auto simp: expand_fun_eq pinfreal_noteq_omega_Ex) show ?thesis using assms unfolding * by (auto intro!: measurable_If) qed lemma (in sigma_algebra) borel_measurable_pinfreal_times[intro, simp]: fixes f :: "'a \ pinfreal" assumes "f \ borel_measurable M" "g \ borel_measurable M" shows "(\x. f x * g x) \ borel_measurable M" proof - have *: "(\x. f x * g x) = (\x. if f x = 0 then 0 else if g x = 0 then 0 else if f x = \ then \ else if g x = \ then \ else Real (real (f x) * real (g x)))" by (auto simp: expand_fun_eq pinfreal_noteq_omega_Ex) show ?thesis using assms unfolding * by (auto intro!: measurable_If) qed lemma (in sigma_algebra) borel_measurable_pinfreal_setsum[simp, intro]: fixes f :: "'c \ 'a \ pinfreal" 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_pinfreal_min[intro, simp]: fixes f g :: "'a \ pinfreal" 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_pinfreal_max[intro]: fixes f g :: "'a \ pinfreal" 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 \ pinfreal" assumes "\i. i \ A \ f i \ borel_measurable M" shows "(SUP i : A. f i) \ borel_measurable M" (is "?sup \ borel_measurable M") unfolding borel_measurable_pinfreal_iff_greater proof safe fix a have "{x\space M. a < ?sup x} = (\i\A. {x\space M. a < f i x})" by (auto simp: less_Sup_iff SUPR_def[where 'a=pinfreal] SUPR_fun_expand[where 'c=pinfreal]) then show "{x\space M. a < ?sup x} \ sets M" using assms by auto qed lemma (in sigma_algebra) borel_measurable_INF[simp, intro]: fixes f :: "'d :: countable \ 'a \ pinfreal" assumes "\i. i \ A \ f i \ borel_measurable M" shows "(INF i : A. f i) \ borel_measurable M" (is "?inf \ borel_measurable M") unfolding borel_measurable_pinfreal_iff_less proof safe fix a have "{x\space M. ?inf x < a} = (\i\A. {x\space M. f i x < a})" by (auto simp: Inf_less_iff INFI_def[where 'a=pinfreal] INFI_fun_expand) then show "{x\space M. ?inf x < a} \ sets M" using assms by auto qed lemma (in sigma_algebra) borel_measurable_pinfreal_diff: fixes f g :: "'a \ pinfreal" assumes "f \ borel_measurable M" assumes "g \ borel_measurable M" shows "(\x. f x - g x) \ borel_measurable M" unfolding borel_measurable_pinfreal_iff_greater proof safe fix a have "{x \ space M. a < f x - g x} = {x \ space M. g x + a < f x}" by (simp add: pinfreal_less_minus_iff) then show "{x \ space M. a < f x - g x} \ sets M" using assms by auto qed lemma (in sigma_algebra) borel_measurable_psuminf: assumes "\i. f i \ borel_measurable M" shows "(\x. (\\<^isub>\ i. f i x)) \ borel_measurable M" using assms unfolding psuminf_def by (auto intro!: borel_measurable_SUP[unfolded SUPR_fun_expand]) 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 - let "?pu x i" = "max (u i x) 0" let "?nu x i" = "max (- u i x) 0" { fix x assume x: "x \ space M" have "(?pu x) ----> max (u' x) 0" "(?nu x) ----> max (- u' x) 0" using u'[OF x] by (auto intro!: LIMSEQ_max LIMSEQ_minus) from LIMSEQ_imp_lim_INF[OF _ this(1)] LIMSEQ_imp_lim_INF[OF _ this(2)] have "(SUP n. INF m. Real (u (n + m) x)) = Real (u' x)" "(SUP n. INF m. Real (- u (n + m) x)) = Real (- u' x)" by (simp_all add: Real_max'[symmetric]) } note eq = this have *: "\x. real (Real (u' x)) - real (Real (- u' x)) = u' x" by auto have "(SUP n. INF m. (\x. Real (u (n + m) x))) \ borel_measurable M" "(SUP n. INF m. (\x. Real (- u (n + m) x))) \ borel_measurable M" using u by (auto intro: borel_measurable_SUP borel_measurable_INF borel_measurable_Real) with eq[THEN measurable_cong, of M "\x. x" borel_space] have "(\x. Real (u' x)) \ borel_measurable M" "(\x. Real (- u' x)) \ borel_measurable M" unfolding SUPR_fun_expand INFI_fun_expand by auto note this[THEN borel_measurable_real] from borel_measurable_diff[OF this] show ?thesis unfolding * . qed end