# HG changeset patch # User hoelzl # Date 1307620511 -7200 # Node ID 9ba256ad678191558fae2f275f68fea03778a873 # Parent a150d16bf77c0a7b00a9e36989c22b1c22017526 jensens inequality diff -r a150d16bf77c -r 9ba256ad6781 src/HOL/Probability/Lebesgue_Integration.thy --- a/src/HOL/Probability/Lebesgue_Integration.thy Thu Jun 09 11:50:16 2011 +0200 +++ b/src/HOL/Probability/Lebesgue_Integration.thy Thu Jun 09 13:55:11 2011 +0200 @@ -1712,6 +1712,12 @@ shows "integral\<^isup>L N f = integral\<^isup>L M f" by (simp add: positive_integral_cong_measure[OF assms] lebesgue_integral_def) +lemma (in measure_space) integrable_cong_measure: + assumes "\A. A \ sets M \ measure N A = \ A" "sets N = sets M" "space N = space M" + shows "integrable N f \ integrable M f" + using assms + by (simp add: positive_integral_cong_measure[OF assms] integrable_def measurable_def) + lemma (in measure_space) integral_cong_AE: assumes cong: "AE x. f x = g x" shows "integral\<^isup>L M f = integral\<^isup>L M g" @@ -1722,6 +1728,18 @@ unfolding *[THEN positive_integral_cong_AE] lebesgue_integral_def .. qed +lemma (in measure_space) integrable_cong_AE: + assumes borel: "f \ borel_measurable M" "g \ borel_measurable M" + assumes "AE x. f x = g x" + shows "integrable M f = integrable M g" +proof - + have "(\\<^isup>+ x. extreal (f x) \M) = (\\<^isup>+ x. extreal (g x) \M)" + "(\\<^isup>+ x. extreal (- f x) \M) = (\\<^isup>+ x. extreal (- g x) \M)" + using assms by (auto intro!: positive_integral_cong_AE) + with assms show ?thesis + by (auto simp: integrable_def) +qed + lemma (in measure_space) integrable_cong: "(\x. x \ space M \ f x = g x) \ integrable M f \ integrable M g" by (simp cong: positive_integral_cong measurable_cong add: integrable_def) @@ -1767,6 +1785,48 @@ by (auto simp: borel[THEN positive_integral_vimage[OF T]]) qed +lemma (in measure_space) integral_translated_density: + assumes f: "f \ borel_measurable M" "AE x. 0 \ f x" + and g: "g \ borel_measurable M" + and N: "space N = space M" "sets N = sets M" + and density: "\A. A \ sets M \ measure N A = (\\<^isup>+ x. f x * indicator A x \M)" + (is "\A. _ \ _ = ?d A") + shows "integral\<^isup>L N g = (\ x. f x * g x \M)" (is ?integral) + and "integrable N g = integrable M (\x. f x * g x)" (is ?integrable) +proof - + from f have ms: "measure_space (M\measure := ?d\)" + by (intro measure_space_density[where u="\x. extreal (f x)"]) auto + + from ms density N have "(\\<^isup>+ x. g x \N) = (\\<^isup>+ x. max 0 (extreal (g x)) \M\measure := ?d\)" + unfolding positive_integral_max_0 + by (intro measure_space.positive_integral_cong_measure) auto + also have "\ = (\\<^isup>+ x. extreal (f x) * max 0 (extreal (g x)) \M)" + using f g by (intro positive_integral_translated_density) auto + also have "\ = (\\<^isup>+ x. max 0 (extreal (f x * g x)) \M)" + using f by (intro positive_integral_cong_AE) + (auto simp: extreal_max_0 zero_le_mult_iff split: split_max) + finally have pos: "(\\<^isup>+ x. g x \N) = (\\<^isup>+ x. f x * g x \M)" + by (simp add: positive_integral_max_0) + + from ms density N have "(\\<^isup>+ x. - (g x) \N) = (\\<^isup>+ x. max 0 (extreal (- g x)) \M\measure := ?d\)" + unfolding positive_integral_max_0 + by (intro measure_space.positive_integral_cong_measure) auto + also have "\ = (\\<^isup>+ x. extreal (f x) * max 0 (extreal (- g x)) \M)" + using f g by (intro positive_integral_translated_density) auto + also have "\ = (\\<^isup>+ x. max 0 (extreal (- f x * g x)) \M)" + using f by (intro positive_integral_cong_AE) + (auto simp: extreal_max_0 mult_le_0_iff split: split_max) + finally have neg: "(\\<^isup>+ x. - g x \N) = (\\<^isup>+ x. - (f x * g x) \M)" + by (simp add: positive_integral_max_0) + + have g_N: "g \ borel_measurable N" + using g N unfolding measurable_def by simp + + show ?integral ?integrable + unfolding lebesgue_integral_def integrable_def + using pos neg f g g_N by auto +qed + lemma (in measure_space) integral_minus[intro, simp]: assumes "integrable M f" shows "integrable M (\x. - f x)" "(\x. - f x \M) = - integral\<^isup>L M f" @@ -2221,9 +2281,14 @@ by (simp add: \'_def lebesgue_integral_def positive_integral_const_If) qed +lemma indicator_less[simp]: + "indicator A x \ (indicator B x::extreal) \ (x \ A \ x \ B)" + by (simp add: indicator_def not_le) + lemma (in finite_measure) integral_less_AE: assumes int: "integrable M X" "integrable M Y" - assumes gt: "AE x. X x < Y x" and neq0: "\ (space M) \ 0" + assumes A: "\ A \ 0" "A \ sets M" "AE x. x \ A \ X x \ Y x" + assumes gt: "AE x. X x \ Y x" shows "integral\<^isup>L M X < integral\<^isup>L M Y" proof - have "integral\<^isup>L M X \ integral\<^isup>L M Y" @@ -2231,24 +2296,30 @@ moreover have "integral\<^isup>L M X \ integral\<^isup>L M Y" proof - from gt have "AE x. Y x - X x \ 0" - by auto - then have \: "\ {x\space M. Y x - X x \ 0} = \ (space M)" - using int - by (intro AE_measure borel_measurable_neq) (auto simp add: integrable_def) - assume eq: "integral\<^isup>L M X = integral\<^isup>L M Y" have "integral\<^isup>L M (\x. \Y x - X x\) = integral\<^isup>L M (\x. Y x - X x)" using gt by (intro integral_cong_AE) auto also have "\ = 0" using eq int by simp - finally show False - using \ int neq0 - by (subst (asm) integral_0_iff) auto + finally have "\ {x \ space M. Y x - X x \ 0} = 0" + using int by (simp add: integral_0_iff) + moreover + have "(\\<^isup>+x. indicator A x \M) \ (\\<^isup>+x. indicator {x \ space M. Y x - X x \ 0} x \M)" + using A by (intro positive_integral_mono_AE) auto + then have "\ A \ \ {x \ space M. Y x - X x \ 0}" + using int A by (simp add: integrable_def) + moreover note `\ A \ 0` positive_measure[OF `A \ sets M`] + ultimately show False by auto qed ultimately show ?thesis by auto qed +lemma (in finite_measure) integral_less_AE_space: + assumes int: "integrable M X" "integrable M Y" + assumes gt: "AE x. X x < Y x" "\ (space M) \ 0" + shows "integral\<^isup>L M X < integral\<^isup>L M Y" + using gt by (intro integral_less_AE[OF int, where A="space M"]) auto + lemma (in measure_space) integral_dominated_convergence: assumes u: "\i. integrable M (u i)" and bound: "\x j. x\space M \ \u j x\ \ w x" and w: "integrable M w" diff -r a150d16bf77c -r 9ba256ad6781 src/HOL/Probability/Probability_Measure.thy --- a/src/HOL/Probability/Probability_Measure.thy Thu Jun 09 11:50:16 2011 +0200 +++ b/src/HOL/Probability/Probability_Measure.thy Thu Jun 09 13:55:11 2011 +0200 @@ -28,6 +28,14 @@ abbreviation (in prob_space) "joint_distribution X Y \ distribution (\x. (X x, Y x))" +lemma (in prob_space) prob_space_cong: + assumes "\A. A \ sets M \ measure N A = \ A" "space N = space M" "sets N = sets M" + shows "prob_space N" +proof - + interpret N: measure_space N by (intro measure_space_cong assms) + show ?thesis by default (insert assms measure_space_1, simp) +qed + lemma (in prob_space) distribution_cong: assumes "\x. x \ space M \ X x = Y x" shows "distribution X = distribution Y" @@ -54,15 +62,30 @@ lemma (in prob_space) distribution_positive[simp, intro]: "0 \ distribution X A" unfolding distribution_def by auto +lemma (in prob_space) not_zero_less_distribution[simp]: + "(\ 0 < distribution X A) \ distribution X A = 0" + using distribution_positive[of X A] by arith + lemma (in prob_space) joint_distribution_remove[simp]: "joint_distribution X X {(x, x)} = distribution X {x}" unfolding distribution_def by (auto intro!: arg_cong[where f=\']) +lemma (in prob_space) not_empty: "space M \ {}" + using prob_space empty_measure' by auto + lemma (in prob_space) measure_le_1: "X \ sets M \ \ X \ 1" unfolding measure_space_1[symmetric] using sets_into_space by (intro measure_mono) auto +lemma (in prob_space) AE_I_eq_1: + assumes "\ {x\space M. P x} = 1" "{x\space M. P x} \ sets M" + shows "AE x. P x" +proof (rule AE_I) + show "\ (space M - {x \ space M. P x}) = 0" + using assms measure_space_1 by (simp add: measure_compl) +qed (insert assms, auto) + lemma (in prob_space) distribution_1: "distribution X A \ 1" unfolding distribution_def by simp @@ -245,6 +268,146 @@ using finite_measure_eq[of "X -` A \ space M"] by (auto simp: measurable_sets distribution_def) +lemma (in prob_space) expectation_less: + assumes [simp]: "integrable M X" + assumes gt: "\x\space M. X x < b" + shows "expectation X < b" +proof - + have "expectation X < expectation (\x. b)" + using gt measure_space_1 + by (intro integral_less_AE) auto + then show ?thesis using prob_space by simp +qed + +lemma (in prob_space) expectation_greater: + assumes [simp]: "integrable M X" + assumes gt: "\x\space M. a < X x" + shows "a < expectation X" +proof - + have "expectation (\x. a) < expectation X" + using gt measure_space_1 + by (intro integral_less_AE) auto + then show ?thesis using prob_space by simp +qed + +lemma convex_le_Inf_differential: + fixes f :: "real \ real" + assumes "convex_on I f" + assumes "x \ interior I" "y \ I" + shows "f y \ f x + Inf ((\t. (f x - f t) / (x - t)) ` ({x<..} \ I)) * (y - x)" + (is "_ \ _ + Inf (?F x) * (y - x)") +proof - + show ?thesis + proof (cases rule: linorder_cases) + assume "x < y" + moreover + have "open (interior I)" by auto + from openE[OF this `x \ interior I`] guess e . note e = this + moreover def t \ "min (x + e / 2) ((x + y) / 2)" + ultimately have "x < t" "t < y" "t \ ball x e" + by (auto simp: mem_ball dist_real_def field_simps split: split_min) + with `x \ interior I` e interior_subset[of I] have "t \ I" "x \ I" by auto + + have "open (interior I)" by auto + from openE[OF this `x \ interior I`] guess e . + moreover def K \ "x - e / 2" + with `0 < e` have "K \ ball x e" "K < x" by (auto simp: mem_ball dist_real_def) + ultimately have "K \ I" "K < x" "x \ I" + using interior_subset[of I] `x \ interior I` by auto + + have "Inf (?F x) \ (f x - f y) / (x - y)" + proof (rule Inf_lower2) + show "(f x - f t) / (x - t) \ ?F x" + using `t \ I` `x < t` by auto + show "(f x - f t) / (x - t) \ (f x - f y) / (x - y)" + using `convex_on I f` `x \ I` `y \ I` `x < t` `t < y` by (rule convex_on_diff) + next + fix y assume "y \ ?F x" + with order_trans[OF convex_on_diff[OF `convex_on I f` `K \ I` _ `K < x` _]] + show "(f K - f x) / (K - x) \ y" by auto + qed + then show ?thesis + using `x < y` by (simp add: field_simps) + next + assume "y < x" + moreover + have "open (interior I)" by auto + from openE[OF this `x \ interior I`] guess e . note e = this + moreover def t \ "x + e / 2" + ultimately have "x < t" "t \ ball x e" + by (auto simp: mem_ball dist_real_def field_simps) + with `x \ interior I` e interior_subset[of I] have "t \ I" "x \ I" by auto + + have "(f x - f y) / (x - y) \ Inf (?F x)" + proof (rule Inf_greatest) + have "(f x - f y) / (x - y) = (f y - f x) / (y - x)" + using `y < x` by (auto simp: field_simps) + also + fix z assume "z \ ?F x" + with order_trans[OF convex_on_diff[OF `convex_on I f` `y \ I` _ `y < x`]] + have "(f y - f x) / (y - x) \ z" by auto + finally show "(f x - f y) / (x - y) \ z" . + next + have "open (interior I)" by auto + from openE[OF this `x \ interior I`] guess e . note e = this + then have "x + e / 2 \ ball x e" by (auto simp: mem_ball dist_real_def) + with e interior_subset[of I] have "x + e / 2 \ {x<..} \ I" by auto + then show "?F x \ {}" by blast + qed + then show ?thesis + using `y < x` by (simp add: field_simps) + qed simp +qed + +lemma (in prob_space) jensens_inequality: + fixes a b :: real + assumes X: "integrable M X" "X ` space M \ I" + assumes I: "I = {a <..< b} \ I = {a <..} \ I = {..< b} \ I = UNIV" + assumes q: "integrable M (\x. q (X x))" "convex_on I q" + shows "q (expectation X) \ expectation (\x. q (X x))" +proof - + let "?F x" = "Inf ((\t. (q x - q t) / (x - t)) ` ({x<..} \ I))" + from not_empty X(2) have "I \ {}" by auto + + from I have "open I" by auto + + note I + moreover + { assume "I \ {a <..}" + with X have "a < expectation X" + by (intro expectation_greater) auto } + moreover + { assume "I \ {..< b}" + with X have "expectation X < b" + by (intro expectation_less) auto } + ultimately have "expectation X \ I" + by (elim disjE) (auto simp: subset_eq) + moreover + { fix y assume y: "y \ I" + with q(2) `open I` have "Sup ((\x. q x + ?F x * (y - x)) ` I) = q y" + by (auto intro!: Sup_eq_maximum convex_le_Inf_differential image_eqI[OF _ y] simp: interior_open) } + ultimately have "q (expectation X) = Sup ((\x. q x + ?F x * (expectation X - x)) ` I)" + by simp + also have "\ \ expectation (\w. q (X w))" + proof (rule Sup_least) + show "(\x. q x + ?F x * (expectation X - x)) ` I \ {}" + using `I \ {}` by auto + next + fix k assume "k \ (\x. q x + ?F x * (expectation X - x)) ` I" + then guess x .. note x = this + have "q x + ?F x * (expectation X - x) = expectation (\w. q x + ?F x * (X w - x))" + using prob_space + by (simp add: integral_add integral_cmult integral_diff lebesgue_integral_const X) + also have "\ \ expectation (\w. q (X w))" + using `x \ I` `open I` X(2) + by (intro integral_mono integral_add integral_cmult integral_diff + lebesgue_integral_const X q convex_le_Inf_differential) + (auto simp: interior_open) + finally show "k \ expectation (\w. q (X w))" using x by auto + qed + finally show "q (expectation X) \ expectation (\x. q (X x))" . +qed + lemma (in prob_space) distribution_eq_translated_integral: assumes "random_variable S X" "A \ sets S" shows "distribution X A = integral\<^isup>P (S\measure := extreal \ distribution X\) (indicator A)" @@ -722,9 +885,6 @@ unfolding finite_prob_space_def finite_measure_space_def prob_space_def prob_space_axioms_def by auto -lemma (in prob_space) not_empty: "space M \ {}" - using prob_space empty_measure' by auto - lemma (in finite_prob_space) sum_over_space_eq_1: "(\x\space M. \ {x}) = 1" using measure_space_1 sum_over_space by simp @@ -829,7 +989,7 @@ also have "\ = real_of_nat (card (space M)) * prob {x}" by simp finally have one: "1 = real (card (space M)) * prob {x}" using real_eq_of_nat by auto - hence two: "real (card (space M)) \ 0" by fastsimp + hence two: "real (card (space M)) \ 0" by fastsimp from one have three: "prob {x} \ 0" by fastsimp thus ?thesis using one two three divide_cancel_right by (auto simp:field_simps)