# 偏導數：由差商極限推出二次多項式的偏導公式，並計算一點的梯度

[← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-partial-derivative/)

這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。

derivation-mko-partial-derivative-01 · production-20261019-adopted-96



## 目標與範圍

對係數依 [1,x,y,x²,xy,y²] 排列的二次多項式 f，從差商極限的定義證明 ∂f/∂x=c_1+2c_3x+c_4y、∂f/∂y=c_2+c_4x+2c_5y。再對 c=(1,−2,3,1,2,−1) 算出 (1,2) 的偏導與梯度 (4,1)，並說明單一非零 h 的差商（5 或 41/10）與同時移動兩個座標（極限 5）都不是 x 偏導。

只處理 G1 的二變數二次多項式切片（MKO 假設 a1），偏導以差商極限精確推導。不以偏導存在推出一般函數的連續或全微分（a2）；錯誤控制中的非多項式例子只作對照。不改動 canonical MKO 或其英文 edition。





## 已知條件與符號


- func_limit_def
- abs_rules
- order_basics
- distributive
- power_laws


- G1 — f(x,y)=c_0+c_1x+c_2y+c_3x²+c_4xy+c_5y²，係數為整數，次序固定為 [1,x,y,x²,xy,y²]，f 在 ℝ² 上處處有定義（MKO 假設 a1、a2）。
- G2 — 實例：c=(1,−2,3,1,2,−1)，即 f(x,y)=1−2x+3y+x²+2xy−y²，點 (1,2)。


- c=(c_0,c_1,c_2,c_3,c_4,c_5) — 依 [1,x,y,x²,xy,y²] 次序的係數
- f(x,y) — 二次多項式
- h — 非零增量
- q_x(h) — x 方向差商 (f(x+h,y)−f(x,y))/h
- f_x,\ f_y — x 偏導與 y 偏導
- \nabla f=(f_x,f_y) — 梯度：偏導的有序收集





## 規則與來源


- func_limit_def · prerequisite — 函數極限：lim_{x→a} f(x)=L 表示對每個 ε>0，存在 δ>0，使所有滿足 0<|x−a|<δ 的定義域點 x 都有 |f(x)−L|<ε（a 須為定義域的極限點）。
- abs_rules · prerequisite — 絕對值（實數）：|u|=u（u≥0）、|u|=−u（u<0）；|u|≥0；|uv|=|u||v|；三角不等式 |u+v|≤|u|+|v|；|u|<r ⇔ −r<u<r。
- order_basics · prerequisite — 實數的序：任兩數恰有 u<v、u=v、u>v 之一；u<v 且 v<w 推出 u<w；u<v 推出 u+w<v+w；u<v 且 w>0 推出 uw<vw；u<v 且 w<0 推出 uw>vw。
- distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。
- power_laws · prerequisite — 整數指數律（底數非零或指數為正整數）：a^m·a^n=a^{m+n}，(a^m)^n=a^{mn}，(ab)^n=a^n b^n，a^0=1。
- def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
- add_inverse · prerequisite — 加法反元素：每個 u 都有 −u，使 u+(−u)=0；u−v 定義為 u+(−v)。
- mul_comm · prerequisite — 乘法交換律：uv=vu（在交換的數系中，例如 ℤ、ℚ、ℝ、ℂ）。
- add_comm · prerequisite — 加法交換律：u+v=v+u。
- mul_inverse_nonzero · prerequisite — 非零數的倒數：在 ℚ、ℝ、ℂ 中，若 u≠0，存在 1/u 使 u·(1/u)=1；對 u≠0 定義 v/u 為 v·(1/u)。u=0 時沒有倒數，v/0 不定義。
- frac_rules · prerequisite — 分數運算（分母皆非零）：a/c+b/c=(a+b)/c；(a/b)(c/d)=(ac)/(bd)；(a/b)/(c/d)=(ad)/(bc)（另需 c≠0）；a/b=(ak)/(bk)（k≠0）。
- exists_intro · prerequisite — ∃引入：若找到 a∈D 使 P(a) 成立，則 ∃x∈D, P(x)。
- forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
- eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
- mko_partial_def · cited — 二變數函數 f 在點 (x,y) 的 x 偏導，以 y 固定並令 h≠0 趨近 0 的差商極限定義；y 偏導類似。本輪對二次多項式做精確符號微分，不用單一有限差分代替極限。 · mko-partial-derivative
- mko_mvf_def · cited — 二變數實多項式 f:ℝ²→ℝ 的明示切片，係數依 [1,x,y,x²,xy,y²] 固定次序。 · mko-multivariable-real-function
- L_numerator_x · lemma — 對所有實數 x、y、h：f(x+h,y)−f(x,y)=h(c_1+2c_3x+c_4y)+c_3h²。
- L_affine_limit · lemma — 對實常數 A、B，函數 h↦A+Bh 在 h≠0 上有 lim_{h→0}(A+Bh)=A。





