HighDimProb0.1.0
Lean 4 formalizations for high-dimensional probability, random matrices, concentration inequalities, and matrix Bernstein bounds.
Sort by
Require Order
mathlib
v4.29.1The math library of Lean 4
HighDimProb0.1.0v4.29.1