Quellcode-Bibliothek complete_integral.pvs Sprache: PVS

%------------------------------------------------------------------------------
% Properties of integrals with complete measures
%
%     Author: David Lester, Manchester University, NIA, Université Perpignan
%
% All references are to SK Berberian "Fundamentals of Real Analysis",
% Springer, 1991
%
% Some consequences of complete_integral_ae_eq; compare with the general
% version of 4.4.16 (for non-complete measures) in integral library.
%
%     Version 1.0            1/5/07   Initial Version
%------------------------------------------------------------------------------

complete_integral[T:TYPE,           (IMPORTING subset_algebra_def[T])
                  S:sigma_algebra,  (IMPORTING measure_def[T,S])
                  mu:complete_measure]: THEORY

BEGIN

  IMPORTING complete_measure_theory[T,S,mu],
            integral[T,S,mu],
            integral_convergence[T,S,mu]

  f: VAR integrable
  h: VAR [T->real]
  F: VAR sequence[integrable]
  n: VAR nat
  x: VAR T

  complete_integral_ae_eq:  LEMMA ae_eq?(f,h) =>                       % 4.4.16
                                  (integrable?(h) AND
                                   integral(f) = integral(h))

  complete_measurable_ae_0: LEMMA ae_0?(h) =>
                                  (integrable?(h) AND integral(h) = 0)

  monotone_convergence_complete: THEOREM                               % 4.5.3
      ae_monotonic_converges?(F,h) AND bounded?(integral o F) =>
      (integrable?(h) AND monotonic_converges?((integral o F),integral(h)))

  dominated_convergence_complete: THEOREM                              % 4.5.4
    (FORALL n: ae_le?(abs(F(n)),f)) AND ae_convergence?(F,h) =>
    (integrable?(h) AND convergence?(integral o F, integral(h)))

END complete_integral

quality100%

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