Quellcode-Bibliothek probability_space.prf
Sprache: Lisp
(probability_spacenil 3424623523"" (lemma "constant_is_measurable" )"" (inst - "(LAMBDA t: 0)" )"" (expand "constant?" )"" (expand "const_fun" )"" (assert ) (("" (inst?) nil nil )) nil )) nil ))nil ))nil ))nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" const_fun_def "structures/" )"[S -> T]" const_fun_def "structures/" )nil measure_space_def"measure_integration/" )nil probability_space nil )nil booleans nil )nil booleans nil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def"measure_integration/" )nil subset_algebra_def"measure_integration/" )"sigma_algebra" probability_space nil ))nil ))nil 3424623523"" (lemma "constant_is_measurable" )"" (inst - "(LAMBDA t: 1)" )"" (expand "constant?" )"" (expand "const_fun" ) (("" (inst?) nil nil )) nil )) nil ))nil ))nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" const_fun_def "structures/" )"[S -> T]" const_fun_def "structures/" )nil measure_space_def"measure_integration/" )nil probability_space nil )nil booleans nil )nil booleans nil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def"measure_integration/" )nil subset_algebra_def"measure_integration/" )"sigma_algebra" probability_space nil ))nil ))nil 3314025598"" (skosimp)"" (typepred "X!1" )"" (lemma "measurable_le" ("f" "X!1" ))"" (assert ) (("" (inst - "x!1" ) nil nil )) nil )) nil ))nil ))nil )nil probability_measure nil )"bool" measure_space_def"measure_integration/" )"sigma_algebra" probability_space nil )nil subset_algebra_def"measure_integration/" )"bool" subset_algebra_def"measure_integration/" )nil sets nil )nil defined_types nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil probability_space nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil measure_space_def"measure_integration/" ))nil 3314191251"" (skosimp)"" (typepred "X!1" )"" (lemma "measurable_gt" ("f" "X!1" ))"" (assert ) (("" (inst - "x!1" ) nil nil )) nil )) nil ))nil ))nil )nil probability_measure nil )"bool" measure_space_def"measure_integration/" )"sigma_algebra" probability_space nil )nil subset_algebra_def"measure_integration/" )"bool" subset_algebra_def"measure_integration/" )nil sets nil )nil defined_types nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil probability_space nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil measure_space_def"measure_integration/" ))nil 3314190689"" (skosimp)"" (typepred "X!1" )"" (lemma "measurable_ge" ("f" "X!1" ))"" (lemma "measurable_le" ("f" "X!1" ))"" (assert )"" (inst - "x!1" )"" (inst - "x!1" )"" "measurable_intersection" "a" "{z: T | X!1(z) <= x!1}" "b" "{z: T | X!1(z) >= x!1}" ))"1" "(intersection[T] ") "1" (expand "measurable_set?" )"1" (propax) nil nil )) nil )"2" (hide-all-but 1)"2" (apply-extensionality :hide? t)"2" (grind) nil nil )) nil ))nil ))nil )"2" (expand "measurable_set?" )"2" (propax) nil nil )) nil )"3" (expand "measurable_set?" )"3" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil probability_measure nil )"bool" measure_space_def"measure_integration/" )"sigma_algebra" probability_space nil )nil subset_algebra_def"measure_integration/" )"bool" subset_algebra_def"measure_integration/" )nil sets nil )nil defined_types nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil probability_space nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil measure_space_def"measure_integration/" )"bool" reals nil ) (<= const-decl "bool" reals nil )nil measure_space_def"measure_integration/" )"bool" measure_space_def"measure_integration/" )set type-eq-decl nil sets nil )nil measure_space_def"measure_integration/" )"real" reals nil )"bool" sets nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"[T, T -> boolean]" equalities nil )"set" sets nil )nil measure_space_def"measure_integration/" ))nil 3314191439"" (skosimp)"" (typepred "X!1" )"" (lemma "measurable_lt" ("f" "X!1" ))"" (assert ) (("" (inst - "x!1" ) nil nil )) nil )) nil ))nil ))nil )nil probability_measure nil )"bool" measure_space_def"measure_integration/" )"sigma_algebra" probability_space nil )nil subset_algebra_def"measure_integration/" )"bool" subset_algebra_def"measure_integration/" )nil sets nil )nil defined_types nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil probability_space nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil measure_space_def"measure_integration/" ))nil 3314190689"" (skosimp)"" (typepred "X!1" )"" (lemma "measurable_ge" ("f" "X!1" ))"" (assert ) (("" (inst - "x!1" ) nil nil )) nil )) nil ))nil ))nil )nil probability_measure nil )"bool" measure_space_def"measure_integration/" )"sigma_algebra" probability_space nil )nil subset_algebra_def"measure_integration/" )"bool" subset_algebra_def"measure_integration/" )nil sets nil )nil defined_types nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil probability_space nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil measure_space_def"measure_integration/" ))nil 3314191820"" (skosimp)"" (typepred "X!1" )"" (lemma "measurable_gt" ("f" "X!1" ))"" (lemma "measurable_lt" ("f" "X!1" ))"" (assert )"" (inst - "x!1" )"" (inst - "x!1" )"" "measurable_union" "a" "{z: T | X!1(z) < x!1}" "b" "{z: T | X!1(z) > x!1}" ))"1" "(union[T] ") "1" (expand "measurable_set?" )"1" (propax) nil nil )) nil )"2" (hide-all-but 1)"2" (apply-extensionality :hide? t)"2" (grind) nil nil )) nil ))nil ))nil )"2" (expand "measurable_set?" )"2" (propax) nil nil )) nil )"3" (expand "measurable_set?" )"3" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil probability_measure nil )"bool" measure_space_def"measure_integration/" )"sigma_algebra" probability_space nil )nil subset_algebra_def"measure_integration/" )"bool" subset_algebra_def"measure_integration/" )nil sets nil )nil defined_types nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil probability_space nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil measure_space_def"measure_integration/" )"bool" reals nil ) (< const-decl "bool" reals nil )nil measure_space_def"measure_integration/" )"bool" measure_space_def"measure_integration/" )set type-eq-decl nil sets nil )nil measure_space_def"measure_integration/" )"real" reals nil )"bool" sets nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"[T, T -> boolean]" equalities nil )"set" sets nil )"boolean" notequal nil )nil measure_space_def"measure_integration/" ))nil 3321716438"" (skosimp)"" (expand "<=" )"" (expand "<" )"" (expand "complement" )"" (expand "member" )"" (apply-extensionality 1 :hide? t) nil nil )) nil ))nil ))nil ))nil ))nil )"(S)" probability_space nil )"set" sets nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def"measure_integration/" )nil subset_algebra_def"measure_integration/" )"sigma_algebra" probability_space nil )"bool" measure_space_def"measure_integration/" )nil probability_measure nil )"bool" reals nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil booleans nil )nil probability_space nil )"bool" sets nil )"(S)" probability_space nil ))nil 3321716510"" (skosimp)"" (expand "<=" )"" (expand "<" )"" (expand "complement" )"" (expand "member" )"" (apply-extensionality :hide? t) nil nil )) nil ))nil ))nil ))nil ))nil )"(S)" probability_space nil )"set" sets nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def"measure_integration/" )nil subset_algebra_def"measure_integration/" )"sigma_algebra" probability_space nil )"bool" measure_space_def"measure_integration/" )nil probability_measure nil )"bool" reals nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil booleans nil )nil probability_space nil )"bool" sets nil )"(S)" probability_space nil ))nil 3321716535"" (skosimp)"" (expand "=" )"" (expand "/=" )"" (expand "complement" )"" (expand "member" )"" (apply-extensionality :hide? t) nil nil )) nil ))nil ))nil ))nil ))nil )"(S)" probability_space nil )"set" sets nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[T, T -> boolean]" equalities nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def"measure_integration/" )nil subset_algebra_def"measure_integration/" )"sigma_algebra" probability_space nil )"bool" measure_space_def"measure_integration/" )nil probability_measure nil )"boolean" notequal nil )nil booleans nil )nil probability_space nil )"bool" sets nil )"(S)" probability_space nil ))nil 3321716558"" (skosimp)"" (expand "<" )"" (expand "<=" )"" (expand "complement" )"" (expand "member" )"" (apply-extensionality :hide? t) nil nil )) nil ))nil ))nil ))nil ))nil )"(S)" probability_space nil )"set" sets nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def"measure_integration/" )nil subset_algebra_def"measure_integration/" )"sigma_algebra" probability_space nil )"bool" measure_space_def"measure_integration/" )nil probability_measure nil )"bool" reals nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil booleans nil )nil probability_space nil )"bool" sets nil )"(S)" probability_space nil ))nil 3321716586"" (skosimp)"" (expand "<=" )"" (expand "<" )"" (expand "complement" )"" (apply-extensionality :hide? t)"" (expand "member" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"(S)" probability_space nil )"set" sets nil )nil probability_space nil )nil booleans nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"bool" reals nil )nil probability_measure nil )"bool" measure_space_def"measure_integration/" )"sigma_algebra" probability_space nil )nil subset_algebra_def"measure_integration/" )"bool" subset_algebra_def"measure_integration/" )nil sets nil )nil defined_types nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )"bool" sets nil ) (set type-eq-decl nil sets nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )"(S)" probability_space nil ))nil 3321716617"" (skosimp)"" (expand "=" )"" (expand "/=" )"" (expand "complement" )"" (expand "member" )"" (apply-extensionality :hide? t) nil nil )) nil ))nil ))nil ))nil ))nil )"(S)" probability_space nil )"set" sets nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"boolean" notequal nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def"measure_integration/" )nil subset_algebra_def"measure_integration/" )"sigma_algebra" probability_space nil )"bool" measure_space_def"measure_integration/" )nil probability_measure nil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil probability_space nil )"bool" sets nil )"(S)" probability_space nil ))nil 3322049026"" (skosimp)"" (lemma "sum_measurable" ("g1" "X!1" "g2" "lambda (t:T): x!1" ))"1" (expand "+" ) (("1" (propax) nil nil )) nil )"2" (lemma "constant_is_measurable" )"2" (inst - "(LAMBDA (t: T): x!1)" )"2" (expand "constant?" )"2" (expand "const_fun" ) (("2" (inst?) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"sigma_algebra" probability_space nil )nil subset_algebra_def"measure_integration/" )"bool" subset_algebra_def"measure_integration/" )nil sets nil )nil defined_types nil )nil booleans nil )nil booleans nil )nil probability_space nil )nil probability_measure nil )nil measure_space_def"measure_integration/" )"bool" measure_space_def"measure_integration/" )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil measure_space_def"measure_integration/" )"[T -> real]" real_fun_ops "reals/" )"bool" const_fun_def "structures/" )"real" probability_space nil )"[S -> T]" const_fun_def "structures/" )nil measure_space_def"measure_integration/" ))nil 3351240565"" (skosimp)"" (lemma "sum_measurable" ("g1" "lambda (t:T): x!1" "g2" "X!1" ))"1" (expand "+" ) (("1" (assert ) nil nil )) nil )"2" (lemma "constant_is_measurable" )"2" (inst - "(LAMBDA (t: T): x!1)" )"2" (expand "constant?" )"2" (expand "const_fun" ) (("2" (inst?) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"sigma_algebra" probability_space nil )nil subset_algebra_def"measure_integration/" )"bool" subset_algebra_def"measure_integration/" )nil sets nil )nil defined_types nil )nil booleans nil )nil booleans nil )nil probability_space nil )nil probability_measure nil )nil measure_space_def"measure_integration/" )"bool" measure_space_def"measure_integration/" )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil measure_space_def"measure_integration/" )"real" reals nil )"[T -> real]" real_fun_ops "reals/" )"bool" const_fun_def "structures/" )"real" probability_space nil )"[S -> T]" const_fun_def "structures/" )nil measure_space_def"measure_integration/" ))nil ))nil 3351275929"" (skosimp)"" (lemma "constant_is_measurable" )"" (inst - "lambda t: x!1" )"1" "diff_measurable" ("g1" "X!1" "g2" "LAMBDA t: x!1" ))"1" (expand "-" -1) (("1" (propax) nil nil )) nil )"2" (propax) nil nil ))nil )"2" (expand "constant?" )"2" (expand "const_fun" ) (("2" (inst?) nil nil )) nil ))nil ))nil ))nil ))nil )"sigma_algebra" probability_space nil )nil subset_algebra_def"measure_integration/" )"bool" subset_algebra_def"measure_integration/" )nil sets nil )nil defined_types nil )nil booleans nil )nil booleans nil )nil probability_space nil )nil measure_space_def"measure_integration/" )"[S -> T]" const_fun_def "structures/" )nil probability_measure nil )nil measure_space_def"measure_integration/" )"bool" measure_space_def"measure_integration/" )nil measure_space_def"measure_integration/" )"[T -> real]" real_fun_ops "reals/" )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" const_fun_def "structures/" )"real" probability_space nil ))nil ))nil 3351920614"" (skosimp)"" (lemma "constant_is_measurable" )"" (inst - "lambda t: x!1" )"1" "diff_measurable" ("g2" "X!1" "g1" "LAMBDA t: x!1" ))"1" (expand "-" -1) (("1" (propax) nil nil )) nil )"2" (propax) nil nil ))nil )"2" (expand "constant?" )"2" (expand "const_fun" ) (("2" (inst?) nil nil )) nil ))nil ))nil ))nil ))nil )"sigma_algebra" probability_space nil )nil subset_algebra_def"measure_integration/" )"bool" subset_algebra_def"measure_integration/" )nil sets nil )nil defined_types nil )nil booleans nil )nil booleans nil )nil probability_space nil )nil measure_space_def"measure_integration/" )"[S -> T]" const_fun_def "structures/" )nil probability_measure nil )nil measure_space_def"measure_integration/" )"bool" measure_space_def"measure_integration/" )nil measure_space_def"measure_integration/" )"[T -> real]" real_fun_ops "reals/" )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" const_fun_def "structures/" )"real" probability_space nil ))nil ))nil 3351920614"" (skosimp)"" (lemma "scal_measurable" ("c" "1/n0z!1" "g" "X!1" ))"" (expand "*" ) (("" (assert ) nil nil )) nil )) nil ))nil )"sigma_algebra" probability_space nil )nil subset_algebra_def"measure_integration/" )"bool" subset_algebra_def"measure_integration/" )nil sets nil )nil defined_types nil )nil booleans nil )nil booleans nil )nil probability_space nil )nil probability_measure nil )nil measure_space_def"measure_integration/" )"bool" measure_space_def"measure_integration/" )nil reals nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil measure_space_def"measure_integration/" )"nzreal" nil )"real" reals nil )"real" reals nil )"[T -> real]" real_fun_ops "reals/" ))nil ))nil 3509255376 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil probability_space nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def"measure_integration/" )nil subset_algebra_def"measure_integration/" )"sigma_algebra" probability_space nil )"bool" measure_space_def"measure_integration/" )nil probability_measure nil )"bool" reals nil )nil real_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield, numfield -> numfield]" number_fields nil )"setofsets[T]" metric_space_def"metric_space/" )"sigma_algebra" borel "measure_integration/" )nil borel "measure_integration/" )"set" sets nil )"sigma_algebra" "measure_integration/" )"bool" topology "topology/" )"bool" metric_space_def "metric_space/" )"bool" sets nil )"set[T]" metric_space_def "metric_space/" )"bool" subset_algebra_def"measure_integration/" )"bool" countability "sets_aux/" )"bool" subset_algebra_def"measure_integration/" )"bool" subset_algebra_def"measure_integration/" )"bool" sets nil )"bool" measure_space_def"measure_integration/" )"(surjective?[setofsets[T], set[T]])" sets_lemmas nil )"(surjective?[setofsets[T], set[T]])" sets_lemmas_aux"measure_integration/" )"finite_set" finite_sets nil )"finite_set[T]" countable_props"sets_aux/" )"finite_set[T]" countable_setofsets"sets_aux/" )"finite_set[real]" measure_space"measure_integration/" )"compact[real, (metric_induced_topology)]" convergence_aux"metric_space/" )"clopen[real, (metric_induced_topology)]" convergence_aux"metric_space/" )"(borel?)" real_borel"measure_integration/" )"real" reals nil ))nil ))nil 3509204782"" (skosimp)"" (typepred "X!1" )"" (typepred "Y!1" )"" (typepred "g!1" )"" (typepred "h!1" )"" (expand "independent?" )"" (skosimp)"" (expand "borel_function?" )"" (expand "measurable_function?" )"" (inst -3 "B2!1" )"" (inst -4 "B1!1" )"" (inst -1 "B2!1" )"" (inst -2 "B1!1" )"" "inverse_image(g!1, B1!1)" "inverse_image(h!1, B2!1)" )"" "inverse_image(X!1, inverse_image(g!1, B1!1))=inverse_image(g!1 o X!1, B1!1)" )"1" "inverse_image(Y!1, inverse_image(h!1, B2!1))=inverse_image(h!1 o Y!1, B2!1)" )"1" "1" "1" expand "inverse_image" )"1" expand "o " )"1" expand "member" )"1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "o " )"2" expand "inverse_image" )"2" expand "member" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil probability_measure nil )"bool" measure_space_def"measure_integration/" )"sigma_algebra" probability_space nil )nil subset_algebra_def"measure_integration/" )"bool" subset_algebra_def"measure_integration/" )nil sets nil )nil defined_types nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil probability_space nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil borel_functions"measure_integration/" )"bool" borel_functions"measure_integration/" )"setofsets[T]" metric_space_def"metric_space/" )"[numfield, numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"bool" reals nil )"bool" probability_space nil )nil borel "measure_integration/" )"sigma_algebra" borel "measure_integration/" )set type-eq-decl nil sets nil )"set[D]" function_image nil )"borel_function[real, metric_induced_topology, real, metric_induced_topology]" nil )"borel[real, metric_induced_topology]" nil )"borel_function[real, metric_induced_topology, real, metric_induced_topology]" nil )"borel[real, metric_induced_topology]" nil )"bool" sets nil )"measurable_function[T, S]" probability_space nil )"[T, T -> boolean]" equalities nil )"T3" function_props nil ))nil 3391354647"" (subtype-tcc) nil nil ) nil nil ))nil 3352017383"" (induct "n1" )"1" (expand "sigma" )"1" (skosimp)"1" (typepred "XS!1(0)" )"1" (expand "random_variable?" )"1" (expand "sigma" )"1" (case-replace "(LAMBDA t: XS!1(0)(t))=XS!1(0)" )"1" (apply-extensionality :hide? t) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (inst - "XS!1" )"2" (expand "sigma" 1)"2" (typepred "XS!1(1 + j!1)" )"2" (expand "random_variable?" )"2" "sum_measurable" "g1" "XS!1(1 + j!1)" "g2" "LAMBDA t: LAMBDA n: XS!1(n)(t))")) "1" (expand "+" ) (("1" (propax) nil nil )) nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"[T -> real]" real_fun_ops "reals/" )"(total_order?[real])" nil )nil measure_space_def"measure_integration/" )nil measure_space_def"measure_integration/" )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"posint" nil )NOT const-decl "[bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"real" reals nil )nil naturalnumbers nil )"real" sigma "reals/" )nil sigma "reals/" )nil sigma "reals/" )"bool" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" probability_measure nil )nil probability_measure nil )"bool" measure_space_def"measure_integration/" )"sigma_algebra" probability_space nil )nil subset_algebra_def"measure_integration/" )"bool" subset_algebra_def"measure_integration/" )nil sets nil )nil defined_types nil )nil probability_space nil )nil defined_types nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil 3321775180"" (expand "distribution_function?" )"" (inst + "lambda (t:T): 0" )"1" (skosimp)"1" (expand "<=" )"1" (case-replace "0 <= x!1" )"1" (lemma "P_fullset" ("P" "P" ))"1" (expand "fullset" ) (("1" (assert ) nil nil )) nil ))nil )"2" (lemma "P_emptyset" ("P" "P" ))"2" (expand "emptyset" ) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (lemma "constant_is_measurable" )"2" (inst - "LAMBDA (t: T): 0" )"2" (expand "constant?" )"2" (expand "const_fun" ) (("2" (inst?) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"bool" measure_space_def"measure_integration/" )"sigma_algebra" probability_space nil )nil subset_algebra_def"measure_integration/" )"bool" subset_algebra_def"measure_integration/" )nil sets nil )nil defined_types nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil probability_space nil )nil probability_measure nil )"(S)" probability_space nil )nil probability_measure nil )"set" sets nil )"probability_measure" probability_space nil )nil probability_measurenil )"bool" probability_measure nil )nil probability_measure nil )nil real_types nil )"bool" reals nil )nil probability_measure nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"set" sets nil )"bool" reals nil )"bool" const_fun_def "structures/" )"[S -> T]" const_fun_def "structures/" )nil measure_space_def"measure_integration/" )"bool" probability_space nil ))nil 3352018678"" (skosimp)"" (expand "<" )"" (expand "distribution_function" )"" (expand "<=" )"" (lemma "P_complement" ("A" "{t | X!1(t) > x!1}" ))"1" (inst - "P" )"1" (expand ">" )"1" (lemma "complement_lt1" ("x" "x!1" "X" "X!1" ))"1" (expand "<" -1)"1" (expand ">" -1)"1" (replace -1 -2)"1" (expand "<=" -2) (("1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (typepred "x!1<X!1" )"2" (expand "<" ) (("2" (propax) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"(S)" probability_space nil )"(S)" probability_space nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil probability_measure nil )"bool" probability_measure nil )nil probability_measurenil )"probability_measure" probability_space nil )nil probability_space nil )"real" reals nil )nil probability_measure nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"bool" measure_space_def"measure_integration/" )nil probability_measure nil )nil probability_space nil )nil booleans nil )nil booleans nil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def"measure_integration/" )nil subset_algebra_def"measure_integration/" )"sigma_algebra" probability_space nil )"probability" probability_spacenil ))nil 3352019023"" (skosimp*)"" (assert )"" (expand "distribution_function" )"" (skosimp)"" "P_intersection" ("A" "x!1 < X!1" "B" "X!1 <= y!1" ))"" (inst - "P" )"" (replace -1 1)"" (hide -1)"" (assert )"" "union(x!1 < X!1, X!1 <= y!1) = fullset[T]" )"1" (hide -1)"1" (lemma "P_fullset" )"1" (inst - "P" )"1" (replace -1)"1" "P_complement" "A" "x!1 < X!1" ))"1" "P" )"1" rewrite "complement_lt1" -1)"1" replace -1)"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (apply-extensionality 1 :hide? t)"2" (expand "fullset" )"2" (expand "union" )"2" expand "member" )"2" expand "<" )"2" expand "<=" 1)"2" expand ">" 1)"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" reals nil )"(S)" nil )"(total_order?[real])" nil )"probability_measure" probability_space nil )nil probability_measurenil )"bool" probability_measure nil )nil probability_measure nil )"bool" reals nil )nil real_types nil )"bool" reals nil )"set" sets nil )"set" sets nil )"[T, T -> boolean]" equalities nil )set type-eq-decl nil sets nil )nil probability_measure nil )"(S)" probability_space nil )"measurable_set[T, S]" nil )"real" reals nil )nil probability_space nil )nil probability_measure nil )"bool" reals nil )"(strict_total_order?[real])" real_props nil )"bool" sets nil )"nnreal" nil )"(S)" probability_spacenil )nil probability_measure nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" measure_space_def"measure_integration/" )nil probability_measure nil )"(S)" probability_space nil )"(S)" probability_space nil )nil probability_space nil )nil booleans nil )nil booleans nil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def"measure_integration/" )nil subset_algebra_def"measure_integration/" )"sigma_algebra" probability_space nil )"probability" probability_spacenil ))nil 3425001876"" (skosimp)"" (expand "distribution_function" )"" (replace -1)"" (assert )"" (hide -1)"" (lemma "m_increasing_convergence" )"" (inst - "lambda (n:nat): X!1 <= x!1 - 1 / (1 + n)" )"1" (split -1)"1" (expand "x_converges?" )"1" (expand "to_measure" )"1" (expand "o" ) (("1" (propax) nil nil )) nil ))nil ))nil )"2" (hide 2)"2" (expand "increasing?" )"2" (skosimp)"2" (expand "subset?" )"2" (expand "<=" 1)"2" (expand "member" )"2" "2" "both_sides_div_pos_le2" "py" "x!2+1" "px" "y!1+1" "pz" "1" ))"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp)"2" (expand "measurable_set?" )"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"probability" probability_spacenil )"posrat" nil )"posint" nil )"real" reals nil )"probability_measure" probability_space nil )nil probability_measurenil )"bool" probability_measure nil )nil probability_measure nil )"bool" reals nil )"measure_type" generalized_measure_def"measure_integration/" )nil generalized_measure_def"measure_integration/" )"bool" generalized_measure_def"measure_integration/" )nil extended_nnreal"extended_nnreal/" )nil generalized_measure_def"measure_integration/" )"bool" generalized_measure_def"measure_integration/" )nil real_types nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )"sigma_algebra" probability_space nil )nil subset_algebra_def"measure_integration/" )"bool" subset_algebra_def"measure_integration/" )nil sets nil )nil defined_types nil )nil booleans nil )nil booleans nil )nil probability_space nil )nil measure_props"measure_integration/" )"T3" function_props nil )"bool" extended_nnreal "extended_nnreal/" )"bool" fun_preds_partial "structures/" )"bool" sets nil )"bool" sets nil )"posint" nil )nil real_props nil )nil real_types nil )"bool" reals nil )nil real_types nil )"(total_order?[real])" nil )nil sequences nil )nil measure_space_def"measure_integration/" )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )set type-eq-decl nil sets nil )"bool" measure_space_def"measure_integration/" )"bool" measure_space_def"measure_integration/" )nil probability_measure nil )"(S)" probability_space nil )"random_variable[T, S]" probability_spacenil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"real" probability_space nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fieldsnil ))nil ))nil 3425001894"" (skosimp*)"" (assert )"" (expand "distribution_function" )"" (case-replace "P(X!1 <= x!1)=P(X!1 = x!1)+P(X!1 < x!1)" )"1" (hide -1)"1" (assert )"1" (lemma "P_IUnion" )"1" "P" "LAMBDA (n:nat): X!1 <= x!1 - 1 / (1 + n)" )"1" (split -1)"1" "IUnion(LAMBDA (n: nat): X!1 <= x!1 - 1 / (1 + n))=X!1<x!1" )"1" (hide -1)"1" (expand "o" -1)"1" rewrite "convergence_sequences.limit_def" "1" (expand "convergent?" )"1" (inst + "P(X!1<x!1)" ) nil nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (apply-extensionality :hide? t)"2" (expand "<" 1)"2" (expand "IUnion" )"2" "X!1(x!2) < x!1" )"1" expand "<=" +)"1" "archimedean" "px" "x!1-X!1(x!2)" ))"1" "1" "n!1-1" )"1" (assert ) nil nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" assert )"2" "2" expand "<=" -1)"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (expand "increasing?" )"2" (skolem + ("i!1" "j!1" ))"2" (flatten)"2" (expand "subset?" )"2" expand "member" )"2" "2" expand "<=" (-2 1))"2" assert )"2" "both_sides_div_pos_le2" )"2" "1+j!1" "1+i!1" "1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" "P_disjointunion" "A" "X!1 = x!1" "B" "X!1 < x!1" "P" "P" ))"2" "union(X!1 = x!1, X!1 < x!1)=X!1 <= x!1" )"1" (split)"1" (propax) nil nil )"2" (hide-all-but 1)"2" (expand "=" )"2" (expand "<" )"2" (expand "disjoint?" )"2" (expand "intersection" )"2" (expand "empty?" )"2" expand "member" )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (expand "<=" )"2" (expand "<" )"2" (expand "=" )"2" (expand "union" )"2" (expand "member" )"2" (apply-extensionality :hide? t)"2" expand "<=" )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" reals nil )"posrat" nil )"posint" nil )"nnreal" nil )nil numbers nil )nil booleans nil )"[T, T -> boolean]" equalities nil )nil probability_space nil )nil booleans nil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def"measure_integration/" )nil subset_algebra_def"measure_integration/" )"sigma_algebra" probability_space nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil probability_measure nil )"bool" probability_measure nil )nil probability_measurenil )"probability_measure" probability_space nil )"bool" measure_space_def"measure_integration/" )nil probability_measure nil )"(S)" probability_space nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"(S)" probability_space nil )"(S)" probability_space nil )"odd_int" integers nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )nil sequences nil )"[numfield, numfield -> numfield]" number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"bool" sets nil )nil real_props nil )"bool" sets nil )"bool" fun_preds_partial "structures/" )"set[T]" indexed_sets nil )set type-eq-decl nil sets nil )"(S)" nil )"T3" function_props nil )nil convergence_sequences "analysis/" )"bool" convergence_sequences "analysis/" )"int" integers nil )"nzrat" rationalsnil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil integers nil )nil integers nil )"int" integers nil )AND const-decl "[bool, bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil real_props nil )"bool" reals nil )nil probability_measure nil )nil probability_measure nil )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" sets nil )"bool" sets nil )"set" sets nil )"(S)" probability_spacenil )"set" sets nil )"probability" probability_spacenil ))nil 3314699486"" (skosimp)"" (typepred "F!1" )"" (expand "distribution_function?" )"" (skosimp)"" (expand "<=" )"" (name "BB" "lambda (n:nat): {t:T | X!1(t) <= -n}" )"" (lemma "P_IIntersection" ("X" "BB" "P" "P" ))"1" (split -1)"1" "IIntersection(BB) = emptyset[T]" )"1" (rewrite "P_emptyset" )"1" (expand "o" )"1" (expand "BB" )"1" "extensionality" "f" "F!1" "g" "lambda x: P({t | X!1(t) <= x})" ))"1" (split -1)"1" replace -1)"1" (assert ) nil nil ))nil )"2" "2" (inst - "x!1" ) nil nil ))nil ))nil )"2" (skosimp)"2" "X!1" )"2" "x!1" )"2" rewrite "measurable_le" -1)"2" (inst - "x!1" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -1 2 -2)"2" (expand "IIntersection" )"2" (expand "BB" )"2" (apply-extensionality 1 :hide? t)"2" (expand "emptyset" )"2" "2" "X!1(x!1)<= -1" )"1" "II" "floor(X!1(x!1))" )"1" "floor(X!1(x!1))" )"1" replace -3)"1" expand "<=" -1)"1" "1" "-II" )"1" (assert ) nil nil )"2" (assert ) nil nil ))nil )"2" "1-II" )"1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (inst - "1" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -1 2)"2" (expand "BB" )"2" (expand "decreasing?" )"2" (skosimp*)"2" (expand "subset?" )"2" (expand "member" )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp)"2" (expand "BB" )"2" (typepred "X!1" )"2" (inst - "-x1!1" )"2" (rewrite "measurable_le" -1)"2" (inst - "-x1!1" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil probability_spacenil )"bool" probability_space nil )nil probability_measure nil )"sigma_algebra" probability_space nil )nil subset_algebra_def"measure_integration/" )"bool" subset_algebra_def"measure_integration/" )nil sets nil )nil defined_types nil )nil probability_space nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )nil probability_measure nil )"bool" measure_space_def"measure_integration/" )"[T, T -> boolean]" equalities nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"int" integers nil )"odd_int" integers nil )"int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )"(total_order?[real])" nil )"random_variable[T, S]" probability_spacenil )"T" probability_space nil )"{i | i <= X!1(x!1) & X!1(x!1) < 1 + i}" nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"(total_order?[real])" nil )"{i | i <= x & x < i + 1}" floor_ceil nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )nil probability_measure nil )"[nat -> [T -> bool]]" probability_space nil )nil measure_space_def"measure_integration/" )nil functions nil )"T3" function_props nil )"finite_set" finite_sets nil )"finite_set[T]" countable_props"sets_aux/" )"finite_set[T]" countable_setofsets"sets_aux/" )"(S)" probability_spacenil )"measurable_set[T, S]" nil )set type-eq-decl nil sets nil )"set[T]" indexed_sets nil )"set" sets nil )"bool" sets nil )"bool" sets nil )"bool" fun_preds_partial "structures/" )nil sequences nil )"probability_measure" probability_space nil )nil probability_measurenil )"bool" probability_measure nil )nil probability_measure nil )"(S)" probability_space nil ))nil 3314699095"" (skosimp)"" (typepred "F!1" )"" (expand "distribution_function?" )"" (skosimp)"" (name "BB" "lambda (n:nat): {t:T | X!1(t) <= n}" )"" (lemma "P_IUnion" ("X" "BB" "P" "P" ))"1" (case-replace "IUnion(BB)= fullset[T]" )"1" (rewrite "P_fullset" )"1" (expand "o" )"1" (expand "BB" )"1" (expand "restrict" )"1" (split -2)"1" "extensionality" "f" "lambda (s:nat): F!1(s)" "g" "LAMBDA (x: nat): P({t: T | X!1(t) <= x})" ))"1" (split -1)"1" replace -1 1)"1" (propax) nil nil ))nil )"2" "2" "x!1" )"2" expand "<=" -4)"2" (propax) nil nil ))nil ))nil ))nil ))nil )"2" (skosimp)"2" "X!1" )"2" "x!1" )"2" rewrite "measurable_le" -1)"2" (inst - "x!1" ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -1 2 -2)"2" (expand "increasing?" )"2" expand "subset?" )"2" expand "member" )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (expand "BB" )"2" (expand "IUnion" )"2" (expand "fullset" )"2" (assert )"2" (apply-extensionality :hide? t)"2" (case-replace "X!1(x!1)<=0" )"1" (inst + "0" ) nil nil )"2" "ceiling(X!1(x!1))" )"1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "BB" )"2" (skosimp*)"2" (typepred "X!1" )"2" (inst - "x1!1" )"2" (rewrite "measurable_le" -1)"2" (inst - "x1!1" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil probability_spacenil )"bool" probability_space nil )nil probability_measure nil )"sigma_algebra" probability_space nil )nil subset_algebra_def"measure_integration/" )"bool" subset_algebra_def"measure_integration/" )nil sets nil )nil defined_types nil )nil probability_space nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil probability_measure nil )"bool" probability_measure nil )nil probability_measurenil )"probability_measure" probability_space nil )nil sequences nil )"T" probability_space nil )"random_variable[T, S]" probability_spacenil )"{i | x <= i & i < x + 1}" floor_ceil nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )"(total_order?[real])" nil )"bool" booleans nil )nil probability_measure nil )"[nat -> [T -> bool]]" probability_space nil )nil measure_space_def"measure_integration/" )"(S)" probability_space nil )nil functions nil )"bool" fun_preds_partial "structures/" )"bool" sets nil )"(total_order?[real])" nil )"bool" sets nil )"R" restrict nil )"T3" function_props nil )"(S)" probability_space nil )"measurable_set[T, S]" nil )set type-eq-decl nil sets nil )"set[T]" indexed_sets nil )"set" sets nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )"bool" measure_space_def"measure_integration/" )nil probability_measurenil ))nil 3314700007"" (skosimp)"" (typepred "F!1" )"" (expand "distribution_function?" )"" (expand "increasing?" )"" (skosimp*)"" "P_subset_le" "A" "X!1 <= x!1" "B" "X!1 <= y!1" "P" "P" ))"" (expand "subset?" )"" (expand "member" )"" (inst-cp - "x!1" )"" (inst - "y!1" )"" (split -1)"1" (assert )"1" (expand "restrict" )"1" (assert ) nil nil )) nil ))nil )"2" (expand "<=" 1)"2" (skosimp) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil probability_spacenil )"bool" probability_space nil )nil probability_measure nil )"sigma_algebra" probability_space nil )nil subset_algebra_def"measure_integration/" )"bool" subset_algebra_def"measure_integration/" )nil sets nil )nil defined_types nil )nil probability_space nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" real_fun_preds "reals/" )"probability_measure" probability_space nil )nil probability_measurenil )"bool" probability_measure nil )"(S)" probability_space nil )nil probability_measure nil )"bool" measure_space_def"measure_integration/" )nil probability_measure nil )"bool" sets nil )"(total_order?[real])" nil )"bool" sets nil ))nil 3352018084"" (skosimp)"" (expand "right_continuous?" )"" (skolem + ("x!1" ))"" (expand "right_continuous?" )"" (skosimp)"" (typepred "F!1" )"" (expand "distribution_function?" )"" (skosimp)"" (typepred "X!1" )"" case "EXISTS (delta:posreal): AND y - x!1 < delta IMPLIES") "1" (skosimp)"1" (inst + "delta!1" )"1" (skosimp)"1" (inst - "x!2" )"1" "x!2" )"1" "x!1" )"1" "distribution_increasing" "F" "F!1" ))"1" expand "increasing?" )"1" "x!1" "x!2" )"1" expand "abs" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" "m_decreasing_convergence" "E" "lambda (n:nat): X!1<=x!1+1/(1+n)" ))"1" (split -1)"1" (expand "to_measure" )"1" expand "o" -1)"1" expand "x_converges?" )"1" "1" "IIntersection(LAMBDA (n: nat): X!1 <= 1 / (1 + n) + x!1) = X!1<=x!1" )"1" "1" "convergence_sequences.limit_def" )"1" "P(X!1<=x!1)" "LAMBDA (i:nat): P(X!1 <= 1 / (1 + i) + x!1)" )"1" assert )"1" "1" expand "convergence" )"1" "epsilon!1" )"1" "1" "1/(1+n!1)" )"1" "1" "distribution_increasing" "F" "F!1" ))"1" "n!1" )"1" assert )"1" expand "increasing?" )"1" "y!1" "x!1+1/(1+n!1)" )"1" "x!1" "x!1+1/(1+n!1)" )"1" assert )"1" "x!1" )"1" "x!1+1/(1+n!1)" )"1" "y!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "<=" )"2" expand "IIntersection" )"2" "X!1(x!2) <= x!1" )"1" "1" assert )nil nil ))nil )"2" assert )"2" "archimedean" "px" "X!1(x!2)-x!1" ))"2" "2" "n!1-1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" expand "decreasing?" )"2" "i!1" "j!1" ))"2" "2" expand "subset?" )"2" expand "member" )"2" expand "<=" 1)"2" "t!1" ))"2" "2" "both_sides_div_pos_le2" "py" "i!1+1" "px" "j!1+1" "pz" "1" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide 2)"3" expand "mu_fin?" )"3" expand "to_measure" )"3" (propax) nil nil ))nil ))nil ))nil ))nil )"2" (skosimp)"2" (expand "measurable_set?" )"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" continuous_functions_aux nil )"real" reals nil )"bool" continuous_functions_aux nil )nil probability_spacenil )"bool" probability_space nil )nil probability_measure nil )"sigma_algebra" probability_space nil )nil subset_algebra_def"measure_integration/" )"bool" subset_algebra_def"measure_integration/" )nil sets nil )nil defined_types nil )nil probability_space nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"(S)" probability_space nil )"probability_measure" probability_space nil )nil probability_measurenil )"bool" probability_measure nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" real_fun_preds "reals/" )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil probability_space nil )"measure_type" generalized_measure_def"measure_integration/" )nil generalized_measure_def"measure_integration/" )"bool" generalized_measure_def"measure_integration/" )nil extended_nnreal"extended_nnreal/" )nil generalized_measure_def"measure_integration/" )"bool" generalized_measure_def"measure_integration/" )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )"[numfield, numfield -> numfield]" number_fields nil )nil sequences nil )nil measure_space_def"measure_integration/" )"bool" measure_space_def"measure_integration/" )set type-eq-decl nil sets nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil measure_props"measure_integration/" )"real" reals nil )"posint" nil )"posrat" nil )"bool" measure_props "measure_integration/" )"bool" sets nil )nil real_props nil )"posint" nil )"bool" sets nil )"bool" fun_preds_partial "structures/" )"bool" extended_nnreal "extended_nnreal/" )"set[T]" indexed_sets nil )"[T, T -> boolean]" equalities nil )"(S)" nil )nil convergence_sequences "analysis/" )"bool" convergence_sequences "analysis/" )"(total_order?[real])" nil )"real" probability_space nil )"random_variable[T, S]" probability_spacenil )"bool" convergence_sequences "analysis/" )"int" integers nil )"nzrat" rationalsnil )nil integers nil )nil integers nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )nil real_props nil )"T3" function_props nil )nil probability_measure nil )"bool" measure_space_def"measure_integration/" ))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ 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.0.79Bemerkung:
(Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können 2026-04-29)
¤ *Bot Zugriff
2026-05-26
