new file for complex transcendental functions
authorpaulson <lp15@cam.ac.uk>
Wed Mar 18 14:55:17 2015 +0000 (2015-03-18)
changeset 59745390476a0ef13
parent 59744 37c3ffe95b8a
child 59746 ddae5727c5a9
new file for complex transcendental functions
src/HOL/Multivariate_Analysis/Complex_Transcendental.thy
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Wed Mar 18 14:55:17 2015 +0000
     1.3 @@ -0,0 +1,229 @@
     1.4 +(*  Author: John Harrison, Marco Maggesi, Graziano Gentili, Gianni Ciolli, Valentina Bruno
     1.5 +    Ported from "hol_light/Multivariate/transcendentals.ml" by L C Paulson (2015)
     1.6 +*)
     1.7 +
     1.8 +section {* Complex Transcendental Functions *}
     1.9 +
    1.10 +theory Complex_Transcendental
    1.11 +imports  "~~/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics"
    1.12 +begin
    1.13 +
    1.14 +
    1.15 +lemma complex_differentiable_at_exp: "exp complex_differentiable at z"
    1.16 +  using DERIV_exp complex_differentiable_def by blast
    1.17 +
    1.18 +lemma complex_differentiable_within_exp: "exp complex_differentiable (at z within s)"
    1.19 +  by (simp add: complex_differentiable_at_exp complex_differentiable_at_within)
    1.20 +
    1.21 +lemma continuous_within_exp:
    1.22 +  fixes z::"'a::{real_normed_field,banach}"
    1.23 +  shows "continuous (at z within s) exp"
    1.24 +by (simp add: continuous_at_imp_continuous_within)
    1.25 +
    1.26 +lemma continuous_on_exp:
    1.27 +  fixes s::"'a::{real_normed_field,banach} set"
    1.28 +  shows "continuous_on s exp"
    1.29 +by (simp add: continuous_on_exp continuous_on_id)
    1.30 +
    1.31 +lemma holomorphic_on_exp: "exp holomorphic_on s"
    1.32 +  by (simp add: complex_differentiable_within_exp holomorphic_on_def)
    1.33 +
    1.34 +
    1.35 +
    1.36 +subsection{*Euler and de Moivre formulas.*}
    1.37 +
    1.38 +text{*The sine series times @{term i}*}
    1.39 +lemma sin_ii_eq: "(\<lambda>n. (ii * sin_coeff n) * z^n) sums (ii * sin z)"
    1.40 +proof -
    1.41 +  have "(\<lambda>n. ii * sin_coeff n *\<^sub>R z^n) sums (ii * sin z)"
    1.42 +    using sin_converges sums_mult by blast
    1.43 +  then show ?thesis
    1.44 +    by (simp add: scaleR_conv_of_real field_simps)
    1.45 +qed
    1.46 +
    1.47 +theorem exp_Euler: "exp(ii * z) = cos(z) + ii * sin(z)"
    1.48 +proof -
    1.49 +  have "(\<lambda>n. (cos_coeff n + ii * sin_coeff n) * z^n) 
    1.50 +        = (\<lambda>n. (ii * z) ^ n /\<^sub>R (fact n))"
    1.51 +  proof
    1.52 +    fix n
    1.53 +    show "(cos_coeff n + ii * sin_coeff n) * z^n = (ii * z) ^ n /\<^sub>R (fact n)"
    1.54 +      by (auto simp: cos_coeff_def sin_coeff_def scaleR_conv_of_real field_simps elim!: evenE oddE)
    1.55 +  qed
    1.56 +  also have "... sums (exp (ii * z))"
    1.57 +    by (rule exp_converges)
    1.58 +  finally have "(\<lambda>n. (cos_coeff n + ii * sin_coeff n) * z^n) sums (exp (ii * z))" .
    1.59 +  moreover have "(\<lambda>n. (cos_coeff n + ii * sin_coeff n) * z^n) sums (cos z + ii * sin z)"
    1.60 +    using sums_add [OF cos_converges [of z] sin_ii_eq [of z]]
    1.61 +    by (simp add: field_simps scaleR_conv_of_real)
    1.62 +  ultimately show ?thesis
    1.63 +    using sums_unique2 by blast
    1.64 +qed
    1.65 +
    1.66 +corollary exp_minus_Euler: "exp(-(ii * z)) = cos(z) - ii * sin(z)"
    1.67 +  using exp_Euler [of "-z"]
    1.68 +  by simp
    1.69 +
    1.70 +lemma sin_exp_eq: "sin z = (exp(ii * z) - exp(-(ii * z))) / (2*ii)"
    1.71 +  by (simp add: exp_Euler exp_minus_Euler)
    1.72 +
    1.73 +lemma sin_exp_eq': "sin z = ii * (exp(-(ii * z)) - exp(ii * z)) / 2"
    1.74 +  by (simp add: exp_Euler exp_minus_Euler)
    1.75 +
    1.76 +lemma cos_exp_eq:  "cos z = (exp(ii * z) + exp(-(ii * z))) / 2"
    1.77 +  by (simp add: exp_Euler exp_minus_Euler)
    1.78 +
    1.79 +subsection{*Relationships between real and complex trig functions*}
    1.80 +
    1.81 +declare sin_of_real [simp] cos_of_real [simp]
    1.82 +
    1.83 +lemma real_sin_eq [simp]:
    1.84 +  fixes x::real
    1.85 +  shows "Re(sin(of_real x)) = sin x"
    1.86 +  by (simp add: sin_of_real)
    1.87 +  
    1.88 +lemma real_cos_eq [simp]:
    1.89 +  fixes x::real
    1.90 +  shows "Re(cos(of_real x)) = cos x"
    1.91 +  by (simp add: cos_of_real)
    1.92 +
    1.93 +lemma DeMoivre: "(cos z + ii * sin z) ^ n = cos(n * z) + ii * sin(n * z)"
    1.94 +  apply (simp add: exp_Euler [symmetric])
    1.95 +  by (metis exp_of_nat_mult mult.left_commute)
    1.96 +
    1.97 +lemma exp_cnj:
    1.98 +  fixes z::complex
    1.99 +  shows "cnj (exp z) = exp (cnj z)"
   1.100 +proof -
   1.101 +  have "(\<lambda>n. cnj (z ^ n /\<^sub>R (fact n))) = (\<lambda>n. (cnj z)^n /\<^sub>R (fact n))"
   1.102 +    by auto
   1.103 +  also have "... sums (exp (cnj z))"
   1.104 +    by (rule exp_converges)
   1.105 +  finally have "(\<lambda>n. cnj (z ^ n /\<^sub>R (fact n))) sums (exp (cnj z))" .
   1.106 +  moreover have "(\<lambda>n. cnj (z ^ n /\<^sub>R (fact n))) sums (cnj (exp z))"
   1.107 +    by (metis exp_converges sums_cnj) 
   1.108 +  ultimately show ?thesis
   1.109 +    using sums_unique2
   1.110 +    by blast 
   1.111 +qed
   1.112 +
   1.113 +lemma cnj_sin: "cnj(sin z) = sin(cnj z)"
   1.114 +  by (simp add: sin_exp_eq exp_cnj field_simps)
   1.115 +
   1.116 +lemma cnj_cos: "cnj(cos z) = cos(cnj z)"
   1.117 +  by (simp add: cos_exp_eq exp_cnj field_simps)
   1.118 +
   1.119 +lemma exp_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> exp z \<in> \<real>"
   1.120 +  by (metis Reals_cases Reals_of_real exp_of_real)
   1.121 +
   1.122 +lemma sin_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> sin z \<in> \<real>"
   1.123 +  by (metis Reals_cases Reals_of_real sin_of_real)
   1.124 +
   1.125 +lemma cos_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> cos z \<in> \<real>"
   1.126 +  by (metis Reals_cases Reals_of_real cos_of_real)
   1.127 +
   1.128 +lemma complex_differentiable_at_sin: "sin complex_differentiable at z"
   1.129 +  using DERIV_sin complex_differentiable_def by blast
   1.130 +
   1.131 +lemma complex_differentiable_within_sin: "sin complex_differentiable (at z within s)"
   1.132 +  by (simp add: complex_differentiable_at_sin complex_differentiable_at_within)
   1.133 +
   1.134 +lemma complex_differentiable_at_cos: "cos complex_differentiable at z"
   1.135 +  using DERIV_cos complex_differentiable_def by blast
   1.136 +
   1.137 +lemma complex_differentiable_within_cos: "cos complex_differentiable (at z within s)"
   1.138 +  by (simp add: complex_differentiable_at_cos complex_differentiable_at_within)
   1.139 +
   1.140 +lemma holomorphic_on_sin: "sin holomorphic_on s"
   1.141 +  by (simp add: complex_differentiable_within_sin holomorphic_on_def)
   1.142 +
   1.143 +lemma holomorphic_on_cos: "cos holomorphic_on s"
   1.144 +  by (simp add: complex_differentiable_within_cos holomorphic_on_def)
   1.145 +
   1.146 +subsection{* Get a nice real/imaginary separation in Euler's formula.*}
   1.147 +
   1.148 +lemma Euler: "exp(z) = of_real(exp(Re z)) * 
   1.149 +              (of_real(cos(Im z)) + ii * of_real(sin(Im z)))"
   1.150 +by (cases z) (simp add: exp_add exp_Euler cos_of_real exp_of_real sin_of_real)
   1.151 +
   1.152 +lemma Re_sin: "Re(sin z) = sin(Re z) * (exp(Im z) + exp(-(Im z))) / 2"
   1.153 +  by (simp add: sin_exp_eq field_simps Re_divide Im_exp)
   1.154 +
   1.155 +lemma Im_sin: "Im(sin z) = cos(Re z) * (exp(Im z) - exp(-(Im z))) / 2"
   1.156 +  by (simp add: sin_exp_eq field_simps Im_divide Re_exp)
   1.157 +
   1.158 +lemma Re_cos: "Re(cos z) = cos(Re z) * (exp(Im z) + exp(-(Im z))) / 2"
   1.159 +  by (simp add: cos_exp_eq field_simps Re_divide Re_exp)
   1.160 +
   1.161 +lemma Im_cos: "Im(cos z) = sin(Re z) * (exp(-(Im z)) - exp(Im z)) / 2"
   1.162 +  by (simp add: cos_exp_eq field_simps Im_divide Im_exp)
   1.163 +
   1.164 +(* Now more relatively easy consequences.*)
   1.165 +
   1.166 +lemma sin_times_pi_eq_0: "sin(x * pi) = 0 \<longleftrightarrow> x \<in> Ints"
   1.167 +  by (simp add: sin_zero_iff_int2) (metis Ints_cases Ints_real_of_int real_of_int_def)
   1.168 +
   1.169 +lemma cos_one_2pi: 
   1.170 +    "cos(x) = 1 \<longleftrightarrow> (\<exists>n::nat. x = n * 2*pi) | (\<exists>n::nat. x = -(n * 2*pi))"
   1.171 +    (is "?lhs = ?rhs")
   1.172 +proof
   1.173 +  assume "cos(x) = 1"
   1.174 +  then have "sin x = 0"
   1.175 +    by (simp add: cos_one_sin_zero)
   1.176 +  then show ?rhs
   1.177 +  proof (simp only: sin_zero_iff, elim exE disjE conjE)
   1.178 +    fix n::nat
   1.179 +    assume n: "even n" "x = real n * (pi/2)"
   1.180 +    then obtain m where m: "n = 2 * m"
   1.181 +      using dvdE by blast
   1.182 +    then have me: "even m" using `?lhs` n
   1.183 +      by (auto simp: field_simps) (metis one_neq_neg_one  power_minus_odd power_one)
   1.184 +    show ?rhs
   1.185 +      using m me n
   1.186 +      by (auto simp: field_simps elim!: evenE)
   1.187 +  next    
   1.188 +    fix n::nat
   1.189 +    assume n: "even n" "x = - (real n * (pi/2))"
   1.190 +    then obtain m where m: "n = 2 * m"
   1.191 +      using dvdE by blast
   1.192 +    then have me: "even m" using `?lhs` n
   1.193 +      by (auto simp: field_simps) (metis one_neq_neg_one  power_minus_odd power_one)
   1.194 +    show ?rhs
   1.195 +      using m me n
   1.196 +      by (auto simp: field_simps elim!: evenE)
   1.197 +  qed
   1.198 +next
   1.199 +  assume "?rhs"
   1.200 +  then show "cos x = 1"
   1.201 +    by (metis cos_2npi cos_minus mult.assoc mult.left_commute)
   1.202 +qed
   1.203 +
   1.204 +lemma cos_one_2pi_int: "cos(x) = 1 \<longleftrightarrow> (\<exists>n::int. x = n * 2*pi)"
   1.205 +  apply auto  --{*FIXME simproc bug*}
   1.206 +  apply (auto simp: cos_one_2pi)
   1.207 +  apply (metis real_of_int_of_nat_eq)
   1.208 +  apply (metis mult_minus_right real_of_int_minus real_of_int_of_nat_eq)
   1.209 +  by (metis mult_minus_right of_int_of_nat real_of_int_def real_of_nat_def)
   1.210 +
   1.211 +lemma sin_cos_sqrt: "0 \<le> sin(x) \<Longrightarrow> (sin(x) = sqrt(1 - (cos(x) ^ 2)))"
   1.212 +  using sin_squared_eq real_sqrt_unique by fastforce
   1.213 +
   1.214 +lemma sin_eq_0_pi: "-pi < x \<Longrightarrow> x < pi \<Longrightarrow> sin(x) = 0 \<Longrightarrow> x = 0"
   1.215 +  by (metis sin_gt_zero sin_minus minus_less_iff neg_0_less_iff_less not_less_iff_gr_or_eq)
   1.216 +
   1.217 +lemma cos_treble_cos: 
   1.218 +  fixes x :: "'a::{real_normed_field,banach}"
   1.219 +  shows "cos(3 * x) = 4 * cos(x) ^ 3 - 3 * cos x"
   1.220 +proof -
   1.221 +  have *: "(sin x * (sin x * 3)) = 3 - (cos x * (cos x * 3))"
   1.222 +    by (simp add: mult.assoc [symmetric] sin_squared_eq [unfolded power2_eq_square])
   1.223 +  have "cos(3 * x) = cos(2*x + x)"
   1.224 +    by simp
   1.225 +  also have "... = 4 * cos(x) ^ 3 - 3 * cos x"
   1.226 +    apply (simp only: cos_add cos_double sin_double)
   1.227 +    apply (simp add: * field_simps power2_eq_square power3_eq_cube)
   1.228 +    done
   1.229 +  finally show ?thesis .
   1.230 +qed
   1.231 +
   1.232 +end