實 Banach 空間：(ℝ², ℓ¹) 的範數、誘導度量與完備性

目標與範圍

在 V=ℝ² 上取 ℓ¹ 範數 ‖x‖₁=|x₁|+|x₂| 與同一範數誘導的度量 d₁(x,y)=‖x−y‖₁。（一）證明 ‖·‖₁ 是範數、d₁ 是度量，並算出 d₁((3,−1),(1,2))。（二）由實數的 Cauchy 完備性完整證明 (ℝ²,d₁) 完備，所以 (ℝ²,‖·‖₁) 是實 Banach 空間；並引用有限維實賦範空間完備的命名定理。（三）證明 ‖·‖₁ 不滿足平行四邊形律，所以不是由任何內積誘導。

在 MKO 的範圍內工作：明示的有限維 ℝ²、命名的 ℓ¹ 範數，度量必須由同一範數誘導（假設 a1）；完備性以證明加命名定理證書處理，不以有限條 Cauchy 序列抽樣代替（假設 a2）。本稿完整證明 n=2、ℓ¹ 的特例，只假設實數的 Cauchy 完備性；一般有限維情形（含 ℓ^∞）引用命名定理。不處理無限維 Banach 空間或 Hilbert 空間理論，不改動 canonical MKO 或英文 edition。

已知條件與符號

• abs_rules
• order_basics
• vector_space_axioms
• completeness_axiom
• numeric_evaluation

• G1 — V=ℝ²，加法與實數倍數逐坐標進行，是實向量空間。
• G2 — ‖x‖₁=|x₁|+|x₂|；度量取同一範數誘導的 d₁(x,y)=‖x−y‖₁，不使用其他度量。
• G3 — 數值例：x=(3,−1)、y=(1,2)；平行四邊形律的例子 u=(1,0)、v=(0,1)。

• \|x\|_1=|x_1|+|x_2| — ℝ² 上的 ℓ¹ 範數
• d_1(x,y)=\|x-y\|_1 — 由同一範數誘導的度量
• \|x\|_\infty=\max(|x_1|,|x_2|) — ℓ^∞ 範數，只作對照
• (x^{(m)})_{m\ge 1} — ℝ² 中的序列，坐標 x^{(m)}_k
• a=(a_1,a_2) — 候選極限
• \varepsilon,\ N — 收斂與 Cauchy 定義中的容許誤差與門檻

規則與來源

