|
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.24 Sekunden
(vorverarbeitet)
¤
|
Laden
Fehler beim Verzeichnis:
in der Quellcodebibliothek suchen
Die farbliche Syntaxdarstellung ist noch experimentell.
|
