Induced infinity operator norm

The induced infinity operator norm measures the largest possible amplification of a vector’s supremum norm under matrix action.

For a finite vector \(x=(x_j)\),

For a finite matrix \(A=(A_{ij})\), the induced matrix norm is

This is the maximum absolute row-sum norm. Rows appear because row \(i\) computes output coordinate \((Ax)_i\).

Compute one matrix completely

Take

First discard signs inside the row budgets:

The absolute row sums are

and

The second row is the maximizing row. Therefore

The norm is not the largest entry, which would be \(4\). It adds magnitudes within each row before taking the maximum.

Verify the action inequality on a concrete vector

Choose

Its supremum norm is

Matrix action gives

Hence

and the induced-norm inequality reads

The inequality is true but not tight for this \(x\). An operator norm is a worst-case factor, not the amplification experienced by every vector.

A vector that attains equality

The maximizing row \((3,4)\) has both entries positive. Choose matching signs:

Then

so

This equality shows that the bound is sharp for this matrix.

For a general real maximizing row, choose each input coordinate to match the entry’s sign. For a nonzero complex entry \(A_{i_*j}=|A_{i_*j}|e^{i\theta_j}\), choose \(x_j=e^{-i\theta_j}\). Then \(A_{i_*j}x_j=|A_{i_*j}|\), so every summand in the selected row points in the same phase and the row sum is attained.

Why the inequality always holds

The \(i\)-th output coordinate is

Apply the triangle inequality:

The last quantity is independent of \(i\). Taking the maximum over output coordinates gives

The sign or phase construction above supplies a unit vector that reaches the maximizing row budget. For finite nonempty coordinate spaces, the row-sum formula is therefore not merely an upper bound; it equals the induced operator norm.

Near-miss: column sums compute a different norm

For the same matrix, the absolute column sums are

Their maximum is \(6\), not \(7\). If one incorrectly declared \(\lVert A\rVert_\infty=6\), the attaining vector refutes the claimed bound:

Maximum absolute column sum is the matrix norm induced by the vector one-norm. Maximum absolute row sum is induced by the vector infinity norm. The two conventions agree for some matrices, but not in general.

Products multiply worst-case budgets

For compatible matrices,

Operationally, \(B\) acts first and can amplify by at most \(\lVert B\rVert_\infty\); \(A\) acts next and can amplify that intermediate vector by at most \(\lVert A\rVert_\infty\).

For the project’s forward product

repeated submultiplicativity gives

and

If every factor through horizon \(k\) has norm at most \(C\), then

For the constant system \(A_j=A\) from the example, this gives

These are upper envelopes. Cancellation and invariant directions can make actual growth much smaller.

The empty-index policy

If the row and column index type is empty, there is one empty vector and one empty square matrix. The supremum of the empty family of row sums is zero, so

for that unique matrix. The unique identity matrix equals the unique zero matrix, and its selected row-sum norm is also zero.

Mathlib’s matrix-product and matrix-vector inequalities remain meaningful for empty finite index types. The project’s four normalized finite-product norm theorems ask for Nonempty ι. That hypothesis supplies positive dimension and the usual identity normalization \(\lVert I\rVert_\infty=1\) used by the current proof interface at horizon zero.

The algebraic definitions of the forward product, its split law, and its chronological vector action do not require positive dimension.

In Lean: expose the maximum row-sum formula

The matrix norm notation depends on a scoped instance:

open scoped Matrix.Norms.Operator

Inside that scope, the following theorem identifies the notation.

Matrix.linfty_opNorm_def A

The scope is semantic context, not cosmetic formatting. Matrices admit several useful norms, and the same notation should not be interpreted without knowing which instance is active.

In Lean: bound one matrix-vector action

Matrix.linfty_opNorm_mulVec A x

In Lean: pass the bound through a finite product

NonlinearDynamics.Random.MatrixProducts.linfty_opNorm_forwardProduct_mulVec_le_pow A C k hA x

Exact source excerpts

Resource label: pinned Mathlib. The selected norm formula and its two fundamental bounds come from the repository’s pinned Mathlib/Analysis/Matrix/Normed.lean:

theorem linfty_opNorm_def (A : Matrix m n α) :
    ‖A‖ = ((Finset.univ : Finset m).sup fun i : m => ∑ j : n, ‖A i j‖₊ : ℝ≥0) := by
  change ‖fun i => toLp 1 (A i)‖ = _
  simp [Pi.norm_def, PiLp.nnnorm_eq_of_L1]

