---

Step * of Lemma approx-arg-interval_wf

∀l:ℝ. ∀r:{r:ℝ| l < r} . ∀f,f':[l, r] ⟶ℝ.
  ((∀x,y:{t:ℝ| t ∈ [l, r]} .  ((x = y) ⇒ (f'[x] = f'[y])))
  ⇒ d(f[x])/dx = λx.f'[x] on [l, r]
  ⇒ (∀B:ℕ
        ((∀x:{x:ℝ| x ∈ [l, r]} . (|f'[x]| ≤ r(B)))
        ⇒ (∀x:{x:ℝ| x ∈ [l, r]} . (approx-arg-interval(f;l;r;B;x) ∈ {y:ℝ| y = (f x)} )))))
BY
{ (RepeatFor 2 ((D 0 THENA Auto))
   THEN (InstLemma `mean-value-for-bounded-derivative` [⌜[l, r]⌝]⋅ THENA (Auto THEN RepUR ``iproper`` 0 THEN Auto))
   THEN RepeatFor 4 ((ParallelLast' THENA Auto))
   THEN (D 0 THENA Auto)
   THEN (D -2 With ⌜r(B)⌝  THENA Auto)
   THEN ParallelLast'
   THEN Auto
   THEN Unfold `approx-arg-interval` 0) }

1
1. l : ℝ
2. r : {r:ℝ| l < r} 
3. f : [l, r] ⟶ℝ
4. f' : [l, r] ⟶ℝ
5. ∀x,y:{t:ℝ| t ∈ [l, r]} .  ((x = y) ⇒ (f'[x] = f'[y]))
6. d(f[x])/dx = λx.f'[x] on [l, r]
7. B : ℕ
8. ∀x:{x:ℝ| x ∈ [l, r]} . (|f'[x]| ≤ r(B))
9. ∀x,y:{x:ℝ| x ∈ [l, r]} .  (|f[x] - f[y]| ≤ (r(B) * |x - y|))
10. x : {x:ℝ| x ∈ [l, r]} 
⊢ accelerate(1 + (2 * B);λn.eval a = x n in
                            eval m = 2 * n in
                            eval x' = if (a * 2) < ((l m) + 2)
                                         then l
                                         else if ((r m) - 2) < (a * 2)  then r  else (r(a))/m in
                              f x' n) ∈ {y:ℝ| y = (f x)} 

---

Latex:

---

Latex:
\mforall{}l:\mBbbR{}.  \mforall{}r:\{r:\mBbbR{}|  l  <  r\}  .  \mforall{}f,f':[l,  r]  {}\mrightarrow{}\mBbbR{}.
    ((\mforall{}x,y:\{t:\mBbbR{}|  t  \mmember{}  [l,  r]\}  .    ((x  =  y)  {}\mRightarrow{}  (f'[x]  =  f'[y])))
    {}\mRightarrow{}  d(f[x])/dx  =  \mlambda{}x.f'[x]  on  [l,  r]
    {}\mRightarrow{}  (\mforall{}B:\mBbbN{}
                ((\mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  [l,  r]\}  .  (|f'[x]|  \mleq{}  r(B)))
                {}\mRightarrow{}  (\mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  [l,  r]\}  .  (approx-arg-interval(f;l;r;B;x)  \mmember{}  \{y:\mBbbR{}|  y  =  (f  x)\}  )))))


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))
  THEN  (InstLemma  `mean-value-for-bounded-derivative`  [\mkleeneopen{}[l,  r]\mkleeneclose{}]\mcdot{}
              THENA  (Auto  THEN  RepUR  ``iproper``  0  THEN  Auto)
              )
  THEN  RepeatFor  4  ((ParallelLast'  THENA  Auto))
  THEN  (D  0  THENA  Auto)
  THEN  (D  -2  With  \mkleeneopen{}r(B)\mkleeneclose{}    THENA  Auto)
  THEN  ParallelLast'
  THEN  Auto
  THEN  Unfold  `approx-arg-interval`  0)

---

Home Index