有界線性算子：矩陣在 ℓ^∞ 與 ℓ¹ 下的精確誘導算子範數

目標與範圍

設 A 為第一行 (1,−2)、第二行 (3,4) 的整數矩陣，T(x)=Ax:ℝ²→ℝ²。（一）在兩端都用 ℓ^∞ 範數時，證明對所有 x 有 ‖Ax‖_∞≤7‖x‖_∞，且沒有更小的常數可用，所以 ‖T‖_{∞→∞}=7（最大行絕對值和）。（二）兩端都用 ℓ¹ 範數時，證明 ‖T‖_{1→1}=6（最大列絕對值和）。（三）說明非最佳常數、有限輸入與值域無界這三個陷阱。

在 MKO 的範圍內工作：來源與目標都是明示的 ℝ²，兩端範數名稱固定（假設 a1）；ℓ¹ 用最大列絕對值和、ℓ^∞ 用最大行絕對值和，並對這個矩陣完整證明上界與達成（假設 a2）。一般 m×n 矩陣的公式只由 MKO 敘述，不另證。不處理連續性、對偶或譜理論，不改動 canonical MKO 或英文 edition。

已知條件與符號

• abs_rules
• order_basics
• matrix_product_def
• forall_intro
• numeric_evaluation

• G1 — ℝ² 上的兩個命名範數：‖x‖_∞=max(|x₁|,|x₂|)，‖x‖₁=|x₁|+|x₂|；每個任務在來源與目標兩端使用同一個指定名稱。
• G2 — A 的列為 (1,−2) 與 (3,4)；T(x)=Ax。
• G3 — 測試向量：x*=(1,1)、e₁=(1,0)、e₂=(0,1)。

• A=\begin{pmatrix}1&-2\\3&4\end{pmatrix} — 給定的整數矩陣
• \|x\|_\infty=\max(|x_1|,|x_2|) — ℓ^∞ 範數
• \|x\|_1=|x_1|+|x_2| — ℓ¹ 範數
• \|T\|_{\infty\to\infty},\ \|T\|_{1\to1} — 兩種誘導算子範數
• C — 可用的界常數
• x^{*}=(1,1) — 達成 ℓ^∞ 上界的向量

規則與來源

• 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。
• matrix_product_def · prerequisite — 矩陣乘法：若 A 為 m×n、B 為 n×p，則 (AB)_{ij}=Σ_{k=1}^{n} A_{ik}B_{kj}。矩陣乘法一般不可交換。
• forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
• numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
• def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
• distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。
• add_comm · prerequisite — 加法交換律：u+v=v+u。
• quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。
• archimedean · prerequisite — 阿基米德性質：對任意實數 x，存在自然數 n>x；因此對任意 ε>0，存在 n 使 1/n<ε。
• and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
• mko_bounded_def · cited — 獨立來源追加式勘誤（使用者已採用於本地修訂；未合併或發布）：先要求 T:V→W 是線性映射，再要求存在 C≥0 使所有 x 有 ‖Tx‖_W≤C‖x‖_V，兩項共同構成有界線性算子資格。單有此增長界不推出線性，例如 x↦|x|。本輪整矩陣在 ℓ¹ 下採最大列絕對值和，在 ℓ^∞ 下採最大行絕對值和作精確誘導範數證書；instance 通過不代替全稱證書。原始引文與 canonical MKO 保留。 · mko-bounded-linear-operator
• mko_linear_map_def · cited — 實線性映射滿足 T(αu+βv)=αT(u)+βT(v)；有限維矩陣公式提供全稱座標證書。 · mko-general-linear-map
• op_norm_def · prerequisite — 有界算子的誘導算子範數 ‖T‖ 是所有可用常數 C（對所有 x 有 ‖Tx‖≤C‖x‖）的下確界；若某個可用常數 C₀ 使每個可用常數都 ≥C₀，則 ‖T‖=C₀。
• max_rules · prerequisite — max(s,t)≥s 且 max(s,t)≥t；max(s,t)≤K 當且僅當 s≤K 且 t≤K。
• L_row_bound · lemma — 對實數 c₁,c₂ 與 x∈ℝ²：|c₁x₁+c₂x₂|≤(|c₁|+|c₂|)‖x‖_∞。

逐步主鏈

T:(\mathbb{R}^2,\|\cdot\|_\infty)\to(\mathbb{R}^2,\|\cdot\|_\infty)\ \text{bounded}

\exists C\ge0\ \forall x:\ \|Tx\|_\infty\le C\|x\|_\infty;\ \ \|T\|_{\infty\to\infty}=\text{least admissible}\ C

