Homotopy Type Theory Newton-Leibniz operator > history (Rev #5)

Contents

Definition

Given a algebraic limit field FF and a subtype SFS \subseteq F, the Newton–Leibniz operator or D operator D˜:D 1(S,F)(SF)\tilde{D}: D^1(S, F) \to (S \to F) is a function from the type of differentiable functions D 1(S,F)D^1(S, F) to the type of functions SFS \to F, and is pointwise defined as

D˜(f)lim (x,y)(x,x)f(x)f(y)xy\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)f:D^1(S, F). For any differentiable function f:D 1(S,F)f:D^1(S, F), the function D˜(f)\tilde{D}(f) is called the derivative of ff.

Properties

These all follow from the algebraic limit theorems of the limit of a binary function approaching a diagonal.

Constant function rule

Let c:SFc:S \to F be a constant function. With constant functions the function c:SFc:S \to F and the value of the function c:Fc:F are usually written with the same symbol.

c:SFD˜(c)=lim (x,y)(x,x)ccxy\prod_{c:S \to F} \tilde{D}(c) = \lim_{(x, y) \to (x, x)} \frac{c - c}{x - y}
c:SFD˜(c)=lim (x,y)(x,x)0xy\prod_{c:S \to F} \tilde{D}(c) = \lim_{(x, y) \to (x, x)} \frac{0}{x - y}
c:SFD˜(c)=lim (x,y)(x,x)0\prod_{c:S \to F} \tilde{D}(c) = \lim_{(x, y) \to (x, x)} 0
c:SFD˜(c)=0\prod_{c:S \to F} \tilde{D}(c) = 0

Identity function rule

Where xx\frac{x}{x} is another notation for xx 1x \cdot x^{-1}

D˜(id F)=lim (x,y)(x,x)xyxy\tilde{D}(id_F) = \lim_{(x, y) \to (x, x)} \frac{x - y}{x - y}
D˜(id F)=1\tilde{D}(id_F) = 1

Linearity

a:F f:SF b:F g:SFD˜(af+bg)=lim (x,y)(x,x)(af(x)+bg(x))(af(y)+bg(y)xy\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}
a:F f:SF b:F g:SFD˜(af+bg)=lim (x,y)(x,x)(af(x)af(y))+(bg(x)bg(y)xy\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}
a:F f:SF b:F g:SFD˜(af+bg)=lim (x,y)(x,x)(a(f(x)f(y))+(b(g(x)g(y))xy\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}
a:F f:SF b:F g:SFD˜(af+bg)=lim (x,y)(x,x)a(f(x)f(y)xy+b(g(x)g(y)xy\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}
a:F f:SF b:F g:SFD˜(af+bg)=alim (x,y)(x,x)(f(x)f(y)xy+blim (x,y)(x,x)(g(x)g(y)xy\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}
a:F f:SF b:F g:SFD˜(af+bg)=aD˜(f)+bD˜(g)\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

f:SF g:SFD˜(fg)=lim (x,y)(x,x)(f(x)g(x))(f(y)g(y)xy\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}
f:SF g:SFD˜(fg)=lim (x,y)(x,x)(f(x)g(x))(f(x)g(y))+(f(x)g(y))(f(y)g(y)xy\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}
f:SF g:SFD˜(fg)=lim (x,y)(x,x)(f(x)(g(x)g(y))+((f(x)f(y))g(y))xy\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}
f:SF g:SFD˜(fg)=lim (x,y)(x,x)f(x)(g(x)g(y)xy+(f(x)f(y))g(y)xy\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}
f:SF g:SFD˜(fg)=f(lim (x,y)(x,x)g(x)g(y)xy)+(lim (x,y)(x,x)f(x)f(y)xy)g\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
f:SF g:SFD˜(fg)=fD˜(g)+D˜(f)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

n:N f:SFD˜(f n)=lim (x,y)(x,x)f(x) nf(y) nxy\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=0n = 0:

f:SFD˜(f 0)=lim (x,y)(x,x)f(x) 0f(y) 0xy\prod_{f:S \to F} \tilde{D}(f^0) = \lim_{(x, y) \to (x, x)} \frac{f(x)^0 - f(y)^0}{x - y}
f:SFD˜(f 0)=lim (x,y)(x,x)11xy\prod_{f:S \to F} \tilde{D}(f^0) = \lim_{(x, y) \to (x, x)} \frac{1 - 1}{x - y}
f:SFD˜(f 0)=D˜(1)\prod_{f:S \to F} \tilde{D}(f^0) = \tilde{D}(1)

Then the inductive case:

n:N f:SFD˜(f n+1)=lim (x,y)(x,x)f(x) n+1f(y) n+1xy\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}
n:N f:SFD˜(f n+1)=lim (x,y)(x,x)f(x)f(x) nf(y)f(y) nxy\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}
n:N f:SFD˜(f n+1)=D˜(f)f n+D˜(f n)f\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
n:N f:SFD˜(f n+1)= n=0 nD˜(f)f n\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

Revision on May 4, 2022 at 15:59:44 by Anonymous?. See the history of this page for a list of all contributions to it.