SSL Complex.thy Sprache: Isabelle

(*  Title:       HOL/Complex.thy
    Author:      Jacques D. Fleuriot, 2001 University of Edinburgh
    Author:      Lawrence C Paulson, 2003/4
*)

section \<open>Complex Numbers: Rectangular and Polar Representations\<close>

theory Complex
imports Transcendental Real_Vector_Spaces
begin

text \<open>
  We use the \<^theory_text>\<open>codatatype\<close> command to define the type of complex numbers. This
  allows us to use \<^theory_text>\<open>primcorec\<close> to define complex functions by defining their
  real and imaginary result separately.
\<close>

codatatype complex = Complex (Re: real) (Im: real)

lemma complex_surj: "Complex (Re z) (Im z) = z"
  by (rule complex.collapse)

lemma complex_eqI [intro?]: "Re x = Re y \ Im x = Im y \ x = y"
  by (rule complex.expand) simp

lemma complex_eq_iff: "x = y \ Re x = Re y \ Im x = Im y"
  by (auto intro: complex.expand)

subsection \<open>Addition and Subtraction\<close>

instantiation complex :: ab_group_add
begin

primcorec zero_complex
  where
    "Re 0 = 0"
  | "Im 0 = 0"

primcorec plus_complex
  where
    "Re (x + y) = Re x + Re y"
  | "Im (x + y) = Im x + Im y"

primcorec uminus_complex
  where
    "Re (- x) = - Re x"
  | "Im (- x) = - Im x"

primcorec minus_complex
  where
    "Re (x - y) = Re x - Re y"
  | "Im (x - y) = Im x - Im y"

instance
  by standard (simp_all add: complex_eq_iff)

end

subsection \<open>Multiplication and Division\<close>

instantiation complex :: field
begin

primcorec one_complex
  where
    "Re 1 = 1"
  | "Im 1 = 0"

primcorec times_complex
  where
    "Re (x * y) = Re x * Re y - Im x * Im y"
  | "Im (x * y) = Re x * Im y + Im x * Re y"

primcorec inverse_complex
  where
    "Re (inverse x) = Re x / ((Re x)\<^sup>2 + (Im x)\<^sup>2)"
  | "Im (inverse x) = - Im x / ((Re x)\<^sup>2 + (Im x)\<^sup>2)"

definition "x div y = x * inverse y" for x y :: complex

instance
  by standard
     (simp_all add: complex_eq_iff divide_complex_def
      distrib_left distrib_right right_diff_distrib left_diff_distrib
      power2_eq_square add_divide_distrib [symmetric])

end

lemma Re_divide: "Re (x / y) = (Re x * Re y + Im x * Im y) / ((Re y)\<^sup>2 + (Im y)\<^sup>2)"
  by (simp add: divide_complex_def add_divide_distrib)

lemma Im_divide: "Im (x / y) = (Im x * Re y - Re x * Im y) / ((Re y)\<^sup>2 + (Im y)\<^sup>2)"
  by (simp add: divide_complex_def diff_divide_distrib)

lemma Complex_divide:
    "(x / y) = Complex ((Re x * Re y + Im x * Im y) / ((Re y)\<^sup>2 + (Im y)\<^sup>2))
                       ((Im x * Re y - Re x * Im y) / ((Re y)\<^sup>2 + (Im y)\<^sup>2))"
  by (metis Im_divide Re_divide complex_surj)

lemma Re_power2: "Re (x ^ 2) = (Re x)^2 - (Im x)^2"
  by (simp add: power2_eq_square)

lemma Im_power2: "Im (x ^ 2) = 2 * Re x * Im x"
  by (simp add: power2_eq_square)

lemma Re_power_real [simp]: "Im x = 0 \ Re (x ^ n) = Re x ^ n "
  by (induct n) simp_all

lemma Im_power_real [simp]: "Im x = 0 \ Im (x ^ n) = 0"
  by (induct n) simp_all

subsection \<open>Scalar Multiplication\<close>

instantiation complex :: real_field
begin

primcorec scaleR_complex
  where
    "Re (scaleR r x) = r * Re x"
  | "Im (scaleR r x) = r * Im x"

instance
proof
  fix a b :: real and x y :: complex
  show "scaleR a (x + y) = scaleR a x + scaleR a y"
    by (simp add: complex_eq_iff distrib_left)
  show "scaleR (a + b) x = scaleR a x + scaleR b x"
    by (simp add: complex_eq_iff distrib_right)
  show "scaleR a (scaleR b x) = scaleR (a * b) x"
    by (simp add: complex_eq_iff mult.assoc)
  show "scaleR 1 x = x"
    by (simp add: complex_eq_iff)
  show "scaleR a x * y = scaleR a (x * y)"
    by (simp add: complex_eq_iff algebra_simps)
  show "x * scaleR a y = scaleR a (x * y)"
    by (simp add: complex_eq_iff algebra_simps)
qed

end

subsection \<open>Numerals, Arithmetic, and Embedding from R\<close>

declare [[coercion "of_real :: real \ complex"]]
declare [[coercion "of_rat :: rat \ complex"]]
declare [[coercion "of_int :: int \ complex"]]
declare [[coercion "of_nat :: nat \ complex"]]

abbreviation complex_of_nat::"nat \ complex"
  where "complex_of_nat \ of_nat"

abbreviation complex_of_int::"int \ complex"
  where "complex_of_int \ of_int"

abbreviation complex_of_rat::"rat \ complex"
  where "complex_of_rat \ of_rat"

abbreviation complex_of_real :: "real \ complex"
  where "complex_of_real \ of_real"

lemma complex_Re_of_nat [simp]: "Re (of_nat n) = of_nat n"
  by (induct n) simp_all

lemma complex_Im_of_nat [simp]: "Im (of_nat n) = 0"
  by (induct n) simp_all

lemma complex_Re_of_int [simp]: "Re (of_int z) = of_int z"
  by (cases z rule: int_diff_cases) simp

lemma complex_Im_of_int [simp]: "Im (of_int z) = 0"
  by (cases z rule: int_diff_cases) simp

lemma complex_Re_numeral [simp]: "Re (numeral v) = numeral v"
  using complex_Re_of_int [of "numeral v"] by simp

lemma complex_Im_numeral [simp]: "Im (numeral v) = 0"
  using complex_Im_of_int [of "numeral v"] by simp

lemma Re_complex_of_real [simp]: "Re (complex_of_real z) = z"
  by (simp add: of_real_def)

lemma Im_complex_of_real [simp]: "Im (complex_of_real z) = 0"
  by (simp add: of_real_def)

lemma Re_divide_numeral [simp]: "Re (z / numeral w) = Re z / numeral w"
  by (simp add: Re_divide sqr_conv_mult)

lemma Im_divide_numeral [simp]: "Im (z / numeral w) = Im z / numeral w"
  by (simp add: Im_divide sqr_conv_mult)

lemma Re_divide_of_nat [simp]: "Re (z / of_nat n) = Re z / of_nat n"
  by (cases n) (simp_all add: Re_divide field_split_simps power2_eq_square del: of_nat_Suc)

lemma Im_divide_of_nat [simp]: "Im (z / of_nat n) = Im z / of_nat n"
  by (cases n) (simp_all add: Im_divide field_split_simps power2_eq_square del: of_nat_Suc)

lemma Re_inverse [simp]: "r \ \ \ Re (inverse r) = inverse (Re r)"
  by (metis Re_complex_of_real Reals_cases of_real_inverse)

lemma Im_inverse [simp]: "r \ \ \ Im (inverse r) = 0"
  by (metis Im_complex_of_real Reals_cases of_real_inverse)

lemma of_real_Re [simp]: "z \ \ \ of_real (Re z) = z"
  by (auto simp: Reals_def)

lemma complex_Re_fact [simp]: "Re (fact n) = fact n"
proof -
  have "(fact n :: complex) = of_real (fact n)"
    by simp
  also have "Re \ = fact n"
    by (subst Re_complex_of_real) simp_all
  finally show ?thesis .
qed

lemma surj_Re: "surj Re"
  by (metis Re_complex_of_real surj_def)

lemma surj_Im: "surj Im"
  by (metis complex.sel(2) surj_def)

lemma complex_Im_fact [simp]: "Im (fact n) = 0"
  by (metis complex_Im_of_nat of_nat_fact)

lemma Re_prod_Reals: "(\x. x \ A \ f x \ \) \ Re (prod f A) = prod (\x. Re (f x)) A"
proof (induction A rule: infinite_finite_induct)
  case (insert x A)
  hence "Re (prod f (insert x A)) = Re (f x) * Re (prod f A) - Im (f x) * Im (prod f A)"
    by simp
  also from insert.prems have "f x \ \" by simp
  hence "Im (f x) = 0" by (auto elim!: Reals_cases)
  also have "Re (prod f A) = (\x\A. Re (f x))"
    by (intro insert.IH insert.prems) auto
  finally show ?case using insert.hyps by simp
qed auto

subsection \<open>The Complex Number $i$\<close>

