LemmaStatement: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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.

The Euclidean logarithmic norm is a real Rayleigh-quotient maximum

Statement

For $n \geq 1$ and $A \in M_{n} (C)$ , $H_{A} = (A + A^{*}) / 2$ is Hermitian, its eigenvalues are real, and

$μ_{2} (A) = λ_{\max} (H_{A}) = \max_{∥ x ∥_{2} = 1} Re ⟨ A x, x ⟩ .$

Facts & Assumptions

Given: $n \geq 1$ , $A \in M_{n} (C)$ , and $H_{A} = (A + A^{*}) / 2$ as in The Euclidean logarithmic norm of a complex matrix.

[F1]

The standard formulas $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ and $\sum_{k < n} x_{k} \overline{y_{k}}$ on $C^{n}$ are inner products: $⟨ x, y ⟩ = \sum_{i < n} x_{i} \overline{y_{i}}$ is the standard complex inner product, linear in the first variable.

[F2]

In orthonormal bases, the matrix of the adjoint is the conjugate transpose of the matrix: in orthonormal coordinates, the matrix of the adjoint is the conjugate transpose.

[F3]

Self-adjoint and normal endomorphisms of a finite-dimensional real or complex inner product space: a self-adjoint endomorphism satisfies $H^{*} = H$ and is normal.

[F4]

Complex spectral theorem: a normal endomorphism of a finite-dimensional complex inner product space has an orthonormal eigenbasis, and conversely: every normal endomorphism of a finite-dimensional complex inner-product space has an orthonormal eigenbasis.

[F5]

The Euclidean logarithmic norm of a complex matrix: $μ_{2} (A) = λ_{\max} (H_{A})$ for $H_{A} = (A + A^{*}) / 2$ .

Proof

technique · direct

1.1givenF2F3algebra

By [F2], $H_{A}^{*} = (A^{*} + A) / 2 = H_{A}$ , so $H_{A}$ is self-adjoint and hence normal by [F3].

2.1step 1.1F1F3F4choosealgebra

By [F4], choose an orthonormal eigenbasis $u_{1}, \dots, u_{n}$ for $H_{A}$ , with $H_{A} u_{j} = λ_{j} u_{j}$ . Since $λ_{j} = ⟨ H_{A} u_{j}, u_{j} ⟩$ and self-adjointness gives $⟨ H_{A} u_{j}, u_{j} ⟩ = ⟨ u_{j}, H_{A} u_{j} ⟩ = \overline{⟨ H_{A} u_{j}, u_{j} ⟩}$ , each eigenvalue $λ_{j}$ is real; the finite set has a largest member.

3.1givenstep 2.1F5

By [F5], $μ_{2} (A) = λ_{\max} (H_{A}) = \max_{j} λ_{j}$ .

4.1step 2.1step 3.1F1F2algebra∎

For $x = \sum_{j = 1}^{n} c_{j} u_{j}$ , [F1] and orthonormality give $⟨ H_{A} x, x ⟩ = \sum_{j} λ_{j} ∣ c_{j} ∣^{2} \leq μ_{2} (A) \sum_{j} ∣ c_{j} ∣^{2} = μ_{2} (A) ∥ x ∥_{2}^{2}$ . Also $⟨ H_{A} x, x ⟩ = Re ⟨ A x, x ⟩$ because $⟨ A^{*} x, x ⟩ = \overline{⟨ A x, x ⟩}$ . A unit eigenvector for the largest $λ_{j}$ attains equality, proving the maximum formula.

Depends on

Used by

The logarithmic norm bounds forward and reverse matrix exponentials Lemma

Cited to discharge well-definedness by The Euclidean logarithmic norm of a complex matrix.

Dependency tree · two levels

23 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

Nicholas J. Higham, What Is the Logarithmic Norm? (standard reference, not scraped)