## 逐步主鏈

S01 · definition操作前

f_x(x,y)

操作後

\lim_{h\to0,\ h\neq0}\frac{f(x+h,y)-f(x,y)}{h}

條件：y\ \text{fixed}

規則：mko_partial_def · 依賴：mko_partial_def

葉節點依據：mko_partial_def + def_unfold

依 MKO 展開 x 偏導：y 固定不動，只讓第一個座標增加 h（h≠0），取差商後令 h→0。y 偏導則固定 x、只動第二個座標（MKO 段落 0）。偏導是一個極限，不是某一個 h 的差商值。



S02 · definition操作前

c=(c_0,c_1,c_2,c_3,c_4,c_5)

操作後

f(x,y)=c_0+c_1x+c_2y+c_3x^2+c_4xy+c_5y^2

條件：無

規則：mko_mvf_def · 依賴：G1, mko_mvf_def

葉節點依據：mko_mvf_def + def_unfold

依固定次序把係數向量讀成多項式。之後的推導對任意係數成立，最後再代入 G2 的實例。



S03 · equivalent操作前

f(x+h,y)-f(x,y)

操作後

h(c_1+2c_3x+c_4y)+c_3h^2

條件：無

規則：L_numerator_x · 依賴：S02, L_numerator_x

葉節點依據：L_numerator_x + distributive

引理 L_numerator_x（S03.1、S03.2 證明）：分子是 h 的二次式，常數項為 0。N1 在 3^9 個格點上驗證這個多項式恆等式（每個變數次數至多 2，足以判定）。



S04 · equivalent操作前

\frac{h(c_1+2c_3x+c_4y)+c_3h^2}{h}

操作後

q_x(h)=(c_1+2c_3x+c_4y)+c_3h\quad(h\neq0)

條件：h\neq0

規則：mul_inverse_nonzero · 依賴：S03, mul_inverse_nonzero

葉節點依據：mul_inverse_nonzero + frac_rules + power_laws

因 h≠0，可以乘以 1/h：h·A/h=A、c_3h²/h=c_3h。所以對每個非零 h，差商是 h 的仿射式 A+Bh，其中 A=c_1+2c_3x+c_4y、B=c_3。h=0 時差商沒有定義，但極限不看 h=0。



S05 · theorem_application操作前

\lim_{h\to0}\big(A+Bh\big)

操作後

A

條件：A=c_1+2c_3x+c_4y,\ B=c_3

規則：L_affine_limit · 依賴：S04, L_affine_limit

葉節點依據：L_affine_limit + func_limit_def

引理 L_affine_limit（S05.1、S05.2 以 ε-δ 證明）：仿射式 A+Bh 在 h→0 時的極限是 A。這把極限從「直覺代入 h=0」變成可核對的論證。



S06 · implies操作前

f_x(x,y)=\lim_{h\to0}q_x(h)

操作後

f_x(x,y)=c_1+2c_3x+c_4y

條件：無

規則：L_affine_limit · 依賴：S01, S04, S05

葉節點依據：L_affine_limit + def_unfold

S04 說差商在 h≠0 時是 A+Bh，S05 說它的極限是 A。依 S01 的定義，x 偏導存在且等於 A=c_1+2c_3x+c_4y。這是對每一點 (x,y) 與任意係數成立的精確公式。



S07 · implies操作前

\frac{f(x,y+h)-f(x,y)}{h}=(c_2+c_4x+2c_5y)+c_5h

操作後

f_y(x,y)=c_2+c_4x+2c_5y

