Quelle probability_space.pvs Sprache: PVS

probability_space[T:TYPE+,(IMPORTING measure_integration@subset_algebra_def[T])
                  S:sigma_algebra,   (IMPORTING probability_measure[T,S])
                  P:probability_measure]: THEORY

BEGIN

   IMPORTING measure_integration@sigma_algebra[T,S],
             probability_measure[T,S],
             continuous_functions_aux[real],
             measure_integration@measure_space[T,S],
             measure_integration@measure_props[T,S,to_measure(P)],
             measure_integration@real_borel

   limit: MACRO [(convergence_sequences.convergent?)->real]
                                                  = convergence_sequences.limit

   phi,g,h: VAR borel_function
   B1,B2:   VAR borel
   A,B: VAR (S)
   x,y: VAR real
   n0z: VAR nzreal
   t:   VAR T
   n:   VAR nat
   X,Y: VAR random_variable
   XS:  VAR [nat->random_variable]

   null?(A)         :bool = P(A) = 0
   non_null?(A)     :bool = NOT null?(A)
   independent?(A,B):bool = P(intersection(A,B)) = P(A) * P(B)

% Note carefully that the above DOES NOT say: ... = 0

   zero: random_variable = (LAMBDA t: 0)
   one:  random_variable = (LAMBDA t: 1)

   ; % needed for syntax purposes!

   <=(X,x):(S) = {t | X(t) <= x};
   <(x,X): (S) = {t | X(t) >  x};
   =(X,x): (S) = {t | X(t) =  x};
   <(X,x): (S) = {t | X(t) <  x};
   <=(x,X):(S) = {t | X(t) >= x};
   /=(X,x):(S) = {t | X(t) /= x};

   complement_le1: LEMMA complement(X <= x) = (x <  X)
   complement_lt1: LEMMA complement(x <  X) = (X <= x)
   complement_eq : LEMMA complement(X =  x) = (X /= x)
   complement_lt2: LEMMA complement(X <  x) = (x <= X)
   complement_le2: LEMMA complement(x <= X) = (X <  x)
   complement_ne:  LEMMA complement(X /= x) = (X =  x)

   ; % needed for syntax purposes!

   +(X,x)  :random_variable = (LAMBDA t: X(t) + x);
   +(x,X)  :random_variable = (LAMBDA t: x + X(t));
   -(X,x)  :random_variable = (LAMBDA t: X(t) - x);
   -(x,X)  :random_variable = (LAMBDA t: x - X(t));
   /(X,n0z):random_variable = (LAMBDA t: X(t)/n0z);

   independent?(X,Y):bool
     = FORALL B1,B2: independent?(inverse_image(X,B1),inverse_image(Y,B2))

   borel_comp_rv_is_rv: JUDGEMENT o(phi,X) HAS_TYPE random_variable

   borel_independence: LEMMA independent?(X,Y) => independent?(g o X, h o Y)

   partial_sum_is_random_variable:
     LEMMA random_variable?(LAMBDA t: sigma(0,n,LAMBDA n: XS(n)(t)))

   distribution_function?(F:[real->probability]):bool
                                       = EXISTS X: FORALL x: F(x) = P(X <= x)

   distribution_function: TYPE+ = (distribution_function?) CONTAINING
                                      (LAMBDA x: IF x < 0 THEN 0 ELSE 1 ENDIF)

   distribution_function(X)(x):probability = P(X <= x)

   convergence_in_distribution?(XS,X):bool
     = FORALL x: continuous?(distribution_function(X),x) IMPLIES
                  convergence((LAMBDA n: distribution_function(XS(n))(x)),
                                         distribution_function(X)(x))
% Lemma 2.1.11 (G&S)

   invert_distribution:   LEMMA LET F = distribution_function(X) IN
                                P(x < X) = 1 - F(x)
   interval_distribution: LEMMA LET F = distribution_function(X) IN
                                x <= y IMPLIES
                                P(intersection(x < X, X <= y)) = F(y) - F(x)
   limit_distribution:    LEMMA LET F = distribution_function(X) IN
                                P(X = x) = F(x) - limit(LAMBDA n: F(x-1/(n+1)))

% Lemma 2.1.6 in G&S

   F: VAR distribution_function

   distribution_0:                LEMMA convergence(F o (lambda (n:nat): -n),0)
   distribution_1:                LEMMA convergence(F,1)
   distribution_increasing:       LEMMA increasing?[real](F)
   distribution_right_continuous: LEMMA right_continuous?(F)


END probability_space

quality52%

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