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