條件：h\neq0; x\ \text{fixed}

規則：L_affine_limit · 依賴：S01, S02, S05

葉節點依據：L_affine_limit + distributive + mul_inverse_nonzero

y 偏導固定 x、只動 y。同樣逐項相減：f(x,y+h)−f(x,y)=h(c_2+c_4x+2c_5y)+c_5h²（N2 為恆等式），除以 h≠0 得仿射式 A'+B'h，A'=c_2+c_4x+2c_5y、B'=c_5。由 L_affine_limit，f_y=A'。



S08 · equivalent操作前

c=(1,-2,3,1,2,-1)

操作後

f_x=-2+2x+2y,\quad f_y=3+2x-2y

條件：無

規則：eq_replace · 依賴：S06, S07, G2

葉節點依據：eq_replace + numeric_evaluation

代入 c_1=−2、c_2=3、c_3=1、c_4=2、c_5=−1：f_x=−2+2·1·x+2y=−2+2x+2y；f_y=3+2x+2·(−1)·y=3+2x−2y。



S09 · equivalent操作前

(x,y)=(1,2)

操作後

f_x(1,2)=4,\ \ f_y(1,2)=1,\ \ \nabla f(1,2)=(4,1)

條件：無

規則：numeric_evaluation · 依賴：S08

葉節點依據：numeric_evaluation

f_x(1,2)=−2+2+4=4（N3）；f_y(1,2)=3+2−4=1（N4）。梯度只是依座標次序收集兩個偏導：(4,1)（MKO 段落 1）。



S10 · implies操作前

\frac{f(1+h,2)-f(1,2)}{h}

操作後

\frac{4h+h^2}{h}=4+h\ \xrightarrow{h\to0}\ 4

條件：h\neq0

規則：L_affine_limit · 依賴：G2, S04, S09

葉節點依據：L_affine_limit + numeric_evaluation + distributive

直接核對實例：f(1,2)=6（N5），f(1+h,2)−6=4h+h²（N6 為 h 的恆等式），差商為 4+h，極限 4，與 S09 一致。這是一般公式之外的獨立計算。



S11 · implies操作前

q_x(h)=4+h

操作後

q_x(1)=5,\ \ q_x(\tfrac1{10})=\tfrac{41}{10},\ \ q_x(h)\neq4\ \text{for every}\ h\neq0

條件：h\neq0

規則：order_basics · 依賴：S10

葉節點依據：order_basics + numeric_evaluation

h=1 給差商 (f(2,2)−6)/1=5（N7）；h=1/10 給 41/10（N8）。事實上 q_x(h)=4+h 對每個非零 h 都不等於 4。所以任何單一非零 h 的差商都不是偏導；偏導是 h→0 的極限（MKO 段落 2：有限差分只是近似或差商樣本）。



S12 · implies操作前

\frac{f(1+h,2+h)-f(1,2)}{h}

操作後

\frac{5h+2h^2}{h}=5+2h\ \xrightarrow{h\to0}\ 5\neq4=f_x(1,2)

條件：h\neq0

規則：L_affine_limit · 依賴：G2, S09, L_affine_limit

葉節點依據：L_affine_limit + numeric_evaluation + distributive

若同時移動兩個座標：f(1+h,2+h)−6=5h+2h²（N9 為恆等式），差商 5+2h，由 L_affine_limit 極限為 5。這是沿 (1,1) 方向的變化率，在本例等於 f_x+f_y=4+1，不是 x 偏導 4。偏導必須固定另一個座標（MKO 指出的誤解）。



S13 · implies操作前

\text{S06 to S12}

操作後

f_x=c_1+2c_3x+c_4y,\ f_y=c_2+c_4x+2c_5y;\ \nabla f(1,2)=(4,1)

條件：無

規則：and_intro_elim · 依賴：S06, S07, S09, S11, S12

葉節點依據：and_intro_elim

總結：由差商極限證得二次多項式偏導公式；實例在 (1,2) 的梯度為 (4,1)；單一 h 的差商（5、41/10）與同時移動兩座標的極限（5）都不是 x 偏導。







## 局部子步與引理

S03.1 · equivalent操作前

