(* Title: HOL/Nonstandard_Analysis/CLim.thy Author: Jacques D. Fleuriot Copyright: 2001 University of Edinburgh Conversion to Isar and new proofs by Lawrence C Paulson, 2004
*)
section \<open>Limits, Continuity and Differentiation for Complex Functions\<close>
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)\<^sup>2 = inverse x" for x :: complex by (simp add: numeral_2_eq_2)
text\<open>Changing the quantified variable. Install earlier?\<close> lemma all_shift: "(\x::'a::comm_ring_1. P x) \ (\x. P (x - a))" by (metis add_diff_cancel)
subsection \<open>Limit of Complex to Complex Function\<close>
lemma NSLIM_Re: "f \a\\<^sub>N\<^sub>S L \ (\x. Re (f x)) \a\\<^sub>N\<^sub>S Re L" by (simp add: NSLIM_def starfunC_approx_Re_Im_iff hRe_hcomplex_of_complex)
lemma NSLIM_Im: "f \a\\<^sub>N\<^sub>S L \ (\x. Im (f x)) \a\\<^sub>N\<^sub>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" by (simp add: LIM_NSLIM_iff NSLIM_Re)
lemma LIM_Im: "f \a\ L \ (\x. Im (f x)) \a\ Im L" for f :: "'a::real_normed_vector \ complex" by (simp add: LIM_NSLIM_iff NSLIM_Im)
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\<open>Another equivalence result.\<close> lemma NSCLIM_NSCRLIM_iff: "f \x\\<^sub>N\<^sub>S L \ (\y. cmod (f y - L)) \x\\<^sub>N\<^sub>S 0" by (simp add: NSLIM_def starfun_norm
approx_approx_zero_iff [symmetric] approx_minus_iff [symmetric])
text\<open>Much, much easier standard proof.\<close> lemma CLIM_CRLIM_iff: "f \x\ L \ (\y. cmod (f y - L)) \x\ 0" for f :: "'a::real_normed_vector \ complex" by (simp add: LIM_eq)
text\<open>So this is nicer nonstandard proof.\<close> lemma NSCLIM_NSCRLIM_iff2: "f \x\\<^sub>N\<^sub>S L \ (\y. cmod (f y - L)) \x\\<^sub>N\<^sub>S 0" by (simp add: LIM_NSLIM_iff [symmetric] CLIM_CRLIM_iff)
lemma NSLIM_NSCRLIM_Re_Im_iff: "f \a\\<^sub>N\<^sub>S L \ (\x. Re (f x)) \a\\<^sub>N\<^sub>S Re L \ (\x. Im (f x)) \a\\<^sub>N\<^sub>S Im L" apply (auto intro: NSLIM_Re NSLIM_Im) apply (auto simp add: NSLIM_def starfun_Re starfun_Im) apply (auto dest!: spec) apply (simp add: hcomplex_approx_iff) 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" by (simp add: LIM_NSLIM_iff NSLIM_NSCRLIM_Re_Im_iff)
subsection \<open>Continuity\<close>
lemma NSLIM_isContc_iff: "f \a\\<^sub>N\<^sub>S f a \ (\h. f (a + h)) \0\\<^sub>N\<^sub>S f a" by (rule NSLIM_at0_iff)
subsection \<open>Functions from Complex to Reals\<close>
text\<open>Nonstandard version.\<close> 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\<open>Can't relax the premise \<^term>\<open>x \<noteq> 0\<close>: it isn't continuous at zero.\<close> lemma NSCDERIV_inverse: "x \ 0 \ NSDERIV (\x. inverse x) x :> - (inverse x)\<^sup>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)\<^sup>2" for x :: complex unfolding numeral_2_eq_2 by (rule DERIV_inverse)
subsection \<open>Derivative of Reciprocals (Function \<^term>\<open>inverse\<close>)\<close>
lemma CDERIV_inverse_fun: "DERIV f x :> d \ f x \ 0 \ DERIV (\x. inverse (f x)) x :> - (d * inverse ((f x)\<^sup>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)\<^sup>2))" for x :: complex unfolding numeral_2_eq_2 by (rule NSDERIV_inverse_fun)
subsection \<open>Derivative of Quotient\<close>
lemma CDERIV_quotient: "DERIV f x :> d \ DERIV g x :> e \ g(x) \ 0 \
DERIV (\<lambda>y. f y / g y) x :> (d * g x - (e * f x)) / (g x)\<^sup>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 (\<lambda>y. f y / g y) x :> (d * g x - (e * f x)) / (g x)\<^sup>2" unfolding numeral_2_eq_2 by (rule NSDERIV_quotient)
subsection \<open>Caratheodory Formulation of Derivative at a Point: Standard Proof\<close>
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
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤
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.
