Quelle holder_scaf.prf
Sprache: Lisp
(holder_scafnil 3477456171"" (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 holder_scaf nil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def"measure_integration/" )nil subset_algebra_def"measure_integration/" )"sigma_algebra[T]" holder_scaf nil ))nil ))nil 3477456171 ("" (assert ) nil nil ) nil nil ))nil 3477456171 ("" (assert ) nil nil )"(total_order?[real])" nil ))nil ))nil 3477456171"" (typepred "q" )"" (typepred "p" )"" (lemma "div_cancel3" ("x" "1" "n0z" "q" "y" "1-1/p" ))"" (assert )"" (flatten)"" (hide -2)"" (split)"1" (replace -1 1)"1" "both_sides_times_pos_ge1" "pz" "q" "x" "1" "y" "1-1/p" ))"1" (assert )"1" (hide 2)"1" "posreal_div_posreal_is_posreal" "px" "1" "py" "p" ))"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"nzreal" nil )"real" reals nil )"real" reals nil )"nzreal" nil )"posreal" nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"posreal" nil )nil real_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_props nil )"real" reals nil )nil real_props nil )nil reals nil )"[numfield, numfield -> numfield]" number_fields nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"[T, T -> boolean]" equalities nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"{a: real | a > 1}" holder_scaf nil )"{a: posreal | 1 / p + 1 / a = 1}" holder_scafnil ))nil ))nil 3477461478"" (skosimp)"" (typepred "f!1" )"" (typepred "g!1" )"" (case "p>1" )"1" (case "q>1" )"1" (typepred "norm[T, S, mu, q](g!1)" )"1" (typepred "norm[T, S, mu, p](f!1)" )"1" (expand ">=" )"1" (expand "<=" -1)"1" (split)"1" (expand "<=" -2)"1" (split)"1" (expand "p_integrable?" )"1" (flatten)"1" rewrite "prod_complex_measurable[T,S]" )"1" "ALPHA" "norm[T, S, mu, p](f!1)" )"1" replace -1)"1" "BETA" "norm[T, S, mu, q](g!1)" )"1" replace -1)"1" "posreal_times_posreal_is_posreal" "px" "ALPHA" "py" "BETA" ))"1" "real_expt_pos" "px" "ALPHA" "a" "p" ))"1" "real_expt_pos" "px" "BETA" "a" "q" ))"1" case "FORALL (x: T): ") "1" "abs(f!1 * g!1) ^ 1=abs(f!1 * g!1)" )"1" "1" expand "norm" )"1" "abs(f!1 * g!1) ^ 1=abs(f!1 * g!1)" )"1" "1" "1" "both_sides_real_expt" "x" "integral.integral(abs(g!1) ^ q) ^ (1 / q)" "y" "BETA" "pa" "q" ))"1" rewrite "real_expt_times" "1" assert )"1" "both_sides_real_expt" "x" "integral.integral(abs(f!1)^p)^(1/p)" "y" "ALPHA" "pa" "p" ))"1" rewrite "real_expt_times" "1" assert )"1" rewrite "real_expt_x1" "1" rewrite "real_expt_x1" "1" "integral.integrable_is_measurable" )"1" "abs(f!1) ^ p" )"1" "abs(g!1) ^ q" )"1" "expt_measurable" "g" "abs(f!1) ^ p" "a" "1/p" ))"1" "expt_measurable" "g" "abs(g!1) ^ q" "a" "1/q" ))"1" "(^[T](abs(g!1) ^ q, 1 / q))=abs(g!1)" )"1" "(^[T](abs(f!1)^p, 1 / p))=abs(f!1)" )"1" "1" case "measurable_function?[T,S](abs(f!1*g!1))" )"1" "scal_measurable" "c" "1/(ALPHA * BETA)" "g" "abs(f!1 * g!1)" ))"1" "1" "integral.integrable_scal" "c" "(1/p)*(1/ALPHA ^ p)" "f" "abs(f!1) ^ p" ))"1" "integral.integrable_scal" "c" "(1/q)*(1/BETA ^ q)" "f" "abs(g!1) ^ q" ))"1" "integral.integrable_add" "f1" "*[T]((1 / p) * (1 / ALPHA ^ p), abs(f!1) ^ p)" "f2" "*[T]((1 / q) * (1 / BETA ^ q), abs(g!1) ^ q)" ))"1" "1" "integral_ae_abs" "h" "*[T](1 / (ALPHA * BETA), abs(f!1 * g!1))" "f" "(+[T]) ")) "1" "1" "1" "integral.integrable_scal" "c" "ALPHA*BETA" "f" "*[T](1 / (ALPHA * BETA), abs(f!1 * g!1))" ))"1" "(*[T] ") "1" rewrite "real_expt_x1" )"1" "integral.integral_scal" "c" "1/(ALPHA*BETA)" "f" "abs(f!1*g!1)" ))"1" replace "1" "integral_nonneg" "f" "abs(f!1*g!1)" ))"1" "1" rewrite "real_props.abs_mult" "1" "posreal_div_posreal_is_posreal" "px" "1" "py" "ALPHA*BETA" ))"1" expand "abs" "1" assert )"1" expand "abs" "1" case "integral(abs((+[T]) ") "1" assert )"1" "div_mult_pos_le1" "z" "integral.integral(abs(f!1 * g!1))" "py" "ALPHA * BETA" "x" "1" ))"1" assert )nil nil ))nil ))nil )"2" "2" "abs((+[T]) A^q))* abs(g!1)^q") "1" "1" "posreal_times_posreal_is_posreal" "px" "1/p" "py" "1/(ALPHA^p)" ))"1" "posreal_times_posreal_is_posreal" "px" "1/q" "py" "1/(BETA^q)" ))"1" "AA" "1 / p * (1 / (ALPHA ^ p))" )"1" "BB" "1 / q * (1 / (BETA ^ q))" )"1" "integral.integral_scal" "c" "AA" "f" "abs(f!1)^p" ))"1" "integral.integral_scal" "c" "BB" "f" "abs(g!1)^q" ))"1" replace "1" replace "1" "integral.integral_add" "f1" "AA * abs(f!1) ^ p" "f2" "BB * abs(g!1) ^ q" ))"1" replace "1" replace "1" replace "1" "1" expand "AA" )"1" expand "BB" )"1" "AP" "ALPHA ^ p" )"1" rewrite "div_cancel1" )"1" "q" )"1" assert )"1" assert )"1" rewrite "one_times" )"1" replace "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "posreal_div_posreal_is_posreal" "px" "1" "py" "BETA^q" ))"2" assert )nil nil ))nil ))nil ))nil )"2" "posreal_div_posreal_is_posreal" "px" "1" "py" "ALPHA^p" ))"2" assert )nil nil ))nil ))nil ))nil )"2" "2" "1" expand "abs" "1" expand "+" "1" expand "*" "1" expand "^" "1" expand "^" "1" expand "^" "1" expand "^" "1" rewrite "div_div2" )"1" rewrite "div_div2" )"1" "abs(f!1(x!1)) ^ p * (1 / ALPHA ^ p) * (1 / p)=(1 / (p * (ALPHA ^ p))) * abs(f!1(x!1)) ^ p" )"1" "abs(g!1(x!1)) ^ q * (1 / BETA ^ q) * (1 / q)=(1 / (q * (BETA ^ q))) * abs(g!1(x!1)) ^ q" )"1" "1" "posreal_times_posreal_is_posreal" "px" "p" "py" "ALPHA^p" ))"1" "posreal_times_posreal_is_posreal" "px" "q" "py" "BETA^q" ))"1" "posreal_div_posreal_is_posreal" "px" "1" "py" "q*BETA^q" ))"1" "posreal_div_posreal_is_posreal" "px" "1" "py" "p*ALPHA^p" ))"1" "AA" "(1 / (p * (ALPHA ^ p)))" )"1" "BB" "(1 / (q * (BETA ^ q)))" )"1" "both_sides_times_pos_le1" "pz" "AA" "x" "0" "y" "abs(f!1(x!1))^p" ))"1" assert )"1" "both_sides_times_pos_le1" "pz" "BB" "x" "0" "y" "abs(g!1(x!1))^q" ))"1" assert )"1" expand "abs" "1" nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil )"2" assert )nil nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "x!1" )"2" "2" expand "+" "2" expand "*" "2" expand "^" "2" expand "^" "2" expand "abs" "2" "posreal_div_posreal_is_posreal" "px" "1/p" "py" "ALPHA^p" ))"2" "posreal_div_posreal_is_posreal" "px" "1/q" "py" "BETA^q" ))"2" "AA" "(1 / p) / (ALPHA ^ p)" )"2" "BB" "(1 / q) / (BETA ^ q)" )"2" "both_sides_times_pos_le1" "pz" "AA" "x" "0" "y" "abs(f!1(x!1))^p" ))"1" "both_sides_times_pos_le1" "pz" "BB" "x" "0" "y" "abs(g!1(x!1))^q" ))"1" assert )nil nil )"2" assert )nil nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "abs" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "complex_abs_mul" nil nil ))nil )"2" "integral_nonneg" "f" "abs(f!1*g!1)" ))"2" assert )"2" "2" expand "abs" )"2" assert )"2" "2" expand "*" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "*" "2" expand "abs" "2" assert )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" "2" expand "member" )"2" expand "*" "2" expand "abs" "2" expand "+" "2" expand "^" "2" expand "^" "2" "x!1" )"2" "abs(f!1(x!1) * g!1(x!1))" )"2" "both_sides_div_pos_ge1" "pz" "ALPHA*BETA" "x" "abs(f!1(x!1) * g!1(x!1))" "y" "0" ))"2" assert )"2" "1 / (ALPHA * BETA) * (abs(f!1(x!1)) * abs(g!1(x!1)))=abs(f!1(x!1)) * abs(g!1(x!1)) / (ALPHA * BETA)" )"1" "1" expand "abs" "1" "LHS" "abs(f!1(x!1)) * abs(g!1(x!1)) / (ALPHA * BETA)" )"1" expand "abs" "1" assert )nil nil ))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 ))nil ))nil ))nil ))nil )"2" "2" rewrite "complex_abs_mul" nil nil ))nil )"3" nil nil ))nil ))nil )"2" nil nil )"3" nil nil ))nil ))nil ))nil ))nil )"2" rewrite "complex_abs_mul" nil nil ))nil )"2" "2" "prod_measurable[T,S]" "g1" "abs(f!1)" "g2" "abs(g!1)" ))"1" "(*[T](abs(f!1), abs(g!1)))=abs(f!1 * g!1)" )"1" nil nil ))nil )"2" nil nil )"3" nil nil ))nil ))nil ))nil ))nil )"2" "1" "1" expand "^" )"1" expand "abs" )"1" rewrite "real_expt_times" "1" rewrite "real_expt_x1" )nil nil ))nil ))nil ))nil ))nil )"2" "posreal_div_posreal_is_posreal" "px" "1" "py" "p" ))"2" assert )nil nil ))nil ))nil )"3" "posreal_div_posreal_is_posreal" "px" "1" "py" "p" ))"3" assert )nil nil ))nil ))nil )"2" "2" "posreal_div_posreal_is_posreal" "px" "1" "py" "q" ))"2" "2" expand "abs" )"2" expand "^" )"2" rewrite "real_expt_times" "2" rewrite "real_expt_x1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "nn_measurable?" )"2" assert )"2" "2" "2" expand "^" )"2" expand "abs" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "nn_measurable?" )"2" assert )"2" "2" "2" expand "^" )"2" expand "abs" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "posreal_div_posreal_is_posreal" "px" "1" "py" "p" ))"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "integral_nonneg" "f" "^[T](abs[T](f!1), p)" ))"2" assert )"2" "2" expand "^" "2" expand "abs" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "integral_nonneg" "f" "^[T](abs[T](g!1), q)" ))"2" assert )"2" "2" "2" expand "^" )"2" expand "abs" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "^" "2" rewrite "real_expt_x1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "^" )"2" rewrite "real_expt_x1" )nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" "q" )"2" "2" "youngs_inequality" "p" "p" "q" "q" "a" "abs(f!1(x!1))/ALPHA" "b" "abs(g!1(x!1))/BETA" ))"1" replace "1" rewrite "abs_mult" "1" "abs(f!1(x!1))" )"1" "abs(g!1(x!1))" )"1" "FX" "abs(f!1(x!1))" )"1" "GX" "abs(g!1(x!1))" )"1" rewrite "div_times" )"1" "LHS" "(FX * GX) / (ALPHA * BETA)" )"1" rewrite "div_real_expt" "1" rewrite "div_real_expt" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil )"3" assert )nil nil )"4" rewrite "div_mult_pos_ge1" "4" assert )nil nil ))nil )"5" assert )nil nil )"6" rewrite "div_mult_pos_ge1" "6" assert )nil nil ))nil )"7" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" assert )nil nil ))nil )"4" "4" assert )nil nil ))nil )"5" "5" assert )nil nil ))nil )"6" "6" assert )nil nil ))nil )"7" "7" assert )nil nil ))nil )"8" "8" assert )nil nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (replace -1 * rl)"2" (rewrite "zero_times2" )"2" "norm_eq_0[T, S, mu, q]" "f" "g!1" ))"2" "2" "1" "1" case "cal_N?[T, S, mu](f!1*g!1)" )"1" "cal_N_is_p_integrable[T, S, mu, 1]" )"1" "f!1 * g!1" )"1" replace -1)"1" "norm_eq_0[T,S,mu,1]" "f" "f!1*g!1" ))"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" expand "p_integrable?" )"2" "2" "2" expand "cal_N?" )"2" expand "ae_0?" )"2" expand "pointwise_ae?" )"2" expand "ae?" )"2" expand "fullset" )"2" expand "ae_in?" )"2" "2" "2" expand "member" )"2" rewrite "prod_complex_measurable[T,S]" )"2" "2" "E!1" )"2" "2" "x!1" )"2" expand "*" )"2" assert )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (replace -1 * rl)"2" (rewrite "zero_times1" )"2" "norm_eq_0[T, S, mu, p]" "f" "f!1" ))"2" (flatten)"2" "2" "1" case "cal_N?[T,S,mu](f!1*g!1)" )"1" "cal_N_is_p_integrable[T, S, mu, 1]" )"1" "f!1 * g!1" )"1" replace -1)"1" "norm_eq_0[T,S,mu,1]" "f" "f!1*g!1" ))"1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" "2" expand "cal_N?" )"2" "2" expand "p_integrable?" )"2" "2" "prod_complex_measurable[T,S]" "g1" "f!1" "g2" "g!1" ))"1" replace -1)"1" "1" expand "ae_0?" )"1" expand "pointwise_ae?" )"1" expand "ae?" )"1" expand "fullset" )"1" expand "ae_in?" )"1" "1" "E!1" )"1" "1" "x!1" )"1" expand "member" )"1" assert )"1" expand "*" )"1" assert )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil )"2" (hide-all-but (-1 1))"2" (typepred "q" )"2" "div_cancel3" ("x" "1" "n0z" "q" "y" "1-1/p" ))"2" (flatten)"2" (hide -2)"2" (split)"1" (replace -1 1)"1" (hide -1)"1" "both_sides_times_pos_gt1" "pz" "q" "x" "1" "y" "1-1/p" ))"1" "posreal_div_posreal_is_posreal" "px" "1" "py" "p" ))"1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )nil p_integrable_def nil )"bool" p_integrable_def nil )"{a: real | a > 1}" holder_scaf nil )"bool" reals nil )"measure_type[T, S]" holder_scaf nil )nil generalized_measure_def"measure_integration/" )"bool" generalized_measure_def"measure_integration/" )nil extended_nnreal"extended_nnreal/" )nil real_types nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )"sigma_algebra[T]" holder_scaf nil )nil subset_algebra_def"measure_integration/" )"bool" subset_algebra_def"measure_integration/" )nil sets nil )nil defined_types nil )nil complex_types "complex_alt/" )nil holder_scaf nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil real_props nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_props nil )"nnreal" p_integrable_def nil )"(total_order?[real])" nil )nil real_types nil )"(strict_total_order?[real])" real_props nil )nil real_props nil )"nnreal" nil )nil real_props nil )nil real_expt "power/" )nil young nil )"[T -> complex]" complex_fun_ops "complex_alt/" )"[T -> nonneg_real]" complex_fun_ops"complex_alt/" )"[T -> nnreal]" real_fun_power "power/" )"posreal" nil )nil real_expt "power/" )"bool" integral "measure_integration/" )nil integral"measure_integration/" )"real" integral "measure_integration/" )"(strict_total_order?[real])" real_props nil )nil polar "complex_alt/" )nil complex_fun_ops "complex_alt/" )nil real_expt "power/" )nil integral"measure_integration/" )"bool" measure_space_def"measure_integration/" )"(total_order?[real])" nil )nil real_types nil )"nzreal" real_typesnil )"[T -> nonneg_real]" real_fun_ops "reals/" )nil real_props nil )nil reals nil )nil integral "measure_integration/" )"nzreal" holder_scaf nil )nil reals nil )nil real_props nil )nil extra_tegies nil )"nzreal" holder_scaf nil )"p_integrable[T, S, mu, q]" holder_scaf nil )"nnreal" holder_scaf nil )"p_integrable[T, S, mu, p]" holder_scaf nil )"nnreal" holder_scaf nil )nil real_props nil )nil real_props nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"{y: posreal | y >= x}" nil )nil real_props nil )nil integral "measure_integration/" )nil integral "measure_integration/" )"bool" measure_theory "measure_integration/" )"(S)" holder_scaf nil )"measurable_set[T, S]" nil )"bool" measure_theory "measure_integration/" )"bool" measure_theory "measure_integration/" )"bool" sets nil )"bool" booleans nil )nil real_props 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)" holder_scaf nil )"null_set[T, S, mu]" holder_scaf nil )"set" sets nil )"bool" measure_theory"measure_integration/" )"[T -> real]" real_fun_ops "reals/" )nil integral "measure_integration/" )"[T -> real]" real_fun_ops "reals/" )nil integral "measure_integration/" )nil integral "measure_integration/" )"nzreal" nil )"[T -> real]" real_fun_ops "reals/" )nil measure_space_def"measure_integration/" )nil measure_space_def"measure_integration/" )nil measure_space"measure_integration/" )AND const-decl "[bool, bool -> bool]" booleans nil )nil measure_space"measure_integration/" )"bool" measure_space"measure_integration/" )nil measure_space"measure_integration/" )"posreal" nil )"nzreal" nil )"real" reals nil )nil real_expt "power/" )"nnreal" real_expt "power/" )OR const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )"complex" complex_types "complex_alt/" )"nnreal" polar "complex_alt/" )"real" reals nil )"real" reals nil )"nnreal" nil )nil real_expt "power/" )nil complex_measurable nil )"bool" complex_measurable nil )nil complex_measurablenil )nil real_props nil )"bool" complex_measure_theory nil )"real" reals nil )nil complex_types "complex_alt/" )nil complex_types "complex_alt/" )nil complex_types "complex_alt/" )nil complex_types "complex_alt/" )nil complex_types "complex_alt/" )"bool" complex_measure_theory nil )nil p_integrable_def nil )nil complex_measure_theory nil )"bool" complex_measure_theory nil )nil p_integrable_def nil )nil real_props nil )"bool" reals nil )nil real_types nil )nil real_types nil )"[T, T -> boolean]" equalities nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"{a: posreal | 1 / p + 1 / a = 1}" holder_scafnil ))nil 3477456171"" (skosimp)"" (lemma "holder_aux" ("f" "f!1" "g" "g!1" ))"" (flatten) nil nil )) nil ))nil )"{a: posreal | 1 / p + 1 / a = 1}" holder_scafnil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )nil real_types nil )nil real_types nil )nil p_integrable_def nil )"bool" p_integrable_def nil )"{a: real | a > 1}" holder_scaf nil )"bool" reals nil )"measure_type[T, S]" holder_scaf nil )nil generalized_measure_def"measure_integration/" )"bool" generalized_measure_def"measure_integration/" )nil extended_nnreal"extended_nnreal/" )nil real_types nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )"sigma_algebra[T]" holder_scaf nil )nil subset_algebra_def"measure_integration/" )"bool" subset_algebra_def"measure_integration/" )nil sets nil )nil defined_types nil )nil booleans nil )nil booleans nil )nil complex_types "complex_alt/" )nil holder_scaf nil )nil holder_scaf nil ))nil ))nil 3477456171"" (skosimp)"" (lemma "holder_aux" ("f" "f!1" "g" "g!1" ))"" (flatten)"" (hide -2)"" (expand "*" )"" (expand "*" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"{a: posreal | 1 / p + 1 / a = 1}" holder_scafnil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )nil real_types nil )nil real_types nil )nil p_integrable_def nil )"bool" p_integrable_def nil )"{a: real | a > 1}" holder_scaf nil )"bool" reals nil )"measure_type[T, S]" holder_scaf nil )nil generalized_measure_def"measure_integration/" )"bool" generalized_measure_def"measure_integration/" )nil extended_nnreal"extended_nnreal/" )nil real_types nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )"sigma_algebra[T]" holder_scaf nil )nil subset_algebra_def"measure_integration/" )"bool" subset_algebra_def"measure_integration/" )nil sets nil )nil defined_types nil )nil booleans nil )nil booleans nil )nil complex_types "complex_alt/" )nil holder_scaf nil )nil holder_scaf nil )"real" reals nil )"complex" complex_types "complex_alt/" )"[T -> complex]" complex_fun_ops "complex_alt/" ))nil ))nil 3452581063"" (skosimp)"" (lemma "holder_aux" ("f" "f!1" "g" "g!1" ))"" (flatten) nil nil )) nil ))nil )"{a: posreal | 1 / p + 1 / a = 1}" holder_scafnil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )nil real_types nil )nil real_types nil )nil p_integrable_def nil )"bool" p_integrable_def nil )"{a: real | a > 1}" holder_scaf nil )"bool" reals nil )"measure_type[T, S]" holder_scaf nil )nil generalized_measure_def"measure_integration/" )"bool" generalized_measure_def"measure_integration/" )nil extended_nnreal"extended_nnreal/" )nil real_types nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )"sigma_algebra[T]" holder_scaf nil )nil subset_algebra_def"measure_integration/" )"bool" subset_algebra_def"measure_integration/" )nil sets nil )nil defined_types nil )nil booleans nil )nil booleans nil )nil complex_types "complex_alt/" )nil holder_scaf nil )nil holder_scaf nil ))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Dauer der Verarbeitung: 0.136 Sekunden
(vorverarbeitet am 2026-04-30)
¤ *© Formatika GbR, Deutschland
2026-05-26
