Quelle nn_integral.pvs Sprache: PVS

%------------------------------------------------------------------------------
% Non-negative Integrals
%
%     Author: David Lester, Manchester University, NIA, Université Perpignan
%
% All references are to SK Berberian "Fundamentals of Real Analysis",
% Springer, 1991
%
% Definition and basic properties of integrals of functions f:[T->nnreal]
%
%     Version 1.0            1/5/07   Initial Version
%------------------------------------------------------------------------------

nn_integral[T:TYPE,          (IMPORTING subset_algebra_def[T])
            S:sigma_algebra, (IMPORTING measure_def[T,S])
            m:measure_type]: THEORY

BEGIN

  IMPORTING measure_space[T,S],
            measure_props[T,S,m],
            measure_theory[T,S,m],
            isf[T,S,m]

  convergent?: MACRO pred[sequence[real]] = topological_convergence.convergent?
  limit:       MACRO [convergent->real]   = topological_convergence.limit

  n: VAR nat
  pn: VAR posnat
  x: VAR T
  c: VAR nnreal
  E: VAR measurable_set
  F: VAR (mu_fin?)
  g: VAR measurable_function
  h: VAR nn_bounded_measurable

  nn_isf?(i:isf):bool = FORALL x: i(x) >= 0

  nn_isf: TYPE+ = (nn_isf?) CONTAINING (lambda x: 0)

  i: VAR nn_isf
  w: VAR sequence[nn_isf]

  increasing_nn_isf?(u:sequence[nn_isf]):bool = pointwise_increasing?(u)

  increasing_nn_isf: TYPE+ = (increasing_nn_isf?) CONTAINING
                                               (lambda n: lambda x: 0)

  u,u1,u2: VAR increasing_nn_isf

  nn_integrable?(g:[T->nnreal]):bool                                    % 4.4.1
    = EXISTS u: pointwise_convergence?(u,g) AND convergent?(isf_integral o u)

  nn_integrable_zero:      LEMMA nn_integrable?(lambda x: 0)

  nn_integrable: TYPE+ = (nn_integrable?) CONTAINING (lambda x: 0)

  f,f1,f2: VAR nn_integrable

  nn_integrable_is_nonneg: LEMMA f(x) >= 0

  nn_integrable_is_measurable:
                 JUDGEMENT nn_integrable SUBTYPE_OF measurable_function % 4.4.1

  nn_convergence: LEMMA pointwise_convergence?(u1,f) AND                % 4.4.2
                        pointwise_convergence?(u2,f) AND
                        convergent?(isf_integral o u1) =>
                        (convergent?(isf_integral o u2) AND
                        limit(isf_integral o u1) = limit(isf_integral o u2))

  nn_integral(f):nnreal                                                 % 4.4.3
    = limit(isf_integral o choose({u | pointwise_convergence?(u,f)}))

  nn_integrable_add:       JUDGEMENT +(f1,f2) HAS_TYPE   nn_integrable
  nn_integrable_scal:      JUDGEMENT *(c,f)   HAS_TYPE   nn_integrable
  nn_isf_is_nn_integrable: JUDGEMENT nn_isf   SUBTYPE_OF nn_integrable  % 4.4.4

  nn_integral_isf:  LEMMA nn_integral(i) = isf_integral(i)              % 4.4.4

  nn_integrable_le: LEMMA (FORALL x: 0 <= g(x) AND g(x) <= f(x)) =>     % 4.4.5
                          (nn_integrable?(g) AND
                           nn_integral(g) <= nn_integral(f))

  nn_integral_zero:LEMMA nn_integral(lambda x: 0) = 0
  nn_integral_phi: LEMMA nn_integral(phi(F)) = mu(F)
  nn_integral_add: LEMMA nn_integral(f1+f2) = nn_integral(f1) + nn_integral(f2)
  nn_integral_scal:LEMMA nn_integral(c*f)   = c * nn_integral(f)

  nn_integrable_prod:    JUDGEMENT *(f,h)       HAS_TYPE nn_integrable

  nn_indefinite_integrable: LEMMA nn_integrable?(phi(E)*f)              % 4.4.6

  nn_0_le:    LEMMA 0 <= nn_integral(f)

  nn_integral_def: LEMMA
     EXISTS u: pointwise_convergence?(u,f) AND
               convergence?(isf_integral o u, nn_integral(f))

END nn_integral

quality94%

¤ 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:

Die farbliche Syntaxdarstellung ist noch experimentell.