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: root.tex   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.35 Sekunden  (vorverarbeitet)  ¤



Druckansicht
unsichere Verbindung
Druckansicht
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