# Theory CLim

```(*  Title:      HOL/Nonstandard_Analysis/CLim.thy
Author:     Jacques D. Fleuriot
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 epsilon_not_zero [simp]

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

text ‹Changing the quantified variable. Install earlier?›
lemma all_shift: "(∀x::'a::comm_ring_1. P x) ⟷ (∀x. P (x - a))"

subsection ‹Limit of Complex to Complex Function›

lemma NSLIM_Re: "f ─a→⇩N⇩S L ⟹ (λx. Re (f x)) ─a→⇩N⇩S Re L"
by (simp add: NSLIM_def starfunC_approx_Re_Im_iff hRe_hcomplex_of_complex)

lemma NSLIM_Im: "f ─a→⇩N⇩S L ⟹ (λx. Im (f x)) ─a→⇩N⇩S Im L"
by (simp add: NSLIM_def starfunC_approx_Re_Im_iff hIm_hcomplex_of_complex)

lemma LIM_Re: "f ─a→ L ⟹ (λx. Re (f x)) ─a→ Re L"
for f :: "'a::real_normed_vector ⇒ complex"

lemma LIM_Im: "f ─a→ L ⟹ (λx. Im (f x)) ─a→ Im L"
for f :: "'a::real_normed_vector ⇒ complex"

lemma LIM_cnj: "f ─a→ L ⟹ (λx. cnj (f x)) ─a→ cnj L"
for f :: "'a::real_normed_vector ⇒ complex"
by (simp add: LIM_eq complex_cnj_diff [symmetric] del: complex_cnj_diff)

lemma LIM_cnj_iff: "((λx. cnj (f x)) ─a→ cnj L) ⟷ f ─a→ L"
for f :: "'a::real_normed_vector ⇒ complex"
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])

text ‹Much, much easier standard proof.›
lemma CLIM_CRLIM_iff: "f ─x→ L ⟷ (λy. cmod (f y - L)) ─x→ 0"
for f :: "'a::real_normed_vector ⇒ complex"

text ‹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: "f ─a→ L ⟷ (λx. Re (f x)) ─a→ Re L ∧ (λx. Im (f x)) ─a→ Im L"
for f :: "'a::real_normed_vector ⇒ complex"

subsection ‹Continuity›

lemma NSLIM_isContc_iff: "f ─a→⇩N⇩S f a ⟷ (λh. f (a + h)) ─0→⇩N⇩S f a"
by (rule NSLIM_at0_iff)

subsection ‹Functions from Complex to Reals›

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

lemma isContCR_cmod [simp]: "isCont cmod a"

lemma isCont_Re: "isCont f a ⟹ isCont (λx. Re (f x)) a"
for f :: "'a::real_normed_vector ⇒ complex"

lemma isCont_Im: "isCont f a ⟹ isCont (λx. Im (f x)) a"
for f :: "'a::real_normed_vector ⇒ complex"

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 ≠ 0 ⟹ NSDERIV (λx. inverse x) x :> - (inverse x)⇧2"
for x :: complex
unfolding numeral_2_eq_2 by (rule NSDERIV_inverse)

lemma CDERIV_inverse: "x ≠ 0 ⟹ DERIV (λx. inverse x) x :> - (inverse x)⇧2"
for x :: complex
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 ⟹ DERIV (λx. inverse (f x)) x :> - (d * inverse ((f x)⇧2))"
for x :: complex
unfolding numeral_2_eq_2 by (rule DERIV_inverse_fun)

lemma NSCDERIV_inverse_fun:
"NSDERIV f x :> d ⟹ f x ≠ 0 ⟹ NSDERIV (λx. inverse (f x)) x :> - (d * inverse ((f x)⇧2))"
for x :: complex
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 ⟹
DERIV (λy. f y / g y) x :> (d * g x - (e * f x)) / (g x)⇧2"
for x :: complex
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
```