|
(finite_fubini_tonelli
(mu_TCC1 0
(mu_TCC1-1 nil 3458551591
("" (typepred "S1")
(("" (expand "sigma_algebra?")
(("" (expand "subset_algebra_empty?")
(("" (flatten)
(("" (expand "member") (("" (propax) nil nil)) nil)) nil))
nil))
nil))
nil)
((member const-decl "bool" sets nil)
(subset_algebra_empty? const-decl "bool" subset_algebra_def nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(T1 formal-type-decl nil finite_fubini_tonelli nil)
(setof type-eq-decl nil defined_types nil)
(setofsets type-eq-decl nil sets nil)
(sigma_algebra? const-decl "bool" subset_algebra_def nil)
(sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
(S1 formal-const-decl "sigma_algebra[T1]" finite_fubini_tonelli
nil))
nil))
(nu_TCC1 0
(nu_TCC1-1 nil 3458551591
("" (typepred "S2")
(("" (expand "sigma_algebra?")
(("" (expand "subset_algebra_empty?")
(("" (flatten)
(("" (expand "member") (("" (propax) nil nil)) nil)) nil))
nil))
nil))
nil)
((member const-decl "bool" sets nil)
(subset_algebra_empty? const-decl "bool" subset_algebra_def nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(T2 formal-type-decl nil finite_fubini_tonelli nil)
(setof type-eq-decl nil defined_types nil)
(setofsets type-eq-decl nil sets nil)
(sigma_algebra? const-decl "bool" subset_algebra_def nil)
(sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
(S2 formal-const-decl "sigma_algebra[T2]" finite_fubini_tonelli
nil))
nil))
(finite_fubini_tonelli_1 0
(finite_fubini_tonelli_1-1 nil 3458552933
("" (skosimp)
(("" (split)
(("1" (flatten)
(("1" (typepred "h!1")
(("1" (expand "nn_measurable?")
(("1" (flatten)
(("1"
(lemma "nn_integrable_is_nn_integrable" ("f" "h!1"))
(("1" (split)
(("1" (hide -4)
(("1" (lemma "nn_integral_def" ("f" "h!1"))
(("1" (skolem - "HH")
(("1" (flatten)
(("1" (typepred "HH")
(("1" (case "FORALL (n: nat): isf?(HH(n))")
(("1"
(case
"FORALL (n: nat,z:[T1,T2]): HH(n)(z)>=0")
(("1"
(name
"FF"
"lambda (n:nat): lambda (x:T1): isf_integral(lambda (y:T2): HH(n)(x,y))")
(("1"
(case
"FORALL (n: nat): integrable?[T1, S1, to_measure(mu)](FF(n))")
(("1"
(case
"forall (n:nat): integral[T1,S1,to_measure(mu)](FF(n))=integral[[T1,T2],sigma_times(S1,S2),to_measure(fm_times(mu,nu))](HH(n))")
(("1"
(case-replace
"(isf_integral o HH)=integral o FF")
(("1"
(case
"forall (n:nat,x:T1): FF(n)(x)>=0")
(("1"
(case
"pointwise_increasing?(FF)")
(("1"
(case
"bounded?(integral o FF)")
(("1"
(lemma
"monotone_convergence[T1, S1, to_measure(mu)]"
("F" "FF"))
(("1"
(split -1)
(("1"
(flatten)
(("1"
(hide -1)
(("1"
(split -1)
(("1"
(skolem
-
"F")
(("1"
(inst
-
"F")
(("1"
(assert)
(("1"
(typepred
"F")
(("1"
(expand
"integrable1?")
(("1"
(expand
"ae_convergence?")
(("1"
(expand
"fullset")
(("1"
(expand
"ae_convergence_in?")
(("1"
(expand
"ae_in?")
(("1"
(skosimp)
(("1"
(expand
"member")
(("1"
(typepred
"E!1")
(("1"
(expand
"negligible_set?")
(("1"
(skolem
-
"N1")
(("1"
(flatten)
(("1"
(inst
+
"N1"
"F")
(("1"
(skosimp)
(("1"
(expand
"subset?")
(("1"
(inst
-
"x!1")
(("1"
(expand
"member")
(("1"
(inst
-
"x!1")
(("1"
(assert)
(("1"
(lemma
"monotone_convergence_scaf[T2,S2,to_measure(nu)]"
("f"
"LAMBDA (y: T2): h!1(x!1, y)"
"F"
"lambda (n:nat): lambda (y:T2): HH(n)(x!1,y)"))
(("1"
(split
-1)
(("1"
(flatten)
(("1"
(replace
-1)
(("1"
(name-replace
"LHS"
"integral(LAMBDA (y: T2): h!1(x!1, y))")
(("1"
(case-replace
"(integral o
(LAMBDA (n: nat): LAMBDA (y: T2): HH(n)(x!1, y)))=LAMBDA (n:nat): FF(n)(x!1)")
(("1"
(expand
"converges_upto?")
(("1"
(flatten)
(("1"
(hide-all-but
(-3
-7
3))
(("1"
(lemma
"hausdorff_convergence.unique_limit"
("u"
"LAMBDA (n: nat): FF(n)(x!1)"
"l1"
"LHS"
"l2"
"F(x!1)"))
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(apply-extensionality
:hide?
t)
(("1"
(expand
"FF"
1)
(("1"
(expand
"o"
1)
(("1"
(inst
-15
"x!2")
(("1"
(lemma
"isf_x_section"
("x"
"x!1"
"i"
"HH(x!2)"))
(("1"
(rewrite
"isf_integral"
1)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp)
(("2"
(inst
-15
"n!1")
(("2"
(lemma
"isf_x_section"
("x"
"x!1"
"i"
"HH(n!1)"))
(("2"
(lemma
"isf_is_integrable[T2, S2, to_measure(nu)]")
(("2"
(inst
-
"LAMBDA (y: T2): HH(n!1)(x!1, y)")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but
(1
-14
-15))
(("2"
(expand
"increasing_nn_isf?")
(("2"
(expand
"pointwise_converges_upto?")
(("2"
(split)
(("1"
(expand
"pointwise_convergence?")
(("1"
(skolem
+
"y!1")
(("1"
(inst
-
"(x!1,y!1)")
nil
nil))
nil))
nil)
("2"
(expand
"pointwise_increasing?")
(("2"
(skolem
+
"y!1")
(("2"
(inst
-
"(x!1,y!1)")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3"
(replace
-8
-5
rl)
(("3"
(hide-all-but
(-7
1
-13
-12
-8
-3
-6))
(("3"
(expand
"FF")
(("3"
(expand
"o ")
(("3"
(expand
"pointwise_increasing?")
(("3"
(inst
-2
"x!1")
(("3"
(hide
-4)
(("3"
(expand
"bounded?")
(("3"
(split)
(("1"
(expand
"bounded_above?")
(("1"
(inst
+
"F(x!1)")
(("1"
(skolem
+
"n!1")
(("1"
(inst-cp
-5
"n!1")
(("1"
(lemma
"isf_x_section"
("i"
"HH(n!1)"
"x"
"x!1"))
(("1"
(rewrite
"isf_integral")
(("1"
(rewrite
"metric_convergence_def")
(("1"
(expand
"metric_converges_to")
(("1"
(inst
-
"isf_integral(LAMBDA (y: T2): HH(n!1)(x!1, y))-F(x!1)")
(("1"
(skosimp)
(("1"
(inst
-
"n!1+n!2")
(("1"
(assert)
(("1"
(expand
"ball")
(("1"
(expand
"increasing?")
(("1"
(inst
-3
"n!1"
"n!1+n!2")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
nil
nil))
nil))
nil)
("2"
(skosimp)
(("2"
(rewrite
"isf_x_section")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"bounded_below?")
(("2"
(inst
+
"0")
(("2"
(skolem
+
"n!1")
(("2"
(inst
-5
"n!1")
(("2"
(lemma
"isf_x_section"
("i"
"HH(n!1)"
"x"
"x!1"))
(("2"
(rewrite
"isf_integral"
1)
(("2"
(inst
-4
"n!1"
"x!1")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp)
(("2"
(inst
-13
"n!1")
(("2"
(lemma
"isf_x_section"
("i"
"HH(n!1)"
"x"
"x!1"))
(("2"
(lemma
"isf_is_integrable[T2, S2, to_measure(nu)]")
(("2"
(inst
-
"LAMBDA (y: T2): HH(n!1)(x!1, y)")
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-all-but
(-2 1 -7))
(("2"
(expand
"bounded?")
(("2"
(skosimp)
(("2"
(split)
(("1"
(expand
"bounded_above?")
(("1"
(inst
+
"c!1")
(("1"
(skolem
+
"n!1")
(("1"
(inst
-
"n!1")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"bounded_below?")
(("2"
(inst
+
"-c!1")
(("2"
(skolem
+
"n!1")
(("2"
(inst
-
"n!1")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but
(1 -2))
(("2"
(expand
"ae_increasing?")
(("2"
(inst
+
"emptyset")
(("2"
(skosimp)
(("2"
(expand
"pointwise_increasing?")
(("2"
(inst
-
"x!1")
(("2"
(expand
"increasing?")
(("2"
(propax)
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.130 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.
|
