equal
deleted
inserted
replaced
1451 moreover have "norm c = 1" using df0 c by auto |
1451 moreover have "norm c = 1" using df0 c by auto |
1452 ultimately show ?thesis |
1452 ultimately show ?thesis |
1453 using fz_eq by auto |
1453 using fz_eq by auto |
1454 qed |
1454 qed |
1455 qed |
1455 qed |
|
1456 |
|
1457 corollary Schwarz_Lemma': |
|
1458 assumes holf: "f holomorphic_on (ball 0 1)" and [simp]: "f 0 = 0" |
|
1459 and no: "\<And>z. norm z < 1 \<Longrightarrow> norm (f z) < 1" |
|
1460 shows "((\<forall>\<xi>. norm \<xi> < 1 \<longrightarrow> norm (f \<xi>) \<le> norm \<xi>) \<and> norm(deriv f 0) \<le> 1) \<and> |
|
1461 (((\<exists>z. norm z < 1 \<and> z \<noteq> 0 \<and> norm(f z) = norm z) \<or> norm(deriv f 0) = 1) |
|
1462 \<longrightarrow> (\<exists>\<alpha>. (\<forall>z. norm z < 1 \<longrightarrow> f z = \<alpha> * z) \<and> norm \<alpha> = 1))" |
|
1463 using Schwarz_Lemma [OF assms] |
|
1464 by (metis (no_types) norm_eq_zero zero_less_one) |
1456 |
1465 |
1457 subsection\<open>The Schwarz reflection principle\<close> |
1466 subsection\<open>The Schwarz reflection principle\<close> |
1458 |
1467 |
1459 lemma hol_pal_lem0: |
1468 lemma hol_pal_lem0: |
1460 assumes "d \<bullet> a \<le> k" "k \<le> d \<bullet> b" |
1469 assumes "d \<bullet> a \<le> k" "k \<le> d \<bullet> b" |