src/HOL/Analysis/Conformal_Mappings.thy
changeset 66793 deabce3ccf1f
parent 66660 bc3584f7ac0c
child 66827 c94531b5007d
     1.1 --- a/src/HOL/Analysis/Conformal_Mappings.thy	Sun Oct 08 16:50:37 2017 +0200
     1.2 +++ b/src/HOL/Analysis/Conformal_Mappings.thy	Mon Oct 09 15:34:23 2017 +0100
     1.3 @@ -1454,6 +1454,15 @@
     1.4    qed
     1.5  qed
     1.6  
     1.7 +corollary Schwarz_Lemma':
     1.8 +  assumes holf: "f holomorphic_on (ball 0 1)" and [simp]: "f 0 = 0"
     1.9 +      and no: "\<And>z. norm z < 1 \<Longrightarrow> norm (f z) < 1"
    1.10 +    shows "((\<forall>\<xi>. norm \<xi> < 1 \<longrightarrow> norm (f \<xi>) \<le> norm \<xi>) \<and> norm(deriv f 0) \<le> 1) \<and>
    1.11 +           (((\<exists>z. norm z < 1 \<and> z \<noteq> 0 \<and> norm(f z) = norm z) \<or> norm(deriv f 0) = 1)
    1.12 +           \<longrightarrow> (\<exists>\<alpha>. (\<forall>z. norm z < 1 \<longrightarrow> f z = \<alpha> * z) \<and> norm \<alpha> = 1))"
    1.13 +  using Schwarz_Lemma [OF assms]
    1.14 +  by (metis (no_types) norm_eq_zero zero_less_one)
    1.15 +
    1.16  subsection\<open>The Schwarz reflection principle\<close>
    1.17  
    1.18  lemma hol_pal_lem0: