| products/sources/formale sprachen/PVS/vect_analysis/ |
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei: Ideal.thy Sprache: Unknown
|
limit_vect[n,m:posnat]: THEORY
BEGIN IMPORTING vectors@vectors, reals@abs_lems, analysis@epsilon_lemmas f, f1, f2: VAR [ Vector[n] -> Vector[m] ] a,b,x,v : VAR Vector[n] l,l1,l2 : VAR Vector[m] epsilon, delta : VAR posreal k : VAR real ;+(f1, f2)(v) : MACRO Vector[m] = f1(v) + f2(v) ;-(f)(v): MACRO Vector[m] = -f(v) ;-(f1, f2)(v) : MACRO Vector[m] = f1(v) - f2(v) ;*(k, f)(v) : MACRO Vector[m] = k*f(v) ;*(f1,f2)(v) : MACRO real = f1(v)*f2(v) const_fun(l)(x): Vector[m] = l %--------------------------------------------------- % Convergence of f at a point a towards a limit l %-------------------------------------------------- convergence(f, a, l): bool = FORALL epsilon : EXISTS delta : FORALL v: norm(v-a) < delta IMPLIES norm(f(v) - l) < epsilon cv_unique : LEMMA convergence(f, a, l1) AND convergence(f, a, l2) IMPLIES l1 = l2 cv_in_domain : LEMMA convergence(f, a, l) IMPLIES l = f(a) %------------------------------------------- % 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_const : LEMMA convergence(LAMBDA v: l, a, l) cv_scal : LEMMA convergence(f, a, l) IMPLIES convergence(k*f, a, k*l) %------------------------- % f is convergent at a %------------------------- convergent?(f, a) : bool = EXISTS l : convergence(f, a, l) lim(f, (x0 : {a | convergent?(f, a)})) : Vector[m] = choose(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 convergnce 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(l), a) scal_fun_convergent : LEMMA convergent?(f, a) IMPLIES convergent?(k * f, 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(l), a) = l lim_scal_fun : LEMMA convergent?(f, a) IMPLIES lim(k * f, a) = k * lim(f, a) END limit_vect [ zur Elbe Produktseite wechseln0.1Quellennavigators Analyse erneut starten ] |