---

Step * of Lemma integral-by-parts

∀I:Interval. ∀u,v,u',v':{h:I ⟶ℝ| ∀x,y:{t:ℝ| t ∈ I} .  ((x = y) ⇒ ((h x) = (h y)))} .
  (d(u[t])/dt = λt.u'[t] on I
  ⇒ d(v[t])/dt = λt.v'[t] on I
  ⇒ iproper(I)
  ⇒ (∀a,b:{a:ℝ| a ∈ I} .  (a_∫-b u[t] * v'[t] dt = ((u[b] * v[b]) - u[a] * v[a] - a_∫-b u'[t] * v[t] dt))))
BY
{ (InstLemma `integration-by-parts` []
   THEN RepeatFor 3 ((ParallelLast' THENA Auto))
   THEN Auto
   THEN Assert ⌜∀x:{x:ℝ| x ∈ I} . (λt.(u'[t] * v[t]) ∈ {f:[rmin(a;x), rmax(a;x)] ⟶ℝ| ifun(f;[rmin(a;x), rmax(a;x)])} )⌝\000C⋅) }

1
.....assertion..... 
1. I : Interval
2. u : {h:I ⟶ℝ| ∀x,y:{t:ℝ| t ∈ I} .  ((x = y) ⇒ ((h x) = (h y)))} 
3. v : {h:I ⟶ℝ| ∀x,y:{t:ℝ| t ∈ I} .  ((x = y) ⇒ ((h x) = (h y)))} 
4. ∀h:I ⟶ℝ. ∀u',v':{h:I ⟶ℝ| ∀x,y:{t:ℝ| t ∈ I} .  ((x = y) ⇒ ((h x) = (h y)))} .
     (d(u[t])/dt = λt.u'[t] on I
     ⇒ d(v[t])/dt = λt.v'[t] on I
     ⇒ d(h[t])/dt = λt.u'[t] * v[t] on I
     ⇒ d((u[t] * v[t]) - h[t])/dt = λt.u[t] * v'[t] on I)
5. u' : {h:I ⟶ℝ| ∀x,y:{t:ℝ| t ∈ I} .  ((x = y) ⇒ ((h x) = (h y)))} 
6. v' : {h:I ⟶ℝ| ∀x,y:{t:ℝ| t ∈ I} .  ((x = y) ⇒ ((h x) = (h y)))} 
7. d(u[t])/dt = λt.u'[t] on I
8. d(v[t])/dt = λt.v'[t] on I
9. iproper(I)
10. a : {a:ℝ| a ∈ I} 
11. b : {a:ℝ| a ∈ I} 
⊢ ∀x:{x:ℝ| x ∈ I} . (λt.(u'[t] * v[t]) ∈ {f:[rmin(a;x), rmax(a;x)] ⟶ℝ| ifun(f;[rmin(a;x), rmax(a;x)])} )

2
1. I : Interval
2. u : {h:I ⟶ℝ| ∀x,y:{t:ℝ| t ∈ I} .  ((x = y) ⇒ ((h x) = (h y)))} 
3. v : {h:I ⟶ℝ| ∀x,y:{t:ℝ| t ∈ I} .  ((x = y) ⇒ ((h x) = (h y)))} 
4. ∀h:I ⟶ℝ. ∀u',v':{h:I ⟶ℝ| ∀x,y:{t:ℝ| t ∈ I} .  ((x = y) ⇒ ((h x) = (h y)))} .
     (d(u[t])/dt = λt.u'[t] on I
     ⇒ d(v[t])/dt = λt.v'[t] on I
     ⇒ d(h[t])/dt = λt.u'[t] * v[t] on I
     ⇒ d((u[t] * v[t]) - h[t])/dt = λt.u[t] * v'[t] on I)
5. u' : {h:I ⟶ℝ| ∀x,y:{t:ℝ| t ∈ I} .  ((x = y) ⇒ ((h x) = (h y)))} 
6. v' : {h:I ⟶ℝ| ∀x,y:{t:ℝ| t ∈ I} .  ((x = y) ⇒ ((h x) = (h y)))} 
7. d(u[t])/dt = λt.u'[t] on I
8. d(v[t])/dt = λt.v'[t] on I
9. iproper(I)
10. a : {a:ℝ| a ∈ I} 
11. b : {a:ℝ| a ∈ I} 
12. ∀x:{x:ℝ| x ∈ I} . (λt.(u'[t] * v[t]) ∈ {f:[rmin(a;x), rmax(a;x)] ⟶ℝ| ifun(f;[rmin(a;x), rmax(a;x)])} )
⊢ a_∫-b u[t] * v'[t] dt = ((u[b] * v[b]) - u[a] * v[a] - a_∫-b u'[t] * v[t] dt)

---

Latex:

---

Latex:
\mforall{}I:Interval.  \mforall{}u,v,u',v':\{h:I  {}\mrightarrow{}\mBbbR{}|  \mforall{}x,y:\{t:\mBbbR{}|  t  \mmember{}  I\}  .    ((x  =  y)  {}\mRightarrow{}  ((h  x)  =  (h  y)))\}  .
    (d(u[t])/dt  =  \mlambda{}t.u'[t]  on  I
    {}\mRightarrow{}  d(v[t])/dt  =  \mlambda{}t.v'[t]  on  I
    {}\mRightarrow{}  iproper(I)
    {}\mRightarrow{}  (\mforall{}a,b:\{a:\mBbbR{}|  a  \mmember{}  I\}  .
                (a\_\mint{}\msupminus{}b  u[t]  *  v'[t]  dt  =  ((u[b]  *  v[b])  -  u[a]  *  v[a]  -  a\_\mint{}\msupminus{}b  u'[t]  *  v[t]  dt))))


By

---

Latex:
(InstLemma  `integration-by-parts`  []
  THEN  RepeatFor  3  ((ParallelLast'  THENA  Auto))
  THEN  Auto
  THEN  Assert  \mkleeneopen{}\mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  I\} 
                                (\mlambda{}t.(u'[t]  *  v[t])  \mmember{}  \{f:[rmin(a;x),  rmax(a;x)]  {}\mrightarrow{}\mBbbR{}|  ifun(f;[rmin(a;x),  rmax(a;x)])\}  \000C)\mkleeneclose{}\mcdot{})

---

Home Index