|
(integral_convergence_scaf
(monotone_convergence_scaf 0
(monotone_convergence_scaf-1 nil 3409476910
(""
(case "FORALL (F: sequence[nn_integrable], f: [T -> nnreal]):
pointwise_converges_upto?(F, f)&bounded?(nn_integral o F) =>(nn_integrable?(f) AND converges_upto?((nn_integral o F), nn_integral(f)))")
(("1" (skosimp)
(("1" (inst - "lambda (n:nat): F!1(n)-F!1(0)" "f!1-F!1(0)")
(("1" (split -1)
(("1" (flatten)
(("1" (lemma "nn_integrable_is_integrable")
(("1" (inst - "f!1 - F!1(0)")
(("1"
(lemma "integrable_add"
("f1" "f!1 - F!1(0)" "f2" "F!1(0)"))
(("1"
(case-replace "((+[T])(f!1 - F!1(0), F!1(0)))=f!1")
(("1" (hide -1)
(("1" (replace -1)
(("1" (expand "o ")
(("1" (expand "converges_upto?")
(("1" (flatten)
(("1"
(split)
(("1"
(rewrite "integral_nn" -4 :dir rl)
(("1"
(rewrite "integral_diff")
(("1"
(rewrite
"metric_convergence_def")
(("1"
(rewrite
"metric_convergence_def")
(("1"
(expand
"metric_converges_to")
(("1"
(skosimp)
(("1"
(inst - "r!1")
(("1"
(skosimp)
(("1"
(inst + "n!1")
(("1"
(skosimp)
(("1"
(inst - "i!1")
(("1"
(assert)
(("1"
(rewrite
"integral_nn"
-5
:dir
rl)
(("1"
(rewrite
"integral_diff")
(("1"
(assert)
(("1"
(expand
"ball")
(("1"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(skolem + ("n!1"))
(("2"
(lemma
"integrable_diff"
("f1"
"F!1(n!1)"
"f2"
"F!1(0)"))
(("2"
(lemma
"nn_integrable_is_nn_integrable"
("f"
"(-[T])(F!1(n!1), F!1(0))"))
(("2"
(case-replace
"(FORALL (x1: T): ((-[T])(F!1(n!1), F!1(0)))(x1) >= 0)")
(("2"
(expand
"pointwise_converges_upto?")
(("2"
(flatten)
(("2"
(hide-all-but
(1 -9))
(("2"
(skosimp)
(("2"
(expand
"-")
(("2"
(expand
"pointwise_increasing?")
(("2"
(inst
-
"x1!1")
(("2"
(expand
"increasing?")
(("2"
(inst
-
"0"
"n!1")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand "increasing?")
(("2"
(skolem + ("i!1" "j!1"))
(("2"
(flatten)
(("2"
(inst - "i!1" "j!1")
(("2"
(assert)
(("2"
(hide -5 -8 -3 -4)
(("2"
(rewrite
"integral_nn"
-3
:dir
rl)
(("2"
(rewrite
"integral_nn"
-3
:dir
rl)
(("2"
(rewrite
"integral_diff")
(("2"
(rewrite
"integral_diff")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but 1)
(("2" (apply-extensionality :hide? t)
(("2" (expand "+")
(("2" (expand "-") (("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (propax) nil nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (expand "pointwise_converges_upto?")
(("2" (flatten)
(("2" (split)
(("1" (expand "pointwise_convergence?")
(("1" (skosimp)
(("1" (inst - "x!1")
(("1" (rewrite "metric_convergence_def")
(("1" (rewrite "metric_convergence_def")
(("1" (expand "metric_converges_to")
(("1"
(skosimp)
(("1"
(inst - "r!1")
(("1"
(skosimp)
(("1"
(inst + "n!1")
(("1"
(skosimp)
(("1"
(inst - "i!1")
(("1"
(expand "ball")
(("1"
(assert)
(("1"
(expand "-")
(("1"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "pointwise_increasing?")
(("2" (skosimp)
(("2" (inst - "x!1")
(("2" (expand "increasing?")
(("2" (skolem + ("i!1" "j!1"))
(("2" (flatten)
(("2"
(inst - "i!1" "j!1")
(("2"
(expand "-")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (hide 2)
(("3" (expand "o ")
(("3" (expand "bounded?")
(("3" (flatten)
(("3" (split)
(("1" (expand "bounded_above?")
(("1" (skosimp)
(("1" (expand "pointwise_converges_upto?")
(("1" (flatten)
(("1" (hide -1)
(("1"
(expand "bounded_below?")
(("1"
(skosimp)
(("1"
(inst + "a!1-a!2")
(("1"
(skolem + ("n!1"))
(("1"
(inst - "n!1")
(("1"
(inst - "0")
(("1"
(rewrite
"integral_nn"
1
:dir
rl)
(("1"
(rewrite "integral_diff")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "bounded_below?")
(("2" (skosimp)
(("2" (expand "bounded_above?")
(("2" (expand "pointwise_converges_upto?")
(("2" (flatten)
(("2"
(hide -1)
(("2"
(skosimp)
(("2"
(inst + "a!1-a!2")
(("2"
(skolem + ("n!1"))
(("2"
(inst - "0")
(("2"
(inst - "n!1")
(("2"
(rewrite
"integral_nn"
1
:dir
rl)
(("2"
(rewrite "integral_diff")
(("2" (assert) 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 "-")
(("2" (expand "pointwise_converges_upto?")
(("2" (expand "pointwise_increasing?")
(("2" (flatten)
(("2" (inst - "x1!1")
(("2" (hide -3)
(("2" (expand "pointwise_convergence?")
(("2" (inst - "x1!1")
(("2" (rewrite "metric_convergence_def")
(("2"
(expand "metric_converges_to")
(("2"
(inst - "F!1(0)(x1!1)-f!1(x1!1)")
(("1"
(skosimp)
(("1"
(expand "ball")
(("1"
(expand "member")
(("1"
(inst - "n!1")
(("1"
(assert)
(("1"
(expand "increasing?")
(("1"
(inst - "0" "n!1")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (hide 2)
(("3" (skosimp)
(("3" (split)
(("1" (skosimp)
(("1" (expand "pointwise_converges_upto?")
(("1" (flatten)
(("1" (expand "pointwise_increasing?")
(("1" (inst - "x1!1")
(("1" (expand "increasing?")
(("1" (inst - "0" "n!1")
(("1" (expand "-") (("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(lemma "integrable_diff"
("f1" "F!1(n!1)" "f2" "F!1(0)"))
(("2" (expand "pointwise_converges_upto?")
(("2" (flatten)
(("2" (rewrite "nn_integrable_is_nn_integrable")
(("2" (skosimp)
(("2" (expand "pointwise_increasing?")
(("2" (inst - "x!1")
(("2" (expand "-")
(("2"
(expand "increasing?")
(("2"
(inst - "0" "n!1")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (skosimp)
(("2" (lemma "pointwise_measurable" ("u" "F!1" "f" "f!1"))
(("2" (split -1)
(("1"
(name "ISF"
"lambda (n:nat): choose({u:increasing_nn_isf | pointwise_convergence?(u,F!1(n))})")
(("1" (hide -1)
(("1"
(case "forall (n:nat): increasing_nn_isf?(ISF(n))")
(("1"
(case "forall (n:nat): pointwise_convergence?(ISF(n), F!1(n))")
(("1"
(name "G"
"lambda (n:nat): maximum(lambda (i:nat): ISF(i)(n),n)")
(("1"
(case "forall (n:nat,x:T): G(n)(x)<=F!1(n)(x)")
(("1"
(case "forall (n:nat, x: T): F!1(n)(x)<=f!1(x)")
(("1"
(case "forall (n:nat,x:T): 0 <= G(n)(x)")
(("1" (case "pointwise_increasing?(G)")
(("1"
(case
"nonempty?({nn:nn_isf | exists (n:nat): nn = G(n)})")
(("1"
(case "pointwise_bounded_above?(G)")
(("1"
(case
"pointwise_converges_upto?(G, f!1)")
(("1"
(case-replace
"nn_integrable?(f!1)")
(("1"
(expand "converges_upto?")
(("1"
(case-replace
"increasing?(nn_integral o F!1)")
(("1"
(case
"convergence?((nn_integral o G), nn_integral(f!1))")
(("1"
(expand
"pointwise_converges_upto?")
(("1"
(flatten)
(("1"
(rewrite
"metric_convergence_def")
(("1"
(rewrite
"metric_convergence_def")
(("1"
(case
"forall (n:nat): (nn_integral o G)(n)<=(nn_integral o F!1)(n)")
(("1"
(case
"increasing?(nn_integral o G)")
(("1"
(case
"forall (n:nat): (nn_integral o F!1)(n)<=nn_integral(f!1)")
(("1"
(name-replace
"LIMIT"
"nn_integral(f!1)")
(("1"
(name-replace
"INT_F"
"nn_integral o F!1")
(("1"
(name-replace
"INT_G"
"nn_integral o G")
(("1"
(hide-all-but
(-1
-2
-3
-4
-5
1))
(("1"
(expand
"metric_converges_to")
(("1"
(skosimp)
(("1"
(inst
-4
"r!1")
(("1"
(skosimp)
(("1"
(inst
+
"n!1")
(("1"
(skosimp)
(("1"
(inst
-4
"i!1")
(("1"
(expand
"ball")
(("1"
(assert)
(("1"
(inst
-
"i!1")
(("1"
(expand
"abs")
(("1"
(inst
-
"i!1")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but
(1
-5
-12))
(("2"
(skosimp)
(("2"
(expand
"o ")
(("2"
(lemma
"nn_integrable_le"
("g"
"F!1(n!1)"
"f"
"f!1"))
(("2"
(split
-1)
(("1"
(flatten)
nil
nil)
("2"
(skosimp)
(("2"
(inst
-
"n!1"
"x!1")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but
(1 -6 -10))
(("2"
(expand
"pointwise_increasing?")
(("2"
(expand
"increasing?")
(("2"
(expand
"o ")
(("2"
(skolem
+
("i!1"
"j!1"))
(("2"
(flatten)
(("2"
(lemma
"nn_integrable_le"
("g"
"G(i!1)"
"f"
"G(j!1)"))
(("2"
(split
-1)
(("1"
(flatten)
nil
nil)
("2"
(hide
2)
(("2"
(skosimp)
(("2"
(inst
-
"x!1")
(("2"
(inst
-
"i!1"
"j!1")
(("2"
(inst
-
"i!1"
"x!1")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but
(1 -9 -11))
(("2"
(skosimp)
(("2"
(expand
"o ")
(("2"
(lemma
"nn_integrable_le"
("g"
"G(n!1)"
"f"
"F!1(n!1)"))
(("2"
(split
-1)
(("1"
(flatten)
nil
nil)
("2"
(skosimp)
(("2"
(inst
-
"n!1"
"x!1")
(("2"
(inst
-
"n!1"
"x!1")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(expand
"pointwise_converges_upto?")
(("2"
(flatten)
(("2"
(hide
-1
-14
-15
-16
-17
-11)
(("2"
(copy -1)
(("2"
(expand
"nn_integrable?"
-1)
(("2"
(skosimp)
(("2"
(lemma
"nn_convergence"
("u1"
"u!1"
"f"
"f!1"
"u2"
"choose({u:increasing_nn_isf | pointwise_convergence?(u,f!1)})"))
(("1"
(replace
-2)
(("1"
(replace
-3)
(("1"
(split
-1)
(("1"
(flatten)
(("1"
(expand
"nn_integral"
1
2)
(("1"
(replace
-2
1
rl)
(("1"
(hide
-2)
(("1"
(hide
-1)
(("1"
(lemma
"nn_convergence"
("u1"
"u!1"
"f"
"f!1"
"u2"
"G"))
(("1"
(replace
-2)
(("1"
(replace
-3)
(("1"
(replace
-5)
(("1"
(flatten)
(("1"
(replace
-2)
(("1"
(expand
"o"
1
1)
(("1"
(case-replace
"(LAMBDA (x: nat): nn_integral(G(x)))=isf_integral o G")
(("1"
(rewrite
"hausdorff_convergence.limit_def"
1
:dir
rl)
nil
nil)
("2"
(hide
2)
(("2"
(apply-extensionality
:hide?
t)
(("1"
(expand
"o"
1)
(("1"
(rewrite
"nn_integral_isf")
(("1"
(expand
"nn_isf?")
(("1"
(skosimp)
(("1"
(inst
-11
"x!1"
"x!2")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"o")
(("2"
(skolem
+
"n!1")
(("2"
(lemma
"isf_integral_pos"
("i"
"G(n!1)"))
(("2"
(assert)
(("2"
(skosimp)
(("2"
(inst
-
"n!1"
"x!1")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3"
(skolem
+
"n!1")
(("3"
(split)
(("1"
(skosimp)
(("1"
(inst
-
"n!1"
"x1!1")
(("1"
(assert)
nil
nil))
nil))
nil)
("2"
(lemma
"nn_isf_is_nn_integrable"
("x"
"G(n!1)"))
(("1"
(assert)
nil
nil)
("2"
(expand
"nn_isf?")
(("2"
(skosimp)
(("2"
(inst
-
"n!1"
"x!1")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
--> --------------------
--> maximum size reached
--> --------------------
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.140Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Laden
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
in der Quellcodebibliothek suchen
Entwicklung einer Software für die statische Quellcodeanalyse
|