theorem linfty_opNorm_mul (A : Matrix l m α) (B : Matrix m n α) :
    ‖A * B‖ ≤ ‖A‖ * ‖B‖ :=
  linfty_opNNNorm_mul _ _

theorem linfty_opNorm_mulVec (A : Matrix l m α) (v : m → α) :
    ‖A *ᵥ v‖ ≤ ‖A‖ * ‖v‖ :=
  linfty_opNNNorm_mulVec _ _

The use of sup rather than an arbitrarily chosen maximizing row makes the definition total even when there are no rows.

Full project check. This uses the repository’s pinned Lean and Mathlib dependencies and may require substantial disk space and memory. The project then iterates submultiplicativity in FiniteProducts.lean:

theorem linfty_opNorm_forwardProduct_le_prod (A : ℕ → Matrix ι ι 𝕜) (k : ℕ) :
    ‖forwardProduct A k‖ ≤ ∏ j ∈ Finset.range k, ‖A j‖ := by
  induction k with
  | zero => simp
  | succ k ih =>
      rw [forwardProduct_succ, Finset.prod_range_succ]
      calc
        ‖A k * forwardProduct A k‖ ≤ ‖A k‖ * ‖forwardProduct A k‖ :=
          norm_mul_le _ _
        _ ≤ ‖A k‖ * ∏ j ∈ Finset.range k, ‖A j‖ :=
          mul_le_mul_of_nonneg_left ih (norm_nonneg _)
        _ = (∏ j ∈ Finset.range k, ‖A j‖) * ‖A k‖ := by
          rw [mul_comm]

The induction follows the definition: the newest factor \(A_k\) is multiplied on the left, then its norm budget is appended to the scalar product.

Standalone tutorial: arithmetic worksheet

Standalone tutorial. This worksheet imports only Std. It calculates the integer matrix, row and column sums, two matrix-vector actions, and the corresponding numerical inequalities. It does not define Mathlib’s norm instance or prove the general theorem.

Save it as InfinityNorm2Scratch.lean:

import Std

structure Matrix2 where
  a00 : Int
  a01 : Int
  a10 : Int
  a11 : Int
deriving Repr

structure Vector2 where
  x0 : Int
  x1 : Int
deriving Repr

def row0Sum (A : Matrix2) : Nat :=
  A.a00.natAbs + A.a01.natAbs

def row1Sum (A : Matrix2) : Nat :=
  A.a10.natAbs + A.a11.natAbs

def column0Sum (A : Matrix2) : Nat :=
  A.a00.natAbs + A.a10.natAbs

def column1Sum (A : Matrix2) : Nat :=
  A.a01.natAbs + A.a11.natAbs

def matrixInfinityNorm (A : Matrix2) : Nat :=
  max (row0Sum A) (row1Sum A)

def vectorInfinityNorm (x : Vector2) : Nat :=
  max x.x0.natAbs x.x1.natAbs

def mulVec (A : Matrix2) (x : Vector2) : Vector2 :=
  { x0 := A.a00 * x.x0 + A.a01 * x.x1
    x1 := A.a10 * x.x0 + A.a11 * x.x1 }

def boundHolds (A : Matrix2) (x : Vector2) : Bool :=
  decide (vectorInfinityNorm (mulVec A x)
    ≤ matrixInfinityNorm A * vectorInfinityNorm x)

def A : Matrix2 :=
  { a00 := 1, a01 := -2, a10 := 3, a11 := 4 }

def test : Vector2 := { x0 := 2, x1 := -1 }
def attainer : Vector2 := { x0 := 1, x1 := 1 }

#eval row0Sum A
#eval row1Sum A
#eval matrixInfinityNorm A
#eval max (column0Sum A) (column1Sum A)
#eval mulVec A test
#eval vectorInfinityNorm (mulVec A test)
#eval boundHolds A test
#eval mulVec A attainer
#eval vectorInfinityNorm (mulVec A attainer)
#eval boundHolds A attainer

Run it with:

elan run leanprover/lean4:v4.32.0 lean InfinityNorm2Scratch.lean

The scalar outputs should include row sums \(3,7\), matrix infinity norm \(7\), column maximum \(6\), output norms \(4\) and \(7\), and true for both inequality checks. The displayed vectors should be \((4,2)\) and \((-1,7)\).

Try the exact declarations in the project

import NonlinearDynamics.Random.MatrixProducts.FiniteProducts

open scoped Matrix.Norms.Operator

