Quelle essential_bound_complete_scaf.prf
Sprache: Lisp
(essential_bound_complete_scafnil 3502969751"" (typepred "S" )"" (expand "sigma_algebra?" )"" (flatten)"" (expand "subset_algebra_empty?" )"" (expand "member" ) (("" (propax) nil nil )) nil )) nil ))nil ))nil ))nil )"bool" subset_algebra_def"measure_integration/" )"bool" sets nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil essential_bound_complete_scaf nil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def"measure_integration/" )nil subset_algebra_def"measure_integration/" )"sigma_algebra[T]" nil ))nil ))nil 3502969847"" case "FORALL (F: sequence[essentially_bounded]): ") "1" (skosimp)"1" "NEXT" "lambda (n,m:nat): (n+1,choose({k:nat | k > m & FORALL i, j: AND j >= k => essential_bound(F!1(j) - F!1(i)) < 2^(-n)}))") "1" (name "SEQ" "lambda n: (iterate(NEXT,n+1)(0,0))`2" )"1" case "forall n,i: i >= SEQ(n) => essential_bound(F!1(i) - F!1(SEQ(n))) < 2 ^ (-n)" )"1" (case "subseq?(F!1 o SEQ, F!1)" )"1" (inst -5 "F!1 o SEQ" )"1" (split -5)"1" (skosimp)"1" (inst + "f!1" )"1" (skosimp)"1" (inst - "r!1/2" )"1" (skosimp)"1" (case "exists n: 2^(-n) < r!1/2" )"1" "1" "SEQ(n!1+n!2)" )"1" "1" "n!1+n!2" )"1" assert )"1" "n!1+n!2" "i!1" )"1" assert )"1" expand "o" -2)"1" "essential_bound_diff" "f0" "f!1 - F!1(SEQ(n!1 + n!2))" "f1" "F!1(i!1) - F!1(SEQ(n!1 + n!2))" ))"1" assert )"1" case "2 ^ (-(n!1 + n!2))<=2 ^ (-n!2)" )"1" assert )"1" "LHS1" "essential_bound(f!1 - F!1(SEQ(n!1 + n!2)) - ") "1" "LHS2" "essential_bound(f!1 - F!1(i!1))" )"1" "LHS1=LHS2" )"1" assert )nil nil )"2" "2" expand "LHS2" )"2" expand "LHS1" )"2" expand "-" )"2" assert )"2" "F1" "F!1(i!1)" )"2" "F2" "F!1(SEQ(n!1 + n!2))" )"2" expand "essential_bound" )"2" expand "ae_le?" )"2" expand "abs" )"2" expand "pointwise_ae?" )"2" expand "ae?" )"2" expand "fullset" )"2" expand "ae_in?" )"2" expand "member" )"2" expand "-" )"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" "both_sides_real_expt_gt1_ge" "gt1x" "2" "a" "-n!2" "b" "-(n!1 + n!2)" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "small_expt" ("px" "1/2" ))"2" assert )"2" "r!1/2" )"2" "2" "n!2" )"2" rewrite "real_expt_neg" )"2" rewrite "real_expt_int_rew" )"2" expand "^" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp)"2" (inst -2 "n!1" "SEQ(n!1+1)" )"2" (expand "o " )"2" (assert )"2" (hide 1 -1 -2 -3)"2" expand "SEQ" )"2" expand "iterate" 1 1)"2" "NN" "iterate(NEXT, 1 + n!1)(0, 0)" )"2" expand "NEXT" )"2" case "nonempty?({k: nat | AND j >= k =>") "1" "choose_member" "a" "{k: nat | AND j >= k =>")) "1" "1" "CC" "choose({k: nat | AND j >= k =>") "1" expand "member" )"1" "1" assert )nil nil ))nil ))nil ))nil )"2" expand "nonempty?" )"2" (propax) nil nil ))nil ))nil ))nil )"2" "2" expand "nonempty?" )"2" expand "empty?" )"2" expand "member" )"2" "2 ^ (-NN`1)" )"1" "1" "n!2+NN`2+1" )"1" assert )"1" "1" "i!1" "j!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "real_expt_pos" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (expand "subseq?" )"2" (inst + "SEQ" )"1" (expand "o " ) (("1" (propax) nil nil )) nil )"2" (expand "strict_increasing?" )"2" case "forall (i,n:nat): SEQ(i) < SEQ(1+i+n)" )"1" (skosimp)"1" (inst - "x!1" "y!1-x!1-1" )"1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil )"2" (hide 2)"2" (induct "n" )"1" (skosimp)"1" expand "SEQ" )"1" expand "iterate" 1 2)"1" "NN" "iterate(NEXT, 1 + i!1)(0, 0)" )"1" expand "NEXT" )"1" "1" case "nonempty?({k: nat | AND j >= k =>") "1" "choose_member" "a" "{k: nat | AND j >= k =>")) "1" "1" "RHS" "choose({k: nat | AND j >= k =>") "1" expand "member" )"1" "1" assert )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" "2 ^ (-NN`1)" )"1" "1" "n!1+NN`2+1" )"1" assert )"1" "1" "i!2" "j!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "real_expt_pos" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp)"2" "2" "i!1" )"2" "LHS" "SEQ(i!1)" )"2" "2" expand "SEQ" )"2" expand "iterate" 1)"2" "NN" "iterate(NEXT, 2 + i!1 + j!1)(0, 0)" )"2" expand "NEXT" )"2" case "nonempty?({k: nat | AND j >= k =>") "1" "choose_member" "a" "{k: nat | AND j >= k =>")) "1" "1" "ZZ" "choose({k: nat | AND j >= k =>") "1" expand "member" )"1" "1" assert )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" "2 ^ (-NN`1)" )"1" "1" "n!1+NN`2+1" )"1" assert )"1" "1" "i!2" "j!2" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" rewrite "real_expt_pos" )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" (induct "n" )"1" (skosimp)"1" (expand "SEQ" )"1" (expand "iterate" )"1" (expand "iterate" )"1" (hide -2)"1" (name "ZZ" "NEXT(0, 0)`2" )"1" (replace -1)"1" expand "NEXT" -1)"1" case "nonempty?({k: nat | AND j >= k =>") "1" "choose_member" "a" "{k: nat | AND j >= k =>")) "1" replace -3)"1" "1" expand "member" )"1" "1" "ZZ" "i!1" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" expand "nonempty?" )"2" (propax) nil nil ))nil ))nil ))nil ))nil )"2" "2" expand "nonempty?" )"2" expand "empty?" )"2" expand "member" )"2" "2^(-0)" )"1" "1" "n!1+1" )"1" assert )"1" "1" "i!2" "j!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "real_expt_pos" "px" "2" "a" "-0" ))"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp)"2" (skosimp)"2" (hide -3 -4)"2" (expand "SEQ" )"2" (expand "iterate" 1)"2" (expand "iterate" -2)"2" "NN" "iterate(NEXT, 1 + j!1)(0, 0)" )"2" expand "NEXT" )"2" case "nonempty?({k: nat | AND j >= k") "1" "choose_member" "a" "{k: nat | AND j >= k")) "1" "1" expand "member" )"1" "CC" "choose({k: nat | AND j >= k") "1" "1" "CC" "i!1" )"1" "NN`1=1+j!1" )"1" (assert ) nil nil )"2" expand "NN" 1)"2" case "forall n: iterate(NEXT,n)(0, 0)`1 = n" )"1" "1+j!1" )nil nil )"2" "2" "n" )"1" expand "iterate" )"1" nil nil ))nil )"2" "2" expand "iterate" "2" expand "NEXT" "2" nil nil ))nil ))nil ))nil )"3" "3" expand "NEXT" )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "nonempty?" )"2" (propax) nil nil ))nil ))nil ))nil )"2" "2" expand "nonempty?" )"2" expand "empty?" )"2" expand "member" )"2" "2^(-NN`1)" )"1" "1" "n!1+NN`2+1" )"1" assert )"1" "1" "i!2" "j!2" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "real_expt_pos" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp)"2" (expand "NEXT" ) (("2" (assert ) nil nil )) nil )) nil ))nil )"2" (skosimp)"2" (expand "nonempty?" )"2" (expand "empty?" )"2" (expand "member" )"2" (hide 1 -2)"2" (inst -2 "2 ^ (-n!1)" )"1" (skosimp)"1" (inst - "n!2+m!1+1" )"1" (assert )"1" (skosimp)"1" (inst - "i!1" "j!1" )"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (lemma "real_expt_pos" ("px" "2" "a" "-n!1" ))"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" case "FORALL (F: sequence[essentially_bounded]): NOT N(x) => abs(F(n+1)(x)-F(n)(x)) <= essential_bound(F(n + 1) - F(n))") "1" (skosimp)"1" (inst - "F!1" )"1" (skosimp)"1" case "FORALL (x: T, n, m: nat): NOT N!1(x) =>") "1" case "forall (n,m:nat): sigma[nat](n, n + m - 1, geometric(1 / 2)) < 2^(1-n)" )"1" case "exists (g:[T->complex]): pointwise_convergence?(lambda n: lambda (x:T): phi(complement(N!1))(x) * F!1(n)(x),g)" )"1" (skosimp)"1" "pointwise_complex_measurable" "f" "g!1" "u" "LAMBDA n: LAMBDA (x: T):")) "1" (replace -2)"1" case "FORALL (x: T, n): NOT N!1(x) => abs(g!1(x) - F!1(n)(x)) < 2 ^ (2 - n)" )"1" (case "essentially_bounded?(g!1)" )"1" "g!1" )"1" "1" "1" "exp_of_exists" "py" "r!1" "b" "2" ))"1" "1" "both_sides_real_expt_gt1_lt" "gt1x" "2" "a" "i!1-1" "b" "i!1" ))"1" assert )"1" rewrite "real_expt_int_rew" "1" rewrite "real_expt_int_rew" "1" case "3-i!1>=0" )"1" "3-i!1" )"1" "1" "both_sides_real_expt_gt1_le" "gt1x" "2" "a" "2-i!2" "b" "i!1-1" ))"1" assert )"1" "essential_bound_def1" "f" "g!1 - F!1(i!2)" "K" "2^(2-i!2)" ))"1" "1" assert )nil nil )"2" "2" expand "ae_le?" )"2" expand "pointwise_ae?" )"2" expand "ae?" )"2" expand "fullset" )"2" expand "ae_in?" )"2" "N!1" )"2" "2" expand "member" )"2" "x!1" "i!2" )"2" assert )"2" expand "abs" "2" assert )"2" expand "-" "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" assert )"2" case "3-i!1<0" )"1" "1" "both_sides_real_expt_gt1_lt" "gt1x" "2" "a" "3" "b" "i!1" ))"1" assert )"1" rewrite "real_expt_int_rew" "1" rewrite "expt_x3" )"1" "0" )"1" "1" "_" "i!2" )"1" case "2 ^ (2 - i!2)< 8" )"1" "essential_bound_def1" "f" "g!1 - F!1(i!2)" "K" "8" ))"1" "1" assert )nil nil )"2" "2" expand "ae_le?" )"2" expand "pointwise_ae?" )"2" expand "ae?" )"2" expand "fullset" )"2" expand "ae_in?" )"2" expand "member" )"2" "N!1" )"2" "2" "x!1" )"2" assert )"2" expand "abs" "2" expand "-" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "both_sides_real_expt_gt1_lt" "gt1x" "2" "a" "2-i!2" "b" "3" ))"2" assert )"2" "real_expt_int_rew" "x" "2" "i" "3" ))"2" replace "2" rewrite "expt_x3" )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 )"2" "2" "F!1(0)" )"2" expand "essentially_bounded?" )"2" replace -3)"2" "2" "2" expand "ae_bounded?" )"2" "2" "K!1+4" )"2" expand "ae_le?" )"2" expand "pointwise_ae?" )"2" expand "ae?" )"2" expand "fullset" )"2" expand "ae_in?" )"2" "2" "E!1" )"2" expand "member" )"2" "union(N!1,E!1)" )"2" "2" expand "union" )"2" expand "member" )"2" "2" "2" "x!1" )"2" "x!1" "0" )"2" assert )"2" rewrite "real_expt_int_rew" )"2" rewrite "expt_x2" )"2" "polar.abs_triangle" "z1" "g!1(x!1)-F!1(0)(x!1)" "z2" "F!1(0)(x!1)" ))"2" "abs(g!1(x!1) - F!1(0)(x!1) + F!1(0)(x!1))=abs(g!1)(x!1)" )"1" assert )"1" assert )"1" expand "abs" "1" expand "abs" "1" expand "abs" "1" assert )"1" "LHS" "abs(g!1(x!1))" )"1" expand "abs" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "abs" )"2" expand "abs" )"2" expand "sq_abs" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -1 2)"2" "2" expand "pointwise_convergence?" )"2" "x!1" )"2" expand "complement" )"2" expand "phi" )"2" expand "member" )"2" "x!1" "_" "_" )"2" "x!1" "_" )"2" replace 1)"2" "2" rewrite "metric_convergence_def" "2" expand "metric_converges_to" )"2" expand "ball" )"2" expand "member" )"2" "2^(-n!1)" )"1" "1" "n!1+n!2+1" )"1" assert )"1" "n!1" "1+n!2" )"1" "n!1" "1+n!2" )"1" "1" "polar.abs_triangle" "z1" "g!1(x!1) - 1 * F!1(1 + n!1 + n!2)(x!1)" "z2" "F!1(1 + n!2 + n!1)(x!1) - F!1(n!1)(x!1)" ))"1" "abs(g!1(x!1) - 1 * F!1(1 + n!1 + n!2)(x!1) + ") "1" "1" case "2 ^ (-n!1)+2 ^ (1 - n!1) <=2 ^ (2 - n!1)" )"1" assert )nil nil )"2" "2" "real_expt_plus" "x" "2" "a" "1" "b" "-n!1" ))"2" "real_expt_plus" "x" "2" "a" "2" "b" "-n!1" ))"2" replace "2" replace "2" "2" "both_sides_times_pos_le1" "pz" "2^(-n!1)" "x" "1+2^1" "y" "2^2" ))"1" assert )"1" "1" rewrite "real_expt_int_rew" )"1" rewrite "real_expt_int_rew" )"1" nil nil ))nil ))nil ))nil ))nil )"2" rewrite "real_expt_int_rew" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "abs" )"2" expand "sq_abs" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "real_expt_pos" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (skosimp)"2" (typepred "F!1(n!1)" )"2" "N!1" )"2" "null_set_is_measurable[T,S,mu]" )"2" "N!1" )"2" "measurable_complement[T,S]" "a" "N!1" ))"2" "phi_is_simple" "X" "complement[T](N!1)" ))"1" assert )"1" "prod_measurable" "g1" "phi(complement[T](N!1))" "g2" "Re(F!1(n!1))" ))"1" expand "*" -1)"1" expand "Re" 1)"1" expand "Im" 1)"1" "prod_measurable" "g1" "phi(complement[T](N!1))" "g2" "Im(F!1(n!1))" ))"1" expand "*" -1)"1" assert )nil nil ))nil )"2" expand "essentially_bounded?" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "essentially_bounded?" )"2" "2" assert )nil nil ))nil ))nil )"3" expand "simple?" )"3" (flatten) nil nil ))nil ))nil ))nil )"2" assert )"2" expand "measurable_set?" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2 -3 -4)"2" case "FORALL (x: T): NOT N!1(x) IMPLIESLAMBDA (n:nat): F!1(n)(x))") "1" "lambda (x:T): if N!1(x) then complex_(0,0) else limit(LAMBDA (n: nat): F!1(n)(x)) endif" )"1" (expand "pointwise_convergence?" )"1" (skosimp)"1" "x!1" )"1" expand "complement" )"1" expand "phi" )"1" expand "member" )"1" "N!1(x!1)" )"1" rewrite "metric_convergence_def" )"1" expand "metric_converges_to" )"1" "1" "0" )"1" "1" expand "ball" )"1" expand "member" )"1" expand "abs" )"1" expand "sq_abs" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "limit_lemma" "v" "LAMBDA (n_1: nat): 1 * F!1(n_1)(x!1)" ))"1" "1" expand "*" )"1" assert )"1" expand "convergence?" )"1" "1" "U!1" )"1" assert )"1" "1" nil nil )"2" "2" "equalities.=(LAMBDA (n_1: nat): LAMBDA (n: nat): F!1(n)(x!1))") "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "metric_convergent?" )"2" expand "convergent?" )"2" "2" "x!2" )"2" rewrite "metric_convergence_def" )"2" expand "metric_converges_to" )"2" expand "ball" )"2" expand "member" )"2" "2" "2" "r!1" )"2" "2" "n!1" )"2" "2" "i!1" )"2" assert )"2" expand "*" )"2" expand "-" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp)"2" (inst - "x!1" )"2" assert )"2" expand "convergent?" )"2" expand "metric_convergent?" )"2" "2" "x!2" )"2" rewrite "metric_convergence_def" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp)"2" (inst - "x!1" "_" "_" )"2" assert )"2" "2" "complex_is_complete" )"2" expand "fullset" )"2" expand "complete_metric_space?" )"2" expand "metric_complete?" )"2" "2" "LAMBDA (n: nat): F!1(n)(x!1)" )"2" "1" expand "metric_convergent?" )"1" nil nil ))nil )"2" "2" expand "cauchy?" )"2" "2" expand "ball" )"2" expand "member" )"2" "exp_of_exists" "b" "2" "py" "r!1" ))"2" "2" case "i!1>=0" )"1" "2" )"1" "1" "trich_lt" "x" "i!2" "y" "j!1" ))"1" "1" "i!2" "j!1-i!2" )"1" "i!2" "j!1-i!2" )"1" assert )"1" "both_sides_real_expt_gt1_lt" "gt1x" "2" "a" "1-i!2" "b" "i!1" ))"1" assert )"1" rewrite "real_expt_int_rew" )"1" rewrite "real_expt_int_rew" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil )"2" assert )nil nil ))nil )"2" replace "2" assert )"2" expand "abs" )"2" expand "sq_abs" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"3" "j!1" "i!2-j!1" )"1" "j!1" "i!2-j!1" )"1" "both_sides_real_expt_gt1_lt" "gt1x" "2" "a" "1-j!1" "b" "i!1" ))"1" assert )"1" rewrite "real_expt_int_rew" )"1" rewrite "real_expt_int_rew" )"1" assert )"1" expand "abs" )"1" expand "sq_abs" )"1" assert )"1" "sq_neg_minus" "a" "Im(F!1(j!1)(x!1))" "b" "Im(F!1(i!2)(x!1))" ))"1" "sq_neg_minus" "a" "Re(F!1(j!1)(x!1))" "b" "Re(F!1(i!2)(x!1))" ))"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" assert )"2" case "i!1<0" )"1" "1" "2-i!1" )"1" "1" "trich_lt" "x" "i!2" "y" "j!1" ))"1" "1" "i!2" "j!1-i!2" )"1" "i!2" "j!1-i!2" )"1" "both_sides_real_expt_gt1_lt" "gt1x" "2" "a" "1-i!2" "b" "i!1" ))"1" assert )"1" rewrite "real_expt_int_rew" )"1" rewrite "real_expt_int_rew" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil )"2" assert )nil nil ))nil )"2" replace "2" expand "abs" )"2" expand "sq_abs" )"2" assert )nil nil ))nil ))nil ))nil )"3" "j!1" "i!2-j!1" )"1" "j!1" "i!2-j!1" )"1" "both_sides_real_expt_gt1_lt" "gt1x" "2" "a" "1-j!1" "b" "i!1" ))"1" assert )"1" rewrite "real_expt_int_rew" )"1" rewrite "real_expt_int_rew" )"1" "abs(F!1(i!2)(x!1) - F!1(j!1)(x!1))=abs(F!1(j!1)(x!1) - F!1(i!2)(x!1))" )"1" assert )nil nil )"2" "2" expand "abs" )"2" expand "sq_abs" )"2" "sq_neg_minus" "a" "Im(F!1(i!2)(x!1))" "b" "Im(F!1(j!1)(x!1))" ))"2" "sq_neg_minus" "a" "Re(F!1(i!2)(x!1))" "b" "Re(F!1(j!1)(x!1))" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil )"2" assert )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 ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (skosimp*)"2" (case-replace "m!1=0" )"1" (expand "sigma" )"1" "real_expt_pos" "px" "2" "a" "1-n!1" ))"1" (assert ) nil nil )) nil ))nil )"2" (case "m!1>=1" )"1" (hide 1)"1" "sigma_geometric" "x" "1/2" "n" "n!1+m!1-1" ))"1" "n!1=0" )"1" assert )"1" rewrite "real_expt_int_rew" 1)"1" assert )"1" rewrite "expt_x1" )"1" case "(1 - (1 / 2) ^ m!1) / (1 - 1 / 2) < 2" )"1" (assert ) nil nil )"2" "2" "2" "2" assert )"2" rewrite "real_expt_int_rew" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "n!1>=1" )"1" "1" "sigma_geometric" "x" "1/2" "n" "n!1-1" ))"1" "sigma_split" "low" "0" "high" "n!1+m!1-1" "F" "geometric(1 / 2)" "z" "n!1-1" ))"1" assert )"1" "LHS" "sigma(n!1, m!1 - 1 + n!1, geometric(1 / 2))" )"1" "DRL1" "sigma(0, m!1 - 1 + n!1, geometric(1 / 2))" )"1" "DRL2" "sigma(0, n!1 - 1, geometric(1 / 2))" )"1" rewrite "real_expt_int_rew" )"1" assert )"1" case "DRL1-DRL2 = 2*(exponentiation.^(1/2,n!1)-exponentiation.^(1/2,m!1+n!1))" )"1" rewrite "expt_plus" "1" "expt_plus" "n0x" "2" "i" "1" "j" "-n!1" ))"1" rewrite "expt_x1" )"1" replace "1" "both_sides_times_pos_lt1" "pz" " 2 * exponentiation.^(1 / 2, n!1)" "x" "1-exponentiation.^(1 / 2, m!1)" "y" "1" ))"1" rewrite "expt_inverse" "1" rewrite "inv_expt" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"3" (skosimp)"3" (inst + "n!1+m!1" ) (("3" (assert ) nil nil ))nil ))nil ))nil )"2" (hide 2)"2" (skolem + ("x!1" "n!1" "_" ))"2" (inst - "x!1" "_" )"2" (case-replace "N!1(x!1)" )"2" (assert )"2" (hide 1)"2" (induct "m" )"1" expand "sigma" )"1" expand "abs" )"1" expand "sq_abs" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" "2" assert )"2" expand "sigma" 1)"2" "j!1+n!1" )"2" "j!1+n!1" )"2" expand "geometric" 1 1)"2" rewrite "real_expt_neg" "2" rewrite "real_expt_int_rew" "2" "polar.abs_triangle" "z1" "F!1(1 + (j!1 + n!1))(x!1) - F!1(j!1 + n!1)(x!1)" "z2" "F!1(j!1 + n!1)(x!1) - F!1(n!1)(x!1)" ))"2" "abs(F!1(1 + j!1 + n!1)(x!1) - F!1(n!1)(x!1))=abs(F!1(1 + (j!1 + n!1))(x!1) - F!1(j!1 + n!1)(x!1) + ") "1" assert )nil nil )"2" "2" expand "abs" )"2" expand "sq_abs" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "n!1+m!1" )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (skosimp)"3" (inst + "3" ) (("3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp)"2" "EE" "lambda n: choose[(S)]({E:(S) | null_set?(E) & forall (x:T): not E(x) => abs(F!1(n+1)(x)-F!1(n)(x)) <= essential_bound(F!1(n+1)-F!1(n))})" )"1" (inst + "IUnion(EE)" )"1" (hide -1)"1" (skosimp)"1" case "forall n: not EE(n)(x!1) => abs(F!1(n + 1)(x!1) - F!1(n)(x!1)) <= essential_bound(F!1(n + 1) - F!1(n))" )"1" (expand "IUnion" )"1" (inst + "n!1" )"1" (inst - "n!1" ) (("1" (assert ) nil nil ))nil ))nil ))nil )"2" (hide 2 3)"2" (skosimp)"2" (expand "EE" )"2" case "nonempty?[(S)]({E: (S) | NOT E(x) =>") "1" "choose_member[(S)]" "a" "{E: (S) | NOT E(x) =>")) "1" "CC" "choose[(S)] NOT E(x) =>") "1" "1" expand "member" )"1" "x!1" )"1" (assert ) nil nil ))nil ))nil )"2" expand "nonempty?" )"2" (propax) nil nil ))nil ))nil ))nil ))nil )"2" "2" expand "nonempty?" )"2" expand "empty?" )"2" expand "member" )"2" "essential_bound_def2" "f" "F!1(n!2 + 1) - F!1(n!2)" ))"2" expand "ae_le?" )"2" expand "pointwise_ae?" )"2" expand "ae?" )"2" expand "fullset" )"2" expand "ae_in?" )"2" "2" "E!1" )"2" expand "negligible_set?" )"2" "2" "X!1" )"1" assert )"1" "1" "x!2" )"1" assert )"1" expand "subset?" )"1" "x!2" )"1" assert )"1" expand "abs" "1" expand "-" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "null_set_is_measurable" )"2" "X!1" )"2" expand "measurable_set?" )"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 )"2" (hide 2)"2" (skosimp)"2" (expand "nonempty?" )"2" (expand "empty?" )"2" (expand "member" )"2" "diff_essentially_bounded" "f0" "F!1(1+n!1)" "f1" "F!1(n!1)" ))"2" "essential_bound_def2" "f" "((-[T])(F!1(1 + n!1), F!1(n!1)))" ))"2" "EB" " essential_bound(((-[T])(F!1(1 + n!1), F!1(n!1))))" )"2" "2" expand "ae_le?" )"2" expand "pointwise_ae?" )"2" expand "ae?" )"2" expand "fullset" )"2" expand "ae_in?" )"2" expand "member" )"2" "2" "E!1" )"2" expand "negligible_set?" )"2" "2" "X!1" )"1" assert )"1" "1" expand "subset?" )"1" "x!1" )"1" expand "member" )"1" assert )"1" "x!1" )"1" assert )"1" expand "abs" "1" expand "-" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "null_set_is_measurable" )"2" "X!1" )"2" expand "measurable_set?" )"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 )"(partial_order?[set[T]])" nil )"bool" sets nil )"set[T]" essential_bound_complete_scaf nil )nil essentially_bounded nil )"[n: nat -> NOT E(x) =>" nil )"set[T]" indexed_sets nil )"(S)" nil )"null_set[T, S, mu]" nil )nil essentially_boundednil )"set[T]" essential_bound_complete_scaf nil )"nat" essential_bound_complete_scaf nil )"bool" metric_space_def"metric_space/" )"nat" essential_bound_complete_scaf nil )"nat" essential_bound_complete_scaf nil )nil real_props nil )nil sq "reals/" )"nat" essential_bound_complete_scaf nil )"nat" essential_bound_complete_scaf nil )"bool" metric_space_def "metric_space/" )"bool" metric_space_def"metric_space/" )"bool" metric_space_def"metric_space/" )nil complex_topology nil )"hausdorff[complex]" nil )"(hausdorff?)" nil )"null_set[T, S, mu]" nil )"setofsets[T]" metric_space_def"metric_space/" )"bool" topological_convergence "topology/" )"sequence[essentially_bounded]" nil )"T" topological_convergence "topology/" )nil topological_convergence "topology/" )"[[real, real] -> (complex_?)]" "complex_alt/" )IF const-decl "[boolean, T, T -> T]" if_def nil )"[complex -> boolean]" complex_types"complex_alt/" )nil complex_types "complex_alt/" )"[numfield, numfield -> numfield]" number_fields nil )"real" complex_types "complex_alt/" )"real" complex_types "complex_alt/" )"bool" topology "topology/" )nil topology "topology/" )"bool" topological_convergence"topology/" )nil topological_convergence "topology/" )nil sqrt "reals/" )nil sq "reals/" )"bool" metric_space_def"metric_space/" )nil measure_theory"measure_integration/" )nil measure_space_def"measure_integration/" )"bool" measure_space_def"measure_integration/" )nil measure_space_def"measure_integration/" )"bool" measure_space "measure_integration/" )"[T -> real]" real_fun_ops "reals/" )nil complex_measurable nil )nil complex_fun_ops "complex_alt/" )nil complex_fun_ops "complex_alt/" )nil measure_space_def"measure_integration/" )nil measure_space"measure_integration/" )nil measure_space"measure_integration/" )"bool" metric_space_def"metric_space/" )"real" reals nil )nil complex_types "complex_alt/" )nil complex_types "complex_alt/" )nil real_props nil )"posnat" exponentiation nil )"real" exponentiation nil )"nnreal" nil )nil real_expt "power/" )"nat" essential_bound_complete_scaf nil )"set[T]" metric_space_def "metric_space/" )nil metric_space"metric_space/" )nil exponentiation nil )nil integers nil )nil real_expt "power/" )"bool" booleans nil )"bool" measure_theory"measure_integration/" )nil measure_theory"measure_integration/" )nil essentially_bounded nil )nil real_expt "power/" )"int" essential_bound_complete_scaf nil )"posint" exponentiation nil )"posint" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )nil exponentiation nil )"[T -> complex]" nil )"negligible[T, S, mu]" nil )"set" sets nil )"posreal" nil )nil exponentiation nil )"complex" complex_types "complex_alt/" )"nnreal" complex_types "complex_alt/" )"real" reals nil )nil complex_types "complex_alt/" )nil complex_types "complex_alt/" )nil complex_types "complex_alt/" )nil complex_types "complex_alt/" )nil polar "complex_alt/" )"posreal" nil )"bool" complex_measure_theory nil )"bool" measure_space_def"measure_integration/" )"[T -> real]" complex_fun_ops "complex_alt/" )"[T -> real]" complex_fun_ops "complex_alt/" )nil complex_measurablenil )"bool" complex_measurable nil )nil complex_measurablenil )"set" sets nil )"nat" measure_space "measure_integration/" )"complex" complex_types "complex_alt/" )"bool" complex_measurable nil )"measurable_set[T, S]" nil )"(S)" measure_def"measure_integration/" )nil series "series/" )"odd_int" integersnil )"rat" rationals nil )nil exponentiation nil )nil exponentiation nil )nil real_props nil )"odd_int" integers nil )nil exponentiation nil )nil reals nil )nil sigma "reals/" )"odd_int" integersnil )"rat" rationals nil )"real" reals nil )nil real_props nil )nil real_props nil )"posrat" nil )"nzrat" rationals nil )"real" reals nil )"even_int" integersnil )"[bool, bool -> bool]" booleans nil )nil exponentiation nil )"rat" rationals nil )"even_int" integersnil )"sequence[real]" series "series/" )"real" sigma "reals/" )nil sigma "reals/" )nil sigma "reals/" )"nnreal" polar "complex_alt/" )NOT const-decl "[bool -> bool]" booleans nil )nil measure_theory"measure_integration/" )"bool" measure_theory "measure_integration/" )"nat" essential_bound_complete_scaf nil )"T" function_iterate nil )"[nat, nat]" essential_bound_complete_scafnil )"sequence[essentially_bounded]" nil )"nzint" integers nil )"even_int" integers nil )"bool" subseq "topology/" )"T3" function_props nil )"posreal" nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )"nonneg_int" nil )"nnreal" nil )"(total_order?[real])" nil )nil real_expt "power/" )"nnreal" essential_bound_complete_scaf nil )"bool" measure_theory "measure_integration/" )"bool" measure_theory"measure_integration/" )"set" sets nil )"bool" sets nil )nil complex_types "complex_alt/" )nil complex_types "complex_alt/" )"real" reals nil )"complex" complex_types "complex_alt/" )"bool" measure_theory "measure_integration/" )"bool" measure_theory "measure_integration/" )"measurable_set[T, S]" nil )"(S)" nil )"[T -> nonneg_real]" complex_fun_ops"complex_alt/" )"nnreal" essential_bound_complete_scaf nil )"bool" reals nil )nil essentially_bounded nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"posrat" nil )nil exponentiation nil )nil real_expt "power/" )"posrat" exponentiation nil )"nnrat" exponentiation nil )"real" exponentiation nil )nil real_expt "power/" )"[d: [nat, nat] -> AND j >= k =>" nil )"bool" sets nil )"[nat, nat]" essential_bound_complete_scafnil )nil real_expt "power/" )nil sets_lemmas nil )"(strict_total_order?[real])" real_props nil )"[nat -> nat]" essential_bound_complete_scafnil )"posint" nil )"[nat, nat]" essential_bound_complete_scafnil )"even_int" integersnil )"[nat, nat]" essential_bound_complete_scafnil )nil naturalnumbers nil )nil defined_types nil )"int" integers nil )"nat" essential_bound_complete_scaf nil )"nat" essential_bound_complete_scaf nil )"[numfield, numfield -> numfield]" number_fields nil )"int" integers nil )"bool" real_fun_preds "reals/" )AND const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )set type-eq-decl nil sets nil )"bool" sets nil )"(p)" sets nil )"essentially_bounded[T, S, mu]" essential_bound_complete_scaf nil )"posint" nil )"int" integers nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )nil essential_bound_complete_scaf nil )nil complex_types "complex_alt/" )nil defined_types nil )nil sets nil )"bool" subset_algebra_def"measure_integration/" )nil subset_algebra_def"measure_integration/" )"sigma_algebra[T]" nil )nil real_types nil )nil extended_nnreal"extended_nnreal/" )"bool" generalized_measure_def"measure_integration/" )nil generalized_measure_def"measure_integration/" )"measure_type[T, S]" nil )"bool" essentially_bounded nil )nil essentially_boundednil )nil sequences nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil )"nnreal" essentially_bounded nil )"[T -> complex]" complex_fun_ops "complex_alt/" )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )"nnreal" real_expt "power/" )"[numfield -> numfield]" number_fields nil )nil real_types nil )nil real_types nil ))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Dauer der Verarbeitung: 0.174 Sekunden
(vorverarbeitet am 2026-04-27)
¤ *© Formatika GbR, Deutschland
2026-05-26
