Quelle product_measure.prf
Sprache: Lisp
(product_measurenil 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" ))"" "XX" "{X: disjoint_indexed_measurable[T1, S1] | 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 )"disjoint_indexed_measurable" measure_def nil )nil nil )"bool" nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil measure_def nil )"bool" measure_def nil )nil extended_nnreal"extended_nnreal/" )nil real_types nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )"sigma_algebra[T1]" product_measure nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )nil product_measure nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"(S)" nil )"[T, T -> boolean]" equalities nil )AND const-decl "[bool, bool -> bool]" booleans nil )set type-eq-decl nil sets nil )"set[T]" indexed_sets nil )"set" sets nil )"bool" sets nil )"[disjoint_indexed_measurable[T1, S1] -> boolean]" product_measurenil )"bool" sets nil )"(p)" sets nil )nil sets_lemmas nil )nil measure_def nil )"bool" measure_space_def nil ))nil ))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" )"" "XX" "{X: disjoint_indexed_measurable[T2, S2] | 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 )"disjoint_indexed_measurable" measure_def nil )nil nil )"bool" nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil measure_def nil )"bool" measure_def nil )nil extended_nnreal"extended_nnreal/" )nil real_types nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )"sigma_algebra[T2]" product_measure nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )nil product_measure nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil measure_def nil )"set" sets nil )"set[T]" indexed_sets nil )set type-eq-decl nil sets nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"(S)" nil )nil sets_lemmas nil )"(p)" sets nil )"bool" sets nil )"bool" sets nil )"[disjoint_indexed_measurable[T2, S2] -> boolean]" product_measurenil )"bool" measure_space_def nil ))nil ))nil 3456295627"" (skosimp)"" "x_sum_measure" "F" "LAMBDA i: lambda M: LAMBDA j:")) "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" "A_of_TCC1[T2,S2]" ("f" "nu!1" ))"1" "A_of_TCC1[T1,S1]" "f" "mu!1" ))"1" expand "nonempty?" )"1" expand "A_of" )"1" "choose_member" "a" "{X: disjoint_indexed_measurable[T1, S1] | AND ")) "1" replace -4)"1" replace 1)"1" "choose_member" "a" "{X: disjoint_indexed_measurable[T2, S2] | AND ")) "1" replace -4)"1" replace 2)"1" "1" expand "member" )"1" "1" expand "measure_sigma_finite?" )"1" "UU" "lambda i,j: cross_product(X!1(i), Y!1(j))" )"1" "1" case "FORALL i, j: sigma_times(S1, S2)(UU(i,j))" )"1" "1" case "disjoint?(single_index(UU))" )"1" "single_index(UU)" )"1" "1" "1" "extensionality_postulate" "f" "IUnion[nat, T2](Y!1)" "g" "fullset[T2]" ))"1" "extensionality_postulate" "f" "IUnion[nat, T1](X!1)" "g" "fullset[T1]" ))"1" "1" "1" "1" "1" expand "fullset" )"1" expand "single_index" )"1" expand "IUnion" )"1" "x!2" )"1" "j!1" )"1" "x!1" )"1" "i!1" )"1" "double_index_n(i!1,j!1)" )"1" "double_index_ij_n" "i" "i!1" "j" "j!1" ))"1" "1" assert )"1" replace "1" replace "1" expand "UU" )"1" expand "cross_product" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "n!1" )"2" expand "single_index" )"2" case "forall i,j: to_measure[[T1, T2], sigma_times(S1, S2)] 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: IF i = double_index_i(n!1)") "1" "(LAMBDA i: LAMBDA j:lambda i: IF i = double_index_i(n!1)") "1" "1" expand "x_sum" )"1" "(FORALL (i_1: nat): IF i_1 = double_index_i(n!1) THEN TRUE ELSE TRUE ENDIF)") "1" "1" "single_nz_series_conv" "a" "(LAMBDA (i_1: nat): IF i_1 = double_index_i(n!1)" "n" "double_index_i(n!1)" ))"1" assert )"1" "1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" nil nil ))nil ))nil ))nil ))nil )"2" "1" expand "measurable_set?" )"1" nil nil ))nil )"2" expand "measurable_set?" )"2" nil nil ))nil )"3" "double_index_i(n!1)" "double_index_j(n!1)" )nil nil ))nil ))nil )"2" "2" "2" "i!1" "_" )"2" "2" "(LAMBDA j: lambda j: IF i!1 = double_index_i(n!1) & j = double_index_j(n!1)") "1" "1" "1" "i!1 = double_index_i(n!1)" )"1" replace "1" "1" expand "x_sum" )"1" "1" "1" assert )"1" "single_nz_series_conv" "a" "LAMBDA i: IF i = double_index_j(n!1)" "n" "double_index_j(n!1)" ))"1" "single_nz_series_limit" "a" "LAMBDA i: IF i = double_index_j(n!1)" "n" "double_index_j(n!1)" ))"1" "(FORALL (m:nat): LAMBDA i:IF i = double_index_j(n!1)") "1" assert )nil nil )"2" "2" "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" "1" expand "measurable_set?" )"1" nil nil ))nil )"2" expand "measurable_set?" )"2" "i!1" )nil nil ))nil )"3" "double_index_i(n!1)" "double_index_j(n!1)" )nil nil ))nil )"3" expand "measurable_set?" )"3" "i!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "to_measure" )"2" expand "fm_times" )"2" "2" assert )"2" expand "UU" )"2" "rectangle_measure1" "M" "cross_product(X!1(double_index_i(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" expand "fm_contraction" )"1" "double_index_i(n!1)=i!1" )"1" rewrite "intersection_idempotent" )"1" "double_index_j(n!1)=j!1" )"1" rewrite "intersection_idempotent" )nil nil )"2" assert )"2" expand "disjoint?" "2" "j!1" "double_index_j(n!1)" )"2" assert )"2" expand "disjoint?" )"2" rewrite "emptyset_is_empty?" )"2" replace "2" "nu!1" )"2" expand "sigma_finite_measure?" )"2" expand "measure?" )"2" "2" expand "measure_empty?" )"2" replace "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" expand "disjoint?" "2" "i!1" "double_index_i(n!1)" )"2" assert )"2" expand "disjoint?" )"2" rewrite "emptyset_is_empty?" )"2" replace "2" "mu!1" )"2" expand "sigma_finite_measure?" )"2" expand "measure?" )"2" "2" expand "measure_empty?" )"2" replace "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "measurable_set?" )"2" "j!1" )nil nil ))nil )"3" expand "measurable_set?" )"3" "i!1" )nil nil ))nil )"4" "double_index_i(n!1)" "double_index_j(n!1)" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" expand "measurable_set?" )"3" "j!1" )nil nil ))nil ))nil )"4" expand "measurable_set?" )"4" nil nil ))nil )"5" "double_index_i(n!1)" "double_index_j(n!1)" )nil nil ))nil ))nil ))nil ))nil )"2" assert )"2" "1" "n!1" )"1" expand "single_index" )"1" "double_index_i(n!1)" "double_index_j(n!1)" )nil nil ))nil ))nil )"2" expand "disjoint_indexed_measurable?" )"2" nil nil ))nil ))nil ))nil ))nil )"2" "2" expand "disjoint?" )"2" "2" expand "single_index" )"2" expand "UU" )"2" "double_index_i(j!1)=double_index_i(i!1)" )"1" "double_index_n_ij" "n" "i!1" ))"1" "double_index_n_ij" "n" "j!1" ))"1" replace "1" "double_index_j(j!1)=double_index_j(i!1)" )"1" assert )nil nil )"2" "double_index_j(i!1)" "double_index_j(j!1)" )"2" assert )"2" "2" expand "cross_product" )"2" expand "disjoint?" )"2" expand "intersection" )"2" expand "empty?" )"2" expand "member" )"2" "2" "x!1`2" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "double_index_i(i!1)" "double_index_i(j!1)" )"2" assert )"2" "2" expand "cross_product" )"2" expand "disjoint?" )"2" expand "intersection" )"2" expand "empty?" )"2" expand "member" )"2" "2" "x!1`1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "i!1" "j!1" )"2" expand "UU" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "sigma_times" )"2" "generated_sigma_algebra_subset1" "X" "(extend ")) "2" expand "subset?" )"2" "cross_product(X!1(i!1), Y!1(j!1))" )"2" assert )"2" "2" expand "fullset" )"2" expand "extend" )"2" "2" expand "measurable_rectangle?" )"2" "X!1(i!1)" "Y!1(j!1)" )"2" assert )"2" expand "cross_product" )"2" 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 2)"2" (skosimp)"2" "x_sum_measure" "F" "lambda j: to_measure[[T1, T2], sigma_times[T1, T2](S1, S2)] ")) "2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"sigma_algebra[T2]" product_measure nil )"sigma_algebra[T1]" product_measure nil )"sigma_algebra[[T1, T2]]" product_sigma_defnil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )nil booleans nil )nil booleans nil )nil product_measure nil )nil product_measure nil )"finite_measure[[T1, T2], sigma_times(S1, S2)]" product_measurenil )nil measure_def nil )"bool" measure_def nil )"measure_type" generalized_measure_def nil )nil generalized_measure_defnil )"bool" generalized_measure_def nil )"extended_nnreal" extended_nnreal"extended_nnreal/" )nil sequences nil )nil generalized_measure_defnil )"bool" generalized_measure_def nil )nil extended_nnreal"extended_nnreal/" )nil real_types nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil generalized_measure_def nil )set type-eq-decl nil sets nil )"set[[T1, T2]]" cross_product"topology/" )"(S)" nil )"bool" sets nil )"bool" measure_def nil )nil code_product"extended_nnreal/" )"bool" sets nil )"[[nat, nat] -> set[[T1, T2]]]" nil )"nnreal" nil )"finite_measure[[T1, T2], sigma_times(S1, S2)]" nil )"bool" measure_space_def nil )nil measure_space_def nil )"finite_measure" measure_contractionnil )"nat" code_product "extended_nnreal/" )"nat" code_product "extended_nnreal/" )nil number_fields nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"bool" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )nil series "series/" )nil series "series/" )"boolean" notequal nil )"[bool, bool -> bool]" booleans nil )nil series_lems "series/" )"nat" product_measure nil )nil series_lems "series/" )"nat" product_measure nil )"disjoint_indexed_measurable[T1, S1]" nil )"sigma_finite_measure[T1, S1]" nil )"disjoint_indexed_measurable[T2, S2]" nil )"sigma_finite_measure[T2, S2]" nil )nil product_finite_measure nil )"(S)" nil )"(S)" product_measure nil )"measurable_set" nil )nil sets_lemmas nil )"(S)" nil )"bool" sets nil )"bool" generalized_measure_def nil )"finite_set" finite_sets nil )"finite_set[T]" countable_props"sets_aux/" )"finite_set[T]" sigma_countable"sigma_set/" )"finite_set[T]" countable_setofsets"sets_aux/" )"(S)" product_measure nil )"measurable_set" nil )nil sets_lemmas nil )"set" sets nil )"(S)" product_measure nil )"measurable_set[T, S]" nil )"(S)" product_measure nil )"measurable_set[T, S]" nil )"(S)" product_measure nil )"measurable_set[T, S]" nil )"nat" code_product "extended_nnreal/" )nil code_product"extended_nnreal/" )nil functions nil )"[nat -> T]" double_index"extended_nnreal/" )"bool" indexed_sets_aux "sets_aux/" )"set" sets nil )"set[T]" indexed_sets nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil sets_lemmas nil )"(S)" nil )"bool" sets nil )nil measure_def nil )nil nil )"bool" product_sigma_def nil )nil product_sigma_defnil )"bool" booleans nil )"R" extend nil )"bool" sets nil )"[T, T -> boolean]" equalities nil )"disjoint_indexed_measurable" measure_def nil )nil nil )"bool" nil )NOT const-decl "[bool -> bool]" booleans nil ))nil ))nil 3460264253"" (skosimp)"" (expand "m_times" ) (("" (rewrite "double_x_sum_eq" ) nil nil ))nil ))nil )"sigma_finite_measure[[T1, T2], sigma_times(S1, S2)]" nil )"finite_measure[[T1, T2], sigma_times(S1, S2)]" product_measurenil )nil measure_def nil )"bool" measure_def nil )"measure_type" generalized_measure_def nil )nil generalized_measure_defnil )"bool" generalized_measure_def nil )nil generalized_measure_defnil )"bool" generalized_measure_def nil )"sigma_algebra[T2]" product_measure nil )"sigma_algebra[T1]" product_measure nil )"sigma_algebra[[T1, T2]]" product_sigma_defnil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )nil product_measure nil )nil product_measure nil )nil extended_nnreal"extended_nnreal/" )nil real_types nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil extended_nnreal"extended_nnreal/" ))nil 3457153332"" (skosimp)"" (expand "sigma_times" )"" "generated_sigma_algebra_subset1" "X" "(extend ")) "" (expand "subset?" )"" (expand "member" )"" (inst - "cross_product[T1, T2](X!1, Y!1)" )"" (assert )"" (hide 2)"" (expand "fullset" )"" (expand "extend" )"" (prop)"" (expand "measurable_rectangle?" )"" (inst + "X!1" "Y!1" )"" (assert )"" expand "cross_product" )"" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"sigma_algebra[[T1, T2]]" product_sigma_defnil )"bool" sets nil )"set[[T1, T2]]" cross_product"topology/" )"bool" sets nil )nil nil )nil booleans nil )nil booleans nil )nil defined_types nil )nil sets nil )set type-eq-decl nil sets nil )"bool" subset_algebra_def nil )nil subset_algebra_def nil )"bool" product_sigma_def nil )"sigma_algebra[T1]" product_measure nil )"sigma_algebra[T2]" product_measure nil )nil product_sigma_defnil )"bool" booleans nil )"R" extend nil )"set" sets nil )nil product_measure nil )nil product_measure nil ))nil ))nil 3457153506"" (skosimp)"" (expand "m_times" )"" (expand "product_measure_approx" )"" "FF" "LAMBDA i,j:to_measure(fm_times ") "1" case "x_eq(x_sum(LAMBDA i: LAMBDA j: FF(i,j)(cross_product(X!1, Y!1)))),x_times(mu!1(X!1), nu!1(Y!1)))") "1" (expand "FF" ) (("1" (propax) nil nil )) nil )"2" (hide 2)"2" case "forall i,j: x_eq(FF(i, j)(cross_product(X!1, Y!1)),fm_contraction[T1, S1](mu!1, A_of(mu!1)(i))(X!1)*fm_contraction[T2, S2](nu!1, A_of(nu!1)(j))(Y!1))" )"1" (hide -2)"1" "x_sum_eq" "S" "LAMBDA i: LAMBDA j: FF(i, j)(cross_product(X!1, Y!1)))" "T" "LAMBDA i:x_times(fm_contraction[T1, S1](mu!1, A_of(mu!1)(i))(X!1),nu!1(Y!1))" ))"1" (split -1)"1" "LHS" "x_sum(LAMBDA i: LAMBDA j: FF(i, j)(cross_product(X!1, Y!1))))") "1" "sigma_finite_contraction_def[T1,S1]" "nu" "mu!1" "E" "X!1" ))"1" "x_times_sum" "x" "nu!1(Y!1)" "S" "LAMBDA i: " "T" "LAMBDA i: ")) "1" (split -1)"1" "DRL1" "x_sum(LAMBDA i: ") "1" "DRL2" "x_sum(LAMBDA i: ") "1" "1" expand "x_times" )"1" expand "x_eq" )"1" "1" "LHS`1" )"1" assert )"1" "mu!1(X!1)`1" )"1" assert )"1" "nu!1(Y!1)`1" )"1" assert )nil nil )"2" assert )"2" "1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )"2" "nu!1(Y!1)`1" )"1" assert )"1" "1" assert )nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )"2" "nu!1(Y!1)`1" )"1" assert )"1" "DRL2`1" )"1" assert )nil nil ))nil ))nil )"2" assert )"2" "DRL2`1" )"1" assert )"1" "1" assert )nil nil )"2" assert )nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "x_times" )"2" expand "x_times" )"2" expand "x_eq" )"2" "nu!1(Y!1)`1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "measurable_set?" )"2" (propax) nil nil )) nil ))nil ))nil )"2" (hide 2)"2" (skosimp)"2" (expand "x_times" )"2" "x_sum_eq" "S" "LAMBDA j: FF(i!1, j)(cross_product(X!1, Y!1))" "T" "lambda j: (TRUE,fm_contraction[T1, S1](mu!1, A_of(mu!1)(i!1))(X!1) * ")) "2" "1" "LHS" "x_sum(LAMBDA j: FF(i!1, j)(cross_product(X!1, Y!1)))" )"1" "i!1" "_" )"1" "KX" "fm_contraction[T1, S1](mu!1, A_of(mu!1)(i!1))(X!1)" )"1" "x_times_sum" "S" "LAMBDA j:(TRUE,fm_contraction[T2, S2](nu!1, A_of(nu!1)(j))(Y!1))" "x" "(TRUE,KX)" "T" "LAMBDA j: ")) "1" "1" "DRL1" "x_sum(LAMBDA j: ") "1" "sigma_finite_contraction_def" "nu" "nu!1" "E" "Y!1" ))"1" "DRL2" "x_sum(LAMBDA i: ") "1" "1" expand "x_times" )"1" expand "x_eq" )"1" "1" assert )"1" "KX = 0" )"1" assert )nil nil )"2" assert )"2" "DRL2`1" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "measurable_set?" )"2" nil nil ))nil ))nil ))nil )"2" "2" "2" expand "x_times" )"2" expand "x_eq" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "j!1" )"2" "i!1" "j!1" )"2" assert )"2" expand "x_eq" )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -1 2)"2" (skosimp)"2" (expand "FF" )"2" (expand "to_measure" )"2" (expand "x_eq" )"2" "rectangle_measure1" "M" "cross_product(X!1, Y!1)" "X" "X!1" "Y" "Y!1" "mu" "fm_contraction[T1, S1](mu!1, A_of(mu!1)(i!1))" "nu" "fm_contraction[T2, S2](nu!1, A_of(nu!1)(j!1))" ))"2" (expand "fm_times" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide-all-but 1)"3" (rewrite "rectangle_measure_TCC1" ) nil nil )) nil ))nil )"2" (hide 2)"2" (skosimp)"2" (expand "measurable_set?" )"2" (expand "A_of" )"2" (lemma "A_of_TCC1[T2,S2]" ("f" "nu!1" ))"2" "choose_member" "a" "{X: disjoint_indexed_measurable[T2, S2] | AND (FORALL i: nu!1(X(i))`1)}")) "2" (split)"1" (expand "member" )"1" (flatten)"1" (inst - "j!1" ) nil nil )) nil ))nil )"2" (expand "nonempty?" )"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide 2)"3" (skosimp)"3" (expand "measurable_set?" )"3" (expand "A_of" )"3" (lemma "A_of_TCC1[T1,S1]" ("f" "mu!1" ))"3" "choose_member" "a" "{X: disjoint_indexed_measurable[T1, S1] | AND (FORALL i: mu!1(X(i))`1)}")) "3" (split)"1" (expand "member" )"1" (flatten)"1" (inst - "i!1" ) nil nil )) nil ))nil )"2" (expand "nonempty?" )"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"sigma_finite_measure[[T1, T2], sigma_times(S1, S2)]" nil )"disjoint_indexed_measurable" measure_def nil )nil nil )"bool" nil )nil measure_def nil )"bool" measure_def nil )"finite_measure" measure_contractionnil )nil measure_space_def nil )"bool" measure_space_def nil )set type-eq-decl nil sets nil )"finite_measure[[T1, T2], sigma_times(S1, S2)]" nil )"measure_type" generalized_measure_def nil )nil generalized_measure_defnil )"bool" generalized_measure_def nil )"[T, T -> boolean]" equalities nil )nil generalized_measure_defnil )"bool" generalized_measure_def nil )nil extended_nnreal"extended_nnreal/" )nil real_types nil )"sigma_algebra[T2]" product_measure nil )"sigma_algebra[T1]" product_measure nil )"sigma_algebra[[T1, T2]]" product_sigma_defnil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )nil product_measure nil )nil product_measure nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil product_measure nil )nil product_finite_measure nil )nil measure_contractionnil )"extended_nnreal" extended_nnreal"extended_nnreal/" )"bool" booleans nil )nil extended_nnreal "extended_nnreal/" )"extended_nnreal" extended_nnreal"extended_nnreal/" )nil extended_nnreal "extended_nnreal/" )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" extended_nnreal "extended_nnreal/" )"nnreal" nil )"[[nat, nat] -> measure_type[[T1, T2], sigma_times(S1, S2)]]" nil )"extended_nnreal" extended_nnreal"extended_nnreal/" )"set[[T1, T2]]" cross_product"topology/" )"extended_nnreal" extended_nnreal"extended_nnreal/" )"bool" extended_nnreal "extended_nnreal/" )"(S)" nil )nil sets_lemmas nil )"set[T]" indexed_sets nil )"set" sets nil )"bool" sets nil )"bool" sets nil )nil measure_def nil )"(S)" nil )"finite_measure[[T1, T2], sigma_times(S1, S2)]" product_measurenil ))nil 3460264247"" (skosimp)"" "cross_product_is_sigma_times" "X" "X!1" "Y" "fullset[T2]" ))"" (rewrite "phi_is_simple" ) nil nil )) nil ))nil )"sigma_algebra[T2]" product_measure nil )"sigma_algebra[T1]" product_measure nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )nil booleans nil )nil booleans nil )nil product_measure nil )nil product_measure nil )"set" sets nil ) (set type-eq-decl nil sets nil )nil product_sigma nil )"measurable_set[T, S]" nil )"(S)" product_measure nil )"sigma_algebra[[T1, T2]]" product_sigma_defnil )"set[[T1, T2]]" cross_product"topology/" )nil measure_space nil ))nil ))nil 3460264247"" (skosimp)"" "cross_product_is_sigma_times" "Y" "Y!1" "X" "fullset[T1]" ))"" (rewrite "phi_is_simple" ) nil nil )) nil ))nil )"sigma_algebra[T2]" product_measure nil )"sigma_algebra[T1]" product_measure nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )nil booleans nil )nil booleans nil )nil product_measure nil )nil product_measure nil )"set" sets nil ) (set type-eq-decl nil sets nil )nil product_sigma nil )"measurable_set[T, S]" nil )"(S)" product_measure nil )"sigma_algebra[[T1, T2]]" product_sigma_defnil )"set[[T1, T2]]" cross_product"topology/" )nil measure_space nil ))nil )))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Dauer der Verarbeitung: 0.90 Sekunden
(vorverarbeitet am 2026-05-06)
¤ *© Formatika GbR, Deutschland
2026-05-26
