# 凸最佳化問題：資格核對、可行性、單點求值與兩候選比較，以及它們不能推出什麼

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

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

derivation-mko-convex-optimization-problem-01 · production-20261019-adopted-96



## 目標與範圍

問題 P：在可行域 X=[0,5] 上最小化 f(x)=x²−6x+10。（一）分別核對可行域凸與目標凸，判定 P 具凸問題資格；（二）判定候選 x₁=1、x₂=4、x₃=−1 的可行性；（三）求 f(1)、f(4) 並比較兩個可行候選；（四）說明兩候選中較低者不因此是 P 的最優解，並以 P′：在 X′=(0,1] 上最小化 x² 說明凸問題不一定有最小值點。

停在 MKO 的切片內：一元明示實區間作可行域、整係數二次目標；只做資格核對、單點可行性、單點求值與兩個可行候選的比較。為否證「某點最優」可再求一個可行點的值；不給任何點的全域最優證書，不引入 KKT、對偶、通用求解器或收斂結果；不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- order_basics
- square_nonneg
- distributive
- numeric_evaluation
- quantifier_negation
- forall_intro


- G1 — 問題 P：在 X=[0,5] 上最小化 f(x)=x²−6x+10（整係數 a=1、b=−6、c=10）。
- G2 — 提出的候選：x₁=1、x₂=4、x₃=−1。
- G3 — 問題 P′：在 X′=(0,1]={x ∣ 0<x≤1} 上最小化 f₀(x)=x²。


- P:\ \min_{x\in X} f(x) — 問題 P：在 X 上最小化 f
- X=[0,5],\ X'=(0,1] — 可行域
- f(x)=x^2-6x+10 — P 的目標函數
- f_0(x)=x^2 — P′ 的目標函數
- G_q(x,y,\lambda) — Jensen gap：λq(x)+(1−λ)q(y)−q(λx+(1−λ)y)
- x^\ast — 最小值點（全域最優解）





## 規則與來源


- 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。
- square_nonneg · prerequisite — 實數平方非負：對所有實數 u，u²≥0，且 u²=0 ⇔ u=0。
- distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。
- forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
- def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
- power_laws · prerequisite — 整數指數律（底數非零或指數為正整數）：a^m·a^n=a^{m+n}，(a^m)^n=a^{mn}，(ab)^n=a^n b^n，a^0=1。
- add_inverse · prerequisite — 加法反元素：每個 u 都有 −u，使 u+(−u)=0；u−v 定義為 u+(−v)。
- mul_one · prerequisite — 乘法單位元：1·u=u。
- mul_comm · prerequisite — 乘法交換律：uv=vu（在交換的數系中，例如 ℤ、ℚ、ℝ、ℂ）。
- mul_zero · prerequisite — 乘以零：u·0=0。理由：u·0=u·(0+0)=u·0+u·0，兩邊同減 u·0 得 0=u·0。
- and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
- set_builder · prerequisite — 集合建構式：x∈{y∈A ∣ P(y)} 當且僅當 x∈A 且 P(x)。
- case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
- 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）。
- mko_cvxopt · cited — 最小化問題只有在目標函數凸且可行域凸時，才具本條目的凸問題資格。本輪只核一元區間與二次目標的資格、單點可行性、單點求值及兩個可行候選的局部比較；不由資格、單點或兩點比較宣稱已找到全域解。 · mko-convex-optimization-problem
- mko_cvxf · cited — 在凸定義域 C 上，f 為凸若對所有 x,y∈C 及 λ∈[0,1]，f(λx+(1−λ)y)≤λf(x)+(1−λ)f(y)。 · mko-convex-function
- mko_cvxset · cited — 實向量空間的子集 C 為凸，若對所有 x,y∈C 及所有 λ∈[0,1]，λx+(1−λ)y 仍屬於 C。 · mko-convex-set
- mono_nonneg · prerequisite — 乘以非負數保持不等號：若 u≤v 且 w≥0，則 wu≤wv（w>0 時由實數的序，w=0 時兩邊都是 0）。
- ineq_add · prerequisite — 不等式相加：若 u₁≤v₁ 且 u₂≤v₂，則 u₁+u₂≤v₁+v₂；若其中一個是嚴格不等，和也是嚴格不等。
- minimizer_def · prerequisite — 最小值點：x*∈X 是 f 在 X 上的（全域）最小值點，當且僅當 x* 可行且對每個 x∈X 都有 f(x*)≤f(x)。因此只要找到可行的 x 使 f(x)<f(x*)，x* 就不是最小值點。
- L_interval · lemma — 若 α≤s≤β、α≤t≤β 且 λ∈[0,1]，則 α≤λs+(1−λ)t≤β；因此閉區間 [α,β] 是凸集合。
- L_gap1 · lemma — 對 q(x)=x²+bx+c 與任意實數 x、y、λ：λq(x)+(1−λ)q(y)−q(λx+(1−λ)y)=λ(1−λ)(x−y)²。
- L_halfopen · lemma — 若 0<s≤1、0<t≤1 且 λ∈[0,1]，則 0<λs+(1−λ)t≤1；因此 (0,1] 是凸集合。





