凸函數：二次函數 Jensen gap 的完整證書與單一 Jensen 反例

目標與範圍

（一）證明 f(x)=2x²−3x+1 在區間 I=[−1,4] 上是凸函數：先確認 I 是凸集合，再對所有 x,y∈I 與所有 λ∈[0,1] 證明 f(λx+(1−λ)y)≤λf(x)+(1−λ)f(y)，方法是證明二次函數的 Jensen gap 等於 aλ(1−λ)(x−y)²。（二）由同一恆等式得仿射函數 ℓ(x)=3x−5 在 I 上取等號。（三）用一個精確的 Jensen 違反否證 g(x)=−x²+x 在 J=[0,2] 上的凸性，並說明幾個通過的樣本為何不能證明凸性。

停在 MKO 的切片內：明示的非空實區間作定義域，一元仿射與二次函數，精確係數。正面結論用覆蓋全部 x、y、λ 的代數證書；反面結論用單一精確違反。不處理嚴格凸、次梯度、二階導數判別或高維凸函數；不改動 canonical MKO 或英文 edition。

已知條件與符號

• order_basics
• square_nonneg
• distributive
• power_laws
• forall_intro
• quantifier_negation

• G1 — I=[−1,4]；f:I→ℝ，f(x)=2x²−3x+1（a=2、b=−3、c=1）。
• G2 — ℓ:I→ℝ，ℓ(x)=3x−5（a=0、b=3、c=−5，仿射）。
• G3 — J=[0,2]；g:J→ℝ，g(x)=−x²+x（a=−1、b=1、c=0）。

• I=[-1,4],\ J=[0,2] — 明示的定義域區間
• \lambda\in[0,1] — Jensen 組合的權重
• z=\lambda x+(1-\lambda)y — x 與 y 的凸組合
• G_q(x,y,\lambda) — 函數 q 的 Jensen gap：λq(x)+(1−λ)q(y)−q(z)
• a,\ b,\ c — 二次函數 ax²+bx+c 的係數

規則與來源

• 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。
• power_laws · prerequisite — 整數指數律（底數非零或指數為正整數）：a^m·a^n=a^{m+n}，(a^m)^n=a^{mn}，(ab)^n=a^n b^n，a^0=1。
• forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
• quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。
• def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
• def_intro · prerequisite — 引入定義：可為一個命題、式子或物件取名；之後名稱與被定義者可互相替換。
• add_inverse · prerequisite — 加法反元素：每個 u 都有 −u，使 u+(−u)=0；u−v 定義為 u+(−v)。
• mul_one · prerequisite — 乘法單位元：1·u=u。
• mul_comm · prerequisite — 乘法交換律：uv=vu（在交換的數系中，例如 ℤ、ℚ、ℝ、ℂ）。
• add_comm · prerequisite — 加法交換律：u+v=v+u。
• forall_elim · prerequisite — ∀消去（代入特例）：若 ∀x∈D, P(x) 成立且 a∈D，則 P(a) 成立。
• eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
• 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。
• numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
• exists_intro · prerequisite — ∃引入：若找到 a∈D 使 P(a) 成立，則 ∃x∈D, P(x)。
• mko_cvxf · cited — 在凸定義域 C 上，f 為凸若對所有 x,y∈C 及 λ∈[0,1]，f(λx+(1−λ)y)≤λf(x)+(1−λ)f(y)。單一 Jensen 違反足以否證；單一通過實例不能證凸，正證書需覆蓋全部 x、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₂。
• L_interval · lemma — 若 α≤s≤β、α≤t≤β 且 λ∈[0,1]，則 α≤λs+(1−λ)t≤β；因此每個閉區間 [α,β] 都是凸集合。
• L_gap · lemma — 對 q(x)=ax²+bx+c 與任意實數 x、y、λ：λq(x)+(1−λ)q(y)−q(λx+(1−λ)y)=aλ(1−λ)(x−y)²。

逐步主鏈

f\ \text{convex on}\ I

I\ \text{convex}\ \land\ \forall x,y\in I\ \forall\lambda\in[0,1]:\ f(\lambda x+(1-\lambda)y)\le\lambda f(x)+(1-\lambda)f(y)

