How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
The chain rule, in one line from Carathéodory: if is differentiable at and is differentiable at , then is differentiable at with
Statement
Let , let with and let , so that the composite is defined. Let be a limit point of (Limit point, isolated point, adherent point, derived set, and dense subset of ) at which is differentiable (The derivative of at a point that is a limit point of , and differentiability on a set), put , and suppose is a limit point of at which is differentiable. Then is differentiable at and
Both limit-point hypotheses are needed, and neither is automatic. That is a limit point of is what makes and defined symbols; that is a limit point of is what makes one. Nothing forces the second: may be differentiable at and send to an isolated point of , and there is not defined and the formula asserts nothing.
No case analysis appears anywhere. The naive difference-quotient proof writes and then has to say what happens where , which may occur at points arbitrarily close to . Carathéodory's factorisation never divides by the inner increment, so the difficulty does not arise.
Facts & Assumptions
Given: Sets , functions with and , a point that is a limit point of at which is differentiable, and the point , a limit point of at which is differentiable (The derivative of at a point that is a limit point of , and differentiability on a set, Limit point, isolated point, adherent point, derived set, and dense subset of ).
Carathéodory's characterisation (Carathéodory's characterisation: is differentiable at if and only if there is , continuous at , with for every , and then is unique and ), used in both directions: for , a point that is a limit point of and , the function is differentiable at if and only if there is , continuous at , with for every , and then .
Algebra of continuous functions (Sums, scalar multiples, products, absolute values, maxima, minima and quotients with nonvanishing denominator of continuous functions are continuous, as are constants, the identity and every polynomial function, claim 1): a product of two functions continuous at a point of their common domain is continuous there.
Composition of continuous functions (A composite of continuous functions is continuous, with no side hypothesis of the kind the composition of limits needs): if has and is continuous at , and if is continuous at , then is continuous at (Continuity of at a point of and on : the - condition, its agreement with at a limit point, and continuity at an isolated point).
A function differentiable at a point is continuous there (A function differentiable at is continuous at ).
Proof
By [L1], applied to on at , fix , continuous at , with for every and .
By [L1], applied to on at , fix , continuous at , with for every and .
The factorisation. Let . Then , so taking in step 1.2 gives , and by step 1.1. Since , this reads for every , where is the pointwise product .
The outer factor is continuous at . By [L4] the function is continuous at ; by step 1.2 the function is continuous at ; and . So is continuous at by [L3].
The factor is continuous at , with the right value. is the product of , continuous at by step 2.2, with , continuous at by step 1.1, so is continuous at by [L2]; and .
By step 2.1 the function factors the increment of at , and by step 3.1 it is continuous at . So [L1], applied to on at the limit point , gives that is differentiable at with .
Remarks
-
Where the classical proof goes wrong, precisely. It divides by , which may vanish at points arbitrarily close to even when is differentiable at with ; the usual repair defines an auxiliary function equal to the outer quotient off the bad set and to on it, and then proves that auxiliary function continuous. That auxiliary function is , and Carathéodory's characterisation: is differentiable at if and only if there is , continuous at , with for every , and then is unique and is the observation that it exists before any repair is attempted.
-
What is composed is continuity, not differentiability. The only theorem about composites used above is A composite of continuous functions is continuous, with no side hypothesis of the kind the composition of limits needs, and it needs no side hypothesis, unlike the corresponding statement for limits. That is the whole reason the proof has no cases.
-
The formula is about the point , not about near . Both derivatives on the right are taken at single points, and the theorem says nothing about on the image of any neighbourhood of . In particular no hypothesis is placed on beyond its lying in .
Depends on
- The derivative $f'(c) = \lim_{x \to c} \frac{f(x) - f(c)}{x - c}$ of $f : A \to \mathbb{R}$ at a point $c \in A$ that is a limit point of $A$, and differentiability on a set
- Carathéodory's characterisation: $f$ is differentiable at $c$ if and only if there is $\varphi : A \to \mathbb{R}$, continuous at $c$, with $f(x) - f(c) = \varphi(x)(x - c)$ for every $x \in A$, and then $\varphi$ is unique and $\varphi(c) = f'(c)$
- A composite of continuous functions is continuous, with no side hypothesis of the kind the composition of limits needs
- A function differentiable at $c$ is continuous at $c$
- Sums, scalar multiples, products, absolute values, maxima, minima and quotients with nonvanishing denominator of continuous functions are continuous, as are constants, the identity and every polynomial function
- Continuity of $f : A \to \mathbb{R}$ at a point of $A$ and on $A$: the $\varepsilon$-$\delta$ condition, its agreement with $\lim_{x \to c} f(x) = f(c)$ at a limit point, and continuity at an isolated point
- Limit point, isolated point, adherent point, derived set, and dense subset of $\mathbb{R}$
Used by
- A regular C¹ path has a C¹ arc-length reparametrization with derivative of Euclidean norm one Corollary
- A uniform limit of smooth functions need not be differentiable anywhere Corollary
- Every continuous function on [0,1] is uniformly approximated by everywhere-differentiable functions whose derivative vanishes at a prescribed point Corollary
- Henstock–Kurzweil substitution for a derivative composed with a differentiable map Corollary
- A flat smooth real function has no holomorphic extension near zero Counterexample
- A function differentiable on [0,1] whose derivative is unbounded, hence not Riemann integrable Counterexample
- A map with two preimages but degree zero Counterexample
- A smooth function not equal to its Maclaurin series Counterexample
- An invertible derivative at one point does not give a local inverse without C¹ regularity Counterexample
- Differentiation under an improper integral can fail without uniform domination Counterexample
- Infinite variance can defeat square-root-n CLT scaling Counterexample
- L'Hôpital's conclusion does not imply convergence of the derivative quotient Counterexample
- Pointwise limit discontinuous at zero signals mass escape Counterexample
- Principal arcsine has no finite derivative at -1 or 1 Counterexample
- Smooth data do not force an analytic solution Counterexample
- Volterra's function is differentiable everywhere with bounded derivative, but its derivative is not Riemann integrable Counterexample
- x↦ x³ is a C¹ bijection whose inverse is not differentiable at zero Counterexample
- Carleson tiles wave packets and tile order Definition
- A differentiable function whose derivative is discontinuous Example
- A function with positive derivative at 0 that is monotone on no neighbourhood of 0 Example
- A nonzero smooth compactly supported bump Example
- Cauchy law and its characteristic function Example
- Characteristic function of a gaussian law Example
- Characteristic function of the uniform law Example
- Conditional density of a bivariate normal law Example
- F(x)=x² sin(1/x²) has an unbounded derivative whose Henstock–Kurzweil integral is sin 1 Example
- G(x)=x² sin(1/x) has a bounded derivative discontinuous at 0 that is nevertheless Riemann integrable, and Newton–Leibniz evaluates its integral Example
- Geodesics in the Poincare upper half-plane Example
- Great circles as round-sphere geodesics Example
- Independent sums via characteristic functions Example
- r² sin(1/r) is differentiable at the origin with a discontinuous gradient Example
- sin(xy) and its mixed partial derivatives Example
- The chain rule applied to x ↦ (x²+1)⁵ and to x ↦ ((3x-1)²+2)³, with the Carathéodory factor written out in closed form in the first case Example
- The de Rham map on the angular form Example
- The extension of x² sin(1/x) by zero is differentiable but its derivative is discontinuous at zero Example
- The Fourier series of a sawtooth and the Basel sum Example
- The Fourier series of a square wave and the odd reciprocal-square sum Example
- The integral test applied to ∑ 1/ι(k+1)ᵖ for rational p>0, cross-checked against the published p-series theorem Example
- The one-sided flat function is C^∞ with identically zero Taylor series Example
- The solid generated by rotating y=sin x on [0,π] has volume π²/2 Example
…and 38 more results.
Dependency tree · two levels
26 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- Chain rule (Wikipedia) (standard reference, not scraped)
- W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 5 (Thm 5.5) (standard reference, not scraped)
- J. Lebl, Basic Analysis I, §4.1 (standard reference, not scraped)
- J. Lebl, Basic Analysis I, The Derivative (standard reference, not scraped)
- J. Hunter, An Introduction to Real Analysis (standard reference, not scraped)