Quelle product_finite_measure.pvs Sprache: PVS

%------------------------------------------------------------------------------
% Product of two finite measures
%
%     Author: David Lester, Manchester University, NIA, Université Perpignan
%
% All references are to SK Berberian "Fundamentals of Real Analysis",
% Springer, 1991
%
% How to get a finite measure for sets of [T1,T2], given mu and nu
% (finite measures for T1 and T2 respectively).
%
% Suppose that mu=nu and T1=T2=real. Then fm_times(mu,nu) has to be able to
% calculate the measure (i.e. area) of a circle; not just for rectangles.
%
%     Version 1.0            1/5/07   Initial Version
%------------------------------------------------------------------------------

product_finite_measure[(IMPORTING subset_algebra_def)
                       T1,T2:TYPE,
                       S1:sigma_algebra[T1], S2:sigma_algebra[T2]]: THEORY

BEGIN

  IMPORTING product_sigma_def[T1,T2],
            product_sigma[T1,T2,S1,S2],
            measure_def[T1,S1],
            measure_def[T2,S2],
            measure_def[[T1,T2],sigma_times(S1,S2)],
            integral,
            finite_measure,
            monotone_classes,        % Proof only
            integral_convergence     % Proof only

  M: VAR (sigma_times(S1,S2))
  x: VAR T1
  y: VAR T2
  X: VAR (S1)
  Y: VAR (S2)
  E: VAR sequence[(sigma_times(S1,S2))]
  mu: VAR finite_measure[T1,S1]
  nu: VAR finite_measure[T2,S2]

  x_section_bounded: LEMMA 0 <= (nu o x_section(M))(x) AND        % SKB 7.2.9
                           (nu o x_section(M))(x) <= nu(fullset[T2])
  y_section_bounded: LEMMA 0 <= (mu o y_section(M))(y) AND        % SKB 7.2.9
                           (mu o y_section(M))(y) <= mu(fullset[T1])

  x_section_measurable: LEMMA measurable_function?[T1,S1](nu o x_section(M))
  y_section_measurable: LEMMA measurable_function?[T2,S2](mu o y_section(M))
                                                                   % SKB 7.2.10
  x_section_integrable: LEMMA
    integrable?[T1,S1,to_measure(mu)](nu o x_section(M))
  y_section_integrable: LEMMA
    integrable?[T2,S2,to_measure(nu)](mu o y_section(M))

  rectangle_measure1: LEMMA M = cross_product(X,Y) =>
        integral[T1,S1,to_measure(mu)](nu o x_section(M)) = mu(X)*nu(Y)
  rectangle_measure2: LEMMA M = cross_product(X,Y) =>
        integral[T2,S2,to_measure(nu)](mu o y_section(M)) = mu(X)*nu(Y)

  fm_times(mu,nu):finite_measure[[T1,T2],sigma_times(S1,S2)]
    = lambda M: integral[T1,S1,to_measure(mu)](nu o x_section(M))

  fm_times_alt: LEMMA finite_measure?[[T1,T2],sigma_times(S1,S2)]
       (lambda M: integral[T2,S2,to_measure(nu)](mu o y_section(M)))

  finite_product_alt: THEOREM                                      % SKB 7.2.11
    fm_times(mu,nu)(M) = integral[T2,S2,to_measure(nu)](mu o y_section(M))

END product_finite_measure

quality90%

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