# HG changeset patch # User paulson # Date 1426690517 0 # Node ID 390476a0ef1377efde6dae54ad64f45970a28be3 # Parent 37c3ffe95b8a8d2930310e5d0d2d526189ffd03f new file for complex transcendental functions diff -r 37c3ffe95b8a -r 390476a0ef13 src/HOL/Multivariate_Analysis/Complex_Transcendental.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy Wed Mar 18 14:55:17 2015 +0000 @@ -0,0 +1,229 @@ +(* Author: John Harrison, Marco Maggesi, Graziano Gentili, Gianni Ciolli, Valentina Bruno + Ported from "hol_light/Multivariate/transcendentals.ml" by L C Paulson (2015) +*) + +section {* Complex Transcendental Functions *} + +theory Complex_Transcendental +imports "~~/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics" +begin + + +lemma complex_differentiable_at_exp: "exp complex_differentiable at z" + using DERIV_exp complex_differentiable_def by blast + +lemma complex_differentiable_within_exp: "exp complex_differentiable (at z within s)" + by (simp add: complex_differentiable_at_exp complex_differentiable_at_within) + +lemma continuous_within_exp: + fixes z::"'a::{real_normed_field,banach}" + shows "continuous (at z within s) exp" +by (simp add: continuous_at_imp_continuous_within) + +lemma continuous_on_exp: + fixes s::"'a::{real_normed_field,banach} set" + shows "continuous_on s exp" +by (simp add: continuous_on_exp continuous_on_id) + +lemma holomorphic_on_exp: "exp holomorphic_on s" + by (simp add: complex_differentiable_within_exp holomorphic_on_def) + + + +subsection{*Euler and de Moivre formulas.*} + +text{*The sine series times @{term i}*} +lemma sin_ii_eq: "(\n. (ii * sin_coeff n) * z^n) sums (ii * sin z)" +proof - + have "(\n. ii * sin_coeff n *\<^sub>R z^n) sums (ii * sin z)" + using sin_converges sums_mult by blast + then show ?thesis + by (simp add: scaleR_conv_of_real field_simps) +qed + +theorem exp_Euler: "exp(ii * z) = cos(z) + ii * sin(z)" +proof - + have "(\n. (cos_coeff n + ii * sin_coeff n) * z^n) + = (\n. (ii * z) ^ n /\<^sub>R (fact n))" + proof + fix n + show "(cos_coeff n + ii * sin_coeff n) * z^n = (ii * z) ^ n /\<^sub>R (fact n)" + by (auto simp: cos_coeff_def sin_coeff_def scaleR_conv_of_real field_simps elim!: evenE oddE) + qed + also have "... sums (exp (ii * z))" + by (rule exp_converges) + finally have "(\n. (cos_coeff n + ii * sin_coeff n) * z^n) sums (exp (ii * z))" . + moreover have "(\n. (cos_coeff n + ii * sin_coeff n) * z^n) sums (cos z + ii * sin z)" + using sums_add [OF cos_converges [of z] sin_ii_eq [of z]] + by (simp add: field_simps scaleR_conv_of_real) + ultimately show ?thesis + using sums_unique2 by blast +qed + +corollary exp_minus_Euler: "exp(-(ii * z)) = cos(z) - ii * sin(z)" + using exp_Euler [of "-z"] + by simp + +lemma sin_exp_eq: "sin z = (exp(ii * z) - exp(-(ii * z))) / (2*ii)" + by (simp add: exp_Euler exp_minus_Euler) + +lemma sin_exp_eq': "sin z = ii * (exp(-(ii * z)) - exp(ii * z)) / 2" + by (simp add: exp_Euler exp_minus_Euler) + +lemma cos_exp_eq: "cos z = (exp(ii * z) + exp(-(ii * z))) / 2" + by (simp add: exp_Euler exp_minus_Euler) + +subsection{*Relationships between real and complex trig functions*} + +declare sin_of_real [simp] cos_of_real [simp] + +lemma real_sin_eq [simp]: + fixes x::real + shows "Re(sin(of_real x)) = sin x" + by (simp add: sin_of_real) + +lemma real_cos_eq [simp]: + fixes x::real + shows "Re(cos(of_real x)) = cos x" + by (simp add: cos_of_real) + +lemma DeMoivre: "(cos z + ii * sin z) ^ n = cos(n * z) + ii * sin(n * z)" + apply (simp add: exp_Euler [symmetric]) + by (metis exp_of_nat_mult mult.left_commute) + +lemma exp_cnj: + fixes z::complex + shows "cnj (exp z) = exp (cnj z)" +proof - + have "(\n. cnj (z ^ n /\<^sub>R (fact n))) = (\n. (cnj z)^n /\<^sub>R (fact n))" + by auto + also have "... sums (exp (cnj z))" + by (rule exp_converges) + finally have "(\n. cnj (z ^ n /\<^sub>R (fact n))) sums (exp (cnj z))" . + moreover have "(\n. cnj (z ^ n /\<^sub>R (fact n))) sums (cnj (exp z))" + by (metis exp_converges sums_cnj) + ultimately show ?thesis + using sums_unique2 + by blast +qed + +lemma cnj_sin: "cnj(sin z) = sin(cnj z)" + by (simp add: sin_exp_eq exp_cnj field_simps) + +lemma cnj_cos: "cnj(cos z) = cos(cnj z)" + by (simp add: cos_exp_eq exp_cnj field_simps) + +lemma exp_in_Reals [simp]: "z \ \ \ exp z \ \" + by (metis Reals_cases Reals_of_real exp_of_real) + +lemma sin_in_Reals [simp]: "z \ \ \ sin z \ \" + by (metis Reals_cases Reals_of_real sin_of_real) + +lemma cos_in_Reals [simp]: "z \ \ \ cos z \ \" + by (metis Reals_cases Reals_of_real cos_of_real) + +lemma complex_differentiable_at_sin: "sin complex_differentiable at z" + using DERIV_sin complex_differentiable_def by blast + +lemma complex_differentiable_within_sin: "sin complex_differentiable (at z within s)" + by (simp add: complex_differentiable_at_sin complex_differentiable_at_within) + +lemma complex_differentiable_at_cos: "cos complex_differentiable at z" + using DERIV_cos complex_differentiable_def by blast + +lemma complex_differentiable_within_cos: "cos complex_differentiable (at z within s)" + by (simp add: complex_differentiable_at_cos complex_differentiable_at_within) + +lemma holomorphic_on_sin: "sin holomorphic_on s" + by (simp add: complex_differentiable_within_sin holomorphic_on_def) + +lemma holomorphic_on_cos: "cos holomorphic_on s" + by (simp add: complex_differentiable_within_cos holomorphic_on_def) + +subsection{* Get a nice real/imaginary separation in Euler's formula.*} + +lemma Euler: "exp(z) = of_real(exp(Re z)) * + (of_real(cos(Im z)) + ii * of_real(sin(Im z)))" +by (cases z) (simp add: exp_add exp_Euler cos_of_real exp_of_real sin_of_real) + +lemma Re_sin: "Re(sin z) = sin(Re z) * (exp(Im z) + exp(-(Im z))) / 2" + by (simp add: sin_exp_eq field_simps Re_divide Im_exp) + +lemma Im_sin: "Im(sin z) = cos(Re z) * (exp(Im z) - exp(-(Im z))) / 2" + by (simp add: sin_exp_eq field_simps Im_divide Re_exp) + +lemma Re_cos: "Re(cos z) = cos(Re z) * (exp(Im z) + exp(-(Im z))) / 2" + by (simp add: cos_exp_eq field_simps Re_divide Re_exp) + +lemma Im_cos: "Im(cos z) = sin(Re z) * (exp(-(Im z)) - exp(Im z)) / 2" + by (simp add: cos_exp_eq field_simps Im_divide Im_exp) + +(* Now more relatively easy consequences.*) + +lemma sin_times_pi_eq_0: "sin(x * pi) = 0 \ x \ Ints" + by (simp add: sin_zero_iff_int2) (metis Ints_cases Ints_real_of_int real_of_int_def) + +lemma cos_one_2pi: + "cos(x) = 1 \ (\n::nat. x = n * 2*pi) | (\n::nat. x = -(n * 2*pi))" + (is "?lhs = ?rhs") +proof + assume "cos(x) = 1" + then have "sin x = 0" + by (simp add: cos_one_sin_zero) + then show ?rhs + proof (simp only: sin_zero_iff, elim exE disjE conjE) + fix n::nat + assume n: "even n" "x = real n * (pi/2)" + then obtain m where m: "n = 2 * m" + using dvdE by blast + then have me: "even m" using `?lhs` n + by (auto simp: field_simps) (metis one_neq_neg_one power_minus_odd power_one) + show ?rhs + using m me n + by (auto simp: field_simps elim!: evenE) + next + fix n::nat + assume n: "even n" "x = - (real n * (pi/2))" + then obtain m where m: "n = 2 * m" + using dvdE by blast + then have me: "even m" using `?lhs` n + by (auto simp: field_simps) (metis one_neq_neg_one power_minus_odd power_one) + show ?rhs + using m me n + by (auto simp: field_simps elim!: evenE) + qed +next + assume "?rhs" + then show "cos x = 1" + by (metis cos_2npi cos_minus mult.assoc mult.left_commute) +qed + +lemma cos_one_2pi_int: "cos(x) = 1 \ (\n::int. x = n * 2*pi)" + apply auto --{*FIXME simproc bug*} + apply (auto simp: cos_one_2pi) + apply (metis real_of_int_of_nat_eq) + apply (metis mult_minus_right real_of_int_minus real_of_int_of_nat_eq) + by (metis mult_minus_right of_int_of_nat real_of_int_def real_of_nat_def) + +lemma sin_cos_sqrt: "0 \ sin(x) \ (sin(x) = sqrt(1 - (cos(x) ^ 2)))" + using sin_squared_eq real_sqrt_unique by fastforce + +lemma sin_eq_0_pi: "-pi < x \ x < pi \ sin(x) = 0 \ x = 0" + by (metis sin_gt_zero sin_minus minus_less_iff neg_0_less_iff_less not_less_iff_gr_or_eq) + +lemma cos_treble_cos: + fixes x :: "'a::{real_normed_field,banach}" + shows "cos(3 * x) = 4 * cos(x) ^ 3 - 3 * cos x" +proof - + have *: "(sin x * (sin x * 3)) = 3 - (cos x * (cos x * 3))" + by (simp add: mult.assoc [symmetric] sin_squared_eq [unfolded power2_eq_square]) + have "cos(3 * x) = cos(2*x + x)" + by simp + also have "... = 4 * cos(x) ^ 3 - 3 * cos x" + apply (simp only: cos_add cos_double sin_double) + apply (simp add: * field_simps power2_eq_square power3_eq_cube) + done + finally show ?thesis . +qed + +end