x,y\in[-1,4],\ \lambda\in[0,1]

z=\lambda x+(1-\lambda)y\in[-1,4];\ I\ \text{convex}

f(z)\le\lambda f(x)+(1-\lambda)f(y)

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

G_q(x,y,\lambda)\ \text{for } q(x)=ax^2+bx+c

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

G_f(x,y,\lambda)

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

0\le\lambda\le 1

\lambda(1-\lambda)\ge 0

2>0,\ \lambda(1-\lambda)\ge 0,\ (x-y)^2\ge 0

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

G_f(x,y,\lambda)\ge 0\ \text{for arbitrary } x,y\in I,\ \lambda\in[0,1]

f\ \text{convex on}\ I

x=-1,\ y=4,\ \lambda=\tfrac15

z=3,\ f(3)=10\le 18=\tfrac15 f(-1)+\tfrac45 f(4),\ G_f=8=2\cdot\tfrac15\cdot\tfrac45\cdot 25

G_\ell(x,y,\lambda)\ \text{for}\ \ell(x)=3x-5

G_\ell=0\cdot\lambda(1-\lambda)(x-y)^2=0;\ \ell\ \text{convex on}\ I\ \text{with equality}

\neg(g\ \text{convex on}\ J)

\exists x,y\in J\ \exists\lambda\in[0,1]:\ g(\lambda x+(1-\lambda)y)>\lambda g(x)+(1-\lambda)g(y)

x=0,\ y=2,\ \lambda=\tfrac12

z=1\in J,\ g(1)=0,\ \tfrac12 g(0)+\tfrac12 g(2)=\tfrac12\cdot 0+\tfrac12\cdot(-2)=-1

g(1)=0,\ \tfrac12 g(0)+\tfrac12 g(2)=-1

0>-1;\ g\ \text{is not convex on}\ J

G_g(x,y,\lambda)

G_g=-\lambda(1-\lambda)(x-y)^2;\ G_g(0,2,\tfrac12)=-1

\lambda\in\{0,1\}\ \text{or}\ x=y

G_g=0\ \text{(samples pass)},\ \text{yet } g\ \text{not convex}

局部子步與引理

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

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

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

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

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

0

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

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

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

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

逐步反向審查

• S15 · premise_audit · S13, S14, mul_zero — 只用乘以零與 S13 的反例；結論是「通過的樣本不足以證凸」，由 g 這個具體反例支持。
• S14 · premise_audit · S04, S12, forall_elim — 這是與 S13 獨立的核對；S13 的結論不依賴本步。「x≠y 且 0<λ<1 時 G_g<0」用到 λ(1−λ)>0 與 (x−y)²>0，兩者在這些條件下成立。
• S13 · premise_audit · S11, S12, exists_intro — 需要見證在範圍內且不等式嚴格反向，兩者都已核對。
• S12 · premise_audit · G3, numeric_evaluation — 精確計算；x、y 確實在 J 中，λ 確實在 [0,1] 中。
• S11 · inverse_equivalence · quantifier_negation, order_basics, L_interval — 量詞否定與序的三分律都是雙向的；J 凸是此等價的前提。
• S10 · premise_audit · S04, S02, forall_elim, forall_intro — 需要 L_gap 與定義域凸。等號成立並不表示仿射以外的函數也取等號。
• S09 · premise_audit · S05, numeric_evaluation — 精確的有理數計算；只說明這一組 x、y、λ，不推出任何全稱結論。
• S08 · premise_audit · S01, S02, S03, S07, forall_intro — 需要兩部分（定義域凸與 Jensen）都已證，以及 x、y、λ 的任意性。
• S07 · premise_audit · S05, S06, square_nonneg, mono_nonneg — 關鍵是 a=2≥0；若 a<0，同一論證給出 gap≤0（見 S14）。不宣稱反向。
• S06 · premise_audit · mono_nonneg, mul_zero — 需要 λ∈[0,1]；λ>1 或 λ<0 時 λ(1−λ)<0，這正是定義限制 λ 範圍的原因。
• S05 · inverse_equivalence · S04, forall_elim — 代入後仍是恆等式，兩邊相等，雙向成立。
• S04.3 · inverse_equivalence · distributive, power_laws, S04.2 — 展開 aλ(1−λ)(x−y)² 即回到左邊；不使用 L_gap 本身。
• S04.2 · inverse_equivalence · distributive, power_laws — 展開與因式分解互逆，雙向成立。
• S04.1 · inverse_equivalence · distributive, add_inverse — 多項式恆等式，雙向成立。
• S04 · inverse_equivalence · L_gap — 這是多項式恆等式，兩邊是同一個多項式，雙向成立，沒有附加條件。
• S03 · inverse_equivalence · order_basics, def_intro — 同減 f(z) 與同加 f(z) 互逆，兩者都保持不等號方向，雙向成立。
• 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 — 需要 x、y 在區間內與 λ∈[0,1]；不宣稱反向。
• S01 · inverse_equivalence · mko_cvxf, def_unfold — 展開與收回定義互逆，雙向成立。

