--- a/src/HOL/Analysis/Infinite_Sum.thy Mon Nov 15 17:26:31 2021 +0100
+++ b/src/HOL/Analysis/Infinite_Sum.thy Mon Nov 15 18:04:07 2021 +0100
@@ -1,8 +1,9 @@
(*
Title: HOL/Analysis/Infinite_Sum.thy
Author: Dominique Unruh, University of Tartu
+ Manuel Eberl, University of Innsbruck
- A theory of sums over possible infinite sets.
+ A theory of sums over possibly infinite sets.
*)
section \<open>Infinite sums\<close>
@@ -23,7 +24,7 @@
theory Infinite_Sum
imports
- "HOL-Analysis.Elementary_Topology"
+ Elementary_Topology
"HOL-Library.Extended_Nonnegative_Real"
"HOL-Library.Complex_Order"
begin
@@ -107,6 +108,14 @@
shows \<open>infsum f A = 0\<close>
by (simp add: assms infsum_def)
+lemma summable_iff_has_sum_infsum: "f summable_on A \<longleftrightarrow> has_sum f A (infsum f A)"
+ using infsumI summable_on_def by blast
+
+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 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>
@@ -131,8 +140,7 @@
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 -
+ finally show ?thesis .
qed
with \<open>F0' \<subseteq> T\<close> \<open>finite F0'\<close> show \<open>eventually P (filtermap (sum g) (finite_subsets_at_top T))\<close>
by (metis (no_types, lifting) eventually_filtermap eventually_finite_subsets_at_top)
@@ -151,8 +159,7 @@
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 -
+ finally show ?thesis .
qed
with \<open>F0' \<subseteq> S\<close> \<open>finite F0'\<close> show \<open>eventually P (filtermap (sum f) (finite_subsets_at_top S))\<close>
by (metis (no_types, lifting) eventually_filtermap eventually_finite_subsets_at_top)
@@ -186,7 +193,7 @@
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)
+ using assms by (intro has_sum_cong_neutral) auto
lemma summable_on_cong:
assumes "\<And>x. x\<in>A \<Longrightarrow> f x = g x"
@@ -361,9 +368,7 @@
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)+
+ by (rule has_sum_mono_neutral[of f A _ g B _]) (use assms in \<open>auto intro: has_sum_infsum\<close>)
lemma has_sum_mono:
fixes f :: "'a\<Rightarrow>'b::{ordered_comm_monoid_add,linorder_topology}"
@@ -407,15 +412,20 @@
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)
+ thus ?thesis
+ unfolding eventually_finite_subsets_at_top by fastforce
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)
+proof -
+ from assms have "has_sum f A (infsum f A)"
+ by (simp add: summable_iff_has_sum_infsum)
+ from this and \<open>\<epsilon> > 0\<close> show ?thesis
+ by (rule has_sum_finite_approximation)
+qed
lemma abs_summable_summable:
fixes f :: \<open>'a \<Rightarrow> 'b :: banach\<close>
@@ -435,7 +445,7 @@
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
@@ -447,29 +457,26 @@
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 (verit, ccfv_threshold) 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)
+ have dist_F_subset: \<open>dist (sum f F) (sum f F') < 2*d\<close> if F': \<open>F' \<subseteq> F\<close> \<open>P F'\<close> for F'
+ proof -
+ have \<open>dist (sum f F) (sum f F') = norm (sum f (F-F'))\<close>
+ unfolding dist_norm using \<open>finite F\<close> F' by (subst sum_diff) auto
+ also have \<open>\<dots> \<le> norm (\<Sum>x\<in>F-F'. norm (f x))\<close>
+ by (rule order.trans[OF sum_norm_le[OF order.refl]]) auto
+ also have \<open>\<dots> = dist (\<Sum>x\<in>F. norm (f x)) (\<Sum>x\<in>F'. norm (f x))\<close>
+ unfolding dist_norm using \<open>finite F\<close> F' by (subst sum_diff) auto
+ also have \<open>\<dots> < 2 * d\<close>
+ using dist_F F' unfolding P_def dist_norm real_norm_def by linarith
+ finally show \<open>dist (sum f F) (sum f F') < 2*d\<close> .
+ qed
- 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 (verit, best) 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))
+ have \<open>dist (sum f F1) (sum f F2) \<le> dist (sum f F) (sum f F1) + dist (sum f F) (sum f F2)\<close>
+ by (rule dist_triangle3)
+ also have \<open>\<dots> < 2 * d + 2 * d\<close>
+ by (intro add_strict_mono dist_F_subset that) (auto simp: F_def)
+ also have \<open>\<dots> \<le> e\<close>
+ by (auto simp: d_def)
+ finally show \<open>dist (sum f F1) (sum f F2) < e\<close> .
qed
then show ?thesis
using ev_P by blast
@@ -583,11 +590,6 @@
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>
@@ -692,8 +694,13 @@
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)
+ by (intro infsumI has_sum_Un_disjoint has_sum_infsum assms)
+(* TODO move *)
+lemma (in uniform_space) cauchy_filter_complete_converges:
+ assumes "cauchy_filter F" "complete A" "F \<le> principal A" "F \<noteq> bot"
+ shows "\<exists>c. F \<le> nhds c"
+ using assms unfolding complete_uniform by blast
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:
@@ -720,68 +727,71 @@
assumes \<open>B \<subseteq> A\<close>
shows \<open>f summable_on B\<close>
proof -
+ let ?filter_fB = \<open>filtermap (sum f) (finite_subsets_at_top B)\<close>
from \<open>f summable_on A\<close>
obtain S where \<open>(sum f \<longlongrightarrow> S) (finite_subsets_at_top A)\<close> (is \<open>(sum f \<longlongrightarrow> S) ?filter_A\<close>)
using summable_on_def has_sum_def by blast
then have cauchy_fA: \<open>cauchy_filter (filtermap (sum f) (finite_subsets_at_top A))\<close> (is \<open>cauchy_filter ?filter_fA\<close>)
by (auto intro!: nhds_imp_cauchy_filter simp: filterlim_def)
- 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>
+ using plus_cont \<open>eventually E' uniformity\<close>
+ unfolding uniformly_continuous_on_uniformity filterlim_def le_filter_def uniformity_prod_def
+ by (auto simp: case_prod_beta eventually_filtermap eventually_prod_same uniformity_refl)
+ have DE': "E' (x, y)" if "D (x + c, y + c)" for x y c
+ using DE[of "x + c" "y + c" "-c"] that by simp
+
+ from \<open>eventually D uniformity\<close> and cauchy_fA have \<open>eventually D (?filter_fA \<times>\<^sub>F ?filter_fA)\<close>
unfolding cauchy_filter_def le_filter_def by simp
- then obtain P1 P2 where ev_P1: \<open>eventually (\<lambda>F. P1 (sum f F)) ?filter_A\<close> and ev_P2: \<open>eventually (\<lambda>F. P2 (sum f F)) ?filter_A\<close>
- and P1P2E: \<open>P1 x \<Longrightarrow> P2 y \<Longrightarrow> D (x, y)\<close> for x y
+ 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>
+ from ev_P1 obtain F1 where F1: \<open>finite F1\<close> \<open>F1 \<subseteq> A\<close> \<open>\<And>F. F\<supseteq>F1 \<Longrightarrow> finite F \<Longrightarrow> F\<subseteq>A \<Longrightarrow> P1 (sum f F)\<close>
by (metis eventually_finite_subsets_at_top)
- from ev_P2 obtain F2 where \<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>
+ from ev_P2 obtain F2 where F2: \<open>finite F2\<close> \<open>F2 \<subseteq> A\<close> \<open>\<And>F. F\<supseteq>F2 \<Longrightarrow> finite F \<Longrightarrow> F\<subseteq>A \<Longrightarrow> P2 (sum f F)\<close>
by (metis eventually_finite_subsets_at_top)
define F0 F0A F0B where \<open>F0 \<equiv> F1 \<union> F2\<close> and \<open>F0A \<equiv> F0 - B\<close> and \<open>F0B \<equiv> F0 \<inter> B\<close>
have [simp]: \<open>finite F0\<close> \<open>F0 \<subseteq> A\<close>
- 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')
+ using \<open>F1 \<subseteq> A\<close> \<open>F2 \<subseteq> A\<close> \<open>finite F1\<close> \<open>finite F2\<close> unfolding F0_def by blast+
+
+ have *: "E' (sum f F1', sum f F2')"
+ if "F1'\<supseteq>F0B" "F2'\<supseteq>F0B" "finite F1'" "finite F2'" "F1'\<subseteq>B" "F2'\<subseteq>B" for F1' F2'
+ proof (intro DE'[where c = "sum f F0A"] P1P2E)
+ have "P1 (sum f (F1' \<union> F0A))"
+ using that assms F1(1,2) F2(1,2) by (intro F1) (auto simp: F0A_def F0B_def F0_def)
+ thus "P1 (sum f F1' + sum f F0A)"
+ by (subst (asm) sum.union_disjoint) (use that in \<open>auto simp: F0A_def\<close>)
+ next
+ have "P2 (sum f (F2' \<union> F0A))"
+ using that assms F1(1,2) F2(1,2) by (intro F2) (auto simp: F0A_def F0B_def F0_def)
+ thus "P2 (sum f F2' + sum f F0A)"
+ by (subst (asm) sum.union_disjoint) (use that in \<open>auto simp: F0A_def\<close>)
+ qed
+
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
+ unfolding eventually_prod_filter
+ proof (safe intro!: exI)
+ show "eventually (\<lambda>x. E' (x, sum f F0B)) (filtermap (sum f) (finite_subsets_at_top B))"
+ and "eventually (\<lambda>x. E' (sum f F0B, x)) (filtermap (sum f) (finite_subsets_at_top B))"
+ unfolding eventually_filtermap eventually_finite_subsets_at_top
+ by (rule exI[of _ F0B]; use * in \<open>force simp: F0B_def\<close>)+
+ next
+ show "E (x, y)" if "E' (x, sum f F0B)" and "E' (sum f F0B, y)" for x y
+ using E'E'E that by blast
+ qed
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 obtain x where \<open>?filter_fB \<le> nhds x\<close>
+ using cauchy_filter_complete_converges[of ?filter_fB UNIV] \<open>complete (UNIV :: _)\<close>
+ by (auto simp: filtermap_bot_iff)
then have \<open>(sum f \<longlongrightarrow> x) (finite_subsets_at_top B)\<close>
by (auto simp: filterlim_def)
then show ?thesis
@@ -795,9 +805,8 @@
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)
+ by (rule summable_on_subset[OF _ _ assms])
+ (auto simp: complete_def convergent_def dest!: Cauchy_convergent)
lemma has_sum_empty[simp]: \<open>has_sum f {} 0\<close>
by (meson ex_in_conv has_sum_0)
@@ -847,9 +856,8 @@
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)
+ by (rule sym, rule infsumI)
+ (use sum_has_sum[of A f B \<open>\<lambda>a. infsum f (B a)\<close>] assms in auto)
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
@@ -897,7 +905,8 @@
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)
+ using assms
+ by (intro infsumI has_sum_comm_additive_general has_sum_infsum) (auto simp: isCont_def)
lemma has_sum_comm_additive:
fixes f :: \<open>'b :: {ab_group_add,topological_space} \<Rightarrow> 'c :: {ab_group_add,topological_space}\<close>
@@ -906,7 +915,8 @@
\<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)
+ using assms
+ by (intro has_sum_comm_additive_general has_sum_infsum) (auto simp: isCont_def additive.sum)
lemma summable_on_comm_additive:
fixes f :: \<open>'b :: {ab_group_add,t2_space} \<Rightarrow> 'c :: {ab_group_add,topological_space}\<close>
@@ -924,8 +934,7 @@
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:
+lemma nonneg_bdd_above_has_sum:
fixes f :: \<open>'a \<Rightarrow> 'b :: {conditionally_complete_linorder, ordered_comm_monoid_add, linorder_topology}\<close>
assumes \<open>\<And>x. x\<in>A \<Longrightarrow> f x \<ge> 0\<close>
assumes \<open>bdd_above (sum f ` {F. F\<subseteq>A \<and> finite F})\<close>
@@ -938,14 +947,24 @@
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)
+ proof (rule exI[of _ F], safe)
+ fix Y assume Y: "finite Y" "F \<subseteq> Y" "Y \<subseteq> A"
+ have "a < sum f F"
+ by fact
+ also have "\<dots> \<le> sum f Y"
+ using assms Y by (intro sum_mono2) auto
+ finally show "a < sum f Y" .
+ qed (use \<open>finite F\<close> \<open>F \<subseteq> A\<close> in auto)
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))
+ fix a assume *: \<open>(SUP F\<in>{F. finite F \<and> F\<subseteq>A}. sum f F) < a\<close>
+ have \<open>sum f F < a\<close> if \<open>F\<subseteq>A\<close> and \<open>finite F\<close> for F
+ proof -
+ have "sum f F \<le> (SUP F\<in>{F. finite F \<and> F\<subseteq>A}. sum f F)"
+ by (rule cSUP_upper) (use that assms(2) in \<open>auto simp: conj_commute\<close>)
+ also have "\<dots> < a"
+ by fact
+ finally show ?thesis .
+ qed
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
@@ -953,38 +972,37 @@
using has_sum_def by blast
qed
-lemma pos_summable_on:
+lemma nonneg_bdd_above_summable_on:
fixes f :: \<open>'a \<Rightarrow> 'b :: {conditionally_complete_linorder, ordered_comm_monoid_add, linorder_topology}\<close>
assumes \<open>\<And>x. x\<in>A \<Longrightarrow> f x \<ge> 0\<close>
assumes \<open>bdd_above (sum f ` {F. F\<subseteq>A \<and> finite F})\<close>
shows \<open>f summable_on A\<close>
- using assms(1) assms(2) summable_on_def pos_has_sum by blast
+ using assms(1) assms(2) summable_on_def nonneg_bdd_above_has_sum by blast
-
-lemma pos_infsum:
+lemma nonneg_bdd_above_infsum:
fixes f :: \<open>'a \<Rightarrow> 'b :: {conditionally_complete_linorder, ordered_comm_monoid_add, linorder_topology}\<close>
assumes \<open>\<And>x. x\<in>A \<Longrightarrow> f x \<ge> 0\<close>
assumes \<open>bdd_above (sum f ` {F. F\<subseteq>A \<and> finite F})\<close>
shows \<open>infsum f A = (SUP F\<in>{F. finite F \<and> F\<subseteq>A}. sum f F)\<close>
- using assms by (auto intro!: infsumI pos_has_sum)
+ using assms by (auto intro!: infsumI nonneg_bdd_above_has_sum)
-lemma pos_has_sum_complete:
+lemma nonneg_has_sum_complete:
fixes f :: \<open>'a \<Rightarrow> 'b :: {complete_linorder, ordered_comm_monoid_add, linorder_topology}\<close>
assumes \<open>\<And>x. x\<in>A \<Longrightarrow> f x \<ge> 0\<close>
shows \<open>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
+ using assms nonneg_bdd_above_has_sum by blast
-lemma pos_summable_on_complete:
+lemma nonneg_summable_on_complete:
fixes f :: \<open>'a \<Rightarrow> 'b :: {complete_linorder, ordered_comm_monoid_add, linorder_topology}\<close>
assumes \<open>\<And>x. x\<in>A \<Longrightarrow> f x \<ge> 0\<close>
shows \<open>f summable_on A\<close>
- using assms pos_summable_on by blast
+ using assms nonneg_bdd_above_summable_on by blast
-lemma pos_infsum_complete:
+lemma nonneg_infsum_complete:
fixes f :: \<open>'a \<Rightarrow> 'b :: {complete_linorder, ordered_comm_monoid_add, linorder_topology}\<close>
assumes \<open>\<And>x. x\<in>A \<Longrightarrow> f x \<ge> 0\<close>
shows \<open>infsum f A = (SUP F\<in>{F. finite F \<and> F\<subseteq>A}. sum f F)\<close>
- using assms pos_infsum by blast
+ using assms nonneg_bdd_above_infsum by blast
lemma has_sum_nonneg:
fixes f :: "'a \<Rightarrow> 'b::{ordered_comm_monoid_add,linorder_topology}"
@@ -995,10 +1013,51 @@
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"
+ assumes "\<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)
+ apply (cases \<open>f summable_on M\<close>)
+ apply (metis assms infsum_0_simp summable_on_0_simp infsum_mono)
+ using assms by (auto simp add: infsum_not_exists)
+
+lemma has_sum_mono2:
+ fixes f :: "'a \<Rightarrow> 'b::{topological_ab_group_add, ordered_comm_monoid_add,linorder_topology}"
+ assumes "has_sum f A S" "has_sum f B S'" "A \<subseteq> B"
+ assumes "\<And>x. x \<in> B - A \<Longrightarrow> f x \<ge> 0"
+ shows "S \<le> S'"
+proof -
+ have "has_sum f (B - A) (S' - S)"
+ by (rule has_sum_Diff) fact+
+ hence "S' - S \<ge> 0"
+ by (rule has_sum_nonneg) (use assms(4) in auto)
+ thus ?thesis
+ by (metis add_0 add_mono_thms_linordered_semiring(3) diff_add_cancel)
+qed
+
+lemma infsum_mono2:
+ fixes f :: "'a \<Rightarrow> 'b::{topological_ab_group_add, ordered_comm_monoid_add,linorder_topology}"
+ assumes "f summable_on A" "f summable_on B" "A \<subseteq> B"
+ assumes "\<And>x. x \<in> B - A \<Longrightarrow> f x \<ge> 0"
+ shows "infsum f A \<le> infsum f B"
+ by (rule has_sum_mono2[OF has_sum_infsum has_sum_infsum]) (use assms in auto)
+
+lemma finite_sum_le_has_sum:
+ fixes f :: "'a \<Rightarrow> 'b::{topological_ab_group_add, ordered_comm_monoid_add,linorder_topology}"
+ assumes "has_sum f A S" "finite B" "B \<subseteq> A"
+ assumes "\<And>x. x \<in> A - B \<Longrightarrow> f x \<ge> 0"
+ shows "sum f B \<le> S"
+proof (rule has_sum_mono2)
+ show "has_sum f A S"
+ by fact
+ show "has_sum f B (sum f B)"
+ by (rule has_sum_finite) fact+
+qed (use assms in auto)
+
+lemma finite_sum_le_infsum:
+ fixes f :: "'a \<Rightarrow> 'b::{topological_ab_group_add, ordered_comm_monoid_add,linorder_topology}"
+ assumes "f summable_on A" "finite B" "B \<subseteq> A"
+ assumes "\<And>x. x \<in> A - B \<Longrightarrow> f x \<ge> 0"
+ shows "sum f B \<le> infsum f A"
+ by (rule finite_sum_le_has_sum[OF has_sum_infsum]) (use assms in auto)
lemma has_sum_reindex:
assumes \<open>inj_on h A\<close>
@@ -1016,11 +1075,9 @@
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 -
+ finally show ?thesis .
qed
-
lemma summable_on_reindex:
assumes \<open>inj_on h A\<close>
shows \<open>g summable_on (h ` A) \<longleftrightarrow> (g \<circ> h) summable_on A\<close>
@@ -1029,8 +1086,32 @@
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)
+ 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 summable_on_reindex_bij_betw:
+ assumes "bij_betw g A B"
+ shows "(\<lambda>x. f (g x)) summable_on A \<longleftrightarrow> f summable_on B"
+proof -
+ thm summable_on_reindex
+ have \<open>(\<lambda>x. f (g x)) summable_on A \<longleftrightarrow> f summable_on g ` A\<close>
+ apply (rule summable_on_reindex[symmetric, unfolded o_def])
+ using assms bij_betw_imp_inj_on by blast
+ also have \<open>\<dots> \<longleftrightarrow> f summable_on B\<close>
+ using assms bij_betw_imp_surj_on by blast
+ finally show ?thesis .
+qed
+
+lemma infsum_reindex_bij_betw:
+ assumes "bij_betw g A B"
+ shows "infsum (\<lambda>x. f (g x)) A = infsum f B"
+proof -
+ have \<open>infsum (\<lambda>x. f (g x)) A = infsum f (g ` A)\<close>
+ by (metis (mono_tags, lifting) assms bij_betw_imp_inj_on infsum_cong infsum_reindex o_def)
+ also have \<open>\<dots> = infsum f B\<close>
+ using assms bij_betw_imp_surj_on by blast
+ finally show ?thesis .
+qed
lemma sum_uniformity:
assumes plus_cont: \<open>uniformly_continuous_on UNIV (\<lambda>(x::'b::{uniform_space,comm_monoid_add},y). x+y)\<close>
@@ -1152,7 +1233,7 @@
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
+ unfolding FB_def eventually_finite_subsets_at_top unfolding prod.case 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]
@@ -1180,19 +1261,23 @@
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))
+ unfolding FMB_def eventually_finite_subsets_at_top
+ by (intro exI[of _ "Sigma M Ha"])
+ (use Ha_fin that(2,3) in \<open>fastforce intro!: finite_SigmaI\<close>)
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 (meson Sigma_mono dual_order.refl order_trans)
+ proof (rule exI[of _ G], safe)
+ fix Y assume Y: "finite Y" "G \<subseteq> Y" "Y \<subseteq> Sigma M B"
+ have "Y \<subseteq> Sigma A B"
+ using Y \<open>M \<subseteq> A\<close> by blast
+ thus "D (\<Sum>(a,b)\<in>Y. f (a, b), a)"
+ using G_sum[of Y] Y by auto
+ qed (use \<open>finite G\<close> \<open>G \<subseteq> Sigma A B\<close> that in auto)
ultimately have \<open>\<forall>\<^sub>F x in FMB. E (sum b M, a)\<close>
- by (smt (verit, best) DDE' eventually_elim2)
+ by eventually_elim (use DDE' in auto)
then show \<open>E (sum b M, a)\<close>
- apply (rule eventually_const[THEN iffD1, rotated])
- using FMB_def by force
+ by (rule eventually_const[THEN iffD1, rotated]) (force simp: FMB_def)
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>
@@ -1277,7 +1362,8 @@
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)
+ using assms
+ by (subst infsum_Sigma'_banach) auto
lemma infsum_swap:
fixes A :: "'a set" and B :: "'b set"
@@ -1302,8 +1388,7 @@
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 -
+ finally show ?thesis .
qed
lemma infsum_swap_banach:
@@ -1326,11 +1411,10 @@
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 -
+ finally show ?thesis .
qed
-lemma infsum_0D:
+lemma nonneg_infsum_le_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"
@@ -1340,34 +1424,31 @@
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
+ by (rule summable_on_cofin_subset) (use assms in auto)
+ have pos: \<open>infsum f (A - {x}) \<ge> 0\<close>
+ by (rule infsum_nonneg) (use nneg in 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)
+ by (subst infsum_Un_disjoint[symmetric]) (use assms ex in \<open>auto simp: insert_absorb\<close>)
also have \<open>\<dots> \<ge> infsum f {x}\<close> (is \<open>_ \<ge> \<dots>\<close>)
- using pos apply (rule add_increasing) by simp
+ using pos by (rule add_increasing) simp
also have \<open>\<dots> = f x\<close> (is \<open>_ = \<dots>\<close>)
- apply (subst infsum_finite) by auto
+ by (subst infsum_finite) 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:
+lemma nonneg_has_sum_le_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)
+ by (metis assms(1) assms(2) assms(4) infsumI nonneg_infsum_le_0D summable_on_def nneg)
lemma has_sum_cmult_left:
fixes f :: "'a \<Rightarrow> 'b :: {topological_semigroup_mult, semiring_0}"
@@ -1563,8 +1644,7 @@
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 -
+ finally show ?thesis .
qed
then show False
by (meson linordered_field_no_ub not_less)
@@ -1596,13 +1676,548 @@
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)
+lemma has_sum_le_finite_sums:
+ fixes a :: \<open>'a::{comm_monoid_add,topological_space,linorder_topology}\<close>
+ assumes \<open>has_sum f A a\<close>
+ assumes \<open>\<And>F. finite F \<Longrightarrow> F \<subseteq> A \<Longrightarrow> sum f F \<le> b\<close>
+ shows \<open>a \<le> b\<close>
+proof -
+ from assms(1)
+ have 1: \<open>(sum f \<longlongrightarrow> a) (finite_subsets_at_top A)\<close>
+ unfolding has_sum_def .
+ from assms(2)
+ have 2: \<open>\<forall>\<^sub>F F in finite_subsets_at_top A. sum f F \<le> b\<close>
+ by (rule_tac eventually_finite_subsets_at_top_weakI)
+ show \<open>a \<le> b\<close>
+ using _ _ 1 2
+ apply (rule tendsto_le[where f=\<open>\<lambda>_. b\<close>])
+ by auto
+qed
+
+lemma infsum_le_finite_sums:
+ fixes b :: \<open>'a::{comm_monoid_add,topological_space,linorder_topology}\<close>
+ assumes \<open>f summable_on A\<close>
+ assumes \<open>\<And>F. finite F \<Longrightarrow> F \<subseteq> A \<Longrightarrow> sum f F \<le> b\<close>
+ shows \<open>infsum f A \<le> b\<close>
+ by (meson assms(1) assms(2) has_sum_infsum has_sum_le_finite_sums)
+
+
+lemma summable_on_scaleR_left [intro]:
+ fixes c :: \<open>'a :: real_normed_vector\<close>
+ assumes "c \<noteq> 0 \<Longrightarrow> f summable_on A"
+ shows "(\<lambda>x. f x *\<^sub>R c) summable_on A"
+ apply (cases \<open>c \<noteq> 0\<close>)
+ apply (subst asm_rl[of \<open>(\<lambda>x. f x *\<^sub>R c) = (\<lambda>y. y *\<^sub>R c) o f\<close>], simp add: o_def)
+ apply (rule summable_on_comm_additive)
+ using assms by (auto simp add: scaleR_left.additive_axioms)
+
+
+lemma summable_on_scaleR_right [intro]:
+ fixes f :: \<open>'a \<Rightarrow> 'b :: real_normed_vector\<close>
+ assumes "c \<noteq> 0 \<Longrightarrow> f summable_on A"
+ shows "(\<lambda>x. c *\<^sub>R f x) summable_on A"
+ apply (cases \<open>c \<noteq> 0\<close>)
+ apply (subst asm_rl[of \<open>(\<lambda>x. c *\<^sub>R f x) = (\<lambda>y. c *\<^sub>R y) o f\<close>], simp add: o_def)
+ apply (rule summable_on_comm_additive)
+ using assms by (auto simp add: scaleR_right.additive_axioms)
+
+lemma infsum_scaleR_left:
+ fixes c :: \<open>'a :: real_normed_vector\<close>
+ assumes "c \<noteq> 0 \<Longrightarrow> f summable_on A"
+ shows "infsum (\<lambda>x. f x *\<^sub>R c) A = infsum f A *\<^sub>R c"
+ apply (cases \<open>c \<noteq> 0\<close>)
+ apply (subst asm_rl[of \<open>(\<lambda>x. f x *\<^sub>R c) = (\<lambda>y. y *\<^sub>R c) o f\<close>], simp add: o_def)
+ apply (rule infsum_comm_additive)
+ using assms by (auto simp add: scaleR_left.additive_axioms)
+
+lemma infsum_scaleR_right:
+ fixes f :: \<open>'a \<Rightarrow> 'b :: real_normed_vector\<close>
+ shows "infsum (\<lambda>x. c *\<^sub>R f x) A = c *\<^sub>R infsum f A"
+proof -
+ consider (summable) \<open>f summable_on A\<close> | (c0) \<open>c = 0\<close> | (not_summable) \<open>\<not> f summable_on A\<close> \<open>c \<noteq> 0\<close>
+ by auto
+ then show ?thesis
+ proof cases
+ case summable
+ then show ?thesis
+ apply (subst asm_rl[of \<open>(\<lambda>x. c *\<^sub>R f x) = (\<lambda>y. c *\<^sub>R y) o f\<close>], simp add: o_def)
+ apply (rule infsum_comm_additive)
+ using summable by (auto simp add: scaleR_right.additive_axioms)
+ next
+ case c0
+ then show ?thesis by auto
+ next
+ case not_summable
+ have \<open>\<not> (\<lambda>x. c *\<^sub>R f x) summable_on A\<close>
+ proof (rule notI)
+ assume \<open>(\<lambda>x. c *\<^sub>R f x) summable_on A\<close>
+ then have \<open>(\<lambda>x. inverse c *\<^sub>R c *\<^sub>R f x) summable_on A\<close>
+ using summable_on_scaleR_right by blast
+ then have \<open>f summable_on A\<close>
+ using not_summable by auto
+ with not_summable show False
+ by simp
+ qed
+ then show ?thesis
+ by (simp add: infsum_not_exists not_summable(1))
+ qed
+qed
+
+
+lemma infsum_Un_Int:
+ fixes f :: "'a \<Rightarrow> 'b::{topological_ab_group_add, t2_space}"
+ assumes [simp]: "f summable_on A - B" "f summable_on B - A" \<open>f summable_on A \<inter> B\<close>
+ shows "infsum f (A \<union> B) = infsum f A + infsum f B - infsum f (A \<inter> B)"
+proof -
+ have [simp]: \<open>f summable_on A\<close>
+ apply (subst asm_rl[of \<open>A = (A-B) \<union> (A\<inter>B)\<close>]) apply auto[1]
+ apply (rule summable_on_Un_disjoint)
+ by auto
+ have \<open>infsum f (A \<union> B) = infsum f A + infsum f (B - A)\<close>
+ apply (subst infsum_Un_disjoint[symmetric])
+ by auto
+ moreover have \<open>infsum f (B - A \<union> A \<inter> B) = infsum f (B - A) + infsum f (A \<inter> B)\<close>
+ by (rule infsum_Un_disjoint) auto
+ moreover have "B - A \<union> A \<inter> B = B"
+ by blast
+ ultimately show ?thesis
+ by auto
+qed
+
+lemma inj_combinator':
+ assumes "x \<notin> F"
+ shows \<open>inj_on (\<lambda>(g, y). g(x := y)) (Pi\<^sub>E F B \<times> B x)\<close>
+proof -
+ have "inj_on ((\<lambda>(y, g). g(x := y)) \<circ> prod.swap) (Pi\<^sub>E F B \<times> B x)"
+ using inj_combinator[of x F B] assms by (intro comp_inj_on) (auto simp: product_swap)
+ thus ?thesis
+ by (simp add: o_def)
+qed
+
+lemma infsum_prod_PiE:
+ \<comment> \<open>See also \<open>infsum_prod_PiE_abs\<close> below with incomparable premises.\<close>
+ fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c :: {comm_monoid_mult, topological_semigroup_mult, division_ring, banach}"
+ assumes finite: "finite A"
+ assumes "\<And>x. x \<in> A \<Longrightarrow> f x summable_on B x"
+ assumes "(\<lambda>g. \<Prod>x\<in>A. f x (g x)) summable_on (PiE A B)"
+ shows "infsum (\<lambda>g. \<Prod>x\<in>A. f x (g x)) (PiE A B) = (\<Prod>x\<in>A. infsum (f x) (B x))"
+proof (use finite assms(2-) in induction)
+ case empty
+ then show ?case
+ by auto
+next
+ case (insert x F)
+ have pi: \<open>Pi\<^sub>E (insert x F) B = (\<lambda>(g,y). g(x:=y)) ` (Pi\<^sub>E F B \<times> B x)\<close>
+ unfolding PiE_insert_eq
+ by (subst swap_product [symmetric]) (simp add: image_image case_prod_unfold)
+ have prod: \<open>(\<Prod>x'\<in>F. f x' ((p(x:=y)) x')) = (\<Prod>x'\<in>F. f x' (p x'))\<close> for p y
+ by (rule prod.cong) (use insert.hyps in auto)
+ have inj: \<open>inj_on (\<lambda>(g, y). g(x := y)) (Pi\<^sub>E F B \<times> B x)\<close>
+ using \<open>x \<notin> F\<close> by (rule inj_combinator')
+
+ have summable1: \<open>(\<lambda>g. \<Prod>x\<in>insert x F. f x (g x)) summable_on Pi\<^sub>E (insert x F) B\<close>
+ using insert.prems(2) .
+ also have \<open>Pi\<^sub>E (insert x F) B = (\<lambda>(g,y). g(x:=y)) ` (Pi\<^sub>E F B \<times> B x)\<close>
+ by (simp only: pi)
+ also have "(\<lambda>g. \<Prod>x\<in>insert x F. f x (g x)) summable_on \<dots> \<longleftrightarrow>
+ ((\<lambda>g. \<Prod>x\<in>insert x F. f x (g x)) \<circ> (\<lambda>(g,y). g(x:=y))) summable_on (Pi\<^sub>E F B \<times> B x)"
+ using inj by (rule summable_on_reindex)
+ also have "(\<Prod>z\<in>F. f z ((g(x := y)) z)) = (\<Prod>z\<in>F. f z (g z))" for g y
+ using insert.hyps by (intro prod.cong) auto
+ hence "((\<lambda>g. \<Prod>x\<in>insert x F. f x (g x)) \<circ> (\<lambda>(g,y). g(x:=y))) =
+ (\<lambda>(p, y). f x y * (\<Prod>x'\<in>F. f x' (p x')))"
+ using insert.hyps by (auto simp: fun_eq_iff cong: prod.cong_simp)
+ finally have summable2: \<open>(\<lambda>(p, y). f x y * (\<Prod>x'\<in>F. f x' (p x'))) summable_on Pi\<^sub>E F B \<times> B x\<close> .
+
+ then have \<open>(\<lambda>p. \<Sum>\<^sub>\<infinity>y\<in>B x. f x y * (\<Prod>x'\<in>F. f x' (p x'))) summable_on Pi\<^sub>E F B\<close>
+ by (rule summable_on_Sigma_banach)
+ then have \<open>(\<lambda>p. (\<Sum>\<^sub>\<infinity>y\<in>B x. f x y) * (\<Prod>x'\<in>F. f x' (p x'))) summable_on Pi\<^sub>E F B\<close>
+ apply (subst infsum_cmult_left[symmetric])
+ using insert.prems(1) by blast
+ then have summable3: \<open>(\<lambda>p. (\<Prod>x'\<in>F. f x' (p x'))) summable_on Pi\<^sub>E F B\<close> if \<open>(\<Sum>\<^sub>\<infinity>y\<in>B x. f x y) \<noteq> 0\<close>
+ apply (subst (asm) summable_on_cmult_right')
+ using that by auto
+
+ have \<open>(\<Sum>\<^sub>\<infinity>g\<in>Pi\<^sub>E (insert x F) B. \<Prod>x\<in>insert x F. f x (g x))
+ = (\<Sum>\<^sub>\<infinity>(p,y)\<in>Pi\<^sub>E F B \<times> B x. \<Prod>x'\<in>insert x F. f x' ((p(x:=y)) x'))\<close>
+ apply (subst pi)
+ apply (subst infsum_reindex)
+ using inj by (auto simp: o_def case_prod_unfold)
+ also have \<open>\<dots> = (\<Sum>\<^sub>\<infinity>(p, y)\<in>Pi\<^sub>E F B \<times> B x. f x y * (\<Prod>x'\<in>F. f x' ((p(x:=y)) x')))\<close>
+ apply (subst prod.insert)
+ using insert by auto
+ also have \<open>\<dots> = (\<Sum>\<^sub>\<infinity>(p, y)\<in>Pi\<^sub>E F B \<times> B x. f x y * (\<Prod>x'\<in>F. f x' (p x')))\<close>
+ apply (subst prod) by rule
+ also have \<open>\<dots> = (\<Sum>\<^sub>\<infinity>p\<in>Pi\<^sub>E F B. \<Sum>\<^sub>\<infinity>y\<in>B x. f x y * (\<Prod>x'\<in>F. f x' (p x')))\<close>
+ apply (subst infsum_Sigma_banach[symmetric])
+ using summable2 apply blast
+ by fastforce
+ also have \<open>\<dots> = (\<Sum>\<^sub>\<infinity>y\<in>B x. f x y) * (\<Sum>\<^sub>\<infinity>p\<in>Pi\<^sub>E F B. \<Prod>x'\<in>F. f x' (p x'))\<close>
+ apply (subst infsum_cmult_left')
+ apply (subst infsum_cmult_right')
+ by (rule refl)
+ also have \<open>\<dots> = (\<Prod>x\<in>insert x F. infsum (f x) (B x))\<close>
+ apply (subst prod.insert)
+ using \<open>finite F\<close> \<open>x \<notin> F\<close> apply auto[2]
+ apply (cases \<open>infsum (f x) (B x) = 0\<close>)
+ apply simp
+ apply (subst insert.IH)
+ apply (simp add: insert.prems(1))
+ apply (rule summable3)
+ by auto
+ finally show ?case
+ by simp
+qed
+
+lemma infsum_prod_PiE_abs:
+ \<comment> \<open>See also @{thm [source] infsum_prod_PiE} above with incomparable premises.\<close>
+ fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c :: {banach, real_normed_div_algebra, comm_semiring_1}"
+ assumes finite: "finite A"
+ assumes "\<And>x. x \<in> A \<Longrightarrow> f x abs_summable_on B x"
+ shows "infsum (\<lambda>g. \<Prod>x\<in>A. f x (g x)) (PiE A B) = (\<Prod>x\<in>A. infsum (f x) (B x))"
+proof (use finite assms(2) in induction)
+ case empty
+ then show ?case
+ by auto
+next
+ case (insert x F)
+
+ have pi: \<open>Pi\<^sub>E (insert x F) B = (\<lambda>(g,y). g(x:=y)) ` (Pi\<^sub>E F B \<times> B x)\<close> for x F and B :: "'a \<Rightarrow> 'b set"
+ unfolding PiE_insert_eq
+ by (subst swap_product [symmetric]) (simp add: image_image case_prod_unfold)
+ have prod: \<open>(\<Prod>x'\<in>F. f x' ((p(x:=y)) x')) = (\<Prod>x'\<in>F. f x' (p x'))\<close> for p y
+ by (rule prod.cong) (use insert.hyps in auto)
+ have inj: \<open>inj_on (\<lambda>(g, y). g(x := y)) (Pi\<^sub>E F B \<times> B x)\<close>
+ using \<open>x \<notin> F\<close> by (rule inj_combinator')
+
+ define s where \<open>s x = infsum (\<lambda>y. norm (f x y)) (B x)\<close> for x
+
+ have *: \<open>(\<Sum>p\<in>P. norm (\<Prod>x\<in>F. f x (p x))) \<le> prod s F\<close>
+ if P: \<open>P \<subseteq> Pi\<^sub>E F B\<close> and [simp]: \<open>finite P\<close> \<open>finite F\<close>
+ and sum: \<open>\<And>x. x \<in> F \<Longrightarrow> f x abs_summable_on B x\<close> for P F
+ proof -
+ define B' where \<open>B' x = {p x| p. p\<in>P}\<close> for x
+ have [simp]: \<open>finite (B' x)\<close> for x
+ using that by (auto simp: B'_def)
+ have [simp]: \<open>finite (Pi\<^sub>E F B')\<close>
+ by (simp add: finite_PiE)
+ have [simp]: \<open>P \<subseteq> Pi\<^sub>E F B'\<close>
+ using that by (auto simp: B'_def)
+ have B'B: \<open>B' x \<subseteq> B x\<close> if \<open>x \<in> F\<close> for x
+ unfolding B'_def using P that
+ by auto
+ have s_bound: \<open>(\<Sum>y\<in>B' x. norm (f x y)) \<le> s x\<close> if \<open>x \<in> F\<close> for x
+ apply (simp_all add: s_def flip: infsum_finite)
+ apply (rule infsum_mono_neutral)
+ using that sum B'B by auto
+ have \<open>(\<Sum>p\<in>P. norm (\<Prod>x\<in>F. f x (p x))) \<le> (\<Sum>p\<in>Pi\<^sub>E F B'. norm (\<Prod>x\<in>F. f x (p x)))\<close>
+ apply (rule sum_mono2)
+ by auto
+ also have \<open>\<dots> = (\<Sum>p\<in>Pi\<^sub>E F B'. \<Prod>x\<in>F. norm (f x (p x)))\<close>
+ apply (subst prod_norm[symmetric])
+ by simp
+ also have \<open>\<dots> = (\<Prod>x\<in>F. \<Sum>y\<in>B' x. norm (f x y))\<close>
+ proof (use \<open>finite F\<close> in induction)
+ case empty
+ then show ?case by simp
+ next
+ case (insert x F)
+ have aux: \<open>a = b \<Longrightarrow> c * a = c * b\<close> for a b c :: real
+ by auto
+ have inj: \<open>inj_on (\<lambda>(g, y). g(x := y)) (Pi\<^sub>E F B' \<times> B' x)\<close>
+ by (rule inj_combinator') (use insert.hyps in auto)
+ have \<open>(\<Sum>p\<in>Pi\<^sub>E (insert x F) B'. \<Prod>x\<in>insert x F. norm (f x (p x)))
+ = (\<Sum>(p,y)\<in>Pi\<^sub>E F B' \<times> B' x. \<Prod>x'\<in>insert x F. norm (f x' ((p(x := y)) x')))\<close>
+ apply (subst pi)
+ apply (subst sum.reindex)
+ using inj by (auto simp: case_prod_unfold)
+ also have \<open>\<dots> = (\<Sum>(p,y)\<in>Pi\<^sub>E F B' \<times> B' x. norm (f x y) * (\<Prod>x'\<in>F. norm (f x' ((p(x := y)) x'))))\<close>
+ apply (subst prod.insert)
+ using insert.hyps by (auto simp: case_prod_unfold)
+ also have \<open>\<dots> = (\<Sum>(p, y)\<in>Pi\<^sub>E F B' \<times> B' x. norm (f x y) * (\<Prod>x'\<in>F. norm (f x' (p x'))))\<close>
+ apply (rule sum.cong)
+ apply blast
+ unfolding case_prod_unfold
+ apply (rule aux)
+ apply (rule prod.cong)
+ using insert.hyps(2) by auto
+ also have \<open>\<dots> = (\<Sum>y\<in>B' x. norm (f x y)) * (\<Sum>p\<in>Pi\<^sub>E F B'. \<Prod>x'\<in>F. norm (f x' (p x')))\<close>
+ apply (subst sum_product)
+ apply (subst sum.swap)
+ apply (subst sum.cartesian_product)
+ by simp
+ also have \<open>\<dots> = (\<Sum>y\<in>B' x. norm (f x y)) * (\<Prod>x\<in>F. \<Sum>y\<in>B' x. norm (f x y))\<close>
+ by (simp add: insert.IH)
+ also have \<open>\<dots> = (\<Prod>x\<in>insert x F. \<Sum>y\<in>B' x. norm (f x y))\<close>
+ using insert.hyps(1) insert.hyps(2) by force
+ finally show ?case .
+ qed
+ also have \<open>\<dots> = (\<Prod>x\<in>F. \<Sum>\<^sub>\<infinity>y\<in>B' x. norm (f x y))\<close>
+ by auto
+ also have \<open>\<dots> \<le> (\<Prod>x\<in>F. s x)\<close>
+ apply (rule prod_mono)
+ apply auto
+ apply (simp add: sum_nonneg)
+ using s_bound by presburger
+ finally show ?thesis .
+ qed
+ have \<open>(\<lambda>g. \<Prod>x\<in>insert x F. f x (g x)) abs_summable_on Pi\<^sub>E (insert x F) B\<close>
+ apply (rule nonneg_bdd_above_summable_on)
+ apply (simp; fail)
+ apply (rule bdd_aboveI[where M=\<open>\<Prod>x'\<in>insert x F. s x'\<close>])
+ using * insert.hyps insert.prems by blast
+
+ also have \<open>Pi\<^sub>E (insert x F) B = (\<lambda>(g,y). g(x:=y)) ` (Pi\<^sub>E F B \<times> B x)\<close>
+ by (simp only: pi)
+ also have "(\<lambda>g. \<Prod>x\<in>insert x F. f x (g x)) abs_summable_on \<dots> \<longleftrightarrow>
+ ((\<lambda>g. \<Prod>x\<in>insert x F. f x (g x)) \<circ> (\<lambda>(g,y). g(x:=y))) abs_summable_on (Pi\<^sub>E F B \<times> B x)"
+ using inj by (subst summable_on_reindex) (auto simp: o_def)
+ also have "(\<Prod>z\<in>F. f z ((g(x := y)) z)) = (\<Prod>z\<in>F. f z (g z))" for g y
+ using insert.hyps by (intro prod.cong) auto
+ hence "((\<lambda>g. \<Prod>x\<in>insert x F. f x (g x)) \<circ> (\<lambda>(g,y). g(x:=y))) =
+ (\<lambda>(p, y). f x y * (\<Prod>x'\<in>F. f x' (p x')))"
+ using insert.hyps by (auto simp: fun_eq_iff cong: prod.cong_simp)
+ finally have summable2: \<open>(\<lambda>(p, y). f x y * (\<Prod>x'\<in>F. f x' (p x'))) abs_summable_on Pi\<^sub>E F B \<times> B x\<close> .
+
+ have \<open>(\<Sum>\<^sub>\<infinity>g\<in>Pi\<^sub>E (insert x F) B. \<Prod>x\<in>insert x F. f x (g x))
+ = (\<Sum>\<^sub>\<infinity>(p,y)\<in>Pi\<^sub>E F B \<times> B x. \<Prod>x'\<in>insert x F. f x' ((p(x:=y)) x'))\<close>
+ apply (subst pi)
+ apply (subst infsum_reindex)
+ using inj by (auto simp: o_def case_prod_unfold)
+ also have \<open>\<dots> = (\<Sum>\<^sub>\<infinity>(p, y)\<in>Pi\<^sub>E F B \<times> B x. f x y * (\<Prod>x'\<in>F. f x' ((p(x:=y)) x')))\<close>
+ apply (subst prod.insert)
+ using insert by auto
+ also have \<open>\<dots> = (\<Sum>\<^sub>\<infinity>(p, y)\<in>Pi\<^sub>E F B \<times> B x. f x y * (\<Prod>x'\<in>F. f x' (p x')))\<close>
+ apply (subst prod) by rule
+ also have \<open>\<dots> = (\<Sum>\<^sub>\<infinity>p\<in>Pi\<^sub>E F B. \<Sum>\<^sub>\<infinity>y\<in>B x. f x y * (\<Prod>x'\<in>F. f x' (p x')))\<close>
+ apply (subst infsum_Sigma_banach[symmetric])
+ using summable2 abs_summable_summable apply blast
+ by fastforce
+ also have \<open>\<dots> = (\<Sum>\<^sub>\<infinity>y\<in>B x. f x y) * (\<Sum>\<^sub>\<infinity>p\<in>Pi\<^sub>E F B. \<Prod>x'\<in>F. f x' (p x'))\<close>
+ apply (subst infsum_cmult_left')
+ apply (subst infsum_cmult_right')
+ by (rule refl)
+ also have \<open>\<dots> = (\<Prod>x\<in>insert x F. infsum (f x) (B x))\<close>
+ apply (subst prod.insert)
+ using \<open>finite F\<close> \<open>x \<notin> F\<close> apply auto[2]
+ apply (cases \<open>infsum (f x) (B x) = 0\<close>)
+ apply (simp; fail)
+ apply (subst insert.IH)
+ apply (auto simp add: insert.prems(1))
+ done
+ finally show ?case
+ by simp
+qed
+
+
+
+subsection \<open>Absolute convergence\<close>
+
+lemma abs_summable_countable:
+ assumes \<open>f abs_summable_on A\<close>
+ shows \<open>countable {x\<in>A. f x \<noteq> 0}\<close>
+proof -
+ have fin: \<open>finite {x\<in>A. norm (f x) \<ge> t}\<close> if \<open>t > 0\<close> for t
+ proof (rule ccontr)
+ assume *: \<open>infinite {x \<in> A. t \<le> norm (f x)}\<close>
+ have \<open>infsum (\<lambda>x. norm (f x)) A \<ge> b\<close> for b
+ proof -
+ obtain b' where b': \<open>of_nat b' \<ge> b / t\<close>
+ by (meson real_arch_simple)
+ from *
+ obtain F where cardF: \<open>card F \<ge> b'\<close> and \<open>finite F\<close> and F: \<open>F \<subseteq> {x \<in> A. t \<le> norm (f x)}\<close>
+ by (meson finite_if_finite_subsets_card_bdd nle_le)
+ have \<open>b \<le> of_nat b' * t\<close>
+ using b' \<open>t > 0\<close> by (simp add: field_simps split: if_splits)
+ also have \<open>\<dots> \<le> of_nat (card F) * t\<close>
+ by (simp add: cardF that)
+ also have \<open>\<dots> = sum (\<lambda>x. t) F\<close>
+ by simp
+ also have \<open>\<dots> \<le> sum (\<lambda>x. norm (f x)) F\<close>
+ by (metis (mono_tags, lifting) F in_mono mem_Collect_eq sum_mono)
+ also have \<open>\<dots> = infsum (\<lambda>x. norm (f x)) F\<close>
+ using \<open>finite F\<close> by (rule infsum_finite[symmetric])
+ also have \<open>\<dots> \<le> infsum (\<lambda>x. norm (f x)) A\<close>
+ by (rule infsum_mono_neutral) (use \<open>finite F\<close> assms F in auto)
+ finally show ?thesis .
+ qed
+ then show False
+ by (meson gt_ex linorder_not_less)
+ qed
+ have \<open>countable (\<Union>i\<in>{1..}. {x\<in>A. norm (f x) \<ge> 1/of_nat i})\<close>
+ by (rule countable_UN) (use fin in \<open>auto intro!: countable_finite\<close>)
+ also have \<open>\<dots> = {x\<in>A. f x \<noteq> 0}\<close>
+ proof safe
+ fix x assume x: "x \<in> A" "f x \<noteq> 0"
+ define i where "i = max 1 (nat (ceiling (1 / norm (f x))))"
+ have "i \<ge> 1"
+ by (simp add: i_def)
+ moreover have "real i \<ge> 1 / norm (f x)"
+ unfolding i_def by linarith
+ hence "1 / real i \<le> norm (f x)" using \<open>f x \<noteq> 0\<close>
+ by (auto simp: divide_simps mult_ac)
+ ultimately show "x \<in> (\<Union>i\<in>{1..}. {x \<in> A. 1 / real i \<le> norm (f x)})"
+ using \<open>x \<in> A\<close> by auto
+ qed auto
+ finally show ?thesis .
+qed
+
+(* Logically belongs in the section about reals, but needed as a dependency here *)
+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
+
+lemma abs_summable_on_Sigma_iff:
+ shows "f abs_summable_on Sigma A B \<longleftrightarrow>
+ (\<forall>x\<in>A. (\<lambda>y. f (x, y)) abs_summable_on B x) \<and>
+ ((\<lambda>x. infsum (\<lambda>y. norm (f (x, y))) (B x)) abs_summable_on A)"
+proof (intro iffI conjI ballI)
+ assume asm: \<open>f abs_summable_on Sigma A B\<close>
+ then have \<open>(\<lambda>x. infsum (\<lambda>y. norm (f (x,y))) (B x)) summable_on A\<close>
+ apply (rule_tac summable_on_Sigma_banach)
+ by (auto simp: case_prod_unfold)
+ then show \<open>(\<lambda>x. \<Sum>\<^sub>\<infinity>y\<in>B x. norm (f (x, y))) abs_summable_on A\<close>
+ using summable_on_iff_abs_summable_on_real by force
+
+ show \<open>(\<lambda>y. f (x, y)) abs_summable_on B x\<close> if \<open>x \<in> A\<close> for x
+ proof -
+ from asm have \<open>f abs_summable_on Pair x ` B x\<close>
+ apply (rule summable_on_subset_banach)
+ using that by auto
+ then show ?thesis
+ apply (subst (asm) summable_on_reindex)
+ by (auto simp: o_def inj_on_def)
+ qed
+next
+ assume asm: \<open>(\<forall>x\<in>A. (\<lambda>xa. f (x, xa)) abs_summable_on B x) \<and>
+ (\<lambda>x. \<Sum>\<^sub>\<infinity>y\<in>B x. norm (f (x, y))) abs_summable_on A\<close>
+ have \<open>(\<Sum>xy\<in>F. norm (f xy)) \<le> (\<Sum>\<^sub>\<infinity>x\<in>A. \<Sum>\<^sub>\<infinity>y\<in>B x. norm (f (x, y)))\<close>
+ if \<open>F \<subseteq> Sigma A B\<close> and [simp]: \<open>finite F\<close> for F
+ proof -
+ have [simp]: \<open>(SIGMA x:fst ` F. {y. (x, y) \<in> F}) = F\<close>
+ by (auto intro!: set_eqI simp add: Domain.DomainI fst_eq_Domain)
+ have [simp]: \<open>finite {y. (x, y) \<in> F}\<close> for x
+ by (metis \<open>finite F\<close> Range.intros finite_Range finite_subset mem_Collect_eq subsetI)
+ have \<open>(\<Sum>xy\<in>F. norm (f xy)) = (\<Sum>x\<in>fst ` F. \<Sum>y\<in>{y. (x,y)\<in>F}. norm (f (x,y)))\<close>
+ apply (subst sum.Sigma)
+ by auto
+ also have \<open>\<dots> = (\<Sum>\<^sub>\<infinity>x\<in>fst ` F. \<Sum>\<^sub>\<infinity>y\<in>{y. (x,y)\<in>F}. norm (f (x,y)))\<close>
+ apply (subst infsum_finite)
+ by auto
+ also have \<open>\<dots> \<le> (\<Sum>\<^sub>\<infinity>x\<in>fst ` F. \<Sum>\<^sub>\<infinity>y\<in>B x. norm (f (x,y)))\<close>
+ apply (rule infsum_mono)
+ apply (simp; fail)
+ apply (simp; fail)
+ apply (rule infsum_mono_neutral)
+ using asm that(1) by auto
+ also have \<open>\<dots> \<le> (\<Sum>\<^sub>\<infinity>x\<in>A. \<Sum>\<^sub>\<infinity>y\<in>B x. norm (f (x,y)))\<close>
+ by (rule infsum_mono_neutral) (use asm that(1) in \<open>auto simp add: infsum_nonneg\<close>)
+ finally show ?thesis .
+ qed
+ then show \<open>f abs_summable_on Sigma A B\<close>
+ by (intro nonneg_bdd_above_summable_on) (auto simp: bdd_above_def)
+qed
+
+lemma abs_summable_on_comparison_test:
+ assumes "g abs_summable_on A"
+ assumes "\<And>x. x \<in> A \<Longrightarrow> norm (f x) \<le> norm (g x)"
+ shows "f abs_summable_on A"
+proof (rule nonneg_bdd_above_summable_on)
+ show "bdd_above (sum (\<lambda>x. norm (f x)) ` {F. F \<subseteq> A \<and> finite F})"
+ proof (rule bdd_aboveI2)
+ fix F assume F: "F \<in> {F. F \<subseteq> A \<and> finite F}"
+ have \<open>sum (\<lambda>x. norm (f x)) F \<le> sum (\<lambda>x. norm (g x)) F\<close>
+ using assms F by (intro sum_mono) auto
+ also have \<open>\<dots> = infsum (\<lambda>x. norm (g x)) F\<close>
+ using F by simp
+ also have \<open>\<dots> \<le> infsum (\<lambda>x. norm (g x)) A\<close>
+ proof (rule infsum_mono_neutral)
+ show "g abs_summable_on F"
+ by (rule summable_on_subset_banach[OF assms(1)]) (use F in auto)
+ qed (use F assms in auto)
+ finally show "(\<Sum>x\<in>F. norm (f x)) \<le> (\<Sum>\<^sub>\<infinity>x\<in>A. norm (g x))" .
+ qed
+qed auto
+
+lemma abs_summable_iff_bdd_above:
+ fixes f :: \<open>'a \<Rightarrow> 'b::real_normed_vector\<close>
+ shows \<open>f abs_summable_on A \<longleftrightarrow> bdd_above (sum (\<lambda>x. norm (f x)) ` {F. F\<subseteq>A \<and> finite F})\<close>
+proof (rule iffI)
+ assume \<open>f abs_summable_on A\<close>
+ show \<open>bdd_above (sum (\<lambda>x. norm (f x)) ` {F. F \<subseteq> A \<and> finite F})\<close>
+ proof (rule bdd_aboveI2)
+ fix F assume F: "F \<in> {F. F \<subseteq> A \<and> finite F}"
+ show "(\<Sum>x\<in>F. norm (f x)) \<le> (\<Sum>\<^sub>\<infinity>x\<in>A. norm (f x))"
+ by (rule finite_sum_le_infsum) (use \<open>f abs_summable_on A\<close> F in auto)
+ qed
+next
+ assume \<open>bdd_above (sum (\<lambda>x. norm (f x)) ` {F. F\<subseteq>A \<and> finite F})\<close>
+ then show \<open>f abs_summable_on A\<close>
+ by (simp add: nonneg_bdd_above_summable_on)
+qed
+
+lemma abs_summable_product:
+ fixes x :: "'a \<Rightarrow> 'b::{real_normed_div_algebra,banach,second_countable_topology}"
+ assumes x2_sum: "(\<lambda>i. (x i) * (x i)) abs_summable_on A"
+ and y2_sum: "(\<lambda>i. (y i) * (y i)) abs_summable_on A"
+ shows "(\<lambda>i. x i * y i) abs_summable_on A"
+proof (rule nonneg_bdd_above_summable_on)
+ show "bdd_above (sum (\<lambda>xa. norm (x xa * y xa)) ` {F. F \<subseteq> A \<and> finite F})"
+ proof (rule bdd_aboveI2)
+ fix F assume F: \<open>F \<in> {F. F \<subseteq> A \<and> finite F}\<close>
+ then have r1: "finite F" and b4: "F \<subseteq> A"
+ by auto
+
+ have a1: "(\<Sum>\<^sub>\<infinity>i\<in>F. norm (x i * x i)) \<le> (\<Sum>\<^sub>\<infinity>i\<in>A. norm (x i * x i))"
+ apply (rule infsum_mono_neutral)
+ using b4 r1 x2_sum by auto
+
+ have "norm (x i * y i) \<le> norm (x i * x i) + norm (y i * y i)" for i
+ unfolding norm_mult by (smt mult_left_mono mult_nonneg_nonneg mult_right_mono norm_ge_zero)
+ hence "(\<Sum>i\<in>F. norm (x i * y i)) \<le> (\<Sum>i\<in>F. norm (x i * x i) + norm (y i * y i))"
+ by (simp add: sum_mono)
+ also have "\<dots> = (\<Sum>i\<in>F. norm (x i * x i)) + (\<Sum>i\<in>F. norm (y i * y i))"
+ by (simp add: sum.distrib)
+ also have "\<dots> = (\<Sum>\<^sub>\<infinity>i\<in>F. norm (x i * x i)) + (\<Sum>\<^sub>\<infinity>i\<in>F. norm (y i * y i))"
+ by (simp add: \<open>finite F\<close>)
+ also have "\<dots> \<le> (\<Sum>\<^sub>\<infinity>i\<in>A. norm (x i * x i)) + (\<Sum>\<^sub>\<infinity>i\<in>A. norm (y i * y i))"
+ using F assms
+ by (intro add_mono infsum_mono2) auto
+ finally show \<open>(\<Sum>xa\<in>F. norm (x xa * y xa)) \<le> (\<Sum>\<^sub>\<infinity>i\<in>A. norm (x i * x i)) + (\<Sum>\<^sub>\<infinity>i\<in>A. norm (y i * y i))\<close>
+ by simp
+ qed
+qed auto
+
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
+ by (rule nonneg_summable_on_complete) simp
lemma summable_on_enat[simp]: \<open>(f::_ \<Rightarrow> enat) summable_on S\<close>
- apply (rule pos_summable_on_complete) by simp
+ by (rule nonneg_summable_on_complete) simp
lemma has_sum_superconst_infinite_ennreal:
fixes f :: \<open>'a \<Rightarrow> ennreal\<close>
@@ -1629,8 +2244,7 @@
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 -
+ finally show ?thesis .
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
@@ -1657,19 +2271,20 @@
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 "0 < e2ennreal b"
+ using b' b
+ by (metis dual_order.refl enn2ereal_e2ennreal gr_zeroI order_less_le zero_ennreal.abs_eq)
+ hence *: \<open>infsum (e2ennreal o f) S = \<infinity>\<close>
+ using assms b'
+ by (intro infsum_superconst_infinite_ennreal[where b=b']) (auto intro!: e2ennreal_mono)
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)
+ using geqb b by (intro infsum_cong) (fastforce simp: enn2ereal_e2ennreal)
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 -
+ finally show ?thesis .
qed
lemma has_sum_superconst_infinite_ereal:
@@ -1704,7 +2319,7 @@
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)
+ by (metis assms i0_lb has_sum_infsum infsum_superconst_infinite_enat nonneg_summable_on_complete)
text \<open>This lemma helps to relate a real-valued infsum to a supremum over extended nonnegative reals.\<close>
@@ -1719,12 +2334,11 @@
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 (subst nonneg_infsum_complete, simp)
apply (rule SUP_cong, blast)
apply (subst sum_ennreal[symmetric])
using fnn by auto
- finally show ?thesis
- by -
+ finally show ?thesis .
qed
text \<open>This lemma helps to related a real-valued infsum to a supremum over extended reals.\<close>
@@ -1739,10 +2353,8 @@
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 -
+ by (subst nonneg_infsum_complete) (simp_all add: assms)
+ finally show ?thesis .
qed
@@ -1776,33 +2388,11 @@
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:
+lemma summable_countable_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
+ assumes \<open>f summable_on A\<close>
+ shows \<open>countable {x\<in>A. f x \<noteq> 0}\<close>
+ using abs_summable_countable assms summable_on_iff_abs_summable_on_real by blast
subsection \<open>Complex numbers\<close>
@@ -1854,7 +2444,7 @@
apply (rule summable_on_comm_additive[where f=Im, unfolded o_def])
using assms by (auto intro!: additive.intro)
-lemma infsum_0D_complex:
+lemma nonneg_infsum_le_0D_complex:
fixes f :: "'a \<Rightarrow> complex"
assumes "infsum f A \<le> 0"
and abs_sum: "f summable_on A"
@@ -1863,22 +2453,22 @@
shows "f x = 0"
proof -
have \<open>Im (f x) = 0\<close>
- apply (rule infsum_0D[where A=A])
+ apply (rule nonneg_infsum_le_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])
+ apply (rule nonneg_infsum_le_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:
+lemma nonneg_has_sum_le_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)
+ by (metis assms infsumI nonneg_infsum_le_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>
@@ -1929,14 +2519,16 @@
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))
+ proof (rule infsum_comm_additive[symmetric, unfolded o_def])
+ have "(\<lambda>z. Re (f z)) summable_on M"
+ using assms summable_on_Re by blast
+ also have "?this \<longleftrightarrow> f abs_summable_on M"
+ using fnn by (intro summable_on_cong) (auto simp: less_eq_complex_def cmod_def)
+ finally show \<dots> .
+ qed (auto simp: additive_def)
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
+ using fnn 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
@@ -1965,8 +2557,8 @@
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 nonneg_bdd_above_summable_on)
+ apply (simp add: n_def; fail)
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
@@ -1974,4 +2566,11 @@
using abs_summable_summable by blast
qed
+lemma summable_countable_complex:
+ fixes f :: \<open>'a \<Rightarrow> complex\<close>
+ assumes \<open>f summable_on A\<close>
+ shows \<open>countable {x\<in>A. f x \<noteq> 0}\<close>
+ using abs_summable_countable assms summable_on_iff_abs_summable_on_complex by blast
+
end
+