|
(essential_bound_complete_scaf
(mu_TCC1 0
(mu_TCC1-1 nil 3502969751
("" (typepred "S")
(("" (expand "sigma_algebra?")
(("" (flatten)
(("" (expand "subset_algebra_empty?")
(("" (expand "member") (("" (propax) nil nil)) nil)) nil))
nil))
nil))
nil)
((subset_algebra_empty? const-decl "bool" subset_algebra_def
"measure_integration/")
(member const-decl "bool" sets nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(T formal-type-decl nil essential_bound_complete_scaf nil)
(setof type-eq-decl nil defined_types nil)
(setofsets type-eq-decl nil sets nil)
(sigma_algebra? const-decl "bool" subset_algebra_def
"measure_integration/")
(sigma_algebra nonempty-type-eq-decl nil subset_algebra_def
"measure_integration/")
(S formal-const-decl "sigma_algebra[T]"
essential_bound_complete_scaf nil))
nil))
(essential_bound_complete_scaf 0
(essential_bound_complete_scaf-1 nil 3502969847
(""
(case "FORALL (F: sequence[essentially_bounded]):
(FORALL n: essential_bound(F(n+1) - F(n)) < 2^(-n))
IMPLIES
(EXISTS f:
FORALL r:
EXISTS n: FORALL i: i >= n => essential_bound(f - F(i)) < r)")
(("1" (skosimp)
(("1"
(name "NEXT"
"lambda (n,m:nat): (n+1,choose({k:nat | k > m & FORALL i, j:
i >= k 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"
(skosimp)
(("1"
(inst + "SEQ(n!1+n!2)")
(("1"
(skosimp)
(("1"
(inst - "n!1+n!2")
(("1"
(assert)
(("1"
(inst - "n!1+n!2" "i!1")
(("1"
(assert)
(("1"
(expand "o" -2)
(("1"
(lemma
"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"
(name
"LHS1"
"essential_bound(f!1 - F!1(SEQ(n!1 + n!2)) -
(F!1(i!1) - F!1(SEQ(n!1 + n!2))))")
(("1"
(name-replace
"LHS2"
"essential_bound(f!1 - F!1(i!1))")
(("1"
(case-replace
"LHS1=LHS2")
(("1"
(assert)
nil
nil)
("2"
(hide-all-but
1)
(("2"
(expand
"LHS2")
(("2"
(expand
"LHS1")
(("2"
(expand
"-")
(("2"
(assert)
(("2"
(name-replace
"F1"
"F!1(i!1)")
(("2"
(name-replace
"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"
(lemma
"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"
(hide-all-but 1)
(("2"
(lemma "small_expt" ("px" "1/2"))
(("2"
(assert)
(("2"
(inst - "r!1/2")
(("2"
(skosimp)
(("2"
(inst + "n!2")
(("2"
(rewrite "real_expt_neg")
(("2"
(rewrite
"real_expt_int_rew")
(("2"
(expand "^")
(("2"
(propax)
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"
(name-replace
"NN"
"iterate(NEXT, 1 + n!1)(0, 0)")
(("2"
(expand "NEXT")
(("2"
(case
"nonempty?({k: nat |
k > NN`2 &
(FORALL i, j:
i >= k AND j >= k =>
essential_bound(F!1(j) - F!1(i)) < 2 ^ (-NN`1))})")
(("1"
(lemma
"choose_member"
("a"
"{k: nat |
k > NN`2 &
(FORALL i, j:
i >= k AND j >= k =>
essential_bound(F!1(j) - F!1(i)) < 2 ^ (-NN`1))}"))
(("1"
(split)
(("1"
(name-replace
"CC"
"choose({k: nat |
k > NN`2 &
(FORALL i, j:
i >= k AND j >= k =>
essential_bound(F!1(j) - F!1(i)) < 2 ^ (-NN`1))})")
(("1"
(expand "member")
(("1"
(flatten)
(("1"
(assert)
nil
nil))
nil))
nil))
nil)
("2"
(expand "nonempty?")
(("2" (propax) nil nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(expand "nonempty?")
(("2"
(expand "empty?")
(("2"
(expand "member")
(("2"
(inst
-2
"2 ^ (-NN`1)")
(("1"
(skosimp)
(("1"
(inst
-
"n!2+NN`2+1")
(("1"
(assert)
(("1"
(skosimp)
(("1"
(inst
-
"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"
(name-replace
"NN"
"iterate(NEXT, 1 + i!1)(0, 0)")
(("1"
(expand "NEXT")
(("1"
(hide -2 -1)
(("1"
(case
"nonempty?({k: nat |
k > NN`2 &
(FORALL i, j:
i >= k AND j >= k =>
essential_bound(F!1(j) - F!1(i)) < 2 ^ (-NN`1))})")
(("1"
(lemma
"choose_member"
("a"
"{k: nat |
k > NN`2 &
(FORALL i, j:
i >= k AND j >= k =>
essential_bound(F!1(j) - F!1(i)) < 2 ^ (-NN`1))}"))
(("1"
(split)
(("1"
(name-replace
"RHS"
"choose({k: nat |
k > NN`2 &
(FORALL i, j:
i >= k AND j >= k =>
essential_bound(F!1(j) - F!1(i)) < 2 ^ (-NN`1))})")
(("1"
(expand "member")
(("1"
(flatten)
(("1"
(assert)
nil
nil))
nil))
nil))
nil)
("2"
(expand "nonempty?")
(("2"
(propax)
nil
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(expand "nonempty?")
(("2"
(expand "empty?")
(("2"
(expand "member")
(("2"
(inst
-3
"2 ^ (-NN`1)")
(("1"
(skosimp)
(("1"
(inst
-
"n!1+NN`2+1")
(("1"
(assert)
(("1"
(skosimp)
(("1"
(inst
-
"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"
(skosimp)
(("2"
(inst - "i!1")
(("2"
(name-replace "LHS" "SEQ(i!1)")
(("2"
(hide -2 -3 -4)
(("2"
(expand "SEQ")
(("2"
(expand "iterate" 1)
(("2"
(name-replace
"NN"
"iterate(NEXT, 2 + i!1 + j!1)(0, 0)")
(("2"
(expand "NEXT")
(("2"
(case
"nonempty?({k: nat |
k > NN`2 &
(FORALL i, j:
i >= k AND j >= k =>
essential_bound(F!1(j) - F!1(i)) < 2 ^ (-NN`1))})")
(("1"
(lemma
"choose_member"
("a"
"{k: nat |
k > NN`2 &
(FORALL i, j:
i >= k AND j >= k =>
essential_bound(F!1(j) - F!1(i)) < 2 ^ (-NN`1))}"))
(("1"
(split)
(("1"
(name-replace
"ZZ"
"choose({k: nat |
k > NN`2 &
(FORALL i, j:
i >= k AND j >= k =>
essential_bound(F!1(j) - F!1(i)) < 2 ^ (-NN`1))})")
(("1"
(expand
"member")
(("1"
(flatten)
(("1"
(assert)
nil
nil))
nil))
nil))
nil)
("2"
(expand
"nonempty?")
(("2"
(propax)
nil
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(expand
"nonempty?")
(("2"
(expand "empty?")
(("2"
(expand
"member")
(("2"
(inst
-4
"2 ^ (-NN`1)")
(("1"
(skosimp)
(("1"
(inst
-
"n!1+NN`2+1")
(("1"
(assert)
(("1"
(skosimp)
(("1"
(inst
-
"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 |
k > 0 &
(FORALL i, j:
i >= k AND j >= k =>
essential_bound(F!1(j) - F!1(i)) < 2 ^ (-0))})")
(("1"
(lemma
"choose_member"
("a"
"{k: nat |
k > 0 &
(FORALL i, j:
i >= k AND j >= k =>
essential_bound(F!1(j) - F!1(i)) < 2 ^ (-0))}"))
(("1"
(replace -3)
(("1"
(split -1)
(("1"
(expand "member")
(("1"
(flatten)
(("1"
(inst - "ZZ" "i!1")
(("1" (assert) nil nil))
nil))
nil))
nil)
("2"
(expand "nonempty?")
(("2" (propax) nil nil))
nil))
nil))
nil))
nil)
("2"
(hide -1 -2 2)
(("2"
(expand "nonempty?")
(("2"
(expand "empty?")
(("2"
(expand "member")
(("2"
(inst -4 "2^(-0)")
(("1"
(skosimp)
(("1"
(inst - "n!1+1")
(("1"
(assert)
(("1"
(skosimp)
(("1"
(inst
-5
"i!2"
"j!1")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(lemma
"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"
(name-replace "NN"
"iterate(NEXT, 1 + j!1)(0, 0)")
(("2"
(expand "NEXT")
(("2"
(case
"nonempty?({k: nat |
k > NN`2
&
(FORALL
i, j:
i >= k AND j >= k
=>
essential_bound(F!1(j) - F!1(i))
<
2 ^ (-NN`1))})")
(("1"
(lemma
"choose_member"
("a"
"{k: nat |
k > NN`2
&
(FORALL
i, j:
i >= k AND j >= k
=>
essential_bound(F!1(j) - F!1(i))
<
2 ^ (-NN`1))}"))
(("1"
(split -1)
(("1"
(expand "member")
(("1"
(name-replace
"CC"
"choose({k: nat |
k > NN`2
&
(FORALL
i, j:
i >= k AND j >= k
=>
essential_bound(F!1(j) - F!1(i))
<
2 ^ (-NN`1))})")
(("1"
(flatten)
(("1"
(inst - "CC" "i!1")
(("1"
(case-replace
"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"
(inst - "1+j!1")
nil
nil)
("2"
(hide-all-but 1)
(("2"
(induct "n")
(("1"
(expand
"iterate")
(("1"
(propax)
nil
nil))
nil)
("2"
(skosimp)
(("2"
(expand
"iterate"
1)
(("2"
(expand
"NEXT"
1
1)
(("2"
(propax)
nil
nil))
nil))
nil))
nil)
("3"
(skosimp)
(("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"
(hide 2 -1 -2)
(("2"
(expand "nonempty?")
(("2"
(expand "empty?")
(("2"
(expand "member")
(("2"
(inst -3 "2^(-NN`1)")
(("1"
(skosimp)
(("1"
(inst - "n!1+NN`2+1")
(("1"
(assert)
(("1"
(skosimp)
(("1"
(inst
-
"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]):
EXISTS (N:null_set): FORALL (x:T,n): 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) =>
abs(F!1(n + m)(x) - F!1(n)(x)) <= sigma[nat](n,n+m-1,geometric(1/2))")
(("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"
(lemma "pointwise_complex_measurable"
("f" "g!1" "u" "LAMBDA n:
LAMBDA (x: T):
phi(complement(N!1))(x) * F!1(n)(x)"))
(("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"
(inst + "g!1")
(("1"
(skosimp)
(("1"
(hide-all-but (-2 1))
(("1"
(lemma
"exp_of_exists"
("py" "r!1" "b" "2"))
(("1"
(skosimp)
(("1"
(lemma
"both_sides_real_expt_gt1_lt"
("gt1x"
"2"
"a"
"i!1-1"
"b"
"i!1"))
(("1"
(assert)
(("1"
(rewrite
"real_expt_int_rew"
*
:dir
rl)
(("1"
(rewrite
"real_expt_int_rew"
*
:dir
rl)
(("1"
(case "3-i!1>=0")
(("1"
(inst + "3-i!1")
(("1"
(skosimp)
(("1"
(lemma
"both_sides_real_expt_gt1_le"
("gt1x"
"2"
"a"
"2-i!2"
"b"
"i!1-1"))
(("1"
(assert)
(("1"
(lemma
"essential_bound_def1"
("f"
"g!1 - F!1(i!2)"
"K"
"2^(2-i!2)"))
(("1"
(split
-1)
(("1"
(assert)
nil
nil)
("2"
(hide
2)
(("2"
(expand
"ae_le?")
(("2"
(expand
"pointwise_ae?")
(("2"
(expand
"ae?")
(("2"
(expand
"fullset")
(("2"
(expand
"ae_in?")
(("2"
(inst
+
"N!1")
(("2"
(skosimp)
(("2"
(expand
"member")
(("2"
(inst
-
"x!1"
"i!2")
(("2"
(assert)
(("2"
(expand
"abs"
2)
(("2"
(assert)
(("2"
(expand
"-"
2)
(("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"
(hide 1)
(("1"
(lemma
"both_sides_real_expt_gt1_lt"
("gt1x"
"2"
"a"
"3"
"b"
"i!1"))
(("1"
(assert)
(("1"
(rewrite
"real_expt_int_rew"
-1)
(("1"
(rewrite
"expt_x3")
(("1"
(inst
+
"0")
(("1"
(skosimp)
(("1"
(inst
-
"_"
"i!2")
(("1"
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.168 Sekunden
(vorverarbeitet)
¤
|
Laden
Fehler beim Verzeichnis:
in der Quellcodebibliothek suchen
Die farbliche Syntaxdarstellung ist noch experimentell.
|