錯誤控制與反例

幾個 Jensen 樣本通過不證凸

MKO 指出的誤解是由幾個 Jensen 樣本通過就宣稱全域凸。g 在 λ=0、λ=1 與 x=y 的所有樣本上都通過（S15），卻不是凸函數。S09 對 f 的實例同樣只是例示；f 的凸性來自 S04 至 S08 對全部 x、y、λ 的恆等式與符號論證。

定義域必須凸

MKO 的另一個誤解是在非凸定義域上談一般凸函數。若定義域是 D=[0,1]∪[2,3]，x=1、y=2、λ=1/2 給出 3/2∉D，函數在 3/2 沒有值，Jensen 不等式根本無法陳述。所以 S02 先證 I 是凸的，S11 也先確認 J 是凸的。

a 的正負決定 gap 的正負

依 L_gap，二次函數的 Jensen gap 是 aλ(1−λ)(x−y)²。a=2 時 gap≥0（凸），a=0 時 gap=0（仿射，取等號），a=−1 時 gap≤0，而且 x≠y、0<λ<1 時嚴格小於 0（不凸）。「二次函數都是凸的」是錯的。

• g 在 λ=0、λ=1 與 x=y 的樣本上都滿足 Jensen，所以 g 在 [0,2] 上凸 → reject — x=0、y=2、λ=1/2：g(1)=0>−1。
• f 在 x=−1、y=4、λ=1/5 的 Jensen 實例通過，這就證明 f 在 I 上凸 → reject — 單一通過實例不能證凸（MKO a2）；結論成立是因為 S04 至 S08 覆蓋全部 x、y、λ。
• x² 在 D=[0,1]∪[2,3] 上是 MKO 意義下的凸函數 → reject — D 不是凸集合：1、2∈D 但 (1/2)·1+(1/2)·2=3/2∉D；定義要求凸定義域。
• 每個二次函數都是凸函數 → reject — g(x)=−x²+x 的 a=−1，在 x=0、y=2、λ=1/2 違反 Jensen。

結論與限制

I=[−1,4] 是凸集合，且對所有 x,y∈I、λ∈[0,1]，f(x)=2x²−3x+1 的 Jensen gap 等於 2λ(1−λ)(x−y)²≥0，所以 f 在 I 上是凸函數。ℓ(x)=3x−5 的 gap 恆為 0，Jensen 取等號。g(x)=−x²+x 在 J=[0,2] 上不凸：x=0、y=2、λ=1/2 時 g(1)=0>−1=(1/2)g(0)+(1/2)g(2)。

• mono_nonneg 與 ineq_add 是本稿的前提，不在本稿中由實數公理推出（mono_nonneg 在凸集合教學稿中以引理證明）。
• N7 至 N10 只核 S09 的一個實例；它們是例示，證明不依賴它們。

驗證及來源綁定

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

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: 3f396010579d87300f52e4a41245fcd8d02d372b3712f863225c958c4632db0c
• original source SHA-256: 3f396010579d87300f52e4a41245fcd8d02d372b3712f863225c958c4632db0c
• Lean: NOT_RUN · independent AI: NOT_MEASURED

同源完整 JSON（含公式、AST、反控制與修訂記錄）