Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: monotone_classes.pvs Sprache: PVS

Original von: PVS^©

%------------------------------------------------------------------------------
% Integrals of functions [T->complex]
%
%     Author: David Lester, Manchester University
%
% All references are to SK Berberian "Fundamentals of Real Analysis",
% Springer, 1991
%
% Definition and basic properties of integrals for functions f: [T->complex]
%
%     Version 1.0            1/5/07   Initial Version
%------------------------------------------------------------------------------

complex_integral[(IMPORTING measure_integration@subset_algebra_def,
                            measure_integration@measure_def)
                 T:TYPE, S:sigma_algebra[T], mu:measure_type[T,S]]: THEORY

BEGIN

  IMPORTING measure_integration@integral[T,S,mu],
            complex_alt@complex_fun_ops[T],
            complex_measure_theory[T,S,mu]

  x: VAR T
  c: VAR complex

  integrable?(f:[T->complex]): bool =
    integrable?(Re(f)) AND integrable?(Im(f))

  integrable: TYPE+ = (integrable?) CONTAINING (lambda x: complex_(0,0))

  integral(f:integrable):complex = complex_(integral(Re(f)),integral(Im(f)))

  f,f1,f2: VAR integrable

  integrable_def: LEMMA FORALL (f:[T->complex]):
                        integrable?(f) IFF
                        (integrable?(Re(f)) AND integrable?(Im(f)))

  Re_integral: LEMMA Re(integral(f)) = integral(Re(f))
  Im_integral: LEMMA Im(integral(f)) = integral(Im(f))

  AUTO_REWRITE+ integrable_def
  AUTO_REWRITE+ Re_integral
  AUTO_REWRITE+ Im_integral

  integrable_is_measurable: JUDGEMENT integrable SUBTYPE_OF complex_measurable
  cal_N_is_measurable:      JUDGEMENT cal_N      SUBTYPE_OF integrable

  integrable_add:  JUDGEMENT +(f1,f2)    HAS_TYPE integrable
  integrable_scal: JUDGEMENT *(c,f)      HAS_TYPE integrable
  integrable_opp:  JUDGEMENT -(f)        HAS_TYPE integrable
  integrable_diff: JUDGEMENT -(f1,f2)    HAS_TYPE integrable
  integrable_abs:  JUDGEMENT abs(f)      HAS_TYPE integral.integrable

  integral_add:    LEMMA integral(f1+f2)  = integral(f1) + integral(f2)
  integral_scal:   LEMMA integral(c*f)    = c*integral(f)
  integral_opp:    LEMMA integral(-f)     = -integral(f)
  integral_diff:   LEMMA integral(f1-f2)  = integral(f1) - integral(f2)

  integral_abs:    LEMMA abs(integral(f)) <= integral(abs(f))           % 6.4.6

END complex_integral

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht sprechenden Kalenders
Eigene Datei ansehen

Haftungshinweis

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.