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_ax/ (Beweissystem der NASA Version 6.0.9^©) Datei vom 28.9.2014 mit Größe 5 kB

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],
             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

quality93%

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