# Bounded linear operator: exact induced operator norms of a matrix under ℓ^∞ and ℓ¹

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-bounded-linear-operator/)

This is an owner-adopted natural-language teaching guide. Finite/arithmetic checks are not universal proofs; no Lean was run, and review scope is recorded per revision. Original source status labels are retained as historical data. Formulas retain exact TeX; no new semantic AST is invented.

derivation-mko-bounded-linear-operator-01 · production-20261019-adopted-96



## Goal and scope

Let A be the integer matrix with first row (1,−2) and second row (3,4), and T(x)=Ax:ℝ²→ℝ². (1) With the ℓ^∞ norm at both ends, prove that ‖Ax‖_∞≤7‖x‖_∞ for all x and that no smaller constant works, so ‖T‖_{∞→∞}=7 (the maximum absolute row sum). (2) With the ℓ¹ norm at both ends, prove ‖T‖_{1→1}=6 (the maximum absolute column sum). (3) Explain three traps: non-optimal constants, finitely many inputs, and unbounded range.

Works inside the MKO's scope: source and target are the explicit ℝ² with fixed norm names at both ends (assumption a1); ℓ¹ uses the maximum absolute column sum and ℓ^∞ the maximum absolute row sum, and for this matrix both the bound and its attainment are proved completely (assumption a2). The formula for general m-by-n matrices is taken from the MKO's statement and not proved separately. Continuity, duality and spectral theory are not treated, and the canonical MKO and its English edition are not changed.





## Givens and symbols


- abs_rules
- order_basics
- matrix_product_def
- forall_intro
- numeric_evaluation


- G1 — Two named norms on ℝ²: ‖x‖_∞=max(|x₁|,|x₂|) and ‖x‖₁=|x₁|+|x₂|; each task uses one specified name at both the source and the target.
- G2 — A has rows (1,−2) and (3,4); T(x)=Ax.
- G3 — Test vectors: x*=(1,1), e₁=(1,0), e₂=(0,1).


- A=\begin{pmatrix}1&-2\\3&4\end{pmatrix} — the given integer matrix
- \|x\|_\infty=\max(|x_1|,|x_2|) — the ℓ^∞ norm
- \|x\|_1=|x_1|+|x_2| — the ℓ¹ norm
- \|T\|_{\infty\to\infty},\ \|T\|_{1\to1} — the two induced operator norms
- C — an admissible bounding constant
- x^{*}=(1,1) — the vector attaining the ℓ^∞ bound





## 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.
- matrix_product_def · prerequisite — Matrix product: for A of size m×n and B of size n×p, (AB)_{ij}=Σ_{k=1}^{n} A_{ik}B_{kj}. Matrix multiplication is in general not commutative.
- 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.
- 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_comm · prerequisite — Commutativity of addition: u+v=v+u.
- quantifier_negation · prerequisite — Negating quantifiers: ¬(∀x, P(x)) is equivalent to ∃x, ¬P(x), and ¬(∃x, P(x)) is equivalent to ∀x, ¬P(x).
- archimedean · prerequisite — Archimedean property: for every real x there is a natural number n>x; hence for every ε>0 there is n with 1/n<ε.
- and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
- mko_bounded_def · cited — Independent append-only source erratum (owner-adopted in this local revision; not merged or published): first require T:V→W to be linear, and separately require C≥0 with ‖Tx‖_W≤C‖x‖_V for every x. Together these give a bounded linear operator. The growth bound alone does not imply linearity, as x↦|x| shows. For the integer matrices here, exact induced-norm certificates use the maximum absolute column sum for ℓ¹ and row sum for ℓ^∞; an instance pass does not replace a universal certificate. The original citation and canonical MKO are retained. · mko-bounded-linear-operator
- mko_linear_map_def · cited — A real linear map satisfies T(αu+βv)=αT(u)+βT(v); a finite-dimensional matrix formula supplies a universal coordinate certificate. · mko-general-linear-map
- op_norm_def · prerequisite — The induced operator norm ‖T‖ of a bounded operator is the infimum of all admissible constants C (those with ‖Tx‖≤C‖x‖ for all x); if some admissible C₀ is at most every admissible constant, then ‖T‖=C₀.
- max_rules · prerequisite — max(s,t)≥s and max(s,t)≥t; max(s,t)≤K iff s≤K and t≤K.
- L_row_bound · lemma — For reals c₁,c₂ and x∈ℝ²: |c₁x₁+c₂x₂|≤(|c₁|+|c₂|)‖x‖_∞.





