src/HOL/Analysis/Conformal_Mappings.thy
author wenzelm
Sun Sep 18 20:33:48 2016 +0200 (2016-09-18)
changeset 63915 bab633745c7f
parent 63627 6ddb43c6b711
child 63918 6bf55e6e0b75
permissions -rw-r--r--
tuned proofs;
lp15@62408
     1
section \<open>Conformal Mappings. Consequences of Cauchy's integral theorem.\<close>
lp15@62408
     2
lp15@62408
     3
text\<open>By John Harrison et al.  Ported from HOL Light by L C Paulson (2016)\<close>
lp15@62408
     4
lp15@62540
     5
text\<open>Also Cauchy's residue theorem by Wenda Li (2016)\<close>
lp15@62540
     6
lp15@62408
     7
theory Conformal_Mappings
hoelzl@63627
     8
imports "~~/src/HOL/Analysis/Cauchy_Integral_Theorem"
lp15@62408
     9
lp15@62408
    10
begin
lp15@62408
    11
lp15@62408
    12
subsection\<open>Cauchy's inequality and more versions of Liouville\<close>
lp15@62408
    13
lp15@62408
    14
lemma Cauchy_higher_deriv_bound:
lp15@62408
    15
    assumes holf: "f holomorphic_on (ball z r)"
lp15@62408
    16
        and contf: "continuous_on (cball z r) f"
lp15@62408
    17
        and "0 < r" and "0 < n"
lp15@62408
    18
        and fin : "\<And>w. w \<in> ball z r \<Longrightarrow> f w \<in> ball y B0"
lp15@62408
    19
      shows "norm ((deriv ^^ n) f z) \<le> (fact n) * B0 / r^n"
lp15@62408
    20
proof -
lp15@62408
    21
  have "0 < B0" using \<open>0 < r\<close> fin [of z]
lp15@62408
    22
    by (metis ball_eq_empty ex_in_conv fin not_less)
lp15@62408
    23
  have le_B0: "\<And>w. cmod (w - z) \<le> r \<Longrightarrow> cmod (f w - y) \<le> B0"
lp15@62408
    24
    apply (rule continuous_on_closure_norm_le [of "ball z r" "\<lambda>w. f w - y"])
lp15@62408
    25
    apply (auto simp: \<open>0 < r\<close>  dist_norm norm_minus_commute)
lp15@62408
    26
    apply (rule continuous_intros contf)+
lp15@62408
    27
    using fin apply (simp add: dist_commute dist_norm less_eq_real_def)
lp15@62408
    28
    done
lp15@62408
    29
  have "(deriv ^^ n) f z = (deriv ^^ n) (\<lambda>w. f w) z - (deriv ^^ n) (\<lambda>w. y) z"
lp15@62408
    30
    using \<open>0 < n\<close> by simp
lp15@62408
    31
  also have "... = (deriv ^^ n) (\<lambda>w. f w - y) z"
lp15@62408
    32
    by (rule higher_deriv_diff [OF holf, symmetric]) (auto simp: \<open>0 < r\<close>)
lp15@62408
    33
  finally have "(deriv ^^ n) f z = (deriv ^^ n) (\<lambda>w. f w - y) z" .
lp15@62408
    34
  have contf': "continuous_on (cball z r) (\<lambda>u. f u - y)"
lp15@62408
    35
    by (rule contf continuous_intros)+
lp15@62408
    36
  have holf': "(\<lambda>u. (f u - y)) holomorphic_on (ball z r)"
lp15@62408
    37
    by (simp add: holf holomorphic_on_diff)
wenzelm@63040
    38
  define a where "a = (2 * pi)/(fact n)"
lp15@62408
    39
  have "0 < a"  by (simp add: a_def)
lp15@62408
    40
  have "B0/r^(Suc n)*2 * pi * r = a*((fact n)*B0/r^n)"
lp15@62408
    41
    using \<open>0 < r\<close> by (simp add: a_def divide_simps)
lp15@62408
    42
  have der_dif: "(deriv ^^ n) (\<lambda>w. f w - y) z = (deriv ^^ n) f z"
lp15@62408
    43
    using \<open>0 < r\<close> \<open>0 < n\<close>
lp15@62408
    44
    by (auto simp: higher_deriv_diff [OF holf holomorphic_on_const])
wenzelm@63589
    45
  have "norm ((2 * of_real pi * \<i>)/(fact n) * (deriv ^^ n) (\<lambda>w. f w - y) z)
lp15@62408
    46
        \<le> (B0/r^(Suc n)) * (2 * pi * r)"
lp15@62408
    47
    apply (rule has_contour_integral_bound_circlepath [of "(\<lambda>u. (f u - y)/(u - z)^(Suc n))" _ z])
lp15@62408
    48
    using Cauchy_has_contour_integral_higher_derivative_circlepath [OF contf' holf']
lp15@62408
    49
    using \<open>0 < B0\<close> \<open>0 < r\<close>
lp15@62408
    50
    apply (auto simp: norm_divide norm_mult norm_power divide_simps le_B0)
lp15@62408
    51
    done
lp15@62408
    52
  then show ?thesis
lp15@62408
    53
    using \<open>0 < r\<close>
lp15@62408
    54
    by (auto simp: norm_divide norm_mult norm_power field_simps der_dif le_B0)
lp15@62408
    55
qed
lp15@62408
    56
lp15@62408
    57
proposition Cauchy_inequality:
lp15@62408
    58
    assumes holf: "f holomorphic_on (ball \<xi> r)"
lp15@62408
    59
        and contf: "continuous_on (cball \<xi> r) f"
lp15@62408
    60
        and "0 < r"
lp15@62408
    61
        and nof: "\<And>x. norm(\<xi>-x) = r \<Longrightarrow> norm(f x) \<le> B"
lp15@62408
    62
      shows "norm ((deriv ^^ n) f \<xi>) \<le> (fact n) * B / r^n"
lp15@62408
    63
proof -
lp15@62408
    64
  obtain x where "norm (\<xi>-x) = r"
lp15@62408
    65
    by (metis abs_of_nonneg add_diff_cancel_left' \<open>0 < r\<close> diff_add_cancel
lp15@62408
    66
                 dual_order.strict_implies_order norm_of_real)
lp15@62408
    67
  then have "0 \<le> B"
lp15@62408
    68
    by (metis nof norm_not_less_zero not_le order_trans)
lp15@62408
    69
  have  "((\<lambda>u. f u / (u - \<xi>) ^ Suc n) has_contour_integral (2 * pi) * \<i> / fact n * (deriv ^^ n) f \<xi>)
lp15@62408
    70
         (circlepath \<xi> r)"
lp15@62408
    71
    apply (rule Cauchy_has_contour_integral_higher_derivative_circlepath [OF contf holf])
lp15@62408
    72
    using \<open>0 < r\<close> by simp
wenzelm@63589
    73
  then have "norm ((2 * pi * \<i>)/(fact n) * (deriv ^^ n) f \<xi>) \<le> (B / r^(Suc n)) * (2 * pi * r)"
lp15@62408
    74
    apply (rule has_contour_integral_bound_circlepath)
lp15@62408
    75
    using \<open>0 \<le> B\<close> \<open>0 < r\<close>
lp15@62408
    76
    apply (simp_all add: norm_divide norm_power nof frac_le norm_minus_commute del: power_Suc)
lp15@62408
    77
    done
lp15@62408
    78
  then show ?thesis using \<open>0 < r\<close>
lp15@62408
    79
    by (simp add: norm_divide norm_mult field_simps)
lp15@62408
    80
qed
lp15@62408
    81
lp15@62408
    82
proposition Liouville_polynomial:
lp15@62408
    83
    assumes holf: "f holomorphic_on UNIV"
lp15@62408
    84
        and nof: "\<And>z. A \<le> norm z \<Longrightarrow> norm(f z) \<le> B * norm z ^ n"
lp15@62408
    85
      shows "f \<xi> = (\<Sum>k\<le>n. (deriv^^k) f 0 / fact k * \<xi> ^ k)"
lp15@62408
    86
proof (cases rule: le_less_linear [THEN disjE])
lp15@62408
    87
  assume "B \<le> 0"
lp15@62408
    88
  then have "\<And>z. A \<le> norm z \<Longrightarrow> norm(f z) = 0"
lp15@62408
    89
    by (metis nof less_le_trans zero_less_mult_iff neqE norm_not_less_zero norm_power not_le)
lp15@62408
    90
  then have f0: "(f \<longlongrightarrow> 0) at_infinity"
lp15@62408
    91
    using Lim_at_infinity by force
lp15@62408
    92
  then have [simp]: "f = (\<lambda>w. 0)"
lp15@62408
    93
    using Liouville_weak [OF holf, of 0]
lp15@62408
    94
    by (simp add: eventually_at_infinity f0) meson
lp15@62408
    95
  show ?thesis by simp
lp15@62408
    96
next
lp15@62408
    97
  assume "0 < B"
lp15@62408
    98
  have "((\<lambda>k. (deriv ^^ k) f 0 / (fact k) * (\<xi> - 0)^k) sums f \<xi>)"
lp15@62408
    99
    apply (rule holomorphic_power_series [where r = "norm \<xi> + 1"])
lp15@62408
   100
    using holf holomorphic_on_subset apply auto
lp15@62408
   101
    done
lp15@62408
   102
  then have sumsf: "((\<lambda>k. (deriv ^^ k) f 0 / (fact k) * \<xi>^k) sums f \<xi>)" by simp
lp15@62408
   103
  have "(deriv ^^ k) f 0 / fact k * \<xi> ^ k = 0" if "k>n" for k
lp15@62408
   104
  proof (cases "(deriv ^^ k) f 0 = 0")
lp15@62408
   105
    case True then show ?thesis by simp
lp15@62408
   106
  next
lp15@62408
   107
    case False
wenzelm@63040
   108
    define w where "w = complex_of_real (fact k * B / cmod ((deriv ^^ k) f 0) + (\<bar>A\<bar> + 1))"
wenzelm@63040
   109
    have "1 \<le> abs (fact k * B / cmod ((deriv ^^ k) f 0) + (\<bar>A\<bar> + 1))"
wenzelm@63040
   110
      using \<open>0 < B\<close> by simp
wenzelm@63040
   111
    then have wge1: "1 \<le> norm w"
wenzelm@63040
   112
      by (metis norm_of_real w_def)
wenzelm@63040
   113
    then have "w \<noteq> 0" by auto
wenzelm@63040
   114
    have kB: "0 < fact k * B"
wenzelm@63040
   115
      using \<open>0 < B\<close> by simp
wenzelm@63040
   116
    then have "0 \<le> fact k * B / cmod ((deriv ^^ k) f 0)"
wenzelm@63040
   117
      by simp
wenzelm@63040
   118
    then have wgeA: "A \<le> cmod w"
wenzelm@63040
   119
      by (simp only: w_def norm_of_real)
wenzelm@63040
   120
    have "fact k * B / cmod ((deriv ^^ k) f 0) < abs (fact k * B / cmod ((deriv ^^ k) f 0) + (\<bar>A\<bar> + 1))"
wenzelm@63040
   121
      using \<open>0 < B\<close> by simp
wenzelm@63040
   122
    then have wge: "fact k * B / cmod ((deriv ^^ k) f 0) < norm w"
wenzelm@63040
   123
      by (metis norm_of_real w_def)
wenzelm@63040
   124
    then have "fact k * B / norm w < cmod ((deriv ^^ k) f 0)"
wenzelm@63040
   125
      using False by (simp add: divide_simps mult.commute split: if_split_asm)
wenzelm@63040
   126
    also have "... \<le> fact k * (B * norm w ^ n) / norm w ^ k"
wenzelm@63040
   127
      apply (rule Cauchy_inequality)
wenzelm@63040
   128
         using holf holomorphic_on_subset apply force
wenzelm@63040
   129
        using holf holomorphic_on_imp_continuous_on holomorphic_on_subset apply blast
wenzelm@63040
   130
       using \<open>w \<noteq> 0\<close> apply (simp add:)
wenzelm@63040
   131
       by (metis nof wgeA dist_0_norm dist_norm)
wenzelm@63040
   132
    also have "... = fact k * (B * 1 / cmod w ^ (k-n))"
wenzelm@63040
   133
      apply (simp only: mult_cancel_left times_divide_eq_right [symmetric])
wenzelm@63040
   134
      using \<open>k>n\<close> \<open>w \<noteq> 0\<close> \<open>0 < B\<close> apply (simp add: divide_simps semiring_normalization_rules)
wenzelm@63040
   135
      done
wenzelm@63040
   136
    also have "... = fact k * B / cmod w ^ (k-n)"
wenzelm@63040
   137
      by simp
wenzelm@63040
   138
    finally have "fact k * B / cmod w < fact k * B / cmod w ^ (k - n)" .
wenzelm@63040
   139
    then have "1 / cmod w < 1 / cmod w ^ (k - n)"
wenzelm@63040
   140
      by (metis kB divide_inverse inverse_eq_divide mult_less_cancel_left_pos)
wenzelm@63040
   141
    then have "cmod w ^ (k - n) < cmod w"
wenzelm@63040
   142
      by (metis frac_le le_less_trans norm_ge_zero norm_one not_less order_refl wge1 zero_less_one)
wenzelm@63040
   143
    with self_le_power [OF wge1] have False
wenzelm@63040
   144
      by (meson diff_is_0_eq not_gr0 not_le that)
wenzelm@63040
   145
    then show ?thesis by blast
lp15@62408
   146
  qed
lp15@62408
   147
  then have "(deriv ^^ (k + Suc n)) f 0 / fact (k + Suc n) * \<xi> ^ (k + Suc n) = 0" for k
lp15@62408
   148
    using not_less_eq by blast
lp15@62408
   149
  then have "(\<lambda>i. (deriv ^^ (i + Suc n)) f 0 / fact (i + Suc n) * \<xi> ^ (i + Suc n)) sums 0"
lp15@62408
   150
    by (rule sums_0)
lp15@62408
   151
  with sums_split_initial_segment [OF sumsf, where n = "Suc n"]
lp15@62408
   152
  show ?thesis
lp15@62408
   153
    using atLeast0AtMost lessThan_Suc_atMost sums_unique2 by fastforce
lp15@62408
   154
qed
lp15@62408
   155
lp15@62408
   156
text\<open>Every bounded entire function is a constant function.\<close>
lp15@62408
   157
theorem Liouville_theorem:
lp15@62408
   158
    assumes holf: "f holomorphic_on UNIV"
lp15@62408
   159
        and bf: "bounded (range f)"
lp15@62408
   160
    obtains c where "\<And>z. f z = c"
lp15@62408
   161
proof -
lp15@62408
   162
  obtain B where "\<And>z. cmod (f z) \<le> B"
lp15@62408
   163
    by (meson bf bounded_pos rangeI)
lp15@62408
   164
  then show ?thesis
lp15@62408
   165
    using Liouville_polynomial [OF holf, of 0 B 0, simplified] that by blast
lp15@62408
   166
qed
lp15@62408
   167
lp15@62408
   168
lp15@62408
   169
lp15@62408
   170
text\<open>A holomorphic function f has only isolated zeros unless f is 0.\<close>
lp15@62408
   171
lp15@62408
   172
proposition powser_0_nonzero:
lp15@62408
   173
  fixes a :: "nat \<Rightarrow> 'a::{real_normed_field,banach}"
lp15@62408
   174
  assumes r: "0 < r"
lp15@62408
   175
      and sm: "\<And>x. norm (x - \<xi>) < r \<Longrightarrow> (\<lambda>n. a n * (x - \<xi>) ^ n) sums (f x)"
lp15@62408
   176
      and [simp]: "f \<xi> = 0"
lp15@62408
   177
      and m0: "a m \<noteq> 0" and "m>0"
lp15@62408
   178
  obtains s where "0 < s" and "\<And>z. z \<in> cball \<xi> s - {\<xi>} \<Longrightarrow> f z \<noteq> 0"
lp15@62408
   179
proof -
lp15@62408
   180
  have "r \<le> conv_radius a"
lp15@62408
   181
    using sm sums_summable by (auto simp: le_conv_radius_iff [where \<xi>=\<xi>])
lp15@62408
   182
  obtain m where am: "a m \<noteq> 0" and az [simp]: "(\<And>n. n<m \<Longrightarrow> a n = 0)"
lp15@62408
   183
    apply (rule_tac m = "LEAST n. a n \<noteq> 0" in that)
lp15@62408
   184
    using m0
lp15@62408
   185
    apply (rule LeastI2)
lp15@62408
   186
    apply (fastforce intro:  dest!: not_less_Least)+
lp15@62408
   187
    done
wenzelm@63040
   188
  define b where "b i = a (i+m) / a m" for i
wenzelm@63040
   189
  define g where "g x = suminf (\<lambda>i. b i * (x - \<xi>) ^ i)" for x
lp15@62408
   190
  have [simp]: "b 0 = 1"
lp15@62408
   191
    by (simp add: am b_def)
lp15@62408
   192
  { fix x::'a
lp15@62408
   193
    assume "norm (x - \<xi>) < r"
lp15@62408
   194
    then have "(\<lambda>n. (a m * (x - \<xi>)^m) * (b n * (x - \<xi>)^n)) sums (f x)"
lp15@62408
   195
      using am az sm sums_zero_iff_shift [of m "(\<lambda>n. a n * (x - \<xi>) ^ n)" "f x"]
lp15@62408
   196
      by (simp add: b_def monoid_mult_class.power_add algebra_simps)
lp15@62408
   197
    then have "x \<noteq> \<xi> \<Longrightarrow> (\<lambda>n. b n * (x - \<xi>)^n) sums (f x / (a m * (x - \<xi>)^m))"
lp15@62408
   198
      using am by (simp add: sums_mult_D)
lp15@62408
   199
  } note bsums = this
lp15@62408
   200
  then have  "norm (x - \<xi>) < r \<Longrightarrow> summable (\<lambda>n. b n * (x - \<xi>)^n)" for x
lp15@62408
   201
    using sums_summable by (cases "x=\<xi>") auto
lp15@62408
   202
  then have "r \<le> conv_radius b"
lp15@62408
   203
    by (simp add: le_conv_radius_iff [where \<xi>=\<xi>])
lp15@62408
   204
  then have "r/2 < conv_radius b"
lp15@62408
   205
    using not_le order_trans r by fastforce
lp15@62408
   206
  then have "continuous_on (cball \<xi> (r/2)) g"
lp15@62408
   207
    using powser_continuous_suminf [of "r/2" b \<xi>] by (simp add: g_def)
lp15@62408
   208
  then obtain s where "s>0"  "\<And>x. \<lbrakk>norm (x - \<xi>) \<le> s; norm (x - \<xi>) \<le> r/2\<rbrakk> \<Longrightarrow> dist (g x) (g \<xi>) < 1/2"
lp15@62408
   209
    apply (rule continuous_onE [where x=\<xi> and e = "1/2"])
lp15@62408
   210
    using r apply (auto simp: norm_minus_commute dist_norm)
lp15@62408
   211
    done
lp15@62408
   212
  moreover have "g \<xi> = 1"
lp15@62408
   213
    by (simp add: g_def)
lp15@62408
   214
  ultimately have gnz: "\<And>x. \<lbrakk>norm (x - \<xi>) \<le> s; norm (x - \<xi>) \<le> r/2\<rbrakk> \<Longrightarrow> (g x) \<noteq> 0"
lp15@62408
   215
    by fastforce
lp15@62408
   216
  have "f x \<noteq> 0" if "x \<noteq> \<xi>" "norm (x - \<xi>) \<le> s" "norm (x - \<xi>) \<le> r/2" for x
lp15@62408
   217
    using bsums [of x] that gnz [of x]
lp15@62408
   218
    apply (auto simp: g_def)
lp15@62408
   219
    using r sums_iff by fastforce
lp15@62408
   220
  then show ?thesis
lp15@62408
   221
    apply (rule_tac s="min s (r/2)" in that)
lp15@62408
   222
    using \<open>0 < r\<close> \<open>0 < s\<close> by (auto simp: dist_commute dist_norm)
lp15@62408
   223
qed
lp15@62408
   224
lp15@62408
   225
proposition isolated_zeros:
lp15@62408
   226
  assumes holf: "f holomorphic_on S"
lp15@62408
   227
      and "open S" "connected S" "\<xi> \<in> S" "f \<xi> = 0" "\<beta> \<in> S" "f \<beta> \<noteq> 0"
lp15@62408
   228
  obtains r where "0 < r" "ball \<xi> r \<subseteq> S" "\<And>z. z \<in> ball \<xi> r - {\<xi>} \<Longrightarrow> f z \<noteq> 0"
lp15@62408
   229
proof -
lp15@62408
   230
  obtain r where "0 < r" and r: "ball \<xi> r \<subseteq> S"
lp15@62408
   231
    using \<open>open S\<close> \<open>\<xi> \<in> S\<close> open_contains_ball_eq by blast
lp15@62408
   232
  have powf: "((\<lambda>n. (deriv ^^ n) f \<xi> / (fact n) * (z - \<xi>)^n) sums f z)" if "z \<in> ball \<xi> r" for z
lp15@62408
   233
    apply (rule holomorphic_power_series [OF _ that])
lp15@62408
   234
    apply (rule holomorphic_on_subset [OF holf r])
lp15@62408
   235
    done
lp15@62408
   236
  obtain m where m: "(deriv ^^ m) f \<xi> / (fact m) \<noteq> 0"
lp15@62408
   237
    using holomorphic_fun_eq_0_on_connected [OF holf \<open>open S\<close> \<open>connected S\<close> _ \<open>\<xi> \<in> S\<close> \<open>\<beta> \<in> S\<close>] \<open>f \<beta> \<noteq> 0\<close>
lp15@62408
   238
    by auto
lp15@62408
   239
  then have "m \<noteq> 0" using assms(5) funpow_0 by fastforce
lp15@62408
   240
  obtain s where "0 < s" and s: "\<And>z. z \<in> cball \<xi> s - {\<xi>} \<Longrightarrow> f z \<noteq> 0"
lp15@62408
   241
    apply (rule powser_0_nonzero [OF \<open>0 < r\<close> powf \<open>f \<xi> = 0\<close> m])
lp15@62408
   242
    using \<open>m \<noteq> 0\<close> by (auto simp: dist_commute dist_norm)
lp15@62408
   243
  have "0 < min r s"  by (simp add: \<open>0 < r\<close> \<open>0 < s\<close>)
lp15@62408
   244
  then show ?thesis
lp15@62408
   245
    apply (rule that)
lp15@62408
   246
    using r s by auto
lp15@62408
   247
qed
lp15@62408
   248
lp15@62408
   249
lp15@62408
   250
proposition analytic_continuation:
lp15@62408
   251
  assumes holf: "f holomorphic_on S"
lp15@62408
   252
      and S: "open S" "connected S"
lp15@62408
   253
      and "U \<subseteq> S" "\<xi> \<in> S"
lp15@62408
   254
      and "\<xi> islimpt U"
lp15@62408
   255
      and fU0 [simp]: "\<And>z. z \<in> U \<Longrightarrow> f z = 0"
lp15@62408
   256
      and "w \<in> S"
lp15@62408
   257
    shows "f w = 0"
lp15@62408
   258
proof -
lp15@62408
   259
  obtain e where "0 < e" and e: "cball \<xi> e \<subseteq> S"
lp15@62408
   260
    using \<open>open S\<close> \<open>\<xi> \<in> S\<close> open_contains_cball_eq by blast
wenzelm@63040
   261
  define T where "T = cball \<xi> e \<inter> U"
lp15@62408
   262
  have contf: "continuous_on (closure T) f"
