Quelle Infinite_Sum.thy Sprache: Isabelle

(*
  Title:    HOL/Analysis/Infinite_Sum.thy
  Author:   Dominique Unruh, University of Tartu
            Manuel Eberl, University of Innsbruck

  A theory of sums over possibly infinite sets.
*)

section \<open>Infinite sums\<close>
\<^latex>\<open>\label{section:Infinite_Sum}\<close>

text \<open>In this theory, we introduce the definition of infinite sums, i.e., sums ranging over an
infinite, potentially uncountable index set with no particular ordering.
(This is different from series. Those are sums indexed by natural numbers,
and the order of the index set matters.)

Our definition is quite standard: $s:=\sum_{x\in A} f(x)$ is the limit of finite sums $s_F:=\sum_{x\in F} f(x)$ for increasing $F$.
That is, $s$ is the limit of the net $s_F$ where $F$ are finite subsets of $A$ ordered by inclusion.
We believe that this is the standard definition for such sums.
See, e.g., Definition 4.11 in \<^cite>\<open>"conway2013course"\<close>.
This definition is quite general: it is well-defined whenever $f$ takes values in some
commutative monoid endowed with a Hausdorff topology.
(Examples are reals, complex numbers, normed vector spaces, and more.)\<close>

theory Infinite_Sum
  imports
    Elementary_Topology
    "HOL-Library.Extended_Nonnegative_Real"
    "HOL-Library.Complex_Order"
    "HOL-Computational_Algebra.Formal_Power_Series"
begin

subsection \<open>Definition and syntax\<close>

definition HAS_SUM :: \<open>('a \<Rightarrow> 'b :: {comm_monoid_add, topological_space}) \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> bool\<close>
    where has_sum_def: \<open>HAS_SUM f A x \<equiv> (sum f \<longlongrightarrow> x) (finite_subsets_at_top A)\<close>

