# 實賦範向量空間：ℓ¹ 與 ℓ^∞ 公式的全稱範數證書，以及兩個非範數公式 [← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-real-normed-vector-space/) 這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。 derivation-mko-real-normed-vector-space-01 · production-20261019-adopted-96 ## 目標與範圍在 ℝⁿ（n≥1 固定）上，對所有向量 u、v 與所有實數 a，證明 ‖v‖₁=Σ|v_i| 與 ‖v‖_∞=max|v_i| 都滿足範數的三條公理：非負且 ‖v‖=0 ⇔ v=0、‖av‖=|a|‖v‖、‖u+v‖≤‖u‖+‖v‖。再在 ℝ³ 中對整數座標向量 u=(3,−4,1)、v=(−1,2,5) 計算兩種範數與三角不等式、齊次性的實例；最後說明 φ(v)=|v₁| 與 ψ(v)=(‖v‖₁)² 不是範數。停在 MKO 的切片內：只用 ℝⁿ 上命名的 ℓ¹ 與 ℓ^∞ 公式，資格來自對所有向量與純量成立的代數證書；具體例子用整數座標向量。不處理誘導度量、完備性（Banach 空間）、範數等價或有界算子；不改動 canonical MKO 或英文 edition。 ## 已知條件與符號 - abs_rules - finite_sum_rules - order_basics - vector_space_axioms - forall_intro - quantifier_negation - G1 — n≥1 固定；ℝⁿ 是實向量空間，加法與純量乘法逐座標進行；v=0 當且僅當每個 v_i=0。 - G2 — 命名公式：‖v‖₁=Σ_{i=1}^{n}|v_i|，‖v‖_∞=max_{1≤i≤n}|v_i|。 - G3 — 範數公理（MKO）：(N1) ‖v‖≥0，且 ‖v‖=0 ⇔ v=0；(N2) ‖av‖=|a|‖v‖；(N3) ‖u+v‖≤‖u‖+‖v‖；三條都要對所有 u,v∈ℝⁿ、a∈ℝ 成立。 - G4 — ℝ³ 中的具體資料：u=(3,−4,1)、v=(−1,2,5)；候選公式 φ(v)=|v₁| 與 ψ(v)=(‖v‖₁)²。 - v=(v_i)_{i=1}^{n} — ℝⁿ 中的向量及其座標 - \|v\|_1=\sum_{i=1}^{n}|v_i| — ℓ¹ 範數：座標絕對值總和 - \|v\|_\infty=\max_{1\le i\le n}|v_i| — ℓ^∞ 範數：座標絕對值最大值 - (N1),(N2),(N3) — 範數三公理：正定、齊次、三角不等式 - e_1,\ e_2 — ℝ³ 的標準基向量 (1,0,0)、(0,1,0) - \varphi,\ \psi — 兩個待審的候選公式 ## 規則與來源 - abs_rules · prerequisite — 絕對值（實數）：|u|=u（u≥0）、|u|=−u（u<0）；|u|≥0；|uv|=|u||v|；三角不等式 |u+v|≤|u|+|v|；|u|v 之一；u0 推出 uwvw。 - vector_space_axioms · prerequisite — 向量空間公理（實數或其他域 F 上）：加法成交換群；純量乘法滿足 a(u+v)=au+av、(a+b)u=au+bu、(ab)u=a(bu)、1u=u。 - forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。 - quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。 - def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。 - case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。 - and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。 - numeric_evaluation · 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。 - mko_norm · cited — 範數把向量送到非負實數，且 norm(v)=0 當且僅當 v=0、norm(av)=|a| norm(v)、norm(u+v) 不超過 norm(u)+norm(v)。本輪只使用 ℝⁿ 上的 l1 與 linfinity 命名公式；資格來自公式的全稱代數證書，有限抽樣不冒充一般範數證明。 · mko-real-normed-vector-space - coord_ops · prerequisite — 逐座標運算：(u+v)_i=u_i+v_i，(av)_i=a v_i；v=0 ⇔ 每個 v_i=0。 - sum_order · prerequisite — 有限和與序：若對每個 i 都有 s_i≤t_i，則 Σs_i≤Σt_i；若每個 s_i≥0，則 Σs_i≥0，且對每個 j 有 Σs_i≥s_j。 - max_finite · prerequisite — 有限個實數的最大值：對 t_i（1≤i≤n，n≥1），M=max_i t_i 存在且等於某個 t_k；對每個 i 有 t_i≤M；若對每個 i 有 t_i≤K，則 M≤K。 - mono_nonneg · prerequisite — 乘以非負數保持不等號：若 u≤v 且 w≥0，則 wu≤wv。 - ineq_add · prerequisite — 不等式相加：若 u₁≤v₁ 且 u₂≤v₂，則 u₁+u₂≤v₁+v₂。 - L_abs_zero · lemma — 對實數 t：|t|=0 ⇔ t=0。 ## 逐步主鏈 S01 · definition操作前 \|\cdot\|_1,\ \|\cdot\|_\infty\ \text{are norms on}\ \mathbb{R}^n 操作後 (N1)\land(N2)\land(N3)\ \text{for all } u,v\in\mathbb{R}^n,\ a\in\mathbb{R},\ \text{for each formula} 條件：無規則：mko_norm · 依賴：G2, G3, mko_norm 葉節點依據：mko_norm + def_unfold 依 MKO，公式是範數，當且僅當三條公理對所有向量與所有純量成立。所以要給的是全稱證書：每一步對任意 u、v、a 論證，而不是代入幾個向量。 S02 · implies操作前 |v_i|\ge 0\ \text{for every } i 操作後 \|v\|_1=\sum_{i=1}^{n}|v_i|\ge 0 條件：無規則：sum_order · 依賴：G2, abs_rules, sum_order 葉節點依據：abs_rules + sum_order 絕對值非負：每個 |v_i|≥0。非負數的有限和非負，所以 ‖v‖₁≥0（N1 的前半）。 S03 · equivalent操作前 \|v\|_1=0 操作後 v=0 條件：無規則：sum_order · 依賴：S02, G1, sum_order, L_abs_zero 葉節點依據：sum_order + L_abs_zero + coord_ops 正向：若 ‖v‖₁=0，對每個 j，0≤|v_j|≤Σ|v_i|=0（非負項的和不小於任一項），所以 |v_j|=0；依引理 L_abs_zero（S03.1），v_j=0；每個座標為 0，即 v=0。反向：v=0 時每個 |v_i|=|0|=0，和為 0。這是 N1 的後半。 S04 · equivalent操作前 \|av\|_1=\sum_{i=1}^{n}|a v_i| 操作後 \|av\|_1=\sum_{i=1}^{n}|a||v_i|=|a|\,\|v\|_1 條件：無規則：finite_sum_rules · 依賴：G1, G2, abs_rules, finite_sum_rules 葉節點依據：coord_ops + abs_rules + finite_sum_rules (av)_i=a v_i，且 |a v_i|=|a||v_i|；常數 |a| 可從有限和中提出：Σ|a||v_i|=|a|Σ|v_i|。對任意 a、v 成立，這是 N2。 S05 · implies操作前 \|u+v\|_1=\sum_{i=1}^{n}|u_i+v_i| 操作後 \|u+v\|_1\le\sum_{i=1}^{n}(|u_i|+|v_i|)=\|u\|_1+\|v\|_1 條件：無規則：sum_order · 依賴：G1, G2, abs_rules, sum_order, finite_sum_rules 葉節點依據：abs_rules + sum_order + finite_sum_rules + coord_ops 每個座標用實數的三角不等式 |u_i+v_i|≤|u_i|+|v_i|；逐項不等式相加得和的不等式；再把 Σ(|u_i|+|v_i|) 拆成 Σ|u_i|+Σ|v_i|。對任意 u、v 成立，這是 N3。 S06 · implies操作前 (N1),(N2),(N3)\ \text{for}\ \|\cdot\|_1\ \text{with arbitrary } u,v,a 操作後 \|\cdot\|_1\ \text{is a norm on}\ \mathbb{R}^n 條件：無規則：forall_intro · 依賴：S02, S03, S04, S05, forall_intro 葉節點依據：forall_intro + and_intro_elim S02 至 S05 對任意 u、v、a 證明三條公理，沒有用到具體數值；依 ∀ 引入與合取，ℓ¹ 公式是 ℝⁿ 上的範數。 S07 · implies操作前 \|v\|_\infty=\max_i|v_i| 操作後 \|v\|_\infty=|v_k|\ge 0\ \text{for some } k 條件：n\ge 1 規則：max_finite · 依賴：G2, max_finite, abs_rules 葉節點依據：max_finite + abs_rules n≥1，有限個數的最大值存在且等於其中某個 |v_k|，而絕對值非負，所以 ‖v‖_∞≥0（N1 的前半）。 S08 · equivalent操作前 \|v\|_\infty=0 操作後 v=0 條件：無規則：max_finite · 依賴：S07, G1, max_finite, L_abs_zero 葉節點依據：max_finite + L_abs_zero + coord_ops 正向：若 max|v_i|=0，對每個 i 有 0≤|v_i|≤0，所以 |v_i|=0，依 L_abs_zero 得 v_i=0，即 v=0。反向：v=0 時每個 |v_i|=0，最大值為 0。 S09 · equivalent操作前 \|av\|_\infty=\max_i|a||v_i| 操作後 \|av\|_\infty=|a|\max_i|v_i|=|a|\,\|v\|_\infty 條件：|a|\ge 0 規則：max_finite · 依賴：G1, G2, abs_rules, max_finite, mono_nonneg 葉節點依據：abs_rules + max_finite + mono_nonneg + order_basics |(av)_i|=|a||v_i|。記 M=max|v_i|=|v_k|。上界（S09.1）：每個 |a||v_i|≤|a|M，所以最大值 ≤|a|M；下界（S09.2）：|a||v_k|=|a|M 本身是其中一個值，所以最大值 ≥|a|M。兩者合起來相等，這是 N2。提出的是 |a|≥0，不是 a。 S10 · implies操作前 |u_i+v_i|\ \text{for each } i 操作後 \|u+v\|_\infty\le\|u\|_\infty+\|v\|_\infty 條件：無規則：max_finite · 依賴：G1, G2, abs_rules, max_finite, ineq_add 葉節點依據：abs_rules + max_finite + ineq_add + coord_ops 對每個 i：|u_i+v_i|≤|u_i|+|v_i|（三角不等式），而 |u_i|≤‖u‖_∞、|v_i|≤‖v‖_∞，相加得 |u_i+v_i|≤‖u‖_∞+‖v‖_∞。每個值都不超過同一個上界 K=‖u‖_∞+‖v‖_∞，所以最大值也不超過 K。這是 N3。 S11 · implies操作前 (N1),(N2),(N3)\ \text{for}\ \|\cdot\|_\infty\ \text{with arbitrary } u,v,a 操作後 \|\cdot\|_\infty\ \text{is a norm on}\ \mathbb{R}^n 條件：無規則：forall_intro · 依賴：S07, S08, S09, S10, forall_intro 葉節點依據：forall_intro + and_intro_elim S07 至 S10 對任意 u、v、a 證明三條公理；依 ∀ 引入與合取，ℓ^∞ 公式是 ℝⁿ 上的範數。 S12 · implies操作前 u=(3,-4,1),\ v=(-1,2,5) 操作後 \|u\|_1=8,\ \|u\|_\infty=4,\ \|v\|_1=8,\ \|v\|_\infty=5 條件：無規則：numeric_evaluation · 依賴：G4, G2 葉節點依據：numeric_evaluation + abs_rules 直接用公式：‖u‖₁=3+4+1=8，‖u‖_∞=max(3,4,1)=4；‖v‖₁=1+2+5=8，‖v‖_∞=max(1,2,5)=5。兩個向量的 ℓ¹ 範數相同，但 ℓ^∞ 範數不同：不同範數衡量的大小不同。 S13 · implies操作前 u+v=(2,-2,6) 操作後 \|u+v\|_1=10\le 16,\ \|u+v\|_\infty=6\le 9 條件：無規則：numeric_evaluation · 依賴：S12, S05, S10 葉節點依據：numeric_evaluation + coord_ops u+v=(2,−2,6)。‖u+v‖₁=2+2+6=10≤8+8=16；‖u+v‖_∞=6≤4+5=9。這兩個數值與 S05、S10 的一般結論一致，但它們只是實例，不是證明。 S14 · implies操作前 -2u=(-6,8,-2) 操作後 \|-2u\|_1=16=|-2|\cdot 8,\ \|-2u\|_\infty=8=|-2|\cdot 4 條件：無規則：numeric_evaluation · 依賴：S12, S04, S09 葉節點依據：numeric_evaluation + coord_ops −2u=(−6,8,−2)。‖−2u‖₁=6+8+2=16=2·8，‖−2u‖_∞=8=2·4。乘的是 |−2|=2，不是 −2；範數不會是負的。 S15 · implies操作前 \varphi(v)=|v_1|\ \text{on}\ \mathbb{R}^3 操作後 \varphi(0,1,0)=0,\ (0,1,0)\neq 0;\ \varphi\ \text{is not a norm} 條件：無規則：quantifier_negation · 依賴：G4, quantifier_negation, G3 葉節點依據：quantifier_negation + abs_rules + numeric_evaluation φ 滿足非負、齊次（|a v₁|=|a||v₁|）與三角不等式（|u₁+v₁|≤|u₁|+|v₁|），而且都對所有向量成立。但 N1 要求 φ(v)=0 只在 v=0 時發生；v=(0,1,0)≠0 卻有 φ(v)=|0|=0。一個反例否定這條全稱公理，所以 φ 不是範數（它只是半範數）。 S16 · implies操作前 \psi(v)=(\|v\|_1)^2,\ e_1=(1,0,0),\ e_2=(0,1,0) 操作後 \psi(e_1+e_2)=4>2=\psi(e_1)+\psi(e_2);\ \psi(2e_1)=4\neq 2=|2|\psi(e_1) 條件：無規則：quantifier_negation · 依賴：G4, S06, quantifier_negation 葉節點依據：quantifier_negation + numeric_evaluation + power_laws ψ≥0，且由 S03，ψ(v)=0 ⇔ ‖v‖₁=0 ⇔ v=0，所以 N1 成立。但 ψ(e₁+e₂)=(1+1)²=4，而 ψ(e₁)+ψ(e₂)=1+1=2，三角不等式失敗；ψ(2e₁)=2²=4，而 |2|ψ(e₁)=2，齊次性也失敗。所以 ψ 不是範數。 ## 局部子步與引理 S03.1 · equivalent操作前 t\in\mathbb{R} 操作後 |t|=0\iff t=0 條件：無規則：case_analysis · 依賴：abs_rules, case_analysis 葉節點依據：abs_rules + case_analysis + order_basics 若 t=0，|0|=0。若 t≠0，分兩種情況：t>0 時 |t|=t>0；t<0 時 |t|=−t>0。兩種情況 |t|≠0。所以 |t|=0 恰好在 t=0 時成立。這證明了引理 L_abs_zero。 S09.1 · implies操作前 |v_i|\le M\ \text{for every } i,\ |a|\ge 0 操作後 \max_i|a||v_i|\le|a|M 條件：|a|\ge 0 規則：mono_nonneg · 依賴：max_finite, mono_nonneg, abs_rules 葉節點依據：mono_nonneg + max_finite 每個 |v_i|≤M，乘以 |a|≥0 不改變方向：|a||v_i|≤|a|M。所有值都不超過 |a|M，所以它們的最大值也不超過。 S09.2 · implies操作前 M=|v_k| 操作後 |a|M=|a||v_k|\le\max_i|a||v_i| 條件：無規則：max_finite · 依賴：S09.1, max_finite 葉節點依據：max_finite 最大值 M 由某個 |v_k| 取到，所以 |a|M=|a||v_k| 是被取最大值的數之一，不超過它們的最大值。與 S09.1 合起來得等號。 ## 逐步反向審查 - S16 · premise_audit · S03, quantifier_negation, numeric_evaluation — 每條失敗的公理只需一個精確反例；ψ 通過 N1 不能補救。 - S15 · premise_audit · G3, quantifier_negation, abs_rules — 否證只需一個向量；其餘兩條公理成立並不能補救。 - S14 · premise_audit · S12, numeric_evaluation — 實例，與 S04、S09 一致；不作為證明。 - S13 · premise_audit · S12, numeric_evaluation — 精確計算；不推出任何全稱結論。 - S12 · premise_audit · G4, numeric_evaluation — 精確整數計算；只關於這兩個向量。 - S11 · premise_audit · S07, S08, S09, S10, forall_intro, and_intro_elim — 三條公理缺一不可。 - S10 · premise_audit · abs_rules, max_finite, ineq_add — 需要一個與 i 無關的共同上界；不宣稱等號。 - S09.2 · premise_audit · max_finite — 需要最大值被取到（有限個數）。 - S09.1 · premise_audit · max_finite, mono_nonneg — 需要乘數非負；若乘以負數，方向會反轉（見錯誤控制）。 - S09 · inverse_equivalence · abs_rules, max_finite, mono_nonneg — 兩邊是同一個數（上下界相等），等式雙向成立；關鍵條件是 |a|≥0。 - S08 · inverse_equivalence · max_finite, L_abs_zero, G1 — 正向用「每項不超過最大值」與 L_abs_zero，反向用 |0|=0；兩個方向都有理由。 - S07 · premise_audit · max_finite, abs_rules — 需要 n≥1 使最大值存在；不宣稱反向。 - S06 · premise_audit · S02, S03, S04, S05, forall_intro, and_intro_elim — 三條公理缺一不可。 - S05 · premise_audit · abs_rules, sum_order, finite_sum_rules — 需要逐座標的三角不等式；不宣稱等號成立。 - S04 · inverse_equivalence · abs_rules, finite_sum_rules, coord_ops — 每個等號都是等值改寫，可逆向讀。 - S03.1 · inverse_equivalence · abs_rules, case_analysis, order_basics — t=0、t>0、t<0 三種情況涵蓋全部實數（三分律），兩個方向都已論證；不使用 L_abs_zero 本身。 - S03 · inverse_equivalence · sum_order, L_abs_zero, G1 — 兩個方向都有各自的理由：正向用「和不小於每一項」與 L_abs_zero，反向用 |0|=0。 - S02 · premise_audit · abs_rules, sum_order — 只需絕對值非負；不宣稱反向。 - S01 · premise_audit · G3, mko_norm — 此步只列出義務，不推出新事實。 ## 錯誤控制與反例有限點通過測試不是範數證明MKO 指出的誤解是以有限點通過非負與三角測試就宣稱任意公式是範數。ψ 處處非負，且在 e₁ 與 −e₁ 上 ψ(0)=0≤1+1 通過三角測試，但在 e₁、e₂ 上失敗（S16）。S13、S14 對 ℓ¹、ℓ^∞ 的數值也只是實例；資格來自 S02 至 S11 的全稱證書。三條公理都要核：半範數不一定是範數φ(v)=|v₁| 的非負、齊次與三角不等式對所有向量都成立，最容易被誤認為範數；它失敗的是「只在 v=0 時為 0」（S15）。正定性與其他兩條同樣必須證明。最大值的齊次性要提出 |a|max_i(c t_i)=c·max_i t_i 只對 c≥0 成立：t=(1,3)、c=−1 時，max(−1,−3)=−1，而 −1·max(1,3)=−3。S09 先把 |a v_i| 寫成 |a||v_i|，再提出非負的 |a|，才可用 S09.1 的單調性。 - ψ(v)=(‖v‖₁)² 處處非負，且在 e₁、−e₁ 上通過三角不等式，所以 ψ 是範數 → reject — ψ(e₁+e₂)=4>2=ψ(e₁)+ψ(e₂)。 - φ(v)=|v₁| 是 ℝ³ 上的範數 → reject — φ(0,1,0)=0，但 (0,1,0)≠0。 - ‖u+v‖₁=10≤16 這個例子證明了 ℓ¹ 的三角不等式 → reject — 一個實例不是全稱證明；證明是 S05 的逐座標論證。 - 對任意實數 c，max_i(c t_i)=c·max_i t_i → reject — c=−1、t=(1,3)：左邊 −1，右邊 −3。 ## 結論與限制對所有 n≥1、所有 u,v∈ℝⁿ 與 a∈ℝ，‖v‖₁=Σ|v_i| 與 ‖v‖_∞=max|v_i| 都滿足 (N1) 非負且只在 v=0 時為 0、(N2) ‖av‖=|a|‖v‖、(N3) 三角不等式，所以兩者都是 ℝⁿ 上的範數。例：u=(3,−4,1)、v=(−1,2,5) 有 ‖u‖₁=‖v‖₁=8、‖u‖_∞=4、‖v‖_∞=5、‖u+v‖₁=10≤16、‖u+v‖_∞=6≤9。φ(v)=|v₁| 因 φ(0,1,0)=0 不是範數；ψ(v)=(‖v‖₁)² 因 ψ(e₁+e₂)=4>2 不是範數。 - sum_order、max_finite、mono_nonneg、ineq_add 與 coord_ops 是本稿的前提，不在本稿中由實數公理推出。 - N1 至 N10 只是 S12 至 S14 具體向量的數值；範數資格不依賴它們。誘導度量與 Banach 空間屬於 MKO 的 formal next。 ## 驗證及來源綁定 15 個本稿宣告算術檢查；只支持所列算式。 - source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f - adopted source SHA-256: 69969d495840bc7b4387481a8711aa588a4d19c47ffa88dc52585857ed099067 - original source SHA-256: 69969d495840bc7b4387481a8711aa588a4d19c47ffa88dc52585857ed099067 - Lean: NOT_RUN · independent AI: NOT_MEASURED [同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-real-normed-vector-space-01.json)