Rearrangement of material in Complex_Analysis_Basics, which contained much that had nothing to do with complex analysis.
--- a/src/HOL/Analysis/Complex_Analysis_Basics.thy Tue Nov 26 08:09:44 2019 +0100
+++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy Tue Nov 26 14:32:08 2019 +0000
@@ -3,13 +3,12 @@
*)
section \<open>Complex Analysis Basics\<close>
+text \<open>Definitions of analytic and holomorphic functions, limit theorems, complex differentiation\<close>
theory Complex_Analysis_Basics
imports Derivative "HOL-Library.Nonpos_Ints"
begin
-(* TODO FIXME: A lot of the things in here have nothing to do with complex analysis *)
-
subsection\<^marker>\<open>tag unimportant\<close>\<open>General lemmas\<close>
lemma nonneg_Reals_cmod_eq_Re: "z \<in> \<real>\<^sub>\<ge>\<^sub>0 \<Longrightarrow> norm z = Re z"
@@ -38,26 +37,6 @@
shows "vector_derivative (\<lambda>z. cnj (f z)) (at x) = cnj (vector_derivative f (at x))"
using assms by (intro vector_derivative_cnj_within) auto
-lemma lambda_zero: "(\<lambda>h::'a::mult_zero. 0) = (*) 0"
- by auto
-
-lemma lambda_one: "(\<lambda>x::'a::monoid_mult. x) = (*) 1"
- by auto
-
-lemma uniformly_continuous_on_cmul_right [continuous_intros]:
- fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra"
- shows "uniformly_continuous_on s f \<Longrightarrow> uniformly_continuous_on s (\<lambda>x. f x * c)"
- using bounded_linear.uniformly_continuous_on[OF bounded_linear_mult_left] .
-
-lemma uniformly_continuous_on_cmul_left[continuous_intros]:
- fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra"
- assumes "uniformly_continuous_on s f"
- shows "uniformly_continuous_on s (\<lambda>x. c * f x)"
-by (metis assms bounded_linear.uniformly_continuous_on bounded_linear_mult_right)
-
-lemma continuous_on_norm_id [continuous_intros]: "continuous_on S norm"
- by (intro continuous_on_id continuous_on_norm)
-
lemma
shows open_halfspace_Re_lt: "open {z. Re(z) < b}"
and open_halfspace_Re_gt: "open {z. Re(z) > b}"
@@ -135,7 +114,6 @@
assumes "eventually (\<lambda>x. norm(f x) \<le> Re(g x)) F" "(g \<longlongrightarrow> 0) F" shows "(f \<longlongrightarrow> 0) F"
by (rule Lim_null_comparison[OF assms(1)] tendsto_eq_intros assms(2))+ simp
-
lemma closed_segment_same_Re:
assumes "Re a = Re b"
shows "closed_segment a b = {z. Re z = Re a \<and> Im z \<in> closed_segment (Im a) (Im b)}"
@@ -426,20 +404,6 @@
by (rule nonzero_deriv_nonconstant [of f "deriv f \<xi>" \<xi> S])
(use assms in \<open>auto simp: holomorphic_derivI\<close>)
-subsection\<^marker>\<open>tag unimportant\<close>\<open>Caratheodory characterization\<close>
-
-lemma field_differentiable_caratheodory_at:
- "f field_differentiable (at z) \<longleftrightarrow>
- (\<exists>g. (\<forall>w. f(w) - f(z) = g(w) * (w - z)) \<and> continuous (at z) g)"
- using CARAT_DERIV [of f]
- by (simp add: field_differentiable_def has_field_derivative_def)
-
-lemma field_differentiable_caratheodory_within:
- "f field_differentiable (at z within s) \<longleftrightarrow>
- (\<exists>g. (\<forall>w. f(w) - f(z) = g(w) * (w - z)) \<and> continuous (at z within s) g)"
- using DERIV_caratheodory_within [of f]
- by (simp add: field_differentiable_def has_field_derivative_def)
-
subsection\<open>Analyticity on a set\<close>
definition\<^marker>\<open>tag important\<close> analytic_on (infixl "(analytic'_on)" 50)
@@ -813,60 +777,6 @@
qed
qed
-
-lemma field_differentiable_series:
- fixes f :: "nat \<Rightarrow> 'a::{real_normed_field,banach} \<Rightarrow> 'a"
- assumes "convex S" "open S"
- assumes "\<And>n x. x \<in> S \<Longrightarrow> (f n has_field_derivative f' n x) (at x)"
- assumes "uniformly_convergent_on S (\<lambda>n x. \<Sum>i<n. f' i x)"
- assumes "x0 \<in> S" "summable (\<lambda>n. f n x0)" and x: "x \<in> S"
- shows "(\<lambda>x. \<Sum>n. f n x) field_differentiable (at x)"
-proof -
- from assms(4) obtain g' where A: "uniform_limit S (\<lambda>n x. \<Sum>i<n. f' i x) g' sequentially"
- unfolding uniformly_convergent_on_def by blast
- from x and \<open>open S\<close> have S: "at x within S = at x" by (rule at_within_open)
- have "\<exists>g. \<forall>x\<in>S. (\<lambda>n. f n x) sums g x \<and> (g has_field_derivative g' x) (at x within S)"
- by (intro has_field_derivative_series[of S f f' g' x0] assms A has_field_derivative_at_within)
- then obtain g where g: "\<And>x. x \<in> S \<Longrightarrow> (\<lambda>n. f n x) sums g x"
- "\<And>x. x \<in> S \<Longrightarrow> (g has_field_derivative g' x) (at x within S)" by blast
- from g(2)[OF x] have g': "(g has_derivative (*) (g' x)) (at x)"
- by (simp add: has_field_derivative_def S)
- have "((\<lambda>x. \<Sum>n. f n x) has_derivative (*) (g' x)) (at x)"
- by (rule has_derivative_transform_within_open[OF g' \<open>open S\<close> x])
- (insert g, auto simp: sums_iff)
- thus "(\<lambda>x. \<Sum>n. f n x) field_differentiable (at x)" unfolding differentiable_def
- by (auto simp: summable_def field_differentiable_def has_field_derivative_def)
-qed
-
-subsection\<^marker>\<open>tag unimportant\<close>\<open>Bound theorem\<close>
-
-lemma field_differentiable_bound:
- fixes S :: "'a::real_normed_field set"
- assumes cvs: "convex S"
- and df: "\<And>z. z \<in> S \<Longrightarrow> (f has_field_derivative f' z) (at z within S)"
- and dn: "\<And>z. z \<in> S \<Longrightarrow> norm (f' z) \<le> B"
- and "x \<in> S" "y \<in> S"
- shows "norm(f x - f y) \<le> B * norm(x - y)"
- apply (rule differentiable_bound [OF cvs])
- apply (erule df [unfolded has_field_derivative_def])
- apply (rule onorm_le, simp_all add: norm_mult mult_right_mono assms)
- done
-
-subsection\<^marker>\<open>tag unimportant\<close>\<open>Inverse function theorem for complex derivatives\<close>
-
-lemma has_field_derivative_inverse_basic:
- shows "DERIV f (g y) :> f' \<Longrightarrow>
- f' \<noteq> 0 \<Longrightarrow>
- continuous (at y) g \<Longrightarrow>
- open t \<Longrightarrow>
- y \<in> t \<Longrightarrow>
- (\<And>z. z \<in> t \<Longrightarrow> f (g z) = z)
- \<Longrightarrow> DERIV g y :> inverse (f')"
- unfolding has_field_derivative_def
- apply (rule has_derivative_inverse_basic)
- apply (auto simp: bounded_linear_mult_right)
- done
-
subsection\<^marker>\<open>tag unimportant\<close> \<open>Taylor on Complex Numbers\<close>
lemma sum_Suc_reindex:
@@ -1053,92 +963,4 @@
qed
-subsection\<^marker>\<open>tag unimportant\<close> \<open>Polynomal function extremal theorem, from HOL Light\<close>
-
-lemma polyfun_extremal_lemma: (*COMPLEX_POLYFUN_EXTREMAL_LEMMA in HOL Light*)
- fixes c :: "nat \<Rightarrow> 'a::real_normed_div_algebra"
- assumes "0 < e"
- shows "\<exists>M. \<forall>z. M \<le> norm(z) \<longrightarrow> norm (\<Sum>i\<le>n. c(i) * z^i) \<le> e * norm(z) ^ (Suc n)"
-proof (induct n)
- case 0 with assms
- show ?case
- apply (rule_tac x="norm (c 0) / e" in exI)
- apply (auto simp: field_simps)
- done
-next
- case (Suc n)
- obtain M where M: "\<And>z. M \<le> norm z \<Longrightarrow> norm (\<Sum>i\<le>n. c i * z^i) \<le> e * norm z ^ Suc n"
- using Suc assms by blast
- show ?case
- proof (rule exI [where x= "max M (1 + norm(c(Suc n)) / e)"], clarsimp simp del: power_Suc)
- fix z::'a
- assume z1: "M \<le> norm z" and "1 + norm (c (Suc n)) / e \<le> norm z"
- then have z2: "e + norm (c (Suc n)) \<le> e * norm z"
- using assms by (simp add: field_simps)
- have "norm (\<Sum>i\<le>n. c i * z^i) \<le> e * norm z ^ Suc n"
- using M [OF z1] by simp
- then have "norm (\<Sum>i\<le>n. c i * z^i) + norm (c (Suc n) * z ^ Suc n) \<le> e * norm z ^ Suc n + norm (c (Suc n) * z ^ Suc n)"
- by simp
- then have "norm ((\<Sum>i\<le>n. c i * z^i) + c (Suc n) * z ^ Suc n) \<le> e * norm z ^ Suc n + norm (c (Suc n) * z ^ Suc n)"
- by (blast intro: norm_triangle_le elim: )
- also have "... \<le> (e + norm (c (Suc n))) * norm z ^ Suc n"
- by (simp add: norm_power norm_mult algebra_simps)
- also have "... \<le> (e * norm z) * norm z ^ Suc n"
- by (metis z2 mult.commute mult_left_mono norm_ge_zero norm_power)
- finally show "norm ((\<Sum>i\<le>n. c i * z^i) + c (Suc n) * z ^ Suc n) \<le> e * norm z ^ Suc (Suc n)"
- by simp
- qed
-qed
-
-lemma polyfun_extremal: (*COMPLEX_POLYFUN_EXTREMAL in HOL Light*)
- fixes c :: "nat \<Rightarrow> 'a::real_normed_div_algebra"
- assumes k: "c k \<noteq> 0" "1\<le>k" and kn: "k\<le>n"
- shows "eventually (\<lambda>z. norm (\<Sum>i\<le>n. c(i) * z^i) \<ge> B) at_infinity"
-using kn
-proof (induction n)
- case 0
- then show ?case
- using k by simp
-next
- case (Suc m)
- let ?even = ?case
- show ?even
- proof (cases "c (Suc m) = 0")
- case True
- then show ?even using Suc k
- by auto (metis antisym_conv less_eq_Suc_le not_le)
- next
- case False
- then obtain M where M:
- "\<And>z. M \<le> norm z \<Longrightarrow> norm (\<Sum>i\<le>m. c i * z^i) \<le> norm (c (Suc m)) / 2 * norm z ^ Suc m"
- using polyfun_extremal_lemma [of "norm(c (Suc m)) / 2" c m] Suc
- by auto
- have "\<exists>b. \<forall>z. b \<le> norm z \<longrightarrow> B \<le> norm (\<Sum>i\<le>Suc m. c i * z^i)"
- proof (rule exI [where x="max M (max 1 (\<bar>B\<bar> / (norm(c (Suc m)) / 2)))"], clarsimp simp del: power_Suc)
- fix z::'a
- assume z1: "M \<le> norm z" "1 \<le> norm z"
- and "\<bar>B\<bar> * 2 / norm (c (Suc m)) \<le> norm z"
- then have z2: "\<bar>B\<bar> \<le> norm (c (Suc m)) * norm z / 2"
- using False by (simp add: field_simps)
- have nz: "norm z \<le> norm z ^ Suc m"
- by (metis \<open>1 \<le> norm z\<close> One_nat_def less_eq_Suc_le power_increasing power_one_right zero_less_Suc)
- have *: "\<And>y x. norm (c (Suc m)) * norm z / 2 \<le> norm y - norm x \<Longrightarrow> B \<le> norm (x + y)"
- by (metis abs_le_iff add.commute norm_diff_ineq order_trans z2)
- have "norm z * norm (c (Suc m)) + 2 * norm (\<Sum>i\<le>m. c i * z^i)
- \<le> norm (c (Suc m)) * norm z + norm (c (Suc m)) * norm z ^ Suc m"
- using M [of z] Suc z1 by auto
- also have "... \<le> 2 * (norm (c (Suc m)) * norm z ^ Suc m)"
- using nz by (simp add: mult_mono del: power_Suc)
- finally show "B \<le> norm ((\<Sum>i\<le>m. c i * z^i) + c (Suc m) * z ^ Suc m)"
- using Suc.IH
- apply (auto simp: eventually_at_infinity)
- apply (rule *)
- apply (simp add: field_simps norm_mult norm_power)
- done
- qed
- then show ?even
- by (simp add: eventually_at_infinity)
- qed
-qed
-
end
--- a/src/HOL/Analysis/Conformal_Mappings.thy Tue Nov 26 08:09:44 2019 +0100
+++ b/src/HOL/Analysis/Conformal_Mappings.thy Tue Nov 26 14:32:08 2019 +0000
@@ -386,8 +386,7 @@
have frne: "frontier (cball \<xi> r) \<noteq> {}"
using \<open>0 < r\<close> by auto
have contfr: "continuous_on (frontier (cball \<xi> r)) (\<lambda>z. norm (f z - f \<xi>))"
- apply (rule continuous_on_compose2 [OF Complex_Analysis_Basics.continuous_on_norm_id])
- using hol frsbU holomorphic_on_imp_continuous_on holomorphic_on_subset by blast+
+ by (metis continuous_on_norm continuous_on_subset frsbU hol holomorphic_on_imp_continuous_on)
obtain w where "norm (\<xi> - w) = r"
and w: "(\<And>z. norm (\<xi> - z) = r \<Longrightarrow> norm (f w - f \<xi>) \<le> norm(f z - f \<xi>))"
apply (rule bexE [OF continuous_attains_inf [OF cof frne contfr]])
--- a/src/HOL/Analysis/Derivative.thy Tue Nov 26 08:09:44 2019 +0100
+++ b/src/HOL/Analysis/Derivative.thy Tue Nov 26 14:32:08 2019 +0000
@@ -937,6 +937,18 @@
finally show ?thesis .
qed
+lemma field_differentiable_bound:
+ fixes S :: "'a::real_normed_field set"
+ assumes cvs: "convex S"
+ and df: "\<And>z. z \<in> S \<Longrightarrow> (f has_field_derivative f' z) (at z within S)"
+ and dn: "\<And>z. z \<in> S \<Longrightarrow> norm (f' z) \<le> B"
+ and "x \<in> S" "y \<in> S"
+ shows "norm(f x - f y) \<le> B * norm(x - y)"
+ apply (rule differentiable_bound [OF cvs])
+ apply (erule df [unfolded has_field_derivative_def])
+ apply (rule onorm_le, simp_all add: norm_mult mult_right_mono assms)
+ done
+
lemma
differentiable_bound_segment:
fixes f::"'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
@@ -1162,6 +1174,20 @@
qed
qed
+text\<^marker>\<open>tag unimportant\<close>\<open>Inverse function theorem for complex derivatives\<close>
+lemma has_field_derivative_inverse_basic:
+ shows "DERIV f (g y) :> f' \<Longrightarrow>
+ f' \<noteq> 0 \<Longrightarrow>
+ continuous (at y) g \<Longrightarrow>
+ open t \<Longrightarrow>
+ y \<in> t \<Longrightarrow>
+ (\<And>z. z \<in> t \<Longrightarrow> f (g z) = z)
+ \<Longrightarrow> DERIV g y :> inverse (f')"
+ unfolding has_field_derivative_def
+ apply (rule has_derivative_inverse_basic)
+ apply (auto simp: bounded_linear_mult_right)
+ done
+
text \<open>Simply rewrite that based on the domain point x.\<close>
lemma has_derivative_inverse_basic_x:
@@ -2175,6 +2201,45 @@
using exp_scaleR_has_vector_derivative_right[of A t]
by (simp add: exp_times_scaleR_commute)
+lemma field_differentiable_series:
+ fixes f :: "nat \<Rightarrow> 'a::{real_normed_field,banach} \<Rightarrow> 'a"
+ assumes "convex S" "open S"
+ assumes "\<And>n x. x \<in> S \<Longrightarrow> (f n has_field_derivative f' n x) (at x)"
+ assumes "uniformly_convergent_on S (\<lambda>n x. \<Sum>i<n. f' i x)"
+ assumes "x0 \<in> S" "summable (\<lambda>n. f n x0)" and x: "x \<in> S"
+ shows "(\<lambda>x. \<Sum>n. f n x) field_differentiable (at x)"
+proof -
+ from assms(4) obtain g' where A: "uniform_limit S (\<lambda>n x. \<Sum>i<n. f' i x) g' sequentially"
+ unfolding uniformly_convergent_on_def by blast
+ from x and \<open>open S\<close> have S: "at x within S = at x" by (rule at_within_open)
+ have "\<exists>g. \<forall>x\<in>S. (\<lambda>n. f n x) sums g x \<and> (g has_field_derivative g' x) (at x within S)"
+ by (intro has_field_derivative_series[of S f f' g' x0] assms A has_field_derivative_at_within)
+ then obtain g where g: "\<And>x. x \<in> S \<Longrightarrow> (\<lambda>n. f n x) sums g x"
+ "\<And>x. x \<in> S \<Longrightarrow> (g has_field_derivative g' x) (at x within S)" by blast
+ from g(2)[OF x] have g': "(g has_derivative (*) (g' x)) (at x)"
+ by (simp add: has_field_derivative_def S)
+ have "((\<lambda>x. \<Sum>n. f n x) has_derivative (*) (g' x)) (at x)"
+ by (rule has_derivative_transform_within_open[OF g' \<open>open S\<close> x])
+ (insert g, auto simp: sums_iff)
+ thus "(\<lambda>x. \<Sum>n. f n x) field_differentiable (at x)" unfolding differentiable_def
+ by (auto simp: summable_def field_differentiable_def has_field_derivative_def)
+qed
+
+subsubsection\<^marker>\<open>tag unimportant\<close>\<open>Caratheodory characterization\<close>
+
+lemma field_differentiable_caratheodory_at:
+ "f field_differentiable (at z) \<longleftrightarrow>
+ (\<exists>g. (\<forall>w. f(w) - f(z) = g(w) * (w - z)) \<and> continuous (at z) g)"
+ using CARAT_DERIV [of f]
+ by (simp add: field_differentiable_def has_field_derivative_def)
+
+lemma field_differentiable_caratheodory_within:
+ "f field_differentiable (at z within s) \<longleftrightarrow>
+ (\<exists>g. (\<forall>w. f(w) - f(z) = g(w) * (w - z)) \<and> continuous (at z within s) g)"
+ using DERIV_caratheodory_within [of f]
+ by (simp add: field_differentiable_def has_field_derivative_def)
+
+
subsection \<open>Field derivative\<close>
definition\<^marker>\<open>tag important\<close> deriv :: "('a \<Rightarrow> 'a::real_normed_field) \<Rightarrow> 'a \<Rightarrow> 'a" where
@@ -2236,7 +2301,6 @@
apply (rule vector_derivative_at [OF field_vector_diff_chain_at])
using assms vector_derivative_works by (auto simp: field_differentiable_derivI)
-
subsection \<open>Relation between convexity and derivative\<close>
(* TODO: Generalise to real vector spaces? *)
--- a/src/HOL/Analysis/Elementary_Normed_Spaces.thy Tue Nov 26 08:09:44 2019 +0100
+++ b/src/HOL/Analysis/Elementary_Normed_Spaces.thy Tue Nov 26 14:32:08 2019 +0000
@@ -1085,6 +1085,17 @@
unfolding dist_real_def by simp
qed
+lemma uniformly_continuous_on_cmul_right [continuous_intros]:
+ fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra"
+ shows "uniformly_continuous_on s f \<Longrightarrow> uniformly_continuous_on s (\<lambda>x. f x * c)"
+ using bounded_linear.uniformly_continuous_on[OF bounded_linear_mult_left] .
+
+lemma uniformly_continuous_on_cmul_left[continuous_intros]:
+ fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra"
+ assumes "uniformly_continuous_on s f"
+ shows "uniformly_continuous_on s (\<lambda>x. c * f x)"
+by (metis assms bounded_linear.uniformly_continuous_on bounded_linear_mult_right)
+
lemma uniformly_continuous_on_norm[continuous_intros]:
fixes f :: "'a :: metric_space \<Rightarrow> 'b :: real_normed_vector"
assumes "uniformly_continuous_on s f"
--- a/src/HOL/Limits.thy Tue Nov 26 08:09:44 2019 +0100
+++ b/src/HOL/Limits.thy Tue Nov 26 14:32:08 2019 +0000
@@ -341,6 +341,94 @@
by (intro Bseq_eq_bounded[of X B "X 0"]) (auto simp: decseq_def)
+subsubsection\<^marker>\<open>tag unimportant\<close> \<open>Polynomal function extremal theorem, from HOL Light\<close>
+
+lemma polyfun_extremal_lemma: (*COMPLEX_POLYFUN_EXTREMAL_LEMMA in HOL Light*)
+ fixes c :: "nat \<Rightarrow> 'a::real_normed_div_algebra"
+ assumes "0 < e"
+ shows "\<exists>M. \<forall>z. M \<le> norm(z) \<longrightarrow> norm (\<Sum>i\<le>n. c(i) * z^i) \<le> e * norm(z) ^ (Suc n)"
+proof (induct n)
+ case 0 with assms
+ show ?case
+ apply (rule_tac x="norm (c 0) / e" in exI)
+ apply (auto simp: field_simps)
+ done
+next
+ case (Suc n)
+ obtain M where M: "\<And>z. M \<le> norm z \<Longrightarrow> norm (\<Sum>i\<le>n. c i * z^i) \<le> e * norm z ^ Suc n"
+ using Suc assms by blast
+ show ?case
+ proof (rule exI [where x= "max M (1 + norm(c(Suc n)) / e)"], clarsimp simp del: power_Suc)
+ fix z::'a
+ assume z1: "M \<le> norm z" and "1 + norm (c (Suc n)) / e \<le> norm z"
+ then have z2: "e + norm (c (Suc n)) \<le> e * norm z"
+ using assms by (simp add: field_simps)
+ have "norm (\<Sum>i\<le>n. c i * z^i) \<le> e * norm z ^ Suc n"
+ using M [OF z1] by simp
+ then have "norm (\<Sum>i\<le>n. c i * z^i) + norm (c (Suc n) * z ^ Suc n) \<le> e * norm z ^ Suc n + norm (c (Suc n) * z ^ Suc n)"
+ by simp
+ then have "norm ((\<Sum>i\<le>n. c i * z^i) + c (Suc n) * z ^ Suc n) \<le> e * norm z ^ Suc n + norm (c (Suc n) * z ^ Suc n)"
+ by (blast intro: norm_triangle_le elim: )
+ also have "... \<le> (e + norm (c (Suc n))) * norm z ^ Suc n"
+ by (simp add: norm_power norm_mult algebra_simps)
+ also have "... \<le> (e * norm z) * norm z ^ Suc n"
+ by (metis z2 mult.commute mult_left_mono norm_ge_zero norm_power)
+ finally show "norm ((\<Sum>i\<le>n. c i * z^i) + c (Suc n) * z ^ Suc n) \<le> e * norm z ^ Suc (Suc n)"
+ by simp
+ qed
+qed
+
+lemma polyfun_extremal: (*COMPLEX_POLYFUN_EXTREMAL in HOL Light*)
+ fixes c :: "nat \<Rightarrow> 'a::real_normed_div_algebra"
+ assumes k: "c k \<noteq> 0" "1\<le>k" and kn: "k\<le>n"
+ shows "eventually (\<lambda>z. norm (\<Sum>i\<le>n. c(i) * z^i) \<ge> B) at_infinity"
+using kn
+proof (induction n)
+ case 0
+ then show ?case
+ using k by simp
+next
+ case (Suc m)
+ let ?even = ?case
+ show ?even
+ proof (cases "c (Suc m) = 0")
+ case True
+ then show ?even using Suc k
+ by auto (metis antisym_conv less_eq_Suc_le not_le)
+ next
+ case False
+ then obtain M where M:
+ "\<And>z. M \<le> norm z \<Longrightarrow> norm (\<Sum>i\<le>m. c i * z^i) \<le> norm (c (Suc m)) / 2 * norm z ^ Suc m"
+ using polyfun_extremal_lemma [of "norm(c (Suc m)) / 2" c m] Suc
+ by auto
+ have "\<exists>b. \<forall>z. b \<le> norm z \<longrightarrow> B \<le> norm (\<Sum>i\<le>Suc m. c i * z^i)"
+ proof (rule exI [where x="max M (max 1 (\<bar>B\<bar> / (norm(c (Suc m)) / 2)))"], clarsimp simp del: power_Suc)
+ fix z::'a
+ assume z1: "M \<le> norm z" "1 \<le> norm z"
+ and "\<bar>B\<bar> * 2 / norm (c (Suc m)) \<le> norm z"
+ then have z2: "\<bar>B\<bar> \<le> norm (c (Suc m)) * norm z / 2"
+ using False by (simp add: field_simps)
+ have nz: "norm z \<le> norm z ^ Suc m"
+ by (metis \<open>1 \<le> norm z\<close> One_nat_def less_eq_Suc_le power_increasing power_one_right zero_less_Suc)
+ have *: "\<And>y x. norm (c (Suc m)) * norm z / 2 \<le> norm y - norm x \<Longrightarrow> B \<le> norm (x + y)"
+ by (metis abs_le_iff add.commute norm_diff_ineq order_trans z2)
+ have "norm z * norm (c (Suc m)) + 2 * norm (\<Sum>i\<le>m. c i * z^i)
+ \<le> norm (c (Suc m)) * norm z + norm (c (Suc m)) * norm z ^ Suc m"
+ using M [of z] Suc z1 by auto
+ also have "... \<le> 2 * (norm (c (Suc m)) * norm z ^ Suc m)"
+ using nz by (simp add: mult_mono del: power_Suc)
+ finally show "B \<le> norm ((\<Sum>i\<le>m. c i * z^i) + c (Suc m) * z ^ Suc m)"
+ using Suc.IH
+ apply (auto simp: eventually_at_infinity)
+ apply (rule *)
+ apply (simp add: field_simps norm_mult norm_power)
+ done
+ qed
+ then show ?even
+ by (simp add: eventually_at_infinity)
+ qed
+qed
+
subsection \<open>Convergence to Zero\<close>
definition Zfun :: "('a \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a filter \<Rightarrow> bool"
@@ -545,6 +633,9 @@
"continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. norm (f x))"
unfolding continuous_on_def by (auto intro: tendsto_norm)
+lemma continuous_on_norm_id [continuous_intros]: "continuous_on S norm"
+ by (intro continuous_on_id continuous_on_norm)
+
lemma tendsto_norm_zero: "(f \<longlongrightarrow> 0) F \<Longrightarrow> ((\<lambda>x. norm (f x)) \<longlongrightarrow> 0) F"
by (drule tendsto_norm) simp
--- a/src/HOL/Rings.thy Tue Nov 26 08:09:44 2019 +0100
+++ b/src/HOL/Rings.thy Tue Nov 26 14:32:08 2019 +0000
@@ -128,6 +128,11 @@
end
+lemma lambda_zero: "(\<lambda>h::'a::mult_zero. 0) = (*) 0"
+ by auto
+
+lemma lambda_one: "(\<lambda>x::'a::monoid_mult. x) = (*) 1"
+ by auto
subsection \<open>Abstract divisibility\<close>
--- a/src/HOL/Set_Interval.thy Tue Nov 26 08:09:44 2019 +0100
+++ b/src/HOL/Set_Interval.thy Tue Nov 26 14:32:08 2019 +0000
@@ -1944,6 +1944,9 @@
"F g {Suc m..Suc n} = F (\<lambda>i. g(Suc i)){m..n}"
by (simp add: shift_bounds_cl_nat_ivl[where k="Suc 0", simplified])
+corollary Suc_reindex_ivl: "m \<le> n \<Longrightarrow> F g {m..n} \<^bold>* g (Suc n) = g m \<^bold>* F (\<lambda>i. g (Suc i)) {m..n}"
+ by (simp add: assoc atLeast_Suc_atMost flip: shift_bounds_cl_Suc_ivl)
+
corollary shift_bounds_Suc_ivl:
"F g {Suc m..<Suc n} = F (\<lambda>i. g(Suc i)){m..<n}"
by (simp add: shift_bounds_nat_ivl[where k="Suc 0", simplified])