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.60    by (simp add: exp_add exp_Euler exp_of_real sin_of_real cos_of_real)
    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.129    using unwinding_2pi by (simp add: exp_add)
   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.141 -subsection{*Quadrant-type results for Ln*}
   1.142 +subsection\<open>Quadrant-type results for Ln\<close>
   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.181    by (simp add: powr_def)
   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.192      by (simp add: divide_simps)
   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.197      by (simp add: field_simps)
   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.301    by (simp add: Arcsin_Arccos_csqrt_pos)
   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.329    by (simp add: arccos_minus)
   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