Homotopy Type Theory
iterated differentiable function > history (Rev #2)
Contents
Definition
For a calculus field? F F and a subtype S ⊆ F S \subseteq F , the types of functions S → F S \to F , pointwise continuous function s C 0 ( S , F ) C^0(S, F) , and differentiable function s D 1 ( S , F ) D^1(S, F) between S S and F F are subtypes of the type of functions S → F S \to F . For the Newton-Leibniz operator D ˜ : D 1 ( S , F ) → ( S → F ) \tilde{D}: D^1(S, F) \to (S \to F) , the type of n n -fold iterated differentiable functions between S S and F F is the n n -fold iterated inverse image of S → F S \to F under the Newton-Leibniz operator:
D 0 ( S , F ) : = D ˜ − 0 ( S → F ) : = S → F D^0(S, F) := \tilde{D}^{-0}(S \to F) := S \to F n : ℕ ⊢ D n + 1 ( S , F ) : = D ˜ − ( n + 1 ) ( S → F ) : = ∑ f : D 1 ( S , F ) ‖ ∑ g : D n ( S , F ) D ˜ ( f ) = g ‖ n:\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 n n -fold iterated differentiable functions between S S and F F is the n n -fold iterated inverse image s 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 ) = g ‖ n:\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 April 23, 2022 at 03:58:52 by
Anonymous? .
See the history of this page for a list of all contributions to it.