Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/Sources/formale Sprachen/PVS/analysis/ (Beweissystem der NASA Version 6.0.9^©) Datei vom 28.9.2014 mit Größe 6 kB

Quelle rs_integral_prep.pvs Sprache: PVS

rs_integral_prep[T:TYPE+ from real]: THEORY
%------------------------------------------------------------------------------
%  Basic Properties of the Riemann-Stieltjes Integral
%------------------------------------------------------------------------------

BEGIN

   ASSUMING
      IMPORTING deriv_domain_def[T]

      connected_domain : ASSUMPTION connected?[T]

      not_one_element : ASSUMPTION not_one_element?[T]

   ENDASSUMING

   IMPORTING rs_integral_def[T], reals@real_fun_ops[T]

   a,b,x,y,z: VAR T
   c,S: VAR real
   D,m,M,v1,v2,cc,RS1,RS2,K: VAR real
   delta : VAR posreal

   f,g,h,G: VAR [T -> real]

  %--------------------------------%

   integral_const_fun: LEMMA a < b IMPLIES integrable?(a,b,g,const_fun(D))
                               AND integral(a,b,g, const_fun(D)) = D*(g(b)-g(a))

   integral_const_restrict: LEMMA a < b AND
               (FORALL (x: closed_interval(a,b)): f(x) = D) IMPLIES
                                  integral?(a,b,g,f,D*(g(b)-g(a)))


   IMPORTING continuous_functions, convergence_sequences

