src/HOL/Multivariate_Analysis/Complex_Transcendental.thy
 changeset 60420 884f54e01427 parent 60162 645058aa9d6f child 60809 457abb82fb9e
```     1.1 --- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Wed Jun 10 19:05:19 2015 +0200
1.2 +++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Wed Jun 10 19:10:20 2015 +0200
1.3 @@ -2,7 +2,7 @@
1.4      Ported from "hol_light/Multivariate/transcendentals.ml" by L C Paulson (2015)
1.5  *)
1.6
1.7 -section {* Complex Transcendental Functions *}
1.8 +section \<open>Complex Transcendental Functions\<close>
1.9
1.10  theory Complex_Transcendental
1.11  imports  "~~/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics"
1.12 @@ -40,7 +40,7 @@
1.13    apply (simp add: norm_power Im_power2)
1.14    done
1.15
1.16 -subsection{*The Exponential Function is Differentiable and Continuous*}
1.17 +subsection\<open>The Exponential Function is Differentiable and Continuous\<close>
1.18
1.19  lemma complex_differentiable_within_exp: "exp complex_differentiable (at z within s)"
1.20    using DERIV_exp complex_differentiable_at_within complex_differentiable_def by blast
1.21 @@ -58,9 +58,9 @@
1.22  lemma holomorphic_on_exp: "exp holomorphic_on s"
1.23    by (simp add: complex_differentiable_within_exp holomorphic_on_def)
1.24
1.25 -subsection{*Euler and de Moivre formulas.*}
1.26 -
1.27 -text{*The sine series times @{term i}*}
1.28 +subsection\<open>Euler and de Moivre formulas.\<close>
1.29 +
1.30 +text\<open>The sine series times @{term i}\<close>
1.31  lemma sin_ii_eq: "(\<lambda>n. (ii * sin_coeff n) * z^n) sums (ii * sin z)"
1.32  proof -
1.33    have "(\<lambda>n. ii * sin_coeff n *\<^sub>R z^n) sums (ii * sin z)"
1.34 @@ -101,7 +101,7 @@
1.35  lemma cos_exp_eq:  "cos z = (exp(ii * z) + exp(-(ii * z))) / 2"
1.36    by (simp add: exp_Euler exp_minus_Euler)
1.37
1.38 -subsection{*Relationships between real and complex trig functions*}
1.39 +subsection\<open>Relationships between real and complex trig functions\<close>
1.40
1.41  lemma real_sin_eq [simp]:
1.42    fixes x::real
1.43 @@ -157,7 +157,7 @@
1.44  lemma holomorphic_on_cos: "cos holomorphic_on s"
1.45    by (simp add: complex_differentiable_within_cos holomorphic_on_def)
1.46
1.47 -subsection{* Get a nice real/imaginary separation in Euler's formula.*}
1.48 +subsection\<open>Get a nice real/imaginary separation in Euler's formula.\<close>
1.49
1.50  lemma Euler: "exp(z) = of_real(exp(Re z)) *
1.51                (of_real(cos(Im z)) + ii * of_real(sin(Im z)))"
1.52 @@ -184,7 +184,7 @@
1.53  lemma Im_sin_nonneg2: "Re z = pi \<Longrightarrow> Im z \<le> 0 \<Longrightarrow> 0 \<le> Im (sin z)"
1.54    by (simp add: Re_sin Im_sin algebra_simps)
1.55
1.56 -subsection{*More on the Polar Representation of Complex Numbers*}
1.57 +subsection\<open>More on the Polar Representation of Complex Numbers\<close>
1.58
1.59  lemma exp_Complex: "exp(Complex r t) = of_real(exp r) * Complex (cos t) (sin t)"
1.61 @@ -456,7 +456,7 @@
1.62      done
1.63  qed
1.64
1.65 -subsection{* Taylor series for complex exponential, sine and cosine.*}
1.66 +subsection\<open>Taylor series for complex exponential, sine and cosine.\<close>
1.67
1.68  declare power_Suc [simp del]
1.69
1.70 @@ -600,7 +600,7 @@
1.71
1.72  declare power_Suc [simp]
1.73
1.74 -text{*32-bit Approximation to e*}
1.75 +text\<open>32-bit Approximation to e\<close>
1.76  lemma e_approx_32: "abs(exp(1) - 5837465777 / 2147483648) \<le> (inverse(2 ^ 32)::real)"
1.77    using Taylor_exp [of 1 14] exp_le
1.78    apply (simp add: setsum_left_distrib in_Reals_norm Re_exp atMost_nat_numeral fact_numeral)
1.79 @@ -615,7 +615,7 @@
1.80    by (metis e_less_3 exp_less_cancel_iff exp_ln_iff less_trans ln_exp)
1.81
1.82
1.83 -subsection{*The argument of a complex number*}
1.84 +subsection\<open>The argument of a complex number\<close>
1.85
1.86  definition Arg :: "complex \<Rightarrow> real" where
1.87   "Arg z \<equiv> if z = 0 then 0
1.88 @@ -874,7 +874,7 @@
1.89    by (rule Arg_unique [of  "exp(Re z)"]) (auto simp: Exp_eq_polar)
1.90
1.91
1.92 -subsection{*Analytic properties of tangent function*}
1.93 +subsection\<open>Analytic properties of tangent function\<close>
1.94
1.95  lemma cnj_tan: "cnj(tan z) = tan(cnj z)"
1.96    by (simp add: cnj_cos cnj_sin tan_def)
1.97 @@ -897,7 +897,7 @@
1.98    by (simp add: complex_differentiable_within_tan holomorphic_on_def)
1.99
1.100
1.101 -subsection{*Complex logarithms (the conventional principal value)*}
1.102 +subsection\<open>Complex logarithms (the conventional principal value)\<close>
1.103
1.104  instantiation complex :: ln
1.105  begin
1.106 @@ -934,7 +934,7 @@
1.107    apply auto
1.108    done
1.109
1.110 -subsection{*Relation to Real Logarithm*}
1.111 +subsection\<open>Relation to Real Logarithm\<close>
1.112
1.113  lemma Ln_of_real:
1.114    assumes "0 < z"
1.115 @@ -998,9 +998,9 @@
1.116    done
1.117
1.118
1.119 -subsection{*The Unwinding Number and the Ln-product Formula*}
1.120 -
1.121 -text{*Note that in this special case the unwinding number is -1, 0 or 1.*}
1.122 +subsection\<open>The Unwinding Number and the Ln-product Formula\<close>
1.123 +
1.124 +text\<open>Note that in this special case the unwinding number is -1, 0 or 1.\<close>
1.125
1.126  definition unwinding :: "complex \<Rightarrow> complex" where
1.127     "unwinding(z) = (z - Ln(exp z)) / (of_real(2*pi) * ii)"
1.128 @@ -1013,7 +1013,7 @@
1.130
1.131
1.132 -subsection{*Derivative of Ln away from the branch cut*}
1.133 +subsection\<open>Derivative of Ln away from the branch cut\<close>
1.134
1.135  lemma
1.136    assumes "Im(z) = 0 \<Longrightarrow> 0 < Re(z)"
1.137 @@ -1061,7 +1061,7 @@
1.138    by (simp add: complex_differentiable_within_Ln holomorphic_on_def)
1.139
1.140
1.143
1.144  lemma cos_lt_zero_pi: "pi/2 < x \<Longrightarrow> x < 3*pi/2 \<Longrightarrow> cos x < 0"
1.145    using cos_minus_pi cos_gt_zero_pi [of "x-pi"]
1.146 @@ -1160,7 +1160,7 @@
1.147    by (metis Im_Ln_eq_0 Im_Ln_less_pi Im_Ln_pos_le Im_Ln_pos_lt add.right_neutral complex_eq mult_zero_right not_less not_less_iff_gr_or_eq of_real_0)
1.148
1.149
1.150 -subsection{*More Properties of Ln*}
1.151 +subsection\<open>More Properties of Ln\<close>
1.152
1.153  lemma cnj_Ln: "(Im z = 0 \<Longrightarrow> 0 < Re z) \<Longrightarrow> cnj(Ln z) = Ln(cnj z)"
1.154    apply (cases "z=0", auto)
1.155 @@ -1283,7 +1283,7 @@
1.156    by (auto simp: of_real_numeral Ln_times)
1.157
1.158
1.159 -subsection{*Relation between Ln and Arg, and hence continuity of Arg*}
1.160 +subsection\<open>Relation between Ln and Arg, and hence continuity of Arg\<close>
1.161
1.162  lemma Arg_Ln:
1.163    assumes "0 < Arg z" shows "Arg z = Im(Ln(-z)) + pi"
1.164 @@ -1327,7 +1327,7 @@
1.165      done
1.166  qed
1.167
1.168 -text{*Relation between Arg and arctangent in upper halfplane*}
1.169 +text\<open>Relation between Arg and arctangent in upper halfplane\<close>
1.170  lemma Arg_arctan_upperhalf:
1.171    assumes "0 < Im z"
1.172      shows "Arg z = pi/2 - arctan(Re z / Im z)"
1.173 @@ -1439,7 +1439,7 @@
1.174    using open_Arg_gt [of t]
1.175    by (simp add: closed_def Set.Collect_neg_eq [symmetric] not_le)
1.176
1.177 -subsection{*Complex Powers*}
1.178 +subsection\<open>Complex Powers\<close>
1.179
1.180  lemma powr_to_1 [simp]: "z powr 1 = (z::complex)"
1.182 @@ -1517,7 +1517,7 @@
1.183    by (auto simp add: norm_powr_real powr_def Im_Ln_eq_0 complex_is_Real_iff in_Reals_norm)
1.184
1.185
1.186 -subsection{*Some Limits involving Logarithms*}
1.187 +subsection\<open>Some Limits involving Logarithms\<close>
1.188
1.189  lemma lim_Ln_over_power:
1.190    fixes s::complex
1.191 @@ -1626,12 +1626,12 @@
1.193    then have "ln (exp (inverse r)) < ln (of_nat n)"
1.194      by (metis exp_gt_zero less_trans ln_exp ln_less_cancel_iff)
1.195 -  with `0 < r` have "1 < r * ln (real_of_nat n)"
1.196 +  with \<open>0 < r\<close> have "1 < r * ln (real_of_nat n)"
1.198    moreover have "n > 0" using n
1.199      using neq0_conv by fastforce
1.200    ultimately show "\<exists>no. \<forall>n. Ln (of_nat n) \<noteq> 0 \<longrightarrow> no \<le> n \<longrightarrow> 1 < r * cmod (Ln (of_nat n))"
1.201 -    using n `0 < r`
1.202 +    using n \<open>0 < r\<close>
1.203      apply (rule_tac x=n in exI)
1.204      apply (auto simp: divide_simps)
1.205      apply (erule less_le_trans, auto)
1.206 @@ -1646,7 +1646,7 @@
1.207    done
1.208
1.209
1.210 -subsection{*Relation between Square Root and exp/ln, hence its derivative*}
1.211 +subsection\<open>Relation between Square Root and exp/ln, hence its derivative\<close>
1.212
1.213  lemma csqrt_exp_Ln:
1.214    assumes "z \<noteq> 0"
1.215 @@ -1757,9 +1757,9 @@
1.216  by (metis linear not_less real_sqrt_less_iff real_sqrt_pow2_iff real_sqrt_power)
1.217  qed
1.218
1.219 -subsection{*Complex arctangent*}
1.220 -
1.221 -text{*branch cut gives standard bounds in real case.*}
1.222 +subsection\<open>Complex arctangent\<close>
1.223 +
1.224 +text\<open>branch cut gives standard bounds in real case.\<close>
1.225
1.226  definition Arctan :: "complex \<Rightarrow> complex" where
1.227      "Arctan \<equiv> \<lambda>z. (\<i>/2) * Ln((1 - \<i>*z) / (1 + \<i>*z))"
1.228 @@ -1889,7 +1889,7 @@
1.229    by (simp add: complex_differentiable_within_Arctan holomorphic_on_def)
1.230
1.231
1.232 -subsection {*Real arctangent*}
1.233 +subsection \<open>Real arctangent\<close>
1.234
1.235  lemma norm_exp_ii_times [simp]: "norm (exp(\<i> * of_real y)) = 1"
1.236    by simp
1.237 @@ -2026,7 +2026,7 @@
1.238    by (metis abs_arctan_le abs_less_iff arctan_tan minus_less_iff)
1.239
1.240
1.241 -subsection{*Inverse Sine*}
1.242 +subsection\<open>Inverse Sine\<close>
1.243
1.244  definition Arcsin :: "complex \<Rightarrow> complex" where
1.245     "Arcsin \<equiv> \<lambda>z. -\<i> * Ln(\<i> * z + csqrt(1 - z\<^sup>2))"
1.246 @@ -2074,7 +2074,7 @@
1.247  lemma sin_Arcsin [simp]: "sin(Arcsin z) = z"
1.248  proof -
1.249    have "\<i>*z*2 + csqrt (1 - z\<^sup>2)*2 = 0 \<longleftrightarrow> (\<i>*z)*2 + csqrt (1 - z\<^sup>2)*2 = 0"
1.250 -    by (simp add: algebra_simps)  --{*Cancelling a factor of 2*}
1.251 +    by (simp add: algebra_simps)  --\<open>Cancelling a factor of 2\<close>
1.252    moreover have "... \<longleftrightarrow> (\<i>*z) + csqrt (1 - z\<^sup>2) = 0"
1.253      by (metis Arcsin_body_lemma distrib_right no_zero_divisors zero_neq_numeral)
1.254    ultimately show ?thesis
1.255 @@ -2177,7 +2177,7 @@
1.256    by (simp add: complex_differentiable_within_Arcsin holomorphic_on_def)
1.257
1.258
1.259 -subsection{*Inverse Cosine*}
1.260 +subsection\<open>Inverse Cosine\<close>
1.261
1.262  definition Arccos :: "complex \<Rightarrow> complex" where
1.263     "Arccos \<equiv> \<lambda>z. -\<i> * Ln(z + \<i> * csqrt(1 - z\<^sup>2))"
1.264 @@ -2197,7 +2197,7 @@
1.265  lemma Im_Arccos: "Im(Arccos z) = - ln (cmod (z + \<i> * csqrt (1 - z\<^sup>2)))"
1.266    by (simp add: Arccos_def Arccos_body_lemma)
1.267
1.268 -text{*A very tricky argument to find!*}
1.269 +text\<open>A very tricky argument to find!\<close>
1.270  lemma abs_Re_less_1_preserve:
1.271    assumes "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1)"  "Im (z + \<i> * csqrt (1 - z\<^sup>2)) = 0"
1.272      shows "0 < Re (z + \<i> * csqrt (1 - z\<^sup>2))"
1.273 @@ -2252,7 +2252,7 @@
1.274  lemma cos_Arccos [simp]: "cos(Arccos z) = z"
1.275  proof -
1.276    have "z*2 + \<i> * (2 * csqrt (1 - z\<^sup>2)) = 0 \<longleftrightarrow> z*2 + \<i> * csqrt (1 - z\<^sup>2)*2 = 0"
1.277 -    by (simp add: algebra_simps)  --{*Cancelling a factor of 2*}
1.278 +    by (simp add: algebra_simps)  --\<open>Cancelling a factor of 2\<close>
1.279    moreover have "... \<longleftrightarrow> z + \<i> * csqrt (1 - z\<^sup>2) = 0"
1.280      by (metis distrib_right mult_eq_0_iff zero_neq_numeral)
1.281    ultimately show ?thesis
1.282 @@ -2349,7 +2349,7 @@
1.283    by (simp add: complex_differentiable_within_Arccos holomorphic_on_def)
1.284
1.285
1.286 -subsection{*Upper and Lower Bounds for Inverse Sine and Cosine*}
1.287 +subsection\<open>Upper and Lower Bounds for Inverse Sine and Cosine\<close>
1.288
1.289  lemma Arcsin_bounds: "\<bar>Re z\<bar> < 1 \<Longrightarrow> abs(Re(Arcsin z)) < pi/2"
1.290    unfolding Re_Arcsin
1.291 @@ -2374,7 +2374,7 @@
1.292    using Re_Arcsin_bounds abs_le_interval_iff less_eq_real_def by blast
1.293
1.294
1.295 -subsection{*Interrelations between Arcsin and Arccos*}
1.296 +subsection\<open>Interrelations between Arcsin and Arccos\<close>
1.297
1.298  lemma cos_Arcsin_nonzero:
1.299    assumes "z\<^sup>2 \<noteq> 1" shows "cos(Arcsin z) \<noteq> 0"
1.300 @@ -2478,7 +2478,7 @@
1.302
1.303
1.304 -subsection{*Relationship with Arcsin on the Real Numbers*}
1.305 +subsection\<open>Relationship with Arcsin on the Real Numbers\<close>
1.306
1.307  lemma Im_Arcsin_of_real:
1.308    assumes "abs x \<le> 1"
1.309 @@ -2528,7 +2528,7 @@
1.310    by (metis Im_Arcsin_of_real add.right_neutral arcsin_eq_Re_Arcsin complex_eq mult_zero_right of_real_0)
1.311
1.312
1.313 -subsection{*Relationship with Arccos on the Real Numbers*}
1.314 +subsection\<open>Relationship with Arccos on the Real Numbers\<close>
1.315
1.316  lemma Im_Arccos_of_real:
1.317    assumes "abs x \<le> 1"
1.318 @@ -2577,7 +2577,7 @@
1.319  lemma of_real_arccos: "abs x \<le> 1 \<Longrightarrow> of_real(arccos x) = Arccos(of_real x)"
1.320    by (metis Im_Arccos_of_real add.right_neutral arccos_eq_Re_Arccos complex_eq mult_zero_right of_real_0)
1.321
1.322 -subsection{*Some interrelationships among the real inverse trig functions.*}
1.323 +subsection\<open>Some interrelationships among the real inverse trig functions.\<close>
1.324
1.325  lemma arccos_arctan:
1.326    assumes "-1 < x" "x < 1"
1.327 @@ -2647,7 +2647,7 @@
1.328    using arccos_arcsin_sqrt_pos [of "-x"]
1.330
1.331 -subsection{*continuity results for arcsin and arccos.*}
1.332 +subsection\<open>continuity results for arcsin and arccos.\<close>
1.333
1.334  lemma continuous_on_Arcsin_real [continuous_intros]:
1.335      "continuous_on {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1} Arcsin"
1.336 @@ -2702,7 +2702,7 @@
1.337  qed
1.338
1.339
1.340 -subsection{*Roots of unity*}
1.341 +subsection\<open>Roots of unity\<close>
1.342
1.343  lemma complex_root_unity:
1.344    fixes j::nat
```