| 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 206 kB |
|
Impressum essential_bound_complete_scaf.prfSprache: Lisp |
|||||||||||||||
|
(essential_bound_complete_scaf (mu_TCC1 0 (mu_TCC1-1 nil 3502969751 ("" (typepred "S") (("" (expand "sigma_algebra?") (("" (flatten) (("" (expand "subset_algebra_empty?") (("" (expand "member") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ((subset_algebra_empty? const-decl "bool" subset_algebra_def "measure_integration/") (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 essential_bound_complete_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]" essential_bound_complete_scaf nil)) nil)) (essential_bound_complete_scaf 0 (essential_bound_complete_scaf-1 nil 3502969847 ("" (case "FORALL (F: sequence[essentially_bounded]): (FORALL n: essential_bound(F(n+1) - F(n)) < 2^(-n)) IMPLIES (EXISTS f: FORALL r: EXISTS n: FORALL i: i >= n => essential_bound(f - F(i)) < r)") (("1" (skosimp) (("1" (name "NEXT" "lambda (n,m:nat): (n+1,choose({k:nat | k > m & FORALL i, j: i >= k AND j >= k => essential_bound(F!1(j) - F!1(i)) < 2^(-n)}))") (("1" (name "SEQ" "lambda n: (iterate(NEXT,n+1)(0,0))`2") (("1" (case "forall n,i: i >= SEQ(n) => essential_bound(F!1(i) - F!1(SEQ(n))) < 2 ^ (-n)") (("1" (case "subseq?(F!1 o SEQ, F!1)") (("1" (inst -5 "F!1 o SEQ") (("1" (split -5) (("1" (skosimp) (("1" (inst + "f!1") (("1" (skosimp) (("1" (inst - "r!1/2") (("1" (skosimp) (("1" (case "exists n: 2^(-n) < r!1/2") (("1" (skosimp) (("1" (inst + "SEQ(n!1+n!2)") (("1" (skosimp) (("1" (inst - "n!1+n!2") (("1" (assert) (("1" (inst - "n!1+n!2" "i!1") (("1" (assert) (("1" (expand "o" -2) (("1" (lemma "essential_bound_diff" ("f0" "f!1 - F!1(SEQ(n!1 + n!2))" "f1" "F!1(i!1) - F!1(SEQ(n!1 + n!2))")) (("1" (assert) (("1" (case "2 ^ (-(n!1 + n!2))<=2 ^ (-n!2)") (("1" (assert) (("1" (name "LHS1" "essential_bound(f!1 - F!1(SEQ(n!1 + n!2)) - (F!1(i!1) - F!1(SEQ(n!1 + n!2))))") (("1" (name-replace "LHS2" "essential_bound(f!1 - F!1(i!1))") (("1" (case-replace "LHS1=LHS2") (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (expand "LHS2") (("2" (expand "LHS1") (("2" (expand "-") (("2" (assert) (("2" (name-replace "F1" "F!1(i!1)") (("2" (name-replace "F2" "F!1(SEQ(n!1 + n!2))") (("2" (expand "essential_bound") (("2" (expand "ae_le?") (("2" (expand "abs") (("2" (expand "pointwise_ae?") (("2" (expand "ae?") (("2" (expand "fullset") (("2" (expand "ae_in?") (("2" (expand "member") (("2" (expand "-") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "both_sides_real_expt_gt1_ge" ("gt1x" "2" "a" "-n!2" "b" "-(n!1 + n!2)")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (lemma "small_expt" ("px" "1/2")) (("2" (assert) (("2" (inst - "r!1/2") (("2" (skosimp) (("2" (inst + "n!2") (("2" (rewrite "real_expt_neg") (("2" (rewrite "real_expt_int_rew") (("2" (expand "^") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (inst -2 "n!1" "SEQ(n!1+1)") (("2" (expand "o ") (("2" (assert) (("2" (hide 1 -1 -2 -3) (("2" (expand "SEQ") (("2" (expand "iterate" 1 1) (("2" (name-replace "NN" "iterate(NEXT, 1 + n!1)(0, 0)") (("2" (expand "NEXT") (("2" (case "nonempty?({k: nat | k > NN`2 & (FORALL i, j: i >= k AND j >= k => essential_bound(F!1(j) - F!1(i)) < 2 ^ (-NN`1))})") (("1" (lemma "choose_member" ("a" "{k: nat | k > NN`2 & (FORALL i, j: i >= k AND j >= k => essential_bound(F!1(j) - F!1(i)) < 2 ^ (-NN`1))}")) (("1" (split) (("1" (name-replace "CC" "choose({k: nat | k > NN`2 & (FORALL i, j: i >= k AND j >= k => essential_bound(F!1(j) - F!1(i)) < 2 ^ (-NN`1))})") (("1" (expand "member") (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "nonempty?") (("2" (propax) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (inst -2 "2 ^ (-NN`1)") (("1" (skosimp) (("1" (inst - "n!2+NN`2+1") (("1" (assert) (("1" (skosimp) (("1" (inst - "i!1" "j!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "real_expt_pos") 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 "subseq?") (("2" (inst + "SEQ") (("1" (expand "o ") (("1" (propax) nil nil)) nil) ("2" (expand "strict_increasing?") (("2" (case "forall (i,n:nat): SEQ(i) < SEQ(1+i+n)") (("1" (skosimp) (("1" (inst - "x!1" "y!1-x!1-1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (induct "n") (("1" (skosimp) (("1" (expand "SEQ") (("1" (expand "iterate" 1 2) (("1" (name-replace "NN" "iterate(NEXT, 1 + i!1)(0, 0)") (("1" (expand "NEXT") (("1" (hide -2 -1) (("1" (case "nonempty?({k: nat | k > NN`2 & (FORALL i, j: i >= k AND j >= k => essential_bound(F!1(j) - F!1(i)) < 2 ^ (-NN`1))})") (("1" (lemma "choose_member" ("a" "{k: nat | k > NN`2 & (FORALL i, j: i >= k AND j >= k => essential_bound(F!1(j) - F!1(i)) < 2 ^ (-NN`1))}")) (("1" (split) (("1" (name-replace "RHS" "choose({k: nat | k > NN`2 & (FORALL i, j: i >= k AND j >= k => essential_bound(F!1(j) - F!1(i)) < 2 ^ (-NN`1))})") (("1" (expand "member") (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "nonempty?") (("2" (propax) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (inst -3 "2 ^ (-NN`1)") (("1" (skosimp) (("1" (inst - "n!1+NN`2+1") (("1" (assert) (("1" (skosimp) (("1" (inst - "i!2" "j!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "real_expt_pos") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (skosimp) (("2" (inst - "i!1") (("2" (name-replace "LHS" "SEQ(i!1)") (("2" (hide -2 -3 -4) (("2" (expand "SEQ") (("2" (expand "iterate" 1) (("2" (name-replace "NN" "iterate(NEXT, 2 + i!1 + j!1)(0, 0)") (("2" (expand "NEXT") (("2" (case "nonempty?({k: nat | k > NN`2 & (FORALL i, j: i >= k AND j >= k => essential_bound(F!1(j) - F!1(i)) < 2 ^ (-NN`1))})") (("1" (lemma "choose_member" ("a" "{k: nat | k > NN`2 & (FORALL i, j: i >= k AND j >= k => essential_bound(F!1(j) - F!1(i)) < 2 ^ (-NN`1))}")) (("1" (split) (("1" (name-replace "ZZ" "choose({k: nat | k > NN`2 & (FORALL i, j: i >= k AND j >= k => essential_bound(F!1(j) - F!1(i)) < 2 ^ (-NN`1))})") (("1" (expand "member") (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "nonempty?") (("2" (propax) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (inst -4 "2 ^ (-NN`1)") (("1" (skosimp) (("1" (inst - "n!1+NN`2+1") (("1" (assert) (("1" (skosimp) (("1" (inst - "i!2" "j!2") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (rewrite "real_expt_pos") 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" (induct "n") (("1" (skosimp) (("1" (expand "SEQ") (("1" (expand "iterate") (("1" (expand "iterate") (("1" (hide -2) (("1" (name "ZZ" "NEXT(0, 0)`2") (("1" (replace -1) (("1" (expand "NEXT" -1) (("1" (case "nonempty?({k: nat | k > 0 & (FORALL i, j: i >= k AND j >= k => essential_bound(F!1(j) - F!1(i)) < 2 ^ (-0))})") (("1" (lemma "choose_member" ("a" "{k: nat | k > 0 & (FORALL i, j: i >= k AND j >= k => essential_bound(F!1(j) - F!1(i)) < 2 ^ (-0))}")) (("1" (replace -3) (("1" (split -1) (("1" (expand "member") (("1" (flatten) (("1" (inst - "ZZ" "i!1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "nonempty?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (hide -1 -2 2) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (inst -4 "2^(-0)") (("1" (skosimp) (("1" (inst - "n!1+1") (("1" (assert) (("1" (skosimp) (("1" (inst -5 "i!2" "j!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "real_expt_pos" ("px" "2" "a" "-0")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (skosimp) (("2" (hide -3 -4) (("2" (expand "SEQ") (("2" (expand "iterate" 1) (("2" (expand "iterate" -2) (("2" (name-replace "NN" "iterate(NEXT, 1 + j!1)(0, 0)") (("2" (expand "NEXT") (("2" (case "nonempty?({k: nat | k > NN`2 & (FORALL i, j: i >= k AND j >= k => essential_bound(F!1(j) - F!1(i)) < 2 ^ (-NN`1))})") (("1" (lemma "choose_member" ("a" "{k: nat | k > NN`2 & (FORALL i, j: i >= k AND j >= k => essential_bound(F!1(j) - F!1(i)) < 2 ^ (-NN`1))}")) (("1" (split -1) (("1" (expand "member") (("1" (name-replace "CC" "choose({k: nat | k > NN`2 & (FORALL i, j: i >= k AND j >= k => essential_bound(F!1(j) - F!1(i)) < 2 ^ (-NN`1))})") (("1" (flatten) (("1" (inst - "CC" "i!1") (("1" (case-replace "NN`1=1+j!1") (("1" (assert) nil nil) ("2" (expand "NN" 1) (("2" (case "forall n: iterate(NEXT,n)(0, 0)`1 = n") (("1" (inst - "1+j!1") nil nil) ("2" (hide-all-but 1) (("2" (induct "n") (("1" (expand "iterate") (("1" (propax) nil nil)) nil) ("2" (skosimp) (("2" (expand "iterate" 1) (("2" (expand "NEXT" 1 1) (("2" (propax) nil nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (expand "NEXT") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "nonempty?") (("2" (propax) nil nil)) nil)) nil)) nil) ("2" (hide 2 -1 -2) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (inst -3 "2^(-NN`1)") (("1" (skosimp) (("1" (inst - "n!1+NN`2+1") (("1" (assert) (("1" (skosimp) (("1" (inst - "i!2" "j!2") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "real_expt_pos") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (expand "NEXT") (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (hide 1 -2) (("2" (inst -2 "2 ^ (-n!1)") (("1" (skosimp) (("1" (inst - "n!2+m!1+1") (("1" (assert) (("1" (skosimp) (("1" (inst - "i!1" "j!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "real_expt_pos" ("px" "2" "a" "-n!1")) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (case "FORALL (F: sequence[essentially_bounded]): EXISTS (N:null_set): FORALL (x:T,n): NOT N(x) => abs(F(n+1)(x)-F(n)(x)) <= essential_bound( (("1" (skosimp) (("1" (inst - "F!1") (("1" (skosimp) (("1" (case "FORALL (x: T, n, m: nat): NOT N!1(x) => abs(F!1(n + m)(x) - F!1(n)(x)) <= sigma[nat](n,n+m-1,geometric(1/2))") (("1" (case "forall (n,m:nat): sigma[nat](n, n + m - 1, geometric(1 / 2)) < 2^(1-n)") (("1" (case "exists (g:[T->complex]): pointwise_convergence?(lambda n: lambda (x:T): phi(compl (("1" (skosimp) (("1" (lemma "pointwise_complex_measurable" ("f" "g!1" "u" "LAMBDA n: LAMBDA (x: T): phi(complement(N!1))(x) * F!1(n)(x)")) (("1" (replace -2) (("1" (case "FORALL (x: T, n): NOT N!1(x) => abs(g!1(x) - F!1(n)(x)) < 2 ^ (2 - n)") (("1" (case "essentially_bounded?(g!1)") (("1" (inst + "g!1") (("1" (skosimp) (("1" (hide-all-but (-2 1)) (("1" (lemma "exp_of_exists" ("py" "r!1" "b" "2")) (("1" (skosimp) (("1" (lemma "both_sides_real_expt_gt1_lt" ("gt1x" "2" "a" "i!1-1" "b" "i!1")) (("1" (assert) (("1" (rewrite "real_expt_int_rew" * :dir rl) (("1" (rewrite "real_expt_int_rew" * :dir rl) (("1" (case "3-i!1>=0") (("1" (inst + "3-i!1") (("1" (skosimp) (("1" (lemma "both_sides_real_expt_gt1_le" ("gt1x" "2" "a" "2-i!2" "b" "i!1-1")) (("1" (assert) (("1" (lemma "essential_bound_def1" ("f" "g!1 - F!1(i!2)" "K" "2^(2-i!2)")) (("1" (split -1) (("1" (assert) nil nil) ("2" (hide 2) (("2" (expand "ae_le?") (("2" (expand "pointwise_ae?") (("2" (expand "ae?") (("2" (expand "fullset") (("2" (expand "ae_in?") (("2" (inst + "N!1") (("2" (skosimp) (("2" (expand "member") (("2" (inst - "x!1" "i!2") (("2" (assert) (("2" (expand "abs" 2) (("2" (assert) (("2" (expand "-" 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) ("2" (assert) (("2" (case "3-i!1<0") (("1" (hide 1) (("1" (lemma "both_sides_real_expt_gt1_lt" ("gt1x" "2" "a" "3" "b" "i!1")) (("1" (assert) (("1" (rewrite "real_expt_int_rew" -1) (("1" (rewrite "expt_x3") (("1" (inst + "0") (("1" (skosimp) (("1" (inst - "_" "i!2") (("1" (case "2 ^ (2 - i!2)< 8") (("1" (lemma "essential_bound_def1" ("f" "g!1 - F!1(i!2)" "K" "8")) (("1" (split -1) (("1" (assert) nil nil) ("2" (hide 2) (("2" (expand "ae_le?") (("2" (expand "pointwise_ae?") (("2" (expand "ae?") (("2" (expand "fullset") (("2" (expand "ae_in?") (("2" (expand "member") (("2" (inst + "N!1") (("2" (skosimp) (("2" (inst - "x!1") (("2" (assert) (("2" (expand "abs" 2) (("2" (expand "-" 2) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (lemma "both_sides_real_expt_gt1_lt" ("gt1x" "2" "a" "2-i!2" "b" "3")) (("2" (assert) (("2" (lemma "real_expt_int_rew" ("x" "2" "i" "3")) (("2" (replace -1) (("2" (rewrite "expt_x3") 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)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 1 -2)) (("2" (typepred "F!1(0)") (("2" (expand "essentially_bounded?") (("2" (replace -3) (("2" (flatten) (("2" (hide -1 -4) (("2" (expand "ae_bounded?") (("2" (skosimp) (("2" (inst + "K!1+4") (("2" (expand "ae_le?") (("2" (expand "pointwise_ae?") (("2" (expand "ae?") (("2" (expand "fullset") (("2" (expand "ae_in?") (("2" (skosimp) (("2" (typepred "E!1") (("2" (expand "member") (("2" (inst + "union(N!1,E!1)") (("2" (skosimp) (("2" (expand "union") (("2" (expand "member") (("2" (flatten) (("2" (hide -1) (("2" (inst - "x!1") (("2" (inst - "x!1" "0") (("2" (assert) (("2" (rewrite "real_expt_int_rew") (("2" (rewrite "expt_x2") (("2" (lemma "polar.abs_triangle" ("z1" "g!1(x!1)-F!1(0)(x!1)" "z2" "F!1(0)(x!1)")) (("2" (case-replace "abs(g!1(x!1) - F!1(0)(x!1) + F!1(0)(x!1))=abs(g!1)(x!1)") (("1" (assert) (("1" (assert) (("1" (expand "abs" 3) (("1" (expand "abs" -1 2) (("1" (expand "abs" -2 1) (("1" (assert) (("1" (name-replace "LHS" "abs(g!1(x!1))") (("1" (expand "abs" -3) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "abs") (("2" (expand "abs") (("2" (expand "sq_abs") (("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)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 2) (("2" (skosimp) (("2" (expand "pointwise_convergence?") (("2" (inst - "x!1") (("2" (expand "complement") (("2" (expand "phi") (("2" (expand "member") (("2" (inst -3 "x!1" "_" "_") (("2" (inst -4 "x!1" "_") (("2" (replace 1) (("2" (hide 1) (("2" (rewrite "metric_convergence_def" -1) (("2" (expand "metric_converges_to") (("2" (expand "ball") (("2" (expand "member") (("2" (inst - "2^(-n!1)") (("1" (skosimp) (("1" (inst - "n!1+n!2+1") (("1" (assert) (("1" (inst - "n!1" "1+n!2") (("1" (inst - "n!1" "1+n!2") (("1" (hide -4 -5) (("1" (lemma "polar.abs_triangle" ("z1" "g!1(x!1) - 1 * F!1(1 + n!1 + n!2)(x!1)" "z2" "F!1(1 + n!2 + n!1)(x!1) - F!1(n!1)(x!1)")) (("1" (case-replace "abs(g!1(x!1) - 1 * F!1(1 + n!1 + n!2)(x!1) + (F!1(1 + n!2 + n!1)(x!1) - F!1(n!1)(x!1)))=abs(g!1(x!1) - F!1(n!1)(x!1))") (("1" (hide -1) (("1" (case "2 ^ (-n!1)+2 ^ (1 - n!1) <=2 ^ (2 - n!1)") (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (lemma "real_expt_plus" ("x" "2" "a" "1" "b" "-n!1")) (("2" (lemma "real_expt_plus" ("x" "2" "a" "2" "b" "-n!1")) (("2" (replace -1) (("2" (replace -2) (("2" (hide -1 -2) (("2" (lemma "both_sides_times_pos_le1" ("pz" "2^(-n!1)" "x" "1+2^1" "y" "2^2")) (("1" (assert) (("1" (hide 2) (("1" (rewrite "real_expt_int_rew") (("1" (rewrite "real_expt_int_rew") (("1" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (rewrite "real_expt_int_rew") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "abs") (("2" (expand "sq_abs") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "real_expt_pos") 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) (("2" (skosimp) (("2" (typepred "F!1(n!1)") (("2" (typepred "N!1") (("2" (lemma "null_set_is_measurable[T,S,mu]") (("2" (inst - "N!1") (("2" (lemma "measurable_complement[T,S]" ("a" "N!1")) (("2" (lemma "phi_is_simple" ("X" "complement[T](N!1)")) (("1" (assert) (("1" (lemma "prod_measurable" ("g1" "phi(complement[T](N!1))" "g2" "Re(F!1(n!1))")) (("1" (expand "*" -1) (("1" (expand "Re" 1) (("1" (expand "Im" 1) (("1" (lemma "prod_measurable" ("g1" "phi(complement[T](N!1))" "g2" "Im(F!1(n!1))")) (("1" (expand "*" -1) (("1" (assert) nil nil)) nil) ("2" (expand "essentially_bounded?") (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "essentially_bounded?") (("2" (flatten) (("2" (assert) nil nil)) nil)) nil) ("3" (expand "simple?") (("3" (flatten) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "measurable_set?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2 -3 -4) (("2" (case "FORALL (x: T): NOT N!1(x) IMPLIES metric_convergent? (LAMBDA (n:nat): F!1(n)(x))") (("1" (inst + "lambda (x:T): if N!1(x) then complex_(0,0) else limit(LAMBDA (n: nat): F!1(n)(x)) endif") (("1" (expand "pointwise_convergence?") (("1" (skosimp) (("1" (inst - "x!1") (("1" (expand "complement") (("1" (expand "phi") (("1" (expand "member") (("1" (case-replace "N!1(x!1)") (("1" (rewrite "metric_convergence_def") (("1" (expand "metric_converges_to") (("1" (skosimp) (("1" (inst + "0") (("1" (skosimp) (("1" (expand "ball") (("1" (expand "member") (("1" (expand "abs") (("1" (expand "sq_abs") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma "limit_lemma" ("v" "LAMBDA (n_1: nat): 1 * F!1(n_1)(x!1)")) (("1" (hide -3 -4 1) (("1" (expand "*") (("1" (assert) (("1" (expand "convergence?") (("1" (skosimp) (("1" (inst - "U!1") (("1" (assert) (("1" (split) (("1" (propax) nil nil) ("2" (hide 2) (("2" (case-replace "equalities.=(LAMBDA (n_1: nat): complex_(1 * Re(F!1(n_1)(x!1)), 1 * Im(F!1(n_1)(x!1))),LAMBDA (n: nat): F!1(n)(x!1))") (("2" (apply-extensionality :hide? t) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "metric_convergent?") (("2" (expand "convergent?") (("2" (skosimp) (("2" (inst + "x!2") (("2" (rewrite "metric_convergence_def") (("2" (expand "metric_converges_to") (("2" (expand "ball") (("2" (expand "member") (("2" (hide-all-but (-1 1)) (("2" (skosimp) (("2" (inst - "r!1") (("2" (skosimp) (("2" (inst + "n!1") (("2" (skosimp) (("2" (inst - "i!1") (("2" (assert) (("2" (expand "*") (("2" (expand "-") (("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) ("2" (skosimp) (("2" (inst - "x!1") (("2" (assert) (("2" (expand "convergent?") (("2" (expand "metric_convergent?") (("2" (skosimp) (("2" (inst + "x!2") (("2" (rewrite "metric_convergence_def") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (inst - "x!1" "_" "_") (("2" (assert) (("2" (hide 1) (("2" (lemma "complex_is_complete") (("2" (expand "fullset") (("2" (expand "complete_metric_space?") (("2" (expand "metric_complete?") (("2" (flatten) (("2" (inst - "LAMBDA (n: nat): F!1(n)(x!1)") (("2" (split) (("1" (expand "metric_convergent?") (("1" (propax) nil nil)) nil) ("2" (hide -1 2) (("2" (expand "cauchy?") (("2" (skosimp) (("2" (expand "ball") (("2" (expand "member") (("2" (lemma "exp_of_exists" ("b" "2" "py" "r!1")) (("2" (skosimp) (("2" (case "i!1>=0") (("1" (inst + "2") (("1" (skosimp) (("1" (lemma "trich_lt" ("x" "i!2" "y" "j!1")) (("1" (split) (("1" (inst - "i!2" "j!1-i!2") (("1" (inst - "i!2" "j!1-i!2") (("1" (assert) (("1" (lemma "both_sides_real_expt_gt1_lt" ("gt1x" "2" "a" "1-i!2" "b" "i!1")) (("1" (assert) (("1" (rewrite "real_expt_int_rew") (("1" (rewrite "real_expt_int_rew") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil) ("2" (replace -1) (("2" (assert) (("2" (expand "abs") (("2" (expand "sq_abs") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (inst - "j!1" "i!2-j!1") (("1" (inst - "j!1" "i!2-j!1") (("1" (lemma "both_sides_real_expt_gt1_lt" ("gt1x" "2" "a" "1-j!1" "b" "i!1")) (("1" (assert) (("1" (rewrite "real_expt_int_rew") (("1" (rewrite "real_expt_int_rew") (("1" (assert) (("1" (expand "abs") (("1" (expand "sq_abs") (("1" (assert) (("1" (lemma "sq_neg_minus" ("a" "Im(F!1(j!1)(x!1))" "b" "Im(F!1(i!2)(x!1))")) (("1" (lemma "sq_neg_minus" ("a" "Re(F!1(j!1)(x!1))" "b" "Re(F!1(i!2)(x!1))")) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (assert) (("2" (case "i!1<0") (("1" (hide 1) (("1" (inst + "2-i!1") (("1" (skosimp) (("1" (lemma "trich_lt" ("x" "i!2" "y" "j!1")) (("1" (split) (("1" (inst - "i!2" "j!1-i!2") (("1" (inst - "i!2" "j!1-i!2") (("1" (lemma "both_sides_real_expt_gt1_lt" ("gt1x" "2" "a" "1-i!2" "b" "i!1")) (("1" (assert) (("1" (rewrite "real_expt_int_rew") (("1" (rewrite "real_expt_int_rew") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil) ("2" (replace -1) (("2" (expand "abs") (("2" (expand "sq_abs") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (inst - "j!1" "i!2-j!1") (("1" (inst - "j!1" "i!2-j!1") (("1" (lemma "both_sides_real_expt_gt1_lt" ("gt1x" "2" "a" "1-j!1" "b" "i!1")) (("1" (assert) (("1" (rewrite "real_expt_int_rew") (("1" (rewrite "real_expt_int_rew") (("1" (case-replace "abs(F!1(i!2)(x!1) - F!1(j!1)(x!1))=abs(F!1(j!1)(x!1) - F!1(i!2)(x!1))") (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (expand "abs") (("2" (expand "sq_abs") (("2" (lemma "sq_neg_minus" ("a" "Im(F!1(i!2)(x!1))" "b" "Im(F!1(j!1)(x!1))")) (("2" (lemma "sq_neg_minus" ("a" "Re(F!1(i!2)(x!1))" "b" "Re(F!1(j!1)(x!1))")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (assert) 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) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (case-replace "m!1=0") (("1" (expand "sigma") (("1" (lemma "real_expt_pos" ("px" "2" "a" "1-n!1")) (("1" (assert) nil nil)) nil)) nil) ("2" (case "m!1>=1") (("1" (hide 1) (("1" (lemma "sigma_geometric" ("x" "1/2" "n" "n!1+m!1-1")) (("1" (case-replace "n!1=0") (("1" (assert) (("1" (rewrite "real_expt_int_rew" 1) (("1" (assert) (("1" (rewrite "expt_x1") (("1" (case "(1 - (1 / 2) ^ m!1) / (1 - 1 / 2) < 2") (("1" (assert) nil nil) ("2" (hide-all-but (-3 1)) (("2" (grind-reals) (("2" (move-terms 1 l 1) (("2" (assert) (("2" (rewrite "real_expt_int_rew" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "n!1>=1") (("1" (hide 1) (("1" (lemma "sigma_geometric" ("x" "1/2" "n" "n!1-1")) (("1" (lemma "sigma_split" ("low" "0" "high" "n!1+m!1-1" "F" "geometric(1 / 2)" "z" "n!1-1")) (("1" (assert) (("1" (name-replace "LHS" "sigma(n!1, m!1 - 1 + n!1, geometric(1 / 2))") (("1" (name-replace "DRL1" "sigma(0, m!1 - 1 + n!1, geometric(1 / 2))") (("1" (name-replace "DRL2" "sigma(0, n!1 - 1, geometric(1 / 2))") (("1" (rewrite "real_expt_int_rew") (("1" (assert) (("1" (case "DRL1-DRL2 = 2*(exponentiation.^(1/2,n!1)-exponentiation.^(1/2,m!1+n!1))") (("1" (rewrite "expt_plus" -1) (("1" (lemma "expt_plus" ("n0x" "2" "i" "1" "j" "-n!1")) (("1" (rewrite "expt_x1") (("1" (replace -1) (("1" (lemma "both_sides_times_pos_lt1" ("pz" " 2 * exponentiation.^(1 / 2, n!1)" "x" "1-exponentiation.^(1 / 2, m!1)" "y" "1")) (("1" (rewrite "expt_inverse" 1) (("1" (rewrite "inv_expt" 1 :dir rl) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (inst + "n!1+m!1") (("3" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skolem + ("x!1" "n!1" "_")) (("2" (inst - "x!1" "_") (("2" (case-replace "N!1(x!1)") (("2" (assert) (("2" (hide 1) (("2" (induct "m") (("1" (expand "sigma") (("1" (expand "abs") (("1" (expand "sq_abs") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) (("2" (expand "sigma" 1) (("2" (inst - "j!1+n!1") (("2" (inst - "j!1+n!1") (("2" (expand "geometric" 1 1) (("2" (rewrite "real_expt_neg" -3) (("2" (rewrite "real_expt_int_rew" -3) (("2" (lemma "polar.abs_triangle" ("z1" "F!1(1 + (j!1 + n!1))(x!1) - F!1(j!1 + n!1)(x!1)" "z2" "F!1(j!1 + n!1)(x!1) - F!1(n!1)(x!1)")) (("2" (case-replace "abs(F!1(1 + j!1 + n!1)(x!1) - F!1(n!1)(x!1))=abs(F!1(1 + (j!1 + n!1))(x!1) - F!1(j!1 + n!1)(x (F!1(j!1 + n!1)(x!1) - F!1(n!1)(x!1)))") (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (expand "abs") (("2" (expand "sq_abs") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (inst + "n!1+m!1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (inst + "3") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (name "EE" "lambda n: choose[(S)]({E:(S) | null_set?(E) & forall (x:T): not E(x) => abs(F!1(n+1)(x) (("1" (inst + "IUnion(EE)") (("1" (hide -1) (("1" (skosimp) (("1" (case "forall n: not EE(n)(x!1) => abs(F!1(n + 1)(x!1) - F!1(n)(x!1)) <= essential_bound(F!1(n (("1" (expand "IUnion") (("1" (inst + "n!1") (("1" (inst - "n!1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2 3) (("2" (skosimp) (("2" (expand "EE") (("2" (case "nonempty?[(S)]({E: (S) | null_set?(E) & (FORALL (x: T): NOT E(x) => abs(F!1(1 + n!2)(x) - F!1(n!2)(x)) <= essential_bound(F!1(1 + n!2) - F!1(n!2)))})") (("1" (lemma "choose_member[(S)]" ("a" "{E: (S) | null_set?(E) & (FORALL (x: T): NOT E(x) => abs(F!1(1 + n!2)(x) - F!1(n!2)(x)) <= essential_bound(F!1(1 + n!2) - F!1(n!2)))}")) (("1" (name-replace "CC" "choose[(S)] ({E: (S) | null_set?(E) & (FORALL (x: T): NOT E(x) => abs(F!1(1 + n!2)(x) - F!1(n!2)(x)) <= essential_bound(F!1(1 + n!2) - F!1(n!2)))})") (("1" (split -1) (("1" (expand "member") (("1" (inst - "x!1") (("1" (assert) nil nil)) nil)) nil) ("2" (expand "nonempty?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (lemma "essential_bound_def2" ("f" "F!1(n!2 + 1) - F!1(n!2)")) (("2" (expand "ae_le?") (("2" (expand "pointwise_ae?") (("2" (expand "ae?") (("2" (expand "fullset") (("2" (expand "ae_in?") (("2" (skosimp) (("2" (typepred "E!1") (("2" (expand "negligible_set?") (("2" (skosimp) (("2" (inst -4 "X!1") (("1" (assert) (("1" (skosimp) (("1" (inst - "x!2") (("1" (assert) (("1" (expand "subset?") (("1" (inst - "x!2") (("1" (assert) (("1" (expand "abs" -2) (("1" (expand "-" -2 1) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "null_set_is_measurable") (("2" (inst - "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)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (lemma "diff_essentially_bounded" ("f0" "F!1(1+n!1)" "f1" "F!1(n!1)")) (("2" (lemma "essential_bound_def2" ("f" "((-[T])(F!1(1 + n!1), F!1(n!1)))")) (("2" (name-replace "EB" " essential_bound(((-[T])(F!1(1 + n!1), F!1(n!1))))") (("2" (hide -2) (("2" (expand "ae_le?") (("2" (expand "pointwise_ae?") (("2" (expand "ae?") (("2" (expand "fullset") (("2" (expand "ae_in?") (("2" (expand "member") (("2" (skosimp) (("2" (typepred "E!1") (("2" (expand "negligible_set?") (("2" (skosimp) (("2" (inst -4 "X!1") (("1" (assert) (("1" (skosimp) (("1" (expand "subset?") (("1" (inst -2 "x!1") (("1" (expand "member") (("1" (assert) (("1" (inst - "x!1") (("1" (assert) (("1" (expand "abs" -2) (("1" (expand "-" -2) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma "null_set_is_measurable") (("2" (inst - "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)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (subset? const-decl "bool" sets nil) (X!1 skolem-const-decl "set[T]" essential_bound_complete_scaf nil) (essential_bound_def2 formula-decl nil essentially_bounded nil) (EE skolem-const-decl "[n: nat -> ({E: (S) | null_set?(E) & (FORALL (x: T): NOT E(x) => abs(F!1(n + 1)(x) - F!1(n)(x)) <= essential_bound(F!1(n + 1) - F!1(n)))})]" essential_bound_complete_scaf nil) (IUnion const-decl "set[T]" indexed_sets nil) (sigma_algebra_IUnion_rew application-judgement "(S)" essential_bound_complete_scaf nil) (null_IUnion application-judgement "null_set[T, S, mu]" essential_bound_complete_scaf nil) (diff_essentially_bounded judgement-tcc nil essentially_bounded nil) (X!1 skolem-const-decl "set[T]" essential_bound_complete_scaf nil) (n!1 skolem-const-decl "nat" essential_bound_complete_scaf nil) (metric_complete? const-decl "bool" metric_space_def "metric_space/") (j!1 skolem-const-decl "nat" essential_bound_complete_scaf nil) (i!2 skolem-const-decl "nat" essential_bound_complete_scaf nil) (trich_lt formula-decl nil real_props nil) (sq_neg_minus formula-decl nil sq "reals/") (j!1 skolem-const-decl "nat" essential_bound_complete_scaf nil) (i!2 skolem-const-decl "nat" essential_bound_complete_scaf nil) (cauchy? const-decl "bool" metric_space_def "metric_space/") (metric_convergent? const-decl "bool" metric_space_def "metric_space/") (complete_metric_space? const-decl "bool" metric_space_def "metric_space/") (complex_is_complete judgement-tcc nil complex_topology nil) (metric_space_is_hausdorff name-judgement "hausdorff[complex]" complex_topology nil) (metric_space_is_hausdorff? name-judgement "(hausdorff?)" complex_topology nil) (N!1 skolem-const-decl "null_set[T, S, mu]" essential_bound_complete_scaf nil) (metric_induced_topology const-decl "setofsets[T]" metric_space_def "metric_space/") (convergent? const-decl "bool" topological_convergence "topology/") (F!1 skolem-const-decl "sequence[essentially_bounded]" essential_bound_complete_scaf nil) (limit const-decl "T" topological_convergence "topology/") (convergent type-eq-decl nil topological_convergence "topology/") (complex_ adt-constructor-decl "[[real, real] -> (complex_?)]" complex_types "complex_alt/") (IF const-decl "[boolean, T, T -> T]" if_def nil) (complex_? adt-recognizer-decl "[complex -> boolean]" complex_types "complex_alt/") (eq_rew formula-decl nil complex_types "complex_alt/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (Re const-decl "real" complex_types "complex_alt/") (Im const-decl "real" complex_types "complex_alt/") (open? const-decl "bool" topology "topology/") (open nonempty-type-eq-decl nil topology "topology/") (convergence? const-decl "bool" topological_convergence "topology/") (limit_lemma formula-decl nil topological_convergence "topology/") (sqrt_0 formula-decl nil sqrt "reals/") (sq_0 formula-decl nil sq "reals/") (metric_convergent? const-decl "bool" metric_space_def "metric_space/") (null_set_is_measurable judgement-tcc nil measure_theory "measure_integration/") (measurable_complement judgement-tcc nil measure_space_def "measure_integration/") (measurable_set? const-decl "bool" measure_space_def "measure_integration/") (measurable_set nonempty-type-eq-decl nil measure_space_def "measure_integration/") (simple? const-decl "bool" measure_space "measure_integration/") (* const-decl "[T -> real]" real_fun_ops "reals/") (complex_measurable_def formula-decl nil complex_measurable nil) (Re_fun_rew formula-decl nil complex_fun_ops "complex_alt/") (Im_fun_rew formula-decl nil complex_fun_ops "complex_alt/") (measurable_function nonempty-type-eq-decl nil measure_space_def "measure_integration/") (prod_measurable judgement-tcc nil measure_space "measure_integration/") (phi_is_simple judgement-tcc nil measure_space "measure_integration/") (metric_converges_to const-decl "bool" metric_space_def "metric_space/") (real_times_real_is_real application-judgement "real" reals nil) (Re_mul2 formula-decl nil complex_types "complex_alt/") (Im_mul2 formula-decl nil complex_types "complex_alt/") (both_sides_times_pos_le1 formula-decl nil real_props nil) (posnat_expt application-judgement "posnat" exponentiation nil) (expt def-decl "real" exponentiation nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (real_expt_plus formula-decl nil real_expt "power/") (n!1 skolem-const-decl "nat" essential_bound_complete_scaf nil) (ball const-decl "set[T]" metric_space_def "metric_space/") (metric_convergence_def formula-decl nil metric_space "metric_space/") (exp_of_exists formula-decl nil exponentiation nil) (above nonempty-type-eq-decl nil integers nil) (both_sides_real_expt_gt1_lt formula-decl nil real_expt "power/") (TRUE const-decl "bool" booleans nil) (negligible_set? const-decl "bool" measure_theory "measure_integration/") (negligible nonempty-type-eq-decl nil measure_theory "measure_integration/") (essential_bound_def1 formula-decl nil essentially_bounded nil) (both_sides_real_expt_gt1_le formula-decl nil real_expt "power/") (i!1 skolem-const-decl "int" essential_bound_complete_scaf nil) (posint_exp application-judgement "posint" exponentiation nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (even_times_int_is_even application-judgement "even_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (expt_x3 formula-decl nil exponentiation nil) (g!1 skolem-const-decl "[T -> complex]" essential_bound_complete_scaf nil) (negligible_union application-judgement "negligible[T, S, mu]" essential_bound_complete_scaf nil) (union const-decl "set" sets nil) (posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types nil) (expt_x2 formula-decl nil exponentiation nil) (+ const-decl "complex" complex_types "complex_alt/") (sq_abs const-decl "nnreal" complex_types "complex_alt/") (real_plus_real_is_real application-judgement "real" reals nil) (Re_add1 formula-decl nil complex_types "complex_alt/") (Re_sub1 formula-decl nil complex_types "complex_alt/") (Im_add1 formula-decl nil complex_types "complex_alt/") (Im_sub1 formula-decl nil complex_types "complex_alt/") (abs_triangle formula-decl nil polar "complex_alt/") (nnreal_plus_posreal_is_posreal application-judgement "posreal" real_types nil) (ae_bounded? const-decl "bool" complex_measure_theory nil) (measurable_function? const-decl "bool" measure_space_def "measure_integration/") (Re const-decl "[T -> real]" complex_fun_ops "complex_alt/") (Im const-decl "[T -> real]" complex_fun_ops "complex_alt/") (complex_measurable nonempty-type-eq-decl nil complex_measurable nil) (complex_measurable? const-decl "bool" complex_measurable nil) (pointwise_complex_measurable formula-decl nil complex_measurable nil) (complement const-decl "set" sets nil) (phi const-decl "nat" measure_space "measure_integration/") (* const-decl "complex" complex_types "complex_alt/") (pointwise_convergence? const-decl "bool" complex_measurable nil) (measurable_complement application-judgement "measurable_set[T, S]" essential_bound_complete_scaf nil) (subset_algebra_complement application-judgement "(S)" measure_def "measure_integration/") (sigma_geometric formula-decl nil series "series/") (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (rat_times_rat_is_rat application-judgement "rat" rationals nil) (expt_inverse formula-decl nil exponentiation nil) (inv_expt formula-decl nil exponentiation nil) (both_sides_times_pos_lt1 formula-decl nil real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (expt_plus formula-decl nil exponentiation nil) (nzreal nonempty-type-eq-decl nil reals nil) (sigma_split formula-decl nil sigma "reals/") (odd_minus_even_is_odd application-judgement "odd_int" integers nil) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (div_mult_pos_lt1 formula-decl nil real_props nil) (div_div1 formula-decl nil real_props nil) (posrat_times_posrat_is_posrat application-judgement "posrat" rationals nil) (minus_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (minus_real_is_real application-judgement "real" reals nil) (even_minus_even_is_even application-judgement "even_int" integers nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (expt_x1 formula-decl nil exponentiation nil) (rat_minus_rat_is_rat application-judgement "rat" rationals nil) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (geometric const-decl "sequence[real]" series "series/") (sigma def-decl "real" sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (abs const-decl "nnreal" polar "complex_alt/") (NOT const-decl "[bool -> bool]" booleans nil) (null_set nonempty-type-eq-decl nil measure_theory "measure_integration/") (null_set? const-decl "bool" measure_theory "measure_integration/") (n!1 skolem-const-decl "nat" essential_bound_complete_scaf nil) (iterate def-decl "T" function_iterate nil) (NN skolem-const-decl "[nat, nat]" essential_bound_complete_scaf nil) (F!1 skolem-const-decl "sequence[essentially_bounded]" essential_bound_complete_scaf nil) (minus_nzint_is_nzint application-judgement "nzint" integers nil) (minus_even_is_even application-judgement "even_int" integers nil) (subseq? const-decl "bool" subseq "topology/") (O const-decl "T3" function_props nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (both_sides_real_expt_gt1_ge formula-decl nil real_expt "power/") (LHS1 skolem-const-decl "nnreal" essential_bound_complete_scaf nil) (ae_le? const-decl "bool" measure_theory "measure_integration/") (pointwise_ae? const-decl "bool" measure_theory "measure_integration/") (fullset const-decl "set" sets nil) (member const-decl "bool" sets nil) (Re_rew formula-decl nil complex_types "complex_alt/") (Im_rew formula-decl nil complex_types "complex_alt/") (real_minus_real_is_real application-judgement "real" reals nil) (- const-decl "complex" complex_types "complex_alt/") (ae_in? const-decl "bool" measure_theory "measure_integration/") (ae? const-decl "bool" measure_theory "measure_integration/") (measurable_fullset name-judgement "measurable_set[T, S]" essential_bound_complete_scaf nil) (subset_algebra_fullset name-judgement "(S)" essential_bound_complete_scaf nil) (abs const-decl "[T -> nonneg_real]" complex_fun_ops "complex_alt/") (LHS2 skolem-const-decl "nnreal" essential_bound_complete_scaf nil) (<= const-decl "bool" reals nil) (essential_bound_diff formula-decl nil essentially_bounded nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (small_expt formula-decl nil exponentiation nil) (real_expt_int_rew formula-decl nil real_expt "power/") (posrat_exp application-judgement "posrat" exponentiation nil) (nnrat_exp application-judgement "nnrat" exponentiation nil) (^ const-decl "real" exponentiation nil) (real_expt_neg formula-decl nil real_expt "power/") (NEXT skolem-const-decl "[d: [nat, nat] -> [numfield, ({k: nat | k > d`2 & (FORALL i, j: i >= k AND j >= k => essential_bound(F!1(j) - F!1(i)) < 2 ^ (-d`1))})]]" essential_bound_complete_scaf nil) (empty? const-decl "bool" sets nil) (NN skolem-const-decl "[nat, nat]" essential_bound_complete_scaf nil) (real_expt_pos formula-decl nil real_expt "power/") (choose_member formula-decl nil sets_lemmas nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (SEQ skolem-const-decl "[nat -> nat]" essential_bound_complete_scaf nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (NN skolem-const-decl "[nat, nat]" essential_bound_complete_scaf nil) (odd_plus_odd_is_even application-judgement "even_int" integers nil) (NN skolem-const-decl "[nat, nat]" essential_bound_complete_scaf nil) (nat_induction formula-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil) (int_plus_int_is_int application-judgement "int" integers nil) (y!1 skolem-const-decl "nat" essential_bound_complete_scaf nil) (x!1 skolem-const-decl "nat" essential_bound_complete_scaf nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (int_minus_int_is_int application-judgement "int" integers nil) (strict_increasing? const-decl "bool" real_fun_preds "reals/") (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (set type-eq-decl nil sets nil) (nonempty? const-decl "bool" sets nil) (choose const-decl "(p)" sets nil) (diff_essentially_bounded application-judgement "essentially_bounded[T, S, mu]" essential_bound_complete_scaf nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (minus_int_is_int application-judgement "int" integers nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans 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) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (T formal-type-decl nil essential_bound_complete_scaf nil) (complex type-decl nil complex_types "complex_alt/") (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]" essential_bound_complete_scaf nil) (nnreal type-eq-decl nil real_types nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (measure? const-decl "bool" generalized_measure_def "measure_integration/") (measure_type nonempty-type-eq-decl nil generalized_measure_def "measure_integration/") (mu formal-const-decl "measure_type[T, S]" essential_bound_complete_scaf nil) (essentially_bounded? const-decl "bool" essentially_bounded nil) (essentially_bounded nonempty-type-eq-decl nil essentially_bounded nil) (sequence type-eq-decl nil sequences nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (essential_bound const-decl "nnreal" essentially_bounded 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) (OR const-decl "[bool, bool -> bool]" booleans nil) (> const-decl "bool" reals nil) (^ const-decl "nnreal" real_expt "power/") (- const-decl "[numfield -> numfield]" number_fields nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil)) shostak)))
¤ 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.0.172Bemerkung: (vorverarbeitet am 2026-04-27) ¤*Bot Zugriff |
|
||||||||||||||
2026-05-26