|
%------------------------------------------------------------------------------
% Measurable functions [T->complex]
%
% Author: David Lester, Manchester University
%
% All references are to SK Berberian "Fundamentals of Real Analysis",
% Springer, 1991
%
% Definition and basic properties of measurable functions f: [T->complex]
%
% Version 1.0 10/3/10 Initial Version
%------------------------------------------------------------------------------
complex_measurable[(IMPORTING measure_integration@subset_algebra_def,
measure_integration@measure_def)
T:TYPE, S:sigma_algebra[T]]: THEORY
BEGIN
IMPORTING measure_integration@measure_space[T,S],
complex_alt@complex_fun_ops[T],
structures@const_fun_def[T,complex],
complex_topology
f: VAR [T->complex]
s: VAR sequence[[T->complex]]
x: VAR T
c: VAR complex
n: VAR nat
a: VAR posreal
complex_measurable?(f):bool = measurable_function?(Re(f)) AND % SKB 6.4.1
measurable_function?(Im(f))
complex_measurable: TYPE+ = (complex_measurable?)
CONTAINING (LAMBDA x: complex_(0,0))
complex_measurable_def:
LEMMA complex_measurable?(f) <=>
(measurable_function?(Re(f)) AND measurable_function?(Im(f)))
AUTO_REWRITE+ complex_measurable_def
g,g1,g2: VAR complex_measurable
constant_is_complex_measurable: JUDGEMENT (constant?[T,complex]) SUBTYPE_OF
complex_measurable
pointwise_convergence?(s,f):bool
= FORALL x: convergence?(lambda n: s(n)(x),f(x))
scal_complex_measurable: JUDGEMENT *(c,g) HAS_TYPE complex_measurable
sum_complex_measurable: JUDGEMENT +(g1,g2) HAS_TYPE complex_measurable
opp_complex_measurable: JUDGEMENT -(g) HAS_TYPE complex_measurable
diff_complex_measurable: JUDGEMENT -(g1,g2) HAS_TYPE complex_measurable
const_measurable: LEMMA complex_measurable?(lambda x: c)
abs_complex_measurable: JUDGEMENT abs(g) HAS_TYPE measurable_function
sq_complex_measurable: JUDGEMENT sq(g) HAS_TYPE complex_measurable
prod_complex_measurable: JUDGEMENT *(g1,g2) HAS_TYPE complex_measurable
abs_expt_measurable: LEMMA measurable_function?(abs(g)^a)
u: VAR sequence[complex_measurable]
pointwise_complex_measurable: LEMMA % complex analog to SKB 4.1.20
pointwise_convergence?(u,f) => complex_measurable?(f)
END complex_measurable
¤ Dauer der Verarbeitung: 0.18 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.
|
