ユークリディアンノルム付きユークリディアンベクトルたちスペース（空間）たち\(C^1\)マップ（写像）のための微積分の基本定理の記述/証明
話題
About: ベクトルたちスペース（空間）
この記事の目次
開始コンテキスト
- 読者は、ユークリディアンノルム付きユークリディアンベクトルたちスペース（空間）の定義を知っている。
- 読者は、ノルム付きベクトルたちスペース（空間）のオープンサブセット（開部分集合）からノルム付きベクトルたちスペース（空間）のサブセット（部分集合）の中へのマップ（写像）のポイントにおけるデリバティブ（微分係数）の定義を知っている。
- 読者は、任意のユークリディアン\(C^\infty\)マニフォールド（多様体）たちの任意のサブセット（部分集合）たち間の任意のマップ（写像）たちで対応するポイントたちにおいて\(C^k\)であるものたち、ここで、\(k\)は\(\infty\)を含む、に対して、コンポジション（合成）は当該ポイントにおいて\(C^k\)であるという命題を認めている。
- 読者は、1引数1値ファンクション（関数）に対する微積分の基本定理を認めている。
- 読者は、任意の\(C^1\)、ユークリディアンノルム付きユークリディアンベクトルたちスペース（空間）たちマップ（写像）のデリバティブ（微分係数）はヤコビアンであるという命題を認めている。
ターゲットコンテキスト
- 読者は、ユークリディアンノルム付きユークリディアンベクトルたちスペース（空間）たち\(C^1\)マップ（写像）のための微積分の基本定理の記述および証明を得る。
オリエンテーション
本サイトにてこれまで議論された定義たちの一覧があります。
本サイトにてこれまで議論された命題たちの一覧があります。
本体
1: 構造化された記述
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\(\mathbb{R}^{d_1}\): \(= \text{ 当該ユークリディアンノルム付きユークリディアンベクトルたちスペース（空間） }\)で、ユークリディアン\(C^\infty\)マニフォールド（多様体）でもあるもの
\(\mathbb{R}^{d_2}\): \(= \text{ 当該ユークリディアンノルム付きユークリディアンベクトルたちスペース（空間） }\)で、ユークリディアン\(C^\infty\)マニフォールド（多様体）でもあるもの
\(f\): \(: \mathbb{R}^{d_1} \to \mathbb{R}^{d_2}\), \(\in \{\text{ 全ての } C^1 \text{ マップ（写像）たち }\}\)
//
ステートメント（言明）たち:
\(\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: 証明
全体戦略: ステップ1: \(f^j (v_1 + t v'_1): \mathbb{R} \to \mathbb{R}, t \mapsto f^j (v_1 + t v'_1)\)のことを考え、1引数1値ファンクション（関数）に対する微積分の基本定理を適用する。
ステップ1:
\(f^j (v_1 + t v'_1): \mathbb{R} \to \mathbb{R}, t \mapsto f^j (v_1 + t v'_1)\)は、\(t\)に関するある1引数1値ファンクション（関数）である。
\(f^j (v_1 + t v'_1)\)は\(C^1\)である、\(C^1\)マップ（写像）たち\(: \mathbb{R} \to \mathbb{R}^{d_1}, t \mapsto v_1 + t v'_1\)および\(: \mathbb{R}^{d_1} \to \mathbb{R}, p \mapsto f^j (p)\)のコンポジション（合成）として、任意のユークリディアン\(C^\infty\)マニフォールド（多様体）たちの任意のサブセット（部分集合）たち間の任意のマップ（写像）たちで対応するポイントたちにおいて\(C^k\)であるものたち、ここで、\(k\)は\(\infty\)を含む、に対して、コンポジション（合成）は当該ポイントにおいて\(C^k\)であるという命題によって。
1引数1値ファンクション（関数）に対する微積分の基本定理によって、\(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\)。
つまり、\(f (v_1 + t v'_1) = f (v_1) + \int^t_0 {D f}_{v_1 + s v'_1} v'_1 d s\)、なぜなら、マップ（写像）のデリバティブ（微分係数）はヤコビアンである、任意の\(C^1\)、ユークリディアンノルム付きユークリディアンベクトルたちスペース（空間）たちマップ（写像）のデリバティブ（微分係数）はヤコビアンであるという命題によって。