• 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。
• vector_space_axioms · prerequisite — 向量空間公理（實數或其他域 F 上）：加法成交換群；純量乘法滿足 a(u+v)=au+av、(a+b)u=au+bu、(ab)u=a(bu)、1u=u。
• completeness_axiom · prerequisite — 實數完備性：ℝ 的每個非空且有上界的子集都有最小上界（上確界）。
• numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
• def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
• distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。
• add_assoc · prerequisite — 加法結合律：(u+v)+w=u+(v+w)。
• add_comm · prerequisite — 加法交換律：u+v=v+u。
• and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
• metric_def · prerequisite — 度量：d:X×X→ℝ 滿足 d(x,y)≥0 且 d(x,y)=0 ⇔ x=y；d(x,y)=d(y,x)；三角不等式 d(x,z)≤d(x,y)+d(y,z)。
• add_zero · prerequisite — 加法單位元：u+0=u。
• seq_limit_def · prerequisite — 數列極限：a_n→L 表示對每個 ε>0，存在 N 使所有 n≥N 都有 |a_n−L|<ε。
• 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）。
• forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
• contrapositive · prerequisite — 逆否命題：P⇒Q 與 ¬Q⇒¬P 等價。逆命題 Q⇒P 一般不與 P⇒Q 等價。
• eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
• add_inverse · prerequisite — 加法反元素：每個 u 都有 −u，使 u+(−u)=0；u−v 定義為 u+(−v)。
• mko_banach_def · cited — 實 Banach 空間必須把同一載體、實向量運算、範數、由該範數誘導的度量及完備性綁成一體。本輪使用有限維 ℝⁿ 配命名 ℓ¹ 或 ℓ^∞ 範數的精確定理證書，不以序列抽樣證完備。 · mko-real-banach-space
• mko_norm_def · cited — 範數把向量送到非負實數，且 norm(v)=0 當且僅當 v=0、norm(av)=|a| norm(v)、norm(u+v)≤norm(u)+norm(v)。 · mko-real-normed-vector-space
• mko_complete_def · cited — 度量空間 (X,d) 完備，若 X 內每個 Cauchy 序列都收斂到某個仍屬 X 的點；抽樣若干序列不足以證一般完備性。 · mko-complete-metric-space
• cauchy_def · prerequisite — 在度量空間 (X,d) 中，序列 (x^{(m)}) 是 Cauchy 序列，若對每個 ε>0 存在 N 使所有 m,p≥N 有 d(x^{(m)},x^{(p)})<ε；它收斂到 a，若對每個 ε>0 存在 N 使所有 m≥N 有 d(x^{(m)},a)<ε。
• real_cauchy_complete · prerequisite — 實數的 Cauchy 完備性：ℝ 中（以 |s−t| 為距離）每個 Cauchy 序列都收斂到某個實數。這是最小上界公理的標準推論，本稿不重證。
• inner_product_def · prerequisite — 實內積 ⟨·,·⟩ 是兩槽線性、對稱、正定的實值函數；範數由它誘導，指 ‖x‖²=⟨x,x⟩ 對所有 x 成立。
• thm_findim_complete · cited — 每個有限維實賦範向量空間，在由其範數誘導的度量下都是完備的；特別地，對每個正整數 n，(ℝⁿ,‖·‖₁) 與 (ℝⁿ,‖·‖_∞) 都是實 Banach 空間。 · Theo Buehler and Dietmar A. Salamon, Functional Analysis, 11 May 2016 notes, Corollary 1.2.7, p.16
• L_induced_metric · lemma — 若 ‖·‖ 是實向量空間 V 上的範數，則 d(x,y)=‖x−y‖ 是 V 上的度量。
• L_coord_le · lemma — 對 x,y∈ℝ² 與 k=1,2：|x_k−y_k|≤d₁(x,y)。
• L_parallelogram · lemma — 若範數由實內積誘導，則對所有 u,v：‖u+v‖²+‖u−v‖²=2‖u‖²+2‖v‖²。

逐步主鏈

(\mathbb{R}^2,\|\cdot\|_1)\ \text{Banach}

\|\cdot\|_1\ \text{norm}\ \land\ d_1=\|x-y\|_1\ \text{metric}\ \land\ (\mathbb{R}^2,d_1)\ \text{complete}

\|x\|_1=|x_1|+|x_2|=0

x=(0,0);\ \ \text{and}\ \|x\|_1\ge 0\ \text{for all}\ x

\|\lambda x\|_1=|\lambda x_1|+|\lambda x_2|

\|\lambda x\|_1=|\lambda|(|x_1|+|x_2|)=|\lambda|\,\|x\|_1

\|x+y\|_1=|x_1+y_1|+|x_2+y_2|

\|x+y\|_1\le(|x_1|+|y_1|)+(|x_2|+|y_2|)=\|x\|_1+\|y\|_1

\text{S02},\ \text{S03},\ \text{S04}

(\mathbb{R}^2,\|\cdot\|_1)\ \text{is a real normed vector space}

d_1(x,y)=\|x-y\|_1

d_1\ \text{is a metric on}\ \mathbb{R}^2

x=(3,-1),\ y=(1,2)

d_1(x,y)=|2|+|-3|=5;\ \ \max(|2|,|-3|)=3\neq 5

x,y\in\mathbb{R}^2,\ k\in\{1,2\}

|x_k-y_k|\le d_1(x,y)

(x^{(m)})\ \text{Cauchy in}\ (\mathbb{R}^2,d_1)

