ユークリディアンノルム付きユークリディアンベクトルたちスペース（空間）ODEに対するインターバル（区間）上のユニークなグローバル解の存在に対する十分条件たちの記述/証明
話題
About: ノルム付きベクトルたちスペース（空間）
About: 微分方程式
この記事の目次
開始コンテキスト
ターゲットコンテキスト
- 読者は、任意のユークリディアンノルム付きユークリディアンベクトルたちスペース（空間）常微分方程式に対する、任意の初期条件に対してインターバル（区間）全体上のユニーク解があるためのいくつかの十分条件たちの記述および証明を得る。
オリエンテーション
本サイトにてこれまで議論された定義たちの一覧があります。
本サイトにてこれまで議論された命題たちの一覧があります。
本体
1: 構造化された記述
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\(\mathbb{R}^d\): \(= \text{ ユークリディアンノルム付きユークリディアンベクトルたちスペース（空間） }\)
\(\mathbb{R}\): \(= \text{ ユークリディアンノルム付きユークリディアンベクトルたちスペース（空間） }\)
\(J\): \(\subseteq \mathbb{R}\), \(= [t_1, t_e]\)
\(f\): \(: \mathbb{R}^d \times J \to \mathbb{R}^d\), \(\in \{\text{ 全ての } C^0 \text{ マップ（写像）たち }\}\)
\(\frac{dx}{dt} = f (x, t)\): = 常微分方程式で初期条件\(x (t_1) = x_{t_1}\)を持ったもの
//
ステートメントたち:
\(\forall t_0 \in J\)
(
\(\exists [t_0 - \epsilon_{t_0, 1}, t_0 + \epsilon_{t_0, 2}]\)、それは、\(t_0\)に対する任意の初期値\(x_{t_0}\)に対して当該方程式の当該初期条件に対するローカル解存在のための条件たちを満たす、ここで、\(\epsilon_{t_0, j}\)は\(\epsilon_{t_1, 1}\)および\(\epsilon_{t_e, 2}\)を除きゼロではない、そして、\(x_{t_0}\)に依存しない、\(t_0\)には依存してよいが、それが意味するのは、各\(t \in [t_0 - \epsilon_{t_0, 1}, t_0 + \epsilon_{t_0, 2}]\)に対してあるマップ（写像）\(x_{t_0} \mapsto x (t)\)があるということ、そして、当該マップ（写像）はバイジェクティブ（全単射）である
)
\(\implies\)
当該常微分方程式は\(J\)全体上でユニークな解を持つ。
//
2: 自然言語記述1
任意のユークリディアンノルム付きユークリディアンベクトルたちスペース（空間）\(\mathbb{R}^d\)および\(\mathbb{R}\)、任意のクローズドインターバル（閉区間）\(J \subseteq \mathbb{R} = [t_1, t_e]\)、任意の\(C^0\)マップ（写像）\(f: \mathbb{R}^d \times J \to \mathbb{R}^d\)に対して、常微分方程式\(\frac{dx}{dt} = f (x, t)\)で任意の初期条件\(x (t_1) = x_{t_1}\)を持つものは、\(J\)全体上でユニークな解を持つ、もしも、各ポイント\(t_0 \in J\)において、あるクローズドインターバル（閉区間）\([t_0 - \epsilon_{t_0, 1}, t_0 + \epsilon_{t_0, 2}]\)で、\(t_0\)に対する任意の初期値\(x_{t_0}\)に対して当該方程式の当該初期条件に対するローカル解存在のための条件たちを満たす、ここで、\(\epsilon_{t_0, j}\)は\(\epsilon_{t_1, 1}\)と\(\epsilon_{t_e, 2}\)を除きゼロでなく、\(x_{t_0}\)に依存しない、\(t_0\)には依存してよいが、それが意味するのは、各\(t \in [t_0 - \epsilon_{t_0, 1}, t_0 + \epsilon_{t_0, 2}]\)に対してあるマップ（写像）\(x_{t_0} \mapsto x (t)\)があるということ、そして当該マップ（写像）はバイジェクティブ（全単射）である、ものがある場合。
3: 証明1
\(t_0 \neq t_1, t_e\)に対するオープンインターバル（開区間）たち\((t_0 - \epsilon_{t_0, 1}, t_0 + \epsilon_{t_0, 2})\)、\([t_1, t_1 + \epsilon_{t_1, 2})\)、\((t_e - \epsilon_{t_e, 1}, t_e]\)たちは、コンパクトな\(J\)をカバーする、したがって、あるファイナイト（有限）サブカバー\([t_1, t_1 + \epsilon_{t_1, 2})、(t_2 - \epsilon_{t_2, 1}, t_2 + \epsilon_{t_2, 2})、...、(t_e - \epsilon_{t_e, 1}, t_e]\)がある。
\([t_1, t_1 + \epsilon_{t_1, 2})\)に対して、初期条件\(\overline{x} (t_1) = x_{t_1}\)に対し、ローカルユニーク解\(\overline{x}: [t_1, t_1 + \epsilon_{t_1, 2}) \to \mathbb{R}^d\)がある。\(x\)のリストリクション（制限）\(x \vert_{[t_1, t_1 + \epsilon_{t_1, 2})} = \overline{x}\)を定義しよう。
\([t_1, t_1 + \epsilon_{t_1, 2})\)に交わるあるインターバル（区間）\((t_{j_2} - \epsilon_{t_{j_2}, 1}, t_{j_2} + \epsilon_{t_{j_2}, 2})\)があり（ある交わるポイントを\(t_{1, j_2}\)と表記する ）、それに対する初期条件\(\overline{x} (t_{j_2}) = x_{t_{j_2}}\)によるローカルユニーク解がある、ここで、\(x_{t_{j_2}}\)は\(\overline{x} (t_{1, j_2}) = x (t_{1, j_2})\)であるように選べる、その理由は、"記述"で言及されたバイジェクティブ（全単射）マップ（写像）が存在すると仮定されていること。実のところ、\(\overline{x}\)は\(x\)とインターセクションエリア全体上で一致する、なぜなら、\(t_{1, j_2}\)の周りにあるインターバル（区間）があり、その上に当該初期条件によるユニーク解がある、それは、そこで\(x\)および\(\overline{x}\)と一致しなければならない、そして、もしも、\(x\)と\(\overline{x}\)がインターセクションエリア全体で一致しなかったら、\((t_{j_2} - \epsilon_{t_{j_2}, 1}, t_{j_2} + \epsilon_{t_{j_2}, 2})\)は別の解を持つことになる、\(t_{1, j_2}\)を通過した後で\(x\)へスイッチすることによって、または、\([t_1, t_1 + \epsilon_{t_1, 2})\)は別の解を持つことになる、\(t_{1, j_2}\)を通過した後で\(\overline{x}\)へスイッチすることによって。\(x\)を\([t_1, t_{j_2} + \epsilon_{t_{j_2}, 2})\)へ\(\overline{x}\)でもって拡張しよう。
そのように、\(x\)は\(J\)全体へ拡張できる。この拡張はユニークである、なぜなら、各ポイント\(t_{j_k}\)において、\(x_{t_{j_k}}\)はユニークに定められる。
4: 注1
本命題のためには、そうしたあるバイジェクティブ（全単射）マップ（写像）が存在することが必要である。各ポイントの周りにあるローカル解があるというだけでは、グローバル解の存在は保障されない、別の記事に記述されているとおり。