T(x)=Ax

Ax=(x_1-2x_2,\ 3x_1+4x_2),\ \ T\ \text{linear}

\|Ax\|_\infty

\max(|x_1-2x_2|,\ |3x_1+4x_2|)

|x_1-2x_2|

|x_1-2x_2|\le(|1|+|-2|)\|x\|_\infty=3\|x\|_\infty

|3x_1+4x_2|

|3x_1+4x_2|\le(|3|+|4|)\|x\|_\infty=7\|x\|_\infty

\max(|x_1-2x_2|,|3x_1+4x_2|)

\le\max(3,7)\|x\|_\infty=7\|x\|_\infty\ \ \forall x\ \Rightarrow\ T\ \text{bounded with}\ C=7

x^{*}=(1,1),\ \|x^{*}\|_\infty=1

Ax^{*}=(-1,7),\ \|Ax^{*}\|_\infty=7=7\|x^{*}\|_\infty

C\ \text{admissible}\ \Rightarrow\ 7=\|Ax^{*}\|_\infty\le C\|x^{*}\|_\infty=C

C\ge7\ \text{for every admissible}\ C;\ \ \|T\|_{\infty\to\infty}=7

\|Ax\|_1=|x_1-2x_2|+|3x_1+4x_2|

\|Ax\|_1\le 6\|x\|_1\ \ \forall x

e_2=(0,1),\ \|e_2\|_1=1

Ae_2=(-2,4),\ \|Ae_2\|_1=6\ \Rightarrow\ \|T\|_{1\to1}=6

\|T\|_{\infty\to\infty}=7,\ \|T\|_{1\to1}=6

C=7\ \text{admissible for}\ \ell^1\ \text{but}\ \neq\|T\|_{1\to1};\ C=10\ \text{admissible for}\ \ell^\infty\ \text{but}\ \neq\|T\|_{\infty\to\infty}

C=5:\ \|Ae_1\|_\infty=\|(1,3)\|_\infty=3\le5,\ \|Ae_2\|_\infty=\|(-2,4)\|_\infty=4\le5

\|Ax^{*}\|_\infty=7>5=5\|x^{*}\|_\infty\ \Rightarrow\ C=5\ \text{not admissible}

T(tx^{*})=tAx^{*}=(-t,7t),\ t\in\mathbb{R}

\|T(tx^{*})\|_\infty=7|t|\ \text{unbounded in}\ t,\ \text{yet}\ T\ \text{is bounded}

\text{S08},\ \text{S10},\ \text{S11},\ \text{S12},\ \text{S13}

\|T\|_{\infty\to\infty}=7,\ \|T\|_{1\to1}=6;\ \text{traps refuted}

局部子步與引理

|c_1x_1+c_2x_2|

|c_1x_1+c_2x_2|\le|c_1||x_1|+|c_2||x_2|

|c_1||x_1|+|c_2||x_2|

\le|c_1|\|x\|_\infty+|c_2|\|x\|_\infty=(|c_1|+|c_2|)\|x\|_\infty

|x_1-2x_2|+|3x_1+4x_2|

\le(|x_1|+2|x_2|)+(3|x_1|+4|x_2|)=4|x_1|+6|x_2|

4|x_1|+6|x_2|

\le6|x_1|+6|x_2|=6\|x\|_1

逐步反向審查

