Rectangular singular values and adjoint-product spectra

For a linear map A : E →ₗ[𝕜] F between finite-dimensional inner-product spaces, the two Gram operators A†A (on E) and AA† (on F) share their nonzero spectrum, including multiplicity. Mathlib defines the zero-padded singular-value sequence LinearMap.singularValues through A†A only; this file supplies the canonical bridge to the codomain-side Gram operator.

Main results

• TauCeti.nonzeroEigenspaceEquivAdjointCompSelfSelfCompAdjoint: the linear equivalence x ↦ A x (inverse y ↦ μ⁻¹ • A† y) between the nonzero μ-eigenspaces of A†A and AA†;
• TauCeti.eigenvalues_adjointCompSelf_eq_selfCompAdjoint: the sorted eigenvalue lists of A†A and AA† agree at every index below both dimensions;
• LinearMap.singularValues_adjoint: zero-padded adjoint invariance A†.singularValues = A.singularValues;
• TauCeti.sq_singularValues_selfCompAdjoint: the sorted eigenvalues of AA† are the squared singular values of A, zero-padded past the rank;
• TauCeti.le_eigenvalues_selfCompAdjoint_of_norm_sq_floor: a quadratic floor α‖x‖² ≤ ‖Ax‖² forces the first finrank 𝕜 E sorted eigenvalues of AA† to be at least α, and TauCeti.norm_sq_floor_of_le_eigenvalues_adjointCompSelf is the converse direction used to descend from spectral floors back to quadratic floors.

The combinatorial engine is TauCeti.antitone_eq_of_card_filter_eq: two antitone nonnegative finite sequences with equal fiber cardinalities over every nonzero value agree at every index where both are defined.

Proof sources

The eigenspace equivalence and the counting argument are original to this file. The vendored Apache-2.0 excerpt vendor/lean/lean-stat-learning-theory/SingularSystemGram.excerpt.lean (Zhang–Lee–Liu) constructs explicit left singular vectors for Euclidean matrix maps and was consulted as a cross-check for the spectral bookkeeping; no code was copied from it here.

Preferred variant

This is the preferred implementation of the rectangular adjoint-spectrum layer, and the one the Perfect Quench build depends on (via GramSpectrumBridge). A near-identical alternative proof from the dk-work branch (GPT-5.6 High) is preserved verbatim for comparison at RectangularSingularValuesDkVariant.lean; the two differ only in three minor spots, and that variant does not elaborate on the pinned toolchain (its calc form of sq_singularValues_selfCompAdjoint provokes a whnf heartbeat blow-up), which is why this file rewrote that proof.

Sorted sequences determined by fiber cardinalities

Pure finite combinatorics: an antitone nonnegative sequence is determined below any index by the cardinalities of its positive fibers.

theorem TauCeti.antitone_le_apply_iff_lt_card_filter {d : ℕ} {f : Fin d → ℝ} (hf : Antitone f) (c : ℝ) (k : Fin d) : c ≤ f k ↔ ↑k < {i : Fin d | c ≤ f i}.card

For an antitone real sequence on Fin d, the k-th entry is at least c exactly when more than k entries are at least c.

theorem TauCeti.card_filter_le_eq_of_card_filter_eq {d n : ℕ} {f : Fin d → ℝ} {g : Fin n → ℝ} (hcard : ∀ (c : ℝ), c ≠ 0 → {i : Fin d | f i = c}.card = {j : Fin n | g j = c}.card) {c : ℝ} (hc : 0 < c) : {i : Fin d | c ≤ f i}.card = {j : Fin n | c ≤ g j}.card

If two real sequences have fibers of equal cardinality over every nonzero value, their super-level sets over every positive threshold have equal cardinality.

theorem TauCeti.antitone_eq_of_card_filter_eq {d n : ℕ} {f : Fin d → ℝ} {g : Fin n → ℝ} (hf : Antitone f) (hg : Antitone g) (hf0 : ∀ (i : Fin d), 0 ≤ f i) (hg0 : ∀ (j : Fin n), 0 ≤ g j) (hcard : ∀ (c : ℝ), c ≠ 0 → {i : Fin d | f i = c}.card = {j : Fin n | g j = c}.card) {k : ℕ} (hkd : k < d) (hkn : k < n) : f ⟨k, hkd⟩ = g ⟨k, hkn⟩

