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