Impressum finite_fubini_tonelli.prf
Sprache: Lisp
(finite_fubini_tonellinil 3458551591"" (typepred "S1" )"" (expand "sigma_algebra?" )"" (expand "subset_algebra_empty?" )"" (flatten)"" (expand "member" ) (("" (propax) nil nil )) nil )) nil ))nil ))nil ))nil )"bool" sets nil )"bool" subset_algebra_def nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil finite_fubini_tonelli nil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def nil )nil subset_algebra_def nil )"sigma_algebra[T1]" finite_fubini_tonellinil ))nil ))nil 3458551591"" (typepred "S2" )"" (expand "sigma_algebra?" )"" (expand "subset_algebra_empty?" )"" (flatten)"" (expand "member" ) (("" (propax) nil nil )) nil )) nil ))nil ))nil ))nil )"bool" sets nil )"bool" subset_algebra_def nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil finite_fubini_tonelli nil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def nil )nil subset_algebra_def nil )"sigma_algebra[T2]" finite_fubini_tonellinil ))nil ))nil 3458552933"" (skosimp)"" (split)"1" (flatten)"1" (typepred "h!1" )"1" (expand "nn_measurable?" )"1" (flatten)"1" "nn_integrable_is_nn_integrable" ("f" "h!1" ))"1" (split)"1" (hide -4)"1" (lemma "nn_integral_def" ("f" "h!1" ))"1" (skolem - "HH" )"1" (flatten)"1" (typepred "HH" )"1" (case "FORALL (n: nat): isf?(HH(n))" )"1" case "FORALL (n: nat,z:[T1,T2]): HH(n)(z)>=0" )"1" "FF" "lambda (n:nat): lambda (x:T1): isf_integral(lambda (y:T2): HH(n)(x,y))" )"1" case "FORALL (n: nat): integrable?[T1, S1, to_measure(mu)](FF(n))" )"1" case "forall (n:nat): integral[T1,S1,to_measure(mu)](FF(n))=integral[[T1,T2],sigma_times(S1,S2),to_measure(fm_times(mu,nu))](HH(n))" )"1" "(isf_integral o HH)=integral o FF" )"1" case "forall (n:nat,x:T1): FF(n)(x)>=0" )"1" case "pointwise_increasing?(FF)" )"1" case "bounded?(integral o FF)" )"1" "monotone_convergence[T1, S1, to_measure(mu)]" "F" "FF" ))"1" "1" "1" "1" "1" "F" )"1" "F" )"1" assert )"1" "F" )"1" expand "integrable1?" )"1" expand "ae_convergence?" )"1" expand "fullset" )"1" expand "ae_convergence_in?" )"1" expand "ae_in?" )"1" "1" expand "member" )"1" "E!1" )"1" expand "negligible_set?" )"1" "N1" )"1" "1" "N1" "F" )"1" "1" expand "subset?" )"1" "x!1" )"1" expand "member" )"1" "x!1" )"1" assert )"1" "monotone_convergence_scaf[T2,S2,to_measure(nu)]" "f" "LAMBDA (y: T2): h!1(x!1, y)" "F" "lambda (n:nat): lambda (y:T2): HH(n)(x!1,y)" ))"1" "1" "1" replace "1" "LHS" "integral(LAMBDA (y: T2): h!1(x!1, y))" )"1" "(integral o LAMBDA (n: nat): LAMBDA (y: T2): HH(n)(x!1, y)))=LAMBDA (n:nat): FF(n)(x!1)") "1" expand "converges_upto?" )"1" "1" "1" "hausdorff_convergence.unique_limit" "u" "LAMBDA (n: nat): FF(n)(x!1)" "l1" "LHS" "l2" "F(x!1)" ))"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "1" expand "FF" "1" expand "o" "1" "x!2" )"1" "isf_x_section" "x" "x!1" "i" "HH(x!2)" ))"1" rewrite "isf_integral" nil nil ))nil ))nil ))nil ))nil )"2" "2" "n!1" )"2" "isf_x_section" "x" "x!1" "i" "HH(n!1)" ))"2" "isf_is_integrable[T2, S2, to_measure(nu)]" )"2" "LAMBDA (y: T2): HH(n!1)(x!1, y)" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "increasing_nn_isf?" )"2" expand "pointwise_converges_upto?" )"2" "1" expand "pointwise_convergence?" )"1" "y!1" )"1" "(x!1,y!1)" )nil nil ))nil ))nil )"2" expand "pointwise_increasing?" )"2" "y!1" )"2" "(x!1,y!1)" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" replace "3" "3" expand "FF" )"3" expand "o " )"3" expand "pointwise_increasing?" )"3" "x!1" )"3" "3" expand "bounded?" )"3" "1" expand "bounded_above?" )"1" "F(x!1)" )"1" "n!1" )"1" "n!1" )"1" "isf_x_section" "i" "HH(n!1)" "x" "x!1" ))"1" rewrite "isf_integral" )"1" rewrite "metric_convergence_def" )"1" expand "metric_converges_to" )"1" "isf_integral(LAMBDA (y: T2): HH(n!1)(x!1, y))-F(x!1)" )"1" "1" "n!1+n!2" )"1" assert )"1" expand "ball" )"1" expand "increasing?" )"1" "n!1" "n!1+n!2" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"2" "2" rewrite "isf_x_section" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "bounded_below?" )"2" "0" )"2" "n!1" )"2" "n!1" )"2" "isf_x_section" "i" "HH(n!1)" "x" "x!1" ))"2" rewrite "isf_integral" "2" "n!1" "x!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "n!1" )"2" "isf_x_section" "i" "HH(n!1)" "x" "x!1" ))"2" "isf_is_integrable[T2, S2, to_measure(nu)]" )"2" "LAMBDA (y: T2): HH(n!1)(x!1, y)" )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 "bounded?" )"2" "2" "1" expand "bounded_above?" )"1" "c!1" )"1" "n!1" )"1" "n!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" expand "bounded_below?" )"2" "-c!1" )"2" "n!1" )"2" "n!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "ae_increasing?" )"2" "emptyset" )"2" "2" expand "pointwise_increasing?" )"2" "x!1" )"2" expand "increasing?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace -3 * rl)"2" "2" expand "bounded?" )"2" "nn_integral(h!1)" )"2" "n!1" )"2" "isf_integral_pos" "i" "HH(n!1)" ))"2" "1" expand "abs" "1" assert )"1" expand "o" "1" rewrite "metric_convergence_def" )"1" expand "metric_converges_to" )"1" "isf_integral(HH(n!1))-nn_integral(h!1)" )"1" "1" "n!1+n!2" )"1" assert )"1" expand "ball" )"1" expand "increasing_nn_isf?" )"1" expand "pointwise_increasing?" )"1" "n!1" )"1" "n!1+n!2" )"1" case "isf_integral(HH(n!1)) <= isf_integral(HH(n!1+n!2))" )"1" expand "o " )"1" assert )nil nil ))nil )"2" assert )"2" "2" "isf_integral_le" "i1" "HH(n!1)" "i2" "HH(n!1 + n!2)" ))"2" assert )"2" "z!1" )"2" "z!1" )"2" expand "increasing?" )"2" "n!1" "n!1+n!2" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "z!1" )"2" "n!1" "z!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "increasing_nn_isf?" )"2" "2" expand "FF" )"2" expand "pointwise_increasing?" )"2" "2" expand "increasing?" )"2" "i!1" "j!1" ))"2" "2" "j!1" )"2" "i!1" )"2" "isf_x_section" "x" "x!1" "i" "HH(j!1)" ))"2" "isf_x_section" "x" "x!1" "i" "HH(i!1)" ))"2" "isf_integral_le" "i1" "LAMBDA (y: T2): HH(i!1)(x!1, y)" "i2" "LAMBDA (y: T2): HH(j!1)(x!1, y)" ))"1" assert )"1" "y!1" )"1" "(x!1,y!1)" )"1" "i!1" "j!1" )"1" assert )nil 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 )"2" "2" expand "FF" 1)"2" "2" "n!1" )"2" "isf_x_section" "x" "x!1" "i" "HH(n!1)" ))"2" "isf_integral_pos" "i" "LAMBDA (y: T2): HH(n!1)(x!1, y)" ))"1" assert )"1" "y!1" )"1" "n!1" "(x!1,y!1)" )nil nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "o" )"2" "x!1" )"2" replace -1)"2" "x!1" )"2" rewrite "isf_integral" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "n!1" )"2" expand "FF" )"2" "n!1" )"2" rewrite "isf_integral[[T1, T2], sigma_times(S1, S2), to_measure(fm_times(mu, nu))]" "2" "isf_fubini_tonelli_3" "i" "HH(n!1)" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (propax) nil nil ))nil )"2" "2" expand "FF" )"2" "n!1" )"2" rewrite "isf_integral_x" )"2" "(LAMBDA (x: T1, y: T2): HH(n!1)(x, y))=HH(n!1)" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "n!1" )"2" rewrite "isf_x_section" )nil nil ))nil ))nil ))nil )"2" "2" "HH(n!1)" )"2" expand "nn_isf?" )"2" (inst - "z!1" ) nil nil ))nil ))nil ))nil ))nil )"2" "2" "HH(n!1)" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil )"2" (skosimp)"2" (inst - "x!1" ) (("2" (assert ) nil nil )) nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (expand "integrable1?" )"2" (skolem - ("N!1" "f!1" ))"2" (expand "member" )"2" (typepred "N!1" )"2" (name "N" "complement(N!1)" )"2" "NN" "cross_product(complement(N!1),fullset[T2])" )"2" "sigma_algebra_complement[T1,S1]" "x" "N!1" ))"1" (expand "member" )"1" (replace -3)"1" "cross_product_is_sigma_times" "Y" "fullset[T2]" "X" "N" ))"1" (name "H" "*[[T1,T2]](phi(NN),h!1)" )"1" "F" "*[T1](phi(N),f!1)" )"1" case "forall (x:T1): integrable?(LAMBDA (y: T2): H(x, y))" )"1" case "forall (x:T1): integral(LAMBDA (y: T2): H(x, y))=F(x)" )"1" "1" case "integrable?(F)" )"1" case "forall (x:T1): F(x)>=0" )"1" case "forall (z:[T1,T2]): H(z)>=0" )"1" case "nn_integrable?(H)" )"1" "integral_ae_eq" "f" "H" "h" "h!1" ))"1" assert )"1" "1" expand "ae_eq?" )"1" expand "restrict" )"1" expand "pointwise_ae?" )"1" expand "ae?" )"1" expand "fullset" "1" expand "H" )"1" expand "*" )"1" expand "ae_in?" )"1" expand "member" )"1" "cross_product(N!1,fullset[T2])" )"1" "y!1" )"1" "1" expand "NN" )"1" expand "fullset" )"1" expand "complement" )"1" expand "cross_product" )"1" expand "phi" )"1" expand "member" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "negligible_set?" )"2" "cross_product[T1, T2](N!1, fullset[T2])" )"2" "1" "1" expand "null_set?" )"1" expand "mu_fin?" )"1" expand "to_measure" )"1" expand "mu" )"1" expand "to_measure" )"1" "1" expand "measurable_set?" )"1" rewrite "cross_product_is_sigma_times" )"1" expand "fm_times" )"1" "rectangle_measure1" "M" "cross_product[T1, T2](N!1,fullset[T2])" "Y" "fullset[T2]" "X" "N!1" "mu" "mu" "nu" "nu" ))"1" assert )nil nil )"2" rewrite "cross_product_is_sigma_times" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "subset?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "h!1" )"2" expand "nn_measurable?" )"2" nil nil ))nil ))nil )"3" "nn_integrable_is_integrable[[T1, T2], sigma_times(S1, S2), to_measure(fm_times(mu, nu))]" )"3" "H" )nil nil ))nil ))nil )"2" "2" case "nn_measurable?(H)" )"1" "1" "nn_integrable_is_nn_integrable" "f" "F" ))"1" replace -4)"1" "nn_measurable_def" "f" "H" ))"1" "1" "1" "1" "1" "HH" )"1" "HH" )"1" "1" case "forall (n:nat): isf?(HH(n))" )"1" case "forall (n:nat,z:[T1, T2]): HH(n)(z) >= 0" )"1" "FF" "lambda (n:nat): lambda (x:T1): isf_integral(LAMBDA (y: T2): HH(n)(x, y))" )"1" case "forall (n:nat): integrable?(FF(n))" )"1" case "pointwise_increasing?(FF)" )"1" case "pointwise_converges_upto?(FF, F)" )"1" case "bounded?(integral o HH)" )"1" "monotone_convergence_scaf[[T1, T2], sigma_times(S1, S2), " "F" "HH" "f" "H" ))"1" assert )"1" "1" "1" "nn_integrable_is_nn_integrable" "f" "H" ))"1" replace "1" nil nil ))nil ))nil ))nil )"2" "2" expand "bounded?" )"2" "2" "1" expand "bounded_above?" )"1" "c!1" )"1" "1" "x!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" expand "bounded_below?" )"2" "-c!1" )"2" "2" "x!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "integral o HH=isf_integral o HH" )"1" expand "bounded?" )"1" "integral(F)" )"1" "n!1" )"1" expand "o " )"1" expand "abs" )"1" "isf_integral_pos" "i" "HH(n!1)" ))"1" "n!1" "_" )"1" replace "1" assert )"1" "1" rewrite "isf_fubini_tonelli_3" )"1" "integral_ae_le" "f1" "FF(n!1)" "f2" "F" ))"1" "1" expand "FF" )"1" nil nil ))nil )"2" "2" expand "pointwise_converges_upto?" )"2" expand "pointwise_increasing?" )"2" expand "pointwise_convergence?" )"2" expand "ae_le?" )"2" expand "pointwise_ae?" )"2" expand "ae?" )"2" expand "fullset" )"2" expand "ae_in?" )"2" "emptyset" )"2" "2" "2" "x!1" )"2" "x!1" )"2" rewrite "metric_convergence_def" )"2" expand "metric_converges_to" )"2" assert )"2" "FF(n!1)(x!1)-F(x!1)" )"2" "2" expand "increasing?" )"2" "n!1+n!2" )"2" "n!1" "n!1+n!2" )"2" expand "ball" )"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" "n!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "n!1" )nil nil ))nil ))nil ))nil ))nil )"2" "integral_nonneg" "f" "F" ))"2" assert )nil nil ))nil ))nil ))nil )"2" "2" "2" expand "o " )"2" "x!1" )"2" rewrite "isf_integral" )nil nil ))nil ))nil ))nil ))nil ))nil )"3" "n!1" )"3" "n!1" )"3" "isf_is_integrable[[T1, T2], sigma_times(S1, S2), to_measure(fm_times(mu, nu))]" )"3" "HH(n!1)" )nil nil ))nil ))nil ))nil ))nil )"2" expand "pointwise_converges_upto?" )"2" assert )"2" "2" expand "pointwise_convergence?" )"2" "2" "x!1" )"2" "x!1" )"2" replace "2" expand "FF" "2" "monotone_convergence_scaf[T2,S2,to_measure(nu)]" "f" "LAMBDA (y: T2): H(x!1, y)" "F" "lambda (n:nat): lambda (y:T2): HH(n)(x!1, y)" ))"1" "1" "1" expand "converges_upto?" )"1" "1" expand "o" )"1" "(LAMBDA (x_1: nat): LAMBDA (y: T2): HH(x_1)(x!1, y)))=LAMBDA (n:nat): isf_integral(LAMBDA (y: T2): HH(n)(x!1, y))") "1" "1" "x!2" )"1" "isf_x_section" "x" "x!1" "i" "HH(x!2)" ))"1" rewrite "isf_integral" nil nil )"2" nil nil ))nil ))nil )"2" "2" "n!1" )"2" rewrite "isf_x_section" )nil nil ))nil ))nil )"3" "n!1" )"3" "n!1" )"3" "isf_x_section" "x" "x!1" "i" "HH(n!1)" ))"1" "isf_is_integrable[T2, S2, to_measure(nu)]" )"1" "LAMBDA (y: T2): HH(n!1)(x!1, y)" )nil nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil )"2" "2" "n!1" )"2" rewrite "isf_x_section" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "pointwise_converges_upto?" )"2" "1" expand "pointwise_convergence?" )"1" "y!1" )"1" "(x!1,y!1)" )nil nil ))nil ))nil )"2" expand "pointwise_increasing?" )"2" "y!1" )"2" "(x!1,y!1)" )nil nil ))nil ))nil ))nil ))nil ))nil )"3" "3" expand "bounded?" )"3" expand "o" )"3" "1" expand "bounded_above?" )"1" "F(x!1)" )"1" "n!1" )"1" "integral_ae_le[T2,S2,to_measure(nu)]" "f1" "LAMBDA (y: T2): HH(n!1)(x!1, y)" "f2" "LAMBDA (y: T2): H(x!1,y)" ))"1" "1" assert )nil nil )"2" "2" expand "increasing_nn_simple?" )"2" "2" "2" expand "pointwise_increasing?" )"2" expand "ae_le?" )"2" expand "pointwise_ae?" )"2" expand "ae?" )"2" expand "fullset" )"2" expand "ae_in?" )"2" "emptyset" )"2" "y!1" )"2" expand "member" )"2" "2" "2" "(x!1,y!1)" )"2" "(x!1,y!1)" )"2" rewrite "metric_convergence_def" )"2" expand "metric_converges_to" )"2" "HH(n!1)(x!1, y!1)-H(x!1, y!1)" )"1" "1" "n!1+n!2" )"1" expand "ball" )"1" expand "increasing?" )"1" "n!1" "n!1+n!2" )"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 ))nil ))nil ))nil ))nil ))nil )"2" nil nil )"3" "isf_x_section" "x" "x!1" "i" "HH(n!1)" ))"1" "isf_is_integrable[T2, S2, to_measure(nu)]" )"1" "LAMBDA (y: T2): HH(n!1)(x!1, y)" )nil nil ))nil )"2" "n!1" )nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "bounded_below?" )"2" "0" )"2" "n!1" )"2" "n!1" )"2" "isf_x_section" "x" "x!1" "i" "HH(n!1)" ))"1" rewrite "isf_integral" "1" "isf_integral_pos" "i" "LAMBDA (y: T2): HH(n!1)(x!1, y)" ))"1" assert )"1" "y!1" )"1" "n!1" "(x!1,y!1)" )nil nil ))nil ))nil )"2" nil nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "n!1" )"2" "isf_x_section" "x" "x!1" "i" "HH(n!1)" ))"1" "isf_is_integrable[T2, S2, to_measure(nu)]" )"1" "LAMBDA (y: T2): HH(n!1)(x!1, y)" )nil nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "increasing_nn_simple?" )"2" "2" expand "pointwise_increasing?" )"2" "2" expand "FF" )"2" "2" expand "increasing?" )"2" "i!1" "j!1" ))"2" "2" "j!1" )"2" "i!1" )"2" "isf_x_section" "x" "x!1" "i" "HH(j!1)" ))"1" "isf_x_section" "x" "x!1" "i" "HH(i!1)" ))"1" "isf_integral_le" "i1" "LAMBDA (y: T2): HH(i!1)(x!1, y)" "i2" "LAMBDA (y: T2): HH(j!1)(x!1, y)" ))"1" assert )"1" "y!1" )"1" "(x!1,y!1)" )"1" "i!1" "j!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" nil nil )"3" nil nil ))nil )"2" nil nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "FF" )"2" "n!1" )"2" "isf_integral_x" "i" "HH(n!1)" ))"1" nil nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "n!1" )"2" rewrite "isf_x_section" )nil nil ))nil ))nil ))nil )"2" "2" expand "increasing_nn_simple?" )"2" expand "nn_simple?" )"2" "2" "n!1" )"2" "2" "z!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "increasing_nn_simple?" )"2" "2" "n!1" )"2" expand "nn_simple?" )"2" "2" expand "isf?" )"2" expand "mu_fin?" )"2" expand "to_measure" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "nn_measurable?" )"2" nil nil ))nil ))nil ))nil ))nil )"2" "2" "x!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil )"2" "2" "h!1" )"2" expand "nn_measurable?" )"2" "2" "1" expand "H" )"1" rewrite "prod_measurable" )"1" "phi_is_simple[[T1, T2], sigma_times(S1, S2)]" "X" "NN" ))"1" expand "simple?" )"1" nil nil ))nil ))nil ))nil ))nil )"2" "2" "x!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (propax) nil nil ))nil )"2" "2" expand "H" )"2" "h!1" )"2" expand "nn_measurable?" )"2" "2" "z!1" )"2" expand "*" )"2" expand "phi" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "x!1" )"2" "x!1" )"2" "integral_nonneg" "f" "LAMBDA (y: T2): H(x!1, y)" ))"1" assert )"1" "y!1" )"1" expand "H" )"1" expand "*" )"1" expand "phi" )"1" "1" "h!1" )"1" expand "nn_measurable?" )"1" "1" "(x!1,y!1)" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "f!1" )"2" expand "F" )"2" rewrite "indefinite_integrable" )nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" "x!1" )"2" "x!1" )"2" expand "H" )"2" expand "F" )"2" expand "*" )"2" expand "phi" )"2" expand "NN" )"2" expand "cross_product" )"2" expand "fullset" )"2" expand "complement" )"2" expand "member" )"2" expand "N" )"2" expand "complement" )"2" expand "member" )"2" "2" "N!1(x!1)" )"1" rewrite "integral_zero" )"1" assert )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 )"3" (propax) nil nil ))nil )"2" "2" expand "H" )"2" expand "NN" )"2" expand "cross_product" )"2" expand "fullset" )"2" expand "complement" )"2" expand "phi" )"2" expand "member" )"2" expand "*" )"2" "x!1" )"2" "N!1(x!1)" )"1" rewrite "integrable_zero" )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil )"2" (expand "null_set?" )"2" (expand "measurable_set?" )"2" (flatten) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil measure_space nil )"bool" measure_space nil )"sigma_algebra[T2]" finite_fubini_tonellinil )"sigma_algebra[T1]" finite_fubini_tonellinil )"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 reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil finite_fubini_tonelli nil )nil finite_fubini_tonelli nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil nn_integral nil )"bool" nn_integral nil )nil nn_integral nil )"[T, T -> boolean]" equalities nil )"real" isf nil )nil finite_fubini_scaf nil )"real" integral nil )"bool" sup_norm nil )"real" reals nil )"bool" product_integral_def nil )"set" sets nil )"bool" measure_theory nil )"bool" sets nil )"bool" booleans nil )nil nil )"bool" metric_space_def"metric_space/" )"bool" real_fun_preds "reals/" )"(strict_total_order?[real])" real_props nil )"set[T]" metric_space_def "metric_space/" )"[numfield, numfield -> numfield]" number_fields nil )"nonneg_int" nil )nil real_types nil )"bool" reals nil )"integrable[T1, S1, to_measure(mu)]" nil )"nat" finite_fubini_tonelli nil )"real" reals nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil metric_space"metric_space/" )"bool" real_fun_preds "reals/" )"bool" real_fun_preds "reals/" )"bool" real_fun_preds "reals/" )"bool" pointwise_convergencenil )"bool" pointwise_convergencenil )"T1" finite_fubini_tonelli nil )"increasing_nn_isf " nil )nil finite_fubini_scaf nil )nil integral nil )"[nat -> [T1 -> real]]" finite_fubini_tonellinil )nil integral nil )"nat" finite_fubini_tonelli nil )"bool" convergence_aux "metric_space/" )"setofsets[T]" metric_space_def"metric_space/" )"[numfield, numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )nil hausdorff_convergence "topology/" )"nat" finite_fubini_tonelli nil )"bool" sets nil )nil measure_theory nil )"set[T1]" finite_fubini_tonelli nil )"bool" measure_theory nil )nil measure_theory nil )"bool" measure_theory nil )set type-eq-decl nil sets nil )"bool" measure_theory nil )"bool" measure_theory nil )"bool" measure_theory nil )"set" sets nil )"finite_set" finite_sets nil )"finite_set[T]" countable_props"sets_aux/" )"finite_set[T]" countable_setofsets"sets_aux/" )"finite_set[T]" sigma_countable"sigma_set/" )"(S)" finite_fubini_tonellinil )"null_set" finite_fubini_tonelli nil )nil integral_convergence nil )"nnreal" nn_integral nil )nil isf nil )"bool" reals nil )nil isf nil )"nn_measurable[[T1, T2], sigma_times(S1, S2)]" nil )"nat" finite_fubini_tonelli nil )"bool" pointwise_convergence nil )"T3" function_props nil )nil finite_fubini_scaf nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"bool" isf nil )nil isf nil )"bool" nn_integral nil )nil nn_integral nil )nil sequences nil )"bool" nn_integral nil )nil nn_integral nil )nil integral nil )"bool" integral nil )nil integral nil )"bool" reals nil )nil real_types nil )"bool" generalized_measure_def nil )nil generalized_measure_defnil )nil extended_nnreal"extended_nnreal/" )"bool" generalized_measure_def nil )nil generalized_measure_defnil )"measure_type" generalized_measure_def nil )"finite_measure[[T1, T2], sigma_times(S1, S2)]" nil )"finite_measure[T1, S1]" nil )"finite_measure[T2, S2]" nil )"(S)" nil )"measurable_set" nil )"set" sets nil )nil sigma_algebra nil )"[T -> real]" real_fun_ops "reals/" )"nat" measure_space nil )nil integral nil )"(null_set?)" finite_fubini_tonelli nil )nil measure_space_def nil )nil integral nil )nil integral nil )"bool" measure_theory nil )"bool" measure_theory nil )"real" reals nil )"bool" measure_space_def nil )nil product_finite_measure nil )"nnreal" measure_props nil )"bool" measure_props nil )"set[[T1, T2]]" finite_fubini_tonelli nil )"null_set[T1, S1, to_measure(mu)]" nil )"[[T1, T2] -> real]" finite_fubini_tonellinil )"bool" measure_theory nil )"measurable_set[T, S]" nil )"(S)" finite_fubini_tonellinil )"R" restrict nil )nil measure_space_defnil )"bool" measure_space_def nil )nil integral nil )nil measure_space nil )"bool" measure_space nil )nil measure_space nil )"bool" measure_space nil )"nat" finite_fubini_tonelli nil )"T1" finite_fubini_tonelli nil )"nat" finite_fubini_tonelli nil )"null_set" finite_fubini_tonelli nil )"(S)" finite_fubini_tonellinil )"({x | TRUE})" finite_fubini_tonelli nil )"nat" finite_fubini_tonelli nil )nil integral nil )"[nat -> [T1 -> real]]" finite_fubini_tonellinil )"measurable_set[T, S]" nil )"(S)" finite_fubini_tonellinil )"bool" measure_theory nil )nil integral nil )"[T1 -> real]" finite_fubini_tonelli nil )"increasing_nn_simple[[T1, T2], sigma_times(S1, S2)]" nil )"nat" finite_fubini_tonelli nil )nil measure_space nil )"bool" measure_space nil )nil measure_space nil )nil integral nil )nil product_sigma nil )"measurable_set[T, S]" nil )"(S)" finite_fubini_tonellinil )"set[[T1, T2]]" cross_product"topology/" ))nil 3459084018"" (skosimp)"" (split)"1" (flatten)"1" (typepred "h!1" )"1" (expand "nn_measurable?" )"1" (flatten)"1" "nn_integrable_is_nn_integrable" ("f" "h!1" ))"1" (split)"1" (hide -4)"1" (lemma "nn_integral_def" ("f" "h!1" ))"1" (skolem - "HH" )"1" (flatten)"1" (typepred "HH" )"1" (case "FORALL (n: nat): isf?(HH(n))" )"1" case "FORALL (n: nat,z:[T1,T2]): HH(n)(z)>=0" )"1" "GG" "lambda (n:nat): lambda (y:T2): isf_integral(lambda (x:T1): HH(n)(x,y))" )"1" case "FORALL (n: nat): integrable?[T2, S2, to_measure(nu)](GG(n))" )"1" case "forall (n:nat): integral[T2,S2,to_measure(nu)](GG(n))=integral[[T1,T2],sigma_times(S1,S2),to_measure(fm_times(mu,nu))](HH(n))" )"1" "(isf_integral o HH)=integral o GG" )"1" "1" case "forall (n:nat,y:T2): GG(n)(y)>=0" )"1" case "pointwise_increasing?(GG)" )"1" case "bounded?(integral o GG)" )"1" "monotone_convergence[T2, S2, to_measure(nu)]" "F" "GG" ))"1" "1" "1" "1" "1" "G" )"1" "G" )"1" assert )"1" "G" )"1" expand "integrable2?" )"1" expand "ae_convergence?" )"1" expand "fullset" )"1" expand "ae_convergence_in?" )"1" expand "ae_in?" )"1" "1" "E!1" )"1" expand "negligible_set?" )"1" "N2" )"1" "1" "N2" "G" )"1" "1" expand "subset?" )"1" expand "member" )"1" "y!1" )"1" assert )"1" "y!1" )"1" assert )"1" "monotone_convergence_scaf[T1,S1,to_measure(mu)]" "f" "LAMBDA (x: T1): h!1(x, y!1)" "F" "lambda (n:nat): lambda (x:T1): HH(n)(x,y!1)" ))"1" "1" "1" replace "1" "LHS" "integral(LAMBDA (x: T1): h!1(x, y!1))" )"1" "(integral o LAMBDA (n: nat): LAMBDA (x: T1): HH(n)(x, y!1)))=LAMBDA (n:nat): GG(n)(y!1)") "1" "1" expand "converges_upto?" )"1" "1" "1" "hausdorff_convergence.unique_limit" "u" "LAMBDA (n: nat): GG(n)(y!1)" "l1" "LHS" "l2" "G(y!1)" ))"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" expand "GG" "1" expand "o" "1" "x!1" )"1" "isf_y_section" "y" "y!1" "i" "HH(x!1)" ))"1" rewrite "isf_integral" )nil nil ))nil ))nil ))nil ))nil )"2" "2" "n!1" )"2" "isf_y_section" "y" "y!1" "i" "HH(n!1)" ))"2" "isf_is_integrable[T1, S1, to_measure(mu)]" )"2" "LAMBDA (x: T1): HH(n!1)(x, y!1)" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "increasing_nn_isf?" )"2" expand "pointwise_converges_upto?" )"2" "1" expand "pointwise_convergence?" )"1" "1" "(x!1,y!1)" )nil nil ))nil ))nil )"2" expand "pointwise_increasing?" )"2" "2" "(x!1,y!1)" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" expand "bounded?" )"3" expand "o" )"3" "1" expand "bounded_above?" )"1" "G(y!1)" )"1" "n!1" )"1" expand "GG" )"1" expand "pointwise_increasing?" )"1" "y!1" )"1" rewrite "metric_convergence_def" )"1" expand "metric_converges_to" )"1" "n!1" )"1" "isf_y_section" "y" "y!1" "i" "HH(n!1)" ))"1" rewrite "isf_integral" "1" "isf_integral(LAMBDA (x: T1): HH(n!1)(x, y!1))-G(y!1)" )"1" "1" "n!1+n!2" )"1" assert )"1" expand "ball" )"1" expand "increasing?" )"1" "n!1" "n!1+n!2" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "isf_y_section" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "bounded_below?" )"2" "0" )"2" "n!1" )"2" "n!1" )"2" "isf_y_section" "y" "y!1" "i" "HH(n!1)" ))"2" rewrite "isf_integral" )"2" "isf_integral_pos" "i" "LAMBDA (x: T1): HH(n!1)(x, y!1)" ))"1" assert )"1" "1" assert )"1" "n!1" "(x!1,y!1)" )nil nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "n!1" )"2" "isf_y_section" "y" "y!1" "i" "HH(n!1)" ))"2" "isf_is_integrable[T1, S1, to_measure(mu)]" )"2" "LAMBDA (x: T1): HH(n!1)(x, y!1)" )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 "bounded?" )"2" "2" "1" expand "bounded_above?" )"1" "c!1" )"1" "n!1" )"1" "n!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" expand "bounded_below?" )"2" "-c!1" )"2" "n!1" )"2" "n!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "ae_increasing?" )"2" expand "pointwise_increasing?" )"2" expand "increasing?" )"2" "emptyset" )"2" "y!1" )"2" "y!1" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "bounded?" )"2" "nn_integral(h!1)" )"2" "n!1" )"2" expand "o " )"2" "integral_nonneg" "f" "GG(n!1)" ))"2" "n!1" "_" )"2" replace "2" expand "abs" )"2" assert )"2" rewrite "metric_convergence_def" )"2" expand "metric_converges_to" )"2" "integral(GG(n!1))-nn_integral(h!1)" )"2" "2" "n!1+n!2" )"2" assert )"2" expand "ball" )"2" expand "pointwise_increasing?" )"2" "n!1" )"2" "n!1+n!2" )"2" case "integral(GG(n!1)) <= integral(GG(n!1 + n!2))" )"1" assert )nil nil )"2" "2" "integral_ae_le" "f1" "GG(n!1)" "f2" "GG(n!1 + n!2)" ))"2" assert )"2" "2" expand "ae_le?" )"2" expand "pointwise_ae?" )"2" expand "ae?" )"2" expand "fullset" )"2" expand "ae_in?" )"2" "emptyset" )"2" "y!1" )"2" expand "member" )"2" "2" "y!1" )"2" expand "increasing?" )"2" "n!1" "n!1+n!2" )"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 )"2" expand "pointwise_increasing?" )"2" "y!1" )"2" expand "increasing_nn_isf?" )"2" expand "pointwise_increasing?" )"2" expand "increasing?" )"2" "i!1" "j!1" ))"2" "2" "2" expand "GG" )"2" "i!1" )"2" "j!1" )"2" "isf_y_section" "i" "HH(i!1)" "y" "y!1" ))"2" "isf_y_section" "i" "HH(j!1)" "y" "y!1" ))"2" "isf_integral_le" "i1" "LAMBDA (x: T1): HH(i!1)(x, y!1)" "i2" "LAMBDA (x: T1): HH(j!1)(x, y!1)" ))"1" assert )"1" "1" "(x!1,y!1)" )"1" "i!1" "j!1" )"1" assert )nil 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" "2" expand "GG" )"2" "n!1" "_" )"2" "n!1" )"2" "isf_y_section" "y" "y!1" "i" "HH(n!1)" ))"2" "isf_integral_pos" "i" "LAMBDA (x: T1): HH(n!1)(x, y!1)" ))"1" assert )"1" "1" "(x!1,y!1)" )nil nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "o " )"2" "x!1" )"2" replace -1)"2" "x!1" )"2" rewrite "isf_integral[[T1, T2], sigma_times(S1, S2), to_measure(fm_times(mu, nu))]" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "n!1" )"2" "n!1" )"2" "2" rewrite "isf_integral[[T1, T2], sigma_times(S1, S2), to_measure(fm_times(mu, nu))]" )"2" rewrite "isf_fubini_tonelli_4" "2" expand "GG" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (propax) nil nil ))nil )"2" "2" "2" expand "GG" )"2" rewrite "isf_integral_y" )"2" "(LAMBDA (x: T1, y: T2): HH(n!1)(x, y))=HH(n!1)" )"1" (assert ) nil nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "isf_y_section" )nil nil ))nil ))nil )"2" "2" "HH(n!1)" )"2" expand "nn_isf?" )"2" (inst - "z!1" ) nil nil ))nil ))nil ))nil ))nil )"2" "2" "HH(n!1)" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil )"2" (skosimp)"2" (inst - "x!1" ) (("2" (assert ) nil nil )) nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (expand "integrable2?" )"2" (skolem - ("N!1" "g!1" ))"2" (expand "member" )"2" (typepred "N!1" )"2" (name "N" "complement(N!1)" )"2" "NN" "cross_product(fullset[T1],complement(N!1))" )"2" "sigma_algebra_complement[T2,S2]" "x" "N!1" ))"1" (expand "member" )"1" (replace -3)"1" "cross_product_is_sigma_times" "X" "fullset[T1]" "Y" "N" ))"1" (replace -3)"1" "H" "*[[T1,T2]](phi(NN),h!1)" )"1" "G" "*[T2](phi(N),g!1)" )"1" case "forall (y:T2): integrable?(LAMBDA (x: T1): H(x, y))" )"1" case "forall (y:T2): integral(LAMBDA (x: T1): H(x, y))=G(y)" )"1" "1" case "integrable?(G)" )"1" case "forall (y:T2): G(y)>=0" )"1" case "forall (z:[T1,T2]): H(z)>=0" )"1" case "nn_integrable?(H)" )"1" "integral_ae_eq" "f" "H" "h" "h!1" ))"1" assert )"1" "1" expand "ae_eq?" )"1" expand "pointwise_ae?" )"1" expand "restrict" )"1" expand "ae?" )"1" expand "fullset" "1" expand "H" )"1" expand "*" )"1" expand "phi" )"1" expand "ae_in?" )"1" expand "member" )"1" "cross_product(fullset[T1], N!1)" )"1" "z!1" )"1" expand "NN" )"1" expand "fullset" )"1" expand "cross_product" )"1" expand "complement" )"1" expand "member" )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "negligible_set?" )"2" "cross_product[T1, T2](fullset[T1], N!1)" )"2" "1" "1" expand "null_set?" )"1" "1" expand "mu_fin?" )"1" expand "mu" )"1" expand "to_measure" )"1" "cross_product_is_sigma_times" "X" "fullset[T1]" "Y" "N!1" ))"1" expand "measurable_set?" )"1" assert )"1" expand "fm_times" )"1" "rectangle_measure1" "M" "cross_product[T1, T2](fullset[T1], N!1)" "X" "fullset[T1]" "Y" "N!1" "mu" "mu" "nu" "nu" ))"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "subset?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "h!1" )"2" expand "nn_measurable?" )"2" nil nil ))nil ))nil )"3" "nn_integrable_is_integrable[[T1, T2], sigma_times(S1, S2), to_measure(fm_times(mu, nu))]" )"3" "H" )nil nil ))nil ))nil )"2" "2" case "nn_measurable?(H)" )"1" "1" "nn_integrable_is_nn_integrable" "f" "G" ))"1" replace -4)"1" "nn_measurable_def" "f" "H" ))"1" "1" "1" "1" "HH" )"1" "HH" )"1" "1" case "forall (n:nat): isf?(HH(n))" )"1" case "forall (n:nat,z:[T1, T2]): HH(n)(z) >= 0" )"1" "GG" "lambda (n:nat): lambda (y:T2): isf_integral(LAMBDA (x: T1): HH(n)(x, y))" )"1" case "forall (n:nat): integrable?(GG(n))" )"1" case "pointwise_increasing?(GG)" )"1" case "pointwise_converges_upto?(GG, G)" )"1" case "bounded?(integral o HH)" )"1" "monotone_convergence_scaf[[T1, T2], sigma_times(S1, S2), " "F" "HH" "f" "H" ))"1" assert )"1" "1" "1" "nn_integrable_is_nn_integrable" "f" "H" ))"1" replace "1" nil nil ))nil ))nil ))nil )"2" "2" expand "o " )"2" assert )"2" expand "bounded?" )"2" "2" "1" expand "bounded_above?" )"1" "c!1" )"1" "n!1" )"1" "n!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" expand "bounded_below?" )"2" "-c!1" )"2" "n!1" )"2" "n!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "integral o HH=isf_integral o HH" )"1" "1" expand "bounded?" )"1" "integral(G)" )"1" "n!1" )"1" expand "o" "1" expand "abs" "1" "n!1" )"1" "isf_integral_pos" "i" "HH(n!1)" ))"1" "n!1" "_" )"1" replace "1" assert )"1" "1" rewrite "isf_fubini_tonelli_4" )"1" "integral_ae_le" "f1" "GG(n!1)" "f2" "G" ))"1" "1" expand "GG" "1" nil nil ))nil )"2" "2" "2" expand "ae_le?" )"2" expand "pointwise_ae?" )"2" expand "ae?" )"2" expand "fullset" )"2" expand "ae_in?" )"2" "emptyset" )"2" "y!1" )"2" expand "member" )"2" "2" expand "pointwise_converges_upto?" )"2" expand "pointwise_convergence?" )"2" expand "pointwise_increasing?" )"2" "y!1" )"2" "y!1" )"2" "y!1" )"2" "2" rewrite "metric_convergence_def" )"2" expand "metric_converges_to" )"2" expand "increasing?" )"2" "GG(n!1)(y!1)-G(y!1)" )"1" "1" "n!1+n!2" )"1" expand "ball" )"1" assert )"1" "n!1" "n!1+n!2" )"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 ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "n!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "integral_nonneg" "f" "G" ))"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "o " )"2" "x!1" )"2" rewrite "isf_integral" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "n!1" )"3" "n!1" )"3" "isf_is_integrable[[T1, T2], sigma_times(S1, S2), to_measure(fm_times(mu, nu))]" )"3" "HH(n!1)" )nil nil ))nil ))nil ))nil ))nil )"2" expand "pointwise_converges_upto?" )"2" assert )"2" "2" "2" expand "pointwise_convergence?" )"2" "y!1" )"2" "y!1" )"2" "y!1" )"2" replace "2" expand "GG" "2" "monotone_convergence_scaf[T1,S1,to_measure(mu)]" "f" "LAMBDA (x: T1): H(x, y!1)" "F" "lambda (n:nat): lambda (x:T1): HH(n)(x, y!1)" ))"1" "1" "1" expand "converges_upto?" )"1" "1" expand "o" "1" "(LAMBDA (x_1: nat): LAMBDA (x: T1): HH(x_1)(x, y!1)))=LAMBDA (n:nat): isf_integral(LAMBDA (x: T1): HH(n)(x, y!1))") "1" "1" "x!1" )"1" "isf_y_section" "y" "y!1" "i" "HH(x!1)" ))"1" rewrite "isf_integral" nil nil )"2" nil nil ))nil ))nil )"2" "2" "n!1" )"2" rewrite "isf_y_section" )nil nil ))nil ))nil )"3" "n!1" )"3" "n!1" )"3" "isf_y_section" "y" "y!1" "i" "HH(n!1)" ))"1" "isf_is_integrable" "x" "LAMBDA (x: T1): HH(n!1)(x, y!1)" ))"1" nil nil )"2" nil nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil )"2" "2" "n!1" )"2" rewrite "isf_y_section" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "pointwise_converges_upto?" )"2" "1" expand "pointwise_convergence?" )"1" "1" "(x!1,y!1)" )nil nil ))nil ))nil )"2" "2" expand "pointwise_increasing?" )"2" "2" "(x!1,y!1)" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" expand "bounded?" )"3" "1" expand "o" )"1" expand "bounded_above?" )"1" "G(y!1)" )"1" "n!1" )"1" "integral_ae_le[T1,S1,to_measure(mu)]" "f1" "LAMBDA (x: T1): HH(n!1)(x, y!1)" "f2" "LAMBDA (x: T1): H(x, y!1)" ))"1" assert )"1" "1" expand "ae_le?" )"1" expand "pointwise_ae?" )"1" expand "ae?" )"1" expand "fullset" )"1" expand "ae_in?" )"1" "emptyset" )"1" "1" expand "member" )"1" "1" expand "pointwise_increasing?" )"1" "(x!1,y!1)" )"1" "(x!1,y!1)" )"1" expand "increasing?" )"1" rewrite "metric_convergence_def" )"1" expand "metric_converges_to" )"1" "HH(n!1)(x!1, y!1)-H(x!1, y!1)" )"1" "1" "n!1+n!2" )"1" assert )"1" expand "ball" )"1" "n!1" "n!1+n!2" )"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 ))nil ))nil )"2" nil nil )"3" "n!1" )"3" "isf_y_section" "y" "y!1" "i" "HH(n!1)" ))"1" "isf_is_integrable[T1, S1, to_measure(mu)]" )"1" "LAMBDA (x: T1): HH(n!1)(x, y!1)" )nil nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "bounded_below?" )"2" "0" )"2" "n!1" )"2" expand "o " )"2" "n!1" )"2" "isf_y_section" "y" "y!1" "i" "HH(n!1)" ))"1" rewrite "isf_integral" "1" "isf_integral_pos[T1,S1,to_measure(mu)]" "i" "LAMBDA (x: T1): HH(n!1)(x, y!1)" ))"1" assert )"1" "1" "n!1" "(x!1,y!1)" )nil nil ))nil ))nil )"2" nil nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "n!1" )"2" "isf_y_section" "i" "HH(n!1)" "y" "y!1" ))"1" "isf_is_integrable" "x" "LAMBDA (x: T1): HH(n!1)(x, y!1)" ))"1" nil nil )"2" nil nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "increasing_nn_simple?" )"2" "2" expand "pointwise_increasing?" )"2" "y!1" )"2" expand "increasing?" )"2" "i!1" "j!1" ))"2" "2" expand "GG" )"2" "isf_integral_le" "i1" "LAMBDA (x: T1): HH(i!1)(x, y!1)" "i2" "LAMBDA (x: T1): HH(j!1)(x, y!1)" ))"1" assert )"1" "1" "1" "(x!1, y!1)" )"1" "i!1" "j!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "j!1" )"2" rewrite "isf_y_section" )nil nil ))nil )"3" "i!1" )"3" rewrite "isf_y_section" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "GG" )"2" "n!1" )"2" rewrite "isf_integral_y" )"2" "(LAMBDA (x: T1, y: T2): HH(n!1)(x, y))=HH(n!1)" )
Messung V0.5 in Prozent C=100 H=99 G=99
¤ Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.0.695Bemerkung:
(vorverarbeitet am 2026-05-01)
¤ *Bot Zugriff
2026-05-26
