Homotopy Type Theory iterated differentiable function > history (Rev #3, changes)

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

Contents

< iterated differentiable function

Definition

For a calculus field? FF and a subtype SFS \subseteq F, the types of functions SFS \to F, pointwise continuous functions C 0(S,F)C^0(S, F), and differentiable functions D 1(S,F)D^1(S, F) between SS and FF are subtypes of the type of functions SFS \to F. For the Newton-Leibniz operator D˜:D 1(S,F)(SF)\tilde{D}: D^1(S, F) \to (S \to F), the type of nn-fold iterated differentiable functions between SS and FF is the nn-fold iterated inverse image of SFS \to F under the Newton-Leibniz operator:

D 0(S,F):=D˜ 0(SF):=SFD^0(S, F) := \tilde{D}^{-0}(S \to F) := S \to F
n:D n+1(S,F):=D˜ (n+1)(SF):= f:D 1(S,F) g:D n(S,F)D˜(f)=gn:\mathbb{N} \vdash D^{n+1}(S, F) := \tilde{D}^{-(n+1)}(S \to F) := \sum_{f:D^1(S, F)} \Vert\sum_{g:D^{n}(S, F)} \tilde{D}(f) = g\Vert

and the type of pointwise continuously nn-fold iterated differentiable functions between SS and FF is the nn-fold iterated inverse images of C 0(S,F)C^0(S, F) under the Newton-Leibniz operator:

C 0(S,F):=D˜ 0(C 0(S,F)):=C 0(S,F)C^0(S, F) := \tilde{D}^{-0}(C^0(S, F)) := C^0(S, F)
n:C n+1(S,F):=D˜ (n+1)(C 0(S,F)):= f:D 1(S,F) g:C n(S,F)D˜(f)=gn:\mathbb{N} \vdash C^{n+1}(S, F) := \tilde{D}^{-(n+1)}(C^0(S, F)) := \sum_{f:D^1(S, F)} \Vert\sum_{g:C^{n}(S, F)} \tilde{D}(f) = g\Vert

See also

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