Rocq proofs, checked by the kernel, of the sharp threshold for random ellipsoid fitting and of new results on optimal conditioning, mixtures, dependent laws and translated samples, with the reusable library GaussianAnalysis.
coq probability theorem-proving formal-verification mathcomp random-matrices rocq mathcomp-analysis ellipsoid-fitting
-
Updated
Oct 27, 2026 - Rocq Prover