| 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 2 kB |
|
Quelle cont_vect.pvs Sprache: PVS |
|||||||||
|
cont_vect[n,m:posnat] : THEORY
%------------------------------------------------------------------------------ % Continuous functions [ Vector[n] -> Vector[m] ] % % Author: Cesar Munoz % Ricky Butler % NASA Langley Research Center 8/12/2009 %------------------------------------------------------------------------------ BEGIN IMPORTING vectors@vectors IMPORTING limit_vect[n,m] f, f1, f2,g : VAR [Vector[n] -> Vector[m]] u : VAR Vector[m] x, x0 : VAR Vector[n] epsilon, delta : VAR posreal %-------------------- % Continuity at x0 %-------------------- continuous_vv?(f, x0) : bool = FORALL epsilon : EXISTS delta : FORALL x: norm(x-x0) < delta IMPLIES norm(f(x) - f(x0)) < epsilon continuity_def : LEMMA continuous_vv?(f, x0) IFF convergence(f, x0, f(x0)) continuity_def2 : LEMMA continuous_vv?(f, x0) IFF convergent?(f, x0) %------------------------------------------ % Operations preserving continuity at x0 %------------------------------------------ sum_continuous_vv : LEMMA continuous_vv?(f1, x0) AND continuous_vv?(f2, x0) IMPLIES continuous_vv?(f1 + f2, x0) diff_continuous_vv : LEMMA continuous_vv?(f1, x0) AND continuous_vv?(f2, x0) IMPLIES continuous_vv?(f1 - f2, x0) const_continuous_vv: LEMMA continuous_vv?(const_fun(u), x0) %% identity_continuous_vv: LEMMA continuous_vv?((LAMBDA(x):x),x0) neg_continuous_vv : LEMMA continuous_vv?(f, x0) IMPLIES continuous_vv?(- f, x0) %--------------------------------- % Continuity of f in its domain %--------------------------------- continuous_vv?(f): bool = FORALL x0: continuous_vv?(f, x0) %--- Properties ---% continuous_vv_fun: TYPE+ = { f | continuous_vv?(f) } nz_continuous_vv_fun: TYPE = { g | continuous_vv?(g) } h, h1, h2: VAR continuous_vv_fun h3: VAR nz_continuous_vv_fun sum_fun_continuous_vv : JUDGEMENT +(h1, h2) HAS_TYPE continuous_vv_fun diff_fun_continuous_vv: JUDGEMENT -(h1, h2) HAS_TYPE continuous_vv_fun const_fun_continuous_vv: JUDGEMENT const_fun(u) HAS_TYPE continuous_vv_fun neg_fun_continuous_vv : JUDGEMENT -(h) HAS_TYPE continuous_vv_fun % ------------ Alternate forms and names for convenience --------------- sum_cont_fun : LEMMA continuous_vv?(f1) AND continuous_vv?(f2) IMPLIES continuous_vv?(f1 + f2) diff_cont_fun : LEMMA continuous_vv?(f1) AND continuous_vv?(f2) IMPLIES continuous_vv?(f1 - f2) const_cont_fun: LEMMA continuous_vv?(const_fun(u)) neg_cont_fun : LEMMA continuous_vv?(f) IMPLIES continuous_vv?(-f) %% id_cont_fun : LEMMA continuous_vv?((LAMBDA(x):x)) END cont_vect ¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28