# HG changeset patch # User hoelzl # Date 1291233782 -3600 # Node ID 688f6ff859e181f330a26d7c75bcb9efc38ae0d8 # Parent 94427db32392a2cc2027168e8079c4c5808559aa Generalized simple_functionD and less_SUP_iff. Moved theorems to appropriate places. diff -r 94427db32392 -r 688f6ff859e1 src/HOL/Probability/Complete_Measure.thy --- a/src/HOL/Probability/Complete_Measure.thy Wed Dec 01 20:12:53 2010 +0100 +++ b/src/HOL/Probability/Complete_Measure.thy Wed Dec 01 21:03:02 2010 +0100 @@ -189,56 +189,13 @@ qed qed -lemma (in sigma_algebra) simple_functionD': - assumes "simple_function f" - shows "f -` {x} \ space M \ sets M" -proof cases - assume "x \ f`space M" from simple_functionD(2)[OF assms this] show ?thesis . -next - assume "x \ f`space M" then have "f -` {x} \ space M = {}" by auto - then show ?thesis by auto -qed - -lemma (in sigma_algebra) simple_function_If: - assumes sf: "simple_function f" "simple_function g" and A: "A \ sets M" - shows "simple_function (\x. if x \ A then f x else g x)" (is "simple_function ?IF") -proof - - def F \ "\x. f -` {x} \ space M" and G \ "\x. g -` {x} \ space M" - show ?thesis unfolding simple_function_def - proof safe - have "?IF ` space M \ f ` space M \ g ` space M" by auto - from finite_subset[OF this] assms - show "finite (?IF ` space M)" unfolding simple_function_def by auto - next - fix x assume "x \ space M" - then have *: "?IF -` {?IF x} \ space M = (if x \ A - then ((F (f x) \ A) \ (G (f x) - (G (f x) \ A))) - else ((F (g x) \ A) \ (G (g x) - (G (g x) \ A))))" - using sets_into_space[OF A] by (auto split: split_if_asm simp: G_def F_def) - have [intro]: "\x. F x \ sets M" "\x. G x \ sets M" - unfolding F_def G_def using sf[THEN simple_functionD'] by auto - show "?IF -` {?IF x} \ space M \ sets M" unfolding * using A by auto - qed -qed - -lemma (in measure_space) null_sets_finite_UN: - assumes "finite S" "\i. i \ S \ A i \ null_sets" - shows "(\i\S. A i) \ null_sets" -proof (intro CollectI conjI) - show "(\i\S. A i) \ sets M" using assms by (intro finite_UN) auto - have "\ (\i\S. A i) \ (\i\S. \ (A i))" - using assms by (intro measure_finitely_subadditive) auto - then show "\ (\i\S. A i) = 0" - using assms by auto -qed - lemma (in completeable_measure_space) completion_ex_simple_function: assumes f: "completion.simple_function f" shows "\f'. simple_function f' \ (AE x. f x = f' x)" proof - let "?F x" = "f -` {x} \ space M" have F: "\x. ?F x \ sets completion" and fin: "finite (f`space M)" - using completion.simple_functionD'[OF f] + using completion.simple_functionD[OF f] completion.simple_functionD[OF f] by simp_all have "\x. \N. N \ null_sets \ null_part (?F x) \ N" using F null_part by auto diff -r 94427db32392 -r 688f6ff859e1 src/HOL/Probability/Lebesgue_Integration.thy --- a/src/HOL/Probability/Lebesgue_Integration.thy Wed Dec 01 20:12:53 2010 +0100 +++ b/src/HOL/Probability/Lebesgue_Integration.thy Wed Dec 01 21:03:02 2010 +0100 @@ -6,20 +6,6 @@ imports Measure Borel_Space begin -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" -proof safe - fix x assume "x \ A" - with A obtain y where "f x = g y" "y \ B" by auto - then show "f x \ g ` B" by auto -next - fix y assume "y \ B" - with B obtain x where "g y = f x" "x \ A" by auto - then show "g y \ f ` A" by auto -qed - lemma sums_If_finite: assumes finite: "finite {r. P r}" shows "(\r. if P r then f r else 0) sums (\r\{r. P r}. f r)" (is "?F sums _") @@ -57,9 +43,20 @@ lemma (in sigma_algebra) simple_functionD: assumes "simple_function g" - shows "finite (g ` space M)" - "x \ g ` space M \ g -` {x} \ space M \ sets M" - using assms unfolding simple_function_def by auto + shows "finite (g ` space M)" and "g -` {x} \ space M \ sets M" +proof - + show "finite (g ` space M)" + using assms unfolding simple_function_def by auto + show "g -` {x} \ space M \ sets M" + proof cases + assume "x \ g`space M" then show ?thesis + using assms unfolding simple_function_def by auto + next + assume "x \ g`space M" + then have "g -` {x} \ space M = {}" by auto + then show ?thesis by auto + qed +qed lemma (in sigma_algebra) simple_function_indicator_representation: fixes f ::"'a \ pinfreal" @@ -516,9 +513,7 @@ proof - interpret v: measure_space M \ by (rule measure_space_cong) fact - have "\x. x \ space M \ f -` {f x} \ space M \ sets M" - using `simple_function f`[THEN simple_functionD(2)] by auto - with assms show ?thesis + from simple_functionD[OF `simple_function f`] assms show ?thesis unfolding simple_integral_def v.simple_integral_def by (auto intro!: setsum_cong) qed @@ -629,6 +624,28 @@ by (auto simp: setsum_right_distrib field_simps intro!: setsum_cong) qed +lemma (in sigma_algebra) simple_function_If: + assumes sf: "simple_function f" "simple_function g" and A: "A \ sets M" + shows "simple_function (\x. if x \ A then f x else g x)" (is "simple_function ?IF") +proof - + def F \ "\x. f -` {x} \ space M" and G \ "\x. g -` {x} \ space M" + show ?thesis unfolding simple_function_def + proof safe + have "?IF ` space M \ f ` space M \ g ` space M" by auto + from finite_subset[OF this] assms + show "finite (?IF ` space M)" unfolding simple_function_def by auto + next + fix x assume "x \ space M" + then have *: "?IF -` {?IF x} \ space M = (if x \ A + then ((F (f x) \ A) \ (G (f x) - (G (f x) \ A))) + else ((F (g x) \ A) \ (G (g x) - (G (g x) \ A))))" + using sets_into_space[OF A] by (auto split: split_if_asm simp: G_def F_def) + have [intro]: "\x. F x \ sets M" "\x. G x \ sets M" + unfolding F_def G_def using sf[THEN simple_functionD(2)] by auto + show "?IF -` {?IF x} \ space M \ sets M" unfolding * using A by auto + qed +qed + lemma (in measure_space) simple_integral_mono_AE: assumes "simple_function f" and "simple_function g" and mono: "AE x. f x \ g x" @@ -652,8 +669,8 @@ obtain N where N: "{x\space M. \ f x \ g x} \ N" "N \ sets M" "\ N = 0" using mono by (auto elim!: AE_E) have "?S x \ N" using N `x \ space M` False by auto - moreover have "?S x \ sets M" using assms `x \ space M` - by (rule_tac Int) (auto intro!: simple_functionD(2)) + moreover have "?S x \ sets M" using assms + by (rule_tac Int) (auto intro!: simple_functionD) ultimately have "\ (?S x) \ \ N" using `N \ sets M` by (auto intro!: measure_mono) then show ?thesis using `\ N = 0` by auto @@ -1008,6 +1025,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)" @@ -1030,6 +1053,7 @@ 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) diff -r 94427db32392 -r 688f6ff859e1 src/HOL/Probability/Lebesgue_Measure.thy --- a/src/HOL/Probability/Lebesgue_Measure.thy Wed Dec 01 20:12:53 2010 +0100 +++ b/src/HOL/Probability/Lebesgue_Measure.thy Wed Dec 01 21:03:02 2010 +0100 @@ -4,89 +4,6 @@ imports Product_Measure Gauge_Measure Complete_Measure begin -lemma (in complete_lattice) SUP_pair: - "(SUP i:A. SUP j:B. f i j) = (SUP p:A\B. (\ (i, j). f i j) p)" (is "?l = ?r") -proof (intro antisym SUP_leI) - fix i j assume "i \ A" "j \ B" - then have "(case (i,j) of (i,j) \ f i j) \ ?r" - by (intro SUPR_upper) auto - then show "f i j \ ?r" by auto -next - fix p assume "p \ A \ B" - then obtain i j where "p = (i,j)" "i \ A" "j \ B" by auto - have "f i j \ (SUP j:B. f i j)" using `j \ B` by (intro SUPR_upper) - also have "(SUP j:B. f i j) \ ?l" using `i \ A` by (intro SUPR_upper) - finally show "(case p of (i, j) \ f i j) \ ?l" using `p = (i,j)` by simp -qed - -lemma (in complete_lattice) SUP_surj_compose: - assumes *: "f`A = B" shows "SUPR A (g \ f) = SUPR B g" - unfolding SUPR_def unfolding *[symmetric] - by (simp add: image_compose) - -lemma (in complete_lattice) SUP_swap: - "(SUP i:A. SUP j:B. f i j) = (SUP j:B. SUP i:A. f i j)" -proof - - have *: "(\(i,j). (j,i)) ` (B \ A) = A \ B" by auto - show ?thesis - unfolding SUP_pair SUP_surj_compose[symmetric, OF *] - by (auto intro!: arg_cong[where f=Sup] image_eqI simp: comp_def SUPR_def) -qed - -lemma SUP_\: "(SUP i:A. f i) = \ \ (\x<\. \i\A. x < f i)" -proof - assume *: "(SUP i:A. f i) = \" - show "(\x<\. \i\A. x < f i)" unfolding *[symmetric] - proof (intro allI impI) - fix x assume "x < SUPR A f" then show "\i\A. x < f i" - unfolding less_SUP_iff by auto - qed -next - assume *: "\x<\. \i\A. x < f i" - show "(SUP i:A. f i) = \" - proof (rule pinfreal_SUPI) - fix y assume **: "\i. i \ A \ f i \ y" - show "\ \ y" - proof cases - assume "y < \" - from *[THEN spec, THEN mp, OF this] - obtain i where "i \ A" "\ (f i \ y)" by auto - with ** show ?thesis by auto - qed auto - qed auto -qed - -lemma psuminf_commute: - shows "(\\<^isub>\ i j. f i j) = (\\<^isub>\ j i. f i j)" -proof - - have "(SUP n. \ i < n. SUP m. \ j < m. f i j) = (SUP n. SUP m. \ i < n. \ j < m. f i j)" - apply (subst SUPR_pinfreal_setsum) - by auto - also have "\ = (SUP m n. \ j < m. \ i < n. f i j)" - apply (subst SUP_swap) - apply (subst setsum_commute) - by auto - also have "\ = (SUP m. \ j < m. SUP n. \ i < n. f i j)" - apply (subst SUPR_pinfreal_setsum) - by auto - finally show ?thesis - unfolding psuminf_def by auto -qed - -lemma psuminf_SUP_eq: - assumes "\n i. f n i \ f (Suc n) i" - shows "(\\<^isub>\ i. SUP n::nat. f n i) = (SUP n::nat. \\<^isub>\ i. f n i)" -proof - - { fix n :: nat - have "(\ii 'a::ordered_euclidean_space set" where diff -r 94427db32392 -r 688f6ff859e1 src/HOL/Probability/Measure.thy --- a/src/HOL/Probability/Measure.thy Wed Dec 01 20:12:53 2010 +0100 +++ b/src/HOL/Probability/Measure.thy Wed Dec 01 21:03:02 2010 +0100 @@ -651,27 +651,6 @@ abbreviation (in measure_space) "null_sets \ {N\sets M. \ N = 0}" -definition (in measure_space) - almost_everywhere :: "('a \ bool) \ bool" (binder "AE " 10) where - "almost_everywhere P \ (\N\null_sets. { x \ space M. \ P x } \ N)" - -lemma (in measure_space) AE_I': - "N \ null_sets \ {x\space M. \ P x} \ N \ (AE x. P x)" - unfolding almost_everywhere_def by auto - -lemma (in measure_space) AE_iff_null_set: - assumes "{x\space M. \ P x} \ sets M" (is "?P \ sets M") - shows "(AE x. P x) \ {x\space M. \ P x} \ null_sets" -proof - assume "AE x. P x" then obtain N where N: "N \ sets M" "?P \ N" "\ N = 0" - unfolding almost_everywhere_def by auto - moreover have "\ ?P \ \ N" - using assms N(1,2) by (auto intro: measure_mono) - ultimately show "?P \ null_sets" using assms by auto -next - assume "?P \ null_sets" with assms show "AE x. P x" by (auto intro: AE_I') -qed - lemma (in measure_space) null_sets_Un[intro]: assumes "N \ null_sets" "N' \ null_sets" shows "N \ N' \ null_sets" @@ -703,6 +682,17 @@ using assms by auto qed +lemma (in measure_space) null_sets_finite_UN: + assumes "finite S" "\i. i \ S \ A i \ null_sets" + shows "(\i\S. A i) \ null_sets" +proof (intro CollectI conjI) + show "(\i\S. A i) \ sets M" using assms by (intro finite_UN) auto + have "\ (\i\S. A i) \ (\i\S. \ (A i))" + using assms by (intro measure_finitely_subadditive) auto + then show "\ (\i\S. A i) = 0" + using assms by auto +qed + lemma (in measure_space) null_set_Int1: assumes "B \ null_sets" "A \ sets M" shows "A \ B \ null_sets" using assms proof (intro CollectI conjI) @@ -741,6 +731,29 @@ by (subst measure_additive[symmetric]) auto qed +section "Formalise almost everywhere" + +definition (in measure_space) + almost_everywhere :: "('a \ bool) \ bool" (binder "AE " 10) where + "almost_everywhere P \ (\N\null_sets. { x \ space M. \ P x } \ N)" + +lemma (in measure_space) AE_I': + "N \ null_sets \ {x\space M. \ P x} \ N \ (AE x. P x)" + unfolding almost_everywhere_def by auto + +lemma (in measure_space) AE_iff_null_set: + assumes "{x\space M. \ P x} \ sets M" (is "?P \ sets M") + shows "(AE x. P x) \ {x\space M. \ P x} \ null_sets" +proof + assume "AE x. P x" then obtain N where N: "N \ sets M" "?P \ N" "\ N = 0" + unfolding almost_everywhere_def by auto + moreover have "\ ?P \ \ N" + using assms N(1,2) by (auto intro: measure_mono) + ultimately show "?P \ null_sets" using assms by auto +next + assume "?P \ null_sets" with assms show "AE x. P x" by (auto intro: AE_I') +qed + lemma (in measure_space) AE_True[intro, simp]: "AE x. True" unfolding almost_everywhere_def by auto @@ -1409,7 +1422,7 @@ show "\ {x} \ \" by (auto simp: insert_absorb[OF *] Diff_subset) } qed -sublocale finite_measure_space < finite_measure +sublocale finite_measure_space \ finite_measure proof show "\ (space M) \ \" unfolding sum_over_space[symmetric] setsum_\ diff -r 94427db32392 -r 688f6ff859e1 src/HOL/Probability/Positive_Infinite_Real.thy --- a/src/HOL/Probability/Positive_Infinite_Real.thy Wed Dec 01 20:12:53 2010 +0100 +++ b/src/HOL/Probability/Positive_Infinite_Real.thy Wed Dec 01 21:03:02 2010 +0100 @@ -6,6 +6,49 @@ imports Complex_Main Nat_Bijection Multivariate_Analysis begin +lemma (in complete_lattice) SUPR_upper: + "x \ A \ f x \ SUPR A f" + unfolding SUPR_def apply(rule Sup_upper) by auto + +lemma (in complete_lattice) SUPR_subset: + assumes "A \ B" shows "SUPR A f \ SUPR B f" + apply(rule SUP_leI) apply(rule SUPR_upper) using assms by auto + +lemma (in complete_lattice) SUPR_mono: + assumes "\a\A. \b\B. f b \ f a" + shows "SUPR A f \ SUPR B f" + unfolding SUPR_def apply(rule Sup_mono) + using assms by auto + +lemma (in complete_lattice) SUP_pair: + "(SUP i:A. SUP j:B. f i j) = (SUP p:A\B. (\ (i, j). f i j) p)" (is "?l = ?r") +proof (intro antisym SUP_leI) + fix i j assume "i \ A" "j \ B" + then have "(case (i,j) of (i,j) \ f i j) \ ?r" + by (intro SUPR_upper) auto + then show "f i j \ ?r" by auto +next + fix p assume "p \ A \ B" + then obtain i j where "p = (i,j)" "i \ A" "j \ B" by auto + have "f i j \ (SUP j:B. f i j)" using `j \ B` by (intro SUPR_upper) + also have "(SUP j:B. f i j) \ ?l" using `i \ A` by (intro SUPR_upper) + finally show "(case p of (i, j) \ f i j) \ ?l" using `p = (i,j)` by simp +qed + +lemma (in complete_lattice) SUP_surj_compose: + assumes *: "f`A = B" shows "SUPR A (g \ f) = SUPR B g" + unfolding SUPR_def unfolding *[symmetric] + by (simp add: image_compose) + +lemma (in complete_lattice) SUP_swap: + "(SUP i:A. SUP j:B. f i j) = (SUP j:B. SUP i:A. f i j)" +proof - + have *: "(\(i,j). (j,i)) ` (B \ A) = A \ B" by auto + show ?thesis + unfolding SUP_pair SUP_surj_compose[symmetric, OF *] + by (auto intro!: arg_cong[where f=Sup] image_eqI simp: comp_def SUPR_def) +qed + lemma range_const[simp]: "range (\x. c) = {c}" by auto lemma (in complete_lattice) SUPR_const[simp]: "(SUP i. c) = c" @@ -549,6 +592,14 @@ lemma pinfreal_of_nat[simp]: "of_nat m = Real (real m)" by (induct m) (auto simp: real_of_nat_Suc one_pinfreal_def simp del: Real_1) +lemma less_\_Ex_of_nat: "x < \ \ (\n. x < of_nat n)" +proof safe + assume "x < \" + then obtain r where "0 \ r" "x = Real r" by (cases x) auto + moreover obtain n where "r < of_nat n" using ex_less_of_nat by auto + ultimately show "\n. x < of_nat n" by (auto simp: real_eq_of_nat) +qed auto + lemma real_of_pinfreal_mono: fixes a b :: pinfreal assumes "b \ \" "a \ b" @@ -831,6 +882,34 @@ qed simp qed simp +lemma less_SUP_iff: + fixes a :: "'a::{complete_lattice,linorder}" + shows "(a < (SUP i:A. f i)) \ (\x\A. a < f x)" + unfolding SUPR_def less_Sup_iff by auto + +lemma SUP_\: "(SUP i:A. f i) = \ \ (\x<\. \i\A. x < f i)" +proof + assume *: "(SUP i:A. f i) = \" + show "(\x<\. \i\A. x < f i)" unfolding *[symmetric] + proof (intro allI impI) + fix x assume "x < SUPR A f" then show "\i\A. x < f i" + unfolding less_SUP_iff by auto + qed +next + assume *: "\x<\. \i\A. x < f i" + show "(SUP i:A. f i) = \" + proof (rule pinfreal_SUPI) + fix y assume **: "\i. i \ A \ f i \ y" + show "\ \ y" + proof cases + assume "y < \" + from *[THEN spec, THEN mp, OF this] + obtain i where "i \ A" "\ (f i \ y)" by auto + with ** show ?thesis by auto + qed auto + qed auto +qed + subsubsection {* Equivalence between @{text "f ----> x"} and @{text SUP} on @{typ pinfreal} *} lemma monoseq_monoI: "mono f \ monoseq f" @@ -1384,6 +1463,37 @@ qed simp qed simp +lemma psuminf_SUP_eq: + assumes "\n i. f n i \ f (Suc n) i" + shows "(\\<^isub>\ i. SUP n::nat. f n i) = (SUP n::nat. \\<^isub>\ i. f n i)" +proof - + { fix n :: nat + have "(\ii\<^isub>\ i j. f i j) = (\\<^isub>\ j i. f i j)" +proof - + have "(SUP n. \ i < n. SUP m. \ j < m. f i j) = (SUP n. SUP m. \ i < n. \ j < m. f i j)" + apply (subst SUPR_pinfreal_setsum) + by auto + also have "\ = (SUP m n. \ j < m. \ i < n. f i j)" + apply (subst SUP_swap) + apply (subst setsum_commute) + by auto + also have "\ = (SUP m. \ j < m. SUP n. \ i < n. f i j)" + apply (subst SUPR_pinfreal_setsum) + by auto + finally show ?thesis + unfolding psuminf_def by auto +qed + lemma Real_max: assumes "x \ 0" "y \ 0" shows "Real (max x y) = max (Real x) (Real y)" @@ -2076,20 +2186,6 @@ lemma real_Real_max:"real (Real x) = max x 0" unfolding real_Real by auto -lemma (in complete_lattice) SUPR_upper: - "x \ A \ f x \ SUPR A f" - unfolding SUPR_def apply(rule Sup_upper) by auto - -lemma (in complete_lattice) SUPR_subset: - assumes "A \ B" shows "SUPR A f \ SUPR B f" - apply(rule SUP_leI) apply(rule SUPR_upper) using assms by auto - -lemma (in complete_lattice) SUPR_mono: - assumes "\a\A. \b\B. f b \ f a" - shows "SUPR A f \ SUPR B f" - unfolding SUPR_def apply(rule Sup_mono) - using assms by auto - lemma Sup_lim: assumes "\n. b n \ s" "b ----> (a::pinfreal)" shows "a \ Sup s" @@ -2161,11 +2257,6 @@ unfolding Real_real using om by auto qed qed -lemma less_SUP_iff: - fixes a :: pinfreal - shows "(a < (SUP i:A. f i)) \ (\x\A. a < f x)" - unfolding SUPR_def less_Sup_iff by auto - lemma Sup_mono_lim: assumes "\a\A. \b. \n. b n \ B \ b ----> (a::pinfreal)" shows "Sup A \ Sup B" @@ -2707,4 +2798,21 @@ lemma lessThan_0_Empty: "{..< 0 :: pinfreal} = {}" by auto +lemma real_of_pinfreal_inverse[simp]: + fixes X :: pinfreal + shows "real (inverse X) = 1 / real X" + by (cases X) (auto simp: inverse_eq_divide) + +lemma real_of_pinfreal_le_0[simp]: "real (X :: pinfreal) \ 0 \ (X = 0 \ X = \)" + by (cases X) auto + +lemma real_of_pinfreal_less_0[simp]: "\ (real (X :: pinfreal) < 0)" + by (cases X) auto + +lemma abs_real_of_pinfreal[simp]: "\real (X :: pinfreal)\ = real X" + by simp + +lemma zero_less_real_of_pinfreal: "0 < real (X :: pinfreal) \ X \ 0 \ X \ \" + by (cases X) auto + end diff -r 94427db32392 -r 688f6ff859e1 src/HOL/Probability/Product_Measure.thy --- a/src/HOL/Probability/Product_Measure.thy Wed Dec 01 20:12:53 2010 +0100 +++ b/src/HOL/Probability/Product_Measure.thy Wed Dec 01 21:03:02 2010 +0100 @@ -2,28 +2,6 @@ imports Lebesgue_Integration begin -lemma in_sigma[intro, simp]: "A \ sets M \ A \ sets (sigma M)" - unfolding sigma_def by (auto intro!: sigma_sets.Basic) - -lemma (in sigma_algebra) sigma_eq[simp]: "sigma M = M" - unfolding sigma_def sigma_sets_eq by simp - -lemma vimage_algebra_sigma: - assumes E: "sets E \ Pow (space E)" - and f: "f \ space F \ space E" - and "\A. A \ sets F \ A \ (\X. f -` X \ space F) ` sets E" - and "\A. A \ sets E \ f -` A \ space F \ sets F" - shows "sigma_algebra.vimage_algebra (sigma E) (space 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" - using assms by auto - show "vimage_algebra (space F) f = sigma F" - unfolding vimage_algebra_def using assms - by (simp add: sigma_def eq sigma_sets_vimage) -qed - lemma times_Int_times: "A \ B \ C \ D = (A \ C) \ (B \ D)" by auto @@ -786,13 +764,10 @@ positive_integral f" proof - interpret Q: pair_sigma_finite M2 \2 M1 \1 by default - have s: "\x y. (case (x, y) of (x, y) \ f (y, x)) = f (y, x)" by simp have t: "(\x. f (case x of (x, y) \ (y, x))) = (\(x, y). f (y, x))" by (auto simp: fun_eq_iff) - have bij: "bij_betw (\(x, y). (y, x)) (space M2 \ space M1) (space P)" by (auto intro!: inj_onI simp: space_pair_algebra bij_betw_def) - note pair_sigma_algebra_measurable[OF f] from Q.positive_integral_fst_measurable[OF this] have "M2.positive_integral (\y. M1.positive_integral (\x. f (x, y))) = @@ -930,7 +905,6 @@ using E1 E2 by (auto simp add: pair_algebra_def) interpret E: sigma_algebra ?E unfolding pair_algebra_def using E1 E2 by (intro sigma_algebra_sigma) auto - { fix A assume "A \ sets E1" then have "fst -` A \ space ?E = A \ (\i. S2 i)" using E1 2 unfolding isoton_def pair_algebra_def by auto @@ -954,7 +928,6 @@ "fst \ measurable ?E (sigma E1) \ snd \ measurable ?E (sigma E2)" using E1 E2 by (subst (1 2) E.measurable_iff_sigma) (auto simp: pair_algebra_def sets_sigma) - { fix A B assume A: "A \ sets (sigma E1)" and B: "B \ sets (sigma E2)" with proj have "fst -` A \ space ?E \ sets ?E" "snd -` B \ space ?E \ sets ?E" unfolding measurable_def by simp_all @@ -966,7 +939,6 @@ by (intro E.sigma_sets_subset) (auto simp add: pair_algebra_def sets_sigma) then have subset: "sets ?S \ sets ?E" by (simp add: sets_sigma pair_algebra_def) - have "sets ?S = sets ?E" proof (intro set_eqI iffI) fix A assume "A \ sets ?E" then show "A \ sets ?S" @@ -1304,7 +1276,6 @@ unfolding product_singleton_vimage_algebra_eq[OF `i \ I` `finite I`, symmetric] using bij_betw_restrict_I_i[OF `i \ I`, of M] by (intro P.measure_space_isomorphic) auto - show ?case proof (intro exI[of _ ?\] conjI ballI) { fix A assume A: "A \ (\ i\insert i I. sets (M i))" @@ -1322,7 +1293,6 @@ apply fastsimp using `i \ I` `finite I` prod[of A] by (auto simp: ac_simps) } note product = this - show "sigma_finite_measure I'.P ?\" proof from I'.sigma_finite_pairs guess F :: "'i \ nat \ 'a set" .. @@ -1455,17 +1425,13 @@ have "finite (I \ J)" using fin by auto interpret IJ: finite_product_sigma_finite M \ "I \ J" by default fact interpret P: pair_sigma_finite I.P I.measure J.P J.measure by default - let ?f = "\x. ((\i\I. x i), (\i\J. x i))" - have P_borel: "(\x. f (case x of (x, y) \ merge I x J y)) \ borel_measurable P.P" by (subst product_product_vimage_algebra_eq[OF IJ fin, symmetric]) (auto simp: space_pair_algebra intro!: IJ.measurable_vimage f) - have split_f_image[simp]: "\F. ?f ` (Pi\<^isub>E (I \ J) F) = (Pi\<^isub>E I F) \ (Pi\<^isub>E J F)" apply auto apply (rule_tac x="merge I a J b" in image_eqI) by (auto dest: extensional_restrict) - have "IJ.positive_integral f = IJ.positive_integral (\x. f (restrict x (I \ J)))" by (auto intro!: IJ.positive_integral_cong arg_cong[where f=f] dest!: extensional_restrict) also have "\ = I.positive_integral (\x. J.positive_integral (\y. f (merge I x J y)))" diff -r 94427db32392 -r 688f6ff859e1 src/HOL/Probability/Radon_Nikodym.thy --- a/src/HOL/Probability/Radon_Nikodym.thy Wed Dec 01 20:12:53 2010 +0100 +++ b/src/HOL/Probability/Radon_Nikodym.thy Wed Dec 01 21:03:02 2010 +0100 @@ -69,6 +69,8 @@ qed qed +subsection "Absolutely continuous" + definition (in measure_space) "absolutely_continuous \ = (\N\null_sets. \ N = (0 :: pinfreal))" @@ -111,6 +113,14 @@ finally show "\ N = 0" . qed +lemma (in measure_space) density_is_absolutely_continuous: + assumes "\A. A \ sets M \ \ A = positive_integral (\x. f x * indicator A x)" + shows "absolutely_continuous \" + using assms unfolding absolutely_continuous_def + by (simp add: positive_integral_null_set) + +subsection "Existence of the Radon-Nikodym derivative" + lemma (in finite_measure) Radon_Nikodym_aux_epsilon: fixes e :: real assumes "0 < e" assumes "finite_measure M s" @@ -120,21 +130,17 @@ proof - let "?d A" = "real (\ A) - real (s A)" interpret M': finite_measure M s by fact - let "?A A" = "if (\B\sets M. B \ space M - A \ -e < ?d B) then {} else (SOME B. B \ sets M \ B \ space M - A \ ?d B \ -e)" def A \ "\n. ((\B. B \ ?A B) ^^ n) {}" - have A_simps[simp]: "A 0 = {}" "\n. A (Suc n) = (A n \ ?A (A n))" unfolding A_def by simp_all - { fix A assume "A \ sets M" have "?A A \ sets M" by (auto intro!: someI2[of _ _ "\A. A \ sets M"] simp: not_less) } note A'_in_sets = this - { fix n have "A n \ sets M" proof (induct n) case (Suc n) thus "A (Suc n) \ sets M" @@ -142,7 +148,6 @@ qed (simp add: A_def) } note A_in_sets = this hence "range A \ sets M" by auto - { fix n B assume Ex: "\B. B \ sets M \ B \ space M - A n \ ?d B \ -e" hence False: "\ (\B\sets M. B \ space M - A n \ -e < ?d B)" by (auto simp: not_less) @@ -156,7 +161,6 @@ finally show "?d (A n \ B) \ ?d (A n) - e" . qed } note dA_epsilon = this - { fix n have "?d (A (Suc n)) \ ?d (A n)" proof (cases "\B. B\sets M \ B \ space M - A n \ ?d B \ - e") case True from dA_epsilon[OF this] show ?thesis using `0 < e` by simp @@ -166,7 +170,6 @@ thus ?thesis by simp qed } note dA_mono = this - show ?thesis proof (cases "\n. \B\sets M. B \ space M - A n \ -e < ?d B") case True then obtain n where B: "\B. \ B \ sets M; B \ space M - A n\ \ -e < ?d B" by blast @@ -220,11 +223,8 @@ proof - let "?d A" = "real (\ A) - real (s A)" let "?P A B n" = "A \ sets M \ A \ B \ ?d B \ ?d A \ (\C\sets M. C \ A \ - 1 / real (Suc n) < ?d C)" - interpret M': finite_measure M s by fact - let "?r S" = "restricted_space S" - { fix S n assume S: "S \ sets M" hence **: "\X. X \ op \ S ` sets M \ X \ sets M \ X \ S" by auto @@ -242,11 +242,9 @@ qed hence "\A. ?P A S n" by auto } note Ex_P = this - def A \ "nat_rec (space M) (\n A. SOME B. ?P B A n)" have A_Suc: "\n. A (Suc n) = (SOME B. ?P B (A n) n)" by (simp add: A_def) have A_0[simp]: "A 0 = space M" unfolding A_def by simp - { fix i have "A i \ sets M" unfolding A_def proof (induct i) case (Suc i) @@ -254,19 +252,15 @@ by (rule someI2_ex) simp qed simp } note A_in_sets = this - { fix n have "?P (A (Suc n)) (A n) n" using Ex_P[OF A_in_sets] unfolding A_Suc by (rule someI2_ex) simp } note P_A = this - have "range A \ sets M" using A_in_sets by auto - have A_mono: "\i. A (Suc i) \ A i" using P_A by simp have mono_dA: "mono (\i. ?d (A i))" using P_A by (simp add: mono_iff_le_Suc) have epsilon: "\C i. \ C \ sets M; C \ A (Suc i) \ \ - 1 / real (Suc i) < ?d C" using P_A by auto - show ?thesis proof (safe intro!: bexI[of _ "\i. A i"]) show "(\i. A i) \ sets M" using A_in_sets by auto @@ -298,24 +292,19 @@ shows "\f \ borel_measurable M. \A\sets M. \ A = positive_integral (\x. f x * indicator A x)" proof - interpret M': finite_measure M \ using assms(1) . - def G \ "{g \ borel_measurable M. \A\sets M. positive_integral (\x. g x * indicator A x) \ \ A}" have "(\x. 0) \ G" unfolding G_def by auto hence "G \ {}" by auto - { fix f g assume f: "f \ G" and g: "g \ G" have "(\x. max (g x) (f x)) \ G" (is "?max \ G") unfolding G_def proof safe show "?max \ borel_measurable M" using f g unfolding G_def by auto - let ?A = "{x \ space M. f x \ g x}" have "?A \ sets M" using f g unfolding G_def by auto - fix A assume "A \ sets M" hence sets: "?A \ A \ sets M" "(space M - ?A) \ A \ sets M" using `?A \ sets M` by auto have union: "((?A \ A) \ ((space M - ?A) \ A)) = A" using sets_into_space[OF `A \ sets M`] by auto - have "\x. x \ space M \ max (g x) (f x) * indicator A x = g x * indicator (?A \ A) x + f x * indicator ((space M - ?A) \ A) x" by (auto simp: indicator_def max_def) @@ -331,14 +320,12 @@ finally show "positive_integral (\x. max (g x) (f x) * indicator A x) \ \ A" . qed } note max_in_G = this - { fix f g assume "f \ g" and f: "\i. f i \ G" have "g \ G" unfolding G_def proof safe from `f \ g` have [simp]: "g = (SUP i. f i)" unfolding isoton_def by simp have f_borel: "\i. f i \ borel_measurable M" using f unfolding G_def by simp thus "g \ borel_measurable M" by (auto intro!: borel_measurable_SUP) - fix A assume "A \ sets M" hence "\i. (\x. f i x * indicator A x) \ borel_measurable M" using f_borel by (auto intro!: borel_measurable_indicator) @@ -350,7 +337,6 @@ using f `A \ sets M` unfolding G_def by (auto intro!: SUP_leI) qed } note SUP_in_G = this - let ?y = "SUP g : G. positive_integral g" have "?y \ \ (space M)" unfolding G_def proof (safe intro!: SUP_leI) @@ -385,7 +371,6 @@ hence isoton_g: "?g \ f" by (simp add: isoton_def le_fun_def f_def) from SUP_in_G[OF this g_in_G] have "f \ G" . hence [simp, intro]: "f \ borel_measurable M" unfolding G_def by auto - have "(\i. positive_integral (?g i)) \ positive_integral f" using isoton_g g_in_G by (auto intro!: positive_integral_isoton simp: G_def f_def) hence "positive_integral f = (SUP i. positive_integral (?g i))" @@ -398,9 +383,7 @@ by (auto intro!: SUP_mono positive_integral_mono Max_ge) qed finally have int_f_eq_y: "positive_integral f = ?y" . - let "?t A" = "\ A - positive_integral (\x. f x * indicator A x)" - have "finite_measure M ?t" proof show "?t {} = 0" by simp @@ -435,9 +418,7 @@ qed qed then interpret M: finite_measure M ?t . - have ac: "absolutely_continuous ?t" using `absolutely_continuous \` unfolding absolutely_continuous_def by auto - have upper_bound: "\A\sets M. ?t A \ 0" proof (rule ccontr) assume "\ ?thesis" @@ -460,7 +441,6 @@ ultimately have b: "b \ 0" "b \ \" using M'.finite_measure_of_space by (auto simp: pinfreal_inverse_eq_0 finite_measure_of_space) - have "finite_measure M (\A. b * \ A)" (is "finite_measure M ?b") proof show "?b {} = 0" by simp @@ -469,7 +449,6 @@ unfolding countably_additive_def psuminf_cmult_right using measure_countably_additive by auto qed - from M.Radon_Nikodym_aux[OF this] obtain A0 where "A0 \ sets M" and space_less_A0: "real (?t (space M)) - real (b * \ (space M)) \ real (?t A0) - real (b * \ A0)" and @@ -479,9 +458,7 @@ using M'.finite_measure b finite_measure by (cases "b * \ B", cases "?t B") (auto simp: field_simps) } note bM_le_t = this - let "?f0 x" = "f x + b * indicator A0 x" - { fix A assume A: "A \ sets M" hence "A \ A0 \ sets M" using `A0 \ sets M` by auto have "positive_integral (\x. ?f0 x * indicator A x) = @@ -492,7 +469,6 @@ using `A0 \ sets M` `A \ A0 \ sets M` A by (simp add: borel_measurable_indicator positive_integral_add positive_integral_cmult_indicator) } note f0_eq = this - { fix A assume A: "A \ sets M" hence "A \ A0 \ sets M" using `A0 \ sets M` by auto have f_le_v: "positive_integral (\x. f x * indicator A x) \ \ A" @@ -511,18 +487,15 @@ finally have "positive_integral (\x. ?f0 x * indicator A x) \ \ A" . } hence "?f0 \ G" using `A0 \ sets M` unfolding G_def by (auto intro!: borel_measurable_indicator borel_measurable_pinfreal_add borel_measurable_pinfreal_times) - have real: "?t (space M) \ \" "?t A0 \ \" "b * \ (space M) \ \" "b * \ A0 \ \" using `A0 \ sets M` b finite_measure[of A0] M.finite_measure[of A0] finite_measure_of_space M.finite_measure_of_space by auto - have int_f_finite: "positive_integral f \ \" using M'.finite_measure_of_space pos_t unfolding pinfreal_zero_less_diff_iff by (auto cong: positive_integral_cong) - have "?t (space M) > b * \ (space M)" unfolding b_def apply (simp add: field_simps) apply (subst mult_assoc[symmetric]) @@ -539,18 +512,15 @@ hence "0 < \ A0" using ac unfolding absolutely_continuous_def using `A0 \ sets M` by auto hence "0 < b * \ A0" using b by auto - from int_f_finite this have "?y + 0 < positive_integral f + b * \ A0" unfolding int_f_eq_y by (rule pinfreal_less_add) also have "\ = positive_integral ?f0" using f0_eq[OF top] `A0 \ sets M` sets_into_space by (simp cong: positive_integral_cong) finally have "?y < positive_integral ?f0" by simp - moreover from `?f0 \ G` have "positive_integral ?f0 \ ?y" by (auto intro!: le_SUPI) ultimately show False by auto qed - show ?thesis proof (safe intro!: bexI[of _ f]) fix A assume "A\sets M" @@ -575,10 +545,8 @@ interpret v: measure_space M \ by fact let ?Q = "{Q\sets M. \ Q \ \}" let ?a = "SUP Q:?Q. \ Q" - have "{} \ ?Q" using v.empty_measure by auto then have Q_not_empty: "?Q \ {}" by blast - have "?a \ \ (space M)" using sets_into_space by (auto intro!: SUP_leI measure_mono top) then have "?a \ \" using finite_measure_of_space @@ -596,9 +564,7 @@ show "range ?O \ sets M" using Q' by (auto intro!: finite_UN) show "\i. ?O i \ ?O (Suc i)" by fastsimp qed - have Q'_sets: "\i. Q' i \ sets M" using Q' by auto - have O_sets: "\i. ?O i \ sets M" using Q' by (auto intro!: finite_UN Un) then have O_in_G: "\i. ?O i \ ?Q" @@ -611,7 +577,6 @@ finally show "\ (?O i) \ \" unfolding pinfreal_less_\ by auto qed auto have O_mono: "\n. ?O n \ ?O (Suc n)" by fastsimp - have a_eq: "?a = \ (\i. ?O i)" unfolding Union[symmetric] proof (rule antisym) show "?a \ (SUP i. \ (?O i))" unfolding a_Lim @@ -625,14 +590,11 @@ using O_in_G[of i] by (auto intro!: exI[of _ "?O i"]) qed qed - let "?O_0" = "(\i. ?O i)" have "?O_0 \ sets M" using Q' by auto - def Q \ "\i. case i of 0 \ Q' 0 | Suc n \ ?O (Suc n) - ?O n" { fix i have "Q i \ sets M" unfolding Q_def using Q'[of 0] by (cases i) (auto intro: O_sets) } note Q_sets = this - show ?thesis proof (intro bexI exI conjI ballI impI allI) show "disjoint_family Q" @@ -640,7 +602,6 @@ split: nat.split_asm) show "range Q \ sets M" using Q_sets by auto - { fix A assume A: "A \ sets M" "A \ space M - ?O_0" show "\ A = 0 \ \ A = 0 \ 0 < \ A \ \ A = \" proof (rule disjCI, simp) @@ -677,7 +638,6 @@ with `\ A \ 0` show ?thesis by auto qed qed } - { fix i show "\ (Q i) \ \" proof (cases i) case 0 then show ?thesis @@ -688,9 +648,7 @@ using `?O n \ ?Q` `?O (Suc n) \ ?Q` O_mono using v.measure_Diff[of "?O n" "?O (Suc n)"] by auto qed } - show "space M - ?O_0 \ sets M" using Q'_sets by auto - { fix j have "(\i\j. ?O i) = (\i\j. Q i)" proof (induct j) case 0 then show ?case by (simp add: Q_def) @@ -713,7 +671,6 @@ shows "\f \ borel_measurable M. \A\sets M. \ A = positive_integral (\x. f x * indicator A x)" proof - interpret v: measure_space M \ by fact - from split_space_into_finite_sets_and_rest[OF assms] obtain Q0 and Q :: "nat \ 'a set" where Q: "disjoint_family Q" "range Q \ sets M" @@ -721,7 +678,6 @@ and in_Q0: "\A. A \ sets M \ A \ Q0 \ \ A = 0 \ \ A = 0 \ 0 < \ A \ \ A = \" and Q_fin: "\i. \ (Q i) \ \" by force from Q have Q_sets: "\i. Q i \ sets M" by auto - have "\i. \f. f\borel_measurable M \ (\A\sets M. \ (Q i \ A) = positive_integral (\x. f x * indicator (Q i \ A) x))" proof @@ -729,7 +685,6 @@ have indicator_eq: "\f x A. (f x :: pinfreal) * indicator (Q i \ A) x * indicator (Q i) x = (f x * indicator (Q i) x) * indicator A x" unfolding indicator_def by auto - have fm: "finite_measure (restricted_space (Q i)) \" (is "finite_measure ?R \") by (rule restricted_finite_measure[OF Q_sets[of i]]) then interpret R: finite_measure ?R . @@ -843,12 +798,6 @@ section "Uniqueness of densities" -lemma (in measure_space) density_is_absolutely_continuous: - assumes "\A. A \ sets M \ \ A = positive_integral (\x. f x * indicator A x)" - shows "absolutely_continuous \" - using assms unfolding absolutely_continuous_def - by (simp add: positive_integral_null_set) - lemma (in measure_space) finite_density_unique: assumes borel: "f \ borel_measurable M" "g \ borel_measurable M" and fin: "positive_integral f < \" @@ -973,19 +922,16 @@ using h_borel by (rule measure_space_density) interpret h: finite_measure M "\A. positive_integral (\x. h x * indicator A x)" by default (simp cong: positive_integral_cong add: fin) - interpret f: measure_space M "\A. positive_integral (\x. f x * indicator A x)" using borel(1) by (rule measure_space_density) interpret f': measure_space M "\A. positive_integral (\x. f' x * indicator A x)" using borel(2) by (rule measure_space_density) - { fix A assume "A \ sets M" then have " {x \ space M. h x \ 0 \ indicator A x \ (0::pinfreal)} = A" using pos sets_into_space by (force simp: indicator_def) then have "positive_integral (\xa. h xa * indicator A xa) = 0 \ A \ null_sets" using h_borel `A \ sets M` by (simp add: positive_integral_0_iff) } note h_null_sets = this - { fix A assume "A \ sets M" have "positive_integral (\x. h x * (f x * indicator A x)) = f.positive_integral (\x. h x * indicator A x)" @@ -1101,7 +1047,7 @@ qed qed -section "Radon Nikodym derivative" +section "Radon-Nikodym derivative" definition (in sigma_finite_measure) "RN_deriv \ \ SOME f. f \ borel_measurable M \ diff -r 94427db32392 -r 688f6ff859e1 src/HOL/Probability/Sigma_Algebra.thy --- a/src/HOL/Probability/Sigma_Algebra.thy Wed Dec 01 20:12:53 2010 +0100 +++ b/src/HOL/Probability/Sigma_Algebra.thy Wed Dec 01 21:03:02 2010 +0100 @@ -403,6 +403,12 @@ shows "sets (sigma N) \ sets M" by (unfold assms sets_sigma, rule sigma_sets_subset, rule assms) +lemma in_sigma[intro, simp]: "A \ sets M \ A \ sets (sigma M)" + unfolding sigma_def by (auto intro!: sigma_sets.Basic) + +lemma (in sigma_algebra) sigma_eq[simp]: "sigma M = M" + unfolding sigma_def sigma_sets_eq by simp + section {* Measurable functions *} definition @@ -865,6 +871,22 @@ qed qed +lemma vimage_algebra_sigma: + assumes E: "sets E \ Pow (space E)" + and f: "f \ space F \ space E" + and "\A. A \ sets F \ A \ (\X. f -` X \ space F) ` sets E" + and "\A. A \ sets E \ f -` A \ space F \ sets F" + shows "sigma_algebra.vimage_algebra (sigma E) (space 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" + using assms by auto + show "vimage_algebra (space F) f = sigma F" + unfolding vimage_algebra_def using assms + by (simp add: sigma_def eq sigma_sets_vimage) +qed + section {* Conditional space *} definition (in algebra)