Singular-value submultiplicativity, Plücker coordinates and the eigenvalue ceiling #
Building on the exterior-power operator-norm engine and the compound matrix, this module proves the
submultiplicativity of the product of the top-k singular values, the Rayleigh / sin-Θ
off-diagonal estimates, and the Plücker bridge giving the top eigenpair and second-eigenvalue
ceiling of the compound of a gapped symmetric map in compound-matrix coordinates.
Main results #
Oseledets.ExteriorNorm.prod_singularValues_comp_le—∏_{i<k} σᵢ(g ∘ f) ≤ (∏_{i<k} σᵢ(g)) · (∏_{i<k} σᵢ(f)), the input to the Oseledets singular-value exponents via Kingman's subadditive ergodic theorem.Oseledets.ExteriorNorm.plucker_eigenpair_ceiling_standard— for a symmetric map with an eigenvalue gap, the top eigenpair and second-eigenvalue ceiling of the compound, in compound-matrix coordinates (the Plücker bridge).Oseledets.ExteriorNorm.norm_offdiag_residual_compound_le,Oseledets.ExteriorNorm.perturbed_compound_gram_ceiling— the off-diagonal numerator bound and theν-ceiling feeding the band-projector increment estimate.
Submultiplicativity of the product of singular values #
Submultiplicativity of the product of the top-k singular values, assembled from the
submultiplicativity engine and the singular-value bridge:
∏_{i<k} σᵢ(g ∘ f) ≤ (∏_{i<k} σᵢ(g)) · (∏_{i<k} σᵢ(f)).
The rank-1 exterior Rayleigh-deficit bound #
The band-projector increment reduces to a rank-1 dominant-eigenvector sin Θ estimate
(sin_sq_le_rayleigh_deficit_div_gap in Oseledets.Lyapunov.OseledetsLimit). This section
provides the deficit-side pieces feeding that core: the per-vector compound operator-norm step
(Lemma 1), the Rayleigh quotient identity and top-eigenvalue ceiling μ₀ = ‖compound‖²
(Lemma 2), and the assembled deficit bound μ₀ − ⟨C_n v', v'⟩ ≤ (1 − 1/κ²)·μ₀ (Lemma 3),
with κ = ‖compound B‖·‖(compound B)⁻¹‖ the compound condition number.
Per-vector L2 operator-norm bound for toEuclideanLin: ‖toEuclideanLin N w‖ ≤ ‖N‖·‖w‖.
Routed through the bundled continuous-linear-map toEuclideanCLM, whose operator norm is the L2
matrix norm ‖N‖ by Matrix.l2_opNorm_toEuclideanCLM.
The k-th compound of the identity matrix is the identity. Via the compound bridge
conjExteriorMap_eq_toEuclideanLin_compound, since ⋀^k id = id (exteriorPower.map_id).
For invertible B, compound k B⁻¹ is a right inverse of compound k B
(compoundMatrix_mul + compoundMatrix_one).
The compound factorisation compound M = (compound B)⁻¹ · compound(B · M), for invertible
B. Used in Lemma 3 to lower-bound ‖compound M‖ by ‖compound(B·M)‖.
The rank-1 lower bound μ̃₀ ≥ cM²/cBi². For invertible B, the
squared compound operator norm of the perturbed cocycle step B · M (= the top eigenvalue μ̃₀ of
Cₙ₊₁ = adjoint Gₙ₊₁ ∘ₗ Gₙ₊₁) is bounded below by cM²/cBi², where cM = ‖compound k M‖ and
cBi = ‖compound k B⁻¹‖. Route: compound k M = compound k B⁻¹ · compound k (B·M) gives
cM ≤ cBi·‖compound(B·M)‖, hence ‖compound(B·M)‖ ≥ cM/cBi; squaring yields the bound.
Lemma 1 — the rank-1 per-vector step. The squared norm of the compound of a product,
applied to w, is dominated by ‖compound B‖² times the squared norm of the M-compound at w:
‖compound(B·M) w‖² ≤ ‖compound B‖²·‖compound M w‖². This relates the Rayleigh quotients of the
compound Gram operators C_{n+1} (from B·M) and C_n (from M). Via
toEuclideanLin_compoundMatrix_mul + the per-vector operator-norm step.
Lemma 2 (Rayleigh identity). The Rayleigh quotient of the compound Gram operator
C_n = adjoint(compound M) ∘ₗ compound M at w equals ‖compound M w‖².
Lemma 2 (top-eigenvalue ceiling). The Rayleigh quotient of the compound Gram operator is
bounded by ‖compound M‖²·‖w‖²; equivalently the top eigenvalue μ₀ of
C_n = adjoint(compound M) ∘ₗ compound M is ‖compound M‖² (the squared operator norm of the
compound = top eigenvalue of AᵀA).
Pure-real algebraic kernel of the deficit bound: from BM ≤ CB·r and mu ≤ CBi·BM (with all
nonnegative) one gets mu² − r² ≤ (1 − 1/(CB·CBi)²)·mu².
Lemma 3 — the rank-1 exterior Rayleigh-deficit bound.
For invertible B and a unit vector v' that achieves the operator norm of the compound
compound (B·M) (so ‖compound(B·M) v'‖ = ‖compound(B·M)‖, i.e. v' is a top right-singular
vector / dominant eigenvector of C_{n+1}), the Rayleigh deficit of the operator
C_n = adjoint(compound M) ∘ₗ compound M at v' against its top value μ₀ = ‖compound M‖²
obeys μ₀ − ⟨C_n v', v'⟩ ≤ (1 − 1/κ²)·μ₀ with κ = ‖compound B‖·‖(compound B)⁻¹‖.
This is the deficit-side input to sin_sq_le_rayleigh_deficit_div_gap (with
ε := μ₀ − ⟨C_n v', v'⟩, μ₀ := ‖compound M‖²). The v'-achieves-the-op-norm hypothesis encodes
that v' is the top eigenvector of C_{n+1}; its existence is the caller's responsibility.
The off-diagonal residual estimate and the perturbed Gram ceiling #
The refined Davis–Kahan sin-Θ estimate in off-diagonal/residual form
(offdiag_sin_le_residual_div_gap in Oseledets.Lyapunov.OseledetsLimit) needs two
cocycle-specific inputs:
- the off-diagonal residual numerator
‖Cₙ₊₁ v₀ − ⟪Cₙ₊₁ v₀, v₀⟫ v₀‖ ≤ τ₀ τ₁ ‖H‖², whereCₙ₊₁ = adjoint G' ∘ₗ G',G' = H ∘ₗ G, andv₀is the top eigenvector ofCₙ = adjoint G ∘ₗ G(offdiag_residual_norm_le); - the
ν-ceiling∀ z ⊥ v₀, ⟪Cₙ₊₁ z, z⟫ ≤ (μ₁ ‖H‖²) ‖z‖²transported from theCₙ-ceiling∀ z ⊥ v₀, ⟪Cₙ z, z⟫ ≤ μ₁ ‖z‖²(perturbed_gram_ceiling).
Both are abstract operator facts (no compound/exterior structure); the cocycle specialisation in
standard coordinates (where G = toEuclideanLin (compoundMatrix k ·)) follows by
toEuclideanLin_compoundMatrix_mul (functoriality G' = H ∘ₗ G) and the per-vector operator-norm
bound norm_toEuclideanLin_apply_le. These pieces feed the band-projector increment bound
together with the back-transport norm_proj_sub_le_wedge.
The off-diagonal residual is orthogonal to v₀. For a unit v₀, the residual
C v₀ − ⟪C v₀, v₀⟫ v₀ = (I − P) C v₀ is orthogonal to v₀.
Rayleigh of the Gram operator is the squared norm: ⟪(adjoint G ∘ₗ G) v, v⟫ = ‖G v‖²
(abstract form; rayleigh_compound_eq_norm_sq is the compound-matrix specialisation).
The off-diagonal inner product reduction:
⟪(adjoint G' ∘ₗ G') v₀, z⟫ = ⟪G' v₀, G' z⟫
(plain adjoint move; for z ⊥ v₀ this is the off-diagonal block of Cₙ₊₁).
The off-diagonal residual norm estimate.
For the perturbed Gram operator Cₙ₊₁ = adjoint G' ∘ₗ G' with G' = H ∘ₗ G (functoriality) and
v₀ the top unit eigenvector of Cₙ = adjoint G ∘ₗ G, the off-diagonal residual
Cₙ₊₁ v₀ − ⟪Cₙ₊₁ v₀, v₀⟫ v₀ has norm at most τ₀ · τ₁ · ‖H‖², where τ₀ = ‖G v₀‖ (the top
singular value of G) and τ₁ is the second-singular-value ceiling on v₀^⊥
(hperp : ∀ z ⊥ v₀, ‖z‖ ≤ 1 → ‖G z‖ ≤ τ₁).
Proof: the residual res ⊥ v₀; ‖res‖² = ⟪res, res⟫ = ⟪Cₙ₊₁ v₀, res⟫ (since res ⊥ v₀)
= ⟪H G v₀, H G res⟫ ≤ ‖H‖²‖G v₀‖‖G res‖ ≤ ‖H‖² τ₀ τ₁ ‖res‖ by Cauchy–Schwarz, the per-vector
operator-norm bound on H, htop, and hperp applied to the unit normalisation of res. Dividing
by ‖res‖ gives the bound.
The ν-ceiling for the perturbed Gram operator.
From a Rayleigh ceiling ∀ z ⊥ v₀, ⟪Cₙ z, z⟫ ≤ μ₁ ‖z‖² on the unperturbed Gram operator
Cₙ = adjoint G ∘ₗ G, the perturbed operator Cₙ₊₁ = adjoint G' ∘ₗ G' with G' = H ∘ₗ G obeys
the amplified ceiling ∀ z ⊥ v₀, ⟪Cₙ₊₁ z, z⟫ ≤ (μ₁ ‖H‖²) ‖z‖². Proof: ⟪Cₙ₊₁ z, z⟫ = ‖H G z‖² ≤ ‖H‖² ‖G z‖² = ‖H‖² ⟪Cₙ z, z⟫ ≤ ‖H‖² μ₁ ‖z‖². This supplies the ν := μ₁ ‖H‖² ceiling consumed
by offdiag_sin_le_residual_div_gap.
The cocycle specialisation in compound-matrix coordinates #
Specialising offdiag_residual_norm_le / perturbed_gram_ceiling to the cocycle Gram operators
Cₙ = adjoint Gₙ ∘ₗ Gₙ, Gₙ = toEuclideanLin (compoundMatrix k Mₙ), with the one-step left factor
B = A(Tⁿx) (so Mₙ₊₁ = B · Mₙ and Gₙ₊₁ = (compound B) ∘ Gₙ by
toEuclideanLin_compoundMatrix_mul). The SVD ceiling hperp of the abstract lemma is discharged
from a μ₁-ceiling on Cₙ via rayleigh_compound_eq_norm_sq:
‖Gₙ z‖² = ⟪Cₙ z, z⟫ ≤ μ₁ ‖z‖² ≤ μ₁ for ‖z‖ ≤ 1, hence ‖Gₙ z‖ ≤ √μ₁ =: τ₁.
The off-diagonal residual estimate for the compound Gram operators.
With Gₙ = toEuclideanLin (compoundMatrix k M), Cₙ = adjoint Gₙ ∘ₗ Gₙ, the one-step left factor
B, and Cₙ₊₁ = adjoint Gₙ₊₁ ∘ₗ Gₙ₊₁ for Gₙ₊₁ = toEuclideanLin (compoundMatrix k (B * M)): if
v₀ is a unit vector achieving the compound operator norm ‖Gₙ v₀‖ = ‖compoundMatrix k M‖ = τ₀
(the top right-singular vector of Gₙ, i.e. the top eigenvector of Cₙ) with a μ₁-Rayleigh
ceiling on v₀^⊥, then the off-diagonal residual obeys
‖Cₙ₊₁ v₀ − ⟪Cₙ₊₁ v₀, v₀⟫ v₀‖ ≤ ‖compoundMatrix k M‖ · √μ₁ · ‖compoundMatrix k B‖².
(τ₀ = ‖compoundMatrix k M‖, τ₁ = √μ₁, ‖H‖ = ‖compoundMatrix k B‖.)
The ν-ceiling for the perturbed compound Gram operator.
From a μ₁-Rayleigh ceiling on Cₙ = adjoint Gₙ ∘ₗ Gₙ over v₀^⊥, the perturbed compound Gram
operator Cₙ₊₁ = adjoint Gₙ₊₁ ∘ₗ Gₙ₊₁ (with Gₙ₊₁ = toEuclideanLin (compoundMatrix k (B * M)))
obeys the amplified ceiling ∀ z ⊥ v₀, ⟪Cₙ₊₁ z, z⟫ ≤ (μ₁ ‖compoundMatrix k B‖²) ‖z‖². This is the
ν := μ₁ ‖H‖² ceiling consumed by offdiag_sin_le_residual_div_gap.
The Plücker bridge #
For a symmetric PD map f with orthonormal eigenbasis u and eigenvalues lam, the compound
⋀^k f, conjugated through the eigenbasis wedge trivialization onbTriv u, is a diagonal
Euclidean operator: it scales basisFun i by the subset product ∏_{a ∈ Sᵢ} lam a. The top set
{0,…,k-1} (maximal by prod_le_prod_top for antitone weights) gives the top eigenvector
v₀ = basisFun i₀ with eigenvalue μ₀, and every other weight is ≤ μ₁ (the second-eigenvalue
ceiling). The bridge is completed by the det-Gram identity for the Plücker (wedge) inner
product.
The Plücker (wedge) inner product is the cross-Gram determinant. For two families
v, w : Fin k → E, the L2 inner product of their Hodge-trivialized wedges equals the determinant
of the cross-Gram matrix ⟪v j, w i⟫. With orthonormal frames this is the wedge-sine identity
⟪w_E, w_E'⟫ = det(UᵀV) feeding the Frobenius back-transport norm_proj_sub_le_wedge.
The j-th column of a d×k matrix, viewed as a vector in EuclideanSpace ℝ (Fin d). The
columns of the band-projector frames U_top (bandProjector_indicator_eq_frame) are the
orthonormal top-block eigenvectors; their wedge is the Plücker top eigenvector.
Equations
- Oseledets.ExteriorNorm.colE U j = (EuclideanSpace.equiv (Fin d) ℝ).symm fun (a : Fin d) => U a j
Instances For
The Plücker frame ↔ wedge determinant bridge (matrix form). For two d×k
column-frames U, V, the determinant of the cross-Gram Uᵀ V equals the L2 inner product of the
Hodge-trivialized wedges of their columns. This is the hdet : det(UᵀV) = ⟪vt, v₀⟫ plumbing fact
consumed by Oseledets.norm_bandProjector_succ_sub_le, with v₀ = wedge of U-columns (the Plücker
top eigenvector of Cₙ) and vt = wedge of V-columns (the perturbed top eigenvector of Cₙ₊₁).
Since the band-projector frames U_top have orthonormal eigenvector columns
(bandProjector_indicator_eq_frame) which are the same eigenbasis the Plücker eigenpair
(plucker_eigenpair_ceiling_standard, applied with u = eigenvectorBasis) is built from, the
two wedges are exactly these Hodge-trivialized column wedges, and this identity supplies hdet.
Abstract diagonal Euclidean operators: eigenpair and second-eigenvalue ceiling #
The Plücker eigenpair and second-eigenvalue ceiling #
The Plücker bridge for a symmetric map. Let f be symmetric with orthonormal
eigenbasis u : OrthonormalBasis (Fin n) and antitone nonnegative eigenvalues
lam : ℕ → ℝ (f (u i) = lam i • u i). At a genuine gap lam k < lam (k-1) (with 1 ≤ k ≤ n),
the conjugated compound C = ⋀^k f (through the eigenbasis wedge trivialization onbTriv u) is a
symmetric operator with:
- top eigenpair:
C v₀ = μ₀ • v₀, wherev₀ = basisFun i₀is the Plücker image of the top-keigenframe andμ₀ = ∏_{i<k} lam i; - second-eigenvalue ceiling:
∀ w ⊥ v₀, ⟪C w, w⟫ ≤ μ₁ ‖w‖²withμ₁ = (∏_{i<k-1} lam i)·lam k; - the gap:
μ₁ < μ₀.
This lands in exactly the shape consumed by sin_sq_le_rayleigh_deficit_div_gap (hC, hv₀,
hev, hgap, hμ₁).
Witness-exposing Plücker bridge (eigenbasis coords). Same as plucker_eigenpair_ceiling,
but with the top eigenvector index i₀ produced explicitly as wIndexEquiv u k topSet (where
topSet is the top-k prefix subset), and with the extra identity pinning the standard basis
vector basisFun i₀ to the explicit Hodge-trivialized wedge
onbTriv u k (e_{u₀} ∧ ⋯ ∧ e_{u_{k-1}}) of the top-k eigenframe. This is the variant
plucker_eigenpair_ceiling_standard' transports to standard coordinates to expose the
band-projector frame wedge.
The reconciliation bridge: transporting the Plücker eigenpair into standard coordinates #
plucker_eigenpair_ceiling produces the top eigenpair and second-eigenvalue ceiling of the
conjugated compound conjExteriorMap k (onbTriv u) (onbTriv u) f in the eigenbasis wedge
trivialization (u = an orthonormal eigenbasis of the symmetric f). The Rayleigh-deficit input
rayleigh_deficit_le lives in the standard trivialization, where the conjugated compound is
toEuclideanLin (compoundMatrix k ·) (the compound matrix). These are the same abstract operator
⋀^k f viewed through two isometric o.n.-basis wedge trivializations, hence unitarily equivalent by
the orthogonal change-of-coordinates onbChange. Since an isometry preserves the inner product, the
Rayleigh quotient is trivialization-independent; this lets sin_sq_le_rayleigh_deficit_div_gap be
applied in eigenbasis coordinates with the deficit supplied from standard coordinates.
Transport of a top-eigenpair + second-eigenvalue ceiling across the change of o.n.-wedge
trivialization. Given the top eigenpair (hev) and the μ₁-ceiling on the orthogonal complement
(hceil) of the conjugated compound in the b'-trivialization (b' = the eigenbasis), the same
data transports — via the orthogonal W = onbChange b b' k — to the b-trivialization (b = the
standard basis): the eigenvector is v₀ = W⁻¹ (basisFun i₀), the eigenvalue/gap are unchanged, and
the Rayleigh ceiling holds verbatim on v₀ᗮ. This is the abstract (matrix-free) reconciliation core
that feeds sin_sq_le_rayleigh_deficit_div_gap once conjExteriorMap (onbTriv b) f is identified
with the standard compound.
The Plücker eigenpair in standard (compound-matrix) coordinates #
The matrix-level packaging plucker_eigenpair_ceiling_standard transports
plucker_eigenpair_ceiling through the orthogonal change-of-trivialization onbChange
(via eigenpair_ceiling_transport) into the standard wedge trivialization
onbTriv (EuclideanSpace.basisFun (Fin d) ℝ), where the compound bridge
conjExteriorMap_eq_toEuclideanLin_compound identifies the conjugated compound of
toEuclideanLin Q with toEuclideanLin (compoundMatrix k Q) — exactly the operator consumed by
the off-diagonal residual lemmas norm_offdiag_residual_compound_le /
perturbed_compound_gram_ceiling.
A single declaration combining plucker ∘ transport ∘ matrix-identification times out even at
maxHeartbeats 1600000. The fix is to split the heavy matrix-identification step into an
isolated scoped lemma (conjExteriorMap_basisFun_toEuclideanLin_eq_compound below — a thin alias
of the compound bridge, kept separate so its ⋀^k finrank elaboration cost is contained) and to
keep the transport/assembly in its own scoped declaration.
(A) — the isolated matrix-identification step. Through the standard orthonormal-wedge
trivialization (onbTriv (EuclideanSpace.basisFun (Fin d) ℝ)), the conjugated compound of
toEuclideanLin M is toEuclideanLin (compoundMatrix k M). This is a thin re-export of
conjExteriorMap_eq_toEuclideanLin_compound, isolated in its own scoped declaration so
that the (heavy) ⋀^k finrank-indexed elaboration is paid here exactly once, keeping the
assembled plucker_eigenpair_ceiling_standard under budget.
(B) — plucker_eigenpair_ceiling_standard. The Plücker eigenpair + second-eigenvalue
ceiling in standard compound-matrix coordinates. For a symmetric PSD f = toEuclideanLin Q with
orthonormal eigenbasis u and antitone nonnegative eigenvalues lam, at a genuine gap
lam k < lam (k-1), the operator toEuclideanLin (compoundMatrix k Q) (= ⋀^k Q in the standard
trivialization) has:
- top eigenpair: a unit vector
v₀withtoEuclideanLin (compoundMatrix k Q) v₀ = μ₀ • v₀,μ₀ = ∏_{i<k} lam i; - the gap:
μ₁ < μ₀withμ₁ = (∏_{i<k-1} lam i)·lam k; - second-eigenvalue ceiling:
∀ w ⊥ v₀, ⟪(toEuclideanLin (compoundMatrix k Q)) w, w⟫ ≤ μ₁‖w‖².
Assembled from plucker_eigenpair_ceiling (eigenbasis-wedge coords) → eigenpair_ceiling_transport
(onbChange to standard basisFun coords) → conjExteriorMap_basisFun_toEuclideanLin_eq_compound
(matrix identification, isolated in (A)). This is the top spectral data of Cₙ = ⋀^k Qₙ that
norm_offdiag_residual_compound_le / perturbed_compound_gram_ceiling consume.
(B') — witness-exposing plucker_eigenpair_ceiling_standard. Same spectral data as
plucker_eigenpair_ceiling_standard, but with the top eigenvector produced explicitly as the
standard-trivialization wedge w₀ = onbTriv basisFun k (e_{u₀} ∧ ⋯ ∧ e_{u_{k-1}}) of the top-k
eigenframe of u — exactly the Plücker top eigenvector that the band-projector frame wedge equals.
This is the variant whose witness can be plugged into det_transpose_mul_eq_inner_onbTriv to
discharge the hdet hypothesis of Oseledets.norm_bandProjector_succ_sub_le.
(C) — the Plücker frame ↔ wedge determinant bridge through the standard trivialization.
The hdet plumbing fact for Oseledets.norm_bandProjector_succ_sub_le, expressed through the same
trivialization onbTriv basisFun in which plucker_eigenpair_ceiling_standard' produces its top
eigenvectors: det(UᵀV) = ⟪onbTriv basisFun (⋀ V-cols), onbTriv basisFun (⋀ U-cols)⟫. Together with
plucker_eigenpair_ceiling_standard' (whose v₀/vt ARE these column wedges), this discharges the
hdet hypothesis with v₀ = U-column wedge, vt = V-column wedge.