Quelle probability_measure.pvs Sprache: 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

quality96%

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