Real Banach space: norm, induced metric and completeness of (ℝ², ℓ¹)

Goal and scope

On V=ℝ² take the ℓ¹ norm ‖x‖₁=|x₁|+|x₂| and the metric induced by that same norm, d₁(x,y)=‖x−y‖₁. (1) Prove that ‖·‖₁ is a norm and d₁ a metric, and compute d₁((3,−1),(1,2)). (2) Prove completely, from the Cauchy completeness of the reals, that (ℝ²,d₁) is complete, so (ℝ²,‖·‖₁) is a real Banach space; also cite the named theorem that finite-dimensional real normed spaces are complete. (3) Prove that ‖·‖₁ violates the parallelogram law and hence is induced by no inner product.

Works inside the MKO's scope: the explicit finite-dimensional ℝ² with the named ℓ¹ norm, the metric induced by that same norm (assumption a1); completeness is handled by a proof plus a named-theorem certificate, not by sampling finitely many Cauchy sequences (assumption a2). The guide proves the special case n=2, ℓ¹ completely, assuming only Cauchy completeness of the reals; the general finite-dimensional case (including ℓ^∞) is cited from the named theorem. Infinite-dimensional Banach spaces and Hilbert-space theory are not treated, and the canonical MKO and its English edition are not changed.

Givens and symbols

• abs_rules
• order_basics
• vector_space_axioms
• completeness_axiom
• numeric_evaluation

• G1 — V=ℝ² with coordinatewise addition and real scalar multiplication is a real vector space.
• G2 — ‖x‖₁=|x₁|+|x₂|; the metric is the one induced by this same norm, d₁(x,y)=‖x−y‖₁, and no other metric is used.
• G3 — Numerical example: x=(3,−1) and y=(1,2); for the parallelogram law, u=(1,0) and v=(0,1).

• \|x\|_1=|x_1|+|x_2| — the ℓ¹ norm on ℝ²
• d_1(x,y)=\|x-y\|_1 — the metric induced by the same norm
• \|x\|_\infty=\max(|x_1|,|x_2|) — the ℓ^∞ norm, for contrast only
• (x^{(m)})_{m\ge 1} — a sequence in ℝ², with coordinates x^{(m)}_k
• a=(a_1,a_2) — the candidate limit
• \varepsilon,\ N — the tolerance and threshold in the limit and Cauchy definitions

Rules and sources

• abs_rules · prerequisite — Absolute value (reals): |u|=u if u≥0 and |u|=−u if u<0; |u|≥0; |uv|=|u||v|; triangle inequality |u+v|≤|u|+|v|; |u|<r ⇔ −r<u<r.
• order_basics · prerequisite — Order of the reals: exactly one of u<v, u=v, u>v holds; u<v and v<w give u<w; u<v gives u+w<v+w; u<v and w>0 give uw<vw; u<v and w<0 give uw>vw.
• vector_space_axioms · prerequisite — Vector space axioms (over ℝ or another field F): vectors form a commutative group under addition; scalar multiplication satisfies a(u+v)=au+av, (a+b)u=au+bu, (ab)u=a(bu) and 1u=u.
• completeness_axiom · prerequisite — Completeness of the reals: every nonempty subset of ℝ that is bounded above has a least upper bound (supremum).
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• def_unfold · prerequisite — Unfolding a definition: replacing a defined term by its definition (or folding it back) does not change whether a statement is true.
• distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu.
• add_assoc · prerequisite — Associativity of addition: (u+v)+w=u+(v+w).
• add_comm · prerequisite — Commutativity of addition: u+v=v+u.
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• metric_def · prerequisite — Metric: d:X×X→ℝ with d(x,y)≥0 and d(x,y)=0 ⇔ x=y; d(x,y)=d(y,x); triangle inequality d(x,z)≤d(x,y)+d(y,z).
• add_zero · prerequisite — Additive identity: u+0=u.
• seq_limit_def · prerequisite — Limit of a sequence: a_n→L means that for every ε>0 there is N such that |a_n−L|<ε for all n≥N.
• frac_rules · prerequisite — Fraction rules (all denominators nonzero): a/c+b/c=(a+b)/c; (a/b)(c/d)=(ac)/(bd); (a/b)/(c/d)=(ad)/(bc) (also needing c≠0); a/b=(ak)/(bk) for k≠0.
• forall_intro · prerequisite — ∀-introduction (generalization): if a statement is proved for an arbitrary element x, with no extra assumption on x, it holds for every x in the domain.
• contrapositive · prerequisite — Contrapositive: P⇒Q is equivalent to ¬Q⇒¬P. The converse Q⇒P is in general not equivalent to P⇒Q.
• eq_replace · prerequisite — Replacement of equals: an expression inside a statement may be replaced by an equal expression without changing whether the statement is true.
• add_inverse · prerequisite — Additive inverse: every u has −u with u+(−u)=0; u−v means u+(−v).
• mko_banach_def · cited — A real Banach space binds one carrier, its real vector operations, its norm, the metric induced by that norm and completeness into one structure. This slice uses exact named-theorem certificates for finite-dimensional ℝⁿ with ℓ¹ or ℓ^∞, not sampled sequences as completeness proofs. · mko-real-banach-space
• mko_norm_def · cited — A norm sends vectors to nonnegative real numbers, with norm(v)=0 iff v=0, norm(av)=|a| norm(v), and norm(u+v)≤norm(u)+norm(v). · mko-real-normed-vector-space
• mko_complete_def · cited — A metric space (X,d) is complete if every Cauchy sequence in X converges to some point of X; testing a few sequences does not establish general completeness. · mko-complete-metric-space
• cauchy_def · prerequisite — In a metric space (X,d), a sequence (x^{(m)}) is Cauchy if for every ε>0 there is N with d(x^{(m)},x^{(p)})<ε for all m,p≥N; it converges to a if for every ε>0 there is N with d(x^{(m)},a)<ε for all m≥N.
• real_cauchy_complete · prerequisite — Cauchy completeness of the reals: every Cauchy sequence in ℝ (with distance |s−t|) converges to a real number. This is a standard consequence of the least-upper-bound axiom and is not reproved here.
• inner_product_def · prerequisite — A real inner product ⟨·,·⟩ is a real-valued function, linear in each slot, symmetric and positive definite; a norm is induced by it when ‖x‖²=⟨x,x⟩ for every x.
• thm_findim_complete · cited — Every finite-dimensional real normed vector space is complete in the metric induced by its norm; in particular, for every positive integer n, (ℝⁿ,‖·‖₁) and (ℝⁿ,‖·‖_∞) are real Banach spaces. · Theo Buehler and Dietmar A. Salamon, Functional Analysis, 11 May 2016 notes, Corollary 1.2.7, p.16
• L_induced_metric · lemma — If ‖·‖ is a norm on a real vector space V, then d(x,y)=‖x−y‖ is a metric on V.
• L_coord_le · lemma — For x,y∈ℝ² and k=1,2: |x_k−y_k|≤d₁(x,y).
• L_parallelogram · lemma — If a norm is induced by a real inner product, then for all u,v: ‖u+v‖²+‖u−v‖²=2‖u‖²+2‖v‖².

