FLYWHEEL

Formalized Linear Algebra in Lean 4

Machine-checked matrix analysis on Mathlib: the SVD, Courant–Fischer, Weyl and Thompson interlacing, Eckart–Young (with uniqueness under a gap), Kronecker (Van Loan–Pitsianis) approximation, Davis–Kahan bounds for eigenvectors, and Wedin's sin Θ theorem for singular subspaces.

Main results

Matrices are complex and square unless stated otherwise. Singular values σ₀ ≥ σ₁ ≥ ⋯ and eigenvalues λ₀ ≥ λ₁ ≥ ⋯ are sorted and 0-indexed, as in the code. Aₖ is the rank-k truncated SVD.

Result	Statement
SVD svd_decomposition svd_decomposition_rectangular Real.svd_decomposition	A = UΣVᴴ with U, V unitary and Σ diagonal, σᵢ ≥ 0. Also for m × n matrices (Σ rectangular diagonal, σ sorted) and for real matrices (U, V orthogonal).
Norms from σ (m × n) spectral_norm_eq_max_singularValue_rect frobeniusNorm_sq_eq_sum_singularValues_sq_rect	‖A‖₂ = σ₀ and ‖A‖F² = Σᵢ σᵢ²
Courant–Fischer courantFischer_maxMin_bounds courantFischer_minMax_bounds	For Hermitian A with Rayleigh quotient R: λₖ = maxdim W = k+1 min0 ≠ x ∈ W R(x) = mindim W = n−k max0 ≠ x ∈ W R(x)
Weyl weyl_eigenvalue_bounds weyl_singularValue_perturbation weyl_singularValue_rect_perturbation	For Hermitian A, B: λₖ(A) + λₙ₋₁(B) ≤ λₖ(A + B) ≤ λₖ(A) + λ₀(B). For any A, B: |σₖ(A) − σₖ(B)| ≤ σ₀(A − B), square or m × n (with σᵢ = √λᵢ(AᴴA) and ‖A − B‖₂)
Thompson interlacing thompson_interlacing thompson_interlacing_rect	rank B ≤ r ⇒ σᵢ₊ᵣ(A) ≤ σᵢ(A + B) (square / m × n)
Eckart–Young (Frobenius) FrobeniusNorm.eckart_young_frobenius eckart_young_frobenius_rect	rank B ≤ k ⇒ ‖A − Aₖ‖F ≤ ‖A − B‖F (square / m × n)
Eckart–Young (spectral) eckart_young_spectral eckart_young_spectral_rect	rank B ≤ k ⇒ ‖A − Aₖ‖₂ ≤ ‖A − B‖₂ (square / m × n)
Truncation error spectral_error_truncatedSVD(_rect) frobenius_error_truncatedSVD(_rect) truncatedSVD_rect_rank_le	‖A − Aₖ‖₂ = σₖ, ‖A − Aₖ‖F² = Σi≥k σᵢ² and rank Aₖ ≤ k
Uniqueness (Frobenius) eckart_young_frobenius_unique eckart_young_frobenius_rect_unique	σₖ < σₖ₋₁, rank B ≤ k and ‖A − B‖F ≤ ‖A − Aₖ‖F ⇒ B = Aₖ (square / m × n)
Non-uniqueness (spectral) spectral_best_rank_one_not_unique	For A = diag(2, 1), both diag(2, 0) and diag(3/2, 0) minimize ‖A − C‖₂ over rank C ≤ 1
Van Loan–Pitsianis R_kronecker R_frobenius_norm_eq kroneckerApprox_optimal	R(A ⊗ B) = vec(A) vec(B)ᵀ, ‖R(M)‖F = ‖M‖F, and C̃ = R⁻¹ of the rank-1 truncated SVD of R(C) satisfies ‖C − C̃‖F ≤ ‖C − A ⊗ B‖F
Kronecker uniqueness kroneckerApprox_unique	σ₁(R(C)) < σ₀(R(C)) and ‖C − A ⊗ B‖F ≤ ‖C − C̃‖F ⇒ A ⊗ B = C̃
Kronecker approximation kronecker_approx_frobenius_error spectral_error_bound_via_R	‖C − A ⊗ B‖F = ‖R(C) − vec(A) vec(B)ᵀ‖F and ‖C − R⁻¹(M)‖₂ ≤ ‖R(C) − M‖F
Kronecker norm l2_opNorm_kronecker	‖A ⊗ B‖₂ = ‖A‖₂ ‖B‖₂ for rectangular A, B
Spectral vs. Frobenius spectral_eq_frobenius_rect_iff_rank_le_one R_inv_spectral_eq_frobenius_iff_rank_le_one	‖E‖₂ = ‖E‖F ⇔ rank E ≤ 1 (m × n), and ‖R⁻¹X‖₂ = ‖X‖F ⇔ rank R⁻¹X ≤ 1
Coherence coherenceFactorRect_ge_inv_sqrt_rank coherenceFactorRect_le_one coherenceFactor_eq_one_iff	μ(E) = ‖E‖F / (√rank E · ‖E‖₂) lies in [1/√rank E, 1] for E ≠ 0, and μ(E) = 1 iff the nonzero σᵢ are all equal
Stable vs. effective rank stableRank_le_effectiveRank	(‖E‖F / ‖E‖₂)² ≤ exp(−Σᵢ pᵢ log pᵢ) with pᵢ = σᵢ² / ‖E‖F², for E ≠ 0
Davis–Kahan (top eigenvector) davis_kahan_top_eigenvector	A, E Hermitian, ‖E‖₂ < δ = λ₀(A) − λ₁(A), u₀ the top vector of A's eigenvector basis, v a unit top eigenvector of A + E ⇒ ‖v − ⟨u₀, v⟩u₀‖ ≤ ‖E‖₂ / (δ − ‖E‖₂)
Davis–Kahan sin Θ (top-k, Frobenius) davis_kahan_sin_theta	A, E Hermitian, ‖E‖₂ < δ = λₖ₋₁(A) − λₖ(A), P the projection onto A's top-k eigenvectors, ũⱼ the top-k eigenvectors of A + E ⇒ Σⱼ ‖ũⱼ − Pũⱼ‖² ≤ k (‖E‖₂ / (δ − ‖E‖₂))²
Top right singular vector top_right_singular_vector_perturbation top_right_singular_vector_perturbation_of_spectralGap	The top-eigenvector bound for AᴴA vs ÃᴴÃ with gap σ₀(A)² − σ₁(A)²; with η = ‖Ã − A‖₂(‖Ã‖₂ + ‖A‖₂) < γ = (σ₀ − σ₁)‖A‖₂ the bound is η / (γ − η)
Wedin sin Θ (Frobenius, m × n) wedin_sin_theta wedin_sin_theta_l2 wedin_sin_theta_l2_of_norm_lt_gap	à = A + E, σₖ₋₁(A) > 0, δ = σₖ₋₁(Ã) − σₖ(A) > 0, ũⱼ, ṽⱼ the top-k left and right singular vectors of Ã, P_U, P_V the projections onto A's top-k singular subspaces ⇒ Σⱼ (‖ũⱼ − P_U ũⱼ‖² + ‖ṽⱼ − P_V ṽⱼ‖²) ≤ Σⱼ (‖E ṽⱼ‖² + ‖Eᴴ ũⱼ‖²) / δ² ≤ 2k ‖E‖₂² / δ². With A's own gap: ‖E‖₂ < δ_A = σₖ₋₁(A) − σₖ(A) ⇒ the same sum ≤ 2k ‖E‖₂² / (δ_A − ‖E‖₂)²

