TheoremBase

Proof

Define v:[0,T]β†’Rv:[0,T]\to\mathbb{R} by v(t)=∫0tu(s) dsv(t)=\int_0^t u(s)\,ds, with v(0)=0v(0)=0 by the stated convention. The hypothesis reads u(t)≀a+b v(t)u(t)\le a+b\,v(t) for 0≀t≀T0\le t\le T.

Case b=0b=0. By claim 1 of Basic Properties of the Exponential Function, exp⁑(0)=1\exp(0)=1, so for every t∈[0,T]t\in[0,T], u(t)≀a=a exp⁑(bt)u(t)\le a=a\,\exp(bt). Assume from now on b>0b>0.

We use repeatedly that if x≀yx\le y are real numbers and Ξ»>0\lambda>0, then Ξ»x≀λy\lambda x\le\lambda y: this is claim 10 of Elementary Order Arithmetic in an Ordered Field when x<yx<y, and immediate when x=yx=y.

Step 1: regularity of vv. Since 0<T0<T and uu is continuous on [0,T][0,T], Fundamental Theorem of Calculus, Part I, on a Closed Real Interval applies with 00 and TT as the endpoints of the closed interval there and with uu as the continuous function there. The function FF produced there is exactly vv, since both are given by tβ†¦βˆ«0tu(s) dst\mapsto\int_0^t u(s)\,ds with the same convention at t=0t=0. Claim 2 of that theorem gives that vv is continuous on [0,T][0,T], and claim 3 gives that vv is differentiable at every t∈(0,T)t\in(0,T) with vβ€²(t)=u(t)v'(t)=u(t).

Step 2: the auxiliary function decreases. Define E:Rβ†’RE:\mathbb{R}\to\mathbb{R} by E(t)=exp⁑(βˆ’bt)E(t)=\exp(-bt), and define Ο‡:[0,T]β†’R\chi:[0,T]\to\mathbb{R} by

Ο‡(t)=E(t)(ab+v(t)).\chi(t)=E(t)\Bigl(\frac{a}{b}+v(t)\Bigr).

Apply Derivative and Continuity of the Scaled Exponential Function with c=βˆ’bc=-b: claim 1 gives that EE is differentiable at every real point with Eβ€²(t)=βˆ’bexp⁑(βˆ’bt)E'(t)=-b\exp(-bt), and claim 2 gives that EE is continuous on R\mathbb{R}. Both R\mathbb{R} and [0,T][0,T] are intervals and [0,T]βŠ†R[0,T]\subseteq\mathbb{R}, so claim 1 of Restriction Stability of Continuity and of the Derivative shows that the restriction E∣[0,T]E|_{[0,T]} is continuous on [0,T][0,T], and claim 2 of that lemma shows that E∣[0,T]E|_{[0,T]} is differentiable, with the same derivative as EE, at every interior point of [0,T][0,T]. Every t∈(0,T)t\in(0,T) is such an interior point, since 0,T∈[0,T]0,T\in[0,T] and 0<t<T0<t<T.

The map on [0,T][0,T] with constant value a/ba/b is continuous on [0,T][0,T] by claim 1 of Continuity of Sums and Products of Real-Valued Functions on a Metric Space, applied at each point of [0,T][0,T]. Hence, together with Step 1, claim 5 of that theorem shows first that a/b+va/b+v is continuous on [0,T][0,T] and then that the product Ο‡=E∣[0,T]β‹…(a/b+v)\chi=E|_{[0,T]}\cdot(a/b+v) is continuous on [0,T][0,T].

Let t∈(0,T)t\in(0,T), an interior point of [0,T][0,T]. By claim 1 of Sum, Constant Multiple, and Product Rules for One-Dimensional Derivatives the function on [0,T][0,T] with constant value a/ba/b is differentiable at tt with derivative 00, so by claim 2 the function a/b+va/b+v is differentiable at tt with derivative vβ€²(t)=u(t)v'(t)=u(t) (Step 1); by claim 3 (the product rule) applied to E∣[0,T]E|_{[0,T]} and a/b+va/b+v,

