equal
deleted
inserted
replaced
851 by (rule Arg_unique [of "exp(Re z)"]) (auto simp: exp_eq_polar) |
851 by (rule Arg_unique [of "exp(Re z)"]) (auto simp: exp_eq_polar) |
852 |
852 |
853 lemma complex_split_polar: |
853 lemma complex_split_polar: |
854 obtains r a::real where "z = complex_of_real r * (cos a + \<i> * sin a)" "0 \<le> r" "0 \<le> a" "a < 2*pi" |
854 obtains r a::real where "z = complex_of_real r * (cos a + \<i> * sin a)" "0 \<le> r" "0 \<le> a" "a < 2*pi" |
855 using Arg cis.ctr cis_conv_exp by fastforce |
855 using Arg cis.ctr cis_conv_exp by fastforce |
|
856 |
|
857 lemma Re_Im_le_cmod: "Im w * sin \<phi> + Re w * cos \<phi> \<le> cmod w" |
|
858 proof (cases w rule: complex_split_polar) |
|
859 case (1 r a) with sin_cos_le1 [of a \<phi>] show ?thesis |
|
860 apply (simp add: norm_mult cmod_unit_one) |
|
861 by (metis (no_types, hide_lams) abs_le_D1 distrib_left mult.commute mult.left_commute mult_left_le) |
|
862 qed |
856 |
863 |
857 subsection\<open>Analytic properties of tangent function\<close> |
864 subsection\<open>Analytic properties of tangent function\<close> |
858 |
865 |
859 lemma cnj_tan: "cnj(tan z) = tan(cnj z)" |
866 lemma cnj_tan: "cnj(tan z) = tan(cnj z)" |
860 by (simp add: cnj_cos cnj_sin tan_def) |
867 by (simp add: cnj_cos cnj_sin tan_def) |