| products/sources/formale sprachen/PVS/measure_integration/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: finite_fubini_tonelli.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(finite_fubini_tonelli
(mu_TCC1 0 (mu_TCC1-1 nil 3458551591 ("" (typepred "S1") (("" (expand "sigma_algebra?") (("" (expand "subset_algebra_empty?") (("" (flatten) (("" (expand "member") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ((member const-decl "bool" sets nil) (subset_algebra_empty? const-decl "bool" subset_algebra_def nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (T1 formal-type-decl nil finite_fubini_tonelli nil) (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets nil) (sigma_algebra? const-decl "bool" subset_algebra_def nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil) (S1 formal-const-decl "sigma_algebra[T1]" finite_fubini_tonelli nil)) nil)) (nu_TCC1 0 (nu_TCC1-1 nil 3458551591 ("" (typepred "S2") (("" (expand "sigma_algebra?") (("" (expand "subset_algebra_empty?") (("" (flatten) (("" (expand "member") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ((member const-decl "bool" sets nil) (subset_algebra_empty? const-decl "bool" subset_algebra_def nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (T2 formal-type-decl nil finite_fubini_tonelli nil) (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets nil) (sigma_algebra? const-decl "bool" subset_algebra_def nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil) (S2 formal-const-decl "sigma_algebra[T2]" finite_fubini_tonelli nil)) nil)) (finite_fubini_tonelli_1 0 (finite_fubini_tonelli_1-1 nil 3458552933 ("" (skosimp) (("" (split) (("1" (flatten) (("1" (typepred "h!1") (("1" (expand "nn_measurable?") (("1" (flatten) (("1" (lemma "nn_integrable_is_nn_integrable" ("f" "h!1")) (("1" (split) (("1" (hide -4) (("1" (lemma "nn_integral_def" ("f" "h!1")) (("1" (skolem - "HH") (("1" (flatten) (("1" (typepred "HH") (("1" (case "FORALL (n: nat): isf?(HH(n))") (("1" (case "FORALL (n: nat,z:[T1,T2]): HH(n)(z)>=0") (("1" (name "FF" "lambda (n:nat): lambda (x:T1): isf_integral(lambda (y:T2): HH(n)(x,y))") (("1" (case "FORALL (n: nat): integrable?[T1, S1, to_measure(mu)](FF(n))") (("1" (case "forall (n:nat): integral[T1,S1,to_measure(mu)](FF(n))=integral[[T1,T2],sigma_ti (("1" (case-replace "(isf_integral o HH)=integral o FF") (("1" (case "forall (n:nat,x:T1): FF(n)(x)>=0") (("1" (case "pointwise_increasing?(FF)") (("1" (case "bounded?(integral o FF)") (("1" (lemma "monotone_convergence[T1, S1, to_measure(mu)]" ("F" "FF")) (("1" (split -1) (("1" (flatten) (("1" (hide -1) (("1" (split -1) (("1" (skolem - "F") (("1" (inst - "F") (("1" (assert) (("1" (typepred "F") (("1" (expand "integrable1?") (("1" (expand "ae_convergence?") (("1" (expand "fullset") (("1" (expand "ae_convergence_in?") (("1" (expand "ae_in?") (("1" (skosimp) (("1" (expand "member") (("1" (typepred "E!1") (("1" (expand "negligible_set?") (("1" (skolem - "N1") (("1" (flatten) (("1" (inst + "N1" "F") (("1" (skosimp) (("1" (expand "subset?") (("1" (inst - "x!1") (("1" (expand "member") (("1" (inst - "x!1") (("1" (assert) (("1" (lemma "monotone_convergence_scaf[T2,S2,to_measure(nu)]" ("f" "LAMBDA (y: T2): h!1(x!1, y)" "F" "lambda (n:nat): lambda (y:T2): HH(n)(x!1,y)")) (("1" (split -1) (("1" (flatten) (("1" (replace -1) (("1" (name-replace "LHS" "integral(LAMBDA (y: T2): h!1(x!1, y))") (("1" (case-replace "(integral o (LAMBDA (n: nat): LAMBDA (y: T2): HH(n)(x!1, y)))=LAMBDA (n:nat): FF(n)(x!1)") (("1" (expand "converges_upto?") (("1" (flatten) (("1" (hide-all-but (-3 -7 3)) (("1" (lemma "hausdorff_convergence.unique_limit" ("u" "LAMBDA (n: nat): FF(n)(x!1)" "l1" "LHS" "l2" "F(x!1)")) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (apply-extensionality :hide? t) (("1" (expand "FF" 1) (("1" (expand "o" 1) (("1" (inst -15 "x!2") (("1" (lemma "isf_x_section" ("x" "x!1" "i" "HH(x!2)")) (("1" (rewrite "isf_integral" 1) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (inst -15 "n!1") (("2" (lemma "isf_x_section" ("x" "x!1" "i" "HH(n!1)")) (("2" (lemma "isf_is_integrable[T2, S2, to_measure(nu)]") (("2" (inst - "LAMBDA (y: T2): HH(n!1)(x!1, y)") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 -14 -15)) (("2" (expand "increasing_nn_isf?") (("2" (expand "pointwise_converges_upto?") (("2" (split) (("1" (expand "pointwise_convergence?") (("1" (skolem + "y!1") (("1" (inst - "(x!1,y!1)") nil nil)) nil)) nil) ("2" (expand "pointwise_increasing?") (("2" (skolem + "y!1") (("2" (inst - "(x!1,y!1)") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (replace -8 -5 rl) (("3" (hide-all-but (-7 1 -13 -12 -8 -3 -6)) (("3" (expand "FF") (("3" (expand "o ") (("3" (expand "pointwise_increasing?") (("3" (inst -2 "x!1") (("3" (hide -4) (("3" (expand "bounded?") (("3" (split) (("1" (expand "bounded_above?") (("1" (inst + "F(x!1)") (("1" (skolem + "n!1") (("1" (inst-cp -5 "n!1") (("1" (lemma "isf_x_section" ("i" "HH(n!1)" "x" "x!1")) (("1" (rewrite "isf_integral") (("1" (rewrite "metric_convergence_def") (("1" (expand "metric_converges_to") (("1" (inst - "isf_integral(LAMBDA (y: T2): HH(n!1)(x!1, y))-F(x!1)") (("1" (skosimp) (("1" (inst - "n!1+n!2") (("1" (assert) (("1" (expand "ball") (("1" (expand "increasing?") (("1" (inst -3 "n!1" "n!1+n!2") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (skosimp) (("2" (rewrite "isf_x_section") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "bounded_below?") (("2" (inst + "0") (("2" (skolem + "n!1") (("2" (inst -5 "n!1") (("2" (lemma "isf_x_section" ("i" "HH(n!1)" "x" "x!1")) (("2" (rewrite "isf_integral" 1) (("2" (inst -4 "n!1" "x!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (inst -13 "n!1") (("2" (lemma "isf_x_section" ("i" "HH(n!1)" "x" "x!1")) (("2" (lemma "isf_is_integrable[T2, S2, to_measure(nu)]") (("2" (inst - "LAMBDA (y: T2): HH(n!1)(x!1, y)") 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" (hide-all-but (-2 1 -7)) (("2" (expand "bounded?") (("2" (skosimp) (("2" (split) (("1" (expand "bounded_above?") (("1" (inst + "c!1") (("1" (skolem + "n!1") (("1" (inst - "n!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "bounded_below?") (("2" (inst + "-c!1") (("2" (skolem + "n!1") (("2" (inst - "n!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 -2)) (("2" (expand "ae_increasing?") (("2" (inst + "emptyset") (("2" (skosimp) (("2" (expand "pointwise_increasing?") (("2" (inst - "x!1") (("2" (expand "increasing?") (("2" (propax) --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.32 Sekunden (vorverarbeitet) ¤ |
Haftungshinweis
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.
Bemerkung:Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