c_0,\ c_1x,\ c_2y,\ c_3x^2,\ c_4xy,\ c_5y^2\ \text{at}\ (x+h,y)\ \text{minus at}\ (x,y)

操作後

0,\ c_1h,\ 0,\ c_3(2xh+h^2),\ c_4hy,\ 0

條件：無

規則：distributive · 依賴：S02, power_laws, distributive

葉節點依據：distributive + power_laws + add_inverse

逐項相減：常數項、c_2y、c_5y² 不含 x，因為 y 固定而相消為 0；c_1(x+h)−c_1x=c_1h；c_3((x+h)²−x²)=c_3(2xh+h²)，用到 (x+h)²=x²+2xh+h²；c_4((x+h)y−xy)=c_4hy。



S03.2 · equivalent操作前

c_1h+c_3(2xh+h^2)+c_4hy

操作後

h(c_1+2c_3x+c_4y)+c_3h^2

條件：無

規則：distributive · 依賴：S03.1, distributive

葉節點依據：distributive + mul_comm + add_comm

把含 h 一次方的項提出 h：c_1h+2c_3xh+c_4yh=h(c_1+2c_3x+c_4y)，剩下 c_3h²。這證得引理 L_numerator_x。



S05.1 · implies操作前

\varepsilon>0

操作後

\delta=\frac{\varepsilon}{|B|+1}>0

條件：\varepsilon>0

規則：exists_intro · 依賴：func_limit_def, abs_rules

葉節點依據：exists_intro + abs_rules + order_basics

任取 ε>0。|B|+1≥1>0，所以 δ=ε/(|B|+1) 是正數。加 1 是為了在 B=0 時也不會除以 0。



S05.2 · implies操作前

0<|h|<\delta

操作後

|(A+Bh)-A|=|B||h|\le|B|\delta=\frac{|B|}{|B|+1}\varepsilon<\varepsilon

條件：0<|h|<\delta

規則：abs_rules · 依賴：S05.1, abs_rules, order_basics

葉節點依據：abs_rules + order_basics + forall_intro

|(A+Bh)−A|=|Bh|=|B||h|。|h|<δ 且 |B|≥0 給 |B||h|≤|B|δ=|B|ε/(|B|+1)。因 |B|<|B|+1，比值 |B|/(|B|+1)<1，再乘以正的 ε 得 <ε。ε 任意，所以極限是 A；S05.1 與 S05.2 證得引理 L_affine_limit。







## 逐步反向審查


- S13 · premise_audit · S06, S07, S09 — 只合取已證結論；不宣稱 f 全微分或連續（雖然多項式事實上如此，本稿不證）。
- S12 · premise_audit · L_affine_limit, numeric_evaluation — 只說明這個極限不是 f_x；「方向導數等於 f_x+f_y」只是本例的數值觀察，本稿不證明一般公式。
- S11 · premise_audit · S10, order_basics — 4+h=4 ⇔ h=0，而 h=0 被排除；這個結論只針對本實例。
- S10 · premise_audit · L_affine_limit, numeric_evaluation — 與 S06 的公式互相核對；只對這個實例。
- S09 · inverse_equivalence · numeric_evaluation — 精確整數求值。
- S08 · inverse_equivalence · eq_replace — 等量代換，雙向成立。
- S07 · premise_audit · L_affine_limit, distributive, mul_inverse_nonzero — 與 S03 到 S06 相同的四步，只是 x、y 的角色互換；N2 獨立驗證分子恆等式。
- S06 · premise_audit · S04, S05, S01 — 兩個函數在 h≠0 上相同，極限就相同；h=0 的值不參與。
- S05.2 · premise_audit · abs_rules, order_basics, forall_intro — 用到 |uv|=|u||v|、乘非負數保序、乘正數保持嚴格不等；只宣稱上界。
- S05.1 · premise_audit · abs_rules, order_basics — 正數除以正數為正；δ 只依賴 ε 與 B。
- S05 · premise_audit · L_affine_limit, func_limit_def — 0 是 ℝ∖{0} 的極限點，所以函數極限有意義。
- S04 · inverse_equivalence · mul_inverse_nonzero, frac_rules — 乘 1/h 與乘 h 互逆，前提 h≠0。
- S03.2 · inverse_equivalence · distributive, mul_comm — 提出公因子與展開互逆。
- S03.1 · inverse_equivalence · distributive, power_laws, add_inverse — 每一項都是恆等展開；只有含 x 的項留下，這正是「固定 y」的效果。
- S03 · inverse_equivalence · L_numerator_x, distributive — 這是代數恆等式，對所有 x、y、h 成立，雙向皆可。
- S02 · premise_audit · mko_mvf_def — 係數次序是輸入契約，錯置可能改變多項式與偏導；但不是每個置換都一定改變結果，例如交換相等係數不變。本題 c_1=−2、c_2=3 不相等，交換後確會改變所列偏導。
- S01 · premise_audit · mko_partial_def — 只展開定義；h=0 被排除，因為差商在 h=0 沒有定義。





