--- 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 \<in> 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]: "\<bar>- x\<bar> = \<bar>x::ereal\<bar>"
by (cases x) auto
+lemma ereal_infinity_cases: "(a::ereal) \<noteq> \<infinity> \<Longrightarrow> a \<noteq> -\<infinity> \<Longrightarrow> \<bar>a\<bar> \<noteq> \<infinity>"
+ 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 \<le> 1 \<Longrightarrow> real a \<le> 1"
by (cases a) (auto simp: one_ereal_def)
@@ -659,6 +664,16 @@
shows "0 < a * b \<longleftrightarrow> (0 < a \<and> 0 < b) \<or> (a < 0 \<and> 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 \<noteq> 0 \<Longrightarrow> a = b) \<Longrightarrow> c * a = c * b"
+ by (cases "c = 0") simp_all
+
+lemma ereal_right_mult_cong:
+ fixes a b c :: ereal
+ shows "(c \<noteq> 0 \<Longrightarrow> a = b) \<Longrightarrow> a * c = b * c"
+ by (cases "c = 0") simp_all
+
lemma ereal_distrib:
fixes a b c :: ereal
assumes "a \<noteq> \<infinity> \<or> b \<noteq> -\<infinity>" "a \<noteq> -\<infinity> \<or> b \<noteq> \<infinity>" "\<bar>c\<bar> \<noteq> \<infinity>"
@@ -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 = \<infinity> \<longleftrightarrow> y = -\<infinity> \<or> x = \<infinity>"
+ by (cases x y rule: ereal2_cases) simp_all
+
subsubsection {* Division *}
instantiation ereal :: inverse
--- 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 \<in> A\<rightarrow>B ==> f ` A \<subseteq> B"
-by auto
+ by auto
+
+lemma image_subset_iff_funcset: "F ` A \<subseteq> B \<longleftrightarrow> F \<in> A \<rightarrow> B"
+ by auto
lemma Pi_eq_empty[simp]: "((PI x: A. B x) = {}) = (\<exists>x\<in>A. B(x) = {})"
apply (simp add: Pi_def, auto)
--- 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 \<Rightarrow> real"
+ assumes "convex_on I f"
+ assumes "x \<in> interior I" "y \<in> I"
+ shows "f y \<ge> f x + Inf ((\<lambda>t. (f x - f t) / (x - t)) ` ({x<..} \<inter> I)) * (y - x)"
+ (is "_ \<ge> _ + 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 \<in> interior I`] guess e . note e = this
+ moreover def t \<equiv> "min (x + e / 2) ((x + y) / 2)"
+ ultimately have "x < t" "t < y" "t \<in> ball x e"
+ by (auto simp: dist_real_def field_simps split: split_min)
+ with `x \<in> interior I` e interior_subset[of I] have "t \<in> I" "x \<in> I" by auto
+
+ have "open (interior I)" by auto
+ from openE[OF this `x \<in> interior I`] guess e .
+ moreover def K \<equiv> "x - e / 2"
+ with `0 < e` have "K \<in> ball x e" "K < x" by (auto simp: dist_real_def)
+ ultimately have "K \<in> I" "K < x" "x \<in> I"
+ using interior_subset[of I] `x \<in> interior I` by auto
+
+ have "Inf (?F x) \<le> (f x - f y) / (x - y)"
+ proof (rule Inf_lower2)
+ show "(f x - f t) / (x - t) \<in> ?F x"
+ using `t \<in> I` `x < t` by auto
+ show "(f x - f t) / (x - t) \<le> (f x - f y) / (x - y)"
+ using `convex_on I f` `x \<in> I` `y \<in> I` `x < t` `t < y` by (rule convex_on_diff)
+ next
+ fix y assume "y \<in> ?F x"
+ with order_trans[OF convex_on_diff[OF `convex_on I f` `K \<in> I` _ `K < x` _]]
+ show "(f K - f x) / (K - x) \<le> 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 \<in> interior I`] guess e . note e = this
+ moreover def t \<equiv> "x + e / 2"
+ ultimately have "x < t" "t \<in> ball x e"
+ by (auto simp: dist_real_def field_simps)
+ with `x \<in> interior I` e interior_subset[of I] have "t \<in> I" "x \<in> I" by auto
+
+ have "(f x - f y) / (x - y) \<le> 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 \<in> ?F x"
+ with order_trans[OF convex_on_diff[OF `convex_on I f` `y \<in> I` _ `y < x`]]
+ have "(f y - f x) / (y - x) \<le> z" by auto
+ finally show "(f x - f y) / (x - y) \<le> z" .
+ next
+ have "open (interior I)" by auto
+ from openE[OF this `x \<in> interior I`] guess e . note e = this
+ then have "x + e / 2 \<in> ball x e" by (auto simp: dist_real_def)
+ with e interior_subset[of I] have "x + e / 2 \<in> {x<..} \<inter> I" by auto
+ then show "?F x \<noteq> {}" by blast
+ qed
+ then show ?thesis
+ using `y < x` by (simp add: field_simps)
+qed simp
+
end
--- 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 \<Rightarrow> ereal"
+ shows "convergent X \<Longrightarrow> limsup X = lim X"
+ by (auto simp: convergent_def limI lim_imp_Limsup)
+
lemma Liminf_PInfty:
fixes f :: "'a \<Rightarrow> ereal"
assumes "\<not> trivial_limit net"
@@ -486,6 +491,12 @@
shows "(f ---> f0) net \<longleftrightarrow> Liminf net f = f0 \<and> Limsup net f = f0"
by (metis assms ereal_Liminf_eq_Limsup lim_imp_Liminf lim_imp_Limsup)
+lemma convergent_ereal:
+ fixes X :: "nat \<Rightarrow> ereal"
+ shows "convergent X \<longleftrightarrow> limsup X = liminf X"
+ using ereal_Liminf_eq_Limsup_iff[of sequentially]
+ by (auto simp: convergent_def)
+
lemma limsup_INFI_SUPR:
fixes f :: "nat \<Rightarrow> 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 \<Rightarrow> ereal"
+ assumes nneg: "\<And>i. 0 \<le> f i"
+ shows "(\<Sum>i. f i) = 0 \<longleftrightarrow> (\<forall>i. f i = 0)"
+proof
+ assume "(\<Sum>i. f i) = 0"
+ { fix i assume "f i \<noteq> 0"
+ with nneg have "0 < f i" by (auto simp: less_le)
+ also have "f i = (\<Sum>j. if j = i then f i else 0)"
+ by (subst suminf_finite[where N="{i}"]) auto
+ also have "\<dots> \<le> (\<Sum>i. f i)"
+ using nneg by (auto intro!: suminf_le_pos)
+ finally have False using `(\<Sum>i. f i) = 0` by auto }
+ then show "\<forall>i. f i = 0" by auto
+qed simp
+
end
--- 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 *: "\<forall>i<DIM('a). (0::'a)$$i \<le> (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 \<noteq> 0 \<Longrightarrow> (f has_integral x) A"
+ shows "((\<lambda>x. c * f x) has_integral c * x) A"
+proof cases
+ assume "c \<noteq> 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 \<Longrightarrow> ((\<lambda>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 \<Longrightarrow> (\<lambda>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 \<noteq> 0"
+ shows "(\<lambda>x. c * f x) integrable_on s \<longleftrightarrow> f integrable_on s"
+ using integrable_cmul[of "\<lambda>x. c * f x" s "1 / c"] integrable_cmul[of f s c] `c \<noteq> 0`
+ by auto
+
lemma integrable_neg:
shows "f integrable_on s \<Longrightarrow> (\<lambda>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} (\<lambda>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) \<le> e"
--- 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
--- 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 "\<forall>x\<in>s. abs (x::real) \<le> 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 \<Longrightarrow> S \<subseteq> T ==> bounded S"
by (metis bounded_def subset_eq)
--- 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 \<times> B = C \<times> D \<longleftrightarrow> A = C \<and> B = D \<or> ((A = {} \<or> B = {}) \<and> (C = {} \<or> D = {}))"
- by auto
-
-lemma times_Int_times: "A \<times> B \<inter> C \<times> D = (A \<inter> C) \<times> (B \<inter> D)"
- by auto
-
-lemma Pair_vimage_times[simp]: "\<And>A B x. Pair x -` (A \<times> B) = (if x \<in> A then B else {})"
+lemma Pair_vimage_times[simp]: "Pair x -` (A \<times> B) = (if x \<in> A then B else {})"
by auto
-lemma rev_Pair_vimage_times[simp]: "\<And>A B y. (\<lambda>x. (x, y)) -` (A \<times> B) = (if y \<in> B then A else {})"
+lemma rev_Pair_vimage_times[simp]: "(\<lambda>x. (x, y)) -` (A \<times> B) = (if y \<in> B then A else {})"
by auto
-lemma case_prod_distrib: "f (case x of (x, y) \<Rightarrow> g x y) = (case x of (x, y) \<Rightarrow> f (g x y))"
- by (cases x) simp
-
-lemma split_beta': "(\<lambda>(x,y). f x y) = (\<lambda>x. f (fst x) (snd x))"
- by (auto simp: fun_eq_iff)
-
section "Binary products"
definition pair_measure (infixr "\<Otimes>\<^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 \<Otimes>\<^isub>M M2) = sets M"
+ assumes emeasure: "\<And>A B. A \<in> sets M1 \<Longrightarrow> B \<in> sets M2 \<Longrightarrow> emeasure M1 A * emeasure M2 B = emeasure M (A \<times> B)"
+ shows "M1 \<Otimes>\<^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 \<Rightarrow> ('a \<times> 'b) set" .. note F = this
+ let ?E = "{a \<times> b |a b. a \<in> sets M1 \<and> b \<in> sets M2}"
+ let ?P = "M1 \<Otimes>\<^isub>M M2"
+ show ?thesis
+ proof (rule measure_eqI_generator_eq[OF Int_stable_pair_measure_generator[of M1 M2]])
+ show "?E \<subseteq> 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 \<subseteq> ?E" "(\<Union>i. F i) = space ?P" "\<And>i. emeasure ?P (F i) \<noteq> \<infinity>"
+ using F by (auto simp: space_pair_measure)
+ next
+ fix X assume "X \<in> ?E"
+ then obtain A B where X[simp]: "X = A \<times> B" and A: "A \<in> sets M1" and B: "B \<in> 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 "\<dots> = emeasure M (A \<times> 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
--- 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: "(\<lambda>x. limsup (\<lambda>i. f i x)) \<in> 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]:
"(\<And>i. {x\<in>space M. P x i} \<in> sets M) \<Longrightarrow> {x\<in>space M. eventually (P x) sequentially} \<in> sets M"
unfolding eventually_sequentially by simp
-lemma convergent_ereal:
- fixes X :: "nat \<Rightarrow> ereal"
- shows "convergent X \<longleftrightarrow> limsup X = liminf X"
- using ereal_Liminf_eq_Limsup_iff[of sequentially]
- by (auto simp: convergent_def)
-
-lemma convergent_ereal_limsup:
- fixes X :: "nat \<Rightarrow> ereal"
- shows "convergent X \<Longrightarrow> limsup X = lim X"
- by (auto simp: convergent_def limI lim_imp_Limsup)
-
lemma sets_Collect_ereal_convergent[measurable]:
fixes f :: "nat \<Rightarrow> 'a => ereal"
assumes f[measurable]: "\<And>i. f i \<in> borel_measurable M"
--- 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 *: "\<And>f. f \<in> F (insert a A) \<Longrightarrow> f(a := d) \<in> F A"
+ and **: "\<And>f. f \<in> F (insert a A) \<Longrightarrow> f a \<in> G (f(a:=d))"
+ and ***: "\<And>f x. \<lbrakk> f \<in> F A ; x \<in> G f \<rbrakk> \<Longrightarrow> f(a:=x) \<in> F (insert a A)"
+ shows "F (insert a A) = (\<Union>f\<in>F A. fun_upd f a ` (G f))"
+proof safe
+ fix f assume f: "f \<in> F (insert a A)"
+ show "f \<in> (\<Union>f\<in>F A. fun_upd f a ` G f)"
+ proof (rule UN_I[of "f(a := d)"])
+ show "f(a := d) \<in> F A" using *[OF f] .
+ show "f \<in> fun_upd (f(a:=d)) a ` G (f(a:=d))"
+ proof (rule image_eqI[of _ _ "f a"])
+ show "f a \<in> G (f(a := d))" using **[OF f] .
+ qed simp
+ qed
+next
+ fix f x assume "f \<in> F A" "x \<in> G f"
+ from ***[OF this] show "f(a := x) \<in> F (insert a A)" .
+qed
+
+lemma extensional_funcset_insert_eq[simp]:
+ assumes "a \<notin> A"
+ shows "extensional (insert a A) \<inter> (insert a A \<rightarrow> B) = (\<Union>f \<in> extensional A \<inter> (A \<rightarrow> B). (\<lambda>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 \<inter> (A \<rightarrow> B))"
+ using assms by induct auto
+
+lemma finite_PiE[simp, intro]:
+ assumes fin: "finite A" "\<And>i. i \<in> A \<Longrightarrow> finite (B i)"
+ shows "finite (Pi\<^isub>E A B)"
+proof -
+ have *: "(Pi\<^isub>E A B) \<subseteq> extensional A \<inter> (A \<rightarrow> (\<Union>i\<in>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: "(\<And>i. i \<in> I \<Longrightarrow> sets (M i) = sets (N i))"
+ shows "prod_algebra I M = prod_algebra J N"
+proof -
+ have space: "\<And>i. i \<in> I \<Longrightarrow> 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:
+ "(\<Pi>\<^isub>E i\<in>I. space (M i)) \<in> 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 \<noteq> {}"
+ then obtain i where "i \<in> I" by auto
+ then have "(\<Pi>\<^isub>E i\<in>I. space (M i)) = prod_emb I M {i} (\<Pi>\<^isub>E i\<in>{i}. space (M i))"
+ by (auto simp: prod_emb_def Pi_iff)
+ also have "\<dots> \<in> prod_algebra I M"
+ using `i \<in> I` by (intro prod_algebraI) auto
+ finally show ?thesis .
+qed
+
lemma space_PiM: "space (\<Pi>\<^isub>M i\<in>I. M i) = (\<Pi>\<^isub>E i\<in>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) (\<lambda>x. \<lambda>i\<in>{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: "\<And>x. x \<in> extensional {i} \<Longrightarrow> (\<lambda>j\<in>{i}. x i) = x"
+ by (auto simp: extensional_def restrict_def)
+
+ fix A assume A: "A \<in> sets ?P"
+ then have "emeasure ?P A = (\<integral>\<^isup>+x. indicator A x \<partial>?P)"
+ by simp
+ also have "\<dots> = (\<integral>\<^isup>+x. indicator ((\<lambda>x. \<lambda>i\<in>{i}. x) -` A \<inter> space (M i)) (x i) \<partial>PiM {i} M)"
+ by (intro positive_integral_cong) (auto simp: space_PiM indicator_def simp: eq)
+ also have "\<dots> = 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 \<inter> 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 \<Otimes>\<^isub>M M2) = distr (Pi\<^isub>M UNIV (bool_case M1 M2)) (M1 \<Otimes>\<^isub>M M2) (\<lambda>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 \<circ> (\<lambda>x. (x True, x False)) = (\<lambda>x. x True)" "snd \<circ> (\<lambda>x. (x True, x False)) = (\<lambda>x. x False)"
+ by auto
+ fix A B assume A: "A \<in> sets M1" and B: "B \<in> sets M2"
+ have "emeasure M1 A * emeasure M2 B = (\<Prod> i\<in>UNIV. emeasure (bool_case M1 M2 i) (bool_case A B i))"
+ by (simp add: UNIV_bool ac_simps)
+ also have "\<dots> = 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) = (\<lambda>x. (x True, x False)) -` (A \<times> B) \<inter> 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 \<times> 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
--- 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 \<longleftrightarrow> indep_sets (\<lambda>i. {A i}) I"
-lemma image_subset_iff_funcset: "F ` A \<subseteq> B \<longleftrightarrow> F \<in> A \<rightarrow> B"
- by auto
-
lemma (in prob_space) indep_events_def:
"indep_events A I \<longleftrightarrow> (A`I \<subseteq> events) \<and>
(\<forall>J\<subseteq>I. J \<noteq> {} \<longrightarrow> finite J \<longrightarrow> prob (\<Inter>j\<in>J. A j) = (\<Prod>j\<in>J. prob (A j)))"
@@ -827,31 +824,6 @@
using I by auto
qed fact+
-lemma prod_algebra_cong:
- assumes "I = J" and sets: "(\<And>i. i \<in> I \<Longrightarrow> sets (M i) = sets (N i))"
- shows "prod_algebra I M = prod_algebra J N"
-proof -
- have space: "\<And>i. i \<in> I \<Longrightarrow> 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:
- "(\<Pi>\<^isub>E i\<in>I. space (M i)) \<in> 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 \<noteq> {}"
- then obtain i where "i \<in> I" by auto
- then have "(\<Pi>\<^isub>E i\<in>I. space (M i)) = prod_emb I M {i} (\<Pi>\<^isub>E i\<in>{i}. space (M i))"
- by (auto simp: prod_emb_def Pi_iff)
- also have "\<dots> \<in> prod_algebra I M"
- using `i \<in> 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 \<Rightarrow> 'a \<Rightarrow> 'b"
assumes "I \<noteq> {}"
@@ -972,114 +944,6 @@
unfolding UNIV_bool by auto
qed
-lemma measurable_bool_case[simp, intro]:
- "(\<lambda>(x, y). bool_case x y) \<in> measurable (M \<Otimes>\<^isub>M N) (Pi\<^isub>M UNIV (bool_case M N))"
- (is "?f \<in> measurable ?B ?P")
-proof (rule measurable_PiM_single)
- show "?f \<in> space ?B \<rightarrow> (\<Pi>\<^isub>E i\<in>UNIV. space (bool_case M N i))"
- by (auto simp: space_pair_measure extensional_def split: bool.split)
- fix i A assume "A \<in> sets (case i of True \<Rightarrow> M | False \<Rightarrow> N)"
- moreover then have "{\<omega> \<in> space (M \<Otimes>\<^isub>M N). prod_case bool_case \<omega> i \<in> A}
- = (case i of True \<Rightarrow> A \<times> space N | False \<Rightarrow> space M \<times> A)"
- by (auto simp: space_pair_measure split: bool.split dest!: sets_into_space)
- ultimately show "{\<omega> \<in> space (M \<Otimes>\<^isub>M N). prod_case bool_case \<omega> i \<in> A} \<in> sets ?B"
- by (auto split: bool.split)
-qed
-
-lemma borel_measurable_indicator':
- "A \<in> sets N \<Longrightarrow> f \<in> measurable M N \<Longrightarrow> (\<lambda>x. indicator A (f x)) \<in> 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) (\<lambda>x. \<lambda>i\<in>{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: "\<And>x. x \<in> extensional {i} \<Longrightarrow> (\<lambda>j\<in>{i}. x i) = x"
- by (auto simp: extensional_def restrict_def)
-
- fix A assume A: "A \<in> sets ?P"
- then have "emeasure ?P A = (\<integral>\<^isup>+x. indicator A x \<partial>?P)"
- by simp
- also have "\<dots> = (\<integral>\<^isup>+x. indicator ((\<lambda>x. \<lambda>i\<in>{i}. x) -` A \<inter> space (M i)) (x i) \<partial>PiM {i} M)"
- by (intro positive_integral_cong) (auto simp: space_PiM indicator_def simp: eq)
- also have "\<dots> = 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 pair_measure_eqI:
- assumes "sigma_finite_measure M1" "sigma_finite_measure M2"
- assumes sets: "sets (M1 \<Otimes>\<^isub>M M2) = sets M"
- assumes emeasure: "\<And>A B. A \<in> sets M1 \<Longrightarrow> B \<in> sets M2 \<Longrightarrow> emeasure M1 A * emeasure M2 B = emeasure M (A \<times> B)"
- shows "M1 \<Otimes>\<^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 \<Rightarrow> ('a \<times> 'b) set" .. note F = this
- let ?E = "{a \<times> b |a b. a \<in> sets M1 \<and> b \<in> sets M2}"
- let ?P = "M1 \<Otimes>\<^isub>M M2"
- show ?thesis
- proof (rule measure_eqI_generator_eq[OF Int_stable_pair_measure_generator[of M1 M2]])
- show "?E \<subseteq> 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 \<subseteq> ?E" "(\<Union>i. F i) = space ?P" "\<And>i. emeasure ?P (F i) \<noteq> \<infinity>"
- using F by (auto simp: space_pair_measure)
- next
- fix X assume "X \<in> ?E"
- then obtain A B where X[simp]: "X = A \<times> B" and A: "A \<in> sets M1" and B: "B \<in> 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 "\<dots> = emeasure M (A \<times> B)"
- using A B emeasure by auto
- finally show "emeasure ?P X = emeasure M X"
- by simp
- qed
-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 \<Otimes>\<^isub>M M2) = distr (Pi\<^isub>M UNIV (bool_case M1 M2)) (M1 \<Otimes>\<^isub>M M2) (\<lambda>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 \<circ> (\<lambda>x. (x True, x False)) = (\<lambda>x. x True)" "snd \<circ> (\<lambda>x. (x True, x False)) = (\<lambda>x. x False)"
- by auto
- fix A B assume A: "A \<in> sets M1" and B: "B \<in> sets M2"
- have "emeasure M1 A * emeasure M2 B = (\<Prod> i\<in>UNIV. emeasure (bool_case M1 M2 i) (bool_case A B i))"
- by (simp add: UNIV_bool ac_simps)
- also have "\<dots> = 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) = (\<lambda>x. (x True, x False)) -` (A \<times> B) \<inter> 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 \<times> 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
-
-lemma measurable_Pair:
- assumes rvs: "X \<in> measurable M S" "Y \<in> measurable M T"
- shows "(\<lambda>x. (X x, Y x)) \<in> measurable M (S \<Otimes>\<^isub>M T)"
-proof -
- have [simp]: "fst \<circ> (\<lambda>x. (X x, Y x)) = (\<lambda>x. X x)" "snd \<circ> (\<lambda>x. (X x, Y x)) = (\<lambda>x. Y x)"
- by auto
- show " (\<lambda>x. (X x, Y x)) \<in> measurable M (S \<Otimes>\<^isub>M T)"
- by (auto simp: measurable_pair_iff rvs)
-qed
-
lemma (in prob_space) indep_var_distribution_eq:
"indep_var S X T Y \<longleftrightarrow> random_variable S X \<and> random_variable T Y \<and>
distr M S X \<Otimes>\<^isub>M distr M T Y = distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))" (is "_ \<longleftrightarrow> _ \<and> _ \<and> ?S \<Otimes>\<^isub>M ?T = ?J")
--- a/src/HOL/Probability/Lebesgue_Integration.thy Fri Nov 16 18:49:46 2012 +0100
+++ b/src/HOL/Probability/Lebesgue_Integration.thy Fri Nov 16 18:45:57 2012 +0100
@@ -9,16 +9,6 @@
imports Measure_Space Borel_Space
begin
-lemma ereal_minus_eq_PInfty_iff:
- fixes x y :: ereal shows "x - y = \<infinity> \<longleftrightarrow> y = -\<infinity> \<or> x = \<infinity>"
- by (cases x y rule: ereal2_cases) simp_all
-
-lemma real_ereal_1[simp]: "real (1::ereal) = 1"
- unfolding one_ereal_def by simp
-
-lemma ereal_indicator_pos[simp,intro]: "0 \<le> (indicator A x ::ereal)"
- unfolding indicator_def by auto
-
lemma tendsto_real_max:
fixes x y :: real
assumes "(X ---> x) net"
@@ -42,11 +32,6 @@
then show ?thesis using assms by (auto intro: measurable_sets)
qed
-lemma incseq_Suc_iff: "incseq f \<longleftrightarrow> (\<forall>n. f n \<le> f (Suc n))"
-proof
- assume "\<forall>n. f n \<le> f (Suc n)" then show "incseq f" by (auto intro!: incseq_SucI)
-qed (auto simp: incseq_def)
-
section "Simple function"
text {*
--- a/src/HOL/Probability/Lebesgue_Measure.thy Fri Nov 16 18:49:46 2012 +0100
+++ b/src/HOL/Probability/Lebesgue_Measure.thy Fri Nov 16 18:45:57 2012 +0100
@@ -9,14 +9,32 @@
imports Finite_Product_Measure
begin
-lemma borel_measurable_indicator':
- "A \<in> sets borel \<Longrightarrow> f \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. indicator A (f x)) \<in> borel_measurable M"
- using measurable_comp[OF _ borel_measurable_indicator, of f M borel A] by (auto simp add: comp_def)
+lemma bchoice_iff: "(\<forall>x\<in>A. \<exists>y. P x y) \<longleftrightarrow> (\<exists>f. \<forall>x\<in>A. P x (f x))"
+ by metis
+
+lemma absolutely_integrable_on_indicator[simp]:
+ fixes A :: "'a::ordered_euclidean_space set"
+ shows "((indicator A :: _ \<Rightarrow> real) absolutely_integrable_on X) \<longleftrightarrow>
+ (indicator A :: _ \<Rightarrow> real) integrable_on X"
+ unfolding absolutely_integrable_on_def by simp
-lemma borel_measurable_sets:
- assumes "f \<in> measurable borel M" "A \<in> sets M"
- shows "f -` A \<in> sets borel"
- using measurable_sets[OF assms] by simp
+lemma has_integral_indicator_UNIV:
+ fixes s A :: "'a::ordered_euclidean_space set" and x :: real
+ shows "((indicator (s \<inter> A) :: 'a\<Rightarrow>real) has_integral x) UNIV = ((indicator s :: _\<Rightarrow>real) has_integral x) A"
+proof -
+ have "(\<lambda>x. if x \<in> A then indicator s x else 0) = (indicator (s \<inter> A) :: _\<Rightarrow>real)"
+ by (auto simp: fun_eq_iff indicator_def)
+ then show ?thesis
+ unfolding has_integral_restrict_univ[where s=A, symmetric] by simp
+qed
+
+lemma
+ fixes s a :: "'a::ordered_euclidean_space set"
+ shows integral_indicator_UNIV:
+ "integral UNIV (indicator (s \<inter> A) :: 'a\<Rightarrow>real) = integral A (indicator s :: _\<Rightarrow>real)"
+ and integrable_indicator_UNIV:
+ "(indicator (s \<inter> A) :: 'a\<Rightarrow>real) integrable_on UNIV \<longleftrightarrow> (indicator s :: 'a\<Rightarrow>real) integrable_on A"
+ unfolding integral_def integrable_on_def has_integral_indicator_UNIV by auto
subsection {* Standard Cubes *}
@@ -62,6 +80,23 @@
lemma cube_subset_Suc[intro]: "cube n \<subseteq> cube (Suc n)"
unfolding cube_def subset_eq apply safe unfolding mem_interval apply auto done
+lemma has_integral_interval_cube:
+ fixes a b :: "'a::ordered_euclidean_space"
+ shows "(indicator {a .. b} has_integral
+ content ({\<chi>\<chi> i. max (- real n) (a $$ i) .. \<chi>\<chi> i. min (real n) (b $$ i)} :: 'a set)) (cube n)"
+ (is "(?I has_integral content ?R) (cube n)")
+proof -
+ let "{?N .. ?P}" = ?R
+ have [simp]: "(\<lambda>x. if x \<in> cube n then ?I x else 0) = indicator ?R"
+ by (auto simp: indicator_def cube_def fun_eq_iff eucl_le[where 'a='a])
+ have "(?I has_integral content ?R) (cube n) \<longleftrightarrow> (indicator ?R has_integral content ?R) UNIV"
+ unfolding has_integral_restrict_univ[where s="cube n", symmetric] by simp
+ also have "\<dots> \<longleftrightarrow> ((\<lambda>x. 1) has_integral content ?R) ?R"
+ unfolding indicator_def [abs_def] has_integral_restrict_univ ..
+ finally show ?thesis
+ using has_integral_const[of "1::real" "?N" "?P"] by simp
+qed
+
subsection {* Lebesgue measure *}
definition lebesgue :: "'a::ordered_euclidean_space measure" where
@@ -74,26 +109,6 @@
lemma lebesgueI: "(\<And>n. (indicator A :: _ \<Rightarrow> real) integrable_on cube n) \<Longrightarrow> A \<in> sets lebesgue"
unfolding lebesgue_def by simp
-lemma absolutely_integrable_on_indicator[simp]:
- fixes A :: "'a::ordered_euclidean_space set"
- shows "((indicator A :: _ \<Rightarrow> real) absolutely_integrable_on X) \<longleftrightarrow>
- (indicator A :: _ \<Rightarrow> real) integrable_on X"
- unfolding absolutely_integrable_on_def by simp
-
-lemma LIMSEQ_indicator_UN:
- "(\<lambda>k. indicator (\<Union> i<k. A i) x) ----> (indicator (\<Union>i. A i) x :: real)"
-proof cases
- assume "\<exists>i. x \<in> A i" then guess i .. note i = this
- then have *: "\<And>n. (indicator (\<Union> i<n + Suc i. A i) x :: real) = 1"
- "(indicator (\<Union> i. A i) x :: real) = 1" by (auto simp: indicator_def)
- show ?thesis
- apply (rule LIMSEQ_offset[of _ "Suc i"]) unfolding * by auto
-qed (auto simp: indicator_def)
-
-lemma indicator_add:
- "A \<inter> B = {} \<Longrightarrow> (indicator A x::_::monoid_add) + indicator B x = indicator (A \<union> B) x"
- unfolding indicator_def by auto
-
lemma sigma_algebra_lebesgue:
defines "leb \<equiv> {A. \<forall>n. (indicator A :: 'a::ordered_euclidean_space \<Rightarrow> real) integrable_on cube n}"
shows "sigma_algebra UNIV leb"
@@ -198,23 +213,6 @@
qed
qed (auto, fact)
-lemma has_integral_interval_cube:
- fixes a b :: "'a::ordered_euclidean_space"
- shows "(indicator {a .. b} has_integral
- content ({\<chi>\<chi> i. max (- real n) (a $$ i) .. \<chi>\<chi> i. min (real n) (b $$ i)} :: 'a set)) (cube n)"
- (is "(?I has_integral content ?R) (cube n)")
-proof -
- let "{?N .. ?P}" = ?R
- have [simp]: "(\<lambda>x. if x \<in> cube n then ?I x else 0) = indicator ?R"
- by (auto simp: indicator_def cube_def fun_eq_iff eucl_le[where 'a='a])
- have "(?I has_integral content ?R) (cube n) \<longleftrightarrow> (indicator ?R has_integral content ?R) UNIV"
- unfolding has_integral_restrict_univ[where s="cube n", symmetric] by simp
- also have "\<dots> \<longleftrightarrow> ((\<lambda>x. 1) has_integral content ?R) ?R"
- unfolding indicator_def [abs_def] has_integral_restrict_univ ..
- finally show ?thesis
- using has_integral_const[of "1::real" "?N" "?P"] by simp
-qed
-
lemma lebesgueI_borel[intro, simp]:
fixes s::"'a::ordered_euclidean_space set"
assumes "s \<in> sets borel" shows "s \<in> sets lebesgue"
@@ -261,24 +259,6 @@
using cube_subset assms by (intro monoI integral_subset_le) (auto dest!: lebesgueD)
qed
-lemma has_integral_indicator_UNIV:
- fixes s A :: "'a::ordered_euclidean_space set" and x :: real
- shows "((indicator (s \<inter> A) :: 'a\<Rightarrow>real) has_integral x) UNIV = ((indicator s :: _\<Rightarrow>real) has_integral x) A"
-proof -
- have "(\<lambda>x. if x \<in> A then indicator s x else 0) = (indicator (s \<inter> A) :: _\<Rightarrow>real)"
- by (auto simp: fun_eq_iff indicator_def)
- then show ?thesis
- unfolding has_integral_restrict_univ[where s=A, symmetric] by simp
-qed
-
-lemma
- fixes s a :: "'a::ordered_euclidean_space set"
- shows integral_indicator_UNIV:
- "integral UNIV (indicator (s \<inter> A) :: 'a\<Rightarrow>real) = integral A (indicator s :: _\<Rightarrow>real)"
- and integrable_indicator_UNIV:
- "(indicator (s \<inter> A) :: 'a\<Rightarrow>real) integrable_on UNIV \<longleftrightarrow> (indicator s :: 'a\<Rightarrow>real) integrable_on A"
- unfolding integral_def integrable_on_def has_integral_indicator_UNIV by auto
-
lemma lmeasure_finite_has_integral:
fixes s :: "'a::ordered_euclidean_space set"
assumes "s \<in> sets lebesgue" "emeasure lebesgue s = ereal m"
@@ -429,11 +409,6 @@
qed
qed
-lemma integral_const[simp]:
- fixes a b :: "'a::ordered_euclidean_space"
- shows "integral {a .. b} (\<lambda>x. c) = content {a .. b} *\<^sub>R c"
- by (rule integral_unique) (rule has_integral_const)
-
lemma lmeasure_UNIV[intro]: "emeasure lebesgue (UNIV::'a::ordered_euclidean_space set) = \<infinity>"
proof (simp add: emeasure_lebesgue, intro SUP_PInfty bexI)
fix n :: nat
@@ -467,17 +442,6 @@
by (simp add: indicator_def [abs_def])
qed
-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 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 lmeasure_singleton[simp]:
fixes a :: "'a::ordered_euclidean_space" shows "emeasure lebesgue {a} = 0"
using lmeasure_atLeastAtMost[of a a] by simp
@@ -609,16 +573,6 @@
subsection {* Lebesgue integrable implies Gauge integrable *}
-lemma has_integral_cmult_real:
- fixes c :: real
- assumes "c \<noteq> 0 \<Longrightarrow> (f has_integral x) A"
- shows "((\<lambda>x. c * f x) has_integral c * x) A"
-proof cases
- assume "c \<noteq> 0"
- from has_integral_cmul[OF assms[OF this], of c] show ?thesis
- unfolding real_scaleR_def .
-qed simp
-
lemma simple_function_has_integral:
fixes f::"'a::ordered_euclidean_space \<Rightarrow> ereal"
assumes f:"simple_function lebesgue f"
@@ -657,10 +611,6 @@
finally show "((\<lambda>x. real (\<Sum>y\<in>range f. y * ?F y x)) has_integral real (\<Sum>x\<in>range f. x * ?M x)) UNIV" .
qed fact
-lemma bounded_realI: assumes "\<forall>x\<in>s. abs (x::real) \<le> B" shows "bounded s"
- unfolding bounded_def dist_real_def apply(rule_tac x=0 in exI)
- using assms by auto
-
lemma simple_function_has_integral':
fixes f::"'a::ordered_euclidean_space \<Rightarrow> ereal"
assumes f: "simple_function lebesgue f" "\<And>x. 0 \<le> f x"
@@ -695,9 +645,6 @@
qed
qed
-lemma ereal_indicator: "ereal (indicator A x) = indicator A x"
- by (auto simp: indicator_def one_ereal_def)
-
lemma positive_integral_has_integral:
fixes f :: "'a::ordered_euclidean_space \<Rightarrow> ereal"
assumes f: "f \<in> borel_measurable lebesgue" "range f \<subseteq> {0..<\<infinity>}" "integral\<^isup>P lebesgue f \<noteq> \<infinity>"
@@ -843,12 +790,6 @@
unfolding lebesgue_integral_eq_borel[OF borel] by simp
qed
-lemma integrable_on_cmult_iff:
- fixes c :: real assumes "c \<noteq> 0"
- shows "(\<lambda>x. c * f x) integrable_on s \<longleftrightarrow> f integrable_on s"
- using integrable_cmul[of "\<lambda>x. c * f x" s "1 / c"] integrable_cmul[of f s c] `c \<noteq> 0`
- by auto
-
lemma positive_integral_lebesgue_has_integral:
fixes f :: "'a::ordered_euclidean_space \<Rightarrow> real"
assumes f_borel: "f \<in> borel_measurable lebesgue" and nonneg: "\<And>x. 0 \<le> f x"
@@ -983,9 +924,6 @@
interpretation lborel_space: finite_product_sigma_finite "\<lambda>x. lborel::real measure" "{..<n}" for n :: nat
by default auto
-lemma bchoice_iff: "(\<forall>x\<in>A. \<exists>y. P x y) \<longleftrightarrow> (\<exists>f. \<forall>x\<in>A. P x (f x))"
- by metis
-
lemma sets_product_borel:
assumes I: "finite I"
shows "sets (\<Pi>\<^isub>M i\<in>I. lborel) = sigma_sets (\<Pi>\<^isub>E i\<in>I. UNIV) { \<Pi>\<^isub>E i\<in>I. {..< x i :: real} | x. True}" (is "_ = ?G")
--- a/src/HOL/Probability/Measure_Space.thy Fri Nov 16 18:49:46 2012 +0100
+++ b/src/HOL/Probability/Measure_Space.thy Fri Nov 16 18:45:57 2012 +0100
@@ -18,6 +18,28 @@
apply (subst LIMSEQ_Suc_iff[symmetric])
unfolding atLeastLessThanSuc_atLeastAtMost atLeast0AtMost ..
+subsection "Relate extended reals and the indicator function"
+
+lemma ereal_indicator: "ereal (indicator A x) = indicator A x"
+ by (auto simp: indicator_def one_ereal_def)
+
+lemma ereal_indicator_pos[simp,intro]: "0 \<le> (indicator A x ::ereal)"
+ unfolding indicator_def by auto
+
+lemma LIMSEQ_indicator_UN:
+ "(\<lambda>k. indicator (\<Union> i<k. A i) x) ----> (indicator (\<Union>i. A i) x :: real)"
+proof cases
+ assume "\<exists>i. x \<in> A i" then guess i .. note i = this
+ then have *: "\<And>n. (indicator (\<Union> i<n + Suc i. A i) x :: real) = 1"
+ "(indicator (\<Union> i. A i) x :: real) = 1" by (auto simp: indicator_def)
+ show ?thesis
+ apply (rule LIMSEQ_offset[of _ "Suc i"]) unfolding * by auto
+qed (auto simp: indicator_def)
+
+lemma indicator_add:
+ "A \<inter> B = {} \<Longrightarrow> (indicator A x::_::monoid_add) + indicator B x = indicator (A \<union> B) x"
+ unfolding indicator_def by auto
+
lemma suminf_cmult_indicator:
fixes f :: "nat \<Rightarrow> ereal"
assumes "disjoint_family A" "x \<in> A i" "\<And>i. 0 \<le> f i"
@@ -111,7 +133,7 @@
"increasing M f \<Longrightarrow> x \<subseteq> y \<Longrightarrow> x\<in>M \<Longrightarrow> y\<in>M \<Longrightarrow> f x \<le> f y"
by (auto simp add: increasing_def)
-lemma countably_additiveI:
+lemma countably_additiveI[case_names countably]:
"(\<And>A. range A \<subseteq> M \<Longrightarrow> disjoint_family A \<Longrightarrow> (\<Union>i. A i) \<in> M \<Longrightarrow> (\<Sum>i. f (A i)) = f (\<Union>i. A i))
\<Longrightarrow> countably_additive M f"
by (simp add: countably_additive_def)
@@ -1114,6 +1136,9 @@
show "sigma_algebra (space N) (sets N)" ..
qed fact
+lemma distr_id[simp]: "distr N N (\<lambda>x. x) = N"
+ by (rule measure_eqI) (auto simp: emeasure_distr)
+
lemma measure_distr:
"f \<in> measurable M N \<Longrightarrow> S \<in> sets N \<Longrightarrow> measure (distr M N f) S = measure M (f -` S \<inter> space M)"
by (simp add: emeasure_distr measure_def)
@@ -1389,6 +1414,107 @@
shows "measure M A = measure M B"
using assms emeasure_eq_AE[OF assms] by (simp add: emeasure_eq_measure)
+lemma (in finite_measure) measure_increasing: "increasing M (measure M)"
+ by (auto intro!: finite_measure_mono simp: increasing_def)
+
+lemma (in finite_measure) measure_zero_union:
+ assumes "s \<in> sets M" "t \<in> sets M" "measure M t = 0"
+ shows "measure M (s \<union> t) = measure M s"
+using assms
+proof -
+ have "measure M (s \<union> t) \<le> measure M s"
+ using finite_measure_subadditive[of s t] assms by auto
+ moreover have "measure M (s \<union> t) \<ge> measure M s"
+ using assms by (blast intro: finite_measure_mono)
+ ultimately show ?thesis by simp
+qed
+
+lemma (in finite_measure) measure_eq_compl:
+ assumes "s \<in> sets M" "t \<in> sets M"
+ assumes "measure M (space M - s) = measure M (space M - t)"
+ shows "measure M s = measure M t"
+ using assms finite_measure_compl by auto
+
+lemma (in finite_measure) measure_eq_bigunion_image:
+ assumes "range f \<subseteq> sets M" "range g \<subseteq> sets M"
+ assumes "disjoint_family f" "disjoint_family g"
+ assumes "\<And> n :: nat. measure M (f n) = measure M (g n)"
+ shows "measure M (\<Union> i. f i) = measure M (\<Union> i. g i)"
+using assms
+proof -
+ have a: "(\<lambda> i. measure M (f i)) sums (measure M (\<Union> i. f i))"
+ by (rule finite_measure_UNION[OF assms(1,3)])
+ have b: "(\<lambda> i. measure M (g i)) sums (measure M (\<Union> i. g i))"
+ by (rule finite_measure_UNION[OF assms(2,4)])
+ show ?thesis using sums_unique[OF b] sums_unique[OF a] assms by simp
+qed
+
+lemma (in finite_measure) measure_countably_zero:
+ assumes "range c \<subseteq> sets M"
+ assumes "\<And> i. measure M (c i) = 0"
+ shows "measure M (\<Union> i :: nat. c i) = 0"
+proof (rule antisym)
+ show "measure M (\<Union> i :: nat. c i) \<le> 0"
+ using finite_measure_subadditive_countably[OF assms(1)] by (simp add: assms(2))
+qed (simp add: measure_nonneg)
+
+lemma (in finite_measure) measure_space_inter:
+ assumes events:"s \<in> sets M" "t \<in> sets M"
+ assumes "measure M t = measure M (space M)"
+ shows "measure M (s \<inter> t) = measure M s"
+proof -
+ have "measure M ((space M - s) \<union> (space M - t)) = measure M (space M - s)"
+ using events assms finite_measure_compl[of "t"] by (auto intro!: measure_zero_union)
+ also have "(space M - s) \<union> (space M - t) = space M - (s \<inter> t)"
+ by blast
+ finally show "measure M (s \<inter> t) = measure M s"
+ using events by (auto intro!: measure_eq_compl[of "s \<inter> t" s])
+qed
+
+lemma (in finite_measure) measure_equiprobable_finite_unions:
+ assumes s: "finite s" "\<And>x. x \<in> s \<Longrightarrow> {x} \<in> sets M"
+ assumes "\<And> x y. \<lbrakk>x \<in> s; y \<in> s\<rbrakk> \<Longrightarrow> measure M {x} = measure M {y}"
+ shows "measure M s = real (card s) * measure M {SOME x. x \<in> s}"
+proof cases
+ assume "s \<noteq> {}"
+ then have "\<exists> x. x \<in> s" by blast
+ from someI_ex[OF this] assms
+ have prob_some: "\<And> x. x \<in> s \<Longrightarrow> measure M {x} = measure M {SOME y. y \<in> s}" by blast
+ have "measure M s = (\<Sum> x \<in> s. measure M {x})"
+ using finite_measure_eq_setsum_singleton[OF s] by simp
+ also have "\<dots> = (\<Sum> x \<in> s. measure M {SOME y. y \<in> s})" using prob_some by auto
+ also have "\<dots> = real (card s) * measure M {(SOME x. x \<in> s)}"
+ using setsum_constant assms by (simp add: real_eq_of_nat)
+ finally show ?thesis by simp
+qed simp
+
+lemma (in finite_measure) measure_real_sum_image_fn:
+ assumes "e \<in> sets M"
+ assumes "\<And> x. x \<in> s \<Longrightarrow> e \<inter> f x \<in> sets M"
+ assumes "finite s"
+ assumes disjoint: "\<And> x y. \<lbrakk>x \<in> s ; y \<in> s ; x \<noteq> y\<rbrakk> \<Longrightarrow> f x \<inter> f y = {}"
+ assumes upper: "space M \<subseteq> (\<Union> i \<in> s. f i)"
+ shows "measure M e = (\<Sum> x \<in> s. measure M (e \<inter> f x))"
+proof -
+ have e: "e = (\<Union> i \<in> s. e \<inter> f i)"
+ using `e \<in> sets M` sets_into_space upper by blast
+ hence "measure M e = measure M (\<Union> i \<in> s. e \<inter> f i)" by simp
+ also have "\<dots> = (\<Sum> x \<in> s. measure M (e \<inter> f x))"
+ proof (rule finite_measure_finite_Union)
+ show "finite s" by fact
+ show "(\<lambda>i. e \<inter> f i)`s \<subseteq> sets M" using assms(2) by auto
+ show "disjoint_family_on (\<lambda>i. e \<inter> f i) s"
+ using disjoint by (auto simp: disjoint_family_on_def)
+ qed
+ finally show ?thesis .
+qed
+
+lemma (in finite_measure) measure_exclude:
+ assumes "A \<in> sets M" "B \<in> sets M"
+ assumes "measure M A = measure M (space M)" "A \<inter> B = {}"
+ shows "measure M B = 0"
+ using measure_space_inter[of B A] assms by (auto simp: ac_simps)
+
section {* Counting space *}
lemma strict_monoI_Suc:
--- a/src/HOL/Probability/Probability_Measure.thy Fri Nov 16 18:49:46 2012 +0100
+++ b/src/HOL/Probability/Probability_Measure.thy Fri Nov 16 18:45:57 2012 +0100
@@ -9,125 +9,6 @@
imports Lebesgue_Measure Radon_Nikodym
begin
-lemma funset_eq_UN_fun_upd_I:
- assumes *: "\<And>f. f \<in> F (insert a A) \<Longrightarrow> f(a := d) \<in> F A"
- and **: "\<And>f. f \<in> F (insert a A) \<Longrightarrow> f a \<in> G (f(a:=d))"
- and ***: "\<And>f x. \<lbrakk> f \<in> F A ; x \<in> G f \<rbrakk> \<Longrightarrow> f(a:=x) \<in> F (insert a A)"
- shows "F (insert a A) = (\<Union>f\<in>F A. fun_upd f a ` (G f))"
-proof safe
- fix f assume f: "f \<in> F (insert a A)"
- show "f \<in> (\<Union>f\<in>F A. fun_upd f a ` G f)"
- proof (rule UN_I[of "f(a := d)"])
- show "f(a := d) \<in> F A" using *[OF f] .
- show "f \<in> fun_upd (f(a:=d)) a ` G (f(a:=d))"
- proof (rule image_eqI[of _ _ "f a"])
- show "f a \<in> G (f(a := d))" using **[OF f] .
- qed simp
- qed
-next
- fix f x assume "f \<in> F A" "x \<in> G f"
- from ***[OF this] show "f(a := x) \<in> F (insert a A)" .
-qed
-
-lemma extensional_funcset_insert_eq[simp]:
- assumes "a \<notin> A"
- shows "extensional (insert a A) \<inter> (insert a A \<rightarrow> B) = (\<Union>f \<in> extensional A \<inter> (A \<rightarrow> B). (\<lambda>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 \<inter> (A \<rightarrow> B))"
- using assms by induct auto
-
-lemma finite_PiE[simp, intro]:
- assumes fin: "finite A" "\<And>i. i \<in> A \<Longrightarrow> finite (B i)"
- shows "finite (Pi\<^isub>E A B)"
-proof -
- have *: "(Pi\<^isub>E A B) \<subseteq> extensional A \<inter> (A \<rightarrow> (\<Union>i\<in>A. B i))" by auto
- show ?thesis
- using fin by (intro finite_subset[OF *] finite_extensional_funcset) auto
-qed
-
-
-lemma countably_additiveI[case_names countably]:
- assumes "\<And>A. \<lbrakk> range A \<subseteq> M ; disjoint_family A ; (\<Union>i. A i) \<in> M\<rbrakk> \<Longrightarrow> (\<Sum>n. \<mu> (A n)) = \<mu> (\<Union>i. A i)"
- shows "countably_additive M \<mu>"
- using assms unfolding countably_additive_def by auto
-
-lemma convex_le_Inf_differential:
- fixes f :: "real \<Rightarrow> real"
- assumes "convex_on I f"
- assumes "x \<in> interior I" "y \<in> I"
- shows "f y \<ge> f x + Inf ((\<lambda>t. (f x - f t) / (x - t)) ` ({x<..} \<inter> I)) * (y - x)"
- (is "_ \<ge> _ + Inf (?F x) * (y - x)")
-proof -
- show ?thesis
- proof (cases rule: linorder_cases)
- assume "x < y"
- moreover
- have "open (interior I)" by auto
- from openE[OF this `x \<in> interior I`] guess e . note e = this
- moreover def t \<equiv> "min (x + e / 2) ((x + y) / 2)"
- ultimately have "x < t" "t < y" "t \<in> ball x e"
- by (auto simp: dist_real_def field_simps split: split_min)
- with `x \<in> interior I` e interior_subset[of I] have "t \<in> I" "x \<in> I" by auto
-
- have "open (interior I)" by auto
- from openE[OF this `x \<in> interior I`] guess e .
- moreover def K \<equiv> "x - e / 2"
- with `0 < e` have "K \<in> ball x e" "K < x" by (auto simp: dist_real_def)
- ultimately have "K \<in> I" "K < x" "x \<in> I"
- using interior_subset[of I] `x \<in> interior I` by auto
-
- have "Inf (?F x) \<le> (f x - f y) / (x - y)"
- proof (rule Inf_lower2)
- show "(f x - f t) / (x - t) \<in> ?F x"
- using `t \<in> I` `x < t` by auto
- show "(f x - f t) / (x - t) \<le> (f x - f y) / (x - y)"
- using `convex_on I f` `x \<in> I` `y \<in> I` `x < t` `t < y` by (rule convex_on_diff)
- next
- fix y assume "y \<in> ?F x"
- with order_trans[OF convex_on_diff[OF `convex_on I f` `K \<in> I` _ `K < x` _]]
- show "(f K - f x) / (K - x) \<le> 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 \<in> interior I`] guess e . note e = this
- moreover def t \<equiv> "x + e / 2"
- ultimately have "x < t" "t \<in> ball x e"
- by (auto simp: dist_real_def field_simps)
- with `x \<in> interior I` e interior_subset[of I] have "t \<in> I" "x \<in> I" by auto
-
- have "(f x - f y) / (x - y) \<le> 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 \<in> ?F x"
- with order_trans[OF convex_on_diff[OF `convex_on I f` `y \<in> I` _ `y < x`]]
- have "(f y - f x) / (y - x) \<le> z" by auto
- finally show "(f x - f y) / (x - y) \<le> z" .
- next
- have "open (interior I)" by auto
- from openE[OF this `x \<in> interior I`] guess e . note e = this
- then have "x + e / 2 \<in> ball x e" by (auto simp: dist_real_def)
- with e interior_subset[of I] have "x + e / 2 \<in> {x<..} \<inter> I" by auto
- then show "?F x \<noteq> {}" by blast
- qed
- then show ?thesis
- using `y < x` by (simp add: field_simps)
- qed simp
-qed
-
-lemma distr_id[simp]: "distr N N (\<lambda>x. x) = N"
- by (rule measure_eqI) (auto simp: emeasure_distr)
-
locale prob_space = finite_measure +
assumes emeasure_space_1: "emeasure M (space M) = 1"
@@ -230,101 +111,6 @@
then show False by auto
qed
-lemma (in finite_measure) prob_space_increasing: "increasing M (measure M)"
- by (auto intro!: finite_measure_mono simp: increasing_def)
-
-lemma (in finite_measure) prob_zero_union:
- assumes "s \<in> sets M" "t \<in> sets M" "measure M t = 0"
- shows "measure M (s \<union> t) = measure M s"
-using assms
-proof -
- have "measure M (s \<union> t) \<le> measure M s"
- using finite_measure_subadditive[of s t] assms by auto
- moreover have "measure M (s \<union> t) \<ge> measure M s"
- using assms by (blast intro: finite_measure_mono)
- ultimately show ?thesis by simp
-qed
-
-lemma (in finite_measure) prob_eq_compl:
- assumes "s \<in> sets M" "t \<in> sets M"
- assumes "measure M (space M - s) = measure M (space M - t)"
- shows "measure M s = measure M t"
- using assms finite_measure_compl by auto
-
-lemma (in prob_space) prob_one_inter:
- assumes events:"s \<in> events" "t \<in> events"
- assumes "prob t = 1"
- shows "prob (s \<inter> t) = prob s"
-proof -
- have "prob ((space M - s) \<union> (space M - t)) = prob (space M - s)"
- using events assms prob_compl[of "t"] by (auto intro!: prob_zero_union)
- also have "(space M - s) \<union> (space M - t) = space M - (s \<inter> t)"
- by blast
- finally show "prob (s \<inter> t) = prob s"
- using events by (auto intro!: prob_eq_compl[of "s \<inter> t" s])
-qed
-
-lemma (in finite_measure) prob_eq_bigunion_image:
- assumes "range f \<subseteq> sets M" "range g \<subseteq> sets M"
- assumes "disjoint_family f" "disjoint_family g"
- assumes "\<And> n :: nat. measure M (f n) = measure M (g n)"
- shows "measure M (\<Union> i. f i) = measure M (\<Union> i. g i)"
-using assms
-proof -
- have a: "(\<lambda> i. measure M (f i)) sums (measure M (\<Union> i. f i))"
- by (rule finite_measure_UNION[OF assms(1,3)])
- have b: "(\<lambda> i. measure M (g i)) sums (measure M (\<Union> i. g i))"
- by (rule finite_measure_UNION[OF assms(2,4)])
- show ?thesis using sums_unique[OF b] sums_unique[OF a] assms by simp
-qed
-
-lemma (in finite_measure) prob_countably_zero:
- assumes "range c \<subseteq> sets M"
- assumes "\<And> i. measure M (c i) = 0"
- shows "measure M (\<Union> i :: nat. c i) = 0"
-proof (rule antisym)
- show "measure M (\<Union> i :: nat. c i) \<le> 0"
- using finite_measure_subadditive_countably[OF assms(1)] by (simp add: assms(2))
-qed (simp add: measure_nonneg)
-
-lemma (in prob_space) prob_equiprobable_finite_unions:
- assumes "s \<in> events"
- assumes s_finite: "finite s" "\<And>x. x \<in> s \<Longrightarrow> {x} \<in> events"
- assumes "\<And> x y. \<lbrakk>x \<in> s; y \<in> s\<rbrakk> \<Longrightarrow> (prob {x} = prob {y})"
- shows "prob s = real (card s) * prob {SOME x. x \<in> s}"
-proof (cases "s = {}")
- case False hence "\<exists> x. x \<in> s" by blast
- from someI_ex[OF this] assms
- have prob_some: "\<And> x. x \<in> s \<Longrightarrow> prob {x} = prob {SOME y. y \<in> s}" by blast
- have "prob s = (\<Sum> x \<in> s. prob {x})"
- using finite_measure_eq_setsum_singleton[OF s_finite] by simp
- also have "\<dots> = (\<Sum> x \<in> s. prob {SOME y. y \<in> s})" using prob_some by auto
- also have "\<dots> = real (card s) * prob {(SOME x. x \<in> s)}"
- using setsum_constant assms by (simp add: real_eq_of_nat)
- finally show ?thesis by simp
-qed simp
-
-lemma (in prob_space) prob_real_sum_image_fn:
- assumes "e \<in> events"
- assumes "\<And> x. x \<in> s \<Longrightarrow> e \<inter> f x \<in> events"
- assumes "finite s"
- assumes disjoint: "\<And> x y. \<lbrakk>x \<in> s ; y \<in> s ; x \<noteq> y\<rbrakk> \<Longrightarrow> f x \<inter> f y = {}"
- assumes upper: "space M \<subseteq> (\<Union> i \<in> s. f i)"
- shows "prob e = (\<Sum> x \<in> s. prob (e \<inter> f x))"
-proof -
- have e: "e = (\<Union> i \<in> s. e \<inter> f i)"
- using `e \<in> events` sets_into_space upper by blast
- hence "prob e = prob (\<Union> i \<in> s. e \<inter> f i)" by simp
- also have "\<dots> = (\<Sum> x \<in> s. prob (e \<inter> f x))"
- proof (rule finite_measure_finite_Union)
- show "finite s" by fact
- show "(\<lambda>i. e \<inter> f i)`s \<subseteq> events" using assms(2) by auto
- show "disjoint_family_on (\<lambda>i. e \<inter> f i) s"
- using disjoint by (auto simp: disjoint_family_on_def)
- qed
- finally show ?thesis .
-qed
-
lemma (in prob_space) expectation_less:
assumes [simp]: "integrable M X"
assumes gt: "AE x in M. X x < b"
@@ -398,14 +184,6 @@
finally show "q (expectation X) \<le> expectation (\<lambda>x. q (X x))" .
qed
-lemma (in prob_space) prob_x_eq_1_imp_prob_y_eq_0:
- assumes "{x} \<in> events"
- assumes "prob {x} = 1"
- assumes "{y} \<in> events"
- assumes "y \<noteq> x"
- shows "prob {y} = 0"
- using prob_one_inter[of "{y}" "{x}"] assms by auto
-
subsection {* Introduce binder for probability *}
syntax
--- a/src/HOL/Product_Type.thy Fri Nov 16 18:49:46 2012 +0100
+++ b/src/HOL/Product_Type.thy Fri Nov 16 18:45:57 2012 +0100
@@ -393,6 +393,9 @@
from `PROP P (fst x, snd x)` show "PROP P x" by simp
qed
+lemma case_prod_distrib: "f (case x of (x, y) \<Rightarrow> g x y) = (case x of (x, y) \<Rightarrow> f (g x y))"
+ by (cases x) simp
+
text {*
The rule @{thm [source] split_paired_all} does not work with the
Simplifier because it also affects premises in congrence rules,
@@ -495,6 +498,10 @@
lemma split_beta [mono]: "(%(x, y). P x y) z = P (fst z) (snd z)"
by (subst surjective_pairing, rule split_conv)
+lemma split_beta': "(\<lambda>(x,y). f x y) = (\<lambda>x. f (fst x) (snd x))"
+ by (auto simp: fun_eq_iff)
+
+
lemma split_split [no_atp]: "R(split c p) = (ALL x y. p = (x, y) --> R(c x y))"
-- {* For use with @{text split} and the Simplifier. *}
by (insert surj_pair [of p], clarify, simp)
@@ -1019,6 +1026,9 @@
lemma Times_empty[simp]: "A \<times> B = {} \<longleftrightarrow> A = {} \<or> B = {}"
by auto
+lemma times_eq_iff: "A \<times> B = C \<times> D \<longleftrightarrow> A = C \<and> B = D \<or> ((A = {} \<or> B = {}) \<and> (C = {} \<or> D = {}))"
+ by auto
+
lemma fst_image_times[simp]: "fst ` (A \<times> B) = (if B = {} then {} else A)"
by force
@@ -1036,6 +1046,9 @@
apply auto
done
+lemma times_Int_times: "A \<times> B \<inter> C \<times> D = (A \<inter> C) \<times> (B \<inter> D)"
+ by auto
+
lemma swap_inj_on:
"inj_on (\<lambda>(i, j). (j, i)) A"
by (auto intro!: inj_onI)