#check Matrix.linfty_opNorm_def
#check Matrix.linfty_opNorm_mul
#check Matrix.linfty_opNorm_mulVec
#check Matrix.linfty_opNorm_diagonal
#check Matrix.linfty_opNorm_eq_opNorm
#check NonlinearDynamics.Random.MatrixProducts.forwardProduct
#check NonlinearDynamics.Random.MatrixProducts.forwardProduct_zero
#check NonlinearDynamics.Random.MatrixProducts.forwardProduct_succ
#check NonlinearDynamics.Random.MatrixProducts.forwardProduct_add
#check NonlinearDynamics.Random.MatrixProducts.forwardProduct_const
#check NonlinearDynamics.Random.MatrixProducts.linfty_opNorm_forwardProduct_le_prod
#check NonlinearDynamics.Random.MatrixProducts.linfty_opNorm_forwardProduct_le_pow
#check NonlinearDynamics.Random.MatrixProducts.linfty_opNorm_forwardProduct_mulVec_le_prod
#check NonlinearDynamics.Random.MatrixProducts.linfty_opNorm_forwardProduct_mulVec_le_pow

cd formalization
lake env lean -DwarningAsError=true NonlinearDynamics/Random/MatrixProducts/FiniteProducts.lean

Compare the nearby matrix norms

For the worked matrix:

These are not interchangeable. The Frobenius norm is natural for entrywise Euclidean geometry. The induced infinity norm is natural when a state is measured by its largest coordinate.

Mathlib also proves that the concrete row-sum norm equals the ordinary operator norm of the continuous linear map \(x\mapsto Ax\) after the finite function spaces are equipped with supremum norms. That is the exact sense in which the row-sum formula is induced.

What product growth does and does not say

The project theorem is deterministic and finite-horizon. It uses a scalar type with the RCLike interface, covering the real and complex numbers needed by Mathlib’s analytic matrix norm API.

A bound such as

does not by itself prove:

• equality or sharpness of the product bound;
• contraction unless an additional condition such as \(C\lt1\) is supplied;
• a lower growth bound;
• convergence of the matrix product or vector orbit;
• a spectral-radius identity;
• measurability or integrability of random matrix factors;
• existence of an asymptotic growth rate; or
• a Lyapunov exponent or multiplicative ergodic theorem.

These estimates are the finite-time envelope used by later stability and random-cocycle arguments, not their conclusion.

Distinctions and failure modes

Exercises

1. Compute the induced infinity norm of \(\bigl[\begin{smallmatrix}2&-1\\-4&0\end{smallmatrix}\bigr]\) and find a supremum-norm-one attaining vector.
2. For the worked \(A\), find a nonzero vector whose output amplification is strictly less than one.
3. Replace the entries by complex numbers and construct the conjugate-phase vector for a chosen maximizing row.
4. Prove the row-sum bound directly for a \(3\times3\) matrix before reading the general triangle-inequality derivation.
5. Explain why the empty matrix has norm zero without violating positive definiteness of a norm.

Where to continue

Ordered Finite Matrix Products and Operator-Norm Growth derives the product, geometric-power, and vector-orbit bounds from the exact Lean declarations. The forward matrix product entry fixes the chronological multiplication order.

For a deliberately different matrix geometry, read Hermitian Frobenius geometry . Random Matrices from Outcomes to Spectra explains how deterministic matrices become values of measurable random variables. No probability layer appears in the finite-products module itself.

References

Mathlib contributors. Norms on finite matrices, Mathlib 4 documentation. This official source defines the maximum absolute row-sum norm, proves its product and matrix-vector inequalities, and identifies it with the operator norm on finite supremum-norm spaces.

Roger A. Horn and Charles R. Johnson. Matrix Analysis, second edition, Cambridge University Press, 2013. Chapter 5 develops induced matrix norms, attaining vectors, and finite-dimensional norm comparisons.

W. A. Coppel. Dichotomies in Stability Theory, Lecture Notes in Mathematics 629, Springer, 1978. This is classical motivation for transition-matrix bounds in stability theory; no dichotomy theorem is claimed here.

V. I. Oseledets. A multiplicative ergodic theorem. Characteristic Ljapunov exponents of dynamical systems, Transactions of the Moscow Mathematical Society 19 (1968), 197-231. This primary source supplies asymptotic motivation only.

Nonlinear Dynamics in Lean contributors. FiniteProducts.lean, the checked project source for ordered products and induced-infinity-norm growth estimates.

The upstream Mathlib revision audited for this entry is commit 81a5d257, pinned by formalization/lake-manifest.json.