Quellcode-Bibliothek integral_split.pvs Sprache: PVS

integral_split[T: TYPE+ FROM real]: THEORY
%------------------------------------------------------------------------------
%  Integral Split: integral(a,b,f) + integral(b,c,f) = integral(a,c,f)
%
%  Theory and proofs taken from Introduction to Analysis (Maxwell Rosenlicht)
%
%  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

   AUTO_REWRITE+ not_one_element

   IMPORTING integral_split_scaf,
             step_fun_props,
             reals@sigma_below,
             structures@concat_arrays, reals@sigma_below_sub

   a,b,c,d,x,y,z: VAR T
   f,f1,f2,g: VAR [T -> real]
   eps, delta: VAR posreal
   xv,yv: VAR real

%    step_function_subrng: LEMMA a <= b AND b < c AND c <= d AND
%                                step_function?(a, d, f)
%                                IMPLIES step_function?(b, c, f)

   partition_join: LEMMA a < b AND b < c IMPLIES
                      (FORALL (Pa: partition[T](a,b), xisa:(xis?(a,b,Pa)),
                               Pb: partition[T](b,c), xisb:(xis?(b,c,Pb))):
                   width(a,b,Pa) < delta AND
                   width(b,c,Pb) < delta
                      IMPLIES
                         (EXISTS (PP: partition[T](a,c), xisp:(xis?(a,c,PP))):
                             width(a,c,PP) < delta
                             AND Rie_sum(a, c, PP, xisp, f) =
                                 Rie_sum(a, b, Pa, xisa, f) +
                                      Rie_sum(b, c, Pb, xisb, f)))

   iss_prep: LEMMA a < b AND b < c IMPLIES
                              FORALL (P: partition[T](a,c)):
                               step_function_on?(a, c, f, P)
                  IMPLIES
                     EXISTS (PP: partition[T](a,c)):
                 step_function_on?(a, c, f, PP) AND
                 (EXISTS (ib: below(length(PP))): seq(PP)(ib) = b)

   integrable_split_step: LEMMA a < b AND b < c AND   %% Rosenlight: clearly T
                                  integrable?(a,b,f) AND
                                  integrable?(b,c,f) AND
                                  step_function?(a,c,f)
                             IMPLIES integrable?(a,c,f) AND
                                     integral(a,b,f) + integral(b,c,f)
                                          = integral(a,c,f)

   integrable_split: LEMMA a < b AND b < c AND
                           integrable?(a,b,f) AND
                           integrable?(b,c,f)
                        IMPLIES integrable?(a,c,f)

   integral_split: THEOREM a < b AND b < c AND
                         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)

   integrable?_split: LEMMA a < b AND b < c AND
                            integrable?(a, c, f) IMPLIES
                            integrable?(a, b, f) AND integrable?(b, c, f)

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

%   step_function_on_subrng: LEMMA a <= b AND b < c AND c <= d IMPLIES
%                              FORALL (P: partition[T](a,d)):
%          LET N  = length(P),
%              ib = min_nat.min({ii: below(N) | seq(P)(ii) > b}),
%              ic = max_below[N].max({ii: below(N) | seq(P)(ii) < c}) IN
%                               step_function_on?(a, d, f, P)
%                  IMPLIES step_function_on?(b, c, f, #(b) o P^(ib,ic) o #(c))

END integral_split

quality95%

¤ 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.0.1Bemerkung: (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:

Die farbliche Syntaxdarstellung ist noch experimentell.