src/HOL/Probability/Lebesgue.thy
 author hoelzl Thu Mar 04 21:52:26 2010 +0100 (2010-03-04) changeset 35582 b16d99a72dc9 child 35692 f1315bbf1bc9 permissions -rw-r--r--
Add Lebesgue integral and probability space.
 hoelzl@35582 ` 1` ```header {*Lebesgue Integration*} ``` hoelzl@35582 ` 2` hoelzl@35582 ` 3` ```theory Lebesgue ``` hoelzl@35582 ` 4` ```imports Measure Borel ``` hoelzl@35582 ` 5` ```begin ``` hoelzl@35582 ` 6` hoelzl@35582 ` 7` ```text{*From the HOL4 Hurd/Coble Lebesgue integration, translated by Armin Heller and Johannes Hoelzl.*} ``` hoelzl@35582 ` 8` hoelzl@35582 ` 9` ```definition ``` hoelzl@35582 ` 10` ``` "pos_part f = (\x. max 0 (f x))" ``` hoelzl@35582 ` 11` hoelzl@35582 ` 12` ```definition ``` hoelzl@35582 ` 13` ``` "neg_part f = (\x. - min 0 (f x))" ``` hoelzl@35582 ` 14` hoelzl@35582 ` 15` ```definition ``` hoelzl@35582 ` 16` ``` "nonneg f = (\x. 0 \ f x)" ``` hoelzl@35582 ` 17` hoelzl@35582 ` 18` ```lemma nonneg_pos_part[intro!]: ``` hoelzl@35582 ` 19` ``` fixes f :: "'c \ 'd\{linorder,zero}" ``` hoelzl@35582 ` 20` ``` shows "nonneg (pos_part f)" ``` hoelzl@35582 ` 21` ``` unfolding nonneg_def pos_part_def by auto ``` hoelzl@35582 ` 22` hoelzl@35582 ` 23` ```lemma nonneg_neg_part[intro!]: ``` hoelzl@35582 ` 24` ``` fixes f :: "'c \ 'd\{linorder,ordered_ab_group_add}" ``` hoelzl@35582 ` 25` ``` shows "nonneg (neg_part f)" ``` hoelzl@35582 ` 26` ``` unfolding nonneg_def neg_part_def min_def by auto ``` hoelzl@35582 ` 27` hoelzl@35582 ` 28` ```context measure_space ``` hoelzl@35582 ` 29` ```begin ``` hoelzl@35582 ` 30` hoelzl@35582 ` 31` ```definition ``` hoelzl@35582 ` 32` ``` "pos_simple f = ``` hoelzl@35582 ` 33` ``` { (s :: nat set, a, x). ``` hoelzl@35582 ` 34` ``` finite s \ nonneg f \ nonneg x \ a ` s \ sets M \ ``` hoelzl@35582 ` 35` ``` (\t \ space M. (\!i\s. t\a i) \ (\i\s. t \ a i \ f t = x i)) }" ``` hoelzl@35582 ` 36` hoelzl@35582 ` 37` ```definition ``` hoelzl@35582 ` 38` ``` "pos_simple_integral \ \(s, a, x). \ i \ s. x i * measure M (a i)" ``` hoelzl@35582 ` 39` hoelzl@35582 ` 40` ```definition ``` hoelzl@35582 ` 41` ``` "psfis f = pos_simple_integral ` (pos_simple f)" ``` hoelzl@35582 ` 42` hoelzl@35582 ` 43` ```definition ``` hoelzl@35582 ` 44` ``` "nnfis f = { y. \u x. mono_convergent u f (space M) \ ``` hoelzl@35582 ` 45` ``` (\n. x n \ psfis (u n)) \ x ----> y }" ``` hoelzl@35582 ` 46` hoelzl@35582 ` 47` ```definition ``` hoelzl@35582 ` 48` ``` "integrable f \ (\x. x \ nnfis (pos_part f)) \ (\y. y \ nnfis (neg_part f))" ``` hoelzl@35582 ` 49` hoelzl@35582 ` 50` ```definition ``` hoelzl@35582 ` 51` ``` "integral f = (THE i :: real. i \ nnfis (pos_part f)) - (THE j. j \ nnfis (neg_part f))" ``` hoelzl@35582 ` 52` hoelzl@35582 ` 53` ```definition ``` hoelzl@35582 ` 54` ``` "enumerate s \ SOME f. bij_betw f UNIV s" ``` hoelzl@35582 ` 55` hoelzl@35582 ` 56` ```definition ``` hoelzl@35582 ` 57` ``` "countable_space_integral f \ ``` hoelzl@35582 ` 58` ``` let e = enumerate (f ` space M) in ``` hoelzl@35582 ` 59` ``` suminf (\r. e r * measure M (f -` {e r} \ space M))" ``` hoelzl@35582 ` 60` hoelzl@35582 ` 61` ```definition ``` hoelzl@35582 ` 62` ``` "RN_deriv v \ SOME f. measure_space (M\measure := v\) \ ``` hoelzl@35582 ` 63` ``` f \ borel_measurable M \ ``` hoelzl@35582 ` 64` ``` (\a \ sets M. (integral (\x. f x * indicator_fn a x) = v a))" ``` hoelzl@35582 ` 65` hoelzl@35582 ` 66` ```lemma pos_simpleE[consumes 1]: ``` hoelzl@35582 ` 67` ``` assumes ps: "(s, a, x) \ pos_simple f" ``` hoelzl@35582 ` 68` ``` obtains "finite s" and "nonneg f" and "nonneg x" ``` hoelzl@35582 ` 69` ``` and "a ` s \ sets M" and "(\i\s. a i) = space M" ``` hoelzl@35582 ` 70` ``` and "disjoint_family_on a s" ``` hoelzl@35582 ` 71` ``` and "\t. t \ space M \ (\!i. i \ s \ t \ a i)" ``` hoelzl@35582 ` 72` ``` and "\t i. \ t \ space M ; i \ s ; t \ a i \ \ f t = x i" ``` hoelzl@35582 ` 73` ```proof ``` hoelzl@35582 ` 74` ``` show "finite s" and "nonneg f" and "nonneg x" ``` hoelzl@35582 ` 75` ``` and as_in_M: "a ` s \ sets M" ``` hoelzl@35582 ` 76` ``` and *: "\t. t \ space M \ (\!i. i \ s \ t \ a i)" ``` hoelzl@35582 ` 77` ``` and **: "\t i. \ t \ space M ; i \ s ; t \ a i \ \ f t = x i" ``` hoelzl@35582 ` 78` ``` using ps unfolding pos_simple_def by auto ``` hoelzl@35582 ` 79` hoelzl@35582 ` 80` ``` thus t: "(\i\s. a i) = space M" ``` hoelzl@35582 ` 81` ``` proof safe ``` hoelzl@35582 ` 82` ``` fix x assume "x \ space M" ``` hoelzl@35582 ` 83` ``` from *[OF this] show "x \ (\i\s. a i)" by auto ``` hoelzl@35582 ` 84` ``` next ``` hoelzl@35582 ` 85` ``` fix t i assume "i \ s" ``` hoelzl@35582 ` 86` ``` hence "a i \ sets M" using as_in_M by auto ``` hoelzl@35582 ` 87` ``` moreover assume "t \ a i" ``` hoelzl@35582 ` 88` ``` ultimately show "t \ space M" using sets_into_space by blast ``` hoelzl@35582 ` 89` ``` qed ``` hoelzl@35582 ` 90` hoelzl@35582 ` 91` ``` show "disjoint_family_on a s" unfolding disjoint_family_on_def ``` hoelzl@35582 ` 92` ``` proof safe ``` hoelzl@35582 ` 93` ``` fix i j and t assume "i \ s" "t \ a i" and "j \ s" "t \ a j" and "i \ j" ``` hoelzl@35582 ` 94` ``` with t * show "t \ {}" by auto ``` hoelzl@35582 ` 95` ``` qed ``` hoelzl@35582 ` 96` ```qed ``` hoelzl@35582 ` 97` hoelzl@35582 ` 98` ```lemma pos_simple_cong: ``` hoelzl@35582 ` 99` ``` assumes "nonneg f" and "nonneg g" and "\t. t \ space M \ f t = g t" ``` hoelzl@35582 ` 100` ``` shows "pos_simple f = pos_simple g" ``` hoelzl@35582 ` 101` ``` unfolding pos_simple_def using assms by auto ``` hoelzl@35582 ` 102` hoelzl@35582 ` 103` ```lemma psfis_cong: ``` hoelzl@35582 ` 104` ``` assumes "nonneg f" and "nonneg g" and "\t. t \ space M \ f t = g t" ``` hoelzl@35582 ` 105` ``` shows "psfis f = psfis g" ``` hoelzl@35582 ` 106` ``` unfolding psfis_def using pos_simple_cong[OF assms] by simp ``` hoelzl@35582 ` 107` hoelzl@35582 ` 108` ```lemma pos_simple_setsum_indicator_fn: ``` hoelzl@35582 ` 109` ``` assumes ps: "(s, a, x) \ pos_simple f" ``` hoelzl@35582 ` 110` ``` and "t \ space M" ``` hoelzl@35582 ` 111` ``` shows "(\i\s. x i * indicator_fn (a i) t) = f t" ``` hoelzl@35582 ` 112` ```proof - ``` hoelzl@35582 ` 113` ``` from assms obtain i where *: "i \ s" "t \ a i" ``` hoelzl@35582 ` 114` ``` and "finite s" and xi: "x i = f t" by (auto elim!: pos_simpleE) ``` hoelzl@35582 ` 115` hoelzl@35582 ` 116` ``` have **: "(\i\s. x i * indicator_fn (a i) t) = ``` hoelzl@35582 ` 117` ``` (\j\s. if j \ {i} then x i else 0)" ``` hoelzl@35582 ` 118` ``` unfolding indicator_fn_def using assms * ``` hoelzl@35582 ` 119` ``` by (auto intro!: setsum_cong elim!: pos_simpleE) ``` hoelzl@35582 ` 120` ``` show ?thesis unfolding ** setsum_cases[OF `finite s`] xi ``` hoelzl@35582 ` 121` ``` using `i \ s` by simp ``` hoelzl@35582 ` 122` ```qed ``` hoelzl@35582 ` 123` hoelzl@35582 ` 124` ```lemma (in measure_space) measure_setsum_split: ``` hoelzl@35582 ` 125` ``` assumes "finite r" and "a \ sets M" and br_in_M: "b ` r \ sets M" ``` hoelzl@35582 ` 126` ``` assumes "(\i \ r. b i) = space M" ``` hoelzl@35582 ` 127` ``` assumes "disjoint_family_on b r" ``` hoelzl@35582 ` 128` ``` shows "(measure M) a = (\ i \ r. measure M (a \ (b i)))" ``` hoelzl@35582 ` 129` ```proof - ``` hoelzl@35582 ` 130` ``` have *: "measure M a = measure M (\i \ r. a \ b i)" ``` hoelzl@35582 ` 131` ``` using assms by auto ``` hoelzl@35582 ` 132` ``` show ?thesis unfolding * ``` hoelzl@35582 ` 133` ``` proof (rule measure_finitely_additive''[symmetric]) ``` hoelzl@35582 ` 134` ``` show "finite r" using `finite r` by auto ``` hoelzl@35582 ` 135` ``` { fix i assume "i \ r" ``` hoelzl@35582 ` 136` ``` hence "b i \ sets M" using br_in_M by auto ``` hoelzl@35582 ` 137` ``` thus "a \ b i \ sets M" using `a \ sets M` by auto ``` hoelzl@35582 ` 138` ``` } ``` hoelzl@35582 ` 139` ``` show "disjoint_family_on (\i. a \ b i) r" ``` hoelzl@35582 ` 140` ``` using `disjoint_family_on b r` ``` hoelzl@35582 ` 141` ``` unfolding disjoint_family_on_def by auto ``` hoelzl@35582 ` 142` ``` qed ``` hoelzl@35582 ` 143` ```qed ``` hoelzl@35582 ` 144` hoelzl@35582 ` 145` ```lemma (in measure_space) pos_simple_common_partition: ``` hoelzl@35582 ` 146` ``` assumes psf: "(s, a, x) \ pos_simple f" ``` hoelzl@35582 ` 147` ``` assumes psg: "(s', b, y) \ pos_simple g" ``` hoelzl@35582 ` 148` ``` obtains z z' c k where "(k, c, z) \ pos_simple f" "(k, c, z') \ pos_simple g" ``` hoelzl@35582 ` 149` ```proof - ``` hoelzl@35582 ` 150` ``` (* definitions *) ``` hoelzl@35582 ` 151` hoelzl@35582 ` 152` ``` def k == "{0 ..< card (s \ s')}" ``` hoelzl@35582 ` 153` ``` have fs: "finite s" "finite s'" "finite k" unfolding k_def ``` hoelzl@35582 ` 154` ``` using psf psg unfolding pos_simple_def by auto ``` hoelzl@35582 ` 155` ``` hence "finite (s \ s')" by simp ``` hoelzl@35582 ` 156` ``` then obtain p where p: "p ` k = s \ s'" "inj_on p k" ``` hoelzl@35582 ` 157` ``` using ex_bij_betw_nat_finite[of "s \ s'"] unfolding bij_betw_def k_def by blast ``` hoelzl@35582 ` 158` ``` def c == "\ i. a (fst (p i)) \ b (snd (p i))" ``` hoelzl@35582 ` 159` ``` def z == "\ i. x (fst (p i))" ``` hoelzl@35582 ` 160` ``` def z' == "\ i. y (snd (p i))" ``` hoelzl@35582 ` 161` hoelzl@35582 ` 162` ``` have "finite k" unfolding k_def by simp ``` hoelzl@35582 ` 163` hoelzl@35582 ` 164` ``` have "nonneg z" and "nonneg z'" ``` hoelzl@35582 ` 165` ``` using psf psg unfolding z_def z'_def pos_simple_def nonneg_def by auto ``` hoelzl@35582 ` 166` hoelzl@35582 ` 167` ``` have ck_subset_M: "c ` k \ sets M" ``` hoelzl@35582 ` 168` ``` proof ``` hoelzl@35582 ` 169` ``` fix x assume "x \ c ` k" ``` hoelzl@35582 ` 170` ``` then obtain j where "j \ k" and "x = c j" by auto ``` hoelzl@35582 ` 171` ``` hence "p j \ s \ s'" using p(1) by auto ``` hoelzl@35582 ` 172` ``` hence "a (fst (p j)) \ sets M" (is "?a \ _") ``` hoelzl@35582 ` 173` ``` and "b (snd (p j)) \ sets M" (is "?b \ _") ``` hoelzl@35582 ` 174` ``` using psf psg unfolding pos_simple_def by auto ``` hoelzl@35582 ` 175` ``` thus "x \ sets M" unfolding `x = c j` c_def using Int by simp ``` hoelzl@35582 ` 176` ``` qed ``` hoelzl@35582 ` 177` hoelzl@35582 ` 178` ``` { fix t assume "t \ space M" ``` hoelzl@35582 ` 179` ``` hence ex1s: "\!i\s. t \ a i" and ex1s': "\!i\s'. t \ b i" ``` hoelzl@35582 ` 180` ``` using psf psg unfolding pos_simple_def by auto ``` hoelzl@35582 ` 181` ``` then obtain j j' where j: "j \ s" "t \ a j" and j': "j' \ s'" "t \ b j'" ``` hoelzl@35582 ` 182` ``` by auto ``` hoelzl@35582 ` 183` ``` then obtain i :: nat where i: "(j,j') = p i" and "i \ k" using p by auto ``` hoelzl@35582 ` 184` ``` have "\!i\k. t \ c i" ``` hoelzl@35582 ` 185` ``` proof (rule ex1I[of _ i]) ``` hoelzl@35582 ` 186` ``` show "\x. x \ k \ t \ c x \ x = i" ``` hoelzl@35582 ` 187` ``` proof - ``` hoelzl@35582 ` 188` ``` fix l assume "l \ k" "t \ c l" ``` hoelzl@35582 ` 189` ``` hence "p l \ s \ s'" and t_in: "t \ a (fst (p l))" "t \ b (snd (p l))" ``` hoelzl@35582 ` 190` ``` using p unfolding c_def by auto ``` hoelzl@35582 ` 191` ``` hence "fst (p l) \ s" and "snd (p l) \ s'" by auto ``` hoelzl@35582 ` 192` ``` with t_in j j' ex1s ex1s' have "p l = (j, j')" by (cases "p l", auto) ``` hoelzl@35582 ` 193` ``` thus "l = i" ``` hoelzl@35582 ` 194` ``` using `(j, j') = p i` p(2)[THEN inj_onD] `l \ k` `i \ k` by auto ``` hoelzl@35582 ` 195` ``` qed ``` hoelzl@35582 ` 196` hoelzl@35582 ` 197` ``` show "i \ k \ t \ c i" ``` hoelzl@35582 ` 198` ``` using `i \ k` `t \ a j` `t \ b j'` c_def i[symmetric] by auto ``` hoelzl@35582 ` 199` ``` qed auto ``` hoelzl@35582 ` 200` ``` } note ex1 = this ``` hoelzl@35582 ` 201` hoelzl@35582 ` 202` ``` show thesis ``` hoelzl@35582 ` 203` ``` proof (rule that) ``` hoelzl@35582 ` 204` ``` { fix t i assume "t \ space M" and "i \ k" ``` hoelzl@35582 ` 205` ``` hence "p i \ s \ s'" using p(1) by auto ``` hoelzl@35582 ` 206` ``` hence "fst (p i) \ s" by auto ``` hoelzl@35582 ` 207` ``` moreover ``` hoelzl@35582 ` 208` ``` assume "t \ c i" ``` hoelzl@35582 ` 209` ``` hence "t \ a (fst (p i))" unfolding c_def by auto ``` hoelzl@35582 ` 210` ``` ultimately have "f t = z i" using psf `t \ space M` ``` hoelzl@35582 ` 211` ``` unfolding z_def pos_simple_def by auto ``` hoelzl@35582 ` 212` ``` } ``` hoelzl@35582 ` 213` ``` thus "(k, c, z) \ pos_simple f" ``` hoelzl@35582 ` 214` ``` using psf `finite k` `nonneg z` ck_subset_M ex1 ``` hoelzl@35582 ` 215` ``` unfolding pos_simple_def by auto ``` hoelzl@35582 ` 216` hoelzl@35582 ` 217` ``` { fix t i assume "t \ space M" and "i \ k" ``` hoelzl@35582 ` 218` ``` hence "p i \ s \ s'" using p(1) by auto ``` hoelzl@35582 ` 219` ``` hence "snd (p i) \ s'" by auto ``` hoelzl@35582 ` 220` ``` moreover ``` hoelzl@35582 ` 221` ``` assume "t \ c i" ``` hoelzl@35582 ` 222` ``` hence "t \ b (snd (p i))" unfolding c_def by auto ``` hoelzl@35582 ` 223` ``` ultimately have "g t = z' i" using psg `t \ space M` ``` hoelzl@35582 ` 224` ``` unfolding z'_def pos_simple_def by auto ``` hoelzl@35582 ` 225` ``` } ``` hoelzl@35582 ` 226` ``` thus "(k, c, z') \ pos_simple g" ``` hoelzl@35582 ` 227` ``` using psg `finite k` `nonneg z'` ck_subset_M ex1 ``` hoelzl@35582 ` 228` ``` unfolding pos_simple_def by auto ``` hoelzl@35582 ` 229` ``` qed ``` hoelzl@35582 ` 230` ```qed ``` hoelzl@35582 ` 231` hoelzl@35582 ` 232` ```lemma (in measure_space) pos_simple_integral_equal: ``` hoelzl@35582 ` 233` ``` assumes psx: "(s, a, x) \ pos_simple f" ``` hoelzl@35582 ` 234` ``` assumes psy: "(s', b, y) \ pos_simple f" ``` hoelzl@35582 ` 235` ``` shows "pos_simple_integral (s, a, x) = pos_simple_integral (s', b, y)" ``` hoelzl@35582 ` 236` ``` unfolding pos_simple_integral_def ``` hoelzl@35582 ` 237` ```proof simp ``` hoelzl@35582 ` 238` ``` have "(\i\s. x i * measure M (a i)) = ``` hoelzl@35582 ` 239` ``` (\i\s. (\j \ s'. x i * measure M (a i \ b j)))" (is "?left = _") ``` hoelzl@35582 ` 240` ``` using psy psx unfolding setsum_right_distrib[symmetric] ``` hoelzl@35582 ` 241` ``` by (auto intro!: setsum_cong measure_setsum_split elim!: pos_simpleE) ``` hoelzl@35582 ` 242` ``` also have "... = (\i\s. (\j \ s'. y j * measure M (a i \ b j)))" ``` hoelzl@35582 ` 243` ``` proof (rule setsum_cong, simp, rule setsum_cong, simp_all) ``` hoelzl@35582 ` 244` ``` fix i j assume i: "i \ s" and j: "j \ s'" ``` hoelzl@35582 ` 245` ``` hence "a i \ sets M" using psx by (auto elim!: pos_simpleE) ``` hoelzl@35582 ` 246` hoelzl@35582 ` 247` ``` show "measure M (a i \ b j) = 0 \ x i = y j" ``` hoelzl@35582 ` 248` ``` proof (cases "a i \ b j = {}") ``` hoelzl@35582 ` 249` ``` case True thus ?thesis using empty_measure by simp ``` hoelzl@35582 ` 250` ``` next ``` hoelzl@35582 ` 251` ``` case False then obtain t where t: "t \ a i" "t \ b j" by auto ``` hoelzl@35582 ` 252` ``` hence "t \ space M" using `a i \ sets M` sets_into_space by auto ``` hoelzl@35582 ` 253` ``` with psx psy t i j have "x i = f t" and "y j = f t" ``` hoelzl@35582 ` 254` ``` unfolding pos_simple_def by auto ``` hoelzl@35582 ` 255` ``` thus ?thesis by simp ``` hoelzl@35582 ` 256` ``` qed ``` hoelzl@35582 ` 257` ``` qed ``` hoelzl@35582 ` 258` ``` also have "... = (\j\s'. (\i\s. y j * measure M (a i \ b j)))" ``` hoelzl@35582 ` 259` ``` by (subst setsum_commute) simp ``` hoelzl@35582 ` 260` ``` also have "... = (\i\s'. y i * measure M (b i))" (is "?sum_sum = ?right") ``` hoelzl@35582 ` 261` ``` proof (rule setsum_cong) ``` hoelzl@35582 ` 262` ``` fix j assume "j \ s'" ``` hoelzl@35582 ` 263` ``` have "y j * measure M (b j) = (\i\s. y j * measure M (b j \ a i))" ``` hoelzl@35582 ` 264` ``` using psx psy `j \ s'` unfolding setsum_right_distrib[symmetric] ``` hoelzl@35582 ` 265` ``` by (auto intro!: measure_setsum_split elim!: pos_simpleE) ``` hoelzl@35582 ` 266` ``` thus "(\i\s. y j * measure M (a i \ b j)) = y j * measure M (b j)" ``` hoelzl@35582 ` 267` ``` by (auto intro!: setsum_cong arg_cong[where f="measure M"]) ``` hoelzl@35582 ` 268` ``` qed simp ``` hoelzl@35582 ` 269` ``` finally show "?left = ?right" . ``` hoelzl@35582 ` 270` ```qed ``` hoelzl@35582 ` 271` hoelzl@35582 ` 272` ```lemma (in measure_space)psfis_present: ``` hoelzl@35582 ` 273` ``` assumes "A \ psfis f" ``` hoelzl@35582 ` 274` ``` assumes "B \ psfis g" ``` hoelzl@35582 ` 275` ``` obtains z z' c k where ``` hoelzl@35582 ` 276` ``` "A = pos_simple_integral (k, c, z)" ``` hoelzl@35582 ` 277` ``` "B = pos_simple_integral (k, c, z')" ``` hoelzl@35582 ` 278` ``` "(k, c, z) \ pos_simple f" ``` hoelzl@35582 ` 279` ``` "(k, c, z') \ pos_simple g" ``` hoelzl@35582 ` 280` ```using assms ``` hoelzl@35582 ` 281` ```proof - ``` hoelzl@35582 ` 282` ``` from assms obtain s a x s' b y where ``` hoelzl@35582 ` 283` ``` ps: "(s, a, x) \ pos_simple f" "(s', b, y) \ pos_simple g" and ``` hoelzl@35582 ` 284` ``` A: "A = pos_simple_integral (s, a, x)" and ``` hoelzl@35582 ` 285` ``` B: "B = pos_simple_integral (s', b, y)" ``` hoelzl@35582 ` 286` ``` unfolding psfis_def pos_simple_integral_def by auto ``` hoelzl@35582 ` 287` hoelzl@35582 ` 288` ``` guess z z' c k using pos_simple_common_partition[OF ps] . note part = this ``` hoelzl@35582 ` 289` ``` show thesis ``` hoelzl@35582 ` 290` ``` proof (rule that[of k c z z', OF _ _ part]) ``` hoelzl@35582 ` 291` ``` show "A = pos_simple_integral (k, c, z)" ``` hoelzl@35582 ` 292` ``` unfolding A by (rule pos_simple_integral_equal[OF ps(1) part(1)]) ``` hoelzl@35582 ` 293` ``` show "B = pos_simple_integral (k, c, z')" ``` hoelzl@35582 ` 294` ``` unfolding B by (rule pos_simple_integral_equal[OF ps(2) part(2)]) ``` hoelzl@35582 ` 295` ``` qed ``` hoelzl@35582 ` 296` ```qed ``` hoelzl@35582 ` 297` hoelzl@35582 ` 298` ```lemma (in measure_space) pos_simple_integral_add: ``` hoelzl@35582 ` 299` ``` assumes "(s, a, x) \ pos_simple f" ``` hoelzl@35582 ` 300` ``` assumes "(s', b, y) \ pos_simple g" ``` hoelzl@35582 ` 301` ``` obtains s'' c z where ``` hoelzl@35582 ` 302` ``` "(s'', c, z) \ pos_simple (\x. f x + g x)" ``` hoelzl@35582 ` 303` ``` "(pos_simple_integral (s, a, x) + ``` hoelzl@35582 ` 304` ``` pos_simple_integral (s', b, y) = ``` hoelzl@35582 ` 305` ``` pos_simple_integral (s'', c, z))" ``` hoelzl@35582 ` 306` ```using assms ``` hoelzl@35582 ` 307` ```proof - ``` hoelzl@35582 ` 308` ``` guess z z' c k ``` hoelzl@35582 ` 309` ``` by (rule pos_simple_common_partition[OF `(s, a, x) \ pos_simple f ` `(s', b, y) \ pos_simple g`]) ``` hoelzl@35582 ` 310` ``` note kczz' = this ``` hoelzl@35582 ` 311` ``` have x: "pos_simple_integral (s, a, x) = pos_simple_integral (k, c, z)" ``` hoelzl@35582 ` 312` ``` by (rule pos_simple_integral_equal) (fact, fact) ``` hoelzl@35582 ` 313` ``` have y: "pos_simple_integral (s', b, y) = pos_simple_integral (k, c, z')" ``` hoelzl@35582 ` 314` ``` by (rule pos_simple_integral_equal) (fact, fact) ``` hoelzl@35582 ` 315` hoelzl@35582 ` 316` ``` have "pos_simple_integral (k, c, (\ x. z x + z' x)) ``` hoelzl@35582 ` 317` ``` = (\ x \ k. (z x + z' x) * measure M (c x))" ``` hoelzl@35582 ` 318` ``` unfolding pos_simple_integral_def by auto ``` hoelzl@35582 ` 319` ``` also have "\ = (\ x \ k. z x * measure M (c x) + z' x * measure M (c x))" using real_add_mult_distrib by auto ``` hoelzl@35582 ` 320` ``` also have "\ = (\ x \ k. z x * measure M (c x)) + (\ x \ k. z' x * measure M (c x))" using setsum_addf by auto ``` hoelzl@35582 ` 321` ``` also have "\ = pos_simple_integral (k, c, z) + pos_simple_integral (k, c, z')" unfolding pos_simple_integral_def by auto ``` hoelzl@35582 ` 322` ``` finally have ths: "pos_simple_integral (s, a, x) + pos_simple_integral (s', b, y) = ``` hoelzl@35582 ` 323` ``` pos_simple_integral (k, c, (\ x. z x + z' x))" using x y by auto ``` hoelzl@35582 ` 324` ``` show ?thesis ``` hoelzl@35582 ` 325` ``` apply (rule that[of k c "(\ x. z x + z' x)", OF _ ths]) ``` hoelzl@35582 ` 326` ``` using kczz' unfolding pos_simple_def nonneg_def by (auto intro!: add_nonneg_nonneg) ``` hoelzl@35582 ` 327` ```qed ``` hoelzl@35582 ` 328` hoelzl@35582 ` 329` ```lemma psfis_add: ``` hoelzl@35582 ` 330` ``` assumes "a \ psfis f" "b \ psfis g" ``` hoelzl@35582 ` 331` ``` shows "a + b \ psfis (\x. f x + g x)" ``` hoelzl@35582 ` 332` ```using assms pos_simple_integral_add ``` hoelzl@35582 ` 333` ```unfolding psfis_def by auto blast ``` hoelzl@35582 ` 334` hoelzl@35582 ` 335` ```lemma pos_simple_integral_mono_on_mspace: ``` hoelzl@35582 ` 336` ``` assumes f: "(s, a, x) \ pos_simple f" ``` hoelzl@35582 ` 337` ``` assumes g: "(s', b, y) \ pos_simple g" ``` hoelzl@35582 ` 338` ``` assumes mono: "\ x. x \ space M \ f x \ g x" ``` hoelzl@35582 ` 339` ``` shows "pos_simple_integral (s, a, x) \ pos_simple_integral (s', b, y)" ``` hoelzl@35582 ` 340` ```using assms ``` hoelzl@35582 ` 341` ```proof - ``` hoelzl@35582 ` 342` ``` guess z z' c k by (rule pos_simple_common_partition[OF f g]) ``` hoelzl@35582 ` 343` ``` note kczz' = this ``` hoelzl@35582 ` 344` ``` (* w = z and w' = z' except where c _ = {} or undef *) ``` hoelzl@35582 ` 345` ``` def w == "\ i. if i \ k \ c i = {} then 0 else z i" ``` hoelzl@35582 ` 346` ``` def w' == "\ i. if i \ k \ c i = {} then 0 else z' i" ``` hoelzl@35582 ` 347` ``` { fix i ``` hoelzl@35582 ` 348` ``` have "w i \ w' i" ``` hoelzl@35582 ` 349` ``` proof (cases "i \ k \ c i = {}") ``` hoelzl@35582 ` 350` ``` case False hence "i \ k" "c i \ {}" by auto ``` hoelzl@35582 ` 351` ``` then obtain v where v: "v \ c i" and "c i \ sets M" ``` hoelzl@35582 ` 352` ``` using kczz'(1) unfolding pos_simple_def by blast ``` hoelzl@35582 ` 353` ``` hence "v \ space M" using sets_into_space by blast ``` hoelzl@35582 ` 354` ``` with mono[OF `v \ space M`] kczz' `i \ k` `v \ c i` ``` hoelzl@35582 ` 355` ``` have "z i \ z' i" unfolding pos_simple_def by simp ``` hoelzl@35582 ` 356` ``` thus ?thesis unfolding w_def w'_def using False by auto ``` hoelzl@35582 ` 357` ``` next ``` hoelzl@35582 ` 358` ``` case True thus ?thesis unfolding w_def w'_def by auto ``` hoelzl@35582 ` 359` ``` qed ``` hoelzl@35582 ` 360` ``` } note w_mn = this ``` hoelzl@35582 ` 361` hoelzl@35582 ` 362` ``` (* some technical stuff for the calculation*) ``` hoelzl@35582 ` 363` ``` have "\ i. i \ k \ c i \ sets M" using kczz' unfolding pos_simple_def by auto ``` hoelzl@35582 ` 364` ``` hence "\ i. i \ k \ measure M (c i) \ 0" using positive by auto ``` hoelzl@35582 ` 365` ``` hence w_mono: "\ i. i \ k \ w i * measure M (c i) \ w' i * measure M (c i)" ``` hoelzl@35582 ` 366` ``` using mult_right_mono w_mn by blast ``` hoelzl@35582 ` 367` hoelzl@35582 ` 368` ``` { fix i have "\i \ k ; z i \ w i\ \ measure M (c i) = 0" ``` hoelzl@35582 ` 369` ``` unfolding w_def by (cases "c i = {}") auto } ``` hoelzl@35582 ` 370` ``` hence zw: "\ i. i \ k \ z i * measure M (c i) = w i * measure M (c i)" by auto ``` hoelzl@35582 ` 371` hoelzl@35582 ` 372` ``` { fix i have "i \ k \ z i * measure M (c i) = w i * measure M (c i)" ``` hoelzl@35582 ` 373` ``` unfolding w_def by (cases "c i = {}") simp_all } ``` hoelzl@35582 ` 374` ``` note zw = this ``` hoelzl@35582 ` 375` hoelzl@35582 ` 376` ``` { fix i have "i \ k \ z' i * measure M (c i) = w' i * measure M (c i)" ``` hoelzl@35582 ` 377` ``` unfolding w'_def by (cases "c i = {}") simp_all } ``` hoelzl@35582 ` 378` ``` note z'w' = this ``` hoelzl@35582 ` 379` hoelzl@35582 ` 380` ``` (* the calculation *) ``` hoelzl@35582 ` 381` ``` have "pos_simple_integral (s, a, x) = pos_simple_integral (k, c, z)" ``` hoelzl@35582 ` 382` ``` using f kczz'(1) by (rule pos_simple_integral_equal) ``` hoelzl@35582 ` 383` ``` also have "\ = (\ i \ k. z i * measure M (c i))" ``` hoelzl@35582 ` 384` ``` unfolding pos_simple_integral_def by auto ``` hoelzl@35582 ` 385` ``` also have "\ = (\ i \ k. w i * measure M (c i))" ``` hoelzl@35582 ` 386` ``` using setsum_cong2[of k, OF zw] by auto ``` hoelzl@35582 ` 387` ``` also have "\ \ (\ i \ k. w' i * measure M (c i))" ``` hoelzl@35582 ` 388` ``` using setsum_mono[OF w_mono, of k] by auto ``` hoelzl@35582 ` 389` ``` also have "\ = (\ i \ k. z' i * measure M (c i))" ``` hoelzl@35582 ` 390` ``` using setsum_cong2[of k, OF z'w'] by auto ``` hoelzl@35582 ` 391` ``` also have "\ = pos_simple_integral (k, c, z')" ``` hoelzl@35582 ` 392` ``` unfolding pos_simple_integral_def by auto ``` hoelzl@35582 ` 393` ``` also have "\ = pos_simple_integral (s', b, y)" ``` hoelzl@35582 ` 394` ``` using kczz'(2) g by (rule pos_simple_integral_equal) ``` hoelzl@35582 ` 395` ``` finally show "pos_simple_integral (s, a, x) \ pos_simple_integral (s', b, y)" ``` hoelzl@35582 ` 396` ``` by simp ``` hoelzl@35582 ` 397` ```qed ``` hoelzl@35582 ` 398` hoelzl@35582 ` 399` ```lemma pos_simple_integral_mono: ``` hoelzl@35582 ` 400` ``` assumes a: "(s, a, x) \ pos_simple f" "(s', b, y) \ pos_simple g" ``` hoelzl@35582 ` 401` ``` assumes "\ z. f z \ g z" ``` hoelzl@35582 ` 402` ``` shows "pos_simple_integral (s, a, x) \ pos_simple_integral (s', b, y)" ``` hoelzl@35582 ` 403` ```using assms pos_simple_integral_mono_on_mspace by auto ``` hoelzl@35582 ` 404` hoelzl@35582 ` 405` ```lemma psfis_mono: ``` hoelzl@35582 ` 406` ``` assumes "a \ psfis f" "b \ psfis g" ``` hoelzl@35582 ` 407` ``` assumes "\ x. x \ space M \ f x \ g x" ``` hoelzl@35582 ` 408` ``` shows "a \ b" ``` hoelzl@35582 ` 409` ```using assms pos_simple_integral_mono_on_mspace unfolding psfis_def by auto ``` hoelzl@35582 ` 410` hoelzl@35582 ` 411` ```lemma pos_simple_fn_integral_unique: ``` hoelzl@35582 ` 412` ``` assumes "(s, a, x) \ pos_simple f" "(s', b, y) \ pos_simple f" ``` hoelzl@35582 ` 413` ``` shows "pos_simple_integral (s, a, x) = pos_simple_integral (s', b, y)" ``` hoelzl@35582 ` 414` ```using assms real_le_antisym real_le_refl pos_simple_integral_mono by metis ``` hoelzl@35582 ` 415` hoelzl@35582 ` 416` ```lemma psfis_unique: ``` hoelzl@35582 ` 417` ``` assumes "a \ psfis f" "b \ psfis f" ``` hoelzl@35582 ` 418` ``` shows "a = b" ``` hoelzl@35582 ` 419` ```using assms real_le_antisym real_le_refl psfis_mono by metis ``` hoelzl@35582 ` 420` hoelzl@35582 ` 421` ```lemma pos_simple_integral_indicator: ``` hoelzl@35582 ` 422` ``` assumes "A \ sets M" ``` hoelzl@35582 ` 423` ``` obtains s a x where ``` hoelzl@35582 ` 424` ``` "(s, a, x) \ pos_simple (indicator_fn A)" ``` hoelzl@35582 ` 425` ``` "measure M A = pos_simple_integral (s, a, x)" ``` hoelzl@35582 ` 426` ```using assms ``` hoelzl@35582 ` 427` ```proof - ``` hoelzl@35582 ` 428` ``` def s == "{0, 1} :: nat set" ``` hoelzl@35582 ` 429` ``` def a == "\ i :: nat. if i = 0 then A else space M - A" ``` hoelzl@35582 ` 430` ``` def x == "\ i :: nat. if i = 0 then 1 else (0 :: real)" ``` hoelzl@35582 ` 431` ``` have eq: "pos_simple_integral (s, a, x) = measure M A" ``` hoelzl@35582 ` 432` ``` unfolding s_def a_def x_def pos_simple_integral_def by auto ``` hoelzl@35582 ` 433` ``` have "(s, a, x) \ pos_simple (indicator_fn A)" ``` hoelzl@35582 ` 434` ``` unfolding pos_simple_def indicator_fn_def s_def a_def x_def nonneg_def ``` hoelzl@35582 ` 435` ``` using assms sets_into_space by auto ``` hoelzl@35582 ` 436` ``` from that[OF this] eq show thesis by auto ``` hoelzl@35582 ` 437` ```qed ``` hoelzl@35582 ` 438` hoelzl@35582 ` 439` ```lemma psfis_indicator: ``` hoelzl@35582 ` 440` ``` assumes "A \ sets M" ``` hoelzl@35582 ` 441` ``` shows "measure M A \ psfis (indicator_fn A)" ``` hoelzl@35582 ` 442` ```using pos_simple_integral_indicator[OF assms] ``` hoelzl@35582 ` 443` ``` unfolding psfis_def image_def by auto ``` hoelzl@35582 ` 444` hoelzl@35582 ` 445` ```lemma pos_simple_integral_mult: ``` hoelzl@35582 ` 446` ``` assumes f: "(s, a, x) \ pos_simple f" ``` hoelzl@35582 ` 447` ``` assumes "0 \ z" ``` hoelzl@35582 ` 448` ``` obtains s' b y where ``` hoelzl@35582 ` 449` ``` "(s', b, y) \ pos_simple (\x. z * f x)" ``` hoelzl@35582 ` 450` ``` "pos_simple_integral (s', b, y) = z * pos_simple_integral (s, a, x)" ``` hoelzl@35582 ` 451` ``` using assms that[of s a "\i. z * x i"] ``` hoelzl@35582 ` 452` ``` by (simp add: pos_simple_def pos_simple_integral_def setsum_right_distrib algebra_simps nonneg_def mult_nonneg_nonneg) ``` hoelzl@35582 ` 453` hoelzl@35582 ` 454` ```lemma psfis_mult: ``` hoelzl@35582 ` 455` ``` assumes "r \ psfis f" ``` hoelzl@35582 ` 456` ``` assumes "0 \ z" ``` hoelzl@35582 ` 457` ``` shows "z * r \ psfis (\x. z * f x)" ``` hoelzl@35582 ` 458` ```using assms ``` hoelzl@35582 ` 459` ```proof - ``` hoelzl@35582 ` 460` ``` from assms obtain s a x ``` hoelzl@35582 ` 461` ``` where sax: "(s, a, x) \ pos_simple f" ``` hoelzl@35582 ` 462` ``` and r: "r = pos_simple_integral (s, a, x)" ``` hoelzl@35582 ` 463` ``` unfolding psfis_def image_def by auto ``` hoelzl@35582 ` 464` ``` obtain s' b y where ``` hoelzl@35582 ` 465` ``` "(s', b, y) \ pos_simple (\x. z * f x)" ``` hoelzl@35582 ` 466` ``` "z * pos_simple_integral (s, a, x) = pos_simple_integral (s', b, y)" ``` hoelzl@35582 ` 467` ``` using pos_simple_integral_mult[OF sax `0 \ z`, of thesis] by auto ``` hoelzl@35582 ` 468` ``` thus ?thesis using r unfolding psfis_def image_def by auto ``` hoelzl@35582 ` 469` ```qed ``` hoelzl@35582 ` 470` hoelzl@35582 ` 471` ```lemma pos_simple_integral_setsum_image: ``` hoelzl@35582 ` 472` ``` assumes "finite P" ``` hoelzl@35582 ` 473` ``` assumes "\ i. i \ P \ (s i, a i, x i) \ pos_simple (f i)" ``` hoelzl@35582 ` 474` ``` obtains s' a' x' where ``` hoelzl@35582 ` 475` ``` "(s', a', x') \ pos_simple (\t. (\ i \ P. f i t))" ``` hoelzl@35582 ` 476` ``` "pos_simple_integral (s', a', x') = (\ i \ P. pos_simple_integral (s i, a i, x i))" ``` hoelzl@35582 ` 477` ```using assms that ``` hoelzl@35582 ` 478` ```proof (induct P arbitrary:thesis rule:finite.induct) ``` hoelzl@35582 ` 479` ``` case emptyI note asms = this ``` hoelzl@35582 ` 480` ``` def s' == "{0 :: nat}" ``` hoelzl@35582 ` 481` ``` def a' == "\ x. if x = (0 :: nat) then space M else {}" ``` hoelzl@35582 ` 482` ``` def x' == "\ x :: nat. (0 :: real)" ``` hoelzl@35582 ` 483` ``` have "(s', a', x') \ pos_simple (\ t. 0)" ``` hoelzl@35582 ` 484` ``` unfolding s'_def a'_def x'_def pos_simple_def nonneg_def by auto ``` hoelzl@35582 ` 485` ``` moreover have "pos_simple_integral (s', a', x') = 0" ``` hoelzl@35582 ` 486` ``` unfolding s'_def a'_def x'_def pos_simple_integral_def by auto ``` hoelzl@35582 ` 487` ``` ultimately show ?case using asms by auto ``` hoelzl@35582 ` 488` ```next ``` hoelzl@35582 ` 489` hoelzl@35582 ` 490` ``` case (insertI P c) note asms = this ``` hoelzl@35582 ` 491` ``` then obtain s' a' x' where ``` hoelzl@35582 ` 492` ``` sax: "(s', a', x') \ pos_simple (\t. \i\P. f i t)" ``` hoelzl@35582 ` 493` ``` "pos_simple_integral (s', a', x') = ``` hoelzl@35582 ` 494` ``` (\i\P. pos_simple_integral (s i, a i, x i))" ``` hoelzl@35582 ` 495` ``` by auto ``` hoelzl@35582 ` 496` hoelzl@35582 ` 497` ``` { assume "c \ P" ``` hoelzl@35582 ` 498` ``` hence "P = insert c P" by auto ``` hoelzl@35582 ` 499` ``` hence thesis using asms sax by auto ``` hoelzl@35582 ` 500` ``` } ``` hoelzl@35582 ` 501` ``` moreover ``` hoelzl@35582 ` 502` ``` { assume "c \ P" ``` hoelzl@35582 ` 503` ``` from asms obtain s'' a'' x'' where ``` hoelzl@35582 ` 504` ``` sax': "s'' = s c" "a'' = a c" "x'' = x c" ``` hoelzl@35582 ` 505` ``` "(s'', a'', x'') \ pos_simple (f c)" by auto ``` hoelzl@35582 ` 506` ``` from sax sax' obtain k :: "nat \ bool" and b :: "nat \ 'a \ bool" and z :: "nat \ real" where ``` hoelzl@35582 ` 507` ``` tybbie: ``` hoelzl@35582 ` 508` ``` "(k, b, z) \ pos_simple (\t. ((\i\P. f i t) + f c t))" ``` hoelzl@35582 ` 509` ``` "(pos_simple_integral (s', a', x') + ``` hoelzl@35582 ` 510` ``` pos_simple_integral (s'', a'', x'') = ``` hoelzl@35582 ` 511` ``` pos_simple_integral (k, b, z))" ``` hoelzl@35582 ` 512` ``` using pos_simple_integral_add by blast ``` hoelzl@35582 ` 513` hoelzl@35582 ` 514` ``` from tybbie have ``` hoelzl@35582 ` 515` ``` "pos_simple_integral (k, b, z) = ``` hoelzl@35582 ` 516` ``` pos_simple_integral (s', a', x') + ``` hoelzl@35582 ` 517` ``` pos_simple_integral (s'', a'', x'')" by simp ``` hoelzl@35582 ` 518` ``` also have "\ = (\ i \ P. pos_simple_integral (s i, a i, x i)) ``` hoelzl@35582 ` 519` ``` + pos_simple_integral (s c, a c, x c)" ``` hoelzl@35582 ` 520` ``` using sax sax' by auto ``` hoelzl@35582 ` 521` ``` also have "\ = (\ i \ insert c P. pos_simple_integral (s i, a i, x i))" ``` hoelzl@35582 ` 522` ``` using asms `c \ P` by auto ``` hoelzl@35582 ` 523` ``` finally have A: "pos_simple_integral (k, b, z) = (\ i \ insert c P. pos_simple_integral (s i, a i, x i))" ``` hoelzl@35582 ` 524` ``` by simp ``` hoelzl@35582 ` 525` hoelzl@35582 ` 526` ``` have "\ t. (\ i \ P. f i t) + f c t = (\ i \ insert c P. f i t)" ``` hoelzl@35582 ` 527` ``` using `c \ P` `finite P` by auto ``` hoelzl@35582 ` 528` ``` hence B: "(k, b, z) \ pos_simple (\ t. (\ i \ insert c P. f i t))" ``` hoelzl@35582 ` 529` ``` using tybbie by simp ``` hoelzl@35582 ` 530` hoelzl@35582 ` 531` ``` from A B have thesis using asms by auto ``` hoelzl@35582 ` 532` ``` } ultimately show thesis by blast ``` hoelzl@35582 ` 533` ```qed ``` hoelzl@35582 ` 534` hoelzl@35582 ` 535` ```lemma psfis_setsum_image: ``` hoelzl@35582 ` 536` ``` assumes "finite P" ``` hoelzl@35582 ` 537` ``` assumes "\i. i \ P \ a i \ psfis (f i)" ``` hoelzl@35582 ` 538` ``` shows "(setsum a P) \ psfis (\t. \i \ P. f i t)" ``` hoelzl@35582 ` 539` ```using assms ``` hoelzl@35582 ` 540` ```proof (induct P) ``` hoelzl@35582 ` 541` ``` case empty ``` hoelzl@35582 ` 542` ``` let ?s = "{0 :: nat}" ``` hoelzl@35582 ` 543` ``` let ?a = "\ i. if i = (0 :: nat) then space M else {}" ``` hoelzl@35582 ` 544` ``` let ?x = "\ (i :: nat). (0 :: real)" ``` hoelzl@35582 ` 545` ``` have "(?s, ?a, ?x) \ pos_simple (\ t. (0 :: real))" ``` hoelzl@35582 ` 546` ``` unfolding pos_simple_def image_def nonneg_def by auto ``` hoelzl@35582 ` 547` ``` moreover have "(\ i \ ?s. ?x i * measure M (?a i)) = 0" by auto ``` hoelzl@35582 ` 548` ``` ultimately have "0 \ psfis (\ t. 0)" ``` hoelzl@35582 ` 549` ``` unfolding psfis_def image_def pos_simple_integral_def nonneg_def ``` hoelzl@35582 ` 550` ``` by (auto intro!:bexI[of _ "(?s, ?a, ?x)"]) ``` hoelzl@35582 ` 551` ``` thus ?case by auto ``` hoelzl@35582 ` 552` ```next ``` hoelzl@35582 ` 553` ``` case (insert x P) note asms = this ``` hoelzl@35582 ` 554` ``` have "finite P" by fact ``` hoelzl@35582 ` 555` ``` have "x \ P" by fact ``` hoelzl@35582 ` 556` ``` have "(\i. i \ P \ a i \ psfis (f i)) \ ``` hoelzl@35582 ` 557` ``` setsum a P \ psfis (\t. \i\P. f i t)" by fact ``` hoelzl@35582 ` 558` ``` have "setsum a (insert x P) = a x + setsum a P" using `finite P` `x \ P` by auto ``` hoelzl@35582 ` 559` ``` also have "\ \ psfis (\ t. f x t + (\ i \ P. f i t))" ``` hoelzl@35582 ` 560` ``` using asms psfis_add by auto ``` hoelzl@35582 ` 561` ``` also have "\ = psfis (\ t. \ i \ insert x P. f i t)" ``` hoelzl@35582 ` 562` ``` using `x \ P` `finite P` by auto ``` hoelzl@35582 ` 563` ``` finally show ?case by simp ``` hoelzl@35582 ` 564` ```qed ``` hoelzl@35582 ` 565` hoelzl@35582 ` 566` ```lemma psfis_intro: ``` hoelzl@35582 ` 567` ``` assumes "a ` P \ sets M" and "nonneg x" and "finite P" ``` hoelzl@35582 ` 568` ``` shows "(\i\P. x i * measure M (a i)) \ psfis (\t. \i\P. x i * indicator_fn (a i) t)" ``` hoelzl@35582 ` 569` ```using assms psfis_mult psfis_indicator ``` hoelzl@35582 ` 570` ```unfolding image_def nonneg_def ``` hoelzl@35582 ` 571` ```by (auto intro!:psfis_setsum_image) ``` hoelzl@35582 ` 572` hoelzl@35582 ` 573` ```lemma psfis_nonneg: "a \ psfis f \ nonneg f" ``` hoelzl@35582 ` 574` ```unfolding psfis_def pos_simple_def by auto ``` hoelzl@35582 ` 575` hoelzl@35582 ` 576` ```lemma pos_psfis: "r \ psfis f \ 0 \ r" ``` hoelzl@35582 ` 577` ```unfolding psfis_def pos_simple_integral_def image_def pos_simple_def nonneg_def ``` hoelzl@35582 ` 578` ```using positive[unfolded positive_def] by (auto intro!:setsum_nonneg mult_nonneg_nonneg) ``` hoelzl@35582 ` 579` hoelzl@35582 ` 580` ```lemma pos_part_neg_part_borel_measurable: ``` hoelzl@35582 ` 581` ``` assumes "f \ borel_measurable M" ``` hoelzl@35582 ` 582` ``` shows "pos_part f \ borel_measurable M" and "neg_part f \ borel_measurable M" ``` hoelzl@35582 ` 583` ```using assms ``` hoelzl@35582 ` 584` ```proof - ``` hoelzl@35582 ` 585` ``` { fix a :: real ``` hoelzl@35582 ` 586` ``` { assume asm: "0 \ a" ``` hoelzl@35582 ` 587` ``` from asm have pp: "\ w. (pos_part f w \ a) = (f w \ a)" unfolding pos_part_def by auto ``` hoelzl@35582 ` 588` ``` have "{w | w. w \ space M \ f w \ a} \ sets M" ``` hoelzl@35582 ` 589` ``` unfolding pos_part_def using assms borel_measurable_le_iff by auto ``` hoelzl@35582 ` 590` ``` hence "{w . w \ space M \ pos_part f w \ a} \ sets M" using pp by auto } ``` hoelzl@35582 ` 591` ``` moreover have "a < 0 \ {w \ space M. pos_part f w \ a} \ sets M" ``` hoelzl@35582 ` 592` ``` unfolding pos_part_def using empty_sets by auto ``` hoelzl@35582 ` 593` ``` ultimately have "{w . w \ space M \ pos_part f w \ a} \ sets M" ``` hoelzl@35582 ` 594` ``` using le_less_linear by auto ``` hoelzl@35582 ` 595` ``` } hence pos: "pos_part f \ borel_measurable M" using borel_measurable_le_iff by auto ``` hoelzl@35582 ` 596` ``` { fix a :: real ``` hoelzl@35582 ` 597` ``` { assume asm: "0 \ a" ``` hoelzl@35582 ` 598` ``` from asm have pp: "\ w. (neg_part f w \ a) = (f w \ - a)" unfolding neg_part_def by auto ``` hoelzl@35582 ` 599` ``` have "{w | w. w \ space M \ f w \ - a} \ sets M" ``` hoelzl@35582 ` 600` ``` unfolding neg_part_def using assms borel_measurable_ge_iff by auto ``` hoelzl@35582 ` 601` ``` hence "{w . w \ space M \ neg_part f w \ a} \ sets M" using pp by auto } ``` hoelzl@35582 ` 602` ``` moreover have "a < 0 \ {w \ space M. neg_part f w \ a} = {}" unfolding neg_part_def by auto ``` hoelzl@35582 ` 603` ``` moreover hence "a < 0 \ {w \ space M. neg_part f w \ a} \ sets M" by (simp only: empty_sets) ``` hoelzl@35582 ` 604` ``` ultimately have "{w . w \ space M \ neg_part f w \ a} \ sets M" ``` hoelzl@35582 ` 605` ``` using le_less_linear by auto ``` hoelzl@35582 ` 606` ``` } hence neg: "neg_part f \ borel_measurable M" using borel_measurable_le_iff by auto ``` hoelzl@35582 ` 607` ``` from pos neg show "pos_part f \ borel_measurable M" and "neg_part f \ borel_measurable M" by auto ``` hoelzl@35582 ` 608` ```qed ``` hoelzl@35582 ` 609` hoelzl@35582 ` 610` ```lemma pos_part_neg_part_borel_measurable_iff: ``` hoelzl@35582 ` 611` ``` "f \ borel_measurable M \ ``` hoelzl@35582 ` 612` ``` pos_part f \ borel_measurable M \ neg_part f \ borel_measurable M" ``` hoelzl@35582 ` 613` ```proof - ``` hoelzl@35582 ` 614` ``` { fix x ``` hoelzl@35582 ` 615` ``` have "f x = pos_part f x - neg_part f x" ``` hoelzl@35582 ` 616` ``` unfolding pos_part_def neg_part_def unfolding max_def min_def ``` hoelzl@35582 ` 617` ``` by auto } ``` hoelzl@35582 ` 618` ``` hence "(\ x. f x) = (\ x. pos_part f x - neg_part f x)" by auto ``` hoelzl@35582 ` 619` ``` hence "f = (\ x. pos_part f x - neg_part f x)" by blast ``` hoelzl@35582 ` 620` ``` from pos_part_neg_part_borel_measurable[of f] ``` hoelzl@35582 ` 621` ``` borel_measurable_diff_borel_measurable[of "pos_part f" "neg_part f"] ``` hoelzl@35582 ` 622` ``` this ``` hoelzl@35582 ` 623` ``` show ?thesis by auto ``` hoelzl@35582 ` 624` ```qed ``` hoelzl@35582 ` 625` hoelzl@35582 ` 626` ```lemma borel_measurable_cong: ``` hoelzl@35582 ` 627` ``` assumes "\ w. w \ space M \ f w = g w" ``` hoelzl@35582 ` 628` ``` shows "f \ borel_measurable M \ g \ borel_measurable M" ``` hoelzl@35582 ` 629` ```using assms unfolding in_borel_measurable by (simp cong: vimage_inter_cong) ``` hoelzl@35582 ` 630` hoelzl@35582 ` 631` ```lemma psfis_borel_measurable: ``` hoelzl@35582 ` 632` ``` assumes "a \ psfis f" ``` hoelzl@35582 ` 633` ``` shows "f \ borel_measurable M" ``` hoelzl@35582 ` 634` ```using assms ``` hoelzl@35582 ` 635` ```proof - ``` hoelzl@35582 ` 636` ``` from assms obtain s a' x where sa'x: "(s, a', x) \ pos_simple f" and sa'xa: "pos_simple_integral (s, a', x) = a" ``` hoelzl@35582 ` 637` ``` and fs: "finite s" ``` hoelzl@35582 ` 638` ``` unfolding psfis_def pos_simple_integral_def image_def ``` hoelzl@35582 ` 639` ``` by (auto elim:pos_simpleE) ``` hoelzl@35582 ` 640` ``` { fix w assume "w \ space M" ``` hoelzl@35582 ` 641` ``` hence "(f w \ a) = ((\ i \ s. x i * indicator_fn (a' i) w) \ a)" ``` hoelzl@35582 ` 642` ``` using pos_simple_setsum_indicator_fn[OF sa'x, of w] by simp ``` hoelzl@35582 ` 643` ``` } hence "\ w. (w \ space M \ f w \ a) = (w \ space M \ (\ i \ s. x i * indicator_fn (a' i) w) \ a)" ``` hoelzl@35582 ` 644` ``` by auto ``` hoelzl@35582 ` 645` ``` { fix i assume "i \ s" ``` hoelzl@35582 ` 646` ``` hence "indicator_fn (a' i) \ borel_measurable M" ``` hoelzl@35582 ` 647` ``` using borel_measurable_indicator using sa'x[unfolded pos_simple_def] by auto ``` hoelzl@35582 ` 648` ``` hence "(\ w. x i * indicator_fn (a' i) w) \ borel_measurable M" ``` hoelzl@35582 ` 649` ``` using affine_borel_measurable[of "\ w. indicator_fn (a' i) w" 0 "x i"] ``` hoelzl@35582 ` 650` ``` real_mult_commute by auto } ``` hoelzl@35582 ` 651` ``` from borel_measurable_setsum_borel_measurable[OF fs this] affine_borel_measurable ``` hoelzl@35582 ` 652` ``` have "(\ w. (\ i \ s. x i * indicator_fn (a' i) w)) \ borel_measurable M" by auto ``` hoelzl@35582 ` 653` ``` from borel_measurable_cong[OF pos_simple_setsum_indicator_fn[OF sa'x]] this ``` hoelzl@35582 ` 654` ``` show ?thesis by simp ``` hoelzl@35582 ` 655` ```qed ``` hoelzl@35582 ` 656` hoelzl@35582 ` 657` ```lemma mono_conv_outgrow: ``` hoelzl@35582 ` 658` ``` assumes "incseq x" "x ----> y" "z < y" ``` hoelzl@35582 ` 659` ``` shows "\b. \ a \ b. z < x a" ``` hoelzl@35582 ` 660` ```using assms ``` hoelzl@35582 ` 661` ```proof - ``` hoelzl@35582 ` 662` ``` from assms have "y - z > 0" by simp ``` hoelzl@35582 ` 663` ``` hence A: "\n. (\ m \ n. \ x m + - y \ < y - z)" using assms ``` hoelzl@35582 ` 664` ``` unfolding incseq_def LIMSEQ_def dist_real_def real_diff_def ``` hoelzl@35582 ` 665` ``` by simp ``` hoelzl@35582 ` 666` ``` have "\m. x m \ y" using incseq_le assms by auto ``` hoelzl@35582 ` 667` ``` hence B: "\m. \ x m + - y \ = y - x m" ``` hoelzl@35582 ` 668` ``` by (metis abs_if abs_minus_add_cancel less_iff_diff_less_0 linorder_not_le real_diff_def) ``` hoelzl@35582 ` 669` ``` from A B show ?thesis by auto ``` hoelzl@35582 ` 670` ```qed ``` hoelzl@35582 ` 671` hoelzl@35582 ` 672` ```lemma psfis_mono_conv_mono: ``` hoelzl@35582 ` 673` ``` assumes mono: "mono_convergent u f (space M)" ``` hoelzl@35582 ` 674` ``` and ps_u: "\n. x n \ psfis (u n)" ``` hoelzl@35582 ` 675` ``` and "x ----> y" ``` hoelzl@35582 ` 676` ``` and "r \ psfis s" ``` hoelzl@35582 ` 677` ``` and f_upper_bound: "\t. t \ space M \ s t \ f t" ``` hoelzl@35582 ` 678` ``` shows "r <= y" ``` hoelzl@35582 ` 679` ```proof (rule field_le_mult_one_interval) ``` hoelzl@35582 ` 680` ``` fix z :: real assume "0 < z" and "z < 1" ``` hoelzl@35582 ` 681` ``` hence "0 \ z" by auto ``` hoelzl@35582 ` 682` ```(* def B' \ "\n. {w \ space M. z * s w <= u n w}" *) ``` hoelzl@35582 ` 683` ``` let "?B' n" = "{w \ space M. z * s w <= u n w}" ``` hoelzl@35582 ` 684` hoelzl@35582 ` 685` ``` have "incseq x" unfolding incseq_def ``` hoelzl@35582 ` 686` ``` proof safe ``` hoelzl@35582 ` 687` ``` fix m n :: nat assume "m \ n" ``` hoelzl@35582 ` 688` ``` show "x m \ x n" ``` hoelzl@35582 ` 689` ``` proof (rule psfis_mono[OF `x m \ psfis (u m)` `x n \ psfis (u n)`]) ``` hoelzl@35582 ` 690` ``` fix t assume "t \ space M" ``` hoelzl@35582 ` 691` ``` with mono_convergentD[OF mono this] `m \ n` show "u m t \ u n t" ``` hoelzl@35582 ` 692` ``` unfolding incseq_def by auto ``` hoelzl@35582 ` 693` ``` qed ``` hoelzl@35582 ` 694` ``` qed ``` hoelzl@35582 ` 695` hoelzl@35582 ` 696` ``` from `r \ psfis s` ``` hoelzl@35582 ` 697` ``` obtain s' a x' where r: "r = pos_simple_integral (s', a, x')" ``` hoelzl@35582 ` 698` ``` and ps_s: "(s', a, x') \ pos_simple s" ``` hoelzl@35582 ` 699` ``` unfolding psfis_def by auto ``` hoelzl@35582 ` 700` hoelzl@35582 ` 701` ``` { fix t i assume "i \ s'" "t \ a i" ``` hoelzl@35582 ` 702` ``` hence "t \ space M" using ps_s by (auto elim!: pos_simpleE) } ``` hoelzl@35582 ` 703` ``` note t_in_space = this ``` hoelzl@35582 ` 704` hoelzl@35582 ` 705` ``` { fix n ``` hoelzl@35582 ` 706` ``` from psfis_borel_measurable[OF `r \ psfis s`] ``` hoelzl@35582 ` 707` ``` psfis_borel_measurable[OF ps_u] ``` hoelzl@35582 ` 708` ``` have "?B' n \ sets M" ``` hoelzl@35582 ` 709` ``` by (auto intro!: ``` hoelzl@35582 ` 710` ``` borel_measurable_leq_borel_measurable ``` hoelzl@35582 ` 711` ``` borel_measurable_times_borel_measurable ``` hoelzl@35582 ` 712` ``` borel_measurable_const) } ``` hoelzl@35582 ` 713` ``` note B'_in_M = this ``` hoelzl@35582 ` 714` hoelzl@35582 ` 715` ``` { fix n have "(\i. a i \ ?B' n) ` s' \ sets M" using B'_in_M ps_s ``` hoelzl@35582 ` 716` ``` by (auto intro!: Int elim!: pos_simpleE) } ``` hoelzl@35582 ` 717` ``` note B'_inter_a_in_M = this ``` hoelzl@35582 ` 718` hoelzl@35582 ` 719` ``` let "?sum n" = "(\i\s'. x' i * measure M (a i \ ?B' n))" ``` hoelzl@35582 ` 720` ``` { fix n ``` hoelzl@35582 ` 721` ``` have "z * ?sum n \ x n" ``` hoelzl@35582 ` 722` ``` proof (rule psfis_mono[OF _ ps_u]) ``` hoelzl@35582 ` 723` ``` have *: "\i t. indicator_fn (?B' n) t * (x' i * indicator_fn (a i) t) = ``` hoelzl@35582 ` 724` ``` x' i * indicator_fn (a i \ ?B' n) t" unfolding indicator_fn_def by auto ``` hoelzl@35582 ` 725` ``` have ps': "?sum n \ psfis (\t. indicator_fn (?B' n) t * (\i\s'. x' i * indicator_fn (a i) t))" ``` hoelzl@35582 ` 726` ``` unfolding setsum_right_distrib * using B'_in_M ps_s ``` hoelzl@35582 ` 727` ``` by (auto intro!: psfis_intro Int elim!: pos_simpleE) ``` hoelzl@35582 ` 728` ``` also have "... = psfis (\t. indicator_fn (?B' n) t * s t)" (is "psfis ?l = psfis ?r") ``` hoelzl@35582 ` 729` ``` proof (rule psfis_cong) ``` hoelzl@35582 ` 730` ``` show "nonneg ?l" using psfis_nonneg[OF ps'] . ``` hoelzl@35582 ` 731` ``` show "nonneg ?r" using psfis_nonneg[OF `r \ psfis s`] unfolding nonneg_def indicator_fn_def by auto ``` hoelzl@35582 ` 732` ``` fix t assume "t \ space M" ``` hoelzl@35582 ` 733` ``` show "?l t = ?r t" unfolding pos_simple_setsum_indicator_fn[OF ps_s `t \ space M`] .. ``` hoelzl@35582 ` 734` ``` qed ``` hoelzl@35582 ` 735` ``` finally show "z * ?sum n \ psfis (\t. z * ?r t)" using psfis_mult[OF _ `0 \ z`] by simp ``` hoelzl@35582 ` 736` ``` next ``` hoelzl@35582 ` 737` ``` fix t assume "t \ space M" ``` hoelzl@35582 ` 738` ``` show "z * (indicator_fn (?B' n) t * s t) \ u n t" ``` hoelzl@35582 ` 739` ``` using psfis_nonneg[OF ps_u] unfolding nonneg_def indicator_fn_def by auto ``` hoelzl@35582 ` 740` ``` qed } ``` hoelzl@35582 ` 741` ``` hence *: "\N. \n\N. z * ?sum n \ x n" by (auto intro!: exI[of _ 0]) ``` hoelzl@35582 ` 742` hoelzl@35582 ` 743` ``` show "z * r \ y" unfolding r pos_simple_integral_def ``` hoelzl@35582 ` 744` ``` proof (rule LIMSEQ_le[OF mult_right.LIMSEQ `x ----> y` *], ``` hoelzl@35582 ` 745` ``` simp, rule LIMSEQ_setsum, rule mult_right.LIMSEQ) ``` hoelzl@35582 ` 746` ``` fix i assume "i \ s'" ``` hoelzl@35582 ` 747` ``` from psfis_nonneg[OF `r \ psfis s`, unfolded nonneg_def] ``` hoelzl@35582 ` 748` ``` have "\t. 0 \ s t" by simp ``` hoelzl@35582 ` 749` hoelzl@35582 ` 750` ``` have *: "(\j. a i \ ?B' j) = a i" ``` hoelzl@35582 ` 751` ``` proof (safe, simp, safe) ``` hoelzl@35582 ` 752` ``` fix t assume "t \ a i" ``` hoelzl@35582 ` 753` ``` thus "t \ space M" using t_in_space[OF `i \ s'`] by auto ``` hoelzl@35582 ` 754` ``` show "\j. z * s t \ u j t" ``` hoelzl@35582 ` 755` ``` proof (cases "s t = 0") ``` hoelzl@35582 ` 756` ``` case True thus ?thesis ``` hoelzl@35582 ` 757` ``` using psfis_nonneg[OF ps_u] unfolding nonneg_def by auto ``` hoelzl@35582 ` 758` ``` next ``` hoelzl@35582 ` 759` ``` case False with `0 \ s t` ``` hoelzl@35582 ` 760` ``` have "0 < s t" by auto ``` hoelzl@35582 ` 761` ``` hence "z * s t < 1 * s t" using `0 < z` `z < 1` ``` hoelzl@35582 ` 762` ``` by (auto intro!: mult_strict_right_mono simp del: mult_1_left) ``` hoelzl@35582 ` 763` ``` also have "... \ f t" using f_upper_bound `t \ space M` by auto ``` hoelzl@35582 ` 764` ``` finally obtain b where "\j. b \ j \ z * s t < u j t" using `t \ space M` ``` hoelzl@35582 ` 765` ``` using mono_conv_outgrow[of "\n. u n t" "f t" "z * s t"] ``` hoelzl@35582 ` 766` ``` using mono_convergentD[OF mono] by auto ``` hoelzl@35582 ` 767` ``` from this[of b] show ?thesis by (auto intro!: exI[of _ b]) ``` hoelzl@35582 ` 768` ``` qed ``` hoelzl@35582 ` 769` ``` qed ``` hoelzl@35582 ` 770` hoelzl@35582 ` 771` ``` show "(\n. measure M (a i \ ?B' n)) ----> measure M (a i)" ``` hoelzl@35582 ` 772` ``` proof (safe intro!: ``` hoelzl@35582 ` 773` ``` monotone_convergence[of "\n. a i \ ?B' n", unfolded comp_def *]) ``` hoelzl@35582 ` 774` ``` fix n show "a i \ ?B' n \ sets M" ``` hoelzl@35582 ` 775` ``` using B'_inter_a_in_M[of n] `i \ s'` by auto ``` hoelzl@35582 ` 776` ``` next ``` hoelzl@35582 ` 777` ``` fix j t assume "t \ space M" and "z * s t \ u j t" ``` hoelzl@35582 ` 778` ``` thus "z * s t \ u (Suc j) t" ``` hoelzl@35582 ` 779` ``` using mono_convergentD(1)[OF mono, unfolded incseq_def, ``` hoelzl@35582 ` 780` ``` rule_format, of t j "Suc j"] ``` hoelzl@35582 ` 781` ``` by auto ``` hoelzl@35582 ` 782` ``` qed ``` hoelzl@35582 ` 783` ``` qed ``` hoelzl@35582 ` 784` ```qed ``` hoelzl@35582 ` 785` hoelzl@35582 ` 786` ```lemma psfis_nnfis: ``` hoelzl@35582 ` 787` ``` "a \ psfis f \ a \ nnfis f" ``` hoelzl@35582 ` 788` ``` unfolding nnfis_def mono_convergent_def incseq_def ``` hoelzl@35582 ` 789` ``` by (auto intro!: exI[of _ "\n. f"] exI[of _ "\n. a"] LIMSEQ_const) ``` hoelzl@35582 ` 790` hoelzl@35582 ` 791` ```lemma nnfis_times: ``` hoelzl@35582 ` 792` ``` assumes "a \ nnfis f" and "0 \ z" ``` hoelzl@35582 ` 793` ``` shows "z * a \ nnfis (\t. z * f t)" ``` hoelzl@35582 ` 794` ```proof - ``` hoelzl@35582 ` 795` ``` obtain u x where "mono_convergent u f (space M)" and ``` hoelzl@35582 ` 796` ``` "\n. x n \ psfis (u n)" "x ----> a" ``` hoelzl@35582 ` 797` ``` using `a \ nnfis f` unfolding nnfis_def by auto ``` hoelzl@35582 ` 798` ``` with `0 \ z`show ?thesis unfolding nnfis_def mono_convergent_def incseq_def ``` hoelzl@35582 ` 799` ``` by (auto intro!: exI[of _ "\n w. z * u n w"] exI[of _ "\n. z * x n"] ``` hoelzl@35582 ` 800` ``` LIMSEQ_mult LIMSEQ_const psfis_mult mult_mono1) ``` hoelzl@35582 ` 801` ```qed ``` hoelzl@35582 ` 802` hoelzl@35582 ` 803` ```lemma nnfis_add: ``` hoelzl@35582 ` 804` ``` assumes "a \ nnfis f" and "b \ nnfis g" ``` hoelzl@35582 ` 805` ``` shows "a + b \ nnfis (\t. f t + g t)" ``` hoelzl@35582 ` 806` ```proof - ``` hoelzl@35582 ` 807` ``` obtain u x w y ``` hoelzl@35582 ` 808` ``` where "mono_convergent u f (space M)" and ``` hoelzl@35582 ` 809` ``` "\n. x n \ psfis (u n)" "x ----> a" and ``` hoelzl@35582 ` 810` ``` "mono_convergent w g (space M)" and ``` hoelzl@35582 ` 811` ``` "\n. y n \ psfis (w n)" "y ----> b" ``` hoelzl@35582 ` 812` ``` using `a \ nnfis f` `b \ nnfis g` unfolding nnfis_def by auto ``` hoelzl@35582 ` 813` ``` thus ?thesis unfolding nnfis_def mono_convergent_def incseq_def ``` hoelzl@35582 ` 814` ``` by (auto intro!: exI[of _ "\n a. u n a + w n a"] exI[of _ "\n. x n + y n"] ``` hoelzl@35582 ` 815` ``` LIMSEQ_add LIMSEQ_const psfis_add add_mono) ``` hoelzl@35582 ` 816` ```qed ``` hoelzl@35582 ` 817` hoelzl@35582 ` 818` ```lemma nnfis_mono: ``` hoelzl@35582 ` 819` ``` assumes nnfis: "a \ nnfis f" "b \ nnfis g" ``` hoelzl@35582 ` 820` ``` and mono: "\t. t \ space M \ f t \ g t" ``` hoelzl@35582 ` 821` ``` shows "a \ b" ``` hoelzl@35582 ` 822` ```proof - ``` hoelzl@35582 ` 823` ``` obtain u x w y where ``` hoelzl@35582 ` 824` ``` mc: "mono_convergent u f (space M)" "mono_convergent w g (space M)" and ``` hoelzl@35582 ` 825` ``` psfis: "\n. x n \ psfis (u n)" "\n. y n \ psfis (w n)" and ``` hoelzl@35582 ` 826` ``` limseq: "x ----> a" "y ----> b" using nnfis unfolding nnfis_def by auto ``` hoelzl@35582 ` 827` ``` show ?thesis ``` hoelzl@35582 ` 828` ``` proof (rule LIMSEQ_le_const2[OF limseq(1)], rule exI[of _ 0], safe) ``` hoelzl@35582 ` 829` ``` fix n ``` hoelzl@35582 ` 830` ``` show "x n \ b" ``` hoelzl@35582 ` 831` ``` proof (rule psfis_mono_conv_mono[OF mc(2) psfis(2) limseq(2) psfis(1)]) ``` hoelzl@35582 ` 832` ``` fix t assume "t \ space M" ``` hoelzl@35582 ` 833` ``` from mono_convergent_le[OF mc(1) this] mono[OF this] ``` hoelzl@35582 ` 834` ``` show "u n t \ g t" by (rule order_trans) ``` hoelzl@35582 ` 835` ``` qed ``` hoelzl@35582 ` 836` ``` qed ``` hoelzl@35582 ` 837` ```qed ``` hoelzl@35582 ` 838` hoelzl@35582 ` 839` ```lemma nnfis_unique: ``` hoelzl@35582 ` 840` ``` assumes a: "a \ nnfis f" and b: "b \ nnfis f" ``` hoelzl@35582 ` 841` ``` shows "a = b" ``` hoelzl@35582 ` 842` ``` using nnfis_mono[OF a b] nnfis_mono[OF b a] ``` hoelzl@35582 ` 843` ``` by (auto intro!: real_le_antisym[of a b]) ``` hoelzl@35582 ` 844` hoelzl@35582 ` 845` ```lemma psfis_equiv: ``` hoelzl@35582 ` 846` ``` assumes "a \ psfis f" and "nonneg g" ``` hoelzl@35582 ` 847` ``` and "\t. t \ space M \ f t = g t" ``` hoelzl@35582 ` 848` ``` shows "a \ psfis g" ``` hoelzl@35582 ` 849` ``` using assms unfolding psfis_def pos_simple_def by auto ``` hoelzl@35582 ` 850` hoelzl@35582 ` 851` ```lemma psfis_mon_upclose: ``` hoelzl@35582 ` 852` ``` assumes "\m. a m \ psfis (u m)" ``` hoelzl@35582 ` 853` ``` shows "\c. c \ psfis (mon_upclose n u)" ``` hoelzl@35582 ` 854` ```proof (induct n) ``` hoelzl@35582 ` 855` ``` case 0 thus ?case unfolding mon_upclose.simps using assms .. ``` hoelzl@35582 ` 856` ```next ``` hoelzl@35582 ` 857` ``` case (Suc n) ``` hoelzl@35582 ` 858` ``` then obtain sn an xn where ps: "(sn, an, xn) \ pos_simple (mon_upclose n u)" ``` hoelzl@35582 ` 859` ``` unfolding psfis_def by auto ``` hoelzl@35582 ` 860` ``` obtain ss as xs where ps': "(ss, as, xs) \ pos_simple (u (Suc n))" ``` hoelzl@35582 ` 861` ``` using assms[of "Suc n"] unfolding psfis_def by auto ``` hoelzl@35582 ` 862` ``` from pos_simple_common_partition[OF ps ps'] guess x x' a s . ``` hoelzl@35582 ` 863` ``` hence "(s, a, upclose x x') \ pos_simple (mon_upclose (Suc n) u)" ``` hoelzl@35582 ` 864` ``` by (simp add: upclose_def pos_simple_def nonneg_def max_def) ``` hoelzl@35582 ` 865` ``` thus ?case unfolding psfis_def by auto ``` hoelzl@35582 ` 866` ```qed ``` hoelzl@35582 ` 867` hoelzl@35582 ` 868` ```text {* Beppo-Levi monotone convergence theorem *} ``` hoelzl@35582 ` 869` ```lemma nnfis_mon_conv: ``` hoelzl@35582 ` 870` ``` assumes mc: "mono_convergent f h (space M)" ``` hoelzl@35582 ` 871` ``` and nnfis: "\n. x n \ nnfis (f n)" ``` hoelzl@35582 ` 872` ``` and "x ----> z" ``` hoelzl@35582 ` 873` ``` shows "z \ nnfis h" ``` hoelzl@35582 ` 874` ```proof - ``` hoelzl@35582 ` 875` ``` have "\n. \u y. mono_convergent u (f n) (space M) \ (\m. y m \ psfis (u m)) \ ``` hoelzl@35582 ` 876` ``` y ----> x n" ``` hoelzl@35582 ` 877` ``` using nnfis unfolding nnfis_def by auto ``` hoelzl@35582 ` 878` ``` from choice[OF this] guess u .. ``` hoelzl@35582 ` 879` ``` from choice[OF this] guess y .. ``` hoelzl@35582 ` 880` ``` hence mc_u: "\n. mono_convergent (u n) (f n) (space M)" ``` hoelzl@35582 ` 881` ``` and psfis: "\n m. y n m \ psfis (u n m)" and "\n. y n ----> x n" ``` hoelzl@35582 ` 882` ``` by auto ``` hoelzl@35582 ` 883` hoelzl@35582 ` 884` ``` let "?upclose n" = "mon_upclose n (\m. u m n)" ``` hoelzl@35582 ` 885` hoelzl@35582 ` 886` ``` have "\c. \n. c n \ psfis (?upclose n)" ``` hoelzl@35582 ` 887` ``` by (safe intro!: choice psfis_mon_upclose) (rule psfis) ``` hoelzl@35582 ` 888` ``` then guess c .. note c = this[rule_format] ``` hoelzl@35582 ` 889` hoelzl@35582 ` 890` ``` show ?thesis unfolding nnfis_def ``` hoelzl@35582 ` 891` ``` proof (safe intro!: exI) ``` hoelzl@35582 ` 892` ``` show mc_upclose: "mono_convergent ?upclose h (space M)" ``` hoelzl@35582 ` 893` ``` by (rule mon_upclose_mono_convergent[OF mc_u mc]) ``` hoelzl@35582 ` 894` ``` show psfis_upclose: "\n. c n \ psfis (?upclose n)" ``` hoelzl@35582 ` 895` ``` using c . ``` hoelzl@35582 ` 896` hoelzl@35582 ` 897` ``` { fix n m :: nat assume "n \ m" ``` hoelzl@35582 ` 898` ``` hence "c n \ c m" ``` hoelzl@35582 ` 899` ``` using psfis_mono[OF c c] ``` hoelzl@35582 ` 900` ``` using mono_convergentD(1)[OF mc_upclose, unfolded incseq_def] ``` hoelzl@35582 ` 901` ``` by auto } ``` hoelzl@35582 ` 902` ``` hence "incseq c" unfolding incseq_def by auto ``` hoelzl@35582 ` 903` hoelzl@35582 ` 904` ``` { fix n ``` hoelzl@35582 ` 905` ``` have c_nnfis: "c n \ nnfis (?upclose n)" using c by (rule psfis_nnfis) ``` hoelzl@35582 ` 906` ``` from nnfis_mono[OF c_nnfis nnfis] ``` hoelzl@35582 ` 907` ``` mon_upclose_le_mono_convergent[OF mc_u] ``` hoelzl@35582 ` 908` ``` mono_convergentD(1)[OF mc] ``` hoelzl@35582 ` 909` ``` have "c n \ x n" by fast } ``` hoelzl@35582 ` 910` ``` note c_less_x = this ``` hoelzl@35582 ` 911` hoelzl@35582 ` 912` ``` { fix n ``` hoelzl@35582 ` 913` ``` note c_less_x[of n] ``` hoelzl@35582 ` 914` ``` also have "x n \ z" ``` hoelzl@35582 ` 915` ``` proof (rule incseq_le) ``` hoelzl@35582 ` 916` ``` show "x ----> z" by fact ``` hoelzl@35582 ` 917` ``` from mono_convergentD(1)[OF mc] ``` hoelzl@35582 ` 918` ``` show "incseq x" unfolding incseq_def ``` hoelzl@35582 ` 919` ``` by (auto intro!: nnfis_mono[OF nnfis nnfis]) ``` hoelzl@35582 ` 920` ``` qed ``` hoelzl@35582 ` 921` ``` finally have "c n \ z" . } ``` hoelzl@35582 ` 922` ``` note c_less_z = this ``` hoelzl@35582 ` 923` hoelzl@35582 ` 924` ``` have "convergent c" ``` hoelzl@35582 ` 925` ``` proof (rule Bseq_mono_convergent[unfolded incseq_def[symmetric]]) ``` hoelzl@35582 ` 926` ``` show "Bseq c" ``` hoelzl@35582 ` 927` ``` using pos_psfis[OF c] c_less_z ``` hoelzl@35582 ` 928` ``` by (auto intro!: BseqI'[of _ z]) ``` hoelzl@35582 ` 929` ``` show "incseq c" by fact ``` hoelzl@35582 ` 930` ``` qed ``` hoelzl@35582 ` 931` ``` then obtain l where l: "c ----> l" unfolding convergent_def by auto ``` hoelzl@35582 ` 932` hoelzl@35582 ` 933` ``` have "l \ z" using c_less_x l ``` hoelzl@35582 ` 934` ``` by (auto intro!: LIMSEQ_le[OF _ `x ----> z`]) ``` hoelzl@35582 ` 935` ``` moreover have "z \ l" ``` hoelzl@35582 ` 936` ``` proof (rule LIMSEQ_le_const2[OF `x ----> z`], safe intro!: exI[of _ 0]) ``` hoelzl@35582 ` 937` ``` fix n ``` hoelzl@35582 ` 938` ``` have "l \ nnfis h" ``` hoelzl@35582 ` 939` ``` unfolding nnfis_def using l mc_upclose psfis_upclose by auto ``` hoelzl@35582 ` 940` ``` from nnfis this mono_convergent_le[OF mc] ``` hoelzl@35582 ` 941` ``` show "x n \ l" by (rule nnfis_mono) ``` hoelzl@35582 ` 942` ``` qed ``` hoelzl@35582 ` 943` ``` ultimately have "l = z" by (rule real_le_antisym) ``` hoelzl@35582 ` 944` ``` thus "c ----> z" using `c ----> l` by simp ``` hoelzl@35582 ` 945` ``` qed ``` hoelzl@35582 ` 946` ```qed ``` hoelzl@35582 ` 947` hoelzl@35582 ` 948` ```lemma nnfis_pos_on_mspace: ``` hoelzl@35582 ` 949` ``` assumes "a \ nnfis f" and "x \space M" ``` hoelzl@35582 ` 950` ``` shows "0 \ f x" ``` hoelzl@35582 ` 951` ```using assms ``` hoelzl@35582 ` 952` ```proof - ``` hoelzl@35582 ` 953` ``` from assms[unfolded nnfis_def] guess u y by auto note uy = this ``` hoelzl@35582 ` 954` ``` hence "\ n. 0 \ u n x" ``` hoelzl@35582 ` 955` ``` unfolding nnfis_def psfis_def pos_simple_def nonneg_def mono_convergent_def ``` hoelzl@35582 ` 956` ``` by auto ``` hoelzl@35582 ` 957` ``` thus "0 \ f x" using uy[rule_format] ``` hoelzl@35582 ` 958` ``` unfolding nnfis_def psfis_def pos_simple_def nonneg_def mono_convergent_def ``` hoelzl@35582 ` 959` ``` using incseq_le[of "\ n. u n x" "f x"] real_le_trans ``` hoelzl@35582 ` 960` ``` by fast ``` hoelzl@35582 ` 961` ```qed ``` hoelzl@35582 ` 962` hoelzl@35582 ` 963` ```lemma nnfis_borel_measurable: ``` hoelzl@35582 ` 964` ``` assumes "a \ nnfis f" ``` hoelzl@35582 ` 965` ``` shows "f \ borel_measurable M" ``` hoelzl@35582 ` 966` ```using assms unfolding nnfis_def ``` hoelzl@35582 ` 967` ```apply auto ``` hoelzl@35582 ` 968` ```apply (rule mono_convergent_borel_measurable) ``` hoelzl@35582 ` 969` ```using psfis_borel_measurable ``` hoelzl@35582 ` 970` ```by auto ``` hoelzl@35582 ` 971` hoelzl@35582 ` 972` ```lemma borel_measurable_mon_conv_psfis: ``` hoelzl@35582 ` 973` ``` assumes f_borel: "f \ borel_measurable M" ``` hoelzl@35582 ` 974` ``` and nonneg: "\t. t \ space M \ 0 \ f t" ``` hoelzl@35582 ` 975` ``` shows"\u x. mono_convergent u f (space M) \ (\n. x n \ psfis (u n))" ``` hoelzl@35582 ` 976` ```proof (safe intro!: exI) ``` hoelzl@35582 ` 977` ``` let "?I n" = "{0<.. space M" ``` hoelzl@35582 ` 985` ``` have "?u n t = ?w n t" (is "_ = (if _ then real ?i / _ else _)") ``` hoelzl@35582 ` 986` ``` proof (cases "f t < real n") ``` hoelzl@35582 ` 987` ``` case True ``` hoelzl@35582 ` 988` ``` with nonneg t ``` hoelzl@35582 ` 989` ``` have i: "?i < n * 2^n" ``` hoelzl@35582 ` 990` ``` by (auto simp: real_of_nat_power[symmetric] ``` hoelzl@35582 ` 991` ``` intro!: less_natfloor mult_nonneg_nonneg) ``` hoelzl@35582 ` 992` hoelzl@35582 ` 993` ``` hence t_in_A: "t \ ?A n ?i" ``` hoelzl@35582 ` 994` ``` unfolding divide_le_eq less_divide_eq ``` hoelzl@35582 ` 995` ``` using nonneg t True ``` hoelzl@35582 ` 996` ``` by (auto intro!: real_natfloor_le ``` hoelzl@35582 ` 997` ``` real_natfloor_gt_diff_one[unfolded diff_less_eq] ``` hoelzl@35582 ` 998` ``` simp: real_of_nat_Suc zero_le_mult_iff) ``` hoelzl@35582 ` 999` hoelzl@35582 ` 1000` ``` hence *: "real ?i / 2^n \ f t" ``` hoelzl@35582 ` 1001` ``` "f t < real (?i + 1) / 2^n" by auto ``` hoelzl@35582 ` 1002` ``` { fix j assume "t \ ?A n j" ``` hoelzl@35582 ` 1003` ``` hence "real j / 2^n \ f t" ``` hoelzl@35582 ` 1004` ``` and "f t < real (j + 1) / 2^n" by auto ``` hoelzl@35582 ` 1005` ``` with * have "j \ {?i}" unfolding divide_le_eq less_divide_eq ``` hoelzl@35582 ` 1006` ``` by auto } ``` hoelzl@35582 ` 1007` ``` hence *: "\j. t \ ?A n j \ j \ {?i}" using t_in_A by auto ``` hoelzl@35582 ` 1008` hoelzl@35582 ` 1009` ``` have "?u n t = real ?i / 2^n" ``` hoelzl@35582 ` 1010` ``` unfolding indicator_fn_def if_distrib * ``` hoelzl@35582 ` 1011` ``` setsum_cases[OF finite_greaterThanLessThan] ``` hoelzl@35582 ` 1012` ``` using i by (cases "?i = 0") simp_all ``` hoelzl@35582 ` 1013` ``` thus ?thesis using True by auto ``` hoelzl@35582 ` 1014` ``` next ``` hoelzl@35582 ` 1015` ``` case False ``` hoelzl@35582 ` 1016` ``` have "?u n t = (\i \ {0 <..< n*2^n}. 0)" ``` hoelzl@35582 ` 1017` ``` proof (rule setsum_cong) ``` hoelzl@35582 ` 1018` ``` fix i assume "i \ {0 <..< n*2^n}" ``` hoelzl@35582 ` 1019` ``` hence "i + 1 \ n * 2^n" by simp ``` hoelzl@35582 ` 1020` ``` hence "real (i + 1) \ real n * 2^n" ``` hoelzl@35582 ` 1021` ``` unfolding real_of_nat_le_iff[symmetric] ``` hoelzl@35582 ` 1022` ``` by (auto simp: real_of_nat_power[symmetric]) ``` hoelzl@35582 ` 1023` ``` also have "... \ f t * 2^n" ``` hoelzl@35582 ` 1024` ``` using False by (auto intro!: mult_nonneg_nonneg) ``` hoelzl@35582 ` 1025` ``` finally have "t \ ?A n i" ``` hoelzl@35582 ` 1026` ``` by (auto simp: divide_le_eq less_divide_eq) ``` hoelzl@35582 ` 1027` ``` thus "real i / 2^n * indicator_fn (?A n i) t = 0" ``` hoelzl@35582 ` 1028` ``` unfolding indicator_fn_def by auto ``` hoelzl@35582 ` 1029` ``` qed simp ``` hoelzl@35582 ` 1030` ``` thus ?thesis using False by auto ``` hoelzl@35582 ` 1031` ``` qed } ``` hoelzl@35582 ` 1032` ``` note u_at_t = this ``` hoelzl@35582 ` 1033` hoelzl@35582 ` 1034` ``` show "mono_convergent ?u f (space M)" unfolding mono_convergent_def ``` hoelzl@35582 ` 1035` ``` proof safe ``` hoelzl@35582 ` 1036` ``` fix t assume t: "t \ space M" ``` hoelzl@35582 ` 1037` ``` { fix m n :: nat assume "m \ n" ``` hoelzl@35582 ` 1038` ``` hence *: "(2::real)^n = 2^m * 2^(n - m)" unfolding class_semiring.mul_pwr by auto ``` hoelzl@35582 ` 1039` ``` have "real (natfloor (f t * 2^m) * natfloor (2^(n-m))) \ real (natfloor (f t * 2 ^ n))" ``` hoelzl@35582 ` 1040` ``` apply (subst *) ``` hoelzl@35582 ` 1041` ``` apply (subst class_semiring.mul_a) ``` hoelzl@35582 ` 1042` ``` apply (subst real_of_nat_le_iff) ``` hoelzl@35582 ` 1043` ``` apply (rule le_mult_natfloor) ``` hoelzl@35582 ` 1044` ``` using nonneg[OF t] by (auto intro!: mult_nonneg_nonneg) ``` hoelzl@35582 ` 1045` ``` hence "real (natfloor (f t * 2^m)) * 2^n \ real (natfloor (f t * 2^n)) * 2^m" ``` hoelzl@35582 ` 1046` ``` apply (subst *) ``` hoelzl@35582 ` 1047` ``` apply (subst (3) class_semiring.mul_c) ``` hoelzl@35582 ` 1048` ``` apply (subst class_semiring.mul_a) ``` hoelzl@35582 ` 1049` ``` by (auto intro: mult_right_mono simp: natfloor_power real_of_nat_power[symmetric]) } ``` hoelzl@35582 ` 1050` ``` thus "incseq (\n. ?u n t)" unfolding u_at_t[OF t] unfolding incseq_def ``` hoelzl@35582 ` 1051` ``` by (auto simp add: le_divide_eq divide_le_eq less_divide_eq) ``` hoelzl@35582 ` 1052` hoelzl@35582 ` 1053` ``` show "(\i. ?u i t) ----> f t" unfolding u_at_t[OF t] ``` hoelzl@35582 ` 1054` ``` proof (rule LIMSEQ_I, safe intro!: exI) ``` hoelzl@35582 ` 1055` ``` fix r :: real and n :: nat ``` hoelzl@35582 ` 1056` ``` let ?N = "natfloor (1/r) + 1" ``` hoelzl@35582 ` 1057` ``` assume "0 < r" and N: "max ?N (natfloor (f t) + 1) \ n" ``` hoelzl@35582 ` 1058` ``` hence "?N \ n" by auto ``` hoelzl@35582 ` 1059` hoelzl@35582 ` 1060` ``` have "1 / r < real (natfloor (1/r) + 1)" using real_natfloor_add_one_gt ``` hoelzl@35582 ` 1061` ``` by (simp add: real_of_nat_Suc) ``` hoelzl@35582 ` 1062` ``` also have "... < 2^?N" by (rule two_realpow_gt) ``` hoelzl@35582 ` 1063` ``` finally have less_r: "1 / 2^?N < r" using `0 < r` ``` hoelzl@35582 ` 1064` ``` by (auto simp: less_divide_eq divide_less_eq algebra_simps) ``` hoelzl@35582 ` 1065` hoelzl@35582 ` 1066` ``` have "f t < real (natfloor (f t) + 1)" using real_natfloor_add_one_gt[of "f t"] by auto ``` hoelzl@35582 ` 1067` ``` also have "... \ real n" unfolding real_of_nat_le_iff using N by auto ``` hoelzl@35582 ` 1068` ``` finally have "f t < real n" . ``` hoelzl@35582 ` 1069` hoelzl@35582 ` 1070` ``` have "real (natfloor (f t * 2^n)) \ f t * 2^n" ``` hoelzl@35582 ` 1071` ``` using nonneg[OF t] by (auto intro!: real_natfloor_le mult_nonneg_nonneg) ``` hoelzl@35582 ` 1072` ``` hence less: "real (natfloor (f t * 2^n)) / 2^n \ f t" unfolding divide_le_eq by auto ``` hoelzl@35582 ` 1073` hoelzl@35582 ` 1074` ``` have "f t * 2 ^ n - 1 < real (natfloor (f t * 2^n))" using real_natfloor_gt_diff_one . ``` hoelzl@35582 ` 1075` ``` hence "f t - real (natfloor (f t * 2^n)) / 2^n < 1 / 2^n" ``` hoelzl@35582 ` 1076` ``` by (auto simp: less_divide_eq divide_less_eq algebra_simps) ``` hoelzl@35582 ` 1077` ``` also have "... \ 1 / 2^?N" using `?N \ n` ``` hoelzl@35582 ` 1078` ``` by (auto intro!: divide_left_mono mult_pos_pos simp del: power_Suc) ``` hoelzl@35582 ` 1079` ``` also have "... < r" using less_r . ``` hoelzl@35582 ` 1080` ``` finally show "norm (?w n t - f t) < r" using `f t < real n` less by auto ``` hoelzl@35582 ` 1081` ``` qed ``` hoelzl@35582 ` 1082` ``` qed ``` hoelzl@35582 ` 1083` hoelzl@35582 ` 1084` ``` fix n ``` hoelzl@35582 ` 1085` ``` show "?x n \ psfis (?u n)" ``` hoelzl@35582 ` 1086` ``` proof (rule psfis_intro) ``` hoelzl@35582 ` 1087` ``` show "?A n ` ?I n \ sets M" ``` hoelzl@35582 ` 1088` ``` proof safe ``` hoelzl@35582 ` 1089` ``` fix i :: nat ``` hoelzl@35582 ` 1090` ``` from Int[OF ``` hoelzl@35582 ` 1091` ``` f_borel[unfolded borel_measurable_less_iff, rule_format, of "real (i+1) / 2^n"] ``` hoelzl@35582 ` 1092` ``` f_borel[unfolded borel_measurable_ge_iff, rule_format, of "real i / 2^n"]] ``` hoelzl@35582 ` 1093` ``` show "?A n i \ sets M" ``` hoelzl@35582 ` 1094` ``` by (metis Collect_conj_eq Int_commute Int_left_absorb Int_left_commute) ``` hoelzl@35582 ` 1095` ``` qed ``` hoelzl@35582 ` 1096` ``` show "nonneg (\i :: nat. real i / 2 ^ n)" ``` hoelzl@35582 ` 1097` ``` unfolding nonneg_def by (auto intro!: divide_nonneg_pos) ``` hoelzl@35582 ` 1098` ``` qed auto ``` hoelzl@35582 ` 1099` ```qed ``` hoelzl@35582 ` 1100` hoelzl@35582 ` 1101` ```lemma nnfis_dom_conv: ``` hoelzl@35582 ` 1102` ``` assumes borel: "f \ borel_measurable M" ``` hoelzl@35582 ` 1103` ``` and nnfis: "b \ nnfis g" ``` hoelzl@35582 ` 1104` ``` and ord: "\t. t \ space M \ f t \ g t" ``` hoelzl@35582 ` 1105` ``` and nonneg: "\t. t \ space M \ 0 \ f t" ``` hoelzl@35582 ` 1106` ``` shows "\a. a \ nnfis f \ a \ b" ``` hoelzl@35582 ` 1107` ```proof - ``` hoelzl@35582 ` 1108` ``` obtain u x where mc_f: "mono_convergent u f (space M)" and ``` hoelzl@35582 ` 1109` ``` psfis: "\n. x n \ psfis (u n)" ``` hoelzl@35582 ` 1110` ``` using borel_measurable_mon_conv_psfis[OF borel nonneg] by auto ``` hoelzl@35582 ` 1111` hoelzl@35582 ` 1112` ``` { fix n ``` hoelzl@35582 ` 1113` ``` { fix t assume t: "t \ space M" ``` hoelzl@35582 ` 1114` ``` note mono_convergent_le[OF mc_f this, of n] ``` hoelzl@35582 ` 1115` ``` also note ord[OF t] ``` hoelzl@35582 ` 1116` ``` finally have "u n t \ g t" . } ``` hoelzl@35582 ` 1117` ``` from nnfis_mono[OF psfis_nnfis[OF psfis] nnfis this] ``` hoelzl@35582 ` 1118` ``` have "x n \ b" by simp } ``` hoelzl@35582 ` 1119` ``` note x_less_b = this ``` hoelzl@35582 ` 1120` hoelzl@35582 ` 1121` ``` have "convergent x" ``` hoelzl@35582 ` 1122` ``` proof (safe intro!: Bseq_mono_convergent) ``` hoelzl@35582 ` 1123` ``` from x_less_b pos_psfis[OF psfis] ``` hoelzl@35582 ` 1124` ``` show "Bseq x" by (auto intro!: BseqI'[of _ b]) ``` hoelzl@35582 ` 1125` hoelzl@35582 ` 1126` ``` fix n m :: nat assume *: "n \ m" ``` hoelzl@35582 ` 1127` ``` show "x n \ x m" ``` hoelzl@35582 ` 1128` ``` proof (rule psfis_mono[OF `x n \ psfis (u n)` `x m \ psfis (u m)`]) ``` hoelzl@35582 ` 1129` ``` fix t assume "t \ space M" ``` hoelzl@35582 ` 1130` ``` from mc_f[THEN mono_convergentD(1), unfolded incseq_def, OF this] ``` hoelzl@35582 ` 1131` ``` show "u n t \ u m t" using * by auto ``` hoelzl@35582 ` 1132` ``` qed ``` hoelzl@35582 ` 1133` ``` qed ``` hoelzl@35582 ` 1134` ``` then obtain a where "x ----> a" unfolding convergent_def by auto ``` hoelzl@35582 ` 1135` ``` with LIMSEQ_le_const2[OF `x ----> a`] x_less_b mc_f psfis ``` hoelzl@35582 ` 1136` ``` show ?thesis unfolding nnfis_def by auto ``` hoelzl@35582 ` 1137` ```qed ``` hoelzl@35582 ` 1138` hoelzl@35582 ` 1139` ```lemma psfis_0: "0 \ psfis (\x. 0)" ``` hoelzl@35582 ` 1140` ``` unfolding psfis_def pos_simple_def pos_simple_integral_def ``` hoelzl@35582 ` 1141` ``` by (auto simp: nonneg_def ``` hoelzl@35582 ` 1142` ``` intro: image_eqI[where x="({0}, (\i. space M), (\i. 0))"]) ``` hoelzl@35582 ` 1143` hoelzl@35582 ` 1144` ```lemma the_nnfis[simp]: "a \ nnfis f \ (THE a. a \ nnfis f) = a" ``` hoelzl@35582 ` 1145` ``` by (auto intro: the_equality nnfis_unique) ``` hoelzl@35582 ` 1146` hoelzl@35582 ` 1147` ```lemma nnfis_cong: ``` hoelzl@35582 ` 1148` ``` assumes cong: "\x. x \ space M \ f x = g x" ``` hoelzl@35582 ` 1149` ``` shows "nnfis f = nnfis g" ``` hoelzl@35582 ` 1150` ```proof - ``` hoelzl@35582 ` 1151` ``` { fix f g :: "'a \ real" assume cong: "\x. x \ space M \ f x = g x" ``` hoelzl@35582 ` 1152` ``` fix x assume "x \ nnfis f" ``` hoelzl@35582 ` 1153` ``` then guess u y unfolding nnfis_def by safe note x = this ``` hoelzl@35582 ` 1154` ``` hence "mono_convergent u g (space M)" ``` hoelzl@35582 ` 1155` ``` unfolding mono_convergent_def using cong by auto ``` hoelzl@35582 ` 1156` ``` with x(2,3) have "x \ nnfis g" unfolding nnfis_def by auto } ``` hoelzl@35582 ` 1157` ``` from this[OF cong] this[OF cong[symmetric]] ``` hoelzl@35582 ` 1158` ``` show ?thesis by safe ``` hoelzl@35582 ` 1159` ```qed ``` hoelzl@35582 ` 1160` hoelzl@35582 ` 1161` ```lemma integral_cong: ``` hoelzl@35582 ` 1162` ``` assumes cong: "\x. x \ space M \ f x = g x" ``` hoelzl@35582 ` 1163` ``` shows "integral f = integral g" ``` hoelzl@35582 ` 1164` ```proof - ``` hoelzl@35582 ` 1165` ``` have "nnfis (pos_part f) = nnfis (pos_part g)" ``` hoelzl@35582 ` 1166` ``` using cong by (auto simp: pos_part_def intro!: nnfis_cong) ``` hoelzl@35582 ` 1167` ``` moreover ``` hoelzl@35582 ` 1168` ``` have "nnfis (neg_part f) = nnfis (neg_part g)" ``` hoelzl@35582 ` 1169` ``` using cong by (auto simp: neg_part_def intro!: nnfis_cong) ``` hoelzl@35582 ` 1170` ``` ultimately show ?thesis ``` hoelzl@35582 ` 1171` ``` unfolding integral_def by auto ``` hoelzl@35582 ` 1172` ```qed ``` hoelzl@35582 ` 1173` hoelzl@35582 ` 1174` ```lemma nnfis_integral: ``` hoelzl@35582 ` 1175` ``` assumes "a \ nnfis f" ``` hoelzl@35582 ` 1176` ``` shows "integrable f" and "integral f = a" ``` hoelzl@35582 ` 1177` ```proof - ``` hoelzl@35582 ` 1178` ``` have a: "a \ nnfis (pos_part f)" ``` hoelzl@35582 ` 1179` ``` using assms nnfis_pos_on_mspace[OF assms] ``` hoelzl@35582 ` 1180` ``` by (auto intro!: nnfis_mon_conv[of "\i. f" _ "\i. a"] ``` hoelzl@35582 ` 1181` ``` LIMSEQ_const simp: mono_convergent_def pos_part_def incseq_def max_def) ``` hoelzl@35582 ` 1182` hoelzl@35582 ` 1183` ``` have "\t. t \ space M \ neg_part f t = 0" ``` hoelzl@35582 ` 1184` ``` unfolding neg_part_def min_def ``` hoelzl@35582 ` 1185` ``` using nnfis_pos_on_mspace[OF assms] by auto ``` hoelzl@35582 ` 1186` ``` hence 0: "0 \ nnfis (neg_part f)" ``` hoelzl@35582 ` 1187` ``` by (auto simp: nnfis_def mono_convergent_def psfis_0 incseq_def ``` hoelzl@35582 ` 1188` ``` intro!: LIMSEQ_const exI[of _ "\ x n. 0"] exI[of _ "\ n. 0"]) ``` hoelzl@35582 ` 1189` hoelzl@35582 ` 1190` ``` from 0 a show "integrable f" "integral f = a" ``` hoelzl@35582 ` 1191` ``` unfolding integrable_def integral_def by auto ``` hoelzl@35582 ` 1192` ```qed ``` hoelzl@35582 ` 1193` hoelzl@35582 ` 1194` ```lemma nnfis_minus_nnfis_integral: ``` hoelzl@35582 ` 1195` ``` assumes "a \ nnfis f" and "b \ nnfis g" ``` hoelzl@35582 ` 1196` ``` shows "integrable (\t. f t - g t)" and "integral (\t. f t - g t) = a - b" ``` hoelzl@35582 ` 1197` ```proof - ``` hoelzl@35582 ` 1198` ``` have borel: "(\t. f t - g t) \ borel_measurable M" using assms ``` hoelzl@35582 ` 1199` ``` by (blast intro: ``` hoelzl@35582 ` 1200` ``` borel_measurable_diff_borel_measurable nnfis_borel_measurable) ``` hoelzl@35582 ` 1201` hoelzl@35582 ` 1202` ``` have "\x. x \ nnfis (pos_part (\t. f t - g t)) \ x \ a + b" ``` hoelzl@35582 ` 1203` ``` (is "\x. x \ nnfis ?pp \ _") ``` hoelzl@35582 ` 1204` ``` proof (rule nnfis_dom_conv) ``` hoelzl@35582 ` 1205` ``` show "?pp \ borel_measurable M" ``` hoelzl@35582 ` 1206` ``` using borel by (rule pos_part_neg_part_borel_measurable) ``` hoelzl@35582 ` 1207` ``` show "a + b \ nnfis (\t. f t + g t)" using assms by (rule nnfis_add) ``` hoelzl@35582 ` 1208` ``` fix t assume "t \ space M" ``` hoelzl@35582 ` 1209` ``` with assms nnfis_add assms[THEN nnfis_pos_on_mspace[OF _ this]] ``` hoelzl@35582 ` 1210` ``` show "?pp t \ f t + g t" unfolding pos_part_def by auto ``` hoelzl@35582 ` 1211` ``` show "0 \ ?pp t" using nonneg_pos_part[of "\t. f t - g t"] ``` hoelzl@35582 ` 1212` ``` unfolding nonneg_def by auto ``` hoelzl@35582 ` 1213` ``` qed ``` hoelzl@35582 ` 1214` ``` then obtain x where x: "x \ nnfis ?pp" by auto ``` hoelzl@35582 ` 1215` ``` moreover ``` hoelzl@35582 ` 1216` ``` have "\x. x \ nnfis (neg_part (\t. f t - g t)) \ x \ a + b" ``` hoelzl@35582 ` 1217` ``` (is "\x. x \ nnfis ?np \ _") ``` hoelzl@35582 ` 1218` ``` proof (rule nnfis_dom_conv) ``` hoelzl@35582 ` 1219` ``` show "?np \ borel_measurable M" ``` hoelzl@35582 ` 1220` ``` using borel by (rule pos_part_neg_part_borel_measurable) ``` hoelzl@35582 ` 1221` ``` show "a + b \ nnfis (\t. f t + g t)" using assms by (rule nnfis_add) ``` hoelzl@35582 ` 1222` ``` fix t assume "t \ space M" ``` hoelzl@35582 ` 1223` ``` with assms nnfis_add assms[THEN nnfis_pos_on_mspace[OF _ this]] ``` hoelzl@35582 ` 1224` ``` show "?np t \ f t + g t" unfolding neg_part_def by auto ``` hoelzl@35582 ` 1225` ``` show "0 \ ?np t" using nonneg_neg_part[of "\t. f t - g t"] ``` hoelzl@35582 ` 1226` ``` unfolding nonneg_def by auto ``` hoelzl@35582 ` 1227` ``` qed ``` hoelzl@35582 ` 1228` ``` then obtain y where y: "y \ nnfis ?np" by auto ``` hoelzl@35582 ` 1229` ``` ultimately show "integrable (\t. f t - g t)" ``` hoelzl@35582 ` 1230` ``` unfolding integrable_def by auto ``` hoelzl@35582 ` 1231` hoelzl@35582 ` 1232` ``` from x and y ``` hoelzl@35582 ` 1233` ``` have "a + y \ nnfis (\t. f t + ?np t)" ``` hoelzl@35582 ` 1234` ``` and "b + x \ nnfis (\t. g t + ?pp t)" using assms by (auto intro: nnfis_add) ``` hoelzl@35582 ` 1235` ``` moreover ``` hoelzl@35582 ` 1236` ``` have "\t. f t + ?np t = g t + ?pp t" ``` hoelzl@35582 ` 1237` ``` unfolding pos_part_def neg_part_def by auto ``` hoelzl@35582 ` 1238` ``` ultimately have "a - b = x - y" ``` hoelzl@35582 ` 1239` ``` using nnfis_unique by (auto simp: algebra_simps) ``` hoelzl@35582 ` 1240` ``` thus "integral (\t. f t - g t) = a - b" ``` hoelzl@35582 ` 1241` ``` unfolding integral_def ``` hoelzl@35582 ` 1242` ``` using the_nnfis[OF x] the_nnfis[OF y] by simp ``` hoelzl@35582 ` 1243` ```qed ``` hoelzl@35582 ` 1244` hoelzl@35582 ` 1245` ```lemma integral_borel_measurable: ``` hoelzl@35582 ` 1246` ``` "integrable f \ f \ borel_measurable M" ``` hoelzl@35582 ` 1247` ``` unfolding integrable_def ``` hoelzl@35582 ` 1248` ``` by (subst pos_part_neg_part_borel_measurable_iff) ``` hoelzl@35582 ` 1249` ``` (auto intro: nnfis_borel_measurable) ``` hoelzl@35582 ` 1250` hoelzl@35582 ` 1251` ```lemma integral_indicator_fn: ``` hoelzl@35582 ` 1252` ``` assumes "a \ sets M" ``` hoelzl@35582 ` 1253` ``` shows "integral (indicator_fn a) = measure M a" ``` hoelzl@35582 ` 1254` ``` and "integrable (indicator_fn a)" ``` hoelzl@35582 ` 1255` ``` using psfis_indicator[OF assms, THEN psfis_nnfis] ``` hoelzl@35582 ` 1256` ``` by (auto intro!: nnfis_integral) ``` hoelzl@35582 ` 1257` hoelzl@35582 ` 1258` ```lemma integral_add: ``` hoelzl@35582 ` 1259` ``` assumes "integrable f" and "integrable g" ``` hoelzl@35582 ` 1260` ``` shows "integrable (\t. f t + g t)" ``` hoelzl@35582 ` 1261` ``` and "integral (\t. f t + g t) = integral f + integral g" ``` hoelzl@35582 ` 1262` ```proof - ``` hoelzl@35582 ` 1263` ``` { fix t ``` hoelzl@35582 ` 1264` ``` have "pos_part f t + pos_part g t - (neg_part f t + neg_part g t) = ``` hoelzl@35582 ` 1265` ``` f t + g t" ``` hoelzl@35582 ` 1266` ``` unfolding pos_part_def neg_part_def by auto } ``` hoelzl@35582 ` 1267` ``` note part_sum = this ``` hoelzl@35582 ` 1268` hoelzl@35582 ` 1269` ``` from assms obtain a b c d where ``` hoelzl@35582 ` 1270` ``` a: "a \ nnfis (pos_part f)" and b: "b \ nnfis (neg_part f)" and ``` hoelzl@35582 ` 1271` ``` c: "c \ nnfis (pos_part g)" and d: "d \ nnfis (neg_part g)" ``` hoelzl@35582 ` 1272` ``` unfolding integrable_def by auto ``` hoelzl@35582 ` 1273` ``` note sums = nnfis_add[OF a c] nnfis_add[OF b d] ``` hoelzl@35582 ` 1274` ``` note int = nnfis_minus_nnfis_integral[OF sums, unfolded part_sum] ``` hoelzl@35582 ` 1275` hoelzl@35582 ` 1276` ``` show "integrable (\t. f t + g t)" using int(1) . ``` hoelzl@35582 ` 1277` hoelzl@35582 ` 1278` ``` show "integral (\t. f t + g t) = integral f + integral g" ``` hoelzl@35582 ` 1279` ``` using int(2) sums a b c d by (simp add: the_nnfis integral_def) ``` hoelzl@35582 ` 1280` ```qed ``` hoelzl@35582 ` 1281` hoelzl@35582 ` 1282` ```lemma integral_mono: ``` hoelzl@35582 ` 1283` ``` assumes "integrable f" and "integrable g" ``` hoelzl@35582 ` 1284` ``` and mono: "\t. t \ space M \ f t \ g t" ``` hoelzl@35582 ` 1285` ``` shows "integral f \ integral g" ``` hoelzl@35582 ` 1286` ```proof - ``` hoelzl@35582 ` 1287` ``` from assms obtain a b c d where ``` hoelzl@35582 ` 1288` ``` a: "a \ nnfis (pos_part f)" and b: "b \ nnfis (neg_part f)" and ``` hoelzl@35582 ` 1289` ``` c: "c \ nnfis (pos_part g)" and d: "d \ nnfis (neg_part g)" ``` hoelzl@35582 ` 1290` ``` unfolding integrable_def by auto ``` hoelzl@35582 ` 1291` hoelzl@35582 ` 1292` ``` have "a \ c" ``` hoelzl@35582 ` 1293` ``` proof (rule nnfis_mono[OF a c]) ``` hoelzl@35582 ` 1294` ``` fix t assume "t \ space M" ``` hoelzl@35582 ` 1295` ``` from mono[OF this] show "pos_part f t \ pos_part g t" ``` hoelzl@35582 ` 1296` ``` unfolding pos_part_def by auto ``` hoelzl@35582 ` 1297` ``` qed ``` hoelzl@35582 ` 1298` ``` moreover have "d \ b" ``` hoelzl@35582 ` 1299` ``` proof (rule nnfis_mono[OF d b]) ``` hoelzl@35582 ` 1300` ``` fix t assume "t \ space M" ``` hoelzl@35582 ` 1301` ``` from mono[OF this] show "neg_part g t \ neg_part f t" ``` hoelzl@35582 ` 1302` ``` unfolding neg_part_def by auto ``` hoelzl@35582 ` 1303` ``` qed ``` hoelzl@35582 ` 1304` ``` ultimately have "a - b \ c - d" by auto ``` hoelzl@35582 ` 1305` ``` thus ?thesis unfolding integral_def ``` hoelzl@35582 ` 1306` ``` using a b c d by (simp add: the_nnfis) ``` hoelzl@35582 ` 1307` ```qed ``` hoelzl@35582 ` 1308` hoelzl@35582 ` 1309` ```lemma integral_uminus: ``` hoelzl@35582 ` 1310` ``` assumes "integrable f" ``` hoelzl@35582 ` 1311` ``` shows "integrable (\t. - f t)" ``` hoelzl@35582 ` 1312` ``` and "integral (\t. - f t) = - integral f" ``` hoelzl@35582 ` 1313` ```proof - ``` hoelzl@35582 ` 1314` ``` have "pos_part f = neg_part (\t.-f t)" and "neg_part f = pos_part (\t.-f t)" ``` hoelzl@35582 ` 1315` ``` unfolding pos_part_def neg_part_def by (auto intro!: ext) ``` hoelzl@35582 ` 1316` ``` with assms show "integrable (\t.-f t)" and "integral (\t.-f t) = -integral f" ``` hoelzl@35582 ` 1317` ``` unfolding integrable_def integral_def by simp_all ``` hoelzl@35582 ` 1318` ```qed ``` hoelzl@35582 ` 1319` hoelzl@35582 ` 1320` ```lemma integral_times_const: ``` hoelzl@35582 ` 1321` ``` assumes "integrable f" ``` hoelzl@35582 ` 1322` ``` shows "integrable (\t. a * f t)" (is "?P a") ``` hoelzl@35582 ` 1323` ``` and "integral (\t. a * f t) = a * integral f" (is "?I a") ``` hoelzl@35582 ` 1324` ```proof - ``` hoelzl@35582 ` 1325` ``` { fix a :: real assume "0 \ a" ``` hoelzl@35582 ` 1326` ``` hence "pos_part (\t. a * f t) = (\t. a * pos_part f t)" ``` hoelzl@35582 ` 1327` ``` and "neg_part (\t. a * f t) = (\t. a * neg_part f t)" ``` hoelzl@35582 ` 1328` ``` unfolding pos_part_def neg_part_def max_def min_def ``` hoelzl@35582 ` 1329` ``` by (auto intro!: ext simp: zero_le_mult_iff) ``` hoelzl@35582 ` 1330` ``` moreover ``` hoelzl@35582 ` 1331` ``` obtain x y where x: "x \ nnfis (pos_part f)" and y: "y \ nnfis (neg_part f)" ``` hoelzl@35582 ` 1332` ``` using assms unfolding integrable_def by auto ``` hoelzl@35582 ` 1333` ``` ultimately ``` hoelzl@35582 ` 1334` ``` have "a * x \ nnfis (pos_part (\t. a * f t))" and ``` hoelzl@35582 ` 1335` ``` "a * y \ nnfis (neg_part (\t. a * f t))" ``` hoelzl@35582 ` 1336` ``` using nnfis_times[OF _ `0 \ a`] by auto ``` hoelzl@35582 ` 1337` ``` with x y have "?P a \ ?I a" ``` hoelzl@35582 ` 1338` ``` unfolding integrable_def integral_def by (auto simp: algebra_simps) } ``` hoelzl@35582 ` 1339` ``` note int = this ``` hoelzl@35582 ` 1340` hoelzl@35582 ` 1341` ``` have "?P a \ ?I a" ``` hoelzl@35582 ` 1342` ``` proof (cases "0 \ a") ``` hoelzl@35582 ` 1343` ``` case True from int[OF this] show ?thesis . ``` hoelzl@35582 ` 1344` ``` next ``` hoelzl@35582 ` 1345` ``` case False with int[of "- a"] integral_uminus[of "\t. - a * f t"] ``` hoelzl@35582 ` 1346` ``` show ?thesis by auto ``` hoelzl@35582 ` 1347` ``` qed ``` hoelzl@35582 ` 1348` ``` thus "integrable (\t. a * f t)" ``` hoelzl@35582 ` 1349` ``` and "integral (\t. a * f t) = a * integral f" by simp_all ``` hoelzl@35582 ` 1350` ```qed ``` hoelzl@35582 ` 1351` hoelzl@35582 ` 1352` ```lemma integral_cmul_indicator: ``` hoelzl@35582 ` 1353` ``` assumes "s \ sets M" ``` hoelzl@35582 ` 1354` ``` shows "integral (\x. c * indicator_fn s x) = c * (measure M s)" ``` hoelzl@35582 ` 1355` ``` and "integrable (\x. c * indicator_fn s x)" ``` hoelzl@35582 ` 1356` ```using assms integral_times_const integral_indicator_fn by auto ``` hoelzl@35582 ` 1357` hoelzl@35582 ` 1358` ```lemma integral_zero: ``` hoelzl@35582 ` 1359` ``` shows "integral (\x. 0) = 0" ``` hoelzl@35582 ` 1360` ``` and "integrable (\x. 0)" ``` hoelzl@35582 ` 1361` ``` using integral_cmul_indicator[OF empty_sets, of 0] ``` hoelzl@35582 ` 1362` ``` unfolding indicator_fn_def by auto ``` hoelzl@35582 ` 1363` hoelzl@35582 ` 1364` ```lemma integral_setsum: ``` hoelzl@35582 ` 1365` ``` assumes "finite S" ``` hoelzl@35582 ` 1366` ``` assumes "\n. n \ S \ integrable (f n)" ``` hoelzl@35582 ` 1367` ``` shows "integral (\x. \ i \ S. f i x) = (\ i \ S. integral (f i))" (is "?int S") ``` hoelzl@35582 ` 1368` ``` and "integrable (\x. \ i \ S. f i x)" (is "?I s") ``` hoelzl@35582 ` 1369` ```proof - ``` hoelzl@35582 ` 1370` ``` from assms have "?int S \ ?I S" ``` hoelzl@35582 ` 1371` ``` proof (induct S) ``` hoelzl@35582 ` 1372` ``` case empty thus ?case by (simp add: integral_zero) ``` hoelzl@35582 ` 1373` ``` next ``` hoelzl@35582 ` 1374` ``` case (insert i S) ``` hoelzl@35582 ` 1375` ``` thus ?case ``` hoelzl@35582 ` 1376` ``` apply simp ``` hoelzl@35582 ` 1377` ``` apply (subst integral_add) ``` hoelzl@35582 ` 1378` ``` using assms apply auto ``` hoelzl@35582 ` 1379` ``` apply (subst integral_add) ``` hoelzl@35582 ` 1380` ``` using assms by auto ``` hoelzl@35582 ` 1381` ``` qed ``` hoelzl@35582 ` 1382` ``` thus "?int S" and "?I S" by auto ``` hoelzl@35582 ` 1383` ```qed ``` hoelzl@35582 ` 1384` hoelzl@35582 ` 1385` ```lemma markov_ineq: ``` hoelzl@35582 ` 1386` ``` assumes "integrable f" "0 < a" "integrable (\x. \f x\^n)" ``` hoelzl@35582 ` 1387` ``` shows "measure M (f -` {a ..} \ space M) \ integral (\x. \f x\^n) / a^n" ``` hoelzl@35582 ` 1388` ```using assms ``` hoelzl@35582 ` 1389` ```proof - ``` hoelzl@35582 ` 1390` ``` from assms have "0 < a ^ n" using real_root_pow_pos by auto ``` hoelzl@35582 ` 1391` ``` from assms have "f \ borel_measurable M" ``` hoelzl@35582 ` 1392` ``` using integral_borel_measurable[OF `integrable f`] by auto ``` hoelzl@35582 ` 1393` ``` hence w: "{w . w \ space M \ a \ f w} \ sets M" ``` hoelzl@35582 ` 1394` ``` using borel_measurable_ge_iff by auto ``` hoelzl@35582 ` 1395` ``` have i: "integrable (indicator_fn {w . w \ space M \ a \ f w})" ``` hoelzl@35582 ` 1396` ``` using integral_indicator_fn[OF w] by simp ``` hoelzl@35582 ` 1397` ``` have v1: "\ t. a ^ n * (indicator_fn {w . w \ space M \ a \ f w}) t ``` hoelzl@35582 ` 1398` ``` \ (f t) ^ n * (indicator_fn {w . w \ space M \ a \ f w}) t" ``` hoelzl@35582 ` 1399` ``` unfolding indicator_fn_def ``` hoelzl@35582 ` 1400` ``` using `0 < a` power_mono[of a] assms by auto ``` hoelzl@35582 ` 1401` ``` have v2: "\ t. (f t) ^ n * (indicator_fn {w . w \ space M \ a \ f w}) t \ \f t\ ^ n" ``` hoelzl@35582 ` 1402` ``` unfolding indicator_fn_def ``` hoelzl@35582 ` 1403` ``` using power_mono[of a _ n] abs_ge_self `a > 0` ``` hoelzl@35582 ` 1404` ``` by auto ``` hoelzl@35582 ` 1405` ``` have "{w \ space M. a \ f w} \ space M = {w . a \ f w} \ space M" ``` hoelzl@35582 ` 1406` ``` using Collect_eq by auto ``` hoelzl@35582 ` 1407` ``` from Int_absorb2[OF sets_into_space[OF w]] `0 < a ^ n` sets_into_space[OF w] w this ``` hoelzl@35582 ` 1408` ``` have "(a ^ n) * (measure M ((f -` {y . a \ y}) \ space M)) = ``` hoelzl@35582 ` 1409` ``` (a ^ n) * measure M {w . w \ space M \ a \ f w}" ``` hoelzl@35582 ` 1410` ``` unfolding vimage_Collect_eq[of f] by simp ``` hoelzl@35582 ` 1411` ``` also have "\ = integral (\ t. a ^ n * (indicator_fn {w . w \ space M \ a \ f w}) t)" ``` hoelzl@35582 ` 1412` ``` using integral_cmul_indicator[OF w] i by auto ``` hoelzl@35582 ` 1413` ``` also have "\ \ integral (\ t. \ f t \ ^ n)" ``` hoelzl@35582 ` 1414` ``` apply (rule integral_mono) ``` hoelzl@35582 ` 1415` ``` using integral_cmul_indicator[OF w] ``` hoelzl@35582 ` 1416` ``` `integrable (\ x. \f x\ ^ n)` real_le_trans[OF v1 v2] by auto ``` hoelzl@35582 ` 1417` ``` finally show "measure M (f -` {a ..} \ space M) \ integral (\x. \f x\^n) / a^n" ``` hoelzl@35582 ` 1418` ``` unfolding atLeast_def ``` hoelzl@35582 ` 1419` ``` by (auto intro!: mult_imp_le_div_pos[OF `0 < a ^ n`], simp add: real_mult_commute) ``` hoelzl@35582 ` 1420` ```qed ``` hoelzl@35582 ` 1421` hoelzl@35582 ` 1422` ```lemma integral_finite_on_sets: ``` hoelzl@35582 ` 1423` ``` assumes "f \ borel_measurable M" and "finite (space M)" and "a \ sets M" ``` hoelzl@35582 ` 1424` ``` shows "integral (\x. f x * indicator_fn a x) = ``` hoelzl@35582 ` 1425` ``` (\ r \ f`a. r * measure M (f -` {r} \ a))" (is "integral ?f = _") ``` hoelzl@35582 ` 1426` ```proof - ``` hoelzl@35582 ` 1427` ``` { fix x assume "x \ a" ``` hoelzl@35582 ` 1428` ``` with assms have "f -` {f x} \ space M \ sets M" ``` hoelzl@35582 ` 1429` ``` by (subst Int_commute) ``` hoelzl@35582 ` 1430` ``` (auto simp: vimage_def Int_def ``` hoelzl@35582 ` 1431` ``` intro!: borel_measurable_const ``` hoelzl@35582 ` 1432` ``` borel_measurable_eq_borel_measurable) ``` hoelzl@35582 ` 1433` ``` from Int[OF this assms(3)] ``` hoelzl@35582 ` 1434` ``` sets_into_space[OF assms(3), THEN Int_absorb1] ``` hoelzl@35582 ` 1435` ``` have "f -` {f x} \ a \ sets M" by (simp add: Int_assoc) } ``` hoelzl@35582 ` 1436` ``` note vimage_f = this ``` hoelzl@35582 ` 1437` hoelzl@35582 ` 1438` ``` have "finite a" ``` hoelzl@35582 ` 1439` ``` using assms(2,3) sets_into_space ``` hoelzl@35582 ` 1440` ``` by (auto intro: finite_subset) ``` hoelzl@35582 ` 1441` hoelzl@35582 ` 1442` ``` have "integral (\x. f x * indicator_fn a x) = ``` hoelzl@35582 ` 1443` ``` integral (\x. \i\f ` a. i * indicator_fn (f -` {i} \ a) x)" ``` hoelzl@35582 ` 1444` ``` (is "_ = integral (\x. setsum (?f x) _)") ``` hoelzl@35582 ` 1445` ``` unfolding indicator_fn_def if_distrib ``` hoelzl@35582 ` 1446` ``` using `finite a` by (auto simp: setsum_cases intro!: integral_cong) ``` hoelzl@35582 ` 1447` ``` also have "\ = (\i\f`a. integral (\x. ?f x i))" ``` hoelzl@35582 ` 1448` ``` proof (rule integral_setsum, safe) ``` hoelzl@35582 ` 1449` ``` fix n x assume "x \ a" ``` hoelzl@35582 ` 1450` ``` thus "integrable (\y. ?f y (f x))" ``` hoelzl@35582 ` 1451` ``` using integral_indicator_fn(2)[OF vimage_f] ``` hoelzl@35582 ` 1452` ``` by (auto intro!: integral_times_const) ``` hoelzl@35582 ` 1453` ``` qed (simp add: `finite a`) ``` hoelzl@35582 ` 1454` ``` also have "\ = (\i\f`a. i * measure M (f -` {i} \ a))" ``` hoelzl@35582 ` 1455` ``` using integral_cmul_indicator[OF vimage_f] ``` hoelzl@35582 ` 1456` ``` by (auto intro!: setsum_cong) ``` hoelzl@35582 ` 1457` ``` finally show ?thesis . ``` hoelzl@35582 ` 1458` ```qed ``` hoelzl@35582 ` 1459` hoelzl@35582 ` 1460` ```lemma integral_finite: ``` hoelzl@35582 ` 1461` ``` assumes "f \ borel_measurable M" and "finite (space M)" ``` hoelzl@35582 ` 1462` ``` shows "integral f = (\ r \ f ` space M. r * measure M (f -` {r} \ space M))" ``` hoelzl@35582 ` 1463` ``` using integral_finite_on_sets[OF assms top] ``` hoelzl@35582 ` 1464` ``` integral_cong[of "\x. f x * indicator_fn (space M) x" f] ``` hoelzl@35582 ` 1465` ``` by (auto simp add: indicator_fn_def) ``` hoelzl@35582 ` 1466` hoelzl@35582 ` 1467` ```lemma integral_finite_singleton: ``` hoelzl@35582 ` 1468` ``` assumes fin: "finite (space M)" and "Pow (space M) = sets M" ``` hoelzl@35582 ` 1469` ``` shows "integral f = (\x \ space M. f x * measure M {x})" ``` hoelzl@35582 ` 1470` ```proof - ``` hoelzl@35582 ` 1471` ``` have "f \ borel_measurable M" ``` hoelzl@35582 ` 1472` ``` unfolding borel_measurable_le_iff ``` hoelzl@35582 ` 1473` ``` using assms by auto ``` hoelzl@35582 ` 1474` ``` { fix r let ?x = "f -` {r} \ space M" ``` hoelzl@35582 ` 1475` ``` have "?x \ space M" by auto ``` hoelzl@35582 ` 1476` ``` with assms have "measure M ?x = (\i \ ?x. measure M {i})" ``` hoelzl@35582 ` 1477` ``` by (auto intro!: measure_real_sum_image) } ``` hoelzl@35582 ` 1478` ``` note measure_eq_setsum = this ``` hoelzl@35582 ` 1479` ``` show ?thesis ``` hoelzl@35582 ` 1480` ``` unfolding integral_finite[OF `f \ borel_measurable M` fin] ``` hoelzl@35582 ` 1481` ``` measure_eq_setsum setsum_right_distrib ``` hoelzl@35582 ` 1482` ``` apply (subst setsum_Sigma) ``` hoelzl@35582 ` 1483` ``` apply (simp add: assms) ``` hoelzl@35582 ` 1484` ``` apply (simp add: assms) ``` hoelzl@35582 ` 1485` ``` proof (rule setsum_reindex_cong[symmetric]) ``` hoelzl@35582 ` 1486` ``` fix a assume "a \ Sigma (f ` space M) (\x. f -` {x} \ space M)" ``` hoelzl@35582 ` 1487` ``` thus "(\(x, y). x * measure M {y}) a = f (snd a) * measure_space.measure M {snd a}" ``` hoelzl@35582 ` 1488` ``` by auto ``` hoelzl@35582 ` 1489` ``` qed (auto intro!: image_eqI inj_onI) ``` hoelzl@35582 ` 1490` ```qed ``` hoelzl@35582 ` 1491` hoelzl@35582 ` 1492` ```lemma borel_measurable_inverse: ``` hoelzl@35582 ` 1493` ``` assumes "f \ borel_measurable M" ``` hoelzl@35582 ` 1494` ``` shows "(\x. inverse (f x)) \ borel_measurable M" ``` hoelzl@35582 ` 1495` ``` unfolding borel_measurable_ge_iff ``` hoelzl@35582 ` 1496` ```proof (safe, rule linorder_cases) ``` hoelzl@35582 ` 1497` ``` fix a :: real assume "0 < a" ``` hoelzl@35582 ` 1498` ``` { fix w ``` hoelzl@35582 ` 1499` ``` from `0 < a` have "a \ inverse (f w) \ 0 < f w \ f w \ 1 / a" ``` hoelzl@35582 ` 1500` ``` by (metis inverse_eq_divide inverse_inverse_eq le_imp_inverse_le ``` hoelzl@35582 ` 1501` ``` linorder_not_le real_le_refl real_le_trans real_less_def ``` hoelzl@35582 ` 1502` ``` xt1(7) zero_less_divide_1_iff) } ``` hoelzl@35582 ` 1503` ``` hence "{w \ space M. a \ inverse (f w)} = ``` hoelzl@35582 ` 1504` ``` {w \ space M. 0 < f w} \ {w \ space M. f w \ 1 / a}" by auto ``` hoelzl@35582 ` 1505` ``` with Int assms[unfolded borel_measurable_gr_iff] ``` hoelzl@35582 ` 1506` ``` assms[unfolded borel_measurable_le_iff] ``` hoelzl@35582 ` 1507` ``` show "{w \ space M. a \ inverse (f w)} \ sets M" by simp ``` hoelzl@35582 ` 1508` ```next ``` hoelzl@35582 ` 1509` ``` fix a :: real assume "0 = a" ``` hoelzl@35582 ` 1510` ``` { fix w have "a \ inverse (f w) \ 0 \ f w" ``` hoelzl@35582 ` 1511` ``` unfolding `0 = a`[symmetric] by auto } ``` hoelzl@35582 ` 1512` ``` thus "{w \ space M. a \ inverse (f w)} \ sets M" ``` hoelzl@35582 ` 1513` ``` using assms[unfolded borel_measurable_ge_iff] by simp ``` hoelzl@35582 ` 1514` ```next ``` hoelzl@35582 ` 1515` ``` fix a :: real assume "a < 0" ``` hoelzl@35582 ` 1516` ``` { fix w ``` hoelzl@35582 ` 1517` ``` from `a < 0` have "a \ inverse (f w) \ f w \ 1 / a \ 0 \ f w" ``` hoelzl@35582 ` 1518` ``` apply (cases "0 \ f w") ``` hoelzl@35582 ` 1519` ``` apply (metis inverse_eq_divide linorder_not_le xt1(8) xt1(9) ``` hoelzl@35582 ` 1520` ``` zero_le_divide_1_iff) ``` hoelzl@35582 ` 1521` ``` apply (metis inverse_eq_divide inverse_inverse_eq inverse_le_imp_le_neg ``` hoelzl@35582 ` 1522` ``` linorder_not_le real_le_refl real_le_trans) ``` hoelzl@35582 ` 1523` ``` done } ``` hoelzl@35582 ` 1524` ``` hence "{w \ space M. a \ inverse (f w)} = ``` hoelzl@35582 ` 1525` ``` {w \ space M. f w \ 1 / a} \ {w \ space M. 0 \ f w}" by auto ``` hoelzl@35582 ` 1526` ``` with Un assms[unfolded borel_measurable_ge_iff] ``` hoelzl@35582 ` 1527` ``` assms[unfolded borel_measurable_le_iff] ``` hoelzl@35582 ` 1528` ``` show "{w \ space M. a \ inverse (f w)} \ sets M" by simp ``` hoelzl@35582 ` 1529` ```qed ``` hoelzl@35582 ` 1530` hoelzl@35582 ` 1531` ```lemma borel_measurable_divide: ``` hoelzl@35582 ` 1532` ``` assumes "f \ borel_measurable M" ``` hoelzl@35582 ` 1533` ``` and "g \ borel_measurable M" ``` hoelzl@35582 ` 1534` ``` shows "(\x. f x / g x) \ borel_measurable M" ``` hoelzl@35582 ` 1535` ``` unfolding field_divide_inverse ``` hoelzl@35582 ` 1536` ``` by (rule borel_measurable_inverse borel_measurable_times_borel_measurable assms)+ ``` hoelzl@35582 ` 1537` hoelzl@35582 ` 1538` ```lemma RN_deriv_finite_singleton: ``` hoelzl@35582 ` 1539` ``` fixes v :: "'a set \ real" ``` hoelzl@35582 ` 1540` ``` assumes finite: "finite (space M)" and Pow: "Pow (space M) = sets M" ``` hoelzl@35582 ` 1541` ``` and ms_v: "measure_space (M\measure := v\)" ``` hoelzl@35582 ` 1542` ``` and eq_0: "\x. measure M {x} = 0 \ v {x} = 0" ``` hoelzl@35582 ` 1543` ``` and "x \ space M" and "measure M {x} \ 0" ``` hoelzl@35582 ` 1544` ``` shows "RN_deriv v x = v {x} / (measure M {x})" (is "_ = ?v x") ``` hoelzl@35582 ` 1545` ``` unfolding RN_deriv_def ``` hoelzl@35582 ` 1546` ```proof (rule someI2_ex[where Q = "\f. f x = ?v x"], rule exI[where x = ?v], safe) ``` hoelzl@35582 ` 1547` ``` show "(\a. v {a} / measure_space.measure M {a}) \ borel_measurable M" ``` hoelzl@35582 ` 1548` ``` unfolding borel_measurable_le_iff using Pow by auto ``` hoelzl@35582 ` 1549` ```next ``` hoelzl@35582 ` 1550` ``` fix a assume "a \ sets M" ``` hoelzl@35582 ` 1551` ``` hence "a \ space M" and "finite a" ``` hoelzl@35582 ` 1552` ``` using sets_into_space finite by (auto intro: finite_subset) ``` hoelzl@35582 ` 1553` ``` have *: "\x a. (if measure M {x} = 0 then 0 else v {x} * indicator_fn a x) = ``` hoelzl@35582 ` 1554` ``` v {x} * indicator_fn a x" using eq_0 by auto ``` hoelzl@35582 ` 1555` hoelzl@35582 ` 1556` ``` from measure_space.measure_real_sum_image[OF ms_v, of a] ``` hoelzl@35582 ` 1557` ``` Pow `a \ sets M` sets_into_space `finite a` ``` hoelzl@35582 ` 1558` ``` have "v a = (\x\a. v {x})" by auto ``` hoelzl@35582 ` 1559` ``` thus "integral (\x. v {x} / measure_space.measure M {x} * indicator_fn a x) = v a" ``` hoelzl@35582 ` 1560` ``` apply (simp add: eq_0 integral_finite_singleton[OF finite Pow]) ``` hoelzl@35582 ` 1561` ``` apply (unfold divide_1) ``` hoelzl@35582 ` 1562` ``` by (simp add: * indicator_fn_def if_distrib setsum_cases finite `a \ space M` Int_absorb1) ``` hoelzl@35582 ` 1563` ```next ``` hoelzl@35582 ` 1564` ``` fix w assume "w \ borel_measurable M" ``` hoelzl@35582 ` 1565` ``` assume int_eq_v: "\a\sets M. integral (\x. w x * indicator_fn a x) = v a" ``` hoelzl@35582 ` 1566` ``` have "{x} \ sets M" using Pow `x \ space M` by auto ``` hoelzl@35582 ` 1567` hoelzl@35582 ` 1568` ``` have "w x * measure M {x} = ``` hoelzl@35582 ` 1569` ``` (\y\space M. w y * indicator_fn {x} y * measure M {y})" ``` hoelzl@35582 ` 1570` ``` apply (subst (3) mult_commute) ``` hoelzl@35582 ` 1571` ``` unfolding indicator_fn_def if_distrib setsum_cases[OF finite] ``` hoelzl@35582 ` 1572` ``` using `x \ space M` by simp ``` hoelzl@35582 ` 1573` ``` also have "... = v {x}" ``` hoelzl@35582 ` 1574` ``` using int_eq_v[rule_format, OF `{x} \ sets M`] ``` hoelzl@35582 ` 1575` ``` by (simp add: integral_finite_singleton[OF finite Pow]) ``` hoelzl@35582 ` 1576` ``` finally show "w x = v {x} / measure M {x}" ``` hoelzl@35582 ` 1577` ``` using `measure M {x} \ 0` by (simp add: eq_divide_eq) ``` hoelzl@35582 ` 1578` ```qed fact ``` hoelzl@35582 ` 1579` hoelzl@35582 ` 1580` ```lemma countable_space_integral_reduce: ``` hoelzl@35582 ` 1581` ``` assumes "positive M (measure M)" and "f \ borel_measurable M" ``` hoelzl@35582 ` 1582` ``` and "countable (f ` space M)" ``` hoelzl@35582 ` 1583` ``` and "\ finite (pos_part f ` space M)" ``` hoelzl@35582 ` 1584` ``` and "\ finite (neg_part f ` space M)" ``` hoelzl@35582 ` 1585` ``` and "((\r. r * measure m (neg_part f -` {r} \ space m)) o enumerate (neg_part f ` space M)) sums n" ``` hoelzl@35582 ` 1586` ``` and "((\r. r * measure m (pos_part f -` {r} \ space m)) o enumerate (pos_part f ` space M)) sums p" ``` hoelzl@35582 ` 1587` ``` shows "integral f = p - n" ``` hoelzl@35582 ` 1588` ```oops ``` hoelzl@35582 ` 1589` hoelzl@35582 ` 1590` ```(* ``` hoelzl@35582 ` 1591` ```val countable_space_integral_reduce = store_thm ``` hoelzl@35582 ` 1592` ``` ("countable_space_integral_reduce", ``` hoelzl@35582 ` 1593` ``` "\m f p n. measure_space m \ ``` hoelzl@35582 ` 1594` ``` positive m \ ``` hoelzl@35582 ` 1595` ``` f \ borel_measurable (space m, sets m) \ ``` hoelzl@35582 ` 1596` ``` countable (IMAGE f (space m)) \ ``` hoelzl@35582 ` 1597` ``` ~(FINITE (IMAGE (pos_part f) (space m))) \ ``` hoelzl@35582 ` 1598` ``` ~(FINITE (IMAGE (neg_part f) (space m))) \ ``` hoelzl@35582 ` 1599` ``` (\r. r * ``` hoelzl@35582 ` 1600` ``` measure m (PREIMAGE (neg_part f) {r} \ space m)) o ``` hoelzl@35582 ` 1601` ``` enumerate ((IMAGE (neg_part f) (space m))) sums n \ ``` hoelzl@35582 ` 1602` ``` (\r. r * ``` hoelzl@35582 ` 1603` ``` measure m (PREIMAGE (pos_part f) {r} \ space m)) o ``` hoelzl@35582 ` 1604` ``` enumerate ((IMAGE (pos_part f) (space m))) sums p ==> ``` hoelzl@35582 ` 1605` ``` (integral m f = p - n)", ``` hoelzl@35582 ` 1606` ``` RW_TAC std_ss [integral_def] ``` hoelzl@35582 ` 1607` ``` ++ Suff `((@i. i \ nnfis m (pos_part f)) = p) \ ((@i. i \ nnfis m (neg_part f)) = n)` ``` hoelzl@35582 ` 1608` ``` >> RW_TAC std_ss [] ``` hoelzl@35582 ` 1609` ``` ++ (CONJ_TAC ++ MATCH_MP_TAC SELECT_UNIQUE ++ RW_TAC std_ss []) ``` hoelzl@35582 ` 1610` ``` >> (Suff `p \ nnfis m (pos_part f)` >> METIS_TAC [nnfis_unique] ``` hoelzl@35582 ` 1611` ``` ++ MATCH_MP_TAC nnfis_mon_conv ``` hoelzl@35582 ` 1612` ``` ++ `BIJ (enumerate(IMAGE (pos_part f) (space m))) UNIV (IMAGE (pos_part f) (space m))` ``` hoelzl@35582 ` 1613` ``` by (`countable (IMAGE (pos_part f) (space m))` ``` hoelzl@35582 ` 1614` ``` by (MATCH_MP_TAC COUNTABLE_SUBSET ``` hoelzl@35582 ` 1615` ``` ++ Q.EXISTS_TAC `0 INSERT (IMAGE f (space m))` ``` hoelzl@35582 ` 1616` ``` ++ RW_TAC std_ss [SUBSET_DEF, IN_IMAGE, pos_part_def, COUNTABLE_INSERT, IN_INSERT] ``` hoelzl@35582 ` 1617` ``` ++ METIS_TAC []) ``` hoelzl@35582 ` 1618` ``` ++ METIS_TAC [COUNTABLE_ALT]) ``` hoelzl@35582 ` 1619` ``` ++ FULL_SIMP_TAC std_ss [sums, BIJ_DEF, INJ_DEF, SURJ_DEF, IN_UNIV] ``` hoelzl@35582 ` 1620` ``` ++ Q.EXISTS_TAC `(\n t. if t \ space m \ pos_part f t \ IMAGE (enumerate (IMAGE (pos_part f) (space m))) ``` hoelzl@35582 ` 1621` ``` (pred_set\$count n) then pos_part f t else 0)` ``` hoelzl@35582 ` 1622` ``` ++ Q.EXISTS_TAC `(\n. ``` hoelzl@35582 ` 1623` ``` sum (0,n) ``` hoelzl@35582 ` 1624` ``` ((\r. ``` hoelzl@35582 ` 1625` ``` r * ``` hoelzl@35582 ` 1626` ``` measure m (PREIMAGE (pos_part f) {r} \ space m)) o ``` hoelzl@35582 ` 1627` ``` enumerate (IMAGE (pos_part f) (space m))))` ``` hoelzl@35582 ` 1628` ``` ++ ASM_SIMP_TAC std_ss [] ``` hoelzl@35582 ` 1629` ``` ++ CONJ_TAC ``` hoelzl@35582 ` 1630` ``` >> (RW_TAC std_ss [mono_convergent_def] ``` hoelzl@35582 ` 1631` ``` >> (RW_TAC real_ss [IN_IMAGE, pred_setTheory.IN_COUNT, pos_part_def] ++ METIS_TAC [LESS_LESS_EQ_TRANS]) ``` hoelzl@35582 ` 1632` ``` ++ RW_TAC std_ss [SEQ] ``` hoelzl@35582 ` 1633` ``` ++ `\N. enumerate (IMAGE (pos_part f) (space m)) N = (pos_part f) t` ``` hoelzl@35582 ` 1634` ``` by METIS_TAC [IN_IMAGE] ``` hoelzl@35582 ` 1635` ``` ++ Q.EXISTS_TAC `SUC N` ``` hoelzl@35582 ` 1636` ``` ++ RW_TAC real_ss [GREATER_EQ, real_ge, IN_IMAGE, REAL_SUB_LZERO] ``` hoelzl@35582 ` 1637` ``` ++ FULL_SIMP_TAC std_ss [pred_setTheory.IN_COUNT] ``` hoelzl@35582 ` 1638` ``` ++ METIS_TAC [DECIDE "!n:num. n < SUC n", LESS_LESS_EQ_TRANS, pos_part_def]) ``` hoelzl@35582 ` 1639` ``` ++ STRIP_TAC ++ MATCH_MP_TAC psfis_nnfis ++ ASM_SIMP_TAC std_ss [GSYM REAL_SUM_IMAGE_COUNT] ``` hoelzl@35582 ` 1640` ``` ++ `(\t. (if t \ space m \ pos_part f t \ IMAGE (enumerate (IMAGE (pos_part f) (space m))) (pred_set\$count n') ``` hoelzl@35582 ` 1641` ``` then pos_part f t else 0)) = ``` hoelzl@35582 ` 1642` ``` (\t. SIGMA (\i. (\i. enumerate (IMAGE (pos_part f) (space m)) i) i * ``` hoelzl@35582 ` 1643` ``` indicator_fn ((\i. PREIMAGE (pos_part f) {enumerate (IMAGE (pos_part f) (space m)) i} ``` hoelzl@35582 ` 1644` ``` \ (space m)) i) t) ``` hoelzl@35582 ` 1645` ``` (pred_set\$count n'))` ``` hoelzl@35582 ` 1646` ``` by (RW_TAC std_ss [FUN_EQ_THM] ++ RW_TAC real_ss [IN_IMAGE] ``` hoelzl@35582 ` 1647` ``` >> (`pred_set\$count n' = x INSERT (pred_set\$count n')` ``` hoelzl@35582 ` 1648` ``` by (ONCE_REWRITE_TAC [EXTENSION] ++ RW_TAC std_ss [IN_INSERT] ++ METIS_TAC []) ``` hoelzl@35582 ` 1649` ``` ++ POP_ORW ``` hoelzl@35582 ` 1650` ``` ++ RW_TAC std_ss [REAL_SUM_IMAGE_THM, pred_setTheory.FINITE_COUNT] ``` hoelzl@35582 ` 1651` ``` ++ ONCE_REWRITE_TAC [(REWRITE_RULE [pred_setTheory.FINITE_COUNT] o ``` hoelzl@35582 ` 1652` ``` REWRITE_RULE [FINITE_DELETE] o Q.ISPEC `pred_set\$count n' DELETE x`) REAL_SUM_IMAGE_IN_IF] ``` hoelzl@35582 ` 1653` ``` ++ RW_TAC real_ss [IN_DELETE, indicator_fn_def, IN_INTER, IN_SING, IN_PREIMAGE] ``` hoelzl@35582 ` 1654` ``` ++ `(\x'. (if x' \ pred_set\$count n' \ ~(x' = x) then ``` hoelzl@35582 ` 1655` ``` enumerate (IMAGE (pos_part f) (space m)) x' * ``` hoelzl@35582 ` 1656` ``` (if enumerate (IMAGE (pos_part f) (space m)) x = ``` hoelzl@35582 ` 1657` ``` enumerate (IMAGE (pos_part f) (space m)) x' ``` hoelzl@35582 ` 1658` ``` then 1 else 0) else 0)) = (\x. 0)` ``` hoelzl@35582 ` 1659` ``` by (RW_TAC std_ss [FUN_EQ_THM] ++ RW_TAC real_ss [] ++ METIS_TAC []) ``` hoelzl@35582 ` 1660` ``` ++ POP_ORW ``` hoelzl@35582 ` 1661` ``` ++ RW_TAC real_ss [REAL_SUM_IMAGE_0, pred_setTheory.FINITE_COUNT, FINITE_DELETE]) ``` hoelzl@35582 ` 1662` ``` ++ FULL_SIMP_TAC real_ss [IN_IMAGE, indicator_fn_def, IN_INTER, IN_PREIMAGE, IN_SING] ``` hoelzl@35582 ` 1663` ``` >> RW_TAC real_ss [REAL_SUM_IMAGE_0, pred_setTheory.FINITE_COUNT, FINITE_DELETE] ``` hoelzl@35582 ` 1664` ``` ++ ONCE_REWRITE_TAC [(REWRITE_RULE [pred_setTheory.FINITE_COUNT] o Q.ISPEC `pred_set\$count n'`) ``` hoelzl@35582 ` 1665` ``` REAL_SUM_IMAGE_IN_IF] ``` hoelzl@35582 ` 1666` ``` ++ `(\x. (if x \ pred_set\$count n' then ``` hoelzl@35582 ` 1667` ``` (\i. enumerate (IMAGE (pos_part f) (space m)) i * ``` hoelzl@35582 ` 1668` ``` (if (pos_part f t = enumerate (IMAGE (pos_part f) (space m)) i) \ ``` hoelzl@35582 ` 1669` ``` t \ space m then 1 else 0)) x else 0)) = (\x. 0)` ``` hoelzl@35582 ` 1670` ``` by (RW_TAC std_ss [FUN_EQ_THM] ++ RW_TAC real_ss [] ++ METIS_TAC []) ``` hoelzl@35582 ` 1671` ``` ++ POP_ORW ``` hoelzl@35582 ` 1672` ``` ++ RW_TAC real_ss [REAL_SUM_IMAGE_0, pred_setTheory.FINITE_COUNT]) ``` hoelzl@35582 ` 1673` ``` ++ POP_ORW ``` hoelzl@35582 ` 1674` ``` ++ `((\r. r * measure m (PREIMAGE (pos_part f) {r} \ space m)) o ``` hoelzl@35582 ` 1675` ``` enumerate (IMAGE (pos_part f) (space m))) = ``` hoelzl@35582 ` 1676` ``` (\i. (\i. enumerate (IMAGE (pos_part f) (space m)) i) i * ``` hoelzl@35582 ` 1677` ``` measure m ((\i. ``` hoelzl@35582 ` 1678` ``` PREIMAGE (pos_part f) ``` hoelzl@35582 ` 1679` ``` {enumerate (IMAGE (pos_part f) (space m)) i} \ ``` hoelzl@35582 ` 1680` ``` space m) i))` ``` hoelzl@35582 ` 1681` ``` by (RW_TAC std_ss [FUN_EQ_THM, o_DEF] ++ RW_TAC real_ss []) ``` hoelzl@35582 ` 1682` ``` ++ POP_ORW ``` hoelzl@35582 ` 1683` ``` ++ MATCH_MP_TAC psfis_intro ``` hoelzl@35582 ` 1684` ``` ++ ASM_SIMP_TAC std_ss [pred_setTheory.FINITE_COUNT] ``` hoelzl@35582 ` 1685` ``` ++ REVERSE CONJ_TAC ``` hoelzl@35582 ` 1686` ``` >> (FULL_SIMP_TAC real_ss [IN_IMAGE, pos_part_def] ``` hoelzl@35582 ` 1687` ``` ++ METIS_TAC [REAL_LE_REFL]) ``` hoelzl@35582 ` 1688` ``` ++ `(pos_part f) \ borel_measurable (space m, sets m)` ``` hoelzl@35582 ` 1689` ``` by METIS_TAC [pos_part_neg_part_borel_measurable] ``` hoelzl@35582 ` 1690` ``` ++ REPEAT STRIP_TAC ``` hoelzl@35582 ` 1691` ``` ++ `PREIMAGE (pos_part f) {enumerate (IMAGE (pos_part f) (space m)) i} \ space m = ``` hoelzl@35582 ` 1692` ``` {w | w \ space m \ ((pos_part f) w = (\w. enumerate (IMAGE (pos_part f) (space m)) i) w)}` ``` hoelzl@35582 ` 1693` ``` by (ONCE_REWRITE_TAC [EXTENSION] ++ RW_TAC std_ss [GSPECIFICATION, IN_INTER, IN_PREIMAGE, IN_SING] ``` hoelzl@35582 ` 1694` ``` ++ DECIDE_TAC) ``` hoelzl@35582 ` 1695` ``` ++ POP_ORW ``` hoelzl@35582 ` 1696` ``` ++ MATCH_MP_TAC borel_measurable_eq_borel_measurable ``` hoelzl@35582 ` 1697` ``` ++ METIS_TAC [borel_measurable_const, measure_space_def]) ``` hoelzl@35582 ` 1698` ``` ++ Suff `n \ nnfis m (neg_part f)` >> METIS_TAC [nnfis_unique] ``` hoelzl@35582 ` 1699` ``` ++ MATCH_MP_TAC nnfis_mon_conv ``` hoelzl@35582 ` 1700` ``` ++ `BIJ (enumerate(IMAGE (neg_part f) (space m))) UNIV (IMAGE (neg_part f) (space m))` ``` hoelzl@35582 ` 1701` ``` by (`countable (IMAGE (neg_part f) (space m))` ``` hoelzl@35582 ` 1702` ``` by (MATCH_MP_TAC COUNTABLE_SUBSET ``` hoelzl@35582 ` 1703` ``` ++ Q.EXISTS_TAC `0 INSERT (IMAGE abs (IMAGE f (space m)))` ``` hoelzl@35582 ` 1704` ``` ++ RW_TAC std_ss [SUBSET_DEF, IN_IMAGE, abs, neg_part_def, COUNTABLE_INSERT, IN_INSERT, COUNTABLE_IMAGE] ``` hoelzl@35582 ` 1705` ``` ++ METIS_TAC []) ``` hoelzl@35582 ` 1706` ``` ++ METIS_TAC [COUNTABLE_ALT]) ``` hoelzl@35582 ` 1707` ``` ++ FULL_SIMP_TAC std_ss [sums, BIJ_DEF, INJ_DEF, SURJ_DEF, IN_UNIV] ``` hoelzl@35582 ` 1708` ``` ++ Q.EXISTS_TAC `(\n t. if t \ space m \ neg_part f t \ IMAGE (enumerate (IMAGE (neg_part f) (space m))) ``` hoelzl@35582 ` 1709` ``` (pred_set\$count n) then neg_part f t else 0)` ``` hoelzl@35582 ` 1710` ``` ++ Q.EXISTS_TAC `(\n. ``` hoelzl@35582 ` 1711` ``` sum (0,n) ``` hoelzl@35582 ` 1712` ``` ((\r. ``` hoelzl@35582 ` 1713` ``` r * ``` hoelzl@35582 ` 1714` ``` measure m (PREIMAGE (neg_part f) {r} \ space m)) o ``` hoelzl@35582 ` 1715` ``` enumerate (IMAGE (neg_part f) (space m))))` ``` hoelzl@35582 ` 1716` ``` ++ ASM_SIMP_TAC std_ss [] ``` hoelzl@35582 ` 1717` ``` ++ CONJ_TAC ``` hoelzl@35582 ` 1718` ``` >> (RW_TAC std_ss [mono_convergent_def] ``` hoelzl@35582 ` 1719` ``` >> (RW_TAC real_ss [IN_IMAGE, pred_setTheory.IN_COUNT, neg_part_def] ++ METIS_TAC [LESS_LESS_EQ_TRANS, REAL_LE_NEGTOTAL]) ``` hoelzl@35582 ` 1720` ``` ++ RW_TAC std_ss [SEQ] ``` hoelzl@35582 ` 1721` ``` ++ `\N. enumerate (IMAGE (neg_part f) (space m)) N = (neg_part f) t` ``` hoelzl@35582 ` 1722` ``` by METIS_TAC [IN_IMAGE] ``` hoelzl@35582 ` 1723` ``` ++ Q.EXISTS_TAC `SUC N` ``` hoelzl@35582 ` 1724` ``` ++ RW_TAC real_ss [GREATER_EQ, real_ge, IN_IMAGE, REAL_SUB_LZERO] ``` hoelzl@35582 ` 1725` ``` ++ FULL_SIMP_TAC std_ss [pred_setTheory.IN_COUNT] ``` hoelzl@35582 ` 1726` ``` ++ METIS_TAC [DECIDE "!n:num. n < SUC n", LESS_LESS_EQ_TRANS, neg_part_def]) ``` hoelzl@35582 ` 1727` ``` ++ STRIP_TAC ++ MATCH_MP_TAC psfis_nnfis ++ ASM_SIMP_TAC std_ss [GSYM REAL_SUM_IMAGE_COUNT] ``` hoelzl@35582 ` 1728` ``` ++ `(\t. (if t \ space m \ neg_part f t \ IMAGE (enumerate (IMAGE (neg_part f) (space m))) (pred_set\$count n') ``` hoelzl@35582 ` 1729` ``` then neg_part f t else 0)) = ``` hoelzl@35582 ` 1730` ``` (\t. SIGMA (\i. (\i. enumerate (IMAGE (neg_part f) (space m)) i) i * ``` hoelzl@35582 ` 1731` ``` indicator_fn ((\i. PREIMAGE (neg_part f) {enumerate (IMAGE (neg_part f) (space m)) i} ``` hoelzl@35582 ` 1732` ``` \ (space m)) i) t) ``` hoelzl@35582 ` 1733` ``` (pred_set\$count n'))` ``` hoelzl@35582 ` 1734` ``` by (RW_TAC std_ss [FUN_EQ_THM] ++ RW_TAC real_ss [IN_IMAGE] ``` hoelzl@35582 ` 1735` ``` >> (`pred_set\$count n' = x INSERT (pred_set\$count n')` ``` hoelzl@35582 ` 1736` ``` by (ONCE_REWRITE_TAC [EXTENSION] ++ RW_TAC std_ss [IN_INSERT] ++ METIS_TAC []) ``` hoelzl@35582 ` 1737` ``` ++ POP_ORW ``` hoelzl@35582 ` 1738` ``` ++ RW_TAC std_ss [REAL_SUM_IMAGE_THM, pred_setTheory.FINITE_COUNT] ``` hoelzl@35582 ` 1739` ``` ++ ONCE_REWRITE_TAC [(REWRITE_RULE [pred_setTheory.FINITE_COUNT] o ``` hoelzl@35582 ` 1740` ``` REWRITE_RULE [FINITE_DELETE] o Q.ISPEC `pred_set\$count n' DELETE x`) REAL_SUM_IMAGE_IN_IF] ``` hoelzl@35582 ` 1741` ``` ++ RW_TAC real_ss [IN_DELETE, indicator_fn_def, IN_INTER, IN_SING, IN_PREIMAGE] ``` hoelzl@35582 ` 1742` ``` ++ `(\x'. (if x' \ pred_set\$count n' \ ~(x' = x) then ``` hoelzl@35582 ` 1743` ``` enumerate (IMAGE (neg_part f) (space m)) x' * ``` hoelzl@35582 ` 1744` ``` (if enumerate (IMAGE (neg_part f) (space m)) x = ``` hoelzl@35582 ` 1745` ``` enumerate (IMAGE (neg_part f) (space m)) x' ``` hoelzl@35582 ` 1746` ``` then 1 else 0) else 0)) = (\x. 0)` ``` hoelzl@35582 ` 1747` ``` by (RW_TAC std_ss [FUN_EQ_THM] ++ RW_TAC real_ss [] ++ METIS_TAC []) ``` hoelzl@35582 ` 1748` ``` ++ POP_ORW ``` hoelzl@35582 ` 1749` ``` ++ RW_TAC real_ss [REAL_SUM_IMAGE_0, pred_setTheory.FINITE_COUNT, FINITE_DELETE]) ``` hoelzl@35582 ` 1750` ``` ++ FULL_SIMP_TAC real_ss [IN_IMAGE, indicator_fn_def, IN_INTER, IN_PREIMAGE, IN_SING] ``` hoelzl@35582 ` 1751` ``` >> RW_TAC real_ss [REAL_SUM_IMAGE_0, pred_setTheory.FINITE_COUNT, FINITE_DELETE] ``` hoelzl@35582 ` 1752` ``` ++ ONCE_REWRITE_TAC [(REWRITE_RULE [pred_setTheory.FINITE_COUNT] o Q.ISPEC `pred_set\$count n'`) ``` hoelzl@35582 ` 1753` ``` REAL_SUM_IMAGE_IN_IF] ``` hoelzl@35582 ` 1754` ``` ++ `(\x. (if x \ pred_set\$count n' then ``` hoelzl@35582 ` 1755` ``` (\i. enumerate (IMAGE (neg_part f) (space m)) i * ``` hoelzl@35582 ` 1756` ``` (if (neg_part f t = enumerate (IMAGE (neg_part f) (space m)) i) \ ``` hoelzl@35582 ` 1757` ``` t \ space m then 1 else 0)) x else 0)) = (\x. 0)` ``` hoelzl@35582 ` 1758` ``` by (RW_TAC std_ss [FUN_EQ_THM] ++ RW_TAC real_ss [] ++ METIS_TAC []) ``` hoelzl@35582 ` 1759` ``` ++ POP_ORW ``` hoelzl@35582 ` 1760` ``` ++ RW_TAC real_ss [REAL_SUM_IMAGE_0, pred_setTheory.FINITE_COUNT]) ``` hoelzl@35582 ` 1761` ``` ++ POP_ORW ``` hoelzl@35582 ` 1762` ``` ++ `((\r. r * measure m (PREIMAGE (neg_part f) {r} \ space m)) o ``` hoelzl@35582 ` 1763` ``` enumerate (IMAGE (neg_part f) (space m))) = ``` hoelzl@35582 ` 1764` ``` (\i. (\i. enumerate (IMAGE (neg_part f) (space m)) i) i * ``` hoelzl@35582 ` 1765` ``` measure m ((\i. ``` hoelzl@35582 ` 1766` ``` PREIMAGE (neg_part f) ``` hoelzl@35582 ` 1767` ``` {enumerate (IMAGE (neg_part f) (space m)) i} \ ``` hoelzl@35582 ` 1768` ``` space m) i))` ``` hoelzl@35582 ` 1769` ``` by (RW_TAC std_ss [FUN_EQ_THM, o_DEF] ++ RW_TAC real_ss []) ``` hoelzl@35582 ` 1770` ``` ++ POP_ORW ``` hoelzl@35582 ` 1771` ``` ++ MATCH_MP_TAC psfis_intro ``` hoelzl@35582 ` 1772` ``` ++ ASM_SIMP_TAC std_ss [pred_setTheory.FINITE_COUNT] ``` hoelzl@35582 ` 1773` ``` ++ REVERSE CONJ_TAC ``` hoelzl@35582 ` 1774` ``` >> (FULL_SIMP_TAC real_ss [IN_IMAGE, neg_part_def] ``` hoelzl@35582 ` 1775` ``` ++ METIS_TAC [REAL_LE_REFL, REAL_LE_NEGTOTAL]) ``` hoelzl@35582 ` 1776` ``` ++ `(neg_part f) \ borel_measurable (space m, sets m)` ``` hoelzl@35582 ` 1777` ``` by METIS_TAC [pos_part_neg_part_borel_measurable] ``` hoelzl@35582 ` 1778` ``` ++ REPEAT STRIP_TAC ``` hoelzl@35582 ` 1779` ``` ++ `PREIMAGE (neg_part f) {enumerate (IMAGE (neg_part f) (space m)) i} \ space m = ``` hoelzl@35582 ` 1780` ``` {w | w \ space m \ ((neg_part f) w = (\w. enumerate (IMAGE (neg_part f) (space m)) i) w)}` ``` hoelzl@35582 ` 1781` ``` by (ONCE_REWRITE_TAC [EXTENSION] ++ RW_TAC std_ss [GSPECIFICATION, IN_INTER, IN_PREIMAGE, IN_SING] ``` hoelzl@35582 ` 1782` ``` ++ DECIDE_TAC) ``` hoelzl@35582 ` 1783` ``` ++ POP_ORW ``` hoelzl@35582 ` 1784` ``` ++ MATCH_MP_TAC borel_measurable_eq_borel_measurable ``` hoelzl@35582 ` 1785` ``` ++ METIS_TAC [borel_measurable_const, measure_space_def]); ``` hoelzl@35582 ` 1786` ```*) ``` hoelzl@35582 ` 1787` hoelzl@35582 ` 1788` ```end ``` hoelzl@35582 ` 1789` hoelzl@35582 ` 1790` `end`