## 錯誤控制與反例

不要同時移動兩個座標MKO 指出的誤解之一是同時改變兩個座標。S12 中 (f(1+h,2+h)−f(1,2))/h→5，而 x 偏導是 4。x 偏導的定義要求 y 固定，只有第一個座標加 h。

一個 h 的差商不是偏導MKO 的另一個誤解是以一個非零 h 的差商聲稱偏導存在。本例 q_x(h)=4+h，對每個非零 h 都不是 4（h=1 給 5，h=1/10 給 41/10）。即使某種有限差分碰巧給出正確數字（例如中心差分 (q_x(1)+q_x(−1))/2=(5+3)/2=4），那也只是二次多項式的特性，不是存在性的證明：對 u(x,y)=|x| 在 (0,0)，中心差分 (|h|−|−h|)/(2h)=0 對每個 h≠0 成立，但 x 偏導不存在（右差商為 1、左差商為 −1）。

偏導存在不推出連續MKO 假設 a2 提醒偏導存在不用來推出一般函數連續。例：g(x,y)=xy/(x²+y²)（(x,y)≠(0,0)）、g(0,0)=0。g(x,0)=0 與 g(0,y)=0 對所有 x、y 成立，所以兩個偏導在原點存在且為 0；但沿 y=x，g(t,t)=1/2 對所有 t≠0 成立，不趨近 g(0,0)=0，所以 g 在原點不連續。


- q_x(1)=5，所以 f_x(1,2)=5 → reject — 偏導是 h→0 的極限：q_x(h)=4+h→4（S10、S11）。
- (f(1+h,2+h)−f(1,2))/h→5，所以 x 偏導是 5 → reject — 這同時移動了 y；固定 y=2 的極限是 4（S12）。
- 函數在一點的兩個偏導都存在，所以它在該點連續 → reject — g(x,y)=xy/(x²+y²)、g(0,0)=0 在原點兩偏導皆為 0，但 g(t,t)=1/2（錯誤控制 3）。
- 中心差分 (q(h)+q(−h))/2 對某個 h 給出一個數，就證明了偏導存在且等於它 → reject — u(x,y)=|x| 在 (0,0) 的中心差分恆為 0，但 x 偏導不存在（錯誤控制 2）。





## 結論與限制

對 f=c_0+c_1x+c_2y+c_3x²+c_4xy+c_5y²，差商在 h≠0 時為仿射式，故 f_x=c_1+2c_3x+c_4y、f_y=c_2+c_4x+2c_5y。對 c=(1,−2,3,1,2,−1)：f_x=−2+2x+2y、f_y=3+2x−2y，在 (1,2) 得梯度 (4,1)。q_x(h)=4+h 對任何非零 h 都不等於 4；同時移動兩座標的極限為 5。


- 錯誤控制 2、3 的非多項式例子以文字論證，沒有拆成編號步驟；本稿主結論不依賴它們。
- 梯度的幾何意義、全微分與高階偏導（MKO 的 formal next）不在範圍內。





## 驗證及來源綁定

11 個本稿宣告算術檢查；只支持所列算式。


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: cec61d27ae749c4333888ce08539fdb4a14ce72bd62e3e9d85ee86ac92f9eab1
- original source SHA-256: 277ef1a5d5807fe90f5ab864bef246dbbc0d025aaa5183b9a9d7f44340c942e7
- Lean: NOT_RUN · independent AI: NOT_MEASURED

[同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-partial-derivative-01.json)