| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/measure_integration/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 734 kB |
|
Quelle integral_convergence.prfSprache: Lisp |
|||||||||||||||
|
(integral_convergence (monotone_convergence 0 (monotone_convergence-1 nil 3409506492 ("" (skosimp*) (("" (case-replace "(EXISTS f: ae_convergence?(F!1, f)) IFF bounded?(integral o F!1)") (("1" (assert) (("1" (skolem!) (("1" (flatten) (("1" (hide -2) (("1" (split -1) (("1" (expand "ae_increasing?") (("1" (expand "ae_convergence?") (("1" (expand "fullset") (("1" (expand "ae_convergence_in?") (("1" (expand "ae_in?") (("1" (skolem - "E1") (("1" (skolem - "E2") (("1" (typepred "union(E1,E2)") (("1" (expand "negligible_set?") (("1" (skosimp) (("1" (lemma "null_set_is_measurable") (("1" (inst - "X!1") (("1" (lemma "monotone_convergence_scaf" ("f" "phi(complement(X!1))*f!1" "F" "lambda n: phi(complement(X!1))*F!1(n)")) (("1" (case-replace "integral o (LAMBDA n: phi(complement(X!1)) * F!1(n))=integral o F!1") (("1" (hide -1) (("1" (replace -5) (("1" (case-replace "integral(phi(complement(X!1)) * f!1)=integral(f!1)") (("1" (split -2) (("1" (flatten) nil nil) ("2" (hide 2) (("2" (expand "pointwise_converges_upto?") (("2" (case-replace "pointwise_increasing?(LAMBDA n: phi(complement(X!1)) * F!1(n))") (("1" (expand "pointwise_convergence?") (("1" (skosimp) (("1" (inst -8 "x!1") (("1" (expand "complement") (("1" (expand "member") (("1" (expand "phi") (("1" (expand "member") (("1" (hide -1 -2) (("1" (expand "subset?") (("1" (expand "union") (("1" (expand "member") (("1" (inst - "x!1") (("1" (expand "*" 1) (("1" (case-replace "E2(x!1)") (("1" (assert) (("1" (hide-all-but 1) (("1" (expand "convergence?") (("1" (skosimp) (("1" (inst + "0") (("1" (skosimp) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (case-replace "X!1(x!1)") (("1" (hide-all-but 2) (("1" (expand "convergence?") (("1" (skosimp) (("1" (inst + "0") (("1" (skosimp) (("1" (assert) nil 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) ("2" (hide 2) (("2" (hide -1 -5 -7) (("2" (expand "pointwise_increasing?") (("2" (skosimp) (("2" (expand "*") (("2" (expand "complement") (("2" (expand "phi") (("2" (expand "member") (("2" (inst - "x!1") (("2" (expand "subset?") (("2" (expand "union") (("2" (expand "member") (("2" (inst - "x!1") (("2" (case-replace "X!1(x!1)") (("1" (expand "increasing?") (("1" (propax) nil nil)) nil) ("2" (assert) (("2" (expand "increasing?") (("2" (skosimp) (("2" (assert) (("2" (inst - "x!2" "y!1") (("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)) nil) ("2" (hide -1 2) (("2" (lemma "integral_ae_eq" ("f" "f!1" "h" "phi(complement(X!1)) * f!1")) (("1" (split -1) (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (expand "ae_eq?") (("2" (expand "restrict") (("2" (expand "pointwise_ae?") (("2" (expand "*") (("2" (expand "complement") (("2" (expand "phi") (("2" (expand "member") (("2" (expand "ae?") (("2" (expand "fullset") (("2" (expand "ae_in?") (("2" (inst + "X!1") (("1" (skosimp) (("1" (assert) nil nil)) nil) ("2" (expand "negligible_set?") (("2" (inst + "X!1") (("2" (assert) (("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (rewrite "integrable_is_measurable") (("2" (hide 2) (("2" (rewrite "indefinite_integrable") (("2" (hide 2) (("2" (rewrite "measurable_complement") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (rewrite "indefinite_integrable") (("3" (rewrite "measurable_complement") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 2) (("2" (expand "o ") (("2" (apply-extensionality :hide? t) (("1" (lemma "integral_ae_eq" ("f" "F!1(x!1)" "h" "phi(complement(X!1)) * F!1(x!1)")) (("1" (split -1) (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (expand "ae_eq?") (("2" (expand "restrict") (("2" (expand "pointwise_ae?") (("2" (expand "*" 1) (("2" (expand "complement") (("2" (expand "phi") (("2" (expand "member") (("2" (expand "ae?") (("2" (expand "fullset") (("2" (expand "ae_in?") (("2" (inst + "X!1") (("1" (skosimp) (("1" (assert) nil nil)) nil) ("2" (expand "negligible_set?") (("2" (inst + "X!1") (("2" (assert) (("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (rewrite "integrable_is_measurable") (("2" (rewrite "indefinite_integrable") (("2" (rewrite "measurable_complement") nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (rewrite "indefinite_integrable") (("2" (rewrite "measurable_complement") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (rewrite "indefinite_integrable") (("2" (rewrite "measurable_complement") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst + "f!1") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (split) (("1" (skosimp*) (("1" (expand "bounded?") (("1" (split) (("1" (expand "bounded_above?") (("1" (inst + "integral(f!1)") (("1" (skolem + ("n!1")) (("1" (expand "o ") (("1" (expand "ae_convergence?") (("1" (expand "ae_increasing?") (("1" (expand "ae_convergence_in?") (("1" (expand "fullset") (("1" (expand "ae_in?") (("1" (skosimp*) (("1" (typepred "union(E!1,E!2)") (("1" (expand "negligible_set?") (("1" (skosimp) (("1" (lemma "integral_ae_le" ("f1" "phi(complement(X!1))*F!1(n!1)" "f2" "phi(complement(X!1))*f!1")) (("1" (split -1) (("1" (lemma "integral_ae_eq" ("f" "f!1" "h" "phi(complement(X!1)) * f!1")) (("1" (split -1) (("1" (flatten) (("1" (replace -2 * rl) (("1" (lemma "integral_ae_eq" ("f" "F!1(n!1)" "h" "phi(complement(X!1)) * F!1(n!1)")) (("1" (split -1) (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (hide-all-but (-4 -5 1)) (("2" (expand "ae_eq?") (("2" (expand "restrict") (("2" (expand "pointwise_ae?") (("2" (expand "ae?") (("2" (expand "*") (("2" (expand "complement") (("2" (expand "phi") (("2" (expand "member") (("2" (expand "fullset") (("2" (expand "ae_in?") (("2" (inst + "X!1") (("1" (skosimp) (("1" (assert) nil nil)) nil) ("2" (rewrite "null_is_negligible") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "integrable_is_measurable") nil nil)) nil)) nil)) nil) ("2" (hide -1 -4 -5 2) (("2" (expand "ae_eq?") (("2" (expand "restrict") (("2" (expand "pointwise_ae?") (("2" (expand "complement") (("2" (expand "phi") (("2" (expand "member") (("2" (expand "ae?") (("2" (expand "fullset") (("2" (expand "ae_in?") (("2" (inst + "X!1") (("1" (skosimp) (("1" (assert) (("1" (expand "*") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (rewrite "null_is_negligible") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "integrable_is_measurable") nil nil)) nil) ("2" (hide 2) (("2" (expand "ae_le?") (("2" (expand "*") (("2" (expand "pointwise_ae?") (("2" (expand "complement") (("2" (expand "phi") (("2" (expand "member") (("2" (expand "ae?") (("2" (expand "fullset") (("2" (expand "ae_in?") (("2" (inst + "X!1") (("1" (skosimp) (("1" (assert) (("1" (expand "union") (("1" (expand "subset?") (("1" (expand "member") (("1" (inst - "x!1") (("1" (inst - "x!1") (("1" (inst - "x!1") (("1" (case-replace "E!1(x!1)") (("1" (case-replace "E!2(x!1)") (("1" (assert) (("1" (hide 1 2 3 -1 -2) (("1" (rewrite "metric_convergence_def") (("1" (case "F!1(n!1)(x!1)-f!1(x!1)>0") (("1" (expand "metric_converges_to") (("1" (inst - "F!1(n!1)(x!1) - f!1(x!1)") (("1" (hide 1) (("1" (skosimp) (("1" (inst - "n!1+n!2") (("1" (assert) (("1" (inst - "n!1" "n!1+n!2") (("1" (expand "ball") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "null_is_negligible") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "indefinite_integrable") (("2" (rewrite "measurable_complement") (("2" (expand "null_set?") (("2" (propax) nil nil)) nil)) nil)) nil) ("3" (rewrite "indefinite_integrable") (("3" (rewrite "measurable_complement") (("3" (expand "null_set?") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "bounded_below?") (("2" (inst + "integral(F!1(0))") (("2" (skolem + ("n!1")) (("2" (expand "o ") (("2" (expand "ae_increasing?") (("2" (skosimp) (("2" (lemma "integral_ae_le" ("f1" "F!1(0)" "f2" "F!1(n!1)")) (("2" (assert) (("2" (hide 2) (("2" (expand "ae_le?") (("2" (expand "pointwise_ae?") (("2" (expand "ae?") (("2" (expand "fullset") (("2" (expand "ae_in?") (("2" (inst + "E!1") (("2" (skosimp) (("2" (inst - "x!1") (("2" (assert) (("2" (inst - "0" "n!1") (("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" (flatten) (("2" (expand "ae_increasing?") (("2" (skosimp) (("2" (typepred "E!1") (("2" (expand "negligible_set?") (("2" (skosimp) (("2" (case "forall (F:sequence[nn_integrable]): bounded?(integral o F)&pointwise_increasing?(F)=>EXISTS (f:nn_integ (("1" (inst - "lambda n: phi(complement(X!1))*(F!1(n)-F!1(0))") (("1" (split -1) (("1" (skosimp) (("1" (typepred "f!1") (("1" (inst + "f!1+phi(complement(X!1)) *F!1(0)") (("1" (expand "ae_convergence?") (("1" (expand "fullset") (("1" (expand "ae_convergence_in?") (("1" (expand "ae_in?") (("1" (skosimp) (("1" (inst + "union(X!1,E!2)") (("1" (skosimp) (("1" (expand "union") (("1" (expand "member") (("1" (flatten) (("1" (expand "+ ") (("1" (expand "*") (("1" (inst - "x!1") (("1" (assert) (("1" (expand "-") (("1" (expand "complement") (("1" (expand "phi") (("1" (expand "member") (("1" (hide-all-but (-2 3)) (("1" (rewrite "metric_convergence_def") (("1" (rewrite "metric_convergence_def") (("1" (expand "metric_converges_to") (("1" (skosimp) (("1" (inst - "r!1") (("1" (skosimp) (("1" (inst + "n!1") (("1" (skosimp) (("1" (inst - "i!1") (("1" (expand "ball") (("1" (expand "member") (("1" (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)) nil)) nil) ("2" (rewrite "negligible_union") (("2" (rewrite "null_is_negligible") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "integrable_add") (("2" (hide 2) (("2" (lemma "integral_ae_eq" ("f" "F!1(0)" "h" "*[T](phi[T, S](complement[T](X!1)), F!1(0))")) (("1" (split -1) (("1" (flatten) nil nil) ("2" (hide 2) (("2" (expand "ae_eq?") (("2" (expand "restrict") (("2" (expand "pointwise_ae?") (("2" (expand "ae?") (("2" (expand "fullset") (("2" (expand "ae_in?") (("2" (inst + "X!1") (("1" (skosimp) (("1" (expand "*") (("1" (expand "complement") (("1" (expand "phi") (("1" (expand "member") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "null_is_negligible") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "phi_is_simple" ("X" "complement[T](X!1)")) (("1" (expand "simple?") (("1" (flatten) (("1" (rewrite "prod_measurable") nil nil)) nil)) nil) ("2" (expand "null_set?") (("2" (flatten) (("2" (lemma "measurable_complement" ("a" "X!1")) (("2" (expand "measurable_set?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "bounded?") (("2" (split) (("1" (flatten) (("1" (expand "bounded_above?") (("1" (skosimp) (("1" (hide -4) (("1" (inst + "a!1-integral(F!1(0))") (("1" (skolem + ("n!1")) (("1" (expand "o") (("1" (inst - "n!1") (("1" (lemma "integral_ae_eq" ("f" "F!1(n!1) - F!1(0)" "h" "phi(complement(X!1)) * (F!1(n!1) - F!1(0))")) (("1" (split -1) (("1" (flatten) (("1" (replace -2 1 rl) (("1" (rewrite "integral_diff") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide -3 2) (("2" (expand "ae_eq?") (("2" (expand "restrict") (("2" (expand "pointwise_ae?") (("2" (expand "ae?") (("2" (expand "fullset") (("2" (expand "ae_in?") (("2" (inst + "X!1") (("1" (skosimp) (("1" (expand "subset?") (("1" (inst - "x!1") (("1" (inst - "x!1") (("1" (expand "complement") (("1" (expand "phi") (("1" (expand "member") (("1" (expand "*") (("1" (expand "-") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "null_is_negligible") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "integrable_diff" ("f1" "F!1(n!1)" "f2" "F!1(0)")) (("2" (lemma "integrable_is_measurable" ("x" "(-[T])(F!1(n!1), F!1(0))")) (("2" (lemma "phi_is_simple" ("X" "complement[T](X!1)")) (("1" (expand "simple?") (("1" (flatten) (("1" (rewrite "prod_measurable") nil nil)) nil)) nil) ("2" (expand "null_set?") (("2" (flatten) (("2" (lemma "measurable_complement" ("a" "X!1")) (("2" (expand "measurable_set?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -3) (("2" (expand "bounded_below?") (("2" (inst + "0") (("2" (skolem + ("n!1")) (("2" (expand "o ") (("2" (lemma "integral_nonneg" ("f" "phi(complement(X!1)) * (F!1(n!1) - F!1(0))")) (("2" (split -1) (("1" (assert) nil nil) ("2" (hide 2) (("2" (skosimp) (("2" (expand "*") (("2" (expand "-") (("2" (inst - "x!1") (("2" (expand "subset?") (("2" (inst - "x!1") (("2" (expand "complement") (("2" (expand "phi") (("2" (expand "member") (("2" (case-replace "X!1(x!1)") (("1" (assert) nil nil) ("2" (assert) (("2" (inst - "0" "n!1") (("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)) nil) ("3" (hide 2) (("3" (expand "pointwise_increasing?") (("3" (skosimp) (("3" (inst - "x!1") (("3" (expand "subset?") (("3" (inst - "x!1") (("3" (expand "member") (("3" (expand "increasing?") (("3" (skolem + ("i!1" "j!1")) (("3" (flatten) (("3" (expand "*") (("3" (expand "-") (("3" (expand "complement") (("3" (expand "phi") (("3" (expand "member") (("3" (case-replace "X!1(x!1)") (("1" (assert) nil nil) ("2" (assert) (("2" (inst - "i!1" "j!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (split) (("1" (skolem + "x!1") (("1" (expand "*") (("1" (expand "complement") (("1" (expand "phi") (("1" (expand "member") (("1" (expand "subset?") (("1" (inst - "x!1") (("1" (expand "member") (("1" (inst - "x!1") (("1" (case-replace "X!1(x!1)") (("1" (assert) nil nil) ("2" (assert) (("2" (expand "-") (("2" (inst - "0" "n!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "integrable_diff" ("f1" "F!1(n!1)" "f2" "F!1(0)")) (("2" (lemma "integral_ae_eq" ("f" "(-[T])(F!1(n!1), F!1(0))" "h" "*[T](phi[T, S](complement[T](X!1)), ((-[T])(F!1(n!1), F!1(0))))")) (("1" (split -1) (("1" (flatten) (("1" (rewrite "nn_integrable_is_nn_integrable") (("1" (hide-all-but (-5 -7 1)) (("1" (skosimp) (("1" (expand "*") (("1" (expand "complement") (("1" (expand "phi") (("1" (expand "member") (("1" (expand "-") (("1" (inst - "x!1") (("1" (expand "subset?") (("1" (inst - "x!1") (("1" (expand "member") (("1" (case-replace "X!1(x!1)") (("1" (assert) nil nil) ("2" (assert) (("2" (inst - "0" "n!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "ae_eq?") (("2" (expand "restrict") (("2" (expand "pointwise_ae?") (("2" (expand "ae?") (("2" (expand "fullset") (("2" (expand "ae_in?") (("2" (inst + "X!1") (("1" (skosimp) (("1" (expand "complement") (("1" (expand "phi") (("1" (expand "member") (("1" (expand "*") (("1" (expand "-") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "null_is_negligible") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "integrable_is_measurable" ("x" "(-[T])(F!1(n!1), F!1(0))")) (("2" (rewrite "prod_measurable") (("2" (lemma "phi_is_simple" ("X" "complement[T](X!1)")) (("1" (rewrite "simple_is_measurable") nil nil) ("2" (expand "null_set?") (("2" (flatten) (("2" (lemma "measurable_complement" ("a" "X!1")) (("2" (expand "measurable_set?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp) (("2" (name "H" "LAMBDA n: LAMBDA (m: nat): {x | F!2(n)(x) >= m+1}") (("2" (name "HH" "LAMBDA (m: nat): IUnion(LAMBDA n: H(n)(m))") (("2" (hide -1 -2) (("2" (case "forall (n,m:nat): measurable_set?(H(n)(m))") (("1" (case "forall (m:nat): measurable_set?(HH(m))") (("1" (lemma "measurable_IIntersection" ("SS" "HH")) (("1" (case "FORALL x: (NOT IIntersection[nat, T](HH)(x)) IFF (EXISTS (k: posnat): FORALL n: F!2(n)(x) < k)") (("1" (case "forall (n,m:nat): mu_fin?(H(n)(m))") (("1" (case "forall (n,m:nat,x:T): ((m+1)*phi(H(n)(m)))(x) <= F!2(n)(x)") (("1" (case "forall (n,m:nat): (m+1)*mu(H(n)(m)) <= nn_integral(F!2(n))") (("1" (expand "bounded?") (("1" (flatten) (("1" (hide -9) (("1" (expand "bounded_above?") (("1" (skolem - "M") (("1" (expand "o ") (("1" (case "forall (n,m:nat): subset?(H(n)(m),HH(m))") (("1" (case "forall (n,m:nat): mu(H(n)(m)) <= M/(1+m)") (("1" (name-replace "DIVERGENT" "IIntersection[nat, T](HH)") (("1" (case "null_set?(DIVERGENT)") (("1" (case "pointwise_bounded?(lambda n: phi(complement(DIVERGENT))*F!2(n))") (("1" (name "SUP" "lambda x: sup(Im(lambda n: (phi(complement(DIVERGENT)) * F!2(n))(x)))") (("1" (case "forall x: least_upper_bound(<=)(SUP(x),Im(LAMBDA n: (phi(complement(DIVERGENT)) * F!2( (("1" (lemma "monotone_convergence_scaf" ("F" "lambda n: phi(complement(DIVERGENT)) * F!2(n)" "f" "SUP")) (("1" (split -1) (("1" (flatten) (("1" (hide -2 -4) (("1" (lemma "nn_integrable_is_nn_integrable" ("f" "SUP")) (("1" (split -1) (("1" (inst + "SUP") (("1" (expand "ae_convergence?") (("1" (expand "fullset") (("1" (expand "ae_convergence_in?") (("1" (expand "ae_in?") (("1" (inst + "DIVERGENT") (("1" (skosimp) (("1" (inst - "x!1") (("1" (expand "*" -3) (("1" (expand "complement") (("1" (expand "phi" -3) (("1" (expand "member") (("1" (hide -4) (("1" (assert) (("1" (replace 1 -3) (("1" (hide-all-but (-3 -15 2)) (("1" (expand "pointwise_increasing?") (("1" (inst - "x!1") (("1" (rewrite "metric_convergence_def") (("1" (expand "metric_converges_to") (("1" (skosimp) (("1" (expand "member") (("1" (expand "ball") (("1" (name-replace "LIMIT" "SUP(x!1)") (("1" (expand "Im") (("1" (expand "least_upper_bound") (("1" (flatten) (("1" (inst - "LIMIT-r!1") (("1" (assert) (("1" (expand "upper_bound") (("1" (skosimp) (("1" (typepred "z!1") (("1" (skolem - "n!1") (("1" (case "z!1>LIMIT-r!1") (("1" (hide 1) (("1" (inst + "n!1") (("1" (skosimp) (("1" (expand "increasing?") (("1" (inst - "n!1" "i!1") (("1" (assert) (("1" (inst - "F!2(i!1)(x!1)") (("1" (expand "abs") (("1" (assert) nil nil)) nil) ("2" (inst + "i!1") (("2" (assert) nil nil)) nil)) nil)) 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)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "null_is_negligible") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-15 1 -2)) (("2" (skosimp) (("2" (expand "pointwise_increasing?") (("2" (inst - "x!1") (("2" (inst - "x!1") (("2" (expand "least_upper_bound") (("2" (flatten) (("2" (hide -2) (("2" (expand "Im") (("2" (expand "upper_bound") (("2" (inst - "(phi(complement(DIVERGENT)) * F!2(0))(x!1)") (("1" (expand "*") (("1" (expand "phi") (("1" (hide -2) (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (inst + "0") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "pointwise_converges_upto?") (("2" (case-replace "pointwise_increasing?(LAMBDA n: phi(complement(DIVERGENT)) * F!2(n))") (("1" (expand "pointwise_convergence?") (("1" (skosimp) (("1" (hide -16) (("1" (expand "pointwise_increasing?") (("1" (inst - "x!1") (("1" (inst - "x!1") (("1" (name-replace "G" "LAMBDA (n_1: nat): (phi(complement(DIVERGENT)) * F!2(n_1))(x!1)") (("1" (name-replace "LIMIT" "SUP(x!1)") (("1" (hide-all-but (-1 -2 1)) (("1" (rewrite "metric_convergence_def") (("1" (expand "metric_converges_to") (("1" (skosimp) (("1" (expand "ball") (("1" (expand "member") (("1" (expand "least_upper_bound") (("1" (flatten) (("1" (inst - "LIMIT-r!1") (("1" (assert) (("1" (expand "upper_bound") (("1" (skosimp) (("1" (typepred "z!1") (("1" (case "z!1>LIMIT-r!1") (("1" (hide 2) (("1" (expand "Im") (("1" (skolem - "n!1") (("1" (inst + "n!1") (("1" (skosimp) (("1" (inst - "G(i!1)") (("1" (expand "abs") (("1" (expand "increasing?") (("1" (inst - "n!1" "i!1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "Im") (("2" (inst + "i!1") nil nil)) nil)) 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)) nil) ("2" (hide-all-but (-15 1)) (("2" (expand "pointwise_increasing?") (("2" (skosimp) (("2" (inst - "x!1") (("2" (expand "increasing?") (("2" (skolem + ("i!1" "j!1")) (("2" (inst - "i!1" "j!1") (("2" (flatten) (("2" (assert) (("2" (expand "*") (("2" (expand "phi") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but (1 -14 -15 -4 -11)) (("3" (expand "bounded?") (("3" (split) (("1" (expand "bounded_above?") (("1" (inst + "M") (("1" (skolem + ("n!1")) (("1" (expand "o ") (("1" (inst - "n!1") (("1" (lemma "integral_ae_eq" ("f" "F!2(n!1)" "h" "phi(complement(DIVERGENT)) * F!2(n!1)")) (("1" (split -1) (("1" (flatten) (("1" (replace -2 * rl) (("1" (propax) nil nil)) nil)) nil) ("2" (hide 2 -4 -3) (("2" (expand "ae_eq?") (("2" (expand "restrict") (("2" (expand "pointwise_ae?") (("2" (expand "ae?") (("2" (expand "fullset") (("2" (expand "ae_in?") (("2" (inst + "DIVERGENT") (("1" (skosimp) (("1" (expand "*") (("1" (expand "complement") (("1" (expand "phi") (("1" (expand "member") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "null_is_negligible") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2 -3 -4) (("2" (lemma "indefinite_integrable" ("E" "complement[T](DIVERGENT)" "f" "F!2(n!1)")) (("1" (rewrite "integrable_is_measurable") nil nil) ("2" (rewrite "measurable_complement") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "bounded_below?") (("2" (inst + "0") (("2" (skolem + ("n!1")) (("2" (expand "o ") (("2" (hide -3 -4) (("2" (lemma "measurable_complement" ("a" "DIVERGENT")) (("1" (lemma "indefinite_integrable" ("E" "complement[T](DIVERGENT)" "f" "F!2(n!1)")) (("1" (lemma "integral_ae_eq" ("f" "F!2(n!1)" "h" "phi(complement[T](DIVERGENT)) * F!2(n!1)")) (("1" (split -1) (("1" (flatten) (("1" (replace -2 * rl) (("1" (lemma "integral_nonneg" ("f" "F!2(n!1)")) (("1" (split -1) (("1" (assert) nil nil) ("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2 -1) (("2" (expand "ae_eq?") (("2" (expand "restrict") (("2" (expand "pointwise_ae?") (("2" (expand "ae?") (("2" (expand "fullset") (("2" (expand "ae_in?") (("2" (inst + "DIVERGENT") (("1" (skosimp) (("1" (expand "*") (("1" (expand "complement") (("1" (expand "phi") (("1" (expand "member") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "null_is_negligible") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "integrable_is_measurable") nil nil)) nil) ("2" (propax) nil nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (rewrite "indefinite_integrable" 1) (("2" (rewrite "measurable_complement") nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (replace -1 1 rl) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 -1 -13 -8)) (("2" (skosimp) (("2" (expand "pointwise_bounded?") (("2" (expand "pointwise?") (("2" (inst - "x!1") (("2" (expand "bounded_seq?") (("2" (expand "fullset") (("2" (expand "image") (("2" (expand "Im") (("2" (expand "bounded?") (("2" (skosimp) (("2" (expand "subset?") (("2" (expand "member") (("2" (expand "above_bounded") (("2" (inst + "x!2+r!1") (("2" (expand "upper_bound") (("2" (skosimp) (("2" (typepred "z!1") (("2" (skosimp) (("2" (inst - "z!1") (("2" (split -2) (("1" (hide-all-but (-1 1)) (("1" (expand "ball") (("1" (grind) nil nil)) nil)) nil) ("2" (inst + "x!3") 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 (-7 -12 1)) (("2" (expand "pointwise_bounded?") (("2" (expand "pointwise_increasing?") (("2" (expand "pointwise?") (("2" (skosimp) (("2" (inst - "x!1") (("2" (inst - "x!1") (("2" (expand "*") (("2" (expand "complement") (("2" (expand "phi") (("2" (expand "member") (("2" (case-replace "DIVERGENT(x!1)") (("1" (expand "bounded_seq?") (("1" (expand "fullset") (("1" (expand "image") (("1" (expand "bounded?") (("1" (inst + "0" "1") (("1" (expand "subset?") (("1" (expand "member") (("1" (expand "ball") (("1" (expand "abs") (("1" (hide-all-but 1) (("1" (skosimp) (("1" (skosimp) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (skosimp) (("2" (expand "bounded_seq?") (("2" (expand "fullset") (("2" (expand "image") (("2" (expand "bounded?") (("2" (inst + "0" "k!1") (("2" (expand "subset?") (("2" (expand "member") (("2" (skosimp*) (("2" (replace -1) (("2" (hide -1) (("2" (expand "ball") (("2" (inst - "x!3") (("2" (hide -2 1) (("2" (grind) 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" (hide 2) (("2" (expand "null_set?") (("2" (assert) (("2" (case "FORALL (n, m,k: nat): n<=k=>subset?(H(n)(m), H(k)(m))") (("1" (hide -4 -5) (("1" (lemma "m_decreasing_convergence" ("E" "HH")) (("1" (case-replace "decreasing?(HH)") (("1" (case-replace "mu_fin?[T, S, m](HH(0))") (("1" (expand "x_converges?" -3) (("1" (expand "o" -3) (("1" (case-replace "(FORALL (i:nat): m(HH(i))`1)") (("1" (hide -9) (("1" (expand "DIVERGENT") (("1" (case-replace "m(IIntersection(HH))`1") (("1" (expand "mu_fin?") (("1" (assert) (("1" (name-replace "mH" "lambda n: m(HH(n))`2") (("1" (lemma "bounded_below_is_convergent" ("u" "mH")) (("1" (split -1) (("1" (case-replace "convergent(mH)") (("1" (case "forall n: mH(n) <= M / (1 + n)") (("1" (expand "mu" 1) (("1" (replace -8) (("1" (hide -4 -8 -13) (("1" (rewrite "limit_def" 1) (("1" (expand "convergent_downto?") (("1" (expand "converges_downto?") (("1" (skosimp) (("1" (hide-all-but (-1 -4 1)) (("1" (expand "convergence") (("1" (skosimp) (("1" (inst-cp - "0") (("1" (expand "mH" -2) (("1" (case "0<=M") (("1" (hide -3) (("1" (expand "<=" -1) (("1" (split -1) (("1" (lemma "posreal_div_posreal_is_posreal" ("px" "epsilon!1" "py" "M")) (("1" (lemma "archimedean" ("px" "epsilon!1 / M")) (("1" (skosimp) (("1" (inst - "n!1-1") (("1" (inst + "n!1-1") (("1" (assert) (("1" (skosimp) (("1" (expand "decreasing?") (("1" (inst - "n!1-1" "i!1") (("1" (assert) (("1" (expand "abs") (("1" (assert) (("1" (rewrite "div_mult_pos_lt2" -1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil) ("2" (replace -1 * rl) (("2" (inst + "0") (("2" (skosimp) (("2" (expand "mH") (("2" (expand "abs") (("2" (assert) (("2" (inst - "i!1") (("2" (typepred "m(HH(i!1))`2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2 -3 -7 -12) (("2" (skosimp) (("2" (expand "convergent_downto?") (("2" (skosimp) (("2" (rewrite "converges_downto_def" -2) (("2" (flatten) (("2" (inst -9 "_" "n!1") (("2" (name-replace "RHS" "M / (1 + n!1)") (("2" (hide -15 -14) (("2" (lemma "m_increasing_convergence" ("E" "lambda n: H(n)(n!1)")) (("1" (case-replace "increasing?(LAMBDA n: H(n)(n!1))") (("1" (expand "o ") (("1" (expand "x_converges?") (("1" (inst -13 "_" "n!1") (("1" (replace -13) (("1" (case-replace "convergent(LAMBDA i: m(H(i)(n!1))`2)") (("1" (flatten) (("1" (expand "mH") (("1" (expand "HH") (("1" (replace -4) (("1" (name-replace "UU" "LAMBDA (i:nat): m(H(i)(n!1))`2") (("1" (case "increasing?(UU)") (("1" (case "forall n: UU(n)<=RHS") (("1" (hide-all-but (-1 -2 -3 1)) (("1" (lemma "increasing_bounded_convergence" ("v1" "UU")) (("1" (split) (("1" (rewrite "limit_def" -1 :dir rl) (("1" (replace -1) (("1" (hide -1 -4) (("1" (rewrite "supfun_is_sup2") nil nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil) ("2" (hide 2 -3) (("2" (expand "bounded_above?") (("2" (inst + "RHS") nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (expand "UU") (("2" (inst -14 "n!2") (("2" (expand "mu") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2 -1) (("2" (expand "increasing?") (("2" (skosimp) (("2" (expand "UU") (("2" (inst - "x!2" "y!1") (("2" (assert) (("2" (inst-cp -17 "x!2" "n!1") (("2" (inst -17 "y!1" "n!1") (("2" (inst -15 "y!1") (("2" (lemma "m_monotone" ("a" "H(x!2)(n!1)" "b" "H(y!1)(n!1)")) (("1" (assert) (("1" (expand "x_le") (("1" (propax) nil nil)) nil)) nil) ("2" (propax) nil nil) ("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (inst -17 "i!1" "n!1") (("2" (expand "measurable_set?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "bounded_above_is_convergent" ("u" "LAMBDA n: m(H(n)(n!1))`2")) (("1" (split -1) (("1" (hide-all-but (-1 1)) (("1" (expand "convergent_upto?") (("1" (expand "converges_upto?") (("1" (skosimp) (("1" (rewrite "metric_convergence_def") (("1" (hide -2) (("1" (expand "metric_converges_to") (("1" (expand "ball") (("1" (assert) (("1" (expand "convergent?") (("1" (expand "convergence") (("1" (inst + "x!2") (("1" (skosimp) (("1" (inst - "epsilon!1") (("1" (skosimp) (("1" (inst + "n!2") (("1" (skosimp) (("1" (inst - "i!1") (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 -11)) (("2" (expand "bounded_above?") (("2" (inst + "RHS") (("2" (skosimp) (("2" (inst - "x!2") (("2" (expand "mu") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but (-11 -13 -15 1 -1)) (("3" (expand "increasing?") (("3" (skolem + ("i!1" "j!1")) (("3" (flatten) (("3" (inst - "i!1" "j!1") (("3" (assert) (("3" (inst-cp - "i!1" "n!1") (("3" (inst - "j!1" "n!1") (("3" (lemma "m_monotone" ("a" "H(i!1)(n!1)" "b" "H(j!1)(n!1)")) (("1" (assert) (("1" (expand "x_le") (("1" (inst -4 "j!1") nil nil)) nil)) nil) ("2" (propax) nil nil) ("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (inst -15 "n!2" "n!1") (("2" (expand "measurable_set?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (inst -15 "i!1" "n!1") (("3" (expand "measurable_set?") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-9 1)) (("2" (expand "increasing?") (("2" (skosimp) (("2" (inst - "x!2" "n!1" "y!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (inst -13 "n!2" "n!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (expand "convergent_downto?") (("2" (skosimp) (("2" (expand "converges_downto?") (("2" (flatten) (("2" (rewrite "metric_convergence_def") (("2" (expand "metric_converges_to") (("2" (assert) (("2" (expand "ball") (("2" (hide -2) (("2" (expand "convergent?") (("2" (expand "convergence") (("2" (inst + "x!1") (("2" (skosimp) (("2" (inst - "epsilon!1") (("2" (skosimp) (("2" (inst + "n!1") (("2" (skosimp) (("2" (inst - "i!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "bounded_below?") (("2" (inst + "0") (("2" (skosimp) (("2" (expand "mH") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide -5 2) (("3" (expand "decreasing?") (("3" (skolem + ("i!1" "j!1")) (("3" (inst - "i!1" "j!1") (("3" (assert) (("3" (flatten) (("3" (assert) (("3" (hide-all-but (-3 -5 -11 1)) (("3" (inst-cp - "i!1") (("3" (inst - "j!1") (("3" (inst-cp - "i!1") (("3" (inst - "j!1") (("3" (lemma "m_monotone" ("a" "HH(j!1)" "b" "HH(i!1)")) (("1" (assert) (("1" (expand "x_le") (("1" (expand "mH") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (propax) nil nil) ("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (inst -11 "n!1") (("2" (expand "measurable_set?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2 -4) (("2" (expand "mu_fin?") (("2" (lemma "m_monotone" ("a" "IIntersection(HH)" "b" "HH(0)")) (("1" (split -1) (("1" (expand "x_le") (("1" (assert) nil nil)) nil) ("2" (hide-all-but 1) (("2" (expand "subset?") (("2" (expand "IIntersection") (("2" (expand "member") (("2" (skosimp) (("2" (inst - "0") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst -9 "0") nil nil) ("3" (propax) nil nil)) nil)) nil)) nil) ("3" (expand "measurable_set?") (("3" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (expand "decreasing?") (("2" (inst - "0" "i!1") (("2" (assert) (("2" (lemma "m_monotone" ("a" "HH(i!1)" "b" "HH(0)")) (("1" (assert) (("1" (hide-all-but (-1 -2 1)) (("1" (expand "mu_fin?") (("1" (expand "x_le") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (inst -10 "i!1") nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (inst -10 "i!1") (("3" (expand "measurable_set?") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (hide -1 -2 -5) (("2" (expand "HH") (("2" (inst - "_" "0") (("2" (inst - "_" "0") (("2" (inst - "_" "0") (("2" (assert) (("2" (lemma "m_increasing_convergence" ("E" "LAMBDA n: H(n)(0)")) (("1" (case-replace "increasing?(LAMBDA n: H(n)(0))") (("1" (expand "o" -2) (("1" (expand "x_converges?") (("1" (expand "mu_fin?" (-5 1)) (("1" (replace 1 -2) (("1" (replace -5) (("1" (prop) (("1" (hide 2) (("1" (name-replace "mH" "LAMBDA n: m(H(n)(0))`2") (("1" (case "increasing?(mH)") (("1" (case "forall n: mH(n)<=M") (("1" (hide-all-but (-1 -2 1)) (("1" (lemma "bounded_above_is_convergent" ("u" "mH")) (("1" (assert) (("1" (split -1) (("1" (expand "convergent_upto?") (("1" (skosimp) (("1" (expand "converges_upto?") (("1" (rewrite "metric_convergence_def") (("1" (expand "metric_converges_to") (("1" (expand "ball") (("1" (expand "member") (("1" (assert) (("1" (hide -2 -3 -4) (("1" (expand "convergent?") (("1" (expand "convergence") (("1" (inst + "x!1") (("1" (skosimp) (("1" (inst - "epsilon!1") (("1" (skosimp) (("1" (inst + " n!1") (("1" (skosimp) (("1" (inst - "i!1") (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "bounded_above?") (("2" (inst + "M") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (inst -4 "n!1") (("2" (expand "mu") (("2" (expand "mH") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2 -10 -9 -5 -2 -3 -6 -7) (("2" (expand "increasing?") (("2" (skolem + ("i!1" "j!1")) (("2" (flatten) (("2" (inst - "i!1" "j!1") (("2" (assert) (("2" (expand "mH") (("2" (inst-cp - "i!1") (("2" (inst - "j!1") (("2" (inst-cp - "i!1") (("2" (inst - "j!1") (("2" (lemma "m_monotone" ("a" "H(i!1)(0)" "b" "H(j!1)(0)")) (("1" (assert) (("1" (expand "x_le") (("1" (propax) nil nil)) nil)) nil) ("2" (propax) nil nil) ("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (inst -8 "n!1") (("2" (expand "measurable_set?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-2 1)) (("2" (expand "increasing?") (("2" (skolem + ("i!1" "j!1")) (("2" (flatten) (("2" (inst - "i!1" "0" "j!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (inst -9 "0") nil nil)) nil) ("2" (hide-all-but (1 -11)) (("2" (expand "decreasing?") (("2" (skolem + ("i!1" "j!1")) (("2" (flatten) (("2" (expand "subset?") (("2" (skosimp) (("2" (expand "pointwise_increasing?") (("2" (inst - "x!1") (("2" (assert) (("2" (expand "HH") (("2" (expand "IUnion") (("2" (skosimp) (("2" (expand "H") (("2" (expand "increasing?") (("2" (inst + "i!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-11 1)) (("2" (skosimp) (("2" (expand "subset?") (("2" (expand "member") (("2" (expand "H") (("2" (skosimp) (("2" (expand "pointwise_increasing?") (("2" (inst - "x!1") (("2" (expand "increasing?") (("2" (inst - "n!1" "k!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-2 -9 1)) (("2" (skosimp) (("2" (inst - "n!1" "m!1") (("2" (inst - "n!1") (("2" (lemma "div_mult_pos_le2" ("py" "m!1 + 1" "x" "mu(H(n!1)(m!1))" "z" "M")) (("2" (assert) (("2" (assert) (("2" (rewrite "integral_nn") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "HH") (("2" (expand "IUnion") (("2" (expand "subset?") (("2" (expand "member") (("2" (skosimp*) (("2" (inst + "n!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (inst - "n!1" "m!1" "_") (("2" (hide 2) (("2" (lemma "nn_integrable_le" ("g" "(m!1 + 1) * phi(H(n!1)(m!1))" "f" "F!2(n!1)")) (("1" (split -1) (("1" (flatten) (("1" (lemma "isf_phi" ("E" "H(n!1)(m!1)")) (("1" (lemma "isf_scal" ("c" "m!1+1" "i" "phi[T, S](H(n!1)(m!1))")) (("1" (name-replace "RHS" "nn_integral(F!2(n!1))") (("1" (rewrite "integral_nn" -4 :dir rl) (("1" (rewrite "integral_scal" -4) (("1" (rewrite "integral_phi" -4) (("1" (assert) nil nil)) nil) ("2" (hide-all-but (-2 1)) (("2" (lemma "nn_isf_is_nn_integrable") (("2" (inst - "phi[T, S](H(n!1)(m!1))") (("1" (flatten) (("1" (lemma "nn_integrable_is_nn_integrable") (("1" (lemma "nn_integrable_is_integrable") (("1" (inst - "phi[T, S](H(n!1)(m!1))") nil nil)) nil)) nil)) nil) ("2" (expand "nn_isf?") (("2" (skosimp) (("2" (hide-all-but 1) (("2" (expand "phi") (("2" (expand "member") (("2" (case-replace "H(n!1)(m!1)(x!1)") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil) ("2" (inst -8 "n!1" "m!1") nil nil)) nil)) nil) ("2" (skosimp) (("2" (inst - "x!1") (("2" (assert) (("2" (hide-all-but 1) (("2" (expand "*") (("2" (expand "phi") (("2" (expand "member") (("2" (case-replace "H(n!1)(m!1)(x!1)") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "scal_measurable") (("2" (lemma "phi_is_simple" ("X" "H(n!1)(m!1)")) (("2" (rewrite "simple_is_measurable") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (inst -2 "n!1" "m!1") (("3" (inst -6 "n!1" "m!1") (("3" (expand "measurable_set?") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2 -2 -1) (("2" (skosimp) (("2" (expand "phi") (("2" (expand "H") (("2" (expand "member") (("2" (expand "*") (("2" (case-replace "F!2(n!1)(x!1) >= 1 + m!1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 -4)) (("2" (skosimp) (("2" (expand "H") (("2" (inst - "n!1" "m!1") (("2" (lemma "integrable_nz_finite" ("f" "F!2(n!1)" "epsilon" "m!1+1/2")) (("2" (flatten) (("2" (case-replace "{x: T | abs(F!2(n!1)(x)) >= m!1 + 1 / 2}={x | F!2(n!1)(x) >= m!1 + 1 / 2}") (("1" (hide -1) (("1" (lemma "m_monotone" ("a" "{x | F!2(n!1)(x) >= 1 + m!1}" "b" "{x | F!2(n!1)(x) >= m!1 + 1 / 2}")) (("1" (split -1) (("1" (expand "x_le") (("1" (expand "mu_fin?") (("1" (assert) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "subset?") (("2" (expand "member") (("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil) ("3" (propax) nil nil)) nil)) nil) ("2" (apply-extensionality :hide? t) (("2" (expand "abs") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (propax) nil nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp) (("2" (split) (("1" (flatten) (("1" (expand "IIntersection") (("1" (skosimp) (("1" (expand "HH") (("1" (expand "IUnion") (("1" (expand "H") (("1" (inst 2 "1+i!1") (("1" (skosimp) (("1" (inst + "n!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "IIntersection") (("2" (expand "HH") (("2" (expand "IUnion") (("2" (expand "H") (("2" (typepred "k!1") (("2" (inst -3 "k!1-1") (("2" (skosimp) (("2" (inst - "i!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (skosimp) (("2" (expand "HH") (("2" (rewrite "measurable_IUnion") (("2" (skosimp) (("2" (inst - "n!1" "m!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp) (("2" (expand "measurable_set?") (("2" (expand "H") (("2" (typepred "F!2(n!1)") (("2" (lemma "nn_integrable_is_measurable") (("2" (inst - "F!2(n!1)") (("2" (rewrite "measurable_ge") (("2" (inst - "1+m!1") nil nil)) nil)) nil)) nil)) nil)) nil)) --> -------------------- --> maximum size reached --> --------------------
¤ Dauer der Verarbeitung: 0.648 Sekunden (vorverarbeitet am 2026-04-25) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26