| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/complex_integration/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 172 kB |
|
Quelle minkowski_scaf.prfSprache: Lisp |
|||||||||||||||
|
(minkowski_scaf (mu_TCC1 0 (mu_TCC1-1 nil 3477582206 ("" (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 minkowski_scaf 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]" minkowski_scaf nil)) nil)) (minkowski_scaf 0 (minkowski_scaf-1 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" (case "integrable?(+[T](abs[T](f!1)^p,abs[T](g!1)^p))") (("1" (lemma "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" (split -1) (("1" (name "q" "p/(p-1)") (("1" (case "q>1 & 1/p+1/q =1") (("1" (flatten -1) (("1" (hide -8 -9) (("1" (case "abs(f!1 + g!1) ^ p=(abs(f!1 + g!1) ^(p-1))^q") (("1" (name "H" "abs(f!1 + g!1) ^ (p - 1)") (("1" (replace -1) (("1" (name "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" (lemma "holder_scaf[T,S,mu,p,p / (p - 1)]" ("f" "f!1" "g" "CH")) (("1" (lemma "holder_scaf[T,S,mu,p,p / (p - 1)]" ("f" "g!1" "g" "CH")) (("1" (replace -3) (("1" (case "forall (f:p_integrable[T,S,mu,1]): integral.integrable?(abs(f)) & norm[T, S, mu, 1 (("1" (inst-cp - "f!1*CH") (("1" (inst - "g!1*CH") (("1" (flatten -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]( (("1" (name "RHS" "norm[T, S, mu, p](f!1) + norm[T, S, mu, p](g!1)") (("1" (replace -1) (("1" (expand "norm" -1) (("1" (replace -1) (("1" (hide -1) (("1" (hide -3 -4 -5 -6 -19 -20) (("1" (case "abs(f!1 + g!1)*H = abs(f!1 + g!1) ^ p") (("1" (lemma "integral_ae_le" ("f1" "abs(f!1+g!1)*H" "f2" "abs(f!1 * CH) + abs(g!1 * CH)")) (("1" (name-replace "INT" "integral.integral(abs(f!1 * CH) + abs(g!1 * CH))") (("1" (split -1) (("1" (replace -2) (("1" (expand "norm" -3) (("1" (lemma "integral_nonneg" ("f" "abs(f!1 + g!1) ^ p")) (("1" (split -1) (("1" (name-replace "INT2" "integral.integral(abs(f!1 + g!1) ^ p)") (("1" (hide-all-but (-1 -2 -4 -11 -12 -13 -14 1)) (("1" (lemma "real_expt_times" ("x" "INT2" "a" "1/p" "b" "p/q")) (("1" (case-replace "1 / p * (p / q)=1/q") (("1" (replace -2 -5 rl) (("1" (case "INT2 <= RHS * INT2 ^ (1 / q)") (("1" (hide -2 -3 -5 -6) (("1" (expand ">=" -2) (("1" (expand "<=" -2) (("1" (split -2) (("1" (lemma "posreal_div_posreal_is_posreal" ("px" "1" "py" "p")) (("1" (lemma "posreal_div_posreal_is_posreal" ("px" "1" "py" "q")) (("1" (lemma "real_expt_plus" ("x" "INT2" "a" "1/p" "b" "1/q")) (("1" (replace -7) (("1" (rewrite "real_expt_x1" -1) (("1" (lemma "real_expt_pos" ("px" "INT2" "a" "1/q")) (("1" (lemma "both_sides_times_pos_le1" ("pz" "INT2 ^ (1 / q)" "x" "INT2 ^ (1 / p)" "y" "RHS")) (("1" (replace -3 * rl) (("1" (assert) nil nil)) nil) ("2" (propax) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1 * rl) (("2" (rewrite "real_expt_0x" 1) (("1" (expand "RHS") (("1" (assert) nil nil)) nil) ("2" (lemma "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" (propax) nil nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (expand "^" 1) (("2" (expand "abs" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 -12 -9 -10 -11 -7 -6 -8)) (("2" (expand "ae_le?") (("2" (expand "pointwise_ae?") (("2" (expand "ae?") (("2" (expand "fullset") (("2" (expand "ae_in?") (("2" (inst + "emptyset") (("2" (skosimp) (("2" (expand "member") (("2" (hide 1) (("2" (expand "*" 1) (("2" (expand "+" 1 2) (("2" (expand "abs" 1) (("2" (expand "+" 1) (("2" (replace -1 1 rl) (("2" (hide -1 -3) (("2" (replace -1 1 rl) (("2" (hide -1) (("2" (simplify 1) (("2" (expand "^" 1) (("2" (expand "abs" 1 2) (("2" (expand "+" 1 2) (("2" (expand "abs" 1 4) (("2" (expand "abs" 1 6) (("2" (expand "+ " 1 3) (("2" (expand "+ " 1 5) (("2" (rewrite "abs_mult" 1) (("2" (rewrite "abs_mult" 1) (("2" (typepred "abs(f!1(x!1) + g!1(x!1)) ^ (p - 1)") (("2" (name-replace "FGp1" "abs(f!1(x!1) + g!1(x!1)) ^ (p - 1)") (("2" (expand "abs" 1 3) (("2" (expand "abs" 1 4) (("2" (expand "sq_abs") (("2" (expand "Im" 1) (("2" (expand "Re" 1) (("2" (rewrite "sq_0") (("2" (lemma "sqrt_sq") (("2" (inst - "FGp1") (("2" (split) (("1" (replace -1) (("1" (hide -1) (("1" (expand ">=" -1) (("1" (expand "<=" -1) (("1" (split -1) (("1" (lemma "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) (("1" (hide -1 -2) (("1" (rewrite "abs_triangle") nil nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (replace -1 * rl) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (propax) nil nil)) nil)) nil) ("2" (apply-extensionality :hide? t) (("2" (hide 2) (("2" (expand "*" 1) (("2" (replace -6 1 rl) (("2" (expand "^" 1) (("2" (typepred "abs(f!1 + g!1)(x!1)") (("2" (name-replace "ABS" "abs(f!1 + g!1)(x!1)") (("2" (hide-all-but (-1 1 -12)) (("2" (lemma "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" 1) (("2" (assert) nil nil)) nil) ("3" (rewrite "integral.integrable_add" 1) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp) (("2" (typepred "f!2") (("2" (expand "p_integrable?") (("2" (flatten) (("2" (expand "norm") (("2" (case-replace "abs(f!2) ^ 1=abs(f!2)") (("1" (replace -3) (("1" (rewrite "real_expt_x1") (("1" (lemma "integral_nonneg" ("f" "abs(f!2)")) (("1" (assert) (("1" (skosimp) (("1" (expand "abs") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (apply-extensionality :hide? t) (("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 -9) (("2" (assert) nil nil)) nil)) nil) ("2" (replace -8) (("2" (assert) nil nil)) nil) ("3" (assert) nil nil)) nil) ("2" (hide 2) (("2" (expand "norm") (("2" (case-replace "abs(CH) ^ (p / (p - 1))=abs(f!1 + g!1) ^ p") (("1" (lemma "integral_nonneg" ("f" "abs(f!1 + g!1) ^ p")) (("1" (split) (("1" (name-replace "INT" "integral.integral(abs(f!1 + g!1) ^ p)") (("1" (case-replace "(1 / (p / (p - 1)))=1/q") (("1" (hide -1) (("1" (rewrite "real_expt_times" 1 :dir rl) (("1" (rewrite "div_times" 1) nil nil)) nil)) nil) ("2" (hide -2 2) (("2" (cross-mult 1) (("2" (replace -8 1 rl) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp) (("2" (expand "^") (("2" (expand "abs") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -4 1) (("2" (replace -7 1) (("2" (case-replace "abs(CH)=H") (("2" (hide-all-but 1) (("2" (apply-extensionality :hide? t) (("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 -7) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (lemma "posreal_div_posreal_is_posreal" ("px" "p" "py" "q")) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil) ("4" (propax) nil nil) ("5" (propax) nil nil)) nil) ("2" (hide 2) (("2" (expand "p_integrable?" +) (("2" (split) (("1" (expand "complex_measurable?" 1) (("1" (replace -1 1 rl) (("1" (expand "Re" 1) (("1" (expand "Im" 1) (("1" (assert) (("1" (split) (("1" (expand "H") (("1" (expand "^" 1) (("1" (expand "abs" 1) (("1" (expand "+" 1) (("1" (lemma "expt_measurable" ("g" "abs(f!1 + g!1)" "a" "p-1")) (("1" (expand "^" -1) (("1" (expand "abs" -1) (("1" (expand "+" -1) (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (expand "nn_measurable?" 1) (("2" (split) (("1" (assert) (("1" (hide-all-but 1) (("1" (typepred "f!1") (("1" (typepred "g!1") (("1" (expand "p_integrable?") (("1" (flatten) (("1" (lemma "sum_complex_measurable" ("g1" "f!1" "g2" "g!1")) (("1" (lemma "abs_complex_measurable" ("g" "(+[T])(f!1, g!1)")) (("1" (propax) 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" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "measure_space.const_measurable" 1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -6 1) (("2" (case-replace "abs(CH) ^ q=abs(f!1 + g!1) ^ p") (("1" (replace -3) (("1" (hide-all-but 1) (("1" (case-replace "abs(CH)=H") (("1" (hide 2) (("1" (apply-extensionality :hide? t) (("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" (hide-all-but (-1 -2 -3 -4 1)) (("2" (apply-extensionality :hide? t) (("2" (expand "^") (("2" (expand "abs") (("2" (typepred "abs((f!1 + g!1)(x!1))") (("2" (name-replace "FG" "abs((f!1 + g!1)(x!1))") (("2" (rewrite "real_expt_times" + :dir rl) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (assert) nil nil) ("4" (assert) nil nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 -2 1)) (("2" (case-replace "q>1") (("1" (rewrite "div_cancel3" -2) (("1" (lemma "div_cancel3" ("n0z" "p" "x" "1" "y" "1-1/q")) (("1" (flatten) (("1" (hide -1) (("1" (split -1) (("1" (assert) nil nil) ("2" (hide 2) (("2" (assert) (("2" (lemma "div_cancel3" ("n0z" "q" "x" "p" "y" "p-1")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "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" (hide-all-but 1) (("3" (flatten) (("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" (inst-cp - "f!1") (("1" (inst-cp - "g!1") (("1" (inst - "f!1+g!1") (("1" (typepred "f!1") (("1" (typepred "g!1") (("1" (expand "p_integrable?") (("1" (flatten) (("1" (replace -8 * rl) (("1" (replace -5) (("1" (replace -6) (("1" (replace -7) (("1" (rewrite "real_expt_x1" +) (("1" (rewrite "real_expt_x1" 1) (("1" (rewrite "real_expt_x1" 1) (("1" (rewrite "integral.integral_add" 1 :dir rl) (("1" (lemma "integral_ae_le" ("f1" "abs(f!1 + g!1)" "f2" "abs(f!1) + abs(g!1)")) (("1" (split) (("1" (propax) nil nil) ("2" (hide-all-but 1) (("2" (expand "ae_le?") (("2" (expand "pointwise_ae?") (("2" (expand "ae?") (("2" (expand "fullset") (("2" (expand "ae_in?") (("2" (inst + "emptyset") (("2" (skosimp) (("2" (expand "member") (("2" (hide 1) (("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" (hide-all-but (1 -2)) (("2" (lemma "integral_nonneg" ("f" "abs[T](g!1)")) (("2" (assert) (("2" (skosimp) (("2" (expand "abs") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 -4)) (("2" (lemma "integral_nonneg" ("f" "abs[T](f!1)")) (("2" (assert) (("2" (skosimp) (("2" (expand "abs") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-10 1)) (("2" (lemma "integral_nonneg" ("f" "abs(f!1 + g!1)")) (("2" (split) (("1" (propax) nil nil) ("2" (skosimp) (("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" (hide-all-but 1) (("2" (skosimp) (("2" (apply-extensionality :hide? t) (("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" (typepred "g!1") (("1" (expand "p_integrable?") (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (typepred "f!1") (("2" (expand "p_integrable?") (("2" (flatten) (("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" (inst - "x!1") (("2" (hide -1) (("2" (expand "+ " -1) (("2" (expand "abs" -1) (("2" (flatten) (("2" (case "abs(f!1(x!1) + g!1(x!1)) <= 2 * KK(x!1)") (("1" (hide -2 -3) (("1" (case "KK(x!1)^p <= abs(f!1(x!1)) ^ p + abs(g!1(x!1)) ^ p") (("1" (lemma "real_expt_pos" ("px" "2" "a" "p")) (("1" (lemma "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 :dir rl) (("1" (name-replace "RHS" "2 ^ p * abs(f!1(x!1)) ^ p + 2 ^ p * abs(g!1(x!1)) ^ p") (("1" (lemma "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" (propax) nil nil)) nil)) nil) ("2" (expand "KK") (("2" (hide-all-but 1) (("2" (expand "max") (("2" (expand "abs" 1 1) (("2" (expand "abs" 1 2) (("2" (expand "max") (("2" (case-replace "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" (lemma "sum_complex_measurable" ("g1" "f!1" "g2" "g!1")) (("1" (lemma "abs_complex_measurable" ("g" "f!1+g!1")) (("1" (rewrite "expt_measurable") (("1" (expand "nn_measurable?") (("1" (hide-all-but 1) (("1" (skosimp) (("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" (lemma "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" (name-replace "FF" "((+[T])(abs[T](f!1) ^ p, abs[T](g!1) ^ p))") (("1" (lemma "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" (skosimp) (("2" (hide-all-but 1) (("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" (prop) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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) (p formal-const-decl "{x: real | x >= 1}" minkowski_scaf nil) (mu formal-const-decl "measure_type[T, S]" minkowski_scaf 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) (S formal-const-decl "sigma_algebra[T]" minkowski_scaf 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) (abs const-decl "[T -> nonneg_real]" complex_fun_ops "complex_alt/") (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (complex type-decl nil complex_types "complex_alt/") (max const-decl "[T -> real]" real_fun_ops_aux "reals/") (= const-decl "[T, T -> boolean]" equalities 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) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (T formal-type-decl nil minkowski_scaf nil) (nonneg_real_max application-judgement "{z: nonneg_real | z >= x AND z >= y}" real_defs nil) (integrable? const-decl "bool" integral "measure_integration/") (+ const-decl "[T -> real]" real_fun_ops "reals/") (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (^ const-decl "[T -> nnreal]" real_fun_power "power/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nn_integrable_is_nn_integrable formula-decl nil integral "measure_integration/") (FF skolem-const-decl "[T -> real]" minkowski_scaf nil) (nn_integrable_scal judgement-tcc nil nn_integral "measure_integration/") (both_sides_times_pos_ge1 formula-decl nil real_props nil) (nn_integrable_is_integrable judgement-tcc nil integral "measure_integration/") (integral_nn formula-decl nil integral "measure_integration/") (norm const-decl "nnreal" p_integrable_def nil) (real_plus_real_is_real application-judgement "real" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (q skolem-const-decl "real" minkowski_scaf nil) (complex_? adt-recognizer-decl "[complex -> boolean]" complex_types "complex_alt/") (complex_ adt-constructor-decl "[[real, real] -> (complex_?)]" complex_types "complex_alt/") (Im const-decl "[T -> real]" complex_fun_ops "complex_alt/") (sum_complex_measurable judgement-tcc nil complex_measurable nil) (complex_measurable nonempty-type-eq-decl nil complex_measurable nil) (Im_fun_add1 formula-decl nil complex_fun_ops "complex_alt/") (Re_fun_add1 formula-decl nil complex_fun_ops "complex_alt/") (abs_complex_measurable judgement-tcc nil complex_measurable nil) (nn_measurable nonempty-type-eq-decl nil measure_space "measure_integration/") (nn_measurable? const-decl "bool" measure_space "measure_integration/") (expt_measurable judgement-tcc nil measure_space "measure_integration/") (H skolem-const-decl "[T -> nnreal]" minkowski_scaf nil) (const_measurable formula-decl nil measure_space "measure_integration/") (Re const-decl "[T -> real]" complex_fun_ops "complex_alt/") (complex_measurable? const-decl "bool" complex_measurable nil) (integrable nonempty-type-eq-decl nil integral "measure_integration/") (integral const-decl "real" integral "measure_integration/") (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (complex_abs_mul formula-decl nil complex_fun_ops "complex_alt/") (integral_ae_le formula-decl nil integral "measure_integration/") (real_expt_pos formula-decl nil real_expt "power/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (both_sides_times_pos_le1 formula-decl nil real_props nil) (real_expt_x1 formula-decl nil real_expt "power/") (real_expt_plus formula-decl nil real_expt "power/") (posreal_div_posreal_is_posreal judgement-tcc nil real_types nil) (real_expt_0x formula-decl nil real_expt "power/") (RHS skolem-const-decl "nnreal" minkowski_scaf nil) (real_expt_times formula-decl nil real_expt "power/") (integral_nonneg formula-decl nil integral "measure_integration/") (ae_le? const-decl "bool" measure_theory "measure_integration/") (subset_algebra_fullset name-judgement "(S)" minkowski_scaf nil) (measurable_fullset name-judgement "measurable_set[T, S]" minkowski_scaf nil) (ae? const-decl "bool" measure_theory "measure_integration/") (ae_in? const-decl "bool" measure_theory "measure_integration/") (Im const-decl "real" complex_types "complex_alt/") (sq_0 formula-decl nil sq "reals/") (abs_triangle formula-decl nil polar "complex_alt/") (sqrt_sq formula-decl nil sqrt "reals/") (Re const-decl "real" complex_types "complex_alt/") (sq_abs const-decl "nnreal" complex_types "complex_alt/") (abs_mult formula-decl nil polar "complex_alt/") (TRUE const-decl "bool" booleans nil) (abs const-decl "nnreal" polar "complex_alt/") (+ const-decl "complex" complex_types "complex_alt/") (member const-decl "bool" sets 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/") (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/") (finite_emptyset name-judgement "finite_set[T]" step_fun_props "analysis/") (subset_algebra_emptyset name-judgement "(S)" minkowski_scaf nil) (null_emptyset name-judgement "null_set[T, S, mu]" minkowski_scaf nil) (fullset const-decl "set" sets nil) (pointwise_ae? const-decl "bool" measure_theory "measure_integration/") (integral_add formula-decl nil integral "measure_integration/") (integrable_add judgement-tcc nil integral "measure_integration/") (* const-decl "[T -> complex]" complex_fun_ops "complex_alt/") (complex_measurable_def formula-decl nil complex_measurable nil) (holder_scaf formula-decl nil holder_scaf nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (CH skolem-const-decl "[T -> (complex_?)]" minkowski_scaf nil) (Re_rew formula-decl nil complex_types "complex_alt/") (Im_rew formula-decl nil complex_types "complex_alt/") (div_cancel4 formula-decl nil real_props nil) (times_div2 formula-decl nil real_props nil) (times_div1 formula-decl nil real_props nil) (div_cancel3 formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (div_times formula-decl nil real_props nil) (div_mult_pos_gt1 formula-decl nil extra_real_props nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (div_simp formula-decl nil real_props nil) (f!1 skolem-const-decl "p_integrable[T, S, mu, p]" minkowski_scaf nil) (g!1 skolem-const-decl "p_integrable[T, S, mu, p]" minkowski_scaf nil) (NOT const-decl "[bool -> bool]" booleans nil) (mult_real_expt formula-decl nil real_expt "power/") (both_sides_real_expt_le formula-decl nil real_expt "power/") (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (< const-decl "bool" reals nil) (KK skolem-const-decl "[T -> real]" minkowski_scaf nil) (measurable_function nonempty-type-eq-decl nil measure_space_def "measure_integration/") (measurable_function? const-decl "bool" measure_space_def "measure_integration/") (^ const-decl "nnreal" real_expt "power/") (OR const-decl "[bool, bool -> bool]" booleans nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (nn_integrable nonempty-type-eq-decl nil nn_integral "measure_integration/") (nn_integrable? const-decl "bool" nn_integral "measure_integration/") (nn_integrable_le formula-decl nil nn_integral "measure_integration/") (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (real_times_real_is_real application-judgement "real" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (+ const-decl "[T -> complex]" complex_fun_ops "complex_alt/") (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil)) shostak)))
¤ Dauer der Verarbeitung: 0.84 Sekunden (vorverarbeitet am 2026-04-28) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26