src/HOL/Series.thy
changeset 66447 a1f5c5c26fa6
parent 65680 378a2f11bec9
child 66456 621897f47fab
     1.1 --- a/src/HOL/Series.thy	Thu Aug 17 14:40:42 2017 +0200
     1.2 +++ b/src/HOL/Series.thy	Thu Aug 17 14:52:56 2017 +0200
     1.3 @@ -1107,7 +1107,7 @@
     1.4  qed
     1.5  
     1.6  lemma sums_mono_reindex:
     1.7 -  assumes subseq: "subseq g"
     1.8 +  assumes subseq: "strict_mono g"
     1.9      and zero: "\<And>n. n \<notin> range g \<Longrightarrow> f n = 0"
    1.10    shows "(\<lambda>n. f (g n)) sums c \<longleftrightarrow> f sums c"
    1.11    unfolding sums_def
    1.12 @@ -1117,10 +1117,10 @@
    1.13    proof
    1.14      fix n :: nat
    1.15      from subseq have "(\<Sum>k<n. f (g k)) = (\<Sum>k\<in>g`{..<n}. f k)"
    1.16 -      by (subst sum.reindex) (auto intro: subseq_imp_inj_on)
    1.17 +      by (subst sum.reindex) (auto intro: strict_mono_imp_inj_on)
    1.18      also from subseq have "\<dots> = (\<Sum>k<g n. f k)"
    1.19        by (intro sum.mono_neutral_left ballI zero)
    1.20 -        (auto dest: subseq_strict_mono simp: strict_mono_less strict_mono_less_eq)
    1.21 +        (auto simp: strict_mono_less strict_mono_less_eq)
    1.22      finally show "(\<Sum>k<n. f (g k)) = (\<Sum>k<g n. f k)" .
    1.23    qed
    1.24    also from LIMSEQ_subseq_LIMSEQ[OF lim subseq] have "\<dots> \<longlonglongrightarrow> c"
    1.25 @@ -1150,7 +1150,7 @@
    1.26          have "g l < g (g_inv n)"
    1.27            by (rule less_le_trans[OF _ g_inv]) (use k l in simp_all)
    1.28          with subseq have "l < g_inv n"
    1.29 -          by (simp add: subseq_strict_mono strict_mono_less)
    1.30 +          by (simp add: strict_mono_less)
    1.31          with k l show False
    1.32            by simp
    1.33        qed
    1.34 @@ -1160,7 +1160,7 @@
    1.35      with g_inv_least' g_inv have "(\<Sum>k<n. f k) = (\<Sum>k\<in>g`{..<g_inv n}. f k)"
    1.36        by (intro sum.mono_neutral_right) auto
    1.37      also from subseq have "\<dots> = (\<Sum>k<g_inv n. f (g k))"
    1.38 -      using subseq_imp_inj_on by (subst sum.reindex) simp_all
    1.39 +      using strict_mono_imp_inj_on by (subst sum.reindex) simp_all
    1.40      finally show "(\<Sum>k<n. f k) = (\<Sum>k<g_inv n. f (g k))" .
    1.41    qed
    1.42    also {
    1.43 @@ -1169,7 +1169,7 @@
    1.44      also have "n \<le> g (g_inv n)"
    1.45        by (rule g_inv)
    1.46      finally have "K \<le> g_inv n"
    1.47 -      using subseq by (simp add: strict_mono_less_eq subseq_strict_mono)
    1.48 +      using subseq by (simp add: strict_mono_less_eq)
    1.49    }
    1.50    then have "filterlim g_inv at_top sequentially"
    1.51      by (auto simp: filterlim_at_top eventually_at_top_linorder)
    1.52 @@ -1179,14 +1179,14 @@
    1.53  qed
    1.54  
    1.55  lemma summable_mono_reindex:
    1.56 -  assumes subseq: "subseq g"
    1.57 +  assumes subseq: "strict_mono g"
    1.58      and zero: "\<And>n. n \<notin> range g \<Longrightarrow> f n = 0"
    1.59    shows "summable (\<lambda>n. f (g n)) \<longleftrightarrow> summable f"
    1.60    using sums_mono_reindex[of g f, OF assms] by (simp add: summable_def)
    1.61  
    1.62  lemma suminf_mono_reindex:
    1.63    fixes f :: "nat \<Rightarrow> 'a::{t2_space,comm_monoid_add}"
    1.64 -  assumes "subseq g" "\<And>n. n \<notin> range g \<Longrightarrow> f n = 0"
    1.65 +  assumes "strict_mono g" "\<And>n. n \<notin> range g \<Longrightarrow> f n = 0"
    1.66    shows   "suminf (\<lambda>n. f (g n)) = suminf f"
    1.67  proof (cases "summable f")
    1.68    case True