Two antitone nonnegative finite real sequences with equal fiber cardinalities over every nonzero value agree at every index where both are defined. The zero fibers may have different cardinalities: they absorb the length difference of the two sequences.

The nonzero eigenspace equivalence between A†A and AA†

theorem TauCeti.isSymmetric_self_comp_adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) : (A ∘ₗ LinearMap.adjoint A).IsSymmetric

The codomain Gram operator AA† is symmetric.

theorem TauCeti.apply_mem_eigenspace_selfCompAdjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) {μ : 𝕜} {x : E} (hx : x ∈ Module.End.eigenspace (LinearMap.adjoint A ∘ₗ A) μ) : A x ∈ Module.End.eigenspace (A ∘ₗ LinearMap.adjoint A) μ

A maps each eigenspace of A†A into the same eigenspace of AA†.

theorem TauCeti.adjoint_apply_mem_eigenspace_adjointCompSelf {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) {μ : 𝕜} {y : F} (hy : y ∈ Module.End.eigenspace (A ∘ₗ LinearMap.adjoint A) μ) : (LinearMap.adjoint A) y ∈ Module.End.eigenspace (LinearMap.adjoint A ∘ₗ A) μ

A† maps each eigenspace of AA† into the same eigenspace of A†A.

noncomputable def TauCeti.nonzeroEigenspaceEquivAdjointCompSelfSelfCompAdjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) (μ : 𝕜) (hμ : μ ≠ 0) : ↥(Module.End.eigenspace (LinearMap.adjoint A ∘ₗ A) μ) ≃ₗ[𝕜] ↥(Module.End.eigenspace (A ∘ₗ LinearMap.adjoint A) μ)

The nonzero μ-eigenspaces of A†A and AA† are linearly equivalent, via x ↦ A x with inverse y ↦ μ⁻¹ • A† y. This is the multiplicity-preserving form of the statement that A†A and AA† have the same nonzero spectrum.

Equations

• TauCeti.nonzeroEigenspaceEquivAdjointCompSelfSelfCompAdjoint A μ hμ = LinearEquiv.ofLinearMap (A.restrict ⋯) ((μ⁻¹ • LinearMap.adjoint A).restrict ⋯) ⋯ ⋯

theorem TauCeti.finrank_eigenspace_adjointCompSelf_eq_selfCompAdjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) (μ : 𝕜) (hμ : μ ≠ 0) : Module.finrank 𝕜 ↥(Module.End.eigenspace (LinearMap.adjoint A ∘ₗ A) μ) = Module.finrank 𝕜 ↥(Module.End.eigenspace (A ∘ₗ LinearMap.adjoint A) μ)

Corresponding nonzero eigenspaces of A†A and AA† have equal dimension.

theorem TauCeti.hasEigenvalue_adjointCompSelf_iff_selfCompAdjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) (μ : 𝕜) (hμ : μ ≠ 0) : Module.End.HasEigenvalue (LinearMap.adjoint A ∘ₗ A) μ ↔ Module.End.HasEigenvalue (A ∘ₗ LinearMap.adjoint A) μ

A nonzero scalar is an eigenvalue of A†A exactly when it is an eigenvalue of AA†.

Equality of the sorted nonzero spectra

theorem TauCeti.eigenvalues_congr' {𝕜 : Type u_1} [RCLike 𝕜] {G : Type u_4} [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] [FiniteDimensional 𝕜 G] {S₁ S₂ : G →ₗ[𝕜] G} (h : S₁ = S₂) (hS₁ : S₁.IsSymmetric) (hS₂ : S₂.IsSymmetric) {m : ℕ} (hm : Module.finrank 𝕜 G = m) : hS₁.eigenvalues hm = hS₂.eigenvalues hm

Sorted eigenvalues are congruent along an operator equality. (A primed variant of TauCeti.eigenvalues_congr from SingularSubspace.lean, restated here to keep this file's import footprint minimal; the two should be merged when upstreaming.)

theorem TauCeti.card_filter_eigenvalues_adjointCompSelf_eq_selfCompAdjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) {d n : ℕ} (hd : Module.finrank 𝕜 E = d) (hn : Module.finrank 𝕜 F = n) {c : ℝ} (hc : c ≠ 0) : {i : Fin d | ⋯.eigenvalues hd i = c}.card = {j : Fin n | ⋯.eigenvalues hn j = c}.card

