Quelle vect2_cont_dot.pvs Sprache: 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

quality59%

¤ Dauer der Verarbeitung: 0.9 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.