products/sources/formale Sprachen/PVS/complex_integration/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: young.pvs   Sprache: PVS

Original von: 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

¤ Dauer der Verarbeitung: 0.14 Sekunden  (vorverarbeitet)  ¤



Kontakt
Drucken
Kontakt
sprechenden Kalenders

in der Quellcodebibliothek suchen




schauen Sie vor die Tür

Fenster


Die Firma ist wie angegeben erreichbar.

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff