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