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