Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-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 maximum trace over q-dimensional orthonormal frames is the sum of the top q eigenvalues

Statement

Let A∈Rp×p be symmetric with eigenvalues λ1≥⋯≥λp, counted with multiplicity. For 1≤q≤p and every Q∈Rp×q satisfying QTQ=Iq,

tr⁡(QTAQ)≤∑j=1qλj.

Equality is attained by taking the columns of Q to be orthonormal eigenvectors for the q largest eigenvalues. Equality holds exactly when the column space of Q contains every eigenspace with eigenvalue greater than λq, is orthogonal to every eigenspace with eigenvalue less than λq, and uses a subspace of dimension q−#{j:λj>λq} from the eigenspace with eigenvalue λq.

Facts & Assumptions

Given: A symmetric real matrix A∈Rp×p and an integer q with 1≤q≤p.

[F1]

In the standard real coordinate inner product, ⟨x,y⟩=∑i<pxiyi (The standard formulas ⟨x,y⟩=∑k<nxkyk on Rn and ∑k<nxkyk‾ on Cn are inner products).

[F2]

In an orthonormal basis, a real endomorphism is self-adjoint exactly when its matrix is symmetric (In an orthonormal basis, self-adjoint means conjugate-transpose symmetry and normal means commuting with the conjugate transpose).

[F3]

Every self-adjoint endomorphism of a finite-dimensional real inner-product space has an orthonormal eigenbasis (Real spectral theorem: a self-adjoint endomorphism of a finite-dimensional real inner product space has an orthonormal eigenbasis).

[F4]

The trace of a square matrix is the sum of its diagonal entries (The trace tr⁡(A) as the sum of the diagonal entries).

[F5]

For conformable rectangular matrices A,B, tr⁡(AB)=tr⁡(BA) (For A∈Mm×n(F) and B∈Mn×m(F), tr⁡(AB)=tr⁡(BA)).

Proof

1.1givenF1F2F3

By [F1] and [F2], the matrix A represents a self-adjoint map on Rp with its standard inner product; [F3] gives an orthonormal eigenbasis u1,…,up ordered with eigenvalues λ1≥⋯≥λp.

2.1step 1.1F4F5algebra

For any feasible Q, put P=QQT. Since QTQ=Iq, PT=P and P2=P, so uj=Puj+(I−P)uj is an orthogonal decomposition and aj:=ujTPuj=∥QTuj∥22=∥Puj∥22 lies in [0,1]. This decomposition gives aj=0 exactly when Puj=0, and aj=1 exactly when Puj=uj. Also ∑j=1paj=tr⁡(P)=q by [F4]. The frame trace equals tr⁡(PA) by [F5]. If U has columns uj and Λ=UTAU=diag⁡(λj), [F5] and UUT=I give tr⁡(PA)=tr⁡(UTPAU)=tr⁡((UTPU)Λ)=∑j=1pλjaj.

3.1step 2.1algebra

Because λj≥λq for j≤q and λj≤λq for j>q, ∑j=1pλjaj≤∑j=1q(λjaj+λq(1−aj))≤∑j=1qλj. The first inequality uses ∑jaj=q; the second uses 0≤aj≤1 and λj≥λq for j≤q.

4.1step 2.1step 3.1algebra

The first inequality in step 3.1 has nonnegative difference ∑j>q(λq−λj)aj, so equality requires aj=0 whenever λj<λq. The second has nonnegative difference ∑j≤q(λj−λq)(1−aj), so equality requires aj=1 whenever λj>λq. By step 2.1, these conditions say the chosen subspace contains all higher-eigenvalue eigenspaces, is orthogonal to all lower-eigenvalue eigenspaces, and takes its remaining dimension in the λq eigenspace. Conversely, each such subspace makes both differences zero. If A=0, all eigenvalues are zero and both differences vanish for every feasible Q, as does the stated equality condition.

5.1step 1.1step 3.1F3∎

Taking the first q vectors of the eigenbasis from step 1.1 as the columns of Q gives a feasible frame and makes the trace equal ∑j=1qλj. Thus the upper bound is the attained maximum, with the stated equality cases.

Depends on

Used by

Dependency tree · two levels

20 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