Ο‡β€²(t)=βˆ’bexp⁑(βˆ’bt)(ab+v(t))+exp⁑(βˆ’bt) u(t)=exp⁑(βˆ’bt)(u(t)βˆ’aβˆ’b v(t)).\chi'(t)=-b\exp(-bt)\Bigl(\frac{a}{b}+v(t)\Bigr)+\exp(-bt)\,u(t)=\exp(-bt)\bigl(u(t)-a-b\,v(t)\bigr).

By claim 2 of Basic Properties of the Exponential Function, exp⁑(βˆ’bt)>0\exp(-bt)>0, and u(t)βˆ’aβˆ’b v(t)≀0u(t)-a-b\,v(t)\le0 by hypothesis; hence Ο‡β€²(t)≀0\chi'(t)\le0 for every t∈(0,T)t\in(0,T).

Step 3: conclusion. Fix t∈(0,T]t\in(0,T]. Since [0,t]βŠ†[0,T][0,t]\subseteq[0,T], claim 1 of Restriction Stability of Continuity and of the Derivative shows that Ο‡βˆ£[0,t]\chi|_{[0,t]} is continuous on [0,t][0,t], and claim 2 of that lemma shows that Ο‡βˆ£[0,t]\chi|_{[0,t]} is differentiable, with the same derivative as Ο‡\chi, at every interior point of [0,t][0,t]; every s∈(0,t)s\in(0,t) is such a point and lies in (0,T)(0,T), so (Ο‡βˆ£[0,t])β€²(s)=Ο‡β€²(s)≀0(\chi|_{[0,t]})'(s)=\chi'(s)\le0 by Step 2. As 0<t0<t, Mean Value Theorem on a Closed Real Interval applied to Ο‡βˆ£[0,t]\chi|_{[0,t]} on [0,t][0,t] yields ξ∈(0,t)\xi\in(0,t) with

Ο‡(t)βˆ’Ο‡(0)=Ο‡β€²(ΞΎ) (tβˆ’0).\chi(t)-\chi(0)=\chi'(\xi)\,(t-0).

Since Ο‡β€²(ΞΎ)≀0\chi'(\xi)\le0 and tβˆ’0>0t-0>0, the right-hand side is at most 00, so Ο‡(t)≀χ(0)\chi(t)\le\chi(0). Since Ο‡(0)=exp⁑(0)(a/b+v(0))=a/b\chi(0)=\exp(0)\bigl(a/b+v(0)\bigr)=a/b, using exp⁑(0)=1\exp(0)=1 and v(0)=0v(0)=0, we obtain, for every t∈[0,T]t\in[0,T] (the case t=0t=0 holding with equality),

exp⁑(βˆ’bt)(ab+v(t))≀ab.\exp(-bt)\Bigl(\frac{a}{b}+v(t)\Bigr)\le\frac{a}{b}.

By claims 1 and 2 of Basic Properties of the Exponential Function, exp⁑(bt)>0\exp(bt)>0 and exp⁑(βˆ’bt)exp⁑(bt)=exp⁑(0)=1\exp(-bt)\exp(bt)=\exp(0)=1; multiplying the last display by exp⁑(bt)\exp(bt) therefore gives

ab+v(t)≀abexp⁑(bt),\frac{a}{b}+v(t)\le\frac{a}{b}\exp(bt),

hence b v(t)≀aexp⁑(bt)βˆ’ab\,v(t)\le a\exp(bt)-a, and by the hypothesis,

u(t)≀a+b v(t)≀aexp⁑(bt)(0≀t≀T).u(t)\le a+b\,v(t)\le a\exp(bt)\qquad(0\le t\le T).

β– \blacksquare

Citations

Loading…

Dependencies

Uses0

Loading…

Comments

Log in to comment.

Loading…