src/HOL/Probability/Borel.thy
 author paulson Mon Nov 09 15:50:15 2009 +0000 (2009-11-09) changeset 33533 40b44cb20c8c child 33535 b233f48a4d3d permissions -rw-r--r--
New theory Probability/Borel.thy, and some associated lemmas
 paulson@33533 ` 1` ```header {*Borel Sets*} ``` paulson@33533 ` 2` paulson@33533 ` 3` ```theory Borel ``` paulson@33533 ` 4` ``` imports Measure ``` paulson@33533 ` 5` ```begin ``` paulson@33533 ` 6` paulson@33533 ` 7` ```text{*From the Hurd/Coble measure theory development, translated by Lawrence Paulson.*} ``` paulson@33533 ` 8` paulson@33533 ` 9` ```definition borel_space where ``` paulson@33533 ` 10` ``` "borel_space = sigma (UNIV::real set) (range (\a::real. {x. x \ a}))" ``` paulson@33533 ` 11` paulson@33533 ` 12` ```definition borel_measurable where ``` paulson@33533 ` 13` ``` "borel_measurable a = measurable a borel_space" ``` paulson@33533 ` 14` paulson@33533 ` 15` ```definition indicator_fn where ``` paulson@33533 ` 16` ``` "indicator_fn s = (\x. if x \ s then 1 else (0::real))" ``` paulson@33533 ` 17` paulson@33533 ` 18` ```definition mono_convergent where ``` paulson@33533 ` 19` ``` "mono_convergent u f s \ ``` paulson@33533 ` 20` ``` (\x m n. m \ n \ x \ s \ u m x \ u n x) \ ``` paulson@33533 ` 21` ``` (\x \ s. (\i. u i x) ----> f x)" ``` paulson@33533 ` 22` paulson@33533 ` 23` ```lemma in_borel_measurable: ``` paulson@33533 ` 24` ``` "f \ borel_measurable M \ ``` paulson@33533 ` 25` ``` sigma_algebra M \ ``` paulson@33533 ` 26` ``` (\s \ sets (sigma UNIV (range (\a::real. {x. x \ a}))). ``` paulson@33533 ` 27` ``` f -` s \ space M \ sets M)" ``` paulson@33533 ` 28` ```apply (auto simp add: borel_measurable_def measurable_def borel_space_def) ``` paulson@33533 ` 29` ```apply (metis PowD UNIV_I Un_commute sigma_algebra_sigma subset_Pow_Union subset_UNIV subset_Un_eq) ``` paulson@33533 ` 30` ```done ``` paulson@33533 ` 31` paulson@33533 ` 32` ```lemma (in sigma_algebra) borel_measurable_const: ``` paulson@33533 ` 33` ``` "(\x. c) \ borel_measurable M" ``` paulson@33533 ` 34` ``` by (auto simp add: in_borel_measurable prems) ``` paulson@33533 ` 35` paulson@33533 ` 36` ```lemma (in sigma_algebra) borel_measurable_indicator: ``` paulson@33533 ` 37` ``` assumes a: "a \ sets M" ``` paulson@33533 ` 38` ``` shows "indicator_fn a \ borel_measurable M" ``` paulson@33533 ` 39` ```apply (auto simp add: in_borel_measurable indicator_fn_def prems) ``` paulson@33533 ` 40` ```apply (metis Diff_eq Int_commute a compl_sets) ``` paulson@33533 ` 41` ```done ``` paulson@33533 ` 42` paulson@33533 ` 43` ```lemma Collect_eq: "{w \ X. f w \ a} = {w. f w \ a} \ X" ``` paulson@33533 ` 44` ``` by (metis Collect_conj_eq Collect_mem_eq Int_commute) ``` paulson@33533 ` 45` paulson@33533 ` 46` ```lemma (in measure_space) borel_measurable_le_iff: ``` paulson@33533 ` 47` ``` "f \ borel_measurable M = (\a. {w \ space M. f w \ a} \ sets M)" ``` paulson@33533 ` 48` ```proof ``` paulson@33533 ` 49` ``` assume f: "f \ borel_measurable M" ``` paulson@33533 ` 50` ``` { fix a ``` paulson@33533 ` 51` ``` have "{w \ space M. f w \ a} \ sets M" using f ``` paulson@33533 ` 52` ``` apply (auto simp add: in_borel_measurable sigma_def Collect_eq) ``` paulson@33533 ` 53` ``` apply (drule_tac x="{x. x \ a}" in bspec, auto) ``` paulson@33533 ` 54` ``` apply (metis equalityE rangeI subsetD sigma_sets.Basic) ``` paulson@33533 ` 55` ``` done ``` paulson@33533 ` 56` ``` } ``` paulson@33533 ` 57` ``` thus "\a. {w \ space M. f w \ a} \ sets M" by blast ``` paulson@33533 ` 58` ```next ``` paulson@33533 ` 59` ``` assume "\a. {w \ space M. f w \ a} \ sets M" ``` paulson@33533 ` 60` ``` thus "f \ borel_measurable M" ``` paulson@33533 ` 61` ``` apply (simp add: borel_measurable_def borel_space_def Collect_eq) ``` paulson@33533 ` 62` ``` apply (rule measurable_sigma, auto) ``` paulson@33533 ` 63` ``` done ``` paulson@33533 ` 64` ```qed ``` paulson@33533 ` 65` paulson@33533 ` 66` ```lemma Collect_less_le: ``` paulson@33533 ` 67` ``` "{w \ X. f w < g w} = (\n. {w \ X. f w \ g w - inverse(real(Suc n))})" ``` paulson@33533 ` 68` ``` proof auto ``` paulson@33533 ` 69` ``` fix w ``` paulson@33533 ` 70` ``` assume w: "f w < g w" ``` paulson@33533 ` 71` ``` hence nz: "g w - f w \ 0" ``` paulson@33533 ` 72` ``` by arith ``` paulson@33533 ` 73` ``` with w have "real(Suc(natceiling(inverse(g w - f w)))) > inverse(g w - f w)" ``` paulson@33533 ` 74` ``` by (metis lessI order_le_less_trans real_natceiling_ge real_of_nat_less_iff) hence "inverse(real(Suc(natceiling(inverse(g w - f w))))) ``` paulson@33533 ` 75` ``` < inverse(inverse(g w - f w))" ``` paulson@33533 ` 76` ``` by (metis less_iff_diff_less_0 less_imp_inverse_less linorder_neqE_ordered_idom nz positive_imp_inverse_positive real_le_anti_sym real_less_def w) ``` paulson@33533 ` 77` ``` hence "inverse(real(Suc(natceiling(inverse(g w - f w))))) < g w - f w" ``` paulson@33533 ` 78` ``` by (metis inverse_inverse_eq order_less_le_trans real_le_refl) ``` paulson@33533 ` 79` ``` thus "\n. f w \ g w - inverse(real(Suc n))" using w ``` paulson@33533 ` 80` ``` by (rule_tac x="natceiling(inverse(g w - f w))" in exI, auto) ``` paulson@33533 ` 81` ``` next ``` paulson@33533 ` 82` ``` fix w n ``` paulson@33533 ` 83` ``` assume le: "f w \ g w - inverse(real(Suc n))" ``` paulson@33533 ` 84` ``` hence "0 < inverse(real(Suc n))" ``` paulson@33533 ` 85` ``` by (metis inverse_real_of_nat_gt_zero) ``` paulson@33533 ` 86` ``` thus "f w < g w" using le ``` paulson@33533 ` 87` ``` by arith ``` paulson@33533 ` 88` ``` qed ``` paulson@33533 ` 89` paulson@33533 ` 90` paulson@33533 ` 91` ```lemma (in sigma_algebra) sigma_le_less: ``` paulson@33533 ` 92` ``` assumes M: "!!a::real. {w \ space M. f w \ a} \ sets M" ``` paulson@33533 ` 93` ``` shows "{w \ space M. f w < a} \ sets M" ``` paulson@33533 ` 94` ```proof - ``` paulson@33533 ` 95` ``` show ?thesis using Collect_less_le [of "space M" f "\x. a"] ``` paulson@33533 ` 96` ``` by (auto simp add: countable_UN M) ``` paulson@33533 ` 97` ```qed ``` paulson@33533 ` 98` paulson@33533 ` 99` ```lemma (in sigma_algebra) sigma_less_ge: ``` paulson@33533 ` 100` ``` assumes M: "!!a::real. {w \ space M. f w < a} \ sets M" ``` paulson@33533 ` 101` ``` shows "{w \ space M. a \ f w} \ sets M" ``` paulson@33533 ` 102` ```proof - ``` paulson@33533 ` 103` ``` have "{w \ space M. a \ f w} = space M - {w \ space M. f w < a}" ``` paulson@33533 ` 104` ``` by auto ``` paulson@33533 ` 105` ``` thus ?thesis using M ``` paulson@33533 ` 106` ``` by auto ``` paulson@33533 ` 107` ```qed ``` paulson@33533 ` 108` paulson@33533 ` 109` ```lemma (in sigma_algebra) sigma_ge_gr: ``` paulson@33533 ` 110` ``` assumes M: "!!a::real. {w \ space M. a \ f w} \ sets M" ``` paulson@33533 ` 111` ``` shows "{w \ space M. a < f w} \ sets M" ``` paulson@33533 ` 112` ```proof - ``` paulson@33533 ` 113` ``` show ?thesis using Collect_less_le [of "space M" "\x. a" f] ``` paulson@33533 ` 114` ``` by (auto simp add: countable_UN le_diff_eq M) ``` paulson@33533 ` 115` ```qed ``` paulson@33533 ` 116` paulson@33533 ` 117` ```lemma (in sigma_algebra) sigma_gr_le: ``` paulson@33533 ` 118` ``` assumes M: "!!a::real. {w \ space M. a < f w} \ sets M" ``` paulson@33533 ` 119` ``` shows "{w \ space M. f w \ a} \ sets M" ``` paulson@33533 ` 120` ```proof - ``` paulson@33533 ` 121` ``` have "{w \ space M. f w \ a} = space M - {w \ space M. a < f w}" ``` paulson@33533 ` 122` ``` by auto ``` paulson@33533 ` 123` ``` thus ?thesis ``` paulson@33533 ` 124` ``` by (simp add: M compl_sets) ``` paulson@33533 ` 125` ```qed ``` paulson@33533 ` 126` paulson@33533 ` 127` ```lemma (in measure_space) borel_measurable_gr_iff: ``` paulson@33533 ` 128` ``` "f \ borel_measurable M = (\a. {w \ space M. a < f w} \ sets M)" ``` paulson@33533 ` 129` ```proof (auto simp add: borel_measurable_le_iff sigma_gr_le) ``` paulson@33533 ` 130` ``` fix u ``` paulson@33533 ` 131` ``` assume M: "\a. {w \ space M. f w \ a} \ sets M" ``` paulson@33533 ` 132` ``` have "{w \ space M. u < f w} = space M - {w \ space M. f w \ u}" ``` paulson@33533 ` 133` ``` by auto ``` paulson@33533 ` 134` ``` thus "{w \ space M. u < f w} \ sets M" ``` paulson@33533 ` 135` ``` by (force simp add: compl_sets countable_UN M) ``` paulson@33533 ` 136` ```qed ``` paulson@33533 ` 137` paulson@33533 ` 138` ```lemma (in measure_space) borel_measurable_less_iff: ``` paulson@33533 ` 139` ``` "f \ borel_measurable M = (\a. {w \ space M. f w < a} \ sets M)" ``` paulson@33533 ` 140` ```proof (auto simp add: borel_measurable_le_iff sigma_le_less) ``` paulson@33533 ` 141` ``` fix u ``` paulson@33533 ` 142` ``` assume M: "\a. {w \ space M. f w < a} \ sets M" ``` paulson@33533 ` 143` ``` have "{w \ space M. f w \ u} = space M - {w \ space M. u < f w}" ``` paulson@33533 ` 144` ``` by auto ``` paulson@33533 ` 145` ``` thus "{w \ space M. f w \ u} \ sets M" ``` paulson@33533 ` 146` ``` using Collect_less_le [of "space M" "\x. u" f] ``` paulson@33533 ` 147` ``` by (force simp add: compl_sets countable_UN le_diff_eq sigma_less_ge M) ``` paulson@33533 ` 148` ```qed ``` paulson@33533 ` 149` paulson@33533 ` 150` ```lemma (in measure_space) borel_measurable_ge_iff: ``` paulson@33533 ` 151` ``` "f \ borel_measurable M = (\a. {w \ space M. a \ f w} \ sets M)" ``` paulson@33533 ` 152` ```proof (auto simp add: borel_measurable_less_iff sigma_le_less sigma_ge_gr sigma_gr_le) ``` paulson@33533 ` 153` ``` fix u ``` paulson@33533 ` 154` ``` assume M: "\a. {w \ space M. f w < a} \ sets M" ``` paulson@33533 ` 155` ``` have "{w \ space M. u \ f w} = space M - {w \ space M. f w < u}" ``` paulson@33533 ` 156` ``` by auto ``` paulson@33533 ` 157` ``` thus "{w \ space M. u \ f w} \ sets M" ``` paulson@33533 ` 158` ``` by (force simp add: compl_sets countable_UN M) ``` paulson@33533 ` 159` ```qed ``` paulson@33533 ` 160` paulson@33533 ` 161` ```lemma (in measure_space) affine_borel_measurable: ``` paulson@33533 ` 162` ``` assumes g: "g \ borel_measurable M" ``` paulson@33533 ` 163` ``` shows "(\x. a + (g x) * b) \ borel_measurable M" ``` paulson@33533 ` 164` ```proof (cases rule: linorder_cases [of b 0]) ``` paulson@33533 ` 165` ``` case equal thus ?thesis ``` paulson@33533 ` 166` ``` by (simp add: borel_measurable_const) ``` paulson@33533 ` 167` ```next ``` paulson@33533 ` 168` ``` case less ``` paulson@33533 ` 169` ``` { ``` paulson@33533 ` 170` ``` fix w c ``` paulson@33533 ` 171` ``` have "a + g w * b \ c \ g w * b \ c - a" ``` paulson@33533 ` 172` ``` by auto ``` paulson@33533 ` 173` ``` also have "... \ (c-a)/b \ g w" using less ``` paulson@33533 ` 174` ``` by (metis divide_le_eq less less_asym) ``` paulson@33533 ` 175` ``` finally have "a + g w * b \ c \ (c-a)/b \ g w" . ``` paulson@33533 ` 176` ``` } ``` paulson@33533 ` 177` ``` hence "\w c. a + g w * b \ c \ (c-a)/b \ g w" . ``` paulson@33533 ` 178` ``` thus ?thesis using less g ``` paulson@33533 ` 179` ``` by (simp add: borel_measurable_ge_iff [of g]) ``` paulson@33533 ` 180` ``` (simp add: borel_measurable_le_iff) ``` paulson@33533 ` 181` ```next ``` paulson@33533 ` 182` ``` case greater ``` paulson@33533 ` 183` ``` hence 0: "\x c. (g x * b \ c - a) \ (g x \ (c - a) / b)" ``` paulson@33533 ` 184` ``` by (metis mult_imp_le_div_pos le_divide_eq) ``` paulson@33533 ` 185` ``` have 1: "\x c. (a + g x * b \ c) \ (g x * b \ c - a)" ``` paulson@33533 ` 186` ``` by auto ``` paulson@33533 ` 187` ``` from greater g ``` paulson@33533 ` 188` ``` show ?thesis ``` paulson@33533 ` 189` ``` by (simp add: borel_measurable_le_iff 0 1) ``` paulson@33533 ` 190` ```qed ``` paulson@33533 ` 191` paulson@33533 ` 192` ```definition ``` paulson@33533 ` 193` ``` nat_to_rat_surj :: "nat \ rat" where ``` paulson@33533 ` 194` ``` "nat_to_rat_surj n = (let (i,j) = nat_to_nat2 n ``` paulson@33533 ` 195` ``` in Fract (nat_to_int_bij i) (nat_to_int_bij j))" ``` paulson@33533 ` 196` paulson@33533 ` 197` ```lemma nat_to_rat_surj: "surj nat_to_rat_surj" ``` paulson@33533 ` 198` ```proof (auto simp add: surj_def nat_to_rat_surj_def) ``` paulson@33533 ` 199` ``` fix y ``` paulson@33533 ` 200` ``` show "\x. y = (\(i, j). Fract (nat_to_int_bij i) (nat_to_int_bij j)) (nat_to_nat2 x)" ``` paulson@33533 ` 201` ``` proof (cases y) ``` paulson@33533 ` 202` ``` case (Fract a b) ``` paulson@33533 ` 203` ``` obtain i where i: "nat_to_int_bij i = a" using surj_nat_to_int_bij ``` paulson@33533 ` 204` ``` by (metis surj_def) ``` paulson@33533 ` 205` ``` obtain j where j: "nat_to_int_bij j = b" using surj_nat_to_int_bij ``` paulson@33533 ` 206` ``` by (metis surj_def) ``` paulson@33533 ` 207` ``` obtain n where n: "nat_to_nat2 n = (i,j)" using nat_to_nat2_surj ``` paulson@33533 ` 208` ``` by (metis surj_def) ``` paulson@33533 ` 209` paulson@33533 ` 210` ``` from Fract i j n show ?thesis ``` paulson@33533 ` 211` ``` by (metis prod.cases prod_case_split) ``` paulson@33533 ` 212` ``` qed ``` paulson@33533 ` 213` ```qed ``` paulson@33533 ` 214` paulson@33533 ` 215` ```lemma rats_enumeration: "\ = range (of_rat o nat_to_rat_surj)" ``` paulson@33533 ` 216` ``` using nat_to_rat_surj ``` paulson@33533 ` 217` ``` by (auto simp add: image_def surj_def) (metis Rats_cases) ``` paulson@33533 ` 218` paulson@33533 ` 219` ```lemma (in measure_space) borel_measurable_less_borel_measurable: ``` paulson@33533 ` 220` ``` assumes f: "f \ borel_measurable M" ``` paulson@33533 ` 221` ``` assumes g: "g \ borel_measurable M" ``` paulson@33533 ` 222` ``` shows "{w \ space M. f w < g w} \ sets M" ``` paulson@33533 ` 223` ```proof - ``` paulson@33533 ` 224` ``` have "{w \ space M. f w < g w} = ``` paulson@33533 ` 225` ``` (\r\\. {w \ space M. f w < r} \ {w \ space M. r < g w })" ``` paulson@33533 ` 226` ``` by (auto simp add: Rats_dense_in_real) ``` paulson@33533 ` 227` ``` thus ?thesis using f g ``` paulson@33533 ` 228` ``` by (simp add: borel_measurable_less_iff [of f] ``` paulson@33533 ` 229` ``` borel_measurable_gr_iff [of g]) ``` paulson@33533 ` 230` ``` (blast intro: gen_countable_UN [OF rats_enumeration]) ``` paulson@33533 ` 231` ```qed ``` paulson@33533 ` 232` ``` ``` paulson@33533 ` 233` ```lemma (in measure_space) borel_measurable_leq_borel_measurable: ``` paulson@33533 ` 234` ``` assumes f: "f \ borel_measurable M" ``` paulson@33533 ` 235` ``` assumes g: "g \ borel_measurable M" ``` paulson@33533 ` 236` ``` shows "{w \ space M. f w \ g w} \ sets M" ``` paulson@33533 ` 237` ```proof - ``` paulson@33533 ` 238` ``` have "{w \ space M. f w \ g w} = space M - {w \ space M. g w < f w}" ``` paulson@33533 ` 239` ``` by auto ``` paulson@33533 ` 240` ``` thus ?thesis using f g ``` paulson@33533 ` 241` ``` by (simp add: borel_measurable_less_borel_measurable compl_sets) ``` paulson@33533 ` 242` ```qed ``` paulson@33533 ` 243` paulson@33533 ` 244` ```lemma (in measure_space) borel_measurable_eq_borel_measurable: ``` paulson@33533 ` 245` ``` assumes f: "f \ borel_measurable M" ``` paulson@33533 ` 246` ``` assumes g: "g \ borel_measurable M" ``` paulson@33533 ` 247` ``` shows "{w \ space M. f w = g w} \ sets M" ``` paulson@33533 ` 248` ```proof - ``` paulson@33533 ` 249` ``` have "{w \ space M. f w = g w} = ``` paulson@33533 ` 250` ``` {w \ space M. f w \ g w} \ {w \ space M. g w \ f w}" ``` paulson@33533 ` 251` ``` by auto ``` paulson@33533 ` 252` ``` thus ?thesis using f g ``` paulson@33533 ` 253` ``` by (simp add: borel_measurable_leq_borel_measurable Int) ``` paulson@33533 ` 254` ```qed ``` paulson@33533 ` 255` paulson@33533 ` 256` ```lemma (in measure_space) borel_measurable_neq_borel_measurable: ``` paulson@33533 ` 257` ``` assumes f: "f \ borel_measurable M" ``` paulson@33533 ` 258` ``` assumes g: "g \ borel_measurable M" ``` paulson@33533 ` 259` ``` shows "{w \ space M. f w \ g w} \ sets M" ``` paulson@33533 ` 260` ```proof - ``` paulson@33533 ` 261` ``` have "{w \ space M. f w \ g w} = space M - {w \ space M. f w = g w}" ``` paulson@33533 ` 262` ``` by auto ``` paulson@33533 ` 263` ``` thus ?thesis using f g ``` paulson@33533 ` 264` ``` by (simp add: borel_measurable_eq_borel_measurable compl_sets) ``` paulson@33533 ` 265` ```qed ``` paulson@33533 ` 266` paulson@33533 ` 267` ```lemma (in measure_space) borel_measurable_plus_borel_measurable: ``` paulson@33533 ` 268` ``` assumes f: "f \ borel_measurable M" ``` paulson@33533 ` 269` ``` assumes g: "g \ borel_measurable M" ``` paulson@33533 ` 270` ``` shows "(\x. f x + g x) \ borel_measurable M" ``` paulson@33533 ` 271` ```proof - ``` paulson@33533 ` 272` ``` have 1:"!!a. {w \ space M. a \ f w + g w} = {w \ space M. a + (g w) * -1 \ f w}" ``` paulson@33533 ` 273` ``` by auto ``` paulson@33533 ` 274` ``` have "!!a. (\w. a + (g w) * -1) \ borel_measurable M" ``` paulson@33533 ` 275` ``` by (rule affine_borel_measurable [OF g]) ``` paulson@33533 ` 276` ``` hence "!!a. {w \ space M. (\w. a + (g w) * -1)(w) \ f w} \ sets M" using f ``` paulson@33533 ` 277` ``` by (rule borel_measurable_leq_borel_measurable) ``` paulson@33533 ` 278` ``` hence "!!a. {w \ space M. a \ f w + g w} \ sets M" ``` paulson@33533 ` 279` ``` by (simp add: 1) ``` paulson@33533 ` 280` ``` thus ?thesis ``` paulson@33533 ` 281` ``` by (simp add: borel_measurable_ge_iff) ``` paulson@33533 ` 282` ```qed ``` paulson@33533 ` 283` paulson@33533 ` 284` paulson@33533 ` 285` ```lemma (in measure_space) borel_measurable_square: ``` paulson@33533 ` 286` ``` assumes f: "f \ borel_measurable M" ``` paulson@33533 ` 287` ``` shows "(\x. (f x)^2) \ borel_measurable M" ``` paulson@33533 ` 288` ```proof - ``` paulson@33533 ` 289` ``` { ``` paulson@33533 ` 290` ``` fix a ``` paulson@33533 ` 291` ``` have "{w \ space M. (f w)\ \ a} \ sets M" ``` paulson@33533 ` 292` ``` proof (cases rule: linorder_cases [of a 0]) ``` paulson@33533 ` 293` ``` case less ``` paulson@33533 ` 294` ``` hence "{w \ space M. (f w)\ \ a} = {}" ``` paulson@33533 ` 295` ``` by auto (metis less order_le_less_trans power2_less_0) ``` paulson@33533 ` 296` ``` also have "... \ sets M" ``` paulson@33533 ` 297` ``` by (rule empty_sets) ``` paulson@33533 ` 298` ``` finally show ?thesis . ``` paulson@33533 ` 299` ``` next ``` paulson@33533 ` 300` ``` case equal ``` paulson@33533 ` 301` ``` hence "{w \ space M. (f w)\ \ a} = ``` paulson@33533 ` 302` ``` {w \ space M. f w \ 0} \ {w \ space M. 0 \ f w}" ``` paulson@33533 ` 303` ``` by auto ``` paulson@33533 ` 304` ``` also have "... \ sets M" ``` paulson@33533 ` 305` ``` apply (insert f) ``` paulson@33533 ` 306` ``` apply (rule Int) ``` paulson@33533 ` 307` ``` apply (simp add: borel_measurable_le_iff) ``` paulson@33533 ` 308` ``` apply (simp add: borel_measurable_ge_iff) ``` paulson@33533 ` 309` ``` done ``` paulson@33533 ` 310` ``` finally show ?thesis . ``` paulson@33533 ` 311` ``` next ``` paulson@33533 ` 312` ``` case greater ``` paulson@33533 ` 313` ``` have "\x. (f x ^ 2 \ sqrt a ^ 2) = (- sqrt a \ f x & f x \ sqrt a)" ``` paulson@33533 ` 314` ``` by (metis abs_le_interval_iff abs_of_pos greater real_sqrt_abs ``` paulson@33533 ` 315` ``` real_sqrt_le_iff real_sqrt_power) ``` paulson@33533 ` 316` ``` hence "{w \ space M. (f w)\ \ a} = ``` paulson@33533 ` 317` ``` {w \ space M. -(sqrt a) \ f w} \ {w \ space M. f w \ sqrt a}" ``` paulson@33533 ` 318` ``` using greater by auto ``` paulson@33533 ` 319` ``` also have "... \ sets M" ``` paulson@33533 ` 320` ``` apply (insert f) ``` paulson@33533 ` 321` ``` apply (rule Int) ``` paulson@33533 ` 322` ``` apply (simp add: borel_measurable_ge_iff) ``` paulson@33533 ` 323` ``` apply (simp add: borel_measurable_le_iff) ``` paulson@33533 ` 324` ``` done ``` paulson@33533 ` 325` ``` finally show ?thesis . ``` paulson@33533 ` 326` ``` qed ``` paulson@33533 ` 327` ``` } ``` paulson@33533 ` 328` ``` thus ?thesis by (auto simp add: borel_measurable_le_iff) ``` paulson@33533 ` 329` ```qed ``` paulson@33533 ` 330` paulson@33533 ` 331` ```lemma times_eq_sum_squares: ``` paulson@33533 ` 332` ``` fixes x::real ``` paulson@33533 ` 333` ``` shows"x*y = ((x+y)^2)/4 - ((x-y)^ 2)/4" ``` paulson@33533 ` 334` ```by (simp add: power2_eq_square ring_distribs diff_divide_distrib [symmetric]) ``` paulson@33533 ` 335` paulson@33533 ` 336` paulson@33533 ` 337` ```lemma (in measure_space) borel_measurable_uminus_borel_measurable: ``` paulson@33533 ` 338` ``` assumes g: "g \ borel_measurable M" ``` paulson@33533 ` 339` ``` shows "(\x. - g x) \ borel_measurable M" ``` paulson@33533 ` 340` ```proof - ``` paulson@33533 ` 341` ``` have "(\x. - g x) = (\x. 0 + (g x) * -1)" ``` paulson@33533 ` 342` ``` by simp ``` paulson@33533 ` 343` ``` also have "... \ borel_measurable M" ``` paulson@33533 ` 344` ``` by (fast intro: affine_borel_measurable g) ``` paulson@33533 ` 345` ``` finally show ?thesis . ``` paulson@33533 ` 346` ```qed ``` paulson@33533 ` 347` paulson@33533 ` 348` ```lemma (in measure_space) borel_measurable_times_borel_measurable: ``` paulson@33533 ` 349` ``` assumes f: "f \ borel_measurable M" ``` paulson@33533 ` 350` ``` assumes g: "g \ borel_measurable M" ``` paulson@33533 ` 351` ``` shows "(\x. f x * g x) \ borel_measurable M" ``` paulson@33533 ` 352` ```proof - ``` paulson@33533 ` 353` ``` have 1: "(\x. 0 + (f x + g x)\ * inverse 4) \ borel_measurable M" ``` paulson@33533 ` 354` ``` by (fast intro: affine_borel_measurable borel_measurable_square ``` paulson@33533 ` 355` ``` borel_measurable_plus_borel_measurable f g) ``` paulson@33533 ` 356` ``` have "(\x. -((f x + -g x) ^ 2 * inverse 4)) = ``` paulson@33533 ` 357` ``` (\x. 0 + ((f x + -g x) ^ 2 * inverse -4))" ``` paulson@33533 ` 358` ``` by (simp add: Ring_and_Field.minus_divide_right) ``` paulson@33533 ` 359` ``` also have "... \ borel_measurable M" ``` paulson@33533 ` 360` ``` by (fast intro: affine_borel_measurable borel_measurable_square ``` paulson@33533 ` 361` ``` borel_measurable_plus_borel_measurable ``` paulson@33533 ` 362` ``` borel_measurable_uminus_borel_measurable f g) ``` paulson@33533 ` 363` ``` finally have 2: "(\x. -((f x + -g x) ^ 2 * inverse 4)) \ borel_measurable M" . ``` paulson@33533 ` 364` ``` show ?thesis ``` paulson@33533 ` 365` ``` apply (simp add: times_eq_sum_squares real_diff_def) ``` paulson@33533 ` 366` ``` using 1 2 apply (simp add: borel_measurable_plus_borel_measurable) ``` paulson@33533 ` 367` ``` done ``` paulson@33533 ` 368` ```qed ``` paulson@33533 ` 369` paulson@33533 ` 370` ```lemma (in measure_space) borel_measurable_diff_borel_measurable: ``` paulson@33533 ` 371` ``` assumes f: "f \ borel_measurable M" ``` paulson@33533 ` 372` ``` assumes g: "g \ borel_measurable M" ``` paulson@33533 ` 373` ``` shows "(\x. f x - g x) \ borel_measurable M" ``` paulson@33533 ` 374` ```unfolding real_diff_def ``` paulson@33533 ` 375` ``` by (fast intro: borel_measurable_plus_borel_measurable ``` paulson@33533 ` 376` ``` borel_measurable_uminus_borel_measurable f g) ``` paulson@33533 ` 377` paulson@33533 ` 378` ```lemma (in measure_space) mono_convergent_borel_measurable: ``` paulson@33533 ` 379` ``` assumes u: "!!n. u n \ borel_measurable M" ``` paulson@33533 ` 380` ``` assumes mc: "mono_convergent u f (space M)" ``` paulson@33533 ` 381` ``` shows "f \ borel_measurable M" ``` paulson@33533 ` 382` ```proof - ``` paulson@33533 ` 383` ``` { ``` paulson@33533 ` 384` ``` fix a ``` paulson@33533 ` 385` ``` have 1: "!!w. w \ space M & f w <= a \ w \ space M & (\i. u i w <= a)" ``` paulson@33533 ` 386` ``` proof safe ``` paulson@33533 ` 387` ``` fix w i ``` paulson@33533 ` 388` ``` assume w: "w \ space M" and f: "f w \ a" ``` paulson@33533 ` 389` ``` hence "u i w \ f w" ``` paulson@33533 ` 390` ``` by (auto intro: SEQ.incseq_le ``` paulson@33533 ` 391` ``` simp add: incseq_def mc [unfolded mono_convergent_def]) ``` paulson@33533 ` 392` ``` thus "u i w \ a" using f ``` paulson@33533 ` 393` ``` by auto ``` paulson@33533 ` 394` ``` next ``` paulson@33533 ` 395` ``` fix w ``` paulson@33533 ` 396` ``` assume w: "w \ space M" and u: "\i. u i w \ a" ``` paulson@33533 ` 397` ``` thus "f w \ a" ``` paulson@33533 ` 398` ``` by (metis LIMSEQ_le_const2 mc [unfolded mono_convergent_def]) ``` paulson@33533 ` 399` ``` qed ``` paulson@33533 ` 400` ``` have "{w \ space M. f w \ a} = {w \ space M. (\i. u i w <= a)}" ``` paulson@33533 ` 401` ``` by (simp add: 1) ``` paulson@33533 ` 402` ``` also have "... = (\i. {w \ space M. u i w \ a})" ``` paulson@33533 ` 403` ``` by auto ``` paulson@33533 ` 404` ``` also have "... \ sets M" using u ``` paulson@33533 ` 405` ``` by (auto simp add: borel_measurable_le_iff intro: countable_INT) ``` paulson@33533 ` 406` ``` finally have "{w \ space M. f w \ a} \ sets M" . ``` paulson@33533 ` 407` ``` } ``` paulson@33533 ` 408` ``` thus ?thesis ``` paulson@33533 ` 409` ``` by (auto simp add: borel_measurable_le_iff) ``` paulson@33533 ` 410` ```qed ``` paulson@33533 ` 411` paulson@33533 ` 412` ```lemma (in measure_space) borel_measurable_SIGMA_borel_measurable: ``` paulson@33533 ` 413` ``` assumes s: "finite s" ``` paulson@33533 ` 414` ``` shows "(!!i. i \ s ==> f i \ borel_measurable M) \ (\x. setsum (\i. f i x) s) \ borel_measurable M" using s ``` paulson@33533 ` 415` ```proof (induct s) ``` paulson@33533 ` 416` ``` case empty ``` paulson@33533 ` 417` ``` thus ?case ``` paulson@33533 ` 418` ``` by (simp add: borel_measurable_const) ``` paulson@33533 ` 419` ```next ``` paulson@33533 ` 420` ``` case (insert x s) ``` paulson@33533 ` 421` ``` thus ?case ``` paulson@33533 ` 422` ``` by (auto simp add: borel_measurable_plus_borel_measurable) ``` paulson@33533 ` 423` ```qed ``` paulson@33533 ` 424` paulson@33533 ` 425` ```end ```