Main derivation

(\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}

Substeps and lemmas

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

Reverse audits

• S15 · sufficient_goal_reduction · S06, S07, S12, S14, and_intro_elim — The goal is the conjunction of the three tasks; each part is proved forwards by the listed steps, and H⇒G by conjunction introduction.
• S14.2 · inverse_equivalence · S14.1, add_inverse, inner_product_def — Adding and rewriting are equal-value operations, so both directions hold.
• S14.1 · inverse_equivalence · inner_product_def — The expansion is an identity, so both sides have the same value.
• S14 · premise_audit · L_parallelogram, contrapositive, numeric_evaluation — Only the necessary direction of the lemma is used (inner-product norm ⇒ parallelogram law); one counterexample suffices (N5, N6).
• S13 · premise_audit · thm_findim_complete, S12 — The citation carries citation_verified; finite dimension is an essential hypothesis, and infinite-dimensional normed spaces can fail to be complete (see the error controls).
• S12 · sufficient_goal_reduction · S05, S06, S11, forall_intro, mko_complete_def, mko_banach_def — Goal G: Banach. Sufficient condition H: a norm, the metric induced by that norm, completeness; H⇒G by the MKO's definition. H is proved forwards in S05, S06 and S09 to S11, using neither G nor any sampled sequence.
• S11.2 · premise_audit · S11.1, order_basics, cauchy_def — It uses that strict inequalities in the same direction add; ε was not specified, so the conclusion holds for every ε.
• S11.1 · premise_audit · seq_limit_def, order_basics — It needs ε/2>0 (a positive number halved is positive) and the property of the maximum; there are only two coordinates, so the max is finite.
• S11 · premise_audit · S10, cauchy_def — Both coordinates must converge; convergence of one coordinate alone would not give convergence in d₁.
• S10 · premise_audit · S09, real_cauchy_complete — The premise is that the coordinate sequences are Cauchy (S09); real_cauchy_complete is a prerequisite not proved here, see the open items.
• S09 · premise_audit · S08, cauchy_def, order_basics — It uses transitivity of ≤ and <; the sequence is arbitrary, which lets S12 generalize.
• S08.1 · premise_audit · abs_rules, order_basics — It uses only |t|≥0 and 'u≥0 ⇒ s+u≥s'.
• S08 · premise_audit · L_coord_le — Only a one-way inequality is claimed; a small coordinate distance does not make d₁ small unless both coordinates are small (handled in S11).
• S07 · premise_audit · G2, numeric_evaluation — Exact computation (N1, N2); it only shows the two metrics differ and implies nothing about completeness.
• S06.3 · premise_audit · mko_norm_def, vector_space_axioms — It needs only the norm triangle inequality and associativity of vector addition; no converse is claimed.
• S06.2 · inverse_equivalence · mko_norm_def, vector_space_axioms, abs_rules — Every link of the chain is an equal rewriting, so both directions hold.
• S06.1 · inverse_equivalence · mko_norm_def, vector_space_axioms — Each ⇔ comes from a norm axiom or from invertibility of vector addition, so both directions hold.
• S06 · premise_audit · S05, L_induced_metric — It needs ‖·‖₁ to be a norm (S05); the converse (every metric comes from a norm) is false, see the negative controls.
• S05 · sufficient_goal_reduction · S02, S03, S04, mko_norm_def — Goal: ‖·‖₁ is a norm. Sufficient condition: the three axioms; all three are proved forwards, and the goal is never used as a premise.
• S04 · premise_audit · abs_rules, order_basics, add_assoc, add_comm — This is an inequality and goes one way only; when equality holds is not claimed. N4 is a finite grid check, not a proof.
• S03 · inverse_equivalence · abs_rules, distributive — Only identities are used, so both sides have the same value; N3 is a finite check on an integer grid and is only auxiliary.
• S02 · inverse_equivalence · abs_rules, order_basics — Backward: for x=(0,0), |0|+|0|=0. The forward direction uses 'a sum of nonnegatives is 0 ⇒ each is 0', from the order axioms.
• S01 · premise_audit · mko_banach_def, G2 — It only unfolds the definition; G2 fixes that the metric comes from the same norm, and the ℓ^∞ contrast in S07 shows that a different metric gives a different structure.

