--- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy Thu Apr 09 20:42:38 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy Sat Apr 11 11:56:40 2015 +0100
@@ -8,7 +8,6 @@
imports "~~/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics"
begin
-
lemma cmod_add_real_less:
assumes "Im z \<noteq> 0" "r\<noteq>0"
shows "cmod (z + r) < cmod z + abs r"
@@ -613,6 +612,14 @@
apply (simp only: pos_le_divide_eq [symmetric], linarith)
done
+lemma e_less_3: "exp 1 < (3::real)"
+ using e_approx_32
+ by (simp add: abs_if split: split_if_asm)
+
+lemma ln3_gt_1: "ln 3 > (1::real)"
+ by (metis e_less_3 exp_less_cancel_iff exp_ln_iff less_trans ln_exp)
+
+
subsection{*The argument of a complex number*}
definition Arg :: "complex \<Rightarrow> real" where
@@ -892,8 +899,9 @@
subsection{*Complex logarithms (the conventional principal value)*}
-definition Ln where
- "Ln \<equiv> \<lambda>z. THE w. exp w = z & -pi < Im(w) & Im(w) \<le> pi"
+definition Ln :: "complex \<Rightarrow> complex"
+ where "Ln \<equiv> \<lambda>z. THE w. exp w = z & -pi < Im(w) & Im(w) \<le> pi"
+
lemma
assumes "z \<noteq> 0"
@@ -941,6 +949,7 @@
apply (auto simp: exp_of_nat_mult [symmetric])
done
+
subsection{*The Unwinding Number and the Ln-product Formula*}
text{*Note that in this special case the unwinding number is -1, 0 or 1.*}
@@ -1128,8 +1137,8 @@
apply (cases "z=0", auto)
apply (rule exp_complex_eqI)
apply (auto simp: abs_if split: split_if_asm)
- 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)
- 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)
+ apply (metis Im_Ln_less_pi add_mono_thms_linordered_field(5) cnj.simps mult_2 neg_equal_0_iff_equal)
+ apply (metis complex_cnj_zero_iff diff_minus_eq_add diff_strict_mono minus_less_iff mpi_less_Im_Ln mult.commute mult_2_right)
by (metis exp_Ln exp_cnj)
lemma Ln_inverse: "(Im(z) = 0 \<Longrightarrow> 0 < Re z) \<Longrightarrow> Ln(inverse z) = -(Ln z)"
@@ -1141,7 +1150,7 @@
inverse_inverse_eq inverse_zero le_less mult.commute mult_2_right)
done
-lemma Ln_1 [simp]: "Ln(1) = 0"
+lemma Ln_1 [simp]: "Ln 1 = 0"
proof -
have "Ln (exp 0) = 0"
by (metis exp_zero ln_exp Ln_of_real of_real_0 of_real_1 zero_less_one)
@@ -1149,6 +1158,18 @@
by simp
qed
+instantiation complex :: ln
+begin
+
+definition ln_complex :: "complex \<Rightarrow> complex"
+ where "ln_complex \<equiv> Ln"
+
+instance
+ by intro_classes (simp add: ln_complex_def)
+
+end
+
+
lemma Ln_minus1 [simp]: "Ln(-1) = ii * pi"
apply (rule exp_complex_eqI)
using Im_Ln_le_pi [of "-1"] mpi_less_Im_Ln [of "-1"] cis_conv_exp cis_pi
@@ -1242,6 +1263,93 @@
by (auto simp: of_real_numeral Ln_times)
+
+subsection{*Complex Powers*}
+
+lemma powr_0 [simp]: "0 powr z = 0"
+ by (simp add: powr_def)
+
+lemma powr_to_1 [simp]: "z powr 1 = (z::complex)"
+ by (simp add: powr_def ln_complex_def)
+
+lemma powr_nat:
+ fixes n::nat and z::complex shows "z powr n = (if z = 0 then 0 else z^n)"
+ by (simp add: exp_of_nat_mult powr_def ln_complex_def)
+
+lemma powr_add:
+ fixes w::complex shows "w powr (z1 + z2) = w powr z1 * w powr z2"
+ by (simp add: powr_def algebra_simps exp_add)
+
+lemma powr_minus:
+ fixes w::complex shows "w powr (-z) = inverse(w powr z)"
+ by (simp add: powr_def exp_minus)
+
+lemma powr_diff:
+ fixes w::complex shows "w powr (z1 - z2) = w powr z1 / w powr z2"
+ by (simp add: powr_def algebra_simps exp_diff)
+
+lemma norm_powr_real: "w \<in> \<real> \<Longrightarrow> 0 < Re w \<Longrightarrow> norm(w powr z) = exp(Re z * ln(Re w))"
+ apply (simp add: powr_def ln_complex_def)
+ using Im_Ln_eq_0 complex_is_Real_iff norm_complex_def
+ by auto
+
+lemma powr_real_real:
+ "\<lbrakk>w \<in> \<real>; z \<in> \<real>; 0 < Re w\<rbrakk> \<Longrightarrow> w powr z = exp(Re z * ln(Re w))"
+ apply (simp add: powr_def ln_complex_def)
+ by (metis complex_eq complex_is_Real_iff diff_0 diff_0_right diff_minus_eq_add exp_ln exp_not_eq_zero
+ exp_of_real Ln_of_real mult_zero_right of_real_0 of_real_mult)
+
+lemma powr_of_real:
+ fixes x::real
+ shows "0 < x \<Longrightarrow> x powr y = x powr y"
+ by (simp add: powr_def powr_real_real)
+
+lemma norm_powr_real_mono:
+ "w \<in> \<real> \<Longrightarrow> 1 < Re w
+ \<Longrightarrow> norm(w powr z1) \<le> norm(w powr z2) \<longleftrightarrow> Re z1 \<le> Re z2"
+ by (auto simp: powr_def ln_complex_def algebra_simps Reals_def Ln_of_real)
+
+lemma powr_times_real:
+ "\<lbrakk>x \<in> \<real>; y \<in> \<real>; 0 \<le> Re x; 0 \<le> Re y\<rbrakk>
+ \<Longrightarrow> (x * y) powr z = x powr z * y powr z"
+ by (auto simp: Reals_def powr_def ln_complex_def Ln_times exp_add algebra_simps less_eq_real_def Ln_of_real)
+
+lemma has_field_derivative_powr:
+ "(Im z = 0 \<Longrightarrow> 0 < Re z)
+ \<Longrightarrow> ((\<lambda>z. z powr s) has_field_derivative (s * z powr (s - 1))) (at z)"
+ apply (cases "z=0", auto)
+ apply (simp add: powr_def ln_complex_def)
+ apply (rule DERIV_transform_at [where d = "norm z" and f = "\<lambda>z. exp (s * Ln z)"])
+ apply (auto simp: dist_complex_def ln_complex_def)
+ apply (intro derivative_eq_intros | simp add: assms)+
+ apply (simp add: field_simps exp_diff)
+ done
+
+lemma has_field_derivative_powr_right:
+ "w \<noteq> 0 \<Longrightarrow> ((\<lambda>z. w powr z) has_field_derivative Ln w * w powr z) (at z)"
+ apply (simp add: powr_def ln_complex_def)
+ apply (intro derivative_eq_intros | simp add: assms)+
+ done
+
+lemma complex_differentiable_powr_right:
+ "w \<noteq> 0 \<Longrightarrow> (\<lambda>z. w powr z) complex_differentiable (at z)"
+using complex_differentiable_def has_field_derivative_powr_right by blast
+
+
+lemma holomorphic_on_powr_right:
+ "f holomorphic_on s \<Longrightarrow> w \<noteq> 0 \<Longrightarrow> (\<lambda>z. w powr (f z)) holomorphic_on s"
+ unfolding holomorphic_on_def
+ using DERIV_chain' complex_differentiable_def has_field_derivative_powr_right by fastforce
+
+
+lemma norm_powr_real_powr:
+ "w \<in> \<real> \<Longrightarrow> 0 < Re w \<Longrightarrow> norm(w powr z) = Re w powr Re z"
+ by (auto simp add: norm_powr_real powr_def Im_Ln_eq_0 complex_is_Real_iff in_Reals_norm ln_complex_def)
+
+lemma cmod_Ln_Reals [simp]:"z \<in> Reals \<Longrightarrow> 0 < Re z \<Longrightarrow> cmod (Ln z) = norm (ln (Re z))"
+ using Ln_of_real by force
+
+
subsection{*Relation between Square Root and exp/ln, hence its derivative*}
lemma csqrt_exp_Ln:
@@ -1336,10 +1444,6 @@
using open_Compl
by (force simp add: continuous_def eventually_at_topological filterlim_iff open_Collect_neg)
-lemma closed_Real_halfspace_Re_ge: "closed (\<real> \<inter> {w. x \<le> Re(w)})"
- using closed_halfspace_Re_ge
- by (simp add: closed_Int closed_complex_Reals)
-
lemma continuous_within_csqrt_posreal:
"continuous (at z within (\<real> \<inter> {w. 0 \<le> Re(w)})) csqrt"
proof (cases "Im z = 0 --> 0 < Re(z)")
@@ -1867,15 +1971,15 @@
Re z = pi & Im z \<le> 0"
shows "Arccos(cos z) = z"
proof -
- have *: "((\<i> - (Exp (\<i> * z))\<^sup>2 * \<i>) / (2 * Exp (\<i> * z))) = sin z"
+ have *: "((\<i> - (exp (\<i> * z))\<^sup>2 * \<i>) / (2 * exp (\<i> * z))) = sin z"
by (simp add: sin_exp_eq exp_minus field_simps power2_eq_square)
- have "1 - (exp (\<i> * z) + inverse (exp (\<i> * z)))\<^sup>2 / 4 = ((\<i> - (Exp (\<i> * z))\<^sup>2 * \<i>) / (2 * Exp (\<i> * z)))\<^sup>2"
+ have "1 - (exp (\<i> * z) + inverse (exp (\<i> * z)))\<^sup>2 / 4 = ((\<i> - (exp (\<i> * z))\<^sup>2 * \<i>) / (2 * exp (\<i> * z)))\<^sup>2"
by (simp add: field_simps power2_eq_square)
then have "Arccos(cos z) = - (\<i> * Ln ((exp (\<i> * z) + inverse (exp (\<i> * z))) / 2 +
- \<i> * csqrt (((\<i> - (Exp (\<i> * z))\<^sup>2 * \<i>) / (2 * Exp (\<i> * z)))\<^sup>2)))"
+ \<i> * csqrt (((\<i> - (exp (\<i> * z))\<^sup>2 * \<i>) / (2 * exp (\<i> * z)))\<^sup>2)))"
by (simp add: cos_exp_eq Arccos_def exp_minus)
also have "... = - (\<i> * Ln ((exp (\<i> * z) + inverse (exp (\<i> * z))) / 2 +
- \<i> * ((\<i> - (Exp (\<i> * z))\<^sup>2 * \<i>) / (2 * Exp (\<i> * z)))))"
+ \<i> * ((\<i> - (exp (\<i> * z))\<^sup>2 * \<i>) / (2 * exp (\<i> * z)))))"
apply (subst csqrt_square)
using assms Re_sin_pos [of z] Im_sin_nonneg [of z] Im_sin_nonneg2 [of z]
apply (auto simp: * Re_sin Im_sin)
@@ -2177,4 +2281,129 @@
lemma of_real_arccos: "abs x \<le> 1 \<Longrightarrow> of_real(arccos x) = Arccos(of_real x)"
by (metis Im_Arccos_of_real add.right_neutral arccos_eq_Re_Arccos complex_eq mult_zero_right of_real_0)
+subsection{*Some interrelationships among the real inverse trig functions.*}
+
+lemma arccos_arctan:
+ assumes "-1 < x" "x < 1"
+ shows "arccos x = pi/2 - arctan(x / sqrt(1 - x\<^sup>2))"
+proof -
+ have "arctan(x / sqrt(1 - x\<^sup>2)) - (pi/2 - arccos x) = 0"
+ proof (rule sin_eq_0_pi)
+ show "- pi < arctan (x / sqrt (1 - x\<^sup>2)) - (pi / 2 - arccos x)"
+ using arctan_lbound [of "x / sqrt(1 - x\<^sup>2)"] arccos_bounded [of x] assms
+ by (simp add: algebra_simps)
+ next
+ show "arctan (x / sqrt (1 - x\<^sup>2)) - (pi / 2 - arccos x) < pi"
+ using arctan_ubound [of "x / sqrt(1 - x\<^sup>2)"] arccos_bounded [of x] assms
+ by (simp add: algebra_simps)
+ next
+ show "sin (arctan (x / sqrt (1 - x\<^sup>2)) - (pi / 2 - arccos x)) = 0"
+ using assms
+ by (simp add: algebra_simps sin_diff cos_add sin_arccos sin_arctan cos_arctan
+ power2_eq_square square_eq_1_iff)
+ qed
+ then show ?thesis
+ by simp
+qed
+
+lemma arcsin_plus_arccos:
+ assumes "-1 \<le> x" "x \<le> 1"
+ shows "arcsin x + arccos x = pi/2"
+proof -
+ have "arcsin x = pi/2 - arccos x"
+ apply (rule sin_inj_pi)
+ using assms arcsin [OF assms] arccos [OF assms]
+ apply (auto simp: algebra_simps sin_diff)
+ done
+ then show ?thesis
+ by (simp add: algebra_simps)
+qed
+
+lemma arcsin_arccos_eq: "-1 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> arcsin x = pi/2 - arccos x"
+ using arcsin_plus_arccos by force
+
+lemma arccos_arcsin_eq: "-1 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> arccos x = pi/2 - arcsin x"
+ using arcsin_plus_arccos by force
+
+lemma arcsin_arctan: "-1 < x \<Longrightarrow> x < 1 \<Longrightarrow> arcsin x = arctan(x / sqrt(1 - x\<^sup>2))"
+ by (simp add: arccos_arctan arcsin_arccos_eq)
+
+lemma zz: "csqrt (1 - (of_real x)\<^sup>2) = (if x^2 \<le> 1 then sqrt (1 - x^2) else \<i> * sqrt (x^2 - 1))"
+ by ( simp add: of_real_sqrt del: csqrt_of_real_nonneg)
+
+lemma arcsin_arccos_sqrt_pos: "0 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> arcsin x = arccos(sqrt(1 - x\<^sup>2))"
+ apply (simp add: abs_square_le_1 diff_le_iff arcsin_eq_Re_Arcsin arccos_eq_Re_Arccos)
+ apply (subst Arcsin_Arccos_csqrt_pos)
+ apply (auto simp: power_le_one zz)
+ done
+
+lemma arcsin_arccos_sqrt_neg: "-1 \<le> x \<Longrightarrow> x \<le> 0 \<Longrightarrow> arcsin x = -arccos(sqrt(1 - x\<^sup>2))"
+ using arcsin_arccos_sqrt_pos [of "-x"]
+ by (simp add: arcsin_minus)
+
+lemma arccos_arcsin_sqrt_pos: "0 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> arccos x = arcsin(sqrt(1 - x\<^sup>2))"
+ apply (simp add: abs_square_le_1 diff_le_iff arcsin_eq_Re_Arcsin arccos_eq_Re_Arccos)
+ apply (subst Arccos_Arcsin_csqrt_pos)
+ apply (auto simp: power_le_one zz)
+ done
+
+lemma arccos_arcsin_sqrt_neg: "-1 \<le> x \<Longrightarrow> x \<le> 0 \<Longrightarrow> arccos x = pi - arcsin(sqrt(1 - x\<^sup>2))"
+ using arccos_arcsin_sqrt_pos [of "-x"]
+ by (simp add: arccos_minus)
+
+subsection{*continuity results for arcsin and arccos.*}
+
+lemma continuous_on_Arcsin_real [continuous_intros]:
+ "continuous_on {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1} Arcsin"
+proof -
+ have "continuous_on {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1} (\<lambda>x. complex_of_real (arcsin (Re x))) =
+ continuous_on {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1} (\<lambda>x. complex_of_real (Re (Arcsin (of_real (Re x)))))"
+ by (rule continuous_on_cong [OF refl]) (simp add: arcsin_eq_Re_Arcsin)
+ also have "... = ?thesis"
+ by (rule continuous_on_cong [OF refl]) simp
+ finally show ?thesis
+ using continuous_on_arcsin [OF continuous_on_Re [OF continuous_on_id], of "{w \<in> \<real>. \<bar>Re w\<bar> \<le> 1}"]
+ continuous_on_of_real
+ by fastforce
+qed
+
+lemma continuous_within_Arcsin_real:
+ "continuous (at z within {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1}) Arcsin"
+proof (cases "z \<in> {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1}")
+ case True then show ?thesis
+ using continuous_on_Arcsin_real continuous_on_eq_continuous_within
+ by blast
+next
+ case False
+ with closed_real_abs_le [of 1] show ?thesis
+ by (rule continuous_within_closed_nontrivial)
+qed
+
+lemma continuous_on_Arccos_real:
+ "continuous_on {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1} Arccos"
+proof -
+ have "continuous_on {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1} (\<lambda>x. complex_of_real (arccos (Re x))) =
+ continuous_on {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1} (\<lambda>x. complex_of_real (Re (Arccos (of_real (Re x)))))"
+ by (rule continuous_on_cong [OF refl]) (simp add: arccos_eq_Re_Arccos)
+ also have "... = ?thesis"
+ by (rule continuous_on_cong [OF refl]) simp
+ finally show ?thesis
+ using continuous_on_arccos [OF continuous_on_Re [OF continuous_on_id], of "{w \<in> \<real>. \<bar>Re w\<bar> \<le> 1}"]
+ continuous_on_of_real
+ by fastforce
+qed
+
+lemma continuous_within_Arccos_real:
+ "continuous (at z within {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1}) Arccos"
+proof (cases "z \<in> {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1}")
+ case True then show ?thesis
+ using continuous_on_Arccos_real continuous_on_eq_continuous_within
+ by blast
+next
+ case False
+ with closed_real_abs_le [of 1] show ?thesis
+ by (rule continuous_within_closed_nontrivial)
+qed
+
+
end