|
(fubini_tonelli_scaf
(product_measure_contraction_TCC1 0
(product_measure_contraction_TCC1-1 nil 3459570741
("" (skosimp)
(("" (expand "measurable_set?")
(("" (rewrite "cross_product_is_sigma_times") nil nil)) nil))
nil)
((measurable_set? const-decl "bool" measure_space_def nil)
(S2 formal-const-decl "sigma_algebra[T2]" fubini_tonelli_scaf nil)
(S1 formal-const-decl "sigma_algebra[T1]" fubini_tonelli_scaf nil)
(sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
(sigma_algebra? const-decl "bool" subset_algebra_def nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T2 formal-type-decl nil fubini_tonelli_scaf nil)
(T1 formal-type-decl nil fubini_tonelli_scaf nil)
(cross_product_is_sigma_times formula-decl nil product_sigma nil))
nil))
(product_measure_contraction_TCC2 0
(product_measure_contraction_TCC2-1 nil 3459570741
("" (skosimp)
(("" (expand "measurable_set?") (("" (propax) nil nil)) nil)) nil)
((measurable_set? const-decl "bool" measure_space_def nil)) nil))
(product_measure_contraction_TCC3 0
(product_measure_contraction_TCC3-1 nil 3459570741
("" (skosimp)
(("" (expand "measurable_set?") (("" (propax) nil nil)) nil)) nil)
((measurable_set? const-decl "bool" measure_space_def nil)) nil))
(product_measure_contraction 0
(product_measure_contraction-1 nil 3460776966
("" (skosimp)
(("" (lemma "cross_product_is_sigma_times" ("X" "X!1" "Y" "Y!1"))
((""
(lemma "measurable_intersection"
("a" "cross_product(X!1, Y!1)" "b" "E!1"))
(("1" (expand "contraction" 1 1)
(("1"
(name "F"
"lambda j: fm_contraction[T2, S2](nu, A_of(nu)(j)) o
x_section(intersection
(cross_product(X!1, Y!1),
E!1))")
(("1" (case "forall j,x: F(j)(x)>=0")
(("1"
(name "MU" "lambda i: fm_contraction[T1, S1]
(mu, A_of(mu)(i))")
(("1"
(case "forall (E:(S1)): x_eq(mu(E),
x_sum(LAMBDA i: to_measure(MU(i))(E)))")
(("1"
(case "forall i,j: integrable?[T1,S1,to_measure(MU(i))](F(j))")
(("1"
(case "forall x: measurable_set?(x_section(intersection(cross_product(X!1, Y!1), E!1),x))")
(("1"
(name "EE"
"intersection(cross_product(X!1, Y!1),
E!1)")
(("1" (replace -1)
(("1"
(case "forall x: x_eq(x_sum(lambda j: F(j)(x)),nu(x_section(EE,x)))")
(("1" (hide -6 -8)
(("1"
(case
"forall x: measurable_set?(x_section(E!1,x))")
(("1"
(name
"G"
"lambda j: (fm_contraction[T2, S2]
(contraction(nu, Y!1),
A_of(contraction(nu, Y!1))(j))
o x_section(E!1))")
(("1"
(case "forall j,x: G(j)(x)>=0")
(("1"
(name
"NU"
"lambda i: fm_contraction[T1, S1]
(contraction(mu, X!1),
A_of
(contraction(mu, X!1))(i))")
(("1"
(case
"forall i,j: integrable?[T1,S1,to_measure(NU(i))](G(j))")
(("1"
(hide -2 -4)
(("1"
(case
"FORALL (E: (S1)): x_eq(contraction(mu, X!1)(E), x_sum(LAMBDA i: to_measure(NU(i))(E)))")
(("1"
(case
"FORALL x: x_eq(x_sum(LAMBDA j: G(j)(x)), contraction(nu, Y!1)(x_section(E!1, x)))")
(("1"
(case
"forall x: X!1(x)=> x_eq(contraction(nu, Y!1)(x_section(E!1, x)), nu(x_section(EE, x)))")
(("1"
(case
"x_eq(x_sum(LAMBDA i:
x_sum(LAMBDA j:
(TRUE,
integral
[T1, S1,
to_measure(MU(i))]
(F(j))))),
x_sum(LAMBDA i:
x_sum(LAMBDA j:
(TRUE,
integral
[T1, S1,
to_measure(NU(i))]
(G(j))))))")
(("1"
(expand "m_times")
(("1"
(expand
"to_measure"
1)
(("1"
(expand
"product_measure_approx")
(("1"
(expand
"fm_times")
(("1"
(lemma
"x_sum_eq"
("S"
"LAMBDA i:
x_sum(LAMBDA j:
(TRUE,
integral[T1, S1, to_measure(MU(i))](F(j))))"
"T"
"LAMBDA i:
x_sum(LAMBDA j:
(TRUE,
integral
[T1, S1,
to_measure(fm_contraction[T1, S1]
(mu, A_of(mu)(i)))]
(fm_contraction[T2, S2](nu, A_of(nu)(j)) o
x_section(EE))))"))
(("1"
(split
-1)
(("1"
(lemma
"x_sum_eq"
("S"
"LAMBDA i:
x_sum(LAMBDA j:
(TRUE,
integral
[T1, S1,
to_measure(fm_contraction[T1, S1]
(contraction(mu, X!1),
A_of
(contraction(mu, X!1))(i)))]
(fm_contraction[T2, S2]
(contraction(nu, Y!1),
A_of(contraction(nu, Y!1))(j))
o x_section(E!1))))"
"T"
"LAMBDA i:
x_sum(LAMBDA j:
(TRUE,
integral[T1, S1, to_measure(NU(i))](G(j))))"))
(("1"
(split
-1)
(("1"
(hide-all-but
(-1
-2
-3
1))
(("1"
(expand
"x_eq")
(("1"
(flatten)
(("1"
(assert)
(("1"
(flatten)
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide
2
-1
-2)
(("2"
(assert)
(("2"
(skolem
+
"i!1")
(("2"
(lemma
"x_sum_eq"
("S"
"LAMBDA j:
(TRUE,
integral
[T1, S1,
to_measure(fm_contraction[T1, S1]
(contraction(mu, X!1),
A_of(contraction(mu, X!1))(i!1)))]
(fm_contraction[T2, S2]
(contraction(nu, Y!1),
A_of(contraction(nu, Y!1))(j))
o x_section(E!1)))"
"T"
"LAMBDA j:
(TRUE, integral[T1, S1, to_measure(NU(i!1))](G(j)))"))
(("1"
(split)
(("1"
(propax)
nil
nil)
("2"
(hide
2)
(("2"
(assert)
(("2"
(skolem
+
"j!1")
(("2"
(expand
"x_eq"
1)
(("2"
(inst
-4
"i!1"
"j!1")
(("2"
(lemma
"measure_eq_integral[T1,S1]"
("mu"
"to_measure(fm_contraction[T1, S1]
(contraction(mu, X!1),
A_of(contraction(mu, X!1))(i!1)))"
"nu"
"to_measure(NU(i!1))"
"f"
"G(j!1)"))
(("2"
(assert)
(("2"
(expand
"G")
(("2"
(assert)
(("2"
(hide-all-but
(1
-6
-8
-9
-13))
(("2"
(skosimp)
(("2"
(expand
"to_measure")
(("2"
(expand
"x_eq")
(("2"
(expand
"NU")
(("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
-4
"i!1"
"j!1")
(("2"
(inst
-5
"j!1"
"_")
(("2"
(lemma
"integral_nonneg[T1, S1, to_measure[T1, S1](NU(i!1))]"
("f"
"G(j!1)"))
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("3"
(skosimp)
(("3"
(inst
-4
"i!1"
"j!1")
nil
nil))
nil)
("4"
(hide
2)
(("4"
(skosimp)
(("4"
(inst
-4
"i!1"
"j!1")
(("4"
(inst
-5
"j!1"
"_")
(("4"
(lemma
"integral_nonneg[T1, S1, to_measure(NU(i!1))]"
("f"
"G(j!1)"))
(("1"
(replace
-6)
(("1"
(lemma
"measure_eq_integral[T1,S1]"
("mu"
"to_measure[T1, S1]
(fm_contraction[T1, S1]
(contraction[T1, S1](mu, X!1),
A_of[T1, S1](contraction[T1, S1](mu, X!1))(i!1)))"
"nu"
"to_measure(NU(i!1))"
"f"
"G(j!1)"))
(("1"
(assert)
(("1"
(expand
"G"
-1
1)
(("1"
(hide-all-but
1)
(("1"
(skosimp)
(("1"
(expand
"to_measure")
(("1"
(expand
"NU")
(("1"
(expand
"x_eq")
(("1"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"measurable_set?")
(("2"
(rewrite
"A_of_def2")
nil
nil))
nil))
nil))
nil)
("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("5"
(expand
"measurable_set?")
(("5"
(rewrite
"A_of_def2")
nil
nil))
nil)
("6"
(skosimp)
(("6"
(inst
-4
"i!1"
"j!1")
(("6"
(hide
2)
(("6"
(lemma
"measure_eq_integrable?[T1,S1]"
("mu"
"to_measure(NU(i!1))"
"nu"
"to_measure(fm_contraction[T1, S1]
(contraction(mu, X!1),
A_of(contraction(mu, X!1))(i!1)))"
"f"
"G(j!1)"))
(("1"
(split
-1)
(("1"
(assert)
(("1"
(expand
"G")
(("1"
(propax)
nil
nil))
nil))
nil)
("2"
(hide-all-but
1)
(("2"
(skosimp)
(("2"
(expand
"to_measure")
(("2"
(expand
"x_eq")
(("2"
(expand
"NU")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"measurable_set?")
(("2"
(rewrite
"A_of_def2")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide
-1
-2
2)
(("2"
(skosimp)
(("2"
(inst
-4
"i!1"
"j!1")
(("2"
(inst
-5
"j!1"
"_")
(("2"
(lemma
"integral_nonneg[T1, S1, to_measure(NU(i!1))]"
("f"
"G(j!1)"))
(("1"
(replace
-6)
(("1"
(lemma
"measure_eq_integral[T1,S1]"
("mu"
"to_measure[T1, S1]
(fm_contraction[T1, S1]
(contraction[T1, S1](mu, X!1),
A_of[T1, S1](contraction[T1, S1](mu, X!1))(i!1)))"
"nu"
"to_measure(NU(i!1))"
"f"
"G(j!1)"))
(("1"
(split
-1)
(("1"
(expand
"G"
-1
1)
(("1"
(assert)
nil
nil))
nil)
("2"
(hide-all-but
1)
(("2"
(skosimp)
(("2"
(expand
"to_measure")
(("2"
(expand
"x_eq")
(("2"
(expand
"NU")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("3"
(flatten)
nil
nil))
nil)
("2"
(expand
"measurable_set?")
(("2"
(rewrite
"A_of_def2")
nil
nil))
nil)
("3"
(expand
"measurable_set?")
(("3"
(propax)
nil
nil))
nil))
nil))
nil)
("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("3"
(expand
"measurable_set?")
(("3"
(propax)
nil
nil))
nil)
("4"
(hide
-1
-2
2)
(("4"
(skosimp)
(("4"
(inst
-4
"i!1"
"j!1")
(("4"
(lemma
"measure_eq_integrable?[T1,S1]"
("mu"
"to_measure(fm_contraction[T1, S1]
(contraction(mu, X!1),
A_of(contraction(mu, X!1))(i!1)))"
"nu"
"to_measure(NU(i!1))"
"f"
"G(j!1)"))
(("1"
(assert)
(("1"
(expand
"G")
(("1"
(assert)
(("1"
(hide-all-but
1)
(("1"
(skosimp)
(("1"
(expand
"to_measure")
(("1"
(expand
"x_eq")
(("1"
(expand
"NU")
(("1"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"measurable_set?")
(("2"
(rewrite
"A_of_def2")
nil
nil))
nil)
("3"
(expand
"measurable_set?")
(("3"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("5"
(expand
"measurable_set?")
(("5"
(propax)
nil
nil))
nil))
nil)
("2"
(hide
2
-1)
(("2"
(assert)
(("2"
(skolem
+
"i!1")
(("2"
(lemma
"x_sum_eq"
("S"
"LAMBDA j:
(TRUE, integral[T1, S1, to_measure(MU(i!1))](F(j)))"
"T"
"LAMBDA j:
(TRUE,
integral
[T1, S1,
to_measure(fm_contraction[T1, S1]
(mu, A_of(mu)(i!1)))]
(fm_contraction[T2, S2](nu, A_of(nu)(j)) o
x_section(EE)))"))
(("1"
(assert)
(("1"
(skolem
+
"j!1")
(("1"
(hide
-1
2)
(("1"
(expand
"x_eq"
1)
(("1"
(lemma
"measure_eq_integral[T1,S1]"
("mu"
"to_measure(fm_contraction[T1, S1](mu, A_of(mu)(i!1)))"
"nu"
"to_measure(MU(i!1))"
"f"
"F(j!1)"))
(("1"
(inst
-10
"i!1"
"j!1")
(("1"
(assert)
(("1"
(expand
"F"
-1
1)
(("1"
(hide-all-but
1)
(("1"
(skosimp)
(("1"
(expand
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.125 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.
|
