Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: rs_integral_prep.pvs Sprache: PVS

Original von: 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

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