Impressum integral.prf
Sprache: Lisp
(integralnil 3390735612"" (expand "integrable?" )"" (lemma "nn_integrable_zero" )"" (inst + "lambda x: 0" "lambda x: 0" )"" (apply-extensionality 1 :hide? t)"" (expand "-" ) (("" (propax) nil nil )) nil )) nil ))nil ))nil ))nil )"measure_type" 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" 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 integral nil )nil nn_integral nil )"[T -> real]" real_fun_ops "reals/" )nil nn_integral nil )"bool" nn_integral nil )"bool" integral nil ))nil ))nil 3391020617"" (skosimp)"" (typepred "x!1" )"" (expand "integrable?" )"" (inst + "x!1" "lambda x: 0" )"1" (apply-extensionality :hide? t)"1" (expand "-" ) (("1" (propax) nil nil )) nil )"2" (skosimp)"2" (expand "-" ) (("2" (assert ) nil nil )) nil )) nil ))nil )"2" (rewrite "nn_integrable_zero" ) nil nil ))nil ))nil ))nil ))nil )nil nn_integral nil )"bool" nn_integral nil )"measure_type" integral nil )nil generalized_measure_defnil )"bool" generalized_measure_def nil )nil extended_nnreal"extended_nnreal/" )"sigma_algebra" integral nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )nil real_types nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil integral nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"(total_order?[real])" nil )"nn_integrable" integral nil )"[T -> real]" real_fun_ops "reals/" )nil nn_integral nil )"bool" integral nil ))nil ))nil 3391430136"" (skosimp)"" (expand "integrable?" )"" (inst + "plus(x!1)" "minus(x!1)" )"1" (lemma "plus_minus_def" ("f" "x!1" ))"1" (propax) nil nil )) nil )"2" (lemma "isf_minus" ("i" "x!1" ))"2" (assert )"2" (lemma "nn_isf_is_nn_integrable" )"2" (inst - "minus[T](x!1)" )"1" (flatten) nil nil )"2" (expand "nn_isf?" )"2" (hide-all-but 1) (("2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"3" (lemma "isf_plus" ("i" "x!1" ))"3" (assert )"3" (lemma "nn_isf_is_nn_integrable" )"3" (inst - "plus[T](x!1)" )"1" (flatten) nil nil )"2" (hide 2)"2" (expand "nn_isf?" )"2" (hide -1) (("2" (grind) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" integral nil )nil isf nil )"(strict_total_order?[real])" real_props nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )nil isf nil )nil nn_integral nil )"real" reals nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"(strict_total_order?[real])" real_props nil )nil nn_integral nil )"bool" nn_integral nil )nil real_fun_ops_aux "reals/" )nil nn_integral nil )"[T -> nnreal]" real_fun_ops_aux "reals/" )nil integral nil )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 )"bool" reals nil )nil real_types nil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def nil )nil subset_algebra_def nil )"sigma_algebra" integral nil )nil extended_nnreal"extended_nnreal/" )"bool" generalized_measure_def nil )nil generalized_measure_defnil )"measure_type" integral nil )"bool" nn_integral nil )"[T -> nnreal]" real_fun_ops_aux "reals/" )"bool" isf nil )nil isf nil )"isf" integral nil )"isf" integral nil )"isf[T, S, m]" integral nil ))nil ))nil 3395201756"" (skosimp)"" (lemma "nn_integrable_is_measurable" )"" (typepred "x!1" )"" (expand "integrable?" )"" (skosimp)"" (replace -1)"" (inst-cp - "g!1" )"" (inst - "h!1" )"" (rewrite "diff_measurable" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"measure_type" 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" 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 integral nil )nil nn_integral nil )nil measure_space_def nil )"bool" measure_space_def nil )nil measure_space_defnil )"bool" nn_integral nil )nil nn_integral nil )nil integral nil )"bool" integral nil )NOT const-decl "[bool -> bool]" booleans nil ))nil ))nil 3395200583"" (skosimp)"" (lemma "nn_integral_add" ("f1" "g1!1" "f2" "g4!1" ))"" (lemma "nn_integral_add" ("f1" "g2!1" "f2" "g3!1" ))"" (case-replace "g2!1 + g3!1=g1!1 + g4!1" )"1" (assert ) nil nil )"2" (apply-extensionality 1 :hide? t)"2" "extensionality_postulate" "f" "g1!1 - g3!1" "g" "g2!1 - g4!1" ))"2" (replace -1 -4 rl)"2" (inst -4 "x!1" )"2" (hide-all-but (-4 1)) (("2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"measure_type" 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" 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 integral nil )nil nn_integral nil )"bool" nn_integral nil )nil nn_integral nil )"nn_integrable" integralnil )"[T, T -> boolean]" equalities nil )"[T -> real]" real_fun_ops "reals/" )"nnreal" nil )"measurable_function[T, S]" nil )"real" reals nil )nil functions nil )"[T -> real]" real_fun_ops "reals/" ))nil 3391020617"" (skosimp)"" (typepred "f1!1" )"" (typepred "f2!1" )"" (expand "integrable?" )"" (skosimp*)"" (inst + "g!1+g!2" "h!1+h!2" )"" (apply-extensionality 1 :hide? t)"" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )nil integral nil )"bool" integral nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil integral nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"nn_integrable" integralnil )"bool" reals nil )nil real_types nil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def nil )nil subset_algebra_def nil )"sigma_algebra" integral nil )nil extended_nnreal"extended_nnreal/" )"bool" generalized_measure_def nil )nil generalized_measure_defnil )"measure_type" integral nil )"bool" nn_integral nil )nil nn_integral nil )"[T -> real]" real_fun_ops "reals/" )"real" reals nil )"nnreal" nil )"real" reals nil )"measurable_function[T, S]" nil )"measurable_function[T, S]" nil )"[T -> real]" real_fun_ops "reals/" ))nil ))nil 3391020617"" (skosimp)"" (typepred "f!1" )"" (expand "integrable?" )"" (skosimp)"" (case "c!1>=0" )"1" (inst + "c!1*g!1" "c!1*h!1" )"1" (apply-extensionality :hide? t)"1" (grind) nil nil )) nil )"2" (split)"1" (skosimp)"1" (expand "*" )"1" "le_times_le_pos" "nnx" "0" "y" "c!1" "nnz" "0" "w" "h!1(x1!1)" ))"1" (assert ) nil nil )) nil ))nil ))nil )"2" (typepred "h!1" )"2" "nn_integrable_scal" ("c" "c!1" "f" "h!1" ))"1" (flatten) nil nil ) ("2" (propax) nil nil ))nil ))nil ))nil )"3" (split)"1" (skosimp)"1" "nn_integrable_scal" ("c" "c!1" "f" "g!1" ))"1" (flatten) (("1" (inst - "x1!1" ) nil nil ))nil )"2" (propax) nil nil ))nil ))nil )"2" "nn_integrable_scal" ("c" "c!1" "f" "g!1" ))"1" (flatten) nil nil ) ("2" (propax) nil nil ))nil ))nil ))nil )"2" (inst + "-c!1*h!1" "-c!1*g!1" )"1" (replace -1)"1" (hide-all-but 2)"1" (apply-extensionality :hide? t)"1" (grind) nil nil )) nil ))nil ))nil )"2" (split)"1" (hide -1)"1" (skosimp)"1" (grind)"1" "both_sides_times_pos_le1" "pz" "-c!1" "x" "0" "y" "g!1(x1!1)" ))"1" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" "nn_integrable_scal" ("c" "-c!1" "f" "g!1" ))"1" (flatten) nil nil ) ("2" (assert ) nil nil ))nil ))nil )"3" (split)"1" (skosimp)"1" "both_sides_times_pos_le1" "pz" "-c!1" "x" "0" "y" "h!1(x1!1)" ))"1" (assert ) (("1" (grind) nil nil )) nil )"2" (assert ) nil nil ))nil ))nil )"2" "nn_integrable_scal" ("c" "-c!1" "f" "h!1" ))"1" (flatten) nil nil ) ("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil integral nil )"bool" integral nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil integral nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"real" reals nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"(strict_total_order?[real])" real_props nil )nil real_types nil )"bool" reals nil )nil real_props nil )"measurable_function[T, S]" nil )"nn_integrable" integral nil )nil nn_integral nil )"bool" nn_integral nil )"measure_type" integral nil )nil generalized_measure_defnil )"bool" generalized_measure_def nil )nil extended_nnreal"extended_nnreal/" )"sigma_algebra" integral nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )nil real_types nil )"real" integral nil )"[T -> real]" real_fun_ops "reals/" )AND const-decl "[bool, bool -> bool]" booleans nil )"nn_integrable" integral nil )"real" reals nil )"real" reals nil )"(total_order?[real])" nil )"measurable_function[T, S]" nil )"[T -> real]" real_fun_ops "reals/" )nil nn_integral nil )nil real_props nil )nil real_types nil )"(total_order?[real])" nil )"bool" reals nil ))nil ))nil 3391020617"" (skosimp)"" (typepred "f!1" )"" (lemma "integrable_scal" ("c" "-1" "f" "f!1" ))"" (expand "*" )"" (expand "-" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )nil integral nil )"bool" integral nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil integral nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"[T -> real]" real_fun_ops "reals/" )"real" reals nil )"[T -> real]" real_fun_ops "reals/" )"real" reals nil )"odd_int" integers nil )nil integral nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil ))nil ))nil 3391142033"" (skosimp)"" (lemma "integrable_opp" ("f" "f2!1" ))"" (lemma "integrable_add" ("f1" "f1!1" "f2" "-f2!1" ))"" (case-replace "(+[T])(f1!1, -f2!1)=(-[T])(f1!1, f2!1)" )"" (apply-extensionality 1 :hide? t)"" (expand "+" )"" (expand "-" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )nil integral nil )"bool" integral 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 integral nil )nil integral nil )"[T -> real]" real_fun_ops "reals/" )"[T -> real]" real_fun_ops "reals/" )"[T, T -> boolean]" equalities nil )"measurable_function[T, S]" nil )"integrable" integral nil )"real" reals nil )"real" reals nil )"real" reals nil )"integrable" integral nil )nil integral nil )"[T -> real]" real_fun_ops "reals/" ))nil ))nil 3391332663"" (rewrite "integrable_TCC1" ) nil nil )nil integral nil )) shostak))nil 3391183431"" (skosimp)"" (typepred "f!1" )"" (expand "integrable?" )"" (skosimp)"" (expand "integrals" )"" (expand "nonempty?" )"" (expand "empty?" )"" (expand "member" )"" (inst - "nn_integral(g!1)-nn_integral(h!1)" )"" (inst + "g!1" "h!1" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil integral nil )"bool" integral nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil integral nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" sets nil )"bool" sets nil )"nnreal" nn_integral nil )nil nn_integral nil )"bool" nn_integral nil )"measure_type" integral nil )nil generalized_measure_defnil )"bool" generalized_measure_def nil )nil extended_nnreal"extended_nnreal/" )"sigma_algebra" integral nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )nil real_types nil )"bool" reals nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"real" reals nil )"bool" sets nil )"set[real]" integral nil ))nil 3391183368"" (skosimp)"" (lemma "nonempty_integrals" ("f" "f!1" ))"" (expand "nonempty?" )"" (expand "empty?" )"" (skosimp)"" (expand "singleton?" )"" (inst + "x!1" )"1" (skosimp)"1" (typepred "y!1" )"1" (expand "member" )"1" (expand "integrals" )"1" (skosimp*)"1" (replace -2)"1" (replace -4)"1" "1" "nn_integrable_add" "f1" "g!2" "f2" "h!1" ))"1" "nn_integrable_add" "f1" "g!1" "f2" "h!2" ))"1" "1" "nn_integral_add" "f1" "g!2" "f2" "h!1" ))"1" "nn_integral_add" "f1" "g!1" "f2" "h!2" ))"1" assert )"1" "g!1 + h!2=g!2 + h!1" )"1" (assert ) nil nil )"2" "2" "2" "extensionality_postulate" "f" "f!1" "g" "g!1-h!1" ))"2" "extensionality_postulate" "f" "f!1" "g" "g!2-h!2" ))"2" "2" "1" "1" "1" "x!2" )"1" "x!2" )"1" expand "+" )"1" assert )"1" expand "-" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil )"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" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil integral nil )"bool" integral 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 integral nil )nil integral nil )"bool" sets nil )"bool" sets nil )"bool" sets nil )"measure_type" 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" integral nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )nil nn_integral nil )"bool" nn_integral nil )nil nn_integral nil )"[T -> real]" real_fun_ops "reals/" )"[T, T -> boolean]" equalities nil )"[T -> real]" real_fun_ops "reals/" )nil functions nil )"integrable" integral nil )"nn_integrable" integralnil )"nnreal" nil )"integrable" integral nil )"real" reals nil )nil nn_integral nil )NOT const-decl "[bool -> bool]" booleans nil )set type-eq-decl nil sets nil )"set[real]" integral nil )"integrable" integral nil )"real" integral nil )"bool" sets nil ))nil 3391183280"" (skosimp)"" (lemma "nonempty_integrals" ("f" "f!1" ))"" (propax) nil nil )) nil ))nil )nil integral nil )"bool" integral 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 integral nil )nil integral nil ))nil ))nil 3391225798"" (skosimp)"" (typepred "f!1" )"" (expand "integrable?" )"" (skosimp)"" (typepred "g!1" )"" (typepred "h!1" )"" (lemma "nn_integrable_le" ("f" "g!1" "g" "f!1" ))"" (split -1)"1" (flatten) nil nil )"2" (skosimp)"2" (replace -3)"2" (expand "-" )"2" (inst - "x!1" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil integral nil )"bool" integral nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil integral nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"[T -> real]" real_fun_ops "reals/" )"real" reals nil )nil nn_integral nil )"bool" measure_space_def nil )nil measure_space_defnil )"bool" reals nil )nil real_types nil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def nil )nil subset_algebra_def nil )"sigma_algebra" integral nil )nil extended_nnreal"extended_nnreal/" )"bool" generalized_measure_def nil )nil generalized_measure_defnil )"measure_type" integral nil )"bool" nn_integral nil )nil nn_integral nil ))nil 3391166946"" (skosimp)"" (typepred "g!1" )"" (name "CC" "integral(g!1)" )"" (replace -1)"" (expand "integral" )"" (typepred "choose[real](integrals(g!1))" )"" (replace -2)"" (expand "integrals" -1)"" (skosimp)"" "nn_integral_add" ("f1" "g!1" "f2" "h!1" ))"" (replace -3)"" (case "g!2=g!1+h!1" )"1" (assert ) nil nil )"2" (hide-all-but (-2 1))"2" (apply-extensionality :hide? t)"2" replace -1)"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil nn_integral nil )"bool" nn_integral nil )"measure_type" integral nil )nil generalized_measure_defnil )"bool" generalized_measure_def nil )nil extended_nnreal"extended_nnreal/" )"sigma_algebra" integral nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )nil real_types nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil integral nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"(p)" sets nil )"bool" sets nil )"set[real]" integral nil )set type-eq-decl nil sets nil )nil nn_integral nil )"integrable" integral nil )"nn_integrable" integralnil )"[T -> real]" real_fun_ops "reals/" )"nnreal" nil )"integrable" integral nil )"real" reals nil )"real" reals nil )"[T -> real]" real_fun_ops "reals/" )"[T, T -> boolean]" equalities nil )"bool" integral nil )nil integral nil )"real" integral nil ))nil 3391167424"" (lemma "integrable_zero" )"" (lemma "nn_integrable_is_nn_integrable" ("f" "LAMBDA x: 0" ))"1" (split -1)"1" (lemma "integral_nn" ("g" "LAMBDA x: 0" ))"1" (replace -1)"1" (hide -1 -3)"1" (rewrite "nn_integral_zero" ) nil nil )) nil ))nil )"2" (propax) nil nil ))nil )"2" (skosimp) (("2" (assert ) nil nil )) nil ))nil )"2" (propax) nil nil ))nil ))nil )nil integral nil )"bool" integral 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 integral nil )nil integral nil )"(total_order?[real])" nil )nil nn_integral nil )"bool" nn_integral nil )"measure_type" integral nil )nil generalized_measure_defnil )"bool" generalized_measure_def nil )nil extended_nnreal"extended_nnreal/" )"sigma_algebra" integral nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )nil real_types nil )"bool" reals nil )nil integral nil )nil nn_integral nil )nil integral nil ))nil 3391167398"" (skosimp)"" (typepred "F!1" )"" (assert )"" (expand "measurable_set?" ) (("" (propax) nil nil )) nil ))nil ))nil ))nil )"bool" measure_props nil )"measure_type" 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" 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 integral nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil ))nil 3391181089"" (skosimp)"" (lemma "nn_integral_phi" ("F" "F!1" ))"" (rewrite "integral_nn" ) nil nil )) nil ))nil )"measure_type" 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" 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 integral nil )"bool" measure_props nil )nil measure_space_def nil )"bool" measure_space_def nil )set type-eq-decl nil sets nil )nil nn_integral nil )"nat" measure_space nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil nn_integral nil )"bool" nn_integral nil )nil integral nil )"isf" integral nil ))nil 3390735896"" (skosimp)"" (expand "integral" )"" (typepred "choose[real](integrals(f1!1 + f2!1))" )"" (typepred "choose[real](integrals(f2!1))" )"" (typepred "choose[real](integrals(f1!1))" )"" "XY" "choose[real](integrals(f1!1 + f2!1))" )"" (name-replace "X" "choose[real](integrals(f1!1))" )"" (name-replace "Y" "choose[real](integrals(f2!1))" )"" (expand "integrals" )"" (skosimp*)"" (replace -2)"" (replace -4)"" (replace -6)"" (hide -2 -4 -6)"" replace -1)"" replace -2)"" "" "nn_integral_add" "f1" "g!1" "f2" "g!2" ))"" "nn_integral_add" "f1" "h!1" "f2" "h!2" ))"" case "(g!1+g!2)+h!3=(h!1+h!2)+g!3" )"1" "nn_integral_add" "f1" "g!1 + g!2" "f2" "h!3" ))"1" "nn_integral_add" "f1" "h!1 + h!2" "f2" "g!3" ))"1" (assert ) nil nil ))nil ))nil )"2" "extensionality_postulate" "f" "g!1 - h!1 + (g!2 - h!2)" "g" "g!3 - h!3" ))"2" "2" "1" "1" "1" "x!1" )"1" nil nil ))nil ))nil ))nil )"2" 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 )"real" integral nil )"[T, T -> boolean]" equalities nil )"real" reals nil )"odd_int" integers nil )"measure_type" 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" integral nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )nil nn_integral nil )"bool" nn_integral nil )nil nn_integral nil )"nn_integrable" integralnil )"nnreal" nil )"integrable" integral nil )"real" reals nil )"[T -> real]" real_fun_ops "reals/" )nil functions nil )"integrable" integral nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil integral nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" integral nil )nil integral nil )set type-eq-decl nil sets nil )"set[real]" integral nil )"[T -> real]" real_fun_ops "reals/" )"bool" sets nil )"(p)" sets nil ))nil 3390736302"" (skosimp)"" (expand "integral" )"" (typepred "choose[real](integrals(f!1))" )"" (typepred "choose[real](integrals(c!1*f!1))" )"" (name-replace "X" "choose[real](integrals(f!1))" )"" (name-replace "CX" "choose[real](integrals(c!1*f!1))" )"" (expand "integrals" )"" (skosimp*)"" (replace -3)"" (replace -2)"" (replace -4)"" (hide-all-but (-1 1))"" (case "c!1*g!2+h!1 = c!1*h!2+g!1" )"1" (hide -2)"1" case "c!1>=0" )"1" "nn_integral_scal" "c" "c!1" "f" "g!2" ))"1" "nn_integral_scal" "c" "c!1" "f" "h!2" ))"1" "nn_integral_add" "f1" "c!1 * g!2" "f2" "h!1" ))"1" "nn_integral_add" "f1" "c!1 * h!2" "f2" "g!1" ))"1" (assert ) nil nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil )"2" case "-c!1*h!2+h!1=-c!1*g!2+g!1" )"1" "1" "nn_integral_scal" "c" "-c!1" "f" "h!2" ))"1" "nn_integral_scal" "c" "-c!1" "f" "g!2" ))"1" "nn_integral_add" "f1" "-c!1 * g!2" "f2" "g!1" ))"1" "nn_integral_add" "f1" "-c!1 * h!2" "f2" "h!1" ))"1" (assert ) nil nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" "extensionality_postulate" "f" "c!1 * g!2 + h!1" "g" "c!1 * h!2 + g!1" ))"2" "2" "1" "1" "1" "x!1" )"1" (grind) nil nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "extensionality_postulate" "f" "c!1 * (g!2 - h!2)" "g" "g!1 - h!1" ))"2" "2" "1" "1" "1" "x!1" )"1" (grind) nil nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" integral nil )"integrable" integral nil )"[T -> real]" real_fun_ops "reals/" )"integrable" integral nil )"[T -> real]" real_fun_ops "reals/" )"real" reals nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"real" reals nil )nil functions nil )nil nn_integral nil )"(total_order?[real])" nil )nil nn_integral nil )"real" reals nil )"real" reals nil )"nnreal" nil )"integrable" integral nil )"[T -> real]" real_fun_ops "reals/" )"bool" reals nil )nil real_types nil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def nil )nil subset_algebra_def nil )"sigma_algebra" integral nil )nil extended_nnreal"extended_nnreal/" )"bool" generalized_measure_def nil )nil generalized_measure_defnil )"measure_type" integral nil )"bool" nn_integral nil )nil nn_integral nil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil integral nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" integral nil )nil integral nil )set type-eq-decl nil sets nil )"set[real]" integral nil )"bool" sets nil )"(p)" sets nil ))nil 3391186785"" (skosimp)"" (lemma "integral_scal" ("c" "-1" "f" "f!1" ))"" (assert )"" (expand "*" -1)"" (assert ) (("" (expand "-" ) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )nil integral nil )"bool" integral nil )nil booleans nil )nil 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 integral nil )"odd_int" integers nil )"[T -> real]" real_fun_ops "reals/" )"[T -> real]" real_fun_ops "reals/" )"integrable" integral nil )"real" reals nil )"integrable" integral nil )"real" reals nil ))nil 3391186839"" (skosimp)"" (lemma "integral_opp" ("f" "f2!1" ))"" (lemma "integral_add" ("f1" "f1!1" "f2" "-f2!1" ))"" (expand "-" -1 1)"" (expand "+" -1 1)"" (expand "-" 1) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )nil integral nil )"bool" integral 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 integral nil )nil integral nil )"[T -> real]" real_fun_ops "reals/" )"real" reals nil )"real" reals nil )"real" reals nil )"[T -> real]" real_fun_ops "reals/" )"integrable" integral nil )nil integral nil )"[T -> real]" real_fun_ops "reals/" ))nil 3390736251"" (skosimp)"" (lemma "nn_integrable_is_nn_integrable" ("f" "f!1" ))"" (assert )"" (split -1)"1" (rewrite "integral_nn" ) (("1" (assert ) nil nil )) nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil )nil integral nil )"bool" integral 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 integral nil )nil integral nil )nil nn_integral nil )"bool" nn_integral nil )"measure_type" integral nil )nil generalized_measure_defnil )"bool" generalized_measure_def nil )nil extended_nnreal"extended_nnreal/" )"sigma_algebra" integral nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )nil real_types nil )"bool" reals nil )nil integral nil )"(total_order?[real])" nil ))nil 3391224442"" (skosimp)"" (typepred "f!1" )"" (expand "integrable?" )"" (skosimp)"" (typepred "g!1" )"" (typepred "h!1" )"" (lemma "abs_measurable" ("g" "f!1" ))"" (case "forall x: abs(f!1)(x)<= (g!1+h!1)(x)" )"1" "nn_integrable_add" ("f1" "g!1" "f2" "h!1" ))"1" (flatten)"1" "nn_integrable_le" "f" "g!1+h!1" "g" "abs(f!1)" ))"1" (split -1)"1" (flatten)"1" (lemma "nn_integrable_is_integrable" )"1" "abs(f!1)" )"1" expand "integrable?" )"1" (propax) nil nil ))nil ))nil ))nil ))nil )"2" (skosimp)"2" (inst -3 "x!1" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (-4 1))"2" (replace -1)"2" (hide -1) (("2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil integral nil )"bool" integral nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil integral nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"[T -> real]" real_fun_ops "reals/" )"[T -> nonneg_real]" real_fun_ops "reals/" )nil real_types nil )"bool" reals nil )nil integral nil )"(total_order?[real])" nil )"integrable" integral nil )nil nn_integral nil )"measurable_function[T, S]" nil )"nn_integrable" integralnil )"integrable" integral nil )nil nn_integral nil )"real" reals nil )"[T -> real]" real_fun_ops "reals/" )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"real" reals nil )"nnreal" nil )"(strict_total_order?[real])" real_props nil )nil measure_space_defnil )"bool" measure_space_def nil )nil measure_space nil )"bool" reals nil )nil real_types nil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def nil )nil subset_algebra_def nil )"sigma_algebra" integral nil )nil extended_nnreal"extended_nnreal/" )"bool" generalized_measure_def nil )nil generalized_measure_defnil )"measure_type" integral nil )"bool" nn_integral nil )nil nn_integral nil ))nil ))nil 3391224442"" (skosimp)"" (rewrite "max_def" ) (("" (rewrite "integrable_scal" ) nil nil ))nil ))nil )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 )"bool" integral nil )nil integral nil )nil integral nil )"integrable" integral nil )"integrable" integral nil )"integrable" integral nil )"posrat" nil )"integrable" integral nil )"[T -> real]" real_fun_ops "reals/" )"[T -> nonneg_real]" real_fun_ops "reals/" )nil real_types nil )"bool" reals nil )"[T -> real]" real_fun_ops "reals/" )nil integral nil ))nil ))nil 3391224442"" (skosimp)"" (typepred "f2!1" )"" (typepred "f1!1" )"" (lemma "integrable_opp" ("f" "f2!1" ))"" (lemma "integrable_opp" ("f" "f1!1" ))"" (expand "-" )"" "integrable_max" "f1" "LAMBDA (x: T): -f1!1(x)" "f2" "LAMBDA (x: T): -f2!1(x)" ))"1" (expand "max" )"1" "integrable_opp" "f" "LAMBDA (x_1: T): max(-f1!1(x_1), -f2!1(x_1))" ))"1" (expand "-" )"1" (expand "min" )"1" "(LAMBDA (x: T): -max(-f1!1(x), -f2!1(x)))=(LAMBDA (x: T): min(f1!1(x), f2!1(x)))" )"1" (apply-extensionality :hide? t)"1" (hide-all-but 1)"1" (grind) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil )"2" (propax) nil nil ) ("3" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil integral nil )"bool" integral nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil integral nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil integral nil )"[T -> real]" real_fun_ops "reals/" )max const-decl "[T -> real]" real_fun_ops_aux "reals/" )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"bool" reals nil )"[T, T -> boolean]" equalities nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )min const-decl "[T -> real]" real_fun_ops_aux "reals/" )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )nil integral nil )"real" reals nil ))nil ))nil 3391224442"" (skosimp)"" (lemma "integrable_max" ("f1" "f!1" "f2" "lambda x: 0" ))"1" (expand "max" )"1" (expand "plus" ) (("1" (propax) nil nil )) nil )) nil )"2" (rewrite "integrable_zero" ) nil nil ))nil ))nil )nil integral nil )"bool" integral 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 integral nil )nil integral nil )"[T -> nnreal]" real_fun_ops_aux "reals/" )max const-decl "[T -> real]" real_fun_ops_aux "reals/" )nil integral nil ))nil ))nil 3391224442"" (skosimp)"" (lemma "integrable_min" ("f1" "f!1" "f2" "lambda x: 0" ))"1" (expand "min" )"1" "integrable_opp" "f" "LAMBDA (x_1: T): min(f!1(x_1), 0)" ))"1" (expand "minus" )"1" (expand "-" -1) (("1" (propax) nil nil )) nil )) nil )"2" (propax) nil nil ))nil ))nil )"2" (rewrite "integrable_TCC1" ) nil nil ))nil ))nil )nil integral nil )"bool" integral 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 integral nil )nil integral nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil integral nil )"[T -> real]" real_fun_ops "reals/" )"[T -> nnreal]" real_fun_ops_aux "reals/" )"real" reals nil )min const-decl "[T -> real]" real_fun_ops_aux "reals/" )nil integral nil ))nil ))nil 3391189479"" (skosimp)"" (lemma "integral_nonneg" ("f" "abs(f!1)-f!1" ))"" (split -1)"1" (rewrite "integral_diff" )"1" (lemma "integral_nonneg" ("f" "f!1+abs(f!1)" ))"1" (split -1)"1" (rewrite "integral_add" )"1" (name-replace "INTF" "integral(f!1)" )"1" (name-replace "INTA" "integral(abs(f!1))" )"1" (grind) nil nil )) nil ))nil ))nil )"2" (hide-all-but 1) (("2" (grind) nil nil )) nil ))nil ))nil ))nil )"2" (hide-all-but 1) (("2" (grind) nil nil )) nil ))nil ))nil ))nil )"[T -> nonneg_real]" real_fun_ops "reals/" )nil real_types nil )"bool" reals nil )"[T -> real]" real_fun_ops "reals/" )nil integral nil )"bool" integral 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 integral nil )nil integral nil )"integrable" integral nil )"integrable" integral nil )nil integral nil )"real" reals nil )"real" integral nil )"[T, T -> boolean]" equalities nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"odd_int" integers nil )"real" reals nil )nil integral nil )"real" reals nil )"[T -> real]" real_fun_ops "reals/" )"integrable" integral nil ))nil 3395577345"" (skosimp)"" (split)"1" (flatten)"1" (assert )"1" (lemma "integrable_plus" ("f" "f0!1" ))"1" (lemma "integrable_minus" ("f" "f0!1" ))"1" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (flatten)"2" "integrable_diff" "f1" "plus(f0!1)" "f2" "minus(f0!1)" ))"1" (rewrite "plus_minus_def" -1 :dir rl) nil nil )"2" (propax) nil nil ) ("3" (propax) nil nil ))nil ))nil ))nil ))nil )nil integral nil )nil integral nil )nil integral nil )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 )"bool" integral nil )nil integral nil )"[T -> nnreal]" real_fun_ops_aux "reals/" )"[T -> nnreal]" real_fun_ops_aux "reals/" )nil real_types nil )"bool" reals nil )nil integral nil )nil real_fun_ops_aux "reals/" ))nil 3391606213"" (skosimp)"" (lemma "integral_diff" ("f1" "plus(f!1)" "f2" "minus(f!1)" ))"" (replace -1 1 rl)"" (hide-all-but 1)"" (case-replace "plus(f!1) - minus(f!1)=f!1" )"" (hide 2)"" (apply-extensionality :hide? t)"" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"[T -> nnreal]" real_fun_ops_aux "reals/" )"[T -> nnreal]" real_fun_ops_aux "reals/" )nil real_types nil )"bool" reals nil )nil integral nil )"bool" integral 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 integral nil )nil integral nil )"integrable" integral nil )"integrable" integral nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"(strict_total_order?[real])" real_props 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 )"integrable" integral nil )"[T, T -> boolean]" equalities nil )"[T -> real]" real_fun_ops "reals/" ))nil 3395577514"" (skosimp)"" (split)"1" (flatten)"1" (rewrite "integrable_pm_def" +)"1" (lemma "plus_measurable" ("g" "h!1" ))"1" (lemma "minus_measurable" ("g" "h!1" ))"1" "abs(h!1)=plus[T](h!1)+minus[T](h!1)" )"1" (replace -1 -4 rl)"1" "nn_integrable_le" "g" "plus[T](h!1)" "f" "abs(h!1)" ))"1" "nn_integrable_le" "g" "minus[T](h!1)" "f" "abs(h!1)" ))"1" (split -1)"1" (flatten)"1" (split)"1" (flatten)"1" assert )"1" "nn_integrable_is_integrable" )"1" "plus[T](h!1)" )"1" "minus[T](h!1)" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (grind) nil nil )) nil ))nil ))nil )"2" (hide-all-but 1) (("2" (grind) nil nil ))nil ))nil ))nil )"2" "nn_integrable_is_nn_integrable" "f" "abs[T](h!1)" ))"1" (split -1)"1" (propax) nil nil )"2" (hide-all-but 1) (("2" (grind) nil nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (apply-extensionality :hide? t)"1" (grind) nil nil ) ("2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten) (("2" (rewrite "integrable_abs" ) nil nil )) nil ))nil ))nil )nil integral nil )nil integral nil )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 )nil defined_types nil )nil sets nil )"bool" subset_algebra_def nil )nil subset_algebra_def nil )"sigma_algebra" integral nil )"bool" measure_space_def nil )nil measure_space_defnil )"measurable_function[T, S]" nil )"measurable_function[T, S]" nil )nil measure_space nil )"real" reals nil )"nnreal" nil )"real" reals nil )"measurable_function[T, S]" integral nil )nil integral nil )"bool" integral nil )nil integral nil )"(strict_total_order?[real])" real_props nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"(strict_total_order?[real])" real_props nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"real" reals nil )nil integral nil )"(total_order?[real])" nil )"measure_type" integral nil )nil generalized_measure_defnil )"bool" generalized_measure_def nil )nil extended_nnreal"extended_nnreal/" )nil nn_integral nil )"bool" nn_integral nil )nil nn_integral nil )"[T -> nnreal]" real_fun_ops_aux "reals/" )"[T -> nnreal]" real_fun_ops_aux "reals/" )nil real_types nil )"[T -> real]" real_fun_ops "reals/" )"[T -> nonneg_real]" real_fun_ops "reals/" )nil real_types nil )"bool" reals nil )"[T, T -> boolean]" equalities nil )"measurable_function[T, S]" nil )"measurable_function[T, S]" nil )nil measure_space nil )nil integral nil ))nil 3410216774"" case "FORALL (epsilon: posreal, f: nn_integrable): AND ") "1" (skosimp)"1" (inst - "epsilon!1/2" "abs(f!1)" )"1" (expand "abs" -1)"1" (flatten)"1" (split)"1" (typepred "f!1" )"1" (lemma "measurable_ge" ("f" "abs(f!1)" ))"1" (assert )"1" (lemma "integrable_abs_def" ("h" "f!1" ))"1" (lemma "integrable_is_measurable" )"1" (inst - "abs(f!1)" )"1" (assert )"1" (inst - "epsilon!1" )"1" expand "measurable_set?" )"1" expand "abs" -3)"1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "m_monotone" "a" "{x | abs(f!1(x)) >= epsilon!1}" "b" "{x | abs(f!1(x)) > epsilon!1 / 2}" ))"1" (split -1)"1" (expand "x_le" )"1" (expand "mu_fin?" ) (("1" (assert ) nil nil ))nil ))nil )"2" (hide-all-but 1)"2" (expand "subset?" )"2" (expand "member" )"2" (skosimp) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil )"3" (hide-all-but 1)"3" (lemma "measurable_ge" ("f" "abs(f!1)" ))"3" "integrable_is_measurable" "x" "abs(f!1)" ))"3" (assert )"3" (expand "abs" -2)"3" (inst - "epsilon!1" )"3" (expand "measurable_set?" )"3" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" "nn_integrable_is_nn_integrable" ("f" "abs(f!1)" ))"2" (assert )"2" (hide 2)"2" (expand "abs" )"2" (skosimp) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp)"2" (typepred "f!1" )"2" "measurable_set?({x | f!1(x) > epsilon!1})" )"1" (expand "nn_integrable?" )"1" (skosimp)"1" (typepred "u!1" )"1" (expand "increasing_nn_isf?" )"1" "EN" "lambda n: {x | u!1(n)(x) > epsilon!1}" )"1" (hide -1)"1" (case "forall n: measurable_set?(EN(n))" )"1" (case "forall n: mu_fin?(EN(n))" )"1" (case "increasing?(EN)" )"1" "m_increasing_convergence" "E" "EN" ))"1" assert )"1" expand "convergent?" )"1" "M" )"1" case "M>=0" )"1" case "increasing?(isf_integral o u!1)" )"1" case "forall n: isf_integral(u!1(n)) <= M" )"1" case "forall n: mu(EN(n))<=M/epsilon!1" )"1" case "mu_fin?(IUnion(EN))" )"1" "{x | f!1(x) > epsilon!1}=IUnion(EN)" )"1" "1" "1" expand "IUnion" )"1" expand "pointwise_convergence?" )"1" expand "pointwise_increasing?" )"1" "x!1" )"1" "x!1" )"1" rewrite "metric_convergence_def" )"1" expand "metric_converges_to" )"1" expand "ball" )"1" expand "member" )"1" expand "increasing?" )"1" expand "EN" )"1" "f!1(x!1) > epsilon!1" )"1" "f!1(x!1)-epsilon!1" )"1" "1" "n!1" )"1" assert )"1" "n!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil )"2" assert )"2" "2" "u!1(i!1)(x!1) - epsilon!1" )"1" "1" "i!1+n!1" )"1" expand "abs" )"1" "i!1" "i!1+n!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "x_converges?" )"2" expand "mu_fin?" )"2" replace 1 -5)"2" expand "o " )"2" replace "2" "2" "2" "bounded_above_is_convergent" "u" "LAMBDA (i:nat): m(EN(i))`2" ))"1" "1" expand "convergent_upto?" )"1" "1" expand "converges_upto?" )"1" "1" "DRL1" "LAMBDA (i: nat): m(EN(i))`2" )"1" "1" rewrite "metric_convergence_def" )"1" expand "metric_converges_to" )"1" expand "ball" )"1" expand "convergent?" )"1" expand "convergence" )"1" expand "member" )"1" "x!1" )"1" "1" "epsilon!2" )"1" "1" "n!1" )"1" "1" "i!1" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "mu" )"2" expand "bounded_above?" )"2" "M / epsilon!1" )nil nil ))nil ))nil ))nil )"3" "3" expand "increasing?" )"3" "i!1" "j!1" ))"3" "i!1" "j!1" )"3" "3" assert )"3" "m_monotone" "a" "EN(i!1)" "b" "EN(j!1)" ))"1" assert )"1" expand "x_le" )"1" "j!1" )nil nil ))nil ))nil )"2" "j!1" )nil nil )"3" "i!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "i!1" )"2" expand "measurable_set?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" rewrite "measurable_IUnion" )nil nil ))nil )"2" "2" "2" "n!1" )"2" "isf_integral_le" "i1" "epsilon!1*phi(EN(n!1))" "i2" "u!1(n!1)" ))"1" "1" "n!1" )"1" "n!1" )"1" "isf_phi" "E" "EN(n!1)" ))"1" "isf_scal" "c" "epsilon!1" "i" "phi[T, S](EN(n!1))" ))"1" rewrite "isf_integral_scal" )"1" rewrite "isf_integral_phi" )"1" "div_mult_pos_le2" "x" "mu(EN(n!1))" "z" "M" "py" "epsilon!1" ))"1" assert )nil nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil )"2" "2" expand "*" )"2" expand "phi" )"2" expand "EN" )"2" expand "member" )"2" "u!1(n!1)(x!1) > epsilon!1" )"1" assert )nil nil )"2" assert )"2" "u!1(n!1)" )"2" expand "nn_isf?" )"2" "x!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "n!1" )"2" "n!1" )"2" rewrite "isf_scal" )"2" rewrite "isf_phi" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "n!1" )"3" "n!1" )"3" "n!1" )"3" expand "measurable_set?" )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "o " )"2" expand "increasing?" )"2" rewrite "metric_convergence_def" )"2" expand "metric_converges_to" )"2" "isf_integral(u!1(n!1))-M" )"1" "1" expand "ball" )"1" expand "member" )"1" "n!1+n!2" )"1" "n!1" "n!1+n!2" )"1" assert )"1" expand "abs" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "o " )"2" expand "pointwise_increasing?" )"2" expand "increasing?" )"2" "i!1" "j!1" ))"2" "2" "isf_integral_le" "i1" "u!1(i!1)" "i2" "u!1(j!1)" ))"2" "1" nil nil )"2" "2" "x!1" )"2" "i!1" "j!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "metric_convergence_def" )"2" expand "metric_converges_to" )"2" expand "o " )"2" expand "ball" )"2" expand "member" )"2" "u!1(0)" )"2" expand "nn_isf?" )"2" "isf_integral_pos" "i" "u!1(0)" ))"2" replace "2" "isf_integral(u!1(0))-M" )"1" "1" "n!1" )"1" assert )"1" expand "pointwise_increasing?" )"1" expand "increasing?" )"1" "u!1(n!1)" )"1" expand "nn_isf?" )"1" "isf_integral_pos" "i" "u!1(n!1)" ))"1" replace "1" expand "abs" )"1" assert )"1" "isf_integral_le" "i1" "u!1(0)" "i2" "u!1(n!1)" ))"1" "1" assert )nil nil )"2" "2" "x!1" )"2" "0" "n!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "pointwise_increasing?" )"2" expand "increasing?" )"2" "i!1" "j!1" ))"2" "2" expand "subset?" )"2" expand "EN" )"2" expand "member" )"2" "2" "x!1" )"2" "i!1" "j!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (-1 1))"2" "2" "n!1" )"2" "m_monotone" "a" "EN(n!1)" "b" "nonzero_set?(u!1(n!1))" ))"1" "1" "u!1(n!1)" )"1" expand "isf?" )"1" "1" expand "x_le" )"1" expand "mu_fin?" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "nonzero_set?" )"2" expand "EN" )"2" expand "subset?" )"2" expand "member" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "nonzero_measurable" )nil nil ))nil ))nil ))nil ))nil )"3" (propax) nil nil ))nil )"2" (skosimp)"2" (hide-all-but 1)"2" expand "EN" )"2" expand "measurable_set?" )"2" "u!1(n!1)" )"2" "isf_is_simple" "x" "u!1(n!1)" ))"2" expand "simple?" )"2" "2" rewrite "measurable_gt" )"2" "epsilon!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (lemma "nn_integrable_is_measurable" )"2" (inst - "f!1" )"2" (rewrite "measurable_gt" )"2" (inst - "epsilon!1" )"2" (expand "measurable_set?" )"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil nn_integral nil )nil nn_integral nil )"bool" nn_integral nil )nil sequences nil )nil nn_integral nil )"bool" nn_integral nil )nil isf nil )"bool" isf nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[T, T -> boolean]" equalities nil )nil isf nil )"set[T]" isf nil )"(total_order?[S])" nil )"(dichotomous?[S])" nil )"(partial_order?[S])" nil )"(preorder?[S])" nil )"(transitive?[S])" nil )"(antisymmetric?[S])" nil )"(reflexive?[S])" nil )"(partial_order?[set[T]])" nil )"R" restrict nil )"bool" reals nil )"bool" fun_preds_partial "structures/" )nil isf nil )"bool" real_fun_preds "reals/" )"T3" function_props nil )"real" isf nil )"nat" integral nil )"real" integral nil )"real" reals nil )"nnreal" measure_props nil )nil measure_space_def nil )nil convergence_aux"metric_space/" )"bool" real_fun_preds "reals/" )"bool" convergence_aux"metric_space/" )"bool" convergence_aux "metric_space/" )"bool" convergence_sequences "analysis/" )"bool" convergence_sequences "analysis/" )"bool" extended_nnreal "extended_nnreal/" )"bool" pointwise_convergencenil )"[numfield, numfield -> numfield]" number_fields nil )nil metric_space"metric_space/" )"real" reals nil )"set[T]" metric_space_def "metric_space/" )"(strict_total_order?[real])" real_props nil )"posreal" integral nil )"T" integral nil )"nn_integrable" integral nil )"real" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"nonneg_int" nil )"nat" integral nil )"increasing_nn_isf[T, S, m]" integral nil )"[nat -> [T -> bool]]" integral nil )"bool" metric_space_def"metric_space/" )"bool" pointwise_convergence nil )"set[T]" indexed_sets nil )nil isf nil )"[T -> real]" real_fun_ops "reals/" )"nat" measure_space nil )"posreal" nil )nil isf nil )nil isf nil )"real" reals nil )nil real_props nil )"nnreal" nil )nil isf nil )nil isf nil )"bool" topological_convergence "topology/" )nil measure_props nil )nil isf nil )nil measure_space_def nil )"bool" measure_space nil )nil integral nil )nil measure_space_def nil )nil integral nil )"bool" measure_space_def nil )nil measure_space_defnil )nil integral nil )NOT const-decl "[bool -> bool]" booleans nil )"(total_order?[real])" nil )"bool" extended_nnreal "extended_nnreal/" )"bool" sets nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"bool" sets nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil measure_props nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"integrable" integral nil )nil integral nil )"bool" integral nil )"[T -> nonneg_real]" real_fun_ops "reals/" )"posreal" nil )"integrable" integral nil )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 )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil integral nil )nil real_types nil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def nil )nil subset_algebra_def nil )"sigma_algebra" integral nil )nil extended_nnreal"extended_nnreal/" )"bool" generalized_measure_def nil )nil generalized_measure_defnil )"measure_type" integral nil )"bool" nn_integral nil )nil nn_integral nil )AND const-decl "[bool, bool -> bool]" booleans nil )set type-eq-decl nil sets nil )"bool" measure_space_def nil )nil measure_space_def nil )"bool" measure_props nil ))nil 3391607536"" (skosimp)"" (rewrite "integral_pm" )"" (lemma "integrable_pm_def" ("f0" "i!1" ))"" (assert )"" (rewrite "isf_is_integrable" )"" (flatten)"" (rewrite "integral_nn" )"1" (rewrite "integral_nn" )"1" (rewrite "nn_integral_isf" )"1" (rewrite "nn_integral_isf" )"1" "isf_integral_diff" "i1" "plus(i!1)" "i2" "minus(i!1)" ))"1" (rewrite "plus_minus_def" -1 :dir rl)"1" (assert ) nil nil )) nil ))nil )"2" (expand "nn_isf?" )"2" (hide-all-but 1) (("2" (grind) nil nil ))nil ))nil ))nil )"2" (expand "nn_isf?" )"2" (hide-all-but 1) (("2" (grind) nil nil ))nil ))nil ))nil )"2" "nn_integrable_is_nn_integrable" "f" "minus[T](i!1)" ))"2" (split -1)"1" (propax) nil nil )"2" (hide-all-but 1) (("2" (grind) nil nil ))nil ))nil ))nil ))nil )"2" "nn_integrable_is_nn_integrable" "f" "plus[T](i!1)" ))"2" (split -1)"1" (propax) nil nil )"2" (hide-all-but 1) (("2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil integral nil )nil integral nil )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 )"bool" integral nil )nil integral nil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def nil )nil subset_algebra_def nil )"sigma_algebra" 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" integral nil )"bool" isf nil )nil isf nil )"isf[T, S, m]" integral nil )"integrable" integral nil )"isf" integral nil )"integrable" integral nil )"real" reals nil )"[T -> nnreal]" real_fun_ops_aux "reals/" )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"(strict_total_order?[real])" real_props nil )nil real_fun_ops_aux "reals/" )nil isf nil )"(strict_total_order?[real])" real_props nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )nil nn_integral nil )"bool" nn_integral nil )nil nn_integral nil )nil integral nil )"odd_int" integers nil )nil integral nil )"bool" nn_integral nil )nil nn_integral nil )"[T -> nnreal]" real_fun_ops_aux "reals/" )nil integral nil )nil integral nil ))nil 3391187912"" (skosimp)"" (typepred "f!1" )"" (name "H" "abs(h!1-f!1)" )"" (case "measurable_function?(H)" )"1" (case "forall x: 0 <= H(x)" )"1" (case "ae_0?(H)" )"1" (lemma "nn_measurable_def" ("f" "H" ))"1" (replace -3 -1)"1" (replace -4 -1)"1" (assert )"1" (skosimp)"1" (typepred "w!1" )"1" (case "forall (n:nat): ae_0?(w!1(n))" )"1" case "forall (n:nat): isf_integral(w!1(n)) = 0" )"1" case "pointwise_convergence?(w!1,H) AND convergence?(isf_integral o w!1,0)" )"1" "1" case "nn_integrable?(H)" )"1" "integrable_abs_def" "h" "h!1 - f!1" ))"1" replace -12)"1" "nn_integrable_is_integrable" )"1" "H" )"1" assert )"1" "integrable_add" "f1" "h!1 - f!1" "f2" "f!1" ))"1" "(+[T])(h!1 - f!1, f!1)=h!1" )"1" assert )"1" case "nn_integral(H)=0" )"1" replace "1" "integral_nn" "g" "abs(h!1 - f!1)" ))"1" replace "1" "1" "integral_abs" "f" "h!1-f!1" ))"1" replace "1" "integral(h!1 - f!1)=0" )"1" rewrite "integral_diff" )"1" assert )nil nil ))nil )"2" "abs(integral(h!1 - f!1))" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "nn_integral" )"2" "2" case "nonempty?[increasing_nn_isf[T, S, m]] ") "1" "choose_member" "a" "{u: increasing_nn_isf[T, S, m] | ")) "1" "1" "CU" "choose({u: increasing_nn_isf[T, S, m] | ") "1" expand "member" )"1" "1" "nn_convergence" "u1" "w!1" "f" "H" "u2" "CU" ))"1" replace "1" replace "1" "1" "1" replace "1" rewrite "limit_def" nil nil ))nil ))nil )"2" "2" expand "convergent?" )"2" "0" )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" "n!1" ))"1" expand "nn_isf?" )"1" expand "isf?" )"1" "1" "n!1" )"1" expand "increasing_nn_simple?" )"1" "1" "n!1" )"1" expand "nn_simple?" )"1" "1" assert )"1" "1" expand "ae_0?" )"1" expand "restrict" )"1" expand "pointwise_ae?" )"1" expand "ae?" )"1" expand "fullset" )"1" expand "ae_in?" )"1" "1" "E!1" )"1" expand "negligible_set?" )"1" "1" expand "null_set?" )"1" "1" "m_monotone" "a" "nonzero_set?(w!1(n!1))" "b" "X!1" ))"1" "1" expand "mu_fin?" )"1" expand "x_le" )"1" assert )nil nil ))nil ))nil )"2" "2" expand "nonzero_set?" )"2" expand "subset?" )"2" expand "member" )"2" "2" "x!1" )"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 )"2" "2" "x!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "increasing_nn_simple?" )"2" expand "increasing_nn_isf?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "nonempty?" )"2" nil nil ))nil ))nil ))nil )"2" "2" expand "nonempty?" )"2" expand "empty?" )"2" expand "member" )"2" "w!1" )"2" "1" "n!1" ))"1" expand "nn_isf?" )"1" expand "isf?" )"1" expand "increasing_nn_simple?" )"1" "1" "n!1" )"1" expand "nn_simple?" )"1" "1" assert )"1" "1" "n!1" )"1" "1" expand "ae_0?" "1" expand "restrict" )"1" expand "pointwise_ae?" )"1" expand "ae?" )"1" expand "fullset" )"1" expand "ae_in?" )"1" "1" "E!1" )"1" expand "negligible_set?" )"1" "1" expand "null_set?" )"1" "1" "m_monotone" "a" "nonzero_set?(w!1(n!1))" "b" "X!1" ))"1" "1" expand "x_le" )"1" expand "mu_fin?" )"1" assert )nil nil ))nil ))nil )"2" "2" expand "nonzero_set?" )"2" expand "subset?" )"2" expand "member" )"2" "2" "x!1" )"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 )"2" "2" "x!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "increasing_nn_isf?" )"2" expand "pointwise_converges_upto?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "nn_integrable?" )"2" "w!1" )"1" assert )"1" expand "convergent?" )"1" "0" )nil nil ))nil ))nil )"2" expand "increasing_nn_isf?" )"2" expand "nn_isf?" )"2" expand "increasing_nn_simple?" )"2" "2" assert )"2" "2" "n!1" ))"2" expand "isf?" )"2" "n!1" )"2" "n!1" )"2" expand "nn_simple?" )"2" "2" assert )"2" "1" "1" expand "ae_0?" )"1" expand "restrict" )"1" expand "pointwise_ae?" )"1" expand "nonzero_set?" )"1" expand "ae?" )"1" expand "fullset" )"1" expand "ae_in?" )"1" "1" "E!1" )"1" expand "negligible_set?" )"1" "1" expand "null_set?" )"1" "1" "m_monotone" "a" "nonzero_set?(w!1(n!1))" "b" "X!1" ))"1" "1" expand "x_le" )"1" expand "mu_fin?" )"1" assert )"1" expand "nonzero_set?" )"1" nil nil ))nil ))nil ))nil ))nil )"2" "2" expand "nonzero_set?" )"2" expand "subset?" )"2" expand "member" )"2" "2" "x!1" )"2" "x!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "w!1(n!1)" )"2" rewrite "nonzero_measurable" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "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 )"2" "2" expand "pointwise_converges_upto?" )"2" "2" assert )"2" "isf_integral o w!1 = lambda (n:nat): 0" )"1" expand "convergence?" )"1" "1" "0" )"1" nil nil ))nil ))nil ))nil )"2" "2" "2" "x!1" )"2" expand "o " )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" "n!1" ))"3" expand "increasing_nn_simple?" )"3" "3" "n!1" )"3" "n!1" )"3" expand "isf?" )"3" expand "nn_simple?" )"3" "3" assert )"3" "3" expand "ae_0?" )"3" expand "restrict" )"3" expand "pointwise_ae?" )"3" expand "ae?" )"3" expand "fullset" )"3" expand "ae_in?" )"3" "3" "E!1" )"3" expand "negligible_set?" )"3" "3" expand "null_set?" )"3" "3" "m_monotone" "a" "nonzero_set?(w!1(n!1))" "b" "X!1" ))"3" "1" expand "x_le" )"1" expand "mu_fin?" )"1" assert )nil nil ))nil ))nil )"2" "2" expand "nonzero_set?" )"2" expand "subset?" )"2" expand "member" )"2" "2" "x!1" )"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 ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "n!1" )"2" "2" "isf_ae_0" "f" "w!1(n!1)" ))"2" replace -2)"2" expand "increasing_nn_simple?" )"2" "2" expand "nn_simple?" )"2" "n!1" )"2" "2" replace -4)"2" "2" "isf_integral_abs" "i" "w!1(n!1)" ))"2" replace -3)"2" "abs(isf_integral(w!1(n!1)))" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" expand "increasing_nn_simple?" )"3" "3" "3" "n!1" )"3" "n!1" )"3" expand "isf?" )"3" expand "nn_simple?" )"3" "3" assert )"3" "3" expand "ae_0?" -1)"3" expand "restrict" )"3" expand "pointwise_ae?" )"3" expand "ae?" )"3" expand "fullset" )"3" expand "ae_in?" )"3" "3" "E!1" )"3" expand "negligible_set?" )"3" "3" expand "null_set?" )"3" "3" "m_monotone" "a" "nonzero_set?(w!1(n!1))" "b" "X!1" ))"3" "1" expand "x_le" )"1" expand "mu_fin?" )"1" assert )nil nil ))nil ))nil )"2" "2" expand "nonzero_set?" )"2" expand "subset?" )"2" expand "member" )"2" "2" "x!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 ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2 -7)"2" "2" expand "pointwise_converges_upto?" )"2" "2" case "FORALL x: w!1(n!1)(x) <= H(x)" )"1" "1" expand "ae_0?" )"1" expand "restrict" )"1" expand "pointwise_ae?" )"1" expand "ae?" )"1" expand "fullset" )"1" expand "ae_in?" )"1" "1" "E!1" )"1" "1" "x!1" )"1" assert )"1" "x!1" )"1" "x!1" )"1" assert )"1" "w!1" )"1" expand "increasing_nn_simple?" )"1" expand "nn_simple?" )"1" "1" "n!1" )"1" "1" "x!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "pointwise_convergence?" )"2" "2" "2" case "H(x!1)<w!1(n!1)(x!1)" )"1" "1" "x!1" )"1" rewrite "metric_convergence_def" "1" expand "metric_converges_to" )"1" "w!1(n!1)(x!1)-H(x!1)" )"1" "1" expand "ball" )"1" expand "member" )"1" "n!1+n!2" )"1" assert )"1" expand "pointwise_increasing?" )"1" "x!1" )"1" "x!1" )"1" expand "increasing?" )"1" "n!1" "n!1+n!2" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (-5 1))"2" (expand "ae_0?" )"2" (expand "ae_eq?" )"2" (expand "H" )"2" (expand "abs" )"2" (expand "restrict" )"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" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1) (("2" (grind) nil nil )) nil ))nil )"2" (hide -1 -3 2)"2" (expand "H" ) (("2" (propax) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )nil integral nil )"bool" integral nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil integral nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil real_types nil )nil extended_nnreal"extended_nnreal/" )"bool" generalized_measure_def nil )nil generalized_measure_defnil )"measure_type" integral nil )"bool" measure_theory nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )nil sequences nil )"bool" measure_space nil )nil measure_space nil )"(S)" integral nil )"measurable_set[T, S]" integralnil )"bool" reals nil )"bool" metric_space_def"metric_space/" )"(strict_total_order?[real])" real_props nil )"bool" real_fun_preds "reals/" )"bool" pointwise_convergence nil )"[numfield, numfield -> numfield]" number_fields nil )"nonneg_int" nil )"set[T]" metric_space_def "metric_space/" )nil real_types nil )"bool" reals nil )"T" integral nil )"nat" integral nil )"(strict_total_order?[real])" real_props nil )nil metric_space"metric_space/" )"bool" isf nil )nil isf nil )"real" isf nil )nil isf nil )nil integral nil )nil integral nil )"[T -> real]" real_fun_ops "reals/" )"measurable_function[T, S]" nil )"nnreal" nn_integral nil )nil integral nil )"(total_order?[real])" nil )"real" reals nil )"(total_order?[real])" nil )nil integral nil )"real" integral nil )nil integral nil )"bool" nn_integral nil )nil nn_integral nil )"bool" nn_integral nil )nil nn_integral nil )set type-eq-decl nil sets nil )"bool" sets nil )"bool" sets nil )nil nn_integral nil )nil topological_convergence "topology/" )"bool" topological_convergence "topology/" )nil hausdorff_convergence "topology/" )"R" restrict nil )"bool" measure_theory nil )"bool" measure_theory nil )"bool" measure_theory nil )nil measure_theory nil )"bool" extended_nnreal "extended_nnreal/" )"(partial_order?[set[T]])" nil )"bool" measure_props nil )"bool" booleans nil )"bool" sets nil )"set[T]" isf nil )nil measure_space_def nil )"bool" measure_space_def nil )nil measure_props nil )"bool" measure_theory nil )"set" sets nil )"bool" measure_theory nil )"bool" measure_space nil )"(p)" sets nil )nil sets_lemmas nil )"bool" pointwise_convergencenil )"increasing_nn_simple[T, S]" integral nil )"bool" sets nil )"real" reals nil )nil integral nil )nil nn_integral nil )"[T -> nonneg_real]" integral nil )"bool" nn_integral nil )"[bool, bool -> bool]" booleans nil )"T3" function_props nil )"bool" topological_convergence"topology/" )"setofsets[T]" metric_space_def"metric_space/" )"[numfield, numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" pointwise_convergencenil )AND const-decl "[bool, bool -> bool]" booleans nil )"(hausdorff?)" "metric_space/" )"hausdorff[real]" "metric_space/" )"second_countable" real_topology "metric_space/" )"real" reals nil )nil isf nil )nil isf nil )nil measure_space nil )"bool" measure_theory nil )"bool" reals nil )"measurable_function[T, S]" nil )"measurable_function[T, S]" nil )"bool" reals nil )nil real_types nil )"[T, T -> boolean]" equalities nil )"[T -> nonneg_real]" real_fun_ops "reals/" )"[T -> real]" real_fun_ops "reals/" )nil defined_types nil )nil sets nil )"bool" subset_algebra_def nil )nil subset_algebra_def nil )"sigma_algebra" integral nil )"bool" measure_space_def nil )nil measure_space_defnil ))nil 3395585459"" (skosimp) (("" (rewrite "integrable_abs" ) nil nil )) nil )"measurable_function[T, S]" nil )nil integral nil )nil integral nil )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 )"bool" integral nil )nil integral nil )"[T -> real]" real_fun_ops "reals/" )nil defined_types nil )nil sets nil )"bool" subset_algebra_def nil )nil subset_algebra_def nil )"sigma_algebra" integral nil )"bool" measure_space_def nil )nil measure_space_defnil ))nil ))nil 3395605522"" (skosimp)"" (expand "ae_le?" )"" (expand "pointwise_ae?" )"" (expand "ae?" )"" (expand "fullset" )"" (expand "ae_in?" )"" (skosimp)"" (typepred "E!1" )"" (expand "negligible_set?" )"" (skosimp)"" (lemma "measurable_complement" ("a" "X!1" ))"1" case "measurable_function?(phi(complement[T](X!1)))" )"1" case "forall x: (phi(complement[T](X!1))*abs(f!1 * h!1))(x) <= (phi(complement[T](X!1))* (nnc!1*abs(f!1)))(x) & (phi(complement[T](X!1))* (nnc!1*abs(f!1)))(x) <= (nnc!1*abs(f!1))(x)" )"1" "nn_integrable_le" "f" "nnc!1 * abs(f!1)" "g" "phi(complement[T](X!1)) * abs(f!1 * h!1)" ))"1" "1" "1" "1" "nn_integrable_is_integrable" )"1" "phi(complement[T](X!1)) * abs(f!1 * h!1)" )"1" "integral_ae_eq" "f" "phi(complement[T](X!1)) * abs(f!1 * h!1)" "h" "abs(f!1 * h!1)" ))"1" "1" "1" "integrable_abs_def" "h" "f!1*h!1" ))"1" assert )"1" "I_0" "integral(abs(f!1 * h!1))" )"1" rewrite "integral_nn" "1" replace -3)"1" rewrite "integral_nn" "1" rewrite "integral_scal" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "ae_eq?" )"2" expand "restrict" )"2" expand "pointwise_ae?" )"2" expand "ae?" )"2" expand "fullset" )"2" expand "ae_in?" )"2" "X!1" )"1" "1" expand "*" )"1" expand "abs" )"1" expand "complement" )"1" expand "phi" )"1" expand "member" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "negligible_set?" )"2" "X!1" )"2" assert )"2" expand "subset?" )"2" 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" "2" "x!1" )"2" "2" assert )"2" "2" expand "*" )"2" expand "abs" )"2" expand "complement" )"2" expand "phi" )"2" expand "member" )"2" "X!1(x!1)" )"1" assert )nil nil )"2" "abs(f!1(x!1) * h!1(x!1))" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "prod_measurable" )nil nil ))nil )"3" "1" "1" "x!1" ))"1" expand "*" )"1" "nnc!1=0" )"1" (assert ) nil nil )"2" "both_sides_times_pos_le1" "pz" "nnc!1" "x" "0" "y" "abs[T](f!1)(x!1)" ))"1" expand "abs" )"1" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" "integrable_abs" ("f" "f!1" ))"2" "integrable_scal" "f" "abs[T](f!1)" "c" "nnc!1" ))"2" "nn_integrable_is_nn_integrable" "f" "*[T](nnc!1, abs[T](f!1))" ))"2" assert )"2" "2" "2" expand "*" )"2" expand "abs" )"2" "nnc!1=0" )"1" assert )nil nil )"2" "both_sides_times_pos_le1" "pz" "nnc!1" "x" "0" "y" "abs(f!1(x!1))" ))"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" "2" "1" expand "*" )"1" expand "abs" )"1" expand "complement" )"1" expand "phi" )"1" expand "member" )"1" "X!1(x!1)" )"1" (assert ) nil nil )"2" assert )"2" "x!1" )"2" expand "subset?" )"2" "x!1" )"2" assert )"2" rewrite "abs_mult" "2" "abs(f!1(x!1))=0" )"1" assert )nil nil )"2" "both_sides_times_pos_le1" "pz" "abs(f!1(x!1))" "x" "abs(h!1(x!1))" "y" "nnc!1" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "*" )"2" expand "complement" )"2" expand "phi" )"2" expand "member" )"2" "X!1(x!1)" )"1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (-1 1))"2" "phi_is_simple" "X" "complement[T](X!1)" ))"1" "simple_is_measurable" )"1" "phi(complement[T](X!1))" )nil nil ))nil )"2" expand "measurable_set?" )"2" (propax) nil nil ))nil ))nil ))nil ))nil )"2" (expand "null_set?" )"2" (flatten) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" measure_theory nil )"bool" measure_theory nil )"bool" measure_theory nil )nil measure_theory nil )"bool" measure_theory nil )"measure_type" 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" 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 integral nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" measure_theory nil )"bool" measure_space_def 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 )"bool" booleans nil )nil real_props nil )nil nn_integral nil )"bool" nn_integral nil )nil nn_integral nil )"real" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )nil integral nil )nil integral nil )"R" restrict nil )"measurable_set[T, S]" integralnil )"(S)" integral nil )"bool" sets nil )"(total_order?[real])" nil )"nnreal" nil )"set[T]" integral nil )"bool" measure_theory nil )"(partial_order?[set[T]])" nil )"(total_order?[real])" nil )"bool" sets nil )nil integral nil )nil integral nil )"real" reals nil )"[T, T -> boolean]" equalities nil )"real" integral nil )nil integral nil )nil measure_space nil )nil integral nil )nil integral nil )nil integral nil )nil real_props nil )"bool" reals nil )nil real_types nil )"(strict_total_order?[real])" real_props nil )"[T -> real]" real_fun_ops "reals/" )nil measure_space_defnil )nil integral nil )"bool" integral nil )"[T -> nonneg_real]" real_fun_ops "reals/" )nil real_types nil )"[T -> real]" real_fun_ops "reals/" )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"integrable" integral nil )"integrable" integral nil )"measurable_function[T, S]" nil )"measurable_function[T, S]" nil )nil measure_space nil )nil measure_space nil )"bool" measure_space nil )nil measure_space nil )nil measure_space_def nil )"bool" measure_space_def nil )nil measure_space_def nil )"set" sets nil )"bool" measure_theory nil ))nil 3395576297"" (skosimp)"" (lemma "integral_prod" ("h" "phi(E!1)" "nnc" "1" "f" "f!1" ))"1" (case-replace "f!1 * phi(E!1)=phi(E!1) * f!1" )"1" (hide -1)"1" (assert )"1" (hide 2)"1" (expand "phi" )"1" (expand "abs" )"1" (expand "member" )"1" (expand "abs" )"1" (expand "ae_le?" )"1" (expand "pointwise_ae?" )"1" (expand "ae?" )"1" (expand "fullset" )"1" expand "ae_in?" )"1" "emptyset[T]" )"1" "1" "1" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (apply-extensionality :hide? t)"2" (expand "*" ) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil )"2" (lemma "phi_is_simple" ("X" "E!1" ))"1" (expand "simple?" ) (("1" (flatten) nil nil )) nil )"2" (typepred "E!1" )"2" (expand "measurable_set?" ) (("2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )nil real_types nil )nil measure_space_def nil )"bool" measure_space_def nil )"nat" measure_space 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 measure_space_defnil )"bool" measure_space_def nil )"sigma_algebra" integral nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )nil integral nil )"bool" integral 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 integral nil )nil integral nil )"real" reals nil )"[T -> nonneg_real]" real_fun_ops "reals/" )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"bool" measure_theory nil )"set" sets nil )"(S)" integral nil )"null_set" 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 )"measure_type" integral nil )nil generalized_measure_defnil )"bool" generalized_measure_def nil )nil extended_nnreal"extended_nnreal/" )"(total_order?[real])" nil )"real" reals nil )"bool" measure_theory nil )"bool" measure_theory nil )"(S)" integral nil )"measurable_set[T, S]" integralnil )"bool" measure_theory nil )"bool" sets nil )"[T, T -> boolean]" equalities nil )"[T -> real]" real_fun_ops "reals/" )NOT const-decl "[bool -> bool]" booleans nil )"bool" measure_space nil )nil measure_space nil ))nil 3391188035"" (skosimp)"" (assert )"" (expand "ae_le?" )"" (expand "pointwise_ae?" )"" (expand "ae?" )"" (expand "fullset" )"" (expand "ae_in?" )"" (skosimp)"" (typepred "E!1" )"" (expand "negligible_set?" )"" (skosimp)"" (expand "null_set?" )"" (flatten)"" "integral_ae_eq" "f" "f1!1" "h" "phi(complement(X!1))*f1!1" ))"1" "integral_ae_eq" "f" "f2!1" "h" "phi(complement(X!1))*f2!1" ))"1" "1" "1" "1" replace -2)"1" replace -4)"1" "1" "integrable_diff" "f1" "phi(complement(X!1)) * f2!1" "f2" "phi(complement(X!1)) * f1!1" ))"1" "integral_diff" "f1" "phi(complement(X!1)) * f2!1" "f2" "phi(complement(X!1)) * f1!1" ))"1" "integral_nonneg" "f" "phi(complement(X!1)) * f2!1 - phi(complement(X!1)) * f1!1" ))"1" "1" assert )nil nil )"2" "2" "2" expand "subset?" )"2" "x!1" )"2" "x!1" )"2" expand "member" )"2" assert )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "ae_eq?" )"2" expand "restrict" )"2" expand "pointwise_ae?" )"2" expand "*" )"2" expand "ae?" )"2" expand "fullset" )"2" expand "ae_in?" )"2" "X!1" )"1" "1" expand "complement" )"1" expand "phi" )"1" expand "member" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" expand "negligible_set?" )"2" "X!1" )"2" expand "null_set?" )"2" assert )"2" expand "subset?" )"2" expand "member" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "ae_eq?" )"2" expand "restrict" )"2" expand "pointwise_ae?" )"2" expand "ae?" )"2" expand "fullset" )"2" expand "ae_in?" )"2" "X!1" )"1" "1" expand "complement" )"1" expand "phi" )"1" expand "member" )"1" expand "*" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "negligible_set?" )"2" "X!1" )"2" expand "null_set?" )"2" assert )"2" expand "subset?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "prod_measurable" )"2" "phi_is_simple" "X" "complement[T](X!1)" ))"1" rewrite "simple_is_measurable" )nil nil )"2" "measurable_complement" "a" "X!1" ))"2" expand "measurable_set?" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"2" "measurable_complement" "a" "X!1" ))"2" rewrite "prod_measurable" )"2" "phi_is_simple" "X" "complement[T](X!1)" ))"1" rewrite "simple_is_measurable" )nil nil )"2" expand "measurable_set?" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"(total_order?[real])" nil )"bool" measure_theory nil )"set" sets nil )"bool" measure_theory nil )nil integral nil )"bool" integral nil )nil integral nil )"bool" measure_space_def nil )nil measure_space_defnil )"[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 )"set" sets nil )nil measure_space nil )nil measure_space_def nil )"bool" measure_space_def nil )nil measure_space_def nil )nil measure_space nil )"bool" measure_space nil )nil measure_space nil )nil measure_space nil )"R" restrict nil )"set[T]" integral nil )"(S)" integral nil )"measurable_set[T, S]" integralnil )"bool" measure_theory nil )nil integral nil )nil integral nil )"[T -> real]" real_fun_ops "reals/" )"bool" sets nil )"bool" booleans nil )"real" reals nil )"bool" sets nil )"(partial_order?[set[T]])" nil )"real" reals nil )"(total_order?[real])" nil )nil integral nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil 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" 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" integral nil )"bool" measure_theory nil )nil measure_theory nil )"bool" measure_theory nil )"bool" measure_theory nil )"bool" measure_theory nil ))nil 3395600022"" (skosimp)"" (lemma "integrable_abs" ("f" "f!1" ))"" (copy -2)"" (expand "ae_le?" -1)"" (expand "pointwise_ae?" )"" (expand "ae?" )"" (expand "fullset" )"" (expand "ae_in?" )"" (skosimp)"" (typepred "E!1" )"" (expand "negligible_set?" )"" (skosimp)"" case " measurable_set?[T, S](complement[T](X!1))" )"1" "indefinite_integrable" "f" "abs(f!1)" "E" "complement(X!1)" ))"1" "nn_integrable_le" "g" "phi(complement(X!1))*abs(h!1)" "f" "phi(complement(X!1)) * abs(f!1)" ))"1" "1" "1" "nn_integrable_is_integrable" )"1" "phi(complement(X!1)) * abs(h!1)" )"1" rewrite "integral_nn" "1" rewrite "integral_nn" "1" "integrable_abs_def" "h" "phi(complement(X!1)) * h!1" ))"1" "abs(phi(complement(X!1)) * h!1)=phi(complement(X!1)) * abs(h!1)" )"1" assert )"1" "1" "integral_ae_eq" "f" "phi(complement(X!1)) * h!1" "h" "h!1" ))"1" "1" "1" assert )"1" "integral_abs" "f" "phi(complement(X!1)) * h!1" ))"1" replace "1" "phi(complement(X!1)) * abs(h!1)=abs(phi(complement(X!1)) * h!1)" )"1" "1" "I_0" "abs(integral(h!1))" )"1" "I_1" "integral(abs(phi(complement(X!1)) * h!1))" )"1" "integral_ae_eq" "f" "abs(f!1)" "h" "phi(complement(X!1)) * abs(f!1)" ))"1" "1" "1" assert )nil nil ))nil )"2" expand "ae_eq?" )"2" expand "restrict" )"2" expand "pointwise_ae?" )"2" expand "ae?" )"2" expand "fullset" )"2" expand "ae_in?" )"2" "X!1" )"1" "1" expand "*" )"1" expand "complement" )"1" expand "member" )"1" expand "phi" )"1" expand "member" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "negligible_set?" )"2" "X!1" )"2" assert )"2" expand "subset?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "prod_measurable" )"2" "simple_is_measurable" )"2" "phi[T, S](complement[T](X!1))" )"2" rewrite "phi_is_simple" )"2" expand "measurable_set?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "ae_eq?" )"2" expand "restrict" )"2" expand "pointwise_ae?" )"2" expand "ae?" )"2" expand "fullset" )"2" expand "ae_in?" )"2" "X!1" )"1" "1" expand "*" )"1" expand "complement" )"1" expand "member" )"1" expand "phi" )"1" expand "member" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "negligible_set?" )"2" "X!1" )"2" assert )"2" expand "subset?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" nil nil )"2" nil nil ))nil ))nil ))nil )"2" rewrite "prod_measurable" )"2" "2" "simple_is_measurable" )"2" "phi[T, S](complement[T](X!1))" )"2" rewrite "phi_is_simple" )"2" expand "measurable_set?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "subset?" )"2" "x!1" )"2" "x!1" )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "prod_measurable" )"2" "phi_is_simple" "X" "complement[T](X!1)" ))"1" "simple_is_measurable" )"1" "phi(complement[T](X!1))" )nil nil ))nil )"2" expand "measurable_set?" )"2" (propax) nil nil ))nil ))nil ))nil )"3" "3" "1" "1" (grind) nil nil ))nil )"2" "nn_integrable_is_nn_integrable" "f" "phi(complement(X!1)) * abs(f!1)" ))"1" "1" (propax) nil nil )"2" "2" (grind) nil nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil )"2" (expand "null_set?" )"2" "2" rewrite "measurable_complement" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil integral nil )"bool" integral 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 integral nil )nil integral nil )"bool" measure_theory nil )"bool" measure_theory nil )"bool" measure_theory nil )nil measure_theory nil )"bool" measure_theory nil )"measure_type" 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" 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 )NOT const-decl "[bool -> bool]" booleans nil )"bool" measure_theory nil )nil measure_space_def nil )"integrable" integral nil )nil integral nil )nil measure_space_def nil )nil real_types nil )"[T -> nonneg_real]" real_fun_ops "reals/" )nil integral nil )nil integral nil )nil integral nil )nil integral nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"measurable_function[T, S]" integral nil )"(partial_order?[set[T]])" nil )"(total_order?[real])" nil )"bool" sets nil )nil integral nil )nil integral nil )"real" integral nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" measure_theory nil )"set[T]" integral nil )"real" reals nil )"nnreal" nil )"bool" sets nil )"(S)" integral nil )"measurable_set[T, S]" integralnil )"R" restrict nil )nil measure_space nil )nil measure_space nil )"bool" measure_space nil )nil measure_space nil )nil measure_space nil )"[T, T -> boolean]" equalities nil )"bool" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil measure_space_defnil )"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 )"[T -> real]" real_fun_ops "reals/" )nil nn_integral nil )"bool" nn_integral nil )nil nn_integral nil )"measurable_function[T, S]" nil )"set" sets nil )"bool" measure_space_def nil )"set" sets nil )"bool" measure_theory nil ))nil 3452145726"" (skosimp)"" (lemma "sup_norm_prop" ("f" "phi(F!1) * h!1" ))"1" (flatten)"1" (name-replace "K" "sup_norm(phi(F!1) * h!1)" )"1" (case "nonempty?(fullset[T])" )"1" (case "K>=0" )"1" (lemma "isf_is_integrable" )"1" (inst - "K*phi(F!1)" )"1" "integral_ae_abs" "h" "phi(F!1) * h!1" "f" "K * phi(F!1)" ))"1" (case-replace "abs(K * phi(F!1))=K*phi(F!1)" )"1" (hide -1)"1" (rewrite "integral_scal" -1)"1" (rewrite "integral_phi" -1)"1" (assert )"1" "1" "1" (assert ) nil nil ))nil )"2" "2" expand "ae_le?" )"2" expand "pointwise_ae?" )"2" expand "ae?" )"2" expand "fullset" )"2" expand "ae_in?" )"2" "emptyset[T]" )"2" "2" expand "*" )"2" "x!1" )"2" expand "abs" "2" expand "phi" )"2" expand "member" )"2" "F!1(x!1)" )"1" assert )nil nil )"2" assert )"2" rewrite "abs_mult" )"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 )"2" (hide-all-but (-3 1))"2" (apply-extensionality :hide? t)"1" (grind) nil nil ) ("2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (-1 -2 1))"2" (expand "fullset" )"2" (expand "nonempty?" )"2" (expand "empty?" )"2" (skosimp)"2" (expand "member" )"2" (inst - "x!1" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "nonempty?" )"2" (case-replace "F!1=emptyset[T]" )"1" (hide -3 -4 -5)"1" "phi(emptyset[T]) * h!1 = lambda x: 0" )"1" (rewrite "integral_zero" )"1" (expand "mu" )"1" (typepred "m" )"1" (expand "measure?" )"1" (flatten)"1" expand "measure_empty?" )"1" replace -1)"1" expand "abs" )"1" "nn_integrable_zero" )"1" rewrite "nn_integrable_is_integrable" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (apply-extensionality :hide? t)"2" (expand "*" )"2" (expand "phi" )"2" (expand "member" )"2" expand "emptyset" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2 -3 -4 -2)"2" (apply-extensionality :hide? t)"2" (expand "emptyset" )"2" (expand "fullset" )"2" (expand "empty?" )"2" (inst - "x!1" )"2" (expand "member" )"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil )nil integral nil )nil measure_space_defnil )"bool" measure_space_def nil )"bool" measure_props nil )"measure_type" integral nil )nil generalized_measure_defnil )"bool" generalized_measure_def nil )nil extended_nnreal"extended_nnreal/" )nil real_types nil )nil measure_space_def nil )"bool" measure_space_def nil )"nat" measure_space nil )"sigma_algebra" 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 )"[T -> real]" real_fun_ops "reals/" )nil sup_norm nil )"bool" sup_norm 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 sup_norm nil )"measurable_function[T, S]" nil )"isf" integral nil )"nnreal" sup_norm nil )"[T, T -> boolean]" equalities nil )nil integral nil )NOT const-decl "[bool -> bool]" booleans nil )nil nn_integral nil )nil integral nil )"bool" nn_integral nil )nil nn_integral nil )"bool" generalized_measure_def nil )"nnreal" measure_props nil )"simple" integral nil )"isf" integral nil )"integrable" integral nil )"[T -> real]" real_fun_ops "reals/" )nil isf nil )"bool" isf nil )"[T -> nonneg_real]" real_fun_ops "reals/" )nil real_types nil )"isf" integral nil )"integrable" integral nil )nil integral nil )"real" reals nil )"measurable_function[T, S]" nil )"(total_order?[real])" nil )"bool" measure_theory nil )"(S)" integral nil )"null_set" 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 )"bool" sets nil )nil abs_lems "reals/" )"bool" booleans nil )"bool" measure_theory nil )"bool" measure_theory nil )"bool" measure_theory nil )"(total_order?[real])" nil )"nnreal" nil )nil integral nil )"(mu_fin?)" integral nil )"nnreal" integral nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"(strict_total_order?[real])" real_props nil )"real" reals nil )nil integral nil )"bool" integral nil )nil integral nil )nil integral nil )"bool" sets nil )"set" sets nil )"bool" sets nil )"(S)" integral nil )"measurable_set[T, S]" integralnil ))nil 3395602959"" (skosimp)"" (lemma "nn_integrable_is_nn_integrable" ("f" "abs(f!1)" ))"" (split -1)"1" (expand "nn_integrable?" )"1" (skosimp)"1" (typepred "u!1" )"1" (case "forall (n:nat): ae_0?(u!1(n))" )"1" (expand "pointwise_convergence?" )"1" (expand "convergent?" )"1" (skosimp)"1" "ae_eq_convergence" "F" "u!1" "G" "lambda (n:nat): lambda x: 0" "f" "abs(f!1)" ))"1" (split)"1" (hide-all-but (-1 1))"1" (expand "ae_convergence?" )"1" expand "ae_0?" )"1" expand "restrict" )"1" expand "pointwise_ae?" )"1" expand "ae?" )"1" expand "fullset" )"1" expand "ae_convergence_in?" )"1" expand "ae_in?" )"1" "1" "E!1" )"1" expand "negligible_set?" )"1" "1" "X!1" )"1" "1" expand "subset?" )"1" "x!1" )"1" assert )"1" "x!1" )"1" assert )"1" "hausdorff_convergence.unique_limit" "l1" "abs(f!1)(x!1)" "l2" "0" "u" "LAMBDA (n:nat): 0" ))"1" assert )"1" "1" expand "abs" )"1" "1" nil nil ))nil ))nil )"2" "2" expand "convergence?" )"2" "2" "0" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" expand "negligible_set?" )"2" "X!1" )"2" assert )"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 )"2" (hide-all-but (-3 1))"2" (expand "ae_convergence?" )"2" expand "fullset" )"2" expand "ae_convergence_in?" )"2" expand "ae_in?" )"2" "emptyset[T]" )"2" expand "emptyset" )"2" "2" expand "member" )"2" "x!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide-all-but (-1 1))"3" (skosimp)"3" "n!1" )"3" expand "ae_0?" )"3" expand "restrict" )"3" expand "pointwise_ae?" )"3" expand "ae_eq?" )"3" expand "restrict" )"3" expand "pointwise_ae?" )"3" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp)"2" (hide 2)"2" (lemma "isf_ae_ge_0" ("i" "u!1(n!1)" ))"2" (assert )"2" (hide 2)"2" (split)"1" (expand "ae_nonneg?" )"1" expand "pointwise_ae?" )"1" expand "ae?" )"1" expand "fullset" )"1" expand "ae_in?" )"1" "emptyset[T]" )"1" "1" assert )"1" expand "increasing_nn_isf?" )"1" "u!1(n!1)" )"1" expand "nn_isf?" )"1" "x!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "integral_nn" ("g" "abs(f!1)" ))"1" replace -1)"1" "1" expand "nn_integral" )"1" rewrite "limit_def" )"1" "nn_convergence" "u1" "u!1" "f" "abs(f!1)" "u2" "choose({u: increasing_nn_isf[T, S, m] | ")) "1" assert )"1" "1" "1" "hausdorff_convergence.limit_def" "v" "(isf_integral o " "l" "0" ))"1" replace -1 -6 rl)"1" replace -6)"1" "1" rewrite "limit_def" "1" "1" rewrite "metric_convergence_def" "1" expand "metric_converges_to" )"1" "isf_integral_pos" "i" "u!1(n!1)" ))"1" "1" case "isf_integral(u!1(n!1)) > 0" )"1" "1" "isf_integral(u!1(n!1))" )"1" "1" "n!1+n!2" )"1" assert )"1" expand "ball" )"1" expand "o " )"1" expand "increasing_nn_isf?" )"1" expand "pointwise_increasing?" )"1" "isf_integral_le" "i1" "u!1(n!1)" "i2" "u!1(n!1+n!2)" ))"1" "1" "I_0" "isf_integral(u!1(n!1))" )"1" "I_1" "isf_integral(u!1(n!1+n!2))" )"1" "1" nil nil ))nil ))nil ))nil )"2" "2" "x!1" )"2" expand "increasing?" )"2" "n!1" "n!1+n!2" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"2" assert )nil nil ))nil )"2" "2" expand "increasing_nn_isf?" )"2" expand "pointwise_increasing?" )"2" "u!1(n!1)" )"2" expand "nn_isf?" )"2" "x!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "nonempty?" )"2" expand "empty?" )"2" expand "member" )"2" "u!1" )nil nil ))nil ))nil ))nil ))nil )"2" expand "nonempty?" )"2" expand "empty?" )"2" "u!1" )"2" expand "member" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "nn_integrable_is_nn_integrable" "f" "abs(f!1)" ))"2" "1" (propax) nil nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1) (("2" (grind) nil nil )) nil ))nil ))nil ))nil )"[T -> nonneg_real]" real_fun_ops "reals/" )nil real_types nil )"bool" reals nil )nil integral nil )"bool" integral 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 integral nil )nil integral nil )"integrable" integral nil )"bool" nn_integral nil )nil nn_integral nil )"bool" nn_integral nil )nil sequences nil )nil nn_integral nil )"bool" nn_integral nil )nil isf nil )"bool" isf nil )"measure_type" integral nil )nil generalized_measure_defnil )"bool" generalized_measure_def nil )nil extended_nnreal"extended_nnreal/" )nil real_types nil )"sigma_algebra" integral nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )NOT const-decl "[bool -> bool]" booleans nil )nil isf nil )nil integral nil )nil nn_integral nil )nil hausdorff_convergence "topology/" )nil topological_convergence "topology/" )"T3" function_props nil )"real" isf nil )"bool" sets nil )"(p)" sets nil )"bool" sets nil )"bool" metric_space_def"metric_space/" )"bool" pointwise_convergence nil )"real" reals nil )"[T, T -> boolean]" equalities nil )"bool" real_fun_preds "reals/" )nil isf nil )"set[T]" metric_space_def "metric_space/" )"real" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"nonneg_int" nil )nil real_types nil )"nat" integral nil )"increasing_nn_isf[T, S, m]" integral nil )"(strict_total_order?[real])" real_props nil )"bool" reals nil )nil isf nil )nil metric_space"metric_space/" )nil nn_integral nil )"nnreal" nn_integral nil )"bool" measure_theory nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"bool" pointwise_convergencenil )"bool" measure_theory nil )"R" restrict nil )"measurable_set[T, S]" integralnil )"(S)" integral nil )"bool" measure_theory nil )"bool" measure_theory nil )"set[T]" integral nil )"bool" sets nil )"bool" sets nil )"bool" topological_convergence"topology/" )"real" reals nil )"(strict_total_order?[real])" real_props nil )"setofsets[T]" metric_space_def"metric_space/" )"[numfield, numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil hausdorff_convergence "topology/" )"bool" booleans nil )"(partial_order?[set[T]])" nil )nil measure_theory nil )"bool" measure_theory nil )set type-eq-decl nil sets nil )"bool" measure_theory nil )"set" sets nil )"bool" measure_theory nil )"(S)" integral nil )"null_set" 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 )"bool" measure_theory nil )nil measure_theory nil )"bool" topological_convergence "topology/" )"bool" measure_theory nil ))nil 3395603530"" (skosimp)"" (lemma "integral_ae_eq" ("f" "lambda x: 0" "h" "h!1" ))"1" (split -1)"1" (flatten)"1" (rewrite "integral_zero" ) (("1" (assert ) nil nil ))nil ))nil )"2" (hide 2)"2" (expand "ae_0?" )"2" (expand "ae_eq?" )"2" (expand "restrict" )"2" (expand "pointwise_ae?" )"2" (expand "ae?" )"2" (expand "fullset" )"2" (expand "ae_in?" )"2" (skosimp)"2" (inst + "E!1" )"2" (skosimp)"2" "x!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (rewrite "integrable_zero" ) nil nil ))nil ))nil )nil measure_space_defnil )"bool" measure_space_def nil )"sigma_algebra" integral nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )nil integral nil )"bool" integral 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 integral nil )nil integral nil )"bool" measure_theory nil )"bool" measure_theory nil )"set" sets nil )"bool" sets nil )"bool" booleans nil )set type-eq-decl nil sets nil ) (>= const-decl "bool" reals nil )nil real_types nil )nil extended_nnreal"extended_nnreal/" )"bool" generalized_measure_def nil )nil generalized_measure_defnil )"measure_type" integral nil )"bool" measure_theory nil )nil measure_theory nil )"bool" measure_theory nil )"bool" measure_theory nil )"(S)" integral nil )"measurable_set[T, S]" integralnil )"R" restrict nil )"bool" measure_theory nil )nil integral nil )nil integral nil ))nil 3391334061"" (skosimp)"" (lemma "integral_ae_eq" ("f" "f!1" "h" "abs(f!1)" ))"" (split -1)"1" (flatten)"1" (lemma "integral_abs_0" ("f" "f!1" ))"1" (assert ) nil nil )) nil ))nil )"2" (hide -2 2)"2" (expand "ae_nonneg?" )"2" (expand "ae_eq?" )"2" (expand "restrict" )"2" (expand "pointwise_ae?" )"2" (expand "ae?" )"2" (expand "fullset" )"2" (expand "ae_in?" )"2" (skosimp)"2" (inst + "E!1" )"2" (skosimp)"2" "x!1" )"2" assert )"2" expand "abs" )"2" expand "abs" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"[T -> nonneg_real]" real_fun_ops "reals/" )nil real_types nil )"bool" reals nil )nil measure_space_defnil )"bool" measure_space_def nil )"sigma_algebra" integral nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )nil integral nil )"bool" integral 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 integral nil )nil integral nil )"integrable" integral nil )"bool" measure_theory nil )"bool" measure_theory nil )"set" sets nil )"bool" sets nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"bool" booleans nil )set type-eq-decl nil sets nil )nil real_types nil )nil extended_nnreal"extended_nnreal/" )"bool" generalized_measure_def nil )nil generalized_measure_defnil )"measure_type" integral nil )"bool" measure_theory nil )nil measure_theory nil )"bool" measure_theory nil )"bool" measure_theory nil )"(S)" integral nil )"measurable_set[T, S]" integralnil )"R" restrict nil )"bool" measure_theory nil )nil integral nil ))nil 3409639019"" (induct "n" )"1" (skosimp)"1" (assert )"1" (expand "maximum" ) (("1" (propax) nil nil )) nil )) nil ))nil )"2" (skosimp*)"2" (inst - "w!1" )"2" (expand "maximum" 1)"2" (rewrite "integrable_max" ) nil nil )) nil ))nil ))nil ))nil )"measurable_function[T, S]" nil )"posint" nil )nil integral nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"measurable_function[T, S]" integral nil )nil naturalnumbers nil )"[T -> real]" real_fun_ops_aux "reals/" )nil sequences nil )nil integral nil )"bool" integral nil )nil integral nil )nil defined_types nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil ))nil 3409639019"" (induct "n" )"1" (skosimp)"1" (expand "minimum" ) (("1" (propax) nil nil )) nil )) nil )"2" (skosimp*)"2" (inst - "w!1" )"2" (expand "minimum" 1)"2" (rewrite "integrable_min" ) nil nil )) nil ))nil ))nil ))nil )"measurable_function[T, S]" nil )"posint" nil )"measurable_function[T, S]" integral nil )nil integral nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil naturalnumbers nil )"[T -> real]" real_fun_ops_aux "reals/" )nil sequences nil )nil integral nil )"bool" integral nil )nil integral nil )nil defined_types nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil ))nil 3452508415"" (skosimp)"" (split)"1" (flatten)"1" (rewrite "indefinite_integrable" )"1" (rewrite "indefinite_integrable" ) nil nil )) nil ))nil )"2" (flatten)"2" "integrable_add" "f1" "phi(E!1) * h!1" "f2" "phi(complement(E!1)) * h!1" ))"1" (expand "*" )"1" (expand "+" )"1" (expand "phi" )"1" (expand "complement" )"1" (expand "member" )"1" "(LAMBDA (x_1: T): IF NOT E!1(x_1) THEN 1 ELSE 0 ENDIF * h!1(x_1) +IF E!1(x_1) THEN 1 ELSE 0 ENDIF * h!1(x_1))=h!1") "1" (apply-extensionality :hide? t)"1" (case-replace "E!1(x!1)" )"1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ) ("3" (propax) nil nil ))nil ))nil ))nil ))nil )nil integral nil )nil integral nil )nil booleans 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" integral nil )"bool" measure_space_def nil )nil measure_space_def nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" integral nil )nil integral nil )"set" sets nil )"measurable_set" nil )"nat" measure_space nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[T -> real]" real_fun_ops "reals/" )nil integral nil )"[T -> real]" real_fun_ops "reals/" )NOT const-decl "[bool -> bool]" booleans nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[T, T -> boolean]" equalities nil )nil number_fields nil )"real" reals nil )"real" reals nil )"bool" sets nil ))nil 3452508415"" (skosimp) (("" (rewrite "indefinite_integrable" ) nil nil )) nil )nil integral nil )nil integral nil )nil booleans 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" integral nil )"bool" measure_space_def nil )nil measure_space_def nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" integral nil )nil integral nil ))nil ))nil 3452508415"" (skosimp) (("" (rewrite "indefinite_integrable" ) nil nil )) nil )"measurable_set" nil )nil integral nil )nil integral nil )nil booleans 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" integral nil )"bool" measure_space_def nil )nil measure_space_def nil )"set" sets nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" integral nil )nil integral nil ))nil ))nil 3452508680"" (skosimp)"" "integral_add" "f1" "phi(E!1) * f!1" "f2" "phi(complement(E!1)) * f!1" ))"" (replace -1 1 rl)"" (hide -1)"" (expand "phi" )"" (expand "complement" )"" (expand "member" )"" (expand "+" )"" (expand "*" )"" "(LAMBDA (x_1: T): IF NOT E!1(x_1) THEN 1 ELSE 0 ENDIF * f!1(x_1) +IF E!1(x_1) THEN 1 ELSE 0 ENDIF * f!1(x_1))=f!1") "" (apply-extensionality :hide? t)"" (case-replace "E!1(x!1)" )"1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"set" sets nil )nil measure_space_def nil )"bool" measure_space_def nil )"nat" measure_space nil )"sigma_algebra" 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 )"[T -> real]" real_fun_ops "reals/" )nil integral nil )"bool" integral 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 integral nil )nil integral nil )"measurable_set" nil )"[T -> real]" real_fun_ops "reals/" )NOT const-decl "[bool -> bool]" booleans nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[T, T -> boolean]" equalities nil )nil number_fields nil )"real" reals nil )"real" reals nil )"bool" sets nil ))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.0.734Bemerkung:
(vorverarbeitet am 2026-05-06)
¤ *Bot Zugriff
2026-05-26
