298 unfolding o_def |
298 unfolding o_def |
299 using tendsto_compose_filtermap finite_subsets2 limA tendsto_mono |
299 using tendsto_compose_filtermap finite_subsets2 limA tendsto_mono |
300 \<open>(\<lambda>F. sum f (F \<inter> A)) = sum f \<circ> (\<lambda>F. F \<inter> A)\<close> by fastforce |
300 \<open>(\<lambda>F. sum f (F \<inter> A)) = sum f \<circ> (\<lambda>F. F \<inter> A)\<close> by fastforce |
301 qed |
301 qed |
302 |
302 |
303 with limB have "((\<lambda>F. sum f F - sum f (F\<inter>A)) \<longlongrightarrow> b - a) (finite_subsets_at_top B)" |
303 with limB have \<section>: "((\<lambda>F. sum f F - sum f (F\<inter>A)) \<longlongrightarrow> b - a) (finite_subsets_at_top B)" |
304 using tendsto_diff by blast |
304 using tendsto_diff by blast |
305 have "sum f X - sum f (X \<inter> A) = sum f (X - A)" if "finite X" and "X \<subseteq> B" for X :: "'a set" |
305 have "sum f X - sum f (X \<inter> A) = sum f (X - A)" if "finite X" and "X \<subseteq> B" for X :: "'a set" |
306 using that by (metis add_diff_cancel_left' sum.Int_Diff) |
306 using that by (metis add_diff_cancel_left' sum.Int_Diff) |
307 hence "\<forall>\<^sub>F x in finite_subsets_at_top B. sum f x - sum f (x \<inter> A) = sum f (x - A)" |
307 hence "\<forall>\<^sub>F x in finite_subsets_at_top B. sum f x - sum f (x \<inter> A) = sum f (x - A)" |
308 by (rule eventually_finite_subsets_at_top_weakI) |
308 by (rule eventually_finite_subsets_at_top_weakI) |
309 hence "((\<lambda>F. sum f (F-A)) \<longlongrightarrow> b - a) (finite_subsets_at_top B)" |
309 hence "((\<lambda>F. sum f (F-A)) \<longlongrightarrow> b - a) (finite_subsets_at_top B)" |
310 using tendsto_cong [THEN iffD1 , rotated] |
310 using \<section> tendsto_cong by fastforce |
311 \<open>((\<lambda>F. sum f F - sum f (F \<inter> A)) \<longlongrightarrow> b - a) (finite_subsets_at_top B)\<close> by fastforce |
|
312 hence "(sum f \<longlongrightarrow> b - a) (filtermap (\<lambda>F. F-A) (finite_subsets_at_top B))" |
311 hence "(sum f \<longlongrightarrow> b - a) (filtermap (\<lambda>F. F-A) (finite_subsets_at_top B))" |
313 by (subst tendsto_compose_filtermap[symmetric], simp add: o_def) |
312 by (subst tendsto_compose_filtermap[symmetric], simp add: o_def) |
314 thus ?thesis |
313 thus ?thesis |
315 using finite_subsets1 has_sum_def tendsto_mono by blast |
314 using finite_subsets1 has_sum_def tendsto_mono by blast |
316 qed |
315 qed |
427 fixes f :: "'a \<Rightarrow> 'b :: {ordered_ab_group_add, topological_ab_group_add, linorder_topology}" |
426 fixes f :: "'a \<Rightarrow> 'b :: {ordered_ab_group_add, topological_ab_group_add, linorder_topology}" |
428 assumes \<open>(f has_sum a) A\<close> and "(g has_sum b) A" |
427 assumes \<open>(f has_sum a) A\<close> and "(g has_sum b) A" |
429 assumes \<open>\<And>x. x \<in> A \<Longrightarrow> f x \<le> g x\<close> |
428 assumes \<open>\<And>x. x \<in> A \<Longrightarrow> f x \<le> g x\<close> |
430 assumes \<open>x \<in> A\<close> \<open>f x < g x\<close> |
429 assumes \<open>x \<in> A\<close> \<open>f x < g x\<close> |
431 shows "a < b" |
430 shows "a < b" |
432 by (rule has_sum_strict_mono_neutral[OF assms(1,2), where x = x]) |
431 using assms has_sum_strict_mono_neutral by force |
433 (use assms(3-) in auto) |
|
434 |
432 |
435 lemma has_sum_finite_approximation: |
433 lemma has_sum_finite_approximation: |
436 fixes f :: "'a \<Rightarrow> 'b::{comm_monoid_add,metric_space}" |
434 fixes f :: "'a \<Rightarrow> 'b::{comm_monoid_add,metric_space}" |
437 assumes "(f has_sum x) A" and "\<epsilon> > 0" |
435 assumes "(f has_sum x) A" and "\<epsilon> > 0" |
438 shows "\<exists>F. finite F \<and> F \<subseteq> A \<and> dist (sum f F) x \<le> \<epsilon>" |
436 shows "\<exists>F. finite F \<and> F \<subseteq> A \<and> dist (sum f F) x \<le> \<epsilon>" |