[[!redirects derivative]] #Contents# * table of contents {:toc} ## Definition ## Given a [[calculus field]] $F$ and a subtype $S \subseteq F$, the __Newton–Leibniz operator__ $\tilde{D}: D^1(S, F) \to (S \to F)$ is a function from the type of [[differentiable function]]s $D^1(S, F)$ to the type of functions $S \to F$, and is pointwise defined as $$\tilde{D}(f) \coloneqq \lim_{(x, y) \to (x, x)} \frac{f(x) - f(y)}{x - y}$$ for a [[differentiable function]] $f:D^1(S, F)$. For any differentiable function $f:D^1(S, F)$, the function $\tilde{D}(f)$ is called the __derivative__ of $f$. ## Properties ## These all follow from the [[algebraic limit theorem]]s of the [[limit of a binary function approaching a diagonal]]. ### Constant function rule ### Let $c:S \to F$ be a constant function. With constant functions the function $c:S \to F$ and the value of the function $c:F$ are usually written with the same symbol. $$\prod_{c:S \to F} \tilde{D}(c) = \lim_{(x, y) \to (x, x)} \frac{c - c}{x - y}$$ $$\prod_{c:S \to F} \tilde{D}(c) = \lim_{(x, y) \to (x, x)} \frac{0}{x - y}$$ $$\prod_{c:S \to F} \tilde{D}(c) = \lim_{(x, y) \to (x, x)} 0$$ $$\prod_{c:S \to F} \tilde{D}(c) = 0$$ ### Identity function rule ### Where $\frac{x}{x}$ is another notation for $x \cdot x^{-1}$ $$\tilde{D}(id_F) = \lim_{(x, y) \to (x, x)} \frac{x - y}{x - y}$$ $$\tilde{D}(id_F) = 1$$ ### Linearity ### $$\prod_{a:F} \prod_{f:S \to F} \prod_{b:F} \prod_{g:S \to F} \tilde{D}(a \cdot f + b \cdot g) = \lim_{(x, y) \to (x, x)} \frac{(a \cdot f(x) + b \cdot g(x)) - (a \cdot f(y) + b \cdot g(y)}{x - y}$$ $$\prod_{a:F} \prod_{f:S \to F} \prod_{b:F} \prod_{g:S \to F} \tilde{D}(a \cdot f + b \cdot g) = \lim_{(x, y) \to (x, x)} \frac{(a \cdot f(x) - a \cdot f(y)) + (b \cdot g(x) - b \cdot g(y)}{x - y}$$ $$\prod_{a:F} \prod_{f:S \to F} \prod_{b:F} \prod_{g:S \to F} \tilde{D}(a \cdot f + b \cdot g) = \lim_{(x, y) \to (x, x)} \frac{(a \cdot (f(x) - f(y)) + (b \cdot (g(x) - g(y))}{x - y}$$ $$\prod_{a:F} \prod_{f:S \to F} \prod_{b:F} \prod_{g:S \to F} \tilde{D}(a \cdot f + b \cdot g) = \lim_{(x, y) \to (x, x)} \frac{a \cdot (f(x) - f(y)}{x - y} + \frac{b \cdot (g(x) - g(y)}{x - y}$$ $$\prod_{a:F} \prod_{f:S \to F} \prod_{b:F} \prod_{g:S \to F} \tilde{D}(a \cdot f + b \cdot g) = a \cdot \lim_{(x, y) \to (x, x)} \frac{(f(x) - f(y)}{x - y} + b \cdot \lim_{(x, y) \to (x, x)} \frac{(g(x) - g(y)}{x - y}$$ $$\prod_{a:F} \prod_{f:S \to F} \prod_{b:F} \prod_{g:S \to F} \tilde{D}(a \cdot f + b \cdot g) = a \cdot \tilde{D}(f) + b \cdot \tilde{D}(g)$$ ### Leibniz rule ### $$\prod_{f:S \to F} \prod_{g:S \to F} \tilde{D}(f \cdot g) = \lim_{(x, y) \to (x, x)} \frac{(f(x) \cdot g(x)) - (f(y) \cdot g(y)}{x - y}$$ $$\prod_{f:S \to F} \prod_{g:S \to F} \tilde{D}(f \cdot g) = \lim_{(x, y) \to (x, x)} \frac{(f(x) \cdot g(x)) - (f(x) \cdot g(y)) + (f(x) \cdot g(y)) - (f(y) \cdot g(y)}{x - y}$$ $$\prod_{f:S \to F} \prod_{g:S \to F} \tilde{D}(f \cdot g) = \lim_{(x, y) \to (x, x)} \frac{(f(x) \cdot (g(x) - g(y)) + ((f(x) - f(y)) \cdot g(y))}{x - y}$$ $$\prod_{f:S \to F} \prod_{g:S \to F} \tilde{D}(f \cdot g) = \lim_{(x, y) \to (x, x)} \frac{f(x) \cdot (g(x) - g(y)}{x - y} + \frac{(f(x) - f(y)) \cdot g(y)}{x - y}$$ $$\prod_{f:S \to F} \prod_{g:S \to F} \tilde{D}(f \cdot g) = f \cdot \left(\lim_{(x, y) \to (x, x)} \frac{g(x) - g(y)}{x - y}\right) + \left(\lim_{(x, y) \to (x, x)} \frac{f(x) - f(y)}{x - y}\right) \cdot g$$ $$\prod_{f:S \to F} \prod_{g:S \to F} \tilde{D}(f \cdot g) = f \cdot \tilde{D}(g) + \tilde{D}(f) \cdot g$$ ### Power rule ### $$\prod_{n:\mathbf{N}} \prod_{f:S \to F} \tilde{D}(f^n) = \lim_{(x, y) \to (x, x)} \frac{f(x)^n - f(y)^n}{x - y}$$ We proceed by induction on the natural numbers. The base case $n = 0$: $$\prod_{f:S \to F} \tilde{D}(f^0) = \lim_{(x, y) \to (x, x)} \frac{f(x)^0 - f(y)^0}{x - y}$$ $$\prod_{f:S \to F} \tilde{D}(f^0) = \lim_{(x, y) \to (x, x)} \frac{1 - 1}{x - y}$$ $$\prod_{f:S \to F} \tilde{D}(f^0) = \tilde{D}(1)$$ Then the inductive case: $$\prod_{n:\mathbf{N}} \prod_{f:S \to F} \tilde{D}(f^{n+1}) = \lim_{(x, y) \to (x, x)} \frac{f(x)^{n+1} - f(y)^{n+1}}{x - y}$$ $$\prod_{n:\mathbf{N}} \prod_{f:S \to F} \tilde{D}(f^{n+1}) = \lim_{(x, y) \to (x, x)} \frac{f(x) \cdot f(x)^{n} - f(y) \cdot f(y)^{n}}{x - y}$$ $$\prod_{n:\mathbf{N}} \prod_{f:S \to F} \tilde{D}(f^{n+1}) = \tilde{D}(f) \cdot f^n + \tilde{D}(f^n) \cdot f$$ $$\prod_{n:\mathbf{N}} \prod_{f:S \to F} \tilde{D}(f^{n+1}) = \sum_{n=0}^{n} \tilde{D}(f) \cdot f^n$$ ### Reciprocal rule ### ### Chain rule ### ## See also ## * [[differentiable function]] * [[iterated differentiable function]] * [[smooth function]] * [[antiderivative]]