1776 finally show ?thesis . |
1776 finally show ?thesis . |
1777 qed |
1777 qed |
1778 |
1778 |
1779 subsection\<open>The Argument of a Complex Number\<close> |
1779 subsection\<open>The Argument of a Complex Number\<close> |
1780 |
1780 |
1781 text\<open>Finally: it's is defined for the same interval as the complex logarithm: \<open>(-\<pi>,\<pi>]\<close>.\<close> |
1781 text\<open>Unlike in HOL Light, it's defined for the same interval as the complex logarithm: \<open>(-\<pi>,\<pi>]\<close>.\<close> |
|
1782 |
|
1783 lemma Arg_eq_Im_Ln: |
|
1784 assumes "z \<noteq> 0" shows "arg z = Im (Ln z)" |
|
1785 proof (rule arg_unique) |
|
1786 show "sgn z = cis (Im (Ln z))" |
|
1787 by (metis assms exp_Ln exp_eq_polar nonzero_mult_div_cancel_left norm_eq_zero |
|
1788 norm_exp_eq_Re of_real_eq_0_iff sgn_eq) |
|
1789 show "- pi < Im (Ln z)" |
|
1790 by (simp add: assms mpi_less_Im_Ln) |
|
1791 show "Im (Ln z) \<le> pi" |
|
1792 by (simp add: Im_Ln_le_pi assms) |
|
1793 qed |
|
1794 |
|
1795 text \<open>The 1990s definition of argument coincides with the more recent one\<close> |
|
1796 lemma Arg_definition_equivalence: |
|
1797 shows "arg z = (if z = 0 then 0 else Im (Ln z))" |
|
1798 by (simp add: Arg_eq_Im_Ln arg_zero) |
1782 |
1799 |
1783 definition\<^marker>\<open>tag important\<close> Arg :: "complex \<Rightarrow> real" where "Arg z \<equiv> (if z = 0 then 0 else Im (Ln z))" |
1800 definition\<^marker>\<open>tag important\<close> Arg :: "complex \<Rightarrow> real" where "Arg z \<equiv> (if z = 0 then 0 else Im (Ln z))" |
1784 |
1801 |
1785 lemma Arg_of_real: "Arg (of_real r) = (if r<0 then pi else 0)" |
1802 lemma Arg_of_real: "Arg (of_real r) = (if r<0 then pi else 0)" |
1786 by (simp add: Im_Ln_eq_pi Arg_def) |
1803 by (simp add: Im_Ln_eq_pi Arg_def) |