| products/sources/formale Sprachen/PVS/analysis/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: lim_of_functions.pvs Sprache: PVSOriginal von: PVS© |
|
||||||
|
lim_of_functions [ T : TYPE FROM real ] : THEORY
%---------------------------------------------------------------------------- % Limit of a functions [T -> real] at a point a % % % Author: Bruno Dutertre Royal Holloway & Bedford New College %---------------------------------------------------------------------------- BEGIN IMPORTING convergence_functions %------------------------------------------------ % Subtype of reals where the limit makes sense %------------------------------------------------ a, b, l, l1, l2 : VAR real c : VAR (adh[T](fullset[real])) f, f1, f2 : VAR [ T -> real] g : VAR [T -> nzreal] epsilon, delta : VAR posreal x : VAR T %--------------------------------------------------- % Convergence of f at a point a towards a limit l %--------------------------------------------------- convergence(f, a, l) : bool = convergence(f, fullset[real], a, l) convergence_def : LEMMA FORALL f, a, l : convergence(f, a, l) IFF adh[T](fullset[real])(a) AND FORALL epsilon : EXISTS delta : FORALL x : abs(x - a) < delta IMPLIES abs(f(x) - l) < epsilon adherence_fullset : LEMMA adh[T](fullset[real])(x) cv_unique : LEMMA convergence(f, a, l1) AND convergence(f, a, l2) IMPLIES l1 = l2 cv_in_domain : LEMMA convergence(f, x, l) IMPLIES l = f(x) %------------------------------------------- % convergence and operations on functions %------------------------------------------- cv_sum : LEMMA convergence(f1, a, l1) AND convergence(f2, a, l2) IMPLIES convergence(f1 + f2, a, l1 + l2) cv_diff : LEMMA convergence(f1, a, l1) AND convergence(f2, a, l2) IMPLIES convergence(f1 - f2, a, l1 - l2) cv_prod : LEMMA convergence(f1, a, l1) AND convergence(f2, a, l2) IMPLIES convergence(f1 * f2, a, l1 * l2) cv_const : LEMMA convergence(const_fun(b), c, b) cv_scal : LEMMA convergence(f, a, l) IMPLIES convergence(b * f, a, b * l) cv_neg : LEMMA convergence(f, a, l) IMPLIES convergence(- f, a, - l) cv_div : LEMMA convergence(f, a, l1) AND convergence(g, a, l2) AND l2 /= 0 IMPLIES convergence(f / g, a, l1 / l2) cv_inv : LEMMA convergence(g, a, l) AND l /= 0 IMPLIES convergence(1 / g, a, 1 / l) cv_identity: LEMMA convergence(I[T], c, c) cv_abs : LEMMA convergence(abs, c, abs(c)) conv_0_0_abs: LEMMA convergence(f, 0, 0) IFF convergence(abs(f), 0, 0) %------------------------- % f is convergent at a %------------------------- convergent?(f, a) : bool = EXISTS l : convergence(f, a, l) % lim(f, (x0 : {a | convergent?(f, a)})) : real = % choose(LAMBDA l : convergence(f, x0, l)) lim(f, (x0 : {a | convergent?(f, a)})) : {l: real | convergence(f, x0, l)} lim_fun_lemma : LEMMA FORALL f, (x0 : {a | convergent?(f, a)}) : convergence(f, x0, lim(f, x0)) lim_fun_def : LEMMA FORALL f, l, (x0 : {a | convergent?(f, a)}) : lim(f, x0) = l IFF convergence(f, x0, l) lim_e_del: LEMMA convergent?(f, a) IMPLIES (lim(f, a) = l IFF FORALL (e: posreal): EXISTS (del: posreal): FORALL (x: T): abs(x-a) < del IMPLIES abs(f(x) - l) < e) convergence_equiv : LEMMA convergence(f, a, l) IFF convergent?(f, a) AND lim(f, a) = l convergent_in_domain : LEMMA convergent?(f, x) IFF convergence(f, x, f(x)) lim_in_domain : LEMMA convergent?(f, x) IMPLIES lim(f, x) = f(x) %------------------------------------------ % Operations preserving convergence at a %------------------------------------------ sum_fun_convergent : LEMMA convergent?(f1, a) AND convergent?(f2, a) IMPLIES convergent?(f1 + f2, a) neg_fun_convergent : LEMMA convergent?(f, a) IMPLIES convergent?(- f, a) diff_fun_convergent : LEMMA convergent?(f1, a) AND convergent?(f2, a) IMPLIES convergent?(f1 - f2, a) prod_fun_convergent : LEMMA convergent?(f1, a) AND convergent?(f2, a) IMPLIES convergent?(f1 * f2, a) const_fun_convergent: LEMMA convergent?(const_fun(b), c) scal_fun_convergent : LEMMA convergent?(f, a) IMPLIES convergent?(b * f, a) inv_fun_convergent : LEMMA convergent?(g, a) AND lim(g, a) /= 0 IMPLIES convergent?(1/g, a) div_fun_convergent : LEMMA convergent?(f, a) AND convergent?(g, a) AND lim(g, a) /= 0 IMPLIES convergent?(f / g, a) convergent_identity : LEMMA convergent?(I[T], c) %---------------------------- % Same things with lim(a) %---------------------------- lim_sum_fun : LEMMA convergent?(f1, a) AND convergent?(f2, a) IMPLIES lim(f1 + f2, a) = lim(f1, a) + lim(f2, a) lim_neg_fun : LEMMA convergent?(f, a) IMPLIES lim(- f, a) = - lim(f, a) lim_diff_fun : LEMMA convergent?(f1, a) AND convergent?(f2, a) IMPLIES lim(f1 - f2, a) = lim(f1, a) - lim(f2, a) lim_prod_fun : LEMMA convergent?(f1, a) AND convergent?(f2, a) IMPLIES lim(f1 * f2, a) = lim(f1, a) * lim(f2, a) lim_const_fun : LEMMA lim(const_fun(b), c) = b lim_scal_fun : LEMMA convergent?(f, a) IMPLIES lim(b * f, a) = b * lim(f, a) lim_inv_fun : LEMMA convergent?(g, a) AND lim(g, a) /= 0 IMPLIES lim(1/g, a) = 1/lim(g, a) lim_div_fun : LEMMA convergent?(f, a) AND convergent?(g, a) AND lim(g, a) /= 0 IMPLIES lim(f / g, a) = lim(f, a)/lim(g, a) lim_identity : LEMMA lim(I[T], c) = c %-------------------- % Bounds on limits %-------------------- E : VAR setof[real] lim_le1 : LEMMA convergent?(f, a) AND (FORALL x : f(x) <= b) IMPLIES lim(f, a) <= b lim_ge1 : LEMMA convergent?(f, a) AND (FORALL x : f(x) >= b) IMPLIES lim(f, a) >= b lim_order1 : LEMMA convergent?(f1, a) AND convergent?(f2, a) AND (FORALL x : f1(x) <= f2(x)) IMPLIES lim(f1, a) <= lim(f2, a) lim_le2 : LEMMA convergent?(f, a) AND adh[T](E)(a) AND (FORALL x : E(x) IMPLIES f(x) <= b) IMPLIES lim(f, a) <= b lim_ge2 : LEMMA convergent?(f, a) AND adh[T](E)(a) AND (FORALL x : E(x) IMPLIES f(x) >= b) IMPLIES lim(f, a) >= b lim_order2 : LEMMA convergent?(f1, a) AND convergent?(f2, a) AND adh[T](E)(a) AND (FORALL x : E(x) IMPLIES f1(x) <= f2(x)) IMPLIES lim(f1, a) <= lim(f2, a) AUTO_REWRITE+ adherence_fullset END lim_of_functions ¤ Dauer der Verarbeitung: 0.20 Sekunden (vorverarbeitet) ¤ |
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.Bot Zugriff |
