| products/Sources/formale Sprachen/PVS/complex_integration/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: complex_integral.pvs Sprache: VDMOriginal von: PVS© |
|
||||||
|
(complex_integral
(mu_TCC1 0 (mu_TCC1-1 nil 3476682253 ("" (typepred "S") (("" (expand "sigma_algebra?") (("" (flatten) (("" (expand "subset_algebra_empty?") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((subset_algebra_empty? const-decl "bool" subset_algebra_def "measure_integration/") (finite_emptyset name-judgement "finite_set" finite_sets nil) (finite_emptyset name-judgement "finite_set[T]" countable_props "sets_aux/") (finite_emptyset name-judgement "finite_set[T]" countable_setofsets "sets_aux/") (member const-decl "bool" sets nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (T formal-type-decl nil complex_integral 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_integral nil)) nil)) (integrable_TCC1 0 (integrable_TCC1-1 nil 3476682253 ("" (expand "integrable?") (("" (expand "Re") (("" (expand "Im") (("" (assert) (("" (rewrite "integrable_zero") 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/") (mu formal-const-decl "measure_type[T, S]" complex_integral nil) (measure_type nonempty-type-eq-decl nil generalized_measure_def "measure_integration/") (measure? const-decl "bool" generalized_measure_def "measure_integration/") (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (S formal-const-decl "sigma_algebra[T]" complex_integral 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_integral nil) (integrable_zero formula-decl nil integral "measure_integration/") (Im const-decl "[T -> real]" complex_fun_ops "complex_alt/") (integrable? const-decl "bool" complex_integral nil)) nil)) (integral_TCC1 0 (integral_TCC1-1 nil 3476767415 ("" (skosimp) (("" (typepred "f!1") (("" (expand "integrable?" -) (("" (flatten) nil nil)) nil)) nil)) nil) ((integrable nonempty-type-eq-decl nil complex_integral nil) (integrable? const-decl "bool" complex_integral nil) (complex type-decl nil complex_types "complex_alt/") (T formal-type-decl nil complex_integral nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil)) (integral_TCC2 0 (integral_TCC2-1 nil 3476767415 ("" (skosimp) (("" (typepred "f!1") (("" (expand "integrable?" -) (("" (flatten) nil nil)) nil)) nil)) nil) ((integrable nonempty-type-eq-decl nil complex_integral nil) (integrable? const-decl "bool" complex_integral nil) (complex type-decl nil complex_types "complex_alt/") (T formal-type-decl nil complex_integral nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil)) (integrable_def 0 (integrable_def-1 nil 3477202127 ("" (skosimp) (("" (expand "integrable?" 1 1) (("" (propax) nil nil)) nil)) nil) ((integrable? const-decl "bool" complex_integral nil)) shostak)) (Re_integral 0 (Re_integral-1 nil 3477202145 ("" (skosimp) (("" (assert) (("" (expand "integral" 1 1) (("" (assert) nil nil)) nil)) nil)) nil) ((Re_rew formula-decl nil complex_types "complex_alt/") (integral const-decl "complex" complex_integral nil)) shostak)) (Im_integral 0 (Im_integral-1 nil 3477202176 ("" (skosimp) (("" (expand "integral" 1 1) (("" (assert) nil nil)) nil)) nil) ((integral const-decl "complex" complex_integral nil) (Im_rew formula-decl nil complex_types "complex_alt/")) shostak)) (integrable_is_measurable 0 (integrable_is_measurable-1 nil 3477465321 ("" (skolem + "f!1") (("" (typepred "f!1") (("" (assert) (("" (flatten) (("" (lemma "integrable_is_measurable") (("" (inst-cp - "Re(f!1)") (("" (inst - "Im(f!1)") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((integrable nonempty-type-eq-decl nil complex_integral nil) (integrable? const-decl "bool" complex_integral nil) (complex type-decl nil complex_types "complex_alt/") (T formal-type-decl nil complex_integral nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (integrable? const-decl "bool" integral "measure_integration/") (Re const-decl "[T -> real]" complex_fun_ops "complex_alt/") (f!1 skolem-const-decl "integrable" complex_integral nil) (integrable nonempty-type-eq-decl nil integral "measure_integration/") (Im const-decl "[T -> real]" complex_fun_ops "complex_alt/") (integrable_is_measurable judgement-tcc nil integral "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) (nnreal type-eq-decl nil real_types nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (measure? const-decl "bool" generalized_measure_def "measure_integration/") (measure_type nonempty-type-eq-decl nil generalized_measure_def "measure_integration/") (mu formal-const-decl "measure_type[T, S]" complex_integral nil) (integrable_def formula-decl nil complex_integral nil) (S formal-const-decl "sigma_algebra[T]" complex_integral 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) (complex_measurable_def formula-decl nil complex_measurable nil)) nil)) (cal_N_is_measurable 0 (cal_N_is_measurable-1 nil 3477465321 ("" (skolem + "f!1") (("" (typepred "f!1") (("" (rewrite "cal_N_def") (("" (flatten) (("" (assert) (("" (split) (("1" (lemma "measurable_ae_0" ("h" "Re(f!1)")) (("1" (assert) nil nil)) nil) ("2" (lemma "measurable_ae_0" ("h" "Im(f!1)")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((cal_N nonempty-type-eq-decl nil complex_measure_theory nil) (cal_N? const-decl "bool" complex_measure_theory nil) (mu formal-const-decl "measure_type[T, S]" complex_integral nil) (measure_type nonempty-type-eq-decl nil generalized_measure_def "measure_integration/") (measure? const-decl "bool" generalized_measure_def "measure_integration/") (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (S formal-const-decl "sigma_algebra[T]" complex_integral 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) (complex type-decl nil complex_types "complex_alt/") (T formal-type-decl nil complex_integral nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (measurable_ae_0 formula-decl nil integral "measure_integration/") (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/") (Im const-decl "[T -> real]" complex_fun_ops "complex_alt/") (integrable_def formula-decl nil complex_integral nil) (cal_N_def formula-decl nil complex_measure_theory nil)) nil)) (integrable_add 0 (integrable_add-1 nil 3476682466 ("" (skosimp) (("" (typepred "f1!1") (("" (typepred "f2!1") (("" (expand "integrable?") (("" (flatten) (("" (case-replace "Re((+[T])(f1!1, f2!1)) = +[T](Re(f1!1),Re(f2!1))") (("1" (case-replace "Im((+[T])(f1!1, f2!1)) = +[T](Im(f1!1),Im(f2!1))") (("1" (assert) (("1" (rewrite "integrable_add") (("1" (rewrite "integrable_add") nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (apply-extensionality :hide? t) (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) (("2" (apply-extensionality :hide? t) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((integrable nonempty-type-eq-decl nil complex_integral nil) (integrable? const-decl "bool" complex_integral nil) (complex type-decl nil complex_types "complex_alt/") (T formal-type-decl nil complex_integral nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (sum_complex_measurable application-judgement "complex_measurable" complex_integral nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (Re const-decl "[T -> real]" complex_fun_ops "complex_alt/") (+ const-decl "[T -> complex]" complex_fun_ops "complex_alt/") (+ const-decl "[T -> real]" real_fun_ops "reals/") (Im_fun_add1 formula-decl nil complex_fun_ops "complex_alt/") (Re_fun_add1 formula-decl nil complex_fun_ops "complex_alt/") (mu formal-const-decl "measure_type[T, S]" complex_integral nil) (measure_type nonempty-type-eq-decl nil generalized_measure_def "measure_integration/") (measure? const-decl "bool" generalized_measure_def "measure_integration/") (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (S formal-const-decl "sigma_algebra[T]" complex_integral 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) (integrable nonempty-type-eq-decl nil integral "measure_integration/") (integrable? const-decl "bool" integral "measure_integration/") (integrable_add judgement-tcc nil integral "measure_integration/") (Im const-decl "[T -> real]" complex_fun_ops "complex_alt/") (real_minus_real_is_real application-judgement "real" reals nil)) nil)) (integrable_scal 0 (integrable_scal-1 nil 3476682466 ("" (skosimp) (("" (typepred "f!1") (("" (expand "integrable?") (("" (flatten) (("" (assert) (("" (lemma "integrable_scal" ("c" "Re(c!1)" "f" "Re(f!1)")) (("" (lemma "integrable_scal" ("c" "Im(c!1)" "f" "Im(f!1)")) (("" (lemma "integrable_scal" ("c" "Im(c!1)" "f" "Re(f!1)")) (("" (lemma "integrable_scal" ("c" "Re(c!1)" "f" "Im(f!1)")) (("" (rewrite "integrable_diff") (("" (rewrite "integral.integrable_add") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((integrable nonempty-type-eq-decl nil complex_integral nil) (integrable? const-decl "bool" complex_integral nil) (complex type-decl nil complex_types "complex_alt/") (T formal-type-decl nil complex_integral nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (mu formal-const-decl "measure_type[T, S]" complex_integral nil) (measure_type nonempty-type-eq-decl nil generalized_measure_def "measure_integration/") (measure? const-decl "bool" generalized_measure_def "measure_integration/") (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (S formal-const-decl "sigma_algebra[T]" complex_integral 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/") (integrable nonempty-type-eq-decl nil integral "measure_integration/") (integrable? const-decl "bool" integral "measure_integration/") (Re const-decl "real" complex_types "complex_alt/") (integrable_scal judgement-tcc nil integral "measure_integration/") (* const-decl "[T -> real]" real_fun_ops "reals/") (integrable_diff judgement-tcc nil integral "measure_integration/") (integrable_add judgement-tcc nil integral "measure_integration/") (Im const-decl "[T -> real]" complex_fun_ops "complex_alt/") (Im const-decl "real" complex_types "complex_alt/") (Im_fun_mul2 formula-decl nil complex_fun_ops "complex_alt/") (Re_fun_mul2 formula-decl nil complex_fun_ops "complex_alt/") (scal_complex_measurable application-judgement "complex_measurable" complex_integral nil)) nil)) (integrable_opp 0 (integrable_opp-1 nil 3476682466 ("" (skosimp) (("" (assert) (("" (typepred "f!1") (("" (expand "integrable?" -) (("" (flatten) (("" (rewrite "integrable_opp") (("" (rewrite "integrable_opp") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((opp_complex_measurable application-judgement "complex_measurable[T, S]" complex_integral nil) (integrable_def formula-decl nil complex_integral nil) (Im_fun_neg1 formula-decl nil complex_fun_ops "complex_alt/") (Re_fun_neg1 formula-decl nil complex_fun_ops "complex_alt/") (T formal-type-decl nil complex_integral nil) (integrable_opp judgement-tcc nil integral "measure_integration/") (integrable? const-decl "bool" integral "measure_integration/") (integrable nonempty-type-eq-decl nil integral "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_integral nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (measure? const-decl "bool" generalized_measure_def "measure_integration/") (measure_type nonempty-type-eq-decl nil generalized_measure_def "measure_integration/") (mu formal-const-decl "measure_type[T, S]" complex_integral nil) (Im const-decl "[T -> real]" complex_fun_ops "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/") (integrable? const-decl "bool" complex_integral nil) (integrable nonempty-type-eq-decl nil complex_integral nil)) nil)) (integrable_diff 0 (integrable_diff-1 nil 3476682466 ("" (skosimp) (("" (typepred "f1!1") (("" (typepred "f2!1") (("" (assert) (("" (flatten) (("" (rewrite "integrable_diff") (("" (rewrite "integrable_diff") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((integrable nonempty-type-eq-decl nil complex_integral nil) (integrable? const-decl "bool" complex_integral nil) (complex type-decl nil complex_types "complex_alt/") (T formal-type-decl nil complex_integral nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (diff_complex_measurable application-judgement "complex_measurable" complex_integral nil) (integrable_def formula-decl nil complex_integral nil) (Re_fun_sub1 formula-decl nil complex_fun_ops "complex_alt/") (Im_fun_sub1 formula-decl nil complex_fun_ops "complex_alt/") (integrable_diff judgement-tcc nil integral "measure_integration/") (integrable? const-decl "bool" integral "measure_integration/") (integrable nonempty-type-eq-decl nil integral "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_integral nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (measure? const-decl "bool" generalized_measure_def "measure_integration/") (measure_type nonempty-type-eq-decl nil generalized_measure_def "measure_integration/") (mu formal-const-decl "measure_type[T, S]" complex_integral nil) (Im const-decl "[T -> real]" complex_fun_ops "complex_alt/")) nil)) (integrable_abs 0 (integrable_abs-1 nil 3477710890 ("" (skosimp) (("" (typepred "f!1") (("" (lemma "integrable_is_measurable") (("" (inst - "f!1") (("" (lemma "abs_complex_measurable" ("g" "f!1")) (("" (expand "integrable?" -3) (("" (flatten) (("" (lemma "integrable_abs" ("f" "Re(f!1)")) (("1" (lemma "integrable_abs" ("f" "Im(f!1)")) (("1" (case "forall x: abs(f!1)(x) <= (abs(Re(f!1))+abs(Im(f!1)))(x)") (("1" (lemma "integral.integrable_add" ("f1" "abs[T](Re(f!1))" "f2" "abs[T](Im(f!1))")) (("1" (lemma "integral_ae_abs" ("h" "abs(f!1)" "f" "abs(Re(f!1)) + abs(Im(f!1))")) (("1" (assert) (("1" (hide-all-but (1 -2)) (("1" (expand "ae_le?") (("1" (expand "pointwise_ae?") (("1" (expand "ae?") (("1" (expand "fullset") (("1" (expand "ae_in?") (("1" (inst + "emptyset") (("1" (skosimp) (("1" (expand "member") (("1" (hide 1) (("1" (inst - "x!1") (("1" (expand "abs" -1 1) (("1" (expand "abs" 1 1) (("1" (expand "abs" 1 2) (("1" (expand "abs" 1 1) (("1" (assert) (("1" (expand "abs" 1 2) (("1" (expand "abs" 1 2) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil) ("2" (propax) nil nil) ("3" (propax) nil nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp) (("2" (expand "abs") (("2" (expand "+") (("2" (expand "Im") (("2" (expand "Re") (("2" (expand "abs" 1 1) (("2" (expand "sq_abs") (("2" (lemma "sq_le" ("nna" "sqrt(sq(Im(f!1(x!1))) + sq(Re(f!1(x!1))))" "nnb" "abs(Im(f!1(x!1))) + abs(Re(f!1(x!1)))")) (("2" (replace -1 1 rl) (("2" (hide -1) (("2" (rewrite "sq_sqrt") (("2" (rewrite "sq_plus" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((integrable nonempty-type-eq-decl nil complex_integral nil) (integrable? const-decl "bool" complex_integral nil) (complex type-decl nil complex_types "complex_alt/") (T formal-type-decl nil complex_integral nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (mu formal-const-decl "measure_type[T, S]" complex_integral nil) (measure_type nonempty-type-eq-decl nil generalized_measure_def "measure_integration/") (measure? const-decl "bool" generalized_measure_def "measure_integration/") (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (Re const-decl "[T -> real]" complex_fun_ops "complex_alt/") (integrable nonempty-type-eq-decl nil integral "measure_integration/") (integrable? const-decl "bool" integral "measure_integration/") (integrable_abs judgement-tcc nil integral "measure_integration/") (<= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (abs const-decl "[T -> nonneg_real]" complex_fun_ops "complex_alt/") (+ const-decl "[T -> real]" real_fun_ops "reals/") (abs const-decl "[T -> nonneg_real]" real_fun_ops "reals/") (abs_complex_measurable application-judgement "measurable_function" complex_integral nil) (integral_ae_abs formula-decl nil integral "measure_integration/") (measurable_function? const-decl "bool" measure_space_def "measure_integration/") (measurable_function nonempty-type-eq-decl nil measure_space_def "measure_integration/") (pointwise_ae? const-decl "bool" measure_theory "measure_integration/") (fullset const-decl "set" sets nil) (null_emptyset name-judgement "null_set[T, S, mu]" complex_integral nil) (subset_algebra_emptyset name-judgement "(S)" complex_integral nil) (finite_emptyset name-judgement "finite_set[T]" sigma_countable "sigma_set/") (finite_emptyset name-judgement "finite_set[T]" countable_setofsets "sets_aux/") (finite_emptyset name-judgement "finite_set[T]" countable_props "sets_aux/") (finite_emptyset name-judgement "finite_set" finite_sets nil) (emptyset const-decl "set" sets nil) (negligible nonempty-type-eq-decl nil measure_theory "measure_integration/") (negligible_set? const-decl "bool" measure_theory "measure_integration/") (set type-eq-decl nil sets nil) (member const-decl "bool" sets nil) (TRUE const-decl "bool" booleans nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (ae_in? const-decl "bool" measure_theory "measure_integration/") (ae? const-decl "bool" measure_theory "measure_integration/") (measurable_fullset name-judgement "measurable_set[T, S]" complex_integral nil) (subset_algebra_fullset name-judgement "(S)" complex_integral nil) (ae_le? const-decl "bool" measure_theory "measure_integration/") (complex_measurable_def formula-decl nil complex_measurable nil) (abs_measurable application-judgement "measurable_function[T, S]" complex_integral nil) (integrable_add judgement-tcc nil integral "measure_integration/") (sq_abs const-decl "nnreal" complex_types "complex_alt/") (sq_sqrt formula-decl nil sqrt "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sq_abs formula-decl nil sq "reals/") (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (sq_plus formula-decl nil sq "reals/") (- const-decl "[numfield -> numfield]" number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans 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) (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (sq_le formula-decl nil sq "reals/") (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (abs const-decl "nnreal" polar "complex_alt/") (Im const-decl "[T -> real]" complex_fun_ops "complex_alt/") (abs_complex_measurable judgement-tcc nil complex_measurable nil) (complex_measurable? const-decl "bool" complex_measurable nil) (complex_measurable nonempty-type-eq-decl nil complex_measurable nil) (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets nil) (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration/") (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration/") (S formal-const-decl "sigma_algebra[T]" complex_integral nil) (integrable_is_measurable judgement-tcc nil complex_integral nil)) nil)) (integral_add 0 (integral_add-1 nil 3476767793 ("" (skosimp) (("" (expand "integral") (("" (assert) (("" (typepred "f1!1") (("" (typepred "f2!1") (("" (expand "integrable?") (("" (flatten) (("" (rewrite "integral_add") (("" (rewrite "integral_add") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((integral const-decl "complex" complex_integral nil) (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/") (integrable? const-decl "bool" complex_integral nil) (integrable nonempty-type-eq-decl nil complex_integral nil) (integral_add formula-decl nil integral "measure_integration/") (integrable? const-decl "bool" integral "measure_integration/") (integrable nonempty-type-eq-decl nil integral "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_integral nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (measure? const-decl "bool" generalized_measure_def "measure_integration/") (measure_type nonempty-type-eq-decl nil generalized_measure_def "measure_integration/") (mu formal-const-decl "measure_type[T, S]" complex_integral nil) (Im const-decl "[T -> real]" complex_fun_ops "complex_alt/") (T formal-type-decl nil complex_integral nil) (Re_fun_add1 formula-decl nil complex_fun_ops "complex_alt/") (Im_fun_add1 formula-decl nil complex_fun_ops "complex_alt/") (Re_rew formula-decl nil complex_types "complex_alt/") (Re_add1 formula-decl nil complex_types "complex_alt/") (Im_rew formula-decl nil complex_types "complex_alt/") (Im_add1 formula-decl nil complex_types "complex_alt/") (c_eq1 formula-decl nil complex_types "complex_alt/") (integrable_add application-judgement "integrable" complex_integral nil) (real_plus_real_is_real application-judgement "real" reals nil)) shostak)) (integral_scal 0 (integral_scal-1 nil 3476767954 ("" (skosimp) (("" (assert) (("" (typepred "f!1") (("" (expand "integrable?") (("" (flatten) (("" (lemma "integral.integrable_scal" ("c" "Re(c!1)" "f" "Re(f!1)")) (("1" (lemma "integral.integrable_scal" ("c" "Im(c!1)" "f" "Re(f!1)")) (("1" (lemma "integral.integrable_scal" ("c" "Re(c!1)" "f" "Im(f!1)")) (("1" (lemma "integral.integrable_scal" ("c" "Im(c!1)" "f" "Im(f!1)")) (("1" (rewrite "integral_diff" 1) (("1" (rewrite "integral.integral_add" 1) (("1" (rewrite "integral_scal" 1) (("1" (rewrite "integral_scal" 1) (("1" (rewrite "integral_scal" 1) (("1" (rewrite "integral_scal" 1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_plus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (integrable_scal application-judgement "integrable" complex_integral nil) (c_eq1 formula-decl nil complex_types "complex_alt/") (Im_mul1 formula-decl nil complex_types "complex_alt/") (Im_fun_mul2 formula-decl nil complex_fun_ops "complex_alt/") (Re_mul1 formula-decl nil complex_types "complex_alt/") (Im_integral formula-decl nil complex_integral nil) (Re_integral formula-decl nil complex_integral nil) (Re_fun_mul2 formula-decl nil complex_fun_ops "complex_alt/") (T formal-type-decl nil complex_integral nil) (mu formal-const-decl "measure_type[T, S]" complex_integral nil) (measure_type nonempty-type-eq-decl nil generalized_measure_def "measure_integration/") (measure? const-decl "bool" generalized_measure_def "measure_integration/") (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (S formal-const-decl "sigma_algebra[T]" complex_integral 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/") (integrable nonempty-type-eq-decl nil integral "measure_integration/") (integrable? const-decl "bool" integral "measure_integration/") (Re const-decl "real" complex_types "complex_alt/") (integrable_scal judgement-tcc nil integral "measure_integration/") (Im const-decl "[T -> real]" complex_fun_ops "complex_alt/") (* const-decl "[T -> real]" real_fun_ops "reals/") (integral_diff formula-decl nil integral "measure_integration/") (integral_scal formula-decl nil integral "measure_integration/") (minus_odd_is_odd application-judgement "odd_int" integers nil) (integral_add formula-decl nil integral "measure_integration/") (Im const-decl "real" complex_types "complex_alt/") (integrable nonempty-type-eq-decl nil complex_integral nil) (integrable? const-decl "bool" complex_integral nil) (complex type-decl nil complex_types "complex_alt/") (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) shostak)) (integral_opp 0 (integral_opp-1 nil 3477202455 ("" (skosimp) (("" (lemma "integral_scal" ("f" "f!1" "c" "complex_(-1,0)")) (("" (assert) (("" (flatten) (("" (case-replace "-1 * Re(f!1) - 0 * Im(f!1)=-(Re(f!1))") (("1" (assert) (("1" (case-replace "0 * Re(f!1) + -1 * Im(f!1)=-(Im(f!1))") (("1" (assert) nil nil) ("2" (apply-extensionality :hide? t) (("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (apply-extensionality :hide? t) (("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((integrable nonempty-type-eq-decl nil complex_integral nil) (integrable? const-decl "bool" complex_integral nil) (bool nonempty-type-eq-decl nil booleans nil) (T formal-type-decl nil complex_integral nil) (- const-decl "[numfield -> numfield]" number_fields 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) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (complex type-decl nil complex_types "complex_alt/") (integral_scal formula-decl nil complex_integral nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (Re const-decl "real" complex_types "complex_alt/") (Im const-decl "real" complex_types "complex_alt/") (+ const-decl "[T -> real]" real_fun_ops "reals/") (= const-decl "[T, T -> boolean]" equalities nil) (- const-decl "[T -> real]" real_fun_ops "reals/") (* const-decl "[T -> real]" real_fun_ops "reals/") (Re const-decl "[T -> real]" complex_fun_ops "complex_alt/") (Im const-decl "[T -> real]" complex_fun_ops "complex_alt/") (- const-decl "[T -> real]" real_fun_ops "reals/") (Im_neg1 formula-decl nil complex_types "complex_alt/") (Im_fun_neg1 formula-decl nil complex_fun_ops "complex_alt/") (Re_neg1 formula-decl nil complex_types "complex_alt/") (Re_fun_neg1 formula-decl nil complex_fun_ops "complex_alt/") (c_eq1 formula-decl nil complex_types "complex_alt/") (Im_mul1 formula-decl nil complex_types "complex_alt/") (Im_fun_mul2 formula-decl nil complex_fun_ops "complex_alt/") (Re_mul1 formula-decl nil complex_types "complex_alt/") (Im_integral formula-decl nil complex_integral nil) (Re_integral formula-decl nil complex_integral nil) (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/") (integrable_scal application-judgement "integrable" complex_integral nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (integrable_opp application-judgement "integrable" complex_integral nil) (minus_real_is_real application-judgement "real" reals nil)) shostak)) (integral_diff 0 (integral_diff-1 nil 3477202588 ("" (skosimp) (("" (lemma "integral_opp" ("f" "f2!1")) (("" (lemma "integral_add" ("f1" "f1!1" "f2" "-f2!1")) (("" (case-replace "f1!1 + -f2!1=f1!1 - f2!1") (("1" (assert) (("1" (flatten) (("1" (assert) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) (("1" (expand "-") (("1" (expand "+") (("1" (apply-extensionality :hide? t) nil nil)) nil)) nil) ("2" (expand "+") (("2" (expand "-") (("2" (apply-extensionality :hide? t) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((integrable nonempty-type-eq-decl nil complex_integral nil) (integrable? const-decl "bool" complex_integral 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_integral nil) (integral_opp formula-decl nil complex_integral nil) (- const-decl "[T -> complex]" complex_fun_ops "complex_alt/") (+ const-decl "[T -> complex]" complex_fun_ops "complex_alt/") (= const-decl "bool" complex_fun_ops "complex_alt/") (integrable_diff application-judgement "integrable" complex_integral nil) (integrable_add application-judgement "integrable" complex_integral nil) (Im_sub1 formula-decl nil complex_types "complex_alt/") (Re_sub1 formula-decl nil complex_types "complex_alt/") (Im_neg1 formula-decl nil complex_types "complex_alt/") (Re_neg1 formula-decl nil complex_types "complex_alt/") (c_eq1 formula-decl nil complex_types "complex_alt/") (Im_add1 formula-decl nil complex_types "complex_alt/") (Im_integral formula-decl nil complex_integral nil) (Re_add1 formula-decl nil complex_types "complex_alt/") (Re_integral formula-decl nil complex_integral nil) (c_fun_eq1 formula-decl nil complex_fun_ops "complex_alt/") (Im_fun_sub1 formula-decl nil complex_fun_ops "complex_alt/") (Im_fun_add1 formula-decl nil complex_fun_ops "complex_alt/") (Im_fun_neg1 formula-decl nil complex_fun_ops "complex_alt/") (Re_fun_sub1 formula-decl nil complex_fun_ops "complex_alt/") (Re_fun_add1 formula-decl nil complex_fun_ops "complex_alt/") (Re_fun_neg1 formula-decl nil complex_fun_ops "complex_alt/") (real_plus_real_is_real application-judgement "real" reals nil) (minus_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (+ const-decl "[T -> real]" real_fun_ops "reals/") (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (Im const-decl "real" complex_types "complex_alt/") (+ const-decl "[numfield, numfield -> numfield]" 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) (Im const-decl "[T -> real]" complex_fun_ops "complex_alt/") (- const-decl "[numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[T -> real]" real_fun_ops "reals/") (- const-decl "[T -> real]" real_fun_ops "reals/") (Re const-decl "real" complex_types "complex_alt/") (Re const-decl "[T -> real]" complex_fun_ops "complex_alt/") (integrable_opp application-judgement "integrable" complex_integral nil) (integral_add formula-decl nil complex_integral nil) (- const-decl "[T -> complex]" complex_fun_ops "complex_alt/")) shostak)) (integral_abs 0 (integral_abs-1 nil 3477711946 ("" (skosimp) (("" (typepred "f!1") (("" (lemma "integrable_abs" ("f" "f!1")) (("" (case "EXISTS c: abs(c) = 1 & abs(integral(f!1)) = c * integral(f!1)") (("1" (skosimp) (("1" (assert) (("1" (flatten) (("1" (typepred "abs(integral(f!1))") (("1" (replace -3) (("1" (hide -3) (("1" (name "A" "Re(c!1)") (("1" (replace -1) (("1" (name "B" "Im(c!1)") (("1" (replace -1) (("1" (name "G" "Re(f!1)") (("1" (replace -1) (("1" (name "H" "Im(f!1)") (("1" (replace -1) (("1" (case "A * integral.integral(G) - B *integral.integral(H) <= integral.integral(abs(A*G-B*H))") (("1" (lemma "integral_ae_le" ("f1" "abs(A * G - B * H)" "f2" "abs(f!1)")) (("1" (assert) (("1" (hide -1 -6 -8 -9 -10 -11 2) (("1" (expand "ae_le?") (("1" (expand "pointwise_ae?") (("1" (expand "ae?") (("1" (expand "fullset") (("1" (expand "ae_in?") (("1" (expand "member") (("1" (inst + "emptyset") (("1" (skosimp) (("1" (hide 1) (("1" (case-replace "abs(f!1)=abs(c!1*f!1)") (("1" (hide -1) (("1" (expand "abs" 1) (("1" (expand "*" 1) (("1" (expand "-" 1) (("1" (lemma "sq_le" ("nna" "abs(A * G(x!1) - B * H(x!1))" "nnb" "abs(c!1 * f!1(x!1))")) (("1" (replace -1 1 rl) (("1" (hide -1) (("1" (rewrite "sq_abs") (("1" (rewrite "sq_minus") (("1" (rewrite "sq_times") (("1" (rewrite "sq_times") (("1" (case "sq(A) * sq(G(x!1)) + sq(B) * sq(H(x!1)) - 2 * (G(x!1) * H(x!1) * A * B) <= (sq(A)+sq(B))*(sq(G(x!1))+sq(H(x!1)))") (("1" (rewrite "abs_mult" 1) (("1" (replace -6) (("1" (rewrite "sq_times" 1) (("1" (rewrite "one_times") (("1" (case-replace "sq(abs(f!1(x!1)))=sq(G(x!1)) + sq(H(x!1))") (("1" (case-replace "sq(A) + sq(B)=1") (("1" (assert) nil nil) ("2" (hide-all-but (1 -5 -6 -7)) (("2" (expand "abs") (("2" (lemma "sq_eq_rew" ("a" "sqrt(sq_abs(c!1))" "b" "1")) (("2" (rewrite "sq_sqrt") (("2" (expand "sq_abs") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-2 -3 1)) (("2" (expand "abs") (("2" (rewrite "sq_sqrt") (("2" (expand --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.38 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.Bot Zugriff |