## 逐步主鏈

S01 · equivalent操作前

P\ \text{qualifies as convex}

操作後

X\ \text{convex}\ \land\ f\ \text{convex on}\ X

條件：無

規則：mko_cvxopt · 依賴：G1, mko_cvxopt

葉節點依據：mko_cvxopt + def_unfold

依 MKO，凸問題資格由兩個獨立義務組成：可行域 X 是凸集合，目標 f 在 X 上是凸函數。兩者要分別核對（MKO para0）；任何一個失敗，P 就不具資格。



S02 · implies操作前

x,y\in[0,5],\ \lambda\in[0,1]

操作後

\lambda x+(1-\lambda)y\in[0,5];\ X\ \text{convex}

條件：\lambda\in[0,1]

規則：L_interval · 依賴：G1, L_interval, mko_cvxset

葉節點依據：L_interval + forall_intro

用引理 L_interval（α=0、β=5）：任取 x、y∈[0,5] 與 λ∈[0,1]，凸組合仍在 [0,5]。依凸集合定義與 ∀ 引入，X 是凸的。引理在 S02.1、S02.2 中證明。



S03 · equivalent操作前

G_f(x,y,\lambda)=\lambda f(x)+(1-\lambda)f(y)-f(\lambda x+(1-\lambda)y)

操作後

G_f(x,y,\lambda)=\lambda(1-\lambda)(x-y)^2

條件：無

規則：L_gap1 · 依賴：G1, L_gap1

葉節點依據：distributive + power_laws + add_inverse

f 的首項係數是 1，用引理 L_gap1（b=−6、c=10）：f 的 Jensen gap 等於 λ(1−λ)(x−y)²，對所有實數 x、y、λ 成立。引理在 S03.1（一次與常數部分抵消）與 S03.2（二次部分化成完全平方）中證明；N1 核對整個恆等式。



S04 · implies操作前

G_f=\lambda(1-\lambda)(x-y)^2,\ \lambda\in[0,1]

操作後

G_f\ge 0;\ f\ \text{convex on}\ X

條件：\lambda\in[0,1]

規則：mko_cvxf · 依賴：S02, S03, mono_nonneg, square_nonneg, mko_cvxf

葉節點依據：mono_nonneg + square_nonneg + mul_zero + forall_intro

λ≥0、1−λ≥0 給出 λ(1−λ)≥0；(x−y)²≥0；非負數相乘仍非負，所以 G_f≥0，即 f(λx+(1−λ)y)≤λf(x)+(1−λ)f(y)。x、y∈X、λ 任意，X 已在 S02 證為凸，依凸函數定義 f 在 X 上凸。



S05 · implies操作前

X\ \text{convex},\ f\ \text{convex on}\ X

操作後

P\ \text{qualifies as a convex problem}

條件：無

規則：and_intro_elim · 依賴：S01, S02, S04

葉節點依據：and_intro_elim

兩個義務都成立，依 S01，P 具凸問題資格。這只是資格判定：它沒有說哪一點是最優解，也沒有說最優解存在（MKO a2）。



S06 · implies操作前

x_1=1

操作後

0\le 1\le 5,\ x_1\in X

條件：無

規則：set_builder · 依賴：G1, G2, set_builder

葉節點依據：set_builder + order_basics

可行性就是屬於 X=[0,5]={x ∣ 0≤x≤5}。0≤1 且 1≤5，所以 x₁ 可行。



S07 · implies操作前

x_2=4,\ x_3=-1

操作後

0\le 4\le 5\ (x_2\in X);\ -1<0\ (x_3\notin X)

條件：無

規則：set_builder · 依賴：G1, G2, set_builder

葉節點依據：set_builder + order_basics

0≤4≤5，所以 x₂ 可行。−1<0，違反下界，所以 x₃ 不可行；不論 f(−1)=17 是多少，x₃ 都不是 P 的候選，不能參加比較。



S08 · equivalent操作前

f(1)

操作後

f(1)=1-6+10=5

條件：無

規則：numeric_evaluation · 依賴：G1, S06

葉節點依據：numeric_evaluation

