--- a/src/HOL/Analysis/Complex_Transcendental.thy Tue Dec 20 19:43:55 2022 +0100
+++ b/src/HOL/Analysis/Complex_Transcendental.thy Tue Dec 20 22:24:36 2022 +0000
@@ -1526,6 +1526,47 @@
qed
+lemma norm_Ln_le:
+ fixes z :: complex
+ assumes "norm z < 1/2"
+ shows "norm (Ln(1+z)) \<le> 2 * norm z"
+proof -
+ have sums: "(\<lambda>n. - ((- z) ^ n) / of_nat n) sums ln (1 + z)"
+ by (intro Ln_series') (use assms in auto)
+ have summable: "summable (\<lambda>n. norm (- ((- z) ^ n / of_nat n)))"
+ using ln_series'[of "-norm z"] assms
+ by (simp add: sums_iff summable_minus_iff norm_power norm_divide)
+
+ have "norm (ln (1 + z)) = norm (\<Sum>n. -((-z) ^ n / of_nat n))"
+ using sums by (simp add: sums_iff)
+ also have "\<dots> \<le> (\<Sum>n. norm (-((-z) ^ n / of_nat n)))"
+ using summable by (rule summable_norm)
+ also have "\<dots> = (\<Sum>n. norm (-((-z) ^ Suc n / of_nat (Suc n))))"
+ using summable by (subst suminf_split_head) auto
+ also have "\<dots> \<le> (\<Sum>n. norm z * (1 / 2) ^ n)"
+ proof (rule suminf_le)
+ show "summable (\<lambda>n. norm z * (1 / 2) ^ n)"
+ by (intro summable_mult summable_geometric) auto
+ next
+ show "summable (\<lambda>n. norm (- ((- z) ^ Suc n / of_nat (Suc n))))"
+ using summable by (subst summable_Suc_iff)
+ next
+ fix n
+ have "norm (-((-z) ^ Suc n / of_nat (Suc n))) = norm z * (norm z ^ n / real (Suc n))"
+ by (simp add: norm_power norm_divide norm_mult del: of_nat_Suc)
+ also have "\<dots> \<le> norm z * ((1 / 2) ^ n / 1)"
+ using assms by (intro mult_left_mono frac_le power_mono) auto
+ finally show "norm (- ((- z) ^ Suc n / of_nat (Suc n))) \<le> norm z * (1 / 2) ^ n"
+ by simp
+ qed
+ also have "\<dots> = norm z * (\<Sum>n. (1 / 2) ^ n)"
+ by (subst suminf_mult) (auto intro: summable_geometric)
+ also have "(\<Sum>n. (1 / 2 :: real) ^ n) = 2"
+ using geometric_sums[of "1 / 2 :: real"] by (simp add: sums_iff)
+ finally show ?thesis
+ by (simp add: mult_ac)
+qed
+
subsection\<^marker>\<open>tag unimportant\<close>\<open>Quadrant-type results for Ln\<close>
lemma cos_lt_zero_pi: "pi/2 < x \<Longrightarrow> x < 3*pi/2 \<Longrightarrow> cos x < 0"
@@ -1796,6 +1837,218 @@
finally show ?thesis .
qed
+lemma norm_Ln_times_le:
+ assumes "w \<noteq> 0" "z \<noteq> 0"
+ shows "cmod (Ln(w * z)) \<le> cmod (Ln(w) + Ln(z))"
+proof (cases "- pi < Im(Ln w + Ln z) \<and> Im(Ln w + Ln z) \<le> pi")
+ case True
+ then show ?thesis
+ by (simp add: Ln_times_simple assms)
+next
+ case False
+ then show ?thesis
+ by (smt (verit) Im_Ln_le_pi assms cmod_Im_le_iff exp_Ln exp_add ln_unique mpi_less_Im_Ln mult_eq_0_iff norm_exp_eq_Re)
+qed
+
+corollary norm_Ln_prod_le:
+ fixes f :: "'a \<Rightarrow> complex"
+ assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<noteq> 0"
+ shows "cmod (Ln (prod f A)) \<le> (\<Sum>x \<in> A. cmod (Ln (f x)))"
+ using assms
+proof (induction A rule: infinite_finite_induct)
+ case (insert x A)
+ then show ?case
+ by simp (smt (verit) norm_Ln_times_le norm_triangle_ineq prod_zero_iff)
+qed auto
+
+lemma norm_Ln_exp_le: "norm (Ln (exp z)) \<le> norm z"
+ by (smt (verit) Im_Ln_le_pi Ln_exp Re_Ln cmod_Im_le_iff exp_not_eq_zero ln_exp mpi_less_Im_Ln norm_exp_eq_Re)
+
+subsection\<^marker>\<open>tag unimportant\<close>\<open>Uniform convergence and products\<close>
+
+(* TODO: could be generalised perhaps, but then one would have to do without the ln *)
+lemma uniformly_convergent_on_prod_aux:
+ fixes f :: "nat \<Rightarrow> complex \<Rightarrow> complex"
+ assumes norm_f: "\<And>n x. x \<in> A \<Longrightarrow> norm (f n x) < 1"
+ assumes cont: "\<And>n. continuous_on A (f n)"
+ assumes conv: "uniformly_convergent_on A (\<lambda>N x. \<Sum>n<N. ln (1 + f n x))"
+ assumes A: "compact A"
+ shows "uniformly_convergent_on A (\<lambda>N x. \<Prod>n<N. 1 + f n x)"
+proof -
+ from conv obtain S where S: "uniform_limit A (\<lambda>N x. \<Sum>n<N. ln (1 + f n x)) S sequentially"
+ by (auto simp: uniformly_convergent_on_def)
+ have cont': "continuous_on A S"
+ proof (rule uniform_limit_theorem[OF _ S])
+ have "f n x + 1 \<notin> \<real>\<^sub>\<le>\<^sub>0" if "x \<in> A" for n x
+ proof
+ assume "f n x + 1 \<in> \<real>\<^sub>\<le>\<^sub>0"
+ then obtain t where t: "t \<le> 0" "f n x + 1 = of_real t"
+ by (auto elim!: nonpos_Reals_cases)
+ hence "f n x = of_real (t - 1)"
+ by (simp add: algebra_simps)
+ also have "norm \<dots> \<ge> 1"
+ using t by (subst norm_of_real) auto
+ finally show False
+ using norm_f[of x n] that by auto
+ qed
+ thus "\<forall>\<^sub>F n in sequentially. continuous_on A (\<lambda>x. \<Sum>n<n. Ln (1 + f n x))"
+ by (auto intro!: always_eventually continuous_intros cont simp: add_ac)
+ qed auto
+
+ define B where "B = {x + y |x y. x \<in> S ` A \<and> y \<in> cball 0 1}"
+ have "compact B"
+ unfolding B_def by (intro compact_sums compact_continuous_image cont' A) auto
+
+ have "uniformly_convergent_on A (\<lambda>N x. exp ((\<Sum>n<N. ln (1 + f n x))))"
+ using conv
+ proof (rule uniformly_convergent_on_compose_uniformly_continuous_on)
+ show "closed B"
+ using \<open>compact B\<close> by (auto dest: compact_imp_closed)
+ show "uniformly_continuous_on B exp"
+ by (intro compact_uniformly_continuous continuous_intros \<open>compact B\<close>)
+
+ have "eventually (\<lambda>N. \<forall>x\<in>A. dist (\<Sum>n<N. Ln (1 + f n x)) (S x) < 1) sequentially"
+ using S unfolding uniform_limit_iff by simp
+ thus "eventually (\<lambda>N. \<forall>x\<in>A. (\<Sum>n<N. Ln (1 + f n x)) \<in> B) sequentially"
+ proof eventually_elim
+ case (elim N)
+ show "\<forall>x\<in>A. (\<Sum>n<N. Ln (1 + f n x)) \<in> B"
+ proof safe
+ fix x assume x: "x \<in> A"
+ have "(\<Sum>n<N. Ln (1 + f n x)) = S x + ((\<Sum>n<N. Ln (1 + f n x)) - S x)"
+ by auto
+ moreover have "((\<Sum>n<N. Ln (1 + f n x)) - S x) \<in> ball 0 1"
+ using elim x by (auto simp: dist_norm norm_minus_commute)
+ ultimately show "(\<Sum>n<N. Ln (1 + f n x)) \<in> B"
+ unfolding B_def using x by fastforce
+ qed
+ qed
+ qed
+ also have "?this \<longleftrightarrow> uniformly_convergent_on A (\<lambda>N x. \<Prod>n<N. 1 + f n x)"
+ proof (intro uniformly_convergent_cong refl always_eventually allI ballI)
+ fix N :: nat and x assume x: "x \<in> A"
+ have "exp (\<Sum>n<N. ln (1 + f n x)) = (\<Prod>n<N. exp (ln (1 + f n x)))"
+ by (simp add: exp_sum)
+ also have "\<dots> = (\<Prod>n<N. 1 + f n x)"
+ proof (rule prod.cong)
+ fix n assume "n \<in> {..<N}"
+ have "f n x \<noteq> -1"
+ using norm_f[of x n] x by auto
+ thus "exp (ln (1 + f n x)) = 1 + f n x"
+ by (simp add: add_eq_0_iff)
+ qed auto
+ finally show "exp (\<Sum>n<N. ln (1 + f n x)) = (\<Prod>n<N. 1 + f n x)" .
+ qed
+ finally show ?thesis .
+qed
+
+(* Theorem 17.6 by Bak & Newman, roughly *)
+lemma uniformly_convergent_on_prod:
+ fixes f :: "nat \<Rightarrow> complex \<Rightarrow> complex"
+ assumes cont: "\<And>n. continuous_on A (f n)"
+ assumes A: "compact A"
+ assumes conv_sum: "uniformly_convergent_on A (\<lambda>N x. \<Sum>n<N. norm (f n x))"
+ shows "uniformly_convergent_on A (\<lambda>N x. \<Prod>n<N. 1 + f n x)"
+proof -
+ obtain M where M: "\<And>n x. n \<ge> M \<Longrightarrow> x \<in> A \<Longrightarrow> norm (f n x) < 1 / 2"
+ proof -
+ from conv_sum have "uniformly_Cauchy_on A (\<lambda>N x. \<Sum>n<N. norm (f n x))"
+ using uniformly_convergent_Cauchy by blast
+ moreover have "(1 / 2 :: real) > 0"
+ by simp
+ ultimately obtain M where M:
+ "\<And>x m n. x \<in> A \<Longrightarrow> m \<ge> M \<Longrightarrow> n \<ge> M \<Longrightarrow> dist (\<Sum>k<m. norm (f k x)) (\<Sum>k<n. norm (f k x)) < 1 / 2"
+ unfolding uniformly_Cauchy_on_def by fast
+ show ?thesis
+ proof (rule that[of M])
+ fix n x assume nx: "n \<ge> M" "x \<in> A"
+ have "dist (\<Sum>k<Suc n. norm (f k x)) (\<Sum>k<n. norm (f k x)) < 1 / 2"
+ by (rule M) (use nx in auto)
+ also have "dist (\<Sum>k<Suc n. norm (f k x)) (\<Sum>k<n. norm (f k x)) = norm (f n x)"
+ by (simp add: dist_norm)
+ finally show "norm (f n x) < 1 / 2" .
+ qed
+ qed
+
+ have conv: "uniformly_convergent_on A (\<lambda>N x. \<Sum>n<N. ln (1 + f (n + M) x))"
+ proof (rule uniformly_summable_comparison_test)
+ show "norm (ln (1 + f (n + M) x)) \<le> 2 * norm (f (n + M) x)" if "x \<in> A" for n x
+ by (rule norm_Ln_le) (use M[of "n + M" x] that in auto)
+ have *: "filterlim (\<lambda>n. n + M) at_top at_top"
+ by (rule filterlim_add_const_nat_at_top)
+ have "uniformly_convergent_on A (\<lambda>N x. 2 * ((\<Sum>n<N+M. norm (f n x)) - (\<Sum>n<M. norm (f n x))))"
+ by (intro uniformly_convergent_mult uniformly_convergent_minus
+ uniformly_convergent_on_compose[OF conv_sum *] uniformly_convergent_on_const)
+ also have "(\<lambda>N x. 2 * ((\<Sum>n<N+M. norm (f n x)) - (\<Sum>n<M. norm (f n x)))) =
+ (\<lambda>N x. \<Sum>n<N. 2 * norm (f (n + M) x))" (is "?lhs = ?rhs")
+ proof (intro ext)
+ fix N x
+ have "(\<Sum>n<N+M. norm (f n x)) - (\<Sum>n<M. norm (f n x)) = (\<Sum>n\<in>{..<N+M}-{..<M}. norm (f n x))"
+ by (subst sum_diff) auto
+ also have "\<dots> = (\<Sum>n<N. norm (f (n + M) x))"
+ by (intro sum.reindex_bij_witness[of _ "\<lambda>n. n + M" "\<lambda>n. n - M"]) auto
+ finally show "?lhs N x = ?rhs N x"
+ by (simp add: sum_distrib_left)
+ qed
+ finally show "uniformly_convergent_on A (\<lambda>N x. \<Sum>n<N. 2 * cmod (f (n + M) x))" .
+ qed
+
+ have conv': "uniformly_convergent_on A (\<lambda>N x. \<Prod>n<N. 1 + f (n + M) x)"
+ proof (rule uniformly_convergent_on_prod_aux)
+ show "norm (f (n + M) x) < 1" if "x \<in> A" for n x
+ using M[of "n + M" x] that by simp
+ qed (use M assms conv in auto)
+
+ then obtain S where S: "uniform_limit A (\<lambda>N x. \<Prod>n<N. 1 + f (n + M) x) S sequentially"
+ by (auto simp: uniformly_convergent_on_def)
+ have cont': "continuous_on A S"
+ by (intro uniform_limit_theorem[OF _ S] always_eventually ballI allI continuous_intros cont) auto
+
+ have "uniform_limit A (\<lambda>N x. (\<Prod>n<M. 1 + f n x) * (\<Prod>n<N. 1 + f (n + M) x)) (\<lambda>x. (\<Prod>n<M. 1 + f n x) * S x) sequentially"
+ proof (rule uniform_lim_mult[OF uniform_limit_const S])
+ show "bounded (S ` A)"
+ by (intro compact_imp_bounded compact_continuous_image A cont')
+ show "bounded ((\<lambda>x. \<Prod>n<M. 1 + f n x) ` A)"
+ by (intro compact_imp_bounded compact_continuous_image A continuous_intros cont)
+ qed
+ hence "uniformly_convergent_on A (\<lambda>N x. (\<Prod>n<M. 1 + f n x) * (\<Prod>n<N. 1 + f (n + M) x))"
+ by (auto simp: uniformly_convergent_on_def)
+ also have "(\<lambda>N x. (\<Prod>n<M. 1 + f n x) * (\<Prod>n<N. 1 + f (n + M) x)) = (\<lambda>N x. (\<Prod>n<M+N. 1 + f n x))"
+ proof (intro ext)
+ fix N :: nat and x :: complex
+ have "(\<Prod>n<N. 1 + f (n + M) x) = (\<Prod>n\<in>{M..<M+N}. 1 + f n x)"
+ by (intro prod.reindex_bij_witness[of _ "\<lambda>n. n - M" "\<lambda>n. n + M"]) auto
+ also have "(\<Prod>n<M. 1 + f n x) * \<dots> = (\<Prod>n\<in>{..<M}\<union>{M..<M+N}. 1 + f n x)"
+ by (subst prod.union_disjoint) auto
+ also have "{..<M} \<union> {M..<M+N} = {..<M+N}"
+ by auto
+ finally show "(\<Prod>n<M. 1 + f n x) * (\<Prod>n<N. 1 + f (n + M) x) = (\<Prod>n<M+N. 1 + f n x)" .
+ qed
+ finally have "uniformly_convergent_on A (\<lambda>N x. \<Prod>n<M + N. 1 + f n x)"
+ by simp
+ hence "uniformly_convergent_on A (\<lambda>N x. \<Prod>n<M + (N - M). 1 + f n x)"
+ by (rule uniformly_convergent_on_compose) (rule filterlim_minus_const_nat_at_top)
+ also have "?this \<longleftrightarrow> ?thesis"
+ proof (rule uniformly_convergent_cong)
+ show "eventually (\<lambda>x. \<forall>y\<in>A. (\<Prod>n<M + (x - M). 1 + f n y) = (\<Prod>n<x. 1 + f n y)) at_top"
+ using eventually_ge_at_top[of M] by eventually_elim auto
+ qed auto
+ finally show ?thesis .
+qed
+
+lemma uniformly_convergent_on_prod':
+ fixes f :: "nat \<Rightarrow> complex \<Rightarrow> complex"
+ assumes cont: "\<And>n. continuous_on A (f n)"
+ assumes A: "compact A"
+ assumes conv_sum: "uniformly_convergent_on A (\<lambda>N x. \<Sum>n<N. norm (f n x - 1))"
+ shows "uniformly_convergent_on A (\<lambda>N x. \<Prod>n<N. f n x)"
+proof -
+ have "uniformly_convergent_on A (\<lambda>N x. \<Prod>n<N. 1 + (f n x - 1))"
+ by (rule uniformly_convergent_on_prod) (use assms in \<open>auto intro!: continuous_intros\<close>)
+ thus ?thesis
+ by simp
+qed
+
subsection\<open>The Argument of a Complex Number\<close>
text\<open>Unlike in HOL Light, it's defined for the same interval as the complex logarithm: \<open>(-\<pi>,\<pi>]\<close>.\<close>
@@ -2623,7 +2876,6 @@
qed
qed
-
subsection\<^marker>\<open>tag unimportant\<close>\<open>Some Limits involving Logarithms\<close>
lemma lim_Ln_over_power:
--- a/src/HOL/Analysis/Infinite_Products.thy Tue Dec 20 19:43:55 2022 +0100
+++ b/src/HOL/Analysis/Infinite_Products.thy Tue Dec 20 22:24:36 2022 +0000
@@ -118,6 +118,48 @@
shows "f has_prod s \<Longrightarrow> s = prodinf f"
by (simp add: has_prod_unique2 prodinf_def the_equality)
+lemma has_prod_eq_0_iff:
+ fixes f :: "nat \<Rightarrow> 'a :: {semidom, comm_semiring_1, t2_space}"
+ assumes "f has_prod P"
+ shows "P = 0 \<longleftrightarrow> 0 \<in> range f"
+proof
+ assume "0 \<in> range f"
+ then obtain N where N: "f N = 0"
+ by auto
+ have "eventually (\<lambda>n. n > N) at_top"
+ by (rule eventually_gt_at_top)
+ hence "eventually (\<lambda>n. (\<Prod>k<n. f k) = 0) at_top"
+ by eventually_elim (use N in auto)
+ hence "(\<lambda>n. \<Prod>k<n. f k) \<longlonglongrightarrow> 0"
+ by (simp add: tendsto_eventually)
+ moreover have "(\<lambda>n. \<Prod>k<n. f k) \<longlonglongrightarrow> P"
+ using assms by (metis N calculation prod_defs(2) raw_has_prod_eq_0 zero_le)
+ ultimately show "P = 0"
+ using tendsto_unique by force
+qed (use assms in \<open>auto simp: has_prod_def\<close>)
+
+lemma has_prod_0D:
+ fixes f :: "nat \<Rightarrow> 'a :: {semidom, comm_semiring_1, t2_space}"
+ shows "f has_prod 0 \<Longrightarrow> 0 \<in> range f"
+ using has_prod_eq_0_iff[of f 0] by auto
+
+lemma has_prod_zeroI:
+ fixes f :: "nat \<Rightarrow> 'a :: {semidom, comm_semiring_1, t2_space}"
+ assumes "f has_prod P" "f n = 0"
+ shows "P = 0"
+ using assms by (auto simp: has_prod_eq_0_iff)
+
+lemma raw_has_prod_in_Reals:
+ assumes "raw_has_prod (complex_of_real \<circ> z) M p"
+ shows "p \<in> \<real>"
+ using assms by (auto simp: raw_has_prod_def real_lim_sequentially)
+
+lemma raw_has_prod_of_real_iff: "raw_has_prod (complex_of_real \<circ> z) M (of_real p) \<longleftrightarrow> raw_has_prod z M p"
+ by (auto simp: raw_has_prod_def tendsto_of_real_iff simp flip: of_real_prod)
+
+lemma convergent_prod_of_real_iff: "convergent_prod (complex_of_real \<circ> z) \<longleftrightarrow> convergent_prod z"
+ by (smt (verit, best) Reals_cases convergent_prod_def raw_has_prod_in_Reals raw_has_prod_of_real_iff)
+
lemma convergent_prod_altdef:
fixes f :: "nat \<Rightarrow> 'a :: {t2_space,comm_semiring_1}"
shows "convergent_prod f \<longleftrightarrow> (\<exists>M L. (\<forall>n\<ge>M. f n \<noteq> 0) \<and> (\<lambda>n. \<Prod>i\<le>n. f (i+M)) \<longlonglongrightarrow> L \<and> L \<noteq> 0)"
@@ -1394,6 +1436,25 @@
shows "(\<Prod>n. f (Suc n)) = prodinf f / f 0"
using prodinf_split_initial_segment[of 1] assms by simp
+lemma has_prod_ignore_initial_segment':
+ assumes "convergent_prod f"
+ shows "f has_prod ((\<Prod>k<n. f k) * (\<Prod>k. f (k + n)))"
+proof (cases "\<exists>k<n. f k = 0")
+ case True
+ hence [simp]: "(\<Prod>k<n. f k) = 0"
+ by (meson finite_lessThan lessThan_iff prod_zero)
+ thus ?thesis using True assms
+ by (metis convergent_prod_has_prod_iff has_prod_zeroI mult_not_zero)
+next
+ case False
+ hence "(\<lambda>i. f (i + n)) has_prod (prodinf f / prod f {..<n})"
+ using assms by (intro has_prod_split_initial_segment) (auto simp: convergent_prod_has_prod_iff)
+ hence "prodinf f = prod f {..<n} * (\<Prod>k. f (k + n))"
+ using False by (simp add: has_prod_iff divide_simps mult_ac)
+ thus ?thesis
+ using assms by (simp add: convergent_prod_has_prod_iff)
+qed
+
end
context
@@ -1745,53 +1806,29 @@
assumes z: "summable (\<lambda>k. norm (z k))" and non0: "\<And>k. z k \<noteq> -1"
shows "convergent_prod (\<lambda>k. 1 + z k)"
proof -
- note if_cong [cong] power_Suc [simp del]
- obtain N where N: "\<And>k. k\<ge>N \<Longrightarrow> norm (z k) < 1/2"
+ obtain N where "\<And>k. k\<ge>N \<Longrightarrow> norm (z k) < 1/2"
using summable_LIMSEQ_zero [OF z]
by (metis diff_zero dist_norm half_gt_zero_iff less_numeral_extra(1) lim_sequentially tendsto_norm_zero_iff)
- have "norm (Ln (1 + z k)) \<le> 2 * norm (z k)" if "k \<ge> N" for k
- proof (cases "z k = 0")
- case False
- let ?f = "\<lambda>i. cmod ((- 1) ^ i * z k ^ i / of_nat (Suc i))"
- have normf: "norm (?f n) \<le> (1 / 2) ^ n" for n
- proof -
- have "norm (?f n) = cmod (z k) ^ n / cmod (1 + of_nat n)"
- by (auto simp: norm_divide norm_mult norm_power)
- also have "\<dots> \<le> cmod (z k) ^ n"
- by (auto simp: field_split_simps mult_le_cancel_left1 in_Reals_norm)
- also have "\<dots> \<le> (1 / 2) ^ n"
- using N [OF that] by (simp add: power_mono)
- finally show "norm (?f n) \<le> (1 / 2) ^ n" .
- qed
- have summablef: "summable ?f"
- by (intro normf summable_comparison_test' [OF summable_geometric [of "1/2"]]) auto
- have "(\<lambda>n. (- 1) ^ Suc n / of_nat n * z k ^ n) sums Ln (1 + z k)"
- using Ln_series [of "z k"] N that by fastforce
- then have *: "(\<lambda>i. z k * (((- 1) ^ i * z k ^ i) / (Suc i))) sums Ln (1 + z k)"
- using sums_split_initial_segment [where n= 1] by (force simp: power_Suc mult_ac)
- then have "norm (Ln (1 + z k)) = norm (suminf (\<lambda>i. z k * (((- 1) ^ i * z k ^ i) / (Suc i))))"
- using sums_unique by force
- also have "\<dots> = norm (z k * suminf (\<lambda>i. ((- 1) ^ i * z k ^ i) / (Suc i)))"
- apply (subst suminf_mult)
- using * False
- by (auto simp: sums_summable intro: summable_mult_D [of "z k"])
- also have "\<dots> = norm (z k) * norm (suminf (\<lambda>i. ((- 1) ^ i * z k ^ i) / (Suc i)))"
- by (simp add: norm_mult)
- also have "\<dots> \<le> norm (z k) * suminf (\<lambda>i. norm (((- 1) ^ i * z k ^ i) / (Suc i)))"
- by (intro mult_left_mono summable_norm summablef) auto
- also have "\<dots> \<le> norm (z k) * suminf (\<lambda>i. (1/2) ^ i)"
- by (intro mult_left_mono suminf_le) (use summable_geometric [of "1/2"] summablef normf in auto)
- also have "\<dots> \<le> norm (z k) * 2"
- using suminf_geometric [of "1/2::real"] by simp
- finally show ?thesis
- by (simp add: mult_ac)
- qed simp
then have "summable (\<lambda>k. Ln (1 + z k))"
- by (metis summable_comparison_test summable_mult z)
+ by (metis norm_Ln_le summable_comparison_test summable_mult z)
with non0 show ?thesis
by (simp add: add_eq_0_iff convergent_prod_iff_summable_complex)
qed
+corollary summable_imp_convergent_prod_real:
+ fixes z :: "nat \<Rightarrow> real"
+ assumes z: "summable (\<lambda>k. \<bar>z k\<bar>)" and non0: "\<And>k. z k \<noteq> -1"
+ shows "convergent_prod (\<lambda>k. 1 + z k)"
+proof -
+ have "\<And>k. (complex_of_real \<circ> z) k \<noteq> - 1"
+ by (metis non0 o_apply of_real_1 of_real_eq_iff of_real_minus)
+ with z
+ have "convergent_prod (\<lambda>k. 1 + (complex_of_real \<circ> z) k)"
+ by (auto intro: summable_imp_convergent_prod_complex)
+ then show ?thesis
+ using convergent_prod_of_real_iff [of "\<lambda>k. 1 + z k"] by (simp add: o_def)
+qed
+
lemma summable_Ln_complex:
fixes z :: "nat \<Rightarrow> complex"
assumes "convergent_prod z" "\<And>k. z k \<noteq> 0"
--- a/src/HOL/Analysis/Uniform_Limit.thy Tue Dec 20 19:43:55 2022 +0100
+++ b/src/HOL/Analysis/Uniform_Limit.thy Tue Dec 20 22:24:36 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>
--- a/src/HOL/Complex.thy Tue Dec 20 19:43:55 2022 +0100
+++ b/src/HOL/Complex.thy Tue Dec 20 22:24:36 2022 +0000
@@ -6,7 +6,7 @@
section \<open>Complex Numbers: Rectangular and Polar Representations\<close>
theory Complex
-imports Transcendental
+imports Transcendental Real_Vector_Spaces
begin
text \<open>
@@ -196,6 +196,12 @@
lemma Im_divide_of_nat [simp]: "Im (z / of_nat n) = Im z / of_nat n"
by (cases n) (simp_all add: Im_divide field_split_simps power2_eq_square del: of_nat_Suc)
+lemma Re_inverse [simp]: "r \<in> \<real> \<Longrightarrow> Re (inverse r) = inverse (Re r)"
+ by (metis Re_complex_of_real Reals_cases of_real_inverse)
+
+lemma Im_inverse [simp]: "r \<in> \<real> \<Longrightarrow> Im (inverse r) = 0"
+ by (metis Im_complex_of_real Reals_cases of_real_inverse)
+
lemma of_real_Re [simp]: "z \<in> \<real> \<Longrightarrow> of_real (Re z) = z"
by (auto simp: Reals_def)
--- a/src/HOL/Filter.thy Tue Dec 20 19:43:55 2022 +0100
+++ b/src/HOL/Filter.thy Tue Dec 20 22:24:36 2022 +0000
@@ -1519,6 +1519,24 @@
by eventually_elim (insert n, auto)
qed
+lemma filterlim_minus_const_nat_at_top:
+ "filterlim (\<lambda>n. n - c) sequentially sequentially"
+ unfolding filterlim_at_top
+proof
+ fix a :: nat
+ show "eventually (\<lambda>n. n - c \<ge> a) at_top"
+ using eventually_ge_at_top[of "a + c"] by eventually_elim auto
+qed
+
+lemma filterlim_add_const_nat_at_top:
+ "filterlim (\<lambda>n. n + c) sequentially sequentially"
+ unfolding filterlim_at_top
+proof
+ fix a :: nat
+ show "eventually (\<lambda>n. n + c \<ge> a) at_top"
+ using eventually_ge_at_top[of a] by eventually_elim auto
+qed
+
subsection \<open>Setup \<^typ>\<open>'a filter\<close> for lifting and transfer\<close>
lemma filtermap_id [simp, id_simps]: "filtermap id = id"
--- a/src/HOL/Fun.thy Tue Dec 20 19:43:55 2022 +0100
+++ b/src/HOL/Fun.thy Tue Dec 20 22:24:36 2022 +0000
@@ -300,11 +300,17 @@
using lin [of x y] ne by (force simp: dual_order.order_iff_strict)
qed
+lemma linorder_inj_onI':
+ fixes A :: "'a :: linorder set"
+ assumes "\<And>i j. i \<in> A \<Longrightarrow> j \<in> A \<Longrightarrow> i < j \<Longrightarrow> f i \<noteq> f j"
+ shows "inj_on f A"
+ by (intro linorder_inj_onI) (auto simp add: assms)
+
lemma linorder_injI:
assumes "\<And>x y::'a::linorder. x < y \<Longrightarrow> f x \<noteq> f y"
shows "inj f"
\<comment> \<open>Courtesy of Stephan Merz\<close>
-using assms by (auto intro: linorder_inj_onI linear)
+using assms by (simp add: linorder_inj_onI')
lemma inj_on_image_Pow: "inj_on f A \<Longrightarrow>inj_on (image f) (Pow A)"
unfolding Pow_def inj_on_def by blast