(x^{(m)}_k)_{m\ge1}\ \text{Cauchy in}\ \mathbb{R}\ \ (k=1,2)

(x^{(m)}_k)_{m\ge1}\ \text{Cauchy in}\ \mathbb{R}

x^{(m)}_k\to a_k\in\mathbb{R}\ (k=1,2),\ \ a=(a_1,a_2)\in\mathbb{R}^2

x^{(m)}_1\to a_1,\ x^{(m)}_2\to a_2

d_1(x^{(m)},a)\to 0

\text{arbitrary Cauchy}\ (x^{(m)})\ \text{converges in}\ (\mathbb{R}^2,d_1)

(\mathbb{R}^2,d_1)\ \text{complete};\ (\mathbb{R}^2,\|\cdot\|_1)\ \text{real Banach space}

\dim\mathbb{R}^n=n<\infty,\ \ \|\cdot\|\in\{\|\cdot\|_1,\|\cdot\|_\infty\}

(\mathbb{R}^n,\|\cdot\|)\ \text{Banach (named-theorem certificate)}

u=(1,0),\ v=(0,1):\ \|u+v\|_1^2+\|u-v\|_1^2=2^2+2^2=8

8\neq 4=2\|u\|_1^2+2\|v\|_1^2\ \Rightarrow\ \|\cdot\|_1\ \text{induced by no inner product}

\text{S06},\ \text{S07},\ \text{S12},\ \text{S14}

(\mathbb{R}^2,\|\cdot\|_1)\ \text{Banach};\ d_1((3,-1),(1,2))=5;\ \|\cdot\|_1\ \text{not from an inner product}

局部子步與引理

d(x,y)=\|x-y\|

d(x,y)\ge 0,\ \ d(x,y)=0\iff x-y=0\iff x=y

d(y,x)=\|y-x\|=\|(-1)(x-y)\|

d(y,x)=|-1|\,\|x-y\|=d(x,y)

x-z=(x-y)+(y-z)

d(x,z)\le d(x,y)+d(y,z)

d_1(x,y)=|x_1-y_1|+|x_2-y_2|

d_1(x,y)\ge|x_1-y_1|\ \text{and}\ d_1(x,y)\ge|x_2-y_2|

\varepsilon>0;\ \exists N_k:\ m\ge N_k\Rightarrow|x^{(m)}_k-a_k|<\tfrac{\varepsilon}{2}

N=\max(N_1,N_2):\ m\ge N\Rightarrow|x^{(m)}_1-a_1|<\tfrac{\varepsilon}{2}\ \land\ |x^{(m)}_2-a_2|<\tfrac{\varepsilon}{2}

m\ge N

d_1(x^{(m)},a)=|x^{(m)}_1-a_1|+|x^{(m)}_2-a_2|<\tfrac{\varepsilon}{2}+\tfrac{\varepsilon}{2}=\varepsilon

\langle u\pm v,u\pm v\rangle

\langle u,u\rangle\pm 2\langle u,v\rangle+\langle v,v\rangle

\langle u+v,u+v\rangle+\langle u-v,u-v\rangle

2\langle u,u\rangle+2\langle v,v\rangle,\ \text{i.e.}\ \|u+v\|^2+\|u-v\|^2=2\|u\|^2+2\|v\|^2

逐步反向審查

