| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/measure_integration/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 MB |
|
Quelle finite_fubini_tonelli.prfSprache: Lisp |
|||||||||||||||
|
(finite_fubini_tonelli (mu_TCC1 0 (mu_TCC1-1 nil 3458551591 ("" (typepred "S1") (("" (expand "sigma_algebra?") (("" (expand "subset_algebra_empty?") (("" (flatten) (("" (expand "member") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ((member const-decl "bool" sets nil) (subset_algebra_empty? const-decl "bool" subset_algebra_def nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (T1 formal-type-decl nil finite_fubini_tonelli nil) (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets nil) (sigma_algebra? const-decl "bool" subset_algebra_def nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil) (S1 formal-const-decl "sigma_algebra[T1]" finite_fubini_tonelli nil)) nil)) (nu_TCC1 0 (nu_TCC1-1 nil 3458551591 ("" (typepred "S2") (("" (expand "sigma_algebra?") (("" (expand "subset_algebra_empty?") (("" (flatten) (("" (expand "member") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ((member const-decl "bool" sets nil) (subset_algebra_empty? const-decl "bool" subset_algebra_def nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (T2 formal-type-decl nil finite_fubini_tonelli nil) (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets nil) (sigma_algebra? const-decl "bool" subset_algebra_def nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil) (S2 formal-const-decl "sigma_algebra[T2]" finite_fubini_tonelli nil)) nil)) (finite_fubini_tonelli_1 0 (finite_fubini_tonelli_1-1 nil 3458552933 ("" (skosimp) (("" (split) (("1" (flatten) (("1" (typepred "h!1") (("1" (expand "nn_measurable?") (("1" (flatten) (("1" (lemma "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" (name "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_time (("1" (case-replace "(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" (lemma "monotone_convergence[T1, S1, to_measure(mu)]" ("F" "FF")) (("1" (split -1) (("1" (flatten) (("1" (hide -1) (("1" (split -1) (("1" (skolem - "F") (("1" (inst - "F") (("1" (assert) (("1" (typepred "F") (("1" (expand "integrable1?") (("1" (expand "ae_convergence?") (("1" (expand "fullset") (("1" (expand "ae_convergence_in?") (("1" (expand "ae_in?") (("1" (skosimp) (("1" (expand "member") (("1" (typepred "E!1") (("1" (expand "negligible_set?") (("1" (skolem - "N1") (("1" (flatten) (("1" (inst + "N1" "F") (("1" (skosimp) (("1" (expand "subset?") (("1" (inst - "x!1") (("1" (expand "member") (("1" (inst - "x!1") (("1" (assert) (("1" (lemma "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" (split -1) (("1" (flatten) (("1" (replace -1) (("1" (name-replace "LHS" "integral(LAMBDA (y: T2): h!1(x!1, y))") (("1" (case-replace "(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" (flatten) (("1" (hide-all-but (-3 -7 3)) (("1" (lemma "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" (apply-extensionality :hide? t) (("1" (expand "FF" 1) (("1" (expand "o" 1) (("1" (inst -15 "x!2") (("1" (lemma "isf_x_section" ("x" "x!1" "i" "HH(x!2)")) (("1" (rewrite "isf_integral" 1) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (inst -15 "n!1") (("2" (lemma "isf_x_section" ("x" "x!1" "i" "HH(n!1)")) (("2" (lemma "isf_is_integrable[T2, S2, to_measure(nu)]") (("2" (inst - "LAMBDA (y: T2): HH(n!1)(x!1, y)") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 -14 -15)) (("2" (expand "increasing_nn_isf?") (("2" (expand "pointwise_converges_upto?") (("2" (split) (("1" (expand "pointwise_convergence?") (("1" (skolem + "y!1") (("1" (inst - "(x!1,y!1)") nil nil)) nil)) nil) ("2" (expand "pointwise_increasing?") (("2" (skolem + "y!1") (("2" (inst - "(x!1,y!1)") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (replace -8 -5 rl) (("3" (hide-all-but (-7 1 -13 -12 -8 -3 -6)) (("3" (expand "FF") (("3" (expand "o ") (("3" (expand "pointwise_increasing?") (("3" (inst -2 "x!1") (("3" (hide -4) (("3" (expand "bounded?") (("3" (split) (("1" (expand "bounded_above?") (("1" (inst + "F(x!1)") (("1" (skolem + "n!1") (("1" (inst-cp -5 "n!1") (("1" (lemma "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" (inst - "isf_integral(LAMBDA (y: T2): HH(n!1)(x!1, y))-F(x!1)") (("1" (skosimp) (("1" (inst - "n!1+n!2") (("1" (assert) (("1" (expand "ball") (("1" (expand "increasing?") (("1" (inst -3 "n!1" "n!1+n!2") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (skosimp) (("2" (rewrite "isf_x_section") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "bounded_below?") (("2" (inst + "0") (("2" (skolem + "n!1") (("2" (inst -5 "n!1") (("2" (lemma "isf_x_section" ("i" "HH(n!1)" "x" "x!1")) (("2" (rewrite "isf_integral" 1) (("2" (inst -4 "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" (skosimp) (("2" (inst -13 "n!1") (("2" (lemma "isf_x_section" ("i" "HH(n!1)" "x" "x!1")) (("2" (lemma "isf_is_integrable[T2, S2, to_measure(nu)]") (("2" (inst - "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" (hide-all-but (-2 1 -7)) (("2" (expand "bounded?") (("2" (skosimp) (("2" (split) (("1" (expand "bounded_above?") (("1" (inst + "c!1") (("1" (skolem + "n!1") (("1" (inst - "n!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "bounded_below?") (("2" (inst + "-c!1") (("2" (skolem + "n!1") (("2" (inst - "n!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 -2)) (("2" (expand "ae_increasing?") (("2" (inst + "emptyset") (("2" (skosimp) (("2" (expand "pointwise_increasing?") (("2" (inst - "x!1") (("2" (expand "increasing?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -3 * rl) (("2" (hide-all-but (1 -11 -12 -9 -8 -7)) (("2" (expand "bounded?") (("2" (inst + "nn_integral(h!1)") (("2" (skolem + "n!1") (("2" (lemma "isf_integral_pos" ("i" "HH(n!1)")) (("2" (split) (("1" (expand "abs" 1) (("1" (assert) (("1" (expand "o" 1) (("1" (rewrite "metric_convergence_def") (("1" (expand "metric_converges_to") (("1" (inst -5 "isf_integral(HH(n!1))-nn_integral(h!1)") (("1" (skosimp) (("1" (inst -5 "n!1+n!2") (("1" (assert) (("1" (expand "ball") (("1" (expand "increasing_nn_isf?") (("1" (expand "pointwise_increasing?") (("1" (inst-cp -3 "n!1") (("1" (inst -3 "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" (hide 2 -6) (("2" (lemma "isf_integral_le" ("i1" "HH(n!1)" "i2" "HH(n!1 + n!2)")) (("2" (assert) (("2" (skolem + "z!1") (("2" (inst -5 "z!1") (("2" (expand "increasing?") (("2" (inst -5 "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" (skolem + "z!1") (("2" (inst - "n!1" "z!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "increasing_nn_isf?") (("2" (hide-all-but (1 -8 -7)) (("2" (expand "FF") (("2" (expand "pointwise_increasing?") (("2" (skosimp) (("2" (expand "increasing?") (("2" (skolem + ("i!1" "j!1")) (("2" (flatten) (("2" (inst-cp - "j!1") (("2" (inst - "i!1") (("2" (lemma "isf_x_section" ("x" "x!1" "i" "HH(j!1)")) (("2" (lemma "isf_x_section" ("x" "x!1" "i" "HH(i!1)")) (("2" (lemma "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" (skolem + "y!1") (("1" (inst -6 "(x!1,y!1)") (("1" (inst - "i!1" "j!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil) ("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (expand "FF" 1) (("2" (hide-all-but (-5 -6 1)) (("2" (inst - "n!1") (("2" (lemma "isf_x_section" ("x" "x!1" "i" "HH(n!1)")) (("2" (lemma "isf_integral_pos" ("i" "LAMBDA (y: T2): HH(n!1)(x!1, y)")) (("1" (assert) (("1" (skolem + "y!1") (("1" (inst - "n!1" "(x!1,y!1)") nil nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (apply-extensionality :hide? t) (("2" (expand "o") (("2" (inst - "x!1") (("2" (replace -1) (("2" (inst -5 "x!1") (("2" (rewrite "isf_integral") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (inst - "n!1") (("2" (expand "FF") (("2" (inst -4 "n!1") (("2" (rewrite "isf_integral[[T1, T2], sigma_times(S1, S2), to_measure(fm_times(mu, nu))]" 1) (("2" (lemma "isf_fubini_tonelli_3" ("i" "HH(n!1)")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (propax) nil nil)) nil) ("2" (skosimp) (("2" (expand "FF") (("2" (inst -3 "n!1") (("2" (rewrite "isf_integral_x") (("2" (case-replace "(LAMBDA (x: T1, y: T2): HH(n!1)(x, y))=HH(n!1)") (("2" (apply-extensionality :hide? t) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (inst -2 "n!1") (("2" (rewrite "isf_x_section") nil nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (typepred "HH(n!1)") (("2" (expand "nn_isf?") (("2" (inst - "z!1") nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (typepred "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" (name "NN" "cross_product(complement(N!1),fullset[T2])") (("2" (lemma "sigma_algebra_complement[T1,S1]" ("x" "N!1")) (("1" (expand "member") (("1" (replace -3) (("1" (lemma "cross_product_is_sigma_times" ("Y" "fullset[T2]" "X" "N")) (("1" (name "H" "*[[T1,T2]](phi(NN),h!1)") (("1" (name "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" (hide -10) (("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" (lemma "integral_ae_eq" ("f" "H" "h" "h!1")) (("1" (assert) (("1" (hide 2 -1) (("1" (expand "ae_eq?") (("1" (expand "restrict") (("1" (expand "pointwise_ae?") (("1" (expand "ae?") (("1" (expand "fullset" 1) (("1" (expand "H") (("1" (expand "*") (("1" (expand "ae_in?") (("1" (expand "member") (("1" (inst + "cross_product(N!1,fullset[T2])") (("1" (skolem + "y!1") (("1" (flatten) (("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" (inst + "cross_product[T1, T2](N!1, fullset[T2])") (("2" (split) (("1" (hide-all-but (-12 1)) (("1" (expand "null_set?") (("1" (expand "mu_fin?") (("1" (expand "to_measure") (("1" (expand "mu") (("1" (expand "to_measure") (("1" (flatten) (("1" (expand "measurable_set?") (("1" (rewrite "cross_product_is_sigma_times") (("1" (expand "fm_times") (("1" (lemma "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" (skosimp) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "h!1") (("2" (expand "nn_measurable?") (("2" (flatten) nil nil)) nil)) nil) ("3" (lemma "nn_integrable_is_integrable[[T1, T2], sigma_times(S1, S2), to_measure(fm_times(mu, n (("3" (inst - "H") nil nil)) nil)) nil) ("2" (hide 2) (("2" (case "nn_measurable?(H)") (("1" (hide (-7 -8 -9 -10 -11 -12 -13)) (("1" (lemma "nn_integrable_is_nn_integrable" ("f" "F")) (("1" (replace -4) (("1" (lemma "nn_measurable_def" ("f" "H")) (("1" (split -1) (("1" (flatten) (("1" (hide -2) (("1" (split -1) (("1" (skolem - "HH") (("1" (typepred "HH") (("1" (hide -3 -4) (("1" (case "forall (n:nat): isf?(HH(n))") (("1" (case "forall (n:nat,z:[T1, T2]): HH(n)(z) >= 0") (("1" (name "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" (lemma "monotone_convergence_scaf[[T1, T2], sigma_times(S1, S2), to_measure(fm_times(mu, nu))]" ("F" "HH" "f" "H")) (("1" (assert) (("1" (split -1) (("1" (flatten) (("1" (lemma "nn_integrable_is_nn_integrable" ("f" "H")) (("1" (replace -13) (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (expand "bounded?") (("2" (skosimp) (("2" (split) (("1" (expand "bounded_above?") (("1" (inst + "c!1") (("1" (skosimp) (("1" (inst - "x!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "bounded_below?") (("2" (inst + "-c!1") (("2" (skosimp) (("2" (inst - "x!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case-replace "integral o HH=isf_integral o HH") (("1" (expand "bounded?") (("1" (inst + "integral(F)") (("1" (skolem + "n!1") (("1" (expand "o ") (("1" (expand "abs") (("1" (lemma "isf_integral_pos" ("i" "HH(n!1)")) (("1" (inst -7 "n!1" "_") (("1" (replace -7) (("1" (assert) (("1" (hide -1 2) (("1" (rewrite "isf_fubini_tonelli_3") (("1" (lemma "integral_ae_le" ("f1" "FF(n!1)" "f2" "F")) (("1" (split -1) (("1" (expand "FF") (("1" (propax) nil nil)) nil) ("2" (hide-all-but (-2 -3 1)) (("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" (inst + "emptyset") (("2" (skosimp) (("2" (hide 1) (("2" (inst - "x!1") (("2" (inst - "x!1") (("2" (rewrite "metric_convergence_def") (("2" (expand "metric_converges_to") (("2" (assert) (("2" (inst - "FF(n!1)(x!1)-F(x!1)") (("2" (skosimp) (("2" (expand "increasing?") (("2" (inst - "n!1+n!2") (("2" (inst - "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" (inst -4 "n!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst -7 "n!1") nil nil)) nil)) nil)) nil)) nil) ("2" (lemma "integral_nonneg" ("f" "F")) (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (hide -4 2 3) (("2" (apply-extensionality :hide? t) (("2" (expand "o ") (("2" (inst -5 "x!1") (("2" (rewrite "isf_integral") nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (skolem + "n!1") (("3" (inst -6 "n!1") (("3" (lemma "isf_is_integrable[[T1, T2], sigma_times(S1, S2), to_measure(fm_times(mu, nu))]") (("3" (inst - "HH(n!1)") nil nil)) nil)) nil)) nil)) nil) ("2" (expand "pointwise_converges_upto?") (("2" (assert) (("2" (hide 2) (("2" (expand "pointwise_convergence?") (("2" (skosimp) (("2" (inst -12 "x!1") (("2" (inst -13 "x!1") (("2" (replace -12 1 rl) (("2" (expand "FF" 1) (("2" (lemma "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" (split -1) (("1" (flatten) (("1" (expand "converges_upto?") (("1" (flatten) (("1" (expand "o") (("1" (case-replace "(LAMBDA (x_1: nat): integral(LAMBDA (y: T2): HH(x_1)(x!1, y)))=LAMBDA (n:nat): isf_integral(LAMBDA (y: T2): H (("1" (apply-extensionality :hide? t) (("1" (inst -8 "x!2") (("1" (lemma "isf_x_section" ("x" "x!1" "i" "HH(x!2)")) (("1" (rewrite "isf_integral" 1) nil nil) ("2" (propax) nil nil)) nil)) nil) ("2" (skosimp) (("2" (inst -8 "n!1") (("2" (rewrite "isf_x_section") nil nil)) nil)) nil) ("3" (skolem + "n!1") (("3" (inst -8 "n!1") (("3" (lemma "isf_x_section" ("x" "x!1" "i" "HH(n!1)")) (("1" (lemma "isf_is_integrable[T2, S2, to_measure(nu)]") (("1" (inst - "LAMBDA (y: T2): HH(n!1)(x!1, y)") nil nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (inst -8 "n!1") (("2" (rewrite "isf_x_section") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "pointwise_converges_upto?") (("2" (split 1) (("1" (expand "pointwise_convergence?") (("1" (skolem + "y!1") (("1" (inst -7 "(x!1,y!1)") nil nil)) nil)) nil) ("2" (expand "pointwise_increasing?") (("2" (skolem + "y!1") (("2" (inst -8 "(x!1,y!1)") nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (expand "bounded?") (("3" (expand "o") (("3" (split 1) (("1" (expand "bounded_above?") (("1" (inst + "F(x!1)") (("1" (skolem + "n!1") (("1" (lemma "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" (split -1) (("1" (assert) nil nil) ("2" (hide-all-but (1 -6 -7)) (("2" (expand "increasing_nn_simple?") (("2" (flatten) (("2" (hide -1) (("2" (expand "pointwise_increasing?") (("2" (expand "ae_le?") (("2" (expand "pointwise_ae?") (("2" (expand "ae?") (("2" (expand "fullset") (("2" (expand "ae_in?") (("2" (inst + "emptyset") (("2" (skolem + "y!1") (("2" (expand "member") (("2" (flatten) (("2" (hide 1) (("2" (inst - "(x!1,y!1)") (("2" (inst - "(x!1,y!1)") (("2" (rewrite "metric_convergence_def") (("2" (expand "metric_converges_to") (("2" (inst - "HH(n!1)(x!1, y!1)-H(x!1, y!1)") (("1" (skosimp) (("1" (inst - "n!1+n!2") (("1" (expand "ball") (("1" (expand "increasing?") (("1" (inst - "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" (propax) nil nil) ("3" (lemma "isf_x_section" ("x" "x!1" "i" "HH(n!1)")) (("1" (lemma "isf_is_integrable[T2, S2, to_measure(nu)]") (("1" (inst - "LAMBDA (y: T2): HH(n!1)(x!1, y)") nil nil)) nil) ("2" (inst -5 "n!1") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "bounded_below?") (("2" (inst + "0") (("2" (skolem + "n!1") (("2" (inst -5 "n!1") (("2" (lemma "isf_x_section" ("x" "x!1" "i" "HH(n!1)")) (("1" (rewrite "isf_integral" 1) (("1" (lemma "isf_integral_pos" ("i" "LAMBDA (y: T2): HH(n!1)(x!1, y)")) (("1" (assert) (("1" (skolem + "y!1") (("1" (inst -5 "n!1" "(x!1,y!1)") nil nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (inst -5 "n!1") (("2" (lemma "isf_x_section" ("x" "x!1" "i" "HH(n!1)")) (("1" (lemma "isf_is_integrable[T2, S2, to_measure(nu)]") (("1" (inst - "LAMBDA (y: T2): HH(n!1)(x!1, y)") nil nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "increasing_nn_simple?") (("2" (flatten) (("2" (expand "pointwise_increasing?") (("2" (skosimp) (("2" (expand "FF") (("2" (hide-all-but (-4 -6 1)) (("2" (expand "increasing?") (("2" (skolem + ("i!1" "j!1")) (("2" (flatten) (("2" (inst-cp - "j!1") (("2" (inst - "i!1") (("2" (lemma "isf_x_section" ("x" "x!1" "i" "HH(j!1)")) (("1" (lemma "isf_x_section" ("x" "x!1" "i" "HH(i!1)")) (("1" (lemma "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" (skolem + "y!1") (("1" (inst -6 "(x!1,y!1)") (("1" (inst -6 "i!1" "j!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil) ("3" (propax) nil nil)) nil) ("2" (propax) nil nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (hide 2 -1) (("2" (expand "FF") (("2" (inst -2 "n!1") (("2" (lemma "isf_integral_x" ("i" "HH(n!1)")) (("1" (propax) nil nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (inst -2 "n!1") (("2" (rewrite "isf_x_section") nil nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (expand "increasing_nn_simple?") (("2" (expand "nn_simple?") (("2" (flatten) (("2" (inst -2 "n!1") (("2" (flatten) (("2" (inst -2 "z!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (expand "increasing_nn_simple?") (("2" (flatten) (("2" (inst - "n!1") (("2" (expand "nn_simple?") (("2" (flatten) (("2" (expand "isf?") (("2" (expand "mu_fin?") (("2" (expand "to_measure") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "nn_measurable?") (("2" (flatten) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (inst - "x!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil) ("2" (hide -3 -4 -5 2) (("2" (typepred "h!1") (("2" (expand "nn_measurable?") (("2" (flatten) (("2" (split) (("1" (expand "H") (("1" (rewrite "prod_measurable") (("1" (lemma "phi_is_simple[[T1, T2], sigma_times(S1, S2)]" ("X" "NN")) (("1" (expand "simple?") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (inst -3 "x!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (propax) nil nil)) nil) ("2" (skosimp) (("2" (expand "H") (("2" (typepred "h!1") (("2" (expand "nn_measurable?") (("2" (flatten) (("2" (inst - "z!1") (("2" (expand "*") (("2" (expand "phi") (("2" (lift-if 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (inst - "x!1") (("2" (inst - "x!1") (("2" (lemma "integral_nonneg" ("f" "LAMBDA (y: T2): H(x!1, y)")) (("1" (assert) (("1" (skolem + "y!1") (("1" (expand "H") (("1" (expand "*") (("1" (expand "phi") (("1" (lift-if) (("1" (typepred "h!1") (("1" (expand "nn_measurable?") (("1" (flatten) (("1" (inst - "(x!1,y!1)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "f!1") (("2" (expand "F") (("2" (rewrite "indefinite_integrable") nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (inst - "x!1") (("2" (inst -9 "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" (lift-if 1) (("2" (case-replace "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" (skosimp) (("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" (inst -8 "x!1") (("2" (case-replace "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) ((nn_measurable nonempty-type-eq-decl nil measure_space nil) (nn_measurable? const-decl "bool" measure_space nil) (S2 formal-const-decl "sigma_algebra[T2]" finite_fubini_tonelli nil) (S1 formal-const-decl "sigma_algebra[T1]" finite_fubini_tonelli nil) (sigma_times const-decl "sigma_algebra[[T1, T2]]" product_sigma_def nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil) (sigma_algebra? const-decl "bool" subset_algebra_def nil) (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (T2 formal-type-decl nil finite_fubini_tonelli nil) (T1 formal-type-decl nil finite_fubini_tonelli nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (nn_integral_def formula-decl nil nn_integral nil) (nn_integrable? const-decl "bool" nn_integral nil) (nn_integrable nonempty-type-eq-decl nil nn_integral nil) (= const-decl "[T, T -> boolean]" equalities nil) (isf_integral const-decl "real" isf nil) (isf_integral_x formula-decl nil finite_fubini_scaf nil) (integral const-decl "real" integral nil) (bounded? const-decl "bool" sup_norm nil) (minus_real_is_real application-judgement "real" reals nil) (integrable1? const-decl "bool" product_integral_def nil) (fullset const-decl "set" sets nil) (ae_in? const-decl "bool" measure_theory nil) (member const-decl "bool" sets nil) (TRUE const-decl "bool" booleans nil) (monotone_convergence_scaf formula-decl nil integral_convergence_scaf nil) (metric_converges_to const-decl "bool" metric_space_def "metric_space/") (increasing? const-decl "bool" real_fun_preds "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (ball const-decl "set[T]" metric_space_def "metric_space/") (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (F skolem-const-decl "integrable[T1, S1, to_measure(mu)]" finite_fubini_tonelli nil) (n!1 skolem-const-decl "nat" finite_fubini_tonelli nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (metric_convergence_def formula-decl nil metric_space "metric_space/") (bounded_above? const-decl "bool" real_fun_preds "reals/") (bounded_below? const-decl "bool" real_fun_preds "reals/") (bounded? const-decl "bool" real_fun_preds "reals/") (pointwise_converges_upto? const-decl "bool" pointwise_convergence nil) (pointwise_convergence? const-decl "bool" pointwise_convergence nil) (x!1 skolem-const-decl "T1" finite_fubini_tonelli nil) (HH skolem-const-decl "increasing_nn_isf [[T1, T2], sigma_times(S1, S2), to_measure(fm_times(mu, nu))]" finite_fubini_tonelli nil) (isf_x_section formula-decl nil finite_fubini_scaf nil) (isf_integral formula-decl nil integral nil) (FF skolem-const-decl "[nat -> [T1 -> real]]" finite_fubini_tonelli nil) (isf_is_integrable judgement-tcc nil integral nil) (n!1 skolem-const-decl "nat" finite_fubini_tonelli nil) (converges_upto? const-decl "bool" convergence_aux "metric_space/") (metric_induced_topology const-decl "setofsets[T]" metric_space_def "metric_space/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (unique_limit formula-decl nil hausdorff_convergence "topology/") (n!1 skolem-const-decl "nat" finite_fubini_tonelli nil) (subset? const-decl "bool" sets nil) (null_set nonempty-type-eq-decl nil measure_theory nil) (N1 skolem-const-decl "set[T1]" finite_fubini_tonelli nil) (null_set? const-decl "bool" measure_theory nil) (negligible nonempty-type-eq-decl nil measure_theory nil) (negligible_set? const-decl "bool" measure_theory nil) (set type-eq-decl nil sets nil) (ae_convergence_in? const-decl "bool" measure_theory nil) (ae_convergence? const-decl "bool" measure_theory nil) (ae_increasing? const-decl "bool" measure_theory nil) (emptyset const-decl "set" sets nil) (finite_emptyset name-judgement "finite_set" finite_sets nil) (finite_emptyset name-judgement "finite_set[T]" countable_props "sets_aux/") (finite_emptyset name-judgement "finite_set[T]" countable_setofsets "sets_aux/") (finite_emptyset name-judgement "finite_set[T]" sigma_countable "sigma_set/") (subset_algebra_emptyset name-judgement "(S)" finite_fubini_tonelli nil) (null_emptyset name-judgement "null_set" finite_fubini_tonelli nil) (monotone_convergence formula-decl nil integral_convergence nil) (nn_integral const-decl "nnreal" nn_integral nil) (isf_integral_pos formula-decl nil isf nil) (<= const-decl "bool" reals nil) (isf_integral_le formula-decl nil isf nil) (h!1 skolem-const-decl "nn_measurable[[T1, T2], sigma_times(S1, S2)]" finite_fubini_tonelli nil) (n!1 skolem-const-decl "nat" finite_fubini_tonelli nil) (pointwise_increasing? const-decl "bool" pointwise_convergence nil) (O const-decl "T3" function_props nil) (isf_fubini_tonelli_3 formula-decl nil finite_fubini_scaf nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (isf? const-decl "bool" isf nil) (isf nonempty-type-eq-decl nil isf nil) (nn_isf? const-decl "bool" nn_integral nil) (nn_isf nonempty-type-eq-decl nil nn_integral nil) (sequence type-eq-decl nil sequences nil) (increasing_nn_isf? const-decl "bool" nn_integral nil) (increasing_nn_isf nonempty-type-eq-decl nil nn_integral nil) (nn_integrable_is_nn_integrable formula-decl nil integral nil) (integrable? const-decl "bool" integral nil) (integrable nonempty-type-eq-decl nil integral nil) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (finite_measure? const-decl "bool" generalized_measure_def nil) (finite_measure nonempty-type-eq-decl nil generalized_measure_def nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (measure? const-decl "bool" generalized_measure_def nil) (measure_type nonempty-type-eq-decl nil generalized_measure_def nil) (to_measure const-decl "measure_type" generalized_measure_def nil) (fm_times const-decl "finite_measure[[T1, T2], sigma_times(S1, S2)]" product_finite_measure nil) (mu formal-const-decl "finite_measure[T1, S1]" finite_fubini_tonelli nil) (nu formal-const-decl "finite_measure[T2, S2]" finite_fubini_tonelli nil) (subset_algebra_complement application-judgement "(S)" sigma_algebra nil) (measurable_complement application-judgement "measurable_set" finite_fubini_tonelli nil) (complement const-decl "set" sets nil) (sigma_algebra_complement formula-decl nil sigma_algebra nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (phi const-decl "nat" measure_space nil) (integral_zero formula-decl nil integral nil) (N skolem-const-decl "(null_set?)" finite_fubini_tonelli nil) (measurable_set nonempty-type-eq-decl nil measure_space_def nil) (indefinite_integrable formula-decl nil integral nil) (nn_integrable_is_integrable judgement-tcc nil integral nil) (ae_eq? const-decl "bool" measure_theory nil) (pointwise_ae? const-decl "bool" measure_theory nil) (real_times_real_is_real application-judgement "real" reals nil) (measurable_set? const-decl "bool" measure_space_def nil) (rectangle_measure1 formula-decl nil product_finite_measure nil) (mu const-decl "nnreal" measure_props nil) (mu_fin? const-decl "bool" measure_props nil) (NN skolem-const-decl "set[[T1, T2]]" finite_fubini_tonelli nil) (N!1 skolem-const-decl "null_set[T1, S1, to_measure(mu)]" finite_fubini_tonelli nil) (H skolem-const-decl "[[T1, T2] -> real]" finite_fubini_tonelli nil) (ae? const-decl "bool" measure_theory nil) (measurable_fullset name-judgement "measurable_set[T, S]" finite_fubini_tonelli nil) (subset_algebra_fullset name-judgement "(S)" finite_fubini_tonelli nil) (restrict const-decl "R" restrict nil) (measurable_function nonempty-type-eq-decl nil measure_space_def nil) (measurable_function? const-decl "bool" measure_space_def nil) (integral_ae_eq formula-decl nil integral nil) (nn_measurable_def formula-decl nil measure_space nil) (increasing_nn_simple? const-decl "bool" measure_space nil) (increasing_nn_simple nonempty-type-eq-decl nil measure_space nil) (nn_simple? const-decl "bool" measure_space nil) (n!1 skolem-const-decl "nat" finite_fubini_tonelli nil) (x!1 skolem-const-decl "T1" finite_fubini_tonelli nil) (n!1 skolem-const-decl "nat" finite_fubini_tonelli nil) (null_emptyset name-judgement "null_set" finite_fubini_tonelli nil) (subset_algebra_emptyset name-judgement "(S)" finite_fubini_tonelli nil) (y!1 skolem-const-decl "({x | TRUE})" finite_fubini_tonelli nil) (n!1 skolem-const-decl "nat" finite_fubini_tonelli nil) (integral_nonneg formula-decl nil integral nil) (FF skolem-const-decl "[nat -> [T1 -> real]]" finite_fubini_tonelli nil) (measurable_fullset name-judgement "measurable_set[T, S]" finite_fubini_tonelli nil) (subset_algebra_fullset name-judgement "(S)" finite_fubini_tonelli nil) (ae_le? const-decl "bool" measure_theory nil) (integral_ae_le formula-decl nil integral nil) (F skolem-const-decl "[T1 -> real]" finite_fubini_tonelli nil) (HH skolem-const-decl "increasing_nn_simple[[T1, T2], sigma_times(S1, S2)]" finite_fubini_tonelli nil) (n!1 skolem-const-decl "nat" finite_fubini_tonelli nil) (phi_is_simple judgement-tcc nil measure_space nil) (simple? const-decl "bool" measure_space nil) (prod_measurable judgement-tcc nil measure_space nil) (integrable_zero formula-decl nil integral nil) (cross_product_is_sigma_times formula-decl nil product_sigma nil) (measurable_fullset name-judgement "measurable_set[T, S]" finite_fubini_tonelli nil) (subset_algebra_fullset name-judgement "(S)" finite_fubini_tonelli nil) (cross_product const-decl "set[[T1, T2]]" cross_product "topology/")) shostak)) (finite_fubini_tonelli_2 0 (finite_fubini_tonelli_2-1 nil 3459084018 ("" (skosimp) (("" (split) (("1" (flatten) (("1" (typepred "h!1") (("1" (expand "nn_measurable?") (("1" (flatten) (("1" (lemma "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" (name "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_time (("1" (case-replace "(isf_integral o HH)=integral o GG") (("1" (hide -1) (("1" (case "forall (n:nat,y:T2): GG(n)(y)>=0") (("1" (case "pointwise_increasing?(GG)") (("1" (case "bounded?(integral o GG)") (("1" (lemma "monotone_convergence[T2, S2, to_measure(nu)]" ("F" "GG")) (("1" (split -1) (("1" (flatten) (("1" (hide -1) (("1" (split -1) (("1" (skolem - "G") (("1" (inst - "G") (("1" (assert) (("1" (typepred "G") (("1" (expand "integrable2?") (("1" (expand "ae_convergence?") (("1" (expand "fullset") (("1" (expand "ae_convergence_in?") (("1" (expand "ae_in?") (("1" (skosimp) (("1" (typepred "E!1") (("1" (expand "negligible_set?") (("1" (skolem - "N2") (("1" (flatten) (("1" (inst + "N2" "G") (("1" (skosimp) (("1" (expand "subset?") (("1" (expand "member") (("1" (inst - "y!1") (("1" (assert) (("1" (inst -3 "y!1") (("1" (assert) (("1" (lemma "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" (split -1) (("1" (flatten) (("1" (replace -1) (("1" (name-replace "LHS" "integral(LAMBDA (x: T1): h!1(x, y!1))") (("1" (case-replace "(integral o (LAMBDA (n: nat): LAMBDA (x: T1): HH(n)(x, y!1)))=LAMBDA (n:nat): GG(n)(y!1)") (("1" (hide -1) (("1" (expand "converges_upto?") (("1" (flatten) (("1" (hide-all-but (-2 -6 3)) (("1" (lemma "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" (hide 4) (("2" (apply-extensionality :hide? t) (("1" (expand "GG" 1) (("1" (expand "o" 1) (("1" (inst -14 "x!1") (("1" (lemma "isf_y_section" ("y" "y!1" "i" "HH(x!1)")) (("1" (rewrite "isf_integral") nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (inst -14 "n!1") (("2" (lemma "isf_y_section" ("y" "y!1" "i" "HH(n!1)")) (("2" (lemma "isf_is_integrable[T1, S1, to_measure(mu)]") (("2" (inst - "LAMBDA (x: T1): HH(n!1)(x, y!1)") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 -14 -13)) (("2" (expand "increasing_nn_isf?") (("2" (expand "pointwise_converges_upto?") (("2" (split) (("1" (expand "pointwise_convergence?") (("1" (skosimp) (("1" (inst - "(x!1,y!1)") nil nil)) nil)) nil) ("2" (expand "pointwise_increasing?") (("2" (skosimp) (("2" (inst - "(x!1,y!1)") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but (-3 -6 1 -11 -12 -7)) (("3" (expand "bounded?") (("3" (expand "o") (("3" (split) (("1" (expand "bounded_above?") (("1" (inst + "G(y!1)") (("1" (skolem + "n!1") (("1" (expand "GG") (("1" (expand "pointwise_increasing?") (("1" (inst - "y!1") (("1" (rewrite "metric_convergence_def") (("1" (expand "metric_converges_to") (("1" (inst-cp -5 "n!1") (("1" (lemma "isf_y_section" ("y" "y!1" "i" "HH(n!1)")) (("1" (rewrite "isf_integral" 1) (("1" (inst - "isf_integral(LAMBDA (x: T1): HH(n!1)(x, y!1))-G(y!1)") (("1" (skosimp) (("1" (inst - "n!1+n!2") (("1" (assert) (("1" (expand "ball") (("1" (expand "increasing?") (("1" (inst -3 "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" (skosimp) (("2" (rewrite "isf_y_section") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "bounded_below?") (("2" (inst + "0") (("2" (skolem + "n!1") (("2" (inst -5 "n!1") (("2" (lemma "isf_y_section" ("y" "y!1" "i" "HH(n!1)")) (("2" (rewrite "isf_integral") (("2" (lemma "isf_integral_pos" ("i" "LAMBDA (x: T1): HH(n!1)(x, y!1)")) (("1" (assert) (("1" (skosimp) (("1" (assert) (("1" (inst -5 "n!1" "(x!1,y!1)") nil nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (inst -12 "n!1") (("2" (lemma "isf_y_section" ("y" "y!1" "i" "HH(n!1)")) (("2" (lemma "isf_is_integrable[T1, S1, to_measure(mu)]") (("2" (inst - "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" (hide -1 -5 2) (("2" (expand "bounded?") (("2" (skosimp) (("2" (split 1) (("1" (expand "bounded_above?") (("1" (inst + "c!1") (("1" (skolem + "n!1") (("1" (inst - "n!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "bounded_below?") (("2" (inst + "-c!1") (("2" (skolem + "n!1") (("2" (inst - "n!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-2 1)) (("2" (expand "ae_increasing?") (("2" (expand "pointwise_increasing?") (("2" (expand "increasing?") (("2" (inst + "emptyset") (("2" (skolem + "y!1") (("2" (inst - "y!1") (("2" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -5 2) (("2" (expand "bounded?") (("2" (inst + "nn_integral(h!1)") (("2" (skolem + "n!1") (("2" (expand "o ") (("2" (lemma "integral_nonneg" ("f" "GG(n!1)")) (("2" (inst-cp -3 "n!1" "_") (("2" (replace -4) (("2" (expand "abs") (("2" (assert) (("2" (rewrite "metric_convergence_def") (("2" (expand "metric_converges_to") (("2" (inst -11 "integral(GG(n!1))-nn_integral(h!1)") (("2" (skosimp) (("2" (inst -11 "n!1+n!2") (("2" (assert) (("2" (expand "ball") (("2" (expand "pointwise_increasing?") (("2" (inst-cp -6 "n!1") (("2" (inst -6 "n!1+n!2") (("2" (case "integral(GG(n!1)) <= integral(GG(n!1 + n!2))") (("1" (assert) nil nil) ("2" (hide 2) (("2" (lemma "integral_ae_le" ("f1" "GG(n!1)" "f2" "GG(n!1 + n!2)")) (("2" (assert) (("2" (hide 2) (("2" (expand "ae_le?") (("2" (expand "pointwise_ae?") (("2" (expand "ae?") (("2" (expand "fullset") (("2" (expand "ae_in?") (("2" (inst + "emptyset") (("2" (skolem + "y!1") (("2" (expand "member") (("2" (flatten) (("2" (inst - "y!1") (("2" (expand "increasing?") (("2" (inst - "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" (skolem + "y!1") (("2" (expand "increasing_nn_isf?") (("2" (expand "pointwise_increasing?") (("2" (expand "increasing?") (("2" (skolem + ("i!1" "j!1")) (("2" (flatten) (("2" (hide -3 -4 2 -5) (("2" (expand "GG") (("2" (inst-cp -4 "i!1") (("2" (inst -4 "j!1") (("2" (lemma "isf_y_section" ("i" "HH(i!1)" "y" "y!1")) (("2" (lemma "isf_y_section" ("i" "HH(j!1)" "y" "y!1")) (("2" (lemma "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" (skosimp) (("1" (inst -8 "(x!1,y!1)") (("1" (inst -8 "i!1" "j!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil) ("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2 -1 -2 -3) (("2" (skosimp) (("2" (expand "GG") (("2" (inst - "n!1" "_") (("2" (inst -2 "n!1") (("2" (lemma "isf_y_section" ("y" "y!1" "i" "HH(n!1)")) (("2" (lemma "isf_integral_pos" ("i" "LAMBDA (x: T1): HH(n!1)(x, y!1)")) (("1" (assert) (("1" (skosimp) (("1" (inst - "(x!1,y!1)") nil nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (apply-extensionality :hide? t) (("2" (expand "o ") (("2" (inst - "x!1") (("2" (replace -1) (("2" (inst -5 "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" (skosimp) (("2" (inst - "n!1") (("2" (inst -4 "n!1") (("2" (hide -2 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" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (propax) nil nil)) nil) ("2" (hide -1 2) (("2" (skosimp) (("2" (expand "GG") (("2" (rewrite "isf_integral_y") (("2" (case-replace "(LAMBDA (x: T1, y: T2): HH(n!1)(x, y))=HH(n!1)") (("1" (assert) nil nil) ("2" (apply-extensionality :hide? t) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (rewrite "isf_y_section") nil nil)) nil)) nil) ("2" (skosimp) (("2" (typepred "HH(n!1)") (("2" (expand "nn_isf?") (("2" (inst - "z!1") nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (typepred "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" (name "NN" "cross_product(fullset[T1],complement(N!1))") (("2" (lemma "sigma_algebra_complement[T2,S2]" ("x" "N!1")) (("1" (expand "member") (("1" (replace -3) (("1" (lemma "cross_product_is_sigma_times" ("X" "fullset[T1]" "Y" "N")) (("1" (replace -3) (("1" (name "H" "*[[T1,T2]](phi(NN),h!1)") (("1" (name "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" (hide -10) (("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" (lemma "integral_ae_eq" ("f" "H" "h" "h!1")) (("1" (assert) (("1" (hide 2 -1) (("1" (expand "ae_eq?") (("1" (expand "pointwise_ae?") (("1" (expand "restrict") (("1" (expand "ae?") (("1" (expand "fullset" 1) (("1" (expand "H") (("1" (expand "*") (("1" (expand "phi") (("1" (expand "ae_in?") (("1" (expand "member") (("1" (inst + "cross_product(fullset[T1], N!1)") (("1" (skolem + "z!1") (("1" (expand "NN") (("1" (expand "fullset") (("1" (expand "cross_product") (("1" (expand "complement") (("1" (expand "member") (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "negligible_set?") (("2" (inst + "cross_product[T1, T2](fullset[T1], N!1)") (("2" (split) (("1" (hide-all-but (-12 1)) (("1" (expand "null_set?") (("1" (flatten) (("1" (expand "mu_fin?") (("1" (expand "mu") (("1" (expand "to_measure") (("1" (lemma "cross_product_is_sigma_times" ("X" "fullset[T1]" "Y" "N!1")) (("1" (expand "measurable_set?") (("1" (assert) (("1" (expand "fm_times") (("1" (lemma "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" (skosimp) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "h!1") (("2" (expand "nn_measurable?") (("2" (flatten) nil nil)) nil)) nil) ("3" (lemma "nn_integrable_is_integrable[[T1, T2], sigma_times(S1, S2), to_measure(fm_times(mu, n (("3" (inst - "H") nil nil)) nil)) nil) ("2" (hide 2) (("2" (case "nn_measurable?(H)") (("1" (hide (-7 -8 -9 -10 -11 -12 -13)) (("1" (lemma "nn_integrable_is_nn_integrable" ("f" "G")) (("1" (replace -4) (("1" (lemma "nn_measurable_def" ("f" "H")) (("1" (split) (("1" (flatten) (("1" (split -1) (("1" (skolem - "HH") (("1" (typepred "HH") (("1" (hide -3 -4) (("1" (case "forall (n:nat): isf?(HH(n))") (("1" (case "forall (n:nat,z:[T1, T2]): HH(n)(z) >= 0") (("1" (name "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" (lemma "monotone_convergence_scaf[[T1, T2], sigma_times(S1, S2), to_measure(fm_times(mu, nu))]" ("F" "HH" "f" "H")) (("1" (assert) (("1" (split -1) (("1" (flatten) (("1" (lemma "nn_integrable_is_nn_integrable" ("f" "H")) (("1" (replace -14) (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (expand "o ") (("2" (assert) (("2" (expand "bounded?") (("2" (skosimp) (("2" (split) (("1" (expand "bounded_above?") (("1" (inst + "c!1") (("1" (skolem + "n!1") (("1" (inst - "n!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "bounded_below?") (("2" (inst + "-c!1") (("2" (skolem + "n!1") (("2" (inst - "n!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (case-replace "integral o HH=isf_integral o HH") (("1" (hide -1) (("1" (expand "bounded?") (("1" (inst + "integral(G)") (("1" (skolem + "n!1") (("1" (expand "o" 1) (("1" (expand "abs" 1) (("1" (inst-cp -6 "n!1") (("1" (lemma "isf_integral_pos" ("i" "HH(n!1)")) (("1" (inst -6 "n!1" "_") (("1" (replace -6) (("1" (assert) (("1" (hide -1) (("1" (rewrite "isf_fubini_tonelli_4") (("1" (lemma "integral_ae_le" ("f1" "GG(n!1)" "f2" "G")) (("1" (split) (("1" (expand "GG" -1) (("1" (propax) nil nil)) nil) ("2" (hide 2) (("2" (hide-all-but (-1 -2 -12 1)) (("2" (expand "ae_le?") (("2" (expand "pointwise_ae?") (("2" (expand "ae?") (("2" (expand "fullset") (("2" (expand "ae_in?") (("2" (inst + "emptyset") (("2" (skolem + "y!1") (("2" (expand "member") (("2" (flatten) (("2" (expand "pointwise_converges_upto?") (("2" (expand "pointwise_convergence?") (("2" (expand "pointwise_increasing?") (("2" (inst - "y!1") (("2" (inst - "y!1") (("2" (inst - "y!1") (("2" (hide 1) (("2" (rewrite "metric_convergence_def") (("2" (expand "metric_converges_to") (("2" (expand "increasing?") (("2" (inst - "GG(n!1)(y!1)-G(y!1)") (("1" (skosimp) (("1" (inst - "n!1+n!2") (("1" (expand "ball") (("1" (assert) (("1" (inst - "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" (inst - "n!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "integral_nonneg" ("f" "G")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (apply-extensionality :hide? t) (("2" (expand "o ") (("2" (inst -6 "x!1") (("2" (rewrite "isf_integral") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skolem + "n!1") (("3" (inst -6 "n!1") (("3" (lemma "isf_is_integrable[[T1, T2], sigma_times(S1, S2), to_measure(fm_times(mu, nu))]") (("3" (inst - "HH(n!1)") nil nil)) nil)) nil)) nil)) nil) ("2" (expand "pointwise_converges_upto?") (("2" (assert) (("2" (flatten) (("2" (hide 2) (("2" (expand "pointwise_convergence?") (("2" (skolem + "y!1") (("2" (inst -13 "y!1") (("2" (inst -14 "y!1") (("2" (replace -13 1 rl) (("2" (expand "GG" 1) (("2" (lemma "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" (split -1) (("1" (flatten) (("1" (expand "converges_upto?") (("1" (flatten) (("1" (expand "o" -2) (("1" (case-replace "(LAMBDA (x_1: nat): integral(LAMBDA (x: T1): HH(x_1)(x, y!1)))=LAMBDA (n:nat): isf_integral(LAMBDA (x: T1): H (("1" (apply-extensionality :hide? t) (("1" (inst -8 "x!1") (("1" (lemma "isf_y_section" ("y" "y!1" "i" "HH(x!1)")) (("1" (rewrite "isf_integral" 1) nil nil) ("2" (propax) nil nil)) nil)) nil) ("2" (skosimp) (("2" (inst -8 "n!1") (("2" (rewrite "isf_y_section") nil nil)) nil)) nil) ("3" (skolem + "n!1") (("3" (inst -8 "n!1") (("3" (lemma "isf_y_section" ("y" "y!1" "i" "HH(n!1)")) (("1" (lemma "isf_is_integrable" ("x" "LAMBDA (x: T1): HH(n!1)(x, y!1)")) (("1" (propax) nil nil) ("2" (propax) nil nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (inst -8 "n!1") (("2" (rewrite "isf_y_section") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "pointwise_converges_upto?") (("2" (split) (("1" (expand "pointwise_convergence?") (("1" (skosimp) (("1" (inst -7 "(x!1,y!1)") nil nil)) nil)) nil) ("2" (hide-all-but (-8 1)) (("2" (expand "pointwise_increasing?") (("2" (skosimp) (("2" (inst - "(x!1,y!1)") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (expand "bounded?") (("3" (split) (("1" (expand "o") (("1" (expand "bounded_above?") (("1" (inst + "G(y!1)") (("1" (skolem + "n!1") (("1" (lemma "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" (hide 2) (("1" (expand "ae_le?") (("1" (expand "pointwise_ae?") (("1" (expand "ae?") (("1" (expand "fullset") (("1" (expand "ae_in?") (("1" (inst + "emptyset") (("1" (skosimp) (("1" (expand "member") (("1" (hide-all-but (-7 -8 2)) (("1" (expand "pointwise_increasing?") (("1" (inst - "(x!1,y!1)") (("1" (inst - "(x!1,y!1)") (("1" (expand "increasing?") (("1" (rewrite "metric_convergence_def") (("1" (expand "metric_converges_to") (("1" (inst - "HH(n!1)(x!1, y!1)-H(x!1, y!1)") (("1" (skosimp) (("1" (inst - "n!1+n!2") (("1" (assert) (("1" (expand "ball") (("1" (inst - "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" (propax) nil nil) ("3" (inst -5 "n!1") (("3" (lemma "isf_y_section" ("y" "y!1" "i" "HH(n!1)")) (("1" (lemma "isf_is_integrable[T1, S1, to_measure(mu)]") (("1" (inst - "LAMBDA (x: T1): HH(n!1)(x, y!1)") nil nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "bounded_below?") (("2" (inst + "0") (("2" (skolem + "n!1") (("2" (expand "o ") (("2" (inst -5 "n!1") (("2" (lemma "isf_y_section" ("y" "y!1" "i" "HH(n!1)")) (("1" (rewrite "isf_integral" 1) (("1" (lemma "isf_integral_pos[T1,S1,to_measure(mu)]" ("i" "LAMBDA (x: T1): HH(n!1)(x, y!1)")) (("1" (assert) (("1" (skosimp) (("1" (inst -5 "n!1" "(x!1,y!1)") nil nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (inst -5 "n!1") (("2" (lemma "isf_y_section" ("i" "HH(n!1)" "y" "y!1")) (("1" (lemma "isf_is_integrable" ("x" "LAMBDA (x: T1): HH(n!1)(x, y!1)")) (("1" (propax) nil nil) ("2" (propax) nil nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2 -2 -1) (("2" (expand "increasing_nn_simple?") (("2" (flatten) (("2" (expand "pointwise_increasing?") (("2" (skolem + "y!1") (("2" (expand "increasing?") (("2" (skolem + ("i!1" "j!1")) (("2" (flatten) (("2" (expand "GG") (("2" (lemma "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" (hide 2) (("1" (skosimp) (("1" (inst -5 "(x!1, y!1)") (("1" (inst -5 "i!1" "j!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst -3 "j!1") (("2" (rewrite "isf_y_section") nil nil)) nil) ("3" (inst -3 "i!1") (("3" (rewrite "isf_y_section") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 2) (("2" (skosimp) (("2" (expand "GG") (("2" (inst -2 "n!1") (("2" (rewrite "isf_integral_y") (("2" (case-replace "(LAMBDA (x: T1, y: T2): HH(n!1)(x, y))=HH(n!1)") --> -------------------- --> maximum size reached --> --------------------
¤ 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.650Bemerkung: (vorverarbeitet am 2026-05-01) ¤*Bot Zugriff |
|
||||||||||||||
2026-05-26