%------------------------------------------------------------------------------ % 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.1 Sekunden
(vorverarbeitet)
¤
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.
