Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: vect2_cont_dot.pvs Sprache: PVS

Original von: PVS^©

vect2_cont_dot[T: TYPE from real] : THEORY
%----------------------------------------------------------------------------
%
%   AUTHOR: Rick Butler         NASA langley Research Center
%
%   The proofs in this theory are tricky.
%
%   f,g: [real -> vect2] are continuous
%
%     || f(x) * g(x) - f(x0) * g(x0) || <= ||f(x) || || f(x) * g(x) - g(x0) ||
%                                          + || g(x0) || || f(x)  - f(x0) ||
%
%     need || f(x)  - f(x0) || < eps/(2*||g(x0)||)
%
%     need || g(x)  - g(x0) || < eps/(2*r) where || f(x) || < r near x0
%
%     EXISTS delta1: | x - x0 | < delta1 IMPLIES
%                                   || f(x)|| < ||f(x0)|| + 1 = r
%
%     EXISTS delta2: | x - x0 | < delta2 IMPLIES
%                       || f(x)  - f(x0) || < eps/(2*||g(x0)||)
%
%     EXISTS delta3: | x - x0 | < delta3 IMPLIES
%               || g(x)  - g(x0) || < eps/(2*r)
%
%     let delta = min(delta1,delta2,delta3)
%
%     || f(x) * g(x) - f(x0) * g(x0) || <= ||f(x) || || f(x) * g(x) - g(x0) ||
%                                          + || g(x0) || || f(x)  - f(x0) ||
%                                  < r * eps    + eps || g(x0)||
%                                        ---      ---
%                                         2r     (2||g(x0)||)
%                                  = eps
%
%----------------------------------------------------------------------------
BEGIN

  IMPORTING cont_vect2_real,
            cont_vect2_vect2,
            analysis@continuous_lambda[T],
            cont_real_vect2[T]

  frr : VAR [T -> real]
  continuous_rr?(frr): MACRO bool = continuous?(frr)

  v   : VAR Vect2
  x,y : VAR T

   vv,vv1,vv2 : VAR { f:[Vect2->Vect2] | continuous_vv?(f) }
   vr,vr1,vr2 : VAR { f:[Vect2->real] | continuous_vr?(f) }
   rr         : VAR continuous_fun
   rv,rv1,rv2 : VAR { f:[T->Vect2] | continuous_rv?(f) }

  dot_cont_vr : LEMMA
    continuous_vr?(LAMBDA(v):vv1(v)*vv2(v))

  dot_cont_rr : LEMMA
    continuous?[T](LAMBDA(x):rv1(x)*rv2(x))

  scal_cont_rv : LEMMA
    continuous_rv?(LAMBDA(x):rr(x)*rv(x))

  scal_cont_vv : LEMMA
    continuous_vv?(LAMBDA(v):vr(v)*vv(v))

  scal_scal_cont_rv : LEMMA
    continuous_rv?(LAMBDA(x):y*rv(x))

END vect2_cont_dot

¤ Dauer der Verarbeitung: 0.0 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.