Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: probability_measure.pvs Sprache: PVS

Original von: PVS^©

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.1 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.