|
probability_measure[T:TYPE+,(IMPORTING measure_integration@subset_algebra_def[T])
S:sigma_algebra]: THEORY
BEGIN
IMPORTING measure_integration@sigma_algebra[T,S],
measure_integration@measure_def[T,S],
%% ..... @fun_preds[T,real],
reals@real_fun_ops[T],
structures@fun_preds_partial[nat,set[T],reals.<=,subset?[T]],
metric_space@real_topology,
topology@basis[real],
%% metric_space@borel[real,metric_induced_topology],
measure_integration@hausdorff_borel[real,metric_induced_topology],
measure_integration@real_borel,
measure_integration@measure_space_def[T,S],
measure_integration@finite_measure
probability: TYPE+ = {x:nnreal | x <= 1} CONTAINING 1
nzprobability: TYPE+ = {x:posreal | x <= 1} CONTAINING 1
nzprobability_is_probability: JUDGEMENT nzprobability SUBTYPE_OF probability
probability_measure_full?(P:[(S)->probability]):bool = P(fullset[T])= 1
probability_measure?(P:[(S)->probability]):bool
= probability_measure_full?(P) AND finite_measure?(P)
trivial_probability_measure(A:(S)):probability
= IF member(choose(fullset[T]),A) THEN 1 ELSE 0 ENDIF
probability_measure: TYPE+ = (probability_measure?)
CONTAINING trivial_probability_measure
probability_measure_is_finite_measure:
JUDGEMENT probability_measure SUBTYPE_OF finite_measure
random_variable?(f:[T->real]):bool = measurable_function?(f)
random_variable: TYPE+ = (measurable_function?) CONTAINING (lambda (x:T): 0)
random_variable_is_measurable_function:
JUDGEMENT random_variable SUBTYPE_OF measurable_function
P: VAR probability_measure
A,B: VAR (S)
SS: VAR disjoint_indexed_measurable
X: VAR sequence[(S)]
Y: VAR random_variable
x: VAR real
t: VAR T
P_fullset: LEMMA P(fullset) = 1
P_convergence: LEMMA convergence(series(P o SS), P(IUnion(SS)))
P_emptyset: LEMMA P(emptyset) = 0
P_disjointunion:LEMMA disjoint?(A,B) => P(union(A,B)) = P(A) + P(B)
P_complement: LEMMA P(complement(A)) = 1 - P(A)
P_union: LEMMA P(union(A,B)) = P(A) + P(B) - P(intersection(A,B))
P_intersection: LEMMA P(intersection(A,B))= P(A) + P(B) - P(union(A,B))
P_difference: LEMMA P(difference(A,B)) = P(A) - P(B) + P(difference(B,A))
P_subset: LEMMA subset?(A,B) => P(B) = P(A) + P(difference(B,A))
P_subset_le: LEMMA subset?(A,B) => P(A) <= P(B)
P_IUnion: LEMMA increasing?(X) => convergence(P o X,P(IUnion(X)))
P_IIntersection:LEMMA decreasing?(X) => convergence(P o X,P(IIntersection(X)))
P0_intersection:LEMMA P(A) = 0 => P(intersection(A,B)) = 0
P0_union: LEMMA P(A) = 0 => P(union(A,B)) = P(B)
P1_intersection:LEMMA P(A) = 1 => P(intersection(A,B)) = P(B)
P1_union: LEMMA P(A) = 1 => P(union(A,B)) = 1
measure_to_df(P)(Y)(x):probability = P({t | Y(t) <= x})
END probability_measure
¤ Dauer der Verarbeitung: 0.16 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.
|
