products/sources/formale sprachen/Isabelle/HOL/Analysis/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: TestClass.vdmpp   Sprache: PVS

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

¤ Dauer der Verarbeitung: 0.0 Sekunden  (vorverarbeitet)  ¤



Kontakt
Drucken
Kontakt
sprechenden Kalenders

Eigene Datei ansehen




schauen Sie vor die Tür

Fenster


Die Firma ist wie angegeben erreichbar.

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff