(essentially_bounded
(mu_TCC1 0
(mu_TCC1-1 nil 3477287079
("" (typepred "S")
(("" (expand "sigma_algebra?")
(("" (flatten)
(("" (expand "subset_algebra_empty?") (("" (assert) nil nil))
nil))
nil))
nil))
nil)
((subset_algebra_empty? const-decl "bool" subset_algebra_def
"measure_integration/")
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(finite_emptyset name-judgement "finite_set[T]" countable_props
"sets_aux/")
(finite_emptyset name-judgement "finite_set[T]" countable_setofsets
"sets_aux/")
(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)
(T formal-type-decl nil essentially_bounded nil)
(setof type-eq-decl nil defined_types nil)
(setofsets type-eq-decl nil sets nil)
(sigma_algebra? const-decl "bool" subset_algebra_def
"measure_integration/")
(sigma_algebra nonempty-type-eq-decl nil subset_algebra_def
"measure_integration/")
(S formal-const-decl "sigma_algebra[T]" essentially_bounded nil))
nil))
(essentially_bounded_TCC1 0
(essentially_bounded_TCC1-1 nil 3477287079
("" (expand "essentially_bounded?")
(("" (rewrite "const_measurable")
(("" (expand "ae_bounded?")
(("" (inst + "0")
(("" (expand "abs")
(("" (expand "abs")
(("" (expand "sq_abs")
(("" (assert)
(("" (expand "ae_le?")
(("" (expand "pointwise_ae?")
(("" (expand "ae?")
(("" (expand "ae_in?")
(("" (inst + "emptyset[T]")
(("" (skosimp) (("" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((const_measurable formula-decl nil complex_measurable nil)
(complex type-decl nil complex_types "complex_alt/")
(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)
(complex_? adt-recognizer-decl "[complex -> boolean]" complex_types
"complex_alt/")
(complex_ adt-constructor-decl "[[real, real] -> (complex_?)]"
complex_types "complex_alt/")
(T formal-type-decl nil essentially_bounded 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
"measure_integration/")
(sigma_algebra nonempty-type-eq-decl nil subset_algebra_def
"measure_integration/")
(S formal-const-decl "sigma_algebra[T]" essentially_bounded nil)
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(abs const-decl "nnreal" polar "complex_alt/")
(Im_rew formula-decl nil complex_types "complex_alt/")
(sq_0 formula-decl nil sq "reals/")
(Re_rew formula-decl nil complex_types "complex_alt/")
(sqrt_0 formula-decl nil sqrt "reals/")
(pointwise_ae? const-decl "bool" measure_theory
"measure_integration/")
(ae_in? const-decl "bool" measure_theory "measure_integration/")
(member const-decl "bool" sets nil) (set type-eq-decl nil sets nil)
(extended_nnreal nonempty-type-eq-decl nil extended_nnreal
"extended_nnreal/")
(measure? const-decl "bool" generalized_measure_def
"measure_integration/")
(measure_type nonempty-type-eq-decl nil generalized_measure_def
"measure_integration/")
(mu formal-const-decl "measure_type[T, S]" essentially_bounded nil)
(negligible_set? const-decl "bool" measure_theory
"measure_integration/")
(negligible nonempty-type-eq-decl nil measure_theory
"measure_integration/")
(emptyset const-decl "set" sets nil)
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(finite_emptyset name-judgement "finite_set[T]" countable_props
"sets_aux/")
(finite_emptyset name-judgement "finite_set[T]" countable_setofsets
"sets_aux/")
(null_emptyset name-judgement "null_set[T, S, mu]"
essentially_bounded nil)
(subset_algebra_emptyset name-judgement "(S)" essentially_bounded
nil)
(ae? const-decl "bool" measure_theory "measure_integration/")
(subset_algebra_fullset name-judgement "(S)" essentially_bounded
nil)
(measurable_fullset name-judgement "measurable_set[T, S]"
essentially_bounded nil)
(ae_le? const-decl "bool" measure_theory "measure_integration/")
(sq_abs const-decl "nnreal" complex_types "complex_alt/")
(abs const-decl "[T -> nonneg_real]" complex_fun_ops
"complex_alt/")
(ae_bounded? const-decl "bool" complex_measure_theory nil)
(essentially_bounded? const-decl "bool" essentially_bounded nil))
nil))
(essential_bound_TCC1 0
(essential_bound_TCC1-1 nil 3477287079
("" (skosimp)
(("" (split)
(("1" (typepred "f!1")
(("1" (expand "essentially_bounded?")
(("1" (flatten)
(("1" (expand "ae_bounded?")
(("1" (skosimp)
(("1" (expand "extend")
(("1" (expand "nonempty?")
(("1" (expand "empty?")
(("1" (expand "member")
(("1" (inst - "K!1") (("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "extend")
(("2" (expand "below_bounded")
(("2" (inst + "0")
(("2" (expand "lower_bound") (("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((ae_bounded? const-decl "bool" complex_measure_theory nil)
(extend const-decl "R" extend nil)
(empty? const-decl "bool" sets nil)
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals 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)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(complex_measurable_def formula-decl nil complex_measurable nil)
(setof type-eq-decl nil defined_types nil)
(setofsets type-eq-decl nil sets nil)
(sigma_algebra? const-decl "bool" subset_algebra_def
"measure_integration/")
(sigma_algebra nonempty-type-eq-decl nil subset_algebra_def
"measure_integration/")
(S formal-const-decl "sigma_algebra[T]" essentially_bounded nil)
(member const-decl "bool" sets nil)
(nonempty? 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)
(T formal-type-decl nil essentially_bounded nil)
(complex type-decl nil complex_types "complex_alt/")
(essentially_bounded? const-decl "bool" essentially_bounded nil)
(essentially_bounded nonempty-type-eq-decl nil essentially_bounded
nil)
(below_bounded const-decl "bool" bounded_reals "reals/")
(lower_bound const-decl "bool" bound_defs "reals/"))
nil))
(essential_bound_TCC2 0
(essential_bound_TCC2-1 nil 3477287079
("" (skosimp)
(("" (lemma "essential_bound_TCC1" ("f" "f!1"))
(("" (flatten)
((""
(typepred "inf[real]
(extend[real, nnreal, bool, FALSE]
({K | ae_le?[T, S, mu](abs[T](f!1), LAMBDA x: K)}))")
((""
(name-replace "INF" "inf[real]
(extend[real, nnreal, bool, FALSE]
({K | ae_le?[T, S, mu](abs[T](f!1), LAMBDA x: K)}))")
(("" (hide -2 -3)
(("" (expand "greatest_lower_bound")
(("" (flatten)
(("" (expand "lower_bound")
(("" (inst -2 "0")
(("" (split -2)
(("1" (assert) nil nil) ("2" (assert) nil nil)
("3" (skosimp)
(("3" (typepred "z!1")
(("3" (case "z!1<0")
(("1"
(hide 1)
(("1"
(expand "extend")
(("1" (assert) nil nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((essentially_bounded nonempty-type-eq-decl nil essentially_bounded
nil)
(essentially_bounded? const-decl "bool" essentially_bounded nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(complex type-decl nil complex_types "complex_alt/")
(T formal-type-decl nil essentially_bounded nil)
(essential_bound_TCC1 subtype-tcc nil essentially_bounded nil)
(abs const-decl "[T -> nonneg_real]" complex_fun_ops
"complex_alt/")
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(ae_le? const-decl "bool" measure_theory "measure_integration/")
(mu formal-const-decl "measure_type[T, S]" essentially_bounded nil)
(measure_type nonempty-type-eq-decl nil generalized_measure_def
"measure_integration/")
(measure? const-decl "bool" generalized_measure_def
"measure_integration/")
(extended_nnreal nonempty-type-eq-decl nil extended_nnreal
"extended_nnreal/")
(S formal-const-decl "sigma_algebra[T]" essentially_bounded nil)
(sigma_algebra nonempty-type-eq-decl nil subset_algebra_def
"measure_integration/")
(sigma_algebra? const-decl "bool" subset_algebra_def
"measure_integration/")
(setofsets type-eq-decl nil sets nil)
(extend const-decl "R" extend nil)
(FALSE const-decl "bool" booleans nil)
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(inf const-decl "{x | greatest_lower_bound(<=)(x, Sl)}"
bounded_reals "reals/")
(inf_set type-eq-decl nil bounded_reals "reals/")
(below_bounded const-decl "bool" bounded_reals "reals/")
(setof type-eq-decl nil defined_types nil)
(nonempty? const-decl "bool" sets nil)
(set type-eq-decl nil sets nil) (<= const-decl "bool" reals nil)
(greatest_lower_bound const-decl "bool" bound_defs "reals/")
(pred 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)
(NOT const-decl "[bool -> bool]" booleans nil)
(< const-decl "bool" reals nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props 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)
(lower_bound const-decl "bool" bound_defs "reals/")
(= const-decl "[T, T -> boolean]" equalities nil))
nil))
(essential_bound_def1 0
(essential_bound_def1-1 nil 3477311458
("" (skosimp)
(("" (expand "essential_bound")
(("" (lemma "essential_bound_TCC1" ("f" "f!1"))
((""
(typepred "inf(extend[real, nnreal, bool, FALSE]
({K | ae_le?(abs(f!1), LAMBDA x: K)}))")
((""
(name-replace "INF" "inf(extend[real, nnreal, bool, FALSE]
({K | ae_le?(abs(f!1), LAMBDA x: K)}))")
(("" (expand "greatest_lower_bound")
(("" (flatten)
(("" (expand "lower_bound")
(("" (inst - "K!1")
(("" (hide -1 -2 -3 2)
(("" (expand "extend") (("" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((essential_bound const-decl "nnreal" essentially_bounded nil)
(abs const-decl "[T -> nonneg_real]" complex_fun_ops
"complex_alt/")
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(ae_le? const-decl "bool" measure_theory "measure_integration/")
(mu formal-const-decl "measure_type[T, S]" essentially_bounded nil)
(measure_type nonempty-type-eq-decl nil generalized_measure_def
"measure_integration/")
(measure? const-decl "bool" generalized_measure_def
"measure_integration/")
(extended_nnreal nonempty-type-eq-decl nil extended_nnreal
"extended_nnreal/")
(S formal-const-decl "sigma_algebra[T]" essentially_bounded nil)
(sigma_algebra nonempty-type-eq-decl nil subset_algebra_def
"measure_integration/")
(sigma_algebra? const-decl "bool" subset_algebra_def
"measure_integration/")
(setofsets type-eq-decl nil sets nil)
(extend const-decl "R" extend nil)
(FALSE const-decl "bool" booleans nil)
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(inf const-decl "{x | greatest_lower_bound(<=)(x, Sl)}"
bounded_reals "reals/")
(inf_set type-eq-decl nil bounded_reals "reals/")
(below_bounded const-decl "bool" bounded_reals "reals/")
(setof type-eq-decl nil defined_types nil)
(nonempty? const-decl "bool" sets nil)
(set type-eq-decl nil sets nil) (<= const-decl "bool" reals nil)
(greatest_lower_bound const-decl "bool" bound_defs "reals/")
(pred 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)
(NOT const-decl "[bool -> bool]" booleans nil)
(lower_bound const-decl "bool" bound_defs "reals/")
(K!1 skolem-const-decl "nnreal" essentially_bounded nil)
(f!1 skolem-const-decl "essentially_bounded" essentially_bounded
nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(essential_bound_TCC1 subtype-tcc nil essentially_bounded nil)
(T formal-type-decl nil essentially_bounded nil)
(complex type-decl nil complex_types "complex_alt/")
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(essentially_bounded? const-decl "bool" essentially_bounded nil)
(essentially_bounded nonempty-type-eq-decl nil essentially_bounded
nil))
shostak))
(essential_bound_def2 0
(essential_bound_def2-1 nil 3477312383
("" (skosimp)
(("" (lemma "essential_bound_TCC1" ("f" "f!1"))
(("" (expand "essential_bound")
((""
(typepred "inf(extend[real, nnreal, bool, FALSE]
({K | ae_le?(abs(f!1), LAMBDA x: K)}))")
(("1"
(name-replace "INF" "inf(extend[real, nnreal, bool, FALSE]
({K | ae_le?(abs(f!1), LAMBDA x: K)}))")
(("1" (flatten)
(("1"
(name "X"
"{a:real | a >= 0 & ae_le?(abs(f!1), LAMBDA x: a)}")
(("1" (case "nonempty?[real](X)")
(("1" (case "below_bounded[real](X)")
(("1" (hide -5 -6)
(("1" (name "M" "lambda (n:posnat): inf(X)+1/n")
(("1" (case "forall (n:posnat): X(M(n))")
(("1" (case-replace "inf(X)=INF")
(("1" (hide -1)
(("1"
(expand "greatest_lower_bound")
(("1"
(flatten)
(("1"
(case
"convergence?(lambda (n:nat): M(n+1),INF)")
(("1"
(expand "lower_bound")
(("1"
(name
"E"
"lambda (n:nat): choose({N:null_set[T,S,mu] | FORALL x: (not N(x)) => abs(f!1(x)) <= M(1+n)})")
(("1"
(case "null_set?(IUnion(E))")
(("1"
(case
"forall x: (not IUnion(E)(x)) => abs(f!1(x)) <= INF")
(("1"
(expand "ae_le?")
(("1"
(expand
"pointwise_ae?")
(("1"
(expand "ae?")
(("1"
(expand "fullset")
(("1"
(expand "ae_in?")
(("1"
(inst
+
"IUnion(E)")
(("1"
(skosimp)
(("1"
(expand
"member")
(("1"
(expand
"abs"
2)
(("1"
(inst
-
"x!1")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(skosimp)
(("2"
(hide -1)
(("2"
(expand "IUnion" 1)
(("2"
(inst
-9
"abs(f!1(x!1))")
(("2"
(assert)
(("2"
(split -9)
(("1"
(assert)
(("1"
(replace
-1
2
rl)
(("1"
(assert)
nil
nil))
nil))
nil)
("2"
(skosimp)
(("2"
(case
"z!1)
(("1"
(hide
1)
(("1"
(typepred
"z!1")
(("1"
(expand
"extend"
-1)
(("1"
(prop)
(("1"
(inst
-11
"z!1")
(("1"
(expand
"<="
-11)
(("1"
(split
-11)
(("1"
(name
"EPS"
"z!1-INF")
(("1"
(case
"EPS>0")
(("1"
(lemma
"archimedean"
("px"
"EPS"))
(("1"
(skosimp)
(("1"
(inst
-10
"n!1+1")
(("1"
(expand
"X"
-10)
(("1"
(flatten)
(("1"
(case
"INF < M(1 + n!1) & M(1 + n!1) < z!1")
(("1"
(flatten)
(("1"
(inst
+
"n!1")
(("1"
(expand
"E"
1)
(("1"
(lemma
"choose_member"
("a"
"{N: null_set[T, S, mu] |
FORALL x: (NOT N(x)) => abs(f!1(x)) <= M(1 + n!1)}"))
(("1"
(name-replace
"EE"
"choose({N: null_set[T, S, mu] |
FORALL x: (NOT N(x)) => abs(f!1(x)) <= M(1 + n!1)})")
(("1"
(expand
"member")
(("1"
(split
-1)
(("1"
(inst
-
"x!1")
(("1"
(assert)
nil
nil))
nil)
("2"
(expand
"empty?")
(("2"
(expand
"member")
(("2"
(hide-all-but
(-1
-14))
(("2"
(expand
"ae_le?")
(("2"
(expand
"pointwise_ae?")
(("2"
(expand
"ae?")
(("2"
(expand
"fullset")
(("2"
(expand
"ae_in?")
(("2"
(skosimp)
(("2"
(typepred
"E!1")
(("2"
(expand
"negligible_set?")
(("2"
(skosimp)
(("2"
(inst
-
"X!1")
(("2"
(skosimp)
(("2"
(inst
-
"x!2")
(("2"
(expand
"abs"
-3)
(("2"
(assert)
(("2"
(expand
"subset?")
(("2"
(inst
-
"x!2")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but
(1
-14))
(("2"
(expand
"nonempty?")
(("2"
(expand
"ae_le?")
(("2"
(expand
"empty?")
(("2"
(expand
"pointwise_ae?")
(("2"
(expand
"ae?")
(("2"
(expand
"fullset")
(("2"
(expand
"ae_in?")
(("2"
(skosimp)
(("2"
(typepred
"E!1")
(("2"
(expand
"negligible_set?")
(("2"
(skosimp)
(("2"
(inst
-3
"X!1")
(("2"
(expand
"subset?")
(("2"
(expand
"member")
(("2"
(skosimp)
(("2"
(inst
-
"x!2")
(("2"
(inst
-
"x!2")
(("2"
(expand
"abs"
-3)
(("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"
(replace
-12
*
rl)
(("2"
(hide-all-but
(-1
-2
-3
-4
-5
1))
(("2"
(assert)
(("2"
(lemma
"posreal_div_posreal_is_posreal"
("px"
"1"
"py"
"1+n!1"))
(("2"
(assert)
(("2"
(replace
-4
-2
rl)
(("2"
(lemma
"both_sides_div_pos_lt2"
("pz"
"1"
"py"
"n!1"
"px"
"1+n!1"))
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
nil
nil))
nil)
("2"
(assert)
nil
nil))
nil))
nil)
("2"
(reveal
2)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(rewrite "null_IUnion")
nil
nil))
nil)
("2"
(skosimp)
(("2"
(inst -2 "1+n!1")
(("2"
(expand "X" -2)
(("2"
(flatten)
(("2"
(hide-all-but
(-2 -3 1))
(("2"
(expand
"nonempty?")
(("2"
(expand "empty?")
(("2"
(expand
"ae_le?")
(("2"
(expand
"pointwise_ae?")
(("2"
(expand
"ae?")
(("2"
(expand
"fullset")
(("2"
(expand
"ae_in?")
(("2"
(expand
"member")
(("2"
(skosimp)
(("2"
(typepred
"E!1")
(("2"
(expand
"negligible_set?")
(("2"
(skosimp)
(("2"
(inst
-3
"X!1")
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.110 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
