src/HOL/Probability/Lebesgue_Integration.thy
changeset 44568 e6f291cb5810
parent 43941 481566bc20e4
child 44666 8670a39d4420
     1.1 --- a/src/HOL/Probability/Lebesgue_Integration.thy	Sat Aug 27 17:26:14 2011 +0200
     1.2 +++ b/src/HOL/Probability/Lebesgue_Integration.thy	Sun Aug 28 09:20:12 2011 -0700
     1.3 @@ -2191,9 +2191,9 @@
     1.4    have 3: "\<And>x n. 0 \<le> f n x - f 0 x" using `mono f`
     1.5        unfolding mono_def le_fun_def by (auto simp: field_simps)
     1.6    have 4: "\<And>x. (\<lambda>i. f i x - f 0 x) ----> u x - f 0 x"
     1.7 -    using lim by (auto intro!: LIMSEQ_diff)
     1.8 +    using lim by (auto intro!: tendsto_diff)
     1.9    have 5: "(\<lambda>i. (\<integral>x. f i x - f 0 x \<partial>M)) ----> x - integral\<^isup>L M (f 0)"
    1.10 -    using f ilim by (auto intro!: LIMSEQ_diff simp: integral_diff)
    1.11 +    using f ilim by (auto intro!: tendsto_diff simp: integral_diff)
    1.12    note diff = integral_monotone_convergence_pos[OF 1 2 3 4 5]
    1.13    have "integrable M (\<lambda>x. (u x - f 0 x) + f 0 x)"
    1.14      using diff(1) f by (rule integral_add(1))
    1.15 @@ -2329,7 +2329,7 @@
    1.16    and "(\<lambda>i. integral\<^isup>L M (u i)) ----> integral\<^isup>L M u'" (is ?lim)
    1.17  proof -
    1.18    { fix x j assume x: "x \<in> space M"
    1.19 -    from u'[OF x] have "(\<lambda>i. \<bar>u i x\<bar>) ----> \<bar>u' x\<bar>" by (rule LIMSEQ_imp_rabs)
    1.20 +    from u'[OF x] have "(\<lambda>i. \<bar>u i x\<bar>) ----> \<bar>u' x\<bar>" by (rule tendsto_rabs)
    1.21      from LIMSEQ_le_const2[OF this]
    1.22      have "\<bar>u' x\<bar> \<le> w x" using bound[OF x] by auto }
    1.23    note u'_bound = this
    1.24 @@ -2400,7 +2400,7 @@
    1.25          unfolding ereal_max_0
    1.26        proof (rule lim_imp_Liminf[symmetric], unfold lim_ereal)
    1.27          have "(\<lambda>i. ?diff i x) ----> 2 * w x - \<bar>u' x - u' x\<bar>"
    1.28 -          using u'[OF x] by (safe intro!: LIMSEQ_diff LIMSEQ_const LIMSEQ_imp_rabs)
    1.29 +          using u'[OF x] by (safe intro!: tendsto_intros)
    1.30          then show "(\<lambda>i. max 0 (?diff i x)) ----> max 0 (2 * w x)"
    1.31            by (auto intro!: tendsto_real_max simp add: lim_ereal)
    1.32        qed (rule trivial_limit_sequentially)
    1.33 @@ -2492,7 +2492,7 @@
    1.34      show "mono ?w'"
    1.35        by (auto simp: mono_def le_fun_def intro!: setsum_mono2)
    1.36      { fix x show "(\<lambda>n. ?w' n x) ----> ?w x"
    1.37 -        using w by (cases "x \<in> space M") (simp_all add: LIMSEQ_const sums_def) }
    1.38 +        using w by (cases "x \<in> space M") (simp_all add: tendsto_const sums_def) }
    1.39      have *: "\<And>n. integral\<^isup>L M (?w' n) = (\<Sum>i = 0..< n. (\<integral>x. \<bar>f i x\<bar> \<partial>M))"
    1.40        using borel by (simp add: integral_setsum integrable_abs cong: integral_cong)
    1.41      from abs_sum