| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/vect_analysis/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 5 kB |
|
Quelle limit_vect3_real.pvs Sprache: PVS |
|||||||||
|
limit_vect3_real: THEORY
BEGIN IMPORTING vectors@vect3_fun_ops, reals@abs_lems, analysis@epsilon_lemmas f, f1, f2: VAR [ Vect3 -> real] g : VAR [Vect3 -> nzreal] epsilon, delta : VAR posreal a,x,v: VAR Vect3 l,l1,l2,b,c,y1,y2: VAR real %--------------------------------------------------- % Convergence of f at a point a towards a limit l %--------------------------------------------------- convergence(f, a, l) : bool = FORALL epsilon : EXISTS delta : FORALL x: %%% 0 < norm(x-a) AND norm(x-a) < delta %% AND x in dom(f) IMPLIES abs(f(x) - l) < epsilon 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_neg : LEMMA convergence(f, a, l) IMPLIES convergence(- f, a, - l) 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), v, b) cv_scal : LEMMA convergence(f, a, l) IMPLIES convergence(b * f, a, b * l) cv_inv : LEMMA convergence(g, a, l) AND l /= 0 IMPLIES convergence(1 / g, a, 1 / l) cv_div : LEMMA convergence(f, a, l1) AND convergence(g, a, l2) AND l2 /= 0 IMPLIES convergence(f / g, a, l1 / l2) %------------------------- % f is convergent at a %------------------------- convergent?(f, a) : bool = EXISTS l : convergence(f, a, l) lim(f, (x0 : {a | convergent?(f, a)})) : real = epsilon(LAMBDA l : 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) 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), v) 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) %---------------------------- % 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), v) = 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) %----------------------------- % Limit preserve order %----------------------------- convergence_order : LEMMA FORALL f1, f2, a, l1, l2 : convergence(f1, a, l1) AND convergence(f2, a, l2) AND (FORALL x : f1(x) <= f2(x)) IMPLIES l1 <= l2 %------------------------------------------- % Bounds on function are bounds on limits %------------------------------------------- convergence_lower_bound : COROLLARY FORALL f, b, a, l : convergence(f, a, l) AND (FORALL x : b <= f(x)) IMPLIES b <= l convergence_upper_bound : COROLLARY FORALL f, b, a, l : convergence(f, a, l) AND (FORALL x : f(x) <= b) IMPLIES l <= b %-------------------- % Bounds on limits %-------------------- 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) END limit_vect3_real ¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28