src/HOL/Probability/Probability_Measure.thy
 changeset 43339 9ba256ad6781 parent 42991 3fa22920bf86 child 43340 60e181c4eae4
```     1.1 --- a/src/HOL/Probability/Probability_Measure.thy	Thu Jun 09 11:50:16 2011 +0200
1.2 +++ b/src/HOL/Probability/Probability_Measure.thy	Thu Jun 09 13:55:11 2011 +0200
1.3 @@ -28,6 +28,14 @@
1.4  abbreviation (in prob_space)
1.5    "joint_distribution X Y \<equiv> distribution (\<lambda>x. (X x, Y x))"
1.6
1.7 +lemma (in prob_space) prob_space_cong:
1.8 +  assumes "\<And>A. A \<in> sets M \<Longrightarrow> measure N A = \<mu> A" "space N = space M" "sets N = sets M"
1.9 +  shows "prob_space N"
1.10 +proof -
1.11 +  interpret N: measure_space N by (intro measure_space_cong assms)
1.12 +  show ?thesis by default (insert assms measure_space_1, simp)
1.13 +qed
1.14 +
1.15  lemma (in prob_space) distribution_cong:
1.16    assumes "\<And>x. x \<in> space M \<Longrightarrow> X x = Y x"
1.17    shows "distribution X = distribution Y"
1.18 @@ -54,15 +62,30 @@
1.19  lemma (in prob_space) distribution_positive[simp, intro]:
1.20    "0 \<le> distribution X A" unfolding distribution_def by auto
1.21
1.22 +lemma (in prob_space) not_zero_less_distribution[simp]:
1.23 +  "(\<not> 0 < distribution X A) \<longleftrightarrow> distribution X A = 0"
1.24 +  using distribution_positive[of X A] by arith
1.25 +
1.26  lemma (in prob_space) joint_distribution_remove[simp]:
1.27      "joint_distribution X X {(x, x)} = distribution X {x}"
1.28    unfolding distribution_def by (auto intro!: arg_cong[where f=\<mu>'])
1.29
1.30 +lemma (in prob_space) not_empty: "space M \<noteq> {}"
1.31 +  using prob_space empty_measure' by auto
1.32 +
1.33  lemma (in prob_space) measure_le_1: "X \<in> sets M \<Longrightarrow> \<mu> X \<le> 1"
1.34    unfolding measure_space_1[symmetric]
1.35    using sets_into_space
1.36    by (intro measure_mono) auto
1.37
1.38 +lemma (in prob_space) AE_I_eq_1:
1.39 +  assumes "\<mu> {x\<in>space M. P x} = 1" "{x\<in>space M. P x} \<in> sets M"
1.40 +  shows "AE x. P x"
1.41 +proof (rule AE_I)
1.42 +  show "\<mu> (space M - {x \<in> space M. P x}) = 0"
1.43 +    using assms measure_space_1 by (simp add: measure_compl)
1.44 +qed (insert assms, auto)
1.45 +
1.46  lemma (in prob_space) distribution_1:
1.47    "distribution X A \<le> 1"
1.48    unfolding distribution_def by simp
1.49 @@ -245,6 +268,146 @@
1.50    using finite_measure_eq[of "X -` A \<inter> space M"]
1.51    by (auto simp: measurable_sets distribution_def)
1.52
1.53 +lemma (in prob_space) expectation_less:
1.54 +  assumes [simp]: "integrable M X"
1.55 +  assumes gt: "\<forall>x\<in>space M. X x < b"
1.56 +  shows "expectation X < b"
1.57 +proof -
1.58 +  have "expectation X < expectation (\<lambda>x. b)"
1.59 +    using gt measure_space_1
1.60 +    by (intro integral_less_AE) auto
1.61 +  then show ?thesis using prob_space by simp
1.62 +qed
1.63 +
1.64 +lemma (in prob_space) expectation_greater:
1.65 +  assumes [simp]: "integrable M X"
1.66 +  assumes gt: "\<forall>x\<in>space M. a < X x"
1.67 +  shows "a < expectation X"
1.68 +proof -
1.69 +  have "expectation (\<lambda>x. a) < expectation X"
1.70 +    using gt measure_space_1
1.71 +    by (intro integral_less_AE) auto
1.72 +  then show ?thesis using prob_space by simp
1.73 +qed
1.74 +
1.75 +lemma convex_le_Inf_differential:
1.76 +  fixes f :: "real \<Rightarrow> real"
1.77 +  assumes "convex_on I f"
1.78 +  assumes "x \<in> interior I" "y \<in> I"
1.79 +  shows "f y \<ge> f x + Inf ((\<lambda>t. (f x - f t) / (x - t)) ` ({x<..} \<inter> I)) * (y - x)"
1.80 +    (is "_ \<ge> _ + Inf (?F x) * (y - x)")
1.81 +proof -
1.82 +  show ?thesis
1.83 +  proof (cases rule: linorder_cases)
1.84 +    assume "x < y"
1.85 +    moreover
1.86 +    have "open (interior I)" by auto
1.87 +    from openE[OF this `x \<in> interior I`] guess e . note e = this
1.88 +    moreover def t \<equiv> "min (x + e / 2) ((x + y) / 2)"
1.89 +    ultimately have "x < t" "t < y" "t \<in> ball x e"
1.90 +      by (auto simp: mem_ball dist_real_def field_simps split: split_min)
1.91 +    with `x \<in> interior I` e interior_subset[of I] have "t \<in> I" "x \<in> I" by auto
1.92 +
1.93 +    have "open (interior I)" by auto
1.94 +    from openE[OF this `x \<in> interior I`] guess e .
1.95 +    moreover def K \<equiv> "x - e / 2"
1.96 +    with `0 < e` have "K \<in> ball x e" "K < x" by (auto simp: mem_ball dist_real_def)
1.97 +    ultimately have "K \<in> I" "K < x" "x \<in> I"
1.98 +      using interior_subset[of I] `x \<in> interior I` by auto
1.99 +
1.100 +    have "Inf (?F x) \<le> (f x - f y) / (x - y)"
1.101 +    proof (rule Inf_lower2)
1.102 +      show "(f x - f t) / (x - t) \<in> ?F x"
1.103 +        using `t \<in> I` `x < t` by auto
1.104 +      show "(f x - f t) / (x - t) \<le> (f x - f y) / (x - y)"
1.105 +        using `convex_on I f` `x \<in> I` `y \<in> I` `x < t` `t < y` by (rule convex_on_diff)
1.106 +    next
1.107 +      fix y assume "y \<in> ?F x"
1.108 +      with order_trans[OF convex_on_diff[OF `convex_on I f` `K \<in> I` _ `K < x` _]]
1.109 +      show "(f K - f x) / (K - x) \<le> y" by auto
1.110 +    qed
1.111 +    then show ?thesis
1.112 +      using `x < y` by (simp add: field_simps)
1.113 +  next
1.114 +    assume "y < x"
1.115 +    moreover
1.116 +    have "open (interior I)" by auto
1.117 +    from openE[OF this `x \<in> interior I`] guess e . note e = this
1.118 +    moreover def t \<equiv> "x + e / 2"
1.119 +    ultimately have "x < t" "t \<in> ball x e"
1.120 +      by (auto simp: mem_ball dist_real_def field_simps)
1.121 +    with `x \<in> interior I` e interior_subset[of I] have "t \<in> I" "x \<in> I" by auto
1.122 +
1.123 +    have "(f x - f y) / (x - y) \<le> Inf (?F x)"
1.124 +    proof (rule Inf_greatest)
1.125 +      have "(f x - f y) / (x - y) = (f y - f x) / (y - x)"
1.126 +        using `y < x` by (auto simp: field_simps)
1.127 +      also
1.128 +      fix z  assume "z \<in> ?F x"
1.129 +      with order_trans[OF convex_on_diff[OF `convex_on I f` `y \<in> I` _ `y < x`]]
1.130 +      have "(f y - f x) / (y - x) \<le> z" by auto
1.131 +      finally show "(f x - f y) / (x - y) \<le> z" .
1.132 +    next
1.133 +      have "open (interior I)" by auto
1.134 +      from openE[OF this `x \<in> interior I`] guess e . note e = this
1.135 +      then have "x + e / 2 \<in> ball x e" by (auto simp: mem_ball dist_real_def)
1.136 +      with e interior_subset[of I] have "x + e / 2 \<in> {x<..} \<inter> I" by auto
1.137 +      then show "?F x \<noteq> {}" by blast
1.138 +    qed
1.139 +    then show ?thesis
1.140 +      using `y < x` by (simp add: field_simps)
1.141 +  qed simp
1.142 +qed
1.143 +
1.144 +lemma (in prob_space) jensens_inequality:
1.145 +  fixes a b :: real
1.146 +  assumes X: "integrable M X" "X ` space M \<subseteq> I"
1.147 +  assumes I: "I = {a <..< b} \<or> I = {a <..} \<or> I = {..< b} \<or> I = UNIV"
1.148 +  assumes q: "integrable M (\<lambda>x. q (X x))" "convex_on I q"
1.149 +  shows "q (expectation X) \<le> expectation (\<lambda>x. q (X x))"
1.150 +proof -
1.151 +  let "?F x" = "Inf ((\<lambda>t. (q x - q t) / (x - t)) ` ({x<..} \<inter> I))"
1.152 +  from not_empty X(2) have "I \<noteq> {}" by auto
1.153 +
1.154 +  from I have "open I" by auto
1.155 +
1.156 +  note I
1.157 +  moreover
1.158 +  { assume "I \<subseteq> {a <..}"
1.159 +    with X have "a < expectation X"
1.160 +      by (intro expectation_greater) auto }
1.161 +  moreover
1.162 +  { assume "I \<subseteq> {..< b}"
1.163 +    with X have "expectation X < b"
1.164 +      by (intro expectation_less) auto }
1.165 +  ultimately have "expectation X \<in> I"
1.166 +    by (elim disjE)  (auto simp: subset_eq)
1.167 +  moreover
1.168 +  { fix y assume y: "y \<in> I"
1.169 +    with q(2) `open I` have "Sup ((\<lambda>x. q x + ?F x * (y - x)) ` I) = q y"
1.170 +      by (auto intro!: Sup_eq_maximum convex_le_Inf_differential image_eqI[OF _ y] simp: interior_open) }
1.171 +  ultimately have "q (expectation X) = Sup ((\<lambda>x. q x + ?F x * (expectation X - x)) ` I)"
1.172 +    by simp
1.173 +  also have "\<dots> \<le> expectation (\<lambda>w. q (X w))"
1.174 +  proof (rule Sup_least)
1.175 +    show "(\<lambda>x. q x + ?F x * (expectation X - x)) ` I \<noteq> {}"
1.176 +      using `I \<noteq> {}` by auto
1.177 +  next
1.178 +    fix k assume "k \<in> (\<lambda>x. q x + ?F x * (expectation X - x)) ` I"
1.179 +    then guess x .. note x = this
1.180 +    have "q x + ?F x * (expectation X  - x) = expectation (\<lambda>w. q x + ?F x * (X w - x))"
1.181 +      using prob_space
1.183 +    also have "\<dots> \<le> expectation (\<lambda>w. q (X w))"
1.184 +      using `x \<in> I` `open I` X(2)
1.185 +      by (intro integral_mono integral_add integral_cmult integral_diff
1.186 +                lebesgue_integral_const X q convex_le_Inf_differential)
1.187 +         (auto simp: interior_open)
1.188 +    finally show "k \<le> expectation (\<lambda>w. q (X w))" using x by auto
1.189 +  qed
1.190 +  finally show "q (expectation X) \<le> expectation (\<lambda>x. q (X x))" .
1.191 +qed
1.192 +
1.193  lemma (in prob_space) distribution_eq_translated_integral:
1.194    assumes "random_variable S X" "A \<in> sets S"
1.195    shows "distribution X A = integral\<^isup>P (S\<lparr>measure := extreal \<circ> distribution X\<rparr>) (indicator A)"
1.196 @@ -722,9 +885,6 @@
1.197    unfolding finite_prob_space_def finite_measure_space_def prob_space_def prob_space_axioms_def
1.198    by auto
1.199
1.200 -lemma (in prob_space) not_empty: "space M \<noteq> {}"
1.201 -  using prob_space empty_measure' by auto
1.202 -
1.203  lemma (in finite_prob_space) sum_over_space_eq_1: "(\<Sum>x\<in>space M. \<mu> {x}) = 1"
1.204    using measure_space_1 sum_over_space by simp
1.205
1.206 @@ -829,7 +989,7 @@
1.207    also have "\<dots> = real_of_nat (card (space M)) * prob {x}" by simp
1.208    finally have one: "1 = real (card (space M)) * prob {x}"
1.209      using real_eq_of_nat by auto
1.210 -  hence two: "real (card (space M)) \<noteq> 0" by fastsimp
1.211 +  hence two: "real (card (space M)) \<noteq> 0" by fastsimp
1.212    from one have three: "prob {x} \<noteq> 0" by fastsimp
1.213    thus ?thesis using one two three divide_cancel_right
1.214      by (auto simp:field_simps)
```