%  ------------ Linearity Properties of Integral

   integral_scal: LEMMA a < b AND integrable?(a,b,g,f) IMPLIES
                            integrable?(a,b,g,D*f) AND
                               integral(a,b,g,D*f) = D*integral(a,b,g,f)

   integral_scal_g: LEMMA a < b AND integrable?(a,b,g,f) IMPLIES
                            integrable?(a,b,D*g,f) AND
                               integral(a,b,D*g,f) = D*integral(a,b,g,f)

   integral_sum: LEMMA a < b AND integrable?(a,b,g,f) AND integrable?(a,b,g,h)
                      IMPLIES
                         integrable?(a,b,g,(LAMBDA x: f(x) + h(x)))  AND
                             integral(a,b,g,(LAMBDA x: f(x) + h(x))) =
                                  integral(a,b,g,f) + integral(a,b,g,h)

   integral_sum_g: LEMMA a < b AND integrable?(a,b,g,f) AND integrable?(a,b,h,f)
                      IMPLIES
                         integrable?(a,b,(LAMBDA x: g(x) + h(x)),f)  AND
                             integral(a,b,(LAMBDA x: g(x) + h(x)),f) =
                                  integral(a,b,g,f) + integral(a,b,h,f)

   integral?_sum: LEMMA a < b AND integral?(a,b,g,f,v1) AND
                                    integral?(a,b,g,h,v2)
                      IMPLIES
                         integral?(a,b,g,(LAMBDA x: f(x) + h(x)),v1+v2)

   integral?_sum_g: LEMMA a < b AND integral?(a,b,g,f,v1) AND
                                    integral?(a,b,h,f,v2)
                      IMPLIES
                         integral?(a,b,(LAMBDA x:g(x)+h(x)),f,v1+v2)

   integral_diff: LEMMA a < b AND integrable?(a,b,g,f) AND integrable?(a,b,g,h)
                      IMPLIES
                         integrable?(a,b,g,(LAMBDA x: f(x) - h(x)))  AND
                             integral(a,b,g,(LAMBDA x: f(x) - h(x))) =
                                  integral(a,b,g,f) - integral(a,b,g,h)

   integral_diff_g: LEMMA a < b AND integrable?(a,b,g,f) AND integrable?(a,b,h,f)
                      IMPLIES
                         integrable?(a,b,(LAMBDA x:g(x)-h(x)),f)  AND
                             integral(a,b,(LAMBDA x:g(x)-h(x)),f) =
                                  integral(a,b,g,f) - integral(a,b,h,f)

   integral_ge_0: LEMMA a < b AND increasing?(g) AND
        integrable?(a,b,g,f) AND
                     (FORALL (x: closed_interval(a,b)): f(x) >= 0) IMPLIES
                           integral(a,b,g,f) >= 0

   integral_restr_eq: LEMMA a < b AND
                                (FORALL x: a <= x AND x <= b IMPLIES
                                          f(x) = h(x)) AND
                               integrable?(a,b,g,f)
                          IMPLIES integrable?(a,b,g,h) AND
                                   integral(a,b,g,h) = integral(a,b,g,f)

   integral_bound_above: LEMMA a < b AND increasing?(g) AND
            integrable?(a,b,g,f) AND
                           (FORALL (x: closed_interval(a,b)):f(x)<=M)
           IMPLIES integral(a,b,g,f) <= M*(g(b)-g(a))

   integral_bound_below: LEMMA a < b AND increasing?(g) AND
            integrable?(a,b,g,f) AND
                           (FORALL (x: closed_interval(a,b)): m<=f(x))
           IMPLIES m*(g(b)-g(a)) <= integral(a,b,g,f)

   integral_le : LEMMA a < b AND increasing?(g) AND
                   integrable?(a,b,g,f) AND integrable?(a,b,g,h)
                       AND (FORALL (x: closed_interval(a,b)): f(x) <= h(x))
                    IMPLIES
                       integral(a,b,g,f) <= integral(a,b,g,h)

   eps: VAR posreal

   Lemma_1: LEMMA a < b IMPLIES
               (integrable?(a,b,g,f) IMPLIES
                  (FORALL eps: EXISTS delta:
                      (FORALL (P1,P2: partition(a,b),
                               xis1:xis?(a,b,P1),
                               xis2:xis?(a,b,P2)):
                        LET S1 = Rie_sum(a,b,g,P1,xis1,f),
                            S2 = Rie_sum(a,b,g,P2,xis2,f) IN
                        (width(a,b,P1) < delta AND
                         width(a,b,P2) < delta)
                           IMPLIES
                              abs(S1 - S2) < eps )))

   integrable_lem: THEOREM  a < b IMPLIES
                     (integrable?(a,b,g,f) IFF
                        (FORALL (epsi: posreal): (EXISTS (delta: posreal):
                             (FORALL (P1,P2: partition(a,b)):
                               width(a,b,P1) < delta AND
                               width(a,b,P2) < delta IMPLIES
                               (FORALL (RS1: (Riemann_sum?(a,b,P1,g,f)),
                                        RS2: (Riemann_sum?(a,b,P2,g,f))):
                                   abs(RS1 - RS2) < epsi )))))

   %-------------------------------------------------------------------------%

   integrable_lem2_alt: LEMMA a<b IMPLIES LET CI = closed_intv(a,b) IN
     (monotonic?[(CI)](g) IMPLIES   % Added 8/2010 for RS integral
           (integrable?(a,b,g,f) IFF
                        (FORALL (epsi: posreal): (EXISTS (delta: posreal):
                             (FORALL (P: partition(a,b)):
                               width(a,b,P) < delta IMPLIES
                               (FORALL (RS1: (Riemann_sum?(a,b,P,g,f)),
                                        RS2: (Riemann_sum?(a,b,P,g,f))):
                                   abs(RS1 - RS2) < epsi ))))))

   integrable_lem2: LEMMA a<b IMPLIES LET CI = closed_intv(a,b) IN
     (monotonic?[(CI)](g) IMPLIES   % Added 8/2010 for RS integral
           (integrable?(a,b,g,f) IFF
                        (FORALL (epsi: posreal): (EXISTS (delta: posreal):
                             (FORALL (P: partition(a,b)):
                               width(a,b,P) < delta IMPLIES
                               (FORALL (RS1: (Riemann_sum?(a,b,P,g,f)),
                                        RS2: (Riemann_sum?(a,b,P,g,f))):
                                   abs(RS1 - RS2) < epsi ))))))

END rs_integral_prep

quality97%

¤ Dauer der Verarbeitung: 0.14 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.