Homotopy Type Theory sequential antiderivative > history (Rev #3, changes)

Showing changes from revision #2 to #3: Added | Removed | Changed

Contents

Definition

Given a $\mathbb{Z}$-module MM and a sequence x:Mx:\mathbb{N} \to M, the type of sequential antiderivatives of xx is the fiber of the sequential derivative at xx:

sequentialAntiderivatives(x) y:MD(y)=x\mathrm{sequentialAntiderivatives}(x) \coloneqq \sum_{y:\mathbb{N} \to M} D(y) = x

A sequential antiderivative is a term of the above type.

In \mathbb{Q}-vector spaces

If MM is a $\mathbb{Q}$-vector space, then every sequence in MM has an antiderivative operator for every term m:Mm:M,

m:MD m 1:(M)(M)m:M \vdash D^{-1}_m:(\mathbb{N} \to M) \to (\mathbb{N} \to M)

defined as

D m 1(x)(0)=mD^{-1}_m(x)(0) = m
D m 1(x)(i+i)x(i)iD^{-1}_m(x)(i + i) \coloneqq \frac{x(i)}{i}

for i:i:\mathbb{N}.

See also

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