# HG changeset patch # User eberlm # Date 1502454570 -7200 # Node ID 32084d7e6b598414e500e03f89ed6dbad450c3dd # Parent 2a6371fb31f053bd54ab02f730c53f0b5fb9f945 Some facts about orders of zeros diff -r 2a6371fb31f0 -r 32084d7e6b59 src/HOL/Analysis/Conformal_Mappings.thy --- a/src/HOL/Analysis/Conformal_Mappings.thy Thu Aug 10 13:37:27 2017 +0200 +++ b/src/HOL/Analysis/Conformal_Mappings.thy Fri Aug 11 14:29:30 2017 +0200 @@ -3141,6 +3141,160 @@ ultimately show ?thesis using \n>0\ unfolding P_def by auto qed +lemma zorder_eqI: + assumes "open s" "z \ s" "g holomorphic_on s" "g z \ 0" "n > 0" + assumes "\w. w \ s \ f w = g w * (w - z) ^ n" + shows "zorder f z = n" +proof - + have "continuous_on s g" by (rule holomorphic_on_imp_continuous_on) fact + moreover have "open (-{0::complex})" by auto + ultimately have "open ((g -` (-{0})) \ s)" + unfolding continuous_on_open_vimage[OF \open s\] by blast + moreover from assms have "z \ (g -` (-{0})) \ s" by auto + ultimately obtain r where r: "r > 0" "cball z r \ (g -` (-{0})) \ s" + unfolding open_contains_cball by blast + + have "n > 0 \ r > 0 \ g holomorphic_on cball z r \ + (\w\cball z r. f w = (w - z) ^ n * g w \ g w \ 0)" (is "?P g r n") + using r assms(3,5,6) by auto + hence ex: "\g r. ?P g r n" by blast + have unique: "\!n. \g r. ?P g r n" + proof (rule holomorphic_factor_zero_Ex1) + from r have "(\w. g w * (w - z) ^ n) holomorphic_on ball z r" + by (intro holomorphic_intros holomorphic_on_subset[OF assms(3)]) auto + also have "?this \ f holomorphic_on ball z r" + using r assms by (intro holomorphic_cong refl) (auto simp: cball_def subset_iff) + finally show \ . + next + let ?w = "z + of_real r / 2" + have "?w \ ball z r" + using r by (auto simp: dist_norm) + moreover from this and r have "g ?w \ 0" and "?w \ s" + by (auto simp: cball_def ball_def subset_iff) + with assms have "f ?w \ 0" using \r > 0\ by auto + ultimately show "\w\ball z r. f w \ 0" by blast + qed (insert assms r, auto) + from unique and ex have "(THE n. \g r. ?P g r n) = n" + by (rule the1_equality) + also have "(THE n. \g r. ?P g r n) = zorder f z" + by (simp add: zorder_def mult.commute) + finally show ?thesis . +qed + +lemma simple_zeroI: + assumes "open s" "z \ s" "g holomorphic_on s" "g z \ 0" + assumes "\w. w \ s \ f w = g w * (w - z)" + shows "zorder f z = 1" + using assms(1-4) by (rule zorder_eqI) (use assms(5) in auto) + +lemma higher_deriv_power: + shows "(deriv ^^ j) (\w. (w - z) ^ n) w = + pochhammer (of_nat (Suc n - j)) j * (w - z) ^ (n - j)" +proof (induction j arbitrary: w) + case 0 + thus ?case by auto +next + case (Suc j w) + have "(deriv ^^ Suc j) (\w. (w - z) ^ n) w = deriv ((deriv ^^ j) (\w. (w - z) ^ n)) w" + by simp + also have "(deriv ^^ j) (\w. (w - z) ^ n) = + (\w. pochhammer (of_nat (Suc n - j)) j * (w - z) ^ (n - j))" + using Suc by (intro Suc.IH ext) + also { + have "(\ has_field_derivative of_nat (n - j) * + pochhammer (of_nat (Suc n - j)) j * (w - z) ^ (n - Suc j)) (at w)" + using Suc.prems by (auto intro!: derivative_eq_intros) + also have "of_nat (n - j) * pochhammer (of_nat (Suc n - j)) j = + pochhammer (of_nat (Suc n - Suc j)) (Suc j)" + by (cases "Suc j \ n", subst pochhammer_rec) + (insert Suc.prems, simp_all add: algebra_simps Suc_diff_le pochhammer_0_left) + finally have "deriv (\w. pochhammer (of_nat (Suc n - j)) j * (w - z) ^ (n - j)) w = + \ * (w - z) ^ (n - Suc j)" + by (rule DERIV_imp_deriv) + } + finally show ?case . +qed + +lemma zorder_eqI': + assumes "open s" "connected s" "z \ s" "f holomorphic_on s" + assumes zero: "\i. i < n' \ (deriv ^^ i) f z = 0" + assumes nz: "(deriv ^^ n') f z \ 0" and n: "n' > 0" + shows "zorder f z = n'" +proof - + { + assume *: "\w. w \ s \ f w = 0" + hence "eventually (\u. u \ s) (nhds z)" + using assms by (intro eventually_nhds_in_open) auto + hence "eventually (\u. f u = 0) (nhds z)" + by eventually_elim (simp_all add: *) + hence "(deriv ^^ n') f z = (deriv ^^ n') (\_. 0) z" + by (intro higher_deriv_cong_ev) auto + also have "(deriv ^^ n') (\_. 0) z = 0" + by (induction n') simp_all + finally have False using nz by contradiction + } + hence nz': "\w\s. f w \ 0" by blast + + from zero[of 0] and n have [simp]: "f z = 0" by simp + + define n g where "n = zorder f z" and "g = zer_poly f z" + from zorder_exist[OF assms(1-4) \f z = 0\ nz'] + obtain r where r: "n > 0" "r > 0" "cball z r \ s" "g holomorphic_on cball z r" + "\w\cball z r. f w = g w * (w - z) ^ n \ g w \ 0" + unfolding n_def g_def by blast + + define A where "A = (\i. of_nat (i choose n) * fact n * (deriv ^^ (i - n)) g z)" + { + fix i :: nat + have "eventually (\w. w \ ball z r) (nhds z)" + using r by (intro eventually_nhds_in_open) auto + hence "eventually (\w. f w = (w - z) ^ n * g w) (nhds z)" + by eventually_elim (use r in auto) + hence "(deriv ^^ i) f z = (deriv ^^ i) (\w. (w - z) ^ n * g w) z" + by (intro higher_deriv_cong_ev) auto + also have "\ = (\j=0..i. of_nat (i choose j) * + (deriv ^^ j) (\w. (w - z) ^ n) z * (deriv ^^ (i - j)) g z)" + using r by (intro higher_deriv_mult[of _ "ball z r"]) (auto intro!: holomorphic_intros) + also have "\ = (\j=0..i. if j = n then of_nat (i choose n) * fact n * (deriv ^^ (i - n)) g z + else 0)" + proof (intro sum.cong refl, goal_cases) + case (1 j) + have "(deriv ^^ j) (\w. (w - z) ^ n) z = + pochhammer (of_nat (Suc n - j)) j * 0 ^ (n - j)" + by (subst higher_deriv_power) auto + also have "\ = (if j = n then fact j else 0)" + by (auto simp: not_less pochhammer_0_left pochhammer_fact) + also have "of_nat (i choose j) * \ * (deriv ^^ (i - j)) g z = + (if j = n then of_nat (i choose n) * fact n * (deriv ^^ (i - n)) g z else 0)" + by simp + finally show ?case . + qed + also have "\ = (if i \ n then A i else 0)" + by (auto simp: A_def) + finally have "(deriv ^^ i) f z = \" . + } note * = this + + from *[of n] and r have "(deriv ^^ n) f z \ 0" + by (simp add: A_def) + with zero[of n] have "n \ n'" by (cases "n \ n'") auto + with nz show "n = n'" + by (auto simp: * split: if_splits) +qed + +lemma simple_zeroI': + assumes "open s" "connected s" "z \ s" + assumes "\z. z \ s \ (f has_field_derivative f' z) (at z)" + assumes "f z = 0" "f' z \ 0" + shows "zorder f z = 1" +proof - + have "deriv f z = f' z" if "z \ s" for z + using that by (intro DERIV_imp_deriv assms) auto + moreover from assms have "f holomorphic_on s" + by (subst holomorphic_on_open) auto + ultimately show ?thesis using assms + by (intro zorder_eqI'[of s]) auto +qed + lemma porder_exist: fixes f::"complex \ complex" and z::complex defines "n \ porder f z" and "h \ pol_poly f z" diff -r 2a6371fb31f0 -r 32084d7e6b59 src/HOL/Analysis/Derivative.thy --- a/src/HOL/Analysis/Derivative.thy Thu Aug 10 13:37:27 2017 +0200 +++ b/src/HOL/Analysis/Derivative.thy Fri Aug 11 14:29:30 2017 +0200 @@ -2421,6 +2421,22 @@ thus ?thesis by (simp add: deriv_def assms) qed +lemma higher_deriv_cong_ev: + assumes "eventually (\x. f x = g x) (nhds x)" "x = y" + shows "(deriv ^^ n) f x = (deriv ^^ n) g y" +proof - + from assms(1) have "eventually (\x. (deriv ^^ n) f x = (deriv ^^ n) g x) (nhds x)" + proof (induction n arbitrary: f g) + case (Suc n) + from Suc.prems have "eventually (\y. eventually (\z. f z = g z) (nhds y)) (nhds x)" + by (simp add: eventually_eventually) + hence "eventually (\x. deriv f x = deriv g x) (nhds x)" + by eventually_elim (rule deriv_cong_ev, simp_all) + thus ?case by (auto intro!: deriv_cong_ev Suc simp: funpow_Suc_right simp del: funpow.simps) + qed auto + from eventually_nhds_x_imp_x[OF this] assms(2) show ?thesis by simp +qed + lemma real_derivative_chain: fixes x :: real shows "f differentiable at x \ g differentiable at (f x) diff -r 2a6371fb31f0 -r 32084d7e6b59 src/HOL/Factorial.thy --- a/src/HOL/Factorial.thy Thu Aug 10 13:37:27 2017 +0200 +++ b/src/HOL/Factorial.thy Fri Aug 11 14:29:30 2017 +0200 @@ -264,6 +264,10 @@ pochhammer_of_nat_eq_0_lemma'[of k n, where ?'a = 'a] by (auto simp add: not_le[symmetric]) +lemma pochhammer_0_left: + "pochhammer 0 n = (if n = 0 then 1 else 0)" + by (induction n) (simp_all add: pochhammer_rec) + lemma pochhammer_eq_0_iff: "pochhammer a n = (0::'a::field_char_0) \ (\k < n. a = - of_nat k)" by (auto simp add: pochhammer_prod eq_neg_iff_add_eq_0)