PropositionStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-28

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.

For normal endomorphisms, the spectral functional calculus respects sums, products, adjoints, and composition of scalar functions

Statement

Let $V$ be a finite-dimensional complex inner product space, let $T : V \to V$ be normal, and let $f, g : σ (T) \to C$ .

$(f + g) (T) = f (T) + g (T)$ .
$(f g) (T) = f (T) g (T)$ .
If $\overline{f} (λ) = \overline{f (λ)}$ , then $\overline{f} (T) = f (T)^{*}$ .
If $h : f (σ (T)) \to C$ , then $(h \circ f) (T) = h (f (T))$ .

Facts & Assumptions

Given: A finite-dimensional complex inner product space $V$ , a normal endomorphism $T : V \to V$ , its spectral resolution $T = \sum_{j = 1}^{r} λ_{j} P_{j},$ and functions $f, g : σ (T) \to C$ .

[L1]

A normal endomorphism has a spectral resolution by pairwise orthogonal projections $P_{j}$ with $P_{i} P_{j} = 0$ for $i \neq j$ and $P_{j}^{2} = P_{j} = P_{j}^{*}$ (A normal endomorphism is a sum of its eigenvalues times pairwise orthogonal projections, and each spectral projection is a polynomial in the endomorphism).

Proof

technique · direct

1.1

By definition $f (T) = \sum_{j} f (λ_{j}) P_{j}$ and $g (T) = \sum_{j} g (λ_{j}) P_{j}$ , so $(f + g) (T) = \sum_{j} (f (λ_{j}) + g (λ_{j})) P_{j} = f (T) + g (T)$ ; using $P_{i} P_{j} = 0$ for $i \neq j$ and $P_{j}^{2} = P_{j}$ from [L1], one also gets $f (T) g (T) = \sum_{j} f (λ_{j}) g (λ_{j}) P_{j} = (f g) (T)$ .

L1algebra

1.2

Because each $P_{j}$ is self-adjoint by [L1], one has $f (T)^{*} = {(\sum_{j} f (λ_{j}) P_{j})}^{*} = \sum_{j} \overline{f (λ_{j})} P_{j} = \overline{f} (T)$ .

L1algebra

2.1

Put $μ_{1}, \dots, μ_{s}$ for the distinct values taken by $f$ on $σ (T)$ and define $Q_{ℓ} : = \sum_{f (λ_{j}) = μ_{ℓ}} P_{j}$ ; then the $Q_{ℓ}$ are pairwise orthogonal projections, $f (T) = \sum_{ℓ = 1}^{s} μ_{ℓ} Q_{ℓ}$ , and applying the same definition of functional calculus once more gives $h (f (T)) = \sum_{ℓ = 1}^{s} h (μ_{ℓ}) Q_{ℓ} = \sum_{j} h (f (λ_{j})) P_{j} = (h \circ f) (T)$ .

L1step 1.1algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

10 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

Sheldon Axler, Linear Algebra Done Right, fourth edition (standard reference, not scraped)