| products/sources/formale sprachen/PVS/vect_analysis/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: Sprache: XMLOriginal von: PVS© |
|
||||||
|
(expectation
(E_zero_TCC1 0 (E_zero_TCC1-1 nil 3424623896 ("" (lemma "integrable_zero") (("" (expand "const_fun") (("" (expand "zero") (("" (propax) nil nil)) nil)) nil)) nil) ((zero const-decl "random_variable" probability_space nil) (integrable_zero formula-decl nil integral "measure_integration/") (T formal-nonempty-type-decl nil expectation nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets nil) (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration/") (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration/") (S formal-const-decl "sigma_algebra" expectation nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (finite_measure? const-decl "bool" generalized_measure_def "measure_integration/") (finite_measure nonempty-type-eq-decl nil generalized_measure_def "measure_integration/") (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (measure? const-decl "bool" generalized_measure_def "measure_integration/") (measure_type nonempty-type-eq-decl nil generalized_measure_def "measure_integration/") (to_measure const-decl "measure_type" generalized_measure_def "measure_integration/") (<= const-decl "bool" reals nil) (probability nonempty-type-eq-decl nil probability_measure nil) (probability_measure? const-decl "bool" probability_measure nil) (probability_measure nonempty-type-eq-decl nil probability_measure nil) (P formal-const-decl "probability_measure" expectation nil)) nil)) (E_zero 0 (E_zero-1 nil 3424623896 ("" (expand "E") (("" (expand "zero") (("" (lemma "integral_zero") (("" (expand "const_fun") (("" (propax) nil nil)) nil)) nil)) nil)) nil) ((zero const-decl "random_variable" probability_space nil) (integral_zero formula-decl nil integral "measure_integration/") (T formal-nonempty-type-decl nil expectation nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets nil) (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration/") (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration/") (S formal-const-decl "sigma_algebra" expectation nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (finite_measure? const-decl "bool" generalized_measure_def "measure_integration/") (finite_measure nonempty-type-eq-decl nil generalized_measure_def "measure_integration/") (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (measure? const-decl "bool" generalized_measure_def "measure_integration/") (measure_type nonempty-type-eq-decl nil generalized_measure_def "measure_integration/") (to_measure const-decl "measure_type" generalized_measure_def "measure_integration/") (<= const-decl "bool" reals nil) (probability nonempty-type-eq-decl nil probability_measure nil) (probability_measure? const-decl "bool" probability_measure nil) (probability_measure nonempty-type-eq-decl nil probability_measure nil) (P formal-const-decl "probability_measure" expectation nil) (E const-decl "real" expectation nil)) shostak)) (E_one_TCC1 0 (E_one_TCC1-1 nil 3424688983 ("" (rewrite "isf_is_integrable") (("" (hide 2) (("" (expand "isf?") (("" (split) (("1" (expand "simple?") (("1" (expand "one") (("1" (expand "fullset") (("1" (expand "image") (("1" (case-replace "{y: real | EXISTS (x_1: ({x: T | TRUE})): y = 1}=singleton[real](1)") (("1" (hide -1) (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (apply-extensionality :hide? t) (("2" (expand "singleton") (("2" (case-replace "x!1=1") (("1" (inst + "choose[T](fullset[T])") (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (expand "fullset") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "one") (("2" (expand "nonzero_set?") (("2" (expand "mu_fin?") (("2" (expand "to_measure") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((image const-decl "set[R]" function_image nil) (measurable_fullset name-judgement "measurable_set[T, S]" expectation nil) (subset_algebra_fullset name-judgement "(S)" expectation nil) (choose const-decl "(p)" sets nil) (nonempty? const-decl "bool" sets nil) (empty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set[real]" measure_space "measure_integration/") (nonempty_singleton_finite application-judgement "non_empty_finite_set[posreal]" metric_continuity "metric_space/") (singleton_is_closed application-judgement "closed[real, (metric_induced_topology)]" convergence_aux "metric_space/") (singleton_is_compact application-judgement "compact[real, (metric_induced_topology)]" convergence_aux "metric_space/") (nonempty_singleton_finite application-judgement "non_empty_finite_set[nat]" countability "sets_aux/") (= const-decl "[T, T -> boolean]" equalities nil) (TRUE const-decl "bool" booleans nil) (set type-eq-decl nil sets nil) (singleton? const-decl "bool" sets nil) (singleton const-decl "(singleton?)" sets nil) (fullset const-decl "set" sets nil) (simple? const-decl "bool" measure_space "measure_integration/") (nonzero_set? const-decl "set[T]" isf "measure_integration/") (mu_fin? const-decl "bool" measure_props "measure_integration/") (P formal-const-decl "probability_measure" expectation nil) (probability_measure nonempty-type-eq-decl nil probability_measure nil) (probability_measure? const-decl "bool" probability_measure nil) (probability nonempty-type-eq-decl nil probability_measure nil) (<= const-decl "bool" reals nil) (to_measure const-decl "measure_type" generalized_measure_def "measure_integration/") (measure_type nonempty-type-eq-decl nil generalized_measure_def "measure_integration/") (measure? const-decl "bool" generalized_measure_def "measure_integration/") (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (finite_measure nonempty-type-eq-decl nil generalized_measure_def "measure_integration/") (finite_measure? const-decl "bool" generalized_measure_def "measure_integration/") (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (S formal-const-decl "sigma_algebra" expectation nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration/") (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration/") (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-nonempty-type-decl nil expectation nil) (one const-decl "random_variable" probability_space nil) (random_variable nonempty-type-eq-decl nil probability_measure nil) (measurable_function? const-decl "bool" measure_space_def "measure_integration/") (isf nonempty-type-eq-decl nil isf "measure_integration/") (isf? const-decl "bool" isf "measure_integration/") (isf_is_integrable judgement-tcc nil integral "measure_integration/")) nil)) (E_one 0 (E_one-1 nil 3424689250 ("" (expand "one") (("" (expand "E") (("" (lemma "integral_phi" ("F" "fullset[T]")) (("1" (expand "mu") (("1" (expand "to_measure") (("1" (typepred "P") (("1" (expand "probability_measure?") (("1" (flatten) (("1" (expand "probability_measure_full?") (("1" (replace -1) (("1" (case-replace "phi(fullset[T])=(LAMBDA (t: T): 1)") (("1" (hide-all-but 1) (("1" (apply-extensionality :hide? t) (("1" (expand "fullset") (("1" (expand "phi") (("1" (expand "member") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "mu_fin?") (("2" (expand "to_measure") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ((E const-decl "real" expectation nil) (mu const-decl "nnreal" measure_props "measure_integration/") (NOT const-decl "[bool -> bool]" booleans nil) (member const-decl "bool" sets nil) (phi_is_simple application-judgement "simple[T, S]" expectation nil) (= const-decl "[T, T -> boolean]" equalities nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (phi const-decl "nat" measure_space "measure_integration/") (probability_measure_full? const-decl "bool" probability_measure nil) (subset_algebra_fullset name-judgement "(S)" expectation nil) (measurable_fullset name-judgement "measurable_set[T, S]" expectation nil) (integral_phi formula-decl nil integral "measure_integration/") (set type-eq-decl nil sets nil) (measurable_set? const-decl "bool" measure_space_def "measure_integration/") (measurable_set nonempty-type-eq-decl nil measure_space_def "measure_integration/") (mu_fin? const-decl "bool" measure_props "measure_integration/") (fullset const-decl "set" sets nil) (T formal-nonempty-type-decl nil expectation nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets nil) (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration/") (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration/") (S formal-const-decl "sigma_algebra" expectation nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (finite_measure? const-decl "bool" generalized_measure_def "measure_integration/") (finite_measure nonempty-type-eq-decl nil generalized_measure_def "measure_integration/") (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (measure? const-decl "bool" generalized_measure_def "measure_integration/") (measure_type nonempty-type-eq-decl nil generalized_measure_def "measure_integration/") (to_measure const-decl "measure_type" generalized_measure_def "measure_integration/") (<= const-decl "bool" reals nil) (probability nonempty-type-eq-decl nil probability_measure nil) (probability_measure? const-decl "bool" probability_measure nil) (probability_measure nonempty-type-eq-decl nil probability_measure nil) (P formal-const-decl "probability_measure" expectation nil) (one const-decl "random_variable" probability_space nil)) shostak)) (E_phi_TCC1 0 (E_phi_TCC1-1 nil 3424592613 ("" (skosimp) (("" (lemma "isf_phi" ("E" "A!1")) (("1" (rewrite "isf_is_integrable") nil nil) ("2" (hide 2) (("2" (typepred "A!1") (("2" (expand "measurable_set?") (("2" (expand "mu_fin?") (("2" (expand "to_measure") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((P formal-const-decl "probability_measure" expectation nil) (probability_measure nonempty-type-eq-decl nil probability_measure nil) (probability_measure? const-decl "bool" probability_measure nil) (probability nonempty-type-eq-decl nil probability_measure nil) (<= const-decl "bool" reals nil) (to_measure const-decl "measure_type" generalized_measure_def "measure_integration/") (measure_type nonempty-type-eq-decl nil generalized_measure_def "measure_integration/") (measure? const-decl "bool" generalized_measure_def "measure_integration/") (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (finite_measure nonempty-type-eq-decl nil generalized_measure_def "measure_integration/") (finite_measure? const-decl "bool" generalized_measure_def "measure_integration/") (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (S formal-const-decl "sigma_algebra" expectation nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration/") (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration/") (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-nonempty-type-decl nil expectation nil) (mu_fin? const-decl "bool" measure_props "measure_integration/") (measurable_set nonempty-type-eq-decl nil measure_space_def "measure_integration/") (measurable_set? const-decl "bool" measure_space_def "measure_integration/") (set type-eq-decl nil sets nil) (isf_phi judgement-tcc nil isf "measure_integration/") (AND const-decl "[bool, bool -> bool]" booleans nil) (phi const-decl "nat" measure_space "measure_integration/") (nat nonempty-type-eq-decl nil naturalnumbers nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (isf nonempty-type-eq-decl nil isf "measure_integration/") (isf? const-decl "bool" isf "measure_integration/") (isf_is_integrable judgement-tcc nil integral "measure_integration/") (phi_is_simple application-judgement "simple[T, S]" expectation nil) (NOT const-decl "[bool -> bool]" booleans nil)) nil)) (E_phi 0 (E_phi-1 nil 3424621209 ("" (skosimp) (("" (expand "E") (("" (lemma "E_phi_TCC1" ("A" "A!1")) (("" (rewrite "integral_phi") (("1" (expand "mu") (("1" (expand "to_measure") (("1" (propax) nil nil)) nil)) nil) ("2" (expand "measurable_set?") (("2" (expand "mu_fin?") (("2" (expand "to_measure") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((E const-decl "real" expectation nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (integral_phi formula-decl nil integral "measure_integration/") (set type-eq-decl nil sets nil) (measurable_set? const-decl "bool" measure_space_def "measure_integration/") (measurable_set nonempty-type-eq-decl nil measure_space_def "measure_integration/") (mu_fin? const-decl "bool" measure_props "measure_integration/") (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (finite_measure? const-decl "bool" generalized_measure_def "measure_integration/") (finite_measure nonempty-type-eq-decl nil generalized_measure_def "measure_integration/") (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (measure? const-decl "bool" generalized_measure_def "measure_integration/") (measure_type nonempty-type-eq-decl nil generalized_measure_def "measure_integration/") (to_measure const-decl "measure_type" generalized_measure_def "measure_integration/") (<= const-decl "bool" reals nil) (probability nonempty-type-eq-decl nil probability_measure nil) (probability_measure? const-decl "bool" probability_measure nil) (probability_measure nonempty-type-eq-decl nil probability_measure nil) (P formal-const-decl "probability_measure" expectation nil) (phi_is_simple application-judgement "simple[T, S]" expectation nil) (mu const-decl "nnreal" measure_props "measure_integration/") (E_phi_TCC1 subtype-tcc nil expectation nil) (T formal-nonempty-type-decl nil expectation nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets nil) (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration/") (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration/") (S formal-const-decl "sigma_algebra" expectation nil)) shostak)) (E_add 0 (E_add-1 nil 3424591769 ("" (skosimp) (("" (expand "E") (("" (rewrite "integral_add") nil nil)) nil)) nil) ((E const-decl "real" expectation nil) (P formal-const-decl "probability_measure" expectation nil) (probability_measure nonempty-type-eq-decl nil probability_measure nil) (probability_measure? const-decl "bool" probability_measure nil) (probability nonempty-type-eq-decl nil probability_measure nil) (<= const-decl "bool" reals nil) (to_measure const-decl "measure_type" generalized_measure_def "measure_integration/") (measure_type nonempty-type-eq-decl nil generalized_measure_def "measure_integration/") (measure? const-decl "bool" generalized_measure_def "measure_integration/") (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (finite_measure nonempty-type-eq-decl nil generalized_measure_def "measure_integration/") (finite_measure? const-decl "bool" generalized_measure_def "measure_integration/") (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (S formal-const-decl "sigma_algebra" expectation nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration/") (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration/") (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-nonempty-type-decl nil expectation nil) (integrable nonempty-type-eq-decl nil integral "measure_integration/") (integrable? const-decl "bool" integral "measure_integration/") (integral_add formula-decl nil integral "measure_integration/")) shostak)) (E_scal 0 (E_scal-1 nil 3424622429 ("" (skosimp) (("" (expand "E") (("" (lemma "integral_scal" ("c" "c!1" "f" "X!1")) (("" (expand "*") (("" (propax) nil nil)) nil)) nil)) nil)) nil) ((E const-decl "real" expectation nil) (integral_scal formula-decl nil integral "measure_integration/") (integrable? const-decl "bool" integral "measure_integration/") (integrable nonempty-type-eq-decl nil integral "measure_integration/") (T formal-nonempty-type-decl nil expectation nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets nil) (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration/") (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration/") (S formal-const-decl "sigma_algebra" expectation nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (finite_measure? const-decl "bool" generalized_measure_def "measure_integration/") (finite_measure nonempty-type-eq-decl nil generalized_measure_def "measure_integration/") (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (measure? const-decl "bool" generalized_measure_def "measure_integration/") (measure_type nonempty-type-eq-decl nil generalized_measure_def "measure_integration/") (to_measure const-decl "measure_type" generalized_measure_def "measure_integration/") (<= const-decl "bool" reals nil) (probability nonempty-type-eq-decl nil probability_measure nil) (probability_measure? const-decl "bool" probability_measure nil) (probability_measure nonempty-type-eq-decl nil probability_measure nil) (P formal-const-decl "probability_measure" expectation nil)) shostak)) (E_opp 0 (E_opp-1 nil 3424622550 ("" (skosimp) (("" (expand "E") (("" (rewrite "integral_opp") nil nil)) nil)) nil) ((E const-decl "real" expectation nil) (P formal-const-decl "probability_measure" expectation nil) (probability_measure nonempty-type-eq-decl nil probability_measure nil) (probability_measure? const-decl "bool" probability_measure nil) (probability nonempty-type-eq-decl nil probability_measure nil) (<= const-decl "bool" reals nil) (to_measure const-decl "measure_type" generalized_measure_def "measure_integration/") (measure_type nonempty-type-eq-decl nil generalized_measure_def "measure_integration/") (measure? const-decl "bool" generalized_measure_def "measure_integration/") (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (finite_measure nonempty-type-eq-decl nil generalized_measure_def "measure_integration/") (finite_measure? const-decl "bool" generalized_measure_def "measure_integration/") (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (S formal-const-decl "sigma_algebra" expectation nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration/") (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration/") (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-nonempty-type-decl nil expectation nil) (integrable nonempty-type-eq-decl nil integral "measure_integration/") (integrable? const-decl "bool" integral "measure_integration/") (integral_opp formula-decl nil integral "measure_integration/")) shostak)) (E_diff 0 (E_diff-1 nil 3424622569 ("" (skosimp) (("" (expand "E") (("" (rewrite "integral_diff") nil nil)) nil)) nil) ((E const-decl "real" expectation nil) (P formal-const-decl "probability_measure" expectation nil) (probability_measure nonempty-type-eq-decl nil probability_measure nil) (probability_measure? const-decl "bool" probability_measure nil) (probability nonempty-type-eq-decl nil probability_measure nil) (<= const-decl "bool" reals nil) (to_measure const-decl "measure_type" generalized_measure_def "measure_integration/") (measure_type nonempty-type-eq-decl nil generalized_measure_def "measure_integration/") (measure? const-decl "bool" generalized_measure_def "measure_integration/") (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (finite_measure nonempty-type-eq-decl nil generalized_measure_def "measure_integration/") (finite_measure? const-decl "bool" generalized_measure_def "measure_integration/") (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (S formal-const-decl "sigma_algebra" expectation nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration/") (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration/") (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-nonempty-type-decl nil expectation nil) (integrable nonempty-type-eq-decl nil integral "measure_integration/") (integrable? const-decl "bool" integral "measure_integration/") (integral_diff formula-decl nil integral "measure_integration/")) shostak)) (E_nonneg 0 (E_nonneg-1 nil 3424622396 ("" (skosimp) (("" (expand "E") (("" (lemma "integral_nonneg" ("f" "X!1")) (("" (split) (("1" (propax) nil nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil) ((E const-decl "real" expectation nil) (integral_nonneg formula-decl nil integral "measure_integration/") (integrable? const-decl "bool" integral "measure_integration/") (integrable nonempty-type-eq-decl nil integral "measure_integration/") (T formal-nonempty-type-decl nil expectation nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets nil) (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration/") (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration/") (S formal-const-decl "sigma_algebra" expectation nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (finite_measure? const-decl "bool" generalized_measure_def "measure_integration/") (finite_measure nonempty-type-eq-decl nil generalized_measure_def "measure_integration/") (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (measure? const-decl "bool" generalized_measure_def "measure_integration/") (measure_type nonempty-type-eq-decl nil generalized_measure_def "measure_integration/") (to_measure const-decl "measure_type" generalized_measure_def "measure_integration/") (<= const-decl "bool" reals nil) (probability nonempty-type-eq-decl nil probability_measure nil) (probability_measure? const-decl "bool" probability_measure nil) (probability_measure nonempty-type-eq-decl nil probability_measure nil) (P formal-const-decl "probability_measure" expectation nil)) shostak)) (markov_inequality_TCC1 0 (markov_inequality_TCC1-1 nil 3424592613 ("" (skosimp) (("" (lemma "integrable_abs" ("f" "X!1")) (("" (rewrite "integrable_is_measurable") nil nil)) nil)) nil) ((P formal-const-decl "probability_measure" expectation nil) (probability_measure nonempty-type-eq-decl nil probability_measure nil) (probability_measure? const-decl "bool" probability_measure nil) (probability nonempty-type-eq-decl nil probability_measure nil) (<= const-decl "bool" reals nil) (to_measure const-decl "measure_type" generalized_measure_def "measure_integration/") (measure_type nonempty-type-eq-decl nil generalized_measure_def "measure_integration/") (measure? const-decl "bool" generalized_measure_def "measure_integration/") (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (finite_measure nonempty-type-eq-decl nil generalized_measure_def "measure_integration/") (finite_measure? const-decl "bool" generalized_measure_def "measure_integration/") (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (S formal-const-decl "sigma_algebra" expectation nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration/") (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration/") (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-nonempty-type-decl nil expectation nil) (integrable nonempty-type-eq-decl nil integral "measure_integration/") (integrable? const-decl "bool" integral "measure_integration/") (integrable_abs judgement-tcc nil integral "measure_integration/") (abs const-decl "[T -> nonneg_real]" real_fun_ops "reals/") (nonneg_real nonempty-type-eq-decl nil real_types nil) (integrable_is_measurable judgement-tcc nil integral "measure_integration/") (integrable_abs application-judgement "integrable[T, S, to_measure(P)]" expectation nil)) nil)) (markov_inequality 0 (markov_inequality-1 nil 3424593171 ("" (skosimp) (("" (rewrite "div_mult_pos_le2") (("" (expand "E") (("" (lemma "indefinite_subset" ("E1" "{x:T | abs[T](X!1)(x) >= px!1}" "E2" "fullset[T]" "f" "abs[T](X!1)")) (("1" (split) (("1" (expand "integral" -1) (("1" (case-replace "phi(fullset[T]) * abs[T](X!1)=abs[T](X!1)") (("1" (hide -1) (("1" (typepred "px!1 <= abs[T](X!1)") (("1" (expand "<=" -1) (("1" (expand "<=" 1 1) (("1" (lemma "E_phi" ("A" "{t: T | abs[T](X!1)(t) >= px!1}")) (("1" (replace -1 1 rl) (("1" (hide -1) (("1" (expand "E" 1) (("1" (lemma "E_phi_TCC1" ("A" "{t: T | abs[T](X!1)(t) >= px!1}")) (("1" (lemma "integrable_scal" ("c" "px!1" "f" "phi[T, S]({t: T | abs[T](X!1)(t) >= px!1})")) (("1" (lemma "integral_scal" ("c" "px!1" "f" "phi[T, S]({t: T | abs[T](X!1)(t) >= px!1})")) (("1" (lemma "integral_ae_le" ("f1" "px!1 * phi[T, S]({t: T | abs[T](X!1)(t) >= px!1})" "f2" "phi({x:T | abs[T](X!1)(x) >= px!1}) * abs[T](X!1)")) (("1" (split -1) (("1" (name-replace "LHI" "integral.integral(phi({t: T | abs[T](X!1)(t) >= px!1}))") (("1" (name-replace "RHI" "integral.integral(abs[T](X!1))") (("1" (name-replace "MI1" "integral.integral(phi({x:T | abs[T](X!1)(x) >= px!1}) * abs[T](X!1))") (("1" (expand "*" -1) (("1" (expand "*" -2) (("1" (name-replace "FF" "(LAMBDA (t_1: T): px!1 * phi[T, S]({t: T | abs[T](X!1)(t) >= px!1})(t_1))") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "ae_le?") (("2" (expand "pointwise_ae?") (("2" (expand "*") (("2" (expand "phi") (("2" (expand "member") (("2" (expand "abs") (("2" (expand "ae?") (("2" (expand "fullset") (("2" (expand "ae_in?") (("2" (inst + "emptyset[T]") (("1" (skosimp) (("1" (case-replace "abs(X!1(x!1)) >= px!1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil) ("2" (expand "negligible_set?") (("2" (inst + "emptyset[T]") (("2" (split) (("1" (expand "null_set?") (("1" (expand "mu_fin?") (("1" (expand "mu") (("1" (expand "to_measure") (("1" (typepred "P") (("1" (expand "probability_measure?") (("1" (expand "finite_measure?") (("1" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (apply-extensionality :hide? t) (("2" (expand "*") (("2" (expand "fullset") (("2" (expand "phi") (("2" (expand "member") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (grind) nil nil)) nil) ("3" (hide 2) (("3" (expand "ae_nonneg?") (("3" (expand "pointwise_ae?") (("3" (expand "abs") (("3" (expand "ae?") (("3" (expand "fullset") (("3" (expand "ae_in?") (("3" (inst + "emptyset[T]") (("1" (skosimp) (("1" (assert) nil nil)) nil) ("2" (expand "negligible_set?") (("2" (inst + "emptyset[T]") (("2" (split) (("1" (expand "null_set?") (("1" (expand "mu_fin?") (("1" (expand "mu") (("1" (typepred "P") (("1" (expand "probability_measure?") (("1" (expand "finite_measure?") (("1" (flatten) (("1" (expand "to_measure") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (typepred "abs[T](X!1)") (("2" (lemma "measurable_ge") (("2" (inst - "abs[T](X!1)") (("2" (lemma "integrable_is_measurable") (("2" (inst - "abs[T](X!1)") (("2" (assert) (("2" (inst - "px!1") (("2" (expand "integrable?" 1) (("2" (case-replace "phi(fullset[T]) * abs[T](X!1) = abs[T](X!1)") (("2" (apply-extensionality :hide? t) (("2" (hide-all-but 1) (("2" (expand "*") (("2" (expand "fullset") (("2" (expand "phi") (("2" (expand "member") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "measurable_set?") (("3" (hide 2) (("3" (lemma "measurable_ge[T,S]" ("f" "abs[T](X!1)")) (("3" (typepred "X!1") (("3" (lemma "integrable_is_measurable[T,S,to_measure(P)]") (("3" (inst - "X!1") (("3" (lemma "abs_measurable[T,S]" ("g" "X!1")) (("1" (assert) (("1" (inst - "px!1") nil nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((integrable_abs application-judgement "integrable[T, S, to_measure(P)]" expectation nil) (div_mult_pos_le2 formula-decl nil real_props nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (T formal-nonempty-type-decl nil expectation nil) (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets nil) (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration/") (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration/") (S formal-const-decl "sigma_algebra" expectation nil) (nnreal type-eq-decl nil real_types nil) (<= const-decl "bool" reals nil) (probability nonempty-type-eq-decl nil probability_measure nil) (probability_measure? const-decl "bool" probability_measure nil) (probability_measure nonempty-type-eq-decl nil probability_measure nil) (P formal-const-decl "probability_measure" expectation nil) (measurable_function? const-decl "bool" measure_space_def "measure_integration/") (random_variable nonempty-type-eq-decl nil probability_measure nil) (<= const-decl "(S)" probability_space nil) (abs const-decl "[T -> nonneg_real]" real_fun_ops "reals/") (finite_measure? const-decl "bool" generalized_measure_def "measure_integration/") (finite_measure nonempty-type-eq-decl nil generalized_measure_def "measure_integration/") (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (measure? const-decl "bool" generalized_measure_def "measure_integration/") (measure_type nonempty-type-eq-decl nil generalized_measure_def "measure_integration/") (to_measure const-decl "measure_type" generalized_measure_def "measure_integration/") (integrable? const-decl "bool" integral "measure_integration/") (integrable nonempty-type-eq-decl nil integral "measure_integration/") (E const-decl "real" expectation nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (subset_algebra_fullset name-judgement "(S)" expectation nil) (measurable_fullset name-judgement "measurable_set[T, S]" expectation nil) (indefinite_subset formula-decl nil indefinite_integral "measure_integration/") (set type-eq-decl nil sets nil) (measurable_set? const-decl "bool" measure_space_def "measure_integration/") (measurable_set nonempty-type-eq-decl nil measure_space_def "measure_integration/") (fullset const-decl "set" sets nil) (integrable? const-decl "bool" indefinite_integral "measure_integration/") (ae_nonneg? const-decl "bool" measure_theory "measure_integration/") (integral const-decl "real" indefinite_integral "measure_integration/") (E_phi formula-decl nil expectation nil) (E_phi_TCC1 subtype-tcc nil expectation nil) (integral_scal formula-decl nil integral "measure_integration/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (real_times_real_is_real application-judgement "real" reals nil) (integral const-decl "real" integral "measure_integration/") (ae_le? const-decl "bool" measure_theory "measure_integration/") (member const-decl "bool" sets nil) (ae? const-decl "bool" measure_theory "measure_integration/") (ae_in? const-decl "bool" measure_theory "measure_integration/") (mu_fin? const-decl "bool" measure_props "measure_integration/") (sigma_algebra_IUnion_rew application-judgement "(S)" expectation nil) (mu const-decl "nnreal" measure_props "measure_integration/") (null_set? const-decl "bool" measure_theory "measure_integration/") (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas_aux "measure_integration/") (subset? const-decl "bool" sets nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (TRUE const-decl "bool" booleans nil) (negligible nonempty-type-eq-decl nil measure_theory "measure_integration/") (emptyset const-decl "set" sets nil) (negligible_set? const-decl "bool" measure_theory "measure_integration/") (finite_emptyset name-judgement "finite_set" finite_sets nil) (finite_emptyset name-judgement "finite_set[T]" countable_props "sets_aux/") (finite_emptyset name-judgement "finite_set[T]" countable_setofsets "sets_aux/") (finite_emptyset name-judgement "finite_set[T]" sigma_countable "sigma_set/") (null_emptyset name-judgement "null_set[T, S, to_measure(P)]" expectation nil) (subset_algebra_emptyset name-judgement "(S)" expectation nil) (measurable_emptyset name-judgement "measurable_set[T, S]" expectation nil) (pointwise_ae? const-decl "bool" measure_theory "measure_integration/") (* const-decl "[T -> real]" real_fun_ops "reals/") (integral_ae_le formula-decl nil integral "measure_integration/") (integrable_scal judgement-tcc nil integral "measure_integration/") (NOT const-decl "[bool -> bool]" booleans nil) (phi_is_simple application-judgement "simple[T, S]" expectation nil) (= const-decl "[T, T -> boolean]" equalities nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (phi const-decl "nat" measure_space "measure_integration/") (integrable_is_measurable judgement-tcc nil integral "measure_integration/") (measurable_ge formula-decl nil measure_space_def "measure_integration/") (measurable_function nonempty-type-eq-decl nil measure_space_def "measure_integration/") (abs_measurable judgement-tcc nil measure_space "measure_integration/")) shostak)) (markov_inequality_alt 0 (markov_inequality_alt-1 nil 3424688983 ("" (skosimp) (("" (lemma "trichotomy" ("x" "x!1")) (("" (split -1) (("1" (lemma "markov_inequality" ("px" "x!1" "X" "X!1")) (("1" (rewrite "div_mult_pos_le2") (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil) ("2" (replace -1) (("2" (lemma "E_nonneg" ("X" "abs(X!1)")) (("2" (split) (("1" (assert) nil nil) ("2" (skosimp) (("2" (expand "abs") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (lemma "both_sides_times_neg_le1" ("nz" "x!1" "x" "P(x!1 <= abs(X!1))" "y" "0")) (("1" (lemma "E_nonneg" ("X" "abs(X!1)")) (("1" (split -1) (("1" (assert) nil nil) ("2" (skosimp) (("2" (expand "abs") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ((real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (trichotomy formula-decl nil real_axioms nil) (negreal nonempty-type-eq-decl nil real_types nil) (< const-decl "bool" reals nil) (nonpos_real nonempty-type-eq-decl nil real_types nil) (both_sides_times_neg_le1 formula-decl nil real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (E_nonneg formula-decl nil expectation nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (integrable nonempty-type-eq-decl nil integral "measure_integration/") (integrable? const-decl "bool" integral "measure_integration/") (P formal-const-decl "probability_measure" expectation nil) (probability_measure nonempty-type-eq-decl nil probability_measure nil) (probability_measure? const-decl "bool" probability_measure nil) (probability nonempty-type-eq-decl nil probability_measure nil) (<= const-decl "bool" reals nil) (to_measure const-decl "measure_type" generalized_measure_def "measure_integration/") (measure_type nonempty-type-eq-decl nil generalized_measure_def "measure_integration/") (measure? const-decl "bool" generalized_measure_def "measure_integration/") (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (finite_measure nonempty-type-eq-decl nil generalized_measure_def "measure_integration/") (finite_measure? const-decl "bool" generalized_measure_def "measure_integration/") (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (S formal-const-decl "sigma_algebra" expectation nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration/") (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration/") (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (T formal-nonempty-type-decl nil expectation nil) (markov_inequality formula-decl nil expectation nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (E const-decl "real" expectation nil) (abs const-decl "[T -> nonneg_real]" real_fun_ops "reals/") (<= const-decl "(S)" probability_space nil) (random_variable nonempty-type-eq-decl nil probability_measure nil) (measurable_function? const-decl "bool" measure_space_def "measure_integration/") (div_mult_pos_le2 formula-decl nil real_props nil) (integrable_abs application-judgement "integrable[T, S, to_measure(P)]" expectation nil)) shostak))) ¤ Dauer der Verarbeitung: 0.347 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.Bot Zugriff |
