changeset 76819 | fc4ad2a2b6b1 |
parent 76724 | 7ff71bdcf731 |
child 77089 | b4f892d0625d |
76797:18e719c6b633 | 76819:fc4ad2a2b6b1 |
---|---|
658 done |
658 done |
659 qed |
659 qed |
660 |
660 |
661 lemma norm_sin_squared: |
661 lemma norm_sin_squared: |
662 "norm(sin z) ^ 2 = (exp(2 * Im z) + inverse(exp(2 * Im z)) - 2 * cos(2 * Re z)) / 4" |
662 "norm(sin z) ^ 2 = (exp(2 * Im z) + inverse(exp(2 * Im z)) - 2 * cos(2 * Re z)) / 4" |
663 proof (cases z) |
663 using cos_double_sin [of "Re z"] |
664 case (Complex x1 x2) |
664 apply (simp add: sin_cos_eq norm_cos_squared exp_minus mult.commute [of _ 2] exp_double) |
665 then show ?thesis |
665 apply (simp add: algebra_simps power2_eq_square) |
666 apply (simp only: sin_add cmod_power2 cos_of_real sin_of_real cos_double_cos exp_double Complex_eq) |
666 done |
667 apply (simp add: cos_exp_eq sin_exp_eq exp_minus exp_of_real Re_divide Im_divide power_divide) |
|
668 apply (simp only: left_diff_distrib [symmetric] power_mult_distrib cos_squared_eq) |
|
669 apply (simp add: power2_eq_square field_split_simps) |
|
670 done |
|
671 qed |
|
672 |
667 |
673 lemma exp_uminus_Im: "exp (- Im z) \<le> exp (cmod z)" |
668 lemma exp_uminus_Im: "exp (- Im z) \<le> exp (cmod z)" |
674 using abs_Im_le_cmod linear order_trans by fastforce |
669 using abs_Im_le_cmod linear order_trans by fastforce |
675 |
670 |
676 lemma norm_cos_le: |
671 lemma norm_cos_le: |
1000 using cos_Arg2pi sin_Arg2pi Arg2pi_ge_0 Arg2pi_lt_2pi [of z] assms |
995 using cos_Arg2pi sin_Arg2pi Arg2pi_ge_0 Arg2pi_lt_2pi [of z] assms |
1001 by (auto simp: Re_exp Im_exp) |
996 by (auto simp: Re_exp Im_exp) |
1002 |
997 |
1003 lemma Arg2pi_times_of_real [simp]: |
998 lemma Arg2pi_times_of_real [simp]: |
1004 assumes "0 < r" shows "Arg2pi (of_real r * z) = Arg2pi z" |
999 assumes "0 < r" shows "Arg2pi (of_real r * z) = Arg2pi z" |
1005 proof (cases "z=0") |
1000 by (metis (no_types, lifting) Arg2pi Arg2pi_eq Arg2pi_unique assms mult.assoc |
1006 case False |
1001 mult_eq_0_iff mult_pos_pos of_real_mult zero_less_norm_iff) |
1007 show ?thesis |
|
1008 by (rule Arg2pi_unique [of "r * norm z"]) (use Arg2pi False assms is_Arg_def in auto) |
|
1009 qed auto |
|
1010 |
1002 |
1011 lemma Arg2pi_times_of_real2 [simp]: "0 < r \<Longrightarrow> Arg2pi (z * of_real r) = Arg2pi z" |
1003 lemma Arg2pi_times_of_real2 [simp]: "0 < r \<Longrightarrow> Arg2pi (z * of_real r) = Arg2pi z" |
1012 by (metis Arg2pi_times_of_real mult.commute) |
1004 by (metis Arg2pi_times_of_real mult.commute) |
1013 |
1005 |
1014 lemma Arg2pi_divide_of_real [simp]: "0 < r \<Longrightarrow> Arg2pi (z / of_real r) = Arg2pi z" |
1006 lemma Arg2pi_divide_of_real [simp]: "0 < r \<Longrightarrow> Arg2pi (z / of_real r) = Arg2pi z" |
1015 by (metis Arg2pi_times_of_real2 less_numeral_extra(3) nonzero_eq_divide_eq of_real_eq_0_iff) |
1007 by (metis Arg2pi_times_of_real2 less_irrefl nonzero_eq_divide_eq of_real_eq_0_iff) |
1016 |
1008 |
1017 lemma Arg2pi_le_pi: "Arg2pi z \<le> pi \<longleftrightarrow> 0 \<le> Im z" |
1009 lemma Arg2pi_le_pi: "Arg2pi z \<le> pi \<longleftrightarrow> 0 \<le> Im z" |
1018 proof (cases "z=0") |
1010 proof (cases "z=0") |
1019 case False |
1011 case False |
1020 have "0 \<le> Im z \<longleftrightarrow> 0 \<le> Im (of_real (cmod z) * exp (\<i> * complex_of_real (Arg2pi z)))" |
1012 have "0 \<le> Im z \<longleftrightarrow> 0 \<le> Im (of_real (cmod z) * exp (\<i> * complex_of_real (Arg2pi z)))" |
1093 by (auto simp: Arg2pi_real in_Reals_norm exp_diff field_simps) |
1085 by (auto simp: Arg2pi_real in_Reals_norm exp_diff field_simps) |
1094 qed auto |
1086 qed auto |
1095 |
1087 |
1096 lemma Arg2pi_eq_iff: |
1088 lemma Arg2pi_eq_iff: |
1097 assumes "w \<noteq> 0" "z \<noteq> 0" |
1089 assumes "w \<noteq> 0" "z \<noteq> 0" |
1098 shows "Arg2pi w = Arg2pi z \<longleftrightarrow> (\<exists>x. 0 < x & w = of_real x * z)" |
1090 shows "Arg2pi w = Arg2pi z \<longleftrightarrow> (\<exists>x. 0 < x & w = of_real x * z)" (is "?lhs = ?rhs") |
1099 using assms Arg2pi_eq [of z] Arg2pi_eq [of w] |
1091 proof |
1100 apply auto |
1092 assume ?lhs |
1101 apply (rule_tac x="norm w / norm z" in exI) |
1093 then have "(cmod w) * (z / cmod z) = w" |
1102 apply (simp add: field_split_simps) |
1094 by (metis Arg2pi_eq assms(2) mult_eq_0_iff nonzero_mult_div_cancel_left) |
1103 by (metis mult.commute mult.left_commute) |
1095 then show ?rhs |
1096 by (metis assms divide_pos_pos of_real_divide times_divide_eq_left times_divide_eq_right zero_less_norm_iff) |
|
1097 qed auto |
|
1104 |
1098 |
1105 lemma Arg2pi_inverse_eq_0: "Arg2pi(inverse z) = 0 \<longleftrightarrow> Arg2pi z = 0" |
1099 lemma Arg2pi_inverse_eq_0: "Arg2pi(inverse z) = 0 \<longleftrightarrow> Arg2pi z = 0" |
1106 by (metis Arg2pi_eq_0 Arg2pi_inverse inverse_inverse_eq) |
1100 by (metis Arg2pi_eq_0 Arg2pi_inverse inverse_inverse_eq) |
1107 |
1101 |
1108 lemma Arg2pi_divide: |
1102 lemma Arg2pi_divide: |
1140 shows "Arg2pi (w * z) = (if Arg2pi w + Arg2pi z < 2*pi then Arg2pi w + Arg2pi z |
1134 shows "Arg2pi (w * z) = (if Arg2pi w + Arg2pi z < 2*pi then Arg2pi w + Arg2pi z |
1141 else (Arg2pi w + Arg2pi z) - 2*pi)" |
1135 else (Arg2pi w + Arg2pi z) - 2*pi)" |
1142 using Arg2pi_add [OF assms] |
1136 using Arg2pi_add [OF assms] |
1143 by auto |
1137 by auto |
1144 |
1138 |
1145 lemma Arg2pi_cnj_eq_inverse: "z\<noteq>0 \<Longrightarrow> Arg2pi (cnj z) = Arg2pi (inverse z)" |
1139 lemma Arg2pi_cnj_eq_inverse: |
1146 apply (simp add: Arg2pi_eq_iff field_split_simps complex_norm_square [symmetric]) |
1140 assumes "z \<noteq> 0" shows "Arg2pi (cnj z) = Arg2pi (inverse z)" |
1147 by (metis of_real_power zero_less_norm_iff zero_less_power) |
1141 proof - |
1142 have "\<exists>r>0. of_real r / z = cnj z" |
|
1143 by (metis assms complex_norm_square nonzero_mult_div_cancel_left zero_less_norm_iff zero_less_power) |
|
1144 then show ?thesis |
|
1145 by (metis Arg2pi_times_of_real2 divide_inverse_commute) |
|
1146 qed |
|
1148 |
1147 |
1149 lemma Arg2pi_cnj: "Arg2pi(cnj z) = (if z \<in> \<real> then Arg2pi z else 2*pi - Arg2pi z)" |
1148 lemma Arg2pi_cnj: "Arg2pi(cnj z) = (if z \<in> \<real> then Arg2pi z else 2*pi - Arg2pi z)" |
1150 proof (cases "z=0") |
1149 by (metis Arg2pi_cnj_eq_inverse Arg2pi_inverse Reals_cnj_iff complex_cnj_zero) |
1151 case False |
|
1152 then show ?thesis |
|
1153 by (simp add: Arg2pi_cnj_eq_inverse Arg2pi_inverse) |
|
1154 qed auto |
|
1155 |
1150 |
1156 lemma Arg2pi_exp: "0 \<le> Im z \<Longrightarrow> Im z < 2*pi \<Longrightarrow> Arg2pi(exp z) = Im z" |
1151 lemma Arg2pi_exp: "0 \<le> Im z \<Longrightarrow> Im z < 2*pi \<Longrightarrow> Arg2pi(exp z) = Im z" |
1157 by (rule Arg2pi_unique [of "exp(Re z)"]) (auto simp: exp_eq_polar) |
1152 by (simp add: Arg2pi_unique exp_eq_polar) |
1158 |
1153 |
1159 lemma complex_split_polar: |
1154 lemma complex_split_polar: |
1160 obtains r a::real where "z = complex_of_real r * (cos a + \<i> * sin a)" "0 \<le> r" "0 \<le> a" "a < 2*pi" |
1155 obtains r a::real where "z = complex_of_real r * (cos a + \<i> * sin a)" "0 \<le> r" "0 \<le> a" "a < 2*pi" |
1161 using Arg2pi cis.ctr cis_conv_exp unfolding Complex_eq is_Arg_def by fastforce |
1156 using Arg2pi cis.ctr cis_conv_exp unfolding Complex_eq is_Arg_def by fastforce |
1162 |
1157 |
2213 by (auto simp: Re_exp Im_exp) |
2208 by (auto simp: Re_exp Im_exp) |
2214 qed |
2209 qed |
2215 |
2210 |
2216 lemma Arg_times_of_real [simp]: |
2211 lemma Arg_times_of_real [simp]: |
2217 assumes "0 < r" shows "Arg (of_real r * z) = Arg z" |
2212 assumes "0 < r" shows "Arg (of_real r * z) = Arg z" |
2218 proof (cases "z=0") |
2213 using Arg_def Ln_times_of_real assms by auto |
2219 case True |
|
2220 then show ?thesis |
|
2221 by (simp add: Arg_def) |
|
2222 next |
|
2223 case False |
|
2224 with Arg_eq assms show ?thesis |
|
2225 by (auto simp: mpi_less_Arg Arg_le_pi intro!: Arg_unique [of "r * norm z"]) |
|
2226 qed |
|
2227 |
2214 |
2228 lemma Arg_times_of_real2 [simp]: "0 < r \<Longrightarrow> Arg (z * of_real r) = Arg z" |
2215 lemma Arg_times_of_real2 [simp]: "0 < r \<Longrightarrow> Arg (z * of_real r) = Arg z" |
2229 by (metis Arg_times_of_real mult.commute) |
2216 by (metis Arg_times_of_real mult.commute) |
2230 |
2217 |
2231 lemma Arg_divide_of_real [simp]: "0 < r \<Longrightarrow> Arg (z / of_real r) = Arg z" |
2218 lemma Arg_divide_of_real [simp]: "0 < r \<Longrightarrow> Arg (z / of_real r) = Arg z" |
2232 by (metis Arg_times_of_real2 less_numeral_extra(3) nonzero_eq_divide_eq of_real_eq_0_iff) |
2219 by (metis Arg_times_of_real2 less_irrefl nonzero_eq_divide_eq of_real_eq_0_iff) |
2233 |
2220 |
2234 lemma Arg_less_0: "0 \<le> Arg z \<longleftrightarrow> 0 \<le> Im z" |
2221 lemma Arg_less_0: "0 \<le> Arg z \<longleftrightarrow> 0 \<le> Im z" |
2235 using Im_Ln_le_pi Im_Ln_pos_le |
2222 using Im_Ln_le_pi Im_Ln_pos_le |
2236 by (simp add: Arg_def) |
2223 by (simp add: Arg_def) |
2237 |
2224 |
2241 lemma Arg_lt_pi: "0 < Arg z \<and> Arg z < pi \<longleftrightarrow> 0 < Im z" |
2228 lemma Arg_lt_pi: "0 < Arg z \<and> Arg z < pi \<longleftrightarrow> 0 < Im z" |
2242 using Arg_less_0 [of z] Im_Ln_pos_lt |
2229 using Arg_less_0 [of z] Im_Ln_pos_lt |
2243 by (auto simp: order.order_iff_strict Arg_def) |
2230 by (auto simp: order.order_iff_strict Arg_def) |
2244 |
2231 |
2245 lemma Arg_eq_0: "Arg z = 0 \<longleftrightarrow> z \<in> \<real> \<and> 0 \<le> Re z" |
2232 lemma Arg_eq_0: "Arg z = 0 \<longleftrightarrow> z \<in> \<real> \<and> 0 \<le> Re z" |
2246 using complex_is_Real_iff |
2233 using Arg_def Im_Ln_eq_0 complex_eq_iff complex_is_Real_iff by auto |
2247 by (simp add: Arg_def Im_Ln_eq_0) (metis less_eq_real_def of_real_Re of_real_def scale_zero_left) |
|
2248 |
2234 |
2249 corollary\<^marker>\<open>tag unimportant\<close> Arg_ne_0: assumes "z \<notin> \<real>\<^sub>\<ge>\<^sub>0" shows "Arg z \<noteq> 0" |
2235 corollary\<^marker>\<open>tag unimportant\<close> Arg_ne_0: assumes "z \<notin> \<real>\<^sub>\<ge>\<^sub>0" shows "Arg z \<noteq> 0" |
2250 using assms by (auto simp: nonneg_Reals_def Arg_eq_0) |
2236 using assms by (auto simp: nonneg_Reals_def Arg_eq_0) |
2251 |
2237 |
2252 lemma Arg_eq_pi_iff: "Arg z = pi \<longleftrightarrow> z \<in> \<real> \<and> Re z < 0" |
2238 lemma Arg_eq_pi_iff: "Arg z = pi \<longleftrightarrow> z \<in> \<real> \<and> Re z < 0" |
2253 proof (cases "z=0") |
2239 using Arg_eq_pi complex_is_Real_iff by blast |
2254 case False |
|
2255 then show ?thesis |
|
2256 using Arg_eq_0 [of "-z"] Arg_eq_pi complex_is_Real_iff by blast |
|
2257 qed (simp add: Arg_def) |
|
2258 |
2240 |
2259 lemma Arg_eq_0_pi: "Arg z = 0 \<or> Arg z = pi \<longleftrightarrow> z \<in> \<real>" |
2241 lemma Arg_eq_0_pi: "Arg z = 0 \<or> Arg z = pi \<longleftrightarrow> z \<in> \<real>" |
2260 using Arg_eq_pi_iff Arg_eq_0 by force |
2242 using Arg_eq_pi_iff Arg_eq_0 by force |
2261 |
2243 |
2262 lemma Arg_real: "z \<in> \<real> \<Longrightarrow> Arg z = (if 0 \<le> Re z then 0 else pi)" |
2244 lemma Arg_real: "z \<in> \<real> \<Longrightarrow> Arg z = (if 0 \<le> Re z then 0 else pi)" |
2264 |
2246 |
2265 lemma Arg_inverse: "Arg(inverse z) = (if z \<in> \<real> then Arg z else - Arg z)" |
2247 lemma Arg_inverse: "Arg(inverse z) = (if z \<in> \<real> then Arg z else - Arg z)" |
2266 proof (cases "z \<in> \<real>") |
2248 proof (cases "z \<in> \<real>") |
2267 case True |
2249 case True |
2268 then show ?thesis |
2250 then show ?thesis |
2269 by simp (metis Arg2pi_inverse Arg2pi_real Arg_real Reals_inverse) |
2251 by (metis Arg2pi_inverse Arg2pi_real Arg_real Reals_inverse) |
2270 next |
2252 next |
2271 case False |
2253 case False |
2272 then have z: "Arg z < pi" "z \<noteq> 0" |
2254 then show ?thesis |
2273 using Arg_eq_0_pi Arg_le_pi by (auto simp: less_eq_real_def) |
2255 by (simp add: Arg_def Ln_inverse complex_is_Real_iff complex_nonpos_Reals_iff) |
2274 show ?thesis |
|
2275 apply (rule Arg_unique [of "inverse (norm z)"]) |
|
2276 using False z mpi_less_Arg [of z] Arg_eq [of z] |
|
2277 by (auto simp: exp_minus field_simps) |
|
2278 qed |
2256 qed |
2279 |
2257 |
2280 lemma Arg_eq_iff: |
2258 lemma Arg_eq_iff: |
2281 assumes "w \<noteq> 0" "z \<noteq> 0" |
2259 assumes "w \<noteq> 0" "z \<noteq> 0" |
2282 shows "Arg w = Arg z \<longleftrightarrow> (\<exists>x. 0 < x \<and> w = of_real x * z)" (is "?lhs = ?rhs") |
2260 shows "Arg w = Arg z \<longleftrightarrow> (\<exists>x. 0 < x \<and> w = of_real x * z)" (is "?lhs = ?rhs") |
2283 proof |
2261 proof |
2284 assume ?lhs |
2262 assume ?lhs |
2285 then have "w = complex_of_real (cmod w / cmod z) * z" |
2263 then have "w = (cmod w / cmod z) * z" |
2286 by (metis Arg_eq assms divide_divide_eq_right eq_divide_eq exp_not_eq_zero of_real_divide) |
2264 by (metis Arg_eq assms divide_divide_eq_right eq_divide_eq exp_not_eq_zero of_real_divide) |
2287 then show ?rhs |
2265 then show ?rhs |
2288 using assms divide_pos_pos zero_less_norm_iff by blast |
2266 using assms divide_pos_pos zero_less_norm_iff by blast |
2289 qed auto |
2267 qed auto |
2290 |
2268 |
2305 |
2283 |
2306 lemma continuous_at_Arg: |
2284 lemma continuous_at_Arg: |
2307 assumes "z \<notin> \<real>\<^sub>\<le>\<^sub>0" |
2285 assumes "z \<notin> \<real>\<^sub>\<le>\<^sub>0" |
2308 shows "continuous (at z) Arg" |
2286 shows "continuous (at z) Arg" |
2309 proof - |
2287 proof - |
2310 have [simp]: "(\<lambda>z. Im (Ln z)) \<midarrow>z\<rightarrow> Arg z" |
2288 have "(\<lambda>z. Im (Ln z)) \<midarrow>z\<rightarrow> Arg z" |
2311 using Arg_def assms continuous_at by fastforce |
2289 using Arg_def assms continuous_at by fastforce |
2312 show ?thesis |
2290 then show ?thesis |
2313 unfolding continuous_at |
2291 unfolding continuous_at |
2314 proof (rule Lim_transform_within_open) |
2292 by (smt (verit, del_insts) Arg_eq_Im_Ln Lim_transform_away_at assms nonpos_Reals_zero_I) |
2315 show "\<And>w. \<lbrakk>w \<in> - \<real>\<^sub>\<le>\<^sub>0; w \<noteq> z\<rbrakk> \<Longrightarrow> Im (Ln w) = Arg w" |
|
2316 by (metis Arg_def Compl_iff nonpos_Reals_zero_I) |
|
2317 qed (use assms in auto) |
|
2318 qed |
2293 qed |
2319 |
2294 |
2320 lemma continuous_within_Arg: "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> continuous (at z within S) Arg" |
2295 lemma continuous_within_Arg: "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> continuous (at z within S) Arg" |
2321 using continuous_at_Arg continuous_at_imp_continuous_within by blast |
2296 using continuous_at_Arg continuous_at_imp_continuous_within by blast |
2322 |
2297 |
2386 finally show "Im (sgn z) = Im (cis (arctan (Im z / Re z)))" |
2361 finally show "Im (sgn z) = Im (cis (arctan (Im z / Re z)))" |
2387 by simp |
2362 by simp |
2388 qed |
2363 qed |
2389 next |
2364 next |
2390 show "arctan (Im z / Re z) > -pi" |
2365 show "arctan (Im z / Re z) > -pi" |
2391 by (rule le_less_trans[OF _ arctan_lbound]) auto |
2366 by (smt (verit, ccfv_SIG) arctan field_sum_of_halves) |
2392 next |
2367 next |
2393 have "arctan (Im z / Re z) < pi / 2" |
2368 show "arctan (Im z / Re z) \<le> pi" |
2394 by (rule arctan_ubound) |
2369 by (smt (verit, best) arctan field_sum_of_halves) |
2395 also have "\<dots> \<le> pi" by simp |
|
2396 finally show "arctan (Im z / Re z) \<le> pi" |
|
2397 by simp |
|
2398 qed |
2370 qed |
2399 |
2371 |
2400 subsection\<^marker>\<open>tag unimportant\<close>\<open>Relation between Ln and Arg2pi, and hence continuity of Arg2pi\<close> |
2372 subsection\<^marker>\<open>tag unimportant\<close>\<open>Relation between Ln and Arg2pi, and hence continuity of Arg2pi\<close> |
2401 |
2373 |
2402 lemma Arg2pi_Ln: |
2374 lemma Arg2pi_Ln: "0 < Arg2pi z \<Longrightarrow> Arg2pi z = Im(Ln(-z)) + pi" |
2403 assumes "0 < Arg2pi z" shows "Arg2pi z = Im(Ln(-z)) + pi" |
2375 by (smt (verit, best) Arg2pi_0 Arg2pi_exp Arg2pi_minus Arg_exp Arg_minus Im_Ln_le_pi |
2404 proof (cases "z = 0") |
2376 exp_Ln mpi_less_Im_Ln neg_equal_0_iff_equal) |
2405 case True |
|
2406 with assms show ?thesis |
|
2407 by simp |
|
2408 next |
|
2409 case False |
|
2410 then have "z / of_real(norm z) = exp(\<i> * of_real(Arg2pi z))" |
|
2411 using Arg2pi [of z] |
|
2412 by (metis is_Arg_def abs_norm_cancel nonzero_mult_div_cancel_left norm_of_real zero_less_norm_iff) |
|
2413 then have "- z / of_real(norm z) = exp (\<i> * (of_real (Arg2pi z) - pi))" |
|
2414 using cis_conv_exp cis_pi |
|
2415 by (auto simp: exp_diff algebra_simps) |
|
2416 then have "ln (- z / of_real(norm z)) = ln (exp (\<i> * (of_real (Arg2pi z) - pi)))" |
|
2417 by simp |
|
2418 also have "\<dots> = \<i> * (of_real(Arg2pi z) - pi)" |
|
2419 using Arg2pi [of z] assms pi_not_less_zero |
|
2420 by auto |
|
2421 finally have "Arg2pi z = Im (Ln (- z / of_real (cmod z))) + pi" |
|
2422 by simp |
|
2423 also have "\<dots> = Im (Ln (-z) - ln (cmod z)) + pi" |
|
2424 by (metis diff_0_right minus_diff_eq zero_less_norm_iff Ln_divide_of_real False) |
|
2425 also have "\<dots> = Im (Ln (-z)) + pi" |
|
2426 by simp |
|
2427 finally show ?thesis . |
|
2428 qed |
|
2429 |
2377 |
2430 lemma continuous_at_Arg2pi: |
2378 lemma continuous_at_Arg2pi: |
2431 assumes "z \<notin> \<real>\<^sub>\<ge>\<^sub>0" |
2379 assumes "z \<notin> \<real>\<^sub>\<ge>\<^sub>0" |
2432 shows "continuous (at z) Arg2pi" |
2380 shows "continuous (at z) Arg2pi" |
2433 proof - |
2381 proof - |
2434 have *: "isCont (\<lambda>z. Im (Ln (- z)) + pi) z" |
2382 have *: "isCont (\<lambda>z. Im (Ln (- z)) + pi) z" |
2435 by (rule Complex.isCont_Im isCont_Ln' continuous_intros | simp add: assms complex_is_Real_iff)+ |
2383 by (rule Complex.isCont_Im isCont_Ln' continuous_intros | simp add: assms complex_is_Real_iff)+ |
2436 have [simp]: "Im x \<noteq> 0 \<Longrightarrow> Im (Ln (- x)) + pi = Arg2pi x" for x |
|
2437 using Arg2pi_Ln by (simp add: Arg2pi_gt_0 complex_nonneg_Reals_iff) |
|
2438 consider "Re z < 0" | "Im z \<noteq> 0" using assms |
2384 consider "Re z < 0" | "Im z \<noteq> 0" using assms |
2439 using complex_nonneg_Reals_iff not_le by blast |
2385 using complex_nonneg_Reals_iff not_le by blast |
2440 then have [simp]: "(\<lambda>z. Im (Ln (- z)) + pi) \<midarrow>z\<rightarrow> Arg2pi z" |
2386 then have "(\<lambda>z. Im (Ln (- z)) + pi) \<midarrow>z\<rightarrow> Arg2pi z" |
2441 using "*" by (simp add: Arg2pi_Ln Arg2pi_gt_0 assms continuous_within) |
2387 using "*" by (simp add: Arg2pi_Ln Arg2pi_gt_0 assms continuous_within) |
2442 show ?thesis |
2388 then show ?thesis |
2443 unfolding continuous_at |
2389 unfolding continuous_at |
2444 proof (rule Lim_transform_within_open) |
2390 by (metis (mono_tags, lifting) Arg2pi_Ln Arg2pi_gt_0 Compl_iff Lim_transform_within_open assms |
2445 show "\<And>x. \<lbrakk>x \<in> - \<real>\<^sub>\<ge>\<^sub>0; x \<noteq> z\<rbrakk> \<Longrightarrow> Im (Ln (- x)) + pi = Arg2pi x" |
2391 closed_nonneg_Reals_complex open_Compl) |
2446 by (auto simp add: Arg2pi_Ln [OF Arg2pi_gt_0] complex_nonneg_Reals_iff) |
|
2447 qed (use assms in auto) |
|
2448 qed |
2392 qed |
2449 |
2393 |
2450 |
2394 |
2451 text\<open>Relation between Arg2pi and arctangent in upper halfplane\<close> |
2395 text\<open>Relation between Arg2pi and arctangent in upper halfplane\<close> |
2452 lemma Arg2pi_arctan_upperhalf: |
2396 lemma Arg2pi_arctan_upperhalf: |
2465 qed (use assms in auto) |
2409 qed (use assms in auto) |
2466 |
2410 |
2467 lemma Arg2pi_eq_Im_Ln: |
2411 lemma Arg2pi_eq_Im_Ln: |
2468 assumes "0 \<le> Im z" "0 < Re z" |
2412 assumes "0 \<le> Im z" "0 < Re z" |
2469 shows "Arg2pi z = Im (Ln z)" |
2413 shows "Arg2pi z = Im (Ln z)" |
2470 proof (cases "Im z = 0") |
2414 by (smt (verit, ccfv_SIG) Arg2pi_exp Im_Ln_pos_le assms exp_Ln pi_neq_zero zero_complex.simps(1)) |
2471 case True then show ?thesis |
|
2472 using Arg2pi_eq_0 Ln_in_Reals assms(2) complex_is_Real_iff by auto |
|
2473 next |
|
2474 case False |
|
2475 then have *: "Arg2pi z > 0" |
|
2476 using Arg2pi_gt_0 complex_is_Real_iff by blast |
|
2477 then have "z \<noteq> 0" |
|
2478 by auto |
|
2479 with * assms False show ?thesis |
|
2480 by (subst Arg2pi_Ln) (auto simp: Ln_minus) |
|
2481 qed |
|
2482 |
2415 |
2483 lemma continuous_within_upperhalf_Arg2pi: |
2416 lemma continuous_within_upperhalf_Arg2pi: |
2484 assumes "z \<noteq> 0" |
2417 assumes "z \<noteq> 0" |
2485 shows "continuous (at z within {z. 0 \<le> Im z}) Arg2pi" |
2418 shows "continuous (at z within {z. 0 \<le> Im z}) Arg2pi" |
2486 proof (cases "z \<in> \<real>\<^sub>\<ge>\<^sub>0") |
2419 proof (cases "z \<in> \<real>\<^sub>\<ge>\<^sub>0") |
2679 \<longleftrightarrow> ((\<lambda>z. g z powr of_int n) has_field_derivative dd') (at z within S)" |
2612 \<longleftrightarrow> ((\<lambda>z. g z powr of_int n) has_field_derivative dd') (at z within S)" |
2680 by simp |
2613 by simp |
2681 also have "\<dots> \<longleftrightarrow> ((\<lambda>z. g z ^ nat n) has_field_derivative dd') (at z within S)" |
2614 also have "\<dots> \<longleftrightarrow> ((\<lambda>z. g z ^ nat n) has_field_derivative dd') (at z within S)" |
2682 proof (rule has_field_derivative_cong_eventually) |
2615 proof (rule has_field_derivative_cong_eventually) |
2683 show "\<forall>\<^sub>F x in at z within S. g x powr of_int n = g x ^ nat n" |
2616 show "\<forall>\<^sub>F x in at z within S. g x powr of_int n = g x ^ nat n" |
2684 unfolding eventually_at |
2617 unfolding eventually_at by (metis e_dist \<open>e>0\<close> dist_commute powr_of_int that) |
2685 apply (rule exI[where x=e]) |
|
2686 using powr_of_int that \<open>e>0\<close> e_dist by (simp add: dist_commute) |
|
2687 qed (use powr_of_int \<open>g z\<noteq>0\<close> that in simp) |
2618 qed (use powr_of_int \<open>g z\<noteq>0\<close> that in simp) |
2688 also have "\<dots>" unfolding dd'_def using gderiv that |
2619 also have "\<dots>" unfolding dd'_def using gderiv that |
2689 by (auto intro!: derivative_eq_intros) |
2620 by (auto intro!: derivative_eq_intros) |
2690 finally have "((\<lambda>z. g z powr of_int n) has_field_derivative dd) (at z within S)" . |
2621 finally have "((\<lambda>z. g z powr of_int n) has_field_derivative dd) (at z within S)" . |
2691 then show ?thesis unfolding dd_def by simp |
2622 then show ?thesis unfolding dd_def by simp |
2705 by simp |
2636 by simp |
2706 also have "\<dots> \<longleftrightarrow> ((\<lambda>z. inverse (g z ^ nat (-n))) has_field_derivative dd') (at z within S)" |
2637 also have "\<dots> \<longleftrightarrow> ((\<lambda>z. inverse (g z ^ nat (-n))) has_field_derivative dd') (at z within S)" |
2707 proof (rule has_field_derivative_cong_eventually) |
2638 proof (rule has_field_derivative_cong_eventually) |
2708 show "\<forall>\<^sub>F x in at z within S. g x powr of_int n = inverse (g x ^ nat (- n))" |
2639 show "\<forall>\<^sub>F x in at z within S. g x powr of_int n = inverse (g x ^ nat (- n))" |
2709 unfolding eventually_at |
2640 unfolding eventually_at |
2710 apply (rule exI[where x=e]) |
2641 by (metis \<open>e>0\<close> e_dist dist_commute linorder_not_le powr_of_int that) |
2711 using powr_of_int that \<open>e>0\<close> e_dist by (simp add: dist_commute) |
|
2712 qed (use powr_of_int \<open>g z\<noteq>0\<close> that in simp) |
2642 qed (use powr_of_int \<open>g z\<noteq>0\<close> that in simp) |
2713 also have "\<dots>" |
2643 also have "\<dots>" |
2714 proof - |
2644 proof - |
2715 have "nat (- n) + nat (1 - n) - Suc 0 = nat (- n) + nat (- n)" |
2645 have "nat (- n) + nat (1 - n) - Suc 0 = nat (- n) + nat (- n)" |
2716 by auto |
2646 by auto |
2757 fixes w::complex |
2687 fixes w::complex |
2758 shows "w \<noteq> 0 \<Longrightarrow> (\<lambda>z. w powr z) field_differentiable (at z)" |
2688 shows "w \<noteq> 0 \<Longrightarrow> (\<lambda>z. w powr z) field_differentiable (at z)" |
2759 using field_differentiable_def has_field_derivative_powr_right by blast |
2689 using field_differentiable_def has_field_derivative_powr_right by blast |
2760 |
2690 |
2761 lemma holomorphic_on_powr_right [holomorphic_intros]: |
2691 lemma holomorphic_on_powr_right [holomorphic_intros]: |
2762 assumes "f holomorphic_on s" |
2692 assumes "f holomorphic_on S" |
2763 shows "(\<lambda>z. w powr (f z)) holomorphic_on s" |
2693 shows "(\<lambda>z. w powr (f z)) holomorphic_on S" |
2764 proof (cases "w = 0") |
2694 proof (cases "w = 0") |
2765 case False |
2695 case False |
2766 with assms show ?thesis |
2696 with assms show ?thesis |
2767 unfolding holomorphic_on_def field_differentiable_def |
2697 unfolding holomorphic_on_def field_differentiable_def |
2768 by (metis (full_types) DERIV_chain' has_field_derivative_powr_right) |
2698 by (metis (full_types) DERIV_chain' has_field_derivative_powr_right) |
2769 qed simp |
2699 qed simp |
2770 |
2700 |
2771 lemma holomorphic_on_divide_gen [holomorphic_intros]: |
2701 lemma holomorphic_on_divide_gen [holomorphic_intros]: |
2772 assumes f: "f holomorphic_on s" and g: "g holomorphic_on s" and 0: "\<And>z z'. \<lbrakk>z \<in> s; z' \<in> s\<rbrakk> \<Longrightarrow> g z = 0 \<longleftrightarrow> g z' = 0" |
2702 assumes "f holomorphic_on S" "g holomorphic_on S" and "\<And>z z'. \<lbrakk>z \<in> S; z' \<in> S\<rbrakk> \<Longrightarrow> g z = 0 \<longleftrightarrow> g z' = 0" |
2773 shows "(\<lambda>z. f z / g z) holomorphic_on s" |
2703 shows "(\<lambda>z. f z / g z) holomorphic_on S" |
2774 proof (cases "\<exists>z\<in>s. g z = 0") |
2704 by (metis (no_types, lifting) assms division_ring_divide_zero holomorphic_on_divide holomorphic_transform) |
2775 case True |
|
2776 with 0 have "g z = 0" if "z \<in> s" for z |
|
2777 using that by blast |
|
2778 then show ?thesis |
|
2779 using g holomorphic_transform by auto |
|
2780 next |
|
2781 case False |
|
2782 with 0 have "g z \<noteq> 0" if "z \<in> s" for z |
|
2783 using that by blast |
|
2784 with holomorphic_on_divide show ?thesis |
|
2785 using f g by blast |
|
2786 qed |
|
2787 |
2705 |
2788 lemma norm_powr_real_powr: |
2706 lemma norm_powr_real_powr: |
2789 "w \<in> \<real> \<Longrightarrow> 0 \<le> Re w \<Longrightarrow> cmod (w powr z) = Re w powr Re z" |
2707 "w \<in> \<real> \<Longrightarrow> 0 \<le> Re w \<Longrightarrow> cmod (w powr z) = Re w powr Re z" |
2790 by (metis dual_order.order_iff_strict norm_powr_real norm_zero of_real_0 of_real_Re powr_def) |
2708 by (metis dual_order.order_iff_strict norm_powr_real norm_zero of_real_0 of_real_Re powr_def) |
2791 |
2709 |
2877 qed |
2795 qed |
2878 |
2796 |
2879 lemma tendsto_neg_powr_complex_of_nat: |
2797 lemma tendsto_neg_powr_complex_of_nat: |
2880 assumes "filterlim f at_top F" and "Re s < 0" |
2798 assumes "filterlim f at_top F" and "Re s < 0" |
2881 shows "((\<lambda>x. of_nat (f x) powr s) \<longlongrightarrow> 0) F" |
2799 shows "((\<lambda>x. of_nat (f x) powr s) \<longlongrightarrow> 0) F" |
2800 using tendsto_neg_powr_complex_of_real [of "real o f" F s] |
|
2882 proof - |
2801 proof - |
2883 have "((\<lambda>x. of_real (real (f x)) powr s) \<longlongrightarrow> 0) F" using assms(2) |
2802 have "((\<lambda>x. of_real (real (f x)) powr s) \<longlongrightarrow> 0) F" using assms(2) |
2884 by (intro filterlim_compose[OF _ tendsto_neg_powr_complex_of_real] |
2803 by (intro filterlim_compose[OF _ tendsto_neg_powr_complex_of_real] |
2885 filterlim_compose[OF _ assms(1)] filterlim_real_sequentially filterlim_ident) auto |
2804 filterlim_compose[OF _ assms(1)] filterlim_real_sequentially filterlim_ident) auto |
2886 thus ?thesis by simp |
2805 thus ?thesis by simp |
3091 finally have "csqrt z = csqrt ((exp (Ln z / 2))\<^sup>2)" |
3010 finally have "csqrt z = csqrt ((exp (Ln z / 2))\<^sup>2)" |
3092 by simp |
3011 by simp |
3093 also have "\<dots> = exp (Ln z / 2)" |
3012 also have "\<dots> = exp (Ln z / 2)" |
3094 apply (rule csqrt_square) |
3013 apply (rule csqrt_square) |
3095 using cos_gt_zero_pi [of "(Im (Ln z) / 2)"] Im_Ln_le_pi mpi_less_Im_Ln assms |
3014 using cos_gt_zero_pi [of "(Im (Ln z) / 2)"] Im_Ln_le_pi mpi_less_Im_Ln assms |
3096 by (fastforce simp: Re_exp Im_exp ) |
3015 by (fastforce simp: Re_exp Im_exp) |
3097 finally show ?thesis using assms csqrt_square |
3016 finally show ?thesis using assms csqrt_square |
3098 by simp |
3017 by simp |
3099 qed |
3018 qed |
3100 |
3019 |
3101 lemma csqrt_inverse: |
3020 lemma csqrt_inverse: |
3102 assumes "z \<notin> \<real>\<^sub>\<le>\<^sub>0" |
3021 "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> csqrt (inverse z) = inverse (csqrt z)" |
3103 shows "csqrt (inverse z) = inverse (csqrt z)" |
3022 by (metis Ln_inverse csqrt_eq_0 csqrt_exp_Ln divide_minus_left exp_minus |
3104 proof (cases "z=0") |
3023 inverse_nonzero_iff_nonzero) |
3105 case False |
3024 |
3106 then show ?thesis |
3025 lemma cnj_csqrt: "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> cnj(csqrt z) = csqrt(cnj z)" |
3107 using assms csqrt_exp_Ln Ln_inverse exp_minus |
3026 by (metis cnj_Ln complex_cnj_divide complex_cnj_numeral complex_cnj_zero_iff csqrt_eq_0 csqrt_exp_Ln exp_cnj) |
3108 by (simp add: csqrt_exp_Ln Ln_inverse exp_minus) |
|
3109 qed auto |
|
3110 |
|
3111 lemma cnj_csqrt: |
|
3112 assumes "z \<notin> \<real>\<^sub>\<le>\<^sub>0" |
|
3113 shows "cnj(csqrt z) = csqrt(cnj z)" |
|
3114 proof (cases "z=0") |
|
3115 case False |
|
3116 then show ?thesis |
|
3117 by (simp add: assms cnj_Ln csqrt_exp_Ln exp_cnj) |
|
3118 qed auto |
|
3119 |
3027 |
3120 lemma has_field_derivative_csqrt: |
3028 lemma has_field_derivative_csqrt: |
3121 assumes "z \<notin> \<real>\<^sub>\<le>\<^sub>0" |
3029 assumes "z \<notin> \<real>\<^sub>\<le>\<^sub>0" |
3122 shows "(csqrt has_field_derivative inverse(2 * csqrt z)) (at z)" |
3030 shows "(csqrt has_field_derivative inverse(2 * csqrt z)) (at z)" |
3123 proof - |
3031 proof - |
3173 |
3081 |
3174 lemma continuous_within_csqrt_posreal: |
3082 lemma continuous_within_csqrt_posreal: |
3175 "continuous (at z within (\<real> \<inter> {w. 0 \<le> Re(w)})) csqrt" |
3083 "continuous (at z within (\<real> \<inter> {w. 0 \<le> Re(w)})) csqrt" |
3176 proof (cases "z \<in> \<real>\<^sub>\<le>\<^sub>0") |
3084 proof (cases "z \<in> \<real>\<^sub>\<le>\<^sub>0") |
3177 case True |
3085 case True |
3178 have [simp]: "Im z = 0" and 0: "Re z < 0 \<or> z = 0" |
3086 then have [simp]: "Im z = 0" and 0: "Re z < 0 \<or> z = 0" |
3179 using True cnj.code complex_cnj_zero_iff by (auto simp: Complex_eq complex_nonpos_Reals_iff) fastforce |
3087 using complex_nonpos_Reals_iff complex_eq_iff by force+ |
3180 show ?thesis |
3088 show ?thesis |
3181 using 0 |
3089 using 0 |
3182 proof |
3090 proof |
3183 assume "Re z < 0" |
3091 assume "Re z < 0" |
3184 then show ?thesis |
3092 then show ?thesis |
3294 by (metis Im_complex_div_lemma Re_complex_div_lemma cmod_eq_Im divide_complex_def |
3202 by (metis Im_complex_div_lemma Re_complex_div_lemma cmod_eq_Im divide_complex_def |
3295 less_irrefl mult_zero_right zero_complex.simps(1) zero_complex.simps(2)) |
3203 less_irrefl mult_zero_right zero_complex.simps(1) zero_complex.simps(2)) |
3296 have nzi: "((1 - \<i>*z) * inverse (1 + \<i>*z)) \<noteq> 0" |
3204 have nzi: "((1 - \<i>*z) * inverse (1 + \<i>*z)) \<noteq> 0" |
3297 using nz1 nz2 by auto |
3205 using nz1 nz2 by auto |
3298 have "Im ((1 - \<i>*z) / (1 + \<i>*z)) = 0 \<Longrightarrow> 0 < Re ((1 - \<i>*z) / (1 + \<i>*z))" |
3206 have "Im ((1 - \<i>*z) / (1 + \<i>*z)) = 0 \<Longrightarrow> 0 < Re ((1 - \<i>*z) / (1 + \<i>*z))" |
3299 apply (simp add: divide_complex_def) |
3207 by (simp add: Im_complex_div_lemma Re_complex_div_lemma assms cmod_eq_Im) |
3300 apply (simp add: divide_simps split: if_split_asm) |
|
3301 using assms |
|
3302 apply (auto simp: algebra_simps abs_square_less_1 [unfolded power2_eq_square]) |
|
3303 done |
|
3304 then have *: "((1 - \<i>*z) / (1 + \<i>*z)) \<notin> \<real>\<^sub>\<le>\<^sub>0" |
3208 then have *: "((1 - \<i>*z) / (1 + \<i>*z)) \<notin> \<real>\<^sub>\<le>\<^sub>0" |
3305 by (auto simp add: complex_nonpos_Reals_iff) |
3209 by (auto simp add: complex_nonpos_Reals_iff) |
3306 show "\<bar>Re(Arctan z)\<bar> < pi/2" |
3210 show "\<bar>Re(Arctan z)\<bar> < pi/2" |
3307 unfolding Arctan_def divide_complex_def |
3211 unfolding Arctan_def divide_complex_def |
3308 using mpi_less_Im_Ln [OF nzi] |
3212 using mpi_less_Im_Ln [OF nzi] |
3481 have "tan (Re (Arctan (of_real x))) = Re (tan (Arctan (of_real x)))" |
3385 have "tan (Re (Arctan (of_real x))) = Re (tan (Arctan (of_real x)))" |
3482 by (auto simp: tan_def Complex.Re_divide Re_sin Re_cos Im_sin Im_cos field_simps power2_eq_square) |
3386 by (auto simp: tan_def Complex.Re_divide Re_sin Re_cos Im_sin Im_cos field_simps power2_eq_square) |
3483 also have "\<dots> = x" |
3387 also have "\<dots> = x" |
3484 proof - |
3388 proof - |
3485 have "(complex_of_real x)\<^sup>2 \<noteq> - 1" |
3389 have "(complex_of_real x)\<^sup>2 \<noteq> - 1" |
3486 by (metis diff_0_right minus_diff_eq mult_zero_left not_le of_real_1 of_real_eq_iff of_real_minus of_real_power power2_eq_square real_minus_mult_self_le zero_less_one) |
3390 by (smt (verit, best) Im_complex_of_real imaginary_unit.sel(2) of_real_minus power2_eq_iff power2_i) |
3487 then show ?thesis |
3391 then show ?thesis |
3488 by simp |
3392 by simp |
3489 qed |
3393 qed |
3490 finally show "tan (Re (Arctan (complex_of_real x))) = x" . |
3394 finally show "tan (Re (Arctan (complex_of_real x))) = x" . |
3491 qed |
3395 qed |
3524 using cos_gt_zero_pi [OF 12] |
3428 using cos_gt_zero_pi [OF 12] |
3525 by (simp add: arctan tan_add) |
3429 by (simp add: arctan tan_add) |
3526 qed |
3430 qed |
3527 |
3431 |
3528 lemma arctan_inverse: |
3432 lemma arctan_inverse: |
3529 assumes "0 < x" |
3433 "0 < x \<Longrightarrow>arctan(inverse x) = pi/2 - arctan x" |
3530 shows "arctan(inverse x) = pi/2 - arctan x" |
3434 by (smt (verit, del_insts) arctan arctan_unique tan_cot zero_less_arctan_iff) |
3531 proof - |
|
3532 have "arctan(inverse x) = arctan(inverse(tan(arctan x)))" |
|
3533 by (simp add: arctan) |
|
3534 also have "\<dots> = arctan (tan (pi / 2 - arctan x))" |
|
3535 by (simp add: tan_cot) |
|
3536 also have "\<dots> = pi/2 - arctan x" |
|
3537 proof - |
|
3538 have "0 < pi - arctan x" |
|
3539 using arctan_ubound [of x] pi_gt_zero by linarith |
|
3540 with assms show ?thesis |
|
3541 by (simp add: Transcendental.arctan_tan) |
|
3542 qed |
|
3543 finally show ?thesis . |
|
3544 qed |
|
3545 |
3435 |
3546 lemma arctan_add_small: |
3436 lemma arctan_add_small: |
3547 assumes "\<bar>x * y\<bar> < 1" |
3437 assumes "\<bar>x * y\<bar> < 1" |
3548 shows "(arctan x + arctan y = arctan((x + y) / (1 - x * y)))" |
3438 shows "(arctan x + arctan y = arctan((x + y) / (1 - x * y)))" |
3549 proof (cases "x = 0 \<or> y = 0") |
3439 proof (cases "x = 0 \<or> y = 0") |
3588 have tendsto_zero: "?a \<longlonglongrightarrow> 0" |
3478 have tendsto_zero: "?a \<longlonglongrightarrow> 0" |
3589 proof (rule tendsto_eq_rhs) |
3479 proof (rule tendsto_eq_rhs) |
3590 show "(\<lambda>k. 1 / real (k * 2 + 1) * x ^ (k * 2 + 1)) \<longlonglongrightarrow> 0 * 0" |
3480 show "(\<lambda>k. 1 / real (k * 2 + 1) * x ^ (k * 2 + 1)) \<longlonglongrightarrow> 0 * 0" |
3591 using assms |
3481 using assms |
3592 by (intro tendsto_mult real_tendsto_divide_at_top) |
3482 by (intro tendsto_mult real_tendsto_divide_at_top) |
3593 (auto simp: filterlim_real_sequentially filterlim_sequentially_iff_filterlim_real |
3483 (auto simp: filterlim_sequentially_iff_filterlim_real |
3594 intro!: real_tendsto_divide_at_top tendsto_power_zero filterlim_real_sequentially |
3484 intro!: real_tendsto_divide_at_top tendsto_power_zero filterlim_real_sequentially |
3595 tendsto_eq_intros filterlim_at_top_mult_tendsto_pos filterlim_tendsto_add_at_top) |
3485 tendsto_eq_intros filterlim_at_top_mult_tendsto_pos filterlim_tendsto_add_at_top) |
3596 qed simp |
3486 qed simp |
3597 have nonneg: "0 \<le> ?a n" for n |
3487 have nonneg: "0 \<le> ?a n" for n |
3598 by (force intro!: divide_nonneg_nonneg mult_nonneg_nonneg zero_le_power assms) |
3488 by (force intro!: divide_nonneg_nonneg mult_nonneg_nonneg zero_le_power assms) |
3703 moreover have "\<dots> \<longleftrightarrow> (\<i>*z) + csqrt (1 - z\<^sup>2) = 0" |
3593 moreover have "\<dots> \<longleftrightarrow> (\<i>*z) + csqrt (1 - z\<^sup>2) = 0" |
3704 by (metis Arcsin_body_lemma distrib_right no_zero_divisors zero_neq_numeral) |
3594 by (metis Arcsin_body_lemma distrib_right no_zero_divisors zero_neq_numeral) |
3705 ultimately show ?thesis |
3595 ultimately show ?thesis |
3706 apply (simp add: sin_exp_eq Arcsin_def Arcsin_body_lemma exp_minus divide_simps) |
3596 apply (simp add: sin_exp_eq Arcsin_def Arcsin_body_lemma exp_minus divide_simps) |
3707 apply (simp add: algebra_simps) |
3597 apply (simp add: algebra_simps) |
3708 apply (simp add: power2_eq_square [symmetric] algebra_simps) |
3598 apply (simp add: right_diff_distrib flip: power2_eq_square) |
3709 done |
3599 done |
3710 qed |
3600 qed |
3711 |
3601 |
3712 lemma Re_eq_pihalf_lemma: |
3602 lemma Re_eq_pihalf_lemma: |
3713 "\<bar>Re z\<bar> = pi/2 \<Longrightarrow> Im z = 0 \<Longrightarrow> |
3603 "\<bar>Re z\<bar> = pi/2 \<Longrightarrow> Im z = 0 \<Longrightarrow> |
3746 lemma Arcsin_unique: |
3636 lemma Arcsin_unique: |
3747 "\<lbrakk>sin z = w; \<bar>Re z\<bar> < pi/2 \<or> (\<bar>Re z\<bar> = pi/2 \<and> Im z = 0)\<rbrakk> \<Longrightarrow> Arcsin w = z" |
3637 "\<lbrakk>sin z = w; \<bar>Re z\<bar> < pi/2 \<or> (\<bar>Re z\<bar> = pi/2 \<and> Im z = 0)\<rbrakk> \<Longrightarrow> Arcsin w = z" |
3748 by (metis Arcsin_sin) |
3638 by (metis Arcsin_sin) |
3749 |
3639 |
3750 lemma Arcsin_0 [simp]: "Arcsin 0 = 0" |
3640 lemma Arcsin_0 [simp]: "Arcsin 0 = 0" |
3751 by (metis Arcsin_sin norm_zero pi_half_gt_zero real_norm_def sin_zero zero_complex.simps(1)) |
3641 by (simp add: Arcsin_unique) |
3752 |
3642 |
3753 lemma Arcsin_1 [simp]: "Arcsin 1 = pi/2" |
3643 lemma Arcsin_1 [simp]: "Arcsin 1 = pi/2" |
3754 by (metis Arcsin_sin Im_complex_of_real Re_complex_of_real numeral_One of_real_numeral pi_half_ge_zero real_sqrt_abs real_sqrt_pow2 real_sqrt_power sin_of_real sin_pi_half) |
3644 using Arcsin_unique sin_of_real_pi_half by fastforce |
3755 |
3645 |
3756 lemma Arcsin_minus_1 [simp]: "Arcsin(-1) = - (pi/2)" |
3646 lemma Arcsin_minus_1 [simp]: "Arcsin(-1) = - (pi/2)" |
3757 by (metis Arcsin_1 Arcsin_sin Im_complex_of_real Re_complex_of_real abs_of_nonneg of_real_minus pi_half_ge_zero power2_minus real_sqrt_abs sin_Arcsin sin_minus) |
3647 by (simp add: Arcsin_unique) |
3758 |
3648 |
3759 lemma has_field_derivative_Arcsin: |
3649 lemma has_field_derivative_Arcsin: |
3760 assumes "Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1" |
3650 assumes "Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1" |
3761 shows "(Arcsin has_field_derivative inverse(cos(Arcsin z))) (at z)" |
3651 shows "(Arcsin has_field_derivative inverse(cos(Arcsin z))) (at z)" |
3762 proof - |
3652 proof - |
3798 |
3688 |
3799 lemma Arccos_range_lemma: "\<bar>Re z\<bar> < 1 \<Longrightarrow> 0 < Im(z + \<i> * csqrt(1 - z\<^sup>2))" |
3689 lemma Arccos_range_lemma: "\<bar>Re z\<bar> < 1 \<Longrightarrow> 0 < Im(z + \<i> * csqrt(1 - z\<^sup>2))" |
3800 using Arcsin_range_lemma [of "-z"] by simp |
3690 using Arcsin_range_lemma [of "-z"] by simp |
3801 |
3691 |
3802 lemma Arccos_body_lemma: "z + \<i> * csqrt(1 - z\<^sup>2) \<noteq> 0" |
3692 lemma Arccos_body_lemma: "z + \<i> * csqrt(1 - z\<^sup>2) \<noteq> 0" |
3803 using Arcsin_body_lemma [of z] |
3693 by (metis Arcsin_body_lemma complex_i_mult_minus diff_0 diff_eq_eq power2_minus) |
3804 by (metis Arcsin_body_lemma complex_i_mult_minus diff_minus_eq_add power2_minus right_minus_eq) |
|
3805 |
3694 |
3806 lemma Re_Arccos: "Re(Arccos z) = Im (Ln (z + \<i> * csqrt(1 - z\<^sup>2)))" |
3695 lemma Re_Arccos: "Re(Arccos z) = Im (Ln (z + \<i> * csqrt(1 - z\<^sup>2)))" |
3807 by (simp add: Arccos_def) |
3696 by (simp add: Arccos_def) |
3808 |
3697 |
3809 lemma Im_Arccos: "Im(Arccos z) = - ln (cmod (z + \<i> * csqrt (1 - z\<^sup>2)))" |
3698 lemma Im_Arccos: "Im(Arccos z) = - ln (cmod (z + \<i> * csqrt (1 - z\<^sup>2)))" |
3810 by (simp add: Arccos_def Arccos_body_lemma) |
3699 by (simp add: Arccos_def Arccos_body_lemma) |
3811 |
3700 |
3812 text\<open>A very tricky argument to find!\<close> |
3701 text\<open>A very tricky argument to find!\<close> |
3813 lemma isCont_Arccos_lemma: |
3702 lemma isCont_Arccos_lemma: |
3814 assumes eq0: "Im (z + \<i> * csqrt (1 - z\<^sup>2)) = 0" and "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1)" |
3703 assumes eq0: "Im (z + \<i> * csqrt (1 - z\<^sup>2)) = 0" and "Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1" |
3815 shows False |
3704 shows False |
3816 proof (cases "Im z = 0") |
3705 proof (cases "Im z = 0") |
3817 case True |
3706 case True |
3818 then show ?thesis |
3707 then show ?thesis |
3819 using assms by (fastforce simp add: cmod_def abs_square_less_1 [symmetric]) |
3708 using assms by (fastforce simp add: cmod_def abs_square_less_1 [symmetric]) |
3985 have Re: "(Re (Arccos w))\<^sup>2 \<le> pi\<^sup>2" "(Im (Arccos w))\<^sup>2 \<le> (cmod w)\<^sup>2" |
3874 have Re: "(Re (Arccos w))\<^sup>2 \<le> pi\<^sup>2" "(Im (Arccos w))\<^sup>2 \<le> (cmod w)\<^sup>2" |
3986 using Re_Arccos_bound [of w] Im_Arccos_bound [of w] abs_le_square_iff by force+ |
3875 using Re_Arccos_bound [of w] Im_Arccos_bound [of w] abs_le_square_iff by force+ |
3987 have "Arccos w \<bullet> Arccos w \<le> pi\<^sup>2 + (cmod w)\<^sup>2" |
3876 have "Arccos w \<bullet> Arccos w \<le> pi\<^sup>2 + (cmod w)\<^sup>2" |
3988 using Re by (simp add: dot_square_norm cmod_power2 [of "Arccos w"]) |
3877 using Re by (simp add: dot_square_norm cmod_power2 [of "Arccos w"]) |
3989 then have "cmod (Arccos w) \<le> pi + cmod (cos (Arccos w))" |
3878 then have "cmod (Arccos w) \<le> pi + cmod (cos (Arccos w))" |
3990 apply (simp add: norm_le_square) |
3879 by (smt (verit) Im_Arccos_bound Re_Arccos_bound cmod_le cos_Arccos) |
3991 by (metis dot_square_norm norm_ge_zero norm_le_square pi_ge_zero triangle_lemma) |
|
3992 then show "cmod (Arccos w) \<le> pi + cmod w" |
3880 then show "cmod (Arccos w) \<le> pi + cmod w" |
3993 by auto |
3881 by auto |
3994 qed |
3882 qed |
3995 |
3883 |
3996 |
3884 |
3997 subsection\<^marker>\<open>tag unimportant\<close>\<open>Interrelations between Arcsin and Arccos\<close> |
3885 subsection\<^marker>\<open>tag unimportant\<close>\<open>Interrelations between Arcsin and Arccos\<close> |
3998 |
3886 |
3999 lemma cos_Arcsin_nonzero: |
3887 lemma cos_Arcsin_nonzero: "z\<^sup>2 \<noteq> 1 \<Longrightarrow>cos(Arcsin z) \<noteq> 0" |
4000 assumes "z\<^sup>2 \<noteq> 1" shows "cos(Arcsin z) \<noteq> 0" |
3888 by (metis diff_0_right power_zero_numeral sin_Arcsin sin_squared_eq) |
4001 proof - |
3889 |
4002 have eq: "(\<i> * z * (csqrt (1 - z\<^sup>2)))\<^sup>2 = z\<^sup>2 * (z\<^sup>2 - 1)" |
3890 lemma sin_Arccos_nonzero: "z\<^sup>2 \<noteq> 1 \<Longrightarrow>sin(Arccos z) \<noteq> 0" |
4003 by (simp add: algebra_simps) |
3891 by (metis add.right_neutral cos_Arccos power2_eq_square power_zero_numeral sin_cos_squared_add3) |
4004 have "\<i> * z * (csqrt (1 - z\<^sup>2)) \<noteq> z\<^sup>2 - 1" |
|
4005 proof |
|
4006 assume "\<i> * z * (csqrt (1 - z\<^sup>2)) = z\<^sup>2 - 1" |
|
4007 then have "(\<i> * z * (csqrt (1 - z\<^sup>2)))\<^sup>2 = (z\<^sup>2 - 1)\<^sup>2" |
|
4008 by simp |
|
4009 then have "z\<^sup>2 * (z\<^sup>2 - 1) = (z\<^sup>2 - 1)*(z\<^sup>2 - 1)" |
|
4010 using eq power2_eq_square by auto |
|
4011 then show False |
|
4012 using assms by simp |
|
4013 qed |
|
4014 then have "1 + \<i> * z * (csqrt (1 - z * z)) \<noteq> z\<^sup>2" |
|
4015 by (metis add_minus_cancel power2_eq_square uminus_add_conv_diff) |
|
4016 then have "2*(1 + \<i> * z * (csqrt (1 - z * z))) \<noteq> 2*z\<^sup>2" (*FIXME cancel_numeral_factor*) |
|
4017 by (metis mult_cancel_left zero_neq_numeral) |
|
4018 then have "(\<i> * z + csqrt (1 - z\<^sup>2))\<^sup>2 \<noteq> -1" |
|
4019 using assms |
|
4020 apply (simp add: power2_sum) |
|
4021 apply (simp add: power2_eq_square algebra_simps) |
|
4022 done |
|
4023 then show ?thesis |
|
4024 apply (simp add: cos_exp_eq Arcsin_def exp_minus) |
|
4025 apply (simp add: divide_simps Arcsin_body_lemma) |
|
4026 apply (metis add.commute minus_unique power2_eq_square) |
|
4027 done |
|
4028 qed |
|
4029 |
|
4030 lemma sin_Arccos_nonzero: |
|
4031 assumes "z\<^sup>2 \<noteq> 1" shows "sin(Arccos z) \<noteq> 0" |
|
4032 proof - |
|
4033 have eq: "(\<i> * z * (csqrt (1 - z\<^sup>2)))\<^sup>2 = -(z\<^sup>2) * (1 - z\<^sup>2)" |
|
4034 by (simp add: algebra_simps) |
|
4035 have "\<i> * z * (csqrt (1 - z\<^sup>2)) \<noteq> 1 - z\<^sup>2" |
|
4036 proof |
|
4037 assume "\<i> * z * (csqrt (1 - z\<^sup>2)) = 1 - z\<^sup>2" |
|
4038 then have "(\<i> * z * (csqrt (1 - z\<^sup>2)))\<^sup>2 = (1 - z\<^sup>2)\<^sup>2" |
|
4039 by simp |
|
4040 then have "-(z\<^sup>2) * (1 - z\<^sup>2) = (1 - z\<^sup>2)*(1 - z\<^sup>2)" |
|
4041 using eq power2_eq_square by auto |
|
4042 then have "-(z\<^sup>2) = (1 - z\<^sup>2)" |
|
4043 using assms |
|
4044 by (metis add.commute add.right_neutral diff_add_cancel mult_right_cancel) |
|
4045 then show False |
|
4046 using assms by simp |
|
4047 qed |
|
4048 then have "z\<^sup>2 + \<i> * z * (csqrt (1 - z\<^sup>2)) \<noteq> 1" |
|
4049 by (simp add: algebra_simps) |
|
4050 then have "2*(z\<^sup>2 + \<i> * z * (csqrt (1 - z\<^sup>2))) \<noteq> 2*1" |
|
4051 by (metis mult_cancel_left2 zero_neq_numeral) (*FIXME cancel_numeral_factor*) |
|
4052 then have "(z + \<i> * csqrt (1 - z\<^sup>2))\<^sup>2 \<noteq> 1" |
|
4053 using assms |
|
4054 by (metis Arccos_def add.commute add.left_neutral cancel_comm_monoid_add_class.diff_cancel cos_Arccos csqrt_0 mult_zero_right) |
|
4055 then show ?thesis |
|
4056 apply (simp add: sin_exp_eq Arccos_def exp_minus) |
|
4057 apply (simp add: divide_simps Arccos_body_lemma) |
|
4058 apply (simp add: power2_eq_square) |
|
4059 done |
|
4060 qed |
|
4061 |
3892 |
4062 lemma cos_sin_csqrt: |
3893 lemma cos_sin_csqrt: |
4063 assumes "0 < cos(Re z) \<or> cos(Re z) = 0 \<and> Im z * sin(Re z) \<le> 0" |
3894 assumes "0 < cos(Re z) \<or> cos(Re z) = 0 \<and> Im z * sin(Re z) \<le> 0" |
4064 shows "cos z = csqrt(1 - (sin z)\<^sup>2)" |
3895 shows "cos z = csqrt(1 - (sin z)\<^sup>2)" |
4065 proof (rule csqrt_unique [THEN sym]) |
3896 proof (rule csqrt_unique [THEN sym]) |
4074 show "(sin z)\<^sup>2 = 1 - (cos z)\<^sup>2" |
3905 show "(sin z)\<^sup>2 = 1 - (cos z)\<^sup>2" |
4075 by (simp add: sin_squared_eq) |
3906 by (simp add: sin_squared_eq) |
4076 qed (use assms in \<open>auto simp: Re_sin Im_sin add_pos_pos mult_le_0_iff zero_le_mult_iff\<close>) |
3907 qed (use assms in \<open>auto simp: Re_sin Im_sin add_pos_pos mult_le_0_iff zero_le_mult_iff\<close>) |
4077 |
3908 |
4078 lemma Arcsin_Arccos_csqrt_pos: |
3909 lemma Arcsin_Arccos_csqrt_pos: |
4079 "(0 < Re z | Re z = 0 & 0 \<le> Im z) \<Longrightarrow> Arcsin z = Arccos(csqrt(1 - z\<^sup>2))" |
3910 "(0 < Re z \<or> Re z = 0 \<and> 0 \<le> Im z) \<Longrightarrow> Arcsin z = Arccos(csqrt(1 - z\<^sup>2))" |
4080 by (simp add: Arcsin_def Arccos_def Complex.csqrt_square add.commute) |
3911 by (simp add: Arcsin_def Arccos_def Complex.csqrt_square add.commute) |
4081 |
3912 |
4082 lemma Arccos_Arcsin_csqrt_pos: |
3913 lemma Arccos_Arcsin_csqrt_pos: |
4083 "(0 < Re z | Re z = 0 & 0 \<le> Im z) \<Longrightarrow> Arccos z = Arcsin(csqrt(1 - z\<^sup>2))" |
3914 "(0 < Re z \<or> Re z = 0 \<and> 0 \<le> Im z) \<Longrightarrow> Arccos z = Arcsin(csqrt(1 - z\<^sup>2))" |
4084 by (simp add: Arcsin_def Arccos_def Complex.csqrt_square add.commute) |
3915 by (simp add: Arcsin_def Arccos_def Complex.csqrt_square add.commute) |
4085 |
3916 |
4086 lemma sin_Arccos: |
3917 lemma sin_Arccos: |
4087 "0 < Re z | Re z = 0 & 0 \<le> Im z \<Longrightarrow> sin(Arccos z) = csqrt(1 - z\<^sup>2)" |
3918 "0 < Re z \<or> Re z = 0 \<and> 0 \<le> Im z \<Longrightarrow> sin(Arccos z) = csqrt(1 - z\<^sup>2)" |
4088 by (simp add: Arccos_Arcsin_csqrt_pos) |
3919 by (simp add: Arccos_Arcsin_csqrt_pos) |
4089 |
3920 |
4090 lemma cos_Arcsin: |
3921 lemma cos_Arcsin: |
4091 "0 < Re z | Re z = 0 & 0 \<le> Im z \<Longrightarrow> cos(Arcsin z) = csqrt(1 - z\<^sup>2)" |
3922 "0 < Re z \<or> Re z = 0 \<and> 0 \<le> Im z \<Longrightarrow> cos(Arcsin z) = csqrt(1 - z\<^sup>2)" |
4092 by (simp add: Arcsin_Arccos_csqrt_pos) |
3923 by (simp add: Arcsin_Arccos_csqrt_pos) |
4093 |
3924 |
4094 |
3925 |
4095 subsection\<^marker>\<open>tag unimportant\<close>\<open>Relationship with Arcsin on the Real Numbers\<close> |
3926 subsection\<^marker>\<open>tag unimportant\<close>\<open>Relationship with Arcsin on the Real Numbers\<close> |
4096 |
3927 |
4097 lemma Im_Arcsin_of_real: |
3928 lemma of_real_arcsin: "\<bar>x\<bar> \<le> 1 \<Longrightarrow> of_real(arcsin x) = Arcsin(of_real x)" |
4098 assumes "\<bar>x\<bar> \<le> 1" |
3929 by (smt (verit, best) Arcsin_sin Im_complex_of_real Re_complex_of_real arcsin sin_of_real) |
4099 shows "Im (Arcsin (of_real x)) = 0" |
3930 |
4100 proof - |
3931 lemma Im_Arcsin_of_real: "\<bar>x\<bar> \<le> 1 \<Longrightarrow> Im (Arcsin (of_real x)) = 0" |
4101 have "csqrt (1 - (of_real x)\<^sup>2) = (if x^2 \<le> 1 then sqrt (1 - x^2) else \<i> * sqrt (x^2 - 1))" |
3932 by (metis Im_complex_of_real of_real_arcsin) |
4102 by (simp add: of_real_sqrt del: csqrt_of_real_nonneg) |
|
4103 then have "cmod (\<i> * of_real x + csqrt (1 - (of_real x)\<^sup>2))^2 = 1" |
|
4104 using assms abs_square_le_1 |
|
4105 by (force simp add: Complex.cmod_power2) |
|
4106 then have "cmod (\<i> * of_real x + csqrt (1 - (of_real x)\<^sup>2)) = 1" |
|
4107 by (simp add: norm_complex_def) |
|
4108 then show ?thesis |
|
4109 by (simp add: Im_Arcsin exp_minus) |
|
4110 qed |
|
4111 |
3933 |
4112 corollary\<^marker>\<open>tag unimportant\<close> Arcsin_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> \<bar>Re z\<bar> \<le> 1 \<Longrightarrow> Arcsin z \<in> \<real>" |
3934 corollary\<^marker>\<open>tag unimportant\<close> Arcsin_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> \<bar>Re z\<bar> \<le> 1 \<Longrightarrow> Arcsin z \<in> \<real>" |
4113 by (metis Im_Arcsin_of_real Re_complex_of_real Reals_cases complex_is_Real_iff) |
3935 by (metis Im_Arcsin_of_real Re_complex_of_real Reals_cases complex_is_Real_iff) |
4114 |
3936 |
4115 lemma arcsin_eq_Re_Arcsin: |
3937 lemma arcsin_eq_Re_Arcsin: "\<bar>x\<bar> \<le> 1 \<Longrightarrow> arcsin x = Re (Arcsin (of_real x))" |
4116 assumes "\<bar>x\<bar> \<le> 1" |
3938 by (metis Re_complex_of_real of_real_arcsin) |
4117 shows "arcsin x = Re (Arcsin (of_real x))" |
|
4118 unfolding arcsin_def |
|
4119 proof (rule the_equality, safe) |
|
4120 show "- (pi / 2) \<le> Re (Arcsin (complex_of_real x))" |
|
4121 using Re_Ln_pos_le [OF Arcsin_body_lemma, of "of_real x"] |
|
4122 by (auto simp: Complex.in_Reals_norm Re_Arcsin) |
|
4123 next |
|
4124 show "Re (Arcsin (complex_of_real x)) \<le> pi / 2" |
|
4125 using Re_Ln_pos_le [OF Arcsin_body_lemma, of "of_real x"] |
|
4126 by (auto simp: Complex.in_Reals_norm Re_Arcsin) |
|
4127 next |
|
4128 show "sin (Re (Arcsin (complex_of_real x))) = x" |
|
4129 using Re_sin [of "Arcsin (of_real x)"] Arcsin_body_lemma [of "of_real x"] |
|
4130 by (simp add: Im_Arcsin_of_real assms) |
|
4131 next |
|
4132 fix x' |
|
4133 assume "- (pi / 2) \<le> x'" "x' \<le> pi / 2" "x = sin x'" |
|
4134 then show "x' = Re (Arcsin (complex_of_real (sin x')))" |
|
4135 unfolding sin_of_real [symmetric] |
|
4136 by (subst Arcsin_sin) auto |
|
4137 qed |
|
4138 |
|
4139 lemma of_real_arcsin: "\<bar>x\<bar> \<le> 1 \<Longrightarrow> of_real(arcsin x) = Arcsin(of_real x)" |
|
4140 by (metis Im_Arcsin_of_real add.right_neutral arcsin_eq_Re_Arcsin complex_eq mult_zero_right of_real_0) |
|
4141 |
3939 |
4142 |
3940 |
4143 subsection\<^marker>\<open>tag unimportant\<close>\<open>Relationship with Arccos on the Real Numbers\<close> |
3941 subsection\<^marker>\<open>tag unimportant\<close>\<open>Relationship with Arccos on the Real Numbers\<close> |
4144 |
3942 |
4145 lemma Im_Arccos_of_real: |
3943 lemma of_real_arccos: "\<bar>x\<bar> \<le> 1 \<Longrightarrow> of_real(arccos x) = Arccos(of_real x)" |
4146 assumes "\<bar>x\<bar> \<le> 1" |
3944 by (smt (verit, del_insts) Arccos_unique Im_complex_of_real Re_complex_of_real arccos_lbound |
4147 shows "Im (Arccos (of_real x)) = 0" |
3945 arccos_ubound cos_arccos_abs cos_of_real) |
4148 proof - |
3946 |
4149 have "csqrt (1 - (of_real x)\<^sup>2) = (if x^2 \<le> 1 then sqrt (1 - x^2) else \<i> * sqrt (x^2 - 1))" |
3947 lemma Im_Arccos_of_real: "\<bar>x\<bar> \<le> 1 \<Longrightarrow> Im (Arccos (of_real x)) = 0" |
4150 by (simp add: of_real_sqrt del: csqrt_of_real_nonneg) |
3948 by (metis Im_complex_of_real of_real_arccos) |
4151 then have "cmod (of_real x + \<i> * csqrt (1 - (of_real x)\<^sup>2))^2 = 1" |
|
4152 using assms abs_square_le_1 |
|
4153 by (force simp add: Complex.cmod_power2) |
|
4154 then have "cmod (of_real x + \<i> * csqrt (1 - (of_real x)\<^sup>2)) = 1" |
|
4155 by (simp add: norm_complex_def) |
|
4156 then show ?thesis |
|
4157 by (simp add: Im_Arccos exp_minus) |
|
4158 qed |
|
4159 |
3949 |
4160 corollary\<^marker>\<open>tag unimportant\<close> Arccos_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> \<bar>Re z\<bar> \<le> 1 \<Longrightarrow> Arccos z \<in> \<real>" |
3950 corollary\<^marker>\<open>tag unimportant\<close> Arccos_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> \<bar>Re z\<bar> \<le> 1 \<Longrightarrow> Arccos z \<in> \<real>" |
4161 by (metis Im_Arccos_of_real Re_complex_of_real Reals_cases complex_is_Real_iff) |
3951 by (metis Im_Arccos_of_real complex_is_Real_iff of_real_Re) |
4162 |
3952 |
4163 lemma arccos_eq_Re_Arccos: |
3953 lemma arccos_eq_Re_Arccos: "\<bar>x\<bar> \<le> 1 \<Longrightarrow> arccos x = Re (Arccos (of_real x))" |
4164 assumes "\<bar>x\<bar> \<le> 1" |
3954 by (metis Re_complex_of_real of_real_arccos) |
4165 shows "arccos x = Re (Arccos (of_real x))" |
|
4166 unfolding arccos_def |
|
4167 proof (rule the_equality, safe) |
|
4168 show "0 \<le> Re (Arccos (complex_of_real x))" |
|
4169 using Im_Ln_pos_le [OF Arccos_body_lemma, of "of_real x"] |
|
4170 by (auto simp: Complex.in_Reals_norm Re_Arccos) |
|
4171 next |
|
4172 show "Re (Arccos (complex_of_real x)) \<le> pi" |
|
4173 using Im_Ln_pos_le [OF Arccos_body_lemma, of "of_real x"] |
|
4174 by (auto simp: Complex.in_Reals_norm Re_Arccos) |
|
4175 next |
|
4176 show "cos (Re (Arccos (complex_of_real x))) = x" |
|
4177 using Re_cos [of "Arccos (of_real x)"] Arccos_body_lemma [of "of_real x"] |
|
4178 by (simp add: Im_Arccos_of_real assms) |
|
4179 next |
|
4180 fix x' |
|
4181 assume "0 \<le> x'" "x' \<le> pi" "x = cos x'" |
|
4182 then show "x' = Re (Arccos (complex_of_real (cos x')))" |
|
4183 unfolding cos_of_real [symmetric] |
|
4184 by (subst Arccos_cos) auto |
|
4185 qed |
|
4186 |
|
4187 lemma of_real_arccos: "\<bar>x\<bar> \<le> 1 \<Longrightarrow> of_real(arccos x) = Arccos(of_real x)" |
|
4188 by (metis Im_Arccos_of_real add.right_neutral arccos_eq_Re_Arccos complex_eq mult_zero_right of_real_0) |
|
4189 |
|
4190 subsection\<^marker>\<open>tag unimportant\<close>\<open>Some interrelationships among the real inverse trig functions\<close> |
|
4191 |
|
4192 lemma arccos_arctan: |
|
4193 assumes "-1 < x" "x < 1" |
|
4194 shows "arccos x = pi/2 - arctan(x / sqrt(1 - x\<^sup>2))" |
|
4195 proof - |
|
4196 have "arctan(x / sqrt(1 - x\<^sup>2)) - (pi/2 - arccos x) = 0" |
|
4197 proof (rule sin_eq_0_pi) |
|
4198 show "- pi < arctan (x / sqrt (1 - x\<^sup>2)) - (pi / 2 - arccos x)" |
|
4199 using arctan_lbound [of "x / sqrt(1 - x\<^sup>2)"] arccos_bounded [of x] assms |
|
4200 by (simp add: algebra_simps) |
|
4201 next |
|
4202 show "arctan (x / sqrt (1 - x\<^sup>2)) - (pi / 2 - arccos x) < pi" |
|
4203 using arctan_ubound [of "x / sqrt(1 - x\<^sup>2)"] arccos_bounded [of x] assms |
|
4204 by (simp add: algebra_simps) |
|
4205 next |
|
4206 show "sin (arctan (x / sqrt (1 - x\<^sup>2)) - (pi / 2 - arccos x)) = 0" |
|
4207 using assms |
|
4208 by (simp add: algebra_simps sin_diff cos_add sin_arccos sin_arctan cos_arctan |
|
4209 power2_eq_square square_eq_1_iff) |
|
4210 qed |
|
4211 then show ?thesis |
|
4212 by simp |
|
4213 qed |
|
4214 |
|
4215 lemma arcsin_plus_arccos: |
|
4216 assumes "-1 \<le> x" "x \<le> 1" |
|
4217 shows "arcsin x + arccos x = pi/2" |
|
4218 proof - |
|
4219 have "arcsin x = pi/2 - arccos x" |
|
4220 apply (rule sin_inj_pi) |
|
4221 using assms arcsin [OF assms] arccos [OF assms] |
|
4222 by (auto simp: algebra_simps sin_diff) |
|
4223 then show ?thesis |
|
4224 by (simp add: algebra_simps) |
|
4225 qed |
|
4226 |
|
4227 lemma arcsin_arccos_eq: "-1 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> arcsin x = pi/2 - arccos x" |
|
4228 using arcsin_plus_arccos by force |
|
4229 |
|
4230 lemma arccos_arcsin_eq: "-1 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> arccos x = pi/2 - arcsin x" |
|
4231 using arcsin_plus_arccos by force |
|
4232 |
|
4233 lemma arcsin_arctan: "-1 < x \<Longrightarrow> x < 1 \<Longrightarrow> arcsin x = arctan(x / sqrt(1 - x\<^sup>2))" |
|
4234 by (simp add: arccos_arctan arcsin_arccos_eq) |
|
4235 |
|
4236 lemma csqrt_1_diff_eq: "csqrt (1 - (of_real x)\<^sup>2) = (if x^2 \<le> 1 then sqrt (1 - x^2) else \<i> * sqrt (x^2 - 1))" |
|
4237 by ( simp add: of_real_sqrt del: csqrt_of_real_nonneg) |
|
4238 |
|
4239 lemma arcsin_arccos_sqrt_pos: "0 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> arcsin x = arccos(sqrt(1 - x\<^sup>2))" |
|
4240 apply (simp add: abs_square_le_1 arcsin_eq_Re_Arcsin arccos_eq_Re_Arccos) |
|
4241 apply (subst Arcsin_Arccos_csqrt_pos) |
|
4242 apply (auto simp: power_le_one csqrt_1_diff_eq) |
|
4243 done |
|
4244 |
|
4245 lemma arcsin_arccos_sqrt_neg: "-1 \<le> x \<Longrightarrow> x \<le> 0 \<Longrightarrow> arcsin x = -arccos(sqrt(1 - x\<^sup>2))" |
|
4246 using arcsin_arccos_sqrt_pos [of "-x"] |
|
4247 by (simp add: arcsin_minus) |
|
4248 |
|
4249 lemma arccos_arcsin_sqrt_pos: "0 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> arccos x = arcsin(sqrt(1 - x\<^sup>2))" |
|
4250 apply (simp add: abs_square_le_1 arcsin_eq_Re_Arcsin arccos_eq_Re_Arccos) |
|
4251 apply (subst Arccos_Arcsin_csqrt_pos) |
|
4252 apply (auto simp: power_le_one csqrt_1_diff_eq) |
|
4253 done |
|
4254 |
|
4255 lemma arccos_arcsin_sqrt_neg: "-1 \<le> x \<Longrightarrow> x \<le> 0 \<Longrightarrow> arccos x = pi - arcsin(sqrt(1 - x\<^sup>2))" |
|
4256 using arccos_arcsin_sqrt_pos [of "-x"] |
|
4257 by (simp add: arccos_minus) |
|
4258 |
3955 |
4259 subsection\<^marker>\<open>tag unimportant\<close>\<open>Continuity results for arcsin and arccos\<close> |
3956 subsection\<^marker>\<open>tag unimportant\<close>\<open>Continuity results for arcsin and arccos\<close> |
4260 |
3957 |
4261 lemma continuous_on_Arcsin_real [continuous_intros]: |
3958 lemma continuous_on_Arcsin_real [continuous_intros]: |
4262 "continuous_on {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1} Arcsin" |
3959 "continuous_on {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1} Arcsin" |