Homotopy Type Theory
Newton-Leibniz operator > history (Rev #3)
Contents
Definition
Given a calculus field? F F and a subtype S ⊆ F S \subseteq F , the Newton–Leibniz operator D ˜ : D 1 ( S , F ) → ( S → F ) \tilde{D}: D^1(S, F) \to (S \to F) is a function from the type of differentiable function s D 1 ( S , F ) D^1(S, F) to the type of functions S → F S \to F , and is pointwise defined as
D ˜ ( f ) ≔ lim ( x , y ) → ( x , x ) f ( x ) − f ( y ) x − y \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 f 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 → F c:S \to F be a constant function. With constant functions the function c : S → F c:S \to F and the value of the function c : F c:F are usually written with the same symbol.
∏ c : S → F D ˜ ( c ) = lim ( x , y ) → ( x , x ) c − c x − y \prod_{c:S \to F} \tilde{D}(c) = \lim_{(x, y) \to (x, x)} \frac{c - c}{x - y} ∏ c : S → F D ˜ ( c ) = lim ( x , y ) → ( x , x ) 0 x − y \prod_{c:S \to F} \tilde{D}(c) = \lim_{(x, y) \to (x, x)} \frac{0}{x - y} ∏ c : S → F D ˜ ( c ) = lim ( x , y ) → ( x , x ) 0 \prod_{c:S \to F} \tilde{D}(c) = \lim_{(x, y) \to (x, x)} 0 ∏ c : S → F D ˜ ( c ) = 0 \prod_{c:S \to F} \tilde{D}(c) = 0
Identity function rule
Where x x \frac{x}{x} is another notation for x ⋅ x − 1 x \cdot x^{-1}
D ˜ ( id F ) = lim ( x , y ) → ( x , x ) x − y x − y \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 : S → F ∏ b : F ∏ g : S → F D ˜ ( a ⋅ f + b ⋅ g ) = lim ( x , y ) → ( x , x ) ( a ⋅ f ( x ) + b ⋅ g ( x ) ) − ( a ⋅ f ( y ) + b ⋅ 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) + b \cdot g(x)) - (a \cdot f(y) + b \cdot g(y)}{x - y} ∏ a : F ∏ f : S → F ∏ b : F ∏ g : S → F D ˜ ( a ⋅ f + b ⋅ g ) = lim ( x , y ) → ( x , x ) ( a ⋅ f ( x ) − a ⋅ f ( y ) ) + ( b ⋅ g ( x ) − b ⋅ 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} ∏ a : F ∏ f : S → F ∏ b : F ∏ g : S → F D ˜ ( a ⋅ f + b ⋅ g ) = lim ( x , y ) → ( x , x ) ( a ⋅ ( f ( x ) − f ( y ) ) + ( b ⋅ ( 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)) + (b \cdot (g(x) - g(y))}{x - y} ∏ a : F ∏ f : S → F ∏ b : F ∏ g : S → F D ˜ ( a ⋅ f + b ⋅ g ) = lim ( x , y ) → ( x , x ) a ⋅ ( f ( x ) − f ( y ) x − y + b ⋅ ( 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} ∏ a : F ∏ f : S → F ∏ b : F ∏ g : S → F D ˜ ( a ⋅ f + b ⋅ g ) = a ⋅ lim ( x , y ) → ( x , x ) ( f ( x ) − f ( y ) x − y + b ⋅ lim ( x , y ) → ( x , x ) ( 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} ∏ a : F ∏ f : S → F ∏ b : F ∏ g : S → F D ˜ ( a ⋅ f + b ⋅ g ) = a ⋅ D ˜ ( f ) + b ⋅ D ˜ ( 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 : S → F ∏ g : S → F D ˜ ( f ⋅ g ) = lim ( x , y ) → ( x , x ) ( f ( x ) ⋅ g ( x ) ) − ( f ( y ) ⋅ 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(y) \cdot g(y)}{x - y} ∏ f : S → F ∏ g : S → F D ˜ ( f ⋅ g ) = lim ( x , y ) → ( x , x ) ( f ( x ) ⋅ g ( x ) ) − ( f ( x ) ⋅ g ( y ) ) + ( f ( x ) ⋅ g ( y ) ) − ( f ( y ) ⋅ 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} ∏ f : S → F ∏ g : S → F D ˜ ( f ⋅ g ) = lim ( x , y ) → ( x , x ) ( f ( x ) ⋅ ( g ( x ) − g ( y ) ) + ( ( f ( x ) − f ( y ) ) ⋅ 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} ∏ f : S → F ∏ g : S → F D ˜ ( f ⋅ g ) = lim ( x , y ) → ( x , x ) f ( x ) ⋅ ( g ( x ) − g ( y ) x − y + ( f ( x ) − f ( y ) ) ⋅ 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} ∏ f : S → F ∏ g : S → F D ˜ ( f ⋅ g ) = f ⋅ ( lim ( x , y ) → ( x , x ) g ( x ) − g ( y ) x − y ) + ( lim ( x , y ) → ( x , x ) f ( x ) − f ( y ) x − y ) ⋅ 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 : S → F ∏ g : S → F D ˜ ( f ⋅ g ) = f ⋅ D ˜ ( 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 : S → F D ˜ ( f n ) = lim ( x , y ) → ( x , x ) f ( x ) n − f ( y ) n x − y \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 n = 0 :
∏ f : S → F D ˜ ( f 0 ) = lim ( x , y ) → ( x , x ) f ( x ) 0 − f ( y ) 0 x − y \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 : S → F D ˜ ( f 0 ) = lim ( x , y ) → ( x , x ) 1 − 1 x − y \prod_{f:S \to F} \tilde{D}(f^0) = \lim_{(x, y) \to (x, x)} \frac{1 - 1}{x - y} ∏ f : S → F D ˜ ( f 0 ) = D ˜ ( 1 ) \prod_{f:S \to F} \tilde{D}(f^0) = \tilde{D}(1)
Then the inductive case:
∏ n : N ∏ f : S → F D ˜ ( f n + 1 ) = lim ( x , y ) → ( x , x ) 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)^{n+1} - f(y)^{n+1}}{x - y} ∏ n : N ∏ f : S → F D ˜ ( f n + 1 ) = lim ( x , y ) → ( x , x ) f ( x ) ⋅ f ( x ) n − f ( y ) ⋅ f ( y ) n 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} ∏ n : N ∏ f : S → F D ˜ ( 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 : S → F D ˜ ( f n + 1 ) = ∑ n = 0 n D ˜ ( 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 April 16, 2022 at 15:01:19 by
Anonymous? .
See the history of this page for a list of all contributions to it.