Nuprl Lemma : power-series-converges-everywhere

∀a:ℕ ⟶ ℝ. ∀g:ℝ ⟶ ℝ.
  ((∀x:ℝ. Σi.a[i] * x^i = g[x])
  ⇒ (∀r:{r:ℝ| r0 < r} . ∃N:ℕ. ∀n:{N...}. (|a[n + 1]| ≤ (|a[n]|/r)))
  ⇒ lim n→∞.Σ{a[i] * x^i | 0≤i≤n} = λx.g[x] for x ∈ (-∞, ∞))

Proof

Error : references

Latex:
\mforall{}a:\mBbbN{} {}\mrightarrow{} \mBbbR{}. \mforall{}g:\mBbbR{} {}\mrightarrow{} \mBbbR{}. ((\mforall{}x:\mBbbR{}. \mSigma{}i.a[i] * x\^{}i = g[x]) {}\mRightarrow{} (\mforall{}r:\{r:\mBbbR{}| r0 < r\} . \mexists{}N:\mBbbN{}. \mforall{}n:\{N...\}. (|a[n + 1]| \mleq{} (|a[n]|/r))) {}\mRightarrow{} lim n\mrightarrow{}\minfty{}.\mSigma{}\{a[i] * x\^{}i | 0\mleq{}i\mleq{}n\} = \mlambda{}x.g[x] for x \mmember{} (-\minfty{}, \minfty{})) Date html generated: 2020_05_21-AM-10_28_21 Last ObjectModification: 2020_01_07-PM-03_00_17 Theory : reals Home Index