## Main derivation

S01 · definitionBefore

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

After

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

Conditions: none

Rule: mko_bounded_def · Uses: G1, mko_bounded_def, op_norm_def

Leaf basis: mko_bounded_def + def_unfold

By the MKO, bounded means there is one constant C that controls every input x (the quantifier order is 'there exists C such that for all x'). The operator norm is the least admissible constant. The norm names at both ends are first fixed as ℓ^∞.



S02 · equivalentBefore

T(x)=Ax

After

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

Conditions: none

Rule: matrix_product_def · Uses: G2, mko_linear_map_def, matrix_product_def

Leaf basis: matrix_product_def + mko_linear_map_def

By the matrix product, the two coordinates of Ax are the rows paired with x. A matrix map is linear (citing the universal certificate of the linear-map node), so T is a linear operator and only boundedness remains.



S03 · equivalentBefore

\|Ax\|_\infty

After

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

Conditions: none

Rule: def_unfold · Uses: S02, G1

Leaf basis: def_unfold

Unfold the ℓ^∞ norm at the target: take the larger absolute value of the two coordinates.



S04 · impliesBefore

|x_1-2x_2|

After

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

Conditions: none

Rule: L_row_bound · Uses: S03

Leaf basis: abs_rules + order_basics + max_rules

First row (1,−2): by Lemma L_row_bound (c₁=1, c₂=−2), the absolute value of the coordinate is at most the absolute row sum 3 times ‖x‖_∞. The lemma is proved in sub-steps S04.1 and S04.2 for all x.



S05 · impliesBefore

|3x_1+4x_2|

After

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

Conditions: none

Rule: L_row_bound · Uses: S03, L_row_bound

Leaf basis: abs_rules + order_basics + max_rules

Second row (3,4): the same lemma (c₁=3, c₂=4) gives the bound 7‖x‖_∞.



S06 · impliesBefore

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

After

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

Conditions: none

Rule: forall_intro · Uses: S03, S04, S05, max_rules

Leaf basis: max_rules + forall_intro + order_basics

Both coordinates are ≤7‖x‖_∞ (since 3‖x‖_∞≤7‖x‖_∞), so their maximum is ≤7‖x‖_∞ as well. x was arbitrary, so by generalization the single constant C=7 controls every input: T is bounded. 7 is exactly the maximum absolute row sum max(1+2, 3+4).



S07 · impliesBefore

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

After

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

Conditions: none

Rule: numeric_evaluation · Uses: S02, G3

Leaf basis: numeric_evaluation + matrix_product_def

Take x* with coordinates equal to the signs of the second-row coefficients (3 and 4 are positive, so 1 and 1): Ax*=(1−2, 3+4)=(−1,7), so ‖Ax*‖_∞=7 while ‖x*‖_∞=1. The bound 7 is attained.



S08 · impliesBefore

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

After

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

Conditions: none

Rule: op_norm_def · Uses: S06, S07, op_norm_def

Leaf basis: op_norm_def + order_basics

Any admissible constant C must work at x*, so 7≤C. C=7 itself is admissible (S06) and is at most every admissible constant, so by definition ‖T‖_{∞→∞}=7, in agreement with the MKO's maximum-absolute-row-sum formula.



S09 · impliesBefore

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

After

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

Conditions: none

Rule: abs_rules · Uses: S02, G1, abs_rules

Leaf basis: abs_rules + order_basics + forall_intro

Now use ℓ¹ at both ends. Sub-step S09.1 regroups by columns to get ‖Ax‖₁≤4|x₁|+6|x₂|, and S09.2 enlarges this to 6‖x‖₁. 6 is the maximum absolute column sum max(|1|+|3|, |−2|+|4|).



S10 · impliesBefore

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

After

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

Conditions: none

Rule: op_norm_def · Uses: S02, S09, G3, op_norm_def

Leaf basis: op_norm_def + numeric_evaluation

Ae₂ is the second column of A, (−2,4), with ℓ¹ norm 2+4=6, while ‖e₂‖₁=1. Every admissible constant C must be ≥6; 6 itself is admissible (S09), so ‖T‖_{1→1}=6.



S11 · impliesBefore

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

After

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}

Conditions: none

Rule: op_norm_def · Uses: S06, S08, S09, S10

Leaf basis: op_norm_def + order_basics

