Proof of Nuprl Lemma : integral-from-Taylor

Step * of Lemma integral-from-Taylor

∀a:ℝ. ∀t:{t:ℝ| r0 < t} . ∀F:ℕ ⟶ (a - t, a + t) ⟶ℝ.
  ((∀k:ℕ. ∀x,y:{x:ℝ| x ∈ (a - t, a + t)} .  ((x = y) ⇒ (F[k;x] = F[k;y])))
  ⇒ infinite-deriv-seq((a - t, a + 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, a + t))

⇒ (∀b:{b:ℝ| b ∈ (a - t, a + t)}

        lim n→∞.Σ{(F[i;a]/r((i)!)) * (x - a^i + 1 - b - a^i + 1/r(i + 1)) | 0≤i≤n} = λx.b_∫^-x F[0;t] dt for x ∈ (a

        - t, a + t)))
BY
{ (InstLemma `integral-from-Taylor-1` []
   THEN RepeatFor 7 ((ParallelLast' THENA Auto))
   THEN (InstLemma `fun-converges-to_functionality` [⌜(a - t, a + t)⌝;

         ⌜λ₂n x.b_∫^-x Σ{(F[i;a]/r((i)!)) * t - a^i | 0≤i≤n} dt⌝;⌜λ₂n x.Σ{(F[i;a]/r((i)!))

                                                                 * (x - a^i + 1 - b - a^i + 1/r(i + 1)) | 0≤i≤n}⌝;

         ⌜λ₂x.b_∫^-x F[0;t] dt⌝]⋅
         THENA Auto
         )
   THEN Try (((Assert [rmin(b;x), rmax(b;x)] ⊆ (a - t, a + t)  BY EAuto 2) THEN Auto))) }

1
1. a : ℝ
2. t : {t:ℝ| r0 < t}
3. F : ℕ ⟶ (a - t, a + t) ⟶ℝ
4. ∀k:ℕ. ∀x,y:{x:ℝ| x ∈ (a - t, a + t)} .  ((x = y) ⇒ (F[k;x] = F[k;y]))
5. infinite-deriv-seq((a - t, a + t);i,x.F[i;x])

6. ∀r:{r:ℝ| (r0 ≤ r) ∧ (r < t)} . lim k→∞.r^k * (F[k + 1;x]/r((k)!)) = λx.r0 for x ∈ (a - t, a + t)

7. b : {b:ℝ| b ∈ (a - t, a + t)}

8. lim n→∞.b_∫^-x Σ{(F[i;a]/r((i)!)) * t - a^i | 0≤i≤n} dt = λx.b_∫^-x F[0;t] dt for x ∈ (a - t, a + t)

9. n : ℕ
10. x : {x:ℝ| x ∈ (a - t, a + t)}
11. [rmin(b;x), rmax(b;x)] ⊆ (a - t, a + t)

⊢ b_∫^-x Σ{(F[i;a]/r((i)!)) * t - a^i | 0≤i≤n} dt = Σ{(F[i;a]/r((i)!)) * (x - a^i + 1 - b - a^i + 1/r(i + 1)) | 0≤i≤n}

2
1. a : ℝ
2. t : {t:ℝ| r0 < t}
3. F : ℕ ⟶ (a - t, a + t) ⟶ℝ
4. ∀k:ℕ. ∀x,y:{x:ℝ| x ∈ (a - t, a + t)} . ((x = y) ⇒ (F[k;x] = F[k;y]))
5. infinite-deriv-seq((a - t, a + t);i,x.F[i;x])

6. ∀r:{r:ℝ| (r0 ≤ r) ∧ (r < t)} . lim k→∞.r^k * (F[k + 1;x]/r((k)!)) = λx.r0 for x ∈ (a - t, a + t)

7. b : {b:ℝ| b ∈ (a - t, a + t)}

8. lim n→∞.b_∫^-x Σ{(F[i;a]/r((i)!)) * t - a^i | 0≤i≤n} dt = λx.b_∫^-x F[0;t] dt for x ∈ (a - t, a + t)

9. lim n→∞.b_∫^-x Σ{(F[i;a]/r((i)!)) * t - a^i | 0≤i≤n} dt = λy.b_∫^-y F[0;t] dt for x ∈ (a - t, a + t)

⇒

 lim n→∞.Σ{(F[i;a]/r((i)!)) * (x - a^i + 1 - b - a^i + 1/r(i + 1)) | 0≤i≤n} = λy.b_∫^-y F[0;t] dt for x ∈ (a - t, a

+ t)

⊢ lim n→∞.Σ{(F[i;a]/r((i)!)) * (x - a^i + 1 - b - a^i + 1/r(i + 1)) | 0≤i≤n} = λx.b_∫^-x F[0;t] dt for x ∈ (a - t, a + t)

Latex:

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{} (\mforall{}b:\{b:\mBbbR{}| b \mmember{} (a - t, a + t)\} lim n\mrightarrow{}\minfty{}.\mSigma{}\{(F[i;a]/r((i)!)) * (x - a\^{}i + 1 - b - a\^{}i + 1/r(i + 1)) | 0\mleq{}i\mleq{}n\} = \mlambda{}x.b\_\mint{}\msupminus{}x F[0;t] dt for x \mmember{} (a - t, a + t))) By Latex: (InstLemma `integral-from-Taylor-1` [] THEN RepeatFor 7 ((ParallelLast' THENA Auto)) THEN (InstLemma `fun-converges-to\_functionality` [\mkleeneopen{}(a - t, a + t)\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}n x.b\_\mint{}\msupminus{}x \mSigma{}\{(F[i;a]/r((i)!)) * t - a\^{}i | 0\mleq{}i\mleq{}n\} dt\mkleeneclose{}; \mkleeneopen{}\mlambda{}\msubtwo{}n x.\mSigma{}\{(F[i;a]/r((i)!)) * (x - a\^{}i + 1 - b - a\^{}i + 1/r(i + 1)) | 0\mleq{}i\mleq{}n\}\mkleeneclose{}; \mkleeneopen{}\mlambda{}\msubtwo{}x.b\_\mint{}\msupminus{}x F[0;t] dt\mkleeneclose{}]\mcdot{} THENA Auto ) THEN Try (((Assert [rmin(b;x), rmax(b;x)] \msubseteq{} (a - t, a + t) BY EAuto 2) THEN Auto))) Home Index