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.
What is fixed here and what is not: the derivative is taken at a point of the domain that is also a limit point of it, one-sided derivatives and derivatives of order above one are not introduced at this point in the reading order, and and name the same real number
This page fixes fewer conventions than a reader of a calculus text may expect, and it is worth saying which, so that a later page can rely on them and so that nothing here is read as more than it is.
Where a derivative may be taken. is defined only when belongs to the domain of and is a limit point of (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 ). At an isolated point of the symbol is not defined, and the function is neither differentiable nor non-differentiable there: the question is not posed. This is inherited from The - limit of at a limit point of , which leaves undefined at an isolated point for the reason recorded there, namely that the - condition would be satisfied vacuously by every real at once.
The domain is part of the data. "Differentiable at " is a statement about the pair and the point , not about near in isolation. Shrinking the domain preserves differentiability and the value of the derivative whenever the smaller domain still has as a limit point (The derivative of at a point that is a limit point of , and differentiability on a set), but enlarging it need not, and the companion page's witness at a corner shows that it need not. Wherever a statement on this page says "differentiable at every point of " for a function on , the domain meant is .
One-sided derivatives are not introduced at this point in the reading order. No item up to this point in the reading order defines one, and nothing below may be cited as though one had been. The ingredient is available: The left and right limits of at , as limits of the restrictions of to and defines the limit of at from the right as the limit at of the restriction of to (Intervals of : the nine order-convex forms, nondegeneracy, and length), and a right derivative would be that limit applied to the difference quotient. Nothing on this page needs it, so nothing on this page defines it. What does occur, and should not be confused with it, is the derivative at an endpoint of an interval: for on the symbol is defined by The derivative of at a point that is a limit point of , and differentiability on a set without any new convention, because the domain supplies points on one side of only and the difference quotient is a function on . So the object other texts call a one-sided derivative appears here as an ordinary derivative on a domain that happens to lie on one side.
Derivatives of order above one are not introduced at this point in the reading order either, and no item up to this point in the reading order defines one. A later page takes them up; nothing on this page anticipates it. Doing so requires more than iterating the definition: is a function on the set of points at which is differentiable, and to differentiate that function at a point one needs the point to be a limit point of that set, which is a hypothesis about and not a formality. No statement on this page mentions , and none should be read as implying anything about it.
Two notations, one object. and name the same real number. The second is a name, not a quotient: nothing in this library divides by , no object called is introduced, and the letter in it is a name for the argument of and not a variable that is being fixed or varied. This page writes throughout.
Two descriptions, one notion. By Carathéodory's characterisation: is differentiable at if and only if there is , continuous at , with for every , and then is unique and , " is differentiable at " may be read either as the convergence of the difference quotient or as the existence of a factorisation with continuous at . The two are equivalent, and the factor is unique, so either may be taken as the meaning of the word without ambiguity. Every statement on this page is phrased in the first, and the two readings divide the proofs between them: the differentiation rules use the factorisation, namely A function differentiable at is continuous at , Sums, scalar multiples, products and quotients: , , , and when , The chain rule, in one line from Carathéodory: if is differentiable at and is differentiable at , then is differentiable at with and Derivative of an inverse: if is continuous and injective on a nondegenerate interval and differentiable at with , then the inverse is differentiable at with ; and if then is not differentiable at , each exhibiting a factor and reading its continuity off the algebra of continuous functions; while the rest of the page works with the difference quotient directly, among them The linear-approximation form of the derivative: is differentiable at with if and only if the remainder satisfies ; at most one does so, so is the unique affine map approximating to first order at , the base cases of For a natural the function is differentiable everywhere with derivative ; for it is the constant , with derivative ; for a natural the function is differentiable at every with derivative ; consequently every polynomial function is differentiable at every real, with the derivative computed term by term, and Fermat's interior extremum theorem: if has a local extremum at a point interior to its domain and is differentiable at , then , whose whole mechanism is the sign of the quotient near the point.
What is deliberately not claimed anywhere on this page. That is continuous where it exists; that differentiability alone, with no hypothesis on , gives any regularity beyond the continuity of A function differentiable at is continuous at — a bound on does give more, and that is If is continuous on an interval and at every interior point, then for all , so is Lipschitz with constant and uniformly continuous on ; and that a vanishing derivative marks a local extremum. None of the three is addressed here, and no item on this page may be cited for any of them. What is recorded, as the two false statements of this page, is that the mean value theorem needs continuity on the closed interval and that a vanishing derivative at a point does not prevent a function from being increasing; each carries its own witness.
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
- The $\varepsilon$-$\delta$ limit $\lim_{x \to c} f(x) = L$ of $f : A \to \mathbb{R}$ at a limit point $c$ of $A$
- Limit point, isolated point, adherent point, derived set, and dense subset of $\mathbb{R}$
- The left and right limits of $f$ at $c$, as limits of the restrictions of $f$ to $A \cap (-\infty, c)$ and $A \cap (c, \infty)$
- Intervals of $\mathbb{R}$: the nine order-convex forms, nondegeneracy, and length
- 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 function differentiable at $c$ is continuous at $c$
- Sums, scalar multiples, products and quotients: $(f+g)'(c) = f'(c) + g'(c)$, $(\alpha f)'(c) = \alpha f'(c)$, $(fg)'(c) = f'(c)g(c) + f(c)g'(c)$, and $(f/g)'(c) = \bigl(f'(c)g(c) - f(c)g'(c)\bigr)/g(c)^{2}$ when $g(c) \ne 0$
- The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g(c)$, then $f \circ g$ is differentiable at $c$ with $(f \circ g)'(c) = f'(g(c))\,g'(c)$
- Derivative of an inverse: if $f$ is continuous and injective on a nondegenerate interval $I$ and differentiable at $c \in I$ with $f'(c) \ne 0$, then the inverse $g$ is differentiable at $f(c)$ with $g'(f(c)) = 1/f'(c)$; and if $f'(c) = 0$ then $g$ is not differentiable at $f(c)$
- The linear-approximation form of the derivative: $f$ is differentiable at $c$ with $f'(c) = L$ if and only if the remainder $r(x) = f(x) - f(c) - L(x-c)$ satisfies $\lim_{x \to c} r(x)/(x-c) = 0$; at most one $L$ does so, so $x \mapsto f(c) + L(x-c)$ is the unique affine map approximating $f$ to first order at $c$
- For a natural $n \ge 1$ the function $x \mapsto x^{n}$ is differentiable everywhere with derivative $\iota(n)\,x^{\,n-1}$; for $n = 0$ it is the constant $1$, with derivative $0$; for a natural $n \ge 1$ the function $x \mapsto x^{-n}$ is differentiable at every $x \ne 0$ with derivative $-\iota(n)\,x^{-n-1}$; consequently every polynomial function is differentiable at every real, with the derivative computed term by term
- Fermat's interior extremum theorem: if $f$ has a local extremum at a point $c$ interior to its domain and is differentiable at $c$, then $f'(c) = 0$
- If $f$ is continuous on an interval $I$ and $|f'| \le M$ at every interior point, then $|f(x) - f(y)| \le M|x-y|$ for all $x,y \in I$, so $f$ is Lipschitz with constant $M$ and uniformly continuous on $I$
Used by
Nothing in the library uses this result yet.
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 110 results over 23 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.
Sources
- Derivative (Wikipedia) (standard reference, not scraped)
- Notation for differentiation (Wikipedia) (standard reference, not scraped)
- One-sided limit (Wikipedia) (standard reference, not scraped)
- T. Gantumur, Differentiation (standard reference, not scraped)
- J. Lebl, Basic Analysis I, The Derivative (standard reference, not scraped)