Skip to content

v4.31.0

Choose a tag to compare

View all tags
@YuanheZ YuanheZ released this 03 Jul 17:38
v4.31.0
148db35

v4.31.0

This release upgrades SLT to Lean and Mathlib v4.31.0 and upstreams the local matrix concentration development.

Highlights

  • Pins lean-toolchain, lakefile.lean, and lake-manifest.json to Lean 4.31.0 and Mathlib v4.31.0.
  • Adds SLT.MatrixInfra, covering singular values, SVD and spectral decompositions, Courant-Fischer min-max principles, Eckart-Young-Mirsky, Weyl perturbation, Davis-Kahan, Loewner/matrix calculus, and deterministic Lieb concavity for HDP Theorem 5.4.8.
  • Adds SLT.HansonWright, deriving Hanson-Wright MGF certificates from independent sub-Gaussian or bounded coordinates and proving HDP-style Hanson-Wright tail bounds.
  • Adds SLT.RMT random-matrix results: rectangular and symmetric sub-Gaussian operator-norm bounds, expectation forms, lower bounds, two-sided singular-value bounds for isotropic sub-Gaussian rows, the random-matrix Lieb step, and the finite matrix Bernstein inequality.
  • Adds SLT.TDudley, a truncated Dudley entropy bound using subset nets, local/global oscillation controls, and the existing metric-entropy API.
  • Extends SLT.SubGaussian with scalar IsSubGaussian, ψ₂-scale infrastructure, Bernstein-style CGF tail bounds, finite-supremum integrability lemmas, and compatibility with Mathlib HasSubgaussianMGF.
  • Updates existing Gaussian, Poincare, Dudley, and least-squares files for Lean 4.31 and Mathlib API changes while preserving the prior development.

Verification

  • LEAN_NUM_THREADS=$(nproc) lake build completed successfully.
  • Scanned SLT/ for sorry, admit, axiom, and native_decide; none were found.
Assets 2
Loading