• S15 · sufficient_goal_reduction · S06, S07, S12, S14, and_intro_elim — 目標是三個任務的合取；各部分由所列步驟正向證得，H⇒G 由合取引入。
• S14.2 · inverse_equivalence · S14.1, add_inverse, inner_product_def — 相加與改寫都是等值操作，雙向成立。
• S14.1 · inverse_equivalence · inner_product_def — 展開是恆等式，兩邊同值。
• S14 · premise_audit · L_parallelogram, contrapositive, numeric_evaluation — 只用引理的必要方向（內積範數 ⇒ 平行四邊形律）；一組反例足以否定（N5、N6）。
• S13 · premise_audit · thm_findim_complete, S12 — 定理的引用帶 citation_verified；有限維是必要的前提，無限維賦範空間可以不完備（見錯誤控制）。
• S12 · sufficient_goal_reduction · S05, S06, S11, forall_intro, mko_complete_def, mko_banach_def — 目標 G：Banach。足夠條件 H：範數、同一範數誘導的度量、完備；H⇒G 由 MKO 定義。H 由 S05、S06 與 S09 到 S11 正向證得，沒有用到 G，也沒有用到任何序列樣本。
• S11.2 · premise_audit · S11.1, order_basics, cauchy_def — 用到同向嚴格不等式可相加；ε 未被指定，所以結論對每個 ε 成立。
• S11.1 · premise_audit · seq_limit_def, order_basics — 需要 ε/2>0（正數除以 2 仍為正）與最大值的性質；只有兩個坐標，所以 max 有限。
• S11 · premise_audit · S10, cauchy_def — 需要兩個坐標都收斂；只有一個坐標收斂不足以推出 d₁ 收斂。
• S10 · premise_audit · S09, real_cauchy_complete — 前提是坐標序列為 Cauchy（S09）；real_cauchy_complete 是前置規則，未在本稿證明，見待處理項。
• S09 · premise_audit · S08, cauchy_def, order_basics — 用到 ≤ 與 < 的傳遞性；序列是任意的，S12 才能全稱化。
• S08.1 · premise_audit · abs_rules, order_basics — 只用 |t|≥0 與「u≥0 ⇒ s+u≥s」。
• S08 · premise_audit · L_coord_le — 只宣稱一個方向的不等式；坐標距離小並不推出 d₁ 小，除非兩個坐標都小（S11 處理）。
• S07 · premise_audit · G2, numeric_evaluation — 精確計算（N1、N2）；只說明這兩個度量不同，不推出任何完備性結論。
• S06.3 · premise_audit · mko_norm_def, vector_space_axioms — 只需範數三角不等式與向量加法的結合律；不宣稱反向。
• S06.2 · inverse_equivalence · mko_norm_def, vector_space_axioms, abs_rules — 等式鏈每一步都是等值改寫，雙向成立。
• S06.1 · inverse_equivalence · mko_norm_def, vector_space_axioms — 每個 ⇔ 都由範數公理或向量加法的可逆性給出，雙向成立。
• S06 · premise_audit · S05, L_induced_metric — 需要 ‖·‖₁ 是範數（S05）；反向（每個度量都來自範數）不成立，見負向控制。
• S05 · sufficient_goal_reduction · S02, S03, S04, mko_norm_def — 目標：‖·‖₁ 是範數。足夠條件：三項公理；三項都已正向證得，沒有把目標當作前提。
• S04 · premise_audit · abs_rules, order_basics, add_assoc, add_comm — 這是不等式，只有一個方向；等號何時成立不在本稿宣稱範圍內。N4 是有限格點核對，不是證明。
• S03 · inverse_equivalence · abs_rules, distributive — 所用都是恆等式，兩邊同值；N3 在一個整數格上作有限核對，只是輔助。
• S02 · inverse_equivalence · abs_rules, order_basics — 反向：x=(0,0) 時 |0|+|0|=0。正向用「非負數之和為 0 ⇒ 各項為 0」，由順序公理得到。
• S01 · premise_audit · mko_banach_def, G2 — 只展開定義；G2 固定度量必須來自同一範數，S07 的 ℓ^∞ 對照說明換了度量就不是同一結構。

錯誤控制與反例

抽樣 Cauchy 序列不證完備

