|
%------------------------------------------------------------------------------
% p-th power integrable definitions
%
% Author: David Lester, Manchester University
%
% Version 1.0 12/03/10 Initial version (DRL)
%------------------------------------------------------------------------------
p_integrable_def[(IMPORTING measure_integration@subset_algebra_def,
measure_integration@measure_def)
T:TYPE, S:sigma_algebra[T],
mu:measure_type[T,S], p:{a:real | a >= 1}]: THEORY
BEGIN
IMPORTING complex_integral,
complex_measure_theory[T,S,mu],
measure_integration@integral[T,S,mu]
h: VAR [T->complex]
x: VAR T
p_integrable?(h):bool = complex_measurable?(h) AND integrable?(abs(h)^p)
p_integrable: TYPE+ = (p_integrable?) CONTAINING (lambda x: complex_(0,0))
cal_N_is_p_integrable: JUDGEMENT cal_N SUBTYPE_OF p_integrable
f: VAR p_integrable
norm(f):nnreal = integral(abs(f)^p)^(1/p)
norm_eq_0: LEMMA norm(f) = 0 <=> cal_N?(f)
END p_integrable_def
¤ Dauer der Verarbeitung: 0.15 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.
|
