| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/analysis/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 4 kB |
|
Quelle convergence_functions.pvs Sprache: PVS |
|||||||||
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% General convergence of functions [T -> real] % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% convergence_functions [T : TYPE FROM real] : THEORY BEGIN IMPORTING reals@real_fun_ops, epsilon_lemmas epsilon, delta : VAR posreal e, e1, e2 : VAR posreal E, E1, E2 : VAR setof[real] f, f1, f2 : VAR [T -> real] g : VAR [T -> nzreal] l, l1, l2, a, b, z : VAR real x, y : VAR T %--------------------------- % Reals adherent to a set %--------------------------- adh(E) : setof[real] = { z | FORALL e : EXISTS x : E(x) AND abs(x - z) < e } member_adherent : LEMMA E(x) IMPLIES adh(E)(x) adherence_subset1 : LEMMA subset?(E1, E2) AND adh(E1)(z) IMPLIES adh(E2)(z) adherence_subset2 : LEMMA subset?(E1, E2) IMPLIES subset?(adh(E1), adh(E2)) adherence_prop1 : LEMMA FORALL e, E, (a : (adh(E))) : EXISTS x : E(x) AND abs(x - a) < e adherence_prop2 : LEMMA FORALL e1, e2, E, (a : (adh(E))) : EXISTS x : E(x) AND abs(x - a) < e1 AND abs(x - a) < e2 %------------------------------------------------------ % Definition of convergence and immediate properties %------------------------------------------------------ convergence(f, E, a, l) : bool = adh(E)(a) AND FORALL epsilon : EXISTS delta : FORALL x : E(x) AND abs(x - a) < delta IMPLIES abs(f(x) - l) < epsilon convergence_unicity : LEMMA FORALL E, f, a, l1, l2 : convergence(f, E, a, l1) AND convergence(f, E, a, l2) IMPLIES l1 = l2 subset_convergence : LEMMA subset?(E1, E2) IMPLIES FORALL f, (a : (adh(E1))), l : convergence(f, E2, a, l) IMPLIES convergence(f, E1, a, l) subset_convergence2 : LEMMA FORALL E1, E2, f, (a : (adh(E1))), l : subset?(E1, E2) AND convergence(f, E2, a, l) IMPLIES convergence(f, E1, a, l) convergence_in_domain : LEMMA FORALL f, x, l : E(x) AND convergence(f, E, x, l) IMPLIES l = f(x) %---------------------------------- % Limits and function operations %---------------------------------- convergence_sum : LEMMA FORALL E, f1, f2, a, l1, l2 : convergence(f1, E, a, l1) AND convergence(f2, E, a, l2) IMPLIES convergence(f1 + f2, E, a, l1 + l2) convergence_neg : LEMMA FORALL E, f1, a, l1 : convergence(f1, E, a, l1) IMPLIES convergence(- f1, E, a, - l1) convergence_diff : LEMMA FORALL E, f1, f2, a, l1, l2 : convergence(f1, E, a, l1) AND convergence(f2, E, a, l2) IMPLIES convergence(f1 - f2, E, a, l1 - l2) convergence_prod : LEMMA FORALL E, f1, f2, a, l1, l2 : convergence(f1, E, a, l1) AND convergence(f2, E, a, l2) IMPLIES convergence(f1 * f2, E, a, l1 * l2) convergence_const : LEMMA FORALL E, (a : (adh(E))), b : convergence(const_fun(b), E, a, b) convergence_scal : LEMMA FORALL E, f1, a, l1, b : convergence(f1, E, a, l1) IMPLIES convergence(b * f1, E, a, b * l1) convergence_inv : LEMMA FORALL E, g, a, l1: convergence(g, E, a, l1) AND l1 /= 0 IMPLIES convergence(1/g, E, a, 1/l1) convergence_div : LEMMA FORALL E, f, g, a, l1, l2 : convergence(f, E, a, l1) AND convergence(g, E, a, l2) AND l2 /= 0 IMPLIES convergence(f/g, E, a, l1/l2) %--------------------- % Identity function %--------------------- convergence_identity : LEMMA FORALL E, (a : (adh(E))) : convergence(I[T], E, a, a) %----------------------------- % Limit preserve order %----------------------------- convergence_order : LEMMA FORALL E, f1, f2, a, l1, l2 : convergence(f1, E, a, l1) AND convergence(f2, E, a, l2) AND (FORALL x : E(x) IMPLIES f1(x) <= f2(x)) IMPLIES l1 <= l2 %------------------------------------------- % Bounds on function are bounds on limits %------------------------------------------- convergence_lower_bound : COROLLARY FORALL E, f, b, a, l : convergence(f, E, a, l) AND (FORALL x : E(x) IMPLIES b <= f(x)) IMPLIES b <= l convergence_upper_bound : COROLLARY FORALL E, f, b, a, l : convergence(f, E, a, l) AND (FORALL x : E(x) IMPLIES f(x) <= b) IMPLIES l <= b %-------------------------- % Function constant on E %-------------------------- convergence_locally_constant : LEMMA FORALL E, f, b, (a : (adh(E))) : (FORALL x : E(x) IMPLIES f(x) = b) IMPLIES convergence(f, E, a, b) %------------- % Squeezing %------------- convergence_squeezing : LEMMA FORALL f1, f2, f, a, l : convergence(f1, E, a, l) AND convergence(f2, E, a, l) AND (FORALL x : E(x) IMPLIES f1(x) <= f(x) AND f(x) <= f2(x)) IMPLIES convergence(f, E, a, l) END convergence_functions ¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28