# Theory CLim

theory CLim
imports CStar
```(*  Title       : CLim.thy
Author      : Jacques D. Fleuriot
Copyright   : 2001 University of Edinburgh
Conversion to Isar and new proofs by Lawrence C Paulson, 2004
*)

section‹Limits, Continuity and Differentiation for Complex Functions›

theory CLim
imports CStar
begin

(*not in simpset?*)
declare hypreal_epsilon_not_zero [simp]

(*??generalize*)
lemma lemma_complex_mult_inverse_squared [simp]:
"x ≠ (0::complex) ⟹ x * (inverse x)⇧2 = inverse x"

text‹Changing the quantified variable. Install earlier?›
lemma all_shift: "(∀x::'a::comm_ring_1. P x) = (∀x. P (x-a))"
apply auto
apply (drule_tac x="x+a" in spec)
done

lemma complex_add_minus_iff [simp]: "(x + - a = (0::complex)) = (x=a)"

lemma complex_add_eq_0_iff [iff]: "(x+y = (0::complex)) = (y = -x)"
apply auto
apply (drule sym [THEN diff_eq_eq [THEN iffD2]], auto)
done

subsection‹Limit of Complex to Complex Function›

lemma NSLIM_Re: "f ─a→⇩N⇩S L ==> (%x. Re(f x)) ─a→⇩N⇩S Re(L)"
hRe_hcomplex_of_complex)

lemma NSLIM_Im: "f ─a→⇩N⇩S L ==> (%x. Im(f x)) ─a→⇩N⇩S Im(L)"
hIm_hcomplex_of_complex)

(** get this result easily now **)
lemma LIM_Re:
fixes f :: "'a::real_normed_vector ⇒ complex"
shows "f ─a→ L ==> (%x. Re(f x)) ─a→ Re(L)"

lemma LIM_Im:
fixes f :: "'a::real_normed_vector ⇒ complex"
shows "f ─a→ L ==> (%x. Im(f x)) ─a→ Im(L)"

lemma LIM_cnj:
fixes f :: "'a::real_normed_vector ⇒ complex"
shows "f ─a→ L ==> (%x. cnj (f x)) ─a→ cnj L"
by (simp add: LIM_eq complex_cnj_diff [symmetric] del: complex_cnj_diff)

lemma LIM_cnj_iff:
fixes f :: "'a::real_normed_vector ⇒ complex"
shows "((%x. cnj (f x)) ─a→ cnj L) = (f ─a→ L)"
by (simp add: LIM_eq complex_cnj_diff [symmetric] del: complex_cnj_diff)

lemma starfun_norm: "( *f* (λx. norm (f x))) = (λx. hnorm (( *f* f) x))"
by transfer (rule refl)

lemma star_of_Re [simp]: "star_of (Re x) = hRe (star_of x)"
by transfer (rule refl)

lemma star_of_Im [simp]: "star_of (Im x) = hIm (star_of x)"
by transfer (rule refl)

text""
(** another equivalence result **)
lemma NSCLIM_NSCRLIM_iff:
"(f ─x→⇩N⇩S L) = ((%y. cmod(f y - L)) ─x→⇩N⇩S 0)"
approx_approx_zero_iff [symmetric] approx_minus_iff [symmetric])

(** much, much easier standard proof **)
lemma CLIM_CRLIM_iff:
fixes f :: "'a::real_normed_vector ⇒ complex"
shows "(f ─x→ L) = ((%y. cmod(f y - L)) ─x→ 0)"

(* so this is nicer nonstandard proof *)
lemma NSCLIM_NSCRLIM_iff2:
"(f ─x→⇩N⇩S L) = ((%y. cmod(f y - L)) ─x→⇩N⇩S 0)"
by (simp add: LIM_NSLIM_iff [symmetric] CLIM_CRLIM_iff)

lemma NSLIM_NSCRLIM_Re_Im_iff:
"(f ─a→⇩N⇩S L) = ((%x. Re(f x)) ─a→⇩N⇩S Re(L) &
(%x. Im(f x)) ─a→⇩N⇩S Im(L))"
apply (auto intro: NSLIM_Re NSLIM_Im)
apply (auto simp add: NSLIM_def starfun_Re starfun_Im)
apply (auto dest!: spec)
done

lemma LIM_CRLIM_Re_Im_iff:
fixes f :: "'a::real_normed_vector ⇒ complex"
shows "(f ─a→ L) = ((%x. Re(f x)) ─a→ Re(L) &
(%x. Im(f x)) ─a→ Im(L))"

subsection‹Continuity›

lemma NSLIM_isContc_iff:
"(f ─a→⇩N⇩S f a) = ((%h. f(a + h)) ─0→⇩N⇩S f a)"
by (rule NSLIM_h_iff)

subsection‹Functions from Complex to Reals›

lemma isNSContCR_cmod [simp]: "isNSCont cmod (a)"
by (auto intro: approx_hnorm
isNSCont_def)

lemma isContCR_cmod [simp]: "isCont cmod (a)"

lemma isCont_Re:
fixes f :: "'a::real_normed_vector ⇒ complex"
shows "isCont f a ==> isCont (%x. Re (f x)) a"

lemma isCont_Im:
fixes f :: "'a::real_normed_vector ⇒ complex"
shows "isCont f a ==> isCont (%x. Im (f x)) a"

subsection‹Differentiation of Natural Number Powers›

lemma CDERIV_pow [simp]:
"DERIV (%x. x ^ n) x :> (complex_of_real (real n)) * (x ^ (n - Suc 0))"
apply (induct n)
apply (drule_tac [2] DERIV_ident [THEN DERIV_mult])
apply (auto simp add: distrib_right of_nat_Suc)
apply (case_tac "n")
done

text‹Nonstandard version›
lemma NSCDERIV_pow: "NSDERIV (%x. x ^ n) x :> complex_of_real (real n) * (x ^ (n - 1))"
by (metis CDERIV_pow NSDERIV_DERIV_iff One_nat_def)

text‹Can't relax the premise @{term "x ≠ 0"}: it isn't continuous at zero›
lemma NSCDERIV_inverse:
"(x::complex) ≠ 0 ==> NSDERIV (%x. inverse(x)) x :> (- ((inverse x)⇧2))"
unfolding numeral_2_eq_2
by (rule NSDERIV_inverse)

lemma CDERIV_inverse:
"(x::complex) ≠ 0 ==> DERIV (%x. inverse(x)) x :> (- ((inverse x)⇧2))"
unfolding numeral_2_eq_2
by (rule DERIV_inverse)

subsection‹Derivative of Reciprocals (Function @{term inverse})›

lemma CDERIV_inverse_fun:
"[| DERIV f x :> d; f(x) ≠ (0::complex) |]
==> DERIV (%x. inverse(f x)) x :> (- (d * inverse ((f x)⇧2)))"
unfolding numeral_2_eq_2
by (rule DERIV_inverse_fun)

lemma NSCDERIV_inverse_fun:
"[| NSDERIV f x :> d; f(x) ≠ (0::complex) |]
==> NSDERIV (%x. inverse(f x)) x :> (- (d * inverse ((f x)⇧2)))"
unfolding numeral_2_eq_2
by (rule NSDERIV_inverse_fun)

subsection‹Derivative of Quotient›

lemma CDERIV_quotient:
"[| DERIV f x :> d; DERIV g x :> e; g(x) ≠ (0::complex) |]
==> DERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / ((g x)⇧2)"
unfolding numeral_2_eq_2
by (rule DERIV_quotient)

lemma NSCDERIV_quotient:
"[| NSDERIV f x :> d; NSDERIV g x :> e; g(x) ≠ (0::complex) |]
==> NSDERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / ((g x)⇧2)"
unfolding numeral_2_eq_2
by (rule NSDERIV_quotient)

subsection‹Caratheodory Formulation of Derivative at a Point: Standard Proof›

lemma CARAT_CDERIVD:
"(∀z. f z - f x = g z * (z - x)) & isNSCont g x & g x = l
==> NSDERIV f x :> l"
by clarify (rule CARAT_DERIVD)

end
```