# HG changeset patch # User hoelzl # Date 1353087957 -3600 # Node ID de19856feb5468549d04ff5095134fe7fa8f5e81 # Parent 3d89c38408cd72170e74d3c794d2817e4e6acd00 move theorems to be more generally useable diff -r 3d89c38408cd -r de19856feb54 src/HOL/Library/Extended_Real.thy --- a/src/HOL/Library/Extended_Real.thy Fri Nov 16 18:49:46 2012 +0100 +++ b/src/HOL/Library/Extended_Real.thy Fri Nov 16 18:45:57 2012 +0100 @@ -124,7 +124,6 @@ fix x :: ereal show "x \ range uminus" by (intro image_eqI[of _ _ "-x"]) auto qed auto - instantiation ereal :: abs begin function abs_ereal where @@ -145,6 +144,9 @@ lemma abs_ereal_uminus[simp]: "\- x\ = \x::ereal\" by (cases x) auto +lemma ereal_infinity_cases: "(a::ereal) \ \ \ a \ -\ \ \a\ \ \" + by auto + subsubsection "Addition" instantiation ereal :: comm_monoid_add @@ -530,6 +532,9 @@ qed end +lemma real_ereal_1[simp]: "real (1::ereal) = 1" + unfolding one_ereal_def by simp + lemma real_of_ereal_le_1: fixes a :: ereal shows "a \ 1 \ real a \ 1" by (cases a) (auto simp: one_ereal_def) @@ -659,6 +664,16 @@ shows "0 < a * b \ (0 < a \ 0 < b) \ (a < 0 \ b < 0)" by (cases rule: ereal2_cases[of a b]) (simp_all add: zero_less_mult_iff) +lemma ereal_left_mult_cong: + fixes a b c :: ereal + shows "(c \ 0 \ a = b) \ c * a = c * b" + by (cases "c = 0") simp_all + +lemma ereal_right_mult_cong: + fixes a b c :: ereal + shows "(c \ 0 \ a = b) \ a * c = b * c" + by (cases "c = 0") simp_all + lemma ereal_distrib: fixes a b c :: ereal assumes "a \ \ \ b \ -\" "a \ -\ \ b \ \" "\c\ \ \" @@ -941,6 +956,10 @@ using assms apply (cases x, cases e) apply auto done +lemma ereal_minus_eq_PInfty_iff: + fixes x y :: ereal shows "x - y = \ \ y = -\ \ x = \" + by (cases x y rule: ereal2_cases) simp_all + subsubsection {* Division *} instantiation ereal :: inverse diff -r 3d89c38408cd -r de19856feb54 src/HOL/Library/FuncSet.thy --- a/src/HOL/Library/FuncSet.thy Fri Nov 16 18:49:46 2012 +0100 +++ b/src/HOL/Library/FuncSet.thy Fri Nov 16 18:45:57 2012 +0100 @@ -81,7 +81,10 @@ by (simp add: Pi_def) lemma funcset_image: "f \ A\B ==> f ` A \ B" -by auto + by auto + +lemma image_subset_iff_funcset: "F ` A \ B \ F \ A \ B" + by auto lemma Pi_eq_empty[simp]: "((PI x: A. B x) = {}) = (\x\A. B(x) = {})" apply (simp add: Pi_def, auto) diff -r 3d89c38408cd -r de19856feb54 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri Nov 16 18:49:46 2012 +0100 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri Nov 16 18:45:57 2012 +0100 @@ -5914,4 +5914,71 @@ } ultimately show ?thesis by blast qed + +lemma convex_le_Inf_differential: + fixes f :: "real \ real" + assumes "convex_on I f" + assumes "x \ interior I" "y \ I" + shows "f y \ f x + Inf ((\t. (f x - f t) / (x - t)) ` ({x<..} \ I)) * (y - x)" + (is "_ \ _ + Inf (?F x) * (y - x)") +proof (cases rule: linorder_cases) + assume "x < y" + moreover + have "open (interior I)" by auto + from openE[OF this `x \ interior I`] guess e . note e = this + moreover def t \ "min (x + e / 2) ((x + y) / 2)" + ultimately have "x < t" "t < y" "t \ ball x e" + by (auto simp: dist_real_def field_simps split: split_min) + with `x \ interior I` e interior_subset[of I] have "t \ I" "x \ I" by auto + + have "open (interior I)" by auto + from openE[OF this `x \ interior I`] guess e . + moreover def K \ "x - e / 2" + with `0 < e` have "K \ ball x e" "K < x" by (auto simp: dist_real_def) + ultimately have "K \ I" "K < x" "x \ I" + using interior_subset[of I] `x \ interior I` by auto + + have "Inf (?F x) \ (f x - f y) / (x - y)" + proof (rule Inf_lower2) + show "(f x - f t) / (x - t) \ ?F x" + using `t \ I` `x < t` by auto + show "(f x - f t) / (x - t) \ (f x - f y) / (x - y)" + using `convex_on I f` `x \ I` `y \ I` `x < t` `t < y` by (rule convex_on_diff) + next + fix y assume "y \ ?F x" + with order_trans[OF convex_on_diff[OF `convex_on I f` `K \ I` _ `K < x` _]] + show "(f K - f x) / (K - x) \ y" by auto + qed + then show ?thesis + using `x < y` by (simp add: field_simps) +next + assume "y < x" + moreover + have "open (interior I)" by auto + from openE[OF this `x \ interior I`] guess e . note e = this + moreover def t \ "x + e / 2" + ultimately have "x < t" "t \ ball x e" + by (auto simp: dist_real_def field_simps) + with `x \ interior I` e interior_subset[of I] have "t \ I" "x \ I" by auto + + have "(f x - f y) / (x - y) \ Inf (?F x)" + proof (rule Inf_greatest) + have "(f x - f y) / (x - y) = (f y - f x) / (y - x)" + using `y < x` by (auto simp: field_simps) + also + fix z assume "z \ ?F x" + with order_trans[OF convex_on_diff[OF `convex_on I f` `y \ I` _ `y < x`]] + have "(f y - f x) / (y - x) \ z" by auto + finally show "(f x - f y) / (x - y) \ z" . + next + have "open (interior I)" by auto + from openE[OF this `x \ interior I`] guess e . note e = this + then have "x + e / 2 \ ball x e" by (auto simp: dist_real_def) + with e interior_subset[of I] have "x + e / 2 \ {x<..} \ I" by auto + then show "?F x \ {}" by blast + qed + then show ?thesis + using `y < x` by (simp add: field_simps) +qed simp + end diff -r 3d89c38408cd -r de19856feb54 src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy --- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Fri Nov 16 18:49:46 2012 +0100 +++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Fri Nov 16 18:45:57 2012 +0100 @@ -423,6 +423,11 @@ using ereal_Lim_uminus[of f f0] lim_imp_Liminf[of net "(%x. -(f x))" "-f0"] ereal_Liminf_uminus[of net f] assms by simp +lemma convergent_ereal_limsup: + fixes X :: "nat \ ereal" + shows "convergent X \ limsup X = lim X" + by (auto simp: convergent_def limI lim_imp_Limsup) + lemma Liminf_PInfty: fixes f :: "'a \ ereal" assumes "\ trivial_limit net" @@ -486,6 +491,12 @@ shows "(f ---> f0) net \ Liminf net f = f0 \ Limsup net f = f0" by (metis assms ereal_Liminf_eq_Limsup lim_imp_Liminf lim_imp_Limsup) +lemma convergent_ereal: + fixes X :: "nat \ ereal" + shows "convergent X \ limsup X = liminf X" + using ereal_Liminf_eq_Limsup_iff[of sequentially] + by (auto simp: convergent_def) + lemma limsup_INFI_SUPR: fixes f :: "nat \ ereal" shows "limsup f = (INF n. SUP m:{n..}. f m)" @@ -1496,4 +1507,20 @@ by induct (simp_all add: suminf_add_ereal setsum_nonneg) qed simp +lemma suminf_ereal_eq_0: + fixes f :: "nat \ ereal" + assumes nneg: "\i. 0 \ f i" + shows "(\i. f i) = 0 \ (\i. f i = 0)" +proof + assume "(\i. f i) = 0" + { fix i assume "f i \ 0" + with nneg have "0 < f i" by (auto simp: less_le) + also have "f i = (\j. if j = i then f i else 0)" + by (subst suminf_finite[where N="{i}"]) auto + also have "\ \ (\i. f i)" + using nneg by (auto intro!: suminf_le_pos) + finally have False using `(\i. f i) = 0` by auto } + then show "\i. f i = 0" by auto +qed simp + end diff -r 3d89c38408cd -r de19856feb54 src/HOL/Multivariate_Analysis/Integration.thy --- a/src/HOL/Multivariate_Analysis/Integration.thy Fri Nov 16 18:49:46 2012 +0100 +++ b/src/HOL/Multivariate_Analysis/Integration.thy Fri Nov 16 18:45:57 2012 +0100 @@ -483,6 +483,13 @@ show ?thesis unfolding content_def using assms by (auto simp: *) qed +lemma content_singleton[simp]: "content {a} = 0" +proof - + have "content {a .. a} = 0" + by (subst content_closed_interval) auto + then show ?thesis by simp +qed + lemma content_unit[intro]: "content{0..One::'a::ordered_euclidean_space} = 1" proof - have *: "\i (One::'a)$$i" by auto @@ -1665,6 +1672,16 @@ unfolding o_def[THEN sym] apply(rule has_integral_linear,assumption) by(rule bounded_linear_scaleR_right) +lemma has_integral_cmult_real: + fixes c :: real + assumes "c \ 0 \ (f has_integral x) A" + shows "((\x. c * f x) has_integral c * x) A" +proof cases + assume "c \ 0" + from has_integral_cmul[OF assms[OF this], of c] show ?thesis + unfolding real_scaleR_def . +qed simp + lemma has_integral_neg: shows "(f has_integral k) s \ ((\x. -(f x)) has_integral (-k)) s" apply(drule_tac c="-1" in has_integral_cmul) by auto @@ -1746,6 +1763,12 @@ shows "f integrable_on s \ (\x. c *\<^sub>R f(x)) integrable_on s" unfolding integrable_on_def by(auto intro: has_integral_cmul) +lemma integrable_on_cmult_iff: + fixes c :: real assumes "c \ 0" + shows "(\x. c * f x) integrable_on s \ f integrable_on s" + using integrable_cmul[of "\x. c * f x" s "1 / c"] integrable_cmul[of f s c] `c \ 0` + by auto + lemma integrable_neg: shows "f integrable_on s \ (\x. -f(x)) integrable_on s" unfolding integrable_on_def by(auto intro: has_integral_neg) @@ -2669,6 +2692,11 @@ unfolding split_def apply(subst scaleR_left.setsum[THEN sym, unfolded o_def]) defer apply(subst additive_content_tagged_division[unfolded split_def]) apply assumption by auto +lemma integral_const[simp]: + fixes a b :: "'a::ordered_euclidean_space" + shows "integral {a .. b} (\x. c) = content {a .. b} *\<^sub>R c" + by (rule integral_unique) (rule has_integral_const) + subsection {* Bounds on the norm of Riemann sums and the integral itself. *} lemma dsum_bound: assumes "p division_of {a..b}" "norm(c) \ e" diff -r 3d89c38408cd -r de19856feb54 src/HOL/Multivariate_Analysis/Linear_Algebra.thy --- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Fri Nov 16 18:49:46 2012 +0100 +++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Fri Nov 16 18:45:57 2012 +0100 @@ -2891,6 +2891,10 @@ by (fast intro: less_trans, fast intro: le_less_trans, fast intro: order_trans) +lemma atLeastAtMost_singleton_euclidean[simp]: + fixes a :: "'a::ordered_euclidean_space" shows "{a .. a} = {a}" + by (force simp: eucl_le[where 'a='a] euclidean_eq[where 'a='a]) + lemma basis_real_range: "basis ` {..<1} = {1::real}" by auto instance real::ordered_euclidean_space diff -r 3d89c38408cd -r de19856feb54 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri Nov 16 18:49:46 2012 +0100 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri Nov 16 18:45:57 2012 +0100 @@ -2044,6 +2044,10 @@ unfolding bounded_any_center [where a=0] by (simp add: dist_norm) +lemma bounded_realI: assumes "\x\s. abs (x::real) \ B" shows "bounded s" + unfolding bounded_def dist_real_def apply(rule_tac x=0 in exI) + using assms by auto + lemma bounded_empty[simp]: "bounded {}" by (simp add: bounded_def) lemma bounded_subset: "bounded T \ S \ T ==> bounded S" by (metis bounded_def subset_eq) diff -r 3d89c38408cd -r de19856feb54 src/HOL/Probability/Binary_Product_Measure.thy --- a/src/HOL/Probability/Binary_Product_Measure.thy Fri Nov 16 18:49:46 2012 +0100 +++ b/src/HOL/Probability/Binary_Product_Measure.thy Fri Nov 16 18:45:57 2012 +0100 @@ -8,24 +8,12 @@ imports Lebesgue_Integration begin -lemma times_eq_iff: "A \ B = C \ D \ A = C \ B = D \ ((A = {} \ B = {}) \ (C = {} \ D = {}))" - by auto - -lemma times_Int_times: "A \ B \ C \ D = (A \ C) \ (B \ D)" - by auto - -lemma Pair_vimage_times[simp]: "\A B x. Pair x -` (A \ B) = (if x \ A then B else {})" +lemma Pair_vimage_times[simp]: "Pair x -` (A \ B) = (if x \ A then B else {})" by auto -lemma rev_Pair_vimage_times[simp]: "\A B y. (\x. (x, y)) -` (A \ B) = (if y \ B then A else {})" +lemma rev_Pair_vimage_times[simp]: "(\x. (x, y)) -` (A \ B) = (if y \ B then A else {})" by auto -lemma case_prod_distrib: "f (case x of (x, y) \ g x y) = (case x of (x, y) \ f (g x y))" - by (cases x) simp - -lemma split_beta': "(\(x,y). f x y) = (\x. f (fst x) (snd x))" - by (auto simp: fun_eq_iff) - section "Binary products" definition pair_measure (infixr "\\<^isub>M" 80) where @@ -787,4 +775,39 @@ intro!: positive_integral_cong arg_cong[where f="emeasure N"]) qed simp +lemma pair_measure_eqI: + assumes "sigma_finite_measure M1" "sigma_finite_measure M2" + assumes sets: "sets (M1 \\<^isub>M M2) = sets M" + assumes emeasure: "\A B. A \ sets M1 \ B \ sets M2 \ emeasure M1 A * emeasure M2 B = emeasure M (A \ B)" + shows "M1 \\<^isub>M M2 = M" +proof - + interpret M1: sigma_finite_measure M1 by fact + interpret M2: sigma_finite_measure M2 by fact + interpret pair_sigma_finite M1 M2 by default + from sigma_finite_up_in_pair_measure_generator guess F :: "nat \ ('a \ 'b) set" .. note F = this + let ?E = "{a \ b |a b. a \ sets M1 \ b \ sets M2}" + let ?P = "M1 \\<^isub>M M2" + show ?thesis + proof (rule measure_eqI_generator_eq[OF Int_stable_pair_measure_generator[of M1 M2]]) + show "?E \ Pow (space ?P)" + using space_closed[of M1] space_closed[of M2] by (auto simp: space_pair_measure) + show "sets ?P = sigma_sets (space ?P) ?E" + by (simp add: sets_pair_measure space_pair_measure) + then show "sets M = sigma_sets (space ?P) ?E" + using sets[symmetric] by simp + next + show "range F \ ?E" "(\i. F i) = space ?P" "\i. emeasure ?P (F i) \ \" + using F by (auto simp: space_pair_measure) + next + fix X assume "X \ ?E" + then obtain A B where X[simp]: "X = A \ B" and A: "A \ sets M1" and B: "B \ sets M2" by auto + then have "emeasure ?P X = emeasure M1 A * emeasure M2 B" + by (simp add: M2.emeasure_pair_measure_Times) + also have "\ = emeasure M (A \ B)" + using A B emeasure by auto + finally show "emeasure ?P X = emeasure M X" + by simp + qed +qed + end \ No newline at end of file diff -r 3d89c38408cd -r de19856feb54 src/HOL/Probability/Borel_Space.thy --- a/src/HOL/Probability/Borel_Space.thy Fri Nov 16 18:49:46 2012 +0100 +++ b/src/HOL/Probability/Borel_Space.thy Fri Nov 16 18:45:57 2012 +0100 @@ -1114,21 +1114,10 @@ and borel_measurable_limsup: "(\x. limsup (\i. f i x)) \ borel_measurable M" unfolding liminf_SUPR_INFI limsup_INFI_SUPR using assms by auto -lemma sets_Collect_eventually_sequientially[measurable]: +lemma sets_Collect_eventually_sequentially[measurable]: "(\i. {x\space M. P x i} \ sets M) \ {x\space M. eventually (P x) sequentially} \ sets M" unfolding eventually_sequentially by simp -lemma convergent_ereal: - fixes X :: "nat \ ereal" - shows "convergent X \ limsup X = liminf X" - using ereal_Liminf_eq_Limsup_iff[of sequentially] - by (auto simp: convergent_def) - -lemma convergent_ereal_limsup: - fixes X :: "nat \ ereal" - shows "convergent X \ limsup X = lim X" - by (auto simp: convergent_def limI lim_imp_Limsup) - lemma sets_Collect_ereal_convergent[measurable]: fixes f :: "nat \ 'a => ereal" assumes f[measurable]: "\i. f i \ borel_measurable M" diff -r 3d89c38408cd -r de19856feb54 src/HOL/Probability/Finite_Product_Measure.thy --- a/src/HOL/Probability/Finite_Product_Measure.thy Fri Nov 16 18:49:46 2012 +0100 +++ b/src/HOL/Probability/Finite_Product_Measure.thy Fri Nov 16 18:45:57 2012 +0100 @@ -262,6 +262,47 @@ using Pi_eq_empty_iff[of I F] Pi_eq_empty_iff[of I F'] by auto qed +lemma funset_eq_UN_fun_upd_I: + assumes *: "\f. f \ F (insert a A) \ f(a := d) \ F A" + and **: "\f. f \ F (insert a A) \ f a \ G (f(a:=d))" + and ***: "\f x. \ f \ F A ; x \ G f \ \ f(a:=x) \ F (insert a A)" + shows "F (insert a A) = (\f\F A. fun_upd f a ` (G f))" +proof safe + fix f assume f: "f \ F (insert a A)" + show "f \ (\f\F A. fun_upd f a ` G f)" + proof (rule UN_I[of "f(a := d)"]) + show "f(a := d) \ F A" using *[OF f] . + show "f \ fun_upd (f(a:=d)) a ` G (f(a:=d))" + proof (rule image_eqI[of _ _ "f a"]) + show "f a \ G (f(a := d))" using **[OF f] . + qed simp + qed +next + fix f x assume "f \ F A" "x \ G f" + from ***[OF this] show "f(a := x) \ F (insert a A)" . +qed + +lemma extensional_funcset_insert_eq[simp]: + assumes "a \ A" + shows "extensional (insert a A) \ (insert a A \ B) = (\f \ extensional A \ (A \ B). (\b. f(a := b)) ` B)" + apply (rule funset_eq_UN_fun_upd_I) + using assms + by (auto intro!: inj_onI dest: inj_onD split: split_if_asm simp: extensional_def) + +lemma finite_extensional_funcset[simp, intro]: + assumes "finite A" "finite B" + shows "finite (extensional A \ (A \ B))" + using assms by induct auto + +lemma finite_PiE[simp, intro]: + assumes fin: "finite A" "\i. i \ A \ finite (B i)" + shows "finite (Pi\<^isub>E A B)" +proof - + have *: "(Pi\<^isub>E A B) \ extensional A \ (A \ (\i\A. B i))" by auto + show ?thesis + using fin by (intro finite_subset[OF *] finite_extensional_funcset) auto +qed + section "Finite product spaces" section "Products" @@ -441,6 +482,31 @@ done qed +lemma prod_algebra_cong: + assumes "I = J" and sets: "(\i. i \ I \ sets (M i) = sets (N i))" + shows "prod_algebra I M = prod_algebra J N" +proof - + have space: "\i. i \ I \ space (M i) = space (N i)" + using sets_eq_imp_space_eq[OF sets] by auto + with sets show ?thesis unfolding `I = J` + by (intro antisym prod_algebra_mono) auto +qed + +lemma space_in_prod_algebra: + "(\\<^isub>E i\I. space (M i)) \ prod_algebra I M" +proof cases + assume "I = {}" then show ?thesis + by (auto simp add: prod_algebra_def image_iff prod_emb_def) +next + assume "I \ {}" + then obtain i where "i \ I" by auto + then have "(\\<^isub>E i\I. space (M i)) = prod_emb I M {i} (\\<^isub>E i\{i}. space (M i))" + by (auto simp: prod_emb_def Pi_iff) + also have "\ \ prod_algebra I M" + using `i \ I` by (intro prod_algebraI) auto + finally show ?thesis . +qed + lemma space_PiM: "space (\\<^isub>M i\I. M i) = (\\<^isub>E i\I. space (M i))" using prod_algebra_sets_into_space unfolding PiM_def prod_algebra_def by (intro space_extend_measure) simp @@ -1007,6 +1073,23 @@ show ?thesis unfolding lebesgue_integral_def *[THEN product_positive_integral_singleton] .. qed +lemma (in product_sigma_finite) distr_component: + "distr (M i) (Pi\<^isub>M {i} M) (\x. \i\{i}. x) = Pi\<^isub>M {i} M" (is "?D = ?P") +proof (intro measure_eqI[symmetric]) + interpret I: finite_product_sigma_finite M "{i}" by default simp + + have eq: "\x. x \ extensional {i} \ (\j\{i}. x i) = x" + by (auto simp: extensional_def restrict_def) + + fix A assume A: "A \ sets ?P" + then have "emeasure ?P A = (\\<^isup>+x. indicator A x \?P)" + by simp + also have "\ = (\\<^isup>+x. indicator ((\x. \i\{i}. x) -` A \ space (M i)) (x i) \PiM {i} M)" + by (intro positive_integral_cong) (auto simp: space_PiM indicator_def simp: eq) + also have "\ = emeasure ?D A" + using A by (simp add: product_positive_integral_singleton emeasure_distr) + finally show "emeasure (Pi\<^isub>M {i} M) A = emeasure ?D A" . +qed simp lemma (in product_sigma_finite) product_integral_fold: assumes IJ[simp]: "I \ J = {}" and fin: "finite I" "finite J" @@ -1250,4 +1333,31 @@ by (auto intro!: sigma_sets_subset sets_PiM_I_finite simp: E_generates P_def) qed +lemma pair_measure_eq_distr_PiM: + fixes M1 :: "'a measure" and M2 :: "'a measure" + assumes "sigma_finite_measure M1" "sigma_finite_measure M2" + shows "(M1 \\<^isub>M M2) = distr (Pi\<^isub>M UNIV (bool_case M1 M2)) (M1 \\<^isub>M M2) (\x. (x True, x False))" + (is "?P = ?D") +proof (rule pair_measure_eqI[OF assms]) + interpret B: product_sigma_finite "bool_case M1 M2" + unfolding product_sigma_finite_def using assms by (auto split: bool.split) + let ?B = "Pi\<^isub>M UNIV (bool_case M1 M2)" + + have [simp]: "fst \ (\x. (x True, x False)) = (\x. x True)" "snd \ (\x. (x True, x False)) = (\x. x False)" + by auto + fix A B assume A: "A \ sets M1" and B: "B \ sets M2" + have "emeasure M1 A * emeasure M2 B = (\ i\UNIV. emeasure (bool_case M1 M2 i) (bool_case A B i))" + by (simp add: UNIV_bool ac_simps) + also have "\ = emeasure ?B (Pi\<^isub>E UNIV (bool_case A B))" + using A B by (subst B.emeasure_PiM) (auto split: bool.split) + also have "Pi\<^isub>E UNIV (bool_case A B) = (\x. (x True, x False)) -` (A \ B) \ space ?B" + using A[THEN sets_into_space] B[THEN sets_into_space] + by (auto simp: Pi_iff all_bool_eq space_PiM split: bool.split) + finally show "emeasure M1 A * emeasure M2 B = emeasure ?D (A \ B)" + using A B + measurable_component_singleton[of True UNIV "bool_case M1 M2"] + measurable_component_singleton[of False UNIV "bool_case M1 M2"] + by (subst emeasure_distr) (auto simp: measurable_pair_iff) +qed simp + end diff -r 3d89c38408cd -r de19856feb54 src/HOL/Probability/Independent_Family.thy --- a/src/HOL/Probability/Independent_Family.thy Fri Nov 16 18:49:46 2012 +0100 +++ b/src/HOL/Probability/Independent_Family.thy Fri Nov 16 18:45:57 2012 +0100 @@ -18,9 +18,6 @@ definition (in prob_space) indep_events_def_alt: "indep_events A I \ indep_sets (\i. {A i}) I" -lemma image_subset_iff_funcset: "F ` A \ B \ F \ A \ B" - by auto - lemma (in prob_space) indep_events_def: "indep_events A I \ (A`I \ events) \ (\J\I. J \ {} \ finite J \ prob (\j\J. A j) = (\j\J. prob (A j)))" @@ -827,31 +824,6 @@ using I by auto qed fact+ -lemma prod_algebra_cong: - assumes "I = J" and sets: "(\i. i \ I \ sets (M i) = sets (N i))" - shows "prod_algebra I M = prod_algebra J N" -proof - - have space: "\i. i \ I \ space (M i) = space (N i)" - using sets_eq_imp_space_eq[OF sets] by auto - with sets show ?thesis unfolding `I = J` - by (intro antisym prod_algebra_mono) auto -qed - -lemma space_in_prod_algebra: - "(\\<^isub>E i\I. space (M i)) \ prod_algebra I M" -proof cases - assume "I = {}" then show ?thesis - by (auto simp add: prod_algebra_def image_iff prod_emb_def) -next - assume "I \ {}" - then obtain i where "i \ I" by auto - then have "(\\<^isub>E i\I. space (M i)) = prod_emb I M {i} (\\<^isub>E i\{i}. space (M i))" - by (auto simp: prod_emb_def Pi_iff) - also have "\ \ prod_algebra I M" - using `i \ I` by (intro prod_algebraI) auto - finally show ?thesis . -qed - lemma (in prob_space) indep_vars_iff_distr_eq_PiM: fixes I :: "'i set" and X :: "'i \ 'a \ 'b" assumes "I \ {}" @@ -972,114 +944,6 @@ unfolding UNIV_bool by auto qed -lemma measurable_bool_case[simp, intro]: - "(\(x, y). bool_case x y) \ measurable (M \\<^isub>M N) (Pi\<^isub>M UNIV (bool_case M N))" - (is "?f \ measurable ?B ?P") -proof (rule measurable_PiM_single) - show "?f \ space ?B \ (\\<^isub>E i\UNIV. space (bool_case M N i))" - by (auto simp: space_pair_measure extensional_def split: bool.split) - fix i A assume "A \ sets (case i of True \ M | False \ N)" - moreover then have "{\ \ space (M \\<^isub>M N). prod_case bool_case \ i \ A} - = (case i of True \ A \ space N | False \ space M \ A)" - by (auto simp: space_pair_measure split: bool.split dest!: sets_into_space) - ultimately show "{\ \ space (M \\<^isub>M N). prod_case bool_case \ i \ A} \ sets ?B" - by (auto split: bool.split) -qed - -lemma borel_measurable_indicator': - "A \ sets N \ f \ measurable M N \ (\x. indicator A (f x)) \ borel_measurable M" - using measurable_comp[OF _ borel_measurable_indicator, of f M N A] by (auto simp add: comp_def) - -lemma (in product_sigma_finite) distr_component: - "distr (M i) (Pi\<^isub>M {i} M) (\x. \i\{i}. x) = Pi\<^isub>M {i} M" (is "?D = ?P") -proof (intro measure_eqI[symmetric]) - interpret I: finite_product_sigma_finite M "{i}" by default simp - - have eq: "\