### Nuprl Lemma : fun-ratio-test

I:Interval. ∀f:ℕ ⟶ I ⟶ℝ.
((∀n:ℕf[n;x] continuous for x ∈ I)
(∀m:{m:ℕ+icompact(i-approx(I;m))}
∃c:ℝ((r0 ≤ c) ∧ (c < r1) ∧ (∃N:ℕ. ∀n:{N...}. ∀x:{x:ℝx ∈ i-approx(I;m)} .  (|f[n 1;x]| ≤ (c |f[n;x]|)))))
Σn.f[n;x]↓ absolutely for x ∈ I)

Proof

Definitions occuring in Statement :  fun-series-converges-absolutely: Σn.f[n; x]↓ absolutely for x ∈ I continuous: f[x] continuous for x ∈ I icompact: icompact(I) rfun: I ⟶ℝ i-approx: i-approx(I;n) i-member: r ∈ I interval: Interval rleq: x ≤ y rless: x < y rabs: |x| rmul: b int-to-real: r(n) real: int_upper: {i...} nat_plus: + nat: so_apply: x[s1;s2] all: x:A. B[x] exists: x:A. B[x] implies:  Q and: P ∧ Q set: {x:A| B[x]}  function: x:A ⟶ B[x] add: m natural_number: \$n
Definitions unfolded in proof :  fun-series-converges-absolutely: Σn.f[n; x]↓ absolutely for x ∈ I fun-series-converges: Σn.f[n; x]↓ for x ∈ I all: x:A. B[x] member: t ∈ T so_lambda: λ2y.t[x; y] rfun: I ⟶ℝ uall: [x:A]. B[x] nat: so_lambda: λ2x.t[x] so_apply: x[s1;s2] int_seg: {i..j-} lelt: i ≤ j < k and: P ∧ Q le: A ≤ B less_than: a < b squash: T ge: i ≥  decidable: Dec(P) or: P ∨ Q uimplies: supposing a not: ¬A implies:  Q satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False prop: subtype_rel: A ⊆B so_apply: x[s] sq_stable: SqStable(P) nat_plus: + rless: x < y sq_exists: x:A [B[x]] int_upper: {i...} label: ...\$L... t cand: c∧ B rleq: x ≤ y rnonneg: rnonneg(x) top: Top uiff: uiff(P;Q) rev_uimplies: rev_uimplies(P;Q) req_int_terms: t1 ≡ t2 guard: {T} sq_type: SQType(T) nequal: a ≠ b ∈  assert: b bnot: ¬bb bfalse: ff ifthenelse: if then else fi  btrue: tt it: unit: Unit bool: 𝔹 real: rge: x ≥ y rev_implies:  Q iff: ⇐⇒ Q rabs: |x| less_than': less_than'(a;b) rneq: x ≠ y series-converges: Σn.x[n]↓ series-sum: Σn.x[n] a converges: x[n]↓ as n→∞ rfun-eq: rfun-eq(I;f;g) r-ap: f(x) pointwise-req: x[k] y[k] for k ∈ [n,m] subtract: m

Latex:
\mforall{}I:Interval.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  I  {}\mrightarrow{}\mBbbR{}.
((\mforall{}n:\mBbbN{}.  f[n;x]  continuous  for  x  \mmember{}  I)
{}\mRightarrow{}  (\mforall{}m:\{m:\mBbbN{}\msupplus{}|  icompact(i-approx(I;m))\}
\mexists{}c:\mBbbR{}
((r0  \mleq{}  c)
\mwedge{}  (c  <  r1)
\mwedge{}  (\mexists{}N:\mBbbN{}.  \mforall{}n:\{N...\}.  \mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  i-approx(I;m)\}  .    (|f[n  +  1;x]|  \mleq{}  (c  *  |f[n;x]|)))))
{}\mRightarrow{}  \mSigma{}n.f[n;x]\mdownarrow{}  absolutely  for  x  \mmember{}  I)

Date html generated: 2020_05_20-PM-01_06_42
Last ObjectModification: 2020_01_01-PM-02_27_21

Theory : reals

Home Index