src/HOL/Probability/Lebesgue_Integration.thy
changeset 51000 c9adb50f74ad
parent 50384 b9b967da28e9
child 51340 5e6296afe08d
     1.1 --- a/src/HOL/Probability/Lebesgue_Integration.thy	Thu Jan 31 11:31:27 2013 +0100
     1.2 +++ b/src/HOL/Probability/Lebesgue_Integration.thy	Thu Jan 31 11:31:30 2013 +0100
     1.3 @@ -297,7 +297,7 @@
     1.4      qed
     1.5    next
     1.6      fix x show "(SUP i. ?g i x) = max 0 (u x)"
     1.7 -    proof (rule ereal_SUPI)
     1.8 +    proof (rule SUP_eqI)
     1.9        fix i show "?g i x \<le> max 0 (u x)" unfolding max_def f_def
    1.10          by (cases "u x") (auto simp: field_simps real_natfloor_le natfloor_neg
    1.11                                       mult_nonpos_nonneg mult_nonneg_nonneg)
    1.12 @@ -2147,7 +2147,7 @@
    1.13      assume neq_0: "(\<integral>\<^isup>+ x. max 0 (ereal (2 * w x)) \<partial>M) \<noteq> 0" (is "?wx \<noteq> 0")
    1.14      have "0 = limsup (\<lambda>n. 0 :: ereal)" by (simp add: Limsup_const)
    1.15      also have "\<dots> \<le> limsup (\<lambda>n. \<integral>\<^isup>+ x. ereal \<bar>u n x - u' x\<bar> \<partial>M)"
    1.16 -      by (intro limsup_mono positive_integral_positive)
    1.17 +      by (simp add: Limsup_mono  positive_integral_positive)
    1.18      finally have pos: "0 \<le> limsup (\<lambda>n. \<integral>\<^isup>+ x. ereal \<bar>u n x - u' x\<bar> \<partial>M)" .
    1.19      have "?wx = (\<integral>\<^isup>+ x. liminf (\<lambda>n. max 0 (ereal (?diff n x))) \<partial>M)"
    1.20        using u'
    1.21 @@ -2178,11 +2178,11 @@
    1.22    qed
    1.23  
    1.24    have "liminf ?f \<le> limsup ?f"
    1.25 -    by (intro ereal_Liminf_le_Limsup trivial_limit_sequentially)
    1.26 +    by (intro Liminf_le_Limsup trivial_limit_sequentially)
    1.27    moreover
    1.28    { have "0 = liminf (\<lambda>n. 0 :: ereal)" by (simp add: Liminf_const)
    1.29      also have "\<dots> \<le> liminf ?f"
    1.30 -      by (intro liminf_mono positive_integral_positive)
    1.31 +      by (simp add: Liminf_mono positive_integral_positive)
    1.32      finally have "0 \<le> liminf ?f" . }
    1.33    ultimately have liminf_limsup_eq: "liminf ?f = ereal 0" "limsup ?f = ereal 0"
    1.34      using `limsup ?f = 0` by auto