Anforderungen  |   Konzepte  |   Entwurf  |   Entwicklung  |   Qualitätssicherung  |   Lebenszyklus  |   Steuerung
 
 
 
 


Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: real_lebesgue_scaf.pvs   Sprache: Unknown

%------------------------------------------------------------------------------
% 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

[ Dauer der Verarbeitung: 0.0 Sekunden  (vorverarbeitet)  ]

                                                                                                                                                                                                                                                                                                                                                                                                     


Neuigkeiten

     Aktuelles
     Motto des Tages

Software

     Produkte
     Quellcodebibliothek

Aktivitäten

     Artikel über Sicherheit
     Anleitung zur Aktivierung von SSL

Muße

     Gedichte
     Musik
     Bilder

Jenseits des Üblichen ....
    

Besucherstatistik

Besucherstatistik