The band spectral projector #
The band spectral projectors bandProjector A T χ n x = cfc χ (qpow A T n x) of the candidate
Oseledets matrices qpow, together with their self-adjoint / idempotent algebra, the sorted Gram
eigenbasis and top frame, and the Cauchy / summability and abstract sin-Θ machinery used to extract
limiting spectral projectors from the candidates.
Main definitions #
Oseledets.bandProjector— the band spectral projector ofqpow A T n xcut at a thresholdχ.Oseledets.sortedGramEigenbasis,Oseledets.sortedTopFrame— the sorted Gram eigenbasis and the orthonormal frame spanning the top eigenvalue-block.
Main results #
Oseledets.bandProjector_isSelfAdjoint,Oseledets.bandProjector_mul_self,Oseledets.bandProjector_rank— the band-projector algebra.Oseledets.norm_cfc_le_of_forall_eigenvalue_abs_le— the spectral-block operator-norm bound.Oseledets.exists_tendsto_cfc_of_summable— CFC convergence from summable increments.Oseledets.sin_sq_le_rayleigh_deficit_div_gap,Oseledets.offdiag_sin_le_residual_div_gap— the abstract Rayleigh-deficit / sin-Θ core.
The band spectral projector and its basic algebra #
The spectral projectors of the Oseledets matrix limit are obtained as limits of band spectral
projectors of the candidate matrices qpow A T n x = (Qₙ)^{1/(2n)}: cut the spectrum at a
continuous threshold function χ via the continuous functional calculus. For a χ that equals the
0/1 indicator of a spectral gap on the (finite) spectrum, cfc χ (qpow) is the orthogonal
projector onto the top eigenvalue-block. This subsection records the projector and its self-adjoint
/ idempotent algebra; the gap hypothesis discharging idempotence is supplied by the root-test layer
below.
The band spectral projector of qpow A T n x cut at a continuous threshold function
χ: bandProjector A T χ n x = cfc χ (qpow A T n x). For a χ that equals the 0/1 indicator of
a spectral gap on the (finite) spectrum it is the orthogonal projector onto the top
eigenvalue-block; the projector identity is provided conditionally below.
Equations
- Oseledets.bandProjector A T χ n x = cfc χ (Oseledets.qpow A T n x)
Instances For
The band spectral projector is self-adjoint (a CFC of a real-valued function is always self-adjoint).
If the cutoff χ is idempotent on the spectrum of qpow (i.e. χ = χ² there — true
for a 0/1 indicator separated from the spectrum by a gap), the band projector is idempotent: a
genuine orthogonal projector. Conditional; the gap hypothesis that supplies hidem is discharged by
the root-test layer below.
The band projector is the top-block eigenprojector #
For a cutoff χ equal on the (finite) spectrum of qpow A T n x to the 0/1 indicator of
(c, ∞), the band projector bandProjector A T χ n x = cfc χ (qpow…) is a genuine orthogonal
projector (self-adjoint idempotent) whose rank equals the number of eigenvalues of qpow
strictly above c — i.e. the dimension of the top eigenvalue-block. The explicit Hermitian-CFC
triple-product formula cfc χ A = U · diag(χ ∘ eigenvalues) · Uᴴ makes the projector concrete;
the rank is the count of nonzero diagonal entries, and a {0,1}-valued χ selects exactly the
eigenvalues above the cut.
When χ equals the 0/1 indicator of (c, ∞) on the spectrum of qpow, the band
projector is idempotent (a genuine orthogonal projector). Specialization of bandProjector_mul_self
to the indicator cutoff, whose continuity hypothesis is discharged because the spectrum is finite
and the indicator is 0/1-valued (hence χ² = χ on it).
The explicit Hermitian-CFC triple product: for a Hermitian matrix M, cfc χ M equals the
unitary conjugate of the diagonal matrix of χ applied to the eigenvalues,
U · diag(RCLike.ofReal ∘ χ ∘ eigenvalues) · Uᴴ. Matrix analogue of the spectral step
hA.cfc χ = U · diag(ofReal ∘ χ ∘ eig) · star U.
Rank of the band projector. The rank of bandProjector A T χ n x = cfc χ (qpow…)
is the number of eigenvalues i of qpow A T n x with χ (eigenvalues i) ≠ 0. Computed from the
explicit Hermitian-CFC triple product U · diag(χ ∘ eig) · Uᴴ: conjugation by the (invertible)
eigenvector unitary preserves rank, and the rank of the diagonal is the count of nonzero entries.
Frame form: the band projector is U_top · U_topᵀ #
The Frobenius back-transport ExteriorNorm.norm_proj_sub_le_wedge consumes the band projector in
the
shape P = U Uᵀ with Uᵀ U = 1 (orthonormal columns). The 0/1 indicator cutoff selects exactly
the eigenvectors of qpow with eigenvalue > c; through the explicit Hermitian-CFC triple product
cfc χ M = U · diag(χ ∘ eig) · Uᴴ (cfc_eq_eigenvectorUnitary_conj), the band projector equals
U_top · U_topᵀ, where U_top is the column-submatrix of the eigenvector unitary selecting the
columns above the cut. The selected columns are orthonormal (U_topᵀ U_top = 1).
Diag-selection. For a real matrix U and the 0/1 indicator of (c, ∞) precomposed with a
scalar e : Fin d → ℝ, conjugating the indicator diagonal by U selects the columns of U whose
e-value exceeds c: U · diag(𝟙_{(c,∞)} ∘ e) · Uᵀ = U_S · U_Sᵀ, where U_S is the
column-submatrix of U on S = {i | c < e i}.
Orthonormal columns of the selected submatrix. If U has orthonormal columns
(Uᵀ U = 1, e.g. an eigenvector unitary), then any column-subselection of U still has orthonormal
columns: U_Sᵀ U_S = 1. (U_S = U.submatrix id Subtype.val over a subtype of column indices.)
CFC indicator = U_top · U_topᵀ. For a Hermitian real matrix M with eigenvector unitary
U and eigenvalues eig, the band projector cut by the 0/1 indicator of (c, ∞) is
U_top · U_topᵀ, where U_top is the column-submatrix of U selecting the eigenvectors with
eigenvalue > c. Combines cfc_eq_eigenvectorUnitary_conj (the triple product
U · diag(χ ∘ eig) · Uᴴ) with diag_indicator_conj_eq_submatrix.
The band-projector frame extraction. The band projector of qpow cut
by the 0/1 indicator of (c, ∞) is U_top · U_topᵀ, with U_top the column-submatrix of the
eigenvector unitary of qpow A T n x selecting the eigenvectors with eigenvalue > c, and the
selected columns are orthonormal (U_topᵀ U_top = 1). This is the P = U Uᵀ input consumed by the
Frobenius back-transport ExteriorNorm.norm_proj_sub_le_wedge.
Sorted frame: the band projector is the SORTED top-k gram eigenframe projector #
The Plücker eigenpair ExteriorNorm.plucker_eigenpair_ceiling_standard' and the det-Gram bridge
ExteriorNorm.det_transpose_mul_eq_inner_onbTriv both speak of the sorted gram eigenbasis: the
top eigenvector wedge is onbTriv basisFun (⋀ {u₀, …, u_{k-1}}) of the orthonormal eigenframe u
with antitone eigenvalues lam = σ². The bandProjector_indicator_eq_frame expresses
the band projector through qpow's unsorted eigenvector unitary; this subsection reconciles the
two by showing the band projector equals W Wᵀ, where W is the d×k matrix whose columns are the
sorted top-k gram eigenvectors. Both are the orthogonal projector onto the same eigenvalue-> c
subspace; the reconciliation is via the elementary "self-adjoint idempotent of trace k and range
fixing W is W Wᵀ" device (trace-zero symmetric idempotent vanishes).
CFC acts diagonally on the matrix eigenbasis. For a Hermitian real matrix M with
eigenvector basis eigenvectorBasis and eigenvalues eigenvalues, cfc g M sends the j-th
eigenvector to g (eigenvalues j) times itself: cfc g M *ᵥ (eigenvectorBasis j) = g (eigenvalues j) • eigenvectorBasis j. The matrix-level spectral action, derived from the explicit
triple product cfc g M = U · diag(g ∘ eig) · Uᴴ (cfc_eq_eigenvectorUnitary_conj).
CFC acts diagonally on the matrix eigenbasis (Euclidean-linear form). The EuclideanSpace
analogue of cfc_mulVec_eigenvectorBasis: toEuclideanLin (cfc g M) sends the j-th eigenvector
to
g (eigenvalues j) times itself.
The spectral operator-norm bound. For a Hermitian matrix M and a function
g, if |g (eigenvalue i)| ≤ c for every eigenvalue (and 0 ≤ c), then the L2 operator norm of
cfc g M is at most c. This is the analytic core of the spectral-block approximation: applied
with
g = (· − v ·) (the deviation between the identity and the block-value step function), it bounds
the
distance between qpow and its block-approximant by the maximal eigenvalue deviation.
Proof: in the orthonormal eigenbasis b of M, cfc g M acts diagonally
(toEuclideanLin_cfc_eigenvectorBasis), so ⟪b i, (cfc g M) v⟫ = g (eig i) · ⟪b i, v⟫; Parseval
(OrthonormalBasis.sum_sq_norm_inner_right) then gives
‖(cfc g M) v‖² = ∑ |g(eig i)|² |⟪b i,v⟫|² ≤ c² ∑ |⟪b i,v⟫|² = c² ‖v‖².
Trace of the indicator band projector = number of eigenvalues above the cut. For a Hermitian
real matrix M, the trace of cfc (𝟙_{(c,∞)}) M is the count of eigenvalues > c. The
0/1-valued
cutoff makes the conjugated-diagonal trace a count. (For a self-adjoint idempotent this is its
rank.)
A symmetric idempotent of trace 0 vanishes. Over ℝ, a matrix E with Eᵀ = E and
E * E = E and tr E = 0 is the zero matrix: tr(Eᴴ E) = tr(E²) = tr E = 0, and the squared
Frobenius norm tr(Eᴴ E) = ∑ Eᵢⱼ² is zero only for E = 0. The kernel that turns "same range,
same trace" into a projector identity.
The band projector via the cfc on the Gram matrix. Since qpow = cfc (·^{1/(2n)}) (gram)
and cfc composes, bandProjector A T 𝟙_{(c,∞)} n x = cfc (𝟙_{(c,∞)} ∘ (·^{1/(2n)})) (gram A T n x).
This unfolds the band projector onto the gram spectral data, where the sorted eigenbasis lives.
The sorted Gram eigenbasis. The orthonormal eigenbasis of gram A T n x, reindexed by
Fin (card (Fin d)) so that sortedGramEigenbasis i has eigenvalue eigenvalues₀ i = σᵢ²
(antitone, descending). This is exactly the u consumed by
ExteriorNorm.plucker_eigenpair_ceiling_standard' (with lam = σ²).
Equations
Instances For
The sorted Gram eigenbasis diagonalizes toEuclideanLin (gram) with the antitone
eigenvalues
eigenvalues₀: toEuclideanLin (gram) (sortedGramEigenbasis i) = eigenvalues₀ i • sortedGramEigenbasis i.
The eigenpair hypothesis hf of ExteriorNorm.plucker_eigenpair_ceiling_standard'.
The 1/(2n)-power of the sorted Gram eigenvalue is the sorted qpow eigenvalue:
(eigenvalues₀(gram) i)^{1/(2n)} = eigenvalues₀(qpow) i. The monotone-CFC bridge identifying the
gram cut with the qpow cut.
The sorted top-k Gram eigenframe. The d×k matrix whose j-th column is the j-th
sorted
Gram eigenvector sortedGramEigenbasis ⟨j, …⟩. Its column wedge is the Plücker top eigenvector
w₀ = onbTriv basisFun (⋀ {u₀, …, u_{k-1}}) of ExteriorNorm.plucker_eigenpair_ceiling_standard',
and it is the W of the band-projector frame identity bandProjector = W Wᵀ.
Equations
- Oseledets.sortedTopFrame A T n x hk = Matrix.of fun (a : Fin d) (j : Fin k) => ((Oseledets.sortedGramEigenbasis A T n x) ⟨↑j, ⋯⟩).ofLp a
Instances For
The j-th column of sortedTopFrame (as a Euclidean vector) is the j-th sorted Gram
eigenvector. This is the identification that makes ExteriorNorm.det_transpose_mul_eq_inner_onbTriv
and ExteriorNorm.plucker_eigenpair_ceiling_standard' share the same wedge.
The sorted top-k Gram eigenframe has orthonormal columns: Wᵀ W = 1.
The band projector fixes the sorted top-k Gram eigenframe. If each of the top-k sorted
qpow eigenvalues exceeds the cut c, then bandProjector * W = W, i.e. the band projector acts
as
the identity on each top-k sorted Gram eigenvector. (Each column is a qpow-eigenvector with
eigenvalue > c, where the 0/1 cutoff is 1.)
The band projector is the SORTED top-k Gram eigenframe projector. For a
cut
c such that exactly k of the qpow eigenvalues exceed c (hcount) and the top-k sorted
ones
all exceed it (htop), the band projector equals W Wᵀ with Wᵀ W = 1, where W = sortedTopFrame
has the sorted top-k Gram eigenvectors as columns. The unsorted↔sorted eigenframe reconciliation:
both bandProjector (the cfc-indicator eigenvalue-> c projector of qpow) and W Wᵀ (the
sorted
top-k Gram eigenspace projector) are the orthogonal projector onto the same subspace. Proof:
the
difference E = bandProjector − W Wᵀ is a symmetric idempotent (bandProjector fixes the columns
of
W — bandProjector_mul_sortedTopFrame) of trace k − k = 0, hence vanishes
(eq_zero_of_transpose_eq_of_mul_self_of_trace_zero). The frame W and its column wedge are
exactly
the data consumed by ExteriorNorm.plucker_eigenpair_ceiling_standard' and
ExteriorNorm.det_transpose_mul_eq_inner_onbTriv.
Cauchy packaging — summable increments give a convergent (band-projector) sequence #
The hard mathematical content (the gapped band-projector-Cauchy estimate and its summability)
produces
the summability of the consecutive-norm increments of the band projectors. Once that is in hand,
convergence is pure soft analysis: matrices form a finite-dimensional, hence complete, normed space,
so a sequence with summable increments is Cauchy and converges. We package this abstractly (no
dynamics) so it is upstreamable and reusable for any matrix sequence — and keep a cfc χ (H n)
specialization that plugs directly into bandProjector.
A matrix sequence whose consecutive-difference norms ‖f (n+1) - f n‖ are summable is Cauchy
(matrices over ℝ are a finite-dimensional, hence complete, normed space). General soft-analysis
fact, independent of the continuous functional calculus.
Packaging. A sequence of band-projector-shaped matrices cfc χ (H n) whose
consecutive-norm increments are summable is Cauchy. The mathematical content lives in supplying the
summability (the gapped-Cauchy estimate and root test); this is the soft-analysis packaging.
Packaging. A band-projector-shaped sequence cfc χ (H n) with summable
consecutive-norm increments converges (matrices are a complete space). The limit is the candidate
Oseledets spectral projector.
The rank-1 Rayleigh-gap sin-Θ core #
The irreducible analytic kernel of the gapped band-projector Cauchy estimate. It is an
elementary (Parseval + one scalar inequality) replacement for an abstract Davis–Kahan sin-Θ
theorem, which Mathlib lacks entirely. Stated abstractly for a symmetric operator on any real inner
product space (upstreamable, no dynamics): if a unit vector v' nearly maximizes the Rayleigh
quotient of C, it is close to the top eigenvector v₀, with the squared sine of the angle
controlled by the Rayleigh deficit divided by the spectral gap. The cocycle consumer takes
C = ⋀^k Qₙ and v' the top eigenvector of ⋀^k Qₙ₊₁, where the deficit is the one-step
distortion.
The rank-1 Rayleigh-gap sin-Θ bound. For a symmetric operator C with a top unit
eigenvector v₀ of eigenvalue μ₀, whose v₀-orthogonal complement has Rayleigh quotient bounded
above by a strictly smaller μ₁, any unit vector v' whose Rayleigh quotient is within ε of μ₀
makes a small angle with v₀: the squared sine ‖v' - ⟪v', v₀⟫ v₀‖² is at most ε / (μ₀ - μ₁).
The tempered one-step factor #
The relative-gap projector-increment bound carries a one-step distortion factor
‖A(Tⁿx)‖·‖A(Tⁿx)⁻¹‖. For the increments to be summable a.e. this factor must be
tempered: its normalized logarithm vanishes a.e. This is the orbital-tail consequence of
Birkhoff's theorem (ae_tendsto_orbit_div_atTop_zero: n⁻¹·g(Tⁿx) → 0 a.e. for integrable g)
applied to the integrable signed log-norms log‖A·‖ and log‖A·⁻¹‖ (integrable_logNorm_cocycle
at n = 1, where cocycle A T 1 = A).
The tempered one-step factor. The normalized log-norm of the one-step generator
along the orbit vanishes a.e.: (1/n)·log‖A(Tⁿx)‖ → 0.
The tempered one-step factor (inverse). The normalized log-norm of the inverse of
the one-step generator along the orbit vanishes a.e.: (1/n)·log‖A(Tⁿx)⁻¹‖ → 0.
Compound operator-norm upper bound ‖compound k B‖ ≤ ‖B‖^k. From the singular-value
product ∏_{i<k} σᵢ = ‖compound k B‖ (prod_singularValues_eq_l2_opNorm_compound) and the
per-index
ceiling σᵢ ≤ ‖B‖ (sigma_le_opNorm).
Compound operator-norm lower bound (‖B⁻¹‖⁻¹)^k ≤ ‖compound k B‖, for invertible B and
k ≤ d. From the singular-value product and the per-index floor ‖B⁻¹‖⁻¹ ≤ σᵢ
(inv_opNorm_inv_le_sigma).
The tempered compound factor. The normalized log compound operator norm along the
orbit vanishes a.e.: (1/n)·log‖compound k (A(Tⁿx))‖ → 0. Squeezed between
-k·(1/n)log‖A(Tⁿx)⁻¹‖ → 0 and k·(1/n)log‖A(Tⁿx)‖ → 0 via the compound-norm sandwich
(norm_compound_le, norm_inv_pow_le_norm_compound) and the tempered one-step factors
(tendsto_logNorm_orbit_div_atTop_zero and its inverse). This makes κ(⋀ᵏB) = ‖compound k B‖· ‖compound k B⁻¹‖ subexponential, so it contributes 0 to the root-test log-limit.
Refined Davis–Kahan off-diagonal sin-Θ #
The Rayleigh-DEFICIT bound sin_sq_le_rayleigh_deficit_div_gap is true but the WRONG tool for the
gapped band-projector summability: feeding it the only provable deficit ε ≤ (1−1/κ²)μ₀ yields
sin²θ ≤ (1−1/κ²)/(1−r²), which is NOT summable along the orbit (the one-step κ is tempered with
positive mean, so 1−1/κ² does not decay), and the route is structurally circular (ε ≈ μ₀ sin²θ).
The summable estimate needs the refined Davis–Kahan sin-Θ in off-diagonal/residual form: the
numerator is the off-diagonal block C v₀ − ⟪C v₀, v₀⟫ v₀, which (for the cocycle compound) carries
the extra σₖ/σₖ₋₁ factor the deficit route loses.
Refined off-diagonal rank-1 sin-Θ. For a perturbed operator C
with top unit eigenvector vt (eigenvalue μ₀), an unperturbed top eigenline v₀, and a Rayleigh
ceiling ν < μ₀ of C on v₀^⊥, the sine of the angle between vt and v₀ is bounded by the
off-diagonal residual ‖C v₀ − ⟪C v₀, v₀⟫ v₀‖ over the gap μ₀ − ν. Elementary (Rayleigh +
Cauchy–Schwarz + |⟪vt,v₀⟫| ≤ 1); no symmetry, no functional calculus. This replaces the
deficit-form sin_sq_le_rayleigh_deficit_div_gap as the load-bearing sin-Θ core.
Summability by the root test (engine) #
The corrected per-step bound has the shape ‖Pₙ₊₁ − Pₙ‖ ≤ √(2k)·κ(⋀ᵏB)²·rₙ with
rₙ = σₖ(Mₙ)/σₖ₋₁(Mₙ) geometric ((1/n)log rₙ → λₖ−λₖ₋₁ < 0) and κ(⋀ᵏB)² subexponential
((1/n)log → 0). Their product is summable by the root test. These are the scalar engines.
Root test (log form). For an eventually-positive a whose normalized log tends to a
negative limit L, a is summable. The engine that turns the geometric×subexponential per-step
projector bound into summability (take L = λₖ − λₖ₋₁ < 0).