SSL complex_measurable.pvs Sprache: PVS

%------------------------------------------------------------------------------
% 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%

¤ Dauer der Verarbeitung: 0.17 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.