--- a/CONTRIBUTORS Thu Oct 07 10:34:48 2021 +0200
+++ b/CONTRIBUTORS Wed Oct 06 14:19:46 2021 +0200
@@ -16,6 +16,11 @@
* July .. September 2021: Jasmin Blanchette, Martin Desharnais
Various improvements to Sledgehammer.
+* September 2021: Dominique Unruh
+ New theory of infinite sums (HOL-Analysis/Infinite_Sum),
+ ordering of complex numbers (HOL-Library/Complex_Order),
+ and products of uniform spaces (in HOL-Analysis/Product_Vector).
+
* July 2021: Florian Haftmann
Further consolidation of bit operations and word types.
--- a/NEWS Thu Oct 07 10:34:48 2021 +0200
+++ b/NEWS Wed Oct 06 14:19:46 2021 +0200
@@ -144,6 +144,15 @@
*** HOL ***
+* Theory "HOL-Analysis.Infinite_Sum": new theory for infinite sums with
+a more general definition than the existing theory Infinite_Set_Sum.
+(Infinite_Set_Sum contains theorems relating the two definitions.)
+
+* Theory "HOL-Analysis.Product_Vector": Instantiation of the product of
+uniform spaces as a uniform space. Minor INCOMPATIBILITY: the old
+definition "uniformity_prod_def" is available as a derived fact
+"uniformity_dist".
+
* Theorems "antisym" and "eq_iff" in class "order" have been renamed to
"order.antisym" and "order.eq_iff", to coexist locally with "antisym"
and "eq_iff" from locale "ordering". INCOMPATIBILITY: significant
@@ -232,6 +241,9 @@
multiset_inter_count ~> count_inter_mset
sup_subset_mset_count ~> count_union_mset
+* Theory "HOL-Library.Complex_Order": Defines less, less_eq on complex
+numbers. Not imported by default.
+
* Theory "HOL-Library.Multiset": syntax precendence for membership
operations has been adjusted to match the corresponding precendences on
sets. Rare INCOMPATIBILITY.
--- a/src/HOL/Analysis/Analysis.thy Thu Oct 07 10:34:48 2021 +0200
+++ b/src/HOL/Analysis/Analysis.thy Wed Oct 06 14:19:46 2021 +0200
@@ -34,6 +34,7 @@
Product_Topology
Lindelof_Spaces
Infinite_Products
+ Infinite_Sum
Infinite_Set_Sum
Polytope
Jordan_Curve
--- a/src/HOL/Analysis/Infinite_Set_Sum.thy Thu Oct 07 10:34:48 2021 +0200
+++ b/src/HOL/Analysis/Infinite_Set_Sum.thy Wed Oct 06 14:19:46 2021 +0200
@@ -7,9 +7,12 @@
section \<open>Sums over Infinite Sets\<close>
theory Infinite_Set_Sum
- imports Set_Integral
+ imports Set_Integral Infinite_Sum
begin
+text \<open>Conflicting notation from \<^theory>\<open>HOL-Analysis.Infinite_Sum\<close>\<close>
+no_notation Infinite_Sum.abs_summable_on (infixr "abs'_summable'_on" 46)
+
(* TODO Move *)
lemma sets_eq_countable:
assumes "countable A" "space M = A" "\<And>x. x \<in> A \<Longrightarrow> {x} \<in> sets M"
@@ -865,4 +868,518 @@
(auto simp: infsetsum_cmult_left infsetsum_cmult_right)
qed
+lemma abs_summable_finite_sumsI:
+ assumes "\<And>F. finite F \<Longrightarrow> F\<subseteq>S \<Longrightarrow> sum (\<lambda>x. norm (f x)) F \<le> B"
+ shows "f abs_summable_on S"
+proof -
+ have main: "f abs_summable_on S \<and> infsetsum (\<lambda>x. norm (f x)) S \<le> B" if \<open>B \<ge> 0\<close> and \<open>S \<noteq> {}\<close>
+ proof -
+ define M normf where "M = count_space S" and "normf x = ennreal (norm (f x))" for x
+ have "sum normf F \<le> ennreal B"
+ if "finite F" and "F \<subseteq> S" and
+ "\<And>F. finite F \<Longrightarrow> F \<subseteq> S \<Longrightarrow> (\<Sum>i\<in>F. ennreal (norm (f i))) \<le> ennreal B" and
+ "ennreal 0 \<le> ennreal B" for F
+ using that unfolding normf_def[symmetric] by simp
+ hence normf_B: "finite F \<Longrightarrow> F\<subseteq>S \<Longrightarrow> sum normf F \<le> ennreal B" for F
+ using assms[THEN ennreal_leI]
+ by auto
+ have "integral\<^sup>S M g \<le> B" if "simple_function M g" and "g \<le> normf" for g
+ proof -
+ define gS where "gS = g ` S"
+ have "finite gS"
+ using that unfolding gS_def M_def simple_function_count_space by simp
+ have "gS \<noteq> {}" unfolding gS_def using \<open>S \<noteq> {}\<close> by auto
+ define part where "part r = g -` {r} \<inter> S" for r
+ have r_finite: "r < \<infinity>" if "r : gS" for r
+ using \<open>g \<le> normf\<close> that unfolding gS_def le_fun_def normf_def apply auto
+ using ennreal_less_top neq_top_trans top.not_eq_extremum by blast
+ define B' where "B' r = (SUP F\<in>{F. finite F \<and> F\<subseteq>part r}. sum normf F)" for r
+ have B'fin: "B' r < \<infinity>" for r
+ proof -
+ have "B' r \<le> (SUP F\<in>{F. finite F \<and> F\<subseteq>part r}. sum normf F)"
+ unfolding B'_def
+ by (metis (mono_tags, lifting) SUP_least SUP_upper)
+ also have "\<dots> \<le> B"
+ using normf_B unfolding part_def
+ by (metis (no_types, lifting) Int_subset_iff SUP_least mem_Collect_eq)
+ also have "\<dots> < \<infinity>"
+ by simp
+ finally show ?thesis by simp
+ qed
+ have sumB': "sum B' gS \<le> ennreal B + \<epsilon>" if "\<epsilon>>0" for \<epsilon>
+ proof -
+ define N \<epsilon>N where "N = card gS" and "\<epsilon>N = \<epsilon> / N"
+ have "N > 0"
+ unfolding N_def using \<open>gS\<noteq>{}\<close> \<open>finite gS\<close>
+ by (simp add: card_gt_0_iff)
+ from \<epsilon>N_def that have "\<epsilon>N > 0"
+ by (simp add: ennreal_of_nat_eq_real_of_nat ennreal_zero_less_divide)
+ have c1: "\<exists>y. B' r \<le> sum normf y + \<epsilon>N \<and> finite y \<and> y \<subseteq> part r"
+ if "B' r = 0" for r
+ using that by auto
+ have c2: "\<exists>y. B' r \<le> sum normf y + \<epsilon>N \<and> finite y \<and> y \<subseteq> part r" if "B' r \<noteq> 0" for r
+ proof-
+ have "B' r - \<epsilon>N < B' r"
+ using B'fin \<open>0 < \<epsilon>N\<close> ennreal_between that by fastforce
+ have "B' r - \<epsilon>N < Sup (sum normf ` {F. finite F \<and> F \<subseteq> part r}) \<Longrightarrow>
+ \<exists>F. B' r - \<epsilon>N \<le> sum normf F \<and> finite F \<and> F \<subseteq> part r"
+ by (metis (no_types, lifting) leD le_cases less_SUP_iff mem_Collect_eq)
+ hence "B' r - \<epsilon>N < B' r \<Longrightarrow> \<exists>F. B' r - \<epsilon>N \<le> sum normf F \<and> finite F \<and> F \<subseteq> part r"
+ by (subst (asm) (2) B'_def)
+ then obtain F where "B' r - \<epsilon>N \<le> sum normf F" and "finite F" and "F \<subseteq> part r"
+ using \<open>B' r - \<epsilon>N < B' r\<close> by auto
+ thus "\<exists>F. B' r \<le> sum normf F + \<epsilon>N \<and> finite F \<and> F \<subseteq> part r"
+ by (metis add.commute ennreal_minus_le_iff)
+ qed
+ have "\<forall>x. \<exists>y. B' x \<le> sum normf y + \<epsilon>N \<and>
+ finite y \<and> y \<subseteq> part x"
+ using c1 c2
+ by blast
+ hence "\<exists>F. \<forall>x. B' x \<le> sum normf (F x) + \<epsilon>N \<and> finite (F x) \<and> F x \<subseteq> part x"
+ by metis
+ then obtain F where F: "sum normf (F r) + \<epsilon>N \<ge> B' r" and Ffin: "finite (F r)" and Fpartr: "F r \<subseteq> part r" for r
+ using atomize_elim by auto
+ have w1: "finite gS"
+ by (simp add: \<open>finite gS\<close>)
+ have w2: "\<forall>i\<in>gS. finite (F i)"
+ by (simp add: Ffin)
+ have False
+ if "\<And>r. F r \<subseteq> g -` {r} \<and> F r \<subseteq> S"
+ and "i \<in> gS" and "j \<in> gS" and "i \<noteq> j" and "x \<in> F i" and "x \<in> F j"
+ for i j x
+ by (metis subsetD that(1) that(4) that(5) that(6) vimage_singleton_eq)
+ hence w3: "\<forall>i\<in>gS. \<forall>j\<in>gS. i \<noteq> j \<longrightarrow> F i \<inter> F j = {}"
+ using Fpartr[unfolded part_def] by auto
+ have w4: "sum normf (\<Union> (F ` gS)) + \<epsilon> = sum normf (\<Union> (F ` gS)) + \<epsilon>"
+ by simp
+ have "sum B' gS \<le> (\<Sum>r\<in>gS. sum normf (F r) + \<epsilon>N)"
+ using F by (simp add: sum_mono)
+ also have "\<dots> = (\<Sum>r\<in>gS. sum normf (F r)) + (\<Sum>r\<in>gS. \<epsilon>N)"
+ by (simp add: sum.distrib)
+ also have "\<dots> = (\<Sum>r\<in>gS. sum normf (F r)) + (card gS * \<epsilon>N)"
+ by auto
+ also have "\<dots> = (\<Sum>r\<in>gS. sum normf (F r)) + \<epsilon>"
+ unfolding \<epsilon>N_def N_def[symmetric] using \<open>N>0\<close>
+ by (simp add: ennreal_times_divide mult.commute mult_divide_eq_ennreal)
+ also have "\<dots> = sum normf (\<Union> (F ` gS)) + \<epsilon>"
+ using w1 w2 w3 w4
+ by (subst sum.UNION_disjoint[symmetric])
+ also have "\<dots> \<le> B + \<epsilon>"
+ using \<open>finite gS\<close> normf_B add_right_mono Ffin Fpartr unfolding part_def
+ by (simp add: \<open>gS \<noteq> {}\<close> cSUP_least)
+ finally show ?thesis
+ by auto
+ qed
+ hence sumB': "sum B' gS \<le> B"
+ using ennreal_le_epsilon ennreal_less_zero_iff by blast
+ have "\<forall>r. \<exists>y. r \<in> gS \<longrightarrow> B' r = ennreal y"
+ using B'fin less_top_ennreal by auto
+ hence "\<exists>B''. \<forall>r. r \<in> gS \<longrightarrow> B' r = ennreal (B'' r)"
+ by (rule_tac choice)
+ then obtain B'' where B'': "B' r = ennreal (B'' r)" if "r \<in> gS" for r
+ by atomize_elim
+ have cases[case_names zero finite infinite]: "P" if "r=0 \<Longrightarrow> P" and "finite (part r) \<Longrightarrow> P"
+ and "infinite (part r) \<Longrightarrow> r\<noteq>0 \<Longrightarrow> P" for P r
+ using that by metis
+ have emeasure_B': "r * emeasure M (part r) \<le> B' r" if "r : gS" for r
+ proof (cases rule:cases[of r])
+ case zero
+ thus ?thesis by simp
+ next
+ case finite
+ have s1: "sum g F \<le> sum normf F"
+ if "F \<in> {F. finite F \<and> F \<subseteq> part r}"
+ for F
+ using \<open>g \<le> normf\<close>
+ by (simp add: le_fun_def sum_mono)
+
+ have "r * of_nat (card (part r)) = r * (\<Sum>x\<in>part r. 1)" by simp
+ also have "\<dots> = (\<Sum>x\<in>part r. r)"
+ using mult.commute by auto
+ also have "\<dots> = (\<Sum>x\<in>part r. g x)"
+ unfolding part_def by auto
+ also have "\<dots> \<le> (SUP F\<in>{F. finite F \<and> F\<subseteq>part r}. sum g F)"
+ using finite
+ by (simp add: Sup_upper)
+ also have "\<dots> \<le> B' r"
+ unfolding B'_def
+ using s1 SUP_subset_mono by blast
+ finally have "r * of_nat (card (part r)) \<le> B' r" by assumption
+ thus ?thesis
+ unfolding M_def
+ using part_def finite by auto
+ next
+ case infinite
+ from r_finite[OF \<open>r : gS\<close>] obtain r' where r': "r = ennreal r'"
+ using ennreal_cases by auto
+ with infinite have "r' > 0"
+ using ennreal_less_zero_iff not_gr_zero by blast
+ obtain N::nat where N:"N > B / r'" and "real N > 0" apply atomize_elim
+ using reals_Archimedean2
+ by (metis less_trans linorder_neqE_linordered_idom)
+ obtain F where "finite F" and "card F = N" and "F \<subseteq> part r"
+ using infinite(1) infinite_arbitrarily_large by blast
+ from \<open>F \<subseteq> part r\<close> have "F \<subseteq> S" unfolding part_def by simp
+ have "B < r * N"
+ unfolding r' ennreal_of_nat_eq_real_of_nat
+ using N \<open>0 < r'\<close> \<open>B \<ge> 0\<close> r'
+ by (metis enn2real_ennreal enn2real_less_iff ennreal_less_top ennreal_mult' less_le mult_less_cancel_left_pos nonzero_mult_div_cancel_left times_divide_eq_right)
+ also have "r * N = (\<Sum>x\<in>F. r)"
+ using \<open>card F = N\<close> by (simp add: mult.commute)
+ also have "(\<Sum>x\<in>F. r) = (\<Sum>x\<in>F. g x)"
+ using \<open>F \<subseteq> part r\<close> part_def sum.cong subsetD by fastforce
+ also have "(\<Sum>x\<in>F. g x) \<le> (\<Sum>x\<in>F. ennreal (norm (f x)))"
+ by (metis (mono_tags, lifting) \<open>g \<le> normf\<close> \<open>normf \<equiv> \<lambda>x. ennreal (norm (f x))\<close> le_fun_def
+ sum_mono)
+ also have "(\<Sum>x\<in>F. ennreal (norm (f x))) \<le> B"
+ using \<open>F \<subseteq> S\<close> \<open>finite F\<close> \<open>normf \<equiv> \<lambda>x. ennreal (norm (f x))\<close> normf_B by blast
+ finally have "B < B" by auto
+ thus ?thesis by simp
+ qed
+
+ have "integral\<^sup>S M g = (\<Sum>r \<in> gS. r * emeasure M (part r))"
+ unfolding simple_integral_def gS_def M_def part_def by simp
+ also have "\<dots> \<le> (\<Sum>r \<in> gS. B' r)"
+ by (simp add: emeasure_B' sum_mono)
+ also have "\<dots> \<le> B"
+ using sumB' by blast
+ finally show ?thesis by assumption
+ qed
+ hence int_leq_B: "integral\<^sup>N M normf \<le> B"
+ unfolding nn_integral_def by (metis (no_types, lifting) SUP_least mem_Collect_eq)
+ hence "integral\<^sup>N M normf < \<infinity>"
+ using le_less_trans by fastforce
+ hence "integrable M f"
+ unfolding M_def normf_def by (rule integrableI_bounded[rotated], simp)
+ hence v1: "f abs_summable_on S"
+ unfolding abs_summable_on_def M_def by simp
+
+ have "(\<lambda>x. norm (f x)) abs_summable_on S"
+ using v1 Infinite_Set_Sum.abs_summable_on_norm_iff[where A = S and f = f]
+ by auto
+ moreover have "0 \<le> norm (f x)"
+ if "x \<in> S" for x
+ by simp
+ moreover have "(\<integral>\<^sup>+ x. ennreal (norm (f x)) \<partial>count_space S) \<le> ennreal B"
+ using M_def \<open>normf \<equiv> \<lambda>x. ennreal (norm (f x))\<close> int_leq_B by auto
+ ultimately have "ennreal (\<Sum>\<^sub>ax\<in>S. norm (f x)) \<le> ennreal B"
+ by (simp add: nn_integral_conv_infsetsum)
+ hence v2: "(\<Sum>\<^sub>ax\<in>S. norm (f x)) \<le> B"
+ by (subst ennreal_le_iff[symmetric], simp add: assms \<open>B \<ge> 0\<close>)
+ show ?thesis
+ using v1 v2 by auto
+ qed
+ then show "f abs_summable_on S"
+ by (metis abs_summable_on_finite assms empty_subsetI finite.emptyI sum_clauses(1))
+qed
+
+
+lemma infsetsum_nonneg_is_SUPREMUM_ennreal:
+ fixes f :: "'a \<Rightarrow> real"
+ assumes summable: "f abs_summable_on A"
+ and fnn: "\<And>x. x\<in>A \<Longrightarrow> f x \<ge> 0"
+ shows "ennreal (infsetsum f A) = (SUP F\<in>{F. finite F \<and> F \<subseteq> A}. (ennreal (sum f F)))"
+proof -
+ have sum_F_A: "sum f F \<le> infsetsum f A"
+ if "F \<in> {F. finite F \<and> F \<subseteq> A}"
+ for F
+ proof-
+ from that have "finite F" and "F \<subseteq> A" by auto
+ from \<open>finite F\<close> have "sum f F = infsetsum f F" by auto
+ also have "\<dots> \<le> infsetsum f A"
+ proof (rule infsetsum_mono_neutral_left)
+ show "f abs_summable_on F"
+ by (simp add: \<open>finite F\<close>)
+ show "f abs_summable_on A"
+ by (simp add: local.summable)
+ show "f x \<le> f x"
+ if "x \<in> F"
+ for x :: 'a
+ by simp
+ show "F \<subseteq> A"
+ by (simp add: \<open>F \<subseteq> A\<close>)
+ show "0 \<le> f x"
+ if "x \<in> A - F"
+ for x :: 'a
+ using that fnn by auto
+ qed
+ finally show ?thesis by assumption
+ qed
+ hence geq: "ennreal (infsetsum f A) \<ge> (SUP F\<in>{G. finite G \<and> G \<subseteq> A}. (ennreal (sum f F)))"
+ by (meson SUP_least ennreal_leI)
+
+ define fe where "fe x = ennreal (f x)" for x
+
+ have sum_f_int: "infsetsum f A = \<integral>\<^sup>+ x. fe x \<partial>(count_space A)"
+ unfolding infsetsum_def fe_def
+ proof (rule nn_integral_eq_integral [symmetric])
+ show "integrable (count_space A) f"
+ using abs_summable_on_def local.summable by blast
+ show "AE x in count_space A. 0 \<le> f x"
+ using fnn by auto
+ qed
+ also have "\<dots> = (SUP g \<in> {g. finite (g`A) \<and> g \<le> fe}. integral\<^sup>S (count_space A) g)"
+ unfolding nn_integral_def simple_function_count_space by simp
+ also have "\<dots> \<le> (SUP F\<in>{F. finite F \<and> F \<subseteq> A}. (ennreal (sum f F)))"
+ proof (rule Sup_least)
+ fix x assume "x \<in> integral\<^sup>S (count_space A) ` {g. finite (g ` A) \<and> g \<le> fe}"
+ then obtain g where xg: "x = integral\<^sup>S (count_space A) g" and fin_gA: "finite (g`A)"
+ and g_fe: "g \<le> fe" by auto
+ define F where "F = {z:A. g z \<noteq> 0}"
+ hence "F \<subseteq> A" by simp
+
+ have fin: "finite {z:A. g z = t}" if "t \<noteq> 0" for t
+ proof (rule ccontr)
+ assume inf: "infinite {z:A. g z = t}"
+ hence tgA: "t \<in> g ` A"
+ by (metis (mono_tags, lifting) image_eqI not_finite_existsD)
+ have "x = (\<Sum>x \<in> g ` A. x * emeasure (count_space A) (g -` {x} \<inter> A))"
+ unfolding xg simple_integral_def space_count_space by simp
+ also have "\<dots> \<ge> (\<Sum>x \<in> {t}. x * emeasure (count_space A) (g -` {x} \<inter> A))" (is "_ \<ge> \<dots>")
+ proof (rule sum_mono2)
+ show "finite (g ` A)"
+ by (simp add: fin_gA)
+ show "{t} \<subseteq> g ` A"
+ by (simp add: tgA)
+ show "0 \<le> b * emeasure (count_space A) (g -` {b} \<inter> A)"
+ if "b \<in> g ` A - {t}"
+ for b :: ennreal
+ using that
+ by simp
+ qed
+ also have "\<dots> = t * emeasure (count_space A) (g -` {t} \<inter> A)"
+ by auto
+ also have "\<dots> = t * \<infinity>"
+ proof (subst emeasure_count_space_infinite)
+ show "g -` {t} \<inter> A \<subseteq> A"
+ by simp
+ have "{a \<in> A. g a = t} = {a \<in> g -` {t}. a \<in> A}"
+ by auto
+ thus "infinite (g -` {t} \<inter> A)"
+ by (metis (full_types) Int_def inf)
+ show "t * \<infinity> = t * \<infinity>"
+ by simp
+ qed
+ also have "\<dots> = \<infinity>" using \<open>t \<noteq> 0\<close>
+ by (simp add: ennreal_mult_eq_top_iff)
+ finally have x_inf: "x = \<infinity>"
+ using neq_top_trans by auto
+ have "x = integral\<^sup>S (count_space A) g" by (fact xg)
+ also have "\<dots> = integral\<^sup>N (count_space A) g"
+ by (simp add: fin_gA nn_integral_eq_simple_integral)
+ also have "\<dots> \<le> integral\<^sup>N (count_space A) fe"
+ using g_fe
+ by (simp add: le_funD nn_integral_mono)
+ also have "\<dots> < \<infinity>"
+ by (metis sum_f_int ennreal_less_top infinity_ennreal_def)
+ finally have x_fin: "x < \<infinity>" by simp
+ from x_inf x_fin show False by simp
+ qed
+ have F: "F = (\<Union>t\<in>g`A-{0}. {z\<in>A. g z = t})"
+ unfolding F_def by auto
+ hence "finite F"
+ unfolding F using fin_gA fin by auto
+ have "x = integral\<^sup>N (count_space A) g"
+ unfolding xg
+ by (simp add: fin_gA nn_integral_eq_simple_integral)
+ also have "\<dots> = set_nn_integral (count_space UNIV) A g"
+ by (simp add: nn_integral_restrict_space[symmetric] restrict_count_space)
+ also have "\<dots> = set_nn_integral (count_space UNIV) F g"
+ proof -
+ have "\<forall>a. g a * (if a \<in> {a \<in> A. g a \<noteq> 0} then 1 else 0) = g a * (if a \<in> A then 1 else 0)"
+ by auto
+ hence "(\<integral>\<^sup>+ a. g a * (if a \<in> A then 1 else 0) \<partial>count_space UNIV)
+ = (\<integral>\<^sup>+ a. g a * (if a \<in> {a \<in> A. g a \<noteq> 0} then 1 else 0) \<partial>count_space UNIV)"
+ by presburger
+ thus ?thesis unfolding F_def indicator_def
+ using mult.right_neutral mult_zero_right nn_integral_cong
+ by (simp add: of_bool_def)
+ qed
+ also have "\<dots> = integral\<^sup>N (count_space F) g"
+ by (simp add: nn_integral_restrict_space[symmetric] restrict_count_space)
+ also have "\<dots> = sum g F"
+ using \<open>finite F\<close> by (rule nn_integral_count_space_finite)
+ also have "sum g F \<le> sum fe F"
+ using g_fe unfolding le_fun_def
+ by (simp add: sum_mono)
+ also have "\<dots> \<le> (SUP F \<in> {G. finite G \<and> G \<subseteq> A}. (sum fe F))"
+ using \<open>finite F\<close> \<open>F\<subseteq>A\<close>
+ by (simp add: SUP_upper)
+ also have "\<dots> = (SUP F \<in> {F. finite F \<and> F \<subseteq> A}. (ennreal (sum f F)))"
+ proof (rule SUP_cong [OF refl])
+ have "finite x \<Longrightarrow> x \<subseteq> A \<Longrightarrow> (\<Sum>x\<in>x. ennreal (f x)) = ennreal (sum f x)"
+ for x
+ by (metis fnn subsetCE sum_ennreal)
+ thus "sum fe x = ennreal (sum f x)"
+ if "x \<in> {G. finite G \<and> G \<subseteq> A}"
+ for x :: "'a set"
+ using that unfolding fe_def by auto
+ qed
+ finally show "x \<le> \<dots>" by simp
+ qed
+ finally have leq: "ennreal (infsetsum f A) \<le> (SUP F\<in>{F. finite F \<and> F \<subseteq> A}. (ennreal (sum f F)))"
+ by assumption
+ from leq geq show ?thesis by simp
+qed
+
+lemma infsetsum_nonneg_is_SUPREMUM_ereal:
+ fixes f :: "'a \<Rightarrow> real"
+ assumes summable: "f abs_summable_on A"
+ and fnn: "\<And>x. x\<in>A \<Longrightarrow> f x \<ge> 0"
+ shows "ereal (infsetsum f A) = (SUP F\<in>{F. finite F \<and> F \<subseteq> A}. (ereal (sum f F)))"
+proof -
+ have "ereal (infsetsum f A) = enn2ereal (ennreal (infsetsum f A))"
+ by (simp add: fnn infsetsum_nonneg)
+ also have "\<dots> = enn2ereal (SUP F\<in>{F. finite F \<and> F \<subseteq> A}. ennreal (sum f F))"
+ apply (subst infsetsum_nonneg_is_SUPREMUM_ennreal)
+ using fnn by (auto simp add: local.summable)
+ also have "\<dots> = (SUP F\<in>{F. finite F \<and> F \<subseteq> A}. (ereal (sum f F)))"
+ proof (simp add: image_def Sup_ennreal.rep_eq)
+ have "0 \<le> Sup {y. \<exists>x. (\<exists>xa. finite xa \<and> xa \<subseteq> A \<and> x = ennreal (sum f xa)) \<and>
+ y = enn2ereal x}"
+ by (metis (mono_tags, lifting) Sup_upper empty_subsetI ennreal_0 finite.emptyI
+ mem_Collect_eq sum.empty zero_ennreal.rep_eq)
+ moreover have "Sup {y. \<exists>x. (\<exists>y. finite y \<and> y \<subseteq> A \<and> x = ennreal (sum f y)) \<and>
+ y = enn2ereal x} = Sup {y. \<exists>x. finite x \<and> x \<subseteq> A \<and> y = ereal (sum f x)}"
+ using enn2ereal_ennreal fnn in_mono sum_nonneg Collect_cong
+ by smt
+ ultimately show "max 0 (Sup {y. \<exists>x. (\<exists>xa. finite xa \<and> xa \<subseteq> A \<and> x
+ = ennreal (sum f xa)) \<and> y = enn2ereal x})
+ = Sup {y. \<exists>x. finite x \<and> x \<subseteq> A \<and> y = ereal (sum f x)}"
+ by linarith
+ qed
+ finally show ?thesis
+ by simp
+qed
+
+
+text \<open>The following theorem relates \<^const>\<open>Infinite_Set_Sum.abs_summable_on\<close> with \<^const>\<open>Infinite_Sum.abs_summable_on\<close>.
+ Note that while this theorem expresses an equivalence, the notion on the lhs is more general
+ nonetheless because it applies to a wider range of types. (The rhs requires second-countable
+ Banach spaces while the lhs is well-defined on arbitrary real vector spaces.)\<close>
+
+lemma abs_summable_equivalent: \<open>Infinite_Sum.abs_summable_on f A \<longleftrightarrow> f abs_summable_on A\<close>
+proof (rule iffI)
+ define n where \<open>n x = norm (f x)\<close> for x
+ assume \<open>n summable_on A\<close>
+ then have \<open>sum n F \<le> infsum n A\<close> if \<open>finite F\<close> and \<open>F\<subseteq>A\<close> for F
+ using that by (auto simp flip: infsum_finite simp: n_def[abs_def] intro!: infsum_mono_neutral)
+
+ then show \<open>f abs_summable_on A\<close>
+ by (auto intro!: abs_summable_finite_sumsI simp: n_def)
+next
+ define n where \<open>n x = norm (f x)\<close> for x
+ assume \<open>f abs_summable_on A\<close>
+ then have \<open>n abs_summable_on A\<close>
+ by (simp add: \<open>f abs_summable_on A\<close> n_def)
+ then have \<open>sum n F \<le> infsetsum n A\<close> if \<open>finite F\<close> and \<open>F\<subseteq>A\<close> for F
+ using that by (auto simp flip: infsetsum_finite simp: n_def[abs_def] intro!: infsetsum_mono_neutral)
+ then show \<open>n summable_on A\<close>
+ apply (rule_tac pos_summable_on)
+ by (auto simp add: n_def bdd_above_def)
+qed
+
+lemma infsetsum_infsum:
+ assumes "f abs_summable_on A"
+ shows "infsetsum f A = infsum f A"
+proof -
+ have conv_sum_norm[simp]: "(\<lambda>x. norm (f x)) summable_on A"
+ using abs_summable_equivalent assms by blast
+ have "norm (infsetsum f A - infsum f A) \<le> \<epsilon>" if "\<epsilon>>0" for \<epsilon>
+ proof -
+ define \<delta> where "\<delta> = \<epsilon>/2"
+ with that have [simp]: "\<delta> > 0" by simp
+ obtain F1 where F1A: "F1 \<subseteq> A" and finF1: "finite F1" and leq_eps: "infsetsum (\<lambda>x. norm (f x)) (A-F1) \<le> \<delta>"
+ proof -
+ have sum_SUP: "ereal (infsetsum (\<lambda>x. norm (f x)) A) = (SUP F\<in>{F. finite F \<and> F \<subseteq> A}. ereal (sum (\<lambda>x. norm (f x)) F))"
+ (is "_ = ?SUP")
+ apply (rule infsetsum_nonneg_is_SUPREMUM_ereal)
+ using assms by auto
+
+ have "(SUP F\<in>{F. finite F \<and> F \<subseteq> A}. ereal (\<Sum>x\<in>F. norm (f x))) - ereal \<delta>
+ < (SUP i\<in>{F. finite F \<and> F \<subseteq> A}. ereal (\<Sum>x\<in>i. norm (f x)))"
+ using \<open>\<delta>>0\<close>
+ by (metis diff_strict_left_mono diff_zero ereal_less_eq(3) ereal_minus(1) not_le sum_SUP)
+ then obtain F where "F\<in>{F. finite F \<and> F \<subseteq> A}" and "ereal (sum (\<lambda>x. norm (f x)) F) > ?SUP - ereal (\<delta>)"
+ by (meson less_SUP_iff)
+
+ hence "sum (\<lambda>x. norm (f x)) F > infsetsum (\<lambda>x. norm (f x)) A - (\<delta>)"
+ unfolding sum_SUP[symmetric] by auto
+ hence "\<delta> > infsetsum (\<lambda>x. norm (f x)) (A-F)"
+ proof (subst infsetsum_Diff)
+ show "(\<lambda>x. norm (f x)) abs_summable_on A"
+ if "(\<Sum>\<^sub>ax\<in>A. norm (f x)) - \<delta> < (\<Sum>x\<in>F. norm (f x))"
+ using that
+ by (simp add: assms)
+ show "F \<subseteq> A"
+ if "(\<Sum>\<^sub>ax\<in>A. norm (f x)) - \<delta> < (\<Sum>x\<in>F. norm (f x))"
+ using that \<open>F \<in> {F. finite F \<and> F \<subseteq> A}\<close> by blast
+ show "(\<Sum>\<^sub>ax\<in>A. norm (f x)) - (\<Sum>\<^sub>ax\<in>F. norm (f x)) < \<delta>"
+ if "(\<Sum>\<^sub>ax\<in>A. norm (f x)) - \<delta> < (\<Sum>x\<in>F. norm (f x))"
+ using that \<open>F \<in> {F. finite F \<and> F \<subseteq> A}\<close> by auto
+ qed
+ thus ?thesis using that
+ apply atomize_elim
+ using \<open>F \<in> {F. finite F \<and> F \<subseteq> A}\<close> less_imp_le by blast
+ qed
+ obtain F2 where F2A: "F2 \<subseteq> A" and finF2: "finite F2"
+ and dist: "dist (sum (\<lambda>x. norm (f x)) F2) (infsum (\<lambda>x. norm (f x)) A) \<le> \<delta>"
+ apply atomize_elim
+ by (metis \<open>0 < \<delta>\<close> conv_sum_norm infsum_finite_approximation)
+ have leq_eps': "infsum (\<lambda>x. norm (f x)) (A-F2) \<le> \<delta>"
+ apply (subst infsum_Diff)
+ using finF2 F2A dist by (auto simp: dist_norm)
+ define F where "F = F1 \<union> F2"
+ have FA: "F \<subseteq> A" and finF: "finite F"
+ unfolding F_def using F1A F2A finF1 finF2 by auto
+
+ have "(\<Sum>\<^sub>ax\<in>A - (F1 \<union> F2). norm (f x)) \<le> (\<Sum>\<^sub>ax\<in>A - F1. norm (f x))"
+ apply (rule infsetsum_mono_neutral_left)
+ using abs_summable_on_subset assms by fastforce+
+ hence leq_eps: "infsetsum (\<lambda>x. norm (f x)) (A-F) \<le> \<delta>"
+ unfolding F_def
+ using leq_eps by linarith
+ have "infsum (\<lambda>x. norm (f x)) (A - (F1 \<union> F2))
+ \<le> infsum (\<lambda>x. norm (f x)) (A - F2)"
+ apply (rule infsum_mono_neutral)
+ using finF by (auto simp add: finF2 summable_on_cofin_subset F_def)
+ hence leq_eps': "infsum (\<lambda>x. norm (f x)) (A-F) \<le> \<delta>"
+ unfolding F_def
+ by (rule order.trans[OF _ leq_eps'])
+ have "norm (infsetsum f A - infsetsum f F) = norm (infsetsum f (A-F))"
+ apply (subst infsetsum_Diff [symmetric])
+ by (auto simp: FA assms)
+ also have "\<dots> \<le> infsetsum (\<lambda>x. norm (f x)) (A-F)"
+ using norm_infsetsum_bound by blast
+ also have "\<dots> \<le> \<delta>"
+ using leq_eps by simp
+ finally have diff1: "norm (infsetsum f A - infsetsum f F) \<le> \<delta>"
+ by assumption
+ have "norm (infsum f A - infsum f F) = norm (infsum f (A-F))"
+ apply (subst infsum_Diff [symmetric])
+ by (auto simp: assms abs_summable_summable finF FA)
+ also have "\<dots> \<le> infsum (\<lambda>x. norm (f x)) (A-F)"
+ by (simp add: finF summable_on_cofin_subset norm_infsum_bound)
+ also have "\<dots> \<le> \<delta>"
+ using leq_eps' by simp
+ finally have diff2: "norm (infsum f A - infsum f F) \<le> \<delta>"
+ by assumption
+
+ have x1: "infsetsum f F = infsum f F"
+ using finF by simp
+ have "norm (infsetsum f A - infsum f A) \<le> norm (infsetsum f A - infsetsum f F) + norm (infsum f A - infsum f F)"
+ apply (rule_tac norm_diff_triangle_le)
+ apply auto
+ by (simp_all add: x1 norm_minus_commute)
+ also have "\<dots> \<le> \<epsilon>"
+ using diff1 diff2 \<delta>_def by linarith
+ finally show ?thesis
+ by assumption
+ qed
+ hence "norm (infsetsum f A - infsum f A) = 0"
+ by (meson antisym_conv1 dense_ge norm_not_less_zero)
+ thus ?thesis
+ by auto
+qed
+
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Analysis/Infinite_Sum.thy Wed Oct 06 14:19:46 2021 +0200
@@ -0,0 +1,1977 @@
+(*
+ Title: HOL/Analysis/Infinite_Sum.thy
+ Author: Dominique Unruh, University of Tartu
+
+ A theory of sums over possible 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{conway2013course}.
+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
+ "HOL-Analysis.Elementary_Topology"
+ "HOL-Library.Extended_Nonnegative_Real"
+ "HOL-Library.Complex_Order"
+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
+ \<open>has_sum f A x \<longleftrightarrow> (sum f \<longlongrightarrow> x) (finite_subsets_at_top A)\<close>
+
+definition summable_on :: "('a \<Rightarrow> 'b::{comm_monoid_add, topological_space}) \<Rightarrow> 'a set \<Rightarrow> bool" (infixr "summable'_on" 46) where
+ "f summable_on A \<longleftrightarrow> (\<exists>x. has_sum f A x)"
+
+definition infsum :: "('a \<Rightarrow> 'b::{comm_monoid_add,t2_space}) \<Rightarrow> 'a set \<Rightarrow> '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 \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a set \<Rightarrow> bool" (infixr "abs'_summable'_on" 46) where
+ "f abs_summable_on A \<equiv> (\<lambda>x. norm (f x)) summable_on A"
+
+syntax (ASCII)
+ "_infsum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::topological_comm_monoid_add" ("(3INFSUM (_/:_)./ _)" [0, 51, 10] 10)
+syntax
+ "_infsum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::topological_comm_monoid_add" ("(2\<Sum>\<^sub>\<infinity>(_/\<in>_)./ _)" [0, 51, 10] 10)
+translations \<comment> \<open>Beware of argument permutation!\<close>
+ "\<Sum>\<^sub>\<infinity>i\<in>A. b" \<rightleftharpoons> "CONST infsum (\<lambda>i. b) A"
+
+syntax (ASCII)
+ "_univinfsum" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a" ("(3INFSUM _./ _)" [0, 10] 10)
+syntax
+ "_univinfsum" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a" ("(2\<Sum>\<^sub>\<infinity>_./ _)" [0, 10] 10)
+translations
+ "\<Sum>\<^sub>\<infinity>x. t" \<rightleftharpoons> "CONST infsum (\<lambda>x. t) (CONST UNIV)"
+
+syntax (ASCII)
+ "_qinfsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3INFSUM _ |/ _./ _)" [0, 0, 10] 10)
+syntax
+ "_qinfsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(2\<Sum>\<^sub>\<infinity>_ | (_)./ _)" [0, 0, 10] 10)
+translations
+ "\<Sum>\<^sub>\<infinity>x|P. t" => "CONST infsum (\<lambda>x. t) {x. P}"
+
+print_translation \<open>
+let
+ fun sum_tr' [Abs (x, Tx, t), Const (@{const_syntax Collect}, _) $ Abs (y, Ty, P)] =
+ if x <> y then raise Match
+ else
+ let
+ val x' = Syntax_Trans.mark_bound_body (x, Tx);
+ val t' = subst_bound (x', t);
+ val P' = subst_bound (x', P);
+ in
+ Syntax.const @{syntax_const "_qinfsum"} $ Syntax_Trans.mark_bound_abs (x, Tx) $ P' $ t'
+ end
+ | sum_tr' _ = raise Match;
+in [(@{const_syntax infsum}, K sum_tr')] end
+\<close>
+
+subsection \<open>General properties\<close>
+
+lemma infsumI:
+ fixes f g :: \<open>'a \<Rightarrow> 'b::{comm_monoid_add, t2_space}\<close>
+ assumes \<open>has_sum f A x\<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>has_sum f A x\<close>
+ assumes \<open>has_sum g B y\<close>
+ shows \<open>infsum f A = infsum g B\<close>
+ by (metis assms(1) assms(2) assms(3) 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>\<And>x. has_sum f A x \<longleftrightarrow> has_sum g B x\<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_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 "has_sum f S x \<longleftrightarrow> has_sum g T x"
+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 \<open>F0' = F0 \<inter> T\<close>
+ have [simp]: \<open>finite F0'\<close> \<open>F0' \<subseteq> T\<close>
+ by (simp_all add: F0'_def \<open>finite F0\<close>)
+ 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>
+ apply (rule F0_P)
+ using \<open>F0 \<subseteq> S\<close> \<open>finite F0\<close> that by auto
+ also have \<open>sum f ((F\<inter>S) \<union> (F0\<inter>S)) = sum g F\<close>
+ apply (rule sum.mono_neutral_cong)
+ using that \<open>finite F0\<close> F0'_def assms by auto
+ finally show ?thesis
+ by -
+ 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 \<open>F0' = F0 \<inter> S\<close>
+ have [simp]: \<open>finite F0'\<close> \<open>F0' \<subseteq> S\<close>
+ by (simp_all add: F0'_def \<open>finite F0\<close>)
+ 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>
+ apply (rule F0_P)
+ using \<open>F0 \<subseteq> T\<close> \<open>finite F0\<close> that by auto
+ also have \<open>sum g ((F\<inter>T) \<union> (F0\<inter>T)) = sum f F\<close>
+ apply (rule sum.mono_neutral_cong)
+ using that \<open>finite F0\<close> F0'_def assms by auto
+ finally show ?thesis
+ by -
+ 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 \<longlongrightarrow> x) (finite_subsets_at_top S) \<longleftrightarrow> (sum g \<longlongrightarrow> 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 \<longleftrightarrow> 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>
+ apply (rule infsum_eqI')
+ using assms by (rule has_sum_cong_neutral)
+
+lemma has_sum_cong:
+ assumes "\<And>x. x\<in>A \<Longrightarrow> f x = g x"
+ shows "has_sum f A x \<longleftrightarrow> has_sum g A x"
+ by (smt (verit, best) DiffE IntD2 assms has_sum_cong_neutral)
+
+lemma summable_on_cong:
+ assumes "\<And>x. x\<in>A \<Longrightarrow> f x = g x"
+ shows "f summable_on A \<longleftrightarrow> g summable_on A"
+ by (metis assms summable_on_def has_sum_cong)
+
+lemma infsum_cong:
+ assumes "\<And>x. x\<in>A \<Longrightarrow> 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 \<Rightarrow> '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 \<longlongrightarrow> 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 ((\<union>)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 \<subseteq> A"
+ and P: "\<forall>Y. finite Y \<and> X \<subseteq> Y \<and> Y \<subseteq> A \<longrightarrow> P Y"
+ unfolding eventually_finite_subsets_at_top by auto
+ define X' where "X' = X-F"
+ hence [simp]: "finite X'" and [simp]: "X' \<subseteq> A-F"
+ using XA by auto
+ hence "finite Y \<and> X' \<subseteq> Y \<and> Y \<subseteq> A - F \<longrightarrow> P (F' \<union> Y)" for Y
+ using P XA unfolding X'_def using F'_def \<open>finite F'\<close> by blast
+ thus "eventually P (filtermap ((\<union>) 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 \<longlongrightarrow> x) (filtermap ((\<union>)F') (finite_subsets_at_top (A-F)))"
+ using tendsto_mono by blast
+ have "((\<lambda>G. sum f (F' \<union> G)) \<longlongrightarrow> x) (finite_subsets_at_top (A - F))"
+ if "((sum f \<circ> (\<union>) F') \<longlongrightarrow> x) (finite_subsets_at_top (A - F))"
+ using that unfolding o_def by auto
+ hence "((\<lambda>G. sum f (F' \<union> G)) \<longlongrightarrow> 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 "\<forall>Y. finite Y \<and> Y \<subseteq> A - F \<longrightarrow> sum f (F' \<union> 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 "\<forall>\<^sub>F x in finite_subsets_at_top (A - F). sum f (F' \<union> 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 "((\<lambda>G. sum f F' + sum f G) \<longlongrightarrow> 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 "((\<lambda>G. sum f F' + sum f G) \<longlongrightarrow> sum f F' + (x-sum f F')) (finite_subsets_at_top (A-F))"
+ by simp
+ hence "(sum f \<longlongrightarrow> 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 \<Rightarrow> 'b::{topological_ab_group_add}"
+ assumes \<open>has_sum f B b\<close> and \<open>has_sum f A a\<close> and AB: "A \<subseteq> B"
+ shows has_sum_Diff: "has_sum f (B - A) (b - a)"
+proof -
+ have finite_subsets1:
+ "finite_subsets_at_top (B - A) \<le> filtermap (\<lambda>F. F - A) (finite_subsets_at_top B)"
+ proof (rule filter_leI)
+ fix P assume "eventually P (filtermap (\<lambda>F. F - A) (finite_subsets_at_top B))"
+ then obtain X where "finite X" and "X \<subseteq> B"
+ and P: "finite Y \<and> X \<subseteq> Y \<and> Y \<subseteq> B \<longrightarrow> P (Y - A)" for Y
+ unfolding eventually_filtermap eventually_finite_subsets_at_top by auto
+
+ hence "finite (X-A)" and "X-A \<subseteq> B - A"
+ by auto
+ moreover have "finite Y \<and> X-A \<subseteq> Y \<and> Y \<subseteq> B - A \<longrightarrow> P Y" for Y
+ using P[where Y="Y\<union>X"] \<open>finite X\<close> \<open>X \<subseteq> B\<close>
+ 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 (\<lambda>F. F \<inter> A) (finite_subsets_at_top B) \<le> 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 \<longlongrightarrow> b) (finite_subsets_at_top B)"
+ using has_sum_def by auto
+ from assms(2) have limA: "(sum f \<longlongrightarrow> a) (finite_subsets_at_top A)"
+ using has_sum_def by blast
+ have "((\<lambda>F. sum f (F\<inter>A)) \<longlongrightarrow> a) (finite_subsets_at_top B)"
+ proof (subst asm_rl [of "(\<lambda>F. sum f (F\<inter>A)) = sum f o (\<lambda>F. F\<inter>A)"])
+ show "(\<lambda>F. sum f (F \<inter> A)) = sum f \<circ> (\<lambda>F. F \<inter> A)"
+ unfolding o_def by auto
+ show "((sum f \<circ> (\<lambda>F. F \<inter> A)) \<longlongrightarrow> 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 "((\<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 \<inter> A) = sum f (X - A)" if "finite X" and "X \<subseteq> B" for X :: "'a set"
+ using that by (metis add_diff_cancel_left' sum.Int_Diff)
+ hence "\<forall>\<^sub>F x in finite_subsets_at_top B. sum f x - sum f (x \<inter> A) = sum f (x - A)"
+ by (rule eventually_finite_subsets_at_top_weakI)
+ hence "((\<lambda>F. sum f (F-A)) \<longlongrightarrow> b - a) (finite_subsets_at_top B)"
+ using tendsto_cong [THEN iffD1 , rotated]
+ \<open>((\<lambda>F. sum f F - sum f (F \<inter> A)) \<longlongrightarrow> b - a) (finite_subsets_at_top B)\<close> by fastforce
+ hence "(sum f \<longlongrightarrow> b - a) (filtermap (\<lambda>F. F-A) (finite_subsets_at_top B))"
+ by (subst tendsto_compose_filtermap[symmetric], simp add: o_def)
+ hence limBA: "(sum f \<longlongrightarrow> b - a) (finite_subsets_at_top (B-A))"
+ apply (rule tendsto_mono[rotated])
+ by (rule finite_subsets1)
+ thus ?thesis
+ by (simp add: has_sum_def)
+qed
+
+
+lemma
+ fixes f :: "'a \<Rightarrow> 'b::{topological_ab_group_add}"
+ assumes "f summable_on B" and "f summable_on A" and "A \<subseteq> B"
+ shows summable_on_Diff: "f summable_on (B-A)"
+ by (meson assms summable_on_def has_sum_Diff)
+
+lemma
+ fixes f :: "'a \<Rightarrow> 'b::{topological_ab_group_add,t2_space}"
+ assumes "f summable_on B" and "f summable_on A" and AB: "A \<subseteq> B"
+ shows infsum_Diff: "infsum f (B - A) = infsum f B - infsum f A"
+ by (smt (z3) AB assms(1) assms(2) finite_subsets_at_top_neq_bot infsum_def summable_on_def has_sum_Diff has_sum_def tendsto_Lim)
+
+lemma has_sum_mono_neutral:
+ fixes f :: "'a\<Rightarrow>'b::{ordered_comm_monoid_add,linorder_topology}"
+ (* Does this really require a linorder topology? (Instead of order topology.) *)
+ assumes \<open>has_sum f A a\<close> and "has_sum g 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 \<le> 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>has_sum f' (A\<union>B) a\<close>
+ apply (subst has_sum_cong_neutral[where g=f and T=A])
+ by (auto simp: f'_def assms(1))
+ then have f'_lim: \<open>(sum f' \<longlongrightarrow> a) (finite_subsets_at_top (A\<union>B))\<close>
+ by (meson has_sum_def)
+ have \<open>has_sum g' (A\<union>B) b\<close>
+ apply (subst has_sum_cong_neutral[where g=g and T=B])
+ by (auto simp: g'_def assms(2))
+ then have g'_lim: \<open>(sum g' \<longlongrightarrow> b) (finite_subsets_at_top (A\<union>B))\<close>
+ using has_sum_def by blast
+
+ have *: \<open>\<forall>\<^sub>F x in finite_subsets_at_top (A \<union> B). sum f' x \<le> sum g' x\<close>
+ apply (rule eventually_finite_subsets_at_top_weakI)
+ apply (rule sum_mono)
+ using assms by (auto simp: f'_def g'_def)
+ show ?thesis
+ apply (rule tendsto_le)
+ using * g'_lim f'_lim by auto
+qed
+
+lemma infsum_mono_neutral:
+ fixes f :: "'a\<Rightarrow>'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 \<le> infsum g B"
+ apply (rule has_sum_mono_neutral[of f A _ g B _])
+ using assms apply auto
+ by (metis finite_subsets_at_top_neq_bot infsum_def summable_on_def has_sum_def tendsto_Lim)+
+
+lemma has_sum_mono:
+ fixes f :: "'a\<Rightarrow>'b::{ordered_comm_monoid_add,linorder_topology}"
+ assumes "has_sum f A x" and "has_sum g A y"
+ assumes \<open>\<And>x. x \<in> A \<Longrightarrow> f x \<le> g x\<close>
+ shows "x \<le> y"
+ apply (rule has_sum_mono_neutral)
+ using assms by auto
+
+lemma infsum_mono:
+ fixes f :: "'a\<Rightarrow>'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 \<le> infsum g A"
+ apply (rule infsum_mono_neutral)
+ using assms by auto
+
+lemma has_sum_finite[simp]:
+ assumes "finite F"
+ shows "has_sum f F (sum 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"
+ using assms by (auto intro: tendsto_Lim simp: finite_subsets_at_top_finite infsum_def principal_eq_bot_iff)
+
+lemma has_sum_finite_approximation:
+ fixes f :: "'a \<Rightarrow> 'b::{comm_monoid_add,metric_space}"
+ assumes "has_sum f A x" and "\<epsilon> > 0"
+ shows "\<exists>F. finite F \<and> F \<subseteq> A \<and> dist (sum f F) x \<le> \<epsilon>"
+proof -
+ have "(sum f \<longlongrightarrow> x) (finite_subsets_at_top A)"
+ by (meson assms(1) has_sum_def)
+ hence *: "\<forall>\<^sub>F F in (finite_subsets_at_top A). dist (sum f F) x < \<epsilon>"
+ using assms(2) by (rule tendstoD)
+ show ?thesis
+ by (smt (verit) * eventually_finite_subsets_at_top order_refl)
+qed
+
+lemma infsum_finite_approximation:
+ fixes f :: "'a \<Rightarrow> 'b::{comm_monoid_add,metric_space}"
+ assumes "f summable_on A" and "\<epsilon> > 0"
+ shows "\<exists>F. finite F \<and> F \<subseteq> A \<and> dist (sum f F) (infsum f A) \<le> \<epsilon>"
+ by (metis assms(1) assms(2) finite_subsets_at_top_neq_bot infsum_def summable_on_def has_sum_finite_approximation has_sum_def tendsto_Lim)
+
+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 \<open>finite F'\<close> and \<open>F' \<subseteq> A\<close> and P_sup_F': \<open>finite F \<and> F \<supseteq> F' \<and> F \<subseteq> A \<Longrightarrow> P F\<close> for F
+ apply atomize_elim by (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)
+
+ from dist_F have \<open>dist (sum (\<lambda>x. norm (f x)) F) (sum (\<lambda>x. norm (f x)) F2) < 2*d\<close>
+ by (smt (z3) P_def dist_norm real_norm_def that(2))
+ then have \<open>norm (sum (\<lambda>x. norm (f x)) (F-F2)) < 2*d\<close>
+ unfolding dist_norm
+ by (metis F_def \<open>finite F\<close> sum_diff sup_commute sup_ge1)
+ then have \<open>norm (sum f (F-F2)) < 2*d\<close>
+ by (smt (verit, ccfv_threshold) real_norm_def sum_norm_le)
+ then have dist_F_F2: \<open>dist (sum f F) (sum f F2) < 2*d\<close>
+ by (metis F_def \<open>finite F\<close> dist_norm sum_diff sup_commute sup_ge1)
+
+ from dist_F have \<open>dist (sum (\<lambda>x. norm (f x)) F) (sum (\<lambda>x. norm (f x)) F1) < 2*d\<close>
+ by (smt (z3) P_def dist_norm real_norm_def that(1))
+ then have \<open>norm (sum (\<lambda>x. norm (f x)) (F-F1)) < 2*d\<close>
+ unfolding dist_norm
+ by (metis F_def \<open>finite F\<close> inf_sup_ord(3) order_trans sum_diff sup_ge2)
+ then have \<open>norm (sum f (F-F1)) < 2*d\<close>
+ by (smt (verit, ccfv_threshold) real_norm_def sum_norm_le)
+ then have dist_F_F1: \<open>dist (sum f F) (sum f F1) < 2*d\<close>
+ by (metis F_def \<open>finite F\<close> dist_norm inf_sup_ord(3) le_supE sum_diff)
+
+ from dist_F_F2 dist_F_F1 show \<open>dist (sum f F1) (sum f F2) < e\<close>
+ unfolding d_def apply auto
+ by (meson dist_triangle_half_r less_divide_eq_numeral1(1))
+ 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)
+ then obtain L' where \<open>(sum f \<longlongrightarrow> L') (finite_subsets_at_top A)\<close>
+ apply atomize_elim unfolding filterlim_def
+ apply (rule complete_uniform[where S=UNIV, simplified, THEN iffD1, rule_format])
+ apply (auto simp add: filtermap_bot_iff)
+ by (meson Cauchy_convergent UNIV_I complete_def convergent_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 \<Rightarrow> 'a::real_normed_vector"
+ and A :: "'b set"
+ assumes "has_sum (\<lambda>x. norm (f x)) A n"
+ assumes "has_sum f A a"
+ shows "norm a \<le> n"
+proof -
+ have "norm a \<le> n + \<epsilon>" if "\<epsilon>>0" for \<epsilon>
+ proof-
+ have "\<exists>F. norm (a - sum f F) \<le> \<epsilon> \<and> finite F \<and> F \<subseteq> 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) \<le> \<epsilon>"
+ and "finite F" and "F \<subseteq> A"
+ by (simp add: atomize_elim)
+ hence "norm a \<le> norm (sum f F) + \<epsilon>"
+ by (smt norm_triangle_sub)
+ also have "\<dots> \<le> sum (\<lambda>x. norm (f x)) F + \<epsilon>"
+ using norm_sum by auto
+ also have "\<dots> \<le> n + \<epsilon>"
+ apply (rule add_right_mono)
+ apply (rule has_sum_mono_neutral[where A=F and B=A and f=\<open>\<lambda>x. norm (f x)\<close> and g=\<open>\<lambda>x. norm (f x)\<close>])
+ using \<open>finite F\<close> \<open>F \<subseteq> A\<close> assms by 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 \<Rightarrow> 'a::real_normed_vector"
+ and A :: "'b set"
+ assumes "f abs_summable_on A"
+ shows "norm (infsum f A) \<le> infsum (\<lambda>x. norm (f x)) A"
+proof (cases "f summable_on A")
+ case True
+ show ?thesis
+ apply (rule norm_has_sum_bound[where A=A and f=f and a=\<open>infsum f A\<close> and n=\<open>infsum (\<lambda>x. norm (f x)) A\<close>])
+ using assms True
+ by (metis finite_subsets_at_top_neq_bot infsum_def summable_on_def has_sum_def tendsto_Lim)+
+next
+ case False
+ obtain t where t_def: "(sum (\<lambda>x. norm (f x)) \<longlongrightarrow> t) (finite_subsets_at_top A)"
+ using assms unfolding summable_on_def has_sum_def by blast
+ have sumpos: "sum (\<lambda>x. norm (f x)) X \<ge> 0"
+ for X
+ by (simp add: sum_nonneg)
+ have tgeq0:"t \<ge> 0"
+ proof(rule ccontr)
+ define S::"real set" where "S = {s. s < 0}"
+ assume "\<not> 0 \<le> t"
+ hence "t < 0" by simp
+ hence "t \<in> S"
+ unfolding S_def by blast
+ moreover have "open S"
+ proof-
+ have "closed {s::real. s \<ge> 0}"
+ using Elementary_Topology.closed_sequential_limits[where S = "{s::real. s \<ge> 0}"]
+ by (metis Lim_bounded2 mem_Collect_eq)
+ moreover have "{s::real. s \<ge> 0} = UNIV - S"
+ unfolding S_def by auto
+ ultimately have "closed (UNIV - S)"
+ by simp
+ thus ?thesis
+ by (simp add: Compl_eq_Diff_UNIV open_closed)
+ qed
+ ultimately have "\<forall>\<^sub>F X in finite_subsets_at_top A. (\<Sum>x\<in>X. norm (f x)) \<in> S"
+ using t_def unfolding tendsto_def by blast
+ hence "\<exists>X. (\<Sum>x\<in>X. norm (f x)) \<in> S"
+ by (metis (no_types, lifting) eventually_mono filterlim_iff finite_subsets_at_top_neq_bot tendsto_Lim)
+ then obtain X where "(\<Sum>x\<in>X. norm (f x)) \<in> S"
+ by blast
+ hence "(\<Sum>x\<in>X. norm (f x)) < 0"
+ unfolding S_def by auto
+ thus False using sumpos by smt
+ qed
+ have "\<exists>!h. (sum (\<lambda>x. norm (f x)) \<longlongrightarrow> 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 (\<lambda>x. norm (f x))))"
+ using t_def unfolding Topological_Spaces.Lim_def
+ by (metis the_equality)
+ hence "Lim (finite_subsets_at_top A) (sum (\<lambda>x. norm (f x))) \<ge> 0"
+ using tgeq0 by blast
+ thus ?thesis unfolding infsum_def
+ using False by auto
+qed
+
+lemma has_sum_infsum[simp]:
+ assumes \<open>f summable_on S\<close>
+ shows \<open>has_sum f S (infsum f S)\<close>
+ using assms by (auto simp: summable_on_def infsum_def has_sum_def tendsto_Lim)
+
+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 by (simp flip: has_sum_def)
+
+
+lemma has_sum_0:
+ assumes \<open>\<And>x. x\<in>M \<Longrightarrow> f x = 0\<close>
+ shows \<open>has_sum f M 0\<close>
+ unfolding has_sum_def
+ apply (subst tendsto_cong[where g=\<open>\<lambda>_. 0\<close>])
+ apply (rule eventually_finite_subsets_at_top_weakI)
+ using assms by (auto simp add: subset_iff)
+
+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>has_sum (\<lambda>_. 0) M 0\<close>
+ by (simp_all add: has_sum_0)
+
+
+lemma has_sum_add:
+ fixes f g :: "'a \<Rightarrow> 'b::{topological_comm_monoid_add}"
+ assumes \<open>has_sum f A a\<close>
+ assumes \<open>has_sum g A b\<close>
+ shows \<open>has_sum (\<lambda>x. f x + g x) A (a + b)\<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 \<Rightarrow> '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(1) assms(2) summable_on_def has_sum_add)
+
+lemma infsum_add:
+ fixes f g :: "'a \<Rightarrow> '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>has_sum (\<lambda>x. f x + g x) A (infsum f A + infsum g A)\<close>
+ by (simp add: assms(1) assms(2) has_sum_add)
+ then show ?thesis
+ by (smt (z3) finite_subsets_at_top_neq_bot infsum_def summable_on_def has_sum_def tendsto_Lim)
+qed
+
+
+lemma has_sum_Un_disjoint:
+ fixes f :: "'a \<Rightarrow> 'b::topological_comm_monoid_add"
+ assumes "has_sum f A a"
+ assumes "has_sum f B b"
+ assumes disj: "A \<inter> B = {}"
+ shows \<open>has_sum f (A \<union> B) (a + 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>has_sum fA (A \<union> B) a\<close>
+ apply (subst has_sum_cong_neutral[where T=A and g=f])
+ using assms by (auto simp: fA_def)
+ have fB: \<open>has_sum fB (A \<union> B) b\<close>
+ apply (subst has_sum_cong_neutral[where T=B and g=f])
+ using assms by (auto simp: fB_def)
+ 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 \<Rightarrow> 'b::topological_comm_monoid_add"
+ assumes "f summable_on A"
+ assumes "f summable_on B"
+ assumes disj: "A \<inter> B = {}"
+ shows \<open>f summable_on (A \<union> B)\<close>
+ by (meson assms(1) assms(2) disj summable_on_def has_sum_Un_disjoint)
+
+lemma infsum_Un_disjoint:
+ fixes f :: "'a \<Rightarrow> 'b::{topological_comm_monoid_add, t2_space}"
+ assumes "f summable_on A"
+ assumes "f summable_on B"
+ assumes disj: "A \<inter> B = {}"
+ shows \<open>infsum f (A \<union> B) = infsum f A + infsum f B\<close>
+ by (smt (verit, ccfv_threshold) assms(1) assms(2) disj finite_subsets_at_top_neq_bot summable_on_def has_sum_Un_disjoint has_sum_def has_sum_infsum tendsto_Lim)
+
+
+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:
+ 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 -
+ 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)
+
+ let ?filter_fB = \<open>filtermap (sum f) (finite_subsets_at_top B)\<close>
+
+ 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 \<open>eventually E' uniformity\<close> and E'E'E: \<open>E' (x, y) \<longrightarrow> E' (y, z) \<longrightarrow> E (x, z)\<close> for x y z
+ using uniformity_trans by blast
+ from plus_cont[simplified uniformly_continuous_on_uniformity filterlim_def le_filter_def, rule_format,
+ OF \<open>eventually E' uniformity\<close>]
+ 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
+ apply atomize_elim
+ by (auto simp: case_prod_beta eventually_filtermap uniformity_prod_def
+ eventually_prod_same uniformity_refl)
+ with 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 \<open>finite F1\<close> and \<open>F1 \<subseteq> A\<close> and \<open>\<forall>F. F\<supseteq>F1 \<and> finite F \<and> F\<subseteq>A \<longrightarrow> P1 (sum f F)\<close>
+ by (metis eventually_finite_subsets_at_top)
+ from ev_P2 obtain F2 where \<open>finite F2\<close> and \<open>F2 \<subseteq> A\<close> and \<open>\<forall>F. F\<supseteq>F2 \<and> finite F \<and> 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>
+ apply (simp add: F0_def \<open>finite F1\<close> \<open>finite F2\<close>)
+ by (simp add: F0_def \<open>F1 \<subseteq> A\<close> \<open>F2 \<subseteq> A\<close>)
+ have [simp]: \<open>finite F0A\<close>
+ by (simp add: F0A_def)
+ have \<open>\<forall>F1 F2. F1\<supseteq>F0 \<and> F2\<supseteq>F0 \<and> finite F1 \<and> finite F2 \<and> F1\<subseteq>A \<and> F2\<subseteq>A \<longrightarrow> D (sum f F1, sum f F2)\<close>
+ by (simp add: F0_def P1P2E \<open>\<forall>F. F1 \<subseteq> F \<and> finite F \<and> F \<subseteq> A \<longrightarrow> P1 (sum f F)\<close> \<open>\<forall>F. F2 \<subseteq> F \<and> finite F \<and> F \<subseteq> A \<longrightarrow> P2 (sum f F)\<close>)
+ then have \<open>\<forall>F1 F2. F1\<supseteq>F0B \<and> F2\<supseteq>F0B \<and> finite F1 \<and> finite F2 \<and> F1\<subseteq>B \<and> F2\<subseteq>B \<longrightarrow>
+ D (sum f (F1 \<union> F0A), sum f (F2 \<union> F0A))\<close>
+ by (smt (verit) Diff_Diff_Int Diff_subset_conv F0A_def F0B_def \<open>F0 \<subseteq> A\<close> \<open>finite F0A\<close> assms(4) finite_UnI sup.absorb_iff1 sup.mono sup_commute)
+ then have \<open>\<forall>F1 F2. F1\<supseteq>F0B \<and> F2\<supseteq>F0B \<and> finite F1 \<and> finite F2 \<and> F1\<subseteq>B \<and> F2\<subseteq>B \<longrightarrow>
+ D (sum f F1 + sum f F0A, sum f F2 + sum f F0A)\<close>
+ by (metis Diff_disjoint F0A_def \<open>finite F0A\<close> inf.absorb_iff1 inf_assoc inf_bot_right sum.union_disjoint)
+ then have *: \<open>\<forall>F1 F2. F1\<supseteq>F0B \<and> F2\<supseteq>F0B \<and> finite F1 \<and> finite F2 \<and> F1\<subseteq>B \<and> F2\<subseteq>B \<longrightarrow>
+ E' (sum f F1, sum f F2)\<close>
+ using DE[where c=\<open>- sum f F0A\<close>]
+ apply auto by (metis add.commute add_diff_cancel_left')
+ show \<open>eventually E (?filter_fB \<times>\<^sub>F ?filter_fB)\<close>
+ apply (subst eventually_prod_filter)
+ apply (rule exI[of _ \<open>\<lambda>x. E' (x, sum f F0B)\<close>])
+ apply (rule exI[of _ \<open>\<lambda>x. E' (sum f F0B, x)\<close>])
+ apply (auto simp: eventually_filtermap)
+ using * apply (metis (no_types, lifting) F0B_def Int_lower2 \<open>finite F0\<close> eventually_finite_subsets_at_top finite_Int order_refl)
+ using * apply (metis (no_types, lifting) F0B_def Int_lower2 \<open>finite F0\<close> eventually_finite_subsets_at_top finite_Int order_refl)
+ using E'E'E by auto
+ qed
+
+ then obtain x where \<open>filtermap (sum f) (finite_subsets_at_top B) \<le> nhds x\<close>
+ apply atomize_elim
+ apply (rule complete_uniform[where S=UNIV, THEN iffD1, rule_format, simplified])
+ using assms by (auto simp add: 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} for Banach spaces with less 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>
+ apply (rule summable_on_subset)
+ using assms apply auto
+ by (metis Cauchy_convergent UNIV_I complete_def convergent_def)
+
+lemma has_sum_empty[simp]: \<open>has_sum f {} 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 \<Rightarrow> 'b::topological_comm_monoid_add"
+ assumes finite: \<open>finite A\<close>
+ assumes conv: \<open>\<And>a. a \<in> A \<Longrightarrow> has_sum f (B a) (s 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>has_sum f (\<Union>a\<in>A. B a) (sum s A)\<close>
+ using assms
+proof (insert finite conv disj, induction)
+ case empty
+ then show ?case
+ by simp
+next
+ case (insert x A)
+ have \<open>has_sum f (B x) (s x)\<close>
+ by (simp add: insert.prems)
+ moreover have IH: \<open>has_sum f (\<Union>a\<in>A. B a) (sum s A)\<close>
+ using insert by simp
+ ultimately have \<open>has_sum f (B x \<union> (\<Union>a\<in>A. B a)) (s x + sum s A)\<close>
+ apply (rule has_sum_Un_disjoint)
+ using insert by auto
+ then show ?case
+ using insert.hyps by auto
+qed
+
+
+lemma summable_on_finite_union_disjoint:
+ fixes f :: "'a \<Rightarrow> '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 finite conv disj apply induction by (auto intro!: summable_on_Un_disjoint)
+
+lemma sum_infsum:
+ fixes f :: "'a \<Rightarrow> '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>
+ using sum_has_sum[of A f B \<open>\<lambda>a. infsum f (B a)\<close>]
+ using assms apply auto
+ by (metis finite_subsets_at_top_neq_bot infsum_def summable_on_def has_sum_def tendsto_Lim)
+
+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 o 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>has_sum g S x\<close>
+ shows \<open>has_sum (f o g) S (f x)\<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 o sum g) \<longlongrightarrow> f x) (finite_subsets_at_top S)\<close>
+ apply (rule tendsto_compose_at)
+ using assms by auto
+ then have \<open>(sum (f o g) \<longlongrightarrow> f x) (finite_subsets_at_top S)\<close>
+ apply (rule tendsto_cong[THEN iffD1, rotated])
+ using f_sum by fastforce
+ then show \<open>has_sum (f o g) S (f x)\<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 o 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. has_sum g S x \<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 o 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 o 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 o g) S = f (infsum g S)\<close>
+ by (smt (verit) assms(2) assms(3) continuous_within f_sum finite_subsets_at_top_neq_bot summable_on_comm_additive_general has_sum_comm_additive_general has_sum_def has_sum_infsum tendsto_Lim)
+
+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>has_sum g S x\<close>
+ shows \<open>has_sum (f o g) S (f x)\<close>
+ by (smt (verit, best) additive.sum assms(1) assms(2) comp_eq_dest_lhs continuous_within finite_subsets_at_top_neq_bot infsum summable_on_def has_sum_comm_additive_general has_sum_def has_sum_infsum sum.cong tendsto_Lim)
+
+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 o g) summable_on S\<close>
+ by (meson assms(1) assms(2) assms(3) 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 o g) S = f (infsum g S)\<close>
+ by (rule infsum_comm_additive_general; auto simp: assms additive.sum)
+
+
+lemma pos_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>has_sum f A (SUP F\<in>{F. finite F \<and> F\<subseteq>A}. sum f F)\<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)
+ show \<open>\<forall>\<^sub>F x in finite_subsets_at_top A. a < sum f x\<close>
+ unfolding eventually_finite_subsets_at_top
+ apply (rule exI[of _ F])
+ using \<open>a < sum f F\<close> and \<open>finite F\<close> and \<open>F \<subseteq> A\<close>
+ apply auto
+ by (smt (verit, best) Diff_iff assms(1) less_le_trans subset_iff sum_mono2)
+ next
+ fix a assume \<open>(SUP F\<in>{F. finite F \<and> F\<subseteq>A}. sum f F) < a\<close>
+ then have \<open>sum f F < a\<close> if \<open>F\<subseteq>A\<close> and \<open>finite F\<close> for F
+ by (smt (verit, best) Collect_cong antisym_conv assms(2) cSUP_upper dual_order.trans le_less_linear less_le mem_Collect_eq that(1) that(2))
+ then show \<open>\<forall>\<^sub>F x in finite_subsets_at_top A. sum f x < a\<close>
+ by (rule eventually_finite_subsets_at_top_weakI)
+ qed
+ then show ?thesis
+ using has_sum_def by blast
+qed
+
+lemma pos_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(1) assms(2) summable_on_def pos_has_sum by blast
+
+
+lemma pos_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 pos_has_sum)
+
+lemma pos_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>has_sum f A (SUP F\<in>{F. finite F \<and> F\<subseteq>A}. sum f F)\<close>
+ using assms pos_has_sum by blast
+
+lemma pos_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 pos_summable_on by blast
+
+lemma pos_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 pos_infsum by blast
+
+lemma has_sum_nonneg:
+ fixes f :: "'a \<Rightarrow> 'b::{ordered_comm_monoid_add,linorder_topology}"
+ assumes "has_sum f M a"
+ and "\<And>x. x \<in> M \<Longrightarrow> 0 \<le> f x"
+ shows "a \<ge> 0"
+ by (metis (no_types, lifting) DiffD1 assms(1) assms(2) empty_iff has_sum_0 has_sum_mono_neutral order_refl)
+
+lemma infsum_nonneg:
+ fixes f :: "'a \<Rightarrow> 'b::{ordered_comm_monoid_add,linorder_topology}"
+ assumes "f summable_on M"
+ and "\<And>x. x \<in> M \<Longrightarrow> 0 \<le> f x"
+ shows "infsum f M \<ge> 0" (is "?lhs \<ge> _")
+ by (metis assms infsum_0_simp summable_on_0_simp infsum_mono)
+
+lemma has_sum_reindex:
+ assumes \<open>inj_on h A\<close>
+ shows \<open>has_sum g (h ` A) x \<longleftrightarrow> has_sum (g \<circ> h) A x\<close>
+proof -
+ have \<open>has_sum g (h ` A) x \<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>
+ apply (subst filtermap_image_finite_subsets_at_top[symmetric])
+ using assms by (auto simp: filterlim_def filtermap_filtermap)
+ also have \<open>\<dots> \<longleftrightarrow> (sum (g \<circ> h) \<longlongrightarrow> x) (finite_subsets_at_top A)\<close>
+ apply (rule tendsto_cong)
+ apply (rule eventually_finite_subsets_at_top_weakI)
+ apply (rule sum.reindex)
+ using assms subset_inj_on by blast
+ also have \<open>\<dots> \<longleftrightarrow> has_sum (g \<circ> h) A x\<close>
+ by (simp add: has_sum_def)
+ finally show ?thesis
+ by -
+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 (no_types, opaque_lifting) assms finite_subsets_at_top_neq_bot infsum_def summable_on_reindex has_sum_def has_sum_infsum has_sum_reindex tendsto_Lim)
+
+
+lemma sum_uniformity:
+ assumes plus_cont: \<open>uniformly_continuous_on UNIV (\<lambda>(x::'b::{uniform_space,comm_monoid_add},y). x+y)\<close>
+ assumes \<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 \<open>eventually E uniformity\<close>, 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 \<Rightarrow> '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: "has_sum f (Sigma A B) a"
+ assumes summableB: \<open>\<And>x. x\<in>A \<Longrightarrow> has_sum (\<lambda>y. f (x, y)) (B x) (b x)\<close>
+ shows "has_sum b A a"
+proof -
+ define F FB FA where \<open>F = finite_subsets_at_top (Sigma A B)\<close> and \<open>FB x = finite_subsets_at_top (B x)\<close>
+ and \<open>FA = finite_subsets_at_top A\<close> for x
+
+ from summableB
+ have sum_b: \<open>(sum (\<lambda>y. f (x, y)) \<longlongrightarrow> b x) (FB x)\<close> if \<open>x \<in> A\<close> for x
+ using FB_def[abs_def] has_sum_def that by auto
+ from summableAB
+ have sum_S: \<open>(sum f \<longlongrightarrow> a) F\<close>
+ using F_def has_sum_def by blast
+
+ have finite_proj: \<open>finite {b| b. (a,b) \<in> H}\<close> if \<open>finite H\<close> for H :: \<open>('a\<times>'b) set\<close> and a
+ apply (subst asm_rl[of \<open>{b| b. (a,b) \<in> H} = snd ` {ab. ab \<in> H \<and> fst ab = a}\<close>])
+ by (auto simp: image_iff that)
+
+ have \<open>(sum b \<longlongrightarrow> a) FA\<close>
+ proof (rule tendsto_iff_uniformity[THEN iffD2, rule_format])
+ fix E :: \<open>('c \<times> 'c) \<Rightarrow> bool\<close>
+ assume \<open>eventually E uniformity\<close>
+ then obtain D where D_uni: \<open>eventually D uniformity\<close> and DDE': \<open>\<And>x y z. D (x, y) \<Longrightarrow> D (y, z) \<Longrightarrow> E (x, z)\<close>
+ by (metis (no_types, lifting) \<open>eventually E uniformity\<close> uniformity_transE)
+ from sum_S obtain G where \<open>finite G\<close> and \<open>G \<subseteq> Sigma A B\<close>
+ and G_sum: \<open>G \<subseteq> H \<Longrightarrow> H \<subseteq> Sigma A B \<Longrightarrow> finite H \<Longrightarrow> D (sum f H, a)\<close> for H
+ unfolding tendsto_iff_uniformity
+ by (metis (mono_tags, lifting) D_uni F_def eventually_finite_subsets_at_top)
+ have \<open>finite (fst ` G)\<close> and \<open>fst ` G \<subseteq> A\<close>
+ using \<open>finite G\<close> \<open>G \<subseteq> Sigma A B\<close> by auto
+ thm uniformity_prod_def
+ define Ga where \<open>Ga a = {b. (a,b) \<in> G}\<close> for a
+ have Ga_fin: \<open>finite (Ga a)\<close> and Ga_B: \<open>Ga a \<subseteq> B a\<close> for a
+ using \<open>finite G\<close> \<open>G \<subseteq> Sigma A B\<close> finite_proj by (auto simp: Ga_def finite_proj)
+
+ have \<open>E (sum b M, a)\<close> if \<open>M \<supseteq> fst ` G\<close> and \<open>finite M\<close> and \<open>M \<subseteq> A\<close> for M
+ proof -
+ define FMB where \<open>FMB = finite_subsets_at_top (Sigma M B)\<close>
+ have \<open>eventually (\<lambda>H. D (\<Sum>a\<in>M. b a, \<Sum>(a,b)\<in>H. f (a,b))) FMB\<close>
+ proof -
+ obtain D' where D'_uni: \<open>eventually D' uniformity\<close>
+ and \<open>card M' \<le> card M \<and> (\<forall>m\<in>M'. D' (g m, g' m)) \<Longrightarrow> D (sum g M', sum g' M')\<close>
+ for M' :: \<open>'a set\<close> and g g'
+ apply (rule sum_uniformity[OF plus_cont \<open>eventually D uniformity\<close>, where n=\<open>card M\<close>])
+ by auto
+ then have D'_sum_D: \<open>(\<forall>m\<in>M. D' (g m, g' m)) \<Longrightarrow> D (sum g M, sum g' M)\<close> for g g'
+ by auto
+
+ obtain Ha where \<open>Ha a \<supseteq> Ga a\<close> and Ha_fin: \<open>finite (Ha a)\<close> and Ha_B: \<open>Ha a \<subseteq> B a\<close>
+ and D'_sum_Ha: \<open>Ha a \<subseteq> L \<Longrightarrow> L \<subseteq> B a \<Longrightarrow> finite L \<Longrightarrow> D' (b a, sum (\<lambda>b. f (a,b)) L)\<close> if \<open>a \<in> A\<close> for a L
+ proof -
+ from sum_b[unfolded tendsto_iff_uniformity, rule_format, OF _ D'_uni[THEN uniformity_sym]]
+ obtain Ha0 where \<open>finite (Ha0 a)\<close> and \<open>Ha0 a \<subseteq> B a\<close>
+ and \<open>Ha0 a \<subseteq> L \<Longrightarrow> L \<subseteq> B a \<Longrightarrow> finite L \<Longrightarrow> D' (b a, sum (\<lambda>b. f (a,b)) L)\<close> if \<open>a \<in> A\<close> for a L
+ unfolding FB_def eventually_finite_subsets_at_top apply auto by metis
+ moreover define Ha where \<open>Ha a = Ha0 a \<union> Ga a\<close> for a
+ ultimately show ?thesis
+ using that[where Ha=Ha]
+ using Ga_fin Ga_B by auto
+ qed
+
+ have \<open>D (\<Sum>a\<in>M. b a, \<Sum>(a,b)\<in>H. f (a,b))\<close> if \<open>finite H\<close> and \<open>H \<subseteq> Sigma M B\<close> and \<open>H \<supseteq> Sigma M Ha\<close> for H
+ proof -
+ define Ha' where \<open>Ha' a = {b| b. (a,b) \<in> H}\<close> for a
+ have [simp]: \<open>finite (Ha' a)\<close> and [simp]: \<open>Ha' a \<supseteq> Ha a\<close> and [simp]: \<open>Ha' a \<subseteq> B a\<close> if \<open>a \<in> M\<close> for a
+ unfolding Ha'_def using \<open>finite H\<close> \<open>H \<subseteq> Sigma M B\<close> \<open>Sigma M Ha \<subseteq> H\<close> that finite_proj by auto
+ have \<open>Sigma M Ha' = H\<close>
+ using that by (auto simp: Ha'_def)
+ then have *: \<open>(\<Sum>(a,b)\<in>H. f (a,b)) = (\<Sum>a\<in>M. \<Sum>b\<in>Ha' a. f (a,b))\<close>
+ apply (subst sum.Sigma)
+ using \<open>finite M\<close> by auto
+ have \<open>D' (b a, sum (\<lambda>b. f (a,b)) (Ha' a))\<close> if \<open>a \<in> M\<close> for a
+ apply (rule D'_sum_Ha)
+ using that \<open>M \<subseteq> A\<close> by auto
+ then have \<open>D (\<Sum>a\<in>M. b a, \<Sum>a\<in>M. sum (\<lambda>b. f (a,b)) (Ha' a))\<close>
+ by (rule_tac D'_sum_D, auto)
+ with * show ?thesis
+ by auto
+ qed
+ moreover have \<open>Sigma M Ha \<subseteq> Sigma M B\<close>
+ using Ha_B \<open>M \<subseteq> A\<close> by auto
+ ultimately show ?thesis
+ apply (simp add: FMB_def eventually_finite_subsets_at_top)
+ by (metis Ha_fin finite_SigmaI subsetD that(2) that(3))
+ qed
+ moreover have \<open>eventually (\<lambda>H. D (\<Sum>(a,b)\<in>H. f (a,b), a)) FMB\<close>
+ unfolding FMB_def eventually_finite_subsets_at_top
+ apply (rule exI[of _ G])
+ using \<open>G \<subseteq> Sigma A B\<close> \<open>finite G\<close> that G_sum apply auto
+ by (smt (z3) Sigma_Un_distrib1 dual_order.trans subset_Un_eq)
+ ultimately have \<open>\<forall>\<^sub>F x in FMB. E (sum b M, a)\<close>
+ by (smt (verit, best) DDE' eventually_elim2)
+ then show \<open>E (sum b M, a)\<close>
+ apply (rule eventually_const[THEN iffD1, rotated])
+ using FMB_def by force
+ qed
+ then show \<open>\<forall>\<^sub>F x in FA. E (sum b x, a)\<close>
+ using \<open>finite (fst ` G)\<close> and \<open>fst ` G \<subseteq> A\<close>
+ by (auto intro!: exI[of _ \<open>fst ` G\<close>] simp add: FA_def eventually_finite_subsets_at_top)
+ qed
+ then show ?thesis
+ by (simp add: FA_def has_sum_def)
+qed
+
+lemma summable_on_Sigma:
+ fixes A :: "'a set" and B :: "'a \<Rightarrow> 'b set"
+ and f :: \<open>'a \<Rightarrow> 'b \<Rightarrow> 'c::{comm_monoid_add, t2_space, uniform_space}\<close>
+ assumes plus_cont: \<open>uniformly_continuous_on UNIV (\<lambda>(x::'c,y). x+y)\<close>
+ assumes summableAB: "(\<lambda>(x,y). f x y) summable_on (Sigma A B)"
+ assumes summableB: \<open>\<And>x. x\<in>A \<Longrightarrow> (f x) summable_on (B x)\<close>
+ shows \<open>(\<lambda>x. infsum (f x) (B x)) summable_on A\<close>
+proof -
+ from summableAB obtain a where a: \<open>has_sum (\<lambda>(x,y). f x y) (Sigma A B) a\<close>
+ using has_sum_infsum by blast
+ from summableB have b: \<open>\<And>x. x\<in>A \<Longrightarrow> has_sum (f x) (B x) (infsum (f x) (B x))\<close>
+ by (auto intro!: has_sum_infsum)
+ show ?thesis
+ using plus_cont a b
+ by (auto intro: has_sum_Sigma[where f=\<open>\<lambda>(x,y). f x y\<close>, simplified] simp: summable_on_def)
+qed
+
+lemma infsum_Sigma:
+ fixes A :: "'a set" and B :: "'a \<Rightarrow> 'b set"
+ and f :: \<open>'a \<times> 'b \<Rightarrow> 'c::{comm_monoid_add, t2_space, uniform_space}\<close>
+ assumes plus_cont: \<open>uniformly_continuous_on UNIV (\<lambda>(x::'c,y). x+y)\<close>
+ assumes summableAB: "f summable_on (Sigma A B)"
+ assumes summableB: \<open>\<And>x. x\<in>A \<Longrightarrow> (\<lambda>y. f (x, y)) summable_on (B x)\<close>
+ shows "infsum f (Sigma A B) = infsum (\<lambda>x. infsum (\<lambda>y. f (x, y)) (B x)) A"
+proof -
+ from summableAB have a: \<open>has_sum f (Sigma A B) (infsum f (Sigma A B))\<close>
+ using has_sum_infsum by blast
+ from summableB have b: \<open>\<And>x. x\<in>A \<Longrightarrow> has_sum (\<lambda>y. f (x, y)) (B x) (infsum (\<lambda>y. f (x, y)) (B x))\<close>
+ by (auto intro!: has_sum_infsum)
+ show ?thesis
+ using plus_cont a b by (auto intro: infsumI[symmetric] has_sum_Sigma simp: summable_on_def)
+qed
+
+lemma infsum_Sigma':
+ fixes A :: "'a set" and B :: "'a \<Rightarrow> 'b set"
+ and f :: \<open>'a \<Rightarrow> 'b \<Rightarrow> 'c::{comm_monoid_add, t2_space, uniform_space}\<close>
+ assumes plus_cont: \<open>uniformly_continuous_on UNIV (\<lambda>(x::'c,y). x+y)\<close>
+ assumes summableAB: "(\<lambda>(x,y). f x y) summable_on (Sigma A B)"
+ assumes summableB: \<open>\<And>x. x\<in>A \<Longrightarrow> (f x) summable_on (B x)\<close>
+ shows \<open>infsum (\<lambda>x. infsum (f x) (B x)) A = infsum (\<lambda>(x,y). f x y) (Sigma A B)\<close>
+ using infsum_Sigma[of \<open>\<lambda>(x,y). f x y\<close> A B]
+ using assms by auto
+
+text \<open>A special case of @{thm [source] infsum_Sigma} etc. for Banach spaces. It has less premises.\<close>
+lemma
+ fixes A :: "'a set" and B :: "'a \<Rightarrow> 'b set"
+ and f :: \<open>'a \<Rightarrow> 'b \<Rightarrow> 'c::banach\<close>
+ assumes [simp]: "(\<lambda>(x,y). f x y) summable_on (Sigma A B)"
+ shows infsum_Sigma'_banach: \<open>infsum (\<lambda>x. infsum (f x) (B x)) A = infsum (\<lambda>(x,y). f x y) (Sigma A B)\<close> (is ?thesis1)
+ and summable_on_Sigma_banach: \<open>(\<lambda>x. infsum (f x) (B x)) summable_on A\<close> (is ?thesis2)
+proof -
+ have [simp]: \<open>(f x) summable_on (B x)\<close> if \<open>x \<in> A\<close> for x
+ proof -
+ from assms
+ have \<open>(\<lambda>(x,y). f x y) summable_on (Pair x ` B x)\<close>
+ by (meson image_subset_iff summable_on_subset_banach mem_Sigma_iff that)
+ then have \<open>((\<lambda>(x,y). f x y) o Pair x) summable_on (B x)\<close>
+ apply (rule_tac summable_on_reindex[THEN iffD1])
+ by (simp add: inj_on_def)
+ then show ?thesis
+ by (auto simp: o_def)
+ qed
+ show ?thesis1
+ apply (rule infsum_Sigma')
+ by auto
+ show ?thesis2
+ apply (rule summable_on_Sigma)
+ by auto
+qed
+
+lemma infsum_Sigma_banach:
+ fixes A :: "'a set" and B :: "'a \<Rightarrow> 'b set"
+ and f :: \<open>'a \<times> 'b \<Rightarrow> 'c::banach\<close>
+ assumes [simp]: "f summable_on (Sigma A B)"
+ shows \<open>infsum (\<lambda>x. infsum (\<lambda>y. f (x,y)) (B x)) A = infsum f (Sigma A B)\<close>
+ by (smt (verit, best) SigmaE assms infsum_Sigma'_banach infsum_cong summable_on_cong old.prod.case)
+
+lemma infsum_swap:
+ fixes A :: "'a set" and B :: "'b set"
+ fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::{comm_monoid_add,t2_space,uniform_space}"
+ assumes plus_cont: \<open>uniformly_continuous_on UNIV (\<lambda>(x::'c,y). x+y)\<close>
+ assumes \<open>(\<lambda>(x, y). f x y) summable_on (A \<times> B)\<close>
+ assumes \<open>\<And>a. a\<in>A \<Longrightarrow> (f a) summable_on B\<close>
+ assumes \<open>\<And>b. b\<in>B \<Longrightarrow> (\<lambda>a. f a b) summable_on A\<close>
+ shows \<open>infsum (\<lambda>x. infsum (\<lambda>y. f x y) B) A = infsum (\<lambda>y. infsum (\<lambda>x. f x y) A) B\<close>
+proof -
+ have [simp]: \<open>(\<lambda>(x, y). f y x) summable_on (B \<times> A)\<close>
+ apply (subst product_swap[symmetric])
+ apply (subst summable_on_reindex)
+ using assms by (auto simp: o_def)
+ have \<open>infsum (\<lambda>x. infsum (\<lambda>y. f x y) B) A = infsum (\<lambda>(x,y). f x y) (A \<times> B)\<close>
+ apply (subst infsum_Sigma)
+ using assms by auto
+ also have \<open>\<dots> = infsum (\<lambda>(x,y). f y x) (B \<times> A)\<close>
+ apply (subst product_swap[symmetric])
+ apply (subst infsum_reindex)
+ using assms by (auto simp: o_def)
+ also have \<open>\<dots> = infsum (\<lambda>y. infsum (\<lambda>x. f x y) A) B\<close>
+ apply (subst infsum_Sigma)
+ using assms by auto
+ finally show ?thesis
+ by -
+qed
+
+lemma infsum_swap_banach:
+ fixes A :: "'a set" and B :: "'b set"
+ fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::banach"
+ assumes \<open>(\<lambda>(x, y). f x y) summable_on (A \<times> B)\<close>
+ shows "infsum (\<lambda>x. infsum (\<lambda>y. f x y) B) A = infsum (\<lambda>y. infsum (\<lambda>x. f x y) A) B"
+proof -
+ have [simp]: \<open>(\<lambda>(x, y). f y x) summable_on (B \<times> A)\<close>
+ apply (subst product_swap[symmetric])
+ apply (subst summable_on_reindex)
+ using assms by (auto simp: o_def)
+ have \<open>infsum (\<lambda>x. infsum (\<lambda>y. f x y) B) A = infsum (\<lambda>(x,y). f x y) (A \<times> B)\<close>
+ apply (subst infsum_Sigma'_banach)
+ using assms by auto
+ also have \<open>\<dots> = infsum (\<lambda>(x,y). f y x) (B \<times> A)\<close>
+ apply (subst product_swap[symmetric])
+ apply (subst infsum_reindex)
+ using assms by (auto simp: o_def)
+ also have \<open>\<dots> = infsum (\<lambda>y. infsum (\<lambda>x. f x y) A) B\<close>
+ apply (subst infsum_Sigma'_banach)
+ using assms by auto
+ finally show ?thesis
+ by -
+qed
+
+lemma infsum_0D:
+ fixes f :: "'a \<Rightarrow> 'b::{topological_ab_group_add,ordered_ab_group_add,linorder_topology}"
+ assumes "infsum f A \<le> 0"
+ and abs_sum: "f summable_on A"
+ and nneg: "\<And>x. x \<in> A \<Longrightarrow> f x \<ge> 0"
+ and "x \<in> A"
+ shows "f x = 0"
+proof (rule ccontr)
+ assume \<open>f x \<noteq> 0\<close>
+ have ex: \<open>f summable_on (A-{x})\<close>
+ apply (rule summable_on_cofin_subset)
+ using assms by auto
+ then have pos: \<open>infsum f (A - {x}) \<ge> 0\<close>
+ apply (rule infsum_nonneg)
+ using nneg by auto
+
+ have [trans]: \<open>x \<ge> y \<Longrightarrow> y > z \<Longrightarrow> x > z\<close> for x y z :: 'b by auto
+
+ have \<open>infsum f A = infsum f (A-{x}) + infsum f {x}\<close>
+ apply (subst infsum_Un_disjoint[symmetric])
+ using assms ex apply auto by (metis insert_absorb)
+ also have \<open>\<dots> \<ge> infsum f {x}\<close> (is \<open>_ \<ge> \<dots>\<close>)
+ using pos apply (rule add_increasing) by simp
+ also have \<open>\<dots> = f x\<close> (is \<open>_ = \<dots>\<close>)
+ apply (subst infsum_finite) by auto
+ also have \<open>\<dots> > 0\<close>
+ using \<open>f x \<noteq> 0\<close> assms(4) nneg by fastforce
+ finally show False
+ using assms by auto
+qed
+
+lemma has_sum_0D:
+ fixes f :: "'a \<Rightarrow> 'b::{topological_ab_group_add,ordered_ab_group_add,linorder_topology}"
+ assumes "has_sum f A a" \<open>a \<le> 0\<close>
+ and nneg: "\<And>x. x \<in> A \<Longrightarrow> f x \<ge> 0"
+ and "x \<in> A"
+ shows "f x = 0"
+ by (metis assms(1) assms(2) assms(4) infsumI infsum_0D summable_on_def nneg)
+
+lemma has_sum_cmult_left:
+ fixes f :: "'a \<Rightarrow> 'b :: {topological_semigroup_mult, semiring_0}"
+ assumes \<open>has_sum f A a\<close>
+ shows "has_sum (\<lambda>x. f x * c) A (a * c)"
+proof -
+ from assms have \<open>(sum f \<longlongrightarrow> a) (finite_subsets_at_top A)\<close>
+ using has_sum_def by blast
+ then have \<open>((\<lambda>F. sum f F * c) \<longlongrightarrow> a * c) (finite_subsets_at_top A)\<close>
+ by (simp add: tendsto_mult_right)
+ then have \<open>(sum (\<lambda>x. f x * c) \<longlongrightarrow> a * c) (finite_subsets_at_top A)\<close>
+ apply (rule tendsto_cong[THEN iffD1, rotated])
+ apply (rule eventually_finite_subsets_at_top_weakI)
+ using sum_distrib_right by blast
+ then show ?thesis
+ using infsumI has_sum_def by blast
+qed
+
+lemma infsum_cmult_left:
+ fixes f :: "'a \<Rightarrow> 'b :: {t2_space, topological_semigroup_mult, semiring_0}"
+ assumes \<open>c \<noteq> 0 \<Longrightarrow> f summable_on A\<close>
+ shows "infsum (\<lambda>x. f x * c) A = infsum f A * c"
+proof (cases \<open>c=0\<close>)
+ case True
+ then show ?thesis by auto
+next
+ case False
+ then have \<open>has_sum f A (infsum f A)\<close>
+ by (simp add: assms)
+ then show ?thesis
+ by (auto intro!: infsumI has_sum_cmult_left)
+qed
+
+lemma summable_on_cmult_left:
+ fixes f :: "'a \<Rightarrow> 'b :: {t2_space, topological_semigroup_mult, semiring_0}"
+ assumes \<open>f summable_on A\<close>
+ shows "(\<lambda>x. f x * c) summable_on A"
+ using assms summable_on_def has_sum_cmult_left by blast
+
+lemma has_sum_cmult_right:
+ fixes f :: "'a \<Rightarrow> 'b :: {topological_semigroup_mult, semiring_0}"
+ assumes \<open>has_sum f A a\<close>
+ shows "has_sum (\<lambda>x. c * f x) A (c * a)"
+proof -
+ from assms have \<open>(sum f \<longlongrightarrow> a) (finite_subsets_at_top A)\<close>
+ using has_sum_def by blast
+ then have \<open>((\<lambda>F. c * sum f F) \<longlongrightarrow> c * a) (finite_subsets_at_top A)\<close>
+ by (simp add: tendsto_mult_left)
+ then have \<open>(sum (\<lambda>x. c * f x) \<longlongrightarrow> c * a) (finite_subsets_at_top A)\<close>
+ apply (rule tendsto_cong[THEN iffD1, rotated])
+ apply (rule eventually_finite_subsets_at_top_weakI)
+ using sum_distrib_left by blast
+ then show ?thesis
+ using infsumI has_sum_def by blast
+qed
+
+lemma infsum_cmult_right:
+ fixes f :: "'a \<Rightarrow> 'b :: {t2_space, topological_semigroup_mult, semiring_0}"
+ assumes \<open>c \<noteq> 0 \<Longrightarrow> f summable_on A\<close>
+ shows \<open>infsum (\<lambda>x. c * f x) A = c * infsum f A\<close>
+proof (cases \<open>c=0\<close>)
+ case True
+ then show ?thesis by auto
+next
+ case False
+ then have \<open>has_sum f A (infsum f A)\<close>
+ by (simp add: assms)
+ then show ?thesis
+ by (auto intro!: infsumI has_sum_cmult_right)
+qed
+
+lemma summable_on_cmult_right:
+ fixes f :: "'a \<Rightarrow> 'b :: {t2_space, topological_semigroup_mult, semiring_0}"
+ assumes \<open>f summable_on A\<close>
+ shows "(\<lambda>x. c * f x) summable_on A"
+ using assms summable_on_def has_sum_cmult_right by blast
+
+lemma summable_on_cmult_left':
+ fixes f :: "'a \<Rightarrow> 'b :: {t2_space, topological_semigroup_mult, division_ring}"
+ assumes \<open>c \<noteq> 0\<close>
+ shows "(\<lambda>x. f x * c) summable_on A \<longleftrightarrow> f summable_on A"
+proof
+ assume \<open>f summable_on A\<close>
+ then show \<open>(\<lambda>x. f x * c) summable_on A\<close>
+ by (rule summable_on_cmult_left)
+next
+ assume \<open>(\<lambda>x. f x * c) summable_on A\<close>
+ then have \<open>(\<lambda>x. f x * c * inverse c) summable_on A\<close>
+ by (rule summable_on_cmult_left)
+ then show \<open>f summable_on A\<close>
+ by (metis (no_types, lifting) assms summable_on_cong mult.assoc mult.right_neutral right_inverse)
+qed
+
+lemma summable_on_cmult_right':
+ fixes f :: "'a \<Rightarrow> 'b :: {t2_space, topological_semigroup_mult, division_ring}"
+ assumes \<open>c \<noteq> 0\<close>
+ shows "(\<lambda>x. c * f x) summable_on A \<longleftrightarrow> f summable_on A"
+proof
+ assume \<open>f summable_on A\<close>
+ then show \<open>(\<lambda>x. c * f x) summable_on A\<close>
+ by (rule summable_on_cmult_right)
+next
+ assume \<open>(\<lambda>x. c * f x) summable_on A\<close>
+ then have \<open>(\<lambda>x. inverse c * (c * f x)) summable_on A\<close>
+ by (rule summable_on_cmult_right)
+ then show \<open>f summable_on A\<close>
+ by (metis (no_types, lifting) assms summable_on_cong left_inverse mult.assoc mult.left_neutral)
+qed
+
+lemma infsum_cmult_left':
+ fixes f :: "'a \<Rightarrow> 'b :: {t2_space, topological_semigroup_mult, division_ring}"
+ shows "infsum (\<lambda>x. f x * c) A = infsum f A * c"
+proof (cases \<open>c \<noteq> 0 \<longrightarrow> f summable_on A\<close>)
+ case True
+ then show ?thesis
+ apply (rule_tac infsum_cmult_left) by auto
+next
+ case False
+ note asm = False
+ then show ?thesis
+ proof (cases \<open>c=0\<close>)
+ case True
+ then show ?thesis by auto
+ next
+ case False
+ with asm have nex: \<open>\<not> f summable_on A\<close>
+ by simp
+ moreover have nex': \<open>\<not> (\<lambda>x. f x * c) summable_on A\<close>
+ using asm False apply (subst summable_on_cmult_left') by auto
+ ultimately show ?thesis
+ unfolding infsum_def by simp
+ qed
+qed
+
+lemma infsum_cmult_right':
+ fixes f :: "'a \<Rightarrow> 'b :: {t2_space,topological_semigroup_mult,division_ring}"
+ shows "infsum (\<lambda>x. c * f x) A = c * infsum f A"
+proof (cases \<open>c \<noteq> 0 \<longrightarrow> f summable_on A\<close>)
+ case True
+ then show ?thesis
+ apply (rule_tac infsum_cmult_right) by auto
+next
+ case False
+ note asm = False
+ then show ?thesis
+ proof (cases \<open>c=0\<close>)
+ case True
+ then show ?thesis by auto
+ next
+ case False
+ with asm have nex: \<open>\<not> f summable_on A\<close>
+ by simp
+ moreover have nex': \<open>\<not> (\<lambda>x. c * f x) summable_on A\<close>
+ using asm False apply (subst summable_on_cmult_right') by auto
+ ultimately show ?thesis
+ unfolding infsum_def by simp
+ qed
+qed
+
+
+lemma has_sum_constant[simp]:
+ assumes \<open>finite F\<close>
+ shows \<open>has_sum (\<lambda>_. c) F (of_nat (card F) * c)\<close>
+ by (metis assms has_sum_finite sum_constant)
+
+lemma infsum_constant[simp]:
+ assumes \<open>finite F\<close>
+ shows \<open>infsum (\<lambda>_. c) F = of_nat (card F) * c\<close>
+ apply (subst infsum_finite[OF assms]) by simp
+
+lemma infsum_diverge_constant:
+ \<comment> \<open>This probably does not really need all of \<^class>\<open>archimedean_field\<close> but Isabelle/HOL
+ has no type class such as, e.g., "archimedean ring".\<close>
+ fixes c :: \<open>'a::{archimedean_field, comm_monoid_add, linorder_topology, topological_semigroup_mult}\<close>
+ assumes \<open>infinite A\<close> and \<open>c \<noteq> 0\<close>
+ shows \<open>\<not> (\<lambda>_. c) summable_on A\<close>
+proof (rule notI)
+ assume \<open>(\<lambda>_. c) summable_on A\<close>
+ then have \<open>(\<lambda>_. inverse c * c) summable_on A\<close>
+ by (rule summable_on_cmult_right)
+ then have [simp]: \<open>(\<lambda>_. 1::'a) summable_on A\<close>
+ using assms by auto
+ have \<open>infsum (\<lambda>_. 1) A \<ge> d\<close> for d :: 'a
+ proof -
+ obtain n :: nat where \<open>of_nat n \<ge> d\<close>
+ by (meson real_arch_simple)
+ from assms
+ obtain F where \<open>F \<subseteq> A\<close> and \<open>finite F\<close> and \<open>card F = n\<close>
+ by (meson infinite_arbitrarily_large)
+ note \<open>d \<le> of_nat n\<close>
+ also have \<open>of_nat n = infsum (\<lambda>_. 1::'a) F\<close>
+ by (simp add: \<open>card F = n\<close> \<open>finite F\<close>)
+ also have \<open>\<dots> \<le> infsum (\<lambda>_. 1::'a) A\<close>
+ apply (rule infsum_mono_neutral)
+ using \<open>finite F\<close> \<open>F \<subseteq> A\<close> by auto
+ finally show ?thesis
+ by -
+ qed
+ then show False
+ by (meson linordered_field_no_ub not_less)
+qed
+
+lemma has_sum_constant_archimedean[simp]:
+ \<comment> \<open>This probably does not really need all of \<^class>\<open>archimedean_field\<close> but Isabelle/HOL
+ has no type class such as, e.g., "archimedean ring".\<close>
+ fixes c :: \<open>'a::{archimedean_field, comm_monoid_add, linorder_topology, topological_semigroup_mult}\<close>
+ shows \<open>infsum (\<lambda>_. c) A = of_nat (card A) * c\<close>
+ apply (cases \<open>finite A\<close>)
+ apply simp
+ apply (cases \<open>c = 0\<close>)
+ apply simp
+ by (simp add: infsum_diverge_constant infsum_not_exists)
+
+lemma has_sum_uminus:
+ fixes f :: \<open>'a \<Rightarrow> 'b::topological_ab_group_add\<close>
+ shows \<open>has_sum (\<lambda>x. - f x) A a \<longleftrightarrow> has_sum f A (- a)\<close>
+ by (auto simp add: sum_negf[abs_def] tendsto_minus_cancel_left has_sum_def)
+
+lemma summable_on_uminus:
+ fixes f :: \<open>'a \<Rightarrow> 'b::topological_ab_group_add\<close>
+ shows\<open>(\<lambda>x. - f x) summable_on A \<longleftrightarrow> f summable_on A\<close>
+ by (metis summable_on_def has_sum_uminus verit_minus_simplify(4))
+
+lemma infsum_uminus:
+ fixes f :: \<open>'a \<Rightarrow> 'b::{topological_ab_group_add, t2_space}\<close>
+ shows \<open>infsum (\<lambda>x. - f x) A = - infsum f A\<close>
+ by (metis (full_types) add.inverse_inverse add.inverse_neutral infsumI infsum_def has_sum_infsum has_sum_uminus)
+
+subsection \<open>Extended reals and nats\<close>
+
+lemma summable_on_ennreal[simp]: \<open>(f::_ \<Rightarrow> ennreal) summable_on S\<close>
+ apply (rule pos_summable_on_complete) by simp
+
+lemma summable_on_enat[simp]: \<open>(f::_ \<Rightarrow> enat) summable_on S\<close>
+ apply (rule pos_summable_on_complete) by simp
+
+lemma has_sum_superconst_infinite_ennreal:
+ fixes f :: \<open>'a \<Rightarrow> ennreal\<close>
+ assumes geqb: \<open>\<And>x. x \<in> S \<Longrightarrow> f x \<ge> b\<close>
+ assumes b: \<open>b > 0\<close>
+ assumes \<open>infinite S\<close>
+ shows "has_sum f S \<infinity>"
+proof -
+ have \<open>(sum f \<longlongrightarrow> \<infinity>) (finite_subsets_at_top S)\<close>
+ proof (rule order_tendstoI[rotated], simp)
+ fix y :: ennreal assume \<open>y < \<infinity>\<close>
+ then have \<open>y / b < \<infinity>\<close>
+ by (metis b ennreal_divide_eq_top_iff gr_implies_not_zero infinity_ennreal_def top.not_eq_extremum)
+ then obtain F where \<open>finite F\<close> and \<open>F \<subseteq> S\<close> and cardF: \<open>card F > y / b\<close>
+ using \<open>infinite S\<close>
+ by (metis ennreal_Ex_less_of_nat infinite_arbitrarily_large infinity_ennreal_def)
+ moreover have \<open>sum f Y > y\<close> if \<open>finite Y\<close> and \<open>F \<subseteq> Y\<close> and \<open>Y \<subseteq> S\<close> for Y
+ proof -
+ have \<open>y < b * card F\<close>
+ by (metis \<open>y < \<infinity>\<close> b cardF divide_less_ennreal ennreal_mult_eq_top_iff gr_implies_not_zero infinity_ennreal_def mult.commute top.not_eq_extremum)
+ also have \<open>\<dots> \<le> b * card Y\<close>
+ by (meson b card_mono less_imp_le mult_left_mono of_nat_le_iff that(1) that(2))
+ also have \<open>\<dots> = sum (\<lambda>_. b) Y\<close>
+ by (simp add: mult.commute)
+ also have \<open>\<dots> \<le> sum f Y\<close>
+ using geqb by (meson subset_eq sum_mono that(3))
+ finally show ?thesis
+ by -
+ qed
+ ultimately show \<open>\<forall>\<^sub>F x in finite_subsets_at_top S. y < sum f x\<close>
+ unfolding eventually_finite_subsets_at_top
+ by auto
+ qed
+ then show ?thesis
+ by (simp add: has_sum_def)
+qed
+
+lemma infsum_superconst_infinite_ennreal:
+ fixes f :: \<open>'a \<Rightarrow> ennreal\<close>
+ assumes \<open>\<And>x. x \<in> S \<Longrightarrow> f x \<ge> b\<close>
+ assumes \<open>b > 0\<close>
+ assumes \<open>infinite S\<close>
+ shows "infsum f S = \<infinity>"
+ using assms infsumI has_sum_superconst_infinite_ennreal by blast
+
+lemma infsum_superconst_infinite_ereal:
+ fixes f :: \<open>'a \<Rightarrow> ereal\<close>
+ assumes geqb: \<open>\<And>x. x \<in> S \<Longrightarrow> f x \<ge> b\<close>
+ assumes b: \<open>b > 0\<close>
+ assumes \<open>infinite S\<close>
+ shows "infsum f S = \<infinity>"
+proof -
+ obtain b' where b': \<open>e2ennreal b' = b\<close> and \<open>b' > 0\<close>
+ using b by blast
+ have *: \<open>infsum (e2ennreal o f) S = \<infinity>\<close>
+ apply (rule infsum_superconst_infinite_ennreal[where b=b'])
+ using assms \<open>b' > 0\<close> b' e2ennreal_mono apply auto
+ by (metis dual_order.strict_iff_order enn2ereal_e2ennreal le_less_linear zero_ennreal_def)
+ have \<open>infsum f S = infsum (enn2ereal o (e2ennreal o f)) S\<close>
+ by (smt (verit, best) b comp_apply dual_order.trans enn2ereal_e2ennreal geqb infsum_cong less_imp_le)
+ also have \<open>\<dots> = enn2ereal \<infinity>\<close>
+ apply (subst infsum_comm_additive_general)
+ using * by (auto simp: continuous_at_enn2ereal)
+ also have \<open>\<dots> = \<infinity>\<close>
+ by simp
+ finally show ?thesis
+ by -
+qed
+
+lemma has_sum_superconst_infinite_ereal:
+ fixes f :: \<open>'a \<Rightarrow> ereal\<close>
+ assumes \<open>\<And>x. x \<in> S \<Longrightarrow> f x \<ge> b\<close>
+ assumes \<open>b > 0\<close>
+ assumes \<open>infinite S\<close>
+ shows "has_sum f S \<infinity>"
+ by (metis Infty_neq_0(1) assms infsum_def has_sum_infsum infsum_superconst_infinite_ereal)
+
+lemma infsum_superconst_infinite_enat:
+ fixes f :: \<open>'a \<Rightarrow> enat\<close>
+ assumes geqb: \<open>\<And>x. x \<in> S \<Longrightarrow> f x \<ge> b\<close>
+ assumes b: \<open>b > 0\<close>
+ assumes \<open>infinite S\<close>
+ shows "infsum f S = \<infinity>"
+proof -
+ have \<open>ennreal_of_enat (infsum f S) = infsum (ennreal_of_enat o f) S\<close>
+ apply (rule infsum_comm_additive_general[symmetric])
+ by auto
+ also have \<open>\<dots> = \<infinity>\<close>
+ by (metis assms(3) b comp_apply ennreal_of_enat_0 ennreal_of_enat_inj ennreal_of_enat_le_iff geqb infsum_superconst_infinite_ennreal not_gr_zero)
+ also have \<open>\<dots> = ennreal_of_enat \<infinity>\<close>
+ by simp
+ finally show ?thesis
+ by (rule ennreal_of_enat_inj[THEN iffD1])
+qed
+
+lemma has_sum_superconst_infinite_enat:
+ fixes f :: \<open>'a \<Rightarrow> enat\<close>
+ assumes \<open>\<And>x. x \<in> S \<Longrightarrow> f x \<ge> b\<close>
+ assumes \<open>b > 0\<close>
+ assumes \<open>infinite S\<close>
+ shows "has_sum f S \<infinity>"
+ by (metis assms i0_lb has_sum_infsum infsum_superconst_infinite_enat pos_summable_on_complete)
+
+text \<open>This lemma helps to relate a real-valued infsum to a supremum over extended nonnegative reals.\<close>
+
+lemma infsum_nonneg_is_SUPREMUM_ennreal:
+ fixes f :: "'a \<Rightarrow> real"
+ assumes summable: "f summable_on A"
+ and fnn: "\<And>x. x\<in>A \<Longrightarrow> f x \<ge> 0"
+ shows "ennreal (infsum f A) = (SUP F\<in>{F. finite F \<and> F \<subseteq> A}. (ennreal (sum f F)))"
+proof -
+ have \<open>ennreal (infsum f A) = infsum (ennreal o f) A\<close>
+ apply (rule infsum_comm_additive_general[symmetric])
+ apply (subst sum_ennreal[symmetric])
+ using assms by auto
+ also have \<open>\<dots> = (SUP F\<in>{F. finite F \<and> F \<subseteq> A}. (ennreal (sum f F)))\<close>
+ apply (subst pos_infsum_complete, simp)
+ apply (rule SUP_cong, blast)
+ apply (subst sum_ennreal[symmetric])
+ using fnn by auto
+ finally show ?thesis
+ by -
+qed
+
+text \<open>This lemma helps to related a real-valued infsum to a supremum over extended reals.\<close>
+
+lemma infsum_nonneg_is_SUPREMUM_ereal:
+ fixes f :: "'a \<Rightarrow> real"
+ assumes summable: "f summable_on A"
+ and fnn: "\<And>x. x\<in>A \<Longrightarrow> f x \<ge> 0"
+ shows "ereal (infsum f A) = (SUP F\<in>{F. finite F \<and> F \<subseteq> A}. (ereal (sum f F)))"
+proof -
+ have \<open>ereal (infsum f A) = infsum (ereal o f) A\<close>
+ apply (rule infsum_comm_additive_general[symmetric])
+ using assms by auto
+ also have \<open>\<dots> = (SUP F\<in>{F. finite F \<and> F \<subseteq> A}. (ereal (sum f F)))\<close>
+ apply (subst pos_infsum_complete)
+ by (simp_all add: assms)[2]
+ finally show ?thesis
+ by -
+qed
+
+
+subsection \<open>Real numbers\<close>
+
+text \<open>Most lemmas in the general property section already apply to real numbers.
+ A few ones that are specific to reals are given here.\<close>
+
+lemma infsum_nonneg_is_SUPREMUM_real:
+ fixes f :: "'a \<Rightarrow> real"
+ assumes summable: "f summable_on A"
+ and fnn: "\<And>x. x\<in>A \<Longrightarrow> f x \<ge> 0"
+ shows "infsum f A = (SUP F\<in>{F. finite F \<and> F \<subseteq> A}. (sum f F))"
+proof -
+ have "ereal (infsum f A) = (SUP F\<in>{F. finite F \<and> F \<subseteq> A}. (ereal (sum f F)))"
+ using assms by (rule infsum_nonneg_is_SUPREMUM_ereal)
+ also have "\<dots> = ereal (SUP F\<in>{F. finite F \<and> F \<subseteq> A}. (sum f F))"
+ proof (subst ereal_SUP)
+ show "\<bar>SUP a\<in>{F. finite F \<and> F \<subseteq> A}. ereal (sum f a)\<bar> \<noteq> \<infinity>"
+ using calculation by fastforce
+ show "(SUP F\<in>{F. finite F \<and> F \<subseteq> A}. ereal (sum f F)) = (SUP a\<in>{F. finite F \<and> F \<subseteq> A}. ereal (sum f a))"
+ by simp
+ qed
+ finally show ?thesis by simp
+qed
+
+
+lemma has_sum_nonneg_SUPREMUM_real:
+ fixes f :: "'a \<Rightarrow> real"
+ assumes "f summable_on A" and "\<And>x. x\<in>A \<Longrightarrow> f x \<ge> 0"
+ shows "has_sum f A (SUP F\<in>{F. finite F \<and> F \<subseteq> A}. (sum f F))"
+ by (metis (mono_tags, lifting) assms has_sum_infsum infsum_nonneg_is_SUPREMUM_real)
+
+
+lemma summable_on_iff_abs_summable_on_real:
+ fixes f :: \<open>'a \<Rightarrow> real\<close>
+ shows \<open>f summable_on A \<longleftrightarrow> f abs_summable_on A\<close>
+proof (rule iffI)
+ assume \<open>f summable_on A\<close>
+ define n A\<^sub>p A\<^sub>n
+ where \<open>n x = norm (f x)\<close> and \<open>A\<^sub>p = {x\<in>A. f x \<ge> 0}\<close> and \<open>A\<^sub>n = {x\<in>A. f x < 0}\<close> for x
+ have [simp]: \<open>A\<^sub>p \<union> A\<^sub>n = A\<close> \<open>A\<^sub>p \<inter> A\<^sub>n = {}\<close>
+ by (auto simp: A\<^sub>p_def A\<^sub>n_def)
+ from \<open>f summable_on A\<close> have [simp]: \<open>f summable_on A\<^sub>p\<close> \<open>f summable_on A\<^sub>n\<close>
+ using A\<^sub>p_def A\<^sub>n_def summable_on_subset_banach by fastforce+
+ then have [simp]: \<open>n summable_on A\<^sub>p\<close>
+ apply (subst summable_on_cong[where g=f])
+ by (simp_all add: A\<^sub>p_def n_def)
+ moreover have [simp]: \<open>n summable_on A\<^sub>n\<close>
+ apply (subst summable_on_cong[where g=\<open>\<lambda>x. - f x\<close>])
+ apply (simp add: A\<^sub>n_def n_def[abs_def])
+ by (simp add: summable_on_uminus)
+ ultimately have [simp]: \<open>n summable_on (A\<^sub>p \<union> A\<^sub>n)\<close>
+ apply (rule summable_on_Un_disjoint) by simp
+ then show \<open>n summable_on A\<close>
+ by simp
+next
+ show \<open>f abs_summable_on A \<Longrightarrow> f summable_on A\<close>
+ using abs_summable_summable by blast
+qed
+
+subsection \<open>Complex numbers\<close>
+
+lemma has_sum_cnj_iff[simp]:
+ fixes f :: \<open>'a \<Rightarrow> complex\<close>
+ shows \<open>has_sum (\<lambda>x. cnj (f x)) M (cnj a) \<longleftrightarrow> has_sum f M a\<close>
+ by (simp add: has_sum_def lim_cnj del: cnj_sum add: cnj_sum[symmetric, abs_def, of f])
+
+lemma summable_on_cnj_iff[simp]:
+ "(\<lambda>i. cnj (f i)) summable_on A \<longleftrightarrow> f summable_on A"
+ by (metis complex_cnj_cnj summable_on_def has_sum_cnj_iff)
+
+lemma infsum_cnj[simp]: \<open>infsum (\<lambda>x. cnj (f x)) M = cnj (infsum f M)\<close>
+ by (metis complex_cnj_zero infsumI has_sum_cnj_iff infsum_def summable_on_cnj_iff has_sum_infsum)
+
+lemma infsum_Re:
+ assumes "f summable_on M"
+ shows "infsum (\<lambda>x. Re (f x)) M = Re (infsum f M)"
+ apply (rule infsum_comm_additive[where f=Re, unfolded o_def])
+ using assms by (auto intro!: additive.intro)
+
+lemma has_sum_Re:
+ assumes "has_sum f M a"
+ shows "has_sum (\<lambda>x. Re (f x)) M (Re a)"
+ apply (rule has_sum_comm_additive[where f=Re, unfolded o_def])
+ using assms by (auto intro!: additive.intro tendsto_Re)
+
+lemma summable_on_Re:
+ assumes "f summable_on M"
+ shows "(\<lambda>x. Re (f x)) summable_on M"
+ apply (rule summable_on_comm_additive[where f=Re, unfolded o_def])
+ using assms by (auto intro!: additive.intro)
+
+lemma infsum_Im:
+ assumes "f summable_on M"
+ shows "infsum (\<lambda>x. Im (f x)) M = Im (infsum f M)"
+ apply (rule infsum_comm_additive[where f=Im, unfolded o_def])
+ using assms by (auto intro!: additive.intro)
+
+lemma has_sum_Im:
+ assumes "has_sum f M a"
+ shows "has_sum (\<lambda>x. Im (f x)) M (Im a)"
+ apply (rule has_sum_comm_additive[where f=Im, unfolded o_def])
+ using assms by (auto intro!: additive.intro tendsto_Im)
+
+lemma summable_on_Im:
+ assumes "f summable_on M"
+ shows "(\<lambda>x. Im (f x)) summable_on M"
+ apply (rule summable_on_comm_additive[where f=Im, unfolded o_def])
+ using assms by (auto intro!: additive.intro)
+
+lemma infsum_0D_complex:
+ fixes f :: "'a \<Rightarrow> complex"
+ assumes "infsum f A \<le> 0"
+ and abs_sum: "f summable_on A"
+ and nneg: "\<And>x. x \<in> A \<Longrightarrow> f x \<ge> 0"
+ and "x \<in> A"
+ shows "f x = 0"
+proof -
+ have \<open>Im (f x) = 0\<close>
+ apply (rule infsum_0D[where A=A])
+ using assms
+ by (auto simp add: infsum_Im summable_on_Im less_eq_complex_def)
+ moreover have \<open>Re (f x) = 0\<close>
+ apply (rule infsum_0D[where A=A])
+ using assms by (auto simp add: summable_on_Re infsum_Re less_eq_complex_def)
+ ultimately show ?thesis
+ by (simp add: complex_eqI)
+qed
+
+lemma has_sum_0D_complex:
+ fixes f :: "'a \<Rightarrow> complex"
+ assumes "has_sum f A a" and \<open>a \<le> 0\<close>
+ and "\<And>x. x \<in> A \<Longrightarrow> f x \<ge> 0" and "x \<in> A"
+ shows "f x = 0"
+ by (metis assms infsumI infsum_0D_complex summable_on_def)
+
+text \<open>The lemma @{thm [source] infsum_mono_neutral} above applies to various linear ordered monoids such as the reals but not to the complex numbers.
+ Thus we have a separate corollary for those:\<close>
+
+lemma infsum_mono_neutral_complex:
+ fixes f :: "'a \<Rightarrow> complex"
+ assumes [simp]: "f summable_on A"
+ and [simp]: "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 \<open>infsum f A \<le> infsum g B\<close>
+proof -
+ have \<open>infsum (\<lambda>x. Re (f x)) A \<le> infsum (\<lambda>x. Re (g x)) B\<close>
+ apply (rule infsum_mono_neutral)
+ using assms(3-5) by (auto simp add: summable_on_Re less_eq_complex_def)
+ then have Re: \<open>Re (infsum f A) \<le> Re (infsum g B)\<close>
+ by (metis assms(1-2) infsum_Re)
+ have \<open>infsum (\<lambda>x. Im (f x)) A = infsum (\<lambda>x. Im (g x)) B\<close>
+ apply (rule infsum_cong_neutral)
+ using assms(3-5) by (auto simp add: summable_on_Re less_eq_complex_def)
+ then have Im: \<open>Im (infsum f A) = Im (infsum g B)\<close>
+ by (metis assms(1-2) infsum_Im)
+ from Re Im show ?thesis
+ by (auto simp: less_eq_complex_def)
+qed
+
+lemma infsum_mono_complex:
+ \<comment> \<open>For \<^typ>\<open>real\<close>, @{thm [source] infsum_mono} can be used.
+ But \<^typ>\<open>complex\<close> does not have the right typeclass.\<close>
+ fixes f g :: "'a \<Rightarrow> complex"
+ assumes f_sum: "f summable_on A" and g_sum: "g summable_on A"
+ assumes leq: "\<And>x. x \<in> A \<Longrightarrow> f x \<le> g x"
+ shows "infsum f A \<le> infsum g A"
+ by (metis DiffE IntD1 f_sum g_sum infsum_mono_neutral_complex leq)
+
+
+lemma infsum_nonneg_complex:
+ fixes f :: "'a \<Rightarrow> complex"
+ assumes "f summable_on M"
+ and "\<And>x. x \<in> M \<Longrightarrow> 0 \<le> f x"
+ shows "infsum f M \<ge> 0" (is "?lhs \<ge> _")
+ by (metis assms(1) assms(2) infsum_0_simp summable_on_0_simp infsum_mono_complex)
+
+lemma infsum_cmod:
+ assumes "f summable_on M"
+ and fnn: "\<And>x. x \<in> M \<Longrightarrow> 0 \<le> f x"
+ shows "infsum (\<lambda>x. cmod (f x)) M = cmod (infsum f M)"
+proof -
+ have \<open>complex_of_real (infsum (\<lambda>x. cmod (f x)) M) = infsum (\<lambda>x. complex_of_real (cmod (f x))) M\<close>
+ apply (rule infsum_comm_additive[symmetric, unfolded o_def])
+ apply auto
+ apply (simp add: additive.intro)
+ by (smt (verit, best) assms(1) cmod_eq_Re fnn summable_on_Re summable_on_cong less_eq_complex_def zero_complex.simps(1) zero_complex.simps(2))
+ also have \<open>\<dots> = infsum f M\<close>
+ apply (rule infsum_cong)
+ using fnn
+ using cmod_eq_Re complex_is_Real_iff less_eq_complex_def by force
+ finally show ?thesis
+ by (metis abs_of_nonneg infsum_def le_less_trans norm_ge_zero norm_infsum_bound norm_of_real not_le order_refl)
+qed
+
+
+lemma summable_on_iff_abs_summable_on_complex:
+ fixes f :: \<open>'a \<Rightarrow> complex\<close>
+ shows \<open>f summable_on A \<longleftrightarrow> f abs_summable_on A\<close>
+proof (rule iffI)
+ assume \<open>f summable_on A\<close>
+ define i r ni nr n where \<open>i x = Im (f x)\<close> and \<open>r x = Re (f x)\<close>
+ and \<open>ni x = norm (i x)\<close> and \<open>nr x = norm (r x)\<close> and \<open>n x = norm (f x)\<close> for x
+ from \<open>f summable_on A\<close> have \<open>i summable_on A\<close>
+ by (simp add: i_def[abs_def] summable_on_Im)
+ then have [simp]: \<open>ni summable_on A\<close>
+ using ni_def[abs_def] summable_on_iff_abs_summable_on_real by force
+
+ from \<open>f summable_on A\<close> have \<open>r summable_on A\<close>
+ by (simp add: r_def[abs_def] summable_on_Re)
+ then have [simp]: \<open>nr summable_on A\<close>
+ by (metis nr_def summable_on_cong summable_on_iff_abs_summable_on_real)
+
+ have n_sum: \<open>n x \<le> nr x + ni x\<close> for x
+ by (simp add: n_def nr_def ni_def r_def i_def cmod_le)
+
+ have *: \<open>(\<lambda>x. nr x + ni x) summable_on A\<close>
+ apply (rule summable_on_add) by auto
+ show \<open>n summable_on A\<close>
+ apply (rule pos_summable_on)
+ apply (simp add: n_def)
+ apply (rule bdd_aboveI[where M=\<open>infsum (\<lambda>x. nr x + ni x) A\<close>])
+ using * n_sum by (auto simp flip: infsum_finite simp: ni_def[abs_def] nr_def[abs_def] intro!: infsum_mono_neutral)
+next
+ show \<open>f abs_summable_on A \<Longrightarrow> f summable_on A\<close>
+ using abs_summable_summable by blast
+qed
+
+end
--- a/src/HOL/Analysis/Product_Vector.thy Thu Oct 07 10:34:48 2021 +0200
+++ b/src/HOL/Analysis/Product_Vector.thy Wed Oct 06 14:19:46 2021 +0200
@@ -1,5 +1,6 @@
(* Title: HOL/Analysis/Product_Vector.thy
Author: Brian Huffman
+ Dominique Unruh, University of Tartu
*)
section \<open>Cartesian Products as Vector Spaces\<close>
@@ -122,15 +123,149 @@
instance ..
end
-instantiation\<^marker>\<open>tag unimportant\<close> prod :: (metric_space, metric_space) uniformity_dist
-begin
+instantiation\<^marker>\<open>tag unimportant\<close> prod :: (uniformity, uniformity) uniformity begin
+
+definition [code del]: \<open>(uniformity :: (('a \<times> 'b) \<times> ('a \<times> 'b)) filter) =
+ filtermap (\<lambda>((x1,x2),(y1,y2)). ((x1,y1),(x2,y2))) (uniformity \<times>\<^sub>F uniformity)\<close>
+
+instance..
+end
-definition [code del]:
- "(uniformity :: (('a \<times> 'b) \<times> ('a \<times> 'b)) filter) =
- (INF e\<in>{0 <..}. principal {(x, y). dist x y < e})"
+instantiation\<^marker>\<open>tag unimportant\<close> prod :: (uniform_space, uniform_space) uniform_space begin
+instance
+proof standard
+ fix U :: \<open>('a \<times> 'b) set\<close>
+ show \<open>open U \<longleftrightarrow> (\<forall>x\<in>U. \<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> y \<in> U)\<close>
+ proof (intro iffI ballI)
+ fix x assume \<open>open U\<close> and \<open>x \<in> U\<close>
+ then obtain A B where \<open>open A\<close> \<open>open B\<close> \<open>x \<in> A\<times>B\<close> \<open>A\<times>B \<subseteq> U\<close>
+ by (metis open_prod_elim)
+ define UA where \<open>UA = (\<lambda>(x'::'a,y). x' = fst x \<longrightarrow> y \<in> A)\<close>
+ from \<open>open A\<close> \<open>x \<in> A\<times>B\<close>
+ have \<open>eventually UA uniformity\<close>
+ unfolding open_uniformity UA_def by auto
+ define UB where \<open>UB = (\<lambda>(x'::'b,y). x' = snd x \<longrightarrow> y \<in> B)\<close>
+ from \<open>open A\<close> \<open>open B\<close> \<open>x \<in> A\<times>B\<close>
+ have \<open>eventually UA uniformity\<close> \<open>eventually UB uniformity\<close>
+ unfolding open_uniformity UA_def UB_def by auto
+ then have \<open>\<forall>\<^sub>F ((x'1, y1), (x'2, y2)) in uniformity \<times>\<^sub>F uniformity. (x'1,x'2) = x \<longrightarrow> (y1,y2) \<in> U\<close>
+ apply (auto intro!: exI[of _ UA] exI[of _ UB] simp add: eventually_prod_filter)
+ using \<open>A\<times>B \<subseteq> U\<close> by (auto simp: UA_def UB_def)
+ then show \<open>\<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> y \<in> U\<close>
+ by (simp add: uniformity_prod_def eventually_filtermap case_prod_unfold)
+ next
+ assume asm: \<open>\<forall>x\<in>U. \<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> y \<in> U\<close>
+ show \<open>open U\<close>
+ proof (unfold open_prod_def, intro ballI)
+ fix x assume \<open>x \<in> U\<close>
+ with asm have \<open>\<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> y \<in> U\<close>
+ by auto
+ then have \<open>\<forall>\<^sub>F ((x'1, y1), (x'2, y2)) in uniformity \<times>\<^sub>F uniformity. (x'1,x'2) = x \<longrightarrow> (y1,y2) \<in> U\<close>
+ by (simp add: uniformity_prod_def eventually_filtermap case_prod_unfold)
+ then obtain UA UB where \<open>eventually UA uniformity\<close> and \<open>eventually UB uniformity\<close>
+ and UA_UB_U: \<open>UA (a1, a2) \<Longrightarrow> UB (b1, b2) \<Longrightarrow> (a1, b1) = x \<Longrightarrow> (a2, b2) \<in> U\<close> for a1 a2 b1 b2
+ apply atomize_elim by (simp add: case_prod_beta eventually_prod_filter)
+ have \<open>eventually (\<lambda>a. UA (fst x, a)) (nhds (fst x))\<close>
+ using \<open>eventually UA uniformity\<close> eventually_mono eventually_nhds_uniformity by fastforce
+ then obtain A where \<open>open A\<close> and A_UA: \<open>A \<subseteq> {a. UA (fst x, a)}\<close> and \<open>fst x \<in> A\<close>
+ by (metis (mono_tags, lifting) eventually_nhds mem_Collect_eq subsetI)
+ have \<open>eventually (\<lambda>b. UB (snd x, b)) (nhds (snd x))\<close>
+ using \<open>eventually UB uniformity\<close> eventually_mono eventually_nhds_uniformity by fastforce
+ then obtain B where \<open>open B\<close> and B_UB: \<open>B \<subseteq> {b. UB (snd x, b)}\<close> and \<open>snd x \<in> B\<close>
+ by (metis (mono_tags, lifting) eventually_nhds mem_Collect_eq subsetI)
+ have \<open>x \<in> A \<times> B\<close>
+ by (simp add: \<open>fst x \<in> A\<close> \<open>snd x \<in> B\<close> mem_Times_iff)
+ have \<open>A \<times> B \<subseteq> U\<close>
+ using A_UA B_UB UA_UB_U by fastforce
+ show \<open>\<exists>A B. open A \<and> open B \<and> x \<in> A \<times> B \<and> A \<times> B \<subseteq> U\<close>
+ using \<open>A \<times> B \<subseteq> U\<close> \<open>open A\<close> \<open>open B\<close> \<open>x \<in> A \<times> B\<close> by auto
+ qed
+ qed
+next
+ show \<open>eventually E uniformity \<Longrightarrow> E (x, x)\<close> for E and x :: \<open>'a \<times> 'b\<close>
+ apply (simp add: uniformity_prod_def eventually_filtermap case_prod_unfold eventually_prod_filter)
+ by (metis surj_pair uniformity_refl)
+next
+ show \<open>eventually E uniformity \<Longrightarrow> \<forall>\<^sub>F (x::'a\<times>'b, y) in uniformity. E (y, x)\<close> for E
+ apply (simp only: uniformity_prod_def eventually_filtermap case_prod_unfold eventually_prod_filter)
+ apply (erule exE, erule exE, rename_tac Pf Pg)
+ apply (rule_tac x=\<open>\<lambda>(x,y). Pf (y,x)\<close> in exI)
+ apply (rule_tac x=\<open>\<lambda>(x,y). Pg (y,x)\<close> in exI)
+ by (auto simp add: uniformity_sym)
+next
+ show \<open>\<exists>D. eventually D uniformity \<and> (\<forall>x y z. D (x::'a\<times>'b, y) \<longrightarrow> D (y, z) \<longrightarrow> E (x, z))\<close>
+ if \<open>eventually E uniformity\<close> for E
+ proof -
+ from that
+ obtain EA EB where \<open>eventually EA uniformity\<close> and \<open>eventually EB uniformity\<close>
+ and EA_EB_E: \<open>EA (a1, a2) \<Longrightarrow> EB (b1, b2) \<Longrightarrow> E ((a1, b1), (a2, b2))\<close> for a1 a2 b1 b2
+ by (auto simp add: uniformity_prod_def eventually_filtermap case_prod_unfold eventually_prod_filter)
+ obtain DA where \<open>eventually DA uniformity\<close> and DA_EA: \<open>DA (x,y) \<Longrightarrow> DA (y,z) \<Longrightarrow> EA (x,z)\<close> for x y z
+ using \<open>eventually EA uniformity\<close> uniformity_transE by blast
+ obtain DB where \<open>eventually DB uniformity\<close> and DB_EB: \<open>DB (x,y) \<Longrightarrow> DB (y,z) \<Longrightarrow> EB (x,z)\<close> for x y z
+ using \<open>eventually EB uniformity\<close> uniformity_transE by blast
+ define D where \<open>D = (\<lambda>((a1,b1),(a2,b2)). DA (a1,a2) \<and> DB (b1,b2))\<close>
+ have \<open>eventually D uniformity\<close>
+ using \<open>eventually DA uniformity\<close> \<open>eventually DB uniformity\<close>
+ by (auto simp add: uniformity_prod_def eventually_filtermap case_prod_unfold eventually_prod_filter D_def)
+ moreover have \<open>D ((a1, b1), (a2, b2)) \<Longrightarrow> D ((a2, b2), (a3, b3)) \<Longrightarrow> E ((a1, b1), (a3, b3))\<close> for a1 b1 a2 b2 a3 b3
+ using DA_EA DB_EB D_def EA_EB_E by blast
+ ultimately show ?thesis
+ by auto
+ qed
+qed
+end
+instantiation\<^marker>\<open>tag unimportant\<close> prod :: (metric_space, metric_space) uniformity_dist begin
instance
- by standard (rule uniformity_prod_def)
+proof
+ show \<open>uniformity = (INF e\<in>{0 <..}. principal {(x::'a\<times>'b, y). dist x y < e})\<close>
+ proof (subst filter_eq_iff, intro allI iffI)
+ fix P :: \<open>('a \<times> 'b) \<times> ('a \<times> 'b) \<Rightarrow> bool\<close>
+
+ have 1: \<open>\<exists>e\<in>{0<..}.
+ {(x,y). dist x y < e} \<subseteq> {(x,y). dist x y < a} \<and>
+ {(x,y). dist x y < e} \<subseteq> {(x,y). dist x y < b}\<close> if \<open>a>0\<close> \<open>b>0\<close> for a b
+ apply (rule bexI[of _ \<open>min a b\<close>])
+ using that by auto
+ have 2: \<open>mono (\<lambda>P. eventually (\<lambda>x. P (Q x)) F)\<close> for F :: \<open>'z filter\<close> and Q :: \<open>'z \<Rightarrow> 'y\<close>
+ unfolding mono_def using eventually_mono le_funD by fastforce
+ have \<open>\<forall>\<^sub>F ((x1::'a,y1),(x2::'b,y2)) in uniformity \<times>\<^sub>F uniformity. dist x1 y1 < e/2 \<and> dist x2 y2 < e/2\<close> if \<open>e>0\<close> for e
+ by (auto intro!: eventually_prodI exI[of _ \<open>e/2\<close>] simp: case_prod_unfold eventually_uniformity_metric that)
+ then have 3: \<open>\<forall>\<^sub>F ((x1::'a,y1),(x2::'b,y2)) in uniformity \<times>\<^sub>F uniformity. dist (x1,x2) (y1,y2) < e\<close> if \<open>e>0\<close> for e
+ apply (rule eventually_rev_mp)
+ by (auto intro!: that eventuallyI simp: case_prod_unfold dist_prod_def sqrt_sum_squares_half_less)
+ show \<open>eventually P (INF e\<in>{0<..}. principal {(x, y). dist x y < e}) \<Longrightarrow> eventually P uniformity\<close>
+ apply (subst (asm) eventually_INF_base)
+ using 1 3 apply (auto simp: uniformity_prod_def case_prod_unfold eventually_filtermap 2 eventually_principal)
+ by (smt (verit, best) eventually_mono)
+ next
+ fix P :: \<open>('a \<times> 'b) \<times> ('a \<times> 'b) \<Rightarrow> bool\<close>
+ assume \<open>eventually P uniformity\<close>
+ then obtain P1 P2 where \<open>eventually P1 uniformity\<close> \<open>eventually P2 uniformity\<close>
+ and P1P2P: \<open>P1 (x1, y1) \<Longrightarrow> P2 (x2, y2) \<Longrightarrow> P ((x1, x2), (y1, y2))\<close> for x1 y1 x2 y2
+ by (auto simp: eventually_filtermap case_prod_beta eventually_prod_filter uniformity_prod_def)
+ from \<open>eventually P1 uniformity\<close> obtain e1 where \<open>e1>0\<close> and e1P1: \<open>dist x y < e1 \<Longrightarrow> P1 (x,y)\<close> for x y
+ using eventually_uniformity_metric by blast
+ from \<open>eventually P2 uniformity\<close> obtain e2 where \<open>e2>0\<close> and e2P2: \<open>dist x y < e2 \<Longrightarrow> P2 (x,y)\<close> for x y
+ using eventually_uniformity_metric by blast
+ define e where \<open>e = min e1 e2\<close>
+ have \<open>e > 0\<close>
+ using \<open>0 < e1\<close> \<open>0 < e2\<close> e_def by auto
+ have \<open>dist (x1,x2) (y1,y2) < e \<Longrightarrow> dist x1 y1 < e1\<close> for x1 y1 :: 'a and x2 y2 :: 'b
+ unfolding dist_prod_def e_def apply auto
+ by (smt (verit, best) real_sqrt_sum_squares_ge1)
+ moreover have \<open>dist (x1,x2) (y1,y2) < e \<Longrightarrow> dist x2 y2 < e2\<close> for x1 y1 :: 'a and x2 y2 :: 'b
+ unfolding dist_prod_def e_def apply auto
+ by (smt (verit, best) real_sqrt_sum_squares_ge1)
+ ultimately have *: \<open>dist (x1,x2) (y1,y2) < e \<Longrightarrow> P ((x1, x2), (y1, y2))\<close> for x1 y1 x2 y2
+ using e1P1 e2P2 P1P2P by auto
+
+ show \<open>eventually P (INF e\<in>{0<..}. principal {(x, y). dist x y < e})\<close>
+ apply (rule eventually_INF1[where i=e])
+ using \<open>e > 0\<close> * by (auto simp: eventually_principal)
+ qed
+qed
end
declare uniformity_Abort[where 'a="'a :: metric_space \<times> 'b :: metric_space", code]
@@ -221,24 +356,21 @@
ultimately show "\<exists>A B. open A \<and> open B \<and> x \<in> A \<times> B \<and> A \<times> B \<subseteq> S" by fast
qed
qed
- show "open S = (\<forall>x\<in>S. \<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> y \<in> S)"
- unfolding * eventually_uniformity_metric
- by (simp del: split_paired_All add: dist_prod_def dist_commute)
qed
end
declare [[code abort: "dist::('a::metric_space*'b::metric_space)\<Rightarrow>('a*'b) \<Rightarrow> real"]]
-lemma Cauchy_fst: "Cauchy X \<Longrightarrow> Cauchy (\<lambda>n. fst (X n))"
+lemma Cauchy_fst: "Cauchy X \<Longrightarrow> Cauchy (\<lambda>n. fst (X n :: 'a::metric_space \<times> 'b::metric_space))"
unfolding Cauchy_def by (fast elim: le_less_trans [OF dist_fst_le])
-lemma Cauchy_snd: "Cauchy X \<Longrightarrow> Cauchy (\<lambda>n. snd (X n))"
+lemma Cauchy_snd: "Cauchy X \<Longrightarrow> Cauchy (\<lambda>n. snd (X n :: 'a::metric_space \<times> 'b::metric_space))"
unfolding Cauchy_def by (fast elim: le_less_trans [OF dist_snd_le])
lemma Cauchy_Pair:
assumes "Cauchy X" and "Cauchy Y"
- shows "Cauchy (\<lambda>n. (X n, Y n))"
+ shows "Cauchy (\<lambda>n. (X n :: 'a::metric_space, Y n :: 'a::metric_space))"
proof (rule metric_CauchyI)
fix r :: real assume "0 < r"
hence "0 < r / sqrt 2" (is "0 < ?s") by simp
@@ -251,6 +383,56 @@
then show "\<exists>n0. \<forall>m\<ge>n0. \<forall>n\<ge>n0. dist (X m, Y m) (X n, Y n) < r" ..
qed
+text \<open>Analogue to @{thm [source] uniformly_continuous_on_def} for two-argument functions.\<close>
+lemma uniformly_continuous_on_prod_metric:
+ fixes f :: \<open>('a::metric_space \<times> 'b::metric_space) \<Rightarrow> 'c::metric_space\<close>
+ shows \<open>uniformly_continuous_on (S\<times>T) f \<longleftrightarrow> (\<forall>e>0. \<exists>d>0. \<forall>x\<in>S. \<forall>y\<in>S. \<forall>x'\<in>T. \<forall>y'\<in>T. dist x y < d \<longrightarrow> dist x' y' < d \<longrightarrow> dist (f (x, x')) (f (y, y')) < e)\<close>
+proof (unfold uniformly_continuous_on_def, intro iffI impI allI)
+ fix e :: real
+ assume \<open>e > 0\<close> and \<open>\<forall>e>0. \<exists>d>0. \<forall>x\<in>S. \<forall>y\<in>S. \<forall>x'\<in>T. \<forall>y'\<in>T. dist x y < d \<longrightarrow> dist x' y' < d \<longrightarrow> dist (f (x, x')) (f (y, y')) < e\<close>
+ then obtain d where \<open>d > 0\<close>
+ and d: \<open>\<forall>x\<in>S. \<forall>y\<in>S. \<forall>x'\<in>T. \<forall>y'\<in>T. dist x y < d \<longrightarrow> dist x' y' < d \<longrightarrow> dist (f (x, x')) (f (y, y')) < e\<close>
+ by auto
+ show \<open>\<exists>d>0. \<forall>x\<in>S\<times>T. \<forall>y\<in>S\<times>T. dist y x < d \<longrightarrow> dist (f y) (f x) < e\<close>
+ apply (rule exI[of _ d])
+ using \<open>d>0\<close> d[rule_format] apply auto
+ by (smt (verit, del_insts) dist_fst_le dist_snd_le fst_conv snd_conv)
+next
+ fix e :: real
+ assume \<open>e > 0\<close> and \<open>\<forall>e>0. \<exists>d>0. \<forall>x\<in>S\<times>T. \<forall>x'\<in>S\<times>T. dist x' x < d \<longrightarrow> dist (f x') (f x) < e\<close>
+ then obtain d where \<open>d > 0\<close> and d: \<open>\<forall>x\<in>S\<times>T. \<forall>x'\<in>S\<times>T. dist x' x < d \<longrightarrow> dist (f x') (f x) < e\<close>
+ by auto
+ show \<open>\<exists>d>0. \<forall>x\<in>S. \<forall>y\<in>S. \<forall>x'\<in>T. \<forall>y'\<in>T. dist x y < d \<longrightarrow> dist x' y' < d \<longrightarrow> dist (f (x, x')) (f (y, y')) < e\<close>
+ proof (intro exI conjI impI ballI)
+ from \<open>d > 0\<close> show \<open>d / 2 > 0\<close> by auto
+ fix x y x' y'
+ assume [simp]: \<open>x \<in> S\<close> \<open>y \<in> S\<close> \<open>x' \<in> T\<close> \<open>y' \<in> T\<close>
+ assume \<open>dist x y < d / 2\<close> and \<open>dist x' y' < d / 2\<close>
+ then have \<open>dist (x, x') (y, y') < d\<close>
+ by (simp add: dist_Pair_Pair sqrt_sum_squares_half_less)
+ with d show \<open>dist (f (x, x')) (f (y, y')) < e\<close>
+ by auto
+ qed
+qed
+
+text \<open>Analogue to @{thm [source] isUCont_def} for two-argument functions.\<close>
+lemma isUCont_prod_metric:
+ fixes f :: \<open>('a::metric_space \<times> 'b::metric_space) \<Rightarrow> 'c::metric_space\<close>
+ shows \<open>isUCont f \<longleftrightarrow> (\<forall>e>0. \<exists>d>0. \<forall>x. \<forall>y. \<forall>x'. \<forall>y'. dist x y < d \<longrightarrow> dist x' y' < d \<longrightarrow> dist (f (x, x')) (f (y, y')) < e)\<close>
+ using uniformly_continuous_on_prod_metric[of UNIV UNIV]
+ by auto
+
+text \<open>This logically belong with the real vector spaces by we only have the necessary lemmas now.\<close>
+lemma isUCont_plus[simp]:
+ shows \<open>isUCont (\<lambda>(x::'a::real_normed_vector,y). x+y)\<close>
+proof (rule isUCont_prod_metric[THEN iffD2], intro allI impI, simp)
+ fix e :: real assume \<open>0 < e\<close>
+ show \<open>\<exists>d>0. \<forall>x y :: 'a. dist x y < d \<longrightarrow> (\<forall>x' y'. dist x' y' < d \<longrightarrow> dist (x + x') (y + y') < e)\<close>
+ apply (rule exI[of _ \<open>e/2\<close>])
+ using \<open>0 < e\<close> apply auto
+ by (smt (verit, ccfv_SIG) dist_add_cancel dist_add_cancel2 dist_commute dist_triangle_lt)
+qed
+
subsection \<open>Product is a Complete Metric Space\<close>
instance\<^marker>\<open>tag important\<close> prod :: (complete_space, complete_space) complete_space
--- a/src/HOL/Analysis/document/root.bib Thu Oct 07 10:34:48 2021 +0200
+++ b/src/HOL/Analysis/document/root.bib Wed Oct 06 14:19:46 2021 +0200
@@ -23,4 +23,12 @@
bibsource = {dblp computer science bibliography, https://dblp.org}
}
+@book{conway2013course,
+ title={A course in functional analysis},
+ author={Conway, John B},
+ volume={96},
+ year={2013},
+ publisher={Springer Science \& Business Media}
+}
+
@misc{dummy}
--- a/src/HOL/Complex_Analysis/Winding_Numbers.thy Thu Oct 07 10:34:48 2021 +0200
+++ b/src/HOL/Complex_Analysis/Winding_Numbers.thy Wed Oct 06 14:19:46 2021 +0200
@@ -529,7 +529,7 @@
fixes z::complex
assumes \<gamma>: "valid_path \<gamma>" and z: "z \<notin> path_image \<gamma>" and 1: "Re (winding_number \<gamma> z) \<ge> 1"
and w: "w \<noteq> z"
- shows "\<exists>a::real. 0 < a \<and> z + a*(w - z) \<in> path_image \<gamma>"
+ shows "\<exists>a::real. 0 < a \<and> z + of_real a * (w - z) \<in> path_image \<gamma>"
proof -
have [simp]: "\<And>x. 0 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> \<gamma> x \<noteq> z"
using z by (auto simp: path_image_def)
@@ -582,7 +582,7 @@
fixes z::complex
assumes \<gamma>: "valid_path \<gamma>" and z: "z \<notin> path_image \<gamma>" and "\<bar>Re (winding_number \<gamma> z)\<bar> \<ge> 1"
and w: "w \<noteq> z"
- shows "\<exists>a::real. 0 < a \<and> z + a*(w - z) \<in> path_image \<gamma>"
+ shows "\<exists>a::real. 0 < a \<and> z + of_real a * (w - z) \<in> path_image \<gamma>"
proof -
{ assume "Re (winding_number \<gamma> z) \<le> - 1"
then have "Re (winding_number (reversepath \<gamma>) z) \<ge> 1"
@@ -591,7 +591,7 @@
using \<gamma> valid_path_imp_reverse by auto
moreover have "z \<notin> path_image (reversepath \<gamma>)"
by (simp add: z)
- ultimately have "\<exists>a::real. 0 < a \<and> z + a*(w - z) \<in> path_image (reversepath \<gamma>)"
+ ultimately have "\<exists>a::real. 0 < a \<and> z + of_real a * (w - z) \<in> path_image (reversepath \<gamma>)"
using winding_number_pos_meets w by blast
then have ?thesis
by simp
@@ -605,7 +605,7 @@
fixes z::complex
shows
"\<lbrakk>valid_path \<gamma>; z \<notin> path_image \<gamma>; w \<noteq> z;
- \<And>a::real. 0 < a \<Longrightarrow> z + a*(w - z) \<notin> path_image \<gamma>\<rbrakk>
+ \<And>a::real. 0 < a \<Longrightarrow> z + of_real a * (w - z) \<notin> path_image \<gamma>\<rbrakk>
\<Longrightarrow> Re(winding_number \<gamma> z) < 1"
by (auto simp: not_less dest: winding_number_big_meets)
@@ -1736,7 +1736,7 @@
ultimately
have pa_subset_pm_kde: "path_image ?q \<inter> closed_segment (a - kde) (a + kde) \<subseteq> {a - kde, a + kde}"
by (auto simp: path_image_join assms)
- have ge_kde1: "\<exists>y. x = a + y \<and> y \<ge> kde" if x: "x \<in> closed_segment (a + kde) (a + e)" for x
+ have ge_kde1: "\<exists>y. x = a + of_real y \<and> y \<ge> kde" if x: "x \<in> closed_segment (a + kde) (a + e)" for x
proof -
obtain u where "0 \<le> u" "u \<le> 1" and u: "x = (1 - u) *\<^sub>R (a + kde) + u *\<^sub>R (a + e)"
using x by (auto simp: in_segment)
@@ -1747,7 +1747,7 @@
ultimately
show ?thesis by blast
qed
- have ge_kde2: "\<exists>y. x = a + y \<and> y \<le> -kde" if x: "x \<in> closed_segment (a - d) (a - kde)" for x
+ have ge_kde2: "\<exists>y. x = a + of_real y \<and> y \<le> -kde" if x: "x \<in> closed_segment (a - d) (a - kde)" for x
proof -
obtain u where "0 \<le> u" "u \<le> 1" and u: "x = (1 - u) *\<^sub>R (a - d) + u *\<^sub>R (a - kde)"
using x by (auto simp: in_segment)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Complex_Order.thy Wed Oct 06 14:19:46 2021 +0200
@@ -0,0 +1,39 @@
+(*
+ Title: HOL/Library/Complex_Order.thy
+ Author: Dominique Unruh, University of Tartu
+
+ Instantiation of complex numbers as an ordered set.
+*)
+
+theory Complex_Order
+ imports Complex_Main
+begin
+
+instantiation complex :: order begin
+
+definition \<open>x < y \<longleftrightarrow> Re x < Re y \<and> Im x = Im y\<close>
+definition \<open>x \<le> y \<longleftrightarrow> Re x \<le> Re y \<and> Im x = Im y\<close>
+
+instance
+ apply standard
+ by (auto simp: less_complex_def less_eq_complex_def complex_eq_iff)
+end
+
+lemma nonnegative_complex_is_real: \<open>(x::complex) \<ge> 0 \<Longrightarrow> x \<in> \<real>\<close>
+ by (simp add: complex_is_Real_iff less_eq_complex_def)
+
+lemma complex_is_real_iff_compare0: \<open>(x::complex) \<in> \<real> \<longleftrightarrow> x \<le> 0 \<or> x \<ge> 0\<close>
+ using complex_is_Real_iff less_eq_complex_def by auto
+
+instance complex :: ordered_comm_ring
+ apply standard
+ by (auto simp: less_complex_def less_eq_complex_def complex_eq_iff mult_left_mono mult_right_mono)
+
+instance complex :: ordered_real_vector
+ apply standard
+ by (auto simp: less_complex_def less_eq_complex_def mult_left_mono mult_right_mono)
+
+instance complex :: ordered_cancel_comm_semiring
+ by standard
+
+end
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy Thu Oct 07 10:34:48 2021 +0200
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy Wed Oct 06 14:19:46 2021 +0200
@@ -1173,6 +1173,17 @@
lemma ennreal_of_enat_eSuc[simp]: "ennreal_of_enat (eSuc x) = 1 + ennreal_of_enat x"
by (cases x) (auto simp: eSuc_enat)
+(* Contributed by Dominique Unruh *)
+lemma ennreal_of_enat_plus[simp]: \<open>ennreal_of_enat (a+b) = ennreal_of_enat a + ennreal_of_enat b\<close>
+ apply (induction a)
+ apply auto
+ by (smt (z3) add.commute add.right_neutral enat.exhaust enat.simps(4) enat.simps(5) ennreal_add_left_cancel ennreal_of_enat_def infinity_ennreal_def of_nat_add of_nat_eq_enat plus_enat_simps(2))
+
+(* Contributed by Dominique Unruh *)
+lemma sum_ennreal_of_enat[simp]: "(\<Sum>i\<in>I. ennreal_of_enat (f i)) = ennreal_of_enat (sum f I)"
+ apply (induction I rule: infinite_finite_induct)
+ by (auto simp: sum_nonneg)
+
subsection \<open>Topology on \<^typ>\<open>ennreal\<close>\<close>
lemma enn2ereal_Iio: "enn2ereal -` {..<a} = (if 0 \<le> a then {..< e2ennreal a} else {})"
@@ -1657,6 +1668,60 @@
apply (auto simp del: sup_ereal_def simp add: sup_INF)
done
+(* Contributed by Dominique Unruh *)
+lemma isCont_ennreal[simp]: \<open>isCont ennreal x\<close>
+ apply (auto intro!: sequentially_imp_eventually_within simp: continuous_within tendsto_def)
+ by (metis tendsto_def tendsto_ennrealI)
+
+(* Contributed by Dominique Unruh *)
+lemma isCont_ennreal_of_enat[simp]: \<open>isCont ennreal_of_enat x\<close>
+proof -
+ have continuous_at_open:
+ \<comment> \<open>Copied lemma from \<^session>\<open>HOL-Analysis\<close> to avoid dependency.\<close>
+ "continuous (at x) f \<longleftrightarrow> (\<forall>t. open t \<and> f x \<in> t --> (\<exists>s. open s \<and> x \<in> s \<and> (\<forall>x' \<in> s. (f x') \<in> t)))" for f :: \<open>enat \<Rightarrow> 'z::topological_space\<close>
+ unfolding continuous_within_topological [of x UNIV f]
+ unfolding imp_conjL
+ by (intro all_cong imp_cong ex_cong conj_cong refl) auto
+ show ?thesis
+ proof (subst continuous_at_open, intro allI impI, cases \<open>x = \<infinity>\<close>)
+ case True
+
+ fix t assume \<open>open t \<and> ennreal_of_enat x \<in> t\<close>
+ then have \<open>\<exists>y<\<infinity>. {y <.. \<infinity>} \<subseteq> t\<close>
+ apply (rule_tac open_left[where y=0])
+ by (auto simp: True)
+ then obtain y where \<open>{y<..} \<subseteq> t\<close> and \<open>y \<noteq> \<infinity>\<close>
+ apply atomize_elim
+ apply (auto simp: greaterThanAtMost_def)
+ by (metis atMost_iff inf.orderE subsetI top.not_eq_extremum top_greatest)
+
+ from \<open>y \<noteq> \<infinity>\<close>
+ obtain x' where x'y: \<open>ennreal_of_enat x' > y\<close> and \<open>x' \<noteq> \<infinity>\<close>
+ by (metis enat.simps(3) ennreal_Ex_less_of_nat ennreal_of_enat_enat infinity_ennreal_def top.not_eq_extremum)
+ define s where \<open>s = {x'<..}\<close>
+ have \<open>open s\<close>
+ by (simp add: s_def)
+ moreover have \<open>x \<in> s\<close>
+ by (simp add: \<open>x' \<noteq> \<infinity>\<close> s_def True)
+ moreover have \<open>ennreal_of_enat z \<in> t\<close> if \<open>z \<in> s\<close> for z
+ by (metis x'y \<open>{y<..} \<subseteq> t\<close> ennreal_of_enat_le_iff greaterThan_iff le_less_trans less_imp_le not_less s_def subsetD that)
+ ultimately show \<open>\<exists>s. open s \<and> x \<in> s \<and> (\<forall>z\<in>s. ennreal_of_enat z \<in> t)\<close>
+ by auto
+ next
+ case False
+ fix t assume asm: \<open>open t \<and> ennreal_of_enat x \<in> t\<close>
+ define s where \<open>s = {x}\<close>
+ have \<open>open s\<close>
+ using False open_enat_iff s_def by blast
+ moreover have \<open>x \<in> s\<close>
+ using s_def by auto
+ moreover have \<open>ennreal_of_enat z \<in> t\<close> if \<open>z \<in> s\<close> for z
+ using asm s_def that by blast
+ ultimately show \<open>\<exists>s. open s \<and> x \<in> s \<and> (\<forall>z\<in>s. ennreal_of_enat z \<in> t)\<close>
+ by auto
+ qed
+qed
+
subsection \<open>Approximation lemmas\<close>
lemma INF_approx_ennreal:
--- a/src/HOL/Limits.thy Thu Oct 07 10:34:48 2021 +0200
+++ b/src/HOL/Limits.thy Wed Oct 06 14:19:46 2021 +0200
@@ -1000,7 +1000,7 @@
unfolding tendsto_iff by simp
lemma tendsto_add_const_iff:
- "((\<lambda>x. c + f x :: 'a::real_normed_vector) \<longlongrightarrow> c + d) F \<longleftrightarrow> (f \<longlongrightarrow> d) F"
+ "((\<lambda>x. c + f x :: 'a::topological_group_add) \<longlongrightarrow> c + d) F \<longleftrightarrow> (f \<longlongrightarrow> d) F"
using tendsto_add[OF tendsto_const[of c], of f d]
and tendsto_add[OF tendsto_const[of "-c"], of "\<lambda>x. c + f x" "c + d"] by auto
--- a/src/HOL/ROOT Thu Oct 07 10:34:48 2021 +0200
+++ b/src/HOL/ROOT Wed Oct 06 14:19:46 2021 +0200
@@ -76,6 +76,7 @@
Code_Real_Approx_By_Float
Code_Target_Numeral
Code_Target_Numeral_Float
+ Complex_Order
DAList
DAList_Multiset
RBT_Mapping
--- a/src/HOL/Real_Vector_Spaces.thy Thu Oct 07 10:34:48 2021 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy Wed Oct 06 14:19:46 2021 +0200
@@ -1781,6 +1781,38 @@
by auto
qed (auto intro!: exI[of _ "{y. dist x y < e}" for e] open_ball simp: dist_commute)
+(* Contributed by Dominique Unruh *)
+lemma tendsto_iff_uniformity:
+ \<comment> \<open>More general analogus of \<open>tendsto_iff\<close> below. Applies to all uniform spaces, not just metric ones.\<close>
+ fixes l :: \<open>'b :: uniform_space\<close>
+ shows \<open>(f \<longlongrightarrow> l) F \<longleftrightarrow> (\<forall>E. eventually E uniformity \<longrightarrow> (\<forall>\<^sub>F x in F. E (f x, l)))\<close>
+proof (intro iffI allI impI)
+ fix E :: \<open>('b \<times> 'b) \<Rightarrow> bool\<close>
+ assume \<open>(f \<longlongrightarrow> l) F\<close> and \<open>eventually E uniformity\<close>
+ from \<open>eventually E uniformity\<close>
+ have \<open>eventually (\<lambda>(x, y). E (y, x)) uniformity\<close>
+ by (simp add: uniformity_sym)
+ then have \<open>\<forall>\<^sub>F (y, x) in uniformity. y = l \<longrightarrow> E (x, y)\<close>
+ using eventually_mono by fastforce
+ with \<open>(f \<longlongrightarrow> l) F\<close> have \<open>eventually (\<lambda>x. E (x ,l)) (filtermap f F)\<close>
+ by (simp add: filterlim_def le_filter_def eventually_nhds_uniformity)
+ then show \<open>\<forall>\<^sub>F x in F. E (f x, l)\<close>
+ by (simp add: eventually_filtermap)
+next
+ assume assm: \<open>\<forall>E. eventually E uniformity \<longrightarrow> (\<forall>\<^sub>F x in F. E (f x, l))\<close>
+ have \<open>eventually P (filtermap f F)\<close> if \<open>\<forall>\<^sub>F (x, y) in uniformity. x = l \<longrightarrow> P y\<close> for P
+ proof -
+ from that have \<open>\<forall>\<^sub>F (y, x) in uniformity. x = l \<longrightarrow> P y\<close>
+ using uniformity_sym[where E=\<open>\<lambda>(x,y). x=l \<longrightarrow> P y\<close>] by auto
+ with assm have \<open>\<forall>\<^sub>F x in F. P (f x)\<close>
+ by auto
+ then show ?thesis
+ by (auto simp: eventually_filtermap)
+ qed
+ then show \<open>(f \<longlongrightarrow> l) F\<close>
+ by (simp add: filterlim_def le_filter_def eventually_nhds_uniformity)
+qed
+
lemma (in metric_space) tendsto_iff: "(f \<longlongrightarrow> l) F \<longleftrightarrow> (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) F)"
unfolding nhds_metric filterlim_INF filterlim_principal by auto
@@ -2186,6 +2218,52 @@
done
+setup \<open>Sign.add_const_constraint (\<^const_name>\<open>dist\<close>, SOME \<^typ>\<open>'a::dist \<Rightarrow> 'a \<Rightarrow> real\<close>)\<close>
+
+(* Contributed by Dominique Unruh *)
+lemma cauchy_filter_metric:
+ fixes F :: "'a::{uniformity_dist,uniform_space} filter"
+ shows "cauchy_filter F \<longleftrightarrow> (\<forall>e. e>0 \<longrightarrow> (\<exists>P. eventually P F \<and> (\<forall>x y. P x \<and> P y \<longrightarrow> dist x y < e)))"
+proof (unfold cauchy_filter_def le_filter_def, auto)
+ assume assm: \<open>\<forall>e>0. \<exists>P. eventually P F \<and> (\<forall>x y. P x \<and> P y \<longrightarrow> dist x y < e)\<close>
+ then show \<open>eventually P uniformity \<Longrightarrow> eventually P (F \<times>\<^sub>F F)\<close> for P
+ apply (auto simp: eventually_uniformity_metric)
+ using eventually_prod_same by blast
+next
+ fix e :: real
+ assume \<open>e > 0\<close>
+ assume asm: \<open>\<forall>P. eventually P uniformity \<longrightarrow> eventually P (F \<times>\<^sub>F F)\<close>
+
+ define P where \<open>P \<equiv> \<lambda>(x,y :: 'a). dist x y < e\<close>
+ with asm \<open>e > 0\<close> have \<open>eventually P (F \<times>\<^sub>F F)\<close>
+ by (metis case_prod_conv eventually_uniformity_metric)
+ then
+ show \<open>\<exists>P. eventually P F \<and> (\<forall>x y. P x \<and> P y \<longrightarrow> dist x y < e)\<close>
+ by (auto simp add: eventually_prod_same P_def)
+qed
+
+(* Contributed by Dominique Unruh *)
+lemma cauchy_filter_metric_filtermap:
+ fixes f :: "'a \<Rightarrow> 'b::{uniformity_dist,uniform_space}"
+ shows "cauchy_filter (filtermap f F) \<longleftrightarrow> (\<forall>e. e>0 \<longrightarrow> (\<exists>P. eventually P F \<and> (\<forall>x y. P x \<and> P y \<longrightarrow> dist (f x) (f y) < e)))"
+proof (subst cauchy_filter_metric, intro iffI allI impI)
+ assume \<open>\<forall>e>0. \<exists>P. eventually P (filtermap f F) \<and> (\<forall>x y. P x \<and> P y \<longrightarrow> dist x y < e)\<close>
+ then show \<open>e>0 \<Longrightarrow> \<exists>P. eventually P F \<and> (\<forall>x y. P x \<and> P y \<longrightarrow> dist (f x) (f y) < e)\<close> for e
+ unfolding eventually_filtermap by blast
+next
+ assume asm: \<open>\<forall>e>0. \<exists>P. eventually P F \<and> (\<forall>x y. P x \<and> P y \<longrightarrow> dist (f x) (f y) < e)\<close>
+ fix e::real assume \<open>e > 0\<close>
+ then obtain P where \<open>eventually P F\<close> and PPe: \<open>P x \<and> P y \<longrightarrow> dist (f x) (f y) < e\<close> for x y
+ using asm by blast
+
+ show \<open>\<exists>P. eventually P (filtermap f F) \<and> (\<forall>x y. P x \<and> P y \<longrightarrow> dist x y < e)\<close>
+ apply (rule exI[of _ \<open>\<lambda>x. \<exists>y. P y \<and> x = f y\<close>])
+ using PPe \<open>eventually P F\<close> apply (auto simp: eventually_filtermap)
+ by (smt (verit, ccfv_SIG) eventually_elim2)
+qed
+
+setup \<open>Sign.add_const_constraint (\<^const_name>\<open>dist\<close>, SOME \<^typ>\<open>'a::metric_space \<Rightarrow> 'a \<Rightarrow> real\<close>)\<close>
+
subsubsection \<open>Cauchy Sequences are Convergent\<close>
(* TODO: update to uniform_space *)
--- a/src/HOL/Topological_Spaces.thy Thu Oct 07 10:34:48 2021 +0200
+++ b/src/HOL/Topological_Spaces.thy Wed Oct 06 14:19:46 2021 +0200
@@ -788,6 +788,11 @@
lemma tendsto_eventually: "eventually (\<lambda>x. f x = l) net \<Longrightarrow> ((\<lambda>x. f x) \<longlongrightarrow> l) net"
by (rule topological_tendstoI) (auto elim: eventually_mono)
+(* Contributed by Dominique Unruh *)
+lemma tendsto_principal_singleton[simp]:
+ shows "(f \<longlongrightarrow> f x) (principal {x})"
+ unfolding tendsto_def eventually_principal by simp
+
end
lemma (in topological_space) filterlim_within_subset:
@@ -3438,7 +3443,6 @@
end
-
subsubsection \<open>Uniformly continuous functions\<close>
definition uniformly_continuous_on :: "'a set \<Rightarrow> ('a::uniform_space \<Rightarrow> 'b::uniform_space) \<Rightarrow> bool"