|
(finite_fubini
(mu_TCC1 0
(mu_TCC1-1 nil 3458563403
("" (typepred "S1")
(("" (expand "sigma_algebra?")
(("" (flatten)
(("" (expand "subset_algebra_empty?")
(("" (expand "member") (("" (propax) nil nil)) nil)) nil))
nil))
nil))
nil)
((subset_algebra_empty? const-decl "bool" subset_algebra_def nil)
(member const-decl "bool" sets 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 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 nil))
nil))
(nu_TCC1 0
(nu_TCC1-1 nil 3458563403
("" (typepred "S2")
(("" (expand "sigma_algebra?")
(("" (flatten)
(("" (expand "subset_algebra_empty?")
(("" (expand "member") (("" (propax) nil nil)) nil)) nil))
nil))
nil))
nil)
((subset_algebra_empty? const-decl "bool" subset_algebra_def nil)
(member const-decl "bool" sets 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 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 nil))
nil))
(finite_integrable_is_integrable1 0
(finite_integrable_is_integrable1-1 nil 3458565294
("" (skosimp)
(("" (typepred "f!1")
(("" (lemma "integrable_pm_def" ("f0" "f!1"))
(("" (flatten)
(("" (split -1)
(("1" (flatten)
(("1" (hide -3 -4)
(("1"
(case "nn_measurable?[[T1, T2], sigma_times[T1, T2](S1, S2)]
(minus[[T1, T2]](f!1))")
(("1"
(case "nn_measurable?[[T1, T2], sigma_times[T1, T2](S1, S2)]
(plus[[T1, T2]](f!1))")
(("1"
(lemma "finite_fubini_tonelli_1"
("h" "minus(f!1)"))
(("1"
(lemma "finite_fubini_tonelli_1"
("h" "plus(f!1)"))
(("1" (assert)
(("1"
(lemma "integrable1_diff"
("g1" "plus(f!1)" "h1" "minus(f!1)"))
(("1"
(case-replace
"((-[[T1, T2]])(plus(f!1), minus(f!1)))=f!1")
(("1"
(assert)
(("1"
(hide-all-but 1)
(("1"
(apply-extensionality :hide? t)
(("1" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (propax) nil nil))
nil)
("2" (propax) nil nil))
nil)
("2" (hide-all-but (-2 1))
(("2" (expand "nn_measurable?")
(("2"
(use "integrable_is_measurable[[T1,T2],sigma_times(S1,S2),to_measure(fm_times(mu,nu))]")
(("2" (replace -1)
(("2" (hide-all-but 1)
(("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide -1 2)
(("2" (expand "nn_measurable?")
(("2"
(use "integrable_is_measurable[[T1,T2],sigma_times(S1,S2),to_measure(fm_times(mu,nu))]")
(("2" (assert)
(("2" (hide-all-but 1)
(("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil)
((integrable nonempty-type-eq-decl nil integral nil)
(integrable? const-decl "bool" integral nil)
(nu formal-const-decl "finite_measure[T2, S2]" finite_fubini nil)
(mu formal-const-decl "finite_measure[T1, S1]" finite_fubini nil)
(fm_times const-decl
"finite_measure[[T1, T2], sigma_times(S1, S2)]"
product_finite_measure nil)
(to_measure const-decl "measure_type" generalized_measure_def nil)
(measure_type nonempty-type-eq-decl nil generalized_measure_def
nil)
(measure? const-decl "bool" generalized_measure_def nil)
(extended_nnreal nonempty-type-eq-decl nil extended_nnreal
"extended_nnreal/")
(finite_measure nonempty-type-eq-decl nil generalized_measure_def
nil)
(finite_measure? const-decl "bool" generalized_measure_def nil)
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(S2 formal-const-decl "sigma_algebra[T2]" finite_fubini nil)
(S1 formal-const-decl "sigma_algebra[T1]" finite_fubini 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 nil)
(T1 formal-type-decl nil finite_fubini nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(minus const-decl "[T -> nnreal]" real_fun_ops_aux "reals/")
(nn_measurable? const-decl "bool" measure_space nil)
(integrable_is_measurable judgement-tcc nil integral nil)
(integrable_minus application-judgement "integrable" finite_fubini
nil)
(finite_fubini_tonelli_1 formula-decl nil finite_fubini_tonelli
nil)
(nn_measurable nonempty-type-eq-decl nil measure_space nil)
(- const-decl "[T -> real]" real_fun_ops "reals/")
(= const-decl "[T, T -> boolean]" equalities nil)
(integrable_diff application-judgement "integrable" finite_fubini
nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
(min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
(integrable1 nonempty-type-eq-decl nil product_integral_def nil)
(integrable1? const-decl "bool" product_integral_def nil)
(integrable1_diff judgement-tcc nil product_integral_def nil)
(integrable_plus application-judgement "integrable" finite_fubini
nil)
(plus const-decl "[T -> nnreal]" real_fun_ops_aux "reals/")
(integrable_pm_def formula-decl nil integral nil))
shostak))
(finite_integrable_is_integrable2 0
(finite_integrable_is_integrable2-1 nil 3458565308
("" (skosimp)
(("" (typepred "f!1")
(("" (lemma "integrable_pm_def" ("f0" "f!1"))
(("" (flatten)
(("" (split -1)
(("1" (flatten)
(("1" (hide -3)
(("1"
(case "nn_measurable?[[T1, T2], sigma_times[T1, T2](S1, S2)]
(minus[[T1, T2]](f!1))")
(("1"
(case "nn_measurable?[[T1, T2], sigma_times[T1, T2](S1, S2)]
(plus[[T1, T2]](f!1))")
(("1"
(lemma "finite_fubini_tonelli_2"
("h" "minus(f!1)"))
(("1"
(lemma "finite_fubini_tonelli_2"
("h" "plus(f!1)"))
(("1"
(lemma "integrable2_diff"
("g2" "plus(f!1)" "h2" "minus(f!1)"))
(("1"
(case-replace
"((-[[T1, T2]])(plus(f!1), minus(f!1)))=f!1")
(("1" (hide-all-but 1)
(("1"
(apply-extensionality :hide? t)
(("1" (grind) nil nil))
nil))
nil))
nil)
("2" (assert) nil nil)
("3" (assert) nil nil))
nil)
("2" (propax) nil nil))
nil)
("2" (propax) nil nil))
nil)
("2" (expand "nn_measurable?")
(("2"
(use "integrable_is_measurable[[T1,T2],sigma_times(S1,S2),to_measure(fm_times(mu,nu))]")
(("2" (assert)
(("2" (hide-all-but 1)
(("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (expand "nn_measurable?")
(("2"
(use "integrable_is_measurable[[T1,T2],sigma_times(S1,S2),to_measure(fm_times(mu,nu))]")
(("2" (assert)
(("2" (hide-all-but 1) (("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil)
((integrable nonempty-type-eq-decl nil integral nil)
(integrable? const-decl "bool" integral nil)
(nu formal-const-decl "finite_measure[T2, S2]" finite_fubini nil)
(mu formal-const-decl "finite_measure[T1, S1]" finite_fubini nil)
(fm_times const-decl
"finite_measure[[T1, T2], sigma_times(S1, S2)]"
product_finite_measure nil)
(to_measure const-decl "measure_type" generalized_measure_def nil)
(measure_type nonempty-type-eq-decl nil generalized_measure_def
nil)
(measure? const-decl "bool" generalized_measure_def nil)
(extended_nnreal nonempty-type-eq-decl nil extended_nnreal
"extended_nnreal/")
(finite_measure nonempty-type-eq-decl nil generalized_measure_def
nil)
(finite_measure? const-decl "bool" generalized_measure_def nil)
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(S2 formal-const-decl "sigma_algebra[T2]" finite_fubini nil)
(S1 formal-const-decl "sigma_algebra[T1]" finite_fubini 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 nil)
(T1 formal-type-decl nil finite_fubini nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(minus const-decl "[T -> nnreal]" real_fun_ops_aux "reals/")
(nn_measurable? const-decl "bool" measure_space nil)
(integrable_is_measurable judgement-tcc nil integral nil)
(integrable_minus application-judgement "integrable" finite_fubini
nil)
(finite_fubini_tonelli_2 formula-decl nil finite_fubini_tonelli
nil)
(nn_measurable nonempty-type-eq-decl nil measure_space nil)
(integrable2_diff judgement-tcc nil product_integral_def nil)
(integrable2? const-decl "bool" product_integral_def nil)
(integrable2 nonempty-type-eq-decl nil product_integral_def nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
(min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
(integrable_diff application-judgement "integrable" finite_fubini
nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(- const-decl "[T -> real]" real_fun_ops "reals/")
(integrable_plus application-judgement "integrable" finite_fubini
nil)
(plus const-decl "[T -> nnreal]" real_fun_ops_aux "reals/")
(integrable_pm_def formula-decl nil integral nil))
shostak))
(finite_fubini1_TCC1 0
(finite_fubini1_TCC1-1 nil 3459088348
("" (skosimp)
(("" (lemma "finite_integrable_is_integrable1" ("f" "f!1"))
(("" (propax) nil nil)) nil))
nil)
((integrable nonempty-type-eq-decl nil integral nil)
(integrable? const-decl "bool" integral nil)
(nu formal-const-decl "finite_measure[T2, S2]" finite_fubini nil)
(mu formal-const-decl "finite_measure[T1, S1]" finite_fubini nil)
(fm_times const-decl
"finite_measure[[T1, T2], sigma_times(S1, S2)]"
product_finite_measure nil)
(to_measure const-decl "measure_type" generalized_measure_def nil)
(measure_type nonempty-type-eq-decl nil generalized_measure_def
nil)
(measure? const-decl "bool" generalized_measure_def nil)
(extended_nnreal nonempty-type-eq-decl nil extended_nnreal
"extended_nnreal/")
(finite_measure nonempty-type-eq-decl nil generalized_measure_def
nil)
(finite_measure? const-decl "bool" generalized_measure_def nil)
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(S2 formal-const-decl "sigma_algebra[T2]" finite_fubini nil)
(S1 formal-const-decl "sigma_algebra[T1]" finite_fubini 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)
(bool nonempty-type-eq-decl nil booleans 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)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(T2 formal-type-decl nil finite_fubini nil)
(T1 formal-type-decl nil finite_fubini nil)
(finite_integrable_is_integrable1 formula-decl nil finite_fubini
nil))
nil))
(finite_fubini1 0
(finite_fubini1-1 nil 3453185968
("" (skosimp)
(("" (rewrite "integral_pm")
(("" (lemma "integral_pm" ("f" "integral1(f!1)"))
(("" (replace -1)
(("" (hide -1)
(("" (lemma "finite_fubini_tonelli_3" ("g" "plus(f!1)"))
(("1"
(lemma "finite_fubini_tonelli_3" ("g" "minus(f!1)"))
(("1" (assert)
(("1" (replace -1)
(("1" (replace -2)
(("1" (hide -1 -2)
(("1" (rewrite "integral_diff" 1 :dir rl)
(("1" (rewrite "integral_diff" 1 :dir rl)
(("1"
(case-replace
"plus(integral1(f!1)) - minus(integral1(f!1))=integral1(f!1)")
(("1"
(hide -1)
(("1"
(lemma
"integral1_diff"
("g1"
"plus(f!1)"
"h1"
"minus(f!1)"))
(("1"
(case-replace
"plus(f!1) - minus(f!1)=f!1")
(("1"
(hide -1)
(("1"
(lemma
"integral_ae_eq"
("f"
"integral1(f!1)"
"h"
"integral1(plus(f!1)) - integral1(minus(f!1))"))
(("1" (assert) nil nil))
nil))
nil)
("2"
(hide-all-but 1)
(("2"
(apply-extensionality :hide? t)
(("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(name-replace "DRL" "integral1(f!1)")
(("2"
(apply-extensionality :hide? t)
(("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "integrable_pm_def" ("f0" "f!1"))
(("2"
(lemma "nn_integrable_is_nn_integrable"
("f" "minus[[T1, T2]](f!1)"))
(("2" (assert)
(("2" (hide-all-but 1) (("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil)
("2"
(lemma "nn_integrable_is_nn_integrable"
("f" "plus[[T1, T2]](f!1)"))
(("2" (assert)
(("2" (hide-all-but 1) (("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((integral_pm formula-decl nil integral nil)
(integrable? const-decl "bool" integral nil)
(integrable nonempty-type-eq-decl nil integral nil)
(T1 formal-type-decl nil finite_fubini nil)
(T2 formal-type-decl nil finite_fubini nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans 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)
(sigma_times const-decl "sigma_algebra[[T1, T2]]" product_sigma_def
nil)
(S1 formal-const-decl "sigma_algebra[T1]" finite_fubini nil)
(S2 formal-const-decl "sigma_algebra[T2]" finite_fubini nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals 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 nil)
(nu formal-const-decl "finite_measure[T2, S2]" finite_fubini nil)
(integrable_minus application-judgement "integrable" finite_fubini
nil)
(integrable_plus application-judgement "integrable" finite_fubini
nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(finite_fubini_tonelli_3 formula-decl nil finite_fubini_tonelli
nil)
(nn_integrable? const-decl "bool" nn_integral nil)
(nn_integrable nonempty-type-eq-decl nil nn_integral nil)
(plus const-decl "[T -> nnreal]" real_fun_ops_aux "reals/")
(integrable_pm_def formula-decl nil integral nil)
(nn_integrable_is_nn_integrable formula-decl nil integral nil)
(integrable_minus application-judgement "integrable" finite_fubini
nil)
(minus_measurable application-judgement "measurable_function[T, S]"
finite_fubini nil)
(integrable_plus application-judgement "integrable" finite_fubini
nil)
(plus_measurable application-judgement "measurable_function[T, S]"
finite_fubini nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(integral_diff formula-decl nil integral nil)
(integrable_diff application-judgement "integrable" finite_fubini
nil)
(diff_measurable application-judgement "measurable_function[T, S]"
finite_fubini nil)
(- const-decl "[T -> real]" real_fun_ops "reals/")
(= const-decl "[T, T -> boolean]" equalities nil)
(integral1_diff formula-decl nil product_integral_def nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
(min const-decl "{p: real | p <= m AND p <= n}" real_defs 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)
(integrable_diff application-judgement "integrable" finite_fubini
nil)
(minus const-decl "[T -> nnreal]" real_fun_ops_aux "reals/")
(integrable1? const-decl "bool" product_integral_def nil)
(integrable1 nonempty-type-eq-decl nil product_integral_def nil)
(integral1 const-decl "integrable[T1, S1, mu]" product_integral_def
nil))
shostak))
(finite_fubini2_TCC1 0
(finite_fubini2_TCC1-1 nil 3459088348
("" (skosimp)
(("" (lemma "finite_integrable_is_integrable2" ("f" "f!1"))
(("" (propax) nil nil)) nil))
nil)
((integrable nonempty-type-eq-decl nil integral nil)
(integrable? const-decl "bool" integral nil)
(nu formal-const-decl "finite_measure[T2, S2]" finite_fubini nil)
(mu formal-const-decl "finite_measure[T1, S1]" finite_fubini nil)
(fm_times const-decl
"finite_measure[[T1, T2], sigma_times(S1, S2)]"
product_finite_measure nil)
(to_measure const-decl "measure_type" generalized_measure_def nil)
(measure_type nonempty-type-eq-decl nil generalized_measure_def
nil)
(measure? const-decl "bool" generalized_measure_def nil)
(extended_nnreal nonempty-type-eq-decl nil extended_nnreal
"extended_nnreal/")
(finite_measure nonempty-type-eq-decl nil generalized_measure_def
nil)
(finite_measure? const-decl "bool" generalized_measure_def nil)
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(S2 formal-const-decl "sigma_algebra[T2]" finite_fubini nil)
(S1 formal-const-decl "sigma_algebra[T1]" finite_fubini 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)
(bool nonempty-type-eq-decl nil booleans 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)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(T2 formal-type-decl nil finite_fubini nil)
(T1 formal-type-decl nil finite_fubini nil)
(finite_integrable_is_integrable2 formula-decl nil finite_fubini
nil))
nil))
(finite_fubini2 0
(finite_fubini2-1 nil 3453186371
("" (skosimp)
(("" (rewrite "integral_pm")
(("" (lemma "integral_pm" ("f" "integral2(f!1)"))
(("" (replace -1)
(("" (hide -1)
(("" (lemma "finite_fubini_tonelli_4" ("g" "plus(f!1)"))
(("1"
(lemma "finite_fubini_tonelli_4" ("g" "minus(f!1)"))
(("1" (replace -1)
(("1" (replace -2)
(("1" (hide -1 -2)
(("1" (rewrite "integral_diff" 1 :dir rl)
(("1" (rewrite "integral_diff" 1 :dir rl)
(("1"
(case-replace
"plus(integral2(f!1)) - minus(integral2(f!1))=integral2(f!1)")
(("1" (hide -1)
(("1"
(lemma
"integral2_diff"
("g2" "plus(f!1)" "h2" "minus(f!1)"))
(("1"
(case-replace
"plus(f!1) - minus(f!1)=f!1")
(("1"
(hide -1)
(("1"
(lemma
"integral_ae_eq"
("f"
"integral2(f!1)"
"h"
"integral2(plus(f!1)) - integral2(minus(f!1))"))
(("1" (assert) nil nil))
nil))
nil)
("2"
(hide-all-but 1)
(("2"
(apply-extensionality :hide? t)
(("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (name-replace "DRL" "integral2(f!1)")
(("2"
(hide 2)
(("2"
(apply-extensionality :hide? t)
(("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(lemma "nn_integrable_is_nn_integrable"
("f" "minus[[T1, T2]](f!1)"))
(("2" (assert)
(("2" (hide-all-but 1) (("2" (grind) nil nil))
nil))
nil))
nil))
nil)
("2"
(lemma "nn_integrable_is_nn_integrable"
("f" "plus[[T1, T2]](f!1)"))
(("2" (assert)
(("2" (hide-all-but 1) (("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((integral_pm formula-decl nil integral nil)
(integrable? const-decl "bool" integral nil)
(integrable nonempty-type-eq-decl nil integral nil)
(T1 formal-type-decl nil finite_fubini nil)
(T2 formal-type-decl nil finite_fubini nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans 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)
(sigma_times const-decl "sigma_algebra[[T1, T2]]" product_sigma_def
nil)
(S1 formal-const-decl "sigma_algebra[T1]" finite_fubini nil)
(S2 formal-const-decl "sigma_algebra[T2]" finite_fubini nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals 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 nil)
(nu formal-const-decl "finite_measure[T2, S2]" finite_fubini nil)
(integrable_minus application-judgement "integrable" finite_fubini
nil)
(integrable_plus application-judgement "integrable" finite_fubini
nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(finite_fubini_tonelli_4 formula-decl nil finite_fubini_tonelli
nil)
(nn_integrable? const-decl "bool" nn_integral nil)
(nn_integrable nonempty-type-eq-decl nil nn_integral nil)
(plus const-decl "[T -> nnreal]" real_fun_ops_aux "reals/")
(nn_integrable_is_nn_integrable formula-decl nil integral nil)
(integrable_minus application-judgement "integrable" finite_fubini
nil)
(minus_measurable application-judgement "measurable_function[T, S]"
finite_fubini nil)
(integrable_plus application-judgement "integrable" finite_fubini
nil)
(plus_measurable application-judgement "measurable_function[T, S]"
finite_fubini nil)
(integrable_diff application-judgement "integrable" finite_fubini
nil)
(integral_ae_eq formula-decl nil integral nil)
(measurable_function? const-decl "bool" measure_space_def nil)
(measurable_function nonempty-type-eq-decl nil measure_space_def
nil)
(min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
(max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(integral2_diff formula-decl nil product_integral_def nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(- const-decl "[T -> real]" real_fun_ops "reals/")
(diff_measurable application-judgement "measurable_function[T, S]"
finite_fubini nil)
(integrable_diff application-judgement "integrable" finite_fubini
nil)
(integral_diff formula-decl nil integral nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(minus const-decl "[T -> nnreal]" real_fun_ops_aux "reals/")
(integrable2? const-decl "bool" product_integral_def nil)
(integrable2 nonempty-type-eq-decl nil product_integral_def nil)
(integral2 const-decl "integrable[T2, S2, nu]" product_integral_def
nil))
shostak))
(integrable_x_section 0
(integrable_x_section-1 nil 3460343970
("" (skosimp)
(("" (rewrite "integrable_abs_def" 1 :dir rl)
(("1" (lemma "nn_integrable_is_integrable[T2,S2,to_measure(nu)]")
(("1" (inst - "abs(LAMBDA y: h!1(x!1, y))")
(("1" (hide 2)
(("1" (typepred "h!1")
(("1" (expand "bounded_measurable?")
(("1" (flatten)
(("1" (expand "bounded?")
(("1" (skosimp)
(("1"
(lemma "measurable_x_section"
("x" "x!1" "m" "h!1"))
(("1"
(lemma
"nn_integrable_le[T2, S2, to_measure(nu)]"
("g" "abs[T2](LAMBDA y: h!1(x!1, y))" "f"
"lambda y: c!1"))
(("1" (assert)
(("1" (skolem + "y!1")
(("1"
(inst - "(x!1,y!1)")
(("1"
(expand "abs" 1)
(("1" (assert) nil nil))
nil))
nil))
nil))
nil)
("2" (assert)
(("2" (rewrite "abs_measurable[T2, S2]")
nil nil))
nil)
("3" (hide-all-but (-2 1))
(("3"
(lemma
"nn_isf_is_nn_integrable[T2, S2, to_measure(nu)]")
(("3"
(inst - "LAMBDA y: c!1")
(("1" (flatten) nil nil)
("2"
(expand "nn_isf?")
(("2"
(hide 2)
(("2"
(expand "isf?")
(("2"
(expand "mu_fin?")
(("2"
(expand "to_measure")
(("2"
(lemma
"phi_is_simple[T2,S2]"
("X" "fullset[T2]"))
(("2"
(lemma
"simple_scal[T2,S2]"
("c"
"c!1"
"h"
"phi(fullset[T2])"))
(("2"
(expand "fullset")
(("2"
(expand "phi")
(("2"
(expand "member")
(("2"
(expand "*")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (typepred "h!1")
(("2" (expand "bounded_measurable?")
(("2" (flatten)
(("2" (rewrite "measurable_x_section") nil nil)) nil))
nil))
nil))
nil))
nil)
((integrable_abs_def formula-decl nil integral nil)
(measurable_function? const-decl "bool" measure_space_def nil)
(measurable_function nonempty-type-eq-decl nil measure_space_def
nil)
(T1 formal-type-decl nil finite_fubini nil)
(sigma_times const-decl "sigma_algebra[[T1, T2]]" product_sigma_def
nil)
(S1 formal-const-decl "sigma_algebra[T1]" finite_fubini nil)
(bounded_measurable? const-decl "bool" measure_space nil)
(bounded_measurable nonempty-type-eq-decl nil measure_space nil)
(T2 formal-type-decl nil finite_fubini nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans 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 nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals 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)
(nu formal-const-decl "finite_measure[T2, S2]" finite_fubini nil)
(nn_integrable? const-decl "bool" nn_integral nil)
(nn_integrable nonempty-type-eq-decl nil nn_integral nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(abs const-decl "[T -> nonneg_real]" real_fun_ops "reals/")
(x!1 skolem-const-decl "T1" finite_fubini nil)
(h!1 skolem-const-decl
"bounded_measurable[[T1, T2], sigma_times(S1, S2)]" finite_fubini
nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(nn_integrable_le formula-decl nil nn_integral nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(abs_measurable judgement-tcc nil measure_space nil)
(nn_isf_is_nn_integrable judgement-tcc nil nn_integral nil)
(phi_is_simple application-judgement "simple" finite_fubini nil)
(simple_scal judgement-tcc nil measure_space nil)
(simple? const-decl "bool" measure_space nil)
(simple nonempty-type-eq-decl nil measure_space 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)
(phi const-decl "nat" measure_space nil)
(* const-decl "[T -> real]" real_fun_ops "reals/")
(member const-decl "bool" sets nil)
(fullset const-decl "set" sets nil) (set type-eq-decl nil sets nil)
(phi_is_simple judgement-tcc nil measure_space nil)
(subset_algebra_fullset name-judgement "(S)" finite_fubini nil)
(measurable_fullset name-judgement "measurable_set[T, S]"
finite_fubini nil)
(mu_fin? const-decl "bool" measure_props nil)
(nn_isf nonempty-type-eq-decl nil nn_integral nil)
(nn_isf? const-decl "bool" nn_integral nil)
(isf nonempty-type-eq-decl nil isf nil)
(c!1 skolem-const-decl "nnreal" finite_fubini nil)
(isf? const-decl "bool" isf nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(mu formal-const-decl "finite_measure[T1, S1]" finite_fubini nil)
(measurable_x_section formula-decl nil finite_fubini_scaf nil)
(bounded? const-decl "bool" sup_norm nil)
(nn_integrable_is_integrable judgement-tcc nil integral nil))
shostak))
(integrable_y_section 0
(integrable_y_section-1 nil 3473502496
("" (skosimp)
(("" (rewrite "integrable_abs_def" 1 :dir rl)
(("1" (lemma "nn_integrable_is_integrable[T1,S1,to_measure(mu)]")
(("1" (inst - "abs(LAMBDA x: h!1(x, y!1))")
(("1" (hide 2)
(("1" (typepred "h!1")
(("1" (expand "bounded_measurable?")
(("1" (flatten)
(("1" (expand "bounded?")
(("1" (skosimp)
(("1"
(lemma "measurable_y_section"
("y" "y!1" "m" "h!1"))
(("1"
(lemma
"nn_integrable_le[T1, S1, to_measure(mu)]"
("g" "abs[T1](LAMBDA x: h!1(x, y!1))" "f"
"lambda x: c!1"))
(("1" (assert)
(("1" (skosimp)
(("1"
(assert)
(("1"
(expand "abs" 1)
(("1"
(assert)
(("1"
(inst - "(x!1,y!1)")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (rewrite "abs_measurable[T1, S1]") nil
nil)
("3" (hide-all-but 1)
(("3"
(lemma
"nn_isf_is_nn_integrable[T1,S1,to_measure(mu)]")
(("3"
(inst - "LAMBDA x: c!1")
(("1" (flatten) nil nil)
("2"
(hide 2)
(("2"
(expand "nn_isf?")
(("2"
(expand "isf?")
(("2"
(expand "mu_fin?")
(("2"
(expand "to_measure")
(("2"
(lemma
"phi_is_simple[T1,S1]"
("X" "fullset[T1]"))
(("2"
(lemma
"simple_scal[T1,S1]"
("c"
"c!1"
"h"
"phi(fullset[T1])"))
(("2"
(expand "fullset")
(("2"
(expand "phi")
(("2"
(expand "member")
(("2"
(expand "*")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (typepred "h!1")
(("2" (expand "bounded_measurable?")
(("2" (flatten)
(("2" (hide -1 2)
(("2" (rewrite "measurable_y_section") nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((integrable_abs_def formula-decl nil integral nil)
(measurable_function? const-decl "bool" measure_space_def nil)
(measurable_function nonempty-type-eq-decl nil measure_space_def
nil)
(T2 formal-type-decl nil finite_fubini nil)
(sigma_times const-decl "sigma_algebra[[T1, T2]]" product_sigma_def
nil)
(S2 formal-const-decl "sigma_algebra[T2]" finite_fubini nil)
(bounded_measurable? const-decl "bool" measure_space nil)
(bounded_measurable nonempty-type-eq-decl nil measure_space nil)
(T1 formal-type-decl nil finite_fubini nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans 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 nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals 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)
(mu formal-const-decl "finite_measure[T1, S1]" finite_fubini nil)
(nn_integrable? const-decl "bool" nn_integral nil)
(nn_integrable nonempty-type-eq-decl nil nn_integral nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(abs const-decl "[T -> nonneg_real]" real_fun_ops "reals/")
(y!1 skolem-const-decl "T2" finite_fubini nil)
(h!1 skolem-const-decl
"bounded_measurable[[T1, T2], sigma_times(S1, S2)]" finite_fubini
nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(nn_integrable_le formula-decl nil nn_integral nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(abs_measurable judgement-tcc nil measure_space nil)
(nn_isf_is_nn_integrable judgement-tcc nil nn_integral nil)
(phi_is_simple application-judgement "simple" finite_fubini nil)
(simple_scal judgement-tcc nil measure_space nil)
(simple? const-decl "bool" measure_space nil)
(simple nonempty-type-eq-decl nil measure_space 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)
(phi const-decl "nat" measure_space nil)
(* const-decl "[T -> real]" real_fun_ops "reals/")
(member const-decl "bool" sets nil)
(fullset const-decl "set" sets nil) (set type-eq-decl nil sets nil)
(phi_is_simple judgement-tcc nil measure_space nil)
(subset_algebra_fullset name-judgement "(S)" finite_fubini nil)
(measurable_fullset name-judgement "measurable_set[T, S]"
finite_fubini nil)
(mu_fin? const-decl "bool" measure_props nil)
(nn_isf nonempty-type-eq-decl nil nn_integral nil)
(nn_isf? const-decl "bool" nn_integral nil)
(isf nonempty-type-eq-decl nil isf nil)
(c!1 skolem-const-decl "nnreal" finite_fubini nil)
(isf? const-decl "bool" isf nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nu formal-const-decl "finite_measure[T2, S2]" finite_fubini nil)
(measurable_y_section formula-decl nil finite_fubini_scaf nil)
(bounded? const-decl "bool" sup_norm nil)
(nn_integrable_is_integrable judgement-tcc nil integral nil))
shostak))
(integrable_integral_x_section_TCC1 0
(integrable_integral_x_section_TCC1-1 nil 3460343887
("" (skosimp) (("" (rewrite "integrable_x_section") nil nil)) nil)
((integrable_x_section formula-decl nil finite_fubini nil)
(T1 formal-type-decl nil finite_fubini nil)
(T2 formal-type-decl nil finite_fubini nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(bool nonempty-type-eq-decl nil booleans 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)
(sigma_times const-decl "sigma_algebra[[T1, T2]]" product_sigma_def
nil)
(S1 formal-const-decl "sigma_algebra[T1]" finite_fubini nil)
(S2 formal-const-decl "sigma_algebra[T2]" finite_fubini nil)
(bounded_measurable? const-decl "bool" measure_space nil)
(bounded_measurable nonempty-type-eq-decl nil measure_space nil))
nil))
(integrable_integral_x_section 0
(integrable_integral_x_section-1 nil 3473928016
(""
(case "FORALL (h: bounded_measurable[[T1, T2], sigma_times(S1, S2)]):
(forall x,y: 0<=h(x,y)) => integrable?(LAMBDA x: integral(LAMBDA y: h(x, y)))")
(("1" (skosimp)
(("1" (typepred "h!1")
(("1" (inst-cp - "plus(h!1)")
(("1" (inst - "minus(h!1)")
(("1" (split -2)
(("1" (split -3)
(("1"
(lemma "integrable_diff"
("f1"
"LAMBDA x: integral(LAMBDA y: plus(h!1)(x, y))"
"f2"
"LAMBDA x: integral(LAMBDA y: minus(h!1)(x, y))"))
(("1"
(case-replace "((-[T1])
(LAMBDA x: integral(LAMBDA y: plus(h!1)(x, y)),
LAMBDA x: integral(LAMBDA y: minus(h!1)(x, y))))=(LAMBDA x: integral(LAMBDA y: h!1(x, y)))")
(("1" (expand "-" 1)
(("1" (apply-extensionality 1 :hide? t)
(("1"
(lemma "integral_pm"
("f" "LAMBDA y: h!1(x!1, y)"))
(("1" (expand "plus")
(("1" (expand "minus")
(("1"
(replace -1 1 rl)
(("1" (propax) nil nil))
nil))
nil))
nil)
("2" (rewrite "integrable_x_section") nil
nil))
nil)
("2" (skosimp)
(("2" (rewrite "integrable_x_section") nil
nil))
nil)
("3" (skosimp)
(("3"
(lemma "integrable_x_section"
("x" "x!1" "h" "h!1"))
(("3"
(lemma "integrable_minus"
("f" "LAMBDA y: h!1(x!1, y)"))
(("1"
(expand "minus")
(("1" (propax) nil nil))
nil)
("2" (propax) nil nil))
nil))
nil))
nil)
("4" (skosimp)
(("4"
(lemma "integrable_x_section"
("x" "x!1" "h" "h!1"))
(("4"
(lemma "integrable_plus"
("f" "LAMBDA y: h!1(x!1, y)"))
(("1"
(expand "plus")
(("1" (propax) nil nil))
nil)
("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp)
(("2" (rewrite "integrable_x_section") nil nil))
nil))
nil)
("2" (propax) nil nil)
("3" (skosimp)
(("3"
(lemma "integrable_x_section"
("x" "x!1" "h" "h!1"))
(("3" (hide-all-but (-1 1))
(("3"
(lemma
"integrable_minus[T2, S2, to_measure(nu)]"
("f" "LAMBDA y: h!1(x!1, y)"))
(("1" (expand "minus")
(("1" (propax) nil nil)) nil)
("2" (propax) nil nil))
nil))
nil))
nil))
nil)
("4" (propax) nil nil)
("5" (skosimp)
(("5"
(lemma "integrable_x_section"
("x" "x!1" "h" "h!1"))
(("5"
(lemma
"integrable_plus[T2, S2, to_measure(nu)]"
("f" "LAMBDA y: h!1(x!1, y)"))
(("1" (expand "plus") (("1" (propax) nil nil))
nil)
("2" (propax) nil nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but 1) (("2" (grind) nil nil)) nil))
nil)
("2" (hide-all-but 1) (("2" (grind) nil nil)) nil))
nil)
("2" (hide-all-but (-1 1))
(("2" (expand "bounded_measurable?")
(("2" (flatten)
(("2" (split)
(("1" (hide -2)
(("1" (expand "bounded?")
(("1" (skosimp)
(("1" (inst + "c!1")
(("1" (skosimp)
(("1"
(inst - "x!1")
(("1" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (rewrite "minus_measurable") nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (expand "bounded_measurable?")
(("2" (flatten)
(("2" (split)
(("1" (hide -2)
(("1" (expand "bounded?")
(("1" (skosimp)
(("1" (inst + "c!1")
(("1" (skosimp)
(("1" (inst - "x!1")
(("1" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (rewrite "plus_measurable") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (skosimp)
(("2"
(case "forall x: bounded_measurable?(LAMBDA y: h!1(x, y))")
(("1" (case "forall x: integrable?(LAMBDA y: h!1(x, y))")
(("1" (lemma "nn_measurable_def" ("f" "h!1"))
(("1" (split -1)
(("1" (flatten -1)
(("1" (hide -2)
(("1" (split -1)
(("1" (skosimp)
(("1" (typepred "w!1")
(("1"
(case "forall (n:nat): integrable?(LAMBDA x: isf_integral(LAMBDA y: w!1(n)(x, y)))")
(("1"
(lemma
"monotone_convergence_scaf[T1,S1,to_measure(mu)]"
("f"
"LAMBDA x: integral(LAMBDA y: h!1(x, y))"
"F"
"lambda (n:nat): LAMBDA x: isf_integral(LAMBDA y: w!1(n)(x, y))"))
(("1"
(replace 1 -1)
(("1"
(hide 2)
(("1"
(split)
(("1"
(expand
"pointwise_converges_upto?")
(("1"
(flatten)
(("1"
(split)
(("1"
(expand
"pointwise_convergence?")
(("1"
(skosimp)
(("1"
(lemma
"monotone_convergence_scaf[T2,S2,to_measure(nu)]"
("f"
"LAMBDA y: h!1(x!1, y)"
"F"
"lambda (n:nat): LAMBDA y: w!1(n)(x!1, y)"))
(("1"
(expand
"converges_upto?")
(("1"
(split -1)
(("1"
(flatten)
(("1"
(expand "o")
(("1"
(case-replace
"(LAMBDA (n: nat): integral(LAMBDA y: w!1(n)(x!1, y)))=LAMBDA (n: nat):
isf_integral(LAMBDA y: w!1(n)(x!1, y))")
(("1"
(apply-extensionality
:hide?
t)
(("1"
(rewrite
"isf_integral")
(("1"
(rewrite
"isf_x_section"
1)
(("1"
(expand
"isf?")
(("1"
(expand
"mu_fin?")
(("1"
(expand
"to_measure")
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.77 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
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.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
