equal
deleted
inserted
replaced
167 then show "norm (\<Sum>i\<le>Suc n. c i * z^i) \<le> e * norm z ^ Suc (Suc n)" using M norm1 |
167 then show "norm (\<Sum>i\<le>Suc n. c i * z^i) \<le> e * norm z ^ Suc (Suc n)" using M norm1 |
168 by (drule_tac x=z in spec) (auto simp: intro!: adhoc_norm_triangle) |
168 by (drule_tac x=z in spec) (auto simp: intro!: adhoc_norm_triangle) |
169 qed |
169 qed |
170 qed |
170 qed |
171 |
171 |
172 lemma norm_lemma_xy: "\<lbrakk>\<bar>b\<bar> + 1 \<le> norm(y) - a; norm(x) \<le> a\<rbrakk> \<Longrightarrow> b \<le> norm(x + y)" |
172 lemma norm_lemma_xy: assumes "\<bar>b\<bar> + 1 \<le> norm(y) - a" "norm(x) \<le> a" shows "b \<le> norm(x + y)" |
173 by (metis abs_add_one_not_less_self add.commute diff_le_eq dual_order.trans le_less_linear |
173 proof - |
174 norm_diff_ineq) |
174 have "b \<le> norm y - norm x" |
|
175 using assms by linarith |
|
176 then show ?thesis |
|
177 by (metis (no_types) add.commute norm_diff_ineq order_trans) |
|
178 qed |
175 |
179 |
176 lemma polyfun_extremal: |
180 lemma polyfun_extremal: |
177 fixes c :: "nat \<Rightarrow> 'a::real_normed_div_algebra" |
181 fixes c :: "nat \<Rightarrow> 'a::real_normed_div_algebra" |
178 assumes "\<exists>k. k \<noteq> 0 \<and> k \<le> n \<and> c k \<noteq> 0" |
182 assumes "\<exists>k. k \<noteq> 0 \<and> k \<le> n \<and> c k \<noteq> 0" |
179 shows "eventually (\<lambda>z. norm(\<Sum>i\<le>n. c i * z^i) \<ge> B) at_infinity" |
183 shows "eventually (\<lambda>z. norm(\<Sum>i\<le>n. c i * z^i) \<ge> B) at_infinity" |