summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | hoelzl |

Thu, 26 May 2011 20:51:03 +0200 | |

changeset 42991 | 3fa22920bf86 |

parent 42990 | 3706951a6421 |

child 42992 | 4fc15e3217eb |

integral strong monotone; finite subadditivity for measure

--- a/src/HOL/Probability/Lebesgue_Integration.thy Thu May 26 20:49:56 2011 +0200 +++ b/src/HOL/Probability/Lebesgue_Integration.thy Thu May 26 20:51:03 2011 +0200 @@ -9,6 +9,9 @@ imports Measure Borel_Space begin +lemma real_extreal_1[simp]: "real (1::extreal) = 1" + unfolding one_extreal_def by simp + lemma extreal_indicator_pos[simp,intro]: "0 \<le> (indicator A x ::extreal)" unfolding indicator_def by auto @@ -1604,6 +1607,10 @@ finally show ?thesis . qed +lemma (in measure_space) positive_integral_const_If: + "(\<integral>\<^isup>+x. a \<partial>M) = (if 0 \<le> a then a * \<mu> (space M) else 0)" + by (auto intro!: positive_integral_0_iff_AE[THEN iffD2]) + lemma (in measure_space) positive_integral_restricted: assumes A: "A \<in> sets M" shows "integral\<^isup>P (restricted_space A) f = (\<integral>\<^isup>+ x. f x * indicator A x \<partial>M)" @@ -1765,6 +1772,15 @@ shows "integrable M (\<lambda>x. - f x)" "(\<integral>x. - f x \<partial>M) = - integral\<^isup>L M f" using assms by (auto simp: integrable_def lebesgue_integral_def) +lemma (in measure_space) integral_minus_iff[simp]: + "integrable M (\<lambda>x. - f x) \<longleftrightarrow> integrable M f" +proof + assume "integrable M (\<lambda>x. - f x)" + then have "integrable M (\<lambda>x. - (- f x))" + by (rule integral_minus) + then show "integrable M f" by simp +qed (rule integral_minus) + lemma (in measure_space) integral_of_positive_diff: assumes integrable: "integrable M u" "integrable M v" and f_def: "\<And>x. f x = u x - v x" and pos: "\<And>x. 0 \<le> u x" "\<And>x. 0 \<le> v x" @@ -2181,6 +2197,58 @@ using assms unfolding lebesgue_integral_def by (subst (1 2) positive_integral_cong_AE) (auto simp add: extreal_real) +lemma (in finite_measure) lebesgue_integral_const[simp]: + shows "integrable M (\<lambda>x. a)" + and "(\<integral>x. a \<partial>M) = a * \<mu>' (space M)" +proof - + { fix a :: real assume "0 \<le> a" + then have "(\<integral>\<^isup>+ x. extreal a \<partial>M) = extreal a * \<mu> (space M)" + by (subst positive_integral_const) auto + moreover + from `0 \<le> a` have "(\<integral>\<^isup>+ x. extreal (-a) \<partial>M) = 0" + by (subst positive_integral_0_iff_AE) auto + ultimately have "integrable M (\<lambda>x. a)" by (auto simp: integrable_def) } + note * = this + show "integrable M (\<lambda>x. a)" + proof cases + assume "0 \<le> a" with * show ?thesis . + next + assume "\<not> 0 \<le> a" + then have "0 \<le> -a" by auto + from *[OF this] show ?thesis by simp + qed + show "(\<integral>x. a \<partial>M) = a * \<mu>' (space M)" + by (simp add: \<mu>'_def lebesgue_integral_def positive_integral_const_If) +qed + +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: "\<mu> (space M) \<noteq> 0" + shows "integral\<^isup>L M X < integral\<^isup>L M Y" +proof - + have "integral\<^isup>L M X \<le> integral\<^isup>L M Y" + using gt int by (intro integral_mono_AE) auto + moreover + have "integral\<^isup>L M X \<noteq> integral\<^isup>L M Y" + proof + from gt have "AE x. Y x - X x \<noteq> 0" + by auto + then have \<mu>: "\<mu> {x\<in>space M. Y x - X x \<noteq> 0} = \<mu> (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 (\<lambda>x. \<bar>Y x - X x\<bar>) = integral\<^isup>L M (\<lambda>x. Y x - X x)" + using gt by (intro integral_cong_AE) auto + also have "\<dots> = 0" + using eq int by simp + finally show False + using \<mu> int neq0 + by (subst (asm) integral_0_iff) auto + qed + ultimately show ?thesis by auto +qed + lemma (in measure_space) integral_dominated_convergence: 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" and w: "integrable M w"

--- a/src/HOL/Probability/Measure.thy Thu May 26 20:49:56 2011 +0200 +++ b/src/HOL/Probability/Measure.thy Thu May 26 20:51:03 2011 +0200 @@ -132,6 +132,10 @@ ultimately show "\<mu> a \<le> \<mu> b" by auto qed +lemma (in measure_space) measure_top: + "A \<in> sets M \<Longrightarrow> \<mu> A \<le> \<mu> (space M)" + using sets_into_space[of A] by (auto intro!: measure_mono) + lemma (in measure_space) measure_compl: assumes s: "s \<in> sets M" and fin: "\<mu> s \<noteq> \<infinity>" shows "\<mu> (space M - s) = \<mu> (space M) - \<mu> s" @@ -409,6 +413,22 @@ finally show ?thesis . qed +lemma (in measure_space) measure_subadditive_finite: + assumes "finite I" "\<And>i. i\<in>I \<Longrightarrow> A i \<in> sets M" + shows "\<mu> (\<Union>i\<in>I. A i) \<le> (\<Sum>i\<in>I. \<mu> (A i))" +using assms proof induct + case (insert i I) + then have "\<mu> (\<Union>i\<in>insert i I. A i) = \<mu> (A i \<union> (\<Union>i\<in>I. A i))" + by simp + also have "\<dots> \<le> \<mu> (A i) + \<mu> (\<Union>i\<in>I. A i)" + using insert by (intro measure_subadditive finite_UN) auto + also have "\<dots> \<le> \<mu> (A i) + (\<Sum>i\<in>I. \<mu> (A i))" + using insert by (intro add_mono) auto + also have "\<dots> = (\<Sum>i\<in>insert i I. \<mu> (A i))" + using insert by auto + finally show ?case . +qed simp + lemma (in measure_space) measure_eq_0: assumes "N \<in> sets M" and "\<mu> N = 0" and "K \<subseteq> N" and "K \<in> sets M" shows "\<mu> K = 0" @@ -724,6 +744,20 @@ and AE_conj_iff[simp]: "(AE x. P x \<and> Q x) \<longleftrightarrow> (AE x. P x) \<and> (AE x. Q x)" by auto +lemma (in measure_space) AE_measure: + assumes AE: "AE x. P x" and sets: "{x\<in>space M. P x} \<in> sets M" + shows "\<mu> {x\<in>space M. P x} = \<mu> (space M)" +proof - + from AE_E[OF AE] guess N . note N = this + with sets have "\<mu> (space M) \<le> \<mu> ({x\<in>space M. P x} \<union> N)" + by (intro measure_mono) auto + also have "\<dots> \<le> \<mu> {x\<in>space M. P x} + \<mu> N" + using sets N by (intro measure_subadditive) auto + also have "\<dots> = \<mu> {x\<in>space M. P x}" using N by simp + finally show "\<mu> {x\<in>space M. P x} = \<mu> (space M)" + using measure_top[OF sets] by auto +qed + lemma (in measure_space) AE_space: "AE x. x \<in> space M" by (rule AE_I[where N="{}"]) auto @@ -1168,7 +1202,7 @@ lemma (in finite_measure) finite_measure_eq: "A \<in> sets M \<Longrightarrow> \<mu> A = extreal (\<mu>' A)" by (auto simp: \<mu>'_def extreal_real) -lemma (in finite_measure) positive_measure': "0 \<le> \<mu>' A" +lemma (in finite_measure) positive_measure'[simp, intro]: "0 \<le> \<mu>' A" unfolding \<mu>'_def by (auto simp: real_of_extreal_pos) lemma (in finite_measure) bounded_measure: "\<mu>' A \<le> \<mu>' (space M)" @@ -1251,6 +1285,12 @@ using measure_subadditive[OF m] using m[THEN finite_measure_eq] Un[OF m, THEN finite_measure_eq] by simp +lemma (in finite_measure) finite_measure_subadditive_finite: + assumes "finite I" "\<And>i. i\<in>I \<Longrightarrow> A i \<in> sets M" + shows "\<mu>' (\<Union>i\<in>I. A i) \<le> (\<Sum>i\<in>I. \<mu>' (A i))" + using measure_subadditive_finite[OF assms] assms + by (simp add: finite_measure_eq finite_UN) + lemma (in finite_measure) finite_measure_countably_subadditive: assumes A: "range A \<subseteq> sets M" and sum: "summable (\<lambda>i. \<mu>' (A i))" shows "\<mu>' (\<Union>i. A i) \<le> (\<Sum>i. \<mu>' (A i))" @@ -1378,6 +1418,23 @@ using A finite_subset[OF A finite_space] by (intro finite_measure_finite_singleton) auto +lemma (in finite_measure_space) finite_measure_subadditive_setsum: + assumes "finite I" + shows "\<mu>' (\<Union>i\<in>I. A i) \<le> (\<Sum>i\<in>I. \<mu>' (A i))" +proof cases + assume "(\<Union>i\<in>I. A i) \<subseteq> space M" + then have "\<And>i. i\<in>I \<Longrightarrow> A i \<in> sets M" by auto + from finite_measure_subadditive_finite[OF `finite I` this] + show ?thesis by auto +next + assume "\<not> (\<Union>i\<in>I. A i) \<subseteq> space M" + then have "\<mu>' (\<Union>i\<in>I. A i) = 0" + by (simp add: \<mu>'_def) + also have "0 \<le> (\<Sum>i\<in>I. \<mu>' (A i))" + by (auto intro!: setsum_nonneg) + finally show ?thesis . +qed + lemma suminf_cmult_indicator: fixes f :: "nat \<Rightarrow> extreal" assumes "disjoint_family A" "x \<in> A i" "\<And>i. 0 \<le> f i"

--- a/src/HOL/Probability/Probability_Measure.thy Thu May 26 20:49:56 2011 +0200 +++ b/src/HOL/Probability/Probability_Measure.thy Thu May 26 20:51:03 2011 +0200 @@ -28,8 +28,6 @@ abbreviation (in prob_space) "joint_distribution X Y \<equiv> distribution (\<lambda>x. (X x, Y x))" -declare (in finite_measure) positive_measure'[intro, simp] - lemma (in prob_space) distribution_cong: assumes "\<And>x. x \<in> space M \<Longrightarrow> X x = Y x" shows "distribution X = distribution Y"