equal
deleted
inserted
replaced
1015 begin |
1015 begin |
1016 |
1016 |
1017 definition ln_complex :: "complex \<Rightarrow> complex" |
1017 definition ln_complex :: "complex \<Rightarrow> complex" |
1018 where "ln_complex \<equiv> \<lambda>z. THE w. exp w = z & -pi < Im(w) & Im(w) \<le> pi" |
1018 where "ln_complex \<equiv> \<lambda>z. THE w. exp w = z & -pi < Im(w) & Im(w) \<le> pi" |
1019 |
1019 |
|
1020 text\<open>NOTE: within this scope, the constant Ln is not yet available!\<close> |
1020 lemma |
1021 lemma |
1021 assumes "z \<noteq> 0" |
1022 assumes "z \<noteq> 0" |
1022 shows exp_Ln [simp]: "exp(ln z) = z" |
1023 shows exp_Ln [simp]: "exp(ln z) = z" |
1023 and mpi_less_Im_Ln: "-pi < Im(ln z)" |
1024 and mpi_less_Im_Ln: "-pi < Im(ln z)" |
1024 and Im_Ln_le_pi: "Im(ln z) \<le> pi" |
1025 and Im_Ln_le_pi: "Im(ln z) \<le> pi" |
1044 apply (rule exp_complex_eqI) |
1045 apply (rule exp_complex_eqI) |
1045 using assms mpi_less_Im_Ln [of "exp z"] Im_Ln_le_pi [of "exp z"] |
1046 using assms mpi_less_Im_Ln [of "exp z"] Im_Ln_le_pi [of "exp z"] |
1046 apply auto |
1047 apply auto |
1047 done |
1048 done |
1048 |
1049 |
1049 lemma Ln_eq_zero_iff [simp]: "x \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> Ln x = 0 \<longleftrightarrow> x = 1" |
|
1050 by auto (metis exp_Ln exp_zero nonpos_Reals_zero_I) |
|
1051 |
|
1052 subsection\<open>Relation to Real Logarithm\<close> |
1050 subsection\<open>Relation to Real Logarithm\<close> |
1053 |
1051 |
1054 lemma Ln_of_real: |
1052 lemma Ln_of_real: |
1055 assumes "0 < z" |
1053 assumes "0 < z" |
1056 shows "ln(of_real z::complex) = of_real(ln z)" |
1054 shows "ln(of_real z::complex) = of_real(ln z)" |
1071 by (simp add: Ln_of_real) |
1069 by (simp add: Ln_of_real) |
1072 |
1070 |
1073 lemma cmod_Ln_Reals [simp]: "z \<in> \<real> \<Longrightarrow> 0 < Re z \<Longrightarrow> cmod (ln z) = norm (ln (Re z))" |
1071 lemma cmod_Ln_Reals [simp]: "z \<in> \<real> \<Longrightarrow> 0 < Re z \<Longrightarrow> cmod (ln z) = norm (ln (Re z))" |
1074 using Ln_of_real by force |
1072 using Ln_of_real by force |
1075 |
1073 |
1076 lemma Ln_1: "ln 1 = (0::complex)" |
1074 lemma Ln_1 [simp]: "ln 1 = (0::complex)" |
1077 proof - |
1075 proof - |
1078 have "ln (exp 0) = (0::complex)" |
1076 have "ln (exp 0) = (0::complex)" |
1079 by (metis (mono_tags, hide_lams) Ln_of_real exp_zero ln_one of_real_0 of_real_1 zero_less_one) |
1077 by (metis (mono_tags, hide_lams) Ln_of_real exp_zero ln_one of_real_0 of_real_1 zero_less_one) |
1080 then show ?thesis |
1078 then show ?thesis |
1081 by simp |
1079 by simp |
1082 qed |
1080 qed |
|
1081 |
|
1082 |
|
1083 lemma Ln_eq_zero_iff [simp]: "x \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> ln x = 0 \<longleftrightarrow> x = 1" for x::complex |
|
1084 by auto (metis exp_Ln exp_zero nonpos_Reals_zero_I) |
1083 |
1085 |
1084 instance |
1086 instance |
1085 by intro_classes (rule ln_complex_def Ln_1) |
1087 by intro_classes (rule ln_complex_def Ln_1) |
1086 |
1088 |
1087 end |
1089 end |