Error controls and negative controls

Sampled Cauchy sequences do not prove completeness

The misconception identified in the MKO is to declare a space Banach after testing a few Cauchy sequences. Completeness quantifies over all Cauchy sequences. Counterexample: the space c₀₀ of finitely supported real sequences with the ℓ¹ norm, and x^{(m)} whose k-th entry is 2^{−k} for k≤m and 0 for k>m; it is Cauchy (for m<p the distance is Σ_{k=m+1}^{p} 2^{−k}<2^{−m}), but a limit y would need y_k=2^{−k}, which is not finitely supported, so c₀₀ is not complete. Many sampled Cauchy sequences in c₀₀ (for example eventually constant ones) do converge, so selecting only such convergent examples need not reveal the defect. Selecting the displayed x^{(m)} and fully proving that it is Cauchy without a limit in c₀₀ does reveal incompleteness; finitely many truncation values alone are still not that proof. Completeness here comes from the proof for an arbitrary sequence in S09 to S12.

The metric must be induced by the same norm

Another misconception identified in the MKO is to call a space Banach because some metric on it is complete. d′(x,y)=min(1,‖x−y‖₁) is a complete metric on ℝ² but is induced by no norm: if d′(x,y)=‖x−y‖ for some norm, then d′(2e₁,0)=2d′(e₁,0); in fact the left side is min(1,2)=1 and the right side is 2·min(1,1)=2. Likewise S07 shows that the ℓ^∞ metric is not the metric induced by ‖·‖₁.

A Banach space need not be a Hilbert space

A complete normed space need not have an inner product inducing its specified norm. The underlying vector space may still carry another, incompatible inner product, such as the standard dot product on ℝ². S14 shows that the ℓ¹ norm violates the parallelogram law (8≠4), so (ℝ²,‖·‖₁) is a Banach space whose norm does not come from an inner product.

• Five Cauchy sequences in (ℝ²,‖·‖₁) were tested and all converged, so it is complete → reject — The conclusion is true, but finite sampling is not a proof; samples in c₀₀ can all converge although c₀₀ is incomplete. Completeness comes from S09 to S12.
• (ℝ²,‖·‖₁) equipped with the ℓ^∞ metric is this Banach space → reject — The ℓ^∞ metric is not induced by ‖·‖₁: the distance between (3,−1) and (1,2) is 3 while ‖x−y‖₁=5.
• d′(x,y)=min(1,‖x−y‖₁) is a complete metric on ℝ², so (ℝ²,d′) is a Banach space → reject — d′ is induced by no norm: d′(2e₁,0)=1, while homogeneity would require 2d′(e₁,0)=2.
• The norm of every Banach space is induced by some inner product → reject — The ℓ¹ norm violates the parallelogram law at u=(1,0), v=(0,1): 8≠4.

Result and limitations

‖x‖₁=|x₁|+|x₂| is a norm on ℝ², d₁(x,y)=‖x−y‖₁ is its induced metric, and d₁((3,−1),(1,2))=5 (the ℓ^∞ metric gives 3, a different metric). The coordinates of any d₁-Cauchy sequence are real Cauchy sequences converging to a₁ and a₂, and d₁(x^{(m)},a)→0, so (ℝ²,‖·‖₁) is a real Banach space; the general finite-dimensional case comes from the named theorem (citation_verified). The ℓ¹ norm violates the parallelogram law at u=(1,0), v=(0,1) (8≠4), so it is induced by no inner product.

• Cauchy completeness of the reals (real_cauchy_complete) is a prerequisite; the guide does not re-derive it from the least-upper-bound axiom.
• That d′=min(1,‖x−y‖₁) is a complete metric and that c₀₀ is incomplete are only sketched in the error controls, not written as full steps.
• N3 and N4 are finite checks on integer grids and are only auxiliary; the general claims of S03 and S04 are proved by the absolute-value rules.

Verification and source binding

8 declared checks for this guide; only the listed expressions are covered.

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

Same-source full JSON (formulas, ASTs, controls and revision log)