src/HOL/Probability/Borel.thy
 author hoelzl Mon Aug 23 19:35:57 2010 +0200 (2010-08-23) changeset 38656 d5d342611edb parent 37887 2ae085b07f2f child 38705 aaee86c0e237 permissions -rw-r--r--
Rewrite the Probability theory.

Introduced pinfreal as real numbers with infinity.
Use pinfreal as value for measures.
Introduces Lebesgue Measure based on the integral in Multivariate Analysis.
Proved Radon Nikodym for arbitrary sigma finite measure spaces.
 hoelzl@38656 ` 1` ```(* Author: Armin Heller, Johannes Hoelzl, TU Muenchen *) ``` hoelzl@38656 ` 2` hoelzl@38656 ` 3` ```header {*Borel spaces*} ``` paulson@33533 ` 4` paulson@33533 ` 5` ```theory Borel ``` hoelzl@38656 ` 6` ``` imports Sigma_Algebra Positive_Infinite_Real Multivariate_Analysis ``` paulson@33533 ` 7` ```begin ``` paulson@33533 ` 8` hoelzl@38656 ` 9` ```section "Generic Borel spaces" ``` paulson@33533 ` 10` hoelzl@38656 ` 11` ```definition "borel_space = sigma (UNIV::'a::topological_space set) open" ``` hoelzl@38656 ` 12` ```abbreviation "borel_measurable M \ measurable M borel_space" ``` paulson@33533 ` 13` hoelzl@38656 ` 14` ```interpretation borel_space: sigma_algebra borel_space ``` hoelzl@38656 ` 15` ``` using sigma_algebra_sigma by (auto simp: borel_space_def) ``` paulson@33533 ` 16` paulson@33533 ` 17` ```lemma in_borel_measurable: ``` paulson@33533 ` 18` ``` "f \ borel_measurable M \ ``` hoelzl@38656 ` 19` ``` (\S \ sets (sigma UNIV open). ``` hoelzl@38656 ` 20` ``` f -` S \ space M \ sets M)" ``` hoelzl@38656 ` 21` ``` by (auto simp add: measurable_def borel_space_def) ``` paulson@33533 ` 22` hoelzl@38656 ` 23` ```lemma in_borel_measurable_borel_space: ``` hoelzl@38656 ` 24` ``` "f \ borel_measurable M \ ``` hoelzl@38656 ` 25` ``` (\S \ sets borel_space. ``` hoelzl@38656 ` 26` ``` f -` S \ space M \ sets M)" ``` hoelzl@38656 ` 27` ``` by (auto simp add: measurable_def borel_space_def) ``` paulson@33533 ` 28` hoelzl@38656 ` 29` ```lemma space_borel_space[simp]: "space borel_space = UNIV" ``` hoelzl@38656 ` 30` ``` unfolding borel_space_def by auto ``` hoelzl@38656 ` 31` hoelzl@38656 ` 32` ```lemma borel_space_open[simp]: ``` hoelzl@38656 ` 33` ``` assumes "open A" shows "A \ sets borel_space" ``` hoelzl@38656 ` 34` ```proof - ``` hoelzl@38656 ` 35` ``` have "A \ open" unfolding mem_def using assms . ``` hoelzl@38656 ` 36` ``` thus ?thesis unfolding borel_space_def sigma_def by (auto intro!: sigma_sets.Basic) ``` paulson@33533 ` 37` ```qed ``` paulson@33533 ` 38` hoelzl@38656 ` 39` ```lemma borel_space_closed[simp]: ``` hoelzl@38656 ` 40` ``` assumes "closed A" shows "A \ sets borel_space" ``` paulson@33533 ` 41` ```proof - ``` hoelzl@38656 ` 42` ``` have "space borel_space - (- A) \ sets borel_space" ``` hoelzl@38656 ` 43` ``` using assms unfolding closed_def by (blast intro: borel_space_open) ``` hoelzl@38656 ` 44` ``` thus ?thesis by simp ``` paulson@33533 ` 45` ```qed ``` paulson@33533 ` 46` hoelzl@38656 ` 47` ```lemma (in sigma_algebra) borel_measurable_vimage: ``` hoelzl@38656 ` 48` ``` fixes f :: "'a \ 'x::t2_space" ``` hoelzl@38656 ` 49` ``` assumes borel: "f \ borel_measurable M" ``` hoelzl@38656 ` 50` ``` shows "f -` {x} \ space M \ sets M" ``` hoelzl@38656 ` 51` ```proof (cases "x \ f ` space M") ``` hoelzl@38656 ` 52` ``` case True then obtain y where "x = f y" by auto ``` hoelzl@38656 ` 53` ``` from closed_sing[of "f y"] ``` hoelzl@38656 ` 54` ``` have "{f y} \ sets borel_space" by (rule borel_space_closed) ``` hoelzl@38656 ` 55` ``` with assms show ?thesis ``` hoelzl@38656 ` 56` ``` unfolding in_borel_measurable_borel_space `x = f y` by auto ``` hoelzl@38656 ` 57` ```next ``` hoelzl@38656 ` 58` ``` case False hence "f -` {x} \ space M = {}" by auto ``` hoelzl@38656 ` 59` ``` thus ?thesis by auto ``` paulson@33533 ` 60` ```qed ``` paulson@33533 ` 61` hoelzl@38656 ` 62` ```lemma (in sigma_algebra) borel_measurableI: ``` hoelzl@38656 ` 63` ``` fixes f :: "'a \ 'x\topological_space" ``` hoelzl@38656 ` 64` ``` assumes "\S. open S \ f -` S \ space M \ sets M" ``` hoelzl@38656 ` 65` ``` shows "f \ borel_measurable M" ``` hoelzl@38656 ` 66` ``` unfolding borel_space_def ``` hoelzl@38656 ` 67` ```proof (rule measurable_sigma) ``` hoelzl@38656 ` 68` ``` fix S :: "'x set" assume "S \ open" thus "f -` S \ space M \ sets M" ``` hoelzl@38656 ` 69` ``` using assms[of S] by (simp add: mem_def) ``` hoelzl@38656 ` 70` ```qed simp_all ``` paulson@33533 ` 71` hoelzl@38656 ` 72` ```lemma borel_space_singleton[simp, intro]: ``` hoelzl@38656 ` 73` ``` fixes x :: "'a::t1_space" ``` hoelzl@38656 ` 74` ``` shows "A \ sets borel_space \ insert x A \ sets borel_space" ``` hoelzl@38656 ` 75` ``` proof (rule borel_space.insert_in_sets) ``` hoelzl@38656 ` 76` ``` show "{x} \ sets borel_space" ``` hoelzl@38656 ` 77` ``` using closed_sing[of x] by (rule borel_space_closed) ``` hoelzl@38656 ` 78` ``` qed simp ``` hoelzl@38656 ` 79` hoelzl@38656 ` 80` ```lemma (in sigma_algebra) borel_measurable_const[simp, intro]: ``` hoelzl@38656 ` 81` ``` "(\x. c) \ borel_measurable M" ``` hoelzl@38656 ` 82` ``` by (auto intro!: measurable_const) ``` paulson@33533 ` 83` hoelzl@38656 ` 84` ```lemma (in sigma_algebra) borel_measurable_indicator: ``` hoelzl@38656 ` 85` ``` assumes A: "A \ sets M" ``` hoelzl@38656 ` 86` ``` shows "indicator A \ borel_measurable M" ``` hoelzl@38656 ` 87` ``` unfolding indicator_def_raw using A ``` hoelzl@38656 ` 88` ``` by (auto intro!: measurable_If_set borel_measurable_const) ``` paulson@33533 ` 89` hoelzl@38656 ` 90` ```lemma borel_measurable_translate: ``` hoelzl@38656 ` 91` ``` assumes "A \ sets borel_space" and trans: "\B. open B \ f -` B \ sets borel_space" ``` hoelzl@38656 ` 92` ``` shows "f -` A \ sets borel_space" ``` hoelzl@38656 ` 93` ```proof - ``` hoelzl@38656 ` 94` ``` have "A \ sigma_sets UNIV open" using assms ``` hoelzl@38656 ` 95` ``` by (simp add: borel_space_def sigma_def) ``` hoelzl@38656 ` 96` ``` thus ?thesis ``` hoelzl@38656 ` 97` ``` proof (induct rule: sigma_sets.induct) ``` hoelzl@38656 ` 98` ``` case (Basic a) thus ?case using trans[of a] by (simp add: mem_def) ``` hoelzl@38656 ` 99` ``` next ``` hoelzl@38656 ` 100` ``` case (Compl a) ``` hoelzl@38656 ` 101` ``` moreover have "UNIV \ sets borel_space" ``` hoelzl@38656 ` 102` ``` by (metis borel_space.top borel_space_def_raw mem_def space_sigma) ``` hoelzl@38656 ` 103` ``` ultimately show ?case ``` hoelzl@38656 ` 104` ``` by (auto simp: vimage_Diff borel_space.Diff) ``` hoelzl@38656 ` 105` ``` qed (auto simp add: vimage_UN) ``` paulson@33533 ` 106` ```qed ``` paulson@33533 ` 107` hoelzl@38656 ` 108` ```section "Borel spaces on euclidean spaces" ``` hoelzl@38656 ` 109` hoelzl@38656 ` 110` ```lemma lessThan_borel[simp, intro]: ``` hoelzl@38656 ` 111` ``` fixes a :: "'a\ordered_euclidean_space" ``` hoelzl@38656 ` 112` ``` shows "{..< a} \ sets borel_space" ``` hoelzl@38656 ` 113` ``` by (blast intro: borel_space_open) ``` hoelzl@38656 ` 114` hoelzl@38656 ` 115` ```lemma greaterThan_borel[simp, intro]: ``` hoelzl@38656 ` 116` ``` fixes a :: "'a\ordered_euclidean_space" ``` hoelzl@38656 ` 117` ``` shows "{a <..} \ sets borel_space" ``` hoelzl@38656 ` 118` ``` by (blast intro: borel_space_open) ``` hoelzl@38656 ` 119` hoelzl@38656 ` 120` ```lemma greaterThanLessThan_borel[simp, intro]: ``` hoelzl@38656 ` 121` ``` fixes a b :: "'a\ordered_euclidean_space" ``` hoelzl@38656 ` 122` ``` shows "{a<.. sets borel_space" ``` hoelzl@38656 ` 123` ``` by (blast intro: borel_space_open) ``` hoelzl@38656 ` 124` hoelzl@38656 ` 125` ```lemma atMost_borel[simp, intro]: ``` hoelzl@38656 ` 126` ``` fixes a :: "'a\ordered_euclidean_space" ``` hoelzl@38656 ` 127` ``` shows "{..a} \ sets borel_space" ``` hoelzl@38656 ` 128` ``` by (blast intro: borel_space_closed) ``` hoelzl@38656 ` 129` hoelzl@38656 ` 130` ```lemma atLeast_borel[simp, intro]: ``` hoelzl@38656 ` 131` ``` fixes a :: "'a\ordered_euclidean_space" ``` hoelzl@38656 ` 132` ``` shows "{a..} \ sets borel_space" ``` hoelzl@38656 ` 133` ``` by (blast intro: borel_space_closed) ``` hoelzl@38656 ` 134` hoelzl@38656 ` 135` ```lemma atLeastAtMost_borel[simp, intro]: ``` hoelzl@38656 ` 136` ``` fixes a b :: "'a\ordered_euclidean_space" ``` hoelzl@38656 ` 137` ``` shows "{a..b} \ sets borel_space" ``` hoelzl@38656 ` 138` ``` by (blast intro: borel_space_closed) ``` paulson@33533 ` 139` hoelzl@38656 ` 140` ```lemma greaterThanAtMost_borel[simp, intro]: ``` hoelzl@38656 ` 141` ``` fixes a b :: "'a\ordered_euclidean_space" ``` hoelzl@38656 ` 142` ``` shows "{a<..b} \ sets borel_space" ``` hoelzl@38656 ` 143` ``` unfolding greaterThanAtMost_def by blast ``` hoelzl@38656 ` 144` hoelzl@38656 ` 145` ```lemma atLeastLessThan_borel[simp, intro]: ``` hoelzl@38656 ` 146` ``` fixes a b :: "'a\ordered_euclidean_space" ``` hoelzl@38656 ` 147` ``` shows "{a.. sets borel_space" ``` hoelzl@38656 ` 148` ``` unfolding atLeastLessThan_def by blast ``` hoelzl@38656 ` 149` hoelzl@38656 ` 150` ```lemma hafspace_less_borel[simp, intro]: ``` hoelzl@38656 ` 151` ``` fixes a :: real ``` hoelzl@38656 ` 152` ``` shows "{x::'a::euclidean_space. a < x \$\$ i} \ sets borel_space" ``` hoelzl@38656 ` 153` ``` by (auto intro!: borel_space_open open_halfspace_component_gt) ``` paulson@33533 ` 154` hoelzl@38656 ` 155` ```lemma hafspace_greater_borel[simp, intro]: ``` hoelzl@38656 ` 156` ``` fixes a :: real ``` hoelzl@38656 ` 157` ``` shows "{x::'a::euclidean_space. x \$\$ i < a} \ sets borel_space" ``` hoelzl@38656 ` 158` ``` by (auto intro!: borel_space_open open_halfspace_component_lt) ``` paulson@33533 ` 159` hoelzl@38656 ` 160` ```lemma hafspace_less_eq_borel[simp, intro]: ``` hoelzl@38656 ` 161` ``` fixes a :: real ``` hoelzl@38656 ` 162` ``` shows "{x::'a::euclidean_space. a \ x \$\$ i} \ sets borel_space" ``` hoelzl@38656 ` 163` ``` by (auto intro!: borel_space_closed closed_halfspace_component_ge) ``` paulson@33533 ` 164` hoelzl@38656 ` 165` ```lemma hafspace_greater_eq_borel[simp, intro]: ``` hoelzl@38656 ` 166` ``` fixes a :: real ``` hoelzl@38656 ` 167` ``` shows "{x::'a::euclidean_space. x \$\$ i \ a} \ sets borel_space" ``` hoelzl@38656 ` 168` ``` by (auto intro!: borel_space_closed closed_halfspace_component_le) ``` paulson@33533 ` 169` hoelzl@38656 ` 170` ```lemma (in sigma_algebra) borel_measurable_less[simp, intro]: ``` hoelzl@38656 ` 171` ``` fixes f :: "'a \ real" ``` paulson@33533 ` 172` ``` assumes f: "f \ borel_measurable M" ``` paulson@33533 ` 173` ``` assumes g: "g \ borel_measurable M" ``` paulson@33533 ` 174` ``` shows "{w \ space M. f w < g w} \ sets M" ``` paulson@33533 ` 175` ```proof - ``` paulson@33533 ` 176` ``` have "{w \ space M. f w < g w} = ``` hoelzl@38656 ` 177` ``` (\r. (f -` {..< of_rat r} \ space M) \ (g -` {of_rat r <..} \ space M))" ``` hoelzl@38656 ` 178` ``` using Rats_dense_in_real by (auto simp add: Rats_def) ``` hoelzl@38656 ` 179` ``` then show ?thesis using f g ``` hoelzl@38656 ` 180` ``` by simp (blast intro: measurable_sets) ``` paulson@33533 ` 181` ```qed ``` hoelzl@38656 ` 182` hoelzl@38656 ` 183` ```lemma (in sigma_algebra) borel_measurable_le[simp, intro]: ``` hoelzl@38656 ` 184` ``` fixes f :: "'a \ real" ``` paulson@33533 ` 185` ``` assumes f: "f \ borel_measurable M" ``` paulson@33533 ` 186` ``` assumes g: "g \ borel_measurable M" ``` paulson@33533 ` 187` ``` shows "{w \ space M. f w \ g w} \ sets M" ``` paulson@33533 ` 188` ```proof - ``` hoelzl@38656 ` 189` ``` have "{w \ space M. f w \ g w} = space M - {w \ space M. g w < f w}" ``` hoelzl@38656 ` 190` ``` by auto ``` hoelzl@38656 ` 191` ``` thus ?thesis using f g ``` hoelzl@38656 ` 192` ``` by simp blast ``` paulson@33533 ` 193` ```qed ``` paulson@33533 ` 194` hoelzl@38656 ` 195` ```lemma (in sigma_algebra) borel_measurable_eq[simp, intro]: ``` hoelzl@38656 ` 196` ``` fixes f :: "'a \ real" ``` paulson@33533 ` 197` ``` assumes f: "f \ borel_measurable M" ``` paulson@33533 ` 198` ``` assumes g: "g \ borel_measurable M" ``` paulson@33533 ` 199` ``` shows "{w \ space M. f w = g w} \ sets M" ``` paulson@33533 ` 200` ```proof - ``` paulson@33533 ` 201` ``` have "{w \ space M. f w = g w} = ``` wenzelm@33536 ` 202` ``` {w \ space M. f w \ g w} \ {w \ space M. g w \ f w}" ``` paulson@33533 ` 203` ``` by auto ``` hoelzl@38656 ` 204` ``` thus ?thesis using f g by auto ``` paulson@33533 ` 205` ```qed ``` paulson@33533 ` 206` hoelzl@38656 ` 207` ```lemma (in sigma_algebra) borel_measurable_neq[simp, intro]: ``` hoelzl@38656 ` 208` ``` fixes f :: "'a \ real" ``` paulson@33533 ` 209` ``` assumes f: "f \ borel_measurable M" ``` paulson@33533 ` 210` ``` assumes g: "g \ borel_measurable M" ``` paulson@33533 ` 211` ``` shows "{w \ space M. f w \ g w} \ sets M" ``` paulson@33533 ` 212` ```proof - ``` paulson@33533 ` 213` ``` have "{w \ space M. f w \ g w} = space M - {w \ space M. f w = g w}" ``` paulson@33533 ` 214` ``` by auto ``` hoelzl@38656 ` 215` ``` thus ?thesis using f g by auto ``` hoelzl@38656 ` 216` ```qed ``` hoelzl@38656 ` 217` hoelzl@38656 ` 218` ```subsection "Borel space equals sigma algebras over intervals" ``` hoelzl@38656 ` 219` hoelzl@38656 ` 220` ```lemma rational_boxes: ``` hoelzl@38656 ` 221` ``` fixes x :: "'a\ordered_euclidean_space" ``` hoelzl@38656 ` 222` ``` assumes "0 < e" ``` hoelzl@38656 ` 223` ``` shows "\a b. (\i. a \$\$ i \ \) \ (\i. b \$\$ i \ \) \ x \ {a <..< b} \ {a <..< b} \ ball x e" ``` hoelzl@38656 ` 224` ```proof - ``` hoelzl@38656 ` 225` ``` def e' \ "e / (2 * sqrt (real (DIM ('a))))" ``` hoelzl@38656 ` 226` ``` then have e: "0 < e'" using assms by (auto intro!: divide_pos_pos) ``` hoelzl@38656 ` 227` ``` have "\i. \y. y \ \ \ y < x \$\$ i \ x \$\$ i - y < e'" (is "\i. ?th i") ``` hoelzl@38656 ` 228` ``` proof ``` hoelzl@38656 ` 229` ``` fix i from Rats_dense_in_real[of "x \$\$ i - e'" "x \$\$ i"] e ``` hoelzl@38656 ` 230` ``` show "?th i" by auto ``` hoelzl@38656 ` 231` ``` qed ``` hoelzl@38656 ` 232` ``` from choice[OF this] guess a .. note a = this ``` hoelzl@38656 ` 233` ``` have "\i. \y. y \ \ \ x \$\$ i < y \ y - x \$\$ i < e'" (is "\i. ?th i") ``` hoelzl@38656 ` 234` ``` proof ``` hoelzl@38656 ` 235` ``` fix i from Rats_dense_in_real[of "x \$\$ i" "x \$\$ i + e'"] e ``` hoelzl@38656 ` 236` ``` show "?th i" by auto ``` hoelzl@38656 ` 237` ``` qed ``` hoelzl@38656 ` 238` ``` from choice[OF this] guess b .. note b = this ``` hoelzl@38656 ` 239` ``` { fix y :: 'a assume *: "Chi a < y" "y < Chi b" ``` hoelzl@38656 ` 240` ``` have "dist x y = sqrt (\i)" ``` hoelzl@38656 ` 241` ``` unfolding setL2_def[symmetric] by (rule euclidean_dist_l2) ``` hoelzl@38656 ` 242` ``` also have "\ < sqrt (\i {.. y\$\$i < b i" using * i eucl_less[where 'a='a] by auto ``` hoelzl@38656 ` 246` ``` moreover have "a i < x\$\$i" "x\$\$i - a i < e'" using a by auto ``` hoelzl@38656 ` 247` ``` moreover have "x\$\$i < b i" "b i - x\$\$i < e'" using b by auto ``` hoelzl@38656 ` 248` ``` ultimately have "\x\$\$i - y\$\$i\ < 2 * e'" by auto ``` hoelzl@38656 ` 249` ``` then have "dist (x \$\$ i) (y \$\$ i) < e/sqrt (real (DIM('a)))" ``` hoelzl@38656 ` 250` ``` unfolding e'_def by (auto simp: dist_real_def) ``` hoelzl@38656 ` 251` ``` then have "(dist (x \$\$ i) (y \$\$ i))\ < (e/sqrt (real (DIM('a))))\" ``` hoelzl@38656 ` 252` ``` by (rule power_strict_mono) auto ``` hoelzl@38656 ` 253` ``` then show "(dist (x \$\$ i) (y \$\$ i))\ < e\ / real DIM('a)" ``` hoelzl@38656 ` 254` ``` by (simp add: power_divide) ``` hoelzl@38656 ` 255` ``` qed auto ``` hoelzl@38656 ` 256` ``` also have "\ = e" using `0 < e` by (simp add: real_eq_of_nat DIM_positive) ``` hoelzl@38656 ` 257` ``` finally have "dist x y < e" . } ``` hoelzl@38656 ` 258` ``` with a b show ?thesis ``` hoelzl@38656 ` 259` ``` apply (rule_tac exI[of _ "Chi a"]) ``` hoelzl@38656 ` 260` ``` apply (rule_tac exI[of _ "Chi b"]) ``` hoelzl@38656 ` 261` ``` using eucl_less[where 'a='a] by auto ``` hoelzl@38656 ` 262` ```qed ``` hoelzl@38656 ` 263` hoelzl@38656 ` 264` ```lemma ex_rat_list: ``` hoelzl@38656 ` 265` ``` fixes x :: "'a\ordered_euclidean_space" ``` hoelzl@38656 ` 266` ``` assumes "\ i. x \$\$ i \ \" ``` hoelzl@38656 ` 267` ``` shows "\ r. length r = DIM('a) \ (\ i < DIM('a). of_rat (r ! i) = x \$\$ i)" ``` hoelzl@38656 ` 268` ```proof - ``` hoelzl@38656 ` 269` ``` have "\i. \r. x \$\$ i = of_rat r" using assms unfolding Rats_def by blast ``` hoelzl@38656 ` 270` ``` from choice[OF this] guess r .. ``` hoelzl@38656 ` 271` ``` then show ?thesis by (auto intro!: exI[of _ "map r [0 ..< DIM('a)]"]) ``` hoelzl@38656 ` 272` ```qed ``` hoelzl@38656 ` 273` hoelzl@38656 ` 274` ```lemma open_UNION: ``` hoelzl@38656 ` 275` ``` fixes M :: "'a\ordered_euclidean_space set" ``` hoelzl@38656 ` 276` ``` assumes "open M" ``` hoelzl@38656 ` 277` ``` shows "M = UNION {(a, b) | a b. {Chi (of_rat \ op ! a) <..< Chi (of_rat \ op ! b)} \ M} ``` hoelzl@38656 ` 278` ``` (\ (a, b). {Chi (of_rat \ op ! a) <..< Chi (of_rat \ op ! b)})" ``` hoelzl@38656 ` 279` ``` (is "M = UNION ?idx ?box") ``` hoelzl@38656 ` 280` ```proof safe ``` hoelzl@38656 ` 281` ``` fix x assume "x \ M" ``` hoelzl@38656 ` 282` ``` obtain e where e: "e > 0" "ball x e \ M" ``` hoelzl@38656 ` 283` ``` using openE[OF assms `x \ M`] by auto ``` hoelzl@38656 ` 284` ``` then obtain a b where ab: "x \ {a <..< b}" "\i. a \$\$ i \ \" "\i. b \$\$ i \ \" "{a <..< b} \ ball x e" ``` hoelzl@38656 ` 285` ``` using rational_boxes[OF e(1)] by blast ``` hoelzl@38656 ` 286` ``` then obtain p q where pq: "length p = DIM ('a)" ``` hoelzl@38656 ` 287` ``` "length q = DIM ('a)" ``` hoelzl@38656 ` 288` ``` "\ i < DIM ('a). of_rat (p ! i) = a \$\$ i \ of_rat (q ! i) = b \$\$ i" ``` hoelzl@38656 ` 289` ``` using ex_rat_list[OF ab(2)] ex_rat_list[OF ab(3)] by blast ``` hoelzl@38656 ` 290` ``` hence p: "Chi (of_rat \ op ! p) = a" ``` hoelzl@38656 ` 291` ``` using euclidean_eq[of "Chi (of_rat \ op ! p)" a] ``` hoelzl@38656 ` 292` ``` unfolding o_def by auto ``` hoelzl@38656 ` 293` ``` from pq have q: "Chi (of_rat \ op ! q) = b" ``` hoelzl@38656 ` 294` ``` using euclidean_eq[of "Chi (of_rat \ op ! q)" b] ``` hoelzl@38656 ` 295` ``` unfolding o_def by auto ``` hoelzl@38656 ` 296` ``` have "x \ ?box (p, q)" ``` hoelzl@38656 ` 297` ``` using p q ab by auto ``` hoelzl@38656 ` 298` ``` thus "x \ UNION ?idx ?box" using ab e p q exI[of _ p] exI[of _ q] by auto ``` hoelzl@38656 ` 299` ```qed auto ``` hoelzl@38656 ` 300` hoelzl@38656 ` 301` ```lemma halfspace_span_open: ``` hoelzl@38656 ` 302` ``` "sets (sigma UNIV (range (\ (a, i). {x\'a\ordered_euclidean_space. x \$\$ i < a}))) ``` hoelzl@38656 ` 303` ``` \ sets borel_space" ``` hoelzl@38656 ` 304` ``` by (auto intro!: borel_space.sigma_sets_subset[simplified] borel_space_open ``` hoelzl@38656 ` 305` ``` open_halfspace_component_lt simp: sets_sigma) ``` hoelzl@38656 ` 306` hoelzl@38656 ` 307` ```lemma halfspace_lt_in_halfspace: ``` hoelzl@38656 ` 308` ``` "{x\'a. x \$\$ i < a} \ sets (sigma UNIV (range (\ (a, i). {x\'a\ordered_euclidean_space. x \$\$ i < a})))" ``` hoelzl@38656 ` 309` ``` unfolding sets_sigma by (rule sigma_sets.Basic) auto ``` hoelzl@38656 ` 310` hoelzl@38656 ` 311` ```lemma halfspace_gt_in_halfspace: ``` hoelzl@38656 ` 312` ``` "{x\'a. a < x \$\$ i} \ sets (sigma UNIV (range (\ (a, i). {x\'a\ordered_euclidean_space. x \$\$ i < a})))" ``` hoelzl@38656 ` 313` ``` (is "?set \ sets ?SIGMA") ``` hoelzl@38656 ` 314` ```proof - ``` hoelzl@38656 ` 315` ``` interpret sigma_algebra ?SIGMA by (rule sigma_algebra_sigma) simp ``` hoelzl@38656 ` 316` ``` have *: "?set = (\n. space ?SIGMA - {x\'a. x \$\$ i < a + 1 / real (Suc n)})" ``` hoelzl@38656 ` 317` ``` proof (safe, simp_all add: not_less) ``` hoelzl@38656 ` 318` ``` fix x assume "a < x \$\$ i" ``` hoelzl@38656 ` 319` ``` with reals_Archimedean[of "x \$\$ i - a"] ``` hoelzl@38656 ` 320` ``` obtain n where "a + 1 / real (Suc n) < x \$\$ i" ``` hoelzl@38656 ` 321` ``` by (auto simp: inverse_eq_divide field_simps) ``` hoelzl@38656 ` 322` ``` then show "\n. a + 1 / real (Suc n) \ x \$\$ i" ``` hoelzl@38656 ` 323` ``` by (blast intro: less_imp_le) ``` hoelzl@38656 ` 324` ``` next ``` hoelzl@38656 ` 325` ``` fix x n ``` hoelzl@38656 ` 326` ``` have "a < a + 1 / real (Suc n)" by auto ``` hoelzl@38656 ` 327` ``` also assume "\ \ x" ``` hoelzl@38656 ` 328` ``` finally show "a < x" . ``` hoelzl@38656 ` 329` ``` qed ``` hoelzl@38656 ` 330` ``` show "?set \ sets ?SIGMA" unfolding * ``` hoelzl@38656 ` 331` ``` by (safe intro!: countable_UN Diff halfspace_lt_in_halfspace) ``` paulson@33533 ` 332` ```qed ``` paulson@33533 ` 333` hoelzl@38656 ` 334` ```lemma (in sigma_algebra) sets_sigma_subset: ``` hoelzl@38656 ` 335` ``` assumes "A = space M" ``` hoelzl@38656 ` 336` ``` assumes "B \ sets M" ``` hoelzl@38656 ` 337` ``` shows "sets (sigma A B) \ sets M" ``` hoelzl@38656 ` 338` ``` by (unfold assms sets_sigma, rule sigma_sets_subset, rule assms) ``` hoelzl@38656 ` 339` hoelzl@38656 ` 340` ```lemma open_span_halfspace: ``` hoelzl@38656 ` 341` ``` "sets borel_space \ sets (sigma UNIV (range (\ (a, i). {x::'a::ordered_euclidean_space. x \$\$ i < a})))" ``` hoelzl@38656 ` 342` ``` (is "_ \ sets ?SIGMA") ``` hoelzl@38656 ` 343` ```proof (unfold borel_space_def, rule sigma_algebra.sets_sigma_subset, safe) ``` hoelzl@38656 ` 344` ``` show "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) simp ``` hoelzl@38656 ` 345` ``` then interpret sigma_algebra ?SIGMA . ``` hoelzl@38656 ` 346` ``` fix S :: "'a set" assume "S \ open" then have "open S" unfolding mem_def . ``` hoelzl@38656 ` 347` ``` from open_UNION[OF this] ``` hoelzl@38656 ` 348` ``` obtain I where *: "S = ``` hoelzl@38656 ` 349` ``` (\(a, b)\I. ``` hoelzl@38656 ` 350` ``` (\ i op ! a)::'a) \$\$ i < x \$\$ i}) \ ``` hoelzl@38656 ` 351` ``` (\ i op ! b)::'a) \$\$ i}))" ``` hoelzl@38656 ` 352` ``` unfolding greaterThanLessThan_def ``` hoelzl@38656 ` 353` ``` unfolding eucl_greaterThan_eq_halfspaces[where 'a='a] ``` hoelzl@38656 ` 354` ``` unfolding eucl_lessThan_eq_halfspaces[where 'a='a] ``` hoelzl@38656 ` 355` ``` by blast ``` hoelzl@38656 ` 356` ``` show "S \ sets ?SIGMA" ``` hoelzl@38656 ` 357` ``` unfolding * ``` hoelzl@38656 ` 358` ``` by (auto intro!: countable_UN Int countable_INT halfspace_lt_in_halfspace halfspace_gt_in_halfspace) ``` hoelzl@38656 ` 359` ```qed auto ``` hoelzl@38656 ` 360` hoelzl@38656 ` 361` ```lemma halfspace_span_halfspace_le: ``` hoelzl@38656 ` 362` ``` "sets (sigma UNIV (range (\ (a, i). {x\'a\ordered_euclidean_space. x \$\$ i < a}))) \ ``` hoelzl@38656 ` 363` ``` sets (sigma UNIV (range (\ (a, i). {x. x \$\$ i \ a})))" ``` hoelzl@38656 ` 364` ``` (is "_ \ sets ?SIGMA") ``` hoelzl@38656 ` 365` ```proof (rule sigma_algebra.sets_sigma_subset, safe) ``` hoelzl@38656 ` 366` ``` show "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto ``` hoelzl@38656 ` 367` ``` then interpret sigma_algebra ?SIGMA . ``` hoelzl@38656 ` 368` ``` fix a i ``` hoelzl@38656 ` 369` ``` have *: "{x::'a. x\$\$i < a} = (\n. {x. x\$\$i \ a - 1/real (Suc n)})" ``` hoelzl@38656 ` 370` ``` proof (safe, simp_all) ``` hoelzl@38656 ` 371` ``` fix x::'a assume *: "x\$\$i < a" ``` hoelzl@38656 ` 372` ``` with reals_Archimedean[of "a - x\$\$i"] ``` hoelzl@38656 ` 373` ``` obtain n where "x \$\$ i < a - 1 / (real (Suc n))" ``` hoelzl@38656 ` 374` ``` by (auto simp: field_simps inverse_eq_divide) ``` hoelzl@38656 ` 375` ``` then show "\n. x \$\$ i \ a - 1 / (real (Suc n))" ``` hoelzl@38656 ` 376` ``` by (blast intro: less_imp_le) ``` hoelzl@38656 ` 377` ``` next ``` hoelzl@38656 ` 378` ``` fix x::'a and n ``` hoelzl@38656 ` 379` ``` assume "x\$\$i \ a - 1 / real (Suc n)" ``` hoelzl@38656 ` 380` ``` also have "\ < a" by auto ``` hoelzl@38656 ` 381` ``` finally show "x\$\$i < a" . ``` hoelzl@38656 ` 382` ``` qed ``` hoelzl@38656 ` 383` ``` show "{x. x\$\$i < a} \ sets ?SIGMA" unfolding * ``` hoelzl@38656 ` 384` ``` by (safe intro!: countable_UN) ``` hoelzl@38656 ` 385` ``` (auto simp: sets_sigma intro!: sigma_sets.Basic) ``` hoelzl@38656 ` 386` ```qed auto ``` hoelzl@38656 ` 387` hoelzl@38656 ` 388` ```lemma halfspace_span_halfspace_ge: ``` hoelzl@38656 ` 389` ``` "sets (sigma UNIV (range (\ (a, i). {x\'a\ordered_euclidean_space. x \$\$ i < a}))) \ ``` hoelzl@38656 ` 390` ``` sets (sigma UNIV (range (\ (a, i). {x. a \ x \$\$ i})))" ``` hoelzl@38656 ` 391` ``` (is "_ \ sets ?SIGMA") ``` hoelzl@38656 ` 392` ```proof (rule sigma_algebra.sets_sigma_subset, safe) ``` hoelzl@38656 ` 393` ``` show "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto ``` hoelzl@38656 ` 394` ``` then interpret sigma_algebra ?SIGMA . ``` hoelzl@38656 ` 395` ``` fix a i have *: "{x::'a. x\$\$i < a} = space ?SIGMA - {x::'a. a \ x\$\$i}" by auto ``` hoelzl@38656 ` 396` ``` show "{x. x\$\$i < a} \ sets ?SIGMA" unfolding * ``` hoelzl@38656 ` 397` ``` by (safe intro!: Diff) ``` hoelzl@38656 ` 398` ``` (auto simp: sets_sigma intro!: sigma_sets.Basic) ``` hoelzl@38656 ` 399` ```qed auto ``` hoelzl@38656 ` 400` hoelzl@38656 ` 401` ```lemma halfspace_le_span_halfspace_gt: ``` hoelzl@38656 ` 402` ``` "sets (sigma UNIV (range (\ (a, i). {x\'a\ordered_euclidean_space. x \$\$ i \ a}))) \ ``` hoelzl@38656 ` 403` ``` sets (sigma UNIV (range (\ (a, i). {x. a < x \$\$ i})))" ``` hoelzl@38656 ` 404` ``` (is "_ \ sets ?SIGMA") ``` hoelzl@38656 ` 405` ```proof (rule sigma_algebra.sets_sigma_subset, safe) ``` hoelzl@38656 ` 406` ``` show "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto ``` hoelzl@38656 ` 407` ``` then interpret sigma_algebra ?SIGMA . ``` hoelzl@38656 ` 408` ``` fix a i have *: "{x::'a. x\$\$i \ a} = space ?SIGMA - {x::'a. a < x\$\$i}" by auto ``` hoelzl@38656 ` 409` ``` show "{x. x\$\$i \ a} \ sets ?SIGMA" unfolding * ``` hoelzl@38656 ` 410` ``` by (safe intro!: Diff) ``` hoelzl@38656 ` 411` ``` (auto simp: sets_sigma intro!: sigma_sets.Basic) ``` hoelzl@38656 ` 412` ```qed auto ``` hoelzl@38656 ` 413` hoelzl@38656 ` 414` ```lemma halfspace_le_span_atMost: ``` hoelzl@38656 ` 415` ``` "sets (sigma UNIV (range (\ (a, i). {x\'a\ordered_euclidean_space. x \$\$ i \ a}))) \ ``` hoelzl@38656 ` 416` ``` sets (sigma UNIV (range (\a. {..a\'a\ordered_euclidean_space})))" ``` hoelzl@38656 ` 417` ``` (is "_ \ sets ?SIGMA") ``` hoelzl@38656 ` 418` ```proof (rule sigma_algebra.sets_sigma_subset, safe) ``` hoelzl@38656 ` 419` ``` show "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto ``` hoelzl@38656 ` 420` ``` then interpret sigma_algebra ?SIGMA . ``` hoelzl@38656 ` 421` ``` fix a i ``` hoelzl@38656 ` 422` ``` show "{x. x\$\$i \ a} \ sets ?SIGMA" ``` hoelzl@38656 ` 423` ``` proof cases ``` hoelzl@38656 ` 424` ``` assume "i < DIM('a)" ``` hoelzl@38656 ` 425` ``` then have *: "{x::'a. x\$\$i \ a} = (\k::nat. {.. (\\ n. if n = i then a else real k)})" ``` hoelzl@38656 ` 426` ``` proof (safe, simp_all add: eucl_le[where 'a='a] split: split_if_asm) ``` hoelzl@38656 ` 427` ``` fix x ``` hoelzl@38656 ` 428` ``` from real_arch_simple[of "Max ((\i. x\$\$i)`{..i. i < DIM('a) \ x\$\$i \ real k" ``` hoelzl@38656 ` 430` ``` by (subst (asm) Max_le_iff) auto ``` hoelzl@38656 ` 431` ``` then show "\k::nat. \ia. ia \ i \ ia < DIM('a) \ x \$\$ ia \ real k" ``` hoelzl@38656 ` 432` ``` by (auto intro!: exI[of _ k]) ``` hoelzl@38656 ` 433` ``` qed ``` hoelzl@38656 ` 434` ``` show "{x. x\$\$i \ a} \ sets ?SIGMA" unfolding * ``` hoelzl@38656 ` 435` ``` by (safe intro!: countable_UN) ``` hoelzl@38656 ` 436` ``` (auto simp: sets_sigma intro!: sigma_sets.Basic) ``` hoelzl@38656 ` 437` ``` next ``` hoelzl@38656 ` 438` ``` assume "\ i < DIM('a)" ``` hoelzl@38656 ` 439` ``` then show "{x. x\$\$i \ a} \ sets ?SIGMA" ``` hoelzl@38656 ` 440` ``` using top by auto ``` hoelzl@38656 ` 441` ``` qed ``` hoelzl@38656 ` 442` ```qed auto ``` hoelzl@38656 ` 443` hoelzl@38656 ` 444` ```lemma halfspace_le_span_greaterThan: ``` hoelzl@38656 ` 445` ``` "sets (sigma UNIV (range (\ (a, i). {x\'a\ordered_euclidean_space. x \$\$ i \ a}))) \ ``` hoelzl@38656 ` 446` ``` sets (sigma UNIV (range (\a. {a<..})))" ``` hoelzl@38656 ` 447` ``` (is "_ \ sets ?SIGMA") ``` hoelzl@38656 ` 448` ```proof (rule sigma_algebra.sets_sigma_subset, safe) ``` hoelzl@38656 ` 449` ``` show "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto ``` hoelzl@38656 ` 450` ``` then interpret sigma_algebra ?SIGMA . ``` hoelzl@38656 ` 451` ``` fix a i ``` hoelzl@38656 ` 452` ``` show "{x. x\$\$i \ a} \ sets ?SIGMA" ``` hoelzl@38656 ` 453` ``` proof cases ``` hoelzl@38656 ` 454` ``` assume "i < DIM('a)" ``` hoelzl@38656 ` 455` ``` have "{x::'a. x\$\$i \ a} = space ?SIGMA - {x::'a. a < x\$\$i}" by auto ``` hoelzl@38656 ` 456` ``` 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" ``` hoelzl@38656 ` 466` ``` by (auto intro!: exI[of _ k]) ``` hoelzl@38656 ` 467` ``` qed ``` hoelzl@38656 ` 468` ``` finally show "{x. x\$\$i \ a} \ sets ?SIGMA" ``` hoelzl@38656 ` 469` ``` apply (simp only:) ``` hoelzl@38656 ` 470` ``` apply (safe intro!: countable_UN Diff) ``` hoelzl@38656 ` 471` ``` by (auto simp: sets_sigma intro!: sigma_sets.Basic) ``` hoelzl@38656 ` 472` ``` next ``` hoelzl@38656 ` 473` ``` assume "\ i < DIM('a)" ``` hoelzl@38656 ` 474` ``` then show "{x. x\$\$i \ a} \ sets ?SIGMA" ``` hoelzl@38656 ` 475` ``` using top by auto ``` hoelzl@38656 ` 476` ``` qed ``` hoelzl@38656 ` 477` ```qed auto ``` hoelzl@38656 ` 478` hoelzl@38656 ` 479` ```lemma atMost_span_atLeastAtMost: ``` hoelzl@38656 ` 480` ``` "sets (sigma UNIV (range (\a. {..a\'a\ordered_euclidean_space}))) \ ``` hoelzl@38656 ` 481` ``` sets (sigma UNIV (range (\(a,b). {a..b})))" ``` hoelzl@38656 ` 482` ``` (is "_ \ sets ?SIGMA") ``` hoelzl@38656 ` 483` ```proof (rule sigma_algebra.sets_sigma_subset, safe) ``` hoelzl@38656 ` 484` ``` show "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto ``` hoelzl@38656 ` 485` ``` then interpret sigma_algebra ?SIGMA . ``` hoelzl@38656 ` 486` ``` fix a::'a ``` hoelzl@38656 ` 487` ``` have *: "{..a} = (\n::nat. {- real n *\<^sub>R One .. a})" ``` hoelzl@38656 ` 488` ``` proof (safe, simp_all add: eucl_le[where 'a='a]) ``` hoelzl@38656 ` 489` ``` fix x ``` hoelzl@38656 ` 490` ``` from real_arch_simple[of "Max ((\i. - x\$\$i)`{.. real k" ``` hoelzl@38656 ` 494` ``` by (subst (asm) Max_le_iff) (auto simp: field_simps) ``` hoelzl@38656 ` 495` ``` then have "- real k \ x\$\$i" by simp } ``` hoelzl@38656 ` 496` ``` then show "\n::nat. \i x \$\$ i" ``` hoelzl@38656 ` 497` ``` by (auto intro!: exI[of _ k]) ``` hoelzl@38656 ` 498` ``` qed ``` hoelzl@38656 ` 499` ``` show "{..a} \ sets ?SIGMA" unfolding * ``` hoelzl@38656 ` 500` ``` by (safe intro!: countable_UN) ``` hoelzl@38656 ` 501` ``` (auto simp: sets_sigma intro!: sigma_sets.Basic) ``` hoelzl@38656 ` 502` ```qed auto ``` hoelzl@38656 ` 503` hoelzl@38656 ` 504` ```lemma borel_space_eq_greaterThanLessThan: ``` hoelzl@38656 ` 505` ``` "sets borel_space = sets (sigma UNIV (range (\ (a, b). {a <..< (b :: 'a \ ordered_euclidean_space)})))" ``` hoelzl@38656 ` 506` ``` (is "_ = sets ?SIGMA") ``` hoelzl@38656 ` 507` ```proof (rule antisym) ``` hoelzl@38656 ` 508` ``` show "sets ?SIGMA \ sets borel_space" ``` hoelzl@38656 ` 509` ``` by (rule borel_space.sets_sigma_subset) auto ``` hoelzl@38656 ` 510` ``` show "sets borel_space \ sets ?SIGMA" ``` hoelzl@38656 ` 511` ``` unfolding borel_space_def ``` hoelzl@38656 ` 512` ``` proof (rule sigma_algebra.sets_sigma_subset, safe) ``` hoelzl@38656 ` 513` ``` show "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto ``` hoelzl@38656 ` 514` ``` then interpret sigma_algebra ?SIGMA . ``` hoelzl@38656 ` 515` ``` fix M :: "'a set" assume "M \ open" ``` hoelzl@38656 ` 516` ``` then have "open M" by (simp add: mem_def) ``` hoelzl@38656 ` 517` ``` show "M \ sets ?SIGMA" ``` hoelzl@38656 ` 518` ``` apply (subst open_UNION[OF `open M`]) ``` hoelzl@38656 ` 519` ``` apply (safe intro!: countable_UN) ``` hoelzl@38656 ` 520` ``` by (auto simp add: sigma_def intro!: sigma_sets.Basic) ``` hoelzl@38656 ` 521` ``` qed auto ``` hoelzl@38656 ` 522` ```qed ``` hoelzl@38656 ` 523` hoelzl@38656 ` 524` ```lemma borel_space_eq_atMost: ``` hoelzl@38656 ` 525` ``` "sets borel_space = sets (sigma UNIV (range (\ a. {.. a::'a\ordered_euclidean_space})))" ``` hoelzl@38656 ` 526` ``` (is "_ = sets ?SIGMA") ``` hoelzl@38656 ` 527` ```proof (rule antisym) ``` hoelzl@38656 ` 528` ``` show "sets borel_space \ sets ?SIGMA" ``` hoelzl@38656 ` 529` ``` using halfspace_le_span_atMost halfspace_span_halfspace_le open_span_halfspace ``` hoelzl@38656 ` 530` ``` by auto ``` hoelzl@38656 ` 531` ``` show "sets ?SIGMA \ sets borel_space" ``` hoelzl@38656 ` 532` ``` by (rule borel_space.sets_sigma_subset) auto ``` hoelzl@38656 ` 533` ```qed ``` hoelzl@38656 ` 534` hoelzl@38656 ` 535` ```lemma borel_space_eq_atLeastAtMost: ``` hoelzl@38656 ` 536` ``` "sets borel_space = sets (sigma UNIV (range (\ (a :: 'a\ordered_euclidean_space, b). {a .. b})))" ``` hoelzl@38656 ` 537` ``` (is "_ = sets ?SIGMA") ``` hoelzl@38656 ` 538` ```proof (rule antisym) ``` hoelzl@38656 ` 539` ``` show "sets borel_space \ sets ?SIGMA" ``` hoelzl@38656 ` 540` ``` using atMost_span_atLeastAtMost halfspace_le_span_atMost ``` hoelzl@38656 ` 541` ``` halfspace_span_halfspace_le open_span_halfspace ``` hoelzl@38656 ` 542` ``` by auto ``` hoelzl@38656 ` 543` ``` show "sets ?SIGMA \ sets borel_space" ``` hoelzl@38656 ` 544` ``` by (rule borel_space.sets_sigma_subset) auto ``` hoelzl@38656 ` 545` ```qed ``` hoelzl@38656 ` 546` hoelzl@38656 ` 547` ```lemma borel_space_eq_greaterThan: ``` hoelzl@38656 ` 548` ``` "sets borel_space = sets (sigma UNIV (range (\ (a :: 'a\ordered_euclidean_space). {a <..})))" ``` hoelzl@38656 ` 549` ``` (is "_ = sets ?SIGMA") ``` hoelzl@38656 ` 550` ```proof (rule antisym) ``` hoelzl@38656 ` 551` ``` show "sets borel_space \ sets ?SIGMA" ``` hoelzl@38656 ` 552` ``` using halfspace_le_span_greaterThan ``` hoelzl@38656 ` 553` ``` halfspace_span_halfspace_le open_span_halfspace ``` hoelzl@38656 ` 554` ``` by auto ``` hoelzl@38656 ` 555` ``` show "sets ?SIGMA \ sets borel_space" ``` hoelzl@38656 ` 556` ``` by (rule borel_space.sets_sigma_subset) auto ``` hoelzl@38656 ` 557` ```qed ``` hoelzl@38656 ` 558` hoelzl@38656 ` 559` ```lemma borel_space_eq_halfspace_le: ``` hoelzl@38656 ` 560` ``` "sets borel_space = sets (sigma UNIV (range (\ (a, i). {x::'a::ordered_euclidean_space. x\$\$i \ a})))" ``` hoelzl@38656 ` 561` ``` (is "_ = sets ?SIGMA") ``` hoelzl@38656 ` 562` ```proof (rule antisym) ``` hoelzl@38656 ` 563` ``` show "sets borel_space \ sets ?SIGMA" ``` hoelzl@38656 ` 564` ``` using open_span_halfspace halfspace_span_halfspace_le by auto ``` hoelzl@38656 ` 565` ``` show "sets ?SIGMA \ sets borel_space" ``` hoelzl@38656 ` 566` ``` by (rule borel_space.sets_sigma_subset) auto ``` hoelzl@38656 ` 567` ```qed ``` hoelzl@38656 ` 568` hoelzl@38656 ` 569` ```lemma borel_space_eq_halfspace_less: ``` hoelzl@38656 ` 570` ``` "sets borel_space = sets (sigma UNIV (range (\ (a, i). {x::'a::ordered_euclidean_space. x\$\$i < a})))" ``` hoelzl@38656 ` 571` ``` (is "_ = sets ?SIGMA") ``` hoelzl@38656 ` 572` ```proof (rule antisym) ``` hoelzl@38656 ` 573` ``` show "sets borel_space \ sets ?SIGMA" ``` hoelzl@38656 ` 574` ``` using open_span_halfspace . ``` hoelzl@38656 ` 575` ``` show "sets ?SIGMA \ sets borel_space" ``` hoelzl@38656 ` 576` ``` by (rule borel_space.sets_sigma_subset) auto ``` hoelzl@38656 ` 577` ```qed ``` hoelzl@38656 ` 578` hoelzl@38656 ` 579` ```lemma borel_space_eq_halfspace_gt: ``` hoelzl@38656 ` 580` ``` "sets borel_space = sets (sigma UNIV (range (\ (a, i). {x::'a::ordered_euclidean_space. a < x\$\$i})))" ``` hoelzl@38656 ` 581` ``` (is "_ = sets ?SIGMA") ``` hoelzl@38656 ` 582` ```proof (rule antisym) ``` hoelzl@38656 ` 583` ``` show "sets borel_space \ sets ?SIGMA" ``` hoelzl@38656 ` 584` ``` using halfspace_le_span_halfspace_gt open_span_halfspace halfspace_span_halfspace_le by auto ``` hoelzl@38656 ` 585` ``` show "sets ?SIGMA \ sets borel_space" ``` hoelzl@38656 ` 586` ``` by (rule borel_space.sets_sigma_subset) auto ``` hoelzl@38656 ` 587` ```qed ``` hoelzl@38656 ` 588` hoelzl@38656 ` 589` ```lemma borel_space_eq_halfspace_ge: ``` hoelzl@38656 ` 590` ``` "sets borel_space = sets (sigma UNIV (range (\ (a, i). {x::'a::ordered_euclidean_space. a \ x\$\$i})))" ``` hoelzl@38656 ` 591` ``` (is "_ = sets ?SIGMA") ``` hoelzl@38656 ` 592` ```proof (rule antisym) ``` hoelzl@38656 ` 593` ``` show "sets borel_space \ sets ?SIGMA" ``` hoelzl@38656 ` 594` ``` using halfspace_span_halfspace_ge open_span_halfspace by auto ``` hoelzl@38656 ` 595` ``` show "sets ?SIGMA \ sets borel_space" ``` hoelzl@38656 ` 596` ``` by (rule borel_space.sets_sigma_subset) auto ``` hoelzl@38656 ` 597` ```qed ``` hoelzl@38656 ` 598` hoelzl@38656 ` 599` ```lemma (in sigma_algebra) borel_measurable_halfspacesI: ``` hoelzl@38656 ` 600` ``` fixes f :: "'a \ 'c\ordered_euclidean_space" ``` hoelzl@38656 ` 601` ``` assumes "sets borel_space = sets (sigma UNIV (range F))" ``` hoelzl@38656 ` 602` ``` and "\a i. S a i = f -` F (a,i) \ space M" ``` hoelzl@38656 ` 603` ``` and "\a i. \ i < DIM('c) \ S a i \ sets M" ``` hoelzl@38656 ` 604` ``` shows "f \ borel_measurable M = (\ia::real. S a i \ sets M)" ``` hoelzl@38656 ` 605` ```proof safe ``` hoelzl@38656 ` 606` ``` fix a :: real and i assume i: "i < DIM('c)" and f: "f \ borel_measurable M" ``` hoelzl@38656 ` 607` ``` then show "S a i \ sets M" unfolding assms ``` hoelzl@38656 ` 608` ``` by (auto intro!: measurable_sets sigma_sets.Basic simp: assms(1) sigma_def) ``` hoelzl@38656 ` 609` ```next ``` hoelzl@38656 ` 610` ``` assume a: "\ia. S a i \ sets M" ``` hoelzl@38656 ` 611` ``` { fix a i have "S a i \ sets M" ``` hoelzl@38656 ` 612` ``` proof cases ``` hoelzl@38656 ` 613` ``` assume "i < DIM('c)" ``` hoelzl@38656 ` 614` ``` with a show ?thesis unfolding assms(2) by simp ``` hoelzl@38656 ` 615` ``` next ``` hoelzl@38656 ` 616` ``` assume "\ i < DIM('c)" ``` hoelzl@38656 ` 617` ``` from assms(3)[OF this] show ?thesis . ``` hoelzl@38656 ` 618` ``` qed } ``` hoelzl@38656 ` 619` ``` then have "f \ measurable M (sigma UNIV (range F))" ``` hoelzl@38656 ` 620` ``` by (auto intro!: measurable_sigma simp: assms(2)) ``` hoelzl@38656 ` 621` ``` then show "f \ borel_measurable M" unfolding measurable_def ``` hoelzl@38656 ` 622` ``` unfolding assms(1) by simp ``` hoelzl@38656 ` 623` ```qed ``` hoelzl@38656 ` 624` hoelzl@38656 ` 625` ```lemma (in sigma_algebra) borel_measurable_iff_halfspace_le: ``` hoelzl@38656 ` 626` ``` fixes f :: "'a \ 'c\ordered_euclidean_space" ``` hoelzl@38656 ` 627` ``` shows "f \ borel_measurable M = (\ia. {w \ space M. f w \$\$ i \ a} \ sets M)" ``` hoelzl@38656 ` 628` ``` by (rule borel_measurable_halfspacesI[OF borel_space_eq_halfspace_le]) auto ``` hoelzl@38656 ` 629` hoelzl@38656 ` 630` ```lemma (in sigma_algebra) borel_measurable_iff_halfspace_less: ``` hoelzl@38656 ` 631` ``` fixes f :: "'a \ 'c\ordered_euclidean_space" ``` hoelzl@38656 ` 632` ``` shows "f \ borel_measurable M \ (\ia. {w \ space M. f w \$\$ i < a} \ sets M)" ``` hoelzl@38656 ` 633` ``` by (rule borel_measurable_halfspacesI[OF borel_space_eq_halfspace_less]) auto ``` hoelzl@38656 ` 634` hoelzl@38656 ` 635` ```lemma (in sigma_algebra) borel_measurable_iff_halfspace_ge: ``` hoelzl@38656 ` 636` ``` fixes f :: "'a \ 'c\ordered_euclidean_space" ``` hoelzl@38656 ` 637` ``` shows "f \ borel_measurable M = (\ia. {w \ space M. a \ f w \$\$ i} \ sets M)" ``` hoelzl@38656 ` 638` ``` by (rule borel_measurable_halfspacesI[OF borel_space_eq_halfspace_ge]) auto ``` hoelzl@38656 ` 639` hoelzl@38656 ` 640` ```lemma (in sigma_algebra) borel_measurable_iff_halfspace_greater: ``` hoelzl@38656 ` 641` ``` fixes f :: "'a \ 'c\ordered_euclidean_space" ``` hoelzl@38656 ` 642` ``` shows "f \ borel_measurable M \ (\ia. {w \ space M. a < f w \$\$ i} \ sets M)" ``` hoelzl@38656 ` 643` ``` by (rule borel_measurable_halfspacesI[OF borel_space_eq_halfspace_gt]) auto ``` hoelzl@38656 ` 644` hoelzl@38656 ` 645` ```lemma (in sigma_algebra) borel_measurable_iff_le: ``` hoelzl@38656 ` 646` ``` "(f::'a \ real) \ borel_measurable M = (\a. {w \ space M. f w \ a} \ sets M)" ``` hoelzl@38656 ` 647` ``` using borel_measurable_iff_halfspace_le[where 'c=real] by simp ``` hoelzl@38656 ` 648` hoelzl@38656 ` 649` ```lemma (in sigma_algebra) borel_measurable_iff_less: ``` hoelzl@38656 ` 650` ``` "(f::'a \ real) \ borel_measurable M = (\a. {w \ space M. f w < a} \ sets M)" ``` hoelzl@38656 ` 651` ``` using borel_measurable_iff_halfspace_less[where 'c=real] by simp ``` hoelzl@38656 ` 652` hoelzl@38656 ` 653` ```lemma (in sigma_algebra) borel_measurable_iff_ge: ``` hoelzl@38656 ` 654` ``` "(f::'a \ real) \ borel_measurable M = (\a. {w \ space M. a \ f w} \ sets M)" ``` hoelzl@38656 ` 655` ``` using borel_measurable_iff_halfspace_ge[where 'c=real] by simp ``` hoelzl@38656 ` 656` hoelzl@38656 ` 657` ```lemma (in sigma_algebra) borel_measurable_iff_greater: ``` hoelzl@38656 ` 658` ``` "(f::'a \ real) \ borel_measurable M = (\a. {w \ space M. a < f w} \ sets M)" ``` hoelzl@38656 ` 659` ``` using borel_measurable_iff_halfspace_greater[where 'c=real] by simp ``` hoelzl@38656 ` 660` hoelzl@38656 ` 661` ```subsection "Borel measurable operators" ``` hoelzl@38656 ` 662` hoelzl@38656 ` 663` ```lemma (in sigma_algebra) affine_borel_measurable_vector: ``` hoelzl@38656 ` 664` ``` fixes f :: "'a \ 'x::real_normed_vector" ``` hoelzl@38656 ` 665` ``` assumes "f \ borel_measurable M" ``` hoelzl@38656 ` 666` ``` shows "(\x. a + b *\<^sub>R f x) \ borel_measurable M" ``` hoelzl@38656 ` 667` ```proof (rule borel_measurableI) ``` hoelzl@38656 ` 668` ``` fix S :: "'x set" assume "open S" ``` hoelzl@38656 ` 669` ``` show "(\x. a + b *\<^sub>R f x) -` S \ space M \ sets M" ``` hoelzl@38656 ` 670` ``` proof cases ``` hoelzl@38656 ` 671` ``` assume "b \ 0" ``` hoelzl@38656 ` 672` ``` with `open S` have "((\x. (- a + x) /\<^sub>R b) ` S) \ open" (is "?S \ open") ``` hoelzl@38656 ` 673` ``` by (auto intro!: open_affinity simp: scaleR.add_right mem_def) ``` hoelzl@38656 ` 674` ``` hence "?S \ sets borel_space" ``` hoelzl@38656 ` 675` ``` unfolding borel_space_def by (auto simp: sigma_def intro!: sigma_sets.Basic) ``` hoelzl@38656 ` 676` ``` moreover ``` hoelzl@38656 ` 677` ``` from `b \ 0` have "(\x. a + b *\<^sub>R f x) -` S = f -` ?S" ``` hoelzl@38656 ` 678` ``` apply auto by (rule_tac x="a + b *\<^sub>R f x" in image_eqI, simp_all) ``` hoelzl@38656 ` 679` ``` ultimately show ?thesis using assms unfolding in_borel_measurable_borel_space ``` hoelzl@38656 ` 680` ``` by auto ``` hoelzl@38656 ` 681` ``` qed simp ``` hoelzl@38656 ` 682` ```qed ``` hoelzl@38656 ` 683` hoelzl@38656 ` 684` ```lemma (in sigma_algebra) affine_borel_measurable: ``` hoelzl@38656 ` 685` ``` fixes g :: "'a \ real" ``` hoelzl@38656 ` 686` ``` assumes g: "g \ borel_measurable M" ``` hoelzl@38656 ` 687` ``` shows "(\x. a + (g x) * b) \ borel_measurable M" ``` hoelzl@38656 ` 688` ``` using affine_borel_measurable_vector[OF assms] by (simp add: mult_commute) ``` hoelzl@38656 ` 689` hoelzl@38656 ` 690` ```lemma (in sigma_algebra) borel_measurable_add[simp, intro]: ``` hoelzl@38656 ` 691` ``` fixes f :: "'a \ real" ``` paulson@33533 ` 692` ``` assumes f: "f \ borel_measurable M" ``` paulson@33533 ` 693` ``` assumes g: "g \ borel_measurable M" ``` paulson@33533 ` 694` ``` shows "(\x. f x + g x) \ borel_measurable M" ``` paulson@33533 ` 695` ```proof - ``` hoelzl@38656 ` 696` ``` have 1: "\a. {w\space M. a \ f w + g w} = {w \ space M. a + g w * -1 \ f w}" ``` paulson@33533 ` 697` ``` by auto ``` hoelzl@38656 ` 698` ``` have "\a. (\w. a + (g w) * -1) \ borel_measurable M" ``` hoelzl@38656 ` 699` ``` by (rule affine_borel_measurable [OF g]) ``` hoelzl@38656 ` 700` ``` then have "\a. {w \ space M. (\w. a + (g w) * -1)(w) \ f w} \ sets M" using f ``` hoelzl@38656 ` 701` ``` by auto ``` hoelzl@38656 ` 702` ``` then have "\a. {w \ space M. a \ f w + g w} \ sets M" ``` hoelzl@38656 ` 703` ``` by (simp add: 1) ``` hoelzl@38656 ` 704` ``` then show ?thesis ``` hoelzl@38656 ` 705` ``` by (simp add: borel_measurable_iff_ge) ``` paulson@33533 ` 706` ```qed ``` paulson@33533 ` 707` hoelzl@38656 ` 708` ```lemma (in sigma_algebra) borel_measurable_square: ``` hoelzl@38656 ` 709` ``` fixes f :: "'a \ real" ``` paulson@33533 ` 710` ``` assumes f: "f \ borel_measurable M" ``` paulson@33533 ` 711` ``` shows "(\x. (f x)^2) \ borel_measurable M" ``` paulson@33533 ` 712` ```proof - ``` paulson@33533 ` 713` ``` { ``` paulson@33533 ` 714` ``` fix a ``` paulson@33533 ` 715` ``` have "{w \ space M. (f w)\ \ a} \ sets M" ``` paulson@33533 ` 716` ``` proof (cases rule: linorder_cases [of a 0]) ``` paulson@33533 ` 717` ``` case less ``` hoelzl@38656 ` 718` ``` hence "{w \ space M. (f w)\ \ a} = {}" ``` paulson@33533 ` 719` ``` by auto (metis less order_le_less_trans power2_less_0) ``` paulson@33533 ` 720` ``` also have "... \ sets M" ``` hoelzl@38656 ` 721` ``` by (rule empty_sets) ``` paulson@33533 ` 722` ``` finally show ?thesis . ``` paulson@33533 ` 723` ``` next ``` paulson@33533 ` 724` ``` case equal ``` hoelzl@38656 ` 725` ``` hence "{w \ space M. (f w)\ \ a} = ``` paulson@33533 ` 726` ``` {w \ space M. f w \ 0} \ {w \ space M. 0 \ f w}" ``` paulson@33533 ` 727` ``` by auto ``` paulson@33533 ` 728` ``` also have "... \ sets M" ``` hoelzl@38656 ` 729` ``` apply (insert f) ``` hoelzl@38656 ` 730` ``` apply (rule Int) ``` hoelzl@38656 ` 731` ``` apply (simp add: borel_measurable_iff_le) ``` hoelzl@38656 ` 732` ``` apply (simp add: borel_measurable_iff_ge) ``` paulson@33533 ` 733` ``` done ``` paulson@33533 ` 734` ``` finally show ?thesis . ``` paulson@33533 ` 735` ``` next ``` paulson@33533 ` 736` ``` case greater ``` paulson@33533 ` 737` ``` have "\x. (f x ^ 2 \ sqrt a ^ 2) = (- sqrt a \ f x & f x \ sqrt a)" ``` paulson@33533 ` 738` ``` by (metis abs_le_interval_iff abs_of_pos greater real_sqrt_abs ``` paulson@33533 ` 739` ``` real_sqrt_le_iff real_sqrt_power) ``` paulson@33533 ` 740` ``` hence "{w \ space M. (f w)\ \ a} = ``` hoelzl@38656 ` 741` ``` {w \ space M. -(sqrt a) \ f w} \ {w \ space M. f w \ sqrt a}" ``` paulson@33533 ` 742` ``` using greater by auto ``` paulson@33533 ` 743` ``` also have "... \ sets M" ``` hoelzl@38656 ` 744` ``` apply (insert f) ``` hoelzl@38656 ` 745` ``` apply (rule Int) ``` hoelzl@38656 ` 746` ``` apply (simp add: borel_measurable_iff_ge) ``` hoelzl@38656 ` 747` ``` apply (simp add: borel_measurable_iff_le) ``` paulson@33533 ` 748` ``` done ``` paulson@33533 ` 749` ``` finally show ?thesis . ``` paulson@33533 ` 750` ``` qed ``` paulson@33533 ` 751` ``` } ``` hoelzl@38656 ` 752` ``` thus ?thesis by (auto simp add: borel_measurable_iff_le) ``` paulson@33533 ` 753` ```qed ``` paulson@33533 ` 754` paulson@33533 ` 755` ```lemma times_eq_sum_squares: ``` paulson@33533 ` 756` ``` fixes x::real ``` paulson@33533 ` 757` ``` shows"x*y = ((x+y)^2)/4 - ((x-y)^ 2)/4" ``` hoelzl@38656 ` 758` ```by (simp add: power2_eq_square ring_distribs diff_divide_distrib [symmetric]) ``` paulson@33533 ` 759` hoelzl@38656 ` 760` ```lemma (in sigma_algebra) borel_measurable_uminus[simp, intro]: ``` hoelzl@38656 ` 761` ``` fixes g :: "'a \ real" ``` paulson@33533 ` 762` ``` assumes g: "g \ borel_measurable M" ``` paulson@33533 ` 763` ``` shows "(\x. - g x) \ borel_measurable M" ``` paulson@33533 ` 764` ```proof - ``` paulson@33533 ` 765` ``` have "(\x. - g x) = (\x. 0 + (g x) * -1)" ``` paulson@33533 ` 766` ``` by simp ``` hoelzl@38656 ` 767` ``` also have "... \ borel_measurable M" ``` hoelzl@38656 ` 768` ``` by (fast intro: affine_borel_measurable g) ``` paulson@33533 ` 769` ``` finally show ?thesis . ``` paulson@33533 ` 770` ```qed ``` paulson@33533 ` 771` hoelzl@38656 ` 772` ```lemma (in sigma_algebra) borel_measurable_times[simp, intro]: ``` hoelzl@38656 ` 773` ``` fixes f :: "'a \ real" ``` paulson@33533 ` 774` ``` assumes f: "f \ borel_measurable M" ``` paulson@33533 ` 775` ``` assumes g: "g \ borel_measurable M" ``` paulson@33533 ` 776` ``` shows "(\x. f x * g x) \ borel_measurable M" ``` paulson@33533 ` 777` ```proof - ``` paulson@33533 ` 778` ``` have 1: "(\x. 0 + (f x + g x)\ * inverse 4) \ borel_measurable M" ``` hoelzl@38656 ` 779` ``` using assms by (fast intro: affine_borel_measurable borel_measurable_square) ``` hoelzl@38656 ` 780` ``` have "(\x. -((f x + -g x) ^ 2 * inverse 4)) = ``` paulson@33533 ` 781` ``` (\x. 0 + ((f x + -g x) ^ 2 * inverse -4))" ``` hoelzl@35582 ` 782` ``` by (simp add: minus_divide_right) ``` hoelzl@38656 ` 783` ``` also have "... \ borel_measurable M" ``` hoelzl@38656 ` 784` ``` using f g by (fast intro: affine_borel_measurable borel_measurable_square f g) ``` paulson@33533 ` 785` ``` finally have 2: "(\x. -((f x + -g x) ^ 2 * inverse 4)) \ borel_measurable M" . ``` paulson@33533 ` 786` ``` show ?thesis ``` hoelzl@38656 ` 787` ``` apply (simp add: times_eq_sum_squares diff_minus) ``` hoelzl@38656 ` 788` ``` using 1 2 by simp ``` paulson@33533 ` 789` ```qed ``` paulson@33533 ` 790` hoelzl@38656 ` 791` ```lemma (in sigma_algebra) borel_measurable_diff[simp, intro]: ``` hoelzl@38656 ` 792` ``` fixes f :: "'a \ real" ``` paulson@33533 ` 793` ``` assumes f: "f \ borel_measurable M" ``` paulson@33533 ` 794` ``` assumes g: "g \ borel_measurable M" ``` paulson@33533 ` 795` ``` shows "(\x. f x - g x) \ borel_measurable M" ``` hoelzl@38656 ` 796` ``` unfolding diff_minus using assms by fast ``` paulson@33533 ` 797` hoelzl@38656 ` 798` ```lemma (in sigma_algebra) borel_measurable_setsum[simp, intro]: ``` hoelzl@38656 ` 799` ``` fixes f :: "'c \ 'a \ real" ``` hoelzl@38656 ` 800` ``` assumes "\i. i \ S \ f i \ borel_measurable M" ``` hoelzl@38656 ` 801` ``` shows "(\x. \i\S. f i x) \ borel_measurable M" ``` hoelzl@38656 ` 802` ```proof cases ``` hoelzl@38656 ` 803` ``` assume "finite S" ``` hoelzl@38656 ` 804` ``` thus ?thesis using assms by induct auto ``` hoelzl@38656 ` 805` ```qed simp ``` hoelzl@35692 ` 806` hoelzl@38656 ` 807` ```lemma (in sigma_algebra) borel_measurable_inverse[simp, intro]: ``` hoelzl@38656 ` 808` ``` fixes f :: "'a \ real" ``` hoelzl@35692 ` 809` ``` assumes "f \ borel_measurable M" ``` hoelzl@35692 ` 810` ``` shows "(\x. inverse (f x)) \ borel_measurable M" ``` hoelzl@38656 ` 811` ``` unfolding borel_measurable_iff_ge unfolding inverse_eq_divide ``` hoelzl@38656 ` 812` ```proof safe ``` hoelzl@38656 ` 813` ``` fix a :: real ``` hoelzl@38656 ` 814` ``` have *: "{w \ space M. a \ 1 / f w} = ``` hoelzl@38656 ` 815` ``` ({w \ space M. 0 < f w} \ {w \ space M. a * f w \ 1}) \ ``` hoelzl@38656 ` 816` ``` ({w \ space M. f w < 0} \ {w \ space M. 1 \ a * f w}) \ ``` hoelzl@38656 ` 817` ``` ({w \ space M. f w = 0} \ {w \ space M. a \ 0})" by (auto simp: le_divide_eq) ``` hoelzl@38656 ` 818` ``` show "{w \ space M. a \ 1 / f w} \ sets M" using assms unfolding * ``` hoelzl@38656 ` 819` ``` by (auto intro!: Int Un) ``` hoelzl@35692 ` 820` ```qed ``` hoelzl@35692 ` 821` hoelzl@38656 ` 822` ```lemma (in sigma_algebra) borel_measurable_divide[simp, intro]: ``` hoelzl@38656 ` 823` ``` fixes f :: "'a \ real" ``` hoelzl@35692 ` 824` ``` assumes "f \ borel_measurable M" ``` hoelzl@35692 ` 825` ``` and "g \ borel_measurable M" ``` hoelzl@35692 ` 826` ``` shows "(\x. f x / g x) \ borel_measurable M" ``` hoelzl@35692 ` 827` ``` unfolding field_divide_inverse ``` hoelzl@38656 ` 828` ``` by (rule borel_measurable_inverse borel_measurable_times assms)+ ``` hoelzl@38656 ` 829` hoelzl@38656 ` 830` ```lemma (in sigma_algebra) borel_measurable_max[intro, simp]: ``` hoelzl@38656 ` 831` ``` fixes f g :: "'a \ real" ``` hoelzl@38656 ` 832` ``` assumes "f \ borel_measurable M" ``` hoelzl@38656 ` 833` ``` assumes "g \ borel_measurable M" ``` hoelzl@38656 ` 834` ``` shows "(\x. max (g x) (f x)) \ borel_measurable M" ``` hoelzl@38656 ` 835` ``` unfolding borel_measurable_iff_le ``` hoelzl@38656 ` 836` ```proof safe ``` hoelzl@38656 ` 837` ``` fix a ``` hoelzl@38656 ` 838` ``` have "{x \ space M. max (g x) (f x) \ a} = ``` hoelzl@38656 ` 839` ``` {x \ space M. g x \ a} \ {x \ space M. f x \ a}" by auto ``` hoelzl@38656 ` 840` ``` thus "{x \ space M. max (g x) (f x) \ a} \ sets M" ``` hoelzl@38656 ` 841` ``` using assms unfolding borel_measurable_iff_le ``` hoelzl@38656 ` 842` ``` by (auto intro!: Int) ``` hoelzl@38656 ` 843` ```qed ``` hoelzl@38656 ` 844` hoelzl@38656 ` 845` ```lemma (in sigma_algebra) borel_measurable_min[intro, simp]: ``` hoelzl@38656 ` 846` ``` fixes f g :: "'a \ real" ``` hoelzl@38656 ` 847` ``` assumes "f \ borel_measurable M" ``` hoelzl@38656 ` 848` ``` assumes "g \ borel_measurable M" ``` hoelzl@38656 ` 849` ``` shows "(\x. min (g x) (f x)) \ borel_measurable M" ``` hoelzl@38656 ` 850` ``` unfolding borel_measurable_iff_ge ``` hoelzl@38656 ` 851` ```proof safe ``` hoelzl@38656 ` 852` ``` fix a ``` hoelzl@38656 ` 853` ``` have "{x \ space M. a \ min (g x) (f x)} = ``` hoelzl@38656 ` 854` ``` {x \ space M. a \ g x} \ {x \ space M. a \ f x}" by auto ``` hoelzl@38656 ` 855` ``` thus "{x \ space M. a \ min (g x) (f x)} \ sets M" ``` hoelzl@38656 ` 856` ``` using assms unfolding borel_measurable_iff_ge ``` hoelzl@38656 ` 857` ``` by (auto intro!: Int) ``` hoelzl@38656 ` 858` ```qed ``` hoelzl@38656 ` 859` hoelzl@38656 ` 860` ```lemma (in sigma_algebra) borel_measurable_abs[simp, intro]: ``` hoelzl@38656 ` 861` ``` assumes "f \ borel_measurable M" ``` hoelzl@38656 ` 862` ``` shows "(\x. \f x :: real\) \ borel_measurable M" ``` hoelzl@38656 ` 863` ```proof - ``` hoelzl@38656 ` 864` ``` have *: "\x. \f x\ = max 0 (f x) + max 0 (- f x)" by (simp add: max_def) ``` hoelzl@38656 ` 865` ``` show ?thesis unfolding * using assms by auto ``` hoelzl@38656 ` 866` ```qed ``` hoelzl@38656 ` 867` hoelzl@38656 ` 868` ```section "Borel space over the real line with infinity" ``` hoelzl@35692 ` 869` hoelzl@38656 ` 870` ```lemma borel_space_Real_measurable: ``` hoelzl@38656 ` 871` ``` "A \ sets borel_space \ Real -` A \ sets borel_space" ``` hoelzl@38656 ` 872` ```proof (rule borel_measurable_translate) ``` hoelzl@38656 ` 873` ``` fix B :: "pinfreal set" assume "open B" ``` hoelzl@38656 ` 874` ``` then obtain T x where T: "open T" "Real ` (T \ {0..}) = B - {\}" and ``` hoelzl@38656 ` 875` ``` x: "\ \ B \ 0 \ x" "\ \ B \ {Real x <..} \ B" ``` hoelzl@38656 ` 876` ``` unfolding open_pinfreal_def by blast ``` hoelzl@38656 ` 877` hoelzl@38656 ` 878` ``` have "Real -` B = Real -` (B - {\})" by auto ``` hoelzl@38656 ` 879` ``` also have "\ = Real -` (Real ` (T \ {0..}))" using T by simp ``` hoelzl@38656 ` 880` ``` also have "\ = (if 0 \ T then T \ {.. 0} else T \ {0..})" ``` hoelzl@38656 ` 881` ``` apply (auto simp add: Real_eq_Real image_iff) ``` hoelzl@38656 ` 882` ``` apply (rule_tac x="max 0 x" in bexI) ``` hoelzl@38656 ` 883` ``` by (auto simp: max_def) ``` hoelzl@38656 ` 884` ``` finally show "Real -` B \ sets borel_space" ``` hoelzl@38656 ` 885` ``` using `open T` by auto ``` hoelzl@38656 ` 886` ```qed simp ``` hoelzl@38656 ` 887` hoelzl@38656 ` 888` ```lemma borel_space_real_measurable: ``` hoelzl@38656 ` 889` ``` "A \ sets borel_space \ (real -` A :: pinfreal set) \ sets borel_space" ``` hoelzl@38656 ` 890` ```proof (rule borel_measurable_translate) ``` hoelzl@38656 ` 891` ``` fix B :: "real set" assume "open B" ``` hoelzl@38656 ` 892` ``` { fix x have "0 < real x \ (\r>0. x = Real r)" by (cases x) auto } ``` hoelzl@38656 ` 893` ``` note Ex_less_real = this ``` hoelzl@38656 ` 894` ``` have *: "real -` B = (if 0 \ B then real -` (B \ {0 <..}) \ {0, \} else real -` (B \ {0 <..}))" ``` hoelzl@38656 ` 895` ``` by (force simp: Ex_less_real) ``` hoelzl@38656 ` 896` hoelzl@38656 ` 897` ``` have "open (real -` (B \ {0 <..}) :: pinfreal set)" ``` hoelzl@38656 ` 898` ``` unfolding open_pinfreal_def using `open B` ``` hoelzl@38656 ` 899` ``` by (auto intro!: open_Int exI[of _ "B \ {0 <..}"] simp: image_iff Ex_less_real) ``` hoelzl@38656 ` 900` ``` then show "(real -` B :: pinfreal set) \ sets borel_space" unfolding * by auto ``` hoelzl@38656 ` 901` ```qed simp ``` hoelzl@38656 ` 902` hoelzl@38656 ` 903` ```lemma (in sigma_algebra) borel_measurable_Real[intro, simp]: ``` hoelzl@38656 ` 904` ``` assumes "f \ borel_measurable M" ``` hoelzl@38656 ` 905` ``` shows "(\x. Real (f x)) \ borel_measurable M" ``` hoelzl@38656 ` 906` ``` unfolding in_borel_measurable_borel_space ``` hoelzl@38656 ` 907` ```proof safe ``` hoelzl@38656 ` 908` ``` fix S :: "pinfreal set" assume "S \ sets borel_space" ``` hoelzl@38656 ` 909` ``` from borel_space_Real_measurable[OF this] ``` hoelzl@38656 ` 910` ``` have "(Real \ f) -` S \ space M \ sets M" ``` hoelzl@38656 ` 911` ``` using assms ``` hoelzl@38656 ` 912` ``` unfolding vimage_compose in_borel_measurable_borel_space ``` hoelzl@38656 ` 913` ``` by auto ``` hoelzl@38656 ` 914` ``` thus "(\x. Real (f x)) -` S \ space M \ sets M" by (simp add: comp_def) ``` hoelzl@35748 ` 915` ```qed ``` hoelzl@35692 ` 916` hoelzl@38656 ` 917` ```lemma (in sigma_algebra) borel_measurable_real[intro, simp]: ``` hoelzl@38656 ` 918` ``` fixes f :: "'a \ pinfreal" ``` hoelzl@38656 ` 919` ``` assumes "f \ borel_measurable M" ``` hoelzl@38656 ` 920` ``` shows "(\x. real (f x)) \ borel_measurable M" ``` hoelzl@38656 ` 921` ``` unfolding in_borel_measurable_borel_space ``` hoelzl@38656 ` 922` ```proof safe ``` hoelzl@38656 ` 923` ``` fix S :: "real set" assume "S \ sets borel_space" ``` hoelzl@38656 ` 924` ``` from borel_space_real_measurable[OF this] ``` hoelzl@38656 ` 925` ``` have "(real \ f) -` S \ space M \ sets M" ``` hoelzl@38656 ` 926` ``` using assms ``` hoelzl@38656 ` 927` ``` unfolding vimage_compose in_borel_measurable_borel_space ``` hoelzl@38656 ` 928` ``` by auto ``` hoelzl@38656 ` 929` ``` thus "(\x. real (f x)) -` S \ space M \ sets M" by (simp add: comp_def) ``` hoelzl@38656 ` 930` ```qed ``` hoelzl@35692 ` 931` hoelzl@38656 ` 932` ```lemma (in sigma_algebra) borel_measurable_Real_eq: ``` hoelzl@38656 ` 933` ``` assumes "\x. x \ space M \ 0 \ f x" ``` hoelzl@38656 ` 934` ``` shows "(\x. Real (f x)) \ borel_measurable M \ f \ borel_measurable M" ``` hoelzl@38656 ` 935` ```proof ``` hoelzl@38656 ` 936` ``` have [simp]: "(\x. Real (f x)) -` {\} \ space M = {}" ``` hoelzl@38656 ` 937` ``` by auto ``` hoelzl@38656 ` 938` ``` assume "(\x. Real (f x)) \ borel_measurable M" ``` hoelzl@38656 ` 939` ``` hence "(\x. real (Real (f x))) \ borel_measurable M" ``` hoelzl@38656 ` 940` ``` by (rule borel_measurable_real) ``` hoelzl@38656 ` 941` ``` moreover have "\x. x \ space M \ real (Real (f x)) = f x" ``` hoelzl@38656 ` 942` ``` using assms by auto ``` hoelzl@38656 ` 943` ``` ultimately show "f \ borel_measurable M" ``` hoelzl@38656 ` 944` ``` by (simp cong: measurable_cong) ``` hoelzl@38656 ` 945` ```qed auto ``` hoelzl@35692 ` 946` hoelzl@38656 ` 947` ```lemma (in sigma_algebra) borel_measurable_pinfreal_eq_real: ``` hoelzl@38656 ` 948` ``` "f \ borel_measurable M \ ``` hoelzl@38656 ` 949` ``` ((\x. real (f x)) \ borel_measurable M \ f -` {\} \ space M \ sets M)" ``` hoelzl@38656 ` 950` ```proof safe ``` hoelzl@38656 ` 951` ``` assume "f \ borel_measurable M" ``` hoelzl@38656 ` 952` ``` then show "(\x. real (f x)) \ borel_measurable M" "f -` {\} \ space M \ sets M" ``` hoelzl@38656 ` 953` ``` by (auto intro: borel_measurable_vimage borel_measurable_real) ``` hoelzl@38656 ` 954` ```next ``` hoelzl@38656 ` 955` ``` assume *: "(\x. real (f x)) \ borel_measurable M" "f -` {\} \ space M \ sets M" ``` hoelzl@38656 ` 956` ``` have "f -` {\} \ space M = {x\space M. f x = \}" by auto ``` hoelzl@38656 ` 957` ``` with * have **: "{x\space M. f x = \} \ sets M" by simp ``` hoelzl@38656 ` 958` ``` have f: "f = (\x. if f x = \ then \ else Real (real (f x)))" ``` hoelzl@38656 ` 959` ``` by (simp add: expand_fun_eq Real_real) ``` hoelzl@38656 ` 960` ``` show "f \ borel_measurable M" ``` hoelzl@38656 ` 961` ``` apply (subst f) ``` hoelzl@38656 ` 962` ``` apply (rule measurable_If) ``` hoelzl@38656 ` 963` ``` using * ** by auto ``` hoelzl@38656 ` 964` ```qed ``` hoelzl@38656 ` 965` hoelzl@38656 ` 966` ```lemma (in sigma_algebra) less_eq_ge_measurable: ``` hoelzl@38656 ` 967` ``` fixes f :: "'a \ 'c::linorder" ``` hoelzl@38656 ` 968` ``` shows "{x\space M. a < f x} \ sets M \ {x\space M. f x \ a} \ sets M" ``` hoelzl@38656 ` 969` ```proof ``` hoelzl@38656 ` 970` ``` assume "{x\space M. f x \ a} \ sets M" ``` hoelzl@38656 ` 971` ``` moreover have "{x\space M. a < f x} = space M - {x\space M. f x \ a}" by auto ``` hoelzl@38656 ` 972` ``` ultimately show "{x\space M. a < f x} \ sets M" by auto ``` hoelzl@38656 ` 973` ```next ``` hoelzl@38656 ` 974` ``` assume "{x\space M. a < f x} \ sets M" ``` hoelzl@38656 ` 975` ``` moreover have "{x\space M. f x \ a} = space M - {x\space M. a < f x}" by auto ``` hoelzl@38656 ` 976` ``` ultimately show "{x\space M. f x \ a} \ sets M" by auto ``` hoelzl@38656 ` 977` ```qed ``` hoelzl@35692 ` 978` hoelzl@38656 ` 979` ```lemma (in sigma_algebra) greater_eq_le_measurable: ``` hoelzl@38656 ` 980` ``` fixes f :: "'a \ 'c::linorder" ``` hoelzl@38656 ` 981` ``` shows "{x\space M. f x < a} \ sets M \ {x\space M. a \ f x} \ sets M" ``` hoelzl@38656 ` 982` ```proof ``` hoelzl@38656 ` 983` ``` assume "{x\space M. a \ f x} \ sets M" ``` hoelzl@38656 ` 984` ``` moreover have "{x\space M. f x < a} = space M - {x\space M. a \ f x}" by auto ``` hoelzl@38656 ` 985` ``` ultimately show "{x\space M. f x < a} \ sets M" by auto ``` hoelzl@38656 ` 986` ```next ``` hoelzl@38656 ` 987` ``` assume "{x\space M. f x < a} \ sets M" ``` hoelzl@38656 ` 988` ``` moreover have "{x\space M. a \ f x} = space M - {x\space M. f x < a}" by auto ``` hoelzl@38656 ` 989` ``` ultimately show "{x\space M. a \ f x} \ sets M" by auto ``` hoelzl@38656 ` 990` ```qed ``` hoelzl@38656 ` 991` hoelzl@38656 ` 992` ```lemma (in sigma_algebra) less_eq_le_pinfreal_measurable: ``` hoelzl@38656 ` 993` ``` fixes f :: "'a \ pinfreal" ``` hoelzl@38656 ` 994` ``` shows "(\a. {x\space M. a < f x} \ sets M) \ (\a. {x\space M. a \ f x} \ sets M)" ``` hoelzl@38656 ` 995` ```proof ``` hoelzl@38656 ` 996` ``` assume a: "\a. {x\space M. a \ f x} \ sets M" ``` hoelzl@38656 ` 997` ``` show "\a. {x \ space M. a < f x} \ sets M" ``` hoelzl@38656 ` 998` ``` proof ``` hoelzl@38656 ` 999` ``` fix a show "{x \ space M. a < f x} \ sets M" ``` hoelzl@38656 ` 1000` ``` proof (cases a) ``` hoelzl@38656 ` 1001` ``` case (preal r) ``` hoelzl@38656 ` 1002` ``` have "{x\space M. a < f x} = (\i. {x\space M. a + inverse (of_nat (Suc i)) \ f x})" ``` paulson@33533 ` 1003` ``` proof safe ``` hoelzl@38656 ` 1004` ``` fix x assume "a < f x" and [simp]: "x \ space M" ``` hoelzl@38656 ` 1005` ``` with ex_pinfreal_inverse_of_nat_Suc_less[of "f x - a"] ``` hoelzl@38656 ` 1006` ``` obtain n where "a + inverse (of_nat (Suc n)) < f x" ``` hoelzl@38656 ` 1007` ``` by (cases "f x", auto simp: pinfreal_minus_order) ``` hoelzl@38656 ` 1008` ``` then have "a + inverse (of_nat (Suc n)) \ f x" by simp ``` hoelzl@38656 ` 1009` ``` then show "x \ (\i. {x \ space M. a + inverse (of_nat (Suc i)) \ f x})" ``` paulson@33533 ` 1010` ``` by auto ``` paulson@33533 ` 1011` ``` next ``` hoelzl@38656 ` 1012` ``` fix i x assume [simp]: "x \ space M" ``` hoelzl@38656 ` 1013` ``` have "a < a + inverse (of_nat (Suc i))" using preal by auto ``` hoelzl@38656 ` 1014` ``` also assume "a + inverse (of_nat (Suc i)) \ f x" ``` hoelzl@38656 ` 1015` ``` finally show "a < f x" . ``` paulson@33533 ` 1016` ``` qed ``` hoelzl@38656 ` 1017` ``` with a show ?thesis by auto ``` hoelzl@38656 ` 1018` ``` qed simp ``` hoelzl@35582 ` 1019` ``` qed ``` hoelzl@35582 ` 1020` ```next ``` hoelzl@38656 ` 1021` ``` assume a': "\a. {x \ space M. a < f x} \ sets M" ``` hoelzl@38656 ` 1022` ``` then have a: "\a. {x \ space M. f x \ a} \ sets M" unfolding less_eq_ge_measurable . ``` hoelzl@38656 ` 1023` ``` show "\a. {x \ space M. a \ f x} \ sets M" unfolding greater_eq_le_measurable[symmetric] ``` hoelzl@38656 ` 1024` ``` proof ``` hoelzl@38656 ` 1025` ``` fix a show "{x \ space M. f x < a} \ sets M" ``` hoelzl@38656 ` 1026` ``` proof (cases a) ``` hoelzl@38656 ` 1027` ``` case (preal r) ``` hoelzl@38656 ` 1028` ``` show ?thesis ``` hoelzl@38656 ` 1029` ``` proof cases ``` hoelzl@38656 ` 1030` ``` assume "a = 0" then show ?thesis by simp ``` hoelzl@38656 ` 1031` ``` next ``` hoelzl@38656 ` 1032` ``` assume "a \ 0" ``` hoelzl@38656 ` 1033` ``` have "{x\space M. f x < a} = (\i. {x\space M. f x \ a - inverse (of_nat (Suc i))})" ``` hoelzl@38656 ` 1034` ``` proof safe ``` hoelzl@38656 ` 1035` ``` fix x assume "f x < a" and [simp]: "x \ space M" ``` hoelzl@38656 ` 1036` ``` with ex_pinfreal_inverse_of_nat_Suc_less[of "a - f x"] ``` hoelzl@38656 ` 1037` ``` obtain n where "inverse (of_nat (Suc n)) < a - f x" ``` hoelzl@38656 ` 1038` ``` using preal by (cases "f x") auto ``` hoelzl@38656 ` 1039` ``` then have "f x \ a - inverse (of_nat (Suc n)) " ``` hoelzl@38656 ` 1040` ``` using preal by (cases "f x") (auto split: split_if_asm) ``` hoelzl@38656 ` 1041` ``` then show "x \ (\i. {x \ space M. f x \ a - inverse (of_nat (Suc i))})" ``` hoelzl@38656 ` 1042` ``` by auto ``` hoelzl@38656 ` 1043` ``` next ``` hoelzl@38656 ` 1044` ``` fix i x assume [simp]: "x \ space M" ``` hoelzl@38656 ` 1045` ``` assume "f x \ a - inverse (of_nat (Suc i))" ``` hoelzl@38656 ` 1046` ``` also have "\ < a" using `a \ 0` preal by auto ``` hoelzl@38656 ` 1047` ``` finally show "f x < a" . ``` hoelzl@38656 ` 1048` ``` qed ``` hoelzl@38656 ` 1049` ``` with a show ?thesis by auto ``` hoelzl@38656 ` 1050` ``` qed ``` hoelzl@38656 ` 1051` ``` next ``` hoelzl@38656 ` 1052` ``` case infinite ``` hoelzl@38656 ` 1053` ``` have "f -` {\} \ space M = (\n. {x\space M. of_nat n < f x})" ``` hoelzl@38656 ` 1054` ``` proof (safe, simp_all, safe) ``` hoelzl@38656 ` 1055` ``` fix x assume *: "\n::nat. Real (real n) < f x" ``` hoelzl@38656 ` 1056` ``` show "f x = \" proof (rule ccontr) ``` hoelzl@38656 ` 1057` ``` assume "f x \ \" ``` hoelzl@38656 ` 1058` ``` with real_arch_lt[of "real (f x)"] obtain n where "f x < of_nat n" ``` hoelzl@38656 ` 1059` ``` by (auto simp: pinfreal_noteq_omega_Ex) ``` hoelzl@38656 ` 1060` ``` with *[THEN spec, of n] show False by auto ``` hoelzl@38656 ` 1061` ``` qed ``` hoelzl@38656 ` 1062` ``` qed ``` hoelzl@38656 ` 1063` ``` with a' have \: "f -` {\} \ space M \ sets M" by auto ``` hoelzl@38656 ` 1064` ``` moreover have "{x \ space M. f x < a} = space M - f -` {\} \ space M" ``` hoelzl@38656 ` 1065` ``` using infinite by auto ``` hoelzl@38656 ` 1066` ``` ultimately show ?thesis by auto ``` hoelzl@38656 ` 1067` ``` qed ``` hoelzl@35582 ` 1068` ``` qed ``` hoelzl@35582 ` 1069` ```qed ``` hoelzl@35582 ` 1070` hoelzl@38656 ` 1071` ```lemma (in sigma_algebra) borel_measurable_pinfreal_iff_greater: ``` hoelzl@38656 ` 1072` ``` "(f::'a \ pinfreal) \ borel_measurable M \ (\a. {x\space M. a < f x} \ sets M)" ``` hoelzl@38656 ` 1073` ```proof safe ``` hoelzl@38656 ` 1074` ``` fix a assume f: "f \ borel_measurable M" ``` hoelzl@38656 ` 1075` ``` have "{x\space M. a < f x} = f -` {a <..} \ space M" by auto ``` hoelzl@38656 ` 1076` ``` with f show "{x\space M. a < f x} \ sets M" ``` hoelzl@38656 ` 1077` ``` by (auto intro!: measurable_sets) ``` hoelzl@38656 ` 1078` ```next ``` hoelzl@38656 ` 1079` ``` assume *: "\a. {x\space M. a < f x} \ sets M" ``` hoelzl@38656 ` 1080` ``` hence **: "\a. {x\space M. f x < a} \ sets M" ``` hoelzl@38656 ` 1081` ``` unfolding less_eq_le_pinfreal_measurable ``` hoelzl@38656 ` 1082` ``` unfolding greater_eq_le_measurable . ``` hoelzl@35582 ` 1083` hoelzl@38656 ` 1084` ``` show "f \ borel_measurable M" unfolding borel_measurable_pinfreal_eq_real borel_measurable_iff_greater ``` hoelzl@38656 ` 1085` ``` proof safe ``` hoelzl@38656 ` 1086` ``` have "f -` {\} \ space M = space M - {x\space M. f x < \}" by auto ``` hoelzl@38656 ` 1087` ``` then show \: "f -` {\} \ space M \ sets M" using ** by auto ``` hoelzl@35582 ` 1088` hoelzl@38656 ` 1089` ``` fix a ``` hoelzl@38656 ` 1090` ``` have "{w \ space M. a < real (f w)} = ``` hoelzl@38656 ` 1091` ``` (if 0 \ a then {w\space M. Real a < f w} - (f -` {\} \ space M) else space M)" ``` hoelzl@38656 ` 1092` ``` proof (split split_if, safe del: notI) ``` hoelzl@38656 ` 1093` ``` fix x assume "0 \ a" ``` hoelzl@38656 ` 1094` ``` { assume "a < real (f x)" then show "Real a < f x" "x \ f -` {\} \ space M" ``` hoelzl@38656 ` 1095` ``` using `0 \ a` by (cases "f x", auto) } ``` hoelzl@38656 ` 1096` ``` { assume "Real a < f x" "x \ f -` {\}" then show "a < real (f x)" ``` hoelzl@38656 ` 1097` ``` using `0 \ a` by (cases "f x", auto) } ``` hoelzl@38656 ` 1098` ``` next ``` hoelzl@38656 ` 1099` ``` fix x assume "\ 0 \ a" then show "a < real (f x)" by (cases "f x") auto ``` hoelzl@38656 ` 1100` ``` qed ``` hoelzl@38656 ` 1101` ``` then show "{w \ space M. a < real (f w)} \ sets M" ``` hoelzl@38656 ` 1102` ``` using \ * by (auto intro!: Diff) ``` hoelzl@35582 ` 1103` ``` qed ``` hoelzl@35582 ` 1104` ```qed ``` hoelzl@35582 ` 1105` hoelzl@38656 ` 1106` ```lemma (in sigma_algebra) borel_measurable_pinfreal_iff_less: ``` hoelzl@38656 ` 1107` ``` "(f::'a \ pinfreal) \ borel_measurable M \ (\a. {x\space M. f x < a} \ sets M)" ``` hoelzl@38656 ` 1108` ``` using borel_measurable_pinfreal_iff_greater unfolding less_eq_le_pinfreal_measurable greater_eq_le_measurable . ``` hoelzl@38656 ` 1109` hoelzl@38656 ` 1110` ```lemma (in sigma_algebra) borel_measurable_pinfreal_iff_le: ``` hoelzl@38656 ` 1111` ``` "(f::'a \ pinfreal) \ borel_measurable M \ (\a. {x\space M. f x \ a} \ sets M)" ``` hoelzl@38656 ` 1112` ``` using borel_measurable_pinfreal_iff_greater unfolding less_eq_ge_measurable . ``` hoelzl@38656 ` 1113` hoelzl@38656 ` 1114` ```lemma (in sigma_algebra) borel_measurable_pinfreal_iff_ge: ``` hoelzl@38656 ` 1115` ``` "(f::'a \ pinfreal) \ borel_measurable M \ (\a. {x\space M. a \ f x} \ sets M)" ``` hoelzl@38656 ` 1116` ``` using borel_measurable_pinfreal_iff_greater unfolding less_eq_le_pinfreal_measurable . ``` hoelzl@38656 ` 1117` hoelzl@38656 ` 1118` ```lemma (in sigma_algebra) borel_measurable_pinfreal_eq_const: ``` hoelzl@38656 ` 1119` ``` fixes f :: "'a \ pinfreal" assumes "f \ borel_measurable M" ``` hoelzl@38656 ` 1120` ``` shows "{x\space M. f x = c} \ sets M" ``` hoelzl@38656 ` 1121` ```proof - ``` hoelzl@38656 ` 1122` ``` have "{x\space M. f x = c} = (f -` {c} \ space M)" by auto ``` hoelzl@38656 ` 1123` ``` then show ?thesis using assms by (auto intro!: measurable_sets) ``` hoelzl@38656 ` 1124` ```qed ``` hoelzl@38656 ` 1125` hoelzl@38656 ` 1126` ```lemma (in sigma_algebra) borel_measurable_pinfreal_neq_const: ``` hoelzl@38656 ` 1127` ``` fixes f :: "'a \ pinfreal" ``` hoelzl@38656 ` 1128` ``` assumes "f \ borel_measurable M" ``` hoelzl@38656 ` 1129` ``` shows "{x\space M. f x \ c} \ sets M" ``` hoelzl@38656 ` 1130` ```proof - ``` hoelzl@38656 ` 1131` ``` have "{x\space M. f x \ c} = space M - (f -` {c} \ space M)" by auto ``` hoelzl@38656 ` 1132` ``` then show ?thesis using assms by (auto intro!: measurable_sets) ``` hoelzl@38656 ` 1133` ```qed ``` hoelzl@38656 ` 1134` hoelzl@38656 ` 1135` ```lemma (in sigma_algebra) borel_measurable_pinfreal_less[intro,simp]: ``` hoelzl@38656 ` 1136` ``` fixes f g :: "'a \ pinfreal" ``` hoelzl@38656 ` 1137` ``` assumes f: "f \ borel_measurable M" ``` hoelzl@38656 ` 1138` ``` assumes g: "g \ borel_measurable M" ``` hoelzl@38656 ` 1139` ``` shows "{x \ space M. f x < g x} \ sets M" ``` hoelzl@38656 ` 1140` ```proof - ``` hoelzl@38656 ` 1141` ``` have "(\x. real (f x)) \ borel_measurable M" ``` hoelzl@38656 ` 1142` ``` "(\x. real (g x)) \ borel_measurable M" ``` hoelzl@38656 ` 1143` ``` using assms by (auto intro!: borel_measurable_real) ``` hoelzl@38656 ` 1144` ``` from borel_measurable_less[OF this] ``` hoelzl@38656 ` 1145` ``` have "{x \ space M. real (f x) < real (g x)} \ sets M" . ``` hoelzl@38656 ` 1146` ``` moreover have "{x \ space M. f x \ \} \ sets M" using f by (rule borel_measurable_pinfreal_neq_const) ``` hoelzl@38656 ` 1147` ``` moreover have "{x \ space M. g x = \} \ sets M" using g by (rule borel_measurable_pinfreal_eq_const) ``` hoelzl@38656 ` 1148` ``` moreover have "{x \ space M. g x \ \} \ sets M" using g by (rule borel_measurable_pinfreal_neq_const) ``` hoelzl@38656 ` 1149` ``` moreover have "{x \ space M. f x < g x} = ({x \ space M. g x = \} \ {x \ space M. f x \ \}) \ ``` hoelzl@38656 ` 1150` ``` ({x \ space M. g x \ \} \ {x \ space M. f x \ \} \ {x \ space M. real (f x) < real (g x)})" ``` hoelzl@38656 ` 1151` ``` by (auto simp: real_of_pinfreal_strict_mono_iff) ``` hoelzl@38656 ` 1152` ``` ultimately show ?thesis by auto ``` hoelzl@38656 ` 1153` ```qed ``` hoelzl@38656 ` 1154` hoelzl@38656 ` 1155` ```lemma (in sigma_algebra) borel_measurable_pinfreal_le[intro,simp]: ``` hoelzl@38656 ` 1156` ``` fixes f :: "'a \ pinfreal" ``` hoelzl@38656 ` 1157` ``` assumes f: "f \ borel_measurable M" ``` hoelzl@38656 ` 1158` ``` assumes g: "g \ borel_measurable M" ``` hoelzl@38656 ` 1159` ``` shows "{x \ space M. f x \ g x} \ sets M" ``` hoelzl@38656 ` 1160` ```proof - ``` hoelzl@38656 ` 1161` ``` have "{x \ space M. f x \ g x} = space M - {x \ space M. g x < f x}" by auto ``` hoelzl@38656 ` 1162` ``` then show ?thesis using g f by auto ``` hoelzl@38656 ` 1163` ```qed ``` hoelzl@38656 ` 1164` hoelzl@38656 ` 1165` ```lemma (in sigma_algebra) borel_measurable_pinfreal_eq[intro,simp]: ``` hoelzl@38656 ` 1166` ``` fixes f :: "'a \ pinfreal" ``` hoelzl@38656 ` 1167` ``` assumes f: "f \ borel_measurable M" ``` hoelzl@38656 ` 1168` ``` assumes g: "g \ borel_measurable M" ``` hoelzl@38656 ` 1169` ``` shows "{w \ space M. f w = g w} \ sets M" ``` hoelzl@38656 ` 1170` ```proof - ``` hoelzl@38656 ` 1171` ``` have "{x \ space M. f x = g x} = {x \ space M. g x \ f x} \ {x \ space M. f x \ g x}" by auto ``` hoelzl@38656 ` 1172` ``` then show ?thesis using g f by auto ``` hoelzl@38656 ` 1173` ```qed ``` hoelzl@38656 ` 1174` hoelzl@38656 ` 1175` ```lemma (in sigma_algebra) borel_measurable_pinfreal_neq[intro,simp]: ``` hoelzl@38656 ` 1176` ``` fixes f :: "'a \ pinfreal" ``` hoelzl@38656 ` 1177` ``` assumes f: "f \ borel_measurable M" ``` hoelzl@38656 ` 1178` ``` assumes g: "g \ borel_measurable M" ``` hoelzl@38656 ` 1179` ``` shows "{w \ space M. f w \ g w} \ sets M" ``` hoelzl@35692 ` 1180` ```proof - ``` hoelzl@38656 ` 1181` ``` have "{w \ space M. f w \ g w} = space M - {w \ space M. f w = g w}" by auto ``` hoelzl@38656 ` 1182` ``` thus ?thesis using f g by auto ``` hoelzl@38656 ` 1183` ```qed ``` hoelzl@38656 ` 1184` hoelzl@38656 ` 1185` ```lemma (in sigma_algebra) borel_measurable_pinfreal_add[intro, simp]: ``` hoelzl@38656 ` 1186` ``` fixes f :: "'a \ pinfreal" ``` hoelzl@38656 ` 1187` ``` assumes measure: "f \ borel_measurable M" "g \ borel_measurable M" ``` hoelzl@38656 ` 1188` ``` shows "(\x. f x + g x) \ borel_measurable M" ``` hoelzl@38656 ` 1189` ```proof - ``` hoelzl@38656 ` 1190` ``` have *: "(\x. f x + g x) = ``` hoelzl@38656 ` 1191` ``` (\x. if f x = \ then \ else if g x = \ then \ else Real (real (f x) + real (g x)))" ``` hoelzl@38656 ` 1192` ``` by (auto simp: expand_fun_eq pinfreal_noteq_omega_Ex) ``` hoelzl@38656 ` 1193` ``` show ?thesis using assms unfolding * ``` hoelzl@38656 ` 1194` ``` by (auto intro!: measurable_If) ``` hoelzl@38656 ` 1195` ```qed ``` hoelzl@38656 ` 1196` hoelzl@38656 ` 1197` ```lemma (in sigma_algebra) borel_measurable_pinfreal_times[intro, simp]: ``` hoelzl@38656 ` 1198` ``` fixes f :: "'a \ pinfreal" assumes "f \ borel_measurable M" "g \ borel_measurable M" ``` hoelzl@38656 ` 1199` ``` shows "(\x. f x * g x) \ borel_measurable M" ``` hoelzl@38656 ` 1200` ```proof - ``` hoelzl@38656 ` 1201` ``` have *: "(\x. f x * g x) = ``` hoelzl@38656 ` 1202` ``` (\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 ``` hoelzl@38656 ` 1203` ``` Real (real (f x) * real (g x)))" ``` hoelzl@38656 ` 1204` ``` by (auto simp: expand_fun_eq pinfreal_noteq_omega_Ex) ``` hoelzl@38656 ` 1205` ``` show ?thesis using assms unfolding * ``` hoelzl@38656 ` 1206` ``` by (auto intro!: measurable_If) ``` hoelzl@38656 ` 1207` ```qed ``` hoelzl@38656 ` 1208` hoelzl@38656 ` 1209` ```lemma (in sigma_algebra) borel_measurable_pinfreal_setsum[simp, intro]: ``` hoelzl@38656 ` 1210` ``` fixes f :: "'c \ 'a \ pinfreal" ``` hoelzl@38656 ` 1211` ``` assumes "\i. i \ S \ f i \ borel_measurable M" ``` hoelzl@38656 ` 1212` ``` shows "(\x. \i\S. f i x) \ borel_measurable M" ``` hoelzl@38656 ` 1213` ```proof cases ``` hoelzl@38656 ` 1214` ``` assume "finite S" ``` hoelzl@38656 ` 1215` ``` thus ?thesis using assms ``` hoelzl@38656 ` 1216` ``` by induct auto ``` hoelzl@38656 ` 1217` ```qed (simp add: borel_measurable_const) ``` hoelzl@38656 ` 1218` hoelzl@38656 ` 1219` ```lemma (in sigma_algebra) borel_measurable_pinfreal_min[intro, simp]: ``` hoelzl@38656 ` 1220` ``` fixes f g :: "'a \ pinfreal" ``` hoelzl@38656 ` 1221` ``` assumes "f \ borel_measurable M" ``` hoelzl@38656 ` 1222` ``` assumes "g \ borel_measurable M" ``` hoelzl@38656 ` 1223` ``` shows "(\x. min (g x) (f x)) \ borel_measurable M" ``` hoelzl@38656 ` 1224` ``` using assms unfolding min_def by (auto intro!: measurable_If) ``` hoelzl@38656 ` 1225` hoelzl@38656 ` 1226` ```lemma (in sigma_algebra) borel_measurable_pinfreal_max[intro]: ``` hoelzl@38656 ` 1227` ``` fixes f g :: "'a \ pinfreal" ``` hoelzl@38656 ` 1228` ``` assumes "f \ borel_measurable M" ``` hoelzl@38656 ` 1229` ``` and "g \ borel_measurable M" ``` hoelzl@38656 ` 1230` ``` shows "(\x. max (g x) (f x)) \ borel_measurable M" ``` hoelzl@38656 ` 1231` ``` using assms unfolding max_def by (auto intro!: measurable_If) ``` hoelzl@38656 ` 1232` hoelzl@38656 ` 1233` ```lemma (in sigma_algebra) borel_measurable_SUP[simp, intro]: ``` hoelzl@38656 ` 1234` ``` fixes f :: "'d\countable \ 'a \ pinfreal" ``` hoelzl@38656 ` 1235` ``` assumes "\i. i \ A \ f i \ borel_measurable M" ``` hoelzl@38656 ` 1236` ``` shows "(SUP i : A. f i) \ borel_measurable M" (is "?sup \ borel_measurable M") ``` hoelzl@38656 ` 1237` ``` unfolding borel_measurable_pinfreal_iff_greater ``` hoelzl@38656 ` 1238` ```proof safe ``` hoelzl@38656 ` 1239` ``` fix a ``` hoelzl@38656 ` 1240` ``` have "{x\space M. a < ?sup x} = (\i\A. {x\space M. a < f i x})" ``` hoelzl@38656 ` 1241` ``` by (auto simp: less_Sup_iff SUPR_def[where 'a=pinfreal] SUPR_fun_expand[where 'b=pinfreal]) ``` hoelzl@38656 ` 1242` ``` then show "{x\space M. a < ?sup x} \ sets M" ``` hoelzl@38656 ` 1243` ``` using assms by auto ``` hoelzl@38656 ` 1244` ```qed ``` hoelzl@38656 ` 1245` hoelzl@38656 ` 1246` ```lemma (in sigma_algebra) borel_measurable_INF[simp, intro]: ``` hoelzl@38656 ` 1247` ``` fixes f :: "'d :: countable \ 'a \ pinfreal" ``` hoelzl@38656 ` 1248` ``` assumes "\i. i \ A \ f i \ borel_measurable M" ``` hoelzl@38656 ` 1249` ``` shows "(INF i : A. f i) \ borel_measurable M" (is "?inf \ borel_measurable M") ``` hoelzl@38656 ` 1250` ``` unfolding borel_measurable_pinfreal_iff_less ``` hoelzl@38656 ` 1251` ```proof safe ``` hoelzl@38656 ` 1252` ``` fix a ``` hoelzl@38656 ` 1253` ``` have "{x\space M. ?inf x < a} = (\i\A. {x\space M. f i x < a})" ``` hoelzl@38656 ` 1254` ``` by (auto simp: Inf_less_iff INFI_def[where 'a=pinfreal] INFI_fun_expand) ``` hoelzl@38656 ` 1255` ``` then show "{x\space M. ?inf x < a} \ sets M" ``` hoelzl@38656 ` 1256` ``` using assms by auto ``` hoelzl@38656 ` 1257` ```qed ``` hoelzl@38656 ` 1258` hoelzl@38656 ` 1259` ```lemma (in sigma_algebra) borel_measurable_pinfreal_diff: ``` hoelzl@38656 ` 1260` ``` fixes f g :: "'a \ pinfreal" ``` hoelzl@38656 ` 1261` ``` assumes "f \ borel_measurable M" ``` hoelzl@38656 ` 1262` ``` assumes "g \ borel_measurable M" ``` hoelzl@38656 ` 1263` ``` shows "(\x. f x - g x) \ borel_measurable M" ``` hoelzl@38656 ` 1264` ``` unfolding borel_measurable_pinfreal_iff_greater ``` hoelzl@38656 ` 1265` ```proof safe ``` hoelzl@38656 ` 1266` ``` fix a ``` hoelzl@38656 ` 1267` ``` have "{x \ space M. a < f x - g x} = {x \ space M. g x + a < f x}" ``` hoelzl@38656 ` 1268` ``` by (simp add: pinfreal_less_minus_iff) ``` hoelzl@38656 ` 1269` ``` then show "{x \ space M. a < f x - g x} \ sets M" ``` hoelzl@38656 ` 1270` ``` using assms by auto ``` hoelzl@35692 ` 1271` ```qed ``` hoelzl@35692 ` 1272` paulson@33533 ` 1273` ```end ```