Impressum indefinite_integral.prf
Sprache: Lisp
(indefinite_integralnil 3391140825"" (skosimp)"" (typepred "f!1" )"" (expand "integrable?" -1) (("" (propax) nil nil )) nil ))nil ))nil )"bool" indefinite_integral nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil measure_space_def nil )"bool" measure_space_def nil )"sigma_algebra" indefinite_integral nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )set type-eq-decl nil sets nil )nil indefinite_integral nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil ))nil 3459223617"" (skosimp)"" (expand "integrable?" )"" (case-replace "phi(emptyset[T]) * g!1=lambda x: 0" )"1" (rewrite "integrable_zero" ) nil nil )"2" (apply-extensionality :hide? t)"2" (expand "*" )"2" (expand "emptyset" )"2" (expand "phi" )"2" (expand "member" ) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" indefinite_integral nil )"bool" sets nil )"real" reals nil )"measure_type" indefinite_integral nil )nil generalized_measure_defnil )"bool" generalized_measure_def nil )nil extended_nnreal"extended_nnreal/" )nil real_types nil )nil integral nil )"set" sets nil )"nat" measure_space nil )"sigma_algebra" indefinite_integral nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )set type-eq-decl nil sets nil )nil booleans nil )"[T -> real]" real_fun_ops "reals/" )"[T, T -> boolean]" equalities nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil indefinite_integral nil )"simple" indefinite_integralnil )"(S)" indefinite_integralnil )"null_set" indefinite_integral nil )"finite_set[T]" sigma_countable"sigma_set/" )"finite_set[T]" countable_setofsets"sets_aux/" )"finite_set[T]" countable_props"sets_aux/" )"finite_set" finite_sets nil ))nil ))nil 3459223725"" (skosimp)"" (expand "integral" )"" (case-replace "phi(emptyset) * g!1=lambda x: 0" )"1" (rewrite "integral_zero" ) nil nil )"2" (apply-extensionality :hide? t)"2" (hide 2) (("2" (grind) nil nil )) nil )) nil ))nil ))nil ))nil )"real" indefinite_integral nil )"real" reals nil )"bool" sets nil )"real" reals nil )"measure_type" indefinite_integral nil )nil generalized_measure_defnil )"bool" generalized_measure_def nil )nil extended_nnreal"extended_nnreal/" )nil real_types nil )nil integral nil )"set" sets nil )"nat" measure_space nil )"sigma_algebra" indefinite_integral nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )set type-eq-decl nil sets nil )nil booleans nil )"[T -> real]" real_fun_ops "reals/" )"[T, T -> boolean]" equalities nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil indefinite_integral nil )"simple" indefinite_integralnil )"(S)" indefinite_integralnil )"null_set" indefinite_integral nil )"finite_set[T]" sigma_countable"sigma_set/" )"finite_set[T]" countable_setofsets"sets_aux/" )"finite_set[T]" countable_props"sets_aux/" )"finite_set" finite_sets nil ))nil 3459223617"" (skosimp)"" (expand "integrable?" )"" (rewrite "indefinite_integrable" ) nil nil )) nil ))nil )"measurable_function[T, S]" nil )"bool" indefinite_integral nil )"measure_type" indefinite_integral nil )nil generalized_measure_defnil )"bool" generalized_measure_def nil )nil extended_nnreal"extended_nnreal/" )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" indefinite_integral nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )nil booleans nil )nil booleans nil )nil indefinite_integral nil )nil integral nil )"bool" integral nil )"set" sets nil )nil measure_space_def nil )"bool" measure_space_def nil )set type-eq-decl nil sets nil )nil integral nil )"(S)" indefinite_integralnil )"measurable_set[T, S]" nil ))nil ))nil 3459223764"" (skosimp)"" (expand "integral" 1 1)"" (case-replace "phi(fullset) * f!1=f!1" )"" (hide 2)"" (apply-extensionality :hide? t) (("" (grind) nil nil ))nil ))nil ))nil ))nil ))nil )"real" indefinite_integral nil )"real" reals nil )"bool" sets nil )"real" reals nil )nil integral nil )"bool" integral nil )"measure_type" indefinite_integral nil )nil generalized_measure_defnil )"bool" generalized_measure_def nil )nil extended_nnreal"extended_nnreal/" )nil real_types nil )"set" sets nil )"nat" measure_space nil )"sigma_algebra" indefinite_integral nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )set type-eq-decl nil sets nil )nil booleans nil )"[T -> real]" real_fun_ops "reals/" )"[T, T -> boolean]" equalities nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil indefinite_integral nil )"measurable_function[T, S]" nil )"simple" indefinite_integralnil )"(S)" indefinite_integralnil )"measurable_set[T, S]" nil ))nil 3395207138"" (skosimp)"" (typepred "E!1" )"" (expand "measurable_set?" ) (("" (propax) nil nil )) nil ))nil ))nil )nil measure_space_def nil )"bool" measure_space_def nil )"sigma_algebra" indefinite_integral nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )set type-eq-decl nil sets nil )nil indefinite_integral nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil ))nil 3395604081"" (skosimp)"" (lemma "integral_ae_ge_0" ("f" "phi(E!1) * f!1" ))"" (replace -3)"" (split -1)"1" (hide -3)"1" (expand "ae_in?" )"1" (skosimp)"1" (typepred "E!2" )"1" (expand "negligible_set?" )"1" (skosimp)"1" (expand "ae_0?" )"1" (expand "restrict" )"1" (expand "pointwise_ae?" )"1" (expand "ae?" )"1" expand "fullset" )"1" expand "ae_in?" )"1" "1" "E!3" )"1" expand "negligible_set?" )"1" "1" "FF" "X!1" )"1" case "forall x: difference(E!1,FF)(x) => f!1(x)>0" )"1" "1" "GG" "X!2" )"1" case "FORALL x: difference(E!1, GG)(x) => f!1(x) = 0" )"1" "1" "null_union" "N1" "FF" "N2" "GG" ))"1" "m_monotone" "a" "E!1" "b" "union(FF,GG)" ))"1" "1" "1" expand "null_set?" )"1" expand "x_le" )"1" expand "mu_fin?" )"1" expand "mu" )"1" "1" assert )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "subset?" )"2" "2" expand "member" )"2" "x!1" )"2" "x!1" )"2" expand "union" )"2" "2" expand "member" )"2" expand "difference" )"2" expand "member" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "null_set?" )"2" nil nil ))nil ))nil )"2" nil nil )"3" nil nil ))nil ))nil )"2" "2" "2" expand "difference" )"2" expand "member" )"2" "2" expand "subset?" )"2" "x!1" )"2" expand "member" )"2" assert )"2" "x!1" )"2" assert )"2" expand "*" )"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 ))nil )"2" "2" expand "difference" )"2" expand "member" )"2" "2" "x!1" )"2" expand "subset?" )"2" "x!1" )"2" assert )nil nil ))nil ))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" (hide -2 2)"2" (expand "ae_nonneg?" )"2" (expand "pointwise_ae?" )"2" (expand "ae?" )"2" (expand "fullset" )"2" (expand "ae_in?" )"2" (skosimp)"2" (typepred "E!2" )"2" (expand "*" )"2" (inst + "intersection(E!1,E!2)" )"1" "1" expand "intersection" )"1" assert )"1" expand "phi" )"1" assert )"1" "E!1(x!1)" )"1" "x!1" )"1" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "negligible_subset" "E" "E!2" "X" "intersection[T](E!1, E!2)" ))"2" "1" (propax) nil nil )"2" "2" expand "intersection" )"2" expand "subset?" )"2" expand "member" )"2" (skosimp*) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"measure_type" indefinite_integral nil )nil generalized_measure_defnil )"bool" generalized_measure_def nil )nil extended_nnreal"extended_nnreal/" )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" indefinite_integral nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )nil booleans nil )nil booleans nil )nil indefinite_integral nil )"bool" indefinite_integral nil )nil measure_space_def nil )"bool" measure_space_def nil )"nat" measure_space nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )set type-eq-decl nil sets nil )"[T -> real]" real_fun_ops "reals/" )nil integral nil )"bool" integral nil )nil integral nil )"bool" measure_theory nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" measure_theory nil )nil measure_theory nil )"R" restrict nil )"bool" measure_theory nil )"[bool, bool -> bool]" booleans nil )"set" sets nil )"bool" reals nil )"real" reals nil )"bool" booleans nil )nil measure_props nil )"set" sets nil )"bool" sets nil )"bool" sets nil )"bool" extended_nnreal "extended_nnreal/" )"nnreal" measure_props nil )"(total_order?[real])" nil )"bool" measure_props nil )nil measure_theory nil )"bool" measure_theory nil )nil measure_theory nil )"(strict_total_order?[real])" real_props nil )"T" indefinite_integral nil )"measurable_set[T, S]" indefinite_integralnil )"[T, T -> boolean]" equalities nil )"set" sets nil )"bool" measure_theory nil )"bool" measure_theory nil )"bool" measure_theory nil )"measurable_set[T, S]" nil )"(S)" indefinite_integralnil )"set" sets nil )"negligible[T, S, m]" indefinite_integralnil )"({x | TRUE})" indefinite_integral nil )nil measure_theory nil ))nil 3431893575"" (skosimp)"" (expand "integrable?" )"" (rewrite "indefinite_integrable" ) nil nil )) nil ))nil )"bool" indefinite_integral nil )"measure_type" indefinite_integral nil )nil generalized_measure_defnil )"bool" generalized_measure_def nil )nil extended_nnreal"extended_nnreal/" )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" indefinite_integral nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )nil booleans nil )nil booleans nil )nil indefinite_integral nil )nil integral nil )"bool" integral nil )nil measure_space_def nil )"bool" measure_space_def nil )set type-eq-decl nil sets nil )nil integral nil ))nil ))nil 3391226280"" (skosimp)"" (expand "integral" )"" (name "H" "f1!1-f2!1" )"" (lemma "integrable_diff" ("f1" "f1!1" "f2" "f2!1" ))"" (replace -2)"" (lemma "integrable_is_measurable" ("x" "H" ))"" (lemma "measurable_gt" ("f" "H" ))"" (lemma "measurable_lt" ("f" "H" ))"" (assert )"" (inst - "0" )"" (inst - "0" )"" (inst-cp - "{z: T | H(z) > 0}" )"1" (inst - "{z: T | H(z) < 0}" )"1" "indefinite_eq_0" "E" "{z: T | H(z) > 0}" "f" "H" ))"1" "1" "indefinite_eq_0" "E" "{z: T | H(z) < 0}" "f" "-H" ))"1" "1" "1" "1" "m_disjoint_union" "a" "{z: T | H(z) < 0}" "b" "{z: T | H(z) > 0}" ))"1" "1" expand "x_eq" )"1" expand "mu_fin?" )"1" expand "mu" )"1" assert )"1" "1" expand "x_add" )"1" assert )"1" replace "1" replace "1" "1" expand "ae_eq?" )"1" expand "restrict" )"1" expand "pointwise_ae?" )"1" expand "ae?" )"1" expand "fullset" )"1" expand "ae_in?" )"1" "union({z: T | H(z) < 0}, {z: T | H(z) > 0})" )"1" "1" expand "H" )"1" expand "union" )"1" expand "member" )"1" "1" assert )"1" expand "-" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "negligible_set?" )"2" "union({z: T | H(z) < 0}, {z: T | H(z) > 0})" )"2" "1" expand "null_set?" )"1" rewrite "measurable_union" )"1" expand "mu_fin?" )"1" expand "mu" )"1" nil nil ))nil ))nil ))nil ))nil )"2" expand "subset?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "disjoint?" )"2" expand "intersection" )"2" expand "empty?" )"2" "2" expand "member" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "ae_in?" )"2" "2" "{z: T | H(z) > 0}" )"1" "1" expand "-" )"1" assert )nil nil ))nil ))nil )"2" expand "negligible_set?" )"2" "{z: T | H(z) > 0}" )"2" "1" expand "null_set?" )"1" expand "measurable_set?" )"1" assert )nil nil ))nil ))nil )"2" expand "subset?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" expand "H" 1 2)"3" "phi({z: T | H(z) < 0}) * -(f1!1 - f2!1) = phi({z: T | H(z) < 0}) * f2!1-phi({z: T | H(z) < 0}) * f1!1" )"1" rewrite "integral_diff" )"1" (assert ) nil nil ))nil )"2" "2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "integrable?" )"2" rewrite "indefinite_integrable" )"2" expand "measurable_set?" )"2" (propax) nil nil ))nil ))nil ))nil )"3" expand "measurable_set?" )"3" (propax) nil nil ))nil ))nil )"2" "2" expand "ae_in?" )"2" expand "member" )"2" (propax) nil nil ))nil ))nil ))nil )"3" "3" expand "H" 1 2)"3" expand "-" 1)"3" expand "*" 1)"3" "integral_diff" "f1" "phi({z: T | H(z) > 0}) * f1!1" "f2" "phi({z: T | H(z) > 0}) * f2!1" ))"3" expand "-" -1)"3" expand "*" -1)"3" replace -1 1)"3" assert )"3" expand "*" -8)"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "integrable?" )"2" rewrite "indefinite_integrable" )"2" expand "measurable_set?" )"2" (propax) nil nil ))nil ))nil ))nil )"3" expand "measurable_set?" )"3" (propax) nil nil ))nil ))nil )"2" (expand "measurable_set?" )"2" (propax) nil nil )) nil ))nil )"2" (expand "measurable_set?" )"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" indefinite_integral nil )nil integral nil )nil integral nil )nil measure_space_def nil )set type-eq-decl nil sets nil )"bool" measure_space_def nil )"bool" reals nil )"integrable[T, S, m]" indefinite_integral nil )nil measure_space_def nil )nil indefinite_integral nil )"bool" indefinite_integral nil )"integrable" nil )"[T -> real]" real_fun_ops "reals/" )"nat" measure_space nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[T -> real]" real_fun_ops "reals/" )nil integral nil )"real" reals nil )"real" reals nil )nil measure_props nil )"set" sets nil )"bool" sets nil )"bool" sets nil )"bool" extended_nnreal "extended_nnreal/" )"nnreal" measure_props nil )"bool" measure_theory nil )"bool" measure_theory nil )"set" sets nil )"bool" measure_theory nil )"set" sets nil )nil measure_theory nil )"bool" sets nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"bool" sets nil )"bool" measure_theory nil )nil measure_space_def nil )"bool" measure_theory nil )"bool" measure_theory nil )"(S)" indefinite_integralnil )"measurable_set[T, S]" nil )"R" restrict nil )"extended_nnreal" extended_nnreal"extended_nnreal/" )"bool" measure_props nil )nil integral nil )"bool" reals nil )nil measure_space_def nil )"integrable" nil )nil indefinite_integral nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[T, T -> boolean]" equalities nil )"[T -> real]" real_fun_ops "reals/" )nil booleans nil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def nil )nil subset_algebra_def nil )"sigma_algebra" indefinite_integral nil )"bool" reals nil )nil real_types nil )nil extended_nnreal"extended_nnreal/" )"bool" generalized_measure_def nil )nil generalized_measure_defnil )"measure_type" indefinite_integral nil )"bool" integral nil )nil integral nil ))nil 3391140825"" (skosimp)"" (typepred "F!1" )"" (expand "integrable?" )"" (lemma "isf_is_integrable" )"" (inst - "phi[T, S](intersection(E!1,F!1))" )"1" (expand "intersection" )"1" (expand "phi" )"1" (expand "member" )"1" (expand "*" )"1" "(LAMBDA (x_1: T): IF E!1(x_1) THEN 1 ELSE 0 ENDIF *IF F!1(x_1) THEN 1 ELSE 0 ENDIF)=(LAMBDA (x_1: T):IF E!1(x_1) AND F!1(x_1) THEN 1 ELSE 0 ENDIF)") "1" (apply-extensionality :hide? t)"1" (hide-all-but 1) (("1" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (rewrite "isf_phi" )"2" (hide 2)"2" (expand "mu_fin?" )"2" "m_monotone" "a" "intersection[T](E!1, F!1)" "b" "F!1" ))"2" (split -1)"1" (expand "x_le" ) (("1" (assert ) nil nil ))nil )"2" (hide-all-but 1) (("2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" measure_props nil )"measure_type" indefinite_integral nil )nil generalized_measure_defnil )"bool" generalized_measure_def nil )nil extended_nnreal"extended_nnreal/" )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 )nil measure_space_def nil )"bool" measure_space_def nil )"sigma_algebra" indefinite_integral nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )set type-eq-decl nil sets nil )nil indefinite_integral nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil integral nil )nil measure_props nil )"bool" sets nil )"(partial_order?[set[T]])" nil )"bool" extended_nnreal "extended_nnreal/" )"(total_order?[real])" nil )nil isf nil )"bool" sets nil )AND const-decl "[bool, bool -> bool]" booleans nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"[numfield, numfield -> numfield]" number_fields nil )"[T, T -> boolean]" equalities nil )nil number_fields nil )"real" reals nil )"[T -> real]" real_fun_ops "reals/" )"(divides(m))" divides nil )"(divides(n))" divides nil )"nonneg_int" nil )nil isf nil )"bool" isf nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"nat" measure_space nil )"set" sets nil )"measurable_set[T, S]" indefinite_integralnil )"(mu_fin?)" indefinite_integral nil )"measurable_set" nil )"bool" indefinite_integral nil ))nil ))nil 3431890731"" (skosimp)"" (typepred "F!1" )"" (typepred "E!1" )"" (lemma "measurable_intersection" ("a" "E!1" "b" "F!1" ))"" (expand "measurable_set?" )"" (assert )"" (expand "mu_fin?" )"" "m_monotone" "a" "intersection[T](E!1, F!1)" "b" "F!1" ))"" (split -1)"1" (expand "x_le" ) (("1" (assert ) nil nil )) nil )"2" (hide-all-but 1) (("2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" measure_props nil )"measure_type" indefinite_integral nil )nil generalized_measure_defnil )"bool" generalized_measure_def nil )nil extended_nnreal"extended_nnreal/" )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 )nil measure_space_def nil )"bool" measure_space_def nil )"sigma_algebra" indefinite_integral nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )set type-eq-decl nil sets nil )nil indefinite_integral nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil measure_space_def nil )"measurable_set" nil )nil measure_props nil )"set" sets nil )"bool" sets nil )"bool" sets nil )"(partial_order?[set[T]])" nil )"bool" extended_nnreal "extended_nnreal/" )"(total_order?[real])" nil ))nil ))nil 3391166738"" (skosimp)"" (expand "integral" )"" (lemma "integral_phi" ("F" "intersection(E!1, F!1)" ))"" "phi(intersection(E!1, F!1)) = phi(E!1) * phi(F!1)" )"" (hide-all-but 1)"" (apply-extensionality :hide? t)"1" (grind) nil nil ) ("2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"real" indefinite_integral nil )"isf" indefinite_integral nil )"[T, T -> boolean]" equalities nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"nat" measure_space nil )"[T -> real]" real_fun_ops "reals/" )"(mu_fin?)" indefinite_integral nil )"measurable_set[T, S]" indefinite_integralnil )AND const-decl "[bool, bool -> bool]" booleans nil )"even_int" integersnil )"bool" sets nil )"nonneg_int" nil )"(divides(n))" divides nil )"(divides(m))" divides nil )"real" reals nil )"measurable_set" nil )nil integral nil )set type-eq-decl nil sets nil )"bool" measure_space_def nil )nil measure_space_def nil )"bool" measure_props nil )"set" sets nil )nil indefinite_integral nil )nil booleans nil )nil booleans nil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def nil )nil subset_algebra_def nil )"sigma_algebra" indefinite_integral nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil real_types nil )nil extended_nnreal"extended_nnreal/" )"bool" generalized_measure_def nil )nil generalized_measure_defnil )"measure_type" indefinite_integral nil ))nil 3431890731"" (skosimp)"" (typepred "f1!1" )"" (typepred "f2!1" )"" (expand "integrable?" )"" "integrable_add" "f1" "phi(E!1) * f1!1" "f2" "phi(E!1) * f2!1" ))"1" "((+[T])(phi(E!1) * f1!1, phi(E!1) * f2!1))=(phi(E!1) * ((+[T])(f1!1, f2!1)))" )"1" (apply-extensionality :hide? t)"1" (hide-all-but 1) (("1" (grind) nil nil )) nil ))nil ))nil )"2" (propax) nil nil ) ("3" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"bool" indefinite_integral nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil measure_space_def nil )"bool" measure_space_def nil )"sigma_algebra" indefinite_integral nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )set type-eq-decl nil sets nil )nil indefinite_integral nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"[T -> real]" real_fun_ops "reals/" )"[T, T -> boolean]" equalities nil )"bool" sets nil )"real" reals nil )"real" reals nil )"real" reals nil )nil integral nil )"bool" integral nil )nil integral nil )"[T -> real]" real_fun_ops "reals/" )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"nat" measure_space nil )"bool" reals nil )nil real_types nil )nil extended_nnreal"extended_nnreal/" )"bool" generalized_measure_def nil )nil generalized_measure_defnil )"measure_type" indefinite_integral nil ))nil ))nil 3391222633"" (skosimp)"" (expand "integral" )"" "integral_add" "f1" "phi(E!1) * f1!1" "f2" "phi(E!1) * f2!1" ))"" "phi(E!1) * (f1!1 + f2!1)=phi(E!1) * f1!1 + phi(E!1) * f2!1" )"" (hide-all-but 1)"" (apply-extensionality :hide? t) (("" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" indefinite_integral nil )"[T -> real]" real_fun_ops "reals/" )"[T, T -> boolean]" equalities nil )"bool" sets nil )"real" reals nil )"real" reals nil )"real" reals nil )nil integral nil )"bool" integral nil )nil integral nil )"[T -> real]" real_fun_ops "reals/" )set type-eq-decl nil sets nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"nat" measure_space nil )"bool" measure_space_def nil )nil measure_space_def nil )"bool" indefinite_integral nil )nil indefinite_integral nil )nil booleans nil )nil booleans nil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def nil )nil subset_algebra_def nil )"sigma_algebra" indefinite_integral nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil real_types nil )nil extended_nnreal"extended_nnreal/" )"bool" generalized_measure_def nil )nil generalized_measure_defnil )"measure_type" indefinite_integral nil ))nil 3431890731"" (skosimp)"" (typepred "f!1" )"" (expand "integrable?" )"" (lemma "integrable_scal" ("c" "c!1" "f" "phi(E!1) * f!1" ))"1" "(*[T](c!1, phi(E!1) * f!1))=(phi(E!1) * (*[T](c!1, f!1)))" )"1" (apply-extensionality :hide? t)"1" (hide-all-but 1) (("1" (grind) nil nil )) nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil )"bool" indefinite_integral nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil measure_space_def nil )"bool" measure_space_def nil )"sigma_algebra" indefinite_integral nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )set type-eq-decl nil sets nil )nil indefinite_integral nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"measure_type" indefinite_integral nil )nil generalized_measure_defnil )"bool" generalized_measure_def nil )nil extended_nnreal"extended_nnreal/" )nil real_types nil )"bool" reals nil )"nat" measure_space nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[T -> real]" real_fun_ops "reals/" )nil integral nil )"bool" integral nil )nil integral nil )"real" reals nil )"real" reals nil )"bool" sets nil )"[T, T -> boolean]" equalities nil )"[T -> real]" real_fun_ops "reals/" ))nil ))nil 3391329459"" (skosimp)"" (expand "integral" )"" (case-replace "phi(E!1) * (c!1 * f!1) = c!1*(phi(E!1)*f!1)" )"1" (rewrite "integral_scal" ) nil nil )"2" (hide 2)"2" (apply-extensionality :hide? t) (("2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil )"real" indefinite_integral nil )"real" reals nil )"real" reals nil )"bool" sets nil )nil integral nil )"bool" integral nil )nil integral nil )nil real_types nil )nil extended_nnreal"extended_nnreal/" )"bool" generalized_measure_def nil )nil generalized_measure_defnil )"measure_type" indefinite_integral nil )"bool" indefinite_integral nil )"[T -> real]" real_fun_ops "reals/" )nil measure_space_def nil )"bool" measure_space_def nil )"nat" measure_space nil )"sigma_algebra" indefinite_integral nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )set type-eq-decl nil sets nil )nil booleans nil )"[T -> real]" real_fun_ops "reals/" )"[T, T -> boolean]" equalities nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil indefinite_integral nil ))nil 3431890731"" (skosimp)"" (typepred "f!1" )"" (expand "integrable?" )"" (lemma "integrable_opp" ("f" "phi(E!1) * f!1" ))"1" (case-replace "(-(phi(E!1) * f!1))=(phi(E!1) * -f!1)" )"1" (apply-extensionality :hide? t)"1" (hide-all-but 1) (("1" (grind) nil nil )) nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil )"bool" indefinite_integral nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil measure_space_def nil )"bool" measure_space_def nil )"sigma_algebra" indefinite_integral nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )set type-eq-decl nil sets nil )nil indefinite_integral nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"measure_type" indefinite_integral nil )nil generalized_measure_defnil )"bool" generalized_measure_def nil )nil extended_nnreal"extended_nnreal/" )nil real_types nil )"bool" reals nil )"nat" measure_space nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[T -> real]" real_fun_ops "reals/" )nil integral nil )"bool" integral nil )nil integral nil )"real" reals nil )"real" reals nil )"real" reals nil )"bool" sets nil )"[T, T -> boolean]" equalities nil )"[T -> real]" real_fun_ops "reals/" ))nil ))nil 3391329564"" (skosimp)"" (lemma "indefinite_scal" ("c" "-1" "f" "f!1" "E" "E!1" ))"" (case-replace "-1 * f!1=-f!1" )"1" (assert ) nil nil )"2" (apply-extensionality :hide? t)"2" (hide-all-but 1) (("2" (grind) nil nil )) nil )) nil ))nil ))nil ))nil )"bool" indefinite_integral nil )nil measure_space_def nil )"bool" measure_space_def nil )"sigma_algebra" indefinite_integral nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )set type-eq-decl nil sets nil )nil booleans nil )nil indefinite_integral nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil indefinite_integral nil )"odd_int" integers nil )"real" reals nil )"real" reals nil )"real" reals nil )"[T -> real]" real_fun_ops "reals/" )"[T -> real]" real_fun_ops "reals/" )"[T, T -> boolean]" equalities nil ))nil 3431890731"" (skosimp)"" (typepred "f1!1" )"" (typepred "f2!1" )"" (expand "integrable?" )"" "integrable_diff" "f1" "phi(E!1) * f1!1" "f2" "phi(E!1) * f2!1" ))"1" "((-[T])(phi(E!1) * f1!1, phi(E!1) * f2!1))=(phi(E!1) * ((-[T])(f1!1, f2!1)))" )"1" (hide-all-but 1)"1" (apply-extensionality :hide? t)"1" (grind) nil nil )) nil ))nil ))nil )"2" (propax) nil nil ) ("3" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"bool" indefinite_integral nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil measure_space_def nil )"bool" measure_space_def nil )"sigma_algebra" indefinite_integral nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )set type-eq-decl nil sets nil )nil indefinite_integral nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"[T -> real]" real_fun_ops "reals/" )"[T, T -> boolean]" equalities nil )"bool" sets nil )"real" reals nil )"real" reals nil )nil integral nil )"bool" integral nil )nil integral nil )"[T -> real]" real_fun_ops "reals/" )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"nat" measure_space nil )"bool" reals nil )nil real_types nil )nil extended_nnreal"extended_nnreal/" )"bool" generalized_measure_def nil )nil generalized_measure_defnil )"measure_type" indefinite_integral nil ))nil ))nil 3391329626"" (skosimp)"" (lemma "indefinite_opp" ("f" "f2!1" "E" "E!1" ))"" "indefinite_add" ("f1" "f1!1" "f2" "-f2!1" "E" "E!1" ))"" (case-replace "f1!1 + -f2!1 = f1!1 - f2!1" )"1" (assert ) nil nil )"2" (hide-all-but 1)"2" (apply-extensionality :hide? t)"2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"bool" indefinite_integral nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil measure_space_def nil )"bool" measure_space_def nil )"sigma_algebra" indefinite_integral nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil indefinite_integral nil )nil indefinite_integral nil )"[T, T -> boolean]" equalities nil )"[T -> real]" real_fun_ops "reals/" )"[T -> real]" real_fun_ops "reals/" )"real" reals nil )"real" reals nil )"real" reals nil )nil indefinite_integral nil )"[T -> real]" real_fun_ops "reals/" ))nil 3395208470"" (skosimp)"" (split)"1" (flatten)"1" (skosimp)"1" (typepred "f1!1" )"1" (typepred "f2!1" )"1" (expand "integral" )"1" (assert )"1" (hide -1 -2 2)"1" "integral_ae_eq" "f" "phi(E!1) * f1!1" "h" "phi(E!1) * f2!1" ))"1" (assert )"1" (hide 2)"1" (expand "ae_eq?" )"1" (expand "restrict" )"1" expand "*" )"1" expand "pointwise_ae?" )"1" expand "ae?" )"1" expand "fullset" )"1" expand "ae_in?" )"1" "1" "E!2" )"1" "1" "x!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (rewrite "prod_measurable" )"2" (hide -1 2)"2" (lemma "phi_is_simple" ("X" "E!1" ))"1" "simple_is_measurable" )"1" (inst - "phi(E!1)" ) nil nil ))nil )"2" "E!1" )"2" expand "measurable_set?" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp)"2" (lemma "indefinite_eq" ("f1" "f1!1" "f2" "f2!1" ))"2" (assert ) nil nil )) nil ))nil ))nil ))nil )nil measure_space_defnil )"bool" measure_space_def nil )nil measure_space_def nil )"bool" measure_space_def nil )"nat" measure_space nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )set type-eq-decl nil sets nil )"[T -> real]" real_fun_ops "reals/" )nil integral nil )"R" restrict nil )"bool" measure_theory nil )"set" sets nil )"bool" sets nil )"real" reals nil )"bool" booleans nil )"bool" measure_theory nil )nil measure_theory nil )"bool" measure_theory nil )"bool" measure_theory nil )"(S)" indefinite_integralnil )"measurable_set[T, S]" nil )"bool" measure_theory nil )nil measure_space nil )nil measure_space nil )nil measure_space nil )"bool" measure_space nil )"measurable_set[T, S]" indefinite_integralnil )nil measure_space nil )"real" indefinite_integral nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil indefinite_integral 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 nil )nil subset_algebra_def nil )"sigma_algebra" indefinite_integral nil )"bool" reals nil )nil real_types nil )nil extended_nnreal"extended_nnreal/" )"bool" generalized_measure_def nil )nil generalized_measure_defnil )"measure_type" indefinite_integral nil )"bool" integral nil )nil integral nil )nil indefinite_integral nil ))nil 3391331082"" (skosimp)"" (split)"1" (flatten)"1" (skosimp)"1" (expand "integral" )"1" "integral_ae_le" "f1" "lambda (x:T): 0" "f2" "phi(E!1) * f!1" ))"1" (rewrite "integral_zero" )"1" (assert )"1" (hide 2)"1" (expand "ae_nonneg?" )"1" (expand "ae_le?" )"1" (expand "pointwise_ae?" )"1" (expand "ae?" )"1" (expand "fullset" )"1" expand "ae_in?" )"1" "1" "E!2" )"1" "1" "x!1" )"1" assert )"1" expand "*" )"1" expand "phi" )"1" assert )"1" assert )"1" "E!1(x!1)" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (rewrite "integrable_zero" ) nil nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (inst - "{x | f!1(x) < 0}" )"1" (expand "integral" )"1" "integral_nonneg" "f" "-(phi({x | f!1(x) < 0}) * f!1)" ))"1" (split -1)"1" (rewrite "integral_opp" )"1" "integral(phi({x_1: T | f!1(x_1) < 0}) * f!1)=0" )"1" (hide -2 -3)"1" "indefinite_opp" "f" "f!1" "E" "{x_1: T | f!1(x_1) < 0}" ))"1" (expand "integral" -1)"1" (replace -2)"1" "indefinite_eq_0" "f" "-f!1" "E" "{x_2: T | f!1(x_2) < 0}" ))"1" replace -2)"1" assert )"1" "1" "1" expand "ae_nonneg?" )"1" expand "pointwise_ae?" )"1" expand "ae?" )"1" expand "fullset" )"1" expand "ae_in?" )"1" "{x_1: T | f!1(x_1) < 0}" )"1" "1" assert )nil nil ))nil )"2" expand "negligible_set?" )"2" "2" "{x_1: T | f!1(x_1) < 0}" )"2" expand "null_set?" )"2" assert )"2" "1" "1" "measurable_lt" "f" "f!1" ))"1" "1" "1" "0" )"1" expand "measurable_set?" )"1" nil nil ))nil ))nil )"2" rewrite "integrable_is_measurable" )nil nil ))nil ))nil ))nil ))nil )"2" expand "subset?" )"2" expand "member" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "ae_in?" )"2" "emptyset[T]" )"2" "2" "x!1" )"2" assert )"2" expand "-" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "integrable?" )"2" rewrite "indefinite_integrable" )nil nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (lemma "measurable_lt" ("f" "f!1" ))"2" (flatten)"2" "1" "0" )"1" expand "integrable?" )"1" rewrite "indefinite_integrable" )"1" expand "measurable_set?" )"1" (propax) nil nil ))nil ))nil ))nil ))nil )"2" rewrite "integrable_is_measurable" )nil nil ))nil ))nil ))nil ))nil )"3" (typepred "f!1" )"3" (hide -2 2)"3" (lemma "integrable_is_measurable" )"3" "f!1" )"3" rewrite "measurable_lt" )"3" "0" )"3" expand "measurable_set?" )"3" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (skosimp)"2" (expand "-" )"2" (expand "*" )"2" (expand "phi" )"2" (expand "member" )"2" (hide-all-but 1)"2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (rewrite "integrable_opp" ) nil nil ))nil ))nil )"2" (typepred "f!1" )"2" (lemma "measurable_lt" )"2" (inst - "f!1" )"2" (assert )"2" (flatten)"2" (hide -2)"2" (split)"1" (inst - "0" )"1" (expand "measurable_set?" )"1" (propax) nil nil )) nil ))nil )"2" (assert )"2" (rewrite "integrable_is_measurable" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"measure_type" indefinite_integral nil )nil generalized_measure_defnil )"bool" generalized_measure_def nil )nil extended_nnreal"extended_nnreal/" )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" indefinite_integral nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )nil booleans nil )nil booleans nil )nil indefinite_integral nil )nil measure_space_def nil )"bool" measure_space_def nil )"nat" measure_space nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )set type-eq-decl nil sets nil )"[T -> real]" real_fun_ops "reals/" )nil integral nil )"bool" integral nil )nil integral nil )"(total_order?[real])" nil )"bool" measure_theory nil )"bool" measure_theory nil )"set" sets nil )"bool" sets nil )"real" reals nil )"bool" booleans nil )"bool" measure_theory nil )nil measure_theory nil )"bool" measure_theory nil )"bool" measure_theory nil )"(S)" indefinite_integralnil )"measurable_set[T, S]" nil )"bool" measure_theory nil )nil integral nil )nil integral nil )"real" indefinite_integral nil )"integrable[T, S, m]" indefinite_integralnil )"bool" reals nil )"[T -> real]" real_fun_ops "reals/" )nil integral nil )"real" reals nil )nil integral nil )"real" reals nil )"(total_order?[real])" nil )"integrable" nil )nil indefinite_integral nil )"even_int" integers nil )"(strict_total_order?[real])" real_props nil )NOT const-decl "[bool -> bool]" booleans nil )"set" sets nil )"finite_set" finite_sets nil )"finite_set[T]" countable_props"sets_aux/" )"finite_set[T]" countable_setofsets"sets_aux/" )"finite_set[T]" sigma_countable"sigma_set/" )"null_set" indefinite_integral nil )"(S)" indefinite_integralnil )"(strict_total_order?[real])" real_props nil )"bool" measure_theory nil )nil measure_space_def nil )nil integral nil )"bool" sets nil )nil integral nil )"bool" indefinite_integral nil )nil indefinite_integral nil )"[T, T -> boolean]" equalities nil )"real" integral nil )nil integral nil ))nil 3391330005"" (skosimp)"" (lemma "indefinite_0_le" ("f" "f2!1-f1!1" ))"" (split)"1" (flatten)"1" (split -2)"1" (hide-all-but (-1 1))"1" (skosimp)"1" (inst - "E!1" )"1" (rewrite "indefinite_diff" )"1" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (hide-all-but (-1 1)) (("2" (grind) nil nil )) nil ))nil ))nil )"2" (flatten)"2" (split -3)"1" (hide-all-but (-1 1)) (("1" (grind) nil nil )) nil )"2" (hide-all-but (-1 1))"2" (skosimp)"2" (inst - "E!1" )"2" (rewrite "indefinite_diff" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"[T -> real]" real_fun_ops "reals/" )nil integral nil )"bool" integral nil )"measure_type" indefinite_integral nil )nil generalized_measure_defnil )"bool" generalized_measure_def nil )nil extended_nnreal"extended_nnreal/" )nil real_types nil )"bool" reals nil )"sigma_algebra" indefinite_integral nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )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 indefinite_integral nil )nil indefinite_integral nil )"integrable" nil )nil measure_theory nil )"bool" measure_theory nil )NOT const-decl "[bool -> bool]" booleans nil )"set" sets nil )"bool" sets nil )"bool" measure_theory nil )"nnreal" measure_props nil )"bool" measure_props nil )"bool" measure_theory nil )"bool" measure_theory nil )"bool" measure_theory nil )"bool" measure_theory nil )"bool" measure_theory nil )"bool" sets nil )"measurable_set[T, S]" nil )"(S)" indefinite_integralnil )nil measure_space_def nil )"bool" measure_space_def nil )set type-eq-decl nil sets nil )"(total_order?[real])" nil )"real" reals nil )nil indefinite_integral nil )"bool" indefinite_integral nil ))nil 3431890731"" (skosimp)"" (typepred "f!1" )"" (expand "integrable?" )"" (lemma "integrable_plus" ("f" "phi(E!1) * f!1" ))"1" "(plus[T](phi(E!1) * f!1))=(phi(E!1) * plus[T](f!1))" )"1" (apply-extensionality :hide? t)"1" (hide-all-but 1) (("1" (grind) nil nil )) nil )"2" (hide-all-but 1) (("2" (grind) nil nil )) nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil )"bool" indefinite_integral nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil measure_space_def nil )"bool" measure_space_def nil )"sigma_algebra" indefinite_integral nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )set type-eq-decl nil sets nil )nil indefinite_integral nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"measure_type" indefinite_integral nil )nil generalized_measure_defnil )"bool" generalized_measure_def nil )nil extended_nnreal"extended_nnreal/" )nil real_types nil )"bool" reals nil )"nat" measure_space nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[T -> real]" real_fun_ops "reals/" )nil integral nil )"bool" integral nil )nil integral nil )"(integrable?(E!1))" indefinite_integralnil )"measurable_set[T, S]" indefinite_integralnil )"real" reals nil )"nnreal" nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"bool" sets nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"[T, T -> boolean]" equalities nil )"[T -> nnreal]" real_fun_ops_aux "reals/" ))nil ))nil 3431890731"" (skosimp)"" (typepred "f!1" )"" (expand "integrable?" )"" (lemma "integrable_minus" ("f" "phi(E!1) * f!1" ))"1" "(minus[T](phi(E!1) * f!1))=(phi(E!1) * minus[T](f!1))" )"1" (apply-extensionality :hide? t)"1" (hide-all-but 1) (("1" (grind) nil nil )) nil )"2" (hide-all-but 1) (("2" (grind) nil nil )) nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil )"bool" indefinite_integral nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil measure_space_def nil )"bool" measure_space_def nil )"sigma_algebra" indefinite_integral nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )set type-eq-decl nil sets nil )nil indefinite_integral nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"measure_type" indefinite_integral nil )nil generalized_measure_defnil )"bool" generalized_measure_def nil )nil extended_nnreal"extended_nnreal/" )nil real_types nil )"bool" reals nil )"nat" measure_space nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[T -> real]" real_fun_ops "reals/" )nil integral nil )"bool" integral nil )nil integral nil )"(integrable?(E!1))" indefinite_integralnil )"measurable_set[T, S]" indefinite_integralnil )"real" reals nil )"nnreal" nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"real" reals nil )"bool" sets nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"[T, T -> boolean]" equalities nil )"[T -> nnreal]" real_fun_ops_aux "reals/" ))nil ))nil 3391330468"" (skosimp)"" (expand "integral" )"" (lemma "plus_minus_def" ("f" "f!1" ))"" (rewrite "integral_diff" 1 :dir rl)"" "phi(E!1) * f!1=phi(E!1) * plus(f!1) - phi(E!1) * minus(f!1)" )"" (hide 2)"" (apply-extensionality :hide? t)"" "extensionality_postulate" "f" "f!1" "g" "plus(f!1) - minus(f!1)" ))"" (replace -1 -2 rl)"" (inst - "x!1" )"" (hide -1) (("" (grind) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" indefinite_integral nil )nil integral nil )"bool" integral nil )nil integral nil )"[T -> real]" real_fun_ops "reals/" )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"nat" measure_space nil )"[T -> nnreal]" real_fun_ops_aux "reals/" )"[T -> nnreal]" real_fun_ops_aux "reals/" )"bool" reals nil )nil real_types nil )nil extended_nnreal"extended_nnreal/" )"bool" generalized_measure_def nil )nil generalized_measure_defnil )"measure_type" indefinite_integral nil )nil functions nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"nnreal" nil )"real" reals nil )"bool" sets nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"odd_int" integers nil )"[T, T -> boolean]" equalities nil )"[T -> real]" real_fun_ops "reals/" )nil real_fun_ops_aux "reals/" )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )set type-eq-decl nil sets nil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def nil )nil subset_algebra_def nil )"sigma_algebra" indefinite_integral nil )"bool" measure_space_def nil )nil measure_space_def nil )"bool" indefinite_integral nil )nil indefinite_integral nil ))nil 3431890731"" (skosimp)"" (typepred "f!1" )"" (expand "integrable?" )"" "indefinite_integrable" "E" "E1!1" "f" "phi(union(E1!1, E2!1)) * f!1" ))"1" "(phi(E1!1) * (phi(union(E1!1, E2!1)) * f!1))=(phi(E1!1) * f!1)" )"1" (apply-extensionality :hide? t)"1" (hide-all-but 1) (("1" (grind) nil nil )) nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil )"set" sets nil )"bool" indefinite_integral nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil measure_space_def nil )"bool" measure_space_def nil )"sigma_algebra" indefinite_integral nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )set type-eq-decl nil sets nil )nil indefinite_integral nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"measure_type" indefinite_integral nil )nil generalized_measure_defnil )"bool" generalized_measure_def nil )nil extended_nnreal"extended_nnreal/" )nil real_types nil )"bool" reals nil )"nat" measure_space nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[T -> real]" real_fun_ops "reals/" )nil integral nil )"bool" integral nil )nil integral nil )"measurable_set[T, S]" nil )"real" reals nil )"real" reals nil )"bool" sets nil )"[T, T -> boolean]" equalities nil ))nil ))nil 3431890731"" (skosimp)"" (typepred "f!1" )"" (expand "integrable?" )"" "indefinite_integrable" "E" "E2!1" "f" "phi(union(E1!1, E2!1)) * f!1" ))"1" "(phi(E2!1) * (phi(union(E1!1, E2!1)) * f!1))=(phi(E2!1) * f!1)" )"1" (apply-extensionality :hide? t)"1" (hide-all-but 1) (("1" (grind) nil nil )) nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil )"set" sets nil )"bool" indefinite_integral nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil measure_space_def nil )"bool" measure_space_def nil )"sigma_algebra" indefinite_integral nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )set type-eq-decl nil sets nil )nil indefinite_integral nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"measure_type" indefinite_integral nil )nil generalized_measure_defnil )"bool" generalized_measure_def nil )nil extended_nnreal"extended_nnreal/" )nil real_types nil )"bool" reals nil )"nat" measure_space nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[T -> real]" real_fun_ops "reals/" )nil integral nil )"bool" integral nil )nil integral nil )"measurable_set[T, S]" nil )"real" reals nil )"real" reals nil )"bool" sets nil )"[T, T -> boolean]" equalities nil ))nil ))nil 3391226462"" (skosimp*)"" (expand "integral" )"" "phi(union(E1!1, E2!1)) = phi(E1!1)+phi(E2!1)" )"1" (expand "*" 1 1)"1" (expand "+" 1 1)"1" "integral_add" "f1" "phi(E1!1) * f!1" "f2" "phi(E2!1) * f!1" ))"1" (expand "+" -1 1)"1" (expand "*" -1 1)"1" (expand "*" -1 1) (("1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (apply-extensionality :hide? t)"1" (expand "disjoint?" )"1" (expand "empty?" )"1" (inst - "x!1" ) (("1" (grind) nil nil )) nil ))nil ))nil )"2" (hide -1) (("2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"real" indefinite_integral nil )"bool" sets nil )"set" sets nil )"bool" sets nil )"nonneg_int" nil )"measurable_set" nil )"real" reals nil )"bool" sets nil )AND const-decl "[bool, bool -> bool]" booleans nil )"measurable_set[T, S]" indefinite_integralnil )"measurable_set[T, S]" indefinite_integralnil )"[T -> real]" real_fun_ops "reals/" )"measure_type" indefinite_integral nil )nil generalized_measure_defnil )"bool" generalized_measure_def nil )nil extended_nnreal"extended_nnreal/" )nil real_types nil )"bool" indefinite_integral nil )nil integral nil )"bool" integral nil )nil integral nil )"[T -> real]" real_fun_ops "reals/" )nil measure_space_def nil )"bool" measure_space_def nil )"set" sets nil )"nat" measure_space nil )"sigma_algebra" indefinite_integral nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )set type-eq-decl nil sets nil )nil booleans nil )"[T, T -> boolean]" equalities nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil indefinite_integral nil )"measurable_set[T, S]" nil ))nil 3431890731"" (skosimp)"" (typepred "f!1" )"" (expand "integrable?" )"" "indefinite_integrable" "E" "E1!1" "f" "phi(E2!1) * f!1" ))"1" "(phi(E1!1) * (phi(E2!1) * f!1))=(phi(E1!1) * f!1)" )"1" (hide-all-but (-3 1))"1" (apply-extensionality :hide? t)"1" (expand "subset?" )"1" (inst - "x!1" ) (("1" (grind) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil )"bool" indefinite_integral nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil measure_space_def nil )"bool" measure_space_def nil )"sigma_algebra" indefinite_integral nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )set type-eq-decl nil sets nil )nil indefinite_integral nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"measure_type" indefinite_integral nil )nil generalized_measure_defnil )"bool" generalized_measure_def nil )nil extended_nnreal"extended_nnreal/" )nil real_types nil )"bool" reals nil )"nat" measure_space nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[T -> real]" real_fun_ops "reals/" )nil integral nil )"bool" integral nil )nil integral nil )"bool" sets nil )"real" reals nil )"bool" sets nil )"real" reals nil )"(partial_order?[set[T]])" nil )"[T, T -> boolean]" equalities nil ))nil ))nil 3391226795"" (skosimp)"" "indefinite_union" "f" "f!1" "E1" "E1!1" "E2" "difference(E2!1,E1!1)" ))"1" (rewrite "difference_disjoint" )"1" (lemma "union_diff_subset" ("a" "E1!1" "b" "E2!1" ))"1" (assert )"1" (replace -1)"1" (hide -1 -3)"1" (name-replace "INT1" "integral(E1!1, f!1)" )"1" (name-replace "INT2" "integral(E2!1, f!1)" )"1" (typepred "f!1" )"1" (expand "integrable?" )"1" "indefinite_integrable" "E" "difference(E2!1, E1!1)" "f" "phi(E2!1) * f!1" ))"1" "phi(difference(E2!1, E1!1)) * (phi(E2!1) * f!1)=phi(difference(E2!1, E1!1))*f!1" )"1" (hide -1)"1" expand "integral" )"1" "integral_ae_le" "f1" "lambda x: 0" "f2" "phi(difference(E2!1, E1!1)) * f!1" ))"1" "1" rewrite "integral_zero" )"1" (assert ) nil nil ))nil )"2" "2" expand "ae_nonneg?" )"2" expand "ae_le?" )"2" expand "pointwise_ae?" )"2" expand "ae?" )"2" expand "fullset" )"2" expand "ae_in?" )"2" "2" "E!1" )"2" "2" "x!1" )"2" assert )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "integrable_zero" )nil nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" "2" (grind) nil nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (typepred "f!1" )"2" (hide 2 -3)"2" (expand "integrable?" )"2" (lemma "union_diff_subset" ("a" "E1!1" "b" "E2!1" ))"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"set" sets nil )"bool" indefinite_integral nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )"set" sets nil )nil measure_space_def nil )"bool" measure_space_def nil )"sigma_algebra" indefinite_integral nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil indefinite_integral nil )nil indefinite_integral nil )"measurable_set[T, S]" nil )"measurable_set[T, S]" nil )nil sets_lemmas nil )"real" indefinite_integral nil )"[T, T -> boolean]" equalities nil )NOT const-decl "[bool -> bool]" booleans nil )"measure_type" indefinite_integral nil )nil generalized_measure_defnil )"bool" generalized_measure_def nil )nil extended_nnreal"extended_nnreal/" )nil real_types nil )"bool" reals nil )"nat" measure_space nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[T -> real]" real_fun_ops "reals/" )nil integral nil )"bool" integral nil )nil integral nil )nil integral nil )"bool" measure_theory nil )"measurable_set[T, S]" nil )"(S)" indefinite_integralnil )"bool" measure_theory nil )"bool" measure_theory nil )nil measure_theory nil )"bool" measure_theory nil )"bool" booleans nil )"real" reals nil )"real" reals nil )"bool" sets nil )"set" sets nil )"bool" measure_theory nil )"bool" measure_theory nil )nil integral nil )nil integral nil )"real" reals nil )"(partial_order?[set[T]])" nil )"(total_order?[real])" nil )nil sets_lemmas nil ))nil 3431890731"" (skosimp)"" (expand "integrable?" )"" (typepred "N!1" )"" "integral_ae_eq" "f" "lambda x: 0" "h" "phi(N!1) * h!1" ))"1" (assert )"1" (hide 2)"1" (expand "ae_eq?" )"1" (expand "restrict" )"1" (expand "pointwise_ae?" )"1" (expand "*" )"1" (expand "phi" )"1" (expand "member" )"1" (expand "ae?" )"1" (expand "fullset" )"1" expand "ae_in?" )"1" "N!1" )"1" "1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (rewrite "prod_measurable" )"2" (lemma "phi_is_simple" ("X" "N!1" ))"1" (expand "simple?" ) (("1" (propax) nil nil )) nil )"2" (expand "null_set?" )"2" (expand "measurable_set?" )"2" (flatten) nil nil )) nil ))nil ))nil ))nil ))nil )"3" (rewrite "integrable_zero" ) nil nil ))nil ))nil ))nil ))nil )"bool" indefinite_integral nil )"nat" measure_space nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[T -> real]" real_fun_ops "reals/" )nil measure_space_defnil )"bool" measure_space_def nil )nil integral nil )"bool" integral nil )nil integral nil )"R" restrict nil )"bool" sets nil )"set" sets nil )nil measure_theory nil )"bool" measure_theory nil )"real" reals nil )"bool" measure_theory nil )"bool" measure_theory nil )"(S)" indefinite_integralnil )"measurable_set[T, S]" nil )"bool" measure_theory nil )"bool" measure_theory nil )nil measure_space nil )"bool" measure_space_def nil )"bool" measure_space nil )nil measure_space nil )nil integral nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil indefinite_integral nil )set type-eq-decl nil sets nil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def nil )nil subset_algebra_def nil )"sigma_algebra" indefinite_integral nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil real_types nil )nil extended_nnreal"extended_nnreal/" )"bool" generalized_measure_def nil )nil generalized_measure_defnil )"measure_type" indefinite_integral nil )"bool" measure_theory nil )nil measure_theory nil ))nil ))nil 3391223142"" (skosimp)"" "integral_ae_eq" ("f" "lambda x: 0" "h" "phi(N!1)* h!1" ))"1" (rewrite "integral_zero" )"1" (expand "integral" +)"1" (assert )"1" (hide 2)"1" (typepred "N!1" )"1" (expand "ae_eq?" )"1" (expand "restrict" )"1" (expand "pointwise_ae?" )"1" (expand "ae?" )"1" (expand "fullset" )"1" (expand "ae_in?" )"1" (inst + "N!1" )"1" "1" "1" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (rewrite "prod_measurable" )"2" (lemma "phi_is_simple" ("X" "N!1" ))"1" (expand "simple?" ) (("1" (propax) nil nil )) nil )"2" (typepred "N!1" )"2" (expand "null_set?" )"2" (expand "measurable_set?" )"2" (flatten) nil nil )) nil ))nil ))nil ))nil ))nil )"3" (rewrite "integrable_zero" ) nil nil ))nil ))nil )"measure_type" indefinite_integral nil )nil generalized_measure_defnil )"bool" generalized_measure_def nil )nil extended_nnreal"extended_nnreal/" )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" indefinite_integral nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )nil booleans nil )nil booleans nil )nil indefinite_integral nil )nil measure_theory nil )"bool" measure_theory nil )"nat" measure_space nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )set type-eq-decl nil sets nil )"[T -> real]" real_fun_ops "reals/" )nil measure_space_defnil )"bool" measure_space_def nil )nil integral nil )"bool" integral nil )nil integral nil )"real" indefinite_integral nil )"bool" measure_theory nil )"bool" measure_theory nil )"set" sets nil )nil measure_theory nil )"bool" measure_theory nil )"real" reals nil )"bool" sets nil )"real" reals nil )"bool" measure_theory nil )"bool" measure_theory nil )"(S)" indefinite_integralnil )"measurable_set[T, S]" nil )"R" restrict nil )NOT const-decl "[bool -> bool]" booleans nil )nil integral nil )nil measure_space nil )"bool" measure_space nil )"bool" measure_space_def nil )nil measure_space nil )nil integral nil ))nil 3454503117"" (subtype-tcc) nil nil )"sigma_algebra" indefinite_integral nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )nil booleans nil )nil booleans nil )nil indefinite_integral nil )"bool" measure_space_def nil ))nil ))nil 3454503117"" (skosimp)"" (expand "integrable?" )"" (rewrite "indefinite_integrable" )"" (expand "measurable_set?" ) (("" (propax) nil nil )) nil ))nil ))nil ))nil )"measurable_function[T, S]" nil )"bool" indefinite_integral nil )"simple" indefinite_integralnil )"measure_type" indefinite_integral nil )nil generalized_measure_defnil )"bool" generalized_measure_def nil )nil extended_nnreal"extended_nnreal/" )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" indefinite_integral nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )nil booleans nil )nil booleans nil )nil indefinite_integral nil )nil integral nil )"bool" integral nil )nil nil )"bool" nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil measure_space_def nil )"bool" measure_space_def nil )set type-eq-decl nil sets nil )nil integral nil ))nil ))nil 3454503117"" (skosimp)"" (typepred "S" )"" (rewrite "measurable_IUnion" )"" (skolem + "n!1" )"" (expand "measurable_set?" ) (("" (propax) nil nil )) nil ))nil ))nil ))nil ))nil )"sigma_algebra" indefinite_integral nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )nil indefinite_integral nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"(S)" nil )nil nil )"bool" nil )nil sequences nil )nil measure_space_def nil )"bool" measure_space_def nil )set type-eq-decl nil sets nil )nil naturalnumbers nil )"bool" reals 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 numbers nil )nil measure_space_def nil ))nil ))nil 3454503117"" (skosimp)"" (lemma "indefinite_countably_additive_TCC3" ("DX" "DX!1" ))"" (expand "integrable?" )"" (rewrite "indefinite_integrable" ) nil nil )) nil ))nil ))nil )nil nil )"bool" nil )"sigma_algebra" indefinite_integral nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )nil indefinite_integral 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 nil )"(S)" nil )nil integral nil )set type-eq-decl nil sets nil )"bool" measure_space_def nil )nil measure_space_def nil )"set[T]" indexed_sets nil )"bool" integral nil )nil integral nil )nil real_types nil )nil extended_nnreal"extended_nnreal/" )"bool" generalized_measure_def nil )nil generalized_measure_defnil )"measure_type" indefinite_integral nil )"bool" indefinite_integral nil )"measurable_function[T, S]" nil ))nil ))nil 3454503117"" case "FORALL (DX: disjoint_indexed_measurable[T, S], LAMBDA n: integral(DX(n), f)),") "1" (skosimp)"1" (inst-cp - "DX!1" "minus(f!1)" )"1" (inst - "DX!1" "plus(f!1)" )"1" (split)"1" (split)"1" case "forall (u:sequence[real],l:real): convergence?(u,l) iff convergence(u,l)" )"1" "series(LAMBDA n: integral(DX!1(n), f!1))" "integral(IUnion(DX!1), f!1)" )"1" "series(LAMBDA n: integral(DX!1(n), minus(f!1)))" "integral(IUnion(DX!1), minus(f!1))" )"1" "series(LAMBDA n: integral(DX!1(n), plus(f!1)))" "integral(IUnion(DX!1), plus(f!1))" )"1" (replace -1)"1" (replace -2)"1" (replace -3)"1" (hide -1 -2 -3)"1" "cnv_seq_diff" "s2" "series(LAMBDA n: integral(DX!1(n), minus(f!1)))" "l2" "integral(IUnion(DX!1), minus(f!1))" "s1" "series(LAMBDA n: integral(DX!1(n), plus(f!1)))" "l1" "integral(IUnion(DX!1), plus(f!1))" ))"1" assert )"1" rewrite "series_diff" )"1" expand "-" -1)"1" "(LAMBDA (x: nat): LAMBDA n: integral(DX!1(n), f!1)") "1" "1" "LHS" "series(LAMBDA n: integral(DX!1(n), f!1))" )"1" "1" rewrite "indefinite_diff" "1" "plus(f!1) - minus(f!1)=f!1" )"1" "1" "1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "integrable?" )"2" rewrite "indefinite_integrable" )"2" expand "measurable_set?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "1" "1" "indefinite_diff" "E" "DX!1(x!1)" "f1" "plus(f!1)" "f2" "minus(f!1)" ))"1" replace -1 1 rl)"1" "plus(f!1) - minus(f!1)=f!1" )"1" "1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "integrable?" )"2" rewrite "indefinite_integrable" )"2" expand "measurable_set?" )"2" nil nil ))nil ))nil ))nil ))nil )"3" "3" expand "integrable?" )"3" rewrite "indefinite_integrable" )"3" expand "measurable_set?" )"3" nil nil ))nil ))nil ))nil ))nil )"4" "4" expand "integrable?" )"4" rewrite "indefinite_integrable" )"4" expand "measurable_set?" )"4" nil nil ))nil ))nil ))nil ))nil )"5" "5" expand "measurable_set?" )"5" (propax) nil nil ))nil ))nil ))nil )"3" "3" expand "integrable?" )"3" rewrite "indefinite_integrable" )"3" expand "measurable_set?" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "integrable?" )"2" rewrite "indefinite_integrable" )"2" expand "measurable_set?" )"2" (propax) nil nil ))nil ))nil ))nil ))nil )"3" "3" expand "integrable?" )"3" rewrite "indefinite_integrable" )"3" expand "measurable_set?" )"3" (propax) nil nil ))nil ))nil ))nil ))nil )"4" "4" expand "measurable_set?" )"4" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp)"2" (expand "integrable?" )"2" (rewrite "indefinite_integrable" )"2" (expand "measurable_set?" )"2" (propax) nil nil )) nil ))nil ))nil ))nil )"3" (expand "measurable_set?" )"3" (propax) nil nil )) nil ))nil )"2" (skosimp)"2" (expand "integrable?" )"2" (rewrite "indefinite_integrable" )"2" (expand "measurable_set?" )"2" (propax) nil nil )) nil ))nil ))nil ))nil )"3" (skosimp)"3" (expand "measurable_set?" )"3" (propax) nil nil )) nil ))nil ))nil )"2" (skosimp)"2" (expand "integrable?" )"2" (rewrite "indefinite_integrable" )"2" (expand "measurable_set?" )"2" (propax) nil nil )) nil ))nil ))nil ))nil )"3" (expand "measurable_set?" )"3" (propax) nil nil )) nil ))nil )"2" (hide-all-but 1)"2" (skosimp*)"2" (rewrite "metric_convergence_def" )"2" (expand "metric_converges_to" )"2" (expand "convergence" )"2" (expand "member" )"2" (expand "ball" )"2" "1" "1" "epsilon!1" )"1" "1" "n!1" )"1" "1" "i!1" )"1" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "r!1" )"2" "2" "n!1" )"2" "2" "i!1" )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (expand "ae_nonneg?" )"2" (expand "pointwise_ae?" )"2" (expand "ae?" )"2" (expand "ae_in?" )"2" (inst + "emptyset" )"2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (expand "ae_nonneg?" )"2" (expand "pointwise_ae?" )"2" (expand "ae?" )"2" (expand "ae_in?" )"2" (inst + "emptyset" ) (("2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp)"2" (lemma "increasing_IUnion" ("A" "DX!1" ))"2" (skosimp)"2" case "forall n: S(B!1(n)) & measurable_set?(B!1(n)) & B!1(n) = IUnion(n,DX!1)" )"1" "monotone_convergence" "F" "lambda n: phi(B!1(n))*f!1" ))"1" (split)"1" (flatten)"1" (hide -1 -2)"1" (inst - "phi(IUnion(DX!1))*f!1" )"1" (split)"1" (expand "converges_upto?" )"1" (expand "o " )"1" "1" "series(LAMBDA n: integral(DX!1(n), f!1))=LAMBDA n: integral(phi(B!1(n)) * f!1)" )"1" expand "integral" 1 2)"1" (propax) nil nil ))nil )"2" "2" rewrite "extensionality_postulate" "1" "1" "x" )"1" expand "series" )"1" expand "sigma" )"1" expand "sigma" )"1" expand "integral" "1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" expand "series" )"2" expand "sigma" 1)"2" replace -1)"2" "2" "indefinite_union" "E1" "B!1(j!1)" "E2" "DX!1(1+j!1)" "f" "f!1" ))"1" "1" "j!1" )"1" replace "1" replace "1" expand "integral" "1" expand "integral" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "j!1" )"2" "2" "2" replace "2" "2" "DX!1" )"2" expand "disjoint_indexed_measurable?" )"2" expand "disjoint?" )"2" expand "disjoint?" )"2" expand "intersection" )"2" expand "empty?" )"2" expand "member" )"2" "2" expand "IUnion" )"2" expand "image" )"2" expand "Union" )"2" "2" "a!1" )"2" "n!2" )"2" replace "2" "2" "n!2" "1+j!1" )"2" assert )"2" "x!1" )"2" assert )nil nil ))nil ))nil ))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" expand "integrable?" )"2" rewrite "indefinite_integrable" "2" "j!1" )"2" "j!1+1" )"2" expand "measurable_set?" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"3" "j!1" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "x!2" )"3" "3" rewrite "indefinite_integrable" )nil nil ))nil ))nil ))nil )"4" "4" expand "integrable?" )"4" rewrite "indefinite_integrable" )"4" expand "measurable_set?" )"4" nil nil ))nil ))nil ))nil ))nil )"5" expand "measurable_set?" )"5" (propax) nil nil ))nil ))nil ))nil )"2" "2" expand "integrable?" )"2" rewrite "indefinite_integrable" )"2" expand "measurable_set?" )"2" (propax) nil nil ))nil ))nil ))nil ))nil )"3" expand "measurable_set?" )"3" (propax) nil nil ))nil ))nil ))nil )"3" "3" expand "integrable?" )"3" rewrite "indefinite_integrable" )"3" expand "measurable_set?" )"3" (propax) nil nil ))nil ))nil ))nil ))nil )"4" "4" expand "measurable_set?" )"4" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (replace -5)"2" "2" expand "ae_convergence?" )"2" expand "fullset" )"2" expand "ae_convergence_in?" )"2" expand "ae_in?" )"2" "emptyset" )"2" expand "member" )"2" "2" "2" "2" expand "*" )"2" expand "phi" )"2" expand "member" )"2" rewrite "metric_convergence_def" )"2" expand "metric_converges_to" )"2" "2" "IUnion(B!1)(x!1)" )"1" expand "IUnion" )"1" "1" "i!1" )"1" "1" expand "increasing?" )"1" "i!1" "i!2" )"1" assert )"1" expand "subset?" )"1" "x!1" )"1" expand "ball" )"1" expand "member" )"1" assert )"1" expand "abs" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "0" )"2" "2" "B!1(i!1)(x!1)" )"1" expand "IUnion" )"1" "i!1" )nil nil ))nil )"2" assert )"2" expand "ball" )"2" expand "abs" )"2" assert )nil nil ))nil ))nil ))nil ))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" (rewrite "indefinite_integrable" ) nil nil ))nil ))nil ))nil )"2" (expand "ae_increasing?" )"2" (hide 2 -3 -4 -5)"2" (expand "ae_nonneg?" )"2" (expand "pointwise_ae?" )"2" (expand "ae?" )"2" (expand "fullset" )"2" expand "ae_in?" )"2" "2" "E!1" )"2" "2" expand "member" )"2" "x!1" )"2" "2" assert )"2" expand "*" )"2" expand "increasing?" )"2" "i!1" "j!1" )"2" assert )"2" expand "phi" )"2" expand "member" )"2" "B!1(i!1)(x!1)" )"1" expand "subset?" )"1" "x!1" )"1" assert )"1" assert )nil nil ))nil ))nil ))nil )"2" assert )"2" "2" "1" assert )nil nil )"2" assert )nil nil ))nil ))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" (skosimp)"2" (rewrite "indefinite_integrable" )"2" (inst - "n!1" ) (("2" (flatten) nil nil ))nil ))nil ))nil ))nil )"2" (hide -5 2 -4)"2" (induct "n" )"1" (assert ) nil nil )"2" (assert )"2" (expand "measurable_set?" )"2" (assert ) nil nil )) nil ))nil )"3" (rewrite "IUnion_0_def" ) nil nil )"4" (skosimp*)"4" (inst -6 "j!1" )"4" (replace -6)"4" "measurable_union" "a" "B!1(j!1)" "b" "DX!1(j!1+1)" ))"1" (expand "measurable_set?" )"1" (assert )"1" rewrite "IUnion_n_def" )"1" replace -4 * rl)"1" (propax) nil nil ))nil ))nil ))nil ))nil )"2" (expand "measurable_set?" )"2" (propax) nil nil )) nil )"3" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (skosimp*)"3" (expand "integrable?" )"3" (rewrite "indefinite_integrable" )"3" (expand "measurable_set?" ) (("3" (propax) nil nil ))nil ))nil ))nil ))nil )"4" (skosimp*)"4" (expand "measurable_set?" ) (("4" (propax) nil nil )) nil ))nil )"5" (skosimp)"5" (skosimp)"5" (expand "integrable?" )"5" (rewrite "indefinite_integrable" )"5" (expand "measurable_set?" ) (("5" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"6" (expand "measurable_set?" ) (("6" (propax) nil nil )) nil ))nil )nil nat_indexed_sets "sets_aux/" )"set[T]" nat_indexed_sets "sets_aux/" )"T3" function_props nil )"real" integral nil )nil functions nil )"sequence[set[T]]" indefinite_integral nil )nil defined_types nil )nil naturalnumbers nil )"real" sigma "reals/" )"posint" nil )nil indefinite_integral nil )"[numfield, numfield -> numfield]" number_fields nil )"set" sets nil )"bool" sets nil )"bool" indexed_sets_aux "sets_aux/" )"set" sets nil )"set" sets nil ) (<= const-decl "bool" reals nil )"set[R]" function_image nil )"bool" sets nil )"(S)" nil )"real" reals nil )"odd_int" integersnil )"int" integers nil )"posint" nil )"bool" convergence_aux "metric_space/" )"bool" measure_theory nil )"bool" measure_theory nil )"bool" booleans nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"[numfield, numfield -> numfield]" number_fields nil )"real" reals nil )"bool" fun_preds_partial "structures/" )"(total_order?[real])" nil )"metric_open[real, (LAMBDA (x, y: real): abs(x - y))]" "metric_space/" )nil abs_lems "reals/" )"bool" sets nil )"integrable[T, S, m]" indefinite_integralnil )"disjoint_indexed_measurable[T, S]" nil )"(partial_order?[set[T]])" nil )"bool" measure_theory nil )"nat" measure_space nil )"[T -> real]" real_fun_ops "reals/" )nil integral_convergence nil )nil nat_indexed_sets "sets_aux/" )nil measure_space_def nil )"int" integers nil )"even_int" integersnil )"even_int" integersnil )nil nat_indexed_sets "sets_aux/" )"integrable" nil )"measurable_function[T, S]" nil )"[T -> nnreal]" real_fun_ops_aux "reals/" )nil metric_space"metric_space/" )"set[T]" metric_space_def "metric_space/" )"(total_order?[real])" nil )"bool" reals nil )nil real_types nil )"bool" sets nil )"bool" metric_space_def"metric_space/" )"disjoint_indexed_measurable[T, S]" nil )"integrable[T, S, m]" indefinite_integralnil )"[T -> real]" real_fun_ops "reals/" )nil integral nil )"simple" indefinite_integralnil )"measurable_function[T, S]" nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"integrable" nil )nil indefinite_integral nil )"[T, T -> boolean]" equalities nil )nil series "series/" )nil convergence_ops "analysis/" )"bool" convergence_sequences "analysis/" )"[bool, bool -> bool]" booleans nil )"measurable_set[T, S]" nil )"(S)" indefinite_integralnil )"bool" measure_theory nil )"(S)" indefinite_integralnil )"null_set" indefinite_integral nil )"finite_set[T]" sigma_countable"sigma_set/" )"finite_set[T]" countable_setofsets"sets_aux/" )"finite_set[T]" countable_props"sets_aux/" )"finite_set" finite_sets nil )"set" sets nil )nil measure_theory nil )"bool" measure_theory nil )"set" sets nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" measure_theory nil )"bool" measure_theory nil )"[T -> nnreal]" real_fun_ops_aux "reals/" )"measurable_function[T, S]" nil )"integrable" nil )"(S)" nil )"real" reals nil )"second_countable" real_topology "metric_space/" )"hausdorff[real]" "metric_space/" )"(hausdorff?)" "metric_space/" )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )nil indefinite_integral nil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def nil )nil subset_algebra_def nil )"sigma_algebra" indefinite_integral nil )"bool" nil )nil nil )nil real_types nil )nil extended_nnreal"extended_nnreal/" )"bool" generalized_measure_def nil )nil generalized_measure_defnil )"measure_type" indefinite_integral nil )"bool" integral nil )nil integral nil )"[bool, bool -> bool]" booleans nil )"bool" measure_theory nil )nil sequences 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/" )"bool" topological_convergence"topology/" )"sequence[real]" series "series/" )nil measure_space_def nil )set type-eq-decl nil sets nil )"bool" measure_space_def nil )"bool" indefinite_integral nil )"real" indefinite_integral nil )"set[T]" indexed_sets nil ))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Dauer der Verarbeitung: 0.207 Sekunden
(vorverarbeitet am 2026-05-06)
¤ *© Formatika GbR, Deutschland
2026-05-26