lp15@62408
   263
    by (metis T_def closed_cball closure_minimal e holf holomorphic_on_imp_continuous_on
lp15@62408
   264
              holomorphic_on_subset inf.cobounded1)
lp15@62408
   265
  have fT0 [simp]: "\<And>x. x \<in> T \<Longrightarrow> f x = 0"
lp15@62408
   266
    by (simp add: T_def)
lp15@62408
   267
  have "\<And>r. \<lbrakk>\<forall>e>0. \<exists>x'\<in>U. x' \<noteq> \<xi> \<and> dist x' \<xi> < e; 0 < r\<rbrakk> \<Longrightarrow> \<exists>x'\<in>cball \<xi> e \<inter> U. x' \<noteq> \<xi> \<and> dist x' \<xi> < r"
lp15@62408
   268
    by (metis \<open>0 < e\<close> IntI dist_commute less_eq_real_def mem_cball min_less_iff_conj)
lp15@62408
   269
  then have "\<xi> islimpt T" using \<open>\<xi> islimpt U\<close>
lp15@62408
   270
    by (auto simp: T_def islimpt_approachable)
lp15@62408
   271
  then have "\<xi> \<in> closure T"
lp15@62408
   272
    by (simp add: closure_def)
lp15@62408
   273
  then have "f \<xi> = 0"
lp15@62408
   274
    by (auto simp: continuous_constant_on_closure [OF contf])
lp15@62408
   275
  show ?thesis
lp15@62408
   276
    apply (rule ccontr)
lp15@62408
   277
    apply (rule isolated_zeros [OF holf \<open>open S\<close> \<open>connected S\<close> \<open>\<xi> \<in> S\<close> \<open>f \<xi> = 0\<close> \<open>w \<in> S\<close>], assumption)
lp15@62408
   278
    by (metis open_ball \<open>\<xi> islimpt T\<close> centre_in_ball fT0 insertE insert_Diff islimptE)
lp15@62408
   279
qed
lp15@62408
   280
lp15@62408
   281
lp15@62408
   282
subsection\<open>Open mapping theorem\<close>
lp15@62408
   283
lp15@62408
   284
lemma holomorphic_contract_to_zero:
lp15@62408
   285
  assumes contf: "continuous_on (cball \<xi> r) f"
lp15@62408
   286
      and holf: "f holomorphic_on ball \<xi> r"
lp15@62408
   287
      and "0 < r"
lp15@62408
   288
      and norm_less: "\<And>z. norm(\<xi> - z) = r \<Longrightarrow> norm(f \<xi>) < norm(f z)"
lp15@62408
   289
  obtains z where "z \<in> ball \<xi> r" "f z = 0"
lp15@62408
   290
