# 漸近資源界

漸近上界、下界與緊界必須相對輸入大小、成本模型及全尾段量化定義。

mko-asymptotic-resource-bound · definition · v0.10.0



## 數學敘述

對非負函數 f,g:N→R，f∈O(g) 表示存在 c>0、N，使所有 n≥N 均有 f(n)≤c·g(n)；f∈Ω(g) 反向比較；f∈Θ(g) 表示兩者同時成立。輸入大小與成本模型是聲明的一部分。





## 代表公式（精確 TeX）

f(n)=g(n)





## 成立條件


- 自然數輸入 n 從 0 起；題目明示函數族與非負係數。
- 所有漸近結論都需全尾段 witness 或明示函數族定理；有限 benchmark 只作觀察。





## 符號作用域


- f — 待界定資源函數
- g — 比較函數
- n — 輸入大小





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

大 O 不是等號，也不等於只比較某個 n；常數因子與有限前綴被吸收到 witness 中。

對非負係數多項式，最高非零次數決定其 Θ 次數；題目會保留全零多項式與常數邊界。

不同成本模型可以給同一算法不同函數。沒有先固定基本操作、輸入表示與 size，就不能比較資源界。

用幾個 benchmark 點證明漸近關係，或把 O、Ω、Θ 當成可互換符號。





## 已採用的推導導讀

[漸近資源界：證明 3n²+5n+2∈Θ(n²) 並排除 Θ(n)](https://ocme.evemisslab.com/zh-Hant/derivations/derivation-mko-asymptotic-resource-bound-01/)原始 MKO 保留；導讀有自己的追加式修訂與驗證界線，不代表新 Lean 證明。





## 前置知識


- [自然數](https://ocme.evemisslab.com/zh-Hant/mko/mko-natural-number/) — 輸入大小以自然數索引。
- [四則運算](https://ocme.evemisslab.com/zh-Hant/mko/mko-arithmetic-operations/) — 成本函數與 witness 使用精確運算。
- [實數大小與順序](https://ocme.evemisslab.com/zh-Hant/mko/mko-order-relation/) — 上界與下界是全尾段不等式。
- [函數映射](https://ocme.evemisslab.com/zh-Hant/mko/mko-function-mapping/) — 資源量是由輸入大小到非負數的函數。





## 驗證界線

本輪只在明示非負單項式／多項式族建立全尾段結論；不從有限測量外推一般算法複雜度。

not_formalized

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





## 下一個義務

綁定標準 asymptotic predicates、eventually filter 與具 witness 的算法成本函數。





## 同源結構化資料

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

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