| 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 208 kB |
|
Quelle holder_scaf.prf Sprache: Lisp |
|||||||||
|
(holder_scaf
(mu_TCC1 0 (mu_TCC1-1 nil 3477456171 ("" (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 holder_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]" holder_scaf nil)) nil)) (q_TCC1 0 (q_TCC1-1 nil 3477456171 ("" (assert) nil nil) nil nil)) (f_TCC1 0 (f_TCC1-1 nil 3477456171 ("" (assert) nil nil) ((real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (g_TCC1 0 (g_TCC1-1 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" (lemma "both_sides_times_pos_ge1" ("pz" "q" "x" "1" "y" "1-1/p")) (("1" (assert) (("1" (hide 2) (("1" (lemma "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_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (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) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (posreal_div_posreal_is_posreal judgement-tcc nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (both_sides_times_pos_ge1 formula-decl nil real_props nil) (real_minus_real_is_real application-judgement "real" reals nil) (div_cancel3 formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans 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) (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, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" 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) (p formal-const-decl "{a: real | a > 1}" holder_scaf nil) (q formal-const-decl "{a: posreal | 1 / p + 1 / a = 1}" holder_scaf nil)) nil)) (holder_aux 0 (holder_aux-1 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" (name "ALPHA" "norm[T, S, mu, p](f!1)") (("1" (replace -1) (("1" (name "BETA" "norm[T, S, mu, q](g!1)") (("1" (replace -1) (("1" (lemma "posreal_times_posreal_is_posreal" ("px" "ALPHA" "py" "BETA")) (("1" (lemma "real_expt_pos" ("px" "ALPHA" "a" "p")) (("1" (lemma "real_expt_pos" ("px" "BETA" "a" "q")) (("1" (case "FORALL (x: T): abs(f!1(x) * g!1(x)) / (ALPHA * BETA) <= (1 / p) * (abs(f!1(x)) ^ p / (ALPHA ^ p)) + (1 / q) * (abs(g!1(x)) ^ q / (BETA ^ q))") (("1" (case-replace "abs(f!1 * g!1) ^ 1=abs(f!1 * g!1)") (("1" (hide -1) (("1" (expand "norm") (("1" (case-replace "abs(f!1 * g!1) ^ 1=abs(f!1 * g!1)") (("1" (hide -1) (("1" (hide -11 -13) (("1" (lemma "both_sides_real_expt" ("x" "integral.integral(abs(g!1) ^ q) ^ (1 / q)" "y" "BETA" "pa" "q")) (("1" (rewrite "real_expt_times" -1 :dir rl) (("1" (assert) (("1" (lemma "both_sides_real_expt" ("x" "integral.integral(abs(f!1)^p)^(1/p)" "y" "ALPHA" "pa" "p")) (("1" (rewrite "real_expt_times" -1 :dir rl) (("1" (assert) (("1" (rewrite "real_expt_x1" -1) (("1" (rewrite "real_expt_x1" -2) (("1" (lemma "integral.integrable_is_measurable") (("1" (inst-cp - "abs(f!1) ^ p") (("1" (inst - "abs(g!1) ^ q") (("1" (lemma "expt_measurable" ("g" "abs(f!1) ^ p" "a" "1/p")) (("1" (lemma "expt_measurable" ("g" "abs(g!1) ^ q" "a" "1/q")) (("1" (case-replace "(^[T](abs(g!1) ^ q, 1 / q))=abs(g!1)") (("1" (case-replace "(^[T](abs(f!1)^p, 1 / p))=abs(f!1)") (("1" (hide -1 -2 -5 -6) (("1" (case "measurable_function?[T,S](abs(f!1*g!1))") (("1" (lemma "scal_measurable" ("c" "1/(ALPHA * BETA)" "g" "abs(f!1 * g!1)")) (("1" (hide -2 -3 -4) (("1" (lemma "integral.integrable_scal" ("c" "(1/p)*(1/ALPHA ^ p)" "f" "abs(f!1) ^ p")) (("1" (lemma "integral.integrable_scal" ("c" "(1/q)*(1/BETA ^ q)" "f" "abs(g!1) ^ q")) (("1" (lemma "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" (hide -2 -3) (("1" (lemma "integral_ae_abs" ("h" "*[T](1 / (ALPHA * BETA), abs(f!1 * g!1))" "f" "(+[T]) (*[T]((1 / p) * (1 / ALPHA ^ p), abs(f!1) ^ p), *[T]((1 / q) * (1 / BETA ^ q), abs(g!1) ^ q))")) (("1" (split -1) (("1" (flatten -1) (("1" (lemma "integral.integrable_scal" ("c" "ALPHA*BETA" "f" "*[T](1 / (ALPHA * BETA), abs(f!1 * g!1))")) (("1" (case-replace "(*[T] (ALPHA * BETA, *[T](1 / (ALPHA * BETA), abs(f!1 * g!1))))=abs(f!1 * g!1)") (("1" (rewrite "real_expt_x1") (("1" (lemma "integral.integral_scal" ("c" "1/(ALPHA*BETA)" "f" "abs(f!1*g!1)")) (("1" (replace -1) (("1" (lemma "integral_nonneg" ("f" "abs(f!1*g!1)")) (("1" (split -1) (("1" (rewrite "real_props.abs_mult" -6) (("1" (lemma "posreal_div_posreal_is_posreal" ("px" "1" "py" "ALPHA*BETA")) (("1" (expand "abs" -7 1) (("1" (assert) (("1" (expand "abs" -7 1) (("1" (case "integral(abs((+[T]) (*[T]((1 / p) * (1 / ALPHA ^ p), abs(f!1) ^ p), *[T]((1 / q) * (1 / BETA ^ q), abs(g!1) ^ q)))) <=1") (("1" (assert) (("1" (lemma "div_mult_pos_le1" ("z" "integral.integral(abs(f!1 * g!1))" "py" "ALPHA * BETA" "x" "1")) (("1" (assert) nil nil)) nil)) nil) ("2" (hide 2 -1 -2 -3 -4 -5 -6 -7) (("2" (case-replace "abs((+[T]) (*[T]((1 / p) * (1 / ALPHA ^ p), abs(f!1) ^ p), *[T]((1 / q) * (1 / BETA ^ q), abs(g!1) ^ q)))= ((1/p)*1/(ALPHA^p))* abs(f!1)^p + ((1/q)*1/(BET (("1" (hide -1) (("1" (lemma "posreal_times_posreal_is_posreal" ("px" "1/p" "py" "1/(ALPHA^p)")) (("1" (lemma "posreal_times_posreal_is_posreal" ("px" "1/q" "py" "1/(BETA^q)")) (("1" (name-replace "AA" "1 / p * (1 / (ALPHA ^ p))") (("1" (name-replace "BB" "1 / q * (1 / (BETA ^ q))") (("1" (lemma "integral.integral_scal" ("c" "AA" "f" "abs(f!1)^p")) (("1" (lemma "integral.integral_scal" ("c" "BB" "f" "abs(g!1)^q")) (("1" (replace -7) (("1" (replace -8) (("1" (lemma "integral.integral_add" ("f1" "AA * abs(f!1) ^ p" "f2" "BB * abs(g!1) ^ q")) (("1" (replace -2) (("1" (replace -3) (("1" (replace -1) (("1" (hide -1 -2 -3 -20 -21 -8 -9 -6 -7 -14 -15 -10) (("1" (expand "AA") (("1" (expand "BB") (("1" (name-replace "AP" "ALPHA ^ p") (("1" (rewrite "div_cancel1") (("1" (typepred "q") (("1" (assert) (("1" (assert) (("1" (rewrite "one_times") (("1" (replace -3) (("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" (lemma "posreal_div_posreal_is_posreal" ("px" "1" "py" "BETA^q")) (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (lemma "posreal_div_posreal_is_posreal" ("px" "1" "py" "ALPHA^p")) (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (apply-extensionality :hide? t) (("1" (expand "abs" +) (("1" (expand "+" +) (("1" (expand "*" +) (("1" (expand "^" 1 1) (("1" (expand "^" 1 1) (("1" (expand "^" 1 6) --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.30 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28