primcorec imaginary_unit :: complex  (\<open>\<i>\<close>)
  where
    "Re \ = 0"
  | "Im \ = 1"

lemma Complex_eq: "Complex a b = a + \ * b"
  by (simp add: complex_eq_iff)

lemma complex_eq: "a = Re a + \ * Im a"
  by (simp add: complex_eq_iff)

lemma fun_complex_eq: "f = (\x. Re (f x) + \ * Im (f x))"
  by (simp add: fun_eq_iff complex_eq)

lemma i_squared [simp]: "\ * \ = -1"
  by (simp add: complex_eq_iff)

lemma power2_i [simp]: "\\<^sup>2 = -1"
  by (simp add: power2_eq_square)

lemma inverse_i [simp]: "inverse \ = - \"
  by (rule inverse_unique) simp

lemma divide_i [simp]: "x / \ = - \ * x"
  by (simp add: divide_complex_def)

lemma complex_i_mult_minus [simp]: "\ * (\ * x) = - x"
  by (simp add: mult.assoc [symmetric])

lemma complex_i_not_zero [simp]: "\ \ 0"
  by (simp add: complex_eq_iff)

lemma complex_i_not_one [simp]: "\ \ 1"
  by (simp add: complex_eq_iff)

lemma complex_i_not_numeral [simp]: "\ \ numeral w"
  by (simp add: complex_eq_iff)

lemma complex_i_not_neg_numeral [simp]: "\ \ - numeral w"
  by (simp add: complex_eq_iff)

lemma complex_split_polar: "\r a. z = complex_of_real r * (cos a + \ * sin a)"
  by (simp add: complex_eq_iff polar_Ex)

lemma i_even_power [simp]: "\ ^ (n * 2) = (-1) ^ n"
  by (metis mult.commute power2_i power_mult)

lemma i_even_power' [simp]: "even n \ \ ^ n = (-1) ^ (n div 2)"
  by (metis dvd_mult_div_cancel power2_i power_mult)

lemma Re_i_times [simp]: "Re (\ * z) = - Im z"
  by simp

lemma Im_i_times [simp]: "Im (\ * z) = Re z"
  by simp

lemma i_times_eq_iff: "\ * w = z \ w = - (\ * z)"
  by auto

lemma divide_numeral_i [simp]: "z / (numeral n * \) = - (\ * z) / numeral n"
  by (metis divide_divide_eq_left divide_i mult.commute mult_minus_right)

lemma imaginary_eq_real_iff [simp]:
  assumes "y \ Reals" "x \ Reals"
  shows "\ * y = x \ x=0 \ y=0"
  by (metis Im_complex_of_real Im_i_times assms mult_zero_right of_real_0 of_real_Re)

lemma real_eq_imaginary_iff [simp]:
  assumes "y \ Reals" "x \ Reals"
  shows "x = \ * y \ x=0 \ y=0"
    using assms imaginary_eq_real_iff by fastforce

subsection \<open>Vector Norm\<close>

instantiation complex :: real_normed_field
begin

definition "norm z = sqrt ((Re z)\<^sup>2 + (Im z)\<^sup>2)"

abbreviation cmod :: "complex \ real"
  where "cmod \ norm"

definition complex_sgn_def: "sgn x = x /\<^sub>R cmod x"

definition dist_complex_def: "dist x y = cmod (x - y)"

definition uniformity_complex_def [code del]:
  "(uniformity :: (complex \ complex) filter) = (INF e\{0 <..}. principal {(x, y). dist x y < e})"

definition open_complex_def [code del]:
  "open (U :: complex set) \ (\x\U. eventually (\(x', y). x' = x \ y \ U) uniformity)"

instance
proof
  fix r :: real and x y :: complex and S :: "complex set"
  show "(norm x = 0) = (x = 0)"
    by (simp add: norm_complex_def complex_eq_iff)
  show "norm (x + y) \ norm x + norm y"
    by (simp add: norm_complex_def complex_eq_iff real_sqrt_sum_squares_triangle_ineq)
  show "norm (scaleR r x) = \r\ * norm x"
    by (simp add: norm_complex_def complex_eq_iff power_mult_distrib distrib_left [symmetric]
        real_sqrt_mult)
  show "norm (x * y) = norm x * norm y"
    by (simp add: norm_complex_def complex_eq_iff real_sqrt_mult [symmetric]
        power2_eq_square algebra_simps)
qed (rule complex_sgn_def dist_complex_def open_complex_def uniformity_complex_def)+

end

