SSL riesz_representation.prf
Sprache: Lisp
(riesz_representationnil 3511191506"" (expand "connected?" )"" (skosimp*) (("" (ground) nil nil )) nil )) nil )"(total_order?[real])" nil )"bool" deriv_domain_def nil ))nil ))nil 3511191506"" (expand "not_one_element?" )"" (skosimp*)"" (inst-cp + "a" )"" (inst + "b" ) (("" (grind) nil nil )) nil )) nil ))nil ))nil )"boolean" notequal nil )nil riesz_interval_funs nil )"{bb: real | a < bb}" riesz_representationnil )"bool" reals nil )"real" riesz_representation nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans 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 )"(total_order?[real])" nil )"bool" deriv_domain_def nil ))nil ))nil 3492953409"" (subtype-tcc) nil nil )"(total_order?[real])" nil ))nil ))nil 3492953409"" (subtype-tcc) nil nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3492953409"" (skolem 1 ("ff" "gg" ))"" (flatten)"" (lemma "continuous_implies_bounded[a,b]" )"" (inst - "ff" )"" (expand "zero_off_int_and_bounded?" )"" (ground) nil nil )) nil ))nil ))nil ))nil ))nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil riesz_interval_funs nil )"bool" riesz_interval_funs nil )nil riesz_interval_funs nil )"(total_order?[real])" nil )nil riesz_interval_funsnil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"real" riesz_representation nil )nil booleans nil )"bool" reals nil )"{bb: real | a < bb}" riesz_representationnil ))nil ))nil 3492953409"" (skolem 1 ("ff" "gg" ))"" (case "NOT integrable?(a,b,gg,ff)" )"1" (hide 2)"1" (lemma "RS_integrable_cont_BV" )"1" (inst - "a" "b" "ff" "gg" )"1" (assert )"1" (typepred "ff" )"1" (expand "continuous_on_int?" )"1" (expand "continuous?" )"1" (skosimp*)"1" (inst - "x!1" )"1" (expand "continuous_at?" )"1" (skosimp*)"1" (inst - "epsilon!1" )"1" "1" "delta!1" )"1" "1" "y!1" )"1" (assert ) nil nil )"2" expand "restrict" +)"2" expand "Intab" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "restrict" +)"2" (expand "Intab" )"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (label "fint" -1)"2" (assert )"2" (name "SS" "integral(a,b,gg,ff)" )"2" (label "SSname" -1)"2" (lemma "integral_def" )"2" (inst - "a" "b" "ff" "gg" "SS" )"2" (split -)"1" (flatten)"1" (hide -2)"1" (split -)"1" (label "integrall?" -1)"1" case "FORALL (P:partition(a,b),xis:xis?(a,b,P)): abs(Rie_sum(a,b,gg,P,xis,ff)) <= total_variation(a,b,gg)(b)*fun_norm(ff)" )"1" case "FORALL (eps:posreal): abs(integral(a, b, gg, ff)) <= ") "1" "(abs(integral(a, b, gg, ff)) - ") "1" (assert ) nil nil ))nil )"2" "2" expand "integral?" )"2" "2" "integrall?" "eps/10" )"2" "2" "partition_exists" )"2" "a" "b" "delta!1" )"2" assert )"2" "2" "xis" "gen_xis(a,b,P!1)" )"2" "P!1" "xis" )"2" "P!1" )"2" assert )"2" "Rie_sum(a,b,gg,P!1,xis,ff)" )"1" "gen_xis" "width" "Rie_sum" "total_variation" "integral" "integrable?" ))nil nil )"2" "Riemann?_Rie" )"2" "a" "b" "ff" "gg" )"2" "1" "P!1" "xis" )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" "2" expand "Rie_sum" )"2" "sigma_abs[below(P`length-1)]" )"2" "2" case "sigma(0, P`length - 2, LAMBDA (n_1: below(P`length - 1)):") "1" (assert ) nil nil )"2" "2" "2" "total_variation(a,b,gg)(b)" )"2" assert )"2" "P" )"2" case "sigma(0, P`length - 2, LAMBDA (n_1: below(P`length - 1)):") "1" "fun_norm[a,b](ff)" )"1" assert )nil nil ))nil )"2" "2" expand "variation_on" )"2" "sigma_scal[below(P`length-1)]" )"2" "LAMBDA (n: below(P`length - 1)): " "fun_norm[a,b](ff)" "P`length-2" "0" )"2" replace "2" "2" rewrite "sigma_le" )"2" "2" "2" "n" )"2" "abs_mult" )"2" "ff(xis`seq(n))" "gg(P`seq(1 + n)) -gg(P`seq(n))" )"2" replace "2" case "abs(ff(xis`seq(n))) <= fun_norm(ff)" )"1" "abs(gg(P`seq(1 + n)) - gg(P`seq(n)))" )nil nil )"2" "fun_norm(ff)" )"2" "xis`seq(n)" )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" (propax) nil nil )"3" (propax) nil nil ))nil ))nil ))nil )"2" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (assert )"3" (typepred "b" ) (("3" (assert ) nil nil )) nil )) nil )"4" (assert ) nil nil ))nil ))nil )nil riesz_interval_funs nil )"bool" riesz_interval_funs nil )"bool" bounded_variation nil )"bool" rs_integral_def nil )nil riesz_interval_funs nil )"{bb: real | a < bb}" riesz_representationnil )"bool" reals nil )"real" riesz_representation nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil rs_integral_cont nil )"bool" continuity_ms_def nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )"(LAMBDA (x: INTab[a, b]): TRUE)" nil )"bool" sets nil )"(LAMBDA (x: INTab[a, b]): TRUE)" nil )"bool" booleans nil )"set[real]" riesz_interval_funs nil )set type-eq-decl nil sets nil )"R" restrict nil )"bool" continuity_ms_def nil )"{M: nnreal | AND " nil )"bool" riesz_interval_funs nil )"{M: nnreal | AND AND " bounded_variation nil )"nnreal" bounded_variation nil )"[bool, bool -> bool]" booleans nil )nil real_types nil )"[numfield, numfield -> numfield]" number_fields nil )"real" rs_integral_def nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil rs_integral_def nil )"[numfield, numfield -> numfield]" number_fields nil )nil rs_partition nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" sort_fseq "structures/" )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil fseqs "structures/" )nil fseqs "structures/" )nil naturalnumbers nil )"nnreal" nil )nil rs_integral_def nil )"real" reals nil )"xis?[INTab](a, b, P!1)" nil )"Continuous_Function[a, b]" nil )"(bounded_variation?(a, b))" nil )"partition[INTab](a, b)" nil )"bool" rs_integral_def nil )"xis?(a, b, P)" rs_integral_def nil )nil rs_partition nil )"posreal" nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"(total_order?[real])" nil )"real" reals nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )"real" reals nil )"posreal" nil )nil sigma "reals/" )"real" sigma "reals/" )"nnreal" sigma_below "reals/" )nil extra_real_propsnil )nil integers nil )"int" integers nil )nil real_props nil )nil sigma "reals/" )nil sigma "reals/" )OR const-decl "[bool, bool -> bool]" booleans nil )nil sigma "reals/" )nil sigma "reals/" )"posint" nil )"int" integers nil )"real" reals nil )nil rs_integral_def nil )"[T, T -> boolean]" equalities nil )"bool" rs_integral_def nil )"{S: real | integral?(a, b, gg, ff, S)}" nil ))nil 3492949849"" (skolem 1 ("gg" "ff" ))"" (lemma "RS_integrable_cont_BV" )"" (inst - "a" "b" "ff" "gg" )"" (assert )"" (hide 2)"" (typepred "ff" )"" (expand "continuous_on_int?" )"" (expand "restrict" )"" (expand "continuous?" )"" (skosimp*)"" (inst - "x!1" )"1" (expand "continuous_at?" )"1" (skosimp*)"1" (inst - "epsilon!1" )"1" "1" "delta!1" )"1" "1" "y!1" )"1" (assert ) nil nil )"2" expand "Intab" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "Intab" ) (("2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil riesz_interval_funs nil )"{bb: real | a < bb}" riesz_representationnil )"bool" reals nil )"real" riesz_representation nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans 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 rs_integral_cont nil )"(strict_total_order?[real])" real_props nil )NOT const-decl "[bool -> bool]" booleans nil )"R" restrict nil )"bool" continuity_ms_def nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )"(LAMBDA (x: INTab[a, b]): TRUE)" nil )"bool" sets nil )"(LAMBDA (x: INTab[a, b]): TRUE)" nil )"bool" booleans nil )"set[real]" riesz_interval_funs nil )set type-eq-decl nil sets nil )"bool" continuity_ms_def nil )"bool" bounded_variation nil )nil riesz_interval_funs nil )"bool" riesz_interval_funs nil ))nil ))nil 3492953553"" (skolem 1 "gg" )"" (expand "bounded_linear_operator?" )"" (split)"1" (expand "bounded_op?" )"1" (inst + "total_variation(a,b,gg)(b)" )"1" (skolem 1 "f" )"1" (lemma "integral_norm_bounded" )"1" (inst - "f" "gg" ) (("1" (assert ) nil nil )) nil ))nil ))nil )"2" (typepred "b" ) (("2" (assert ) nil nil )) nil )"3" (assert ) nil nil ) ("4" (assert ) nil nil ))nil ))nil )"2" (expand "linear_op?" )"2" (split)"1" (expand "additive_op?" )"1" (skolem 1 ("ff" "hh" ))"1" (lemma "integral_sum" )"1" (inst?)"1" (assert )"1" (split -)"1" (expand "+" ) (("1" (assert ) nil nil ))nil )"2" (hide 2)"2" (typepred "ff" )"2" (lemma "RS_integrable_cont_BV" )"2" "2" assert )"2" "2" expand "continuous_on_int?" )"2" expand "continuous?" )"2" "2" "x!1" )"1" expand "continuous_at?" )"1" "1" "epsilon!1" )"1" "1" "delta!1" )"1" "1" "y!1" )"1" assert )nil nil )"2" expand "restrict" )"2" expand "Intab" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "restrict" )"2" expand "Intab" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide 2)"3" (lemma "RS_integrable_cont_BV" )"3" (inst?)"3" assert )"3" "3" "hh" )"3" expand "continuous_on_int?" )"3" expand "continuous?" )"3" "3" "x!1" )"1" expand "continuous_at?" )"1" "1" "epsilon!1" )"1" "1" "delta!1" )"1" "1" "y!1" )"1" assert )nil nil )"2" expand "restrict" )"2" expand "Intab" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "restrict" )"2" expand "Intab" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "const_inv_op?" )"2" (skolem 1 ("f" "c" ))"2" (lemma "integral_scal" )"2" (inst?)"2" (assert )"2" (hide 2)"2" (lemma "RS_integrable_cont_BV" )"2" (inst?)"2" (assert )"2" "2" "f" )"2" expand "continuous_on_int?" )"2" expand "continuous?" )"2" "2" "x!1" )"1" expand "continuous_at?" )"1" "1" "epsilon!1" )"1" "1" "delta!1" )"1" "1" "y!1" )"1" assert )nil nil )"2" expand "restrict" )"2" expand "Intab" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "restrict" )"2" expand "Intab" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" nil )"bool" riesz_linear_functionals nil )"bool" riesz_linear_functionals nil )nil rs_integral_prep nil )"real" reals nil )"(LAMBDA (x: INTab[a, b]): TRUE)" nil )"(LAMBDA (x: INTab[a, b]): TRUE)" nil )"bool" riesz_linear_functionals nil )nil rs_integral_prep nil )"real" reals nil )"(LAMBDA (x: INTab[a, b]): TRUE)" nil )"(LAMBDA (x: INTab[a, b]): TRUE)" nil )nil rs_integral_cont nil )"bool" continuity_ms_def nil )nil real_types nil )nil real_types nil )"(LAMBDA (x: INTab[a, b]): TRUE)" nil )"bool" sets nil )"(LAMBDA (x: INTab[a, b]): TRUE)" nil )"bool" booleans nil )"set[real]" riesz_interval_funs nil )set type-eq-decl nil sets nil )"bool" continuity_ms_def nil )"[T -> real]" real_fun_ops "reals/" )"bool" riesz_bounded_functionals nil )NOT const-decl "[bool -> bool]" booleans nil )nil riesz_interval_funs nil )"bool" riesz_interval_funs nil )"(total_order?[real])" nil )"nnreal" nil )nil riesz_representation nil )"{M: nnreal | AND AND " bounded_variation nil )"nnreal" bounded_variation nil )nil rs_partition nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" sort_fseq "structures/" )"R" restrict nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil fseqs "structures/" )nil fseqs "structures/" )nil naturalnumbers nil )"bool" reals nil )"[T, T -> boolean]" equalities nil )"[bool, bool -> bool]" booleans nil )"bool" bounded_variation nil )nil riesz_interval_funs nil )nil real_types nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans 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 )"real" riesz_representation nil )"bool" reals nil )"{bb: real | a < bb}" riesz_representationnil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3492957266 ("" (subtype-tcc) nil nil )"(total_order?[real])" nil ))nil ))nil 3492957266"" (skolem 1 ("ff" "gg" ))"" (lemma "integral_norm_bounded" )"" (expand "fun_to_op" )"" (inst - "ff" "gg" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )nil riesz_representation 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 )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )"real" riesz_representation nil )"bool" reals nil )"{bb: real | a < bb}" riesz_representationnil )nil riesz_interval_funs nil )"bool" riesz_interval_funs nil )nil riesz_interval_funs nil )"bool" bounded_variation nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"nnreal" nil )"C_Bounded_Linear_Operator" nil ))nil 3492957695"" (skeep)"" (expand "-" )"" (expand "char_fun" )"" (decompose-equality) (("" (grind) nil nil )) nil )) nil ))nil ))nil )"[T -> real]" real_fun_ops "reals/" )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"[T, T -> boolean]" equalities nil )nil number_fields nil )nil riesz_interval_funs nil )"{bb: real | a < bb}" riesz_representationnil )"bool" reals nil )"real" riesz_representation nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans 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 )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"nnreal" riesz_representation nil ))nil 3492959104 ("" (subtype-tcc) nil nil ) nil nil ))nil 3492959104 ("" (subtype-tcc) nil nil ) nil nil ))nil 3492959104 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil naturalnumbers nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )"real" riesz_representation nil )"bool" reals nil )"{bb: real | a < bb}" riesz_representationnil )nil riesz_interval_funs nil )nil fseqs "structures/" )nil fseqs "structures/" )"[T, T -> boolean]" equalities nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"R" restrict nil )"bool" sort_fseq "structures/" )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )nil rs_partition nil )"[numfield, numfield -> numfield]" number_fields nil )nil rs_integral_def nil )"bool" riesz_interval_funs nil )nil integers nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3492959104"" (skeep)"" (typepred "fr" )"" (expand "bounded_on_int?" )"" (skosimp*)"" (inst + "M!1*(P`length+2)" )"" (skosimp*)"" case "FORALL (nnn:below(P`length-1)): abs(sigma[below(P`length - 1)] LAMBDA (n: below(P`length - 1)):") "1" (inst?) (("1" (assert ) nil nil )) nil )"2" (hide 2)"2" (induct "nnn" )"1" (flatten)"1" (expand "sigma" )"1" (expand "sigma" )"1" (inst - "xis`seq(0)" )"1" (expand "char_fun" )"1" "1" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skolem 1 "nnn" )"2" (flatten)"2" (expand "sigma" +)"2" (inst - "xis`seq(1+nnn)" )"2" (grind :exclude "sigma" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" riesz_interval_funs nil )nil riesz_interval_funs nil )"{bb: real | a < bb}" riesz_representationnil )"bool" reals nil )"real" riesz_representation nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"real" reals nil )"nnreal" nil )nil abs_lems "reals/" )"(strict_total_order?[real])" real_props nil )"real" reals nil )nil bounded_nat_inductions nil )nil defined_types nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"posint" nil )"(total_order?[real])" nil )"int" integers nil )"posint" nil )"real" reals nil )"int" integers nil )nil real_types nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )OR const-decl "[bool, bool -> bool]" booleans nil )nil sigma "reals/" )nil sigma "reals/" )"real" sigma "reals/" )nil rs_integral_def nil )"nnreal" riesz_representation nil )nil rs_partition nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" sort_fseq "structures/" )"R" restrict nil )"[numfield, numfield -> numfield]" number_fields nil )"[T, T -> boolean]" equalities nil )"bool" reals nil )nil fseqs "structures/" )nil fseqs "structures/" )nil naturalnumbers nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil real_types nil )"bool" reals nil )"nnreal" nil ))nil ))nil 3492960304"" (skeep)"" (typepred "f" )"" (expand "continuous_on_int?" )"" case "uniformly_continuous?[INTab,real_dist,real,real_dist](f,Intab)" )"1" (expand "uniformly_continuous?" )"1" (inst - "eps" )"1" (skosimp*)"1" (inst + "delta!1" )"1" (skeep)"1" (label "Pwidth" -4)"1" (label "Pinc" -3)"1" (label "funif" -1)"1" (hide -2)"1" (skosimp*)"1" "part_in" )"1" case "FORALL (x: INTab, P: partition(a, b)): AND x <= P`seq(ii + 1) AND ") "1" "1" "x!1" "P" )"1" assert )"1" "1" case "step_approx(P,xis)(f)(x!1) = f(xis`seq(ii!1))" )"1" "funif" "x!1" "xis`seq(ii!1)" )"1" expand "real_dist" )"1" assert )"1" "1" "1" "Pinc" )"1" case "P`seq(1+ii!1)-P`seq(ii!1) < delta!1" )"1" "Pwidth" )"1" "xis" )"1" "ii!1" )"1" assert )"1" "char_fun" ))nil nil ))nil ))nil ))nil ))nil )"2" "width_lem" )"2" "a" "b" "P" "ii!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "restrict" )"2" expand "Intab" )"2" assert )nil nil ))nil ))nil )"3" expand "restrict" )"3" expand "Intab" )"3" nil nil ))nil ))nil ))nil )"2" "2" expand "step_approx" )"2" "sigma_split[below(P`length-1)]" )"2" "LAMBDA (n: below(P`length - 1)): " "P`length-2" "0" "ii!1" )"2" assert )"2" replace -1)"2" "2" "sigma_split[below(P`length-1)]" )"2" "LAMBDA (n: below(P`length - 1)): " "ii!1" "0" "ii!1-1" )"2" assert )"2" replace "2" "2" expand "sigma" "2" expand "sigma" "2" case "sigma(0, ii!1 - 1, LAMBDA (n: below(P`length - 1)):AND sigma(1 + ii!1, P`length - 2,LAMBDA (n: below(P`length - 1)):") "1" "1" assert )nil nil ))nil )"2" "2" "1" rewrite "sigma_restrict_eq_0" )"1" "1" "jj" )"1" case "char_fun(P`seq(jj), P`seq(1 + jj))(x!1) = 0" )"1" assert )nil nil )"2" "2" "jj" )"2" expand "strictly_increasing?" )"2" "Pinc" "jj" "1+jj" )"2" "Pinc" "ii!1" "ii!1+1" )"2" assert )"2" "P" )"2" expand "increasing?" )"2" "1+jj" "ii!1" )"2" assert )"2" expand "char_fun" )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "sigma_restrict_eq_0" )"2" "2" "jj" )"2" expand "strictly_increasing?" )"2" "Pinc" "jj" "1+jj" )"2" "Pinc" "ii!1" "ii!1+1" )"2" assert )"2" "P" )"2" expand "increasing?" )"2" "ii!1+1" "jj" )"2" assert )"2" expand "char_fun" )"2" "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 ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "funif" "Pinc" "Pwidth" 2))"2" "yy" "PP" ))"2" "2" "a" "b" "yy" "PP" )"2" assert )"2" assert )"2" "a" "b" "yy" "PP" )"2" assert )"2" "2" case "yy = PP`seq(1+ii!1)" )"1" case "PP`seq(1+ii!1) = b" )"1" "ii!1" )"1" assert )"1" expand "char_fun" )"1" nil nil ))nil ))nil ))nil )"2" "ii!1+1" )"1" assert )"1" "PP" )"1" expand "increasing?" )"1" "1+ii!1" "2+ii!1" )"1" assert )"1" expand "strictly_increasing?" )"1" "1+ii!1" "2+ii!1" )"1" assert )"1" expand "char_fun" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "PP" )"2" "2+ii!1" )"1" nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )"2" "a" "b" "yy" "PP" )"2" assert )"2" "2" "ii!1" )"2" assert )"2" expand "char_fun" )"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 ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (lemma "Heine[real,real_dist,real,real_dist]" )"2" "ff" "LAMBDA (xy:real): IF Intab(xy) THEN f(xy) ELSE 0 ENDIF" )"1" (inst - "Intab" "ff" )"1" (assert )"1" (split -)"1" (hide-all-but (-1 1))"1" (expand "uniformly_continuous?" )"1" (skosimp*)"1" (inst - "epsilon!1" )"1" "1" "delta!1" )"1" "1" "x!1" "p!1" )"1" assert )"1" expand "ff" )"1" case "Intab(x!1) AND Intab(p!1)" )"1" "1" (assert ) nil nil ))nil )"2" expand "Intab" )"2" (propax) nil nil ))nil ))nil ))nil ))nil )"2" expand "Intab" )"2" (propax) nil nil ))nil )"3" expand "Intab" )"3" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (hide -1)"2" (expand "continuous?" )"2" (skosimp*)"2" "x!1" )"1" expand "continuous_at?" )"1" "1" "epsilon!1" )"1" "1" "delta!1" )"1" "1" "y!1" )"1" expand "member" )"1" expand "ball" )"1" expand "ff" )"1" assert )nil nil ))nil ))nil ))nil )"2" assert )"2" "y!1" )"2" expand "Intab" )"2" "2" assert )"2" expand "restrict" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "x!1" )"2" expand "Intab" )"2" assert )"2" "2" assert )"2" expand "restrict" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (lemma "closed_intervals_compact" )"3" (inst - "a" "b" )"3" (expand "Intab" )"3" (propax) nil nil )) nil ))nil ))nil )"4" (hide-all-but -1)"4" (expand "empty?" )"4" (inst - "a" )"4" (expand "member" )"4" expand "Intab" )"4" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (expand "Intab" )"2" (skosimp*) (("2" (ground) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"3" (hide-all-but 1) (("3" (grind) nil nil )) nil )"4" (hide-all-but 1) (("4" (grind) nil nil )) nil ))nil ))nil ))nil ))nil )nil riesz_interval_funs nil )"bool" riesz_interval_funs nil )nil riesz_interval_funs nil )"{bb: real | a < bb}" riesz_representationnil )"bool" reals nil )"real" riesz_representation nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"set[real]" riesz_interval_funs nil )"bool" uniform_continuity nil )"nnreal" real_metric_space nil )"R" restrict nil )nil real_types nil )"bool" reals nil ) (set type-eq-decl nil sets nil )"set" sets nil )"bool" metric_spaces_def nil )nil real_types nil )"bool" reals nil )nil real_types nil )"(total_order?[S])" nil )"(dichotomous?[S])" nil )"(partial_order?[S])" nil )"(preorder?[S])" nil )"(transitive?[S])" nil )"(antisymmetric?[S])" nil )"(reflexive?[S])" nil )"posint" nil )nil naturalnumbers nil )nil fseqs "structures/" )nil fseqs "structures/" )"[T, T -> boolean]" equalities nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" sort_fseq "structures/" )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )nil rs_partition nil )"[bool, bool -> bool]" booleans nil )"bool" sort_fseq "structures/" )"[numfield, numfield -> numfield]" number_fields nil )"nnreal" riesz_representation nil )nil sigma "reals/" )"(strict_total_order?[real])" real_props nil )"odd_int" integersnil )"real" sigma "reals/" )"int" integers nil )nil integers nil )nil sigma "reals/" )"real" reals nil )"[numfield, numfield -> numfield]" number_fields nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil sigma "reals/" )nil sigma "reals/" )"real" reals nil )"INTab[a, b]" riesz_representation nil )"partition[INTab](a, b)" riesz_representationnil )"xis?[INTab](a, b, P)" riesz_representationnil )"below(P`length - 1)" riesz_representationnil )"posint" nil )"(total_order?[real])" nil )"int" integers nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )nil rs_partition nil )"(bounded_on_int?[a, b])" nil )"bool" riesz_interval_funs nil )nil rs_integral_def nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"below(PP`length - 1)" riesz_representationnil )"partition[INTab](a, b)" riesz_representationnil )nil rs_partition nil )nil uniform_continuity nil )"(restrict[real, INTab[a, b], boolean](Intab))" nil )"(restrict[real, INTab[a, b], boolean](Intab))" nil )"[real -> real]" riesz_representation nil )"bool" continuity_ms_def nil )"(Intab)" riesz_representation nil )"set[T]" metric_spaces nil )"bool" sets nil )"(Intab)" riesz_representation nil )"bool" continuity_ms_def nil )nil real_metric_space nil )"bool" sets nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"bool" metric_spaces_def nil )"bool" metric_spaces_def nil )"bool" metric_spaces_def nil )"odd_int" integers nil )"real" reals nil )"real" reals nil ))nil 3493977883"" (expand "fullset" )"" (expand "extend" )"" (expand "bounded_linear_subspace?" )"" (ground)"1" (expand "funs_sum_closed?" )"1" (skolem 1 ("ff" "gg" ))"1" (ground)"1" (typepred "ff" )"1" (typepred "gg" )"1" (lemma "sum_continuous" )"1" (inst?)"1" (assert )"1" (expand "continuous_on_int?" )"1" (inst?) (("1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "funs_const_closed?" )"2" (skolem 1 ("ff" "cc" ))"2" (ground)"2" (typepred "ff" )"2" (lemma "scal_continuous" )"2" (inst?)"2" (assert )"2" (expand "continuous_on_int?" )"2" (inst?) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (expand "funs_bounded?" )"3" (skolem 1 "ff" )"3" (typepred "ff" )"3" (lemma "continuous_implies_bounded[a,b]" )"3" (inst - "ff" ) nil nil )) nil ))nil ))nil ))nil )"4" (expand "funs_contain_constants?" )"4" (skeep)"4" (ground)"4" (expand "continuous_on_int?" )"4" (expand "continuous?" )"4" (expand "continuous_at?" )"4" (assert )"4" (expand "ball" )"4" (expand "real_dist" )"4" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"5" (expand "funs_contain_continuous?" )"5" (skolem 1 "ff" )"5" (flatten) (("5" (ground) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )"R" extend nil )"bool" booleans nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"bool" riesz_interval_funs nil )nil riesz_interval_funs nil )"{bb: real | a < bb}" riesz_representationnil )"bool" reals nil )"real" riesz_representation nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" booleans nil )nil booleans nil )nil booleans nil )nil metric_space_real_fun nil )"bool" reals nil )nil real_types nil )"R" restrict nil )"nnreal" real_metric_space nil )"set[real]" riesz_interval_funs nil )set type-eq-decl nil sets nil )"bool" riesz_function_sets nil )nil metric_space_real_fun nil )"bool" riesz_function_sets nil )nil riesz_interval_funsnil )nil riesz_interval_funs nil )"bool" riesz_function_sets nil )"bool" continuity_ms_def nil )"set[T]" metric_spaces nil )nil abs_lems "reals/" )"real" reals nil )"bool" sets nil )"bool" continuity_ms_def nil )"bool" riesz_function_sets nil )"bool" riesz_function_setsnil )"bool" riesz_function_setsnil )"set" sets nil ))nil ))nil 3493978249"" (expand "fullset" )"" (expand "extend" )"" (expand "bounded_linear_subspace?" )"" (ground)"1" (expand "funs_sum_closed?" )"1" (skolem 1 ("ff" "gg" ))"1" (ground)"1" (typepred "ff" )"1" (typepred "gg" )"1" (expand "bounded_on_int?" )"1" (skosimp*)"1" (inst + "M!1+M!2" )"1" (skosimp*)"1" (inst - "x!1" )"1" "x!1" )"1" "zero_off_int?" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "funs_const_closed?" )"2" (skolem 1 ("ff" "cc" ))"2" (ground)"2" (typepred "ff" )"2" (expand "bounded_on_int?" )"2" (skosimp*)"2" (inst + "abs(cc)*M!1" )"2" (skosimp*)"2" (inst - "x!1" )"2" (expand "*" )"2" rewrite "abs_mult" )"2" "abs(cc)" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (expand "funs_bounded?" ) (("3" (propax) nil nil )) nil )"4" (expand "funs_contain_constants?" )"4" (skeep)"4" (ground)"4" (expand "bounded_on_int?" )"4" (inst + "abs(c)" ) (("4" (grind) nil nil )) nil ))nil ))nil ))nil ))nil )"5" (expand "funs_contain_continuous?" )"5" (skolem 1 "ff" )"5" (flatten)"5" (ground)"5" (lemma "continuous_implies_bounded[a,b]" )"5" (inst - "ff" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"R" extend nil )"bool" booleans nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"bool" riesz_interval_funs nil )nil riesz_interval_funs nil )"{bb: real | a < bb}" riesz_representationnil )"bool" reals nil )"real" riesz_representation nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" booleans nil )nil booleans nil )nil booleans nil )"nnreal" nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil real_types nil )"bool" reals nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[T -> real]" real_fun_ops "reals/" )"real" reals nil )"bool" riesz_function_sets nil )"real" reals nil )"[T -> real]" real_fun_ops "reals/" )nil extra_real_propsnil )"(total_order?[real])" nil )nil real_props nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )"[numfield -> numfield]" number_fields nil )"nnreal" nil )"bool" riesz_function_sets nil )"bool" riesz_function_sets nil )"bool" riesz_function_sets nil )"bool" riesz_interval_funs nil )nil riesz_interval_funs nil )nil riesz_interval_funsnil )"bool" riesz_function_setsnil )"bool" riesz_function_setsnil )"set" sets nil ))nil )nil 3493978219";;; Proof IMP_riesz_bounded_functionals_TCC1-1 for formula riesz_representation.IMP_riesz_bounded_functionals_TCC1" expand "fullset" )";;; Proof IMP_riesz_bounded_functionals_TCC1-1 for formula riesz_representation.IMP_riesz_bounded_functionals_TCC1" expand "extend" )";;; Proof IMP_riesz_bounded_functionals_TCC1-1 for formula riesz_representation.IMP_riesz_bounded_functionals_TCC1" expand "bounded_linear_subspace?" )";;; Proof IMP_riesz_bounded_functionals_TCC1-1 for formula riesz_representation.IMP_riesz_bounded_functionals_TCC1" "1" (expand "funs_sum_closed?" )"1" (skolem 1 ("ff" "gg" ))"1" (ground)"1" (typepred "ff" )"1" (typepred "gg" )"1" (expand "zero_off_int_and_continuous?" )"1" (ground)"1" (lemma "sum_continuous" )"1" (inst?) (("1" (assert ) nil )))))"2" (expand "zero_off_int?" )"2" (skosimp*)"2" (inst - "y!1" )"2" "y!1" )"2" assert )"2" expand "+" )"2" assert )nil )))))))))))))))))))))))))))"2" (expand "funs_const_closed?" )"2" (skolem 1 ("ff" "cc" ))"2" (ground)"2" (typepred "ff" )"2" (expand "zero_off_int_and_continuous?" )"2" (ground)"1" (lemma "scal_continuous" )"1" (inst?) (("1" (assert ) nil )))))"2" (expand "zero_off_int?" )"2" (skosimp*)"2" (inst - "y!1" )"2" (expand "*" )"2" (assert ) nil )))))))))))))))))))))"3" (expand "funs_bounded?" )"3" (skolem 1 "ff" )"3" (typepred "ff" )"3" (expand "zero_off_int_and_continuous?" )"3" (flatten)"3" (lemma "continuous_implies_bounded[a,b]" )"3" (inst - "ff" )"3" (expand "zero_off_int_and_bounded?" )"3" (ground) nil )))))))))))))))))"4" (expand "funs_zero_off_int?" )"4" (skolem 1 "ff" )"4" (typepred "ff" )"4" (expand "zero_off_int_and_continuous?" )"4" (expand "zero_off_int?" )"4" (flatten) nil )))))))))))"5" (expand "funs_contain_constants?" )"5" (skeep)"5" (ground)"5" (expand "zero_off_int_and_continuous?" )"5" (split)"1" (expand "continuous?" )"1" (skeep)"1" (expand "continuous_at?" )"1" (skosimp*)"1" (inst + "1" )"1" (grind) nil )))))))))))"2" (grind) nil )))))))))))"6" (expand "funs_contain_continuous?" )"6" (skolem 1 "ff" )"6" (flatten) (("6" (ground) nil ))))))))))))))";;; developed with shostak decision procedures") nil nil )nil 3493977883"" (assuming-tcc) nil nil ) nil nil ))nil 3492949849"" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )"real" riesz_representation nil )"bool" reals nil )"{bb: real | a < bb}" riesz_representationnil )nil riesz_interval_funs nil )"bool" riesz_interval_funs nil )nil riesz_linear_functionals nil )"bool" nil )nil riesz_hahn_banach nil )"bool" bounded_variation nil )"nnreal" bounded_variation nil )"bool" riesz_linear_functionals nil )"bool" riesz_linear_functionals nil )"bool" riesz_linear_functionals nil )"int" integers nil )nil rs_partition nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" sort_fseq "structures/" )"R" restrict nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )"bool" reals nil )nil fseqs "structures/" )nil fseqs "structures/" )nil naturalnumbers nil )"bool" riesz_bounded_functionals nil )"real" reals nil ))nil ))nil 3495206890"" (auto-rewrite + "member" )"" (skeep)"" (lemma "Hahn_Banach" )"" (inst - "LC" )"" (skeep -)"" "gg" "(LAMBDA (x:INTab): IF x = a THEN 0 ELSE LB(char_fun(a,x)) ENDIF)" )"1" (label "ggname" -1)"1" (label "opeq" -2)"1" (label "LBLC" -3)"1" case "(FORALL (P:partition(a,b)): strictly_increasing?(P) IMPLIES variation_on(a,b,P)(gg) <= op_norm[a,b,Continuous_Function[a,b]](LC))" )"1" (label "VPle" -1)"1" case "total_variation(a,b,gg)(b) <= op_norm[a,b,Continuous_Function[a,b]](LC)" )"1" (label "TVle" -1)"1" (inst + "gg" )"1" case "LC = fun_to_op(gg)" )"1" assert )"1" case "op_norm[a,b,Continuous_Function[a,b]](LC) <= total_variation(a,b,gg)(b)" )"1" (assert ) nil nil )"2" "2" "TVle" )"2" "fun_to_op_bound" )"2" "op_norm[a,b,Continuous_Function[a,b]](LC)" )"2" "total_variation(a,b,gg)(b)" )"2" assert )"2" "2" "f!1" )"2" "f!1" "gg" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" case "FORALL (epsil:posreal,ff:Continuous_Function[a,b]): EXISTS (delta:posreal): FORALL (P:partition(a,b),xis:xis?(a,b,P)): width(a,b,P)<delta and strictly_increasing?(P) IMPLIES abs(LB(step_approx(P,xis)(ff))-fun_to_op(gg)(ff)) < epsil" )"1" case "FORALL (ff:Continuous_Function[a,b]): LC(ff) = fun_to_op(gg)(ff)" )"1" nil nil )"2" "2" "2" case "FORALL (epsil:posreal): abs(LC(ff)-fun_to_op(gg)(ff)) < 32*epsil" )"1" case "abs(LC(ff)-fun_to_op(gg)(ff)) = 0" )"1" "abs_eq_0" )"1" "1" assert )nil nil ))nil ))nil )"2" "2" "abs(LC(ff)-fun_to_op(gg)(ff))/64" )"1" assert )nil nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" case "FORALL (epsil:posreal,ff:Continuous_Function[a,b]): EXISTS (delta:posreal): FORALL (P:partition(a,b),xis:xis?(a,b,P)): AND width(a,b,P)<delta IMPLIES abs(LC(ff)-LB(step_approx(P,xis)(ff)))<epsil") "1" "1" "epsil" "ff" )"1" "epsil" "ff" )"1" "1" "partition_exists" )"1" "a" "b" "min(delta!1,delta!2)" )"1" assert )"1" "1" "SSP" "strictly_sort(P)" )"1" case "width(a,b,SSP) < min(delta!1,delta!2)" )"1" "1" "1" "xis" "gen_xis(a,b,SSP)" )"1" "SSP" "xis" )"1" assert )"1" "SSP" "xis" )"1" assert )"1" "1" "stop_approx" "fun_to_op" ))nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "partition_union_is_strictly_sort" )"2" "a" "b" )"2" assert )"2" "P" )"2" "partition_union_width" )"2" "a" "b" )"2" assert )"2" "P" "P" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "partition_strictly_sort" )"3" "a" "b" )"3" assert )"3" "P" )"3" "3" assert )"3" "3" "i!1" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "LB" )"2" expand "bounded_linear_operator?" )"2" "2" expand "bounded_op?" )"2" "2" "step_approx_def" )"2" "ff!1" "epsil!1/(M!1+1)" )"2" "2" "delta!1" )"2" "2" "P" "xis" )"2" assert )"2" "LBLC" "ff!1" )"2" replace "LBLC" "2" case "LB(ff!1) - LB(step_approx(P, xis)(ff!1)) = LB(ff!1-step_approx(P,xis)(ff!1))" )"1" replace "1" "ff!1 - step_approx(P, xis)(ff!1)" )"1" case "fun_norm(ff!1 - step_approx(P, xis)(ff!1)) <= epsil!1/(M!1+1)" )"1" "1" assert )nil nil ))nil )"2" "2" "fun_norm(ff!1 - step_approx(P, xis)(ff!1))" )"2" "epsil!1/(M!1+1)" )"2" assert )"2" "2" "x!1" )"2" expand "-" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "linear_op?" )"2" "2" expand "additive_op?" )"2" "ff!1" "-1*step_approx(P,xis)(ff!1)" )"1" expand "const_inv_op?" )"1" "step_approx(P,xis)(ff!1)" "-1" )"1" case "ff!1+-1*step_approx(P,xis)(ff!1) = ff!1-step_approx(P,xis)(ff!1)" )"1" assert )nil nil )"2" "2" "step_approx" ))"2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "step_approx(P,xis)(ff!1)" )"2" assert )"2" expand "*" )"2" assert )"2" expand "bounded_on_int?" )"2" "2" "M!2" )"2" "2" "x!1" )"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 )"3" "3" expand "bounded_on_int?" )"3" "step_approx(P,xis)(ff!1)" )"3" "ff!1" )"3" "continuous_implies_bounded" )"3" "ff!1" )"3" "3" expand "bounded_on_int?" )"3" "3" "M!2+M!3" )"3" "3" "x!1" )"3" "x!1" )"3" "step_approx" ))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 ))nil ))nil )"2" case "FORALL (ff:Continuous_Function[a,b],P:partition(a,b),xis:xis?(a,b,P)): strictly_increasing?(P) IMPLIES LB(step_approx(P,xis)(ff)) = Rie_sum(a,b,gg,P,xis,ff)" )"1" "RS_integrable_cont_BV" )"1" "1" "a" "b" "ff" "gg" )"1" assert )"1" "1" "1" expand "integrable?" "1" "1" "integral_def" )"1" "a" "b" "ff" "gg" "S!1" )"1" assert )"1" case "fun_to_op(gg)(ff) = S!1" )"1" replace "1" expand "integral?" )"1" "epsil" )"1" "1" "delta!1" )"1" "1" "P!1" )"1" assert )"1" "Rie_sum(a,b,gg,P!1,xis!1,ff)" )"1" "ff" "P!1" "xis!1" )"1" assert )"1" replace "1" "1" "Rie_sum" )nil nil ))nil ))nil ))nil ))nil )"2" "Riemann?_Rie" )"2" "a" "b" "ff" "gg" )"2" "1" "P!1" "xis!1" )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "fun_to_op" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "ff" )"2" "2" expand "continuous?" )"2" expand "continuous_on_int?" )"2" expand "continuous?" )"2" "2" "x!1" )"1" expand "continuous_at?" )"1" "1" "epsilon!1" )"1" "1" "delta!1" )"1" "1" "y!1" )"1" assert )nil nil )"2" expand "Intab" )"2" expand "restrict" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "Intab" )"2" expand "restrict" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" expand "bounded_variation?" )"3" "op_norm[a,b,Continuous_Function[a,b]](LC)" )"3" "3" "strictly_sort(P)" )"1" assert )"1" "variation_on_strictly_sort" )"1" "a" "b" )"1" assert )"1" "P" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "partition_strictly_sort" )"2" "a" "b" )"2" assert )"2" "P" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" case "LB(step_approx(P, xis)(ff)) = sigma[below(P`length - 1)] LAMBDA (n: below(P`length - 1)):") "1" replace -1)"1" "1" expand "Rie_sum" "1" rewrite "sigma_restrict_eq" )"1" "1" "1" expand "restrict" )"1" "char_fun_minus" )"1" "a" "P`seq(x!1)" "P`seq(1+x!1)" )"1" assert )"1" case "a <= P`seq(x!1) AND P`seq(x!1) < P`seq(1 + x!1)" )"1" "1" assert )"1" expand "gg" "1" case "Intab(P`seq(1+x!1)) AND Intab(P`seq(x!1))" )"1" "1" assert )"1" "1" assert )"1" "1" "1" "LB" )"1" expand "bounded_linear_operator?" )"1" expand "linear_op?" )"1" case "LB(char_fun(a, P`seq(1 + x!1)) - char_fun(a, P`seq(x!1))) = LB(char_fun(a, P`seq(1 + x!1))) - LB(char_fun(a, P`seq(x!1)))" )"1" assert )nil nil )"2" "2" "2" expand "additive_op?" )"2" "char_fun(a, P`seq(1 + x!1))" "-1*char_fun(a, P`seq(x!1))" )"1" expand "const_inv_op?" )"1" "char_fun(a,P`seq(x!1))" "-1" )"1" case "char_fun(a, P`seq(1 + x!1)) + -1 * char_fun(a, P`seq(x!1)) = char_fun(a, P`seq(1 + x!1)) - char_fun(a, P`seq(x!1))" )"1" assert )nil nil )"2" "2" expand "-" )"2" expand "+" )"2" expand "*" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "bounded_on_int?" )"2" "1" )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" expand "bounded_on_int?" )"3" "2" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "Intab" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "strictly_increasing?" )"2" "x!1" "1+x!1" )"2" assert )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "bounded_on_int?" )"2" "1" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "step_approx" "2" case "FORALL (nn:below(P`length-1)): LB(LAMBDA (x:INTab): LAMBDA (n: below(P`length - 1)):LAMBDA (n: below(P`length - 1)):") "1" "P`length-2" )nil nil )"2" "2" "nn" )"1" assert )"1" expand "sigma" )"1" expand "sigma" )"1" "LB" )"1" expand "bounded_linear_operator?" )"1" expand "linear_op?" )"1" expand "const_inv_op?" )"1" "1" "char_fun(P`seq(0),P`seq(1))" "ff(xis`seq(0))" )"1" expand "*" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "nn" )"2" "2" expand "sigma" "2" replace "2" "LB" )"2" expand "bounded_linear_operator?" )"2" expand "linear_op?" )"2" expand "additive_op?" )"2" "2" "LAMBDA (x:INTab): LAMBDA (n: below(P`length - 1)):" "LAMBDA (x:INTab): ") "1" expand "+" )"1" replace "1" expand "const_inv_op?" )"1" "char_fun(P`seq(1 + nn), P`seq(2 + nn))" "ff(xis`seq(1 + nn))" )"1" expand "*" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "bounded_on_int?" )"2" "abs(ff(xis`seq(1+nn)))" )"2" nil nil ))nil ))nil ))nil )"3" "3" expand "bounded_on_int?" )"3" "fun_norm(ff)*(nn+1)" )"3" "3" case "FORALL (mm:below(nn+1)): abs(sigma[below(P`length - 1)] LAMBDA (n: below(P`length - 1)):") "1" "nn" )nil nil )"2" "2" "mm" )"1" assert )"1" expand "sigma" )"1" expand "sigma" )"1" "fun_norm(ff)" )"1" "xis`seq(0)" )"1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "mm" )"2" assert )"2" "2" expand "sigma" "2" "triangle" )"2" "2" case "abs(ff(xis`seq(1 + mm)) * ") "1" assert )nil nil )"2" "2" "2" "2" "fun_norm(ff)" )"2" "xis`seq(1+mm)" )"2" "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 ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" expand "bounded_on_int?" )"3" "1" )"3" nil nil ))nil ))nil ))nil ))nil )"4" "4" "4" expand "bounded_on_int?" )"4" "fun_norm(ff)*(nn+1)" )"4" "4" case "FORALL (mm:below(nn+1)): abs(sigma[below(P`length - 1)] LAMBDA (n: below(P`length - 1)):") "1" "nn" )nil nil )"2" "2" "mm" )"1" assert )"1" expand "sigma" )"1" expand "sigma" )"1" "fun_norm(ff)" )"1" "xis`seq(0)" )"1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "mm" )"2" assert )"2" "2" expand "sigma" "2" "triangle" )"2" "2" case "abs(ff(xis`seq(1 + mm)) * ") "1" assert )nil nil )"2" "2" "2" "2" "fun_norm(ff)" )"2" "xis`seq(1+mm)" )"2" "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 )"3" "3" "3" expand "bounded_on_int?" )"3" "1" )"3" nil nil ))nil ))nil ))nil ))nil )"4" "4" "4" expand "bounded_on_int?" )"4" "fun_norm(ff)*(nn+1)" )"4" "4" case "FORALL (mm:below(nn+1)): abs(sigma[below(P`length - 1)] LAMBDA (n: below(P`length - 1)):") "1" "nn" )nil nil )"2" "2" "mm" )"1" assert )"1" expand "sigma" )"1" expand "sigma" )"1" "fun_norm(ff)" )"1" "xis`seq(0)" )"1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "mm" )"2" assert )"2" "2" expand "sigma" "2" "triangle" )"2" "2" case "abs(ff(xis`seq(1 + mm)) * ") "1" assert )nil nil )"2" "2" "2" "2" "fun_norm(ff)" )"2" "xis`seq(1+mm)" )"2" "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 ))nil )"3" "3" "3" expand "bounded_on_int?" )"3" "1" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" "total_variation(a,b,gg)(b)" )"2" "2" assert )"2" "op_norm[a,b,Continuous_Function[a,b]](LC)" )"2" assert )"2" "2" "strictly_sort(P!1)" )"1" assert )"1" "strictly_sort(P!1)" )"1" assert )"1" "variation_on_strictly_sort" )"1" "a" "b" )"1" assert )"1" "P!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "b" )"2" "partition_strictly_sort" )"2" "a" "b" )"2" assert )"2" "P!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide 2)"3" (expand "bounded_variation?" )"3" "op_norm[a,b,Continuous_Function[a,b]](LC)" )"3" "3" "strictly_sort(P)" )"1" assert )"1" "variation_on_strictly_sort" )"1" "a" "b" )"1" assert )"1" "P" )"1" "variation_on_strictly_sort" )"1" "a" "b" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "b" )"2" "partition_strictly_sort" )"2" "a" "b" )"1" assert )"1" "P" )nil nil ))nil )"2" (assert ) nil nil )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" (typepred "b" ) (("4" (assert ) nil nil ))nil )"5" (assert ) nil nil )"6" (assert ) nil nil ))nil ))nil )"2" (hide 2)"2" (skeep)"2" "siggy" "(# length := P`length-1, seq:= (LAMBDA (nn:nat): IF nn >= P`length THEN default[INTab] ELSE sign(gg(P`seq(nn+1))-gg(P`seq(nn))) ENDIF) #)" )"2" case "FORALL (mm: below(P`length - 1)): LAMBDA (x:INTab):LAMBDA (nn: below(P`length - 1)):") "1" "blem" -1)"1" "blem" )"1" case "FORALL (mm:below(P`length-1)): LB(LAMBDA (x:INTab): LAMBDA (nn: below(P`length - 1)):LAMBDA (nn: below(P`length - 1)):") "1" "alem" -1)"1" "alem" )"1" "sigfun" "LAMBDA (x:INTab): sigma[below(P`length-1)](0,P`length-2,LAMBDA (nn:below(P`length-1)): siggy`seq(nn)*char_fun(P`seq(nn),P`seq(1+nn))(x))" )"1" case "variation_on(a,b,P)(gg) = LB(sigfun) AND fun_norm(sigfun) <= 1" )"1" "1" "NN" "op_norm[a, b, Bounded_Function[a,b]](LB)" )"1" "NN" )"1" "sigfun" )"1" expand "abs" -2)"1" assert )"1" "NN" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" expand "sigfun" +)"1" "alem" )"1" "alem" )"1" "alem" )"1" "P`length-2" )"1" replace "1" "1" expand "variation_on" "1" assert )"1" rewrite "sigma_restrict_eq" )"1" "1" "1" expand "restrict" )"1" case "gg(P`seq(1 + x!1)) - gg(P`seq(x!1)) = LB(char_fun(P`seq(x!1), P`seq(1 + x!1)))" )"1" "1" replace "1" expand "siggy" )"1" replace "1" "1" "char_fun" )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "gg" "2" case "Intab(P`seq(1 + x!1)) AND Intab(P`seq(x!1))" )"1" "1" assert )"1" "1" "1" "1" assert )"1" "1" "zerofun" "(LAMBDA (x:INTab): 0)" )"1" case "char_fun(P`seq(x!1),P`seq(1+x!1)) = zerofun" )"1" replace "1" "LB" )"1" expand "bounded_linear_operator?" )"1" expand "linear_op?" )"1" expand "additive_op?" )"1" "1" "zerofun" "zerofun" )"1" case "zerofun+zerofun = zerofun" )"1" assert )nil nil )"2" "2" "2" expand "zerofun" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" replace "2" replace "2" "2" "2" expand "char_fun" )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "P" )"2" expand "increasing?" )"2" "x!1" "1+x!1" )"2" assert )nil nil ))nil ))nil ))nil )"3" case "P`seq(x!1) < P`seq(1+x!1)" )"1" assert )"1" "char_fun_minus" )"1" expand "Intab" )"1" "1" "a" "P`seq(x!1)" "P`seq(1+x!1)" )"1" assert )"1" replace "1" "1" "LB" )"1" expand "bounded_linear_operator?" )"1" expand "linear_op?" )"1" expand "additive_op?" )"1" expand "const_inv_op?" )"1" "1" "char_fun(a, P`seq(1 + x!1))" "-1*char_fun(a, P`seq(x!1))" )"1" "char_fun(a, P`seq(x!1))" "-1" )"1" case "char_fun(a, P`seq(1 + x!1)) + -1 * char_fun(a, P`seq(x!1)) = char_fun(a, P`seq(1 + x!1)) - char_fun(a, P`seq(x!1))" )"1" assert )nil nil )"2" "2" expand "*" )"2" expand "-" )"2" expand "+" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "bounded_on_int?" )"2" "1" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "strictly_increasing?" )"2" "x!1" "1+x!1" )"2" assert )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "Intab" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "bounded_on_int?" )"2" "1" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "bounded_on_int?" )"2" "1" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "FORALL (xy:INTab):abs(sigfun(xy)) <= 1" )"1" "1" "fun_norm(sigfun)" )"1" "1" )"1" assert )"1" "1" "x!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" case "sigfun(xy) = 0" )"1" replace -1)"1" assert )nil nil ))nil )"2" case "FORaLL (jj:below(P`length-1)): char_fun(P`seq(jj),P`seq(1+jj))(xy) = 0" )"1" expand "sigfun" "1" rewrite "sigma_restrict_eq_0" )"1" "1" "1" "i" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" case "sigfun(xy) = siggy`seq(jj)*char_fun(P`seq(jj), P`seq(1 + jj))(xy)" )"1" replace "1" "1" expand "siggy" )"1" nil nil ))nil ))nil ))nil )"2" "2" expand "sigfun" "2" "sigma_split[below(P`length-1)]" )"2" "LAMBDA (nn: below(P`length - 1)): " "P`length-2" "0" "jj" )"2" assert )"2" replace "2" "2" expand "sigma" "2" case "sigma(0, jj - 1, LAMBDA (nn: below(P`length - 1)):") "1" replace "1" "1" assert )"1" rewrite "sigma_restrict_eq_0" )"1" "1" "1" "1" case "a<=P`seq(jj) AND P`seq(jj) < P`seq(1+jj) AND P`seq(1+jj)<= P`seq(i) AND P`seq(i) < P`seq(1+i) AND P`seq(1+i) <= b" )"1" "1" nil nil ))nil )"2" "2" expand "strictly_increasing?" )"2" "jj" "1+jj" )"2" "i" "1+i" )"2" assert )"2" "P" )"2" expand "increasing?" )"2" "1+jj" "i" )"2" assert )"2" "jj" )"2" "1+i" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "sigma_restrict_eq_0" )"2" "2" "2" "2" case "a<=P`seq(i) AND P`seq(i) < P`seq(1+i) AND P`seq(1+i) <= P`seq(jj) AND P`seq(jj) < P`seq(jj+1) AND P`seq(jj+1) <= b" )"1" "1" nil nil ))nil )"2" "2" expand "strictly_increasing?" )"2" "i" "1+i" )"2" "jj" "1+jj" )"2" assert )"2" "P" )"2" expand "increasing?" )"2" "1+i" "jj" )"2" "i" )"2" "1+jj" )"2" assert )"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 ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "blem" )"3" "3" expand "sigfun" +)"3" "P`length-2" )nil nil ))nil ))nil ))nil ))nil )"4" "4" "blem" )"4" "P`length-2" )"4" expand "sigfun" )"4" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "mm" )"1" assert )"1" expand "sigma" )"1" expand "sigma" )"1" "LB" )"1" expand "bounded_linear_operator?" )"1" expand "linear_op?" )"1" expand "const_inv_op?" )"1" "1" "char_fun(P`seq(0), P`seq(1))" "siggy`seq(0)" )"1" expand "*" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "mm" )"2" "2" assert )"2" expand "sigma" + 2)"2" replace -2 :dir rl)"2" "LB" )"2" expand "bounded_linear_operator?" )"2" expand "linear_op?" )"2" "2" expand "const_inv_op?" )"2" "char_fun(P`seq(1 + mm), P`seq(2 + mm))" "siggy`seq(1+mm)" )"2" replace "2" expand "additive_op?" )"2" "lambda (x:INTab): sigma[below(P`length - 1)] LAMBDA (nn: below(P`length - 1)):" "siggy`seq(1 + mm) * char_fun(P`seq(1 + mm), P`seq(2 + mm))" )"1" replace "1" assert )"1" case "(lambda (x:INTab): sigma[below(P`length - 1)] LAMBDA (nn: below(P`length - 1)):LAMBDA (x:INTab):LAMBDA (nn: below(P`length - 1)):") "1" assert )nil nil )"2" "2" "2" expand "+" )"2" expand "sigma" "2" assert )"2" expand "*" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "blem" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" expand "bounded_on_int?" )"3" "1" )"3" (grind) nil nil ))nil ))nil ))nil ))nil )"4" "blem" )"4" (propax) nil nil ))nil ))nil ))nil )"3" "3" "3" expand "bounded_on_int?" )"3" "1" )"3" (grind) nil nil ))nil ))nil ))nil ))nil )"4" "blem" )"4" (propax) nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "bounded_on_int?" )"2" "mm+1" )"2" "2" case "FORALL (rr:below(P`length-1)):abs(sigma[below(P`length - 1)] LAMBDA (nn: below(P`length - 1)):") "1" (inst - "mm" ) nil nil )"2" "2" "rr" )"1" assert )"1" expand "sigma" )"1" expand "sigma" )"1" expand "siggy" )"1" nil nil ))nil ))nil ))nil ))nil )"2" "rr" )"2" "2" assert )"2" expand "sigma" "2" "CV1" "sigma[below(P`length - 1)] LAMBDA (nn: below(P`length - 1)):") "2" replace -1)"2" "2" expand "siggy" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide-all-but 1)"3" (skeep)"3" (typepred "P" ) (("3" (assert ) nil nil ))nil ))nil ))nil )"4" (skeep) (("4" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (skeep)"2" (expand "bounded_on_int?" )"2" (inst + "1" ) (("2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil riesz_interval_funs nil )"bool" riesz_interval_funs nil )nil riesz_linear_functionals nil )"bool" nil )nil riesz_hahn_banach nil )"nnreal" riesz_representation nil )nil real_types nil )"bool" reals nil )nil riesz_hahn_banach nil )"bool" riesz_interval_funs nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"[T, T -> boolean]" equalities nil )NOT const-decl "[bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )"{M: nnreal | AND " nil )"{M: nnreal | AND " nil )"[numfield, numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil real_types nil )"bool" riesz_bounded_functionals nil )nil riesz_interval_funs nil )"nnreal" bounded_variation nil )"bool" sort_fseq "structures/" )nil rs_partition nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" sort_fseq "structures/" )"R" restrict nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )nil fseqs "structures/" )nil fseqs "structures/" )nil naturalnumbers nil )"(reflexive?[S])" nil )"(antisymmetric?[S])" nil )"(transitive?[S])" nil )"(preorder?[S])" nil )"(partial_order?[S])" nil )"(dichotomous?[S])" nil )"(total_order?[S])" nil )"bool" bounded_variation nil )"{M: nnreal | AND AND " bounded_variation nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"real" rs_integral_def nil )nil bounded_variation nil )"partition[INTab](a, b)" riesz_representationnil )"bool" continuity_ms_def nil )set type-eq-decl nil sets nil )"set[real]" riesz_interval_funs nil )"bool" booleans nil )"(LAMBDA (x: INTab[a, b]): TRUE)" nil )"bool" sets nil )"(LAMBDA (x: INTab[a, b]): TRUE)" nil )"bool" continuity_ms_def nil )"bool" rs_integral_def nil )nil rs_integral_def nil )"xis?[INTab](a, b, P!1)" nil )"Continuous_Function[a, b]" nil )"partition[INTab](a, b)" nil )"bool" rs_integral_def nil )nil rs_integral_def nil )"bool" rs_integral_def nil )nil rs_integral_cont nil )"posint" nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil sigma "reals/" )nil sigma "reals/" )"real" sigma "reals/" )nil sigma "reals/" )"partition[INTab](a, b)" riesz_representationnil )"[T -> real]" sigma "reals/" )nil riesz_representation nil )"even_int" integers nil )"even_int" integersnil )"even_int" integersnil )"odd_int" integersnil )"below(P`length - 1)" riesz_representationnil )"posint" nil )nil real_props nil )"below(P`length - 1)" riesz_representationnil )nil bounded_nat_inductions nil )nil defined_types nil )"xis?[INTab](a, b, P)" riesz_representationnil )"Continuous_Function[a, b]" nil )"posreal" nil )"posreal" nil )"[T -> real]" real_fun_ops "reals/" )nil real_props nil )"nnreal" nil )"[T -> real]" real_fun_ops "reals/" )"partition[INTab](a, b)" riesz_representationnil )"xis?[INTab](a, b, P)" riesz_representationnil )"Continuous_Function[a, b]" nil )"real" reals nil )"real" reals nil )"[T -> real]" real_fun_ops "reals/" )"bool" riesz_linear_functionals nil )"nzint" integers nil )"{j: posint | j >= i}" nil )nil real_props nil )"bool" riesz_linear_functionals nil )"bool" riesz_linear_functionals nil )"real" reals nil )nil riesz_interval_funsnil )"odd_int" integers nil )"posreal" nil )nil riesz_representation nil )nil rs_partition nil )"[bool, bool -> bool]" booleans nil )"bool" fseqs "structures/" )"{ss: fseq | AND " sort_fseq "structures/" )nil rs_partition nil )nil rs_partitionnil )nil rs_partition nil )"xis?(a, b, P)" rs_integral_def nil )"int" integers nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"{z: posreal | z <= x AND z <= y}" real_defs nil )nil abs_lems "reals/" )"nnreal" nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"C_Bounded_Linear_Operator[a, b]" nil )"Continuous_Function[a, b]" nil )"[INTab[a, b] -> real]" riesz_representationnil )nil abs_lems "reals/" )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil )nil extra_real_props nil )"posreal" nil )"(bounded_on_int?[a, b])" nil )"posreal" rs_partition nil )nil rs_integral_def nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )"real" reals nil )nil riesz_representation nil )"nnreal" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"C_Bounded_Linear_Operator" nil )"partition[INTab](a, b)" nil )"partition[INTab](a, b)" riesz_representationnil )"below(P`length - 1)" riesz_representationnil )nil sigma "reals/" )"int" integers nil )nil integers nil )"int" integers nil )"odd_int" integersnil )nil sigma "reals/" )"{j: nonneg_int | j >= i}" nil )"[INTab[a, b] -> real]" nil )"nnreal" sigma_below "reals/" )"below(P`length - 1)" riesz_representationnil )nil naturalnumbers nil )"[INTab[a, b] -> naturalnumber]" nil )"nonneg_int" nil )"[# length: int, seq: [nat -> real] #]" nil )"partition[INTab](a, b)" riesz_representationnil )nil extra_real_propsnil )nil riesz_interval_funs nil )"odd_int" integers nil )"posint" nil )"Sign" sign "reals/" )nil sign "reals/" )nil integers nil )"T" fseqs "structures/" )nil riesz_hahn_banach nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"real" riesz_representation nil )nil booleans nil )"bool" reals nil )"{bb: real | a < bb}" riesz_representationnil ))nil )nil 3492950416"" (skeep)"" (lemma "Hahn_Banach" )"" (inst - "LC" )"" (skeep -)"" "gg" "(LAMBDA (x:INTab): IF x = a THEN 0 ELSE LB(char_fun(a,x)) ENDIF)" )"1" (label "ggname" -1)"1" (label "opeq" -2)"1" (label "LBLC" -3)"1" case "(FORALL (P:partition(a,b)): strictly_increasing?(P) IMPLIES variation_on(a,b,P)(gg) <= op_norm[a,b,Continuous_Function[a,b]](LC))" )"1" (label "VPle" -1)"1" case "total_variation(a,b,gg)(b) <= op_norm[a,b,Continuous_Function[a,b]](LC)" )"1" (label "TVle" -1)"1" (inst + "gg" )"1" (case "LC = fun_to_op(gg)" )"1" assert )"1" case "op_norm[a,b,Continuous_Function[a,b]](LC) <= total_variation(a,b,gg)(b)" )"1" (assert ) nil nil )"2" "2" "TVle" )"2" "fun_to_op_bound" )"2" "op_norm[a,b,Continuous_Function[a,b]](LC)" )"2" "total_variation(a,b,gg)(b)" )"2" assert )"2" "2" "f!1" )"2" "f!1" "gg" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" case "FORALL (epsil:posreal,ff:Continuous_Function[a,b]): EXISTS (delta:posreal): FORALL (P:partition(a,b),xis:xis?(a,b,P)): width(a,b,P)<delta and strictly_increasing?(P) IMPLIES abs(LB(step_approx(P,xis)(ff))-fun_to_op(gg)(ff)) < epsil" )"1" case "FORALL (ff:Continuous_Function[a,b]): LC(ff) = fun_to_op(gg)(ff)" )"1" nil nil )"2" "2" "2" case "FORALL (epsil:posreal): abs(LC(ff)-fun_to_op(gg)(ff)) < 32*epsil" )"1" case "abs(LC(ff)-fun_to_op(gg)(ff)) = 0" )"1" "abs_eq_0" )"1" "1" assert )nil nil ))nil ))nil )"2" "2" "abs(LC(ff)-fun_to_op(gg)(ff))/64" )"1" (assert ) nil nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" case "FORALL (epsil:posreal,ff:Continuous_Function[a,b]): EXISTS (delta:posreal): FORALL (P:partition(a,b),xis:xis?(a,b,P)): AND width(a,b,P)<delta IMPLIES abs(LC(ff)-LB(step_approx(P,xis)(ff)))<epsil") "1" "1" "epsil" "ff" )"1" "epsil" "ff" )"1" "1" "partition_exists" )"1" "a" "b" "min(delta!1,delta!2)" )"1" assert )"1" "1" "SSP" "strictly_sort(P)" )"1" case "width(a,b,SSP) < min(delta!1,delta!2)" )"1" "1" "1" "xis" "gen_xis(a,b,SSP)" )"1" "SSP" "xis" )"1" assert )"1" "SSP" "xis" )"1" assert )"1" "1" "stop_approx" "fun_to_op" ))nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "partition_union_is_strictly_sort" )"2" "a" "b" )"2" assert )"2" "P" )"2" "partition_union_width" )"2" "a" "b" )"2" assert )"2" "P" "P" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "partition_strictly_sort" )"3" "a" "b" )"3" assert )"3" "P" )"3" "3" assert )"3" "3" "i!1" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "LB" )"2" expand "bounded_linear_operator?" )"2" "2" expand "bounded_op?" )"2" "2" "step_approx_def" )"2" "ff!1" "epsil!1/(M!1+1)" )"2" "2" "delta!1" )"2" "2" "P" "xis" )"2" assert )"2" "LBLC" "ff!1" )"2" replace "LBLC" "2" case "LB(ff!1) - LB(step_approx(P, xis)(ff!1)) = LB(ff!1-step_approx(P,xis)(ff!1))" )"1" replace "1" "ff!1 - step_approx(P, xis)(ff!1)" )"1" case "fun_norm(ff!1 - step_approx(P, xis)(ff!1)) <= epsil!1/(M!1+1)" )"1" "1" assert )nil nil ))nil )"2" "2" "fun_norm(ff!1 - step_approx(P, xis)(ff!1))" )"2" "epsil!1/(M!1+1)" )"2" assert )"2" "2" "x!1" )"2" expand "-" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "linear_op?" )"2" "2" expand "additive_op?" )"2" "ff!1" "-1*step_approx(P,xis)(ff!1)" )"1" expand "const_inv_op?" )"1" "step_approx(P,xis)(ff!1)" "-1" )"1" case "ff!1+-1*step_approx(P,xis)(ff!1) = ff!1-step_approx(P,xis)(ff!1)" )"1" assert )nil nil )"2" "2" "step_approx" ))"2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "step_approx(P,xis)(ff!1)" )"2" assert )"2" expand "*" )"2" assert )"2" expand "bounded_on_int?" )"2" "2" "M!2" )"2" "2" "x!1" )"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 )"3" "3" expand "bounded_on_int?" )"3" "step_approx(P,xis)(ff!1)" )"1" "ff!1" )"1" "continuous_implies_bounded" )"1" "ff!1" )"1" "1" expand "bounded_on_int?" )"1" "1" "M!2+M!3" )"1" "1" "x!1" )"1" "x!1" )"1" "step_approx" ))nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "continuous_implies_bounded" )"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 )"3" "3" "3" "continuous_implies_bounded" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "FORALL (ff:Continuous_Function[a,b],P:partition(a,b),xis:xis?(a,b,P)): strictly_increasing?(P) IMPLIES LB(step_approx(P,xis)(ff)) = Rie_sum(a,b,gg,P,xis,ff)" )"1" "RS_integrable_cont_BV" )"1" "1" "a" "b" "ff" "gg" )"1" assert )"1" "1" "1" expand "integrable?" "1" "1" "integral_def" )"1" "a" "b" "ff" "gg" "S!1" )"1" assert )"1" case "fun_to_op(gg)(ff) = S!1" )"1" replace "1" expand "integral?" )"1" "epsil" )"1" "1" "delta!1" )"1" "1" "P!1" )"1" assert )"1" "Rie_sum(a,b,gg,P!1,xis!1,ff)" )"1" "ff" "P!1" "xis!1" )"1" assert )"1" replace "1" "1" "Rie_sum" )nil nil ))nil ))nil ))nil ))nil )"2" "Riemann?_Rie" )"2" "a" "b" "ff" "gg" )"2" "1" "P!1" "xis!1" )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "fun_to_op" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "ff" )"2" "2" expand "continuous?" )"2" expand "continuous_on_int?" )"2" expand "continuous?" )"2" "2" "x!1" )"1" expand "continuous_at?" )"1" "1" "epsilon!1" )"1" "1" "delta!1" )"1" "1" "y!1" )"1" assert )nil nil )"2" expand "Intab" )"2" expand "restrict" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "Intab" )"2" expand "restrict" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" expand "bounded_variation?" )"3" "op_norm[a,b,Continuous_Function[a,b]](LC)" )"3" "3" "strictly_sort(P)" )"1" assert )"1" "variation_on_strictly_sort" )"1" "a" "b" )"1" assert )"1" "P" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "partition_strictly_sort" )"2" "a" "b" )"2" assert )"2" "P" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" case "LB(step_approx(P, xis)(ff)) = sigma[below(P`length - 1)] LAMBDA (n: below(P`length - 1)):") "1" replace -1)"1" "1" expand "Rie_sum" +)"1" rewrite "sigma_restrict_eq" )"1" "1" "1" expand "restrict" )"1" "char_fun_minus" )"1" "a" "P`seq(x!1)" "P`seq(1+x!1)" )"1" assert )"1" case "a <= P`seq(x!1) AND P`seq(x!1) < P`seq(1 + x!1)" )"1" "1" assert )"1" expand "gg" "1" case "Intab(P`seq(1+x!1)) AND Intab(P`seq(x!1))" )"1" "1" assert )"1" "1" assert )"1" "1" "1" "LB" )"1" expand "bounded_linear_operator?" )"1" expand "linear_op?" )"1" case "LB(char_fun(a, P`seq(1 + x!1)) - char_fun(a, P`seq(x!1))) = LB(char_fun(a, P`seq(1 + x!1))) - LB(char_fun(a, P`seq(x!1)))" )"1" assert )nil nil )"2" "2" "2" expand "additive_op?" )"2" "char_fun(a, P`seq(1 + x!1))" "-1*char_fun(a, P`seq(x!1))" )"1" expand "const_inv_op?" )"1" "char_fun(a,P`seq(x!1))" "-1" )"1" case "char_fun(a, P`seq(1 + x!1)) + -1 * char_fun(a, P`seq(x!1)) = char_fun(a, P`seq(1 + x!1)) - char_fun(a, P`seq(x!1))" )"1" assert )nil nil )"2" "2" expand "-" )"2" expand "+" )"2" expand "*" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "bounded_on_int?" )"2" "1" )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" expand "bounded_on_int?" )"3" "2" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "Intab" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "strictly_increasing?" )"2" "x!1" "1+x!1" )"2" assert )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "bounded_on_int?" )"2" "1" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "step_approx" "2" case "FORALL (nn:below(P`length-1)): LB(LAMBDA (x:INTab): LAMBDA (n: below(P`length - 1)):LAMBDA (n: below(P`length - 1)):") "1" "P`length-2" )nil nil )"2" "2" "nn" )"1" assert )"1" expand "sigma" )"1" expand "sigma" )"1" "LB" )"1" expand "bounded_linear_operator?" )"1" expand "linear_op?" )"1" expand "const_inv_op?" )"1" "1" "char_fun(P`seq(0),P`seq(1))" "ff(xis`seq(0))" )"1" expand "*" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "nn" )"2" "2" expand "sigma" "2" replace "2" "LB" )"2" expand "bounded_linear_operator?" )"2" expand "linear_op?" )"2" expand "additive_op?" )"2" "2" "LAMBDA (x:INTab): LAMBDA (n: below(P`length - 1)):" "LAMBDA (x:INTab): ") "1" expand "+" )"1" replace "1" expand "const_inv_op?" )"1" "char_fun(P`seq(1 + nn), P`seq(2 + nn))" "ff(xis`seq(1 + nn))" )"1" expand "*" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "bounded_on_int?" )"2" "abs(ff(xis`seq(1+nn)))" )"2" nil nil ))nil ))nil ))nil )"3" "3" expand "bounded_on_int?" )"3" "fun_norm(ff)*(nn+1)" )"1" "1" case "FORALL (mm:below(nn+1)): abs(sigma[below(P`length - 1)] LAMBDA (n: below(P`length - 1)):") "1" "nn" )nil nil )"2" "2" "mm" )"1" assert )"1" expand "sigma" )"1" expand "sigma" )"1" "fun_norm(ff)" )"1" "xis`seq(0)" )"1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "mm" )"2" assert )"2" "2" expand "sigma" "2" "triangle" )"2" "2" case "abs(ff(xis`seq(1 + mm)) * ") "1"
Messung V0.5 in Prozent C=100 H=99 G=99
¤ 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.791Bemerkung:
(vorverarbeitet am 2026-04-27)
¤ *Bot Zugriff
2026-05-26
