Derivative rules: checking the product and chain rules against differentiating the expansion

Goal and scope

With the ascending coefficient lists f=[2,0,1] and g=[1,3] (that is f(x)=2+x² and g(x)=1+3x): first prove from the definition of the derivative the differentiation formula for polynomials of degree at most three; then find (fg)' and (f∘g)' along two independent routes, differentiating the expansion and applying the product and chain rules, and confirm they agree at every x; also check the sum and scalar rules, expose the errors f'g', a missing inner derivative, an outer derivative at the wrong point and reversed coefficient reading, and evaluate at x=1.

Stays within the MKO's polynomial slice (inputs of degree at most three, ascending lists). The sum, scalar, product and chain rules themselves are cited from the MKO; this guide only checks them for this f and g as polynomial identities and proves from the definition the derivative formula for polynomials of degree at most three; it does not prove the rules for general differentiable functions. It does not change the canonical MKO or its English edition.

Givens and symbols

• distributive
• power_laws
• abs_rules
• order_basics
• frac_rules
• composition_def
• numeric_evaluation

• G1 — Polynomials are ascending coefficient lists: [a0,a1,a2,a3] means a0+a1x+a2x²+a3x³; trailing zeros are normalized; the domain is all of ℝ.
• G2 — f=[2,0,1], g=[1,3].
• G3 — Scalar c=−4; evaluation point x=1.

• [a_0,a_1,a_2,a_3] — the ascending coefficient list for a0+a1x+a2x²+a3x³
• f',\ g' — the derivatives of f and g
• fg,\ f\circ g — the product and the composition f(g(x))
• R,\ M — the remainder of the quotient and its bound

Rules and sources

• distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu.
• power_laws · prerequisite — Integer exponent laws (base nonzero, or exponents positive integers): a^m·a^n=a^{m+n}, (a^m)^n=a^{mn}, (ab)^n=a^n b^n, a^0=1.
• abs_rules · prerequisite — Absolute value (reals): |u|=u if u≥0 and |u|=−u if u<0; |u|≥0; |uv|=|u||v|; triangle inequality |u+v|≤|u|+|v|; |u|<r ⇔ −r<u<r.
• order_basics · prerequisite — Order of the reals: exactly one of u<v, u=v, u>v holds; u<v and v<w give u<w; u<v gives u+w<v+w; u<v and w>0 give uw<vw; u<v and w<0 give uw>vw.
• frac_rules · prerequisite — Fraction rules (all denominators nonzero): a/c+b/c=(a+b)/c; (a/b)(c/d)=(ac)/(bd); (a/b)/(c/d)=(ad)/(bc) (also needing c≠0); a/b=(ak)/(bk) for k≠0.
• composition_def · prerequisite — Composition: for f:A→B and g:B→C, g∘f:A→C is defined by (g∘f)(a)=g(f(a)).
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• def_unfold · prerequisite — Unfolding a definition: replacing a defined term by its definition (or folding it back) does not change whether a statement is true.
• add_inverse · prerequisite — Additive inverse: every u has −u with u+(−u)=0; u−v means u+(−v).
• mul_inverse_nonzero · prerequisite — Inverse of a nonzero number: in ℚ, ℝ or ℂ, if u≠0 there is 1/u with u·(1/u)=1, and v/u means v·(1/u). 0 has no inverse, so v/0 is undefined.
• forall_intro · prerequisite — ∀-introduction (generalization): if a statement is proved for an arbitrary element x, with no extra assumption on x, it holds for every x in the domain.
• mul_comm · prerequisite — Commutativity of multiplication: uv=vu (in commutative number systems such as ℤ, ℚ, ℝ, ℂ).
• eq_refl_symm_trans · prerequisite — Properties of equality: u=u; if u=v then v=u; if u=v and v=w then u=w.
• quantifier_negation · prerequisite — Negating quantifiers: ¬(∀x, P(x)) is equivalent to ∃x, ¬P(x), and ¬(∃x, P(x)) is equivalent to ∀x, ¬P(x).
• mko_deriv_rules · cited — For real functions differentiable at the relevant points, (f+g)'=f'+g', (cf)'=cf' and (fg)'=f'g+fg'; if g is differentiable at x and f at g(x), then (f∘g)'(x)=f'(g(x))g'(x). Here f and g are polynomials defined on all of ℝ given by ascending coefficient lists starting with the constant term. · mko-derivative-rules
• mko_derivative_def · cited — For f:ℝ→ℝ, the derivative at x is lim_(h→0,h≠0)(f(x+h)−f(x))/h when this finite two-sided limit exists. · mko-derivative
• L_poly_deriv3 · lemma — For p(x)=c0+c1x+c2x²+c3x³ with real coefficients and every real x: p is differentiable at x and p'(x)=c1+2c2x+3c3x²; that is, the list [c0,c1,c2,c3] has derivative list [c1,2c2,3c3].

