merged
authorhoelzl
Thu Jun 09 14:24:34 2011 +0200 (2011-06-09)
changeset 433422929f96d3ae7
parent 43334 9970a4580d13
parent 43341 acdac535c7fa
child 43344 b017cfb10df4
merged
     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