products/sources/formale Sprachen/PVS/structures/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: division_ring_def.prf   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.21 Sekunden  (vorverarbeitet)  ¤



Kontakt
Drucken
Kontakt
sprechenden Kalenders

Eigene Datei ansehen




schauen Sie vor die Tür

Fenster


Die Firma ist wie angegeben erreichbar.

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff