equal
deleted
inserted
replaced
12 subsection\<open>Cauchy's inequality and more versions of Liouville\<close> |
12 subsection\<open>Cauchy's inequality and more versions of Liouville\<close> |
13 |
13 |
14 lemma Cauchy_higher_deriv_bound: |
14 lemma Cauchy_higher_deriv_bound: |
15 assumes holf: "f holomorphic_on (ball z r)" |
15 assumes holf: "f holomorphic_on (ball z r)" |
16 and contf: "continuous_on (cball z r) f" |
16 and contf: "continuous_on (cball z r) f" |
|
17 and fin : "\<And>w. w \<in> ball z r \<Longrightarrow> f w \<in> ball y B0" |
17 and "0 < r" and "0 < n" |
18 and "0 < r" and "0 < n" |
18 and fin : "\<And>w. w \<in> ball z r \<Longrightarrow> f w \<in> ball y B0" |
|
19 shows "norm ((deriv ^^ n) f z) \<le> (fact n) * B0 / r^n" |
19 shows "norm ((deriv ^^ n) f z) \<le> (fact n) * B0 / r^n" |
20 proof - |
20 proof - |
21 have "0 < B0" using \<open>0 < r\<close> fin [of z] |
21 have "0 < B0" using \<open>0 < r\<close> fin [of z] |
22 by (metis ball_eq_empty ex_in_conv fin not_less) |
22 by (metis ball_eq_empty ex_in_conv fin not_less) |
23 have le_B0: "\<And>w. cmod (w - z) \<le> r \<Longrightarrow> cmod (f w - y) \<le> B0" |
23 have le_B0: "\<And>w. cmod (w - z) \<le> r \<Longrightarrow> cmod (f w - y) \<le> B0" |