|
(product_measure
(product_measure_approx_TCC1 0
(product_measure_approx_TCC1-1 nil 3456295627
("" (skosimp)
(("" (typepred "A_of[T1, S1](mu!1)(i!1)")
(("" (expand "measurable_set?")
(("" (expand "A_of")
(("" (lemma "A_of_TCC1[T1,S1]" ("f" "mu!1"))
((""
(name-replace "XX"
"{X: disjoint_indexed_measurable[T1, S1] |
IUnion(X) = fullset[T1] AND (FORALL i: mu!1(X(i))`1)}")
(("" (lemma "choose_member" ("a" "XX"))
(("" (expand "nonempty?")
(("" (name-replace "CC" "choose(XX)")
(("" (expand "XX")
(("" (assert)
(("" (flatten) (("" (inst - "i!1") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((A_of const-decl "disjoint_indexed_measurable" measure_def nil)
(disjoint_indexed_measurable nonempty-type-eq-decl nil
generalized_measure_def nil)
(disjoint_indexed_measurable? const-decl "bool"
generalized_measure_def nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(sigma_finite_measure nonempty-type-eq-decl nil measure_def nil)
(sigma_finite_measure? const-decl "bool" measure_def nil)
(extended_nnreal nonempty-type-eq-decl nil extended_nnreal
"extended_nnreal/")
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(S1 formal-const-decl "sigma_algebra[T1]" product_measure 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)
(T1 formal-type-decl nil product_measure nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(sigma_algebra_IUnion_rew application-judgement "(S)"
product_measure nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(set type-eq-decl nil sets nil)
(IUnion const-decl "set[T]" indexed_sets nil)
(fullset const-decl "set" sets nil)
(nonempty? const-decl "bool" sets nil)
(XX skolem-const-decl
"[disjoint_indexed_measurable[T1, S1] -> boolean]" product_measure
nil)
(member const-decl "bool" sets nil)
(choose const-decl "(p)" sets nil)
(choose_member formula-decl nil sets_lemmas nil)
(A_of_TCC1 subtype-tcc nil measure_def nil)
(measurable_set? const-decl "bool" measure_space_def nil))
nil))
(product_measure_approx_TCC2 0
(product_measure_approx_TCC2-1 nil 3456295627
("" (skosimp)
(("" (typepred "A_of[T2, S2](nu!1)(j!1)")
(("" (expand "measurable_set?")
(("" (lemma "A_of_TCC1[T2, S2]" ("f" "nu!1"))
(("" (expand "A_of")
((""
(name "XX" "{X: disjoint_indexed_measurable[T2, S2] |
IUnion(X) = fullset[T2] AND (FORALL i: nu!1(X(i))`1)}")
(("" (replace -1)
(("" (lemma "choose_member" ("a" "XX"))
(("" (split)
(("1" (name-replace "CC" "choose(XX)")
(("1" (expand "XX")
(("1" (expand "member")
(("1" (flatten)
(("1" (inst - "j!1") nil nil)) nil))
nil))
nil))
nil)
("2" (expand "nonempty?") (("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((A_of const-decl "disjoint_indexed_measurable" measure_def nil)
(disjoint_indexed_measurable nonempty-type-eq-decl nil
generalized_measure_def nil)
(disjoint_indexed_measurable? const-decl "bool"
generalized_measure_def nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(sigma_finite_measure nonempty-type-eq-decl nil measure_def nil)
(sigma_finite_measure? const-decl "bool" measure_def nil)
(extended_nnreal nonempty-type-eq-decl nil extended_nnreal
"extended_nnreal/")
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(S2 formal-const-decl "sigma_algebra[T2]" product_measure 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)
(T2 formal-type-decl nil product_measure nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(A_of_TCC1 subtype-tcc nil measure_def nil)
(fullset const-decl "set" sets nil)
(IUnion const-decl "set[T]" indexed_sets nil)
(set type-eq-decl nil sets nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(sigma_algebra_IUnion_rew application-judgement "(S)"
product_measure nil)
(choose_member formula-decl nil sets_lemmas nil)
(choose const-decl "(p)" sets nil)
(nonempty? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(XX skolem-const-decl
"[disjoint_indexed_measurable[T2, S2] -> boolean]" product_measure
nil)
(measurable_set? const-decl "bool" measure_space_def nil))
nil))
(m_times_TCC1 0
(m_times_TCC1-1 nil 3456295627
("" (skosimp)
((""
(lemma "x_sum_measure"
("F" "LAMBDA i: lambda M:
x_sum(LAMBDA j:
to_measure[[T1, T2], sigma_times(S1, S2)]
(product_measure_approx(mu!1, nu!1)(i, j))(M))
"))
(("1" (assert)
(("1" (expand "sigma_finite_measure?")
(("1" (hide -1)
(("1" (expand "product_measure_approx")
(("1" (typepred "A_of(nu!1)")
(("1" (typepred "A_of(mu!1)")
(("1" (name "X!1" "A_of(mu!1)")
(("1" (name "Y!1" "A_of(nu!1)")
(("1" (replace -1)
(("1" (replace -2)
(("1" (expand "disjoint_indexed_measurable?")
(("1"
(case "forall i,j: sigma_times(S1, S2)(cross_product(X!1(i),Y!1(j)))")
(("1"
(lemma "A_of_TCC1[T2,S2]" ("f" "nu!1"))
(("1"
(lemma
"A_of_TCC1[T1,S1]"
("f" "mu!1"))
(("1"
(expand "nonempty?")
(("1"
(expand "A_of")
(("1"
(lemma
"choose_member"
("a"
"{X: disjoint_indexed_measurable[T1, S1] |
IUnion[nat, T1](X) = fullset[T1] AND
(FORALL i: mu!1(X(i))`1)}"))
(("1"
(replace -4)
(("1"
(replace 1)
(("1"
(lemma
"choose_member"
("a"
"{X: disjoint_indexed_measurable[T2, S2] |
IUnion[nat, T2](X) = fullset[T2] AND
(FORALL i: nu!1(X(i))`1)}"))
(("1"
(replace -4)
(("1"
(replace 2)
(("1"
(hide -4 -5 1 2)
(("1"
(expand "member")
(("1"
(flatten)
(("1"
(expand
"measure_sigma_finite?")
(("1"
(name
"UU"
"lambda i,j: cross_product(X!1(i), Y!1(j))")
(("1"
(hide -1)
(("1"
(case
"FORALL i, j: sigma_times(S1, S2)(UU(i,j))")
(("1"
(hide
-6)
(("1"
(case
"disjoint?(single_index(UU))")
(("1"
(inst
+
"single_index(UU)")
(("1"
(split)
(("1"
(apply-extensionality
:hide?
t)
(("1"
(lemma
"extensionality_postulate"
("f"
"IUnion[nat, T2](Y!1)"
"g"
"fullset[T2]"))
(("1"
(lemma
"extensionality_postulate"
("f"
"IUnion[nat, T1](X!1)"
"g"
"fullset[T1]"))
(("1"
(flatten)
(("1"
(split
-2)
(("1"
(split
-4)
(("1"
(hide-all-but
(-1
-2
1))
(("1"
(expand
"fullset")
(("1"
(expand
"single_index")
(("1"
(expand
"IUnion")
(("1"
(inst
-
"x!2")
(("1"
(skolem
-
"j!1")
(("1"
(inst
-
"x!1")
(("1"
(skolem
-
"i!1")
(("1"
(inst
+
"double_index_n(i!1,j!1)")
(("1"
(lemma
"double_index_ij_n"
("i"
"i!1"
"j"
"j!1"))
(("1"
(flatten)
(("1"
(assert)
(("1"
(replace
-1)
(("1"
(replace
-2)
(("1"
(expand
"UU")
(("1"
(expand
"cross_product")
(("1"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(propax)
nil
nil))
nil)
("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skolem
+
"n!1")
(("2"
(expand
"single_index")
(("2"
(case
"forall i,j: to_measure[[T1, T2], sigma_times(S1, S2)]
(fm_times(fm_contraction[T1, S1](mu!1, X!1(i)),
fm_contraction[T2, S2](nu!1, Y!1(j))))
(UU(double_index_i(n!1), double_index_j(n!1))) = if i = double_index_i(n!1) & j = double_index_j(n!1) then (TRUE, mu!1(X!1(i))`2*nu!1(Y!1(j))`2) else (TRUE,0) endif")
(("1"
(case
"forall i: x_sum(LAMBDA j:
to_measure[[T1, T2], sigma_times(S1, S2)]
(fm_times(fm_contraction[T1, S1](mu!1, X!1(i)),
fm_contraction[T2, S2](nu!1, Y!1(j))))
(UU(double_index_i(n!1), double_index_j(n!1)))) = IF i = double_index_i(n!1)
THEN (TRUE, mu!1(X!1(i))`2 * nu!1(Y!1(double_index_j(n!1)))`2)
ELSE (TRUE, 0)
ENDIF")
(("1"
(case-replace
"(LAMBDA i:
x_sum(LAMBDA j:
to_measure[[T1, T2], sigma_times(S1, S2)]
(fm_times(fm_contraction[T1, S1](mu!1, X!1(i)),
fm_contraction[T2, S2](nu!1, Y!1(j))))
(UU(double_index_i(n!1), double_index_j(n!1)))))=lambda i: IF i = double_index_i(n!1)
THEN (TRUE, mu!1(X!1(i))`2 * nu!1(Y!1(double_index_j(n!1)))`2)
ELSE (TRUE, 0)
ENDIF")
(("1"
(hide
-1
-2)
(("1"
(expand
"x_sum")
(("1"
(case-replace
"(FORALL (i_1: nat):
IF i_1 = double_index_i(n!1) THEN TRUE ELSE TRUE ENDIF)")
(("1"
(prop)
(("1"
(lemma
"single_nz_series_conv"
("a"
"(LAMBDA (i_1: nat):
IF i_1 = double_index_i(n!1)
THEN mu!1(X!1(i_1))`2 *
nu!1(Y!1(double_index_j(n!1)))`2
ELSE 0
ENDIF)"
"n"
"double_index_i(n!1)"))
(("1"
(assert)
(("1"
(hide
2)
(("1"
(skosimp)
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(replace
1)
(("2"
(skosimp)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(apply-extensionality
:hide?
t)
(("1"
(expand
"measurable_set?")
(("1"
(propax)
nil
nil))
nil)
("2"
(expand
"measurable_set?")
(("2"
(propax)
nil
nil))
nil)
("3"
(inst
-4
"double_index_i(n!1)"
"double_index_j(n!1)")
nil
nil))
nil))
nil)
("2"
(hide
2)
(("2"
(skosimp)
(("2"
(inst
-
"i!1"
"_")
(("2"
(hide
-4
-6
-8
-9)
(("2"
(case-replace
"(LAMBDA j:
to_measure[[T1, T2], sigma_times(S1, S2)]
(fm_times(fm_contraction[T1, S1](mu!1, X!1(i!1)),
fm_contraction[T2, S2](nu!1, Y!1(j))))
(UU(double_index_i(n!1), double_index_j(n!1))))=lambda j: IF i!1 = double_index_i(n!1) & j = double_index_j(n!1)
THEN (TRUE, mu!1(X!1(i!1))`2 * nu!1(Y!1(j))`2)
ELSE (TRUE, 0)
ENDIF")
(("1"
(hide
-1
-2)
(("1"
(hide
-1)
(("1"
(case-replace
"i!1 = double_index_i(n!1)")
(("1"
(replace
-1
*
rl)
(("1"
(hide
-1)
(("1"
(expand
"x_sum")
(("1"
(lift-if)
(("1"
(lift-if
1)
(("1"
(assert)
(("1"
(lemma
"single_nz_series_conv"
("a"
"LAMBDA i:
IF i = double_index_j(n!1)
THEN mu!1(X!1(i!1))`2 * nu!1(Y!1(i))`2
ELSE 0
ENDIF"
"n"
"double_index_j(n!1)"))
(("1"
(lemma
"single_nz_series_limit"
("a"
"LAMBDA i:
IF i = double_index_j(n!1)
THEN mu!1(X!1(i!1))`2 * nu!1(Y!1(i))`2
ELSE 0
ENDIF"
"n"
"double_index_j(n!1)"))
(("1"
(case-replace
"(FORALL (m:nat):
double_index_j(n!1) /= m =>
(LAMBDA i:
IF i = double_index_j(n!1)
THEN mu!1(X!1(i!1))`2 * nu!1(Y!1(i))`2
ELSE 0
ENDIF)
(m)
= 0)")
(("1"
(assert)
nil
nil)
("2"
(hide
2
-1
-2)
(("2"
(skosimp)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(expand
"x_sum")
(("2"
(rewrite
"zero_series_conv")
(("2"
(rewrite
"zero_series_limit")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(apply-extensionality
:hide?
t)
(("1"
(expand
"measurable_set?")
(("1"
(propax)
nil
nil))
nil)
("2"
(expand
"measurable_set?")
(("2"
(inst
-5
"i!1")
nil
nil))
nil)
("3"
(inst
-3
"double_index_i(n!1)"
"double_index_j(n!1)")
nil
nil))
nil)
("3"
(expand
"measurable_set?")
(("3"
(inst
-5
"i!1")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide
2)
(("2"
(skosimp)
(("2"
(expand
"to_measure")
(("2"
(expand
"fm_times")
(("2"
(lift-if)
(("2"
(assert)
(("2"
(expand
"UU")
(("2"
(lemma
"rectangle_measure1"
("M"
"cross_product(X!1(double_index_i(n!1)),
Y!1(double_index_j(n!1)))"
"X"
"X!1(double_index_i(n!1))"
"Y"
"Y!1(double_index_j(n!1))"
"mu"
"fm_contraction[T1, S1](mu!1, X!1(i!1))"
"nu"
"fm_contraction[T2, S2](nu!1, Y!1(j!1))"))
(("1"
(assert)
(("1"
(replace
-1)
(("1"
(hide
-1)
(("1"
(expand
"fm_contraction")
(("1"
(case-replace
"double_index_i(n!1)=i!1")
(("1"
(rewrite
"intersection_idempotent")
(("1"
(case-replace
"double_index_j(n!1)=j!1")
(("1"
(rewrite
"intersection_idempotent")
nil
nil)
("2"
(assert)
(("2"
(expand
"disjoint?"
-9)
(("2"
(inst
-9
"j!1"
"double_index_j(n!1)")
(("2"
(assert)
(("2"
(expand
"disjoint?")
(("2"
(rewrite
"emptyset_is_empty?")
(("2"
(replace
-9)
(("2"
(typepred
"nu!1")
(("2"
(expand
"sigma_finite_measure?")
(("2"
(expand
"measure?")
(("2"
(flatten)
(("2"
(expand
"measure_empty?")
(("2"
(replace
-1)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.83 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
