Nuprl Lemma : Taylor-series-converges

a:ℝ. ∀t:{t:ℝr0 < t} . ∀F:ℕ ⟶ (a t, t) ⟶ℝ.
  ((∀k:ℕ. ∀x,y:{x:ℝx ∈ (a t, t)} .  ((x y)  (F[k;x] F[k;y])))
   infinite-deriv-seq((a t, t);i,x.F[i;x])
   (∀r:{r:ℝ(r0 ≤ r) ∧ (r < t)} lim k→∞.r^k (F[k 1;x]/r((k)!)) = λx.r0 for x ∈ (a t, t))
   lim k→∞{(F[i;a]/r((i)!)) a^i 0≤i≤k} = λx.F[0;x] for x ∈ (a t, t))


Proof




Definitions occuring in Statement :  infinite-deriv-seq: infinite-deriv-seq(I;i,x.F[i; x]) fun-converges-to: lim n→∞.f[n; x] = λy.g[y] for x ∈ I rfun: I ⟶ℝ rooint: (l, u) i-member: r ∈ I rsum: Σ{x[k] n≤k≤m} rdiv: (x/y) rleq: x ≤ y rless: x < y rnexp: x^k1 rsub: y req: y rmul: b radd: b int-to-real: r(n) real: fact: (n)! nat: so_apply: x[s1;s2] all: 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 :  all: x:A. B[x] implies:  Q fun-converges-to: lim n→∞.f[n; x] = λy.g[y] for x ∈ I member: t ∈ T uall: [x:A]. B[x] prop: and: P ∧ Q so_lambda: λ2y.t[x; y] label: ...$L... t rfun: I ⟶ℝ so_apply: x[s1;s2] nat: ge: i ≥  decidable: Dec(P) or: P ∨ Q uimplies: supposing a not: ¬A satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False top: Top subtype_rel: A ⊆B nat_plus: + iff: ⇐⇒ Q rev_implies:  Q so_lambda: λ2x.t[x] so_apply: x[s] sq_stable: SqStable(P) squash: T iproper: iproper(I) right-endpoint: right-endpoint(I) left-endpoint: left-endpoint(I) i-finite: i-finite(I) rooint: (l, u) isl: isl(x) assert: b ifthenelse: if then else fi  btrue: tt endpoints: endpoints(I) outl: outl(x) pi1: fst(t) pi2: snd(t) less_than: a < b less_than': less_than'(a;b) true: True uiff: uiff(P;Q) req_int_terms: t1 ≡ t2 subtract: m le: A ≤ B icompact: icompact(I) i-nonvoid: i-nonvoid(I) i-member: r ∈ I i-approx: i-approx(I;n) rccint: [l, u] rneq: x ≠ y guard: {T} cand: c∧ B rless: x < y sq_exists: x:A [B[x]] rev_uimplies: rev_uimplies(P;Q) rge: x ≥ y rdiv: (x/y) int_upper: {i...} subinterval: I ⊆  int_seg: {i..j-} lelt: i ≤ j < k finite-deriv-seq: finite-deriv-seq(I;k;i,x.F[i; x]) infinite-deriv-seq: infinite-deriv-seq(I;i,x.F[i; x]) Taylor-remainder: Taylor-remainder(I;n;b;a;i,x.F[i; x]) Taylor-approx: Taylor-approx(n;a;b;i,x.F[i; x])
Lemmas referenced :  nat_plus_wf icompact_wf i-approx_wf rooint_wf rsub_wf radd_wf rleq_wf int-to-real_wf rless_wf fun-converges-to_wf rmul_wf rnexp_wf rdiv_wf nat_properties decidable__le full-omega-unsat intformand_wf intformnot_wf intformle_wf itermConstant_wf itermAdd_wf itermVar_wf istype-int int_formula_prop_and_lemma istype-void int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_add_lemma int_term_value_var_lemma int_formula_prop_wf istype-le fact_wf rneq-int fact-non-zero i-member_wf istype-nat infinite-deriv-seq_wf subtype_rel_self real_wf req_wf rfun_wf iproper-approx sq_stable__icompact radd-preserves-rless true_wf itermSubtract_wf itermMultiply_wf sq_stable__rless rmul_preserves_rless rless-int rless_functionality req-iff-rsub-is-0 real_polynomial_null real_term_value_sub_lemma real_term_value_add_lemma real_term_value_var_lemma real_term_value_const_lemma real_term_value_mul_lemma decidable__lt istype-false not-lt-2 less-iff-le condition-implies-le minus-add minus-one-mul zero-add minus-one-mul-top add-commutes add_functionality_wrt_le add-associates add-zero le-add-cancel istype-less_than iproper_wf nat_plus_properties intformless_wf int_formula_prop_less_lemma trivial-rsub-rless intformeq_wf int_formula_prop_eq_lemma set_subtype_base less_than_wf int_subtype_base rless-int-fractions2 int_term_value_mul_lemma member_rccint_lemma rleq_transitivity rminus_wf radd-preserves-rleq itermMinus_wf rmul_preserves_rleq iff_weakening_uiff rleq_functionality req_weakening real_term_value_minus_lemma r-bound_wf rccint_wf rabs_wf sq_stable__rleq rabs-difference-bound-rleq rleq_functionality_wrt_implies rleq_weakening_equal r-bound-property trivial-rleq-radd rleq-int-fractions2 rsub_functionality_wrt_rleq radd_functionality_wrt_rleq rinv_wf2 req_transitivity rinv-as-rdiv mul_nat_plus i-approx-is-subinterval istype-int_upper rsum_wf int_seg_subtype_nat member_rooint_lemma trivial-rless-radd rless-implies-rless int_seg_wf subtype_rel_sets_simple int_upper_properties rleq-implies-rleq Taylor-theorem less_than_transitivity1 subtype_rel_dep_function nat_wf int_seg_properties rfun_subtype derivative_functionality_wrt_subinterval rcc-subinterval rmin_wf rmax_wf i-member-iff rmin-i-member rmax-i-member Taylor-remainder_wf upper_subtype_nat sq_stable__le le_weakening2 rmin_ub rmax_lb mul_bounds_1b req_functionality rabs_functionality req-int-fractions decidable__equal_int rabs-rmul-rleq rmul_comm rmul-int-rdiv rnexp-rleq zero-rleq-rabs rabs-rnexp rsub_functionality rabs-of-nonneg radd_functionality trivial-rsub-rleq rabs-rmul rleq-int-fractions uimplies_transitivity rdiv_functionality radd-int radd-rdiv r-triangle-inequality rabs-difference-symmetry i-approx-monotonic i-member-approx
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt setElimination thin rename setIsType universeIsType cut introduction extract_by_obid hypothesis sqequalHypSubstitution isectElimination hypothesisEquality because_Cache sqequalRule functionIsType inhabitedIsType productIsType natural_numberEquality lambdaEquality_alt applyEquality dependent_set_memberEquality_alt addEquality dependent_functionElimination unionElimination independent_isectElimination approximateComputation independent_functionElimination dependent_pairFormation_alt int_eqEquality isect_memberEquality_alt voidElimination independent_pairFormation equalityTransitivity equalitySymmetry productElimination functionEquality setEquality imageMemberEquality baseClosed imageElimination closedConclusion minusEquality equalityIsType1 inrFormation_alt equalityIsType4 intEquality multiplyEquality promote_hyp productEquality applyLambdaEquality baseApply