單點求值：f(1)=1²−6·1+10=1−6+10=5。



S09 · equivalent操作前

f(4)

操作後

f(4)=16-24+10=2

條件：無

規則：numeric_evaluation · 依賴：G1, S07

葉節點依據：numeric_evaluation

單點求值：f(4)=4²−6·4+10=16−24+10=2。



S10 · implies操作前

f(x_1)=5,\ f(x_2)=2

操作後

f(x_2)<f(x_1)\ \text{(smaller objective value at }x_2\text{)}

條件：無

規則：order_basics · 依賴：S06, S07, S08, S09

葉節點依據：order_basics + numeric_evaluation

兩個可行候選的比較：2<5，所以在 {x₁,x₂} 這兩點之間，x₂ 的目標值較低。這個結論只關於這兩點（MKO para2），不涉及 X 中的其他點。



S11 · implies操作前

3\in X,\ f(3)=9-18+10=1

操作後

f(3)=1<2=f(x_2);\ x_2\ \text{is not a minimizer of}\ P

條件：無

規則：minimizer_def · 依賴：S10, minimizer_def, quantifier_negation

葉節點依據：minimizer_def + quantifier_negation + numeric_evaluation

3 可行（0≤3≤5），單點求值 f(3)=9−18+10=1<2=f(4)。依最小值點的定義，x₂ 是最小值點需要 f(4)≤f(x) 對每個可行 x 成立；x=3 違反這一點，所以 x₂ 不是 P 的最優解。兩候選比較的勝者並不是整個問題的最優解。本稿也不宣稱 3 是最小值點：那需要本切片以外的最優性證書。



S12 · implies操作前

s,t\in(0,1],\ \lambda\in[0,1]

操作後

\lambda s+(1-\lambda)t\in(0,1];\ X'\ \text{convex}

條件：\lambda\in[0,1]

規則：L_halfopen · 依賴：G3, L_halfopen, mko_cvxset

葉節點依據：L_halfopen + forall_intro

轉向 P′。用引理 L_halfopen：(0,1] 中兩點的凸組合仍在 (0,1]，所以 X′ 是凸集合（半開區間也是明示實區間）。引理在 S12.1（嚴格正）與 S12.2（不超過 1）中證明。



S13 · implies操作前

f_0(x)=x^2\ \text{on}\ X'=(0,1]

操作後

G_{f_0}=\lambda(1-\lambda)(x-y)^2\ge 0;\ P'\ \text{qualifies as convex}

條件：\lambda\in[0,1]

規則：mko_cvxopt · 依賴：S12, L_gap1, mono_nonneg, square_nonneg, mko_cvxopt

葉節點依據：L_gap1 + mono_nonneg + square_nonneg + and_intro_elim

f₀ 是 L_gap1 中 b=c=0 的情形，Jensen gap 為 λ(1−λ)(x−y)²≥0（同 S04 的符號論證），所以 f₀ 在凸集合 X′ 上是凸函數。兩個義務都成立，P′ 具凸問題資格。



S14 · implies操作前

x\in(0,1]

操作後

\tfrac{x}{2}\in(0,1],\ f_0(\tfrac{x}{2})=\tfrac{x^2}{4}<x^2=f_0(x)

條件：x>0

規則：minimizer_def · 依賴：G3, S13, minimizer_def

葉節點依據：minimizer_def + square_nonneg + order_basics + frac_rules

任取可行的 x∈(0,1]。x/2>0，且 x/2<x≤1，所以 x/2 也可行。x²−(x/2)²=3x²/4，而 x≠0 給出 x²>0，因此 3x²/4>0，即 f₀(x/2)<f₀(x)。依最小值點的定義，x 不是最小值點。



S15 · implies操作前

\forall x\in X':\ x\ \text{is not a minimizer}

操作後

P'\ \text{is convex but has no minimizer}

條件：無

規則：forall_intro · 依賴：S13, S14, forall_intro, quantifier_negation

葉節點依據：forall_intro + quantifier_negation

S14 中的 x 任意，依 ∀ 引入，X′ 中沒有任何一點是最小值點，即 P′ 沒有最小值點（f₀ 在 X′ 上的下確界 0 取不到，因為 0∉X′）。而 P′ 已具凸問題資格（S13）。所以「凸問題就有（唯一）全域解」是錯的：凸資格不保證解存在。







## 局部子步與引理

S02.1 · implies操作前

\alpha\le s,\ \alpha\le t,\ 0\le\lambda\le 1

操作後

\alpha=\lambda\alpha+(1-\lambda)\alpha\le\lambda s+(1-\lambda)t

條件：\lambda\ge 0; 1-\lambda\ge 0