The operator norm depends on the norm names at both ends: the same A gives 7 under ℓ^∞ and 6 under ℓ¹. Non-optimal constants still prove boundedness: by S09, ‖Ax‖₁≤6‖x‖₁≤7‖x‖₁, so C=7 is admissible for ℓ¹; by S06, C=10 is admissible for ℓ^∞. But they are not operator norms, and the MKO forbids passing off an arbitrary admissible bound as the operator norm.



S12 · impliesBefore

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

After

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

Conditions: none

Rule: quantifier_negation · Uses: S02, S07, G3

Leaf basis: quantifier_negation + numeric_evaluation

Looking only at the basis vectors e₁ and e₂, C=5 passes both; but x*=(1,1) gives 7>5, so C=5 is not admissible. Finitely many inputs cannot prove a bound, since one C must control every input; the MKO says an instance pass does not replace a universal certificate.



S13 · impliesBefore

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

After

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

Conditions: none

Rule: archimedean · Uses: S07, mko_linear_map_def

Leaf basis: archimedean + mko_linear_map_def + abs_rules

By linearity T(tx*)=tAx*, with norm 7|t|. For any positive K, the Archimedean property gives t>K/7, and then 7|t|>K, so the range of T is unbounded. Yet T is a bounded operator: boundedness gives a common bound on ‖Tx‖/‖x‖ for x≠0, equivalently ‖Tx‖≤C‖x‖ for every x. At x=0 use T0=0 rather than 0/0. This does not bound the range. The MKO lists 'the range looks bounded' as a misconception.



S14 · impliesBefore

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

After

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

Conditions: none

Rule: and_intro_elim · Uses: S08, S10, S11, S12, S13

Leaf basis: and_intro_elim

Combine: under ℓ^∞, T is bounded with operator norm 7 (the maximum absolute row sum, attained at (1,1)); under ℓ¹ the operator norm is 6 (the maximum absolute column sum, attained at e₂). Non-optimal constants only prove boundedness; finitely many inputs cannot prove a bound; an unbounded range does not prevent boundedness.







## Substeps and lemmas

S04.1 · impliesBefore

|c_1x_1+c_2x_2|

After

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

Conditions: none

Rule: abs_rules · Uses: abs_rules

Leaf basis: abs_rules

The triangle inequality |u+v|≤|u|+|v|, then |c_kx_k|=|c_k||x_k|.



S04.2 · impliesBefore

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

After

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

Conditions: none

Rule: max_rules · Uses: S04.1, max_rules, order_basics

Leaf basis: max_rules + order_basics + distributive

By the property of max, |x_k|≤‖x‖_∞; multiplying by the nonnegative |c_k| keeps the inequality (order axioms), and adding the two terms and factoring out ‖x‖_∞ finishes. S04.1 and S04.2 together prove Lemma L_row_bound.



S09.1 · impliesBefore

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

After

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

Conditions: none

Rule: abs_rules · Uses: abs_rules

Leaf basis: abs_rules + add_comm + distributive

Apply the triangle inequality and |cx|=|c||x| in each row, then collect the coefficients of each |x_k|: the coefficient of |x₁| is the first column's absolute sum 1+3=4, and that of |x₂| is the second column's 2+4=6.



S09.2 · impliesBefore

4|x_1|+6|x_2|

After

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

Conditions: none

Rule: order_basics · Uses: S09.1, order_basics

Leaf basis: order_basics + distributive + abs_rules

Since |x₁|≥0 and 4≤6, 4|x₁|≤6|x₁|; add 6|x₂| and factor out 6.







## Reverse audits


