Quelle integral.pvs Sprache: 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], integral_cont[T],
             integral_split[T],
             reals@real_fun_ops,
             continuous_functions_more[T]

   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: LEMMA Integrable?(a,a,f)

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

   Integral_a_to_a   : LEMMA Integral(a,a,f) = 0

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

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

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

   continuous_Integrable?: LEMMA
                            (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: LEMMA Integrable?(a,b,f) IMPLIES
                            Integrable?(a,b,D*f) AND
                Integral(a,b,D*f) = D*Integral(a,b,f)

   Integral_sum: 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_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: LEMMA 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: LEMMA 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: LEMMA 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: LEMMA 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: LEMMA 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: LEMMA 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 : LEMMA 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: LEMMA (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

quality75%

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

sprechenden Kalenders