# HG changeset patch # User hoelzl # Date 1296825408 -3600 # Node ID 8c539202f85426b5993bbbf6bfe66d4d6257b03f # Parent f69bb9077b02f97238f987252f438e73d69ded56 add borel_fubini_integrable; remove unused bijectivity rules for measureable functions diff -r f69bb9077b02 -r 8c539202f854 src/HOL/Probability/Lebesgue_Measure.thy --- a/src/HOL/Probability/Lebesgue_Measure.thy Wed Feb 02 22:48:24 2011 +0100 +++ b/src/HOL/Probability/Lebesgue_Measure.thy Fri Feb 04 14:16:48 2011 +0100 @@ -756,13 +756,6 @@ "p2e (e2p x) = (x::'a::ordered_euclidean_space)" by (auto simp: euclidean_eq[where 'a='a] p2e_def e2p_def) -lemma bij_inv_p2e_e2p: - shows "bij_inv ({..\<^isub>E UNIV) (UNIV :: 'a::ordered_euclidean_space set) - p2e e2p" (is "bij_inv ?P ?U _ _") -proof (rule bij_invI) - show "p2e \ ?P \ ?U" "e2p \ ?U \ ?P" by (auto simp: e2p_def) -qed auto - declare restrict_extensional[intro] lemma e2p_extensional[intro]:"e2p (y::'a::ordered_euclidean_space) \ extensional {.. space ?P \ sets ?P" by auto qed simp +lemma inj_e2p[intro, simp]: "inj e2p" +proof (intro inj_onI conjI allI impI euclidean_eq[where 'a='a, THEN iffD2]) + fix x y ::'a and i assume "e2p x = e2p y" "i < DIM('a)" + then show "x $$ i= y $$ i" + by (auto simp: e2p_def restrict_def fun_eq_iff elim!: allE[where x=i]) +qed + lemma e2p_Int:"e2p ` A \ e2p ` B = e2p ` (A \ B)" (is "?L = ?R") - apply(rule image_Int[THEN sym]) - using bij_inv_p2e_e2p[THEN bij_inv_bij_betw(2)] - unfolding bij_betw_def by auto + by (auto simp: image_Int[THEN sym]) lemma Int_stable_cuboids: fixes x::"'a::ordered_euclidean_space" shows "Int_stable \space = UNIV, sets = range (\(a, b::'a). e2p ` {a..b})\" @@ -947,6 +945,31 @@ using lmeasure_measure_eq_borel_prod[OF A] by (simp add: range_e2p) qed +lemma borel_fubini_integrable: + fixes f :: "'a::ordered_euclidean_space \ real" + shows "integrable lborel f \ + integrable (lborel_space.P TYPE('a)) (\x. f (p2e x))" + (is "_ \ integrable ?B ?f") +proof + assume "integrable lborel f" + moreover then have f: "f \ borel_measurable borel" + by auto + moreover with measurable_p2e + have "f \ p2e \ borel_measurable ?B" + by (rule measurable_comp) + ultimately show "integrable ?B ?f" + by (simp add: comp_def borel_fubini_positiv_integral integrable_def) +next + assume "integrable ?B ?f" + moreover then + have "?f \ e2p \ borel_measurable (borel::'a algebra)" + by (auto intro!: measurable_e2p measurable_comp) + then have "f \ borel_measurable borel" + by (simp cong: measurable_cong) + ultimately show "integrable lborel f" + by (simp add: comp_def borel_fubini_positiv_integral integrable_def) +qed + lemma borel_fubini: fixes f :: "'a::ordered_euclidean_space \ real" assumes f: "f \ borel_measurable borel" diff -r f69bb9077b02 -r 8c539202f854 src/HOL/Probability/Sigma_Algebra.thy --- a/src/HOL/Probability/Sigma_Algebra.thy Wed Feb 02 22:48:24 2011 +0100 +++ b/src/HOL/Probability/Sigma_Algebra.thy Fri Feb 04 14:16:48 2011 +0100 @@ -769,48 +769,6 @@ show ?thesis by (simp add: comp_def) qed -lemma (in sigma_algebra) vimage_vimage_inv: - assumes f: "bij_betw f S (space M)" - assumes [simp]: "\x. x \ space M \ f (g x) = x" and g: "g \ space M \ S" - shows "sigma_algebra.vimage_algebra (vimage_algebra S f) (space M) g = M" -proof - - interpret T: sigma_algebra "vimage_algebra S f" - using f by (safe intro!: sigma_algebra_vimage bij_betw_imp_funcset) - - have inj: "inj_on f S" and [simp]: "f`S = space M" - using f unfolding bij_betw_def by auto - - { fix A assume A: "A \ sets M" - have "g -` f -` A \ g -` S \ space M = (f \ g) -` A \ space M" - using g by auto - also have "\ = A" - using `A \ sets M`[THEN sets_into_space] by auto - finally have "g -` f -` A \ g -` S \ space M = A" . } - note X = this - show ?thesis - unfolding T.vimage_algebra_def unfolding vimage_algebra_def - by (simp add: image_compose[symmetric] comp_def X cong: image_cong) -qed - -lemma (in sigma_algebra) measurable_vimage_iff: - fixes f :: "'b \ 'a" assumes f: "bij_betw f S (space M)" - shows "g \ measurable M M' \ (g \ f) \ measurable (vimage_algebra S f) M'" -proof - assume "g \ measurable M M'" - from measurable_vimage[OF this f[THEN bij_betw_imp_funcset]] - show "(g \ f) \ measurable (vimage_algebra S f) M'" unfolding comp_def . -next - interpret v: sigma_algebra "vimage_algebra S f" - using f[THEN bij_betw_imp_funcset] by (rule sigma_algebra_vimage) - note f' = f[THEN bij_betw_the_inv_into] - assume "g \ f \ measurable (vimage_algebra S f) M'" - from v.measurable_vimage[OF this, unfolded space_vimage_algebra, OF f'[THEN bij_betw_imp_funcset]] - show "g \ measurable M M'" - using f f'[THEN bij_betw_imp_funcset] f[unfolded bij_betw_def] - by (subst (asm) vimage_vimage_inv) - (simp_all add: f_the_inv_into_f cong: measurable_cong) -qed - lemma sigma_sets_vimage: assumes "f \ S' \ S" and "A \ Pow S" shows "sigma_sets S' ((\X. f -` X \ S') ` A) = (\X. f -` X \ S') ` sigma_sets S A" @@ -1417,93 +1375,10 @@ by (auto simp: image_space_def) qed -subsection "Bijective functions with inverse" - -definition "bij_inv A B f g \ - f \ A \ B \ g \ B \ A \ (\x\A. g (f x) = x) \ (\x\B. f (g x) = x)" - -lemma bij_inv_symmetric[sym]: "bij_inv A B f g \ bij_inv B A g f" - unfolding bij_inv_def by auto - -lemma bij_invI: - assumes "f \ A \ B" "g \ B \ A" - and "\x. x \ A \ g (f x) = x" - and "\x. x \ B \ f (g x) = x" - shows "bij_inv A B f g" - using assms unfolding bij_inv_def by auto - -lemma bij_invE: - assumes "bij_inv A B f g" - "\ f \ A \ B ; g \ B \ A ; - (\x. x \ A \ g (f x) = x) ; - (\x. x \ B \ f (g x) = x) \ \ P" - shows P - using assms unfolding bij_inv_def by auto - -lemma bij_inv_bij_betw: - assumes "bij_inv A B f g" - shows "bij_betw f A B" "bij_betw g B A" - using assms by (auto intro: bij_betwI elim!: bij_invE) - -lemma bij_inv_vimage_vimage: - assumes "bij_inv A B f e" - shows "f -` (e -` X \ B) \ A = X \ A" - using assms by (auto elim!: bij_invE) - -lemma (in sigma_algebra) measurable_vimage_iff_inv: - fixes f :: "'b \ 'a" assumes "bij_inv S (space M) f g" - shows "h \ measurable (vimage_algebra S f) M' \ (\x. h (g x)) \ measurable M M'" - unfolding measurable_vimage_iff[OF bij_inv_bij_betw(1), OF assms] -proof (rule measurable_cong) - fix w assume "w \ space (vimage_algebra S f)" - then have "w \ S" by auto - then show "h w = ((\x. h (g x)) \ f) w" - using assms by (auto elim: bij_invE) -qed - -lemma vimage_algebra_sigma: - assumes bi: "bij_inv (space (sigma F)) (space (sigma E)) f e" - and "sets E \ Pow (space E)" and F: "sets F \ Pow (space F)" - and "more E = more F" - and "f \ measurable F E" "e \ measurable E F" - shows "sigma_algebra.vimage_algebra (sigma E) (space (sigma F)) f = sigma F" -proof - - interpret sigma_algebra "sigma E" - using assms by (intro sigma_algebra_sigma) auto - have eq: "sets F = (\X. f -` X \ space F) ` sets E" - proof safe - fix X assume "X \ sets F" - then have "e -` X \ space E \ sets E" - using `e \ measurable E F` unfolding measurable_def by auto - then show "X \(\Y. f -` Y \ space F) ` sets E" - apply (rule rev_image_eqI) - unfolding bij_inv_vimage_vimage[OF bi[simplified]] - using F `X \ sets F` by auto - next - fix X assume "X \ sets E" then show "f -` X \ space F \ sets F" - using `f \ measurable F E` unfolding measurable_def by auto - qed - show "vimage_algebra (space (sigma F)) f = sigma F" - unfolding vimage_algebra_def using assms - by (auto simp: bij_inv_def eq sigma_sets_vimage[symmetric] sigma_def) -qed - lemma measurable_sigma_sigma: assumes M: "sets M \ Pow (space M)" and N: "sets N \ Pow (space N)" shows "f \ measurable M N \ f \ measurable (sigma M) (sigma N)" using sigma_algebra.measurable_subset[OF sigma_algebra_sigma[OF M], of N] using measurable_up_sigma[of M N] N by auto -lemma bij_inv_the_inv_into: - assumes "bij_betw f A B" shows "bij_inv A B f (the_inv_into A f)" -proof (rule bij_invI) - show "the_inv_into A f \ B \ A" - using bij_betw_the_inv_into[OF assms] by (rule bij_betw_imp_funcset) - show "f \ A \ B" using assms by (rule bij_betw_imp_funcset) - show "\x. x \ A \ the_inv_into A f (f x) = x" - "\x. x \ B \ f (the_inv_into A f x) = x" - using the_inv_into_f_f[of f A] f_the_inv_into_f[of f A] - using assms by (auto simp: bij_betw_def) -qed - end