|
(integral_convergence
(monotone_convergence 0
(monotone_convergence-1 nil 3409506492
("" (skosimp*)
((""
(case-replace
"(EXISTS f: ae_convergence?(F!1, f)) IFF bounded?(integral o F!1)")
(("1" (assert)
(("1" (skolem!)
(("1" (flatten)
(("1" (hide -2)
(("1" (split -1)
(("1" (expand "ae_increasing?")
(("1" (expand "ae_convergence?")
(("1" (expand "fullset")
(("1" (expand "ae_convergence_in?")
(("1" (expand "ae_in?")
(("1" (skolem - "E1")
(("1" (skolem - "E2")
(("1"
(typepred "union(E1,E2)")
(("1"
(expand "negligible_set?")
(("1"
(skosimp)
(("1"
(lemma "null_set_is_measurable")
(("1"
(inst - "X!1")
(("1"
(lemma
"monotone_convergence_scaf"
("f"
"phi(complement(X!1))*f!1"
"F"
"lambda n: phi(complement(X!1))*F!1(n)"))
(("1"
(case-replace
"integral o (LAMBDA n: phi(complement(X!1)) * F!1(n))=integral o F!1")
(("1"
(hide -1)
(("1"
(replace -5)
(("1"
(case-replace
"integral(phi(complement(X!1)) * f!1)=integral(f!1)")
(("1"
(split -2)
(("1"
(flatten)
nil
nil)
("2"
(hide 2)
(("2"
(expand
"pointwise_converges_upto?")
(("2"
(case-replace
"pointwise_increasing?(LAMBDA n: phi(complement(X!1)) * F!1(n))")
(("1"
(expand
"pointwise_convergence?")
(("1"
(skosimp)
(("1"
(inst
-8
"x!1")
(("1"
(expand
"complement")
(("1"
(expand
"member")
(("1"
(expand
"phi")
(("1"
(expand
"member")
(("1"
(hide
-1
-2)
(("1"
(expand
"subset?")
(("1"
(expand
"union")
(("1"
(expand
"member")
(("1"
(inst
-
"x!1")
(("1"
(expand
"*"
1)
(("1"
(case-replace
"E2(x!1)")
(("1"
(assert)
(("1"
(hide-all-but
1)
(("1"
(expand
"convergence?")
(("1"
(skosimp)
(("1"
(inst
+
"0")
(("1"
(skosimp)
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(case-replace
"X!1(x!1)")
(("1"
(hide-all-but
2)
(("1"
(expand
"convergence?")
(("1"
(skosimp)
(("1"
(inst
+
"0")
(("1"
(skosimp)
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(hide
-1
-5
-7)
(("2"
(expand
"pointwise_increasing?")
(("2"
(skosimp)
(("2"
(expand
"*")
(("2"
(expand
"complement")
(("2"
(expand
"phi")
(("2"
(expand
"member")
(("2"
(inst
-
"x!1")
(("2"
(expand
"subset?")
(("2"
(expand
"union")
(("2"
(expand
"member")
(("2"
(inst
-
"x!1")
(("2"
(case-replace
"X!1(x!1)")
(("1"
(expand
"increasing?")
(("1"
(propax)
nil
nil))
nil)
("2"
(assert)
(("2"
(expand
"increasing?")
(("2"
(skosimp)
(("2"
(assert)
(("2"
(inst
-
"x!2"
"y!1")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide -1 2)
(("2"
(lemma
"integral_ae_eq"
("f"
"f!1"
"h"
"phi(complement(X!1)) * f!1"))
(("1"
(split -1)
(("1"
(flatten)
(("1"
(assert)
nil
nil))
nil)
("2"
(hide 2)
(("2"
(expand
"ae_eq?")
(("2"
(expand
"restrict")
(("2"
(expand
"pointwise_ae?")
(("2"
(expand
"*")
(("2"
(expand
"complement")
(("2"
(expand
"phi")
(("2"
(expand
"member")
(("2"
(expand
"ae?")
(("2"
(expand
"fullset")
(("2"
(expand
"ae_in?")
(("2"
(inst
+
"X!1")
(("1"
(skosimp)
(("1"
(assert)
nil
nil))
nil)
("2"
(expand
"negligible_set?")
(("2"
(inst
+
"X!1")
(("2"
(assert)
(("2"
(hide-all-but
1)
(("2"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(rewrite
"integrable_is_measurable")
(("2"
(hide 2)
(("2"
(rewrite
"indefinite_integrable")
(("2"
(hide
2)
(("2"
(rewrite
"measurable_complement")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3"
(hide 2)
(("3"
(rewrite
"indefinite_integrable")
(("3"
(rewrite
"measurable_complement")
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide -1 2)
(("2"
(expand "o ")
(("2"
(apply-extensionality
:hide?
t)
(("1"
(lemma
"integral_ae_eq"
("f"
"F!1(x!1)"
"h"
"phi(complement(X!1)) * F!1(x!1)"))
(("1"
(split -1)
(("1"
(flatten)
(("1"
(assert)
nil
nil))
nil)
("2"
(hide 2)
(("2"
(expand
"ae_eq?")
(("2"
(expand
"restrict")
(("2"
(expand
"pointwise_ae?")
(("2"
(expand
"*"
1)
(("2"
(expand
"complement")
(("2"
(expand
"phi")
(("2"
(expand
"member")
(("2"
(expand
"ae?")
(("2"
(expand
"fullset")
(("2"
(expand
"ae_in?")
(("2"
(inst
+
"X!1")
(("1"
(skosimp)
(("1"
(assert)
nil
nil))
nil)
("2"
(expand
"negligible_set?")
(("2"
(inst
+
"X!1")
(("2"
(assert)
(("2"
(hide-all-but
1)
(("2"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(rewrite
"integrable_is_measurable")
(("2"
(rewrite
"indefinite_integrable")
(("2"
(rewrite
"measurable_complement")
nil
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp)
(("2"
(rewrite
"indefinite_integrable")
(("2"
(rewrite
"measurable_complement")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp)
(("2"
(rewrite
"indefinite_integrable")
(("2"
(rewrite
"measurable_complement")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (inst + "f!1") nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (split)
(("1" (skosimp*)
(("1" (expand "bounded?")
(("1" (split)
(("1" (expand "bounded_above?")
(("1" (inst + "integral(f!1)")
(("1" (skolem + ("n!1"))
(("1" (expand "o ")
(("1" (expand "ae_convergence?")
(("1" (expand "ae_increasing?")
(("1" (expand "ae_convergence_in?")
(("1"
(expand "fullset")
(("1"
(expand "ae_in?")
(("1"
(skosimp*)
(("1"
(typepred "union(E!1,E!2)")
(("1"
(expand "negligible_set?")
(("1"
(skosimp)
(("1"
(lemma
"integral_ae_le"
("f1"
"phi(complement(X!1))*F!1(n!1)"
"f2"
"phi(complement(X!1))*f!1"))
(("1"
(split -1)
(("1"
(lemma
"integral_ae_eq"
("f"
"f!1"
"h"
"phi(complement(X!1)) * f!1"))
(("1"
(split -1)
(("1"
(flatten)
(("1"
(replace -2 * rl)
(("1"
(lemma
"integral_ae_eq"
("f"
"F!1(n!1)"
"h"
"phi(complement(X!1)) * F!1(n!1)"))
(("1"
(split -1)
(("1"
(flatten)
(("1"
(assert)
nil
nil))
nil)
("2"
(hide-all-but
(-4 -5 1))
(("2"
(expand
"ae_eq?")
(("2"
(expand
"restrict")
(("2"
(expand
"pointwise_ae?")
(("2"
(expand
"ae?")
(("2"
(expand
"*")
(("2"
(expand
"complement")
(("2"
(expand
"phi")
(("2"
(expand
"member")
(("2"
(expand
"fullset")
(("2"
(expand
"ae_in?")
(("2"
(inst
+
"X!1")
(("1"
(skosimp)
(("1"
(assert)
nil
nil))
nil)
("2"
(rewrite
"null_is_negligible")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(rewrite
"integrable_is_measurable")
nil
nil))
nil))
nil))
nil)
("2"
(hide -1 -4 -5 2)
(("2"
(expand "ae_eq?")
(("2"
(expand
"restrict")
(("2"
(expand
"pointwise_ae?")
(("2"
(expand
"complement")
(("2"
(expand
"phi")
(("2"
(expand
"member")
(("2"
(expand
"ae?")
(("2"
(expand
"fullset")
(("2"
(expand
"ae_in?")
(("2"
(inst
+
"X!1")
(("1"
(skosimp)
(("1"
(assert)
(("1"
(expand
"*")
(("1"
(assert)
nil
nil))
nil))
nil))
nil)
("2"
(rewrite
"null_is_negligible")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(rewrite
"integrable_is_measurable")
nil
nil))
nil)
("2"
(hide 2)
(("2"
(expand "ae_le?")
(("2"
(expand "*")
(("2"
(expand
"pointwise_ae?")
(("2"
(expand
"complement")
(("2"
(expand
"phi")
(("2"
(expand
"member")
(("2"
(expand
"ae?")
(("2"
(expand
"fullset")
(("2"
(expand
"ae_in?")
(("2"
(inst
+
"X!1")
(("1"
(skosimp)
(("1"
(assert)
(("1"
(expand
"union")
(("1"
(expand
"subset?")
(("1"
(expand
"member")
(("1"
(inst
-
"x!1")
(("1"
(inst
-
"x!1")
(("1"
(inst
-
"x!1")
(("1"
(case-replace
"E!1(x!1)")
(("1"
(case-replace
"E!2(x!1)")
(("1"
(assert)
(("1"
(hide
1
2
3
-1
-2)
(("1"
(rewrite
"metric_convergence_def")
(("1"
(case
"F!1(n!1)(x!1)-f!1(x!1)>0")
(("1"
(expand
"metric_converges_to")
(("1"
(inst
-
"F!1(n!1)(x!1) - f!1(x!1)")
(("1"
(hide
1)
(("1"
(skosimp)
(("1"
(inst
-
"n!1+n!2")
(("1"
(assert)
(("1"
(inst
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.248 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
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.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
