Nuprl Lemma : alternating-series-tail-bound
∀x:ℕ ⟶ ℝ. ∀M:ℕ.
((∀n:ℕ. ((M ≤ n) ⇒ ((r0 ≤ x[n]) ∧ (x[n + 1] ≤ x[n]))))
⇒ lim n→∞.x[n] = r0
⇒ (∀a:{M...}. ∀b:ℕ. (|Σ{-1^i * x[i] | a≤i≤b}| ≤ x[a])))
Proof
Definitions occuring in Statement :
rsum: Σ{x[k] | n≤k≤m},
converges-to: lim n→∞.x[n] = y,
rleq: x ≤ y,
rabs: |x|,
int-rmul: k1 * a,
int-to-real: r(n),
real: ℝ,
fastexp: i^n,
int_upper: {i...},
nat: ℕ,
so_apply: x[s],
le: A ≤ B,
all: ∀x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
function: x:A ⟶ B[x],
add: n + m,
minus: -n,
natural_number: $n
Definitions unfolded in proof :
all: ∀x:A. B[x],
implies: P ⇒ Q,
member: t ∈ T,
int_upper: {i...},
nat: ℕ,
decidable: Dec(P),
or: P ∨ Q,
uall: ∀[x:A]. B[x],
so_lambda: λ2x.t[x],
int_seg: {i..j-},
lelt: i ≤ j < k,
and: P ∧ Q,
le: A ≤ B,
less_than: a < b,
squash: ↓T,
ge: i ≥ j ,
uimplies: b supposing a,
not: ¬A,
satisfiable_int_formula: satisfiable_int_formula(fmla),
exists: ∃x:A. B[x],
false: False,
prop: ℙ,
so_apply: x[s],
pointwise-req: x[k] = y[k] for k ∈ [n,m],
uiff: uiff(P;Q),
rev_uimplies: rev_uimplies(P;Q),
subtype_rel: A ⊆r B,
less_than': less_than'(a;b),
absval: |i|,
sq_type: SQType(T),
guard: {T},
sq_stable: SqStable(P),
rnonneg: rnonneg(x),
rleq: x ≤ y,
top: Top,
cand: A c∧ B,
req_int_terms: t1 ≡ t2,
rev_implies: P ⇐ Q,
iff: P ⇐⇒ Q,
nat_plus: ℕ+,
rge: x ≥ y,
true: True,
bool: 𝔹,
unit: Unit,
it: ⋅,
btrue: tt,
ifthenelse: if b then t else f fi ,
bfalse: ff,
bnot: ¬bb,
assert: ↑b,
nequal: a ≠ b ∈ T
Latex:
\mforall{}x:\mBbbN{} {}\mrightarrow{} \mBbbR{}. \mforall{}M:\mBbbN{}.
((\mforall{}n:\mBbbN{}. ((M \mleq{} n) {}\mRightarrow{} ((r0 \mleq{} x[n]) \mwedge{} (x[n + 1] \mleq{} x[n]))))
{}\mRightarrow{} lim n\mrightarrow{}\minfty{}.x[n] = r0
{}\mRightarrow{} (\mforall{}a:\{M...\}. \mforall{}b:\mBbbN{}. (|\mSigma{}\{-1\^{}i * x[i] | a\mleq{}i\mleq{}b\}| \mleq{} x[a])))
Date html generated:
2020_05_20-AM-11_23_29
Last ObjectModification:
2019_12_14-PM-04_52_27
Theory : reals
Home
Index