proof -
lp15@62408
   291
  { assume fnz: "\<And>w. w \<in> ball \<xi> r \<Longrightarrow> f w \<noteq> 0"
lp15@62408
   292
    then have "0 < norm (f \<xi>)"
lp15@62408
   293
      by (simp add: \<open>0 < r\<close>)
lp15@62408
   294
    have fnz': "\<And>w. w \<in> cball \<xi> r \<Longrightarrow> f w \<noteq> 0"
lp15@62408
   295
      by (metis norm_less dist_norm fnz less_eq_real_def mem_ball mem_cball norm_not_less_zero norm_zero)
lp15@62408
   296
    have "frontier(cball \<xi> r) \<noteq> {}"
lp15@62408
   297
      using \<open>0 < r\<close> by simp
wenzelm@63040
   298
    define g where [abs_def]: "g z = inverse (f z)" for z
lp15@62408
   299
    have contg: "continuous_on (cball \<xi> r) g"
lp15@62408
   300
      unfolding g_def using contf continuous_on_inverse fnz' by blast
lp15@62408
   301
    have holg: "g holomorphic_on ball \<xi> r"
lp15@62408
   302
      unfolding g_def using fnz holf holomorphic_on_inverse by blast
lp15@62408
   303
    have "frontier (cball \<xi> r) \<subseteq> cball \<xi> r"
lp15@62408
   304
      by (simp add: subset_iff)
lp15@62408
   305
    then have contf': "continuous_on (frontier (cball \<xi> r)) f"
lp15@62408
   306
          and contg': "continuous_on (frontier (cball \<xi> r)) g"
lp15@62408
   307
      by (blast intro: contf contg continuous_on_subset)+
lp15@62408
   308
    have froc: "frontier(cball \<xi> r) \<noteq> {}"
lp15@62408
   309
      using \<open>0 < r\<close> by simp
lp15@62408
   310
    moreover have "continuous_on (frontier (cball \<xi> r)) (norm o f)"
lp15@62408
   311
      using contf' continuous_on_compose continuous_on_norm_id by blast
lp15@62408
   312
    ultimately obtain w where w: "w \<in> frontier(cball \<xi> r)"
lp15@62408
   313
                          and now: "\<And>x. x \<in> frontier(cball \<xi> r) \<Longrightarrow> norm (f w) \<le> norm (f x)"
lp15@62408
   314
      apply (rule bexE [OF continuous_attains_inf [OF compact_frontier [OF compact_cball]]])
lp15@62408
   315
      apply (simp add:)
lp15@62408
   316
      done
lp15@62408
   317
    then have fw: "0 < norm (f w)"
lp15@62408
   318
      by (simp add: fnz')
lp15@62408
   319
    have "continuous_on (frontier (cball \<xi> r)) (norm o g)"
lp15@62408
   320
      using contg' continuous_on_compose continuous_on_norm_id by blast
lp15@62408
   321
    then obtain v where v: "v \<in> frontier(cball \<xi> r)"
lp15@62408
   322
               and nov: "\<And>x. x \<in> frontier(cball \<xi> r) \<Longrightarrow> norm (g v) \<ge> norm (g x)"
lp15@62408
   323
      apply (rule bexE [OF continuous_attains_sup [OF compact_frontier [OF compact_cball] froc]])
lp15@62408
   324
      apply (simp add:)
lp15@62408
   325
      done
lp15@62408
   326
    then have fv: "0 < norm (f v)"
lp15@62408
   327
      by (simp add: fnz')
lp15@62408
   328
    have "norm ((deriv ^^ 0) g \<xi>) \<le> fact 0 * norm (g v) / r ^ 0"
lp15@62408
   329
      by (rule Cauchy_inequality [OF holg contg \<open>0 < r\<close>]) (simp add: dist_norm nov)
lp15@62408
   330
    then have "cmod (g \<xi>) \<le> norm (g v)"
lp15@62408
   331
      by simp
lp15@62408
   332
    with w have wr: "norm (\<xi> - w) = r" and nfw: "norm (f w) \<le> norm (f \<xi>)"
lp15@62408
   333
      apply (simp_all add: dist_norm)
lp15@62408
   334
      by (metis \<open>0 < cmod (f \<xi>)\<close> g_def less_imp_inverse_less norm_inverse not_le now order_trans v)
lp15@62408
   335
    with fw have False
lp15@62408
   336
      using norm_less by force
lp15@62408
   337
  }
lp15@62408
   338
  with that show ?thesis by blast
lp15@62408
   339
qed
lp15@62408
   340
lp15@62408
   341
lp15@62408
   342
theorem open_mapping_thm:
lp15@62408
   343
  assumes holf: "f holomorphic_on S"
lp15@62408
   344
      and S: "open S" "connected S"
lp15@62408
   345
      and "open U" "U \<subseteq> S"
lp15@62408
   346
      and fne: "~ f constant_on S"
lp15@62408
   347
    shows "open (f ` U)"
lp15@62408
   348
proof -
lp15@62408
   349
  have *: "open (f ` U)"
lp15@62408
   350
          if "U \<noteq> {}" and U: "open U" "connected U" and "f holomorphic_on U" and fneU: "\<And>x. \<exists>y \<in> U. f y \<noteq> x"
lp15@62408
   351
          for U
lp15@62408
   352
  proof (clarsimp simp: open_contains_ball)
lp15@62408
   353
    fix \<xi> assume \<xi>: "\<xi> \<in> U"
lp15@62408
   354
    show "\<exists>e>0. ball (f \<xi>) e \<subseteq> f ` U"
lp15@62408
   355
    proof -
lp15@62408
   356
      have hol: "(\<lambda>z. f z - f \<xi>) holomorphic_on U"
lp15@62408
   357
        by (rule holomorphic_intros that)+
lp15@62408
   358
      obtain s where "0 < s" and sbU: "ball \<xi> s \<subseteq> U"
lp15@62408
   359
                 and sne: "\<And>z. z \<in> ball \<xi> s - {\<xi>} \<Longrightarrow> (\<lambda>z. f z - f \<xi>) z \<noteq> 0"
lp15@62408
   360
        using isolated_zeros [OF hol U \<xi>]  by (metis fneU right_minus_eq)
lp15@62408
   361
      obtain r where "0 < r" and r: "cball \<xi> r \<subseteq> ball \<xi> s"
lp15@62408
   362
        apply (rule_tac r="s/2" in that)
lp15@62408
   363
        using \<open>0 < s\<close> by auto
lp15@62408
   364
      have "cball \<xi> r \<subseteq> U"
lp15@62408
   365
        using sbU r by blast
lp15@62408
   366
      then have frsbU: "frontier (cball \<xi> r) \<subseteq> U"
lp15@62408
   367
        using Diff_subset frontier_def order_trans by fastforce
lp15@62408
   368
      then have cof: "compact (frontier(cball \<xi> r))"
lp15@62408
   369
        by blast
lp15@62408
   370
      have frne: "frontier (cball \<xi> r) \<noteq> {}"
lp15@62408
   371
        using \<open>0 < r\<close> by auto
lp15@62408
   372
      have contfr: "continuous_on (frontier (cball \<xi> r)) (\<lambda>z. norm (f z - f \<xi>))"
lp15@62408
   373
        apply (rule continuous_on_compose2 [OF Complex_Analysis_Basics.continuous_on_norm_id])
lp15@62408
   374
        using hol frsbU holomorphic_on_imp_continuous_on holomorphic_on_subset by blast+
lp15@62408
   375
      obtain w where "norm (\<xi> - w) = r"
lp15@62408
   376
                 and w: "(\<And>z. norm (\<xi> - z) = r \<Longrightarrow> norm (f w - f \<xi>) \<le> norm(f z - f \<xi>))"
lp15@62408
   377
        apply (rule bexE [OF continuous_attains_inf [OF cof frne contfr]])
lp15@62408
   378
        apply (simp add: dist_norm)
lp15@62408
   379
        done
wenzelm@63040
   380
      moreover define \<epsilon> where "\<epsilon> \<equiv> norm (f w - f \<xi>) / 3"
lp15@62408
   381
      ultimately have "0 < \<epsilon>"
lp15@62408
   382
        using \<open>0 < r\<close> dist_complex_def r sne by auto
lp15@62408
   383
      have "ball (f \<xi>) \<epsilon> \<subseteq> f ` U"
lp15@62408
   384
      proof
lp15@62408
   385
        fix \<gamma>
lp15@62408
   386
        assume \<gamma>: "\<gamma> \<in> ball (f \<xi>) \<epsilon>"
lp15@62408
   387
        have *: "cmod (\<gamma> - f \<xi>) < cmod (\<gamma> - f z)" if "cmod (\<xi> - z) = r" for z
lp15@62408
   388
        proof -
lp15@62408
   389
          have lt: "cmod (f w - f \<xi>) / 3 < cmod (\<gamma> - f z)"
lp15@62408
   390
            using w [OF that] \<gamma>
lp15@62408
   391
            using dist_triangle2 [of "f \<xi>" "\<gamma>"  "f z"] dist_triangle2 [of "f \<xi>" "f z" \<gamma>]
lp15@62408
   392
            by (simp add: \<epsilon>_def dist_norm norm_minus_commute)
lp15@62408
   393
          show ?thesis
lp15@62408
   394
            by (metis \<epsilon>_def dist_commute dist_norm less_trans lt mem_ball \<gamma>)
lp15@62408
   395
       qed
lp15@62408
   396
       have "continuous_on (cball \<xi> r) (\<lambda>z. \<gamma> - f z)"
lp15@62408
   397
          apply (rule continuous_intros)+
lp15@62408
   398
          using \<open>cball \<xi> r \<subseteq> U\<close> \<open>f holomorphic_on U\<close>
lp15@62408
   399
          apply (blast intro: continuous_on_subset holomorphic_on_imp_continuous_on)
lp15@62408
   400
          done
lp15@62408
   401
        moreover have "(\<lambda>z. \<gamma> - f z) holomorphic_on ball \<xi> r"
lp15@62408
   402
          apply (rule holomorphic_intros)+
lp15@62408
   403
          apply (metis \<open>cball \<xi> r \<subseteq> U\<close> \<open>f holomorphic_on U\<close> holomorphic_on_subset interior_cball interior_subset)
lp15@62408
   404
          done
lp15@62408
   405
        ultimately obtain z where "z \<in> ball \<xi> r" "\<gamma> - f z = 0"
lp15@62408
   406
          apply (rule holomorphic_contract_to_zero)
lp15@62408
   407
          apply (blast intro!: \<open>0 < r\<close> *)+
lp15@62408
   408
          done
lp15@62408
   409
        then show "\<gamma> \<in> f ` U"
lp15@62408
   410
          using \<open>cball \<xi> r \<subseteq> U\<close> by fastforce
lp15@62408
   411
      qed
lp15@62408
   412
      then show ?thesis using  \<open>0 < \<epsilon>\<close> by blast
lp15@62408
   413
    qed
lp15@62408
   414
  qed
lp15@62408
   415
  have "open (f ` X)" if "X \<in> components U" for X
lp15@62408
   416
  proof -
lp15@62408
   417
    have holfU: "f holomorphic_on U"
lp15@62408
   418
      using \<open>U \<subseteq> S\<close> holf holomorphic_on_subset by blast
lp15@62408
   419
    have "X \<noteq> {}"
lp15@62408
   420
      using that by (simp add: in_components_nonempty)
lp15@62408
   421
    moreover have "open X"
lp15@62408
   422
      using that \<open>open U\<close> open_components by auto
lp15@62408
   423
    moreover have "connected X"
lp15@62408
   424
      using that in_components_maximal by blast
lp15@62408
   425
    moreover have "f holomorphic_on X"
lp15@62408
   426
      by (meson that holfU holomorphic_on_subset in_components_maximal)
lp15@62408
   427
    moreover have "\<exists>y\<in>X. f y \<noteq> x" for x
lp15@62408
   428
    proof (rule ccontr)
lp15@62408
   429
      assume not: "\<not> (\<exists>y\<in>X. f y \<noteq> x)"
lp15@62408
   430
      have "X \<subseteq> S"
lp15@62408
   431
        using \<open>U \<subseteq> S\<close> in_components_subset that by blast
lp15@62408
   432
      obtain w where w: "w \<in> X" using \<open>X \<noteq> {}\<close> by blast
lp15@62408
   433
      have wis: "w islimpt X"
lp15@62408
   434
        using w \<open>open X\<close> interior_eq by auto
lp15@62408
   435
      have hol: "(\<lambda>z. f z - x) holomorphic_on S"
lp15@62408
   436
        by (simp add: holf holomorphic_on_diff)
lp15@62408
   437
      with fne [unfolded constant_on_def] analytic_continuation [OF hol S \<open>X \<subseteq> S\<close> _ wis]
lp15@62408
   438
           not \<open>X \<subseteq> S\<close> w
lp15@62408
   439
      show False by auto
lp15@62408
   440
    qed
lp15@62408
   441
    ultimately show ?thesis
lp15@62408
   442
      by (rule *)
lp15@62408
   443
  qed
lp15@62843
   444
  then have "open (f ` \<Union>components U)"
lp15@62843
   445
    by (metis (no_types, lifting) imageE image_Union open_Union)
lp15@62408
   446
  then show ?thesis
lp15@62843
   447
    by force
lp15@62408
   448
qed
lp15@62408
   449
lp15@62408
   450
lp15@62408
   451
text\<open>No need for @{term S} to be connected. But the nonconstant condition is stronger.\<close>
lp15@62408
   452
corollary open_mapping_thm2:
lp15@62408
   453
  assumes holf: "f holomorphic_on S"
lp15@62408
   454
      and S: "open S"
lp15@62408
   455
      and "open U" "U \<subseteq> S"
lp15@62408
   456
      and fnc: "\<And>X. \<lbrakk>open X; X \<subseteq> S; X \<noteq> {}\<rbrakk> \<Longrightarrow> ~ f constant_on X"
lp15@62408
   457
    shows "open (f ` U)"
lp15@62408
   458
proof -
lp15@62843
   459
  have "S = \<Union>(components S)" by simp
lp15@62408
   460
  with \<open>U \<subseteq> S\<close> have "U = (\<Union>C \<in> components S. C \<inter> U)" by auto
lp15@62408
   461
  then have "f ` U = (\<Union>C \<in> components S. f ` (C \<inter> U))"
lp15@62843
   462
    using image_UN by fastforce
lp15@62408
   463
  moreover
lp15@62408
   464
  { fix C assume "C \<in> components S"
lp15@62408
   465
    with S \<open>C \<in> components S\<close> open_components in_components_connected
lp15@62408
   466
    have C: "open C" "connected C" by auto
lp15@62408
   467
    have "C \<subseteq> S"
lp15@62408
   468
      by (metis \<open>C \<in> components S\<close> in_components_maximal)
lp15@62408
   469
    have nf: "\<not> f constant_on C"
lp15@62408
   470
      apply (rule fnc)
lp15@62408
   471
      using C \<open>C \<subseteq> S\<close> \<open>C \<in> components S\<close> in_components_nonempty by auto
lp15@62408
   472
    have "f holomorphic_on C"
lp15@62408
   473
      by (metis holf holomorphic_on_subset \<open>C \<subseteq> S\<close>)
lp15@62408
   474
    then have "open (f ` (C \<inter> U))"
lp15@62408
   475
      apply (rule open_mapping_thm [OF _ C _ _ nf])
lp15@62408
   476
      apply (simp add: C \<open>open U\<close> open_Int, blast)
lp15@62408
   477
      done
lp15@62408
   478
  } ultimately show ?thesis
lp15@62408
   479
    by force
lp15@62408
   480
qed
lp15@62408
   481
lp15@62408
   482
corollary open_mapping_thm3:
lp15@62408
   483
  assumes holf: "f holomorphic_on S"
lp15@62408
   484
      and "open S" and injf: "inj_on f S"
lp15@62408
   485
    shows  "open (f ` S)"
lp15@62408
   486
apply (rule open_mapping_thm2 [OF holf])
lp15@62408
   487
using assms
lp15@62408
   488
apply (simp_all add:)
lp15@62408
   489
using injective_not_constant subset_inj_on by blast
lp15@62408
   490
lp15@62408
   491
lp15@62408
   492
lp15@62408
   493
subsection\<open>Maximum Modulus Principle\<close>
lp15@62408
   494
lp15@62408
   495
text\<open>If @{term f} is holomorphic, then its norm (modulus) cannot exhibit a true local maximum that is
lp15@62408
   496
   properly within the domain of @{term f}.\<close>
lp15@62408
   497
lp15@62408
   498
proposition maximum_modulus_principle:
lp15@62408
   499
  assumes holf: "f holomorphic_on S"
lp15@62408
   500
      and S: "open S" "connected S"
lp15@62408
   501
      and "open U" "U \<subseteq> S" "\<xi> \<in> U"
lp15@62408
   502
      and no: "\<And>z. z \<in> U \<Longrightarrow> norm(f z) \<le> norm(f \<xi>)"
lp15@62408
   503
    shows "f constant_on S"
lp15@62408
   504
proof (rule ccontr)
lp15@62408
   505
  assume "\<not> f constant_on S"
lp15@62408
   506
  then have "open (f ` U)"
lp15@62408
   507
    using open_mapping_thm assms by blast
lp15@62408
   508
  moreover have "~ open (f ` U)"
lp15@62408
   509
  proof -
lp15@62408
   510
    have "\<exists>t. cmod (f \<xi> - t) < e \<and> t \<notin> f ` U" if "0 < e" for e
lp15@62408
   511
      apply (rule_tac x="if 0 < Re(f \<xi>) then f \<xi> + (e/2) else f \<xi> - (e/2)" in exI)
lp15@62408
   512
      using that
lp15@62408
   513
      apply (simp add: dist_norm)
lp15@62408
   514
      apply (fastforce simp: cmod_Re_le_iff dest!: no dest: sym)
lp15@62408
   515
      done
lp15@62408
   516
    then show ?thesis
lp15@62408
   517
      unfolding open_contains_ball by (metis \<open>\<xi> \<in> U\<close> contra_subsetD dist_norm imageI mem_ball)
lp15@62408
   518
  qed
lp15@62408
   519
  ultimately show False
lp15@62408
   520
    by blast
lp15@62408
   521
qed
lp15@62408
   522
lp15@62408
   523
lp15@62408
   524
proposition maximum_modulus_frontier:
lp15@62408
   525
  assumes holf: "f holomorphic_on (interior S)"
lp15@62408
   526
      and contf: "continuous_on (closure S) f"
lp15@62408
   527
      and bos: "bounded S"
lp15@62408
   528
      and leB: "\<And>z. z \<in> frontier S \<Longrightarrow> norm(f z) \<le> B"
lp15@62408
   529
      and "\<xi> \<in> S"
lp15@62408
   530
    shows "norm(f \<xi>) \<le> B"
lp15@62408
   531
proof -
lp15@62408
   532
  have "compact (closure S)" using bos
lp15@62408
   533
    by (simp add: bounded_closure compact_eq_bounded_closed)
lp15@62408
   534
  moreover have "continuous_on (closure S) (cmod \<circ> f)"
lp15@62408
   535
    using contf continuous_on_compose continuous_on_norm_id by blast
lp15@62408
   536
  ultimately obtain z where zin: "z \<in> closure S" and z: "\<And>y. y \<in> closure S \<Longrightarrow> (cmod \<circ> f) y \<le> (cmod \<circ> f) z"
lp15@62408
   537
    using continuous_attains_sup [of "closure S" "norm o f"] \<open>\<xi> \<in> S\<close> by auto
lp15@62408
   538
  then consider "z \<in> frontier S" | "z \<in> interior S" using frontier_def by auto
lp15@62408
   539
  then have "norm(f z) \<le> B"
lp15@62408
   540
  proof cases
lp15@62408
   541
    case 1 then show ?thesis using leB by blast
lp15@62408
   542
  next
lp15@62408
   543
    case 2
lp15@62408
   544
    have zin: "z \<in> connected_component_set (interior S) z"
lp15@62408
   545
      by (simp add: 2)
lp15@62408
   546
    have "f constant_on (connected_component_set (interior S) z)"
lp15@62408
   547
      apply (rule maximum_modulus_principle [OF _ _ _ _ _ zin])
lp15@62408
   548
      apply (metis connected_component_subset holf holomorphic_on_subset)
lp15@62408
   549
      apply (simp_all add: open_connected_component)
lp15@62408
   550
      by (metis closure_subset comp_eq_dest_lhs  interior_subset subsetCE z connected_component_in)
lp15@62408
   551
    then obtain c where c: "\<And>w. w \<in> connected_component_set (interior S) z \<Longrightarrow> f w = c"
lp15@62408
   552
      by (auto simp: constant_on_def)
lp15@62408
   553
    have "f ` closure(connected_component_set (interior S) z) \<subseteq> {c}"
lp15@62408
   554
      apply (rule image_closure_subset)
lp15@62408
   555
      apply (meson closure_mono connected_component_subset contf continuous_on_subset interior_subset)
lp15@62408
   556
      using c
lp15@62408
   557
      apply auto
lp15@62408
   558
      done
lp15@62408
   559
    then have cc: "\<And>w. w \<in> closure(connected_component_set (interior S) z) \<Longrightarrow> f w = c" by blast
lp15@62408
   560
    have "frontier(connected_component_set (interior S) z) \<noteq> {}"
lp15@62408
   561
      apply (simp add: frontier_eq_empty)
lp15@62408
   562
      by (metis "2" bos bounded_interior connected_component_eq_UNIV connected_component_refl not_bounded_UNIV)
lp15@62408
   563
    then obtain w where w: "w \<in> frontier(connected_component_set (interior S) z)"
lp15@62408
   564
       by auto
lp15@62408
   565
    then have "norm (f z) = norm (f w)"  by (simp add: "2" c cc frontier_def)
lp15@62408
   566
    also have "... \<le> B"
lp15@62408
   567
      apply (rule leB)
lp15@62408
   568
      using w
lp15@62408
   569
using frontier_interior_subset frontier_of_connected_component_subset by blast
lp15@62408
   570
    finally show ?thesis .
lp15@62408
   571
  qed
lp15@62408
   572
  then show ?thesis
lp15@62408
   573
    using z \<open>\<xi> \<in> S\<close> closure_subset by fastforce
lp15@62408
   574
qed
lp15@62408
   575
lp15@62408
   576
corollary maximum_real_frontier:
lp15@62408
   577
  assumes holf: "f holomorphic_on (interior S)"
lp15@62408
   578
      and contf: "continuous_on (closure S) f"
lp15@62408
   579
      and bos: "bounded S"
lp15@62408
   580
      and leB: "\<And>z. z \<in> frontier S \<Longrightarrow> Re(f z) \<le> B"
lp15@62408
   581
      and "\<xi> \<in> S"
lp15@62408
   582
    shows "Re(f \<xi>) \<le> B"
lp15@62408
   583
using maximum_modulus_frontier [of "exp o f" S "exp B"]
lp15@62408
   584
      Transcendental.continuous_on_exp holomorphic_on_compose holomorphic_on_exp assms
lp15@62408
   585
by auto
lp15@62408
   586
lp15@62408
   587
lp15@62408
   588
subsection\<open>Factoring out a zero according to its order\<close>
lp15@62408
   589
lp15@62408
   590
lemma holomorphic_factor_order_of_zero:
lp15@62408
   591
  assumes holf: "f holomorphic_on S"
lp15@62408
   592
      and os: "open S"
lp15@62408
   593
      and "\<xi> \<in> S" "0 < n"
lp15@62408
   594
      and dnz: "(deriv ^^ n) f \<xi> \<noteq> 0"
lp15@62408
   595
      and dfz: "\<And>i. \<lbrakk>0 < i; i < n\<rbrakk> \<Longrightarrow> (deriv ^^ i) f \<xi> = 0"
lp15@62408
   596
   obtains g r where "0 < r"
lp15@62408
   597
                "g holomorphic_on ball \<xi> r"
lp15@62408
   598
                "\<And>w. w \<in> ball \<xi> r \<Longrightarrow> f w - f \<xi> = (w - \<xi>)^n * g w"
lp15@62408
   599
                "\<And>w. w \<in> ball \<xi> r \<Longrightarrow> g w \<noteq> 0"
lp15@62408
   600
proof -
lp15@62408
   601
  obtain r where "r>0" and r: "ball \<xi> r \<subseteq> S" using assms by (blast elim!: openE)
lp15@62408
   602
  then have holfb: "f holomorphic_on ball \<xi> r"
lp15@62408
   603
    using holf holomorphic_on_subset by blast
wenzelm@63040
   604
  define g where "g w = suminf (\<lambda>i. (deriv ^^ (i + n)) f \<xi> / (fact(i + n)) * (w - \<xi>)^i)" for w
lp15@62408
   605
  have sumsg: "(\<lambda>i. (deriv ^^ (i + n)) f \<xi> / (fact(i + n)) * (w - \<xi>)^i) sums g w"
lp15@62408
   606
   and feq: "f w - f \<xi> = (w - \<xi>)^n * g w"
lp15@62408
   607
       if w: "w \<in> ball \<xi> r" for w
lp15@62408
   608
  proof -
wenzelm@63040
   609
    define powf where "powf = (\<lambda>i. (deriv ^^ i) f \<xi>/(fact i) * (w - \<xi>)^i)"
lp15@62408
   610
    have sing: "{..<n} - {i. powf i = 0} = (if f \<xi> = 0 then {} else {0})"
lp15@62408
   611
      unfolding powf_def using \<open>0 < n\<close> dfz by (auto simp: dfz; metis funpow_0 not_gr0)
lp15@62408
   612
    have "powf sums f w"
lp15@62408
   613
      unfolding powf_def by (rule holomorphic_power_series [OF holfb w])
lp15@62408
   614
    moreover have "(\<Sum>i<n. powf i) = f \<xi>"
lp15@62408
   615
      apply (subst Groups_Big.comm_monoid_add_class.setsum.setdiff_irrelevant [symmetric])
lp15@62408
   616
      apply (simp add:)
lp15@62408
   617
      apply (simp only: dfz sing)
lp15@62408
   618
      apply (simp add: powf_def)
lp15@62408
   619
      done
lp15@62408
   620
    ultimately have fsums: "(\<lambda>i. powf (i+n)) sums (f w - f \<xi>)"
lp15@62408
   621
      using w sums_iff_shift' by metis
lp15@62408
   622
    then have *: "summable (\<lambda>i. (w - \<xi>) ^ n * ((deriv ^^ (i + n)) f \<xi> * (w - \<xi>) ^ i / fact (i + n)))"
lp15@62408
   623
      unfolding powf_def using sums_summable
lp15@62408
   624
      by (auto simp: power_add mult_ac)
lp15@62408
   625
    have "summable (\<lambda>i. (deriv ^^ (i + n)) f \<xi> * (w - \<xi>) ^ i / fact (i + n))"
lp15@62408
   626
    proof (cases "w=\<xi>")
lp15@62408
   627
      case False then show ?thesis
lp15@62408
   628
        using summable_mult [OF *, of "1 / (w - \<xi>) ^ n"] by (simp add:)
lp15@62408
   629
    next
lp15@62408
   630
      case True then show ?thesis
lp15@62408
   631
        by (auto simp: Power.semiring_1_class.power_0_left intro!: summable_finite [of "{0}"]
lp15@62408
   632
                 split: if_split_asm)
lp15@62408
   633
    qed
lp15@62408
   634
    then show sumsg: "(\<lambda>i. (deriv ^^ (i + n)) f \<xi> / (fact(i + n)) * (w - \<xi>)^i) sums g w"
lp15@62408
   635
      by (simp add: summable_sums_iff g_def)
lp15@62408
   636
    show "f w - f \<xi> = (w - \<xi>)^n * g w"
lp15@62408
   637
      apply (rule sums_unique2)
lp15@62408
   638
      apply (rule fsums [unfolded powf_def])
lp15@62408
   639
      using sums_mult [OF sumsg, of "(w - \<xi>) ^ n"]
lp15@62408
   640
      by (auto simp: power_add mult_ac)
lp15@62408
   641
  qed
lp15@62408
   642
  then have holg: "g holomorphic_on ball \<xi> r"
lp15@62408
   643
    by (meson sumsg power_series_holomorphic)
lp15@62408
   644
  then have contg: "continuous_on (ball \<xi> r) g"
lp15@62408
   645
    by (blast intro: holomorphic_on_imp_continuous_on)
lp15@62408
   646
  have "g \<xi> \<noteq> 0"
lp15@62408
   647
    using dnz unfolding g_def
lp15@62408
   648
    by (subst suminf_finite [of "{0}"]) auto
lp15@62408
   649
  obtain d where "0 < d" and d: "\<And>w. w \<in> ball \<xi> d \<Longrightarrow> g w \<noteq> 0"
lp15@62408
   650
    apply (rule exE [OF continuous_on_avoid [OF contg _ \<open>g \<xi> \<noteq> 0\<close>]])
lp15@62408
   651
    using \<open>0 < r\<close>
lp15@62408
   652
    apply force
lp15@62408
   653
    by (metis \<open>0 < r\<close> less_trans mem_ball not_less_iff_gr_or_eq)
lp15@62408
   654
  show ?thesis
lp15@62408
   655
    apply (rule that [where g=g and r ="min r d"])
lp15@62408
   656
    using \<open>0 < r\<close> \<open>0 < d\<close> holg
lp15@62408
   657
    apply (auto simp: feq holomorphic_on_subset subset_ball d)
lp15@62408
   658
    done
lp15@62408
   659
qed
lp15@62408
   660
lp15@62408
   661
lp15@62408
   662
lemma holomorphic_factor_order_of_zero_strong:
lp15@62408
   663
  assumes holf: "f holomorphic_on S" "open S"  "\<xi> \<in> S" "0 < n"
lp15@62408
   664
      and "(deriv ^^ n) f \<xi> \<noteq> 0"
lp15@62408
   665
      and "\<And>i. \<lbrakk>0 < i; i < n\<rbrakk> \<Longrightarrow> (deriv ^^ i) f \<xi> = 0"
lp15@62408
   666
   obtains g r where "0 < r"
lp15@62408
   667
                "g holomorphic_on ball \<xi> r"
lp15@62408
   668
                "\<And>w. w \<in> ball \<xi> r \<Longrightarrow> f w - f \<xi> = ((w - \<xi>) * g w) ^ n"
lp15@62408
   669
                "\<And>w. w \<in> ball \<xi> r \<Longrightarrow> g w \<noteq> 0"
lp15@62408
   670
proof -
lp15@62408
   671
  obtain g r where "0 < r"
lp15@62408
   672
               and holg: "g holomorphic_on ball \<xi> r"
lp15@62408
   673
               and feq: "\<And>w. w \<in> ball \<xi> r \<Longrightarrow> f w - f \<xi> = (w - \<xi>)^n * g w"
lp15@62408
   674
               and gne: "\<And>w. w \<in> ball \<xi> r \<Longrightarrow> g w \<noteq> 0"
lp15@62408
   675
    by (auto intro: holomorphic_factor_order_of_zero [OF assms])
lp15@62408
   676
  have con: "continuous_on (ball \<xi> r) (\<lambda>z. deriv g z / g z)"
lp15@62408
   677
    by (rule continuous_intros) (auto simp: gne holg holomorphic_deriv holomorphic_on_imp_continuous_on)
lp15@62534
   678
  have cd: "\<And>x. dist \<xi> x < r \<Longrightarrow> (\<lambda>z. deriv g z / g z) field_differentiable at x"
lp15@62408
   679
    apply (rule derivative_intros)+
lp15@62408
   680
    using holg mem_ball apply (blast intro: holomorphic_deriv holomorphic_on_imp_differentiable_at)
lp15@62408
   681
    apply (metis Topology_Euclidean_Space.open_ball at_within_open holg holomorphic_on_def mem_ball)
lp15@62408
   682
    using gne mem_ball by blast
lp15@62408
   683
  obtain h where h: "\<And>x. x \<in> ball \<xi> r \<Longrightarrow> (h has_field_derivative deriv g x / g x) (at x)"
lp15@62408
   684
    apply (rule exE [OF holomorphic_convex_primitive [of "ball \<xi> r" "{}" "\<lambda>z. deriv g z / g z"]])
lp15@62408
   685
    apply (auto simp: con cd)
lp15@62408
   686
    apply (metis open_ball at_within_open mem_ball)
lp15@62408
   687
    done
lp15@62408
   688
  then have "continuous_on (ball \<xi> r) h"
lp15@62408
   689
    by (metis open_ball holomorphic_on_imp_continuous_on holomorphic_on_open)
lp15@62408
   690
  then have con: "continuous_on (ball \<xi> r) (\<lambda>x. exp (h x) / g x)"
lp15@62408
   691
    by (auto intro!: continuous_intros simp add: holg holomorphic_on_imp_continuous_on gne)
lp15@62408
   692
  have 0: "dist \<xi> x < r \<Longrightarrow> ((\<lambda>x. exp (h x) / g x) has_field_derivative 0) (at x)" for x
lp15@62408
   693
    apply (rule h derivative_eq_intros | simp)+
lp15@62534
   694
    apply (rule DERIV_deriv_iff_field_differentiable [THEN iffD2])
lp15@62408
   695
    using holg apply (auto simp: holomorphic_on_imp_differentiable_at gne h)
lp15@62408
   696
    done
lp15@62408
   697
  obtain c where c: "\<And>x. x \<in> ball \<xi> r \<Longrightarrow> exp (h x) / g x = c"
lp15@62408
   698
    by (rule DERIV_zero_connected_constant [of "ball \<xi> r" "{}" "\<lambda>x. exp(h x) / g x"]) (auto simp: con 0)
lp15@62408
   699
  have hol: "(\<lambda>z. exp ((Ln (inverse c) + h z) / of_nat n)) holomorphic_on ball \<xi> r"
lp15@62408
   700
    apply (rule holomorphic_on_compose [unfolded o_def, where g = exp])
lp15@62408
   701
    apply (rule holomorphic_intros)+
lp15@62408
   702
    using h holomorphic_on_open apply blast
lp15@62408
   703
    apply (rule holomorphic_intros)+
lp15@62408
   704
    using \<open>0 < n\<close> apply (simp add:)
lp15@62408
   705
    apply (rule holomorphic_intros)+
lp15@62408
   706
    done
lp15@62408
   707
  show ?thesis
lp15@62408
   708
    apply (rule that [where g="\<lambda>z. exp((Ln(inverse c) + h z)/n)" and r =r])
lp15@62408
   709
    using \<open>0 < r\<close> \<open>0 < n\<close>
lp15@62408
   710
    apply (auto simp: feq power_mult_distrib exp_divide_power_eq c [symmetric])
lp15@62408
   711
    apply (rule hol)
lp15@62408
   712
    apply (simp add: Transcendental.exp_add gne)
lp15@62408
   713
    done
lp15@62408
   714
qed
lp15@62408
   715
lp15@62408
   716
lp15@62408
   717
lemma
lp15@62408
   718
  fixes k :: "'a::wellorder"
lp15@62408
   719
  assumes a_def: "a == LEAST x. P x" and P: "P k"
lp15@62408
   720
  shows def_LeastI: "P a" and def_Least_le: "a \<le> k"
lp15@62408
   721
unfolding a_def
lp15@62408
   722
by (rule LeastI Least_le; rule P)+
lp15@62408
   723
lp15@62408
   724
lemma holomorphic_factor_zero_nonconstant:
lp15@62408
   725
  assumes holf: "f holomorphic_on S" and S: "open S" "connected S"
lp15@62408
   726
      and "\<xi> \<in> S" "f \<xi> = 0"
lp15@62408
   727
      and nonconst: "\<And>c. \<exists>z \<in> S. f z \<noteq> c"
lp15@62408
   728
   obtains g r n
lp15@62408
   729
      where "0 < n"  "0 < r"  "ball \<xi> r \<subseteq> S"
lp15@62408
   730
            "g holomorphic_on ball \<xi> r"
lp15@62408
   731
            "\<And>w. w \<in> ball \<xi> r \<Longrightarrow> f w = (w - \<xi>)^n * g w"
lp15@62408
   732
            "\<And>w. w \<in> ball \<xi> r \<Longrightarrow> g w \<noteq> 0"
lp15@62408
   733
proof (cases "\<forall>n>0. (deriv ^^ n) f \<xi> = 0")
lp15@62408
   734
  case True then show ?thesis
lp15@62408
   735
    using holomorphic_fun_eq_const_on_connected [OF holf S _ \<open>\<xi> \<in> S\<close>] nonconst by auto
lp15@62408
   736
next
lp15@62408
   737
  case False
lp15@62408
   738
  then obtain n0 where "n0 > 0" and n0: "(deriv ^^ n0) f \<xi> \<noteq> 0" by blast
lp15@62408
   739
  obtain r0 where "r0 > 0" "ball \<xi> r0 \<subseteq> S" using S openE \<open>\<xi> \<in> S\<close> by auto
wenzelm@63040
   740
  define n where "n \<equiv> LEAST n. (deriv ^^ n) f \<xi> \<noteq> 0"
lp15@62408
   741
  have n_ne: "(deriv ^^ n) f \<xi> \<noteq> 0"
lp15@62408
   742
    by (rule def_LeastI [OF n_def]) (rule n0)
lp15@62408
   743
  then have "0 < n" using \<open>f \<xi> = 0\<close>
lp15@62408
   744
    using funpow_0 by fastforce
lp15@62408
   745
  have n_min: "\<And>k. k < n \<Longrightarrow> (deriv ^^ k) f \<xi> = 0"
lp15@62408
   746
    using def_Least_le [OF n_def] not_le by blast
lp15@62408
   747
  then obtain g r1
lp15@62408
   748
    where  "0 < r1" "g holomorphic_on ball \<xi> r1"
lp15@62408
   749
           "\<And>w. w \<in> ball \<xi> r1 \<Longrightarrow> f w = (w - \<xi>) ^ n * g w"
lp15@62408
   750
           "\<And>w. w \<in> ball \<xi> r1 \<Longrightarrow> g w \<noteq> 0"
lp15@62408
   751
    by (auto intro: holomorphic_factor_order_of_zero [OF holf \<open>open S\<close> \<open>\<xi> \<in> S\<close> \<open>n > 0\<close> n_ne] simp: \<open>f \<xi> = 0\<close>)
lp15@62408
   752
  then show ?thesis
lp15@62408
   753
    apply (rule_tac g=g and r="min r0 r1" and n=n in that)
lp15@62408
   754
    using \<open>0 < n\<close> \<open>0 < r0\<close> \<open>0 < r1\<close> \<open>ball \<xi> r0 \<subseteq> S\<close>
lp15@62408
   755
    apply (auto simp: subset_ball intro: holomorphic_on_subset)
lp15@62408
   756
    done
lp15@62408
   757
qed
lp15@62408
   758
lp15@62408
   759
lp15@62408
   760
lemma holomorphic_lower_bound_difference:
lp15@62408
   761
  assumes holf: "f holomorphic_on S" and S: "open S" "connected S"
lp15@62408
   762
      and "\<xi> \<in> S" and "\<phi> \<in> S"
lp15@62408
   763
      and fne: "f \<phi> \<noteq> f \<xi>"
lp15@62408
   764
   obtains k n r
lp15@62408
   765
      where "0 < k"  "0 < r"
lp15@62408
   766
            "ball \<xi> r \<subseteq> S"
lp15@62408
   767
            "\<And>w. w \<in> ball \<xi> r \<Longrightarrow> k * norm(w - \<xi>)^n \<le> norm(f w - f \<xi>)"
lp15@62408
   768
proof -
wenzelm@63040
   769
  define n where "n = (LEAST n. 0 < n \<and> (deriv ^^ n) f \<xi> \<noteq> 0)"
lp15@62408
   770
  obtain n0 where "0 < n0" and n0: "(deriv ^^ n0) f \<xi> \<noteq> 0"
lp15@62408
   771
    using fne holomorphic_fun_eq_const_on_connected [OF holf S] \<open>\<xi> \<in> S\<close> \<open>\<phi> \<in> S\<close> by blast
lp15@62408
   772
  then have "0 < n" and n_ne: "(deriv ^^ n) f \<xi> \<noteq> 0"
lp15@62408
   773
    unfolding n_def by (metis (mono_tags, lifting) LeastI)+
lp15@62408
   774
  have n_min: "\<And>k. \<lbrakk>0 < k; k < n\<rbrakk> \<Longrightarrow> (deriv ^^ k) f \<xi> = 0"
lp15@62408
   775
    unfolding n_def by (blast dest: not_less_Least)
lp15@62408
   776
  then obtain g r
lp15@62408
   777
    where "0 < r" and holg: "g holomorphic_on ball \<xi> r"
lp15@62408
   778
      and fne: "\<And>w. w \<in> ball \<xi> r \<Longrightarrow> f w - f \<xi> = (w - \<xi>) ^ n * g w"
lp15@62408
   779
      and gnz: "\<And>w. w \<in> ball \<xi> r \<Longrightarrow> g w \<noteq> 0"
lp15@62408
   780
      by (auto intro: holomorphic_factor_order_of_zero  [OF holf \<open>open S\<close> \<open>\<xi> \<in> S\<close> \<open>n > 0\<close> n_ne])
lp15@62408
   781
  obtain e where "e>0" and e: "ball \<xi> e \<subseteq> S" using assms by (blast elim!: openE)
lp15@62408
   782
  then have holfb: "f holomorphic_on ball \<xi> e"
lp15@62408
   783
    using holf holomorphic_on_subset by blast
wenzelm@63040
   784
  define d where "d = (min e r) / 2"
lp15@62408
   785
  have "0 < d" using \<open>0 < r\<close> \<open>0 < e\<close> by (simp add: d_def)
lp15@62408
   786
  have "d < r"
lp15@62408
   787
    using \<open>0 < r\<close> by (auto simp: d_def)
lp15@62408
   788
  then have cbb: "cball \<xi> d \<subseteq> ball \<xi> r"
lp15@62408
   789
    by (auto simp: cball_subset_ball_iff)
lp15@62408
   790
  then have "g holomorphic_on cball \<xi> d"
lp15@62408
   791
    by (rule holomorphic_on_subset [OF holg])
lp15@62408
   792
  then have "closed (g ` cball \<xi> d)"
lp15@62408
   793
    by (simp add: compact_imp_closed compact_continuous_image holomorphic_on_imp_continuous_on)
lp15@62408
   794
  moreover have "g ` cball \<xi> d \<noteq> {}"
lp15@62408
   795
    using \<open>0 < d\<close> by auto
lp15@62408
   796
  ultimately obtain x where x: "x \<in> g ` cball \<xi> d" and "\<And>y. y \<in> g ` cball \<xi> d \<Longrightarrow> dist 0 x \<le> dist 0 y"
lp15@62408
   797
    by (rule distance_attains_inf) blast
lp15@62408
   798
  then have leg: "\<And>w. w \<in> cball \<xi> d \<Longrightarrow> norm x \<le> norm (g w)"
lp15@62408
   799
    by auto
lp15@62408
   800
  have "ball \<xi> d \<subseteq> cball \<xi> d" by auto
lp15@62408
   801
  also have "... \<subseteq> ball \<xi> e" using \<open>0 < d\<close> d_def by auto
lp15@62408
   802
  also have "... \<subseteq> S" by (rule e)
lp15@62408
   803
  finally have dS: "ball \<xi> d \<subseteq> S" .
lp15@62408
   804
  moreover have "x \<noteq> 0" using gnz x \<open>d < r\<close> by auto
lp15@62408
   805
  ultimately show ?thesis
lp15@62408
   806
    apply (rule_tac k="norm x" and n=n and r=d in that)
lp15@62408
   807
    using \<open>d < r\<close> leg
lp15@62408
   808
    apply (auto simp: \<open>0 < d\<close> fne norm_mult norm_power algebra_simps mult_right_mono)
lp15@62408
   809
    done
lp15@62408
   810
qed
lp15@62408
   811
lp15@62408
   812
lemma
lp15@62408
   813
  assumes holf: "f holomorphic_on (S - {\<xi>})" and \<xi>: "\<xi> \<in> interior S"
lp15@62408
   814
    shows holomorphic_on_extend_lim:
lp15@62408
   815
          "(\<exists>g. g holomorphic_on S \<and> (\<forall>z \<in> S - {\<xi>}. g z = f z)) \<longleftrightarrow>
lp15@62408
   816
           ((\<lambda>z. (z - \<xi>) * f z) \<longlongrightarrow> 0) (at \<xi>)"
lp15@62408
   817
          (is "?P = ?Q")
lp15@62408
   818
     and holomorphic_on_extend_bounded:
lp15@62408
   819
          "(\<exists>g. g holomorphic_on S \<and> (\<forall>z \<in> S - {\<xi>}. g z = f z)) \<longleftrightarrow>
lp15@62408
   820
           (\<exists>B. eventually (\<lambda>z. norm(f z) \<le> B) (at \<xi>))"
lp15@62408
   821
          (is "?P = ?R")
lp15@62408
   822
proof -
lp15@62408
   823
  obtain \<delta> where "0 < \<delta>" and \<delta>: "ball \<xi> \<delta> \<subseteq> S"
lp15@62408
   824
    using \<xi> mem_interior by blast
lp15@62408
   825
  have "?R" if holg: "g holomorphic_on S" and gf: "\<And>z. z \<in> S - {\<xi>} \<Longrightarrow> g z = f z" for g
lp15@62408
   826
  proof -
lp15@62408
   827
    have *: "\<forall>\<^sub>F z in at \<xi>. dist (g z) (g \<xi>) < 1 \<longrightarrow> cmod (f z) \<le> cmod (g \<xi>) + 1"
lp15@62408
   828
      apply (simp add: eventually_at)
lp15@62408
   829
      apply (rule_tac x="\<delta>" in exI)
lp15@62408
   830
      using \<delta> \<open>0 < \<delta>\<close>
lp15@62408
   831
      apply (clarsimp simp:)
lp15@62408
   832
      apply (drule_tac c=x in subsetD)
lp15@62408
   833
      apply (simp add: dist_commute)
lp15@62408
   834
      by (metis DiffI add.commute diff_le_eq dist_norm gf le_less_trans less_eq_real_def norm_triangle_ineq2 singletonD)
lp15@62408
   835
    have "continuous_on (interior S) g"
lp15@62408
   836
      by (meson continuous_on_subset holg holomorphic_on_imp_continuous_on interior_subset)
lp15@62408
   837
    then have "\<And>x. x \<in> interior S \<Longrightarrow> (g \<longlongrightarrow> g x) (at x)"
lp15@62408
   838
      using continuous_on_interior continuous_within holg holomorphic_on_imp_continuous_on by blast
lp15@62408
   839
    then have "(g \<longlongrightarrow> g \<xi>) (at \<xi>)"
lp15@62408
   840
      by (simp add: \<xi>)
lp15@62408
   841
    then show ?thesis
lp15@62408
   842
      apply (rule_tac x="norm(g \<xi>) + 1" in exI)
lp15@62408
   843
      apply (rule eventually_mp [OF * tendstoD [where e=1]], auto)
lp15@62408
   844
      done
lp15@62408
   845
  qed
lp15@62408
   846
  moreover have "?Q" if "\<forall>\<^sub>F z in at \<xi>. cmod (f z) \<le> B" for B
lp15@62408
   847
    by (rule lim_null_mult_right_bounded [OF _ that]) (simp add: LIM_zero)
lp15@62408
   848
  moreover have "?P" if "(\<lambda>z. (z - \<xi>) * f z) \<midarrow>\<xi>\<rightarrow> 0"
lp15@62408
   849
  proof -
wenzelm@63040
   850
    define h where [abs_def]: "h z = (z - \<xi>)^2 * f z" for z
lp15@62408
   851
    have h0: "(h has_field_derivative 0) (at \<xi>)"
lp15@62408
   852
      apply (simp add: h_def Derivative.DERIV_within_iff)
lp15@62408
   853
      apply (rule Lim_transform_within [OF that, of 1])
lp15@62408
   854
      apply (auto simp: divide_simps power2_eq_square)
lp15@62408
   855
      done
lp15@62408
   856
    have holh: "h holomorphic_on S"
lp15@62408
   857
    proof (simp add: holomorphic_on_def, clarify)
lp15@62408
   858
      fix z assume "z \<in> S"
lp15@62534
   859
      show "h field_differentiable at z within S"
lp15@62408
   860
      proof (cases "z = \<xi>")
lp15@62408
   861
        case True then show ?thesis
lp15@62534
   862
          using field_differentiable_at_within field_differentiable_def h0 by blast
lp15@62408
   863
      next
lp15@62408
   864
        case False
lp15@62534
   865
        then have "f field_differentiable at z within S"
lp15@62408
   866
          using holomorphic_onD [OF holf, of z] \<open>z \<in> S\<close>
lp15@62534
   867
          unfolding field_differentiable_def DERIV_within_iff
lp15@62408
   868
          by (force intro: exI [where x="dist \<xi> z"] elim: Lim_transform_within_set [unfolded eventually_at])
lp15@62408
   869
        then show ?thesis
lp15@62408
   870
          by (simp add: h_def power2_eq_square derivative_intros)
lp15@62408
   871
      qed
lp15@62408
   872
    qed
wenzelm@63040
   873
    define g where [abs_def]: "g z = (if z = \<xi> then deriv h \<xi> else (h z - h \<xi>) / (z - \<xi>))" for z
lp15@62408
   874
    have holg: "g holomorphic_on S"
lp15@62408
   875
      unfolding g_def by (rule pole_lemma [OF holh \<xi>])
lp15@62408
   876
    show ?thesis
lp15@62408
   877
      apply (rule_tac x="\<lambda>z. if z = \<xi> then deriv g \<xi> else (g z - g \<xi>)/(z - \<xi>)" in exI)
lp15@62408
   878
      apply (rule conjI)
lp15@62408
   879
      apply (rule pole_lemma [OF holg \<xi>])
lp15@62408
   880
      apply (auto simp: g_def power2_eq_square divide_simps)
lp15@62408
   881
      using h0 apply (simp add: h0 DERIV_imp_deriv h_def power2_eq_square)
lp15@62408
   882
      done
lp15@62408
   883
  qed
lp15@62408
   884
  ultimately show "?P = ?Q" and "?P = ?R"
lp15@62408
   885
    by meson+
lp15@62408
   886
qed
lp15@62408
   887
lp15@62408
   888
lp15@62408
   889
proposition pole_at_infinity:
lp15@62408
   890
  assumes holf: "f holomorphic_on UNIV" and lim: "((inverse o f) \<longlongrightarrow> l) at_infinity"
lp15@62408
   891
  obtains a n where "\<And>z. f z = (\<Sum>i\<le>n. a i * z^i)"
lp15@62408
   892
proof (cases "l = 0")
lp15@62408
   893
  case False
lp15@62408
   894
  with tendsto_inverse [OF lim] show ?thesis
lp15@62408
   895
    apply (rule_tac a="(\<lambda>n. inverse l)" and n=0 in that)
lp15@62408
   896
    apply (simp add: Liouville_weak [OF holf, of "inverse l"])
lp15@62408
   897
    done
lp15@62408
   898
next
lp15@62408
   899
  case True
lp15@62408
   900
  then have [simp]: "l = 0" .
lp15@62408
   901
  show ?thesis
lp15@62408
   902
  proof (cases "\<exists>r. 0 < r \<and> (\<forall>z \<in> ball 0 r - {0}. f(inverse z) \<noteq> 0)")
lp15@62408
   903
    case True
lp15@62408
   904
      then obtain r where "0 < r" and r: "\<And>z. z \<in> ball 0 r - {0} \<Longrightarrow> f(inverse z) \<noteq> 0"
lp15@62408
   905
             by auto
lp15@62408
   906
      have 1: "inverse \<circ> f \<circ> inverse holomorphic_on ball 0 r - {0}"
lp15@62408
   907
        by (rule holomorphic_on_compose holomorphic_intros holomorphic_on_subset [OF holf] | force simp: r)+
lp15@62408
   908
      have 2: "0 \<in> interior (ball 0 r)"
lp15@62408
   909
        using \<open>0 < r\<close> by simp
lp15@62408
   910
      have "\<exists>B. 0<B \<and> eventually (\<lambda>z. cmod ((inverse \<circ> f \<circ> inverse) z) \<le> B) (at 0)"
lp15@62408
   911
        apply (rule exI [where x=1])
lp15@62408
   912
        apply (simp add:)
lp15@62408
   913
        using tendstoD [OF lim [unfolded lim_at_infinity_0] zero_less_one]
lp15@62408
   914
        apply (rule eventually_mono)
lp15@62408
   915
        apply (simp add: dist_norm)
lp15@62408
   916
        done
lp15@62408
   917
      with holomorphic_on_extend_bounded [OF 1 2]
lp15@62408
   918
      obtain g where holg: "g holomorphic_on ball 0 r"
lp15@62408
   919
                 and geq: "\<And>z. z \<in> ball 0 r - {0} \<Longrightarrow> g z = (inverse \<circ> f \<circ> inverse) z"
lp15@62408
   920
        by meson
lp15@62408
   921
      have ifi0: "(inverse \<circ> f \<circ> inverse) \<midarrow>0\<rightarrow> 0"
lp15@62408
   922
        using \<open>l = 0\<close> lim lim_at_infinity_0 by blast
lp15@62408
   923
      have g2g0: "g \<midarrow>0\<rightarrow> g 0"
lp15@62408
   924
        using \<open>0 < r\<close> centre_in_ball continuous_at continuous_on_eq_continuous_at holg
lp15@62408
   925
        by (blast intro: holomorphic_on_imp_continuous_on)
lp15@62408
   926
      have g2g1: "g \<midarrow>0\<rightarrow> 0"
lp15@62408
   927
        apply (rule Lim_transform_within_open [OF ifi0 open_ball [of 0 r]])
lp15@62408
   928
        using \<open>0 < r\<close> by (auto simp: geq)
lp15@62408
   929
      have [simp]: "g 0 = 0"
lp15@62408
   930
        by (rule tendsto_unique [OF _ g2g0 g2g1]) simp
lp15@62408
   931
      have "ball 0 r - {0::complex} \<noteq> {}"
lp15@62408
   932
        using \<open>0 < r\<close>
lp15@62408
   933
        apply (clarsimp simp: ball_def dist_norm)
lp15@62408
   934
        apply (drule_tac c="of_real r/2" in subsetD, auto)
lp15@62408
   935
        done
lp15@62408
   936
      then obtain w::complex where "w \<noteq> 0" and w: "norm w < r" by force
lp15@62408
   937
      then have "g w \<noteq> 0" by (simp add: geq r)
lp15@62408
   938
      obtain B n e where "0 < B" "0 < e" "e \<le> r"
lp15@62408
   939
                     and leg: "\<And>w. norm w < e \<Longrightarrow> B * cmod w ^ n \<le> cmod (g w)"
lp15@62408
   940
        apply (rule holomorphic_lower_bound_difference [OF holg open_ball connected_ball, of 0 w])
lp15@62408
   941
        using \<open>0 < r\<close> w \<open>g w \<noteq> 0\<close> by (auto simp: ball_subset_ball_iff)
lp15@62408
   942
      have "cmod (f z) \<le> cmod z ^ n / B" if "2/e \<le> cmod z" for z
lp15@62408
   943
      proof -
lp15@62408
   944
        have ize: "inverse z \<in> ball 0 e - {0}" using that \<open>0 < e\<close>
lp15@62408
   945
          by (auto simp: norm_divide divide_simps algebra_simps)
lp15@62408
   946
        then have [simp]: "z \<noteq> 0" and izr: "inverse z \<in> ball 0 r - {0}" using  \<open>e \<le> r\<close>
lp15@62408
   947
          by auto
lp15@62408
   948
        then have [simp]: "f z \<noteq> 0"
lp15@62408
   949
          using r [of "inverse z"] by simp
lp15@62408
   950
        have [simp]: "f z = inverse (g (inverse z))"
lp15@62408
   951
          using izr geq [of "inverse z"] by simp
lp15@62408
   952
        show ?thesis using ize leg [of "inverse z"]  \<open>0 < B\<close>  \<open>0 < e\<close>
lp15@62408
   953
          by (simp add: divide_simps norm_divide algebra_simps)
lp15@62408
   954
      qed
lp15@62408
   955
      then show ?thesis
lp15@62408
   956
        apply (rule_tac a = "\<lambda>k. (deriv ^^ k) f 0 / (fact k)" and n=n in that)
lp15@62408
   957
        apply (rule_tac A = "2/e" and B = "1/B" in Liouville_polynomial [OF holf])
lp15@62408
   958
        apply (simp add:)
lp15@62408
   959
        done
lp15@62408
   960
  next
lp15@62408
   961
    case False
lp15@62408
   962
    then have fi0: "\<And>r. r > 0 \<Longrightarrow> \<exists>z\<in>ball 0 r - {0}. f (inverse z) = 0"
lp15@62408
   963
      by simp
lp15@62408
   964
    have fz0: "f z = 0" if "0 < r" and lt1: "\<And>x. x \<noteq> 0 \<Longrightarrow> cmod x < r \<Longrightarrow> inverse (cmod (f (inverse x))) < 1"
lp15@62408
   965
              for z r
lp15@62408
   966
    proof -
lp15@62408
   967
      have f0: "(f \<longlongrightarrow> 0) at_infinity"
lp15@62408
   968
      proof -
wenzelm@62837
   969
        have DIM_complex[intro]: "2 \<le> DIM(complex)"  \<comment>\<open>should not be necessary!\<close>
lp15@62408
   970
          by simp
lp15@62408
   971
        have "continuous_on (inverse ` (ball 0 r - {0})) f"
lp15@62408
   972
          using continuous_on_subset holf holomorphic_on_imp_continuous_on by blast
lp15@62408
   973
        then have "connected ((f \<circ> inverse) ` (ball 0 r - {0}))"
lp15@62408
   974
          apply (intro connected_continuous_image continuous_intros)
lp15@62408
   975
          apply (force intro: connected_punctured_ball)+
lp15@62408
   976
          done
lp15@62408
   977
        then have "\<lbrakk>w \<noteq> 0; cmod w < r\<rbrakk> \<Longrightarrow> f (inverse w) = 0" for w
lp15@62408
   978
          apply (rule disjE [OF connected_closedD [where A = "{0}" and B = "- ball 0 1"]], auto)
lp15@62408
   979
          apply (metis (mono_tags, hide_lams) not_less_iff_gr_or_eq one_less_inverse lt1 zero_less_norm_iff)
lp15@62408
   980
          using False \<open>0 < r\<close> apply fastforce
lp15@62408
   981
          by (metis (no_types, hide_lams) Compl_iff IntI comp_apply empty_iff image_eqI insert_Diff_single insert_iff mem_ball_0 not_less_iff_gr_or_eq one_less_inverse that(2) zero_less_norm_iff)
lp15@62408
   982
        then show ?thesis
lp15@62408
   983
          apply (simp add: lim_at_infinity_0)
lp15@62408
   984
          apply (rule Lim_eventually)
lp15@62408
   985
          apply (simp add: eventually_at)
lp15@62408
   986
          apply (rule_tac x=r in exI)
lp15@62408
   987
          apply (simp add: \<open>0 < r\<close> dist_norm)
lp15@62408
   988
          done
lp15@62408
   989
      qed
lp15@62408
   990
      obtain w where "w \<in> ball 0 r - {0}" and "f (inverse w) = 0"
lp15@62408
   991
        using False \<open>0 < r\<close> by blast
lp15@62408
   992
      then show ?thesis
lp15@62408
   993
        by (auto simp: f0 Liouville_weak [OF holf, of 0])
lp15@62408
   994
    qed
lp15@62408
   995
    show ?thesis
lp15@62408
   996
      apply (rule that [of "\<lambda>n. 0" 0])
lp15@62408
   997
      using lim [unfolded lim_at_infinity_0]
lp15@62408
   998
      apply (simp add: Lim_at dist_norm norm_inverse)
lp15@62408
   999
      apply (drule_tac x=1 in spec)
lp15@62408
  1000
      using fz0 apply auto
lp15@62408
  1001
      done
lp15@62408
  1002
    qed
lp15@62408
  1003
qed
lp15@62408
  1004
lp15@62408
  1005
lp15@62408
  1006
subsection\<open>Entire proper functions are precisely the non-trivial polynomials\<close>
lp15@62408
  1007
lp15@62408
  1008
proposition proper_map_polyfun:
lp15@62408
  1009
    fixes c :: "nat \<Rightarrow> 'a::{real_normed_div_algebra,heine_borel}"
lp15@62408
  1010
  assumes "closed S" and "compact K" and c: "c i \<noteq> 0" "1 \<le> i" "i \<le> n"
lp15@62408
  1011
    shows "compact (S \<inter> {z. (\<Sum>i\<le>n. c i * z^i) \<in> K})"
lp15@62408
  1012
proof -
lp15@62408
  1013
  obtain B where "B > 0" and B: "\<And>x. x \<in> K \<Longrightarrow> norm x \<le> B"
lp15@62408
  1014
    by (metis compact_imp_bounded \<open>compact K\<close> bounded_pos)
lp15@62408
  1015
  have *: "norm x \<le> b"
lp15@62408
  1016
            if "\<And>x. b \<le> norm x \<Longrightarrow> B + 1 \<le> norm (\<Sum>i\<le>n. c i * x ^ i)"
lp15@62408
  1017
               "(\<Sum>i\<le>n. c i * x ^ i) \<in> K"  for b x
lp15@62408
  1018
  proof -
lp15@62408
  1019
    have "norm (\<Sum>i\<le>n. c i * x ^ i) \<le> B"
lp15@62408
  1020
      using B that by blast
lp15@62408
  1021
    moreover have "\<not> B + 1 \<le> B"
lp15@62408
  1022
      by simp
lp15@62408
  1023
    ultimately show "norm x \<le> b"
lp15@62408
  1024
      using that by (metis (no_types) less_eq_real_def not_less order_trans)
lp15@62408
  1025
  qed
lp15@62408
  1026
  have "bounded {z. (\<Sum>i\<le>n. c i * z ^ i) \<in> K}"
lp15@62408
  1027
    using polyfun_extremal [where c=c and B="B+1", OF c]
lp15@62408
  1028
    by (auto simp: bounded_pos eventually_at_infinity_pos *)
lp15@62408
  1029
  moreover have "closed {z. (\<Sum>i\<le>n. c i * z ^ i) \<in> K}"
lp15@62408
  1030
    apply (rule allI continuous_closed_preimage_univ continuous_intros)+
lp15@62408
  1031
    using \<open>compact K\<close> compact_eq_bounded_closed by blast
lp15@62408
  1032
  ultimately show ?thesis
lp15@62843
  1033
    using closed_Int_compact [OF \<open>closed S\<close>] compact_eq_bounded_closed by blast
lp15@62408
  1034
qed
lp15@62408
  1035
lp15@62408
  1036
corollary proper_map_polyfun_univ:
lp15@62408
  1037
    fixes c :: "nat \<Rightarrow> 'a::{real_normed_div_algebra,heine_borel}"
lp15@62408
  1038
  assumes "compact K" "c i \<noteq> 0" "1 \<le> i" "i \<le> n"
lp15@62408
  1039
    shows "compact ({z. (\<Sum>i\<le>n. c i * z^i) \<in> K})"
lp15@62408
  1040
using proper_map_polyfun [of UNIV K c i n] assms by simp
lp15@62408
  1041
lp15@62408
  1042
lp15@62408
  1043
proposition proper_map_polyfun_eq:
lp15@62408
  1044
  assumes "f holomorphic_on UNIV"
lp15@62408
  1045
    shows "(\<forall>k. compact k \<longrightarrow> compact {z. f z \<in> k}) \<longleftrightarrow>
lp15@62408
  1046
           (\<exists>c n. 0 < n \<and> (c n \<noteq> 0) \<and> f = (\<lambda>z. \<Sum>i\<le>n. c i * z^i))"
lp15@62408
  1047
          (is "?lhs = ?rhs")
lp15@62408
  1048
proof
lp15@62408
  1049
  assume compf [rule_format]: ?lhs
lp15@62408
  1050
  have 2: "\<exists>k. 0 < k \<and> a k \<noteq> 0 \<and> f = (\<lambda>z. \<Sum>i \<le> k. a i * z ^ i)"
lp15@62408
  1051
        if "\<And>z. f z = (\<Sum>i\<le>n. a i * z ^ i)" for a n
lp15@62408
  1052
  proof (cases "\<forall>i\<le>n. 0<i \<longrightarrow> a i = 0")
lp15@62408
  1053
    case True
lp15@62408
  1054
    then have [simp]: "\<And>z. f z = a 0"
lp15@62408
  1055
      by (simp add: that setsum_atMost_shift)
lp15@62408
  1056
    have False using compf [of "{a 0}"] by simp
lp15@62408
  1057
    then show ?thesis ..
lp15@62408
  1058
  next
lp15@62408
  1059
    case False
lp15@62408
  1060
    then obtain k where k: "0 < k" "k\<le>n" "a k \<noteq> 0" by force
wenzelm@63040
  1061
    define m where "m = (GREATEST k. k\<le>n \<and> a k \<noteq> 0)"
lp15@62408
  1062
    have m: "m\<le>n \<and> a m \<noteq> 0"
lp15@62408
  1063
      unfolding m_def
lp15@62408
  1064
      apply (rule GreatestI [where b = "Suc n"])
lp15@62408
  1065
      using k apply auto
lp15@62408
  1066
      done
lp15@62408
  1067
    have [simp]: "a i = 0" if "m < i" "i \<le> n" for i
lp15@62408
  1068
      using Greatest_le [where b = "Suc n" and P = "\<lambda>k. k\<le>n \<and> a k \<noteq> 0"]
lp15@62408
  1069
      using m_def not_le that by auto
lp15@62408
  1070
    have "k \<le> m"
lp15@62408
  1071
      unfolding m_def
lp15@62408
  1072
      apply (rule Greatest_le [where b = "Suc n"])
lp15@62408
  1073
      using k apply auto
lp15@62408
  1074
      done
lp15@62408
  1075
    with k m show ?thesis
lp15@62408
  1076
      by (rule_tac x=m in exI) (auto simp: that comm_monoid_add_class.setsum.mono_neutral_right)
lp15@62408
  1077
  qed
lp15@62408
  1078
  have "((inverse \<circ> f) \<longlongrightarrow> 0) at_infinity"
lp15@62408
  1079
  proof (rule Lim_at_infinityI)
lp15@62408
  1080
    fix e::real assume "0 < e"
lp15@62408
  1081
    with compf [of "cball 0 (inverse e)"]
lp15@62408
  1082
    show "\<exists>B. \<forall>x. B \<le> cmod x \<longrightarrow> dist ((inverse \<circ> f) x) 0 \<le> e"
lp15@62408
  1083
      apply (simp add:)
lp15@62408
  1084
      apply (clarsimp simp add: compact_eq_bounded_closed bounded_pos norm_inverse)
lp15@62408
  1085
      apply (rule_tac x="b+1" in exI)
lp15@62408
  1086
      apply (metis inverse_inverse_eq less_add_same_cancel2 less_imp_inverse_less add.commute not_le not_less_iff_gr_or_eq order_trans zero_less_one)
lp15@62408
  1087
      done
lp15@62408
  1088
  qed
lp15@62408
  1089
  then show ?rhs
lp15@62408
  1090
    apply (rule pole_at_infinity [OF assms])
lp15@62408
  1091
    using 2 apply blast
lp15@62408
  1092
    done
lp15@62408
  1093
next
lp15@62408
  1094
  assume ?rhs
lp15@62408
  1095
  then obtain c n where "0 < n" "c n \<noteq> 0" "f = (\<lambda>z. \<Sum>i\<le>n. c i * z ^ i)" by blast
lp15@62408
  1096
  then have "compact {z. f z \<in> k}" if "compact k" for k
lp15@62408
  1097
    by (auto intro: proper_map_polyfun_univ [OF that])
lp15@62408
  1098
  then show ?lhs by blast
lp15@62408
  1099
qed
lp15@62408
  1100
lp15@62408
  1101
lp15@62408
  1102
subsection\<open>Relating invertibility and nonvanishing of derivative\<close>
lp15@62408
  1103
lp15@62408
  1104
proposition has_complex_derivative_locally_injective:
lp15@62408
  1105
  assumes holf: "f holomorphic_on S"
lp15@62408
  1106
      and S: "\<xi> \<in> S" "open S"
lp15@62408
  1107
      and dnz: "deriv f \<xi> \<noteq> 0"
lp15@62408
  1108
  obtains r where "r > 0" "ball \<xi> r \<subseteq> S" "inj_on f (ball \<xi> r)"
lp15@62408
  1109
proof -
lp15@62408
  1110
  have *: "\<exists>d>0. \<forall>x. dist \<xi> x < d \<longrightarrow> onorm (\<lambda>v. deriv f x * v - deriv f \<xi> * v) < e" if "e > 0" for e
lp15@62408
  1111
  proof -
lp15@62408
  1112
    have contdf: "continuous_on S (deriv f)"
lp15@62408
  1113
      by (simp add: holf holomorphic_deriv holomorphic_on_imp_continuous_on \<open>open S\<close>)
lp15@62408
  1114
    obtain \<delta> where "\<delta>>0" and \<delta>: "\<And>x. \<lbrakk>x \<in> S; dist x \<xi> \<le> \<delta>\<rbrakk> \<Longrightarrow> cmod (deriv f x - deriv f \<xi>) \<le> e/2"
lp15@62408
  1115
      using continuous_onE [OF contdf \<open>\<xi> \<in> S\<close>, of "e/2"] \<open>0 < e\<close>
lp15@62408
  1116
      by (metis dist_complex_def half_gt_zero less_imp_le)
lp15@62408
  1117
    obtain \<epsilon> where "\<epsilon>>0" "ball \<xi> \<epsilon> \<subseteq> S"
lp15@62408
  1118
      by (metis openE [OF \<open>open S\<close> \<open>\<xi> \<in> S\<close>])
lp15@62408
  1119
    with \<open>\<delta>>0\<close> have "\<exists>\<delta>>0. \<forall>x. dist \<xi> x < \<delta> \<longrightarrow> onorm (\<lambda>v. deriv f x * v - deriv f \<xi> * v) \<le> e/2"
lp15@62408
  1120
      apply (rule_tac x="min \<delta> \<epsilon>" in exI)
lp15@62408
  1121
      apply (intro conjI allI impI Operator_Norm.onorm_le)
lp15@62408
  1122
      apply (simp add:)
lp15@62408
  1123
      apply (simp only: Rings.ring_class.left_diff_distrib [symmetric] norm_mult)
lp15@62408
  1124
      apply (rule mult_right_mono [OF \<delta>])
lp15@62408
  1125
      apply (auto simp: dist_commute Rings.ordered_semiring_class.mult_right_mono \<delta>)
lp15@62408
  1126
      done
lp15@62408
  1127
    with \<open>e>0\<close> show ?thesis by force
lp15@62408
  1128
  qed
lp15@62408
  1129
  have "inj (op * (deriv f \<xi>))"
lp15@62408
  1130
    using dnz by simp
lp15@62408
  1131
  then obtain g' where g': "linear g'" "g' \<circ> op * (deriv f \<xi>) = id"
lp15@62408
  1132
    using linear_injective_left_inverse [of "op * (deriv f \<xi>)"]
lp15@62408
  1133
    by (auto simp: linear_times)
lp15@62408
  1134
  show ?thesis
lp15@62408
  1135
    apply (rule has_derivative_locally_injective [OF S, where f=f and f' = "\<lambda>z h. deriv f z * h" and g' = g'])
lp15@62408
  1136
    using g' *
lp15@62408
  1137
    apply (simp_all add: linear_conv_bounded_linear that)
lp15@62534
  1138
    using DERIV_deriv_iff_field_differentiable has_field_derivative_imp_has_derivative holf
lp15@62408
  1139
        holomorphic_on_imp_differentiable_at \<open>open S\<close> apply blast
lp15@62408
  1140
    done
lp15@62408
  1141
qed
lp15@62408
  1142
lp15@62408
  1143
lp15@62408
  1144
proposition has_complex_derivative_locally_invertible:
lp15@62408
  1145
  assumes holf: "f holomorphic_on S"
lp15@62408
  1146
      and S: "\<xi> \<in> S" "open S"
lp15@62408
  1147
      and dnz: "deriv f \<xi> \<noteq> 0"
lp15@62408
  1148
  obtains r where "r > 0" "ball \<xi> r \<subseteq> S" "open (f `  (ball \<xi> r))" "inj_on f (ball \<xi> r)"
lp15@62408
  1149
proof -
lp15@62408
  1150
  obtain r where "r > 0" "ball \<xi> r \<subseteq> S" "inj_on f (ball \<xi> r)"
lp15@62408
  1151
    by (blast intro: that has_complex_derivative_locally_injective [OF assms])
lp15@62408
  1152
  then have \<xi>: "\<xi> \<in> ball \<xi> r" by simp
lp15@62408
  1153
  then have nc: "~ f constant_on ball \<xi> r"
lp15@62408
  1154
    using \<open>inj_on f (ball \<xi> r)\<close> injective_not_constant by fastforce
lp15@62408
  1155
  have holf': "f holomorphic_on ball \<xi> r"
lp15@62408
  1156
    using \<open>ball \<xi> r \<subseteq> S\<close> holf holomorphic_on_subset by blast
lp15@62408
  1157
  have "open (f ` ball \<xi> r)"
lp15@62408
  1158
    apply (rule open_mapping_thm [OF holf'])
lp15@62408
  1159
    using nc apply auto
lp15@62408
  1160
    done
lp15@62408
  1161
  then show ?thesis
lp15@62408
  1162
    using \<open>0 < r\<close> \<open>ball \<xi> r \<subseteq> S\<close> \<open>inj_on f (ball \<xi> r)\<close> that  by blast
lp15@62408
  1163
qed
lp15@62408
  1164
lp15@62408
  1165
lp15@62408
  1166
proposition holomorphic_injective_imp_regular:
lp15@62408
  1167
  assumes holf: "f holomorphic_on S"
lp15@62408
  1168
      and "open S" and injf: "inj_on f S"
lp15@62408
  1169
      and "\<xi> \<in> S"
lp15@62408
  1170
    shows "deriv f \<xi> \<noteq> 0"
lp15@62408
  1171
proof -
lp15@62408
  1172
  obtain r where "r>0" and r: "ball \<xi> r \<subseteq> S" using assms by (blast elim!: openE)
lp15@62408
  1173
  have holf': "f holomorphic_on ball \<xi> r"
lp15@62408
  1174
    using \<open>ball \<xi> r \<subseteq> S\<close> holf holomorphic_on_subset by blast
lp15@62408
  1175
  show ?thesis
lp15@62408
  1176
  proof (cases "\<forall>n>0. (deriv ^^ n) f \<xi> = 0")
lp15@62408
  1177
    case True
lp15@62408
  1178
    have fcon: "f w = f \<xi>" if "w \<in> ball \<xi> r" for w
lp15@62408
  1179
      apply (rule holomorphic_fun_eq_const_on_connected [OF holf'])
lp15@62408
  1180
      using True \<open>0 < r\<close> that by auto
lp15@62408
  1181
    have False
lp15@62408
  1182
      using fcon [of "\<xi> + r/2"] \<open>0 < r\<close> r injf unfolding inj_on_def
lp15@62408
  1183
      by (metis \<open>\<xi> \<in> S\<close> contra_subsetD dist_commute fcon mem_ball perfect_choose_dist)
lp15@62408
  1184
    then show ?thesis ..
lp15@62408
  1185
  next
lp15@62408
  1186
    case False
lp15@62408
  1187
    then obtain n0 where n0: "n0 > 0 \<and> (deriv ^^ n0) f \<xi> \<noteq> 0" by blast
wenzelm@63040
  1188
    define n where [abs_def]: "n = (LEAST n. n > 0 \<and> (deriv ^^ n) f \<xi> \<noteq> 0)"
lp15@62408
  1189
    have n_ne: "n > 0" "(deriv ^^ n) f \<xi> \<noteq> 0"
lp15@62408
  1190
      using def_LeastI [OF n_def n0] by auto
lp15@62408
  1191
    have n_min: "\<And>k. 0 < k \<Longrightarrow> k < n \<Longrightarrow> (deriv ^^ k) f \<xi> = 0"
lp15@62408
  1192
      using def_Least_le [OF n_def] not_le by auto
lp15@62408
  1193
    obtain g \<delta> where "0 < \<delta>"
lp15@62408
  1194
             and holg: "g holomorphic_on ball \<xi> \<delta>"
lp15@62408
  1195
             and fd: "\<And>w. w \<in> ball \<xi> \<delta> \<Longrightarrow> f w - f \<xi> = ((w - \<xi>) * g w) ^ n"
lp15@62408
  1196
             and gnz: "\<And>w. w \<in> ball \<xi> \<delta> \<Longrightarrow> g w \<noteq> 0"
lp15@62408
  1197
      apply (rule holomorphic_factor_order_of_zero_strong [OF holf \<open>open S\<close> \<open>\<xi> \<in> S\<close> n_ne])
lp15@62408
  1198
      apply (blast intro: n_min)+
lp15@62408
  1199
      done
lp15@62408
  1200
    show ?thesis
lp15@62408
  1201
    proof (cases "n=1")
lp15@62408
  1202
      case True
lp15@62408
  1203
      with n_ne show ?thesis by auto
lp15@62408
  1204
    next
lp15@62408
  1205
      case False
lp15@62408
  1206
      have holgw: "(\<lambda>w. (w - \<xi>) * g w) holomorphic_on ball \<xi> (min r \<delta>)"
lp15@62408
  1207
        apply (rule holomorphic_intros)+
lp15@62408
  1208
        using holg by (simp add: holomorphic_on_subset subset_ball)
lp15@62408
  1209
      have gd: "\<And>w. dist \<xi> w < \<delta> \<Longrightarrow> (g has_field_derivative deriv g w) (at w)"
lp15@62408
  1210
        using holg
lp15@62534
  1211
        by (simp add: DERIV_deriv_iff_field_differentiable holomorphic_on_def at_within_open_NO_MATCH)
lp15@62408
  1212
      have *: "\<And>w. w \<in> ball \<xi> (min r \<delta>)
lp15@62408
  1213
            \<Longrightarrow> ((\<lambda>w. (w - \<xi>) * g w) has_field_derivative ((w - \<xi>) * deriv g w + g w))
lp15@62408
  1214
                (at w)"
lp15@62408
  1215
        by (rule gd derivative_eq_intros | simp)+
lp15@62408
  1216
      have [simp]: "deriv (\<lambda>w. (w - \<xi>) * g w) \<xi> \<noteq> 0"
lp15@62408
  1217
        using * [of \<xi>] \<open>0 < \<delta>\<close> \<open>0 < r\<close> by (simp add: DERIV_imp_deriv gnz)
lp15@62408
  1218
      obtain T where "\<xi> \<in> T" "open T" and Tsb: "T \<subseteq> ball \<xi> (min r \<delta>)" and oimT: "open ((\<lambda>w. (w - \<xi>) * g w) ` T)"
lp15@62408
  1219
        apply (rule has_complex_derivative_locally_invertible [OF holgw, of \<xi>])
lp15@62408
  1220
        using \<open>0 < r\<close> \<open>0 < \<delta>\<close>
lp15@62408
  1221
        apply (simp_all add:)
lp15@62408
  1222
        by (meson Topology_Euclidean_Space.open_ball centre_in_ball)
wenzelm@63040
  1223
      define U where "U = (\<lambda>w. (w - \<xi>) * g w) ` T"
lp15@62408
  1224
      have "open U" by (metis oimT U_def)
lp15@62408
  1225
      have "0 \<in> U"
lp15@62408
  1226
        apply (auto simp: U_def)
lp15@62408
  1227
        apply (rule image_eqI [where x = \<xi>])
lp15@62408
  1228
        apply (auto simp: \<open>\<xi> \<in> T\<close>)
lp15@62408
  1229
        done
lp15@62408
  1230
      then obtain \<epsilon> where "\<epsilon>>0" and \<epsilon>: "cball 0 \<epsilon> \<subseteq> U"
lp15@62408
  1231
        using \<open>open U\<close> open_contains_cball by blast
wenzelm@63589
  1232
      then have "\<epsilon> * exp(2 * of_real pi * \<i> * (0/n)) \<in> cball 0 \<epsilon>"
wenzelm@63589
  1233
                "\<epsilon> * exp(2 * of_real pi * \<i> * (1/n)) \<in> cball 0 \<epsilon>"
lp15@62408
  1234
        by (auto simp: norm_mult)
wenzelm@63589
  1235
      with \<epsilon> have "\<epsilon> * exp(2 * of_real pi * \<i> * (0/n)) \<in> U"
wenzelm@63589
  1236
                  "\<epsilon> * exp(2 * of_real pi * \<i> * (1/n)) \<in> U" by blast+
wenzelm@63589
  1237
      then obtain y0 y1 where "y0 \<in> T" and y0: "(y0 - \<xi>) * g y0 = \<epsilon> * exp(2 * of_real pi * \<i> * (0/n))"
wenzelm@63589
  1238
                          and "y1 \<in> T" and y1: "(y1 - \<xi>) * g y1 = \<epsilon> * exp(2 * of_real pi * \<i> * (1/n))"
lp15@62408
  1239
        by (auto simp: U_def)
lp15@62408
  1240
      then have "y0 \<in> ball \<xi> \<delta>" "y1 \<in> ball \<xi> \<delta>" using Tsb by auto
lp15@62408
  1241
      moreover have "y0 \<noteq> y1"
lp15@62408
  1242
        using y0 y1 \<open>\<epsilon> > 0\<close> complex_root_unity_eq_1 [of n 1] \<open>n > 0\<close> False by auto
lp15@62408
  1243
      moreover have "T \<subseteq> S"
lp15@62408
  1244
        by (meson Tsb min.cobounded1 order_trans r subset_ball)
lp15@62408
  1245
      ultimately have False
lp15@62408
  1246
        using inj_onD [OF injf, of y0 y1] \<open>y0 \<in> T\<close> \<open>y1 \<in> T\<close>
lp15@62408
  1247
        using fd [of y0] fd [of y1] complex_root_unity [of n 1]
lp15@62408
  1248
        apply (simp add: y0 y1 power_mult_distrib)
lp15@62408
  1249
        apply (force simp: algebra_simps)
lp15@62408
  1250
        done
lp15@62408
  1251
      then show ?thesis ..
lp15@62408
  1252
    qed
lp15@62408
  1253
  qed
lp15@62408
  1254
qed
lp15@62408
  1255
lp15@62408
  1256
lp15@62408
  1257
text\<open>Hence a nice clean inverse function theorem\<close>
lp15@62408
  1258
lp15@62408
  1259
proposition holomorphic_has_inverse:
lp15@62408
  1260
  assumes holf: "f holomorphic_on S"
lp15@62408
  1261
      and "open S" and injf: "inj_on f S"
lp15@62408
  1262
  obtains g where "g holomorphic_on (f ` S)"
lp15@62408
  1263
                  "\<And>z. z \<in> S \<Longrightarrow> deriv f z * deriv g (f z) = 1"
lp15@62408
  1264
                  "\<And>z. z \<in> S \<Longrightarrow> g(f z) = z"
lp15@62408
  1265
proof -
lp15@62408
  1266
  have ofs: "open (f ` S)"
lp15@62408
  1267
    by (rule open_mapping_thm3 [OF assms])
lp15@62408
  1268
  have contf: "continuous_on S f"
lp15@62408
  1269
    by (simp add: holf holomorphic_on_imp_continuous_on)
lp15@62408
  1270
  have *: "(the_inv_into S f has_field_derivative inverse (deriv f z)) (at (f z))" if "z \<in> S" for z
lp15@62408
  1271
  proof -
lp15@62408
  1272
    have 1: "(f has_field_derivative deriv f z) (at z)"
lp15@62534
  1273
      using DERIV_deriv_iff_field_differentiable \<open>z \<in> S\<close> \<open>open S\<close> holf holomorphic_on_imp_differentiable_at
lp15@62408
  1274
      by blast
lp15@62408
  1275
    have 2: "deriv f z \<noteq> 0"
lp15@62408
  1276
      using \<open>z \<in> S\<close> \<open>open S\<close> holf holomorphic_injective_imp_regular injf by blast
lp15@62408
  1277
    show ?thesis
lp15@62408
  1278
      apply (rule has_complex_derivative_inverse_strong [OF 1 2 \<open>open S\<close> \<open>z \<in> S\<close>])
lp15@62408
  1279
       apply (simp add: holf holomorphic_on_imp_continuous_on)
lp15@62408
  1280
      by (simp add: injf the_inv_into_f_f)
lp15@62408
  1281
  qed
lp15@62408
  1282
  show ?thesis
lp15@62408
  1283
    proof
lp15@62408
  1284
      show "the_inv_into S f holomorphic_on f ` S"
lp15@62408
  1285
        by (simp add: holomorphic_on_open ofs) (blast intro: *)
lp15@62408
  1286
    next
lp15@62408
  1287
      fix z assume "z \<in> S"
lp15@62408
  1288
      have "deriv f z \<noteq> 0"
lp15@62408
  1289
        using \<open>z \<in> S\<close> \<open>open S\<close> holf holomorphic_injective_imp_regular injf by blast
lp15@62408
  1290
      then show "deriv f z * deriv (the_inv_into S f) (f z) = 1"
lp15@62408
  1291
        using * [OF \<open>z \<in> S\<close>]  by (simp add: DERIV_imp_deriv)
lp15@62408
  1292
    next
lp15@62408
  1293
      fix z assume "z \<in> S"
lp15@62408
  1294
      show "the_inv_into S f (f z) = z"
lp15@62408
  1295
        by (simp add: \<open>z \<in> S\<close> injf the_inv_into_f_f)
lp15@62408
  1296
  qed
lp15@62408
  1297
qed
lp15@62408
  1298
lp15@62408
  1299
lp15@62408
  1300
subsection\<open>The Schwarz Lemma\<close>
lp15@62408
  1301
lp15@62408
  1302
lemma Schwarz1:
lp15@62408
  1303
  assumes holf: "f holomorphic_on S"
lp15@62408
  1304
      and contf: "continuous_on (closure S) f"
lp15@62408
  1305
      and S: "open S" "connected S"
lp15@62408
  1306
      and boS: "bounded S"
lp15@62408
  1307
      and "S \<noteq> {}"
lp15@62408
  1308
  obtains w where "w \<in> frontier S"
lp15@62408
  1309
                  "\<And>z. z \<in> closure S \<Longrightarrow> norm (f z) \<le> norm (f w)"
lp15@62408
  1310
proof -
lp15@62408
  1311
  have connf: "continuous_on (closure S) (norm o f)"
lp15@62408
  1312
    using contf continuous_on_compose continuous_on_norm_id by blast
lp15@62408
  1313
  have coc: "compact (closure S)"
lp15@62408
  1314
    by (simp add: \<open>bounded S\<close> bounded_closure compact_eq_bounded_closed)
lp15@62408
  1315
  then obtain x where x: "x \<in> closure S" and xmax: "\<And>z. z \<in> closure S \<Longrightarrow> norm(f z) \<le> norm(f x)"
lp15@62408
  1316
    apply (rule bexE [OF continuous_attains_sup [OF _ _ connf]])
lp15@62408
  1317
    using \<open>S \<noteq> {}\<close> apply auto
lp15@62408
  1318
    done
lp15@62408
  1319
  then show ?thesis
lp15@62408
  1320
  proof (cases "x \<in> frontier S")
lp15@62408
  1321
    case True
lp15@62408
  1322
    then show ?thesis using that xmax by blast
lp15@62408
  1323
  next
lp15@62408
  1324
    case False
lp15@62408
  1325
    then have "x \<in> S"
lp15@62408
  1326
      using \<open>open S\<close> frontier_def interior_eq x by auto
lp15@62408
  1327
    then have "f constant_on S"
lp15@62408
  1328
      apply (rule maximum_modulus_principle [OF holf S \<open>open S\<close> order_refl])
lp15@62408
  1329
      using closure_subset apply (blast intro: xmax)
lp15@62408
  1330
      done
lp15@62408
  1331
    then have "f constant_on (closure S)"
lp15@62408
  1332
      by (rule constant_on_closureI [OF _ contf])
lp15@62408
  1333
    then obtain c where c: "\<And>x. x \<in> closure S \<Longrightarrow> f x = c"
lp15@62408
  1334
      by (meson constant_on_def)
lp15@62408
  1335
    obtain w where "w \<in> frontier S"
lp15@62408
  1336
      by (metis coc all_not_in_conv assms(6) closure_UNIV frontier_eq_empty not_compact_UNIV)
lp15@62408
  1337
    then show ?thesis
lp15@62408
  1338
      by (simp add: c frontier_def that)
lp15@62408
  1339
  qed
lp15@62408
  1340
qed
lp15@62408
  1341
lp15@62408
  1342
lemma Schwarz2:
lp15@62408
  1343
 "\<lbrakk>f holomorphic_on ball 0 r;
lp15@62408
  1344
    0 < s; ball w s \<subseteq> ball 0 r;
lp15@62408
  1345
    \<And>z. norm (w-z) < s \<Longrightarrow> norm(f z) \<le> norm(f w)\<rbrakk>
lp15@62408
  1346
    \<Longrightarrow> f constant_on ball 0 r"
lp15@62408
  1347
by (rule maximum_modulus_principle [where U = "ball w s" and \<xi> = w]) (simp_all add: dist_norm)
lp15@62408
  1348
lp15@62408
  1349
lemma Schwarz3:
lp15@62408
  1350
  assumes holf: "f holomorphic_on (ball 0 r)" and [simp]: "f 0 = 0"
lp15@62408
  1351
  obtains h where "h holomorphic_on (ball 0 r)" and "\<And>z. norm z < r \<Longrightarrow> f z = z * (h z)" and "deriv f 0 = h 0"
lp15@62408
  1352
proof -
wenzelm@63040
  1353
  define h where "h z = (if z = 0 then deriv f 0 else f z / z)" for z
lp15@62408
  1354
  have d0: "deriv f 0 = h 0"
lp15@62408
  1355
    by (simp add: h_def)
lp15@62408
  1356
  moreover have "h holomorphic_on (ball 0 r)"
lp15@62408
  1357
    by (rule pole_theorem_open_0 [OF holf, of 0]) (auto simp: h_def)
lp15@62408
  1358
  moreover have "norm z < r \<Longrightarrow> f z = z * h z" for z
lp15@62408
  1359
    by (simp add: h_def)
lp15@62408
  1360
  ultimately show ?thesis
lp15@62408
  1361
    using that by blast
lp15@62408
  1362
qed
lp15@62408
  1363
lp15@62408
  1364
lp15@62408
  1365
proposition Schwarz_Lemma:
lp15@62408
  1366
  assumes holf: "f holomorphic_on (ball 0 1)" and [simp]: "f 0 = 0"
lp15@62408
  1367
      and no: "\<And>z. norm z < 1 \<Longrightarrow> norm (f z) < 1"
lp15@62408
  1368
      and \<xi>: "norm \<xi> < 1"
lp15@62408
  1369
    shows "norm (f \<xi>) \<le> norm \<xi>" and "norm(deriv f 0) \<le> 1"
lp15@62408
  1370
      and "((\<exists>z. norm z < 1 \<and> z \<noteq> 0 \<and> norm(f z) = norm z) \<or> norm(deriv f 0) = 1)
lp15@62408
  1371
           \<Longrightarrow> \<exists>\<alpha>. (\<forall>z. norm z < 1 \<longrightarrow> f z = \<alpha> * z) \<and> norm \<alpha> = 1" (is "?P \<Longrightarrow> ?Q")
lp15@62408
  1372
proof -
lp15@62408
  1373
  obtain h where holh: "h holomorphic_on (ball 0 1)"
lp15@62408
  1374
             and fz_eq: "\<And>z. norm z < 1 \<Longrightarrow> f z = z * (h z)" and df0: "deriv f 0 = h 0"
lp15@62408
  1375
    by (rule Schwarz3 [OF holf]) auto
lp15@62408
  1376
  have noh_le: "norm (h z) \<le> 1" if z: "norm z < 1" for z
lp15@62408
  1377
  proof -
lp15@62408
  1378
    have "norm (h z) < a" if a: "1 < a" for a
lp15@62408
  1379
    proof -
lp15@62408
  1380
      have "max (inverse a) (norm z) < 1"
lp15@62408
  1381
        using z a by (simp_all add: inverse_less_1_iff)
lp15@62408
  1382
      then obtain r where r: "max (inverse a) (norm z) < r" and "r < 1"
lp15@62408
  1383
        using Rats_dense_in_real by blast
lp15@62408
  1384
      then have nzr: "norm z < r" and ira: "inverse r < a"
lp15@62408
  1385
        using z a less_imp_inverse_less by force+
lp15@62408
  1386
      then have "0 < r"
lp15@62408
  1387
        by (meson norm_not_less_zero not_le order.strict_trans2)
lp15@62408
  1388
      have holh': "h holomorphic_on ball 0 r"
lp15@62408
  1389
        by (meson holh \<open>r < 1\<close> holomorphic_on_subset less_eq_real_def subset_ball)
lp15@62408
  1390
      have conth': "continuous_on (cball 0 r) h"
lp15@62408
  1391
        by (meson \<open>r < 1\<close> dual_order.trans holh holomorphic_on_imp_continuous_on holomorphic_on_subset mem_ball_0 mem_cball_0 not_less subsetI)
lp15@62408
  1392
      obtain w where w: "norm w = r" and lenw: "\<And>z. norm z < r \<Longrightarrow> norm(h z) \<le> norm(h w)"
lp15@62408
  1393
        apply (rule Schwarz1 [OF holh']) using conth' \<open>0 < r\<close> by auto
lp15@62408
  1394
      have "h w = f w / w" using fz_eq \<open>r < 1\<close> nzr w by auto
lp15@62408
  1395
      then have "cmod (h z) < inverse r"
lp15@62408
  1396
        by (metis \<open>0 < r\<close> \<open>r < 1\<close> divide_strict_right_mono inverse_eq_divide
lp15@62408
  1397
                  le_less_trans lenw no norm_divide nzr w)
lp15@62408
  1398
      then show ?thesis using ira by linarith
lp15@62408
  1399
    qed
lp15@62408
  1400
    then show "norm (h z) \<le> 1"
lp15@62408
  1401
      using not_le by blast
lp15@62408
  1402
  qed
lp15@62408
  1403
  show "cmod (f \<xi>) \<le> cmod \<xi>"
lp15@62408
  1404
  proof (cases "\<xi> = 0")
lp15@62408
  1405
    case True then show ?thesis by auto
lp15@62408
  1406
  next
lp15@62408
  1407
    case False
lp15@62408
  1408
    then show ?thesis
lp15@62408
  1409
      by (simp add: noh_le fz_eq \<xi> mult_left_le norm_mult)
lp15@62408
  1410
  qed
lp15@62408
  1411
  show no_df0: "norm(deriv f 0) \<le> 1"
lp15@62408
  1412
    by (simp add: \<open>\<And>z. cmod z < 1 \<Longrightarrow> cmod (h z) \<le> 1\<close> df0)
lp15@62408
  1413
  show "?Q" if "?P"
wenzelm@63540
  1414
    using that
lp15@62408
  1415
  proof
lp15@62408
  1416
    assume "\<exists>z. cmod z < 1 \<and> z \<noteq> 0 \<and> cmod (f z) = cmod z"
lp15@62408
  1417
    then obtain \<gamma> where \<gamma>: "cmod \<gamma> < 1" "\<gamma> \<noteq> 0" "cmod (f \<gamma>) = cmod \<gamma>" by blast
lp15@62408
  1418
    then have [simp]: "norm (h \<gamma>) = 1"
lp15@62408
  1419
      by (simp add: fz_eq norm_mult)
lp15@62408
  1420
    have "ball \<gamma> (1 - cmod \<gamma>) \<subseteq> ball 0 1"
lp15@62408
  1421
      by (simp add: ball_subset_ball_iff)
lp15@62408
  1422
    moreover have "\<And>z. cmod (\<gamma> - z) < 1 - cmod \<gamma> \<Longrightarrow> cmod (h z) \<le> cmod (h \<gamma>)"
lp15@62408
  1423
      apply (simp add: algebra_simps)
lp15@62408
  1424
      by (metis add_diff_cancel_left' diff_diff_eq2 le_less_trans noh_le norm_triangle_ineq4)
lp15@62408
  1425
    ultimately obtain c where c: "\<And>z. norm z < 1 \<Longrightarrow> h z = c"
lp15@62408
  1426
      using Schwarz2 [OF holh, of "1 - norm \<gamma>" \<gamma>, unfolded constant_on_def] \<gamma> by auto
wenzelm@63540
  1427
    then have "norm c = 1"
lp15@62408
  1428
      using \<gamma> by force
wenzelm@63540
  1429
    with c show ?thesis
lp15@62408
  1430
      using fz_eq by auto
lp15@62408
  1431
  next
lp15@62408
  1432
    assume [simp]: "cmod (deriv f 0) = 1"
lp15@62408
  1433
    then obtain c where c: "\<And>z. norm z < 1 \<Longrightarrow> h z = c"
lp15@62408
  1434
      using Schwarz2 [OF holh zero_less_one, of 0, unfolded constant_on_def] df0 noh_le
lp15@62408
  1435
      by auto
lp15@62408
  1436
    moreover have "norm c = 1"  using df0 c by auto
lp15@62408
  1437
    ultimately show ?thesis
lp15@62408
  1438
      using fz_eq by auto
lp15@62408
  1439
  qed
lp15@62408
  1440
qed
lp15@62408
  1441
lp15@62408
  1442
subsection\<open>The Schwarz reflection principle\<close>
lp15@62408
  1443
lp15@62408
  1444
lemma hol_pal_lem0:
lp15@62408
  1445
  assumes "d \<bullet> a \<le> k" "k \<le> d \<bullet> b"
lp15@62408
  1446
  obtains c where
lp15@62408
  1447
     "c \<in> closed_segment a b" "d \<bullet> c = k"
lp15@62408
  1448
     "\<And>z. z \<in> closed_segment a c \<Longrightarrow> d \<bullet> z \<le> k"
lp15@62408
  1449
     "\<And>z. z \<in> closed_segment c b \<Longrightarrow> k \<le> d \<bullet> z"
lp15@62408
  1450
proof -
lp15@62408
  1451
  obtain c where cin: "c \<in> closed_segment a b" and keq: "k = d \<bullet> c"
lp15@62408
  1452
    using connected_ivt_hyperplane [of "closed_segment a b" a b d k]
lp15@62408
  1453
    by (auto simp: assms)
lp15@62408
  1454
  have "closed_segment a c \<subseteq> {z. d \<bullet> z \<le> k}"  "closed_segment c b \<subseteq> {z. k \<le> d \<bullet> z}"
lp15@62408
  1455
    unfolding segment_convex_hull using assms keq
lp15@62408
  1456
    by (auto simp: convex_halfspace_le convex_halfspace_ge hull_minimal)
lp15@62408
  1457
  then show ?thesis using cin that by fastforce
lp15@62408
  1458
qed
lp15@62408
  1459
lp15@62408
  1460
lemma hol_pal_lem1:
lp15@62408
  1461
  assumes "convex S" "open S"
lp15@62408
  1462
      and abc: "a \<in> S" "b \<in> S" "c \<in> S"
lp15@62408
  1463
          "d \<noteq> 0" and lek: "d \<bullet> a \<le> k" "d \<bullet> b \<le> k" "d \<bullet> c \<le> k"
lp15@62408
  1464
      and holf1: "f holomorphic_on {z. z \<in> S \<and> d \<bullet> z < k}"
lp15@62408
  1465
      and contf: "continuous_on S f"
lp15@62408
  1466
    shows "contour_integral (linepath a b) f +
lp15@62408
  1467
           contour_integral (linepath b c) f +
lp15@62408
  1468
           contour_integral (linepath c a) f = 0"
lp15@62408
  1469
proof -
lp15@62408
  1470
  have "interior (convex hull {a, b, c}) \<subseteq> interior(S \<inter> {x. d \<bullet> x \<le> k})"
lp15@62408
  1471
    apply (rule interior_mono)
lp15@62408
  1472
    apply (rule hull_minimal)
lp15@62408
  1473
     apply (simp add: abc lek)
lp15@62408
  1474
    apply (rule convex_Int [OF \<open>convex S\<close> convex_halfspace_le])
lp15@62408
  1475
    done
lp15@62408
  1476
  also have "... \<subseteq> {z \<in> S. d \<bullet> z < k}"
lp15@62408
  1477
    by (force simp: interior_open [OF \<open>open S\<close>] \<open>d \<noteq> 0\<close>)
lp15@62408
  1478
  finally have *: "interior (convex hull {a, b, c}) \<subseteq> {z \<in> S. d \<bullet> z < k}" .
lp15@62408
  1479
  have "continuous_on (convex hull {a,b,c}) f"
lp15@62408
  1480
    using \<open>convex S\<close> contf abc continuous_on_subset subset_hull
lp15@62408
  1481
    by fastforce
lp15@62408
  1482
  moreover have "f holomorphic_on interior (convex hull {a,b,c})"
lp15@62408
  1483
    by (rule holomorphic_on_subset [OF holf1 *])
lp15@62408
  1484
  ultimately show ?thesis
lp15@62408
  1485
    using Cauchy_theorem_triangle_interior has_chain_integral_chain_integral3
lp15@62408
  1486
      by blast
lp15@62408
  1487
qed
lp15@62408
  1488
lp15@62408
  1489
lemma hol_pal_lem2:
lp15@62408
  1490
  assumes S: "convex S" "open S"
lp15@62408
  1491
      and abc: "a \<in> S" "b \<in> S" "c \<in> S"
lp15@62408
  1492
      and "d \<noteq> 0" and lek: "d \<bullet> a \<le> k" "d \<bullet> b \<le> k"
lp15@62408
  1493
      and holf1: "f holomorphic_on {z. z \<in> S \<and> d \<bullet> z < k}"
lp15@62408
  1494
      and holf2: "f holomorphic_on {z. z \<in> S \<and> k < d \<bullet> z}"
lp15@62408
  1495
      and contf: "continuous_on S f"
lp15@62408
  1496
    shows "contour_integral (linepath a b) f +
lp15@62408
  1497
           contour_integral (linepath b c) f +
lp15@62408
  1498
           contour_integral (linepath c a) f = 0"
lp15@62408
  1499
proof (cases "d \<bullet> c \<le> k")
lp15@62408
  1500
  case True show ?thesis
lp15@62408
  1501
    by (rule hol_pal_lem1 [OF S abc \<open>d \<noteq> 0\<close> lek True holf1 contf])
lp15@62408
  1502
next
lp15@62408
  1503
  case False
lp15@62408
  1504
  then have "d \<bullet> c > k" by force
lp15@62408
  1505
  obtain a' where a': "a' \<in> closed_segment b c" and "d \<bullet> a' = k"
lp15@62408
  1506
     and ba': "\<And>z. z \<in> closed_segment b a' \<Longrightarrow> d \<bullet> z \<le> k"
lp15@62408
  1507
     and a'c: "\<And>z. z \<in> closed_segment a' c \<Longrightarrow> k \<le> d \<bullet> z"
lp15@62408
  1508
    apply (rule hol_pal_lem0 [of d b k c, OF \<open>d \<bullet> b \<le> k\<close>])
lp15@62408
  1509
    using False by auto
lp15@62408
  1510
  obtain b' where b': "b' \<in> closed_segment a c" and "d \<bullet> b' = k"
lp15@62408
  1511
     and ab': "\<And>z. z \<in> closed_segment a b' \<Longrightarrow> d \<bullet> z \<le> k"
lp15@62408
  1512
     and b'c: "\<And>z. z \<in> closed_segment b' c \<Longrightarrow> k \<le> d \<bullet> z"
lp15@62408
  1513
    apply (rule hol_pal_lem0 [of d a k c, OF \<open>d \<bullet> a \<le> k\<close>])
lp15@62408
  1514
    using False by auto
lp15@62408
  1515
  have a'b': "a' \<in> S \<and> b' \<in> S"
lp15@62408
  1516
    using a' abc b' convex_contains_segment \<open>convex S\<close> by auto
lp15@62408
  1517
  have "continuous_on (closed_segment c a) f"
lp15@62408
  1518
    by (meson abc contf continuous_on_subset convex_contains_segment \<open>convex S\<close>)
lp15@62408
  1519
  then have 1: "contour_integral (linepath c a) f =
lp15@62408
  1520
                contour_integral (linepath c b') f + contour_integral (linepath b' a) f"
lp15@62408
  1521
    apply (rule contour_integral_split_linepath)
lp15@62408
  1522
    using b' by (simp add: closed_segment_commute)
lp15@62408
  1523
  have "continuous_on (closed_segment b c) f"
lp15@62408
  1524
    by (meson abc contf continuous_on_subset convex_contains_segment \<open>convex S\<close>)
lp15@62408
  1525
  then have 2: "contour_integral (linepath b c) f =
lp15@62408
  1526
                contour_integral (linepath b a') f + contour_integral (linepath a' c) f"
lp15@62408
  1527
    by (rule contour_integral_split_linepath [OF _ a'])
lp15@62463
  1528
  have 3: "contour_integral (reversepath (linepath b' a')) f =
lp15@62408
  1529
                - contour_integral (linepath b' a') f"
lp15@62408
  1530
    by (rule contour_integral_reversepath [OF valid_path_linepath])
lp15@62534
  1531
  have fcd_le: "f field_differentiable at x"
lp15@62408
  1532
               if "x \<in> interior S \<and> x \<in> interior {x. d \<bullet> x \<le> k}" for x
lp15@62408
  1533
  proof -
lp15@62408
  1534
    have "f holomorphic_on S \<inter> {c. d \<bullet> c < k}"
lp15@62408
  1535
      by (metis (no_types) Collect_conj_eq Collect_mem_eq holf1)
lp15@62408
  1536
    then have "\<exists>C D. x \<in> interior C \<inter> interior D \<and> f holomorphic_on interior C \<inter> interior D"
lp15@62408
  1537
      using that
lp15@62408
  1538
      by (metis Collect_mem_eq Int_Collect \<open>d \<noteq> 0\<close> interior_halfspace_le interior_open \<open>open S\<close>)
lp15@62534
  1539
    then show "f field_differentiable at x"
lp15@62408
  1540
      by (metis at_within_interior holomorphic_on_def interior_Int interior_interior)
lp15@62408
  1541
  qed
lp15@62408
  1542
  have ab_le: "\<And>x. x \<in> closed_segment a b \<Longrightarrow> d \<bullet> x \<le> k"
lp15@62408
  1543
  proof -
lp15@62408
  1544
    fix x :: complex
lp15@62408
  1545
    assume "x \<in> closed_segment a b"
lp15@62408
  1546
    then have "\<And>C. x \<in> C \<or> b \<notin> C \<or> a \<notin> C \<or> \<not> convex C"
lp15@62408
  1547
      by (meson contra_subsetD convex_contains_segment)
lp15@62408
  1548
    then show "d \<bullet> x \<le> k"
lp15@62408
  1549
      by (metis lek convex_halfspace_le mem_Collect_eq)
lp15@62408
  1550
  qed
lp15@62408
  1551
  have "continuous_on (S \<inter> {x. d \<bullet> x \<le> k}) f" using contf
lp15@62408
  1552
    by (simp add: continuous_on_subset)
lp15@62408
  1553
  then have "(f has_contour_integral 0)
lp15@62408
  1554
         (linepath a b +++ linepath b a' +++ linepath a' b' +++ linepath b' a)"
lp15@62408
  1555
    apply (rule Cauchy_theorem_convex [where k = "{}"])
lp15@62408
  1556
    apply (simp_all add: path_image_join convex_Int convex_halfspace_le \<open>convex S\<close> fcd_le ab_le
lp15@62408
  1557
                closed_segment_subset abc a'b' ba')
lp15@62408
  1558
    by (metis \<open>d \<bullet> a' = k\<close> \<open>d \<bullet> b' = k\<close> convex_contains_segment convex_halfspace_le lek(1) mem_Collect_eq order_refl)
lp15@62408
  1559
  then have 4: "contour_integral (linepath a b) f +
lp15@62408
  1560
                contour_integral (linepath b a') f +
lp15@62408
  1561
                contour_integral (linepath a' b') f +
lp15@62408
  1562
                contour_integral (linepath b' a) f = 0"
lp15@62408
  1563
    by (rule has_chain_integral_chain_integral4)
lp15@62534
  1564
  have fcd_ge: "f field_differentiable at x"
lp15@62408
  1565
               if "x \<in> interior S \<and> x \<in> interior {x. k \<le> d \<bullet> x}" for x
lp15@62408
  1566
  proof -
lp15@62408
  1567
    have f2: "f holomorphic_on S \<inter> {c. k < d \<bullet> c}"
lp15@62408
  1568
      by (metis (full_types) Collect_conj_eq Collect_mem_eq holf2)
lp15@62408
  1569
    have f3: "interior S = S"
lp15@62408
  1570
      by (simp add: interior_open \<open>open S\<close>)
lp15@62408
  1571
    then have "x \<in> S \<inter> interior {c. k \<le> d \<bullet> c}"
lp15@62408
  1572
      using that by simp
lp15@62534
  1573
    then show "f field_differentiable at x"
lp15@62408
  1574
      using f3 f2 unfolding holomorphic_on_def
lp15@62408
  1575
      by (metis (no_types) \<open>d \<noteq> 0\<close> at_within_interior interior_Int interior_halfspace_ge interior_interior)
lp15@62408
  1576
  qed
lp15@62408
  1577
  have "continuous_on (S \<inter> {x. k \<le> d \<bullet> x}) f" using contf
lp15@62408
  1578
    by (simp add: continuous_on_subset)
lp15@62408
  1579
  then have "(f has_contour_integral 0) (linepath a' c +++ linepath c b' +++ linepath b' a')"
lp15@62408
  1580
    apply (rule Cauchy_theorem_convex [where k = "{}"])
lp15@62408
  1581
    apply (simp_all add: path_image_join convex_Int convex_halfspace_ge \<open>convex S\<close>
lp15@62408
  1582
                      fcd_ge closed_segment_subset abc a'b' a'c)
lp15@62408
  1583
    by (metis \<open>d \<bullet> a' = k\<close> b'c closed_segment_commute convex_contains_segment
lp15@62408
  1584
              convex_halfspace_ge ends_in_segment(2) mem_Collect_eq order_refl)
lp15@62408
  1585
  then have 5: "contour_integral (linepath a' c) f + contour_integral (linepath c b') f + contour_integral (linepath b' a') f = 0"
lp15@62408
  1586
    by (rule has_chain_integral_chain_integral3)
lp15@62408
  1587
  show ?thesis
lp15@62408
  1588
    using 1 2 3 4 5 by (metis add.assoc eq_neg_iff_add_eq_0 reversepath_linepath)
lp15@62408
  1589
qed
lp15@62408
  1590
lp15@62408
  1591
lemma hol_pal_lem3:
lp15@62408
  1592
  assumes S: "convex S" "open S"
lp15@62408
  1593
      and abc: "a \<in> S" "b \<in> S" "c \<in> S"
lp15@62408
  1594
      and "d \<noteq> 0" and lek: "d \<bullet> a \<le> k"
lp15@62408
  1595
      and holf1: "f holomorphic_on {z. z \<in> S \<and> d \<bullet> z < k}"
lp15@62408
  1596
      and holf2: "f holomorphic_on {z. z \<in> S \<and> k < d \<bullet> z}"
lp15@62408
  1597
      and contf: "continuous_on S f"
lp15@62408
  1598
    shows "contour_integral (linepath a b) f +
lp15@62408
  1599
           contour_integral (linepath b c) f +
lp15@62408
  1600
           contour_integral (linepath c a) f = 0"
lp15@62408
  1601
proof (cases "d \<bullet> b \<le> k")
lp15@62408
  1602
  case True show ?thesis
lp15@62408
  1603
    by (rule hol_pal_lem2 [OF S abc \<open>d \<noteq> 0\<close> lek True holf1 holf2 contf])
lp15@62408
  1604
next
lp15@62408
  1605
  case False
lp15@62408
  1606
  show ?thesis
lp15@62408
  1607
  proof (cases "d \<bullet> c \<le> k")
lp15@62408
  1608
    case True
lp15@62408
  1609
    have "contour_integral (linepath c a) f +
lp15@62408
  1610
          contour_integral (linepath a b) f +
lp15@62408
  1611
          contour_integral (linepath b c) f = 0"
lp15@62408
  1612
      by (rule hol_pal_lem2 [OF S \<open>c \<in> S\<close> \<open>a \<in> S\<close> \<open>b \<in> S\<close> \<open>d \<noteq> 0\<close> \<open>d \<bullet> c \<le> k\<close> lek holf1 holf2 contf])
lp15@62408
  1613
    then show ?thesis
lp15@62408
  1614
      by (simp add: algebra_simps)
lp15@62408
  1615
  next
lp15@62408
  1616
    case False
lp15@62408
  1617
    have "contour_integral (linepath b c) f +
lp15@62408
  1618
          contour_integral (linepath c a) f +
lp15@62408
  1619
          contour_integral (linepath a b) f = 0"
lp15@62408
  1620
      apply (rule hol_pal_lem2 [OF S \<open>b \<in> S\<close> \<open>c \<in> S\<close> \<open>a \<in> S\<close>, of "-d" "-k"])
lp15@62408
  1621
      using \<open>d \<noteq> 0\<close> \<open>\<not> d \<bullet> b \<le> k\<close> False by (simp_all add: holf1 holf2 contf)
lp15@62408
  1622
    then show ?thesis
lp15@62408
  1623
      by (simp add: algebra_simps)
lp15@62408
  1624
  qed
lp15@62408
  1625
qed
lp15@62408
  1626
lp15@62408
  1627
lemma hol_pal_lem4:
lp15@62408
  1628
  assumes S: "convex S" "open S"
lp15@62408
  1629
      and abc: "a \<in> S" "b \<in> S" "c \<in> S" and "d \<noteq> 0"
lp15@62408
  1630
      and holf1: "f holomorphic_on {z. z \<in> S \<and> d \<bullet> z < k}"
lp15@62408
  1631
      and holf2: "f holomorphic_on {z. z \<in> S \<and> k < d \<bullet> z}"
lp15@62408
  1632
      and contf: "continuous_on S f"
lp15@62408
  1633
    shows "contour_integral (linepath a b) f +
lp15@62408
  1634
           contour_integral (linepath b c) f +
lp15@62408
  1635
           contour_integral (linepath c a) f = 0"
lp15@62408
  1636
proof (cases "d \<bullet> a \<le> k")
lp15@62408
  1637
  case True show ?thesis
lp15@62408
  1638
    by (rule hol_pal_lem3 [OF S abc \<open>d \<noteq> 0\<close> True holf1 holf2 contf])
lp15@62408
  1639
next
lp15@62408
  1640
  case False
lp15@62408
  1641
  show ?thesis
lp15@62408
  1642
    apply (rule hol_pal_lem3 [OF S abc, of "-d" "-k"])
lp15@62408
  1643
    using \<open>d \<noteq> 0\<close> False by (simp_all add: holf1 holf2 contf)
lp15@62408
  1644
qed
lp15@62408
  1645
lp15@62408
  1646
proposition holomorphic_on_paste_across_line:
lp15@62408
  1647
  assumes S: "open S" and "d \<noteq> 0"
lp15@62408
  1648
      and holf1: "f holomorphic_on (S \<inter> {z. d \<bullet> z < k})"
lp15@62408
  1649
      and holf2: "f holomorphic_on (S \<inter> {z. k < d \<bullet> z})"
lp15@62408
  1650
      and contf: "continuous_on S f"
lp15@62408
  1651
    shows "f holomorphic_on S"
lp15@62408
  1652
proof -
lp15@62408
  1653
  have *: "\<exists>t. open t \<and> p \<in> t \<and> continuous_on t f \<and>
lp15@62408
  1654
               (\<forall>a b c. convex hull {a, b, c} \<subseteq> t \<longrightarrow>
lp15@62408
  1655
                         contour_integral (linepath a b) f +
lp15@62408
  1656
                         contour_integral (linepath b c) f +
lp15@62408
  1657
                         contour_integral (linepath c a) f = 0)"
lp15@62408
  1658
          if "p \<in> S" for p
lp15@62408
  1659
  proof -
lp15@62408
  1660
    obtain e where "e>0" and e: "ball p e \<subseteq> S"
lp15@62408
  1661
      using \<open>p \<in> S\<close> openE S by blast
lp15@62408
  1662
    then have "continuous_on (ball p e) f"
lp15@62408
  1663
      using contf continuous_on_subset by blast
lp15@62408
  1664
    moreover have "f holomorphic_on {z. dist p z < e \<and> d \<bullet> z < k}"
lp15@62408
  1665
      apply (rule holomorphic_on_subset [OF holf1])
lp15@62408
  1666
      using e by auto
lp15@62408
  1667
    moreover have "f holomorphic_on {z. dist p z < e \<and> k < d \<bullet> z}"
lp15@62408
  1668
      apply (rule holomorphic_on_subset [OF holf2])
lp15@62408
  1669
      using e by auto
lp15@62408
  1670
    ultimately show ?thesis
lp15@62408
  1671
      apply (rule_tac x="ball p e" in exI)
lp15@62408
  1672
      using \<open>e > 0\<close> e \<open>d \<noteq> 0\<close>
lp15@62408
  1673
      apply (simp add:, clarify)
lp15@62408
  1674
      apply (rule hol_pal_lem4 [of "ball p e" _ _ _ d _ k])
lp15@62408
  1675
      apply (auto simp: subset_hull)
lp15@62408
  1676
      done
lp15@62408
  1677
  qed
lp15@62408
  1678
  show ?thesis
lp15@62408
  1679
    by (blast intro: * Morera_local_triangle analytic_imp_holomorphic)
lp15@62408
  1680
qed
lp15@62408
  1681
lp15@62408
  1682
proposition Schwarz_reflection:
lp15@62408
  1683
  assumes "open S" and cnjs: "cnj ` S \<subseteq> S"
lp15@62408
  1684
      and  holf: "f holomorphic_on (S \<inter> {z. 0 < Im z})"
lp15@62408
  1685
      and contf: "continuous_on (S \<inter> {z. 0 \<le> Im z}) f"
lp15@62408
  1686
      and f: "\<And>z. \<lbrakk>z \<in> S; z \<in> \<real>\<rbrakk> \<Longrightarrow> (f z) \<in> \<real>"
lp15@62408
  1687
    shows "(\<lambda>z. if 0 \<le> Im z then f z else cnj(f(cnj z))) holomorphic_on S"
lp15@62408
  1688
proof -
lp15@62408
  1689
  have 1: "(\<lambda>z. if 0 \<le> Im z then f z else cnj (f (cnj z))) holomorphic_on (S \<inter> {z. 0 < Im z})"
lp15@62408
  1690
    by (force intro: iffD1 [OF holomorphic_cong [OF refl] holf])
lp15@62408
  1691
  have cont_cfc: "continuous_on (S \<inter> {z. Im z \<le> 0}) (cnj o f o cnj)"
lp15@62408
  1692
    apply (intro continuous_intros continuous_on_compose continuous_on_subset [OF contf])
lp15@62408
  1693
    using cnjs apply auto
lp15@62408
  1694
    done
lp15@62534
  1695
  have "cnj \<circ> f \<circ> cnj field_differentiable at x within S \<inter> {z. Im z < 0}"
lp15@62534
  1696
        if "x \<in> S" "Im x < 0" "f field_differentiable at (cnj x) within S \<inter> {z. 0 < Im z}" for x
lp15@62408
  1697
    using that
lp15@62534
  1698
    apply (simp add: field_differentiable_def Derivative.DERIV_within_iff Lim_within dist_norm, clarify)
lp15@62408
  1699
    apply (rule_tac x="cnj f'" in exI)
lp15@62408
  1700
    apply (elim all_forward ex_forward conj_forward imp_forward asm_rl, clarify)
lp15@62408
  1701
    apply (drule_tac x="cnj xa" in bspec)
lp15@62408
  1702
    using cnjs apply force
lp15@62408
  1703
    apply (metis complex_cnj_cnj complex_cnj_diff complex_cnj_divide complex_mod_cnj)
lp15@62408
  1704
    done
lp15@62408
  1705
  then have hol_cfc: "(cnj o f o cnj) holomorphic_on (S \<inter> {z. Im z < 0})"
lp15@62408
  1706
    using holf cnjs
lp15@62408
  1707
    by (force simp: holomorphic_on_def)
lp15@62408
  1708
  have 2: "(\<lambda>z. if 0 \<le> Im z then f z else cnj (f (cnj z))) holomorphic_on (S \<inter> {z. Im z < 0})"
lp15@62408
  1709
    apply (rule iffD1 [OF holomorphic_cong [OF refl]])
lp15@62408
  1710
    using hol_cfc by auto
lp15@62408
  1711
  have [simp]: "(S \<inter> {z. 0 \<le> Im z}) \<union> (S \<inter> {z. Im z \<le> 0}) = S"
lp15@62408
  1712
    by force
lp15@62408
  1713
  have "continuous_on ((S \<inter> {z. 0 \<le> Im z}) \<union> (S \<inter> {z. Im z \<le> 0}))
lp15@62408
  1714
                       (\<lambda>z. if 0 \<le> Im z then f z else cnj (f (cnj z)))"
lp15@62408
  1715
    apply (rule continuous_on_cases_local)
lp15@62408
  1716
    using cont_cfc contf
lp15@62408
  1717
    apply (simp_all add: closedin_closed_Int closed_halfspace_Im_le closed_halfspace_Im_ge)
lp15@62408
  1718
    using f Reals_cnj_iff complex_is_Real_iff apply auto
lp15@62408
  1719
    done
lp15@62408
  1720
  then have 3: "continuous_on S (\<lambda>z. if 0 \<le> Im z then f z else cnj (f (cnj z)))"
lp15@62408
  1721
    by force
lp15@62408
  1722
  show ?thesis
wenzelm@63589
  1723
    apply (rule holomorphic_on_paste_across_line [OF \<open>open S\<close>, of "- \<i>" _ 0])
lp15@62408
  1724
    using 1 2 3
lp15@62408
  1725
    apply auto
lp15@62408
  1726
    done
lp15@62408
  1727
qed
lp15@62408
  1728
lp15@62533
  1729
subsection\<open>Bloch's theorem\<close>
lp15@62533
  1730
lp15@62533
  1731
lemma Bloch_lemma_0:
lp15@62533
  1732
  assumes holf: "f holomorphic_on cball 0 r" and "0 < r"
lp15@62533
  1733
      and [simp]: "f 0 = 0"
lp15@62533
  1734
      and le: "\<And>z. norm z < r \<Longrightarrow> norm(deriv f z) \<le> 2 * norm(deriv f 0)"
lp15@62533
  1735
    shows "ball 0 ((3 - 2 * sqrt 2) * r * norm(deriv f 0)) \<subseteq> f ` ball 0 r"
lp15@62533
  1736
proof -
lp15@62533
  1737
  have "sqrt 2 < 3/2"
lp15@62533
  1738
    by (rule real_less_lsqrt) (auto simp: power2_eq_square)
lp15@62533
  1739
  then have sq3: "0 < 3 - 2 * sqrt 2" by simp
lp15@62533
  1740
  show ?thesis
lp15@62533
  1741
  proof (cases "deriv f 0 = 0")
lp15@62533
  1742
    case True then show ?thesis by simp
lp15@62533
  1743
  next
lp15@62533
  1744
    case False
wenzelm@63040
  1745
    define C where "C = 2 * norm(deriv f 0)"
lp15@62533
  1746
    have "0 < C" using False by (simp add: C_def)
lp15@62533
  1747
    have holf': "f holomorphic_on ball 0 r" using holf
lp15@62533
  1748
      using ball_subset_cball holomorphic_on_subset by blast
lp15@62533
  1749
    then have holdf': "deriv f holomorphic_on ball 0 r"
lp15@62533
  1750
      by (rule holomorphic_deriv [OF _ open_ball])
lp15@62533
  1751
    have "Le1": "norm(deriv f z - deriv f 0) \<le> norm z / (r - norm z) * C"
lp15@62533
  1752
                if "norm z < r" for z
lp15@62533
  1753
    proof -
lp15@62533
  1754
      have T1: "norm(deriv f z - deriv f 0) \<le> norm z / (R - norm z) * C"
lp15@62533
  1755
              if R: "norm z < R" "R < r" for R
lp15@62533
  1756
      proof -
lp15@62533
  1757
        have "0 < R" using R
lp15@62533
  1758
          by (metis less_trans norm_zero zero_less_norm_iff)
lp15@62533
  1759
        have df_le: "\<And>x. norm x < r \<Longrightarrow> norm (deriv f x) \<le> C"
lp15@62533
  1760
          using le by (simp add: C_def)
lp15@62533
  1761
        have hol_df: "deriv f holomorphic_on cball 0 R"
lp15@62533
  1762
          apply (rule holomorphic_on_subset) using R holdf' by auto
lp15@62533
  1763
        have *: "((\<lambda>w. deriv f w / (w - z)) has_contour_integral 2 * pi * \<i> * deriv f z) (circlepath 0 R)"
lp15@62533
  1764
                 if "norm z < R" for z
lp15@62533
  1765
          using \<open>0 < R\<close> that Cauchy_integral_formula_convex_simple [OF convex_cball hol_df, of _ "circlepath 0 R"]
lp15@62533
  1766
          by (force simp: winding_number_circlepath)
lp15@62533
  1767
        have **: "((\<lambda>x. deriv f x / (x - z) - deriv f x / x) has_contour_integral
lp15@62533
  1768
                   of_real (2 * pi) * \<i> * (deriv f z - deriv f 0))
lp15@62533
  1769
                  (circlepath 0 R)"
lp15@62533
  1770
           using has_contour_integral_diff [OF * [of z] * [of 0]] \<open>0 < R\<close> that
lp15@62533
  1771
           by (simp add: algebra_simps)
lp15@62533
  1772
        have [simp]: "\<And>x. norm x = R \<Longrightarrow> x \<noteq> z"  using that(1) by blast
lp15@62533
  1773
        have "norm (deriv f x / (x - z) - deriv f x / x)
lp15@62533
  1774
                     \<le> C * norm z / (R * (R - norm z))"
lp15@62533
  1775
                  if "norm x = R" for x
lp15@62533
  1776
        proof -
lp15@62533
  1777
          have [simp]: "norm (deriv f x * x - deriv f x * (x - z)) =
lp15@62533
  1778
                        norm (deriv f x) * norm z"
lp15@62533
  1779
            by (simp add: norm_mult right_diff_distrib')
lp15@62533
  1780
          show ?thesis
lp15@62533
  1781
            using  \<open>0 < R\<close> \<open>0 < C\<close> R that
lp15@62533
  1782
            apply (simp add: norm_mult norm_divide divide_simps)
lp15@62533
  1783
            using df_le norm_triangle_ineq2 \<open>0 < C\<close> apply (auto intro!: mult_mono)
lp15@62533
  1784
            done
lp15@62533
  1785
        qed
lp15@62533
  1786
        then show ?thesis
lp15@62533
  1787
          using has_contour_integral_bound_circlepath
lp15@62533
  1788
                  [OF **, of "C * norm z/(R*(R - norm z))"]
lp15@62533
  1789
                \<open>0 < R\<close> \<open>0 < C\<close> R
lp15@62533
  1790
          apply (simp add: norm_mult norm_divide)
lp15@62533
  1791
          apply (simp add: divide_simps mult.commute)
lp15@62533
  1792
          done
lp15@62533
  1793
      qed
lp15@62533
  1794
      obtain r' where r': "norm z < r'" "r' < r"
lp15@62533
  1795
        using Rats_dense_in_real [of "norm z" r] \<open>norm z < r\<close> by blast
lp15@62533
  1796
      then have [simp]: "closure {r'<..<r} = {r'..r}" by simp
lp15@62533
  1797
      show ?thesis
lp15@62533
  1798
        apply (rule continuous_ge_on_closure
lp15@62533
  1799
                 [where f = "\<lambda>r. norm z / (r - norm z) * C" and s = "{r'<..<r}",
lp15@62533
  1800
                  OF _ _ T1])
lp15@62533
  1801
        apply (intro continuous_intros)
lp15@62533
  1802
        using that r'
lp15@62533
  1803
        apply (auto simp: not_le)
lp15@62533
  1804
        done
lp15@62533
  1805
    qed
lp15@62533
  1806
    have "*": "(norm z - norm z^2/(r - norm z)) * norm(deriv f 0) \<le> norm(f z)"
lp15@62533
  1807
              if r: "norm z < r" for z
lp15@62533
  1808
    proof -
lp15@62533
  1809
      have 1: "\<And>x. x \<in> ball 0 r \<Longrightarrow>
lp15@62533
  1810
              ((\<lambda>z. f z - deriv f 0 * z) has_field_derivative deriv f x - deriv f 0)
lp15@62533
  1811
               (at x within ball 0 r)"
lp15@62533
  1812
        by (rule derivative_eq_intros holomorphic_derivI holf' | simp)+
lp15@62533
  1813
      have 2: "closed_segment 0 z \<subseteq> ball 0 r"
lp15@62533
  1814
        by (metis \<open>0 < r\<close> convex_ball convex_contains_segment dist_self mem_ball mem_ball_0 that)
lp15@62533
  1815
      have 3: "(\<lambda>t. (norm z)\<^sup>2 * t / (r - norm z) * C) integrable_on {0..1}"
lp15@62533
  1816
        apply (rule integrable_on_cmult_right [where 'b=real, simplified])
lp15@62533
  1817
        apply (rule integrable_on_cdivide [where 'b=real, simplified])
lp15@62533
  1818
        apply (rule integrable_on_cmult_left [where 'b=real, simplified])
lp15@62533
  1819
        apply (rule ident_integrable_on)
lp15@62533
  1820
        done
lp15@62533
  1821
      have 4: "norm (deriv f (x *\<^sub>R z) - deriv f 0) * norm z \<le> norm z * norm z * x * C / (r - norm z)"
lp15@62533
  1822
              if x: "0 \<le> x" "x \<le> 1" for x
lp15@62533
  1823
      proof -
lp15@62533
  1824
        have [simp]: "x * norm z < r"
lp15@62533
  1825
          using r x by (meson le_less_trans mult_le_cancel_right2 norm_not_less_zero)
lp15@62533
  1826
        have "norm (deriv f (x *\<^sub>R z) - deriv f 0) \<le> norm (x *\<^sub>R z) / (r - norm (x *\<^sub>R z)) * C"
lp15@62533
  1827
          apply (rule Le1) using r x \<open>0 < r\<close> by simp
lp15@62533
  1828
        also have "... \<le> norm (x *\<^sub>R z) / (r - norm z) * C"
lp15@62533
  1829
          using r x \<open>0 < r\<close>
lp15@62533
  1830
          apply (simp add: divide_simps)
lp15@62533
  1831
          by (simp add: \<open>0 < C\<close> mult.assoc mult_left_le_one_le ordered_comm_semiring_class.comm_mult_left_mono)
lp15@62533
  1832
        finally have "norm (deriv f (x *\<^sub>R z) - deriv f 0) * norm z \<le> norm (x *\<^sub>R z)  / (r - norm z) * C * norm z"
lp15@62533
  1833
          by (rule mult_right_mono) simp
lp15@62533
  1834
        with x show ?thesis by (simp add: algebra_simps)
lp15@62533
  1835
      qed
lp15@62533
  1836
      have le_norm: "abc \<le> norm d - e \<Longrightarrow> norm(f - d) \<le> e \<Longrightarrow> abc \<le> norm f" for abc d e and f::complex
lp15@62533
  1837
        by (metis add_diff_cancel_left' add_diff_eq diff_left_mono norm_diff_ineq order_trans)
lp15@62533
  1838
      have "norm (integral {0..1} (\<lambda>x. (deriv f (x *\<^sub>R z) - deriv f 0) * z))
lp15@62533
  1839
            \<le> integral {0..1} (\<lambda>t. (norm z)\<^sup>2 * t / (r - norm z) * C)"
lp15@62533
  1840
        apply (rule integral_norm_bound_integral)
lp15@62533
  1841
        using contour_integral_primitive [OF 1, of "linepath 0 z"] 2
lp15@62533
  1842
        apply (simp add: has_contour_integral_linepath has_integral_integrable_integral)
lp15@62533
  1843
        apply (rule 3)
lp15@62533
  1844
        apply (simp add: norm_mult power2_eq_square 4)
lp15@62533
  1845
        done
lp15@62533
  1846
      then have int_le: "norm (f z - deriv f 0 * z) \<le> (norm z)\<^sup>2 * norm(deriv f 0) / ((r - norm z))"
lp15@62533
  1847
        using contour_integral_primitive [OF 1, of "linepath 0 z"] 2
lp15@62533
  1848
        apply (simp add: has_contour_integral_linepath has_integral_integrable_integral C_def)
lp15@62533
  1849
        done
lp15@62533
  1850
      show ?thesis
lp15@62533
  1851
        apply (rule le_norm [OF _ int_le])
lp15@62533
  1852
        using \<open>norm z < r\<close>
lp15@62533
  1853
        apply (simp add: power2_eq_square divide_simps C_def norm_mult)
lp15@62533
  1854
        proof -
lp15@62533
  1855
          have "norm z * (norm (deriv f 0) * (r - norm z - norm z)) \<le> norm z * (norm (deriv f 0) * (r - norm z) - norm (deriv f 0) * norm z)"
lp15@62533
  1856
            by (simp add: linordered_field_class.sign_simps(38))
lp15@62533
  1857
          then show "(norm z * (r - norm z) - norm z * norm z) * norm (deriv f 0) \<le> norm (deriv f 0) * norm z * (r - norm z) - norm z * norm z * norm (deriv f 0)"
lp15@62533
  1858
            by (simp add: linordered_field_class.sign_simps(38) mult.commute mult.left_commute)
lp15@62533
  1859
        qed
lp15@62533
  1860
    qed
lp15@62533
  1861
    have sq201 [simp]: "0 < (1 - sqrt 2 / 2)" "(1 - sqrt 2 / 2)  < 1"
lp15@62533
  1862
      by (auto simp:  sqrt2_less_2)
lp15@62533
  1863
    have 1: "continuous_on (closure (ball 0 ((1 - sqrt 2 / 2) * r))) f"
lp15@62533
  1864
      apply (rule continuous_on_subset [OF holomorphic_on_imp_continuous_on [OF holf]])
lp15@62533
  1865
      apply (subst closure_ball)
lp15@62533
  1866
      using \<open>0 < r\<close> mult_pos_pos sq201
lp15@62533
  1867
      apply (auto simp: cball_subset_cball_iff)
lp15@62533
  1868
      done
lp15@62533
  1869
    have 2: "open (f ` interior (ball 0 ((1 - sqrt 2 / 2) * r)))"
lp15@62533
  1870
      apply (rule open_mapping_thm [OF holf' open_ball connected_ball], force)
lp15@62533
  1871
      using \<open>0 < r\<close> mult_pos_pos sq201 apply (simp add: ball_subset_ball_iff)
lp15@62533
  1872
      using False \<open>0 < r\<close> centre_in_ball holf' holomorphic_nonconstant by blast
lp15@62533
  1873
    have "ball 0 ((3 - 2 * sqrt 2) * r * norm (deriv f 0)) =
lp15@62533
  1874
          ball (f 0) ((3 - 2 * sqrt 2) * r * norm (deriv f 0))"
lp15@62533
  1875
      by simp
lp15@62533
  1876
    also have "...  \<subseteq> f ` ball 0 ((1 - sqrt 2 / 2) * r)"
lp15@62533
  1877
    proof -
lp15@62533
  1878
      have 3: "(3 - 2 * sqrt 2) * r * norm (deriv f 0) \<le> norm (f z)"
lp15@62533
  1879
           if "norm z = (1 - sqrt 2 / 2) * r" for z
lp15@62533
  1880
        apply (rule order_trans [OF _ *])
lp15@62533
  1881
        using  \<open>0 < r\<close>
lp15@62533
  1882
        apply (simp_all add: field_simps  power2_eq_square that)
lp15@62533
  1883
        apply (simp add: mult.assoc [symmetric])
lp15@62533
  1884
        done
lp15@62533
  1885
      show ?thesis
lp15@62533
  1886
        apply (rule ball_subset_open_map_image [OF 1 2 _ bounded_ball])
lp15@62533
  1887
        using \<open>0 < r\<close> sq201 3 apply simp_all
lp15@62533
  1888
        using C_def \<open>0 < C\<close> sq3 apply force
lp15@62533
  1889
        done
lp15@62533
  1890
     qed
lp15@62533
  1891
    also have "...  \<subseteq> f ` ball 0 r"
lp15@62533
  1892
      apply (rule image_subsetI [OF imageI], simp)
lp15@62533
  1893
      apply (erule less_le_trans)
lp15@62533
  1894
      using \<open>0 < r\<close> apply (auto simp: field_simps)
lp15@62533
  1895
      done
lp15@62533
  1896
    finally show ?thesis .
lp15@62533
  1897
  qed
lp15@62533
  1898
qed
lp15@62533
  1899
hoelzl@63594
  1900
lemma Bloch_lemma:
lp15@62533
  1901
  assumes holf: "f holomorphic_on cball a r" and "0 < r"
lp15@62533
  1902
      and le: "\<And>z. z \<in> ball a r \<Longrightarrow> norm(deriv f z) \<le> 2 * norm(deriv f a)"
lp15@62533
  1903
    shows "ball (f a) ((3 - 2 * sqrt 2) * r * norm(deriv f a)) \<subseteq> f ` ball a r"
lp15@62533
  1904
proof -
lp15@62533
  1905
  have fz: "(\<lambda>z. f (a + z)) = f o (\<lambda>z. (a + z))"
lp15@62533
  1906
    by (simp add: o_def)
lp15@62533
  1907
  have hol0: "(\<lambda>z. f (a + z)) holomorphic_on cball 0 r"
lp15@62533
  1908
    unfolding fz by (intro holomorphic_intros holf holomorphic_on_compose | simp)+
lp15@62534
  1909
  then have [simp]: "\<And>x. norm x < r \<Longrightarrow> (\<lambda>z. f (a + z)) field_differentiable at x"
lp15@62533
  1910
    by (metis Topology_Euclidean_Space.open_ball at_within_open ball_subset_cball diff_0 dist_norm holomorphic_on_def holomorphic_on_subset mem_ball norm_minus_cancel)
lp15@62534
  1911
  have [simp]: "\<And>z. norm z < r \<Longrightarrow> f field_differentiable at (a + z)"
lp15@62533
  1912
    by (metis holf open_ball add_diff_cancel_left' dist_complex_def holomorphic_on_imp_differentiable_at holomorphic_on_subset interior_cball interior_subset mem_ball norm_minus_commute)
lp15@62534
  1913
  then have [simp]: "f field_differentiable at a"
lp15@62533
  1914
    by (metis add.comm_neutral \<open>0 < r\<close> norm_eq_zero)
lp15@62533
  1915
  have hol1: "(\<lambda>z. f (a + z) - f a) holomorphic_on cball 0 r"
lp15@62533
  1916
    by (intro holomorphic_intros hol0)
lp15@62533
  1917
  then have "ball 0 ((3 - 2 * sqrt 2) * r * norm (deriv (\<lambda>z. f (a + z) - f a) 0))
lp15@62533
  1918
             \<subseteq> (\<lambda>z. f (a + z) - f a) ` ball 0 r"
lp15@62533
  1919
    apply (rule Bloch_lemma_0)
lp15@62533
  1920
    apply (simp_all add: \<open>0 < r\<close>)
lp15@62533
  1921
    apply (simp add: fz complex_derivative_chain)
lp15@62533
  1922
    apply (simp add: dist_norm le)
lp15@62533
  1923
    done
lp15@62533
  1924
  then show ?thesis
lp15@62533
  1925
    apply clarify
lp15@62533
  1926
    apply (drule_tac c="x - f a" in subsetD)
lp15@62534
  1927
     apply (force simp: fz \<open>0 < r\<close> dist_norm complex_derivative_chain field_differentiable_compose)+
lp15@62533
  1928
    done
lp15@62533
  1929
qed
lp15@62533
  1930
hoelzl@63594
  1931
proposition Bloch_unit:
lp15@62533
  1932
  assumes holf: "f holomorphic_on ball a 1" and [simp]: "deriv f a = 1"
lp15@62533
  1933
  obtains b r where "1/12 < r" "ball b r \<subseteq> f ` (ball a 1)"
lp15@62533
  1934
proof -
wenzelm@63040
  1935
  define r :: real where "r = 249/256"
lp15@62533
  1936
  have "0 < r" "r < 1" by (auto simp: r_def)
wenzelm@63040
  1937
  define g where "g z = deriv f z * of_real(r - norm(z - a))" for z
lp15@62533
  1938
  have "deriv f holomorphic_on ball a 1"
lp15@62533
  1939
    by (rule holomorphic_deriv [OF holf open_ball])
lp15@62533
  1940
  then have "continuous_on (ball a 1) (deriv f)"
lp15@62533
  1941
    using holomorphic_on_imp_continuous_on by blast
lp15@62533
  1942
  then have "continuous_on (cball a r) (deriv f)"
lp15@62533
  1943
    by (rule continuous_on_subset) (simp add: cball_subset_ball_iff \<open>r < 1\<close>)
lp15@62533
  1944
  then have "continuous_on (cball a r) g"
lp15@62533
  1945
    by (simp add: g_def continuous_intros)
lp15@62533
  1946
  then have 1: "compact (g ` cball a r)"
lp15@62533
  1947
    by (rule compact_continuous_image [OF _ compact_cball])
lp15@62533
  1948
  have 2: "g ` cball a r \<noteq> {}"
lp15@62533
  1949
    using \<open>r > 0\<close> by auto
hoelzl@63594
  1950
  obtain p where pr: "p \<in> cball a r"
lp15@62533
  1951
             and pge: "\<And>y. y \<in> cball a r \<Longrightarrow> norm (g y) \<le> norm (g p)"
lp15@62533
  1952
    using distance_attains_sup [OF 1 2, of 0] by force
wenzelm@63040
  1953
  define t where "t = (r - norm(p - a)) / 2"
lp15@62533
  1954
  have "norm (p - a) \<noteq> r"
lp15@62533
  1955
    using pge [of a] \<open>r > 0\<close> by (auto simp: g_def norm_mult)
hoelzl@63594
  1956
  then have "norm (p - a) < r" using pr
lp15@62533
  1957
    by (simp add: norm_minus_commute dist_norm)
hoelzl@63594
  1958
  then have "0 < t"
lp15@62533
  1959
    by (simp add: t_def)
lp15@62533
  1960
  have cpt: "cball p t \<subseteq> ball a r"
lp15@62533
  1961
    using \<open>0 < t\<close> by (simp add: cball_subset_ball_iff dist_norm t_def field_simps)
hoelzl@63594
  1962
  have gen_le_dfp: "norm (deriv f y) * (r - norm (y - a)) / (r - norm (p - a)) \<le> norm (deriv f p)"
lp15@62533
  1963
            if "y \<in> cball a r" for y
lp15@62533
  1964
  proof -
lp15@62533
  1965
    have [simp]: "norm (y - a) \<le> r"
hoelzl@63594
  1966
      using that by (simp add: dist_norm norm_minus_commute)
lp15@62533
  1967
    have "norm (g y) \<le> norm (g p)"
lp15@62533
  1968
      using pge [OF that] by simp
lp15@62533
  1969
    then have "norm (deriv f y) * abs (r - norm (y - a)) \<le> norm (deriv f p) * abs (r - norm (p - a))"
lp15@62533
  1970
      by (simp only: dist_norm g_def norm_mult norm_of_real)
lp15@62533
  1971
    with that \<open>norm (p - a) < r\<close> show ?thesis
lp15@62533
  1972
      by (simp add: dist_norm divide_simps)
lp15@62533
  1973
  qed
lp15@62533
  1974
  have le_norm_dfp: "r / (r - norm (p - a)) \<le> norm (deriv f p)"
lp15@62533
  1975
    using gen_le_dfp [of a] \<open>r > 0\<close> by auto
lp15@62533
  1976
  have 1: "f holomorphic_on cball p t"
lp15@62533
  1977
    apply (rule holomorphic_on_subset [OF holf])
lp15@62533
  1978
    using cpt \<open>r < 1\<close> order_subst1 subset_ball by auto
lp15@62533
  1979
  have 2: "norm (deriv f z) \<le> 2 * norm (deriv f p)" if "z \<in> ball p t" for z
lp15@62533
  1980
  proof -
lp15@62533
  1981
    have z: "z \<in> cball a r"
lp15@62533
  1982
      by (meson ball_subset_cball subsetD cpt that)
lp15@62533
  1983
    then have "norm(z - a) < r"
lp15@62533
  1984
      by (metis ball_subset_cball contra_subsetD cpt dist_norm mem_ball norm_minus_commute that)
hoelzl@63594
  1985
    have "norm (deriv f z) * (r - norm (z - a)) / (r - norm (p - a)) \<le> norm (deriv f p)"
lp15@62533
  1986
      using gen_le_dfp [OF z] by simp
hoelzl@63594
  1987
    with \<open>norm (z - a) < r\<close> \<open>norm (p - a) < r\<close>
lp15@62533
  1988
    have "norm (deriv f z) \<le> (r - norm (p - a)) / (r - norm (z - a)) * norm (deriv f p)"
lp15@62533
  1989
       by (simp add: field_simps)
lp15@62533
  1990
    also have "... \<le> 2 * norm (deriv f p)"
lp15@62533
  1991
      apply (rule mult_right_mono)
hoelzl@63594
  1992
      using that \<open>norm (p - a) < r\<close> \<open>norm(z - a) < r\<close>
lp15@62533
  1993
      apply (simp_all add: field_simps t_def dist_norm [symmetric])
lp15@62533
  1994
      using dist_triangle3 [of z a p] by linarith
lp15@62533
  1995
    finally show ?thesis .
lp15@62533
  1996
  qed
lp15@62533
  1997
  have sqrt2: "sqrt 2 < 2113/1494"
lp15@62533
  1998
    by (rule real_less_lsqrt) (auto simp: power2_eq_square)
lp15@62533
  1999
  then have sq3: "0 < 3 - 2 * sqrt 2" by simp
lp15@62533
  2000
  have "1 / 12 / ((3 - 2 * sqrt 2) / 2) < r"
hoelzl@63594
  2001
    using sq3 sqrt2 by (auto simp: field_simps r_def)
lp15@62533
  2002
  also have "... \<le> cmod (deriv f p) * (r - cmod (p - a))"
hoelzl@63594
  2003
    using \<open>norm (p - a) < r\<close> le_norm_dfp   by (simp add: pos_divide_le_eq)
hoelzl@63594
  2004
  finally have "1 / 12 < cmod (deriv f p) * (r - cmod (p - a)) * ((3 - 2 * sqrt 2) / 2)"
lp15@62533
  2005
    using pos_divide_less_eq half_gt_zero_iff sq3 by blast
lp15@62533
  2006
  then have **: "1 / 12 < (3 - 2 * sqrt 2) * t * norm (deriv f p)"
lp15@62533
  2007
    using sq3 by (simp add: mult.commute t_def)
lp15@62533
  2008
  have "ball (f p) ((3 - 2 * sqrt 2) * t * norm (deriv f p)) \<subseteq> f ` ball p t"
lp15@62533
  2009
    by (rule Bloch_lemma [OF 1 \<open>0 < t\<close> 2])
lp15@62533
  2010
  also have "... \<subseteq> f ` ball a 1"
lp15@62533
  2011
    apply (rule image_mono)
lp15@62533
  2012
    apply (rule order_trans [OF ball_subset_cball])
lp15@62533
  2013
    apply (rule order_trans [OF cpt])
lp15@62533
  2014
    using \<open>0 < t\<close> \<open>r < 1\<close> apply (simp add: ball_subset_ball_iff dist_norm)
lp15@62533
  2015
    done
lp15@62533
  2016
  finally have "ball (f p) ((3 - 2 * sqrt 2) * t * norm (deriv f p)) \<subseteq> f ` ball a 1" .
lp15@62533
  2017
  with ** show ?thesis
lp15@62533
  2018
    by (rule that)
lp15@62533
  2019
qed
lp15@62533
  2020
lp15@62533
  2021
lp15@62533
  2022
theorem Bloch:
hoelzl@63594
  2023
  assumes holf: "f holomorphic_on ball a r" and "0 < r"
lp15@62533
  2024
      and r': "r' \<le> r * norm (deriv f a) / 12"
lp15@62533
  2025
  obtains b where "ball b r' \<subseteq> f ` (ball a r)"
lp15@62533
  2026
proof (cases "deriv f a = 0")
lp15@62533
  2027
  case True with r' show ?thesis
lp15@62533
  2028
    using ball_eq_empty that by fastforce
lp15@62533
  2029
next
lp15@62533
  2030
  case False
wenzelm@63040
  2031
  define C where "C = deriv f a"
wenzelm@63040
  2032
  have "0 < norm C" using False by (simp add: C_def)
wenzelm@63040
  2033
  have dfa: "f field_differentiable at a"
wenzelm@63040
  2034
    apply (rule holomorphic_on_imp_differentiable_at [OF holf])
wenzelm@63040
  2035
    using \<open>0 < r\<close> by auto
wenzelm@63040
  2036
  have fo: "(\<lambda>z. f (a + of_real r * z)) = f o (\<lambda>z. (a + of_real r * z))"
wenzelm@63040
  2037
    by (simp add: o_def)
wenzelm@63040
  2038
  have holf': "f holomorphic_on (\<lambda>z. a + complex_of_real r * z) ` ball 0 1"
wenzelm@63040
  2039
    apply (rule holomorphic_on_subset [OF holf])
wenzelm@63040
  2040
    using \<open>0 < r\<close> apply (force simp: dist_norm norm_mult)
wenzelm@63040
  2041
    done
wenzelm@63040
  2042
  have 1: "(\<lambda>z. f (a + r * z) / (C * r)) holomorphic_on ball 0 1"
wenzelm@63040
  2043
    apply (rule holomorphic_intros holomorphic_on_compose holf' | simp add: fo)+
wenzelm@63040
  2044
    using \<open>0 < r\<close> by (simp add: C_def False)
wenzelm@63040
  2045
  have "((\<lambda>z. f (a + of_real r * z) / (C * of_real r)) has_field_derivative
hoelzl@63594
  2046
        (deriv f (a + of_real r * z) / C)) (at z)"
wenzelm@63040
  2047
       if "norm z < 1" for z
wenzelm@63040
  2048
  proof -
lp15@62533
  2049
    have *: "((\<lambda>x. f (a + of_real r * x)) has_field_derivative
wenzelm@63040
  2050
           (deriv f (a + of_real r * z) * of_real r)) (at z)"
wenzelm@63040
  2051
      apply (simp add: fo)
lp15@62534
  2052
      apply (rule DERIV_chain [OF field_differentiable_derivI])
wenzelm@63040
  2053
      apply (rule holomorphic_on_imp_differentiable_at [OF holf], simp)
wenzelm@63040
  2054
      using \<open>0 < r\<close> apply (simp add: dist_norm norm_mult that)
wenzelm@63040
  2055
      apply (rule derivative_eq_intros | simp)+
lp15@62533
  2056
      done
lp15@62533
  2057
    show ?thesis
wenzelm@63040
  2058
      apply (rule derivative_eq_intros * | simp)+
wenzelm@63040
  2059
      using \<open>0 < r\<close> by (auto simp: C_def False)
wenzelm@63040
  2060
  qed
wenzelm@63040
  2061
  have 2: "deriv (\<lambda>z. f (a + of_real r * z) / (C * of_real r)) 0 = 1"
wenzelm@63040
  2062
    apply (subst deriv_cdivide_right)
wenzelm@63040
  2063
    apply (simp add: field_differentiable_def fo)
wenzelm@63040
  2064
    apply (rule exI)
wenzelm@63040
  2065
    apply (rule DERIV_chain [OF field_differentiable_derivI])
wenzelm@63040
  2066
    apply (simp add: dfa)
wenzelm@63040
  2067
    apply (rule derivative_eq_intros | simp add: C_def False fo)+
hoelzl@63594
  2068
    using \<open>0 < r\<close>
wenzelm@63040
  2069
    apply (simp add: C_def False fo)
wenzelm@63040
  2070
    apply (simp add: derivative_intros dfa complex_derivative_chain)
wenzelm@63040
  2071
    done
hoelzl@63594
  2072
  have sb1: "op * (C * r) ` (\<lambda>z. f (a + of_real r * z) / (C * r)) ` ball 0 1
wenzelm@63040
  2073
             \<subseteq> f ` ball a r"
wenzelm@63040
  2074
    using \<open>0 < r\<close> by (auto simp: dist_norm norm_mult C_def False)
hoelzl@63594
  2075
  have sb2: "ball (C * r * b) r' \<subseteq> op * (C * r) ` ball b t"
wenzelm@63040
  2076
             if "1 / 12 < t" for b t
wenzelm@63040
  2077
  proof -
wenzelm@63040
  2078
    have *: "r * cmod (deriv f a) / 12 \<le> r * (t * cmod (deriv f a))"
hoelzl@63594
  2079
      using that \<open>0 < r\<close> less_eq_real_def mult.commute mult.right_neutral mult_left_mono norm_ge_zero times_divide_eq_right
wenzelm@63040
  2080
      by auto
wenzelm@63040
  2081
    show ?thesis
wenzelm@63040
  2082
      apply clarify
wenzelm@63040
  2083
      apply (rule_tac x="x / (C * r)" in image_eqI)
hoelzl@63594
  2084
      using \<open>0 < r\<close>
wenzelm@63040
  2085
      apply (simp_all add: dist_norm norm_mult norm_divide C_def False field_simps)
wenzelm@63040
  2086
      apply (erule less_le_trans)
wenzelm@63040
  2087
      apply (rule order_trans [OF r' *])
lp15@62533
  2088
      done
wenzelm@63040
  2089
  qed
wenzelm@63040
  2090
  show ?thesis
wenzelm@63040
  2091
    apply (rule Bloch_unit [OF 1 2])
wenzelm@63040
  2092
    apply (rename_tac t)
wenzelm@63040
  2093
    apply (rule_tac b="(C * of_real r) * b" in that)
wenzelm@63040
  2094
    apply (drule image_mono [where f = "\<lambda>z. (C * of_real r) * z"])
wenzelm@63040
  2095
    using sb1 sb2
wenzelm@63040
  2096
    apply force
wenzelm@63040
  2097
    done
lp15@62533
  2098
qed
lp15@62533
  2099
lp15@62533
  2100
corollary Bloch_general:
hoelzl@63594
  2101
  assumes holf: "f holomorphic_on s" and "a \<in> s"
lp15@62533
  2102
      and tle: "\<And>z. z \<in> frontier s \<Longrightarrow> t \<le> dist a z"
lp15@62533
  2103
      and rle: "r \<le> t * norm(deriv f a) / 12"
lp15@62533
  2104
  obtains b where "ball b r \<subseteq> f ` s"
lp15@62533
  2105
proof -
lp15@62533
  2106
  consider "r \<le> 0" | "0 < t * norm(deriv f a) / 12" using rle by force
lp15@62533
  2107
  then show ?thesis
lp15@62533
  2108
  proof cases
lp15@62533
  2109
    case 1 then show ?thesis
lp15@62533
  2110
      by (simp add: Topology_Euclidean_Space.ball_empty that)
lp15@62533
  2111
  next
lp15@62533
  2112
    case 2
lp15@62533
  2113
    show ?thesis
lp15@62533
  2114
    proof (cases "deriv f a = 0")
lp15@62533
  2115
      case True then show ?thesis
lp15@62533
  2116
        using rle by (simp add: Topology_Euclidean_Space.ball_empty that)
lp15@62533
  2117
    next
lp15@62533
  2118
      case False
lp15@62533
  2119
      then have "t > 0"
lp15@62533
  2120
        using 2 by (force simp: zero_less_mult_iff)
lp15@62533
  2121
      have "~ ball a t \<subseteq> s \<Longrightarrow> ball a t \<inter> frontier s \<noteq> {}"
lp15@62533
  2122
        apply (rule connected_Int_frontier [of "ball a t" s], simp_all)
lp15@62533
  2123
        using \<open>0 < t\<close> \<open>a \<in> s\<close> centre_in_ball apply blast
lp15@62533
  2124
        done
lp15@62533
  2125
      with tle have *: "ball a t \<subseteq> s" by fastforce
lp15@62533
  2126
      then have 1: "f holomorphic_on ball a t"
lp15@62533
  2127
        using holf using holomorphic_on_subset by blast
lp15@62533
  2128
      show ?thesis
lp15@62533
  2129
        apply (rule Bloch [OF 1 \<open>t > 0\<close> rle])
lp15@62533
  2130
        apply (rule_tac b=b in that)
lp15@62533
  2131
        using * apply force
lp15@62533
  2132
        done
lp15@62533
  2133
    qed
lp15@62533
  2134
  qed
lp15@62533
  2135
qed
lp15@62533
  2136
lp15@63151
  2137
subsection \<open>Foundations of Cauchy's residue theorem\<close>
lp15@62540
  2138
lp15@63151
  2139
text\<open>Wenda Li and LC Paulson (2016). A Formal Proof of Cauchy's Residue Theorem.
lp15@63151
  2140
    Interactive Theorem Proving\<close>
lp15@62540
  2141
lp15@63151
  2142
definition residue :: "(complex \<Rightarrow> complex) \<Rightarrow> complex \<Rightarrow> complex" where
hoelzl@63594
  2143
  "residue f z = (SOME int. \<exists>e>0. \<forall>\<epsilon>>0. \<epsilon><e
wenzelm@63589
  2144
    \<longrightarrow> (f has_contour_integral 2*pi* \<i> *int) (circlepath z \<epsilon>))"
lp15@62540
  2145
lp15@63151
  2146
lemma contour_integral_circlepath_eq:
hoelzl@63594
  2147
  assumes "open s" and f_holo:"f holomorphic_on (s-{z})" and "0<e1" "e1\<le>e2"
lp15@63151
  2148
    and e2_cball:"cball z e2 \<subseteq> s"
lp15@63151
  2149
  shows
lp15@63151
  2150
    "f contour_integrable_on circlepath z e1"
lp15@63151
  2151
    "f contour_integrable_on circlepath z e2"
lp15@63151
  2152
    "contour_integral (circlepath z e2) f = contour_integral (circlepath z e1) f"
lp15@62540
  2153
proof -
lp15@63151
  2154
  define l where "l \<equiv> linepath (z+e2) (z+e1)"
lp15@63151
  2155
  have [simp]:"valid_path l" "pathstart l=z+e2" "pathfinish l=z+e1" unfolding l_def by auto
lp15@63151
  2156
  have "e2>0" using \<open>e1>0\<close> \<open>e1\<le>e2\<close> by auto
lp15@63151
  2157
  have zl_img:"z\<notin>path_image l"
hoelzl@63594
  2158
    proof
lp15@63151
  2159
      assume "z \<in> path_image l"
lp15@63151
  2160
      then have "e2 \<le> cmod (e2 - e1)"
lp15@63151
  2161
        using segment_furthest_le[of z "z+e2" "z+e1" "z+e2",simplified] \<open>e1>0\<close> \<open>e2>0\<close> unfolding l_def
lp15@63151
  2162
        by (auto simp add:closed_segment_commute)
hoelzl@63594
  2163
      thus False using \<open>e2>0\<close> \<open>e1>0\<close> \<open>e1\<le>e2\<close>
lp15@63151
  2164
        apply (subst (asm) norm_of_real)
lp15@63151
  2165
        by auto
lp15@63151
  2166
    qed
lp15@63151
  2167
  define g where "g \<equiv> circlepath z e2 +++ l +++ reversepath (circlepath z e1) +++ reversepath l"
hoelzl@63594
  2168
  show [simp]: "f contour_integrable_on circlepath z e2" "f contour_integrable_on (circlepath z e1)"
lp15@62540
  2169
    proof -
hoelzl@63594
  2170
      show "f contour_integrable_on circlepath z e2"
hoelzl@63594
  2171
        apply (intro contour_integrable_continuous_circlepath[OF
lp15@63151
  2172
                continuous_on_subset[OF holomorphic_on_imp_continuous_on[OF f_holo]]])
lp15@63151
  2173
        using \<open>e2>0\<close> e2_cball by auto
hoelzl@63594
  2174
      show "f contour_integrable_on (circlepath z e1)"
hoelzl@63594
  2175
        apply (intro contour_integrable_continuous_circlepath[OF
lp15@63151
  2176
                      continuous_on_subset[OF holomorphic_on_imp_continuous_on[OF f_holo]]])
lp15@63151
  2177
        using \<open>e1>0\<close> \<open>e1\<le>e2\<close> e2_cball by auto
lp15@63151
  2178
    qed
lp15@63151
  2179
  have [simp]:"f contour_integrable_on l"
lp15@63151
  2180
    proof -