src/HOL/Probability/Measure_Space.thy
 changeset 56193 c726ecfb22b6 parent 56154 f0a927235162 child 56212 3253aaf73a01
```     1.1 --- a/src/HOL/Probability/Measure_Space.thy	Tue Mar 18 14:32:23 2014 +0100
1.2 +++ b/src/HOL/Probability/Measure_Space.thy	Tue Mar 18 15:53:48 2014 +0100
1.3 @@ -16,7 +16,7 @@
1.4    "f sums x \<longleftrightarrow> (\<lambda>n. (\<Sum>i\<le>n. f i)) ----> x"
1.5    unfolding sums_def
1.6    apply (subst LIMSEQ_Suc_iff[symmetric])
1.7 -  unfolding atLeastLessThanSuc_atLeastAtMost atLeast0AtMost ..
1.8 +  unfolding lessThan_Suc_atMost ..
1.9
1.10  subsection "Relate extended reals and the indicator function"
1.11
1.12 @@ -304,12 +304,12 @@
1.13    with count_sum[THEN spec, of "disjointed A"] A(3)
1.14    have f_UN: "(\<Sum>i. f (disjointed A i)) = f (\<Union>i. A i)"
1.15      by (auto simp: UN_disjointed_eq disjoint_family_disjointed)
1.16 -  moreover have "(\<lambda>n. (\<Sum>i=0..<n. f (disjointed A i))) ----> (\<Sum>i. f (disjointed A i))"
1.17 +  moreover have "(\<lambda>n. (\<Sum>i<n. f (disjointed A i))) ----> (\<Sum>i. f (disjointed A i))"
1.18      using f(1)[unfolded positive_def] dA
1.19 -    by (auto intro!: summable_sumr_LIMSEQ_suminf summable_ereal_pos)
1.20 +    by (auto intro!: summable_LIMSEQ summable_ereal_pos)
1.21    from LIMSEQ_Suc[OF this]
1.22    have "(\<lambda>n. (\<Sum>i\<le>n. f (disjointed A i))) ----> (\<Sum>i. f (disjointed A i))"
1.23 -    unfolding atLeastLessThanSuc_atLeastAtMost atLeast0AtMost .
1.24 +    unfolding lessThan_Suc_atMost .
1.25    moreover have "\<And>n. (\<Sum>i\<le>n. f (disjointed A i)) = f (A n)"
1.26      using disjointed_additive[OF f A(1,2)] .
1.27    ultimately show "(\<lambda>i. f (A i)) ----> f (\<Union>i. A i)" by simp
```