規則：mono_nonneg · 依賴：mono_nonneg, ineq_add, distributive

葉節點依據：mono_nonneg + ineq_add + distributive

λ≥0 且 1−λ≥0。α≤s 乘以 λ、α≤t 乘以 1−λ，不等號方向不變；相加，左邊依分配律等於 (λ+1−λ)α=α。



S02.2 · implies操作前

s\le\beta,\ t\le\beta

操作後

\lambda s+(1-\lambda)t\le\lambda\beta+(1-\lambda)\beta=\beta

條件：\lambda\ge 0; 1-\lambda\ge 0

規則：mono_nonneg · 依賴：S02.1, mono_nonneg, ineq_add, distributive

葉節點依據：mono_nonneg + ineq_add + distributive

上界對稱：s≤β 乘以 λ、t≤β 乘以 1−λ，相加並化簡為 β。S02.1 與 S02.2 證得 L_interval。



S03.1 · equivalent操作前

\lambda(bx+c)+(1-\lambda)(by+c)-\big(b(\lambda x+(1-\lambda)y)+c\big)

操作後

0

條件：無

規則：distributive · 依賴：distributive

葉節點依據：distributive + add_inverse + mul_one

一次部分 λbx+(1−λ)by−b(λx+(1−λ)y)=0；常數部分 λc+(1−λ)c−c=0。兩者都由分配律得到，對任何 b、c 成立。



S03.2 · equivalent操作前

\lambda x^2+(1-\lambda)y^2-(\lambda x+(1-\lambda)y)^2

操作後

\lambda(1-\lambda)(x-y)^2

條件：無

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

葉節點依據：distributive + power_laws + mul_comm

展開 (λx+(1−λ)y)²=λ²x²+2λ(1−λ)xy+(1−λ)²y²。x² 的係數 λ−λ²=λ(1−λ)，y² 的係數 (1−λ)−(1−λ)²=λ(1−λ)，xy 的係數 −2λ(1−λ)，合起來是 λ(1−λ)(x−y)²。加上 S03.1 的 0，證得 L_gap1。



S12.1 · case_split操作前

0<s,\ 0<t,\ 0\le\lambda\le 1

操作後

\lambda s+(1-\lambda)t>0

條件：無

規則：case_analysis · 依賴：mono_nonneg, order_basics, case_analysis

葉節點依據：case_analysis + order_basics + mono_nonneg

分兩種情況。λ>0：λs>0（兩個正數相乘），而 (1−λ)t≥0（0≤t 乘以 1−λ≥0），正數加非負數仍為正。λ=0：和等於 t>0。λ∈[0,1] 只有這兩種情況，所以 λs+(1−λ)t>0。



S12.2 · implies操作前

s\le 1,\ t\le 1

操作後

\lambda s+(1-\lambda)t\le\lambda+(1-\lambda)=1

條件：\lambda\ge 0; 1-\lambda\ge 0

規則：mono_nonneg · 依賴：S12.1, mono_nonneg, ineq_add, distributive

葉節點依據：mono_nonneg + ineq_add + distributive

s≤1 乘以 λ、t≤1 乘以 1−λ，相加得 λs+(1−λ)t≤λ+(1−λ)=1。S12.1 與 S12.2 證得 L_halfopen。







## 逐步反向審查


