ユークリディアン\(C^\infty\)マニフォールド（多様体）のオープンサブセット（開部分集合）からユークリディアン\(C^\infty\)マニフォールド（多様体）のサブセット（部分集合）の中への\(C^1\)マップ（写像）に対する平均値定理の記述/証明
話題
About: \(C^\infty\)マニフォールド（多様体）
この記事の目次
開始コンテキスト
- 読者は、\(C^\infty\)マニフォールド（多様体）、バウンダリー（境界）付き、たちの任意のサブセット（部分集合）たち間の\(C^k\)マップ（写像）、ここで、\(k\)は\(\infty\)を含む、の定義を知っている。
- 読者は、ベクトルノルムたちによってインデュースト（誘導された）マトリックスノルムの定義を知っている。
- 読者は、任意のクローズドインターバル（閉区間）から\(1\)-ディメンショナル（次元）ユークリディアン\(C^\infty\)マニフォールド（多様体）の中への任意のディファレンシャブル（微分可能）マップ（写像）に対する平均値定理を認めている。
- 読者は、任意のリアル（実）またはコンプレックス（複素）インナープロダクト（内積）付きベクトルたちスペース（空間）に対するコーシー・シュワルツ不等式を認めている。
ターゲットコンテキスト
- 読者は、任意のユークリディアン\(C^\infty\)マニフォールド（多様体）の任意のオープンサブセット（開部分集合）から任意のユークリディアン\(C^\infty\)マニフォールド（多様体）の任意のサブセット（部分集合）の中への任意の\(C^1\)マップ（写像）に対する平均値定理の記述および証明を得る。
オリエンテーション
本サイトにてこれまで議論された定義たちの一覧があります。
本サイトにてこれまで議論された命題たちの一覧があります。
本体
1: 構造化された記述
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\(\mathbb{R}^{d_1}\): \(= \text{ 当該ユークリディアン } C^\infty \text{ マニフォールド（多様体） }\)で、当該ユークリディアンインナープロダクト（内積）を持つもの
\(\mathbb{R}^{d_2}\): \(= \text{ 当該ユークリディアン } C^\infty \text{ マニフォールド（多様体） }\)で、当該ユークリディアンインナープロダクト（内積）を持つもの
\(U\): \(\in \{\mathbb{R}^{d_1} \text{ の全てのオープンサブセット（開部分集合）たち }\}\)
\(S\): \(\in \{\mathbb{R}^{d_2} \text{ の全てのサブセット（部分集合）たち }\}\)
\(f\): \(: U \to S\), \(\in \{\text{ 全ての } C^1 \text{ マップ（写像）たち }\}\)
\(\{r_1, r_2\}\): \(\subseteq U\)で、\(\overline{r_1 r_2} \subseteq U\)を満たすもの、ここで、\(\overline{r_1 r_2}\)はラインセグメント（線分）
\(M\): \(: U \to \{\text{ 全ての } d_2 \times d_1 \mathbb{R} \text{ マトリックス（行列）たち }\}\), \(= \begin{pmatrix} \partial_1 f^1 & ... & \partial_{d_1} f^1 \\ ... \\ \partial_1 f^{d_2} & ... & \partial_{d_1} f^{d_2} \end{pmatrix}\)
\(v\): \(\in \mathbb{R}^{d_2}\)
//
ステートメント（言明）たち:
\(\exists r \in \overline{r_1 r_2} \text{ のインテリア（内部） } (\langle v, f (r_2) - f (r_1) \rangle = \langle v, M_r (r_2 - r_1) \rangle)\)
\(\land\)
\(\Vert f (r_2) - f (r_1) \Vert \le \Vert M_r \Vert \Vert r_2 - r_1 \Vert\)
//
2: 注
本命題は、\(f\)が\(C^1\)であるよう要求する、単にディファレンシャブル（微分可能）ではなく、なぜなら、それは、いくつか複数の中間変数たちを持つデリバティブ（微分係数）たちに対するチェインルール（鎖の規則）を使う。
3: 証明
全体戦略: ステップ1: \(f': [0, 1] \to S, t \mapsto \langle v, f (r_1 + t (r_2 - r_1)) \rangle\)を取り、\(\partial_1 f' = \langle v, M (r_2 - r_1) \rangle\)であることを見る; ステップ2: 以下を満たすある\(t' \in (0, 1)\)、つまり、\({\partial_1 f'}_{t'} = (f' (1) - f' (0)) / 1\)、があることを見る; ステップ3: \(r = r_1 + t' (r_2 - r_1)\)を取り、\(\langle v, M_r (r_2 - r_1) \rangle = \langle v, f (r_2) - f (r_1) \rangle\)であることを見る; ステップ4: \(v\)を\(f (r_2) - f (r_1)\)の方向のユニット（単位）ベクトルと取る。
ステップ1:
\(f': [0, 1] \to S, t \mapsto \langle v, f (r_1 + t (r_2 - r_1)) \rangle\)を取ろう。
\(f'\)は、\(C^1\)で、\(\partial_1 f' = \partial_1 (\sum_{j \in \{1, ..., d_2\}} v^j f^j (r_1 + t (r_2 - r_1))) = \sum_{j \in \{1, ..., d_2\}} \partial_1 (v^j f^j (r_1 + t (r_2 - r_1))) = \sum_{j \in \{1, ..., d_2\}} v^j \partial_1 f^j (r_1 + t (r_2 - r_1)) = \sum_{j \in \{1, ..., d_2\}} v^j \partial_l f^j (r_1 + t (r_2 - r_1)) \partial_1 (r_1 + t (r_2 - r_1))^l\)を持つ、チェーンルール（鎖の規則）によって、\(= \sum_{j \in \{1, ..., d_2\}} v^j \partial_l f^j (r_1 + t (r_2 - r_1)) (r_2 - r_1)^l = \sum_{j \in \{1, ..., d_2\}} v^j M^j_l (r_2 - r_1)^l = \langle v, M (r_2 - r_1) \rangle\)。
ステップ2:
以下を満たすある\(t' \in (0, 1)\)、つまり、\({\partial_1 f'}_{t'} = (f' (1) - f' (0)) / (1 - 0) = f' (1) - f' (0)\)、がある、任意のクローズドインターバル（閉区間）から\(1\)-ディメンショナル（次元）ユークリディアン\(C^\infty\)マニフォールド（多様体）の中への任意のディファレンシャブル（微分可能）マップ（写像）に対する平均値定理によって。
\(r = r_1 + t' (r_2 - r_1)\)としよう。
\(\langle v, M_r (r_2 - r_1) \rangle = {\partial_1 f'}_{t'} = f' (1) - f' (0) = \langle v, f (r_2) \rangle - \langle v, f (r_1) \rangle = \langle v, f (r_2) - f (r_1) \rangle\)。
ステップ4:
\(f (r_2) - f (r_1) = 0\)である時、\(0 = \Vert f (r_2) - f (r_1) \Vert \le \Vert M_r \Vert \Vert r_2 - r_1 \Vert\)が成立する。
\(f (r_2) - f (r_1) \neq 0\)としよう、これ以降。
\(v\)を、\(f (r_2) - f (r_1)\)の方向のユニット（単位）ベクトルとしよう。
\(\langle v, f (r_2) - f (r_1) \rangle = \Vert f (r_2) - f (r_1) \Vert\)。
\(\langle v, M_r (r_2 - r_1) \rangle \le \Vert v \Vert \Vert M_r (r_2 - r_1) \Vert = \Vert M_r (r_2 - r_1) \Vert\)、任意のリアル（実）またはコンプレックス（複素）インナープロダクト（内積）付きベクトルたちスペース（空間）に対するコーシー・シュワルツ不等式によって。
したがって、\(\Vert f (r_2) - f (r_1) \Vert \le \Vert M_r (r_2 - r_1) \Vert \le \Vert M_r \Vert \Vert r_2 - r_1 \Vert\)。