Latex:
\mforall{}a:\mBbbR{}.  \mforall{}t:\{t:\mBbbR{}|  r0  <  t\}  .  \mforall{}F:\mBbbN{}  {}\mrightarrow{}  (a  -  t,  a  +  t)  {}\mrightarrow{}\mBbbR{}.
    ((\mforall{}k:\mBbbN{}.  \mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  (a  -  t,  a  +  t)\}  .    ((x  =  y)  {}\mRightarrow{}  (F[k;x]  =  F[k;y])))
    {}\mRightarrow{}  infinite-deriv-seq((a  -  t,  a  +  t);i,x.F[i;x])
    {}\mRightarrow{}  (\mforall{}r:\{r:\mBbbR{}|  (r0  \mleq{}  r)  \mwedge{}  (r  <  t)\} 
                lim  k\mrightarrow{}\minfty{}.r\^{}k  *  (F[k  +  1;x]/r((k)!))  =  \mlambda{}x.r0  for  x  \mmember{}  (a  -  t,  a  +  t))
    {}\mRightarrow{}  lim  k\mrightarrow{}\minfty{}.\mSigma{}\{(F[i;a]/r((i)!))  *  x  -  a\^{}i  |  0\mleq{}i\mleq{}k\}  =  \mlambda{}x.F[0;x]  for  x  \mmember{}  (a  -  t,  a  +  t))



Date html generated: 2019_10_30-AM-10_11_33
Last ObjectModification: 2018_11_14-AM-11_40_16

Theory : reals


Home Index