description/proof of fundamental theorem of calculus for \(C^1\), Euclidean-normed Euclidean vectors spaces map
Topics
About: vectors space
The table of contents of this article
Starting Context
- The reader knows a definition of Euclidean-normed Euclidean vectors space.
- The reader knows a definition of derivative of map from open subset of normed vectors space into subset of normed vectors space at point.
- The reader admits the proposition that for any maps between any arbitrary subsets of any Euclidean \(C^\infty\) manifolds \(C^k\) at corresponding points, where \(k\) includes \(\infty\), the composition is \(C^k\) at the point.
- The reader admits the fundamental theorem of calculus for 1-argument 1-value function.
- The reader admits the proposition that derivative of \(C^1\), Euclidean-normed Euclidean vectors spaces map is the Jacobian.
Target Context
- The reader will have a description and a proof of the fundamental theorem of calculus for \(C^1\), Euclidean-normed Euclidean vectors spaces map.
Orientation
There is a list of definitions discussed so far in this site.
There is a list of propositions discussed so far in this site.
Main Body
1: Structured Description
Here is the rules of Structured Description.
Entities:
\(\mathbb{R}^{d_1}\): \(= \text{ the Euclidean-normed Euclidean vectors space }\) also as the Euclidean \(C^\infty\) manifold
\(\mathbb{R}^{d_2}\): \(= \text{ the Euclidean-normed Euclidean vectors space }\) also as the Euclidean \(C^\infty\) manifold
\(f\): \(: \mathbb{R}^{d_1} \to \mathbb{R}^{d_2}\), \(\in \{\text{ the } C^1 \text{ maps }\}\)
//
Statements:
\(\forall v_1, v'_1 \in \mathbb{R}^{d_1}, \forall t \in \mathbb{R} (f (v_1 + t v'_1) = f (v_1) + \int^t_0 {D f}_{v_1 + s v'_1} v'_1 d s)\)
//
2: Proof
Whole Strategy: Step 1: think of \(f^j (v_1 + t v'_1): \mathbb{R} \to \mathbb{R}, t \mapsto f^j (v_1 + t v'_1)\), and apply the fundamental theorem of calculus for 1-argument 1-value function.
Step 1:
\(f^j (v_1 + t v'_1): \mathbb{R} \to \mathbb{R}, t \mapsto f^j (v_1 + t v'_1)\) is a 1-argument 1-value function with respect to \(t\).
\(f^j (v_1 + t v'_1)\) is \(C^1\), as the composition of \(C^1\) maps, \(: \mathbb{R} \to \mathbb{R}^{d_1}, t \mapsto v_1 + t v'_1\) and \(: \mathbb{R}^{d_1} \to \mathbb{R}, p \mapsto f^j (p)\), by the proposition that for any maps between any arbitrary subsets of any Euclidean \(C^\infty\) manifolds \(C^k\) at corresponding points, where \(k\) includes \(\infty\), the composition is \(C^k\) at the point.
By the fundamental theorem of calculus for 1-argument 1-value function, \(f^j (v_1 + t v'_1) = f^j (v_1) + \int^t_0 d f^j (v_1 + s v'_1) / d s d s = f^j (v_1) + \int^t_0 \partial_l f^j (v_1 + s v'_1) {v'_1}^l d s\).
That is \(f (v_1 + t v'_1) = f (v_1) + \int^t_0 {D f}_{v_1 + s v'_1} v'_1 d s\), because the derivative of the map is the Jacobian, by the proposition that derivative of \(C^1\), Euclidean-normed Euclidean vectors spaces map is the Jacobian.
