| products/Sources/formale Sprachen/PVS/probability/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: probability_space.pvs Sprache: PVSOriginal von: 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 ¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤ |
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.Bot Zugriff |
