# Homotopy Type Theory Newton-Leibniz operator > history (Rev #6, changes)

Showing changes from revision #5 to #6: Added | Removed | Changed

# Contents

## Definition

Given a an algebraic Archimedean limit ordered field $F$ , and the a subtype$S \subseteq F$, the Newton–Leibniz operator or D operator  \tilde{D}: D^1(S, D^1(F, F) \to (S (F \to F) is a function from the type of differentiable functions  D^1(S, D^1(F, F) to the type of functions  S F \to F , . and For is any pointwise differentiable defined function as$f:D^1(F, F)$, the function $\tilde{D}(f)$ is called the derivative of $f$.

$\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 theorems 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$