Quelle sigma_countable.pvs Sprache: PVS

sigma_countable[T:TYPE]: THEORY
%------------------------------------------------------------------------------
% The sigma_set theory introduces and defines properties of the sigma
% function that sums an arbitrary function F: [T -> real] over a countable
% set of values X. To make this sensible for infinite sets, we will also
% require that f is absolutely convergent in the infinite case.
%
% This notation is a vital simplification for discrete probability theory.
%
%                         ----
%  sigma(X, f)         =  \     f(x)
%                         /
%                         ----
%                      member(x,X)
%
%
%  MODIFICATIONS:
%
%     Author: David Lester, Manchester University 20/4/05
%
%     Additions 20/1/10 DR Lester
%
%------------------------------------------------------------------------------

BEGIN

  IMPORTING sets_aux@countable_props[T],
            countable_convergence[T]

  a:   VAR real
  X,Y: VAR countable_set
  t:   VAR T
  f,g: VAR [T -> real]
  F:   VAR non_empty_finite_set[T]
  n:   VAR nat
  phi: VAR (bijective?[nat,nat])
  npx: VAR npreal
  nnx: VAR nnreal

  sigma(X:countable_set[T],f:(convergent?(X))):real
    = IF empty?(X)
      THEN 0
      ELSIF is_finite(X)
      THEN sigma[below[card(X)]](0,card(X)-1,f o finite_enumeration(X))
      ELSE limit(series(f o denumerable_enumeration(X)))      ENDIF

  sigma_empty: LEMMA sigma(emptyset[T],g) = 0

  sigma_finite: LEMMA LET n = card(F)-1 IN
                sigma(F,g) = sigma[below[n+1]](0,n,g o finite_enumeration(F))

  sigma_singleton: LEMMA sigma(singleton(t),g) = g(t)

  sigma_infinite: LEMMA FORALL (X:countably_infinite_set,f:(convergent?(X))):
                  sigma(X,f) = limit(series(f o denumerable_enumeration(X)))

  nonempty_countable?(X:set[T]):bool = nonempty?(X) AND is_countable(X)

  nonempty_countable: TYPE = (nonempty_countable?)

  nonempty_countable_is_countable:
      JUDGEMENT nonempty_countable SUBTYPE_OF countable_set[T]

  nonempty_countable_is_nonempty:
      JUDGEMENT nonempty_countable SUBTYPE_OF (nonempty?[T])

  sigma_disjoint_union: LEMMA FORALL (f:(convergent?(union(X,Y)))):
    disjoint?(X,Y) => sigma(union(X,Y),f) = sigma(X,f) + sigma(Y,f)

  sigma_union: LEMMA FORALL (f:(convergent?(union(X,Y)))):
    sigma(union(X,Y),f) = sigma(X,f) + sigma(Y,f) - sigma(intersection(X,Y),f)

  sigma_intersection: LEMMA FORALL (f:(convergent?(union(X,Y)))):
    sigma(intersection(X,Y),f) = sigma(X,f) + sigma(Y,f) - sigma(union(X,Y),f)

  sigma_difference: LEMMA FORALL (f:(convergent?(union(X,Y)))):
    sigma(difference(X,Y),f)
         = sigma(X,f) - sigma(Y,f) + sigma(difference(Y,X),f)

  sigma_subset: LEMMA FORALL (f:(convergent?(Y))):
    subset?(X,Y) => sigma(Y,f) = sigma(X,f) + sigma(difference(Y,X),f)

  sigma_add: LEMMA FORALL (f:(convergent?(X))):
      sigma(add(t,X),f) = IF member(t,X) THEN sigma(X,f)
                                         ELSE f(t) + sigma(X,f) ENDIF

  sigma_remove: LEMMA FORALL (f:(convergent?(X))):
      sigma(remove(t,X),f) = IF member(t,X) THEN sigma(X,f) - f(t)
                                            ELSE sigma(X,f) ENDIF

  sigma_choose_rest: LEMMA FORALL (X:nonempty_countable,f:(convergent?(X))):
                           sigma(X,f) = f(choose(X)) + sigma(rest(X),f)

  sigma_zero: LEMMA sigma(X,LAMBDA t: 0) = 0

  sigma_scal: LEMMA FORALL (f:(convergent?(X))): sigma(X,a*f) = a*sigma(X,f)

  sigma_opp:  LEMMA FORALL (f:(convergent?(X))): sigma(X,-f)  = -sigma(X,f)

  sigma_plus: LEMMA FORALL (f,g:(convergent?(X))):
                                      sigma(X,f+g) = sigma(X,f) + sigma(X,g)

  sigma_diff: LEMMA FORALL (f,g:(convergent?(X))):
                                      sigma(X,f-g) = sigma(X,f) - sigma(X,g)

  sigma_ge_0: LEMMA FORALL (f:(convergent?(X))):
                           (FORALL (t:(X)): f(t) >= 0) => sigma(X,f) >= 0

  sigma_gt_0: LEMMA FORALL (X:nonempty_countable,f:(convergent?(X))):
                           (FORALL (t:(X)): f(t) >  0) => sigma(X,f) > 0

  sigma_abs:  LEMMA FORALL (f:(convergent?(X))):
                                      abs(sigma(X,f)) <= sigma(X,abs(f))

  sigma_eq:   LEMMA FORALL (f,g:(convergent?(X))):
                    (FORALL (t:(X)): f(t) =  g(t)) => sigma(X,f) =  sigma(X,g)

  sigma_le:   LEMMA FORALL (f,g:(convergent?(X))):
                    (FORALL (t:(X)): f(t) <= g(t)) => sigma(X,f) <= sigma(X,g)

  sigma_lt:   LEMMA FORALL (X:nonempty_countable,f,g:(convergent?(X))):
                    (FORALL (t:(X)): f(t) <  g(t)) => sigma(X,f) <  sigma(X,g)

  IMPORTING reals@bounded_reals,
            sigma_bijection_nat

  sigma_bij: LEMMA FORALL (f:(convergent?(X)),phi:(bijective?[(X),(X)])):
                   sigma(X,extend[T,(X),real,0](f o phi)) = sigma(X,f)

  sigma_nn_def: LEMMA
    FORALL (f:(convergent?(X))):
           (FORALL t: X(t) => f(t) >= 0) =>
           sigma(X,f)
                 = sup({nnx | EXISTS (F:finite_set[T]):
                              subset?(F,X) AND nnx = sigma(F,f)})

  sigma_def: LEMMA
    FORALL (f:(convergent?(X))):
           sigma(X,f)
                 = sup({nnx | EXISTS (F:finite_set[T]): subset?(F,X) AND
                                        (FORALL t: F(t) => f(t) >= 0) AND
                                        nnx = sigma(F,f)}) +
                   inf({npx | EXISTS (F:finite_set[T]): subset?(F,X) AND
                                        (FORALL t: F(t) => f(t) <= 0) AND
                                         npx = sigma(F,f)})

END sigma_countable

quality40%

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