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


Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: lebesgue_def.pvs   Sprache: Unknown

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