v4.32.0

v4.32.0

This release upgrades SLT to Lean and Mathlib v4.32.0 and updates the formalization for the corresponding API changes.

Highlights

• Pins lean-toolchain, lakefile.lean, and lake-manifest.json to Lean 4.32.0 and Mathlib v4.32.0.
• Updates Gaussian Sobolev cutoff measurability and Gaussian Poincare mapped-integral proofs for v4.32.0 elaboration changes.
• Updates Hanson-Wright and random-matrix measurability proofs by making pointwise multiplication and negation explicit.
• Updates tensorized Gaussian log-Sobolev measurability proofs and removes an obsolete simplification argument exposed by the v4.32.0 linters.
• Refreshes the project README and adds the repository license while preserving the existing formalized statistical-learning and random-matrix development.

Verification

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

v4.31.0

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.