# HG changeset patch # User hoelzl # Date 1291298241 -3600 # Node ID 1ef85f4e709767f2f0dd2b452688d7ac37e3afe9 # Parent 7c556a9240deef738e272b3e6e4ef1f963349a35 Shorter definition for positive_integral. diff -r 7c556a9240de -r 1ef85f4e7097 src/HOL/Probability/Lebesgue_Integration.thy --- a/src/HOL/Probability/Lebesgue_Integration.thy Thu Dec 02 14:34:58 2010 +0100 +++ b/src/HOL/Probability/Lebesgue_Integration.thy Thu Dec 02 14:57:21 2010 +0100 @@ -848,52 +848,13 @@ section "Continuous posititve integration" definition (in measure_space) - "positive_integral f = - SUPR {g. simple_function g \ g \ f \ \ \ g`space M} simple_integral" - -lemma (in measure_space) positive_integral_cong_measure: - assumes "\A. A \ sets M \ \ A = \ A" - shows "measure_space.positive_integral M \ f = positive_integral f" -proof - - interpret v: measure_space M \ - by (rule measure_space_cong) fact - with assms show ?thesis - unfolding positive_integral_def v.positive_integral_def SUPR_def - by (auto intro!: arg_cong[where f=Sup] image_cong - simp: simple_integral_cong_measure[of \]) -qed - -lemma (in measure_space) positive_integral_alt1: - "positive_integral f = - (SUP g : {g. simple_function g \ (\x\space M. g x \ f x \ g x \ \)}. simple_integral g)" - unfolding positive_integral_def SUPR_def -proof (safe intro!: arg_cong[where f=Sup]) - fix g let ?g = "\x. if x \ space M then g x else f x" - assume "simple_function g" "\x\space M. g x \ f x \ g x \ \" - hence "?g \ f" "simple_function ?g" "simple_integral g = simple_integral ?g" - "\ \ g`space M" - unfolding le_fun_def by (auto cong: simple_function_cong simple_integral_cong) - thus "simple_integral g \ simple_integral ` {g. simple_function g \ g \ f \ \ \ g`space M}" - by auto -next - fix g assume "simple_function g" "g \ f" "\ \ g`space M" - hence "simple_function g" "\x\space M. g x \ f x \ g x \ \" - by (auto simp add: le_fun_def image_iff) - thus "simple_integral g \ simple_integral ` {g. simple_function g \ (\x\space M. g x \ f x \ g x \ \)}" - by auto -qed - -lemma image_set_cong: - assumes A: "\x. x \ A \ \y\B. f x = g y" - assumes B: "\y. y \ B \ \x\A. g y = f x" - shows "f ` A = g ` B" - using assms by blast + "positive_integral f = SUPR {g. simple_function g \ g \ f} simple_integral" lemma (in measure_space) positive_integral_alt: "positive_integral f = - (SUP g : {g. simple_function g \ g \ f}. simple_integral g)" (is "_ = ?alt") + (SUPR {g. simple_function g \ g \ f \ \ \ g`space M} simple_integral)" (is "_ = ?alt") proof (rule antisym SUP_leI) - show "?alt \ positive_integral f" unfolding positive_integral_def + show "positive_integral f \ ?alt" unfolding positive_integral_def proof (safe intro!: SUP_leI) fix g assume g: "simple_function g" "g \ f" let ?G = "g -` {\} \ space M" @@ -949,6 +910,38 @@ qed qed (auto intro!: SUP_subset simp: positive_integral_def) +lemma (in measure_space) positive_integral_cong_measure: + assumes "\A. A \ sets M \ \ A = \ A" + shows "measure_space.positive_integral M \ f = positive_integral f" +proof - + interpret v: measure_space M \ + by (rule measure_space_cong) fact + with assms show ?thesis + unfolding positive_integral_def v.positive_integral_def SUPR_def + by (auto intro!: arg_cong[where f=Sup] image_cong + simp: simple_integral_cong_measure[of \]) +qed + +lemma (in measure_space) positive_integral_alt1: + "positive_integral f = + (SUP g : {g. simple_function g \ (\x\space M. g x \ f x \ g x \ \)}. simple_integral g)" + unfolding positive_integral_alt SUPR_def +proof (safe intro!: arg_cong[where f=Sup]) + fix g let ?g = "\x. if x \ space M then g x else f x" + assume "simple_function g" "\x\space M. g x \ f x \ g x \ \" + hence "?g \ f" "simple_function ?g" "simple_integral g = simple_integral ?g" + "\ \ g`space M" + unfolding le_fun_def by (auto cong: simple_function_cong simple_integral_cong) + thus "simple_integral g \ simple_integral ` {g. simple_function g \ g \ f \ \ \ g`space M}" + by auto +next + fix g assume "simple_function g" "g \ f" "\ \ g`space M" + hence "simple_function g" "\x\space M. g x \ f x \ g x \ \" + by (auto simp add: le_fun_def image_iff) + thus "simple_integral g \ simple_integral ` {g. simple_function g \ (\x\space M. g x \ f x \ g x \ \)}" + by auto +qed + lemma (in measure_space) positive_integral_cong: assumes "\x. x \ space M \ f x = g x" shows "positive_integral f = positive_integral g" @@ -961,7 +954,7 @@ lemma (in measure_space) positive_integral_eq_simple_integral: assumes "simple_function f" shows "positive_integral f = simple_integral f" - unfolding positive_integral_alt + unfolding positive_integral_def proof (safe intro!: pinfreal_SUPI) fix g assume "simple_function g" "g \ f" with assms show "simple_integral g \ simple_integral f" @@ -1022,6 +1015,12 @@ shows "positive_integral u \ positive_integral v" using mono by (auto intro!: AE_cong positive_integral_mono_AE) +lemma image_set_cong: + assumes A: "\x. x \ A \ \y\B. f x = g y" + assumes B: "\y. y \ B \ \x\A. g y = f x" + shows "f ` A = g ` B" + using assms by blast + lemma (in measure_space) positive_integral_vimage: fixes g :: "'a \ pinfreal" and f :: "'d \ 'a" assumes f: "bij_betw f S (space M)" @@ -1034,17 +1033,14 @@ from assms have inv: "bij_betw (the_inv_into S f) (space M) S" by (rule bij_betw_the_inv_into) then have inv_fun: "the_inv_into S f \ space M \ S" unfolding bij_betw_def by auto - have surj: "f`S = space M" using f unfolding bij_betw_def by simp have inj: "inj_on f S" using f unfolding bij_betw_def by simp have inv_f: "\x. x \ space M \ f (the_inv_into S f x) = x" using f_the_inv_into_f[of f S] f unfolding bij_betw_def by auto - from simple_integral_vimage[OF assms, symmetric] have *: "simple_integral = T.simple_integral \ (\g. g \ f)" by (simp add: comp_def) - show ?thesis unfolding positive_integral_alt1 T.positive_integral_alt1 SUPR_def * image_compose proof (safe intro!: arg_cong[where f=Sup] image_set_cong, simp_all add: comp_def) @@ -1196,7 +1192,7 @@ by (auto intro!: SUP_leI positive_integral_mono) next show "positive_integral u \ (SUP i. positive_integral (f i))" - unfolding positive_integral_def[of u] + unfolding positive_integral_alt[of u] by (auto intro!: SUP_leI positive_integral_SUP_approx[OF assms]) qed qed @@ -1209,7 +1205,6 @@ proof - have "?u \ borel_measurable M" using borel_measurable_SUP[of _ f] assms by (simp add: SUPR_fun_expand) - show ?thesis proof (rule antisym) show "(SUP j. positive_integral (f j)) \ positive_integral ?u" @@ -1223,7 +1218,7 @@ using SUP_const[OF UNIV_not_empty] by (auto simp: restrict_def le_fun_def SUPR_fun_expand fun_eq_iff) ultimately have "positive_integral ru \ (SUP i. positive_integral (rf i))" - unfolding positive_integral_def[of ru] + unfolding positive_integral_alt[of ru] by (auto simp: le_fun_def intro!: SUP_leI positive_integral_SUP_approx) then show "positive_integral ?u \ (SUP i. positive_integral (f i))" unfolding ru_def rf_def by (simp cong: positive_integral_cong) @@ -1539,19 +1534,18 @@ apply (rule arg_cong[where f=Sup]) proof (auto simp add: image_iff simple_integral_restricted[OF `A \ sets M`]) fix g assume "simple_function (\x. g x * indicator A x)" - "g \ f" "\x\A. \ \ g x" - then show "\x. simple_function x \ x \ (\x. f x * indicator A x) \ (\y\space M. \ \ x y) \ + "g \ f" + then show "\x. simple_function x \ x \ (\x. f x * indicator A x) \ simple_integral (\x. g x * indicator A x) = simple_integral x" apply (rule_tac exI[of _ "\x. g x * indicator A x"]) by (auto simp: indicator_def le_fun_def) next fix g assume g: "simple_function g" "g \ (\x. f x * indicator A x)" - "\x\space M. \ \ g x" then have *: "(\x. g x * indicator A x) = g" "\x. g x * indicator A x = g x" "\x. g x \ f x" by (auto simp: le_fun_def fun_eq_iff indicator_def split: split_if_asm) - from g show "\x. simple_function (\xa. x xa * indicator A xa) \ x \ f \ (\xa\A. \ \ x xa) \ + from g show "\x. simple_function (\xa. x xa * indicator A xa) \ x \ f \ simple_integral g = simple_integral (\xa. x xa * indicator A xa)" using `A \ sets M`[THEN sets_into_space] apply (rule_tac exI[of _ "\x. g x * indicator A x"]) diff -r 7c556a9240de -r 1ef85f4e7097 src/HOL/Probability/Product_Measure.thy --- a/src/HOL/Probability/Product_Measure.thy Thu Dec 02 14:34:58 2010 +0100 +++ b/src/HOL/Probability/Product_Measure.thy Thu Dec 02 14:57:21 2010 +0100 @@ -1365,7 +1365,7 @@ have "\A. measure (Pi\<^isub>E {} A) = 1" using assms by (subst measure_times) auto then show ?thesis - unfolding positive_integral_alt simple_function_def simple_integral_def_raw + unfolding positive_integral_def simple_function_def simple_integral_def_raw proof (simp add: P_empty, intro antisym) show "f (\k. undefined) \ (SUP f:{g. g \ f}. f (\k. undefined))" by (intro le_SUPI) auto