jensens inequality
authorhoelzl
Thu Jun 09 13:55:11 2011 +0200 (2011-06-09)
changeset 433399ba256ad6781
parent 43338 a150d16bf77c
child 43340 60e181c4eae4
jensens inequality
src/HOL/Probability/Lebesgue_Integration.thy
src/HOL/Probability/Probability_Measure.thy
     1.1 --- a/src/HOL/Probability/Lebesgue_Integration.thy	Thu Jun 09 11:50:16 2011 +0200
     1.2 +++ b/src/HOL/Probability/Lebesgue_Integration.thy	Thu Jun 09 13:55:11 2011 +0200
     1.3 @@ -1712,6 +1712,12 @@
     1.4    shows "integral\<^isup>L N f = integral\<^isup>L M f"
     1.5    by (simp add: positive_integral_cong_measure[OF assms] lebesgue_integral_def)
     1.6  
     1.7 +lemma (in measure_space) integrable_cong_measure:
     1.8 +  assumes "\<And>A. A \<in> sets M \<Longrightarrow> measure N A = \<mu> A" "sets N = sets M" "space N = space M"
     1.9 +  shows "integrable N f \<longleftrightarrow> integrable M f"
    1.10 +  using assms
    1.11 +  by (simp add: positive_integral_cong_measure[OF assms] integrable_def measurable_def)
    1.12 +
    1.13  lemma (in measure_space) integral_cong_AE:
    1.14    assumes cong: "AE x. f x = g x"
    1.15    shows "integral\<^isup>L M f = integral\<^isup>L M g"
    1.16 @@ -1722,6 +1728,18 @@
    1.17      unfolding *[THEN positive_integral_cong_AE] lebesgue_integral_def ..
    1.18  qed
    1.19  
    1.20 +lemma (in measure_space) integrable_cong_AE:
    1.21 +  assumes borel: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
    1.22 +  assumes "AE x. f x = g x"
    1.23 +  shows "integrable M f = integrable M g"
    1.24 +proof -
    1.25 +  have "(\<integral>\<^isup>+ x. extreal (f x) \<partial>M) = (\<integral>\<^isup>+ x. extreal (g x) \<partial>M)"
    1.26 +    "(\<integral>\<^isup>+ x. extreal (- f x) \<partial>M) = (\<integral>\<^isup>+ x. extreal (- g x) \<partial>M)"
    1.27 +    using assms by (auto intro!: positive_integral_cong_AE)
    1.28 +  with assms show ?thesis
    1.29 +    by (auto simp: integrable_def)
    1.30 +qed
    1.31 +
    1.32  lemma (in measure_space) integrable_cong:
    1.33    "(\<And>x. x \<in> space M \<Longrightarrow> f x = g x) \<Longrightarrow> integrable M f \<longleftrightarrow> integrable M g"
    1.34    by (simp cong: positive_integral_cong measurable_cong add: integrable_def)
    1.35 @@ -1767,6 +1785,48 @@
    1.36      by (auto simp: borel[THEN positive_integral_vimage[OF T]])
    1.37  qed
    1.38  
    1.39 +lemma (in measure_space) integral_translated_density:
    1.40 +  assumes f: "f \<in> borel_measurable M" "AE x. 0 \<le> f x"
    1.41 +    and g: "g \<in> borel_measurable M"
    1.42 +    and N: "space N = space M" "sets N = sets M"
    1.43 +    and density: "\<And>A. A \<in> sets M \<Longrightarrow> measure N A = (\<integral>\<^isup>+ x. f x * indicator A x \<partial>M)"
    1.44 +      (is "\<And>A. _ \<Longrightarrow> _ = ?d A")
    1.45 +  shows "integral\<^isup>L N g = (\<integral> x. f x * g x \<partial>M)" (is ?integral)
    1.46 +    and "integrable N g = integrable M (\<lambda>x. f x * g x)" (is ?integrable)
    1.47 +proof -
    1.48 +  from f have ms: "measure_space (M\<lparr>measure := ?d\<rparr>)"
    1.49 +    by (intro measure_space_density[where u="\<lambda>x. extreal (f x)"]) auto
    1.50 +
    1.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>)"
    1.52 +    unfolding positive_integral_max_0
    1.53 +    by (intro measure_space.positive_integral_cong_measure) auto
    1.54 +  also have "\<dots> = (\<integral>\<^isup>+ x. extreal (f x) * max 0 (extreal (g x)) \<partial>M)"
    1.55 +    using f g by (intro positive_integral_translated_density) auto
    1.56 +  also have "\<dots> = (\<integral>\<^isup>+ x. max 0 (extreal (f x * g x)) \<partial>M)"
    1.57 +    using f by (intro positive_integral_cong_AE)
    1.58 +               (auto simp: extreal_max_0 zero_le_mult_iff split: split_max)
    1.59 +  finally have pos: "(\<integral>\<^isup>+ x. g x \<partial>N) = (\<integral>\<^isup>+ x. f x * g x \<partial>M)"
    1.60 +    by (simp add: positive_integral_max_0)
    1.61 +  
    1.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>)"
    1.63 +    unfolding positive_integral_max_0
    1.64 +    by (intro measure_space.positive_integral_cong_measure) auto
    1.65 +  also have "\<dots> = (\<integral>\<^isup>+ x. extreal (f x) * max 0 (extreal (- g x)) \<partial>M)"
    1.66 +    using f g by (intro positive_integral_translated_density) auto
    1.67 +  also have "\<dots> = (\<integral>\<^isup>+ x. max 0 (extreal (- f x * g x)) \<partial>M)"
    1.68 +    using f by (intro positive_integral_cong_AE)
    1.69 +               (auto simp: extreal_max_0 mult_le_0_iff split: split_max)
    1.70 +  finally have neg: "(\<integral>\<^isup>+ x. - g x \<partial>N) = (\<integral>\<^isup>+ x. - (f x * g x) \<partial>M)"
    1.71 +    by (simp add: positive_integral_max_0)
    1.72 +
    1.73 +  have g_N: "g \<in> borel_measurable N"
    1.74 +    using g N unfolding measurable_def by simp
    1.75 +
    1.76 +  show ?integral ?integrable
    1.77 +    unfolding lebesgue_integral_def integrable_def
    1.78 +    using pos neg f g g_N by auto
    1.79 +qed
    1.80 +
    1.81  lemma (in measure_space) integral_minus[intro, simp]:
    1.82    assumes "integrable M f"
    1.83    shows "integrable M (\<lambda>x. - f x)" "(\<integral>x. - f x \<partial>M) = - integral\<^isup>L M f"
    1.84 @@ -2221,9 +2281,14 @@
    1.85      by (simp add: \<mu>'_def lebesgue_integral_def positive_integral_const_If)
    1.86  qed
    1.87  
    1.88 +lemma indicator_less[simp]:
    1.89 +  "indicator A x \<le> (indicator B x::extreal) \<longleftrightarrow> (x \<in> A \<longrightarrow> x \<in> B)"
    1.90 +  by (simp add: indicator_def not_le)
    1.91 +
    1.92  lemma (in finite_measure) integral_less_AE:
    1.93    assumes int: "integrable M X" "integrable M Y"
    1.94 -  assumes gt: "AE x. X x < Y x" and neq0: "\<mu> (space M) \<noteq> 0"
    1.95 +  assumes A: "\<mu> A \<noteq> 0" "A \<in> sets M" "AE x. x \<in> A \<longrightarrow> X x \<noteq> Y x"
    1.96 +  assumes gt: "AE x. X x \<le> Y x"
    1.97    shows "integral\<^isup>L M X < integral\<^isup>L M Y"
    1.98  proof -
    1.99    have "integral\<^isup>L M X \<le> integral\<^isup>L M Y"
   1.100 @@ -2231,24 +2296,30 @@
   1.101    moreover
   1.102    have "integral\<^isup>L M X \<noteq> integral\<^isup>L M Y"
   1.103    proof
   1.104 -    from gt have "AE x. Y x - X x \<noteq> 0"
   1.105 -      by auto
   1.106 -    then have \<mu>: "\<mu> {x\<in>space M. Y x - X x \<noteq> 0} = \<mu> (space M)"
   1.107 -      using int
   1.108 -      by (intro AE_measure borel_measurable_neq) (auto simp add: integrable_def)
   1.109 -
   1.110      assume eq: "integral\<^isup>L M X = integral\<^isup>L M Y"
   1.111      have "integral\<^isup>L M (\<lambda>x. \<bar>Y x - X x\<bar>) = integral\<^isup>L M (\<lambda>x. Y x - X x)"
   1.112        using gt by (intro integral_cong_AE) auto
   1.113      also have "\<dots> = 0"
   1.114        using eq int by simp
   1.115 -    finally show False
   1.116 -      using \<mu> int neq0
   1.117 -      by (subst (asm) integral_0_iff) auto
   1.118 +    finally have "\<mu> {x \<in> space M. Y x - X x \<noteq> 0} = 0"
   1.119 +      using int by (simp add: integral_0_iff)
   1.120 +    moreover
   1.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)"
   1.122 +      using A by (intro positive_integral_mono_AE) auto
   1.123 +    then have "\<mu> A \<le> \<mu> {x \<in> space M. Y x - X x \<noteq> 0}"
   1.124 +      using int A by (simp add: integrable_def)
   1.125 +    moreover note `\<mu> A \<noteq> 0` positive_measure[OF `A \<in> sets M`]
   1.126 +    ultimately show False by auto
   1.127    qed
   1.128    ultimately show ?thesis by auto
   1.129  qed
   1.130  
   1.131 +lemma (in finite_measure) integral_less_AE_space:
   1.132 +  assumes int: "integrable M X" "integrable M Y"
   1.133 +  assumes gt: "AE x. X x < Y x" "\<mu> (space M) \<noteq> 0"
   1.134 +  shows "integral\<^isup>L M X < integral\<^isup>L M Y"
   1.135 +  using gt by (intro integral_less_AE[OF int, where A="space M"]) auto
   1.136 +
   1.137  lemma (in measure_space) integral_dominated_convergence:
   1.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"
   1.139    and w: "integrable M w"
     2.1 --- a/src/HOL/Probability/Probability_Measure.thy	Thu Jun 09 11:50:16 2011 +0200
     2.2 +++ b/src/HOL/Probability/Probability_Measure.thy	Thu Jun 09 13:55:11 2011 +0200
     2.3 @@ -28,6 +28,14 @@
     2.4  abbreviation (in prob_space)
     2.5    "joint_distribution X Y \<equiv> distribution (\<lambda>x. (X x, Y x))"
     2.6  
     2.7 +lemma (in prob_space) prob_space_cong:
     2.8 +  assumes "\<And>A. A \<in> sets M \<Longrightarrow> measure N A = \<mu> A" "space N = space M" "sets N = sets M"
     2.9 +  shows "prob_space N"
    2.10 +proof -
    2.11 +  interpret N: measure_space N by (intro measure_space_cong assms)
    2.12 +  show ?thesis by default (insert assms measure_space_1, simp)
    2.13 +qed
    2.14 +
    2.15  lemma (in prob_space) distribution_cong:
    2.16    assumes "\<And>x. x \<in> space M \<Longrightarrow> X x = Y x"
    2.17    shows "distribution X = distribution Y"
    2.18 @@ -54,15 +62,30 @@
    2.19  lemma (in prob_space) distribution_positive[simp, intro]:
    2.20    "0 \<le> distribution X A" unfolding distribution_def by auto
    2.21  
    2.22 +lemma (in prob_space) not_zero_less_distribution[simp]:
    2.23 +  "(\<not> 0 < distribution X A) \<longleftrightarrow> distribution X A = 0"
    2.24 +  using distribution_positive[of X A] by arith
    2.25 +
    2.26  lemma (in prob_space) joint_distribution_remove[simp]:
    2.27      "joint_distribution X X {(x, x)} = distribution X {x}"
    2.28    unfolding distribution_def by (auto intro!: arg_cong[where f=\<mu>'])
    2.29  
    2.30 +lemma (in prob_space) not_empty: "space M \<noteq> {}"
    2.31 +  using prob_space empty_measure' by auto
    2.32 +
    2.33  lemma (in prob_space) measure_le_1: "X \<in> sets M \<Longrightarrow> \<mu> X \<le> 1"
    2.34    unfolding measure_space_1[symmetric]
    2.35    using sets_into_space
    2.36    by (intro measure_mono) auto
    2.37  
    2.38 +lemma (in prob_space) AE_I_eq_1:
    2.39 +  assumes "\<mu> {x\<in>space M. P x} = 1" "{x\<in>space M. P x} \<in> sets M"
    2.40 +  shows "AE x. P x"
    2.41 +proof (rule AE_I)
    2.42 +  show "\<mu> (space M - {x \<in> space M. P x}) = 0"
    2.43 +    using assms measure_space_1 by (simp add: measure_compl)
    2.44 +qed (insert assms, auto)
    2.45 +
    2.46  lemma (in prob_space) distribution_1:
    2.47    "distribution X A \<le> 1"
    2.48    unfolding distribution_def by simp
    2.49 @@ -245,6 +268,146 @@
    2.50    using finite_measure_eq[of "X -` A \<inter> space M"]
    2.51    by (auto simp: measurable_sets distribution_def)
    2.52  
    2.53 +lemma (in prob_space) expectation_less:
    2.54 +  assumes [simp]: "integrable M X"
    2.55 +  assumes gt: "\<forall>x\<in>space M. X x < b"
    2.56 +  shows "expectation X < b"
    2.57 +proof -
    2.58 +  have "expectation X < expectation (\<lambda>x. b)"
    2.59 +    using gt measure_space_1
    2.60 +    by (intro integral_less_AE) auto
    2.61 +  then show ?thesis using prob_space by simp
    2.62 +qed
    2.63 +
    2.64 +lemma (in prob_space) expectation_greater:
    2.65 +  assumes [simp]: "integrable M X"
    2.66 +  assumes gt: "\<forall>x\<in>space M. a < X x"
    2.67 +  shows "a < expectation X"
    2.68 +proof -
    2.69 +  have "expectation (\<lambda>x. a) < expectation X"
    2.70 +    using gt measure_space_1
    2.71 +    by (intro integral_less_AE) auto
    2.72 +  then show ?thesis using prob_space by simp
    2.73 +qed
    2.74 +
    2.75 +lemma convex_le_Inf_differential:
    2.76 +  fixes f :: "real \<Rightarrow> real"
    2.77 +  assumes "convex_on I f"
    2.78 +  assumes "x \<in> interior I" "y \<in> I"
    2.79 +  shows "f y \<ge> f x + Inf ((\<lambda>t. (f x - f t) / (x - t)) ` ({x<..} \<inter> I)) * (y - x)"
    2.80 +    (is "_ \<ge> _ + Inf (?F x) * (y - x)")
    2.81 +proof -
    2.82 +  show ?thesis
    2.83 +  proof (cases rule: linorder_cases)
    2.84 +    assume "x < y"
    2.85 +    moreover
    2.86 +    have "open (interior I)" by auto
    2.87 +    from openE[OF this `x \<in> interior I`] guess e . note e = this
    2.88 +    moreover def t \<equiv> "min (x + e / 2) ((x + y) / 2)"
    2.89 +    ultimately have "x < t" "t < y" "t \<in> ball x e"
    2.90 +      by (auto simp: mem_ball dist_real_def field_simps split: split_min)
    2.91 +    with `x \<in> interior I` e interior_subset[of I] have "t \<in> I" "x \<in> I" by auto
    2.92 +
    2.93 +    have "open (interior I)" by auto
    2.94 +    from openE[OF this `x \<in> interior I`] guess e .
    2.95 +    moreover def K \<equiv> "x - e / 2"
    2.96 +    with `0 < e` have "K \<in> ball x e" "K < x" by (auto simp: mem_ball dist_real_def)
    2.97 +    ultimately have "K \<in> I" "K < x" "x \<in> I"
    2.98 +      using interior_subset[of I] `x \<in> interior I` by auto
    2.99 +
   2.100 +    have "Inf (?F x) \<le> (f x - f y) / (x - y)"
   2.101 +    proof (rule Inf_lower2)
   2.102 +      show "(f x - f t) / (x - t) \<in> ?F x"
   2.103 +        using `t \<in> I` `x < t` by auto
   2.104 +      show "(f x - f t) / (x - t) \<le> (f x - f y) / (x - y)"
   2.105 +        using `convex_on I f` `x \<in> I` `y \<in> I` `x < t` `t < y` by (rule convex_on_diff)
   2.106 +    next
   2.107 +      fix y assume "y \<in> ?F x"
   2.108 +      with order_trans[OF convex_on_diff[OF `convex_on I f` `K \<in> I` _ `K < x` _]]
   2.109 +      show "(f K - f x) / (K - x) \<le> y" by auto
   2.110 +    qed
   2.111 +    then show ?thesis
   2.112 +      using `x < y` by (simp add: field_simps)
   2.113 +  next
   2.114 +    assume "y < x"
   2.115 +    moreover
   2.116 +    have "open (interior I)" by auto
   2.117 +    from openE[OF this `x \<in> interior I`] guess e . note e = this
   2.118 +    moreover def t \<equiv> "x + e / 2"
   2.119 +    ultimately have "x < t" "t \<in> ball x e"
   2.120 +      by (auto simp: mem_ball dist_real_def field_simps)
   2.121 +    with `x \<in> interior I` e interior_subset[of I] have "t \<in> I" "x \<in> I" by auto
   2.122 +
   2.123 +    have "(f x - f y) / (x - y) \<le> Inf (?F x)"
   2.124 +    proof (rule Inf_greatest)
   2.125 +      have "(f x - f y) / (x - y) = (f y - f x) / (y - x)"
   2.126 +        using `y < x` by (auto simp: field_simps)
   2.127 +      also
   2.128 +      fix z  assume "z \<in> ?F x"
   2.129 +      with order_trans[OF convex_on_diff[OF `convex_on I f` `y \<in> I` _ `y < x`]]
   2.130 +      have "(f y - f x) / (y - x) \<le> z" by auto
   2.131 +      finally show "(f x - f y) / (x - y) \<le> z" .
   2.132 +    next
   2.133 +      have "open (interior I)" by auto
   2.134 +      from openE[OF this `x \<in> interior I`] guess e . note e = this
   2.135 +      then have "x + e / 2 \<in> ball x e" by (auto simp: mem_ball dist_real_def)
   2.136 +      with e interior_subset[of I] have "x + e / 2 \<in> {x<..} \<inter> I" by auto
   2.137 +      then show "?F x \<noteq> {}" by blast
   2.138 +    qed
   2.139 +    then show ?thesis
   2.140 +      using `y < x` by (simp add: field_simps)
   2.141 +  qed simp
   2.142 +qed
   2.143 +
   2.144 +lemma (in prob_space) jensens_inequality:
   2.145 +  fixes a b :: real
   2.146 +  assumes X: "integrable M X" "X ` space M \<subseteq> I"
   2.147 +  assumes I: "I = {a <..< b} \<or> I = {a <..} \<or> I = {..< b} \<or> I = UNIV"
   2.148 +  assumes q: "integrable M (\<lambda>x. q (X x))" "convex_on I q"
   2.149 +  shows "q (expectation X) \<le> expectation (\<lambda>x. q (X x))"
   2.150 +proof -
   2.151 +  let "?F x" = "Inf ((\<lambda>t. (q x - q t) / (x - t)) ` ({x<..} \<inter> I))"
   2.152 +  from not_empty X(2) have "I \<noteq> {}" by auto
   2.153 +
   2.154 +  from I have "open I" by auto
   2.155 +
   2.156 +  note I
   2.157 +  moreover
   2.158 +  { assume "I \<subseteq> {a <..}"
   2.159 +    with X have "a < expectation X"
   2.160 +      by (intro expectation_greater) auto }
   2.161 +  moreover
   2.162 +  { assume "I \<subseteq> {..< b}"
   2.163 +    with X have "expectation X < b"
   2.164 +      by (intro expectation_less) auto }
   2.165 +  ultimately have "expectation X \<in> I"
   2.166 +    by (elim disjE)  (auto simp: subset_eq)
   2.167 +  moreover
   2.168 +  { fix y assume y: "y \<in> I"
   2.169 +    with q(2) `open I` have "Sup ((\<lambda>x. q x + ?F x * (y - x)) ` I) = q y"
   2.170 +      by (auto intro!: Sup_eq_maximum convex_le_Inf_differential image_eqI[OF _ y] simp: interior_open) }
   2.171 +  ultimately have "q (expectation X) = Sup ((\<lambda>x. q x + ?F x * (expectation X - x)) ` I)"
   2.172 +    by simp
   2.173 +  also have "\<dots> \<le> expectation (\<lambda>w. q (X w))"
   2.174 +  proof (rule Sup_least)
   2.175 +    show "(\<lambda>x. q x + ?F x * (expectation X - x)) ` I \<noteq> {}"
   2.176 +      using `I \<noteq> {}` by auto
   2.177 +  next
   2.178 +    fix k assume "k \<in> (\<lambda>x. q x + ?F x * (expectation X - x)) ` I"
   2.179 +    then guess x .. note x = this
   2.180 +    have "q x + ?F x * (expectation X  - x) = expectation (\<lambda>w. q x + ?F x * (X w - x))"
   2.181 +      using prob_space
   2.182 +      by (simp add: integral_add integral_cmult integral_diff lebesgue_integral_const X)
   2.183 +    also have "\<dots> \<le> expectation (\<lambda>w. q (X w))"
   2.184 +      using `x \<in> I` `open I` X(2)
   2.185 +      by (intro integral_mono integral_add integral_cmult integral_diff
   2.186 +                lebesgue_integral_const X q convex_le_Inf_differential)
   2.187 +         (auto simp: interior_open)
   2.188 +    finally show "k \<le> expectation (\<lambda>w. q (X w))" using x by auto
   2.189 +  qed
   2.190 +  finally show "q (expectation X) \<le> expectation (\<lambda>x. q (X x))" .
   2.191 +qed
   2.192 +
   2.193  lemma (in prob_space) distribution_eq_translated_integral:
   2.194    assumes "random_variable S X" "A \<in> sets S"
   2.195    shows "distribution X A = integral\<^isup>P (S\<lparr>measure := extreal \<circ> distribution X\<rparr>) (indicator A)"
   2.196 @@ -722,9 +885,6 @@
   2.197    unfolding finite_prob_space_def finite_measure_space_def prob_space_def prob_space_axioms_def
   2.198    by auto
   2.199  
   2.200 -lemma (in prob_space) not_empty: "space M \<noteq> {}"
   2.201 -  using prob_space empty_measure' by auto
   2.202 -
   2.203  lemma (in finite_prob_space) sum_over_space_eq_1: "(\<Sum>x\<in>space M. \<mu> {x}) = 1"
   2.204    using measure_space_1 sum_over_space by simp
   2.205  
   2.206 @@ -829,7 +989,7 @@
   2.207    also have "\<dots> = real_of_nat (card (space M)) * prob {x}" by simp
   2.208    finally have one: "1 = real (card (space M)) * prob {x}"
   2.209      using real_eq_of_nat by auto
   2.210 -  hence two: "real (card (space M)) \<noteq> 0" by fastsimp 
   2.211 +  hence two: "real (card (space M)) \<noteq> 0" by fastsimp
   2.212    from one have three: "prob {x} \<noteq> 0" by fastsimp
   2.213    thus ?thesis using one two three divide_cancel_right
   2.214      by (auto simp:field_simps)