- S14 · sufficient_goal_reduction · S08, S10, S11, S12, S13, and_intro_elim — The goal is the conjunction of the three tasks; each part is proved forwards by the listed steps.
- S13 · premise_audit · archimedean, mko_linear_map_def — It needs T linear and Ax*≠0; only the zero operator has a bounded range.
- S12 · premise_audit · quantifier_negation, numeric_evaluation — One counterexample, x*, suffices to refute C=5 (N7).
- S11 · premise_audit · S06, S08, S09, S10, order_basics — The set of admissible constants is closed upwards (anything larger than an admissible constant is admissible), and the operator norm is its least element (N8).
- S10 · sufficient_goal_reduction · S09, op_norm_def, numeric_evaluation — Goal: ‖T‖_{1→1}=6. Sufficient condition: 6 is admissible (S09) and e₂ forces C≥6 (N4).
- S09.2 · premise_audit · order_basics, distributive — It needs |x₁|≥0; no equality is claimed.
- S09.1 · premise_audit · abs_rules, add_comm, distributive — A one-way inequality plus regrouping; ℓ¹ naturally collects by columns, whereas ℓ^∞ takes the maximum over rows.
- S09 · premise_audit · abs_rules, order_basics, forall_intro — A universal bound; N5 is an auxiliary finite grid check.
- S08 · sufficient_goal_reduction · S06, S07, op_norm_def — Goal: ‖T‖=7. Sufficient condition: 7 is admissible (S06) and every admissible C is ≥7 (S07); both are proved forwards.
- S07 · premise_audit · S02, numeric_evaluation — Exact computation (N1); this single point is used only for the lower bound, never for the upper bound.
- S06 · premise_audit · S04, S05, max_rules, forall_intro — No particular x was substituted; N3 is a finite check on an integer grid and only auxiliary (N2 checks the row sums).
- S05 · premise_audit · L_row_bound — An upper bound; no equality is claimed.
- S04.2 · premise_audit · max_rules, order_basics, distributive — It needs |c_k|≥0; multiplying by a negative number would flip the inequality.
- S04.1 · premise_audit · abs_rules — A one-way inequality; no equality is claimed.
- S04 · premise_audit · L_row_bound — This is an upper bound and claims no equality; attainment is handled separately in S07.
- S03 · inverse_equivalence · def_unfold — Unfolding a definition holds both ways.
- S02 · inverse_equivalence · matrix_product_def — The coordinate formula expands the product, so both sides are the same vector; linearity is cited, not reproved in this step.
- S01 · premise_audit · mko_bounded_def, op_norm_def — It only unfolds the definition; with the quantifiers reversed ('for each x some C') the condition would hold trivially for every linear map and say nothing.





## Error controls and negative controls

Finitely many inputs do not prove a boundOne misconception named by the MKO is to look only at finitely many inputs. C=5 holds at e₁ and e₂, but x*=(1,1) gives 7>5. One C must control every input, so the bound must be proved by the universal estimates of S04 to S06.

An admissible bound need not equal the operator normC=10 proves that T is bounded, but the operator norm is the least admissible constant 7, which is pinned down only by the attaining vector of S07. Likewise under ℓ¹, 7 is admissible but the operator norm is 6.

Bounded does not mean bounded rangeThe range of a nonzero linear operator is always unbounded (S13). A bounded operator is one with ‖Tx‖ controlled by C‖x‖, equivalently a common ratio bound for x≠0; at x=0 use T0=0, not 0/0; taking 'the range looks bounded' as the definition is a misconception named by the MKO.


- ‖Ae₁‖_∞=3≤5 and ‖Ae₂‖_∞=4≤5, so ‖Ax‖_∞≤5‖x‖_∞ for all x → reject — x*=(1,1): ‖Ax*‖_∞=7>5.
- Since ‖Ax‖_∞≤10‖x‖_∞ for all x, ‖T‖_{∞→∞}=10 → reject — 10 is only an admissible constant; the least admissible constant is 7.
- The ℓ^∞ induced operator norm is the maximum absolute column sum max(4,6)=6 → reject — Column sums belong to ℓ¹; ℓ^∞ uses row sums and gives 7, and x* gives 7>6.
- T(tx*)=(−t,7t) has arbitrarily large norm, so T is not a bounded operator → reject — Boundedness means ‖Tx‖≤7‖x‖ for all x, which has nothing to do with whether the range is bounded.





## Result and limitations

For A (rows (1,−2),(3,4)): every x has ‖Ax‖_∞≤7‖x‖_∞, and x*=(1,1) gives ‖Ax*‖_∞=7, so ‖T‖_{∞→∞}=7 (the maximum absolute row sum); every x has ‖Ax‖₁≤6‖x‖₁, and e₂ gives ‖Ae₂‖₁=6, so ‖T‖_{1→1}=6 (the maximum absolute column sum). C=10, or C=7 for ℓ¹, proves boundedness but is not the operator norm; C=5 passes e₁ and e₂ but fails at x*; the range of T is unbounded, yet T is a bounded operator.


- The maximum-row-sum and maximum-column-sum formulas for general m-by-n matrices are taken from the MKO's statement; this guide proves the bound and its attainment completely only for this 2-by-2 matrix.
- N3 and N5 are finite checks on integer grids and only auxiliary; the universal bounds are proved by S04 to S06 and S09.





## Verification and source binding

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


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

[Same-source full JSON (formulas, ASTs, controls and revision log)](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-bounded-linear-operator-01.json)