For every nonzero real value, the sorted eigenvalue lists of A†A and AA† have fibers of equal cardinality.

theorem TauCeti.eigenvalues_adjointCompSelf_eq_selfCompAdjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) {d n : ℕ} (hd : Module.finrank 𝕜 E = d) (hn : Module.finrank 𝕜 F = n) {k : ℕ} (hkd : k < d) (hkn : k < n) : ⋯.eigenvalues hd ⟨k, hkd⟩ = ⋯.eigenvalues hn ⟨k, hkn⟩

Rectangular spectral bridge. The sorted (descending) eigenvalue lists of A†A and AA† agree at every index below both space dimensions. Beyond the rank of A both lists are zero, so no hypothesis relating d and n is required.

Adjoint invariance of singular values

theorem LinearMap.singularValues_adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) : (adjoint A).singularValues = A.singularValues

Singular values are invariant under adjoint. Both sequences are zero-padded past the common rank, so the statement needs no relation between the two dimensions.

@[simp]

theorem LinearMap.singularValues_adjoint_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) (k : ℕ) : (adjoint A).singularValues k = A.singularValues k

Pointwise adjoint invariance, convenient for rewriting a fixed index.

theorem TauCeti.sq_singularValues_selfCompAdjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) {n : ℕ} (hn : Module.finrank 𝕜 F = n) (i : Fin n) : A.singularValues ↑i ^ 2 = ⋯.eigenvalues hn i

The sorted eigenvalues of the codomain Gram operator AA† are the squared singular values of A, zero-padded past the rank of A.

theorem TauCeti.hasEigenvalue_selfCompAdjoint_sq_singularValues {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) {i : ℕ} (hi : i < Module.finrank 𝕜 ↥A.range) : Module.End.HasEigenvalue (A ∘ₗ LinearMap.adjoint A) ↑(A.singularValues i ^ 2)

Every positive squared singular value of A is an eigenvalue of AA†.

Quadratic floors and Gram spectra

Provenance

• Original repository: Davis--Kahan/DKPS formalization (Kitware, Inc.).
• Original module: ForMathlib.Analysis.InnerProductSpace.RectangularSingularValues, moved to ForTauCeti in the Wave-1 staging migration; introduced at Davis--Kahan commit 82d20de.
• Extraction class: moved. The Wave-1 migration renamed the namespace ForMathlib to TauCeti; declaration names and proofs are unchanged.
• Original authors / copyright: Jon Crall, GPT-5.6 High, Claude Fable 5; Copyright (c) 2026 Kitware, Inc.; Apache 2.0.
• Spectra influence: none — this module imports only Mathlib and sibling ForTauCeti staging modules.

theorem TauCeti.re_inner_adjointCompSelf_self {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) (x : E) : RCLike.re (inner 𝕜 ((LinearMap.adjoint A ∘ₗ A) x) x) = ‖A x‖ ^ 2

The Gram quadratic form is the squared image norm: re ⟪(A†A) x, x⟫ = ‖A x‖².

theorem TauCeti.le_eigenvalues_adjointCompSelf_of_norm_sq_floor {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) {α : ℝ} (hfloor : ∀ (x : E), α * ‖x‖ ^ 2 ≤ ‖A x‖ ^ 2) {d : ℕ} (hd : Module.finrank 𝕜 E = d) (i : Fin d) : α ≤ ⋯.eigenvalues hd i

A quadratic floor α‖x‖² ≤ ‖Ax‖² bounds every sorted eigenvalue of A†A below by α.

theorem TauCeti.norm_sq_floor_of_le_eigenvalues_adjointCompSelf {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) {α : ℝ} {d : ℕ} (hd : Module.finrank 𝕜 E = d) (hlow : ∀ (i : Fin d), α ≤ ⋯.eigenvalues hd i) (x : E) : α * ‖x‖ ^ 2 ≤ ‖A x‖ ^ 2

Converse direction: if every sorted eigenvalue of A†A is at least α, the quadratic floor α‖x‖² ≤ ‖Ax‖² holds.

