Quelle essentially_bounded.prf
Sprache: Lisp
(essentially_boundednil 3477287079"" (typepred "S" )"" (expand "sigma_algebra?" )"" (flatten)"" (expand "subset_algebra_empty?" ) (("" (assert ) nil nil ))nil ))nil ))nil ))nil )"bool" subset_algebra_def"measure_integration/" )"finite_set" finite_sets nil )"finite_set[T]" countable_props"sets_aux/" )"finite_set[T]" countable_setofsets"sets_aux/" )"bool" sets nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil essentially_bounded nil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def"measure_integration/" )nil subset_algebra_def"measure_integration/" )"sigma_algebra[T]" essentially_bounded nil ))nil ))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 )nil complex_measurable nil )nil complex_types "complex_alt/" )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[complex -> boolean]" complex_types"complex_alt/" )"[[real, real] -> (complex_?)]" "complex_alt/" )nil essentially_bounded nil )nil booleans nil )nil booleans nil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def"measure_integration/" )nil subset_algebra_def"measure_integration/" )"sigma_algebra[T]" essentially_bounded nil )nil real_types nil )"bool" reals nil )"nnreal" polar "complex_alt/" )nil complex_types "complex_alt/" )nil sq "reals/" )nil complex_types "complex_alt/" )nil sqrt "reals/" )"bool" measure_theory"measure_integration/" )"bool" measure_theory "measure_integration/" )"bool" sets nil ) (set type-eq-decl nil sets nil )nil extended_nnreal"extended_nnreal/" )"bool" generalized_measure_def"measure_integration/" )nil generalized_measure_def"measure_integration/" )"measure_type[T, S]" essentially_bounded nil )"bool" measure_theory"measure_integration/" )nil measure_theory"measure_integration/" )"set" sets nil )"finite_set" finite_sets nil )"finite_set[T]" countable_props"sets_aux/" )"finite_set[T]" countable_setofsets"sets_aux/" )"null_set[T, S, mu]" nil )"(S)" essentially_boundednil )"bool" measure_theory "measure_integration/" )"(S)" essentially_boundednil )"measurable_set[T, S]" nil )"bool" measure_theory "measure_integration/" )"nnreal" complex_types "complex_alt/" )"[T -> nonneg_real]" complex_fun_ops"complex_alt/" )"bool" complex_measure_theory nil )"bool" essentially_bounded nil ))nil ))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 )"bool" complex_measure_theory nil )"R" extend nil )"bool" sets nil )nil real_types nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )"(total_order?[real])" nil )nil complex_measurable nil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def"measure_integration/" )nil subset_algebra_def"measure_integration/" )"sigma_algebra[T]" essentially_bounded nil )"bool" sets nil )"bool" sets nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil essentially_bounded nil )nil complex_types "complex_alt/" )"bool" essentially_bounded nil )nil essentially_boundednil )"bool" bounded_reals "reals/" )"bool" bound_defs "reals/" ))nil ))nil 3477287079"" (skosimp)"" (lemma "essential_bound_TCC1" ("f" "f!1" ))"" (flatten)"" "inf[real] LAMBDA x: K)}))") "" "INF" "inf[real] 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" "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 )nil essentially_boundednil )"bool" essentially_bounded nil )nil booleans nil )nil booleans nil )nil complex_types "complex_alt/" )nil essentially_bounded nil )nil essentially_bounded nil )"[T -> nonneg_real]" complex_fun_ops"complex_alt/" )nil real_types nil )"bool" measure_theory "measure_integration/" )"measure_type[T, S]" essentially_bounded nil )nil generalized_measure_def"measure_integration/" )"bool" generalized_measure_def"measure_integration/" )nil extended_nnreal"extended_nnreal/" )"sigma_algebra[T]" essentially_bounded nil )nil subset_algebra_def"measure_integration/" )"bool" subset_algebra_def"measure_integration/" )nil sets nil )"R" extend nil )"bool" booleans nil )nil real_types nil )"bool" reals nil )"{x | greatest_lower_bound(<=)(x, Sl)}" "reals/" )nil bounded_reals "reals/" )"bool" bounded_reals "reals/" )nil defined_types nil )"bool" sets nil )set type-eq-decl nil sets nil ) (<= const-decl "bool" reals nil )"bool" bound_defs "reals/" )nil defined_types nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" reals nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"bool" bound_defs "reals/" )"[T, T -> boolean]" equalities nil ))nil ))nil 3477311458"" (skosimp)"" (expand "essential_bound" )"" (lemma "essential_bound_TCC1" ("f" "f!1" ))"" "inf(extend[real, nnreal, bool, FALSE] LAMBDA x: K)}))") "" "INF" "inf(extend[real, nnreal, bool, FALSE] 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 )"nnreal" essentially_bounded nil )"[T -> nonneg_real]" complex_fun_ops"complex_alt/" )nil real_types nil )"bool" measure_theory "measure_integration/" )"measure_type[T, S]" essentially_bounded nil )nil generalized_measure_def"measure_integration/" )"bool" generalized_measure_def"measure_integration/" )nil extended_nnreal"extended_nnreal/" )"sigma_algebra[T]" essentially_bounded nil )nil subset_algebra_def"measure_integration/" )"bool" subset_algebra_def"measure_integration/" )nil sets nil )"R" extend nil )"bool" booleans nil )nil real_types nil )"bool" reals nil )"{x | greatest_lower_bound(<=)(x, Sl)}" "reals/" )nil bounded_reals "reals/" )"bool" bounded_reals "reals/" )nil defined_types nil )"bool" sets nil )set type-eq-decl nil sets nil ) (<= const-decl "bool" reals nil )"bool" bound_defs "reals/" )nil defined_types nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" bound_defs "reals/" )"nnreal" essentially_bounded nil )"essentially_bounded" essentially_boundednil )"[T, T -> boolean]" equalities nil )nil essentially_bounded nil )nil essentially_bounded nil )nil complex_types "complex_alt/" )nil booleans nil )nil booleans nil )"bool" essentially_bounded nil )nil essentially_boundednil ))nil 3477312383"" (skosimp)"" (lemma "essential_bound_TCC1" ("f" "f!1" ))"" (expand "essential_bound" )"" "inf(extend[real, nnreal, bool, FALSE] LAMBDA x: K)}))") "1" "INF" "inf(extend[real, nnreal, bool, FALSE] LAMBDA x: K)}))") "1" (flatten)"1" "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" "1" case "convergence?(lambda (n:nat): M(n+1),INF)" )"1" expand "lower_bound" )"1" "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" "IUnion(E)" )"1" "1" expand "member" )"1" expand "abs" "1" "x!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" expand "IUnion" 1)"2" "abs(f!1(x!1))" )"2" assert )"2" "1" assert )"1" replace "1" assert )nil nil ))nil ))nil )"2" "2" case "z!1<abs(f!1(x!1))" )"1" "1" "z!1" )"1" expand "extend" "1" "1" "z!1" )"1" expand "<=" "1" "1" "EPS" "z!1-INF" )"1" case "EPS>0" )"1" "archimedean" "px" "EPS" ))"1" "1" "n!1+1" )"1" expand "X" "1" "1" case "INF < M(1 + n!1) & M(1 + n!1) < z!1" )"1" "1" "n!1" )"1" expand "E" "1" "choose_member" "a" "{N: null_set[T, S, mu] | NOT N(x)) => abs(f!1(x)) <= M(1 + n!1)}")) "1" "EE" "choose({N: null_set[T, S, mu] | NOT N(x)) => abs(f!1(x)) <= M(1 + n!1)})") "1" expand "member" )"1" "1" "x!1" )"1" assert )nil nil ))nil )"2" expand "empty?" )"2" expand "member" )"2" "2" expand "ae_le?" )"2" expand "pointwise_ae?" )"2" expand "ae?" )"2" expand "fullset" )"2" expand "ae_in?" )"2" "2" "E!1" )"2" expand "negligible_set?" )"2" "2" "X!1" )"2" "2" "x!2" )"2" expand "abs" "2" assert )"2" expand "subset?" )"2" "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" "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" "2" "E!1" )"2" expand "negligible_set?" )"2" "2" "X!1" )"2" expand "subset?" )"2" expand "member" )"2" "2" "x!2" )"2" "x!2" )"2" expand "abs" "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 "2" "2" assert )"2" "posreal_div_posreal_is_posreal" "px" "1" "py" "1+n!1" ))"2" assert )"2" replace "2" "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" "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" "2" "1+n!1" )"2" expand "X" -2)"2" "2" "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" "2" "E!1" )"2" expand "negligible_set?" )"2" "2" "X!1" )"2" "2" expand "subset?" "2" "x!1" )"2" expand "member" )"2" "x!1" )"2" expand "abs" "2" replace "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "metric_convergence_def" )"2" replace -2 1 rl)"2" "2" expand "metric_converges_to" )"2" expand "ball" )"2" expand "member" )"2" "2" "archimedean" "px" "r!1" ))"2" "2" "n!1-1" )"2" "2" rewrite "real_props.abs_mult" )"2" "posreal_div_posreal_is_posreal" "px" "1" "py" "1+i!1" ))"2" expand "abs" )"2" rewrite "neg_neg" )"2" rewrite "one_times" )"2" rewrite "div_mult_pos_lt1" "2" rewrite "div_mult_pos_lt1" "2" "both_sides_times_pos_le1" "pz" "r!1" "x" "n!1" "y" "1+i!1" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (1 -6 -3 -4))"2" "inf(X)" )"2" expand "extend" )"2" expand "greatest_lower_bound" )"2" expand "lower_bound" )"2" "2" "INF" )"2" replace 1)"2" "1" "inf(X)" )"1" "1" assert )nil nil )"2" assert )nil nil )"3" "3" "z!1" )"3" assert )"3" case "z!1<inf(X)" )"1" "1" "z!1" )"1" assert )nil nil )"2" expand "X" "2" nil nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" case "z!1<INF" )"1" "z!1" )"1" expand "X" -1)"1" "1" "1" "1" "z!1" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (1 -1 -2 -3))"2" (typepred "inf(X)" )"2" expand "greatest_lower_bound" )"2" "2" expand "lower_bound" )"2" "2" "posreal_div_posreal_is_posreal" "px" "1" "py" "n!1" ))"2" "inf(X) + 1 / n!1" )"1" assert )"1" "1" case "z!1<M(n!1)" )"1" "z!1" )"1" "1" expand "X" )"1" assert )"1" "1" assert )"1" "1" expand "ae_le?" )"1" expand "pointwise_ae?" )"1" expand "ae?" )"1" expand "fullset" )"1" expand "ae_in?" )"1" "1" "E!1" )"1" "1" expand "member" )"1" "x!1" )"1" expand "abs" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" expand "M" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (hide-all-but (-1 -5 1))"2" (expand "below_bounded" )"2" (skosimp)"2" (expand "X" )"2" (inst + "n!1" )"2" expand "extend" )"2" expand "lower_bound" )"2" "2" "z!1" )"2" (inst - "z!1" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (1 -3))"2" (expand "extend" )"2" (expand "nonempty?" )"2" (expand "empty?" )"2" (expand "member" )"2" (skosimp)"2" "x!1" )"2" assert )"2" "2" expand "X" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil )nil essentially_boundednil )"bool" essentially_bounded nil )nil booleans nil )nil booleans nil )nil complex_types "complex_alt/" )nil essentially_bounded nil )nil essentially_bounded nil )"[T -> nonneg_real]" complex_fun_ops"complex_alt/" )nil real_types nil )"bool" measure_theory "measure_integration/" )"measure_type[T, S]" essentially_bounded nil )nil generalized_measure_def"measure_integration/" )"bool" generalized_measure_def"measure_integration/" )nil extended_nnreal"extended_nnreal/" )"sigma_algebra[T]" essentially_bounded nil )nil subset_algebra_def"measure_integration/" )"bool" subset_algebra_def"measure_integration/" )nil sets nil )"R" extend nil )"bool" booleans nil )nil real_types nil )"bool" reals nil )"{x | greatest_lower_bound(<=)(x, Sl)}" "reals/" )nil bounded_reals "reals/" )"bool" bounded_reals "reals/" )nil defined_types nil )"bool" sets nil )set type-eq-decl nil sets nil ) (<= const-decl "bool" reals nil )"bool" bound_defs "reals/" )nil defined_types nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"essentially_bounded" essentially_boundednil )"{t | IF t >= 0 THEN ae_le?(abs(f!1), LAMBDA x: t) ELSE FALSE ENDIF}" nil )"{x: real | X(x)}" essentially_bounded nil )nil metric_space"metric_space/" )"set[T]" metric_space_def "metric_space/" )nil extra_tegies nil )"nnreal" nil )"posreal" nil )nil real_props nil )"posreal" nil )nil real_props nil )"posrat" nil )"{j: posint | j >= i}" nil )"{r: posrat | r >= q}" nil )nil real_props nil )"nzrat" rationalsnil )"bool" metric_space_def"metric_space/" )"bool" bound_defs "reals/" )"set[T]" essentially_bounded nil )"negligible[T, S, mu]" nil )"null_set[T, S, mu]" nil )"set[T]" indexed_sets nil )"bool" reals nil )nil real_props nil )nil real_types nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil real_props nil )nil real_types nil )"[n: nat -> NOT N(x)) => abs(f!1(x)) <= M(1 + n)})]" nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"bool" sets nil )"(partial_order?[set[T]])" nil )"set[T]" essentially_bounded nil )"bool" sets nil )"set[T]" essentially_bounded nil )nil sets_lemmas nil )"[real -> boolean]" essentially_bounded nil )"measurable_set[T, S]" nil )"(S)" essentially_boundednil )"bool" measure_theory "measure_integration/" )"bool" measure_theory "measure_integration/" )"(total_order?[real])" nil )"bool" booleans nil )"bool" sets nil )"bool" measure_theory"measure_integration/" )nil measure_theory"measure_integration/" )"set" sets nil )"bool" measure_theory"measure_integration/" )nil measure_theory"measure_integration/" )"(p)" sets nil )"nnreal" polar "complex_alt/" )"[bool, bool -> bool]" booleans nil )nil measure_theory"measure_integration/" )"bool" measure_theory "measure_integration/" )"posint" nil )"bool" topological_convergence"topology/" )"setofsets[T]" metric_space_def"metric_space/" )"[numfield, numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil sequences nil )nil naturalnumbers nil )"(hausdorff?)" "metric_space/" )"hausdorff[real]" "metric_space/" )"second_countable" real_topology "metric_space/" )"real" reals nil )"posint" nil )"posrat" nil )"[posnat -> real]" essentially_bounded nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil integers nil )"bool" reals nil )nil integers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"real" reals nil )"[T, T -> boolean]" equalities nil )"nnreal" essentially_bounded nil ))nil 3477802082"" (skosimp)"" (typepred "f!1" )"" (expand "essentially_bounded?" )"" (flatten)"" (rewrite "scal_complex_measurable" )"" (hide -1)"" (expand "ae_bounded?" )"" (skosimp)"" (inst + "abs(c!1)*K!1" )"" (expand "ae_le?" )"" (expand "pointwise_ae?" )"" (expand "ae?" )"" (expand "fullset" )"" (expand "ae_in?" )"" "" "E!1" )"" "" "x!1" )"" assert )"" "" expand "abs" -1)"" expand "abs" 1 1)"" expand "*" )"" rewrite "abs_mult" )"" "abs(c!1)" )"" expand ">=" )"" expand "<=" "" "1" "both_sides_times_pos_le1" "pz" "abs(c!1)" "x" "abs(f!1(x!1))" "y" "K!1" ))"1" assert )nil nil )"2" assert )nil nil ))nil )"2" replace "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil essentially_boundednil )"bool" essentially_bounded nil )nil complex_types "complex_alt/" )nil essentially_bounded nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" measure_theory "measure_integration/" )"measurable_set[T, S]" nil )"(S)" essentially_boundednil )"bool" measure_theory "measure_integration/" )"bool" measure_theory "measure_integration/" )nil measure_theory"measure_integration/" )"bool" measure_theory"measure_integration/" )"measure_type[T, S]" essentially_bounded nil )nil generalized_measure_def"measure_integration/" )"bool" generalized_measure_def"measure_integration/" )nil extended_nnreal"extended_nnreal/" )set type-eq-decl nil sets nil )"bool" booleans nil )nil polar "complex_alt/" )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil real_props nil )"bool" reals nil )"[T -> complex]" complex_fun_ops "complex_alt/" )"[T -> nonneg_real]" complex_fun_ops"complex_alt/" )"bool" sets nil )"(total_order?[real])" nil )"set" sets nil )"bool" measure_theory"measure_integration/" )"bool" reals nil )nil real_types nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"nnreal" polar "complex_alt/" )"nnreal" nil )"bool" complex_measure_theory nil )nil complex_fun_ops "complex_alt/" )nil complex_fun_ops "complex_alt/" )nil complex_measurablenil )"bool" complex_measurable nil )nil complex_measurable nil )"[T -> real]" complex_fun_ops "complex_alt/" )"[T -> real]" complex_fun_ops "complex_alt/" )"bool" measure_space_def"measure_integration/" )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil complex_measurable nil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def"measure_integration/" )nil subset_algebra_def"measure_integration/" )"sigma_algebra[T]" essentially_bounded nil ))nil ))nil 3477802082"" (skosimp)"" (typepred "f0!1" )"" (typepred "f1!1" )"" (expand "essentially_bounded?" )"" (flatten)"" (rewrite "sum_complex_measurable" )"" (hide -1 -3)"" (expand "ae_bounded?" )"" (skosimp*)"" (inst + "K!1+K!2" )"" (expand "ae_le?" )"" (expand "pointwise_ae?" )"" (expand "ae?" )"" (expand "fullset" )"" expand "ae_in?" )"" "" "union(E!1,E!2)" )"" "" "x!1" )"" "x!1" )"" expand "union" )"" expand "member" )"" "" assert )"" "" expand "abs" )"" expand "+" )"" "abs_triangle" "z1" "f0!1(x!1)" "z2" "f1!1(x!1)" ))"" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil essentially_boundednil )"bool" essentially_bounded nil )nil complex_types "complex_alt/" )nil essentially_bounded nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"sigma_algebra[T]" essentially_bounded nil )nil subset_algebra_def"measure_integration/" )"bool" subset_algebra_def"measure_integration/" )nil sets nil )nil defined_types nil )nil complex_measurable nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" measure_space_def"measure_integration/" )"[T -> real]" complex_fun_ops "complex_alt/" )"[T -> real]" complex_fun_ops "complex_alt/" )nil complex_measurable nil )"bool" complex_measurable nil )nil complex_measurablenil )nil complex_fun_ops "complex_alt/" )nil complex_fun_ops "complex_alt/" )"bool" complex_measure_theory nil )"nnreal" nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil real_types nil )"bool" reals nil )"bool" measure_theory"measure_integration/" )"set" sets nil )"bool" sets nil )"(total_order?[real])" nil )"[T -> nonneg_real]" complex_fun_ops"complex_alt/" )nil polar "complex_alt/" )"[T -> complex]" complex_fun_ops "complex_alt/" )"bool" booleans nil )set type-eq-decl nil sets nil )nil extended_nnreal"extended_nnreal/" )"bool" generalized_measure_def"measure_integration/" )nil generalized_measure_def"measure_integration/" )"measure_type[T, S]" essentially_bounded nil )"bool" measure_theory"measure_integration/" )nil measure_theory"measure_integration/" )"set" sets nil )"negligible[T, S, mu]" nil )"bool" measure_theory "measure_integration/" )"bool" measure_theory "measure_integration/" )"(S)" essentially_boundednil )"measurable_set[T, S]" nil )"bool" measure_theory "measure_integration/" ))nil ))nil 3477802082"" (skosimp)"" "scal_essentially_bounded" "c" "complex_(-1,0)" "f" "f!1" ))"" (case-replace "*[T](complex_(-1, 0), f!1)=-f!1" )"1" (hide-all-but 1)"1" "scal_essentially_bounded" "c" "complex_(-1,0)" "f" "f!1" ))"1" (expand "*" )"1" (expand "-" )"1" (expand "essentially_bounded?" )"1" (flatten)"1" (expand "-" )"1" (expand "Re" )"1" (expand "Im" )"1" (expand "*" )"1" (assert )"1" "1" assert )"1" expand "Re" )"1" expand "Im" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -1 2)"2" (expand "-" )"2" (expand "=" )"2" (expand "*" )"2" (expand "-" )"2" (expand "Re" )"2" (expand "Re" )"2" (expand "Im" )"2" (expand "Im" )"2" (split)"1" (apply-extensionality :hide? t)"1" (grind) nil nil )) nil )"2" (apply-extensionality :hide? t)"2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil essentially_boundednil )"bool" essentially_bounded nil )nil booleans nil )nil essentially_bounded nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"[[real, real] -> (complex_?)]" "complex_alt/" )"[complex -> boolean]" complex_types"complex_alt/" )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil complex_types "complex_alt/" )nil essentially_boundednil )"odd_int" integers nil )"[complex -> real]" complex_types"complex_alt/" )"[complex -> real]" complex_types"complex_alt/" )"real" reals nil )"real" reals nil )"complex" complex_types "complex_alt/" )"real" complex_types "complex_alt/" )nil complex_types "complex_alt/" )nil complex_types "complex_alt/" )"sigma_algebra[T]" essentially_bounded nil )nil subset_algebra_def"measure_integration/" )"bool" subset_algebra_def"measure_integration/" )nil sets nil )nil defined_types nil )nil complex_measurable nil )"[T -> real]" complex_fun_ops "complex_alt/" )"real" reals nil )"[T -> real]" complex_fun_ops "complex_alt/" )"complex" complex_types "complex_alt/" )"real" reals nil )"real" complex_types "complex_alt/" )"[T -> complex]" complex_fun_ops "complex_alt/" )"[T -> complex]" complex_fun_ops "complex_alt/" )"bool" complex_fun_ops "complex_alt/" )"essentially_bounded" essentially_bounded nil ))nil ))nil 3477802082"" (skosimp)"" (typepred "f0!1" )"" (typepred "f1!1" )"" (lemma "opp_essentially_bounded" ("f" "f1!1" ))"" "add_essentially_bounded" "f0" "f0!1" "f1" "-f1!1" ))"" (hide -2 -3 -4)"" (expand "+" )"" (expand "-" )"" (expand "essentially_bounded?" )"" (flatten)"" (expand "complex_measurable?" )"" (flatten)"" (assert )"" (expand "+ " )"" expand "-" )"" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil essentially_boundednil )"bool" essentially_bounded nil )nil complex_types "complex_alt/" )nil essentially_bounded nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil essentially_bounded nil )"[T -> complex]" complex_fun_ops "complex_alt/" )"complex" complex_types "complex_alt/" )nil complex_types "complex_alt/" )nil complex_types "complex_alt/" )"real" reals nil )"complex" complex_types "complex_alt/" )"complex" complex_types "complex_alt/" )"bool" complex_measurable nil )"[T -> complex]" complex_fun_ops "complex_alt/" )"[T -> complex]" complex_fun_ops "complex_alt/" )nil essentially_bounded nil )"essentially_bounded" essentially_bounded nil ))nil ))nil 3477802082"" (skosimp)"" (typepred "f0!1" )"" (typepred "f1!1" )"" (expand "essentially_bounded?" )"" (rewrite "prod_complex_measurable" )"1" (flatten)"1" (hide -1 -3)"1" (expand "ae_bounded?" )"1" (skosimp*)"1" (inst + "K!1*K!2" )"1" (assert )"1" (expand "ae_le?" )"1" (expand "pointwise_ae?" )"1" (expand "ae?" )"1" expand "fullset" )"1" expand "ae_in?" )"1" "1" "union(E!1,E!2)" )"1" "1" "x!1" )"1" "x!1" )"1" expand "member" )"1" expand "union" )"1" expand "member" )"1" "1" assert )"1" expand "abs" )"1" expand "*" )"1" "1" "le_times_le_pos" "nnx" "abs(f0!1(x!1))" "nnz" "abs(f1!1(x!1))" "w" "K!1" "y" "K!2" ))"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten) (("2" (assert ) nil nil )) nil )"3" (flatten) (("3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )nil essentially_boundednil )"bool" essentially_bounded nil )nil complex_types "complex_alt/" )nil essentially_bounded nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" complex_measure_theory nil )"nnreal" nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil real_types nil )"bool" reals nil )"bool" measure_theory "measure_integration/" )"measurable_set[T, S]" nil )"(S)" essentially_boundednil )"bool" measure_theory "measure_integration/" )"bool" measure_theory "measure_integration/" )"negligible[T, S, mu]" nil )"set" sets nil )nil measure_theory"measure_integration/" )"bool" measure_theory"measure_integration/" )"measure_type[T, S]" essentially_bounded nil )nil generalized_measure_def"measure_integration/" )"bool" generalized_measure_def"measure_integration/" )nil extended_nnreal"extended_nnreal/" )set type-eq-decl nil sets nil )"bool" booleans nil )"bool" sets nil )"(total_order?[real])" nil )"[T -> real]" real_fun_ops "reals/" )nil real_props nil )nil real_types nil )"nnreal" polar "complex_alt/" )"[T -> nonneg_real]" complex_fun_ops"complex_alt/" )"set" sets nil )"bool" measure_theory"measure_integration/" )nil complex_fun_ops "complex_alt/" )nil complex_fun_ops "complex_alt/" )nil complex_fun_ops "complex_alt/" )nil complex_measurablenil )"bool" complex_measurable nil )nil complex_measurable nil )"[T -> real]" complex_fun_ops "complex_alt/" )"[T -> real]" complex_fun_ops "complex_alt/" )"bool" measure_space_def"measure_integration/" )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil complex_measurable nil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def"measure_integration/" )nil subset_algebra_def"measure_integration/" )"sigma_algebra[T]" essentially_bounded nil ))nil ))nil 3477805086"" (skosimp)"" "essential_bound_def1" "f" "c!1*f!1" "K" "abs(c!1) * essential_bound(f!1)" ))"" (split -1)"1" (typepred "abs(c!1)" )"1" (expand ">=" )"1" (expand "<=" -1)"1" (split)"1" "essential_bound_def1" "f" "f!1" "K" "essential_bound(c!1*f!1)/abs(c!1)" ))"1" (split)"1" (rewrite "div_mult_pos_le2" -1)"1" (assert ) nil nil )) nil )"2" (hide -2 2)"2" "essential_bound_def2" ("f" "c!1*f!1" ))"2" (expand "ae_le?" )"2" (expand "pointwise_ae?" )"2" (expand "ae?" )"2" expand "fullset" )"2" expand "ae_in?" )"2" "2" "E!1" )"2" "2" "x!1" )"2" expand "member" )"2" assert )"2" expand "abs" -1)"2" expand "abs" 2 1)"2" "2" expand "*" -1 1)"2" rewrite "abs_mult" "2" rewrite "div_mult_pos_le2" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (rewrite "div_mult_pos_ge1" ) nil nil )) nil )"3" (assert ) nil nil ))nil )"2" (replace -1 * rl) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (lemma "essential_bound_def2" ("f" "f!1" ))"2" (expand "ae_le?" )"2" (expand "pointwise_ae?" )"2" (expand "ae?" )"2" (expand "fullset" )"2" (expand "ae_in?" )"2" (skosimp)"2" (inst + "E!1" )"2" (skosimp)"2" (inst - "x!1" )"2" expand "member" )"2" assert )"2" "2" expand "abs" -1)"2" expand "abs" 1 1)"2" expand "*" 1 1)"2" rewrite "abs_mult" )"2" "abs(c!1)" )"2" expand ">=" )"2" expand "<=" -1)"2" "1" "both_sides_times_pos_le1" "pz" "abs(c!1)" "x" "abs(f!1(x!1))" "y" "essential_bound(f!1)" ))"1" assert )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 ))nil )"[T -> complex]" complex_fun_ops "complex_alt/" )"nnreal" essentially_bounded nil )nil essentially_boundednil )"bool" essentially_bounded nil )nil essentially_bounded nil )"nnreal" polar "complex_alt/" )nil complex_types "complex_alt/" )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil essentially_bounded nil )"essentially_bounded" essentially_bounded nil )"nnreal" nil )nil real_props nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" reals nil )"real" reals nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"(total_order?[real])" nil )"bool" measure_theory "measure_integration/" )"measurable_set[T, S]" nil )"(S)" essentially_boundednil )"bool" measure_theory "measure_integration/" )"bool" measure_theory "measure_integration/" )nil measure_theory"measure_integration/" )"bool" measure_theory"measure_integration/" )"measure_type[T, S]" essentially_bounded nil )nil generalized_measure_def"measure_integration/" )"bool" generalized_measure_def"measure_integration/" )nil extended_nnreal"extended_nnreal/" )"sigma_algebra[T]" essentially_bounded nil )nil subset_algebra_def"measure_integration/" )"bool" subset_algebra_def"measure_integration/" )nil sets nil )nil defined_types nil )set type-eq-decl nil sets nil )"bool" booleans nil )nil polar "complex_alt/" )"[T -> nonneg_real]" complex_fun_ops"complex_alt/" )"bool" sets nil )"set" sets nil )"bool" measure_theory"measure_integration/" )nil essentially_bounded nil )"(strict_total_order?[real])" real_props nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil real_props nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil real_props nil ))nil 3477806906"" (skosimp)"" "essential_bound_def1" "f" "f0!1+f1!1" "K" "essential_bound(f0!1) + essential_bound(f1!1)" ))"" (assert )"" (hide 2)"" (lemma "essential_bound_def2" ("f" "f0!1" ))"" (lemma "essential_bound_def2" ("f" "f1!1" ))"" (expand "ae_le?" )"" (expand "pointwise_ae?" )"" (expand "ae?" )"" (expand "fullset" )"" (expand "ae_in?" )"" (skosimp*)"" (inst + "union(E!1,E!2)" )"" (skosimp)"" "x!1" )"" "x!1" )"" expand "union" )"" assert )"" "" assert )"" expand "abs" )"" "" expand "+" )"" "abs_triangle" "z1" "f0!1(x!1)" "z2" "f1!1(x!1)" ))"" 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 )"[T -> complex]" complex_fun_ops "complex_alt/" )"nnreal" essentially_bounded nil )nil essentially_boundednil )"bool" essentially_bounded nil )nil complex_types "complex_alt/" )nil essentially_bounded nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil essentially_bounded nil )"essentially_bounded" essentially_bounded nil )"nnreal" nil )"bool" measure_theory"measure_integration/" )"set" sets nil )"bool" sets nil )nil polar "complex_alt/" )"[T -> nonneg_real]" complex_fun_ops"complex_alt/" )"bool" booleans nil )set type-eq-decl nil sets nil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def"measure_integration/" )nil subset_algebra_def"measure_integration/" )"sigma_algebra[T]" essentially_bounded nil )nil extended_nnreal"extended_nnreal/" )"bool" generalized_measure_def"measure_integration/" )nil generalized_measure_def"measure_integration/" )"measure_type[T, S]" essentially_bounded nil )"bool" measure_theory"measure_integration/" )nil measure_theory"measure_integration/" )"set" sets nil )"negligible[T, S, mu]" nil )"bool" measure_theory "measure_integration/" )"bool" measure_theory "measure_integration/" )"(S)" essentially_boundednil )"measurable_set[T, S]" nil )"bool" measure_theory "measure_integration/" )nil essentially_bounded nil )"(total_order?[real])" nil ))nil 3477806078"" (skosimp)"" "essential_bound_scal" ("c" "complex_(-1,0)" "f" "f!1" ))"" (expand "abs" )"" (expand "sq_abs" )"" (expand "Im" )"" (expand "Re" )"" (rewrite "sq_0" )"" (rewrite "sq_neg" )"" (rewrite "sqrt_1" )"" (rewrite "one_times" )"" (expand "-" )"" (expand "*" )"" (expand "-" )"" (expand "Re" )"" expand "*" )"" expand "Re" )"" expand "Im" )"" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil essentially_boundednil )"bool" essentially_bounded nil )nil booleans nil )nil essentially_bounded nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"[[real, real] -> (complex_?)]" "complex_alt/" )"[complex -> boolean]" complex_types"complex_alt/" )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil complex_types "complex_alt/" )nil essentially_bounded nil )"odd_int" integers nil )"nnreal" complex_types "complex_alt/" )"posreal" sq "reals/" )"real" complex_types "complex_alt/" )nil sq "reals/" )nil sq "reals/" )"nnreal" essentially_bounded nil )nil real_types nil )"bool" reals nil )nil extra_tegies nil )"[T -> complex]" complex_fun_ops "complex_alt/" )"complex" complex_types "complex_alt/" )"real" reals nil )"complex" complex_types "complex_alt/" )"[T -> complex]" complex_fun_ops "complex_alt/" )nil sqrt "reals/" )"posreal" sqrt "reals/" )nil sq "reals/" )"real" complex_types "complex_alt/" )"nnreal" polar "complex_alt/" ))nil 3477806152"" (skosimp)"" (lemma "essential_bound_add" ("f0" "f0!1" "f1" "-f1!1" ))"" (rewrite "essential_bound_opp" )"" "RHS" "essential_bound(f0!1) + essential_bound(f1!1)" )"" (expand "essential_bound" )"" (expand "-" )"" (expand "+ " )"" (expand "abs" )"" (assert )"" (expand "abs" )"" (expand "sq_abs" )"" (expand "Re" )"" (expand "Im" )"" (assert )"" expand "sq" )"" expand "+ " )"" expand "-" )"" expand "Im" )"" expand "Re" )"" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"[T -> complex]" complex_fun_ops "complex_alt/" )nil essentially_boundednil )"bool" essentially_bounded nil )nil booleans nil )nil booleans nil )nil complex_types "complex_alt/" )nil essentially_bounded nil )nil essentially_bounded nil )"essentially_bounded" essentially_bounded nil )"nnreal" nil )nil numbers nil )"[T, T -> boolean]" equalities nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil real_types nil )"nnreal" essentially_bounded nil )"[T -> complex]" complex_fun_ops "complex_alt/" )"[T -> nonneg_real]" complex_fun_ops"complex_alt/" )"nnreal" polar "complex_alt/" )"real" complex_types "complex_alt/" )"real" reals nil )"complex" complex_types "complex_alt/" )"real" reals nil )"complex" complex_types "complex_alt/" )"complex" complex_types "complex_alt/" )"real" reals nil )"nonneg_real" sq "reals/" )"real" reals nil )"real" complex_types "complex_alt/" )"nnreal" complex_types "complex_alt/" )"(total_order?[real])" nil )"[T -> complex]" complex_fun_ops "complex_alt/" )nil essentially_bounded nil ))nil 3477806280"" (skosimp)"" (typepred "f!1" )"" (expand "essentially_bounded?" )"" (flatten)"" (expand "cal_N?" )"" (replace -1)"" (split)"1" (flatten)"1" (lemma "essential_bound_def2" ("f" "f!1" ))"1" (replace -2)"1" (hide-all-but (-1 1))"1" (expand "ae_le?" )"1" (expand "ae_0?" )"1" (expand "pointwise_ae?" )"1" expand "ae?" )"1" expand "fullset" )"1" expand "ae_in?" )"1" "1" "E!1" )"1" "1" "x!1" )"1" expand "member" )"1" replace 1)"1" expand "abs" -1)"1" expand "<=" -1)"1" "1" assert )nil nil )"2" rewrite "abs_is_0" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" "essential_bound_def1" ("f" "f!1" "K" "0" ))"2" (split)"1" (assert ) nil nil )"2" (hide-all-but (-1 1))"2" (expand "ae_0?" )"2" (expand "ae_le?" )"2" (expand "pointwise_ae?" )"2" expand "ae?" )"2" expand "fullset" )"2" expand "ae_in?" )"2" "2" "E!1" )"2" "2" "x!1" )"2" expand "member" )"2" replace 1)"2" expand "abs" )"2" expand "<=" )"2" "2" rewrite "abs_is_0" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil essentially_boundednil )"bool" essentially_bounded nil )nil complex_types "complex_alt/" )nil essentially_bounded nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"(total_order?[real])" nil )nil essentially_bounded nil )"bool" measure_theory "measure_integration/" )"bool" complex_measure_theory nil )"bool" measure_theory"measure_integration/" )"set" sets nil )"bool" sets nil )"[T -> nonneg_real]" complex_fun_ops"complex_alt/" )"(strict_total_order?[real])" real_props nil )nil complex_types "complex_alt/" )nil complex_types "complex_alt/" )nil complex_types "complex_alt/" )nil complex_types "complex_alt/" )nil polar "complex_alt/" )"bool" reals nil )"bool" booleans nil )nil measure_theory"measure_integration/" )"bool" measure_theory"measure_integration/" )"measure_type[T, S]" essentially_bounded nil )nil generalized_measure_def"measure_integration/" )"bool" generalized_measure_def"measure_integration/" )nil extended_nnreal"extended_nnreal/" )nil real_types nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )"sigma_algebra[T]" essentially_bounded nil )nil subset_algebra_def"measure_integration/" )"bool" subset_algebra_def"measure_integration/" )nil sets nil )nil defined_types nil )set type-eq-decl nil sets nil )"bool" measure_theory "measure_integration/" )"bool" measure_theory "measure_integration/" )"(S)" essentially_boundednil )"measurable_set[T, S]" nil )"bool" complex_measure_theory nil )nil essentially_bounded nil )"bool" complex_measure_theory nil ))nil 3477806660"" (skosimp)"" "essential_bound_def1" "f" "f0!1*f1!1" "K" "essential_bound(f0!1) * essential_bound(f1!1)" ))"" (split -1)"1" (propax) nil nil )"2" (hide 2)"2" (lemma "essential_bound_def2" ("f" "f0!1" ))"2" (lemma "essential_bound_def2" ("f" "f1!1" ))"2" (expand "ae_le?" )"2" (expand "pointwise_ae?" )"2" (expand "ae?" )"2" (expand "fullset" )"2" (expand "ae_in?" )"2" (skosimp*)"2" (inst + "union(E!1,E!2)" )"2" (skosimp)"2" "x!1" )"2" "x!1" )"2" expand "union" )"2" expand "member" )"2" "2" assert )"2" expand "abs" )"2" expand "*" )"2" rewrite "abs_mult" )"2" "le_times_le_pos" "nnx" "abs(f0!1(x!1))" "y" "essential_bound(f0!1)" "nnz" "abs(f1!1(x!1))" "w" "essential_bound(f1!1)" ))"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 )"[T -> complex]" complex_fun_ops "complex_alt/" )"nnreal" essentially_bounded nil )nil essentially_boundednil )"bool" essentially_bounded nil )nil complex_types "complex_alt/" )nil essentially_bounded nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil essentially_bounded nil )"essentially_bounded" essentially_bounded nil )"nnreal" nil )"bool" measure_theory"measure_integration/" )"set" sets nil )"bool" sets nil )"(total_order?[real])" nil )nil complex_fun_ops "complex_alt/" )"[T -> real]" real_fun_ops "reals/" )"nnreal" polar "complex_alt/" )nil real_types nil )nil real_props nil )"[T -> nonneg_real]" complex_fun_ops"complex_alt/" )"bool" booleans nil )set type-eq-decl nil sets nil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def"measure_integration/" )nil subset_algebra_def"measure_integration/" )"sigma_algebra[T]" essentially_bounded nil )nil extended_nnreal"extended_nnreal/" )"bool" generalized_measure_def"measure_integration/" )nil generalized_measure_def"measure_integration/" )"measure_type[T, S]" essentially_bounded nil )"bool" measure_theory"measure_integration/" )nil measure_theory"measure_integration/" )"set" sets nil )"negligible[T, S, mu]" nil )"bool" measure_theory "measure_integration/" )"bool" measure_theory "measure_integration/" )"(S)" essentially_boundednil )"measurable_set[T, S]" nil )"bool" measure_theory "measure_integration/" )nil essentially_bounded nil ))nil 3477802082"" (skosimp)"" (typepred "f!1" )"" (typepred "g!1" )"" (expand "p_integrable?" )"" (expand "essentially_bounded?" )"" (flatten)"" "prod_complex_measurable" "g1" "f!1" "g2" "g!1" ))"1" (replace -1)"1" "abs_complex_measurable" ("g" "f!1*g!1" ))"1" (case "forall h: abs(h)^1 = abs(h)" )"1" (inst-cp - "f!1*g!1" )"1" (inst - "g!1" )"1" (replace -1)"1" (replace -2)"1" "1" "abs_complex_measurable" "g" "f!1" ))"1" expand "ae_bounded?" )"1" "1" "integral_prod" "h" "abs(f!1)" "nnc" "K!1" "f" "abs(g!1)" ))"1" "(abs(g!1) * abs(f!1))=abs(f!1 * g!1)" )"1" "1" (flatten) nil nil )"2" "2" "abs(abs(f!1))=abs(f!1)" )"2" "2" "2" expand "abs" )"2" "abs(f!1(x!1))" )"2" expand "abs" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "*" 1)"2" expand "abs" 1)"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil )"3" (propax) nil nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (skosimp)"2" (apply-extensionality :hide? t)"2" (expand "^" )"2" expand "abs" )"2" rewrite "real_expt_x1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (assert ) nil nil ) ("3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil essentially_boundednil )"bool" essentially_bounded nil )nil complex_types "complex_alt/" )nil essentially_bounded nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"[T, T -> boolean]" equalities nil )nil real_types nil )"bool" reals nil )nil real_types nil )"[T -> nnreal]" real_fun_power "power/" )"[T -> nonneg_real]" complex_fun_ops"complex_alt/" )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"nnreal" polar "complex_alt/" )"[T -> nonneg_real]" real_fun_ops "reals/" )"nnreal" nil )nil complex_fun_ops "complex_alt/" )nil complex_fun_ops "complex_alt/" )nil complex_measurable nil )nil complex_fun_ops "complex_alt/" )nil measure_space_def"measure_integration/" )nil integral"measure_integration/" )"bool" integral "measure_integration/" )nil integral "measure_integration/" )"bool" complex_measure_theory nil )nil real_expt "power/" )"[T -> real]" real_fun_ops "reals/" )"[T -> real]" real_fun_ops "reals/" )"[T -> real]" real_fun_ops "reals/" )nil complex_measurable nil )"[T -> complex]" complex_fun_ops "complex_alt/" )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" measure_space_def"measure_integration/" )"[T -> real]" complex_fun_ops "complex_alt/" )"[T -> real]" complex_fun_ops "complex_alt/" )nil complex_measurable nil )"bool" complex_measurable nil )nil complex_measurablenil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def"measure_integration/" )nil subset_algebra_def"measure_integration/" )"sigma_algebra[T]" essentially_bounded nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil real_types nil )nil extended_nnreal"extended_nnreal/" )"bool" generalized_measure_def"measure_integration/" )nil generalized_measure_def"measure_integration/" )"measure_type[T, S]" essentially_bounded nil )"bool" p_integrable_def nil )nil p_integrable_def nil ))nil ))nil 3477802082"" (skosimp)"" (lemma "holder_judge_infty_1" ("f" "f!1" "g" "g!1" ))"" (case-replace "(*[T](f!1, g!1))=(*[T](g!1, f!1))" )"1" (expand "*" )"1" (assert )"1" (hide-all-but 1)"1" (typepred "f!1" )"1" (typepred "g!1" )"1" (expand "p_integrable?" )"1" (expand "essentially_bounded?" )"1" (flatten)"1" (split)"1" "prod_complex_measurable" "g1" "g!1" "g2" "f!1" ))"1" (assert )"1" "1" assert )"1" expand "Re" )"1" expand "*" )"1" expand "-" )"1" expand "Re" )"1" expand "Im" )"1" expand "Im" )"1" assert )"1" expand "+ ") "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "complex_measurable?" )"2" (propax) nil nil )) nil )"3" (expand "complex_measurable?" )"3" (propax) nil nil )) nil ))nil )"2" case "forall (f:[T->nnreal]): f^1 = f" )"1" (inst-cp - "abs(g!1)" )"1" replace -2)"1" "abs(g!1*f!1)" )"1" expand "*" -1 1)"1" replace -1)"1" "1" "integral_prod" "h" "abs(f!1)" "f" "abs(g!1)" ))"1" expand "ae_bounded?" )"1" "1" "K!1" )"1" "1" "1" assert )nil nil ))nil )"2" "2" expand "ae_le?" )"2" expand "pointwise_ae?" )"2" expand "ae?" )"2" expand "fullset" )"2" expand "ae_in?" )"2" "2" "E!1" )"2" "2" "x!1" )"2" expand "member" )"2" assert )"2" expand "abs" )"2" rewrite "abs_abs" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "abs_complex_measurable" "g" "f!1" ))"1" (propax) nil nil )"2" (assert ) nil nil ))nil ))nil )"3" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" "2" "2" expand "^" )"2" rewrite "real_expt_x1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (expand "*" )"2" (assert )"2" (split)"1" (apply-extensionality :hide? t) nil nil )"2" (apply-extensionality :hide? t) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil p_integrable_def nil )"bool" p_integrable_def nil )"measure_type[T, S]" essentially_bounded nil )nil generalized_measure_def"measure_integration/" )"bool" generalized_measure_def"measure_integration/" )nil extended_nnreal"extended_nnreal/" )nil real_types nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )"sigma_algebra[T]" essentially_bounded nil )nil subset_algebra_def"measure_integration/" )"bool" subset_algebra_def"measure_integration/" )nil sets nil )nil defined_types nil )nil essentially_boundednil )"bool" essentially_bounded nil )nil booleans nil )nil booleans nil )nil complex_types "complex_alt/" )nil essentially_bounded nil )nil essentially_bounded nil )"real" reals nil )nil complex_fun_ops "complex_alt/" )nil complex_types "complex_alt/" )nil complex_fun_ops "complex_alt/" )nil complex_types "complex_alt/" )nil complex_fun_ops "complex_alt/" )nil complex_fun_ops "complex_alt/" )nil complex_measurable nil )"real" reals nil )"complex" complex_types "complex_alt/" )"[T -> real]" real_fun_ops "reals/" )"real" complex_types "complex_alt/" )"[T -> real]" real_fun_ops "reals/" )"real" complex_types "complex_alt/" )"real" reals nil )"[T -> real]" real_fun_ops "reals/" )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" measure_space_def"measure_integration/" )"[T -> real]" complex_fun_ops "complex_alt/" )"[T -> real]" complex_fun_ops "complex_alt/" )nil complex_measurablenil )"bool" complex_measurable nil )nil complex_measurable nil )nil real_expt "power/" )"[T -> nonneg_real]" complex_fun_ops"complex_alt/" )nil integral "measure_integration/" )"bool" integral "measure_integration/" )nil integral"measure_integration/" )nil measure_space_def"measure_integration/" )nil complex_fun_ops "complex_alt/" )"(total_order?[real])" nil )"bool" measure_theory "measure_integration/" )"measurable_set[T, S]" nil )"(S)" essentially_boundednil )"bool" measure_theory "measure_integration/" )"bool" measure_theory "measure_integration/" )nil measure_theory"measure_integration/" )"bool" measure_theory"measure_integration/" )set type-eq-decl nil sets nil )"bool" booleans nil )nil polar "complex_alt/" )"[T -> nonneg_real]" real_fun_ops "reals/" )"bool" sets nil )"set" sets nil )"bool" measure_theory"measure_integration/" )"bool" complex_measure_theory nil )nil complex_measurable nil )"[T -> nnreal]" real_fun_power "power/" )nil real_types nil )"bool" reals nil )nil real_types nil )"[T, T -> boolean]" equalities nil )NOT const-decl "[bool -> bool]" booleans nil )nil complex_fun_ops "complex_alt/" )"[T -> complex]" complex_fun_ops "complex_alt/" )"bool" complex_fun_ops "complex_alt/" )"p_integrable" nil ))nil ))nil 3477804007"" (skosimp)"" (lemma "holder_judge_infty_1" ("f" "f!1" "g" "g!1" ))"" (typepred "f!1" )"" (typepred "g!1" )"" (expand "norm" )"" case "forall h: abs(h)^1 = abs(h) & forall x: abs(h)(x)>=0" )"1" (inst-cp - "f!1*g!1" )"1" (inst - "g!1" )"1" (flatten)"1" (expand "essentially_bounded?" )"1" (expand "p_integrable?" )"1" (flatten)"1" (replace -1)"1" (replace -3)"1" "1" "integral_nonneg" "f" "abs(g!1)" ))"1" "integral_nonneg" "f" "abs(f!1*g!1)" ))"1" replace -3)"1" replace -4)"1" "1" rewrite "real_expt_x1" 1)"1" rewrite "real_expt_x1" "1" "abs_complex_measurable" "g" "f!1" ))"1" "integral_prod" "h" "abs(f!1)" "nnc" "essential_bound(f!1)" "f" "abs(g!1)" ))"1" case "forall h: abs(abs(h)) = abs(h)" )"1" "f!1" )"1" "g!1" )"1" replace -2)"1" replace "1" rewrite "essential_bound_def2" )"1" "1" "abs(g!1) * abs(f!1)=abs(f!1*g!1)" )"1" "f!1*g!1" )"1" assert )nil nil ))nil )"2" "2" "2" expand "*" )"2" expand "abs" )"2" rewrite "abs_mult" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" expand "abs" )"2" "abs(h!1(x!1))" )"2" expand "abs" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (skosimp)"2" (split)"1" (apply-extensionality :hide? t)"1" (expand "^" )"1" (expand "abs" )"1" (rewrite "real_expt_x1" ) nil nil ))nil ))nil ))nil )"2" (skosimp)"2" (expand "abs" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil p_integrable_def nil )"bool" p_integrable_def nil )"measure_type[T, S]" essentially_bounded nil )nil generalized_measure_def"measure_integration/" )"bool" generalized_measure_def"measure_integration/" )nil extended_nnreal"extended_nnreal/" )nil real_types nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )"sigma_algebra[T]" essentially_bounded nil )nil subset_algebra_def"measure_integration/" )"bool" subset_algebra_def"measure_integration/" )nil sets nil )nil defined_types nil )nil essentially_boundednil )"bool" essentially_bounded nil )nil booleans nil )nil booleans nil )nil complex_types "complex_alt/" )nil essentially_bounded nil )nil essentially_bounded nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )nil real_types nil )"bool" reals nil )nil real_types nil )"[T -> nnreal]" real_fun_power "power/" )"[T -> nonneg_real]" complex_fun_ops"complex_alt/" )nil integral "measure_integration/" )"bool" integral "measure_integration/" )nil integral"measure_integration/" )nil integral "measure_integration/" )nil measure_space_def"measure_integration/" )"nnreal" essentially_bounded nil )"nnreal" polar "complex_alt/" )"(strict_total_order?[real])" real_props nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )nil essentially_bounded nil )nil complex_measurable nil )nil complex_fun_ops "complex_alt/" )nil complex_fun_ops "complex_alt/" )"real" reals nil )"(total_order?[real])" nil )"nnreal" nil )"[T -> nonneg_real]" real_fun_ops "reals/" )"bool" measure_space_def"measure_integration/" )"[T -> real]" complex_fun_ops "complex_alt/" )"[T -> real]" complex_fun_ops "complex_alt/" )nil complex_measurablenil )"bool" complex_measurable nil )nil complex_measurable nil )nil real_expt "power/" )"real" integral "measure_integration/" )"(total_order?[real])" nil )"[T -> real]" real_fun_ops "reals/" )nil complex_fun_ops "complex_alt/" )"p_integrable" nil )"[T -> complex]" complex_fun_ops "complex_alt/" )"nnreal" p_integrable_def nil )NOT const-decl "[bool -> bool]" booleans nil ))nil 3477803870"" (skosimp)"" (lemma "holder_infty_1" ("f" "f!1" "g" "g!1" ))"" (case-replace "norm(g!1 * f!1)=norm(f!1 * g!1)" )"1" (assert ) nil nil )"2" (hide-all-but 1)"2" (expand "norm" )"2" (assert )"2" "abs(g!1) * abs(f!1)=abs(f!1) * abs(g!1)" )"1" (expand "abs" )"1" (expand "*" ) (("1" (assert ) nil nil )) nil ))nil )"2" (hide 2)"2" (assert )"2" (expand "*" )"2" (apply-extensionality :hide? t) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil p_integrable_def nil )"bool" p_integrable_def nil )"measure_type[T, S]" essentially_bounded nil )nil generalized_measure_def"measure_integration/" )"bool" generalized_measure_def"measure_integration/" )nil extended_nnreal"extended_nnreal/" )nil real_types nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )"sigma_algebra[T]" essentially_bounded nil )nil subset_algebra_def"measure_integration/" )"bool" subset_algebra_def"measure_integration/" )nil sets nil )nil defined_types nil )nil essentially_boundednil )"bool" essentially_bounded nil )nil booleans nil )nil booleans nil )nil complex_types "complex_alt/" )nil essentially_bounded nil )nil essentially_bounded nil )nil complex_fun_ops "complex_alt/" )"[T -> real]" real_fun_ops "reals/" )nil real_types nil )"[T -> nonneg_real]" complex_fun_ops"complex_alt/" )"nnreal" nil )"(total_order?[real])" nil )"[T -> complex]" complex_fun_ops "complex_alt/" )"nnreal" p_integrable_def nil )"[T, T -> boolean]" equalities nil )"p_integrable" nil )"p_integrable" nil ))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Dauer der Verarbeitung: 0.203 Sekunden
(vorverarbeitet am 2026-05-03)
¤ *© Formatika GbR, Deutschland
2026-05-26
