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