Algebraic multiplicity is at most geometric multiplicity times the index

Proved

JordanBound.algMult_le_geomMult_mul_index

by mbrcic · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

control-theoryjordan-formlinear-algebramatrices

Let $A$ be an $n \times n$ complex matrix and let $\mu \in \mathbb{C}$ . Write

$n_\mu$ for the algebraic multiplicity of $\mu$ , its multiplicity as a root of the characteristic polynomial of $A$ ;
$g_\mu = \dim \ker(\mu I - A)$ for the geometric multiplicity;
$\nu_\mu$ for the index of $\mu$ , its multiplicity as a root of the minimal polynomial of $A$ .

The claim is

n_\mu \;\le\; g_\mu \cdot \nu_\mu .

Equivalently, $g_\mu \ge \lceil n_\mu / \nu_\mu \rceil$ . The multiplicative form is the one stated, so that no truncated division on the naturals is involved.

Why it holds. In a Jordan form of $A$ , the blocks carrying the eigenvalue $\mu$ number exactly $g_\mu$ , each has size at most $\nu_\mu$ , and their sizes sum to $n_\mu$ . A sum of $g_\mu$ terms each at most $\nu_\mu$ is at most $g_\mu \nu_\mu$ . When $\mu$ is not an eigenvalue of $A$ every quantity is $0$ and the inequality is trivial, so no hypothesis on $\mu$ is needed.

Reduction. This should be a short consequence of results already on the platform rather than new machinery: the string basis for a nilpotent map and the Jordan basis for a complex linear map are proved here, as is the formula recovering the number of Jordan blocks of each size from the kernel dimensions $d_r = \dim\ker(A - \mu I)^r$ . What remains is to read $g_\mu$ as the block count, $\nu_\mu$ as the largest block size, and $n_\mu$ as the total.

Where it is used. This is equation (5) of Klamka's 1972 note, the step that lets his sufficient conditions for uncontrollability and unobservability of a linear time-invariant system be checked from the characteristic and minimal polynomials alone, without computing any eigenvalue. The consequence he draws is that if $g_\mu$ exceeds the rank of the input matrix $B$ , then the Hautus pencil $[\mu I - A \;\; B]$ cannot have full rank and the system $\dot x = Ax + Bu$ is uncontrollable. That second half is elementary once the pencil characterisation of controllability is available; this inequality is the half that needs the block structure, and it is the only thing standing between the pencil argument and Klamka's printed hypothesis.

Preamble

import Mathlib
open Matrix

Formal statement

namespace JordanBound

theorem algMult_le_geomMult_mul_index
    {n : ℕ} (A : Matrix (Fin n) (Fin n) ℂ) (μ : ℂ) :
    A.charpoly.rootMultiplicity μ
      ≤ Module.finrank ℂ
          (LinearMap.ker (μ • (1 : Matrix (Fin n) (Fin n) ℂ) - A).mulVecLin)
        * (minpoly ℂ A).rootMultiplicity μ := by
  sorry

end JordanBound

Source

J. Klamka, “Uncontrollability and unobservability of multivariable systems,” IEEE Transactions on Automatic Control, vol. 17, no. 5, pp. 725–726, Oct. 1972, doi:10.1109/TAC.1972.1100128 — p. 726, equation (5), together with equations (1)–(4), which are its proof. Print states it as αᵢ ≥ int[(nᵢ + νᵢ - 1)/νᵢ], where αᵢ is the number of Jordan blocks carrying λᵢ, nᵢ its multiplicity in the characteristic polynomial and νᵢ its index; the form submitted here is the same inequality cleared of the division.

View graph