LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generated

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

A determinant and Frobenius norm give a certified lower bound for small-block separation

Statement

Let $F \in {R, C}$ , $q \geq 1$ , and $M \in F^{q \times q}$ . Define

$δ (M) = {\begin{cases} 0, & ∥ M ∥_{F} = 0, \\ \frac{∣ \det M ∣}{∥ M ∥_{F}^{q - 1}}, & ∥ M ∥_{F} > 0. \end{cases}$

With the empty product convention when $q = 1$ , $0 \leq δ (M) \leq σ_{\min} (M)$ .

Facts & Assumptions

Given: A finite square matrix $M$ over $R$ or $C$ .

[F1]

Every linear map between finite-dimensional real or complex inner product spaces admits a singular value decomposition: There are orthonormal bases on the domain and codomain and singular values $s_{1} \geq \dots \geq s_{r} > 0$ , with zeros appended to length $q$ , giving $M = U diag (s_{1}, \dots, s_{q}) V^{*}$ for unitary $U, V$ .

[F2]

Spectral and Frobenius norms are unitarily invariant, are given by singular values, and satisfy the sharp rank comparison: $∥ M ∥_{F}^{2} = \sum_{i = 1}^{q} s_{i}^{2}$ .

[F3]

For same-sized finite square matrices over a commutative ring, $\det (A B) = \det (A) \det (B)$ : $\det (A B) = \det (A) \det (B)$ for square matrices over a commutative ring.

[F4]

Orthogonal and unitary operators form groups, and their determinants have modulus one: every unitary matrix has determinant modulus one.

[F5]

The determinant of a triangular matrix is the product of its diagonal entries: the determinant of a diagonal matrix is the product of its diagonal entries.

Proof

1.1givenF1

If $M = 0$ , then $δ (M) = 0 = σ_{\min} (M)$ by the definition and the singular values in [F1].

1.2F1F2F3F4F5choosealgebra

Suppose $M \neq 0$ and choose singular values $s_{1} \geq \dots \geq s_{q} \geq 0$ from [F1], with $M = U diag (s_{1}, \dots, s_{q}) V^{*}$ for unitary $U, V$ . By [F3], $\det (M) = \det (U) \det (diag (s_{1}, \dots, s_{q})) \det (V^{*})$ ; [F4] gives $∣ \det (U) ∣ = ∣ \det (V^{*}) ∣ = 1$ , and [F5] gives $\det (diag (s_{1}, \dots, s_{q})) = \prod_{i = 1}^{q} s_{i}$ . Thus $∣ \det M ∣ = \prod_{i = 1}^{q} s_{i}$ . By [F2], every $s_{i} \leq ∥ M ∥_{F}$ ; hence $∣ \det M ∣ \leq s_{q} ∥ M ∥_{F}^{q - 1}$ .

2.1step 1.2algebra∎

Since $s_{q} = σ_{\min} (M)$ and $∥ M ∥_{F} > 0$ , divide the inequality in step 1.2 by $∥ M ∥_{F}^{q - 1}$ to obtain $δ (M) \leq σ_{\min} (M)$ . The lower bound $δ (M) \geq 0$ follows from its definition.

Depends on

Used by

Finite-budget Bartels-Stewart solve for a Sylvester equation Algorithm

Dependency tree · two levels

32 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Valeria Simoncini, Computational Methods for Linear Matrix Equations, SIAM Review 58(3), 2016 (standard reference, not scraped)
Elias Jarlebring, Numerical Methods for Lyapunov Equations, lecture notes in numerical linear algebra, 2017 (standard reference, not scraped)