|
%------------------------------------------------------------------------------
% Minkowski's inequality
%
% 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 13/3/10 Initial Version
%------------------------------------------------------------------------------
minkowski_scaf[(IMPORTING measure_integration@subset_algebra_def,
measure_integration@measure_def)
T:TYPE, S:sigma_algebra[T], mu:measure_type[T,S],
p:{x:real | x>=1}]: THEORY
BEGIN
IMPORTING p_integrable_def[T,S,mu,p],
holder_scaf
f,g: VAR p_integrable
minkowski_scaf: LEMMA p_integrable?(f+g) AND norm(f+g) <= norm(f) + norm(g)
END minkowski_scaf
¤ Dauer der Verarbeitung: 0.14 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.
|
