|
(complex_measurable
(complex_measurable_TCC1 0
(complex_measurable_TCC1-1 nil 3477203515
("" (expand "complex_measurable?")
(("" (expand "Re")
(("" (expand "Im")
(("" (assert)
(("" (lemma "const_measurable" ("c" "0"))
(("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
((Re const-decl "[T -> real]" complex_fun_ops "complex_alt/")
(Re_rew formula-decl nil complex_types "complex_alt/")
(Im_rew formula-decl nil complex_types "complex_alt/")
(const_measurable formula-decl nil measure_space
"measure_integration/")
(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)
(T formal-type-decl nil complex_measurable 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]" complex_measurable nil)
(Im const-decl "[T -> real]" complex_fun_ops "complex_alt/")
(complex_measurable? const-decl "bool" complex_measurable nil))
nil))
(complex_measurable_def 0
(complex_measurable_def-1 nil 3477203878
("" (skosimp)
(("" (expand "complex_measurable?") (("" (propax) nil nil)) nil))
nil)
((complex_measurable? const-decl "bool" complex_measurable nil))
shostak))
(constant_is_complex_measurable 0
(constant_is_complex_measurable-1 nil 3477203515
("" (skolem + "f!1")
(("" (typepred "f!1")
(("" (expand "constant?")
(("" (skosimp)
(("" (replace -1)
(("" (hide -1)
(("" (assert)
(("" (expand "const_fun")
(("" (expand "Re")
(("" (expand "Im")
(("" (lemma "const_measurable" ("c" "Re(a!1)"))
(("" (lemma "const_measurable" ("c" "Im(a!1)"))
(("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((constant? const-decl "bool" const_fun_def "structures/")
(complex type-decl nil complex_types "complex_alt/")
(T formal-type-decl nil complex_measurable nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(const_fun const-decl "[S -> T]" const_fun_def "structures/")
(Im const-decl "[T -> real]" complex_fun_ops "complex_alt/")
(Im const-decl "real" complex_types "complex_alt/")
(const_measurable formula-decl nil measure_space
"measure_integration/")
(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)
(Re const-decl "real" complex_types "complex_alt/")
(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]" complex_measurable nil)
(Re const-decl "[T -> real]" complex_fun_ops "complex_alt/")
(complex_measurable_def formula-decl nil complex_measurable nil))
nil))
(scal_complex_measurable 0
(scal_complex_measurable-1 nil 3477203515
("" (skosimp)
(("" (assert)
(("" (typepred "g!1")
(("" (assert)
(("" (flatten)
((""
(lemma "scal_measurable" ("c" "Re(c!1)" "g" "Re(g!1)"))
(("1"
(lemma "scal_measurable" ("c" "Im(c!1)" "g" "Re(g!1)"))
(("1"
(lemma "scal_measurable"
("c" "Re(c!1)" "g" "Im(g!1)"))
(("1"
(lemma "scal_measurable"
("c" "Im(c!1)" "g" "Im(g!1)"))
(("1" (rewrite "sum_measurable")
(("1" (rewrite "diff_measurable") nil nil)) nil))
nil)
("2" (propax) nil nil))
nil))
nil)
("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((complex_measurable_def formula-decl nil complex_measurable nil)
(Im_fun_mul2 formula-decl nil complex_fun_ops "complex_alt/")
(Re_fun_mul2 formula-decl nil complex_fun_ops "complex_alt/")
(T formal-type-decl nil complex_measurable nil)
(S formal-const-decl "sigma_algebra[T]" complex_measurable 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)
(setof type-eq-decl nil defined_types nil)
(Re const-decl "[T -> real]" complex_fun_ops "complex_alt/")
(measurable_function nonempty-type-eq-decl nil measure_space_def
"measure_integration/")
(measurable_function? const-decl "bool" measure_space_def
"measure_integration/")
(Re const-decl "real" complex_types "complex_alt/")
(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)
(scal_measurable judgement-tcc nil measure_space_def
"measure_integration/")
(Im const-decl "[T -> real]" complex_fun_ops "complex_alt/")
(* const-decl "[T -> real]" real_fun_ops "reals/")
(sum_measurable judgement-tcc nil measure_space_def
"measure_integration/")
(diff_measurable judgement-tcc nil measure_space_def
"measure_integration/")
(Im const-decl "real" complex_types "complex_alt/")
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(complex type-decl nil complex_types "complex_alt/")
(complex_measurable? const-decl "bool" complex_measurable nil)
(complex_measurable nonempty-type-eq-decl nil complex_measurable
nil))
nil))
(sum_complex_measurable 0
(sum_complex_measurable-1 nil 3477203515
("" (skosimp)
(("" (typepred "g1!1")
(("" (typepred "g2!1")
(("" (assert)
(("" (flatten)
(("" (rewrite "sum_measurable")
(("" (rewrite "sum_measurable") nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((complex_measurable nonempty-type-eq-decl nil complex_measurable
nil)
(complex_measurable? const-decl "bool" complex_measurable nil)
(complex type-decl nil complex_types "complex_alt/")
(T formal-type-decl nil complex_measurable nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(complex_measurable_def formula-decl nil complex_measurable nil)
(Re_fun_add1 formula-decl nil complex_fun_ops "complex_alt/")
(Im_fun_add1 formula-decl nil complex_fun_ops "complex_alt/")
(sum_measurable judgement-tcc nil measure_space_def
"measure_integration/")
(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)
(measurable_function? const-decl "bool" measure_space_def
"measure_integration/")
(measurable_function nonempty-type-eq-decl nil measure_space_def
"measure_integration/")
(Re const-decl "[T -> real]" complex_fun_ops "complex_alt/")
(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]" complex_measurable nil)
(Im const-decl "[T -> real]" complex_fun_ops "complex_alt/"))
nil))
(opp_complex_measurable 0
(opp_complex_measurable-1 nil 3477203515
("" (skosimp)
(("" (typepred "g!1")
(("" (assert)
(("" (flatten)
(("" (rewrite "opp_measurable")
(("" (rewrite "opp_measurable") nil nil)) nil))
nil))
nil))
nil))
nil)
((complex_measurable nonempty-type-eq-decl nil complex_measurable
nil)
(complex_measurable? const-decl "bool" complex_measurable nil)
(complex type-decl nil complex_types "complex_alt/")
(T formal-type-decl nil complex_measurable nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(Im const-decl "[T -> real]" complex_fun_ops "complex_alt/")
(S formal-const-decl "sigma_algebra[T]" complex_measurable 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)
(setof type-eq-decl nil defined_types nil)
(Re const-decl "[T -> real]" complex_fun_ops "complex_alt/")
(measurable_function nonempty-type-eq-decl nil measure_space_def
"measure_integration/")
(measurable_function? const-decl "bool" measure_space_def
"measure_integration/")
(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)
(opp_measurable judgement-tcc nil measure_space_def
"measure_integration/")
(Im_fun_neg1 formula-decl nil complex_fun_ops "complex_alt/")
(Re_fun_neg1 formula-decl nil complex_fun_ops "complex_alt/")
(complex_measurable_def formula-decl nil complex_measurable nil))
nil))
(diff_complex_measurable 0
(diff_complex_measurable-1 nil 3477203515
("" (skosimp)
(("" (typepred "g1!1")
(("" (typepred "g2!1")
(("" (assert)
(("" (flatten)
(("" (rewrite "diff_measurable")
(("" (rewrite "diff_measurable") nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((complex_measurable nonempty-type-eq-decl nil complex_measurable
nil)
(complex_measurable? const-decl "bool" complex_measurable nil)
(complex type-decl nil complex_types "complex_alt/")
(T formal-type-decl nil complex_measurable nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(complex_measurable_def formula-decl nil complex_measurable nil)
(Re_fun_sub1 formula-decl nil complex_fun_ops "complex_alt/")
(Im_fun_sub1 formula-decl nil complex_fun_ops "complex_alt/")
(diff_measurable judgement-tcc nil measure_space_def
"measure_integration/")
(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)
(measurable_function? const-decl "bool" measure_space_def
"measure_integration/")
(measurable_function nonempty-type-eq-decl nil measure_space_def
"measure_integration/")
(Re const-decl "[T -> real]" complex_fun_ops "complex_alt/")
(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]" complex_measurable nil)
(Im const-decl "[T -> real]" complex_fun_ops "complex_alt/"))
nil))
(const_measurable 0
(const_measurable-1 nil 3477204885
("" (skosimp)
(("" (assert)
(("" (expand "Re")
(("" (expand "Im")
(("" (rewrite "const_measurable")
(("" (rewrite "const_measurable") nil nil)) nil))
nil))
nil))
nil))
nil)
((complex_measurable_def formula-decl nil complex_measurable nil)
(Im const-decl "[T -> real]" complex_fun_ops "complex_alt/")
(Im const-decl "real" complex_types "complex_alt/")
(S formal-const-decl "sigma_algebra[T]" complex_measurable 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)
(setof type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-type-decl nil complex_measurable nil)
(Re const-decl "real" complex_types "complex_alt/")
(complex type-decl nil complex_types "complex_alt/")
(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)
(const_measurable formula-decl nil measure_space
"measure_integration/")
(Re const-decl "[T -> real]" complex_fun_ops "complex_alt/"))
shostak))
(abs_complex_measurable 0
(abs_complex_measurable-1 nil 3477204847
("" (skosimp)
(("" (typepred "g!1")
(("" (assert)
(("" (flatten)
(("" (expand "abs")
(("" (expand "abs")
(("" (expand "sq_abs")
(("" (lemma "sq_measurable" ("g" "Re(g!1)"))
(("1" (lemma "sq_measurable" ("g" "Im(g!1)"))
(("1"
(lemma "sum_measurable"
("g1" "sq[T](Im(g!1))" "g2" "sq[T](Re(g!1))"))
(("1"
(lemma "expt_measurable"
("g" "(+[T])(sq[T](Im(g!1)), sq[T](Re(g!1)))"
"a" "1/2"))
(("1" (hide-all-but (-1 1))
(("1" (expand "^" -1)
(("1" (expand "+" -1)
(("1"
(expand "sq" -1)
(("1"
(expand "Im" -1)
(("1"
(expand "Re" -1)
(("1"
(case-replace
"(LAMBDA (x: T): (sq(Im(g!1(x))) + sq(Re(g!1(x)))) ^ (1 / 2))=(LAMBDA (x: T): sqrt(sq(Im(g!1(x))) + sq(Re(g!1(x)))))")
(("1"
(hide -1 2)
(("1"
(apply-extensionality
:hide?
t)
(("1"
(name-replace
"DRL"
"sq(Im(g!1(x!1))) + sq(Re(g!1(x!1)))")
(("1"
(lemma
"sq_eq"
("nna"
"DRL ^ (1 / 2)"
"nnb"
"sqrt(DRL)"))
(("1"
(replace -1 1 rl)
(("1"
(hide -1)
(("1"
(rewrite "sq_sqrt")
(("1"
(lemma
"real_expt_times"
("x"
"DRL"
"a"
"1/2"
"b"
"2"))
(("1"
(rewrite
"real_expt_x1")
(("1"
(name-replace
"DRL2"
"DRL ^ (1 / 2)")
(("1"
(rewrite
"real_expt_int_rew")
(("1"
(expand
"^")
(("1"
(expand
"sq")
(("1"
(expand
"expt")
(("1"
(expand
"expt")
(("1"
(expand
"expt")
(("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)
("2" (expand "nn_measurable?")
(("2" (assert)
(("2" (skosimp)
(("2"
(hide-all-but 1)
(("2"
(expand "+")
(("2"
(expand "sq")
(("2"
(expand "Im")
(("2"
(expand "Re")
(("2"
(lemma
"sq_pos"
("a" "Im(g!1(x!1))"))
(("2"
(lemma
"sq_pos"
("a" "Re(g!1(x!1))"))
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
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)
((complex_measurable nonempty-type-eq-decl nil complex_measurable
nil)
(complex_measurable? const-decl "bool" complex_measurable nil)
(complex type-decl nil complex_types "complex_alt/")
(T formal-type-decl nil complex_measurable nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(abs const-decl "nnreal" polar "complex_alt/")
(S formal-const-decl "sigma_algebra[T]" complex_measurable 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)
(setof type-eq-decl nil defined_types nil)
(Re const-decl "[T -> real]" complex_fun_ops "complex_alt/")
(measurable_function nonempty-type-eq-decl nil measure_space_def
"measure_integration/")
(measurable_function? const-decl "bool" measure_space_def
"measure_integration/")
(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)
(sq_measurable judgement-tcc nil measure_space
"measure_integration/")
(sum_measurable judgement-tcc nil measure_space_def
"measure_integration/")
(>= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types nil)
(sq const-decl "[T -> nnreal]" real_fun_ops_aux "reals/")
(sq_pos formula-decl nil sq "reals/")
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/")
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(Re const-decl "real" complex_types "complex_alt/")
(Im const-decl "real" complex_types "complex_alt/")
(sq const-decl "nonneg_real" sq "reals/")
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(^ const-decl "nnreal" real_expt "power/")
(OR const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(sq_eq formula-decl nil sq "reals/")
(real_expt_times formula-decl nil real_expt "power/")
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(^ const-decl "real" exponentiation nil)
(expt def-decl "real" exponentiation nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(nnreal_exp application-judgement "nnreal" exponentiation nil)
(real_expt_int_rew formula-decl nil real_expt "power/")
(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)
(real_expt_x1 formula-decl nil real_expt "power/")
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sq_sqrt formula-decl nil sqrt "reals/")
(^ const-decl "[T -> nnreal]" real_fun_power "power/")
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(expt_measurable judgement-tcc nil measure_space
"measure_integration/")
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nn_measurable? const-decl "bool" measure_space
"measure_integration/")
(nn_measurable nonempty-type-eq-decl nil measure_space
"measure_integration/")
(+ const-decl "[T -> real]" real_fun_ops "reals/")
(Im const-decl "[T -> real]" complex_fun_ops "complex_alt/")
(sq_abs const-decl "nnreal" complex_types "complex_alt/")
(abs const-decl "[T -> nonneg_real]" complex_fun_ops
"complex_alt/")
(complex_measurable_def formula-decl nil complex_measurable nil))
nil))
(sq_complex_measurable 0
(sq_complex_measurable-1 nil 3477204847
("" (skosimp)
(("" (typepred "g!1")
(("" (assert)
(("" (flatten)
(("" (lemma "sq_measurable" ("g" "Re(g!1)"))
(("1" (lemma "sq_measurable" ("g" "Im(g!1)"))
(("1"
(lemma "prod_measurable"
("g1" "Re(g!1)" "g2" "Im(g!1)"))
(("1"
(lemma "scal_measurable"
("c" "2" "g" "Re(g!1) * Im(g!1)"))
(("1" (assert)
(("1" (expand "*")
(("1" (expand "Im")
(("1" (expand "Re")
(("1" (assert)
(("1" (expand "sq")
(("1"
(assert)
(("1"
(expand "sq")
(("1"
(assert)
(("1"
(lemma "diff_measurable")
(("1"
(inst
-
"(LAMBDA (x_1: T): Re(g!1(x_1)) * Re(g!1(x_1)))"
"(LAMBDA (x_1: T): Im(g!1(x_1)) * Im(g!1(x_1)))")
(("1"
(expand "-")
(("1" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (propax) nil nil))
nil))
nil)
("2" (propax) nil nil))
nil)
("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil)
((complex_measurable nonempty-type-eq-decl nil complex_measurable
nil)
(complex_measurable? const-decl "bool" complex_measurable nil)
(complex type-decl nil complex_types "complex_alt/")
(T formal-type-decl nil complex_measurable nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(Im const-decl "[T -> real]" complex_fun_ops "complex_alt/")
(scal_measurable judgement-tcc nil measure_space_def
"measure_integration/")
(* const-decl "[T -> real]" real_fun_ops "reals/")
(* const-decl "[T -> real]" real_fun_ops "reals/")
(sq const-decl "[T -> complex]" complex_fun_ops "complex_alt/")
(sq const-decl "[T -> nnreal]" real_fun_ops_aux "reals/")
(sq const-decl "nonneg_real" sq "reals/")
(diff_measurable judgement-tcc nil measure_space_def
"measure_integration/")
(- const-decl "[T -> real]" real_fun_ops "reals/")
(numfield nonempty-type-eq-decl nil number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(Re const-decl "real" complex_types "complex_alt/")
(Im const-decl "real" complex_types "complex_alt/")
(Im_mul1 formula-decl nil complex_types "complex_alt/")
(Re_mul1 formula-decl nil complex_types "complex_alt/")
(complex_sq_def formula-decl nil complex_types "complex_alt/")
(real_times_real_is_real application-judgement "real" reals nil)
(prod_measurable judgement-tcc nil measure_space
"measure_integration/")
(sq_measurable judgement-tcc nil measure_space
"measure_integration/")
(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)
(measurable_function? const-decl "bool" measure_space_def
"measure_integration/")
(measurable_function nonempty-type-eq-decl nil measure_space_def
"measure_integration/")
(Re const-decl "[T -> real]" complex_fun_ops "complex_alt/")
(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]" complex_measurable nil)
(complex_measurable_def formula-decl nil complex_measurable nil))
nil))
(prod_complex_measurable 0
(prod_complex_measurable-1 nil 3477204847
("" (skosimp)
(("" (lemma "sum_complex_measurable" ("g1" "g1!1" "g2" "g2!1"))
(("" (lemma "diff_complex_measurable" ("g1" "g1!1" "g2" "g2!1"))
(("" (lemma "sq_complex_measurable" ("g" "(+[T])(g1!1, g2!1)"))
((""
(lemma "sq_complex_measurable" ("g" "(-[T])(g1!1, g2!1)"))
((""
(lemma "diff_complex_measurable"
("g1" "sq[T]((+[T])(g1!1, g2!1))" "g2"
"sq[T]((-[T])(g1!1, g2!1))"))
(("" (rewrite "prod_def" 1)
((""
(lemma "scal_complex_measurable"
("c" "complex_(1/4,0)" "g" "(-[T])
(sq[T]((+[T])(g1!1, g2!1)),
sq[T]((-[T])(g1!1, g2!1)))"))
((""
(name-replace "FG"
"sq(g1!1 + g2!1) - sq(g1!1 - g2!1)")
(("" (hide-all-but (-1 1))
(("" (assert)
(("" (flatten)
(("" (expand "Re" 1)
(("" (expand "Im" 1)
((""
(expand "*" 1)
((""
(case-replace
"(LAMBDA (x: T): Re((1 / 4) * FG(x)))=1 / 4 * Re(FG) - 0 * Im(FG)")
(("1"
(case-replace
"(LAMBDA (x: T): Im((1 / 4) * FG(x)))=0 * Re(FG) + 1 / 4 * Im(FG)")
(("1" (assert) nil nil)
("2"
(apply-extensionality :hide? t)
(("2"
(hide-all-but 1)
(("2"
(expand "Im" 1 2)
(("2"
(expand "*")
(("2"
(expand "+")
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but 1)
(("2"
(apply-extensionality :hide? t)
(("2"
(expand "-")
(("2"
(expand "Re" 1 2)
(("2"
(expand "*")
(("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)
((complex_measurable nonempty-type-eq-decl nil complex_measurable
nil)
(complex_measurable? const-decl "bool" complex_measurable 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 complex_measurable nil)
(sum_complex_measurable judgement-tcc nil complex_measurable nil)
(sum_complex_measurable application-judgement "complex_measurable"
complex_measurable nil)
(sq_complex_measurable judgement-tcc nil complex_measurable nil)
(+ const-decl "[T -> complex]" complex_fun_ops "complex_alt/")
(sq_complex_measurable application-judgement "complex_measurable"
complex_measurable nil)
(sq const-decl "[T -> complex]" complex_fun_ops "complex_alt/")
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(complex_ adt-constructor-decl "[[real, real] -> (complex_?)]"
complex_types "complex_alt/")
(complex_? adt-recognizer-decl "[complex -> boolean]" complex_types
"complex_alt/")
(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)
(scal_complex_measurable judgement-tcc nil complex_measurable nil)
(Im const-decl "[T -> real]" complex_fun_ops "complex_alt/")
(* const-decl "[T -> real]" real_fun_ops "reals/")
(- const-decl "[T -> real]" real_fun_ops "reals/")
(* const-decl "complex" complex_types "complex_alt/")
(Re const-decl "real" complex_types "complex_alt/")
(real_times_real_is_real application-judgement "real" reals nil)
(Im_mul2 formula-decl nil complex_types "complex_alt/")
(Re_mul2 formula-decl nil complex_types "complex_alt/")
(Im const-decl "real" complex_types "complex_alt/")
(+ const-decl "[T -> real]" real_fun_ops "reals/")
(* const-decl "[T -> complex]" complex_fun_ops "complex_alt/")
(Re const-decl "[T -> real]" complex_fun_ops "complex_alt/")
(complex_measurable_def formula-decl nil complex_measurable nil)
(Im_fun_mul2 formula-decl nil complex_fun_ops "complex_alt/")
(Re_fun_mul2 formula-decl nil complex_fun_ops "complex_alt/")
(Im_rew formula-decl nil complex_types "complex_alt/")
(Re_rew formula-decl nil complex_types "complex_alt/")
(scal_complex_measurable application-judgement "complex_measurable"
complex_measurable nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(prod_def formula-decl nil complex_fun_ops "complex_alt/")
(- const-decl "[T -> complex]" complex_fun_ops "complex_alt/")
(diff_complex_measurable application-judgement "complex_measurable"
complex_measurable nil)
(diff_complex_measurable judgement-tcc nil complex_measurable nil))
nil))
(abs_expt_measurable 0
(abs_expt_measurable-1 nil 3477205857
("" (skosimp)
(("" (lemma "abs_complex_measurable" ("g" "g!1"))
(("" (lemma "expt_measurable" ("a" "a!1" "g" "abs[T](g!1)"))
(("1" (propax) nil nil)
("2" (expand "nn_measurable?")
(("2" (hide-all-but 1)
(("2" (skosimp)
(("2" (expand "abs") (("2" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil)
((complex_measurable nonempty-type-eq-decl nil complex_measurable
nil)
(complex_measurable? const-decl "bool" complex_measurable 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 complex_measurable nil)
(abs_complex_measurable judgement-tcc nil complex_measurable nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(abs_complex_measurable application-judgement "measurable_function"
complex_measurable nil)
(expt_measurable judgement-tcc nil measure_space
"measure_integration/")
(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)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(nn_measurable? const-decl "bool" measure_space
"measure_integration/")
(nn_measurable nonempty-type-eq-decl nil measure_space
"measure_integration/")
(abs const-decl "[T -> nonneg_real]" complex_fun_ops
"complex_alt/")
(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]" complex_measurable nil))
shostak))
(pointwise_complex_measurable 0
(pointwise_complex_measurable-1 nil 3509601271
("" (skosimp)
((""
(lemma "pointwise_measurable"
("u" "lambda n: Re(u!1(n))" "f" "Re(f!1)"))
(("1"
(lemma "pointwise_measurable"
("u" "lambda n: Im(u!1(n))" "f" "Im(f!1)"))
(("1" (assert)
(("1" (split)
(("1" (split)
(("1" (assert) nil nil)
("2" (hide -1 2)
(("2" (expand "pointwise_convergence?")
(("2" (skosimp)
(("2" (inst - "x!1")
(("2" (rewrite "metric_convergence_def")
(("2" (rewrite "metric_convergence_def")
(("2" (expand "metric_converges_to")
(("2" (skosimp)
(("2"
(inst - "r!1")
(("2"
(skosimp)
(("2"
(inst + "n!1")
(("2"
(skosimp)
(("2"
(inst - "i!1")
(("2"
(assert)
(("2"
(hide -1)
(("2"
(expand "ball")
(("2"
(expand "abs" -1)
(("2"
(rewrite
"sq_lt"
-1
:dir
rl)
(("2"
(rewrite
"sq_lt"
1
:dir
rl)
(("2"
(rewrite
"sq_sqrt")
(("2"
(expand
"sq_abs")
(("2"
(typepred
"sq(Im(f!1(x!1) - u!1(i!1)(x!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 (-2 1))
(("2" (expand "pointwise_convergence?")
(("2" (skosimp)
(("2" (inst - "x!1")
(("2" (rewrite "metric_convergence_def")
(("2" (rewrite "metric_convergence_def")
(("2" (expand "metric_converges_to")
(("2" (skosimp)
(("2" (expand "ball")
(("2"
(expand "member")
(("2"
(inst - "r!1")
(("2"
(skosimp)
(("2"
(inst + "n!1")
(("2"
(skosimp)
(("2"
(inst - "i!1")
(("2"
(assert)
(("2"
(hide -1)
(("2"
(expand "abs" -1)
(("2"
(rewrite
"sq_lt"
-1
:dir
rl)
(("2"
(rewrite "sq_sqrt")
(("2"
(expand "sq_abs")
(("2"
(rewrite
"sq_lt"
1
:dir
rl)
(("2"
(assert)
(("2"
(typepred
"sq(Re(f!1(x!1)) - Re(u!1(i!1)(x!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))
nil))
nil)
("2" (skosimp)
(("2" (typepred "u!1(n!1)")
(("2" (assert) (("2" (flatten) nil nil)) nil)) nil))
nil))
nil)
("2" (skosimp)
(("2" (typepred "u!1(n!1)")
(("2" (assert) (("2" (flatten) nil nil)) nil)) nil))
nil))
nil))
nil)
((S formal-const-decl "sigma_algebra[T]" complex_measurable 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)
(setof type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-type-decl nil complex_measurable nil)
(complex_measurable nonempty-type-eq-decl nil complex_measurable
nil)
(complex_measurable? const-decl "bool" complex_measurable nil)
(sequence type-eq-decl nil sequences nil)
(measurable_function nonempty-type-eq-decl nil measure_space_def
"measure_integration/")
(measurable_function? const-decl "bool" measure_space_def
"measure_integration/")
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals 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)
(Re const-decl "[T -> real]" complex_fun_ops "complex_alt/")
(complex type-decl nil complex_types "complex_alt/")
(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)
(pointwise_measurable formula-decl nil measure_space
"measure_integration/")
(complex_measurable_def formula-decl nil complex_measurable nil)
(Im_fun_rew formula-decl nil complex_fun_ops "complex_alt/")
(pointwise_convergence? const-decl "bool" complex_measurable nil)
(pointwise_convergence? const-decl "bool" pointwise_convergence
"measure_integration/")
(- const-decl "complex" complex_types "complex_alt/")
(abs const-decl "nnreal" polar "complex_alt/")
(nnreal type-eq-decl nil real_types nil)
(ball_is_metric_open application-judgement
"metric_open[real, (LAMBDA (x, y: real): abs(x - y))]"
convergence_aux "metric_space/")
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(member const-decl "bool" sets nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(ball const-decl "set[T]" metric_space_def "metric_space/")
(sq_abs const-decl "nnreal" complex_types "complex_alt/")
(sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/")
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(sq_lt formula-decl nil sq "reals/")
(sq_nz_pos application-judgement "posreal" sq "reals/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(sq_sqrt formula-decl nil sqrt "reals/")
(NOT const-decl "[bool -> bool]" booleans nil)
(sq const-decl "nonneg_real" sq "reals/")
(Im const-decl "real" complex_types "complex_alt/")
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(Re_sub1 formula-decl nil complex_types "complex_alt/")
(Im_sub1 formula-decl nil complex_types "complex_alt/")
(sq_abs formula-decl nil sq "reals/")
(Re const-decl "real" complex_types "complex_alt/")
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(metric_converges_to const-decl "bool" metric_space_def
"metric_space/")
(Re_fun_rew formula-decl nil complex_fun_ops "complex_alt/")
(metric_convergence_def formula-decl nil metric_space
"metric_space/")
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(Im const-decl "[T -> real]" complex_fun_ops "complex_alt/"))
shostak)))
¤ Dauer der Verarbeitung: 0.59 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.
|
