# HG changeset patch
# User hoelzl
# Date 1306435863 -7200
# Node ID 3fa22920bf86e8faf226bfebbd92fd179454d5ec
# Parent  3706951a6421cfe9ca22ff8483252dc57d4f25c5
integral strong monotone; finite subadditivity for measure

diff -r 3706951a6421 -r 3fa22920bf86 src/HOL/Probability/Lebesgue_Integration.thy
--- 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"
diff -r 3706951a6421 -r 3fa22920bf86 src/HOL/Probability/Measure.thy
--- 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"
diff -r 3706951a6421 -r 3fa22920bf86 src/HOL/Probability/Probability_Measure.thy
--- 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"