--- 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