ユークリディアンノルム付きユークリディアンベクトルたちスペース（空間）ODEで初期コンディションを持つものに対する解のローカルユニーク性の記述/証明
話題
About: ベクトルたちスペース（空間）
この記事の目次
開始コンテキスト
- 読者は、ユークリディアンノルム付きユークリディアンベクトルたちスペース（空間）の定義を知っている。
- 読者は、ノルム付きベクトルたちスペース（空間）の任意のサブセット（部分集合）からノルム付きベクトルたちスペース（空間）のサブセット（部分集合）の中へのマップ（写像）のポイントにおけるデリバティブ（微分係数）の定義を知っている。
- 読者は、コンティヌアス（連続）な、トポロジカルスペース（空間）たちマップ（写像）の定義を知っている。
- 読者は、ハイネ-ボレル定理: 任意のユークリディアントポロジカルスペース（空間）の任意のサブセット（部分集合）はコンパクトである、もしも、それがクローズド（閉）でバウンデッド（有界）である場合、そしてその場合に限ってを認めている。
- 読者は、任意のトポロジカルスペース（空間）に対して、当該スペース（空間）の任意のコンパクトサブセット（部分集合）で任意のサブスペース（部分空間）内に包含されているものは当該サブスペース（部分空間）上でコンパクトであるという命題を認めている。
- 読者は、任意のトポロジカルスペース（空間）たち間任意のコンティニュアスマップ（連続写像）に対して、当該ドメイン（定義域）の任意のコンパクトサブセット（部分集合）のイメージ（像）は当該コドメイン（余域）のコンパクトサブセット（部分集合）であるという命題を認めている。
- 読者は、任意のトポロジカルスペース（空間）に対して、任意のファイナイト（有限）数コンパクトサブセット（部分集合）たちのユニオン（和集合）はコンパクトであるという命題を認めている。
- 読者は、任意のコンパクトトポロジカルパラメータスペース（空間）を持つ、任意のユークリディアンメトリックスペース（計量付き空間）の任意のサブスペース（部分空間）でインデュースト（誘導された）トポロジーを持つものから任意のユークリディアンメトリックスペース（計量付き空間）の任意のサブスペース（部分空間）でインデュースト（誘導された）トポロジーを持つものの中への任意のコンティニュアスマップ（連続写像）でローカルにリプシッツ評価たちを満たすものに対して、当該マップ（写像）の任意のコンパクトサブスペース（部分空間）上へのリストリクション（制限）はリプシッツ評価たちを満たすという命題を認めている。
- 読者は、任意のオープンインターバル（開区間）から任意のユークリディアン\(C^\infty\)マニフォールド（多様体）でユークリディアンノルムを持つものの中への任意のディファレンシャブル（微分可能）マップ（写像）に対して、各ポイントイメージ（像）のノルムは、非ネガティブ（負）インターバル（区間）間のあるディファレンシャブルマップ（微分可能写像）である初期コンディションを持つものによってアッパーバウンデッド（上から限られる）である、もしも、非ネガティブ（負）インターバル（区間）間のあるリプシッツマップ（写像）で特定コンディションたちを満たすものがある場合、という命題を認めている。
ターゲットコンテキスト
- 読者は、ユークリディアンノルム付きユークリディアンベクトルたちスペース（空間）オーディナリーディファレンシャルエクエイション（常微分方程式）で初期コンディションを持つものに対する解のローカルユニーク性の記述および証明を得る。
オリエンテーション
本サイトにてこれまで議論された定義たちの一覧があります。
本サイトにてこれまで議論された命題たちの一覧があります。
本体
1: 構造化された記述
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\(\mathbb{R}^d\): \(= \text{ 当該ユークリディアンノルム付きユークリディアンベクトルたちスペース（空間） }\)で当該ノルムによってインデュースト（誘導された）メトリック（計量）によってインデュースト（誘導された）トポロジーを持つもの
\(\mathbb{R}\): \(= \text{ 当該ユークリディアンノルム付きユークリディアンベクトルたちスペース（空間） }\)
\(U\): \(\in \{\mathbb{R}^d \text{ の全てのオープンサブセット（開部分集合）たち }\}\)
\(J\): \(\in \{\mathbb{R} \text{ の全てのインターバル（区間）たち }\}\)
\(f\): \(: U \times J \to \mathbb{R}^d\), \(\in \{\text{ 全ての } C^0 \text{ マップ（写像）たち }\}\)で、以下を満たすもの、つまり、\(\forall x_0 \in U (\exists U_{x_0} \in \{x_0 \text{ の } U \text{ 上における全てのオープンネイバーフッド（開近傍）たち }\} (\forall x_1, x_2 \in U_{x_0}, \forall r \in J (\Vert f (x_1, r) - f (x_2, r) \Vert \le L_{x_0} \Vert x_1 - x_2 \Vert)))\)
\(r_0\): \(\in J\)
\(x'_0\): \(\in U\)
//
ステートメント（言明）たち:
\(\exists J^` \in \{J \text{ の全てのオープンインターバル（開区間）たち }\} \text{ で、以下を満たすもの、つまり、 } r_0 \in J^`, \exists x: J^` \to U (d x / d r = f (x, r) \land x (r_0) = x'_0)\)
\(\implies\)
\(x\)は、\(J^`\)上方におけるユニーク解である
//
2: 注
本命題のあるユークリディアンノルム付きユークリディアンベクトルたちスペース（空間）オーディナリーディファレンシャルエクエイション（常微分方程式）である初期コンディションを持つものに対するあるクローズドインターバルドメイン（閉区間定義域）に対するローカルユニーク解存在、当該解のドメイン（定義域）エリアのある明確化を持ってに対するメリットは、これは任意の\(J^` \subseteq J\)上方の任意の解についてである一方、あるユークリディアンノルム付きユークリディアンベクトルたちスペース（空間）オーディナリーディファレンシャルエクエイション（常微分方程式）である初期コンディションを持つものに対するあるクローズドインターバルドメイン（閉区間定義域）に対するローカルユニーク解存在、当該解のドメイン（定義域）エリアのある明確化を持っては、その命題内で特定された任意のよりリストリクテッド（制限された）ドメイン（定義域）上方の解についてである。
3: 証明
全体戦略: ステップ1: \(J^`\)上方に何らか2個の解たち\(x_1 (t), x_2 (t)\)があったと仮定する; ステップ2: 各\(r_1 \in J^`\)に対して、以下を満たすあるバウンデッド（有界）オープンインターバル（開区間）\(J^{``} \subseteq J^`\)、つまり、\(r_0, r_1 \in J^{``}\)および\(\overline{J^{``}} \subseteq J^`\)、を取り、\(f \vert_{(x_1 (\overline{J^{``}}) \cup x_2 (\overline{J^{``}})) \times \overline{J^{``}}}\)はあるリプシッツ評価を満たすことを見る; ステップ3: \(J^{``}\)上方で、\(\Vert x_1 (r) - x_2 (r) \Vert \le e^{L_{J^{``}} \vert r - r_0 \vert} \Vert x_1 (r_0) - x_2 (r_0) \Vert\)であることを見る; ステップ4: 当該命題を結論する。
ステップ1:
\(J^`\)上方に何らかの2個の解たち\(x_1 (r), x_2 (r)\)があったと仮定しよう。
ステップ2:
各\(r_1 \in J^`\)に対して、以下を満たすあるバウンデッド（有界）オープンインターバル（開区間）\(J^{``} \subseteq J^`\)、つまり、\(r_0, r_1 \in J^{``}\)および\(\overline{J^{``}} \subseteq J^`\)、がある。
\(\overline{J^{``}}\)は\(J^`\)上でコンパクトである、ハイネ-ボレル定理: 任意のユークリディアントポロジカルスペース（空間）の任意のサブセット（部分集合）はコンパクトである、もしも、それがクローズド（閉）でバウンデッド（有界）である場合、そしてその場合に限っておよび任意のトポロジカルスペース（空間）に対して、当該スペース（空間）の任意のコンパクトサブセット（部分集合）で任意のサブスペース（部分空間）内に包含されているものは当該サブスペース（部分空間）上でコンパクトであるという命題によって。
\(x_j (\overline{J^{``}})\)は\(U\)上でコンパクトである、任意のトポロジカルスペース（空間）たち間任意のコンティニュアスマップ（連続写像）に対して、当該ドメイン（定義域）の任意のコンパクトサブセット（部分集合）のイメージ（像）は当該コドメイン（余域）のコンパクトサブセット（部分集合）であるという命題によって、そして、\(x_1 (\overline{J^{``}}) \cup x_2 (\overline{J^{``}})\)は\(U\)上でコンパクトである、任意のトポロジカルスペース（空間）に対して、任意のファイナイト（有限）数コンパクトサブセット（部分集合）たちのユニオン（和集合）はコンパクトであるという命題によって。
\(f\)の\((x_1 (\overline{J^{``}}) \cup x_2 (\overline{J^{``}})) \times \overline{J^{``}}\)上のリストリクション（制限）はあるリプシッツ評価を満たす、任意のコンパクトトポロジカルパラメータスペース（空間）を持つ、任意のユークリディアンメトリックスペース（計量付き空間）の任意のサブスペース（部分空間）でインデュースト（誘導された）トポロジーを持つものから任意のユークリディアンメトリックスペース（計量付き空間）の任意のサブスペース（部分空間）でインデュースト（誘導された）トポロジーを持つものの中への任意のコンティニュアスマップ（連続写像）でローカルにリプシッツ評価たちを満たすものに対して、当該マップ（写像）の任意のコンパクトサブスペース（部分空間）上へのリストリクション（制限）はリプシッツ評価たちを満たすという命題によって。
したがって、\(J^{``}\)上方で、\(\Vert d (x_1 - x_2) / d r \Vert = \Vert d x_1 / d r - d x_2 / d r \Vert = \Vert f (x_1 (r), r) - f (x_2 (r), r) \Vert \le L_{J^{``}} \Vert x_1 (r) - x_2 (r) \Vert\)。
ステップ3:
\(u: J^{``} \to \mathbb{R}^d = x_1 - x_2\)、\(g: [0, \infty) \to [0, \infty), r \mapsto e^{L_{J^{``}} r} \Vert x_1 (r_0) - x_2 (r_0) \Vert\)、\(h: [0, \infty) \to [0, \infty), r \mapsto L_{J^{``}} r\)としよう。
\(u\)はディファレンシャブル（微分可能）である; \(g\)はディファレンシャブル（微分可能）であり、\(g (0) = e^{L_{J^{``}} 0} \Vert x_1 (r_0) - x_2 (r_0) \Vert = \Vert x_1 (r_0) - x_2 (r_0) \Vert = \Vert u (r_0) \Vert\); \(h\)は\(L_{J^{``}}\)を持つあるリプシッツマップ（写像）である、\(\Vert \partial_1 u (r) \Vert \le h (\Vert u (r) \Vert)\)、上記に見られたとおり、そして、\(\partial_1 g (r) = h (g (r))\)。
したがって、任意のオープンインターバル（開区間）から任意のユークリディアン\(C^\infty\)マニフォールド（多様体）でユークリディアンノルムを持つものの中への任意のディファレンシャブル（微分可能）マップ（写像）に対して、各ポイントイメージ（像）のノルムは、非ネガティブ（負）インターバル（区間）間のあるディファレンシャブルマップ（微分可能写像）である初期コンディションを持つものによってアッパーバウンデッド（上から限られる）である、もしも、非ネガティブ（負）インターバル（区間）間のあるリプシッツマップ（写像）で特定コンディションたちを満たすものがある場合、という命題によって、\(\Vert u (r) \Vert \le g (\vert r - r_0 \vert)\)、それは、\(\Vert x_1 (r) - x_2 (r) \Vert \le e^{L_{J^{``}} \vert r - r_0 \vert} \Vert x_1 (r_0) - x_2 (r_0) \Vert\)。
しかし、\(x_1 (r_0) - x_2 (r_0) = 0\)であるから、\(\Vert x_1 (r_0) - x_2 (r_0) \Vert = 0\)、したがって、\(\Vert x_1 (r) - x_2 (r) \Vert \le 0\)、したがって、\(\Vert x_1 (r) - x_2 (r) \Vert = 0\)、したがって、\(x_1 (r) = x_2 (r)\)。
ステップ4:
\(r_1 \in J^`\)は恣意的であるから、そうした\(J^{``}\)たちは\(J^`\)をカバーする、そして、各\(J^{``}\)上方で\(x_1 = x_2\)であるから、\(J^`\)全体上方で\(x_1 = x_2\)。