abbreviation has_sum (infixr \<open>has'_sum\<close> 46) where
  "(f has_sum S) A \ HAS_SUM f A S"

definition summable_on :: "('a \ 'b::{comm_monoid_add, topological_space}) \ 'a set \ bool" (infixr \summable'_on\ 46) where
  "f summable_on A \ (\x. (f has_sum x) A)"

definition infsum :: "('a \ 'b::{comm_monoid_add,t2_space}) \ 'a set \ 'b" where
  "infsum f A = (if f summable_on A then Lim (finite_subsets_at_top A) (sum f) else 0)"

abbreviation abs_summable_on :: "('a \ 'b::real_normed_vector) \ 'a set \ bool" (infixr \abs'_summable'_on\ 46) where
  "f abs_summable_on A \ (\x. norm (f x)) summable_on A"

syntax (ASCII)
  "_infsum" :: "pttrn \ 'a set \ 'b \ 'b::topological_comm_monoid_add"
    (\<open>(\<open>indent=3 notation=\<open>binder INFSUM\<close>\<close>INFSUM (_/:_)./ _)\<close> [0, 51, 10] 10)
syntax
  "_infsum" :: "pttrn \ 'a set \ 'b \ 'b::topological_comm_monoid_add"
    (\<open>(\<open>indent=2 notation=\<open>binder \<Sum>\<^sub>\<infinity>\<close>\<close>\<Sum>\<^sub>\<infinity>(_/\<in>_)./ _)\<close> [0, 51, 10] 10)
syntax_consts
  "_infsum" \<rightleftharpoons> infsum
translations \<comment> \<open>Beware of argument permutation!\<close>
  "\\<^sub>\i\A. b" \ "CONST infsum (\i. b) A"

syntax (ASCII)
  "_univinfsum" :: "pttrn \ 'a \ 'a" (\(\indent=3 notation=\binder INFSUM\\INFSUM _./ _)\ [0, 10] 10)
syntax
  "_univinfsum" :: "pttrn \ 'a \ 'a" (\(\indent=2 notation=\binder \\<^sub>\\\\\<^sub>\_./ _)\ [0, 10] 10)
syntax_consts
  "_univinfsum" \<rightleftharpoons> infsum
translations
  "\\<^sub>\x. t" \ "CONST infsum (\x. t) (CONST UNIV)"

syntax (ASCII)
  "_qinfsum" :: "pttrn \ bool \ 'a \ 'a" (\(\indent=3 notation=\binder INFSUM\\INFSUM _ |/ _./ _)\ [0, 0, 10] 10)
syntax
  "_qinfsum" :: "pttrn \ bool \ 'a \ 'a" (\(\indent=2 notation=\binder \\<^sub>\\\\\<^sub>\_ | (_)./ _)\ [0, 0, 10] 10)
syntax_consts
  "_qinfsum" \<rightleftharpoons> infsum
translations
  "\\<^sub>\x|P. t" => "CONST infsum (\x. t) {x. P}"
print_translation \<open>
  [(\<^const_syntax>\<open>infsum\<close>, K (Collect_binder_tr' \<^syntax_const>\<open>_qinfsum\<close>))]
\<close>

subsection \<open>General properties\<close>

lemma infsumI:
  fixes f g :: \<open>'a \<Rightarrow> 'b::{comm_monoid_add, t2_space}\<close>
  assumes \<open>(f has_sum x) A\<close>
  shows \<open>infsum f A = x\<close>
  by (metis assms finite_subsets_at_top_neq_bot infsum_def summable_on_def has_sum_def tendsto_Lim)

lemma infsum_eqI:
  fixes f g :: \<open>'a \<Rightarrow> 'b::{comm_monoid_add, t2_space}\<close>
  assumes \<open>x = y\<close>
  assumes \<open>(f has_sum x) A\<close>
  assumes \<open>(g has_sum y) B\<close>
  shows \<open>infsum f A = infsum g B\<close>
  using assms infsumI by blast

lemma infsum_eqI':
  fixes f g :: \<open>'a \<Rightarrow> 'b::{comm_monoid_add, t2_space}\<close>
  assumes \<open>\<And>x. (f has_sum x) A \<longleftrightarrow> (g has_sum x) B\<close>
  shows \<open>infsum f A = infsum g B\<close>
  by (metis assms infsum_def infsum_eqI summable_on_def)

lemma infsum_not_exists:
  fixes f :: \<open>'a \<Rightarrow> 'b::{comm_monoid_add, t2_space}\<close>
  assumes \<open>\<not> f summable_on A\<close>
  shows \<open>infsum f A = 0\<close>
  by (simp add: assms infsum_def)

lemma has_sum_unique:
  fixes f :: "_ \ 'a :: {topological_comm_monoid_add, t2_space}"
  assumes "(f has_sum x) A" "(f has_sum y) A"
  shows "x = y"
  using assms infsumI by blast

lemma summable_iff_has_sum_infsum: "f summable_on A \ (f has_sum (infsum f A)) A"
  using infsumI summable_on_def by blast

lemma has_sum_iff: "(f has_sum S) A \ f summable_on A \ infsum f A = S"
  using infsumI summable_iff_has_sum_infsum by blast

lemma has_sum_infsum[simp]:
  assumes \<open>f summable_on S\<close>
  shows \<open>(f has_sum (infsum f S)) S\<close>
  using assms summable_iff_has_sum_infsum by blast

lemma has_sum_cong_neutral:
  fixes f g :: \<open>'a \<Rightarrow> 'b::{comm_monoid_add, topological_space}\<close>
  assumes \<open>\<And>x. x\<in>T-S \<Longrightarrow> g x = 0\<close>
  assumes \<open>\<And>x. x\<in>S-T \<Longrightarrow> f x = 0\<close>
  assumes \<open>\<And>x. x\<in>S\<inter>T \<Longrightarrow> f x = g x\<close>
  shows "(f has_sum x) S \ (g has_sum x) T"
proof -
  have \<open>eventually P (filtermap (sum f) (finite_subsets_at_top S))
      = eventually P (filtermap (sum g) (finite_subsets_at_top T))\<close> for P
  proof
    assume \<open>eventually P (filtermap (sum f) (finite_subsets_at_top S))\<close>
    then obtain F0 where \<open>finite F0\<close> and \<open>F0 \<subseteq> S\<close> and F0_P: \<open>\<And>F. finite F \<Longrightarrow> F \<subseteq> S \<Longrightarrow> F \<supseteq> F0 \<Longrightarrow> P (sum f F)\<close>
      by (metis (no_types, lifting) eventually_filtermap eventually_finite_subsets_at_top)
    define F0' where \F0' = F0 \ T\
    have [simp]: \<open>finite F0'\<close> \<open>F0' \<subseteq> T\<close>
      by (simp_all add: F0'_def \finite F0\)
    have \<open>P (sum g F)\<close> if \<open>finite F\<close> \<open>F \<subseteq> T\<close> \<open>F \<supseteq> F0'\<close> for F
    proof -
      have \<open>P (sum f ((F\<inter>S) \<union> (F0\<inter>S)))\<close>
        by (intro F0_P) (use \<open>F0 \<subseteq> S\<close> \<open>finite F0\<close> that in auto)
      also have \<open>sum f ((F\<inter>S) \<union> (F0\<inter>S)) = sum g F\<close>
        by (intro sum.mono_neutral_cong) (use that \<open>finite F0\<close> F0'_def assms in auto)
      finally show ?thesis .
    qed
    with \<open>F0' \<subseteq> T\<close> \<open>finite F0'\<close> show \<open>eventually P (filtermap (sum g) (finite_subsets_at_top T))\<close>
      by (metis (no_types, lifting) eventually_filtermap eventually_finite_subsets_at_top)
  next
    assume \<open>eventually P (filtermap (sum g) (finite_subsets_at_top T))\<close>
    then obtain F0 where \<open>finite F0\<close> and \<open>F0 \<subseteq> T\<close> and F0_P: \<open>\<And>F. finite F \<Longrightarrow> F \<subseteq> T \<Longrightarrow> F \<supseteq> F0 \<Longrightarrow> P (sum g F)\<close>
      by (metis (no_types, lifting) eventually_filtermap eventually_finite_subsets_at_top)
    define F0' where \F0' = F0 \ S\
    have [simp]: \<open>finite F0'\<close> \<open>F0' \<subseteq> S\<close>
      by (simp_all add: F0'_def \finite F0\)
    have \<open>P (sum f F)\<close> if \<open>finite F\<close> \<open>F \<subseteq> S\<close> \<open>F \<supseteq> F0'\<close> for F
    proof -
      have \<open>P (sum g ((F\<inter>T) \<union> (F0\<inter>T)))\<close>
        by (intro F0_P) (use \<open>F0 \<subseteq> T\<close> \<open>finite F0\<close> that in auto)
      also have \<open>sum g ((F\<inter>T) \<union> (F0\<inter>T)) = sum f F\<close>
        by (intro sum.mono_neutral_cong) (use that \<open>finite F0\<close> F0'_def assms in auto)
      finally show ?thesis .
    qed
    with \<open>F0' \<subseteq> S\<close> \<open>finite F0'\<close> show \<open>eventually P (filtermap (sum f) (finite_subsets_at_top S))\<close>
      by (metis (no_types, lifting) eventually_filtermap eventually_finite_subsets_at_top)
  qed

  then have tendsto_x: "(sum f \ x) (finite_subsets_at_top S) \ (sum g \ x) (finite_subsets_at_top T)" for x
    by (simp add: le_filter_def filterlim_def)

  then show ?thesis
    by (simp add: has_sum_def)
qed

lemma summable_on_cong_neutral:
  fixes f g :: \<open>'a \<Rightarrow> 'b::{comm_monoid_add, topological_space}\<close>
  assumes \<open>\<And>x. x\<in>T-S \<Longrightarrow> g x = 0\<close>
  assumes \<open>\<And>x. x\<in>S-T \<Longrightarrow> f x = 0\<close>
  assumes \<open>\<And>x. x\<in>S\<inter>T \<Longrightarrow> f x = g x\<close>
  shows "f summable_on S \ g summable_on T"
  using has_sum_cong_neutral[of T S g f, OF assms]
  by (simp add: summable_on_def)

lemma infsum_cong_neutral:
  fixes f g :: \<open>'a \<Rightarrow> 'b::{comm_monoid_add, t2_space}\<close>
  assumes \<open>\<And>x. x\<in>T-S \<Longrightarrow> g x = 0\<close>
  assumes \<open>\<And>x. x\<in>S-T \<Longrightarrow> f x = 0\<close>
  assumes \<open>\<And>x. x\<in>S\<inter>T \<Longrightarrow> f x = g x\<close>
  shows \<open>infsum f S = infsum g T\<close>
  by (smt (verit, best) assms has_sum_cong_neutral infsum_eqI')

lemma has_sum_cong:
  assumes "\x. x\A \ f x = g x"
  shows "(f has_sum x) A \ (g has_sum x) A"
  using assms by (intro has_sum_cong_neutral) auto

lemma summable_on_cong:
  assumes "\x. x\A \ f x = g x"
  shows "f summable_on A \ g summable_on A"
  by (metis assms summable_on_def has_sum_cong)

lemma infsum_cong:
  assumes "\x. x\A \ f x = g x"
  shows "infsum f A = infsum g A"
  using assms infsum_eqI' has_sum_cong by blast

lemma summable_on_cofin_subset:
  fixes f :: "'a \ 'b::topological_ab_group_add"
  assumes "f summable_on A" and [simp]: "finite F"
  shows "f summable_on (A - F)"
proof -
  from assms(1) obtain x where lim_f: "(sum f \ x) (finite_subsets_at_top A)"
    unfolding summable_on_def has_sum_def by auto
  define F' where "F' = F\<inter>A"
  with assms have "finite F'" and "A-F = A-F'"
    by auto
  have "filtermap ((\)F') (finite_subsets_at_top (A-F))
      \<le> finite_subsets_at_top A"
  proof (rule filter_leI)
    fix P assume "eventually P (finite_subsets_at_top A)"
    then obtain X where [simp]: "finite X" and XA: "X \ A"
      and P: "\Y. finite Y \ X \ Y \ Y \ A \ P Y"
      unfolding eventually_finite_subsets_at_top by auto
    define X' where "X' = X-F"
    hence [simp]: "finite X'" and [simp]: "X' \ A-F"
      using XA by auto
    hence "finite Y \ X' \ Y \ Y \ A - F \ P (F' \ Y)" for Y
      using P XA unfolding X'_def using F'_def \<open>finite F'\<close> by blast
    thus "eventually P (filtermap ((\) F') (finite_subsets_at_top (A - F)))"
      unfolding eventually_filtermap eventually_finite_subsets_at_top
      by (rule_tac x=X' in exI, simp)
  qed
  with lim_f have "(sum f \ x) (filtermap ((\)F') (finite_subsets_at_top (A-F)))"
    using tendsto_mono by blast
  have "((\G. sum f (F' \ G)) \ x) (finite_subsets_at_top (A - F))"
    if "((sum f \ (\) F') \ x) (finite_subsets_at_top (A - F))"
    using that unfolding o_def by auto
  hence "((\G. sum f (F' \ G)) \ x) (finite_subsets_at_top (A-F))"
    using tendsto_compose_filtermap [symmetric]
    by (simp add: \<open>(sum f \<longlongrightarrow> x) (filtermap ((\<union>) F') (finite_subsets_at_top (A - F)))\<close>
        tendsto_compose_filtermap)
  have "\Y. finite Y \ Y \ A - F \ sum f (F' \ Y) = sum f F' + sum f Y"
    by (metis Diff_disjoint Int_Diff \<open>A - F = A - F'\<close> \<open>finite F'\<close> inf.orderE sum.union_disjoint)
  hence "\\<^sub>F x in finite_subsets_at_top (A - F). sum f (F' \ x) = sum f F' + sum f x"
    unfolding eventually_finite_subsets_at_top
    using exI [where x = "{}"]
    by (simp add: \<open>\<And>P. P {} \<Longrightarrow> \<exists>x. P x\<close>)
  hence "((\G. sum f F' + sum f G) \ x) (finite_subsets_at_top (A-F))"
    using tendsto_cong [THEN iffD1 , rotated]
      \<open>((\<lambda>G. sum f (F' \<union> G)) \<longlongrightarrow> x) (finite_subsets_at_top (A - F))\<close> by fastforce
  hence "((\G. sum f F' + sum f G) \ sum f F' + (x-sum f F')) (finite_subsets_at_top (A-F))"
    by simp
  hence "(sum f \ x - sum f F') (finite_subsets_at_top (A-F))"
    using tendsto_add_const_iff by blast
  thus "f summable_on (A - F)"
    unfolding summable_on_def has_sum_def by auto
qed

lemma
  fixes f :: "'a \ 'b::{topological_ab_group_add}"
  assumes \<open>(f has_sum b) B\<close> and \<open>(f has_sum a) A\<close> and AB: "A \<subseteq> B"
  shows has_sum_Diff: "(f has_sum (b - a)) (B - A)"
proof -
  have finite_subsets1:
    "finite_subsets_at_top (B - A) \ filtermap (\F. F - A) (finite_subsets_at_top B)"
  proof (rule filter_leI)
    fix P assume "eventually P (filtermap (\F. F - A) (finite_subsets_at_top B))"
    then obtain X where "finite X" and "X \ B"
      and P: "finite Y \ X \ Y \ Y \ B \ P (Y - A)" for Y
      unfolding eventually_filtermap eventually_finite_subsets_at_top by auto

    hence "finite (X-A)" and "X-A \ B - A"
      by auto
    moreover have "finite Y \ X-A \ Y \ Y \ B - A \ P Y" for Y
      using P[where Y="Y\X"] \finite X\ \X \ B\
      by (metis Diff_subset Int_Diff Un_Diff finite_Un inf.orderE le_sup_iff sup.orderE sup_ge2)
    ultimately show "eventually P (finite_subsets_at_top (B - A))"
      unfolding eventually_finite_subsets_at_top by meson
  qed
  have finite_subsets2:
    "filtermap (\F. F \ A) (finite_subsets_at_top B) \ finite_subsets_at_top A"
    apply (rule filter_leI)
      using assms unfolding eventually_filtermap eventually_finite_subsets_at_top
      by (metis Int_subset_iff finite_Int inf_le2 subset_trans)

  from assms(1) have limB: "(sum f \ b) (finite_subsets_at_top B)"
    using has_sum_def by auto
  from assms(2) have limA: "(sum f \ a) (finite_subsets_at_top A)"
    using has_sum_def by blast
  have "((\F. sum f (F\A)) \ a) (finite_subsets_at_top B)"
  proof (subst asm_rl [of "(\F. sum f (F\A)) = sum f \ (\F. F\A)"])
    show "(\F. sum f (F \ A)) = sum f \ (\F. F \ A)"
      unfolding o_def by auto
    show "((sum f \ (\F. F \ A)) \ a) (finite_subsets_at_top B)"
      unfolding o_def
      using tendsto_compose_filtermap finite_subsets2 limA tendsto_mono
        \<open>(\<lambda>F. sum f (F \<inter> A)) = sum f \<circ> (\<lambda>F. F \<inter> A)\<close> by fastforce
  qed

  with limB have \<section>: "((\<lambda>F. sum f F - sum f (F\<inter>A)) \<longlongrightarrow> b - a) (finite_subsets_at_top B)"
    using tendsto_diff by blast
  have "sum f X - sum f (X \ A) = sum f (X - A)" if "finite X" and "X \ B" for X :: "'a set"
    using that by (metis add_diff_cancel_left' sum.Int_Diff)
  hence "\\<^sub>F x in finite_subsets_at_top B. sum f x - sum f (x \ A) = sum f (x - A)"
    by (rule eventually_finite_subsets_at_top_weakI)
  hence "((\F. sum f (F-A)) \ b - a) (finite_subsets_at_top B)"
    using \<section> tendsto_cong by fastforce
  hence "(sum f \ b - a) (filtermap (\F. F-A) (finite_subsets_at_top B))"
    by (subst tendsto_compose_filtermap[symmetric], simp add: o_def)
  thus ?thesis
    using finite_subsets1 has_sum_def tendsto_mono by blast
qed

lemma
  fixes f :: "'a \ 'b::{topological_ab_group_add}"
  assumes "f summable_on B" and "f summable_on A" and "A \ B"
  shows summable_on_Diff: "f summable_on (B-A)"
  by (meson assms summable_on_def has_sum_Diff)

lemma
  fixes f :: "'a \ 'b::{topological_ab_group_add,t2_space}"
  assumes "f summable_on B" and "f summable_on A" and AB: "A \ B"
  shows infsum_Diff: "infsum f (B - A) = infsum f B - infsum f A"
  by (metis AB assms has_sum_Diff infsumI summable_on_def)

lemma has_sum_mono_neutral:
  fixes f :: "'a\'b::{ordered_comm_monoid_add,linorder_topology}"
  (* Does this really require a linorder topology? (Instead of order topology.) *)
  assumes \<open>(f has_sum a) A\<close> and "(g has_sum b) B"
  assumes \<open>\<And>x. x \<in> A\<inter>B \<Longrightarrow> f x \<le> g x\<close>
  assumes \<open>\<And>x. x \<in> A-B \<Longrightarrow> f x \<le> 0\<close>
  assumes \<open>\<And>x. x \<in> B-A \<Longrightarrow> g x \<ge> 0\<close>
  shows "a \ b"
proof -
  define f' g' where \<open>f' x = (if x \<in> A then f x else 0)\<close> and \<open>g' x = (if x \<in> B then g x else 0)\<close> for x
  have [simp]: \<open>f summable_on A\<close> \<open>g summable_on B\<close>
    using assms(1,2) summable_on_def by auto
  have \<open>(f' has_sum a) (A\<union>B)\<close>
    by (smt (verit, best) DiffE IntE Un_iff f'_def assms(1) has_sum_cong_neutral)
  then have f'_lim: \(sum f' \ a) (finite_subsets_at_top (A\B))\
    by (meson has_sum_def)
  have \<open>(g' has_sum b) (A\<union>B)\<close>
  by (smt (verit, best) DiffD1 DiffD2 IntE UnCI g'_def assms(2) has_sum_cong_neutral)
  then have g'_lim: \(sum g' \ b) (finite_subsets_at_top (A\B))\
    using has_sum_def by blast

  have "\X i. \X \ A \ B; i \ X\ \ f' i \ g' i"
    using assms by (auto simp: f'_def g'_def)
  then have \<open>\<forall>\<^sub>F x in finite_subsets_at_top (A \<union> B). sum f' x \<le> sum g' x\<close>
    by (intro eventually_finite_subsets_at_top_weakI sum_mono)
  then show ?thesis
    using f'_lim finite_subsets_at_top_neq_bot g'_lim tendsto_le by blast
qed

lemma infsum_mono_neutral:
  fixes f :: "'a\'b::{ordered_comm_monoid_add,linorder_topology}"
  assumes "f summable_on A" and "g summable_on B"
  assumes \<open>\<And>x. x \<in> A\<inter>B \<Longrightarrow> f x \<le> g x\<close>
  assumes \<open>\<And>x. x \<in> A-B \<Longrightarrow> f x \<le> 0\<close>
  assumes \<open>\<And>x. x \<in> B-A \<Longrightarrow> g x \<ge> 0\<close>
  shows "infsum f A \ infsum g B"
  by (smt (verit, best) assms has_sum_infsum has_sum_mono_neutral)

lemma has_sum_mono:
  fixes f :: "'a\'b::{ordered_comm_monoid_add,linorder_topology}"
  assumes "(f has_sum x) A" and "(g has_sum y) A"
  assumes \<open>\<And>x. x \<in> A \<Longrightarrow> f x \<le> g x\<close>
  shows "x \ y"
  using assms has_sum_mono_neutral by force

lemma infsum_mono:
  fixes f :: "'a\'b::{ordered_comm_monoid_add,linorder_topology}"
  assumes "f summable_on A" and "g summable_on A"
  assumes \<open>\<And>x. x \<in> A \<Longrightarrow> f x \<le> g x\<close>
  shows "infsum f A \ infsum g A"
  by (meson assms has_sum_infsum has_sum_mono)

lemma has_sum_finite[simp]:
  assumes "finite F"
  shows "(f has_sum (sum f F)) F"
  using assms
  by (auto intro: tendsto_Lim simp: finite_subsets_at_top_finite infsum_def has_sum_def principal_eq_bot_iff)

lemma summable_on_finite[simp]:
  fixes f :: \<open>'a \<Rightarrow> 'b::{comm_monoid_add,topological_space}\<close>
  assumes "finite F"
  shows "f summable_on F"
  using assms summable_on_def has_sum_finite by blast

lemma infsum_finite[simp]:
  assumes "finite F"
  shows "infsum f F = sum f F"
  by (simp add: assms infsumI)

lemma has_sum_finiteI: "finite A \ S = sum f A \ (f has_sum S) A"
  by simp

lemma has_sum_strict_mono_neutral:
  fixes f :: "'a \ 'b :: {ordered_ab_group_add, topological_ab_group_add, linorder_topology}"
  assumes \<open>(f has_sum a) A\<close> and "(g has_sum b) B"
  assumes \<open>\<And>x. x \<in> A\<inter>B \<Longrightarrow> f x \<le> g x\<close>
  assumes \<open>\<And>x. x \<in> A-B \<Longrightarrow> f x \<le> 0\<close>
  assumes \<open>\<And>x. x \<in> B-A \<Longrightarrow> g x \<ge> 0\<close>
  assumes \<open>x \<in> B\<close> \<open>if x \<in> A then f x < g x else 0 < g x\<close>
  shows "a < b"
proof -
  define y where "y = (if x \ A then f x else 0)"
  have "a - y \ b - g x"
  proof (rule has_sum_mono_neutral)
    show "(f has_sum (a - y)) (A - (if x \ A then {x} else {}))"
      by (intro has_sum_Diff assms has_sum_finiteI) (auto simp: y_def)
    show "(g has_sum (b - g x)) (B - {x})"
      by (intro has_sum_Diff assms has_sum_finiteI) (use assms in auto)
  qed (use assms in \<open>auto split: if_splits\<close>)
  moreover have "y < g x"
    using assms(3,4,5)[of x] assms(6-) by (auto simp: y_def split: if_splits)
  ultimately show ?thesis
    by (metis diff_strict_left_mono diff_strict_mono leD neqE)
qed

lemma has_sum_strict_mono:
  fixes f :: "'a \ 'b :: {ordered_ab_group_add, topological_ab_group_add, linorder_topology}"
  assumes \<open>(f has_sum a) A\<close> and "(g has_sum b) A"
  assumes \<open>\<And>x. x \<in> A \<Longrightarrow> f x \<le> g x\<close>
  assumes \<open>x \<in> A\<close> \<open>f x < g x\<close>
  shows "a < b"
  using assms has_sum_strict_mono_neutral by force

lemma has_sum_finite_approximation:
  fixes f :: "'a \ 'b::{comm_monoid_add,metric_space}"
  assumes "(f has_sum x) A" and "\ > 0"
  shows "\F. finite F \ F \ A \ dist (sum f F) x \ \"
proof -
  have "(sum f \ x) (finite_subsets_at_top A)"
    by (meson assms(1) has_sum_def)
  hence *: "\\<^sub>F F in (finite_subsets_at_top A). dist (sum f F) x < \"
    using assms(2) by (rule tendstoD)
  thus ?thesis
    unfolding eventually_finite_subsets_at_top by fastforce
qed

lemma infsum_finite_approximation:
  fixes f :: "'a \ 'b::{comm_monoid_add,metric_space}"
  assumes "f summable_on A" and "\ > 0"
  shows "\F. finite F \ F \ A \ dist (sum f F) (infsum f A) \ \"
proof -
  from assms have "(f has_sum (infsum f A)) A"
    by (simp add: summable_iff_has_sum_infsum)
  from this and \<open>\<epsilon> > 0\<close> show ?thesis
    by (rule has_sum_finite_approximation)
qed

lemma abs_summable_summable:
  fixes f :: \<open>'a \<Rightarrow> 'b :: banach\<close>
  assumes \<open>f abs_summable_on A\<close>
  shows \<open>f summable_on A\<close>
proof -
  from assms obtain L where lim: \<open>(sum (\<lambda>x. norm (f x)) \<longlongrightarrow> L) (finite_subsets_at_top A)\<close>
    unfolding has_sum_def summable_on_def by blast
  then have *: \<open>cauchy_filter (filtermap (sum (\<lambda>x. norm (f x))) (finite_subsets_at_top A))\<close>
    by (auto intro!: nhds_imp_cauchy_filter simp: filterlim_def)
  have \<open>\<exists>P. eventually P (finite_subsets_at_top A) \<and>
              (\<forall>F F'. P F \<and> P F' \<longrightarrow> dist (sum f F) (sum f F') < e)\<close> if \<open>e>0\<close> for e
  proof -
    define d P where \<open>d = e/4\<close> and \<open>P F \<longleftrightarrow> finite F \<and> F \<subseteq> A \<and> dist (sum (\<lambda>x. norm (f x)) F) L < d\<close> for F
    then have \<open>d > 0\<close>
      by (simp add: d_def that)
    have ev_P: \<open>eventually P (finite_subsets_at_top A)\<close>
      using lim
      by (auto simp add: P_def[abs_def] \<open>0 < d\<close> eventually_conj_iff eventually_finite_subsets_at_top_weakI tendsto_iff)

    moreover have \<open>dist (sum f F1) (sum f F2) < e\<close> if \<open>P F1\<close> and \<open>P F2\<close> for F1 F2
    proof -
      from ev_P
      obtain F' where \finite F'\ and \F' \ A\ and P_sup_F': \finite F \ F \ F' \ F \ A \ P F\ for F
        by atomize_elim (simp add: eventually_finite_subsets_at_top)
      define F where \<open>F = F' \<union> F1 \<union> F2\<close>
      have \<open>finite F\<close> and \<open>F \<subseteq> A\<close>
        using F_def P_def[abs_def] that \<open>finite F'\<close> \<open>F' \<subseteq> A\<close> by auto
      have dist_F: \<open>dist (sum (\<lambda>x. norm (f x)) F) L < d\<close>
        by (metis F_def \<open>F \<subseteq> A\<close> P_def P_sup_F' \<open>finite F\<close> le_supE order_refl)

      have dist_F_subset: \<open>dist (sum f F) (sum f F') < 2*d\<close> if F': \<open>F' \<subseteq> F\<close> \<open>P F'\<close> for F'
      proof -
        have \<open>dist (sum f F) (sum f F') = norm (sum f (F-F'))\<close>
          unfolding dist_norm using \<open>finite F\<close> F' by (subst sum_diff) auto
        also have \<open>\<dots> \<le> norm (\<Sum>x\<in>F-F'. norm (f x))\<close>
          by (rule order.trans[OF sum_norm_le[OF order.refl]]) auto
        also have \<open>\<dots> = dist (\<Sum>x\<in>F. norm (f x)) (\<Sum>x\<in>F'. norm (f x))\<close>
          unfolding dist_norm using \<open>finite F\<close> F' by (subst sum_diff) auto
        also have \<open>\<dots> < 2 * d\<close>
          using dist_F F' unfolding P_def dist_norm real_norm_def by linarith
        finally show \<open>dist (sum f F) (sum f F') < 2*d\<close> .
      qed

      have \<open>dist (sum f F1) (sum f F2) \<le> dist (sum f F) (sum f F1) + dist (sum f F) (sum f F2)\<close>
        by (rule dist_triangle3)
      also have \<open>\<dots> < 2 * d + 2 * d\<close>
        by (intro add_strict_mono dist_F_subset that) (auto simp: F_def)
      also have \<open>\<dots> \<le> e\<close>
        by (auto simp: d_def)
      finally show \<open>dist (sum f F1) (sum f F2) < e\<close> .
    qed
    then show ?thesis
      using ev_P by blast
  qed
  then have \<open>cauchy_filter (filtermap (sum f) (finite_subsets_at_top A))\<close>
    by (simp add: cauchy_filter_metric_filtermap)
  moreover have "complete (UNIV::'b set)"
    by (meson Cauchy_convergent UNIV_I complete_def convergent_def)
  ultimately obtain L' where \(sum f \ L') (finite_subsets_at_top A)\
    using complete_uniform[where S=UNIV] by (force simp add: filterlim_def)
  then show ?thesis
    using summable_on_def has_sum_def by blast
qed

text \<open>The converse of @{thm [source] abs_summable_summable} does not hold:
  Consider the Hilbert space of square-summable sequences.
  Let $e_i$ denote the sequence with 1 in the $i$th position and 0 elsewhere.
  Let $f(i) := e_i/i$ for $i\geq1$. We have \<^term>\<open>\<not> f abs_summable_on UNIV\<close> because $\lVert f(i)\rVert=1/i$
  and thus the sum over $\lVert f(i)\rVert$ diverges. On the other hand, we have \<^term>\<open>f summable_on UNIV\<close>;
  the limit is the sequence with $1/i$ in the $i$th position.

  (We have not formalized this separating example here because to the best of our knowledge,
  this Hilbert space has not been formalized in Isabelle/HOL yet.)\<close>

lemma norm_has_sum_bound:
  fixes f :: "'b \ 'a::real_normed_vector"
    and A :: "'b set"
  assumes "((\x. norm (f x)) has_sum n) A"
  assumes "(f has_sum a) A"
  shows "norm a \ n"
proof -
  have "norm a \ n + \" if "\>0" for \
  proof-
    have "\F. norm (a - sum f F) \ \ \ finite F \ F \ A"
      using has_sum_finite_approximation[where A=A and f=f and \<epsilon>="\<epsilon>"] assms \<open>0 < \<epsilon>\<close>
      by (metis dist_commute dist_norm)
    then obtain F where "norm (a - sum f F) \ \"
      and "finite F" and "F \ A"
      by (simp add: atomize_elim)
    hence "norm a \ norm (sum f F) + \"
      by (metis add.commute diff_add_cancel dual_order.refl norm_triangle_mono)
    also have "\ \ sum (\x. norm (f x)) F + \"
      using norm_sum by auto
    also have "\ \ n + \"
    proof (intro add_right_mono [OF has_sum_mono_neutral])
      show "((\x. norm (f x)) has_sum (\x\F. norm (f x))) F"
        by (simp add: \<open>finite F\<close>)
    qed (use \<open>F \<subseteq> A\<close> assms in auto)
    finally show ?thesis
      by assumption
  qed
  thus ?thesis
    using linordered_field_class.field_le_epsilon by blast
qed

lemma norm_infsum_bound:
  fixes f :: "'b \ 'a::real_normed_vector"
    and A :: "'b set"
  assumes "f abs_summable_on A"
  shows "norm (infsum f A) \ infsum (\x. norm (f x)) A"
proof (cases "f summable_on A")
  case True
  have "((\x. norm (f x)) has_sum (\\<^sub>\x\A. norm (f x))) A"
    by (simp add: assms)
  then show ?thesis
    by (metis True has_sum_infsum norm_has_sum_bound)
next
  case False
  obtain t where t_def: "(sum (\x. norm (f x)) \ t) (finite_subsets_at_top A)"
    using assms unfolding summable_on_def has_sum_def by blast
  have sumpos: "sum (\x. norm (f x)) X \ 0"
    for X
    by (simp add: sum_nonneg)
  have tgeq0:"t \ 0"
  proof(rule ccontr)
    define S::"real set" where "S = {s. s < 0}"
    assume "\ 0 \ t"
    hence "t < 0" by simp
    hence "t \ S"
      unfolding S_def by blast
    moreover have "open S"
      by (metis S_def lessThan_def open_real_lessThan)
    ultimately have "\\<^sub>F X in finite_subsets_at_top A. (\x\X. norm (f x)) \ S"
      using t_def unfolding tendsto_def by blast
    hence "\X. (\x\X. norm (f x)) \ S"
      by (metis (no_types, lifting) eventually_mono filterlim_iff finite_subsets_at_top_neq_bot tendsto_Lim)
    then obtain X where "(\x\X. norm (f x)) \ S"
      by blast
    hence "(\x\X. norm (f x)) < 0"
      unfolding S_def by auto
    thus False by (simp add: leD sumpos)
  qed
  have "\!h. (sum (\x. norm (f x)) \ h) (finite_subsets_at_top A)"
    using t_def finite_subsets_at_top_neq_bot tendsto_unique by blast
  hence "t = (Topological_Spaces.Lim (finite_subsets_at_top A) (sum (\x. norm (f x))))"
    using t_def unfolding Topological_Spaces.Lim_def
    by (metis the_equality)
  hence "Lim (finite_subsets_at_top A) (sum (\x. norm (f x))) \ 0"
    using tgeq0 by blast
  thus ?thesis unfolding infsum_def
    using False by auto
qed

lemma infsum_tendsto:
  assumes \<open>f summable_on S\<close>
  shows \<open>((\<lambda>F. sum f F) \<longlongrightarrow> infsum f S) (finite_subsets_at_top S)\<close>
  using assms has_sum_def has_sum_infsum by blast

lemma has_sum_0:
  assumes \<open>\<And>x. x\<in>M \<Longrightarrow> f x = 0\<close>
  shows \<open>(f has_sum 0) M\<close>
  by (metis assms finite.intros(1) has_sum_cong has_sum_cong_neutral has_sum_finite sum.neutral_const)

lemma summable_on_0:
  assumes \<open>\<And>x. x\<in>M \<Longrightarrow> f x = 0\<close>
  shows \<open>f summable_on M\<close>
  using assms summable_on_def has_sum_0 by blast

lemma infsum_0:
  assumes \<open>\<And>x. x\<in>M \<Longrightarrow> f x = 0\<close>
  shows \<open>infsum f M = 0\<close>
  by (metis assms finite_subsets_at_top_neq_bot infsum_def has_sum_0 has_sum_def tendsto_Lim)

text \<open>Variants of @{thm [source] infsum_0} etc. suitable as simp-rules\<close>
lemma infsum_0_simp[simp]: \<open>infsum (\<lambda>_. 0) M = 0\<close>
  by (simp_all add: infsum_0)

lemma summable_on_0_simp[simp]: \<open>(\<lambda>_. 0) summable_on M\<close>
  by (simp_all add: summable_on_0)

lemma has_sum_0_simp[simp]: \<open>((\<lambda>_. 0) has_sum 0) M\<close>
  by (simp_all add: has_sum_0)

lemma has_sum_add:
  fixes f g :: "'a \ 'b::{topological_comm_monoid_add}"
  assumes \<open>(f has_sum a) A\<close>
  assumes \<open>(g has_sum b) A\<close>
  shows \<open>((\<lambda>x. f x + g x) has_sum (a + b)) A\<close>
proof -
  from assms have lim_f: \<open>(sum f \<longlongrightarrow> a)  (finite_subsets_at_top A)\<close>
    and lim_g: \<open>(sum g \<longlongrightarrow> b)  (finite_subsets_at_top A)\<close>
    by (simp_all add: has_sum_def)
  then have lim: \<open>(sum (\<lambda>x. f x + g x) \<longlongrightarrow> a + b) (finite_subsets_at_top A)\<close>
    unfolding sum.distrib by (rule tendsto_add)
  then show ?thesis
    by (simp_all add: has_sum_def)
qed

lemma summable_on_add:
  fixes f g :: "'a \ 'b::{topological_comm_monoid_add}"
  assumes \<open>f summable_on A\<close>
  assumes \<open>g summable_on A\<close>
  shows \<open>(\<lambda>x. f x + g x) summable_on A\<close>
  by (metis (full_types) assms summable_on_def has_sum_add)

lemma infsum_add:
  fixes f g :: "'a \ 'b::{topological_comm_monoid_add, t2_space}"
  assumes \<open>f summable_on A\<close>
  assumes \<open>g summable_on A\<close>
  shows \<open>infsum (\<lambda>x. f x + g x) A = infsum f A + infsum g A\<close>
proof -
  have \<open>((\<lambda>x. f x + g x) has_sum (infsum f A + infsum g A)) A\<close>
    by (simp add: assms has_sum_add)
  then show ?thesis
    using infsumI by blast
qed

lemma has_sum_Un_disjoint:
  fixes f :: "'a \ 'b::topological_comm_monoid_add"
  assumes "(f has_sum a) A"
  assumes "(f has_sum b) B"
  assumes disj: "A \ B = {}"
  shows \<open>(f has_sum (a + b)) (A \<union> B)\<close>
proof -
  define fA fB where \<open>fA x = (if x \<in> A then f x else 0)\<close>
    and \<open>fB x = (if x \<notin> A then f x else 0)\<close> for x
  have fA: \<open>(fA has_sum a) (A \<union> B)\<close>
    by (smt (verit, ccfv_SIG) DiffD1 DiffD2 UnCI fA_def assms(1) has_sum_cong_neutral inf_sup_absorb)
  have fB: \<open>(fB has_sum b) (A \<union> B)\<close>
    by (smt (verit, best) DiffD1 DiffD2 IntE Un_iff fB_def assms(2) disj disjoint_iff has_sum_cong_neutral)
  have fAB: \<open>f x = fA x + fB x\<close> for x
    unfolding fA_def fB_def by simp
  show ?thesis
    unfolding fAB
    using fA fB by (rule has_sum_add)
qed

lemma summable_on_Un_disjoint:
  fixes f :: "'a \ 'b::topological_comm_monoid_add"
  assumes "f summable_on A"
  assumes "f summable_on B"
  assumes disj: "A \ B = {}"
  shows \<open>f summable_on (A \<union> B)\<close>
  by (meson assms disj summable_on_def has_sum_Un_disjoint)

lemma infsum_Un_disjoint:
  fixes f :: "'a \ 'b::{topological_comm_monoid_add, t2_space}"
  assumes "f summable_on A"
  assumes "f summable_on B"
  assumes disj: "A \ B = {}"
  shows \<open>infsum f (A \<union> B) = infsum f A + infsum f B\<close>
  by (intro infsumI has_sum_Un_disjoint has_sum_infsum assms)

lemma norm_summable_imp_has_sum:
  fixes f :: "nat \ 'a :: banach"
  assumes "summable (\n. norm (f n))" and "f sums S"
  shows   "(f has_sum S) (UNIV :: nat set)"
  unfolding has_sum_def tendsto_iff eventually_finite_subsets_at_top
proof clarsimp
  fix \<epsilon>::real
  assume "\ > 0"
  from assms obtain S' where S': "(\n. norm (f n)) sums S'"
    by (auto simp: summable_def)
  with \<open>\<epsilon> > 0\<close> obtain N where N: "\<And>n. n \<ge> N \<Longrightarrow> \<bar>S' - (\<Sum>i<n. norm (f i))\<bar> < \<epsilon>"
    by (auto simp: tendsto_iff eventually_at_top_linorder sums_def dist_norm abs_minus_commute)
  have "dist (sum f Y) S < \" if "finite Y" "{.. Y" for Y
  proof -
    from that have "(\n. if n \ Y then 0 else f n) sums (S - sum f Y)"
      by (intro sums_If_finite_set'[OF \f sums S\]) (auto simp: sum_negf)
    hence "S - sum f Y = (\n. if n \ Y then 0 else f n)"
      by (simp add: sums_iff)
    also have "norm \ \ (\n. norm (if n \ Y then 0 else f n))"
      by (rule summable_norm[OF summable_comparison_test'[OF assms(1)]]) auto
    also have "\ \ (\n. if n < N then 0 else norm (f n))"
      using that by (intro suminf_le summable_comparison_test'[OF assms(1)]) auto
    also have "(\n. if n \ {..i
      by (intro sums_If_finite_set'[OF S']) (auto simp: sum_negf)
    hence "(\n. if n < N then 0 else norm (f n)) = S' - (\i
      by (simp add: sums_iff)
    also have "S' - (\i \S' - (\i" by simp
    also have "\ < \" by (rule N) auto
    finally show ?thesis by (simp add: dist_norm norm_minus_commute)
  qed
  then show "\X. finite X \ (\Y. finite Y \ X \ Y \ dist (sum f Y) S < \)"
    by (meson finite_lessThan subset_UNIV)
qed

lemma norm_summable_imp_summable_on:
  fixes f :: "nat \ 'a :: banach"
  assumes "summable (\n. norm (f n))"
  shows   "f summable_on UNIV"
  using norm_summable_imp_has_sum[OF assms, of "suminf f"] assms
  by (auto simp: sums_iff summable_on_def dest: summable_norm_cancel)

lemma sums_nonneg_imp_has_sum_strong:
  assumes "f sums (S::real)" "eventually (\n. f n \ 0) sequentially"
  shows   "(f has_sum S) UNIV"
proof -
  from assms(2) obtain N where N: "\n. n \ N \ f n \ 0"
    by (auto simp: eventually_at_top_linorder)
  from assms(1) have "summable f"
    by (simp add: sums_iff)
  hence "summable (\n. f (n + N))"
    by (rule summable_ignore_initial_segment)
  hence "summable (\n. norm (f (n + N)))"
    using N by simp
  hence "summable (\n. norm (f n))"
    using summable_iff_shift by blast
  with assms(1) show ?thesis
    using norm_summable_imp_has_sum by blast
qed

lemma sums_nonneg_imp_has_sum:
  assumes "f sums (S::real)" and "\n. f n \ 0"
  shows   "(f has_sum S) UNIV"
  by (rule sums_nonneg_imp_has_sum_strong) (use assms in auto)

lemma summable_nonneg_imp_summable_on_strong:
  assumes "summable f" "eventually (\n. f n \ (0::real)) sequentially"
  shows   "f summable_on UNIV"
  using assms has_sum_iff sums_nonneg_imp_has_sum_strong by blast

lemma summable_nonneg_imp_summable_on:
  assumes "summable f" "\n. f n \ (0::real)"
  shows   "f summable_on UNIV"
  by (rule summable_nonneg_imp_summable_on_strong) (use assms in auto)

text \<open>The following lemma indeed needs a complete space (as formalized by the premise \<^term>\<open>complete UNIV\<close>).
  The following two counterexamples show this:
  \begin{itemize}
  \item Consider the real vector space $V$ of sequences with finite support, and with the $\ell_2$-norm (sum of squares).
      Let $e_i$ denote the sequence with a $1$ at position $i$.
      Let $f : \mathbb Z \to V$ be defined as $f(n) := e_{\lvert n\rvert} / n$ (with $f(0) := 0$).
      We have that $\sum_{n\in\mathbb Z} f(n) = 0$ (it even converges absolutely).
      But $\sum_{n\in\mathbb N} f(n)$ does not exist (it would converge against a sequence with infinite support).

  \item Let $f$ be a positive rational valued function such that $\sum_{x\in B} f(x)$ is $\sqrt 2$ and $\sum_{x\in A} f(x)$ is 1 (over the reals, with $A\subseteq B$).
      Then $\sum_{x\in B} f(x)$ does not exist over the rationals. But $\sum_{x\in A} f(x)$ exists.
  \end{itemize}

  The lemma also requires uniform continuity of the addition. And example of a topological group with continuous
  but not uniformly continuous addition would be the positive reals with the usual multiplication as the addition.
  We do not know whether the lemma would also hold for such topological groups.\<close>

lemma summable_on_subset_aux:
  fixes A B and f :: \<open>'a \<Rightarrow> 'b::{ab_group_add, uniform_space}\<close>
  assumes \<open>complete (UNIV :: 'b set)\<close>
  assumes plus_cont: \<open>uniformly_continuous_on UNIV (\<lambda>(x::'b,y). x+y)\<close>
  assumes \<open>f summable_on A\<close>
  assumes \<open>B \<subseteq> A\<close>
  shows \<open>f summable_on B\<close>
proof -
  let ?filter_fB = \<open>filtermap (sum f) (finite_subsets_at_top B)\<close>
  from \<open>f summable_on A\<close>
  obtain S where \<open>(sum f \<longlongrightarrow> S) (finite_subsets_at_top A)\<close> (is \<open>(sum f \<longlongrightarrow> S) ?filter_A\<close>)
    using summable_on_def has_sum_def by blast
  then have cauchy_fA: \<open>cauchy_filter (filtermap (sum f) (finite_subsets_at_top A))\<close> (is \<open>cauchy_filter ?filter_fA\<close>)
    by (auto intro!: nhds_imp_cauchy_filter simp: filterlim_def)

  have \<open>cauchy_filter (filtermap (sum f) (finite_subsets_at_top B))\<close>
  proof (unfold cauchy_filter_def, rule filter_leI)
    fix E :: \<open>('b\<times>'b) \<Rightarrow> bool\<close> assume \<open>eventually E uniformity\<close>
    then obtain E' where \eventually E' uniformity\ and E'E'E: \E' (x, y) \ E' (y, z) \ E (x, z)\ for x y z
      using uniformity_trans by blast
    obtain D where \<open>eventually D uniformity\<close> and DE: \<open>D (x, y) \<Longrightarrow> E' (x+c, y+c)\<close> for x y c
      using plus_cont \<open>eventually E' uniformity\<close>
      unfolding uniformly_continuous_on_uniformity filterlim_def le_filter_def uniformity_prod_def
      by (auto simp: case_prod_beta eventually_filtermap eventually_prod_same uniformity_refl)
    have DE': "E' (x, y)" if "D (x + c, y + c)" for x y c
      using DE[of "x + c" "y + c" "-c"] that by simp

    from \<open>eventually D uniformity\<close> and cauchy_fA have \<open>eventually D (?filter_fA \<times>\<^sub>F ?filter_fA)\<close>
      unfolding cauchy_filter_def le_filter_def by simp
    then obtain P1 P2
      where ev_P1: \<open>eventually (\<lambda>F. P1 (sum f F)) ?filter_A\<close>
        and ev_P2: \<open>eventually (\<lambda>F. P2 (sum f F)) ?filter_A\<close>
        and P1P2E: \<open>P1 x \<Longrightarrow> P2 y \<Longrightarrow> D (x, y)\<close> for x y
      unfolding eventually_prod_filter eventually_filtermap
      by auto
    from ev_P1 obtain F1 where F1: \<open>finite F1\<close> \<open>F1 \<subseteq> A\<close> \<open>\<And>F. F\<supseteq>F1 \<Longrightarrow> finite F \<Longrightarrow> F\<subseteq>A \<Longrightarrow> P1 (sum f F)\<close>
      by (metis eventually_finite_subsets_at_top)
    from ev_P2 obtain F2 where F2: \<open>finite F2\<close> \<open>F2 \<subseteq> A\<close> \<open>\<And>F. F\<supseteq>F2 \<Longrightarrow> finite F \<Longrightarrow> F\<subseteq>A \<Longrightarrow> P2 (sum f F)\<close>
      by (metis eventually_finite_subsets_at_top)
    define F0 F0A F0B where \<open>F0 \<equiv> F1 \<union> F2\<close> and \<open>F0A \<equiv> F0 - B\<close> and \<open>F0B \<equiv> F0 \<inter> B\<close>
    have [simp]: \<open>finite F0\<close>  \<open>F0 \<subseteq> A\<close>
      using \<open>F1 \<subseteq> A\<close> \<open>F2 \<subseteq> A\<close> \<open>finite F1\<close> \<open>finite F2\<close> unfolding F0_def by blast+

    have *: "E' (sum f F1', sum f F2')"
      if "F1'\F0B" "F2'\F0B" "finite F1'" "finite F2'" "F1'\B" "F2'\B" for F1' F2'
    proof (intro DE'[where c = "sum f F0A"] P1P2E)
      have "P1 (sum f (F1' \ F0A))"
        using that assms F1(1,2) F2(1,2) by (intro F1) (auto simp: F0A_def F0B_def F0_def)
      thus "P1 (sum f F1' + sum f F0A)"
        by (subst (asm) sum.union_disjoint) (use that in \<open>auto simp: F0A_def\<close>)
    next
      have "P2 (sum f (F2' \ F0A))"
        using that assms F1(1,2) F2(1,2) by (intro F2) (auto simp: F0A_def F0B_def F0_def)
      thus "P2 (sum f F2' + sum f F0A)"
        by (subst (asm) sum.union_disjoint) (use that in \<open>auto simp: F0A_def\<close>)
    qed

    have "eventually (\x. E' (x, sum f F0B)) (filtermap (sum f) (finite_subsets_at_top B))"
     and "eventually (\x. E' (sum f F0B, x)) (filtermap (sum f) (finite_subsets_at_top B))"
        unfolding eventually_filtermap eventually_finite_subsets_at_top
        by (rule exI[of _ F0B]; use * in \<open>force simp: F0B_def\<close>)+
      then
    show \<open>eventually E (?filter_fB \<times>\<^sub>F ?filter_fB)\<close>
      unfolding eventually_prod_filter
      using E'E'E by blast
  qed

  then obtain x where \<open>?filter_fB \<le> nhds x\<close>
    using cauchy_filter_complete_converges[of ?filter_fB UNIV] \<open>complete (UNIV :: _)\<close>
    by (auto simp: filtermap_bot_iff)
  then have \<open>(sum f \<longlongrightarrow> x) (finite_subsets_at_top B)\<close>
    by (auto simp: filterlim_def)
  then show ?thesis
    by (auto simp: summable_on_def has_sum_def)
qed

text \<open>A special case of @{thm [source] summable_on_subset_aux} for Banach spaces with fewer premises.\<close>

lemma summable_on_subset_banach:
  fixes A B and f :: \<open>'a \<Rightarrow> 'b::banach\<close>
  assumes \<open>f summable_on A\<close>
  assumes \<open>B \<subseteq> A\<close>
  shows \<open>f summable_on B\<close>
  by (meson Cauchy_convergent UNIV_I assms complete_def convergent_def isUCont_plus summable_on_subset_aux)

lemma has_sum_empty[simp]: \<open>(f has_sum 0) {}\<close>
  by (meson ex_in_conv has_sum_0)

lemma summable_on_empty[simp]: \<open>f summable_on {}\<close>
  by auto

lemma infsum_empty[simp]: \<open>infsum f {} = 0\<close>
  by simp

lemma sum_has_sum:
  fixes f :: "'a \ 'b::topological_comm_monoid_add"
  assumes \<open>finite A\<close>
  assumes \<open>\<And>a. a \<in> A \<Longrightarrow> (f has_sum (s a)) (B a)\<close>
  assumes \<open>\<And>a a'. a\<in>A \<Longrightarrow> a'\<in>A \<Longrightarrow> a\<noteq>a' \<Longrightarrow> B a \<inter> B a' = {}\<close>
  shows \<open>(f has_sum (sum s A)) (\<Union>a\<in>A. B a)\<close>
  using assms
proof (induction)
  case empty
  then show ?case
    by simp
next
  case (insert x A)
  have \<open>(f has_sum (s x)) (B x)\<close>
    by (simp add: insert.prems)
  moreover have IH: \<open>(f has_sum (sum s A)) (\<Union>a\<in>A. B a)\<close>
    using insert by simp
  ultimately have \<open>(f has_sum (s x + sum s A)) (B x \<union> (\<Union>a\<in>A. B a))\<close>
    using insert by (intro has_sum_Un_disjoint) auto
  then show ?case
    using insert.hyps by auto
qed

lemma summable_on_finite_union_disjoint:
  fixes f :: "'a \ 'b::topological_comm_monoid_add"
  assumes finite: \<open>finite A\<close>
  assumes conv: \<open>\<And>a. a \<in> A \<Longrightarrow> f summable_on (B a)\<close>
  assumes disj: \<open>\<And>a a'. a\<in>A \<Longrightarrow> a'\<in>A \<Longrightarrow> a\<noteq>a' \<Longrightarrow> B a \<inter> B a' = {}\<close>
  shows \<open>f summable_on (\<Union>a\<in>A. B a)\<close>
  using sum_has_sum [of A f B] assms unfolding summable_on_def by metis

lemma sum_infsum:
  fixes f :: "'a \ 'b::{topological_comm_monoid_add, t2_space}"
  assumes finite: \<open>finite A\<close>
  assumes conv: \<open>\<And>a. a \<in> A \<Longrightarrow> f summable_on (B a)\<close>
  assumes disj: \<open>\<And>a a'. a\<in>A \<Longrightarrow> a'\<in>A \<Longrightarrow> a\<noteq>a' \<Longrightarrow> B a \<inter> B a' = {}\<close>
  shows \<open>sum (\<lambda>a. infsum f (B a)) A = infsum f (\<Union>a\<in>A. B a)\<close>
  by (metis (no_types, lifting) assms has_sum_infsum infsumI sum_has_sum)

text \<open>The lemmas \<open>infsum_comm_additive_general\<close> and \<open>infsum_comm_additive\<close> (and variants) below both state that the infinite sum commutes with
  a continuous additive function. \<open>infsum_comm_additive_general\<close> is stated more for more general type classes
  at the expense of a somewhat less compact formulation of the premises.
  E.g., by avoiding the constant \<^const>\<open>additive\<close> which introduces an additional sort constraint
  (group instead of monoid). For example, extended reals (\<^typ>\<open>ereal\<close>, \<^typ>\<open>ennreal\<close>) are not covered
  by \<open>infsum_comm_additive\<close>.\<close>

lemma has_sum_comm_additive_general:
  fixes f :: \<open>'b :: {comm_monoid_add,topological_space} \<Rightarrow> 'c :: {comm_monoid_add,topological_space}\<close>
  assumes f_sum: \<open>\<And>F. finite F \<Longrightarrow> F \<subseteq> S \<Longrightarrow> sum (f \<circ> g) F = f (sum g F)\<close>
      \<comment> \<open>Not using \<^const>\<open>additive\<close> because it would add sort constraint \<^class>\<open>ab_group_add\<close>\<close>
  assumes cont: \<open>f \<midarrow>x\<rightarrow> f x\<close>
    \<comment> \<open>For \<^class>\<open>t2_space\<close>, this is equivalent to \<open>isCont f x\<close> by @{thm [source] isCont_def}.\<close>
  assumes infsum: \<open>(g has_sum x) S\<close>
  shows \<open>((f \<circ> g) has_sum (f x)) S\<close>
proof -
  have \<open>(sum g \<longlongrightarrow> x) (finite_subsets_at_top S)\<close>
    using infsum has_sum_def by blast
  then have \<open>((f \<circ> sum g) \<longlongrightarrow> f x) (finite_subsets_at_top S)\<close>
    by (meson cont filterlim_def tendsto_at_iff_tendsto_nhds tendsto_compose_filtermap tendsto_mono)
  then have \<open>(sum (f \<circ> g) \<longlongrightarrow> f x) (finite_subsets_at_top S)\<close>
    using tendsto_cong f_sum
    by (simp add: Lim_transform_eventually eventually_finite_subsets_at_top_weakI)
  then show \<open>((f \<circ> g) has_sum (f x)) S\<close>
    using has_sum_def by blast
qed

lemma summable_on_comm_additive_general:
  fixes f :: \<open>'b :: {comm_monoid_add,topological_space} \<Rightarrow> 'c :: {comm_monoid_add,topological_space}\<close>
  assumes \<open>\<And>F. finite F \<Longrightarrow> F \<subseteq> S \<Longrightarrow> sum (f \<circ> g) F = f (sum g F)\<close>
    \<comment> \<open>Not using \<^const>\<open>additive\<close> because it would add sort constraint \<^class>\<open>ab_group_add\<close>\<close>
  assumes \<open>\<And>x. (g has_sum x) S \<Longrightarrow> f \<midarrow>x\<rightarrow> f x\<close>
    \<comment> \<open>For \<^class>\<open>t2_space\<close>, this is equivalent to \<open>isCont f x\<close> by @{thm [source] isCont_def}.\<close>
  assumes \<open>g summable_on S\<close>
  shows \<open>(f \<circ> g) summable_on S\<close>
  by (meson assms summable_on_def has_sum_comm_additive_general has_sum_def infsum_tendsto)

lemma infsum_comm_additive_general:
  fixes f :: \<open>'b :: {comm_monoid_add,t2_space} \<Rightarrow> 'c :: {comm_monoid_add,t2_space}\<close>
  assumes f_sum: \<open>\<And>F. finite F \<Longrightarrow> F \<subseteq> S \<Longrightarrow> sum (f \<circ> g) F = f (sum g F)\<close>
      \<comment> \<open>Not using \<^const>\<open>additive\<close> because it would add sort constraint \<^class>\<open>ab_group_add\<close>\<close>
  assumes \<open>isCont f (infsum g S)\<close>
  assumes \<open>g summable_on S\<close>
  shows \<open>infsum (f \<circ> g) S = f (infsum g S)\<close>
  using assms
  by (intro infsumI has_sum_comm_additive_general has_sum_infsum) (auto simp: isCont_def)

lemma has_sum_comm_additive:
  fixes f :: \<open>'b :: {ab_group_add,topological_space} \<Rightarrow> 'c :: {ab_group_add,topological_space}\<close>
  assumes \<open>additive f\<close>
  assumes \<open>f \<midarrow>x\<rightarrow> f x\<close>
    \<comment> \<open>For \<^class>\<open>t2_space\<close>, this is equivalent to \<open>isCont f x\<close> by @{thm [source] isCont_def}.\<close>
  assumes infsum: \<open>(g has_sum x) S\<close>
  shows \<open>((f \<circ> g) has_sum (f x)) S\<close>
  using assms
  by (intro has_sum_comm_additive_general has_sum_infsum) (auto simp: isCont_def additive.sum)

lemma summable_on_comm_additive:
  fixes f :: \<open>'b :: {ab_group_add,t2_space} \<Rightarrow> 'c :: {ab_group_add,topological_space}\<close>
  assumes \<open>additive f\<close>
  assumes \<open>isCont f (infsum g S)\<close>
  assumes \<open>g summable_on S\<close>
  shows \<open>(f \<circ> g) summable_on S\<close>
  by (meson assms summable_on_def has_sum_comm_additive has_sum_infsum isContD)

lemma infsum_comm_additive:
  fixes f :: \<open>'b :: {ab_group_add,t2_space} \<Rightarrow> 'c :: {ab_group_add,t2_space}\<close>
  assumes \<open>additive f\<close>
  assumes \<open>isCont f (infsum g S)\<close>
  assumes \<open>g summable_on S\<close>
  shows \<open>infsum (f \<circ> g) S = f (infsum g S)\<close>
  by (rule infsum_comm_additive_general; auto simp: assms additive.sum)

lemma nonneg_bdd_above_has_sum:
  fixes f :: \<open>'a \<Rightarrow> 'b :: {conditionally_complete_linorder, ordered_comm_monoid_add, linorder_topology}\<close>
  assumes \<open>\<And>x. x\<in>A \<Longrightarrow> f x \<ge> 0\<close>
  assumes \<open>bdd_above (sum f ` {F. F\<subseteq>A \<and> finite F})\<close>
  shows \<open>(f has_sum (SUP F\<in>{F. finite F \<and> F\<subseteq>A}. sum f F)) A\<close>
proof -
  have \<open>(sum f \<longlongrightarrow> (SUP F\<in>{F. finite F \<and> F\<subseteq>A}. sum f F)) (finite_subsets_at_top A)\<close>
  proof (rule order_tendstoI)
    fix a assume \<open>a < (SUP F\<in>{F. finite F \<and> F\<subseteq>A}. sum f F)\<close>
    then obtain F where \<open>a < sum f F\<close> and \<open>finite F\<close> and \<open>F \<subseteq> A\<close>
      by (metis (mono_tags, lifting) Collect_cong Collect_empty_eq assms(2) empty_subsetI finite.emptyI less_cSUP_iff mem_Collect_eq)
    have "\Y. \finite Y; F \ Y; Y \ A\ \ a < sum f Y"
      by (meson DiffE \<open>a < sum f F\<close> assms(1) less_le_trans subset_iff sum_mono2)
    then show \<open>\<forall>\<^sub>F x in finite_subsets_at_top A. a < sum f x\<close>
      by (metis \<open>F \<subseteq> A\<close> \<open>finite F\<close> eventually_finite_subsets_at_top)
  next
    fix a assume *: \<open>(SUP F\<in>{F. finite F \<and> F\<subseteq>A}. sum f F) < a\<close>
    have "sum f F \ (SUP F\{F. finite F \ F\A}. sum f F)" if \F\A\ and \finite F\ for F
        by (rule cSUP_upper) (use that assms(2) in \<open>auto simp: conj_commute\<close>)
    then show \<open>\<forall>\<^sub>F x in finite_subsets_at_top A. sum f x < a\<close>
      by (metis (no_types, lifting) "*" eventually_finite_subsets_at_top_weakI order_le_less_trans)
  qed
  then show ?thesis
    using has_sum_def by blast
qed

lemma nonneg_bdd_above_summable_on:
  fixes f :: \<open>'a \<Rightarrow> 'b :: {conditionally_complete_linorder, ordered_comm_monoid_add, linorder_topology}\<close>
  assumes \<open>\<And>x. x\<in>A \<Longrightarrow> f x \<ge> 0\<close>
  assumes \<open>bdd_above (sum f ` {F. F\<subseteq>A \<and> finite F})\<close>
  shows \<open>f summable_on A\<close>
  using assms summable_on_def nonneg_bdd_above_has_sum by blast

lemma nonneg_bdd_above_infsum:
  fixes f :: \<open>'a \<Rightarrow> 'b :: {conditionally_complete_linorder, ordered_comm_monoid_add, linorder_topology}\<close>
  assumes \<open>\<And>x. x\<in>A \<Longrightarrow> f x \<ge> 0\<close>
  assumes \<open>bdd_above (sum f ` {F. F\<subseteq>A \<and> finite F})\<close>
  shows \<open>infsum f A = (SUP F\<in>{F. finite F \<and> F\<subseteq>A}. sum f F)\<close>
  using assms by (auto intro!: infsumI nonneg_bdd_above_has_sum)

lemma nonneg_has_sum_complete:
  fixes f :: \<open>'a \<Rightarrow> 'b :: {complete_linorder, ordered_comm_monoid_add, linorder_topology}\<close>
  assumes \<open>\<And>x. x\<in>A \<Longrightarrow> f x \<ge> 0\<close>
  shows \<open>(f has_sum (SUP F\<in>{F. finite F \<and> F\<subseteq>A}. sum f F)) A\<close>
  using assms nonneg_bdd_above_has_sum by blast

lemma nonneg_summable_on_complete:
  fixes f :: \<open>'a \<Rightarrow> 'b :: {complete_linorder, ordered_comm_monoid_add, linorder_topology}\<close>
  assumes \<open>\<And>x. x\<in>A \<Longrightarrow> f x \<ge> 0\<close>
  shows \<open>f summable_on A\<close>
  using assms nonneg_bdd_above_summable_on by blast

lemma nonneg_infsum_complete:
  fixes f :: \<open>'a \<Rightarrow> 'b :: {complete_linorder, ordered_comm_monoid_add, linorder_topology}\<close>
  assumes \<open>\<And>x. x\<in>A \<Longrightarrow> f x \<ge> 0\<close>
  shows \<open>infsum f A = (SUP F\<in>{F. finite F \<and> F\<subseteq>A}. sum f F)\<close>
  using assms nonneg_bdd_above_infsum by blast

lemma has_sum_nonneg:
  fixes f :: "'a \ 'b::{ordered_comm_monoid_add,linorder_topology}"
  assumes "(f has_sum a) M"
    and "\x. x \ M \ 0 \ f x"
  shows "a \ 0"
  by (metis (no_types, lifting) DiffD1 assms empty_iff has_sum_0 has_sum_mono_neutral order_refl)

lemma infsum_nonneg:
  fixes f :: "'a \ 'b::{ordered_comm_monoid_add,linorder_topology}"
  assumes "\x. x \ M \ 0 \ f x"
  shows "infsum f M \ 0" (is "?lhs \ _")
  by (metis assms has_sum_infsum has_sum_nonneg infsum_not_exists linorder_linear)

lemma has_sum_mono2:
  fixes f :: "'a \ 'b::{topological_ab_group_add, ordered_comm_monoid_add,linorder_topology}"
  assumes "(f has_sum S) A" "(f has_sum S') B" "A \ B"
  assumes "\x. x \ B - A \ f x \ 0"
  shows   "S \ S'"
  by (metis add_0 add_right_mono assms diff_add_cancel has_sum_Diff has_sum_nonneg)

lemma infsum_mono2:
  fixes f :: "'a \ 'b::{topological_ab_group_add, ordered_comm_monoid_add,linorder_topology}"
  assumes "f summable_on A" "f summable_on B" "A \ B"
  assumes "\x. x \ B - A \ f x \ 0"
  shows   "infsum f A \ infsum f B"
  by (rule has_sum_mono2[OF has_sum_infsum has_sum_infsum]) (use assms in auto)

lemma finite_sum_le_has_sum:
  fixes f :: "'a \ 'b::{topological_ab_group_add, ordered_comm_monoid_add,linorder_topology}"
  assumes "(f has_sum S) A" "finite B" "B \ A"
  assumes "\x. x \ A - B \ f x \ 0"
  shows   "sum f B \ S"
  by (meson assms has_sum_finite has_sum_mono2)

lemma finite_sum_le_infsum:
  fixes f :: "'a \ 'b::{topological_ab_group_add, ordered_comm_monoid_add,linorder_topology}"
  assumes "f summable_on A" "finite B" "B \ A"
  assumes "\x. x \ A - B \ f x \ 0"
  shows   "sum f B \ infsum f A"
  by (rule finite_sum_le_has_sum[OF has_sum_infsum]) (use assms in auto)

lemma has_sum_reindex:
  assumes \<open>inj_on h A\<close>
  shows \<open>(g has_sum x) (h ` A) \<longleftrightarrow> ((g \<circ> h) has_sum x) A\<close>
proof -
  have \<open>(g has_sum x) (h ` A) \<longleftrightarrow> (sum g \<longlongrightarrow> x) (finite_subsets_at_top (h ` A))\<close>
    by (simp add: has_sum_def)
  also have \<open>\<dots> \<longleftrightarrow> ((\<lambda>F. sum g (h ` F)) \<longlongrightarrow> x) (finite_subsets_at_top A)\<close>
    by (metis assms filterlim_filtermap filtermap_image_finite_subsets_at_top)
  also have \<open>\<dots> \<longleftrightarrow> (sum (g \<circ> h) \<longlongrightarrow> x) (finite_subsets_at_top A)\<close>
  proof (intro tendsto_cong eventually_finite_subsets_at_top_weakI sum.reindex)
    show "\X. \finite X; X \ A\ \ inj_on h X"
      using assms inj_on_subset by blast
  qed
  also have \<open>\<dots> \<longleftrightarrow> ((g \<circ> h) has_sum x) A\<close>
    by (simp add: has_sum_def)
  finally show ?thesis .
qed

lemma summable_on_reindex:
  assumes \<open>inj_on h A\<close>
  shows \<open>g summable_on (h ` A) \<longleftrightarrow> (g \<circ> h) summable_on A\<close>
  by (simp add: assms summable_on_def has_sum_reindex)

lemma infsum_reindex:
  assumes \<open>inj_on h A\<close>
  shows \<open>infsum g (h ` A) = infsum (g \<circ> h) A\<close>
  by (metis assms has_sum_infsum has_sum_reindex infsumI infsum_def)

lemma summable_on_reindex_bij_betw:
  assumes "bij_betw g A B"
  shows   "(\x. f (g x)) summable_on A \ f summable_on B"
  by (smt (verit) assms bij_betw_def o_apply summable_on_cong summable_on_reindex)

lemma infsum_reindex_bij_betw:
  assumes "bij_betw g A B"
  shows   "infsum (\x. f (g x)) A = infsum f B"
  by (metis (mono_tags, lifting) assms bij_betw_def infsum_cong infsum_reindex o_def)

lemma sum_uniformity:
  assumes plus_cont: \<open>uniformly_continuous_on UNIV (\<lambda>(x::'b::{uniform_space,comm_monoid_add},y). x+y)\<close>
  assumes EE: \<open>eventually E uniformity\<close>
  obtains D where \<open>eventually D uniformity\<close>
    and \<open>\<And>M::'a set. \<And>f f' :: 'a \<Rightarrow> 'b. card M \<le> n \<and> (\<forall>m\<in>M. D (f m, f' m)) \<Longrightarrow> E (sum f M, sum f' M)\<close>
proof (atomize_elim, insert EE, induction n arbitrary: E rule:nat_induct)
  case 0
  then show ?case
    by (metis card_eq_0_iff equals0D le_zero_eq sum.infinite sum.not_neutral_contains_not_neutral uniformity_refl)
next
  case (Suc n)
  from plus_cont[unfolded uniformly_continuous_on_uniformity filterlim_def le_filter_def, rule_format, OF Suc.prems]
  obtain D1 D2 where \<open>eventually D1 uniformity\<close> and \<open>eventually D2 uniformity\<close>
    and D1D2E: \<open>D1 (x, y) \<Longrightarrow> D2 (x', y') \<Longrightarrow> E (x + x', y + y')\<close> for x y x' y'
    apply atomize_elim
    by (auto simp: eventually_prod_filter case_prod_beta uniformity_prod_def eventually_filtermap)

  from Suc.IH[OF \<open>eventually D2 uniformity\<close>]
  obtain D3 where \<open>eventually D3 uniformity\<close> and D3: \<open>card M \<le> n \<Longrightarrow> (\<forall>m\<in>M. D3 (f m, f' m)) \<Longrightarrow> D2 (sum f M, sum f' M)\<close>
    for M :: \<open>'a set\<close> and f f'
    by metis

  define D where \<open>D x \<equiv> D1 x \<and> D3 x\<close> for x
  have \<open>eventually D uniformity\<close>
    using D_def \<open>eventually D1 uniformity\<close> \<open>eventually D3 uniformity\<close> eventually_elim2 by blast

  have \<open>E (sum f M, sum f' M)\<close>
    if \<open>card M \<le> Suc n\<close> and DM: \<open>\<forall>m\<in>M. D (f m, f' m)\<close>
    for M :: \<open>'a set\<close> and f f'
  proof (cases \<open>card M = 0\<close>)
    case True
    then show ?thesis
      by (metis Suc.prems card_eq_0_iff sum.empty sum.infinite uniformity_refl)
  next
    case False
    with \<open>card M \<le> Suc n\<close> obtain N x where \<open>card N \<le> n\<close> and \<open>x \<notin> N\<close> and \<open>M = insert x N\<close>
      by (metis card_Suc_eq less_Suc_eq_0_disj less_Suc_eq_le)

    from DM have \<open>\<And>m. m\<in>N \<Longrightarrow> D (f m, f' m)\<close>
      using \<open>M = insert x N\<close> by blast
    with D3[OF \<open>card N \<le> n\<close>]
    have D2_N: \<open>D2 (sum f N, sum f' N)\<close>
      using D_def by blast

    from DM
    have \<open>D (f x, f' x)\<close>
      using \<open>M = insert x N\<close> by blast
    then have \<open>D1 (f x, f' x)\<close>
      by (simp add: D_def)

    with D2_N
    have \<open>E (f x + sum f N, f' x + sum f' N)\<close>
      using D1D2E by presburger

    then show \<open>E (sum f M, sum f' M)\<close>
      by (metis False \<open>M = insert x N\<close> \<open>x \<notin> N\<close> card.infinite finite_insert sum.insert)
  qed
  with \<open>eventually D uniformity\<close> show ?case
    by auto
qed

lemma has_sum_Sigma:
  fixes A :: "'a set" and B :: "'a \ 'b set"
    and f :: \<open>'a \<times> 'b \<Rightarrow> 'c::{comm_monoid_add,uniform_space}\<close>
  assumes plus_cont: \<open>uniformly_continuous_on UNIV (\<lambda>(x::'c,y). x+y)\<close>
  assumes summableAB: "(f has_sum a) (Sigma A B)"
  assumes summableB: \<open>\<And>x. x\<in>A \<Longrightarrow> ((\<lambda>y. f (x, y)) has_sum b x) (B x)\<close>
  shows "(b has_sum a) A"
proof -
--> --------------------

--> maximum size reached

--> --------------------

quality91%

¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.