Quelle  young.pvs

%------------------------------------------------------------------------------
% Young's Inequality (used in Holder's inequality)
%
%     Author: David Lester, Manchester University
%
% All references are to SK Berberian "Fundamentals of Real Analysis",
% Springer, 1991
%
%     Version 1.0            12/3/10   Initial Version
%------------------------------------------------------------------------------

young: THEORY

BEGIN

  IMPORTING power@real_expt,
            power@log,
            power@ln_exp_def % eventually this is part of lnexp_fnd@ln_exp

  x,y:   VAR real
  r:     VAR posreal
  a,b:   VAR nnreal
  p,q:   VAR {r | r > 1}
  c:     VAR {r | r < 1}

  youngs_aux:        LEMMA (1-c) + c*p - p^c > 0

  youngs_inequality: LEMMA 1/p + 1/q = 1 => a*b <= a^p/p + b^q/q    % SKB 3.1.3

END young