| 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 348 kB |
|
Quellcode-Bibliothek finite_fubini.prfInteraktion undPortierbarkeitLisp |
|||||||||||||||
|
(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, (("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, (("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, (("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, (("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") (("1" (expand "increasing_nn_simple?") (("1" (inst -5 "x!2") (("1" (expand "nn_simple?") (("1" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (rewrite "isf_x_section" 1) (("2" (expand "isf?") (("2" (expand "mu_fin?") (("2" (expand "to_measure") (("2" (expand "increasing_nn_simple?") (("2" (inst -5 "n!1") (("2" (expand "nn_simple?") (("2" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (lemma "isf_is_integrable[T2, S2, to_measure(nu)]") (("3" (inst - "LAMBDA y: w!1(n!1)(x!1, y)") (("3" (rewrite "isf_x_section") (("3" (expand "isf?") (("3" (expand "mu_fin?") (("3" (expand "to_measure") (("3" (expand "increasing_nn_simple?") (("3" (inst -5 "n!1") (("3" (expand "nn_simple?") (("3" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (rewrite "isf_x_section") (("2" (expand "isf?") (("2" (expand "mu_fin?") (("2" (expand "to_measure") (("2" (expand "increasing_nn_simple?") (("2" (inst -5 "n!1") (("2" (expand "nn_simple?") (("2" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "pointwise_converges_upto?") (("2" (hide 2) (("2" (split) (("1" (expand "pointwise_convergence?") (("1" (skolem + "y!1") (("1" (inst -3 "(x!1,y!1)") nil nil)) nil)) nil) ("2" (expand "pointwise_increasing?") (("2" (skolem + "y!1") (("2" (inst -4 "(x!1,y!1)") nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (expand "o ") (("3" (expand "bounded?") (("3" (split) (("1" (expand "bounded_above?") (("1" (inst -6 "x!1") (("1" (expand "bounded_measurable?") (("1" (flatten) (("1" (expand "bounded?") (("1" (skosimp) (("1" (inst + "c!1*nu(fullset[T2])") (("1" (skolem + "n!1") (("1" (case "forall y: w!1(n!1)(x!1,y) <= c!1") (("1" (expand "increasing_nn_simple?") (("1" (flatten) (("1" (hide -2 -4 -5) (("1" (lemma "integral_ae_le" ("f1" "LAMBDA y: w!1(n!1)(x!1, y)" "f2" "c!1*phi(fullset[T2])")) (("1" (split -1) (("1" (name-replace "LHS" "integral(LAMBDA y: w!1(n!1)(x!1, y))") (("1" (hide-all-but (-1 1)) (("1" (rewrite "integral_scal" -1) (("1" (rewrite "integral_phi" -1) (("1" (expand "mu") (("1" (expand "to_measure") (("1" (propax) nil nil)) nil)) nil) ("2" (expand "mu_fin?") (("2" (expand "to_measure") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 -1)) (("2" (expand "ae_le?") (("2" (expand "pointwise_ae?") (("2" (expand "ae?") (("2" (expand "fullset") (("2" (expand "phi") (("2" (expand "ae_in?") (("2" (expand "member") (("2" (inst + "emptyset[T2]") (("2" (skosimp) (("2" (expand "*") (("2" (inst - "x!2") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (inst -2 "n!1") (("2" (expand "nn_simple?") (("2" (flatten) (("2" (lemma "isf_is_integrable[T2, S2, to_measure(nu)]") (("2" (lemma "isf_x_section" ("i" "w!1(n!1)" "x" "x!1")) (("1" (inst - "LAMBDA (y: T2): w!1(n!1)(x!1, y)") nil nil) ("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" (skosimp) (("2" (hide -1 -2 -5 -7 2) (("2" (inst - "(x!1,y!1)") (("2" (inst - "x!1" "y!1") (("2" (inst - "y!1") (("2" (expand "abs") (("2" (assert) (("2" (rewrite "metric_convergence_def") (("2" (expand "pointwise_increasing?") (("2" (inst - "(x!1,y!1)") (("2" (expand "metric_converges_to") (("2" (expand "ball") (("2" (expand "member") (("2" (name "R" "w!1(n!1)(x!1, y!1)-c!1") (("2" (case "R>0") (("1" (inst - "R") (("1" (skosimp) (("1" (inst -3 "n!1+n!2") (("1" (assert) (("1" (expand "increasing?") (("1" (inst - "n!1" "n!1+n!2") (("1" (name-replace "DRL" "w!1(n!1 + n!2)(x!1, y!1)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (hide-all-but (-1 1 2)) (("2" (grind) 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 "bounded_below?") (("2" (inst + "0") (("2" (skolem + "n!1") (("2" (expand "increasing_nn_simple?") (("2" (expand "nn_simple?") (("2" (flatten) (("2" (inst -2 "n!1") (("2" (flatten) (("2" (lemma "integral_nonneg" ("f" "LAMBDA y: w!1(n!1)(x!1, y)")) (("1" (assert) (("1" (skolem + "y!1") (("1" (inst -2 "(x!1,y!1)") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "isf_is_integrable[T2, S2, to_measure(nu)]") (("2" (inst - "LAMBDA y: w!1(n!1)(x!1, y)") (("2" (rewrite "isf_x_section") (("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)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (lemma "isf_is_integrable[T2, S2, to_measure(nu)]") (("2" (inst - "LAMBDA y: w!1(n!1)(x!1, y)") (("2" (rewrite "isf_x_section") (("2" (expand "isf?") (("2" (expand "mu_fin?") (("2" (expand "to_measure") (("2" (expand "increasing_nn_simple?") (("2" (expand "nn_simple?") (("2" (inst -2 "n!1") (("2" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "pointwise_increasing?") (("2" (skosimp) (("2" (expand "increasing?") (("2" (skolem + ("i!1" "j!1")) (("2" (flatten) (("2" (lemma "isf_integral_le[T2,S2,to_measure(nu)]" ("i1" "LAMBDA y: w!1(i!1)(x!1, y)" "i2" "LAMBDA y: w!1(j!1)(x!1, y)")) (("1" (assert) (("1" (skolem + "y!1") (("1" (inst -5 "(x!1,y!1)") (("1" (inst -5 "i!1" "j!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (rewrite "isf_x_section") (("2" (expand "increasing_nn_simple?") (("2" (flatten) (("2" (inst -3 "j!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) ("3" (rewrite "isf_x_section") (("3" (expand "isf?") (("3" (expand "mu_fin?") (("3" (expand "to_measure") (("3" (expand "increasing_nn_simple?") (("3" (flatten) (("3" (inst -3 "i!1") (("3" (expand "nn_simple?") (("3" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "o" 1) (("2" (expand "bounded?") (("2" (split) (("1" (typepred "h!1") (("1" (expand "bounded_measurable?" -1) (("1" (flatten) (("1" (expand "bounded?" -1) (("1" (skosimp) (("1" (case "forall (n:nat,x,y): w!1(n)(x,y) <= c!1") (("1" (expand "bounded_above?") (("1" (inst + "c!1 * mu(fullset[T1]) * nu(fullset[T2])") (("1" (skolem + "n!1") (("1" (inst -4 "n!1") (("1" (lemma "integral_ae_le" ("f1" "LAMBDA x: isf_integral(LAMBDA y: w!1(n!1)(x, y))" "f2" "(c!1*nu(fullset[T2]))*phi(fullset[T1])")) (("1" (name-replace "LHS" "integral(LAMBDA x: isf_integral(LAMBDA y: w!1(n!1)(x, y)))") (("1" (split -1) (("1" (rewrite "integral_scal" -1) (("1" (rewrite "integral_phi" -1) (("1" (expand "mu") (("1" (expand "to_measure") (("1" (assert) nil nil)) nil)) nil) ("2" (expand "mu_fin?") (("2" (expand "to_measure") (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "ae_le?") (("2" (expand "pointwise_ae?") (("2" (expand "ae?") (("2" (expand "fullset" 1 2) (("2" (expand "fullset" 1 2) (("2" (expand "ae_in?") (("2" (inst + "emptyset[T1]") (("2" (skosimp) (("2" (expand "member") (("2" (expand "*" 2) (("2" (expand "phi") (("2" (expand "member") (("2" (expand "increasing_nn_simple?") (("2" (flatten) (("2" (inst -5 "n!1") (("2" (expand "nn_simple?") (("2" (flatten) (("2" (lemma "isf_integral_le" ("i1" "LAMBDA y: w!1(n!1)(x!1, y)" "i2" "c!1*phi(fullset[T2])")) (("1" (split -1) (("1" (name-replace "LHS1" "isf_integral(LAMBDA y: w!1(n!1)(x!1, y))") (("1" (rewrite "isf_integral_scal" -1) (("1" (rewrite "isf_integral_phi" -1) (("1" (expand "mu") (("1" (expand "to_measure") (("1" (assert) nil nil)) nil)) nil) ("2" (expand "mu_fin?") (("2" (expand "to_measure") (("2" (propax) nil nil)) nil)) nil)) nil) ("2" (rewrite "isf_phi" 1) (("2" (expand "mu_fin?") (("2" (expand "to_measure") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skolem + "y!1") (("2" (expand "*") (("2" (expand "fullset") (("2" (expand "phi") (("2" (expand "member") (("2" (inst - "n!1" "x!1" "y!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "isf_scal") (("2" (rewrite "isf_phi") (("2" (expand "mu_fin?") (("2" (expand "to_measure") (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("3" (rewrite "isf_x_section") (("3" (expand "isf?") (("3" (expand "mu_fin?") (("3" (expand "to_measure") (("3" (propax) 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" (propax) nil nil) ("3" (skosimp) (("3" (expand "increasing_nn_simple?") (("3" (flatten) (("3" (expand "nn_simple?") (("3" (inst -5 "n!1") (("3" (flatten) (("3" (rewrite "isf_x_section" 1) (("3" (expand "isf?") (("3" (expand "mu_fin?") (("3" (expand "to_measure") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 -5 -8 1)) (("2" (skosimp) (("2" (inst - "(x!1,y!1)") (("2" (inst - "x!1" "y!1") (("2" (expand "abs") (("2" (expand "pointwise_converges_upto?") (("2" (flatten) (("2" (assert) (("2" (expand "pointwise_convergence?") (("2" (expand "pointwise_increasing?") (("2" (inst - "(x!1,y!1)") (("2" (inst - "(x!1,y!1)") (("2" (rewrite "metric_convergence_def") (("2" (expand "metric_converges_to") (("2" (expand "ball") (("2" (expand "member") (("2" (name "R" "w!1(n!1)(x!1, y!1)-c!1") (("2" (case "R>0") (("1" (inst - "R") (("1" (skosimp) (("1" (inst - "n!1+n!2") (("1" (expand "increasing?") (("1" (inst - "n!1" "n!1+n!2") (("1" (assert) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (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)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "bounded_below?") (("2" (inst + "0") (("2" (skolem + "n!1") (("2" (inst - "n!1") (("2" (lemma "integral_nonneg[T1,S1,to_measure(mu)]" ("f" "LAMBDA x: isf_integral(LAMBDA y: w!1(n!1)(x, y))")) (("1" (assert) (("1" (skosimp) (("1" (hide 2) (("1" (expand "increasing_nn_simple?") (("1" (flatten) (("1" (expand "nn_simple?") (("1" (inst - "n!1") (("1" (flatten) (("1" (lemma "isf_x_section" ("i" "w!1(n!1)" "x" "x!1")) (("1" (lemma "isf_integral_pos" ("i" "LAMBDA (y: T2): w!1(n!1)(x!1, y)")) (("1" (assert) (("1" (skolem + "y!1") (("1" (inst - "(x!1,y!1)") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil) ("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) ("2" (propax) nil nil) ("3" (skosimp) (("3" (expand "increasing_nn_simple?") (("3" (expand "nn_simple?") (("3" (flatten) (("3" (inst -2 "n!1") (("3" (flatten) (("3" (rewrite "isf_x_section" 1) (("3" (expand "isf?") (("3" (expand "mu_fin?") (("3" (expand "to_measure") (("3" (propax) 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" (propax) nil nil)) nil) ("2" (skosimp) (("2" (lemma "isf_integral_x" ("i" "w!1(n!1)")) (("1" (propax) nil nil) ("2" (expand "increasing_nn_simple?") (("2" (flatten) (("2" (inst - "n!1") (("2" (expand "isf?") (("2" (expand "mu_fin?") (("2" (expand "to_measure") (("2" (expand "nn_simple?") (("2" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (rewrite "isf_x_section" 1) (("3" (expand "increasing_nn_simple?") (("3" (flatten) (("3" (inst - "n!1") (("3" (expand "nn_simple?") (("3" (flatten) (("3" (expand "isf?") (("3" (expand "mu_fin?") (("3" (expand "to_measure") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "h!1") (("2" (expand "bounded_measurable?") (("2" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil) ("2" (skosimp) (("2" (inst - "x!1") (("2" (hide -2 -3 2) (("2" (use "bounded_measurable_is_integrable[T2,S2,nu]") nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (hide-all-but 1) (("2" (typepred "h!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, x!2)") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "measurable_x_section" ("x" "x!1" "m" "h!1")) (("1" (propax) nil nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (rewrite "integrable_x_section") nil nil)) nil)) nil) ((bounded_measurable_is_integrable judgement-tcc nil finite_integral nil) (h!1 skolem-const-decl "bounded_measurable[[T1, T2], sigma_times(S1, S2)]" finite_fubini nil) (x!1 skolem-const-decl "T1" finite_fubini nil) (nn_measurable_def formula-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) (sequence type-eq-decl nil sequences nil) (increasing_nn_simple? const-decl "bool" measure_space nil) (increasing_nn_simple nonempty-type-eq-decl nil measure_space nil) (isf_integral_x formula-decl nil finite_fubini_scaf nil) (monotone_convergence_scaf formula-decl nil integral_convergence_scaf nil) (subset_algebra_fullset name-judgement "(S)" finite_fubini nil) (measurable_fullset name-judgement "measurable_set[T, S]" finite_fubini nil) (isf_phi judgement-tcc nil isf nil) (isf_integral_phi formula-decl nil isf nil) (isf_integral_scal formula-decl nil isf nil) (isf_scal judgement-tcc nil isf nil) (null_emptyset name-judgement "null_set" finite_fubini nil) (subset_algebra_emptyset name-judgement "(S)" finite_fubini nil) (simple_scal application-judgement "simple" finite_fubini nil) (bounded_scal application-judgement "bounded[T1]" finite_fubini nil) (phi_is_simple application-judgement "simple" finite_fubini nil) (R skolem-const-decl "real" finite_fubini nil) (isf_integral_pos formula-decl nil isf nil) (pointwise_converges_upto? const-decl "bool" pointwise_convergence nil) (n!1 skolem-const-decl "nat" finite_fubini nil) (converges_upto? const-decl "bool" convergence_aux "metric_space/") (bounded? const-decl "bool" real_fun_preds "reals/") (bounded_below? const-decl "bool" real_fun_preds "reals/") (integral_nonneg formula-decl nil integral nil) (n!1 skolem-const-decl "nat" finite_fubini nil) (bounded_above? const-decl "bool" real_fun_preds "reals/") (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (subset_algebra_fullset name-judgement "(S)" finite_fubini nil) (measurable_fullset name-judgement "measurable_set[T, S]" finite_fubini nil) (fullset const-decl "set" sets nil) (set type-eq-decl nil sets nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (phi_is_simple application-judgement "simple" finite_fubini nil) (bounded_scal application-judgement "bounded[T2]" finite_fubini nil) (simple_scal application-judgement "simple" finite_fubini nil) (integral_ae_le formula-decl nil integral nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (phi const-decl "nat" measure_space nil) (pointwise_ae? const-decl "bool" measure_theory nil) (ae_in? const-decl "bool" measure_theory nil) (subset_algebra_emptyset name-judgement "(S)" finite_fubini nil) (null_emptyset name-judgement "null_set" finite_fubini nil) (finite_emptyset name-judgement "finite_set[T]" sigma_countable "sigma_set/") (finite_emptyset name-judgement "finite_set[T]" countable_setofsets "sets_aux/") (finite_emptyset name-judgement "finite_set[T]" countable_props "sets_aux/") (finite_emptyset name-judgement "finite_set" finite_sets nil) (emptyset const-decl "set" sets nil) (negligible nonempty-type-eq-decl nil measure_theory nil) (negligible_set? const-decl "bool" measure_theory nil) (TRUE const-decl "bool" booleans nil) (member const-decl "bool" sets nil) (ae? const-decl "bool" measure_theory nil) (ae_le? const-decl "bool" measure_theory nil) (integral_scal formula-decl nil integral nil) (real_times_real_is_real application-judgement "real" reals nil) (mu const-decl "nnreal" measure_props nil) (integral_phi formula-decl nil integral nil) (measurable_set? const-decl "bool" measure_space_def nil) (measurable_set nonempty-type-eq-decl nil measure_space_def nil) (n!1 skolem-const-decl "nat" finite_fubini nil) (- const-decl "[numfield -> numfield]" number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (metric_convergence_def formula-decl nil metric_space "metric_space/") (ball const-decl "set[T]" metric_space_def "metric_space/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (R skolem-const-decl "real" finite_fubini nil) (posreal nonempty-type-eq-decl nil real_types nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (increasing? const-decl "bool" real_fun_preds "reals/") (> const-decl "bool" reals nil) (metric_converges_to const-decl "bool" metric_space_def "metric_space/") (pointwise_increasing? const-decl "bool" pointwise_convergence nil) (n!1 skolem-const-decl "nat" finite_fubini nil) (isf_is_integrable judgement-tcc nil integral nil) (isf_integral formula-decl nil integral nil) (nn_simple? const-decl "bool" measure_space nil) (mu_fin? const-decl "bool" measure_props nil) (isf_x_section formula-decl nil finite_fubini_scaf nil) (fm_times const-decl "finite_measure[[T1, T2], sigma_times(S1, S2)]" product_finite_measure nil) (w!1 skolem-const-decl "increasing_nn_simple[[T1, T2], sigma_times(S1, S2)]" finite_fubini nil) (x!1 skolem-const-decl "T1" finite_fubini nil) (O const-decl "T3" function_props nil) (pointwise_convergence? const-decl "bool" pointwise_convergence nil) (isf_integral_le formula-decl nil isf nil) (isf_integral const-decl "real" isf nil) (isf nonempty-type-eq-decl nil isf nil) (isf? const-decl "bool" isf nil) (measurable_x_section formula-decl nil finite_fubini_scaf nil) (plus const-decl "[T -> nnreal]" real_fun_ops_aux "reals/") (h!1 skolem-const-decl "bounded_measurable[[T1, T2], sigma_times(S1, S2)]" finite_fubini nil) (measurable_function nonempty-type-eq-decl nil measure_space_def nil) (measurable_function? const-decl "bool" measure_space_def nil) (minus_measurable judgement-tcc nil measure_space nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (bounded? const-decl "bool" sup_norm 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) (integrable_diff judgement-tcc nil integral nil) (integrable_plus judgement-tcc nil integral nil) (integrable_minus judgement-tcc nil integral nil) (minus_real_is_real application-judgement "real" reals nil) (integral_pm formula-decl nil integral nil) (integrable_x_section formula-decl nil finite_fubini nil) (real_minus_real_is_real application-judgement "real" reals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (- const-decl "[T -> real]" real_fun_ops "reals/") (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus const-decl "[T -> nnreal]" real_fun_ops_aux "reals/") (plus_measurable judgement-tcc nil measure_space nil) (NOT const-decl "[bool -> bool]" booleans 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) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" 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) (integrable? const-decl "bool" integral nil) (nu formal-const-decl "finite_measure[T2, S2]" finite_fubini nil) (integrable nonempty-type-eq-decl nil integral nil) (integral const-decl "real" integral nil)) shostak)) (integrable_integral_y_section_TCC1 0 (integrable_integral_y_section_TCC1-1 nil 3460343887 ("" (skosimp) (("" (rewrite "integrable_y_section") nil nil)) nil) ((integrable_y_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_y_section 0 (integrable_integral_y_section-1 nil 3473946964 ("" (case "FORALL (h: bounded_measurable[[T1, T2], sigma_times(S1, S2)]): (forall x,y: 0<=h(x,y)) => integrable?(LAMBDA y: integral(LAMBDA x: 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 y: integral(LAMBDA x: plus(h!1)(x, y))" "f2" "LAMBDA y: integral(LAMBDA x: minus(h!1)(x, y))")) (("1" (case-replace "((-[T2]) (LAMBDA y: integral(LAMBDA x: plus(h!1)(x, y)), LAMBDA y: integral(LAMBDA x: minus(h!1)(x, y))))=(LAMBDA y: integral(LAMBDA x: h!1(x, y))) (("1" (expand "-") (("1" (apply-extensionality :hide? t) (("1" (hide 2) (("1" (rewrite "integral_diff" 1 :dir rl) (("1" (case-replace "((LAMBDA x: plus(h!1)(x, x!1)) - (LAMBDA x: minus(h!1)(x, x!1)))=(LAMBDA x: h!1(x, x!1))") (("1" (apply-extensionality :hide? t) (("1" (hide-all-but 1) (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (lemma "integrable_y_section" ("h" "h!1" "y" "x!1")) (("2" (lemma "integrable_minus" ("f" "LAMBDA x: h!1(x, x!1)")) (("1" (expand "minus") (("1" (propax) nil nil)) nil) ("2" (propax) nil nil)) nil)) nil) ("3" (lemma "integrable_y_section" ("h" "h!1" "y" "x!1")) (("3" (lemma "integrable_plus" ("f" "LAMBDA x: h!1(x, x!1)")) (("1" (expand "plus") (("1" (propax) nil nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (rewrite "integrable_y_section") nil nil)) nil) ("3" (skosimp) (("3" (lemma "integrable_y_section" ("h" "h!1" "y" "x!1")) (("3" (lemma "integrable_minus" ("f" "LAMBDA x: h!1(x, x!1)")) (("1" (expand "minus") (("1" (propax) nil nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil) ("4" (skosimp) (("4" (lemma "integrable_y_section" ("h" "h!1" "y" "x!1")) (("4" (lemma "integrable_plus" ("f" "LAMBDA x: h!1(x, x!1)")) (("1" (expand "plus") (("1" (propax) nil nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (rewrite "integrable_y_section") nil nil)) nil)) nil) ("2" (propax) nil nil) ("3" (skosimp) (("3" (lemma "integrable_y_section" ("y" "y!1" "h" "h!1")) (("3" (lemma "integrable_minus[T1, S1, to_measure(mu)]" ("f" "LAMBDA x: h!1(x, y!1)")) (("1" (expand "minus") (("1" (propax) nil nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil) ("4" (propax) nil nil) ("5" (skosimp) (("5" (lemma "integrable_y_section" ("y" "y!1" "h" "h!1")) (("5" (lemma "integrable_plus[T1, S1, to_measure(mu)]" ("f" "LAMBDA x: h!1(x, y!1)")) (("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 y: bounded_measurable?(LAMBDA x: h!1(x, y))") (("1" (case "forall y: integrable?(LAMBDA x: h!1(x, y))") (("1" (lemma "nn_measurable_def" ("f" "h!1")) (("1" (replace -4) (("1" (flatten) (("1" (hide -2) (("1" (split -1) (("1" (skosimp) (("1" (typepred "h!1") (("1" (expand "bounded_measurable?" -1) (("1" (flatten) (("1" (expand "bounded?" -1) (("1" (hide -2) (("1" (skosimp) (("1" (case "forall (n:nat): isf?(w!1(n))") (("1" (case "forall (n:nat,x,y): 0<=w!1(n)(x,y)&w!1(n)(x,y)<=h!1(x,y)") (("1" (case "forall (n:nat): integrable?(LAMBDA y: isf_integral(LAMBDA x: w!1(n)(x, y)))") (("1" (lemma "monotone_convergence_scaf[T2,S2,to_measure(nu)]" ("f" "LAMBDA y: integral(LAMBDA x: h!1(x, y))" "F" "lambda (n:nat): LAMBDA y: isf_integral(LAMBDA x: 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" (skolem + "y!1") (("1" (lemma "monotone_convergence_scaf[T1,S1,to_measure(mu)]" ("f" "LAMBDA x: h!1(x, y!1)" "F" "lambda (n:nat): LAMBDA x: w!1(n)(x, y!1)")) (("1" (expand "converges_upto?") (("1" (expand "o") (("1" (assert) (("1" (case-replace "(LAMBDA (x_1: nat): integral(LAMBDA x: w!1(x_1)(x, y!1)))=LAMBDA (n_1: nat): isf_integral(LAMBDA x: w!1(n_1)(x, y!1))") (("1" (hide -1) (("1" (replace 1 -1) (("1" (hide 2) (("1" (split) (("1" (expand "pointwise_converges_upto?") (("1" (split) (("1" (expand "pointwise_convergence?") (("1" (skosimp) (("1" (inst -5 "(x!1,y!1)") nil nil)) nil)) nil) ("2" (expand "pointwise_increasing?") (("2" (skosimp) (("2" (inst -6 "(x!1,y!1)") nil nil)) nil)) nil)) nil)) nil) ("2" (expand "bounded?") (("2" (split) (("1" (expand "bounded_above?") (("1" (inst + "c!1*mu(fullset[T1])") (("1" (skolem + "n!1") (("1" (inst -2 "n!1" "_" "y!1") (("1" (inst -3 "n!1") (("1" (lemma "isf_y_section" ("i" "w!1(n!1)" "y" "y!1")) (("1" (lemma "isf_integral_le" ("i1" "LAMBDA x: w!1(n!1)(x, y!1)" "i2" "c!1*phi(fullset[T1])")) (("1" (split -1) (("1" (name-replace "LHS1" "isf_integral(LAMBDA x: w!1(n!1)(x, y!1))") (("1" (rewrite "isf_integral_scal") (("1" (rewrite "isf_integral_phi") (("1" (expand "mu") (("1" (expand "to_measure") (("1" (propax) nil nil)) nil)) nil) ("2" (expand "mu_fin?") (("2" (expand "to_measure") (("2" (propax) nil nil)) nil)) nil)) nil) ("2" (rewrite "isf_phi") (("2" (expand "mu_fin?") (("2" (expand "to_measure") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (expand "fullset") (("2" (expand "phi") (("2" (expand "member") (("2" (expand "*") (("2" (hide-all-but (-3 -5 -10 1)) (("2" (inst - "x!1") (("2" (inst - "(x!1,y!1)") (("2" (inst - "x!1" "y!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "isf_scal") (("2" (rewrite "isf_phi") (("2" (expand "mu_fin?") (("2" (expand "to_measure") (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("3" (propax) nil nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "bounded_below?") (("2" (inst + "0") (("2" (skolem + "n!1") (("2" (inst -3 "n!1") (("2" (lemma "isf_y_section" ("y" "y!1" "i" "w!1(n!1)")) (("1" (lemma "isf_integral_pos" ("i" "LAMBDA x: w!1(n!1)(x, y!1)")) (("1" (split -1) (("1" (assert) nil nil) ("2" (skosimp) (("2" (inst - "n!1" "x!1" "y!1") (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (apply-extensionality :hide? t) (("1" (inst -4 "x!1") (("1" (lemma "isf_y_section" ("i" "w!1(x!1)" "y" "y!1")) (("1" (rewrite "isf_integral") nil nil) ("2" (propax) nil nil)) nil)) nil) ("2" (skosimp) (("2" (inst -4 "n!1") (("2" (rewrite "isf_y_section" 1) nil nil)) nil)) nil) ("3" (skolem + "n!1") (("3" (inst -4 "n!1") (("3" (lemma "isf_y_section" ("y" "y!1" "i" "w!1(n!1)")) (("1" (lemma "isf_is_integrable[T1, S1, to_measure(mu)]") (("1" (inst - "LAMBDA x: w!1(n!1)(x, y!1)") nil nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (inst -4 "n!1") (("3" (lemma "isf_y_section" ("y" "y!1" "i" "w!1(n!1)")) (("1" (propax) nil nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (inst -3 "n!1") (("2" (lemma "isf_y_section" ("y" "y!1" "i" "w!1(n!1)")) (("1" (rewrite "isf_is_integrable" 1) nil nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "pointwise_increasing?") (("2" (skolem + "y!1") (("2" (expand "increasing?") (("2" (skolem + ("i!1" "j!1")) (("2" (flatten) (("2" (hide-all-but (1 -1 -7 -4)) (("2" (inst-cp - "i!1") (("2" (inst - "j!1") (("2" (lemma "isf_y_section" ("i" "w!1(i!1)" "y" "y!1")) (("1" (lemma "isf_y_section" ("i" "w!1(j!1)" "y" "y!1")) (("1" (lemma "isf_integral_le" ("i1" "LAMBDA x: w!1(i!1)(x, y!1)" "i2" "LAMBDA x: w!1(j!1)(x, y!1)")) (("1" (assert) (("1" (skosimp) (("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) ("2" (expand "o") (("2" (expand "bounded?") (("2" (split) (("1" (expand "bounded_above?") (("1" (inst + "mu(fullset[T1])*nu(fullset[T2])*c!1") (("1" (skolem + "n!1") (("1" (inst - "n!1") (("1" (inst - "n!1" "_" "_") (("1" (inst - "n!1") (("1" (lemma "integral_ae_le" ("f1" "LAMBDA y: isf_integral(LAMBDA x: w!1(n!1)(x, y))" "f2" "(c!1*mu(fullset[T1]))*phi(fullset[T2])")) (("1" (split -1) (("1" (name-replace "LHS" "integral(LAMBDA y: isf_integral(LAMBDA x: w!1(n!1)(x, y)))") (("1" (rewrite "integral_scal" -1) (("1" (rewrite "integral_phi" -1) (("1" (expand "mu") (("1" (expand "to_measure") (("1" (propax) nil nil)) nil)) nil) ("2" (expand "mu_fin?") (("2" (expand "to_measure") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "ae_le?") (("2" (expand "pointwise_ae?") (("2" (expand "ae?") (("2" (expand "fullset" 1 2) (("2" (expand "fullset" 1 2) (("2" (expand "phi") (("2" (expand "member") (("2" (expand "ae_in?") (("2" (expand "member") (("2" (inst + " emptyset[T2]") (("2" (skolem + "y!1") (("2" (flatten) (("2" (expand "*" 2) (("2" (lemma "isf_y_section" ("i" "w!1(n!1)" "y" "y!1")) (("1" (hide 1) (("1" (lemma "isf_integral_le" ("i1" "LAMBDA x: w!1(n!1)(x, y!1)" "i2" "c!1*phi(fullset[T1])")) (("1" (split -1) (("1" (rewrite "isf_integral_scal") (("1" (rewrite "isf_integral_phi") (("1" (assert) (("1" (expand "mu") (("1" (expand "to_measure") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "mu_fin?") (("2" (expand "to_measure") (("2" (propax) nil nil)) nil)) nil)) nil) ("2" (rewrite "isf_phi") (("2" (expand "mu_fin?") (("2" (expand "to_measure") (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (expand "fullset") (("2" (expand "phi") (("2" (expand "*") (("2" (expand "member") (("2" (inst - "x!1" "y!1") (("2" (flatten) (("2" (inst -10 "x!1" "y!1") (("2" (inst -6 "(x!1,y!1)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "isf_scal") (("2" (rewrite "isf_phi") (("2" (expand "mu_fin?") (("2" (expand "to_measure") (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("3" (propax) nil nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil) ("3" (skosimp) (("3" (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 - "n!1") (("2" (inst - "n!1") (("2" (lemma "isf_y_section" ("i" "w!1(n!1)")) (("1" (lemma "integral_nonneg" ("f" "LAMBDA y: isf_integral(LAMBDA x: w!1(n!1)(x, y))")) (("1" (assert) (("1" (skolem + "y!1") (("1" (hide 2) (("1" (inst - "y!1") (("1" (lemma "isf_integral_pos" ("i" "LAMBDA x: w!1(n!1)(x, y!1)")) (("1" (assert) (("1" (skosimp) (("1" (inst -3 "n!1" "x!1" "y!1") (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil) ("3" (propax) nil nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil) ("3" (propax) nil nil)) nil) ("2" (skosimp) (("2" (inst -2 "n!1") (("2" (rewrite "isf_integral_y" 1) (("2" (hide-all-but (-2 1)) (("2" (case-replace "(LAMBDA (x, y): w!1(n!1)(x, y))=w!1(n!1)") (("2" (apply-extensionality :hide? t) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (inst -2 "n!1") (("3" (hide-all-but (-2 1)) (("3" (rewrite "isf_y_section") nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-3 1)) (("2" (skosimp) (("2" (expand "pointwise_converges_upto?") (("2" (flatten) (("2" (typepred "w!1") (("2" (expand "increasing_nn_simple?") (("2" (flatten) (("2" (inst - "n!1") (("2" (expand "nn_simple?") (("2" (flatten) (("2" (inst - "(x!1,y!1)") (("2" (assert) (("2" (hide -1 -2 -3) (("2" (expand "pointwise_convergence?") (("2" (expand "pointwise_increasing?") (("2" (inst - "(x!1,y!1)") (("2" (inst - "(x!1,y!1)") (("2" (rewrite "metric_convergence_def") (("2" (expand "metric_converges_to") (("2" (name "R" "w!1(n!1)(x!1, y!1) - h!1(x!1, y!1)") (("2" (case "R>0") (("1" (inst - "R") (("1" (skosimp) (("1" (inst - "n!1+n!2") (("1" (expand "ball") (("1" (expand "increasing?") (("1" (inst - "n!1" "n!1+n!2") (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (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)) nil)) nil)) nil)) nil) ("2" (typepred "w!1") (("2" (expand "increasing_nn_simple?") (("2" (flatten) (("2" (skosimp) (("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)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "h!1") (("2" (expand "bounded_measurable?") (("2" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (inst - "y!1") (("2" (lemma "bounded_measurable_is_integrable[T1,S1,mu]") (("2" (inst - "LAMBDA x: h!1(x, y!1)") nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (typepred "h!1") (("2" (expand "bounded_measurable?") (("2" (flatten) (("2" (hide 2 -3) (("2" (split) (("1" (hide -2) (("1" (expand "bounded?") (("1" (skosimp) (("1" (inst + "c!1") (("1" (skosimp) (("1" (inst - "(x!1,y!1)") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "measurable_y_section" ("m" "h!1" "y" "y!1")) (("1" (propax) nil nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (skosimp) (("3" (typepred "h!1") (("3" (lemma "bounded_measurable_is_integrable[T1, S1, mu]") (("3" (inst - "LAMBDA x: h!1(x, y1!1)") (("3" (hide 2 3) (("3" (expand "bounded_measurable?") (("3" (flatten) (("3" (split) (("1" (hide -2 -3) (("1" (expand "bounded?") (("1" (skosimp) (("1" (inst + "c!1") (("1" (skosimp) (("1" (inst - "(x!1,y1!1)") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "measurable_y_section" ("m" "h!1" "y" "y1!1")) (("1" (propax) nil nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((h!1 skolem-const-decl "bounded_measurable[[T1, T2], sigma_times[T1, T2](S1, S2)]" finite_fubini nil) (y1!1 skolem-const-decl "T2" finite_fubini nil) (bounded_measurable_is_integrable judgement-tcc nil finite_integral nil) (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) (nn_measurable_def formula-decl nil measure_space nil) (increasing_nn_simple nonempty-type-eq-decl nil measure_space nil) (increasing_nn_simple? const-decl "bool" measure_space nil) (sequence type-eq-decl nil sequences nil) (isf? const-decl "bool" isf nil) (fm_times const-decl "finite_measure[[T1, T2], sigma_times(S1, S2)]" product_finite_measure nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (nn_simple? const-decl "bool" measure_space nil) (metric_converges_to const-decl "bool" metric_space_def "metric_space/") (> const-decl "bool" reals 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) (R skolem-const-decl "real" finite_fubini nil) (metric_convergence_def formula-decl nil metric_space "metric_space/") (nonneg_real nonempty-type-eq-decl nil real_types nil) (- const-decl "[numfield -> numfield]" number_fields nil) (isf nonempty-type-eq-decl nil isf nil) (isf_integral const-decl "real" isf nil) (increasing? const-decl "bool" real_fun_preds "reals/") (pointwise_convergence? const-decl "bool" pointwise_convergence nil) (O const-decl "T3" function_props nil) (pointwise_increasing? const-decl "bool" pointwise_convergence nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (subset_algebra_fullset name-judgement "(S)" finite_fubini nil) (measurable_fullset name-judgement "measurable_set[T, S]" finite_fubini nil) (fullset const-decl "set" sets nil) (set type-eq-decl nil sets nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (isf_y_section formula-decl nil finite_fubini_scaf nil) (isf_scal judgement-tcc nil isf nil) (isf_integral_scal formula-decl nil isf nil) (real_times_real_is_real application-judgement "real" reals nil) (mu const-decl "nnreal" measure_props nil) (isf_integral_phi formula-decl nil isf nil) (measurable_set? const-decl "bool" measure_space_def nil) (measurable_set nonempty-type-eq-decl nil measure_space_def nil) (mu_fin? const-decl "bool" measure_props nil) (isf_phi judgement-tcc nil isf nil) (member const-decl "bool" sets nil) (phi const-decl "nat" measure_space nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (isf_integral_le formula-decl nil isf nil) (simple_scal application-judgement "simple" finite_fubini nil) (bounded_scal application-judgement "bounded[T1]" finite_fubini nil) (phi_is_simple application-judgement "simple" finite_fubini nil) (bounded_above? const-decl "bool" real_fun_preds "reals/") (isf_integral_pos formula-decl nil isf nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (bounded_below? const-decl "bool" real_fun_preds "reals/") (bounded? const-decl "bool" real_fun_preds "reals/") (n!1 skolem-const-decl "nat" finite_fubini nil) (isf_is_integrable judgement-tcc nil integral nil) (isf_integral formula-decl nil integral nil) (w!1 skolem-const-decl "increasing_nn_simple[[T1, T2], sigma_times(S1, S2)]" finite_fubini nil) (y!1 skolem-const-decl "T2" finite_fubini nil) (converges_upto? const-decl "bool" convergence_aux "metric_space/") (pointwise_converges_upto? const-decl "bool" pointwise_convergence nil) (integral_nonneg formula-decl nil integral nil) (phi_is_simple application-judgement "simple" finite_fubini nil) (bounded_scal application-judgement "bounded[T2]" finite_fubini nil) (simple_scal application-judgement "simple" finite_fubini nil) (integral_ae_le formula-decl nil integral nil) (pointwise_ae? const-decl "bool" measure_theory nil) (ae_in? const-decl "bool" measure_theory nil) (subset_algebra_emptyset name-judgement "(S)" finite_fubini nil) (null_emptyset name-judgement "null_set" finite_fubini nil) (finite_emptyset name-judgement "finite_set[T]" sigma_countable "sigma_set/") (finite_emptyset name-judgement "finite_set[T]" countable_setofsets "sets_aux/") (finite_emptyset name-judgement "finite_set[T]" countable_props "sets_aux/") (finite_emptyset name-judgement "finite_set" finite_sets nil) (emptyset const-decl "set" sets nil) (negligible nonempty-type-eq-decl nil measure_theory nil) (negligible_set? const-decl "bool" measure_theory nil) (TRUE const-decl "bool" booleans nil) (ae? const-decl "bool" measure_theory nil) (ae_le? const-decl "bool" measure_theory nil) (integral_phi formula-decl nil integral nil) (integral_scal formula-decl nil integral nil) (measurable_fullset name-judgement "measurable_set[T, S]" finite_fubini nil) (subset_algebra_fullset name-judgement "(S)" finite_fubini nil) (monotone_convergence_scaf formula-decl nil integral_convergence_scaf nil) (isf_integral_y formula-decl nil finite_fubini_scaf nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (measurable_y_section formula-decl nil finite_fubini_scaf nil) (plus const-decl "[T -> nnreal]" real_fun_ops_aux "reals/") (h!1 skolem-const-decl "bounded_measurable[[T1, T2], sigma_times(S1, S2)]" finite_fubini nil) (measurable_function nonempty-type-eq-decl nil measure_space_def nil) (measurable_function? const-decl "bool" measure_space_def nil) (minus_measurable judgement-tcc nil measure_space nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (bounded? const-decl "bool" sup_norm nil) (integrable_diff judgement-tcc nil integral nil) (integrable_plus judgement-tcc nil integral nil) (integrable_y_section formula-decl nil finite_fubini nil) (integrable_minus judgement-tcc nil integral 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) (integral_diff formula-decl nil integral nil) (real_minus_real_is_real application-judgement "real" reals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (- const-decl "[T -> real]" real_fun_ops "reals/") (minus const-decl "[T -> nnreal]" real_fun_ops_aux "reals/") (plus_measurable judgement-tcc nil measure_space nil) (NOT const-decl "[bool -> bool]" booleans 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) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" 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) (integrable? const-decl "bool" integral nil) (mu formal-const-decl "finite_measure[T1, S1]" finite_fubini nil) (integrable nonempty-type-eq-decl nil integral nil) (integral const-decl "real" integral nil)) shostak)) (integral_integral_x_section_TCC1 0 (integral_integral_x_section_TCC1-1 nil 3460345328 ("" (skosimp) (("" (rewrite "integrable_integral_x_section") nil nil)) nil) ((integrable_integral_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)) (integral_integral_x_section_TCC2 0 (integral_integral_x_section_TCC2-1 nil 3460345328 ("" (skosimp) (("" (typepred "h!1") (("" (lemma "bounded_measurable_is_integrable[[T1, T2], sigma_times(S1, S2),fm_times(mu, nu)]") (("" (inst - "h!1") nil nil)) nil)) nil)) nil) ((bounded_measurable nonempty-type-eq-decl nil measure_space nil) (bounded_measurable? const-decl "bool" measure_space 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) (bounded_measurable_is_integrable judgement-tcc nil finite_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) (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)) nil)) (integral_integral_x_section 0 (integral_integral_x_section-1 nil 3473945614 ("" (skosimp) (("" (typepred "h!1") (("" (lemma "bounded_measurable_is_integrable[[T1,T2],sigma_times(S1,S2),fm_times(mu,nu)]") (("" (inst - "h!1") (("" (rewrite "finite_fubini1" 1) (("" (lemma "finite_integrable_is_integrable1" ("f" "h!1")) (("1" (lemma "integrable_integral_x_section" ("h" "h!1")) (("1" (lemma "integral_ae_eq[T1,S1,to_measure(mu)]" ("f" "LAMBDA x: integral(LAMBDA y: h!1(x, y))" "h" "integral1(h!1)")) (("1" (assert) (("1" (hide 2 -1 -3) (("1" (expand "ae_eq?") (("1" (expand "restrict") (("1" (expand "pointwise_ae?") (("1" (expand "ae?") (("1" (expand "fullset") (("1" (expand "ae_in?") (("1" (expand "member") (("1" (name "FF" "integral1(h!1)") (("1" (replace -1) (("1" (name "NI" "null_integrable1(h!1)") (("1" (expand "integral1" -2) (("1" (replace -1) (("1" (expand "member") (("1" (inst + "NI`1") (("1" (skosimp) (("1" (replace -2 2 rl) (("1" (assert) (("1" (hide -2) (("1" (lemma "null_integral1_def" ("h1" "h!1" "N1" "NI`1" "f" "NI`2" "x" "x!1")) (("1" (expand "member") (("1" (decompose-equality 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) ("2" (propax) nil nil) ("3" (skosimp) (("3" (lemma "integrable_x_section" ("h" "h!1" "x" "x!1")) (("3" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((bounded_measurable nonempty-type-eq-decl nil measure_space nil) (bounded_measurable? const-decl "bool" measure_space 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) (finite_integrable_is_integrable1 formula-decl nil finite_fubini nil) (integral1 const-decl "integrable[T1, S1, mu]" product_integral_def nil) (integrable1 nonempty-type-eq-decl nil product_integral_def nil) (integrable1? const-decl "bool" product_integral_def nil) (measurable_function nonempty-type-eq-decl nil measure_space_def nil) (measurable_function? const-decl "bool" measure_space_def nil) (integral const-decl "real" integral nil) (integral_ae_eq formula-decl nil integral nil) (restrict const-decl "R" restrict nil) (measurable_fullset name-judgement "measurable_set[T, S]" finite_fubini nil) (subset_algebra_fullset name-judgement "(S)" finite_fubini nil) (ae? const-decl "bool" measure_theory nil) (ae_in? const-decl "bool" measure_theory nil) (= const-decl "[T, T -> boolean]" equalities nil) (set type-eq-decl nil sets nil) (null_set? const-decl "bool" measure_theory nil) (null_set nonempty-type-eq-decl nil measure_theory nil) (null_integrable1 const-decl "[null_set[T1, S1, mu], integrable[T1, S1, mu]]" product_integral_def nil) (negligible nonempty-type-eq-decl nil measure_theory nil) (negligible_set? const-decl "bool" measure_theory nil) (TRUE const-decl "bool" booleans nil) (null_integral1_def formula-decl nil product_integral_def nil) (member const-decl "bool" sets nil) (fullset const-decl "set" sets nil) (pointwise_ae? const-decl "bool" measure_theory nil) (ae_eq? const-decl "bool" measure_theory nil) (integrable_x_section formula-decl nil finite_fubini nil) (integrable_integral_x_section formula-decl nil finite_fubini nil) (integrable nonempty-type-eq-decl nil integral nil) (integrable? const-decl "bool" integral 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_fubini1 formula-decl nil finite_fubini nil) (bounded_measurable_is_integrable judgement-tcc nil finite_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) (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)) shostak)) (integral_integral_y_section_TCC1 0 (integral_integral_y_section_TCC1-1 nil 3460345328 ("" (skosimp) (("" (rewrite "integrable_integral_y_section") nil nil)) nil) ((integrable_integral_y_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)) (integral_integral_y_section 0 (integral_integral_y_section-1 nil 3473946590 ("" (skosimp) (("" (typepred "h!1") (("" (lemma "bounded_measurable_is_integrable[[T1,T2],sigma_times(S1,S2),fm_times(mu,nu)]") (("" (inst - "h!1") (("" (rewrite "finite_fubini2" 1) (("" (lemma "finite_integrable_is_integrable2" ("f" "h!1")) (("1" (lemma "integrable_integral_y_section" ("h" "h!1")) (("1" (lemma "integral_ae_eq[T2,S2,to_measure(nu)]" ("f" "LAMBDA y: integral(LAMBDA x: h!1(x, y))" "h" "integral2(h!1)")) (("1" (assert) (("1" (hide 2) (("1" (expand "ae_eq?") (("1" (expand "restrict") (("1" (expand "pointwise_ae?") (("1" (expand "ae?") (("1" (expand "fullset") (("1" (expand "ae_in?") (("1" (expand "member") (("1" (name "NI" "null_integrable2(h!1)") (("1" (inst + "NI`1") (("1" (skolem + "y!1") (("1" (flatten) (("1" (lemma "null_integral2_def" ("h2" "h!1" "N2" "NI`1" "g" "NI`2" "y" "y!1")) (("1" (expand "member") (("1" (assert) (("1" (expand "integral2") (("1" (expand "member") (("1" (replace -2) (("1" (assert) (("1" (decompose-equality) 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" (skosimp) (("3" (rewrite "integrable_y_section") nil nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((bounded_measurable nonempty-type-eq-decl nil measure_space nil) (bounded_measurable? const-decl "bool" measure_space 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) (finite_integrable_is_integrable2 formula-decl nil finite_fubini nil) (integral2 const-decl "integrable[T2, S2, nu]" product_integral_def nil) (integrable2 nonempty-type-eq-decl nil product_integral_def nil) (integrable2? const-decl "bool" product_integral_def nil) (measurable_function nonempty-type-eq-decl nil measure_space_def nil) (measurable_function? const-decl "bool" measure_space_def nil) (integral const-decl "real" integral nil) (integral_ae_eq formula-decl nil integral nil) (restrict const-decl "R" restrict nil) (measurable_fullset name-judgement "measurable_set[T, S]" finite_fubini nil) (subset_algebra_fullset name-judgement "(S)" finite_fubini nil) (ae? const-decl "bool" measure_theory nil) (ae_in? const-decl "bool" measure_theory nil) (set type-eq-decl nil sets nil) (null_set? const-decl "bool" measure_theory nil) (null_set nonempty-type-eq-decl nil measure_theory nil) (= const-decl "[T, T -> boolean]" equalities nil) (null_integrable2 const-decl "[null_set[T2, S2, nu], integrable[T2, S2, nu]]" product_integral_def nil) (null_integral2_def formula-decl nil product_integral_def nil) (TRUE const-decl "bool" booleans nil) (negligible_set? const-decl "bool" measure_theory nil) (negligible nonempty-type-eq-decl nil measure_theory nil) (member const-decl "bool" sets nil) (fullset const-decl "set" sets nil) (pointwise_ae? const-decl "bool" measure_theory nil) (ae_eq? const-decl "bool" measure_theory nil) (integrable_y_section formula-decl nil finite_fubini nil) (integrable_integral_y_section formula-decl nil finite_fubini nil) (integrable nonempty-type-eq-decl nil integral nil) (integrable? const-decl "bool" integral 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_fubini2 formula-decl nil finite_fubini nil) (bounded_measurable_is_integrable judgement-tcc nil finite_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) (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)) shostak)))
¤ 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.366Bemerkung: (Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können 2026-04-27) ¤*Eine klare Vorstellung vom Zielzustand |
|
||||||||||||||
2026-05-26