Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: complete_integral.pvs Sprache: PVS

Original von: 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

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