src/HOL/Probability/Complete_Measure.thy
 author hoelzl Wed Dec 01 19:20:30 2010 +0100 (2010-12-01) changeset 40859 de0b30e6c2d2 child 40871 688f6ff859e1 permissions -rw-r--r--
Support product spaces on sigma finite measures.
Introduce the almost everywhere quantifier.
Introduce 'morphism' theorems for most constants.
Prove uniqueness of measures on cut stable generators.
Prove uniqueness of the Radon-Nikodym derivative.
Removed misleading suffix from borel_space and lebesgue_space.
Use product spaces to introduce Fubini on the Lebesgue integral.
Combine Euclidean_Lebesgue and Lebesgue_Measure.
Generalize theorems about mutual information and entropy to arbitrary probability spaces.
Remove simproc mult_log as it does not work with interpretations.
Introduce completion of measure spaces.
Change type of sigma.
Introduce dynkin systems.
 hoelzl@40859 ` 1` ```(* Title: Complete_Measure.thy ``` hoelzl@40859 ` 2` ``` Author: Robert Himmelmann, Johannes Hoelzl, TU Muenchen ``` hoelzl@40859 ` 3` ```*) ``` hoelzl@40859 ` 4` ```theory Complete_Measure ``` hoelzl@40859 ` 5` ```imports Product_Measure ``` hoelzl@40859 ` 6` ```begin ``` hoelzl@40859 ` 7` hoelzl@40859 ` 8` ```locale completeable_measure_space = measure_space ``` hoelzl@40859 ` 9` hoelzl@40859 ` 10` ```definition (in completeable_measure_space) completion :: "'a algebra" where ``` hoelzl@40859 ` 11` ``` "completion = \ space = space M, ``` hoelzl@40859 ` 12` ``` sets = { S \ N |S N N'. S \ sets M \ N' \ null_sets \ N \ N' } \" ``` hoelzl@40859 ` 13` hoelzl@40859 ` 14` ```lemma (in completeable_measure_space) space_completion[simp]: ``` hoelzl@40859 ` 15` ``` "space completion = space M" unfolding completion_def by simp ``` hoelzl@40859 ` 16` hoelzl@40859 ` 17` ```lemma (in completeable_measure_space) sets_completionE: ``` hoelzl@40859 ` 18` ``` assumes "A \ sets completion" ``` hoelzl@40859 ` 19` ``` obtains S N N' where "A = S \ N" "N \ N'" "N' \ null_sets" "S \ sets M" ``` hoelzl@40859 ` 20` ``` using assms unfolding completion_def by auto ``` hoelzl@40859 ` 21` hoelzl@40859 ` 22` ```lemma (in completeable_measure_space) sets_completionI: ``` hoelzl@40859 ` 23` ``` assumes "A = S \ N" "N \ N'" "N' \ null_sets" "S \ sets M" ``` hoelzl@40859 ` 24` ``` shows "A \ sets completion" ``` hoelzl@40859 ` 25` ``` using assms unfolding completion_def by auto ``` hoelzl@40859 ` 26` hoelzl@40859 ` 27` ```lemma (in completeable_measure_space) sets_completionI_sets[intro]: ``` hoelzl@40859 ` 28` ``` "A \ sets M \ A \ sets completion" ``` hoelzl@40859 ` 29` ``` unfolding completion_def by force ``` hoelzl@40859 ` 30` hoelzl@40859 ` 31` ```lemma (in completeable_measure_space) null_sets_completion: ``` hoelzl@40859 ` 32` ``` assumes "N' \ null_sets" "N \ N'" shows "N \ sets completion" ``` hoelzl@40859 ` 33` ``` apply(rule sets_completionI[of N "{}" N N']) ``` hoelzl@40859 ` 34` ``` using assms by auto ``` hoelzl@40859 ` 35` hoelzl@40859 ` 36` ```sublocale completeable_measure_space \ completion!: sigma_algebra completion ``` hoelzl@40859 ` 37` ```proof (unfold sigma_algebra_iff2, safe) ``` hoelzl@40859 ` 38` ``` fix A x assume "A \ sets completion" "x \ A" ``` hoelzl@40859 ` 39` ``` with sets_into_space show "x \ space completion" ``` hoelzl@40859 ` 40` ``` by (auto elim!: sets_completionE) ``` hoelzl@40859 ` 41` ```next ``` hoelzl@40859 ` 42` ``` fix A assume "A \ sets completion" ``` hoelzl@40859 ` 43` ``` from this[THEN sets_completionE] guess S N N' . note A = this ``` hoelzl@40859 ` 44` ``` let ?C = "space completion" ``` hoelzl@40859 ` 45` ``` show "?C - A \ sets completion" using A ``` hoelzl@40859 ` 46` ``` by (intro sets_completionI[of _ "(?C - S) \ (?C - N')" "(?C - S) \ N' \ (?C - N)"]) ``` hoelzl@40859 ` 47` ``` auto ``` hoelzl@40859 ` 48` ```next ``` hoelzl@40859 ` 49` ``` fix A ::"nat \ 'a set" assume A: "range A \ sets completion" ``` hoelzl@40859 ` 50` ``` then have "\n. \S N N'. A n = S \ N \ S \ sets M \ N' \ null_sets \ N \ N'" ``` hoelzl@40859 ` 51` ``` unfolding completion_def by (auto simp: image_subset_iff) ``` hoelzl@40859 ` 52` ``` from choice[OF this] guess S .. ``` hoelzl@40859 ` 53` ``` from choice[OF this] guess N .. ``` hoelzl@40859 ` 54` ``` from choice[OF this] guess N' .. ``` hoelzl@40859 ` 55` ``` then show "UNION UNIV A \ sets completion" ``` hoelzl@40859 ` 56` ``` using null_sets_UN[of N'] ``` hoelzl@40859 ` 57` ``` by (intro sets_completionI[of _ "UNION UNIV S" "UNION UNIV N" "UNION UNIV N'"]) ``` hoelzl@40859 ` 58` ``` auto ``` hoelzl@40859 ` 59` ```qed auto ``` hoelzl@40859 ` 60` hoelzl@40859 ` 61` ```definition (in completeable_measure_space) ``` hoelzl@40859 ` 62` ``` "split_completion A p = (\N'. A = fst p \ snd p \ fst p \ snd p = {} \ ``` hoelzl@40859 ` 63` ``` fst p \ sets M \ snd p \ N' \ N' \ null_sets)" ``` hoelzl@40859 ` 64` hoelzl@40859 ` 65` ```definition (in completeable_measure_space) ``` hoelzl@40859 ` 66` ``` "main_part A = fst (Eps (split_completion A))" ``` hoelzl@40859 ` 67` hoelzl@40859 ` 68` ```definition (in completeable_measure_space) ``` hoelzl@40859 ` 69` ``` "null_part A = snd (Eps (split_completion A))" ``` hoelzl@40859 ` 70` hoelzl@40859 ` 71` ```lemma (in completeable_measure_space) split_completion: ``` hoelzl@40859 ` 72` ``` assumes "A \ sets completion" ``` hoelzl@40859 ` 73` ``` shows "split_completion A (main_part A, null_part A)" ``` hoelzl@40859 ` 74` ``` unfolding main_part_def null_part_def ``` hoelzl@40859 ` 75` ```proof (rule someI2_ex) ``` hoelzl@40859 ` 76` ``` from assms[THEN sets_completionE] guess S N N' . note A = this ``` hoelzl@40859 ` 77` ``` let ?P = "(S, N - S)" ``` hoelzl@40859 ` 78` ``` show "\p. split_completion A p" ``` hoelzl@40859 ` 79` ``` unfolding split_completion_def using A ``` hoelzl@40859 ` 80` ``` proof (intro exI conjI) ``` hoelzl@40859 ` 81` ``` show "A = fst ?P \ snd ?P" using A by auto ``` hoelzl@40859 ` 82` ``` show "snd ?P \ N'" using A by auto ``` hoelzl@40859 ` 83` ``` qed auto ``` hoelzl@40859 ` 84` ```qed auto ``` hoelzl@40859 ` 85` hoelzl@40859 ` 86` ```lemma (in completeable_measure_space) ``` hoelzl@40859 ` 87` ``` assumes "S \ sets completion" ``` hoelzl@40859 ` 88` ``` shows main_part_sets[intro, simp]: "main_part S \ sets M" ``` hoelzl@40859 ` 89` ``` and main_part_null_part_Un[simp]: "main_part S \ null_part S = S" ``` hoelzl@40859 ` 90` ``` and main_part_null_part_Int[simp]: "main_part S \ null_part S = {}" ``` hoelzl@40859 ` 91` ``` using split_completion[OF assms] by (auto simp: split_completion_def) ``` hoelzl@40859 ` 92` hoelzl@40859 ` 93` ```lemma (in completeable_measure_space) null_part: ``` hoelzl@40859 ` 94` ``` assumes "S \ sets completion" shows "\N. N\null_sets \ null_part S \ N" ``` hoelzl@40859 ` 95` ``` using split_completion[OF assms] by (auto simp: split_completion_def) ``` hoelzl@40859 ` 96` hoelzl@40859 ` 97` ```lemma (in completeable_measure_space) null_part_sets[intro, simp]: ``` hoelzl@40859 ` 98` ``` assumes "S \ sets M" shows "null_part S \ sets M" "\ (null_part S) = 0" ``` hoelzl@40859 ` 99` ```proof - ``` hoelzl@40859 ` 100` ``` have S: "S \ sets completion" using assms by auto ``` hoelzl@40859 ` 101` ``` have "S - main_part S \ sets M" using assms by auto ``` hoelzl@40859 ` 102` ``` moreover ``` hoelzl@40859 ` 103` ``` from main_part_null_part_Un[OF S] main_part_null_part_Int[OF S] ``` hoelzl@40859 ` 104` ``` have "S - main_part S = null_part S" by auto ``` hoelzl@40859 ` 105` ``` ultimately show sets: "null_part S \ sets M" by auto ``` hoelzl@40859 ` 106` ``` from null_part[OF S] guess N .. ``` hoelzl@40859 ` 107` ``` with measure_eq_0[of N "null_part S"] sets ``` hoelzl@40859 ` 108` ``` show "\ (null_part S) = 0" by auto ``` hoelzl@40859 ` 109` ```qed ``` hoelzl@40859 ` 110` hoelzl@40859 ` 111` ```definition (in completeable_measure_space) "\' A = \ (main_part A)" ``` hoelzl@40859 ` 112` hoelzl@40859 ` 113` ```lemma (in completeable_measure_space) \'_set[simp]: ``` hoelzl@40859 ` 114` ``` assumes "S \ sets M" shows "\' S = \ S" ``` hoelzl@40859 ` 115` ```proof - ``` hoelzl@40859 ` 116` ``` have S: "S \ sets completion" using assms by auto ``` hoelzl@40859 ` 117` ``` then have "\ S = \ (main_part S \ null_part S)" by simp ``` hoelzl@40859 ` 118` ``` also have "\ = \ (main_part S)" ``` hoelzl@40859 ` 119` ``` using S assms measure_additive[of "main_part S" "null_part S"] ``` hoelzl@40859 ` 120` ``` by (auto simp: measure_additive) ``` hoelzl@40859 ` 121` ``` finally show ?thesis unfolding \'_def by simp ``` hoelzl@40859 ` 122` ```qed ``` hoelzl@40859 ` 123` hoelzl@40859 ` 124` ```lemma (in completeable_measure_space) sets_completionI_sub: ``` hoelzl@40859 ` 125` ``` assumes N: "N' \ null_sets" "N \ N'" ``` hoelzl@40859 ` 126` ``` shows "N \ sets completion" ``` hoelzl@40859 ` 127` ``` using assms by (intro sets_completionI[of _ "{}" N N']) auto ``` hoelzl@40859 ` 128` hoelzl@40859 ` 129` ```lemma (in completeable_measure_space) \_main_part_UN: ``` hoelzl@40859 ` 130` ``` fixes S :: "nat \ 'a set" ``` hoelzl@40859 ` 131` ``` assumes "range S \ sets completion" ``` hoelzl@40859 ` 132` ``` shows "\' (\i. (S i)) = \ (\i. main_part (S i))" ``` hoelzl@40859 ` 133` ```proof - ``` hoelzl@40859 ` 134` ``` have S: "\i. S i \ sets completion" using assms by auto ``` hoelzl@40859 ` 135` ``` then have UN: "(\i. S i) \ sets completion" by auto ``` hoelzl@40859 ` 136` ``` have "\i. \N. N \ null_sets \ null_part (S i) \ N" ``` hoelzl@40859 ` 137` ``` using null_part[OF S] by auto ``` hoelzl@40859 ` 138` ``` from choice[OF this] guess N .. note N = this ``` hoelzl@40859 ` 139` ``` then have UN_N: "(\i. N i) \ null_sets" by (intro null_sets_UN) auto ``` hoelzl@40859 ` 140` ``` have "(\i. S i) \ sets completion" using S by auto ``` hoelzl@40859 ` 141` ``` from null_part[OF this] guess N' .. note N' = this ``` hoelzl@40859 ` 142` ``` let ?N = "(\i. N i) \ N'" ``` hoelzl@40859 ` 143` ``` have null_set: "?N \ null_sets" using N' UN_N by (intro null_sets_Un) auto ``` hoelzl@40859 ` 144` ``` have "main_part (\i. S i) \ ?N = (main_part (\i. S i) \ null_part (\i. S i)) \ ?N" ``` hoelzl@40859 ` 145` ``` using N' by auto ``` hoelzl@40859 ` 146` ``` also have "\ = (\i. main_part (S i) \ null_part (S i)) \ ?N" ``` hoelzl@40859 ` 147` ``` unfolding main_part_null_part_Un[OF S] main_part_null_part_Un[OF UN] by auto ``` hoelzl@40859 ` 148` ``` also have "\ = (\i. main_part (S i)) \ ?N" ``` hoelzl@40859 ` 149` ``` using N by auto ``` hoelzl@40859 ` 150` ``` finally have *: "main_part (\i. S i) \ ?N = (\i. main_part (S i)) \ ?N" . ``` hoelzl@40859 ` 151` ``` have "\ (main_part (\i. S i)) = \ (main_part (\i. S i) \ ?N)" ``` hoelzl@40859 ` 152` ``` using null_set UN by (intro measure_Un_null_set[symmetric]) auto ``` hoelzl@40859 ` 153` ``` also have "\ = \ ((\i. main_part (S i)) \ ?N)" ``` hoelzl@40859 ` 154` ``` unfolding * .. ``` hoelzl@40859 ` 155` ``` also have "\ = \ (\i. main_part (S i))" ``` hoelzl@40859 ` 156` ``` using null_set S by (intro measure_Un_null_set) auto ``` hoelzl@40859 ` 157` ``` finally show ?thesis unfolding \'_def . ``` hoelzl@40859 ` 158` ```qed ``` hoelzl@40859 ` 159` hoelzl@40859 ` 160` ```lemma (in completeable_measure_space) \_main_part_Un: ``` hoelzl@40859 ` 161` ``` assumes S: "S \ sets completion" and T: "T \ sets completion" ``` hoelzl@40859 ` 162` ``` shows "\' (S \ T) = \ (main_part S \ main_part T)" ``` hoelzl@40859 ` 163` ```proof - ``` hoelzl@40859 ` 164` ``` have UN: "(\i. binary (main_part S) (main_part T) i) = (\i. main_part (binary S T i))" ``` hoelzl@40859 ` 165` ``` unfolding binary_def by (auto split: split_if_asm) ``` hoelzl@40859 ` 166` ``` show ?thesis ``` hoelzl@40859 ` 167` ``` using \_main_part_UN[of "binary S T"] assms ``` hoelzl@40859 ` 168` ``` unfolding range_binary_eq Un_range_binary UN by auto ``` hoelzl@40859 ` 169` ```qed ``` hoelzl@40859 ` 170` hoelzl@40859 ` 171` ```sublocale completeable_measure_space \ completion!: measure_space completion \' ``` hoelzl@40859 ` 172` ```proof ``` hoelzl@40859 ` 173` ``` show "\' {} = 0" by auto ``` hoelzl@40859 ` 174` ```next ``` hoelzl@40859 ` 175` ``` show "countably_additive completion \'" ``` hoelzl@40859 ` 176` ``` proof (unfold countably_additive_def, intro allI conjI impI) ``` hoelzl@40859 ` 177` ``` fix A :: "nat \ 'a set" assume A: "range A \ sets completion" "disjoint_family A" ``` hoelzl@40859 ` 178` ``` have "disjoint_family (\i. main_part (A i))" ``` hoelzl@40859 ` 179` ``` proof (intro disjoint_family_on_bisimulation[OF A(2)]) ``` hoelzl@40859 ` 180` ``` fix n m assume "A n \ A m = {}" ``` hoelzl@40859 ` 181` ``` then have "(main_part (A n) \ null_part (A n)) \ (main_part (A m) \ null_part (A m)) = {}" ``` hoelzl@40859 ` 182` ``` using A by (subst (1 2) main_part_null_part_Un) auto ``` hoelzl@40859 ` 183` ``` then show "main_part (A n) \ main_part (A m) = {}" by auto ``` hoelzl@40859 ` 184` ``` qed ``` hoelzl@40859 ` 185` ``` then have "(\\<^isub>\n. \' (A n)) = \ (\i. main_part (A i))" ``` hoelzl@40859 ` 186` ``` unfolding \'_def using A by (intro measure_countably_additive) auto ``` hoelzl@40859 ` 187` ``` then show "(\\<^isub>\n. \' (A n)) = \' (UNION UNIV A)" ``` hoelzl@40859 ` 188` ``` unfolding \_main_part_UN[OF A(1)] . ``` hoelzl@40859 ` 189` ``` qed ``` hoelzl@40859 ` 190` ```qed ``` hoelzl@40859 ` 191` hoelzl@40859 ` 192` ```lemma (in sigma_algebra) simple_functionD': ``` hoelzl@40859 ` 193` ``` assumes "simple_function f" ``` hoelzl@40859 ` 194` ``` shows "f -` {x} \ space M \ sets M" ``` hoelzl@40859 ` 195` ```proof cases ``` hoelzl@40859 ` 196` ``` assume "x \ f`space M" from simple_functionD(2)[OF assms this] show ?thesis . ``` hoelzl@40859 ` 197` ```next ``` hoelzl@40859 ` 198` ``` assume "x \ f`space M" then have "f -` {x} \ space M = {}" by auto ``` hoelzl@40859 ` 199` ``` then show ?thesis by auto ``` hoelzl@40859 ` 200` ```qed ``` hoelzl@40859 ` 201` hoelzl@40859 ` 202` ```lemma (in sigma_algebra) simple_function_If: ``` hoelzl@40859 ` 203` ``` assumes sf: "simple_function f" "simple_function g" and A: "A \ sets M" ``` hoelzl@40859 ` 204` ``` shows "simple_function (\x. if x \ A then f x else g x)" (is "simple_function ?IF") ``` hoelzl@40859 ` 205` ```proof - ``` hoelzl@40859 ` 206` ``` def F \ "\x. f -` {x} \ space M" and G \ "\x. g -` {x} \ space M" ``` hoelzl@40859 ` 207` ``` show ?thesis unfolding simple_function_def ``` hoelzl@40859 ` 208` ``` proof safe ``` hoelzl@40859 ` 209` ``` have "?IF ` space M \ f ` space M \ g ` space M" by auto ``` hoelzl@40859 ` 210` ``` from finite_subset[OF this] assms ``` hoelzl@40859 ` 211` ``` show "finite (?IF ` space M)" unfolding simple_function_def by auto ``` hoelzl@40859 ` 212` ``` next ``` hoelzl@40859 ` 213` ``` fix x assume "x \ space M" ``` hoelzl@40859 ` 214` ``` then have *: "?IF -` {?IF x} \ space M = (if x \ A ``` hoelzl@40859 ` 215` ``` then ((F (f x) \ A) \ (G (f x) - (G (f x) \ A))) ``` hoelzl@40859 ` 216` ``` else ((F (g x) \ A) \ (G (g x) - (G (g x) \ A))))" ``` hoelzl@40859 ` 217` ``` using sets_into_space[OF A] by (auto split: split_if_asm simp: G_def F_def) ``` hoelzl@40859 ` 218` ``` have [intro]: "\x. F x \ sets M" "\x. G x \ sets M" ``` hoelzl@40859 ` 219` ``` unfolding F_def G_def using sf[THEN simple_functionD'] by auto ``` hoelzl@40859 ` 220` ``` show "?IF -` {?IF x} \ space M \ sets M" unfolding * using A by auto ``` hoelzl@40859 ` 221` ``` qed ``` hoelzl@40859 ` 222` ```qed ``` hoelzl@40859 ` 223` hoelzl@40859 ` 224` ```lemma (in measure_space) null_sets_finite_UN: ``` hoelzl@40859 ` 225` ``` assumes "finite S" "\i. i \ S \ A i \ null_sets" ``` hoelzl@40859 ` 226` ``` shows "(\i\S. A i) \ null_sets" ``` hoelzl@40859 ` 227` ```proof (intro CollectI conjI) ``` hoelzl@40859 ` 228` ``` show "(\i\S. A i) \ sets M" using assms by (intro finite_UN) auto ``` hoelzl@40859 ` 229` ``` have "\ (\i\S. A i) \ (\i\S. \ (A i))" ``` hoelzl@40859 ` 230` ``` using assms by (intro measure_finitely_subadditive) auto ``` hoelzl@40859 ` 231` ``` then show "\ (\i\S. A i) = 0" ``` hoelzl@40859 ` 232` ``` using assms by auto ``` hoelzl@40859 ` 233` ```qed ``` hoelzl@40859 ` 234` hoelzl@40859 ` 235` ```lemma (in completeable_measure_space) completion_ex_simple_function: ``` hoelzl@40859 ` 236` ``` assumes f: "completion.simple_function f" ``` hoelzl@40859 ` 237` ``` shows "\f'. simple_function f' \ (AE x. f x = f' x)" ``` hoelzl@40859 ` 238` ```proof - ``` hoelzl@40859 ` 239` ``` let "?F x" = "f -` {x} \ space M" ``` hoelzl@40859 ` 240` ``` have F: "\x. ?F x \ sets completion" and fin: "finite (f`space M)" ``` hoelzl@40859 ` 241` ``` using completion.simple_functionD'[OF f] ``` hoelzl@40859 ` 242` ``` completion.simple_functionD[OF f] by simp_all ``` hoelzl@40859 ` 243` ``` have "\x. \N. N \ null_sets \ null_part (?F x) \ N" ``` hoelzl@40859 ` 244` ``` using F null_part by auto ``` hoelzl@40859 ` 245` ``` from choice[OF this] obtain N where ``` hoelzl@40859 ` 246` ``` N: "\x. null_part (?F x) \ N x" "\x. N x \ null_sets" by auto ``` hoelzl@40859 ` 247` ``` let ?N = "\x\f`space M. N x" let "?f' x" = "if x \ ?N then undefined else f x" ``` hoelzl@40859 ` 248` ``` have sets: "?N \ null_sets" using N fin by (intro null_sets_finite_UN) auto ``` hoelzl@40859 ` 249` ``` show ?thesis unfolding simple_function_def ``` hoelzl@40859 ` 250` ``` proof (safe intro!: exI[of _ ?f']) ``` hoelzl@40859 ` 251` ``` have "?f' ` space M \ f`space M \ {undefined}" by auto ``` hoelzl@40859 ` 252` ``` from finite_subset[OF this] completion.simple_functionD(1)[OF f] ``` hoelzl@40859 ` 253` ``` show "finite (?f' ` space M)" by auto ``` hoelzl@40859 ` 254` ``` next ``` hoelzl@40859 ` 255` ``` fix x assume "x \ space M" ``` hoelzl@40859 ` 256` ``` have "?f' -` {?f' x} \ space M = ``` hoelzl@40859 ` 257` ``` (if x \ ?N then ?F undefined \ ?N ``` hoelzl@40859 ` 258` ``` else if f x = undefined then ?F (f x) \ ?N ``` hoelzl@40859 ` 259` ``` else ?F (f x) - ?N)" ``` hoelzl@40859 ` 260` ``` using N(2) sets_into_space by (auto split: split_if_asm) ``` hoelzl@40859 ` 261` ``` moreover { fix y have "?F y \ ?N \ sets M" ``` hoelzl@40859 ` 262` ``` proof cases ``` hoelzl@40859 ` 263` ``` assume y: "y \ f`space M" ``` hoelzl@40859 ` 264` ``` have "?F y \ ?N = (main_part (?F y) \ null_part (?F y)) \ ?N" ``` hoelzl@40859 ` 265` ``` using main_part_null_part_Un[OF F] by auto ``` hoelzl@40859 ` 266` ``` also have "\ = main_part (?F y) \ ?N" ``` hoelzl@40859 ` 267` ``` using y N by auto ``` hoelzl@40859 ` 268` ``` finally show ?thesis ``` hoelzl@40859 ` 269` ``` using F sets by auto ``` hoelzl@40859 ` 270` ``` next ``` hoelzl@40859 ` 271` ``` assume "y \ f`space M" then have "?F y = {}" by auto ``` hoelzl@40859 ` 272` ``` then show ?thesis using sets by auto ``` hoelzl@40859 ` 273` ``` qed } ``` hoelzl@40859 ` 274` ``` moreover { ``` hoelzl@40859 ` 275` ``` have "?F (f x) - ?N = main_part (?F (f x)) \ null_part (?F (f x)) - ?N" ``` hoelzl@40859 ` 276` ``` using main_part_null_part_Un[OF F] by auto ``` hoelzl@40859 ` 277` ``` also have "\ = main_part (?F (f x)) - ?N" ``` hoelzl@40859 ` 278` ``` using N `x \ space M` by auto ``` hoelzl@40859 ` 279` ``` finally have "?F (f x) - ?N \ sets M" ``` hoelzl@40859 ` 280` ``` using F sets by auto } ``` hoelzl@40859 ` 281` ``` ultimately show "?f' -` {?f' x} \ space M \ sets M" by auto ``` hoelzl@40859 ` 282` ``` next ``` hoelzl@40859 ` 283` ``` show "AE x. f x = ?f' x" ``` hoelzl@40859 ` 284` ``` by (rule AE_I', rule sets) auto ``` hoelzl@40859 ` 285` ``` qed ``` hoelzl@40859 ` 286` ```qed ``` hoelzl@40859 ` 287` hoelzl@40859 ` 288` ```lemma (in completeable_measure_space) completion_ex_borel_measurable: ``` hoelzl@40859 ` 289` ``` fixes g :: "'a \ pinfreal" ``` hoelzl@40859 ` 290` ``` assumes g: "g \ borel_measurable completion" ``` hoelzl@40859 ` 291` ``` shows "\g'\borel_measurable M. (AE x. g x = g' x)" ``` hoelzl@40859 ` 292` ```proof - ``` hoelzl@40859 ` 293` ``` from g[THEN completion.borel_measurable_implies_simple_function_sequence] ``` hoelzl@40859 ` 294` ``` obtain f where "\i. completion.simple_function (f i)" "f \ g" by auto ``` hoelzl@40859 ` 295` ``` then have "\i. \f'. simple_function f' \ (AE x. f i x = f' x)" ``` hoelzl@40859 ` 296` ``` using completion_ex_simple_function by auto ``` hoelzl@40859 ` 297` ``` from this[THEN choice] obtain f' where ``` hoelzl@40859 ` 298` ``` sf: "\i. simple_function (f' i)" and ``` hoelzl@40859 ` 299` ``` AE: "\i. AE x. f i x = f' i x" by auto ``` hoelzl@40859 ` 300` ``` show ?thesis ``` hoelzl@40859 ` 301` ``` proof (intro bexI) ``` hoelzl@40859 ` 302` ``` from AE[unfolded all_AE_countable] ``` hoelzl@40859 ` 303` ``` show "AE x. g x = (SUP i. f' i) x" (is "AE x. g x = ?f x") ``` hoelzl@40859 ` 304` ``` proof (rule AE_mp, safe intro!: AE_cong) ``` hoelzl@40859 ` 305` ``` fix x assume eq: "\i. f i x = f' i x" ``` hoelzl@40859 ` 306` ``` have "g x = (SUP i. f i x)" ``` hoelzl@40859 ` 307` ``` using `f \ g` unfolding isoton_def SUPR_fun_expand by auto ``` hoelzl@40859 ` 308` ``` then show "g x = ?f x" ``` hoelzl@40859 ` 309` ``` using eq unfolding SUPR_fun_expand by auto ``` hoelzl@40859 ` 310` ``` qed ``` hoelzl@40859 ` 311` ``` show "?f \ borel_measurable M" ``` hoelzl@40859 ` 312` ``` using sf by (auto intro!: borel_measurable_SUP ``` hoelzl@40859 ` 313` ``` intro: borel_measurable_simple_function) ``` hoelzl@40859 ` 314` ``` qed ``` hoelzl@40859 ` 315` ```qed ``` hoelzl@40859 ` 316` hoelzl@40859 ` 317` ```end ```