theorem TauCeti.finrank_le_of_norm_sq_floor {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) {α : ℝ} (hα : 0 < α) (hfloor : ∀ (x : E), α * ‖x‖ ^ 2 ≤ ‖A x‖ ^ 2) : Module.finrank 𝕜 E ≤ Module.finrank 𝕜 F

A positive quadratic floor forces injectivity, hence finrank E ≤ finrank F.

theorem TauCeti.le_eigenvalues_selfCompAdjoint_of_norm_sq_floor {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) {α : ℝ} (hfloor : ∀ (x : E), α * ‖x‖ ^ 2 ≤ ‖A x‖ ^ 2) {n : ℕ} (hn : Module.finrank 𝕜 F = n) (i : Fin n) (hi : ↑i < Module.finrank 𝕜 E) : α ≤ ⋯.eigenvalues hn i

Quadratic floor to codomain-Gram spectral floor. If α‖x‖² ≤ ‖Ax‖² for every x, then the first finrank 𝕜 E sorted eigenvalues of AA† are at least α. The dimension comparison finrank E ≤ finrank F is not assumed: it is automatic when α > 0, and for α ≤ 0 the claim follows from positivity of the Gram operator.

theorem TauCeti.singularValues_eq_of_gram_eq {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] {F' : Type u_4} [NormedAddCommGroup F'] [InnerProductSpace 𝕜 F'] [FiniteDimensional 𝕜 F'] {A : E →ₗ[𝕜] F} {B : E →ₗ[𝕜] F'} (h : LinearMap.adjoint A ∘ₗ A = LinearMap.adjoint B ∘ₗ B) : A.singularValues = B.singularValues

Singular values only depend on the Gram operator.

theorem TauCeti.singularValues_linearIsometry_comp {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {D : Type u_4} {F : Type u_5} [NormedAddCommGroup D] [InnerProductSpace 𝕜 D] [FiniteDimensional 𝕜 D] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (ι : F →ₗᵢ[𝕜] E) (X : D →ₗ[𝕜] F) : (ι.toLinearMap ∘ₗ X).singularValues = X.singularValues

Postcomposing with a linear isometric embedding preserves singular values.

This is the rectangular analogue of unitary invariance on the codomain. It needs no dimension comparison: the Gram operator is unchanged because an isometry preserves inner products.

theorem TauCeti.LinearIsometry.adjoint_apply_apply {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {D : Type u_4} [NormedAddCommGroup D] [InnerProductSpace 𝕜 D] [FiniteDimensional 𝕜 D] (ι : D →ₗᵢ[𝕜] E) (x : D) : (LinearMap.adjoint ι.toLinearMap) (ι x) = x

The adjoint of a linear isometry is a left inverse. ι⋆ (ι x) = x, because ⟪ι⋆ (ι x), y⟫ = ⟪ι x, ι y⟫ = ⟪x, y⟫ for every y.

theorem TauCeti.LinearIsometry.adjoint_eq_zero_of_mem_orthogonal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {D : Type u_4} [NormedAddCommGroup D] [InnerProductSpace 𝕜 D] [FiniteDimensional 𝕜 D] (ι : D →ₗᵢ[𝕜] E) {y : E} (hy : y ∈ ι.rangeᗮ) : (LinearMap.adjoint ι.toLinearMap) y = 0

The adjoint of a linear isometry annihilates the orthogonal complement of its range. Together with LinearIsometry.adjoint_apply_apply this says ι⋆ is the orthogonal projection onto the source.

theorem TauCeti.singularValues_comp_adjoint_linearIsometry {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {D : Type u_4} {F : Type u_5} [NormedAddCommGroup D] [InnerProductSpace 𝕜 D] [FiniteDimensional 𝕜 D] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (ι : D →ₗᵢ[𝕜] E) (X : D →ₗ[𝕜] F) : (X ∘ₗ LinearMap.adjoint ι.toLinearMap).singularValues = X.singularValues

Precomposing with the adjoint of a linear isometric embedding preserves singular values, with the additional ambient-domain slots padded by zero.

This is the reusable coisometry-padding theorem behind the principal-angle embedding and rectangular zero extension. The analytic content is independent of the eventual Davis--Kahan application: the Gram operator is conjugated onto the isometry range and vanishes on its orthogonal complement.