(fubini_tonelli_scafnil 3459570741"" (skosimp)"" (expand "measurable_set?" )"" (rewrite "cross_product_is_sigma_times" ) nil nil )) nil ))nil )"bool" measure_space_def nil )"sigma_algebra[T2]" fubini_tonelli_scaf nil )"sigma_algebra[T1]" fubini_tonelli_scaf 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 fubini_tonelli_scaf nil )nil fubini_tonelli_scaf nil )nil product_sigma nil ))nil ))nil 3459570741"" (skosimp)"" (expand "measurable_set?" ) (("" (propax) nil nil )) nil )) nil )"bool" measure_space_def nil )) nil ))nil 3459570741"" (skosimp)"" (expand "measurable_set?" ) (("" (propax) nil nil )) nil )) nil )"bool" measure_space_def nil )) nil ))nil 3460776966"" (skosimp)"" (lemma "cross_product_is_sigma_times" ("X" "X!1" "Y" "Y!1" ))"" "measurable_intersection" "a" "cross_product(X!1, Y!1)" "b" "E!1" ))"1" (expand "contraction" 1 1)"1" "F" "lambda j: fm_contraction[T2, S2](nu, A_of(nu)(j)) o ") "1" (case "forall j,x: F(j)(x)>=0" )"1" "MU" "lambda i: fm_contraction[T1, S1] ") "1" case "forall (E:(S1)): x_eq(mu(E), 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" "EE" "intersection(cross_product(X!1, Y!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" "G" "lambda j: (fm_contraction[T2, S2] ") "1" case "forall j,x: G(j)(x)>=0" )"1" "NU" "lambda i: fm_contraction[T1, S1] ") "1" case "forall i,j: integrable?[T1,S1,to_measure(NU(i))](G(j))" )"1" "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: LAMBDA j:LAMBDA i:LAMBDA j:") "1" expand "m_times" )"1" expand "to_measure" "1" expand "product_measure_approx" )"1" expand "fm_times" )"1" "x_sum_eq" "S" "LAMBDA i: LAMBDA j:" "T" "LAMBDA i: LAMBDA j:")) "1" "1" "x_sum_eq" "S" "LAMBDA i: LAMBDA j:" "T" "LAMBDA i: LAMBDA j:")) "1" "1" "1" expand "x_eq" )"1" "1" assert )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" "i!1" )"2" "x_sum_eq" "S" "LAMBDA j: " "T" "LAMBDA j: ")) "1" "1" nil nil )"2" "2" assert )"2" "j!1" )"2" expand "x_eq" "2" "i!1" "j!1" )"2" "measure_eq_integral[T1,S1]" "mu" "to_measure(fm_contraction[T1, S1] " "nu" "to_measure(NU(i!1))" "f" "G(j!1)" ))"2" assert )"2" expand "G" )"2" assert )"2" "2" "2" expand "to_measure" )"2" expand "x_eq" )"2" expand "NU" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "i!1" "j!1" )"2" "j!1" "_" )"2" "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" "3" "i!1" "j!1" )nil nil ))nil )"4" "4" "4" "i!1" "j!1" )"4" "j!1" "_" )"4" "integral_nonneg[T1, S1, to_measure(NU(i!1))]" "f" "G(j!1)" ))"1" replace "1" "measure_eq_integral[T1,S1]" "mu" "to_measure[T1, S1] " "nu" "to_measure(NU(i!1))" "f" "G(j!1)" ))"1" assert )"1" expand "G" "1" "1" "1" expand "to_measure" )"1" expand "NU" )"1" expand "x_eq" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "measurable_set?" )"2" rewrite "A_of_def2" )nil nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"5" expand "measurable_set?" )"5" rewrite "A_of_def2" )nil nil ))nil )"6" "6" "i!1" "j!1" )"6" "6" "measure_eq_integrable?[T1,S1]" "mu" "to_measure(NU(i!1))" "nu" "to_measure(fm_contraction[T1, S1] " "f" "G(j!1)" ))"1" "1" assert )"1" expand "G" )"1" nil nil ))nil ))nil )"2" "2" "2" expand "to_measure" )"2" expand "x_eq" )"2" expand "NU" )"2" 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" "2" "2" "i!1" "j!1" )"2" "j!1" "_" )"2" "integral_nonneg[T1, S1, to_measure(NU(i!1))]" "f" "G(j!1)" ))"1" replace "1" "measure_eq_integral[T1,S1]" "mu" "to_measure[T1, S1] " "nu" "to_measure(NU(i!1))" "f" "G(j!1)" ))"1" "1" expand "G" "1" assert )nil nil ))nil )"2" "2" "2" expand "to_measure" )"2" expand "x_eq" )"2" expand "NU" )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"3" nil nil ))nil )"2" expand "measurable_set?" )"2" rewrite "A_of_def2" )nil nil ))nil )"3" expand "measurable_set?" )"3" nil nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"3" expand "measurable_set?" )"3" nil nil ))nil )"4" "4" "4" "i!1" "j!1" )"4" "measure_eq_integrable?[T1,S1]" "mu" "to_measure(fm_contraction[T1, S1] " "nu" "to_measure(NU(i!1))" "f" "G(j!1)" ))"1" assert )"1" expand "G" )"1" assert )"1" "1" "1" expand "to_measure" )"1" expand "x_eq" )"1" expand "NU" )"1" 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" nil nil ))nil ))nil ))nil ))nil ))nil )"5" expand "measurable_set?" )"5" nil nil ))nil ))nil )"2" "2" assert )"2" "i!1" )"2" "x_sum_eq" "S" "LAMBDA j: " "T" "LAMBDA j: ")) "1" assert )"1" "j!1" )"1" "1" expand "x_eq" "1" "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" "i!1" "j!1" )"1" assert )"1" expand "F" "1" "1" "1" expand "MU" )"1" expand "to_measure" )"1" expand "x_eq" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "i!1" "j!1" )"2" "j!1" "_" )"2" "integral_nonneg[T1, S1, to_measure(MU(i!1))]" "f" "F(j!1)" ))"1" replace "1" "measure_eq_integral[T1,S1]" "mu" "to_measure[T1, S1] " "nu" "to_measure(MU(i!1))" "f" "F(j!1)" ))"1" replace "1" expand "F" "1" assert )"1" "1" "1" expand "MU" )"1" expand "to_measure" )"1" expand "x_eq" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "measurable_set?" )"2" rewrite "A_of_def2" )nil nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil )"3" expand "measurable_set?" )"3" rewrite "A_of_def2" )nil nil ))nil )"4" "4" "i!1" "j!1" )"4" "measure_eq_integrable?[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" expand "F" "1" expand "EE" )"1" assert )"1" "1" "1" expand "MU" )"1" expand "to_measure" )"1" expand "x_eq" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "measurable_set?" )"2" rewrite "A_of_def2" )nil nil ))nil ))nil ))nil ))nil )"5" "5" "i!1" "j!1" )"5" "j!1" "_" )"5" "integral_nonneg[T1, S1, to_measure[T1, S1](MU(i!1))]" "f" "F(j!1)" ))"5" assert )nil nil ))nil ))nil ))nil ))nil )"6" "6" "i!1" "j!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "i!1" "j!1" )"2" "j!1" "_" )"2" "measure_eq_integral[T1,S1]" "mu" "to_measure[T1, S1] " "nu" "to_measure(MU(i!1))" "f" "F(j!1)" ))"1" "integral_nonneg[T1,S1,to_measure(MU(i!1))]" "f" "F(j!1)" ))"1" assert )"1" replace "1" "1" assert )"1" expand "F" )"1" assert )nil nil ))nil ))nil )"2" "2" "2" expand "to_measure" )"2" expand "MU" )"2" expand "x_eq" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil )"2" expand "measurable_set?" )"2" rewrite "A_of_def2" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" "i!1" "j!1" )"3" "measure_eq_integrable?[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" expand "F" )"1" assert )"1" "1" "1" expand "MU" )"1" expand "to_measure" )"1" expand "x_eq" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "measurable_set?" )"2" rewrite "A_of_def2" )nil nil ))nil ))nil ))nil ))nil ))nil )"4" "4" "x1!1" )"4" expand "measurable_set?" )"4" assert )"4" expand "x_section" "4" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" case "x_eq(x_sum(LAMBDA j: LAMBDA i:LAMBDA j:LAMBDA i:") "1" "double_x_sum_eq" "U" "lambda i,j: (TRUE, ")) "1" "double_x_sum_eq" "U" "lambda i,j: (TRUE, ")) "1" assert )"1" "1" expand "x_eq" )"1" "1" assert )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" case "forall (E:(S1),i): x_eq(contraction(mu,A_of(mu)(i))(E),to_measure(MU(i))(E))" )"1" case "forall j: integrable?[T1,S1,mu](F(j)) <=> convergent?(series(lambda i: integral[T1, S1, to_measure(MU(i))](F(j))))" )"1" "x_sum_eq" "S" "LAMBDA j: LAMBDA i:" "T" "lambda j: if integrable?[T1,S1,mu](F(j)) then (TRUE,integral[T1,S1,mu](F(j))) else (FALSE,0) endif" ))"1" "1" case "x_eq(x_sum(LAMBDA j: IF integrable?[T1, S1, mu](F(j))LAMBDA j:LAMBDA i:") "1" "1" expand "x_eq" )"1" "1" assert )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" case "measurable_set?[T1, S1](X!1)" )"1" case "FORALL j: u, X!1)](G(j)) >= 0") "1" case "x_eq(x_sum(LAMBDA j: IF integrable?[T1, S1, mu](F(j))LAMBDA j:IF integrable?[T1, S1, contraction(mu,X!1)](G(j))") "1" "x_sum_eq" "S" "LAMBDA j: IF integrable?[T1, S1, contraction(mu, X!1)](G(j))" "T" "LAMBDA j: LAMBDA i:")) "1" "1" "1" expand "x_eq" )"1" "1" assert )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" "j!1" )"2" case "forall (E:(S1),i): x_eq(contraction(contraction(mu, X!1),A_of(contraction(mu,X!1))(i))(E),to_measure(NU(i))(E))" )"1" case "forall j: integrable?[T1,S1,contraction(mu, X!1)](G(j)) <=> convergent?(series(lambda i: integral[T1, S1, to_measure(NU(i))](G(j))))" )"1" expand "x_eq" "1" "integrable?[T1, S1, contraction(mu, X!1)](G(j!1))" )"1" "j!1" )"1" assert )"1" expand "x_sum" "1" "sfm_integral[T1,S1,contraction(mu, X!1)]" "f" "G(j!1)" ))"1" "(LAMBDA i: LAMBDA i:") "1" "1" "DRL1" "(series(LAMBDA (i_1: nat): ") "1" "LHS" "integral[T1, S1, contraction(mu, X!1)](G(j!1))" )"1" "1" assert )"1" rewrite "metric_convergence_def" )"1" "convergence_sequences.limit_def" "l" "LHS" "v" "DRL1" ))"1" assert )"1" expand "metric_converges_to" )"1" expand "convergence" )"1" "1" "1" "convergence_sequences.convergent?(DRL1)" )"1" "1" assert )"1" "1" "epsilon!1" )"1" "1" "n!1" )"1" "1" "i!1" )"1" assert )"1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" expand "convergent?" )"2" "LHS" )"2" expand "convergence" )"2" "2" "2" "epsilon!1" )"2" "2" "n!1" )"2" "2" "i!1" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" expand "convergent?" )"2" "LHS" )"2" expand "metric_converges_to" )"2" expand "convergence" )"2" "2" "epsilon!1" )"2" "2" "n!1" )"2" "2" "i!1" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "i!1" "j!1" )nil nil ))nil ))nil ))nil )"2" "1" "1" "measure_eq_integral[T1,S1]" "mu" "contraction(contraction(mu, X!1), " "nu" "to_measure(NU(x!1))" "f" "G(j!1)" ))"1" assert )"1" "x!1" "j!1" )"1" replace "1" "_" "x!1" )nil nil ))nil ))nil ))nil )"2" expand "measurable_set?" )"2" nil nil ))nil ))nil ))nil )"2" "2" "i!1" "j!1" )nil nil ))nil )"3" expand "measurable_set?" )"3" nil nil ))nil )"4" "4" "4" "_" "i!1" )"4" "i!1" "j!1" )"4" "measure_eq_integrable?[T1,S1]" "mu" "contraction(contraction(mu, X!1), " "nu" "to_measure(NU(i!1))" "f" "G(j!1)" ))"1" replace "1" replace "1" nil nil ))nil ))nil )"2" "2" "A_of[T1, S1](contraction[T1, S1](mu, X!1))(i!1)" )"2" expand "measurable_set?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "i!1" "j!1" )nil nil ))nil )"4" expand "measurable_set?" )"4" nil nil ))nil )"5" "5" "5" "_" "i!1" )"5" "i!1" "j!1" )"5" "measure_eq_integrable?[T1,S1]" "mu" "contraction(contraction(mu, X!1), " "nu" "to_measure(NU(i!1))" "f" "G(j!1)" ))"1" assert )nil nil )"2" expand "measurable_set?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "nn_integrable_is_nn_integrable[T1, S1, contraction[T1, S1](mu, X!1)]" "f" "G(j!1)" ))"2" assert )"2" "2" "j!1" "x!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" assert )"2" expand "x_sum" "2" "2" "j!1" )"2" "DRL1" "series(LAMBDA (i_1: nat): ") "1" replace "1" "1" expand "convergent?" )"1" "1" "l!1" )"1" expand "convergence" )"1" rewrite "metric_convergence_def" )"1" expand "metric_converges_to" )"1" "1" "r!1" )"1" "1" "n!1" )"1" "1" "i!1" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "i!1" "j!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" case "nn_measurable?[T1,S1](G(j!2))" )"1" "sfm_integrable[T1, S1, contraction(mu, X!1)]" "h" "G(j!2)" ))"1" "(LAMBDA i: LAMBDA i:") "1" "1" "(FORALL i: ") "1" assert )"1" replace "1" "UU" "(series((LAMBDA i: integral[T1, S1, to_measure(NU(i))](G(j!2)))))" )"1" "1" "1" nil nil )"2" nil nil ))nil ))nil )"2" "_" "j!2" )nil nil ))nil ))nil ))nil )"2" "2" "_" "i!1" )"2" "i!1" "j!2" )"2" "measure_eq_integrable?[T1,S1]" "mu" "contraction(contraction(mu, X!1), " "nu" "to_measure(NU(i!1))" "f" "G(j!2)" ))"1" assert )nil nil )"2" expand "measurable_set?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"3" expand "measurable_set?" )"3" nil nil ))nil ))nil ))nil )"2" "2" "1" "measure_eq_integral[T1,S1]" "mu" "contraction(contraction(mu, X!1), " "nu" "to_measure(NU(x!1))" "f" "G(j!2)" ))"1" "x!1" "j!2" )"1" "_" "x!1" )"1" assert )nil nil ))nil ))nil )"2" expand "measurable_set?" )"2" nil nil ))nil ))nil )"2" "2" "i!1" "j!2" )nil nil ))nil )"3" expand "measurable_set?" )"3" nil nil ))nil )"4" "4" "i!1" "j!2" )"4" "_" "i!1" )"4" "measure_eq_integrable?[T1,S1]" "mu" "contraction(contraction(mu, X!1), " "nu" "to_measure(NU(i!1))" "f" "G(j!2)" ))"1" replace "1" replace "1" nil nil ))nil ))nil )"2" expand "measurable_set?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "i!1" "j!2" )nil nil ))nil )"4" expand "measurable_set?" )"4" nil nil ))nil )"5" "5" "_" "i!1" )"5" "i!1" "j!2" )"5" "measure_eq_integrable?[T1,S1]" "mu" "contraction(contraction(mu, X!1), " "nu" "to_measure(NU(i!1))" "f" "G(j!2)" ))"1" assert )nil nil )"2" expand "measurable_set?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil )"2" expand "nn_measurable?" )"2" "1" expand "G" )"1" "1" "x_section_measurable" "nu" "fm_contraction[T2, S2] " "M" "E!1" ))"1" nil nil ))nil ))nil ))nil )"2" "2" "j!2" "x!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "NU" )"2" "contraction(mu, X!1)" )"2" "MU1" "contraction(mu, X!1)" )"2" expand "to_measure" )"2" expand "fm_contraction" )"2" expand "contraction" )"2" expand "x_eq" )"2" "A_of_def2" "mu" "MU1" "n" "i!1" ))"2" "m_monotone[T1,S1,MU1]" "a" "intersection(A_of(MU1)(i!1), E!2)" "b" "A_of(MU1)(i!1)" ))"1" expand "x_le" )"1" assert )"1" expand "intersection" )"1" expand "subset?" )"1" expand "member" )"1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "measurable_set?" )"2" nil nil ))nil )"3" expand "measurable_set?" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" expand "measurable_set?" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" case "forall (l:real): ((forall j: integrable?[T1, S1, mu](F(j)))&convergence(series(LAMBDA j:integral[T1, S1, mu](F(j))),l)) <=> ((forall j: integrable?[T1, S1, contraction(mu, X!1)](G(j)))&convergence(series(LAMBDA j:integral[T1, S1, contraction(mu, X!1)](G(j))),l))" )"1" expand "x_sum" "1" "(FORALL i: IF integrable?[T1, S1, mu](F(i)) THEN TRUEAND LAMBDA i:IF integrable?[T1, S1, mu](F(i))") "1" "1" "FORALL j: integrable?[T1, S1, mu](F(j))" )"1" "(LAMBDA i: IF integrable?[T1, S1, mu](F(i))LAMBDA j: integral[T1, S1, mu](F(j)))") "1" "1" "convergence_sequences.limit_lemma" "v" "series(LAMBDA j: integral[T1, S1, mu](F(j)))" ))"1" "convergence_sequences.limit LAMBDA j: integral[T1, S1, mu](F(j))))") "1" replace "1" "(FORALL i: IF integrable?[T1, S1, contraction(mu, X!1)](G(i))AND LAMBDA i:IF integrable?") "1" expand "x_eq" "1" "(LAMBDA i: IF integrable?[T1, S1, contraction(mu, X!1)](G(i))LAMBDA j:") "1" "1" rewrite "convergence_sequences.limit_def" "1" assert )nil nil ))nil ))nil )"2" "2" "1" "1" "x!1" )"1" "1" assert )nil nil ))nil ))nil ))nil )"2" "2" "j!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"3" "3" "j!1" )"3" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" "1" "1" "i!1" )"1" assert )nil nil ))nil ))nil )"2" "(LAMBDA i: IF integrable?[T1, S1, contraction(mu, X!1)]LAMBDA j:") "1" expand "convergence_sequences.convergent?" )"1" "convergence_sequences.limit LAMBDA j: integral[T1, S1, mu](F(j))))") nil nil ))nil )"2" "2" "x!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" expand "measurable_set?" )"3" nil nil ))nil )"4" expand "measurable_set?" )"4" nil nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil )"2" "2" "2" "x!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" "j!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" expand "x_eq" "2" "FORALL j: integrable?[T1, S1, contraction(mu, X!1)](G(j))" )"1" "(LAMBDA i: IF integrable?[T1, S1, contraction(mu, X!1)]LAMBDA j:") "1" "convergence_sequences.convergent?(series(LAMBDA j: ") "1" "1" "convergence_sequences.limit_lemma" "v" "series(LAMBDA j: integral[T1, S1, contraction(mu, X!1)](G(j)))" ))"1" "convergence_sequences.limit(series(LAMBDA j: ") "1" replace "1" "1" "1" "1" "1" "i!1" )"1" assert )nil nil ))nil ))nil )"2" "(LAMBDA i: IF integrable?[T1, S1, mu](F(i))LAMBDA j: integral[T1, S1, mu](F(j)))") "1" "1" expand "convergence_sequences.convergent?" )"1" "convergence_sequences.limit LAMBDA j:") "1" expand "measurable_set?" )"1" nil nil ))nil ))nil ))nil ))nil )"2" "2" "x!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil )"3" nil nil ))nil ))nil )"2" replace "2" nil nil ))nil ))nil )"2" "2" "x!1" )"2" assert )nil nil ))nil ))nil ))nil )"2" "2" "2" "2" "j!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "1" "1" "FF" "lambda j: lambda x: series(lambda i: F(i)(x))(j)" )"1" case "forall j: integrable?[T1, S1, mu](FF(j))" )"1" case "forall (n:nat): series(LAMBDA j: integral[T1, S1, mu](F(j)))(n) = (integral[T1, S1, mu] o FF)(n)" )"1" "extensionality_postulate" "f" "series(LAMBDA j: integral[T1, S1, mu](F(j)))" "g" "integral[T1, S1, mu] o FF" ))"1" replace "1" assert )"1" replace "1" "1" "monotone_convergence[T1, S1, mu]" "F" "FF" ))"1" "ae_increasing?(FF)" )"1" "real_fun_preds.bounded?(integral[T1,S1,mu] o FF)" )"1" assert )"1" "1" "1" "f!1" )"1" assert )"1" "f!1" )"1" case "forall x: x_eq(x_limit(LAMBDA j: (TRUE,FF(j)(x))), nu(x_section(EE, x)))" )"1" case "ae?(lambda x: x_eq((TRUE,plus(f!1)(x)),nu(x_section(EE, x))))" )"1" "1" "FORALL j: integrable?[T1, S1, contraction(mu, X!1)](G(j))" )"1" "GG" "lambda j: lambda x: series(LAMBDA i: G(i)(x))(j)" )"1" "1" case "FORALL j: integrable?[T1, S1, contraction(mu, X!1)](GG(j))" )"1" case "forall j,x: GG(j)(x) >= 0" )"1" case "forall j: series(LAMBDA i: )] o GG)(j)") "1" "series(LAMBDA j: G") "1" "l!1=integral[T1,S1,mu](f!1)" )"1" "1" case "ae_nonneg?(f!1)" )"1" case "ae_eq?(f!1,*[T1](phi(X!1),f!1))" )"1" "1" "HH" "lambda j: *[T1](phi(X!1),GG(j))" )"1" case "forall j: integrable?[T1, S1, mu](HH(j))" )"1" case "FORALL j, x: HH(j)(x) >= 0" )"1" "1" case "forall j: (integral[T1, S1, contraction(mu, X!1)] o GG)(j) = (integral[T1,S1,mu] o HH)(j)" )"1" "integral[T1, S1, contraction(mu, X!1)] o GG=integral[T1, S1, mu] o HH" )"1" "1" "monotone_convergence[T1, S1, mu]" "F" "HH" ))"1" "ae_increasing?(HH)" )"1" "1" "1" "indefinite_integrable[T1, S1, mu]" "f" "f!1" "E" "X!1" ))"1" "*[T1](phi(X!1), f!1)" )"1" "1" expand "converges_upto?" )"1" "1" "SS" "integral[T1, S1, mu] o HH" )"1" "integral_ae_eq[T1,S1,mu]" "f" "f!1" "h" "*[T1](phi(X!1), f!1)" ))"1" assert )"1" replace "1" "LIMIT" "integral[T1, S1, mu](f!1)" )"1" "1" expand "convergence" )"1" rewrite "metric_convergence_def" )"1" expand "metric_converges_to" )"1" "1" "epsilon!1" )"1" "1" "n!1" )"1" "1" "i!1" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "HH" )"2" expand "ae_convergence?" )"2" expand "ae_convergence_in?" )"2" expand "ae_nonneg?" )"2" expand "pointwise_ae?" )"2" expand "ae?" )"2" expand "fullset" )"2" expand "ae_in?" )"2" "2" "union(E!2,E!3)" )"2" "2" expand "union" )"2" "x!1" )"2" "x!1" )"2" assert )"2" "2" assert )"2" expand "plus" )"2" expand "max" )"2" expand "*" )"2" expand "phi" )"2" expand "member" )"2" rewrite "metric_convergence_def" )"2" expand "x_eq" "2" "2" "x!1" )"2" "x!1" )"2" "X!1(x!1)" )"1" expand "x_eq" )"1" "1" assert )"1" "x_limit_to_sum" "S" "LAMBDA j: (TRUE,GG(j)(x!1))" "T" "LAMBDA j: (TRUE,G(j)(x!1))" ))"1" "1" expand "x_eq" )"1" "1" assert )"1" expand "x_sum" )"1" "convergence_sequences.convergent?(series(LAMBDA j: G(j)(x!1)))" )"1" replace "1" replace "1" replace "1" expand "x_limit" )"1" "convergence_sequences.convergent?(LAMBDA i: GG(i)(x!1))" )"1" case "convergence(LAMBDA j: GG(j)(x!1),f!1(x!1))" )"1" "1" expand "metric_converges_to" )"1" expand "convergence" )"1" "1" "r!1" )"1" "1" "n!1" )"1" "1" "i!1" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "convergence_sequences.limit_def" "v" "LAMBDA i: GG(i)(x!1)" "l" "f!1(x!1)" ))"1" assert )nil nil )"2" nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "GG" )"2" expand "series" )"2" expand "x_sigma" )"2" expand "x_eq" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "GG" )"2" expand "series" )"2" "j" )"1" expand "sigma" )"1" assert )nil nil ))nil )"2" "2" expand "sigma" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" expand "metric_converges_to" )"2" "2" "0" )"2" "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 ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "ae_increasing?" )"2" expand "HH" )"2" expand "*" )"2" expand "phi" )"2" expand "member" )"2" "emptyset" )"2" "2" "2" "2" "2" assert )"2" "2" expand "GG" )"2" expand "series" )"2" "_" "x!1" )"2" "sigma_split" "low" "0" "high" "j!1" "z" "i!1" "F" "LAMBDA i: G(i)(x!1)" ))"2" assert )"2" replace "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 )"2" nil nil ))nil )"2" "2" "2" expand "o" )"2" expand "HH" )"2" "j!1" )"2" "contraction_integral[T1,S1]" "A" "X!1" "f" "GG(j!1)" "mu" "mu" ))"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" nil nil ))nil ))nil )"2" expand "HH" )"2" expand "*" )"2" "2" "2" "j!1" "x!1" )"2" expand "phi" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "j!1" )"2" "contraction_integrable[T1,S1]" "mu" "mu" "A" "X!1" "f" "GG(j!1)" ))"1" expand "HH" )"1" assert )nil nil ))nil )"2" "integrable_is_measurable[T1, S1, contraction(mu, X!1)]" )"2" "GG(j!1)" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "ae_nonneg?" )"2" expand "ae_eq?" )"2" expand "restrict" )"2" expand "pointwise_ae?" )"2" expand "ae?" )"2" expand "fullset" )"2" expand "ae_in?" )"2" "2" "union(E!2,E!3)" )"2" "2" "x!1" )"2" "x!1" )"2" expand "union" )"2" expand "member" )"2" "2" assert )"2" expand "plus" )"2" expand "max" )"2" expand "x_eq" )"2" "2" expand "*" )"2" expand "phi" )"2" expand "member" )"2" "2" assert )"2" "2" expand "EE" )"2" expand "cross_product" )"2" expand "intersection" )"2" expand "x_section" )"2" expand "member" )"2" assert )"2" "nu" )"2" expand "sigma_finite_measure?" )"2" expand "measure?" )"2" "2" expand "measure_empty?" )"2" expand "emptyset" )"2" assert )"2" replace "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 ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "ae_increasing?" )"2" expand "ae_convergence?" )"2" expand "ae_convergence_in?" )"2" expand "ae_nonneg?" )"2" expand "pointwise_ae?" )"2" expand "ae?" )"2" expand "fullset" )"2" expand "ae_in?" )"2" "2" "union(E!2,E!3)" )"2" "2" "x!1" )"2" "x!1" )"2" expand "union" )"2" expand "member" )"2" "2" assert )"2" rewrite "metric_convergence_def" )"2" expand "metric_converges_to" )"2" "0" "x!1" )"2" "F(0)(x!1)-f!1(x!1)" )"1" "1" "0" "n!1" )"1" "n!1" )"1" expand "FF" "1" expand "series" )"1" expand "sigma" )"1" assert )"1" expand "ball" )"1" assert )nil nil ))nil ))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 ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "converges_upto?" )"2" "2" "SS" "integral[T1, S1, mu] o FF" )"2" "RHS" "integral[T1, S1, mu](f!1)" )"2" "2" "convergence_sequences.unique_limit" "u" "SS" "l1" "l!1" "l2" "RHS" ))"2" assert )"2" "2" expand "convergence" )"2" rewrite "metric_convergence_def" )"2" expand "metric_converges_to" )"2" "2" "epsilon!1" )"2" "2" "n!1" )"2" "2" "i!1" )
Messung V0.5 in Prozent C=100 H=96 G=97
¤ Dauer der Verarbeitung: 0.464 Sekunden
(vorverarbeitet am 2026-04-28)
¤ *© Formatika GbR, Deutschland
