1.1 --- a/src/HOL/Library/Convex.thy Thu Jun 09 11:57:39 2011 +0200
1.2 +++ b/src/HOL/Library/Convex.thy Thu Jun 09 14:24:34 2011 +0200
1.3 @@ -465,6 +465,25 @@
1.4 thus "convex_on C f" unfolding convex_on_def by auto
1.5 qed
1.6
1.7 +lemma convex_on_diff:
1.8 + fixes f :: "real \<Rightarrow> real"
1.9 + assumes f: "convex_on I f" and I: "x\<in>I" "y\<in>I" and t: "x < t" "t < y"
1.10 + shows "(f x - f t) / (x - t) \<le> (f x - f y) / (x - y)" "(f x - f y) / (x - y) \<le> (f t - f y) / (t - y)"
1.11 +proof -
1.12 + def a \<equiv> "(t - y) / (x - y)"
1.13 + with t have "0 \<le> a" "0 \<le> 1 - a" by (auto simp: field_simps)
1.14 + with f `x \<in> I` `y \<in> I` have cvx: "f (a * x + (1 - a) * y) \<le> a * f x + (1 - a) * f y"
1.15 + by (auto simp: convex_on_def)
1.16 + have "a * x + (1 - a) * y = a * (x - y) + y" by (simp add: field_simps)
1.17 + also have "\<dots> = t" unfolding a_def using `x < t` `t < y` by simp
1.18 + finally have "f t \<le> a * f x + (1 - a) * f y" using cvx by simp
1.19 + also have "\<dots> = a * (f x - f y) + f y" by (simp add: field_simps)
1.20 + finally have "f t - f y \<le> a * (f x - f y)" by simp
1.21 + with t show "(f x - f t) / (x - t) \<le> (f x - f y) / (x - y)"
1.22 + by (simp add: times_divide_eq le_divide_eq divide_le_eq field_simps a_def)
1.23 + with t show "(f x - f y) / (x - y) \<le> (f t - f y) / (t - y)"
1.24 + by (simp add: times_divide_eq le_divide_eq divide_le_eq field_simps)
1.25 +qed
1.26
1.27 lemma pos_convex_function:
1.28 fixes f :: "real \<Rightarrow> real"
2.1 --- a/src/HOL/Ln.thy Thu Jun 09 11:57:39 2011 +0200
2.2 +++ b/src/HOL/Ln.thy Thu Jun 09 14:24:34 2011 +0200
2.3 @@ -387,4 +387,47 @@
2.4 finally show ?thesis using b by (simp add: field_simps)
2.5 qed
2.6
2.7 +lemma ln_le_minus_one:
2.8 + "0 < x \<Longrightarrow> ln x \<le> x - 1"
2.9 + using exp_ge_add_one_self[of "ln x"] by simp
2.10 +
2.11 +lemma ln_eq_minus_one:
2.12 + assumes "0 < x" "ln x = x - 1" shows "x = 1"
2.13 +proof -
2.14 + let "?l y" = "ln y - y + 1"
2.15 + have D: "\<And>x. 0 < x \<Longrightarrow> DERIV ?l x :> (1 / x - 1)"
2.16 + by (auto intro!: DERIV_intros)
2.17 +
2.18 + show ?thesis
2.19 + proof (cases rule: linorder_cases)
2.20 + assume "x < 1"
2.21 + from dense[OF `x < 1`] obtain a where "x < a" "a < 1" by blast
2.22 + from `x < a` have "?l x < ?l a"
2.23 + proof (rule DERIV_pos_imp_increasing, safe)
2.24 + fix y assume "x \<le> y" "y \<le> a"
2.25 + with `0 < x` `a < 1` have "0 < 1 / y - 1" "0 < y"
2.26 + by (auto simp: field_simps)
2.27 + with D show "\<exists>z. DERIV ?l y :> z \<and> 0 < z"
2.28 + by auto
2.29 + qed
2.30 + also have "\<dots> \<le> 0"
2.31 + using ln_le_minus_one `0 < x` `x < a` by (auto simp: field_simps)
2.32 + finally show "x = 1" using assms by auto
2.33 + next
2.34 + assume "1 < x"
2.35 + from dense[OF `1 < x`] obtain a where "1 < a" "a < x" by blast
2.36 + from `a < x` have "?l x < ?l a"
2.37 + proof (rule DERIV_neg_imp_decreasing, safe)
2.38 + fix y assume "a \<le> y" "y \<le> x"
2.39 + with `1 < a` have "1 / y - 1 < 0" "0 < y"
2.40 + by (auto simp: field_simps)
2.41 + with D show "\<exists>z. DERIV ?l y :> z \<and> z < 0"
2.42 + by blast
2.43 + qed
2.44 + also have "\<dots> \<le> 0"
2.45 + using ln_le_minus_one `1 < a` by (auto simp: field_simps)
2.46 + finally show "x = 1" using assms by auto
2.47 + qed simp
2.48 +qed
2.49 +
2.50 end
3.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy Thu Jun 09 11:57:39 2011 +0200
3.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy Thu Jun 09 14:24:34 2011 +0200
3.3 @@ -105,6 +105,22 @@
3.4 "a \<in> s \<Longrightarrow> open s \<Longrightarrow> ((f has_derivative f') (at a within s) \<longleftrightarrow> (f has_derivative f') (at a))"
3.5 by (simp only: at_within_interior interior_open)
3.6
3.7 +lemma has_derivative_right:
3.8 + fixes f :: "real \<Rightarrow> real" and y :: "real"
3.9 + shows "(f has_derivative (op * y)) (at x within ({x <..} \<inter> I)) \<longleftrightarrow>
3.10 + ((\<lambda>t. (f x - f t) / (x - t)) ---> y) (at x within ({x <..} \<inter> I))"
3.11 +proof -
3.12 + have "((\<lambda>t. (f t - (f x + y * (t - x))) / \<bar>t - x\<bar>) ---> 0) (at x within ({x<..} \<inter> I)) \<longleftrightarrow>
3.13 + ((\<lambda>t. (f t - f x) / (t - x) - y) ---> 0) (at x within ({x<..} \<inter> I))"
3.14 + by (intro Lim_cong_within) (auto simp add: divide.diff divide.add)
3.15 + also have "\<dots> \<longleftrightarrow> ((\<lambda>t. (f t - f x) / (t - x)) ---> y) (at x within ({x<..} \<inter> I))"
3.16 + by (simp add: Lim_null[symmetric])
3.17 + also have "\<dots> \<longleftrightarrow> ((\<lambda>t. (f x - f t) / (x - t)) ---> y) (at x within ({x<..} \<inter> I))"
3.18 + by (intro Lim_cong_within) (simp_all add: times_divide_eq field_simps)
3.19 + finally show ?thesis
3.20 + by (simp add: mult.bounded_linear_right has_derivative_within)
3.21 +qed
3.22 +
3.23 lemma bounded_linear_imp_linear: "bounded_linear f \<Longrightarrow> linear f" (* TODO: move elsewhere *)
3.24 proof -
3.25 assume "bounded_linear f"
4.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Thu Jun 09 11:57:39 2011 +0200
4.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Thu Jun 09 14:24:34 2011 +0200
4.3 @@ -1122,6 +1122,100 @@
4.4 thus ?lhs by (rule Lim_at_within)
4.5 qed
4.6
4.7 +lemma Lim_within_LIMSEQ:
4.8 + fixes a :: real and L :: "'a::metric_space"
4.9 + assumes "\<forall>S. (\<forall>n. S n \<noteq> a \<and> S n \<in> T) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L"
4.10 + shows "(X ---> L) (at a within T)"
4.11 +proof (rule ccontr)
4.12 + assume "\<not> (X ---> L) (at a within T)"
4.13 + hence "\<exists>r>0. \<forall>s>0. \<exists>x\<in>T. x \<noteq> a \<and> \<bar>x - a\<bar> < s \<and> r \<le> dist (X x) L"
4.14 + unfolding tendsto_iff eventually_within dist_norm by (simp add: not_less[symmetric])
4.15 + then obtain r where r: "r > 0" "\<And>s. s > 0 \<Longrightarrow> \<exists>x\<in>T-{a}. \<bar>x - a\<bar> < s \<and> dist (X x) L \<ge> r" by blast
4.16 +
4.17 + let ?F = "\<lambda>n::nat. SOME x. x \<in> T \<and> x \<noteq> a \<and> \<bar>x - a\<bar> < inverse (real (Suc n)) \<and> dist (X x) L \<ge> r"
4.18 + have "\<And>n. \<exists>x. x \<in> T \<and> x \<noteq> a \<and> \<bar>x - a\<bar> < inverse (real (Suc n)) \<and> dist (X x) L \<ge> r"
4.19 + using r by (simp add: Bex_def)
4.20 + hence F: "\<And>n. ?F n \<in> T \<and> ?F n \<noteq> a \<and> \<bar>?F n - a\<bar> < inverse (real (Suc n)) \<and> dist (X (?F n)) L \<ge> r"
4.21 + by (rule someI_ex)
4.22 + hence F1: "\<And>n. ?F n \<in> T \<and> ?F n \<noteq> a"
4.23 + and F2: "\<And>n. \<bar>?F n - a\<bar> < inverse (real (Suc n))"
4.24 + and F3: "\<And>n. dist (X (?F n)) L \<ge> r"
4.25 + by fast+
4.26 +
4.27 + have "?F ----> a"
4.28 + proof (rule LIMSEQ_I, unfold real_norm_def)
4.29 + fix e::real
4.30 + assume "0 < e"
4.31 + (* choose no such that inverse (real (Suc n)) < e *)
4.32 + then have "\<exists>no. inverse (real (Suc no)) < e" by (rule reals_Archimedean)
4.33 + then obtain m where nodef: "inverse (real (Suc m)) < e" by auto
4.34 + show "\<exists>no. \<forall>n. no \<le> n --> \<bar>?F n - a\<bar> < e"
4.35 + proof (intro exI allI impI)
4.36 + fix n
4.37 + assume mlen: "m \<le> n"
4.38 + have "\<bar>?F n - a\<bar> < inverse (real (Suc n))"
4.39 + by (rule F2)
4.40 + also have "inverse (real (Suc n)) \<le> inverse (real (Suc m))"
4.41 + using mlen by auto
4.42 + also from nodef have
4.43 + "inverse (real (Suc m)) < e" .
4.44 + finally show "\<bar>?F n - a\<bar> < e" .
4.45 + qed
4.46 + qed
4.47 + moreover note `\<forall>S. (\<forall>n. S n \<noteq> a \<and> S n \<in> T) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L`
4.48 + ultimately have "(\<lambda>n. X (?F n)) ----> L" using F1 by simp
4.49 +
4.50 + moreover have "\<not> ((\<lambda>n. X (?F n)) ----> L)"
4.51 + proof -
4.52 + {
4.53 + fix no::nat
4.54 + obtain n where "n = no + 1" by simp
4.55 + then have nolen: "no \<le> n" by simp
4.56 + (* We prove this by showing that for any m there is an n\<ge>m such that |X (?F n) - L| \<ge> r *)
4.57 + have "dist (X (?F n)) L \<ge> r"
4.58 + by (rule F3)
4.59 + with nolen have "\<exists>n. no \<le> n \<and> dist (X (?F n)) L \<ge> r" by fast
4.60 + }
4.61 + then have "(\<forall>no. \<exists>n. no \<le> n \<and> dist (X (?F n)) L \<ge> r)" by simp
4.62 + with r have "\<exists>e>0. (\<forall>no. \<exists>n. no \<le> n \<and> dist (X (?F n)) L \<ge> e)" by auto
4.63 + thus ?thesis by (unfold LIMSEQ_def, auto simp add: not_less)
4.64 + qed
4.65 + ultimately show False by simp
4.66 +qed
4.67 +
4.68 +lemma Lim_right_bound:
4.69 + fixes f :: "real \<Rightarrow> real"
4.70 + assumes mono: "\<And>a b. a \<in> I \<Longrightarrow> b \<in> I \<Longrightarrow> x < a \<Longrightarrow> a \<le> b \<Longrightarrow> f a \<le> f b"
4.71 + assumes bnd: "\<And>a. a \<in> I \<Longrightarrow> x < a \<Longrightarrow> K \<le> f a"
4.72 + shows "(f ---> Inf (f ` ({x<..} \<inter> I))) (at x within ({x<..} \<inter> I))"
4.73 +proof cases
4.74 + assume "{x<..} \<inter> I = {}" then show ?thesis by (simp add: Lim_within_empty)
4.75 +next
4.76 + assume [simp]: "{x<..} \<inter> I \<noteq> {}"
4.77 + show ?thesis
4.78 + proof (rule Lim_within_LIMSEQ, safe)
4.79 + fix S assume S: "\<forall>n. S n \<noteq> x \<and> S n \<in> {x <..} \<inter> I" "S ----> x"
4.80 +
4.81 + show "(\<lambda>n. f (S n)) ----> Inf (f ` ({x<..} \<inter> I))"
4.82 + proof (rule LIMSEQ_I, rule ccontr)
4.83 + fix r :: real assume "0 < r"
4.84 + with Inf_close[of "f ` ({x<..} \<inter> I)" r]
4.85 + obtain y where y: "x < y" "y \<in> I" "f y < Inf (f ` ({x <..} \<inter> I)) + r" by auto
4.86 + from `x < y` have "0 < y - x" by auto
4.87 + from S(2)[THEN LIMSEQ_D, OF this]
4.88 + obtain N where N: "\<And>n. N \<le> n \<Longrightarrow> \<bar>S n - x\<bar> < y - x" by auto
4.89 +
4.90 + assume "\<not> (\<exists>N. \<forall>n\<ge>N. norm (f (S n) - Inf (f ` ({x<..} \<inter> I))) < r)"
4.91 + moreover have "\<And>n. Inf (f ` ({x<..} \<inter> I)) \<le> f (S n)"
4.92 + using S bnd by (intro Inf_lower[where z=K]) auto
4.93 + ultimately obtain n where n: "N \<le> n" "r + Inf (f ` ({x<..} \<inter> I)) \<le> f (S n)"
4.94 + by (auto simp: not_less field_simps)
4.95 + with N[OF n(1)] mono[OF _ `y \<in> I`, of "S n"] S(1)[THEN spec, of n] y
4.96 + show False by auto
4.97 + qed
4.98 + qed
4.99 +qed
4.100 +
4.101 text{* Another limit point characterization. *}
4.102
4.103 lemma islimpt_sequential:
4.104 @@ -1505,14 +1599,16 @@
4.105 (* FIXME: Only one congruence rule for tendsto can be used at a time! *)
4.106
4.107 lemma Lim_cong_within(*[cong add]*):
4.108 - assumes "\<And>x. x \<noteq> a \<Longrightarrow> f x = g x"
4.109 - shows "((\<lambda>x. f x) ---> l) (at a within S) \<longleftrightarrow> ((g ---> l) (at a within S))"
4.110 + assumes "a = b" "x = y" "S = T"
4.111 + assumes "\<And>x. x \<noteq> b \<Longrightarrow> x \<in> T \<Longrightarrow> f x = g x"
4.112 + shows "(f ---> x) (at a within S) \<longleftrightarrow> (g ---> y) (at b within T)"
4.113 unfolding tendsto_def Limits.eventually_within eventually_at_topological
4.114 using assms by simp
4.115
4.116 lemma Lim_cong_at(*[cong add]*):
4.117 + assumes "a = b" "x = y"
4.118 assumes "\<And>x. x \<noteq> a \<Longrightarrow> f x = g x"
4.119 - shows "((\<lambda>x. f x) ---> l) (at a) \<longleftrightarrow> ((g ---> l) (at a))"
4.120 + shows "((\<lambda>x. f x) ---> x) (at a) \<longleftrightarrow> ((g ---> y) (at a))"
4.121 unfolding tendsto_def eventually_at_topological
4.122 using assms by simp
4.123
5.1 --- a/src/HOL/Probability/Independent_Family.thy Thu Jun 09 11:57:39 2011 +0200
5.2 +++ b/src/HOL/Probability/Independent_Family.thy Thu Jun 09 14:24:34 2011 +0200
5.3 @@ -117,6 +117,16 @@
5.4 using indep[unfolded indep_set_def, THEN indep_setsD, of UNIV "bool_case a b"] ev
5.5 by (simp add: ac_simps UNIV_bool)
5.6
5.7 +lemma (in prob_space) indep_var_eq:
5.8 + "indep_var S X T Y \<longleftrightarrow>
5.9 + (random_variable S X \<and> random_variable T Y) \<and>
5.10 + indep_set
5.11 + (sigma_sets (space M) { X -` A \<inter> space M | A. A \<in> sets S})
5.12 + (sigma_sets (space M) { Y -` A \<inter> space M | A. A \<in> sets T})"
5.13 + unfolding indep_var_def indep_vars_def indep_set_def UNIV_bool
5.14 + by (intro arg_cong2[where f="op \<and>"] arg_cong2[where f=indep_sets] ext)
5.15 + (auto split: bool.split)
5.16 +
5.17 lemma (in prob_space)
5.18 assumes indep: "indep_set A B"
5.19 shows indep_setD_ev1: "A \<subseteq> events"
5.20 @@ -491,7 +501,7 @@
5.21 proof (simp add: sigma_algebra_iff2, safe)
5.22 let ?A = "(\<Inter>n. sigma_sets (space M) (UNION {n..} A))"
5.23 interpret A: sigma_algebra "\<lparr>space = space M, sets = A i\<rparr>" for i by fact
5.24 - { fix X x assume "X \<in> ?A" "x \<in> X"
5.25 + { fix X x assume "X \<in> ?A" "x \<in> X"
5.26 then have "\<And>n. X \<in> sigma_sets (space M) (UNION {n..} A)" by auto
5.27 from this[of 0] have "X \<in> sigma_sets (space M) (UNION UNIV A)" by simp
5.28 then have "X \<subseteq> space M"
5.29 @@ -572,7 +582,7 @@
5.30 show "Int_stable \<lparr>space = space M, sets = A m\<rparr>"
5.31 unfolding Int_stable_def using A.Int by auto
5.32 qed
5.33 - also have "(\<lambda>b. sigma_sets (space M) (\<Union>m\<in>bool_case {..n} {Suc n..} b. A m)) =
5.34 + also have "(\<lambda>b. sigma_sets (space M) (\<Union>m\<in>bool_case {..n} {Suc n..} b. A m)) =
5.35 bool_case (sigma_sets (space M) (\<Union>m\<in>{..n}. A m)) (sigma_sets (space M) (\<Union>m\<in>{Suc n..}. A m))"
5.36 by (auto intro!: ext split: bool.split)
5.37 finally have indep: "indep_set (sigma_sets (space M) (\<Union>m\<in>{..n}. A m)) (sigma_sets (space M) (\<Union>m\<in>{Suc n..}. A m))"
5.38 @@ -732,7 +742,7 @@
5.39 by (auto simp del: vimage_Int intro!: exI[of _ "A \<inter> B"] dest: Int_stableD)
5.40 qed }
5.41 note indep_sets_sigma_sets_iff[OF this, simp]
5.42 -
5.43 +
5.44 { fix i assume "i \<in> I"
5.45 { fix A assume "A \<in> sets (M' i)"
5.46 then have "A \<in> sets (sigma (M' i))" by (auto simp: sets_sigma intro: sigma_sets.Basic)
5.47 @@ -745,7 +755,7 @@
5.48 "space M \<in> {X i -` A \<inter> space M |A. A \<in> sets (M' i)}"
5.49 by (auto intro!: exI[of _ "space (M' i)"]) }
5.50 note indep_sets_finite[OF I this, simp]
5.51 -
5.52 +
5.53 have "(\<forall>A\<in>\<Pi> i\<in>I. {X i -` A \<inter> space M |A. A \<in> sets (M' i)}. prob (INTER I A) = (\<Prod>j\<in>I. prob (A j))) =
5.54 (\<forall>A\<in>\<Pi> i\<in>I. sets (M' i). prob ((\<Inter>j\<in>I. X j -` A j) \<inter> space M) = (\<Prod>x\<in>I. prob (X x -` A x \<inter> space M)))"
5.55 (is "?L = ?R")
5.56 @@ -847,7 +857,7 @@
5.57 by (simp_all add: product_algebra_def)
5.58 show "A \<in> sets (sigma P.G)"
5.59 using `A \<in> sets P.P` by (simp add: product_algebra_def)
5.60 -
5.61 +
5.62 fix E assume E: "E \<in> sets P.G"
5.63 then have "E \<in> sets P.P"
5.64 by (simp add: sets_sigma sigma_sets.Basic product_algebra_def)
5.65 @@ -915,10 +925,67 @@
5.66 finally show ?thesis .
5.67 qed
5.68
5.69 +lemma (in prob_space)
5.70 + assumes "indep_var S X T Y"
5.71 + shows indep_var_rv1: "random_variable S X"
5.72 + and indep_var_rv2: "random_variable T Y"
5.73 +proof -
5.74 + have "\<forall>i\<in>UNIV. random_variable (bool_case S T i) (bool_case X Y i)"
5.75 + using assms unfolding indep_var_def indep_vars_def by auto
5.76 + then show "random_variable S X" "random_variable T Y"
5.77 + unfolding UNIV_bool by auto
5.78 +qed
5.79 +
5.80 lemma (in prob_space) indep_var_distributionD:
5.81 - assumes "indep_var Ma A Mb B"
5.82 - assumes "Xa \<in> sets Ma" "Xb \<in> sets Mb"
5.83 - shows "joint_distribution A B (Xa \<times> Xb) = distribution A Xa * distribution B Xb"
5.84 - unfolding distribution_def using assms by (rule indep_varD)
5.85 + assumes indep: "indep_var S X T Y"
5.86 + defines "P \<equiv> S\<lparr>measure := extreal\<circ>distribution X\<rparr> \<Otimes>\<^isub>M T\<lparr>measure := extreal\<circ>distribution Y\<rparr>"
5.87 + assumes "A \<in> sets P"
5.88 + shows "joint_distribution X Y A = finite_measure.\<mu>' P A"
5.89 +proof -
5.90 + from indep have rvs: "random_variable S X" "random_variable T Y"
5.91 + by (blast dest: indep_var_rv1 indep_var_rv2)+
5.92 +
5.93 + let ?S = "S\<lparr>measure := extreal\<circ>distribution X\<rparr>"
5.94 + let ?T = "T\<lparr>measure := extreal\<circ>distribution Y\<rparr>"
5.95 + interpret X: prob_space ?S by (rule distribution_prob_space) fact
5.96 + interpret Y: prob_space ?T by (rule distribution_prob_space) fact
5.97 + interpret XY: pair_prob_space ?S ?T by default
5.98 +
5.99 + let ?J = "XY.P\<lparr> measure := extreal \<circ> joint_distribution X Y \<rparr>"
5.100 + interpret J: prob_space ?J
5.101 + by (rule joint_distribution_prob_space) (simp_all add: rvs)
5.102 +
5.103 + have "finite_measure.\<mu>' (XY.P\<lparr> measure := extreal \<circ> joint_distribution X Y \<rparr>) A = XY.\<mu>' A"
5.104 + proof (rule prob_space_unique_Int_stable)
5.105 + show "Int_stable (pair_measure_generator ?S ?T)" (is "Int_stable ?P")
5.106 + by fact
5.107 + show "space ?P \<in> sets ?P"
5.108 + unfolding space_pair_measure[simplified pair_measure_def space_sigma]
5.109 + using X.top Y.top by (auto intro!: pair_measure_generatorI)
5.110 +
5.111 + show "prob_space ?J" by default
5.112 + show "space ?J = space ?P"
5.113 + by (simp add: pair_measure_generator_def space_pair_measure)
5.114 + show "sets ?J = sets (sigma ?P)"
5.115 + by (simp add: pair_measure_def)
5.116 +
5.117 + show "prob_space XY.P" by default
5.118 + show "space XY.P = space ?P" "sets XY.P = sets (sigma ?P)"
5.119 + by (simp_all add: pair_measure_generator_def pair_measure_def)
5.120 +
5.121 + show "A \<in> sets (sigma ?P)"
5.122 + using `A \<in> sets P` unfolding P_def pair_measure_def by simp
5.123 +
5.124 + fix X assume "X \<in> sets ?P"
5.125 + then obtain A B where "A \<in> sets S" "B \<in> sets T" "X = A \<times> B"
5.126 + by (auto simp: sets_pair_measure_generator)
5.127 + then show "J.\<mu>' X = XY.\<mu>' X"
5.128 + unfolding J.\<mu>'_def XY.\<mu>'_def using indep
5.129 + by (simp add: XY.pair_measure_times)
5.130 + (simp add: distribution_def indep_varD)
5.131 + qed
5.132 + then show ?thesis
5.133 + using `A \<in> sets P` unfolding P_def J.\<mu>'_def XY.\<mu>'_def by simp
5.134 +qed
5.135
5.136 end
6.1 --- a/src/HOL/Probability/Information.thy Thu Jun 09 11:57:39 2011 +0200
6.2 +++ b/src/HOL/Probability/Information.thy Thu Jun 09 14:24:34 2011 +0200
6.3 @@ -7,14 +7,10 @@
6.4
6.5 theory Information
6.6 imports
6.7 - Probability_Measure
6.8 + Independent_Family
6.9 "~~/src/HOL/Library/Convex"
6.10 begin
6.11
6.12 -lemma (in prob_space) not_zero_less_distribution[simp]:
6.13 - "(\<not> 0 < distribution X A) \<longleftrightarrow> distribution X A = 0"
6.14 - using distribution_positive[of X A] by arith
6.15 -
6.16 lemma log_le: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> x \<le> y \<Longrightarrow> log a x \<le> log a y"
6.17 by (subst log_le_cancel_iff) auto
6.18
6.19 @@ -175,7 +171,211 @@
6.20 Kullback$-$Leibler distance. *}
6.21
6.22 definition
6.23 - "KL_divergence b M \<nu> = \<integral>x. log b (real (RN_deriv M \<nu> x)) \<partial>M\<lparr>measure := \<nu>\<rparr>"
6.24 + "entropy_density b M \<nu> = log b \<circ> real \<circ> RN_deriv M \<nu>"
6.25 +
6.26 +definition
6.27 + "KL_divergence b M \<nu> = integral\<^isup>L (M\<lparr>measure := \<nu>\<rparr>) (entropy_density b M \<nu>)"
6.28 +
6.29 +lemma (in information_space) measurable_entropy_density:
6.30 + assumes ps: "prob_space (M\<lparr>measure := \<nu>\<rparr>)"
6.31 + assumes ac: "absolutely_continuous \<nu>"
6.32 + shows "entropy_density b M \<nu> \<in> borel_measurable M"
6.33 +proof -
6.34 + interpret \<nu>: prob_space "M\<lparr>measure := \<nu>\<rparr>" by fact
6.35 + have "measure_space (M\<lparr>measure := \<nu>\<rparr>)" by fact
6.36 + from RN_deriv[OF this ac] b_gt_1 show ?thesis
6.37 + unfolding entropy_density_def
6.38 + by (intro measurable_comp) auto
6.39 +qed
6.40 +
6.41 +lemma (in information_space) KL_gt_0:
6.42 + assumes ps: "prob_space (M\<lparr>measure := \<nu>\<rparr>)"
6.43 + assumes ac: "absolutely_continuous \<nu>"
6.44 + assumes int: "integrable (M\<lparr> measure := \<nu> \<rparr>) (entropy_density b M \<nu>)"
6.45 + assumes A: "A \<in> sets M" "\<nu> A \<noteq> \<mu> A"
6.46 + shows "0 < KL_divergence b M \<nu>"
6.47 +proof -
6.48 + interpret \<nu>: prob_space "M\<lparr>measure := \<nu>\<rparr>" by fact
6.49 + have ms: "measure_space (M\<lparr>measure := \<nu>\<rparr>)" by default
6.50 + have fms: "finite_measure (M\<lparr>measure := \<nu>\<rparr>)" by default
6.51 + note RN = RN_deriv[OF ms ac]
6.52 +
6.53 + from real_RN_deriv[OF fms ac] guess D . note D = this
6.54 + with absolutely_continuous_AE[OF ms] ac
6.55 + have D\<nu>: "AE x in M\<lparr>measure := \<nu>\<rparr>. RN_deriv M \<nu> x = extreal (D x)"
6.56 + by auto
6.57 +
6.58 + def f \<equiv> "\<lambda>x. if D x = 0 then 1 else 1 / D x"
6.59 + with D have f_borel: "f \<in> borel_measurable M"
6.60 + by (auto intro!: measurable_If)
6.61 +
6.62 + have "KL_divergence b M \<nu> = 1 / ln b * (\<integral> x. ln b * entropy_density b M \<nu> x \<partial>M\<lparr>measure := \<nu>\<rparr>)"
6.63 + unfolding KL_divergence_def using int b_gt_1
6.64 + by (simp add: integral_cmult)
6.65 +
6.66 + { fix A assume "A \<in> sets M"
6.67 + with RN D have "\<nu>.\<mu> A = (\<integral>\<^isup>+ x. extreal (D x) * indicator A x \<partial>M)"
6.68 + by (auto intro!: positive_integral_cong_AE) }
6.69 + note D_density = this
6.70 +
6.71 + have ln_entropy: "(\<lambda>x. ln b * entropy_density b M \<nu> x) \<in> borel_measurable M"
6.72 + using measurable_entropy_density[OF ps ac] by auto
6.73 +
6.74 + have "integrable (M\<lparr>measure := \<nu>\<rparr>) (\<lambda>x. ln b * entropy_density b M \<nu> x)"
6.75 + using int by auto
6.76 + moreover have "integrable (M\<lparr>measure := \<nu>\<rparr>) (\<lambda>x. ln b * entropy_density b M \<nu> x) \<longleftrightarrow>
6.77 + integrable M (\<lambda>x. D x * (ln b * entropy_density b M \<nu> x))"
6.78 + using D D_density ln_entropy
6.79 + by (intro integral_translated_density) auto
6.80 + ultimately have M_int: "integrable M (\<lambda>x. D x * (ln b * entropy_density b M \<nu> x))"
6.81 + by simp
6.82 +
6.83 + have D_neg: "(\<integral>\<^isup>+ x. extreal (- D x) \<partial>M) = 0"
6.84 + using D by (subst positive_integral_0_iff_AE) auto
6.85 +
6.86 + have "(\<integral>\<^isup>+ x. extreal (D x) \<partial>M) = \<nu> (space M)"
6.87 + using RN D by (auto intro!: positive_integral_cong_AE)
6.88 + then have D_pos: "(\<integral>\<^isup>+ x. extreal (D x) \<partial>M) = 1"
6.89 + using \<nu>.measure_space_1 by simp
6.90 +
6.91 + have "integrable M D"
6.92 + using D_pos D_neg D by (auto simp: integrable_def)
6.93 +
6.94 + have "integral\<^isup>L M D = 1"
6.95 + using D_pos D_neg by (auto simp: lebesgue_integral_def)
6.96 +
6.97 + let ?D_set = "{x\<in>space M. D x \<noteq> 0}"
6.98 + have [simp, intro]: "?D_set \<in> sets M"
6.99 + using D by (auto intro: sets_Collect)
6.100 +
6.101 + have "0 \<le> 1 - \<mu>' ?D_set"
6.102 + using prob_le_1 by (auto simp: field_simps)
6.103 + also have "\<dots> = (\<integral> x. D x - indicator ?D_set x \<partial>M)"
6.104 + using `integrable M D` `integral\<^isup>L M D = 1`
6.105 + by (simp add: \<mu>'_def)
6.106 + also have "\<dots> < (\<integral> x. D x * (ln b * entropy_density b M \<nu> x) \<partial>M)"
6.107 + proof (rule integral_less_AE)
6.108 + show "integrable M (\<lambda>x. D x - indicator ?D_set x)"
6.109 + using `integrable M D`
6.110 + by (intro integral_diff integral_indicator) auto
6.111 + next
6.112 + show "integrable M (\<lambda>x. D x * (ln b * entropy_density b M \<nu> x))"
6.113 + by fact
6.114 + next
6.115 + show "\<mu> {x\<in>space M. D x \<noteq> 1 \<and> D x \<noteq> 0} \<noteq> 0"
6.116 + proof
6.117 + assume eq_0: "\<mu> {x\<in>space M. D x \<noteq> 1 \<and> D x \<noteq> 0} = 0"
6.118 + then have disj: "AE x. D x = 1 \<or> D x = 0"
6.119 + using D(1) by (auto intro!: AE_I[OF subset_refl] sets_Collect)
6.120 +
6.121 + have "\<mu> {x\<in>space M. D x = 1} = (\<integral>\<^isup>+ x. indicator {x\<in>space M. D x = 1} x \<partial>M)"
6.122 + using D(1) by auto
6.123 + also have "\<dots> = (\<integral>\<^isup>+ x. extreal (D x) * indicator {x\<in>space M. D x \<noteq> 0} x \<partial>M)"
6.124 + using disj by (auto intro!: positive_integral_cong_AE simp: indicator_def one_extreal_def)
6.125 + also have "\<dots> = \<nu> {x\<in>space M. D x \<noteq> 0}"
6.126 + using D(1) D_density by auto
6.127 + also have "\<dots> = \<nu> (space M)"
6.128 + using D_density D(1) by (auto intro!: positive_integral_cong simp: indicator_def)
6.129 + finally have "AE x. D x = 1"
6.130 + using D(1) \<nu>.measure_space_1 by (intro AE_I_eq_1) auto
6.131 + then have "(\<integral>\<^isup>+x. indicator A x\<partial>M) = (\<integral>\<^isup>+x. extreal (D x) * indicator A x\<partial>M)"
6.132 + by (intro positive_integral_cong_AE) (auto simp: one_extreal_def[symmetric])
6.133 + also have "\<dots> = \<nu> A"
6.134 + using `A \<in> sets M` D_density by simp
6.135 + finally show False using `A \<in> sets M` `\<nu> A \<noteq> \<mu> A` by simp
6.136 + qed
6.137 + show "{x\<in>space M. D x \<noteq> 1 \<and> D x \<noteq> 0} \<in> sets M"
6.138 + using D(1) by (auto intro: sets_Collect)
6.139 +
6.140 + show "AE t. t \<in> {x\<in>space M. D x \<noteq> 1 \<and> D x \<noteq> 0} \<longrightarrow>
6.141 + D t - indicator ?D_set t \<noteq> D t * (ln b * entropy_density b M \<nu> t)"
6.142 + using D(2)
6.143 + proof (elim AE_mp, safe intro!: AE_I2)
6.144 + fix t assume Dt: "t \<in> space M" "D t \<noteq> 1" "D t \<noteq> 0"
6.145 + and RN: "RN_deriv M \<nu> t = extreal (D t)"
6.146 + and eq: "D t - indicator ?D_set t = D t * (ln b * entropy_density b M \<nu> t)"
6.147 +
6.148 + have "D t - 1 = D t - indicator ?D_set t"
6.149 + using Dt by simp
6.150 + also note eq
6.151 + also have "D t * (ln b * entropy_density b M \<nu> t) = - D t * ln (1 / D t)"
6.152 + using RN b_gt_1 `D t \<noteq> 0` `0 \<le> D t`
6.153 + by (simp add: entropy_density_def log_def ln_div less_le)
6.154 + finally have "ln (1 / D t) = 1 / D t - 1"
6.155 + using `D t \<noteq> 0` by (auto simp: field_simps)
6.156 + from ln_eq_minus_one[OF _ this] `D t \<noteq> 0` `0 \<le> D t` `D t \<noteq> 1`
6.157 + show False by auto
6.158 + qed
6.159 +
6.160 + show "AE t. D t - indicator ?D_set t \<le> D t * (ln b * entropy_density b M \<nu> t)"
6.161 + using D(2)
6.162 + proof (elim AE_mp, intro AE_I2 impI)
6.163 + fix t assume "t \<in> space M" and RN: "RN_deriv M \<nu> t = extreal (D t)"
6.164 + show "D t - indicator ?D_set t \<le> D t * (ln b * entropy_density b M \<nu> t)"
6.165 + proof cases
6.166 + assume asm: "D t \<noteq> 0"
6.167 + then have "0 < D t" using `0 \<le> D t` by auto
6.168 + then have "0 < 1 / D t" by auto
6.169 + have "D t - indicator ?D_set t \<le> - D t * (1 / D t - 1)"
6.170 + using asm `t \<in> space M` by (simp add: field_simps)
6.171 + also have "- D t * (1 / D t - 1) \<le> - D t * ln (1 / D t)"
6.172 + using ln_le_minus_one `0 < 1 / D t` by (intro mult_left_mono_neg) auto
6.173 + also have "\<dots> = D t * (ln b * entropy_density b M \<nu> t)"
6.174 + using `0 < D t` RN b_gt_1
6.175 + by (simp_all add: log_def ln_div entropy_density_def)
6.176 + finally show ?thesis by simp
6.177 + qed simp
6.178 + qed
6.179 + qed
6.180 + also have "\<dots> = (\<integral> x. ln b * entropy_density b M \<nu> x \<partial>M\<lparr>measure := \<nu>\<rparr>)"
6.181 + using D D_density ln_entropy
6.182 + by (intro integral_translated_density[symmetric]) auto
6.183 + also have "\<dots> = ln b * (\<integral> x. entropy_density b M \<nu> x \<partial>M\<lparr>measure := \<nu>\<rparr>)"
6.184 + using int by (rule \<nu>.integral_cmult)
6.185 + finally show "0 < KL_divergence b M \<nu>"
6.186 + using b_gt_1 by (auto simp: KL_divergence_def zero_less_mult_iff)
6.187 +qed
6.188 +
6.189 +lemma (in sigma_finite_measure) KL_eq_0:
6.190 + assumes eq: "\<forall>A\<in>sets M. \<nu> A = measure M A"
6.191 + shows "KL_divergence b M \<nu> = 0"
6.192 +proof -
6.193 + have "AE x. 1 = RN_deriv M \<nu> x"
6.194 + proof (rule RN_deriv_unique)
6.195 + show "measure_space (M\<lparr>measure := \<nu>\<rparr>)"
6.196 + using eq by (intro measure_space_cong) auto
6.197 + show "absolutely_continuous \<nu>"
6.198 + unfolding absolutely_continuous_def using eq by auto
6.199 + show "(\<lambda>x. 1) \<in> borel_measurable M" "AE x. 0 \<le> (1 :: extreal)" by auto
6.200 + fix A assume "A \<in> sets M"
6.201 + with eq show "\<nu> A = \<integral>\<^isup>+ x. 1 * indicator A x \<partial>M" by simp
6.202 + qed
6.203 + then have "AE x. log b (real (RN_deriv M \<nu> x)) = 0"
6.204 + by (elim AE_mp) simp
6.205 + from integral_cong_AE[OF this]
6.206 + have "integral\<^isup>L M (entropy_density b M \<nu>) = 0"
6.207 + by (simp add: entropy_density_def comp_def)
6.208 + with eq show "KL_divergence b M \<nu> = 0"
6.209 + unfolding KL_divergence_def
6.210 + by (subst integral_cong_measure) auto
6.211 +qed
6.212 +
6.213 +lemma (in information_space) KL_eq_0_imp:
6.214 + assumes ps: "prob_space (M\<lparr>measure := \<nu>\<rparr>)"
6.215 + assumes ac: "absolutely_continuous \<nu>"
6.216 + assumes int: "integrable (M\<lparr> measure := \<nu> \<rparr>) (entropy_density b M \<nu>)"
6.217 + assumes KL: "KL_divergence b M \<nu> = 0"
6.218 + shows "\<forall>A\<in>sets M. \<nu> A = \<mu> A"
6.219 + by (metis less_imp_neq KL_gt_0 assms)
6.220 +
6.221 +lemma (in information_space) KL_ge_0:
6.222 + assumes ps: "prob_space (M\<lparr>measure := \<nu>\<rparr>)"
6.223 + assumes ac: "absolutely_continuous \<nu>"
6.224 + assumes int: "integrable (M\<lparr> measure := \<nu> \<rparr>) (entropy_density b M \<nu>)"
6.225 + shows "0 \<le> KL_divergence b M \<nu>"
6.226 + using KL_eq_0 KL_gt_0[OF ps ac int]
6.227 + by (cases "\<forall>A\<in>sets M. \<nu> A = measure M A") (auto simp: le_less)
6.228 +
6.229
6.230 lemma (in sigma_finite_measure) KL_divergence_vimage:
6.231 assumes T: "T \<in> measure_preserving M M'"
6.232 @@ -209,7 +409,7 @@
6.233 have AE: "AE x. RN_deriv M' \<nu>' (T x) = RN_deriv M \<nu> x"
6.234 by (rule RN_deriv_vimage[OF T T' inv \<nu>'])
6.235 show ?thesis
6.236 - unfolding KL_divergence_def
6.237 + unfolding KL_divergence_def entropy_density_def comp_def
6.238 proof (subst \<nu>'.integral_vimage[OF sa T'])
6.239 show "(\<lambda>x. log b (real (RN_deriv M \<nu> x))) \<in> borel_measurable (M\<lparr>measure := \<nu>\<rparr>)"
6.240 by (auto intro!: RN_deriv[OF M ac] borel_measurable_log[OF _ `1 < b`])
6.241 @@ -233,9 +433,9 @@
6.242 proof -
6.243 interpret \<nu>: measure_space ?\<nu> by fact
6.244 have "KL_divergence b M \<nu> = \<integral>x. log b (real (RN_deriv N \<nu>' x)) \<partial>?\<nu>"
6.245 - by (simp cong: RN_deriv_cong \<nu>.integral_cong add: KL_divergence_def)
6.246 + by (simp cong: RN_deriv_cong \<nu>.integral_cong add: KL_divergence_def entropy_density_def)
6.247 also have "\<dots> = KL_divergence b N \<nu>'"
6.248 - by (auto intro!: \<nu>.integral_cong_measure[symmetric] simp: KL_divergence_def)
6.249 + by (auto intro!: \<nu>.integral_cong_measure[symmetric] simp: KL_divergence_def entropy_density_def comp_def)
6.250 finally show ?thesis .
6.251 qed
6.252
6.253 @@ -243,7 +443,7 @@
6.254 assumes v: "finite_measure_space (M\<lparr>measure := \<nu>\<rparr>)"
6.255 assumes ac: "absolutely_continuous \<nu>"
6.256 shows "KL_divergence b M \<nu> = (\<Sum>x\<in>space M. real (\<nu> {x}) * log b (real (\<nu> {x}) / real (\<mu> {x})))" (is "_ = ?sum")
6.257 -proof (simp add: KL_divergence_def finite_measure_space.integral_finite_singleton[OF v])
6.258 +proof (simp add: KL_divergence_def finite_measure_space.integral_finite_singleton[OF v] entropy_density_def)
6.259 interpret v: finite_measure_space "M\<lparr>measure := \<nu>\<rparr>" by fact
6.260 have ms: "measure_space (M\<lparr>measure := \<nu>\<rparr>)" by default
6.261 show "(\<Sum>x \<in> space M. log b (real (RN_deriv M \<nu> x)) * real (\<nu> {x})) = ?sum"
6.262 @@ -257,27 +457,10 @@
6.263 and "1 < b"
6.264 shows "0 \<le> KL_divergence b M \<nu>"
6.265 proof -
6.266 + interpret information_space M by default fact
6.267 interpret v: finite_prob_space "M\<lparr>measure := \<nu>\<rparr>" by fact
6.268 - have ms: "finite_measure_space (M\<lparr>measure := \<nu>\<rparr>)" by default
6.269 -
6.270 - have "- (KL_divergence b M \<nu>) \<le> log b (\<Sum>x\<in>space M. real (\<mu> {x}))"
6.271 - proof (subst KL_divergence_eq_finite[OF ms ac], safe intro!: log_setsum_divide not_empty)
6.272 - show "finite (space M)" using finite_space by simp
6.273 - show "1 < b" by fact
6.274 - show "(\<Sum>x\<in>space M. real (\<nu> {x})) = 1"
6.275 - using v.finite_sum_over_space_eq_1 by (simp add: v.\<mu>'_def)
6.276 -
6.277 - fix x assume "x \<in> space M"
6.278 - then have x: "{x} \<in> sets M" unfolding sets_eq_Pow by auto
6.279 - { assume "0 < real (\<nu> {x})"
6.280 - then have "\<nu> {x} \<noteq> 0" by auto
6.281 - then have "\<mu> {x} \<noteq> 0"
6.282 - using ac[unfolded absolutely_continuous_def, THEN bspec, of "{x}"] x by auto
6.283 - thus "0 < real (\<mu> {x})" using real_measure[OF x] by auto }
6.284 - show "0 \<le> real (\<mu> {x})" "0 \<le> real (\<nu> {x})"
6.285 - using real_measure[OF x] v.real_measure[of "{x}"] x by auto
6.286 - qed
6.287 - thus "0 \<le> KL_divergence b M \<nu>" using finite_sum_over_space_eq_1 by (simp add: \<mu>'_def)
6.288 + have ps: "prob_space (M\<lparr>measure := \<nu>\<rparr>)" by default
6.289 + from KL_ge_0[OF this ac v.integral_finite_singleton(1)] show ?thesis .
6.290 qed
6.291
6.292 subsection {* Mutual Information *}
6.293 @@ -287,6 +470,163 @@
6.294 KL_divergence b (S\<lparr>measure := extreal\<circ>distribution X\<rparr> \<Otimes>\<^isub>M T\<lparr>measure := extreal\<circ>distribution Y\<rparr>)
6.295 (extreal\<circ>joint_distribution X Y)"
6.296
6.297 +lemma (in information_space)
6.298 + fixes S T X Y
6.299 + defines "P \<equiv> S\<lparr>measure := extreal\<circ>distribution X\<rparr> \<Otimes>\<^isub>M T\<lparr>measure := extreal\<circ>distribution Y\<rparr>"
6.300 + shows "indep_var S X T Y \<longleftrightarrow>
6.301 + (random_variable S X \<and> random_variable T Y \<and>
6.302 + measure_space.absolutely_continuous P (extreal\<circ>joint_distribution X Y) \<and>
6.303 + integrable (P\<lparr>measure := (extreal\<circ>joint_distribution X Y)\<rparr>)
6.304 + (entropy_density b P (extreal\<circ>joint_distribution X Y)) \<and>
6.305 + mutual_information b S T X Y = 0)"
6.306 +proof safe
6.307 + assume indep: "indep_var S X T Y"
6.308 + then have "random_variable S X" "random_variable T Y"
6.309 + by (blast dest: indep_var_rv1 indep_var_rv2)+
6.310 + then show "sigma_algebra S" "X \<in> measurable M S" "sigma_algebra T" "Y \<in> measurable M T"
6.311 + by blast+
6.312 +
6.313 + interpret X: prob_space "S\<lparr>measure := extreal\<circ>distribution X\<rparr>"
6.314 + by (rule distribution_prob_space) fact
6.315 + interpret Y: prob_space "T\<lparr>measure := extreal\<circ>distribution Y\<rparr>"
6.316 + by (rule distribution_prob_space) fact
6.317 + interpret XY: pair_prob_space "S\<lparr>measure := extreal\<circ>distribution X\<rparr>" "T\<lparr>measure := extreal\<circ>distribution Y\<rparr>" by default
6.318 + interpret XY: information_space XY.P b by default (rule b_gt_1)
6.319 +
6.320 + let ?J = "XY.P\<lparr> measure := (extreal\<circ>joint_distribution X Y) \<rparr>"
6.321 + { fix A assume "A \<in> sets XY.P"
6.322 + then have "extreal (joint_distribution X Y A) = XY.\<mu> A"
6.323 + using indep_var_distributionD[OF indep]
6.324 + by (simp add: XY.P.finite_measure_eq) }
6.325 + note j_eq = this
6.326 +
6.327 + interpret J: prob_space ?J
6.328 + using j_eq by (intro XY.prob_space_cong) auto
6.329 +
6.330 + have ac: "XY.absolutely_continuous (extreal\<circ>joint_distribution X Y)"
6.331 + by (simp add: XY.absolutely_continuous_def j_eq)
6.332 + then show "measure_space.absolutely_continuous P (extreal\<circ>joint_distribution X Y)"
6.333 + unfolding P_def .
6.334 +
6.335 + have ed: "entropy_density b XY.P (extreal\<circ>joint_distribution X Y) \<in> borel_measurable XY.P"
6.336 + by (rule XY.measurable_entropy_density) (default | fact)+
6.337 +
6.338 + have "AE x in XY.P. 1 = RN_deriv XY.P (extreal\<circ>joint_distribution X Y) x"
6.339 + proof (rule XY.RN_deriv_unique[OF _ ac])
6.340 + show "measure_space ?J" by default
6.341 + fix A assume "A \<in> sets XY.P"
6.342 + then show "(extreal\<circ>joint_distribution X Y) A = (\<integral>\<^isup>+ x. 1 * indicator A x \<partial>XY.P)"
6.343 + by (simp add: j_eq)
6.344 + qed (insert XY.measurable_const[of 1 borel], auto)
6.345 + then have ae_XY: "AE x in XY.P. entropy_density b XY.P (extreal\<circ>joint_distribution X Y) x = 0"
6.346 + by (elim XY.AE_mp) (simp add: entropy_density_def)
6.347 + have ae_J: "AE x in ?J. entropy_density b XY.P (extreal\<circ>joint_distribution X Y) x = 0"
6.348 + proof (rule XY.absolutely_continuous_AE)
6.349 + show "measure_space ?J" by default
6.350 + show "XY.absolutely_continuous (measure ?J)"
6.351 + using ac by simp
6.352 + qed (insert ae_XY, simp_all)
6.353 + then show "integrable (P\<lparr>measure := (extreal\<circ>joint_distribution X Y)\<rparr>)
6.354 + (entropy_density b P (extreal\<circ>joint_distribution X Y))"
6.355 + unfolding P_def
6.356 + using ed XY.measurable_const[of 0 borel]
6.357 + by (subst J.integrable_cong_AE) auto
6.358 +
6.359 + show "mutual_information b S T X Y = 0"
6.360 + unfolding mutual_information_def KL_divergence_def P_def
6.361 + by (subst J.integral_cong_AE[OF ae_J]) simp
6.362 +next
6.363 + assume "sigma_algebra S" "X \<in> measurable M S" "sigma_algebra T" "Y \<in> measurable M T"
6.364 + then have rvs: "random_variable S X" "random_variable T Y" by blast+
6.365 +
6.366 + interpret X: prob_space "S\<lparr>measure := extreal\<circ>distribution X\<rparr>"
6.367 + by (rule distribution_prob_space) fact
6.368 + interpret Y: prob_space "T\<lparr>measure := extreal\<circ>distribution Y\<rparr>"
6.369 + by (rule distribution_prob_space) fact
6.370 + interpret XY: pair_prob_space "S\<lparr>measure := extreal\<circ>distribution X\<rparr>" "T\<lparr>measure := extreal\<circ>distribution Y\<rparr>" by default
6.371 + interpret XY: information_space XY.P b by default (rule b_gt_1)
6.372 +
6.373 + let ?J = "XY.P\<lparr> measure := (extreal\<circ>joint_distribution X Y) \<rparr>"
6.374 + interpret J: prob_space ?J
6.375 + using rvs by (intro joint_distribution_prob_space) auto
6.376 +
6.377 + assume ac: "measure_space.absolutely_continuous P (extreal\<circ>joint_distribution X Y)"
6.378 + assume int: "integrable (P\<lparr>measure := (extreal\<circ>joint_distribution X Y)\<rparr>)
6.379 + (entropy_density b P (extreal\<circ>joint_distribution X Y))"
6.380 + assume I_eq_0: "mutual_information b S T X Y = 0"
6.381 +
6.382 + have eq: "\<forall>A\<in>sets XY.P. (extreal \<circ> joint_distribution X Y) A = XY.\<mu> A"
6.383 + proof (rule XY.KL_eq_0_imp)
6.384 + show "prob_space ?J" by default
6.385 + show "XY.absolutely_continuous (extreal\<circ>joint_distribution X Y)"
6.386 + using ac by (simp add: P_def)
6.387 + show "integrable ?J (entropy_density b XY.P (extreal\<circ>joint_distribution X Y))"
6.388 + using int by (simp add: P_def)
6.389 + show "KL_divergence b XY.P (extreal\<circ>joint_distribution X Y) = 0"
6.390 + using I_eq_0 unfolding mutual_information_def by (simp add: P_def)
6.391 + qed
6.392 +
6.393 + { fix S X assume "sigma_algebra S"
6.394 + interpret S: sigma_algebra S by fact
6.395 + have "Int_stable \<lparr>space = space M, sets = {X -` A \<inter> space M |A. A \<in> sets S}\<rparr>"
6.396 + proof (safe intro!: Int_stableI)
6.397 + fix A B assume "A \<in> sets S" "B \<in> sets S"
6.398 + then show "\<exists>C. (X -` A \<inter> space M) \<inter> (X -` B \<inter> space M) = (X -` C \<inter> space M) \<and> C \<in> sets S"
6.399 + by (intro exI[of _ "A \<inter> B"]) auto
6.400 + qed }
6.401 + note Int_stable = this
6.402 +
6.403 + show "indep_var S X T Y" unfolding indep_var_eq
6.404 + proof (intro conjI indep_set_sigma_sets Int_stable)
6.405 + show "indep_set {X -` A \<inter> space M |A. A \<in> sets S} {Y -` A \<inter> space M |A. A \<in> sets T}"
6.406 + proof (safe intro!: indep_setI)
6.407 + { fix A assume "A \<in> sets S" then show "X -` A \<inter> space M \<in> sets M"
6.408 + using `X \<in> measurable M S` by (auto intro: measurable_sets) }
6.409 + { fix A assume "A \<in> sets T" then show "Y -` A \<inter> space M \<in> sets M"
6.410 + using `Y \<in> measurable M T` by (auto intro: measurable_sets) }
6.411 + next
6.412 + fix A B assume ab: "A \<in> sets S" "B \<in> sets T"
6.413 + have "extreal (prob ((X -` A \<inter> space M) \<inter> (Y -` B \<inter> space M))) =
6.414 + extreal (joint_distribution X Y (A \<times> B))"
6.415 + unfolding distribution_def
6.416 + by (intro arg_cong[where f="\<lambda>C. extreal (prob C)"]) auto
6.417 + also have "\<dots> = XY.\<mu> (A \<times> B)"
6.418 + using ab eq by (auto simp: XY.finite_measure_eq)
6.419 + also have "\<dots> = extreal (distribution X A) * extreal (distribution Y B)"
6.420 + using ab by (simp add: XY.pair_measure_times)
6.421 + finally show "prob ((X -` A \<inter> space M) \<inter> (Y -` B \<inter> space M)) =
6.422 + prob (X -` A \<inter> space M) * prob (Y -` B \<inter> space M)"
6.423 + unfolding distribution_def by simp
6.424 + qed
6.425 + qed fact+
6.426 +qed
6.427 +
6.428 +lemma (in information_space) mutual_information_commute_generic:
6.429 + assumes X: "random_variable S X" and Y: "random_variable T Y"
6.430 + assumes ac: "measure_space.absolutely_continuous
6.431 + (S\<lparr>measure := extreal\<circ>distribution X\<rparr> \<Otimes>\<^isub>M T\<lparr>measure := extreal\<circ>distribution Y\<rparr>) (extreal\<circ>joint_distribution X Y)"
6.432 + shows "mutual_information b S T X Y = mutual_information b T S Y X"
6.433 +proof -
6.434 + let ?S = "S\<lparr>measure := extreal\<circ>distribution X\<rparr>" and ?T = "T\<lparr>measure := extreal\<circ>distribution Y\<rparr>"
6.435 + interpret S: prob_space ?S using X by (rule distribution_prob_space)
6.436 + interpret T: prob_space ?T using Y by (rule distribution_prob_space)
6.437 + interpret P: pair_prob_space ?S ?T ..
6.438 + interpret Q: pair_prob_space ?T ?S ..
6.439 + show ?thesis
6.440 + unfolding mutual_information_def
6.441 + proof (intro Q.KL_divergence_vimage[OF Q.measure_preserving_swap _ _ _ _ ac b_gt_1])
6.442 + show "(\<lambda>(x,y). (y,x)) \<in> measure_preserving
6.443 + (P.P \<lparr> measure := extreal\<circ>joint_distribution X Y\<rparr>) (Q.P \<lparr> measure := extreal\<circ>joint_distribution Y X\<rparr>)"
6.444 + using X Y unfolding measurable_def
6.445 + unfolding measure_preserving_def using P.pair_sigma_algebra_swap_measurable
6.446 + by (auto simp add: space_pair_measure distribution_def intro!: arg_cong[where f=\<mu>'])
6.447 + have "prob_space (P.P\<lparr> measure := extreal\<circ>joint_distribution X Y\<rparr>)"
6.448 + using X Y by (auto intro!: distribution_prob_space random_variable_pairI)
6.449 + then show "measure_space (P.P\<lparr> measure := extreal\<circ>joint_distribution X Y\<rparr>)"
6.450 + unfolding prob_space_def by simp
6.451 + qed auto
6.452 +qed
6.453 +
6.454 definition (in prob_space)
6.455 "entropy b s X = mutual_information b s s X X"
6.456
6.457 @@ -356,32 +696,6 @@
6.458 unfolding mutual_information_def .
6.459 qed
6.460
6.461 -lemma (in information_space) mutual_information_commute_generic:
6.462 - assumes X: "random_variable S X" and Y: "random_variable T Y"
6.463 - assumes ac: "measure_space.absolutely_continuous
6.464 - (S\<lparr>measure := extreal\<circ>distribution X\<rparr> \<Otimes>\<^isub>M T\<lparr>measure := extreal\<circ>distribution Y\<rparr>) (extreal\<circ>joint_distribution X Y)"
6.465 - shows "mutual_information b S T X Y = mutual_information b T S Y X"
6.466 -proof -
6.467 - let ?S = "S\<lparr>measure := extreal\<circ>distribution X\<rparr>" and ?T = "T\<lparr>measure := extreal\<circ>distribution Y\<rparr>"
6.468 - interpret S: prob_space ?S using X by (rule distribution_prob_space)
6.469 - interpret T: prob_space ?T using Y by (rule distribution_prob_space)
6.470 - interpret P: pair_prob_space ?S ?T ..
6.471 - interpret Q: pair_prob_space ?T ?S ..
6.472 - show ?thesis
6.473 - unfolding mutual_information_def
6.474 - proof (intro Q.KL_divergence_vimage[OF Q.measure_preserving_swap _ _ _ _ ac b_gt_1])
6.475 - show "(\<lambda>(x,y). (y,x)) \<in> measure_preserving
6.476 - (P.P \<lparr> measure := extreal\<circ>joint_distribution X Y\<rparr>) (Q.P \<lparr> measure := extreal\<circ>joint_distribution Y X\<rparr>)"
6.477 - using X Y unfolding measurable_def
6.478 - unfolding measure_preserving_def using P.pair_sigma_algebra_swap_measurable
6.479 - by (auto simp add: space_pair_measure distribution_def intro!: arg_cong[where f=\<mu>'])
6.480 - have "prob_space (P.P\<lparr> measure := extreal\<circ>joint_distribution X Y\<rparr>)"
6.481 - using X Y by (auto intro!: distribution_prob_space random_variable_pairI)
6.482 - then show "measure_space (P.P\<lparr> measure := extreal\<circ>joint_distribution X Y\<rparr>)"
6.483 - unfolding prob_space_def by simp
6.484 - qed auto
6.485 -qed
6.486 -
6.487 lemma (in information_space) mutual_information_commute:
6.488 assumes X: "finite_random_variable S X" and Y: "finite_random_variable T Y"
6.489 shows "mutual_information b S T X Y = mutual_information b T S Y X"
7.1 --- a/src/HOL/Probability/Lebesgue_Integration.thy Thu Jun 09 11:57:39 2011 +0200
7.2 +++ b/src/HOL/Probability/Lebesgue_Integration.thy Thu Jun 09 14:24:34 2011 +0200
7.3 @@ -1712,6 +1712,12 @@
7.4 shows "integral\<^isup>L N f = integral\<^isup>L M f"
7.5 by (simp add: positive_integral_cong_measure[OF assms] lebesgue_integral_def)
7.6
7.7 +lemma (in measure_space) integrable_cong_measure:
7.8 + assumes "\<And>A. A \<in> sets M \<Longrightarrow> measure N A = \<mu> A" "sets N = sets M" "space N = space M"
7.9 + shows "integrable N f \<longleftrightarrow> integrable M f"
7.10 + using assms
7.11 + by (simp add: positive_integral_cong_measure[OF assms] integrable_def measurable_def)
7.12 +
7.13 lemma (in measure_space) integral_cong_AE:
7.14 assumes cong: "AE x. f x = g x"
7.15 shows "integral\<^isup>L M f = integral\<^isup>L M g"
7.16 @@ -1722,6 +1728,18 @@
7.17 unfolding *[THEN positive_integral_cong_AE] lebesgue_integral_def ..
7.18 qed
7.19
7.20 +lemma (in measure_space) integrable_cong_AE:
7.21 + assumes borel: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
7.22 + assumes "AE x. f x = g x"
7.23 + shows "integrable M f = integrable M g"
7.24 +proof -
7.25 + have "(\<integral>\<^isup>+ x. extreal (f x) \<partial>M) = (\<integral>\<^isup>+ x. extreal (g x) \<partial>M)"
7.26 + "(\<integral>\<^isup>+ x. extreal (- f x) \<partial>M) = (\<integral>\<^isup>+ x. extreal (- g x) \<partial>M)"
7.27 + using assms by (auto intro!: positive_integral_cong_AE)
7.28 + with assms show ?thesis
7.29 + by (auto simp: integrable_def)
7.30 +qed
7.31 +
7.32 lemma (in measure_space) integrable_cong:
7.33 "(\<And>x. x \<in> space M \<Longrightarrow> f x = g x) \<Longrightarrow> integrable M f \<longleftrightarrow> integrable M g"
7.34 by (simp cong: positive_integral_cong measurable_cong add: integrable_def)
7.35 @@ -1767,6 +1785,48 @@
7.36 by (auto simp: borel[THEN positive_integral_vimage[OF T]])
7.37 qed
7.38
7.39 +lemma (in measure_space) integral_translated_density:
7.40 + assumes f: "f \<in> borel_measurable M" "AE x. 0 \<le> f x"
7.41 + and g: "g \<in> borel_measurable M"
7.42 + and N: "space N = space M" "sets N = sets M"
7.43 + and density: "\<And>A. A \<in> sets M \<Longrightarrow> measure N A = (\<integral>\<^isup>+ x. f x * indicator A x \<partial>M)"
7.44 + (is "\<And>A. _ \<Longrightarrow> _ = ?d A")
7.45 + shows "integral\<^isup>L N g = (\<integral> x. f x * g x \<partial>M)" (is ?integral)
7.46 + and "integrable N g = integrable M (\<lambda>x. f x * g x)" (is ?integrable)
7.47 +proof -
7.48 + from f have ms: "measure_space (M\<lparr>measure := ?d\<rparr>)"
7.49 + by (intro measure_space_density[where u="\<lambda>x. extreal (f x)"]) auto
7.50 +
7.51 + from ms density N have "(\<integral>\<^isup>+ x. g x \<partial>N) = (\<integral>\<^isup>+ x. max 0 (extreal (g x)) \<partial>M\<lparr>measure := ?d\<rparr>)"
7.52 + unfolding positive_integral_max_0
7.53 + by (intro measure_space.positive_integral_cong_measure) auto
7.54 + also have "\<dots> = (\<integral>\<^isup>+ x. extreal (f x) * max 0 (extreal (g x)) \<partial>M)"
7.55 + using f g by (intro positive_integral_translated_density) auto
7.56 + also have "\<dots> = (\<integral>\<^isup>+ x. max 0 (extreal (f x * g x)) \<partial>M)"
7.57 + using f by (intro positive_integral_cong_AE)
7.58 + (auto simp: extreal_max_0 zero_le_mult_iff split: split_max)
7.59 + finally have pos: "(\<integral>\<^isup>+ x. g x \<partial>N) = (\<integral>\<^isup>+ x. f x * g x \<partial>M)"
7.60 + by (simp add: positive_integral_max_0)
7.61 +
7.62 + from ms density N have "(\<integral>\<^isup>+ x. - (g x) \<partial>N) = (\<integral>\<^isup>+ x. max 0 (extreal (- g x)) \<partial>M\<lparr>measure := ?d\<rparr>)"
7.63 + unfolding positive_integral_max_0
7.64 + by (intro measure_space.positive_integral_cong_measure) auto
7.65 + also have "\<dots> = (\<integral>\<^isup>+ x. extreal (f x) * max 0 (extreal (- g x)) \<partial>M)"
7.66 + using f g by (intro positive_integral_translated_density) auto
7.67 + also have "\<dots> = (\<integral>\<^isup>+ x. max 0 (extreal (- f x * g x)) \<partial>M)"
7.68 + using f by (intro positive_integral_cong_AE)
7.69 + (auto simp: extreal_max_0 mult_le_0_iff split: split_max)
7.70 + finally have neg: "(\<integral>\<^isup>+ x. - g x \<partial>N) = (\<integral>\<^isup>+ x. - (f x * g x) \<partial>M)"
7.71 + by (simp add: positive_integral_max_0)
7.72 +
7.73 + have g_N: "g \<in> borel_measurable N"
7.74 + using g N unfolding measurable_def by simp
7.75 +
7.76 + show ?integral ?integrable
7.77 + unfolding lebesgue_integral_def integrable_def
7.78 + using pos neg f g g_N by auto
7.79 +qed
7.80 +
7.81 lemma (in measure_space) integral_minus[intro, simp]:
7.82 assumes "integrable M f"
7.83 shows "integrable M (\<lambda>x. - f x)" "(\<integral>x. - f x \<partial>M) = - integral\<^isup>L M f"
7.84 @@ -2221,9 +2281,14 @@
7.85 by (simp add: \<mu>'_def lebesgue_integral_def positive_integral_const_If)
7.86 qed
7.87
7.88 +lemma indicator_less[simp]:
7.89 + "indicator A x \<le> (indicator B x::extreal) \<longleftrightarrow> (x \<in> A \<longrightarrow> x \<in> B)"
7.90 + by (simp add: indicator_def not_le)
7.91 +
7.92 lemma (in finite_measure) integral_less_AE:
7.93 assumes int: "integrable M X" "integrable M Y"
7.94 - assumes gt: "AE x. X x < Y x" and neq0: "\<mu> (space M) \<noteq> 0"
7.95 + assumes A: "\<mu> A \<noteq> 0" "A \<in> sets M" "AE x. x \<in> A \<longrightarrow> X x \<noteq> Y x"
7.96 + assumes gt: "AE x. X x \<le> Y x"
7.97 shows "integral\<^isup>L M X < integral\<^isup>L M Y"
7.98 proof -
7.99 have "integral\<^isup>L M X \<le> integral\<^isup>L M Y"
7.100 @@ -2231,24 +2296,30 @@
7.101 moreover
7.102 have "integral\<^isup>L M X \<noteq> integral\<^isup>L M Y"
7.103 proof
7.104 - from gt have "AE x. Y x - X x \<noteq> 0"
7.105 - by auto
7.106 - then have \<mu>: "\<mu> {x\<in>space M. Y x - X x \<noteq> 0} = \<mu> (space M)"
7.107 - using int
7.108 - by (intro AE_measure borel_measurable_neq) (auto simp add: integrable_def)
7.109 -
7.110 assume eq: "integral\<^isup>L M X = integral\<^isup>L M Y"
7.111 have "integral\<^isup>L M (\<lambda>x. \<bar>Y x - X x\<bar>) = integral\<^isup>L M (\<lambda>x. Y x - X x)"
7.112 using gt by (intro integral_cong_AE) auto
7.113 also have "\<dots> = 0"
7.114 using eq int by simp
7.115 - finally show False
7.116 - using \<mu> int neq0
7.117 - by (subst (asm) integral_0_iff) auto
7.118 + finally have "\<mu> {x \<in> space M. Y x - X x \<noteq> 0} = 0"
7.119 + using int by (simp add: integral_0_iff)
7.120 + moreover
7.121 + have "(\<integral>\<^isup>+x. indicator A x \<partial>M) \<le> (\<integral>\<^isup>+x. indicator {x \<in> space M. Y x - X x \<noteq> 0} x \<partial>M)"
7.122 + using A by (intro positive_integral_mono_AE) auto
7.123 + then have "\<mu> A \<le> \<mu> {x \<in> space M. Y x - X x \<noteq> 0}"
7.124 + using int A by (simp add: integrable_def)
7.125 + moreover note `\<mu> A \<noteq> 0` positive_measure[OF `A \<in> sets M`]
7.126 + ultimately show False by auto
7.127 qed
7.128 ultimately show ?thesis by auto
7.129 qed
7.130
7.131 +lemma (in finite_measure) integral_less_AE_space:
7.132 + assumes int: "integrable M X" "integrable M Y"
7.133 + assumes gt: "AE x. X x < Y x" "\<mu> (space M) \<noteq> 0"
7.134 + shows "integral\<^isup>L M X < integral\<^isup>L M Y"
7.135 + using gt by (intro integral_less_AE[OF int, where A="space M"]) auto
7.136 +
7.137 lemma (in measure_space) integral_dominated_convergence:
7.138 assumes u: "\<And>i. integrable M (u i)" and bound: "\<And>x j. x\<in>space M \<Longrightarrow> \<bar>u j x\<bar> \<le> w x"
7.139 and w: "integrable M w"
8.1 --- a/src/HOL/Probability/Probability_Measure.thy Thu Jun 09 11:57:39 2011 +0200
8.2 +++ b/src/HOL/Probability/Probability_Measure.thy Thu Jun 09 14:24:34 2011 +0200
8.3 @@ -28,6 +28,14 @@
8.4 abbreviation (in prob_space)
8.5 "joint_distribution X Y \<equiv> distribution (\<lambda>x. (X x, Y x))"
8.6
8.7 +lemma (in prob_space) prob_space_cong:
8.8 + assumes "\<And>A. A \<in> sets M \<Longrightarrow> measure N A = \<mu> A" "space N = space M" "sets N = sets M"
8.9 + shows "prob_space N"
8.10 +proof -
8.11 + interpret N: measure_space N by (intro measure_space_cong assms)
8.12 + show ?thesis by default (insert assms measure_space_1, simp)
8.13 +qed
8.14 +
8.15 lemma (in prob_space) distribution_cong:
8.16 assumes "\<And>x. x \<in> space M \<Longrightarrow> X x = Y x"
8.17 shows "distribution X = distribution Y"
8.18 @@ -54,15 +62,30 @@
8.19 lemma (in prob_space) distribution_positive[simp, intro]:
8.20 "0 \<le> distribution X A" unfolding distribution_def by auto
8.21
8.22 +lemma (in prob_space) not_zero_less_distribution[simp]:
8.23 + "(\<not> 0 < distribution X A) \<longleftrightarrow> distribution X A = 0"
8.24 + using distribution_positive[of X A] by arith
8.25 +
8.26 lemma (in prob_space) joint_distribution_remove[simp]:
8.27 "joint_distribution X X {(x, x)} = distribution X {x}"
8.28 unfolding distribution_def by (auto intro!: arg_cong[where f=\<mu>'])
8.29
8.30 +lemma (in prob_space) not_empty: "space M \<noteq> {}"
8.31 + using prob_space empty_measure' by auto
8.32 +
8.33 lemma (in prob_space) measure_le_1: "X \<in> sets M \<Longrightarrow> \<mu> X \<le> 1"
8.34 unfolding measure_space_1[symmetric]
8.35 using sets_into_space
8.36 by (intro measure_mono) auto
8.37
8.38 +lemma (in prob_space) AE_I_eq_1:
8.39 + assumes "\<mu> {x\<in>space M. P x} = 1" "{x\<in>space M. P x} \<in> sets M"
8.40 + shows "AE x. P x"
8.41 +proof (rule AE_I)
8.42 + show "\<mu> (space M - {x \<in> space M. P x}) = 0"
8.43 + using assms measure_space_1 by (simp add: measure_compl)
8.44 +qed (insert assms, auto)
8.45 +
8.46 lemma (in prob_space) distribution_1:
8.47 "distribution X A \<le> 1"
8.48 unfolding distribution_def by simp
8.49 @@ -245,6 +268,146 @@
8.50 using finite_measure_eq[of "X -` A \<inter> space M"]
8.51 by (auto simp: measurable_sets distribution_def)
8.52
8.53 +lemma (in prob_space) expectation_less:
8.54 + assumes [simp]: "integrable M X"
8.55 + assumes gt: "\<forall>x\<in>space M. X x < b"
8.56 + shows "expectation X < b"
8.57 +proof -
8.58 + have "expectation X < expectation (\<lambda>x. b)"
8.59 + using gt measure_space_1
8.60 + by (intro integral_less_AE_space) auto
8.61 + then show ?thesis using prob_space by simp
8.62 +qed
8.63 +
8.64 +lemma (in prob_space) expectation_greater:
8.65 + assumes [simp]: "integrable M X"
8.66 + assumes gt: "\<forall>x\<in>space M. a < X x"
8.67 + shows "a < expectation X"
8.68 +proof -
8.69 + have "expectation (\<lambda>x. a) < expectation X"
8.70 + using gt measure_space_1
8.71 + by (intro integral_less_AE_space) auto
8.72 + then show ?thesis using prob_space by simp
8.73 +qed
8.74 +
8.75 +lemma convex_le_Inf_differential:
8.76 + fixes f :: "real \<Rightarrow> real"
8.77 + assumes "convex_on I f"
8.78 + assumes "x \<in> interior I" "y \<in> I"
8.79 + shows "f y \<ge> f x + Inf ((\<lambda>t. (f x - f t) / (x - t)) ` ({x<..} \<inter> I)) * (y - x)"
8.80 + (is "_ \<ge> _ + Inf (?F x) * (y - x)")
8.81 +proof -
8.82 + show ?thesis
8.83 + proof (cases rule: linorder_cases)
8.84 + assume "x < y"
8.85 + moreover
8.86 + have "open (interior I)" by auto
8.87 + from openE[OF this `x \<in> interior I`] guess e . note e = this
8.88 + moreover def t \<equiv> "min (x + e / 2) ((x + y) / 2)"
8.89 + ultimately have "x < t" "t < y" "t \<in> ball x e"
8.90 + by (auto simp: mem_ball dist_real_def field_simps split: split_min)
8.91 + with `x \<in> interior I` e interior_subset[of I] have "t \<in> I" "x \<in> I" by auto
8.92 +
8.93 + have "open (interior I)" by auto
8.94 + from openE[OF this `x \<in> interior I`] guess e .
8.95 + moreover def K \<equiv> "x - e / 2"
8.96 + with `0 < e` have "K \<in> ball x e" "K < x" by (auto simp: mem_ball dist_real_def)
8.97 + ultimately have "K \<in> I" "K < x" "x \<in> I"
8.98 + using interior_subset[of I] `x \<in> interior I` by auto
8.99 +
8.100 + have "Inf (?F x) \<le> (f x - f y) / (x - y)"
8.101 + proof (rule Inf_lower2)
8.102 + show "(f x - f t) / (x - t) \<in> ?F x"
8.103 + using `t \<in> I` `x < t` by auto
8.104 + show "(f x - f t) / (x - t) \<le> (f x - f y) / (x - y)"
8.105 + using `convex_on I f` `x \<in> I` `y \<in> I` `x < t` `t < y` by (rule convex_on_diff)
8.106 + next
8.107 + fix y assume "y \<in> ?F x"
8.108 + with order_trans[OF convex_on_diff[OF `convex_on I f` `K \<in> I` _ `K < x` _]]
8.109 + show "(f K - f x) / (K - x) \<le> y" by auto
8.110 + qed
8.111 + then show ?thesis
8.112 + using `x < y` by (simp add: field_simps)
8.113 + next
8.114 + assume "y < x"
8.115 + moreover
8.116 + have "open (interior I)" by auto
8.117 + from openE[OF this `x \<in> interior I`] guess e . note e = this
8.118 + moreover def t \<equiv> "x + e / 2"
8.119 + ultimately have "x < t" "t \<in> ball x e"
8.120 + by (auto simp: mem_ball dist_real_def field_simps)
8.121 + with `x \<in> interior I` e interior_subset[of I] have "t \<in> I" "x \<in> I" by auto
8.122 +
8.123 + have "(f x - f y) / (x - y) \<le> Inf (?F x)"
8.124 + proof (rule Inf_greatest)
8.125 + have "(f x - f y) / (x - y) = (f y - f x) / (y - x)"
8.126 + using `y < x` by (auto simp: field_simps)
8.127 + also
8.128 + fix z assume "z \<in> ?F x"
8.129 + with order_trans[OF convex_on_diff[OF `convex_on I f` `y \<in> I` _ `y < x`]]
8.130 + have "(f y - f x) / (y - x) \<le> z" by auto
8.131 + finally show "(f x - f y) / (x - y) \<le> z" .
8.132 + next
8.133 + have "open (interior I)" by auto
8.134 + from openE[OF this `x \<in> interior I`] guess e . note e = this
8.135 + then have "x + e / 2 \<in> ball x e" by (auto simp: mem_ball dist_real_def)
8.136 + with e interior_subset[of I] have "x + e / 2 \<in> {x<..} \<inter> I" by auto
8.137 + then show "?F x \<noteq> {}" by blast
8.138 + qed
8.139 + then show ?thesis
8.140 + using `y < x` by (simp add: field_simps)
8.141 + qed simp
8.142 +qed
8.143 +
8.144 +lemma (in prob_space) jensens_inequality:
8.145 + fixes a b :: real
8.146 + assumes X: "integrable M X" "X ` space M \<subseteq> I"
8.147 + assumes I: "I = {a <..< b} \<or> I = {a <..} \<or> I = {..< b} \<or> I = UNIV"
8.148 + assumes q: "integrable M (\<lambda>x. q (X x))" "convex_on I q"
8.149 + shows "q (expectation X) \<le> expectation (\<lambda>x. q (X x))"
8.150 +proof -
8.151 + let "?F x" = "Inf ((\<lambda>t. (q x - q t) / (x - t)) ` ({x<..} \<inter> I))"
8.152 + from not_empty X(2) have "I \<noteq> {}" by auto
8.153 +
8.154 + from I have "open I" by auto
8.155 +
8.156 + note I
8.157 + moreover
8.158 + { assume "I \<subseteq> {a <..}"
8.159 + with X have "a < expectation X"
8.160 + by (intro expectation_greater) auto }
8.161 + moreover
8.162 + { assume "I \<subseteq> {..< b}"
8.163 + with X have "expectation X < b"
8.164 + by (intro expectation_less) auto }
8.165 + ultimately have "expectation X \<in> I"
8.166 + by (elim disjE) (auto simp: subset_eq)
8.167 + moreover
8.168 + { fix y assume y: "y \<in> I"
8.169 + with q(2) `open I` have "Sup ((\<lambda>x. q x + ?F x * (y - x)) ` I) = q y"
8.170 + by (auto intro!: Sup_eq_maximum convex_le_Inf_differential image_eqI[OF _ y] simp: interior_open) }
8.171 + ultimately have "q (expectation X) = Sup ((\<lambda>x. q x + ?F x * (expectation X - x)) ` I)"
8.172 + by simp
8.173 + also have "\<dots> \<le> expectation (\<lambda>w. q (X w))"
8.174 + proof (rule Sup_least)
8.175 + show "(\<lambda>x. q x + ?F x * (expectation X - x)) ` I \<noteq> {}"
8.176 + using `I \<noteq> {}` by auto
8.177 + next
8.178 + fix k assume "k \<in> (\<lambda>x. q x + ?F x * (expectation X - x)) ` I"
8.179 + then guess x .. note x = this
8.180 + have "q x + ?F x * (expectation X - x) = expectation (\<lambda>w. q x + ?F x * (X w - x))"
8.181 + using prob_space
8.182 + by (simp add: integral_add integral_cmult integral_diff lebesgue_integral_const X)
8.183 + also have "\<dots> \<le> expectation (\<lambda>w. q (X w))"
8.184 + using `x \<in> I` `open I` X(2)
8.185 + by (intro integral_mono integral_add integral_cmult integral_diff
8.186 + lebesgue_integral_const X q convex_le_Inf_differential)
8.187 + (auto simp: interior_open)
8.188 + finally show "k \<le> expectation (\<lambda>w. q (X w))" using x by auto
8.189 + qed
8.190 + finally show "q (expectation X) \<le> expectation (\<lambda>x. q (X x))" .
8.191 +qed
8.192 +
8.193 lemma (in prob_space) distribution_eq_translated_integral:
8.194 assumes "random_variable S X" "A \<in> sets S"
8.195 shows "distribution X A = integral\<^isup>P (S\<lparr>measure := extreal \<circ> distribution X\<rparr>) (indicator A)"
8.196 @@ -722,9 +885,6 @@
8.197 unfolding finite_prob_space_def finite_measure_space_def prob_space_def prob_space_axioms_def
8.198 by auto
8.199
8.200 -lemma (in prob_space) not_empty: "space M \<noteq> {}"
8.201 - using prob_space empty_measure' by auto
8.202 -
8.203 lemma (in finite_prob_space) sum_over_space_eq_1: "(\<Sum>x\<in>space M. \<mu> {x}) = 1"
8.204 using measure_space_1 sum_over_space by simp
8.205
8.206 @@ -829,7 +989,7 @@
8.207 also have "\<dots> = real_of_nat (card (space M)) * prob {x}" by simp
8.208 finally have one: "1 = real (card (space M)) * prob {x}"
8.209 using real_eq_of_nat by auto
8.210 - hence two: "real (card (space M)) \<noteq> 0" by fastsimp
8.211 + hence two: "real (card (space M)) \<noteq> 0" by fastsimp
8.212 from one have three: "prob {x} \<noteq> 0" by fastsimp
8.213 thus ?thesis using one two three divide_cancel_right
8.214 by (auto simp:field_simps)
9.1 --- a/src/HOL/Probability/Radon_Nikodym.thy Thu Jun 09 11:57:39 2011 +0200
9.2 +++ b/src/HOL/Probability/Radon_Nikodym.thy Thu Jun 09 14:24:34 2011 +0200
9.3 @@ -1311,6 +1311,59 @@
9.4 by (auto simp: RN_deriv_positive_integral[OF ms \<nu>(2)])
9.5 qed
9.6
9.7 +lemma (in sigma_finite_measure) real_RN_deriv:
9.8 + assumes "finite_measure (M\<lparr>measure := \<nu>\<rparr>)" (is "finite_measure ?\<nu>")
9.9 + assumes ac: "absolutely_continuous \<nu>"
9.10 + obtains D where "D \<in> borel_measurable M"
9.11 + and "AE x. RN_deriv M \<nu> x = extreal (D x)"
9.12 + and "AE x in M\<lparr>measure := \<nu>\<rparr>. 0 < D x"
9.13 + and "\<And>x. 0 \<le> D x"
9.14 +proof
9.15 + interpret \<nu>: finite_measure ?\<nu> by fact
9.16 + have ms: "measure_space ?\<nu>" by default
9.17 + note RN = RN_deriv[OF ms ac]
9.18 +
9.19 + let ?RN = "\<lambda>t. {x \<in> space M. RN_deriv M \<nu> x = t}"
9.20 +
9.21 + show "(\<lambda>x. real (RN_deriv M \<nu> x)) \<in> borel_measurable M"
9.22 + using RN by auto
9.23 +
9.24 + have "\<nu> (?RN \<infinity>) = (\<integral>\<^isup>+ x. RN_deriv M \<nu> x * indicator (?RN \<infinity>) x \<partial>M)"
9.25 + using RN by auto
9.26 + also have "\<dots> = (\<integral>\<^isup>+ x. \<infinity> * indicator (?RN \<infinity>) x \<partial>M)"
9.27 + by (intro positive_integral_cong) (auto simp: indicator_def)
9.28 + also have "\<dots> = \<infinity> * \<mu> (?RN \<infinity>)"
9.29 + using RN by (intro positive_integral_cmult_indicator) auto
9.30 + finally have eq: "\<nu> (?RN \<infinity>) = \<infinity> * \<mu> (?RN \<infinity>)" .
9.31 + moreover
9.32 + have "\<mu> (?RN \<infinity>) = 0"
9.33 + proof (rule ccontr)
9.34 + assume "\<mu> {x \<in> space M. RN_deriv M \<nu> x = \<infinity>} \<noteq> 0"
9.35 + moreover from RN have "0 \<le> \<mu> {x \<in> space M. RN_deriv M \<nu> x = \<infinity>}" by auto
9.36 + ultimately have "0 < \<mu> {x \<in> space M. RN_deriv M \<nu> x = \<infinity>}" by auto
9.37 + with eq have "\<nu> (?RN \<infinity>) = \<infinity>" by simp
9.38 + with \<nu>.finite_measure[of "?RN \<infinity>"] RN show False by auto
9.39 + qed
9.40 + ultimately have "AE x. RN_deriv M \<nu> x < \<infinity>"
9.41 + using RN by (intro AE_iff_measurable[THEN iffD2]) auto
9.42 + then show "AE x. RN_deriv M \<nu> x = extreal (real (RN_deriv M \<nu> x))"
9.43 + using RN(3) by (auto simp: extreal_real)
9.44 + then have eq: "AE x in (M\<lparr>measure := \<nu>\<rparr>) . RN_deriv M \<nu> x = extreal (real (RN_deriv M \<nu> x))"
9.45 + using ac absolutely_continuous_AE[OF ms] by auto
9.46 +
9.47 + show "\<And>x. 0 \<le> real (RN_deriv M \<nu> x)"
9.48 + using RN by (auto intro: real_of_extreal_pos)
9.49 +
9.50 + have "\<nu> (?RN 0) = (\<integral>\<^isup>+ x. RN_deriv M \<nu> x * indicator (?RN 0) x \<partial>M)"
9.51 + using RN by auto
9.52 + also have "\<dots> = (\<integral>\<^isup>+ x. 0 \<partial>M)"
9.53 + by (intro positive_integral_cong) (auto simp: indicator_def)
9.54 + finally have "AE x in (M\<lparr>measure := \<nu>\<rparr>). RN_deriv M \<nu> x \<noteq> 0"
9.55 + using RN by (intro \<nu>.AE_iff_measurable[THEN iffD2]) auto
9.56 + with RN(3) eq show "AE x in (M\<lparr>measure := \<nu>\<rparr>). 0 < real (RN_deriv M \<nu> x)"
9.57 + by (auto simp: zero_less_real_of_extreal le_less)
9.58 +qed
9.59 +
9.60 lemma (in sigma_finite_measure) RN_deriv_singleton:
9.61 assumes "measure_space (M\<lparr>measure := \<nu>\<rparr>)"
9.62 and ac: "absolutely_continuous \<nu>"
10.1 --- a/src/HOL/Quickcheck_Narrowing.thy Thu Jun 09 11:57:39 2011 +0200
10.2 +++ b/src/HOL/Quickcheck_Narrowing.thy Thu Jun 09 14:24:34 2011 +0200
10.3 @@ -26,7 +26,7 @@
10.4
10.5 code_reserved Haskell_Quickcheck Typerep
10.6
10.7 -subsubsection {* Type @{text "code_int"} for Haskell_Quickcheck's Int type *}
10.8 +subsubsection {* Type @{text "code_int"} for Haskell Quickcheck's Int type *}
10.9
10.10 typedef (open) code_int = "UNIV \<Colon> int set"
10.11 morphisms int_of of_int by rule
10.12 @@ -218,7 +218,7 @@
10.13 datatype narrowing_term = Var "code_int list" narrowing_type | Ctr code_int "narrowing_term list"
10.14 datatype 'a cons = C narrowing_type "(narrowing_term list => 'a) list"
10.15
10.16 -subsubsection {* From narrowing's deep representation of terms to Code_Evaluation's terms *}
10.17 +subsubsection {* From narrowing's deep representation of terms to @{theory Code_Evaluation}'s terms *}
10.18
10.19 class partial_term_of = typerep +
10.20 fixes partial_term_of :: "'a itself => narrowing_term => Code_Evaluation.term"
11.1 --- a/src/HOL/Transcendental.thy Thu Jun 09 11:57:39 2011 +0200
11.2 +++ b/src/HOL/Transcendental.thy Thu Jun 09 14:24:34 2011 +0200
11.3 @@ -1366,7 +1366,7 @@
11.4
11.5 declare
11.6 DERIV_exp[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
11.7 - DERIV_ln[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
11.8 + DERIV_ln_divide[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
11.9 DERIV_sin[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
11.10 DERIV_cos[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
11.11