# HG changeset patch # User hoelzl # Date 1283440360 -7200 # Node ID 98de4085985867c63b78fbc90824349eac4203e3 # Parent 11314c196e119dda4c87e8478fd042ce9262e1ae move lemmas to correct theory files diff -r 11314c196e11 -r 98de40859858 src/HOL/Probability/Borel.thy --- a/src/HOL/Probability/Borel.thy Fri Aug 27 16:23:51 2010 +0200 +++ b/src/HOL/Probability/Borel.thy Thu Sep 02 17:12:40 2010 +0200 @@ -6,6 +6,10 @@ imports Sigma_Algebra Positive_Infinite_Real Multivariate_Analysis begin +lemma LIMSEQ_max: + "u ----> (x::real) \ (\i. max (u i) 0) ----> max x 0" + by (fastsimp intro!: LIMSEQ_I dest!: LIMSEQ_D) + section "Generic Borel spaces" definition "borel_space = sigma (UNIV::'a::topological_space set) open" @@ -105,6 +109,53 @@ qed (auto simp add: vimage_UN) qed +lemma (in sigma_algebra) borel_measurable_restricted: + fixes f :: "'a \ 'x\{topological_space, semiring_1}" assumes "A \ sets M" + shows "f \ borel_measurable (restricted_space A) \ + (\x. f x * indicator A x) \ borel_measurable M" + (is "f \ borel_measurable ?R \ ?f \ borel_measurable M") +proof - + interpret R: sigma_algebra ?R by (rule restricted_sigma_algebra[OF `A \ sets M`]) + have *: "f \ borel_measurable ?R \ ?f \ borel_measurable ?R" + by (auto intro!: measurable_cong) + show ?thesis unfolding * + unfolding in_borel_measurable_borel_space + proof (simp, safe) + fix S :: "'x set" assume "S \ sets borel_space" + "\S\sets borel_space. ?f -` S \ A \ op \ A ` sets M" + then have "?f -` S \ A \ op \ A ` sets M" by auto + then have f: "?f -` S \ A \ sets M" + using `A \ sets M` sets_into_space by fastsimp + show "?f -` S \ space M \ sets M" + proof cases + assume "0 \ S" + then have "?f -` S \ space M = ?f -` S \ A \ (space M - A)" + using `A \ sets M` sets_into_space by auto + then show ?thesis using f `A \ sets M` by (auto intro!: Un Diff) + next + assume "0 \ S" + then have "?f -` S \ space M = ?f -` S \ A" + using `A \ sets M` sets_into_space + by (auto simp: indicator_def split: split_if_asm) + then show ?thesis using f by auto + qed + next + fix S :: "'x set" assume "S \ sets borel_space" + "\S\sets borel_space. ?f -` S \ space M \ sets M" + then have f: "?f -` S \ space M \ sets M" by auto + then show "?f -` S \ A \ op \ A ` sets M" + using `A \ sets M` sets_into_space + apply (simp add: image_iff) + apply (rule bexI[OF _ f]) + by auto + qed +qed + +lemma (in sigma_algebra) borel_measurable_subalgebra: + assumes "N \ sets M" "f \ borel_measurable (M\sets:=N\)" + shows "f \ borel_measurable M" + using assms unfolding measurable_def by auto + section "Borel spaces on euclidean spaces" lemma lessThan_borel[simp, intro]: @@ -1294,4 +1345,46 @@ using assms by auto qed +lemma (in sigma_algebra) borel_measurable_psuminf: + assumes "\i. f i \ borel_measurable M" + shows "(\x. (\\<^isub>\ i. f i x)) \ borel_measurable M" + using assms unfolding psuminf_def + by (auto intro!: borel_measurable_SUP[unfolded SUPR_fun_expand]) + +section "LIMSEQ is borel measurable" + +lemma (in sigma_algebra) borel_measurable_LIMSEQ: + fixes u :: "nat \ 'a \ real" + assumes u': "\x. x \ space M \ (\i. u i x) ----> u' x" + and u: "\i. u i \ borel_measurable M" + shows "u' \ borel_measurable M" +proof - + let "?pu x i" = "max (u i x) 0" + let "?nu x i" = "max (- u i x) 0" + + { fix x assume x: "x \ space M" + have "(?pu x) ----> max (u' x) 0" + "(?nu x) ----> max (- u' x) 0" + using u'[OF x] by (auto intro!: LIMSEQ_max LIMSEQ_minus) + from LIMSEQ_imp_lim_INF[OF _ this(1)] LIMSEQ_imp_lim_INF[OF _ this(2)] + have "(SUP n. INF m. Real (u (n + m) x)) = Real (u' x)" + "(SUP n. INF m. Real (- u (n + m) x)) = Real (- u' x)" + by (simp_all add: Real_max'[symmetric]) } + note eq = this + + have *: "\x. real (Real (u' x)) - real (Real (- u' x)) = u' x" + by auto + + have "(SUP n. INF m. (\x. Real (u (n + m) x))) \ borel_measurable M" + "(SUP n. INF m. (\x. Real (- u (n + m) x))) \ borel_measurable M" + using u by (auto intro: borel_measurable_SUP borel_measurable_INF borel_measurable_Real) + with eq[THEN measurable_cong, of M "\x. x" borel_space] + have "(\x. Real (u' x)) \ borel_measurable M" + "(\x. Real (- u' x)) \ borel_measurable M" + unfolding SUPR_fun_expand INFI_fun_expand by auto + note this[THEN borel_measurable_real] + from borel_measurable_diff[OF this] + show ?thesis unfolding * . +qed + end diff -r 11314c196e11 -r 98de40859858 src/HOL/Probability/Information.thy --- a/src/HOL/Probability/Information.thy Fri Aug 27 16:23:51 2010 +0200 +++ b/src/HOL/Probability/Information.thy Thu Sep 02 17:12:40 2010 +0200 @@ -359,6 +359,48 @@ "(\x\A \ B. f x) = (\x\A. setsum (\y. f (x, y)) B)" unfolding setsum_cartesian_product by simp +lemma (in finite_information_space) mutual_information_generic_eq: + assumes MX: "finite_measure_space MX (distribution X)" + assumes MY: "finite_measure_space MY (distribution Y)" + shows "mutual_information b MX MY X Y = (\ (x,y) \ space MX \ space MY. + real (joint_distribution X Y {(x,y)}) * + log b (real (joint_distribution X Y {(x,y)}) / + (real (distribution X {x}) * real (distribution Y {y}))))" +proof - + let ?P = "prod_measure_space MX MY" + let ?\ = "prod_measure MX (distribution X) MY (distribution Y)" + let ?\ = "joint_distribution X Y" + interpret X: finite_measure_space MX "distribution X" by fact + moreover interpret Y: finite_measure_space MY "distribution Y" by fact + have fms: "finite_measure_space MX (distribution X)" + "finite_measure_space MY (distribution Y)" by fact+ + have fms_P: "finite_measure_space ?P ?\" + by (rule X.finite_measure_space_finite_prod_measure) fact + then interpret P: finite_measure_space ?P ?\ . + have fms_P': "finite_measure_space ?P ?\" + using finite_product_measure_space[of "space MX" "space MY"] + X.finite_space Y.finite_space sigma_prod_sets_finite[OF X.finite_space Y.finite_space] + X.sets_eq_Pow Y.sets_eq_Pow + by (simp add: prod_measure_space_def sigma_def) + then interpret P': finite_measure_space ?P ?\ . + { fix x assume "x \ space ?P" + hence in_MX: "{fst x} \ sets MX" "{snd x} \ sets MY" using X.sets_eq_Pow Y.sets_eq_Pow + by (auto simp: prod_measure_space_def) + assume "?\ {x} = 0" + with X.finite_prod_measure_times[OF fms(2), of "{fst x}" "{snd x}"] in_MX + have "distribution X {fst x} = 0 \ distribution Y {snd x} = 0" + by (simp add: prod_measure_space_def) + hence "joint_distribution X Y {x} = 0" + by (cases x) (auto simp: distribution_order) } + note measure_0 = this + show ?thesis + unfolding Let_def mutual_information_def + using measure_0 fms_P fms_P' MX MY P.absolutely_continuous_def + by (subst P.KL_divergence_eq_finite) + (auto simp add: prod_measure_space_def prod_measure_times_finite + finite_prob_space_eq setsum_cartesian_product' real_of_pinfreal_mult[symmetric]) +qed + lemma (in finite_information_space) assumes MX: "finite_prob_space MX (distribution X)" assumes MY: "finite_prob_space MY (distribution Y)" diff -r 11314c196e11 -r 98de40859858 src/HOL/Probability/Lebesgue_Integration.thy --- a/src/HOL/Probability/Lebesgue_Integration.thy Fri Aug 27 16:23:51 2010 +0200 +++ b/src/HOL/Probability/Lebesgue_Integration.thy Thu Sep 02 17:12:40 2010 +0200 @@ -209,19 +209,6 @@ by (auto intro!: **) qed -lemma setsum_indicator_disjoint_family: - fixes f :: "'d \ 'e::semiring_1" - assumes d: "disjoint_family_on A P" and "x \ A j" and "finite P" and "j \ P" - shows "(\i\P. f i * indicator (A i) x) = f j" -proof - - have "P \ {i. x \ A i} = {j}" - using d `x \ A j` `j \ P` unfolding disjoint_family_on_def - by auto - thus ?thesis - unfolding indicator_def - by (simp add: if_distrib setsum_cases[OF `finite P`]) -qed - lemma (in sigma_algebra) borel_measurable_implies_simple_function_sequence: fixes u :: "'a \ pinfreal" assumes u: "u \ borel_measurable M" @@ -426,6 +413,62 @@ with x show thesis by (auto intro!: that[of f]) qed +lemma (in sigma_algebra) simple_function_eq_borel_measurable: + fixes f :: "'a \ pinfreal" + shows "simple_function f \ + finite (f`space M) \ f \ borel_measurable M" + using simple_function_borel_measurable[of f] + borel_measurable_simple_function[of f] + by (fastsimp simp: simple_function_def) + +lemma (in measure_space) simple_function_restricted: + fixes f :: "'a \ pinfreal" assumes "A \ sets M" + shows "sigma_algebra.simple_function (restricted_space A) f \ simple_function (\x. f x * indicator A x)" + (is "sigma_algebra.simple_function ?R f \ simple_function ?f") +proof - + interpret R: sigma_algebra ?R by (rule restricted_sigma_algebra[OF `A \ sets M`]) + have "finite (f`A) \ finite (?f`space M)" + proof cases + assume "A = space M" + then have "f`A = ?f`space M" by (fastsimp simp: image_iff) + then show ?thesis by simp + next + assume "A \ space M" + then obtain x where x: "x \ space M" "x \ A" + using sets_into_space `A \ sets M` by auto + have *: "?f`space M = f`A \ {0}" + proof (auto simp add: image_iff) + show "\x\space M. f x = 0 \ indicator A x = 0" + using x by (auto intro!: bexI[of _ x]) + next + fix x assume "x \ A" + then show "\y\space M. f x = f y * indicator A y" + using `A \ sets M` sets_into_space by (auto intro!: bexI[of _ x]) + next + fix x + assume "indicator A x \ (0::pinfreal)" + then have "x \ A" by (auto simp: indicator_def split: split_if_asm) + moreover assume "x \ space M" "\y\A. ?f x \ f y" + ultimately show "f x = 0" by auto + qed + then show ?thesis by auto + qed + then show ?thesis + unfolding simple_function_eq_borel_measurable + R.simple_function_eq_borel_measurable + unfolding borel_measurable_restricted[OF `A \ sets M`] + by auto +qed + +lemma (in sigma_algebra) simple_function_subalgebra: + assumes "sigma_algebra.simple_function (M\sets:=N\) f" + and N_subalgebra: "N \ sets M" "sigma_algebra (M\sets:=N\)" + shows "simple_function f" + using assms + unfolding simple_function_def + unfolding sigma_algebra.simple_function_def[OF N_subalgebra(2)] + by auto + section "Simple integral" definition (in measure_space) @@ -668,6 +711,41 @@ qed qed +lemma (in measure_space) simple_integral_restricted: + assumes "A \ sets M" + assumes sf: "simple_function (\x. f x * indicator A x)" + shows "measure_space.simple_integral (restricted_space A) \ f = simple_integral (\x. f x * indicator A x)" + (is "_ = simple_integral ?f") + unfolding measure_space.simple_integral_def[OF restricted_measure_space[OF `A \ sets M`]] + unfolding simple_integral_def +proof (simp, safe intro!: setsum_mono_zero_cong_left) + from sf show "finite (?f ` space M)" + unfolding simple_function_def by auto +next + fix x assume "x \ A" + then show "f x \ ?f ` space M" + using sets_into_space `A \ sets M` by (auto intro!: image_eqI[of _ _ x]) +next + fix x assume "x \ space M" "?f x \ f`A" + then have "x \ A" by (auto simp: image_iff) + then show "?f x * \ (?f -` {?f x} \ space M) = 0" by simp +next + fix x assume "x \ A" + then have "f x \ 0 \ + f -` {f x} \ A = ?f -` {f x} \ space M" + using `A \ sets M` sets_into_space + by (auto simp: indicator_def split: split_if_asm) + then show "f x * \ (f -` {f x} \ A) = + f x * \ (?f -` {f x} \ space M)" + unfolding pinfreal_mult_cancel_left by auto +qed + +lemma (in measure_space) simple_integral_subalgebra[simp]: + assumes "measure_space (M\sets := N\) \" + shows "measure_space.simple_integral (M\sets := N\) \ = simple_integral" + unfolding simple_integral_def_raw + unfolding measure_space.simple_integral_def_raw[OF assms] by simp + section "Continuous posititve integration" definition (in measure_space) @@ -1077,6 +1155,43 @@ qed qed +lemma (in measure_space) positive_integral_translated_density: + assumes "f \ borel_measurable M" "g \ borel_measurable M" + shows "measure_space.positive_integral M (\A. positive_integral (\x. f x * indicator A x)) g = + positive_integral (\x. f x * g x)" (is "measure_space.positive_integral M ?T _ = _") +proof - + from measure_space_density[OF assms(1)] + interpret T: measure_space M ?T . + from borel_measurable_implies_simple_function_sequence[OF assms(2)] + obtain G where G: "\i. simple_function (G i)" "G \ g" by blast + note G_borel = borel_measurable_simple_function[OF this(1)] + from T.positive_integral_isoton[OF `G \ g` G_borel] + have *: "(\i. T.positive_integral (G i)) \ T.positive_integral g" . + { fix i + have [simp]: "finite (G i ` space M)" + using G(1) unfolding simple_function_def by auto + have "T.positive_integral (G i) = T.simple_integral (G i)" + using G T.positive_integral_eq_simple_integral by simp + also have "\ = positive_integral (\x. f x * (\y\G i`space M. y * indicator (G i -` {y} \ space M) x))" + apply (simp add: T.simple_integral_def) + apply (subst positive_integral_cmult[symmetric]) + using G_borel assms(1) apply (fastsimp intro: borel_measurable_indicator borel_measurable_vimage) + apply (subst positive_integral_setsum[symmetric]) + using G_borel assms(1) apply (fastsimp intro: borel_measurable_indicator borel_measurable_vimage) + by (simp add: setsum_right_distrib field_simps) + also have "\ = positive_integral (\x. f x * G i x)" + by (auto intro!: positive_integral_cong + simp: indicator_def if_distrib setsum_cases) + finally have "T.positive_integral (G i) = positive_integral (\x. f x * G i x)" . } + with * have eq_Tg: "(\i. positive_integral (\x. f x * G i x)) \ T.positive_integral g" by simp + from G(2) have "(\i x. f x * G i x) \ (\x. f x * g x)" + unfolding isoton_fun_expand by (auto intro!: isoton_cmult_right) + then have "(\i. positive_integral (\x. f x * G i x)) \ positive_integral (\x. f x * g x)" + using assms(1) G_borel by (auto intro!: positive_integral_isoton borel_measurable_pinfreal_times) + with eq_Tg show "T.positive_integral g = positive_integral (\x. f x * g x)" + unfolding isoton_def by simp +qed + lemma (in measure_space) positive_integral_null_set: assumes borel: "u \ borel_measurable M" and "N \ null_sets" shows "positive_integral (\x. u x * indicator N x) = 0" (is "?I = 0") @@ -1222,6 +1337,58 @@ finally show ?thesis by simp qed +lemma (in measure_space) positive_integral_restricted: + assumes "A \ sets M" + shows "measure_space.positive_integral (restricted_space A) \ f = positive_integral (\x. f x * indicator A x)" + (is "measure_space.positive_integral ?R \ f = positive_integral ?f") +proof - + have msR: "measure_space ?R \" by (rule restricted_measure_space[OF `A \ sets M`]) + then interpret R: measure_space ?R \ . + have saR: "sigma_algebra ?R" by fact + have *: "R.positive_integral f = R.positive_integral ?f" + by (auto intro!: R.positive_integral_cong) + show ?thesis + unfolding * R.positive_integral_def positive_integral_def + unfolding simple_function_restricted[OF `A \ sets M`] + apply (simp add: SUPR_def) + apply (rule arg_cong[where f=Sup]) + proof (auto simp: 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) \ + 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 expand_fun_eq indicator_def split: split_if_asm) + from g show "\x. simple_function (\xa. x xa * indicator A xa) \ x \ f \ (\xa\A. \ \ x xa) \ + 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"]) + by (fastsimp simp: le_fun_def *) + qed +qed + +lemma (in measure_space) positive_integral_subalgebra[simp]: + assumes borel: "f \ borel_measurable (M\sets := N\)" + and N_subalgebra: "N \ sets M" "sigma_algebra (M\sets := N\)" + shows "measure_space.positive_integral (M\sets := N\) \ f = positive_integral f" +proof - + note msN = measure_space_subalgebra[OF N_subalgebra] + then interpret N: measure_space "M\sets:=N\" \ . + from N.borel_measurable_implies_simple_function_sequence[OF borel] + obtain fs where Nsf: "\i. N.simple_function (fs i)" and "fs \ f" by blast + then have sf: "\i. simple_function (fs i)" + using simple_function_subalgebra[OF _ N_subalgebra] by blast + from positive_integral_isoton_simple[OF `fs \ f` sf] N.positive_integral_isoton_simple[OF `fs \ f` Nsf] + show ?thesis unfolding simple_integral_subalgebra[OF msN] isoton_def by simp +qed + section "Lebesgue Integral" definition (in measure_space) integrable where @@ -1629,44 +1796,6 @@ by (simp add: real_of_pinfreal_eq_0) qed -lemma LIMSEQ_max: - "u ----> (x::real) \ (\i. max (u i) 0) ----> max x 0" - by (fastsimp intro!: LIMSEQ_I dest!: LIMSEQ_D) - -lemma (in sigma_algebra) borel_measurable_LIMSEQ: - fixes u :: "nat \ 'a \ real" - assumes u': "\x. x \ space M \ (\i. u i x) ----> u' x" - and u: "\i. u i \ borel_measurable M" - shows "u' \ borel_measurable M" -proof - - let "?pu x i" = "max (u i x) 0" - let "?nu x i" = "max (- u i x) 0" - - { fix x assume x: "x \ space M" - have "(?pu x) ----> max (u' x) 0" - "(?nu x) ----> max (- u' x) 0" - using u'[OF x] by (auto intro!: LIMSEQ_max LIMSEQ_minus) - from LIMSEQ_imp_lim_INF[OF _ this(1)] LIMSEQ_imp_lim_INF[OF _ this(2)] - have "(SUP n. INF m. Real (u (n + m) x)) = Real (u' x)" - "(SUP n. INF m. Real (- u (n + m) x)) = Real (- u' x)" - by (simp_all add: Real_max'[symmetric]) } - note eq = this - - have *: "\x. real (Real (u' x)) - real (Real (- u' x)) = u' x" - by auto - - have "(SUP n. INF m. (\x. Real (u (n + m) x))) \ borel_measurable M" - "(SUP n. INF m. (\x. Real (- u (n + m) x))) \ borel_measurable M" - using u by (auto intro: borel_measurable_SUP borel_measurable_INF borel_measurable_Real) - with eq[THEN measurable_cong, of M "\x. x" borel_space] - have "(\x. Real (u' x)) \ borel_measurable M" - "(\x. Real (- u' x)) \ borel_measurable M" - unfolding SUPR_fun_expand INFI_fun_expand by auto - note this[THEN borel_measurable_real] - from borel_measurable_diff[OF this] - show ?thesis unfolding * . -qed - lemma (in measure_space) integral_dominated_convergence: assumes u: "\i. integrable (u i)" and bound: "\x j. x\space M \ \u j x\ \ w x" and w: "integrable w" "\x. x \ space M \ 0 \ w x" @@ -1926,41 +2055,11 @@ by (simp_all add: integral_cmul_indicator borel_measurable_vimage) qed -lemma sigma_algebra_cong: - fixes M :: "('a, 'b) algebra_scheme" and M' :: "('a, 'c) algebra_scheme" - assumes *: "sigma_algebra M" - and cong: "space M = space M'" "sets M = sets M'" - shows "sigma_algebra M'" -using * unfolding sigma_algebra_def algebra_def sigma_algebra_axioms_def unfolding cong . - -lemma finite_Pow_additivity_sufficient: - assumes "finite (space M)" and "sets M = Pow (space M)" - and "positive \" and "additive M \" - and "\x. x \ space M \ \ {x} \ \" - shows "finite_measure_space M \" -proof - - have "sigma_algebra M" - using assms by (auto intro!: sigma_algebra_cong[OF sigma_algebra_Pow]) - - have "measure_space M \" - by (rule sigma_algebra.finite_additivity_sufficient) (fact+) - thus ?thesis - unfolding finite_measure_space_def finite_measure_space_axioms_def - using assms by simp -qed - -lemma finite_measure_spaceI: - assumes "measure_space M \" and "finite (space M)" and "sets M = Pow (space M)" - and "\x. x \ space M \ \ {x} \ \" - shows "finite_measure_space M \" - unfolding finite_measure_space_def finite_measure_space_axioms_def - using assms by simp +lemma (in finite_measure_space) simple_function_finite[simp, intro]: "simple_function f" + unfolding simple_function_def sets_eq_Pow using finite_space by auto lemma (in finite_measure_space) borel_measurable_finite[intro, simp]: "f \ borel_measurable M" - unfolding measurable_def sets_eq_Pow by auto - -lemma (in finite_measure_space) simple_function_finite: "simple_function f" - unfolding simple_function_def sets_eq_Pow using finite_space by auto + by (auto intro: borel_measurable_simple_function) lemma (in finite_measure_space) positive_integral_finite_eq_setsum: "positive_integral f = (\x \ space M. f x * \ {x})" @@ -1979,10 +2078,8 @@ "positive_integral (\x. Real (f x)) = (\x \ space M. Real (f x) * \ {x})" "positive_integral (\x. Real (- f x)) = (\x \ space M. Real (- f x) * \ {x})" unfolding positive_integral_finite_eq_setsum by auto - show "integrable f" using finite_space finite_measure by (simp add: setsum_\ integrable_def sets_eq_Pow) - show ?I using finite_measure apply (simp add: integral_def sets_eq_Pow real_of_pinfreal_setsum[symmetric] real_of_pinfreal_mult[symmetric] setsum_subtractf[symmetric]) diff -r 11314c196e11 -r 98de40859858 src/HOL/Probability/Measure.thy --- a/src/HOL/Probability/Measure.thy Fri Aug 27 16:23:51 2010 +0200 +++ b/src/HOL/Probability/Measure.thy Thu Sep 02 17:12:40 2010 +0200 @@ -414,6 +414,19 @@ finally show ?thesis . qed +lemma (in measure_space) measure_finitely_subadditive: + assumes "finite I" "A ` I \ sets M" + shows "\ (\i\I. A i) \ (\i\I. \ (A i))" +using assms proof induct + case (insert i I) + then have "(\i\I. A i) \ sets M" by (auto intro: finite_UN) + then have "\ (\i\insert i I. A i) \ \ (A i) + \ (\i\I. A i)" + using insert by (simp add: measure_subadditive) + also have "\ \ (\i\insert i I. \ (A i))" + using insert by (auto intro!: add_left_mono) + finally show ?case . +qed simp + lemma (in measure_space) measurable_countably_subadditive: assumes "range f \ sets M" shows "\ (\i. f i) \ (\\<^isub>\ i. \ (f i))" @@ -432,9 +445,34 @@ finally show ?thesis . qed +lemma (in measure_space) measure_inter_full_set: + assumes "S \ sets M" "T \ sets M" and not_\: "\ (T - S) \ \" + assumes T: "\ T = \ (space M)" + shows "\ (S \ T) = \ S" +proof (rule antisym) + show " \ (S \ T) \ \ S" + using assms by (auto intro!: measure_mono) + + show "\ S \ \ (S \ T)" + proof (rule ccontr) + assume contr: "\ ?thesis" + have "\ (space M) = \ ((T - S) \ (S \ T))" + unfolding T[symmetric] by (auto intro!: arg_cong[where f="\"]) + also have "\ \ \ (T - S) + \ (S \