Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: lebesgue_def.pvs Sprache: PVS

Original von: PVS^©

%------------------------------------------------------------------------------
% Definitions for Lebesgue inetgration
%
%     Author: David Lester, Manchester University
%
% All references are to SK Berberian "Fundamentals of Real Analysis",
% Springer, 1991
%
% cal_M is the sigma-algebra of Lebesgue-measurable sets of real.
% lambda_ is the associated Lebesgue-measure
%
%     Version 1.0            26/2/10   Initial Version
%------------------------------------------------------------------------------

lebesgue_def: THEORY

BEGIN

  IMPORTING real_lebesgue_scaf,
            measure_integration@real_borel

  i,A,B: VAR interval
  X:     VAR sequence[interval]
  n:     VAR nat

  cal_M:sigma_algebra = lebesgue_measurable          % Lebesgue Measurable sets

  a,x: VAR real
  r:   VAR posreal
  nnr: VAR nnreal

  open_semi_infinite_is_cal_M: LEMMA member({x | x < a},cal_M)          % 2.2.1
  borel_is_cal_M:              LEMMA subset?(borel?,cal_M)
  open_interval_is_cal_M:      LEMMA subset?(open_interval?,cal_M)
  closed_interval_is_cal_M:    LEMMA subset?(closed_interval?,cal_M)
  singleton_is_cal_M:          LEMMA member(singleton[real](x),cal_M)
  ball_is_cal_M:               LEMMA member(ball(x,r),cal_M)
  closed_ball_is_cal_M:        LEMMA member(closed_ball(x,nnr),cal_M)   % 2.4.6

  IMPORTING measure_integration@measure_def[real,cal_M]

  lambda_: complete_sigma_finite[real,cal_M] = lebesgue_measure
                                                             % Lebesgue Measure

  lambda_singleton:   LEMMA lambda_(singleton[real](x)) = (TRUE, 0)
  lambda_ball:        LEMMA lambda_(ball(x,r))          = (TRUE, 2*r)
  lambda_closed_ball: LEMMA lambda_(closed_ball(x,nnr)) = (TRUE, 2*nnr)

  IMPORTING measure_integration@measure_space_def[real,cal_M]

  IMPORTING
    measure_integration@complete_measure_theory[real,cal_M,lambda_],
    measure_integration@complete_integral[real,cal_M,lambda_]

  integrable_phi_open:   LEMMA FORALL (a:real,b:{x | a < x}):
                               integrable?(phi(open(a,b)))
  integrable_phi_closed: LEMMA FORALL (a:real,b:{x | a <= x}):
                               integrable?(phi(closed(a,b)))
  integral_phi_open:   LEMMA FORALL (a:real,b:{x | a < x}):
                             integral(phi(open(a,b)))   = b-a
  integral_phi_closed: LEMMA FORALL (a:real,b:{x | a <= x}):
                             integral(phi(closed(a,b))) = b-a

  IMPORTING
    topology@identity_continuity[real,metric_induced_topology]

  I_is_measurable:          JUDGEMENT I[real]    HAS_TYPE   measurable_function
  continuous_is_measurable: JUDGEMENT continuous SUBTYPE_OF measurable_function

  X: VAR finite_set[real]
  C: VAR countable_set[real]

  singleton_is_measurable:
                        JUDGEMENT singleton[real](x)    HAS_TYPE measurable_set
  open_is_measurable:   JUDGEMENT
                          open(a:real,b:{x | a < x})    HAS_TYPE measurable_set
  closed_is_measurable: JUDGEMENT
                          closed(a:real,b:{x | a <= x}) HAS_TYPE measurable_set
  finite_is_measurable: JUDGEMENT finite_set[real]    SUBTYPE_OF measurable_set
  countable_is_measurable:
                        JUDGEMENT countable_set[real] SUBTYPE_OF measurable_set

  singleton_is_null: JUDGEMENT singleton[real](x)    HAS_TYPE null_set
  finite_is_null:    JUDGEMENT finite_set[real]    SUBTYPE_OF null_set
  countable_is_null: JUDGEMENT countable_set[real] SUBTYPE_OF null_set

  integrable_singleton:  LEMMA integrable?(phi(singleton[real](x)))
  integrable_finite:     LEMMA integrable?(phi(X))
  integrable_countable:  LEMMA integrable?(phi(C))

  integral_singleton:  LEMMA integral(phi(singleton[real](x))) = 0
  integral_finite:     LEMMA integral(phi(X)) = 0
  integral_countable:  LEMMA integral(phi(C)) = 0

% The following lemmas are needed to prove the Riemann-Lebesgue lemmas.
% Essentially, we show that any bounded measurable set can be approximated
% by a convergent sequence of bounded open intervals.

  nonempty_bounded_open_interval_prop: LEMMA
     FORALL (b:bounded_open_interval):
            nonempty?[real](b) => EXISTS x,r: b = ball(x,r)

  bounded_open_interval_is_measurable:
     JUDGEMENT bounded_open_interval SUBTYPE_OF measurable_set

  E: VAR (mu_fin?)
  I: VAR sequence[bounded_open_interval]

  lebesgue_measurable_intervals: LEMMA
    EXISTS I: subset?[real](E,IUnion(I)) AND
              mu_fin?(IUnion(I))         AND
              convergence?(lambda n: mu(IUnion(n,I)),mu(IUnion(I))) AND
              mu(IUnion(I)) - mu(E) < r

END lebesgue_def

¤ Dauer der Verarbeitung: 0.18 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.