Quelle  minkowski_scaf.pvs

%------------------------------------------------------------------------------
% 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