author kuncar Fri, 11 Apr 2014 17:53:16 +0200 changeset 56539 1fd920a86173 parent 56538 7c3b6b799b94 (current diff) parent 56537 01caba82e1d2 (diff) child 56540 8267d1ff646f child 56541 0e3abadbef39 child 56546 902960859c66
merged
```--- a/src/HOL/Library/Extended_Real.thy	Fri Apr 11 16:59:42 2014 +0200
+++ b/src/HOL/Library/Extended_Real.thy	Fri Apr 11 17:53:16 2014 +0200
@@ -536,7 +536,7 @@
lemma incseq_ereal: "incseq f \<Longrightarrow> incseq (\<lambda>x. ereal (f x))"
unfolding incseq_def by auto

fixes a b :: ereal
shows "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a + b"
using add_mono[of 0 a 0 b] by simp```
```--- a/src/HOL/Probability/Lebesgue_Integration.thy	Fri Apr 11 16:59:42 2014 +0200
+++ b/src/HOL/Probability/Lebesgue_Integration.thy	Fri Apr 11 17:53:16 2014 +0200
@@ -1114,7 +1114,7 @@
proof (rule SUP_simple_integral_sequences[OF l(3,6,2)])
show "incseq ?L'" "\<And>i x. 0 \<le> ?L' i x" "\<And>i. simple_function M (?L' i)"
using u v  `0 \<le> a` unfolding incseq_Suc_iff le_fun_def
-      by (auto intro!: add_mono ereal_mult_left_mono ereal_add_nonneg_nonneg)
+      by (auto intro!: add_mono ereal_mult_left_mono)
{ fix x
{ fix i have "a * u i x \<noteq> -\<infinity>" "v i x \<noteq> -\<infinity>" "u i x \<noteq> -\<infinity>" using `0 \<le> a` u(6)[of i x] v(6)[of i x]
by auto }
@@ -1122,10 +1122,10 @@
using `0 \<le> a` u(3) v(3) u(6)[of _ x] v(6)[of _ x]
by (subst SUP_ereal_cmult [symmetric, OF u(6) `0 \<le> a`])
-                 simp: incseq_Suc_iff le_fun_def add_mono ereal_mult_left_mono ereal_add_nonneg_nonneg) }
+                 simp: incseq_Suc_iff le_fun_def add_mono ereal_mult_left_mono) }
then show "AE x in M. (SUP i. l i x) = (SUP i. ?L' i x)"
unfolding l(5) using `0 \<le> a` u(5) v(5) l(5) f(2) g(2)
-      by (intro AE_I2) (auto split: split_max simp add: ereal_add_nonneg_nonneg)
+      by (intro AE_I2) (auto split: split_max)
qed
also have "\<dots> = (SUP i. a * integral\<^sup>S M (u i) + integral\<^sup>S M (v i))"
using u(2, 6) v(2, 6) `0 \<le> a` by (auto intro!: arg_cong[where f="SUPREMUM UNIV"] ext)
@@ -1182,7 +1182,7 @@
shows "(\<integral>\<^sup>+ x. f x + g x \<partial>M) = integral\<^sup>P M f + integral\<^sup>P M g"
proof -
have ae: "AE x in M. max 0 (f x) + max 0 (g x) = max 0 (f x + g x)"
-    using assms by (auto split: split_max simp: ereal_add_nonneg_nonneg)
+    using assms by (auto split: split_max)
have "(\<integral>\<^sup>+ x. f x + g x \<partial>M) = (\<integral>\<^sup>+ x. max 0 (f x + g x) \<partial>M)"
by (simp add: positive_integral_max_0)
also have "\<dots> = (\<integral>\<^sup>+ x. max 0 (f x) + max 0 (g x) \<partial>M)"```
```--- a/src/HOL/Probability/Radon_Nikodym.thy	Fri Apr 11 16:59:42 2014 +0200
+++ b/src/HOL/Probability/Radon_Nikodym.thy	Fri Apr 11 17:53:16 2014 +0200
@@ -483,8 +483,7 @@
using f_le_v N.emeasure_eq_measure[of A] positive_integral_positive[of M "?F A"]
by (cases "\<integral>\<^sup>+x. ?F A x \<partial>M", cases "N A") auto
finally have "(\<integral>\<^sup>+x. ?f0 x * indicator A x \<partial>M) \<le> N A" . }
-    hence "?f0 \<in> G" using `A0 \<in> sets M` b `f \<in> G`
-      by (auto intro!: ereal_add_nonneg_nonneg simp: G_def)
+    hence "?f0 \<in> G" using `A0 \<in> sets M` b `f \<in> G` by (auto simp: G_def)
have int_f_finite: "integral\<^sup>P M f \<noteq> \<infinity>"
by (metis N.emeasure_finite ereal_infty_less_eq2(1) int_f_eq_y y_le)
have  "0 < ?M (space M) - emeasure ?Mb (space M)"```