equal
deleted
inserted
replaced
82 lemma summable_cong: |
82 lemma summable_cong: |
83 assumes "eventually (\<lambda>x. f x = (g x :: 'a :: real_normed_vector)) sequentially" |
83 assumes "eventually (\<lambda>x. f x = (g x :: 'a :: real_normed_vector)) sequentially" |
84 shows "summable f = summable g" |
84 shows "summable f = summable g" |
85 proof - |
85 proof - |
86 from assms obtain N where N: "\<forall>n\<ge>N. f n = g n" by (auto simp: eventually_at_top_linorder) |
86 from assms obtain N where N: "\<forall>n\<ge>N. f n = g n" by (auto simp: eventually_at_top_linorder) |
87 def C \<equiv> "(\<Sum>k<N. f k - g k)" |
87 define C where "C = (\<Sum>k<N. f k - g k)" |
88 from eventually_ge_at_top[of N] |
88 from eventually_ge_at_top[of N] |
89 have "eventually (\<lambda>n. setsum f {..<n} = C + setsum g {..<n}) sequentially" |
89 have "eventually (\<lambda>n. setsum f {..<n} = C + setsum g {..<n}) sequentially" |
90 proof eventually_elim |
90 proof eventually_elim |
91 fix n assume n: "n \<ge> N" |
91 fix n assume n: "n \<ge> N" |
92 from n have "{..<n} = {..<N} \<union> {N..<n}" by auto |
92 from n have "{..<n} = {..<N} \<union> {N..<n}" by auto |
1046 qed |
1046 qed |
1047 also from LIMSEQ_subseq_LIMSEQ[OF lim subseq] have "\<dots> \<longlonglongrightarrow> c" unfolding o_def . |
1047 also from LIMSEQ_subseq_LIMSEQ[OF lim subseq] have "\<dots> \<longlonglongrightarrow> c" unfolding o_def . |
1048 finally show "(\<lambda>n. \<Sum>k<n. f (g k)) \<longlonglongrightarrow> c" . |
1048 finally show "(\<lambda>n. \<Sum>k<n. f (g k)) \<longlonglongrightarrow> c" . |
1049 next |
1049 next |
1050 assume lim: "(\<lambda>n. \<Sum>k<n. f (g k)) \<longlonglongrightarrow> c" |
1050 assume lim: "(\<lambda>n. \<Sum>k<n. f (g k)) \<longlonglongrightarrow> c" |
1051 def g_inv \<equiv> "\<lambda>n. LEAST m. g m \<ge> n" |
1051 define g_inv where "g_inv n = (LEAST m. g m \<ge> n)" for n |
1052 from filterlim_subseq[OF subseq] have g_inv_ex: "\<exists>m. g m \<ge> n" for n |
1052 from filterlim_subseq[OF subseq] have g_inv_ex: "\<exists>m. g m \<ge> n" for n |
1053 by (auto simp: filterlim_at_top eventually_at_top_linorder) |
1053 by (auto simp: filterlim_at_top eventually_at_top_linorder) |
1054 hence g_inv: "g (g_inv n) \<ge> n" for n unfolding g_inv_def by (rule LeastI_ex) |
1054 hence g_inv: "g (g_inv n) \<ge> n" for n unfolding g_inv_def by (rule LeastI_ex) |
1055 have g_inv_least: "m \<ge> g_inv n" if "g m \<ge> n" for m n using that |
1055 have g_inv_least: "m \<ge> g_inv n" if "g m \<ge> n" for m n using that |
1056 unfolding g_inv_def by (rule Least_le) |
1056 unfolding g_inv_def by (rule Least_le) |