Quelle complex_integral.pvs Sprache: 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

quality88%

¤ Dauer der Verarbeitung: 0.0 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.