Impressum minkowski_scaf.prf
Interaktion und
(minkowski_scafnil 3477582206"" (typepred "S" )"" (expand "sigma_algebra?" )"" (flatten)"" (expand "subset_algebra_empty?" ) (("" (assert ) nil nil ))nil ))nil ))nil ))nil )"bool" subset_algebra_def"measure_integration/" )"finite_set" finite_sets nil )"finite_set[T]" countable_props"sets_aux/" )"finite_set[T]" countable_setofsets"sets_aux/" )"bool" sets nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil minkowski_scaf nil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def"measure_integration/" )nil subset_algebra_def"measure_integration/" )"sigma_algebra[T]" minkowski_scaf nil ))nil ))nil 3477583588"" (skosimp)"" (name "KK" "reals@real_fun_ops_aux[T].max(abs(f!1),abs(g!1))" )"" case "forall (x:T): abs(f!1+g!1)(x) <= abs(f!1)(x)+abs(g!1)(x) & abs(f!1)(x)+abs(g!1)(x) <= 2*KK(x)" )"1" (case "integrable?(+[T](abs[T](f!1)^p,abs[T](g!1)^p))" )"1" "nn_integrable_le" "f" "2^p * (abs[T](f!1) ^ p + abs[T](g!1) ^ p)" "g" "abs(f!1 + g!1)^p" ))"1" (split -1)"1" (flatten)"1" (lemma "nn_integrable_is_integrable" )"1" (inst - "abs(f!1 + g!1) ^ p" )"1" (rewrite "integral_nn" -3 :dir rl)"1" (case-replace "p_integrable?(f!1 + g!1)" )"1" (expand "norm" )"1" (typepred "p" )"1" (expand ">=" -1)"1" expand "<=" -1)"1" "1" "q" "p/(p-1)" )"1" case "q>1 & 1/p+1/q =1" )"1" "1" "1" case "abs(f!1 + g!1) ^ p=(abs(f!1 + g!1) ^(p-1))^q" )"1" "H" "abs(f!1 + g!1) ^ (p - 1)" )"1" replace -1)"1" "CH" "lambda (x:T): complex_(H(x),0)" )"1" case "p_integrable?[T,S,mu,p/(p-1)](CH)" )"1" case "norm[T,S,mu,p / (p - 1)](CH) = norm(f!1+g!1)^(p/q)" )"1" "holder_scaf[T,S,mu,p,p / (p - 1)]" "f" "f!1" "g" "CH" ))"1" "holder_scaf[T,S,mu,p,p / (p - 1)]" "f" "g!1" "g" "CH" ))"1" replace "1" case "forall (f:p_integrable[T,S,mu,1]): integral.integrable?(abs(f)) & norm[T, S, mu, 1](f) = integral.integral(abs(f))" )"1" "f!1*CH" )"1" "g!1*CH" )"1" "1" case "integral.integral(abs(f!1 * CH)+abs(g!1 * CH)) <= (norm[T, S, mu, p](f!1) + norm[T, S, mu, p](g!1))* norm(f!1 + g!1) ^ (p / q)" )"1" "RHS" "norm[T, S, mu, p](f!1) + norm[T, S, mu, p](g!1)" )"1" replace "1" expand "norm" "1" replace "1" "1" "1" case "abs(f!1 + g!1)*H = abs(f!1 + g!1) ^ p" )"1" "integral_ae_le" "f1" "abs(f!1+g!1)*H" "f2" "abs(f!1 * CH) + abs(g!1 * CH)" ))"1" "INT" "integral.integral(abs(f!1 * CH) + abs(g!1 * CH))" )"1" "1" replace "1" expand "norm" "1" "integral_nonneg" "f" "abs(f!1 + g!1) ^ p" ))"1" "1" "INT2" "integral.integral(abs(f!1 + g!1) ^ p)" )"1" "1" "real_expt_times" "x" "INT2" "a" "1/p" "b" "p/q" ))"1" "1 / p * (p / q)=1/q" )"1" replace "1" case "INT2 <= RHS * INT2 ^ (1 / q)" )"1" "1" expand ">=" "1" expand "<=" "1" "1" "posreal_div_posreal_is_posreal" "px" "1" "py" "p" ))"1" "posreal_div_posreal_is_posreal" "px" "1" "py" "q" ))"1" "real_expt_plus" "x" "INT2" "a" "1/p" "b" "1/q" ))"1" replace "1" rewrite "real_expt_x1" "1" "real_expt_pos" "px" "INT2" "a" "1/q" ))"1" "both_sides_times_pos_le1" "pz" "INT2 ^ (1 / q)" "x" "INT2 ^ (1 / p)" "y" "RHS" ))"1" replace "1" assert )nil nil ))nil )"2" nil nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" rewrite "real_expt_0x" "1" expand "RHS" )"1" assert )nil nil ))nil )"2" "posreal_div_posreal_is_posreal" "px" "1" "py" "p" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"2" assert )nil nil ))nil )"2" nil nil ))nil ))nil ))nil )"2" "2" expand "^" "2" expand "abs" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "ae_le?" )"2" expand "pointwise_ae?" )"2" expand "ae?" )"2" expand "fullset" )"2" expand "ae_in?" )"2" "emptyset" )"2" "2" expand "member" )"2" "2" expand "*" "2" expand "+" "2" expand "abs" "2" expand "+" "2" replace "2" "2" replace "2" "2" "2" expand "^" "2" expand "abs" "2" expand "+" "2" expand "abs" "2" expand "abs" "2" expand "+ " "2" expand "+ " "2" rewrite "abs_mult" "2" rewrite "abs_mult" "2" "abs(f!1(x!1) + g!1(x!1)) ^ (p - 1)" )"2" "FGp1" "abs(f!1(x!1) + g!1(x!1)) ^ (p - 1)" )"2" expand "abs" "2" expand "abs" "2" expand "sq_abs" )"2" expand "Im" "2" expand "Re" "2" rewrite "sq_0" )"2" "sqrt_sq" )"2" "FGp1" )"2" "1" replace "1" "1" expand ">=" "1" expand "<=" "1" "1" "both_sides_times_pos_le1" "pz" "FGp1" "x" "abs(f!1(x!1) + g!1(x!1))" "y" "abs(f!1(x!1))+abs(g!1(x!1))" ))"1" replace "1" "1" rewrite "abs_triangle" )nil nil ))nil ))nil )"2" assert )nil nil ))nil )"2" replace "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" nil nil ))nil ))nil )"2" "2" "2" expand "*" "2" replace "2" expand "^" "2" "abs(f!1 + g!1)(x!1)" )"2" "ABS" "abs(f!1 + g!1)(x!1)" )"2" "2" "real_expt_plus" "x" "ABS" "a" "1" "b" "p-1" ))"2" rewrite "real_expt_x1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "integral.integral_add" "2" assert )nil nil ))nil )"3" rewrite "integral.integrable_add" nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" "f!2" )"2" expand "p_integrable?" )"2" "2" expand "norm" )"2" "abs(f!2) ^ 1=abs(f!2)" )"1" replace "1" rewrite "real_expt_x1" )"1" "integral_nonneg" "f" "abs(f!2)" ))"1" assert )"1" "1" expand "abs" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "abs" )"2" expand "^" )"2" rewrite "real_expt_x1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" assert )nil nil ))nil ))nil )"2" replace -8)"2" assert )nil nil ))nil )"3" assert )nil nil ))nil )"2" "2" expand "norm" )"2" "abs(CH) ^ (p / (p - 1))=abs(f!1 + g!1) ^ p" )"1" "integral_nonneg" "f" "abs(f!1 + g!1) ^ p" ))"1" "1" "INT" "integral.integral(abs(f!1 + g!1) ^ p)" )"1" "(1 / (p / (p - 1)))=1/q" )"1" "1" rewrite "real_expt_times" "1" rewrite "div_times" nil nil ))nil ))nil )"2" "2" "2" replace "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "^" )"2" expand "abs" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" replace "2" "abs(CH)=H" )"2" "2" "2" expand "abs" )"2" expand "abs" )"2" expand "sq_abs" )"2" expand "CH" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" assert )"3" replace "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"3" "posreal_div_posreal_is_posreal" "px" "p" "py" "q" ))"1" assert )nil nil )"2" assert )nil nil ))nil )"4" nil nil )"5" nil nil ))nil )"2" "2" expand "p_integrable?" "2" "1" expand "complex_measurable?" "1" replace "1" expand "Re" "1" expand "Im" "1" assert )"1" "1" expand "H" )"1" expand "^" "1" expand "abs" "1" expand "+" "1" "expt_measurable" "g" "abs(f!1 + g!1)" "a" "p-1" ))"1" expand "^" "1" expand "abs" "1" expand "+" "1" nil nil ))nil ))nil ))nil )"2" expand "nn_measurable?" "2" "1" assert )"1" "1" "f!1" )"1" "g!1" )"1" expand "p_integrable?" )"1" "1" "sum_complex_measurable" "g1" "f!1" "g2" "g!1" ))"1" "abs_complex_measurable" "g" "(+[T])(f!1, g!1)" ))"1" nil nil )"2" assert )nil nil ))nil )"2" assert )nil nil )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "abs" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "measure_space.const_measurable" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" "abs(CH) ^ q=abs(f!1 + g!1) ^ p" )"1" replace "1" "1" "abs(CH)=H" )"1" "1" "1" expand "CH" )"1" expand "abs" )"1" assert )"1" expand "abs" )"1" expand "sq_abs" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"3" assert )"3" replace -6)"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "^" )"2" expand "abs" )"2" "abs((f!1 + g!1)(x!1))" )"2" "FG" "abs((f!1 + g!1)(x!1))" )"2" rewrite "real_expt_times" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (assert ) nil nil )"4" (assert ) nil nil ))nil ))nil ))nil )"2" "2" "q>1" )"1" rewrite "div_cancel3" -2)"1" "div_cancel3" "n0z" "p" "x" "1" "y" "1-1/q" ))"1" "1" "1" "1" assert )nil nil )"2" "2" assert )"2" "div_cancel3" "n0z" "q" "x" "p" "y" "p-1" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "posreal_div_posreal_is_posreal" "px" "p" "py" "p-1" ))"1" replace -2)"1" replace -2 * rl)"1" rewrite "div_mult_pos_gt1" nil nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"3" assert )"3" "3" "3" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" replace -1 * rl)"2" rewrite "div_simp" )"2" case "forall f: abs(f) ^ 1=abs(f)" )"1" "f!1" )"1" "g!1" )"1" "f!1+g!1" )"1" "f!1" )"1" "g!1" )"1" expand "p_integrable?" )"1" "1" replace "1" replace -5)"1" replace "1" replace "1" rewrite "real_expt_x1" "1" rewrite "real_expt_x1" "1" rewrite "real_expt_x1" "1" rewrite "integral.integral_add" "1" "integral_ae_le" "f1" "abs(f!1 + g!1)" "f2" "abs(f!1) + abs(g!1)" ))"1" "1" nil nil )"2" "2" expand "ae_le?" )"2" expand "pointwise_ae?" )"2" expand "ae?" )"2" expand "fullset" )"2" expand "ae_in?" )"2" "emptyset" )"2" "2" expand "member" )"2" "2" expand "abs" )"2" expand "+ " )"2" rewrite "abs_triangle" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "integral_nonneg" "f" "abs[T](g!1)" ))"2" assert )"2" "2" expand "abs" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "integral_nonneg" "f" "abs[T](f!1)" ))"2" assert )"2" "2" expand "abs" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "integral_nonneg" "f" "abs(f!1 + g!1)" ))"2" "1" nil nil )"2" "2" expand "abs" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" expand "^" )"2" expand "abs" )"2" rewrite "real_expt_x1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (expand "p_integrable?" )"2" (replace -1)"2" rewrite "sum_complex_measurable" )"1" "g!1" )"1" expand "p_integrable?" )"1" "1" (assert ) nil nil ))nil ))nil ))nil )"2" "f!1" )"2" expand "p_integrable?" )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp)"2" (expand "abs" 1)"2" (expand "^" 1 1)"2" (expand "^" 1 2)"2" (split 1)"1" (assert ) nil nil )"2" (expand "+" 1)"2" (expand "^" 1 3)"2" expand "*" 1)"2" expand "^" 1 2)"2" "x!1" )"2" "2" expand "+ " -1)"2" expand "abs" -1)"2" "2" case "abs(f!1(x!1) + g!1(x!1)) <= 2 * KK(x!1)" )"1" "1" case "KK(x!1)^p <= abs(f!1(x!1)) ^ p + abs(g!1(x!1)) ^ p" )"1" "real_expt_pos" "px" "2" "a" "p" ))"1" "both_sides_times_pos_le1" "pz" "2^p" "x" "KK(x!1) ^ p" "y" "abs(f!1(x!1)) ^ p + abs(g!1(x!1)) ^ p" ))"1" assert )"1" rewrite "mult_real_expt" "1" "RHS" "2 ^ p * abs(f!1(x!1)) ^ p + 2 ^ p * abs(g!1(x!1)) ^ p" )"1" "both_sides_real_expt_le" "pa" "p" "x" "abs(f!1(x!1)+g!1(x!1))" "y" "2 * KK(x!1)" ))"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil )"2" expand "KK" )"2" "2" expand "max" )"2" expand "abs" "2" expand "abs" "2" expand "max" )"2" "abs(f!1(x!1)) < abs(g!1(x!1))" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" assert )nil nil )"4" assert )nil nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (typepred "f!1" )"2" (typepred "g!1" )"2" (expand "p_integrable?" )"2" (flatten)"2" (hide -2 -4)"2" "sum_complex_measurable" "g1" "f!1" "g2" "g!1" ))"1" "abs_complex_measurable" "g" "f!1+g!1" ))"1" (rewrite "expt_measurable" )"1" expand "nn_measurable?" )"1" "1" "1" expand "abs" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" (assert ) nil nil )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide 2)"3" (split)"1" (skolem + "x!1" )"1" (expand "*" )"1" (expand "+" 1)"1" (expand "^" 1 1)"1" (expand "^" 1 1)"1" (expand "abs" 1)"1" "both_sides_times_pos_ge1" "pz" "2^p" "x" "abs(f!1(x!1)) ^ p+abs(g!1(x!1)) ^ p" "y" "0" ))"1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "FF" "((+[T])(abs[T](f!1) ^ p, abs[T](g!1) ^ p))" )"1" "nn_integrable_scal[T, S, mu]" "c" "2^p" "f" "FF" ))"1" (flatten) nil nil )"2" (hide 2)"2" (split)"1" (skolem + "x!1" )"1" (expand "FF" )"1" (expand "^" 1)"1" expand "+" 1)"1" expand "abs" 1)"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "nn_integrable_is_nn_integrable" )"2" (inst - "FF" )"2" (split)"1" (propax) nil nil )"2" "2" "2" expand "FF" )"2" expand "+" )"2" expand "^" )"2" expand "abs" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil )"4" (assert ) nil nil ))nil )"2" (hide 2)"2" (typepred "f!1" )"2" (typepred "g!1" )"2" (expand "p_integrable?" )"2" (flatten)"2" (rewrite "integral.integrable_add" +) nil nil ))nil ))nil ))nil ))nil ))nil )"3" (assert ) (("3" (assert ) nil nil )) nil ))nil )"2" (hide 2)"2" (skosimp)"2" (replace -1 * rl)"2" (hide -1)"2" (expand "abs" )"2" (expand "max" )"2" (expand "+" )"2" (rewrite "abs_triangle" )"2" (expand "max" )"2" (assert )"2" (lift-if)"2" "1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil p_integrable_def nil )"bool" p_integrable_def nil )"{x: real | x >= 1}" minkowski_scaf nil )"measure_type[T, S]" minkowski_scaf nil )nil generalized_measure_def"measure_integration/" )"bool" generalized_measure_def"measure_integration/" )nil extended_nnreal"extended_nnreal/" )nil real_types nil )"sigma_algebra[T]" minkowski_scaf nil )nil subset_algebra_def"measure_integration/" )"bool" subset_algebra_def"measure_integration/" )nil sets nil )nil defined_types nil )"[T -> nonneg_real]" complex_fun_ops"complex_alt/" )nil real_types nil )"bool" reals nil )nil booleans nil )nil complex_types "complex_alt/" )max const-decl "[T -> real]" real_fun_ops_aux "reals/" )"[T, T -> boolean]" equalities nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil minkowski_scaf nil )"{z: nonneg_real | z >= x AND z >= y}" real_defs nil )"bool" integral "measure_integration/" )"[T -> real]" real_fun_ops "reals/" )"bool" reals nil )nil real_types nil )"[T -> nnreal]" real_fun_power "power/" )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil integral"measure_integration/" )"[T -> real]" minkowski_scaf nil )nil nn_integral"measure_integration/" )nil real_props nil )nil integral"measure_integration/" )nil integral "measure_integration/" )"nnreal" p_integrable_def nil )"real" reals nil )"[bool, bool -> bool]" booleans nil )"real" minkowski_scaf nil )"[complex -> boolean]" complex_types"complex_alt/" )"[[real, real] -> (complex_?)]" "complex_alt/" )"[T -> real]" complex_fun_ops "complex_alt/" )nil complex_measurable nil )nil complex_measurablenil )nil complex_fun_ops "complex_alt/" )nil complex_fun_ops "complex_alt/" )nil complex_measurable nil )nil measure_space"measure_integration/" )"bool" measure_space"measure_integration/" )nil measure_space"measure_integration/" )"[T -> nnreal]" minkowski_scaf nil )nil measure_space"measure_integration/" )"[T -> real]" complex_fun_ops "complex_alt/" )"bool" complex_measurable nil )nil integral"measure_integration/" )"real" integral "measure_integration/" )"nnreal" nil )"[T -> real]" real_fun_ops "reals/" )nil complex_fun_ops "complex_alt/" )nil integral "measure_integration/" )nil real_expt "power/" )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil real_props nil )nil real_expt "power/" )nil real_expt "power/" )nil real_types nil )nil real_expt "power/" )"nnreal" minkowski_scaf nil )nil real_expt "power/" )nil integral "measure_integration/" )"bool" measure_theory "measure_integration/" )"(S)" minkowski_scaf nil )"measurable_set[T, S]" nil )"bool" measure_theory "measure_integration/" )"bool" measure_theory "measure_integration/" )"real" complex_types "complex_alt/" )nil sq "reals/" )nil polar "complex_alt/" )nil sqrt "reals/" )"real" complex_types "complex_alt/" )"nnreal" complex_types "complex_alt/" )nil polar "complex_alt/" )"bool" booleans nil )"nnreal" polar "complex_alt/" )"complex" complex_types "complex_alt/" )"bool" sets nil ) (set type-eq-decl nil sets nil )"bool" measure_theory"measure_integration/" )nil measure_theory"measure_integration/" )"set" sets nil )"finite_set" finite_sets nil )"finite_set[T]" countable_props"sets_aux/" )"finite_set[T]" countable_setofsets"sets_aux/" )"finite_set[T]" sigma_countable"sigma_set/" )"finite_set[T]" step_fun_props"analysis/" )"(S)" minkowski_scaf nil )"null_set[T, S, mu]" minkowski_scafnil )"set" sets nil )"bool" measure_theory"measure_integration/" )nil integral "measure_integration/" )nil integral "measure_integration/" )"[T -> complex]" complex_fun_ops "complex_alt/" )nil complex_measurable nil )nil holder_scaf nil )"nzreal" nil )"posreal" nil )"[T -> (complex_?)]" minkowski_scaf nil )nil complex_types "complex_alt/" )nil complex_types "complex_alt/" )nil real_props nil )nil real_props nil )nil real_props nil )nil real_props nil )nil reals nil )nil real_props nil )nil extra_real_props nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )"real" reals nil )"real" reals nil )nil real_props nil )"p_integrable[T, S, mu, p]" minkowski_scafnil )"p_integrable[T, S, mu, p]" minkowski_scafnil )NOT const-decl "[bool -> bool]" booleans nil )nil real_expt "power/" )nil real_expt "power/" )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"bool" reals nil )"[T -> real]" minkowski_scaf nil )nil measure_space_def"measure_integration/" )"bool" measure_space_def"measure_integration/" )"nnreal" real_expt "power/" )OR const-decl "[bool, bool -> bool]" booleans nil )"[T -> real]" real_fun_ops "reals/" )nil nn_integral"measure_integration/" )"bool" nn_integral"measure_integration/" )nil nn_integral"measure_integration/" )"nnreal" nil )"real" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )"[T -> complex]" complex_fun_ops "complex_alt/" )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fieldsnil ))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ 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.0.120Bemerkung:
(Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können 2026-04-28)
¤ *Eine klare Vorstellung vom Zielzustand
2026-05-26
