|
%-------------------------------------------------------------------------
% Measure Space
%
% Author: David Lester, Manchester University
%
% Version 1.0 04/05/09 Initial (DRL)
%
% Most of Chapter 4, section 1 of Berberian
%
%-------------------------------------------------------------------------
measure_space[T:TYPE, (IMPORTING subset_algebra_def[T])
S:sigma_algebra]: THEORY
BEGIN
IMPORTING
measure_space_def[T,S],
reals@real_fun_ops_aux[T],
power@real_fun_power[T],
real_borel,
borel_functions[real,metric_induced_topology,
real,metric_induced_topology],
topology@constant_continuity[real,metric_induced_topology,
real,metric_induced_topology],
metric_space@metric_continuity[real,(lambda (x,y:real): abs(x-y)),
real,(lambda (x,y:real): abs(x-y))],
metric_space@real_continuity[real,(lambda (x,y:real): abs(x-y))],
pointwise_convergence[T],
reals@bounded_reals[real],
finite_sets@finite_cross,
finite_sets@finite_sets_minmax_props[real,<=] % proof only
f: VAR [T->real]
g,g1,g2: VAR measurable_function[T,S]
phi: VAR borel_function
i,j,n,m: VAR nat
s: VAR sequence[[T->real]]
u: VAR sequence[measurable_function[T,S]]
x: VAR T
c,c1,c2,y: VAR real
X: VAR set[T]
Y: VAR set[real]
a: VAR posreal
borel_comp_measurable_is_measurable:
JUDGEMENT o(phi,g) HAS_TYPE measurable_function[T,S] % SKB 4.1.12
const_measurable: LEMMA measurable_function?(lambda x: c)
nn_measurable?(f):bool = measurable_function?(f) AND FORALL x: 0 <= f(x)
nn_measurable: TYPE+ = (nn_measurable?) CONTAINING (lambda x: 0)
nn_measurable_is_measurable:
JUDGEMENT nn_measurable SUBTYPE_OF measurable_function
abs_measurable: JUDGEMENT abs(g) HAS_TYPE measurable_function[T,S]
expt_nat_measurable: JUDGEMENT expt(g,n) HAS_TYPE measurable_function[T,S]
sq_measurable: JUDGEMENT sq(g) HAS_TYPE measurable_function[T,S]
min_measurable: JUDGEMENT min(g1,g2) HAS_TYPE measurable_function[T,S]
max_measurable: JUDGEMENT max(g1,g2) HAS_TYPE measurable_function[T,S]
minimum_measurable: JUDGEMENT minimum(u,n) HAS_TYPE measurable_function[T,S]
maximum_measurable: JUDGEMENT maximum(u,n) HAS_TYPE measurable_function[T,S]
plus_measurable: JUDGEMENT plus(g) HAS_TYPE measurable_function[T,S]
minus_measurable: JUDGEMENT minus(g) HAS_TYPE measurable_function[T,S]
prod_measurable: JUDGEMENT *(g1,g2) HAS_TYPE measurable_function[T,S]
expt_measurable: JUDGEMENT ^(g:nn_measurable,a)
HAS_TYPE measurable_function[T,S]
% SKB 4.1.13
measurable_plus_minus: LEMMA
measurable_function?[T,S](f) <=>
(measurable_function?[T,S](plus(f)) AND
measurable_function?[T,S](minus(f))) % SKB 4.1.15
measurable_bounded_above?(u):bool = pointwise_bounded_above?(u)
measurable_bounded_below?(u):bool = pointwise_bounded_below?(u)
measurable_bounded?(u):bool
= measurable_bounded_above?(u) AND measurable_bounded_below?(u)
measurable_bounded_above: TYPE+ = (measurable_bounded_above?)
CONTAINING (lambda n: lambda x: 0)
measurable_bounded_below: TYPE+ = (measurable_bounded_below?)
CONTAINING (lambda n: lambda x: 0)
measurable_bounded: TYPE+ = (measurable_bounded?)
CONTAINING (lambda n: lambda x: 0)
measurable_bounded_above_is_bounded_above:
JUDGEMENT measurable_bounded_above SUBTYPE_OF pointwise_bounded_above
measurable_bounded_below_is_bounded_below:
JUDGEMENT measurable_bounded_below SUBTYPE_OF pointwise_bounded_below
measurable_bounded_is_measurable_bounded_above:
JUDGEMENT measurable_bounded SUBTYPE_OF measurable_bounded_above
measurable_bounded_is_measurable_bounded_below:
JUDGEMENT measurable_bounded SUBTYPE_OF measurable_bounded_below
measurable_bounded_is_bounded:
JUDGEMENT measurable_bounded SUBTYPE_OF pointwise_bounded
inf_measurable: LEMMA FORALL (u:measurable_bounded_below):
measurable_function?[T,S](inf(u)(n))
sup_measurable: LEMMA FORALL (u:measurable_bounded_above):
measurable_function?[T,S](sup(u)(n)) % SKB 4.1.19
pointwise_measurable: LEMMA pointwise_convergence?(u,f) => % SKB 4.1.20
measurable_function?[T,S](f)
simple?(f):bool = measurable_function?[T,S](f) AND
is_finite(image(f,fullset[T])) % SKB 4.1.21
simple: TYPE+ = (simple?) CONTAINING (lambda x: 0)
simple_is_measurable: JUDGEMENT simple SUBTYPE_OF measurable_function
simple_const: LEMMA simple?(lambda x: c)
nn_simple?(f):bool = (FORALL x: 0 <= f(x)) AND simple?(f)
nn_simple: TYPE+ = (nn_simple?) CONTAINING (lambda x: 0)
nn_simple_is_simple: JUDGEMENT nn_simple SUBTYPE_OF simple
h,h1,h2: VAR simple
v: VAR sequence[simple]
simple_sq: JUDGEMENT sq(h) HAS_TYPE simple
simple_add: JUDGEMENT +(h1,h2) HAS_TYPE simple
simple_scal: JUDGEMENT *(c,h) HAS_TYPE simple
simple_neg: JUDGEMENT -(h) HAS_TYPE simple
simple_diff: JUDGEMENT -(h1,h2) HAS_TYPE simple
simple_abs: JUDGEMENT abs(h) HAS_TYPE simple
simple_min: JUDGEMENT min(h1,h2) HAS_TYPE simple
simple_max: JUDGEMENT max(h1,h2) HAS_TYPE simple
simple_maximum: JUDGEMENT maximum(v,n) HAS_TYPE simple
simple_minimum: JUDGEMENT minimum(v,n) HAS_TYPE simple
simple_plus: JUDGEMENT plus(h) HAS_TYPE simple
simple_minus: JUDGEMENT minus(h) HAS_TYPE simple
simple_times: JUDGEMENT *(h1,h2) HAS_TYPE simple
simple_expt_nat: JUDGEMENT expt(h,n) HAS_TYPE simple
simple_expt: JUDGEMENT ^(h:nn_simple,a) HAS_TYPE simple % SKB 4.1.22
phi(X)(x):nat = IF member(x,X) THEN 1 ELSE 0 ENDIF
phi_is_simple: JUDGEMENT phi(X:(S)) HAS_TYPE simple
IMPORTING hausdorff_borel[real,metric_induced_topology],
partitions[T]
P: VAR finite_partition[T]
simple_def1: LEMMA simple?(f) <=> % SKB 4.1.23
(is_finite(image(f,fullset[T])) AND
(FORALL (y:(image(f,fullset[T]))): measurable_set?({x | y = f(x)})))
constant_over?(f)(X):bool = EXISTS y: FORALL (x:(X)): y = f(x)
simple_def2: LEMMA simple?(f) <=>
EXISTS P: every(S,P) AND every(constant_over?(f),P)
simple_def3: LEMMA simple?(f) <=> EXISTS c1,c2,h1,h2: c1*h1+c2*h2 = f
IMPORTING sup_norm[T]
bounded_measurable?(f):bool = bounded?(f) AND measurable_function?(f)
bounded_measurable: TYPE+ = (bounded_measurable?) CONTAINING (lambda x: 0)
bounded_measurable_is_bounded:
JUDGEMENT bounded_measurable SUBTYPE_OF bounded
bounded_measurable_is_measurable:
JUDGEMENT bounded_measurable SUBTYPE_OF measurable_function
simple_is_bounded_measurable:
JUDGEMENT simple SUBTYPE_OF bounded_measurable
nn_bounded_measurable?(f):bool = bounded_measurable?(f) AND FORALL x: 0<=f(x)
nn_bounded_measurable: TYPE+ = (nn_bounded_measurable?)
CONTAINING (lambda x: 0)
nn_bounded_measurable_is_bounded_measurable:
JUDGEMENT nn_bounded_measurable SUBTYPE_OF bounded_measurable
increasing_nn_simple?(u):bool = (FORALL n: nn_simple?(u(n))) AND
pointwise_increasing?(u)
increasing_nn_simple: TYPE+ = (increasing_nn_simple?)
CONTAINING (lambda n: lambda x: 0)
p: VAR nn_bounded_measurable
w: VAR increasing_nn_simple
sup_norm_simple: LEMMA EXISTS h: (forall x: 0 <= h(x) & h(x) <= p(x)) AND
sup_norm(p-h) <= sup_norm(p)/2 % SKB 4.1.24
nn_simple_approx(p):nn_simple
= choose({h | (forall x: 0 <= h(x) & h(x) <= p(x)) AND
sup_norm(p-h) <= sup_norm(p)/2})
% The following IMPORT and recursive definition for proof only.
IMPORTING reals@sigma_nat
nn_simple_sequence(p)(n): RECURSIVE {h | forall x: 0 <= h(x) & h(x) <= p(x)}
= IF n = 0 THEN nn_simple_approx(p)
ELSE nn_simple_sequence(p-nn_simple_approx(p))(n-1) ENDIF
MEASURE (lambda p: lambda n: n)
nn_bounded_measurable_as_increasing_simple_sequence: % SKB 4.1.25
LEMMA EXISTS w: sup_norm_converges_to?(w,p)
nn_bounded_measurable_as_sequence_prop: LEMMA sup_norm_converges_to?(w,p) =>
(FORALL n,x: w(n)(x) <= p(x))
bounded_measurable_as_increasing_sequence: LEMMA % SKB 4.1.25
bounded_measurable?(f) => EXISTS v: sup_norm_converges_to?(v,f)
nn_measurable_def: LEMMA (FORALL x: 0 <= f(x)) => % SKB 4.1.26
(measurable_function?(f) <=> EXISTS w: pointwise_converges_upto?(w,f))
measurable_as_limit_simple_def: LEMMA % SKB 4.1.26
measurable_function?(f) <=> EXISTS v: pointwise_convergence?(v,f)
END measure_space
¤ Dauer der Verarbeitung: 0.2 Sekunden
(vorverarbeitet)
¤
|
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.
|
