Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Eigene Datei ansehen e.g. http://myserver.net/mysource.java Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/MASM/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 24.1.2002 mit Größe 677 B

complex_measurable.pvs Interaktion und
PortierbarkeitPVS

%------------------------------------------------------------------------------
% Measurable 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 measurable functions f: [T->complex]
%
%     Version 1.0            10/3/10   Initial Version
%------------------------------------------------------------------------------

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

BEGIN

  IMPORTING measure_integration@measure_space[T,S],
            complex_alt@complex_fun_ops[T],
            structures@const_fun_def[T,complex],
            complex_topology

  f: VAR [T->complex]
  s: VAR sequence[[T->complex]]
  x: VAR T
  c: VAR complex
  n: VAR nat
  a: VAR posreal

  complex_measurable?(f):bool = measurable_function?(Re(f)) AND     % SKB 6.4.1
                                measurable_function?(Im(f))

  complex_measurable: TYPE+ = (complex_measurable?)
                                           CONTAINING (LAMBDA x: complex_(0,0))

  complex_measurable_def:
    LEMMA complex_measurable?(f) <=>
          (measurable_function?(Re(f)) AND measurable_function?(Im(f)))

  AUTO_REWRITE+ complex_measurable_def

  g,g1,g2: VAR complex_measurable

  constant_is_complex_measurable: JUDGEMENT (constant?[T,complex]) SUBTYPE_OF
                                                            complex_measurable

  pointwise_convergence?(s,f):bool
    = FORALL x: convergence?(lambda n: s(n)(x),f(x))

  scal_complex_measurable:  JUDGEMENT *(c,g)   HAS_TYPE complex_measurable
  sum_complex_measurable:   JUDGEMENT +(g1,g2) HAS_TYPE complex_measurable
  opp_complex_measurable:   JUDGEMENT -(g)     HAS_TYPE complex_measurable
  diff_complex_measurable:  JUDGEMENT -(g1,g2) HAS_TYPE complex_measurable

  const_measurable:    LEMMA  complex_measurable?(lambda x: c)

  abs_complex_measurable:      JUDGEMENT abs(g)    HAS_TYPE measurable_function
  sq_complex_measurable:       JUDGEMENT sq(g)     HAS_TYPE complex_measurable
  prod_complex_measurable:     JUDGEMENT *(g1,g2)  HAS_TYPE complex_measurable
  abs_expt_measurable: LEMMA measurable_function?(abs(g)^a)

  u: VAR sequence[complex_measurable]

  pointwise_complex_measurable: LEMMA            % complex analog to SKB 4.1.20
    pointwise_convergence?(u,f) => complex_measurable?(f)

END complex_measurable

quality77%

¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.15Angebot Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤

*Eine klare Vorstellung vom Zielzustand

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.