Main derivation

[a_0,a_1,a_2,a_3]

a_0+a_1x+a_2x^2+a_3x^3

f=[2,0,1],\ g=[1,3]

f(x)=2+x^2,\ g(x)=1+3x

p(x)=c_0+c_1x+c_2x^2+c_3x^3

p'(x)=c_1+2c_2x+3c_3x^2\ (\forall x\in\mathbb{R})

f=[2,0,1],\ g=[1,3]

f'(x)=2x\ ([0,2]),\quad g'(x)=3\ ([3])

f(x)g(x)=(2+x^2)(1+3x)

2+6x+x^2+3x^3\ \to\ [2,6,1,3]

[2,6,1,3]

(fg)'(x)=6+2x+9x^2\ \to\ [6,2,9]

f'(x)g(x)+f(x)g'(x)

2x(1+3x)+(2+x^2)\cdot 3=6+2x+9x^2=(fg)'(x)

f'(x)g'(x)

2x\cdot 3=6x;\ x=0:\ 0\neq 6=(fg)'(0)

(f\circ g)(x)=f(1+3x)

2+(1+3x)^2=3+6x+9x^2\ \to\ [3,6,9]

[3,6,9]

(f\circ g)'(x)=6+18x\ \to\ [6,18]

f'(g(x))\,g'(x)

2(1+3x)\cdot 3=6+18x=(f\circ g)'(x)

f'(x)g'(x),\ f'(g(x))

6x,\ 2+6x;\ x=0:\ 0\neq 6,\ 2\neq 6

f+g=[3,3,1],\ -4f=[-8,0,-4]

(f+g)'=[3,2]=[0,2]+[3],\ (-4f)'=[0,-8]=-4\cdot[0,2]

(fg)'(1),\ (f\circ g)'(1)

6+2+9=17,\ 6+18=24

Substeps and lemmas

(x+h)^2-x^2,\ (x+h)^3-x^3

h(2x+h),\ h(3x^2+3xh+h^2)

\frac{p(x+h)-p(x)}{h}\ (h\neq 0)

(c_1+2c_2x+3c_3x^2)+h\,R,\quad R=c_2+c_3(3x+h)

0<|h|\le 1

|R|\le M=|c_2|+|c_3|(3|x|+1)

\varepsilon>0,\ \delta=\min\left(1,\tfrac{\varepsilon}{M+1}\right)

0<|h|<\delta\Rightarrow|h||R|\le|h|M<\delta(M+1)\le\varepsilon;\ p'(x)=D

Reverse audits

