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