summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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.182 + by (simp add: integral_add integral_cmult integral_diff lebesgue_integral_const X) 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)