| products/sources/formale Sprachen/PVS/complex_integration/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: p_integrable_def.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(p_integrable_def
(mu_TCC1 0 (mu_TCC1-1 nil 3477417010 ("" (typepred "S") (("" (expand "sigma_algebra?") (("" (expand "subset_algebra_empty?") (("" (flatten) (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((finite_emptyset name-judgement "finite_set" finite_sets nil) (finite_emptyset name-judgement "finite_set[T]" countable_props "sets_aux/") (finite_emptyset name-judgement "finite_set[T]" countable_setofsets "sets_aux/") (member const-decl "bool" sets nil) (subset_algebra_empty? const-decl "bool" subset_algebra_def "measure_integration/") (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 p_integrable_def 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]" p_integrable_def nil)) nil)) (p_integrable?_TCC1 0 (p_integrable?_TCC1-1 nil 3477417010 ("" (skosimp) (("" (assert) (("" (typepred "p") (("" (assert) nil nil)) nil)) nil)) nil) ((real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (complex_measurable_def formula-decl nil complex_measurable nil) (T formal-type-decl nil p_integrable_def 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]" p_integrable_def nil) (NOT const-decl "[bool -> bool]" booleans 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) (p formal-const-decl "{a: real | a >= 1}" p_integrable_def nil)) nil)) (p_integrable_TCC1 0 (p_integrable_TCC1-1 nil 3477417010 ("" (expand "p_integrable?") (("" (rewrite "const_measurable") (("" (case-replace "(abs((LAMBDA x: complex_(0, 0))) ^ p)=lambda x:0") (("1" (rewrite "integrable_zero") nil nil) ("2" (apply-extensionality :hide? t) (("2" (hide 2) (("2" (expand "^") (("2" (expand "abs") (("2" (expand "abs") (("2" (expand "sq_abs") (("2" (assert) (("2" (rewrite "real_expt_0x") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (assert) nil nil)) nil)) nil)) nil) ((const_measurable formula-decl nil complex_measurable nil) (complex type-decl nil complex_types "complex_alt/") (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (complex_? adt-recognizer-decl "[complex -> boolean]" complex_types "complex_alt/") (complex_ adt-constructor-decl "[[real, real] -> (complex_?)]" complex_types "complex_alt/") (T formal-type-decl nil p_integrable_def 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]" p_integrable_def nil) (abs const-decl "nnreal" polar "complex_alt/") (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (Im_rew formula-decl nil complex_types "complex_alt/") (sq_0 formula-decl nil sq "reals/") (Re_rew formula-decl nil complex_types "complex_alt/") (sqrt_0 formula-decl nil sqrt "reals/") (real_expt_0x formula-decl nil real_expt "power/") (sq_abs const-decl "nnreal" complex_types "complex_alt/") (mu formal-const-decl "measure_type[T, S]" p_integrable_def 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/") (integrable_zero formula-decl nil integral "measure_integration/") (p formal-const-decl "{a: real | a >= 1}" p_integrable_def nil) (abs const-decl "[T -> nonneg_real]" complex_fun_ops "complex_alt/") (^ const-decl "[T -> nnreal]" real_fun_power "power/") (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (p_integrable? const-decl "bool" p_integrable_def nil)) nil)) (cal_N_is_p_integrable 0 (cal_N_is_p_integrable-1 nil 3477463561 ("" (skolem + "f!1") (("" (typepred "f!1") (("" (expand "cal_N?") (("" (expand "p_integrable?") (("" (flatten) (("" (replace -2) (("" (lemma "measurable_ae_0" ("h" "abs(f!1)^p")) (("1" (assert) (("1" (hide -2 2) (("1" (expand "ae_0?") (("1" (expand "restrict") (("1" (expand "pointwise_ae?") (("1" (expand "ae?") (("1" (expand "fullset") (("1" (expand "ae_in?") (("1" (skosimp) (("1" (inst + "E!1") (("1" (skosimp) (("1" (inst - "x!1") (("1" (expand "member") (("1" (replace 1) (("1" (hide 1) (("1" (expand "^" 1) (("1" (expand "abs" 1) (("1" (rewrite "real_expt_is_0") (("1" (rewrite "abs_is_0") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2 -1) (("2" (lemma "abs_complex_measurable" ("g" "f!1")) (("2" (lemma "expt_measurable" ("g" "abs(f!1)" "a" "p")) (("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) ("3" (assert) nil nil)) nil)) nil)) nil) ("3" (typepred "p") (("3" (assert) nil 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]" p_integrable_def 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]" p_integrable_def 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 p_integrable_def nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (p_integrable? const-decl "bool" p_integrable_def nil) (expt_measurable judgement-tcc nil measure_space "measure_integration/") (nn_measurable? const-decl "bool" measure_space "measure_integration/") (nn_measurable nonempty-type-eq-decl nil measure_space "measure_integration/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (complex_measurable nonempty-type-eq-decl nil complex_measurable nil) (complex_measurable? const-decl "bool" complex_measurable nil) (abs_complex_measurable judgement-tcc nil complex_measurable nil) (complex_measurable_def formula-decl nil complex_measurable nil) (ae_0? const-decl "bool" complex_measure_theory nil) (ae_0? const-decl "bool" measure_theory "measure_integration/") (pointwise_ae? const-decl "bool" complex_measure_theory nil) (pointwise_ae? const-decl "bool" measure_theory "measure_integration/") (fullset const-decl "set" sets nil) (member const-decl "bool" sets nil) (abs_is_0 formula-decl nil polar "complex_alt/") (c_eq3 formula-decl nil complex_types "complex_alt/") (Re_rew formula-decl nil complex_types "complex_alt/") (Im_rew formula-decl nil complex_types "complex_alt/") (c_eq1 formula-decl nil complex_types "complex_alt/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_expt_is_0 formula-decl nil real_expt "power/") (abs const-decl "nnreal" polar "complex_alt/") (OR const-decl "[bool, bool -> bool]" booleans nil) (TRUE const-decl "bool" booleans nil) (set type-eq-decl nil sets nil) (negligible_set? const-decl "bool" measure_theory "measure_integration/") (negligible nonempty-type-eq-decl nil measure_theory "measure_integration/") (ae_in? const-decl "bool" measure_theory "measure_integration/") (ae? const-decl "bool" measure_theory "measure_integration/") (subset_algebra_fullset name-judgement "(S)" p_integrable_def nil) (measurable_fullset name-judgement "measurable_set[T, S]" p_integrable_def nil) (restrict const-decl "R" restrict nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (abs_complex_measurable application-judgement "measurable_function" p_integrable_def 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/") (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (^ const-decl "[T -> nnreal]" real_fun_power "power/") (abs const-decl "[T -> nonneg_real]" complex_fun_ops "complex_alt/") (p formal-const-decl "{a: real | a >= 1}" p_integrable_def nil)) nil)) (norm_TCC1 0 (norm_TCC1-1 nil 3477417965 ("" (assert) (("" (assert) nil nil)) nil) ((real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (norm_TCC2 0 (norm_TCC2-1 nil 3477417965 ("" (skosimp) (("" (typepred "f!1") (("" (expand "p_integrable?") (("" (flatten) nil nil)) nil)) nil)) nil) ((p_integrable nonempty-type-eq-decl nil p_integrable_def nil) (p_integrable? const-decl "bool" p_integrable_def nil) (complex type-decl nil complex_types "complex_alt/") (T formal-type-decl nil p_integrable_def nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil)) (norm_TCC3 0 (norm_TCC3-1 nil 3477417965 ("" (skosimp) (("" (rewrite "integral_nonneg") (("" (hide 2) (("" (skosimp) (("" (expand "^") (("" (expand "abs") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (integral_nonneg formula-decl nil integral "measure_integration/") (integrable? const-decl "bool" integral "measure_integration/") (integrable nonempty-type-eq-decl nil integral "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) (^ const-decl "[T -> nnreal]" real_fun_power "power/") (complex type-decl nil complex_types "complex_alt/") (abs const-decl "[T -> nonneg_real]" complex_fun_ops "complex_alt/") (p_integrable? const-decl "bool" p_integrable_def nil) (p_integrable nonempty-type-eq-decl nil p_integrable_def nil) (p formal-const-decl "{a: real | a >= 1}" p_integrable_def nil) (T formal-type-decl nil p_integrable_def 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]" p_integrable_def 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]" p_integrable_def nil)) nil)) (norm_TCC4 0 (norm_TCC4-1 nil 3477417965 ("" (assert) nil nil) nil nil)) (norm_TCC5 0 (norm_TCC5-1 nil 3477417965 ("" (skosimp) (("" (assert) (("" (lemma "posreal_div_posreal_is_posreal" ("px" "1" "py" "p")) (("" (assert) nil nil)) nil)) nil)) nil) ((real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (posreal_div_posreal_is_posreal judgement-tcc nil real_types nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (>= 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) (p formal-const-decl "{a: real | a >= 1}" p_integrable_def nil)) nil)) (norm_eq_0 0 (norm_eq_0-1 nil 3477453337 ("" (skosimp) (("" (expand "cal_N?") (("" (typepred "f!1") (("" (expand "p_integrable?") (("" (flatten) (("" (replace -1) (("" (expand "norm") (("" (lemma "abs_complex_measurable" ("g" "f!1")) (("1" (lemma "expt_measurable" ("g" "abs[T](f!1)" "a" "p")) (("1" (lemma "posreal_div_posreal_is_posreal" ("px" "1" "py" "p")) (("1" (lemma "integral_nonneg" ("f" "abs(f!1)^p")) (("1" (case-replace "FORALL (x: T): (abs(f!1) ^ p)(x) >= 0") (("1" (rewrite "real_expt_is_0" 1) (("1" (replace -3) (("1" (split 1) (("1" (flatten) (("1" (lemma "integral_ae_ge_0" ("f" "abs(f!1) ^ p")) (("1" (split -1) (("1" (hide-all-but (-1 1)) (("1" (expand "ae_0?") (("1" (expand "restrict") (("1" (expand "pointwise_ae?") (("1" (expand "ae?") (("1" (expand "fullset") (("1" (expand "ae_in?") (("1" (skosimp) (("1" (inst + "E!1") (("1" (skosimp) (("1" (inst - "x!1") (("1" (expand "member") (("1" (replace 1) (("1" (hide 1) (("1" (expand "^") (("1" (expand "abs") (("1" (rewrite "real_expt_is_0") (("1" (rewrite "abs_is_0") (("1" (assert) 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 "ae_nonneg?") (("2" (expand "pointwise_ae?") (("2" (expand "ae?") (("2" (expand "fullset") (("2" (expand "ae_in?") (("2" (inst + "emptyset") (("2" (skosimp) (("2" (expand "member") (("2" (inst - "x!1") (("2" (hide 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (propax) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (lemma "measurable_ae_0" ("h" "abs(f!1)^p")) (("1" (split -1) (("1" (flatten) nil nil) ("2" (hide-all-but (-1 1)) (("2" (expand "ae_0?") (("2" (expand "restrict") (("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" (replace 1) (("2" (hide 1) (("2" (expand "^") (("2" (expand "abs") (("2" (rewrite "real_expt_is_0") (("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) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "^") (("2" (hide-all-but 1) (("2" (expand "abs") (("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "nn_measurable?") (("2" (assert) (("2" (hide-all-but 1) (("2" (skosimp) (("2" (expand "abs") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((cal_N? const-decl "bool" complex_measure_theory nil) (S formal-const-decl "sigma_algebra[T]" p_integrable_def 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 nonempty-type-eq-decl nil complex_measurable nil) (complex_measurable? const-decl "bool" complex_measurable nil) (abs_complex_measurable judgement-tcc nil complex_measurable nil) (Im const-decl "[T -> real]" complex_fun_ops "complex_alt/") (Re const-decl "[T -> real]" complex_fun_ops "complex_alt/") (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) (AND const-decl "[bool, bool -> bool]" booleans nil) (complex_measurable_def formula-decl nil complex_measurable nil) (posreal_div_posreal_is_posreal judgement-tcc nil real_types nil) (measurable_function nonempty-type-eq-decl nil measure_space_def "measure_integration/") (measurable_ae_0 formula-decl nil integral "measure_integration/") (ae_0? const-decl "bool" complex_measure_theory nil) (ae_0? const-decl "bool" measure_theory "measure_integration/") (pointwise_ae? const-decl "bool" complex_measure_theory nil) (pointwise_ae? const-decl "bool" measure_theory "measure_integration/") (fullset const-decl "set" sets nil) (member const-decl "bool" sets nil) (abs_is_0 formula-decl nil polar "complex_alt/") (c_eq3 formula-decl nil complex_types "complex_alt/") (Re_rew formula-decl nil complex_types "complex_alt/") (Im_rew formula-decl nil complex_types "complex_alt/") (c_eq1 formula-decl nil complex_types "complex_alt/") (abs const-decl "nnreal" polar "complex_alt/") (TRUE const-decl "bool" booleans nil) (set type-eq-decl nil sets nil) (negligible_set? const-decl "bool" measure_theory "measure_integration/") (negligible nonempty-type-eq-decl nil measure_theory "measure_integration/") (ae_in? const-decl "bool" measure_theory "measure_integration/") (ae? const-decl "bool" measure_theory "measure_integration/") (subset_algebra_fullset name-judgement "(S)" p_integrable_def nil) (measurable_fullset name-judgement "measurable_set[T, S]" p_integrable_def nil) (restrict const-decl "R" restrict nil) (ae_nonneg? const-decl "bool" measure_theory "measure_integration/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (emptyset const-decl "set" sets nil) (finite_emptyset name-judgement "finite_set" finite_sets nil) (finite_emptyset name-judgement "finite_set[T]" countable_props "sets_aux/") (finite_emptyset name-judgement "finite_set[T]" countable_setofsets "sets_aux/") (finite_emptyset name-judgement "finite_set[T]" sigma_countable "sigma_set/") (null_emptyset name-judgement "null_set[T, S, mu]" p_integrable_def nil) (subset_algebra_emptyset name-judgement "(S)" p_integrable_def nil) (integral_ae_ge_0 formula-decl nil integral "measure_integration/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_expt_is_0 formula-decl nil real_expt "power/") (integral const-decl "real" integral "measure_integration/") (OR const-decl "[bool, bool -> bool]" booleans 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) (^ const-decl "nnreal" real_expt "power/") (mu formal-const-decl "measure_type[T, S]" p_integrable_def 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 "[T -> nnreal]" real_fun_power "power/") (integrable nonempty-type-eq-decl nil integral "measure_integration/") (integrable? const-decl "bool" integral "measure_integration/") (integral_nonneg formula-decl nil integral "measure_integration/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (expt_measurable judgement-tcc nil measure_space "measure_integration/") (>= 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) (p formal-const-decl "{a: real | a >= 1}" p_integrable_def 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/") (norm const-decl "nnreal" p_integrable_def 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 p_integrable_def nil) (complex type-decl nil complex_types "complex_alt/") (p_integrable? const-decl "bool" p_integrable_def nil) (p_integrable nonempty-type-eq-decl nil p_integrable_def nil)) shostak))) ¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.39Angebot Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤ |
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
ZieleEntwicklung einer Software für die statische QuellcodeanalyseBot Zugriff |
