Quelle measure_contraction.pvs Sprache: PVS

%------------------------------------------------------------------------------
% Measure Contraction
%
%     Author: David Lester, Manchester University, NIA, Université Perpignan
%
% If mu is a measure, so is the contraction lambda E: mu(intersection(A,E)).
%
% The integrals using the contracted measure are the same as the indefinite
% integral
%
%     Version 1.0            1/5/07   Initial Version
%------------------------------------------------------------------------------

measure_contraction[T:TYPE,     (IMPORTING subset_algebra_def[T])
                    S:sigma_algebra]: THEORY

BEGIN

  IMPORTING measure_def[T,S],
            measure_space[T,S]
;
  *(f,g:[T -> real]): MACRO [T -> real] = (reals@real_fun_ops[T].*)(f,g)

  mu:  VAR measure_type
  nu:  VAR sigma_finite_measure
  A,E: VAR measurable_set
  f:   VAR measurable_function
  i:   VAR nat

  contraction(mu,A):measure_type = lambda E: mu(intersection(A,E))  % SKB 7.4.2

  fm_contraction(mu:measure_type,A:{E | mu(E)`1}):finite_measure
    = lambda E: mu(intersection(A,E))`2

  sigma_finite_contraction_def: LEMMA
    x_eq(nu(E),x_sum(LAMBDA i: (TRUE,fm_contraction(nu,A_of(nu)(i))(E))))

  IMPORTING isf,
            nn_integral,
            integral,
            indefinite_integral, % Proof only
            integral_convergence % Proof only

  contraction_is_sigma_finite:
                      JUDGEMENT contraction(nu,A) HAS_TYPE sigma_finite_measure

  contraction_isf: LEMMA FORALL (f:simple):
    isf?[T,S,contraction(mu,A)](f) <=> isf?[T,S,mu](phi[T,S](A)*f)

  contraction_isf_integral: LEMMA
    FORALL (f:isf[T,S,contraction(mu,A)]):
      isf_integral[T,S,contraction(mu,A)](f)
        = isf_integral[T,S,mu](phi[T,S](A)*f)

  contraction_nn_integrable: LEMMA FORALL (f:nn_measurable):
    nn_integrable?[T,S,contraction(mu,A)](f) <=>
    nn_integrable?[T,S,mu](phi[T,S](A)*f)

  contraction_nn_integral: LEMMA
    FORALL (f:nn_integrable[T,S,contraction(mu,A)]):
    nn_integral[T,S,contraction(mu,A)](f) = nn_integral[T,S,mu](phi[T,S](A)*f)

  contraction_integrable: LEMMA                                     % SKB 7.4.4
    integrable?[T,S,contraction(mu,A)](f)
      <=> integrable?[T,S,mu](phi[T,S](A)*f)

  contraction_integral:   LEMMA                                     % SKB 7.4.4
    FORALL (f:integrable[T,S,contraction(mu,A)]):
    integral[T,S,contraction(mu,A)](f) = integral[T,S,mu](phi[T,S](A)*f)

END measure_contraction

quality47%

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