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

Contents

Definition

Given a calculus field? FF and a subtype SFS \subseteq F, the Newton–Leibniz 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 that 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, which are axioms used to define a calculus field?.

Linearity

Leibniz rule

Power rule

Quotient rule

See also

Revision on April 16, 2022 at 07:51:41 by Anonymous?. See the history of this page for a list of all contributions to it.