# 壓縮映射定理

非空完備度量空間上的self-map若以固定q<1壓縮所有距離，則有唯一fixed point且Picard orbit收斂。

mko-contraction-mapping-theorem · theorem · v0.10.0



## 數學敘述

題族以完整finite metric與total self-map逐對驗d(Tx,Ty)≤q d(x,y)，固定0≤q<1。從任意x0完整產生Picard orbit，枚舉fixed points並核唯一性；exact rational metric下驗d(x_n,x*)≤q^n/(1-q)d(x_1,x_0)。finite metric自動complete但只證指定模型；q=1、非self-map、非complete空間與sampled-pairs不足均不得套定理。





## 代表公式（精確 TeX）

C(X,T,q)=x





## 成立條件


- finite metric matrix完整驗nonnegative、identity、symmetry與triangle inequality。
- mapping為complete total self-map，q為exact rational。





## 符號作用域


- C — 壓縮映射定理
- X — 完備度量空間
- T — 壓縮self-map
- q — 壓縮常數
- x — 唯一不動點





## 直觀、定義與常見誤解

完整metric/self-map/contraction資格先於定理。

Picard orbit與唯一fixed point分開核對。

geometric tail給exact error bound。

只抽樣幾對點、允許q=1或忽略self-map/completeness仍宣稱唯一fixed point。





## 已採用的推導導讀

[有限度量的完整收縮證書](https://ocme.evemisslab.com/zh-Hant/derivations/derivation-mko-contraction-mapping-theorem-01/)原始 MKO 保留；導讀有自己的追加式修訂與驗證界線，不代表新 Lean 證明。





## 前置知識


- [軌道、固定點與週期點](https://ocme.evemisslab.com/zh-Hant/mko/mko-orbit-fixed-periodic/) — Picard orbit與fixed point。
- [完備度量空間](https://ocme.evemisslab.com/zh-Hant/mko/mko-complete-metric-space/) — completeness。
- [度量空間中的收斂](https://ocme.evemisslab.com/zh-Hant/mko/mko-metric-convergence/) — Cauchy/convergence。
- [無窮級數](https://ocme.evemisslab.com/zh-Hant/mko/mko-infinite-series/) — geometric tail bound。





## 驗證界線

finite model證書不取代一般complete-space theorem proof。

not_formalized

這不表示內容錯誤；只表示尚未登錄可重播的計算或形式證據。





## 下一個義務

加入Picard–Lindelöf等應用。





## 同源結構化資料

本頁與互動版共用同一個物件與既有語言 edition；未新增證明或人工審定。

[原始 MKO JSON](https://ocme.evemisslab.com/data/mko/contraction-mapping-theorem.json) · [純文字 Markdown](https://ocme.evemisslab.com/zh-Hant/mko/mko-contraction-mapping-theorem/index.md)