MKO 指出的誤解是測過幾條 Cauchy 序列就宣稱 Banach。完備性量化所有 Cauchy 序列。反例：有限支撐實數列空間 c₀₀ 配 ℓ¹ 範數，序列 x^{(m)} 的第 k 項在 k≤m 時為 2^{−k}、k>m 時為 0；它是 Cauchy（m<p 時距離 Σ_{k=m+1}^{p} 2^{−k}<2^{−m}），但若有極限 y，坐標必為 y_k=2^{−k}，不是有限支撐，所以 c₀₀ 不完備。在 c₀₀ 中抽到的許多 Cauchy 序列（例如最終為常數的）都收斂，只抽到這些收斂例子不保證揭露缺陷；若選到上述 x^{(m)} 並完整證明它是 Cauchy 且在 c₀₀ 中無極限，就能揭露不完備。有限多個截斷值本身仍不是那個完整證明。本稿的完備性來自 S09 到 S12 對任意序列的證明。

度量必須由同一範數誘導

MKO 的另一個誤解是只知道 metric 完備就宣稱 Banach。d′(x,y)=min(1,‖x−y‖₁) 是 ℝ² 上的完備度量，但不由任何範數誘導：若 d′(x,y)=‖x−y‖ 對某範數成立，則 d′(2e₁,0)=2d′(e₁,0)；實際上左邊 min(1,2)=1，右邊 2·min(1,1)=2。同樣，S07 顯示 ℓ^∞ 度量不是 ‖·‖₁ 誘導的度量。

Banach 空間不一定是 Hilbert 空間

完備的賦範空間不一定有能誘導其指定範數的內積；這不否認底層向量空間可另配不相容的內積，例如 ℝ² 的標準點積。S14 證明 ℓ¹ 範數違反平行四邊形律（8≠4），所以 (ℝ²,‖·‖₁) 是 Banach 空間，但它的範數不來自內積。

• 在 (ℝ²,‖·‖₁) 中測了五條 Cauchy 序列都收斂，所以它完備 → reject — 結論雖真，但有限抽樣不是證明；c₀₀ 中抽樣也能全部收斂卻不完備。完備性來自 S09 到 S12。
• (ℝ²,‖·‖₁) 配上 ℓ^∞ 度量就是這個 Banach 空間 → reject — ℓ^∞ 度量不由 ‖·‖₁ 誘導：(3,−1) 與 (1,2) 的距離是 3，而 ‖x−y‖₁=5。
• d′(x,y)=min(1,‖x−y‖₁) 是 ℝ² 上的完備度量，所以 (ℝ²,d′) 是 Banach 空間 → reject — d′ 不由範數誘導：d′(2e₁,0)=1，而齊次性要求 2d′(e₁,0)=2。
• 每個 Banach 空間的範數都由某個內積誘導 → reject — ℓ¹ 範數在 u=(1,0)、v=(0,1) 違反平行四邊形律：8≠4。

結論與限制

‖x‖₁=|x₁|+|x₂| 是 ℝ² 上的範數，d₁(x,y)=‖x−y‖₁ 是它誘導的度量，d₁((3,−1),(1,2))=5（ℓ^∞ 度量給 3，是不同的度量）。任意 d₁-Cauchy 序列的坐標都是實數 Cauchy 序列，收斂到 a₁、a₂，且 d₁(x^{(m)},a)→0，所以 (ℝ²,‖·‖₁) 是實 Banach 空間；一般有限維情形由命名定理給出（citation_verified）。ℓ¹ 範數在 u=(1,0)、v=(0,1) 違反平行四邊形律（8≠4），所以不由任何內積誘導。

• 實數的 Cauchy 完備性（real_cauchy_complete）是前置規則，本稿不由最小上界公理重新推導。
• 錯誤控制中 d′=min(1,‖x−y‖₁) 是完備度量、c₀₀ 不完備兩件事只以簡述說明，未寫成完整步驟。
• N3、N4 是整數格點上的有限核對，只是輔助；S03、S04 的一般結論由絕對值規則證明。

驗證及來源綁定

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

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: 6d484742c41cc5faf58a8fd96615e0ff74a6ce36d276c7cac9e25d827f7c0e8a
• original source SHA-256: 623ecd0be3adc5a95eedf871819e318c00b6c2f08da1df036992524ab9710438
• Lean: NOT_RUN · independent AI: NOT_MEASURED

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