Quelle real_lebesgue_scaf.pvs Sprache: PVS

%------------------------------------------------------------------------------
% Scaffold Definitions for Lebesgue inetgration
%
%     Author: David Lester, Manchester University
%
% All references are to SK Berberian "Fundamentals of Real Analysis",
% Springer, 1991
%
%     Version 1.0            26/2/10   Initial Version
%------------------------------------------------------------------------------

real_lebesgue_scaf: THEORY

BEGIN

  IMPORTING metric_space@real_topology,
            reals@bounded_reals,
            real_intervals,
            real_intervals_aux,
            sigma_set@absconv_series_aux,
            extended_nnreal@extended_nnreal,
            measure_integration@outer_measure_def[real],
            reals@sqrt % Proof only

  limit: MACRO [convergent->real] = convergence_sequences.limit

  A: VAR set[real]

  b: VAR bounded_interval
  u: VAR unbounded_interval
  i: VAR open_interval
  I: VAR sequence[bounded_open_interval]
  z: VAR extended_nnreal
  n: VAR nat
  r: VAR posreal
  nnr: VAR nnreal
  a,x: VAR real

  x_length(i:interval):extended_nnreal
    = IF bounded_interval?(i) THEN (TRUE,length(i)) ELSE (FALSE,0) ENDIF

  lebesgue_outer_measure: outer_measure                                 % 2.1.6
    = lambda A: x_inf({z | EXISTS I: x_le(x_sum(x_length o I),z) AND
                                     subset?[real](A,IUnion(I))})

  IMPORTING
    measure_integration@outer_measure_props[real,lebesgue_outer_measure]

  lebesgue_outer_measure_singleton: LEMMA                               % 2.1.6
     x_eq(lebesgue_outer_measure(singleton[real](x)),(TRUE,0))

  lebesgue_outer_measure_closed_open: LEMMA nonempty?[real](b) =>       % 2.1.6
     x_eq(lebesgue_outer_measure({x | inf(b) <= x AND x <= sup(b)}),
          lebesgue_outer_measure({x | inf(b) <  x AND x <  sup(b)}))

  lebesgue_outer_measure_closed_open_rew: LEMMA FORALL (b:{x|a<=x}):
     x_eq(lebesgue_outer_measure({x | a <= x AND x <= b}),
          lebesgue_outer_measure({x | a <  x AND x <  b}))

  lebesgue_outer_measure_closed: LEMMA nonempty?[real](b) =>            % 2.1.6
     x_eq(lebesgue_outer_measure(b),
          lebesgue_outer_measure({x | inf(b) <= x AND x <= sup(b)}))

  lebesgue_outer_measure_open: LEMMA nonempty?[real](b) =>              % 2.1.6
     x_eq(lebesgue_outer_measure(b),
          lebesgue_outer_measure({x | inf(b) < x AND x < sup(b)}))

  lebesgue_outer_measure_le_length: LEMMA                               % 2.1.6
     x_le(lebesgue_outer_measure(b),x_length(b))

  IMPORTING metric_space@heine_borel, % Proof Only
            sigma_set@sigma_countable  % Proof Only

  lebesgue_outer_measure_eq_length: LEMMA                               % 2.1.6
     x_eq(lebesgue_outer_measure(b),x_length(b))

  lebesgue_outer_measure_bounded_interval: LEMMA
                   lebesgue_outer_measure(b) = (TRUE,length(b))         % 2.1.6

  lebesgue_outer_measure_unbounded_interval: LEMMA
                   NOT lebesgue_outer_measure(u)`1                      % 2.1.8

  IMPORTING measure_integration@real_borel

  outer_measurable_open_semi_infinite: LEMMA outer_measurable?({x | x < a})
                                                                        % 2.2.1

  lebesgue_measurable:sigma_algebra[real] = fullset[(outer_measurable?)]

  open_interval_is_lebesgue_measurable:
                       JUDGEMENT open_interval   SUBTYPE_OF outer_measurable

  borel_is_lebesgue_measurable: JUDGEMENT borel  SUBTYPE_OF outer_measurable
                                                                        % 2.4.6
  closed_interval_is_lebesgue_measurable:
                       JUDGEMENT closed_interval SUBTYPE_OF outer_measurable

  IMPORTING measure_integration@measure_def[real,lebesgue_measurable]

  lebesgue_measure: complete_sigma_finite[real,lebesgue_measurable]
    = induced_measure

END real_lebesgue_scaf

quality93%

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