--- a/src/HOL/Analysis/Uniform_Limit.thy Mon Dec 19 14:09:37 2022 +0100
+++ b/src/HOL/Analysis/Uniform_Limit.thy Tue Dec 20 17:59:44 2022 +0000
@@ -198,6 +198,19 @@
unfolding uniformly_convergent_on_def assms(2) [symmetric]
by (intro iff_exI uniform_limit_cong eventually_mono [OF assms(1)]) auto
+lemma uniformly_convergent_on_compose:
+ assumes "uniformly_convergent_on A f"
+ assumes "filterlim g sequentially sequentially"
+ shows "uniformly_convergent_on A (\<lambda>n. f (g n))"
+proof -
+ from assms(1) obtain f' where "uniform_limit A f f' sequentially"
+ by (auto simp: uniformly_convergent_on_def)
+ hence "uniform_limit A (\<lambda>n. f (g n)) f' sequentially"
+ by (rule filterlim_compose) fact
+ thus ?thesis
+ by (auto simp: uniformly_convergent_on_def)
+qed
+
lemma uniformly_convergent_uniform_limit_iff:
"uniformly_convergent_on X f \<longleftrightarrow> uniform_limit X f (\<lambda>x. lim (\<lambda>n. f n x)) sequentially"
proof
@@ -308,6 +321,46 @@
ultimately show ?thesis by auto
qed
+lemma uniformly_convergent_on_sum_E:
+ fixes \<epsilon>::real and f :: "nat \<Rightarrow> 'a \<Rightarrow> 'b::{complete_space,real_normed_vector}"
+ assumes uconv: "uniformly_convergent_on K (\<lambda>n z. \<Sum>k<n. f k z)" and "\<epsilon>>0"
+ obtains N where "\<And>m n z. \<lbrakk>N \<le> m; m \<le> n; z\<in>K\<rbrakk> \<Longrightarrow> norm(\<Sum>k=m..<n. f k z) < \<epsilon>"
+proof -
+ obtain N where N: "\<And>m n z. \<lbrakk>N \<le> m; N \<le> n; z\<in>K\<rbrakk> \<Longrightarrow> dist (\<Sum>k<m. f k z) (\<Sum>k<n. f k z) < \<epsilon>"
+ using uconv \<open>\<epsilon>>0\<close> unfolding uniformly_Cauchy_on_def uniformly_convergent_eq_Cauchy by meson
+ show thesis
+ proof
+ fix m n z
+ assume "N \<le> m" "m \<le> n" "z \<in> K"
+ moreover have "(\<Sum>k = m..<n. f k z) = (\<Sum>k<n. f k z) - (\<Sum>k<m. f k z)"
+ by (metis atLeast0LessThan le0 sum_diff_nat_ivl \<open>m \<le> n\<close>)
+ ultimately show "norm(\<Sum>k = m..<n. f k z) < \<epsilon>"
+ using N by (simp add: dist_norm)
+ qed
+qed
+
+lemma uniformly_convergent_on_sum_iff:
+ fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> 'b::{complete_space,real_normed_vector}"
+ shows "uniformly_convergent_on K (\<lambda>n z. \<Sum>k<n. f k z)
+ \<longleftrightarrow> (\<forall>\<epsilon>>0. \<exists>N. \<forall>m n z. N\<le>m \<longrightarrow> m\<le>n \<longrightarrow> z\<in>K \<longrightarrow> norm (\<Sum>k=m..<n. f k z) < \<epsilon>)" (is "?lhs=?rhs")
+proof
+ assume R: ?rhs
+ show ?lhs
+ unfolding uniformly_Cauchy_on_def uniformly_convergent_eq_Cauchy
+ proof (intro strip)
+ fix \<epsilon>::real
+ assume "\<epsilon>>0"
+ then obtain N where "\<And>m n z. \<lbrakk>N \<le> m; m \<le> n; z\<in>K\<rbrakk> \<Longrightarrow> norm(\<Sum>k = m..<n. f k z) < \<epsilon>"
+ using R by blast
+ then have "\<forall>x\<in>K. \<forall>m\<ge>N. \<forall>n\<ge>m. norm ((\<Sum>k<m. f k x) - (\<Sum>k<n. f k x)) < \<epsilon>"
+ by (metis atLeast0LessThan le0 sum_diff_nat_ivl norm_minus_commute)
+ then have "\<forall>x\<in>K. \<forall>m\<ge>N. \<forall>n\<ge>N. norm ((\<Sum>k<m. f k x) - (\<Sum>k<n. f k x)) < \<epsilon>"
+ by (metis linorder_le_cases norm_minus_commute)
+ then show "\<exists>M. \<forall>x\<in>K. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (\<Sum>k<m. f k x) (\<Sum>k<n. f k x) < \<epsilon>"
+ by (metis dist_norm)
+ qed
+qed (metis uniformly_convergent_on_sum_E)
+
text \<open>TODO: remove explicit formulations
@{thm uniformly_convergent_eq_cauchy uniformly_cauchy_imp_uniformly_convergent}?!\<close>
@@ -316,6 +369,102 @@
unfolding uniformly_convergent_on_def convergent_def
by (auto dest: tendsto_uniform_limitI)
+subsection \<open>Comparison Test\<close>
+
+lemma uniformly_summable_comparison_test:
+ fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> 'b :: banach"
+ assumes "uniformly_convergent_on A (\<lambda>N x. \<Sum>n<N. g n x)"
+ assumes "\<And>n x. x \<in> A \<Longrightarrow> norm (f n x) \<le> g n x"
+ shows "uniformly_convergent_on A (\<lambda>N x. \<Sum>n<N. f n x)"
+proof -
+ have "uniformly_Cauchy_on A (\<lambda>N x. \<Sum>n<N. f n x)"
+ proof (rule uniformly_Cauchy_onI')
+ fix e :: real assume e: "e > 0"
+ obtain M where M: "\<And>x m n. x \<in> A \<Longrightarrow> m \<ge> M \<Longrightarrow> n \<ge> M \<Longrightarrow> dist (\<Sum>k<m. g k x) (\<Sum>k<n. g k x) < e"
+ using assms(1) e unfolding uniformly_convergent_eq_Cauchy uniformly_Cauchy_on_def by metis
+ show "\<exists>M. \<forall>x\<in>A. \<forall>m\<ge>M. \<forall>n>m. dist (\<Sum>k<m. f k x) (\<Sum>k<n. f k x) < e"
+ proof (rule exI[of _ M], safe)
+ fix x m n assume xmn: "x \<in> A" "m \<ge> M" "m < n"
+ have nonneg: "g k x \<ge> 0" for k
+ by (rule order.trans[OF _ assms(2)]) (use xmn in auto)
+ have "dist (\<Sum>k<m. f k x) (\<Sum>k<n. f k x) = norm (\<Sum>k\<in>{..<n}-{..<m}. f k x)"
+ using xmn by (subst sum_diff) (auto simp: dist_norm norm_minus_commute)
+ also have "{..<n}-{..<m} = {m..<n}"
+ by auto
+ also have "norm (\<Sum>k\<in>{m..<n}. f k x) \<le> (\<Sum>k\<in>{m..<n}. norm (f k x))"
+ using norm_sum by blast
+ also have "\<dots> \<le> (\<Sum>k\<in>{m..<n}. g k x)"
+ by (intro sum_mono assms xmn)
+ also have "\<dots> = \<bar>\<Sum>k\<in>{m..<n}. g k x\<bar>"
+ by (subst abs_of_nonneg) (auto simp: nonneg intro!: sum_nonneg)
+ also have "{m..<n} = {..<n} - {..<m}"
+ by auto
+ also have "\<bar>\<Sum>k\<in>\<dots>. g k x\<bar> = dist (\<Sum>k<m. g k x) (\<Sum>k<n. g k x)"
+ using xmn by (subst sum_diff) (auto simp: abs_minus_commute dist_norm)
+ also have "\<dots> < e"
+ by (rule M) (use xmn in auto)
+ finally show "dist (\<Sum>k<m. f k x) (\<Sum>k<n. f k x) < e" .
+ qed
+ qed
+ thus ?thesis
+ unfolding uniformly_convergent_eq_Cauchy .
+qed
+
+lemma uniform_limit_compose_uniformly_continuous_on:
+ fixes f :: "'a :: metric_space \<Rightarrow> 'b :: metric_space"
+ assumes lim: "uniform_limit A g g' F"
+ assumes cont: "uniformly_continuous_on B f"
+ assumes ev: "eventually (\<lambda>x. \<forall>y\<in>A. g x y \<in> B) F" and "closed B"
+ shows "uniform_limit A (\<lambda>x y. f (g x y)) (\<lambda>y. f (g' y)) F"
+proof (cases "F = bot")
+ case [simp]: False
+ show ?thesis
+ unfolding uniform_limit_iff
+ proof safe
+ fix e :: real assume e: "e > 0"
+
+ have g'_in_B: "g' y \<in> B" if "y \<in> A" for y
+ proof (rule Lim_in_closed_set)
+ show "eventually (\<lambda>x. g x y \<in> B) F"
+ using ev by eventually_elim (use that in auto)
+ show "((\<lambda>x. g x y) \<longlongrightarrow> g' y) F"
+ using lim that by (metis tendsto_uniform_limitI)
+ qed (use \<open>closed B\<close> in auto)
+
+ obtain d where d: "d > 0" "\<And>x y. x \<in> B \<Longrightarrow> y \<in> B \<Longrightarrow> dist x y < d \<Longrightarrow> dist (f x) (f y) < e"
+ using e cont unfolding uniformly_continuous_on_def by metis
+ from lim have "eventually (\<lambda>x. \<forall>y\<in>A. dist (g x y) (g' y) < d) F"
+ unfolding uniform_limit_iff using \<open>d > 0\<close> by meson
+ thus "eventually (\<lambda>x. \<forall>y\<in>A. dist (f (g x y)) (f (g' y)) < e) F"
+ using assms(3)
+ proof eventually_elim
+ case (elim x)
+ show "\<forall>y\<in>A. dist (f (g x y)) (f (g' y)) < e"
+ proof safe
+ fix y assume y: "y \<in> A"
+ show "dist (f (g x y)) (f (g' y)) < e"
+ proof (rule d)
+ show "dist (g x y) (g' y) < d"
+ using elim y by blast
+ qed (use y elim g'_in_B in auto)
+ qed
+ qed
+ qed
+qed (auto simp: filterlim_def)
+
+lemma uniformly_convergent_on_compose_uniformly_continuous_on:
+ fixes f :: "'a :: metric_space \<Rightarrow> 'b :: metric_space"
+ assumes lim: "uniformly_convergent_on A g"
+ assumes cont: "uniformly_continuous_on B f"
+ assumes ev: "eventually (\<lambda>x. \<forall>y\<in>A. g x y \<in> B) sequentially" and "closed B"
+ shows "uniformly_convergent_on A (\<lambda>x y. f (g x y))"
+proof -
+ from lim obtain g' where g': "uniform_limit A g g' sequentially"
+ by (auto simp: uniformly_convergent_on_def)
+ thus ?thesis
+ using uniform_limit_compose_uniformly_continuous_on[OF g' cont ev \<open>closed B\<close>]
+ by (auto simp: uniformly_convergent_on_def)
+qed
subsection \<open>Weierstrass M-Test\<close>