declare uniformity_Abort[where 'a = complex, code]

lemma Re_divide': "Re (x / y) = (Re x * Re y + Im x * Im y) / (norm y)\<^sup>2"
  by (simp add: Re_divide norm_complex_def)

lemma Im_divide': "Im (x / y) = (Im x * Re y - Re x * Im y) / (norm y)\<^sup>2"
  by (simp add: Im_divide norm_complex_def)

lemma norm_ii [simp]: "norm \ = 1"
  by (simp add: norm_complex_def)

lemma cmod_unit_one: "cmod (cos a + \ * sin a) = 1"
  by (simp add: norm_complex_def)

lemma cmod_complex_polar: "cmod (r * (cos a + \ * sin a)) = \r\"
  by (simp add: norm_mult cmod_unit_one)

lemma complex_Re_le_cmod: "Re x \ cmod x"
  unfolding norm_complex_def by (rule real_sqrt_sum_squares_ge1)

lemma complex_mod_minus_le_complex_mod: "- cmod x \ cmod x"
  by (rule order_trans [OF _ norm_ge_zero]) simp

lemma complex_mod_triangle_ineq2: "cmod (b + a) - cmod b \ cmod a"
  by (rule ord_le_eq_trans [OF norm_triangle_ineq2]) simp

lemma abs_Re_le_cmod: "\Re x\ \ cmod x"
  by (simp add: norm_complex_def)

lemma abs_Im_le_cmod: "\Im x\ \ cmod x"
  by (simp add: norm_complex_def)

lemma cmod_le: "cmod z \ \Re z\ + \Im z\"
  using norm_complex_def sqrt_sum_squares_le_sum_abs by presburger

lemma cmod_eq_Re: "Im z = 0 \ cmod z = \Re z\"
  by (simp add: norm_complex_def)

lemma cmod_eq_Im: "Re z = 0 \ cmod z = \Im z\"
  by (simp add: norm_complex_def)

lemma cmod_power2: "(cmod z)\<^sup>2 = (Re z)\<^sup>2 + (Im z)\<^sup>2"
  by (simp add: norm_complex_def)

lemma cmod_plus_Re_le_0_iff: "cmod z + Re z \ 0 \ Re z = - cmod z"
  using abs_Re_le_cmod[of z] by auto

lemma cmod_Re_le_iff: "Im x = Im y \ cmod x \ cmod y \ \Re x\ \ \Re y\"
  by (metis add.commute add_le_cancel_left norm_complex_def real_sqrt_abs real_sqrt_le_iff)

lemma cmod_Im_le_iff: "Re x = Re y \ cmod x \ cmod y \ \Im x\ \ \Im y\"
  by (metis add_le_cancel_left norm_complex_def real_sqrt_abs real_sqrt_le_iff)

lemma Im_eq_0: "\Re z\ = cmod z \ Im z = 0"
  by (subst (asm) power_eq_iff_eq_base[symmetric, where n=2]) (auto simp add: norm_complex_def)

lemma abs_sqrt_wlog: "(\x. x \ 0 \ P x (x\<^sup>2)) \ P \x\ (x\<^sup>2)"
  for x::"'a::linordered_idom"
  by (metis abs_ge_zero power2_abs)

lemma complex_abs_le_norm: "\Re z\ + \Im z\ \ sqrt 2 * norm z"
  unfolding norm_complex_def
  apply (rule abs_sqrt_wlog [where x="Re z"])
  apply (rule abs_sqrt_wlog [where x="Im z"])
  apply (rule power2_le_imp_le)
   apply (simp_all add: power2_sum add.commute sum_squares_bound real_sqrt_mult [symmetric])
  done

lemma complex_unit_circle: "z \ 0 \ (Re z / cmod z)\<^sup>2 + (Im z / cmod z)\<^sup>2 = 1"
  by (simp add: norm_complex_def complex_eq_iff power2_eq_square add_divide_distrib [symmetric])

text \<open>Properties of complex signum.\<close>

lemma sgn_eq: "sgn z = z / complex_of_real (cmod z)"
  by (simp add: sgn_div_norm divide_inverse scaleR_conv_of_real mult.commute)

lemma Re_sgn [simp]: "Re(sgn z) = Re(z)/cmod z"
  by (simp add: complex_sgn_def divide_inverse)

lemma Im_sgn [simp]: "Im(sgn z) = Im(z)/cmod z"
  by (simp add: complex_sgn_def divide_inverse)

subsection \<open>Absolute value\<close>

instantiation complex :: field_abs_sgn
begin

definition abs_complex :: "complex \ complex"
  where "abs_complex = of_real \ norm"

instance
  proof qed (auto simp add: abs_complex_def complex_sgn_def norm_divide norm_mult scaleR_conv_of_real field_simps)
end

subsection \<open>Completeness of the Complexes\<close>

lemma bounded_linear_Re: "bounded_linear Re"
  by (rule bounded_linear_intro [where K=1]) (simp_all add: norm_complex_def)

lemma bounded_linear_Im: "bounded_linear Im"
  by (rule bounded_linear_intro [where K=1]) (simp_all add: norm_complex_def)

lemmas Cauchy_Re = bounded_linear.Cauchy [OF bounded_linear_Re]
lemmas Cauchy_Im = bounded_linear.Cauchy [OF bounded_linear_Im]
lemmas tendsto_Re [tendsto_intros] = bounded_linear.tendsto [OF bounded_linear_Re]
lemmas tendsto_Im [tendsto_intros] = bounded_linear.tendsto [OF bounded_linear_Im]
lemmas isCont_Re [simp] = bounded_linear.isCont [OF bounded_linear_Re]
lemmas isCont_Im [simp] = bounded_linear.isCont [OF bounded_linear_Im]
lemmas continuous_Re [simp] = bounded_linear.continuous [OF bounded_linear_Re]
lemmas continuous_Im [simp] = bounded_linear.continuous [OF bounded_linear_Im]
lemmas continuous_on_Re [continuous_intros] = bounded_linear.continuous_on[OF bounded_linear_Re]
lemmas continuous_on_Im [continuous_intros] = bounded_linear.continuous_on[OF bounded_linear_Im]
lemmas has_derivative_Re [derivative_intros] = bounded_linear.has_derivative[OF bounded_linear_Re]
lemmas has_derivative_Im [derivative_intros] = bounded_linear.has_derivative[OF bounded_linear_Im]
lemmas sums_Re = bounded_linear.sums [OF bounded_linear_Re]
lemmas sums_Im = bounded_linear.sums [OF bounded_linear_Im]
lemmas Re_suminf = bounded_linear.suminf[OF bounded_linear_Re]
lemmas Im_suminf = bounded_linear.suminf[OF bounded_linear_Im]

lemma continuous_on_Complex [continuous_intros]:
  "continuous_on A f \ continuous_on A g \ continuous_on A (\x. Complex (f x) (g x))"
  unfolding Complex_eq by (intro continuous_intros)

lemma tendsto_Complex [tendsto_intros]:
  "(f \ a) F \ (g \ b) F \ ((\x. Complex (f x) (g x)) \ Complex a b) F"
  unfolding Complex_eq by (auto intro!: tendsto_intros)

lemma tendsto_complex_iff:
  "(f \ x) F \ (((\x. Re (f x)) \ Re x) F \ ((\x. Im (f x)) \ Im x) F)"
proof safe
  assume "((\x. Re (f x)) \ Re x) F" "((\x. Im (f x)) \ Im x) F"
  from tendsto_Complex[OF this] show "(f \ x) F"
    unfolding complex.collapse .
qed (auto intro: tendsto_intros)

lemma continuous_complex_iff:
  "continuous F f \ continuous F (\x. Re (f x)) \ continuous F (\x. Im (f x))"
  by (simp only: continuous_def tendsto_complex_iff)

lemma continuous_on_of_real_o_iff [simp]:
     "continuous_on S (\x. complex_of_real (g x)) = continuous_on S g"
  using continuous_on_Re continuous_on_of_real  by fastforce

lemma continuous_on_of_real_id [simp]:
     "continuous_on S (of_real :: real \ 'a::real_normed_algebra_1)"
  by (rule continuous_on_of_real [OF continuous_on_id])

lemma has_vector_derivative_complex_iff: "(f has_vector_derivative x) F \
    ((\<lambda>x. Re (f x)) has_field_derivative (Re x)) F \<and>
    ((\<lambda>x. Im (f x)) has_field_derivative (Im x)) F"
  by (simp add: has_vector_derivative_def has_field_derivative_def has_derivative_def
      tendsto_complex_iff algebra_simps bounded_linear_scaleR_left bounded_linear_mult_right)

lemma has_field_derivative_Re[derivative_intros]:
  "(f has_vector_derivative D) F \ ((\x. Re (f x)) has_field_derivative (Re D)) F"
  unfolding has_vector_derivative_complex_iff by safe

lemma has_field_derivative_Im[derivative_intros]:
  "(f has_vector_derivative D) F \ ((\x. Im (f x)) has_field_derivative (Im D)) F"
  unfolding has_vector_derivative_complex_iff by safe

instance complex :: banach
proof
  fix X :: "nat \ complex"
  assume X: "Cauchy X"
  then have "(\n. Complex (Re (X n)) (Im (X n))) \
    Complex (lim (\<lambda>n. Re (X n))) (lim (\<lambda>n. Im (X n)))"
    by (intro tendsto_Complex convergent_LIMSEQ_iff[THEN iffD1]
        Cauchy_convergent_iff[THEN iffD1] Cauchy_Re Cauchy_Im)
  then show "convergent X"
    unfolding complex.collapse by (rule convergentI)
qed

declare DERIV_power[where 'a=complex, unfolded of_nat_def[symmetric], derivative_intros]

subsection \<open>Complex Conjugation\<close>

primcorec cnj :: "complex \ complex"
  where
    "Re (cnj z) = Re z"
  | "Im (cnj z) = - Im z"

lemma complex_cnj_cancel_iff [simp]: "cnj x = cnj y \ x = y"
  by (simp add: complex_eq_iff)

lemma complex_cnj_cnj [simp]: "cnj (cnj z) = z"
  by (simp add: complex_eq_iff)

lemma in_image_cnj_iff: "z \ cnj ` A \ cnj z \ A"
  by (metis complex_cnj_cnj image_iff)

lemma image_cnj_conv_vimage_cnj: "cnj ` A = cnj -` A"
  using in_image_cnj_iff by blast

lemma complex_cnj_zero [simp]: "cnj 0 = 0"
  by (simp add: complex_eq_iff)

lemma complex_cnj_zero_iff [iff]: "cnj z = 0 \ z = 0"
  by (simp add: complex_eq_iff)

lemma complex_cnj_one_iff [simp]: "cnj z = 1 \ z = 1"
  by (simp add: complex_eq_iff)

lemma complex_cnj_add [simp]: "cnj (x + y) = cnj x + cnj y"
  by (simp add: complex_eq_iff)

lemma cnj_sum [simp]: "cnj (sum f s) = (\x\s. cnj (f x))"
  by (induct s rule: infinite_finite_induct) auto

lemma complex_cnj_diff [simp]: "cnj (x - y) = cnj x - cnj y"
  by (simp add: complex_eq_iff)

lemma complex_cnj_minus [simp]: "cnj (- x) = - cnj x"
  by (simp add: complex_eq_iff)

lemma complex_cnj_one [simp]: "cnj 1 = 1"
  by (simp add: complex_eq_iff)

lemma complex_cnj_mult [simp]: "cnj (x * y) = cnj x * cnj y"
  by (simp add: complex_eq_iff)

lemma cnj_prod [simp]: "cnj (prod f s) = (\x\s. cnj (f x))"
  by (induct s rule: infinite_finite_induct) auto

lemma complex_cnj_inverse [simp]: "cnj (inverse x) = inverse (cnj x)"
  by (simp add: complex_eq_iff)

lemma complex_cnj_divide [simp]: "cnj (x / y) = cnj x / cnj y"
  by (simp add: divide_complex_def)

lemma complex_cnj_power [simp]: "cnj (x ^ n) = cnj x ^ n"
  by (induct n) simp_all

lemma complex_cnj_of_nat [simp]: "cnj (of_nat n) = of_nat n"
  by (simp add: complex_eq_iff)

lemma complex_cnj_of_int [simp]: "cnj (of_int z) = of_int z"
  by (simp add: complex_eq_iff)

lemma complex_cnj_numeral [simp]: "cnj (numeral w) = numeral w"
  by (simp add: complex_eq_iff)

lemma complex_cnj_neg_numeral [simp]: "cnj (- numeral w) = - numeral w"
  by (simp add: complex_eq_iff)

lemma complex_cnj_scaleR [simp]: "cnj (scaleR r x) = scaleR r (cnj x)"
  by (simp add: complex_eq_iff)

lemma complex_mod_cnj [simp]: "cmod (cnj z) = cmod z"
  by (simp add: norm_complex_def)

lemma complex_cnj_complex_of_real [simp]: "cnj (of_real x) = of_real x"
  by (simp add: complex_eq_iff)

lemma complex_cnj_i [simp]: "cnj \ = - \"
  by (simp add: complex_eq_iff)

lemma complex_add_cnj: "z + cnj z = complex_of_real (2 * Re z)"
  by (simp add: complex_eq_iff)

lemma complex_diff_cnj: "z - cnj z = complex_of_real (2 * Im z) * \"
  by (simp add: complex_eq_iff)

lemma Ints_cnj [intro]: "x \ \ \ cnj x \ \"
  by (auto elim!: Ints_cases)

lemma cnj_in_Ints_iff [simp]: "cnj x \ \ \ x \ \"
  using Ints_cnj[of x] Ints_cnj[of "cnj x"] by auto

lemma complex_mult_cnj: "z * cnj z = complex_of_real ((Re z)\<^sup>2 + (Im z)\<^sup>2)"
  by (simp add: complex_eq_iff power2_eq_square)

lemma cnj_add_mult_eq_Re: "z * cnj w + cnj z * w = 2 * Re (z * cnj w)"
  by (rule complex_eqI) auto

lemma complex_mod_mult_cnj: "cmod (z * cnj z) = (cmod z)\<^sup>2"
  by (simp add: norm_mult power2_eq_square)

lemma complex_mod_sqrt_Re_mult_cnj: "cmod z = sqrt (Re (z * cnj z))"
  by (simp add: norm_complex_def power2_eq_square)

lemma complex_In_mult_cnj_zero [simp]: "Im (z * cnj z) = 0"
  by simp

lemma complex_cnj_fact [simp]: "cnj (fact n) = fact n"
  by (subst of_nat_fact [symmetric], subst complex_cnj_of_nat) simp

lemma complex_cnj_pochhammer [simp]: "cnj (pochhammer z n) = pochhammer (cnj z) n"
  by (induct n arbitrary: z) (simp_all add: pochhammer_rec)

lemma bounded_linear_cnj: "bounded_linear cnj"
  using complex_cnj_add complex_cnj_scaleR by (rule bounded_linear_intro [where K=1]) simp

lemma linear_cnj: "linear cnj"
  using bounded_linear.linear[OF bounded_linear_cnj] .

lemmas tendsto_cnj [tendsto_intros] = bounded_linear.tendsto [OF bounded_linear_cnj]
  and isCont_cnj [simp] = bounded_linear.isCont [OF bounded_linear_cnj]
  and continuous_cnj [simp, continuous_intros] = bounded_linear.continuous [OF bounded_linear_cnj]
  and continuous_on_cnj [simp, continuous_intros] = bounded_linear.continuous_on [OF bounded_linear_cnj]
  and has_derivative_cnj [simp, derivative_intros] = bounded_linear.has_derivative [OF bounded_linear_cnj]

lemma lim_cnj: "((\x. cnj(f x)) \ cnj l) F \ (f \ l) F"
  by (simp add: tendsto_iff dist_complex_def complex_cnj_diff [symmetric] del: complex_cnj_diff)

lemma sums_cnj: "((\x. cnj(f x)) sums cnj l) \ (f sums l)"
  by (simp add: sums_def lim_cnj cnj_sum [symmetric] del: cnj_sum)

lemma differentiable_cnj_iff:
  "(\z. cnj (f z)) differentiable at x within A \ f differentiable at x within A"
proof
  assume "(\z. cnj (f z)) differentiable at x within A"
  then obtain D where "((\z. cnj (f z)) has_derivative D) (at x within A)"
    by (auto simp: differentiable_def)
  from has_derivative_cnj[OF this] show "f differentiable at x within A"
    by (auto simp: differentiable_def)
next
  assume "f differentiable at x within A"
  then obtain D where "(f has_derivative D) (at x within A)"
    by (auto simp: differentiable_def)
  from has_derivative_cnj[OF this] show "(\z. cnj (f z)) differentiable at x within A"
    by (auto simp: differentiable_def)
qed

lemma has_vector_derivative_cnj [derivative_intros]:
  assumes "(f has_vector_derivative f') (at z within A)"
  shows   "((\z. cnj (f z)) has_vector_derivative cnj f') (at z within A)"
  using assms by (auto simp: has_vector_derivative_complex_iff intro: derivative_intros)

lemma has_field_derivative_cnj_cnj:
  assumes "(f has_field_derivative F) (at (cnj z))"
  shows   "((cnj \ f \ cnj) has_field_derivative cnj F) (at z)"
proof -
  have "cnj \0\ cnj 0"
    by (subst lim_cnj) auto
  also have "cnj 0 = 0"
    by simp
  finally have *: "filterlim cnj (at 0) (at 0)"
    by (auto simp: filterlim_at eventually_at_filter)
  have "(\h. (f (cnj z + cnj h) - f (cnj z)) / cnj h) \0\ F"
    by (rule filterlim_compose[OF _ *]) (use assms in \<open>auto simp: DERIV_def\<close>)
  thus ?thesis
    by (subst (asm) lim_cnj [symmetric]) (simp add: DERIV_def)
qed

subsection \<open>Basic Lemmas\<close>

lemma complex_of_real_code[code_unfold]: "of_real = (\x. Complex x 0)"
  by (intro ext, auto simp: complex_eq_iff)

lemma complex_eq_0: "z=0 \ (Re z)\<^sup>2 + (Im z)\<^sup>2 = 0"
  by (metis zero_complex.sel complex_eqI sum_power2_eq_zero_iff)

lemma complex_neq_0: "z\0 \ (Re z)\<^sup>2 + (Im z)\<^sup>2 > 0"
  by (metis complex_eq_0 less_numeral_extra(3) sum_power2_gt_zero_iff)

lemma complex_norm_square: "of_real ((norm z)\<^sup>2) = z * cnj z"
  by (cases z)
    (auto simp: complex_eq_iff norm_complex_def power2_eq_square[symmetric] of_real_power[symmetric]
      simp del: of_real_power)

lemma complex_div_cnj: "a / b = (a * cnj b) / (norm b)\<^sup>2"
  using complex_norm_square by auto

lemma Re_complex_div_eq_0: "Re (a / b) = 0 \ Re (a * cnj b) = 0"
  by (auto simp add: Re_divide)

lemma Im_complex_div_eq_0: "Im (a / b) = 0 \ Im (a * cnj b) = 0"
  by (auto simp add: Im_divide)

lemma complex_div_gt_0: "(Re (a / b) > 0 \ Re (a * cnj b) > 0) \ (Im (a / b) > 0 \ Im (a * cnj b) > 0)"
proof (cases "b = 0")
  case True
  then show ?thesis by auto
next
  case False
  then have "0 < (Re b)\<^sup>2 + (Im b)\<^sup>2"
    by (simp add: complex_eq_iff sum_power2_gt_zero_iff)
  then show ?thesis
    by (simp add: Re_divide Im_divide zero_less_divide_iff)
qed

lemma Re_complex_div_gt_0: "Re (a / b) > 0 \ Re (a * cnj b) > 0"
  and Im_complex_div_gt_0: "Im (a / b) > 0 \ Im (a * cnj b) > 0"
  using complex_div_gt_0 by auto

lemma Re_complex_div_ge_0: "Re (a / b) \ 0 \ Re (a * cnj b) \ 0"
  by (metis le_less Re_complex_div_eq_0 Re_complex_div_gt_0)

lemma Im_complex_div_ge_0: "Im (a / b) \ 0 \ Im (a * cnj b) \ 0"
  by (metis Im_complex_div_eq_0 Im_complex_div_gt_0 le_less)

lemma Re_complex_div_lt_0: "Re (a / b) < 0 \ Re (a * cnj b) < 0"
  by (metis less_asym neq_iff Re_complex_div_eq_0 Re_complex_div_gt_0)

lemma Im_complex_div_lt_0: "Im (a / b) < 0 \ Im (a * cnj b) < 0"
  by (metis Im_complex_div_eq_0 Im_complex_div_gt_0 less_asym neq_iff)

lemma Re_complex_div_le_0: "Re (a / b) \ 0 \ Re (a * cnj b) \ 0"
  by (metis not_le Re_complex_div_gt_0)

lemma Im_complex_div_le_0: "Im (a / b) \ 0 \ Im (a * cnj b) \ 0"
  by (metis Im_complex_div_gt_0 not_le)

lemma Re_divide_of_real [simp]: "Re (z / of_real r) = Re z / r"
  by (simp add: Re_divide power2_eq_square)

lemma Im_divide_of_real [simp]: "Im (z / of_real r) = Im z / r"
  by (simp add: Im_divide power2_eq_square)

lemma Re_divide_Reals [simp]: "r \ \ \ Re (z / r) = Re z / Re r"
  by (metis Re_divide_of_real of_real_Re)

lemma Im_divide_Reals [simp]: "r \ \ \ Im (z / r) = Im z / Re r"
  by (metis Im_divide_of_real of_real_Re)

lemma Re_sum[simp]: "Re (sum f s) = (\x\s. Re (f x))"
  by (induct s rule: infinite_finite_induct) auto

lemma Im_sum[simp]: "Im (sum f s) = (\x\s. Im(f x))"
  by (induct s rule: infinite_finite_induct) auto

lemma Rats_complex_of_real_iff [iff]: "complex_of_real x \ \ \ x \ \"
proof -
  have "\a b. \0 < b; x = complex_of_int a / complex_of_int b\ \ x \ \"
    by (metis Rats_divide Rats_of_int Re_complex_of_real Re_divide_of_real of_real_of_int_eq)
  then show ?thesis
    by (auto simp: elim!: Rats_cases')
qed

lemma sum_Re_le_cmod: "(\i\I. Re (z i)) \ cmod (\i\I. z i)"
  by (metis Re_sum complex_Re_le_cmod)

lemma sum_Im_le_cmod: "(\i\I. Im (z i)) \ cmod (\i\I. z i)"
  by (smt (verit, best) Im_sum abs_Im_le_cmod sum.cong)

lemma sums_complex_iff: "f sums x \ ((\x. Re (f x)) sums Re x) \ ((\x. Im (f x)) sums Im x)"
  unfolding sums_def tendsto_complex_iff Im_sum Re_sum ..

lemma summable_complex_iff: "summable f \ summable (\x. Re (f x)) \ summable (\x. Im (f x))"
  unfolding summable_def sums_complex_iff[abs_def] by (metis complex.sel)

lemma summable_complex_of_real [simp]: "summable (\n. complex_of_real (f n)) \ summable f"
  unfolding summable_complex_iff by simp

lemma summable_Re: "summable f \ summable (\x. Re (f x))"
  unfolding summable_complex_iff by blast

lemma summable_Im: "summable f \ summable (\x. Im (f x))"
  unfolding summable_complex_iff by blast

lemma complex_is_Nat_iff: "z \ \ \ Im z = 0 \ (\i. Re z = of_nat i)"
  by (auto simp: Nats_def complex_eq_iff)

lemma complex_is_Int_iff: "z \ \ \ Im z = 0 \ (\i. Re z = of_int i)"
  by (auto simp: Ints_def complex_eq_iff)

lemma complex_is_Real_iff: "z \ \ \ Im z = 0"
  by (auto simp: Reals_def complex_eq_iff)

lemma sgn_complex_iff: "sgn x = sgn (Re x) \ x \ \"
  by (metis Im_complex_of_real Im_sgn Reals_0 complex_is_Real_iff divide_eq_0_iff
      norm_eq_zero of_real_Re sgn_of_real)

lemma Reals_cnj_iff: "z \ \ \ cnj z = z"
  by (auto simp: complex_is_Real_iff complex_eq_iff)

lemma in_Reals_norm: "z \ \ \ norm z = \Re z\"
  by (simp add: complex_is_Real_iff norm_complex_def)

lemma Re_Reals_divide: "r \ \ \ Re (r / z) = Re r * Re z / (norm z)\<^sup>2"
  by (simp add: Re_divide complex_is_Real_iff cmod_power2)

lemma Im_Reals_divide: "r \ \ \ Im (r / z) = -Re r * Im z / (norm z)\<^sup>2"
  by (simp add: Im_divide complex_is_Real_iff cmod_power2)

lemma series_comparison_complex:
  fixes f:: "nat \ 'a::banach"
  assumes sg: "summable g"
    and "\n. g n \ \" "\n. Re (g n) \ 0"
    and fg: "\n. n \ N \ norm(f n) \ norm(g n)"
  shows "summable f"
proof -
  have g: "\n. cmod (g n) = Re (g n)"
    using assms by (metis abs_of_nonneg in_Reals_norm)
  show ?thesis
    by (metis fg g sg summable_comparison_test summable_complex_iff)
qed

subsection \<open>Polar Form for Complex Numbers\<close>

lemma complex_unimodular_polar:
  assumes "norm z = 1"
  obtains t where "0 \ t" "t < 2 * pi" "z = Complex (cos t) (sin t)"
  by (metis cmod_power2 one_power2 complex_surj sincos_total_2pi [of "Re z" "Im z"] assms)

subsubsection \<open>$\cos \theta + i \sin \theta$\<close>

primcorec cis :: "real \ complex"
  where
    "Re (cis a) = cos a"
  | "Im (cis a) = sin a"

lemma cis_zero [simp]: "cis 0 = 1"
  by (simp add: complex_eq_iff)

lemma norm_cis [simp]: "norm (cis a) = 1"
  by (simp add: norm_complex_def)

lemma sgn_cis [simp]: "sgn (cis a) = cis a"
  by (simp add: sgn_div_norm)

lemma cis_2pi [simp]: "cis (2 * pi) = 1"
  by (simp add: cis.ctr complex_eq_iff)

lemma cis_neq_zero [simp]: "cis a \ 0"
  by (metis norm_cis norm_zero zero_neq_one)

lemma cis_cnj: "cnj (cis t) = cis (-t)"
  by (simp add: complex_eq_iff)

lemma cis_mult: "cis a * cis b = cis (a + b)"
  by (simp add: complex_eq_iff cos_add sin_add)

lemma DeMoivre: "(cis a) ^ n = cis (real n * a)"
  by (induct n) (simp_all add: algebra_simps cis_mult)

lemma cis_inverse [simp]: "inverse (cis a) = cis (- a)"
  by (simp add: complex_eq_iff)

lemma cis_divide: "cis a / cis b = cis (a - b)"
  by (simp add: divide_complex_def cis_mult)

lemma cis_power_int: "cis x powi n = cis (of_int n * x)"
  by (auto simp: power_int_def DeMoivre)

lemma complex_cnj_power_int [simp]: "cnj (x powi n) = cnj x powi n"
  by (auto simp: power_int_def)

lemma divide_conv_cnj: "norm z = 1 \ x / z = x * cnj z"
  by (metis complex_div_cnj div_by_1 mult_1 of_real_1 power2_eq_square)

lemma i_not_in_Reals [simp, intro]: "\ \ \"
  by (auto simp: complex_is_Real_iff)

lemma cos_n_Re_cis_pow_n: "cos (real n * a) = Re (cis a ^ n)"
  by (auto simp add: DeMoivre)

lemma sin_n_Im_cis_pow_n: "sin (real n * a) = Im (cis a ^ n)"
  by (auto simp add: DeMoivre)

lemma cis_pi [simp]: "cis pi = -1"
  by (simp add: complex_eq_iff)

lemma cis_pi_half[simp]: "cis (pi / 2) = \"
  by (simp add: cis.ctr complex_eq_iff)

lemma cis_minus_pi_half[simp]: "cis (-(pi / 2)) = -\"
  by (simp add: cis.ctr complex_eq_iff)

lemma cis_multiple_2pi[simp]: "n \ \ \ cis (2 * pi * n) = 1"
  by (auto elim!: Ints_cases simp: cis.ctr one_complex.ctr)

lemma minus_cis: "-cis x = cis (x + pi)"
  by (simp flip: cis_mult)

lemma minus_cis': "-cis x = cis (x - pi)"
  by (simp flip: cis_divide)

subsubsection \<open>$r(\cos \theta + i \sin \theta)$\<close>

definition rcis :: "real \ real \ complex"
  where "rcis r a = complex_of_real r * cis a"

lemma Re_rcis [simp]: "Re(rcis r a) = r * cos a"
  by (simp add: rcis_def)

lemma Im_rcis [simp]: "Im(rcis r a) = r * sin a"
  by (simp add: rcis_def)

lemma rcis_Ex: "\r a. z = rcis r a"
  by (simp add: complex_eq_iff polar_Ex)

lemma complex_mod_rcis [simp]: "cmod (rcis r a) = \r\"
  by (simp add: rcis_def norm_mult)

lemma cis_rcis_eq: "cis a = rcis 1 a"
  by (simp add: rcis_def)

lemma rcis_mult: "rcis r1 a * rcis r2 b = rcis (r1 * r2) (a + b)"
  by (simp add: rcis_def cis_mult)

lemma rcis_zero_mod [simp]: "rcis 0 a = 0"
  by (simp add: rcis_def)

lemma rcis_zero_arg [simp]: "rcis r 0 = complex_of_real r"
  by (simp add: rcis_def)

lemma rcis_eq_zero_iff [simp]: "rcis r a = 0 \ r = 0"
  by (simp add: rcis_def)

lemma DeMoivre2: "(rcis r a) ^ n = rcis (r ^ n) (real n * a)"
  by (simp add: rcis_def power_mult_distrib DeMoivre)

lemma rcis_inverse: "inverse(rcis r a) = rcis (1 / r) (- a)"
  by (simp add: divide_inverse rcis_def)

lemma rcis_divide: "rcis r1 a / rcis r2 b = rcis (r1 / r2) (a - b)"
  by (simp add: rcis_def cis_divide [symmetric])

subsubsection \<open>Complex exponential\<close>

lemma exp_Reals_eq:
  assumes "z \ \"
  shows   "exp z = of_real (exp (Re z))"
  using assms by (auto elim!: Reals_cases simp: exp_of_real)

lemma cis_conv_exp: "cis b = exp (\ * b)"
proof -
  have "(\ * complex_of_real b) ^ n /\<^sub>R fact n =
      of_real (cos_coeff n * b^n) + \<i> * of_real (sin_coeff n * b^n)"
    for n :: nat
  proof -
    have "\ ^ n = fact n *\<^sub>R (cos_coeff n + \ * sin_coeff n)"
      by (induct n)
        (simp_all add: sin_coeff_Suc cos_coeff_Suc complex_eq_iff Re_divide Im_divide field_simps
          power2_eq_square add_nonneg_eq_0_iff)
    then show ?thesis
      by (simp add: field_simps)
  qed
  then show ?thesis
    using sin_converges [of b] cos_converges [of b]
    by (auto simp add: Complex_eq cis.ctr exp_def simp del: of_real_mult
        intro!: sums_unique sums_add sums_mult sums_of_real)
qed

lemma exp_eq_polar: "exp z = exp (Re z) * cis (Im z)"
  unfolding cis_conv_exp exp_of_real [symmetric] mult_exp_exp
  by (cases z) (simp add: Complex_eq)

lemma Re_exp: "Re (exp z) = exp (Re z) * cos (Im z)"
  unfolding exp_eq_polar by simp

lemma Im_exp: "Im (exp z) = exp (Re z) * sin (Im z)"
  unfolding exp_eq_polar by simp

lemma norm_cos_sin [simp]: "norm (Complex (cos t) (sin t)) = 1"
  by (simp add: norm_complex_def)

lemma norm_exp_eq_Re [simp]: "norm (exp z) = exp (Re z)"
  by (simp add: cis.code cmod_complex_polar exp_eq_polar Complex_eq)

lemma complex_exp_exists: "\a r. z = complex_of_real r * exp a"
  using cis_conv_exp rcis_Ex rcis_def by force

lemma exp_pi_i [simp]: "exp (of_real pi * \) = -1"
  by (metis cis_conv_exp cis_pi mult.commute)

lemma exp_pi_i' [simp]: "exp (\ * of_real pi) = -1"
  using cis_conv_exp cis_pi by auto

lemma exp_two_pi_i [simp]: "exp (2 * of_real pi * \) = 1"
  by (simp add: exp_eq_polar complex_eq_iff)

lemma exp_two_pi_i' [simp]: "exp (\ * (of_real pi * 2)) = 1"
  by (metis exp_two_pi_i mult.commute)

lemma continuous_on_cis [continuous_intros]:
  "continuous_on A f \ continuous_on A (\x. cis (f x))"
  by (auto simp: cis_conv_exp intro!: continuous_intros)

lemma tendsto_exp_0_Re_at_bot: "(exp \ 0) (filtercomap Re at_bot)"
proof -
  have "((\z. cmod (exp z)) \ 0) (filtercomap Re at_bot)"
    by (auto intro!: filterlim_filtercomapI exp_at_bot)
  thus ?thesis
    using tendsto_norm_zero_iff by blast
qed

lemma filterlim_exp_at_infinity_Re_at_top: "filterlim exp at_infinity (filtercomap Re at_top)"
proof -
  have "filterlim (\z. norm (exp z)) at_top (filtercomap Re at_top)"
    by (auto intro!: filterlim_filtercomapI exp_at_top)
  thus ?thesis
    using filterlim_norm_at_top_imp_at_infinity by blast
qed

lemma tendsto_cis [tendsto_intros]:
  assumes "(f \ x) F"
  shows   "((\u. cis (f u)) \ cis x) F"
  unfolding cis_conv_exp by (intro tendsto_intros assms)

lemma tendsto_rcis [tendsto_intros]:
  assumes "(f \ r) F" "(g \ x) F"
  shows   "((\u. rcis (f u) (g u)) \ rcis r x) F"
  unfolding rcis_def by (intro tendsto_intros assms)

lemma continuous_on_rcis [continuous_intros]:
  "continuous_on A f \ continuous_on A g \ continuous_on A (\x. rcis (f x) (g x))"
  unfolding rcis_def by (intro continuous_intros)

lemma has_derivative_cis [derivative_intros]:
  assumes "(f has_derivative d) (at x within A)"
  shows   "((\x. cis (f x)) has_derivative (\t. d t *\<^sub>R (\ * cis (f x)))) (at x within A)"
proof (rule has_derivative_compose[OF assms])
  have cis_eq: "cis = (\x. cos x + \ * sin x)"
    by (auto simp: complex_eq_iff cos_of_real sin_of_real)
  have "(cis has_vector_derivative (\ * cis (f x))) (at (f x))"
    unfolding cis_eq by (auto intro!: derivative_eq_intros simp: cos_of_real sin_of_real algebra_simps)
  thus "(cis has_derivative (\a. a *\<^sub>R (\ * cis (f x)))) (at (f x))"
    by (simp add: has_vector_derivative_def)
qed

subsubsection \<open>Complex argument\<close>

definition Arg :: "complex \ real"
  where "Arg z = (if z = 0 then 0 else (SOME a. sgn z = cis a \ - pi < a \ a \ pi))"

lemma Arg_zero: "Arg 0 = 0"
  by (simp add: Arg_def)

lemma cis_Arg_unique:
  assumes "sgn z = cis x" and "-pi < x" and "x \ pi"
  shows "Arg z = x"
proof -
  from assms have "z \ 0" by auto
  have "(SOME a. sgn z = cis a \ -pi < a \ a \ pi) = x"
  proof
    fix a
    define d where "d = a - x"
    assume a: "sgn z = cis a \ - pi < a \ a \ pi"
    from a assms have "- (2*pi) < d \ d < 2*pi"
      unfolding d_def by simp
    moreover
    from a assms have "cos a = cos x" and "sin a = sin x"
      by (simp_all add: complex_eq_iff)
    then have cos: "cos d = 1"
      by (simp add: d_def cos_diff)
    moreover from cos have "sin d = 0"
      by (rule cos_one_sin_zero)
    ultimately have "d = 0"
      by (auto simp: sin_zero_iff elim!: evenE dest!: less_2_cases)
    then show "a = x"
      by (simp add: d_def)
  qed (simp add: assms del: Re_sgn Im_sgn)
  with \<open>z \<noteq> 0\<close> show "Arg z = x"
    by (simp add: Arg_def)
qed

lemma Arg_correct:
  assumes "z \ 0"
  shows "sgn z = cis (Arg z) \ -pi < Arg z \ Arg z \ pi"
proof (simp add: Arg_def assms, rule someI_ex)
  obtain r a where z: "z = rcis r a"
    using rcis_Ex by fast
  with assms have "r \ 0" by auto
  define b where "b = (if 0 < r then a else a + pi)"
  have b: "sgn z = cis b"
    using \<open>r \<noteq> 0\<close> by (simp add: z b_def rcis_def of_real_def sgn_scaleR sgn_if complex_eq_iff)
  have cis_2pi_nat: "cis (2 * pi * real_of_nat n) = 1" for n
    by (induct n) (simp_all add: distrib_left cis_mult [symmetric] complex_eq_iff)
  have cis_2pi_int: "cis (2 * pi * real_of_int x) = 1" for x
    by (cases x rule: int_diff_cases)
      (simp add: right_diff_distrib cis_divide [symmetric] cis_2pi_nat)
  define c where "c = b - 2 * pi * of_int \(b - pi) / (2 * pi)\"
  have "sgn z = cis c"
    by (simp add: b c_def cis_divide [symmetric] cis_2pi_int)
  moreover have "- pi < c \ c \ pi"
    using ceiling_correct [of "(b - pi) / (2*pi)"]
    by (simp add: c_def less_divide_eq divide_le_eq algebra_simps del: le_of_int_ceiling)
  ultimately show "\a. sgn z = cis a \ -pi < a \ a \ pi"
    by fast
qed

lemma Arg_bounded: "- pi < Arg z \ Arg z \ pi"
  by (cases "z = 0") (simp_all add: Arg_zero Arg_correct)

lemma cis_Arg: "z \ 0 \ cis (Arg z) = sgn z"
  by (simp add: Arg_correct)

lemma rcis_cmod_Arg: "rcis (cmod z) (Arg z) = z"
  by (cases "z = 0") (simp_all add: rcis_def cis_Arg sgn_div_norm of_real_def)

lemma rcis_cnj:
  shows "cnj a = rcis (cmod a) (- Arg a)"
  by (metis cis_cnj complex_cnj_complex_of_real complex_cnj_mult rcis_cmod_Arg rcis_def)

lemma cos_Arg_i_mult_zero [simp]: "y \ 0 \ Re y = 0 \ cos (Arg y) = 0"
  using cis_Arg [of y] by (simp add: complex_eq_iff)

lemma Arg_ii [simp]: "Arg \ = pi/2"
  by (rule cis_Arg_unique; simp add: sgn_eq)

lemma Arg_minus_ii [simp]: "Arg (-\) = -pi/2"
proof (rule cis_Arg_unique)
  show "sgn (- \) = cis (- pi / 2)"
    by (simp add: sgn_eq)
  show "- pi / 2 \ pi"
    using pi_not_less_zero by linarith
qed auto

lemma cos_Arg: "z \ 0 \ cos (Arg z) = Re z / norm z"
  by (metis Re_sgn cis.sel(1) cis_Arg)

lemma sin_Arg: "z \ 0 \ sin (Arg z) = Im z / norm z"
  by (metis Im_sgn cis.sel(2) cis_Arg)

subsection \<open>Complex n-th roots\<close>

lemma bij_betw_roots_unity:
  assumes "n > 0"
  shows   "bij_betw (\k. cis (2 * pi * real k / real n)) {..
    (is "bij_betw ?f _ _")
  unfolding bij_betw_def
proof (intro conjI)
  show inj: "inj_on ?f {.. unfolding inj_on_def
  proof (safe, goal_cases)
    case (1 k l)
    hence kl: "k < n" "l < n" by simp_all
    from 1 have "1 = ?f k / ?f l" by simp
    also have "\ = cis (2*pi*(real k - real l)/n)"
      using assms by (simp add: field_simps cis_divide)
    finally have "cos (2*pi*(real k - real l) / n) = 1"
      by (simp add: complex_eq_iff)
    then obtain m :: int where "2 * pi * (real k - real l) / real n = real_of_int m * 2 * pi"
      by (subst (asm) cos_one_2pi_int) blast
    hence "real_of_int (int k - int l) = real_of_int (m * int n)"
      unfolding of_int_diff of_int_mult using assms
      by (simp add: nonzero_divide_eq_eq)
    also note of_int_eq_iff
    finally have *: "abs m * n = abs (int k - int l)" by (simp add: abs_mult)
    also have "\ < int n" using kl by linarith
    finally have "m = 0" using assms by simp
    with * show "k = l" by simp
  qed

  have subset: "?f ` {.. {z. z ^ n = 1}"
  proof safe
    fix k :: nat
    have "cis (2 * pi * real k / real n) ^ n = cis (2 * pi) ^ k"
      using assms by (simp add: DeMoivre mult_ac)
    also have "cis (2 * pi) = 1" by (simp add: complex_eq_iff)
    finally show "?f k ^ n = 1" by simp
  qed

  have "n = card {.. by simp
  also from assms and subset have "\ \ card {z::complex. z ^ n = 1}"
    by (intro card_inj_on_le[OF inj]) (auto simp: finite_roots_unity)
  finally have card: "card {z::complex. z ^ n = 1} = n"
    using assms by (intro antisym card_roots_unity) auto

  have "card (?f ` {..
    using card inj by (subst card_image) auto
  with subset and assms show "?f ` {..
    by (intro card_subset_eq finite_roots_unity) auto
qed

lemma card_roots_unity_eq:
  assumes "n > 0"
  shows   "card {z::complex. z ^ n = 1} = n"
  using bij_betw_same_card [OF bij_betw_roots_unity [OF assms]] by simp

lemma bij_betw_nth_root_unity:
  fixes c :: complex and n :: nat
  assumes c: "c \ 0" and n: "n > 0"
  defines "c' \ root n (norm c) * cis (Arg c / n)"
  shows "bij_betw (\z. c' * z) {z. z ^ n = 1} {z. z ^ n = c}"
proof -
  have "c' ^ n = of_real (root n (norm c) ^ n) * cis (Arg c)"
    unfolding of_real_power using n by (simp add: c'_def power_mult_distrib DeMoivre)
  also from n have "root n (norm c) ^ n = norm c" by simp
  also from c have "of_real \ * cis (Arg c) = c" by (simp add: cis_Arg Complex.sgn_eq)
  finally have [simp]: "c' ^ n = c" .

  show ?thesis unfolding bij_betw_def inj_on_def
  proof safe
    fix z :: complex assume "z ^ n = 1"
    hence "(c' * z) ^ n = c' ^ n" by (simp add: power_mult_distrib)
    also have "c' ^ n = of_real (root n (norm c) ^ n) * cis (Arg c)"
      unfolding of_real_power using n by (simp add: c'_def power_mult_distrib DeMoivre)
    also from n have "root n (norm c) ^ n = norm c" by simp
    also from c have "\ * cis (Arg c) = c" by (simp add: cis_Arg Complex.sgn_eq)
    finally show "(c' * z) ^ n = c" .
  next
    fix z assume z: "c = z ^ n"
    define z' where "z' = z / c'"
    from c and n have "c' \ 0" by (auto simp: c'_def)
    with n c have "z = c' * z'" and "z' ^ n = 1"
      by (auto simp: z'_def power_divide z)
    thus "z \ (\z. c' * z) ` {z. z ^ n = 1}" by blast
  qed (insert c n, auto simp: c'_def)
qed

lemma finite_nth_roots [intro]:
  assumes "n > 0"
  shows   "finite {z::complex. z ^ n = c}"
proof (cases "c = 0")
  case True
  with assms have "{z::complex. z ^ n = c} = {0}" by auto
  thus ?thesis by simp
next
  case False
  from assms have "finite {z::complex. z ^ n = 1}" by (intro finite_roots_unity) simp_all
  also have "?this \ ?thesis"
    by (rule bij_betw_finite, rule bij_betw_nth_root_unity) fact+
  finally show ?thesis .
qed

lemma card_nth_roots:
  assumes "c \ 0" "n > 0"
  shows   "card {z::complex. z ^ n = c} = n"
proof -
  have "card {z. z ^ n = c} = card {z::complex. z ^ n = 1}"
    by (rule sym, rule bij_betw_same_card, rule bij_betw_nth_root_unity) fact+
  also have "\ = n" by (rule card_roots_unity_eq) fact+
  finally show ?thesis .
qed

lemma sum_roots_unity:
  assumes "n > 1"
  shows   "\{z::complex. z ^ n = 1} = 0"
proof -
  define \<omega> where "\<omega> = cis (2 * pi / real n)"
  have [simp]: "\ \ 1"
  proof
    assume "\ = 1"
    with assms obtain k :: int where "2 * pi / real n = 2 * pi * of_int k"
      by (auto simp: \<omega>_def complex_eq_iff cos_one_2pi_int)
    with assms have "real n * of_int k = 1" by (simp add: field_simps)
    also have "real n * of_int k = of_int (int n * k)" by simp
    also have "1 = (of_int 1 :: real)" by simp
    also note of_int_eq_iff
    finally show False using assms by (auto simp: zmult_eq_1_iff)
  qed

  have "(\z | z ^ n = 1. z :: complex) = (\k
    using assms by (intro sum.reindex_bij_betw [symmetric] bij_betw_roots_unity) auto
  also have "\ = (\k ^ k)"
    by (intro sum.cong refl) (auto simp: \<omega>_def DeMoivre mult_ac)
  also have "\ = (\ ^ n - 1) / (\ - 1)"
    by (subst geometric_sum) auto
  also have "\ ^ n - 1 = cis (2 * pi) - 1" using assms by (auto simp: \_def DeMoivre)
  also have "\ = 0" by (simp add: complex_eq_iff)
  finally show ?thesis by simp
qed

lemma sum_nth_roots:
  assumes "n > 1"
  shows   "\{z::complex. z ^ n = c} = 0"
proof (cases "c = 0")
  case True
  with assms have "{z::complex. z ^ n = c} = {0}" by auto
  also have "\\ = 0" by simp
  finally show ?thesis .
next
  case False
  define c' where "c' = root n (norm c) * cis (Arg c / n)"
  from False and assms have "(\{z. z ^ n = c}) = (\z | z ^ n = 1. c' * z)"
    by (subst sum.reindex_bij_betw [OF bij_betw_nth_root_unity, symmetric])
       (auto simp: sum_distrib_left finite_roots_unity c'_def)
  also from assms have "\ = 0"
    by (simp add: sum_distrib_left [symmetric] sum_roots_unity)
  finally show ?thesis .
qed

subsection \<open>Square root of complex numbers\<close>

primcorec csqrt :: "complex \ complex"
  where
    "Re (csqrt z) = sqrt ((cmod z + Re z) / 2)"
  | "Im (csqrt z) = (if Im z = 0 then 1 else sgn (Im z)) * sqrt ((cmod z - Re z) / 2)"

lemma csqrt_of_real_nonneg [simp]: "Im x = 0 \ Re x \ 0 \ csqrt x = sqrt (Re x)"
  by (simp add: complex_eq_iff norm_complex_def)

lemma csqrt_of_real_nonpos [simp]: "Im x = 0 \ Re x \ 0 \ csqrt x = \ * sqrt \Re x\"
  by (simp add: complex_eq_iff norm_complex_def)

lemma of_real_sqrt: "x \ 0 \ of_real (sqrt x) = csqrt (of_real x)"
  by (simp add: complex_eq_iff norm_complex_def)

lemma csqrt_0 [simp]: "csqrt 0 = 0"
  by simp

lemma csqrt_1 [simp]: "csqrt 1 = 1"
  by simp

lemma csqrt_ii [simp]: "csqrt \ = (1 + \) / sqrt 2"
  by (simp add: complex_eq_iff Re_divide Im_divide real_sqrt_divide real_div_sqrt)

lemma power2_csqrt[simp,algebra]: "(csqrt z)\<^sup>2 = z"
proof (cases "Im z = 0")
  case True
  then show ?thesis
    using real_sqrt_pow2[of "Re z"] real_sqrt_pow2[of "- Re z"]
    by (cases "0::real" "Re z" rule: linorder_cases)
      (simp_all add: complex_eq_iff Re_power2 Im_power2 power2_eq_square cmod_eq_Re)
next
  case False
  moreover have "cmod z * cmod z - Re z * Re z = Im z * Im z"
    by (simp add: norm_complex_def power2_eq_square)
  moreover have "\Re z\ \ cmod z"
    by (simp add: norm_complex_def)
  ultimately show ?thesis
    by (simp add: Re_power2 Im_power2 complex_eq_iff real_sgn_eq
        field_simps real_sqrt_mult[symmetric] real_sqrt_divide)
qed

lemma csqrt_power_even:
  assumes "even n"
  shows   "csqrt z ^ n = z ^ (n div 2)"
  by (metis assms dvd_mult_div_cancel power2_csqrt power_mult)

lemma norm_csqrt [simp]: "norm (csqrt z) = sqrt (norm z)"
  by (metis abs_of_nonneg norm_ge_zero norm_mult power2_csqrt power2_eq_square real_sqrt_abs)

lemma csqrt_eq_0 [simp]: "csqrt z = 0 \ z = 0"
  by auto (metis power2_csqrt power_eq_0_iff)

lemma csqrt_eq_1 [simp]: "csqrt z = 1 \ z = 1"
  by auto (metis power2_csqrt power2_eq_1_iff)

lemma csqrt_principal: "0 < Re (csqrt z) \ Re (csqrt z) = 0 \ 0 \ Im (csqrt z)"
  by (auto simp add: not_less cmod_plus_Re_le_0_iff Im_eq_0)

lemma Re_csqrt: "0 \ Re (csqrt z)"
  by (metis csqrt_principal le_less)

lemma csqrt_square:
  assumes "0 < Re b \ (Re b = 0 \ 0 \ Im b)"
  shows "csqrt (b^2) = b"
proof -
  have "csqrt (b^2) = b \ csqrt (b^2) = - b"
    by (simp add: power2_eq_iff[symmetric])
  moreover have "csqrt (b^2) \ -b \ b = 0"
    using csqrt_principal[of "b ^ 2"] assms
    by (intro disjCI notI) (auto simp: complex_eq_iff)
  ultimately show ?thesis
    by auto
qed

lemma csqrt_unique: "w\<^sup>2 = z \ 0 < Re w \ Re w = 0 \ 0 \ Im w \ csqrt z = w"
  by (auto simp: csqrt_square)

lemma csqrt_minus [simp]:
  assumes "Im x < 0 \ (Im x = 0 \ 0 \ Re x)"
  shows "csqrt (-x) = \ * csqrt x"
proof -
  have "csqrt ((\ * csqrt x)^2) = \ * csqrt x"
  proof (rule csqrt_square)
    have "Im (csqrt x) \ 0"
      using assms by (auto simp add: cmod_eq_Re mult_le_0_iff field_simps complex_Re_le_cmod)
    then show "0 < Re (\ * csqrt x) \ Re (\ * csqrt x) = 0 \ 0 \ Im (\ * csqrt x)"
      by (auto simp add: Re_csqrt simp del: csqrt.simps)
  qed
  also have "(\ * csqrt x)^2 = - x"
    by (simp add: power_mult_distrib)
  finally show ?thesis .
qed

lemma csqrt_neq_neg_real:
  assumes "Im x = 0" "Re x < 0"
  shows   "csqrt z \ x"
  using csqrt_principal[of z] assms by auto

lemma csqrt_of_real: "x \ 0 \ csqrt (of_real x) = of_real (sqrt x)"
  by (rule csqrt_unique) (auto simp flip: of_real_power)

lemma csqrt_of_real': "csqrt (of_real x) = of_real (sqrt \x\) * (if x \ 0 then 1 else \)"
  by (rule csqrt_unique) (auto simp flip: of_real_power simp: power_mult_distrib)

lemma csqrt_minus_Reals:
  assumes "x \ \"
  shows "csqrt (- x) = sgn (Re x) * \ * csqrt x"
proof (cases "Re x \ 0")
  case True
  then show ?thesis
    using assms complex_is_Real_iff sgn_1_pos by force
next
  case False
  then obtain "Im x = 0" "sgn (Re x) = -1"
    using assms complex_is_Real_iff by auto
  with False show ?thesis
    by auto
qed

lemmas cmod_def = norm_complex_def

lemma Complex_simps:
  shows Complex_eq_0: "Complex a b = 0 \ a = 0 \ b = 0"
    and complex_add: "Complex a b + Complex c d = Complex (a + c) (b + d)"
    and complex_minus: "- (Complex a b) = Complex (- a) (- b)"
    and complex_diff: "Complex a b - Complex c d = Complex (a - c) (b - d)"
    and Complex_eq_1: "Complex a b = 1 \ a = 1 \ b = 0"
    and Complex_eq_neg_1: "Complex a b = - 1 \ a = - 1 \ b = 0"
    and complex_mult: "Complex a b * Complex c d = Complex (a * c - b * d) (a * d + b * c)"
    and complex_inverse: "inverse (Complex a b) = Complex (a / (a\<^sup>2 + b\<^sup>2)) (- b / (a\<^sup>2 + b\<^sup>2))"
    and Complex_eq_numeral: "Complex a b = numeral w \ a = numeral w \ b = 0"
    and Complex_eq_neg_numeral: "Complex a b = - numeral w \ a = - numeral w \ b = 0"
    and complex_scaleR: "scaleR r (Complex a b) = Complex (r * a) (r * b)"
    and Complex_eq_i: "Complex x y = \ \ x = 0 \ y = 1"
    and i_mult_Complex: "\ * Complex a b = Complex (- b) a"
    and Complex_mult_i: "Complex a b * \ = Complex (- b) a"
    and i_complex_of_real: "\ * complex_of_real r = Complex 0 r"
    and complex_of_real_i: "complex_of_real r * \ = Complex 0 r"
    and Complex_add_complex_of_real: "Complex x y + complex_of_real r = Complex (x+r) y"
    and complex_of_real_add_Complex: "complex_of_real r + Complex x y = Complex (r+x) y"
    and Complex_mult_complex_of_real: "Complex x y * complex_of_real r = Complex (x*r) (y*r)"
    and complex_of_real_mult_Complex: "complex_of_real r * Complex x y = Complex (r*x) (r*y)"
    and complex_eq_cancel_iff2: "(Complex x y = complex_of_real xa) = (x = xa \ y = 0)"
    and complex_cnj: "cnj (Complex a b) = Complex a (- b)"
    and Complex_sum': "sum (\x. Complex (f x) 0) s = Complex (sum f s) 0"
    and Complex_sum: "Complex (sum f s) 0 = sum (\x. Complex (f x) 0) s"
    and complex_of_real_def: "complex_of_real r = Complex r 0"
    and complex_norm: "cmod (Complex x y) = sqrt (x\<^sup>2 + y\<^sup>2)"
  by (simp_all add: norm_complex_def field_simps complex_eq_iff Re_divide Im_divide)

lemma Complex_in_Reals: "Complex x 0 \ \"
  by (metis Reals_of_real complex_of_real_def)

lemma Complex_divide_complex_of_real: "Complex x y / of_real r = Complex (x/r) (y/r)"
  by (metis complex_of_real_mult_Complex divide_inverse mult.commute of_real_inverse)

lemma cmod_neg_real: "cmod (Complex (-x) y) = cmod (Complex x y)"
  by (metis complex_cnj complex_minus complex_mod_cnj norm_minus_cancel)

text \<open>Express a complex number as a linear combination of two others, not collinear with the origin\<close>
lemma complex_axes:
  assumes "Im (y/x) \ 0"
  obtains a b where "z = of_real a * x + of_real b * y"
proof -
  define dd where "dd \ Re y * Im x - Im y * Re x"
  define a where "a = (Im z * Re y - Re z * Im y) / dd"
  define b where "b = (Re z * Im x - Im z * Re x) / dd"
  have "dd \ 0"
    using assms by (auto simp: dd_def Im_complex_div_eq_0)
  have "a * Re x + b * Re y = Re z"
    using \<open>dd \<noteq> 0\<close>
    apply (simp add: a_def b_def field_simps)
    by (metis dd_def diff_add_cancel distrib_right mult.assoc mult.commute)
  moreover have "a * Im x + b * Im y = Im z"
    using \<open>dd \<noteq> 0\<close>
    apply (simp add: a_def b_def field_simps)
    by (metis (no_types) dd_def diff_add_cancel distrib_right mult.assoc mult.commute)
  ultimately have "z = of_real a * x + of_real b * y"
    by (simp add: complex_eqI)
  then show ?thesis using that by simp
qed

end

quality100%

¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.17Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.