Names are abbreviated. docs/INDEX.md lists every declaration with its full name, file, line and summary.

Note

Uniqueness is proved only in the Frobenius norm and only under the gap σₖ < σₖ₋₁; in the spectral norm the repo shows by one counterexample that optima need not be unique. Kronecker factors are unique only as the product A ⊗ B, not as the pair (A, B), which can be rescaled. The sin Θ bounds for k > 1 are in Frobenius form (Davis–Kahan with a factor k; Wedin with the gap σₖ₋₁(Ã) − σₖ(A), or A's own gap σₖ₋₁(A) − σₖ(A) when ‖E‖₂ is below it); neither operator-norm form is formalized.

Layout

File	Contents
SVD	Singular values; square, real and rectangular SVD; norms via σ; rectangular coherence factor
KroneckerRearrangement	vec, the rearrangement R and its inverse, Frobenius isometry
CourantFischer	Rayleigh quotients and the min-max theorem
TruncatedSVDRank1	rank A ≤ k ⇒ Aₖ = A
WeylInequality	Weyl eigenvalue and singular-value bounds, Thompson interlacing
FrobeniusNorm	Trace formula, unitary invariance, ‖A − Aₖ‖F² = Σi≥k σᵢ², Eckart–Young (Frobenius)
MatrixNormRelations	‖A‖₂ = σ₀, Eckart–Young (spectral), spectral non-uniqueness, ‖A ⊗ B‖₂, Kronecker perturbation bounds
SpectralNormGap	Spectral-norm bounds for Kronecker approximation through R⁻¹
CoherenceCharacterization	Coherence of the approximation error; Frobenius- vs spectral-optimal rank-1 solutions
TightBounds	Rectangular truncated SVD: error formulas, rank bound, Eckart–Young, Van Loan–Pitsianis
FrobeniusUniqueness	Uniqueness of the Frobenius-optimal truncation under a gap (square, m × n, Kronecker)
DavisKahan	sin θ bounds for the top eigenvector and top-k eigenspaces; top right singular vector
Wedin	Wedin's sin Θ theorem (Frobenius form) for the left and right singular subspaces of m × n matrices

Import graph (an arrow points to the file that imports)

graph TD
  SVD --> CourantFischer
  SVD --> TruncatedSVDRank1
  SVD --> WeylInequality
  CourantFischer --> WeylInequality
  SVD --> FrobeniusNorm
  WeylInequality --> FrobeniusNorm
  FrobeniusNorm --> MatrixNormRelations
  KroneckerRearrangement --> MatrixNormRelations
  MatrixNormRelations --> SpectralNormGap
  MatrixNormRelations --> CoherenceCharacterization
  SpectralNormGap --> CoherenceCharacterization
  MatrixNormRelations --> TightBounds
  SpectralNormGap --> TightBounds
  TightBounds --> FrobeniusUniqueness
  CoherenceCharacterization --> DavisKahan
  DavisKahan --> Wedin

Loading

Proof notes: SVD · Eckart–Young · Kronecker · Davis–Kahan.

Build

elan installs the toolchain pinned in lean-toolchain; Mathlib is pinned by commit in lakefile.toml and lake-manifest.json.

lake exe cache get   # prebuilt Mathlib, once
lake build           # all 13 libraries
lake build SVD       # one library and its imports

To bump Mathlib, set rev in lakefile.toml to the new commit and lean-toolchain to Mathlib's, then run lake update mathlib.

CI builds every library on each push to main and each pull request, and fails on:

• any build warning;
• a declaration that depends on an axiom other than propext, Classical.choice and Quot.sound (scripts/CheckAxioms.lean);
• sorry, admit or axiom in the sources;
• a stale docs/INDEX.md.

Citation

@software{flywheel2025,
  author  = {Markovski, Aleksandar},
  title   = {{FLYWHEEL}: Formalized Linear Algebra in Lean 4},
  year    = {2025},
  url     = {https://github.com/acomarce/FLYWHEEL},
  license = {Apache-2.0}
}

References

• C. Davis, W. M. Kahan. The rotation of eigenvectors by a perturbation. III. SIAM J. Numer. Anal. 7(1), 1–46, 1970.
• C. Eckart, G. Young. The approximation of one matrix by another of lower rank. Psychometrika 1(3), 211–218, 1936.
• H. Weyl. Das asymptotische Verteilungsgesetz der Eigenwerte linearer partieller Differentialgleichungen. Math. Ann. 71, 441–479, 1912.
• C. F. Van Loan, N. Pitsianis. Approximation with Kronecker products. In Linear Algebra for Large Scale and Real-Time Applications, 293–314, 1993.
• R. A. Horn, C. R. Johnson. Matrix Analysis, 2nd ed. Cambridge University Press, 2012.
• G. H. Golub, C. F. Van Loan. Matrix Computations, 4th ed. Johns Hopkins University Press, 2013.

License

Apache 2.0