| 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 3 kB |
|
Quelle cont_real_vect2.pvs Sprache: PVS |
|||||||||
|
cont_real_vect2[T : TYPE FROM real]: THEORY
%------------------------------------------------------------------------------ % Continuous functions [T -> Vect2] % % Author: Rick Butler NASA Langley Research Center 2/1/2009 % %------------------------------------------------------------------------------ BEGIN IMPORTING limit_real_vect2[T], analysis@continuous_functions[T], analysis@real_fun_supinf, reals@abs_lems, analysis@epsilon_lemmas f, f1, f2 : VAR [T -> Vect2] g : VAR [T -> Nz_vect2] u : VAR Vect2 a, b, x, x0 : VAR T epsilon, delta : VAR posreal n : VAR nat hh : VAR [T -> real] %-------------------- % Continuity at x0 %-------------------- %% continuous_rv?(f, x0) : bool = convergence(f, x0, f(x0)) continuous_rv?(f, x0) : bool = FORALL epsilon : EXISTS delta : FORALL x: abs(x-x0) < delta IMPLIES norm(f(x) - f(x0)) < epsilon continuous_rv?(f): bool = FORALL x0: continuous_rv?(f, x0) continuous_rv_on?(f:[T->Vect2], E: set[T]) : bool = FORALL (x:(E)): continuous_rv?(f,x) continuity_def : LEMMA continuous_rv?(f, x0) IFF convergence(f, x0, f(x0)) continuity_def2 : LEMMA continuous_rv?(f, x0) IFF convergent?(f, x0) fx(f): MACRO [T-> real] = (LAMBDA (t: T): f(t)`x) fy(f): MACRO [T-> real] = (LAMBDA (t: T): f(t)`y) continuous_iff_comps: LEMMA continuous_rv?(f,a) IFF continuous?(fx(f),a) AND continuous?(fy(f),a) cont_rv_iff_comps: LEMMA continuous_rv?(f) IFF continuous?(fx(f)) AND continuous?(fy(f)) %------------------------------------------ % Operations preserving continuity at x0 %------------------------------------------ sum_continuous_rv : LEMMA continuous_rv?(f1, x0) AND continuous_rv?(f2, x0) IMPLIES continuous_rv?(f1 + f2, x0) diff_continuous_rv : LEMMA continuous_rv?(f1, x0) AND continuous_rv?(f2, x0) IMPLIES continuous_rv?(f1 - f2, x0) const_continuous_rv: LEMMA continuous_rv?(LAMBDA x: u, x0) scal_continuous_rv : LEMMA continuous_rv?(f, x0) IMPLIES continuous_rv?(a * f, x0) prod_continuous_rv : LEMMA continuous?(hh,x0) AND continuous_rv?(f,x0) IMPLIES continuous_rv?(hh * f,x0) neg_continuous_rv : LEMMA continuous_rv?(f, x0) IMPLIES continuous_rv?(- f, x0) %--------------------------------- % Continuity of f in its domain %--------------------------------- sum_cont_rv_fun : LEMMA continuous_rv?(f1) AND continuous_rv?(f2) IMPLIES continuous_rv?(f1 + f2) diff_cont_rv_fun : LEMMA continuous_rv?(f1) AND continuous_rv?(f2) IMPLIES continuous_rv?(f1 - f2) const_cont_rv_fun : LEMMA continuous_rv?(LAMBDA x: u) const_vfun_cont_rv: LEMMA continuous_rv?(const_vfun(u)) scal_cont_rv_fun : LEMMA continuous_rv?(f) IMPLIES continuous_rv?(a * f) prod_cont_rv_fun : LEMMA continuous?(hh) AND continuous_rv?(f) IMPLIES continuous_rv?(hh * f) neg_cont_rv_fun : LEMMA continuous_rv?(f) IMPLIES continuous_rv?(-f) %--- Properties ---% continuous_rv_fun: TYPE+ = { f | continuous_rv?(f) } nz_continuous_rv_fun: TYPE = { g | continuous_rv?(g) } h, h1, h2: VAR continuous_rv_fun h3: VAR nz_continuous_rv_fun sum_fun_continuous_rv : JUDGEMENT +(h1, h2) HAS_TYPE continuous_rv_fun diff_fun_continuous_rv: JUDGEMENT -(h1, h2) HAS_TYPE continuous_rv_fun const_fun_continuous_rv: JUDGEMENT const_vfun(u) HAS_TYPE continuous_rv_fun neg_fun_continuous_rv : JUDGEMENT -(h) HAS_TYPE continuous_rv_fun END cont_real_vect2 ¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28