|
%------------------------------------------------------------------------------
% p-th power integrable
%
% Author: David Lester, Manchester University
%
% Version 1.0 12/03/10 Initial version (DRL)
%------------------------------------------------------------------------------
p_integrable[(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],
minkowski_scaf[T,S,mu,p]
x: VAR T
f,f0,f1: VAR p_integrable
c: VAR complex
scal_p_integrable: JUDGEMENT *(c,f) HAS_TYPE p_integrable
sum_p_integrable: JUDGEMENT +(f0,f1) HAS_TYPE p_integrable
opp_p_integrable: JUDGEMENT -(f) HAS_TYPE p_integrable
diff_p_integrable: JUDGEMENT -(f0,f1) HAS_TYPE p_integrable
norm_scal: LEMMA norm(c*f) = abs(c)*norm(f)
norm_add: LEMMA norm(f0+f1) <= norm(f0)+norm(f1)
norm_opp: LEMMA norm(-f) = norm(f)
norm_diff: LEMMA norm(f0-f1) <= norm(f0)+norm(f1)
END p_integrable
¤ Dauer der Verarbeitung: 0.16 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.
|
