--- a/src/HOL/Analysis/Infinite_Sum.thy Sat Feb 25 17:35:48 2023 +0000
+++ b/src/HOL/Analysis/Infinite_Sum.thy Sun Feb 26 21:17:39 2023 +0000
@@ -787,17 +787,14 @@
by (subst (asm) sum.union_disjoint) (use that in \<open>auto simp: F0A_def\<close>)
qed
+ have "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>)+
+ then
show \<open>eventually E (?filter_fB \<times>\<^sub>F ?filter_fB)\<close>
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
+ using E'E'E by blast
qed
then obtain x where \<open>?filter_fB \<le> nhds x\<close>
@@ -816,8 +813,7 @@
assumes \<open>f summable_on A\<close>
assumes \<open>B \<subseteq> A\<close>
shows \<open>f summable_on B\<close>
- by (rule summable_on_subset_aux[OF _ _ assms])
- (auto simp: complete_def convergent_def dest!: Cauchy_convergent)
+ by (meson Cauchy_convergent UNIV_I assms complete_def convergent_def isUCont_plus summable_on_subset_aux)
lemma has_sum_empty[simp]: \<open>(f has_sum 0) {}\<close>
by (meson ex_in_conv has_sum_0)
@@ -866,7 +862,7 @@
assumes conv: \<open>\<And>a. a \<in> A \<Longrightarrow> f summable_on (B a)\<close>
assumes disj: \<open>\<And>a a'. a\<in>A \<Longrightarrow> a'\<in>A \<Longrightarrow> a\<noteq>a' \<Longrightarrow> B a \<inter> B a' = {}\<close>
shows \<open>sum (\<lambda>a. infsum f (B a)) A = infsum f (\<Union>a\<in>A. B a)\<close>
- by (metis (no_types, lifting) assms has_sum_infsum infsumI sum_has_sum[of A f B \<open>\<lambda>a. infsum f (B a)\<close>])
+ by (metis (no_types, lifting) assms has_sum_infsum infsumI sum_has_sum)
text \<open>The lemmas \<open>infsum_comm_additive_general\<close> and \<open>infsum_comm_additive\<close> (and variants) below both state that the infinite sum commutes with
a continuous additive function. \<open>infsum_comm_additive_general\<close> is stated more for more general type classes
@@ -959,16 +955,10 @@
by (metis \<open>F \<subseteq> A\<close> \<open>finite F\<close> eventually_finite_subsets_at_top)
next
fix a assume *: \<open>(SUP F\<in>{F. finite F \<and> F\<subseteq>A}. sum f F) < a\<close>
- have \<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)"
+ have "sum f F \<le> (SUP F\<in>{F. finite F \<and> F\<subseteq>A}. sum f F)" if \<open>F\<subseteq>A\<close> and \<open>finite F\<close> for 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)
+ by (metis (no_types, lifting) "*" eventually_finite_subsets_at_top_weakI order_le_less_trans)
qed
then show ?thesis
using has_sum_def by blast
@@ -1024,14 +1014,7 @@
assumes "(f has_sum S) A" "(f has_sum S') B" "A \<subseteq> B"
assumes "\<And>x. x \<in> B - A \<Longrightarrow> f x \<ge> 0"
shows "S \<le> S'"
-proof -
- have "(f has_sum (S' - S)) (B - A)"
- 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
+ by (metis add_0 add_right_mono assms diff_add_cancel has_sum_Diff has_sum_nonneg)
lemma infsum_mono2:
fixes f :: "'a \<Rightarrow> 'b::{topological_ab_group_add, ordered_comm_monoid_add,linorder_topology}"
@@ -1045,12 +1028,7 @@
assumes "(f has_sum S) A" "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 "(f has_sum S) A"
- by fact
- show "(f has_sum (sum f B)) B"
- by (rule has_sum_finite) fact+
-qed (use assms in auto)
+ by (meson assms has_sum_finite has_sum_mono2)
lemma finite_sum_le_infsum:
fixes f :: "'a \<Rightarrow> 'b::{topological_ab_group_add, ordered_comm_monoid_add,linorder_topology}"
@@ -1085,39 +1063,24 @@
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 assms has_sum_infsum has_sum_reindex infsumI infsum_def)
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 -
- have "inj_on g A"
- using assms bij_betw_imp_inj_on by blast
- then have \<open>(\<lambda>x. f (g x)) summable_on A \<longleftrightarrow> f summable_on g ` A\<close>
- by (metis (mono_tags, lifting) comp_apply summable_on_cong summable_on_reindex)
- also have \<open>\<dots> \<longleftrightarrow> f summable_on B\<close>
- using assms bij_betw_imp_surj_on by blast
- finally show ?thesis .
-qed
+ by (smt (verit) assms bij_betw_def o_apply summable_on_cong summable_on_reindex)
lemma infsum_reindex_bij_betw:
assumes "bij_betw g A B"
shows "infsum (\<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
+ by (metis (mono_tags, lifting) assms bij_betw_def infsum_cong infsum_reindex o_def)
lemma sum_uniformity:
assumes plus_cont: \<open>uniformly_continuous_on UNIV (\<lambda>(x::'b::{uniform_space,comm_monoid_add},y). x+y)\<close>
- assumes \<open>eventually E uniformity\<close>
+ assumes EE: \<open>eventually E uniformity\<close>
obtains D where \<open>eventually D uniformity\<close>
and \<open>\<And>M::'a set. \<And>f f' :: 'a \<Rightarrow> 'b. card M \<le> n \<and> (\<forall>m\<in>M. D (f m, f' m)) \<Longrightarrow> E (sum f M, sum f' M)\<close>
-proof (atomize_elim, insert \<open>eventually E uniformity\<close>, induction n arbitrary: E rule:nat_induct)
+proof (atomize_elim, insert EE, induction n arbitrary: E rule:nat_induct)
case 0
then show ?case
by (metis card_eq_0_iff equals0D le_zero_eq sum.infinite sum.not_neutral_contains_not_neutral uniformity_refl)
@@ -1169,8 +1132,7 @@
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
+ with \<open>eventually D uniformity\<close> show ?case
by auto
qed
@@ -1257,26 +1219,23 @@
using Ha_B \<open>M \<subseteq> A\<close> by auto
ultimately show ?thesis
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>)
+ by (metis (no_types, lifting) 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
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
+ using G_sum[of Y] Y using that(3) by fastforce
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 eventually_elim (use DDE' in auto)
then show \<open>E (sum b M, a)\<close>
- by (rule eventually_const[THEN iffD1, rotated]) (force simp: FMB_def)
+ 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)
+ by (metis (mono_tags, lifting) FA_def eventually_finite_subsets_at_top)
qed
then show ?thesis
by (simp add: FA_def has_sum_def)
@@ -1295,8 +1254,8 @@
from summableB have b: \<open>\<And>x. x\<in>A \<Longrightarrow> (f x has_sum infsum (f x) (B 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)
+ using plus_cont a b
+ by (smt (verit) has_sum_Sigma[where f=\<open>\<lambda>(x,y). f x y\<close>] has_sum_cong old.prod.case summable_on_def)
qed
lemma infsum_Sigma:
@@ -1354,8 +1313,7 @@
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>
- using assms
- by (subst infsum_Sigma'_banach) auto
+ using assms by (simp add: infsum_Sigma'_banach)
lemma infsum_swap:
fixes A :: "'a set" and B :: "'b set"
@@ -1440,31 +1398,14 @@
fixes f :: "'a \<Rightarrow> 'b :: {topological_semigroup_mult, semiring_0}"
assumes \<open>(f has_sum a) A\<close>
shows "((\<lambda>x. f x * c) has_sum (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. 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>
- by (metis (mono_tags) tendsto_cong eventually_finite_subsets_at_top_weakI sum_distrib_right)
- then show ?thesis
- using infsumI has_sum_def by blast
-qed
+ using assms tendsto_mult_right
+ by (force simp add: has_sum_def sum_distrib_right)
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>(f has_sum (infsum f A)) A\<close>
- by (simp add: assms)
- then show ?thesis
- by (auto intro!: infsumI has_sum_cmult_left)
-qed
+ using assms has_sum_cmult_left infsumI summable_iff_has_sum_infsum by fastforce
lemma summable_on_cmult_left:
fixes f :: "'a \<Rightarrow> 'b :: {t2_space, topological_semigroup_mult, semiring_0}"
@@ -1476,16 +1417,8 @@
fixes f :: "'a \<Rightarrow> 'b :: {topological_semigroup_mult, semiring_0}"
assumes \<open>(f has_sum a) A\<close>
shows "((\<lambda>x. c * f x) has_sum (c * a)) 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>
- by (metis (mono_tags, lifting) tendsto_cong eventually_finite_subsets_at_top_weakI sum_distrib_left)
- then show ?thesis
- using infsumI has_sum_def by blast
-qed
+ using assms tendsto_mult_left
+ by (force simp add: has_sum_def sum_distrib_left)
lemma infsum_cmult_right:
fixes f :: "'a \<Rightarrow> 'b :: {t2_space, topological_semigroup_mult, semiring_0}"
@@ -1512,24 +1445,14 @@
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)
+ by (smt (verit, del_insts) assms divide_inverse nonzero_divide_eq_eq summable_on_cong)
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
+ by (metis (no_types, lifting) assms left_inverse mult.assoc mult_1 summable_on_cmult_right summable_on_cong)
lemma infsum_cmult_left':
fixes f :: "'a \<Rightarrow> 'b :: {t2_space, topological_semigroup_mult, division_ring}"
@@ -2203,15 +2126,10 @@
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)))"
+ 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
+ by (metis (no_types, lifting) * MInfty_neq_ereal(2) PInfty_neq_ereal(2) SUP_cong abs_eq_infinity_cases ereal_SUP)
finally show ?thesis by simp
qed
@@ -2530,7 +2448,7 @@
assumes "eventually (\<lambda>x. x \<in> X) F" "g X \<le> F'"
shows "lift_filter g F \<le> F'"
unfolding lift_filter_def
- by (rule INF_lower2[of X _ g F', OF _ assms(2)]) (use assms(1) in auto)
+ by (metis INF_lower2 assms mem_Collect_eq)
definition lift_filter' :: "('a set \<Rightarrow> 'b set) \<Rightarrow> 'a filter \<Rightarrow> 'b filter" where
"lift_filter' f F = lift_filter (principal \<circ> f) F"
@@ -2649,13 +2567,10 @@
using P eventually_compose_filterlim eventually_uniformity_imp_nhds G by blast
ultimately have "eventually (\<lambda>n. (\<forall>x\<in>B n. P x) \<and> P (L, g n)) sequentially"
by eventually_elim auto
- then obtain n where n: "\<forall>x\<in>B n. P x" "P (L, g n)"
+ then obtain n where "\<forall>x\<in>B n. P x" "P (L, g n)"
unfolding eventually_at_top_linorder by blast
-
- have "eventually (\<lambda>y. y \<in> G n) F" "\<forall>z\<in>G n \<times> G n. P z" "g n \<in> G n" "P (L, g n)"
- using n gG by blast+
- thus "\<exists>X. (\<forall>\<^sub>F y in F. y \<in> X) \<and> (\<forall>z\<in>X \<times> X. P z) \<and> (\<exists>y. P (L, y) \<and> y \<in> X)"
- by blast
+ then show "\<exists>X. (\<forall>\<^sub>F y in F. y \<in> X) \<and> (\<forall>z\<in>X \<times> X. P z) \<and> (\<exists>y. P (L, y) \<and> y \<in> X)"
+ using gG by blast+
qed
thus "convergent_filter F"
by (auto simp: convergent_filter_iff)
@@ -2713,12 +2628,11 @@
proof safe
fix P :: "'a \<times> 'a \<Rightarrow> bool"
assume P: "eventually P uniformity"
- from U[OF this] obtain N where N: "\<forall>x\<in>U N. P x"
+ from U[OF this] obtain N where "\<forall>x\<in>U N. P x"
by blast
-
- show "eventually P (filtermap (map_prod f f) (sequentially \<times>\<^sub>F sequentially))"
+ then show "eventually P (filtermap (map_prod f f) (sequentially \<times>\<^sub>F sequentially))"
unfolding eventually_filtermap eventually_prod_sequentially
- by (rule exI[of _ N]) (use controlled N in \<open>auto simp: map_prod_def\<close>)
+ by (metis controlled map_prod_simp)
qed
qed
@@ -2778,10 +2692,10 @@
thus ?case
by (intro bexI[of _ "min \<epsilon>1 \<epsilon>2"]) auto
qed auto
- from \<open>\<epsilon> > 0\<close> obtain n where n: "1 / real (Suc n) < \<epsilon>"
+ from \<open>\<epsilon> > 0\<close> obtain n where "1 / real (Suc n) < \<epsilon>"
using nat_approx_posE by blast
- have "eventually P (principal {(x, y). dist x y < 1 / real (Suc n)})"
- using \<epsilon>(2) n by (auto simp: eventually_principal)
+ then have "eventually P (principal {(x, y). dist x y < 1 / real (Suc n)})"
+ using \<epsilon>(2) by (auto simp: eventually_principal)
thus "eventually P ?G"
by (intro eventually_INF1) auto
qed
@@ -2813,7 +2727,7 @@
show "((\<lambda>Y. \<Sum>x\<in>Y. g x) \<longlongrightarrow> T) (finite_subsets_at_top X)"
using assms(2) unfolding has_sum_def .
show "\<forall>\<^sub>F x in finite_subsets_at_top X. norm (sum f x) \<le> (\<Sum>x\<in>x. g x)"
- by (rule eventually_finite_subsets_at_top_weakI) (auto intro!: sum_norm_le assms)
+ by (simp add: assms(3) eventually_finite_subsets_at_top_weakI subsetD sum_norm_le)
qed auto
(*
@@ -2835,9 +2749,8 @@
proof -
have "((\<lambda>x. f (g x)) has_sum S) A \<longleftrightarrow> (f has_sum S) (g ` A)"
by (subst has_sum_reindex) (use assms in \<open>auto dest: bij_betw_imp_inj_on simp: o_def\<close>)
- also have "g ` A = B"
- using assms bij_betw_imp_surj_on by blast
- finally show ?thesis .
+ then show ?thesis
+ using assms bij_betw_imp_surj_on by blast
qed
lemma has_sum_reindex_bij_witness:
@@ -2848,16 +2761,7 @@
assumes "\<And>a. a \<in> S \<Longrightarrow> h (j a) = g a"
assumes "s = s'"
shows "(g has_sum s) S = (h has_sum s') T"
-proof -
- have bij:"bij_betw j S T"
- using assms by (intro bij_betwI[of _ _ _ i]) auto
- have "(h has_sum s') T \<longleftrightarrow> ((\<lambda>a. h (j a)) has_sum s) S"
- using has_sum_reindex_bij_betw[OF bij, of h] assms by simp
- also have "\<dots> \<longleftrightarrow> (g has_sum s) S"
- by (intro has_sum_cong) (use assms in auto)
- finally show ?thesis ..
-qed
-
+ by (smt (verit, del_insts) assms bij_betwI' has_sum_cong has_sum_reindex_bij_betw)
lemma has_sum_homomorphism:
@@ -2868,10 +2772,9 @@
by (induction X rule: infinite_finite_induct) (simp_all add: assms)
hence sum_h: "sum (h \<circ> f) = h \<circ> sum f"
by (intro ext) auto
- have "((h \<circ> f) has_sum h S) A"
- unfolding has_sum_def sum_h unfolding o_def
- by (rule continuous_on_tendsto_compose[OF assms(4)])
- (use assms in \<open>auto simp: has_sum_def\<close>)
+ then have "((h \<circ> f) has_sum h S) A"
+ using assms
+ by (metis UNIV_I continuous_on_def has_sum_comm_additive_general o_apply)
thus ?thesis
by (simp add: o_def)
qed
@@ -2892,18 +2795,10 @@
fixes h :: "'a :: {t2_space, topological_comm_monoid_add} \<Rightarrow>
'b :: {t2_space, topological_comm_monoid_add}"
assumes "(\<lambda>x. h (f x)) summable_on A \<longleftrightarrow> f summable_on A"
- assumes "h 0 = 0" "\<And>a b. h (a + b) = h a + h b" "continuous_on UNIV h"
+ assumes "h 0 = 0"
assumes "\<And>S. (f has_sum S) A \<Longrightarrow> ((\<lambda>x. h (f x)) has_sum (h S)) A"
shows "infsum (\<lambda>x. h (f x)) A = h (infsum f A)"
-proof (cases "f summable_on A")
- case False
- thus ?thesis by (simp add: infsum_def assms)
-next
- case True
- then obtain S where "(f has_sum S) A" by (auto simp: summable_on_def)
- moreover from this have "((\<lambda>x. h (f x)) has_sum (h S)) A" by (rule assms)
- ultimately show ?thesis by (simp add: infsumI)
-qed
+ by (metis assms has_sum_infsum infsumI infsum_not_exists)
lemma has_sum_bounded_linear:
assumes "bounded_linear h" and "(f has_sum S) A"
@@ -2917,16 +2812,12 @@
lemma summable_on_bounded_linear:
assumes "bounded_linear h" and "f summable_on A"
shows "(\<lambda>x. h (f x)) summable_on A"
-proof -
- interpret bounded_linear h by fact
- from assms(2) show ?thesis
- by (rule summable_on_homomorphism) (auto simp: add intro!: continuous_on)
-qed
+ by (metis assms has_sum_bounded_linear summable_on_def)
lemma summable_on_bounded_linear_iff:
assumes "bounded_linear h" and "bounded_linear h'" and "\<And>x. h' (h x) = x"
shows "(\<lambda>x. h (f x)) summable_on A \<longleftrightarrow> f summable_on A"
- by (auto dest: assms(1,2)[THEN summable_on_bounded_linear] simp: assms(3))
+ by (metis (full_types) assms summable_on_bounded_linear summable_on_cong)
lemma infsum_bounded_linear_strong:
fixes h :: "'a :: real_normed_vector \<Rightarrow> 'b :: real_normed_vector"
@@ -2946,7 +2837,7 @@
assumes "bounded_linear (mult c)"
assumes [simp]: "\<And>x. mult 0 x = 0"
shows "infsum (\<lambda>x. mult c (f x)) A = mult c (infsum f A)"
- using assms(1,2) by (cases "c = 0") (auto intro: infsum_bounded_linear_strong)
+ by (metis assms infsum_0 infsum_bounded_linear_strong)
lemma has_sum_of_nat: "(f has_sum S) A \<Longrightarrow> ((\<lambda>x. of_nat (f x)) has_sum of_nat S) A"
by (erule has_sum_homomorphism) (auto intro!: continuous_intros)
@@ -2967,9 +2858,8 @@
assume *: "finite {x\<in>A. f x \<noteq> 0}"
hence "f summable_on {x\<in>A. f x \<noteq> 0}"
by (rule summable_on_finite)
- also have "?this \<longleftrightarrow> f summable_on A"
- by (intro summable_on_cong_neutral) auto
- finally show "f summable_on A" .
+ then show "f summable_on A"
+ by (smt (verit) DiffE mem_Collect_eq summable_on_cong_neutral)
next
assume "f summable_on A"
then obtain S where "(f has_sum S) A"
@@ -2985,13 +2875,9 @@
proof (rule ccontr)
assume [simp]: "x \<notin> X"
have "sum f (insert x X) = S"
- using X(1,2) x by (intro X) auto
- also have "sum f (insert x X) = f x + sum f X"
- using X(1) by (subst sum.insert) auto
- also have "sum f X = S"
- by (intro X order.refl)
- finally have "f x = 0"
- by simp
+ using X x by (intro X) auto
+ then have "f x = 0"
+ using X by auto
with x show False
by auto
qed
@@ -3025,28 +2911,20 @@
by blast
have "\<forall>\<^sub>F X in finite_subsets_at_top A. sum f X < C"
using S C by (rule order_tendstoD(2))
- hence "\<forall>\<^sub>F X in finite_subsets_at_top A. sum f X \<le> C"
- by (rule eventually_mono) auto
- thus ?thesis by blast
+ thus ?thesis
+ by (meson eventually_mono nless_le)
next
- case False
- hence "\<forall>\<^sub>F X in finite_subsets_at_top A. sum f X \<le> S"
- by (auto simp: not_less)
- thus ?thesis by blast
+ case False thus ?thesis
+ by (meson not_eventuallyD not_le_imp_less)
qed
qed
lemma has_sum_mono':
fixes S S' :: "'a :: {linorder_topology, ordered_comm_monoid_add, topological_comm_monoid_add}"
- assumes "(f has_sum S) A" "(f has_sum S') B" "A \<subseteq> B" "\<And>x. x \<in> B - A \<Longrightarrow> f x \<ge> 0"
+ assumes f: "(f has_sum S) A" "(f has_sum S') B"
+ and AB: "A \<subseteq> B" "\<And>x. x \<in> B - A \<Longrightarrow> f x \<ge> 0"
shows "S \<le> S'"
-proof (rule has_sum_mono)
- show "(f has_sum S') B" by fact
- have "(f has_sum S) A \<longleftrightarrow> ((\<lambda>x. if x \<in> A then f x else 0) has_sum S) B"
- by (rule has_sum_cong_neutral) (use assms in auto)
- thus "((\<lambda>x. if x \<in> A then f x else 0) has_sum S) B"
- using assms(1) by blast
-qed (insert assms, auto)
+ using AB has_sum_mono_neutral[OF f] by fastforce
context
@@ -3069,8 +2947,9 @@
have bound': "sum f X \<le> C" if "X \<subseteq> A" "finite X" for X
proof -
have "sum f X \<le> sum f (X \<union> X0)"
- using that X0(1,2) assms(1) by (intro sum_mono2) auto
- also have "\<dots> \<le> C" using X0(1,2) that by (intro X0) auto
+ using that X0 assms(1) by (intro sum_mono2) auto
+ also have "\<dots> \<le> C"
+ by (simp add: X0 that)
finally show ?thesis .
qed
hence bdd: "bdd_above (sum f ` {X. X \<subseteq> A \<and> finite X})"
@@ -3115,8 +2994,7 @@
shows "g summable_on A"
proof -
obtain C where C: "\<forall>\<^sub>F X in finite_subsets_at_top A. sum f X \<le> C"
- using summable_on_imp_bounded_partial_sums [of f]
- using assms(1) by presburger
+ using assms(1) summable_on_imp_bounded_partial_sums by blast
show ?thesis
proof (rule nonneg_bounded_partial_sums_imp_summable_on)
show "\<forall>\<^sub>F X in finite_subsets_at_top A. sum g X \<le> C"
@@ -3142,7 +3020,7 @@
shows "f summable_on (A \<union> B)"
proof -
have "f summable_on (A \<union> (B - A))"
- by (intro summable_on_Un_disjoint[OF assms(1) summable_on_subset[OF assms(2)]]) auto
+ by (meson Diff_disjoint Diff_subset assms summable_on_Un_disjoint summable_on_subset)
also have "A \<union> (B - A) = A \<union> B"
by blast
finally show ?thesis .
@@ -3154,7 +3032,7 @@
using summable_on_union[of f A "{x}"] by (auto intro: summable_on_subset)
lemma has_sum_finiteI: "finite A \<Longrightarrow> S = sum f A \<Longrightarrow> (f has_sum S) A"
- using has_sum_finite by blast
+ by simp
lemma has_sum_insert:
fixes f :: "'a \<Rightarrow> 'b :: topological_comm_monoid_add"
@@ -3269,14 +3147,7 @@
assumes g: "(g has_sum S) A"
assumes summable: "f summable_on Sigma A B"
shows "(f has_sum S) (Sigma A B)"
-proof -
- from summable obtain S' where S': "(f has_sum S') (Sigma A B)"
- using summable_on_def by blast
- have "(g has_sum S') A"
- by (rule has_sum_SigmaD[OF S' f])
- with g S' show ?thesis
- using has_sum_unique by blast
-qed
+ by (metis f g has_sum_SigmaD has_sum_infsum has_sum_unique local.summable)
lemma summable_on_SigmaD1:
fixes f :: "_ \<Rightarrow> _ \<Rightarrow> 'a :: {complete_uniform_space, uniform_topological_group_add, ab_group_add, topological_comm_monoid_add}"
@@ -3307,12 +3178,7 @@
lemma summable_on_swap:
"f summable_on (A \<times> B) \<longleftrightarrow> (\<lambda>(x,y). f (y,x)) summable_on (B \<times> A)"
-proof -
- have "bij_betw (\<lambda>(x,y). (y,x)) (B \<times> A) (A \<times> B)"
- by (rule bij_betwI[of _ _ _ "\<lambda>(x,y). (y,x)"]) auto
- from summable_on_reindex_bij_betw[OF this, where f = f] show ?thesis
- by (simp add: case_prod_unfold)
-qed
+ by (metis has_sum_swap summable_on_def)
lemma has_sum_cmult_right_iff:
fixes c :: "'a :: {topological_semigroup_mult, field}"
@@ -3331,13 +3197,7 @@
lemma finite_nonzero_values_imp_summable_on:
assumes "finite {x\<in>X. f x \<noteq> 0}"
shows "f summable_on X"
-proof -
- have "f summable_on {x\<in>X. f x \<noteq> 0}"
- by (intro summable_on_finite assms)
- also have "?this \<longleftrightarrow> f summable_on X"
- by (intro summable_on_cong_neutral) auto
- finally show ?thesis .
-qed
+ by (smt (verit, del_insts) Diff_iff assms mem_Collect_eq summable_on_cong_neutral summable_on_finite)
lemma summable_on_of_int_iff:
"(\<lambda>x::'a. of_int (f x) :: 'b :: real_normed_algebra_1) summable_on A \<longleftrightarrow> f summable_on A"
@@ -3351,7 +3211,7 @@
by (auto simp: summable_on_def)
hence "(sum (\<lambda>x. of_int (f x) :: 'b) \<longlongrightarrow> S) (finite_subsets_at_top A)"
unfolding has_sum_def .
- moreover have "1 / 2 > (0 :: real)"
+ moreover have "1/2 > (0 :: real)"
by auto
ultimately have "eventually (\<lambda>X. dist (sum (\<lambda>x. of_int (f x) :: 'b) X) S < 1/2)
(finite_subsets_at_top A)"
@@ -3360,31 +3220,20 @@
"\<And>Y. finite Y \<Longrightarrow> X \<subseteq> Y \<Longrightarrow> Y \<subseteq> A \<Longrightarrow> dist (sum (\<lambda>x. of_int (f x)) Y) S < 1/2"
unfolding eventually_finite_subsets_at_top by metis
- have X': "sum f Y = sum f X" if "finite Y" "X \<subseteq> Y" "Y \<subseteq> A" for Y
+ have "sum f Y = sum f X" if "finite Y" "X \<subseteq> Y" "Y \<subseteq> A" for Y
proof -
- have "dist (sum (\<lambda>x. of_int (f x)) X) S < 1 / 2"
+ have "dist (sum (\<lambda>x. of_int (f x)) X) S < 1/2"
by (intro X) auto
- moreover have "dist (sum (\<lambda>x. of_int (f x)) Y) S < 1 / 2"
+ moreover have "dist (sum (\<lambda>x. of_int (f x)) Y) S < 1/2"
by (intro X that)
ultimately have "dist (sum (\<lambda>x. of_int (f x)) X) (sum (\<lambda>x. of_int (f x) :: 'b) Y) <
- 1 / 2 + 1 / 2"
+ 1/2 + 1/2"
using dist_triangle_less_add by blast
thus ?thesis
by (simp add: dist_norm flip: of_int_sum of_int_diff)
qed
-
- have "{x\<in>A. f x \<noteq> 0} \<subseteq> X"
- proof (rule ccontr)
- assume "\<not>{x\<in>A. f x \<noteq> 0} \<subseteq> X"
- then obtain x where x: "x \<in> A" "f x \<noteq> 0" "x \<notin> X"
- by blast
- have "sum f (insert x X) = sum f X"
- using x X by (intro X') auto
- also have "sum f (insert x X) = f x + sum f X"
- using x X by auto
- finally show False
- using x by auto
- qed
+ then have "{x\<in>A. f x \<noteq> 0} \<subseteq> X"
+ by (smt (verit) X finite_insert insert_iff mem_Collect_eq subset_eq sum.insert)
with \<open>finite X\<close> have "finite {x\<in>A. f x \<noteq> 0}"
using finite_subset by blast
thus "f summable_on A"
@@ -3403,8 +3252,6 @@
by simp
also have "?this \<longleftrightarrow> (\<lambda>x. int (f x)) summable_on A"
by (rule summable_on_of_int_iff)
- also have "\<dots> \<longleftrightarrow> finite {x\<in>A. f x \<noteq> 0}"
- by (simp add: summable_on_discrete_iff)
also have "\<dots> \<longleftrightarrow> f summable_on A"
by (simp add: summable_on_discrete_iff)
finally show "f summable_on A" .
@@ -3412,13 +3259,11 @@
lemma infsum_of_nat:
"infsum (\<lambda>x::'a. of_nat (f x) :: 'b :: {real_normed_algebra_1}) A = of_nat (infsum f A)"
- by (rule infsum_homomorphism_strong)
- (auto simp: summable_on_of_nat has_sum_of_nat summable_on_of_nat_iff)
+ by (metis has_sum_infsum has_sum_of_nat infsumI infsum_def of_nat_0 summable_on_of_nat_iff)
lemma infsum_of_int:
"infsum (\<lambda>x::'a. of_int (f x) :: 'b :: {real_normed_algebra_1}) A = of_int (infsum f A)"
- by (rule infsum_homomorphism_strong)
- (auto simp: summable_on_of_nat has_sum_of_int summable_on_of_int_iff)
+ by (metis has_sum_infsum has_sum_of_int infsumI infsum_not_exists of_int_0 summable_on_of_int_iff)
lemma summable_on_SigmaI:
@@ -3440,7 +3285,7 @@
"finite X'" "X' \<subseteq> A" "\<And>Y. finite Y \<Longrightarrow> X' \<subseteq> Y \<Longrightarrow> Y \<subseteq> A \<Longrightarrow> sum g Y \<le> C"
unfolding eventually_finite_subsets_at_top by metis
have "sum g X \<le> sum g (X \<union> X')"
- using X X'(1,2) by (intro sum_mono2 g_nonneg) auto
+ using X X' by (intro sum_mono2 g_nonneg) auto
also have "\<dots> \<le> C"
using X X'(1,2) by (intro X'(3)) auto
finally show ?thesis .
@@ -3481,8 +3326,7 @@
hence "\<forall>\<^sub>F X in finite_subsets_at_top (Sigma A B). sum f X \<le> C"
unfolding eventually_finite_subsets_at_top by auto
thus ?thesis
- by (intro nonneg_bounded_partial_sums_imp_summable_on[where C = C])
- (use f_nonneg in auto)
+ by (metis SigmaE f_nonneg nonneg_bounded_partial_sums_imp_summable_on)
qed
lemma summable_on_UnionI:
@@ -3508,14 +3352,8 @@
assumes sum1: "f summable_on (Sigma A B)"
assumes sum2: "\<And>x. x \<in> A \<Longrightarrow> (\<lambda>y. f (x, y)) summable_on (B x)"
shows "(\<lambda>x. infsum (\<lambda>y. f (x, y)) (B x)) summable_on A"
-proof -
- from sum1 have 1: "(f has_sum infsum f (Sigma A B)) (Sigma A B)"
- using has_sum_infsum by blast
- have 2: "((\<lambda>y. f (x, y)) has_sum infsum (\<lambda>y. f (x, y)) (B x)) (B x)"
- if "x \<in> A" for x using sum2[OF that] by simp
- from has_sum_SigmaD[OF 1 2] show ?thesis
- using has_sum_imp_summable by blast
-qed
+ using assms unfolding summable_on_def
+ by (smt (verit, del_insts) assms has_sum_SigmaD has_sum_cong has_sum_infsum)
lemma summable_on_UnionD:
fixes f :: "'a \<Rightarrow> 'c :: {topological_comm_monoid_add,t3_space}"
@@ -3568,24 +3406,9 @@
shows "(\<lambda>x. norm (f x)) summable_on A"
proof (rule Infinite_Sum.abs_summable_on_comparison_test)
have "g summable_on A \<longleftrightarrow> (\<lambda>x. norm (g x)) summable_on A"
- proof (rule summable_on_cong)
- fix x assume "x \<in> A"
- have "0 \<le> norm (f x)"
- by simp
- also have "\<dots> \<le> g x"
- by (rule assms) fact
- finally show "g x = norm (g x)"
- by simp
- qed
+ by (metis summable_on_iff_abs_summable_on_real)
with assms show "(\<lambda>x. norm (g x)) summable_on A" by blast
-next
- fix x assume "x \<in> A"
- have "norm (f x) \<le> g x"
- by (intro assms) fact
- also have "\<dots> \<le> norm (g x)"
- by simp
- finally show "norm (f x) \<le> norm (g x)" .
-qed
+qed (use assms in fastforce)
lemma has_sum_geometric_from_1:
fixes z :: "'a :: {real_normed_field, banach}"