• S14 · inverse_equivalence · numeric_evaluation — Exact evaluation.
• S13 · premise_audit · S03, S04, mko_deriv_rules — The two routes are compared; the general sum and scalar rules are not proved.
• S12 · premise_audit · S04, S10, quantifier_negation — Each wrong formula is refuted by a one-point counterexample.
• S11 · premise_audit · S04, S10, mko_deriv_rules — Hypotheses: g differentiable at x and f at g(x); S04 gives differentiability everywhere for both.
• S10 · premise_audit · S09, S03 — No chain rule is used.
• S09 · inverse_equivalence · composition_def, distributive — Substitution by definition and expansion are equalities, valid both ways.
• S08 · premise_audit · S04, S06, quantifier_negation — One counterexample refutes equality of the two functions.
• S07 · premise_audit · S04, S06, mko_deriv_rules — The rule's hypothesis (f and g differentiable at x) comes from S04; agreement is verified for this f and g only and does not prove the product rule in general.
• S06 · premise_audit · S05, S03 — No product rule is used, only the lemma of S03.
• S05 · inverse_equivalence · distributive — An identity, valid both ways.
• S04 · premise_audit · S02, S03 — A direct substitution into the lemma.
• S03.4 · premise_audit · S03.2, S03.3, mko_derivative_def, forall_intro — M+1 is used instead of M to avoid dividing by 0 when M=0; strictness comes from |h|<δ.
• S03.3 · premise_audit · abs_rules, order_basics — Only an upper bound; it needs |h|≤1, which S03.4 ensures through δ≤1.
• S03.2 · inverse_equivalence · frac_rules, distributive — For h≠0, multiplying and dividing by h undo each other.
• S03.1 · inverse_equivalence · distributive, power_laws — Identities, valid both ways.
• S03 · premise_audit · L_poly_deriv3, mko_derivative_def — The lemma covers degree at most three only; every polynomial differentiated in this guide is in that range.
• S02 · inverse_equivalence · def_unfold — Reading the polynomials back into ascending lists returns the original lists, so it holds both ways.
• S01 · premise_audit · G1, mko_deriv_rules — This step only fixes the reading convention.

Error controls and negative controls

The derivative of a product is not the product of derivatives

One misconception the MKO lists is multiplying the two derivatives. f'g'=6x while (fg)'=6+2x+9x²; at x=0, 0≠6 (S08). The correct form is f'g+fg' (S07), which agrees with differentiating the expansion (S06).

Chain rule: outer derivative at g(x), times the inner derivative

Two more misconceptions: evaluating the outer derivative at x gives 6x, and omitting the inner derivative gives 2+6x (S12); both differ from the correct 6+18x. If the inner function is constant, for example g=[5], then f∘g is the constant f(5)=27 with derivative 0, and the chain rule also gives f'(5)·0=0; this zero result must be kept.

Coefficient lists are ascending

Reading [2,0,1] backwards as 2x²+1 gives the derivative 4x instead of 2x, and this changes the input polynomial and can invalidate later formulas or values; accidental agreement at a test point does not validate the reversed convention. Appending a trailing zero ([2,0,1,0]) gives the same polynomial, not a new exercise; products and compositions may raise the degree, and new terms may not be truncated (S05).

• (fg)'=f'g'=6x → reject — (fg)'=6+2x+9x²; at x=0, 6≠0.
• (f∘g)'(x)=f'(x)g'(x)=6x → reject — The outer derivative must be evaluated at g(x); the correct result is 6+18x.
• (f∘g)'(x)=f'(g(x))=2+6x → reject — The inner derivative g'(x)=3 is missing.
• [2,0,1] means 2x²+0x+1 → reject — Lists are ascending: [2,0,1]=2+x².
• f is quadratic and g has degree one, so (fg)' has degree at most one and the x² term can be dropped → reject — fg has degree three and (fg)'=6+2x+9x² has degree two; new terms may not be truncated.

Result and limitations

f=[2,0,1]=2+x² and g=[1,3]=1+3x, with f'=2x and g'=3. fg=[2,6,1,3] and (fg)'=[6,2,9]=6+2x+9x², the same as f'g+fg' at every x; f'g'=6x is wrong. f∘g=[3,6,9] and (f∘g)'=[6,18]=6+18x, the same as f'(g(x))g'(x)=2(1+3x)·3; both f'(x)g'(x)=6x and f'(g(x))=2+6x are wrong. (f+g)'=[3,2] and (−4f)'=[0,−8]. At x=1: (fg)'(1)=17 and (f∘g)'(1)=24.

• The sum, scalar, product and chain rules are cited from the MKO; this guide checks them only for this f and g as polynomial identities and does not prove them for general differentiable functions. Lemma L_poly_deriv3 covers degree at most three, so products of cubic inputs (up to degree six) are outside what this guide differentiates.

Verification and source binding

13 declared checks for this guide; only the listed expressions are covered.

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: d018b0ec61f9ad721df0ccc4872b72a742b428f70ec5a6bc3709008d1983cb9f
• original source SHA-256: 28b99c11ef6db059516f55a9a5cd9265cb5ca4d59d4d271549486abdf6c12833
• Lean: NOT_RUN · independent AI: NOT_MEASURED

Same-source full JSON (formulas, ASTs, controls and revision log)