src/HOL/Probability/Borel_Space.thy
 author huffman Sun Apr 01 16:09:58 2012 +0200 (2012-04-01) changeset 47255 30a1692557b0 parent 46905 6b1c0a80a57a child 47694 05663f75964c permissions -rw-r--r--
removed Nat_Numeral.thy, moving all theorems elsewhere
 wenzelm@42150 ` 1` ```(* Title: HOL/Probability/Borel_Space.thy ``` hoelzl@42067 ` 2` ``` Author: Johannes Hölzl, TU München ``` hoelzl@42067 ` 3` ``` Author: Armin Heller, TU München ``` hoelzl@42067 ` 4` ```*) ``` hoelzl@38656 ` 5` hoelzl@38656 ` 6` ```header {*Borel spaces*} ``` paulson@33533 ` 7` hoelzl@40859 ` 8` ```theory Borel_Space ``` hoelzl@45288 ` 9` ``` imports Sigma_Algebra "~~/src/HOL/Multivariate_Analysis/Multivariate_Analysis" ``` paulson@33533 ` 10` ```begin ``` paulson@33533 ` 11` hoelzl@38656 ` 12` ```section "Generic Borel spaces" ``` paulson@33533 ` 13` huffman@44537 ` 14` ```definition "borel = sigma \ space = UNIV::'a::topological_space set, sets = {S. open S}\" ``` hoelzl@40859 ` 15` ```abbreviation "borel_measurable M \ measurable M borel" ``` paulson@33533 ` 16` hoelzl@40859 ` 17` ```interpretation borel: sigma_algebra borel ``` hoelzl@40859 ` 18` ``` by (auto simp: borel_def intro!: sigma_algebra_sigma) ``` paulson@33533 ` 19` paulson@33533 ` 20` ```lemma in_borel_measurable: ``` paulson@33533 ` 21` ``` "f \ borel_measurable M \ ``` huffman@44537 ` 22` ``` (\S \ sets (sigma \ space = UNIV, sets = {S. open S}\). ``` hoelzl@38656 ` 23` ``` f -` S \ space M \ sets M)" ``` hoelzl@40859 ` 24` ``` by (auto simp add: measurable_def borel_def) ``` paulson@33533 ` 25` hoelzl@40859 ` 26` ```lemma in_borel_measurable_borel: ``` hoelzl@38656 ` 27` ``` "f \ borel_measurable M \ ``` hoelzl@40859 ` 28` ``` (\S \ sets borel. ``` hoelzl@38656 ` 29` ``` f -` S \ space M \ sets M)" ``` hoelzl@40859 ` 30` ``` by (auto simp add: measurable_def borel_def) ``` paulson@33533 ` 31` hoelzl@40859 ` 32` ```lemma space_borel[simp]: "space borel = UNIV" ``` hoelzl@40859 ` 33` ``` unfolding borel_def by auto ``` hoelzl@38656 ` 34` hoelzl@40859 ` 35` ```lemma borel_open[simp]: ``` hoelzl@40859 ` 36` ``` assumes "open A" shows "A \ sets borel" ``` hoelzl@38656 ` 37` ```proof - ``` huffman@44537 ` 38` ``` have "A \ {S. open S}" unfolding mem_Collect_eq using assms . ``` hoelzl@40859 ` 39` ``` thus ?thesis unfolding borel_def sigma_def by (auto intro!: sigma_sets.Basic) ``` paulson@33533 ` 40` ```qed ``` paulson@33533 ` 41` hoelzl@40859 ` 42` ```lemma borel_closed[simp]: ``` hoelzl@40859 ` 43` ``` assumes "closed A" shows "A \ sets borel" ``` paulson@33533 ` 44` ```proof - ``` hoelzl@40859 ` 45` ``` have "space borel - (- A) \ sets borel" ``` hoelzl@40859 ` 46` ``` using assms unfolding closed_def by (blast intro: borel_open) ``` hoelzl@38656 ` 47` ``` thus ?thesis by simp ``` paulson@33533 ` 48` ```qed ``` paulson@33533 ` 49` hoelzl@41830 ` 50` ```lemma borel_comp[intro,simp]: "A \ sets borel \ - A \ sets borel" ``` hoelzl@41830 ` 51` ``` unfolding Compl_eq_Diff_UNIV by (intro borel.Diff) auto ``` hoelzl@41830 ` 52` hoelzl@38656 ` 53` ```lemma (in sigma_algebra) borel_measurable_vimage: ``` hoelzl@38656 ` 54` ``` fixes f :: "'a \ 'x::t2_space" ``` hoelzl@38656 ` 55` ``` assumes borel: "f \ borel_measurable M" ``` hoelzl@38656 ` 56` ``` shows "f -` {x} \ space M \ sets M" ``` hoelzl@38656 ` 57` ```proof (cases "x \ f ` space M") ``` hoelzl@38656 ` 58` ``` case True then obtain y where "x = f y" by auto ``` hoelzl@41969 ` 59` ``` from closed_singleton[of "f y"] ``` hoelzl@40859 ` 60` ``` have "{f y} \ sets borel" by (rule borel_closed) ``` hoelzl@38656 ` 61` ``` with assms show ?thesis ``` hoelzl@40859 ` 62` ``` unfolding in_borel_measurable_borel `x = f y` by auto ``` hoelzl@38656 ` 63` ```next ``` hoelzl@38656 ` 64` ``` case False hence "f -` {x} \ space M = {}" by auto ``` hoelzl@38656 ` 65` ``` thus ?thesis by auto ``` paulson@33533 ` 66` ```qed ``` paulson@33533 ` 67` hoelzl@38656 ` 68` ```lemma (in sigma_algebra) borel_measurableI: ``` hoelzl@38656 ` 69` ``` fixes f :: "'a \ 'x\topological_space" ``` hoelzl@38656 ` 70` ``` assumes "\S. open S \ f -` S \ space M \ sets M" ``` hoelzl@38656 ` 71` ``` shows "f \ borel_measurable M" ``` hoelzl@40859 ` 72` ``` unfolding borel_def ``` hoelzl@40859 ` 73` ```proof (rule measurable_sigma, simp_all) ``` huffman@44537 ` 74` ``` fix S :: "'x set" assume "open S" thus "f -` S \ space M \ sets M" ``` huffman@44537 ` 75` ``` using assms[of S] by simp ``` hoelzl@40859 ` 76` ```qed ``` paulson@33533 ` 77` hoelzl@40859 ` 78` ```lemma borel_singleton[simp, intro]: ``` hoelzl@38656 ` 79` ``` fixes x :: "'a::t1_space" ``` hoelzl@40859 ` 80` ``` shows "A \ sets borel \ insert x A \ sets borel" ``` hoelzl@40859 ` 81` ``` proof (rule borel.insert_in_sets) ``` hoelzl@40859 ` 82` ``` show "{x} \ sets borel" ``` hoelzl@41969 ` 83` ``` using closed_singleton[of x] by (rule borel_closed) ``` hoelzl@38656 ` 84` ``` qed simp ``` hoelzl@38656 ` 85` hoelzl@38656 ` 86` ```lemma (in sigma_algebra) borel_measurable_const[simp, intro]: ``` hoelzl@38656 ` 87` ``` "(\x. c) \ borel_measurable M" ``` hoelzl@38656 ` 88` ``` by (auto intro!: measurable_const) ``` paulson@33533 ` 89` hoelzl@39083 ` 90` ```lemma (in sigma_algebra) borel_measurable_indicator[simp, intro!]: ``` hoelzl@38656 ` 91` ``` assumes A: "A \ sets M" ``` hoelzl@38656 ` 92` ``` shows "indicator A \ borel_measurable M" ``` wenzelm@46905 ` 93` ``` unfolding indicator_def [abs_def] using A ``` hoelzl@38656 ` 94` ``` by (auto intro!: measurable_If_set borel_measurable_const) ``` paulson@33533 ` 95` hoelzl@40859 ` 96` ```lemma (in sigma_algebra) borel_measurable_indicator_iff: ``` hoelzl@40859 ` 97` ``` "(indicator A :: 'a \ 'x::{t1_space, zero_neq_one}) \ borel_measurable M \ A \ space M \ sets M" ``` hoelzl@40859 ` 98` ``` (is "?I \ borel_measurable M \ _") ``` hoelzl@40859 ` 99` ```proof ``` hoelzl@40859 ` 100` ``` assume "?I \ borel_measurable M" ``` hoelzl@40859 ` 101` ``` then have "?I -` {1} \ space M \ sets M" ``` hoelzl@40859 ` 102` ``` unfolding measurable_def by auto ``` hoelzl@40859 ` 103` ``` also have "?I -` {1} \ space M = A \ space M" ``` wenzelm@46905 ` 104` ``` unfolding indicator_def [abs_def] by auto ``` hoelzl@40859 ` 105` ``` finally show "A \ space M \ sets M" . ``` hoelzl@40859 ` 106` ```next ``` hoelzl@40859 ` 107` ``` assume "A \ space M \ sets M" ``` hoelzl@40859 ` 108` ``` moreover have "?I \ borel_measurable M \ ``` hoelzl@40859 ` 109` ``` (indicator (A \ space M) :: 'a \ 'x) \ borel_measurable M" ``` hoelzl@40859 ` 110` ``` by (intro measurable_cong) (auto simp: indicator_def) ``` hoelzl@40859 ` 111` ``` ultimately show "?I \ borel_measurable M" by auto ``` hoelzl@40859 ` 112` ```qed ``` hoelzl@40859 ` 113` hoelzl@39092 ` 114` ```lemma (in sigma_algebra) borel_measurable_restricted: ``` hoelzl@43920 ` 115` ``` fixes f :: "'a \ ereal" assumes "A \ sets M" ``` hoelzl@39092 ` 116` ``` shows "f \ borel_measurable (restricted_space A) \ ``` hoelzl@39092 ` 117` ``` (\x. f x * indicator A x) \ borel_measurable M" ``` hoelzl@39092 ` 118` ``` (is "f \ borel_measurable ?R \ ?f \ borel_measurable M") ``` hoelzl@39092 ` 119` ```proof - ``` hoelzl@39092 ` 120` ``` interpret R: sigma_algebra ?R by (rule restricted_sigma_algebra[OF `A \ sets M`]) ``` hoelzl@39092 ` 121` ``` have *: "f \ borel_measurable ?R \ ?f \ borel_measurable ?R" ``` hoelzl@39092 ` 122` ``` by (auto intro!: measurable_cong) ``` hoelzl@39092 ` 123` ``` show ?thesis unfolding * ``` hoelzl@40859 ` 124` ``` unfolding in_borel_measurable_borel ``` hoelzl@39092 ` 125` ``` proof (simp, safe) ``` hoelzl@43920 ` 126` ``` fix S :: "ereal set" assume "S \ sets borel" ``` hoelzl@40859 ` 127` ``` "\S\sets borel. ?f -` S \ A \ op \ A ` sets M" ``` hoelzl@39092 ` 128` ``` then have "?f -` S \ A \ op \ A ` sets M" by auto ``` hoelzl@39092 ` 129` ``` then have f: "?f -` S \ A \ sets M" ``` nipkow@44890 ` 130` ``` using `A \ sets M` sets_into_space by fastforce ``` hoelzl@39092 ` 131` ``` show "?f -` S \ space M \ sets M" ``` hoelzl@39092 ` 132` ``` proof cases ``` hoelzl@39092 ` 133` ``` assume "0 \ S" ``` hoelzl@39092 ` 134` ``` then have "?f -` S \ space M = ?f -` S \ A \ (space M - A)" ``` hoelzl@39092 ` 135` ``` using `A \ sets M` sets_into_space by auto ``` hoelzl@39092 ` 136` ``` then show ?thesis using f `A \ sets M` by (auto intro!: Un Diff) ``` hoelzl@39092 ` 137` ``` next ``` hoelzl@39092 ` 138` ``` assume "0 \ S" ``` hoelzl@39092 ` 139` ``` then have "?f -` S \ space M = ?f -` S \ A" ``` hoelzl@39092 ` 140` ``` using `A \ sets M` sets_into_space ``` hoelzl@39092 ` 141` ``` by (auto simp: indicator_def split: split_if_asm) ``` hoelzl@39092 ` 142` ``` then show ?thesis using f by auto ``` hoelzl@39092 ` 143` ``` qed ``` hoelzl@39092 ` 144` ``` next ``` hoelzl@43920 ` 145` ``` fix S :: "ereal set" assume "S \ sets borel" ``` hoelzl@40859 ` 146` ``` "\S\sets borel. ?f -` S \ space M \ sets M" ``` hoelzl@39092 ` 147` ``` then have f: "?f -` S \ space M \ sets M" by auto ``` hoelzl@39092 ` 148` ``` then show "?f -` S \ A \ op \ A ` sets M" ``` hoelzl@39092 ` 149` ``` using `A \ sets M` sets_into_space ``` hoelzl@39092 ` 150` ``` apply (simp add: image_iff) ``` hoelzl@39092 ` 151` ``` apply (rule bexI[OF _ f]) ``` hoelzl@39092 ` 152` ``` by auto ``` hoelzl@39092 ` 153` ``` qed ``` hoelzl@39092 ` 154` ```qed ``` hoelzl@39092 ` 155` hoelzl@39092 ` 156` ```lemma (in sigma_algebra) borel_measurable_subalgebra: ``` hoelzl@41545 ` 157` ``` assumes "sets N \ sets M" "space N = space M" "f \ borel_measurable N" ``` hoelzl@39092 ` 158` ``` shows "f \ borel_measurable M" ``` hoelzl@39092 ` 159` ``` using assms unfolding measurable_def by auto ``` hoelzl@39092 ` 160` hoelzl@38656 ` 161` ```section "Borel spaces on euclidean spaces" ``` hoelzl@38656 ` 162` hoelzl@38656 ` 163` ```lemma lessThan_borel[simp, intro]: ``` hoelzl@38656 ` 164` ``` fixes a :: "'a\ordered_euclidean_space" ``` hoelzl@40859 ` 165` ``` shows "{..< a} \ sets borel" ``` hoelzl@40859 ` 166` ``` by (blast intro: borel_open) ``` hoelzl@38656 ` 167` hoelzl@38656 ` 168` ```lemma greaterThan_borel[simp, intro]: ``` hoelzl@38656 ` 169` ``` fixes a :: "'a\ordered_euclidean_space" ``` hoelzl@40859 ` 170` ``` shows "{a <..} \ sets borel" ``` hoelzl@40859 ` 171` ``` by (blast intro: borel_open) ``` hoelzl@38656 ` 172` hoelzl@38656 ` 173` ```lemma greaterThanLessThan_borel[simp, intro]: ``` hoelzl@38656 ` 174` ``` fixes a b :: "'a\ordered_euclidean_space" ``` hoelzl@40859 ` 175` ``` shows "{a<.. sets borel" ``` hoelzl@40859 ` 176` ``` by (blast intro: borel_open) ``` hoelzl@38656 ` 177` hoelzl@38656 ` 178` ```lemma atMost_borel[simp, intro]: ``` hoelzl@38656 ` 179` ``` fixes a :: "'a\ordered_euclidean_space" ``` hoelzl@40859 ` 180` ``` shows "{..a} \ sets borel" ``` hoelzl@40859 ` 181` ``` by (blast intro: borel_closed) ``` hoelzl@38656 ` 182` hoelzl@38656 ` 183` ```lemma atLeast_borel[simp, intro]: ``` hoelzl@38656 ` 184` ``` fixes a :: "'a\ordered_euclidean_space" ``` hoelzl@40859 ` 185` ``` shows "{a..} \ sets borel" ``` hoelzl@40859 ` 186` ``` by (blast intro: borel_closed) ``` hoelzl@38656 ` 187` hoelzl@38656 ` 188` ```lemma atLeastAtMost_borel[simp, intro]: ``` hoelzl@38656 ` 189` ``` fixes a b :: "'a\ordered_euclidean_space" ``` hoelzl@40859 ` 190` ``` shows "{a..b} \ sets borel" ``` hoelzl@40859 ` 191` ``` by (blast intro: borel_closed) ``` paulson@33533 ` 192` hoelzl@38656 ` 193` ```lemma greaterThanAtMost_borel[simp, intro]: ``` hoelzl@38656 ` 194` ``` fixes a b :: "'a\ordered_euclidean_space" ``` hoelzl@40859 ` 195` ``` shows "{a<..b} \ sets borel" ``` hoelzl@38656 ` 196` ``` unfolding greaterThanAtMost_def by blast ``` hoelzl@38656 ` 197` hoelzl@38656 ` 198` ```lemma atLeastLessThan_borel[simp, intro]: ``` hoelzl@38656 ` 199` ``` fixes a b :: "'a\ordered_euclidean_space" ``` hoelzl@40859 ` 200` ``` shows "{a.. sets borel" ``` hoelzl@38656 ` 201` ``` unfolding atLeastLessThan_def by blast ``` hoelzl@38656 ` 202` hoelzl@38656 ` 203` ```lemma hafspace_less_borel[simp, intro]: ``` hoelzl@38656 ` 204` ``` fixes a :: real ``` hoelzl@40859 ` 205` ``` shows "{x::'a::euclidean_space. a < x \$\$ i} \ sets borel" ``` hoelzl@40859 ` 206` ``` by (auto intro!: borel_open open_halfspace_component_gt) ``` paulson@33533 ` 207` hoelzl@38656 ` 208` ```lemma hafspace_greater_borel[simp, intro]: ``` hoelzl@38656 ` 209` ``` fixes a :: real ``` hoelzl@40859 ` 210` ``` shows "{x::'a::euclidean_space. x \$\$ i < a} \ sets borel" ``` hoelzl@40859 ` 211` ``` by (auto intro!: borel_open open_halfspace_component_lt) ``` paulson@33533 ` 212` hoelzl@38656 ` 213` ```lemma hafspace_less_eq_borel[simp, intro]: ``` hoelzl@38656 ` 214` ``` fixes a :: real ``` hoelzl@40859 ` 215` ``` shows "{x::'a::euclidean_space. a \ x \$\$ i} \ sets borel" ``` hoelzl@40859 ` 216` ``` by (auto intro!: borel_closed closed_halfspace_component_ge) ``` paulson@33533 ` 217` hoelzl@38656 ` 218` ```lemma hafspace_greater_eq_borel[simp, intro]: ``` hoelzl@38656 ` 219` ``` fixes a :: real ``` hoelzl@40859 ` 220` ``` shows "{x::'a::euclidean_space. x \$\$ i \ a} \ sets borel" ``` hoelzl@40859 ` 221` ``` by (auto intro!: borel_closed closed_halfspace_component_le) ``` paulson@33533 ` 222` hoelzl@38656 ` 223` ```lemma (in sigma_algebra) borel_measurable_less[simp, intro]: ``` hoelzl@38656 ` 224` ``` fixes f :: "'a \ real" ``` paulson@33533 ` 225` ``` assumes f: "f \ borel_measurable M" ``` paulson@33533 ` 226` ``` assumes g: "g \ borel_measurable M" ``` paulson@33533 ` 227` ``` shows "{w \ space M. f w < g w} \ sets M" ``` paulson@33533 ` 228` ```proof - ``` paulson@33533 ` 229` ``` have "{w \ space M. f w < g w} = ``` hoelzl@38656 ` 230` ``` (\r. (f -` {..< of_rat r} \ space M) \ (g -` {of_rat r <..} \ space M))" ``` hoelzl@38656 ` 231` ``` using Rats_dense_in_real by (auto simp add: Rats_def) ``` hoelzl@38656 ` 232` ``` then show ?thesis using f g ``` hoelzl@38656 ` 233` ``` by simp (blast intro: measurable_sets) ``` paulson@33533 ` 234` ```qed ``` hoelzl@38656 ` 235` hoelzl@38656 ` 236` ```lemma (in sigma_algebra) borel_measurable_le[simp, intro]: ``` hoelzl@38656 ` 237` ``` fixes f :: "'a \ real" ``` paulson@33533 ` 238` ``` assumes f: "f \ borel_measurable M" ``` paulson@33533 ` 239` ``` assumes g: "g \ borel_measurable M" ``` paulson@33533 ` 240` ``` shows "{w \ space M. f w \ g w} \ sets M" ``` paulson@33533 ` 241` ```proof - ``` hoelzl@38656 ` 242` ``` have "{w \ space M. f w \ g w} = space M - {w \ space M. g w < f w}" ``` hoelzl@38656 ` 243` ``` by auto ``` hoelzl@38656 ` 244` ``` thus ?thesis using f g ``` hoelzl@38656 ` 245` ``` by simp blast ``` paulson@33533 ` 246` ```qed ``` paulson@33533 ` 247` hoelzl@38656 ` 248` ```lemma (in sigma_algebra) borel_measurable_eq[simp, intro]: ``` hoelzl@38656 ` 249` ``` fixes f :: "'a \ real" ``` paulson@33533 ` 250` ``` assumes f: "f \ borel_measurable M" ``` paulson@33533 ` 251` ``` assumes g: "g \ borel_measurable M" ``` paulson@33533 ` 252` ``` shows "{w \ space M. f w = g w} \ sets M" ``` paulson@33533 ` 253` ```proof - ``` paulson@33533 ` 254` ``` have "{w \ space M. f w = g w} = ``` wenzelm@33536 ` 255` ``` {w \ space M. f w \ g w} \ {w \ space M. g w \ f w}" ``` paulson@33533 ` 256` ``` by auto ``` hoelzl@38656 ` 257` ``` thus ?thesis using f g by auto ``` paulson@33533 ` 258` ```qed ``` paulson@33533 ` 259` hoelzl@38656 ` 260` ```lemma (in sigma_algebra) borel_measurable_neq[simp, intro]: ``` hoelzl@38656 ` 261` ``` fixes f :: "'a \ real" ``` paulson@33533 ` 262` ``` assumes f: "f \ borel_measurable M" ``` paulson@33533 ` 263` ``` assumes g: "g \ borel_measurable M" ``` paulson@33533 ` 264` ``` shows "{w \ space M. f w \ g w} \ sets M" ``` paulson@33533 ` 265` ```proof - ``` paulson@33533 ` 266` ``` have "{w \ space M. f w \ g w} = space M - {w \ space M. f w = g w}" ``` paulson@33533 ` 267` ``` by auto ``` hoelzl@38656 ` 268` ``` thus ?thesis using f g by auto ``` hoelzl@38656 ` 269` ```qed ``` hoelzl@38656 ` 270` hoelzl@38656 ` 271` ```subsection "Borel space equals sigma algebras over intervals" ``` hoelzl@38656 ` 272` hoelzl@38656 ` 273` ```lemma rational_boxes: ``` hoelzl@38656 ` 274` ``` fixes x :: "'a\ordered_euclidean_space" ``` hoelzl@38656 ` 275` ``` assumes "0 < e" ``` hoelzl@38656 ` 276` ``` shows "\a b. (\i. a \$\$ i \ \) \ (\i. b \$\$ i \ \) \ x \ {a <..< b} \ {a <..< b} \ ball x e" ``` hoelzl@38656 ` 277` ```proof - ``` hoelzl@38656 ` 278` ``` def e' \ "e / (2 * sqrt (real (DIM ('a))))" ``` hoelzl@38656 ` 279` ``` then have e: "0 < e'" using assms by (auto intro!: divide_pos_pos) ``` hoelzl@38656 ` 280` ``` have "\i. \y. y \ \ \ y < x \$\$ i \ x \$\$ i - y < e'" (is "\i. ?th i") ``` hoelzl@38656 ` 281` ``` proof ``` hoelzl@38656 ` 282` ``` fix i from Rats_dense_in_real[of "x \$\$ i - e'" "x \$\$ i"] e ``` hoelzl@38656 ` 283` ``` show "?th i" by auto ``` hoelzl@38656 ` 284` ``` qed ``` hoelzl@38656 ` 285` ``` from choice[OF this] guess a .. note a = this ``` hoelzl@38656 ` 286` ``` have "\i. \y. y \ \ \ x \$\$ i < y \ y - x \$\$ i < e'" (is "\i. ?th i") ``` hoelzl@38656 ` 287` ``` proof ``` hoelzl@38656 ` 288` ``` fix i from Rats_dense_in_real[of "x \$\$ i" "x \$\$ i + e'"] e ``` hoelzl@38656 ` 289` ``` show "?th i" by auto ``` hoelzl@38656 ` 290` ``` qed ``` hoelzl@38656 ` 291` ``` from choice[OF this] guess b .. note b = this ``` hoelzl@38656 ` 292` ``` { fix y :: 'a assume *: "Chi a < y" "y < Chi b" ``` hoelzl@38656 ` 293` ``` have "dist x y = sqrt (\i)" ``` hoelzl@38656 ` 294` ``` unfolding setL2_def[symmetric] by (rule euclidean_dist_l2) ``` hoelzl@38656 ` 295` ``` also have "\ < sqrt (\i {.. y\$\$i < b i" using * i eucl_less[where 'a='a] by auto ``` hoelzl@38656 ` 299` ``` moreover have "a i < x\$\$i" "x\$\$i - a i < e'" using a by auto ``` hoelzl@38656 ` 300` ``` moreover have "x\$\$i < b i" "b i - x\$\$i < e'" using b by auto ``` hoelzl@38656 ` 301` ``` ultimately have "\x\$\$i - y\$\$i\ < 2 * e'" by auto ``` hoelzl@38656 ` 302` ``` then have "dist (x \$\$ i) (y \$\$ i) < e/sqrt (real (DIM('a)))" ``` hoelzl@38656 ` 303` ``` unfolding e'_def by (auto simp: dist_real_def) ``` hoelzl@38656 ` 304` ``` then have "(dist (x \$\$ i) (y \$\$ i))\ < (e/sqrt (real (DIM('a))))\" ``` hoelzl@38656 ` 305` ``` by (rule power_strict_mono) auto ``` hoelzl@38656 ` 306` ``` then show "(dist (x \$\$ i) (y \$\$ i))\ < e\ / real DIM('a)" ``` hoelzl@38656 ` 307` ``` by (simp add: power_divide) ``` hoelzl@38656 ` 308` ``` qed auto ``` hoelzl@38656 ` 309` ``` also have "\ = e" using `0 < e` by (simp add: real_eq_of_nat DIM_positive) ``` hoelzl@38656 ` 310` ``` finally have "dist x y < e" . } ``` hoelzl@38656 ` 311` ``` with a b show ?thesis ``` hoelzl@38656 ` 312` ``` apply (rule_tac exI[of _ "Chi a"]) ``` hoelzl@38656 ` 313` ``` apply (rule_tac exI[of _ "Chi b"]) ``` hoelzl@38656 ` 314` ``` using eucl_less[where 'a='a] by auto ``` hoelzl@38656 ` 315` ```qed ``` hoelzl@38656 ` 316` hoelzl@38656 ` 317` ```lemma ex_rat_list: ``` hoelzl@38656 ` 318` ``` fixes x :: "'a\ordered_euclidean_space" ``` hoelzl@38656 ` 319` ``` assumes "\ i. x \$\$ i \ \" ``` hoelzl@38656 ` 320` ``` shows "\ r. length r = DIM('a) \ (\ i < DIM('a). of_rat (r ! i) = x \$\$ i)" ``` hoelzl@38656 ` 321` ```proof - ``` hoelzl@38656 ` 322` ``` have "\i. \r. x \$\$ i = of_rat r" using assms unfolding Rats_def by blast ``` hoelzl@38656 ` 323` ``` from choice[OF this] guess r .. ``` hoelzl@38656 ` 324` ``` then show ?thesis by (auto intro!: exI[of _ "map r [0 ..< DIM('a)]"]) ``` hoelzl@38656 ` 325` ```qed ``` hoelzl@38656 ` 326` hoelzl@38656 ` 327` ```lemma open_UNION: ``` hoelzl@38656 ` 328` ``` fixes M :: "'a\ordered_euclidean_space set" ``` hoelzl@38656 ` 329` ``` assumes "open M" ``` hoelzl@38656 ` 330` ``` shows "M = UNION {(a, b) | a b. {Chi (of_rat \ op ! a) <..< Chi (of_rat \ op ! b)} \ M} ``` hoelzl@38656 ` 331` ``` (\ (a, b). {Chi (of_rat \ op ! a) <..< Chi (of_rat \ op ! b)})" ``` hoelzl@38656 ` 332` ``` (is "M = UNION ?idx ?box") ``` hoelzl@38656 ` 333` ```proof safe ``` hoelzl@38656 ` 334` ``` fix x assume "x \ M" ``` hoelzl@38656 ` 335` ``` obtain e where e: "e > 0" "ball x e \ M" ``` hoelzl@38656 ` 336` ``` using openE[OF assms `x \ M`] by auto ``` hoelzl@38656 ` 337` ``` then obtain a b where ab: "x \ {a <..< b}" "\i. a \$\$ i \ \" "\i. b \$\$ i \ \" "{a <..< b} \ ball x e" ``` hoelzl@38656 ` 338` ``` using rational_boxes[OF e(1)] by blast ``` hoelzl@38656 ` 339` ``` then obtain p q where pq: "length p = DIM ('a)" ``` hoelzl@38656 ` 340` ``` "length q = DIM ('a)" ``` hoelzl@38656 ` 341` ``` "\ i < DIM ('a). of_rat (p ! i) = a \$\$ i \ of_rat (q ! i) = b \$\$ i" ``` hoelzl@38656 ` 342` ``` using ex_rat_list[OF ab(2)] ex_rat_list[OF ab(3)] by blast ``` hoelzl@38656 ` 343` ``` hence p: "Chi (of_rat \ op ! p) = a" ``` hoelzl@38656 ` 344` ``` using euclidean_eq[of "Chi (of_rat \ op ! p)" a] ``` hoelzl@38656 ` 345` ``` unfolding o_def by auto ``` hoelzl@38656 ` 346` ``` from pq have q: "Chi (of_rat \ op ! q) = b" ``` hoelzl@38656 ` 347` ``` using euclidean_eq[of "Chi (of_rat \ op ! q)" b] ``` hoelzl@38656 ` 348` ``` unfolding o_def by auto ``` hoelzl@38656 ` 349` ``` have "x \ ?box (p, q)" ``` hoelzl@38656 ` 350` ``` using p q ab by auto ``` hoelzl@38656 ` 351` ``` thus "x \ UNION ?idx ?box" using ab e p q exI[of _ p] exI[of _ q] by auto ``` hoelzl@38656 ` 352` ```qed auto ``` hoelzl@38656 ` 353` hoelzl@38656 ` 354` ```lemma halfspace_span_open: ``` hoelzl@40859 ` 355` ``` "sigma_sets UNIV (range (\ (a, i). {x\'a\ordered_euclidean_space. x \$\$ i < a})) ``` hoelzl@40859 ` 356` ``` \ sets borel" ``` hoelzl@40859 ` 357` ``` by (auto intro!: borel.sigma_sets_subset[simplified] borel_open ``` hoelzl@40859 ` 358` ``` open_halfspace_component_lt) ``` hoelzl@38656 ` 359` hoelzl@38656 ` 360` ```lemma halfspace_lt_in_halfspace: ``` hoelzl@40859 ` 361` ``` "{x\'a. x \$\$ i < a} \ sets (sigma \space=UNIV, sets=range (\ (a, i). {x\'a\ordered_euclidean_space. x \$\$ i < a})\)" ``` hoelzl@40859 ` 362` ``` by (auto intro!: sigma_sets.Basic simp: sets_sigma) ``` hoelzl@38656 ` 363` hoelzl@38656 ` 364` ```lemma halfspace_gt_in_halfspace: ``` hoelzl@40859 ` 365` ``` "{x\'a. a < x \$\$ i} \ sets (sigma \space=UNIV, sets=range (\ (a, i). {x\'a\ordered_euclidean_space. x \$\$ i < a})\)" ``` hoelzl@40859 ` 366` ``` (is "?set \ sets ?SIGMA") ``` hoelzl@38656 ` 367` ```proof - ``` hoelzl@40859 ` 368` ``` interpret sigma_algebra "?SIGMA" ``` hoelzl@40859 ` 369` ``` by (intro sigma_algebra_sigma_sets) (simp_all add: sets_sigma) ``` hoelzl@38656 ` 370` ``` have *: "?set = (\n. space ?SIGMA - {x\'a. x \$\$ i < a + 1 / real (Suc n)})" ``` hoelzl@38656 ` 371` ``` proof (safe, simp_all add: not_less) ``` hoelzl@38656 ` 372` ``` fix x assume "a < x \$\$ i" ``` hoelzl@38656 ` 373` ``` with reals_Archimedean[of "x \$\$ i - a"] ``` hoelzl@38656 ` 374` ``` obtain n where "a + 1 / real (Suc n) < x \$\$ i" ``` hoelzl@38656 ` 375` ``` by (auto simp: inverse_eq_divide field_simps) ``` hoelzl@38656 ` 376` ``` then show "\n. a + 1 / real (Suc n) \ x \$\$ i" ``` hoelzl@38656 ` 377` ``` by (blast intro: less_imp_le) ``` hoelzl@38656 ` 378` ``` next ``` hoelzl@38656 ` 379` ``` fix x n ``` hoelzl@38656 ` 380` ``` have "a < a + 1 / real (Suc n)" by auto ``` hoelzl@38656 ` 381` ``` also assume "\ \ x" ``` hoelzl@38656 ` 382` ``` finally show "a < x" . ``` hoelzl@38656 ` 383` ``` qed ``` hoelzl@38656 ` 384` ``` show "?set \ sets ?SIGMA" unfolding * ``` hoelzl@38656 ` 385` ``` by (safe intro!: countable_UN Diff halfspace_lt_in_halfspace) ``` paulson@33533 ` 386` ```qed ``` paulson@33533 ` 387` hoelzl@38656 ` 388` ```lemma open_span_halfspace: ``` hoelzl@40859 ` 389` ``` "sets borel \ sets (sigma \space=UNIV, sets=range (\ (a, i). {x::'a::ordered_euclidean_space. x \$\$ i < a})\)" ``` hoelzl@38656 ` 390` ``` (is "_ \ sets ?SIGMA") ``` hoelzl@40859 ` 391` ```proof - ``` hoelzl@40859 ` 392` ``` have "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) simp ``` hoelzl@38656 ` 393` ``` then interpret sigma_algebra ?SIGMA . ``` huffman@44537 ` 394` ``` { fix S :: "'a set" assume "S \ {S. open S}" ``` huffman@44537 ` 395` ``` then have "open S" unfolding mem_Collect_eq . ``` hoelzl@40859 ` 396` ``` from open_UNION[OF this] ``` hoelzl@40859 ` 397` ``` obtain I where *: "S = ``` hoelzl@40859 ` 398` ``` (\(a, b)\I. ``` hoelzl@40859 ` 399` ``` (\ i op ! a)::'a) \$\$ i < x \$\$ i}) \ ``` hoelzl@40859 ` 400` ``` (\ i op ! b)::'a) \$\$ i}))" ``` hoelzl@40859 ` 401` ``` unfolding greaterThanLessThan_def ``` hoelzl@40859 ` 402` ``` unfolding eucl_greaterThan_eq_halfspaces[where 'a='a] ``` hoelzl@40859 ` 403` ``` unfolding eucl_lessThan_eq_halfspaces[where 'a='a] ``` hoelzl@40859 ` 404` ``` by blast ``` hoelzl@40859 ` 405` ``` have "S \ sets ?SIGMA" ``` hoelzl@40859 ` 406` ``` unfolding * ``` hoelzl@40859 ` 407` ``` by (auto intro!: countable_UN Int countable_INT halfspace_lt_in_halfspace halfspace_gt_in_halfspace) } ``` hoelzl@40859 ` 408` ``` then show ?thesis unfolding borel_def ``` hoelzl@40859 ` 409` ``` by (intro sets_sigma_subset) auto ``` hoelzl@40859 ` 410` ```qed ``` hoelzl@38656 ` 411` hoelzl@38656 ` 412` ```lemma halfspace_span_halfspace_le: ``` hoelzl@40859 ` 413` ``` "sets (sigma \space=UNIV, sets=range (\ (a, i). {x\'a\ordered_euclidean_space. x \$\$ i < a})\) \ ``` hoelzl@40859 ` 414` ``` sets (sigma \space=UNIV, sets=range (\ (a, i). {x. x \$\$ i \ a})\)" ``` hoelzl@38656 ` 415` ``` (is "_ \ sets ?SIGMA") ``` hoelzl@40859 ` 416` ```proof - ``` hoelzl@40859 ` 417` ``` have "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto ``` hoelzl@38656 ` 418` ``` then interpret sigma_algebra ?SIGMA . ``` hoelzl@40859 ` 419` ``` { fix a i ``` hoelzl@40859 ` 420` ``` have *: "{x::'a. x\$\$i < a} = (\n. {x. x\$\$i \ a - 1/real (Suc n)})" ``` hoelzl@40859 ` 421` ``` proof (safe, simp_all) ``` hoelzl@40859 ` 422` ``` fix x::'a assume *: "x\$\$i < a" ``` hoelzl@40859 ` 423` ``` with reals_Archimedean[of "a - x\$\$i"] ``` hoelzl@40859 ` 424` ``` obtain n where "x \$\$ i < a - 1 / (real (Suc n))" ``` hoelzl@40859 ` 425` ``` by (auto simp: field_simps inverse_eq_divide) ``` hoelzl@40859 ` 426` ``` then show "\n. x \$\$ i \ a - 1 / (real (Suc n))" ``` hoelzl@40859 ` 427` ``` by (blast intro: less_imp_le) ``` hoelzl@40859 ` 428` ``` next ``` hoelzl@40859 ` 429` ``` fix x::'a and n ``` hoelzl@40859 ` 430` ``` assume "x\$\$i \ a - 1 / real (Suc n)" ``` hoelzl@40859 ` 431` ``` also have "\ < a" by auto ``` hoelzl@40859 ` 432` ``` finally show "x\$\$i < a" . ``` hoelzl@40859 ` 433` ``` qed ``` hoelzl@40859 ` 434` ``` have "{x. x\$\$i < a} \ sets ?SIGMA" unfolding * ``` hoelzl@40859 ` 435` ``` by (safe intro!: countable_UN) ``` hoelzl@40859 ` 436` ``` (auto simp: sets_sigma intro!: sigma_sets.Basic) } ``` hoelzl@40859 ` 437` ``` then show ?thesis by (intro sets_sigma_subset) auto ``` hoelzl@40859 ` 438` ```qed ``` hoelzl@38656 ` 439` hoelzl@38656 ` 440` ```lemma halfspace_span_halfspace_ge: ``` hoelzl@40859 ` 441` ``` "sets (sigma \space=UNIV, sets=range (\ (a, i). {x\'a\ordered_euclidean_space. x \$\$ i < a})\) \ ``` hoelzl@40859 ` 442` ``` sets (sigma \space=UNIV, sets=range (\ (a, i). {x. a \ x \$\$ i})\)" ``` hoelzl@38656 ` 443` ``` (is "_ \ sets ?SIGMA") ``` hoelzl@40859 ` 444` ```proof - ``` hoelzl@40859 ` 445` ``` have "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto ``` hoelzl@38656 ` 446` ``` then interpret sigma_algebra ?SIGMA . ``` hoelzl@40859 ` 447` ``` { fix a i have *: "{x::'a. x\$\$i < a} = space ?SIGMA - {x::'a. a \ x\$\$i}" by auto ``` hoelzl@40859 ` 448` ``` have "{x. x\$\$i < a} \ sets ?SIGMA" unfolding * ``` hoelzl@40859 ` 449` ``` by (safe intro!: Diff) ``` hoelzl@40859 ` 450` ``` (auto simp: sets_sigma intro!: sigma_sets.Basic) } ``` hoelzl@40859 ` 451` ``` then show ?thesis by (intro sets_sigma_subset) auto ``` hoelzl@40859 ` 452` ```qed ``` hoelzl@38656 ` 453` hoelzl@38656 ` 454` ```lemma halfspace_le_span_halfspace_gt: ``` hoelzl@40859 ` 455` ``` "sets (sigma \space=UNIV, sets=range (\ (a, i). {x\'a\ordered_euclidean_space. x \$\$ i \ a})\) \ ``` hoelzl@40859 ` 456` ``` sets (sigma \space=UNIV, sets=range (\ (a, i). {x. a < x \$\$ i})\)" ``` hoelzl@38656 ` 457` ``` (is "_ \ sets ?SIGMA") ``` hoelzl@40859 ` 458` ```proof - ``` hoelzl@40859 ` 459` ``` have "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto ``` hoelzl@38656 ` 460` ``` then interpret sigma_algebra ?SIGMA . ``` hoelzl@40859 ` 461` ``` { fix a i have *: "{x::'a. x\$\$i \ a} = space ?SIGMA - {x::'a. a < x\$\$i}" by auto ``` hoelzl@40859 ` 462` ``` have "{x. x\$\$i \ a} \ sets ?SIGMA" unfolding * ``` hoelzl@40859 ` 463` ``` by (safe intro!: Diff) ``` hoelzl@40859 ` 464` ``` (auto simp: sets_sigma intro!: sigma_sets.Basic) } ``` hoelzl@40859 ` 465` ``` then show ?thesis by (intro sets_sigma_subset) auto ``` hoelzl@40859 ` 466` ```qed ``` hoelzl@38656 ` 467` hoelzl@38656 ` 468` ```lemma halfspace_le_span_atMost: ``` hoelzl@40859 ` 469` ``` "sets (sigma \space=UNIV, sets=range (\ (a, i). {x\'a\ordered_euclidean_space. x \$\$ i \ a})\) \ ``` hoelzl@40859 ` 470` ``` sets (sigma \space=UNIV, sets=range (\a. {..a\'a\ordered_euclidean_space})\)" ``` hoelzl@38656 ` 471` ``` (is "_ \ sets ?SIGMA") ``` hoelzl@40859 ` 472` ```proof - ``` hoelzl@40859 ` 473` ``` have "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto ``` hoelzl@38656 ` 474` ``` then interpret sigma_algebra ?SIGMA . ``` hoelzl@40859 ` 475` ``` have "\a i. {x. x\$\$i \ a} \ sets ?SIGMA" ``` hoelzl@38656 ` 476` ``` proof cases ``` hoelzl@40859 ` 477` ``` fix a i assume "i < DIM('a)" ``` hoelzl@38656 ` 478` ``` then have *: "{x::'a. x\$\$i \ a} = (\k::nat. {.. (\\ n. if n = i then a else real k)})" ``` hoelzl@38656 ` 479` ``` proof (safe, simp_all add: eucl_le[where 'a='a] split: split_if_asm) ``` hoelzl@38656 ` 480` ``` fix x ``` hoelzl@38656 ` 481` ``` from real_arch_simple[of "Max ((\i. x\$\$i)`{..i. i < DIM('a) \ x\$\$i \ real k" ``` hoelzl@38656 ` 483` ``` by (subst (asm) Max_le_iff) auto ``` hoelzl@38656 ` 484` ``` then show "\k::nat. \ia. ia \ i \ ia < DIM('a) \ x \$\$ ia \ real k" ``` hoelzl@38656 ` 485` ``` by (auto intro!: exI[of _ k]) ``` hoelzl@38656 ` 486` ``` qed ``` hoelzl@38656 ` 487` ``` show "{x. x\$\$i \ a} \ sets ?SIGMA" unfolding * ``` hoelzl@38656 ` 488` ``` by (safe intro!: countable_UN) ``` hoelzl@38656 ` 489` ``` (auto simp: sets_sigma intro!: sigma_sets.Basic) ``` hoelzl@38656 ` 490` ``` next ``` hoelzl@40859 ` 491` ``` fix a i assume "\ i < DIM('a)" ``` hoelzl@38656 ` 492` ``` then show "{x. x\$\$i \ a} \ sets ?SIGMA" ``` hoelzl@38656 ` 493` ``` using top by auto ``` hoelzl@38656 ` 494` ``` qed ``` hoelzl@40859 ` 495` ``` then show ?thesis by (intro sets_sigma_subset) auto ``` hoelzl@40859 ` 496` ```qed ``` hoelzl@38656 ` 497` hoelzl@38656 ` 498` ```lemma halfspace_le_span_greaterThan: ``` hoelzl@40859 ` 499` ``` "sets (sigma \space=UNIV, sets=range (\ (a, i). {x\'a\ordered_euclidean_space. x \$\$ i \ a})\) \ ``` hoelzl@40859 ` 500` ``` sets (sigma \space=UNIV, sets=range (\a. {a<..})\)" ``` hoelzl@38656 ` 501` ``` (is "_ \ sets ?SIGMA") ``` hoelzl@40859 ` 502` ```proof - ``` hoelzl@40859 ` 503` ``` have "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto ``` hoelzl@38656 ` 504` ``` then interpret sigma_algebra ?SIGMA . ``` hoelzl@40859 ` 505` ``` have "\a i. {x. x\$\$i \ a} \ sets ?SIGMA" ``` hoelzl@38656 ` 506` ``` proof cases ``` hoelzl@40859 ` 507` ``` fix a i assume "i < DIM('a)" ``` hoelzl@38656 ` 508` ``` have "{x::'a. x\$\$i \ a} = space ?SIGMA - {x::'a. a < x\$\$i}" by auto ``` hoelzl@38656 ` 509` ``` 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 ` 519` ``` by (auto intro!: exI[of _ k]) ``` hoelzl@38656 ` 520` ``` qed ``` hoelzl@38656 ` 521` ``` finally show "{x. x\$\$i \ a} \ sets ?SIGMA" ``` hoelzl@38656 ` 522` ``` apply (simp only:) ``` hoelzl@38656 ` 523` ``` apply (safe intro!: countable_UN Diff) ``` wenzelm@46731 ` 524` ``` apply (auto simp: sets_sigma intro!: sigma_sets.Basic) ``` wenzelm@46731 ` 525` ``` done ``` hoelzl@38656 ` 526` ``` next ``` hoelzl@40859 ` 527` ``` fix a i assume "\ i < DIM('a)" ``` hoelzl@38656 ` 528` ``` then show "{x. x\$\$i \ a} \ sets ?SIGMA" ``` hoelzl@38656 ` 529` ``` using top by auto ``` hoelzl@38656 ` 530` ``` qed ``` hoelzl@40859 ` 531` ``` then show ?thesis by (intro sets_sigma_subset) auto ``` hoelzl@40859 ` 532` ```qed ``` hoelzl@40859 ` 533` hoelzl@40859 ` 534` ```lemma halfspace_le_span_lessThan: ``` hoelzl@40859 ` 535` ``` "sets (sigma \space=UNIV, sets=range (\ (a, i). {x\'a\ordered_euclidean_space. a \ x \$\$ i})\) \ ``` hoelzl@40859 ` 536` ``` sets (sigma \space=UNIV, sets=range (\a. {..)" ``` hoelzl@40859 ` 537` ``` (is "_ \ sets ?SIGMA") ``` hoelzl@40859 ` 538` ```proof - ``` hoelzl@40859 ` 539` ``` have "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto ``` hoelzl@40859 ` 540` ``` then interpret sigma_algebra ?SIGMA . ``` hoelzl@40859 ` 541` ``` have "\a i. {x. a \ x\$\$i} \ sets ?SIGMA" ``` hoelzl@40859 ` 542` ``` proof cases ``` hoelzl@40859 ` 543` ``` fix a i assume "i < DIM('a)" ``` hoelzl@40859 ` 544` ``` have "{x::'a. a \ x\$\$i} = space ?SIGMA - {x::'a. x\$\$i < a}" by auto ``` hoelzl@40859 ` 545` ``` also have *: "{x::'a. x\$\$i < a} = (\k::nat. {..< (\\ n. if n = i then a else real k)})" using `i k::nat. \ia. ia \ i \ ia < DIM('a) \ x \$\$ ia < real k" ``` hoelzl@40859 ` 555` ``` by (auto intro!: exI[of _ k]) ``` hoelzl@40859 ` 556` ``` qed ``` hoelzl@40859 ` 557` ``` finally show "{x. a \ x\$\$i} \ sets ?SIGMA" ``` hoelzl@40859 ` 558` ``` apply (simp only:) ``` hoelzl@40859 ` 559` ``` apply (safe intro!: countable_UN Diff) ``` wenzelm@46731 ` 560` ``` apply (auto simp: sets_sigma intro!: sigma_sets.Basic) ``` wenzelm@46731 ` 561` ``` done ``` hoelzl@40859 ` 562` ``` next ``` hoelzl@40859 ` 563` ``` fix a i assume "\ i < DIM('a)" ``` hoelzl@40859 ` 564` ``` then show "{x. a \ x\$\$i} \ sets ?SIGMA" ``` hoelzl@40859 ` 565` ``` using top by auto ``` hoelzl@40859 ` 566` ``` qed ``` hoelzl@40859 ` 567` ``` then show ?thesis by (intro sets_sigma_subset) auto ``` hoelzl@40859 ` 568` ```qed ``` hoelzl@40859 ` 569` hoelzl@40859 ` 570` ```lemma atMost_span_atLeastAtMost: ``` hoelzl@40859 ` 571` ``` "sets (sigma \space=UNIV, sets=range (\a. {..a\'a\ordered_euclidean_space})\) \ ``` hoelzl@40859 ` 572` ``` sets (sigma \space=UNIV, sets=range (\(a,b). {a..b})\)" ``` hoelzl@40859 ` 573` ``` (is "_ \ sets ?SIGMA") ``` hoelzl@40859 ` 574` ```proof - ``` hoelzl@40859 ` 575` ``` have "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto ``` hoelzl@40859 ` 576` ``` then interpret sigma_algebra ?SIGMA . ``` hoelzl@40859 ` 577` ``` { fix a::'a ``` hoelzl@40859 ` 578` ``` have *: "{..a} = (\n::nat. {- real n *\<^sub>R One .. a})" ``` hoelzl@40859 ` 579` ``` proof (safe, simp_all add: eucl_le[where 'a='a]) ``` hoelzl@40859 ` 580` ``` fix x ``` hoelzl@40859 ` 581` ``` from real_arch_simple[of "Max ((\i. - x\$\$i)`{.. real k" ``` hoelzl@40859 ` 585` ``` by (subst (asm) Max_le_iff) (auto simp: field_simps) ``` hoelzl@40859 ` 586` ``` then have "- real k \ x\$\$i" by simp } ``` hoelzl@40859 ` 587` ``` then show "\n::nat. \i x \$\$ i" ``` hoelzl@40859 ` 588` ``` by (auto intro!: exI[of _ k]) ``` hoelzl@40859 ` 589` ``` qed ``` hoelzl@40859 ` 590` ``` have "{..a} \ sets ?SIGMA" unfolding * ``` hoelzl@40859 ` 591` ``` by (safe intro!: countable_UN) ``` hoelzl@40859 ` 592` ``` (auto simp: sets_sigma intro!: sigma_sets.Basic) } ``` hoelzl@40859 ` 593` ``` then show ?thesis by (intro sets_sigma_subset) auto ``` hoelzl@40859 ` 594` ```qed ``` hoelzl@40859 ` 595` hoelzl@40859 ` 596` ```lemma borel_eq_atMost: ``` hoelzl@40859 ` 597` ``` "borel = (sigma \space=UNIV, sets=range (\ a. {.. a::'a\ordered_euclidean_space})\)" ``` hoelzl@40859 ` 598` ``` (is "_ = ?SIGMA") ``` hoelzl@40869 ` 599` ```proof (intro algebra.equality antisym) ``` hoelzl@40859 ` 600` ``` show "sets borel \ sets ?SIGMA" ``` hoelzl@40859 ` 601` ``` using halfspace_le_span_atMost halfspace_span_halfspace_le open_span_halfspace ``` hoelzl@40859 ` 602` ``` by auto ``` hoelzl@40859 ` 603` ``` show "sets ?SIGMA \ sets borel" ``` hoelzl@40859 ` 604` ``` by (rule borel.sets_sigma_subset) auto ``` hoelzl@40859 ` 605` ```qed auto ``` hoelzl@40859 ` 606` hoelzl@40859 ` 607` ```lemma borel_eq_atLeastAtMost: ``` hoelzl@40859 ` 608` ``` "borel = (sigma \space=UNIV, sets=range (\ (a :: 'a\ordered_euclidean_space, b). {a .. b})\)" ``` hoelzl@40859 ` 609` ``` (is "_ = ?SIGMA") ``` hoelzl@40869 ` 610` ```proof (intro algebra.equality antisym) ``` hoelzl@40859 ` 611` ``` show "sets borel \ sets ?SIGMA" ``` hoelzl@40859 ` 612` ``` using atMost_span_atLeastAtMost halfspace_le_span_atMost ``` hoelzl@40859 ` 613` ``` halfspace_span_halfspace_le open_span_halfspace ``` hoelzl@40859 ` 614` ``` by auto ``` hoelzl@40859 ` 615` ``` show "sets ?SIGMA \ sets borel" ``` hoelzl@40859 ` 616` ``` by (rule borel.sets_sigma_subset) auto ``` hoelzl@40859 ` 617` ```qed auto ``` hoelzl@40859 ` 618` hoelzl@40859 ` 619` ```lemma borel_eq_greaterThan: ``` hoelzl@40859 ` 620` ``` "borel = (sigma \space=UNIV, sets=range (\ (a :: 'a\ordered_euclidean_space). {a <..})\)" ``` hoelzl@40859 ` 621` ``` (is "_ = ?SIGMA") ``` hoelzl@40869 ` 622` ```proof (intro algebra.equality antisym) ``` hoelzl@40859 ` 623` ``` show "sets borel \ sets ?SIGMA" ``` hoelzl@40859 ` 624` ``` using halfspace_le_span_greaterThan ``` hoelzl@40859 ` 625` ``` halfspace_span_halfspace_le open_span_halfspace ``` hoelzl@40859 ` 626` ``` by auto ``` hoelzl@40859 ` 627` ``` show "sets ?SIGMA \ sets borel" ``` hoelzl@40859 ` 628` ``` by (rule borel.sets_sigma_subset) auto ``` hoelzl@40859 ` 629` ```qed auto ``` hoelzl@40859 ` 630` hoelzl@40859 ` 631` ```lemma borel_eq_lessThan: ``` hoelzl@40859 ` 632` ``` "borel = (sigma \space=UNIV, sets=range (\ (a :: 'a\ordered_euclidean_space). {..< a})\)" ``` hoelzl@40859 ` 633` ``` (is "_ = ?SIGMA") ``` hoelzl@40869 ` 634` ```proof (intro algebra.equality antisym) ``` hoelzl@40859 ` 635` ``` show "sets borel \ sets ?SIGMA" ``` hoelzl@40859 ` 636` ``` using halfspace_le_span_lessThan ``` hoelzl@40859 ` 637` ``` halfspace_span_halfspace_ge open_span_halfspace ``` hoelzl@40859 ` 638` ``` by auto ``` hoelzl@40859 ` 639` ``` show "sets ?SIGMA \ sets borel" ``` hoelzl@40859 ` 640` ``` by (rule borel.sets_sigma_subset) auto ``` hoelzl@40859 ` 641` ```qed auto ``` hoelzl@40859 ` 642` hoelzl@40859 ` 643` ```lemma borel_eq_greaterThanLessThan: ``` hoelzl@40859 ` 644` ``` "borel = (sigma \space=UNIV, sets=range (\ (a, b). {a <..< (b :: 'a \ ordered_euclidean_space)})\)" ``` hoelzl@40859 ` 645` ``` (is "_ = ?SIGMA") ``` hoelzl@40869 ` 646` ```proof (intro algebra.equality antisym) ``` hoelzl@40859 ` 647` ``` show "sets ?SIGMA \ sets borel" ``` hoelzl@40859 ` 648` ``` by (rule borel.sets_sigma_subset) auto ``` hoelzl@40859 ` 649` ``` show "sets borel \ sets ?SIGMA" ``` hoelzl@40859 ` 650` ``` proof - ``` hoelzl@40859 ` 651` ``` have "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto ``` hoelzl@40859 ` 652` ``` then interpret sigma_algebra ?SIGMA . ``` huffman@44537 ` 653` ``` { fix M :: "'a set" assume "M \ {S. open S}" ``` huffman@44537 ` 654` ``` then have "open M" by simp ``` hoelzl@40859 ` 655` ``` have "M \ sets ?SIGMA" ``` hoelzl@40859 ` 656` ``` apply (subst open_UNION[OF `open M`]) ``` hoelzl@40859 ` 657` ``` apply (safe intro!: countable_UN) ``` wenzelm@46731 ` 658` ``` apply (auto simp add: sigma_def intro!: sigma_sets.Basic) ``` wenzelm@46731 ` 659` ``` done } ``` hoelzl@40859 ` 660` ``` then show ?thesis ``` hoelzl@40859 ` 661` ``` unfolding borel_def by (intro sets_sigma_subset) auto ``` hoelzl@40859 ` 662` ``` qed ``` hoelzl@38656 ` 663` ```qed auto ``` hoelzl@38656 ` 664` hoelzl@42862 ` 665` ```lemma borel_eq_atLeastLessThan: ``` hoelzl@42862 ` 666` ``` "borel = sigma \space=UNIV, sets=range (\(a, b). {a ..< b :: real})\" (is "_ = ?S") ``` hoelzl@42862 ` 667` ```proof (intro algebra.equality antisym) ``` hoelzl@42862 ` 668` ``` interpret sigma_algebra ?S ``` hoelzl@42862 ` 669` ``` by (rule sigma_algebra_sigma) auto ``` hoelzl@42862 ` 670` ``` show "sets borel \ sets ?S" ``` hoelzl@42862 ` 671` ``` unfolding borel_eq_lessThan ``` hoelzl@42862 ` 672` ``` proof (intro sets_sigma_subset subsetI) ``` hoelzl@42862 ` 673` ``` have move_uminus: "\x y::real. -x \ y \ -y \ x" by auto ``` hoelzl@42862 ` 674` ``` fix A :: "real set" assume "A \ sets \space = UNIV, sets = range lessThan\" ``` hoelzl@42862 ` 675` ``` then obtain x where "A = {..< x}" by auto ``` hoelzl@42862 ` 676` ``` then have "A = (\i::nat. {-real i ..< x})" ``` hoelzl@42862 ` 677` ``` by (auto simp: move_uminus real_arch_simple) ``` hoelzl@42862 ` 678` ``` then show "A \ sets ?S" ``` hoelzl@42862 ` 679` ``` by (auto simp: sets_sigma intro!: sigma_sets.intros) ``` hoelzl@42862 ` 680` ``` qed simp ``` hoelzl@42862 ` 681` ``` show "sets ?S \ sets borel" ``` hoelzl@42862 ` 682` ``` by (intro borel.sets_sigma_subset) auto ``` hoelzl@42862 ` 683` ```qed simp_all ``` hoelzl@42862 ` 684` hoelzl@40859 ` 685` ```lemma borel_eq_halfspace_le: ``` hoelzl@40859 ` 686` ``` "borel = (sigma \space=UNIV, sets=range (\ (a, i). {x::'a::ordered_euclidean_space. x\$\$i \ a})\)" ``` hoelzl@40859 ` 687` ``` (is "_ = ?SIGMA") ``` hoelzl@40869 ` 688` ```proof (intro algebra.equality antisym) ``` hoelzl@40859 ` 689` ``` show "sets borel \ sets ?SIGMA" ``` hoelzl@40859 ` 690` ``` using open_span_halfspace halfspace_span_halfspace_le by auto ``` hoelzl@40859 ` 691` ``` show "sets ?SIGMA \ sets borel" ``` hoelzl@40859 ` 692` ``` by (rule borel.sets_sigma_subset) auto ``` hoelzl@40859 ` 693` ```qed auto ``` hoelzl@40859 ` 694` hoelzl@40859 ` 695` ```lemma borel_eq_halfspace_less: ``` hoelzl@40859 ` 696` ``` "borel = (sigma \space=UNIV, sets=range (\ (a, i). {x::'a::ordered_euclidean_space. x\$\$i < a})\)" ``` hoelzl@40859 ` 697` ``` (is "_ = ?SIGMA") ``` hoelzl@40869 ` 698` ```proof (intro algebra.equality antisym) ``` hoelzl@40859 ` 699` ``` show "sets borel \ sets ?SIGMA" ``` hoelzl@40859 ` 700` ``` using open_span_halfspace . ``` hoelzl@40859 ` 701` ``` show "sets ?SIGMA \ sets borel" ``` hoelzl@40859 ` 702` ``` by (rule borel.sets_sigma_subset) auto ``` hoelzl@38656 ` 703` ```qed auto ``` hoelzl@38656 ` 704` hoelzl@40859 ` 705` ```lemma borel_eq_halfspace_gt: ``` hoelzl@40859 ` 706` ``` "borel = (sigma \space=UNIV, sets=range (\ (a, i). {x::'a::ordered_euclidean_space. a < x\$\$i})\)" ``` hoelzl@40859 ` 707` ``` (is "_ = ?SIGMA") ``` hoelzl@40869 ` 708` ```proof (intro algebra.equality antisym) ``` hoelzl@40859 ` 709` ``` show "sets borel \ sets ?SIGMA" ``` hoelzl@40859 ` 710` ``` using halfspace_le_span_halfspace_gt open_span_halfspace halfspace_span_halfspace_le by auto ``` hoelzl@40859 ` 711` ``` show "sets ?SIGMA \ sets borel" ``` hoelzl@40859 ` 712` ``` by (rule borel.sets_sigma_subset) auto ``` hoelzl@40859 ` 713` ```qed auto ``` hoelzl@38656 ` 714` hoelzl@40859 ` 715` ```lemma borel_eq_halfspace_ge: ``` hoelzl@40859 ` 716` ``` "borel = (sigma \space=UNIV, sets=range (\ (a, i). {x::'a::ordered_euclidean_space. a \ x\$\$i})\)" ``` hoelzl@40859 ` 717` ``` (is "_ = ?SIGMA") ``` hoelzl@40869 ` 718` ```proof (intro algebra.equality antisym) ``` hoelzl@40859 ` 719` ``` show "sets borel \ sets ?SIGMA" ``` hoelzl@38656 ` 720` ``` using halfspace_span_halfspace_ge open_span_halfspace by auto ``` hoelzl@40859 ` 721` ``` show "sets ?SIGMA \ sets borel" ``` hoelzl@40859 ` 722` ``` by (rule borel.sets_sigma_subset) auto ``` hoelzl@40859 ` 723` ```qed auto ``` hoelzl@38656 ` 724` hoelzl@38656 ` 725` ```lemma (in sigma_algebra) borel_measurable_halfspacesI: ``` hoelzl@38656 ` 726` ``` fixes f :: "'a \ 'c\ordered_euclidean_space" ``` hoelzl@40859 ` 727` ``` assumes "borel = (sigma \space=UNIV, sets=range F\)" ``` hoelzl@38656 ` 728` ``` and "\a i. S a i = f -` F (a,i) \ space M" ``` hoelzl@38656 ` 729` ``` and "\a i. \ i < DIM('c) \ S a i \ sets M" ``` hoelzl@38656 ` 730` ``` shows "f \ borel_measurable M = (\ia::real. S a i \ sets M)" ``` hoelzl@38656 ` 731` ```proof safe ``` hoelzl@38656 ` 732` ``` fix a :: real and i assume i: "i < DIM('c)" and f: "f \ borel_measurable M" ``` hoelzl@38656 ` 733` ``` then show "S a i \ sets M" unfolding assms ``` hoelzl@38656 ` 734` ``` by (auto intro!: measurable_sets sigma_sets.Basic simp: assms(1) sigma_def) ``` hoelzl@38656 ` 735` ```next ``` hoelzl@38656 ` 736` ``` assume a: "\ia. S a i \ sets M" ``` hoelzl@38656 ` 737` ``` { fix a i have "S a i \ sets M" ``` hoelzl@38656 ` 738` ``` proof cases ``` hoelzl@38656 ` 739` ``` assume "i < DIM('c)" ``` hoelzl@38656 ` 740` ``` with a show ?thesis unfolding assms(2) by simp ``` hoelzl@38656 ` 741` ``` next ``` hoelzl@38656 ` 742` ``` assume "\ i < DIM('c)" ``` hoelzl@38656 ` 743` ``` from assms(3)[OF this] show ?thesis . ``` hoelzl@38656 ` 744` ``` qed } ``` hoelzl@40859 ` 745` ``` then have "f \ measurable M (sigma \space=UNIV, sets=range F\)" ``` hoelzl@38656 ` 746` ``` by (auto intro!: measurable_sigma simp: assms(2)) ``` hoelzl@38656 ` 747` ``` then show "f \ borel_measurable M" unfolding measurable_def ``` hoelzl@38656 ` 748` ``` unfolding assms(1) by simp ``` hoelzl@38656 ` 749` ```qed ``` hoelzl@38656 ` 750` hoelzl@38656 ` 751` ```lemma (in sigma_algebra) borel_measurable_iff_halfspace_le: ``` hoelzl@38656 ` 752` ``` fixes f :: "'a \ 'c\ordered_euclidean_space" ``` hoelzl@38656 ` 753` ``` shows "f \ borel_measurable M = (\ia. {w \ space M. f w \$\$ i \ a} \ sets M)" ``` hoelzl@40859 ` 754` ``` by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_le]) auto ``` hoelzl@38656 ` 755` hoelzl@38656 ` 756` ```lemma (in sigma_algebra) borel_measurable_iff_halfspace_less: ``` hoelzl@38656 ` 757` ``` fixes f :: "'a \ 'c\ordered_euclidean_space" ``` hoelzl@38656 ` 758` ``` shows "f \ borel_measurable M \ (\ia. {w \ space M. f w \$\$ i < a} \ sets M)" ``` hoelzl@40859 ` 759` ``` by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_less]) auto ``` hoelzl@38656 ` 760` hoelzl@38656 ` 761` ```lemma (in sigma_algebra) borel_measurable_iff_halfspace_ge: ``` hoelzl@38656 ` 762` ``` fixes f :: "'a \ 'c\ordered_euclidean_space" ``` hoelzl@38656 ` 763` ``` shows "f \ borel_measurable M = (\ia. {w \ space M. a \ f w \$\$ i} \ sets M)" ``` hoelzl@40859 ` 764` ``` by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_ge]) auto ``` hoelzl@38656 ` 765` hoelzl@38656 ` 766` ```lemma (in sigma_algebra) borel_measurable_iff_halfspace_greater: ``` hoelzl@38656 ` 767` ``` fixes f :: "'a \ 'c\ordered_euclidean_space" ``` hoelzl@38656 ` 768` ``` shows "f \ borel_measurable M \ (\ia. {w \ space M. a < f w \$\$ i} \ sets M)" ``` hoelzl@40859 ` 769` ``` by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_gt]) auto ``` hoelzl@38656 ` 770` hoelzl@38656 ` 771` ```lemma (in sigma_algebra) borel_measurable_iff_le: ``` hoelzl@38656 ` 772` ``` "(f::'a \ real) \ borel_measurable M = (\a. {w \ space M. f w \ a} \ sets M)" ``` hoelzl@38656 ` 773` ``` using borel_measurable_iff_halfspace_le[where 'c=real] by simp ``` hoelzl@38656 ` 774` hoelzl@38656 ` 775` ```lemma (in sigma_algebra) borel_measurable_iff_less: ``` hoelzl@38656 ` 776` ``` "(f::'a \ real) \ borel_measurable M = (\a. {w \ space M. f w < a} \ sets M)" ``` hoelzl@38656 ` 777` ``` using borel_measurable_iff_halfspace_less[where 'c=real] by simp ``` hoelzl@38656 ` 778` hoelzl@38656 ` 779` ```lemma (in sigma_algebra) borel_measurable_iff_ge: ``` hoelzl@38656 ` 780` ``` "(f::'a \ real) \ borel_measurable M = (\a. {w \ space M. a \ f w} \ sets M)" ``` hoelzl@38656 ` 781` ``` using borel_measurable_iff_halfspace_ge[where 'c=real] by simp ``` hoelzl@38656 ` 782` hoelzl@38656 ` 783` ```lemma (in sigma_algebra) borel_measurable_iff_greater: ``` hoelzl@38656 ` 784` ``` "(f::'a \ real) \ borel_measurable M = (\a. {w \ space M. a < f w} \ sets M)" ``` hoelzl@38656 ` 785` ``` using borel_measurable_iff_halfspace_greater[where 'c=real] by simp ``` hoelzl@38656 ` 786` hoelzl@41025 ` 787` ```lemma borel_measurable_euclidean_component: ``` hoelzl@40859 ` 788` ``` "(\x::'a::euclidean_space. x \$\$ i) \ borel_measurable borel" ``` hoelzl@40859 ` 789` ``` unfolding borel_def[where 'a=real] ``` hoelzl@40859 ` 790` ```proof (rule borel.measurable_sigma, simp_all) ``` huffman@44537 ` 791` ``` fix S::"real set" assume "open S" ``` hoelzl@39087 ` 792` ``` from open_vimage_euclidean_component[OF this] ``` hoelzl@40859 ` 793` ``` show "(\x. x \$\$ i) -` S \ sets borel" ``` hoelzl@40859 ` 794` ``` by (auto intro: borel_open) ``` hoelzl@40859 ` 795` ```qed ``` hoelzl@39087 ` 796` hoelzl@41025 ` 797` ```lemma (in sigma_algebra) borel_measurable_euclidean_space: ``` hoelzl@39087 ` 798` ``` fixes f :: "'a \ 'c::ordered_euclidean_space" ``` hoelzl@39087 ` 799` ``` shows "f \ borel_measurable M \ (\ix. f x \$\$ i) \ borel_measurable M)" ``` hoelzl@39087 ` 800` ```proof safe ``` hoelzl@39087 ` 801` ``` fix i assume "f \ borel_measurable M" ``` hoelzl@39087 ` 802` ``` then show "(\x. f x \$\$ i) \ borel_measurable M" ``` hoelzl@39087 ` 803` ``` using measurable_comp[of f _ _ "\x. x \$\$ i", unfolded comp_def] ``` hoelzl@41025 ` 804` ``` by (auto intro: borel_measurable_euclidean_component) ``` hoelzl@39087 ` 805` ```next ``` hoelzl@39087 ` 806` ``` assume f: "\ix. f x \$\$ i) \ borel_measurable M" ``` hoelzl@39087 ` 807` ``` then show "f \ borel_measurable M" ``` hoelzl@39087 ` 808` ``` unfolding borel_measurable_iff_halfspace_le by auto ``` hoelzl@39087 ` 809` ```qed ``` hoelzl@39087 ` 810` hoelzl@38656 ` 811` ```subsection "Borel measurable operators" ``` hoelzl@38656 ` 812` hoelzl@38656 ` 813` ```lemma (in sigma_algebra) affine_borel_measurable_vector: ``` hoelzl@38656 ` 814` ``` fixes f :: "'a \ 'x::real_normed_vector" ``` hoelzl@38656 ` 815` ``` assumes "f \ borel_measurable M" ``` hoelzl@38656 ` 816` ``` shows "(\x. a + b *\<^sub>R f x) \ borel_measurable M" ``` hoelzl@38656 ` 817` ```proof (rule borel_measurableI) ``` hoelzl@38656 ` 818` ``` fix S :: "'x set" assume "open S" ``` hoelzl@38656 ` 819` ``` show "(\x. a + b *\<^sub>R f x) -` S \ space M \ sets M" ``` hoelzl@38656 ` 820` ``` proof cases ``` hoelzl@38656 ` 821` ``` assume "b \ 0" ``` huffman@44537 ` 822` ``` with `open S` have "open ((\x. (- a + x) /\<^sub>R b) ` S)" (is "open ?S") ``` huffman@44537 ` 823` ``` by (auto intro!: open_affinity simp: scaleR_add_right) ``` hoelzl@40859 ` 824` ``` hence "?S \ sets borel" ``` hoelzl@40859 ` 825` ``` unfolding borel_def by (auto simp: sigma_def intro!: sigma_sets.Basic) ``` hoelzl@38656 ` 826` ``` moreover ``` hoelzl@38656 ` 827` ``` from `b \ 0` have "(\x. a + b *\<^sub>R f x) -` S = f -` ?S" ``` hoelzl@38656 ` 828` ``` apply auto by (rule_tac x="a + b *\<^sub>R f x" in image_eqI, simp_all) ``` hoelzl@40859 ` 829` ``` ultimately show ?thesis using assms unfolding in_borel_measurable_borel ``` hoelzl@38656 ` 830` ``` by auto ``` hoelzl@38656 ` 831` ``` qed simp ``` hoelzl@38656 ` 832` ```qed ``` hoelzl@38656 ` 833` hoelzl@38656 ` 834` ```lemma (in sigma_algebra) affine_borel_measurable: ``` hoelzl@38656 ` 835` ``` fixes g :: "'a \ real" ``` hoelzl@38656 ` 836` ``` assumes g: "g \ borel_measurable M" ``` hoelzl@38656 ` 837` ``` shows "(\x. a + (g x) * b) \ borel_measurable M" ``` hoelzl@38656 ` 838` ``` using affine_borel_measurable_vector[OF assms] by (simp add: mult_commute) ``` hoelzl@38656 ` 839` hoelzl@38656 ` 840` ```lemma (in sigma_algebra) borel_measurable_add[simp, intro]: ``` hoelzl@38656 ` 841` ``` fixes f :: "'a \ real" ``` paulson@33533 ` 842` ``` assumes f: "f \ borel_measurable M" ``` paulson@33533 ` 843` ``` assumes g: "g \ borel_measurable M" ``` paulson@33533 ` 844` ``` shows "(\x. f x + g x) \ borel_measurable M" ``` paulson@33533 ` 845` ```proof - ``` hoelzl@38656 ` 846` ``` have 1: "\a. {w\space M. a \ f w + g w} = {w \ space M. a + g w * -1 \ f w}" ``` paulson@33533 ` 847` ``` by auto ``` hoelzl@38656 ` 848` ``` have "\a. (\w. a + (g w) * -1) \ borel_measurable M" ``` hoelzl@38656 ` 849` ``` by (rule affine_borel_measurable [OF g]) ``` hoelzl@38656 ` 850` ``` then have "\a. {w \ space M. (\w. a + (g w) * -1)(w) \ f w} \ sets M" using f ``` hoelzl@38656 ` 851` ``` by auto ``` hoelzl@38656 ` 852` ``` then have "\a. {w \ space M. a \ f w + g w} \ sets M" ``` hoelzl@38656 ` 853` ``` by (simp add: 1) ``` hoelzl@38656 ` 854` ``` then show ?thesis ``` hoelzl@38656 ` 855` ``` by (simp add: borel_measurable_iff_ge) ``` paulson@33533 ` 856` ```qed ``` paulson@33533 ` 857` hoelzl@41026 ` 858` ```lemma (in sigma_algebra) borel_measurable_setsum[simp, intro]: ``` hoelzl@41026 ` 859` ``` fixes f :: "'c \ 'a \ real" ``` hoelzl@41026 ` 860` ``` assumes "\i. i \ S \ f i \ borel_measurable M" ``` hoelzl@41026 ` 861` ``` shows "(\x. \i\S. f i x) \ borel_measurable M" ``` hoelzl@41026 ` 862` ```proof cases ``` hoelzl@41026 ` 863` ``` assume "finite S" ``` hoelzl@41026 ` 864` ``` thus ?thesis using assms by induct auto ``` hoelzl@41026 ` 865` ```qed simp ``` hoelzl@41026 ` 866` hoelzl@38656 ` 867` ```lemma (in sigma_algebra) borel_measurable_square: ``` hoelzl@38656 ` 868` ``` fixes f :: "'a \ real" ``` paulson@33533 ` 869` ``` assumes f: "f \ borel_measurable M" ``` paulson@33533 ` 870` ``` shows "(\x. (f x)^2) \ borel_measurable M" ``` paulson@33533 ` 871` ```proof - ``` paulson@33533 ` 872` ``` { ``` paulson@33533 ` 873` ``` fix a ``` paulson@33533 ` 874` ``` have "{w \ space M. (f w)\ \ a} \ sets M" ``` paulson@33533 ` 875` ``` proof (cases rule: linorder_cases [of a 0]) ``` paulson@33533 ` 876` ``` case less ``` hoelzl@38656 ` 877` ``` hence "{w \ space M. (f w)\ \ a} = {}" ``` paulson@33533 ` 878` ``` by auto (metis less order_le_less_trans power2_less_0) ``` paulson@33533 ` 879` ``` also have "... \ sets M" ``` hoelzl@38656 ` 880` ``` by (rule empty_sets) ``` paulson@33533 ` 881` ``` finally show ?thesis . ``` paulson@33533 ` 882` ``` next ``` paulson@33533 ` 883` ``` case equal ``` hoelzl@38656 ` 884` ``` hence "{w \ space M. (f w)\ \ a} = ``` paulson@33533 ` 885` ``` {w \ space M. f w \ 0} \ {w \ space M. 0 \ f w}" ``` paulson@33533 ` 886` ``` by auto ``` paulson@33533 ` 887` ``` also have "... \ sets M" ``` hoelzl@38656 ` 888` ``` apply (insert f) ``` hoelzl@38656 ` 889` ``` apply (rule Int) ``` hoelzl@38656 ` 890` ``` apply (simp add: borel_measurable_iff_le) ``` hoelzl@38656 ` 891` ``` apply (simp add: borel_measurable_iff_ge) ``` paulson@33533 ` 892` ``` done ``` paulson@33533 ` 893` ``` finally show ?thesis . ``` paulson@33533 ` 894` ``` next ``` paulson@33533 ` 895` ``` case greater ``` paulson@33533 ` 896` ``` have "\x. (f x ^ 2 \ sqrt a ^ 2) = (- sqrt a \ f x & f x \ sqrt a)" ``` paulson@33533 ` 897` ``` by (metis abs_le_interval_iff abs_of_pos greater real_sqrt_abs ``` paulson@33533 ` 898` ``` real_sqrt_le_iff real_sqrt_power) ``` paulson@33533 ` 899` ``` hence "{w \ space M. (f w)\ \ a} = ``` hoelzl@38656 ` 900` ``` {w \ space M. -(sqrt a) \ f w} \ {w \ space M. f w \ sqrt a}" ``` paulson@33533 ` 901` ``` using greater by auto ``` paulson@33533 ` 902` ``` also have "... \ sets M" ``` hoelzl@38656 ` 903` ``` apply (insert f) ``` hoelzl@38656 ` 904` ``` apply (rule Int) ``` hoelzl@38656 ` 905` ``` apply (simp add: borel_measurable_iff_ge) ``` hoelzl@38656 ` 906` ``` apply (simp add: borel_measurable_iff_le) ``` paulson@33533 ` 907` ``` done ``` paulson@33533 ` 908` ``` finally show ?thesis . ``` paulson@33533 ` 909` ``` qed ``` paulson@33533 ` 910` ``` } ``` hoelzl@38656 ` 911` ``` thus ?thesis by (auto simp add: borel_measurable_iff_le) ``` paulson@33533 ` 912` ```qed ``` paulson@33533 ` 913` paulson@33533 ` 914` ```lemma times_eq_sum_squares: ``` paulson@33533 ` 915` ``` fixes x::real ``` paulson@33533 ` 916` ``` shows"x*y = ((x+y)^2)/4 - ((x-y)^ 2)/4" ``` hoelzl@38656 ` 917` ```by (simp add: power2_eq_square ring_distribs diff_divide_distrib [symmetric]) ``` paulson@33533 ` 918` hoelzl@38656 ` 919` ```lemma (in sigma_algebra) borel_measurable_uminus[simp, intro]: ``` hoelzl@38656 ` 920` ``` fixes g :: "'a \ real" ``` paulson@33533 ` 921` ``` assumes g: "g \ borel_measurable M" ``` paulson@33533 ` 922` ``` shows "(\x. - g x) \ borel_measurable M" ``` paulson@33533 ` 923` ```proof - ``` paulson@33533 ` 924` ``` have "(\x. - g x) = (\x. 0 + (g x) * -1)" ``` paulson@33533 ` 925` ``` by simp ``` hoelzl@38656 ` 926` ``` also have "... \ borel_measurable M" ``` hoelzl@38656 ` 927` ``` by (fast intro: affine_borel_measurable g) ``` paulson@33533 ` 928` ``` finally show ?thesis . ``` paulson@33533 ` 929` ```qed ``` paulson@33533 ` 930` hoelzl@38656 ` 931` ```lemma (in sigma_algebra) borel_measurable_times[simp, intro]: ``` hoelzl@38656 ` 932` ``` fixes f :: "'a \ real" ``` paulson@33533 ` 933` ``` assumes f: "f \ borel_measurable M" ``` paulson@33533 ` 934` ``` assumes g: "g \ borel_measurable M" ``` paulson@33533 ` 935` ``` shows "(\x. f x * g x) \ borel_measurable M" ``` paulson@33533 ` 936` ```proof - ``` paulson@33533 ` 937` ``` have 1: "(\x. 0 + (f x + g x)\ * inverse 4) \ borel_measurable M" ``` hoelzl@38656 ` 938` ``` using assms by (fast intro: affine_borel_measurable borel_measurable_square) ``` hoelzl@38656 ` 939` ``` have "(\x. -((f x + -g x) ^ 2 * inverse 4)) = ``` paulson@33533 ` 940` ``` (\x. 0 + ((f x + -g x) ^ 2 * inverse -4))" ``` hoelzl@35582 ` 941` ``` by (simp add: minus_divide_right) ``` hoelzl@38656 ` 942` ``` also have "... \ borel_measurable M" ``` hoelzl@38656 ` 943` ``` using f g by (fast intro: affine_borel_measurable borel_measurable_square f g) ``` paulson@33533 ` 944` ``` finally have 2: "(\x. -((f x + -g x) ^ 2 * inverse 4)) \ borel_measurable M" . ``` paulson@33533 ` 945` ``` show ?thesis ``` hoelzl@38656 ` 946` ``` apply (simp add: times_eq_sum_squares diff_minus) ``` hoelzl@38656 ` 947` ``` using 1 2 by simp ``` paulson@33533 ` 948` ```qed ``` paulson@33533 ` 949` hoelzl@41026 ` 950` ```lemma (in sigma_algebra) borel_measurable_setprod[simp, intro]: ``` hoelzl@41026 ` 951` ``` fixes f :: "'c \ 'a \ real" ``` hoelzl@41026 ` 952` ``` assumes "\i. i \ S \ f i \ borel_measurable M" ``` hoelzl@41026 ` 953` ``` shows "(\x. \i\S. f i x) \ borel_measurable M" ``` hoelzl@41026 ` 954` ```proof cases ``` hoelzl@41026 ` 955` ``` assume "finite S" ``` hoelzl@41026 ` 956` ``` thus ?thesis using assms by induct auto ``` hoelzl@41026 ` 957` ```qed simp ``` hoelzl@41026 ` 958` hoelzl@38656 ` 959` ```lemma (in sigma_algebra) borel_measurable_diff[simp, intro]: ``` hoelzl@38656 ` 960` ``` fixes f :: "'a \ real" ``` paulson@33533 ` 961` ``` assumes f: "f \ borel_measurable M" ``` paulson@33533 ` 962` ``` assumes g: "g \ borel_measurable M" ``` paulson@33533 ` 963` ``` shows "(\x. f x - g x) \ borel_measurable M" ``` hoelzl@38656 ` 964` ``` unfolding diff_minus using assms by fast ``` paulson@33533 ` 965` hoelzl@38656 ` 966` ```lemma (in sigma_algebra) borel_measurable_inverse[simp, intro]: ``` hoelzl@38656 ` 967` ``` fixes f :: "'a \ real" ``` hoelzl@35692 ` 968` ``` assumes "f \ borel_measurable M" ``` hoelzl@35692 ` 969` ``` shows "(\x. inverse (f x)) \ borel_measurable M" ``` hoelzl@38656 ` 970` ``` unfolding borel_measurable_iff_ge unfolding inverse_eq_divide ``` hoelzl@38656 ` 971` ```proof safe ``` hoelzl@38656 ` 972` ``` fix a :: real ``` hoelzl@38656 ` 973` ``` have *: "{w \ space M. a \ 1 / f w} = ``` hoelzl@38656 ` 974` ``` ({w \ space M. 0 < f w} \ {w \ space M. a * f w \ 1}) \ ``` hoelzl@38656 ` 975` ``` ({w \ space M. f w < 0} \ {w \ space M. 1 \ a * f w}) \ ``` hoelzl@38656 ` 976` ``` ({w \ space M. f w = 0} \ {w \ space M. a \ 0})" by (auto simp: le_divide_eq) ``` hoelzl@38656 ` 977` ``` show "{w \ space M. a \ 1 / f w} \ sets M" using assms unfolding * ``` hoelzl@38656 ` 978` ``` by (auto intro!: Int Un) ``` hoelzl@35692 ` 979` ```qed ``` hoelzl@35692 ` 980` hoelzl@38656 ` 981` ```lemma (in sigma_algebra) borel_measurable_divide[simp, intro]: ``` hoelzl@38656 ` 982` ``` fixes f :: "'a \ real" ``` hoelzl@35692 ` 983` ``` assumes "f \ borel_measurable M" ``` hoelzl@35692 ` 984` ``` and "g \ borel_measurable M" ``` hoelzl@35692 ` 985` ``` shows "(\x. f x / g x) \ borel_measurable M" ``` hoelzl@35692 ` 986` ``` unfolding field_divide_inverse ``` hoelzl@38656 ` 987` ``` by (rule borel_measurable_inverse borel_measurable_times assms)+ ``` hoelzl@38656 ` 988` hoelzl@38656 ` 989` ```lemma (in sigma_algebra) borel_measurable_max[intro, simp]: ``` hoelzl@38656 ` 990` ``` fixes f g :: "'a \ real" ``` hoelzl@38656 ` 991` ``` assumes "f \ borel_measurable M" ``` hoelzl@38656 ` 992` ``` assumes "g \ borel_measurable M" ``` hoelzl@38656 ` 993` ``` shows "(\x. max (g x) (f x)) \ borel_measurable M" ``` hoelzl@38656 ` 994` ``` unfolding borel_measurable_iff_le ``` hoelzl@38656 ` 995` ```proof safe ``` hoelzl@38656 ` 996` ``` fix a ``` hoelzl@38656 ` 997` ``` have "{x \ space M. max (g x) (f x) \ a} = ``` hoelzl@38656 ` 998` ``` {x \ space M. g x \ a} \ {x \ space M. f x \ a}" by auto ``` hoelzl@38656 ` 999` ``` thus "{x \ space M. max (g x) (f x) \ a} \ sets M" ``` hoelzl@38656 ` 1000` ``` using assms unfolding borel_measurable_iff_le ``` hoelzl@38656 ` 1001` ``` by (auto intro!: Int) ``` hoelzl@38656 ` 1002` ```qed ``` hoelzl@38656 ` 1003` hoelzl@38656 ` 1004` ```lemma (in sigma_algebra) borel_measurable_min[intro, simp]: ``` hoelzl@38656 ` 1005` ``` fixes f g :: "'a \ real" ``` hoelzl@38656 ` 1006` ``` assumes "f \ borel_measurable M" ``` hoelzl@38656 ` 1007` ``` assumes "g \ borel_measurable M" ``` hoelzl@38656 ` 1008` ``` shows "(\x. min (g x) (f x)) \ borel_measurable M" ``` hoelzl@38656 ` 1009` ``` unfolding borel_measurable_iff_ge ``` hoelzl@38656 ` 1010` ```proof safe ``` hoelzl@38656 ` 1011` ``` fix a ``` hoelzl@38656 ` 1012` ``` have "{x \ space M. a \ min (g x) (f x)} = ``` hoelzl@38656 ` 1013` ``` {x \ space M. a \ g x} \ {x \ space M. a \ f x}" by auto ``` hoelzl@38656 ` 1014` ``` thus "{x \ space M. a \ min (g x) (f x)} \ sets M" ``` hoelzl@38656 ` 1015` ``` using assms unfolding borel_measurable_iff_ge ``` hoelzl@38656 ` 1016` ``` by (auto intro!: Int) ``` hoelzl@38656 ` 1017` ```qed ``` hoelzl@38656 ` 1018` hoelzl@38656 ` 1019` ```lemma (in sigma_algebra) borel_measurable_abs[simp, intro]: ``` hoelzl@38656 ` 1020` ``` assumes "f \ borel_measurable M" ``` hoelzl@38656 ` 1021` ``` shows "(\x. \f x :: real\) \ borel_measurable M" ``` hoelzl@38656 ` 1022` ```proof - ``` hoelzl@38656 ` 1023` ``` have *: "\x. \f x\ = max 0 (f x) + max 0 (- f x)" by (simp add: max_def) ``` hoelzl@38656 ` 1024` ``` show ?thesis unfolding * using assms by auto ``` hoelzl@38656 ` 1025` ```qed ``` hoelzl@38656 ` 1026` hoelzl@41026 ` 1027` ```lemma borel_measurable_nth[simp, intro]: ``` hoelzl@41026 ` 1028` ``` "(\x::real^'n. x \$ i) \ borel_measurable borel" ``` hoelzl@41026 ` 1029` ``` using borel_measurable_euclidean_component ``` hoelzl@41026 ` 1030` ``` unfolding nth_conv_component by auto ``` hoelzl@41026 ` 1031` hoelzl@41830 ` 1032` ```lemma borel_measurable_continuous_on1: ``` hoelzl@41830 ` 1033` ``` fixes f :: "'a::topological_space \ 'b::t1_space" ``` hoelzl@41830 ` 1034` ``` assumes "continuous_on UNIV f" ``` hoelzl@41830 ` 1035` ``` shows "f \ borel_measurable borel" ``` hoelzl@41830 ` 1036` ``` apply(rule borel.borel_measurableI) ``` hoelzl@41830 ` 1037` ``` using continuous_open_preimage[OF assms] unfolding vimage_def by auto ``` hoelzl@41830 ` 1038` hoelzl@41830 ` 1039` ```lemma borel_measurable_continuous_on: ``` hoelzl@41830 ` 1040` ``` fixes f :: "'a::topological_space \ 'b::t1_space" ``` hoelzl@42990 ` 1041` ``` assumes cont: "continuous_on A f" "open A" ``` hoelzl@41830 ` 1042` ``` shows "(\x. if x \ A then f x else c) \ borel_measurable borel" (is "?f \ _") ``` hoelzl@41830 ` 1043` ```proof (rule borel.borel_measurableI) ``` hoelzl@41830 ` 1044` ``` fix S :: "'b set" assume "open S" ``` hoelzl@42990 ` 1045` ``` then have "open {x\A. f x \ S}" ``` hoelzl@41830 ` 1046` ``` by (intro continuous_open_preimage[OF cont]) auto ``` hoelzl@42990 ` 1047` ``` then have *: "{x\A. f x \ S} \ sets borel" by auto ``` hoelzl@42990 ` 1048` ``` have "?f -` S \ space borel = ``` hoelzl@42990 ` 1049` ``` {x\A. f x \ S} \ (if c \ S then space borel - A else {})" ``` hoelzl@42990 ` 1050` ``` by (auto split: split_if_asm) ``` hoelzl@42990 ` 1051` ``` also have "\ \ sets borel" ``` hoelzl@42990 ` 1052` ``` using * `open A` by (auto simp del: space_borel intro!: borel.Un) ``` hoelzl@42990 ` 1053` ``` finally show "?f -` S \ space borel \ sets borel" . ``` hoelzl@42990 ` 1054` ```qed ``` hoelzl@42990 ` 1055` hoelzl@42990 ` 1056` ```lemma (in sigma_algebra) convex_measurable: ``` hoelzl@42990 ` 1057` ``` fixes a b :: real ``` hoelzl@42990 ` 1058` ``` assumes X: "X \ borel_measurable M" "X ` space M \ { a <..< b}" ``` hoelzl@42990 ` 1059` ``` assumes q: "convex_on { a <..< b} q" ``` hoelzl@42990 ` 1060` ``` shows "q \ X \ borel_measurable M" ``` hoelzl@42990 ` 1061` ```proof - ``` hoelzl@42990 ` 1062` ``` have "(\x. if x \ {a <..< b} then q x else 0) \ borel_measurable borel" ``` hoelzl@42990 ` 1063` ``` proof (rule borel_measurable_continuous_on) ``` hoelzl@42990 ` 1064` ``` show "open {a<..x. if x \ {a <..< b} then q x else 0) \ X \ borel_measurable M" (is ?qX) ``` hoelzl@42990 ` 1069` ``` using X by (intro measurable_comp) auto ``` hoelzl@42990 ` 1070` ``` moreover have "?qX \ q \ X \ borel_measurable M" ``` hoelzl@42990 ` 1071` ``` using X by (intro measurable_cong) auto ``` hoelzl@42990 ` 1072` ``` ultimately show ?thesis by simp ``` hoelzl@41830 ` 1073` ```qed ``` hoelzl@41830 ` 1074` hoelzl@41830 ` 1075` ```lemma borel_measurable_borel_log: assumes "1 < b" shows "log b \ borel_measurable borel" ``` hoelzl@41830 ` 1076` ```proof - ``` hoelzl@41830 ` 1077` ``` { fix x :: real assume x: "x \ 0" ``` hoelzl@41830 ` 1078` ``` { fix x::real assume "x \ 0" then have "\u. exp u = x \ False" by auto } ``` hoelzl@41830 ` 1079` ``` from this[of x] x this[of 0] have "log b 0 = log b x" ``` hoelzl@41830 ` 1080` ``` by (auto simp: ln_def log_def) } ``` hoelzl@41830 ` 1081` ``` note log_imp = this ``` hoelzl@41830 ` 1082` ``` have "(\x. if x \ {0<..} then log b x else log b 0) \ borel_measurable borel" ``` hoelzl@41830 ` 1083` ``` proof (rule borel_measurable_continuous_on) ``` hoelzl@41830 ` 1084` ``` show "continuous_on {0<..} (log b)" ``` hoelzl@41830 ` 1085` ``` by (auto intro!: continuous_at_imp_continuous_on DERIV_log DERIV_isCont ``` hoelzl@41830 ` 1086` ``` simp: continuous_isCont[symmetric]) ``` hoelzl@41830 ` 1087` ``` show "open ({0<..}::real set)" by auto ``` hoelzl@41830 ` 1088` ``` qed ``` hoelzl@41830 ` 1089` ``` also have "(\x. if x \ {0<..} then log b x else log b 0) = log b" ``` hoelzl@41830 ` 1090` ``` by (simp add: fun_eq_iff not_less log_imp) ``` hoelzl@41830 ` 1091` ``` finally show ?thesis . ``` hoelzl@41830 ` 1092` ```qed ``` hoelzl@41830 ` 1093` hoelzl@41830 ` 1094` ```lemma (in sigma_algebra) borel_measurable_log[simp,intro]: ``` hoelzl@41830 ` 1095` ``` assumes f: "f \ borel_measurable M" and "1 < b" ``` hoelzl@41830 ` 1096` ``` shows "(\x. log b (f x)) \ borel_measurable M" ``` hoelzl@41830 ` 1097` ``` using measurable_comp[OF f borel_measurable_borel_log[OF `1 < b`]] ``` hoelzl@41830 ` 1098` ``` by (simp add: comp_def) ``` hoelzl@41830 ` 1099` hoelzl@41981 ` 1100` ```subsection "Borel space on the extended reals" ``` hoelzl@41981 ` 1101` hoelzl@43920 ` 1102` ```lemma borel_measurable_ereal_borel: ``` hoelzl@43920 ` 1103` ``` "ereal \ borel_measurable borel" ``` hoelzl@43920 ` 1104` ``` unfolding borel_def[where 'a=ereal] ``` hoelzl@41981 ` 1105` ```proof (rule borel.measurable_sigma) ``` huffman@44537 ` 1106` ``` fix X :: "ereal set" assume "X \ sets \space = UNIV, sets = {S. open S} \" ``` huffman@44537 ` 1107` ``` then have "open X" by simp ``` hoelzl@43920 ` 1108` ``` then have "open (ereal -` X \ space borel)" ``` hoelzl@43920 ` 1109` ``` by (simp add: open_ereal_vimage) ``` hoelzl@43920 ` 1110` ``` then show "ereal -` X \ space borel \ sets borel" by auto ``` hoelzl@41981 ` 1111` ```qed auto ``` hoelzl@41981 ` 1112` hoelzl@43920 ` 1113` ```lemma (in sigma_algebra) borel_measurable_ereal[simp, intro]: ``` hoelzl@43920 ` 1114` ``` assumes f: "f \ borel_measurable M" shows "(\x. ereal (f x)) \ borel_measurable M" ``` hoelzl@43920 ` 1115` ``` using measurable_comp[OF f borel_measurable_ereal_borel] unfolding comp_def . ``` hoelzl@41981 ` 1116` hoelzl@43920 ` 1117` ```lemma borel_measurable_real_of_ereal_borel: ``` hoelzl@43920 ` 1118` ``` "(real :: ereal \ real) \ borel_measurable borel" ``` hoelzl@41981 ` 1119` ``` unfolding borel_def[where 'a=real] ``` hoelzl@41981 ` 1120` ```proof (rule borel.measurable_sigma) ``` huffman@44537 ` 1121` ``` fix B :: "real set" assume "B \ sets \space = UNIV, sets = {S. open S} \" ``` huffman@44537 ` 1122` ``` then have "open B" by simp ``` hoelzl@43920 ` 1123` ``` have *: "ereal -` real -` (B - {0}) = B - {0}" by auto ``` hoelzl@43920 ` 1124` ``` have open_real: "open (real -` (B - {0}) :: ereal set)" ``` hoelzl@43920 ` 1125` ``` unfolding open_ereal_def * using `open B` by auto ``` hoelzl@43920 ` 1126` ``` show "(real -` B \ space borel :: ereal set) \ sets borel" ``` hoelzl@41981 ` 1127` ``` proof cases ``` hoelzl@41981 ` 1128` ``` assume "0 \ B" ``` hoelzl@43923 ` 1129` ``` then have *: "real -` B = real -` (B - {0}) \ {-\, \, 0::ereal}" ``` hoelzl@43920 ` 1130` ``` by (auto simp add: real_of_ereal_eq_0) ``` hoelzl@43920 ` 1131` ``` then show "(real -` B :: ereal set) \ space borel \ sets borel" ``` hoelzl@41981 ` 1132` ``` using open_real by auto ``` hoelzl@41981 ` 1133` ``` next ``` hoelzl@41981 ` 1134` ``` assume "0 \ B" ``` hoelzl@43920 ` 1135` ``` then have *: "(real -` B :: ereal set) = real -` (B - {0})" ``` hoelzl@43920 ` 1136` ``` by (auto simp add: real_of_ereal_eq_0) ``` hoelzl@43920 ` 1137` ``` then show "(real -` B :: ereal set) \ space borel \ sets borel" ``` hoelzl@41981 ` 1138` ``` using open_real by auto ``` hoelzl@41981 ` 1139` ``` qed ``` hoelzl@41981 ` 1140` ```qed auto ``` hoelzl@41981 ` 1141` hoelzl@43920 ` 1142` ```lemma (in sigma_algebra) borel_measurable_real_of_ereal[simp, intro]: ``` hoelzl@43920 ` 1143` ``` assumes f: "f \ borel_measurable M" shows "(\x. real (f x :: ereal)) \ borel_measurable M" ``` hoelzl@43920 ` 1144` ``` using measurable_comp[OF f borel_measurable_real_of_ereal_borel] unfolding comp_def . ``` hoelzl@41981 ` 1145` hoelzl@43920 ` 1146` ```lemma (in sigma_algebra) borel_measurable_ereal_iff: ``` hoelzl@43920 ` 1147` ``` shows "(\x. ereal (f x)) \ borel_measurable M \ f \ borel_measurable M" ``` hoelzl@41981 ` 1148` ```proof ``` hoelzl@43920 ` 1149` ``` assume "(\x. ereal (f x)) \ borel_measurable M" ``` hoelzl@43920 ` 1150` ``` from borel_measurable_real_of_ereal[OF this] ``` hoelzl@41981 ` 1151` ``` show "f \ borel_measurable M" by auto ``` hoelzl@41981 ` 1152` ```qed auto ``` hoelzl@41981 ` 1153` hoelzl@43920 ` 1154` ```lemma (in sigma_algebra) borel_measurable_ereal_iff_real: ``` hoelzl@43923 ` 1155` ``` fixes f :: "'a \ ereal" ``` hoelzl@43923 ` 1156` ``` shows "f \ borel_measurable M \ ``` hoelzl@41981 ` 1157` ``` ((\x. real (f x)) \ borel_measurable M \ f -` {\} \ space M \ sets M \ f -` {-\} \ space M \ sets M)" ``` hoelzl@41981 ` 1158` ```proof safe ``` hoelzl@41981 ` 1159` ``` assume *: "(\x. real (f x)) \ borel_measurable M" "f -` {\} \ space M \ sets M" "f -` {-\} \ space M \ sets M" ``` hoelzl@41981 ` 1160` ``` have "f -` {\} \ space M = {x\space M. f x = \}" "f -` {-\} \ space M = {x\space M. f x = -\}" by auto ``` hoelzl@41981 ` 1161` ``` with * have **: "{x\space M. f x = \} \ sets M" "{x\space M. f x = -\} \ sets M" by simp_all ``` wenzelm@46731 ` 1162` ``` let ?f = "\x. if f x = \ then \ else if f x = -\ then -\ else ereal (real (f x))" ``` hoelzl@41981 ` 1163` ``` have "?f \ borel_measurable M" using * ** by (intro measurable_If) auto ``` hoelzl@43920 ` 1164` ``` also have "?f = f" by (auto simp: fun_eq_iff ereal_real) ``` hoelzl@41981 ` 1165` ``` finally show "f \ borel_measurable M" . ``` hoelzl@43920 ` 1166` ```qed (auto intro: measurable_sets borel_measurable_real_of_ereal) ``` hoelzl@41830 ` 1167` hoelzl@38656 ` 1168` ```lemma (in sigma_algebra) less_eq_ge_measurable: ``` hoelzl@38656 ` 1169` ``` fixes f :: "'a \ 'c::linorder" ``` hoelzl@41981 ` 1170` ``` shows "f -` {a <..} \ space M \ sets M \ f -` {..a} \ space M \ sets M" ``` hoelzl@38656 ` 1171` ```proof ``` hoelzl@41981 ` 1172` ``` assume "f -` {a <..} \ space M \ sets M" ``` hoelzl@41981 ` 1173` ``` moreover have "f -` {..a} \ space M = space M - f -` {a <..} \ space M" by auto ``` hoelzl@41981 ` 1174` ``` ultimately show "f -` {..a} \ space M \ sets M" by auto ``` hoelzl@38656 ` 1175` ```next ``` hoelzl@41981 ` 1176` ``` assume "f -` {..a} \ space M \ sets M" ``` hoelzl@41981 ` 1177` ``` moreover have "f -` {a <..} \ space M = space M - f -` {..a} \ space M" by auto ``` hoelzl@41981 ` 1178` ``` ultimately show "f -` {a <..} \ space M \ sets M" by auto ``` hoelzl@38656 ` 1179` ```qed ``` hoelzl@35692 ` 1180` hoelzl@38656 ` 1181` ```lemma (in sigma_algebra) greater_eq_le_measurable: ``` hoelzl@38656 ` 1182` ``` fixes f :: "'a \ 'c::linorder" ``` hoelzl@41981 ` 1183` ``` shows "f -` {..< a} \ space M \ sets M \ f -` {a ..} \ space M \ sets M" ``` hoelzl@38656 ` 1184` ```proof ``` hoelzl@41981 ` 1185` ``` assume "f -` {a ..} \ space M \ sets M" ``` hoelzl@41981 ` 1186` ``` moreover have "f -` {..< a} \ space M = space M - f -` {a ..} \ space M" by auto ``` hoelzl@41981 ` 1187` ``` ultimately show "f -` {..< a} \ space M \ sets M" by auto ``` hoelzl@38656 ` 1188` ```next ``` hoelzl@41981 ` 1189` ``` assume "f -` {..< a} \ space M \ sets M" ``` hoelzl@41981 ` 1190` ``` moreover have "f -` {a ..} \ space M = space M - f -` {..< a} \ space M" by auto ``` hoelzl@41981 ` 1191` ``` ultimately show "f -` {a ..} \ space M \ sets M" by auto ``` hoelzl@38656 ` 1192` ```qed ``` hoelzl@38656 ` 1193` hoelzl@43920 ` 1194` ```lemma (in sigma_algebra) borel_measurable_uminus_borel_ereal: ``` hoelzl@43920 ` 1195` ``` "(uminus :: ereal \ ereal) \ borel_measurable borel" ``` hoelzl@41981 ` 1196` ```proof (subst borel_def, rule borel.measurable_sigma) ``` huffman@44537 ` 1197` ``` fix X :: "ereal set" assume "X \ sets \space = UNIV, sets = {S. open S}\" ``` huffman@44537 ` 1198` ``` then have "open X" by simp ``` hoelzl@41981 ` 1199` ``` have "uminus -` X = uminus ` X" by (force simp: image_iff) ``` hoelzl@43920 ` 1200` ``` then have "open (uminus -` X)" using `open X` ereal_open_uminus by auto ``` hoelzl@41981 ` 1201` ``` then show "uminus -` X \ space borel \ sets borel" by auto ``` hoelzl@41981 ` 1202` ```qed auto ``` hoelzl@41981 ` 1203` hoelzl@43920 ` 1204` ```lemma (in sigma_algebra) borel_measurable_uminus_ereal[intro]: ``` hoelzl@41981 ` 1205` ``` assumes "f \ borel_measurable M" ``` hoelzl@43920 ` 1206` ``` shows "(\x. - f x :: ereal) \ borel_measurable M" ``` hoelzl@43920 ` 1207` ``` using measurable_comp[OF assms borel_measurable_uminus_borel_ereal] by (simp add: comp_def) ``` hoelzl@41981 ` 1208` hoelzl@43920 ` 1209` ```lemma (in sigma_algebra) borel_measurable_uminus_eq_ereal[simp]: ``` hoelzl@43920 ` 1210` ``` "(\x. - f x :: ereal) \ borel_measurable M \ f \ borel_measurable M" (is "?l = ?r") ``` hoelzl@38656 ` 1211` ```proof ``` hoelzl@43920 ` 1212` ``` assume ?l from borel_measurable_uminus_ereal[OF this] show ?r by simp ``` hoelzl@41981 ` 1213` ```qed auto ``` hoelzl@41981 ` 1214` hoelzl@43920 ` 1215` ```lemma (in sigma_algebra) borel_measurable_eq_atMost_ereal: ``` hoelzl@43923 ` 1216` ``` fixes f :: "'a \ ereal" ``` hoelzl@43923 ` 1217` ``` shows "f \ borel_measurable M \ (\a. f -` {..a} \ space M \ sets M)" ``` hoelzl@41981 ` 1218` ```proof (intro iffI allI) ``` hoelzl@41981 ` 1219` ``` assume pos[rule_format]: "\a. f -` {..a} \ space M \ sets M" ``` hoelzl@41981 ` 1220` ``` show "f \ borel_measurable M" ``` hoelzl@43920 ` 1221` ``` unfolding borel_measurable_ereal_iff_real borel_measurable_iff_le ``` hoelzl@41981 ` 1222` ``` proof (intro conjI allI) ``` hoelzl@41981 ` 1223` ``` fix a :: real ``` hoelzl@43920 ` 1224` ``` { fix x :: ereal assume *: "\i::nat. real i < x" ``` hoelzl@41981 ` 1225` ``` have "x = \" ``` hoelzl@43920 ` 1226` ``` proof (rule ereal_top) ``` huffman@44666 ` 1227` ``` fix B from reals_Archimedean2[of B] guess n .. ``` hoelzl@43920 ` 1228` ``` then have "ereal B < real n" by auto ``` hoelzl@41981 ` 1229` ``` with * show "B \ x" by (metis less_trans less_imp_le) ``` hoelzl@41981 ` 1230` ``` qed } ``` hoelzl@41981 ` 1231` ``` then have "f -` {\} \ space M = space M - (\i::nat. f -` {.. real i} \ space M)" ``` hoelzl@41981 ` 1232` ``` by (auto simp: not_le) ``` hoelzl@41981 ` 1233` ``` then show "f -` {\} \ space M \ sets M" using pos by (auto simp del: UN_simps intro!: Diff) ``` hoelzl@41981 ` 1234` ``` moreover ``` hoelzl@43923 ` 1235` ``` have "{-\::ereal} = {..-\}" by auto ``` hoelzl@41981 ` 1236` ``` then show "f -` {-\} \ space M \ sets M" using pos by auto ``` hoelzl@43920 ` 1237` ``` moreover have "{x\space M. f x \ ereal a} \ sets M" ``` hoelzl@43920 ` 1238` ``` using pos[of "ereal a"] by (simp add: vimage_def Int_def conj_commute) ``` hoelzl@41981 ` 1239` ``` moreover have "{w \ space M. real (f w) \ a} = ``` hoelzl@43920 ` 1240` ``` (if a < 0 then {w \ space M. f w \ ereal a} - f -` {-\} \ space M ``` hoelzl@43920 ` 1241` ``` else {w \ space M. f w \ ereal a} \ (f -` {\} \ space M) \ (f -` {-\} \ space M))" (is "?l = ?r") ``` hoelzl@41981 ` 1242` ``` proof (intro set_eqI) fix x show "x \ ?l \ x \ ?r" by (cases "f x") auto qed ``` hoelzl@41981 ` 1243` ``` ultimately show "{w \ space M. real (f w) \ a} \ sets M" by auto ``` hoelzl@35582 ` 1244` ``` qed ``` hoelzl@41981 ` 1245` ```qed (simp add: measurable_sets) ``` hoelzl@35582 ` 1246` hoelzl@43920 ` 1247` ```lemma (in sigma_algebra) borel_measurable_eq_atLeast_ereal: ``` hoelzl@43920 ` 1248` ``` "(f::'a \ ereal) \ borel_measurable M \ (\a. f -` {a..} \ space M \ sets M)" ``` hoelzl@41981 ` 1249` ```proof ``` hoelzl@41981 ` 1250` ``` assume pos: "\a. f -` {a..} \ space M \ sets M" ``` hoelzl@41981 ` 1251` ``` moreover have "\a. (\x. - f x) -` {..a} = f -` {-a ..}" ``` hoelzl@43920 ` 1252` ``` by (auto simp: ereal_uminus_le_reorder) ``` hoelzl@41981 ` 1253` ``` ultimately have "(\x. - f x) \ borel_measurable M" ``` hoelzl@43920 ` 1254` ``` unfolding borel_measurable_eq_atMost_ereal by auto ``` hoelzl@41981 ` 1255` ``` then show "f \ borel_measurable M" by simp ``` hoelzl@41981 ` 1256` ```qed (simp add: measurable_sets) ``` hoelzl@35582 ` 1257` hoelzl@43920 ` 1258` ```lemma (in sigma_algebra) borel_measurable_ereal_iff_less: ``` hoelzl@43920 ` 1259` ``` "(f::'a \ ereal) \ borel_measurable M \ (\a. f -` {..< a} \ space M \ sets M)" ``` hoelzl@43920 ` 1260` ``` unfolding borel_measurable_eq_atLeast_ereal greater_eq_le_measurable .. ``` hoelzl@38656 ` 1261` hoelzl@43920 ` 1262` ```lemma (in sigma_algebra) borel_measurable_ereal_iff_ge: ``` hoelzl@43920 ` 1263` ``` "(f::'a \ ereal) \ borel_measurable M \ (\a. f -` {a <..} \ space M \ sets M)" ``` hoelzl@43920 ` 1264` ``` unfolding borel_measurable_eq_atMost_ereal less_eq_ge_measurable .. ``` hoelzl@38656 ` 1265` hoelzl@43920 ` 1266` ```lemma (in sigma_algebra) borel_measurable_ereal_eq_const: ``` hoelzl@43920 ` 1267` ``` fixes f :: "'a \ ereal" assumes "f \ borel_measurable M" ``` hoelzl@38656 ` 1268` ``` shows "{x\space M. f x = c} \ sets M" ``` hoelzl@38656 ` 1269` ```proof - ``` hoelzl@38656 ` 1270` ``` have "{x\space M. f x = c} = (f -` {c} \ space M)" by auto ``` hoelzl@38656 ` 1271` ``` then show ?thesis using assms by (auto intro!: measurable_sets) ``` hoelzl@38656 ` 1272` ```qed ``` hoelzl@38656 ` 1273` hoelzl@43920 ` 1274` ```lemma (in sigma_algebra) borel_measurable_ereal_neq_const: ``` hoelzl@43920 ` 1275` ``` fixes f :: "'a \ ereal" assumes "f \ borel_measurable M" ``` hoelzl@38656 ` 1276` ``` shows "{x\space M. f x \ c} \ sets M" ``` hoelzl@38656 ` 1277` ```proof - ``` hoelzl@38656 ` 1278` ``` have "{x\space M. f x \ c} = space M - (f -` {c} \ space M)" by auto ``` hoelzl@38656 ` 1279` ``` then show ?thesis using assms by (auto intro!: measurable_sets) ``` hoelzl@38656 ` 1280` ```qed ``` hoelzl@38656 ` 1281` hoelzl@43920 ` 1282` ```lemma (in sigma_algebra) borel_measurable_ereal_le[intro,simp]: ``` hoelzl@43920 ` 1283` ``` fixes f g :: "'a \ ereal" ``` hoelzl@41981 ` 1284` ``` assumes f: "f \ borel_measurable M" ``` hoelzl@41981 ` 1285` ``` assumes g: "g \ borel_measurable M" ``` hoelzl@41981 ` 1286` ``` shows "{x \ space M. f x \ g x} \ sets M" ``` hoelzl@41981 ` 1287` ```proof - ``` hoelzl@41981 ` 1288` ``` have "{x \ space M. f x \ g x} = ``` hoelzl@41981 ` 1289` ``` {x \ space M. real (f x) \ real (g x)} - (f -` {\, -\} \ space M \ g -` {\, -\} \ space M) \ ``` hoelzl@41981 ` 1290` ``` f -` {-\} \ space M \ g -` {\} \ space M" (is "?l = ?r") ``` hoelzl@41981 ` 1291` ``` proof (intro set_eqI) ``` hoelzl@43920 ` 1292` ``` fix x show "x \ ?l \ x \ ?r" by (cases rule: ereal2_cases[of "f x" "g x"]) auto ``` hoelzl@41981 ` 1293` ``` qed ``` hoelzl@41981 ` 1294` ``` with f g show ?thesis by (auto intro!: Un simp: measurable_sets) ``` hoelzl@41981 ` 1295` ```qed ``` hoelzl@41981 ` 1296` hoelzl@43920 ` 1297` ```lemma (in sigma_algebra) borel_measurable_ereal_less[intro,simp]: ``` hoelzl@43920 ` 1298` ``` fixes f :: "'a \ ereal" ``` hoelzl@38656 ` 1299` ``` assumes f: "f \ borel_measurable M" ``` hoelzl@38656 ` 1300` ``` assumes g: "g \ borel_measurable M" ``` hoelzl@38656 ` 1301` ``` shows "{x \ space M. f x < g x} \ sets M" ``` hoelzl@38656 ` 1302` ```proof - ``` hoelzl@41981 ` 1303` ``` have "{x \ space M. f x < g x} = space M - {x \ space M. g x \ f x}" by auto ``` hoelzl@38656 ` 1304` ``` then show ?thesis using g f by auto ``` hoelzl@38656 ` 1305` ```qed ``` hoelzl@38656 ` 1306` hoelzl@43920 ` 1307` ```lemma (in sigma_algebra) borel_measurable_ereal_eq[intro,simp]: ``` hoelzl@43920 ` 1308` ``` fixes f :: "'a \ ereal" ``` hoelzl@38656 ` 1309` ``` assumes f: "f \ borel_measurable M" ``` hoelzl@38656 ` 1310` ``` assumes g: "g \ borel_measurable M" ``` hoelzl@38656 ` 1311` ``` shows "{w \ space M. f w = g w} \ sets M" ``` hoelzl@38656 ` 1312` ```proof - ``` hoelzl@38656 ` 1313` ``` 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 ` 1314` ``` then show ?thesis using g f by auto ``` hoelzl@38656 ` 1315` ```qed ``` hoelzl@38656 ` 1316` hoelzl@43920 ` 1317` ```lemma (in sigma_algebra) borel_measurable_ereal_neq[intro,simp]: ``` hoelzl@43920 ` 1318` ``` fixes f :: "'a \ ereal" ``` hoelzl@38656 ` 1319` ``` assumes f: "f \ borel_measurable M" ``` hoelzl@38656 ` 1320` ``` assumes g: "g \ borel_measurable M" ``` hoelzl@38656 ` 1321` ``` shows "{w \ space M. f w \ g w} \ sets M" ``` hoelzl@35692 ` 1322` ```proof - ``` hoelzl@38656 ` 1323` ``` have "{w \ space M. f w \ g w} = space M - {w \ space M. f w = g w}" by auto ``` hoelzl@38656 ` 1324` ``` thus ?thesis using f g by auto ``` hoelzl@38656 ` 1325` ```qed ``` hoelzl@38656 ` 1326` hoelzl@41981 ` 1327` ```lemma (in sigma_algebra) split_sets: ``` hoelzl@41981 ` 1328` ``` "{x\space M. P x \ Q x} = {x\space M. P x} \ {x\space M. Q x}" ``` hoelzl@41981 ` 1329` ``` "{x\space M. P x \ Q x} = {x\space M. P x} \ {x\space M. Q x}" ``` hoelzl@41981 ` 1330` ``` by auto ``` hoelzl@41981 ` 1331` hoelzl@43920 ` 1332` ```lemma (in sigma_algebra) borel_measurable_ereal_add[intro, simp]: ``` hoelzl@43920 ` 1333` ``` fixes f :: "'a \ ereal" ``` hoelzl@41025 ` 1334` ``` assumes "f \ borel_measurable M" "g \ borel_measurable M" ``` hoelzl@38656 ` 1335` ``` shows "(\x. f x + g x) \ borel_measurable M" ``` hoelzl@38656 ` 1336` ```proof - ``` hoelzl@41981 ` 1337` ``` { fix x assume "x \ space M" then have "f x + g x = ``` hoelzl@41981 ` 1338` ``` (if f x = \ \ g x = \ then \ ``` hoelzl@41981 ` 1339` ``` else if f x = -\ \ g x = -\ then -\ ``` hoelzl@43920 ` 1340` ``` else ereal (real (f x) + real (g x)))" ``` hoelzl@43920 ` 1341` ``` by (cases rule: ereal2_cases[of "f x" "g x"]) auto } ``` hoelzl@41981 ` 1342` ``` with assms show ?thesis ``` hoelzl@41981 ` 1343` ``` by (auto cong: measurable_cong simp: split_sets ``` hoelzl@41981 ` 1344` ``` intro!: Un measurable_If measurable_sets) ``` hoelzl@38656 ` 1345` ```qed ``` hoelzl@38656 ` 1346` hoelzl@43920 ` 1347` ```lemma (in sigma_algebra) borel_measurable_ereal_setsum[simp, intro]: ``` hoelzl@43920 ` 1348` ``` fixes f :: "'c \ 'a \ ereal" ``` hoelzl@41096 ` 1349` ``` assumes "\i. i \ S \ f i \ borel_measurable M" ``` hoelzl@41096 ` 1350` ``` shows "(\x. \i\S. f i x) \ borel_measurable M" ``` hoelzl@41096 ` 1351` ```proof cases ``` hoelzl@41096 ` 1352` ``` assume "finite S" ``` hoelzl@41096 ` 1353` ``` thus ?thesis using assms ``` hoelzl@41096 ` 1354` ``` by induct auto ``` hoelzl@41096 ` 1355` ```qed (simp add: borel_measurable_const) ``` hoelzl@41096 ` 1356` hoelzl@43920 ` 1357` ```lemma (in sigma_algebra) borel_measurable_ereal_abs[intro, simp]: ``` hoelzl@43920 ` 1358` ``` fixes f :: "'a \ ereal" assumes "f \ borel_measurable M" ``` hoelzl@41981 ` 1359` ``` shows "(\x. \f x\) \ borel_measurable M" ``` hoelzl@41981 ` 1360` ```proof - ``` hoelzl@41981 ` 1361` ``` { fix x have "\f x\ = (if 0 \ f x then f x else - f x)" by auto } ``` hoelzl@41981 ` 1362` ``` then show ?thesis using assms by (auto intro!: measurable_If) ``` hoelzl@41981 ` 1363` ```qed ``` hoelzl@41981 ` 1364` hoelzl@43920 ` 1365` ```lemma (in sigma_algebra) borel_measurable_ereal_times[intro, simp]: ``` hoelzl@43920 ` 1366` ``` fixes f :: "'a \ ereal" assumes "f \ borel_measurable M" "g \ borel_measurable M" ``` hoelzl@38656 ` 1367` ``` shows "(\x. f x * g x) \ borel_measurable M" ``` hoelzl@38656 ` 1368` ```proof - ``` hoelzl@43920 ` 1369` ``` { fix f g :: "'a \ ereal" ``` hoelzl@41981 ` 1370` ``` assume b: "f \ borel_measurable M" "g \ borel_measurable M" ``` hoelzl@41981 ` 1371` ``` and pos: "\x. 0 \ f x" "\x. 0 \ g x" ``` hoelzl@41981 ` 1372` ``` { fix x have *: "f x * g x = (if f x = 0 \ g x = 0 then 0 ``` hoelzl@41981 ` 1373` ``` else if f x = \ \ g x = \ then \ ``` hoelzl@43920 ` 1374` ``` else ereal (real (f x) * real (g x)))" ``` hoelzl@43920 ` 1375` ``` apply (cases rule: ereal2_cases[of "f x" "g x"]) ``` hoelzl@41981 ` 1376` ``` using pos[of x] by auto } ``` hoelzl@41981 ` 1377` ``` with b have "(\x. f x * g x) \ borel_measurable M" ``` hoelzl@41981 ` 1378` ``` by (auto cong: measurable_cong simp: split_sets ``` hoelzl@41981 ` 1379` ``` intro!: Un measurable_If measurable_sets) } ``` hoelzl@41981 ` 1380` ``` note pos_times = this ``` hoelzl@38656 ` 1381` ``` have *: "(\x. f x * g x) = ``` hoelzl@41981 ` 1382` ``` (\x. if 0 \ f x \ 0 \ g x \ f x < 0 \ g x < 0 then \f x\ * \g x\ else - (\f x\ * \g x\))" ``` hoelzl@41981 ` 1383` ``` by (auto simp: fun_eq_iff) ``` hoelzl@38656 ` 1384` ``` show ?thesis using assms unfolding * ``` hoelzl@43920 ` 1385` ``` by (intro measurable_If pos_times borel_measurable_uminus_ereal) ``` hoelzl@41981 ` 1386` ``` (auto simp: split_sets intro!: Int) ``` hoelzl@38656 ` 1387` ```qed ``` hoelzl@38656 ` 1388` hoelzl@43920 ` 1389` ```lemma (in sigma_algebra) borel_measurable_ereal_setprod[simp, intro]: ``` hoelzl@43920 ` 1390` ``` fixes f :: "'c \ 'a \ ereal" ``` hoelzl@38656 ` 1391` ``` assumes "\i. i \ S \ f i \ borel_measurable M" ``` hoelzl@41096 ` 1392` ``` shows "(\x. \i\S. f i x) \ borel_measurable M" ``` hoelzl@38656 ` 1393` ```proof cases ``` hoelzl@38656 ` 1394` ``` assume "finite S" ``` hoelzl@41096 ` 1395` ``` thus ?thesis using assms by induct auto ``` hoelzl@41096 ` 1396` ```qed simp ``` hoelzl@38656 ` 1397` hoelzl@43920 ` 1398` ```lemma (in sigma_algebra) borel_measurable_ereal_min[simp, intro]: ``` hoelzl@43920 ` 1399` ``` fixes f g :: "'a \ ereal" ``` hoelzl@38656 ` 1400` ``` assumes "f \ borel_measurable M" ``` hoelzl@38656 ` 1401` ``` assumes "g \ borel_measurable M" ``` hoelzl@38656 ` 1402` ``` shows "(\x. min (g x) (f x)) \ borel_measurable M" ``` hoelzl@38656 ` 1403` ``` using assms unfolding min_def by (auto intro!: measurable_If) ``` hoelzl@38656 ` 1404` hoelzl@43920 ` 1405` ```lemma (in sigma_algebra) borel_measurable_ereal_max[simp, intro]: ``` hoelzl@43920 ` 1406` ``` fixes f g :: "'a \ ereal" ``` hoelzl@38656 ` 1407` ``` assumes "f \ borel_measurable M" ``` hoelzl@38656 ` 1408` ``` and "g \ borel_measurable M" ``` hoelzl@38656 ` 1409` ``` shows "(\x. max (g x) (f x)) \ borel_measurable M" ``` hoelzl@38656 ` 1410` ``` using assms unfolding max_def by (auto intro!: measurable_If) ``` hoelzl@38656 ` 1411` hoelzl@38656 ` 1412` ```lemma (in sigma_algebra) borel_measurable_SUP[simp, intro]: ``` hoelzl@43920 ` 1413` ``` fixes f :: "'d\countable \ 'a \ ereal" ``` hoelzl@38656 ` 1414` ``` assumes "\i. i \ A \ f i \ borel_measurable M" ``` hoelzl@41097 ` 1415` ``` shows "(\x. SUP i : A. f i x) \ borel_measurable M" (is "?sup \ borel_measurable M") ``` hoelzl@43920 ` 1416` ``` unfolding borel_measurable_ereal_iff_ge ``` hoelzl@41981 ` 1417` ```proof ``` hoelzl@38656 ` 1418` ``` fix a ``` hoelzl@41981 ` 1419` ``` have "?sup -` {a<..} \ space M = (\i\A. {x\space M. a < f i x})" ``` noschinl@46884 ` 1420` ``` by (auto simp: less_SUP_iff) ``` hoelzl@41981 ` 1421` ``` then show "?sup -` {a<..} \ space M \ sets M" ``` hoelzl@38656 ` 1422` ``` using assms by auto ``` hoelzl@38656 ` 1423` ```qed ``` hoelzl@38656 ` 1424` hoelzl@38656 ` 1425` ```lemma (in sigma_algebra) borel_measurable_INF[simp, intro]: ``` hoelzl@43920 ` 1426` ``` fixes f :: "'d :: countable \ 'a \ ereal" ``` hoelzl@38656 ` 1427` ``` assumes "\i. i \ A \ f i \ borel_measurable M" ``` hoelzl@41097 ` 1428` ``` shows "(\x. INF i : A. f i x) \ borel_measurable M" (is "?inf \ borel_measurable M") ``` hoelzl@43920 ` 1429` ``` unfolding borel_measurable_ereal_iff_less ``` hoelzl@41981 ` 1430` ```proof ``` hoelzl@38656 ` 1431` ``` fix a ``` hoelzl@41981 ` 1432` ``` have "?inf -` {.. space M = (\i\A. {x\space M. f i x < a})" ``` noschinl@46884 ` 1433` ``` by (auto simp: INF_less_iff) ``` hoelzl@41981 ` 1434` ``` then show "?inf -` {.. space M \ sets M" ``` hoelzl@38656 ` 1435` ``` using assms by auto ``` hoelzl@38656 ` 1436` ```qed ``` hoelzl@38656 ` 1437` hoelzl@41981 ` 1438` ```lemma (in sigma_algebra) borel_measurable_liminf[simp, intro]: ``` hoelzl@43920 ` 1439` ``` fixes f :: "nat \ 'a \ ereal" ``` hoelzl@41981 ` 1440` ``` assumes "\i. f i \ borel_measurable M" ``` hoelzl@41981 ` 1441` ``` shows "(\x. liminf (\i. f i x)) \ borel_measurable M" ``` hoelzl@41981 ` 1442` ``` unfolding liminf_SUPR_INFI using assms by auto ``` hoelzl@41981 ` 1443` hoelzl@41981 ` 1444` ```lemma (in sigma_algebra) borel_measurable_limsup[simp, intro]: ``` hoelzl@43920 ` 1445` ``` fixes f :: "nat \ 'a \ ereal" ``` hoelzl@41981 ` 1446` ``` assumes "\i. f i \ borel_measurable M" ``` hoelzl@41981 ` 1447` ``` shows "(\x. limsup (\i. f i x)) \ borel_measurable M" ``` hoelzl@41981 ` 1448` ``` unfolding limsup_INFI_SUPR using assms by auto ``` hoelzl@41981 ` 1449` hoelzl@43920 ` 1450` ```lemma (in sigma_algebra) borel_measurable_ereal_diff[simp, intro]: ``` hoelzl@43920 ` 1451` ``` fixes f g :: "'a \ ereal" ``` hoelzl@38656 ` 1452` ``` assumes "f \ borel_measurable M" ``` hoelzl@38656 ` 1453` ``` assumes "g \ borel_measurable M" ``` hoelzl@38656 ` 1454` ``` shows "(\x. f x - g x) \ borel_measurable M" ``` hoelzl@43920 ` 1455` ``` unfolding minus_ereal_def using assms by auto ``` hoelzl@35692 ` 1456` hoelzl@40870 ` 1457` ```lemma (in sigma_algebra) borel_measurable_psuminf[simp, intro]: ``` hoelzl@43920 ` 1458` ``` fixes f :: "nat \ 'a \ ereal" ``` hoelzl@41981 ` 1459` ``` assumes "\i. f i \ borel_measurable M" and pos: "\i x. x \ space M \ 0 \ f i x" ``` hoelzl@41981 ` 1460` ``` shows "(\x. (\i. f i x)) \ borel_measurable M" ``` hoelzl@41981 ` 1461` ``` apply (subst measurable_cong) ``` hoelzl@43920 ` 1462` ``` apply (subst suminf_ereal_eq_SUPR) ``` hoelzl@41981 ` 1463` ``` apply (rule pos) ``` hoelzl@41981 ` 1464` ``` using assms by auto ``` hoelzl@39092 ` 1465` hoelzl@39092 ` 1466` ```section "LIMSEQ is borel measurable" ``` hoelzl@39092 ` 1467` hoelzl@39092 ` 1468` ```lemma (in sigma_algebra) borel_measurable_LIMSEQ: ``` hoelzl@39092 ` 1469` ``` fixes u :: "nat \ 'a \ real" ``` hoelzl@39092 ` 1470` ``` assumes u': "\x. x \ space M \ (\i. u i x) ----> u' x" ``` hoelzl@39092 ` 1471` ``` and u: "\i. u i \ borel_measurable M" ``` hoelzl@39092 ` 1472` ``` shows "u' \ borel_measurable M" ``` hoelzl@39092 ` 1473` ```proof - ``` hoelzl@43920 ` 1474` ``` have "\x. x \ space M \ liminf (\n. ereal (u n x)) = ereal (u' x)" ``` wenzelm@46731 ` 1475` ``` using u' by (simp add: lim_imp_Liminf) ``` hoelzl@43920 ` 1476` ``` moreover from u have "(\x. liminf (\n. ereal (u n x))) \ borel_measurable M" ``` hoelzl@39092 ` 1477` ``` by auto ``` hoelzl@43920 ` 1478` ``` ultimately show ?thesis by (simp cong: measurable_cong add: borel_measurable_ereal_iff) ``` hoelzl@39092 ` 1479` ```qed ``` hoelzl@39092 ` 1480` paulson@33533 ` 1481` ```end ```