--- 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"