- S15 · premise_audit · S13, S14, forall_intro — 需要 S14 對每個可行點成立。括號中關於下確界的說明只是補充，結論不依賴它。
- S14 · premise_audit · minimizer_def, square_nonneg, order_basics — 需要 x>0（使 x/2 在 X′ 中且 x²>0）。這對每個可行 x 都成立，下一步做全稱推廣。
- S13 · premise_audit · S12, L_gap1, mono_nonneg, square_nonneg — 與 S02 至 S05 相同的兩個義務；資格不說最小值點存在。
- S12.2 · premise_audit · mono_nonneg, ineq_add, distributive — 與 L_interval 的上界相同的論證；不使用 L_halfopen 本身。
- S12.1 · premise_audit · mono_nonneg, order_basics, case_analysis — 兩個情況涵蓋 λ≥0 的全部可能；證明 L_halfopen 的下界，不使用 L_halfopen 本身。
- S12 · premise_audit · L_halfopen, mko_cvxset, forall_intro — 需要兩點都在 (0,1] 與 λ∈[0,1]；不宣稱反向。
- S11 · premise_audit · minimizer_def, quantifier_negation, numeric_evaluation — 否證只需一個可行且更低的點；正面宣稱任何點最優則需要對所有可行點的論證，本稿不提供。
- S10 · premise_audit · S06, S07, S08, S09, order_basics — 需要兩點都可行與兩個精確值。不宣稱 x₂ 是 P 的最優解；S11 顯示它不是。
- S09 · inverse_equivalence · numeric_evaluation — 精確整數計算，兩邊是同一個數。
- S08 · inverse_equivalence · numeric_evaluation — 精確整數計算，兩邊是同一個數。
- S07 · premise_audit · set_builder, order_basics — 兩個單點判定；x₃ 只要違反一個邊界條件就不可行。
- S06 · premise_audit · set_builder, order_basics — 單點可行性只說 x₁∈X，不說它的目標值高低。
- S05 · premise_audit · S01, S02, S04, and_intro_elim — 只合取兩個已證義務。
- S04 · premise_audit · S02, S03, mono_nonneg, square_nonneg, forall_intro — 需要 λ∈[0,1] 與首項係數 1>0。這是第二個義務；不宣稱 f 有最小值點。
- S03.2 · inverse_equivalence · distributive, power_laws — 展開右邊即回到左邊；不使用 L_gap1 本身。
- S03.1 · inverse_equivalence · distributive, add_inverse — 多項式恆等式，雙向成立。
- S03 · inverse_equivalence · L_gap1 — 多項式恆等式，兩邊相同，雙向成立。
- S02.2 · premise_audit · mono_nonneg, ineq_add, distributive — 與 S02.1 對稱；不使用 L_interval 本身。
- S02.1 · premise_audit · mono_nonneg, ineq_add, distributive — 證明 L_interval 的下界，沒有使用 L_interval 本身。
- S02 · premise_audit · L_interval, mko_cvxset, forall_intro — 需要 x、y 在區間內與 λ∈[0,1]；這只是義務之一，不涉及 f。
- S01 · inverse_equivalence · mko_cvxopt, def_unfold — 展開與收回定義互逆，雙向成立。





## 錯誤控制與反例

凸資格不保證有解，更不保證唯一MKO 指出的誤解是看到「凸」字樣就宣稱有唯一全域解。P′ 是凸問題，但對每個可行 x，x/2 都更低，所以沒有最小值點（S14、S15）。存在性與唯一性需要另外的條件與證書。

兩候選中目標值較低者不一定是最優解MKO 的另一個誤解是把兩個候選中較低者叫做整個問題的最優解。f(4)=2<5=f(1) 只說 4 比 1 好（S10）；可行點 3 的值 f(3)=1 更低（S11）。兩點比較只說兩點之間的高低（MKO para2）。

兩個義務分別核對，可行性先於比較目標凸不代表問題凸：若可行域換成 [0,1]∪[4,5]，1、4 可行但 (1/2)·1+(1/2)·4=5/2 不可行，可行域不凸，問題不具資格。同樣，不可行的 x₃=−1 即使算得 f(−1)=17，也不能參加候選比較（S07）。


- P 是凸問題，且 f(4)<f(1)，所以 x₂=4 是 P 的最優解 → reject — 3 可行且 f(3)=1<2=f(4)。
- 每個凸最佳化問題都有唯一的全域最優解 → reject — P′：在 (0,1] 上最小化 x² 是凸問題，但沒有最小值點。
- f 是凸函數，所以在 [0,1]∪[4,5] 上最小化 f 也具本條目的凸問題資格 → reject — 可行域不凸：1、4 可行，但 5/2 不可行。
- x₁=1 可行且 f(1)=5，所以 P 的最優值是 5 → reject — 單點求值不是最優性；f(4)=2<5。





## 結論與限制

P（在 [0,5] 上最小化 x²−6x+10）具凸問題資格：[0,5] 是凸集合，f 的 Jensen gap 為 λ(1−λ)(x−y)²≥0。x₁=1、x₂=4 可行，x₃=−1 不可行；f(1)=5、f(4)=2，所以兩候選中 x₂ 較低。但 f(3)=1<2，所以 x₂ 不是 P 的最優解。P′（在 (0,1] 上最小化 x²）也具凸問題資格，卻沒有最小值點。


- 本稿不對 P 的任何點給出全域最優證書（包括 x=3）；最優性證書、KKT 與對偶屬於 MKO 的 formal next。
- mono_nonneg、ineq_add 與 minimizer_def 是本稿的前提，不在本稿中推出。





## 驗證及來源綁定

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


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: 41acd93a76eeb1cda8a7b0d56acf2deac4623d5ac9b30b940dad539544bc41e2
- original source SHA-256: 41acd93a76eeb1cda8a7b0d56acf2deac4623d5ac9b30b940dad539544bc41e2
- Lean: NOT_RUN · independent AI: NOT_MEASURED

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