(integral_convergencenil 3409506492"" (skosimp*)"" "(EXISTS f: ae_convergence?(F!1, f)) IFF bounded?(integral o F!1)" )"1" (assert )"1" (skolem!)"1" (flatten)"1" (hide -2)"1" (split -1)"1" (expand "ae_increasing?" )"1" (expand "ae_convergence?" )"1" (expand "fullset" )"1" (expand "ae_convergence_in?" )"1" (expand "ae_in?" )"1" (skolem - "E1" )"1" (skolem - "E2" )"1" "union(E1,E2)" )"1" expand "negligible_set?" )"1" "1" "null_set_is_measurable" )"1" "X!1" )"1" "monotone_convergence_scaf" "f" "phi(complement(X!1))*f!1" "F" "lambda n: phi(complement(X!1))*F!1(n)" ))"1" "integral o (LAMBDA n: phi(complement(X!1)) * F!1(n))=integral o F!1" )"1" "1" replace -5)"1" "integral(phi(complement(X!1)) * f!1)=integral(f!1)" )"1" "1" nil nil )"2" "2" expand "pointwise_converges_upto?" )"2" "pointwise_increasing?(LAMBDA n: phi(complement(X!1)) * F!1(n))" )"1" expand "pointwise_convergence?" )"1" "1" "x!1" )"1" expand "complement" )"1" expand "member" )"1" expand "phi" )"1" expand "member" )"1" "1" expand "subset?" )"1" expand "union" )"1" expand "member" )"1" "x!1" )"1" expand "*" "1" "E2(x!1)" )"1" assert )"1" "1" expand "convergence?" )"1" "1" "0" )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "X!1(x!1)" )"1" "1" expand "convergence?" )"1" "1" "0" )"1" "1" assert )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 )"2" "2" "2" expand "pointwise_increasing?" )"2" "2" expand "*" )"2" expand "complement" )"2" expand "phi" )"2" expand "member" )"2" "x!1" )"2" expand "subset?" )"2" expand "union" )"2" expand "member" )"2" "x!1" )"2" "X!1(x!1)" )"1" expand "increasing?" )"1" nil nil ))nil )"2" assert )"2" expand "increasing?" )"2" "2" assert )"2" "x!2" "y!1" )"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 )"2" "2" "integral_ae_eq" "f" "f!1" "h" "phi(complement(X!1)) * f!1" ))"1" "1" "1" assert )nil nil ))nil )"2" "2" expand "ae_eq?" )"2" expand "restrict" )"2" expand "pointwise_ae?" )"2" expand "*" )"2" expand "complement" )"2" expand "phi" )"2" expand "member" )"2" expand "ae?" )"2" expand "fullset" )"2" expand "ae_in?" )"2" "X!1" )"1" "1" assert )nil nil ))nil )"2" expand "negligible_set?" )"2" "X!1" )"2" assert )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "integrable_is_measurable" )"2" "2" rewrite "indefinite_integrable" )"2" "2" rewrite "measurable_complement" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" rewrite "indefinite_integrable" )"3" rewrite "measurable_complement" )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "o " )"2" "1" "integral_ae_eq" "f" "F!1(x!1)" "h" "phi(complement(X!1)) * F!1(x!1)" ))"1" "1" "1" assert )nil nil ))nil )"2" "2" expand "ae_eq?" )"2" expand "restrict" )"2" expand "pointwise_ae?" )"2" expand "*" "2" expand "complement" )"2" expand "phi" )"2" expand "member" )"2" expand "ae?" )"2" expand "fullset" )"2" expand "ae_in?" )"2" "X!1" )"1" "1" assert )nil nil ))nil )"2" expand "negligible_set?" )"2" "X!1" )"2" assert )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "integrable_is_measurable" )"2" rewrite "indefinite_integrable" )"2" rewrite "measurable_complement" )nil nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "indefinite_integrable" )"2" rewrite "measurable_complement" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "indefinite_integrable" )"2" rewrite "measurable_complement" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (inst + "f!1" ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (split)"1" (skosimp*)"1" (expand "bounded?" )"1" (split)"1" (expand "bounded_above?" )"1" (inst + "integral(f!1)" )"1" (skolem + ("n!1" ))"1" (expand "o " )"1" (expand "ae_convergence?" )"1" (expand "ae_increasing?" )"1" (expand "ae_convergence_in?" )"1" expand "fullset" )"1" expand "ae_in?" )"1" "1" "union(E!1,E!2)" )"1" expand "negligible_set?" )"1" "1" "integral_ae_le" "f1" "phi(complement(X!1))*F!1(n!1)" "f2" "phi(complement(X!1))*f!1" ))"1" "1" "integral_ae_eq" "f" "f!1" "h" "phi(complement(X!1)) * f!1" ))"1" "1" "1" replace -2 * rl)"1" "integral_ae_eq" "f" "F!1(n!1)" "h" "phi(complement(X!1)) * F!1(n!1)" ))"1" "1" "1" assert )nil nil ))nil )"2" "2" expand "ae_eq?" )"2" expand "restrict" )"2" expand "pointwise_ae?" )"2" expand "ae?" )"2" expand "*" )"2" expand "complement" )"2" expand "phi" )"2" expand "member" )"2" expand "fullset" )"2" expand "ae_in?" )"2" "X!1" )"1" "1" assert )nil nil ))nil )"2" rewrite "null_is_negligible" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "integrable_is_measurable" )nil nil ))nil ))nil ))nil )"2" "2" expand "ae_eq?" )"2" expand "restrict" )"2" expand "pointwise_ae?" )"2" expand "complement" )"2" expand "phi" )"2" expand "member" )"2" expand "ae?" )"2" expand "fullset" )"2" expand "ae_in?" )"2" "X!1" )"1" "1" assert )"1" expand "*" )"1" assert )nil nil ))nil ))nil ))nil )"2" rewrite "null_is_negligible" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "integrable_is_measurable" )nil nil ))nil )"2" "2" expand "ae_le?" )"2" expand "*" )"2" expand "pointwise_ae?" )"2" expand "complement" )"2" expand "phi" )"2" expand "member" )"2" expand "ae?" )"2" expand "fullset" )"2" expand "ae_in?" )"2" "X!1" )"1" "1" assert )"1" expand "union" )"1" expand "subset?" )"1" expand "member" )"1" "x!1" )"1" "x!1" )"1" "x!1" )"1" "E!1(x!1)" )"1" "E!2(x!1)" )"1" assert )"1" "1" rewrite "metric_convergence_def" )"1" case "F!1(n!1)(x!1)-f!1(x!1)>0" )"1" expand "metric_converges_to" )"1" "F!1(n!1)(x!1) - f!1(x!1)" )"1" "1" "1" "n!1+n!2" )"1" assert )"1" "n!1" "n!1+n!2" )"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 )"2" rewrite "null_is_negligible" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "indefinite_integrable" )"2" rewrite "measurable_complement" )"2" expand "null_set?" )"2" nil nil ))nil ))nil ))nil )"3" rewrite "indefinite_integrable" )"3" rewrite "measurable_complement" )"3" expand "null_set?" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "bounded_below?" )"2" (inst + "integral(F!1(0))" )"2" (skolem + ("n!1" ))"2" (expand "o " )"2" (expand "ae_increasing?" )"2" (skosimp)"2" "integral_ae_le" "f1" "F!1(0)" "f2" "F!1(n!1)" ))"2" assert )"2" "2" expand "ae_le?" )"2" expand "pointwise_ae?" )"2" expand "ae?" )"2" expand "fullset" )"2" expand "ae_in?" )"2" "E!1" )"2" "2" "x!1" )"2" assert )"2" "0" "n!1" )"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" (flatten)"2" (expand "ae_increasing?" )"2" (skosimp)"2" (typepred "E!1" )"2" (expand "negligible_set?" )"2" (skosimp)"2" case "forall (F:sequence[nn_integrable]): bounded?(integral o F)&pointwise_increasing?(F)=>EXISTS (f:nn_integrable): ae_convergence?(F, f)" )"1" "lambda n: phi(complement(X!1))*(F!1(n)-F!1(0))" )"1" (split -1)"1" (skosimp)"1" "f!1" )"1" "f!1+phi(complement(X!1)) *F!1(0)" )"1" expand "ae_convergence?" )"1" expand "fullset" )"1" expand "ae_convergence_in?" )"1" expand "ae_in?" )"1" "1" "union(X!1,E!2)" )"1" "1" expand "union" )"1" expand "member" )"1" "1" expand "+ " )"1" expand "*" )"1" "x!1" )"1" assert )"1" expand "-" )"1" expand "complement" )"1" expand "phi" )"1" expand "member" )"1" "1" rewrite "metric_convergence_def" )"1" rewrite "metric_convergence_def" )"1" expand "metric_converges_to" )"1" "1" "r!1" )"1" "1" "n!1" )"1" "1" "i!1" )"1" expand "ball" )"1" expand "member" )"1" 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" rewrite "negligible_union" )"2" rewrite "null_is_negligible" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "integrable_add" )"2" "2" "integral_ae_eq" "f" "F!1(0)" "h" "*[T](phi[T, S](complement[T](X!1)), F!1(0))" ))"1" "1" (flatten) nil nil )"2" "2" expand "ae_eq?" )"2" expand "restrict" )"2" expand "pointwise_ae?" )"2" expand "ae?" )"2" expand "fullset" )"2" expand "ae_in?" )"2" "X!1" )"1" "1" expand "*" )"1" expand "complement" )"1" expand "phi" )"1" expand "member" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "null_is_negligible" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "phi_is_simple" "X" "complement[T](X!1)" ))"1" expand "simple?" )"1" "1" rewrite "prod_measurable" )nil nil ))nil ))nil )"2" expand "null_set?" )"2" "2" "measurable_complement" "a" "X!1" ))"2" expand "measurable_set?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" expand "bounded?" )"2" "1" "1" expand "bounded_above?" )"1" "1" "1" "a!1-integral(F!1(0))" )"1" "n!1" ))"1" expand "o" )"1" "n!1" )"1" "integral_ae_eq" "f" "F!1(n!1) - F!1(0)" "h" "phi(complement(X!1)) * (F!1(n!1) - F!1(0))" ))"1" "1" "1" replace "1" rewrite "integral_diff" )"1" assert )nil nil ))nil ))nil ))nil )"2" "2" expand "ae_eq?" )"2" expand "restrict" )"2" expand "pointwise_ae?" )"2" expand "ae?" )"2" expand "fullset" )"2" expand "ae_in?" )"2" "X!1" )"1" "1" expand "subset?" )"1" "x!1" )"1" "x!1" )"1" expand "complement" )"1" expand "phi" )"1" expand "member" )"1" expand "*" )"1" expand "-" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "null_is_negligible" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "integrable_diff" "f1" "F!1(n!1)" "f2" "F!1(0)" ))"2" "integrable_is_measurable" "x" "(-[T])(F!1(n!1), F!1(0))" ))"2" "phi_is_simple" "X" "complement[T](X!1)" ))"1" expand "simple?" )"1" "1" rewrite "prod_measurable" )nil nil ))nil ))nil )"2" expand "null_set?" )"2" "2" "measurable_complement" "a" "X!1" ))"2" expand "measurable_set?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "bounded_below?" )"2" "0" )"2" "n!1" ))"2" expand "o " )"2" "integral_nonneg" "f" "phi(complement(X!1)) * (F!1(n!1) - F!1(0))" ))"2" "1" (assert ) nil nil )"2" "2" "2" expand "*" )"2" expand "-" )"2" "x!1" )"2" expand "subset?" )"2" "x!1" )"2" expand "complement" )"2" expand "phi" )"2" expand "member" )"2" "X!1(x!1)" )"1" assert )nil nil )"2" assert )"2" "0" "n!1" )"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 )"3" (hide 2)"3" expand "pointwise_increasing?" )"3" "3" "x!1" )"3" expand "subset?" )"3" "x!1" )"3" expand "member" )"3" expand "increasing?" )"3" "i!1" "j!1" ))"3" "3" expand "*" )"3" expand "-" )"3" expand "complement" )"3" expand "phi" )"3" expand "member" )"3" "X!1(x!1)" )"1" assert )nil nil )"2" assert )"2" "i!1" "j!1" )"2" assert )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" "1" "x!1" )"1" expand "*" )"1" expand "complement" )"1" expand "phi" )"1" expand "member" )"1" expand "subset?" )"1" "x!1" )"1" expand "member" )"1" "x!1" )"1" "X!1(x!1)" )"1" assert )nil nil )"2" assert )"2" expand "-" )"2" "0" "n!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "integrable_diff" "f1" "F!1(n!1)" "f2" "F!1(0)" ))"2" "integral_ae_eq" "f" "(-[T])(F!1(n!1), F!1(0))" "h" "*[T](phi[T, S](complement[T](X!1)), ((-[T])(F!1(n!1), F!1(0))))" ))"1" "1" "1" rewrite "nn_integrable_is_nn_integrable" )"1" "1" "1" expand "*" )"1" expand "complement" )"1" expand "phi" )"1" expand "member" )"1" expand "-" )"1" "x!1" )"1" expand "subset?" )"1" "x!1" )"1" expand "member" )"1" "X!1(x!1)" )"1" assert )nil nil )"2" assert )"2" "0" "n!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "ae_eq?" )"2" expand "restrict" )"2" expand "pointwise_ae?" )"2" expand "ae?" )"2" expand "fullset" )"2" expand "ae_in?" )"2" "X!1" )"1" "1" expand "complement" )"1" expand "phi" )"1" expand "member" )"1" expand "*" )"1" expand "-" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "null_is_negligible" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "integrable_is_measurable" "x" "(-[T])(F!1(n!1), F!1(0))" ))"2" rewrite "prod_measurable" )"2" "phi_is_simple" "X" "complement[T](X!1)" ))"1" rewrite "simple_is_measurable" )nil nil )"2" expand "null_set?" )"2" "2" "measurable_complement" "a" "X!1" ))"2" expand "measurable_set?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (skosimp)"2" "H" "LAMBDA n: LAMBDA (m: nat): {x | F!2(n)(x) >= m+1}" )"2" "HH" "LAMBDA (m: nat): IUnion(LAMBDA n: H(n)(m))" )"2" "2" case "forall (n,m:nat): measurable_set?(H(n)(m))" )"1" case "forall (m:nat): measurable_set?(HH(m))" )"1" "measurable_IIntersection" "SS" "HH" ))"1" case "FORALL x: NOT IIntersection[nat, T](HH)(x)) IFF") "1" case "forall (n,m:nat): mu_fin?(H(n)(m))" )"1" case "forall (n,m:nat,x:T): ((m+1)*phi(H(n)(m)))(x) <= F!2(n)(x)" )"1" case "forall (n,m:nat): (m+1)*mu(H(n)(m)) <= nn_integral(F!2(n))" )"1" expand "bounded?" )"1" "1" "1" expand "bounded_above?" )"1" "M" )"1" expand "o " )"1" case "forall (n,m:nat): subset?(H(n)(m),HH(m))" )"1" case "forall (n,m:nat): mu(H(n)(m)) <= M/(1+m)" )"1" "DIVERGENT" "IIntersection[nat, T](HH)" )"1" case "null_set?(DIVERGENT)" )"1" case "pointwise_bounded?(lambda n: phi(complement(DIVERGENT))*F!2(n))" )"1" "SUP" "lambda x: sup(Im(lambda n: (phi(complement(DIVERGENT)) * F!2(n))(x)))" )"1" case "forall x: least_upper_bound(<=)(SUP(x),Im(LAMBDA n: (phi(complement(DIVERGENT)) * F!2(n))(x)))" )"1" "monotone_convergence_scaf" "F" "lambda n: phi(complement(DIVERGENT)) * F!2(n)" "f" "SUP" ))"1" "1" "1" "1" "nn_integrable_is_nn_integrable" "f" "SUP" ))"1" "1" "SUP" )"1" expand "ae_convergence?" )"1" expand "fullset" )"1" expand "ae_convergence_in?" )"1" expand "ae_in?" )"1" "DIVERGENT" )"1" "1" "x!1" )"1" expand "*" "1" expand "complement" )"1" expand "phi" "1" expand "member" )"1" "1" assert )"1" replace "1" "1" expand "pointwise_increasing?" )"1" "x!1" )"1" rewrite "metric_convergence_def" )"1" expand "metric_converges_to" )"1" "1" expand "member" )"1" expand "ball" )"1" "LIMIT" "SUP(x!1)" )"1" expand "Im" )"1" expand "least_upper_bound" )"1" "1" "LIMIT-r!1" )"1" assert )"1" expand "upper_bound" )"1" "1" "z!1" )"1" "n!1" )"1" case "z!1>LIMIT-r!1" )"1" "1" "n!1" )"1" "1" expand "increasing?" )"1" "n!1" "i!1" )"1" assert )"1" "F!2(i!1)(x!1)" )"1" expand "abs" )"1" assert )nil nil ))nil )"2" "i!1" )"2" 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 ))nil ))nil ))nil ))nil )"2" rewrite "null_is_negligible" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "pointwise_increasing?" )"2" "x!1" )"2" "x!1" )"2" expand "least_upper_bound" )"2" "2" "2" expand "Im" )"2" expand "upper_bound" )"2" "(phi(complement(DIVERGENT)) * F!2(0))(x!1)" )"1" expand "*" )"1" expand "phi" )"1" "1" nil nil ))nil ))nil ))nil )"2" "0" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil )"2" "2" expand "pointwise_converges_upto?" )"2" "pointwise_increasing?(LAMBDA n: phi(complement(DIVERGENT)) * F!2(n))" )"1" expand "pointwise_convergence?" )"1" "1" "1" expand "pointwise_increasing?" )"1" "x!1" )"1" "x!1" )"1" "G" "LAMBDA (n_1: nat): ") "1" "LIMIT" "SUP(x!1)" )"1" "1" rewrite "metric_convergence_def" )"1" expand "metric_converges_to" )"1" "1" expand "ball" )"1" expand "member" )"1" expand "least_upper_bound" )"1" "1" "LIMIT-r!1" )"1" assert )"1" expand "upper_bound" )"1" "1" "z!1" )"1" case "z!1>LIMIT-r!1" )"1" "1" expand "Im" )"1" "n!1" )"1" "n!1" )"1" "1" "G(i!1)" )"1" expand "abs" )"1" expand "increasing?" )"1" "n!1" "i!1" )"1" assert )nil nil ))nil ))nil ))nil )"2" expand "Im" )"2" "i!1" )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 )"2" "2" expand "pointwise_increasing?" )"2" "2" "x!1" )"2" expand "increasing?" )"2" "i!1" "j!1" ))"2" "i!1" "j!1" )"2" "2" assert )"2" expand "*" )"2" expand "phi" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" expand "bounded?" )"3" "1" expand "bounded_above?" )"1" "M" )"1" "n!1" ))"1" expand "o " )"1" "n!1" )"1" "integral_ae_eq" "f" "F!2(n!1)" "h" "phi(complement(DIVERGENT)) * F!2(n!1)" ))"1" "1" "1" replace "1" nil nil ))nil ))nil )"2" "2" expand "ae_eq?" )"2" expand "restrict" )"2" expand "pointwise_ae?" )"2" expand "ae?" )"2" expand "fullset" )"2" expand "ae_in?" )"2" "DIVERGENT" )"1" "1" expand "*" )"1" expand "complement" )"1" expand "phi" )"1" expand "member" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "null_is_negligible" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "indefinite_integrable" "E" "complement[T](DIVERGENT)" "f" "F!2(n!1)" ))"1" rewrite "integrable_is_measurable" )nil nil )"2" rewrite "measurable_complement" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "bounded_below?" )"2" "0" )"2" "n!1" ))"2" expand "o " )"2" "2" "measurable_complement" "a" "DIVERGENT" ))"1" "indefinite_integrable" "E" "complement[T](DIVERGENT)" "f" "F!2(n!1)" ))"1" "integral_ae_eq" "f" "F!2(n!1)" "h" "phi(complement[T](DIVERGENT)) * F!2(n!1)" ))"1" "1" "1" replace "1" "integral_nonneg" "f" "F!2(n!1)" ))"1" "1" assert )nil nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "ae_eq?" )"2" expand "restrict" )"2" expand "pointwise_ae?" )"2" expand "ae?" )"2" expand "fullset" )"2" expand "ae_in?" )"2" "DIVERGENT" )"1" "1" expand "*" )"1" expand "complement" )"1" expand "phi" )"1" expand "member" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "null_is_negligible" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "integrable_is_measurable" )nil nil ))nil )"2" nil nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "indefinite_integrable" "2" rewrite "measurable_complement" )nil nil ))nil ))nil ))nil )"2" "2" "2" replace "2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "pointwise_bounded?" )"2" expand "pointwise?" )"2" "x!1" )"2" expand "bounded_seq?" )"2" expand "fullset" )"2" expand "image" )"2" expand "Im" )"2" expand "bounded?" )"2" "2" expand "subset?" )"2" expand "member" )"2" expand "above_bounded" )"2" "x!2+r!1" )"2" expand "upper_bound" )"2" "2" "z!1" )"2" "2" "z!1" )"2" "1" "1" expand "ball" )"1" nil nil ))nil ))nil )"2" "x!3" )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 "pointwise_bounded?" )"2" expand "pointwise_increasing?" )"2" expand "pointwise?" )"2" "2" "x!1" )"2" "x!1" )"2" expand "*" )"2" expand "complement" )"2" expand "phi" )"2" expand "member" )"2" "DIVERGENT(x!1)" )"1" expand "bounded_seq?" )"1" expand "fullset" )"1" expand "image" )"1" expand "bounded?" )"1" "0" "1" )"1" expand "subset?" )"1" expand "member" )"1" expand "ball" )"1" expand "abs" )"1" "1" "1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" expand "bounded_seq?" )"2" expand "fullset" )"2" expand "image" )"2" expand "bounded?" )"2" "0" "k!1" )"2" expand "subset?" )"2" expand "member" )"2" "2" replace "2" "2" expand "ball" )"2" "x!3" )"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 )"2" "2" expand "null_set?" )"2" assert )"2" case "FORALL (n, m,k: nat): n<=k=>subset?(H(n)(m), H(k)(m))" )"1" "1" "m_decreasing_convergence" "E" "HH" ))"1" "decreasing?(HH)" )"1" "mu_fin?[T, S, m](HH(0))" )"1" expand "x_converges?" "1" expand "o" "1" "(FORALL (i:nat): m(HH(i))`1)" )"1" "1" expand "DIVERGENT" )"1" "m(IIntersection(HH))`1" )"1" expand "mu_fin?" )"1" assert )"1" "mH" "lambda n: m(HH(n))`2" )"1" "bounded_below_is_convergent" "u" "mH" ))"1" "1" "convergent(mH)" )"1" case "forall n: mH(n) <= M / (1 + n)" )"1" expand "mu" "1" replace "1" "1" rewrite "limit_def" "1" expand "convergent_downto?" )"1" expand "converges_downto?" )"1" "1" "1" expand "convergence" )"1" "1" "0" )"1" expand "mH" "1" case "0<=M" )"1" "1" expand "<=" "1" "1" "posreal_div_posreal_is_posreal" "px" "epsilon!1" "py" "M" ))"1" "archimedean" "px" "epsilon!1 / M" ))"1" "1" "n!1-1" )"1" "n!1-1" )"1" assert )"1" "1" expand "decreasing?" )"1" "n!1-1" "i!1" )"1" assert )"1" expand "abs" )"1" assert )"1" rewrite "div_mult_pos_lt2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil )"2" assert )nil nil ))nil )"2" replace "2" "0" )"2" "2" expand "mH" )"2" expand "abs" )"2" assert )"2" "i!1" )"2" "m(HH(i!1))`2" )"2" assert )nil nil ))nil ))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 )"2" "2" "2" expand "convergent_downto?" )"2" "2" rewrite "converges_downto_def" "2" "2" "_" "n!1" )"2" "RHS" "M / (1 + n!1)" )"2" "2" "m_increasing_convergence" "E" "lambda n: H(n)(n!1)" ))"1" "increasing?(LAMBDA n: H(n)(n!1))" )"1" expand "o " )"1" expand "x_converges?" )"1" "_" "n!1" )"1" replace "1" "convergent(LAMBDA i: m(H(i)(n!1))`2)" )"1" "1" expand "mH" )"1" expand "HH" )"1" replace "1" "UU" "LAMBDA (i:nat): m(H(i)(n!1))`2" )"1" case "increasing?(UU)" )"1" case "forall n: UU(n)<=RHS" )"1" "1" "increasing_bounded_convergence" "v1" "UU" ))"1" "1" rewrite "limit_def" "1" replace "1" "1" rewrite "supfun_is_sup2" )nil nil ))nil ))nil ))nil )"2" nil nil ))nil )"2" "2" expand "bounded_above?" )"2" "RHS" )nil nil ))nil ))nil ))nil ))nil )"2" "2" expand "UU" )"2" "n!2" )"2" expand "mu" )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "increasing?" )"2" "2" expand "UU" )"2" "x!2" "y!1" )"2" assert )"2" "x!2" "n!1" )"2" "y!1" "n!1" )"2" "y!1" )"2" "m_monotone" "a" "H(x!2)(n!1)" "b" "H(y!1)(n!1)" ))"1" assert )"1" expand "x_le" )"1" nil nil ))nil ))nil )"2" nil nil )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "i!1" "n!1" )"2" expand "measurable_set?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "bounded_above_is_convergent" "u" "LAMBDA n: m(H(n)(n!1))`2" ))"1" "1" "1" expand "convergent_upto?" )"1" expand "converges_upto?" )"1" "1" rewrite "metric_convergence_def" )"1" "1" expand "metric_converges_to" )"1" expand "ball" )"1" assert )"1" expand "convergent?" )"1" expand "convergence" )"1" "x!2" )"1" "1" "epsilon!1" )"1" "1" "n!2" )"1" "1" "i!1" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "bounded_above?" )"2" "RHS" )"2" "2" "x!2" )"2" expand "mu" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" expand "increasing?" )"3" "i!1" "j!1" ))"3" "3" "i!1" "j!1" )"3" assert )"3" "i!1" "n!1" )"3" "j!1" "n!1" )"3" "m_monotone" "a" "H(i!1)(n!1)" "b" "H(j!1)(n!1)" ))"1" assert )"1" expand "x_le" )"1" "j!1" )nil nil ))nil ))nil )"2" nil nil )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "n!2" "n!1" )"2" expand "measurable_set?" )"2" nil nil ))nil ))nil ))nil ))nil )"3" "3" "i!1" "n!1" )"3" expand "measurable_set?" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "increasing?" )"2" "2" "x!2" "n!1" "y!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "n!2" "n!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "convergent_downto?" )"2" "2" expand "converges_downto?" )"2" "2" rewrite "metric_convergence_def" )"2" expand "metric_converges_to" )"2" assert )"2" expand "ball" )"2" "2" expand "convergent?" )"2" expand "convergence" )"2" "x!1" )"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 ))nil ))nil ))nil )"2" expand "bounded_below?" )"2" "0" )"2" "2" expand "mH" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"3" "3" expand "decreasing?" )"3" "i!1" "j!1" ))"3" "i!1" "j!1" )"3" assert )"3" "3" assert )"3" "3" "i!1" )"3" "j!1" )"3" "i!1" )"3" "j!1" )"3" "m_monotone" "a" "HH(j!1)" "b" "HH(i!1)" ))"1" assert )"1" expand "x_le" )"1" expand "mH" )"1" nil nil ))nil ))nil ))nil )"2" nil nil )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "n!1" )"2" expand "measurable_set?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "mu_fin?" )"2" "m_monotone" "a" "IIntersection(HH)" "b" "HH(0)" ))"1" "1" expand "x_le" )"1" assert )nil nil ))nil )"2" "2" expand "subset?" )"2" expand "IIntersection" )"2" expand "member" )"2" "2" "0" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "0" )nil nil )"3" nil nil ))nil ))nil ))nil )"3" expand "measurable_set?" )"3" nil nil ))nil ))nil ))nil ))nil )"2" "2" expand "decreasing?" )"2" "0" "i!1" )"2" assert )"2" "m_monotone" "a" "HH(i!1)" "b" "HH(0)" ))"1" assert )"1" "1" expand "mu_fin?" )"1" expand "x_le" )"1" nil nil ))nil ))nil ))nil ))nil )"2" "i!1" )nil nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "i!1" )"3" expand "measurable_set?" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "HH" )"2" "_" "0" )"2" "_" "0" )"2" "_" "0" )"2" assert )"2" "m_increasing_convergence" "E" "LAMBDA n: H(n)(0)" ))"1" "increasing?(LAMBDA n: H(n)(0))" )"1" expand "o" "1" expand "x_converges?" )"1" expand "mu_fin?" "1" replace "1" replace "1" "1" "1" "mH" "LAMBDA n: m(H(n)(0))`2" )"1" case "increasing?(mH)" )"1" case "forall n: mH(n)<=M" )"1" "1" "bounded_above_is_convergent" "u" "mH" ))"1" assert )"1" "1" expand "convergent_upto?" )"1" "1" expand "converges_upto?" )"1" rewrite "metric_convergence_def" )"1" expand "metric_converges_to" )"1" expand "ball" )"1" expand "member" )"1" assert )"1" "1" expand "convergent?" )"1" expand "convergence" )"1" "x!1" )"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 ))nil )"2" "2" expand "bounded_above?" )"2" "M" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "n!1" )"2" expand "mu" )"2" expand "mH" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "increasing?" )"2" "i!1" "j!1" ))"2" "2" "i!1" "j!1" )"2" assert )"2" expand "mH" )"2" "i!1" )"2" "j!1" )"2" "i!1" )"2" "j!1" )"2" "m_monotone" "a" "H(i!1)(0)" "b" "H(j!1)(0)" ))"1" assert )"1" expand "x_le" )"1" nil nil ))nil ))nil )"2" nil nil )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "n!1" )"2" expand "measurable_set?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "increasing?" )"2" "i!1" "j!1" ))"2" "2" "i!1" "0" "j!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "0" )nil nil ))nil )"2" "2" expand "decreasing?" )"2" "i!1" "j!1" ))"2" "2" expand "subset?" )"2" "2" expand "pointwise_increasing?" )"2" "x!1" )"2" assert )"2" expand "HH" )"2" expand "IUnion" )"2" "2" expand "H" )"2" expand "increasing?" )"2" "i!2" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "subset?" )"2" expand "member" )"2" expand "H" )"2" "2" expand "pointwise_increasing?" )"2" "x!1" )"2" expand "increasing?" )"2" "n!1" "k!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "n!1" "m!1" )"2" "n!1" )"2" "div_mult_pos_le2" "py" "m!1 + 1" "x" "mu(H(n!1)(m!1))" "z" "M" ))"2" assert )"2" assert )"2" rewrite "integral_nn" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "HH" )"2" expand "IUnion" )"2" expand "subset?" )"2" expand "member" )"2" "2" "n!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "n!1" "m!1" "_" )"2" "2" "nn_integrable_le" "g" "(m!1 + 1) * phi(H(n!1)(m!1))" "f" "F!2(n!1)" ))"1" "1" "1" "isf_phi" "E" "H(n!1)(m!1)" ))"1" "isf_scal" "c" "m!1+1" "i" "phi[T, S](H(n!1)(m!1))" ))"1" "RHS" "nn_integral(F!2(n!1))" )"1" rewrite "integral_nn" "1" rewrite "integral_scal" "1" rewrite "integral_phi" "1" assert )nil nil ))nil )"2" "2" "nn_isf_is_nn_integrable" )"2" "phi[T, S](H(n!1)(m!1))" )"1" "1" "nn_integrable_is_nn_integrable" )"1" "nn_integrable_is_integrable" )"1" "phi[T, S](H(n!1)(m!1))" )nil nil ))nil ))nil ))nil )"2" expand "nn_isf?" )"2" "2" "2" expand "phi" )"2" expand "member" )"2" "H(n!1)(m!1)(x!1)" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil )"2" "n!1" "m!1" )nil nil ))nil ))nil )"2" "2" "x!1" )"2" assert )"2" "2" expand "*" )"2" expand "phi" )"2" expand "member" )"2" "H(n!1)(m!1)(x!1)" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "scal_measurable" )"2" "phi_is_simple" "X" "H(n!1)(m!1)" ))"2" rewrite "simple_is_measurable" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "n!1" "m!1" )"3" "n!1" "m!1" )"3" expand "measurable_set?" )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "phi" )"2" expand "H" )"2" expand "member" )"2" expand "*" )"2" "F!2(n!1)(x!1) >= 1 + m!1" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "H" )"2" "n!1" "m!1" )"2" "integrable_nz_finite" "f" "F!2(n!1)" "epsilon" "m!1+1/2" ))"2" "2" "{x: T | abs(F!2(n!1)(x)) >= m!1 + 1 / 2}={x | F!2(n!1)(x) >= m!1 + 1 / 2}" )"1" "1" "m_monotone" "a" "{x | F!2(n!1)(x) >= 1 + m!1}" "b" "{x | F!2(n!1)(x) >= m!1 + 1 / 2}" ))"1" "1" expand "x_le" )"1" expand "mu_fin?" )"1" assert )nil nil ))nil ))nil )"2" "2" expand "subset?" )"2" expand "member" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil )"3" nil nil ))nil ))nil )"2" "2" expand "abs" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (propax) nil nil ))nil )"2" "2" "2" "1" "1" expand "IIntersection" )"1" "1" expand "HH" )"1" expand "IUnion" )"1" expand "H" )"1" "1+i!1" )"1" "1" "n!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "IIntersection" )"2" expand "HH" )"2" expand "IUnion" )"2" expand "H" )"2" "k!1" )"2" "k!1-1" )"2" "2" "i!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil )"2" "2" "2" expand "HH" )"2" rewrite "measurable_IUnion" )"2" "2" "n!1" "m!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "measurable_set?" )"2" expand "H" )"2" "F!2(n!1)" )"2" "nn_integrable_is_measurable" )"2" "F!2(n!1)" )"2" rewrite "measurable_ge" )"2" "1+m!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.708Angebot
(Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können 2026-04-25)
¤ *Eine klare Vorstellung vom Zielzustand
