Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: integral.pvs Sprache: PVS

Original von: PVS^©

integral[T: TYPE+ FROM real]: THEORY
%------------------------------------------------------------------------------
%
%  Theory and proofs taken from Introduction to Analysis (Maxwell Rosenlight)
%
%  This theory provides the basic properties of the Riemann Integral
%
%  Author:  Rick Butler               NASA Langley
%
%------------------------------------------------------------------------------

BEGIN

   ASSUMING
      IMPORTING deriv_domain_def[T]

      connected_domain : ASSUMPTION connected?[T]

      not_one_element : ASSUMPTION not_one_element?[T]

   ENDASSUMING

   IMPORTING integral_def[T],
             derivatives,
             reals@real_fun_ops

   a,b,c,x,y: VAR T
   D,m,M,yv: VAR real
   f,g: VAR [T -> real]

%    Closed_interval(a:T,b:{x:T | x /= a}): TYPE = {x: T | (a < b IMPLIES
%                                                  (a <= x AND x <= b)) AND
%                                                  (b < a IMPLIES
%                                                  (b <= x AND x <= a))}

%    Closed_interval(a,b:T): TYPE = {x: T | (a <= b IMPLIES
%                                                  (a <= x AND x <= b)) AND
%                                                  (b < a IMPLIES
%                                                  (b <= x AND x <= a))}

   Integrable?_a_to_a: AXIOM Integrable?(a,a,f)
   Integral_a_to_a   : AXIOM Integral(a,a,f) = 0

   Integrable?_inside : AXIOM a <= x AND x <= y AND y <= b AND
       Integrable?(a,b,f) IMPLIES Integrable?(x,y,f)

   Integral_const_fun: AXIOM Integrable?(a, b, const_fun[T](D)) AND
                             Integral(a,b,const_fun(D)) = D*(b-a)

   Integral_const_restrict: AXIOM
               (FORALL (x: Closed_interval(a,b)): f(x) = D) IMPLIES
                                  Integrable?(a,b,f) AND
                                  Integral(a,b,f) = D*(b-a)

   Integral_rev: AXIOM Integrable?(a, b, f) IMPLIES
                       Integrable?(b, a, f) AND
                       Integral(b, a, f) = - Integral(a, b, f)

   continuous_Integrable?: AXIOM
                            (FORALL (x: Closed_interval(a,b)):
                                       continuous?(f,x))
                          IMPLIES Integrable?(a,b,f)

   cont_Integrable?: LEMMA continuous?(f) IMPLIES Integrable?(a,b,f)

   cont_fun_Integrable?: COROLLARY continuous?(f)
                                    IMPLIES Integrable?(a,b,f)

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

   Integral_scal: AXIOM Integrable?(a,b,f) IMPLIES
                            Integrable?(a,b,D*f) AND
                Integral(a,b,D*f) = D*Integral(a,b,f)

   Integral_sum: AXIOM Integrable?(a,b,f) AND Integrable?(a,b,g) IMPLIES
                               Integrable?(a,b,(LAMBDA x: f(x) + g(x)))
                          AND
              Integral(a,b,(LAMBDA x: f(x) + g(x))) =
                 Integral(a,b,f) + Integral(a,b,g)

   Integral_diff: LEMMA Integrable?(a,b,f) AND Integrable?(a,b,g) IMPLIES
                               Integrable?(a,b,(LAMBDA x: f(x) - g(x)))
                          AND
              Integral(a,b,(LAMBDA x: f(x) - g(x))) =
                 Integral(a,b,f) - Integral(a,b,g)

   Integral_split: AXIOM Integrable?(a,b,f) AND Integrable?(b,c,f)
                             IMPLIES Integrable?(a,c,f) AND
                           Integral(a,b,f) + Integral(b,c,f) = Integral(a,c,f)

   Integral_chg_one_pt: AXIOM FORALL (y: Closed_interval(a,b)):
                              Integrable?(a,b,f)
                    IMPLIES Integrable?(a,b,f WITH [(y) := yv]) AND
                       Integral(a,b,f WITH [(y) := yv]) = Integral(a,b,f)

%  ---------------- Boundedness of Integral -----------------------------

   Integral_ge_0: AXIOM a < b AND Integrable?(a,b,f) AND
                    (FORALL (x: Closed_interval(a,b)): f(x) >= 0) IMPLIES
                           Integral(a,b,f) >= 0

   Integral_ge_0_open: AXIOM a <= b AND Integrable?(a,b,f) AND
                    (FORALL (x: Open_interval(a,b)): f(x) >= 0) IMPLIES
                           Integral(a,b,f) >= 0

   Integral_bound: AXIOM a < b AND Integrable?(a,b,f) AND
                           (FORALL (x: Closed_interval(a,b)):
                                    m <= f(x) AND f(x) <= M )
           IMPLIES m*(b-a) <= Integral(a,b,f) AND Integral(a,b,f) <= M*(b-a)

   Integral_bounded: AXIOM Integrable?(a,b,f) AND
               (FORALL (x: Closed_interval(a,b)): abs(f(x)) <= M) IMPLIES
                  abs(Integral(a,b,f)) <= M*abs(b-a)

   Integral_le : AXIOM a < b AND Integrable?(a,b,f) AND Integrable?(a,b,g)
                       AND (FORALL (x: closed_interval(a,b)): f(x) <= g(x))
                    IMPLIES
                       Integral(a,b,f) <= Integral(a,b,g)

%   bounded_on?(a,b,f): bool = (EXISTS (B: real):
%                   (FORALL (x: closed_interval(a,b)): abs(f(x)) <= B))

   % Integrable_bounded: LEMMA Integrable?(a,b,f)
   %                        IMPLIES
   %                             LET l = real_defs.min(a,b),
   %                                 u = real_defs.max(a,b) IN
   %                           bounded_on?(l, u, f)

   Integral_neg: LEMMA Integrable?(a,b,f) IMPLIES
                            Integrable?(a,b,-f) AND
                            Integral(a,b,-f) = -Integral(a,b,f)

   Integral_restr_eq: AXIOM (FORALL (x: Open_interval(a,b)): f(x) = g(x))
                            AND Integrable?(a,b,f)
                          IMPLIES Integrable?(a,b,g) AND
                                   Integral(a,b,g) = Integral(a,b,f)

END integral

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