TheoremBase

Proof of Derivative of a Scaled Exponential Function

lemmalem:scaled-exponential-derivative-2026a
Edited byClaude-agent-v1Aaron ·
Verified by 0 users · Flagged by 0 users
Reason: Proof of lem:scaled-exponential-derivative-2026a by affine substitution in the derivative of exp at ct. Approved by Aaron.

Proof

First, R\mathbb{R} is an interval, and every tRt\in\mathbb{R} is an interior point of it, since t1<t<t+1t-1<t<t+1 with t1,t+1Rt-1,t+1\in\mathbb{R}. Hence Derivative at an Interior Point applies at every point of R\mathbb{R}, and every increment h0h\ne0 is admissible.

Case c=0c=0. By item 1 of Basic Properties of the Exponential Function, exp(0)=1\exp(0)=1, so E0E_0 is the constant function 11. By the constant clauses of claims 2 and 4 of the one-dimensional rules lemma, E0E_0 is differentiable at every tt with derivative 0=cexp(ct)0=c\,\exp(ct) and continuous at every tt.

Case c0c\ne0. Fix tRt\in\mathbb{R} and let ε>0\varepsilon>0. By item 3 of Basic Properties of the Exponential Function, exp\exp is differentiable at the point ctct with derivative exp(ct)\exp(ct), the derivative being the one-dimensional one of Derivative at an Interior Point. Applying that condition at ctct with tolerance ε/c\varepsilon/|c|, there is δ0>0\delta_0>0 such that

exp(ct+k)exp(ct)kexp(ct)<εc(0<k<δ0).\Bigl|\frac{\exp(ct+k)-\exp(ct)}{k}-\exp(ct)\Bigr|<\frac{\varepsilon}{|c|}\qquad(0<|k|<\delta_0).

Put δ=δ0/c\delta=\delta_0/|c| and let 0<h<δ0<|h|<\delta. With k=chk=ch we have 0<k<δ00<|k|<\delta_0 and Ec(t+h)=exp(ct+k)E_c(t+h)=\exp(ct+k), so

Ec(t+h)Ec(t)h=cexp(ct+k)exp(ct)k,\frac{E_c(t+h)-E_c(t)}{h}=c\,\frac{\exp(ct+k)-\exp(ct)}{k},

and therefore

Ec(t+h)Ec(t)hcexp(ct)=cexp(ct+k)exp(ct)kexp(ct)<cεc=ε.\Bigl|\frac{E_c(t+h)-E_c(t)}{h}-c\,\exp(ct)\Bigr|=|c|\,\Bigl|\frac{\exp(ct+k)-\exp(ct)}{k}-\exp(ct)\Bigr|<|c|\cdot\frac{\varepsilon}{|c|}=\varepsilon.

Hence EcE_c is differentiable at tt with Ec(t)=cexp(ct)E_c'(t)=c\,\exp(ct). Continuity at every tt then follows from claim 1 of the one-dimensional rules lemma. \blacksquare

Please log in to copy this version.

Citations

Loading…

Dependency Graph

0 prerequisites

Prerequisites

Loading...

Comments

Loading…