# HG changeset patch # User hoelzl # Date 1268044255 -3600 # Node ID f1315bbf1bc9b91d27b59142e2b9a3b72d7f9538 # Parent 74e4542d0a4a04175869988f1d59c61dbc5cb7ed Moved theorems in Lebesgue to the right places diff -r 74e4542d0a4a -r f1315bbf1bc9 src/HOL/Probability/Borel.thy --- a/src/HOL/Probability/Borel.thy Mon Mar 08 09:38:59 2010 +0100 +++ b/src/HOL/Probability/Borel.thy Mon Mar 08 11:30:55 2010 +0100 @@ -15,11 +15,6 @@ definition indicator_fn where "indicator_fn s = (\x. if x \ s then 1 else (0::real))" -definition mono_convergent where - "mono_convergent u f s \ - (\x\s. incseq (\n. u n x)) \ - (\x \ s. (\i. u i x) ----> f x)" - lemma in_borel_measurable: "f \ borel_measurable M \ sigma_algebra M \ @@ -375,6 +370,95 @@ by (fast intro: borel_measurable_add_borel_measurable borel_measurable_uminus_borel_measurable f g) +lemma (in measure_space) borel_measurable_setsum_borel_measurable: + assumes s: "finite s" + shows "(!!i. i \ s ==> f i \ borel_measurable M) \ (\x. setsum (\i. f i x) s) \ borel_measurable M" using s +proof (induct s) + case empty + thus ?case + by (simp add: borel_measurable_const) +next + case (insert x s) + thus ?case + by (auto simp add: borel_measurable_add_borel_measurable) +qed + +lemma (in measure_space) borel_measurable_cong: + assumes "\ w. w \ space M \ f w = g w" + shows "f \ borel_measurable M \ g \ borel_measurable M" +using assms unfolding in_borel_measurable by (simp cong: vimage_inter_cong) + +lemma (in measure_space) borel_measurable_inverse: + assumes "f \ borel_measurable M" + shows "(\x. inverse (f x)) \ borel_measurable M" + unfolding borel_measurable_ge_iff +proof (safe, rule linorder_cases) + fix a :: real assume "0 < a" + { fix w + from `0 < a` have "a \ inverse (f w) \ 0 < f w \ f w \ 1 / a" + by (metis inverse_eq_divide inverse_inverse_eq le_imp_inverse_le + linorder_not_le real_le_refl real_le_trans real_less_def + xt1(7) zero_less_divide_1_iff) } + hence "{w \ space M. a \ inverse (f w)} = + {w \ space M. 0 < f w} \ {w \ space M. f w \ 1 / a}" by auto + with Int assms[unfolded borel_measurable_gr_iff] + assms[unfolded borel_measurable_le_iff] + show "{w \ space M. a \ inverse (f w)} \ sets M" by simp +next + fix a :: real assume "0 = a" + { fix w have "a \ inverse (f w) \ 0 \ f w" + unfolding `0 = a`[symmetric] by auto } + thus "{w \ space M. a \ inverse (f w)} \ sets M" + using assms[unfolded borel_measurable_ge_iff] by simp +next + fix a :: real assume "a < 0" + { fix w + from `a < 0` have "a \ inverse (f w) \ f w \ 1 / a \ 0 \ f w" + apply (cases "0 \ f w") + apply (metis inverse_eq_divide linorder_not_le xt1(8) xt1(9) + zero_le_divide_1_iff) + apply (metis inverse_eq_divide inverse_inverse_eq inverse_le_imp_le_neg + linorder_not_le real_le_refl real_le_trans) + done } + hence "{w \ space M. a \ inverse (f w)} = + {w \ space M. f w \ 1 / a} \ {w \ space M. 0 \ f w}" by auto + with Un assms[unfolded borel_measurable_ge_iff] + assms[unfolded borel_measurable_le_iff] + show "{w \ space M. a \ inverse (f w)} \ sets M" by simp +qed + +lemma (in measure_space) borel_measurable_divide: + assumes "f \ borel_measurable M" + and "g \ borel_measurable M" + shows "(\x. f x / g x) \ borel_measurable M" + unfolding field_divide_inverse + by (rule borel_measurable_inverse borel_measurable_times_borel_measurable assms)+ + + +section "Monotone convergence" + +definition mono_convergent where + "mono_convergent u f s \ + (\x\s. incseq (\n. u n x)) \ + (\x \ s. (\i. u i x) ----> f x)" + +definition "upclose f g x = max (f x) (g x)" + +primrec mon_upclose where +"mon_upclose 0 u = u 0" | +"mon_upclose (Suc n) u = upclose (u (Suc n)) (mon_upclose n u)" + +lemma mono_convergentD: + assumes "mono_convergent u f s" and "x \ s" + shows "incseq (\n. u n x)" and "(\i. u i x) ----> f x" + using assms unfolding mono_convergent_def by auto + +lemma mono_convergentI: + assumes "\x. x \ s \ incseq (\n. u n x)" + assumes "\x. x \ s \ (\i. u i x) ----> f x" + shows "mono_convergent u f s" + using assms unfolding mono_convergent_def by auto + lemma (in measure_space) mono_convergent_borel_measurable: assumes u: "!!n. u n \ borel_measurable M" assumes mc: "mono_convergent u f (space M)" @@ -409,44 +493,11 @@ by (auto simp add: borel_measurable_le_iff) qed -lemma (in measure_space) borel_measurable_setsum_borel_measurable: - assumes s: "finite s" - shows "(!!i. i \ s ==> f i \ borel_measurable M) \ (\x. setsum (\i. f i x) s) \ borel_measurable M" using s -proof (induct s) - case empty - thus ?case - by (simp add: borel_measurable_const) -next - case (insert x s) - thus ?case - by (auto simp add: borel_measurable_add_borel_measurable) -qed - -section "Monotone convergence" - -lemma mono_convergentD: - assumes "mono_convergent u f s" and "x \ s" - shows "incseq (\n. u n x)" and "(\i. u i x) ----> f x" - using assms unfolding mono_convergent_def by auto - - -lemma mono_convergentI: - assumes "\x. x \ s \ incseq (\n. u n x)" - assumes "\x. x \ s \ (\i. u i x) ----> f x" - shows "mono_convergent u f s" - using assms unfolding mono_convergent_def by auto - lemma mono_convergent_le: assumes "mono_convergent u f s" and "t \ s" shows "u n t \ f t" using mono_convergentD[OF assms] by (auto intro!: incseq_le) -definition "upclose f g x = max (f x) (g x)" - -primrec mon_upclose where -"mon_upclose 0 u = u 0" | -"mon_upclose (Suc n) u = upclose (u (Suc n)) (mon_upclose n u)" - lemma mon_upclose_ex: fixes u :: "nat \ 'a \ ('b\linorder)" shows "\n \ m. mon_upclose m u x = u n x" @@ -561,4 +612,19 @@ qed qed +lemma mono_conv_outgrow: + assumes "incseq x" "x ----> y" "z < y" + shows "\b. \ a \ b. z < x a" +using assms +proof - + from assms have "y - z > 0" by simp + hence A: "\n. (\ m \ n. \ x m + - y \ < y - z)" using assms + unfolding incseq_def LIMSEQ_def dist_real_def real_diff_def + by simp + have "\m. x m \ y" using incseq_le assms by auto + hence B: "\m. \ x m + - y \ = y - x m" + by (metis abs_if abs_minus_add_cancel less_iff_diff_less_0 linorder_not_le real_diff_def) + from A B show ?thesis by auto +qed + end diff -r 74e4542d0a4a -r f1315bbf1bc9 src/HOL/Probability/Lebesgue.thy --- a/src/HOL/Probability/Lebesgue.thy Mon Mar 08 09:38:59 2010 +0100 +++ b/src/HOL/Probability/Lebesgue.thy Mon Mar 08 11:30:55 2010 +0100 @@ -25,9 +25,58 @@ shows "nonneg (neg_part f)" unfolding nonneg_def neg_part_def min_def by auto +lemma (in measure_space) + assumes "f \ borel_measurable M" + shows pos_part_borel_measurable: "pos_part f \ borel_measurable M" + and neg_part_borel_measurable: "neg_part f \ borel_measurable M" +using assms +proof - + { fix a :: real + { assume asm: "0 \ a" + from asm have pp: "\ w. (pos_part f w \ a) = (f w \ a)" unfolding pos_part_def by auto + have "{w | w. w \ space M \ f w \ a} \ sets M" + unfolding pos_part_def using assms borel_measurable_le_iff by auto + hence "{w . w \ space M \ pos_part f w \ a} \ sets M" using pp by auto } + moreover have "a < 0 \ {w \ space M. pos_part f w \ a} \ sets M" + unfolding pos_part_def using empty_sets by auto + ultimately have "{w . w \ space M \ pos_part f w \ a} \ sets M" + using le_less_linear by auto + } hence pos: "pos_part f \ borel_measurable M" using borel_measurable_le_iff by auto + { fix a :: real + { assume asm: "0 \ a" + from asm have pp: "\ w. (neg_part f w \ a) = (f w \ - a)" unfolding neg_part_def by auto + have "{w | w. w \ space M \ f w \ - a} \ sets M" + unfolding neg_part_def using assms borel_measurable_ge_iff by auto + hence "{w . w \ space M \ neg_part f w \ a} \ sets M" using pp by auto } + moreover have "a < 0 \ {w \ space M. neg_part f w \ a} = {}" unfolding neg_part_def by auto + moreover hence "a < 0 \ {w \ space M. neg_part f w \ a} \ sets M" by (simp only: empty_sets) + ultimately have "{w . w \ space M \ neg_part f w \ a} \ sets M" + using le_less_linear by auto + } hence neg: "neg_part f \ borel_measurable M" using borel_measurable_le_iff by auto + from pos neg show "pos_part f \ borel_measurable M" and "neg_part f \ borel_measurable M" by auto +qed + +lemma (in measure_space) pos_part_neg_part_borel_measurable_iff: + "f \ borel_measurable M \ + pos_part f \ borel_measurable M \ neg_part f \ borel_measurable M" +proof - + { fix x + have "f x = pos_part f x - neg_part f x" + unfolding pos_part_def neg_part_def unfolding max_def min_def + by auto } + hence "(\ x. f x) = (\ x. pos_part f x - neg_part f x)" by auto + hence "f = (\ x. pos_part f x - neg_part f x)" by blast + from pos_part_borel_measurable[of f] neg_part_borel_measurable[of f] + borel_measurable_diff_borel_measurable[of "pos_part f" "neg_part f"] + this + show ?thesis by auto +qed + context measure_space begin +section "Simple discrete step function" + definition "pos_simple f = { (s :: nat set, a, x). @@ -40,29 +89,6 @@ definition "psfis f = pos_simple_integral ` (pos_simple f)" -definition - "nnfis f = { y. \u x. mono_convergent u f (space M) \ - (\n. x n \ psfis (u n)) \ x ----> y }" - -definition - "integrable f \ (\x. x \ nnfis (pos_part f)) \ (\y. y \ nnfis (neg_part f))" - -definition - "integral f = (THE i :: real. i \ nnfis (pos_part f)) - (THE j. j \ nnfis (neg_part f))" - -definition - "enumerate s \ SOME f. bij_betw f UNIV s" - -definition - "countable_space_integral f \ - let e = enumerate (f ` space M) in - suminf (\r. e r * measure M (f -` {e r} \ space M))" - -definition - "RN_deriv v \ SOME f. measure_space (M\measure := v\) \ - f \ borel_measurable M \ - (\a \ sets M. (integral (\x. f x * indicator_fn a x) = v a))" - lemma pos_simpleE[consumes 1]: assumes ps: "(s, a, x) \ pos_simple f" obtains "finite s" and "nonneg f" and "nonneg x" @@ -105,6 +131,11 @@ shows "psfis f = psfis g" unfolding psfis_def using pos_simple_cong[OF assms] by simp +lemma psfis_0: "0 \ psfis (\x. 0)" + unfolding psfis_def pos_simple_def pos_simple_integral_def + by (auto simp: nonneg_def + intro: image_eqI[where x="({0}, (\i. space M), (\i. 0))"]) + lemma pos_simple_setsum_indicator_fn: assumes ps: "(s, a, x) \ pos_simple f" and "t \ space M" @@ -121,28 +152,7 @@ using `i \ s` by simp qed -lemma (in measure_space) measure_setsum_split: - assumes "finite r" and "a \ sets M" and br_in_M: "b ` r \ sets M" - assumes "(\i \ r. b i) = space M" - assumes "disjoint_family_on b r" - shows "(measure M) a = (\ i \ r. measure M (a \ (b i)))" -proof - - have *: "measure M a = measure M (\i \ r. a \ b i)" - using assms by auto - show ?thesis unfolding * - proof (rule measure_finitely_additive''[symmetric]) - show "finite r" using `finite r` by auto - { fix i assume "i \ r" - hence "b i \ sets M" using br_in_M by auto - thus "a \ b i \ sets M" using `a \ sets M` by auto - } - show "disjoint_family_on (\i. a \ b i) r" - using `disjoint_family_on b r` - unfolding disjoint_family_on_def by auto - qed -qed - -lemma (in measure_space) pos_simple_common_partition: +lemma pos_simple_common_partition: assumes psf: "(s, a, x) \ pos_simple f" assumes psg: "(s', b, y) \ pos_simple g" obtains z z' c k where "(k, c, z) \ pos_simple f" "(k, c, z') \ pos_simple g" @@ -229,7 +239,7 @@ qed qed -lemma (in measure_space) pos_simple_integral_equal: +lemma pos_simple_integral_equal: assumes psx: "(s, a, x) \ pos_simple f" assumes psy: "(s', b, y) \ pos_simple f" shows "pos_simple_integral (s, a, x) = pos_simple_integral (s', b, y)" @@ -269,7 +279,7 @@ finally show "?left = ?right" . qed -lemma (in measure_space)psfis_present: +lemma psfis_present: assumes "A \ psfis f" assumes "B \ psfis g" obtains z z' c k where @@ -295,7 +305,7 @@ qed qed -lemma (in measure_space) pos_simple_integral_add: +lemma pos_simple_integral_add: assumes "(s, a, x) \ pos_simple f" assumes "(s', b, y) \ pos_simple g" obtains s'' c z where @@ -468,70 +478,6 @@ thus ?thesis using r unfolding psfis_def image_def by auto qed -lemma pos_simple_integral_setsum_image: - assumes "finite P" - assumes "\ i. i \ P \ (s i, a i, x i) \ pos_simple (f i)" - obtains s' a' x' where - "(s', a', x') \ pos_simple (\t. (\ i \ P. f i t))" - "pos_simple_integral (s', a', x') = (\ i \ P. pos_simple_integral (s i, a i, x i))" -using assms that -proof (induct P arbitrary:thesis rule:finite.induct) - case emptyI note asms = this - def s' == "{0 :: nat}" - def a' == "\ x. if x = (0 :: nat) then space M else {}" - def x' == "\ x :: nat. (0 :: real)" - have "(s', a', x') \ pos_simple (\ t. 0)" - unfolding s'_def a'_def x'_def pos_simple_def nonneg_def by auto - moreover have "pos_simple_integral (s', a', x') = 0" - unfolding s'_def a'_def x'_def pos_simple_integral_def by auto - ultimately show ?case using asms by auto -next - - case (insertI P c) note asms = this - then obtain s' a' x' where - sax: "(s', a', x') \ pos_simple (\t. \i\P. f i t)" - "pos_simple_integral (s', a', x') = - (\i\P. pos_simple_integral (s i, a i, x i))" - by auto - - { assume "c \ P" - hence "P = insert c P" by auto - hence thesis using asms sax by auto - } - moreover - { assume "c \ P" - from asms obtain s'' a'' x'' where - sax': "s'' = s c" "a'' = a c" "x'' = x c" - "(s'', a'', x'') \ pos_simple (f c)" by auto - from sax sax' obtain k :: "nat \ bool" and b :: "nat \ 'a \ bool" and z :: "nat \ real" where - tybbie: - "(k, b, z) \ pos_simple (\t. ((\i\P. f i t) + f c t))" - "(pos_simple_integral (s', a', x') + - pos_simple_integral (s'', a'', x'') = - pos_simple_integral (k, b, z))" - using pos_simple_integral_add by blast - - from tybbie have - "pos_simple_integral (k, b, z) = - pos_simple_integral (s', a', x') + - pos_simple_integral (s'', a'', x'')" by simp - also have "\ = (\ i \ P. pos_simple_integral (s i, a i, x i)) - + pos_simple_integral (s c, a c, x c)" - using sax sax' by auto - also have "\ = (\ i \ insert c P. pos_simple_integral (s i, a i, x i))" - using asms `c \ P` by auto - finally have A: "pos_simple_integral (k, b, z) = (\ i \ insert c P. pos_simple_integral (s i, a i, x i))" - by simp - - have "\ t. (\ i \ P. f i t) + f c t = (\ i \ insert c P. f i t)" - using `c \ P` `finite P` by auto - hence B: "(k, b, z) \ pos_simple (\ t. (\ i \ insert c P. f i t))" - using tybbie by simp - - from A B have thesis using asms by auto - } ultimately show thesis by blast -qed - lemma psfis_setsum_image: assumes "finite P" assumes "\i. i \ P \ a i \ psfis (f i)" @@ -577,57 +523,6 @@ unfolding psfis_def pos_simple_integral_def image_def pos_simple_def nonneg_def using positive[unfolded positive_def] by (auto intro!:setsum_nonneg mult_nonneg_nonneg) -lemma pos_part_neg_part_borel_measurable: - assumes "f \ borel_measurable M" - shows "pos_part f \ borel_measurable M" and "neg_part f \ borel_measurable M" -using assms -proof - - { fix a :: real - { assume asm: "0 \ a" - from asm have pp: "\ w. (pos_part f w \ a) = (f w \ a)" unfolding pos_part_def by auto - have "{w | w. w \ space M \ f w \ a} \ sets M" - unfolding pos_part_def using assms borel_measurable_le_iff by auto - hence "{w . w \ space M \ pos_part f w \ a} \ sets M" using pp by auto } - moreover have "a < 0 \ {w \ space M. pos_part f w \ a} \ sets M" - unfolding pos_part_def using empty_sets by auto - ultimately have "{w . w \ space M \ pos_part f w \ a} \ sets M" - using le_less_linear by auto - } hence pos: "pos_part f \ borel_measurable M" using borel_measurable_le_iff by auto - { fix a :: real - { assume asm: "0 \ a" - from asm have pp: "\ w. (neg_part f w \ a) = (f w \ - a)" unfolding neg_part_def by auto - have "{w | w. w \ space M \ f w \ - a} \ sets M" - unfolding neg_part_def using assms borel_measurable_ge_iff by auto - hence "{w . w \ space M \ neg_part f w \ a} \ sets M" using pp by auto } - moreover have "a < 0 \ {w \ space M. neg_part f w \ a} = {}" unfolding neg_part_def by auto - moreover hence "a < 0 \ {w \ space M. neg_part f w \ a} \ sets M" by (simp only: empty_sets) - ultimately have "{w . w \ space M \ neg_part f w \ a} \ sets M" - using le_less_linear by auto - } hence neg: "neg_part f \ borel_measurable M" using borel_measurable_le_iff by auto - from pos neg show "pos_part f \ borel_measurable M" and "neg_part f \ borel_measurable M" by auto -qed - -lemma pos_part_neg_part_borel_measurable_iff: - "f \ borel_measurable M \ - pos_part f \ borel_measurable M \ neg_part f \ borel_measurable M" -proof - - { fix x - have "f x = pos_part f x - neg_part f x" - unfolding pos_part_def neg_part_def unfolding max_def min_def - by auto } - hence "(\ x. f x) = (\ x. pos_part f x - neg_part f x)" by auto - hence "f = (\ x. pos_part f x - neg_part f x)" by blast - from pos_part_neg_part_borel_measurable[of f] - borel_measurable_diff_borel_measurable[of "pos_part f" "neg_part f"] - this - show ?thesis by auto -qed - -lemma borel_measurable_cong: - assumes "\ w. w \ space M \ f w = g w" - shows "f \ borel_measurable M \ g \ borel_measurable M" -using assms unfolding in_borel_measurable by (simp cong: vimage_inter_cong) - lemma psfis_borel_measurable: assumes "a \ psfis f" shows "f \ borel_measurable M" @@ -654,21 +549,6 @@ show ?thesis by simp qed -lemma mono_conv_outgrow: - assumes "incseq x" "x ----> y" "z < y" - shows "\b. \ a \ b. z < x a" -using assms -proof - - from assms have "y - z > 0" by simp - hence A: "\n. (\ m \ n. \ x m + - y \ < y - z)" using assms - unfolding incseq_def LIMSEQ_def dist_real_def real_diff_def - by simp - have "\m. x m \ y" using incseq_le assms by auto - hence B: "\m. \ x m + - y \ = y - x m" - by (metis abs_if abs_minus_add_cancel less_iff_diff_less_0 linorder_not_le real_diff_def) - from A B show ?thesis by auto -qed - lemma psfis_mono_conv_mono: assumes mono: "mono_convergent u f (space M)" and ps_u: "\n. x n \ psfis (u n)" @@ -679,7 +559,6 @@ proof (rule field_le_mult_one_interval) fix z :: real assume "0 < z" and "z < 1" hence "0 \ z" by auto -(* def B' \ "\n. {w \ space M. z * s w <= u n w}" *) let "?B' n" = "{w \ space M. z * s w <= u n w}" have "incseq x" unfolding incseq_def @@ -783,6 +662,12 @@ qed qed +section "Continuous posititve integration" + +definition + "nnfis f = { y. \u x. mono_convergent u f (space M) \ + (\n. x n \ psfis (u n)) \ x ----> y }" + lemma psfis_nnfis: "a \ psfis f \ a \ nnfis f" unfolding nnfis_def mono_convergent_def incseq_def @@ -1136,11 +1021,6 @@ show ?thesis unfolding nnfis_def by auto qed -lemma psfis_0: "0 \ psfis (\x. 0)" - unfolding psfis_def pos_simple_def pos_simple_integral_def - by (auto simp: nonneg_def - intro: image_eqI[where x="({0}, (\i. space M), (\i. 0))"]) - lemma the_nnfis[simp]: "a \ nnfis f \ (THE a. a \ nnfis f) = a" by (auto intro: the_equality nnfis_unique) @@ -1158,6 +1038,14 @@ show ?thesis by safe qed +section "Lebesgue Integral" + +definition + "integrable f \ (\x. x \ nnfis (pos_part f)) \ (\y. y \ nnfis (neg_part f))" + +definition + "integral f = (THE i :: real. i \ nnfis (pos_part f)) - (THE j. j \ nnfis (neg_part f))" + lemma integral_cong: assumes cong: "\x. x \ space M \ f x = g x" shows "integral f = integral g" @@ -1203,7 +1091,7 @@ (is "\x. x \ nnfis ?pp \ _") proof (rule nnfis_dom_conv) show "?pp \ borel_measurable M" - using borel by (rule pos_part_neg_part_borel_measurable) + using borel by (rule pos_part_borel_measurable neg_part_borel_measurable) show "a + b \ nnfis (\t. f t + g t)" using assms by (rule nnfis_add) fix t assume "t \ space M" with assms nnfis_add assms[THEN nnfis_pos_on_mspace[OF _ this]] @@ -1217,7 +1105,7 @@ (is "\x. x \ nnfis ?np \ _") proof (rule nnfis_dom_conv) show "?np \ borel_measurable M" - using borel by (rule pos_part_neg_part_borel_measurable) + using borel by (rule pos_part_borel_measurable neg_part_borel_measurable) show "a + b \ nnfis (\t. f t + g t)" using assms by (rule nnfis_add) fix t assume "t \ space M" with assms nnfis_add assms[THEN nnfis_pos_on_mspace[OF _ this]] @@ -1419,6 +1307,8 @@ by (auto intro!: mult_imp_le_div_pos[OF `0 < a ^ n`], simp add: real_mult_commute) qed +section "Lebesgue integration on finite space" + lemma integral_finite_on_sets: assumes "f \ borel_measurable M" and "finite (space M)" and "a \ sets M" shows "integral (\x. f x * indicator_fn a x) = @@ -1489,51 +1379,12 @@ qed (auto intro!: image_eqI inj_onI) qed -lemma borel_measurable_inverse: - assumes "f \ borel_measurable M" - shows "(\x. inverse (f x)) \ borel_measurable M" - unfolding borel_measurable_ge_iff -proof (safe, rule linorder_cases) - fix a :: real assume "0 < a" - { fix w - from `0 < a` have "a \ inverse (f w) \ 0 < f w \ f w \ 1 / a" - by (metis inverse_eq_divide inverse_inverse_eq le_imp_inverse_le - linorder_not_le real_le_refl real_le_trans real_less_def - xt1(7) zero_less_divide_1_iff) } - hence "{w \ space M. a \ inverse (f w)} = - {w \ space M. 0 < f w} \ {w \ space M. f w \ 1 / a}" by auto - with Int assms[unfolded borel_measurable_gr_iff] - assms[unfolded borel_measurable_le_iff] - show "{w \ space M. a \ inverse (f w)} \ sets M" by simp -next - fix a :: real assume "0 = a" - { fix w have "a \ inverse (f w) \ 0 \ f w" - unfolding `0 = a`[symmetric] by auto } - thus "{w \ space M. a \ inverse (f w)} \ sets M" - using assms[unfolded borel_measurable_ge_iff] by simp -next - fix a :: real assume "a < 0" - { fix w - from `a < 0` have "a \ inverse (f w) \ f w \ 1 / a \ 0 \ f w" - apply (cases "0 \ f w") - apply (metis inverse_eq_divide linorder_not_le xt1(8) xt1(9) - zero_le_divide_1_iff) - apply (metis inverse_eq_divide inverse_inverse_eq inverse_le_imp_le_neg - linorder_not_le real_le_refl real_le_trans) - done } - hence "{w \ space M. a \ inverse (f w)} = - {w \ space M. f w \ 1 / a} \ {w \ space M. 0 \ f w}" by auto - with Un assms[unfolded borel_measurable_ge_iff] - assms[unfolded borel_measurable_le_iff] - show "{w \ space M. a \ inverse (f w)} \ sets M" by simp -qed +section "Radon–Nikodym derivative" -lemma borel_measurable_divide: - assumes "f \ borel_measurable M" - and "g \ borel_measurable M" - shows "(\x. f x / g x) \ borel_measurable M" - unfolding field_divide_inverse - by (rule borel_measurable_inverse borel_measurable_times_borel_measurable assms)+ +definition + "RN_deriv v \ SOME f. measure_space (M\measure := v\) \ + f \ borel_measurable M \ + (\a \ sets M. (integral (\x. f x * indicator_fn a x) = v a))" lemma RN_deriv_finite_singleton: fixes v :: "'a set \ real" @@ -1577,6 +1428,11 @@ using `measure M {x} \ 0` by (simp add: eq_divide_eq) qed fact +section "Lebesgue integration on countable spaces" + +definition + "enumerate s \ SOME f. bij_betw f UNIV s" + lemma countable_space_integral_reduce: assumes "positive M (measure M)" and "f \ borel_measurable M" and "countable (f ` space M)" diff -r 74e4542d0a4a -r f1315bbf1bc9 src/HOL/Probability/Measure.thy --- a/src/HOL/Probability/Measure.thy Mon Mar 08 09:38:59 2010 +0100 +++ b/src/HOL/Probability/Measure.thy Mon Mar 08 11:30:55 2010 +0100 @@ -997,4 +997,25 @@ \ measure_space M" by (rule measure_down [OF sigma_algebra.finite_additivity_sufficient], auto) +lemma (in measure_space) measure_setsum_split: + assumes "finite r" and "a \ sets M" and br_in_M: "b ` r \ sets M" + assumes "(\i \ r. b i) = space M" + assumes "disjoint_family_on b r" + shows "(measure M) a = (\ i \ r. measure M (a \ (b i)))" +proof - + have *: "measure M a = measure M (\i \ r. a \ b i)" + using assms by auto + show ?thesis unfolding * + proof (rule measure_finitely_additive''[symmetric]) + show "finite r" using `finite r` by auto + { fix i assume "i \ r" + hence "b i \ sets M" using br_in_M by auto + thus "a \ b i \ sets M" using `a \ sets M` by auto + } + show "disjoint_family_on (\i. a \ b i) r" + using `disjoint_family_on b r` + unfolding disjoint_family_on_def by auto + qed +qed + end \ No newline at end of file