1 section \<open>Complex Transcendental Functions\<close> |
1 section \<open>Complex Transcendental Functions\<close> |
2 |
2 |
3 text\<open>By John Harrison et al. Ported from HOL Light by L C Paulson (2015)\<close> |
3 text\<open>By John Harrison et al. Ported from HOL Light by L C Paulson (2015)\<close> |
4 |
4 |
5 theory Complex_Transcendental |
5 theory Complex_Transcendental |
6 imports Complex_Analysis_Basics |
6 imports |
|
7 Complex_Analysis_Basics |
|
8 Summation |
7 begin |
9 begin |
|
10 |
|
11 (* TODO: Figure out what to do with Möbius transformations *) |
|
12 definition "moebius a b c d = (\<lambda>z. (a*z+b) / (c*z+d :: 'a :: field))" |
|
13 |
|
14 lemma moebius_inverse: |
|
15 assumes "a * d \<noteq> b * c" "c * z + d \<noteq> 0" |
|
16 shows "moebius d (-b) (-c) a (moebius a b c d z) = z" |
|
17 proof - |
|
18 from assms have "(-c) * moebius a b c d z + a \<noteq> 0" unfolding moebius_def |
|
19 by (simp add: field_simps) |
|
20 with assms show ?thesis |
|
21 unfolding moebius_def by (simp add: moebius_def divide_simps) (simp add: algebra_simps)? |
|
22 qed |
|
23 |
|
24 lemma moebius_inverse': |
|
25 assumes "a * d \<noteq> b * c" "c * z - a \<noteq> 0" |
|
26 shows "moebius a b c d (moebius d (-b) (-c) a z) = z" |
|
27 using assms moebius_inverse[of d a "-b" "-c" z] |
|
28 by (auto simp: algebra_simps) |
|
29 |
|
30 |
8 |
31 |
9 lemma cmod_add_real_less: |
32 lemma cmod_add_real_less: |
10 assumes "Im z \<noteq> 0" "r\<noteq>0" |
33 assumes "Im z \<noteq> 0" "r\<noteq>0" |
11 shows "cmod (z + r) < cmod z + \<bar>r\<bar>" |
34 shows "cmod (z + r) < cmod z + \<bar>r\<bar>" |
12 proof (cases z) |
35 proof (cases z) |
1325 apply (rule Lim_transform_within_open [of "-{z. z \<in> \<real> & 0 \<le> Re z}" _ "\<lambda>z. Im(Ln(-z)) + pi"]) |
1348 apply (rule Lim_transform_within_open [of "-{z. z \<in> \<real> & 0 \<le> Re z}" _ "\<lambda>z. Im(Ln(-z)) + pi"]) |
1326 apply (simp add: closed_def [symmetric] closed_Collect_conj closed_complex_Reals closed_halfspace_Re_ge) |
1349 apply (simp add: closed_def [symmetric] closed_Collect_conj closed_complex_Reals closed_halfspace_Re_ge) |
1327 apply (simp_all add: assms not_le Arg_Ln [OF Arg_gt_0]) |
1350 apply (simp_all add: assms not_le Arg_Ln [OF Arg_gt_0]) |
1328 done |
1351 done |
1329 qed |
1352 qed |
|
1353 |
|
1354 lemma Ln_series: |
|
1355 fixes z :: complex |
|
1356 assumes "norm z < 1" |
|
1357 shows "(\<lambda>n. (-1)^Suc n / of_nat n * z^n) sums ln (1 + z)" (is "(\<lambda>n. ?f n * z^n) sums _") |
|
1358 proof - |
|
1359 let ?F = "\<lambda>z. \<Sum>n. ?f n * z^n" and ?F' = "\<lambda>z. \<Sum>n. diffs ?f n * z^n" |
|
1360 have r: "conv_radius ?f = 1" |
|
1361 by (intro conv_radius_ratio_limit_nonzero[of _ 1]) |
|
1362 (simp_all add: norm_divide LIMSEQ_Suc_n_over_n del: of_nat_Suc) |
|
1363 |
|
1364 have "\<exists>c. \<forall>z\<in>ball 0 1. ln (1 + z) - ?F z = c" |
|
1365 proof (rule has_field_derivative_zero_constant) |
|
1366 fix z :: complex assume z': "z \<in> ball 0 1" |
|
1367 hence z: "norm z < 1" by (simp add: dist_0_norm) |
|
1368 def t \<equiv> "of_real (1 + norm z) / 2 :: complex" |
|
1369 from z have t: "norm z < norm t" "norm t < 1" unfolding t_def |
|
1370 by (simp_all add: field_simps norm_divide del: of_real_add) |
|
1371 |
|
1372 have "Re (-z) \<le> norm (-z)" by (rule complex_Re_le_cmod) |
|
1373 also from z have "... < 1" by simp |
|
1374 finally have "((\<lambda>z. ln (1 + z)) has_field_derivative inverse (1+z)) (at z)" |
|
1375 by (auto intro!: derivative_eq_intros) |
|
1376 moreover have "(?F has_field_derivative ?F' z) (at z)" using t r |
|
1377 by (intro termdiffs_strong[of _ t] summable_in_conv_radius) simp_all |
|
1378 ultimately have "((\<lambda>z. ln (1 + z) - ?F z) has_field_derivative (inverse (1 + z) - ?F' z)) |
|
1379 (at z within ball 0 1)" |
|
1380 by (intro derivative_intros) (simp_all add: at_within_open[OF z']) |
|
1381 also have "(\<lambda>n. of_nat n * ?f n * z ^ (n - Suc 0)) sums ?F' z" using t r |
|
1382 by (intro diffs_equiv termdiff_converges[OF t(1)] summable_in_conv_radius) simp_all |
|
1383 from sums_split_initial_segment[OF this, of 1] |
|
1384 have "(\<lambda>i. (-z) ^ i) sums ?F' z" by (simp add: power_minus[of z] del: of_nat_Suc) |
|
1385 hence "?F' z = inverse (1 + z)" using z by (simp add: sums_iff suminf_geometric divide_inverse) |
|
1386 also have "inverse (1 + z) - inverse (1 + z) = 0" by simp |
|
1387 finally show "((\<lambda>z. ln (1 + z) - ?F z) has_field_derivative 0) (at z within ball 0 1)" . |
|
1388 qed simp_all |
|
1389 then obtain c where c: "\<And>z. z \<in> ball 0 1 \<Longrightarrow> ln (1 + z) - ?F z = c" by blast |
|
1390 from c[of 0] have "c = 0" by (simp only: powser_zero) simp |
|
1391 with c[of z] assms have "ln (1 + z) = ?F z" by (simp add: dist_0_norm) |
|
1392 moreover have "summable (\<lambda>n. ?f n * z^n)" using assms r |
|
1393 by (intro summable_in_conv_radius) simp_all |
|
1394 ultimately show ?thesis by (simp add: sums_iff) |
|
1395 qed |
|
1396 |
|
1397 lemma Ln_approx_linear: |
|
1398 fixes z :: complex |
|
1399 assumes "norm z < 1" |
|
1400 shows "norm (ln (1 + z) - z) \<le> norm z^2 / (1 - norm z)" |
|
1401 proof - |
|
1402 let ?f = "\<lambda>n. (-1)^Suc n / of_nat n" |
|
1403 from assms have "(\<lambda>n. ?f n * z^n) sums ln (1 + z)" using Ln_series by simp |
|
1404 moreover have "(\<lambda>n. (if n = 1 then 1 else 0) * z^n) sums z" using powser_sums_if[of 1] by simp |
|
1405 ultimately have "(\<lambda>n. (?f n - (if n = 1 then 1 else 0)) * z^n) sums (ln (1 + z) - z)" |
|
1406 by (subst left_diff_distrib, intro sums_diff) simp_all |
|
1407 from sums_split_initial_segment[OF this, of "Suc 1"] |
|
1408 have "(\<lambda>i. (-(z^2)) * inverse (2 + of_nat i) * (- z)^i) sums (Ln (1 + z) - z)" |
|
1409 by (simp add: power2_eq_square mult_ac power_minus[of z] divide_inverse) |
|
1410 hence "(Ln (1 + z) - z) = (\<Sum>i. (-(z^2)) * inverse (of_nat (i+2)) * (-z)^i)" |
|
1411 by (simp add: sums_iff) |
|
1412 also have A: "summable (\<lambda>n. norm z^2 * (inverse (real_of_nat (Suc (Suc n))) * cmod z ^ n))" |
|
1413 by (rule summable_mult, rule summable_comparison_test_ev[OF _ summable_geometric[of "norm z"]]) |
|
1414 (auto simp: assms field_simps intro!: always_eventually) |
|
1415 hence "norm (\<Sum>i. (-(z^2)) * inverse (of_nat (i+2)) * (-z)^i) \<le> |
|
1416 (\<Sum>i. norm (-(z^2) * inverse (of_nat (i+2)) * (-z)^i))" |
|
1417 by (intro summable_norm) |
|
1418 (auto simp: norm_power norm_inverse norm_mult mult_ac simp del: of_nat_add of_nat_Suc) |
|
1419 also have "norm ((-z)^2 * (-z)^i) * inverse (of_nat (i+2)) \<le> norm ((-z)^2 * (-z)^i) * 1" for i |
|
1420 by (intro mult_left_mono) (simp_all add: divide_simps) |
|
1421 hence "(\<Sum>i. norm (-(z^2) * inverse (of_nat (i+2)) * (-z)^i)) \<le> |
|
1422 (\<Sum>i. norm (-(z^2) * (-z)^i))" using A assms |
|
1423 apply (simp_all only: norm_power norm_inverse norm_divide norm_mult) |
|
1424 apply (intro suminf_le summable_mult summable_geometric) |
|
1425 apply (auto simp: norm_power field_simps simp del: of_nat_add of_nat_Suc) |
|
1426 done |
|
1427 also have "... = norm z^2 * (\<Sum>i. norm z^i)" using assms |
|
1428 by (subst suminf_mult [symmetric]) (auto intro!: summable_geometric simp: norm_mult norm_power) |
|
1429 also have "(\<Sum>i. norm z^i) = inverse (1 - norm z)" using assms |
|
1430 by (subst suminf_geometric) (simp_all add: divide_inverse) |
|
1431 also have "norm z^2 * ... = norm z^2 / (1 - norm z)" by (simp add: divide_inverse) |
|
1432 finally show ?thesis . |
|
1433 qed |
|
1434 |
1330 |
1435 |
1331 text\<open>Relation between Arg and arctangent in upper halfplane\<close> |
1436 text\<open>Relation between Arg and arctangent in upper halfplane\<close> |
1332 lemma Arg_arctan_upperhalf: |
1437 lemma Arg_arctan_upperhalf: |
1333 assumes "0 < Im z" |
1438 assumes "0 < Im z" |
1334 shows "Arg z = pi/2 - arctan(Re z / Im z)" |
1439 shows "Arg z = pi/2 - arctan(Re z / Im z)" |
1804 text\<open>branch cut gives standard bounds in real case.\<close> |
1909 text\<open>branch cut gives standard bounds in real case.\<close> |
1805 |
1910 |
1806 definition Arctan :: "complex \<Rightarrow> complex" where |
1911 definition Arctan :: "complex \<Rightarrow> complex" where |
1807 "Arctan \<equiv> \<lambda>z. (\<i>/2) * Ln((1 - \<i>*z) / (1 + \<i>*z))" |
1912 "Arctan \<equiv> \<lambda>z. (\<i>/2) * Ln((1 - \<i>*z) / (1 + \<i>*z))" |
1808 |
1913 |
|
1914 lemma Arctan_def_moebius: "Arctan z = \<i>/2 * Ln (moebius (-\<i>) 1 \<i> 1 z)" |
|
1915 by (simp add: Arctan_def moebius_def add_ac) |
|
1916 |
|
1917 lemma Ln_conv_Arctan: |
|
1918 assumes "z \<noteq> -1" |
|
1919 shows "Ln z = -2*\<i> * Arctan (moebius 1 (- 1) (- \<i>) (- \<i>) z)" |
|
1920 proof - |
|
1921 have "Arctan (moebius 1 (- 1) (- \<i>) (- \<i>) z) = |
|
1922 \<i>/2 * Ln (moebius (- \<i>) 1 \<i> 1 (moebius 1 (- 1) (- \<i>) (- \<i>) z))" |
|
1923 by (simp add: Arctan_def_moebius) |
|
1924 also from assms have "\<i> * z \<noteq> \<i> * (-1)" by (subst mult_left_cancel) simp |
|
1925 hence "\<i> * z - -\<i> \<noteq> 0" by (simp add: eq_neg_iff_add_eq_0) |
|
1926 from moebius_inverse'[OF _ this, of 1 1] |
|
1927 have "moebius (- \<i>) 1 \<i> 1 (moebius 1 (- 1) (- \<i>) (- \<i>) z) = z" by simp |
|
1928 finally show ?thesis by (simp add: field_simps) |
|
1929 qed |
|
1930 |
1809 lemma Arctan_0 [simp]: "Arctan 0 = 0" |
1931 lemma Arctan_0 [simp]: "Arctan 0 = 0" |
1810 by (simp add: Arctan_def) |
1932 by (simp add: Arctan_def) |
1811 |
1933 |
1812 lemma Im_complex_div_lemma: "Im((1 - \<i>*z) / (1 + \<i>*z)) = 0 \<longleftrightarrow> Re z = 0" |
1934 lemma Im_complex_div_lemma: "Im((1 - \<i>*z) / (1 + \<i>*z)) = 0 \<longleftrightarrow> Re z = 0" |
1813 by (auto simp: Im_complex_div_eq_0 algebra_simps) |
1935 by (auto simp: Im_complex_div_eq_0 algebra_simps) |
1928 |
2050 |
1929 lemma holomorphic_on_Arctan: |
2051 lemma holomorphic_on_Arctan: |
1930 "(\<And>z. z \<in> s \<Longrightarrow> Re z = 0 \<Longrightarrow> \<bar>Im z\<bar> < 1) \<Longrightarrow> Arctan holomorphic_on s" |
2052 "(\<And>z. z \<in> s \<Longrightarrow> Re z = 0 \<Longrightarrow> \<bar>Im z\<bar> < 1) \<Longrightarrow> Arctan holomorphic_on s" |
1931 by (simp add: complex_differentiable_within_Arctan holomorphic_on_def) |
2053 by (simp add: complex_differentiable_within_Arctan holomorphic_on_def) |
1932 |
2054 |
|
2055 lemma Arctan_series: |
|
2056 assumes z: "norm (z :: complex) < 1" |
|
2057 defines "g \<equiv> \<lambda>n. if odd n then -\<i>*\<i>^n / n else 0" |
|
2058 defines "h \<equiv> \<lambda>z n. (-1)^n / of_nat (2*n+1) * (z::complex)^(2*n+1)" |
|
2059 shows "(\<lambda>n. g n * z^n) sums Arctan z" |
|
2060 and "h z sums Arctan z" |
|
2061 proof - |
|
2062 def G \<equiv> "\<lambda>z. (\<Sum>n. g n * z^n)" |
|
2063 have summable: "summable (\<lambda>n. g n * u^n)" if "norm u < 1" for u |
|
2064 proof (cases "u = 0") |
|
2065 assume u: "u \<noteq> 0" |
|
2066 have "(\<lambda>n. ereal (norm (h u n) / norm (h u (Suc n)))) = (\<lambda>n. ereal (inverse (norm u)^2) * |
|
2067 ereal ((2 + inverse (real (Suc n))) / (2 - inverse (real (Suc n)))))" |
|
2068 proof |
|
2069 fix n |
|
2070 have "ereal (norm (h u n) / norm (h u (Suc n))) = |
|
2071 ereal (inverse (norm u)^2) * ereal ((of_nat (2*Suc n+1) / of_nat (Suc n)) / |
|
2072 (of_nat (2*Suc n-1) / of_nat (Suc n)))" |
|
2073 by (simp add: h_def norm_mult norm_power norm_divide divide_simps |
|
2074 power2_eq_square eval_nat_numeral del: of_nat_add of_nat_Suc) |
|
2075 also have "of_nat (2*Suc n+1) / of_nat (Suc n) = (2::real) + inverse (real (Suc n))" |
|
2076 by (auto simp: divide_simps simp del: of_nat_Suc) simp_all? |
|
2077 also have "of_nat (2*Suc n-1) / of_nat (Suc n) = (2::real) - inverse (real (Suc n))" |
|
2078 by (auto simp: divide_simps simp del: of_nat_Suc) simp_all? |
|
2079 finally show "ereal (norm (h u n) / norm (h u (Suc n))) = ereal (inverse (norm u)^2) * |
|
2080 ereal ((2 + inverse (real (Suc n))) / (2 - inverse (real (Suc n))))" . |
|
2081 qed |
|
2082 also have "\<dots> \<longlonglongrightarrow> ereal (inverse (norm u)^2) * ereal ((2 + 0) / (2 - 0))" |
|
2083 by (intro tendsto_intros LIMSEQ_inverse_real_of_nat) simp_all |
|
2084 finally have "liminf (\<lambda>n. ereal (cmod (h u n) / cmod (h u (Suc n)))) = inverse (norm u)^2" |
|
2085 by (intro lim_imp_Liminf) simp_all |
|
2086 moreover from power_strict_mono[OF that, of 2] u have "inverse (norm u)^2 > 1" |
|
2087 by (simp add: divide_simps) |
|
2088 ultimately have A: "liminf (\<lambda>n. ereal (cmod (h u n) / cmod (h u (Suc n)))) > 1" by simp |
|
2089 from u have "summable (h u)" |
|
2090 by (intro summable_norm_cancel[OF ratio_test_convergence[OF _ A]]) |
|
2091 (auto simp: h_def norm_divide norm_mult norm_power simp del: of_nat_Suc |
|
2092 intro!: mult_pos_pos divide_pos_pos always_eventually) |
|
2093 thus "summable (\<lambda>n. g n * u^n)" |
|
2094 by (subst summable_mono_reindex[of "\<lambda>n. 2*n+1", symmetric]) |
|
2095 (auto simp: power_mult subseq_def g_def h_def elim!: oddE) |
|
2096 qed (simp add: h_def) |
|
2097 |
|
2098 have "\<exists>c. \<forall>u\<in>ball 0 1. Arctan u - G u = c" |
|
2099 proof (rule has_field_derivative_zero_constant) |
|
2100 fix u :: complex assume "u \<in> ball 0 1" |
|
2101 hence u: "norm u < 1" by (simp add: dist_0_norm) |
|
2102 def K \<equiv> "(norm u + 1) / 2" |
|
2103 from u and abs_Im_le_cmod[of u] have Im_u: "\<bar>Im u\<bar> < 1" by linarith |
|
2104 from u have K: "0 \<le> K" "norm u < K" "K < 1" by (simp_all add: K_def) |
|
2105 hence "(G has_field_derivative (\<Sum>n. diffs g n * u ^ n)) (at u)" unfolding G_def |
|
2106 by (intro termdiffs_strong[of _ "of_real K"] summable) simp_all |
|
2107 also have "(\<lambda>n. diffs g n * u^n) = (\<lambda>n. if even n then (\<i>*u)^n else 0)" |
|
2108 by (intro ext) (simp_all del: of_nat_Suc add: g_def diffs_def power_mult_distrib) |
|
2109 also have "suminf \<dots> = (\<Sum>n. (-(u^2))^n)" |
|
2110 by (subst suminf_mono_reindex[of "\<lambda>n. 2*n", symmetric]) |
|
2111 (auto elim!: evenE simp: subseq_def power_mult power_mult_distrib) |
|
2112 also from u have "norm u^2 < 1^2" by (intro power_strict_mono) simp_all |
|
2113 hence "(\<Sum>n. (-(u^2))^n) = inverse (1 + u^2)" |
|
2114 by (subst suminf_geometric) (simp_all add: norm_power inverse_eq_divide) |
|
2115 finally have "(G has_field_derivative inverse (1 + u\<^sup>2)) (at u)" . |
|
2116 from DERIV_diff[OF has_field_derivative_Arctan this] Im_u u |
|
2117 show "((\<lambda>u. Arctan u - G u) has_field_derivative 0) (at u within ball 0 1)" |
|
2118 by (simp_all add: dist_0_norm at_within_open[OF _ open_ball]) |
|
2119 qed simp_all |
|
2120 then obtain c where c: "\<And>u. norm u < 1 \<Longrightarrow> Arctan u - G u = c" by (auto simp: dist_0_norm) |
|
2121 from this[of 0] have "c = 0" by (simp add: G_def g_def powser_zero) |
|
2122 with c z have "Arctan z = G z" by simp |
|
2123 with summable[OF z] show "(\<lambda>n. g n * z^n) sums Arctan z" unfolding G_def by (simp add: sums_iff) |
|
2124 thus "h z sums Arctan z" by (subst (asm) sums_mono_reindex[of "\<lambda>n. 2*n+1", symmetric]) |
|
2125 (auto elim!: oddE simp: subseq_def power_mult g_def h_def) |
|
2126 qed |
|
2127 |
|
2128 text \<open>A quickly-converging series for the logarithm, based on the arctangent.\<close> |
|
2129 lemma ln_series_quadratic: |
|
2130 assumes x: "x > (0::real)" |
|
2131 shows "(\<lambda>n. (2*((x - 1) / (x + 1)) ^ (2*n+1) / of_nat (2*n+1))) sums ln x" |
|
2132 proof - |
|
2133 def y \<equiv> "of_real ((x-1)/(x+1)) :: complex" |
|
2134 from x have x': "complex_of_real x \<noteq> of_real (-1)" by (subst of_real_eq_iff) auto |
|
2135 from x have "\<bar>x - 1\<bar> < \<bar>x + 1\<bar>" by linarith |
|
2136 hence "norm (complex_of_real (x - 1) / complex_of_real (x + 1)) < 1" |
|
2137 by (simp add: norm_divide del: of_real_add of_real_diff) |
|
2138 hence "norm (\<i> * y) < 1" unfolding y_def by (subst norm_mult) simp |
|
2139 hence "(\<lambda>n. (-2*\<i>) * ((-1)^n / of_nat (2*n+1) * (\<i>*y)^(2*n+1))) sums ((-2*\<i>) * Arctan (\<i>*y))" |
|
2140 by (intro Arctan_series sums_mult) simp_all |
|
2141 also have "(\<lambda>n. (-2*\<i>) * ((-1)^n / of_nat (2*n+1) * (\<i>*y)^(2*n+1))) = |
|
2142 (\<lambda>n. (-2*\<i>) * ((-1)^n * (\<i>*y*(-y\<^sup>2)^n)/of_nat (2*n+1)))" |
|
2143 by (intro ext) (simp_all add: power_mult power_mult_distrib) |
|
2144 also have "\<dots> = (\<lambda>n. 2*y* ((-1) * (-y\<^sup>2))^n/of_nat (2*n+1))" |
|
2145 by (intro ext, subst power_mult_distrib) (simp add: algebra_simps power_mult) |
|
2146 also have "\<dots> = (\<lambda>n. 2*y^(2*n+1) / of_nat (2*n+1))" |
|
2147 by (subst power_add, subst power_mult) (simp add: mult_ac) |
|
2148 also have "\<dots> = (\<lambda>n. of_real (2*((x-1)/(x+1))^(2*n+1) / of_nat (2*n+1)))" |
|
2149 by (intro ext) (simp add: y_def) |
|
2150 also have "\<i> * y = (of_real x - 1) / (-\<i> * (of_real x + 1))" |
|
2151 by (subst divide_divide_eq_left [symmetric]) (simp add: y_def) |
|
2152 also have "\<dots> = moebius 1 (-1) (-\<i>) (-\<i>) (of_real x)" by (simp add: moebius_def algebra_simps) |
|
2153 also from x' have "-2*\<i>*Arctan \<dots> = Ln (of_real x)" by (intro Ln_conv_Arctan [symmetric]) simp_all |
|
2154 also from x have "\<dots> = ln x" by (rule Ln_of_real) |
|
2155 finally show ?thesis by (subst (asm) sums_of_real_iff) |
|
2156 qed |
1933 |
2157 |
1934 subsection \<open>Real arctangent\<close> |
2158 subsection \<open>Real arctangent\<close> |
1935 |
2159 |
1936 lemma norm_exp_ii_times [simp]: "norm (exp(\<i> * of_real y)) = 1" |
2160 lemma norm_exp_ii_times [simp]: "norm (exp(\<i> * of_real y)) = 1" |
1937 by simp |
2161 by simp |