• S14 · sufficient_goal_reduction · S08, S10, S11, S12, S13, and_intro_elim — 目標是三個任務的合取；各部分由所行步驟正向證得。
• S13 · premise_audit · archimedean, mko_linear_map_def — 需要 T 線性與 Ax*≠0；只有零算子的值域有界。
• S12 · premise_audit · quantifier_negation, numeric_evaluation — 一個反例 x* 足以否定 C=5（N7）。
• S11 · premise_audit · S06, S08, S09, S10, order_basics — 可用常數的集合向上封閉（大於可用常數者仍可用），算子範數是其最小者（N8）。
• S10 · sufficient_goal_reduction · S09, op_norm_def, numeric_evaluation — 目標：‖T‖_{1→1}=6。足夠條件：6 可用（S09）且 e₂ 迫使 C≥6（N4）。
• S09.2 · premise_audit · order_basics, distributive — 需要 |x₁|≥0；不宣稱等號。
• S09.1 · premise_audit · abs_rules, add_comm, distributive — 單向不等式加上重組；ℓ¹ 自然地按列合併，ℓ^∞ 則按行取最大。
• S09 · premise_audit · abs_rules, order_basics, forall_intro — 全稱上界；N5 是有限格點輔助核對。
• S08 · sufficient_goal_reduction · S06, S07, op_norm_def — 目標：‖T‖=7。足夠條件：7 可用（S06）且每個可用 C≥7（S07）；兩者都已正向證得。
• S07 · premise_audit · S02, numeric_evaluation — 精確計算（N1）；這一個點只用來證明下界，不用來證明上界。
• S06 · premise_audit · S04, S05, max_rules, forall_intro — 證明沒有代入特定 x；N3 在整數格上作有限核對，只是輔助（N2 核行和）。
• S05 · premise_audit · L_row_bound — 上界，不宣稱等號。
• S04.2 · premise_audit · max_rules, order_basics, distributive — 需要 |c_k|≥0；若乘以負數，不等號會翻轉。
• S04.1 · premise_audit · abs_rules — 單向不等式，不宣稱等號。
• S04 · premise_audit · L_row_bound — 這是上界，不宣稱等號；等號何時達成由 S07 另行處理。
• S03 · inverse_equivalence · def_unfold — 定義展開，兩向成立。
• S02 · inverse_equivalence · matrix_product_def — 坐標公式是乘積的展開，兩邊同一向量；線性性質是引用，不在本步重證。
• S01 · premise_audit · mko_bounded_def, op_norm_def — 只展開定義；若把量詞順序寫成「對每個 x 有某個 C」，條件就會對每個線性映射平凡成立，失去意義。

錯誤控制與反例

有限輸入不證有界

MKO 指出的誤解之一是只看有限輸入。C=5 對 e₁、e₂ 都成立，但 x*=(1,1) 給 7>5。同一個 C 必須控制所有輸入，所以上界要用 S04 到 S06 的全稱估計證明。

可用上界不一定是算子範數

C=10 證明 T 有界，但算子範數是最小的可用常數 7，需要 S07 的達成向量才能確定。同樣在 ℓ¹ 下 7 可用，但算子範數是 6。

有界不是值域有界

非零線性算子的值域永遠無界（S13）。有界算子的意思是 ‖Tx‖ 被 C‖x‖ 控制，等價於 x≠0 時的比值有共同上界；x=0 的不等式由 T0=0 處理，不取 0/0；把「值域看似有界」當定義是 MKO 指出的誤解。

• ‖Ae₁‖_∞=3≤5 且 ‖Ae₂‖_∞=4≤5，所以對所有 x 有 ‖Ax‖_∞≤5‖x‖_∞ → reject — x*=(1,1)：‖Ax*‖_∞=7>5。
• 因為 ‖Ax‖_∞≤10‖x‖_∞ 對所有 x 成立，所以 ‖T‖_{∞→∞}=10 → reject — 10 只是可用常數；最小可用常數是 7。
• ℓ^∞ 誘導算子範數是最大列絕對值和 max(4,6)=6 → reject — 列和屬於 ℓ¹；ℓ^∞ 用行和，得 7，x* 給出 7>6。
• T(tx*)=(−t,7t) 的範數可任意大，所以 T 不是有界算子 → reject — 有界指 ‖Tx‖≤7‖x‖ 對所有 x 成立，與值域是否有界無關。

結論與限制

對 A（行 (1,−2),(3,4)）：所有 x 都有 ‖Ax‖_∞≤7‖x‖_∞，且 x*=(1,1) 給 ‖Ax*‖_∞=7，所以 ‖T‖_{∞→∞}=7（最大行絕對值和）；所有 x 都有 ‖Ax‖₁≤6‖x‖₁，且 e₂ 給 ‖Ae₂‖₁=6，所以 ‖T‖_{1→1}=6（最大列絕對值和）。C=10 或對 ℓ¹ 的 C=7 只證有界、不是算子範數；C=5 通過 e₁、e₂ 卻在 x* 失敗；T 的值域無界，但 T 是有界算子。

• 一般 m×n 矩陣的最大行和／最大列和公式由 MKO 敘述；本稿只對這個 2×2 矩陣完整證明上界與達成。
• N3、N5 是整數格點上的有限核對，只是輔助；全稱上界由 S04 到 S06 與 S09 證明。

驗證及來源綁定

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

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: 62f768caa7fd6bfdba8a4015f71bafa6a99724583bfdb2b12927754626981870
• original source SHA-256: 63dd897c1a76886df54bea7e1ee19386d14e12f7b203715b1bb3773f979351a1
• Lean: NOT_RUN · independent AI: NOT_MEASURED

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