コントラクション（収斂）マッピングの法則の記述/証明
話題
About: メトリックスペース（計量付き空間）
この記事の目次
開始コンテキスト
- 読者は、コンプリート（完備）メトリックスペース（計量付き空間）の定義を知っている。
- 読者は、マップ（写像）の定義を知っている。
ターゲットコンテキスト
- 読者は、コントラクション（収斂）マッピングの法則の記述および証明を得る。
オリエンテーション
本サイトにてこれまで議論された定義たちの一覧があります。
本サイトにてこれまで議論された命題たちの一覧があります。
本体
1: 構造化された記述
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\(M\): \(\in \{\text{ 全てのコンプリート（完備）メトリックスペース（計量付き空間）たち }\}\)
\(f\): \(: M \to M\)
//
ステートメント（言明）たち:
\(\exists r \in \mathbb{R} \text{ で、以下を満たすもの、つまり、 } 0 \le r \lt 1 (\forall m_1, m_2 \in M (dist (f (m_1), f (m_2)) \le r dist (m_1, m_2)))\)
\(\implies\)
\(!\exists m \in M (f (m) = m \land \forall m' \in M (lim_{j \to \infty} f^k (m') = m))\)
//
\(m\)は、"固定されたポイント"と呼ばれる。
2: Proof
Whole Strategy: Step 1: see that \(f^1 (m'), f^2 (m'), ...\) is a Cauchy sequence and take the convergence, \(m\); Step 2: conclude the proposition.
Step 1:
\(dist (f^{j + 1} (m'), f^j (m')) \le r dist (f^j (m'), f^{j - 1} (m')) \le r^2 dist (f^{j - 1} (m'), f^{j - 2} (m')) \le ... \le r^j dist (f (m'), m')\).
\(dist (f^{j + l} (m'), f^j (m')) \le dist (f^{j + l} (m'), f^{j + l - 1} (m')) + dist (f^{j + l - 1} (m'), f^{j + l - 2} (m')) + ... + dist (f^{j + 1} (m'), f^j (m')) \le (r^{j + l - 1} + r^{j + l -2} + . . . + r^j) dist (f (m'), m') = r^j (r^l - 1) / (r - 1) dist (f (m'), m')\).
So, \(f^1 (m'), f^2 (m'), ...\) is a Cauchy sequence, and as \(M\) is complete, the sequence converges to an \(m\).
Step 2:
As \(dist (f (m_1), f (m_2)) \le r dist (m_1, m_2)\), \(f\) is continuous, and so, \(f (m) = \lim_{j \to \infty} f (f^j (m')) = \lim_{j \to \infty} f^{j + 1} (m') = m\).
\(m\) is unique, because for any fixed points, \(m_1\) and \(m_2\), \(dist (m_1, m_2) = dist (f (m_1), f (m_2)) \le r dist (m_1, m_2)\), which is possible only if \(dist (m_1, m_2) = 0\).
