author | paulson <lp15@cam.ac.uk> |
Thu, 19 Mar 2015 14:24:51 +0000 | |
changeset 59751 | 916c0f6c83e3 |
parent 59746 | ddae5727c5a9 |
child 59862 | 44b3f4fa33ca |
permissions | -rw-r--r-- |
59746
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
1 |
(* Author: John Harrison |
59745
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
2 |
Ported from "hol_light/Multivariate/transcendentals.ml" by L C Paulson (2015) |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
3 |
*) |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
4 |
|
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
5 |
section {* Complex Transcendental Functions *} |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
6 |
|
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
7 |
theory Complex_Transcendental |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
8 |
imports "~~/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics" |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
9 |
begin |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
10 |
|
59746
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
11 |
subsection{*The Exponential Function is Differentiable and Continuous*} |
59745
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
12 |
|
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
13 |
lemma complex_differentiable_at_exp: "exp complex_differentiable at z" |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
14 |
using DERIV_exp complex_differentiable_def by blast |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
15 |
|
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
16 |
lemma complex_differentiable_within_exp: "exp complex_differentiable (at z within s)" |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
17 |
by (simp add: complex_differentiable_at_exp complex_differentiable_at_within) |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
18 |
|
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
19 |
lemma continuous_within_exp: |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
20 |
fixes z::"'a::{real_normed_field,banach}" |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
21 |
shows "continuous (at z within s) exp" |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
22 |
by (simp add: continuous_at_imp_continuous_within) |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
23 |
|
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
24 |
lemma continuous_on_exp: |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
25 |
fixes s::"'a::{real_normed_field,banach} set" |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
26 |
shows "continuous_on s exp" |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
27 |
by (simp add: continuous_on_exp continuous_on_id) |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
28 |
|
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
29 |
lemma holomorphic_on_exp: "exp holomorphic_on s" |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
30 |
by (simp add: complex_differentiable_within_exp holomorphic_on_def) |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
31 |
|
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
32 |
subsection{*Euler and de Moivre formulas.*} |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
33 |
|
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
34 |
text{*The sine series times @{term i}*} |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
35 |
lemma sin_ii_eq: "(\<lambda>n. (ii * sin_coeff n) * z^n) sums (ii * sin z)" |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
36 |
proof - |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
37 |
have "(\<lambda>n. ii * sin_coeff n *\<^sub>R z^n) sums (ii * sin z)" |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
38 |
using sin_converges sums_mult by blast |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
39 |
then show ?thesis |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
40 |
by (simp add: scaleR_conv_of_real field_simps) |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
41 |
qed |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
42 |
|
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
43 |
theorem exp_Euler: "exp(ii * z) = cos(z) + ii * sin(z)" |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
44 |
proof - |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
45 |
have "(\<lambda>n. (cos_coeff n + ii * sin_coeff n) * z^n) |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
46 |
= (\<lambda>n. (ii * z) ^ n /\<^sub>R (fact n))" |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
47 |
proof |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
48 |
fix n |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
49 |
show "(cos_coeff n + ii * sin_coeff n) * z^n = (ii * z) ^ n /\<^sub>R (fact n)" |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
50 |
by (auto simp: cos_coeff_def sin_coeff_def scaleR_conv_of_real field_simps elim!: evenE oddE) |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
51 |
qed |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
52 |
also have "... sums (exp (ii * z))" |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
53 |
by (rule exp_converges) |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
54 |
finally have "(\<lambda>n. (cos_coeff n + ii * sin_coeff n) * z^n) sums (exp (ii * z))" . |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
55 |
moreover have "(\<lambda>n. (cos_coeff n + ii * sin_coeff n) * z^n) sums (cos z + ii * sin z)" |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
56 |
using sums_add [OF cos_converges [of z] sin_ii_eq [of z]] |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
57 |
by (simp add: field_simps scaleR_conv_of_real) |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
58 |
ultimately show ?thesis |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
59 |
using sums_unique2 by blast |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
60 |
qed |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
61 |
|
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
62 |
corollary exp_minus_Euler: "exp(-(ii * z)) = cos(z) - ii * sin(z)" |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
63 |
using exp_Euler [of "-z"] |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
64 |
by simp |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
65 |
|
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
66 |
lemma sin_exp_eq: "sin z = (exp(ii * z) - exp(-(ii * z))) / (2*ii)" |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
67 |
by (simp add: exp_Euler exp_minus_Euler) |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
68 |
|
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
69 |
lemma sin_exp_eq': "sin z = ii * (exp(-(ii * z)) - exp(ii * z)) / 2" |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
70 |
by (simp add: exp_Euler exp_minus_Euler) |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
71 |
|
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
72 |
lemma cos_exp_eq: "cos z = (exp(ii * z) + exp(-(ii * z))) / 2" |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
73 |
by (simp add: exp_Euler exp_minus_Euler) |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
74 |
|
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
75 |
subsection{*Relationships between real and complex trig functions*} |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
76 |
|
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
77 |
declare sin_of_real [simp] cos_of_real [simp] |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
78 |
|
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
79 |
lemma real_sin_eq [simp]: |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
80 |
fixes x::real |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
81 |
shows "Re(sin(of_real x)) = sin x" |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
82 |
by (simp add: sin_of_real) |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
83 |
|
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
84 |
lemma real_cos_eq [simp]: |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
85 |
fixes x::real |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
86 |
shows "Re(cos(of_real x)) = cos x" |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
87 |
by (simp add: cos_of_real) |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
88 |
|
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
89 |
lemma DeMoivre: "(cos z + ii * sin z) ^ n = cos(n * z) + ii * sin(n * z)" |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
90 |
apply (simp add: exp_Euler [symmetric]) |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
91 |
by (metis exp_of_nat_mult mult.left_commute) |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
92 |
|
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
93 |
lemma exp_cnj: |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
94 |
fixes z::complex |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
95 |
shows "cnj (exp z) = exp (cnj z)" |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
96 |
proof - |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
97 |
have "(\<lambda>n. cnj (z ^ n /\<^sub>R (fact n))) = (\<lambda>n. (cnj z)^n /\<^sub>R (fact n))" |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
98 |
by auto |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
99 |
also have "... sums (exp (cnj z))" |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
100 |
by (rule exp_converges) |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
101 |
finally have "(\<lambda>n. cnj (z ^ n /\<^sub>R (fact n))) sums (exp (cnj z))" . |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
102 |
moreover have "(\<lambda>n. cnj (z ^ n /\<^sub>R (fact n))) sums (cnj (exp z))" |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
103 |
by (metis exp_converges sums_cnj) |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
104 |
ultimately show ?thesis |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
105 |
using sums_unique2 |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
106 |
by blast |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
107 |
qed |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
108 |
|
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
109 |
lemma cnj_sin: "cnj(sin z) = sin(cnj z)" |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
110 |
by (simp add: sin_exp_eq exp_cnj field_simps) |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
111 |
|
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
112 |
lemma cnj_cos: "cnj(cos z) = cos(cnj z)" |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
113 |
by (simp add: cos_exp_eq exp_cnj field_simps) |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
114 |
|
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
115 |
lemma exp_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> exp z \<in> \<real>" |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
116 |
by (metis Reals_cases Reals_of_real exp_of_real) |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
117 |
|
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
118 |
lemma sin_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> sin z \<in> \<real>" |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
119 |
by (metis Reals_cases Reals_of_real sin_of_real) |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
120 |
|
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
121 |
lemma cos_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> cos z \<in> \<real>" |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
122 |
by (metis Reals_cases Reals_of_real cos_of_real) |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
123 |
|
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
124 |
lemma complex_differentiable_at_sin: "sin complex_differentiable at z" |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
125 |
using DERIV_sin complex_differentiable_def by blast |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
126 |
|
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
127 |
lemma complex_differentiable_within_sin: "sin complex_differentiable (at z within s)" |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
128 |
by (simp add: complex_differentiable_at_sin complex_differentiable_at_within) |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
129 |
|
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
130 |
lemma complex_differentiable_at_cos: "cos complex_differentiable at z" |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
131 |
using DERIV_cos complex_differentiable_def by blast |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
132 |
|
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
133 |
lemma complex_differentiable_within_cos: "cos complex_differentiable (at z within s)" |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
134 |
by (simp add: complex_differentiable_at_cos complex_differentiable_at_within) |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
135 |
|
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
136 |
lemma holomorphic_on_sin: "sin holomorphic_on s" |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
137 |
by (simp add: complex_differentiable_within_sin holomorphic_on_def) |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
138 |
|
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
139 |
lemma holomorphic_on_cos: "cos holomorphic_on s" |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
140 |
by (simp add: complex_differentiable_within_cos holomorphic_on_def) |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
141 |
|
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
142 |
subsection{* Get a nice real/imaginary separation in Euler's formula.*} |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
143 |
|
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
144 |
lemma Euler: "exp(z) = of_real(exp(Re z)) * |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
145 |
(of_real(cos(Im z)) + ii * of_real(sin(Im z)))" |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
146 |
by (cases z) (simp add: exp_add exp_Euler cos_of_real exp_of_real sin_of_real) |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
147 |
|
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
148 |
lemma Re_sin: "Re(sin z) = sin(Re z) * (exp(Im z) + exp(-(Im z))) / 2" |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
149 |
by (simp add: sin_exp_eq field_simps Re_divide Im_exp) |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
150 |
|
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
151 |
lemma Im_sin: "Im(sin z) = cos(Re z) * (exp(Im z) - exp(-(Im z))) / 2" |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
152 |
by (simp add: sin_exp_eq field_simps Im_divide Re_exp) |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
153 |
|
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
154 |
lemma Re_cos: "Re(cos z) = cos(Re z) * (exp(Im z) + exp(-(Im z))) / 2" |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
155 |
by (simp add: cos_exp_eq field_simps Re_divide Re_exp) |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
156 |
|
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
157 |
lemma Im_cos: "Im(cos z) = sin(Re z) * (exp(-(Im z)) - exp(Im z)) / 2" |
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
158 |
by (simp add: cos_exp_eq field_simps Im_divide Im_exp) |
59746
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
159 |
|
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
160 |
subsection{*More on the Polar Representation of Complex Numbers*} |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
161 |
|
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
162 |
lemma exp_Complex: "exp(Complex r t) = of_real(exp r) * Complex (cos t) (sin t)" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
163 |
by (simp add: exp_add exp_Euler exp_of_real) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
164 |
|
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
165 |
lemma exp_eq_1: "exp z = 1 \<longleftrightarrow> Re(z) = 0 \<and> (\<exists>n::int. Im(z) = of_int (2 * n) * pi)" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
166 |
apply auto |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
167 |
apply (metis exp_eq_one_iff norm_exp_eq_Re norm_one) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
168 |
apply (metis Re_exp cos_one_2pi_int mult.commute mult.left_neutral norm_exp_eq_Re norm_one one_complex.simps(1) real_of_int_def) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
169 |
by (metis Im_exp Re_exp complex_Re_Im_cancel_iff cos_one_2pi_int sin_double Re_complex_of_real complex_Re_numeral exp_zero mult.assoc mult.left_commute mult_eq_0_iff mult_numeral_1 numeral_One of_real_0 real_of_int_def sin_zero_iff_int2) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
170 |
|
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
171 |
lemma exp_eq: "exp w = exp z \<longleftrightarrow> (\<exists>n::int. w = z + (of_int (2 * n) * pi) * ii)" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
172 |
(is "?lhs = ?rhs") |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
173 |
proof - |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
174 |
have "exp w = exp z \<longleftrightarrow> exp (w-z) = 1" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
175 |
by (simp add: exp_diff) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
176 |
also have "... \<longleftrightarrow> (Re w = Re z \<and> (\<exists>n::int. Im w - Im z = of_int (2 * n) * pi))" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
177 |
by (simp add: exp_eq_1) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
178 |
also have "... \<longleftrightarrow> ?rhs" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
179 |
by (auto simp: algebra_simps intro!: complex_eqI) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
180 |
finally show ?thesis . |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
181 |
qed |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
182 |
|
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
183 |
lemma exp_complex_eqI: "abs(Im w - Im z) < 2*pi \<Longrightarrow> exp w = exp z \<Longrightarrow> w = z" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
184 |
by (auto simp: exp_eq abs_mult) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
185 |
|
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
186 |
lemma exp_integer_2pi: |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
187 |
assumes "n \<in> Ints" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
188 |
shows "exp((2 * n * pi) * ii) = 1" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
189 |
proof - |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
190 |
have "exp((2 * n * pi) * ii) = exp 0" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
191 |
using assms |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
192 |
by (simp only: Ints_def exp_eq) auto |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
193 |
also have "... = 1" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
194 |
by simp |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
195 |
finally show ?thesis . |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
196 |
qed |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
197 |
|
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
198 |
lemma sin_cos_eq_iff: "sin y = sin x \<and> cos y = cos x \<longleftrightarrow> (\<exists>n::int. y = x + 2 * n * pi)" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
199 |
proof - |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
200 |
{ assume "sin y = sin x" "cos y = cos x" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
201 |
then have "cos (y-x) = 1" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
202 |
using cos_add [of y "-x"] by simp |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
203 |
then have "\<exists>n::int. y-x = real n * 2 * pi" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
204 |
using cos_one_2pi_int by blast } |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
205 |
then show ?thesis |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
206 |
apply (auto simp: sin_add cos_add) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
207 |
apply (metis add.commute diff_add_cancel mult.commute) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
208 |
done |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
209 |
qed |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
210 |
|
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
211 |
lemma exp_i_ne_1: |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
212 |
assumes "0 < x" "x < 2*pi" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
213 |
shows "exp(\<i> * of_real x) \<noteq> 1" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
214 |
proof |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
215 |
assume "exp (\<i> * of_real x) = 1" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
216 |
then have "exp (\<i> * of_real x) = exp 0" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
217 |
by simp |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
218 |
then obtain n where "\<i> * of_real x = (of_int (2 * n) * pi) * \<i>" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
219 |
by (simp only: Ints_def exp_eq) auto |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
220 |
then have "of_real x = (of_int (2 * n) * pi)" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
221 |
by (metis complex_i_not_zero mult.commute mult_cancel_left of_real_eq_iff real_scaleR_def scaleR_conv_of_real) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
222 |
then have "x = (of_int (2 * n) * pi)" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
223 |
by simp |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
224 |
then show False using assms |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
225 |
by (cases n) (auto simp: zero_less_mult_iff mult_less_0_iff) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
226 |
qed |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
227 |
|
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
228 |
lemma sin_eq_0: |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
229 |
fixes z::complex |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
230 |
shows "sin z = 0 \<longleftrightarrow> (\<exists>n::int. z = of_real(n * pi))" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
231 |
by (simp add: sin_exp_eq exp_eq of_real_numeral) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
232 |
|
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
233 |
lemma cos_eq_0: |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
234 |
fixes z::complex |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
235 |
shows "cos z = 0 \<longleftrightarrow> (\<exists>n::int. z = of_real(n * pi) + of_real pi/2)" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
236 |
using sin_eq_0 [of "z - of_real pi/2"] |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
237 |
by (simp add: sin_diff algebra_simps) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
238 |
|
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
239 |
lemma cos_eq_1: |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
240 |
fixes z::complex |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
241 |
shows "cos z = 1 \<longleftrightarrow> (\<exists>n::int. z = of_real(2 * n * pi))" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
242 |
proof - |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
243 |
have "cos z = cos (2*(z/2))" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
244 |
by simp |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
245 |
also have "... = 1 - 2 * sin (z/2) ^ 2" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
246 |
by (simp only: cos_double_sin) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
247 |
finally have [simp]: "cos z = 1 \<longleftrightarrow> sin (z/2) = 0" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
248 |
by simp |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
249 |
show ?thesis |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
250 |
by (auto simp: sin_eq_0 of_real_numeral) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
251 |
qed |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
252 |
|
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
253 |
lemma csin_eq_1: |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
254 |
fixes z::complex |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
255 |
shows "sin z = 1 \<longleftrightarrow> (\<exists>n::int. z = of_real(2 * n * pi) + of_real pi/2)" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
256 |
using cos_eq_1 [of "z - of_real pi/2"] |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
257 |
by (simp add: cos_diff algebra_simps) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
258 |
|
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
259 |
lemma csin_eq_minus1: |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
260 |
fixes z::complex |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
261 |
shows "sin z = -1 \<longleftrightarrow> (\<exists>n::int. z = of_real(2 * n * pi) + 3/2*pi)" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
262 |
(is "_ = ?rhs") |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
263 |
proof - |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
264 |
have "sin z = -1 \<longleftrightarrow> sin (-z) = 1" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
265 |
by (simp add: equation_minus_iff) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
266 |
also have "... \<longleftrightarrow> (\<exists>n::int. -z = of_real(2 * n * pi) + of_real pi/2)" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
267 |
by (simp only: csin_eq_1) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
268 |
also have "... \<longleftrightarrow> (\<exists>n::int. z = - of_real(2 * n * pi) - of_real pi/2)" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
269 |
apply (rule iff_exI) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
270 |
by (metis (no_types) is_num_normalize(8) minus_minus of_real_def real_vector.scale_minus_left uminus_add_conv_diff) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
271 |
also have "... = ?rhs" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
272 |
apply (auto simp: of_real_numeral) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
273 |
apply (rule_tac [2] x="-(x+1)" in exI) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
274 |
apply (rule_tac x="-(x+1)" in exI) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
275 |
apply (simp_all add: algebra_simps) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
276 |
done |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
277 |
finally show ?thesis . |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
278 |
qed |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
279 |
|
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
280 |
lemma ccos_eq_minus1: |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
281 |
fixes z::complex |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
282 |
shows "cos z = -1 \<longleftrightarrow> (\<exists>n::int. z = of_real(2 * n * pi) + pi)" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
283 |
using csin_eq_1 [of "z - of_real pi/2"] |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
284 |
apply (simp add: sin_diff) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
285 |
apply (simp add: algebra_simps of_real_numeral equation_minus_iff) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
286 |
done |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
287 |
|
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
288 |
lemma sin_eq_1: "sin x = 1 \<longleftrightarrow> (\<exists>n::int. x = (2 * n + 1 / 2) * pi)" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
289 |
(is "_ = ?rhs") |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
290 |
proof - |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
291 |
have "sin x = 1 \<longleftrightarrow> sin (complex_of_real x) = 1" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
292 |
by (metis of_real_1 one_complex.simps(1) real_sin_eq sin_of_real) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
293 |
also have "... \<longleftrightarrow> (\<exists>n::int. complex_of_real x = of_real(2 * n * pi) + of_real pi/2)" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
294 |
by (simp only: csin_eq_1) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
295 |
also have "... \<longleftrightarrow> (\<exists>n::int. x = of_real(2 * n * pi) + of_real pi/2)" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
296 |
apply (rule iff_exI) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
297 |
apply (auto simp: algebra_simps of_real_numeral) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
298 |
apply (rule injD [OF inj_of_real [where 'a = complex]]) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
299 |
apply (auto simp: of_real_numeral) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
300 |
done |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
301 |
also have "... = ?rhs" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
302 |
by (auto simp: algebra_simps) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
303 |
finally show ?thesis . |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
304 |
qed |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
305 |
|
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
306 |
lemma sin_eq_minus1: "sin x = -1 \<longleftrightarrow> (\<exists>n::int. x = (2*n + 3/2) * pi)" (is "_ = ?rhs") |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
307 |
proof - |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
308 |
have "sin x = -1 \<longleftrightarrow> sin (complex_of_real x) = -1" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
309 |
by (metis Re_complex_of_real of_real_def scaleR_minus1_left sin_of_real) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
310 |
also have "... \<longleftrightarrow> (\<exists>n::int. complex_of_real x = of_real(2 * n * pi) + 3/2*pi)" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
311 |
by (simp only: csin_eq_minus1) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
312 |
also have "... \<longleftrightarrow> (\<exists>n::int. x = of_real(2 * n * pi) + 3/2*pi)" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
313 |
apply (rule iff_exI) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
314 |
apply (auto simp: algebra_simps) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
315 |
apply (rule injD [OF inj_of_real [where 'a = complex]], auto) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
316 |
done |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
317 |
also have "... = ?rhs" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
318 |
by (auto simp: algebra_simps) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
319 |
finally show ?thesis . |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
320 |
qed |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
321 |
|
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
322 |
lemma cos_eq_minus1: "cos x = -1 \<longleftrightarrow> (\<exists>n::int. x = (2*n + 1) * pi)" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
323 |
(is "_ = ?rhs") |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
324 |
proof - |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
325 |
have "cos x = -1 \<longleftrightarrow> cos (complex_of_real x) = -1" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
326 |
by (metis Re_complex_of_real of_real_def scaleR_minus1_left cos_of_real) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
327 |
also have "... \<longleftrightarrow> (\<exists>n::int. complex_of_real x = of_real(2 * n * pi) + pi)" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
328 |
by (simp only: ccos_eq_minus1) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
329 |
also have "... \<longleftrightarrow> (\<exists>n::int. x = of_real(2 * n * pi) + pi)" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
330 |
apply (rule iff_exI) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
331 |
apply (auto simp: algebra_simps) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
332 |
apply (rule injD [OF inj_of_real [where 'a = complex]], auto) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
333 |
done |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
334 |
also have "... = ?rhs" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
335 |
by (auto simp: algebra_simps) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
336 |
finally show ?thesis . |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
337 |
qed |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
338 |
|
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
339 |
lemma dist_exp_ii_1: "norm(exp(ii * of_real t) - 1) = 2 * abs(sin(t / 2))" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
340 |
apply (simp add: exp_Euler cmod_def power2_diff algebra_simps) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
341 |
using cos_double_sin [of "t/2"] |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
342 |
apply (simp add: real_sqrt_mult) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
343 |
done |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
344 |
|
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
345 |
lemma sinh_complex: |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
346 |
fixes z :: complex |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
347 |
shows "(exp z - inverse (exp z)) / 2 = -ii * sin(ii * z)" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
348 |
by (simp add: sin_exp_eq divide_simps exp_minus of_real_numeral) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
349 |
|
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
350 |
lemma sin_ii_times: |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
351 |
fixes z :: complex |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
352 |
shows "sin(ii * z) = ii * ((exp z - inverse (exp z)) / 2)" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
353 |
using sinh_complex by auto |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
354 |
|
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
355 |
lemma sinh_real: |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
356 |
fixes x :: real |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
357 |
shows "of_real((exp x - inverse (exp x)) / 2) = -ii * sin(ii * of_real x)" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
358 |
by (simp add: exp_of_real sin_ii_times of_real_numeral) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
359 |
|
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
360 |
lemma cosh_complex: |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
361 |
fixes z :: complex |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
362 |
shows "(exp z + inverse (exp z)) / 2 = cos(ii * z)" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
363 |
by (simp add: cos_exp_eq divide_simps exp_minus of_real_numeral exp_of_real) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
364 |
|
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
365 |
lemma cosh_real: |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
366 |
fixes x :: real |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
367 |
shows "of_real((exp x + inverse (exp x)) / 2) = cos(ii * of_real x)" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
368 |
by (simp add: cos_exp_eq divide_simps exp_minus of_real_numeral exp_of_real) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
369 |
|
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
370 |
lemmas cos_ii_times = cosh_complex [symmetric] |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
371 |
|
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
372 |
lemma norm_cos_squared: |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
373 |
"norm(cos z) ^ 2 = cos(Re z) ^ 2 + (exp(Im z) - inverse(exp(Im z))) ^ 2 / 4" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
374 |
apply (cases z) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
375 |
apply (simp add: cos_add cmod_power2 cos_of_real sin_of_real) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
376 |
apply (simp add: cos_exp_eq sin_exp_eq exp_minus exp_of_real Re_divide Im_divide) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
377 |
apply (simp only: left_diff_distrib [symmetric] power_mult_distrib) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
378 |
apply (simp add: sin_squared_eq) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
379 |
apply (simp add: power2_eq_square algebra_simps divide_simps) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
380 |
done |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
381 |
|
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
382 |
lemma norm_sin_squared: |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
383 |
"norm(sin z) ^ 2 = (exp(2 * Im z) + inverse(exp(2 * Im z)) - 2 * cos(2 * Re z)) / 4" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
384 |
apply (cases z) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
385 |
apply (simp add: sin_add cmod_power2 cos_of_real sin_of_real cos_double_cos exp_double) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
386 |
apply (simp add: cos_exp_eq sin_exp_eq exp_minus exp_of_real Re_divide Im_divide) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
387 |
apply (simp only: left_diff_distrib [symmetric] power_mult_distrib) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
388 |
apply (simp add: cos_squared_eq) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
389 |
apply (simp add: power2_eq_square algebra_simps divide_simps) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
390 |
done |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
391 |
|
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
392 |
lemma exp_uminus_Im: "exp (- Im z) \<le> exp (cmod z)" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
393 |
using abs_Im_le_cmod linear order_trans by fastforce |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
394 |
|
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
395 |
lemma norm_cos_le: |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
396 |
fixes z::complex |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
397 |
shows "norm(cos z) \<le> exp(norm z)" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
398 |
proof - |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
399 |
have "Im z \<le> cmod z" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
400 |
using abs_Im_le_cmod abs_le_D1 by auto |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
401 |
with exp_uminus_Im show ?thesis |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
402 |
apply (simp add: cos_exp_eq norm_divide) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
403 |
apply (rule order_trans [OF norm_triangle_ineq], simp) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
404 |
apply (metis add_mono exp_le_cancel_iff mult_2_right) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
405 |
done |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
406 |
qed |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
407 |
|
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
408 |
lemma norm_cos_plus1_le: |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
409 |
fixes z::complex |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
410 |
shows "norm(1 + cos z) \<le> 2 * exp(norm z)" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
411 |
proof - |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
412 |
have mono: "\<And>u w z::real. (1 \<le> w | 1 \<le> z) \<Longrightarrow> (w \<le> u & z \<le> u) \<Longrightarrow> 2 + w + z \<le> 4 * u" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
413 |
by arith |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
414 |
have *: "Im z \<le> cmod z" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
415 |
using abs_Im_le_cmod abs_le_D1 by auto |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
416 |
have triangle3: "\<And>x y z. norm(x + y + z) \<le> norm(x) + norm(y) + norm(z)" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
417 |
by (simp add: norm_add_rule_thm) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
418 |
have "norm(1 + cos z) = cmod (1 + (exp (\<i> * z) + exp (- (\<i> * z))) / 2)" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
419 |
by (simp add: cos_exp_eq) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
420 |
also have "... = cmod ((2 + exp (\<i> * z) + exp (- (\<i> * z))) / 2)" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
421 |
by (simp add: field_simps) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
422 |
also have "... = cmod (2 + exp (\<i> * z) + exp (- (\<i> * z))) / 2" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
423 |
by (simp add: norm_divide) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
424 |
finally show ?thesis |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
425 |
apply (rule ssubst, simp) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
426 |
apply (rule order_trans [OF triangle3], simp) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
427 |
using exp_uminus_Im * |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
428 |
apply (auto intro: mono) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
429 |
done |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
430 |
qed |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
431 |
|
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
432 |
subsection{* Taylor series for complex exponential, sine and cosine.*} |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
433 |
|
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
434 |
context |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
435 |
begin |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
436 |
|
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
437 |
declare power_Suc [simp del] |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
438 |
|
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
439 |
lemma Taylor_exp: |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
440 |
"norm(exp z - (\<Sum>k\<le>n. z ^ k / (fact k))) \<le> exp\<bar>Re z\<bar> * (norm z) ^ (Suc n) / (fact n)" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
441 |
proof (rule complex_taylor [of _ n "\<lambda>k. exp" "exp\<bar>Re z\<bar>" 0 z, simplified]) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
442 |
show "convex (closed_segment 0 z)" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
443 |
by (rule convex_segment [of 0 z]) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
444 |
next |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
445 |
fix k x |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
446 |
assume "x \<in> closed_segment 0 z" "k \<le> n" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
447 |
show "(exp has_field_derivative exp x) (at x within closed_segment 0 z)" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
448 |
using DERIV_exp DERIV_subset by blast |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
449 |
next |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
450 |
fix x |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
451 |
assume "x \<in> closed_segment 0 z" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
452 |
then show "Re x \<le> \<bar>Re z\<bar>" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
453 |
apply (auto simp: closed_segment_def scaleR_conv_of_real) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
454 |
by (meson abs_ge_self abs_ge_zero linear mult_left_le_one_le mult_nonneg_nonpos order_trans) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
455 |
next |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
456 |
show "0 \<in> closed_segment 0 z" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
457 |
by (auto simp: closed_segment_def) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
458 |
next |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
459 |
show "z \<in> closed_segment 0 z" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
460 |
apply (simp add: closed_segment_def scaleR_conv_of_real) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
461 |
using of_real_1 zero_le_one by blast |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
462 |
qed |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
463 |
|
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
464 |
lemma |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
465 |
assumes "0 \<le> u" "u \<le> 1" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
466 |
shows cmod_sin_le_exp: "cmod (sin (u *\<^sub>R z)) \<le> exp \<bar>Im z\<bar>" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
467 |
and cmod_cos_le_exp: "cmod (cos (u *\<^sub>R z)) \<le> exp \<bar>Im z\<bar>" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
468 |
proof - |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
469 |
have mono: "\<And>u w z::real. w \<le> u \<Longrightarrow> z \<le> u \<Longrightarrow> w + z \<le> u*2" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
470 |
by arith |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
471 |
show "cmod (sin (u *\<^sub>R z)) \<le> exp \<bar>Im z\<bar>" using assms |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
472 |
apply (auto simp: scaleR_conv_of_real norm_mult norm_power sin_exp_eq norm_divide) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
473 |
apply (rule order_trans [OF norm_triangle_ineq4]) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
474 |
apply (rule mono) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
475 |
apply (auto simp: abs_if mult_left_le_one_le) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
476 |
apply (meson mult_nonneg_nonneg neg_le_0_iff_le not_le order_trans) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
477 |
apply (meson less_eq_real_def mult_nonneg_nonpos neg_0_le_iff_le order_trans) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
478 |
done |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
479 |
show "cmod (cos (u *\<^sub>R z)) \<le> exp \<bar>Im z\<bar>" using assms |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
480 |
apply (auto simp: scaleR_conv_of_real norm_mult norm_power cos_exp_eq norm_divide) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
481 |
apply (rule order_trans [OF norm_triangle_ineq]) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
482 |
apply (rule mono) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
483 |
apply (auto simp: abs_if mult_left_le_one_le) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
484 |
apply (meson mult_nonneg_nonneg neg_le_0_iff_le not_le order_trans) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
485 |
apply (meson less_eq_real_def mult_nonneg_nonpos neg_0_le_iff_le order_trans) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
486 |
done |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
487 |
qed |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
488 |
|
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
489 |
lemma Taylor_sin: |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
490 |
"norm(sin z - (\<Sum>k\<le>n. complex_of_real (sin_coeff k) * z ^ k)) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
491 |
\<le> exp\<bar>Im z\<bar> * (norm z) ^ (Suc n) / (fact n)" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
492 |
proof - |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
493 |
have mono: "\<And>u w z::real. w \<le> u \<Longrightarrow> z \<le> u \<Longrightarrow> w + z \<le> u*2" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
494 |
by arith |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
495 |
have *: "cmod (sin z - |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
496 |
(\<Sum>i\<le>n. (-1) ^ (i div 2) * (if even i then sin 0 else cos 0) * z ^ i / (fact i))) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
497 |
\<le> exp \<bar>Im z\<bar> * cmod z ^ Suc n / (fact n)" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
498 |
proof (rule complex_taylor [of "closed_segment 0 z" n "\<lambda>k x. (-1)^(k div 2) * (if even k then sin x else cos x)" "exp\<bar>Im z\<bar>" 0 z, |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
499 |
simplified]) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
500 |
show "convex (closed_segment 0 z)" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
501 |
by (rule convex_segment [of 0 z]) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
502 |
next |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
503 |
fix k x |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
504 |
show "((\<lambda>x. (- 1) ^ (k div 2) * (if even k then sin x else cos x)) has_field_derivative |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
505 |
(- 1) ^ (Suc k div 2) * (if odd k then sin x else cos x)) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
506 |
(at x within closed_segment 0 z)" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
507 |
apply (auto simp: power_Suc) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
508 |
apply (intro derivative_eq_intros | simp)+ |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
509 |
done |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
510 |
next |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
511 |
fix x |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
512 |
assume "x \<in> closed_segment 0 z" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
513 |
then show "cmod ((- 1) ^ (Suc n div 2) * (if odd n then sin x else cos x)) \<le> exp \<bar>Im z\<bar>" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
514 |
by (auto simp: closed_segment_def norm_mult norm_power cmod_sin_le_exp cmod_cos_le_exp) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
515 |
next |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
516 |
show "0 \<in> closed_segment 0 z" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
517 |
by (auto simp: closed_segment_def) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
518 |
next |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
519 |
show "z \<in> closed_segment 0 z" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
520 |
apply (simp add: closed_segment_def scaleR_conv_of_real) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
521 |
using of_real_1 zero_le_one by blast |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
522 |
qed |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
523 |
have **: "\<And>k. complex_of_real (sin_coeff k) * z ^ k |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
524 |
= (-1)^(k div 2) * (if even k then sin 0 else cos 0) * z^k / of_nat (fact k)" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
525 |
by (auto simp: sin_coeff_def elim!: oddE) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
526 |
show ?thesis |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
527 |
apply (rule order_trans [OF _ *]) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
528 |
apply (simp add: **) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
529 |
done |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
530 |
qed |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
531 |
|
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
532 |
lemma Taylor_cos: |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
533 |
"norm(cos z - (\<Sum>k\<le>n. complex_of_real (cos_coeff k) * z ^ k)) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
534 |
\<le> exp\<bar>Im z\<bar> * (norm z) ^ Suc n / (fact n)" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
535 |
proof - |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
536 |
have mono: "\<And>u w z::real. w \<le> u \<Longrightarrow> z \<le> u \<Longrightarrow> w + z \<le> u*2" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
537 |
by arith |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
538 |
have *: "cmod (cos z - |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
539 |
(\<Sum>i\<le>n. (-1) ^ (Suc i div 2) * (if even i then cos 0 else sin 0) * z ^ i / (fact i))) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
540 |
\<le> exp \<bar>Im z\<bar> * cmod z ^ Suc n / (fact n)" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
541 |
proof (rule complex_taylor [of "closed_segment 0 z" n "\<lambda>k x. (-1)^(Suc k div 2) * (if even k then cos x else sin x)" "exp\<bar>Im z\<bar>" 0 z, |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
542 |
simplified]) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
543 |
show "convex (closed_segment 0 z)" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
544 |
by (rule convex_segment [of 0 z]) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
545 |
next |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
546 |
fix k x |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
547 |
assume "x \<in> closed_segment 0 z" "k \<le> n" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
548 |
show "((\<lambda>x. (- 1) ^ (Suc k div 2) * (if even k then cos x else sin x)) has_field_derivative |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
549 |
(- 1) ^ Suc (k div 2) * (if odd k then cos x else sin x)) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
550 |
(at x within closed_segment 0 z)" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
551 |
apply (auto simp: power_Suc) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
552 |
apply (intro derivative_eq_intros | simp)+ |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
553 |
done |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
554 |
next |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
555 |
fix x |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
556 |
assume "x \<in> closed_segment 0 z" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
557 |
then show "cmod ((- 1) ^ Suc (n div 2) * (if odd n then cos x else sin x)) \<le> exp \<bar>Im z\<bar>" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
558 |
by (auto simp: closed_segment_def norm_mult norm_power cmod_sin_le_exp cmod_cos_le_exp) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
559 |
next |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
560 |
show "0 \<in> closed_segment 0 z" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
561 |
by (auto simp: closed_segment_def) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
562 |
next |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
563 |
show "z \<in> closed_segment 0 z" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
564 |
apply (simp add: closed_segment_def scaleR_conv_of_real) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
565 |
using of_real_1 zero_le_one by blast |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
566 |
qed |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
567 |
have **: "\<And>k. complex_of_real (cos_coeff k) * z ^ k |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
568 |
= (-1)^(Suc k div 2) * (if even k then cos 0 else sin 0) * z^k / of_nat (fact k)" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
569 |
by (auto simp: cos_coeff_def elim!: evenE) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
570 |
show ?thesis |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
571 |
apply (rule order_trans [OF _ *]) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
572 |
apply (simp add: **) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
573 |
done |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
574 |
qed |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
575 |
|
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
576 |
end (* of context *) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
577 |
|
59751
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
578 |
text{*32-bit Approximation to e*} |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
579 |
lemma e_approx_32: "abs(exp(1) - 5837465777 / 2147483648) \<le> (inverse(2 ^ 32)::real)" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
580 |
using Taylor_exp [of 1 14] exp_le |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
581 |
apply (simp add: setsum_left_distrib in_Reals_norm Re_exp atMost_nat_numeral fact_numeral) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
582 |
apply (simp only: pos_le_divide_eq [symmetric], linarith) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
583 |
done |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
584 |
|
59746
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
585 |
subsection{*The argument of a complex number*} |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
586 |
|
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
587 |
definition Arg :: "complex \<Rightarrow> real" where |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
588 |
"Arg z \<equiv> if z = 0 then 0 |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
589 |
else THE t. 0 \<le> t \<and> t < 2*pi \<and> |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
590 |
z = of_real(norm z) * exp(ii * of_real t)" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
591 |
|
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
592 |
lemma Arg_0 [simp]: "Arg(0) = 0" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
593 |
by (simp add: Arg_def) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
594 |
|
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
595 |
lemma Arg_unique_lemma: |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
596 |
assumes z: "z = of_real(norm z) * exp(ii * of_real t)" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
597 |
and z': "z = of_real(norm z) * exp(ii * of_real t')" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
598 |
and t: "0 \<le> t" "t < 2*pi" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
599 |
and t': "0 \<le> t'" "t' < 2*pi" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
600 |
and nz: "z \<noteq> 0" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
601 |
shows "t' = t" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
602 |
proof - |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
603 |
have [dest]: "\<And>x y z::real. x\<ge>0 \<Longrightarrow> x+y < z \<Longrightarrow> y<z" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
604 |
by arith |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
605 |
have "of_real (cmod z) * exp (\<i> * of_real t') = of_real (cmod z) * exp (\<i> * of_real t)" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
606 |
by (metis z z') |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
607 |
then have "exp (\<i> * of_real t') = exp (\<i> * of_real t)" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
608 |
by (metis nz mult_left_cancel mult_zero_left z) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
609 |
then have "sin t' = sin t \<and> cos t' = cos t" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
610 |
apply (simp add: exp_Euler sin_of_real cos_of_real) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
611 |
by (metis Complex_eq complex.sel) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
612 |
then obtain n::int where n: "t' = t + 2 * real n * pi" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
613 |
by (auto simp: sin_cos_eq_iff) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
614 |
then have "n=0" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
615 |
apply (rule_tac z=n in int_cases) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
616 |
using t t' |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
617 |
apply (auto simp: mult_less_0_iff algebra_simps) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
618 |
done |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
619 |
then show "t' = t" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
620 |
by (simp add: n) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
621 |
qed |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
622 |
|
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
623 |
lemma Arg: "0 \<le> Arg z & Arg z < 2*pi & z = of_real(norm z) * exp(ii * of_real(Arg z))" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
624 |
proof (cases "z=0") |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
625 |
case True then show ?thesis |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
626 |
by (simp add: Arg_def) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
627 |
next |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
628 |
case False |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
629 |
obtain t where t: "0 \<le> t" "t < 2*pi" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
630 |
and ReIm: "Re z / cmod z = cos t" "Im z / cmod z = sin t" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
631 |
using sincos_total_2pi [OF complex_unit_circle [OF False]] |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
632 |
by blast |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
633 |
have z: "z = of_real(norm z) * exp(ii * of_real t)" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
634 |
apply (rule complex_eqI) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
635 |
using t False ReIm |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
636 |
apply (auto simp: exp_Euler sin_of_real cos_of_real divide_simps) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
637 |
done |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
638 |
show ?thesis |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
639 |
apply (simp add: Arg_def False) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
640 |
apply (rule theI [where a=t]) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
641 |
using t z False |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
642 |
apply (auto intro: Arg_unique_lemma) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
643 |
done |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
644 |
qed |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
645 |
|
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
646 |
|
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
647 |
corollary |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
648 |
shows Arg_ge_0: "0 \<le> Arg z" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
649 |
and Arg_lt_2pi: "Arg z < 2*pi" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
650 |
and Arg_eq: "z = of_real(norm z) * exp(ii * of_real(Arg z))" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
651 |
using Arg by auto |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
652 |
|
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
653 |
lemma complex_norm_eq_1_exp: "norm z = 1 \<longleftrightarrow> (\<exists>t. z = exp(ii * of_real t))" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
654 |
using Arg [of z] by auto |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
655 |
|
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
656 |
lemma Arg_unique: "\<lbrakk>of_real r * exp(ii * of_real a) = z; 0 < r; 0 \<le> a; a < 2*pi\<rbrakk> \<Longrightarrow> Arg z = a" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
657 |
apply (rule Arg_unique_lemma [OF _ Arg_eq]) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
658 |
using Arg [of z] |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
659 |
apply (auto simp: norm_mult) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
660 |
done |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
661 |
|
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
662 |
lemma Arg_minus: "z \<noteq> 0 \<Longrightarrow> Arg (-z) = (if Arg z < pi then Arg z + pi else Arg z - pi)" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
663 |
apply (rule Arg_unique [of "norm z"]) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
664 |
apply (rule complex_eqI) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
665 |
using Arg_ge_0 [of z] Arg_eq [of z] Arg_lt_2pi [of z] Arg_eq [of z] |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
666 |
apply auto |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
667 |
apply (auto simp: Re_exp Im_exp cos_diff sin_diff cis_conv_exp [symmetric]) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
668 |
apply (metis Re_rcis Im_rcis rcis_def)+ |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
669 |
done |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
670 |
|
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
671 |
lemma Arg_times_of_real [simp]: "0 < r \<Longrightarrow> Arg (of_real r * z) = Arg z" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
672 |
apply (cases "z=0", simp) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
673 |
apply (rule Arg_unique [of "r * norm z"]) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
674 |
using Arg |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
675 |
apply auto |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
676 |
done |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
677 |
|
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
678 |
lemma Arg_times_of_real2 [simp]: "0 < r \<Longrightarrow> Arg (z * of_real r) = Arg z" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
679 |
by (metis Arg_times_of_real mult.commute) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
680 |
|
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
681 |
lemma Arg_divide_of_real [simp]: "0 < r \<Longrightarrow> Arg (z / of_real r) = Arg z" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
682 |
by (metis Arg_times_of_real2 less_numeral_extra(3) nonzero_eq_divide_eq of_real_eq_0_iff) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
683 |
|
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
684 |
lemma Arg_le_pi: "Arg z \<le> pi \<longleftrightarrow> 0 \<le> Im z" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
685 |
proof (cases "z=0") |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
686 |
case True then show ?thesis |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
687 |
by simp |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
688 |
next |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
689 |
case False |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
690 |
have "0 \<le> Im z \<longleftrightarrow> 0 \<le> Im (of_real (cmod z) * exp (\<i> * complex_of_real (Arg z)))" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
691 |
by (metis Arg_eq) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
692 |
also have "... = (0 \<le> Im (exp (\<i> * complex_of_real (Arg z))))" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
693 |
using False |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
694 |
by (simp add: zero_le_mult_iff) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
695 |
also have "... \<longleftrightarrow> Arg z \<le> pi" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
696 |
by (simp add: Im_exp) (metis Arg_ge_0 Arg_lt_2pi sin_lt_zero sin_ge_zero not_le) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
697 |
finally show ?thesis |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
698 |
by blast |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
699 |
qed |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
700 |
|
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
701 |
lemma Arg_lt_pi: "0 < Arg z \<and> Arg z < pi \<longleftrightarrow> 0 < Im z" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
702 |
proof (cases "z=0") |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
703 |
case True then show ?thesis |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
704 |
by simp |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
705 |
next |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
706 |
case False |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
707 |
have "0 < Im z \<longleftrightarrow> 0 < Im (of_real (cmod z) * exp (\<i> * complex_of_real (Arg z)))" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
708 |
by (metis Arg_eq) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
709 |
also have "... = (0 < Im (exp (\<i> * complex_of_real (Arg z))))" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
710 |
using False |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
711 |
by (simp add: zero_less_mult_iff) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
712 |
also have "... \<longleftrightarrow> 0 < Arg z \<and> Arg z < pi" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
713 |
using Arg_ge_0 Arg_lt_2pi sin_le_zero sin_gt_zero |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
714 |
apply (auto simp: Im_exp) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
715 |
using le_less apply fastforce |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
716 |
using not_le by blast |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
717 |
finally show ?thesis |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
718 |
by blast |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
719 |
qed |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
720 |
|
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
721 |
lemma Arg_eq_0: "Arg z = 0 \<longleftrightarrow> z \<in> Reals \<and> 0 \<le> Re z" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
722 |
proof (cases "z=0") |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
723 |
case True then show ?thesis |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
724 |
by simp |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
725 |
next |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
726 |
case False |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
727 |
have "z \<in> Reals \<and> 0 \<le> Re z \<longleftrightarrow> z \<in> Reals \<and> 0 \<le> Re (of_real (cmod z) * exp (\<i> * complex_of_real (Arg z)))" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
728 |
by (metis Arg_eq) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
729 |
also have "... \<longleftrightarrow> z \<in> Reals \<and> 0 \<le> Re (exp (\<i> * complex_of_real (Arg z)))" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
730 |
using False |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
731 |
by (simp add: zero_le_mult_iff) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
732 |
also have "... \<longleftrightarrow> Arg z = 0" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
733 |
apply (auto simp: Re_exp) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
734 |
apply (metis Arg_lt_pi Arg_ge_0 Arg_le_pi cos_pi complex_is_Real_iff leD less_linear less_minus_one_simps(2) minus_minus neg_less_eq_nonneg order_refl) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
735 |
using Arg_eq [of z] |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
736 |
apply (auto simp: Reals_def) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
737 |
done |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
738 |
finally show ?thesis |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
739 |
by blast |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
740 |
qed |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
741 |
|
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
742 |
lemma Arg_of_real: "Arg(of_real x) = 0 \<longleftrightarrow> 0 \<le> x" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
743 |
by (simp add: Arg_eq_0) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
744 |
|
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
745 |
lemma Arg_eq_pi: "Arg z = pi \<longleftrightarrow> z \<in> \<real> \<and> Re z < 0" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
746 |
apply (cases "z=0", simp) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
747 |
using Arg_eq_0 [of "-z"] |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
748 |
apply (auto simp: complex_is_Real_iff Arg_minus) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
749 |
apply (simp add: complex_Re_Im_cancel_iff) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
750 |
apply (metis Arg_minus pi_gt_zero add.left_neutral minus_minus minus_zero) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
751 |
done |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
752 |
|
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
753 |
lemma Arg_eq_0_pi: "Arg z = 0 \<or> Arg z = pi \<longleftrightarrow> z \<in> \<real>" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
754 |
using Arg_eq_0 Arg_eq_pi not_le by auto |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
755 |
|
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
756 |
lemma Arg_inverse: "Arg(inverse z) = (if z \<in> \<real> \<and> 0 \<le> Re z then Arg z else 2*pi - Arg z)" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
757 |
apply (cases "z=0", simp) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
758 |
apply (rule Arg_unique [of "inverse (norm z)"]) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
759 |
using Arg_ge_0 [of z] Arg_lt_2pi [of z] Arg_eq [of z] Arg_eq_0 [of z] Exp_two_pi_i |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
760 |
apply (auto simp: of_real_numeral algebra_simps exp_diff divide_simps) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
761 |
done |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
762 |
|
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
763 |
lemma Arg_eq_iff: |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
764 |
assumes "w \<noteq> 0" "z \<noteq> 0" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
765 |
shows "Arg w = Arg z \<longleftrightarrow> (\<exists>x. 0 < x & w = of_real x * z)" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
766 |
using assms Arg_eq [of z] Arg_eq [of w] |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
767 |
apply auto |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
768 |
apply (rule_tac x="norm w / norm z" in exI) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
769 |
apply (simp add: divide_simps) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
770 |
by (metis mult.commute mult.left_commute) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
771 |
|
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
772 |
lemma Arg_inverse_eq_0: "Arg(inverse z) = 0 \<longleftrightarrow> Arg z = 0" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
773 |
using complex_is_Real_iff |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
774 |
apply (simp add: Arg_eq_0) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
775 |
apply (auto simp: divide_simps not_sum_power2_lt_zero) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
776 |
done |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
777 |
|
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
778 |
lemma Arg_divide: |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
779 |
assumes "w \<noteq> 0" "z \<noteq> 0" "Arg w \<le> Arg z" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
780 |
shows "Arg(z / w) = Arg z - Arg w" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
781 |
apply (rule Arg_unique [of "norm(z / w)"]) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
782 |
using assms Arg_eq [of z] Arg_eq [of w] Arg_ge_0 [of w] Arg_lt_2pi [of z] |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
783 |
apply (auto simp: exp_diff norm_divide algebra_simps divide_simps) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
784 |
done |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
785 |
|
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
786 |
lemma Arg_le_div_sum: |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
787 |
assumes "w \<noteq> 0" "z \<noteq> 0" "Arg w \<le> Arg z" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
788 |
shows "Arg z = Arg w + Arg(z / w)" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
789 |
by (simp add: Arg_divide assms) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
790 |
|
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
791 |
lemma Arg_le_div_sum_eq: |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
792 |
assumes "w \<noteq> 0" "z \<noteq> 0" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
793 |
shows "Arg w \<le> Arg z \<longleftrightarrow> Arg z = Arg w + Arg(z / w)" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
794 |
using assms |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
795 |
by (auto simp: Arg_ge_0 intro: Arg_le_div_sum) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
796 |
|
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
797 |
lemma Arg_diff: |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
798 |
assumes "w \<noteq> 0" "z \<noteq> 0" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
799 |
shows "Arg w - Arg z = (if Arg z \<le> Arg w then Arg(w / z) else Arg(w/z) - 2*pi)" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
800 |
using assms |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
801 |
apply (auto simp: Arg_ge_0 Arg_divide not_le) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
802 |
using Arg_divide [of w z] Arg_inverse [of "w/z"] |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
803 |
apply auto |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
804 |
by (metis Arg_eq_0 less_irrefl minus_diff_eq right_minus_eq) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
805 |
|
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
806 |
lemma Arg_add: |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
807 |
assumes "w \<noteq> 0" "z \<noteq> 0" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
808 |
shows "Arg w + Arg z = (if Arg w + Arg z < 2*pi then Arg(w * z) else Arg(w * z) + 2*pi)" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
809 |
using assms |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
810 |
using Arg_diff [of "w*z" z] Arg_le_div_sum_eq [of z "w*z"] |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
811 |
apply (auto simp: Arg_ge_0 Arg_divide not_le) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
812 |
apply (metis Arg_lt_2pi add.commute) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
813 |
apply (metis (no_types) Arg add.commute diff_0 diff_add_cancel diff_less_eq diff_minus_eq_add not_less) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
814 |
done |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
815 |
|
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
816 |
lemma Arg_times: |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
817 |
assumes "w \<noteq> 0" "z \<noteq> 0" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
818 |
shows "Arg (w * z) = (if Arg w + Arg z < 2*pi then Arg w + Arg z |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
819 |
else (Arg w + Arg z) - 2*pi)" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
820 |
using Arg_add [OF assms] |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
821 |
by auto |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
822 |
|
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
823 |
lemma Arg_cnj: "Arg(cnj z) = (if z \<in> \<real> \<and> 0 \<le> Re z then Arg z else 2*pi - Arg z)" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
824 |
apply (cases "z=0", simp) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
825 |
apply (rule trans [of _ "Arg(inverse z)"]) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
826 |
apply (simp add: Arg_eq_iff divide_simps complex_norm_square [symmetric] mult.commute) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
827 |
apply (metis norm_eq_zero of_real_power zero_less_power2) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
828 |
apply (auto simp: of_real_numeral Arg_inverse) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
829 |
done |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
830 |
|
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
831 |
lemma Arg_real: "z \<in> \<real> \<Longrightarrow> Arg z = (if 0 \<le> Re z then 0 else pi)" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
832 |
using Arg_eq_0 Arg_eq_0_pi |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
833 |
by auto |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
834 |
|
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
835 |
lemma Arg_exp: "0 \<le> Im z \<Longrightarrow> Im z < 2*pi \<Longrightarrow> Arg(exp z) = Im z" |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
836 |
by (rule Arg_unique [of "exp(Re z)"]) (auto simp: Exp_eq_polar) |
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59745
diff
changeset
|
837 |
|
59751
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
838 |
|
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
839 |
subsection{*Analytic properties of tangent function*} |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
840 |
|
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
841 |
lemma cnj_tan: "cnj(tan z) = tan(cnj z)" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
842 |
by (simp add: cnj_cos cnj_sin tan_def) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
843 |
|
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
844 |
lemma complex_differentiable_at_tan: "~(cos z = 0) \<Longrightarrow> tan complex_differentiable at z" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
845 |
unfolding complex_differentiable_def |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
846 |
using DERIV_tan by blast |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
847 |
|
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
848 |
lemma complex_differentiable_within_tan: "~(cos z = 0) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
849 |
\<Longrightarrow> tan complex_differentiable (at z within s)" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
850 |
using complex_differentiable_at_tan complex_differentiable_at_within by blast |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
851 |
|
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
852 |
lemma continuous_within_tan: "~(cos z = 0) \<Longrightarrow> continuous (at z within s) tan" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
853 |
using continuous_at_imp_continuous_within isCont_tan by blast |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
854 |
|
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
855 |
lemma continuous_on_tan [continuous_intros]: "(\<And>z. z \<in> s \<Longrightarrow> ~(cos z = 0)) \<Longrightarrow> continuous_on s tan" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
856 |
by (simp add: continuous_at_imp_continuous_on) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
857 |
|
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
858 |
lemma holomorphic_on_tan: "(\<And>z. z \<in> s \<Longrightarrow> ~(cos z = 0)) \<Longrightarrow> tan holomorphic_on s" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
859 |
by (simp add: complex_differentiable_within_tan holomorphic_on_def) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
860 |
|
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
861 |
|
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
862 |
subsection{*Complex logarithms (the conventional principal value)*} |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
863 |
|
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
864 |
definition Ln where |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
865 |
"Ln \<equiv> \<lambda>z. THE w. exp w = z & -pi < Im(w) & Im(w) \<le> pi" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
866 |
|
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
867 |
lemma |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
868 |
assumes "z \<noteq> 0" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
869 |
shows exp_Ln [simp]: "exp(Ln z) = z" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
870 |
and mpi_less_Im_Ln: "-pi < Im(Ln z)" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
871 |
and Im_Ln_le_pi: "Im(Ln z) \<le> pi" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
872 |
proof - |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
873 |
obtain \<psi> where z: "z / (cmod z) = Complex (cos \<psi>) (sin \<psi>)" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
874 |
using complex_unimodular_polar [of "z / (norm z)"] assms |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
875 |
by (auto simp: norm_divide divide_simps) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
876 |
obtain \<phi> where \<phi>: "- pi < \<phi>" "\<phi> \<le> pi" "sin \<phi> = sin \<psi>" "cos \<phi> = cos \<psi>" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
877 |
using sincos_principal_value [of "\<psi>"] assms |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
878 |
by (auto simp: norm_divide divide_simps) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
879 |
have "exp(Ln z) = z & -pi < Im(Ln z) & Im(Ln z) \<le> pi" unfolding Ln_def |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
880 |
apply (rule theI [where a = "Complex (ln(norm z)) \<phi>"]) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
881 |
using z assms \<phi> |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
882 |
apply (auto simp: field_simps exp_complex_eqI Exp_eq_polar cis.code) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
883 |
done |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
884 |
then show "exp(Ln z) = z" "-pi < Im(Ln z)" "Im(Ln z) \<le> pi" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
885 |
by auto |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
886 |
qed |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
887 |
|
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
888 |
lemma Ln_exp [simp]: |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
889 |
assumes "-pi < Im(z)" "Im(z) \<le> pi" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
890 |
shows "Ln(exp z) = z" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
891 |
apply (rule exp_complex_eqI) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
892 |
using assms mpi_less_Im_Ln [of "exp z"] Im_Ln_le_pi [of "exp z"] |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
893 |
apply auto |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
894 |
done |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
895 |
|
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
896 |
lemma Ln_eq_iff: "w \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> (Ln w = Ln z \<longleftrightarrow> w = z)" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
897 |
by (metis exp_Ln) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
898 |
|
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
899 |
lemma Ln_unique: "exp(z) = w \<Longrightarrow> -pi < Im(z) \<Longrightarrow> Im(z) \<le> pi \<Longrightarrow> Ln w = z" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
900 |
using Ln_exp by blast |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
901 |
|
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
902 |
lemma Re_Ln [simp]: "z \<noteq> 0 \<Longrightarrow> Re(Ln z) = ln(norm z)" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
903 |
by (metis exp_Ln assms ln_exp norm_exp_eq_Re) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
904 |
|
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
905 |
lemma exists_complex_root: |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
906 |
fixes a :: complex |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
907 |
shows "n \<noteq> 0 \<Longrightarrow> \<exists>z. z ^ n = a" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
908 |
apply (cases "a=0", simp) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
909 |
apply (rule_tac x= "exp(Ln(a) / n)" in exI) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
910 |
apply (auto simp: exp_of_nat_mult [symmetric]) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
911 |
done |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
912 |
|
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
913 |
subsection{*Derivative of Ln away from the branch cut*} |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
914 |
|
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
915 |
lemma |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
916 |
assumes "Im(z) = 0 \<Longrightarrow> 0 < Re(z)" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
917 |
shows has_field_derivative_Ln: "(Ln has_field_derivative inverse(z)) (at z)" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
918 |
and Im_Ln_less_pi: "Im (Ln z) < pi" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
919 |
proof - |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
920 |
have znz: "z \<noteq> 0" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
921 |
using assms by auto |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
922 |
then show *: "Im (Ln z) < pi" using assms |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
923 |
by (metis exp_Ln Im_Ln_le_pi Im_exp Re_exp abs_of_nonneg cmod_eq_Re cos_pi mult.right_neutral mult_minus_right mult_zero_right neg_less_0_iff_less norm_exp_eq_Re not_less not_less_iff_gr_or_eq sin_pi) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
924 |
show "(Ln has_field_derivative inverse(z)) (at z)" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
925 |
apply (rule has_complex_derivative_inverse_strong_x |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
926 |
[where f = exp and s = "{w. -pi < Im(w) & Im(w) < pi}"]) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
927 |
using znz * |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
928 |
apply (auto simp: continuous_on_exp open_Collect_conj open_halfspace_Im_gt open_halfspace_Im_lt) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
929 |
apply (metis DERIV_exp exp_Ln) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
930 |
apply (metis mpi_less_Im_Ln) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
931 |
done |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
932 |
qed |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
933 |
|
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
934 |
declare has_field_derivative_Ln [derivative_intros] |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
935 |
declare has_field_derivative_Ln [THEN DERIV_chain2, derivative_intros] |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
936 |
|
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
937 |
lemma complex_differentiable_at_Ln: "(Im(z) = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> Ln complex_differentiable at z" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
938 |
using complex_differentiable_def has_field_derivative_Ln by blast |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
939 |
|
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
940 |
lemma complex_differentiable_within_Ln: "(Im(z) = 0 \<Longrightarrow> 0 < Re(z)) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
941 |
\<Longrightarrow> Ln complex_differentiable (at z within s)" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
942 |
using complex_differentiable_at_Ln complex_differentiable_within_subset by blast |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
943 |
|
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
944 |
lemma continuous_at_Ln: "(Im(z) = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> continuous (at z) Ln" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
945 |
by (simp add: complex_differentiable_imp_continuous_at complex_differentiable_within_Ln) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
946 |
|
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
947 |
lemma continuous_within_Ln: "(Im(z) = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> continuous (at z within s) Ln" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
948 |
using continuous_at_Ln continuous_at_imp_continuous_within by blast |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
949 |
|
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
950 |
lemma continuous_on_Ln [continuous_intros]: "(\<And>z. z \<in> s \<Longrightarrow> Im(z) = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> continuous_on s Ln" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
951 |
by (simp add: continuous_at_imp_continuous_on continuous_within_Ln) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
952 |
|
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
953 |
lemma holomorphic_on_Ln: "(\<And>z. z \<in> s \<Longrightarrow> Im(z) = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> Ln holomorphic_on s" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
954 |
by (simp add: complex_differentiable_within_Ln holomorphic_on_def) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
955 |
|
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
956 |
|
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
957 |
subsection{*Relation to Real Logarithm*} |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
958 |
|
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
959 |
lemma ln_of_real: |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
960 |
assumes "0 < z" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
961 |
shows "Ln(of_real z) = of_real(ln z)" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
962 |
proof - |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
963 |
have "Ln(of_real (exp (ln z))) = Ln (exp (of_real (ln z)))" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
964 |
by (simp add: exp_of_real) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
965 |
also have "... = of_real(ln z)" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
966 |
using assms |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
967 |
by (subst Ln_exp) auto |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
968 |
finally show ?thesis |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
969 |
using assms by simp |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
970 |
qed |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
971 |
|
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
972 |
|
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
973 |
subsection{*Quadrant-type results for Ln*} |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
974 |
|
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
975 |
lemma cos_lt_zero_pi: "pi/2 < x \<Longrightarrow> x < 3*pi/2 \<Longrightarrow> cos x < 0" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
976 |
using cos_minus_pi cos_gt_zero_pi [of "x-pi"] |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
977 |
by simp |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
978 |
|
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
979 |
lemma Re_Ln_pos_lt: |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
980 |
assumes "z \<noteq> 0" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
981 |
shows "abs(Im(Ln z)) < pi/2 \<longleftrightarrow> 0 < Re(z)" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
982 |
proof - |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
983 |
{ fix w |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
984 |
assume "w = Ln z" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
985 |
then have w: "Im w \<le> pi" "- pi < Im w" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
986 |
using Im_Ln_le_pi [of z] mpi_less_Im_Ln [of z] assms |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
987 |
by auto |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
988 |
then have "abs(Im w) < pi/2 \<longleftrightarrow> 0 < Re(exp w)" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
989 |
apply (auto simp: Re_exp zero_less_mult_iff cos_gt_zero_pi) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
990 |
using cos_lt_zero_pi [of "-(Im w)"] cos_lt_zero_pi [of "(Im w)"] |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
991 |
apply (simp add: abs_if split: split_if_asm) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
992 |
apply (metis (no_types) cos_minus cos_pi_half eq_divide_eq_numeral1(1) eq_numeral_simps(4) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
993 |
less_numeral_extra(3) linorder_neqE_linordered_idom minus_mult_minus minus_mult_right |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
994 |
mult_numeral_1_right) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
995 |
done |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
996 |
} |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
997 |
then show ?thesis using assms |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
998 |
by auto |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
999 |
qed |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1000 |
|
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1001 |
lemma Re_Ln_pos_le: |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1002 |
assumes "z \<noteq> 0" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1003 |
shows "abs(Im(Ln z)) \<le> pi/2 \<longleftrightarrow> 0 \<le> Re(z)" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1004 |
proof - |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1005 |
{ fix w |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1006 |
assume "w = Ln z" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1007 |
then have w: "Im w \<le> pi" "- pi < Im w" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1008 |
using Im_Ln_le_pi [of z] mpi_less_Im_Ln [of z] assms |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1009 |
by auto |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1010 |
then have "abs(Im w) \<le> pi/2 \<longleftrightarrow> 0 \<le> Re(exp w)" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1011 |
apply (auto simp: Re_exp zero_le_mult_iff cos_ge_zero) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1012 |
using cos_lt_zero_pi [of "- (Im w)"] cos_lt_zero_pi [of "(Im w)"] not_le |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1013 |
apply (auto simp: abs_if split: split_if_asm) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1014 |
done |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1015 |
} |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1016 |
then show ?thesis using assms |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1017 |
by auto |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1018 |
qed |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1019 |
|
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1020 |
lemma Im_Ln_pos_lt: |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1021 |
assumes "z \<noteq> 0" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1022 |
shows "0 < Im(Ln z) \<and> Im(Ln z) < pi \<longleftrightarrow> 0 < Im(z)" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1023 |
proof - |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1024 |
{ fix w |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1025 |
assume "w = Ln z" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1026 |
then have w: "Im w \<le> pi" "- pi < Im w" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1027 |
using Im_Ln_le_pi [of z] mpi_less_Im_Ln [of z] assms |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1028 |
by auto |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1029 |
then have "0 < Im w \<and> Im w < pi \<longleftrightarrow> 0 < Im(exp w)" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1030 |
using sin_gt_zero [of "- (Im w)"] sin_gt_zero [of "(Im w)"] |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1031 |
apply (auto simp: Im_exp zero_less_mult_iff) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1032 |
using less_linear apply fastforce |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1033 |
using less_linear apply fastforce |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1034 |
done |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1035 |
} |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1036 |
then show ?thesis using assms |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1037 |
by auto |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1038 |
qed |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1039 |
|
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1040 |
lemma Im_Ln_pos_le: |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1041 |
assumes "z \<noteq> 0" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1042 |
shows "0 \<le> Im(Ln z) \<and> Im(Ln z) \<le> pi \<longleftrightarrow> 0 \<le> Im(z)" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1043 |
proof - |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1044 |
{ fix w |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1045 |
assume "w = Ln z" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1046 |
then have w: "Im w \<le> pi" "- pi < Im w" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1047 |
using Im_Ln_le_pi [of z] mpi_less_Im_Ln [of z] assms |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1048 |
by auto |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1049 |
then have "0 \<le> Im w \<and> Im w \<le> pi \<longleftrightarrow> 0 \<le> Im(exp w)" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1050 |
using sin_ge_zero [of "- (Im w)"] sin_ge_zero [of "(Im w)"] |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1051 |
apply (auto simp: Im_exp zero_le_mult_iff sin_ge_zero) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1052 |
apply (metis not_le not_less_iff_gr_or_eq pi_not_less_zero sin_eq_0_pi) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1053 |
done } |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1054 |
then show ?thesis using assms |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1055 |
by auto |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1056 |
qed |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1057 |
|
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1058 |
lemma Re_Ln_pos_lt_imp: "0 < Re(z) \<Longrightarrow> abs(Im(Ln z)) < pi/2" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1059 |
by (metis Re_Ln_pos_lt less_irrefl zero_complex.simps(1)) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1060 |
|
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1061 |
lemma Im_Ln_pos_lt_imp: "0 < Im(z) \<Longrightarrow> 0 < Im(Ln z) \<and> Im(Ln z) < pi" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1062 |
by (metis Im_Ln_pos_lt not_le order_refl zero_complex.simps(2)) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1063 |
|
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1064 |
lemma Im_Ln_eq_0: "z \<noteq> 0 \<Longrightarrow> (Im(Ln z) = 0 \<longleftrightarrow> 0 < Re(z) \<and> Im(z) = 0)" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1065 |
by (metis exp_Ln Im_Ln_less_pi Im_Ln_pos_le Im_Ln_pos_lt Re_complex_of_real add.commute add.left_neutral |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1066 |
complex_eq exp_of_real le_less mult_zero_right norm_exp_eq_Re norm_le_zero_iff not_le of_real_0) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1067 |
|
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1068 |
lemma Im_Ln_eq_pi: "z \<noteq> 0 \<Longrightarrow> (Im(Ln z) = pi \<longleftrightarrow> Re(z) < 0 \<and> Im(z) = 0)" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1069 |
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) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1070 |
|
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1071 |
|
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1072 |
subsection{*More Properties of Ln*} |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1073 |
|
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1074 |
lemma cnj_Ln: "(Im z = 0 \<Longrightarrow> 0 < Re z) \<Longrightarrow> cnj(Ln z) = Ln(cnj z)" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1075 |
apply (cases "z=0", auto) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1076 |
apply (rule exp_complex_eqI) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1077 |
apply (auto simp: abs_if split: split_if_asm) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1078 |
apply (metis Im_Ln_less_pi add_mono_thms_linordered_field(5) cnj.simps(1) cnj.simps(2) mult_2 neg_equal_0_iff_equal) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1079 |
apply (metis add_mono_thms_linordered_field(5) complex_cnj_zero_iff diff_0_right diff_minus_eq_add minus_diff_eq mpi_less_Im_Ln mult.commute mult_2_right neg_less_iff_less) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1080 |
by (metis exp_Ln exp_cnj) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1081 |
|
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1082 |
lemma Ln_inverse: "(Im(z) = 0 \<Longrightarrow> 0 < Re z) \<Longrightarrow> Ln(inverse z) = -(Ln z)" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1083 |
apply (cases "z=0", auto) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1084 |
apply (rule exp_complex_eqI) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1085 |
using mpi_less_Im_Ln [of z] mpi_less_Im_Ln [of "inverse z"] |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1086 |
apply (auto simp: abs_if exp_minus split: split_if_asm) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1087 |
apply (metis Im_Ln_less_pi Im_Ln_pos_le add_less_cancel_left add_strict_mono |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1088 |
inverse_inverse_eq inverse_zero le_less mult.commute mult_2_right) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1089 |
done |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1090 |
|
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1091 |
lemma Ln_1 [simp]: "Ln(1) = 0" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1092 |
proof - |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1093 |
have "Ln (exp 0) = 0" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1094 |
by (metis exp_zero ln_exp ln_of_real of_real_0 of_real_1 zero_less_one) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1095 |
then show ?thesis |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1096 |
by simp |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1097 |
qed |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1098 |
|
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1099 |
lemma Ln_minus1 [simp]: "Ln(-1) = ii * pi" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1100 |
apply (rule exp_complex_eqI) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1101 |
using Im_Ln_le_pi [of "-1"] mpi_less_Im_Ln [of "-1"] cis_conv_exp cis_pi |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1102 |
apply (auto simp: abs_if) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1103 |
done |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1104 |
|
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1105 |
lemma Ln_ii [simp]: "Ln ii = ii * of_real pi/2" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1106 |
using Ln_exp [of "ii * (of_real pi/2)"] |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1107 |
unfolding exp_Euler |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1108 |
by simp |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1109 |
|
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1110 |
lemma Ln_minus_ii [simp]: "Ln(-ii) = - (ii * pi/2)" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1111 |
proof - |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1112 |
have "Ln(-ii) = Ln(1/ii)" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1113 |
by simp |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1114 |
also have "... = - (Ln ii)" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1115 |
by (metis Ln_inverse ii.sel(2) inverse_eq_divide zero_neq_one) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1116 |
also have "... = - (ii * pi/2)" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1117 |
by (simp add: Ln_ii) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1118 |
finally show ?thesis . |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1119 |
qed |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1120 |
|
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1121 |
lemma Ln_times: |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1122 |
assumes "w \<noteq> 0" "z \<noteq> 0" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1123 |
shows "Ln(w * z) = |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1124 |
(if Im(Ln w + Ln z) \<le> -pi then |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1125 |
(Ln(w) + Ln(z)) + ii * of_real(2*pi) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1126 |
else if Im(Ln w + Ln z) > pi then |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1127 |
(Ln(w) + Ln(z)) - ii * of_real(2*pi) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1128 |
else Ln(w) + Ln(z))" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1129 |
using pi_ge_zero Im_Ln_le_pi [of w] Im_Ln_le_pi [of z] |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1130 |
using assms mpi_less_Im_Ln [of w] mpi_less_Im_Ln [of z] |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1131 |
by (auto simp: of_real_numeral exp_add exp_diff sin_double cos_double exp_Euler intro!: Ln_unique) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1132 |
|
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1133 |
lemma Ln_times_simple: |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1134 |
"\<lbrakk>w \<noteq> 0; z \<noteq> 0; -pi < Im(Ln w) + Im(Ln z); Im(Ln w) + Im(Ln z) \<le> pi\<rbrakk> |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1135 |
\<Longrightarrow> Ln(w * z) = Ln(w) + Ln(z)" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1136 |
by (simp add: Ln_times) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1137 |
|
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1138 |
lemma Ln_minus: |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1139 |
assumes "z \<noteq> 0" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1140 |
shows "Ln(-z) = (if Im(z) \<le> 0 \<and> ~(Re(z) < 0 \<and> Im(z) = 0) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1141 |
then Ln(z) + ii * pi |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1142 |
else Ln(z) - ii * pi)" (is "_ = ?rhs") |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1143 |
using Im_Ln_le_pi [of z] mpi_less_Im_Ln [of z] assms |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1144 |
Im_Ln_eq_pi [of z] Im_Ln_pos_lt [of z] |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1145 |
by (auto simp: of_real_numeral exp_add exp_diff exp_Euler intro!: Ln_unique) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1146 |
|
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1147 |
lemma Ln_inverse_if: |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1148 |
assumes "z \<noteq> 0" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1149 |
shows "Ln (inverse z) = |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1150 |
(if (Im(z) = 0 \<longrightarrow> 0 < Re z) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1151 |
then -(Ln z) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1152 |
else -(Ln z) + \<i> * 2 * complex_of_real pi)" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1153 |
proof (cases "(Im(z) = 0 \<longrightarrow> 0 < Re z)") |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1154 |
case True then show ?thesis |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1155 |
by (simp add: Ln_inverse) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1156 |
next |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1157 |
case False |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1158 |
then have z: "Im z = 0" "Re z < 0" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1159 |
using assms |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1160 |
apply auto |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1161 |
by (metis cnj.code complex_cnj_cnj not_less_iff_gr_or_eq zero_complex.simps(1) zero_complex.simps(2)) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1162 |
have "Ln(inverse z) = Ln(- (inverse (-z)))" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1163 |
by simp |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1164 |
also have "... = Ln (inverse (-z)) + \<i> * complex_of_real pi" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1165 |
using assms z |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1166 |
apply (simp add: Ln_minus) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1167 |
apply (simp add: field_simps) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1168 |
done |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1169 |
also have "... = - Ln (- z) + \<i> * complex_of_real pi" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1170 |
apply (subst Ln_inverse) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1171 |
using z assms by auto |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1172 |
also have "... = - (Ln z) + \<i> * 2 * complex_of_real pi" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1173 |
apply (subst Ln_minus [OF assms]) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1174 |
using assms z |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1175 |
apply simp |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1176 |
done |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1177 |
finally show ?thesis |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1178 |
using assms z |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1179 |
by simp |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1180 |
qed |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1181 |
|
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1182 |
lemma Ln_times_ii: |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1183 |
assumes "z \<noteq> 0" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1184 |
shows "Ln(ii * z) = (if 0 \<le> Re(z) | Im(z) < 0 |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1185 |
then Ln(z) + ii * of_real pi/2 |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1186 |
else Ln(z) - ii * of_real(3 * pi/2))" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1187 |
using Im_Ln_le_pi [of z] mpi_less_Im_Ln [of z] assms |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1188 |
Im_Ln_eq_pi [of z] Im_Ln_pos_lt [of z] Re_Ln_pos_le [of z] |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1189 |
by (auto simp: of_real_numeral Ln_times) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1190 |
|
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1191 |
|
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1192 |
subsection{*Relation between Square Root and exp/ln, hence its derivative*} |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1193 |
|
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1194 |
lemma csqrt_exp_Ln: |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1195 |
assumes "z \<noteq> 0" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1196 |
shows "csqrt z = exp(Ln(z) / 2)" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1197 |
proof - |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1198 |
have "(exp (Ln z / 2))\<^sup>2 = (exp (Ln z))" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1199 |
by (metis exp_double nonzero_mult_divide_cancel_left times_divide_eq_right zero_neq_numeral) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1200 |
also have "... = z" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1201 |
using assms exp_Ln by blast |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1202 |
finally have "csqrt z = csqrt ((exp (Ln z / 2))\<^sup>2)" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1203 |
by simp |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1204 |
also have "... = exp (Ln z / 2)" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1205 |
apply (subst csqrt_square) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1206 |
using cos_gt_zero_pi [of "(Im (Ln z) / 2)"] Im_Ln_le_pi mpi_less_Im_Ln assms |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1207 |
apply (auto simp: Re_exp Im_exp zero_less_mult_iff zero_le_mult_iff, fastforce+) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1208 |
done |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1209 |
finally show ?thesis using assms csqrt_square |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1210 |
by simp |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1211 |
qed |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1212 |
|
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1213 |
lemma csqrt_inverse: |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1214 |
assumes "Im(z) = 0 \<Longrightarrow> 0 < Re z" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1215 |
shows "csqrt (inverse z) = inverse (csqrt z)" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1216 |
proof (cases "z=0", simp) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1217 |
assume "z \<noteq> 0 " |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1218 |
then show ?thesis |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1219 |
using assms |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1220 |
by (simp add: csqrt_exp_Ln Ln_inverse exp_minus) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1221 |
qed |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1222 |
|
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1223 |
lemma cnj_csqrt: |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1224 |
assumes "Im z = 0 \<Longrightarrow> 0 \<le> Re(z)" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1225 |
shows "cnj(csqrt z) = csqrt(cnj z)" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1226 |
proof (cases "z=0", simp) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1227 |
assume z: "z \<noteq> 0" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1228 |
then have "Im z = 0 \<Longrightarrow> 0 < Re(z)" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1229 |
using assms cnj.code complex_cnj_zero_iff by fastforce |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1230 |
then show ?thesis |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1231 |
using z by (simp add: csqrt_exp_Ln cnj_Ln exp_cnj) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1232 |
qed |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1233 |
|
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1234 |
lemma has_field_derivative_csqrt: |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1235 |
assumes "Im z = 0 \<Longrightarrow> 0 < Re(z)" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1236 |
shows "(csqrt has_field_derivative inverse(2 * csqrt z)) (at z)" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1237 |
proof - |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1238 |
have z: "z \<noteq> 0" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1239 |
using assms by auto |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1240 |
then have *: "inverse z = inverse (2*z) * 2" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1241 |
by (simp add: divide_simps) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1242 |
show ?thesis |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1243 |
apply (rule DERIV_transform_at [where f = "\<lambda>z. exp(Ln(z) / 2)" and d = "norm z"]) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1244 |
apply (intro derivative_eq_intros | simp add: assms)+ |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1245 |
apply (rule *) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1246 |
using z |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1247 |
apply (auto simp: field_simps csqrt_exp_Ln [symmetric]) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1248 |
apply (metis power2_csqrt power2_eq_square) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1249 |
apply (metis csqrt_exp_Ln dist_0_norm less_irrefl) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1250 |
done |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1251 |
qed |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1252 |
|
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1253 |
lemma complex_differentiable_at_csqrt: |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1254 |
"(Im z = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> csqrt complex_differentiable at z" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1255 |
using complex_differentiable_def has_field_derivative_csqrt by blast |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1256 |
|
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1257 |
lemma complex_differentiable_within_csqrt: |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1258 |
"(Im z = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> csqrt complex_differentiable (at z within s)" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1259 |
using complex_differentiable_at_csqrt complex_differentiable_within_subset by blast |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1260 |
|
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1261 |
lemma continuous_at_csqrt: |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1262 |
"(Im z = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> continuous (at z) csqrt" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1263 |
by (simp add: complex_differentiable_within_csqrt complex_differentiable_imp_continuous_at) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1264 |
|
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1265 |
lemma continuous_within_csqrt: |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1266 |
"(Im z = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> continuous (at z within s) csqrt" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1267 |
by (simp add: complex_differentiable_imp_continuous_at complex_differentiable_within_csqrt) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1268 |
|
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1269 |
lemma continuous_on_csqrt [continuous_intros]: |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1270 |
"(\<And>z. z \<in> s \<and> Im z = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> continuous_on s csqrt" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1271 |
by (simp add: continuous_at_imp_continuous_on continuous_within_csqrt) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1272 |
|
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1273 |
lemma holomorphic_on_csqrt: |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1274 |
"(\<And>z. z \<in> s \<and> Im z = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> csqrt holomorphic_on s" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1275 |
by (simp add: complex_differentiable_within_csqrt holomorphic_on_def) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1276 |
|
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1277 |
lemma continuous_within_closed_nontrivial: |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1278 |
"closed s \<Longrightarrow> a \<notin> s ==> continuous (at a within s) f" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1279 |
using open_Compl |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1280 |
by (force simp add: continuous_def eventually_at_topological filterlim_iff open_Collect_neg) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1281 |
|
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1282 |
lemma closed_Real_halfspace_Re_ge: "closed (\<real> \<inter> {w. x \<le> Re(w)})" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1283 |
using closed_halfspace_Re_ge |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1284 |
by (simp add: closed_Int closed_complex_Reals) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1285 |
|
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1286 |
lemma continuous_within_csqrt_posreal: |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1287 |
"continuous (at z within (\<real> \<inter> {w. 0 \<le> Re(w)})) csqrt" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1288 |
proof (cases "Im z = 0 --> 0 < Re(z)") |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1289 |
case True then show ?thesis |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1290 |
by (blast intro: continuous_within_csqrt) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1291 |
next |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1292 |
case False |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1293 |
then have "Im z = 0" "Re z < 0 \<or> z = 0" |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1294 |
using False cnj.code complex_cnj_zero_iff by auto force |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1295 |
then show ?thesis |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1296 |
apply (auto simp: continuous_within_closed_nontrivial [OF closed_Real_halfspace_Re_ge]) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1297 |
apply (auto simp: continuous_within_eps_delta norm_conv_dist [symmetric]) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1298 |
apply (rule_tac x="e^2" in exI) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1299 |
apply (auto simp: Reals_def) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1300 |
by (metis linear not_less real_sqrt_less_iff real_sqrt_pow2_iff real_sqrt_power) |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1301 |
qed |
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1302 |
|
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset
|
1303 |
|
59745
390476a0ef13
new file for complex transcendental functions
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1304 |
end |