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 logarithmic norm bounds forward and reverse matrix exponentials

Statement

For $A \in M_{n} (C)$ , $n \geq 1$ , and $τ \geq 0$ ,

$∥ e^{τ A} ∥_{2} \leq e^{τ μ_{2} (A)} .$

Consequently, for $t \leq 0$ , $∥ e^{t A} ∥_{2} \leq e^{∣ t ∣ μ_{2} (- A)}$ . No normality, spectral stability, or sign assumption on $μ_{2} (A)$ is required.

Facts & Assumptions

Given: $A \in M_{n} (C)$ , $n \geq 1$ , and $τ \geq 0$ .

[F1]

The Euclidean logarithmic norm is a real Rayleigh-quotient maximum: $Re ⟨ A x, x ⟩ \leq μ_{2} (A) ∥ x ∥_{2}^{2}$ for all $x \in C^{n}$ , and $μ_{2} (A) \in R$ .

[F2]

The exponential series of a bounded operator: on a Banach space, $y (t) = e^{t A} x$ is differentiable with $y^{'} (t) = A y (t)$ .

[F3]

Every finite-dimensional normed space is Banach: the finite-dimensional normed space $C^{n}$ is complete.

[F4]

The operator norm is zero on the zero domain and otherwise is max_{||v||=1} ||Tv||: $∥ T ∥_{2} = \max_{∥ x ∥_{2} = 1} ∥ T x ∥_{2}$ for a finite-dimensional endomorphism.

[F5]

The exponential function is smooth and $(\exp)^{'} = \exp$ : the scalar real exponential satisfies $(e^{x})^{'} = e^{x}$ .

[F6]

The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ : a real function continuous on a closed interval and differentiable on its interior satisfies the mean-value identity at some interior point.

[F7]

The exponential is a continuous bijection from $R$ onto $(0, \infty)$ : $e^{r} > 0$ for every $r \in R$ .

Proof

technique · direct

1.1givenF2F3algebra

Fix $x \in C^{n}$ and set $y (t) : = e^{t A} x$ and $q (t) : = ∥ y (t) ∥_{2}^{2}$ . By [F2] and [F3], $y^{'} (t) = A y (t)$ . If $Δ_{h} : = y (t + h) - y (t)$ , differentiability gives $Δ_{h} / h \to A y (t)$ ; expanding the inner product gives $q (t + h) - q (t) = 2 Re ⟨ Δ_{h}, y (t) ⟩ + ∥ Δ_{h} ∥_{2}^{2}$ , so $q^{'} (t) = 2 Re ⟨ A y (t), y (t) ⟩$ .

2.1step 1.1F1F5algebra

By [F1], $q^{'} (t) \leq 2 μ_{2} (A) q (t)$ . Put $a (t) : = e^{- 2 μ_{2} (A) t}$ and $g (t) : = a (t) q (t)$ . By [F5], $a^{'} (t) = - 2 μ_{2} (A) a (t)$ : when $μ_{2} (A) \neq 0$ , write its difference quotient as $(- 2 μ_{2} (A)) e^{- 2 μ_{2} (A) t} (e^{- 2 μ_{2} (A) h} - 1) / (- 2 μ_{2} (A) h)$ and use $(e^{r})^{'} ∣_{r = 0} = 1$ ; when $μ_{2} (A) = 0$ , $a$ is constant. The identity $\frac{a (t + h) q (t + h) - a (t) q (t)}{h} = a (t + h) \frac{q (t + h) - q (t)}{h} + q (t) \frac{a (t + h) - a (t)}{h}$ and the resulting limits give $g^{'} (t) = a (t) (q^{'} (t) - 2 μ_{2} (A) q (t)) \leq 0$ .

3.1step 2.1F6F7algebra

If $t = 0$ , the desired vector inequality is equality. If $t > 0$ , [F6] applied to $g$ on $[0, t]$ and step 2.1 give $g (t) \leq g (0) = ∥ x ∥_{2}^{2}$ . By [F7], $e^{2 μ_{2} (A) t} > 0$ ; multiplying and taking nonnegative square roots yields $∥ e^{t A} x ∥_{2} \leq e^{t μ_{2} (A)} ∥ x ∥_{2}$ .

4.1step 3.1F2F4algebra∎

Taking the maximum over unit vectors $x$ and using [F4] proves $∥ e^{τ A} ∥_{2} \leq e^{τ μ_{2} (A)}$ . For $t \leq 0$ , apply the proved inequality to $- A$ at time $∣ t ∣$ ; termwise equality of the exponential series gives $e^{∣ t ∣ (- A)} = e^{t A}$ , proving the reverse-time claim.

Depends on

Used by

Dependency tree · two levels

48 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)